Fix parsing of trans, comp, etc.

diff --git a/Exp.cf b/Exp.cf
index 398ef387e04f8d0c813a1f1a07cccc51c59e5b1f..f65dc3572becb3383f9c8a031c697a64ef92ebb0 100644 (file)
--- a/Exp.cf
+++ b/Exp.cf
@@ -3,7 +3,7 @@ entrypoints Module, Exp ;
 comment "--" ;
 comment "{-" "-}" ;
 
-layout "where", "let", "mutual", "split" ;
+layout "where", "let", "split" ;
 layout stop "in" ;
 -- Do not use layout toplevel as it makes pExp fail!
 
@@ -28,27 +28,28 @@ Fun.        Exp1 ::= Exp2 "->" Exp1 ;
 Pi.         Exp1 ::= [PTele] "->" Exp1 ;
 Sigma.      Exp1 ::= [PTele] "*" Exp1 ;
 App.        Exp2 ::= Exp2 Exp3 ;
-Var.        Exp3 ::= AIdent ;
-AppFormula. Exp3 ::= Exp3 "@" Formula ;
-U.          Exp3 ::= "U" ;
-PCon.       Exp3 ::= AIdent "{" Exp "}" ; -- c{T A B} x1 x2 @ phi
-Fst.        Exp3 ::= Exp3 ".1" ;
-Snd.        Exp3 ::= Exp3 ".2" ;
-IdP.        Exp3 ::= "IdP" ;
-Trans.      Exp3 ::= "transport" ;
-Comp.       Exp3 ::= "comp" ;
-Glue.       Exp3 ::= "glue" ;
-GlueElem.   Exp3 ::= "glueElem" ;
-CompElem.   Exp3 ::= "compElem" ;
-ElimComp.   Exp3 ::= "elimComp" ;
-System.     Exp3 ::= "[" [Side] "]" ;
-Pair.       Exp3 ::= "(" Exp "," [Exp] ")" ;
-coercions Exp 3 ;
+IdP.        Exp3 ::= "IdP" Exp4 Exp4 Exp4 ;
+Trans.      Exp3 ::= "transport" Exp4 Exp4 ;
+Comp.       Exp3 ::= "comp" Exp4 Exp4 System ;
+Glue.       Exp3 ::= "glue" Exp4 System ;
+GlueElem.   Exp3 ::= "glueElem" Exp4 System ;
+CompElem.   Exp3 ::= "compElem" Exp4 System Exp4 System ;
+ElimComp.   Exp3 ::= "elimComp" Exp4 System Exp4 ;
+Fst.        Exp4 ::= Exp4 ".1" ;
+Snd.        Exp4 ::= Exp4 ".2" ;
+AppFormula. Exp5 ::= Exp5 "@" Formula ;
+Pair.       Exp5 ::= "(" Exp "," [Exp] ")" ;
+Var.        Exp5 ::= AIdent ;
+PCon.       Exp5 ::= AIdent "{" Exp "}" ; -- c{T A B} x1 x2 @ phi
+U.          Exp5 ::= "U" ;
+coercions Exp 5 ;
 separator nonempty Exp "," ;
 
 Dir0.       Dir ::= "0" ;
 Dir1.       Dir ::= "1" ;
 
+System.     System ::= "[" [Side] "]" ;
+
 Face.     Face ::= "(" AIdent "=" Dir ")" ;
 separator Face "" ;
 

diff --git a/Resolver.hs b/Resolver.hs
index 8d37210af78448a7df1e1f42f9bb1547d4196821..76ec78fd302a241275f1d5c8e6a3b7a20b881933 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -168,34 +168,6 @@ binds :: (Ter -> Ter) -> [(Ident,Exp)] -> Resolver Ter -> Resolver Ter
 binds f = flip $ foldr $ bind f
 
 resolveApps :: Exp -> [Exp] -> Resolver Ter
