← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to contrib/firstorder/g_ground.ml4

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
contrib/firstorder/g_ground.ml4
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i camlp4deps: "parsing/grammar.cma"  i*)
 
10
 
 
11
(* $Id: g_ground.ml4 10346 2007-12-05 21:11:19Z aspiwack $ *)
 
12
 
 
13
open Formula
 
14
open Sequent
 
15
open Ground
 
16
open Goptions
 
17
open Tactics
 
18
open Tacticals
 
19
open Tacinterp
 
20
open Term
 
21
open Names
 
22
open Util
 
23
open Libnames
 
24
 
 
25
(* declaring search depth as a global option *)
 
26
 
 
27
let ground_depth=ref 3
 
28
 
 
29
let _=
 
30
  let gdopt=
 
31
    { optsync=true;
 
32
      optname="Firstorder Depth";
 
33
      optkey=SecondaryTable("Firstorder","Depth"); 
 
34
      optread=(fun ()->Some !ground_depth); 
 
35
      optwrite=
 
36
   (function 
 
37
        None->ground_depth:=3
 
38
      | Some i->ground_depth:=(max i 0))}
 
39
  in
 
40
    declare_int_option gdopt
 
41
 
 
42
let congruence_depth=ref 100
 
43
 
 
44
let _=
 
45
  let gdopt=
 
46
    { optsync=true;
 
47
      optname="Congruence Depth";
 
48
      optkey=SecondaryTable("Congruence","Depth"); 
 
49
      optread=(fun ()->Some !congruence_depth); 
 
50
      optwrite=
 
51
   (function 
 
52
        None->congruence_depth:=0
 
53
      | Some i->congruence_depth:=(max i 0))}
 
54
  in
 
55
    declare_int_option gdopt
 
56
 
 
57
let default_solver=(Tacinterp.interp <:tactic<auto with *>>)
 
58
 
 
59
let fail_solver=tclFAIL 0 (Pp.str "GTauto failed")
 
60
                      
 
61
type external_env=
 
62
    Ids of global_reference list
 
63
  | Bases of Auto.hint_db_name list
 
64
  | Void
 
65
 
 
66
let gen_ground_tac flag taco ext gl=
 
67
  let backup= !qflag in
 
68
    try
 
69
      qflag:=flag;
 
70
      let solver= 
 
71
        match taco with 
 
72
            Some tac-> tac
 
73
          | None-> default_solver in
 
74
      let startseq=
 
75
        match ext with
 
76
            Void -> (fun gl -> empty_seq !ground_depth)
 
77
          | Ids l-> create_with_ref_list l !ground_depth
 
78
          | Bases l-> create_with_auto_hints l !ground_depth in
 
79
      let result=ground_tac solver startseq gl in 
 
80
        qflag:=backup;result
 
81
    with e ->qflag:=backup;raise e
 
82
      
 
83
(* special for compatibility with Intuition 
 
84
 
 
85
let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
 
86
 
 
87
let defined_connectives=lazy
 
88
  [[],EvalConstRef (destConst (constant "not"));
 
89
   [],EvalConstRef (destConst (constant "iff"))]
 
90
 
 
91
let normalize_evaluables=
 
92
  onAllClauses
 
93
    (function 
 
94
         None->unfold_in_concl (Lazy.force defined_connectives)
 
95
       | Some id-> 
 
96
           unfold_in_hyp (Lazy.force defined_connectives) 
 
97
           (Tacexpr.InHypType id)) *)
 
98
 
 
99
TACTIC EXTEND firstorder
 
100
    [ "firstorder" tactic_opt(t) "using" ne_reference_list(l) ] -> 
 
101
      [ gen_ground_tac true (Option.map eval_tactic t) (Ids l) ]
 
102
|   [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] -> 
 
103
      [ gen_ground_tac true (Option.map eval_tactic t) (Bases l) ]
 
104
|   [ "firstorder" tactic_opt(t) ] -> 
 
105
      [ gen_ground_tac true (Option.map eval_tactic t) Void ]
 
106
END
 
107
 
 
108
TACTIC EXTEND gintuition
 
109
  [ "gintuition" tactic_opt(t) ] ->
 
110
     [ gen_ground_tac false (Option.map eval_tactic t) Void ]
 
111
END
 
112
 
 
113
 
 
114
let default_declarative_automation gls = 
 
115
  tclORELSE
 
116
    (tclORELSE (Auto.h_trivial [] None) 
 
117
    (Cctac.congruence_tac !congruence_depth []))
 
118
    (gen_ground_tac true 
 
119
       (Some (tclTHEN
 
120
                default_solver
 
121
                (Cctac.congruence_tac !congruence_depth [])))
 
122
       Void) gls
 
123
 
 
124
 
 
125
 
 
126
let () = 
 
127
  Decl_proof_instr.register_automation_tac default_declarative_automation
 
128