← Back to branch summary

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

« back to all changes in this revision

Viewing changes to contrib/field/field.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/field/field.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: field.ml4 10076 2007-08-16 11:16:43Z notin $ *)
 
12
 
 
13
open Names
 
14
open Pp
 
15
open Proof_type
 
16
open Tacinterp
 
17
open Tacmach
 
18
open Term
 
19
open Typing
 
20
open Util
 
21
open Vernacinterp
 
22
open Vernacexpr
 
23
open Tacexpr
 
24
open Mod_subst
 
25
open Coqlib
 
26
 
 
27
(* Interpretation of constr's *)
 
28
let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c
 
29
 
 
30
(* Construction of constants *)
 
31
let constant dir s = gen_constant "Field" ("field"::dir) s
 
32
let init_constant s = gen_constant_in_modules "Field" init_modules s
 
33
 
 
34
(* To deal with the optional arguments *)
 
35
let constr_of_opt a opt =
 
36
  let ac = constr_of a in
 
37
  let ac3 = mkArrow ac (mkArrow ac ac) in
 
38
  match opt with
 
39
  | None -> mkApp (init_constant "None",[|ac3|])
 
40
  | Some f -> mkApp (init_constant "Some",[|ac3;constr_of f|])
 
41
 
 
42
(* Table of theories *)
 
43
let th_tab = ref (Gmap.empty : (constr,constr) Gmap.t)
 
44
 
 
45
let lookup env typ =
 
46
  try Gmap.find typ !th_tab
 
47
  with Not_found -> 
 
48
    errorlabstrm "field"
 
49
      (str "No field is declared for type" ++ spc() ++
 
50
      Printer.pr_lconstr_env env typ)
 
51
 
 
52
let _ = 
 
53
  let init () = th_tab := Gmap.empty in
 
54
  let freeze () = !th_tab in
 
55
  let unfreeze fs = th_tab := fs in
 
56
  Summary.declare_summary "field"
 
57
    { Summary.freeze_function   = freeze;
 
58
      Summary.unfreeze_function = unfreeze;
 
59
      Summary.init_function     = init;
 
60
      Summary.survive_module = false;
 
61
      Summary.survive_section   = false }
 
62
 
 
63
let load_addfield _ = ()
 
64
let cache_addfield (_,(typ,th)) = th_tab := Gmap.add typ th !th_tab
 
65
let subst_addfield (_,subst,(typ,th as obj)) =
 
66
  let typ' = subst_mps subst typ in
 
67
  let th' = subst_mps subst th in
 
68
    if typ' == typ && th' == th then obj else
 
69
      (typ',th')
 
70
let export_addfield x = Some x
 
71
 
 
72
(* Declaration of the Add Field library object *)
 
73
let (in_addfield,out_addfield)=
 
74
  Libobject.declare_object {(Libobject.default_object "ADD_FIELD") with
 
75
       Libobject.open_function = (fun i o -> if i=1 then cache_addfield o);
 
76
       Libobject.cache_function = cache_addfield;
 
77
       Libobject.subst_function = subst_addfield;
 
78
       Libobject.classify_function = (fun (_,a) -> Libobject.Substitute a);
 
79
       Libobject.export_function = export_addfield }
 
80
 
 
81
(* Adds a theory to the table *)
 
82
let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth
 
83
  ainv_l =
 
84
  begin
 
85
    (try
 
86
      Ring.add_theory true true false a None None None aplus amult aone azero
 
87
        (Some aopp) aeq rth Quote.ConstrSet.empty
 
88
     with | UserError("Add Semi Ring",_) -> ());
 
89
    let th = mkApp ((constant ["LegacyField_Theory"] "Build_Field_Theory"),
 
90
      [|a;aplus;amult;aone;azero;aopp;aeq;ainv;aminus_o;adiv_o;rth;ainv_l|]) in
 
91
    begin
 
92
      let _ = type_of (Global.env ()) Evd.empty th in ();
 
93
      Lib.add_anonymous_leaf (in_addfield (a,th))
 
94
    end
 
95
  end
 
96
 
 
97
(* Vernac command declaration *)
 
98
open Extend
 
99
open Pcoq
 
100
open Genarg
 
101
 
 
102
VERNAC ARGUMENT EXTEND divarg
 
103
| [ "div" ":=" constr(adiv) ] -> [ adiv ]
 
104
END
 
105
 
 
106
VERNAC ARGUMENT EXTEND minusarg
 
107
| [ "minus" ":=" constr(aminus) ] -> [ aminus ]
 
108
END
 
109
 
 
110
(*
 
111
(* The v7->v8 translator needs printers, then temporary use ARGUMENT EXTEND...*)
 
112
VERNAC ARGUMENT EXTEND minus_div_arg
 
113
| [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ]
 
114
| [ "with" divarg(d) minusarg_opt(m) ] -> [ m, Some d ]
 
115
| [ ] -> [ None, None ]
 
116
END
 
117
*)
 
118
 
 
119
(* For the translator, otherwise the code above is OK *)
 
120
open Ppconstr
 
121
let pp_minus_div_arg _prc _prlc _prt (omin,odiv) = 
 
122
  if omin=None && odiv=None then mt() else
 
123
    spc() ++ str "with" ++
 
124
    pr_opt (fun c -> str "minus := " ++ _prc c) omin ++
 
125
    pr_opt (fun c -> str "div := " ++ _prc c) odiv
 
126
(*
 
127
let () =
 
128
  Pptactic.declare_extra_genarg_pprule true
 
129
    (rawwit_minus_div_arg,pp_minus_div_arg)
 
130
    (globwit_minus_div_arg,pp_minus_div_arg)
 
131
    (wit_minus_div_arg,pp_minus_div_arg)
 
132
*)
 
133
ARGUMENT EXTEND minus_div_arg 
 
134
  TYPED AS constr_opt * constr_opt
 
135
  PRINTED BY pp_minus_div_arg
 
136
| [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ]
 
137
| [ "with" divarg(d) minusarg_opt(m) ] -> [ m, Some d ]
 
138
| [ ] -> [ None, None ]
 
139
END
 
140
 
 
141
VERNAC COMMAND EXTEND Field
 
142
  [ "Add" "Legacy" "Field" 
 
143
      constr(a) constr(aplus) constr(amult) constr(aone)
 
144
      constr(azero) constr(aopp) constr(aeq)
 
145
      constr(ainv) constr(rth) constr(ainv_l) minus_div_arg(md) ]
 
146
    -> [ let (aminus_o, adiv_o) = md in
 
147
         add_field
 
148
           (constr_of a) (constr_of aplus) (constr_of amult)
 
149
           (constr_of aone) (constr_of azero) (constr_of aopp)
 
150
           (constr_of aeq) (constr_of ainv) (constr_of_opt a aminus_o)
 
151
           (constr_of_opt a adiv_o) (constr_of rth) (constr_of ainv_l) ]
 
152
END
 
153
 
 
154
(* Guesses the type and calls field_gen with the right theory *)
 
155
let field g =
 
156
  Coqlib.check_required_library ["Coq";"field";"LegacyField"];
 
157
  let typ = 
 
158
    match Hipattern.match_with_equation (pf_concl g) with
 
159
      | Some (eq,t::args) when eq = (Coqlib.build_coq_eq_data()).Coqlib.eq -> t
 
160
      | _ -> error "The statement is not built from Leibniz' equality" in
 
161
  let th = VConstr (lookup (pf_env g) typ) in
 
162
  (interp_tac_gen [(id_of_string "FT",th)] [] (get_debug ())
 
163
    <:tactic< match goal with |- (@eq _ _ _) => field_gen FT end >>) g
 
164
 
 
165
(* Verifies that all the terms have the same type and gives the right theory *)
 
166
let guess_theory env evc = function
 
167
  | c::tl ->
 
168
    let t = type_of env evc c in
 
169
    if List.exists (fun c1 ->
 
170
      not (Reductionops.is_conv env evc t (type_of env evc c1))) tl then
 
171
      errorlabstrm "Field:" (str" All the terms must have the same type")
 
172
    else
 
173
      lookup env t
 
174
  | [] -> anomaly "Field: must have a non-empty constr list here"
 
175
 
 
176
(* Guesses the type and calls Field_Term with the right theory *)
 
177
let field_term l g =
 
178
  Coqlib.check_required_library ["Coq";"field";"LegacyField"];
 
179
  let env = (pf_env g)
 
180
  and evc = (project g) in
 
181
  let th = valueIn (VConstr (guess_theory env evc l))
 
182
  and nl = List.map (fun x -> valueIn (VConstr x)) (Quote.sort_subterm g l) in
 
183
  (List.fold_right
 
184
    (fun c a ->
 
185
     let tac = (Tacinterp.interp <:tactic<(Field_Term $th $c)>>) in
 
186
     Tacticals.tclTHENFIRSTn tac [|a|]) nl Tacticals.tclIDTAC) g
 
187
 
 
188
(* Declaration of Field *)
 
189
 
 
190
TACTIC EXTEND legacy_field
 
191
| [ "legacy" "field" ] -> [ field ]
 
192
| [ "legacy" "field" ne_constr_list(l) ] -> [ field_term l ]
 
193
END