diff options
Diffstat (limited to 'kernel')
93 files changed, 2467 insertions, 1475 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 219ea5b24a..5f683790c1 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 @@ -257,12 +259,14 @@ module KeyTable = Hashtbl.Make(IdKeyHash) let eq_table_key = IdKeyHash.equal +type 'a infos_tab = 'a KeyTable.t + type 'a infos_cache = { - i_repr : 'a infos -> constr -> 'a; + i_repr : 'a infos -> 'a infos_tab -> constr -> 'a; i_env : env; i_sigma : existential -> constr option; i_rels : (Context.Rel.Declaration.t * Pre_env.lazy_val) Range.t; - i_tab : 'a KeyTable.t } +} and 'a infos = { i_flags : reds; @@ -277,9 +281,9 @@ let assoc_defined id env = match Environ.lookup_named id env with | LocalDef (_, c, _) -> c | _ -> raise Not_found -let ref_value_cache ({i_cache = cache} as infos) ref = +let ref_value_cache ({i_cache = cache} as infos) tab ref = try - Some (KeyTable.find cache.i_tab ref) + Some (KeyTable.find tab ref) with Not_found -> try let body = @@ -298,8 +302,8 @@ let ref_value_cache ({i_cache = cache} as infos) ref = | VarKey id -> assoc_defined id cache.i_env | ConstKey cst -> constant_value_in cache.i_env cst in - let v = cache.i_repr infos body in - KeyTable.add cache.i_tab ref v; + let v = cache.i_repr infos tab body in + KeyTable.add tab ref v; Some v with | Not_found (* List.assoc *) @@ -316,7 +320,7 @@ let create mk_cl flgs env evars = i_env = env; i_sigma = evars; i_rels = (Environ.pre_env env).env_rel_context.env_rel_map; - i_tab = KeyTable.create 17 } + } in { i_flags = flgs; i_cache = cache } @@ -796,7 +800,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') = @@ -904,23 +908,23 @@ and knht info e t stk = (************************************************************************) (* Computes a weak head normal form from the result of knh. *) -let rec knr info m stk = +let rec knr info tab m stk = match m.term with | FLambda(n,tys,f,e) when red_set info.i_flags fBETA -> (match get_args n tys f e stk with - Inl e', s -> knit info e' f s + Inl e', s -> knit info tab e' f s | Inr lam, s -> (lam,s)) | FFlex(ConstKey (kn,_ as c)) when red_set info.i_flags (fCONST kn) -> - (match ref_value_cache info (ConstKey c) with - Some v -> kni info v stk + (match ref_value_cache info tab (ConstKey c) with + Some v -> kni info tab v stk | None -> (set_norm m; (m,stk))) | FFlex(VarKey id) when red_set info.i_flags (fVAR id) -> - (match ref_value_cache info (VarKey id) with - Some v -> kni info v stk + (match ref_value_cache info tab (VarKey id) with + Some v -> kni info tab v stk | None -> (set_norm m; (m,stk))) | FFlex(RelKey k) when red_set info.i_flags fDELTA -> - (match ref_value_cache info (RelKey k) with - Some v -> kni info v stk + (match ref_value_cache info tab (RelKey k) with + Some v -> kni info tab v stk | None -> (set_norm m; (m,stk))) | FConstruct((ind,c),u) -> let use_match = red_set info.i_flags fMATCH in @@ -930,29 +934,29 @@ let rec knr info m stk = | (depth, args, ZcaseT(ci,_,br,e)::s) when use_match -> assert (ci.ci_npar>=0); let rargs = drop_parameters depth ci.ci_npar args in - knit info e br.(c-1) (rargs@s) + knit info tab e br.(c-1) (rargs@s) | (_, cargs, Zfix(fx,par)::s) when use_fix -> let rarg = fapp_stack(m,cargs) in let stk' = par @ append_stack [|rarg|] s in let (fxe,fxbd) = contract_fix_vect fx.term in - knit info fxe fxbd stk' + knit info tab fxe fxbd stk' | (depth, args, Zproj (n, m, cst)::s) when use_match -> let rargs = drop_parameters depth n args in let rarg = project_nth_arg m rargs in - kni info rarg s + kni info tab rarg s | (_,args,s) -> (m,args@s)) else (m,stk) | FCoFix _ when red_set info.i_flags fCOFIX -> (match strip_update_shift_app m stk with (_, args, (((ZcaseT _|Zproj _)::_) as stk')) -> let (fxe,fxbd) = contract_fix_vect m.term in - knit info fxe fxbd (args@stk') + knit info tab fxe fxbd (args@stk') | (_,args,s) -> (m,args@s)) | FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA -> - knit info (subs_cons([|v|],e)) bd stk + knit info tab (subs_cons([|v|],e)) bd stk | FEvar(ev,env) -> (match evar_value info.i_cache ev with - Some c -> knit info env c stk + Some c -> knit info tab env c stk | None -> (m,stk)) | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FApp _ | FProj _ | FFix _ | FCoFix _ | FCaseT _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _ @@ -960,14 +964,14 @@ let rec knr info m stk = (* Computes the weak head normal form of a term *) -and kni info m stk = +and kni info tab m stk = let (hm,s) = knh info m stk in - knr info hm s -and knit info e t stk = + knr info tab hm s +and knit info tab e t stk = let (ht,s) = knht info e t stk in - knr info ht s + knr info tab ht s -let kh info v stk = fapp_stack(kni info v stk) +let kh info tab v stk = fapp_stack(kni info tab v stk) (************************************************************************) @@ -995,61 +999,61 @@ let rec zip_term zfun m stk = 1- Calls kni 2- tries to rebuild the term. If a closure still has to be computed, calls itself recursively. *) -let rec kl info m = +let rec kl info tab m = if is_val m then (incr prune; term_of_fconstr m) else - let (nm,s) = kni info m [] in + let (nm,s) = kni info tab m [] in let () = if !share then ignore (fapp_stack (nm, s)) in (* to unlock Zupdates! *) - zip_term (kl info) (norm_head info nm) s + zip_term (kl info tab) (norm_head info tab nm) s (* no redex: go up for atoms and already normalized terms, go down otherwise. *) -and norm_head info m = +and norm_head info tab m = if is_val m then (incr prune; term_of_fconstr m) else match m.term with | FLambda(n,tys,f,e) -> let (e',rvtys) = List.fold_left (fun (e,ctxt) (na,ty) -> - (subs_lift e, (na,kl info (mk_clos e ty))::ctxt)) + (subs_lift e, (na,kl info tab (mk_clos e ty))::ctxt)) (e,[]) tys in - let bd = kl info (mk_clos e' f) in + let bd = kl info tab (mk_clos e' f) in List.fold_left (fun b (na,ty) -> mkLambda(na,ty,b)) bd rvtys | FLetIn(na,a,b,f,e) -> let c = mk_clos (subs_lift e) f in - mkLetIn(na, kl info a, kl info b, kl info c) + mkLetIn(na, kl info tab a, kl info tab b, kl info tab c) | FProd(na,dom,rng) -> - mkProd(na, kl info dom, kl info rng) + mkProd(na, kl info tab dom, kl info tab rng) | FCoFix((n,(na,tys,bds)),e) -> let ftys = CArray.Fun1.map mk_clos e tys in let fbds = CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in - mkCoFix(n,(na, CArray.Fun1.map kl info ftys, CArray.Fun1.map kl info fbds)) + mkCoFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds)) | FFix((n,(na,tys,bds)),e) -> let ftys = CArray.Fun1.map mk_clos e tys in let fbds = CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in - mkFix(n,(na, CArray.Fun1.map kl info ftys, CArray.Fun1.map kl info fbds)) + mkFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds)) | FEvar((i,args),env) -> - mkEvar(i, Array.map (fun a -> kl info (mk_clos env a)) args) + mkEvar(i, Array.map (fun a -> kl info tab (mk_clos env a)) args) | FProj (p,c) -> - mkProj (p, kl info c) + mkProj (p, kl info tab c) | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FConstruct _ | FApp _ | FCaseT _ | FLIFT _ | FCLOS _ -> term_of_fconstr m (* Initialization and then normalization *) (* weak reduction *) -let whd_val info v = - with_stats (lazy (term_of_fconstr (kh info v []))) +let whd_val info tab v = + with_stats (lazy (term_of_fconstr (kh info tab v []))) (* strong reduction *) -let norm_val info v = - with_stats (lazy (kl info v)) +let norm_val info tab v = + with_stats (lazy (kl info tab v)) let inject c = mk_clos (subs_id 0) c -let whd_stack infos m stk = - let k = kni infos m stk in +let whd_stack infos tab m stk = + let k = kni infos tab m stk in let () = if !share then ignore (fapp_stack k) in (* to unlock Zupdates! *) k @@ -1057,7 +1061,10 @@ let whd_stack infos m stk = type clos_infos = fconstr infos let create_clos_infos ?(evars=fun _ -> None) flgs env = - create (fun _ -> inject) flgs env evars + create (fun _ _ c -> inject c) flgs env evars + +let create_tab () = KeyTable.create 17 + let oracle_of_infos infos = Environ.oracle infos.i_cache.i_env let env_of_infos infos = infos.i_cache.i_env @@ -1065,14 +1072,14 @@ let env_of_infos infos = infos.i_cache.i_env let infos_with_reds infos reds = { infos with i_flags = reds } -let unfold_reference info key = +let unfold_reference info tab key = match key with | ConstKey (kn,_) -> if red_set info.i_flags (fCONST kn) then - ref_value_cache info key + ref_value_cache info tab key else None | VarKey i -> if red_set info.i_flags (fVAR i) then - ref_value_cache info key + ref_value_cache info tab key else None - | _ -> ref_value_cache info key + | _ -> ref_value_cache info tab key diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index c43fc46239..3a7f77d521 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 @@ -98,13 +100,15 @@ val unfold_red : evaluable_global_reference -> reds type table_key = Constant.t Univ.puniverses tableKey type 'a infos_cache +type 'a infos_tab type 'a infos = { i_flags : reds; i_cache : 'a infos_cache } -val ref_value_cache: 'a infos -> table_key -> 'a option -val create: ('a infos -> constr -> 'a) -> reds -> env -> +val ref_value_cache: 'a infos -> 'a infos_tab -> table_key -> 'a option +val create: ('a infos -> 'a infos_tab -> constr -> 'a) -> reds -> env -> (existential -> constr option) -> 'a infos +val create_tab : unit -> 'a infos_tab val evar_value : 'a infos_cache -> existential -> constr option val info_env : 'a infos -> env @@ -198,15 +202,15 @@ val infos_with_reds : clos_infos -> reds -> clos_infos (** Reduction function *) (** [norm_val] is for strong normalization *) -val norm_val : clos_infos -> fconstr -> constr +val norm_val : clos_infos -> fconstr infos_tab -> fconstr -> constr (** [whd_val] is for weak head normalization *) -val whd_val : clos_infos -> fconstr -> constr +val whd_val : clos_infos -> fconstr infos_tab -> fconstr -> constr (** [whd_stack] performs weak head normalization in a given stack. It stops whenever a reduction is blocked. *) val whd_stack : - clos_infos -> fconstr -> stack -> fconstr * stack + clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack (** [eta_expand_ind_stack env ind c s t] computes stacks correspoding to the conversion of the eta expansion of t, considered as an inhabitant @@ -214,7 +218,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 -> @@ -223,7 +227,7 @@ val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> (** Conversion auxiliary functions to do step by step normalisation *) (** [unfold_reference] unfolds references in a [fconstr] *) -val unfold_reference : clos_infos -> table_key -> fconstr option +val unfold_reference : clos_infos -> fconstr infos_tab -> table_key -> fconstr option val eq_table_key : table_key -> table_key -> bool @@ -239,9 +243,9 @@ val mk_clos_deep : (fconstr subs -> constr -> fconstr) -> fconstr subs -> constr -> fconstr -val kni: clos_infos -> fconstr -> stack -> fconstr * stack -val knr: clos_infos -> fconstr -> stack -> fconstr * stack -val kl : clos_infos -> fconstr -> constr +val kni: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack +val knr: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack +val kl : clos_infos -> fconstr infos_tab -> fconstr -> constr val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr 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 9febc6449b..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,19 +34,64 @@ 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 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_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 +| Const_proj _, _ -> false +| Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2 +| Const_b0 _, _ -> false +| Const_bn (t1, a1), Const_bn (t2, a2) -> + Int.equal t1 t2 && CArray.equal eq_structured_constant a1 a2 +| Const_bn _, _ -> false +| Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2 +| Const_univ_level _ , _ -> false + +let rec hash_structured_constant c = + let open Hashset.Combine in + match c with + | 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) + | Const_bn (t, a) -> + let fold h c = combine h (hash_structured_constant c) in + let h = Array.fold_left fold 0 a in + combinesmall 5 (combine (Int.hash t) h) + | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l) + +let eq_annot_switch asw1 asw2 = + let eq_ci ci1 ci2 = + eq_ind ci1.ci_ind ci2.ci_ind && + Int.equal ci1.ci_npar ci2.ci_npar && + CArray.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls + in + let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in + eq_ci asw1.ci asw2.ci && + CArray.equal eq_rlc asw1.rtbl asw2.rtbl && + (asw1.tailcall : bool) == asw2.tailcall + +let hash_annot_switch asw = + let open Hashset.Combine in + let h1 = Constr.case_info_hash asw.ci in + let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in + let h3 = if asw.tailcall then 1 else 0 in + combine3 h1 h2 h3 + module Label = struct type t = int @@ -135,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 @@ -149,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 @@ -187,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 @@ -208,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 @@ -301,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 5d37a5840b..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 @@ -41,6 +42,12 @@ type reloc_table = (tag * int) array type annot_switch = {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} +val eq_structured_constant : structured_constant -> structured_constant -> bool +val hash_structured_constant : structured_constant -> int + +val eq_annot_switch : annot_switch -> annot_switch -> bool +val hash_annot_switch : annot_switch -> int + module Label : sig type t = int @@ -132,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 @@ -165,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 5dab2932d7..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,112 +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 - let levels = Universe.levels u in - let global_levels = - LSet.filter (fun x -> Level.var_index x = None) levels - in - let local_levels = - List.map_filter (fun x -> Level.var_index x) - (LSet.elements levels) - in + 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 uglob = - LSet.fold (fun lvl u -> Universe.sup u (Universe.make lvl)) global_levels Universe.type0m + let compile_get_univ reloc idx sz cont = + set_max_stack_size sz; + compile_fv_elem reloc (FVuniv_var idx) sz cont in - if local_levels = [] then - compile_str_cst reloc (Bstrconst (Const_sorts (Sorts.Type uglob))) sz cont + if List.is_empty s then + 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 local_levels) 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; @@ -709,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 *) @@ -718,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; @@ -744,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 @@ -781,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 @@ -812,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 @@ -839,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 @@ -880,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 @@ -937,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)]; @@ -978,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 @@ -1001,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 = @@ -1097,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 eeea19c12b..14f4f27c09 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -1,27 +1,62 @@ (************************************************************************) -(* 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 machine, Oct 2004 *) (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *) +open Names open Term open Cbytecodes open Copcodes open Mod_subst +type emitcodes = String.t + +external tcode_of_code : Bytes.t -> int -> Vmvalues.tcode = "coq_tcode_of_code" + (* Relocation information *) type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant | Reloc_getglobal of Names.Constant.t -type patch = reloc_info * int +let eq_reloc_info r1 r2 = match r1, r2 with +| Reloc_annot sw1, Reloc_annot sw2 -> eq_annot_switch sw1 sw2 +| Reloc_annot _, _ -> false +| Reloc_const c1, Reloc_const c2 -> eq_structured_constant c1 c2 +| Reloc_const _, _ -> false +| Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.equal c1 c2 +| Reloc_getglobal _, _ -> false + +let hash_reloc_info r = + let open Hashset.Combine in + match r with + | Reloc_annot sw -> combinesmall 1 (hash_annot_switch sw) + | Reloc_const c -> combinesmall 2 (hash_structured_constant c) + | Reloc_getglobal c -> combinesmall 3 (Constant.hash c) + +module RelocTable = Hashtbl.Make(struct + type t = reloc_info + let equal = eq_reloc_info + let hash = hash_reloc_info +end) + +(** We use arrays for on-disk representation. On 32-bit machines, this means we + can only have a maximum amount of about 4.10^6 relocations, which seems + quite a lot, but potentially reachable if e.g. compiling big proofs. This + would prevent VM computing with these terms on 32-bit architectures. Maybe + we should use a more robust data structure? *) +type patches = { + reloc_infos : (reloc_info * int array) array; +} let patch_char4 buff pos c1 c2 c3 c4 = Bytes.unsafe_set buff pos c1; @@ -29,40 +64,48 @@ let patch_char4 buff pos c1 c2 c3 c4 = Bytes.unsafe_set buff (pos + 2) c3; Bytes.unsafe_set buff (pos + 3) c4 -let patch buff (pos, n) = +let patch1 buff pos n = patch_char4 buff pos (Char.unsafe_chr n) (Char.unsafe_chr (n asr 8)) (Char.unsafe_chr (n asr 16)) (Char.unsafe_chr (n asr 24)) -(* val patch_int : emitcodes -> ((\*pos*\)int * int) list -> emitcodes *) -let patch_int buff patches = +let patch_int buff reloc = (* copy code *before* patching because of nested evaluations: the code we are patching might be called (and thus "concurrently" patched) and results in wrong results. Side-effects... *) let buff = Bytes.of_string buff in - let () = List.iter (fun p -> patch buff p) patches in - (* Note: we follow the apporach suggested by Gabriel Scherer in - PR#136 here, and use unsafe as we own buff. + let iter (reloc, npos) = Array.iter (fun pos -> patch1 buff pos reloc) npos in + let () = CArray.iter iter reloc in + buff - The crux of the question that avoids defining emitcodes just as a - Byte.t is the call to hcons in to_memory below. Even if disabling - this optimization has no visible time impact, test data shows - that the optimization is indeed triggered quite often so we - choose ugliness over altering the semantics. - - Handle with care. - *) - Bytes.unsafe_to_string buff +let patch buff pl f = + (** Order seems important here? *) + let reloc = CArray.map (fun (r, pos) -> (f r, pos)) pl.reloc_infos in + let buff = patch_int buff reloc in + tcode_of_code buff (Bytes.length buff) (* Buffering of bytecode *) -let out_buffer = ref(Bytes.create 1024) -and out_position = ref 0 +type label_definition = + Label_defined of int + | Label_undefined of (int * int) list -let out_word b1 b2 b3 b4 = - let p = !out_position in - if p >= Bytes.length !out_buffer then begin - let len = Bytes.length !out_buffer in +type env = { + mutable out_buffer : Bytes.t; + mutable out_position : int; + mutable label_table : label_definition array; + (* le ieme element de la table = Label_defined n signifie que l'on a + deja rencontrer le label i et qu'il est a l'offset n. + = Label_undefined l signifie que l'on a + pas encore rencontrer ce label, le premier entier indique ou est l'entier + a patcher dans la string, le deuxieme son origine *) + reloc_info : int list RelocTable.t; +} + +let out_word env b1 b2 b3 b4 = + let p = env.out_position in + if p >= Bytes.length env.out_buffer then begin + let len = Bytes.length env.out_buffer in let new_len = if len <= Sys.max_string_length / 2 then 2 * len @@ -71,280 +114,264 @@ let out_word b1 b2 b3 b4 = then invalid_arg "String.create" (* Pas la bonne exception .... *) else Sys.max_string_length in let new_buffer = Bytes.create new_len in - Bytes.blit !out_buffer 0 new_buffer 0 len; - out_buffer := new_buffer + Bytes.blit env.out_buffer 0 new_buffer 0 len; + env.out_buffer <- new_buffer end; - patch_char4 !out_buffer p (Char.unsafe_chr b1) + patch_char4 env.out_buffer p (Char.unsafe_chr b1) (Char.unsafe_chr b2) (Char.unsafe_chr b3) (Char.unsafe_chr b4); - out_position := p + 4 + env.out_position <- p + 4 -let out opcode = - out_word opcode 0 0 0 +let out env opcode = + out_word env opcode 0 0 0 -let out_int n = - out_word n (n asr 8) (n asr 16) (n asr 24) +let out_int env n = + out_word env n (n asr 8) (n asr 16) (n asr 24) (* Handling of local labels and backpatching *) -type label_definition = - Label_defined of int - | Label_undefined of (int * int) list - -let label_table = ref ([| |] : label_definition array) -(* le ieme element de la table = Label_defined n signifie que l'on a - deja rencontrer le label i et qu'il est a l'offset n. - = Label_undefined l signifie que l'on a - pas encore rencontrer ce label, le premier entier indique ou est l'entier - a patcher dans la string, le deuxieme son origine *) - -let extend_label_table needed = - let new_size = ref(Array.length !label_table) in +let extend_label_table env needed = + let new_size = ref(Array.length env.label_table) in while needed >= !new_size do new_size := 2 * !new_size done; let new_table = Array.make !new_size (Label_undefined []) in - Array.blit !label_table 0 new_table 0 (Array.length !label_table); - label_table := new_table - -let backpatch (pos, orig) = - let displ = (!out_position - orig) asr 2 in - Bytes.set !out_buffer pos @@ Char.unsafe_chr displ; - Bytes.set !out_buffer (pos+1) @@ Char.unsafe_chr (displ asr 8); - Bytes.set !out_buffer (pos+2) @@ Char.unsafe_chr (displ asr 16); - Bytes.set !out_buffer (pos+3) @@ Char.unsafe_chr (displ asr 24) - -let define_label lbl = - if lbl >= Array.length !label_table then extend_label_table lbl; - match (!label_table).(lbl) with + Array.blit env.label_table 0 new_table 0 (Array.length env.label_table); + env.label_table <- new_table + +let backpatch env (pos, orig) = + let displ = (env.out_position - orig) asr 2 in + Bytes.set env.out_buffer pos @@ Char.unsafe_chr displ; + Bytes.set env.out_buffer (pos+1) @@ Char.unsafe_chr (displ asr 8); + Bytes.set env.out_buffer (pos+2) @@ Char.unsafe_chr (displ asr 16); + Bytes.set env.out_buffer (pos+3) @@ Char.unsafe_chr (displ asr 24) + +let define_label env lbl = + if lbl >= Array.length env.label_table then extend_label_table env lbl; + match (env.label_table).(lbl) with Label_defined _ -> raise(Failure "CEmitcode.define_label") | Label_undefined patchlist -> - List.iter backpatch patchlist; - (!label_table).(lbl) <- Label_defined !out_position + List.iter (fun p -> backpatch env p) patchlist; + (env.label_table).(lbl) <- Label_defined env.out_position -let out_label_with_orig orig lbl = - if lbl >= Array.length !label_table then extend_label_table lbl; - match (!label_table).(lbl) with +let out_label_with_orig env orig lbl = + if lbl >= Array.length env.label_table then extend_label_table env lbl; + match (env.label_table).(lbl) with Label_defined def -> - out_int((def - orig) asr 2) + out_int env ((def - orig) asr 2) | Label_undefined patchlist -> (* spiwack: patchlist is supposed to be non-empty all the time thus I commented that out. If there is no problem I suggest removing it for next release (cur: 8.1) *) (*if patchlist = [] then *) - (!label_table).(lbl) <- - Label_undefined((!out_position, orig) :: patchlist); - out_int 0 + (env.label_table).(lbl) <- + Label_undefined((env.out_position, orig) :: patchlist); + out_int env 0 -let out_label l = out_label_with_orig !out_position l +let out_label env l = out_label_with_orig env env.out_position l (* Relocation information *) -let reloc_info = ref ([] : (reloc_info * int) list) +let enter env info = + let pos = env.out_position in + let old = try RelocTable.find env.reloc_info info with Not_found -> [] in + RelocTable.replace env.reloc_info info (pos :: old) -let enter info = - reloc_info := (info, !out_position) :: !reloc_info +let slot_for_const env c = + enter env (Reloc_const c); + out_int env 0 -let slot_for_const c = - enter (Reloc_const c); - out_int 0 +let slot_for_annot env a = + enter env (Reloc_annot a); + out_int env 0 -let slot_for_annot a = - enter (Reloc_annot a); - out_int 0 - -let slot_for_getglobal p = - enter (Reloc_getglobal p); - out_int 0 +let slot_for_getglobal env p = + enter env (Reloc_getglobal p); + out_int env 0 (* Emission of one instruction *) -let emit_instr = function - | Klabel lbl -> define_label lbl +let emit_instr env = function + | Klabel lbl -> define_label env lbl | Kacc n -> - if n < 8 then out(opACC0 + n) else (out opACC; out_int n) + if n < 8 then out env(opACC0 + n) else (out env opACC; out_int env n) | Kenvacc n -> if n >= 1 && n <= 4 - then out(opENVACC1 + n - 1) - else (out opENVACC; out_int n) + then out env(opENVACC1 + n - 1) + else (out env opENVACC; out_int env n) | Koffsetclosure ofs -> if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2 - then out (opOFFSETCLOSURE0 + ofs / 2) - else (out opOFFSETCLOSURE; out_int ofs) + then out env (opOFFSETCLOSURE0 + ofs / 2) + else (out env opOFFSETCLOSURE; out_int env ofs) | Kpush -> - out opPUSH + out env opPUSH | Kpop n -> - out opPOP; out_int n + out env opPOP; out_int env n | Kpush_retaddr lbl -> - out opPUSH_RETADDR; out_label lbl + out env opPUSH_RETADDR; out_label env lbl | Kapply n -> - if n < 4 then out(opAPPLY1 + n - 1) else (out opAPPLY; out_int n) + if n < 4 then out env(opAPPLY1 + n - 1) else (out env opAPPLY; out_int env n) | Kappterm(n, sz) -> - if n < 4 then (out(opAPPTERM1 + n - 1); out_int sz) - else (out opAPPTERM; out_int n; out_int sz) + if n < 4 then (out env(opAPPTERM1 + n - 1); out_int env sz) + else (out env opAPPTERM; out_int env n; out_int env sz) | Kreturn n -> - out opRETURN; out_int n + out env opRETURN; out_int env n | Kjump -> - out opRETURN; out_int 0 + out env opRETURN; out_int env 0 | Krestart -> - out opRESTART + out env opRESTART | Kgrab n -> - out opGRAB; out_int n + out env opGRAB; out_int env n | Kgrabrec(rec_arg) -> - out opGRABREC; out_int rec_arg + out env opGRABREC; out_int env rec_arg | Kclosure(lbl, n) -> - out opCLOSURE; out_int n; out_label lbl + out env opCLOSURE; out_int env n; out_label env lbl | Kclosurerec(nfv,init,lbl_types,lbl_bodies) -> - out opCLOSUREREC;out_int (Array.length lbl_bodies); - out_int nfv; out_int init; - let org = !out_position in - Array.iter (out_label_with_orig org) lbl_types; - let org = !out_position in - Array.iter (out_label_with_orig org) lbl_bodies + out env opCLOSUREREC;out_int env (Array.length lbl_bodies); + out_int env nfv; out_int env init; + let org = env.out_position in + Array.iter (out_label_with_orig env org) lbl_types; + let org = env.out_position in + Array.iter (out_label_with_orig env org) lbl_bodies | Kclosurecofix(nfv,init,lbl_types,lbl_bodies) -> - out opCLOSURECOFIX;out_int (Array.length lbl_bodies); - out_int nfv; out_int init; - let org = !out_position in - Array.iter (out_label_with_orig org) lbl_types; - let org = !out_position in - Array.iter (out_label_with_orig org) lbl_bodies + out env opCLOSURECOFIX;out_int env (Array.length lbl_bodies); + out_int env nfv; out_int env init; + let org = env.out_position in + Array.iter (out_label_with_orig env org) lbl_types; + let org = env.out_position in + Array.iter (out_label_with_orig env org) lbl_bodies | Kgetglobal q -> - out opGETGLOBAL; slot_for_getglobal q + out env opGETGLOBAL; slot_for_getglobal env q | Kconst (Const_b0 i) -> if i >= 0 && i <= 3 - then out (opCONST0 + i) - else (out opCONSTINT; out_int i) + then out env (opCONST0 + i) + else (out env opCONSTINT; out_int env i) | Kconst c -> - out opGETGLOBAL; slot_for_const c + out env opGETGLOBAL; slot_for_const env c | Kmakeblock(n, t) -> if Int.equal n 0 then invalid_arg "emit_instr : block size = 0" - else if n < 4 then (out(opMAKEBLOCK1 + n - 1); out_int t) - else (out opMAKEBLOCK; out_int n; out_int t) + else if n < 4 then (out env(opMAKEBLOCK1 + n - 1); out_int env t) + else (out env opMAKEBLOCK; out_int env n; out_int env t) | Kmakeprod -> - out opMAKEPROD + out env opMAKEPROD | Kmakeswitchblock(typlbl,swlbl,annot,sz) -> - out opMAKESWITCHBLOCK; - out_label typlbl; out_label swlbl; - slot_for_annot annot;out_int sz + out env opMAKESWITCHBLOCK; + out_label env typlbl; out_label env swlbl; + slot_for_annot env annot;out_int env sz | Kswitch (tbl_const, tbl_block) -> let lenb = Array.length tbl_block in let lenc = Array.length tbl_const in assert (lenb < 0x100 && lenc < 0x1000000); - out opSWITCH; - out_word lenc (lenc asr 8) (lenc asr 16) (lenb); -(* out_int (Array.length tbl_const + (Array.length tbl_block lsl 23)); *) - let org = !out_position in - Array.iter (out_label_with_orig org) tbl_const; - Array.iter (out_label_with_orig org) tbl_block + out env opSWITCH; + out_word env lenc (lenc asr 8) (lenc asr 16) (lenb); +(* out_int env (Array.length tbl_const + (Array.length tbl_block lsl 23)); *) + let org = env.out_position in + Array.iter (out_label_with_orig env org) tbl_const; + Array.iter (out_label_with_orig env org) tbl_block | Kpushfields n -> - out opPUSHFIELDS;out_int n + out env opPUSHFIELDS;out_int env n | Kfield n -> - if n <= 1 then out (opGETFIELD0+n) - else (out opGETFIELD;out_int n) + if n <= 1 then out env (opGETFIELD0+n) + else (out env opGETFIELD;out_int env n) | Ksetfield n -> - if n <= 1 then out (opSETFIELD0+n) - else (out opSETFIELD;out_int n) + if n <= 1 then out env (opSETFIELD0+n) + else (out env opSETFIELD;out_int env n) | Ksequence _ -> invalid_arg "Cemitcodes.emit_instr" - | Kproj (n,p) -> out opPROJ; out_int n; slot_for_const (Const_proj p) - | Kensurestackcapacity size -> out opENSURESTACKCAPACITY; out_int size + | Kproj (n,p) -> out env opPROJ; out_int env n; slot_for_const env (Const_proj p) + | Kensurestackcapacity size -> out env opENSURESTACKCAPACITY; out_int env size (* spiwack *) - | Kbranch lbl -> out opBRANCH; out_label lbl - | Kaddint31 -> out opADDINT31 - | Kaddcint31 -> out opADDCINT31 - | Kaddcarrycint31 -> out opADDCARRYCINT31 - | Ksubint31 -> out opSUBINT31 - | Ksubcint31 -> out opSUBCINT31 - | Ksubcarrycint31 -> out opSUBCARRYCINT31 - | Kmulint31 -> out opMULINT31 - | Kmulcint31 -> out opMULCINT31 - | Kdiv21int31 -> out opDIV21INT31 - | Kdivint31 -> out opDIVINT31 - | Kaddmuldivint31 -> out opADDMULDIVINT31 - | Kcompareint31 -> out opCOMPAREINT31 - | Khead0int31 -> out opHEAD0INT31 - | Ktail0int31 -> out opTAIL0INT31 - | Kisconst lbl -> out opISCONST; out_label lbl - | Kareconst(n,lbl) -> out opARECONST; out_int n; out_label lbl - | Kcompint31 -> out opCOMPINT31 - | Kdecompint31 -> out opDECOMPINT31 - | Klorint31 -> out opORINT31 - | Klandint31 -> out opANDINT31 - | Klxorint31 -> out opXORINT31 + | Kbranch lbl -> out env opBRANCH; out_label env lbl + | Kaddint31 -> out env opADDINT31 + | Kaddcint31 -> out env opADDCINT31 + | Kaddcarrycint31 -> out env opADDCARRYCINT31 + | Ksubint31 -> out env opSUBINT31 + | Ksubcint31 -> out env opSUBCINT31 + | Ksubcarrycint31 -> out env opSUBCARRYCINT31 + | Kmulint31 -> out env opMULINT31 + | Kmulcint31 -> out env opMULCINT31 + | Kdiv21int31 -> out env opDIV21INT31 + | Kdivint31 -> out env opDIVINT31 + | Kaddmuldivint31 -> out env opADDMULDIVINT31 + | Kcompareint31 -> out env opCOMPAREINT31 + | Khead0int31 -> out env opHEAD0INT31 + | Ktail0int31 -> out env opTAIL0INT31 + | Kisconst lbl -> out env opISCONST; out_label env lbl + | Kareconst(n,lbl) -> out env opARECONST; out_int env n; out_label env lbl + | Kcompint31 -> out env opCOMPINT31 + | Kdecompint31 -> out env opDECOMPINT31 + | Klorint31 -> out env opORINT31 + | Klandint31 -> out env opANDINT31 + | Klxorint31 -> out env opXORINT31 (*/spiwack *) | Kstop -> - out opSTOP + out env opSTOP (* Emission of a current list and remaining lists of instructions. Include some peephole optimization. *) -let rec emit insns remaining = match insns with +let rec emit env insns remaining = match insns with | [] -> (match remaining with [] -> () - | (first::rest) -> emit first rest) + | (first::rest) -> emit env first rest) (* Peephole optimizations *) | Kpush :: Kacc n :: c -> - if n < 8 then out(opPUSHACC0 + n) else (out opPUSHACC; out_int n); - emit c remaining + if n < 8 then out env(opPUSHACC0 + n) else (out env opPUSHACC; out_int env n); + emit env c remaining | Kpush :: Kenvacc n :: c -> if n >= 1 && n <= 4 - then out(opPUSHENVACC1 + n - 1) - else (out opPUSHENVACC; out_int n); - emit c remaining + then out env(opPUSHENVACC1 + n - 1) + else (out env opPUSHENVACC; out_int env n); + emit env c remaining | Kpush :: Koffsetclosure ofs :: c -> if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2 - then out(opPUSHOFFSETCLOSURE0 + ofs / 2) - else (out opPUSHOFFSETCLOSURE; out_int ofs); - emit c remaining + then out env(opPUSHOFFSETCLOSURE0 + ofs / 2) + else (out env opPUSHOFFSETCLOSURE; out_int env ofs); + emit env c remaining | Kpush :: Kgetglobal id :: c -> - out opPUSHGETGLOBAL; slot_for_getglobal id; emit c remaining + out env opPUSHGETGLOBAL; slot_for_getglobal env id; emit env c remaining | Kpush :: Kconst (Const_b0 i) :: c -> if i >= 0 && i <= 3 - then out (opPUSHCONST0 + i) - else (out opPUSHCONSTINT; out_int i); - emit c remaining + then out env (opPUSHCONST0 + i) + else (out env opPUSHCONSTINT; out_int env i); + emit env c remaining | Kpush :: Kconst const :: c -> - out opPUSHGETGLOBAL; slot_for_const const; - emit c remaining + out env opPUSHGETGLOBAL; slot_for_const env const; + emit env c remaining | Kpop n :: Kjump :: c -> - out opRETURN; out_int n; emit c remaining + out env opRETURN; out_int env n; emit env c remaining | Ksequence(c1,c2)::c -> - emit c1 (c2::c::remaining) + emit env c1 (c2::c::remaining) (* Default case *) | instr :: c -> - emit_instr instr; emit c remaining + emit_instr env instr; emit env c remaining (* Initialization *) -let init () = - out_position := 0; - label_table := Array.make 16 (Label_undefined []); - reloc_info := [] - -type emitcodes = String.t - -let length = String.length - -type to_patch = emitcodes * (patch list) * fv +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) -let subst_patch s (ri,pos) = +let subst_reloc s ri = match ri with | Reloc_annot a -> let (kn,i) = a.ci.ci_ind in let ci = {a.ci with ci_ind = (subst_mind s kn,i)} in - (Reloc_annot {a with ci = ci},pos) - | Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos) - | Reloc_getglobal kn -> (Reloc_getglobal (subst_constant s kn), pos) + Reloc_annot {a with ci = ci} + | Reloc_const sc -> Reloc_const (subst_strcst s sc) + | Reloc_getglobal kn -> Reloc_getglobal (subst_constant s kn) + +let subst_patches subst p = + let infos = CArray.map (fun (r, pos) -> (subst_reloc subst r, pos)) p.reloc_infos in + { reloc_infos = infos; } let subst_to_patch s (code,pl,fv) = - code,List.rev_map (subst_patch s) pl,fv + code, subst_patches s pl, fv type body_code = | BCdefined of to_patch @@ -381,16 +408,23 @@ let repr_body_code = function | PBCconstant -> (None, BCconstant) let to_memory (init_code, fun_code, fv) = - init(); - emit init_code []; - emit fun_code []; + let env = { + out_buffer = Bytes.create 1024; + out_position = 0; + label_table = Array.make 16 (Label_undefined []); + reloc_info = RelocTable.create 91; + } in + emit env init_code []; + emit env fun_code []; (** Later uses of this string are all purely functional *) - let code = Bytes.sub_string !out_buffer 0 !out_position in + let code = Bytes.sub_string env.out_buffer 0 env.out_position in let code = CString.hcons code in - let reloc = List.rev !reloc_info in + let fold reloc npos accu = (reloc, Array.of_list npos) :: accu in + let reloc = RelocTable.fold fold env.reloc_info [] in + let reloc = { reloc_infos = CArray.of_list reloc } in Array.iter (fun lbl -> (match lbl with Label_defined _ -> assert true | Label_undefined patchlist -> - assert (patchlist = []))) !label_table; + assert (patchlist = []))) env.label_table; (code, reloc, fv) diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index fee45aafd8..03920dc1a3 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -6,20 +6,12 @@ type reloc_info = | Reloc_const of structured_constant | Reloc_getglobal of Constant.t -type patch = reloc_info * int - -(* A virer *) -val subst_patch : Mod_subst.substitution -> patch -> patch - +type patches type emitcodes -val length : emitcodes -> int - -val patch_int : emitcodes -> ((*pos*)int * int) list -> emitcodes - -type to_patch = emitcodes * (patch list) * fv +val patch : emitcodes -> patches -> (reloc_info -> int) -> Vmvalues.tcode -val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch +type to_patch = emitcodes * patches * fv type body_code = | BCdefined of to_patch 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..ba7fecadf8 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 *) @@ -652,6 +654,11 @@ let map_with_binders g f l c0 = match kind c0 with let bl' = CArray.Fun1.smartmap f l' bl in mkCoFix (ln,(lna,tl',bl')) +type instance_compare_fn = global_reference -> int -> + Univ.Instance.t -> Univ.Instance.t -> bool + +type constr_compare_fn = int -> constr -> constr -> bool + (* [compare_head_gen_evar k1 k2 u s e eq leq c1 c2] compare [c1] and [c2] (using [k1] to expose the structure of [c1] and [k2] to expose the structure [c2]) using [eq] to compare the immediate subterms of @@ -663,38 +670,42 @@ let map_with_binders g f l c0 = match kind c0 with optimisation that physically equal arrays are equals (hence the calls to {!Array.equal_norefl}). *) -let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 = +let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t1 t2 = match kind1 t1, kind2 t2 with | Rel n1, Rel n2 -> Int.equal n1 n2 | Meta m1, Meta m2 -> Int.equal m1 m2 | Var id1, Var id2 -> Id.equal id1 id2 | Sort s1, Sort s2 -> leq_sorts s1 s2 - | Cast (c1,_,_), _ -> leq c1 t2 - | _, Cast (c2,_,_) -> leq t1 c2 - | Prod (_,t1,c1), Prod (_,t2,c2) -> eq t1 t2 && leq c1 c2 - | Lambda (_,t1,c1), Lambda (_,t2,c2) -> eq t1 t2 && eq c1 c2 - | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> eq b1 b2 && eq t1 t2 && leq c1 c2 + | Cast (c1, _, _), _ -> leq nargs c1 t2 + | _, Cast (c2, _, _) -> leq nargs t1 c2 + | Prod (_,t1,c1), Prod (_,t2,c2) -> eq 0 t1 t2 && leq 0 c1 c2 + | Lambda (_,t1,c1), Lambda (_,t2,c2) -> eq 0 t1 t2 && eq 0 c1 c2 + | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> eq 0 b1 b2 && eq 0 t1 t2 && leq nargs c1 c2 (* Why do we suddenly make a special case for Cast here? *) - | App (Cast(c1, _, _),l1), _ -> leq (mkApp (c1,l1)) t2 - | _, App (Cast (c2, _, _),l2) -> leq t1 (mkApp (c2,l2)) - | App (c1,l1), App (c2,l2) -> - Int.equal (Array.length l1) (Array.length l2) && - eq c1 c2 && Array.equal_norefl eq l1 l2 - | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq c1 c2 - | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal eq l1 l2 - | Const (c1,u1), Const (c2,u2) -> Constant.equal c1 c2 && eq_universes true u1 u2 - | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && eq_universes false u1 u2 - | Construct (c1,u1), Construct (c2,u2) -> eq_constructor c1 c2 && eq_universes false u1 u2 + | App (Cast (c1, _, _), l1), _ -> leq nargs (mkApp (c1, l1)) t2 + | _, App (Cast (c2, _, _), l2) -> leq nargs t1 (mkApp (c2, l2)) + | App (c1, l1), App (c2, l2) -> + let len = Array.length l1 in + Int.equal len (Array.length l2) && + eq (nargs+len) c1 c2 && Array.equal_norefl (eq 0) l1 l2 + | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq 0 c1 c2 + | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal (eq 0) l1 l2 + | Const (c1,u1), Const (c2,u2) -> + (* The args length currently isn't used but may as well pass it. *) + Constant.equal c1 c2 && leq_universes (ConstRef c1) nargs u1 u2 + | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (IndRef c1) nargs u1 u2 + | Construct (c1,u1), Construct (c2,u2) -> + eq_constructor c1 c2 && leq_universes (ConstructRef c1) nargs u1 u2 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> - eq p1 p2 && eq c1 c2 && Array.equal eq bl1 bl2 + eq 0 p1 p2 && eq 0 c1 c2 && Array.equal (eq 0) bl1 bl2 | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) -> - Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 - && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2 + Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 + && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2 | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> - Int.equal ln1 ln2 && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2 + Int.equal ln1 ln2 && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2 | (Rel _ | Meta _ | Var _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _ - | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ | Fix _ - | CoFix _), _ -> false + | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ | Fix _ + | CoFix _), _ -> false (* [compare_head_gen_leq u s eq leq c1 c2] compare [c1] and [c2] using [eq] to compare the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity, @@ -702,8 +713,8 @@ let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 = application associativity, binders name and Cases annotations are not taken into account *) -let compare_head_gen_leq eq_universes leq_sorts eq leq t1 t2 = - compare_head_gen_leq_with kind kind eq_universes leq_sorts eq leq t1 t2 +let compare_head_gen_leq leq_universes leq_sorts eq leq t1 t2 = + compare_head_gen_leq_with kind kind leq_universes leq_sorts eq leq t1 t2 (* [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] if needed, [u] to @@ -720,7 +731,7 @@ let compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq t1 t2 = let compare_head_gen eq_universes eq_sorts eq t1 t2 = compare_head_gen_leq eq_universes eq_sorts eq eq t1 t2 -let compare_head = compare_head_gen (fun _ -> Univ.Instance.equal) Sorts.equal +let compare_head = compare_head_gen (fun _ _ -> Univ.Instance.equal) Sorts.equal (*******************************) (* alpha conversion functions *) @@ -728,41 +739,41 @@ let compare_head = compare_head_gen (fun _ -> Univ.Instance.equal) Sorts.equal (* alpha conversion : ignore print names and casts *) -let rec eq_constr m n = - (m == n) || compare_head_gen (fun _ -> Instance.equal) Sorts.equal eq_constr m n +let rec eq_constr nargs m n = + (m == n) || compare_head_gen (fun _ _ -> Instance.equal) Sorts.equal eq_constr nargs m n -let equal m n = eq_constr m n (* to avoid tracing a recursive fun *) +let equal n m = eq_constr 0 m n (* to avoid tracing a recursive fun *) let eq_constr_univs univs m n = if m == n then true else - let eq_universes _ = UGraph.check_eq_instances univs in + let eq_universes _ _ = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = s1 == s2 || UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in - let rec eq_constr' m n = - m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n - in compare_head_gen eq_universes eq_sorts eq_constr' m n + let rec eq_constr' nargs m n = + m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n + in compare_head_gen eq_universes eq_sorts eq_constr' 0 m n let leq_constr_univs univs m n = if m == n then true else - let eq_universes _ = UGraph.check_eq_instances univs in + let eq_universes _ _ = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = s1 == s2 || UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in let leq_sorts s1 s2 = s1 == s2 || UGraph.check_leq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in - let rec eq_constr' m n = - m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n + let rec eq_constr' nargs m n = + m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n in - let rec compare_leq m n = - compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n - and leq_constr' m n = m == n || compare_leq m n in - compare_leq m n + let rec compare_leq nargs m n = + compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' nargs m n + and leq_constr' nargs m n = m == n || compare_leq nargs m n in + compare_leq 0 m n let eq_constr_univs_infer univs m n = if m == n then true, Constraint.empty else let cstrs = ref Constraint.empty in - let eq_universes strict = UGraph.check_eq_instances univs in + let eq_universes _ _ = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else @@ -772,17 +783,17 @@ let eq_constr_univs_infer univs m n = (cstrs := Univ.enforce_eq u1 u2 !cstrs; true) in - let rec eq_constr' m n = - m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n + let rec eq_constr' nargs m n = + m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n in - let res = compare_head_gen eq_universes eq_sorts eq_constr' m n in + let res = compare_head_gen eq_universes eq_sorts eq_constr' 0 m n in res, !cstrs let leq_constr_univs_infer univs m n = if m == n then true, Constraint.empty else let cstrs = ref Constraint.empty in - let eq_universes strict l l' = UGraph.check_eq_instances univs l l' in + let eq_universes _ _ l l' = UGraph.check_eq_instances univs l l' in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else @@ -800,19 +811,17 @@ let leq_constr_univs_infer univs m n = (cstrs := Univ.enforce_leq u1 u2 !cstrs; true) in - let rec eq_constr' m n = - m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n + let rec eq_constr' nargs m n = + m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n in - let rec compare_leq m n = - compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n - and leq_constr' m n = m == n || compare_leq m n in - let res = compare_leq m n in + let rec compare_leq nargs m n = + compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' nargs m n + and leq_constr' nargs m n = m == n || compare_leq nargs m n in + let res = compare_leq 0 m n in res, !cstrs -let always_true _ _ = true - let rec eq_constr_nounivs m n = - (m == n) || compare_head_gen (fun _ -> always_true) always_true eq_constr_nounivs m n + (m == n) || compare_head_gen (fun _ _ _ _ -> true) (fun _ _ -> true) (fun _ -> eq_constr_nounivs) 0 m n let constr_ord_int f t1 t2 = let (=?) f g i1 i2 j1 j2= diff --git a/kernel/constr.mli b/kernel/constr.mli index 19ffa8fe30..98c0eaa28d 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, @@ -400,31 +402,38 @@ val iter : (constr -> unit) -> constr -> unit val iter_with_binders : ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit +type constr_compare_fn = int -> constr -> constr -> bool + (** [compare_head f c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] if needed; Cast's, binders name and Cases annotations are not taken into account *) -val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool +val compare_head : constr_compare_fn -> constr_compare_fn + +(** Convert a global reference applied to 2 instances. The int says + how many arguments are given (as we can only use cumulativity for + fully applied inductives/constructors) .*) +type instance_compare_fn = global_reference -> int -> + Univ.Instance.t -> Univ.Instance.t -> bool -(** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare - the immediate subterms of [c1] of [c2] if needed, [u] to compare universe - instances (the first boolean tells if they belong to a Constant.t), [s] to - compare sorts; Cast's, binders name and Cases annotations are not taken - into account *) +(** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to + compare the immediate subterms of [c1] of [c2] if needed, [u] to + compare universe instances, [s] to compare sorts; Cast's, binders + name and Cases annotations are not taken into account *) -val compare_head_gen : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> +val compare_head_gen : instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> - (constr -> constr -> bool) -> - constr -> constr -> bool + constr_compare_fn -> + constr_compare_fn val compare_head_gen_leq_with : (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> + instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> - (constr -> constr -> bool) -> - (constr -> constr -> bool) -> - constr -> constr -> bool + constr_compare_fn -> + constr_compare_fn -> + constr_compare_fn (** [compare_head_gen_with k1 k2 u s f c1 c2] compares [c1] and [c2] like [compare_head_gen u s f c1 c2], except that [k1] (resp. [k2]) @@ -433,10 +442,10 @@ val compare_head_gen_leq_with : val compare_head_gen_with : (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> + instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> - (constr -> constr -> bool) -> - constr -> constr -> bool + constr_compare_fn -> + constr_compare_fn (** [compare_head_gen_leq u s f fle c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] for @@ -445,11 +454,11 @@ val compare_head_gen_with : [s] to compare sorts for for subtyping; Cast's, binders name and Cases annotations are not taken into account *) -val compare_head_gen_leq : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> +val compare_head_gen_leq : instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> - (constr -> constr -> bool) -> - (constr -> constr -> bool) -> - constr -> constr -> bool + constr_compare_fn -> + constr_compare_fn -> + constr_compare_fn (** {6 Hashconsing} *) 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 2bbb867cd4..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 @@ -14,7 +16,6 @@ open Util open Names -open Constr open Vmvalues open Cemitcodes open Cbytecodes @@ -25,7 +26,6 @@ open Cbytegen module NamedDecl = Context.Named.Declaration module RelDecl = Context.Rel.Declaration -external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code" external eval_tcode : tcode -> values array -> values = "coq_eval_tcode" (*******************) @@ -56,61 +56,12 @@ let set_global v = (* table pour les structured_constant et les annotations des switchs *) -let rec eq_structured_constant c1 c2 = match c1, c2 with -| Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2 -| Const_sorts _, _ -> false -| Const_ind i1, Const_ind i2 -> eq_ind i1 i2 -| Const_ind _, _ -> false -| Const_proj p1, Const_proj p2 -> Constant.equal p1 p2 -| Const_proj _, _ -> false -| Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2 -| Const_b0 _, _ -> false -| Const_bn (t1, a1), Const_bn (t2, a2) -> - Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2 -| Const_bn _, _ -> false -| Const_univ_level l1 , Const_univ_level l2 -> Univ.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_ind i -> combinesmall 2 (ind_hash i) - | Const_proj p -> combinesmall 3 (Constant.hash p) - | Const_b0 t -> combinesmall 4 (Int.hash t) - | Const_bn (t, a) -> - let fold h c = combine h (hash_structured_constant c) in - let h = Array.fold_left fold 0 a in - combinesmall 5 (combine (Int.hash t) h) - | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l) - | Const_type u -> combinesmall 7 (Univ.Universe.hash u) - module SConstTable = Hashtbl.Make (struct type t = structured_constant let equal = eq_structured_constant let hash = hash_structured_constant end) -let eq_annot_switch asw1 asw2 = - let eq_ci ci1 ci2 = - eq_ind ci1.ci_ind ci2.ci_ind && - Int.equal ci1.ci_npar ci2.ci_npar && - Array.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls - in - let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in - eq_ci asw1.ci asw2.ci && - Array.equal eq_rlc asw1.rtbl asw2.rtbl && - (asw1.tailcall : bool) == asw2.tailcall - -let hash_annot_switch asw = - let open Hashset.Combine in - let h1 = Constr.case_info_hash asw.ci in - let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in - let h3 = if asw.tailcall then 1 else 0 in - combine3 h1 h2 h3 - module AnnotTable = Hashtbl.Make (struct type t = annot_switch let equal = eq_annot_switch @@ -201,23 +152,22 @@ 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 and eval_to_patch env (buff,pl,fv) = - let patch = function - | Reloc_annot a, pos -> (pos, slot_for_annot a) - | Reloc_const sc, pos -> (pos, slot_for_str_cst sc) - | Reloc_getglobal kn, pos -> (pos, slot_for_getglobal env kn) + let slots = function + | Reloc_annot a -> slot_for_annot a + | Reloc_const sc -> slot_for_str_cst sc + | Reloc_getglobal kn -> slot_for_getglobal env kn in - let patches = List.map_left patch pl in - let buff = patch_int buff patches in + let tc = patch buff pl slots in let vm_env = Array.map (slot_for_fv env) fv in - let tc = tcode_of_code buff (length buff) in 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 5b9e1a1414..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 @@ -219,7 +221,7 @@ type ('ty,'a) functorize = type with_declaration = | WithMod of Id.t list * ModPath.t - | WithDef of Id.t list * constr Univ.in_universe_context + | WithDef of Id.t list * (constr * Univ.AUContext.t option) type module_alg_expr = | MEident of ModPath.t 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 b7eb481ee3..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 @@ -73,13 +75,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = any implementations of parameters and opaques terms, as long as they have the right type *) let c', univs, ctx' = - match cb.const_universes with - | Monomorphic_const _ -> - (** We do not add the deferred constraints of the body in the - environment, because they do not appear in the type of the - definition. Any inconsistency will be raised at a later stage - when joining the environment. *) - let env' = Environ.push_context ~strict:true ctx env' in + match cb.const_universes, ctx with + | Monomorphic_const _, None -> let c',cst = match cb.const_body with | Undef _ | OpaqueDef _ -> let j = Typeops.infer env' c in @@ -91,11 +88,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = let c' = Mod_subst.force_constr cs in c, Reduction.infer_conv env' (Environ.universes env') c c' in - let ctx = Univ.ContextSet.of_context ctx in - c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst ctx - | Polymorphic_const uctx -> - let inst, ctx = Univ.abstract_universes ctx in - let c = Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in + c', Monomorphic_const Univ.ContextSet.empty, cst + | Polymorphic_const uctx, Some ctx -> let () = if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then error_incorrect_with_constraint lab @@ -116,7 +110,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = in if not (Univ.Constraint.is_empty cst) then error_incorrect_with_constraint lab; - c, Polymorphic_const ctx, Univ.ContextSet.empty + c, Polymorphic_const ctx, Univ.Constraint.empty + | _ -> error_incorrect_with_constraint lab in let def = Def (Mod_subst.from_val c') in (* let ctx' = Univ.UContext.make (newus, cst) in *) @@ -225,11 +220,11 @@ let rec check_with_mod env struc (idl,mp1) mp equiv = | Reduction.NotConvertible -> error_incorrect_with_constraint lab let check_with env mp (sign,alg,reso,cst) = function - |WithDef(idl,c) -> + |WithDef(idl, (c, ctx)) -> let struc = destr_nofunctor sign in - let struc',c',cst' = check_with_def env struc (idl,c) mp reso in - let wd' = WithDef (idl,(c',Univ.ContextSet.to_context cst')) in - NoFunctor struc', MEwith (alg,wd'), reso, cst+++cst' + let struc', c', cst' = check_with_def env struc (idl, (c, ctx)) mp reso in + let wd' = WithDef (idl, (c', ctx)) in + NoFunctor struc', MEwith (alg,wd'), reso, Univ.ContextSet.add_constraints cst' cst |WithMod(idl,mp1) as wd -> let struc = destr_nofunctor sign in let struc',reso',cst' = check_with_mod env struc (idl,mp1) mp reso in 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..a3aa71f24f 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 @@ -699,6 +701,12 @@ end module Constrmap = Map.Make(ConstructorOrdered) module Constrmap_env = Map.Make(ConstructorOrdered_env) +type global_reference = + | VarRef of variable (** A reference to the section-context. *) + | ConstRef of Constant.t (** A reference to the environment. *) + | IndRef of inductive (** A reference to an inductive type. *) + | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) + (* Better to have it here that in closure, since used in grammar.cma *) type evaluable_global_reference = | EvalVarRef of Id.t diff --git a/kernel/names.mli b/kernel/names.mli index b1e8efd8d1..ffd96781b3 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 @@ -498,6 +500,13 @@ val constructor_user_hash : constructor -> int val constructor_syntactic_ord : constructor -> constructor -> int val constructor_syntactic_hash : constructor -> int +(** {6 Global reference is a kernel side type for all references together } *) +type global_reference = + | VarRef of variable (** A reference to the section-context. *) + | ConstRef of Constant.t (** A reference to the environment. *) + | IndRef of inductive (** A reference to an inductive type. *) + | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) + (** Better to have it here that in Closure, since required in grammar.cma *) type evaluable_global_reference = | EvalVarRef of Id.t 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 159d2ea665..81fbd4f5ef 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 @@ -115,12 +117,12 @@ let whd_betaiota env t = | App (c, _) -> begin match kind c with | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | LetIn _ -> t - | _ -> whd_val (create_clos_infos betaiota env) (inject t) + | _ -> whd_val (create_clos_infos betaiota env) (create_tab ()) (inject t) end - | _ -> whd_val (create_clos_infos betaiota env) (inject t) + | _ -> whd_val (create_clos_infos betaiota env) (create_tab ()) (inject t) let nf_betaiota env t = - norm_val (create_clos_infos betaiota env) (inject t) + norm_val (create_clos_infos betaiota env) (create_tab ()) (inject t) let whd_betaiotazeta env x = match kind x with @@ -131,10 +133,10 @@ let whd_betaiotazeta env x = | Ind _ | Construct _ | Evar _ | Meta _ | Const _ -> x | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _ | Case _ | Fix _ | CoFix _ | Proj _ -> - whd_val (create_clos_infos betaiotazeta env) (inject x) + whd_val (create_clos_infos betaiotazeta env) (create_tab ()) (inject x) end | Rel _ | Cast _ | LetIn _ | Case _ | Proj _ -> - whd_val (create_clos_infos betaiotazeta env) (inject x) + whd_val (create_clos_infos betaiotazeta env) (create_tab ()) (inject x) let whd_all env t = match kind t with @@ -145,10 +147,10 @@ let whd_all env t = | Ind _ | Construct _ | Evar _ | Meta _ -> t | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _ | Const _ |Case _ | Fix _ | CoFix _ | Proj _ -> - whd_val (create_clos_infos all env) (inject t) + whd_val (create_clos_infos all env) (create_tab ()) (inject t) end | Rel _ | Cast _ | LetIn _ | Case _ | Proj _ | Const _ | Var _ -> - whd_val (create_clos_infos all env) (inject t) + whd_val (create_clos_infos all env) (create_tab ()) (inject t) let whd_allnolet env t = match kind t with @@ -159,10 +161,10 @@ let whd_allnolet env t = | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ -> t | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | App _ | Const _ | Case _ | Fix _ | CoFix _ | Proj _ -> - whd_val (create_clos_infos allnolet env) (inject t) + whd_val (create_clos_infos allnolet env) (create_tab ()) (inject t) end | Rel _ | Cast _ | Case _ | Proj _ | Const _ | Var _ -> - whd_val (create_clos_infos allnolet env) (inject t) + whd_val (create_clos_infos allnolet env) (create_tab ()) (inject t) (********************************************************************) (* Conversion *) @@ -202,7 +204,8 @@ type 'a universe_compare = { (* Might raise NotConvertible *) compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; - compare_cumul_instances : Univ.Constraint.t -> 'a -> 'a } + compare_cumul_instances : conv_pb -> Univ.Variance.t array -> + Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a } type 'a universe_state = 'a * 'a universe_compare @@ -218,12 +221,12 @@ let sort_cmp_universes env pb s0 s1 (u, check) = let convert_instances ~flex u u' (s, check) = (check.compare_instances ~flex u u' s, check) -let get_cumulativity_constraints cv_pb cumi u u' = +let get_cumulativity_constraints cv_pb variance u u' = match cv_pb with | CONV -> - Univ.ACumulativityInfo.eq_constraints cumi u u' Univ.Constraint.empty + Univ.enforce_eq_variance_instances variance u u' Univ.Constraint.empty | CUMUL -> - Univ.ACumulativityInfo.leq_constraints cumi u u' Univ.Constraint.empty + Univ.enforce_leq_variance_instances variance u u' Univ.Constraint.empty let inductive_cumulativity_arguments (mind,ind) = mind.Declarations.mind_nparams + @@ -241,19 +244,15 @@ let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2 if not (Int.equal num_param_arity nargs) then cmp_instances u1 u2 s else - let csts = get_cumulativity_constraints cv_pb cumi u1 u2 in - cmp_cumul csts s + cmp_cumul cv_pb (Univ.ACumulativityInfo.variance cumi) u1 u2 s let convert_inductives cv_pb ind nargs u1 u2 (s, check) = convert_inductives_gen (check.compare_instances ~flex:false) check.compare_cumul_instances cv_pb ind nargs u1 u2 s, check let constructor_cumulativity_arguments (mind, ind, ctor) = - let nparamsctxt = - mind.Declarations.mind_nparams + - mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs - (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in - nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(ctor - 1) + mind.Declarations.mind_nparams + + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(ctor - 1) let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u2 s = match mind.Declarations.mind_universes with @@ -267,8 +266,10 @@ 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_. *) + let variance = Array.make (Univ.Instance.length u1) Univ.Variance.Irrelevant in + cmp_cumul CONV variance u1 u2 s let convert_constructors ctor nargs u1 u2 (s, check) = convert_constructors_gen (check.compare_instances ~flex:false) check.compare_cumul_instances @@ -313,46 +314,16 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv = cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv else raise NotConvertible -let rec no_arg_available = function - | [] -> true - | Zupdate _ :: stk -> no_arg_available stk - | Zshift _ :: stk -> no_arg_available stk - | Zapp v :: stk -> Int.equal (Array.length v) 0 && no_arg_available stk - | Zproj _ :: _ -> true - | ZcaseT _ :: _ -> true - | Zfix _ :: _ -> true - -let rec no_nth_arg_available n = function - | [] -> true - | Zupdate _ :: stk -> no_nth_arg_available n stk - | Zshift _ :: stk -> no_nth_arg_available n stk - | Zapp v :: stk -> - let k = Array.length v in - if n >= k then no_nth_arg_available (n-k) stk - else false - | Zproj _ :: _ -> true - | ZcaseT _ :: _ -> true - | Zfix _ :: _ -> true - -let rec no_case_available = function - | [] -> true - | Zupdate _ :: stk -> no_case_available stk - | Zshift _ :: stk -> no_case_available stk - | Zapp _ :: stk -> no_case_available stk - | Zproj (_,_,p) :: _ -> false - | ZcaseT _ :: _ -> false - | Zfix _ :: _ -> true - -let in_whnf (t,stk) = - match fterm_of t with - | (FLetIn _ | FCaseT _ | FApp _ - | FCLOS _ | FLIFT _ | FCast _) -> false - | FLambda _ -> no_arg_available stk - | FConstruct _ -> no_case_available stk - | FCoFix _ -> no_case_available stk - | FFix(((ri,n),(_,_,_)),_) -> no_nth_arg_available ri.(n) stk - | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _ | FProj _) -> true - | FLOCKED -> assert false +type conv_tab = { + cnv_inf : clos_infos; + lft_tab : fconstr infos_tab; + rgt_tab : fconstr infos_tab; +} +(** Invariant: for any tl ∈ lft_tab and tr ∈ rgt_tab, there is no mutable memory + location contained both in tl and in tr. *) + +(** The same heap separation invariant must hold for the fconstr arguments + passed to each respective side of the conversion function below. *) (* Conversion between [lft1]term1 and [lft2]term2 *) let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv = @@ -362,15 +333,10 @@ let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv = and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = Control.check_for_interrupt (); (* First head reduce both terms *) - let whd = whd_stack (infos_with_reds infos betaiotazeta) in - let rec whd_both (t1,stk1) (t2,stk2) = - let st1' = whd t1 stk1 in - let st2' = whd t2 stk2 in - (* Now, whd_stack on term2 might have modified st1 (due to sharing), - and st1 might not be in whnf anymore. If so, we iterate ccnv. *) - if in_whnf st1' then (st1',st2') else whd_both st1' st2' in - let ((hd1,v1),(hd2,v2)) = whd_both st1 st2 in - let appr1 = (lft1,(hd1,v1)) and appr2 = (lft2,(hd2,v2)) in + let ninfos = infos_with_reds infos.cnv_inf betaiotazeta in + let (hd1, v1 as appr1) = whd_stack ninfos infos.lft_tab (fst st1) (snd st1) in + let (hd2, v2 as appr2) = whd_stack ninfos infos.rgt_tab (fst st2) (snd st2) in + let appr1 = (lft1, appr1) and appr2 = (lft2, appr2) in (** We delay the computation of the lifts that apply to the head of the term with [el_stack] inside the branches where they are actually used. *) match (fterm_of hd1, fterm_of hd2) with @@ -380,7 +346,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (Sort s1, Sort s2) -> if not (is_empty_stack v1 && is_empty_stack v2) then anomaly (Pp.str "conversion was given ill-typed terms (Sort)."); - sort_cmp_universes (env_of_infos infos) cv_pb s1 s2 cuniv + sort_cmp_universes (env_of_infos infos.cnv_inf) cv_pb s1 s2 cuniv | (Meta n, Meta m) -> if Int.equal n m then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv @@ -407,24 +373,24 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* 2 constants, 2 local defined vars or 2 defined rels *) | (FFlex fl1, FFlex fl2) -> (try - let cuniv = conv_table_key infos fl1 fl2 cuniv in + let cuniv = conv_table_key infos.cnv_inf fl1 fl2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with NotConvertible | Univ.UniverseInconsistency _ -> (* else the oracle tells which constant is to be expanded *) - let oracle = CClosure.oracle_of_infos infos in + let oracle = CClosure.oracle_of_infos infos.cnv_inf in let (app1,app2) = if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then - match unfold_reference infos fl1 with + match unfold_reference infos.cnv_inf infos.lft_tab fl1 with | Some def1 -> ((lft1, (def1, v1)), appr2) | None -> - (match unfold_reference infos fl2 with + (match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with | Some def2 -> (appr1, (lft2, (def2, v2))) | None -> raise NotConvertible) else - match unfold_reference infos fl2 with + match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with | Some def2 -> (appr1, (lft2, (def2, v2))) | None -> - (match unfold_reference infos fl1 with + (match unfold_reference infos.cnv_inf infos.lft_tab fl1 with | Some def1 -> ((lft1, (def1, v1)), appr2) | None -> raise NotConvertible) in @@ -434,11 +400,11 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* Projections: prefer unfolding to first-order unification, which will happen naturally if the terms c1, c2 are not in constructor form *) - (match unfold_projection infos p1 with + (match unfold_projection infos.cnv_inf p1 with | Some s1 -> eqappr cv_pb l2r infos (lft1, (c1, (s1 :: v1))) appr2 cuniv | None -> - match unfold_projection infos p2 with + match unfold_projection infos.cnv_inf p2 with | Some s2 -> eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv | None -> @@ -452,26 +418,26 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = raise NotConvertible) | (FProj (p1,c1), t2) -> - (match unfold_projection infos p1 with + (match unfold_projection infos.cnv_inf p1 with | Some s1 -> eqappr cv_pb l2r infos (lft1, (c1, (s1 :: v1))) appr2 cuniv | None -> (match t2 with | FFlex fl2 -> - (match unfold_reference infos fl2 with + (match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with | Some def2 -> eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv | None -> raise NotConvertible) | _ -> raise NotConvertible)) | (t1, FProj (p2,c2)) -> - (match unfold_projection infos p2 with + (match unfold_projection infos.cnv_inf p2 with | Some s2 -> eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv | None -> (match t1 with | FFlex fl1 -> - (match unfold_reference infos fl1 with + (match unfold_reference infos.cnv_inf infos.lft_tab fl1 with | Some def1 -> eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv | None -> raise NotConvertible) @@ -521,37 +487,37 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* only one constant, defined var or defined rel *) | (FFlex fl1, c2) -> - (match unfold_reference infos fl1 with + (match unfold_reference infos.cnv_inf infos.lft_tab fl1 with | Some def1 -> (** By virtue of the previous case analyses, we know [c2] is rigid. Conversion check to rigid terms eventually implies full weak-head reduction, so instead of repeatedly performing small-step unfoldings, we perform reduction with all flags on. *) - let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos)) in - let r1 = whd_stack (infos_with_reds infos all) def1 v1 in + let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos.cnv_inf)) in + let r1 = whd_stack (infos_with_reds infos.cnv_inf all) infos.lft_tab def1 v1 in eqappr cv_pb l2r infos (lft1, r1) appr2 cuniv | None -> match c2 with | FConstruct ((ind2,j2),u2) -> (try let v2, v1 = - eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1) + eta_expand_ind_stack (info_env infos.cnv_inf) ind2 hd2 v2 (snd appr1) in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) | _ -> raise NotConvertible) | (c1, FFlex fl2) -> - (match unfold_reference infos fl2 with + (match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with | Some def2 -> (** Symmetrical case of above. *) - let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos)) in - let r2 = whd_stack (infos_with_reds infos all) def2 v2 in + let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos.cnv_inf)) in + let r2 = whd_stack (infos_with_reds infos.cnv_inf all) infos.rgt_tab def2 v2 in eqappr cv_pb l2r infos appr1 (lft2, r2) cuniv | None -> match c1 with | FConstruct ((ind1,j1),u1) -> (try let v1, v2 = - eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2) + eta_expand_ind_stack (info_env infos.cnv_inf) ind1 hd1 v1 (snd appr2) in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) | _ -> raise NotConvertible) @@ -563,7 +529,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let cuniv = convert_instances ~flex:false u1 u2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else - let mind = Environ.lookup_mind (fst ind1) (info_env infos) in + let mind = Environ.lookup_mind (fst ind1) (info_env infos.cnv_inf) in let nargs = CClosure.stack_args_size v1 in if not (Int.equal nargs (CClosure.stack_args_size v2)) then raise NotConvertible @@ -578,7 +544,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let cuniv = convert_instances ~flex:false u1 u2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else - let mind = Environ.lookup_mind (fst ind1) (info_env infos) in + let mind = Environ.lookup_mind (fst ind1) (info_env infos.cnv_inf) in let nargs = CClosure.stack_args_size v1 in if not (Int.equal nargs (CClosure.stack_args_size v2)) then raise NotConvertible @@ -591,14 +557,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (FConstruct ((ind1,j1),u1), _) -> (try let v1, v2 = - eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2) + eta_expand_ind_stack (info_env infos.cnv_inf) ind1 hd1 v1 (snd appr2) in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) | (_, FConstruct ((ind2,j2),u2)) -> (try let v2, v1 = - eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1) + eta_expand_ind_stack (info_env infos.cnv_inf) ind2 hd2 v2 (snd appr1) in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) @@ -666,6 +632,11 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv = let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 = let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in let infos = create_clos_infos ~evars reds env in + let infos = { + cnv_inf = infos; + lft_tab = create_tab (); + rgt_tab = create_tab (); + } in ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs @@ -705,7 +676,8 @@ let check_convert_instances ~flex u u' univs = else raise NotConvertible (* general conversion and inference functions *) -let check_inductive_instances csts univs = +let check_inductive_instances cv_pb variance u1 u2 univs = + let csts = get_cumulativity_constraints cv_pb variance u1 u2 in if (UGraph.check_constraints csts univs) then univs else raise NotConvertible @@ -755,7 +727,8 @@ let infer_convert_instances ~flex u u' (univs,cstrs) = else Univ.enforce_eq_instances u u' cstrs in (univs, cstrs') -let infer_inductive_instances csts (univs,csts') = +let infer_inductive_instances cv_pb variance u1 u2 (univs,csts') = + let csts = get_cumulativity_constraints cv_pb variance u1 u2 in (univs, Univ.Constraint.union csts csts') let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = @@ -882,6 +855,18 @@ let hnf_prod_app env t n = let hnf_prod_applist env t nl = List.fold_left (hnf_prod_app env) t nl +let hnf_prod_applist_assum env n c l = + let rec app n subst t l = + if Int.equal n 0 then + if l == [] then substl subst t + else anomaly (Pp.str "Too many arguments.") + else match kind (whd_allnolet env t), l with + | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l + | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l + | _, [] -> anomaly (Pp.str "Not enough arguments.") + | _ -> anomaly (Pp.str "Not enough prod/let's.") in + app n [] c l + (* Dealing with arities *) let dest_prod env = @@ -906,7 +891,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 @@ -924,7 +908,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 0e6a2b8199..14e4270b7c 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 @@ -39,7 +41,8 @@ type 'a universe_compare = { (* Might raise NotConvertible *) compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; - compare_cumul_instances : Univ.Constraint.t -> 'a -> 'a } + compare_cumul_instances : conv_pb -> Univ.Variance.t array -> + Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a } type 'a universe_state = 'a * 'a universe_compare @@ -47,7 +50,7 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t -val get_cumulativity_constraints : conv_pb -> Univ.ACumulativityInfo.t -> +val get_cumulativity_constraints : conv_pb -> Univ.Variance.t array -> Univ.Instance.t -> Univ.Instance.t -> Univ.Constraint.t val inductive_cumulativity_arguments : (Declarations.mutual_inductive_body * int) -> int @@ -105,6 +108,12 @@ val beta_app : constr -> constr -> constr (** Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *) val hnf_prod_applist : env -> types -> constr list -> types +(** In [hnf_prod_applist_assum n c args], [c] is supposed to (whd-)reduce to + the form [∀Γ.t] with [Γ] of length [n] and possibly with let-ins; it + returns [t] with the assumptions of [Γ] instantiated by [args] and + the local definitions of [Γ] expanded. *) +val hnf_prod_applist_assum : env -> int -> types -> constr list -> types + (** Compatibility alias for Term.lambda_appvect_assum *) val betazeta_appvect : int -> constr -> constr array -> 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 d0d5cb1d56..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 @@ -118,6 +120,15 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 let env = check_polymorphic_instance error env auctx auctx' in env, Univ.make_abstract_instance auctx' | Cumulative_ind cumi, Cumulative_ind cumi' -> + (** Currently there is no way to control variance of inductive types, but + just in case we require that they are in a subtyping relation. *) + let () = + let v = ACumulativityInfo.variance cumi in + let v' = ACumulativityInfo.variance cumi' in + if not (Array.for_all2 Variance.check_subtype v' v) then + CErrors.anomaly Pp.(str "Variance of " ++ KerName.print kn1 ++ + str " is not compatible with the one of " ++ KerName.print kn2) + in let auctx = Univ.ACumulativityInfo.univ_context cumi in let auctx' = Univ.ACumulativityInfo.univ_context cumi' in let env = check_polymorphic_instance error env auctx auctx' in 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 fae990d45f..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 @@ -352,10 +354,11 @@ let lambda_applist_assum n c l = let rec app n subst t l = if Int.equal n 0 then if l == [] then substl subst t - else anomaly (Pp.str "Not enough arguments.") + else anomaly (Pp.str "Too many arguments.") else match kind_of_term t, l with | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l + | _, [] -> anomaly (Pp.str "Not enough arguments.") | _ -> anomaly (Pp.str "Not enough lambda/let's.") in app n [] c l @@ -377,10 +380,11 @@ let prod_applist_assum n c l = let rec app n subst t l = if Int.equal n 0 then if l == [] then substl subst t - else anomaly (Pp.str "Not enough arguments.") + else anomaly (Pp.str "Too many arguments.") else match kind_of_term t, l with | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l + | _, [] -> anomaly (Pp.str "Not enough arguments.") | _ -> anomaly (Pp.str "Not enough prod/let's.") in app n [] c l diff --git a/kernel/term.mli b/kernel/term.mli index c9a8cf6e1e..7cb3b662d4 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 @@ -242,7 +244,7 @@ val lambda_applist : constr -> constr list -> constr val lambda_appvect : constr -> constr array -> constr (** In [lambda_applist_assum n c args], [c] is supposed to have the - form [λΓ.c] with [Γ] of length [m] and possibly with let-ins; it + form [λΓ.c] with [Γ] of length [n] and possibly with let-ins; it returns [c] with the assumptions of [Γ] instantiated by [args] and the local definitions of [Γ] expanded. *) val lambda_applist_assum : int -> constr -> constr list -> constr @@ -251,15 +253,15 @@ val lambda_appvect_assum : int -> constr -> constr array -> constr (** pseudo-reduction rule *) (** [prod_appvect] [forall (x1:B1;...;xn:Bn), B] [a1...an] @return [B[a1...an]] *) -val prod_appvect : constr -> constr array -> constr -val prod_applist : constr -> constr list -> constr +val prod_appvect : types -> constr array -> types +val prod_applist : types -> constr list -> types (** In [prod_appvect_assum n c args], [c] is supposed to have the - form [∀Γ.c] with [Γ] of length [m] and possibly with let-ins; it + form [∀Γ.c] with [Γ] of length [n] and possibly with let-ins; it returns [c] with the assumptions of [Γ] instantiated by [args] and the local definitions of [Γ] expanded. *) -val prod_appvect_assum : int -> constr -> constr array -> constr -val prod_applist_assum : int -> constr -> constr list -> constr +val prod_appvect_assum : int -> types -> constr array -> types +val prod_applist_assum : int -> types -> constr list -> types (** {5 Other term destructors. } *) @@ -475,7 +477,7 @@ val iter_constr_with_binders : ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit [@@ocaml.deprecated "Alias for [Constr.iter_with_binders]"] -val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool +val compare_constr : (int -> constr -> constr -> bool) -> int -> constr -> constr -> bool [@@ocaml.deprecated "Alias for [Constr.compare_head]"] type constr = Constr.constr diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 5f501bff10..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 @@ -223,9 +225,8 @@ let rec unzip ctx j = unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) } let feedback_completion_typecheck = - let open Feedback in Option.iter (fun state_id -> - feedback ~id:state_id Feedback.Complete) + Feedback.feedback ~id:state_id Feedback.Complete) let abstract_constant_universes = function | Monomorphic_const_entry uctx -> 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 080bb7ad48..be21381b71 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] *) @@ -266,7 +268,7 @@ struct module Expr = struct type t = Level.t * int - + (* Hashing of expressions *) module ExprHash = struct @@ -487,7 +489,40 @@ struct | [] -> cons a l in List.fold_right (fun a acc -> aux a acc) u [] - + + (** [max_var_pred p u] returns the maximum variable level in [u] satisfying + [p], -1 if not found *) + let rec max_var_pred p u = + let open Level in + match u with + | [] -> -1 + | (v, _) :: u -> + match var_index v with + | Some i when p i -> max i (max_var_pred p u) + | _ -> max_var_pred p u + + let rec remap_var u i j = + let open Level in + match u with + | [] -> [] + | (v, incr) :: u when var_index v = Some i -> + (Level.var j, incr) :: remap_var u i j + | _ :: u -> remap_var u i j + + let rec compact u max_var i = + if i >= max_var then (u,[]) else + let j = max_var_pred (fun j -> j < i) u in + if Int.equal i (j+1) then + let (u,s) = compact u max_var (i+1) in + (u, i :: s) + else + let (u,s) = compact (remap_var u i j) max_var (i+1) in + (u, j+1 :: s) + + let compact u = + let max_var = max_var_pred (fun _ -> true) u in + compact u max_var 0 + (* Returns the formal universe that is greater than the universes u and v. Used to type the products. *) let sup x y = merge_univs x y @@ -726,6 +761,13 @@ struct | Invariant, _ | _, Invariant -> Invariant | Covariant, Covariant -> Covariant + let check_subtype x y = match x, y with + | (Irrelevant | Covariant | Invariant), Irrelevant -> true + | Irrelevant, Covariant -> false + | (Covariant | Invariant), Covariant -> true + | (Irrelevant | Covariant), Invariant -> false + | Invariant, Invariant -> true + let pr = function | Irrelevant -> str "*" | Covariant -> str "+" @@ -872,6 +914,9 @@ let enforce_eq_instances x y = (Pp.str " instances of different lengths.")); CArray.fold_right2 enforce_eq_level ax ay +let enforce_eq_variance_instances = Variance.eq_constraints +let enforce_leq_variance_instances = Variance.leq_constraints + let subst_instance_level s l = match l.Level.data with | Level.Var n -> s.(n) diff --git a/kernel/univ.mli b/kernel/univ.mli index 77ebf5a11b..629d83fb86 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. *) @@ -125,6 +127,13 @@ sig val for_all : (Level.t * int -> bool) -> t -> bool val map : (Level.t * int -> 'a) -> t -> 'a list + + (** [compact u] remaps local variables in [u] such that their indices become + consecutive. It returns the new universe and the mapping. + Example: compact [(Var 0, i); (Prop, 0); (Var 2; j))] = + [(Var 0,i); (Prop, 0); (Var 1; j)], [0; 2] + *) + val compact : t -> t * int list end type universe = Universe.t @@ -246,6 +255,9 @@ sig A'] as opposed to [A' <= A]. *) type t = Irrelevant | Covariant | Invariant + (** [check_subtype x y] holds if variance [y] is also an instance of [x] *) + val check_subtype : t -> t -> bool + val sup : t -> t -> t val pr : t -> Pp.t @@ -300,6 +312,9 @@ type universe_instance = Instance.t val enforce_eq_instances : Instance.t constraint_function +val enforce_eq_variance_instances : Variance.t array -> Instance.t constraint_function +val enforce_leq_variance_instances : Variance.t array -> Instance.t constraint_function + type 'a puniverses = 'a * Instance.t val out_punivs : 'a puniverses -> 'a val in_punivs : 'a -> 'a puniverses 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 1102cdec18..0e0cb4e584 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -1,13 +1,16 @@ (************************************************************************) -(* 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 open Cbytecodes +open Univ (*******************************************) (* Initalization of the abstract machine ***) @@ -117,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 *) @@ -135,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 @@ -166,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" @@ -188,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 u = ref (Obj.obj (Obj.field at 0)) in - for i = 0 to nargs args - 1 do - u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i))) - done; - Vsort (Type !u) + let args = Array.init (nargs args) (arg args) in + 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 -> @@ -242,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 @@ -272,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 @@ -284,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) @@ -303,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) @@ -329,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" (*************************************************) @@ -501,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 |