aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/formula.ml11
-rw-r--r--plugins/firstorder/formula.mli3
-rw-r--r--plugins/firstorder/g_ground.ml421
-rw-r--r--plugins/firstorder/instances.ml8
-rw-r--r--plugins/firstorder/rules.ml10
5 files changed, 35 insertions, 18 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index ae2d059fa2..2ed436c6bf 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -15,6 +15,7 @@ open Tacmach
open Util
open Declarations
open Globnames
+open Context.Rel.Declaration
let qflag=ref true
@@ -139,8 +140,8 @@ let build_atoms gl metagen side cciterm =
negative:= unsigned :: !negative
end;
let v = ind_hyps 0 i l gl in
- let g i _ (_,_,t) =
- build_rec env polarity (lift i t) in
+ let g i _ decl =
+ build_rec env polarity (lift i (get_type decl)) in
let f l =
List.fold_left_i g (1-(List.length l)) () l in
if polarity && (* we have a constant constructor *)
@@ -150,8 +151,8 @@ let build_atoms gl metagen side cciterm =
| Exists(i,l)->
let var=mkMeta (metagen true) in
let v =(ind_hyps 1 i l gl).(0) in
- let g i _ (_,_,t) =
- build_rec (var::env) polarity (lift i t) in
+ let g i _ decl =
+ build_rec (var::env) polarity (lift i (get_type decl)) in
List.fold_left_i g (2-(List.length l)) () v
| Forall(_,b)->
let var=mkMeta (metagen true) in
@@ -224,7 +225,7 @@ let build_formula side nam typ gl metagen=
| And(_,_,_) -> Rand
| Or(_,_,_) -> Ror
| Exists (i,l) ->
- let (_,_,d)=List.last (ind_hyps 0 i l gl).(0) in
+ let d = get_type (List.last (ind_hyps 0 i l gl).(0)) in
Rexists(m,d,trivial)
| Forall (_,a) -> Rforall
| Arrow (a,b) -> Rarrow in
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 39d99d2e08..0f70d3ea05 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Term
-open Context
open Globnames
val qflag : bool ref
@@ -27,7 +26,7 @@ type counter = bool -> metavariable
val construct_nhyps : pinductive -> Proof_type.goal Tacmach.sigma -> int array
val ind_hyps : int -> pinductive -> constr list ->
- Proof_type.goal Tacmach.sigma -> rel_context array
+ Proof_type.goal Tacmach.sigma -> Context.Rel.t array
type atoms = {positive:constr list;negative:constr list}
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 0415268819..587d10d1cc 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -15,6 +15,10 @@ open Goptions
open Tacticals
open Tacinterp
open Libnames
+open Constrarg
+open Stdarg
+open Pcoq.Prim
+open Pcoq.Tactic
DECLARE PLUGIN "ground_plugin"
@@ -52,8 +56,15 @@ let _=
in
declare_int_option gdopt
+let default_intuition_tac =
+ let tac _ _ = Auto.h_auto None [] None in
+ 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.ghost, entry, [])
+
let (set_default_solver, default_solver, print_default_solver) =
- Tactic_option.declare_tactic_option ~default:(<:tactic<auto with *>>) "Firstorder default solver"
+ Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver"
VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
| [ "Set" "Firstorder" "Solver" tactic(t) ] -> [
@@ -128,17 +139,17 @@ END
TACTIC EXTEND firstorder
[ "firstorder" tactic_opt(t) firstorder_using(l) ] ->
- [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) l []) ]
+ [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) l []) ]
| [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] ->
- [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) [] l) ]
+ [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) [] l) ]
| [ "firstorder" tactic_opt(t) firstorder_using(l)
"with" ne_preident_list(l') ] ->
- [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) l l') ]
+ [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) l l') ]
END
TACTIC EXTEND gintuition
[ "gintuition" tactic_opt(t) ] ->
- [ Proofview.V82.tactic (gen_ground_tac false (Option.map eval_tactic t) [] []) ]
+ [ Proofview.V82.tactic (gen_ground_tac false (Option.map (tactic_of_value ist) t) [] []) ]
END
open Proofview.Notations
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index a717cc91ea..0bc40136c5 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -22,6 +22,8 @@ open Formula
open Sequent
open Names
open Misctypes
+open Sigma.Notations
+open Context.Rel.Declaration
let compare_instance inst1 inst2=
match inst1,inst2 with
@@ -116,8 +118,10 @@ let mk_open_instance id idc gl m t=
let rec aux n avoid env evmap decls =
if Int.equal n 0 then evmap, decls else
let nid=(fresh_id avoid var_id gl) in
- let evmap, (c, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
- let decl = (Name nid,None,c) in
+ let evmap = Sigma.Unsafe.of_evar_map evmap in
+ let Sigma ((c, _), evmap, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
+ let evmap = Sigma.to_evar_map evmap in
+ let decl = LocalAssum (Name nid, c) in
aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in
let evmap, decls = aux m [] env evmap [] in
evmap, decls, revt
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index e676a8a936..c05015c538 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -19,6 +19,7 @@ open Formula
open Sequent
open Globnames
open Locus
+open Context.Named.Declaration
type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
@@ -34,12 +35,13 @@ let wrap n b continue seq gls=
if i<=0 then seq else
match nc with
[]->anomaly (Pp.str "Not the expected number of hyps")
- | ((id,_,typ) as nd)::q->
+ | nd::q->
+ let id = get_id nd in
if occur_var env id (pf_concl gls) ||
List.exists (occur_var_in_decl env id) ctx then
(aux (i-1) q (nd::ctx))
else
- add_formula Hyp (VarRef id) typ (aux (i-1) q (nd::ctx)) gls in
+ add_formula Hyp (VarRef id) (get_type nd) (aux (i-1) q (nd::ctx)) gls in
let seq1=aux n nc [] in
let seq2=if b then
add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in
@@ -210,6 +212,6 @@ let defined_connectives=lazy
let normalize_evaluables=
onAllHypsAndConcl
(function
- None->unfold_in_concl (Lazy.force defined_connectives)
+ None-> Proofview.V82.of_tactic (unfold_in_concl (Lazy.force defined_connectives))
| Some id ->
- unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))
+ Proofview.V82.of_tactic (unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly)))
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 20:30:00 +0000