Add GetDef primitive

WhatisRT · Jan 8, 2024 · bf4a0c9 · bf4a0c9
1 parent 8999b2e
commit bf4a0c9
Show file tree

Hide file tree

Showing 25 changed files with 217 additions and 197 deletions.
diff --git a/mced/Bootstrap/Compiled/ConversionHelpers.mced b/mced/Bootstrap/Compiled/ConversionHelpers.mced
@@ -1,13 +1,13 @@
-let nothingTerm := Λ X : * λ v : Π _ : Var X λ s : Π _ : Sort X λ b : Π _ : Binder Π _ : String Π _ : X Π _ : X X λ a : Π _ : X Π _ : [List [[Product Bool] X]] X λ k : Π _ : Char X λ x : X λ u : Π _ : X X [[a [[[[[[[<quoteSq X> v] s] b] a] k] x] u]] [[<<map [[Product Bool] Term]> [[Product Bool] X]> [<<<recursionProduct Bool> Term> [[Product Bool] X]> λ b' : Bool λ t : Term [[<<prodPair Bool> X> b'] [[[[[[[<t X> v] s] b] a] k] x] u]]]] <nil App>]] : Term.
+let nothingTerm := [[appLTerm quoteSq] <nil App>] : Term.
 let nothingTerm1 := λ _ : Term nothingTerm : Π _ : Term Term.
 let nothingTerm2 := λ _ : Term λ _ : Term nothingTerm : Π _ : Term Π _ : Term Term.
 let nothingTerm3 := λ _ : Term λ _ : Term λ _ : Term nothingTerm : Π _ : Term Π _ : Term Π _ : Term Term.
 let cedilleTerm := λ s : String [sVarTerm s] : Π s : String Term.
 let cedilleTerm1 := λ s : String λ t : Term [[appSingle [sVarTerm s]] t] : Π s : String Π t : Term Term.
 let cedilleTerm2 := λ s : String λ t : Term λ t' : Term [[[appDouble [sVarTerm s]] t] t'] : Π s : String Π t : Term Π t' : Term Term.
 let cedilleTerm3 := λ s : String λ t : Term λ t' : Term λ t'' : Term [[appSingle [[[appDouble [sVarTerm s]] t] t']] t''] : Π s : String Π t : Term Π t' : Term Π t'' : Term Term.
