Add syntax for datatypes

mced/Test/Datatypes2.mced

@@ -3,4 +3,5 @@ import Datatypes2/Helpers.
 
 import Datatypes2/Desc.
 import Datatypes2/Define.
-import Datatypes2/Tests.
+import Datatypes2/Parse.
+import Datatypes2/Test.

mced/Test/Datatypes2/Syntax.mced

@@ -0,0 +1,72 @@
+--------------------------------------------------------------------------------
+-- Parsing datatype declarations
+--------------------------------------------------------------------------------
+
+-- If the argument is a term applied to the empty list, return that term
+let reduceTerm : Term -> Term :=
+  foldTerm ?Term varTerm sortTerm binderTerm
+    (λ t : Term. λ l : List App. ifthenelse ?Term (isNil ?App l) t $ appLTerm t l)
+    charTerm unknownTerm unquoteTerm.
+
+-- The telescope of arguments and the rest
+let PreCDesc := Telescope × Term.
+
+elet noArgPreCDesc (t : Term) : PreCDesc := [Param|], t.
+elet consArgPreCDesc (p : Param) (d : PreCDesc) : PreCDesc := (p ∷ pr1 ?_ ?Term d), pr2 ?_ ?Term d.
+
+let ConstrDataTelescope := pr1 ?Telescope ?Term.
+let ConstrDataTerm := pr2 ?Telescope ?Term.
+
+let toPreCDesc (t : Term) : PreCDesc :=
+  recursionTerm ?PreCDesc
+    (λ v : Var.  noArgPreCDesc $ varTerm v)
+    (λ s : Sort. noArgPreCDesc $ sortTerm s)
+    (λ b : Binder. λ n : String. λ T, t : Term. λ recT, rect : PreCDesc.
+      matchBinder ?PreCDesc
+        (noArgPreCDesc $ binderTerm b n T t) (noArgPreCDesc $ binderTerm b n T t)
+        (consArgPreCDesc (mkParam false $ mkPreParam n T) rect)
+        (consArgPreCDesc (mkParam true  $ mkPreParam n T) rect)
+        b)
+    (λ t : Term. λ l : List App. λ _ : PreCDesc. λ _ : List (Bool × PreCDesc).
+      noArgPreCDesc $ appLTerm t l)
+    (λ c : Char. noArgPreCDesc $ charTerm c)
+    (noArgPreCDesc unknownTerm)
+    (λ u : Term. λ recu : PreCDesc. recu)
+    (reduceTerm t).
+
+elet toTDesc (tyName : Name) (t : Term) : TDesc :=
+  ifthenelse ?_ (termEq t (var tyName))
+    (tdRecNN)
+    (tdNonRec t).
+
+elet toADesc (tyName : Name) (p : Param) : ADesc :=
+  paramName p, toTDesc tyName (paramType p).
+
+elet toCDesc (tyName, cName : Name) (t : Term) : Maybe CDesc :=
+  ψ pc = toPreCDesc t : PreCDesc.
+  ifthenelse ?_ (termEq (pr2 ?_ ?Term pc) (var tyName))
+    (just ?_ (cName, map ?_ ?_ (toADesc tyName) (pr1 ?_ ?Term pc)))
+    (nothing ?CDesc).
+
+--------------------------------------------------------------------------------
+-- Syntax
+
+elet init$entry$_string_^space^=colon=^space^_multiTerm_
+  (name : String) (type : Term) := name, type.
+
+let init$entries$ := nil ?(Name × Term).
+let init$entries$=pipe=^space^_entry__entries_ := cons ?(Name × Term).
+
+let init$data2$_string_^space^_telescope_where^space^_entries_
+  (name : String) (t : Telescope) (cs : List (Name × Term)) : Maybe Desc :=
+  ψ cs' = traverseMaybeList ?(Name × Term) ?CDesc
+      (recursionProduct ?Name ?Term ?(Maybe CDesc) (toCDesc name))
+      cs : Maybe (List CDesc).
+  mapMaybe ?(List CDesc) ?Desc (mkTripleProduct ?String ?Telescope ?(List CDesc) name t) cs'.
+
+elet init$newStmt'$data2^space^_data2_=dot= : Maybe Desc -> Eval Unit :=
+  maybe ?_ ?_
+    (throwEval ?Unit "Error: not a valid datatype!")
+    (λ d : Desc. seqEval ?_ ?_ (DefineTy d) (DefineInd d)).
+
+updateEval.

