← Back to branch summary

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

« back to all changes in this revision

Viewing changes to checker/safe_typing.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:
checker/safe_typing.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: safe_typing.ml 10275 2007-10-30 11:01:24Z barras $ *)
 
10
 
 
11
open Pp
 
12
open Util
 
13
open Names
 
14
open Declarations
 
15
open Environ
 
16
open Mod_checking
 
17
 
 
18
(************************************************************************)
 
19
(*
 
20
 * Global environment
 
21
 *)
 
22
 
 
23
let genv = ref empty_env
 
24
let reset () = genv := empty_env
 
25
let get_env () = !genv
 
26
 
 
27
let set_engagement c =
 
28
  genv := set_engagement c !genv
 
29
 
 
30
(* full_add_module adds module with universes and constraints *)
 
31
let full_add_module dp mb digest =
 
32
  let env = !genv in
 
33
  let mp = MPfile dp in
 
34
  let env = add_constraints mb.mod_constraints env in
 
35
  let env = Modops.add_module mp mb env in
 
36
  genv := add_digest env dp digest
 
37
 
 
38
(* Check that the engagement expected by a library matches the initial one *)
 
39
let check_engagement env c =
 
40
  match engagement env, c with
 
41
    | Some ImpredicativeSet, Some ImpredicativeSet -> ()
 
42
    | _, None -> ()
 
43
    | _, Some ImpredicativeSet ->
 
44
        error "Needs option -impredicative-set"
 
45
 
 
46
(* Libraries = Compiled modules *)
 
47
 
 
48
let report_clash f caller dir =
 
49
  let msg =
 
50
    str "compiled library " ++ str(string_of_dirpath caller) ++
 
51
    spc() ++ str "makes inconsistent assumptions over library" ++ spc() ++
 
52
    str(string_of_dirpath dir) ++ fnl() in
 
53
  f msg
 
54
 
 
55
 
 
56
let check_imports f caller env needed =
 
57
  let check (dp,stamp) =
 
58
    try
 
59
      let actual_stamp = lookup_digest env dp in
 
60
      if stamp <> actual_stamp then report_clash f caller dp
 
61
    with Not_found -> 
 
62
      error ("Reference to unknown module " ^ (string_of_dirpath dp))
 
63
  in
 
64
  List.iter check needed
 
65
 
 
66
 
 
67
 
 
68
(* Remove the body of opaque constants in modules *)
 
69
(* also remove mod_expr ? *)
 
70
let rec lighten_module mb =
 
71
  { mb with
 
72
    mod_expr = Option.map lighten_modexpr mb.mod_expr;
 
73
    mod_type = Option.map lighten_modexpr mb.mod_type }
 
74
 
 
75
and lighten_struct struc = 
 
76
  let lighten_body (l,body) = (l,match body with
 
77
    | SFBconst ({const_opaque=true} as x) -> SFBconst {x with const_body=None}
 
78
    | (SFBconst _ | SFBmind _ | SFBalias _) as x -> x
 
79
    | SFBmodule m -> SFBmodule (lighten_module m)
 
80
    | SFBmodtype m -> SFBmodtype 
 
81
        ({m with 
 
82
            typ_expr = lighten_modexpr m.typ_expr}))
 
83
  in
 
84
    List.map lighten_body struc
 
85
 
 
86
and lighten_modexpr = function
 
87
  | SEBfunctor (mbid,mty,mexpr) ->
 
88
      SEBfunctor (mbid, 
 
89
                    ({mty with 
 
90
                        typ_expr = lighten_modexpr mty.typ_expr}),
 
91
                  lighten_modexpr mexpr)
 
92
  | SEBident mp as x -> x
 
93
  | SEBstruct (msid, struc) ->
 
94
      SEBstruct (msid, lighten_struct struc)
 
95
  | SEBapply (mexpr,marg,u) ->
 
96
      SEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u)
 
97
  | SEBwith (seb,wdcl) ->
 
98
      SEBwith (lighten_modexpr seb,wdcl) 
 
99
 
 
100
let lighten_library (dp,mb,depends,s) = (dp,lighten_module mb,depends,s)
 
101
 
 
102
 
 
103
type compiled_library = 
 
104
    dir_path *
 
105
    module_body *
 
106
    (dir_path * Digest.t) list *
 
107
    engagement option
 
108
 
 
109
open Validate
 
110
let val_deps = val_list (val_tuple"dep"[|val_dp;no_val|])
 
111
let val_vo = val_tuple "vo" [|val_dp;val_module;val_deps;val_opt val_eng|]
 
112
 
 
113
(* This function should append a certificate to the .vo file.
 
114
   The digest must be part of the certicate to rule out attackers
 
115
   that could change the .vo file between the time it was read and
 
116
   the time the stamp is written.
 
117
   For the moment, .vo are not signed. *)
 
118
let stamp_library file digest = ()
 
119
 
 
120
(* When the module is checked, digests do not need to match, but a
 
121
   warning is issued in case of mismatch *)
 
122
let import file (dp,mb,depends,engmt as vo) digest = 
 
123
  Validate.apply !Flags.debug val_vo vo;
 
124
  Flags.if_verbose msgnl (str "*** vo structure validated ***");
 
125
  let env = !genv in
 
126
  check_imports msg_warning dp env depends;
 
127
  check_engagement env engmt;
 
128
  check_module (add_constraints mb.mod_constraints env) mb;
 
129
  stamp_library file digest;
 
130
  (* We drop proofs once checked *)
 
131
(*  let mb = lighten_module mb in*)
 
132
  full_add_module dp mb digest
 
133
 
 
134
(* When the module is admitted, digests *must* match *)
 
135
let unsafe_import file (dp,mb,depends,engmt) digest = 
 
136
  let env = !genv in
 
137
  check_imports (errorlabstrm"unsafe_import") dp env depends;
 
138
  check_engagement env engmt;
 
139
  (* We drop proofs once checked *)
 
140
(*  let mb = lighten_module mb in*)
 
141
  full_add_module dp mb digest