From 7d9331a2a188842a98936278d02177f1a6fa7001 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Sat, 17 Oct 2015 21:40:49 -0700 Subject: Adds support for the virtual machine to perform reduction of universe polymorphic definitions. - This implementation passes universes in separate arguments and does not eagerly instanitate polymorphic definitions. - This means that it pays no cost on monomorphic definitions. --- kernel/byterun/coq_interp.c | 34 ++++-- kernel/byterun/coq_values.h | 17 ++- kernel/cbytecodes.ml | 57 +++++----- kernel/cbytecodes.mli | 31 ++++-- kernel/cbytegen.ml | 250 ++++++++++++++++++++++++++++++++++---------- kernel/cbytegen.mli | 10 +- kernel/cemitcodes.ml | 23 ++-- kernel/cemitcodes.mli | 4 +- kernel/csymtable.ml | 30 +++--- kernel/environ.mli | 2 +- kernel/mod_typing.ml | 10 +- kernel/modops.ml | 2 +- kernel/nativelambda.ml | 2 +- kernel/term_typing.ml | 39 ++++--- kernel/univ.ml | 7 +- kernel/univ.mli | 3 + kernel/vars.ml | 4 +- kernel/vars.mli | 2 +- kernel/vconv.ml | 50 +++++++-- kernel/vm.ml | 112 ++++++++++++++++---- kernel/vm.mli | 11 +- 21 files changed, 502 insertions(+), 198 deletions(-) (limited to 'kernel') diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 0553a5ed7e..dc571699ef 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -341,6 +341,7 @@ value coq_interprete /* Fallthrough */ Instruct(ENVACC){ print_instr("ENVACC"); + print_int(*pc); accu = Field(coq_env, *pc++); Next; } @@ -371,6 +372,10 @@ value coq_interprete sp[1] = (value)pc; sp[2] = coq_env; sp[3] = Val_long(coq_extra_args); + print_instr("call stack="); + print_lint(sp[1]); + print_lint(sp[2]); + print_lint(sp[3]); pc = Code_val(accu); coq_env = accu; coq_extra_args = 0; @@ -458,6 +463,7 @@ value coq_interprete sp[0] = arg1; sp[1] = arg2; pc = Code_val(accu); + print_lint(accu); coq_env = accu; coq_extra_args += 1; goto check_stacks; @@ -481,11 +487,18 @@ value coq_interprete print_instr("RETURN"); print_int(*pc); sp += *pc++; + print_instr("stack="); + print_lint(sp[0]); + print_lint(sp[1]); + print_lint(sp[2]); if (coq_extra_args > 0) { + print_instr("extra args > 0"); + print_lint(coq_extra_args); coq_extra_args--; pc = Code_val(accu); coq_env = accu; } else { + print_instr("extra args = 0"); pc = (code_t)(sp[0]); coq_env = sp[1]; coq_extra_args = Long_val(sp[2]); @@ -585,7 +598,10 @@ value coq_interprete Alloc_small(accu, 1 + nvars, Closure_tag); Code_val(accu) = pc + *pc; pc++; - for (i = 0; i < nvars; i++) Field(accu, i + 1) = sp[i]; + for (i = 0; i < nvars; i++) { + print_lint(sp[i]); + Field(accu, i + 1) = sp[i]; + } sp += nvars; Next; } @@ -720,6 +736,7 @@ value coq_interprete /* Fallthrough */ Instruct(GETGLOBAL){ print_instr("GETGLOBAL"); + print_int(*pc); accu = Field(coq_global_data, *pc); pc++; Next; @@ -732,7 +749,7 @@ value coq_interprete tag_t tag = *pc++; mlsize_t i; value block; - print_instr("MAKEBLOCK"); + print_instr("MAKEBLOCK, tag="); Alloc_small(block, wosize, tag); Field(block, 0) = accu; for (i = 1; i < wosize; i++) Field(block, i) = *sp++; @@ -743,7 +760,8 @@ value coq_interprete tag_t tag = *pc++; value block; - print_instr("MAKEBLOCK1"); + print_instr("MAKEBLOCK1, tag="); + print_int(tag); Alloc_small(block, 1, tag); Field(block, 0) = accu; accu = block; @@ -753,7 +771,8 @@ value coq_interprete tag_t tag = *pc++; value block; - print_instr("MAKEBLOCK2"); + print_instr("MAKEBLOCK2, tag="); + print_int(tag); Alloc_small(block, 2, tag); Field(block, 0) = accu; Field(block, 1) = sp[0]; @@ -764,7 +783,8 @@ value coq_interprete Instruct(MAKEBLOCK3) { tag_t tag = *pc++; value block; - print_instr("MAKEBLOCK3"); + print_instr("MAKEBLOCK3, tag="); + print_int(tag); Alloc_small(block, 3, tag); Field(block, 0) = accu; Field(block, 1) = sp[0]; @@ -776,7 +796,8 @@ value coq_interprete Instruct(MAKEBLOCK4) { tag_t tag = *pc++; value block; - print_instr("MAKEBLOCK4"); + print_instr("MAKEBLOCK4, tag="); + print_int(tag); Alloc_small(block, 4, tag); Field(block, 0) = accu; Field(block, 1) = sp[0]; @@ -940,6 +961,7 @@ value coq_interprete /* Fallthrough */ Instruct(CONSTINT) { print_instr("CONSTINT"); + print_int(*pc); accu = Val_int(*pc); pc++; Next; diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index 80100da719..bb0f0eb5e4 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -17,22 +17,17 @@ #define Default_tag 0 #define Accu_tag 0 - - #define ATOM_ID_TAG 0 #define ATOM_INDUCTIVE_TAG 1 -#define ATOM_PROJ_TAG 2 -#define ATOM_FIX_TAG 3 -#define ATOM_SWITCH_TAG 4 -#define ATOM_COFIX_TAG 5 -#define ATOM_COFIXEVALUATED_TAG 6 - - +#define ATOM_TYPE_TAG 2 +#define ATOM_PROJ_TAG 3 +#define ATOM_FIX_TAG 4 +#define ATOM_SWITCH_TAG 5 +#define ATOM_COFIX_TAG 6 +#define ATOM_COFIXEVALUATED_TAG 7 /* Les blocs accumulate */ #define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag)) #define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG)) #endif /* _COQ_VALUES_ */ - - diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 448bf85444..b13b0607b3 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -19,13 +19,12 @@ type tag = int let accu_tag = 0 -let max_atom_tag = 1 -let proj_tag = 2 -let fix_app_tag = 3 -let switch_tag = 4 -let cofix_tag = 5 -let cofix_evaluated_tag = 6 - +let max_atom_tag = 2 +let proj_tag = 3 +let fix_app_tag = 4 +let switch_tag = 5 +let cofix_tag = 6 +let cofix_evaluated_tag = 7 (* It would be great if OCaml exported this value, So fixme if this happens in a new version of OCaml *) @@ -33,10 +32,12 @@ let last_variant_tag = 245 type structured_constant = | Const_sorts of sorts - | Const_ind of pinductive + | Const_ind of inductive | Const_proj of Constant.t | Const_b0 of tag | Const_bn of tag * structured_constant array + | Const_univ_level of Univ.universe_level + | Const_type of Univ.universe type reloc_table = (tag * int) array @@ -71,7 +72,8 @@ type instruction = | Kclosure of Label.t * int | Kclosurerec of int * int * Label.t array * Label.t array | Kclosurecofix of int * int * Label.t array * Label.t array - | Kgetglobal of pconstant + (* nb fv, init, lbl types, lbl bodies *) + | Kgetglobal of constant | Kconst of structured_constant | Kmakeblock of int * tag | Kmakeprod @@ -127,7 +129,10 @@ type instruction = and bytecodes = instruction list -type fv_elem = FVnamed of Id.t | FVrel of int +type fv_elem = + | FVnamed of Id.t + | FVrel of int + | FVuniv_var of int type fv = fv_elem array @@ -145,18 +150,17 @@ type vm_env = { type comp_env = { - nb_stack : int; (* nbre de variables sur la pile *) - in_stack : int list; (* position dans la pile *) - nb_rec : int; (* nbre de fonctions mutuellement *) - (* recursives = nbr *) + nb_uni_stack : int ; (* number of universes on the stack, *) + (* universes are always at the bottom. *) + nb_stack : int; (* number of variables on the stack *) + in_stack : int list; (* position in the stack *) + nb_rec : int; (* number of mutually recursive functions *) pos_rec : instruction list; (* instruction d'acces pour les variables *) (* de point fix ou de cofix *) offset : int; - in_env : vm_env ref + in_env : vm_env ref (* The free variables of the expression *) } - - (* --- Pretty print *) open Pp open Util @@ -169,14 +173,24 @@ let pp_sort s = let rec pp_struct_const = function | Const_sorts s -> pp_sort s - | Const_ind ((mind, i), u) -> pr_mind mind ++ str"#" ++ int i + | Const_ind (mind, i) -> pr_mind mind ++ str"#" ++ int i | Const_proj p -> Constant.print p | Const_b0 i -> int i | Const_bn (i,t) -> int i ++ surround (prvect_with_sep pr_comma pp_struct_const t) + | Const_univ_level l -> Univ.Level.pr l + | Const_type u -> str "Type@{" ++ Univ.pr_uni u ++ str "}" let pp_lbl lbl = str "L" ++ int lbl +let pp_pcon (id,u) = + pr_con id ++ str "@{" ++ Univ.Instance.pr Univ.Level.pr u ++ str "}" + +let pp_fv_elem = function + | FVnamed id -> str "FVnamed(" ++ Id.print id ++ str ")" + | FVrel i -> str "Rel(" ++ int i ++ str ")" + | FVuniv_var v -> str "FVuniv(" ++ int v ++ str ")" + let rec pp_instr i = match i with | Klabel _ | Ksequence _ -> assert false @@ -210,8 +224,7 @@ let rec pp_instr i = prlist_with_sep spc pp_lbl (Array.to_list lblt) ++ str " bodies = " ++ prlist_with_sep spc pp_lbl (Array.to_list lblb)) - | Kgetglobal (id,u) -> - str "getglobal " ++ pr_con id ++ str "@{" ++ Univ.Instance.pr Univ.Level.pr u ++ str "}" + | Kgetglobal idu -> str "getglobal " ++ pr_con idu | Kconst sc -> str "const " ++ pp_struct_const sc | Kmakeblock(n, m) -> @@ -269,10 +282,6 @@ and pp_bytecodes c = | i :: c -> tab () ++ pp_instr i ++ fnl () ++ pp_bytecodes c -let dump_bytecode c = - pperrnl (pp_bytecodes c); - flush_all() - (*spiwack: moved this type in this file because I needed it for retroknowledge which can't depend from cbytegen *) type block = diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 03d6383057..c35ef6920f 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -22,14 +22,18 @@ val switch_tag : tag val cofix_tag : tag val cofix_evaluated_tag : tag -val last_variant_tag : tag +val last_variant_tag : tag type structured_constant = | Const_sorts of sorts - | Const_ind of pinductive + | Const_ind of inductive | Const_proj of Constant.t | Const_b0 of tag | Const_bn of tag * structured_constant array + | Const_univ_level of Univ.universe_level + | Const_type of Univ.universe + +val pp_struct_const : structured_constant -> Pp.std_ppcmds type reloc_table = (tag * int) array @@ -64,9 +68,11 @@ type instruction = (** nb fv, init, lbl types, lbl bodies *) | Kclosurecofix of int * int * Label.t array * Label.t array (** nb fv, init, lbl types, lbl bodies *) - | Kgetglobal of pconstant (** accu = coq_global_data[c] *) + | Kgetglobal of constant | Kconst of structured_constant - | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block *) + | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block. Index 0 + ** is accu, all others are popped from + ** the top of the stack *) | Kmakeprod | Kmakeswitchblock of Label.t * Label.t * annot_switch * int | Kswitch of Label.t array * Label.t array (** consts,blocks *) @@ -120,7 +126,10 @@ type instruction = and bytecodes = instruction list -type fv_elem = FVnamed of Id.t | FVrel of int +type fv_elem = + FVnamed of Id.t +| FVrel of int +| FVuniv_var of int type fv = fv_elem array @@ -129,26 +138,28 @@ type fv = fv_elem array closed terms. *) exception NotClosed -(*spiwack: both type have been moved from Cbytegen because I needed then +(*spiwack: both type have been moved from Cbytegen because I needed them for the retroknowledge *) type vm_env = { - size : int; (** longueur de la liste [n] *) + size : int; (** length of the list [n] *) fv_rev : fv_elem list (** [fvn; ... ;fv1] *) } type comp_env = { + nb_uni_stack : int ; (** number of universes on the stack *) nb_stack : int; (** number of variables on the stack *) in_stack : int list; (** position in the stack *) nb_rec : int; (** number of mutually recursive functions *) - (** recursives = nbr *) + (** (= nbr) *) pos_rec : instruction list; (** instruction d'acces pour les variables *) (** de point fix ou de cofix *) offset : int; - in_env : vm_env ref + in_env : vm_env ref (** the variables that are accessed *) } -val dump_bytecode : bytecodes -> unit +val pp_bytecodes : bytecodes -> Pp.std_ppcmds +val pp_fv_elem : fv_elem -> Pp.std_ppcmds (*spiwack: moved this here because I needed it for retroknowledge *) type block = diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 3462694d61..f9f72efdb9 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -96,13 +96,14 @@ let empty_fv = { size= 0; fv_rev = [] } let fv r = !(r.in_env) -let empty_comp_env ()= - { nb_stack = 0; +let empty_comp_env ?(univs=0) ()= + { nb_uni_stack = univs; + nb_stack = 0; in_stack = []; nb_rec = 0; pos_rec = []; offset = 0; - in_env = ref empty_fv; + in_env = ref empty_fv } (*i Creation functions for comp_env *) @@ -110,8 +111,9 @@ let empty_comp_env ()= let rec add_param n sz l = if Int.equal n 0 then l else add_param (n - 1) sz (n+sz::l) -let comp_env_fun arity = - { nb_stack = arity; +let comp_env_fun ?(univs=0) arity = + { nb_uni_stack = univs ; + nb_stack = arity; in_stack = add_param arity 0 []; nb_rec = 0; pos_rec = []; @@ -120,8 +122,9 @@ let comp_env_fun arity = } -let comp_env_fix_type rfv = - { nb_stack = 0; +let comp_env_fix_type rfv = + { nb_uni_stack = 0; + nb_stack = 0; in_stack = []; nb_rec = 0; pos_rec = []; @@ -134,7 +137,8 @@ let comp_env_fix ndef curr_pos arity rfv = for i = ndef downto 1 do prec := Koffsetclosure (2 * (ndef - curr_pos - i)) :: !prec done; - { nb_stack = arity; + { nb_uni_stack = 0; + nb_stack = arity; in_stack = add_param arity 0 []; nb_rec = ndef; pos_rec = !prec; @@ -143,7 +147,8 @@ let comp_env_fix ndef curr_pos arity rfv = } let comp_env_cofix_type ndef rfv = - { nb_stack = 0; + { nb_uni_stack = 0; + nb_stack = 0; in_stack = []; nb_rec = 0; pos_rec = []; @@ -156,7 +161,8 @@ let comp_env_cofix ndef arity rfv = for i = 1 to ndef do prec := Kenvacc i :: !prec done; - { nb_stack = arity; + { nb_uni_stack = 0; + nb_stack = arity; in_stack = add_param arity 0 []; nb_rec = ndef; pos_rec = !prec; @@ -168,7 +174,7 @@ let comp_env_cofix ndef arity rfv = let push_param n sz r = { r with nb_stack = r.nb_stack + n; - in_stack = add_param n sz r.in_stack } + in_stack = add_param n (sz - r.nb_uni_stack) r.in_stack } (* [push_local sz r] add a new variable on the stack at position [sz] *) let push_local sz r = @@ -176,8 +182,6 @@ let push_local sz r = nb_stack = r.nb_stack + 1; in_stack = (sz + 1) :: r.in_stack } - - (*i Compilation of variables *) let find_at f l = let rec aux n = function @@ -214,6 +218,37 @@ let pos_rel i r sz = r.in_env := { size = pos+1; fv_rev = db:: env.fv_rev}; Kenvacc(r.offset + pos) +(* +let pos_poly_inst idu r = + let env = !(r.in_env) in + let f = function + | FVpoly_inst i -> Univ.eq_puniverses Names.Constant.equal idu i + | _ -> false + in + try Kenvacc (r.offset + env.size - (find_at f env.fv_rev)) + with Not_found -> + let pos = env.size in + let db = FVpoly_inst idu in + r.in_env := { size = pos+1; fv_rev = db:: env.fv_rev}; + Kenvacc(r.offset + pos) +*) + +let pos_universe_var i r sz = + if i < r.nb_uni_stack then + Kacc (sz - r.nb_stack - (r.nb_uni_stack - i)) + else + let env = !(r.in_env) in + let f = function + | FVuniv_var u -> Int.equal i u + | _ -> false + in + try Kenvacc (r.offset + env.size - (find_at f env.fv_rev)) + with Not_found -> + let pos = env.size in + let db = FVuniv_var i in + r.in_env := { size = pos + 1; fv_rev = db::env.fv_rev } ; + Kenvacc(r.offset + pos) + (*i Examination of the continuation *) (* Discard all instructions up to the next label. *) @@ -459,7 +494,8 @@ let rec str_const c = end | _ -> Bconstr c end - | Ind ind -> Bstrconst (Const_ind ind) + | Ind (ind,_) -> + Bstrconst (Const_ind ind) | Construct (((kn,j),i),u) -> begin (* spiwack: tries first to apply the run-time compilation @@ -513,6 +549,7 @@ let compile_fv_elem reloc fv sz cont = match fv with | FVrel i -> pos_rel i reloc sz :: cont | FVnamed id -> pos_named id reloc :: cont + | FVuniv_var i -> pos_universe_var i reloc sz :: cont let rec compile_fv reloc l sz cont = match l with @@ -524,18 +561,21 @@ let rec compile_fv reloc l sz cont = (* Compiling constants *) -let rec get_alias env (kn,u as p) = +let rec get_alias env kn = let cb = lookup_constant kn env in let tps = cb.const_body_code in match tps with - | None -> p + | None -> kn | Some tps -> (match Cemitcodes.force tps with - | BCalias (kn',u') -> get_alias env (kn', Univ.subst_instance_instance u u') - | _ -> p) + | BCalias kn' -> get_alias env kn' + | _ -> kn) (* Compiling expressions *) +type ('a,'b) sum = Inl of 'a | Inr of 'b + +(* sz is the size of the local stack *) let rec compile_constr reloc c sz cont = match kind_of_term c with | Meta _ -> invalid_arg "Cbytegen.compile_constr : Meta" @@ -552,9 +592,40 @@ let rec compile_constr reloc c sz cont = | Rel i -> pos_rel i reloc sz :: cont | Var id -> pos_named id reloc :: cont | Const (kn,u) -> compile_const reloc kn u [||] sz cont - | Sort _ | Ind _ | Construct _ -> + | Ind (i,u) -> + if Univ.Instance.is_empty u then compile_str_cst reloc (str_const c) sz cont - + else + comp_app compile_str_cst compile_universe reloc + (str_const c) + (Univ.Instance.to_array u) + sz + cont + | Sort (Prop _) | Construct _ -> + compile_str_cst reloc (str_const c) sz cont + | Sort (Type u) -> + begin + let levels = Univ.Universe.levels u in + if Univ.LSet.exists (fun x -> Univ.Level.var_index x <> None) levels + then + (** TODO(gmalecha): Fix this **) + (** NOTE: This relies on the order of iteration to be consistent + **) + let level_vars = + List.map_filter (fun x -> Univ.Level.var_index x) + (Univ.LSet.elements levels) + in + let compile_get_univ reloc idx sz cont = + compile_fv_elem reloc (FVuniv_var idx) sz cont + in + comp_app compile_str_cst compile_get_univ reloc + (Bstrconst (Const_type u)) + (Array.of_list level_vars) + sz + cont + else + compile_str_cst reloc (str_const c) sz cont + end | LetIn(_,xb,_,body) -> compile_constr reloc xb sz (Kpush :: @@ -663,7 +734,9 @@ let rec compile_constr reloc c sz cont = let lbl_sw = Label.create () in let sz_b,branch,is_tailcall = match branch1 with - | Kreturn k -> assert (Int.equal k sz); sz, branch1, true + | Kreturn k -> + assert (Int.equal k sz) ; + sz, branch1, true | _ -> sz+3, Kjump, false in let annot = {ci = ci; rtbl = tbl; tailcall = is_tailcall} in @@ -745,6 +818,19 @@ and compile_str_cst reloc sc sz cont = (* spiwack : compilation of constants with their arguments. Makes a special treatment with 31-bit integer addition *) +and compile_get_global reloc (kn,u) sz cont = + let kn = get_alias !global_env kn in + if Univ.Instance.is_empty u then + Kgetglobal kn :: cont + else + comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont) + compile_universe reloc () (Univ.Instance.to_array u) sz cont + +and compile_universe reloc uni sz cont = + match Univ.Level.var_index uni with + | None -> Kconst (Const_univ_level uni) :: cont + | Some idx -> pos_universe_var idx reloc sz :: cont + and compile_const = fun reloc-> fun kn u -> fun args -> fun sz -> fun cont -> let nargs = Array.length args in @@ -756,31 +842,83 @@ and compile_const = (mkConstU (kn,u)) reloc args sz cont with Not_found -> if Int.equal nargs 0 then - Kgetglobal (get_alias !global_env (kn, u)) :: cont + compile_get_global reloc (kn,u) sz cont else - comp_app (fun _ _ _ cont -> - Kgetglobal (get_alias !global_env (kn,u)) :: cont) - compile_constr reloc () args sz cont - -let compile fail_on_error env c = + if Univ.Instance.is_empty u then + (* normal compilation *) + comp_app (fun _ _ sz cont -> + compile_get_global reloc (kn,u) sz cont) + compile_constr reloc () args sz cont + else + let compile_either reloc constr_or_uni sz cont = + match constr_or_uni with + | Inl cst -> compile_constr reloc cst sz cont + | Inr uni -> compile_universe reloc uni sz cont + in + (** TODO(gmalecha): This can be more efficient **) + let all = + Array.of_list (List.map (fun x -> Inr x) (Array.to_list (Univ.Instance.to_array u)) @ + List.map (fun x -> Inl x) (Array.to_list args)) + in + comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont) + compile_either reloc () all sz cont + +let is_univ_copy max u = + let u = Univ.Instance.to_array u in + if Array.length u = max then + Array.fold_left_i (fun i acc u -> + if acc then + match Univ.Level.var_index u with + | None -> false + | Some l -> l = i + else false) true u + else + false + +let dump_bytecodes init code fvs = + let open Pp in + (str "code =" ++ fnl () ++ + pp_bytecodes init ++ fnl () ++ + pp_bytecodes code ++ fnl () ++ + str "fv = " ++ + prlist_with_sep (fun () -> str "; ") pp_fv_elem fvs ++ + fnl ()) + +let compile fail_on_error ?universes:(universes=0) env c = set_global_env env; init_fun_code (); Label.reset_label_counter (); - let reloc = empty_comp_env () in - try - let init_code = compile_constr reloc c 0 [Kstop] in - let fv = List.rev (!(reloc.in_env).fv_rev) in - let pp_v v = - match v with - | FVnamed id -> Pp.str (Id.to_string id) - | FVrel i -> Pp.str (string_of_int i) + let cont = [Kstop] in + try + let reloc, init_code = + if Int.equal universes 0 then + let reloc = empty_comp_env () in + reloc, compile_constr reloc c 0 cont + else + (* We are going to generate a lambda, but merge the universe closure + * with the function closure if it exists. + *) + let reloc = empty_comp_env () in + let arity , body = + match kind_of_term c with + | Lambda _ -> + let params, body = decompose_lam c in + List.length params , body + | _ -> 0 , c + in + let full_arity = arity + universes in + let r_fun = comp_env_fun ~univs:universes arity in + let lbl_fun = Label.create () in + let cont_fun = + compile_constr r_fun body full_arity [Kreturn full_arity] + in + fun_code := [Ksequence(add_grab full_arity lbl_fun cont_fun,!fun_code)]; + let fv = fv r_fun in + reloc, compile_fv reloc fv.fv_rev 0 (Kclosure(lbl_fun,fv.size) :: cont) in - let open Pp in - if !Flags.dump_bytecode then - (dump_bytecode init_code; - dump_bytecode !fun_code; - Pp.msg_debug (Pp.str "fv = " ++ - Pp.prlist_with_sep (fun () -> Pp.str "; ") pp_v fv ++ Pp.fnl ())); + let fv = List.rev (!(reloc.in_env).fv_rev) in + (if !Flags.dump_bytecode then + Pp.msg_debug (dump_bytecodes init_code !fun_code fv)) ; Some (init_code,!fun_code, Array.of_list fv) with TooLargeInductive tname -> let fn = if fail_on_error then Errors.errorlabstrm "compile" else Pp.msg_warning in @@ -789,28 +927,33 @@ let compile fail_on_error env c = Id.print tname ++ str str_max_constructors)); None) -let compile_constant_body fail_on_error env = function +let compile_constant_body fail_on_error env univs = function | Undef _ | OpaqueDef _ -> Some BCconstant | Def sb -> let body = Mod_subst.force_constr sb in + let instance_size = + match univs with + | None -> 0 + | Some univ -> Univ.UContext.size univ + in match kind_of_term body with - | Const (kn',u) -> + | Const (kn',u) when is_univ_copy instance_size u -> (* we use the canonical name of the constant*) let con= constant_of_kn (canonical_con kn') in - Some (BCalias (get_alias env (con,u))) + Some (BCalias (get_alias env con)) | _ -> - let res = compile fail_on_error env body in + let res = compile fail_on_error ~universes:instance_size env body in Option.map (fun x -> BCdefined (to_memory x)) res (* Shortcut of the previous function used during module strengthening *) -let compile_alias (kn,u) = BCalias (constant_of_kn (canonical_con kn), u) +let compile_alias kn = BCalias (constant_of_kn (canonical_con kn)) (* spiwack: additional function which allow different part of compilation of the 31-bit integers *) let make_areconst n else_lbl cont = - if n <=0 then + if n <= 0 then cont else Kareconst (n, else_lbl)::cont @@ -902,14 +1045,14 @@ let op2_compilation op = 3/ if at least one is not, branches to the normal behavior: Kgetglobal (get_alias !global_env kn) *) let op_compilation n op = - let code_construct kn cont = + let code_construct reloc kn sz cont = let f_cont = let else_lbl = Label.create () in Kareconst(n, else_lbl):: Kacc 0:: Kpop 1:: op:: Kreturn 0:: Klabel else_lbl:: (* works as comp_app with nargs = n and tailcall cont [Kreturn 0]*) - Kgetglobal (get_alias !global_env kn):: - Kappterm(n, n):: [] (* = discard_dead_code [Kreturn 0] *) + compile_get_global reloc kn sz ( + Kappterm(n, n):: []) (* = discard_dead_code [Kreturn 0] *) in let lbl = Label.create () in fun_code := [Ksequence (add_grab n lbl f_cont, !fun_code)]; @@ -926,12 +1069,11 @@ let op_compilation n op = (*Kaddint31::escape::Klabel else_lbl::Kpush::*) (op::escape::Klabel else_lbl::Kpush:: (* works as comp_app with nargs = n and non-tailcall cont*) - Kgetglobal (get_alias !global_env kn):: - Kapply n::labeled_cont))) + compile_get_global reloc kn sz (Kapply n::labeled_cont)))) else if Int.equal nargs 0 then - code_construct kn cont + code_construct reloc kn sz cont else - comp_app (fun _ _ _ cont -> code_construct kn cont) + comp_app (fun reloc _ sz cont -> code_construct reloc kn sz cont) compile_constr reloc () args sz cont let int31_escape_before_match fc cont = diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index 1128f0d0b7..c0f48641ce 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -4,17 +4,17 @@ open Term open Declarations open Pre_env - +(** Should only be used for monomorphic terms *) val compile : bool -> (* Fail on error with a nice user message, otherwise simply a warning *) - env -> constr -> (bytecodes * bytecodes * fv) option + ?universes:int -> env -> constr -> (bytecodes * bytecodes * fv) option (** init, fun, fv *) -val compile_constant_body : bool -> - env -> constant_def -> body_code option +val compile_constant_body : bool -> + env -> constant_universes option -> constant_def -> body_code option (** Shortcut of the previous function used during module strengthening *) -val compile_alias : pconstant -> body_code +val compile_alias : Names.constant -> body_code (** spiwack: this function contains the information needed to perform the static compilation of int31 (trying and obtaining diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 9b275cb6c3..2a70d0b1b7 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -19,7 +19,7 @@ open Mod_subst type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant - | Reloc_getglobal of pconstant + | Reloc_getglobal of Names.constant type patch = reloc_info * int @@ -127,11 +127,11 @@ let slot_for_const c = enter (Reloc_const c); out_int 0 -and slot_for_annot a = +let slot_for_annot a = enter (Reloc_annot a); out_int 0 -and slot_for_getglobal p = +let slot_for_getglobal p = enter (Reloc_getglobal p); out_int 0 @@ -190,7 +190,7 @@ let emit_instr = function Array.iter (out_label_with_orig org) lbl_bodies | Kgetglobal q -> out opGETGLOBAL; slot_for_getglobal q - | Kconst((Const_b0 i)) -> + | Kconst (Const_b0 i) -> if i >= 0 && i <= 3 then out (opCONST0 + i) else (out opCONSTINT; out_int i) @@ -310,7 +310,7 @@ let rec subst_strcst s sc = | Const_sorts _ | Const_b0 _ -> sc | Const_proj p -> Const_proj (subst_constant s p) | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args) - | Const_ind(ind,u) -> let kn,i = ind in Const_ind((subst_mind s kn, i), u) + | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i) let subst_patch s (ri,pos) = match ri with @@ -319,7 +319,7 @@ let subst_patch s (ri,pos) = let ci = {a.ci with ci_ind = (subst_mind s kn,i)} in (Reloc_annot {a with ci = ci},pos) | Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos) - | Reloc_getglobal kn -> (Reloc_getglobal (subst_pcon s kn), pos) + | Reloc_getglobal kn -> (Reloc_getglobal (subst_constant s kn), pos) let subst_to_patch s (code,pl,fv) = code,List.rev_map (subst_patch s) pl,fv @@ -328,12 +328,12 @@ let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u) type body_code = | BCdefined of to_patch - | BCalias of pconstant + | BCalias of Names.constant | BCconstant type to_patch_substituted = | PBCdefined of to_patch substituted -| PBCalias of pconstant substituted +| PBCalias of Names.constant substituted | PBCconstant let from_val = function @@ -343,7 +343,7 @@ let from_val = function let force = function | PBCdefined tp -> BCdefined (force subst_to_patch tp) -| PBCalias cu -> BCalias (force subst_pconstant cu) +| PBCalias cu -> BCalias (force subst_constant cu) | PBCconstant -> BCconstant let subst_to_patch_subst s = function @@ -373,8 +373,3 @@ let to_memory (init_code, fun_code, fv) = | Label_undefined patchlist -> assert (patchlist = []))) !label_table; (code, reloc, fv) - - - - - diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index 54b92b9121..10f3a6087a 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -4,7 +4,7 @@ open Cbytecodes type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant - | Reloc_getglobal of constant Univ.puniverses + | Reloc_getglobal of constant type patch = reloc_info * int @@ -25,7 +25,7 @@ val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch type body_code = | BCdefined of to_patch - | BCalias of constant Univ.puniverses + | BCalias of constant | BCconstant diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index b3f0ba5b58..28f0fa4f28 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -58,7 +58,7 @@ let set_global v = let rec eq_structured_constant c1 c2 = match c1, c2 with | Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2 | Const_sorts _, _ -> false -| Const_ind i1, Const_ind i2 -> Univ.eq_puniverses eq_ind i1 i2 +| Const_ind i1, Const_ind i2 -> eq_ind i1 i2 | Const_ind _, _ -> false | Const_proj p1, Const_proj p2 -> Constant.equal p1 p2 | Const_proj _, _ -> false @@ -67,18 +67,24 @@ let rec eq_structured_constant c1 c2 = match c1, c2 with | Const_bn (t1, a1), Const_bn (t2, a2) -> Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2 | Const_bn _, _ -> false +| Const_univ_level l1 , Const_univ_level l2 -> Univ.eq_levels l1 l2 +| Const_univ_level _ , _ -> false +| Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2 +| Const_type _ , _ -> false let rec hash_structured_constant c = let open Hashset.Combine in match c with | Const_sorts s -> combinesmall 1 (Sorts.hash s) - | Const_ind (i,u) -> combinesmall 2 (combine (ind_hash i) (Univ.Instance.hash u)) + | Const_ind i -> combinesmall 2 (ind_hash i) | Const_proj p -> combinesmall 3 (Constant.hash p) | Const_b0 t -> combinesmall 4 (Int.hash t) | Const_bn (t, a) -> let fold h c = combine h (hash_structured_constant c) in let h = Array.fold_left fold 0 a in combinesmall 5 (combine (Int.hash t) h) + | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l) + | Const_type u -> combinesmall 7 (Univ.Universe.hash u) module SConstTable = Hashtbl.Make (struct type t = structured_constant @@ -124,7 +130,7 @@ exception NotEvaluated let key rk = match !rk with | None -> raise NotEvaluated - | Some k -> (*Pp.msgnl (str"found at: "++int k);*) + | Some k -> try Ephemeron.get k with Ephemeron.InvalidKey -> raise NotEvaluated @@ -148,23 +154,22 @@ let slot_for_annot key = AnnotTable.add annot_tbl key n; n -let rec slot_for_getglobal env (kn,u) = +let rec slot_for_getglobal env kn = let (cb,(_,rk)) = lookup_constant_key kn env in try key rk with NotEvaluated -> (* Pp.msgnl(str"not yet evaluated");*) let pos = match cb.const_body_code with - | None -> set_global (val_of_constant (kn,u)) + | None -> set_global (val_of_constant kn) | Some code -> match Cemitcodes.force code with | BCdefined(code,pl,fv) -> - if Univ.Instance.is_empty u then - let v = eval_to_patch env (code,pl,fv) in - set_global v - else set_global (val_of_constant (kn,u)) + let v = eval_to_patch env (code,pl,fv) in + set_global v | BCalias kn' -> slot_for_getglobal env kn' - | BCconstant -> set_global (val_of_constant (kn,u)) in + | BCconstant -> set_global (val_of_constant kn) + in (*Pp.msgnl(str"value stored at: "++int pos);*) rk := Some (Ephemeron.create pos); pos @@ -197,6 +202,8 @@ and slot_for_fv env fv = fill_fv_cache rv i val_of_rel env_of_rel b | Some (v, _) -> v end + | FVuniv_var idu -> + assert false and eval_to_patch env (buff,pl,fv) = (* copy code *before* patching because of nested evaluations: @@ -214,7 +221,6 @@ and eval_to_patch env (buff,pl,fv) = List.iter patch pl; let vm_env = Array.map (slot_for_fv env) fv in let tc = tcode_of_code buff (length buff) in -(*Pp.msgnl (str"execute code");*) eval_tcode tc vm_env and val_of_constr env c = @@ -232,5 +238,3 @@ and val_of_constr env c = let set_transparent_const kn = () (* !?! *) let set_opaque_const kn = () (* !?! *) - - diff --git a/kernel/environ.mli b/kernel/environ.mli index 9f6ea522a7..dfe6cc85b1 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -250,7 +250,7 @@ type unsafe_type_judgment = { (** {6 Compilation of global declaration } *) -val compile_constant_body : env -> constant_def -> Cemitcodes.body_code option +val compile_constant_body : env -> constant_universes option -> constant_def -> Cemitcodes.body_code option exception Hyp_not_found diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index c03c5175fd..bd7ee7b339 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -126,11 +126,17 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = Vars.subst_univs_level_constr subst c, ctx, Univ.ContextSet.empty in let def = Def (Mod_subst.from_val c') in +(* let ctx' = Univ.UContext.make (newus, cst) in *) + let univs = + if cb.const_polymorphic then Some cb.const_universes + else None + in let cb' = { cb with const_body = def; - const_universes = univs; - const_body_code = Option.map Cemitcodes.from_val (compile_constant_body env' def) } + const_universes = ctx ; + const_body_code = Option.map Cemitcodes.from_val + (compile_constant_body env' univs def) } in before@(lab,SFBconst(cb'))::after, c', ctx' else diff --git a/kernel/modops.ml b/kernel/modops.ml index f0cb65c967..cbb7963315 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -335,7 +335,7 @@ let strengthen_const mp_from l cb resolver = in { cb with const_body = Def (Mod_subst.from_val (mkConstU (con,u))); - const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias (con,u))) } + const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) } let rec strengthen_mod mp_from mp_to mb = if mp_in_delta mb.mod_mp mb.mod_delta then mb diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 263befd213..4d033bc999 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -379,7 +379,7 @@ let rec get_alias env (kn, u as p) = | None -> p | Some tps -> match Cemitcodes.force tps with - | Cemitcodes.BCalias kn' -> get_alias env kn' + | Cemitcodes.BCalias kn' -> get_alias env (kn', u) | _ -> p (*i Global environment *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index b6df8f454b..cab99077f0 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -258,33 +258,30 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) let inferred = keep_hyps env (Idset.union ids_typ ids_def) in check declared inferred) lc) in let tps = - (* FIXME: incompleteness of the bytecode vm: we compile polymorphic - constants like opaque definitions. *) - if poly then Some (Cemitcodes.from_val Cemitcodes.BCconstant) - else - let res = - match proj with - | None -> compile_constant_body env def - | Some pb -> + let res = + let comp_univs = if poly then Some univs else None in + match proj with + | None -> compile_constant_body env comp_univs def + | Some pb -> (* The compilation of primitive projections is a bit tricky, because they refer to themselves (the body of p looks like fun c => Proj(p,c)). We break the cycle by building an ad-hoc compilation environment. A cleaner solution would be that kernel projections are simply Proj(i,c) with i an int and c a constr, but we would have to get rid of the compatibility layer. *) - let cb = - { const_hyps = hyps; - const_body = def; - const_type = typ; - const_proj = proj; - const_body_code = None; - const_polymorphic = poly; - const_universes = univs; - const_inline_code = inline_code } - in - let env = add_constant kn cb env in - compile_constant_body env def - in Option.map Cemitcodes.from_val res + let cb = + { const_hyps = hyps; + const_body = def; + const_type = typ; + const_proj = proj; + const_body_code = None; + const_polymorphic = poly; + const_universes = univs; + const_inline_code = inline_code } + in + let env = add_constant kn cb env in + compile_constant_body env comp_univs def + in Option.map Cemitcodes.from_val res in { const_hyps = hyps; const_body = def; diff --git a/kernel/univ.ml b/kernel/univ.ml index c0bd3bacd7..064dde3a64 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1754,7 +1754,7 @@ let eq_puniverses f (x, u) (y, u') = f x y && Instance.equal u u' (** A context of universe levels with universe constraints, - representiong local universe variables and constraints *) + representing local universe variables and constraints *) module UContext = struct @@ -1778,8 +1778,11 @@ struct let union (univs, cst) (univs', cst') = Instance.append univs univs', Constraint.union cst cst' - + let dest x = x + + let size (x,_) = Instance.length x + end type universe_context = UContext.t diff --git a/kernel/univ.mli b/kernel/univ.mli index cbaf7e546a..c926c57bd8 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -343,6 +343,9 @@ sig (** Keeps the order of the instances *) val union : t -> t -> t + (* the number of universes in the context *) + val size : t -> int + end type universe_context = UContext.t diff --git a/kernel/vars.ml b/kernel/vars.ml index 88c1e1038c..a800e25315 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -337,5 +337,5 @@ let subst_instance_context s ctx = if Univ.Instance.is_empty s then ctx else map_rel_context (fun x -> subst_instance_constr s x) ctx -type id_key = pconstant tableKey -let eq_id_key x y = Names.eq_table_key (Univ.eq_puniverses Constant.equal) x y +type id_key = constant tableKey +let eq_id_key x y = Names.eq_table_key Constant.equal x y diff --git a/kernel/vars.mli b/kernel/vars.mli index fdd4603b5b..c0fbeeb6e6 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -88,5 +88,5 @@ val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_ val subst_instance_constr : universe_instance -> constr -> constr val subst_instance_context : universe_instance -> rel_context -> rel_context -type id_key = pconstant tableKey +type id_key = constant tableKey val eq_id_key : id_key -> id_key -> bool diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 2f6be06011..e0d9688486 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -45,8 +45,15 @@ let rec conv_val env pb k v1 v2 cu = else conv_whd env pb k (whd_val v1) (whd_val v2) cu and conv_whd env pb k whd1 whd2 cu = +(* Pp.(msg_debug (str "conv_whd(" ++ pr_whd whd1 ++ str ", " ++ pr_whd whd2 ++ str ")")) ; *) match whd1, whd2 with | Vsort s1, Vsort s2 -> sort_cmp_universes env pb s1 s2 cu + | Vuniv_level _ , _ + | _ , Vuniv_level _ -> + (** Both of these are invalid since universes are handled via + ** special cases in the code. + **) + assert false | Vprod p1, Vprod p2 -> let cu = conv_val env CONV k (dom p1) (dom p2) cu in conv_fun env pb k (codom p1) (codom p2) cu @@ -81,26 +88,53 @@ and conv_whd env pb k whd1 whd2 cu = and conv_atom env pb k a1 stk1 a2 stk2 cu = +(* Pp.(msg_debug (str "conv_atom(" ++ pr_atom a1 ++ str ", " ++ pr_atom a2 ++ str ")")) ; *) match a1, a2 with - | Aind ind1, Aind ind2 -> - if eq_puniverses eq_ind ind1 ind2 && compare_stack stk1 stk2 + | Aind ((mi,i) as ind1) , Aind ind2 -> + if eq_ind ind1 ind2 && compare_stack stk1 stk2 then - conv_stack env k stk1 stk2 cu + if Environ.polymorphic_ind ind1 env + then + let mib = Environ.lookup_mind mi env in + let ulen = Univ.UContext.size mib.Declarations.mind_universes in + match stk1 , stk2 with + | Zapp args1 :: stk1' , Zapp args2 :: stk2' -> + assert (ulen <= nargs args1) ; + assert (ulen <= nargs args2) ; + for i = 0 to ulen - 1 do + let a1 = uni_lvl_val (arg args1 i) in + let a2 = uni_lvl_val (arg args2 i) in + let result = Univ.Level.equal a1 a2 in + if not result + then raise NotConvertible + done ; + conv_arguments env ~from:ulen k args1 args2 + (conv_stack env k stk1' stk2' cu) + | _ -> raise NotConvertible + else + conv_stack env k stk1 stk2 cu else raise NotConvertible | Aid ik1, Aid ik2 -> if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then conv_stack env k stk1 stk2 cu else raise NotConvertible + | Atype u1 , Atype u2 -> + let u1 = Vm.instantiate_universe u1 stk1 in + let u2 = Vm.instantiate_universe u2 stk2 in + sort_cmp_universes env pb (Type u1) (Type u2) cu + | Atype _ , Aid _ + | Atype _ , Aind _ + | Aid _ , Atype _ | Aind _, _ | Aid _, _ -> raise NotConvertible -and conv_stack env k stk1 stk2 cu = +and conv_stack env ?from:(from=0) k stk1 stk2 cu = match stk1, stk2 with | [], [] -> cu | Zapp args1 :: stk1, Zapp args2 :: stk2 -> - conv_stack env k stk1 stk2 (conv_arguments env k args1 args2 cu) + conv_stack env k stk1 stk2 (conv_arguments env ~from:from k args1 args2 cu) | Zfix(f1,args1) :: stk1, Zfix(f2,args2) :: stk2 -> conv_stack env k stk1 stk2 - (conv_arguments env k args1 args2 (conv_fix env k f1 f2 cu)) + (conv_arguments env ~from:from k args1 args2 (conv_fix env k f1 f2 cu)) | Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 -> if check_switch sw1 sw2 then let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in @@ -144,13 +178,13 @@ and conv_cofix env k cf1 cf2 cu = conv_vect (conv_val env CONV (k + Array.length tcf1)) bcf1 bcf2 cu else raise NotConvertible -and conv_arguments env k args1 args2 cu = +and conv_arguments env ?from:(from=0) k args1 args2 cu = if args1 == args2 then cu else let n = nargs args1 in if Int.equal n (nargs args2) then let rcu = ref cu in - for i = 0 to n - 1 do + for i = from to n - 1 do rcu := conv_val env CONV k (arg args1 i) (arg args2 i) !rcu done; !rcu diff --git a/kernel/vm.ml b/kernel/vm.ml index eacd803fd4..858f546c60 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -121,12 +121,12 @@ type vswitch = { (* *) (* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ] *) (* - representation of [accu] : tag_[....] *) -(* -- tag <= 2 : encoding atom type (sorts, free vars, etc.) *) -(* -- 3_[accu|proj name] : a projection blocked by an accu *) -(* -- 4_[accu|fix_app] : a fixpoint blocked by an accu *) -(* -- 5_[accu|vswitch] : a match blocked by an accu *) -(* -- 6_[fcofix] : a cofix function *) -(* -- 7_[fcofix|val] : a cofix function, val represent the value *) +(* -- tag <= 3 : encoding atom type (sorts, free vars, etc.) *) +(* -- 10_[accu|proj name] : a projection blocked by an accu *) +(* -- 11_[accu|fix_app] : a fixpoint blocked by an accu *) +(* -- 12_[accu|vswitch] : a match blocked by an accu *) +(* -- 13_[fcofix] : a cofix function *) +(* -- 14_[fcofix|val] : a cofix function, val represent the value *) (* of the function applied to arg1 ... argn *) (* The [arguments] type, which is abstracted as an array, represents : *) (* tag[ _ | _ |v1|... | vn] *) @@ -136,7 +136,8 @@ type vswitch = { type atom = | Aid of Vars.id_key - | Aind of pinductive + | Aind of inductive + | Atype of Univ.universe (* Zippers *) @@ -159,6 +160,7 @@ type whd = | Vconstr_const of int | Vconstr_block of vblock | Vatom_stk of atom * stack + | Vuniv_level of Univ.universe_level (*************************************************) (* Destructors ***********************************) @@ -199,7 +201,9 @@ let rec whd_accu a stk = | [Zapp args] -> Vcofix(vcofix, res, Some args) | _ -> assert false end - | _ -> assert false + | tg -> + Errors.anomaly + Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg) external kind_of_closure : Obj.t -> int = "coq_kind_of_closure" @@ -212,22 +216,45 @@ let whd_val : values -> whd = if tag = accu_tag then ( if Int.equal (Obj.size o) 1 then Obj.obj o (* sort *) - else + else if is_accumulate (fun_code o) then whd_accu o [] - else (Vprod(Obj.obj o))) + else Vprod(Obj.obj o)) else if tag = Obj.closure_tag || tag = Obj.infix_tag then - ( match kind_of_closure o with + (match kind_of_closure o with | 0 -> Vfun(Obj.obj o) | 1 -> Vfix(Obj.obj o, None) | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o)) | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) | _ -> Errors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work")) - else - Vconstr_block(Obj.obj o) - + else + Vconstr_block(Obj.obj o) + +let uni_lvl_val : values -> Univ.universe_level = + fun v -> + let whd = Obj.magic v in + match whd with + | Vuniv_level lvl -> lvl + | _ -> + let pr = + let open Pp in + match whd with + | Vsort _ -> str "Vsort" + | Vprod _ -> str "Vprod" + | Vfun _ -> str "Vfun" + | Vfix _ -> str "Vfix" + | Vcofix _ -> str "Vcofix" + | Vconstr_const i -> str "Vconstr_const" + | Vconstr_block b -> str "Vconstr_block" + | Vatom_stk (a,stk) -> str "Vatom_stk" + | _ -> assert false + in + Errors.anomaly + Pp.( strbrk "Parsing virtual machine value expected universe level, got " + ++ pr) + (************************************************) -(* Abstrct machine ******************************) +(* Abstract machine *****************************) (************************************************) (* gestion de la pile *) @@ -299,6 +326,8 @@ let rec obj_of_str_const str = Obj.set_field res i (obj_of_str_const args.(i)) done; res + | Const_univ_level l -> Obj.repr (Vuniv_level l) + | Const_type u -> obj_of_atom (Atype u) let val_of_obj o = ((Obj.obj o) : values) @@ -317,11 +346,11 @@ let val_of_proj kn v = module IdKeyHash = struct - type t = pconstant tableKey - let equal = Names.eq_table_key (Univ.eq_puniverses Constant.equal) + type t = constant tableKey + let equal = Names.eq_table_key Constant.equal open Hashset.Combine let hash = function - | ConstKey (c,u) -> combinesmall 1 (Constant.hash c) + | ConstKey c -> combinesmall 1 (Constant.hash c) | VarKey id -> combinesmall 2 (Id.hash id) | RelKey i -> combinesmall 3 (Int.hash i) end @@ -606,3 +635,50 @@ let apply_whd k whd = interprete (fun_code to_up) (Obj.magic to_up) (Obj.magic to_up) 0 | Vatom_stk(a,stk) -> apply_stack (val_of_atom a) stk v + | Vuniv_level lvl -> assert false + +let instantiate_universe (u : Univ.universe) (stk : stack) : Univ.universe = + match stk with + | [] -> u + | [Zapp args] -> + assert (Univ.LSet.cardinal (Univ.Universe.levels u) = nargs args) ; + let _,mp = Univ.LSet.fold (fun key (i,mp) -> + let u = uni_lvl_val (arg args i) in + (i+1, Univ.LMap.add key (Univ.Universe.make u) mp)) + (Univ.Universe.levels u) + (0,Univ.LMap.empty) in + let subst = Univ.make_subst mp in + Univ.subst_univs_universe subst u + | _ -> + Errors.anomaly Pp.(str "ill-formed universe") + + +let rec pr_atom a = + Pp.(match a with + | Aid c -> str "Aid(" ++ (match c with + | ConstKey c -> Names.pr_con c + | RelKey i -> str "#" ++ int i + | _ -> str "...") ++ str ")" + | Aind (mi,i) -> str "Aind(" ++ Names.pr_mind mi ++ str "#" ++ int i ++ str ")" + | Atype _ -> str "Atype(") +and pr_whd w = + Pp.(match w with + | Vsort _ -> str "Vsort" + | Vprod _ -> str "Vprod" + | Vfun _ -> str "Vfun" + | Vfix _ -> str "Vfix" + | Vcofix _ -> str "Vcofix" + | Vconstr_const i -> str "Vconstr_const(" ++ int i ++ str ")" + | Vconstr_block b -> str "Vconstr_block" + | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")" + | Vuniv_level _ -> assert false) +and pr_stack stk = + Pp.(match stk with + | [] -> str "[]" + | s :: stk -> pr_zipper s ++ str " :: " ++ pr_stack stk) +and pr_zipper z = + Pp.(match z with + | Zapp args -> str "Zapp(len = " ++ int (nargs args) ++ str ")" + | Zfix (f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")" + | Zswitch s -> str "Zswitch(...)" + | Zproj c -> str "Zproj(" ++ Names.pr_con c ++ str ")") diff --git a/kernel/vm.mli b/kernel/vm.mli index 045d02333c..bc19786632 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -22,7 +22,8 @@ type arguments type atom = | Aid of Vars.id_key - | Aind of pinductive + | Aind of inductive + | Atype of Univ.universe (** Zippers *) @@ -45,19 +46,25 @@ type whd = | Vconstr_const of int | Vconstr_block of vblock | Vatom_stk of atom * stack + | Vuniv_level of Univ.universe_level + +val pr_atom : atom -> Pp.std_ppcmds +val pr_whd : whd -> Pp.std_ppcmds (** Constructors *) val val_of_str_const : structured_constant -> values val val_of_rel : int -> values val val_of_named : Id.t -> values -val val_of_constant : pconstant -> values +val val_of_constant : constant -> values external val_of_annot_switch : annot_switch -> values = "%identity" (** Destructors *) val whd_val : values -> whd +val uni_lvl_val : values -> Univ.universe_level +val instantiate_universe : Univ.universe -> stack -> Univ.universe (** Arguments *) -- cgit v1.2.3 From 9ce6802ea563437b15e45198f4d8d0f716a576bb Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 27 Oct 2015 23:27:50 +0100 Subject: Fix minor typo in native compiler. --- kernel/nativevalues.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel') diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index e4a7799933..40bef4bc67 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -10,7 +10,7 @@ open Names open Errors open Util -(** This modules defines the representation of values internally used by +(** This module defines the representation of values internally used by the native compiler *) type t = t -> t -- cgit v1.2.3 From 90dfacaacfec8265b11dc9291de9510f515c0081 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 27 Oct 2015 23:59:05 +0100 Subject: Conversion of polymorphic inductive types was incomplete in VM and native. Was showing up when comparing e.g. prod Type Type with prod Type Type (!) with a polymorphic prod. --- kernel/nativeconv.ml | 10 ++++++---- kernel/reduction.ml | 14 ++++++++------ kernel/reduction.mli | 7 ++++++- kernel/vconv.ml | 35 ++++++++++------------------------- 4 files changed, 30 insertions(+), 36 deletions(-) (limited to 'kernel') diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 7ae66c485a..0242fd461c 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -63,10 +63,12 @@ and conv_atom env pb lvl a1 a2 cu = | Ameta _, _ | _, Ameta _ | Aevar _, _ | _, Aevar _ -> assert false | Arel i1, Arel i2 -> if Int.equal i1 i2 then cu else raise NotConvertible - | Aind ind1, Aind ind2 -> - if eq_puniverses eq_ind ind1 ind2 then cu else raise NotConvertible - | Aconstant c1, Aconstant c2 -> - if eq_puniverses eq_constant c1 c2 then cu else raise NotConvertible + | Aind (ind1,u1), Aind (ind2,u2) -> + if eq_ind ind1 ind2 then convert_instances ~flex:false u1 u2 cu + else raise NotConvertible + | Aconstant (c1,u1), Aconstant (c2,u2) -> + if Constant.equal c1 c2 then convert_instances ~flex:true u1 u2 cu + else raise NotConvertible | Asort s1, Asort s2 -> sort_cmp_universes env pb s1 s2 cu | Avar id1, Avar id2 -> diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 2c111a55b5..892557ac6c 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -173,7 +173,7 @@ let is_cumul = function CUMUL -> true | CONV -> false type 'a universe_compare = { (* Might raise NotConvertible *) compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; - compare_instances: bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; + compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; } type 'a universe_state = 'a * 'a universe_compare @@ -185,8 +185,10 @@ type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.co let sort_cmp_universes env pb s0 s1 (u, check) = (check.compare env pb s0 s1 u, check) -let convert_instances flex u u' (s, check) = - (check.compare_instances flex u u' s, check) +(* [flex] should be true for constants, false for inductive types and + constructors. *) +let convert_instances ~flex u u' (s, check) = + (check.compare_instances ~flex u u' s, check) let conv_table_key infos k1 k2 cuniv = if k1 == k2 then cuniv else @@ -196,7 +198,7 @@ let conv_table_key infos k1 k2 cuniv = else let flex = evaluable_constant cst (info_env infos) && RedFlags.red_set (info_flags infos) (RedFlags.fCONST cst) - in convert_instances flex u u' cuniv + in convert_instances ~flex u u' cuniv | VarKey id, VarKey id' when Id.equal id id' -> cuniv | RelKey n, RelKey n' when Int.equal n n' -> cuniv | _ -> raise NotConvertible @@ -590,7 +592,7 @@ let check_sort_cmp_universes env pb s0 s1 univs = let checked_sort_cmp_universes env pb s0 s1 univs = check_sort_cmp_universes env pb s0 s1 univs; univs -let check_convert_instances _flex u u' univs = +let check_convert_instances ~flex u u' univs = if Univ.Instance.check_eq univs u u' then univs else raise NotConvertible @@ -630,7 +632,7 @@ let infer_cmp_universes env pb s0 s1 univs = | CONV -> infer_eq univs u1 u2) else univs -let infer_convert_instances flex u u' (univs,cstrs) = +let infer_convert_instances ~flex u u' (univs,cstrs) = (univs, Univ.enforce_eq_instances u u' cstrs) let inferred_universes : (Univ.universes * Univ.Constraint.t) universe_compare = diff --git a/kernel/reduction.mli b/kernel/reduction.mli index c3cc7b2b69..0df26d6276 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -37,7 +37,7 @@ type conv_pb = CONV | CUMUL type 'a universe_compare = { (* Might raise NotConvertible *) compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; - compare_instances: bool (* Instance of a flexible constant? *) -> + compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; } @@ -50,6 +50,11 @@ type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.co val sort_cmp_universes : env -> conv_pb -> sorts -> sorts -> 'a * 'a universe_compare -> 'a * 'a universe_compare +(* [flex] should be true for constants, false for inductive types and +constructors. *) +val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> + 'a * 'a universe_compare -> 'a * 'a universe_compare + val checked_universes : Univ.universes universe_compare val inferred_universes : (Univ.universes * Univ.Constraint.t) universe_compare diff --git a/kernel/vconv.ml b/kernel/vconv.ml index e0d9688486..2e519789e1 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -99,17 +99,15 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = let ulen = Univ.UContext.size mib.Declarations.mind_universes in match stk1 , stk2 with | Zapp args1 :: stk1' , Zapp args2 :: stk2' -> - assert (ulen <= nargs args1) ; - assert (ulen <= nargs args2) ; - for i = 0 to ulen - 1 do - let a1 = uni_lvl_val (arg args1 i) in - let a2 = uni_lvl_val (arg args2 i) in - let result = Univ.Level.equal a1 a2 in - if not result - then raise NotConvertible - done ; - conv_arguments env ~from:ulen k args1 args2 - (conv_stack env k stk1' stk2' cu) + assert (ulen <= nargs args1); + assert (ulen <= nargs args2); + let u1 = Array.init ulen (fun i -> uni_lvl_val (arg args1 i)) in + let u2 = Array.init ulen (fun i -> uni_lvl_val (arg args2 i)) in + let u1 = Univ.Instance.of_array u1 in + let u2 = Univ.Instance.of_array u2 in + let cu = convert_instances ~flex:false u1 u2 cu in + conv_arguments env ~from:ulen k args1 args2 + (conv_stack env k stk1' stk2' cu) | _ -> raise NotConvertible else conv_stack env k stk1 stk2 cu @@ -118,13 +116,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then conv_stack env k stk1 stk2 cu else raise NotConvertible - | Atype u1 , Atype u2 -> - let u1 = Vm.instantiate_universe u1 stk1 in - let u2 = Vm.instantiate_universe u2 stk2 in - sort_cmp_universes env pb (Type u1) (Type u2) cu - | Atype _ , Aid _ - | Atype _ , Aind _ - | Aid _ , Atype _ + | Atype _ , _ | _, Atype _ -> assert false | Aind _, _ | Aid _, _ -> raise NotConvertible and conv_stack env ?from:(from=0) k stk1 stk2 cu = @@ -190,13 +182,6 @@ and conv_arguments env ?from:(from=0) k args1 args2 cu = !rcu else raise NotConvertible -let rec eq_puniverses f (x,l1) (y,l2) cu = - if f x y then conv_universes l1 l2 cu - else raise NotConvertible - -and conv_universes l1 l2 cu = - if Univ.Instance.equal l1 l2 then cu else raise NotConvertible - let vm_conv_gen cv_pb env univs t1 t2 = try let v1 = val_of_constr env t1 in -- cgit v1.2.3 From 4f8a9d10123bd8aa4d17853a7248d3b3fe8a3625 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 28 Oct 2015 11:16:24 +0100 Subject: Refine Gregory Malecha's patch on VM and universe polymorphism. - Universes are now represented in the VM by a structured constant containing the global levels. This constant is applied to local level variables if any. - When reading back a universe, we perform the union of these levels and return a [Vsort]. - Fixed a bug: structured constants could contain local universe variables in constructor arguments, which has to be prevented. Was showing up for instance when evaluating [cons _ list (nil _)] with a polymorphic [list] type. - Fixed a bug: polymorphic inductive types can have an empty stack. Was showing up when evaluating [bool] with a polymorphic [bool] type. - Made a few cosmetic changes. Patch written with Benjamin Grégoire. --- kernel/cbytecodes.ml | 1 + kernel/cbytecodes.mli | 1 + kernel/cbytegen.ml | 92 ++++++++++++--------------- kernel/cemitcodes.ml | 2 +- kernel/vconv.ml | 3 +- kernel/vm.ml | 167 ++++++++++++++++++++++++-------------------------- kernel/vm.mli | 1 - 7 files changed, 124 insertions(+), 143 deletions(-) (limited to 'kernel') diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index b13b0607b3..0a24a75d68 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -19,6 +19,7 @@ type tag = int let accu_tag = 0 +let type_atom_tag = 2 let max_atom_tag = 2 let proj_tag = 3 let fix_app_tag = 4 diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index c35ef6920f..03ae6b9cdc 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -15,6 +15,7 @@ type tag = int val accu_tag : tag +val type_atom_tag : tag val max_atom_tag : tag val proj_tag : tag val fix_app_tag : tag diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index f9f72efdb9..1f7cc3c7a6 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -91,6 +91,7 @@ open Pre_env (* In Cfxe_t accumulators, we need to store [fcofixi] for testing *) (* conversion of cofixpoints (which is intentional). *) +type argument = ArgConstr of Constr.t | ArgUniv of Univ.Level.t let empty_fv = { size= 0; fv_rev = [] } @@ -218,21 +219,6 @@ let pos_rel i r sz = r.in_env := { size = pos+1; fv_rev = db:: env.fv_rev}; Kenvacc(r.offset + pos) -(* -let pos_poly_inst idu r = - let env = !(r.in_env) in - let f = function - | FVpoly_inst i -> Univ.eq_puniverses Names.Constant.equal idu i - | _ -> false - in - try Kenvacc (r.offset + env.size - (find_at f env.fv_rev)) - with Not_found -> - let pos = env.size in - let db = FVpoly_inst idu in - r.in_env := { size = pos+1; fv_rev = db:: env.fv_rev}; - Kenvacc(r.offset + pos) -*) - let pos_universe_var i r sz = if i < r.nb_uni_stack then Kacc (sz - r.nb_stack - (r.nb_uni_stack - i)) @@ -494,9 +480,9 @@ let rec str_const c = end | _ -> Bconstr c end - | Ind (ind,_) -> + | Ind (ind,u) when Univ.Instance.is_empty u -> Bstrconst (Const_ind ind) - | Construct (((kn,j),i),u) -> + | Construct (((kn,j),i),_) -> begin (* spiwack: tries first to apply the run-time compilation behavior of the constructor, as in 2/ above *) @@ -571,10 +557,6 @@ let rec get_alias env kn = | BCalias kn' -> get_alias env kn' | _ -> kn) -(* Compiling expressions *) - -type ('a,'b) sum = Inl of 'a | Inr of 'b - (* sz is the size of the local stack *) let rec compile_constr reloc c sz cont = match kind_of_term c with @@ -592,39 +574,43 @@ let rec compile_constr reloc c sz cont = | Rel i -> pos_rel i reloc sz :: cont | Var id -> pos_named id reloc :: cont | Const (kn,u) -> compile_const reloc kn u [||] sz cont - | Ind (i,u) -> + | Ind (ind,u) -> + let bcst = Bstrconst (Const_ind ind) in if Univ.Instance.is_empty u then - compile_str_cst reloc (str_const c) sz cont + compile_str_cst reloc bcst sz cont else comp_app compile_str_cst compile_universe reloc - (str_const c) + bcst (Univ.Instance.to_array u) sz cont | Sort (Prop _) | Construct _ -> compile_str_cst reloc (str_const c) sz cont | Sort (Type u) -> - begin - let levels = Univ.Universe.levels u in - if Univ.LSet.exists (fun x -> Univ.Level.var_index x <> None) levels - then - (** TODO(gmalecha): Fix this **) - (** NOTE: This relies on the order of iteration to be consistent - **) - let level_vars = - List.map_filter (fun x -> Univ.Level.var_index x) - (Univ.LSet.elements levels) - in - let compile_get_univ reloc idx sz cont = + (* We separate global and local universes in [u]. The former will be part + of the structured constant, while the later (if any) will be applied as + arguments. *) + let open Univ in begin + let levels = Universe.levels u in + let global_levels = + LSet.filter (fun x -> Level.var_index x = None) levels + in + let local_levels = + List.map_filter (fun x -> Level.var_index x) + (LSet.elements levels) + in + (* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *) + let uglob = + LSet.fold (fun lvl u -> Universe.sup u (Universe.make lvl)) global_levels Universe.type0m + in + if local_levels = [] then + compile_str_cst reloc (Bstrconst (Const_sorts (Type uglob))) sz cont + else + let compile_get_univ reloc idx sz cont = compile_fv_elem reloc (FVuniv_var idx) sz cont in comp_app compile_str_cst compile_get_univ reloc - (Bstrconst (Const_type u)) - (Array.of_list level_vars) - sz - cont - else - compile_str_cst reloc (str_const c) sz cont + (Bstrconst (Const_type u)) (Array.of_list local_levels) sz cont end | LetIn(_,xb,_,body) -> compile_constr reloc xb sz @@ -831,8 +817,7 @@ and compile_universe reloc uni sz cont = | None -> Kconst (Const_univ_level uni) :: cont | Some idx -> pos_universe_var idx reloc sz :: cont -and compile_const = - fun reloc-> fun kn u -> fun args -> fun sz -> fun cont -> +and compile_const reloc kn u args sz cont = let nargs = Array.length args in (* spiwack: checks if there is a specific way to compile the constant if there is not, Not_found is raised, and the function @@ -850,18 +835,19 @@ and compile_const = compile_get_global reloc (kn,u) sz cont) compile_constr reloc () args sz cont else - let compile_either reloc constr_or_uni sz cont = + let compile_arg reloc constr_or_uni sz cont = match constr_or_uni with - | Inl cst -> compile_constr reloc cst sz cont - | Inr uni -> compile_universe reloc uni sz cont - in - (** TODO(gmalecha): This can be more efficient **) - let all = - Array.of_list (List.map (fun x -> Inr x) (Array.to_list (Univ.Instance.to_array u)) @ - List.map (fun x -> Inl x) (Array.to_list args)) + | ArgConstr cst -> compile_constr reloc cst sz cont + | ArgUniv uni -> compile_universe reloc uni sz cont in + let u = Univ.Instance.to_array u in + let lu = Array.length u in + let all = + Array.init (lu + Array.length args) + (fun i -> if i < lu then ArgUniv u.(i) else ArgConstr args.(i-lu)) + in comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont) - compile_either reloc () all sz cont + compile_arg reloc () all sz cont let is_univ_copy max u = let u = Univ.Instance.to_array u in diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 2a70d0b1b7..ef0c9af4ff 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -307,7 +307,7 @@ type to_patch = emitcodes * (patch list) * fv (* Substitution *) let rec subst_strcst s sc = match sc with - | Const_sorts _ | Const_b0 _ -> sc + | Const_sorts _ | Const_b0 _ | Const_univ_level _ | Const_type _ -> sc | Const_proj p -> Const_proj (subst_constant s p) | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args) | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i) diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 2e519789e1..4610dbcb07 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -98,6 +98,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = let mib = Environ.lookup_mind mi env in let ulen = Univ.UContext.size mib.Declarations.mind_universes in match stk1 , stk2 with + | [], [] -> assert (Int.equal ulen 0); cu | Zapp args1 :: stk1' , Zapp args2 :: stk2' -> assert (ulen <= nargs args1); assert (ulen <= nargs args2); @@ -108,7 +109,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = let cu = convert_instances ~flex:false u1 u2 cu in conv_arguments env ~from:ulen k args1 args2 (conv_stack env k stk1' stk2' cu) - | _ -> raise NotConvertible + | _, _ -> assert false (* Should not happen if problem is well typed *) else conv_stack env k stk1 stk2 cu else raise NotConvertible diff --git a/kernel/vm.ml b/kernel/vm.ml index 858f546c60..64ddc43766 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -162,16 +162,96 @@ type whd = | Vatom_stk of atom * stack | Vuniv_level of Univ.universe_level +(************************************************) +(* Abstract machine *****************************) +(************************************************) + +(* gestion de la pile *) +external push_ra : tcode -> unit = "coq_push_ra" +external push_val : values -> unit = "coq_push_val" +external push_arguments : arguments -> unit = "coq_push_arguments" +external push_vstack : vstack -> unit = "coq_push_vstack" + + +(* interpreteur *) +external interprete : tcode -> values -> vm_env -> int -> values = + "coq_interprete_ml" + + + +(* Functions over arguments *) +let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2 +let arg args i = + if 0 <= i && i < (nargs args) then + val_of_obj (Obj.field (Obj.repr args) (i+2)) + else invalid_arg + ("Vm.arg size = "^(string_of_int (nargs args))^ + " acces "^(string_of_int i)) + +(* Apply a value to arguments contained in [vargs] *) +let apply_arguments vf vargs = + let n = nargs vargs in + if Int.equal n 0 then vf + else + begin + push_ra stop; + push_arguments vargs; + interprete (fun_code vf) vf (Obj.magic vf) (n - 1) + end + +(* Apply value [vf] to an array of argument values [varray] *) +let apply_varray vf varray = + let n = Array.length varray in + if Int.equal n 0 then vf + else + begin + push_ra stop; + push_vstack varray; + interprete (fun_code vf) vf (Obj.magic vf) (n - 1) + end + (*************************************************) (* Destructors ***********************************) (*************************************************) +let uni_lvl_val (v : values) : Univ.universe_level = + let whd = Obj.magic v in + match whd with + | Vuniv_level lvl -> lvl + | _ -> + let pr = + let open Pp in + match whd with + | Vsort _ -> str "Vsort" + | Vprod _ -> str "Vprod" + | Vfun _ -> str "Vfun" + | Vfix _ -> str "Vfix" + | Vcofix _ -> str "Vcofix" + | Vconstr_const i -> str "Vconstr_const" + | Vconstr_block b -> str "Vconstr_block" + | Vatom_stk (a,stk) -> str "Vatom_stk" + | _ -> assert false + in + Errors.anomaly + Pp.( strbrk "Parsing virtual machine value expected universe level, got " + ++ pr) + let rec whd_accu a stk = let stk = if Int.equal (Obj.size a) 2 then stk else Zapp (Obj.obj a) :: stk in let at = Obj.field a 1 in match Obj.tag at with + | i when Int.equal i type_atom_tag -> + begin match stk with + | [Zapp args] -> + let u = ref (Obj.obj (Obj.field at 0)) in + for i = 0 to nargs args - 1 do + u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i))) + done; + Vsort (Type !u) + | _ -> assert false + end | i when i <= max_atom_tag -> Vatom_stk(Obj.magic at, stk) | i when Int.equal i proj_tag -> @@ -230,77 +310,6 @@ let whd_val : values -> whd = else Vconstr_block(Obj.obj o) -let uni_lvl_val : values -> Univ.universe_level = - fun v -> - let whd = Obj.magic v in - match whd with - | Vuniv_level lvl -> lvl - | _ -> - let pr = - let open Pp in - match whd with - | Vsort _ -> str "Vsort" - | Vprod _ -> str "Vprod" - | Vfun _ -> str "Vfun" - | Vfix _ -> str "Vfix" - | Vcofix _ -> str "Vcofix" - | Vconstr_const i -> str "Vconstr_const" - | Vconstr_block b -> str "Vconstr_block" - | Vatom_stk (a,stk) -> str "Vatom_stk" - | _ -> assert false - in - Errors.anomaly - Pp.( strbrk "Parsing virtual machine value expected universe level, got " - ++ pr) - -(************************************************) -(* Abstract machine *****************************) -(************************************************) - -(* gestion de la pile *) -external push_ra : tcode -> unit = "coq_push_ra" -external push_val : values -> unit = "coq_push_val" -external push_arguments : arguments -> unit = "coq_push_arguments" -external push_vstack : vstack -> unit = "coq_push_vstack" - - -(* interpreteur *) -external interprete : tcode -> values -> vm_env -> int -> values = - "coq_interprete_ml" - - - -(* Functions over arguments *) -let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2 -let arg args i = - if 0 <= i && i < (nargs args) then - val_of_obj (Obj.field (Obj.repr args) (i+2)) - else invalid_arg - ("Vm.arg size = "^(string_of_int (nargs args))^ - " acces "^(string_of_int i)) - -(* Apply a value to arguments contained in [vargs] *) -let apply_arguments vf vargs = - let n = nargs vargs in - if Int.equal n 0 then vf - else - begin - push_ra stop; - push_arguments vargs; - interprete (fun_code vf) vf (Obj.magic vf) (n - 1) - end - -(* Apply value [vf] to an array of argument values [varray] *) -let apply_varray vf varray = - let n = Array.length varray in - if Int.equal n 0 then vf - else - begin - push_ra stop; - push_vstack varray; - interprete (fun_code vf) vf (Obj.magic vf) (n - 1) - end - (**********************************************) (* Constructors *******************************) (**********************************************) @@ -637,22 +646,6 @@ let apply_whd k whd = apply_stack (val_of_atom a) stk v | Vuniv_level lvl -> assert false -let instantiate_universe (u : Univ.universe) (stk : stack) : Univ.universe = - match stk with - | [] -> u - | [Zapp args] -> - assert (Univ.LSet.cardinal (Univ.Universe.levels u) = nargs args) ; - let _,mp = Univ.LSet.fold (fun key (i,mp) -> - let u = uni_lvl_val (arg args i) in - (i+1, Univ.LMap.add key (Univ.Universe.make u) mp)) - (Univ.Universe.levels u) - (0,Univ.LMap.empty) in - let subst = Univ.make_subst mp in - Univ.subst_univs_universe subst u - | _ -> - Errors.anomaly Pp.(str "ill-formed universe") - - let rec pr_atom a = Pp.(match a with | Aid c -> str "Aid(" ++ (match c with diff --git a/kernel/vm.mli b/kernel/vm.mli index bc19786632..43a42eb9c4 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -64,7 +64,6 @@ external val_of_annot_switch : annot_switch -> values = "%identity" val whd_val : values -> whd val uni_lvl_val : values -> Univ.universe_level -val instantiate_universe : Univ.universe -> stack -> Univ.universe (** Arguments *) -- cgit v1.2.3 From 908dcd613b12645f3b62bf44c2696b80a0b16940 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Oct 2015 16:46:42 +0100 Subject: Avoid type checking private_constants (side_eff) again during Qed (#4357). Side effects are now an opaque data type, called private_constant, you can only obtain from safe_typing. When add_constant is called on a definition_entry that contains private constants, they are either - inlined in the main proof term but not re-checked - declared globally without re-checking them As a safety measure, the opaque data type contains a pointer to the revstruct (an internal field of safe_env that changes every time a new constant is added), and such pointer is compared with the current value store in safe_env when the private_constant is inlined. Only when the comparison is successful the private_constant is not re-checked. Otherwise else it is. In short, we accept into the kernel private constant only when they arrive in the very same order and on top of the very same env they arrived when we fist checked them. Note: private_constants produced by workers never pass the safety measure (the revstruct pointer is an Ephemeron). Sending back the entire revstruct is possible but: 1. we lack a way to quickly compare two revstructs, 2. it can be large. --- kernel/declarations.mli | 6 -- kernel/declareops.ml | 18 ++--- kernel/declareops.mli | 12 +--- kernel/entries.mli | 25 +++++-- kernel/opaqueproof.ml | 5 +- kernel/safe_typing.ml | 103 ++++++++++++++++++++------ kernel/safe_typing.mli | 41 +++++++++-- kernel/term_typing.ml | 188 +++++++++++++++++++++++++++++++++++++++++++----- kernel/term_typing.mli | 33 +++++++-- 9 files changed, 341 insertions(+), 90 deletions(-) (limited to 'kernel') diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 7def963e73..dc5c17a75b 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -79,12 +79,6 @@ type constant_body = { const_proj : projection_body option; const_inline_code : bool } -type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ] - -type side_effect = - | SEsubproof of constant * constant_body * seff_env - | SEscheme of (inductive * constant * constant_body * seff_env) list * string - (** {6 Representation of mutual inductive types in the kernel } *) type recarg = diff --git a/kernel/declareops.ml b/kernel/declareops.ml index a7051d5c13..248504c1b1 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -304,17 +304,7 @@ let hcons_mind mib = (** {6 Stm machinery } *) -let string_of_side_effect = function - | SEsubproof (c,_,_) -> Names.string_of_con c - | SEscheme (cl,_) -> - String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) -type side_effects = side_effect list -let no_seff = ([] : side_effects) -let iter_side_effects f l = List.iter f (List.rev l) -let fold_side_effects f a l = List.fold_left f a l -let uniquize_side_effects l = List.rev (CList.uniquize (List.rev l)) -let union_side_effects l1 l2 = l1 @ l2 -let flatten_side_effects l = List.flatten l -let side_effects_of_list l = l -let cons_side_effects x l = x :: l -let side_effects_is_empty = List.is_empty +let string_of_side_effect { Entries.eff } = match eff with + | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.string_of_con c ^ ")" + | Entries.SEscheme (cl,_) -> + "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) ^ ")" diff --git a/kernel/declareops.mli b/kernel/declareops.mli index ce65af975e..1b87009589 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -9,6 +9,7 @@ open Declarations open Mod_subst open Univ +open Entries (** Operations concerning types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) @@ -49,17 +50,6 @@ val is_opaque : constant_body -> bool val string_of_side_effect : side_effect -> string -type side_effects -val no_seff : side_effects -val iter_side_effects : (side_effect -> unit) -> side_effects -> unit -val fold_side_effects : ('a -> side_effect -> 'a) -> 'a -> side_effects -> 'a -val uniquize_side_effects : side_effects -> side_effects -val union_side_effects : side_effects -> side_effects -> side_effects -val flatten_side_effects : side_effects list -> side_effects -val side_effects_of_list : side_effect list -> side_effects -val cons_side_effects : side_effect -> side_effects -> side_effects -val side_effects_is_empty : side_effects -> bool - (** {6 Inductive types} *) val eq_recarg : recarg -> recarg -> bool diff --git a/kernel/entries.mli b/kernel/entries.mli index 303d27d355..e058519e96 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -54,11 +54,11 @@ type mutual_inductive_entry = { mind_entry_private : bool option } (** {6 Constants (Definition/Axiom) } *) -type proof_output = constr Univ.in_universe_context_set * Declareops.side_effects -type const_entry_body = proof_output Future.computation +type 'a proof_output = constr Univ.in_universe_context_set * 'a +type 'a const_entry_body = 'a proof_output Future.computation -type definition_entry = { - const_entry_body : const_entry_body; +type 'a definition_entry = { + const_entry_body : 'a const_entry_body; (* List of section variables *) const_entry_secctx : Context.section_context option; (* State id on which the completion of type checking is reported *) @@ -78,8 +78,8 @@ type projection_entry = { proj_entry_ind : mutual_inductive; proj_entry_arg : int } -type constant_entry = - | DefinitionEntry of definition_entry +type 'a constant_entry = + | DefinitionEntry of 'a definition_entry | ParameterEntry of parameter_entry | ProjectionEntry of projection_entry @@ -96,3 +96,16 @@ type module_entry = | MType of module_params_entry * module_struct_entry | MExpr of module_params_entry * module_struct_entry * module_struct_entry option + +type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ] + +type side_eff = + | SEsubproof of constant * Declarations.constant_body * seff_env + | SEscheme of (inductive * constant * Declarations.constant_body * seff_env) list * string + +type side_effect = { + from_env : Declarations.structure_body Ephemeron.key; + eff : side_eff; +} + +type side_effects = side_effect list diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 9f4361f401..badb15b561 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -43,7 +43,10 @@ let set_indirect_univ_accessor f = (get_univ := f) let create cu = Direct ([],cu) let turn_indirect dp o (prfs,odp) = match o with - | Indirect _ -> Errors.anomaly (Pp.str "Already an indirect opaque") + | Indirect (_,_,i) -> + if not (Int.Map.mem i prfs) + then Errors.anomaly (Pp.str "Indirect in a different table") + else Errors.anomaly (Pp.str "Already an indirect opaque") | Direct (d,cu) -> let cu = Future.chain ~pure:true cu (fun (c, u) -> hcons_constr c, u) in let id = Int.Map.cardinal prfs in diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ec245b0648..b71cd31b5c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -207,15 +207,55 @@ let get_opaque_body env cbo = (Opaqueproof.force_proof (Environ.opaque_tables env) opaque, Opaqueproof.force_constraints (Environ.opaque_tables env) opaque) -let sideff_of_con env c = +type private_constant = Entries.side_effect +type private_constants = private_constant list + +type private_constant_role = Term_typing.side_effect_role = + | Subproof + | Schema of inductive * string + +let empty_private_constants = [] +let add_private x xs = x :: xs +let concat_private xs ys = xs @ ys +let mk_pure_proof = Term_typing.mk_pure_proof +let inline_private_constants_in_constr = Term_typing.handle_side_effects +let inline_private_constants_in_definition_entry = Term_typing.handle_entry_side_effects +let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x) + +let constant_entry_of_private_constant = function + | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } -> + [ kn, Term_typing.constant_entry_of_side_effect cb eff_env ] + | { Entries.eff = Entries.SEscheme (l,_) } -> + List.map (fun (_,kn,cb,eff_env) -> + kn, Term_typing.constant_entry_of_side_effect cb eff_env) l + +let private_con_of_con env c = let cbo = Environ.lookup_constant c env.env in - SEsubproof (c, cbo, get_opaque_body env.env cbo) -let sideff_of_scheme kind env cl = - SEscheme( - List.map (fun (i,c) -> - let cbo = Environ.lookup_constant c env.env in - i, c, cbo, get_opaque_body env.env cbo) cl, - kind) + { Entries.from_env = Ephemeron.create env.revstruct; + Entries.eff = Entries.SEsubproof (c,cbo,get_opaque_body env.env cbo) } + +let private_con_of_scheme ~kind env cl = + { Entries.from_env = Ephemeron.create env.revstruct; + Entries.eff = Entries.SEscheme( + List.map (fun (i,c) -> + let cbo = Environ.lookup_constant c env.env in + i, c, cbo, get_opaque_body env.env cbo) cl, + kind) } + +let universes_of_private eff = + let open Declarations in + List.fold_left (fun acc { Entries.eff } -> + match eff with + | Entries.SEscheme (l,s) -> + List.fold_left (fun acc (_,_,cb,c) -> + let acc = match c with + | `Nothing -> acc + | `Opaque (_, ctx) -> ctx :: acc in + if cb.const_polymorphic then acc + else (Univ.ContextSet.of_context cb.const_universes) :: acc) + acc l + | Entries.SEsubproof _ -> acc) + [] eff let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env @@ -337,7 +377,7 @@ let safe_push_named (id,_,_ as d) env = let push_named_def (id,de) senv = - let c,typ,univs = Term_typing.translate_local_def senv.env id de in + let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in let poly = de.Entries.const_entry_polymorphic in let univs = Univ.ContextSet.of_context univs in let c, univs = match c with @@ -442,19 +482,16 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver } (** Insertion of constants and parameters in environment *) type global_declaration = - | ConstantEntry of Entries.constant_entry + | ConstantEntry of bool * private_constants Entries.constant_entry | GlobalRecipe of Cooking.recipe -let add_constant dir l decl senv = - let kn = make_con senv.modpath dir l in - let cb = match decl with - | ConstantEntry ce -> Term_typing.translate_constant senv.env kn ce - | GlobalRecipe r -> - let cb = Term_typing.translate_recipe senv.env kn r in - if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb - in +type exported_private_constant = + constant * private_constants Entries.constant_entry * private_constant_role + +let add_constant_aux no_section senv (kn, cb) = + let l = pi3 (Constant.repr3 kn) in let cb, otab = match cb.const_body with - | OpaqueDef lc when DirPath.is_empty dir -> + | OpaqueDef lc when no_section -> (* In coqc, opaque constants outside sections will be stored indirectly in a specific table *) let od, otab = @@ -471,7 +508,33 @@ let add_constant dir l decl senv = (Mod_subst.add_inline_delta_resolver (user_con kn) (lev,None)) senv' | _ -> senv' in - kn, senv'' + senv'' + +let add_constant dir l decl senv = + let kn = make_con senv.modpath dir l in + let no_section = DirPath.is_empty dir in + let seff_to_export, decl = + match decl with + | ConstantEntry (true, ce) -> + let exports, ce = + Term_typing.validate_side_effects_for_export + senv.revstruct senv.env ce in + exports, ConstantEntry (false, ce) + | _ -> [], decl + in + let senv = + List.fold_left (add_constant_aux no_section) senv + (List.map (fun (kn,cb,_,_) -> kn, cb) seff_to_export) in + let senv = + let cb = + match decl with + | ConstantEntry (export_seff,ce) -> + Term_typing.translate_constant senv.revstruct senv.env kn ce + | GlobalRecipe r -> + let cb = Term_typing.translate_recipe senv.env kn r in + if no_section then Declareops.hcons_const_body cb else cb in + add_constant_aux no_section senv (kn, cb) in + (kn, List.map (fun (kn,_,ce,r) -> kn, ce, r) seff_to_export), senv (** Insertion of inductive types *) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index eac08eb834..2214cf8bb8 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -39,10 +39,30 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment (** {6 Stm machinery } *) -val sideff_of_con : safe_environment -> constant -> Declarations.side_effect -val sideff_of_scheme : - string -> safe_environment -> (inductive * constant) list -> - Declarations.side_effect +type private_constant +type private_constants + +type private_constant_role = + | Subproof + | Schema of inductive * string + +val side_effects_of_private_constants : + private_constants -> Entries.side_effects + +val empty_private_constants : private_constants +val add_private : private_constant -> private_constants -> private_constants +val concat_private : private_constants -> private_constants -> private_constants + +val private_con_of_con : safe_environment -> constant -> private_constant +val private_con_of_scheme : kind:string -> safe_environment -> (inductive * constant) list -> private_constant + +val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output +val inline_private_constants_in_constr : + Environ.env -> Constr.constr -> private_constants -> Constr.constr +val inline_private_constants_in_definition_entry : + Environ.env -> private_constants Entries.definition_entry -> private_constants Entries.definition_entry + +val universes_of_private : private_constants -> Univ.universe_context_set list val is_curmod_library : safe_environment -> bool @@ -63,16 +83,23 @@ val push_named_assum : (** Returns the full universe context necessary to typecheck the definition (futures are forced) *) val push_named_def : - Id.t * Entries.definition_entry -> Univ.universe_context_set safe_transformer + Id.t * private_constants Entries.definition_entry -> Univ.universe_context_set safe_transformer (** Insertion of global axioms or definitions *) type global_declaration = - | ConstantEntry of Entries.constant_entry + (* bool: export private constants *) + | ConstantEntry of bool * private_constants Entries.constant_entry | GlobalRecipe of Cooking.recipe +type exported_private_constant = + constant * private_constants Entries.constant_entry * private_constant_role + +(** returns the main constant plus a list of auxiliary constants (empty + unless one requires the side effects to be exported) *) val add_constant : - DirPath.t -> Label.t -> global_declaration -> constant safe_transformer + DirPath.t -> Label.t -> global_declaration -> + (constant * exported_private_constant list) safe_transformer (** Adding an inductive type *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index cab99077f0..d75bd73fb6 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -43,10 +43,29 @@ let map_option_typ = function None -> `None | Some x -> `Some x (* Insertion of constants and parameters in environment. *) -let mk_pure_proof c = (c, Univ.ContextSet.empty), Declareops.no_seff +let mk_pure_proof c = (c, Univ.ContextSet.empty), [] + +let equal_eff e1 e2 = + let open Entries in + match e1, e2 with + | { eff = SEsubproof (c1,_,_) }, { eff = SEsubproof (c2,_,_) } -> + Names.Constant.equal c1 c2 + | { eff = SEscheme (cl1,_) }, { eff = SEscheme (cl2,_) } -> + CList.for_all2eq + (fun (_,c1,_,_) (_,c2,_,_) -> Names.Constant.equal c1 c2) + cl1 cl2 + | _ -> false + +let rec uniq_seff = function + | [] -> [] + | x :: xs -> x :: uniq_seff (List.filter (fun y -> not (equal_eff x y)) xs) +(* The list of side effects is in reverse order (most recent first). + * To keep the "tological" order between effects we have to uniqize from the + * tail *) +let uniq_seff l = List.rev (uniq_seff (List.rev l)) let handle_side_effects env body ctx side_eff = - let handle_sideff (t,ctx) se = + let handle_sideff (t,ctx,sl) { eff = se; from_env = mb } = let cbl = match se with | SEsubproof (c,cb,b) -> [c,cb,b] | SEscheme (cl,_) -> List.map (fun (_,c,cb,b) -> c,cb,b) cl in @@ -65,7 +84,7 @@ let handle_side_effects env body ctx side_eff = let rec sub_body c u b i x = match kind_of_term x with | Const (c',u') when eq_constant c c' -> Vars.subst_instance_constr u' b - | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub_body c u b i x) i x in + | _ -> map_constr_with_binders ((+) 1) (sub_body c u b) i x in let fix_body (c,cb,b) (t,ctx) = match cb.const_body, b with | Def b, _ -> @@ -87,17 +106,60 @@ let handle_side_effects env body ctx side_eff = let t = sub c 1 (Vars.lift 1 t) in mkApp (mkLambda (cname c, b_ty, t), [|b|]), Univ.ContextSet.union ctx - (Univ.ContextSet.of_context cb.const_universes) + (Univ.ContextSet.of_context cb.const_universes) else let univs = cb.const_universes in sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t), ctx | _ -> assert false in - List.fold_right fix_body cbl (t,ctx) + let t, ctx = List.fold_right fix_body cbl (t,ctx) in + t, ctx, (mb,List.length cbl) :: sl in (* CAVEAT: we assure a proper order *) - Declareops.fold_side_effects handle_sideff (body,ctx) - (Declareops.uniquize_side_effects side_eff) + List.fold_left handle_sideff (body,ctx,[]) (uniq_seff side_eff) + +let check_signatures curmb sl = + let is_direct_ancestor (sl, curmb) (mb, how_many) = + match curmb with + | None -> None, None + | Some curmb -> + try + let mb = Ephemeron.get mb in + match sl with + | None -> sl, None + | Some n -> + if List.length mb >= how_many && CList.skipn how_many mb == curmb + then Some (n + how_many), Some mb + else None, None + with Ephemeron.InvalidKey -> None, None in + let sl, _ = List.fold_left is_direct_ancestor (Some 0,Some curmb) sl in + sl + +let trust_seff sl b e = + let rec aux sl b e acc = + match sl, kind_of_term b with + | (None|Some 0), _ -> b, e, acc + | Some sl, LetIn (n,c,ty,bo) -> + aux (Some (sl-1)) bo + (Environ.push_rel (n,Some c,ty) e) (`Let(n,c,ty)::acc) + | Some sl, App(hd,arg) -> + begin match kind_of_term hd with + | Lambda (n,ty,bo) -> + aux (Some (sl-1)) bo + (Environ.push_rel (n,None,ty) e) (`Cut(n,ty,arg)::acc) + | _ -> assert false + end + | _ -> assert false + in + aux sl b e [] + +let rec unzip ctx j = + match ctx with + | [] -> j + | `Let (n,c,ty) :: ctx -> + unzip ctx { j with uj_val = mkLetIn (n,c,ty,j.uj_val) } + | `Cut (n,ty,arg) :: ctx -> + unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) } let hcons_j j = { uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type} @@ -105,7 +167,7 @@ let hcons_j j = let feedback_completion_typecheck = Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete) -let infer_declaration env kn dcl = +let infer_declaration ~trust env kn dcl = match dcl with | ParameterEntry (ctx,poly,(t,uctx),nl) -> let env = push_context ~strict:(not poly) uctx env in @@ -124,9 +186,14 @@ let infer_declaration env kn dcl = let tyj = infer_type env typ in let proofterm = Future.chain ~greedy:true ~pure:true body (fun ((body, ctx),side_eff) -> - let body,ctx = handle_side_effects env body ctx side_eff in + let body, ctx, signatures = + handle_side_effects env body ctx side_eff in + let trusted_signatures = check_signatures trust signatures in let env' = push_context_set ctx env in - let j = infer env' body in + let j = + let body, env', zip_ctx = trust_seff trusted_signatures body env' in + let j = infer env' body in + unzip zip_ctx j in let j = hcons_j j in let subst = Univ.LMap.empty in let _typ = constrain_type env' j c.const_entry_polymorphic subst @@ -143,7 +210,7 @@ let infer_declaration env kn dcl = let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let (body, ctx), side_eff = Future.join body in let univsctx = Univ.ContextSet.of_context c.const_entry_universes in - let body, ctx = handle_side_effects env body + let body, ctx, _ = handle_side_effects env body (Univ.ContextSet.union univsctx ctx) side_eff in let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in @@ -294,8 +361,93 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) (*s Global and local constant declaration. *) -let translate_constant env kn ce = - build_constant_declaration kn env (infer_declaration env (Some kn) ce) +let translate_constant mb env kn ce = + build_constant_declaration kn env + (infer_declaration ~trust:mb env (Some kn) ce) + +let constant_entry_of_side_effect cb u = + let pt = + match cb.const_body, u with + | OpaqueDef _, `Opaque (b, c) -> b, c + | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty + | _ -> assert false in + DefinitionEntry { + const_entry_body = Future.from_val (pt, []); + const_entry_secctx = None; + const_entry_feedback = None; + const_entry_type = + (match cb.const_type with RegularArity t -> Some t | _ -> None); + const_entry_polymorphic = cb.const_polymorphic; + const_entry_universes = cb.const_universes; + const_entry_opaque = Declareops.is_opaque cb; + const_entry_inline_code = cb.const_inline_code } +;; + +let turn_direct (kn,cb,u,r as orig) = + match cb.const_body, u with + | OpaqueDef _, `Opaque (b,c) -> + let pt = Future.from_val (b,c) in + kn, { cb with const_body = OpaqueDef (Opaqueproof.create pt) }, u, r + | _ -> orig +;; + +type side_effect_role = + | Subproof + | Schema of inductive * string + +type exported_side_effect = + constant * constant_body * side_effects Entries.constant_entry * side_effect_role + +let validate_side_effects_for_export mb env ce = + match ce with + | ParameterEntry _ | ProjectionEntry _ -> [], ce + | DefinitionEntry c -> + let { const_entry_body = body } = c in + let _, eff = Future.force body in + let ce = DefinitionEntry { c with + const_entry_body = Future.chain ~greedy:true ~pure:true body + (fun (b_ctx, _) -> b_ctx, []) } in + let not_exists (c,_,_,_) = + try ignore(Environ.lookup_constant c env); false + with Not_found -> true in + let aux (acc,sl) { eff = se; from_env = mb } = + let cbl = match se with + | SEsubproof (c,cb,b) -> [c,cb,b,Subproof] + | SEscheme (cl,k) -> + List.map (fun (i,c,cb,b) -> c,cb,b,Schema(i,k)) cl in + let cbl = List.filter not_exists cbl in + if cbl = [] then acc, sl + else cbl :: acc, (mb,List.length cbl) :: sl in + let seff, signatures = List.fold_left aux ([],[]) (uniq_seff eff) in + let trusted = check_signatures mb signatures in + let push_seff env = function + | kn, cb, `Nothing, _ -> + Environ.add_constant kn cb env + | kn, cb, `Opaque(_, ctx), _ -> + let env = Environ.add_constant kn cb env in + Environ.push_context_set + ~strict:(not cb.const_polymorphic) ctx env in + let rec translate_seff sl seff acc env = + match sl, seff with + | _, [] -> List.rev acc, ce + | (None | Some 0), cbs :: rest -> + let env, cbs = + List.fold_left (fun (env,cbs) (kn, ocb, u, r) -> + let ce = constant_entry_of_side_effect ocb u in + let cb = translate_constant mb env kn ce in + (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs)) + (env,[]) cbs in + translate_seff sl rest (cbs @ acc) env + | Some sl, cbs :: rest -> + let cbs_len = List.length cbs in + let cbs = List.map turn_direct cbs in + let env = List.fold_left push_seff env cbs in + let ecbs = List.map (fun (kn,cb,u,r) -> + kn, cb, constant_entry_of_side_effect cb u, r) cbs in + translate_seff (Some (sl-cbs_len)) rest (ecbs @ acc) env + in + translate_seff trusted seff [] env +;; let translate_local_assum env t = let j = infer env t in @@ -305,9 +457,9 @@ let translate_local_assum env t = let translate_recipe env kn r = build_constant_declaration kn env (Cooking.cook_constant env r) -let translate_local_def env id centry = +let translate_local_def mb env id centry = let def,typ,proj,poly,univs,inline_code,ctx = - infer_declaration env None (DefinitionEntry centry) in + infer_declaration ~trust:mb env None (DefinitionEntry centry) in let typ = type_of_constant_type env typ in if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin match def with @@ -332,9 +484,9 @@ let translate_mind env kn mie = Indtypes.check_inductive env kn mie let handle_entry_side_effects env ce = { ce with const_entry_body = Future.chain ~greedy:true ~pure:true ce.const_entry_body (fun ((body, ctx), side_eff) -> - let body, ctx' = handle_side_effects env body ctx side_eff in - (body, ctx'), Declareops.no_seff); + let body, ctx',_ = handle_side_effects env body ctx side_eff in + (body, ctx'), []); } let handle_side_effects env body side_eff = - fst (handle_side_effects env body Univ.ContextSet.empty side_eff) + pi1 (handle_side_effects env body Univ.ContextSet.empty side_eff) diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 8d92bcc68f..509160ccc7 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -12,23 +12,42 @@ open Environ open Declarations open Entries -val translate_local_def : env -> Id.t -> definition_entry -> +val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry -> constant_def * types * constant_universes val translate_local_assum : env -> types -> types -val mk_pure_proof : constr -> proof_output +val mk_pure_proof : constr -> side_effects proof_output -val handle_side_effects : env -> constr -> Declareops.side_effects -> constr +val handle_side_effects : env -> constr -> side_effects -> constr (** Returns the term where side effects have been turned into let-ins or beta redexes. *) -val handle_entry_side_effects : env -> definition_entry -> definition_entry +val handle_entry_side_effects : env -> side_effects definition_entry -> side_effects definition_entry (** Same as {!handle_side_effects} but applied to entries. Only modifies the {!Entries.const_entry_body} field. It is meant to get a term out of a not yet type checked proof. *) -val translate_constant : env -> constant -> constant_entry -> constant_body +val uniq_seff : side_effects -> side_effects + +val translate_constant : structure_body -> env -> constant -> side_effects constant_entry -> constant_body + +(* Checks weather the side effects in constant_entry can be trusted. + * Returns the list of effects to be exported. + * Note: It forces the Future.computation. *) +type side_effect_role = + | Subproof + | Schema of inductive * string + +type exported_side_effect = + constant * constant_body * side_effects Entries.constant_entry * side_effect_role + +val validate_side_effects_for_export : + structure_body -> env -> side_effects constant_entry -> + exported_side_effect list * side_effects constant_entry + +val constant_entry_of_side_effect : + constant_body -> seff_env -> side_effects constant_entry val translate_mind : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body @@ -37,8 +56,8 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : env -> constant option -> - constant_entry -> Cooking.result +val infer_declaration : trust:structure_body -> env -> constant option -> + side_effects constant_entry -> Cooking.result val build_constant_declaration : constant -> env -> Cooking.result -> constant_body -- cgit v1.2.3