← Back to branch summary

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

« back to all changes in this revision

Viewing changes to contrib/subtac/subtac.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:
contrib/subtac/subtac.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
(* $Id: subtac.ml 12194 2009-06-17 16:38:09Z msozeau $ *)
 
10
 
 
11
open Global
 
12
open Pp
 
13
open Util
 
14
open Names
 
15
open Sign
 
16
open Evd
 
17
open Term
 
18
open Termops
 
19
open Reductionops
 
20
open Environ
 
21
open Type_errors
 
22
open Typeops
 
23
open Libnames
 
24
open Classops
 
25
open List
 
26
open Recordops 
 
27
open Evarutil
 
28
open Pretype_errors
 
29
open Rawterm
 
30
open Evarconv
 
31
open Pattern
 
32
open Dyn
 
33
open Vernacexpr
 
34
 
 
35
open Subtac_coercion
 
36
open Subtac_utils
 
37
open Coqlib
 
38
open Printer
 
39
open Subtac_errors
 
40
open Eterm
 
41
 
 
42
let require_library dirpath =
 
43
  let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in
 
44
    Library.require_library [qualid] None
 
45
 
 
46
open Pp
 
47
open Ppconstr
 
48
open Decl_kinds
 
49
open Tacinterp
 
50
open Tacexpr
 
51
 
 
52
let solve_tccs_in_type env id isevars evm c typ =
 
53
  if not (evm = Evd.empty) then 
 
54
    let stmt_id = Nameops.add_suffix id "_stmt" in
 
55
    let obls, c', t' = eterm_obligations env stmt_id !isevars evm 0 ~status:Expand c typ in
 
56
      match Subtac_obligations.add_definition stmt_id c' typ obls with
 
57
      Subtac_obligations.Defined cst -> constant_value (Global.env()) 
 
58
        (match cst with ConstRef kn -> kn | _ -> assert false)
 
59
      | _ -> 
 
60
          errorlabstrm "start_proof" 
 
61
            (str "The statement obligations could not be resolved automatically, " ++ spc () ++
 
62
                str "write a statement definition first.")
 
63
  else
 
64
    let _ = Typeops.infer_type env c in c
 
65
 
 
66
 
 
67
let start_proof_com env isevars sopt kind (bl,t) hook =
 
68
  let id = match sopt with
 
69
    | Some (loc,id) ->
 
70
        (* We check existence here: it's a bit late at Qed time *)
 
71
        if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
 
72
          user_err_loc (loc,"start_proof",pr_id id ++ str " already exists");
 
73
        id
 
74
    | None ->
 
75
        next_global_ident_away false (id_of_string "Unnamed_thm")
 
76
          (Pfedit.get_all_proof_names ())
 
77
  in
 
78
  let evm, c, typ, _imps = 
 
79
    Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr t bl) None 
 
80
  in
 
81
  let c = solve_tccs_in_type env id isevars evm c typ in
 
82
    Command.start_proof id kind c hook  
 
83
      
 
84
let print_subgoals () = Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
 
85
 
 
86
let start_proof_and_print env isevars idopt k t hook =
 
87
  start_proof_com env isevars idopt k t hook;
 
88
  print_subgoals ()
 
89
          
 
90
let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n)))
 
91
  
 
92
let assumption_message id =
 
93
  Flags.if_verbose message ((string_of_id id) ^ " is assumed")
 
94
 
 
95
let declare_assumption env isevars idl is_coe k bl c nl =
 
96
  if not (Pfedit.refining ()) then
 
97
    let id = snd (List.hd idl) in
 
98
    let evm, c, typ, imps = 
 
99
      Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr c bl) None 
 
100
    in
 
101
    let c = solve_tccs_in_type env id isevars evm c typ in
 
102
      List.iter (Command.declare_one_assumption is_coe k c imps false [] nl) idl
 
103
  else
 
104
    errorlabstrm "Command.Assumption"
 
105
        (str "Cannot declare an assumption while in proof editing mode.")
 
106
 
 
107
let dump_constraint ty ((loc, n), _, _) =
 
108
  match n with
 
109
    | Name id -> Dumpglob.dump_definition (loc, id) false ty
 
110
    | Anonymous -> ()
 
111
 
 
112
let dump_variable lid = ()
 
113
 
 
114
let vernac_assumption env isevars kind l nl =
 
115
  let global = fst kind = Global in
 
116
    List.iter (fun (is_coe,(idl,c)) -> 
 
117
      if Dumpglob.dump () then
 
118
        List.iter (fun lid -> 
 
119
          if global then Dumpglob.dump_definition lid (not global) "ax"
 
120
          else dump_variable lid) idl;
 
121
      declare_assumption env isevars idl is_coe kind [] c nl) l
 
122
 
 
123
let check_fresh (loc,id) =
 
124
  if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
 
125
    user_err_loc (loc,"",pr_id id ++ str " already exists")
 
126
      
 
127
let subtac (loc, command) =
 
128
  check_required_library ["Coq";"Init";"Datatypes"];
 
129
  check_required_library ["Coq";"Init";"Specif"];
 
130
  let env = Global.env () in
 
131
  let isevars = ref (create_evar_defs Evd.empty) in
 
132
  try
 
133
  match command with
 
134
  | VernacDefinition (defkind, (_, id as lid), expr, hook) -> 
 
