From a7d029e669b313d76676c69bbd8b118218f6341b Mon Sep 17 00:00:00 2001 From: Anders Date: Fri, 10 Apr 2015 15:41:24 +0200 Subject: [PATCH] Fix parsing of trans, comp, etc. --- Exp.cf | 35 +++++++++++++++--------------- Resolver.hs | 53 ++++++++++++++++----------------------------- examples/circle.ctt | 5 ----- 3 files changed, 37 insertions(+), 56 deletions(-) diff --git a/Exp.cf b/Exp.cf index 398ef38..f65dc35 100644 --- 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 8d37210..76ec78f 100644 --- 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 db62a60..b753115 100644 --- 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 - -- 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 -- 2.34.1