1(* ========================================================================= *)
2(* MATCHING AND UNIFICATION                                                  *)
3(* Copyright (c) 2001-2004 Joe Hurd.                                         *)
4(* ========================================================================= *)
5
6(*
7app load ["mlibUseful", "Mosml", "mlibTerm"];
8*)
9
10(*
11*)
12structure mlibMatch :> mlibMatch =
13struct
14
15open mlibUseful mlibTerm;
16
17infixr |-> ::>;
18
19type subst        = mlibSubst.subst;
20val |<>|          = mlibSubst.|<>|;
21val op ::>        = mlibSubst.::>;
22val term_subst    = mlibSubst.term_subst;
23val formula_subst = mlibSubst.formula_subst;
24
25(* ------------------------------------------------------------------------- *)
26(* mlibMatching.                                                                 *)
27(* ------------------------------------------------------------------------- *)
28
29fun raw_match env x tm =
30  (case mlibSubst.find_redex x env of NONE => (x |-> tm) ::> env
31   | SOME tm' =>
32     if tm = tm' then env
33     else raise Error "match: one var trying to match two different terms");
34
35fun matchl env [] = env
36  | matchl env ((Var x, tm) :: rest) = matchl (raw_match env x tm) rest
37  | matchl env ((Fn (f, args), Fn (f', args')) :: rest) =
38  if f = f' andalso length args = length args' then
39    matchl env (zip args args' @ rest)
40  else raise Error "match: can't match two different functions"
41  | matchl _ _ = raise Error "match: different structure";
42
43fun match tm tm' = mlibSubst.norm (matchl |<>| [(tm, tm')]);
44
45local
46  fun conv (Atom t, Atom t') = SOME (t, t')
47    | conv (Not p,  Not q)   = conv (p, q)
48    | conv (True,   True)    = NONE
49    | conv (False,  False)   = NONE
50    | conv _                 = raise Error "match_literals: incompatible";
51in
52  fun matchl_literals sub = matchl sub o List.mapPartial conv;
53end;
54
55fun match_literals lit lit' = mlibSubst.norm (matchl_literals |<>| [(lit, lit')]);
56
57(* ------------------------------------------------------------------------- *)
58(* Unification.                                                              *)
59(* ------------------------------------------------------------------------- *)
60
61local
62  fun occurs v tm = mem v (FVT tm);
63
64  fun solve env [] = env
65    | solve env ((tm1, tm2) :: rest) =
66    solve' env (term_subst env tm1) (term_subst env tm2) rest
67  and solve' env (Var x) tm rest =
68    if Var x = tm then solve env rest
69    else if occurs x tm then raise Error "unify: occurs check"
70    else
71      (case mlibSubst.find_redex x env of NONE
72         => solve (mlibSubst.refine env ((x |-> tm) ::> |<>|)) rest
73       | SOME tm' => solve' env tm' tm rest)
74    | solve' env tm (tm' as Var _) rest = solve' env tm' tm rest
75    | solve' env (Fn (f, args)) (Fn (f', args')) rest =
76    if f = f' andalso length args = length args' then
77      solve env (zip args args' @ rest)
78    else raise Error "unify: different structure";
79in
80  val unifyl = solve;
81end;
82
83fun unify env tm tm' = unifyl env [(tm, tm')];
84
85fun unify_and_apply tm tm' = term_subst (unify |<>| tm tm') tm;
86
87local
88  fun conv (Atom t, Atom t') = SOME (t, t')
89    | conv (Not p,  Not q)   = conv (p, q)
90    | conv (True,   True)    = NONE
91    | conv (False,  False)   = NONE
92    | conv _                 = raise Error "unify_literals: incompatible";
93in
94  fun unifyl_literals env = unifyl env o List.mapPartial conv;
95end;
96
97fun unify_literals env lit lit' = unifyl_literals env [(lit, lit')];
98
99end
100