135
      check_fresh lid;
 
136
      Dumpglob.dump_definition lid false "def";
 
137
      (match expr with
 
138
      | ProveBody (bl, t) -> 
 
139
          if Lib.is_modtype () then
 
140
            errorlabstrm "Subtac_command.StartProof"
 
141
              (str "Proof editing mode not supported in module types");
 
142
          start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t) 
 
143
            (fun _ _ -> ())
 
144
      | DefineBody (bl, _, c, tycon) -> 
 
145
          ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon))
 
146
  | VernacFixpoint (l, b) -> 
 
147
      List.iter (fun ((lid, _, _, _, _), _) -> 
 
148
        check_fresh lid;
 
149
        Dumpglob.dump_definition lid false "fix") l;
 
150
      let _ = trace (str "Building fixpoint") in
 
151
        ignore(Subtac_command.build_recursive l b)
 
152
          
 
153
  | VernacStartTheoremProof (thkind, [Some id, (bl, t)], lettop, hook) ->
 
154
      Dumpglob.dump_definition id false "prf";
 
155
      if not(Pfedit.refining ()) then
 
156
        if lettop then
 
157
          errorlabstrm "Subtac_command.StartProof"
 
158
            (str "Let declarations can only be used in proof editing mode");
 
159
      if Lib.is_modtype () then
 
160
        errorlabstrm "Subtac_command.StartProof"
 
161
          (str "Proof editing mode not supported in module types");
 
162
      check_fresh id;
 
163
      start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook
 
164
        
 
165
  | VernacAssumption (stre,nl,l) -> 
 
166
      vernac_assumption env isevars stre l nl
 
167
        
 
168
  | VernacInstance (glob, sup, is, props, pri) ->
 
169
      dump_constraint "inst" is;
 
170
      ignore(Subtac_classes.new_instance ~global:glob sup is props pri)
 
171
        
 
172
  | VernacCoFixpoint (l, b) ->
 
173
      if Dumpglob.dump () then 
 
174
        List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "cofix") l;
 
175
      ignore(Subtac_command.build_corecursive l b)
 
176
        
 
177
  (*| VernacEndProof e -> 
 
178
    subtac_end_proof e*)
 
179
 
 
180
  | _ -> user_err_loc (loc,"", str ("Invalid Program command"))
 
181
  with 
 
182
  | Typing_error e ->
 
183
      msg_warning (str "Type error in Program tactic:");
 
184
      let cmds = 
 
185
        (match e with
 
186
        | NonFunctionalApp (loc, x, mux, e) ->
 
187
            str "non functional application of term " ++ 
 
188
              e ++ str " to function " ++ x ++ str " of (mu) type " ++ mux
 
189
        | NonSigma (loc, t) ->
 
190
            str "Term is not of Sigma type: " ++ t
 
191
        | NonConvertible (loc, x, y) ->
 
192
            str "Unconvertible terms:" ++ spc () ++
 
193
              x ++ spc () ++ str "and" ++ spc () ++ y
 
194
        | IllSorted (loc, t) ->
 
195
            str "Term is ill-sorted:" ++ spc () ++ t
 
196
        )
 
197
      in msg_warning cmds
 
198
        
 
199
  | Subtyping_error e ->
 
200
      msg_warning (str "(Program tactic) Subtyping error:");
 
201
      let cmds = 
 
202
        match e with
 
203
        | UncoercibleInferType (loc, x, y) ->
 
204
            str "Uncoercible terms:" ++ spc ()
 
205
            ++ x ++ spc () ++ str "and" ++ spc () ++ y
 
206
        | UncoercibleInferTerm (loc, x, y, tx, ty) ->
 
207
            str "Uncoercible terms:" ++ spc ()
 
208
            ++ tx ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ x
 
209
            ++ str "and" ++ spc() ++ ty ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ y
 
210
        | UncoercibleRewrite (x, y) ->
 
211
            str "Uncoercible terms:" ++ spc ()
 
212
            ++ x ++ spc () ++ str "and" ++ spc () ++ y
 
213
      in msg_warning cmds
 
214
 
 
215
  | Cases.PatternMatchingError (env, exn) as e ->
 
216
      debug 2 (Himsg.explain_pattern_matching_error env exn);
 
217
      raise e
 
218
        
 
219
  | Type_errors.TypeError (env, exn) as e ->
 
220
      debug 2 (Himsg.explain_type_error env exn);
 
221
      raise e
 
222
        
 
223
  | Pretype_errors.PretypeError (env, exn) as e ->
 
224
      debug 2 (Himsg.explain_pretype_error env exn);
 
225
      raise e
 
226
        
 
227
  | (Stdpp.Exc_located (loc, Proof_type.LtacLocated (_,e')) |
 
228
     Stdpp.Exc_located (loc, e') as e) ->
 
229
      debug 2 (str "Parsing exception: ");
 
230
      (match e' with
 
231
      | Type_errors.TypeError (env, exn) ->
 
232
          debug 2 (Himsg.explain_type_error env exn);
 
233
          raise e
 
234
            
 
235
      | Pretype_errors.PretypeError (env, exn) ->
 
236
          debug 2 (Himsg.explain_pretype_error env exn);
 
237
          raise e
 
238
 
 
239
      | e'' -> raise e)
 
240
        
 
241
  | e -> raise e