diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/firstorder/g_ground.ml4 | 54 | ||||
| -rw-r--r-- | plugins/firstorder/sequent.ml | 17 | ||||
| -rw-r--r-- | plugins/firstorder/sequent.mli | 8 |
3 files changed, 54 insertions, 25 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 96c5bcae4f..8302da5c1d 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -58,12 +58,7 @@ let default_solver=(Tacinterp.interp <:tactic<auto with *>>) let fail_solver=tclFAIL 0 (Pp.str "GTauto failed") -type external_env= - Ids of global_reference list - | Bases of Auto.hint_db_name list - | Void - -let gen_ground_tac flag taco ext gl= +let gen_ground_tac flag taco ids bases gl= let backup= !qflag in try qflag:=flag; @@ -71,11 +66,9 @@ let gen_ground_tac flag taco ext gl= match taco with Some tac-> tac | None-> default_solver in - let startseq= - match ext with - Void -> (fun gl -> empty_seq !ground_depth) - | Ids l-> create_with_ref_list l !ground_depth - | Bases l-> create_with_auto_hints l !ground_depth in + let startseq gl= + let seq=empty_seq !ground_depth in + extend_with_auto_hints bases (extend_with_ref_list ids seq gl) gl in let result=ground_tac solver startseq gl in qflag:=backup;result with e ->qflag:=backup;raise e @@ -96,18 +89,45 @@ let normalize_evaluables= unfold_in_hyp (Lazy.force defined_connectives) (Tacexpr.InHypType id)) *) +open Genarg +open Ppconstr +open Printer +let pr_firstorder_using_raw _ _ _ = prlist_with_sep pr_coma pr_reference +let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_coma (pr_or_var (pr_located pr_global)) +let pr_firstorder_using_typed _ _ _ = prlist_with_sep pr_coma 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 + 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) ] -> [ + Flags.if_verbose + Pp.msg_warning (Pp.str "Deprecated syntax; use \",\" as separator"); + a::b::l + ] +| [ ] -> [ [] ] +END + TACTIC EXTEND firstorder - [ "firstorder" tactic_opt(t) "using" ne_reference_list(l) ] -> - [ gen_ground_tac true (Option.map eval_tactic t) (Ids l) ] + [ "firstorder" tactic_opt(t) firstorder_using(l) ] -> + [ gen_ground_tac true (Option.map eval_tactic t) l [] ] | [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] -> - [ gen_ground_tac true (Option.map eval_tactic t) (Bases l) ] + [ gen_ground_tac true (Option.map eval_tactic t) [] l ] +| [ "firstorder" tactic_opt(t) firstorder_using(l) + "with" ne_preident_list(l') ] -> + [ gen_ground_tac true (Option.map eval_tactic t) l l' ] | [ "firstorder" tactic_opt(t) ] -> - [ gen_ground_tac true (Option.map eval_tactic t) Void ] + [ gen_ground_tac true (Option.map eval_tactic t) [] [] ] END TACTIC EXTEND gintuition [ "gintuition" tactic_opt(t) ] -> - [ gen_ground_tac false (Option.map eval_tactic t) Void ] + [ gen_ground_tac false (Option.map eval_tactic t) [] [] ] END @@ -119,7 +139,7 @@ let default_declarative_automation gls = (Some (tclTHEN default_solver (Cctac.congruence_tac !congruence_depth []))) - Void) gls + [] []) gls diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index fd5972fb74..98b178bdee 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -253,17 +253,26 @@ let empty_seq depth= history=History.empty; depth=depth} -let create_with_ref_list l depth gl= +let expand_constructor_hints = + list_map_append (function + | IndRef ind -> + list_tabulate (fun i -> ConstructRef (ind,i+1)) + (Inductiveops.nconstructors ind) + | gr -> + [gr]) + +let extend_with_ref_list l seq gl= + let l = expand_constructor_hints l in let f gr seq= let c=constr_of_global gr in let typ=(pf_type_of gl c) in add_formula Hyp gr typ seq gl in - List.fold_right f l (empty_seq depth) + List.fold_right f l seq open Auto -let create_with_auto_hints l depth gl= - let seqref=ref (empty_seq depth) in +let extend_with_auto_hints l seq gl= + let seqref=ref seq in let f p_a_t = match p_a_t.code with Res_pf (c,_) | Give_exact c diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index 51db9de167..206de27ed7 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -57,10 +57,10 @@ val take_formula : t -> Formula.t * t val empty_seq : int -> t -val create_with_ref_list : global_reference list -> - int -> Proof_type.goal sigma -> t +val extend_with_ref_list : global_reference list -> + t -> Proof_type.goal sigma -> t -val create_with_auto_hints : Auto.hint_db_name list -> - int -> Proof_type.goal sigma -> t +val extend_with_auto_hints : Auto.hint_db_name list -> + t -> Proof_type.goal sigma -> t val print_cmap: global_reference list CM.t -> unit |