Use the new datatype framework in the COC example

mced/Bootstrap/Compiled/List.mced

@@ -8,7 +8,7 @@ let isNil := Λ X : * λ l : [List X] [[<l Bool> true] λ _ : X λ _ : Bool fals
 let listEq := Λ X : * λ eqX : Π _ : X Π _ : X Bool [[<<recursionList' X> Π l : [List X] Bool> <isNil X>] λ x : X λ rec : Π _ : [List X] Bool [[<<recursionList X> Bool> false] λ y : X λ ys : [List X] λ _ : Bool [[and [[eqX x] y]] [rec ys]]]] : ∀ X : * Π eqX : Π _ : X Π _ : X Bool Π _ : [List X] Π _ : [List X] Bool.
 let pureList := Λ X : * λ x : X [[<cons X> x] <nil X>] : ∀ X : * Π x : X [List X].
 let app := Λ X : * λ l1 : [List X] λ l2 : [List X] [[<l1 [List X]> l2] λ x : X λ rec : [List X] [[<cons X> x] rec]] : ∀ X : * Π l1 : [List X] Π l2 : [List X] [List X].
-let snoc := Λ X : * λ x : X λ xs : [List X] [[<app X> xs] [<pureList X> x]] : ∀ X : * Π x : X Π xs : [List X] [List X].
+let snoc := Λ X : * λ xs : [List X] λ x : X [[<app X> xs] [<pureList X> x]] : ∀ X : * Π xs : [List X] Π x : X [List X].
 let filter := Λ X : * λ f : Π _ : X Bool λ l : [List X] [[<l [List X]> <nil X>] λ x : X λ rec : [List X] [[[<ifthenelse [List X]> [f x]] [[<cons X> x] rec]] rec]] : ∀ X : * Π f : Π _ : X Bool Π l : [List X] [List X].
 let foldl := Λ A : * Λ B : * λ f : Π _ : B Π _ : A B λ l : [List A] [[<l Π _ : B B> λ b : B b] λ a : A λ rec : Π _ : B B λ b : B [[f [rec b]] a]] : ∀ A : * ∀ B : * Π f : Π _ : B Π _ : A B Π l : [List A] Π _ : B B.
 let foldr := Λ A : * Λ B : * λ f : Π _ : A Π _ : B B λ l : [List A] λ b : B [[<l B> b] λ a : A λ rec : B [[f a] rec]] : ∀ A : * ∀ B : * Π f : Π _ : A Π _ : B B Π l : [List A] Π b : B B.

mced/Bootstrap/Stage-1/Bool.mced

@@ -23,4 +23,7 @@ let and := λ b : Bool λ b' : Bool [[[<ifthenelse Bool> b] b'] false].
 let or := λ b : Bool λ b' : Bool [[[<ifthenelse Bool> b] b] b'].
 let not := λ b : Bool [[[<ifthenelse Bool> b] false] true].
 
