aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-03-24 09:00:10 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-03-24 09:00:10 +0100
commit66ad590733b3a4dafe3c55a0b59d4f13f6c4b7bc (patch)
treebd9de08a53a13a5ccf74f2fdd65ade7e4ab03c43 /kernel
parent461aca5aebaf9c928b5125728e257062215db9a6 (diff)
parent9c80dd80feb1cc2ae6d0dc6e08985d4f51d4f329 (diff)
Merge branch 'v8.6' into trunk
Diffstat (limited to 'kernel')
-rw-r--r--kernel/entries.mli2
-rw-r--r--kernel/safe_typing.ml12
-rw-r--r--kernel/safe_typing.mli9
-rw-r--r--kernel/term_typing.ml67
-rw-r--r--kernel/term_typing.mli12
5 files changed, 78 insertions, 24 deletions
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 77081947e..1e07c9690 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -113,5 +113,3 @@ type side_effect = {
from_env : Declarations.structure_body CEphemeron.key;
eff : side_eff;
}
-
-type side_effects = side_effect list
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 2312f891c..caaaff1b8 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -208,19 +208,19 @@ let get_opaque_body env cbo =
Opaqueproof.force_constraints (Environ.opaque_tables env) opaque)
type private_constant = Entries.side_effect
-type private_constants = private_constant list
+type private_constants = Term_typing.side_effects
type private_constant_role = Term_typing.side_effect_role =
| Subproof
| Schema of inductive * string
-let empty_private_constants = []
-let add_private x xs = if List.mem_f Term_typing.equal_eff x xs then xs else x :: xs
-let concat_private xs ys = List.fold_right add_private xs ys
+let empty_private_constants = Term_typing.empty_seff
+let add_private = Term_typing.add_seff
+let concat_private = Term_typing.concat_seff
let mk_pure_proof = Term_typing.mk_pure_proof
let inline_private_constants_in_constr = Term_typing.inline_side_effects
let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects
-let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x)
+let side_effects_of_private_constants = Term_typing.uniq_seff
let private_con_of_con env c =
let cbo = Environ.lookup_constant c env.env in
@@ -250,7 +250,7 @@ let universes_of_private eff =
| Entries.SEsubproof (c, cb, e) ->
if cb.const_polymorphic then acc
else Univ.ContextSet.of_context cb.const_universes :: acc)
- [] eff
+ [] (Term_typing.uniq_seff eff)
let env_of_safe_env senv = senv.env
let env_of_senv = env_of_safe_env
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 15ebc7d88..efeb98bd2 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -47,11 +47,18 @@ type private_constant_role =
| Schema of inductive * string
val side_effects_of_private_constants :
- private_constants -> Entries.side_effects
+ private_constants -> Entries.side_effect list
+(** Return the list of individual side-effects in the order of their
+ creation. *)
val empty_private_constants : private_constants
val add_private : private_constant -> private_constants -> private_constants
+(** Add a constant to a list of private constants. The former must be more
+ recent than all constants appearing in the latter, i.e. one should not
+ create a dependency cycle. *)
val concat_private : private_constants -> private_constants -> private_constants
+(** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in
+ [e1] must be more recent than those of [e2]. *)
val private_con_of_con : safe_environment -> constant -> private_constant
val private_con_of_scheme : kind:string -> safe_environment -> (inductive * constant) list -> private_constant
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 569a58378..2eb2c040e 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -26,8 +26,6 @@ module NamedDecl = Context.Named.Declaration
(* Insertion of constants and parameters in environment. *)
-let mk_pure_proof c = (c, Univ.ContextSet.empty), []
-
let equal_eff e1 e2 =
let open Entries in
match e1, e2 with
@@ -39,13 +37,54 @@ let equal_eff e1 e2 =
cl1 cl2
| _ -> false
-let rec uniq_seff = function
- | [] -> []
- | x :: xs -> x :: uniq_seff (List.filter (fun y -> not (equal_eff x y)) xs)
-(* The list of side effects is in reverse order (most recent first).
- * To keep the "topological" order between effects we have to uniq-ize from
- * the tail *)
-let uniq_seff l = List.rev (uniq_seff (List.rev l))
+module SideEffects :
+sig
+ type t
+ val repr : t -> side_effect list
+ val empty : t
+ val add : side_effect -> t -> t
+ val concat : t -> t -> t
+end =
+struct
+
+let compare_seff e1 e2 = match e1, e2 with
+| SEsubproof (c1, _, _), SEsubproof (c2, _, _) -> Constant.CanOrd.compare c1 c2
+| SEscheme (cl1, _), SEscheme (cl2, _) ->
+ let cmp (_, c1, _, _) (_, c2, _, _) = Constant.CanOrd.compare c1 c2 in
+ CList.compare cmp cl1 cl2
+| SEsubproof _, SEscheme _ -> -1
+| SEscheme _, SEsubproof _ -> 1
+
+module SeffOrd = struct
+type t = side_effect
+let compare e1 e2 = compare_seff e1.eff e2.eff
+end
+
+module SeffSet = Set.Make(SeffOrd)
+
+type t = { seff : side_effect list; elts : SeffSet.t }
+(** Invariant: [seff] is a permutation of the elements of [elts] *)
+
+let repr eff = eff.seff
+let empty = { seff = []; elts = SeffSet.empty }
+let add x es =
+ if SeffSet.mem x es.elts then es
+ else { seff = x :: es.seff; elts = SeffSet.add x es.elts }
+let concat xes yes =
+ List.fold_right add xes.seff yes
+
+end
+
+type side_effects = SideEffects.t
+
+let uniq_seff_rev = SideEffects.repr
+let uniq_seff l = List.rev (SideEffects.repr l)
+
+let empty_seff = SideEffects.empty
+let add_seff = SideEffects.add
+let concat_seff = SideEffects.concat
+
+let mk_pure_proof c = (c, Univ.ContextSet.empty), empty_seff
let inline_side_effects env body ctx side_eff =
let handle_sideff (t,ctx,sl) { eff = se; from_env = mb } =
@@ -98,7 +137,7 @@ let inline_side_effects env body ctx side_eff =
t, ctx, (mb,List.length cbl) :: sl
in
(* CAVEAT: we assure a proper order *)
- List.fold_left handle_sideff (body,ctx,[]) (uniq_seff side_eff)
+ List.fold_left handle_sideff (body,ctx,[]) (uniq_seff_rev side_eff)
(* Given the list of signatures of side effects, checks if they match.
* I.e. if they are ordered descendants of the current revstruct *)
@@ -380,7 +419,7 @@ let constant_entry_of_side_effect cb u =
| Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty
| _ -> assert false in
DefinitionEntry {
- const_entry_body = Future.from_val (pt, []);
+ const_entry_body = Future.from_val (pt, empty_seff);
const_entry_secctx = None;
const_entry_feedback = None;
const_entry_type =
@@ -414,7 +453,7 @@ let export_side_effects mb env ce =
let _, eff = Future.force body in
let ce = DefinitionEntry { c with
const_entry_body = Future.chain ~pure:true body
- (fun (b_ctx, _) -> b_ctx, []) } in
+ (fun (b_ctx, _) -> b_ctx, empty_seff) } in
let not_exists (c,_,_,_) =
try ignore(Environ.lookup_constant c env); false
with Not_found -> true in
@@ -426,7 +465,7 @@ let export_side_effects mb env ce =
let cbl = List.filter not_exists cbl in
if cbl = [] then acc, sl
else cbl :: acc, (mb,List.length cbl) :: sl in
- let seff, signatures = List.fold_left aux ([],[]) (uniq_seff eff) in
+ let seff, signatures = List.fold_left aux ([],[]) (uniq_seff_rev eff) in
let trusted = check_signatures mb signatures in
let push_seff env = function
| kn, cb, `Nothing, _ ->
@@ -498,7 +537,7 @@ let inline_entry_side_effects env ce = { ce with
const_entry_body = Future.chain ~pure:true
ce.const_entry_body (fun ((body, ctx), side_eff) ->
let body, ctx',_ = inline_side_effects env body ctx side_eff in
- (body, ctx'), []);
+ (body, ctx'), empty_seff);
}
let inline_side_effects env body side_eff =
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 89b5fc40e..075389ea5 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -12,6 +12,8 @@ open Environ
open Declarations
open Entries
+type side_effects
+
val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry ->
constant_def * types * constant_universes
@@ -29,7 +31,15 @@ val inline_entry_side_effects :
{!Entries.const_entry_body} field. It is meant to get a term out of a not
yet type checked proof. *)
-val uniq_seff : side_effects -> side_effects
+val empty_seff : side_effects
+val add_seff : side_effect -> side_effects -> side_effects
+val concat_seff : side_effects -> side_effects -> side_effects
+(** [concat_seff e1 e2] adds the side-effects of [e1] to [e2], i.e. effects in
+ [e1] must be more recent than those of [e2]. *)
+val uniq_seff : side_effects -> side_effect list
+(** Return the list of individual side-effects in the order of their
+ creation. *)
+
val equal_eff : side_effect -> side_effect -> bool
val translate_constant :