From 7d220f8b61649646692983872626d6a8042446a9 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 20 Mar 2009 01:22:58 +0000
Subject: Directory 'contrib' renamed into 'plugins', to end confusion with
 archive of user contribs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/firstorder/unify.ml | 143 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 143 insertions(+)
 create mode 100644 plugins/firstorder/unify.ml

(limited to 'plugins/firstorder/unify.ml')

diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
new file mode 100644
index 000000000..782129e5c
--- /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
-- 
cgit v1.2.3