aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/safe_typing.mli
blob: 86e423dd832159527ea1c4160706d6eea3ebd2b0 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(*i $Id$ i*)

(*i*)
open Names
open Term
open Declarations
open Entries
(*i*)

(*s Safe environments. Since we are now able to type terms, we can
  define an abstract type of safe environments, where objects are
  typed before being added.

  We also add [open_structure] and [close_section], [close_module] to
  provide functionnality for sections and interactive modules 
*)

type safe_environment

val env_of_safe_env : safe_environment -> Environ.env

val empty_environment : safe_environment

(* Adding and removing local declarations (Local or Variables) *)
val push_named_assum :
  identifier * types -> safe_environment ->
    Univ.constraints * safe_environment
val push_named_def :
  identifier * constr * types option -> safe_environment ->
    Univ.constraints * safe_environment

(* Adding global axioms or definitions *)
type global_declaration = 
  | ConstantEntry of constant_entry
  | GlobalRecipe of Cooking.recipe

val add_constant : 
  dir_path -> label -> global_declaration -> safe_environment -> 
      kernel_name * safe_environment

(* Adding an inductive type *)
val add_mind : 
  dir_path -> label -> mutual_inductive_entry -> safe_environment ->
    mutual_inductive * safe_environment

(* Adding a module *)
val add_module :
  label -> module_entry -> safe_environment 
    -> module_path * safe_environment

(* Adding a module type *)
val add_modtype :
  label -> module_type_entry -> safe_environment 
    -> kernel_name * safe_environment

(* Adding universe constraints *)
val add_constraints : 
  Univ.constraints -> safe_environment -> safe_environment

(* Settin the strongly constructive or classical logical engagement *)
val set_engagement : Environ.engagement -> safe_environment -> safe_environment


(*s Interactive module functions *)
val start_module : 
  label -> (mod_bound_id * module_type_entry) list 
    -> module_type_entry option 
      -> safe_environment -> module_path * safe_environment

val end_module :
  label -> safe_environment -> module_path * safe_environment 


val start_modtype :
  label -> (mod_bound_id * module_type_entry) list
    -> safe_environment -> module_path * safe_environment

val end_modtype :
  label -> safe_environment -> kernel_name * safe_environment


val current_modpath : safe_environment -> module_path
val current_msid : safe_environment -> mod_self_id


(* Loading and saving compilation units *)

(* exporting and importing modules *)
type compiled_library

val start_library : dir_path -> safe_environment 
      -> module_path * safe_environment

val export : safe_environment -> dir_path  
      -> mod_self_id * compiled_library

val import : compiled_library -> Digest.t -> safe_environment 
      -> module_path * safe_environment

(* Remove the body of opaque constants *)

val lighten_library : compiled_library -> compiled_library

(*s Typing judgments *)

type judgment

val j_val : judgment -> constr
val j_type : judgment -> constr

(* Safe typing of a term returning a typing judgment and universe
   constraints to be added to the environment for the judgment to
   hold. It is guaranteed that the constraints are satisfiable
 *)
val safe_infer : safe_environment -> constr -> judgment * Univ.constraints

val typing : safe_environment -> constr -> judgment