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