1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167

(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(*i camlp4deps: "grammar/grammar.cma"  i*)

open Ltac_plugin
open Formula
open Sequent
open Ground
open Goptions
open Tacmach.New
open Tacticals.New
open Tacinterp
open Libnames
open Stdarg
open Tacarg
open Pcoq.Prim

DECLARE PLUGIN "ground_plugin"

(* declaring search depth as a global option *)

let ground_depth=ref 3

let _=
  let gdopt=
    { optdepr=false;
      optname="Firstorder Depth";
      optkey=["Firstorder";"Depth"];
      optread=(fun ()->Some !ground_depth);
      optwrite=
   (function
        None->ground_depth:=3
      |        Some i->ground_depth:=(max i 0))}
  in
    declare_int_option gdopt

let congruence_depth=ref 100

let _=
  let gdopt=
    { optdepr=false;
      optname="Congruence Depth";
      optkey=["Congruence";"Depth"];
      optread=(fun ()->Some !congruence_depth);
      optwrite=
   (function
        None->congruence_depth:=0
      |        Some i->congruence_depth:=(max i 0))}
  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.tag (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
      set_default_solver
        (Locality.make_section_locality atts.locality)
        (Tacintern.glob_tactic t);
        st
  ]
END

VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY
| [ "Print" "Firstorder" "Solver" ] -> [
    Feedback.msg_info
      (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
  Proofview.tclOR begin
  Proofview.Goal.enter begin fun gl ->
      qflag:=flag;
      let solver=
        match taco with
            Some tac-> tac
          | None-> snd (default_solver ()) in
      let startseq k =
        Proofview.Goal.enter begin fun gl ->
        let seq=empty_seq !ground_depth in
        let seq, sigma = extend_with_ref_list (pf_env gl) (project gl) ids seq in
        let seq, sigma = extend_with_auto_hints (pf_env gl) (project gl) bases seq in
        tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k seq)
        end
      in
      let result=ground_tac solver startseq in
      qflag := backup;
      result
  end
  end
  (fun (e, info) -> qflag := backup; Proofview.tclZERO ~info e)

(* special for compatibility with Intuition

let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str

let defined_connectives=lazy
  [[],EvalConstRef (destConst (constant "not"));
   [],EvalConstRef (destConst (constant "iff"))]

let normalize_evaluables=
  onAllHypsAndConcl
    (function
         None->unfold_in_concl (Lazy.force defined_connectives)
       | Some id->
           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_reference
let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (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) ] -> [
    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) "with" ne_preident_list(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' ]
END

TACTIC EXTEND gintuition
  [ "gintuition" tactic_opt(t) ] ->
     [ gen_ground_tac false (Option.map (tactic_of_value ist) t) [] [] ]
END