diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-27 14:39:14 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-27 14:39:14 +0000 |
commit | b3e1879a09c3623c7a04858a7421b316abd65293 (patch) | |
tree | 7b02b6dd43c7febef378d1f8094d344327ad6457 /kernel | |
parent | fb304bfac1872d724c814fcd860c691582492568 (diff) |
Minor cleanup around Term_typing
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16253 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/cooking.ml | 8 | ||||
-rw-r--r-- | kernel/cooking.mli | 10 | ||||
-rw-r--r-- | kernel/safe_typing.ml | 11 | ||||
-rw-r--r-- | kernel/term_typing.ml | 55 | ||||
-rw-r--r-- | kernel/term_typing.mli | 27 |
5 files changed, 40 insertions, 71 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index e8e35ee85..0ff7d64f0 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -119,6 +119,12 @@ type recipe = { d_abstract : named_context; d_modlist : work_list } +type inline = bool + +type result = + constant_def * constant_type * Univ.constraints * inline + * Sign.section_context option + let on_body f = function | Undef inl -> Undef inl | Def cs -> Def (Lazyconstr.from_val (f (Lazyconstr.force cs))) @@ -151,4 +157,4 @@ let cook_constant env r = let j = make_judge (constr_of_def body) typ in Typeops.make_polymorphic_if_constant_for_ind env j in - (body, typ, cb.const_constraints, cb.const_inline_code, const_hyps) + (body, typ, cb.const_constraints, cb.const_inline_code, Some const_hyps) diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 03acb87a9..d6280e119 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -21,9 +21,13 @@ type recipe = { d_abstract : Sign.named_context; d_modlist : work_list } -val cook_constant : - env -> recipe -> - constant_def * constant_type * constraints * bool * Sign.section_context +type inline = bool + +type result = + constant_def * constant_type * constraints * inline + * Sign.section_context option + +val cook_constant : env -> recipe -> result (** {6 Utility functions used in module [Discharge]. } *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 932e43163..fa565fa34 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -65,7 +65,6 @@ open Declarations open Environ open Entries open Typeops -open Term_typing open Modops open Subtyping open Mod_typing @@ -247,13 +246,13 @@ let safe_push_named (id,_,_ as d) env = Environ.push_named d env let push_named_def (id,b,topt) senv = - let (c,typ,cst) = translate_local_def senv.env (b,topt) in + let (c,typ,cst) = Term_typing.translate_local_def senv.env (b,topt) in let senv' = add_constraints cst senv in let env'' = safe_push_named (id,Some c,typ) senv'.env in (cst, {senv' with env=env''}) let push_named_assum (id,t) senv = - let (t,cst) = translate_local_assum senv.env t in + let (t,cst) = Term_typing.translate_local_assum senv.env t in let senv' = add_constraints cst senv in let env'' = safe_push_named (id,None,t) senv'.env in (cst, {senv' with env=env''}) @@ -268,9 +267,9 @@ type global_declaration = let add_constant dir l decl senv = let kn = make_con senv.modinfo.modpath dir l in let cb = match decl with - | ConstantEntry ce -> translate_constant senv.env kn ce + | ConstantEntry ce -> Term_typing.translate_constant senv.env ce | GlobalRecipe r -> - let cb = translate_recipe senv.env kn r in + let cb = Term_typing.translate_recipe senv.env r in if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb in let senv' = add_field (l,SFBconst cb) (C kn) senv in @@ -295,7 +294,7 @@ let add_mind dir l mie senv = anomaly (Pp.str "the label of inductive packet and its first inductive \ type do not match"); let kn = make_mind senv.modinfo.modpath dir l in - let mib = translate_mind senv.env kn mie in + let mib = Term_typing.translate_mind senv.env kn mie in let mib = match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib in let senv' = add_field (l,SFBmind mib) (I kn) senv in diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 3ec0da457..c70a3f2eb 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -20,7 +20,6 @@ open Term open Declarations open Environ open Entries -open Indtypes open Typeops let constrain_type env j cst1 = function @@ -29,9 +28,9 @@ let constrain_type env j cst1 = function | Some t -> let (tj,cst2) = infer_type env t in let (_,cst3) = judge_of_cast env j DEFAULTcast tj in - assert (eq_constr t tj.utj_val); - let cstrs = union_constraints (union_constraints cst1 cst2) cst3 in - NonPolymorphicType t, cstrs + assert (eq_constr t tj.utj_val); + let cstrs = union_constraints (union_constraints cst1 cst2) cst3 in + NonPolymorphicType t, cstrs let local_constrain_type env j cst1 = function | None -> @@ -52,42 +51,10 @@ let translate_local_assum env t = let t = Typeops.assumption_of_judgment env j in (t,cst) -(* - -(* Same as push_named, but check that the variable is not already - there. Should *not* be done in Environ because tactics add temporary - hypothesis many many times, and the check performed here would - cost too much. *) -let safe_push_named (id,_,_ as d) env = - let _ = - try - let _ = lookup_named id env in - error ("Identifier "^Id.to_string id^" already defined.") - with Not_found -> () in - push_named d env - -let push_named_def = push_rel_or_named_def safe_push_named -let push_rel_def = push_rel_or_named_def push_rel - -let push_rel_or_named_assum push (id,t) env = - let (j,cst) = safe_infer env t in - let t = Typeops.assumption_of_judgment env j in - let env' = add_constraints cst env in - let env'' = push (id,None,t) env' in - (cst,env'') - -let push_named_assum = push_rel_or_named_assum push_named -let push_rel_assum d env = snd (push_rel_or_named_assum push_rel d env) - -let push_rels_with_univ vars env = - List.fold_left (fun env nvar -> push_rel_assum nvar env) env vars -*) - (* Insertion of constants and parameters in environment. *) -let infer_declaration env dcl = - match dcl with +let infer_declaration env = function | DefinitionEntry c -> let (j,cst) = infer env c.const_entry_body in let j = @@ -113,7 +80,7 @@ let global_vars_set_constant_type env = function (fun t c -> Id.Set.union (global_vars_set env t) c)) ctx ~init:Id.Set.empty -let build_constant_declaration env kn (def,typ,cst,inline_code,ctx) = +let build_constant_declaration env (def,typ,cst,inline_code,ctx) = let hyps = let inferred = let ids_typ = global_vars_set_constant_type env typ in @@ -144,14 +111,12 @@ let build_constant_declaration env kn (def,typ,cst,inline_code,ctx) = (*s Global and local constant declaration. *) -let translate_constant env kn ce = - build_constant_declaration env kn (infer_declaration env ce) +let translate_constant env ce = + build_constant_declaration env (infer_declaration env ce) -let translate_recipe env kn r = - build_constant_declaration env kn - (let def,typ,cst,inline,hyps = Cooking.cook_constant env r in - def,typ,cst,inline,Some hyps) +let translate_recipe env r = + build_constant_declaration env (Cooking.cook_constant env r) (* Insertion of inductive types. *) -let translate_mind env kn mie = check_inductive env kn mie +let translate_mind env kn mie = Indtypes.check_inductive env kn mie diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index d001a258e..cc6025dab 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -9,29 +9,24 @@ open Names open Term open Univ -open Declarations -open Inductive open Environ +open Declarations open Entries -open Typeops val translate_local_def : env -> constr * types option -> - constr * types * Univ.constraints - -val translate_local_assum : env -> types -> - types * Univ.constraints - -val infer_declaration : env -> constant_entry -> - constant_def * constant_type * constraints * bool * Sign.section_context option + constr * types * constraints -val build_constant_declaration : env -> 'a -> - constant_def * constant_type * constraints * bool * Sign.section_context option -> - constant_body +val translate_local_assum : env -> types -> types * constraints -val translate_constant : env -> constant -> constant_entry -> constant_body +val translate_constant : env -> constant_entry -> constant_body val translate_mind : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body -val translate_recipe : - env -> constant -> Cooking.recipe -> constant_body +val translate_recipe : env -> Cooking.recipe -> constant_body + + +(** Internal functions, mentioned here for debug purpose only *) + +val infer_declaration : env -> constant_entry -> Cooking.result +val build_constant_declaration : env -> Cooking.result -> constant_body |