← Back to branch summary

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

« back to all changes in this revision

Viewing changes to kernel/term_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:
kernel/term_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: term_typing.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
10
 
 
11
open Util
 
12
open Names
 
13
open Univ
 
14
open Term
 
15
open Reduction
 
16
open Sign
 
17
open Declarations
 
18
open Inductive
 
19
open Environ
 
20
open Entries
 
21
open Type_errors
 
22
open Indtypes
 
23
open Typeops
 
24
 
 
25
let constrain_type env j cst1 = function
 
26
  | None ->
 
27
      make_polymorphic_if_constant_for_ind env j, cst1
 
28
  | Some t -> 
 
29
      let (tj,cst2) = infer_type env t in
 
30
      let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
 
31
      assert (t = tj.utj_val);
 
32
      NonPolymorphicType t, Constraint.union (Constraint.union cst1 cst2) cst3
 
33
 
 
34
let local_constrain_type env j cst1 = function
 
35
  | None ->
 
36
      j.uj_type, cst1
 
37
  | Some t -> 
 
38
      let (tj,cst2) = infer_type env t in
 
39
      let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
 
40
      assert (t = tj.utj_val);
 
41
      t, Constraint.union (Constraint.union cst1 cst2) cst3
 
42
 
 
43
let translate_local_def env (b,topt) =
 
44
  let (j,cst) = infer env b in
 
45
  let (typ,cst) = local_constrain_type env j cst topt in
 
46
    (j.uj_val,typ,cst)
 
47
 
 
48
let translate_local_assum env t =
 
49
  let (j,cst) = infer env t in
 
50
  let t = Typeops.assumption_of_judgment env j in
 
51
    (t,cst)
 
52
 
 
53
(*
 
54
 
 
55
(* Same as push_named, but check that the variable is not already
 
56
   there. Should *not* be done in Environ because tactics add temporary
 
57
   hypothesis many many times, and the check performed here would
 
58
   cost too much. *)
 
59
let safe_push_named (id,_,_ as d) env =
 
60
  let _ =
 
61
    try
 
62
      let _ = lookup_named id env in 
 
63
      error ("Identifier "^string_of_id id^" already defined.")
 
64
    with Not_found -> () in
 
65
  push_named d env
 
66
 
 
67
let push_named_def = push_rel_or_named_def safe_push_named
 
68
let push_rel_def = push_rel_or_named_def push_rel
 
69
 
 
70
let push_rel_or_named_assum push (id,t) env =
 
71
  let (j,cst) = safe_infer env t in
 
72
  let t = Typeops.assumption_of_judgment env j in
 
73
  let env' = add_constraints cst env in
 
74
  let env'' = push (id,None,t) env' in
 
75
  (cst,env'')
 
76
 
 
77
let push_named_assum = push_rel_or_named_assum push_named
 
78
let push_rel_assum d env = snd (push_rel_or_named_assum push_rel d env)
 
79
 
 
80
let push_rels_with_univ vars env =
 
81
  List.fold_left (fun env nvar -> push_rel_assum nvar env) env vars
 
82
*)
 
83
 
 
84
 
 
85
(* Insertion of constants and parameters in environment. *)
 
86
 
 
87
let infer_declaration env dcl =
 
88
  match dcl with
 
89
  | DefinitionEntry c ->
 
90
      let (j,cst) = infer env c.const_entry_body in
 
91
      let (typ,cst) = constrain_type env j cst c.const_entry_type in
 
92
      Some (Declarations.from_val j.uj_val), typ, cst,
 
93
        c.const_entry_opaque, c.const_entry_boxed, false
 
94
  | ParameterEntry (t,nl) ->
 
95
      let (j,cst) = infer env t in
 
96
      None, NonPolymorphicType (Typeops.assumption_of_judgment env j), cst,
 
97
        false, false, nl
 
98
 
 
99
let global_vars_set_constant_type env = function
 
100
  | NonPolymorphicType t -> global_vars_set env t
 
101
  | PolymorphicArity (ctx,_) ->
 
102
      Sign.fold_rel_context 
 
103
        (fold_rel_declaration
 
104
          (fun t c -> Idset.union (global_vars_set env t) c))
 
105
      ctx ~init:Idset.empty
 
106
 
 
107
let build_constant_declaration env kn (body,typ,cst,op,boxed,inline) =
 
108
  let ids =
 
109
    match body with 
 
110
    | None -> global_vars_set_constant_type env typ
 
111
    | Some b ->
 
112
        Idset.union 
 
113
          (global_vars_set env (Declarations.force b)) 
 
114
          (global_vars_set_constant_type env typ)
 
115
  in
 
116
  let tps = Cemitcodes.from_val (compile_constant_body env body op boxed) in
 
117
  let hyps = keep_hyps env ids in
 
118
    { const_hyps = hyps;
 
119
      const_body = body;
 
120
      const_type = typ;
 
121
      const_body_code = tps;
 
122
     (* const_type_code = to_patch env typ;*)
 
123
      const_constraints = cst;
 
124
      const_opaque = op; 
 
125
      const_inline = inline}
 
126
 
 
127
(*s Global and local constant declaration. *)
 
128
 
 
129
let translate_constant env kn ce =
 
130
  build_constant_declaration env kn (infer_declaration env ce)
 
131
 
 
132
let translate_recipe env kn r = 
 
133
  build_constant_declaration env kn (Cooking.cook_constant env r)
 
134
 
 
135
(* Insertion of inductive types. *)
 
136
 
 
137
let translate_mind env mie = check_inductive env mie