unify.ml (5168B)
1 open Util 2 open Eval 3 module I = Internal 4 module V = Value 5 6 exception UnifyFail 7 8 (* TODO: Make this actually solve metas *) 9 (* TODO: η-equality? *) 10 (* Precondition: Both values have the same type. *) 11 let rec unify 12 : V.environment -> V.value -> V.value -> unit 13 = fun env v0 v1 -> match force env v0, force env v1 with 14 | V.RefClo _, _ -> impossible "Unify.unify: RefClo's are removed during forcing" 15 | _, V.RefClo _ -> impossible "Unify.unify: RefClo's are removed during forcing" 16 | V.NeutralMatch _, V.NeutralMatch _ -> no_impl "unify neutral match" 17 | V.NeutralApp (fn0, args0), V.NeutralApp (fn1, args1) -> 18 (* Note that args0 and args1 aren't necessarily the same length, but they 19 * are if fn0 and fn1 unify, so the short-circuiting of (&&) ensures that 20 * for_all2 can't fail. *) 21 (* XXX: fn0 and fn1 needn't have the same type, so we are technically not 22 * obeying the precondition of unify here. However, it's ok in this case, 23 * because fn0 and fn1 can't be Fn's. Rather, fn0 and fn1 are either 24 * variables or builtins, which will fail to unify if they have different 25 * types. *) 26 unify env fn0 fn1; 27 Array.iter2 (unify env) args0 args1 28 | V.FnClosure (clo0, abs0), V.FnClosure (clo1, abs1) -> 29 (* XXX: Testing the entire abstraction for conversion is overkill: Since 30 * both Fn's are assumed to have the same type, we know both multibinders 31 * are convertible, so it suffices to bind fresh variables in the envs and 32 * then test the bodies for conversion. *) 33 conv_abstraction env clo0 clo1 abs0 abs1 34 | V.FnTypeClosure (clo0, abs0), V.FnTypeClosure (clo1, abs1) -> 35 conv_abstraction env clo0 clo1 abs0 abs1 36 | V.Data {tagi = tagi0; args = args0; _}, V.Data {tagi = tagi1; args = args1; _} -> 37 begin if tagi0 <> tagi1 then 38 raise UnifyFail 39 end; 40 Array.iter2 (unify env) args0 args1 41 | V.DataTypeClosure (clo0, datatype0), V.DataTypeClosure (clo1, datatype1) -> 42 conv_datatype env clo0 clo1 datatype0 datatype1 43 | V.Nat n, V.Nat m -> if not @@ Z.equal n m then raise UnifyFail 44 | V.Arb var0, V.Arb var1 -> if var0 <> var1 then raise UnifyFail 45 | V.Builtin b0, V.Builtin b1 -> if b0 <> b1 then raise UnifyFail 46 | V.Future _, _ -> impossible "Unify.unify: Futures do not unify" 47 | _, V.Future _ -> impossible "Unify.unify: Futures do not unify" 48 | (V.NeutralMatch _ | V.NeutralApp _ | V.FnClosure _ | V.FnTypeClosure _ 49 | V.Data _ | V.DataTypeClosure _ | V.Nat _ | V.Arb _ | V.Builtin _), _ -> 50 raise UnifyFail 51 52 and conv 53 : V.environment -> V.environment -> V.environment -> I.term -> I.term -> unit 54 = fun env clo0 clo1 t0 t1 -> 55 let v0 = eval clo0 t0 in 56 let v1 = eval clo1 t1 in 57 unify env v0 v1 58 59 and conv_binder 60 : V.environment -> V.environment -> V.environment 61 -> I.binder -> I.binder -> unit 62 = fun env clo0 clo1 binder0 binder1 -> 63 begin if binder0.plicity <> binder1.plicity then 64 raise UnifyFail 65 end; 66 conv_patt env clo0 clo1 binder0.patt binder1.patt 67 68 and bind_and_conv_multibinder 69 : V.environment -> V.environment -> V.environment 70 -> I.multibinder -> I.multibinder 71 -> V.environment * V.environment * V.environment 72 = fun env clo0 clo1 multibinder0 multibinder1 -> 73 let arity0 = Array.length multibinder0.binders in 74 let arity1 = Array.length multibinder1.binders in 75 begin if arity0 <> arity1 then 76 raise UnifyFail 77 end; 78 79 begin if not @@ Array.for_all2 Int.equal 80 multibinder0.order multibinder1.order then 81 raise UnifyFail 82 end; 83 84 let vars = Uniq.fresh arity0 in 85 let env = Env.bind env vars in 86 let clo0 = Env.bind clo0 vars in 87 let clo1 = Env.bind clo1 vars in 88 Array.iter2 (conv_binder env clo0 clo1) 89 multibinder0.binders multibinder1.binders; 90 91 (env, clo0, clo1) 92 93 and conv_multibinder 94 : V.environment -> V.environment -> V.environment 95 -> I.multibinder -> I.multibinder -> unit 96 = fun env clo0 clo1 multibinder0 multibinder1 -> 97 ignore @@ bind_and_conv_multibinder env clo0 clo1 multibinder0 multibinder1 98 99 and conv_abstraction 100 : V.environment -> V.environment -> V.environment 101 -> I.abstraction -> I.abstraction -> unit 102 = fun env clo0 clo1 abs0 abs1 -> 103 let (env, clo0, clo1) = bind_and_conv_multibinder env clo0 clo1 104 abs0.multibinder abs1.multibinder in 105 conv env clo0 clo1 abs0.term abs1.term 106 107 and conv_patt 108 : V.environment -> V.environment -> V.environment -> I.patt -> I.patt -> unit 109 = fun env clo0 clo1 patt0 patt1 -> 110 conv_disc env clo0 clo1 patt0.disc patt1.disc 111 112 and conv_disc 113 : V.environment -> V.environment -> V.environment 114 -> I.discriminant -> I.discriminant -> unit 115 = fun env clo0 clo1 disc0 disc1 -> match disc0, disc1 with 116 | I.DWild typ0, I.DWild typ1 -> 117 conv env clo0 clo1 typ0 typ1 118 | I.DData data0, I.DData data1 -> 119 conv_datatype env clo0 clo1 data0.datatype data1.datatype; 120 begin if data0.tagi <> data1.tagi then 121 raise UnifyFail 122 end; 123 Array.iter2 (conv_patt env clo0 clo1) data0.subpatts data1.subpatts 124 | I.DWild _, I.DData _ -> raise UnifyFail 125 | I.DData _, I.DWild _ -> raise UnifyFail 126 127 and conv_datatype 128 : V.environment -> V.environment -> V.environment 129 -> I.datatype -> I.datatype -> unit 130 = fun env clo0 clo1 datatype0 datatype1 -> 131 Array.iter2 (conv_multibinder env clo0 clo1) datatype0.ctors datatype1.ctors; 132 if not @@ Name.Tag.Map.equal Int.equal datatype0.names datatype1.names then 133 raise UnifyFail