← Back to branch summary

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

« back to all changes in this revision

Viewing changes to proofs/decl_mode.ml

  • 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:
proofs/decl_mode.ml
 
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 $Id: decl_mode.ml 10739 2008-04-01 14:45:20Z herbelin $ i*)
 
10
 
 
11
open Names
 
12
open Term
 
13
open Evd
 
14
open Util
 
15
 
 
16
let daimon_flag = ref false
 
17
 
 
18
let set_daimon_flag () = daimon_flag:=true 
 
19
let clear_daimon_flag () = daimon_flag:=false
 
20
let get_daimon_flag () = !daimon_flag 
 
21
 
 
22
type command_mode =
 
23
    Mode_tactic
 
24
  | Mode_proof
 
25
  | Mode_none
 
26
 
 
27
let mode_of_pftreestate pts =
 
28
  let goal = sig_it (Refiner.top_goal_of_pftreestate pts) in
 
29
    if goal.evar_extra = None then
 
30
      Mode_tactic 
 
31
    else
 
32
      Mode_proof
 
33
          
 
34
let get_current_mode () =
 
35
  try 
 
36
    mode_of_pftreestate (Pfedit.get_pftreestate ())
 
37
  with _ -> Mode_none
 
38
 
 
39
let check_not_proof_mode str =
 
40
 if get_current_mode () = Mode_proof then
 
41
   error str
 
42
 
 
43
type split_tree=
 
44
    Skip_patt of Idset.t * split_tree
 
45
  | Split_patt of Idset.t * inductive * 
 
46
                (bool array * (Idset.t * split_tree) option) array
 
47
  | Close_patt of split_tree
 
48
  | End_patt of (identifier * int)
 
49
 
 
50
type elim_kind =
 
51
    EK_dep of split_tree
 
52
  | EK_nodep
 
53
  | EK_unknown
 
54
 
 
55
type recpath = int option*Declarations.wf_paths
 
56
 
 
57
type per_info = 
 
58
    {per_casee:constr;
 
59
     per_ctype:types;
 
60
     per_ind:inductive;
 
61
     per_pred:constr;
 
62
     per_args:constr list;
 
63
     per_params:constr list;
 
64
     per_nparams:int;
 
65
     per_wf:recpath}
 
66
 
 
67
type stack_info = 
 
68
    Per of Decl_expr.elim_type * per_info * elim_kind * identifier list
 
69
  | Suppose_case
 
70
  | Claim
 
71
  | Focus_claim
 
72
 
 
73
type pm_info =
 
74
    { pm_stack : stack_info list}
 
75
 
 
76
let pm_in,pm_out = Dyn.create "pm_info" 
 
77
 
 
78
let get_info gl=
 
79
  match gl.evar_extra with
 
80
      None ->  invalid_arg "get_info"
 
81
    | Some extra ->
 
82
        try pm_out extra with _ -> invalid_arg "get_info"
 
83
 
 
84
let get_stack pts = 
 
85
  let info = get_info (sig_it (Refiner.nth_goal_of_pftreestate 1 pts)) in
 
86
    info.pm_stack
 
87
 
 
88
let get_top_stack pts = 
 
89
  let info = get_info (sig_it (Refiner.top_goal_of_pftreestate pts)) in
 
90
    info.pm_stack
 
91
 
 
92
let get_end_command pts =
 
93
  match mode_of_pftreestate pts with 
 
94
      Mode_proof ->
 
95
        Some 
 
96
          begin
 
97
            match get_top_stack pts with
 
98
                [] -> "\"end proof\""
 
99
              | Claim::_ -> "\"end claim\""
 
100
              | Focus_claim::_-> "\"end focus\""
 
101
              | (Suppose_case :: Per (et,_,_,_) :: _ 
 
102
                | Per (et,_,_,_) :: _ ) -> 
 
103
                  begin
 
104
                    match et with
 
105
                        Decl_expr.ET_Case_analysis -> 
 
106
                          "\"end cases\" or start a new case"
 
107
                      | Decl_expr.ET_Induction -> 
 
108
                          "\"end induction\" or start a new case"
 
109
                  end
 
110
              | _ -> anomaly "lonely suppose"
 
111
          end
 
112
    | Mode_tactic ->
 
113
        begin
 
114
          try
 
115
            ignore 
 
116
              (Refiner.up_until_matching_rule Proof_trees.is_proof_instr pts);
 
117
            Some "\"return\""
 
118
          with Not_found -> None
 
119
        end
 
120
    | Mode_none ->
 
121
        error "no proof in progress"
 
122
 
 
123
let get_last env =  
 
124
  try 
 
125
    let (id,_,_) =  List.hd (Environ.named_context env) in id
 
126
  with Invalid_argument _ -> error "no previous statement to use"