Parsing of systems

diff --git a/Connections.hs b/Connections.hs
index 61002dc73ad114a14d7f5d384273282fb1c30a02..c9facd9841d65402672ffe806f29214a89753ada 100644 (file)
--- 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 92a2da4d2b62c9e26d01ee1258686caf3bcbf439..2bf3b0c83537f92569f86faebca9908629cca4e2 100644 (file)
--- 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 f0a431da78aa0cfd849b93a6b1317199463a5415..ce03e9089eca690ab6747fbe298710edc909b7df 100644 (file)
--- 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 2f736b425ef808f8595400caaae966c8260c5b20..68f3dbc1e4fd9620c82be8201ff003a90191f761 100644 (file)
--- 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) = <i> (p @ i,<j> p @ i & j)
+  Id (singl A a) (a,refl A a) (b,p) = <i> (p @ i,<j> 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 =
+  <i> comp A (p @ i) [ (i = 1) -> q ]
\ No newline at end of file