← Back to branch summary

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

« back to all changes in this revision

Viewing changes to interp/reserve.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/reserve.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: reserve.ml 10727 2008-03-28 20:22:43Z msozeau $ i*)
 
10
 
 
11
(* Reserved names *)
 
12
 
 
13
open Util
 
14
open Pp
 
15
open Names
 
16
open Nameops
 
17
open Summary
 
18
open Libobject
 
19
open Lib
 
20
 
 
21
let reserve_table = ref Idmap.empty
 
22
 
 
23
let cache_reserved_type (_,(id,t)) =
 
24
  reserve_table := Idmap.add id t !reserve_table
 
25
 
 
26
let (in_reserved, _) =
 
27
  declare_object {(default_object "RESERVED-TYPE") with 
 
28
    cache_function = cache_reserved_type }
 
29
 
 
30
let _ = 
 
31
  Summary.declare_summary "reserved-type"
 
32
    { Summary.freeze_function = (fun () -> !reserve_table);
 
33
      Summary.unfreeze_function = (fun r -> reserve_table := r);
 
34
      Summary.init_function = (fun () -> reserve_table := Idmap.empty);
 
35
      Summary.survive_module = false;
 
36
      Summary.survive_section = false }
 
37
 
 
38
let declare_reserved_type (loc,id) t = 
 
39
  if id <> root_of_id id then
 
40
    user_err_loc(loc,"declare_reserved_type",
 
41
    (pr_id id ++ str
 
42
      " is not reservable: it must have no trailing digits, quote, or _"));
 
43
  begin try
 
44
    let _ = Idmap.find id !reserve_table in 
 
45
    user_err_loc(loc,"declare_reserved_type",
 
46
    (pr_id id++str" is already bound to a type"))
 
47
  with Not_found -> () end;
 
48
  add_anonymous_leaf (in_reserved (id,t))
 
49
 
 
50
let find_reserved_type id = Idmap.find (root_of_id id) !reserve_table
 
51
 
 
52
open Rawterm
 
53
 
 
54
let rec unloc = function
 
55
  | RVar (_,id) -> RVar (dummy_loc,id)
 
56
  | RApp (_,g,args) -> RApp (dummy_loc,unloc g, List.map unloc args)
 
57
  | RLambda (_,na,bk,ty,c) -> RLambda (dummy_loc,na,bk,unloc ty,unloc c)
 
58
  | RProd (_,na,bk,ty,c) -> RProd (dummy_loc,na,bk,unloc ty,unloc c)
 
59
  | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c)
 
60
  | RCases (_,sty,rtntypopt,tml,pl) ->
 
61
      RCases (dummy_loc,sty,
 
62
        (Option.map unloc rtntypopt),
 
63
        List.map (fun (tm,x) -> (unloc tm,x)) tml,
 
64
        List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl)
 
65
  | RLetTuple (_,nal,(na,po),b,c) ->
 
66
      RLetTuple (dummy_loc,nal,(na,Option.map unloc po),unloc b,unloc c)
 
67
  | RIf (_,c,(na,po),b1,b2) ->
 
68
      RIf (dummy_loc,unloc c,(na,Option.map unloc po),unloc b1,unloc b2)
 
69
  | RRec (_,fk,idl,bl,tyl,bv) ->
 
70
      RRec (dummy_loc,fk,idl,
 
71
            Array.map (List.map 
 
72
              (fun (na,k,obd,ty) -> (na,k,Option.map unloc obd, unloc ty)))
 
73
              bl,
 
74
            Array.map unloc tyl,
 
75
            Array.map unloc bv)
 
76
  | RCast (_,c, CastConv (k,t)) -> RCast (dummy_loc,unloc c, CastConv (k,unloc t))
 
77
  | RCast (_,c, CastCoerce) -> RCast (dummy_loc,unloc c, CastCoerce)
 
78
  | RSort (_,x) -> RSort (dummy_loc,x)
 
79
  | RHole (_,x)  -> RHole (dummy_loc,x)
 
80
  | RRef (_,x) -> RRef (dummy_loc,x)
 
81
  | REvar (_,x,l) -> REvar (dummy_loc,x,l)
 
82
  | RPatVar (_,x) -> RPatVar (dummy_loc,x)
 
83
  | RDynamic (_,x) -> RDynamic (dummy_loc,x)
 
84
 
 
85
let anonymize_if_reserved na t = match na with
 
86
  | Name id as na ->
 
87
      (try 
 
88
        if not !Flags.raw_print & unloc t = find_reserved_type id
 
89
        then RHole (dummy_loc,Evd.BinderType na)
 
90
        else t
 
91
      with Not_found -> t)
 
92
  | Anonymous -> t