internal.ml (3265B)
1 open Node 2 module B = Builtin 3 4 (* Ideas for implicit args/metavariables/unification: Unlike in Andras's 5 * elaboration-zoo, we use globally fresh names in the semantic domain, so 6 * when checking that all variables that occur in a candidate solution for a 7 * metavariable are in scope at the metavariable's site of creation, we don't 8 * need to do any index/level manipulation. Rather, it suffices to simply 9 * lookup the uniq in the metavariable's environment: if it's there, then the 10 * variable is in scope and all is well; otherwise, the variable is out of 11 * scope and we produce a unification error. 12 * 13 * In the elaboration-zoo, metas are instead viewed as closed terms 14 * lambda-abstracted over the entire ambient environment (i.e., roughly 15 * speaking, such that a solution to a meta Γ ⊢ m has form ⋅ ⊢ λ Γ. t for some 16 * term t), which has the disadvantage that forming a meta takes time linear in 17 * the size of the environment. 18 * 19 * When actually solving a metavariable (which happens during unification 20 * between two values, namely the metavariable and its candidate solution), we 21 * optimistically try to quote the candidate solution inside the metavariable's 22 * environment, which will (rightfully) fail if the candidate solution depends 23 * on out-of-scope variables. 24 * 25 * Maybe we can represent metavariables in values as simply a value option ref. 26 * Then when checking an argument list, we keep track of all these refs (one 27 * per implicit argument), and ensure after elaborating every argument that the 28 * metas have been solved to Some solution. Better: Use an inline record so 29 * that there's 1 indirection instead of 2. I.e., V.value becomes 30 * ... | Meta of {mutable soln: V.value} 31 *) 32 33 (* TODO: When we actually start compiling to low-level code, we need to 34 * consider where types should be stored on internal terms. *) 35 36 type term = 37 | Let of definer array * term 38 | Match of { 39 scrutinee: term; 40 cases: case array; 41 switch: switch; 42 } 43 | App of term * term array 44 | Fn of abstraction 45 | FnType of abstraction 46 | Data of { 47 tag: Name.Tag.t; 48 tagi: int; 49 args: term array; 50 datatype: datatype; 51 } 52 | DataType of datatype 53 | Nat of Z.t 54 | Var of Index.t 55 | Builtin of B.builtin 56 57 and definer = { 58 names: Name.Var.t array; 59 rhs: term; 60 typ: term; 61 } 62 63 and case = { 64 patt: patt; 65 body: term; 66 } 67 68 and binder = { 69 plicity: Plicity.t; 70 patt: patt; 71 } 72 73 and multibinder = { 74 binders: binder array; 75 order: int array; 76 } 77 78 and abstraction = { 79 multibinder: multibinder; 80 term: term; 81 } 82 83 and patt = { 84 names: Name.Var.t array; 85 disc: discriminant; 86 } 87 88 and discriminant = 89 | DWild of term 90 | DData of data_discriminant 91 92 and data_discriminant = { 93 tag: Name.Tag.t; 94 tagi: int; 95 subpatts: patt array; 96 datatype: datatype; 97 } 98 99 (* Decision tree of match. Switch is an internal node that switches on a 100 * non-empty datatype, and Goto is a leaf node that jumps to the indicated 101 * case. *) 102 and switch = 103 | Switch of { 104 index: Index.t; 105 subswitches: switch array; 106 names: int Name.Tag.Map.t; (* For pretty-printing. *) 107 } 108 | Goto of int 109 110 and datatype = { 111 ctors: multibinder array; 112 names: int Name.Tag.Map.t; (* TODO: Rename to "tagis" for consistency *) 113 } 114 115 let disc_type 116 : discriminant -> term 117 = function 118 | DWild typ -> typ 119 | DData {datatype; _} -> DataType datatype