-let initTermToTerm := λ t : iTerm [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[<t Term> varTerm] sortTerm] λ c : Const [[[[[[[[<c Term> [sVarTerm [[stringCons κC] [[stringCons κh] [[stringCons κa] [[stringCons κr] stringNil]]]]]] charTerm] [sVarTerm [[stringCons κc] [[stringCons κh] [[stringCons κa] [[stringCons κr] [[stringCons κE] [[stringCons κq] stringNil]]]]]]]] [sVarTerm [[stringCons κM] stringNil]]] [sVarTerm [[stringCons κb] [[stringCons κi] [[stringCons κn] [[stringCons κd] [[stringCons κM] stringNil]]]]]]] [sVarTerm [[stringCons κp] [[stringCons κu] [[stringCons κr] [[stringCons κe] [[stringCons κM] stringNil]]]]]]] [sVarTerm [[stringCons κc] [[stringCons κa] [[stringCons κt] [[stringCons κc] [[stringCons κh] [[stringCons κE] [[stringCons κr] [[stringCons κr] stringNil]]]]]]]]]] [sVarTerm [[stringCons κf] [[stringCons κi] [[stringCons κx] stringNil]]]]]] [cedilleTerm1 [[stringCons κπ] [[stringCons κ1] stringNil]]]] [cedilleTerm1 [[stringCons κπ] [[stringCons κ2] stringNil]]]] [cedilleTerm2 [[stringCons κβ] stringNil]]] [cedilleTerm2 [[stringCons κδ] stringNil]]] [cedilleTerm1 [[stringCons κσ] stringNil]]] [cedilleTerm3 [[stringCons κφ] stringNil]]] [cedilleTerm2 [[stringCons κ=] stringNil]]] appSingle] appSingleE] λ t : Term λ _ : String λ t' : Term λ t'' : Term [[[[cedilleTerm3 [[stringCons κρ] stringNil]] t] t'] t'']] [binderTerm forallBinder]] [binderTerm piBinder]] [binderTerm lambdaBinder]] [binderTerm LambdaBinder]] λ _ : String [cedilleTerm2 [[stringCons κι] stringNil]]] λ t : Term λ t' : Term λ _ : String λ _ : Term [[[cedilleTerm2 [[stringCons κς] [[stringCons κP] [[stringCons κa] [[stringCons κi] [[stringCons κr] stringNil]]]]]] t] t']] nothingTerm1] nothingTerm2] nothingTerm1] nothingTerm2] nothingTerm3] nothingTerm3] nothingTerm2] nothingTerm2] nothingTerm3] nothingTerm1] nothingTerm1] nothingTerm1] nothingTerm1] nothingTerm] nothingTerm1] nothingTerm2] nothingTerm] nothingTerm1] : Π t : iTerm Term.
+let initTermToTerm := λ t : iTerm [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[<t Term> varTerm] sortTerm] λ c : Const [[[[[[[[<c Term> [sVarTerm [[stringCons κC] [[stringCons κh] [[stringCons κa] [[stringCons κr] stringNil]]]]]] charTerm] [sVarTerm [[stringCons κc] [[stringCons κh] [[stringCons κa] [[stringCons κr] [[stringCons κE] [[stringCons κq] stringNil]]]]]]]] [sVarTerm [[stringCons κM] stringNil]]] [sVarTerm [[stringCons κb] [[stringCons κi] [[stringCons κn] [[stringCons κd] [[stringCons κM] stringNil]]]]]]] [sVarTerm [[stringCons κp] [[stringCons κu] [[stringCons κr] [[stringCons κe] [[stringCons κM] stringNil]]]]]]] [sVarTerm [[stringCons κc] [[stringCons κa] [[stringCons κt] [[stringCons κc] [[stringCons κh] [[stringCons κE] [[stringCons κr] [[stringCons κr] stringNil]]]]]]]]]] [sVarTerm [[stringCons κf] [[stringCons κi] [[stringCons κx] stringNil]]]]]] [cedilleTerm1 [[stringCons κπ] [[stringCons κ1] stringNil]]]] [cedilleTerm1 [[stringCons κπ] [[stringCons κ2] stringNil]]]] [cedilleTerm2 [[stringCons κβ] stringNil]]] [cedilleTerm2 [[stringCons κδ] stringNil]]] [cedilleTerm1 [[stringCons κσ] stringNil]]] [cedilleTerm3 [[stringCons κφ] stringNil]]] [cedilleTerm2 [[stringCons κ=] stringNil]]] appSingle] appSingleE] λ t : Term λ _ : String λ t' : Term λ t'' : Term [[[[cedilleTerm3 [[stringCons κρ] stringNil]] t] t'] t'']] [binderTerm forallBinder]] [binderTerm piBinder]] [binderTerm lambdaBinder]] [binderTerm LambdaBinder]] λ _ : String [cedilleTerm2 [[stringCons κι] stringNil]]] λ t : Term λ t' : Term λ _ : String λ _ : Term [[[cedilleTerm2 [[stringCons κς] [[stringCons κP] [[stringCons κa] [[stringCons κi] [[stringCons κr] stringNil]]]]]] t] t']] nothingTerm1] nothingTerm2] nothingTerm1] nothingTerm2] nothingTerm3] nothingTerm3] nothingTerm2] nothingTerm2] nothingTerm3] nothingTerm1] nothingTerm1] nothingTerm1] nothingTerm1] nothingTerm] nothingTerm1] nothingTerm2] nothingTerm] nothingTerm1] nothingTerm1] : Π t : iTerm Term.
 let telescopeFromTypeHelper := λ t : Term [[<<prodPair [List Param]> Term> telNil] t] : Π t : Term [[Product Telescope] Term].
 let telCons := λ n : String λ T : Term [<cons [[Product Bool] PreParam]> [[mkParam false] [[mkPreParam n] T]]] : Π n : String Π T : Term Π as : [List [[Product Bool] PreParam]] [List [[Product Bool] PreParam]].
 let telConsE := λ n : String λ T : Term [<cons [[Product Bool] PreParam]> [[mkParam true] [[mkPreParam n] T]]] : Π n : String Π T : Term Π as : [List [[Product Bool] PreParam]] [List [[Product Bool] PreParam]].
