From 0f4f723a5608075ff4aa48290314df30843efbcb Mon Sep 17 00:00:00 2001
From: corbinea
Date: Wed, 20 Sep 2006 17:18:18 +0000
Subject: Declarative Proof Language: main commit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/decl_expr.mli | 108 +++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 108 insertions(+)
 create mode 100644 proofs/decl_expr.mli

(limited to 'proofs/decl_expr.mli')

diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli
new file mode 100644
index 0000000000..24af3842cb
--- /dev/null
+++ b/proofs/decl_expr.mli
@@ -0,0 +1,108 @@
+(************************************************************************)
+(*  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 ('constr,'tac) justification =
+  By_tactic of 'tac
+| Automated of 'constr list
+
+type 'it statement = 
+    {st_label:name;
+     st_it:'it}
+
+type thesis_kind =
+    Plain
+  | Sub of int
+  | 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 statement;
+     cut_by: ('constr,'tac) justification}
+
+type ('var,'constr) hyp = 
+    Hvar of 'var 
+  | Hprop of 'constr statement
+
+type ('constr,'tac) casee = 
+    Real of 'constr 
+  | Virtual of ('constr,'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,'constr,'tac) cut
+  | Prew of side * ('constr,'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
-- 
cgit v1.2.3