Fix breakableFill: do not impose alignment.

[haskell/symantic.git] / symantic / Language / Symantic / Compiling / Read.hs

diff --git a/symantic/Language/Symantic/Compiling/Read.hs b/symantic/Language/Symantic/Compiling/Read.hs
index 355ba52f9c681407db36c0089ebd560b2366feac..25201b42345cfce5cee873e2204f02bde564ccb1 100644 (file)
--- a/symantic/Language/Symantic/Compiling/Read.hs
+++ b/symantic/Language/Symantic/Compiling/Read.hs
@@ -19,15 +19,13 @@ type ReadTerm src ss ts =
  SourceInj (KindK src) src =>
  SourceInj (AST_Type src) src =>
  Constable (->) =>
- Imports NameTy ->
- ModulesTy src ->
  CtxTy src ts ->
  AST_Term src ss ->
  Either (Error_Term src) (TermVT src ss ts)
 
 -- | Read a 'TermVT' from and 'AST_Term'.
 readTerm :: forall src ss ts. ReadTerm src ss ts
-readTerm impsTy modsTy ctxTy ast = do
+readTerm ctxTy ast = do
        ts <- go ctxTy `traverse` ast
        errorInj `left` betaTerms ts
        where
@@ -41,12 +39,12 @@ readTerm impsTy modsTy ctxTy ast = do
        go ts  (Token_Term_Var _src name) = teVar name ts
        go _ts (Token_Term_App _src)      = Right $ TermVT teApp
        go ts  (Token_Term_Abst _src name_arg ast_ty_arg ast_body) = do
-               TypeVT ty_arg <- errorInj `left` readType impsTy modsTy ast_ty_arg
+               TypeVT ty_arg <- errorInj `left` readType ast_ty_arg
                when_EqKind (kindInj @K.Type) (kindOf ty_arg) $ \Refl ->
                        case lenVars ty_arg of
                         LenS{} -> Left $ Error_Term_polymorphic $ TypeVT ty_arg
                         LenZ | (TypeK qa, TypeK ta) <- unQualTy ty_arg -> do
-                               TermVT (Term qr tr (TeSym res)) <- readTerm impsTy modsTy (CtxTyS name_arg ta ts) ast_body
+                               TermVT (Term qr tr (TeSym res)) <- readTerm (CtxTyS name_arg ta ts) ast_body
                                let (qa', qr') = appendVars qa qr
                                let (ta', tr') = appendVars ta tr
                                Right $
@@ -65,11 +63,11 @@ readTerm impsTy modsTy ctxTy ast = do
                                                Term (qa' # qr') (ta' ~> tr') $
                                                TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c)
        go ts (Token_Term_Let _src name ast_arg ast_body) = do
-               TermVT (Term qa ta (TeSym arg)) <- readTerm impsTy modsTy ts ast_arg
+               TermVT (Term qa ta (TeSym arg)) <- readTerm ts ast_arg
                case lenVars ta of
                 LenS{} -> Left $ Error_Term_polymorphic $ TypeVT (qa #> ta)
                 LenZ -> do
-                       TermVT (Term qr tr (TeSym res)) <- readTerm impsTy modsTy (CtxTyS name ta ts) ast_body
+                       TermVT (Term qr tr (TeSym res)) <- readTerm (CtxTyS name ta ts) ast_body
                        let (qa', qr') = appendVars qa qr
                        let tr' = allocVarsL (lenVars ta) tr
                        Right $
@@ -143,8 +141,6 @@ readTermWithCtx ::
  SourceInj (AST_Type src) src =>
  Constable (->) =>
  f (NameTe, TermT src ss '[] '[]) ->
- Imports NameTy ->
- ModulesTy src ->
  AST_Term src ss ->
  Either (Error_Term src) (TermVT src ss '[])
 readTermWithCtx env =
@@ -167,8 +163,8 @@ readTermWithCtxPush1 ::
  (NameTe, TermT src ss '[] '[]) ->
  (forall ts'. ReadTerm src ss ts') ->
  ReadTerm src ss ts
-readTermWithCtxPush1 (n, TermT (Term qn tn (TeSym te_n))) readTe impsTy modsTy ctxTy ast = do
-       TermVT (Term q t (TeSym te)) <- readTe impsTy modsTy (CtxTyS n (qn #> tn) ctxTy) ast
+readTermWithCtxPush1 (n, TermT (Term qn tn (TeSym te_n))) readTe ctxTy ast = do
+       TermVT (Term q t (TeSym te)) <- readTe (CtxTyS n (qn #> tn) ctxTy) ast
        case proveConstraint qn of
         Nothing -> Left $ Error_Term_proofless $ TypeVT qn
         Just Dict ->
@@ -184,11 +180,9 @@ readTermWithCtxClose ::
  SourceInj (KindK src) src =>
  SourceInj (AST_Type src) src =>
  Constable (->) =>
- Imports NameTy ->
- ModulesTy src ->
  AST_Term src ss ->
  Either (Error_Term src) (TermVT src ss '[])
-readTermWithCtxClose readTe impsTy modsTy = readTe impsTy modsTy CtxTyZ
+readTermWithCtxClose readTe = readTe CtxTyZ
 
 -- * Type 'CtxTy'
 -- | /Typing context/