diff options
Diffstat (limited to 'kernel')
92 files changed, 1837 insertions, 944 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 219ea5b24a..11faef02cb 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Bruno Barras with Benjamin Werner's account to implement @@ -796,7 +798,7 @@ let drop_parameters depth n argstk = s. @assumes [t] is an irreducible term, and not a constructor. [ind] is the inductive of the constructor term [c] - @raises Not_found if the inductive is not a primitive record, or if the + @raise Not_found if the inductive is not a primitive record, or if the constructor is partially applied. *) let eta_expand_ind_stack env ind m s (f, s') = diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index c43fc46239..b9c71d72af 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -214,7 +216,7 @@ val whd_stack : s. @assumes [t] is a rigid term, and not a constructor. [ind] is the inductive of the constructor term [c] - @raises Not_found if the inductive is not a primitive record, or if the + @raise Not_found if the inductive is not a primitive record, or if the constructor is partially applied. *) val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml index 14c11bf107..5b91a9b572 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) type t = diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 8cdffb6702..1e99a69d2f 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) type t = diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 6d91c3ec9e..5ed9b6c675 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Bruno Barras for Benjamin Grégoire as part of the @@ -32,13 +34,12 @@ let cofix_evaluated_tag = 7 let last_variant_tag = 245 type structured_constant = - | Const_sorts of Sorts.t + | Const_sort of Sorts.t | 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.Level.t - | Const_type of Univ.Universe.t type reloc_table = (tag * int) array @@ -46,8 +47,8 @@ type annot_switch = {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} 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_sort s1, Const_sort s2 -> Sorts.equal s1 s2 +| Const_sort _, _ -> false | Const_ind i1, Const_ind i2 -> eq_ind i1 i2 | Const_ind _, _ -> false | Const_proj p1, Const_proj p2 -> Constant.equal p1 p2 @@ -59,13 +60,11 @@ let rec eq_structured_constant c1 c2 = match c1, c2 with | Const_bn _, _ -> false | Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal 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_sort s -> combinesmall 1 (Sorts.hash s) | Const_ind i -> combinesmall 2 (ind_hash i) | Const_proj p -> combinesmall 3 (Constant.hash p) | Const_b0 t -> combinesmall 4 (Int.hash t) @@ -74,7 +73,6 @@ let rec hash_structured_constant c = 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) let eq_annot_switch asw1 asw2 = let eq_ci ci1 ci2 = @@ -184,6 +182,7 @@ type fv_elem = | FVnamed of Id.t | FVrel of int | FVuniv_var of int + | FVevar of Evar.t type fv = fv_elem array @@ -198,12 +197,15 @@ type t = fv_elem let compare e1 e2 = match e1, e2 with | FVnamed id1, FVnamed id2 -> Id.compare id1 id2 -| FVnamed _, _ -> -1 +| FVnamed _, (FVrel _ | FVuniv_var _ | FVevar _) -> -1 | FVrel _, FVnamed _ -> 1 | FVrel r1, FVrel r2 -> Int.compare r1 r2 -| FVrel _, FVuniv_var _ -> -1 +| FVrel _, (FVuniv_var _ | FVevar _) -> -1 | FVuniv_var i1, FVuniv_var i2 -> Int.compare i1 i2 -| FVuniv_var i1, _ -> 1 +| FVuniv_var i1, (FVnamed _ | FVrel _) -> 1 +| FVuniv_var i1, FVevar _ -> -1 +| FVevar _, (FVnamed _ | FVrel _ | FVuniv_var _) -> 1 +| FVevar e1, FVevar e2 -> Evar.compare e1 e2 end @@ -236,20 +238,19 @@ open Util let pp_sort s = let open Sorts in - match family s with - | InSet -> str "Set" - | InProp -> str "Prop" - | InType -> str "Type" + match s with + | Prop Null -> str "Prop" + | Prop Pos -> str "Set" + | Type u -> str "Type@{" ++ Univ.pr_uni u ++ str "}" let rec pp_struct_const = function - | Const_sorts s -> pp_sort s + | Const_sort s -> pp_sort s | Const_ind (mind, i) -> MutInd.print 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 @@ -257,6 +258,7 @@ 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 ")" + | FVevar e -> str "FVevar(" ++ int (Evar.repr e) ++ str ")" let rec pp_instr i = match i with @@ -350,16 +352,3 @@ and pp_bytecodes c = pp_bytecodes l1 ++ pp_bytecodes l2 ++ pp_bytecodes c | i :: c -> pp_instr i ++ fnl () ++ pp_bytecodes c - -(*spiwack: moved this type in this file because I needed it for - retroknowledge which can't depend from cbytegen *) -type block = - | Bconstr of constr - | Bstrconst of structured_constant - | Bmakeblock of int * block array - | Bconstruct_app of int * int * int * block array - (* tag , nparams, arity *) - | Bspecial of (comp_env -> block array -> int -> bytecodes -> bytecodes) * block array - (* spiwack: compilation given by a function *) - (* compilation function (see get_vm_constant_dynamic_info in - retroknowledge.mli for more info) , argument array *) diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index bf2e462e83..03b6bc619d 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* $Id$ *) @@ -26,13 +28,12 @@ val cofix_evaluated_tag : tag val last_variant_tag : tag type structured_constant = - | Const_sorts of Sorts.t + | Const_sort of Sorts.t | 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.Level.t - | Const_type of Univ.Universe.t val pp_struct_const : structured_constant -> Pp.t @@ -138,6 +139,7 @@ type fv_elem = FVnamed of Id.t | FVrel of int | FVuniv_var of int +| FVevar of Evar.t type fv = fv_elem array @@ -171,14 +173,3 @@ type comp_env = { val pp_bytecodes : bytecodes -> Pp.t val pp_fv_elem : fv_elem -> Pp.t - -(*spiwack: moved this here because I needed it for retroknowledge *) -type block = - | Bconstr of constr - | Bstrconst of structured_constant - | Bmakeblock of int * block array - | Bconstruct_app of int * int * int * block array - (** tag , nparams, arity *) - | Bspecial of (comp_env -> block array -> int -> bytecodes -> bytecodes) * block array - (** compilation function (see get_vm_constant_dynamic_info in - retroknowledge.mli for more info) , argument array *) diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 4a34dbcffe..0766f49b39 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Author: Benjamin Grégoire as part of the bytecode-based virtual reduction @@ -14,6 +16,8 @@ open Util open Names open Cbytecodes open Cemitcodes +open Cinstr +open Clambda open Constr open Declarations open Pre_env @@ -96,7 +100,7 @@ module Config = struct let stack_safety_margin = 15 end -type argument = ArgConstr of Constr.t | ArgUniv of Univ.Level.t +type argument = ArgLambda of lambda | ArgUniv of Univ.Level.t let empty_fv = { size= 0; fv_rev = []; fv_fwd = FvMap.empty } let push_fv d e = { @@ -255,6 +259,15 @@ let pos_universe_var i r sz = r.in_env := push_fv db env; Kenvacc(r.offset + pos) +let pos_evar evk r = + let env = !(r.in_env) in + let cid = FVevar evk in + try Kenvacc(r.offset + find_at cid env) + with Not_found -> + let pos = env.size in + r.in_env := push_fv cid env; + Kenvacc (r.offset + pos) + (*i Examination of the continuation *) (* Discard all instructions up to the next label. *) @@ -356,13 +369,6 @@ let cont_cofix arity = Kreturn (arity+2) ] -(*i Global environment *) - -let global_env = ref empty_env - -let set_global_env env = global_env := env - - (* Code of closures *) let fun_code = ref [] @@ -370,31 +376,8 @@ let init_fun_code () = fun_code := [] (* Compilation of constructors and inductive types *) - -(* Limitation due to OCaml's representation of non-constant - constructors: limited to 245 + 1 (0 tag) cases. *) - -exception TooLargeInductive of Id.t - -let max_nb_const = 0x1000000 -let max_nb_block = 0x1000000 + last_variant_tag - 1 - -let str_max_constructors = - Format.sprintf - " which has more than %i constant constructors or more than %i non-constant constructors" max_nb_const max_nb_block - -let check_compilable ib = - - if not (ib.mind_nb_args <= max_nb_block && ib.mind_nb_constant <= max_nb_const) then - raise (TooLargeInductive ib.mind_typename) - (* Inv: arity > 0 *) -let const_bn tag args = - if tag < last_variant_tag then Const_bn(tag, args) - else - Const_bn(last_variant_tag, Array.append [|Const_b0 (tag - last_variant_tag) |] args) - (* If [tag] hits the OCaml limitation for non constant constructors, we switch to another representation for the remaining constructors: @@ -415,126 +398,9 @@ let code_makeblock ~stack_size ~arity ~tag cont = Kpush :: nest_block tag arity cont end -(* [code_construct] compiles an abstracted constructor dropping parameters and - updates [fun_code] *) -(* Inv : nparam + arity > 0 *) -let code_construct tag nparams arity cont = - let f_cont = - add_pop nparams - (if Int.equal arity 0 then - [Kconst (Const_b0 tag); Kreturn 0] - else if tag < last_variant_tag then - [Kacc 0; Kpop 1; Kmakeblock(arity, tag); Kreturn 0] - else - nest_block tag arity [Kreturn 0]) - in - let lbl = Label.create() in - (* No need to grow the stack here, as the function does not push stuff. *) - fun_code := [Ksequence (add_grab (nparams+arity) lbl f_cont,!fun_code)]; - Kclosure(lbl,0) :: cont - -let get_strcst = function - | Bstrconst sc -> sc - | _ -> raise Not_found - -let rec str_const c = - match kind c with - | Sort s -> Bstrconst (Const_sorts s) - | Cast(c,_,_) -> str_const c - | App(f,args) -> - begin - match kind f with - | Construct(((kn,j),i),u) -> - begin - let oib = lookup_mind kn !global_env in - let oip = oib.mind_packets.(j) in - let () = check_compilable oip in - let tag,arity = oip.mind_reloc_tbl.(i-1) in - let nparams = oib.mind_nparams in - if Int.equal (nparams + arity) (Array.length args) then - (* spiwack: *) - (* 1/ tries to compile the constructor in an optimal way, - it is supposed to work only if the arguments are - all fully constructed, fails with Cbytecodes.NotClosed. - it can also raise Not_found when there is no special - treatment for this constructor - for instance: tries to to compile an integer of the - form I31 D1 D2 ... D31 to [D1D2...D31] as - a processor number (a caml number actually) *) - try - try - Bstrconst (Retroknowledge.get_vm_constant_static_info - (!global_env).retroknowledge - f args) - with NotClosed -> - (* 2/ if the arguments are not all closed (this is - expectingly (and it is currently the case) the only - reason why this exception is raised) tries to - give a clever, run-time behavior to the constructor. - Raises Not_found if there is no special treatment - for this integer. - this is done in a lazy fashion, using the constructor - Bspecial because it needs to know the continuation - and such, which can't be done at this time. - for instance, for int31: if one of the digit is - not closed, it's not impossible that the number - gets fully instanciated at run-time, thus to ensure - uniqueness of the representation in the vm - it is necessary to try and build a caml integer - during the execution *) - let rargs = Array.sub args nparams arity in - let b_args = Array.map str_const rargs in - Bspecial ((Retroknowledge.get_vm_constant_dynamic_info - (!global_env).retroknowledge - f), - b_args) - with Not_found -> - (* 3/ if no special behavior is available, then the compiler - falls back to the normal behavior *) - if Int.equal arity 0 then Bstrconst(Const_b0 tag) - else - let rargs = Array.sub args nparams arity in - let b_args = Array.map str_const rargs in - try - let sc_args = Array.map get_strcst b_args in - Bstrconst(const_bn tag sc_args) - with Not_found -> - Bmakeblock(tag,b_args) - else - let b_args = Array.map str_const args in - (* spiwack: tries first to apply the run-time compilation - behavior of the constructor, as in 2/ above *) - try - Bspecial ((Retroknowledge.get_vm_constant_dynamic_info - (!global_env).retroknowledge - f), - b_args) - with Not_found -> - Bconstruct_app(tag, nparams, arity, b_args) - end - | _ -> Bconstr c - end - | Ind (ind,u) when Univ.Instance.is_empty u -> - Bstrconst (Const_ind ind) - | Construct (((kn,j),i),_) -> - begin - (* spiwack: tries first to apply the run-time compilation - behavior of the constructor, as in 2/ above *) - try - Bspecial ((Retroknowledge.get_vm_constant_dynamic_info - (!global_env).retroknowledge - c), - [| |]) - with Not_found -> - let oib = lookup_mind kn !global_env in - let oip = oib.mind_packets.(j) in - let () = check_compilable oip in - let num,arity = oip.mind_reloc_tbl.(i-1) in - let nparams = oib.mind_nparams in - if Int.equal (nparams + arity) 0 then Bstrconst(Const_b0 num) - else Bconstruct_app(num,nparams,arity,[||]) - end - | _ -> Bconstr c +let compile_structured_constant reloc sc sz cont = + set_max_stack_size sz; + Kconst sc :: cont (* compiling application *) let comp_args comp_expr reloc args sz cont = @@ -545,9 +411,10 @@ let comp_args comp_expr reloc args sz cont = done; !c -(* Precondition: args not empty *) let comp_app comp_fun comp_arg reloc f args sz cont = let nargs = Array.length args in + if Int.equal nargs 0 then comp_fun reloc f sz cont + else match is_tailcall cont with | Some k -> comp_args comp_arg reloc args sz @@ -571,6 +438,7 @@ let compile_fv_elem reloc fv sz cont = | 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 + | FVevar evk -> pos_evar evk reloc :: cont let rec compile_fv reloc l sz cont = match l with @@ -593,102 +461,111 @@ let rec get_alias env kn = | BCalias kn' -> get_alias env kn' | _ -> 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 + cont + else + Kareconst (n, else_lbl)::cont + (* sz is the size of the local stack *) -let rec compile_constr reloc c sz cont = +let rec compile_lam env reloc lam sz cont = set_max_stack_size sz; - match kind c with - | Meta _ -> invalid_arg "Cbytegen.compile_constr : Meta" - | Evar _ -> invalid_arg "Cbytegen.compile_constr : Evar" - | Proj (p,c) -> - let kn = Projection.constant p in - let cb = lookup_constant kn !global_env in - let pb = Option.get cb.const_proj in - let n = pb.proj_arg in - compile_constr reloc c sz (Kproj (n,kn) :: cont) - - | Cast(c,_,_) -> 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 (ind,u) -> - let bcst = Bstrconst (Const_ind ind) in + match lam with + | Lrel(_, i) -> pos_rel i reloc sz :: cont + + | Lval v -> compile_structured_constant reloc v sz cont + + | Lproj (n,kn,arg) -> + compile_lam env reloc arg sz (Kproj (n,kn) :: cont) + + | Lvar id -> pos_named id reloc :: cont + + | Levar (evk, args) -> + if Array.is_empty args then + compile_fv_elem reloc (FVevar evk) sz cont + else + comp_app compile_fv_elem (compile_lam env) reloc (FVevar evk) args sz cont + + | Lconst (kn,u) -> compile_constant env reloc kn u [||] sz cont + + | Lind (ind,u) -> if Univ.Instance.is_empty u then - compile_str_cst reloc bcst sz cont - else - comp_app compile_str_cst compile_universe reloc - bcst - (Univ.Instance.to_array u) - sz - cont - | Sort (Sorts.Prop _) | Construct _ -> - compile_str_cst reloc (str_const c) sz cont - | Sort (Sorts.Type u) -> - (* 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 + compile_structured_constant reloc (Const_ind ind) sz cont + else comp_app compile_structured_constant compile_universe reloc + (Const_ind ind) (Univ.Instance.to_array u) sz cont + + | Lsort (Sorts.Prop _ as s) -> + compile_structured_constant reloc (Const_sort s) sz cont + | Lsort (Sorts.Type u) -> + (* 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 u,s = Universe.compact u in (* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *) + let compile_get_univ reloc idx sz cont = + set_max_stack_size sz; + compile_fv_elem reloc (FVuniv_var idx) sz cont + in if List.is_empty s then - compile_str_cst reloc (Bstrconst (Const_sorts (Sorts.Type u))) sz cont + compile_structured_constant reloc (Const_sort (Sorts.Type u)) sz cont else - let compile_get_univ reloc idx sz cont = - set_max_stack_size sz; - 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 s) sz cont + comp_app compile_structured_constant compile_get_univ reloc + (Const_sort (Sorts.Type u)) (Array.of_list s) sz cont end - | LetIn(_,xb,_,body) -> - compile_constr reloc xb sz - (Kpush :: - (compile_constr (push_local sz reloc) body (sz+1) (add_pop 1 cont))) - | Prod(id,dom,codom) -> - let cont1 = - Kpush :: compile_constr reloc dom (sz+1) (Kmakeprod :: cont) in - compile_constr reloc (mkLambda(id,dom,codom)) sz cont1 - | Lambda _ -> - let params, body = Term.decompose_lam c in - let arity = List.length params in - let r_fun = comp_env_fun arity in - let lbl_fun = Label.create() in - let cont_fun = - ensure_stack_capacity (compile_constr r_fun body arity) [Kreturn arity] - in - fun_code := [Ksequence(add_grab arity lbl_fun cont_fun,!fun_code)]; - let fv = fv r_fun in - compile_fv reloc fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont) - - | App(f,args) -> - begin - match kind f with - | Construct _ -> compile_str_cst reloc (str_const c) sz cont - | Const (kn,u) -> compile_const reloc kn u args sz cont - | _ -> comp_app compile_constr compile_constr reloc f args sz cont - end - | Fix ((rec_args,init),(_,type_bodies,rec_bodies)) -> - let ndef = Array.length type_bodies in + + | Llet (id,def,body) -> + compile_lam env reloc def sz + (Kpush :: + compile_lam env (push_local sz reloc) body (sz+1) (add_pop 1 cont)) + + | Lprod (dom,codom) -> + let cont1 = + Kpush :: compile_lam env reloc dom (sz+1) (Kmakeprod :: cont) in + compile_lam env reloc codom sz cont1 + + | Llam (ids,body) -> + let arity = Array.length ids in + let r_fun = comp_env_fun arity in + let lbl_fun = Label.create() in + let cont_fun = + ensure_stack_capacity (compile_lam env r_fun body arity) [Kreturn arity] + in + fun_code := [Ksequence(add_grab arity lbl_fun cont_fun,!fun_code)]; + let fv = fv r_fun in + compile_fv reloc fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont) + + | Lapp (f, args) -> + begin match f with + | Lconst (kn,u) -> compile_constant env reloc kn u args sz cont + | _ -> comp_app (compile_lam env) (compile_lam env) reloc f args sz cont + end + + | Lfix ((rec_args, init), (decl, types, bodies)) -> + let ndef = Array.length types in let rfv = ref empty_fv in let lbl_types = Array.make ndef Label.no in let lbl_bodies = Array.make ndef Label.no in - (* Compilation des types *) + (* Compiling types *) let env_type = comp_env_fix_type rfv in for i = 0 to ndef - 1 do let fcode = - ensure_stack_capacity (compile_constr env_type type_bodies.(i) 0) [Kstop] + ensure_stack_capacity (compile_lam env env_type types.(i) 0) [Kstop] in - let lbl,fcode = label_code fcode in - lbl_types.(i) <- lbl; + let lbl,fcode = label_code fcode in + lbl_types.(i) <- lbl; fun_code := [Ksequence(fcode,!fun_code)] done; (* Compiling bodies *) for i = 0 to ndef - 1 do - let params,body = Term.decompose_lam rec_bodies.(i) in - let arity = List.length params in + let params,body = decompose_Llam bodies.(i) in + let arity = Array.length params in let env_body = comp_env_fix ndef i arity rfv in - let cont1 = - ensure_stack_capacity (compile_constr env_body body arity) [Kreturn arity] + let cont1 = + ensure_stack_capacity (compile_lam env env_body body arity) [Kreturn arity] in let lbl = Label.create () in lbl_bodies.(i) <- lbl; @@ -699,8 +576,9 @@ let rec compile_constr reloc c sz cont = compile_fv reloc fv.fv_rev sz (Kclosurerec(fv.size,init,lbl_types,lbl_bodies) :: cont) - | CoFix(init,(_,type_bodies,rec_bodies)) -> - let ndef = Array.length type_bodies in + + | Lcofix(init, (decl,types,bodies)) -> + let ndef = Array.length types in let lbl_types = Array.make ndef Label.no in let lbl_bodies = Array.make ndef Label.no in (* Compiling types *) @@ -708,22 +586,22 @@ let rec compile_constr reloc c sz cont = let env_type = comp_env_cofix_type ndef rfv in for i = 0 to ndef - 1 do let fcode = - ensure_stack_capacity (compile_constr env_type type_bodies.(i) 0) [Kstop] + ensure_stack_capacity (compile_lam env env_type types.(i) 0) [Kstop] in - let lbl,fcode = label_code fcode in - lbl_types.(i) <- lbl; + let lbl,fcode = label_code fcode in + lbl_types.(i) <- lbl; fun_code := [Ksequence(fcode,!fun_code)] done; (* Compiling bodies *) for i = 0 to ndef - 1 do - let params,body = Term.decompose_lam rec_bodies.(i) in - let arity = List.length params in + let params,body = decompose_Llam bodies.(i) in + let arity = Array.length params in let env_body = comp_env_cofix ndef arity rfv in let lbl = Label.create () in let comp arity = (* 4 stack slots are needed to update the cofix when forced *) set_max_stack_size (arity + 4); - compile_constr env_body body (arity+1) (cont_cofix arity) + compile_lam env env_body body (arity+1) (cont_cofix arity) in let cont = ensure_stack_capacity comp arity in lbl_bodies.(i) <- lbl; @@ -734,33 +612,34 @@ let rec compile_constr reloc c sz cont = compile_fv reloc fv.fv_rev sz (Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont) - | Case(ci,t,a,branchs) -> + + | Lcase(ci,rtbl,t,a,branches) -> let ind = ci.ci_ind in - let mib = lookup_mind (fst ind) !global_env in + let mib = lookup_mind (fst ind) env in let oib = mib.mind_packets.(snd ind) in - let () = check_compilable oib in - let tbl = oib.mind_reloc_tbl in let lbl_consts = Array.make oib.mind_nb_constant Label.no in let nallblock = oib.mind_nb_args + 1 in (* +1 : accumulate *) + let nconst = Array.length branches.constant_branches in let nblock = min nallblock (last_variant_tag + 1) in let lbl_blocks = Array.make nblock Label.no in let neblock = max 0 (nallblock - last_variant_tag) in let lbl_eblocks = Array.make neblock Label.no in - let branch1,cont = make_branch cont in - (* Compiling return type *) + let branch1, cont = make_branch cont in + (* Compilation of the return type *) let fcode = - ensure_stack_capacity (compile_constr reloc t sz) [Kpop sz; Kstop] + ensure_stack_capacity (compile_lam env reloc t sz) [Kpop sz; Kstop] in let lbl_typ,fcode = label_code fcode in fun_code := [Ksequence(fcode,!fun_code)]; - (* Compiling branches *) + (* Compilation of the branches *) 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 - | _ -> sz+3, Kjump, false + match branch1 with + | Kreturn k -> + assert (Int.equal k sz) ; + sz, branch1, true + | Kbranch _ -> sz+3, Kjump, false + | _ -> assert false in let c = ref cont in @@ -771,29 +650,26 @@ let rec compile_constr reloc c sz cont = Kpush :: Kfield 0 :: Kswitch(lbl_eblocks, [||]) :: !c) in lbl_blocks.(last_variant_tag) <- lbl_b; c := code_b - end; - - (* Compiling regular constructor branches *) - for i = 0 to Array.length tbl - 1 do - let tag, arity = tbl.(i) in - if Int.equal arity 0 then - let lbl_b,code_b = - label_code(compile_constr reloc branchs.(i) sz_b (branch :: !c)) in - lbl_consts.(tag) <- lbl_b; - c := code_b - else - let args, body = Term.decompose_lam branchs.(i) in - let nargs = List.length args in - - let code_b = - if Int.equal nargs arity then - compile_constr (push_param arity sz_b reloc) - body (sz_b+arity) (add_pop arity (branch :: !c)) - else - let sz_appterm = if is_tailcall then sz_b + arity else arity in - compile_constr reloc branchs.(i) (sz_b+arity) - (Kappterm(arity,sz_appterm) :: !c) in - let code_b = + end; + + (* Compilation of constant branches *) + for i = nconst - 1 downto 0 do + let aux = + compile_lam env reloc branches.constant_branches.(i) sz_b (branch::!c) + in + let lbl_b,code_b = label_code aux in + lbl_consts.(i) <- lbl_b; + c := code_b + done; + (* -1 for accu branch *) + for i = nallblock - 2 downto 0 do + let tag = i + 1 in + let (ids, body) = branches.nonconstant_branches.(i) in + let arity = Array.length ids in + let code_b = + compile_lam env (push_param arity sz_b reloc) + body (sz_b+arity) (add_pop arity (branch::!c)) in + let code_b = if tag < last_variant_tag then begin set_max_stack_size (sz_b + arity); Kpushfields arity :: code_b @@ -802,15 +678,15 @@ let rec compile_constr reloc c sz cont = set_max_stack_size (sz_b + arity + 1); Kacc 0::Kpop 1::Kpushfields(arity+1)::Kpop 1::code_b end - in - let lbl_b,code_b = label_code code_b in - if tag < last_variant_tag then lbl_blocks.(tag) <- lbl_b + in + let lbl_b, code_b = label_code code_b in + if tag < last_variant_tag then lbl_blocks.(tag) <- lbl_b else lbl_eblocks.(tag - last_variant_tag) <- lbl_b; - c := code_b + c := code_b done; let annot = - {ci = ci; rtbl = tbl; tailcall = is_tailcall; + {ci = ci; rtbl = rtbl; tailcall = is_tailcall; max_stack_size = !max_stack_size - sz} in @@ -829,38 +705,50 @@ let rec compile_constr reloc c sz cont = | Kbranch lbl -> Kpush_retaddr lbl :: !c | _ -> !c in - compile_constr reloc a sz - (try - let entry = mkInd ind in - Retroknowledge.get_vm_before_match_info (!global_env).retroknowledge - entry code_sw - with Not_found -> - code_sw) - -and compile_str_cst reloc sc sz cont = - set_max_stack_size sz; - match sc with - | Bconstr c -> compile_constr reloc c sz cont - | Bstrconst sc -> Kconst sc :: cont - | Bmakeblock(tag,args) -> - let arity = Array.length args in - let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in - comp_args compile_str_cst reloc args sz cont - | Bconstruct_app(tag,nparams,arity,args) -> - if Int.equal (Array.length args) 0 then - code_construct tag nparams arity cont - else - comp_app - (fun _ _ _ cont -> code_construct tag nparams arity cont) - compile_str_cst reloc () args sz cont - | Bspecial (comp_fx, args) -> comp_fx reloc args sz cont + compile_lam env reloc a sz code_sw + + | Lmakeblock (tag,args) -> + let arity = Array.length args in + let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in + comp_args (compile_lam env) reloc args sz cont + + | Lprim (kn, ar, op, args) -> + op_compilation env ar op kn reloc args sz cont + + | Luint v -> + (match v with + | UintVal i -> compile_structured_constant reloc (Const_b0 (Uint31.to_int i)) sz cont + | UintDigits ds -> + let nargs = Array.length ds in + if Int.equal nargs 31 then + let (escape,labeled_cont) = make_branch cont in + let else_lbl = Label.create() in + comp_args (compile_lam env) reloc ds sz + ( Kisconst else_lbl::Kareconst(30,else_lbl)::Kcompint31::escape::Klabel else_lbl::Kmakeblock(31, 1)::labeled_cont) + else + let code_construct cont = (* spiwack: variant of the global code_construct + which handles dynamic compilation of + integers *) + let f_cont = + let else_lbl = Label.create () in + [Kacc 0; Kpop 1; Kisconst else_lbl; Kareconst(30,else_lbl); + Kcompint31; Kreturn 0; Klabel else_lbl; Kmakeblock(31, 1); Kreturn 0] + in + let lbl = Label.create() in + fun_code := [Ksequence (add_grab 31 lbl f_cont,!fun_code)]; + Kclosure(lbl,0) :: cont + in + comp_app (fun _ _ _ cont -> code_construct cont) + (compile_lam env) reloc () ds sz cont + | UintDecomp t -> + let escape_lbl, labeled_cont = label_code cont in + compile_lam env reloc t sz ((Kisconst escape_lbl)::Kdecompint31::labeled_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 = set_max_stack_size sz; - let kn = get_alias !global_env kn in if Univ.Instance.is_empty u then Kgetglobal kn :: cont else @@ -870,41 +758,67 @@ and compile_get_global reloc (kn,u) sz cont = and compile_universe reloc uni sz cont = set_max_stack_size sz; match Univ.Level.var_index uni with - | None -> Kconst (Const_univ_level uni) :: cont + | None -> compile_structured_constant reloc (Const_univ_level uni) sz cont | Some idx -> pos_universe_var idx reloc sz :: cont -and compile_const reloc kn u args sz cont = +and compile_constant env reloc kn u args sz cont = set_max_stack_size sz; + if Univ.Instance.is_empty u then + (* normal compilation *) + comp_app (fun _ _ sz cont -> + compile_get_global reloc (kn,u) sz cont) + (compile_lam env) reloc () args sz cont + else + let compile_arg reloc constr_or_uni sz cont = + match constr_or_uni with + | ArgLambda t -> compile_lam env reloc t 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 ArgLambda args.(i-lu)) + in + comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont) + compile_arg reloc () all sz cont + +(*template for n-ary operation, invariant: n>=1, + the operations does the following : + 1/ checks if all the arguments are constants (i.e. non-block values) + 2/ if they are, uses the "op" instruction to execute + 3/ if at least one is not, branches to the normal behavior: + Kgetglobal (get_alias !global_env kn) *) +and op_compilation env n op = + 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]*) + 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)]; + Kclosure(lbl, 0)::cont + in + fun kn reloc 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 - falls back on its normal behavior *) - try - Retroknowledge.get_vm_compiling_info (!global_env).retroknowledge - (mkConstU (kn,u)) reloc args sz cont - with Not_found -> - if Int.equal nargs 0 then - compile_get_global reloc (kn,u) sz cont - else - 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_arg reloc constr_or_uni sz cont = - match constr_or_uni with - | 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_arg reloc () all sz cont + if Int.equal nargs n then (*if it is a fully applied addition*) + let (escape, labeled_cont) = make_branch cont in + let else_lbl = Label.create () in + assert (n < 4); + comp_args (compile_lam env) reloc args sz + (Kisconst else_lbl::(make_areconst (n-1) else_lbl + (*Kaddint31::escape::Klabel else_lbl::Kpush::*) + (op::escape::Klabel else_lbl::Kpush:: + (* works as comp_app with nargs < 4 and non-tailcall cont*) + compile_get_global reloc kn (sz+n) (Kapply n::labeled_cont)))) + else + comp_app (fun reloc _ sz cont -> code_construct reloc kn sz cont) + (compile_lam env) reloc () args sz cont + let is_univ_copy max u = let u = Univ.Instance.to_array u in @@ -927,33 +841,29 @@ let dump_bytecodes init code fvs = prlist_with_sep (fun () -> str "; ") pp_fv_elem fvs ++ fnl ()) -let compile fail_on_error ?universes:(universes=0) env c = - set_global_env env; +let compile ~fail_on_error ?universes:(universes=0) env c = init_fun_code (); Label.reset_label_counter (); let cont = [Kstop] in try let reloc, init_code = if Int.equal universes 0 then + let lam = lambda_of_constr ~optimize:true env c in let reloc = empty_comp_env () in - reloc, ensure_stack_capacity (compile_constr reloc c 0) cont + reloc, ensure_stack_capacity (compile_lam env reloc lam 0) cont else (* We are going to generate a lambda, but merge the universe closure * with the function closure if it exists. *) + let lam = lambda_of_constr ~optimize:true env c in + let params, body = decompose_Llam lam in + let arity = Array.length params in let reloc = empty_comp_env () in - let arity , body = - match kind c with - | Lambda _ -> - let params, body = Term.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 = - ensure_stack_capacity (compile_constr r_fun body full_arity) + ensure_stack_capacity (compile_lam env r_fun body full_arity) [Kreturn full_arity] in fun_code := [Ksequence(add_grab full_arity lbl_fun cont_fun,!fun_code)]; @@ -968,15 +878,12 @@ let compile fail_on_error ?universes:(universes=0) env c = (if !Flags.dump_bytecode then Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ; Some (init_code,!fun_code, Array.of_list fv) - with TooLargeInductive tname -> + with TooLargeInductive msg -> let fn = if fail_on_error then CErrors.user_err ?loc:None ~hdr:"compile" else - (fun x -> Feedback.msg_warning x) in - (Pp.(fn - (str "Cannot compile code for virtual machine as it uses inductive " ++ - Id.print tname ++ str str_max_constructors)); - None) + (fun x -> Feedback.msg_warning x) in + fn msg; None -let compile_constant_body fail_on_error env univs = 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 @@ -991,65 +898,13 @@ let compile_constant_body fail_on_error env univs = function let con= Constant.make1 (Constant.canonical kn') in Some (BCalias (get_alias env con)) | _ -> - let res = compile fail_on_error ~universes:instance_size 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 = BCalias (Constant.make1 (Constant.canonical 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 - cont - else - Kareconst (n, else_lbl)::cont - - -(* try to compile int31 as a const_b0. Succeed if all the arguments are closed - fails otherwise by raising NotClosed*) -let compile_structured_int31 fc args = - if not fc then raise Not_found else - Const_b0 - (Array.fold_left - (fun temp_i -> fun t -> match kind t with - | Construct ((_,d),_) -> 2*temp_i+d-1 - | _ -> raise NotClosed) - 0 args - ) - -(* this function is used for the compilation of the constructor of - the int31, it is used when it appears not fully applied, or - applied to at least one non-closed digit *) -let dynamic_int31_compilation fc reloc args sz cont = - if not fc then raise Not_found else - let nargs = Array.length args in - if Int.equal nargs 31 then - let (escape,labeled_cont) = make_branch cont in - let else_lbl = Label.create() in - comp_args compile_str_cst reloc args sz - ( Kisconst else_lbl::Kareconst(30,else_lbl)::Kcompint31::escape::Klabel else_lbl::Kmakeblock(31, 1)::labeled_cont) - else - let code_construct cont = (* spiwack: variant of the global code_construct - which handles dynamic compilation of - integers *) - let f_cont = - let else_lbl = Label.create () in - [Kacc 0; Kpop 1; Kisconst else_lbl; Kareconst(30,else_lbl); - Kcompint31; Kreturn 0; Klabel else_lbl; Kmakeblock(31, 1); Kreturn 0] - in - let lbl = Label.create() in - fun_code := [Ksequence (add_grab 31 lbl f_cont,!fun_code)]; - Kclosure(lbl,0) :: cont - in - if Int.equal nargs 0 then - code_construct cont - else - comp_app (fun _ _ _ cont -> code_construct cont) - compile_str_cst reloc () args sz cont - (*(* template compilation for 2ary operation, it probably possible to make a generic such function with arity abstracted *) let op2_compilation op = @@ -1087,47 +942,3 @@ let op2_compilation op = comp_app (fun _ _ _ cont -> code_construct normal cont) compile_constr reloc () args sz cont *) -(*template for n-ary operation, invariant: n>=1, - the operations does the following : - 1/ checks if all the arguments are constants (i.e. non-block values) - 2/ if they are, uses the "op" instruction to execute - 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 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]*) - 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)]; - Kclosure(lbl, 0)::cont - in - fun kn fc reloc args sz cont -> - if not fc then raise Not_found else - let nargs = Array.length args in - if Int.equal nargs n then (*if it is a fully applied addition*) - let (escape, labeled_cont) = make_branch cont in - let else_lbl = Label.create () in - comp_args compile_constr reloc args sz - (Kisconst else_lbl::(make_areconst (n-1) else_lbl - (*Kaddint31::escape::Klabel else_lbl::Kpush::*) - (op::escape::Klabel else_lbl::Kpush:: - (* works as comp_app with nargs = n and non-tailcall cont*) - compile_get_global reloc kn sz (Kapply n::labeled_cont)))) - else if Int.equal nargs 0 then - code_construct reloc kn sz cont - else - 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 = - if not fc then - raise Not_found - else - let escape_lbl, labeled_cont = label_code cont in - (Kisconst escape_lbl)::Kdecompint31::labeled_cont diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index c117d3fb57..abab58b60b 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Cbytecodes @@ -13,38 +15,13 @@ 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 *) +val compile : fail_on_error:bool -> ?universes:int -> env -> constr -> (bytecodes * bytecodes * fv) option (** init, fun, fv *) -val compile_constant_body : bool -> +val compile_constant_body : fail_on_error:bool -> env -> constant_universes -> constant_def -> body_code option (** Shortcut of the previous function used during module strengthening *) val compile_alias : Names.Constant.t -> body_code - -(** spiwack: this function contains the information needed to perform - the static compilation of int31 (trying and obtaining - a 31-bit integer in processor representation at compile time) *) -val compile_structured_int31 : bool -> constr array -> - structured_constant - -(** this function contains the information needed to perform - the dynamic compilation of int31 (trying and obtaining a - 31-bit integer in processor representation at runtime when - it failed at compile time *) -val dynamic_int31_compilation : bool -> comp_env -> - block array -> - int -> bytecodes -> bytecodes - -(*spiwack: template for the compilation n-ary operation, invariant: n>=1. - works as follow: checks if all the arguments are non-pointers - if they are applies the operation (second argument) if not - all of them are, returns to a coq definition (third argument) *) -val op_compilation : int -> instruction -> pconstant -> bool -> comp_env -> - constr array -> int -> bytecodes-> bytecodes - -(*spiwack: compiling function to insert dynamic decompilation before - matching integers (in case they are in processor representation) *) -val int31_escape_before_match : bool -> bytecodes -> bytecodes diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 856b0b465c..14f4f27c09 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Author: Benjamin Grégoire as part of the bytecode-based virtual reduction @@ -350,7 +352,7 @@ type to_patch = emitcodes * patches * fv (* Substitution *) let rec subst_strcst s sc = match sc with - | Const_sorts _ | Const_b0 _ | Const_univ_level _ | Const_type _ -> sc + | Const_sort _ | Const_b0 _ | Const_univ_level _ -> 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/cinstr.mli b/kernel/cinstr.mli new file mode 100644 index 0000000000..4a3c03d85e --- /dev/null +++ b/kernel/cinstr.mli @@ -0,0 +1,46 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +open Names +open Constr +open Cbytecodes + +(** This file defines the lambda code for the bytecode compiler. It has been +extracted from Clambda.ml because of the retroknowledge architecture. *) + +type uint = + | UintVal of Uint31.t + | UintDigits of lambda array + | UintDecomp of lambda + +and lambda = + | Lrel of Name.t * int + | Lvar of Id.t + | Levar of Evar.t * lambda array + | Lprod of lambda * lambda + | Llam of Name.t array * lambda + | Llet of Name.t * lambda * lambda + | Lapp of lambda * lambda array + | Lconst of pconstant + | Lprim of pconstant * int (* arity *) * instruction * lambda array + | Lcase of case_info * reloc_table * lambda * lambda * lam_branches + | Lfix of (int array * int) * fix_decl + | Lcofix of int * fix_decl + | Lmakeblock of int * lambda array + | Lval of structured_constant + | Lsort of Sorts.t + | Lind of pinductive + | Lproj of int * Constant.t * lambda + | Luint of uint + +and lam_branches = + { constant_branches : lambda array; + nonconstant_branches : (Name.t array * lambda) array } + +and fix_decl = Name.t array * lambda array * lambda array diff --git a/kernel/clambda.ml b/kernel/clambda.ml new file mode 100644 index 0000000000..7b637c20e6 --- /dev/null +++ b/kernel/clambda.ml @@ -0,0 +1,863 @@ +open Util +open Names +open Esubst +open Term +open Constr +open Declarations +open Cbytecodes +open Cinstr +open Pre_env +open Pp + +let pr_con sp = str(Names.Label.to_string (Constant.label sp)) + +(** Printing **) + +let pp_names ids = + prlist_with_sep (fun _ -> brk(1,1)) Name.print (Array.to_list ids) + +let pp_rel name n = + Name.print name ++ str "##" ++ int n + +let pp_sort s = + match Sorts.family s with + | InSet -> str "Set" + | InProp -> str "Prop" + | InType -> str "Type" + +let rec pp_lam lam = + match lam with + | Lrel (id,n) -> pp_rel id n + | Lvar id -> Id.print id + | Levar (evk, args) -> + hov 1 (str "evar(" ++ Evar.print evk ++ str "," ++ spc () ++ + prlist_with_sep spc pp_lam (Array.to_list args) ++ str ")") + | Lprod(dom,codom) -> hov 1 + (str "forall(" ++ + pp_lam dom ++ + str "," ++ spc() ++ + pp_lam codom ++ + str ")") + | Llam(ids,body) -> hov 1 + (str "(fun " ++ + pp_names ids ++ + str " =>" ++ + spc() ++ + pp_lam body ++ + str ")") + | Llet(id,def,body) -> hov 0 + (str "let " ++ + Name.print id ++ + str ":=" ++ + pp_lam def ++ + str " in" ++ + spc() ++ + pp_lam body) + | Lapp(f, args) -> hov 1 + (str "(" ++ pp_lam f ++ spc() ++ + prlist_with_sep spc pp_lam (Array.to_list args) ++ + str")") + | Lconst (kn,_) -> pr_con kn + | Lcase(_ci, _rtbl, t, a, branches) -> + let ic = ref (-1) in + let ib = ref 0 in + v 0 (str"<" ++ pp_lam t ++ str">" ++ cut() ++ + str "Case" ++ spc () ++ pp_lam a ++ spc() ++ str "of" ++ cut() ++ + v 0 + ((prlist_with_sep (fun _ -> str "") + (fun c -> + cut () ++ str "| " ++ + int (incr ic; !ic) ++ str " => " ++ pp_lam c) + (Array.to_list branches.constant_branches)) ++ + (prlist_with_sep (fun _ -> str "") + (fun (ids,c) -> + cut () ++ str "| " ++ + int (incr ib; !ib) ++ str " " ++ + pp_names ids ++ str " => " ++ pp_lam c) + (Array.to_list branches.nonconstant_branches))) + ++ cut() ++ str "end") + | Lfix((t,i),(lna,tl,bl)) -> + let fixl = Array.mapi (fun i id -> (id,t.(i),tl.(i),bl.(i))) lna in + hov 1 + (str"fix " ++ int i ++ spc() ++ str"{" ++ + v 0 + (prlist_with_sep spc + (fun (na,i,ty,bd) -> + Name.print na ++ str"/" ++ int i ++ str":" ++ + pp_lam ty ++ cut() ++ str":=" ++ + pp_lam bd) (Array.to_list fixl)) ++ + str"}") + + | Lcofix (i,(lna,tl,bl)) -> + let fixl = Array.mapi (fun i na -> (na,tl.(i),bl.(i))) lna in + hov 1 + (str"cofix " ++ int i ++ spc() ++ str"{" ++ + v 0 + (prlist_with_sep spc + (fun (na,ty,bd) -> + Name.print na ++ str":" ++ pp_lam ty ++ + cut() ++ str":=" ++ pp_lam bd) (Array.to_list fixl)) ++ + str"}") + | Lmakeblock(tag, args) -> + hov 1 + (str "(makeblock " ++ int tag ++ spc() ++ + prlist_with_sep spc pp_lam (Array.to_list args) ++ + str")") + | Lval _ -> str "values" + | Lsort s -> pp_sort s + | Lind ((mind,i), _) -> MutInd.print mind ++ str"#" ++ int i + | Lprim((kn,_u),ar,op,args) -> + hov 1 + (str "(PRIM " ++ pr_con kn ++ spc() ++ + prlist_with_sep spc pp_lam (Array.to_list args) ++ + str")") + | Lproj(i,kn,arg) -> + hov 1 + (str "(proj#" ++ int i ++ spc() ++ pr_con kn ++ str "(" ++ pp_lam arg + ++ str ")") + | Luint _ -> + str "(uint)" + +(*s Constructors *) + +let mkLapp f args = + if Array.length args = 0 then f + else + match f with + | Lapp(f', args') -> Lapp (f', Array.append args' args) + | _ -> Lapp(f, args) + +let mkLlam ids body = + if Array.length ids = 0 then body + else + match body with + | Llam(ids', body) -> Llam(Array.append ids ids', body) + | _ -> Llam(ids, body) + +let decompose_Llam lam = + match lam with + | Llam(ids,body) -> ids, body + | _ -> [||], lam + +(*s Operators on substitution *) +let subst_id = subs_id 0 +let lift = subs_lift +let liftn = subs_liftn +let cons v subst = subs_cons([|v|], subst) +let shift subst = subs_shft (1, subst) + +(* A generic map function *) + +let rec map_lam_with_binders g f n lam = + match lam with + | Lrel _ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ -> lam + | Levar (evk, args) -> + let args' = Array.smartmap (f n) args in + if args == args' then lam else Levar (evk, args') + | Lprod(dom,codom) -> + let dom' = f n dom in + let codom' = f n codom in + if dom == dom' && codom == codom' then lam else Lprod(dom',codom') + | Llam(ids,body) -> + let body' = f (g (Array.length ids) n) body in + if body == body' then lam else mkLlam ids body' + | Llet(id,def,body) -> + let def' = f n def in + let body' = f (g 1 n) body in + if body == body' && def == def' then lam else Llet(id,def',body') + | Lapp(fct,args) -> + let fct' = f n fct in + let args' = Array.smartmap (f n) args in + if fct == fct' && args == args' then lam else mkLapp fct' args' + | Lcase(ci,rtbl,t,a,branches) -> + let const = branches.constant_branches in + let nonconst = branches.nonconstant_branches in + let t' = f n t in + let a' = f n a in + let const' = Array.smartmap (f n) const in + let on_b b = + let (ids,body) = b in + let body' = f (g (Array.length ids) n) body in + if body == body' then b else (ids,body') in + let nonconst' = Array.smartmap on_b nonconst in + let branches' = + if const == const' && nonconst == nonconst' then + branches + else + { constant_branches = const'; + nonconstant_branches = nonconst' } + in + if t == t' && a == a' && branches == branches' then lam else + Lcase(ci,rtbl,t',a',branches') + | Lfix(init,(ids,ltypes,lbodies)) -> + let ltypes' = Array.smartmap (f n) ltypes in + let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in + if ltypes == ltypes' && lbodies == lbodies' then lam + else Lfix(init,(ids,ltypes',lbodies')) + | Lcofix(init,(ids,ltypes,lbodies)) -> + let ltypes' = Array.smartmap (f n) ltypes in + let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in + if ltypes == ltypes' && lbodies == lbodies' then lam + else Lcofix(init,(ids,ltypes',lbodies')) + | Lmakeblock(tag,args) -> + let args' = Array.smartmap (f n) args in + if args == args' then lam else Lmakeblock(tag,args') + | Lprim(kn,ar,op,args) -> + let args' = Array.smartmap (f n) args in + if args == args' then lam else Lprim(kn,ar,op,args') + | Lproj(i,kn,arg) -> + let arg' = f n arg in + if arg == arg' then lam else Lproj(i,kn,arg') + | Luint u -> + let u' = map_uint g f n u in + if u == u' then lam else Luint u' + +and map_uint g f n u = + match u with + | UintVal _ -> u + | UintDigits(args) -> + let args' = Array.smartmap (f n) args in + if args == args' then u else UintDigits(args') + | UintDecomp(a) -> + let a' = f n a in + if a == a' then u else UintDecomp(a') + +(*s Lift and substitution *) + + +let rec lam_exlift el lam = + match lam with + | Lrel(id,i) -> + let i' = reloc_rel i el in + if i == i' then lam else Lrel(id,i') + | _ -> map_lam_with_binders el_liftn lam_exlift el lam + +let lam_lift k lam = + if k = 0 then lam + else lam_exlift (el_shft k el_id) lam + +let lam_subst_rel lam id n subst = + match expand_rel n subst with + | Inl(k,v) -> lam_lift k v + | Inr(n',_) -> + if n == n' then lam + else Lrel(id, n') + +let rec lam_exsubst subst lam = + match lam with + | Lrel(id,i) -> lam_subst_rel lam id i subst + | _ -> map_lam_with_binders liftn lam_exsubst subst lam + +let lam_subst_args subst args = + if is_subs_id subst then args + else Array.smartmap (lam_exsubst subst) args + +(** Simplification of lambda expression *) + +(* [simplify subst lam] simplify the expression [lam_subst subst lam] *) +(* that is : *) +(* - Reduce [let] is the definition can be substituted i.e: *) +(* - a variable (rel or identifier) *) +(* - a constant *) +(* - a structured constant *) +(* - a function *) +(* - Transform beta redex into [let] expression *) +(* - Move arguments under [let] *) +(* Invariant : Terms in [subst] are already simplified and can be *) +(* substituted *) + +let can_subst lam = + match lam with + | Lrel _ | Lvar _ | Lconst _ + | Lval _ | Lsort _ | Lind _ | Llam _ -> true + | _ -> false + +let rec simplify subst lam = + match lam with + | Lrel(id,i) -> lam_subst_rel lam id i subst + + | Llet(id,def,body) -> + let def' = simplify subst def in + if can_subst def' then simplify (cons def' subst) body + else + let body' = simplify (lift subst) body in + if def == def' && body == body' then lam + else Llet(id,def',body') + + | Lapp(f,args) -> + begin match simplify_app subst f subst args with + | Lapp(f',args') when f == f' && args == args' -> lam + | lam' -> lam' + end + + | _ -> map_lam_with_binders liftn simplify subst lam + +and simplify_app substf f substa args = + match f with + | Lrel(id, i) -> + begin match lam_subst_rel f id i substf with + | Llam(ids, body) -> + reduce_lapp + subst_id (Array.to_list ids) body + substa (Array.to_list args) + | f' -> mkLapp f' (simplify_args substa args) + end + | Llam(ids, body) -> + reduce_lapp substf (Array.to_list ids) body substa (Array.to_list args) + | Llet(id, def, body) -> + let def' = simplify substf def in + if can_subst def' then + simplify_app (cons def' substf) body substa args + else + Llet(id, def', simplify_app (lift substf) body (shift substa) args) + | Lapp(f, args') -> + let args = Array.append + (lam_subst_args substf args') (lam_subst_args substa args) in + simplify_app substf f subst_id args + | _ -> mkLapp (simplify substf f) (simplify_args substa args) + +and simplify_args subst args = Array.smartmap (simplify subst) args + +and reduce_lapp substf lids body substa largs = + match lids, largs with + | id::lids, a::largs -> + let a = simplify substa a in + if can_subst a then + reduce_lapp (cons a substf) lids body substa largs + else + let body = reduce_lapp (lift substf) lids body (shift substa) largs in + Llet(id, a, body) + | [], [] -> simplify substf body + | _::_, _ -> + Llam(Array.of_list lids, simplify (liftn (List.length lids) substf) body) + | [], _::_ -> simplify_app substf body substa (Array.of_list largs) + + + + +(* [occurrence kind k lam]: + If [kind] is [true] return [true] if the variable [k] does not appear in + [lam], return [false] if the variable appear one time and not + under a lambda, a fixpoint, a cofixpoint; else raise Not_found. + If [kind] is [false] return [false] if the variable does not appear in [lam] + else raise [Not_found] +*) + +let rec occurrence k kind lam = + match lam with + | Lrel (_,n) -> + if n = k then + if kind then false else raise Not_found + else kind + | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ -> kind + | Levar (_, args) -> + occurrence_args k kind args + | Lprod(dom, codom) -> + occurrence k (occurrence k kind dom) codom + | Llam(ids,body) -> + let _ = occurrence (k+Array.length ids) false body in kind + | Llet(_,def,body) -> + occurrence (k+1) (occurrence k kind def) body + | Lapp(f, args) -> + occurrence_args k (occurrence k kind f) args + | Lprim(_,_,_,args) | Lmakeblock(_,args) -> + occurrence_args k kind args + | Lcase(_ci,_rtbl,t,a,branches) -> + let kind = occurrence k (occurrence k kind t) a in + let r = ref kind in + Array.iter (fun c -> r := occurrence k kind c && !r) branches.constant_branches; + let on_b (ids,c) = + r := occurrence (k+Array.length ids) kind c && !r + in + Array.iter on_b branches.nonconstant_branches; + !r + | Lfix(_,(ids,ltypes,lbodies)) + | Lcofix(_,(ids,ltypes,lbodies)) -> + let kind = occurrence_args k kind ltypes in + let _ = occurrence_args (k+Array.length ids) false lbodies in + kind + | Lproj(_,_,arg) -> + occurrence k kind arg + | Luint u -> occurrence_uint k kind u + +and occurrence_args k kind args = + Array.fold_left (occurrence k) kind args + +and occurrence_uint k kind u = + match u with + | UintVal _ -> kind + | UintDigits args -> occurrence_args k kind args + | UintDecomp t -> occurrence k kind t + +let occur_once lam = + try let _ = occurrence 1 true lam in true + with Not_found -> false + +(* [remove_let lam] remove let expression in [lam] if the variable is *) +(* used at most once time in the body, and does not appear under *) +(* a lambda or a fix or a cofix *) + +let rec remove_let subst lam = + match lam with + | Lrel(id,i) -> lam_subst_rel lam id i subst + | Llet(id,def,body) -> + let def' = remove_let subst def in + if occur_once body then remove_let (cons def' subst) body + else + let body' = remove_let (lift subst) body in + if def == def' && body == body' then lam else Llet(id,def',body') + | _ -> map_lam_with_binders liftn remove_let subst lam + + +(*s Translation from [constr] to [lambda] *) + +(* Translation of constructor *) + +(* Limitation due to OCaml's representation of non-constant + constructors: limited to 245 + 1 (0 tag) cases. *) + +exception TooLargeInductive of Pp.t + +let max_nb_const = 0x1000000 +let max_nb_block = 0x1000000 + last_variant_tag - 1 + +let str_max_constructors = + Format.sprintf + " which has more than %i constant constructors or more than %i non-constant constructors" max_nb_const max_nb_block + +let check_compilable ib = + + if not (ib.mind_nb_args <= max_nb_block && ib.mind_nb_constant <= max_nb_const) then + let msg = + Pp.(str "Cannot compile code for virtual machine as it uses inductive " + ++ Id.print ib.mind_typename ++ str str_max_constructors) + in + raise (TooLargeInductive msg) + +let is_value lc = + match lc with + | Lval _ -> true + | _ -> false + +let get_value lc = + match lc with + | Lval v -> v + | _ -> raise Not_found + +let mkConst_b0 n = Lval (Cbytecodes.Const_b0 n) + +let make_args start _end = + Array.init (start - _end + 1) (fun i -> Lrel (Anonymous, start - i)) + +(* Translation of constructors *) +let expand_constructor tag nparams arity = + let ids = Array.make (nparams + arity) Anonymous in + if arity = 0 then mkLlam ids (mkConst_b0 tag) + else + let args = make_args arity 1 in + Llam(ids, Lmakeblock (tag, args)) + +let makeblock tag nparams arity args = + let nargs = Array.length args in + if nparams > 0 || nargs < arity then + mkLapp (expand_constructor tag nparams arity) args + else + (* The constructor is fully applied *) + if arity = 0 then mkConst_b0 tag + else + if Array.for_all is_value args then + if tag < last_variant_tag then + Lval(Cbytecodes.Const_bn(tag, Array.map get_value args)) + else + let args = Array.map get_value args in + let args = Array.append [|Cbytecodes.Const_b0 (tag - last_variant_tag) |] args in + Lval(Cbytecodes.Const_bn(last_variant_tag, args)) + else Lmakeblock(tag, args) + + +(* Compiling constants *) + +let rec get_alias env kn = + let cb = lookup_constant kn env in + let tps = cb.const_body_code in + match tps with + | None -> kn + | Some tps -> + (match Cemitcodes.force tps with + | Cemitcodes.BCalias kn' -> get_alias env kn' + | _ -> kn) + +(* Compilation of primitive *) + +let _h = Name(Id.of_string "f") + +(* +let expand_prim kn op arity = + let ids = Array.make arity Anonymous in + let args = make_args arity 1 in + Llam(ids, prim kn op args) +*) + +let compile_prim n op kn fc args = + if not fc then raise Not_found + else + Lprim(kn, n, op, args) + + (* + let (nparams, arity) = CPrimitives.arity op in + let expected = nparams + arity in + if Array.length args >= expected then prim kn op args + else mkLapp (expand_prim kn op expected) args +*) + +(*i Global environment *) + +let get_names decl = + let decl = Array.of_list decl in + Array.map fst decl + + +(* Rel Environment *) +module Vect = +struct + type 'a t = { + mutable elems : 'a array; + mutable size : int; + } + + let make n a = { + elems = Array.make n a; + size = 0; + } + + let extend v = + if v.size = Array.length v.elems then + let new_size = min (2*v.size) Sys.max_array_length in + if new_size <= v.size then raise (Invalid_argument "Vect.extend"); + let new_elems = Array.make new_size v.elems.(0) in + Array.blit v.elems 0 new_elems 0 (v.size); + v.elems <- new_elems + + let push v a = + extend v; + v.elems.(v.size) <- a; + v.size <- v.size + 1 + + let popn v n = + v.size <- max 0 (v.size - n) + + let pop v = popn v 1 + + let get_last v n = + if v.size <= n then raise + (Invalid_argument "Vect.get:index out of bounds"); + v.elems.(v.size - n - 1) + +end + +let dummy_lambda = Lrel(Anonymous, 0) + +let empty_args = [||] + +module Renv = +struct + + type constructor_info = tag * int * int (* nparam nrealargs *) + + type t = { + global_env : env; + name_rel : Name.t Vect.t; + construct_tbl : (constructor, constructor_info) Hashtbl.t; + } + + let make env = { + global_env = env; + name_rel = Vect.make 16 Anonymous; + construct_tbl = Hashtbl.create 111 + } + + let push_rel env id = Vect.push env.name_rel id + + let push_rels env ids = + Array.iter (push_rel env) ids + + let pop env = Vect.pop env.name_rel + + let popn env n = + for _i = 1 to n do pop env done + + let get env n = + Lrel (Vect.get_last env.name_rel (n-1), n) + + let get_construct_info env c = + try Hashtbl.find env.construct_tbl c + with Not_found -> + let ((mind,j), i) = c in + let oib = lookup_mind mind env.global_env in + let oip = oib.mind_packets.(j) in + check_compilable oip; + let tag,arity = oip.mind_reloc_tbl.(i-1) in + let nparams = oib.mind_nparams in + let r = (tag, nparams, arity) in + Hashtbl.add env.construct_tbl c r; + r +end + +open Renv + +let rec lambda_of_constr env c = + match Constr.kind c with + | Meta _ -> raise (Invalid_argument "Cbytegen.lambda_of_constr: Meta") + | Evar (evk, args) -> + let args = lambda_of_args env 0 args in + Levar (evk, args) + + | Cast (c, _, _) -> lambda_of_constr env c + + | Rel i -> Renv.get env i + + | Var id -> Lvar id + + | Sort s -> Lsort s + | Ind ind -> Lind ind + + | Prod(id, dom, codom) -> + let ld = lambda_of_constr env dom in + Renv.push_rel env id; + let lc = lambda_of_constr env codom in + Renv.pop env; + Lprod(ld, Llam([|id|], lc)) + + | Lambda _ -> + let params, body = decompose_lam c in + let ids = get_names (List.rev params) in + Renv.push_rels env ids; + let lb = lambda_of_constr env body in + Renv.popn env (Array.length ids); + mkLlam ids lb + + | LetIn(id, def, _, body) -> + let ld = lambda_of_constr env def in + Renv.push_rel env id; + let lb = lambda_of_constr env body in + Renv.pop env; + Llet(id, ld, lb) + + | App(f, args) -> lambda_of_app env f args + + | Const _ -> lambda_of_app env c empty_args + + | Construct _ -> lambda_of_app env c empty_args + + | Case(ci,t,a,branches) -> + let ind = ci.ci_ind in + let mib = lookup_mind (fst ind) env.global_env in + let oib = mib.mind_packets.(snd ind) in + let () = check_compilable oib in + let rtbl = oib.mind_reloc_tbl in + + + (* translation of the argument *) + let la = lambda_of_constr env a in + let entry = mkInd ind in + let la = + try + Retroknowledge.get_vm_before_match_info env.global_env.retroknowledge + entry la + with Not_found -> la + in + (* translation of the type *) + let lt = lambda_of_constr env t in + (* translation of branches *) + let consts = Array.make oib.mind_nb_constant dummy_lambda in + let blocks = Array.make oib.mind_nb_args ([||],dummy_lambda) in + for i = 0 to Array.length rtbl - 1 do + let tag, arity = rtbl.(i) in + let b = lambda_of_constr env branches.(i) in + if arity = 0 then consts.(tag) <- b + else + let b = + match b with + | Llam(ids, body) when Array.length ids = arity -> (ids, body) + | _ -> + let ids = Array.make arity Anonymous in + let args = make_args arity 1 in + let ll = lam_lift arity b in + (ids, mkLapp ll args) + in blocks.(tag-1) <- b + done; + let branches = + { constant_branches = consts; + nonconstant_branches = blocks } + in + Lcase(ci, rtbl, lt, la, branches) + + | Fix(rec_init,(names,type_bodies,rec_bodies)) -> + let ltypes = lambda_of_args env 0 type_bodies in + Renv.push_rels env names; + let lbodies = lambda_of_args env 0 rec_bodies in + Renv.popn env (Array.length names); + Lfix(rec_init, (names, ltypes, lbodies)) + + | CoFix(init,(names,type_bodies,rec_bodies)) -> + let ltypes = lambda_of_args env 0 type_bodies in + Renv.push_rels env names; + let lbodies = lambda_of_args env 0 rec_bodies in + Renv.popn env (Array.length names); + Lcofix(init, (names, ltypes, lbodies)) + + | Proj (p,c) -> + let kn = Projection.constant p in + let cb = lookup_constant kn env.global_env in + let pb = Option.get cb.const_proj in + let n = pb.proj_arg in + let lc = lambda_of_constr env c in + Lproj (n,kn,lc) + +and lambda_of_app env f args = + match Constr.kind f with + | Const (kn,u as c) -> + let kn = get_alias env.global_env kn in + (* spiwack: checks if there is a specific way to compile the constant + if there is not, Not_found is raised, and the function + falls back on its normal behavior *) + (try + (* We delay the compilation of arguments to avoid an exponential behavior *) + let f = Retroknowledge.get_vm_compiling_info env.global_env.retroknowledge + (mkConstU (kn,u)) in + let args = lambda_of_args env 0 args in + f args + with Not_found -> + let cb = lookup_constant kn env.global_env in + begin match cb.const_body with + | Def csubst when cb.const_inline_code -> + lambda_of_app env (Mod_subst.force_constr csubst) args + | Def _ | OpaqueDef _ | Undef _ -> mkLapp (Lconst c) (lambda_of_args env 0 args) + end) + | Construct (c,_) -> + let tag, nparams, arity = Renv.get_construct_info env c in + let nargs = Array.length args in + if Int.equal (nparams + arity) nargs then (* fully applied *) + (* spiwack: *) + (* 1/ tries to compile the constructor in an optimal way, + it is supposed to work only if the arguments are + all fully constructed, fails with Cbytecodes.NotClosed. + it can also raise Not_found when there is no special + treatment for this constructor + for instance: tries to to compile an integer of the + form I31 D1 D2 ... D31 to [D1D2...D31] as + a processor number (a caml number actually) *) + try + try + Retroknowledge.get_vm_constant_static_info + env.global_env.retroknowledge + f args + with NotClosed -> + (* 2/ if the arguments are not all closed (this is + expectingly (and it is currently the case) the only + reason why this exception is raised) tries to + give a clever, run-time behavior to the constructor. + Raises Not_found if there is no special treatment + for this integer. + this is done in a lazy fashion, using the constructor + Bspecial because it needs to know the continuation + and such, which can't be done at this time. + for instance, for int31: if one of the digit is + not closed, it's not impossible that the number + gets fully instanciated at run-time, thus to ensure + uniqueness of the representation in the vm + it is necessary to try and build a caml integer + during the execution *) + let rargs = Array.sub args nparams arity in + let args = lambda_of_args env nparams rargs in + Retroknowledge.get_vm_constant_dynamic_info + env.global_env.retroknowledge + f args + with Not_found -> + (* 3/ if no special behavior is available, then the compiler + falls back to the normal behavior *) + let args = lambda_of_args env nparams args in + makeblock tag 0 arity args + else + let args = lambda_of_args env nparams args in + (* spiwack: tries first to apply the run-time compilation + behavior of the constructor, as in 2/ above *) + (try + (Retroknowledge.get_vm_constant_dynamic_info + env.global_env.retroknowledge + f) args + with Not_found -> + if nparams <= nargs then (* got all parameters *) + makeblock tag 0 arity args + else (* still expecting some parameters *) + makeblock tag (nparams - nargs) arity empty_args) + | _ -> + let f = lambda_of_constr env f in + let args = lambda_of_args env 0 args in + mkLapp f args + +and lambda_of_args env start args = + let nargs = Array.length args in + if start < nargs then + Array.init (nargs - start) + (fun i -> lambda_of_constr env args.(start + i)) + else empty_args + + + + +(*********************************) + + +let optimize_lambda lam = + let lam = simplify subst_id lam in + remove_let subst_id lam + +let lambda_of_constr ~optimize genv c = + let env = Renv.make genv in + let ids = List.rev_map Context.Rel.Declaration.get_name genv.env_rel_context.env_rel_ctx in + Renv.push_rels env (Array.of_list ids); + let lam = lambda_of_constr env c in + let lam = if optimize then optimize_lambda lam else lam in + if !Flags.dump_lambda then + Feedback.msg_debug (pp_lam lam); + lam + +(** Retroknowledge, to be removed once we move to primitive machine integers *) +let compile_structured_int31 fc args = + if not fc then raise Not_found else + Luint (UintVal + (Uint31.of_int (Array.fold_left + (fun temp_i -> fun t -> match kind t with + | Construct ((_,d),_) -> 2*temp_i+d-1 + | _ -> raise NotClosed) + 0 args))) + +let dynamic_int31_compilation fc args = + if not fc then raise Not_found else + Luint (UintDigits args) + +(* We are relying here on the tags of digits constructors *) +let digits_from_uint i = + let d0 = mkConst_b0 0 in + let d1 = mkConst_b0 1 in + let digits = Array.make 31 d0 in + for k = 0 to 30 do + if Int.equal ((Uint31.to_int i lsr k) land 1) 1 then + digits.(30-k) <- d1 + done; + digits + +let int31_escape_before_match fc t = + if not fc then + raise Not_found + else + match t with + | Luint (UintVal i) -> + let digits = digits_from_uint i in + Lmakeblock (1, digits) + | Luint (UintDigits args) -> + Lmakeblock (1,args) + | Luint (UintDecomp _) -> + assert false + | _ -> Luint (UintDecomp t) diff --git a/kernel/clambda.mli b/kernel/clambda.mli new file mode 100644 index 0000000000..89b7fd8e3b --- /dev/null +++ b/kernel/clambda.mli @@ -0,0 +1,27 @@ +open Names +open Cinstr + +exception TooLargeInductive of Pp.t + +val lambda_of_constr : optimize:bool -> Pre_env.env -> Constr.t -> lambda + +val decompose_Llam : lambda -> Name.t array * lambda + +val get_alias : Pre_env.env -> Constant.t -> Constant.t + +val compile_prim : int -> Cbytecodes.instruction -> Constr.pconstant -> bool -> lambda array -> lambda + +(** spiwack: this function contains the information needed to perform + the static compilation of int31 (trying and obtaining + a 31-bit integer in processor representation at compile time) *) +val compile_structured_int31 : bool -> Constr.t array -> lambda + +(** this function contains the information needed to perform + the dynamic compilation of int31 (trying and obtaining a + 31-bit integer in processor representation at runtime when + it failed at compile time *) +val dynamic_int31_compilation : bool -> lambda array -> lambda + +(*spiwack: compiling function to insert dynamic decompilation before + matching integers (in case they are in processor representation) *) +val int31_escape_before_match : bool -> lambda -> lambda diff --git a/kernel/constr.ml b/kernel/constr.ml index 1ff1fcc4c0..2cbcdd76e3 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* File initially created by Gérard Huet and Thierry Coquand in 1984 *) diff --git a/kernel/constr.mli b/kernel/constr.mli index 19ffa8fe30..f7e4eecbad 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This file defines the most important datatype of Coq, namely kernel terms, diff --git a/kernel/context.ml b/kernel/context.ml index d635c4515b..4f3f649c14 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Jean-Christophe Filliâtre out of names.ml as part of the diff --git a/kernel/context.mli b/kernel/context.mli index c3ecd8d4ea..c97db4348e 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** The modules defined below represent a {e local context} diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index ca568fc6ec..7ef63c1860 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Bruno Barras as part of the rewriting of the conversion diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index 02c179ab69..67add5dd35 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 23a578d993..6f4541e956 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Jean-Christophe Filliâtre out of V6.3 file constants.ml diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 7696d7545d..7bd0ae5663 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Constr diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 55430a9d81..0129489542 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Bruno Barras for Benjamin Grégoire as part of the @@ -150,6 +152,7 @@ and slot_for_fv env fv = env |> Pre_env.lookup_rel i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel | Some (v, _) -> v end + | FVevar evk -> val_of_evar evk | FVuniv_var idu -> assert false @@ -164,7 +167,7 @@ and eval_to_patch env (buff,pl,fv) = eval_tcode tc vm_env and val_of_constr env c = - match compile true env c with + match compile ~fail_on_error:true env c with | Some v -> eval_to_patch env (to_memory v) | None -> assert false diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli index fc935f6ee9..19b2b8b50a 100644 --- a/kernel/csymtable.mli +++ b/kernel/csymtable.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* $Id$ *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index cb7f0ecef3..b7427d20a7 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 9eed9efcbd..3652a1ce44 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Declarations diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 0eed11f49c..fb46112ea7 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Declarations diff --git a/kernel/entries.ml b/kernel/entries.ml index 36b75668b2..94da00c7eb 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/environ.ml b/kernel/environ.ml index 738ecc6e1f..9d4063e433 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Author: Jean-Christophe Filliâtre as part of the rebuilding of Coq @@ -468,7 +470,7 @@ type unsafe_type_judgment = types punsafe_type_judgment (*s Compilation of global declaration *) -let compile_constant_body = Cbytegen.compile_constant_body false +let compile_constant_body = Cbytegen.compile_constant_body ~fail_on_error:false exception Hyp_not_found @@ -560,7 +562,7 @@ let dispatch = it to the name of the coq definition in the reactive retroknowledge) *) let int31_op n op prim kn = { empty_reactive_info with - vm_compiling = Some (Cbytegen.op_compilation n op kn); + vm_compiling = Some (Clambda.compile_prim n op kn); native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn)); } in @@ -599,13 +601,13 @@ fun rk value field -> in { empty_reactive_info with vm_decompile_const = Some int31_decompilation; - vm_before_match = Some Cbytegen.int31_escape_before_match; + vm_before_match = Some Clambda.int31_escape_before_match; native_before_match = Some (Nativelambda.before_match_int31 i31bit_type); } | KInt31 (_, Int31Constructor) -> { empty_reactive_info with - vm_constant_static = Some Cbytegen.compile_structured_int31; - vm_constant_dynamic = Some Cbytegen.dynamic_int31_compilation; + vm_constant_static = Some Clambda.compile_structured_int31; + vm_constant_dynamic = Some Clambda.dynamic_int31_compilation; native_constant_static = Some Nativelambda.compile_static_int31; native_constant_dynamic = Some Nativelambda.compile_dynamic_int31; } diff --git a/kernel/environ.mli b/kernel/environ.mli index 69d811a642..4e6ac1e725 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -199,7 +201,7 @@ val lookup_modtype : ModPath.t -> env -> module_type_body (** {5 Universe constraints } *) (** Add universe constraints to the environment. - @raises UniverseInconsistency + @raise UniverseInconsistency . *) val add_constraints : Univ.Constraint.t -> env -> env diff --git a/kernel/esubst.ml b/kernel/esubst.ml index ac2b3f9d59..a11a0dc00c 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Bruno Barras for Coq V7.0, Mar 2001 *) diff --git a/kernel/esubst.mli b/kernel/esubst.mli index 95a2e71c2c..b82d6fdf02 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Explicit substitutions *) diff --git a/kernel/evar.ml b/kernel/evar.ml index dcd2e12a0c..bbe143092b 100644 --- a/kernel/evar.ml +++ b/kernel/evar.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) type t = int diff --git a/kernel/evar.mli b/kernel/evar.mli index 6a058207f6..d14cdce27a 100644 --- a/kernel/evar.mli +++ b/kernel/evar.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This module defines existential variables, which are isomorphic to [int]. diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index cfca335d32..439acd15bf 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 9a9380adb1..5a38172c2d 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 722705bd70..9bed598bb7 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors @@ -1067,6 +1069,9 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = try find_inductive env a with Not_found -> raise_err env i (RecursionNotOnInductiveType a) in + let mib,_ = lookup_mind_specif env (out_punivs mind) in + if mib.mind_finite != Finite then + raise_err env i (RecursionNotOnInductiveType a); (mind, (env', b)) else check_occur env' (n+1) b else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call.") diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 8aaeee831b..c7982f1fc1 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 749854b8cd..370185a721 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -23,8 +23,9 @@ Declareops Retroknowledge Conv_oracle Pre_env -Cbytegen +Clambda Nativelambda +Cbytegen Nativecode Nativelib Environ diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 2c8ef477fc..9c2fa05465 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Claudio Sacerdoti from contents of term.ml, names.ml and diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 1aa7ba519c..b14d392073 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** {6 [Mod_subst] } *) diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 6b89a1da03..1baab7c98c 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index 1225c3e1e3..e74f455efe 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Declarations diff --git a/kernel/modops.ml b/kernel/modops.ml index 11e6be6598..bbf160db21 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of diff --git a/kernel/modops.mli b/kernel/modops.mli index bbb4c918c3..cb41a5123a 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/names.ml b/kernel/names.ml index b02c0b8409..6fa44c0610 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* File created around Apr 1994 for CiC V5.10.5 by Chet Murthy collecting diff --git a/kernel/names.mli b/kernel/names.mli index b1e8efd8d1..209826c1ff 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This file defines a lot of different notions of names used pervasively in diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 8fa2540536..c82d982b4b 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 7d20054f77..4b23cc5f8b 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names open Constr diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index bfa9821360..c71f746bec 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli index 769deacae5..2111739d5e 100644 --- a/kernel/nativeconv.mli +++ b/kernel/nativeconv.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Constr open Reduction diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index 48ad884440..9c17cc2b5f 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names open Constr diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 29b3e59da8..01ddffe3ef 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util open Names @@ -83,9 +85,9 @@ let get_const_prefix env c = (* A generic map function *) -let map_lam_with_binders g f n lam = +let rec map_lam_with_binders g f n lam = match lam with - | Lrel _ | Lvar _ | Lconst _ | Lproj _ | Luint _ | Lval _ | Lsort _ | Lind _ + | Lrel _ | Lvar _ | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _ | Lconstruct _ | Llazy | Lforce | Lmeta _ | Levar _ -> lam | Lprod(dom,codom) -> let dom' = f n dom in @@ -134,6 +136,19 @@ let map_lam_with_binders g f n lam = | Lmakeblock(prefix,cn,tag,args) -> let args' = Array.smartmap (f n) args in if args == args' then lam else Lmakeblock(prefix,cn,tag,args') + | Luint u -> + let u' = map_uint g f n u in + if u == u' then lam else Luint u' + +and map_uint g f n u = + match u with + | UintVal _ -> u + | UintDigits(prefix,c,args) -> + let args' = Array.smartmap (f n) args in + if args == args' then u else UintDigits(prefix,c,args') + | UintDecomp(prefix,c,a) -> + let a' = f n a in + if a == a' then u else UintDecomp(prefix,c,a') (*s Lift and substitution *) diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 933fbc660f..9a1e19b3cb 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names open Constr diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 1e35f6c036..31ad364911 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util open Nativevalues diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index b74d4fdd05..25adcf224b 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Nativecode diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index c68f781213..c69cf722bc 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli index 72e3d80413..31e5255fc4 100644 --- a/kernel/nativelibrary.mli +++ b/kernel/nativelibrary.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names open Declarations diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 3d47b1672e..cfcb0a485b 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 993842740b..4a58a3c7da 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Constr open Names diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index c2fcfbfd6a..a484c08e8d 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index c8339e6eb3..b6ae80b46a 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 6c5e1cde5a..8ebe48e202 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Benjamin Grégoire out of environ.ml for better diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index a6b57bd1b3..b05074814b 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/reduction.ml b/kernel/reduction.ml index da7042713f..b3e6894143 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created under Benjamin Werner account by Bruno Barras to implement @@ -267,8 +269,9 @@ let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u if not (Int.equal num_cnstr_args nargs) then cmp_instances u1 u2 s else - let csts = get_cumulativity_constraints CONV cumi u1 u2 in - cmp_cumul csts s + (** By invariant, both constructors have a common supertype, + so they are convertible _at that type_. *) + s let convert_constructors ctor nargs u1 u2 (s, check) = convert_constructors_gen (check.compare_instances ~flex:false) check.compare_cumul_instances @@ -918,7 +921,6 @@ let dest_prod_assum env = | LetIn (x,b,t,c) -> let d = LocalDef (x,b,t) in prodec_rec (push_rel d env) (Context.Rel.add d l) c - | Cast (c,_,_) -> prodec_rec env l c | _ -> let rty' = whd_all env rty in if Constr.equal rty' rty then l, rty @@ -936,7 +938,6 @@ let dest_lam_assum env = | LetIn (x,b,t,c) -> let d = LocalDef (x,b,t) in lamec_rec (push_rel d env) (Context.Rel.add d l) c - | Cast (c,_,_) -> lamec_rec env l c | _ -> l,rty in lamec_rec env Context.Rel.empty diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 6f7e3f8f8f..ad52c93f62 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Constr diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index 88cf93acc9..d76b05a8bb 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Arnaud Spiwack, May 2007 *) @@ -102,20 +104,18 @@ module Reactive = Map.Make (EntryOrd) type reactive_info = {(*information required by the compiler of the VM *) vm_compiling : (*fastcomputation flag -> continuation -> result *) - (bool -> Cbytecodes.comp_env -> constr array -> - int->Cbytecodes.bytecodes->Cbytecodes.bytecodes) + (bool -> Cinstr.lambda array -> Cinstr.lambda) option; vm_constant_static : (*fastcomputation flag -> constructor -> args -> result*) - (bool->constr array->Cbytecodes.structured_constant) + (bool -> constr array -> Cinstr.lambda) option; vm_constant_dynamic : (*fastcomputation flag -> constructor -> reloc -> args -> sz -> cont -> result *) - (bool->Cbytecodes.comp_env->Cbytecodes.block array->int-> - Cbytecodes.bytecodes->Cbytecodes.bytecodes) + (bool -> Cinstr.lambda array -> Cinstr.lambda) option; (* fastcomputation flag -> cont -> result *) - vm_before_match : (bool -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes) option; + vm_before_match : (bool -> Cinstr.lambda -> Cinstr.lambda) option; (* tag (= compiled int for instance) -> result *) vm_decompile_const : (int -> constr) option; diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index e4d78ba14f..0334e7a9e9 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -82,9 +84,8 @@ val initial_retroknowledge : retroknowledge and the continuation cont of the bytecode compilation returns the compilation of id in cont if it has a specific treatment or raises Not_found if id should be compiled as usual *) -val get_vm_compiling_info : retroknowledge -> entry -> Cbytecodes.comp_env -> - constr array -> - int -> Cbytecodes.bytecodes-> Cbytecodes.bytecodes +val get_vm_compiling_info : retroknowledge -> entry -> + Cinstr.lambda array -> Cinstr.lambda (*Given an identifier id (usually Construct _) and its argument array, returns a function that tries an ad-hoc optimisated compilation (in the case of the 31-bit integers it means compiling them @@ -93,8 +94,7 @@ val get_vm_compiling_info : retroknowledge -> entry -> Cbytecodes.comp_env -> CBytecodes.NotClosed if the term is not a closed constructor pattern (a constant for the compiler) *) val get_vm_constant_static_info : retroknowledge -> entry -> - constr array -> - Cbytecodes.structured_constant + constr array -> Cinstr.lambda (*Given an identifier id (usually Construct _ ) its argument array and a continuation, returns the compiled version @@ -102,16 +102,14 @@ val get_vm_constant_static_info : retroknowledge -> entry -> 31-bit integers, that would be the dynamic compilation into integers) or raises Not_found if id should be compiled as usual *) val get_vm_constant_dynamic_info : retroknowledge -> entry -> - Cbytecodes.comp_env -> - Cbytecodes.block array -> - int -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes + Cinstr.lambda array -> Cinstr.lambda (** Given a type identifier, this function is used before compiling a match over this type. In the case of 31-bit integers for instance, it is used to add the instruction sequence which would perform a dynamic decompilation in case the argument of the match is not in coq representation *) -val get_vm_before_match_info : retroknowledge -> entry -> Cbytecodes.bytecodes - -> Cbytecodes.bytecodes +val get_vm_before_match_info : retroknowledge -> entry -> Cinstr.lambda + -> Cinstr.lambda (** Given a type identifier, this function is used by pretyping/vnorm.ml to recover the elements of that type from their compiled form if it's non @@ -148,20 +146,18 @@ val find : retroknowledge -> field -> entry type reactive_info = {(*information required by the compiler of the VM *) vm_compiling : (*fastcomputation flag -> continuation -> result *) - (bool->Cbytecodes.comp_env->constr array -> - int->Cbytecodes.bytecodes->Cbytecodes.bytecodes) + (bool -> Cinstr.lambda array -> Cinstr.lambda) option; vm_constant_static : (*fastcomputation flag -> constructor -> args -> result*) - (bool->constr array->Cbytecodes.structured_constant) + (bool -> constr array -> Cinstr.lambda) option; vm_constant_dynamic : (*fastcomputation flag -> constructor -> reloc -> args -> sz -> cont -> result *) - (bool->Cbytecodes.comp_env->Cbytecodes.block array->int-> - Cbytecodes.bytecodes->Cbytecodes.bytecodes) + (bool -> Cinstr.lambda array -> Cinstr.lambda) option; (* fastcomputation flag -> cont -> result *) - vm_before_match : (bool -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes) option; + vm_before_match : (bool -> Cinstr.lambda -> Cinstr.lambda) option; (* tag (= compiled int for instance) -> result *) vm_decompile_const : (int -> constr) option; diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 93b8e278fa..de2a890fb5 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Jean-Christophe Filliâtre as part of the rebuilding of diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 757b803a39..4078a9092d 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/sorts.ml b/kernel/sorts.ml index 07688840dd..daeb90be7f 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Univ diff --git a/kernel/sorts.mli b/kernel/sorts.mli index 65ea751386..1bbde26083 100644 --- a/kernel/sorts.mli +++ b/kernel/sorts.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** {6 The sorts of CCI. } *) diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index e95d5d2b57..8cf588c3ea 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli index 67df3759ec..4e755e42ff 100644 --- a/kernel/subtyping.mli +++ b/kernel/subtyping.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Univ diff --git a/kernel/term.ml b/kernel/term.ml index a4c92bd333..403ed881c5 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util diff --git a/kernel/term.mli b/kernel/term.mli index b4597676a3..ba521978e7 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 9b864440d1..e621a61c76 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 7bc029010f..6a0ff072f5 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 781c6bfbcd..1c323e3ea2 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 72861f6e48..20bf300ac3 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 4a935f581a..be4c0e1ecc 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 5584b6ab46..bff40b017f 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index f1e8d10317..5d1644614d 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -833,7 +835,7 @@ let sort_universes g = (** Subtyping of polymorphic contexts *) let check_subtype univs ctxT ctx = - if AUContext.size ctx == AUContext.size ctx then + if AUContext.size ctxT == AUContext.size ctx then let (inst, cst) = UContext.dest (AUContext.repr ctx) in let cstT = UContext.constraints (AUContext.repr ctxT) in let push accu v = add_universe v false accu in diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index f71d83d853..d4fba63fb3 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Univ @@ -41,7 +43,7 @@ val check_constraint : t -> univ_constraint -> bool val check_constraints : Constraint.t -> t -> bool (** Adds a universe to the graph, ensuring it is >= or > Set. - @raises AlreadyDeclared if the level is already declared in the graph. *) + @raise AlreadyDeclared if the level is already declared in the graph. *) exception AlreadyDeclared diff --git a/kernel/univ.ml b/kernel/univ.ml index c42b667492..584593e2fc 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created in Caml by Gérard Huet for CoC 4.8 [Dec 1988] *) diff --git a/kernel/univ.mli b/kernel/univ.mli index 74d1bfd3a8..ce617932cc 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Universes. *) diff --git a/kernel/vars.ml b/kernel/vars.ml index b3b3eff628..0f588a6302 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -310,6 +312,3 @@ let subst_instance_constr subst c = let subst_instance_context s ctx = if Univ.Instance.is_empty s then ctx else Context.Rel.map (fun x -> subst_instance_constr s x) ctx - -type id_key = Constant.t 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 b74d25260f..a0c7ba4bd2 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -137,6 +139,3 @@ val subst_univs_level_context : Univ.universe_level_subst -> Context.Rel.t -> Co (** Instance substitution for polymorphism. *) val subst_instance_constr : Instance.t -> constr -> constr val subst_instance_context : Instance.t -> Context.Rel.t -> Context.Rel.t - -type id_key = Constant.t tableKey -val eq_id_key : id_key -> id_key -> bool diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 8c76581478..f11803b67c 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -44,7 +44,6 @@ let rec conv_val env pb k v1 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 @@ -81,7 +80,7 @@ and conv_whd env pb k whd1 whd2 cu = (* on the fly eta expansion *) conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu - | Vsort _, _ | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _ + | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _ | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible @@ -116,11 +115,12 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = 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 + if Vmvalues.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then conv_stack env k stk1 stk2 cu else raise NotConvertible - | Atype _ , _ | _, Atype _ -> assert false - | Aind _, _ | Aid _, _ -> raise NotConvertible + | Asort s1, Asort s2 -> + sort_cmp_universes env pb s1 s2 cu + | Asort _ , _ | Aind _, _ | Aid _, _ -> raise NotConvertible and conv_stack env k stk1 stk2 cu = match stk1, stk2 with diff --git a/kernel/vconv.mli b/kernel/vconv.mli index c3c9636e89..620f6b5e8a 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Constr diff --git a/kernel/vm.ml b/kernel/vm.ml index 352ea74a41..14aeb732f9 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Cbytecodes @@ -28,7 +30,6 @@ let popstop_code i = let stop = popstop_code 0 - (************************************************) (* Abstract machine *****************************) (************************************************) @@ -70,7 +71,6 @@ let apply_varray vf varray = interprete (fun_code vf) (fun_val vf) (fun_env vf) (n - 1) end -(* Functions over vfun *) let mkrel_vstack k arity = let max = k + arity - 1 in Array.init arity (fun i -> val_of_rel (max - i)) @@ -168,7 +168,7 @@ let rec apply_stack a stk v = let apply_whd k whd = let v = val_of_rel k in match whd with - | Vsort _ | Vprod _ | Vconstr_const _ | Vconstr_block _ -> assert false + | Vprod _ | Vconstr_const _ | Vconstr_block _ -> assert false | Vfun f -> reduce_fun k f | Vfix(f, None) -> push_ra stop; diff --git a/kernel/vm.mli b/kernel/vm.mli index c6d92ba266..50ebc90626 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Vmvalues diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 2d8a1d9761..0e0cb4e584 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names open Sorts @@ -118,10 +120,23 @@ type vswitch = { (* Do not edit this type without editing C code, especially "coq_values.h" *) +type id_key = +| ConstKey of Constant.t +| VarKey of Id.t +| RelKey of Int.t +| EvarKey of Evar.t + +let eq_id_key k1 k2 = match k1, k2 with +| ConstKey c1, ConstKey c2 -> Constant.equal c1 c2 +| VarKey id1, VarKey id2 -> Id.equal id1 id2 +| RelKey n1, RelKey n2 -> Int.equal n1 n2 +| EvarKey evk1, EvarKey evk2 -> Evar.equal evk1 evk2 +| _ -> false + type atom = - | Aid of Vars.id_key + | Aid of id_key | Aind of inductive - | Atype of Univ.Universe.t + | Asort of Sorts.t (* Zippers *) @@ -136,7 +151,6 @@ type stack = zipper list type to_update = values type whd = - | Vsort of Sorts.t | Vprod of vprod | Vfun of vfun | Vfix of vfix * arguments option @@ -167,7 +181,6 @@ let uni_lvl_val (v : values) : Univ.Level.t = let pr = let open Pp in match whd with - | Vsort _ -> str "Vsort" | Vprod _ -> str "Vprod" | Vfun _ -> str "Vfun" | Vfix _ -> str "Vfix" @@ -189,12 +202,17 @@ let rec whd_accu a stk = match Obj.tag at with | i when Int.equal i type_atom_tag -> begin match stk with + | [] -> Vatom_stk(Obj.magic at, stk) | [Zapp args] -> let args = Array.init (nargs args) (arg args) in - let u = Obj.obj (Obj.field at 0) in - let inst = Instance.of_array (Array.map uni_lvl_val args) in - let u = Univ.subst_instance_universe inst u in - Vsort (Type u) + let s = Obj.obj (Obj.field at 0) in + begin match s with + | Type u -> + let inst = Instance.of_array (Array.map uni_lvl_val args) in + let u = Univ.subst_instance_universe inst u in + Vatom_stk (Asort (Type u), []) + | _ -> assert false + end | _ -> assert false end | i when i <= max_atom_tag -> @@ -243,11 +261,8 @@ let whd_val : values -> whd = else let tag = Obj.tag o in if tag = accu_tag then - ( - if Int.equal (Obj.size o) 1 then Obj.obj o (* sort *) - else - if is_accumulate (fun_code o) then whd_accu o [] - else Vprod(Obj.obj o)) + if is_accumulate (fun_code o) then whd_accu o [] + else Vprod(Obj.obj o) else if tag = Obj.closure_tag || tag = Obj.infix_tag then (match kind_of_closure o with @@ -273,7 +288,7 @@ let obj_of_atom : atom -> Obj.t = (* obj_of_str_const : structured_constant -> Obj.t *) let rec obj_of_str_const str = match str with - | Const_sorts s -> Obj.repr (Vsort s) + | Const_sort s -> obj_of_atom (Asort s) | Const_ind ind -> obj_of_atom (Aind ind) | Const_proj p -> Obj.repr p | Const_b0 tag -> Obj.repr tag @@ -285,7 +300,6 @@ let rec obj_of_str_const str = 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) @@ -304,13 +318,14 @@ let val_of_proj kn v = module IdKeyHash = struct - type t = Constant.t tableKey - let equal = Names.eq_table_key Constant.equal + type t = id_key + let equal = eq_id_key open Hashset.Combine let hash = function | ConstKey c -> combinesmall 1 (Constant.hash c) | VarKey id -> combinesmall 2 (Id.hash id) | RelKey i -> combinesmall 3 (Int.hash i) + | EvarKey evk -> combinesmall 4 (Evar.hash evk) end module KeyTable = Hashtbl.Make(IdKeyHash) @@ -330,6 +345,8 @@ let val_of_named id = val_of_idkey (VarKey id) let val_of_constant c = val_of_idkey (ConstKey c) +let val_of_evar evk = val_of_idkey (EvarKey evk) + external val_of_annot_switch : annot_switch -> values = "%identity" (*************************************************) @@ -502,10 +519,9 @@ let rec pr_atom a = | RelKey i -> str "#" ++ int i | _ -> str "...") ++ str ")" | Aind (mi,i) -> str "Aind(" ++ MutInd.print mi ++ str "#" ++ int i ++ str ")" - | Atype _ -> str "Atype(") + | Asort _ -> str "Asort(") and pr_whd w = Pp.(match w with - | Vsort _ -> str "Vsort" | Vprod _ -> str "Vprod" | Vfun _ -> str "Vfun" | Vfix _ -> str "Vfix" diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index 350f71372f..c6e342a965 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -54,10 +56,18 @@ val fun_code : vfun -> tcode val fix_code : vfix -> tcode val cofix_upd_code : to_update -> tcode +type id_key = +| ConstKey of Constant.t +| VarKey of Id.t +| RelKey of Int.t +| EvarKey of Evar.t + +val eq_id_key : id_key -> id_key -> bool + type atom = - | Aid of Vars.id_key + | Aid of id_key | Aind of inductive - | Atype of Univ.Universe.t + | Asort of Sorts.t (** Zippers *) @@ -70,7 +80,6 @@ type zipper = type stack = zipper list type whd = - | Vsort of Sorts.t | Vprod of vprod | Vfun of vfun | Vfix of vfix * arguments option @@ -92,6 +101,7 @@ 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 : Constant.t -> values +val val_of_evar : Evar.t -> values val val_of_proj : Constant.t -> values -> values val val_of_atom : atom -> values |