Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

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
  • Loading branch information...
commit 33c0d04c1ae40fb3eded886f8d82eb941e588fc9 1 parent 351c92f
letouzey authored
View
3  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>'
View
26 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 *)
View
9 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 *)
View
4 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 *)
View
2  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
View
2  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
Please sign in to comment.
Something went wrong with that request. Please try again.