-let boolEq := λ b : Bool λ b' : Bool [[[<ifthenelse Bool> b] b'] [not b']].
+let boolEq := λ b : Bool λ b' : Bool [[[<ifthenelse Bool> b] b'] [not b']].
+
+let contr := Λ X : * λ eq : [[<<UEq Bool> Bool> true] false] δ X eq
+  : ∀ X : * Π eq : [[<<UEq Bool> Bool> true] false] X.

mced/Test.mced

@@ -3,29 +3,23 @@ import Base.
 set PWD "Test/".
 import BootstrapTest.
 
-import Datatypes2/Mono.
-import Datatypes2/Helpers.
-import Datatypes2/Desc.
-
-import Datatypes2/IHelpers.
+import ErrorMonad.
 
-import Datatypes2/Define.
-import Datatypes2/Syntax.
-import Datatypes2/Test.
+import Datatypes2.
 
 import BootstrapCompiler.
+
+let Type := Term.
+
+import Bootstrap/TermC.
+
 import Bootstrap.
 
 import SchemeCompiler.
 
-import ErrorMonad.
-
 import LambdaCalc.
 import LambdaCalcExample.
 
-import Datatypes.
-import DatatypesTest.
-
 import COC.
 
 set PWD "".

mced/Test/Bootstrap/TermC.mced

@@ -1,12 +1,12 @@
 module Bootstrap:TermC.
 
-Given Desc CDesc ADesc Param nil cons prodPair adNonRec adRecNN adRecN stringNil stringCons.
+Given Desc CDesc ADesc TDesc adUnnamed tdNonRec tdRecNN tdRecN Param nil cons prodPair stringNil stringCons.
 Given appLTerm quoteAst sVarTerm App false.
-Given Cast intrCast elimCast monoConst beta beta' Mono MonoD monoId.
+Given Cast intrCast castTrans elimCast monoConst beta beta' Mono MonoD monoId.
 Given Iota iotaMono iPair iPr1 iPr2 castIota.
 Given Rec roll unroll UEq recLB usubst.
-Given Var Sort Char String List Bool.
-Given View elimView selfView extCast indList nilC consC.
+Given Var Sort Char String List map zip Bool Product.
+Given View elimView selfView extCast indList nilC consC Type.
 
 let monoList : Mono List := Λ X, Y : *. λ c : Cast X Y.
   extCast ?(List X) ?(List Y) ?(indList ?X ?(λ l : List X. View (List Y) (beta' ?(List X) l))
@@ -31,26 +31,23 @@ elet indHelperList [AP, A : *] [c : Cast AP A] [P : A -> *] (Pc : Π t : AP. P (
        ?(beta ?(List A) (indHelperList/conv ?AP ?A ?c $ cons ?AP t ts)) ?P' $
        pc (elimCast ?AP ?A ?c t) (Pc t) (indHelperList/conv ?AP ?A ?c ts) p').
 
-elet BinderDesc : Desc := "Binder", [Param|],
-  [CDesc|"lambdaBinder", [ADesc|]
-        ;"LambdaBinder", [ADesc|]
-        ;"piBinder",     [ADesc|]
-        ;"forallBinder", [ADesc|]].
-data2Test BinderDesc.
+data2 Binder : *.
+| lambdaBinder : Binder
+| LambdaBinder : Binder
+| piBinder     : Binder
+| forallBinder : Binder.
 
-elet TermDesc : Desc := "Term", [Param|],
-  [CDesc|"varTerm",     [ADesc|adNonRec θ{Var}]
-        ;"sortTerm",    [ADesc|adNonRec θ{Sort}]
-        ;"binderTerm",  [ADesc|adNonRec θ{Binder}; adNonRec θ{String}; adRecNN; adRecNN]
-        ;"appLTerm'",   [ADesc|adRecNN; adRecN (θ{List}, θ{monoList})]
-        ;"charTerm",    [ADesc|adNonRec θ{Char}]
-        ;"unknownTerm", [ADesc|]
-        ;"unquoteTerm", [ADesc|adRecNN]
-        ;"argTerm",     [ADesc|adNonRec θ{Bool}; adRecNN]].
+elet TermDesc : Desc := "Term", [Param|], [Type|],
+  [CDesc|"varTerm",     map ?_ ?_ adUnnamed [TDesc|tdNonRec θ{Var}], [Type|]
+        ;"sortTerm",    map ?_ ?_ adUnnamed [TDesc|tdNonRec θ{Sort}], [Type|]
+        ;"binderTerm",  map ?_ ?_ adUnnamed [TDesc|tdNonRec θ{Binder}; tdNonRec θ{String}; tdRecNN [Type|]; tdRecNN [Type|]], [Type|]
+        ;"appLTerm'",   map ?_ ?_ adUnnamed [TDesc|tdRecNN [Type|]; tdRecN (θ{List}, θ{monoList})], [Type|]
+        ;"charTerm",    map ?_ ?_ adUnnamed [TDesc|tdNonRec θ{Char}], [Type|]
+        ;"unknownTerm", map ?_ ?_ adUnnamed [TDesc|], [Type|]
+        ;"unquoteTerm", map ?_ ?_ adUnnamed [TDesc|tdRecNN [Type|]], [Type|]
+        ;"argTerm",     map ?_ ?_ adUnnamed [TDesc|tdNonRec θ{Bool}; tdRecNN [Type|]], [Type|]].
 data2Test TermDesc.
 
-Given Product map zip.
-
 let getErased (t : Term) : Bool :=
   (iPr1 ?(TermF Term) ?(WkIndTermF Term) (unrollTerm t)) ?Bool
     (λ _ : Var. false)

mced/Test/Bootstrap/TermC2.mced

@@ -0,0 +1,227 @@
+module Bootstrap:TermC2.
+
+Given Desc CDesc ADesc Param nil cons prodPair stringNil stringCons.
+Given quoteAst sVarTerm.
+Given Cast intrCast elimCast monoConst castTrans beta beta' Mono MonoD monoId.
+Given Iota iotaMono iPair iPr1 iPr2 castIota.
+Given Rec roll unroll UEq recLB usubst.
+Given Var Sort Char String List Bool true false.
+Given View elimView selfView extCast indList nilC consC.
+
+Given Product recursionProduct foldl.
+
+data2 Binder : *.
+| lambdaBinder : Binder
+| LambdaBinder : Binder
+| piBinder : Binder
+| forallBinder : Binder.
+
+data2 PreTerm : Bool -> *.
+| pVarTerm : Var -> PreTerm true
+| pSortTerm : Sort -> PreTerm true
+| pBinderTerm : Binder -> String -> PreTerm true -> PreTerm true -> PreTerm true
+| pAppLTerm : PreTerm true -> PreTerm false -> PreTerm true
+| pCharTerm : Char -> PreTerm true
+| pUnknownTerm : PreTerm true
+| pUnquoteTerm : PreTerm true -> PreTerm true
+| pNilTerm : PreTerm false
+| pConsTerm : Bool -> PreTerm true -> PreTerm false -> PreTerm false.
+
+let Term : * := PreTerm true.
+let App := Bool × Term.
+
+let varTerm : Var -> Term := pVarTerm.
+let sortTerm : Sort -> Term := pSortTerm.
+let binderTerm : Binder -> String -> Term -> Term -> Term := pBinderTerm.
+let charTerm : Char -> Term := pCharTerm.
+let unknownTerm : Term := pUnknownTerm.
+let unquoteTerm : Term -> Term := pUnquoteTerm.
+
+elet appLTerm (t : Term) (as : List App) : Term :=
+  pAppLTerm t (foldl ?_ ?_ (λ x : PreTerm false.
+    recursionProduct ?_ ?_ ?_ λ b : Bool. λ y : Term. pConsTerm b y x) as pNilTerm).
+
+-- elet indPreTerm1 [P' : Π b : Bool. PreTerm b → *]
+--   (hpVarTerm : Π v : Var. P' true (pVarTerm v))
+--   (hpSortTerm : Π s : Sort. P' true (pSortTerm s))
+--   (hpBinderTerm : Π b : Binder. Π s : String. Π t : [PreTerm true]. ([[P' true] ctor2]) → [[P' true] [[[pBinderTerm ctor0] ctor1] ctor2]])
+--   Π hpAppLTerm : Π ctor0 : [PreTerm true]. ([[P' true] ctor0]) → Π ctor1 : [PreTerm false]. ([[P' false] ctor1]) → [[P' true] [[pAppLTerm ctor0] ctor1]]. Π hpCharTerm : Π ctor0 : Char. [[P' true] [pCharTerm ctor0]]. Π hpUnknownTerm : [[P' true] pUnknownTerm]. Π hpUnquoteTerm : Π ctor0 : [PreTerm true]. ([[P' true] ctor0]) → [[P' true] [pUnquoteTerm ctor0]]. Π hpNilTerm : [[P' false] pNilTerm]. Π hpConsTerm : Π ctor0 : Bool. Π ctor1 : [PreTerm true]. ([[P' true] ctor1]) → Π ctor2 : [PreTerm false]. ([[P' false] ctor2]) → [[P' false] [[[pConsTerm ctor0] ctor1] ctor2]]. Π k0 : Bool. Π x' : [PreTerm k0]. [[P' k0] x'] := indPreTerm.
+
+let matchPreTerm [X : Bool -> *]
+  (fvar  : Var -> X true)
+  (fsort : Sort -> X true)
+  (fbind : Binder -> String -> Term -> Term -> X true)
+  (fapp  : Term -> PreTerm false -> X true)
+  (fchar : Char -> X true)
+  (funk  : X true)
+  (funq  : Term -> X true)
+  (fnil  : X false)
+  (fcons : Bool -> Term -> PreTerm false -> X false)
+  (b : Bool)
+  (t : PreTerm b) : X b :=
+  (iPr1 ?(PreTermF PreTerm b) ?(WkIndPreTermF PreTerm b) (unrollPreTerm b t)) ?X
+    fvar fsort fbind fapp fchar funk funq fnil fcons.
+
+-- let recursionPreTerm [X : Bool -> *]
+--   (fvar  : Var -> X true)
+--   (fsort : Sort -> X true)
+--   (fbind : Binder -> String -> Term -> Term -> X true -> X true -> X true)
+--   (fapp  : Term -> PreTerm false -> X true -> X false -> X true)
+--   (fchar : Char -> X true)
+--   (funk  : X true)
+--   (funq  : Term -> X true -> X true)
+--   (fnil  : X false)
+--   (fcons : Bool -> Term -> PreTerm false -> X true -> X false -> X false)
+--   : Π b : Bool. PreTerm b -> X b :=
+--   indPreTerm ?(λ b : Bool. λ _ : PreTerm b. X b) fvar fsort
+--     (λ b : Binder. λ s : String. λ t : Term. λ rect : X true. λ T : Term. λ recT : X true. fbind b s t T rect recT)
+--     (λ x : Term. λ recx : X true. λ a : PreTerm false. λ reca : X false. fapp x a recx reca)
+--     fchar funk funq fnil
+--     (λ b : Bool. λ t : Term. λ rect : X true. λ ts : PreTerm false. λ rects : X false.
+--       fcons b t ts rect rects).
+
+Given Top intrTop.
+
+Given contr.
+
+data2 Bot : *. .
+
+let botElim [X : *] (b : Bot) : X :=
+  indBot ?(λ _ : Bot. X) b.
+
+data2 Eq (X : *) (x : X) : X -> *.
+| refl : Eq x.
+
+-- indTEq (X : *) (x : X) [P : Π y : X. TEq X x y -> *]
+--   : P x (tRefl X x) -> Π y : X. Π eq : TEq X x y. P y eq
+
+let eqToUEq [X : *] (x, y : X) (eq : Eq X x y) : UEq ?X ?X x y :=
+  indEq X x ?(λ z : X. λ _ : Eq X x z. UEq ?X ?X x z) (beta ?X x) y eq.
+
+elet sym [A : *] (a, a' : A) (eq : Eq A a a') : Eq A a' a :=
+  indEq _ _ ?(λ y : A. λ _ : Eq _ a y. Eq _ y a)
+    (refl _ a) a' eq.
+
+elet trans [A : *] (a, a', a'' : A) (eq1 : Eq A a a') (eq2 : Eq A a' a'') : Eq A a a'' :=
+  indEq _ _ ?(λ y : A. λ _ : Eq _ a' y. Eq _ y a'')
+    eq2 a (sym ?_ _ _ eq1).
+
+elet cong [A, B : *] (f : A -> B) (a, a' : A) (eq : Eq A a a') : Eq B (f a) (f a') :=
+  indEq _ _ ?(λ y : A. λ _ : Eq _ a y. Eq _ (f a) (f y))
+    (refl _ (f a)) a' eq.
+
+elet trueNeqFalse (eq : Eq Bool true false) : Bot :=
+  contr ?Bot (eqToUEq ?_ _ _ eq).
+
+elet contrFun [A : *] (f : A -> Bool) (a, b : A)
+  (eq : Eq A a b) (eqa : Eq Bool (f a) true) (eqb : Eq Bool (f b) false) : Bot :=
+  trueNeqFalse
+    $ trans ?_ _ _ _ (sym ?_ _ _ eqa)
+    $ trans ?_ _ _ _ (cong ?_ ?_ f _ _ eq)
+                     eqb.
+
+
+let recursionPreTermF [X : *]
+  (fnil  : X)
+  (fcons : Bool -> Term -> PreTerm false -> X -> X)
+  (pt : PreTerm false)
+  : X :=
+  ψ default = λ eq : Eq Bool true false. botElim ?X (trueNeqFalse eq) : Eq Bool true false -> X.
+  indPreTerm ?(λ b : Bool. λ _ : PreTerm b. Eq Bool b false -> X)
+    (λ _ : Var. default)
+    (λ _ : Sort. default)
+    (λ _ : Binder. λ _ : String. λ _ : Term. λ _ : Eq Bool true false -> X. λ _ : Term. λ _ : Eq Bool true false -> X. default)
+    (λ _ : Term. λ _ : Eq Bool true false -> X. λ _ : PreTerm false. λ _ : Eq Bool false false -> X. default)
+    (λ _ : Char. default)
+    default
+    (λ _ : Term. λ _ : Eq Bool true false -> X. default)
+    (λ _ : Eq Bool false false. fnil)
+    (λ b : Bool. λ t : Term. λ _ : Eq Bool true false -> X. λ ts : PreTerm false. λ rects : Eq Bool false false -> X. λ _ : Eq Bool false false. fcons b t ts (rects (refl Bool false)))
+    false pt (refl Bool false).
+
+elet toListApp : PreTerm false -> List App :=
+  recursionPreTermF ?(List App) [App|]
+    (λ b : Bool. λ t : Term. λ _ : PreTerm false. λ rects : List App. (b, t) ∷ rects).
+
+elet fromListApp (as : List App) : PreTerm false :=
+  foldl ?_ ?_
+    (λ x : PreTerm false. recursionProduct ?_ ?_ ?_ λ b : Bool. λ y : Term. pConsTerm b y x)
+    as pNilTerm.
+
+let matchTerm [X : *]
+  (fvar  : Var -> X)
+  (fsort : Sort -> X)
+  (fbind : Binder -> String -> Term -> Term -> X)
+  (fapp  : Term -> List (Bool × Term) -> X)
+  (fchar : Char -> X)
+  (funk  : X)
+  (funq  : Term -> X)
+  (t : Term) : X :=
+  (iPr1 ?(PreTermF PreTerm true) ?(WkIndPreTermF PreTerm true) (unrollPreTerm true t)) ?(λ _ : Bool. X)
+    fvar fsort fbind
+    (λ t' : Term. λ ts : List Term.
+      ψ erased = map ?Term ?Bool getErased ts : List Bool.
+      fapp t' (zip ?Bool ?Term erased (map ?Term ?Term unApp ts)))
+    fchar funk funq
+    (λ _ : Bool. λ _ : Term. funk).
+
+let recursionTerm [X : *]
+  (fvar  : Var -> X)
+  (fsort : Sort -> X)
+  (fbind : Binder -> String -> Term -> Term -> X -> X -> X)
+  (fapp  : Term -> List (Bool × Term) -> X -> List (Bool × X) -> X)
+  (fchar : Char -> X)
+  (funk  : X)
+  (funq  : Term -> X -> X)
+  : Term -> X :=
+  indTerm ?(λ _ : Term. X) ?(λ _ : List Term. List X) fvar fsort
+    (λ b : Binder. λ s : String. λ t : Term. λ rect : X. λ T : Term. λ recT : X. fbind b s t T rect recT)
+    (λ t : Term. λ rect : X. λ a : List Term. λ reca : List X.
+      ψ erased = map ?Term ?Bool getErased a : List Bool.
+      fapp t    (zip ?Bool ?Term erased (map ?Term ?Term unApp a))
+           rect (zip ?Bool ?X    erased reca))
+    [X|]
+    (λ _ : Term. λ x : X. λ _ : List Term. cons ?X x)
+    fchar funk funq
+    (λ b : Bool. λ t : Term. λ rect : X. rect).
+
+-- let getErased (t : Term) : Bool :=
+--   (iPr1 ?(TermF Term) ?(WkIndTermF Term) (unrollTerm t)) ?Bool
+--     (λ _ : Var. false)
+--     (λ _ : Sort. false)
+--     (λ _ : Binder. λ _ : String. λ _, _ : Term. false)
+--     (λ _ : Term. λ _ : List Term. false)
+--     (λ _ : Char. false)
+--     false
+--     (λ _ : Term. false)
+--     (λ b : Bool. λ _ : Term. b).
+
+-- let unApp (t : Term) : Term :=
+--   (iPr1 ?(TermF Term) ?(WkIndTermF Term) (unrollTerm t)) ?Term
+--     (λ _ : Var. unknownTerm)
+--     (λ _ : Sort. unknownTerm)
+--     (λ _ : Binder. λ _ : String. λ _, _ : Term. unknownTerm)
+--     (λ _ : Term. λ _ : List Term. unknownTerm)
+--     (λ _ : Char. unknownTerm)
+--     unknownTerm
+--     (λ _ : Term. unknownTerm)
+--     (λ _ : Bool. λ t' : Term. t').
+
+let foldTerm [X : *]
+  (fvar  : Var -> X)
+  (fsort : Sort -> X)
+  (fbind : Binder -> String -> X -> X -> X)
+  (fapp  : X -> List (Bool × X) -> X)
+  (fchar : Char -> X)
+  (funk  : X)
+  (funq  : X -> X)
+  : Term -> X :=
+  recursionTerm ?X fvar fsort
+    (λ b : Binder. λ s : String. λ _, _ : Term. λ t, T : X. fbind b s t T)
+    (λ _ : Term. λ _ : List (Bool × Term). λ t : X. λ a : List (Bool × X). fapp t a)
+    fchar funk
+    (λ _ : Term. funq).
+
+endModule.
+
+runMeta compileBootstrapModules [String|"TermC2"].

mced/Test/COC.mced

@@ -1,3 +1,7 @@
+let CNat := Nat.
+let Czero := zero.
+let Csucc := suc.
+
 import COC/Map.
 import COC/Theory.
 import COC/TermAliases.