aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/formula.ml6
-rw-r--r--plugins/firstorder/g_ground.mlg (renamed from plugins/firstorder/g_ground.ml4)68
-rw-r--r--plugins/firstorder/ground.ml12
-rw-r--r--plugins/firstorder/instances.ml4
-rw-r--r--plugins/firstorder/plugin_base.dune2
-rw-r--r--plugins/firstorder/rules.ml28
-rw-r--r--plugins/firstorder/rules.mli4
-rw-r--r--plugins/firstorder/sequent.ml2
-rw-r--r--plugins/firstorder/unify.ml4
9 files changed, 53 insertions, 77 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index a60a966cec..56b3dc97cf 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -13,7 +13,6 @@ open Names
open Constr
open EConstr
open Vars
-open Termops
open Util
open Declarations
open Globnames
@@ -100,9 +99,8 @@ let kind_of_formula env sigma term =
else
let has_realargs=(n>0) in
let is_trivial=
- let is_constant c =
- Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in
- Array.exists is_constant mip.mind_nf_lc in
+ let is_constant n = Int.equal n 0 in
+ Array.exists is_constant mip.mind_consnrealargs in
if Inductiveops.mis_is_recursive (ind,mib,mip) ||
(has_realargs && not is_trivial)
then
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.mlg
index fdeef5f0ac..ea86a4b514 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.mlg
@@ -8,6 +8,7 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+{
open Ltac_plugin
open Formula
@@ -19,15 +20,20 @@ open Tacticals.New
open Tacinterp
open Stdarg
open Tacarg
+open Attributes
open Pcoq.Prim
+}
+
DECLARE PLUGIN "ground_plugin"
(* declaring search depth as a global option *)
+{
+
let ground_depth=ref 3
-let _=
+let ()=
let gdopt=
{ optdepr=false;
optname="Firstorder Depth";
@@ -41,7 +47,7 @@ let _=
declare_int_option gdopt
-let _=
+let ()=
let congruence_depth=ref 100 in
let gdopt=
{ optdepr=true; (* noop *)
@@ -60,28 +66,28 @@ let default_intuition_tac =
let name = { Tacexpr.mltac_plugin = "ground_plugin"; mltac_tactic = "auto_with"; } in
let entry = { Tacexpr.mltac_name = name; mltac_index = 0 } in
Tacenv.register_ml_tactic name [| tac |];
- Tacexpr.TacML (Loc.tag (entry, []))
+ Tacexpr.TacML (CAst.make (entry, []))
let (set_default_solver, default_solver, print_default_solver) =
Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver"
-VERNAC COMMAND FUNCTIONAL EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
-| [ "Set" "Firstorder" "Solver" tactic(t) ] -> [
- fun ~atts ~st -> let open Vernacinterp in
+}
+
+VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
+| #[ locality; ] [ "Set" "Firstorder" "Solver" tactic(t) ] -> {
set_default_solver
- (Locality.make_section_locality atts.locality)
- (Tacintern.glob_tactic t);
- st
- ]
+ (Locality.make_section_locality locality)
+ (Tacintern.glob_tactic t)
+ }
END
VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY
-| [ "Print" "Firstorder" "Solver" ] -> [
+| [ "Print" "Firstorder" "Solver" ] -> {
Feedback.msg_info
- (Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) ]
+ (Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) }
END
-let fail_solver=tclFAIL 0 (Pp.str "GTauto failed")
+{
let gen_ground_tac flag taco ids bases =
let backup= !qflag in
@@ -123,45 +129,43 @@ let normalize_evaluables=
unfold_in_hyp (Lazy.force defined_connectives)
(Tacexpr.InHypType id)) *)
-open Genarg
open Ppconstr
open Printer
let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_qualid
-let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (pr_or_var (fun x -> pr_global (snd x)))
+let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (Pputils.pr_or_var (fun x -> pr_global (snd x)))
let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global
let warn_deprecated_syntax =
CWarnings.create ~name:"firstorder-deprecated-syntax" ~category:"deprecated"
(fun () -> Pp.strbrk "Deprecated syntax; use \",\" as separator")
+}
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
- GLOB_TYPED AS reference_list
- GLOB_PRINTED BY pr_firstorder_using_glob
-| [ "using" reference(a) ] -> [ [a] ]
-| [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> [ a::l ]
-| [ "using" reference(a) reference(b) reference_list(l) ] -> [
+ TYPED AS reference list
+ PRINTED BY { pr_firstorder_using_typed }
+ RAW_PRINTED BY { pr_firstorder_using_raw }
+ GLOB_PRINTED BY { pr_firstorder_using_glob }
+| [ "using" reference(a) ] -> { [a] }
+| [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> { a::l }
+| [ "using" reference(a) reference(b) reference_list(l) ] -> {
warn_deprecated_syntax ();
a::b::l
- ]
-| [ ] -> [ [] ]
+ }
+| [ ] -> { [] }
END
TACTIC EXTEND firstorder
- [ "firstorder" tactic_opt(t) firstorder_using(l) ] ->
- [ gen_ground_tac true (Option.map (tactic_of_value ist) t) l [] ]
+| [ "firstorder" tactic_opt(t) firstorder_using(l) ] ->
+ { gen_ground_tac true (Option.map (tactic_of_value ist) t) l [] }
| [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] ->
- [ gen_ground_tac true (Option.map (tactic_of_value ist) t) [] l ]
+ { gen_ground_tac true (Option.map (tactic_of_value ist) t) [] l }
| [ "firstorder" tactic_opt(t) firstorder_using(l)
"with" ne_preident_list(l') ] ->
- [ gen_ground_tac true (Option.map (tactic_of_value ist) t) l l' ]
+ { gen_ground_tac true (Option.map (tactic_of_value ist) t) l l' }
END
TACTIC EXTEND gintuition
- [ "gintuition" tactic_opt(t) ] ->
- [ gen_ground_tac false (Option.map (tactic_of_value ist) t) [] [] ]
+| [ "gintuition" tactic_opt(t) ] ->
+ { gen_ground_tac false (Option.map (tactic_of_value ist) t) [] [] }
END
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 516b04ea21..6a80525200 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -18,16 +18,16 @@ open Tacticals.New
open Globnames
let update_flags ()=
- let f acc coe =
- match coe.Classops.coe_value with
- | ConstRef c -> Names.Cpred.add c acc
- | _ -> acc
+ let open TransparentState in
+ let f accu coe = match coe.Classops.coe_value with
+ | ConstRef kn -> { accu with tr_cst = Names.Cpred.remove kn accu.tr_cst }
+ | _ -> accu
in
- let pred = List.fold_left f Names.Cpred.empty (Classops.coercions ()) in
+ let flags = List.fold_left f TransparentState.full (Classops.coercions ()) in
red_flags:=
CClosure.RedFlags.red_add_transparent
CClosure.betaiotazeta
- (Names.Id.Pred.full,Names.Cpred.complement pred)
+ flags
let ground_tac solver startseq =
Proofview.Goal.enter begin fun gl ->
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 286021d68e..1c9ab2e3bd 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -107,7 +107,7 @@ let mk_open_instance env evmap id idc m t =
(* since we know we will get a product,
reduction is not too expensive *)
let (nam,_,_)=destProd evmap (whd_all env evmap typ) in
- match nam with
+ match nam.Context.binder_name with
Name id -> id
| Anonymous -> dummy_bvid in
let revt=substl (List.init m (fun i->mkRel (m-i))) t in
@@ -115,7 +115,7 @@ let mk_open_instance env evmap id idc m t =
if Int.equal n 0 then evmap, decls else
let nid=(fresh_id_in_env avoid var_id env) in
let (evmap, (c, _)) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
- let decl = LocalAssum (Name nid, c) in
+ let decl = LocalAssum (Context.make_annot (Name nid) Sorts.Relevant, c) in
aux (n-1) (Id.Set.add nid avoid) (EConstr.push_rel decl env) evmap (decl::decls) in
let evmap, decls = aux m Id.Set.empty env evmap [] in
(evmap, decls, revt)
diff --git a/plugins/firstorder/plugin_base.dune b/plugins/firstorder/plugin_base.dune
index bcbb99d9fc..d88daa23fc 100644
--- a/plugins/firstorder/plugin_base.dune
+++ b/plugins/firstorder/plugin_base.dune
@@ -1,5 +1,5 @@
(library
(name ground_plugin)
- (public_name coq.plugins.ground)
+ (public_name coq.plugins.firstorder)
(synopsis "Coq's first order logic solver plugin")
(libraries coq.plugins.ltac))
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 8fa676de44..7f06ab6777 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -21,7 +21,6 @@ open Termops
open Formula
open Sequent
open Globnames
-open Locus
module NamedDecl = Context.Named.Declaration
@@ -56,10 +55,6 @@ let wrap n b continue seq =
continue seq2
end
-let basename_of_global=function
- VarRef id->id
- | _->assert false
-
let clear_global=function
VarRef id-> clear [id]
| _->tclIDTAC
@@ -168,9 +163,9 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq =
let ll_arrow_tac a b c backtrack id continue seq=
let open EConstr in
let open Vars in
- let cc=mkProd(Anonymous,a,(lift 1 b)) in
- let d idc = mkLambda (Anonymous,b,
- mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
+ let cc=mkProd(Context.make_annot Anonymous Sorts.Relevant,a,(lift 1 b)) in
+ let d idc = mkLambda (Context.make_annot Anonymous Sorts.Relevant,b,
+ mkApp (idc, [|mkLambda (Context.make_annot Anonymous Sorts.Relevant,(lift 1 a),(mkRel 2))|])) in
tclORELSE
(tclTHENS (cut c)
[tclTHENLIST
@@ -230,20 +225,3 @@ let ll_forall_tac prod backtrack id continue seq=
backtrack
(* rules for instantiation with unification moved to instances.ml *)
-
-(* special for compatibility with old Intuition *)
-
-let constant str = UnivGen.constr_of_global
- @@ Coqlib.lib_ref str
-
-let defined_connectives = lazy
- [AllOccurrences, EvalConstRef (fst (Constr.destConst (constant "core.not.type")));
- AllOccurrences, EvalConstRef (fst (Constr.destConst (constant "core.iff.type")))]
-
-let normalize_evaluables=
- Proofview.Goal.enter begin fun gl ->
- unfold_in_concl (Lazy.force defined_connectives) <*>
- tclMAP
- (fun id -> unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))
- (pf_ids_of_hyps gl)
- end
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index 924c26790c..97bc992b26 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -22,8 +22,6 @@ type 'a with_backtracking = tactic -> 'a
val wrap : int -> bool -> seqtac
-val basename_of_global: GlobRef.t -> Id.t
-
val clear_global: GlobRef.t -> tactic
val axiom_tac : constr -> Sequent.t -> tactic
@@ -51,5 +49,3 @@ val forall_tac : seqtac with_backtracking
val left_exists_tac : pinductive -> lseqtac with_backtracking
val ll_forall_tac : types -> lseqtac with_backtracking
-
-val normalize_evaluables : tactic
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 5958fe8203..01b18e2f30 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -235,7 +235,7 @@ let print_cmap map=
str "| " ++
prlist Printer.pr_global l ++
str " : " ++
- Ppconstr.pr_constr_expr xc ++
+ Ppconstr.pr_constr_expr env sigma xc ++
cut () ++
s in
(v 0
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index d63fe9d799..0c958ddee3 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -65,13 +65,13 @@ let unif evd t1 t2=
bind i t else raise (UFAIL(nt1,nt2))
| 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))->
+ | (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 not (Int.equal l (Array.length vb)) then
+ if not (Int.equal l (Array.length vb)) then
raise (UFAIL (nt1,nt2))
else
for i=0 to l-1 do
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 06:55:47 +0000