From de061b8713631452107b48c65a3c6f6bd2a84fef Mon Sep 17 00:00:00 2001
From: =?utf8?q?Anders=20M=C3=B6rtberg?= <andersmortberg@gmail.com>
Date: Tue, 5 Jul 2016 15:42:30 +0200
Subject: [PATCH] add local split

---
 Exp.cf               |  3 ++-
 Resolver.hs          |  8 ++++++++
 cubicaltt.el         |  2 +-
 examples/prelude.ctt | 20 +++++++-------------
 4 files changed, 18 insertions(+), 15 deletions(-)

diff --git a/Exp.cf b/Exp.cf
index d0fbe72..3c347e7 100644
--- 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 3dfd8ef..839af5f 100644
--- 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 2b9bab3..0facab0 100644
--- 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 75f2bce..23bdb3d 100644
--- 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)
 
-- 
2.34.1