diff options
Diffstat (limited to 'plugins/firstorder/unify.ml')
| -rw-r--r-- | plugins/firstorder/unify.ml | 66 |
1 files changed, 37 insertions, 29 deletions
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index d9ab36ad..b869c04a 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -1,13 +1,16 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util open Term +open EConstr open Vars open Termops open Reductionops @@ -21,7 +24,12 @@ exception UFAIL of constr*constr to the equation set. Raises UFAIL with a pair of terms *) -let unif t1 t2= +let pop t = Vars.lift (-1) t +let subst_meta subst t = + let subst = List.map (fun (m, c) -> (m, EConstr.Unsafe.to_constr c)) subst in + EConstr.of_constr (subst_meta subst (EConstr.Unsafe.to_constr t)) + +let unif evd t1 t2= let bige=Queue.create () and sigma=ref [] in let bind i t= @@ -29,7 +37,7 @@ let unif t1 t2= (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 + match EConstr.kind evd t with Meta i-> (try head_reduce (Int.List.assoc i !sigma) @@ -38,25 +46,25 @@ let unif t1 t2= 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 + let nt1=head_reduce (whd_betaiotazeta evd t1) + and nt2=head_reduce (whd_betaiotazeta evd t2) in + match (EConstr.kind evd nt1),(EConstr.kind evd nt2) with Meta i,Meta j-> if not (Int.equal i j) then if i<j then bind j nt1 else bind i nt2 | Meta i,_ -> let t=subst_meta !sigma nt2 in - if Int.Set.is_empty (free_rels t) && - not (occur_term (mkMeta i) t) then + if Int.Set.is_empty (free_rels evd t) && + not (dependent evd (EConstr.mkMeta i) t) then bind i t else raise (UFAIL(nt1,nt2)) | _,Meta i -> let t=subst_meta !sigma nt1 in - if Int.Set.is_empty (free_rels t) && - not (occur_term (mkMeta i) t) then + if Int.Set.is_empty (free_rels evd t) && + not (dependent evd (EConstr.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 (strip_outer_cast evd nt1,nt2) bige + | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast evd 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)-> @@ -78,19 +86,19 @@ let unif t1 t2= for i=0 to l-1 do Queue.add (va.(i),vb.(i)) bige done - | _->if not (eq_constr_nounivs nt1 nt2) then raise (UFAIL (nt1,nt2)) + | _->if not (eq_constr_nounivs evd 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 value evd 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 && Int.equal (destMeta term) i then 0 else + if isMeta evd term && Int.equal (destMeta evd term) i then 0 else let f v t=add v (vaux t) in - let vr=fold_constr f (-1) term in + let vr=EConstr.fold evd f (-1) term in if vr<0 then -1 else vr+1 in vaux t @@ -98,11 +106,11 @@ type instance= Real of (int*constr)*int | Phantom of constr -let mk_rel_inst t= +let mk_rel_inst evd 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 EConstr.kind evd t with Meta n-> (try mkRel (d+(Int.List.assoc n !rel_env)) @@ -111,15 +119,15 @@ let mk_rel_inst t= incr new_rel; rel_env:=(n,m) :: !rel_env; mkRel (m+d)) - | _ -> map_constr_with_binders succ renum_rec d t + | _ -> EConstr.map_with_binders evd succ renum_rec d t in let nt=renum_rec 0 t in (!new_rel - 1,nt) -let unif_atoms i dom t1 t2= +let unif_atoms evd i dom t1 t2= try - let t=Int.List.assoc i (unif t1 t2) in - if isMeta t then Some (Phantom dom) - else Some (Real(mk_rel_inst t,value i t1)) + let t=Int.List.assoc i (unif evd t1 t2) in + if isMeta evd t then Some (Phantom dom) + else Some (Real(mk_rel_inst evd t,value evd i t1)) with UFAIL(_,_) ->None | Not_found ->Some (Phantom dom) @@ -128,11 +136,11 @@ let renum_metas_from k n t= (* requires n = max (free_rels t) *) let l=List.init n (fun i->mkMeta (k+i)) in substl l t -let more_general (m1,t1) (m2,t2)= +let more_general evd (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 + let sigma=unif evd mt1 mt2 in + let p (n,t)= n<m1 || isMeta evd t in List.for_all p sigma with UFAIL(_,_)->false |