diff options
author | Arnaud Spiwack <arnaud@spiwack.net> | 2015-07-24 08:46:09 +0200 |
---|---|---|
committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-09-25 10:41:41 +0200 |
commit | e8bad8abc7be351a34fdf9770409bbab14bcd6a9 (patch) | |
tree | 00ca0103024f39e5943dcce5a89e9283708ae323 /kernel | |
parent | 8f64e84a3560bcf668b00ac93ab33542456a9bda (diff) |
Propagate `Guarded` flag from syntax to kernel.
The path is quite a bit of a maze, this commit is not as simple as it ought to be. Something more robust than a boolean should be used here.
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/fast_typeops.ml | 69 | ||||
-rw-r--r-- | kernel/fast_typeops.mli | 6 | ||||
-rw-r--r-- | kernel/safe_typing.ml | 13 | ||||
-rw-r--r-- | kernel/safe_typing.mli | 4 | ||||
-rw-r--r-- | kernel/term_typing.ml | 28 | ||||
-rw-r--r-- | kernel/term_typing.mli | 8 |
6 files changed, 67 insertions, 61 deletions
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index 358795666..8c14f5e04 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -326,7 +326,7 @@ let type_fixpoint env lna lar vdef vdeft = (* ATTENTION : faudra faire le typage du contexte des Const, Ind et Constructsi un jour cela devient des constructions arbitraires et non plus des variables *) -let rec execute env cstr = +let rec execute ~chkguard env cstr = match kind_of_term cstr with (* Atomic terms *) | Sort (Prop c) -> @@ -345,12 +345,12 @@ let rec execute env cstr = judge_of_constant env c | Proj (p, c) -> - let ct = execute env c in + let ct = execute ~chkguard env c in judge_of_projection env p c ct (* Lambda calculus operators *) | App (f,args) -> - let argst = execute_array env args in + let argst = execute_array ~chkguard env args in let ft = match kind_of_term f with | Ind ind when Environ.template_polymorphic_pind ind env -> @@ -363,7 +363,7 @@ let rec execute env cstr = judge_of_constant_knowing_parameters env cst args | _ -> (* Full or no sort-polymorphism *) - execute env f + execute ~chkguard env f in judge_of_apply env f ft args argst @@ -371,25 +371,25 @@ let rec execute env cstr = | Lambda (name,c1,c2) -> let _ = execute_is_type env c1 in let env1 = push_rel (name,None,c1) env in - let c2t = execute env1 c2 in + let c2t = execute ~chkguard env1 c2 in judge_of_abstraction env name c1 c2t | Prod (name,c1,c2) -> - let vars = execute_is_type env c1 in + let vars = execute_is_type ~chkguard env c1 in let env1 = push_rel (name,None,c1) env in - let vars' = execute_is_type env1 c2 in + let vars' = execute_is_type ~chkguard env1 c2 in judge_of_product env name vars vars' | LetIn (name,c1,c2,c3) -> - let c1t = execute env c1 in + let c1t = execute ~chkguard env c1 in let _c2s = execute_is_type env c2 in let _ = judge_of_cast env c1 c1t DEFAULTcast c2 in let env1 = push_rel (name,Some c1,c2) env in - let c3t = execute env1 c3 in + let c3t = execute ~chkguard env1 c3 in subst1 c1 c3t | Cast (c,k,t) -> - let ct = execute env c in + let ct = execute ~chkguard env c in let _ts = execute_type env t in let _ = judge_of_cast env c ct k t in t @@ -402,20 +402,20 @@ let rec execute env cstr = judge_of_constructor env c | Case (ci,p,c,lf) -> - let ct = execute env c in - let pt = execute env p in - let lft = execute_array env lf in + let ct = execute ~chkguard env c in + let pt = execute ~chkguard env p in + let lft = execute_array ~chkguard env lf in judge_of_case env ci p pt c ct lf lft | Fix ((vn,i as vni),recdef) -> - let (fix_ty,recdef') = execute_recdef env recdef i in + let (fix_ty,recdef') = execute_recdef ~chkguard env recdef i in let fix = (vni,recdef') in - check_fix env ~chk:true fix; fix_ty + check_fix env ~chk:chkguard fix; fix_ty | CoFix (i,recdef) -> - let (fix_ty,recdef') = execute_recdef env recdef i in + let (fix_ty,recdef') = execute_recdef ~chkguard env recdef i in let cofix = (i,recdef') in - check_cofix env ~chk:true cofix; fix_ty + check_cofix env ~chk:chkguard cofix; fix_ty (* Partial proofs: unsupported by the kernel *) | Meta _ -> @@ -424,38 +424,41 @@ let rec execute env cstr = | Evar _ -> anomaly (Pp.str "the kernel does not support existential variables") -and execute_is_type env constr = - let t = execute env constr in +and execute_is_type ~chkguard env constr = + let t = execute ~chkguard env constr in check_type env constr t -and execute_type env constr = - let t = execute env constr in +and execute_type ~chkguard env constr = + let t = execute ~chkguard env constr in type_judgment env constr t -and execute_recdef env (names,lar,vdef) i = - let lart = execute_array env lar in +and execute_recdef ~chkguard env (names,lar,vdef) i = + let lart = execute_array ~chkguard env lar in let lara = Array.map2 (assumption_of_judgment env) lar lart in let env1 = push_rec_types (names,lara,vdef) env in - let vdeft = execute_array env1 vdef in + let vdeft = execute_array ~chkguard env1 vdef in let () = type_fixpoint env1 names lara vdef vdeft in (lara.(i),(names,lara,vdef)) -and execute_array env = Array.map (execute env) +and execute_array ~chkguard env = Array.map (execute ~chkguard env) (* Derived functions *) -let infer env constr = - let t = execute env constr in +let infer ~chkguard env constr = + let t = execute ~chkguard env constr in make_judge constr t let infer = if Flags.profile then let infer_key = Profile.declare_profile "Fast_infer" in - Profile.profile2 infer_key infer - else infer + Profile.profile3 infer_key (fun a b c -> infer ~chkguard:a b c) + else (fun a b c -> infer ~chkguard:a b c) -let infer_type env constr = - execute_type env constr +(* Restores the labels of [infer] lost to profiling. *) +let infer ~chkguard env t = infer chkguard env t -let infer_v env cv = - let jv = execute_array env cv in +let infer_type ~chkguard env constr = + execute_type ~chkguard env constr + +let infer_v ~chkguard env cv = + let jv = execute_array ~chkguard env cv in make_judgev cv jv diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli index 90d9c55f1..98dbefad1 100644 --- a/kernel/fast_typeops.mli +++ b/kernel/fast_typeops.mli @@ -18,6 +18,6 @@ open Environ *) -val infer : env -> constr -> unsafe_judgment -val infer_v : env -> constr array -> unsafe_judgment array -val infer_type : env -> types -> unsafe_type_judgment +val infer : chkguard:bool -> env -> constr -> unsafe_judgment +val infer_v : chkguard:bool -> env -> constr array -> unsafe_judgment array +val infer_type : chkguard:bool -> env -> types -> unsafe_type_judgment diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d9adca0c9..18d897817 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -332,8 +332,8 @@ let safe_push_named (id,_,_ as d) env = Environ.push_named d env -let push_named_def (id,de) senv = - let c,typ,univs = Term_typing.translate_local_def senv.env id de in +let push_named_def ~chkguard (id,de) senv = + let c,typ,univs = Term_typing.translate_local_def ~chkguard senv.env id de in let senv' = push_context univs senv in let c, senv' = match c with | Def c -> Mod_subst.force_constr c, senv' @@ -346,9 +346,9 @@ let push_named_def (id,de) senv = let env'' = safe_push_named (id,Some c,typ) senv'.env in {senv' with env=env''} -let push_named_assum ((id,t),ctx) senv = +let push_named_assum ~chkguard ((id,t),ctx) senv = let senv' = push_context_set ctx senv in - let t = Term_typing.translate_local_assum senv'.env t in + let t = Term_typing.translate_local_assum ~chkguard senv'.env t in let env'' = safe_push_named (id,None,t) senv'.env in {senv' with env=env''} @@ -439,13 +439,14 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver } (** Insertion of constants and parameters in environment *) type global_declaration = - | ConstantEntry of Entries.constant_entry + | ConstantEntry of Entries.constant_entry * bool (* check guard *) | GlobalRecipe of Cooking.recipe let add_constant dir l decl senv = let kn = make_con senv.modpath dir l in let cb = match decl with - | ConstantEntry ce -> Term_typing.translate_constant senv.env kn ce + | ConstantEntry (ce,chkguard) -> + Term_typing.translate_constant ~chkguard senv.env kn ce | GlobalRecipe r -> let cb = Term_typing.translate_recipe senv.env kn r in if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index a57fb108c..80b9bb495 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -57,14 +57,16 @@ val is_joined_environment : safe_environment -> bool (** Insertion of local declarations (Local or Variables) *) val push_named_assum : + chkguard:bool -> (Id.t * Term.types) Univ.in_universe_context_set -> safe_transformer0 val push_named_def : + chkguard:bool -> Id.t * Entries.definition_entry -> safe_transformer0 (** Insertion of global axioms or definitions *) type global_declaration = - | ConstantEntry of Entries.constant_entry + | ConstantEntry of Entries.constant_entry * bool (* chkguard *) | GlobalRecipe of Cooking.recipe val add_constant : diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index a316b4492..539305ed1 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -23,18 +23,18 @@ open Entries open Typeops open Fast_typeops -let constrain_type env j poly subst = function +let constrain_type ~chkguard 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 tj = infer_type ~chkguard 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 tj = infer_type ~chkguard 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) @@ -101,11 +101,11 @@ let hcons_j j = let feedback_completion_typecheck = Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete) -let infer_declaration env kn dcl = +let infer_declaration ~chkguard env kn dcl = match dcl with | ParameterEntry (ctx,poly,(t,uctx),nl) -> let env = push_context uctx env in - let j = infer env t in + let j = infer ~chkguard env t in let abstract = poly && not (Option.is_empty kn) in let usubst, univs = Univ.abstract_universes abstract uctx in let c = Typeops.assumption_of_judgment env j in @@ -122,7 +122,7 @@ let infer_declaration env kn dcl = Future.chain ~greedy:true ~pure:true body (fun ((body, ctx),side_eff) -> let body = handle_side_effects env body side_eff in let env' = push_context_set ctx env in - let j = infer env' body in + let j = infer ~chkguard env' body in let j = hcons_j j in let subst = Univ.LMap.empty in let _typ = constrain_type env' j c.const_entry_polymorphic subst @@ -143,8 +143,8 @@ let infer_declaration env kn dcl = let body = handle_side_effects env body side_eff in let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in let usubst, univs = Univ.abstract_universes abstract c.const_entry_universes in - let j = infer env body in - let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in + let j = infer ~chkguard env body in + let typ = constrain_type ~chkguard env j c.const_entry_polymorphic usubst (map_option_typ typ) 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))) @@ -266,20 +266,20 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) (*s Global and local constant declaration. *) -let translate_constant env kn ce = - build_constant_declaration kn env (infer_declaration env (Some kn) ce) +let translate_constant ~chkguard env kn ce = + build_constant_declaration kn env (infer_declaration ~chkguard env (Some kn) ce) -let translate_local_assum env t = - let j = infer env t in +let translate_local_assum ~chkguard env t = + let j = infer ~chkguard env t in let t = Typeops.assumption_of_judgment env j in t let translate_recipe env kn r = build_constant_declaration kn env (Cooking.cook_constant env r) -let translate_local_def env id centry = +let translate_local_def ~chkguard env id centry = let def,typ,proj,poly,univs,inline_code,ctx = - infer_declaration env None (DefinitionEntry centry) in + infer_declaration ~chkguard env None (DefinitionEntry centry) in let typ = type_of_constant_type env typ in def, typ, univs diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 1b54b1ea1..a71587f0f 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -12,10 +12,10 @@ open Environ open Declarations open Entries -val translate_local_def : env -> Id.t -> definition_entry -> +val translate_local_def : chkguard:bool -> env -> Id.t -> definition_entry -> constant_def * types * constant_universes -val translate_local_assum : env -> types -> types +val translate_local_assum : chkguard:bool -> env -> types -> types val mk_pure_proof : constr -> proof_output @@ -28,7 +28,7 @@ val handle_entry_side_effects : env -> definition_entry -> definition_entry {!Entries.const_entry_body} field. It is meant to get a term out of a not yet type checked proof. *) -val translate_constant : env -> constant -> constant_entry -> constant_body +val translate_constant : chkguard:bool -> env -> constant -> constant_entry -> constant_body val translate_mind : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body @@ -37,7 +37,7 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : env -> constant option -> +val infer_declaration : chkguard:bool -> env -> constant option -> constant_entry -> Cooking.result val build_constant_declaration : |