Names are now strings

diff --git a/Connections.hs b/Connections.hs
index 6e6bb18f3053e11cec582f9e85c69ec583625061..a40b7ccac442a371462a16a82bbbe9101c9b8e58 100644 (file)
--- 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 6386d330dbf07028b1dfb134ec123fc5f72c2aeb..cb623997a8d1dc3a94e48a6b92823ffc4b9b7c28 100644 (file)
--- 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 8dc871933120769dd453dcb0328452343e7cfd7c..81e94edd30bfb07941fd4417918fd2e44148afce 100644 (file)
--- 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 13ca00b296e12b9e57b1e6a30ad880d114fa71ae..1a337987ad2d0899e6d7b8e5032ea56331c38f82 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -238,13 +238,10 @@ infer e = case e of
       VIdP a _ _ -> return $ a @@ phi\r
       _ -> throwError (show e ++ " is not a path")\r
   Trans p t -> case p of\r
-    Path i a -> do\r
-      rho <- asks env\r
-      when (i `elem` support rho)\r
-        (throwError $ show i ++ " is already declared")\r
-      local (addSub (i,Atom i)) $ check VU a\r
-      check (eval (Sub rho (i,Dir 0)) a) t\r
-      return $ (eval (Sub rho (i,Dir 1)) a)\r
+    Path{} -> do\r
+      (a0,a1) <- checkPath p\r
+      check a0 t\r
+      return a1\r
     _ -> do\r
       b <- infer p\r
       case b of\r
@@ -252,6 +249,15 @@ infer e = case e of
         _ -> throwError $ "transport expects a path but got " ++ show p\r
   _ -> throwError ("infer " ++ show e)\r
 \r
+-- Check that a term is a path and output the source and target\r
+checkPath :: Ter -> Typing (Val,Val)\r
+checkPath (Path i a) = do\r
+  rho <- asks env\r
+  when (i `elem` support rho)\r
+    (throwError $ show i ++ " is already declared")\r
+  local (addSub (i,Atom i)) $ check VU a\r
+  return (eval (Sub rho (i,Dir 0)) a,eval (Sub rho (i,Dir 1)) a)\r
+\r
 checks :: (Tele,Env) -> [Ter] -> Typing ()\r
 checks _              []     = return ()\r
 checks ((x,a):xas,nu) (e:es) = do\r

diff --git a/examples/nat.ctt b/examples/nat.ctt
index dd64abc4a1c2b337e2a30bd77a2c92eae3bfbad3..4eccc35b8b29cee086f2ea8cf30c57a64da85384 100644 (file)
--- 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 (<?0> A) a0 a1
+Id (A : U) (a0 a1 : A) : U = IdP (<i> A) a0 a1
 
-refl (A : U) (a : A) : Id A a a = <?0> a
+refl (A : U) (a : A) : Id A a a = <i> a
 
 mapOnPath (A B : U) (f : A -> B) (a b : A)
-          (p : Id A a b) : Id B (f a) (f b) = <?0> f (p @ ?0)
+          (p : Id A a b) : Id B (f a) (f b) = <i> 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 = <?0> \(a : A) -> (p a) @ ?0
+       Id ((y : A) -> B y) f g = <i> \(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) = <?0> (p @ ?0,<?1> p @ ?0 & ?1)
+  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 =