aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder/unify.ml
blob: c3726f1a832613acfa3cd51283984a8f8d007f3a (plain)
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
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Util
open Term
open Termops
open Reductionops

exception UFAIL of constr*constr

(*
   RIGID-only Martelli-Montanari style unification for CLOSED terms
   I repeat : t1 and t2 must NOT have ANY free deBruijn
   sigma is kept normal with respect to itself but is lazily applied
   to the equation set. Raises UFAIL with a pair of  terms
*)

let unif t1 t2=
  let bige=Queue.create ()
  and sigma=ref [] in
  let bind i t=
    sigma:=(i,t)::
      (List.map (function (n,tn)->(n,subst_meta [i,t] tn)) !sigma) in
  let rec head_reduce t=
    (* forbids non-sigma-normal meta in head position*)
    match kind_of_term t with
	Meta i->
	  (try
	     head_reduce (List.assoc i !sigma)
	   with Not_found->t)
      | _->t in
    Queue.add (t1,t2) bige;
    try while true do
      let t1,t2=Queue.take bige in
      let nt1=head_reduce (whd_betaiotazeta Evd.empty t1)
      and nt2=head_reduce (whd_betaiotazeta Evd.empty t2) in
	match (kind_of_term nt1),(kind_of_term nt2) with
	    Meta i,Meta j->
	      if i<>j then
		if i<j then bind j nt1
		else bind i nt2
	  | Meta i,_ ->
	      let t=subst_meta !sigma nt2 in
		if Intset.is_empty (free_rels t) &&
		  not (occur_term (mkMeta i) t) then
		    bind i t else raise (UFAIL(nt1,nt2))
	  | _,Meta i ->
	      let t=subst_meta !sigma nt1 in
		if Intset.is_empty (free_rels t) &&
		  not (occur_term (mkMeta i) t) then
		    bind i t else raise (UFAIL(nt1,nt2))
	  | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige
 	  | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige
	  | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))->
	      Queue.add (a,c) bige;Queue.add (pop b,pop d) bige
	  | Case (_,pa,ca,va),Case (_,pb,cb,vb)->
	      Queue.add (pa,pb) bige;
	      Queue.add (ca,cb) bige;
	      let l=Array.length va in
		if l<>(Array.length vb) then
		  raise (UFAIL (nt1,nt2))
		else
		  for i=0 to l-1 do
		    Queue.add (va.(i),vb.(i)) bige
		  done
	  | App(ha,va),App(hb,vb)->
	      Queue.add (ha,hb) bige;
	      let l=Array.length va in
		if l<>(Array.length vb) then
		  raise (UFAIL (nt1,nt2))
		else
		  for i=0 to l-1 do
		    Queue.add (va.(i),vb.(i)) bige
		  done
	  | _->if not (eq_constr nt1 nt2) then raise (UFAIL (nt1,nt2))
    done;
      assert false
	(* this place is unreachable but needed for the sake of typing *)
    with Queue.Empty-> !sigma

let value i t=
  let add x y=
    if x<0 then y else if y<0 then x else x+y in
  let rec vaux term=
    if isMeta term && destMeta term = i then 0 else
      let f v t=add v (vaux t) in
      let vr=fold_constr f (-1) term in
	if vr<0 then -1 else vr+1 in
    vaux t

type instance=
    Real of (int*constr)*int
  | Phantom of constr

let mk_rel_inst t=
  let new_rel=ref 1 in
  let rel_env=ref [] in
  let rec renum_rec d t=
    match kind_of_term t with
	Meta n->
	  (try
	     mkRel (d+(List.assoc n !rel_env))
	   with Not_found->
	     let m= !new_rel in
	       incr new_rel;
	       rel_env:=(n,m) :: !rel_env;
	       mkRel (m+d))
      | _ -> map_constr_with_binders succ renum_rec d t
  in
  let nt=renum_rec 0 t in (!new_rel - 1,nt)

let unif_atoms i dom t1 t2=
  try
    let t=List.assoc i (unif t1 t2) in
      if isMeta t then Some (Phantom dom)
      else Some (Real(mk_rel_inst t,value i t1))
  with
      UFAIL(_,_) ->None
    | Not_found ->Some (Phantom dom)

let renum_metas_from k n t= (* requires n = max (free_rels t) *)
  let l=List.tabulate (fun i->mkMeta (k+i)) n in
    substl l t

let more_general (m1,t1) (m2,t2)=
  let mt1=renum_metas_from 0 m1 t1
  and mt2=renum_metas_from m1 m2 t2 in
    try
      let sigma=unif mt1 mt2 in
      let p (n,t)= n<m1 || isMeta t in
	List.for_all p sigma
    with UFAIL(_,_)->false