eval.ml (5997B)
1 open Util 2 module B = Builtin 3 module I = Internal 4 module V = Value 5 6 (* TODO: "Glued" evaluation? I.e., evaluation that only lazily unfolds in some 7 * cases? *) 8 (* TODO: Lazily evaluate args? *) 9 10 let rec define_data_args 11 : V.environment -> V.value -> I.patt -> V.environment 12 = fun env value {disc; _} -> match value, disc with 13 | value, I.DWild _ -> env 14 | V.Data v, I.DData d -> 15 begin if v.tagi <> d.tagi then 16 impossible "Eval.define_data_args: value and disc have different tag" 17 end; 18 let tagi = v.tagi in 19 let (_, {I.ctors; _}) = v.datatype_clo in 20 let vorder = ctors.(tagi).order in 21 let dorder = d.datatype.ctors.(tagi).order in 22 23 begin if Array.length v.args <> Array.length d.subpatts then 24 impossible "Eval.define_data_args: value and disc have different arity" 25 end; 26 let arity = Array.length v.args in 27 28 let subvars = Uniq.fresh arity in 29 let env = Env.bind env subvars in 30 let env = ref env in 31 for i = 0 to arity - 1 do 32 begin if vorder.(i) <> dorder.(i) then 33 impossible "Eval.define_data_args: value and disc have different order" 34 end; 35 let j = vorder.(i) in 36 37 let subvar = Uniq.get subvars j in 38 env := Env.define !env subvar v.args.(j); 39 env := define_data_args !env v.args.(j) d.subpatts.(j) 40 done; 41 42 !env 43 | _, I.DData _ -> 44 impossible "Eval.define_data_args: value is not data, but disc is" 45 46 let lower_bool 47 : bool -> V.value 48 = fun b -> if b then Std.v_true else Std.v_false 49 50 let rec eval 51 : V.environment -> I.term -> V.value 52 = fun env -> function 53 | I.Let (definers, body) -> 54 let ndefiners = Array.length definers in 55 let vars = Uniq.fresh ndefiners in 56 let env = Env.bind env vars in 57 let env = ref env in 58 for i = 0 to ndefiners - 1 do 59 let vrhs = V.RefClo (env, definers.(i).rhs) in 60 env := Env.define !env (Uniq.get vars i) vrhs 61 done; 62 eval !env body 63 | I.Match {scrutinee; cases; switch} -> 64 do_match (eval env scrutinee) (env, cases) switch 65 | I.App (fn, args) -> apply (eval env fn) (Array.map (eval env) args) 66 | I.Fn fn -> V.FnClosure (env, fn) 67 | I.FnType fntype -> V.FnTypeClosure (env, fntype) 68 | I.Data {tag; tagi; args; datatype} -> 69 V.Data { 70 tag; 71 tagi; 72 args = Array.map (eval env) args; 73 datatype_clo = (env, datatype); 74 } 75 | I.DataType datatype -> V.DataTypeClosure (env, datatype) 76 | I.Nat n -> V.Nat n 77 | I.Var ij -> 78 let var = Env.index env ij in 79 begin match Env.eval env var with 80 | Some v -> v 81 | None -> V.Arb var 82 end 83 | I.Builtin b -> V.Builtin b 84 85 and do_match 86 : V.value -> I.case array V.closure -> I.switch -> V.value 87 = fun scrutinee (clo, cases) switch -> 88 let vars = Uniq.fresh 1 in 89 let var = Uniq.get vars 0 in 90 let switch_env = Env.bind Env.empty vars in 91 let switch_env = Env.define switch_env var scrutinee in 92 begin match do_switch switch_env (Index.Of (0, 0)) switch with 93 | Some casei -> 94 let {I.patt; I.body} = cases.(casei) in 95 let clo = Env.bind clo vars in 96 let clo = Env.define clo var scrutinee in 97 let clo = define_data_args clo scrutinee patt in 98 (* TODO: "Unify" the scrutinee with the pattern. E.g., if the scrutinee 99 * is a variable, then it gets defined to the "term-version" of the 100 * pattern, which can make some values require further reduction. *) 101 eval clo body 102 | None -> V.NeutralMatch {scrutinee; cases_clo = (clo, cases); switch} 103 end 104 105 and do_switch env ij = function 106 | Switch {index = ij'; subswitches; _} -> 107 let var = Env.index env ij in 108 begin match Env.eval env var with 109 | Some (V.Data {tagi; args; _}) -> 110 let arity = Array.length args in 111 let subvars = Uniq.fresh arity in 112 let env = Env.bind env subvars in 113 let env = ref env in 114 for i = 0 to arity - 1 do 115 let subvar = Uniq.get subvars i in 116 env := Env.define !env subvar args.(i) 117 done; 118 do_switch !env ij' subswitches.(tagi) 119 | Some _ -> None (* Neutral match *) 120 | None -> impossible "Eval.switch: undefined variable" 121 end 122 | Goto casei -> Some casei 123 124 and apply 125 : V.value -> V.value array -> V.value 126 = fun fn args -> match fn, args with 127 | V.RefClo (env, t), args -> apply (eval !env t) args 128 | V.FnClosure (clo, {multibinder = {binders; _}; term = body}), args -> 129 let arity = Array.length binders in 130 let vars = Uniq.fresh arity in 131 let clo = Env.bind clo vars in 132 let clo = ref clo in 133 for i = 0 to arity - 1 do 134 clo := Env.define !clo (Uniq.get vars i) args.(i) 135 done; 136 eval !clo body 137 | V.Builtin B.NatOpAdd, [|V.Nat m; V.Nat n|] -> V.Nat (Z.add m n) 138 | V.Builtin B.NatOpSub, [|V.Nat m; V.Nat n|] -> 139 V.Nat (if Z.lt m n then Z.zero else Z.sub m n) 140 | V.Builtin B.NatOpMul, [|V.Nat m; V.Nat n|] -> V.Nat (Z.mul m n) 141 | V.Builtin B.NatOpDiv, [|V.Nat m; V.Nat n|] -> 142 V.Nat (if Z.equal n Z.zero then Z.zero else Z.div m n) 143 | V.Builtin B.NatOpMod, [|V.Nat m; V.Nat n|] -> 144 V.Nat (if Z.equal n Z.zero then Z.zero else Z.rem m n) 145 | V.Builtin B.NatOpLt, [|V.Nat m; V.Nat n|] -> lower_bool @@ Z.lt m n 146 | V.Builtin B.NatOpLe, [|V.Nat m; V.Nat n|] -> lower_bool @@ Z.leq m n 147 | V.Builtin B.NatOpEq, [|V.Nat m; V.Nat n|] -> lower_bool @@ Z.equal m n 148 | V.Builtin B.NatOpGe, [|V.Nat m; V.Nat n|] -> lower_bool @@ Z.geq m n 149 | V.Builtin B.NatOpGt, [|V.Nat m; V.Nat n|] -> lower_bool @@ Z.gt m n 150 | V.Builtin B.NatOpNe, [|V.Nat m; V.Nat n|] -> lower_bool @@ not (Z.equal m n) 151 | fn, args -> V.NeutralApp (fn, args) 152 153 (* TODO: This is inefficient. We should do something smarter, like lifting 154 * stuck variables to the outside of neutral terms so we can force them without 155 * needing to recurse (i.e., use spine form). *) 156 and force 157 : V.environment -> V.value -> V.value 158 = fun env -> function 159 | V.RefClo (env', t) -> force env (eval !env' t) 160 | V.NeutralMatch {scrutinee; cases_clo; switch} -> 161 do_match (force env scrutinee) cases_clo switch 162 (* XXX: There's no reason to force the arguments for "CbNeed redexes" (i.e., 163 * when fn is a lambda), but we do need to force args in a "CbValue redex" 164 * (i.e., when fn is a builtin with builtin reduction rules). *) 165 | V.NeutralApp (fn, args) -> 166 apply (force env fn) (Array.map (force env) args) 167 | V.Arb var -> 168 begin match Env.eval env var with 169 | Some v -> force env v 170 | None -> V.Arb var 171 end 172 | v -> v