summaryrefslogtreecommitdiff
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/formula.ml4
-rw-r--r--plugins/firstorder/formula.mli4
-rw-r--r--plugins/firstorder/g_ground.ml47
-rw-r--r--plugins/firstorder/ground.ml32
-rw-r--r--plugins/firstorder/ground.mli4
-rw-r--r--plugins/firstorder/instances.ml18
-rw-r--r--plugins/firstorder/instances.mli4
-rw-r--r--plugins/firstorder/rules.ml4
-rw-r--r--plugins/firstorder/rules.mli4
-rw-r--r--plugins/firstorder/sequent.ml71
-rw-r--r--plugins/firstorder/sequent.mli4
-rw-r--r--plugins/firstorder/unify.ml7
-rw-r--r--plugins/firstorder/unify.mli4
13 files changed, 27 insertions, 140 deletions
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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: formula.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Hipattern
open Names
open Term
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index a831c087..379aaff1 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: formula.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Term
open Names
open Libnames
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 8e68506c..4a38c48d 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,8 +8,6 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: g_ground.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Formula
open Sequent
open Ground
@@ -29,6 +27,7 @@ let ground_depth=ref 3
let _=
let gdopt=
{ optsync=true;
+ optdepr=false;
optname="Firstorder Depth";
optkey=["Firstorder";"Depth"];
optread=(fun ()->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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ground.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Formula
open Sequent
open Rules
@@ -18,32 +16,6 @@ open Tactics
open Tacticals
open Libnames
-(*
-let old_search=ref !Auto.searchtable
-
-(* I use this solution as a means to know whether hints have changed,
-but this prevents the GC from collecting the previous table,
-resulting in some limited space wasting*)
-
-let update_flags ()=
- if not ( !Auto.searchtable == !old_search ) then
- begin
- old_search:=!Auto.searchtable;
- let predref=ref Names.KNpred.empty in
- let f p_a_t =
- match p_a_t.Auto.code with
- Auto.Unfold_nth (ConstRef kn)->
- 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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ground.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
-
val ground_tac: Tacmach.tactic ->
(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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: instances.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
open Formula
open Sequent
open Unify
open Rules
open Util
open Term
-open Rawterm
+open Glob_term
open Tacmach
open Tactics
open Tacticals
@@ -35,11 +33,11 @@ let compare_instance inst1 inst2=
| Phantom(_),Real((m,_),_)-> 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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: instances.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
open Term
open Tacmach
open Names
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index e6d73fb6..23eeb2f6 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: rules.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Util
open Names
open Term
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index a5a6b614..7d1e57f4 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: rules.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Term
open Tacmach
open Names
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index faac286e..f75678c6 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: sequent.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Term
open Util
open Formula
@@ -59,71 +57,10 @@ struct
(priority e1.pat) - (priority e2.pat)
end
-(* [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare
- the immediate subterms of [c1] of [c2] if needed; Cast's,
- application associativity, binders name and Cases annotations are
- not taken into account *)
-
-let rec compare_list f l1 l2=
- match l1,l2 with
- [],[]-> 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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: sequent.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Term
open Util
open Formula
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 4e0ad108..299a0054 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: unify.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
open Util
open Formula
open Tacmach
@@ -91,9 +89,8 @@ let unif t1 t2=
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
+ if isMeta term && destMeta term = i 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
diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli
index 4e0d88d3..06865611 100644
--- a/plugins/firstorder/unify.mli
+++ b/plugins/firstorder/unify.mli
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: unify.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Term
exception UFAIL of constr*constr
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-13 02:08:07 +0000