diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-12 22:56:43 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-12 22:56:43 +0000 |
commit | 33c0d04c1ae40fb3eded886f8d82eb941e588fc9 (patch) | |
tree | 2b3863afcfca8ccb73db473c889320f2ec24ac33 | |
parent | 351c92f5c61082e9e8f5e1c9364f1836416f17d3 (diff) |
Checker: re-sync vo structures after Maxime's commit 16136
make validate still fails, but that's another issue (#2949) we're
still working on...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16198 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | Makefile.build | 3 | ||||
-rw-r--r-- | checker/declarations.ml | 26 | ||||
-rw-r--r-- | checker/declarations.mli | 9 | ||||
-rw-r--r-- | checker/term.ml | 4 | ||||
-rw-r--r-- | checker/term.mli | 2 | ||||
-rw-r--r-- | checker/typeops.ml | 2 |
6 files changed, 32 insertions, 14 deletions
diff --git a/Makefile.build b/Makefile.build index 661e762de..d8b9df0d4 100644 --- a/Makefile.build +++ b/Makefile.build @@ -370,7 +370,8 @@ install-ide-info: .PHONY: validate check test-suite $(ALLSTDLIB).v -VALIDOPTS=-silent -o -m + +VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m validate:: $(CHICKEN) $(ALLVO) $(SHOW)'COQCHK <theories & plugins>' diff --git a/checker/declarations.ml b/checker/declarations.ml index c74c95dff..529f08cb1 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -7,6 +7,8 @@ open Validate type values type reloc_table type to_patch_substituted +(* Native code *) +type native_name (*Retroknowledge *) type action type retroknowledge @@ -518,7 +520,9 @@ type constant_body = { const_body : constant_def; const_type : constant_type; const_body_code : to_patch_substituted; - const_constraints : Univ.constraints } + const_constraints : Univ.constraints; + const_native_name : native_name ref; + const_inline_code : bool } let body_of_constant cb = match cb.const_body with | Undef _ -> None @@ -538,7 +542,9 @@ let val_cb = val_tuple ~name:"constant_body" val_cst_def; val_cst_type; no_val; - val_cstrs|] + val_cstrs; + no_val; + val_bool|] let subst_rel_declaration sub (id,copt,t as x) = let copt' = Option.smartmap (subst_mps sub) copt in @@ -689,10 +695,13 @@ type mutual_inductive_body = { (* Universes constraints enforced by the inductive declaration *) mind_constraints : Univ.constraints; + (* Data for native compilation *) + mind_native_name : native_name ref; + } let val_ind_pack = val_tuple ~name:"mutual_inductive_body" [|val_array val_one_ind;val_bool;val_bool;val_int;val_nctxt; - val_int; val_int; val_rctxt;val_cstrs|] + val_int; val_int; val_rctxt;val_cstrs;no_val|] let subst_arity sub = function @@ -700,12 +709,12 @@ let subst_arity sub = function | PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s) (* TODO: should be changed to non-coping after Term.subst_mps *) -let subst_const_body sub cb = { +(* NB: we leave bytecode and native code fields untouched *) +let subst_const_body sub cb = + { cb with const_hyps = (assert (cb.const_hyps=[]); []); const_body = subst_constant_def sub cb.const_body; - const_type = subst_arity sub cb.const_type; - const_body_code = (*Cemitcodes.subst_to_patch_subst sub*) cb.const_body_code; - const_constraints = cb.const_constraints} + const_type = subst_arity sub cb.const_type } let subst_arity sub = function | Monomorphic s -> @@ -742,7 +751,8 @@ let subst_mind sub mib = mind_params_ctxt = map_rel_context (subst_mps sub) mib.mind_params_ctxt; mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; - mind_constraints = mib.mind_constraints } + mind_constraints = mib.mind_constraints; + mind_native_name = mib.mind_native_name} (* Modules *) diff --git a/checker/declarations.mli b/checker/declarations.mli index ad234a3f5..80c895bbe 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -5,6 +5,8 @@ open Term type values type reloc_table type to_patch_substituted +(* Native code *) +type native_name (*Retroknowledge *) type action type retroknowledge @@ -57,7 +59,9 @@ type constant_body = { const_body : constant_def; const_type : constant_type; const_body_code : to_patch_substituted; - const_constraints : Univ.constraints } + const_constraints : Univ.constraints; + const_native_name : native_name ref; + const_inline_code : bool } val body_of_constant : constant_body -> constr_substituted option val constant_has_body : constant_body -> bool @@ -167,6 +171,9 @@ type mutual_inductive_body = { (* Universes constraints enforced by the inductive declaration *) mind_constraints : Univ.constraints; + (* Data for native compilation *) + mind_native_name : native_name ref; + } (* Modules *) diff --git a/checker/term.ml b/checker/term.ml index e7e9c891b..8e968904b 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -80,8 +80,8 @@ let val_fix f = [|val_tuple~name:"fix2"[|val_array val_int;val_int|];val_prec f|] let val_cofix f = val_tuple ~name:"pcofixpoint"[|val_int;val_prec f|] -type cast_kind = VMcast | DEFAULTcast -let val_cast = val_enum "cast_kind" 2 +type cast_kind = VMcast | NATIVEcast | DEFAULTcast +let val_cast = val_enum "cast_kind" 3 (*s*******************************************************************) (* The type of constructions *) diff --git a/checker/term.mli b/checker/term.mli index c417cd14e..cc9d5cf97 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -23,7 +23,7 @@ type 'a pexistential = existential_key * 'a array type 'a prec_declaration = name array * 'a array * 'a array type 'a pfixpoint = (int array * int) * 'a prec_declaration type 'a pcofixpoint = int * 'a prec_declaration -type cast_kind = VMcast | DEFAULTcast +type cast_kind = VMcast | NATIVEcast | DEFAULTcast type constr = Rel of int | Var of Id.t diff --git a/checker/typeops.ml b/checker/typeops.ml index 07c7bc367..a5b110f9b 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -167,7 +167,7 @@ let sort_of_product env domsort rangsort = let judge_of_cast env (c,cj) k tj = let conversion = match k with - | VMcast -> vm_conv CUMUL + | VMcast | NATIVEcast -> vm_conv CUMUL | DEFAULTcast -> conv_leq in try conversion env cj tj |