← Back to branch summary

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

« back to all changes in this revision

Viewing changes to kernel/safe_typing.ml

  • Committer: Package Import Robot
  • Author(s): Stéphane Glondu
  • Date: 2012-01-03 23:42:48 UTC
  • mfrom: (1.2.4)
  • Revision ID: package-import@ubuntu.com-20120103234248-p9r8h1579n67v55a
Tags: 8.3pl3-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
kernel/safe_typing.ml
1
1
(************************************************************************)
2
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
3
 
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 
3
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
4
4
(*   \VV/  **************************************************************)
5
5
(*    //   *      This file is distributed under the terms of the       *)
6
6
(*         *       GNU Lesser General Public License Version 2.1        *)
7
7
(************************************************************************)
8
8
 
9
 
(* $Id: safe_typing.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
9
(* $Id: safe_typing.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
10
10
 
11
11
open Util
12
12
open Names
40
40
     variant : modvariant;
41
41
     resolver : delta_resolver;
42
42
     resolver_of_param : delta_resolver;}
43
 
      
 
43
 
44
44
let check_label l labset =
45
45
  if Labset.mem l labset then error_existing_label l
46
46
 
 
47
let check_labels ls senv =
 
48
  Labset.iter (fun l -> check_label l senv) ls
 
49
 
 
50
let labels_of_mib mib =
 
51
  let add,get =
 
52
    let labels = ref Labset.empty in
 
53
    (fun id -> labels := Labset.add (label_of_id id) !labels),
 
54
    (fun () -> !labels)
 
55
  in
 
56
  let visit_mip mip =
 
57
    add mip.mind_typename;
 
58
    Array.iter add mip.mind_consnames
 
59
  in
 
60
  Array.iter visit_mip mib.mind_packets;
 
61
  get ()
 
62
 
47
63
let set_engagement_opt oeng env =
48
64
  match oeng with
49
65
      Some eng -> set_engagement eng env
107
123
    univ = Univ.Constraint.union cst senv.univ }
108
124
 
109
125
 
110
 
(*spiwack: functions for safe retroknowledge *)
111
 
 
112
 
(* terms which are closed under the environnement env, i.e
113
 
   terms which only depends on constant who are themselves closed *)
114
 
let closed env term =
115
 
  ContextObjectMap.is_empty (assumptions full_transparent_state env term)
116
 
 
117
 
(* the set of safe terms in an environement any recursive set of
118
 
   terms who are known not to prove inconsistent statement. It should
119
 
   include at least all the closed terms. But it could contain other ones
120
 
   like the axiom of excluded middle for instance *)
121
 
let safe =
122
 
  closed
123
 
 
124
 
 
125
 
 
126
126
(* universal lifting, used for the "get" operations mostly *)
127
127
let retroknowledge f senv =
128
128
  Environ.retroknowledge f (env_of_senv senv)
242
242
  if l <> label_of_id id then
243
243
    anomaly ("the label of inductive packet and its first inductive"^
244
244
             " type do not match");
245
 
  check_label l senv.labset;
246
 
    (* TODO: when we will allow reorderings we will have to verify
247
 
       all labels *)
248
245
  let mib = translate_mind senv.env mie in
 
246
  let labels = labels_of_mib mib in
 
247
  check_labels labels senv.labset;
249
248
  let senv' = add_constraints mib.mind_constraints senv in
250
249
  let kn = make_mind senv.modinfo.modpath dir l in
251
250
  let env'' = Environ.add_mind kn mib senv'.env in
252
251
  kn, { old = senv'.old;
253
252
        env = env'';
254
253
        modinfo = senv'.modinfo;
255
 
        labset = Labset.add l senv'.labset;  (* TODO: the same as above *)
 
254
        labset = Labset.union labels senv'.labset;
256
255
        revstruct = (l,SFBmind mib)::senv'.revstruct;
257
256
        univ = senv'.univ;
258
257
        engagement = senv'.engagement;
495
494
             (canonical_mind 
496
495
                (mind_of_delta resolver (mind_of_kn kn)))
497
496
           in
 
497
           let labels = labels_of_mib mib in
 
498
           check_labels labels senv.labset;
498
499
           let senv' = add_constraints mib.mind_constraints senv in
499
500
           let env'' = Environ.add_mind mind mib senv'.env in
500
501
             { old = senv'.old;
501
502
               env = env'';
502
503
               modinfo = senv'.modinfo;
503
 
               labset = Labset.add l senv'.labset;
 
504
               labset = Labset.union labels senv'.labset;
504
505
               revstruct = (l,SFBmind mib)::senv'.revstruct;
505
506
               univ = senv'.univ;
506
507
               engagement = senv'.engagement;