quote.ml (3641B)
1 open Util 2 open Eval 3 module I = Internal 4 module V = Value 5 6 let rec bind_patt_twice 7 : V.environment * V.environment -> I.patt -> V.environment * V.environment 8 = fun (env0, env1) {disc; _} -> 9 let vars = Uniq.fresh 1 in 10 let env0 = Env.bind env0 vars in 11 let env1 = Env.bind env1 vars in 12 match disc with 13 | I.DWild _ -> (env0, env1) 14 | I.DData {subpatts; _} -> 15 let arity = Array.length subpatts in 16 let subvars = Uniq.fresh arity in 17 let env0 = Env.bind env0 subvars in 18 let env1 = Env.bind env1 subvars in 19 Array.fold_left bind_patt_twice (env0, env1) subpatts 20 21 let rec quote 22 : V.environment -> V.value -> I.term 23 = fun env -> function 24 | V.RefClo (env', t) -> shift env !env' t 25 | V.NeutralMatch {scrutinee; cases_clo = (clo, cases); switch} -> 26 I.Match { 27 scrutinee = quote env scrutinee; 28 cases = Array.map (shift_case env clo) cases; 29 switch; 30 } 31 | V.NeutralApp (fn, args) -> 32 I.App (quote env fn, Array.map (quote env) args) 33 | V.FnClosure (clo, abs) -> 34 I.Fn (shift_abstraction env clo abs) 35 | V.FnTypeClosure (clo, abs) -> 36 I.FnType (shift_abstraction env clo abs) 37 | V.Data {tag; tagi; args; datatype_clo = (clo, datatype)} -> 38 I.Data { 39 tag; 40 tagi; 41 args = Array.map (quote env) args; 42 datatype = shift_datatype env clo datatype; 43 } 44 | V.DataTypeClosure (clo, datatype) -> 45 I.DataType (shift_datatype env clo datatype) 46 | V.Nat n -> I.Nat n 47 | V.Arb var -> 48 begin match Env.quote env var with 49 | Some ij -> I.Var ij 50 | None -> impossible "Eval.quote: env does not bind variable" 51 end 52 | V.Builtin b -> I.Builtin b 53 | V.Future _ -> impossible "Eval.quote: can not quote future" 54 55 and shift 56 : V.environment -> V.environment -> I.term -> I.term 57 = fun dst src t -> quote dst (eval src t) 58 59 and shift_case 60 : V.environment -> V.environment -> I.case -> I.case 61 = fun dst src {patt; body} -> 62 let patt = shift_patt dst src patt in 63 let (dst, src) = bind_patt_twice (dst, src) patt in 64 let body = shift dst src body in 65 {patt; body} 66 67 and shift_binder 68 : V.environment -> V.environment -> I.binder -> I.binder 69 = fun dst src {plicity; patt} -> 70 { 71 plicity; 72 patt = shift_patt dst src patt; 73 } 74 75 and bind_and_shift_multibinder 76 : V.environment -> V.environment -> I.multibinder 77 -> V.environment * V.environment * I.multibinder 78 = fun dst src {binders; order} -> 79 let arity = Array.length binders in 80 let vars = Uniq.fresh arity in 81 let dst = Env.bind dst vars in 82 let src = Env.bind src vars in 83 let multibinder = { 84 I.binders = Array.map (shift_binder dst src) binders; 85 I.order; 86 } in 87 (dst, src, multibinder) 88 89 and shift_multibinder 90 : V.environment -> V.environment -> I.multibinder -> I.multibinder 91 = fun dst src multibinder -> 92 let (_, _, multibinder) = 93 bind_and_shift_multibinder dst src multibinder in 94 multibinder 95 96 and shift_abstraction 97 : V.environment -> V.environment -> I.abstraction -> I.abstraction 98 = fun dst src {multibinder; term} -> 99 let (dst, src, multibinder) = 100 bind_and_shift_multibinder dst src multibinder in 101 { 102 multibinder; 103 term = shift dst src term; 104 } 105 106 and shift_patt 107 : V.environment -> V.environment -> I.patt -> I.patt 108 = fun dst src {names; disc} -> 109 { 110 names; 111 disc = shift_disc dst src disc; 112 } 113 114 and shift_disc 115 : V.environment -> V.environment -> I.discriminant -> I.discriminant 116 = fun dst src -> function 117 | I.DWild typ -> I.DWild (shift dst src typ) 118 | I.DData {tag; tagi; subpatts; datatype} -> 119 I.DData { 120 tag; 121 tagi; 122 subpatts = Array.map (shift_patt dst src) subpatts; 123 datatype = shift_datatype dst src datatype; 124 } 125 126 and shift_datatype 127 : V.environment -> V.environment -> I.datatype -> I.datatype 128 = fun dst src {ctors; names} -> 129 { 130 ctors = Array.map (shift_multibinder dst src) ctors; 131 names; 132 }