Skip to content

Commit

Permalink
Support indexed types in the datatype syntax
Browse files Browse the repository at this point in the history
  • Loading branch information
@WhatisRT
WhatisRT committed Jun 5, 2024
1 parent 0ddd759 commit 3cbf443
Show file tree
Hide file tree
Showing 2 changed files with 104 additions and 65 deletions.
133 changes: 88 additions & 45 deletions mced/Test/Datatypes2/Syntax.mced
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,51 +2,94 @@
-- Parsing datatype declarations
--------------------------------------------------------------------------------

let Error (A : *) : * := Sum String A.
let pureError [A : *] (a : A) : Error A := inr ?String ?A a.
let throwError [A : *] (e : String) : Error A := inl ?String ?A e.
let bindError [A, B : *] (x : Error A) (f : A -> Error B) : Error B :=
recursionSum ?String ?A ?(Error B) (throwError ?B) f x.
let runError [A, B : *] (x : Error A) (handler : String -> B) (f : A -> B) : B :=
recursionSum ?String ?A ?B handler f x.

elet traverseErrorList [X, Y : *] (f : X -> Error Y) (l : List X) : Error (List Y) :=
recursionList ?X ?(Error (List Y))
(pureError ?(List Y) [Y|])
(λ x : X. λ xs : List X. λ rec : Error (List Y).
bindError ?Y ?(List Y) (f x) λ y : Y.
bindError ?(List Y) ?(List Y) rec λ ys : List Y.
pureError ?(List Y) (y ∷ ys))
l.

-- 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.

let showTermBasic : Term -> String :=
foldTerm ?String (λ _ : Var. "var") (λ _ : Sort. "sort")
(λ _ : Binder. λ _ : String. λ _, _ : String. "binder")
(λ _ : String. λ l : List (Bool × String). "app")
(λ _ : Char. "char") "unknown" (λ _ : String. "unquote").

-- The telescope of arguments and the rest
let PreCDesc := Telescope × Term.
let TyView := Telescope × Term.

elet noArgPreCDesc (t : Term) : PreCDesc := [Param|], t.
elet consArgPreCDesc (p : Param) (d : PreCDesc) : PreCDesc := (p ∷ pr1 ?_ ?Term d), pr2 ?_ ?Term d.
elet noArgTyView (t : Term) : TyView := [Param|], t.
elet consArgTyView (p : Param) (d : TyView) : TyView := (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)
let toTyView (t : Term) : TyView :=
recursionTerm ?TyView
(λ v : Var. noArgTyView $ varTerm v)
(λ s : Sort. noArgTyView $ sortTerm s)
(λ b : Binder. λ n : String. λ T, t : Term. λ recT, rect : TyView.
matchBinder ?TyView
(noArgTyView $ binderTerm b n T t) (noArgTyView $ binderTerm b n T t)
(consArgTyView (mkParam false $ mkPreParam n T) rect)
(consArgTyView (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)
(λ t : Term. λ l : List App. λ _ : TyView. λ _ : List (Bool × TyView).
noArgTyView $ appLTerm t l)
(λ c : Char. noArgTyView $ charTerm c)
(noArgTyView unknownTerm)
(λ u : Term. λ recu : TyView. recu)
(reduceTerm t).

-- `just`, if `t` is of the form `tyName t1 ... tn`
elet isAppTy (tyName : Name) : Term -> Maybe (List App) :=
matchTerm ?(Maybe (List App))
(λ v : Var. ifthenelse ?_ (termEq (varTerm v) (var tyName)) (just ?_ [App|]) (nothing ?(List App)))
(λ _ : Sort. nothing ?(List App))
(λ _ : Binder. λ _ : String. λ _,_ : Term. nothing ?(List App))
(λ t : Term. λ a : List App.
ifthenelse ?_ (termEq t (var tyName)) (just ?_ a) (nothing ?(List App)))
(λ _ : Char. nothing ?(List App))
(nothing ?(List App))
(λ _ : Term. nothing ?(List App)).

elet toTDesc (tyName : Name) (t : Term) : TDesc :=
ifthenelse ?_ (termEq t (var tyName))
(tdRecNN [Term|])
(tdNonRec t).
maybe ?_ ?_
(tdNonRec t)
(λ a : List App. tdRecNN (map ?_ ?_ appTerm a))
(isAppTy tyName 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), [Term|]))
(nothing ?CDesc).
elet parseIxs (t : Term) : Error Telescope :=
ψ pc = toTyView t : TyView.
ifthenelse ?_ (termEq (pr2 ?_ ?Term pc) (reduceTerm θ{*}))
(pureError ?_ (pr1 ?_ ?Term pc))
(throwError ?Telescope φ"parseIxs failed: ${showTerm (pr2 ?_ ?Term pc)}").

