add local split

diff --git a/Exp.cf b/Exp.cf
index d0fbe722b9b676289011e04ebef56ab1fa80f593..3c347e77362deebf6d6874a27fe46011f7b549de 100644 (file)
--- a/Exp.cf
+++ b/Exp.cf
@@ -3,7 +3,7 @@ entrypoints Module, Exp ;
 comment "--" ;
 comment "{-" "-}" ;
 
-layout "where", "let", "split", "mutual" ;
+layout "where", "let", "split", "mutual", "with" ;
 layout stop "in" ;
 -- Do not use layout toplevel as it makes pExp fail!
 
@@ -26,6 +26,7 @@ NoWhere.  ExpWhere ::= Exp ;
 Let.          Exp  ::= "let" "{" [Decl] "}" "in" Exp ;
 Lam.          Exp  ::= "\\" [PTele] "->" Exp ;
 Path.         Exp  ::= "<" [AIdent] ">" Exp ;
+Split.        Exp  ::= "split@" Exp "with" "{" [Branch] "}" ;
 Fun.          Exp1 ::= Exp2 "->" Exp1 ;
 Pi.           Exp1 ::= [PTele] "->" Exp1 ;
 Sigma.        Exp1 ::= [PTele] "*" Exp1 ;

diff --git a/Resolver.hs b/Resolver.hs
index 3dfd8efe5409c10e8c67b063ec6b217db3b9a422..839af5f9544fedf3970af3c2dda8017a62cde465 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -191,6 +191,14 @@ resolveExp e = case e of
     e  <- resolveExp t0
     es <- mapM resolveExp ts
     return $ foldr1 CTT.Pair (e:es)
+  Split t brs -> do
+    t'   <- resolveExp t
+    brs' <- mapM resolveBranch brs
+    loc  <- getLoc (case brs of
+                      OBranch (AIdent (l,_)) _ _:_ -> l
+                      PBranch (AIdent (l,_)) _ _ _:_ -> l
+                      _ -> (0,0))
+    return $ CTT.Split "" loc t' brs' -- Do we ever use the name?
   Let decls e   -> do
     (rdecls,names) <- resolveDecls decls
     mkWheres rdecls <$> local (insertIdents names) (resolveExp e)

diff --git a/cubicaltt.el b/cubicaltt.el
index 2b9bab3280f263e0aeef6e19b7b42effc2bf0c16..0facab0725c7eaa984a75039bc7f9b21bbbb8901 100644 (file)
--- a/cubicaltt.el
+++ b/cubicaltt.el
@@ -1,6 +1,6 @@
 ;; define several class of keywords
 (setq ctt-keywords '("hdata" "data" "import" "mutual" "let" "in" "split"
-                     "module" "where" "U") )
+                     "with" "module" "where" "U") )
 (setq ctt-special '("undefined" "primitive"))
 
 ;; create regex strings

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index 75f2bce27afa95d7a200829d904128e255d1e7fd..23bdb3d7af596ef2d5343c5a4363cd2136026a5a 100644 (file)
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -216,31 +216,25 @@ propIsContr (A : U) : prop (isContr A) = lemProp (isContr A) rem
 
 data N0 =
 
-efq (A : U) : N0 -> A = split{}
+efq (A : U) : N0 -> A = split {}
 neg (A : U) : U = A -> N0
 
 data Unit = tt
 
-propUnit : prop Unit = rem
- where rem1 : (x:Unit) -> Id Unit x tt = split tt -> refl Unit tt
-       rem (x:Unit) : (y:Unit) -> Id Unit x y = split tt -> rem1 x
+propUnit : prop Unit = split
+ tt -> split@((x:Unit) -> Id Unit tt x) with
+  tt -> <i> tt
 
 setUnit : set Unit = propSet Unit propUnit
 
 data or (A B : U) = inl (a : A)
                   | inr (b : B)
 
-propOr (A B : U) (hA : prop A) (hB : prop B) (h : A -> neg B) : prop (or A B) = rem
-  where
-  rem : (a b : or A B) -> Id (or A B) a b = split
-    inl a' -> rem1
-      where
-      rem1 : (b : or A B) -> Id (or A B) (inl a') b = split
+propOr (A B : U) (hA : prop A) (hB : prop B) (h : A -> neg B) : prop (or A B) = split
+    inl a' -> split@((b : or A B) -> Id (or A B) (inl a') b) with
         inl b' -> <i> inl (hA a' b' @ i)
         inr b' -> efq (Id (or A B) (inl a') (inr b')) (h a' b')
-    inr a' -> rem1
-      where
-      rem1 : (b : or A B) -> Id (or A B) (inr a') b = split
+    inr a' -> split@((b : or A B) -> Id (or A B) (inr a') b) with
         inl b' -> efq (Id (or A B) (inr a') (inl b')) (h b' a')
         inr b' -> <i> inr (hB a' b' @ i)