mced/Test/Datatypes2/Test.mced

@@ -36,44 +36,35 @@ updateEval.
 --------------------------------------------------------------------------------
 -- Tests
 
-elet TNatDesc : Desc := "TNat", [Param|],
-  [CDesc| "tZero", [ADesc|]
-        ; "tSuc",  [ADesc|adUnnamed tdRecNN]].
-data2Test TNatDesc.
-
-elet TNatListDesc : Desc := "TNatList", [Param|],
-  [CDesc| "tNatNil", [ADesc|]
-        ; "tNatCons", [ADesc|adUnnamed (tdNonRec θ{Nat}); adUnnamed tdRecNN]].
-data2Test TNatListDesc.
-
-elet TProdDesc : Desc := "TProd", [Param|(false, "F1", θ{*}); (false, "F2", θ{*})],
-  [CDesc|"tPair", [ADesc|adUnnamed (tdNonRec θ{F1}); adUnnamed (tdNonRec θ{F2})]].
-data2Test TProdDesc.
-runMeta DefineProjLIs TProdDesc.
-
-elet TDSumDesc : Desc := "TDSum", [Param|(false, "F1", θ{*}); (false, "F2", θ{F1 -> *})],
-  [CDesc|"tDPair", [ADesc| "f1", tdNonRec θ{F1}; "f2", tdNonRec θ{F2 f1}]].
-data2Test TDSumDesc.
-runMeta DefineProjLIs TDSumDesc.
-
-elet TListDesc : Desc := "TList", [Param|(false, "F", θ{*})],
-  [CDesc| "tNil", [ADesc|]
-        ; "tCons" , [ADesc|adUnnamed $ tdNonRec θ{F}; adUnnamed tdRecNN]].
-data2Test TListDesc.
-
-elet T1Desc : Desc := "T1", [Param|],
-  [CDesc| "t11", [ADesc|]
-        ; "t12", [ADesc|adUnnamed tdRecNN; adUnnamed tdRecNN]].
-data2Test T1Desc.
+data2 TNat where
+| tZero : TNat
+| tSuc : TNat -> TNat.
+
+data2 TNatList where
+| tNatNil : TNatList
+| tNatCons : Nat -> TNatList -> TNatList.
+
+data2 TProd (A, B : *) where
+| tPair : A -> B -> TProd.
+
+data2 TDSum (A : *) (B : A -> *) where
+| tDPair : Π a : A. Π b : B a. TDSum.
+
+data2 TList (A : *) where
+| tNil : TList
+| tCons : A -> TList -> TList.
+
+data2 T1 where
+| t11 : T1
+| t12 : T1 -> T1 -> T1.
 
 -- golden test
 elet indT1Test : ∀ P : T1 -> *. P t11 -> (Π a0 : T1. P a0 -> Π a1 : T1. P a1 -> P (t12 a0 a1))
               -> Π x : T1. P x := indT1.
 
-elet T2Desc : Desc := "T2", [Param|],
-  [CDesc| "t21", [ADesc|adUnnamed (tdNonRec θ{Nat})]
-        ; "t22", [ADesc|adUnnamed tdRecNN; adUnnamed tdRecNN]].
-data2Test T2Desc.
+data2 T2 where
+| t21 : Nat -> T2
+| t22 : T2 -> T2 -> T2.
 
 elet T3Desc : Desc := "T3", [Param|],
   [CDesc| "t31", [ADesc|]