aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/decl_expr.mli
blob: d02060fc0a3b381d2997e5c1325f178edc90840b (plain)
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
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id:$ *)

open Names
open Util
open Tacexpr

type 'it statement = 
    {st_label:name;
     st_it:'it}

type thesis_kind =
    Plain
  | For of identifier

type 'this or_thesis =
    This of 'this
  | Thesis of thesis_kind

type side = Lhs | Rhs

type elim_type =
    ET_Case_analysis
  | ET_Induction

type block_type =
    B_proof
  | B_claim
  | B_focus
  | B_elim of elim_type

type ('it,'constr,'tac) cut =
    {cut_stat: 'it;
     cut_by: 'constr list option;
     cut_using: 'tac option}

type ('var,'constr) hyp = 
    Hvar of 'var 
  | Hprop of 'constr statement

type ('constr,'tac) casee = 
    Real of 'constr 
  | Virtual of ('constr statement,'constr,'tac) cut

type ('hyp,'constr,'pat,'tac) bare_proof_instr =
  | Pthen of ('hyp,'constr,'pat,'tac) bare_proof_instr
  | Pthus of ('hyp,'constr,'pat,'tac) bare_proof_instr
  | Phence of ('hyp,'constr,'pat,'tac) bare_proof_instr
  | Pcut of ('constr or_thesis statement,'constr,'tac) cut
  | Prew of side * ('constr statement,'constr,'tac) cut
  | Psuffices of ((('hyp,'constr) hyp list * 'constr or_thesis),'constr,'tac) cut
  | Passume of ('hyp,'constr) hyp list
  | Plet of ('hyp,'constr) hyp list
  | Pgiven of ('hyp,'constr) hyp list
  | Pconsider of 'constr*('hyp,'constr) hyp list
  | Pclaim of 'constr statement
  | Pfocus of 'constr statement
  | Pdefine of identifier * 'hyp list * 'constr
  | Pcast of identifier or_thesis * 'constr
  | Psuppose of ('hyp,'constr) hyp list 
  | Pcase of 'hyp list*'pat*(('hyp,'constr or_thesis) hyp list) 
  | Ptake of 'constr list 
  | Pper of elim_type * ('constr,'tac) casee
  | Pend of block_type
  | Pescape

type emphasis = int

type ('hyp,'constr,'pat,'tac) gen_proof_instr=
    {emph: emphasis;
     instr: ('hyp,'constr,'pat,'tac) bare_proof_instr }


type raw_proof_instr =
    ((identifier*(Topconstr.constr_expr option)) located,
     Topconstr.constr_expr,
     Topconstr.cases_pattern_expr,
     raw_tactic_expr) gen_proof_instr

type glob_proof_instr =
    ((identifier*(Genarg.rawconstr_and_expr option)) located,
     Genarg.rawconstr_and_expr,  
     Topconstr.cases_pattern_expr,
     Tacexpr.glob_tactic_expr) gen_proof_instr

type proof_pattern = 
    {pat_vars: Term.types statement list;
     pat_aliases: (Term.constr*Term.types) statement list;
     pat_constr: Term.constr;
     pat_typ: Term.types;
     pat_pat: Rawterm.cases_pattern;
     pat_expr: Topconstr.cases_pattern_expr}

type proof_instr =
    (Term.constr statement,
     Term.constr, 
     proof_pattern,
     Tacexpr.glob_tactic_expr) gen_proof_instr