← Back to branch summary

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

« back to all changes in this revision

Viewing changes to interp/syntax_def.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:
interp/syntax_def.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: syntax_def.ml 11512 2008-10-27 12:28:36Z herbelin $ *)
 
10
 
 
11
open Util
 
12
open Pp
 
13
open Names
 
14
open Libnames
 
15
open Topconstr
 
16
open Libobject
 
17
open Lib
 
18
open Nameops
 
19
 
 
20
(* Syntactic definitions. *)
 
21
 
 
22
let syntax_table = ref (KNmap.empty : interpretation KNmap.t)
 
23
 
 
24
let _ = Summary.declare_summary
 
25
          "SYNTAXCONSTANT"
 
26
          { Summary.freeze_function = (fun () -> !syntax_table);
 
27
            Summary.unfreeze_function = (fun ft -> syntax_table := ft);
 
28
            Summary.init_function = (fun () -> syntax_table := KNmap.empty);
 
29
            Summary.survive_module = false;
 
30
            Summary.survive_section = false }
 
31
 
 
32
let add_syntax_constant kn c =
 
33
  syntax_table := KNmap.add kn c !syntax_table
 
34
 
 
35
let load_syntax_constant i ((sp,kn),(local,pat,onlyparse)) =
 
36
  if Nametab.exists_cci sp then
 
37
    errorlabstrm "cache_syntax_constant"
 
38
      (pr_id (basename sp) ++ str " already exists");
 
39
  add_syntax_constant kn pat;
 
40
  Nametab.push_syntactic_definition (Nametab.Until i) sp kn;
 
41
  if not onlyparse then
 
42
    (* Declare it to be used as long name *)
 
43
    Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
 
44
 
 
45
let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
 
46
  Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn;
 
47
  if not onlyparse then
 
48
    (* Redeclare it to be used as (short) name in case an other (distfix)
 
49
       notation was declared inbetween *)
 
50
    Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
 
51
 
 
52
let cache_syntax_constant d =
 
53
  load_syntax_constant 1 d
 
54
 
 
55
let subst_syntax_constant ((sp,kn),subst,(local,pat,onlyparse)) =
 
56
  (local,subst_interpretation subst pat,onlyparse)
 
57
 
 
58
let classify_syntax_constant (_,(local,_,_ as o)) =
 
59
  if local then Dispose else Substitute o
 
60
 
 
61
let export_syntax_constant (local,_,_ as o) =
 
62
  if local then None else Some o
 
63
 
 
64
let (in_syntax_constant, out_syntax_constant) =
 
65
  declare_object {(default_object "SYNTAXCONSTANT") with
 
66
    cache_function = cache_syntax_constant;
 
67
    load_function = load_syntax_constant;
 
68
    open_function = open_syntax_constant;
 
69
    subst_function = subst_syntax_constant;
 
70
    classify_function = classify_syntax_constant;
 
71
    export_function = export_syntax_constant } 
 
72
 
 
73
type syndef_interpretation = (identifier * subscopes) list * aconstr
 
74
 
 
75
(* Coercions to the general format of notation that also supports
 
76
   variables bound to list of expressions *)
 
77
let in_pat (ids,ac) = ((ids,[]),ac)
 
78
let out_pat ((ids,idsl),ac) = assert (idsl=[]); (ids,ac)
 
79
 
 
80
let declare_syntactic_definition local id onlyparse pat =
 
81
  let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in ()
 
82
 
 
83
let search_syntactic_definition loc kn =
 
84
  out_pat (KNmap.find kn !syntax_table)
 
85
 
 
86
let locate_global_with_alias (loc,qid) =
 
87
  match Nametab.extended_locate qid with
 
88
  | TrueGlobal ref -> ref
 
89
  | SyntacticDef kn -> 
 
90
  match search_syntactic_definition dummy_loc kn with
 
91
  | [],ARef ref -> ref
 
92
  | _ -> 
 
93
      user_err_loc (loc,"",pr_qualid qid ++ 
 
94
        str " is bound to a notation that does not denote a reference")
 
95
 
 
96
let inductive_of_reference_with_alias r =
 
97
  match locate_global_with_alias (qualid_of_reference r) with
 
98
  | IndRef ind -> ind
 
99
  | ref ->
 
100
      user_err_loc (loc_of_reference r,"global_inductive",
 
101
        pr_reference r ++ spc () ++ str "is not an inductive type")
 
102
 
 
103
let global_with_alias r =
 
104
  let (loc,qid as lqid) = qualid_of_reference r in
 
105
  try locate_global_with_alias lqid
 
106
  with Not_found -> Nametab.error_global_not_found_loc loc qid