From 1c760bdb234959d6b5c4e6952e0a023521f95b0b Mon Sep 17 00:00:00 2001 From: Anders Date: Thu, 19 Mar 2015 17:14:21 +0100 Subject: [PATCH] Parsing of systems --- Connections.hs | 24 ++++++++++++---------- Exp.cf | 20 ++++++++++++++----- Resolver.hs | 52 ++++++++++++++++++++++++++++++++++++------------ examples/nat.ctt | 7 +++++-- 4 files changed, 73 insertions(+), 30 deletions(-) diff --git a/Connections.hs b/Connections.hs index 61002dc..c9facd9 100644 --- a/Connections.hs +++ b/Connections.hs @@ -129,8 +129,20 @@ data Formula = Dir Dir | NegAtom Name | Formula :/\: Formula | Formula :\/: Formula - deriving (Eq,Show) - + deriving Eq + +instance Show Formula where + show (Dir Zero) = "0" + show (Dir One) = "1" + show (NegAtom a) = "-" ++ show a + show (Atom a) = show a + show (a :\/: b) = show1 a ++ " \\/ " ++ show1 b + where show1 v@(a :/\: b) = "(" ++ show v ++ ")" + show1 a = show a + show (a :/\: b) = show1 a ++ " /\\ " ++ show1 b + where show1 v@(a :\/: b) = "(" ++ show v ++ ")" + show1 a = show a + arbFormula :: [Name] -> Int -> Gen Formula arbFormula names s = frequency [ (1, Dir <$> arbitrary) @@ -158,14 +170,6 @@ instance ToFormula Name where instance ToFormula Dir where toFormula = Dir --- TODO: FINISH! --- instance Show a => Show (Formula a) where --- show Zero = "0" --- show One = "1" --- show (NegAtom a) = "~" ++ show a --- show (Atom a) = show a --- show (a :/\: b) = show a ++ " /\ " ++ show b - negFormula :: Formula -> Formula negFormula (Dir b) = Dir (- b) negFormula (Atom i) = NegAtom i diff --git a/Exp.cf b/Exp.cf index 92a2da4..2bf3b0c 100644 --- a/Exp.cf +++ b/Exp.cf @@ -35,15 +35,25 @@ Fst. Exp3 ::= Exp3 ".1" ; Snd. Exp3 ::= Exp3 ".2" ; IdP. Exp3 ::= "IdP" ; Trans. Exp3 ::= "transport" ; +Comp. Exp3 ::= "comp" ; +System. Exp3 ::= "[" [Side] "]" ; Pair. Exp3 ::= "(" Exp "," Exp ")" ; coercions Exp 3 ; -Disj. Formula ::= Formula "|" Formula1 ; -Conj. Formula1 ::= Formula1 "&" Formula2 ; +Dir0. Dir ::= "0" ; +Dir1. Dir ::= "1" ; + +Face. Face ::= "(" AIdent "=" Dir ")" ; +separator Face "" ; + +Side. Side ::= [Face] "->" Exp ; +separator Side "," ; + +Disj. Formula ::= Formula "\\/" Formula1 ; +Conj. Formula1 ::= Formula1 "/\\ " Formula2 ; -- Why do we need a space? Neg. Formula2 ::= "-" Formula2 ; Atom. Formula2 ::= AIdent ; -Dir0. Formula2 ::= "0" ; -Dir1. Formula2 ::= "1" ; +Dir. Formula2 ::= Dir ; coercions Formula 2 ; -- Branches @@ -63,5 +73,5 @@ terminator Tele "" ; PTele. PTele ::= "(" Exp ":" Exp ")" ; terminator nonempty PTele "" ; -position token AIdent ((letter|'\''|'_')(letter|digit|'\''|'_')*) ; +position token AIdent ((letter|'_')(letter|digit|'\''|'_')*) ; terminator AIdent "" ; \ No newline at end of file diff --git a/Resolver.hs b/Resolver.hs index f0a431d..ce03e90 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -15,6 +15,8 @@ import Control.Monad.Error (throwError) import Control.Monad (when) import Data.Functor.Identity import Data.List (nub) +import Data.Map (Map,(!)) +import qualified Data.Map as Map import Prelude hiding (pi) type Ter = CTT.Ter @@ -50,7 +52,7 @@ appsToIdents = mapM unVar . uncurry (:) . flip unApps [] -- Flatten a tele flattenTele :: [Tele] -> [(Ident,Exp)] flattenTele tele = - [ (resolveIdent i,typ) | Tele id ids typ <- tele, i <- id:ids ] + [ (unAIdent i,typ) | Tele id ids typ <- tele, i <- id:ids ] -- Flatten a PTele flattenPTele :: [PTele] -> Resolver [(Ident,Exp)] @@ -115,11 +117,17 @@ getLoc l = CTT.Loc <$> asks envModule <*> pure l -- resolveAIdent :: AIdent -> Resolver (Ident,CTT.Loc) -- resolveAIdent (AIdent (l,x)) = (x,) <$> getLoc l -resolveIdent :: AIdent -> Ident -resolveIdent (AIdent (_,x)) = x +unAIdent :: AIdent -> Ident +unAIdent (AIdent (_,x)) = x -resolveName :: AIdent -> C.Name -resolveName (AIdent (_,n)) = C.Name n +resolveName :: AIdent -> Resolver C.Name +resolveName (AIdent (l,x)) = do + modName <- asks envModule + vars <- asks variables + case lookup x vars of + Just Name -> return $ C.Name x + _ -> throwError $ "Cannot resolve name " ++ x ++ " at position " ++ + show l ++ " in module " ++ modName resolveVar :: AIdent -> Resolver Ter resolveVar (AIdent (l,x)) @@ -155,6 +163,9 @@ resolveApps Trans (x:y:xs) = do 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 x xs = CTT.mkApps <$> resolveExp x <*> mapM resolveExp xs resolveExp :: Exp -> Resolver Ter @@ -180,16 +191,31 @@ resolveExp e = case e of (rdecls,names) <- resolveDecls decls CTT.mkWheres rdecls <$> local (insertIdents names) (resolveExp e) Path i e -> - CTT.Path (resolveName i) <$> local (insertName i) (resolveExp e) + CTT.Path (C.Name (unAIdent i)) <$> local (insertName i) (resolveExp e) AppFormula e phi -> CTT.AppFormula <$> resolveExp e <*> resolveFormula phi resolveWhere :: ExpWhere -> Resolver Ter resolveWhere = resolveExp . unWhere +resolveSystem :: Exp -> Resolver (C.System Ter) +resolveSystem (System ts) = + -- TODO: Erase alpha when resolving u?? + 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 = + Map.fromList <$> sequence [ (,) <$> resolveName i <*> resolveDir d + | Face i d <- alpha ] + +resolveDir :: Dir -> Resolver C.Dir +resolveDir Dir0 = return 0 +resolveDir Dir1 = return 1 + resolveFormula :: Formula -> Resolver C.Formula -resolveFormula Dir0 = return $ C.Dir 0 -resolveFormula Dir1 = return $ C.Dir 1 -resolveFormula (Atom i) = return $ C.Atom $ resolveName i +resolveFormula (Dir d) = C.Dir <$> resolveDir d +resolveFormula (Atom i) = C.Atom <$> resolveName i resolveFormula (Neg phi) = C.negFormula <$> resolveFormula phi resolveFormula (Conj phi psi) = C.andFormula <$> resolveFormula phi <*> resolveFormula psi @@ -199,7 +225,7 @@ resolveFormula (Disj phi psi) = C.orFormula <$> resolveFormula phi resolveBranch :: Branch -> Resolver (CTT.Label,([CTT.Label],Ter)) resolveBranch (Branch (AIdent (_,lbl)) args e) = do re <- local (insertAIdents args) $ resolveWhere e - return (lbl, (map resolveIdent args, re)) + return (lbl, (map unAIdent args, re)) resolveTele :: [(Ident,Exp)] -> Resolver CTT.Tele resolveTele [] = return [] @@ -207,10 +233,10 @@ resolveTele ((i,d):t) = ((i,) <$> resolveExp d) <:> local (insertVar i) (resolveTele t) resolveLabel :: Label -> Resolver (CTT.Label,CTT.Tele) -resolveLabel (Label n vdecl) = (resolveIdent n,) <$> resolveTele (flattenTele vdecl) +resolveLabel (Label n vdecl) = (unAIdent n,) <$> resolveTele (flattenTele vdecl) declsLabels :: [Decl] -> [Ident] -declsLabels decls = map resolveIdent [ lbl | Label lbl _ <- sums ] +declsLabels decls = map unAIdent [ lbl | Label lbl _ <- sums ] where sums = concat [ sum | DeclData _ _ sum <- decls ] piToFam :: Exp -> Resolver Ter @@ -232,7 +258,7 @@ resolveDecl d = case d of a <- binds CTT.Pi tele' (return CTT.U) d <- lams tele' $ local (insertVar f) $ CTT.Sum <$> getLoc l <*> pure f <*> mapM resolveLabel sums - let cs = map resolveIdent [ lbl | Label lbl _ <- sums ] + let cs = map unAIdent [ lbl | Label lbl _ <- sums ] return ((f,(a,d)),(f,Variable):map (,Constructor) cs) DeclSplit (AIdent (l,f)) tele t brs -> do let tele' = flattenTele tele diff --git a/examples/nat.ctt b/examples/nat.ctt index 2f736b4..68f3dbc 100644 --- a/examples/nat.ctt +++ b/examples/nat.ctt @@ -62,7 +62,7 @@ substRefl (A : U) (P : A -> U) (a : A) (e : P a) : Id (P a) (subst A P a a (refl singl (A : U) (a : A) : U = (x : A) * Id A a x contrSingl (A : U) (a b : A) (p : Id A a b) : - Id (singl A a) (a,refl A a) (b,p) = (p @ i, p @ i & j) + Id (singl A a) (a,refl A a) (b,p) = (p @ i, p @ i /\ j) J (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d : C a (refl A a)) (x : A) (p : Id A a x) : C x p = @@ -73,4 +73,7 @@ defEqJ (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d : C a (refl A a)) : Id (C a (refl A a)) (J A a C d a (refl A a)) d = refl (C a (refl A a)) d test0 (A : U) (a b : A) (p : Id A a b) : Id A a a = refl A (p @ 0) -test1 (A : U) (a b : A) (p : Id A a b) : Id A b b = refl A (p @ 1) \ No newline at end of file +test1 (A : U) (a b : A) (p : Id A a b) : Id A b b = refl A (p @ 1) + +compId (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c = + comp A (p @ i) [ (i = 1) -> q ] \ No newline at end of file -- 2.34.1