From 4457e6d75affd20c1c13c0d798c490129525bcb5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 4 Jul 2017 13:38:22 +0200 Subject: More precise type for universe entries. We use an algebraic type instead of a pair of a boolean and the corresponding data. For now, this is isomorphic, but this allows later change in the structure. --- kernel/term_typing.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/term_typing.mli') diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 77d126074f..29c9918373 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -15,7 +15,7 @@ open Entries type side_effects val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry -> - constant_def * types * constant_universes + constant_def * types * Univ.universe_context val translate_local_assum : env -> types -> types -- cgit v1.2.3 From 3c6679676c3963b7c3ec7c1eadbf24ae70311408 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 14 Jul 2017 15:43:40 +0200 Subject: More precise type of entries capturing their lack of side-effects. We sprinkle a few GADTs in the kernel in order to statically ensure that entries are pure, so that we get stronger invariants. --- kernel/term_typing.mli | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) (limited to 'kernel/term_typing.mli') diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 29c9918373..082ed7ed0d 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -14,7 +14,11 @@ open Entries type side_effects -val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry -> +type _ trust = +| Pure : unit trust +| SideEffects : structure_body -> side_effects trust + +val translate_local_def : 'a trust -> env -> Id.t -> 'a definition_entry -> constant_def * types * Univ.universe_context val translate_local_assum : env -> types -> types @@ -43,7 +47,7 @@ val uniq_seff : side_effects -> side_effect list val equal_eff : side_effect -> side_effect -> bool val translate_constant : - structure_body -> env -> constant -> side_effects constant_entry -> + 'a trust -> env -> constant -> 'a constant_entry -> constant_body type side_effect_role = @@ -51,7 +55,7 @@ type side_effect_role = | Schema of inductive * string type exported_side_effect = - constant * constant_body * side_effects constant_entry * side_effect_role + constant * constant_body * unit constant_entry * side_effect_role (* Given a constant entry containing side effects it exports them (either * by re-checking them or trusting them). Returns the constant bodies to @@ -59,10 +63,10 @@ type exported_side_effect = * needs to be translated as usual after this step. *) val export_side_effects : structure_body -> env -> side_effects constant_entry -> - exported_side_effect list * side_effects constant_entry + exported_side_effect list * unit constant_entry val constant_entry_of_side_effect : - constant_body -> seff_env -> side_effects constant_entry + constant_body -> seff_env -> unit constant_entry val translate_mind : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body @@ -71,8 +75,8 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : trust:structure_body -> env -> constant option -> - side_effects constant_entry -> Cooking.result +val infer_declaration : trust:'a trust -> env -> constant option -> + 'a constant_entry -> Cooking.result val build_constant_declaration : constant -> env -> Cooking.result -> constant_body -- cgit v1.2.3 From ce830b204ad52f8b3655d2cb4672662120d83101 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 16 Jul 2017 00:05:03 +0200 Subject: Further simplication: do not recreate entries for side-effects. This is actually useless, the code does not depend on the value of the entry for side-effects. --- kernel/term_typing.mli | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) (limited to 'kernel/term_typing.mli') diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 082ed7ed0d..5914c4a954 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -55,7 +55,7 @@ type side_effect_role = | Schema of inductive * string type exported_side_effect = - constant * constant_body * unit constant_entry * side_effect_role + constant * constant_body * side_effect_role (* Given a constant entry containing side effects it exports them (either * by re-checking them or trusting them). Returns the constant bodies to @@ -65,9 +65,6 @@ val export_side_effects : structure_body -> env -> side_effects constant_entry -> exported_side_effect list * unit constant_entry -val constant_entry_of_side_effect : - constant_body -> seff_env -> unit constant_entry - val translate_mind : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body -- cgit v1.2.3 From 665256fec8465ff0adb943063c25f07a6ca54618 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 18 Jul 2017 18:16:43 +0200 Subject: Statically ensuring that inlined entries out of the kernel have no effects. This was an easy to prove property that I somehow overlooked. --- kernel/term_typing.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/term_typing.mli') diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 5914c4a954..24153343e7 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -30,7 +30,7 @@ val inline_side_effects : env -> constr -> side_effects -> constr redexes. *) val inline_entry_side_effects : - env -> side_effects definition_entry -> side_effects definition_entry + env -> side_effects definition_entry -> unit definition_entry (** Same as {!inline_side_effects} but applied to entries. Only modifies the {!Entries.const_entry_body} field. It is meant to get a term out of a not yet type checked proof. *) -- cgit v1.2.3