From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- plugins/firstorder/formula.ml | 4 +-- plugins/firstorder/formula.mli | 4 +-- plugins/firstorder/g_ground.ml4 | 7 ++-- plugins/firstorder/ground.ml | 32 ++---------------- plugins/firstorder/ground.mli | 4 +-- plugins/firstorder/instances.ml | 18 +++++----- plugins/firstorder/instances.mli | 4 +-- plugins/firstorder/rules.ml | 4 +-- plugins/firstorder/rules.mli | 4 +-- plugins/firstorder/sequent.ml | 71 +++------------------------------------- plugins/firstorder/sequent.mli | 4 +-- plugins/firstorder/unify.ml | 7 ++-- plugins/firstorder/unify.mli | 4 +-- 13 files changed, 27 insertions(+), 140 deletions(-) (limited to 'plugins/firstorder') diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 1f3fd595..d67dceea 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Some !ground_depth); @@ -44,6 +43,7 @@ let congruence_depth=ref 100 let _= let gdopt= { optsync=true; + optdepr=false; optname="Congruence Depth"; optkey=["Congruence";"Depth"]; optread=(fun ()->Some !congruence_depth); @@ -111,7 +111,6 @@ let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_comma (pr_or_var (pr_loc let pr_firstorder_using_typed _ _ _ = prlist_with_sep pr_comma pr_global ARGUMENT EXTEND firstorder_using - TYPED AS reference_list PRINTED BY pr_firstorder_using_typed RAW_TYPED AS reference_list RAW_PRINTED BY pr_firstorder_using_raw diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 163b9891..46708053 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* - predref:=Names.KNpred.add kn !predref - | _ ->() in - let g _ l=List.iter f l in - let h _ hdb=Auto.Hint_db.iter g hdb in - Util.Stringmap.iter h !Auto.searchtable; - red_flags:= - Closure.RedFlags.red_add_transparent - Closure.betaiotazeta (Names.Idpred.full,!predref) - end -*) - let update_flags ()= let predref=ref Names.Cpred.empty in let f coe= @@ -61,7 +33,7 @@ let ground_tac solver startseq gl= update_flags (); let rec toptac skipped seq gl= if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 - then Pp.msgnl (Printer.pr_goal (sig_it gl)); + then Pp.msgnl (Printer.pr_goal gl); tclORELSE (axiom_tac seq.gl seq) begin try diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli index 8328bb3a..a4ee68fd 100644 --- a/plugins/firstorder/ground.mli +++ b/plugins/firstorder/ground.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* (Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 4802aaa3..16831d3e 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -1,20 +1,18 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* if m=0 then -1 else 1 | Real((m,_),_),Phantom(_)-> if m=0 then 1 else -1 -let compare_gr id1 id2= +let compare_gr id1 id2 = if id1==id2 then 0 else if id1==dummy_id then 1 else if id2==dummy_id then -1 - else Pervasives.compare id1 id2 + else Libnames.RefOrdered.compare id1 id2 module OrderedInstance= struct @@ -125,9 +123,9 @@ let mk_open_instance id gl m t= let rec raux n t= if n=0 then t else match t with - RLambda(loc,name,k,_,t0)-> + GLambda(loc,name,k,_,t0)-> let t1=raux (n-1) t0 in - RLambda(loc,name,k,RHole (dummy_loc,Evd.BinderType name),t1) + GLambda(loc,name,k,GHole (dummy_loc,Evd.BinderType name),t1) | _-> anomaly "can't happen" in let ntt=try Pretyping.Default.understand evmap env (raux m rawt) @@ -181,12 +179,12 @@ let right_instance_tac inst continue seq= [tclTHENLIST [introf; (fun gls-> - split (Rawterm.ImplicitBindings + split (Glob_term.ImplicitBindings [mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls); tclSOLVE [wrap 0 true continue (deepen seq)]]; tclTRY assumption] | Real ((0,t),_) -> - (tclTHEN (split (Rawterm.ImplicitBindings [t])) + (tclTHEN (split (Glob_term.ImplicitBindings [t])) (tclSOLVE [wrap 0 true continue (deepen seq)])) | Real ((m,t),_) -> tclFAIL 0 (Pp.str "not implemented ... yet") diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli index 537e40e7..be69b067 100644 --- a/plugins/firstorder/instances.mli +++ b/plugins/firstorder/instances.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* 0 - | [],_ -> -1 - | _,[] -> 1 - | (h1::q1),(h2::q2) -> (f =? (compare_list f)) h1 h2 q1 q2 - -let compare_array f v1 v2= - let l=Array.length v1 in - let c=l - Array.length v2 in - if c=0 then - let rec comp_aux i= - if i<0 then 0 - else - let ci=f v1.(i) v2.(i) in - if ci=0 then - comp_aux (i-1) - else ci - in comp_aux (l-1) - else c - -let compare_constr_int f t1 t2 = - match kind_of_term t1, kind_of_term t2 with - | Rel n1, Rel n2 -> n1 - n2 - | Meta m1, Meta m2 -> m1 - m2 - | Var id1, Var id2 -> Pervasives.compare id1 id2 - | Sort s1, Sort s2 -> Pervasives.compare s1 s2 - | Cast (c1,_,_), _ -> f c1 t2 - | _, Cast (c2,_,_) -> f t1 c2 - | Prod (_,t1,c1), Prod (_,t2,c2) - | Lambda (_,t1,c1), Lambda (_,t2,c2) -> - (f =? f) t1 t2 c1 c2 - | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> - ((f =? f) ==? f) b1 b2 t1 t2 c1 c2 - | App (_,_), App (_,_) -> - let c1,l1=decompose_app t1 - and c2,l2=decompose_app t2 in - (f =? (compare_list f)) c1 c2 l1 l2 - | Evar (e1,l1), Evar (e2,l2) -> - ((-) =? (compare_array f)) e1 e2 l1 l2 - | Const c1, Const c2 -> Pervasives.compare c1 c2 - | Ind c1, Ind c2 -> Pervasives.compare c1 c2 - | Construct c1, Construct c2 -> Pervasives.compare c1 c2 - | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> - ((f =? f) ==? (compare_array f)) p1 p2 c1 c2 bl1 bl2 - | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) -> - ((Pervasives.compare =? (compare_array f)) ==? (compare_array f)) - ln1 ln2 tl1 tl2 bl1 bl2 - | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> - ((Pervasives.compare =? (compare_array f)) ==? (compare_array f)) - ln1 ln2 tl1 tl2 bl1 bl2 - | _ -> Pervasives.compare t1 t2 - -let rec compare_constr m n= - compare_constr_int compare_constr m n - module OrderedConstr= struct type t=constr - let compare=compare_constr + let compare=constr_ord end type h_item = global_reference * (int*constr) option @@ -132,7 +69,7 @@ module Hitem= struct type t = h_item let compare (id1,co1) (id2,co2)= - (Pervasives.compare + (Libnames.RefOrdered.compare =? (fun oc1 oc2 -> match oc1,oc2 with Some (m1,c1),Some (m2,c2) -> @@ -283,7 +220,7 @@ let extend_with_auto_hints l seq gl= seqref:=add_formula Hint gr typ !seqref gl with Not_found->()) | _-> () in - let g _ l=List.iter f l in + let g _ l = List.iter f l in let h dbname= let hdb= try diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index ef052605..c5c2bb95 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*