From 9e5e016fe468c74997f1c76851381ca2b91f781f Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 19 Mar 2015 08:15:30 +0100 Subject: [PATCH] Names are now strings --- Connections.hs | 16 ++++++++-------- Exp.cf | 9 +++------ Resolver.hs | 17 ++++++++++++----- TypeChecker.hs | 20 +++++++++++++------- examples/nat.ctt | 10 +++++----- 5 files changed, 41 insertions(+), 31 deletions(-) diff --git a/Connections.hs b/Connections.hs index 6e6bb18..a40b7cc 100644 --- a/Connections.hs +++ b/Connections.hs @@ -11,11 +11,11 @@ import qualified Data.Set as Set import Data.Maybe import Test.QuickCheck -newtype Name = Name Integer +newtype Name = Name String deriving (Arbitrary,Eq,Ord) instance Show Name where - show (Name i) = 'i' : show i + show (Name i) = i swapName :: Name -> (Name,Name) -> Name swapName k (i,j) | k == i = j @@ -137,7 +137,7 @@ arbFormula names s = instance Arbitrary Formula where arbitrary = do n <- arbitrary :: Gen Integer - sized $ arbFormula (map Name [0..(abs n)]) + sized $ arbFormula (map (\x -> Name ('?' : show x)) [0..(abs n)]) class ToFormula a where toFormula :: a -> Formula @@ -211,14 +211,14 @@ propInvFormulaIncomp phi b = incomparables (invFormula phi b) -- prop_invFormula phi b = -- all (\alpha -> phi `evalFormula` alpha == Dir b) (invFormula phi b) -testInvFormula :: [Face] -testInvFormula = invFormula (Atom (Name 0) :/\: Atom (Name 1)) 1 +-- testInvFormula :: [Face] +-- testInvFormula = invFormula (Atom (Name 0) :/\: Atom (Name 1)) 1 -- | Nominal gensym :: [Name] -> Name -gensym [] = Name 0 -gensym xs = Name (max+1) - where Name max = maximum xs +gensym [] = Name "?0" +gensym xs = Name ('?' : show (max+1)) + where max = maximum [ read x | Name ('?':x) <- xs ] gensyms :: [Name] -> [Name] gensyms d = let x = gensym d in x : gensyms (x : d) diff --git a/Exp.cf b/Exp.cf index 6386d33..cb62399 100644 --- a/Exp.cf +++ b/Exp.cf @@ -23,7 +23,7 @@ NoWhere. ExpWhere ::= Exp ; Let. Exp ::= "let" "{" [Decl] "}" "in" Exp ; Lam. Exp ::= "\\" [PTele] "->" Exp ; -Path. Exp ::= "<" Name ">" Exp ; +Path. Exp ::= "<" AIdent ">" Exp ; Fun. Exp1 ::= Exp2 "->" Exp1 ; Pi. Exp1 ::= [PTele] "->" Exp1 ; Sigma. Exp1 ::= [PTele] "*" Exp1 ; @@ -41,7 +41,7 @@ coercions Exp 3 ; Disj. Formula ::= Formula "|" Formula1 ; Conj. Formula1 ::= Formula1 "&" Formula2 ; Neg. Formula2 ::= "-" Formula2 ; -Atom. Formula2 ::= Name ; +Atom. Formula2 ::= AIdent ; coercions Formula 2 ; -- Branches @@ -62,7 +62,4 @@ PTele. PTele ::= "(" Exp ":" Exp ")" ; terminator nonempty PTele "" ; position token AIdent ((letter|'\''|'_')(letter|digit|'\''|'_')*) ; -terminator AIdent "" ; - -position token Name (('?')(digit)*); -terminator Name "" ; \ No newline at end of file +terminator AIdent "" ; \ No newline at end of file diff --git a/Resolver.hs b/Resolver.hs index 8dc8719..81e94ed 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -62,7 +62,7 @@ flattenPTele (PTele exp typ : xs) = case appsToIdents exp of ------------------------------------------------------------------------------- -- | Resolver and environment -data SymKind = Variable | Constructor +data SymKind = Variable | Constructor | Name deriving (Eq,Show) -- local environment for constructors @@ -95,6 +95,9 @@ insertVar x = insertBinder (x,Variable) insertVars :: [CTT.Binder] -> Env -> Env insertVars = flip $ foldr insertVar +insertName :: CTT.Binder -> Env -> Env +insertName x = insertBinder (x,Name) + getLoc :: (Int,Int) -> Resolver CTT.Loc getLoc l = CTT.Loc <$> asks envModule <*> pure l @@ -104,8 +107,8 @@ noLoc = AIdent ((0,0),"_") resolveAIdent :: AIdent -> Resolver CTT.Binder resolveAIdent (AIdent (l,x)) = (x,) <$> getLoc l -resolveName :: Name -> Resolver C.Name -resolveName (Name (_,n)) = return $ C.Name $ read $ tail n +resolveName :: AIdent -> Resolver C.Name +resolveName (AIdent (_,n)) = return $ C.Name n resolveVar :: AIdent -> Resolver Ter resolveVar (AIdent (l,x)) @@ -116,6 +119,9 @@ resolveVar (AIdent (l,x)) case CTT.lookupIdent x vars of Just Variable -> return $ CTT.Var x Just Constructor -> return $ CTT.Con x [] + Just Name -> + throwError $ "Name " ++ x ++ " used as a variable at position " ++ + show l ++ " in module " ++ modName _ -> throwError $ "Cannot resolve variable " ++ x ++ " at position " ++ show l ++ " in module " ++ modName @@ -165,7 +171,9 @@ resolveExp e = case e of Let decls e -> do (rdecls,names) <- resolveDecls decls CTT.mkWheres rdecls <$> local (insertBinders names) (resolveExp e) - Path i e -> CTT.Path <$> resolveName i <*> resolveExp e + Path i e -> do + x <- resolveAIdent i + CTT.Path <$> resolveName i <*> local (insertName x) (resolveExp e) AppFormula e phi -> CTT.AppFormula <$> resolveExp e <*> resolveFormula phi resolveWhere :: ExpWhere -> Resolver Ter @@ -179,7 +187,6 @@ resolveFormula (Conj phi psi) = C.andFormula <$> resolveFormula phi resolveFormula (Disj phi psi) = C.orFormula <$> resolveFormula phi <*> resolveFormula psi - resolveBranch :: Branch -> Resolver (CTT.Label,([CTT.Binder],Ter)) resolveBranch (Branch (AIdent (_,lbl)) args e) = do binders <- mapM resolveAIdent args diff --git a/TypeChecker.hs b/TypeChecker.hs index 13ca00b..1a33798 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -238,13 +238,10 @@ infer e = case e of VIdP a _ _ -> return $ a @@ phi _ -> throwError (show e ++ " is not a path") Trans p t -> case p of - Path i a -> do - rho <- asks env - when (i `elem` support rho) - (throwError $ show i ++ " is already declared") - local (addSub (i,Atom i)) $ check VU a - check (eval (Sub rho (i,Dir 0)) a) t - return $ (eval (Sub rho (i,Dir 1)) a) + Path{} -> do + (a0,a1) <- checkPath p + check a0 t + return a1 _ -> do b <- infer p case b of @@ -252,6 +249,15 @@ infer e = case e of _ -> throwError $ "transport expects a path but got " ++ show p _ -> throwError ("infer " ++ show e) +-- Check that a term is a path and output the source and target +checkPath :: Ter -> Typing (Val,Val) +checkPath (Path i a) = do + rho <- asks env + when (i `elem` support rho) + (throwError $ show i ++ " is already declared") + local (addSub (i,Atom i)) $ check VU a + return (eval (Sub rho (i,Dir 0)) a,eval (Sub rho (i,Dir 1)) a) + checks :: (Tele,Env) -> [Ter] -> Typing () checks _ [] = return () checks ((x,a):xas,nu) (e:es) = do diff --git a/examples/nat.ctt b/examples/nat.ctt index dd64abc..4eccc35 100644 --- a/examples/nat.ctt +++ b/examples/nat.ctt @@ -32,16 +32,16 @@ reverse (A : U) : list A -> list A = split nil -> nil cons x xs -> append A (reverse A xs) (cons x nil) -Id (A : U) (a0 a1 : A) : U = IdP ( A) a0 a1 +Id (A : U) (a0 a1 : A) : U = IdP ( A) a0 a1 -refl (A : U) (a : A) : Id A a a = a +refl (A : U) (a : A) : Id A a a = a mapOnPath (A B : U) (f : A -> B) (a b : A) - (p : Id A a b) : Id B (f a) (f b) = f (p @ ?0) + (p : Id A a b) : Id B (f a) (f b) = f (p @ i) funExt (A : U) (B : A -> U) (f g : (x : A) -> B x) (p : (x : A) -> Id (B x) (f x) (g x)) : - Id ((y : A) -> B y) f g = \(a : A) -> (p a) @ ?0 + Id ((y : A) -> B y) f g = \(a : A) -> (p a) @ i idnat : nat -> nat = split zero -> zero @@ -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 @ ?0, p @ ?0 & ?1) + 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 = -- 2.34.1