Reintroduce hdata

diff --git a/Exp.cf b/Exp.cf
index 6b71f3011e8f9a2488d5aa8d58722a6ab3b3e86f..f067ebf8ae943a7a395a685a077b4de53dc83baa 100644 (file)
--- a/Exp.cf
+++ b/Exp.cf
@@ -14,6 +14,7 @@ separator Imp ";" ;
 
 DeclDef.    Decl ::= AIdent [Tele] ":" Exp "=" ExpWhere ;
 DeclData.   Decl ::= "data" AIdent [Tele] "=" [Label] ;
+DeclHData.  Decl ::= "hdata" AIdent [Tele] "=" [Label] ;
 DeclSplit.  Decl ::= AIdent [Tele] ":" Exp "=" "split" "{" [Branch] "}" ;
 DeclUndef.  Decl ::= AIdent [Tele] ":" Exp "=" "undefined" ;
 DeclMutual. Decl ::= "mutual" "{" [Decl] "}" ;

diff --git a/Resolver.hs b/Resolver.hs
index 4969235231713426434b0b583266f09bd2619e07..bba1f466e5bf3f26a6aa0ef03f81d35e061367cf 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -282,16 +282,9 @@ resolveNonMutualDecl d = case d of
         a     = binds CTT.Pi tele' (resolveExp t)
         d     = lams tele' (local (insertVar f) $ resolveWhere body)
     in (f,a,d,[(f,Variable)])
-  DeclData (AIdent (l,f)) tele sums ->
-    let tele' = flattenTele tele
-        a     = binds CTT.Pi tele' (return CTT.U)
-        cs    = [ (unAIdent lbl,Constructor) | OLabel lbl _ <- sums ]
-        pcs   = [ (unAIdent lbl,PConstructor) | PLabel lbl _ _ _ <- sums ]
-        sum   = if null pcs then CTT.Sum else CTT.HSum
-        d = lams tele' $ local (insertVar f) $
-            sum <$> getLoc l <*> pure f
-               <*> mapM (resolveLabel (cs ++ pcs)) sums
-    in (f,a,d,(f,Variable):cs ++ pcs)
+  DeclData x tele sums  -> resolveDeclData x tele sums null
+  DeclHData x tele sums ->
+    resolveDeclData x tele sums (const False) -- always pick HSum
   DeclSplit (AIdent (l,f)) tele t brs ->
     let tele' = flattenTele tele
         vars  = map fst tele'
@@ -308,6 +301,21 @@ resolveNonMutualDecl d = case d of
         d     = CTT.Undef <$> getLoc l <*> a
     in (f,a,d,[(f,Variable)])
 
+-- Helper function to resolve data declarations. The predicate p is
+-- used to decide if we should use Sum or HSum.
+resolveDeclData :: AIdent -> [Tele] -> [Label] -> ([(Ident,SymKind)] -> Bool) ->
+                   (Ident, Resolver Ter, Resolver Ter, [(Ident, SymKind)])
+resolveDeclData (AIdent (l,f)) tele sums p =
+  let tele' = flattenTele tele
+      a     = binds CTT.Pi tele' (return CTT.U)
+      cs    = [ (unAIdent lbl,Constructor) | OLabel lbl _ <- sums ]
+      pcs   = [ (unAIdent lbl,PConstructor) | PLabel lbl _ _ _ <- sums ]
+      sum   = if p pcs then CTT.Sum else CTT.HSum
+      d = lams tele' $ local (insertVar f) $
+            sum <$> getLoc l <*> pure f
+                <*> mapM (resolveLabel (cs ++ pcs)) sums
+  in (f,a,d,(f,Variable):cs ++ pcs)
+
 resolveRTele :: [Ident] -> [Resolver CTT.Ter] -> Resolver CTT.Tele
 resolveRTele [] _ = return []
 resolveRTele (i:is) (t:ts) = do

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

diff --git a/examples/hnat.ctt b/examples/hnat.ctt
new file mode 100644 (file)
index 0000000..d4c8a8f
--- /dev/null
+++ b/examples/hnat.ctt
@@ -0,0 +1,47 @@
+module hnat where
+
+import nat
+
+-- Non-standard nat:
+hdata hnat = nzero
+           | nsuc (n : hnat)
+
+-- This reduces to "hComp (hnat) nzero []"
+test0 : hnat = comp (<_> hnat) nzero []
+
+-- This reduces to "zero"
+test1 : nat = comp (<_> nat) zero []
+
+test2 : Id hnat nzero (comp (<_> hnat) nzero []) =
+  fill (<_> hnat) nzero []
+
+toNat : hnat -> nat = split
+  nzero -> zero
+  nsuc n -> suc (toNat n)
+
+fromNat : nat -> hnat = split
+  zero -> nzero
+  suc n -> nsuc (fromNat n)
+
+toNatK : (n : hnat) -> Id hnat (fromNat (toNat n)) n = split
+  nzero -> <_> nzero
+  nsuc n -> <i> nsuc (toNatK n @ i)
+
+fromNatK : (n : nat) -> Id nat (toNat (fromNat n)) n = split
+  zero -> <_> zero
+  suc n -> <i> suc (fromNatK n @ i)
+
+hnatEqNat : Id U hnat nat =
+  isoId hnat nat toNat fromNat fromNatK toNatK
+
+-- This is zero
+test3 : nat = trans hnat nat hnatEqNat test0
+
+-- This is "hComp (hnat) nzero []"
+test4 : hnat = trans nat hnat (<i> hnatEqNat @ -i) zero
+
+-- This is "hComp (hnat) (hComp (hnat) nzero []) []"
+test5 : hnat = trans hnat hnat (compId U hnat nat hnat hnatEqNat (<i> hnatEqNat @ -i)) nzero
+
+hnatSet : set hnat = subst U set nat hnat (<i> hnatEqNat @ -i) natSet
+

diff --git a/examples/nat.ctt b/examples/nat.ctt
index 5dd18d147548e525d488ae0cc8e036fe046c40ba..b76fef7d9c4b1a60d7da2b8a338d572d87a18534 100644 (file)
--- a/examples/nat.ctt
+++ b/examples/nat.ctt
@@ -73,3 +73,5 @@ natDec : (n m:nat) -> dec (Id nat n m) = split
                  (sucInj n m) (natDec n m))
 
 natSet : set nat = hedberg nat natDec
+
+