-
Notifications
You must be signed in to change notification settings - Fork 1
/
unif.ml
60 lines (47 loc) · 2.5 KB
/
unif.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
(* ========================================================================= *)
(* Unification for first order terms. *)
(* *)
(* Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.) *)
(* ========================================================================= *)
let rec istriv env x t =
match t with
Var y -> y = x or defined env y & istriv env x (apply env y)
| Fn(f,args) -> exists (istriv env x) args & failwith "cyclic";;
(* ------------------------------------------------------------------------- *)
(* Main unification procedure *)
(* ------------------------------------------------------------------------- *)
let rec unify env eqs =
match eqs with
[] -> env
| (Fn(f,fargs),Fn(g,gargs))::oth ->
if f = g & length fargs = length gargs
then unify env (zip fargs gargs @ oth)
else failwith "impossible unification"
| (Var x,t)::oth | (t,Var x)::oth ->
if defined env x then unify env ((apply env x,t)::oth)
else unify (if istriv env x t then env else (x|->t) env) oth;;
(* ------------------------------------------------------------------------- *)
(* Solve to obtain a single instantiation. *)
(* ------------------------------------------------------------------------- *)
let rec solve env =
let env' = mapf (tsubst env) env in
if env' = env then env else solve env';;
(* ------------------------------------------------------------------------- *)
(* Unification reaching a final solved form (often this isn't needed). *)
(* ------------------------------------------------------------------------- *)
let fullunify eqs = solve (unify undefined eqs);;
(* ------------------------------------------------------------------------- *)
(* Examples. *)
(* ------------------------------------------------------------------------- *)
let unify_and_apply eqs =
let i = fullunify eqs in
let apply (t1,t2) = tsubst i t1,tsubst i t2 in
map apply eqs;;
START_INTERACTIVE;;
unify_and_apply [<<|f(x,g(y))|>>,<<|f(f(z),w)|>>];;
unify_and_apply [<<|f(x,y)|>>,<<|f(y,x)|>>];;
(**** unify_and_apply [<<|f(x,g(y))|>>,<<|f(y,x)|>>];; *****)
unify_and_apply [<<|x_0|>>,<<|f(x_1,x_1)|>>;
<<|x_1|>>,<<|f(x_2,x_2)|>>;
<<|x_2|>>,<<|f(x_3,x_3)|>>];;
END_INTERACTIVE;;