-resolveApps Trans (x:y:xs) = do
-  let c = CTT.Trans <$> resolveExp x <*> resolveExp y
-  CTT.mkApps <$> c <*> mapM resolveExp xs
-resolveApps IdP (x:y:z:xs) = do
-  let c = CTT.IdP <$> resolveExp x <*> resolveExp y <*> resolveExp z
-  CTT.mkApps <$> c <*> mapM resolveExp xs
-resolveApps Comp (u:v:ts:xs) = do
-  let c = CTT.Comp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
-  CTT.mkApps <$> c <*> mapM resolveExp xs
-resolveApps Glue (u:ts:xs) = do
-  rs <- resolveSystem ts
-  let isIso (CTT.Pair _ (CTT.Pair _ (CTT.Pair _ (CTT.Pair _ _)))) = True
-      isIso _ = False
-  unless (all isIso $ Map.elems rs)
-    (throwError $ "Not a system of isomorphisms: " ++ show rs)
-  let c = CTT.Glue <$> resolveExp u <*> pure rs
-  CTT.mkApps <$> c <*> mapM resolveExp xs
-resolveApps GlueElem (u:ts:xs) = do
-  let c = CTT.GlueElem <$> resolveExp u <*> resolveSystem ts
-  CTT.mkApps <$> c <*> mapM resolveExp xs
-resolveApps CompElem (a:es:t:ts:xs) = do
-  let c = CTT.CompElem <$> resolveExp a <*> resolveSystem es
-          <*> resolveExp t <*> resolveSystem ts
-  CTT.mkApps <$> c <*> mapM resolveExp xs
-resolveApps ElimComp (a:es:t:xs) = do
-  let c = CTT.ElimComp <$> resolveExp a <*> resolveSystem es
-          <*> resolveExp t
-  CTT.mkApps <$> c <*> mapM resolveExp xs
 resolveApps x xs = CTT.mkApps <$> resolveExp x <*> mapM resolveExp xs
 
 resolveExp :: Exp -> Resolver Ter
@@ -227,23 +199,36 @@ resolveExp e = case e of
   AppFormula e phi ->
     let (x,xs) = unApps e []
     in case x of
-      PCon n a -> CTT.PCon (unAIdent n) <$> resolveExp a
-                                        <*> mapM resolveExp xs
-                                        <*> resolveFormula phi
+      PCon n a ->
+        CTT.PCon (unAIdent n) <$> resolveExp a <*> mapM resolveExp xs
+                              <*> resolveFormula phi
       _ -> CTT.AppFormula <$> resolveExp e <*> resolveFormula phi
-  _             -> do
+  Trans x y   -> CTT.Trans <$> resolveExp x <*> resolveExp y
+  IdP x y z   -> CTT.IdP <$> resolveExp x <*> resolveExp y <*> resolveExp z
+  Comp u v ts -> CTT.Comp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
+  Glue u ts   -> do
+    rs <- resolveSystem ts
+    let isIso (CTT.Pair _ (CTT.Pair _ (CTT.Pair _ (CTT.Pair _ _)))) = True
+        isIso _ = False
+    unless (all isIso $ Map.elems rs)
+      (throwError $ "Not a system of isomorphisms: " ++ show rs)
+    CTT.Glue <$> resolveExp u <*> pure rs
+  GlueElem u ts      -> CTT.GlueElem <$> resolveExp u <*> resolveSystem ts
+  CompElem a es t ts -> CTT.CompElem <$> resolveExp a <*> resolveSystem es
+                                     <*> resolveExp t <*> resolveSystem ts
+  ElimComp a es t    -> CTT.ElimComp <$> resolveExp a <*> resolveSystem es <*> resolveExp t
+  _ -> do
     modName <- asks envModule
     throwError ("Could not resolve " ++ show e ++ " in module " ++ modName)
 
 resolveWhere :: ExpWhere -> Resolver Ter
 resolveWhere = resolveExp . unWhere
 
-resolveSystem :: Exp -> Resolver (C.System Ter)
+resolveSystem :: System -> Resolver (C.System Ter)
 resolveSystem (System ts) =
   -- Note: the symbols in alpha are in scope in u, but they mean 0 or 1
   Map.fromList <$> sequence [ (,) <$> resolveFace alpha <*> resolveExp u
                             | Side alpha u <- ts ]
-resolveSystem e = throwError $ show e ++ " is not a system"
 
 resolveFace :: [Face] -> Resolver C.Face
 resolveFace alpha =

diff --git a/examples/circle.ctt b/examples/circle.ctt
index db62a60cef1503350199489e1682780a1f72ae42..b753115486be0c28e19378b4e05617ee01909bc3 100644 (file)
--- a/examples/circle.ctt
+++ b/examples/circle.ctt
@@ -30,11 +30,6 @@ mLoop : (x : S1) -> Id S1 x x = split
   base -> loop'
   loop @ i -> (constSquare S1 base loop') @ i
 
-  -- <i> let rem : S1 -> S1 = split
-  --           base -> loop' @ i
-  --           loop @ j -> ((constSquare S1 base loop') @ j) @ i
-  --     in rem x
-
 mult (x : S1) : S1 -> S1 = split
   base -> x
   loop @ i -> (mLoop x) @ i