elet toCDesc (tyName, cName : Name) (t : Term) : Error CDesc :=
ψ pc = toTyView t : TyView.
maybe ?_ ?_ (throwError ?CDesc φ"toCDesc failed: ${showTerm (pr2 ?_ ?Term pc)}")
(λ a : List App. pureError ?_ (cName, map ?_ ?_ (toADesc tyName) (pr1 ?_ ?Term pc),
map ?_ ?_ appTerm a))
(isAppTy tyName (pr2 ?_ ?Term pc)).

--------------------------------------------------------------------------------
-- Syntax
Expand All @@ -57,30 +100,30 @@ elet init$entry$_string_^space^=colon=^space^_multiTerm_
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)) : Bool -> Maybe Desc :=
ψ cs' = traverseMaybeList ?(Name × Term) ?CDesc
(recursionProduct ?Name ?Term ?(Maybe CDesc) (toCDesc name))
cs : Maybe (List CDesc).
λ genRecord : Bool.
ifthenelse ?(Maybe Desc) genRecord
(just ?Desc $ mkDesc name t [Term|] [CDesc|
let init$data2$_string_^space^_telescope_^space^=colon=^space^_multiTerm_^space'^=dot=^space^_entries_
(name : String) (t : Telescope) (ty : Term) (cs : List (Name × Term)) : Bool -> Error Desc :=
λ genRecord : Bool. ifthenelse ?(Error Desc) genRecord
(pureError ?Desc $ mkDesc name t [Term|] [CDesc|
mkTripleProduct ?Name ?(List ADesc) ?(List Term)
φ"mk${name}"
(map ?(Name × Term) ?ADesc (recursionProduct ?Name ?Term ?ADesc
(λ n : Name. λ t : Term. prodPair ?Name ?TDesc n (tdNonRec t)))
cs)
[Term|]])
(mapMaybe ?(List CDesc) ?Desc (mkDesc name t [Term|]) cs').

elet init$newStmt'$data2^space^_data2_=dot= (genD : Bool -> Maybe Desc) : Eval Unit :=
maybe ?_ ?_ (throwEval ?Unit "Error: not a valid datatype!")
(λ d : Desc. DefineHelpers d >> DefineTy d >> DefineInd d)
(genD false).

elet init$newStmt'$record2^space^_data2_=dot= (genD : Bool -> Maybe Desc) : Eval Unit :=
maybe ?_ ?_ (throwEval ?Unit "Error: not a valid record!")
(λ r : Desc. DefineHelpers r >> DefineTy r >> DefineInd r >> DefineProjLIs r)
(genD true).
[Term|]]) $
bindError ?(List CDesc) ?Desc (traverseErrorList ?(Name × Term) ?CDesc
(recursionProduct ?Name ?Term ?(Error CDesc) (toCDesc name))
cs) (λ cs' : List CDesc.
bindError ?Telescope ?Desc (parseIxs ty) (λ ixs : Telescope.
pureError ?Desc $ mkDesc name t (map ?Param ?Term paramType ixs) cs')).

elet init$newStmt'$data2^space^_data2_=dot= (genD : Bool -> Error Desc) : Eval Unit :=
runError ?Desc ?(Eval Unit) (genD false)
(λ e : String. throwEval ?Unit φ"Error: not a valid datatype! ${e}")
(λ d : Desc. DefineHelpers d >> DefineTy d >> DefineInd d).

elet init$newStmt'$record2^space^_data2_=dot= (genD : Bool -> Error Desc) : Eval Unit :=
runError ?_ ?_ (genD true)
(λ e : String. throwEval ?Unit φ"Error: not a valid record! ${e}")
(λ r : Desc. DefineHelpers r >> DefineTy r >> DefineInd r >> DefineProjLIs r).

updateEval.
36 changes: 16 additions & 20 deletions mced/Test/Datatypes2/Test.mced
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,51 +36,47 @@ updateEval.
--------------------------------------------------------------------------------
-- Tests

elet T5Desc : Desc := preprocessDesc ("TVec", [Param|false, "A", θ{*}], [Term|θ{Nat}],
[CDesc| "tVecNil", [ADesc|], [Term|θ{0}]
; "tVecCons", [ADesc|"k", tdNonRec θ{Nat}; adUnnamed (tdNonRec θ{A}); adUnnamed (tdRecNN [Term|θ{k}])], [Term|θ{suc k}]]).
data2 TVec (A : *) : Nat -> *.
| tVecNil : TVec 0
| tVecCons : Π k : Nat. A -> TVec k -> TVec (suc k).

elet TEvenDesc : Desc := preprocessDesc ("TEven", [Param|], [Term|θ{Nat}],
[CDesc| "tEvenZ", [ADesc|], [Term|θ{0}]
; "tEvenSS", [ADesc|"k", tdNonRec θ{Nat}; adUnnamed (tdRecNN [Term|θ{k}])], [Term|θ{suc (suc k)}]]).
data2 TEven : Nat -> *.
| tEvenZ : TEven 0
| tEvenSS : Π k : Nat. TEven k -> TEven (suc (suc k)).

elet TLeqDesc : Desc := preprocessDesc ("TLeq", [Param|], [Term|θ{Nat}; θ{Nat}],
[CDesc| "zlek", [ADesc|"k", tdNonRec θ{Nat}], [Term|θ{0}; θ{k}]
; "sles", [ADesc|"k", tdNonRec θ{Nat}; "l", tdNonRec θ{Nat}; adUnnamed (tdRecNN [Term|θ{k}; θ{l}])], [Term|θ{suc k}; θ{suc l}]]).
data2 TLeq : Nat -> Nat -> *.
| zlek : Π k : Nat. TLeq 0 k
| sles : Π k, l : Nat. TLeq k l -> TLeq (suc k) (suc l).

data2Test T5Desc.
data2Test TEvenDesc.
data2Test TLeqDesc.

data2 TNat where
data2 TNat : *.
| tZero : TNat
| tSuc : TNat -> TNat.

data2 TNatList where
data2 TNatList : *.
| tNatNil : TNatList
| tNatCons : Nat -> TNatList -> TNatList.

record2 TProd (A, B : *) where
record2 TProd (A, B : *) : *.
| tPr1 : A
| tPr2 : B.

record2 TDSum' (A : *) (B : A -> *) where
record2 TDSum' (A : *) (B : A -> *) : *.
| tDPr1 : A
| tDPr2 : B tDPr1.

data2 TList (A : *) where
data2 TList (A : *) : *.
| tNil : TList
| tCons : A -> TList -> TList.

data2 T1 where
data2 T1 : *.
| 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.

data2 T2 where
data2 T2 : *.
| t21 : Nat -> T2
| t22 : T2 -> T2 -> T2.

Expand Down

0 comments on commit 3cbf443

Please sign in to comment.