-let telescopeFromType := λ term : Term [<<pr1 [[Product Telescope] Term]> Term> [[[[[[[<term [[Product [[Product Telescope] Term]] Term]> λ v : Var [[<<prodPair [[Product Telescope] Term]> Term> [λ v : Var [telescopeFromTypeHelper [varTerm v]] v]] [varTerm v]]] λ s : Sort [[<<prodPair [[Product Telescope] Term]> Term> [λ s : Sort [telescopeFromTypeHelper [sortTerm s]] s]] [sortTerm s]]] λ b : Binder λ n : String [<<<recursionProduct [[Product Telescope] Term]> Term> Π _ : [[Product [[Product Telescope] Term]] Term] [[Product [[Product Telescope] Term]] Term]> λ T1 : [[Product Telescope] Term] λ T2 : Term [<<<recursionProduct [[Product Telescope] Term]> Term> [[Product [[Product Telescope] Term]] Term]> λ t1 : [[Product Telescope] Term] λ t2 : Term [[<<prodPair [[Product Telescope] Term]> Term> [[[[[[λ b : Binder λ n : String λ t : Term λ t' : Term λ rect : [[Product Telescope] Term] λ rect' : [[Product Telescope] Term] [[[[<b [[Product Telescope] Term]> [telescopeFromTypeHelper [[[lambdaTerm n] t] t']]] [telescopeFromTypeHelper [[[LambdaTerm n] t] t']]] [[<<<productMap1 Telescope> Term> [List [[Product Bool] PreParam]]> [[telCons n] t]] rect']] [[<<<productMap1 Telescope> Term> [List [[Product Bool] PreParam]]> [[telConsE n] t]] rect']] b] n] T2] t2] T1] t1]] [[[[binderTerm b] n] T2] t2]]]]] [<<<recursionProduct [[Product Telescope] Term]> Term> Π _ : [List [[Product Bool] [[Product [[Product Telescope] Term]] Term]]] [[Product [[Product Telescope] Term]] Term]> λ t1 : [[Product Telescope] Term] λ t2 : Term λ l : [List [[Product Bool] [[Product [[Product Telescope] Term]] Term]]] [[<<<recursionProduct [List [[Product Bool] [[Product Telescope] Term]]]> [List [[Product Bool] Term]]> [[Product [[Product Telescope] Term]] Term]> λ l1 : [List [[Product Bool] [[Product Telescope] Term]]] λ l2 : [List [[Product Bool] Term]] [[<<prodPair [[Product Telescope] Term]> Term> [[[[λ t : Term λ app : [List App] λ _ : [[Product Telescope] Term] λ _ : [List [[Product Bool] [[Product Telescope] Term]]] [telescopeFromTypeHelper [[appLTerm t] app]] t2] l2] t1] l1]] [[appLTerm t2] l2]]] [<<<distList Bool> [[Product Telescope] Term]> Term> l]]]] λ c : Char [[<<prodPair [[Product Telescope] Term]> Term> [λ c : Char [telescopeFromTypeHelper [charTerm c]] c]] [charTerm c]]] [[<<prodPair [[Product Telescope] Term]> Term> [telescopeFromTypeHelper unknownTerm]] unknownTerm]] [<<<recursionProduct [[Product Telescope] Term]> Term> [[Product [[Product Telescope] Term]] Term]> λ u1 : [[Product Telescope] Term] λ u2 : Term [[<<prodPair [[Product Telescope] Term]> Term> [[λ u : Term λ _ : [[Product Telescope] Term] [telescopeFromTypeHelper [unquoteTerm u]] u2] u1]] [unquoteTerm u2]]]]] : Π _ : Term [[Product Telescope] Term].
+let telescopeFromType := [[[[[[[<recursionTerm [[Product Telescope] Term]> λ v : Var [telescopeFromTypeHelper [varTerm v]]] λ s : Sort [telescopeFromTypeHelper [sortTerm s]]] λ b : Binder λ n : String λ t : Term λ t' : Term λ rect : [[Product Telescope] Term] λ rect' : [[Product Telescope] Term] [[[[<b [[Product Telescope] Term]> [telescopeFromTypeHelper [[[lambdaTerm n] t] t']]] [telescopeFromTypeHelper [[[LambdaTerm n] t] t']]] [[<<<productMap1 Telescope> Term> [List [[Product Bool] PreParam]]> [[telCons n] t]] rect']] [[<<<productMap1 Telescope> Term> [List [[Product Bool] PreParam]]> [[telConsE n] t]] rect']]] λ t : Term λ app : [List App] λ _ : [[Product Telescope] Term] λ _ : [List [[Product Bool] [[Product Telescope] Term]]] [telescopeFromTypeHelper [[appLTerm t] app]]] λ c : Char [telescopeFromTypeHelper [charTerm c]]] [telescopeFromTypeHelper unknownTerm]] λ u : Term λ _ : [[Product Telescope] Term] [telescopeFromTypeHelper [unquoteTerm u]]] : Π _ : Term [[Product Telescope] Term].