From 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 Mon Sep 17 00:00:00 2001 From: glondu Date: Thu, 17 Sep 2009 15:58:14 +0000 Subject: Delete trailing whitespaces in all *.{v,ml*} files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/firstorder/unify.ml | 72 ++++++++++++++++++++++----------------------- 1 file changed, 36 insertions(+), 36 deletions(-) (limited to 'plugins/firstorder/unify.ml') diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 782129e5c..e3a4c6a55 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -9,7 +9,7 @@ (*i $Id$ i*) open Util -open Formula +open Formula open Tacmach open Term open Names @@ -18,73 +18,73 @@ 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 +(* + 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 () +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= + 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) + (try + head_reduce (List.assoc i !sigma) with Not_found->t) - | _->t in + | _->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) + 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 + Meta i,Meta j-> + if i<>j then if i let t=subst_meta !sigma nt2 in - if Intset.is_empty (free_rels t) && + if Intset.is_empty (free_rels t) && not (occur_term (mkMeta i) t) then bind i t else raise (UFAIL(nt1,nt2)) - | _,Meta i -> + | _,Meta i -> let t=subst_meta !sigma nt1 in - if Intset.is_empty (free_rels t) && + 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 + | _,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 + if l<>(Array.length vb) then raise (UFAIL (nt1,nt2)) - else + else for i=0 to l-1 do Queue.add (va.(i),vb.(i)) bige - done + done | App(ha,va),App(hb,vb)-> Queue.add (ha,hb) bige; let l=Array.length va in - if l<>(Array.length vb) then + if l<>(Array.length vb) then raise (UFAIL (nt1,nt2)) - else + 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 + assert false (* this place is unreachable but needed for the sake of typing *) with Queue.Empty-> !sigma @@ -93,23 +93,23 @@ let value i t= 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 + 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 + 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 + match kind_of_term t with Meta n-> - (try + (try mkRel (d+(List.assoc n !rel_env)) with Not_found-> let m= !new_rel in @@ -117,18 +117,18 @@ let mk_rel_inst t= rel_env:=(n,m) :: !rel_env; mkRel (m+d)) | _ -> map_constr_with_binders succ renum_rec d t - in + 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 + 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 @@ -136,7 +136,7 @@ let renum_metas_from k n t= (* requires n = max (free_rels 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 + try let sigma=unif mt1 mt2 in let p (n,t)= n