1 files changed, 143 insertions, 0 deletions
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
new file mode 100644
index 00000000..e3a4c6a5
--- /dev/null
+++ b/plugins/firstorder/unify.ml
@@ -0,0 +1,143 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+open Util
+open Formula
+open Tacmach
+open Term
+open Names
+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 tref=mkMeta i in
+  let rec vaux term=
+    if term=tref 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