diff options
| author | mdenes | 2013-01-22 17:37:00 +0000 |
|---|---|---|
| committer | mdenes | 2013-01-22 17:37:00 +0000 |
| commit | 6b908b5185a55a27a82c2b0fce4713812adde156 (patch) | |
| tree | c2857724d8b22ae3d7a91b3a683a57206caf9b54 /kernel/term_typing.ml | |
| parent | 62ce65dadb0afb8815b26069246832662846c7ec (diff) | |
New implementation of the conversion test, using normalization by evaluation to
native OCaml code.
Warning: the "retroknowledge" mechanism has not been ported to the native
compiler, because integers and persistent arrays will ultimately be defined as
primitive constructions. Until then, computation on numbers may be faster using
the VM, since it takes advantage of machine integers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index ccb6a4a7d7..1cd006f25a 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -99,11 +99,11 @@ let infer_declaration env dcl = then OpaqueDef (Declarations.opaque_from_val j.uj_val) else Def (Declarations.from_val j.uj_val) in - def, typ, cst, c.const_entry_secctx + def, typ, cst, c.const_entry_inline_code, c.const_entry_secctx | ParameterEntry (ctx,t,nl) -> let (j,cst) = infer env t in let t = hcons_constr (Typeops.assumption_of_judgment env j) in - Undef nl, NonPolymorphicType t, cst, ctx + Undef nl, NonPolymorphicType t, cst, false, ctx let global_vars_set_constant_type env = function | NonPolymorphicType t -> global_vars_set env t @@ -113,7 +113,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,ctx) = +let build_constant_declaration env kn (def,typ,cst,inline_code,ctx) = let hyps = let inferred = let ids_typ = global_vars_set_constant_type env typ in @@ -138,7 +138,9 @@ let build_constant_declaration env kn (def,typ,cst,ctx) = const_body = def; const_type = typ; const_body_code = tps; - const_constraints = cst } + const_constraints = cst; + const_native_name = ref NotLinked; + const_inline_code = inline_code } (*s Global and local constant declaration. *) @@ -147,8 +149,8 @@ let translate_constant env kn ce = let translate_recipe env kn r = build_constant_declaration env kn - (let def,typ,cst,hyps = Cooking.cook_constant env r in - def,typ,cst,Some hyps) + (let def,typ,cst,inline,hyps = Cooking.cook_constant env r in + def,typ,cst,inline,Some hyps) (* Insertion of inductive types. *) |