From 3502cc7c3bbad154dbfe76558d411d2c76109668 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 5 Mar 2017 17:30:03 +0100 Subject: [future] Remove unused parameter greedy. It was always set to `greedy:true`. --- kernel/term_typing.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 3a0d1a2a5e..a63eb33766 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -191,7 +191,7 @@ let infer_declaration ~trust env kn dcl = let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let tyj = infer_type env typ in let proofterm = - Future.chain ~greedy:true ~pure:true body (fun ((body,uctx),side_eff) -> + Future.chain ~pure:true body (fun ((body,uctx),side_eff) -> let body, uctx, signatures = inline_side_effects env body uctx side_eff in let valid_signatures = check_signatures trust signatures in @@ -416,7 +416,7 @@ let export_side_effects mb env ce = let { const_entry_body = body } = c in let _, eff = Future.force body in let ce = DefinitionEntry { c with - const_entry_body = Future.chain ~greedy:true ~pure:true body + const_entry_body = Future.chain ~pure:true body (fun (b_ctx, _) -> b_ctx, []) } in let not_exists (c,_,_,_) = try ignore(Environ.lookup_constant c env); false @@ -498,7 +498,7 @@ let translate_local_def mb env id centry = let translate_mind env kn mie = Indtypes.check_inductive env kn mie let inline_entry_side_effects env ce = { ce with - const_entry_body = Future.chain ~greedy:true ~pure:true + 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'), []); -- cgit v1.2.3 From 3a050f305293676ccf66d415ab386d9521f0f765 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 23 Feb 2017 04:04:33 +0100 Subject: [safe_string] kernel/term_typing No functional change, we create the new string beforehand and `id_of_string` will become a noop with `-safe-string`. --- kernel/term_typing.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 3a0d1a2a5e..b9cf8101da 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -76,8 +76,7 @@ let inline_side_effects env body ctx side_eff = let cbl = List.filter not_exists cbl in let cname c = let name = string_of_con c in - for i = 0 to String.length name - 1 do - if name.[i] == '.' || name.[i] == '#' then name.[i] <- '_' done; + let name = String.map (fun c -> if c == '.' || c == '#' then '_' else c) name in Name (id_of_string name) in let rec sub c i x = match kind_of_term x with | Const (c', _) when eq_constant c c' -> mkRel i -- cgit v1.2.3 From 09c856a3bcb7369244202ed94db247f7abe84dad Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 21 Mar 2017 14:29:56 +0100 Subject: Do not typecheck twice the type of opaque constants. I believe an unwanted shadowing was introduced by a4043608f704f0. --- kernel/term_typing.ml | 41 +++++++++++++++++------------------------ 1 file changed, 17 insertions(+), 24 deletions(-) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 749b5dbafa..2d55803475 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -22,24 +22,6 @@ open Entries open Typeops open Fast_typeops -let constrain_type env j poly subst = function - | `None -> - if not poly then (* Old-style polymorphism *) - make_polymorphic_if_constant_for_ind env j - else RegularArity (Vars.subst_univs_level_constr subst j.uj_type) - | `Some t -> - let tj = infer_type env t in - let _ = judge_of_cast env j DEFAULTcast tj in - assert (eq_constr t tj.utj_val); - RegularArity (Vars.subst_univs_level_constr subst t) - | `SomeWJ (t, tj) -> - let tj = infer_type env t in - let _ = judge_of_cast env j DEFAULTcast tj in - assert (eq_constr t tj.utj_val); - RegularArity (Vars.subst_univs_level_constr subst t) - -let map_option_typ = function None -> `None | Some x -> `Some x - (* Insertion of constants and parameters in environment. *) let mk_pure_proof c = (c, Univ.ContextSet.empty), [] @@ -193,15 +175,16 @@ let infer_declaration ~trust env kn dcl = let body, uctx, signatures = inline_side_effects env body uctx side_eff in let valid_signatures = check_signatures trust signatures in - let env' = push_context_set uctx env in + let env = push_context_set uctx env in let j = - let body,env',ectx = skip_trusted_seff valid_signatures body env' in - let j = infer env' body in + let body,env,ectx = skip_trusted_seff valid_signatures body env in + let j = infer env body in unzip ectx j in let j = hcons_j j in let subst = Univ.LMap.empty in - let _typ = constrain_type env' j c.const_entry_polymorphic subst - (`SomeWJ (typ,tyj)) in + let _ = judge_of_cast env j DEFAULTcast tyj in + assert (eq_constr typ tyj.utj_val); + let _typ = RegularArity (Vars.subst_univs_level_constr subst typ) in feedback_completion_typecheck feedback_id; j.uj_val, uctx) in let def = OpaqueDef (Opaqueproof.create proofterm) in @@ -221,7 +204,17 @@ let infer_declaration ~trust env kn dcl = let usubst, univs = Univ.abstract_universes abstract (Univ.ContextSet.to_context ctx) in let j = infer env body in - let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in + let typ = match typ with + | None -> + if not c.const_entry_polymorphic then (* Old-style polymorphism *) + make_polymorphic_if_constant_for_ind env j + else RegularArity (Vars.subst_univs_level_constr usubst j.uj_type) + | Some t -> + let tj = infer_type env t in + let _ = judge_of_cast env j DEFAULTcast tj in + assert (eq_constr t tj.utj_val); + RegularArity (Vars.subst_univs_level_constr usubst t) + in let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in let def = if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty))) -- cgit v1.2.3 From 6d416ea54fd26987188858bcf80461247b002a09 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 21 Mar 2017 14:30:58 +0100 Subject: Add a few comments in term_typing.ml. --- kernel/term_typing.ml | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 2d55803475..b7597ba7fb 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -164,6 +164,10 @@ let infer_declaration ~trust env kn dcl = let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in Undef nl, RegularArity t, None, poly, univs, false, ctx + (** Definition [c] is opaque (Qed), non polymorphic and with a specified type, + so we delay the typing and hash consing of its body. + Remark: when the universe quantification is given explicitly, we could + delay even in the polymorphic case. *) | DefinitionEntry ({ const_entry_type = Some typ; const_entry_opaque = true; const_entry_polymorphic = false} as c) -> @@ -192,6 +196,7 @@ let infer_declaration ~trust env kn dcl = c.const_entry_universes, c.const_entry_inline_code, c.const_entry_secctx + (** Other definitions have to be processed immediately. *) | DefinitionEntry c -> let { const_entry_type = typ; const_entry_opaque = opaque } = c in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in -- cgit v1.2.3 From ea8185d872f242f8ebf4274ebe550ed81107150a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 12 Mar 2017 19:57:48 +0100 Subject: Making the side_effects type opaque. We move it from Entries to Term_typing and export the few functions needed to manipulate it in this module. --- kernel/term_typing.ml | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index b7597ba7fb..24da308b4f 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -37,13 +37,20 @@ let equal_eff e1 e2 = cl1 cl2 | _ -> false -let rec uniq_seff = function +type side_effects = side_effect list + +let rec uniq_seff_aux = function | [] -> [] - | x :: xs -> x :: uniq_seff (List.filter (fun y -> not (equal_eff x y)) xs) + | x :: xs -> x :: uniq_seff_aux (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)) +let uniq_seff_rev l = List.rev (uniq_seff_aux (List.rev l)) +let uniq_seff l = List.rev (uniq_seff_aux l) + +let empty_seff = [] +let add_seff x xs = if List.mem_f equal_eff x xs then xs else x :: xs +let concat_seff xs ys = List.fold_right add_seff xs ys let inline_side_effects env body ctx side_eff = let handle_sideff (t,ctx,sl) { eff = se; from_env = mb } = @@ -97,7 +104,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 *) @@ -427,7 +434,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, _ -> -- cgit v1.2.3 From ee1546dc6686e888cc8da5f9442bcf788544dd0e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 12 Mar 2017 20:16:43 +0100 Subject: Using a dedicated datastructure for side effect ordering. We were doing fishy things in the Term_typing file, where side-effects were not considered in the right uniquization order because of the uniq_seff_rev function. It probably did not matter after a9b76df because effects were (mostly) uniquize upfront, but this is not clear because of the use of the transparente API in the module. Now everything has to go through the opaque API, so that a proper dependence order is ensured. --- kernel/term_typing.ml | 66 ++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 49 insertions(+), 17 deletions(-) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 24da308b4f..6ce14c853d 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -24,8 +24,6 @@ open Fast_typeops (* 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 @@ -37,20 +35,54 @@ let equal_eff e1 e2 = cl1 cl2 | _ -> false -type side_effects = side_effect list +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 rec uniq_seff_aux = function - | [] -> [] - | x :: xs -> x :: uniq_seff_aux (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_rev l = List.rev (uniq_seff_aux (List.rev l)) -let uniq_seff l = List.rev (uniq_seff_aux l) +let empty_seff = SideEffects.empty +let add_seff = SideEffects.add +let concat_seff = SideEffects.concat -let empty_seff = [] -let add_seff x xs = if List.mem_f equal_eff x xs then xs else x :: xs -let concat_seff xs ys = List.fold_right add_seff xs ys +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 } = @@ -388,7 +420,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 = @@ -422,7 +454,7 @@ let export_side_effects mb env ce = let _, eff = Future.force body in let ce = DefinitionEntry { c with const_entry_body = Future.chain ~greedy:true ~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 @@ -507,7 +539,7 @@ let inline_entry_side_effects env ce = { ce with const_entry_body = Future.chain ~greedy:true ~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 = -- cgit v1.2.3