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 /proofs | |
| 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 'proofs')
| -rw-r--r-- | proofs/logic.ml | 4 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 3 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 14 |
3 files changed, 17 insertions, 4 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index c48882c1a1..45ef3efadf 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -347,10 +347,10 @@ let rec mk_refgoals sigma goal goalacc conclty trm = check_typability env sigma ty; check_conv_leq_goal env sigma trm ty conclty; let res = mk_refgoals sigma goal goalacc ty t in - (** we keep the casts (in particular VMcast) except + (** we keep the casts (in particular VMcast and NATIVEcast) except when they are annotating metas *) if isMeta t then begin - assert (k != VMcast); + assert (k != VMcast && k != NATIVEcast); res end else let (gls,cty,sigma,trm) = res in diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index c5a1902280..ed985f2927 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -270,7 +270,8 @@ let close_proof () = (fun (c,t) -> { Entries.const_entry_body = c; const_entry_secctx = section_vars; const_entry_type = Some t; - const_entry_opaque = true }) + const_entry_opaque = true; + const_entry_inline_code = false }) proofs_and_types in let { compute_guard=cg ; strength=str ; hook=hook } = diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index c4c821a9e5..91ef038ee5 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -28,6 +28,9 @@ let cbv_vm env _ c = let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in Vnorm.cbv_vm env c ctyp +let cbv_native env _ c = + let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in + Nativenorm.native_norm env c ctyp let set_strategy_one ref l = let k = @@ -206,7 +209,16 @@ let rec reduction_of_red_expr = function let redfun = contextually b lp vmfun in (redfun, VMcast) | CbvVm None -> (cbv_vm, VMcast) - + | CbvNative (Some lp) -> + let b = is_reference (snd lp) in + let lp = out_with_occurrences lp in + let nativefun _ env map c = + let tpe = Retyping.get_type_of env map c in + Nativenorm.native_norm env c tpe + in + let redfun = contextually b lp nativefun in + (redfun, NATIVEcast) + | CbvNative None -> (cbv_native, NATIVEcast) let subst_flags subs flags = { flags with rConst = List.map subs flags.rConst } |