summaryrefslogtreecommitdiff
path: root/kernel/safe_typing.mli
blob: 34dc68d2e00def1a351aa809877acf46a51c93bb (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
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Names
open Term
open Declarations
open Entries
open Mod_subst

(** {6 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
val is_empty : safe_environment -> bool

(** 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 ->
      constant * 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 -> inline -> safe_environment
    -> module_path * delta_resolver * safe_environment

(** Adding a module type *)
val add_modtype :
  label -> module_struct_entry -> inline -> safe_environment
    -> module_path * 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 : engagement -> safe_environment -> safe_environment


(** {6 Interactive module functions } *)

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

val end_module :
  label -> (module_struct_entry * inline) option
      -> safe_environment -> module_path * delta_resolver * safe_environment 

val add_module_parameter :
  mod_bound_id -> module_struct_entry -> inline -> safe_environment -> delta_resolver * safe_environment

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

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

val add_include :
  module_struct_entry -> bool -> inline -> safe_environment ->
   delta_resolver * safe_environment

val pack_module : safe_environment -> module_body
val current_modpath : safe_environment -> module_path
val delta_of_senv : safe_environment -> delta_resolver*delta_resolver
  

(** 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
      -> module_path * compiled_library

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

(** Remove the body of opaque constants *)

module LightenLibrary :
sig
  type table
  type lightened_compiled_library
  val save : compiled_library -> lightened_compiled_library * table
  val load : load_proof:Flags.load_proofs -> table Lazy.t ->
    lightened_compiled_library -> compiled_library
end

(** {6 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

(** {7 Query } *)

val exists_objlabel : label -> safe_environment -> bool

(*spiwack: safe retroknowledge functionalities *)

open Retroknowledge

val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a

val register : safe_environment -> field -> Retroknowledge.entry -> constr
                                         -> safe_environment