diff options
Diffstat (limited to 'kernel')
40 files changed, 514 insertions, 404 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 61ed40394e..ac4c6c52c6 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -397,7 +397,7 @@ let update v1 no t = type stack_member = | Zapp of fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs - | Zproj of int * int * Constant.t + | Zproj of Projection.Repr.t | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr @@ -691,8 +691,8 @@ let rec zip m stk = | ZcaseT(ci,p,br,e)::s -> let t = FCaseT(ci, p, m, br, e) in zip {norm=neutr m.norm; term=t} s - | Zproj (i,j,cst) :: s -> - zip {norm=neutr m.norm; term=FProj(Projection.make cst true,m)} s + | Zproj p :: s -> + zip {norm=neutr m.norm; term=FProj(Projection.make p true,m)} s | Zfix(fx,par)::s -> zip fx (par @ append_stack [|m|] s) | Zshift(n)::s -> @@ -822,21 +822,24 @@ let drop_parameters depth n argstk = let eta_expand_ind_stack env ind m s (f, s') = let open Declarations in let mib = lookup_mind (fst ind) env in - match mib.Declarations.mind_record with - | PrimRecord infos when - mib.Declarations.mind_finite == Declarations.BiFinite -> - let (_, projs, _) = infos.(snd ind) in - (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') -> + (* disallow eta-exp for non-primitive records *) + if not (mib.mind_finite == BiFinite) then raise Not_found; + match Declareops.inductive_make_projections ind mib with + | Some projs -> + (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') -> arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *) - let pars = mib.Declarations.mind_nparams in - let right = fapp_stack (f, s') in - let (depth, args, s) = strip_update_shift_app m s in - (** Try to drop the params, might fail on partially applied constructors. *) - let argss = try_drop_parameters depth pars args in - let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *) - term = FProj (Projection.make p true, right) }) projs in - argss, [Zapp hstack] - | PrimRecord _ | NotRecord | FakeRecord -> raise Not_found (* disallow eta-exp for non-primitive records *) + let pars = mib.Declarations.mind_nparams in + let right = fapp_stack (f, s') in + let (depth, args, s) = strip_update_shift_app m s in + (** Try to drop the params, might fail on partially applied constructors. *) + let argss = try_drop_parameters depth pars args in + let hstack = Array.map (fun p -> + { norm = Red; (* right can't be a constructor though *) + term = FProj (Projection.make p true, right) }) + projs + in + argss, [Zapp hstack] + | None -> raise Not_found (* disallow eta-exp for non-primitive records *) let rec project_nth_arg n argstk = match argstk with @@ -875,9 +878,7 @@ let contract_fix_vect fix = let unfold_projection info p = if red_projection info.i_flags p then - let open Declarations in - let pb = lookup_projection p (info_env info) in - Some (Zproj (pb.proj_npars, pb.proj_arg, Projection.constant p)) + Some (Zproj (Projection.repr p)) else None (*********************************************************************) @@ -958,9 +959,9 @@ let rec knr info tab m stk = let stk' = par @ append_stack [|rarg|] s in let (fxe,fxbd) = contract_fix_vect fx.term in 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 + | (depth, args, Zproj p::s) when use_match -> + let rargs = drop_parameters depth (Projection.Repr.npars p) args in + let rarg = project_nth_arg (Projection.Repr.arg p) rargs in kni info tab rarg s | (_,args,s) -> (m,args@s)) else (m,stk) @@ -1002,7 +1003,7 @@ let rec zip_term zfun m stk = let t = mkCase(ci, zfun (mk_clos e p), m, Array.map (fun b -> zfun (mk_clos e b)) br) in zip_term zfun t s - | Zproj(_,_,p)::s -> + | Zproj p::s -> let t = mkProj (Projection.make p true, m) in zip_term zfun t s | Zfix(fx,par)::s -> diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index f8f98f0abe..1e3e7b48ac 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -152,7 +152,7 @@ type fterm = type stack_member = | Zapp of fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs - | Zproj of int * int * Constant.t + | Zproj of Projection.Repr.t | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 3095ce148b..9a1224aab2 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -128,8 +128,7 @@ type instruction = | Ksetfield of int | Kstop | Ksequence of bytecodes * bytecodes - | Kproj of int * Constant.t (* index of the projected argument, - name of projection *) + | Kproj of Projection.Repr.t | Kensurestackcapacity of int (* spiwack: instructions concerning integers *) | Kbranch of Label.t (* jump to label *) @@ -311,7 +310,7 @@ let rec pp_instr i = | Kbranch lbl -> str "branch " ++ pp_lbl lbl - | Kproj(n,p) -> str "proj " ++ int n ++ str " " ++ Constant.print p + | Kproj p -> str "proj " ++ Projection.Repr.print p | Kensurestackcapacity size -> str "growstack " ++ int size diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index de21401b31..f17a1e657e 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -88,8 +88,7 @@ type instruction = | Ksetfield of int (** accu[n] = sp[0] ; sp = pop sp *) | Kstop | Ksequence of bytecodes * bytecodes - | Kproj of int * Constant.t (** index of the projected argument, - name of projection *) + | Kproj of Projection.Repr.t | Kensurestackcapacity of int (** spiwack: instructions concerning integers *) diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 6677db2fd9..e336ea922d 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -492,8 +492,8 @@ let rec compile_lam env cenv lam sz cont = | Lval v -> compile_structured_constant cenv v sz cont - | Lproj (n,kn,arg) -> - compile_lam env cenv arg sz (Kproj (n,kn) :: cont) + | Lproj (p,arg) -> + compile_lam env cenv arg sz (Kproj p :: cont) | Lvar id -> pos_named id cenv :: cont @@ -501,6 +501,9 @@ let rec compile_lam env cenv lam sz cont = if Array.is_empty args then compile_fv_elem cenv (FVevar evk) sz cont else + (** Arguments are reversed in evar instances *) + let args = Array.copy args in + let () = Array.rev args in comp_app compile_fv_elem (compile_lam env) cenv (FVevar evk) args sz cont | Lconst (kn,u) -> compile_constant env cenv kn u [||] sz cont diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 2426255e48..ca24f9b689 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -27,7 +27,7 @@ type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant | Reloc_getglobal of Names.Constant.t - | Reloc_proj_name of Constant.t + | Reloc_proj_name of Projection.Repr.t let eq_reloc_info r1 r2 = match r1, r2 with | Reloc_annot sw1, Reloc_annot sw2 -> eq_annot_switch sw1 sw2 @@ -36,7 +36,7 @@ let eq_reloc_info r1 r2 = match r1, r2 with | Reloc_const _, _ -> false | Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.equal c1 c2 | Reloc_getglobal _, _ -> false -| Reloc_proj_name p1, Reloc_proj_name p2 -> Constant.equal p1 p2 +| Reloc_proj_name p1, Reloc_proj_name p2 -> Projection.Repr.equal p1 p2 | Reloc_proj_name _, _ -> false let hash_reloc_info r = @@ -45,7 +45,7 @@ let hash_reloc_info r = | 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) - | Reloc_proj_name p -> combinesmall 4 (Constant.hash p) + | Reloc_proj_name p -> combinesmall 4 (Projection.Repr.hash p) module RelocTable = Hashtbl.Make(struct type t = reloc_info @@ -284,7 +284,7 @@ let emit_instr env = function 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 env opPROJ; out_int env n; slot_for_proj_name env p + | Kproj p -> out env opPROJ; out_int env (Projection.Repr.arg p); slot_for_proj_name env p | Kensurestackcapacity size -> out env opENSURESTACKCAPACITY; out_int env size (* spiwack *) | Kbranch lbl -> out env opBRANCH; out_label env lbl @@ -371,7 +371,7 @@ let subst_reloc s ri = Reloc_annot {a with ci = ci} | Reloc_const sc -> Reloc_const (subst_strcst s sc) | Reloc_getglobal kn -> Reloc_getglobal (subst_constant s kn) - | Reloc_proj_name p -> Reloc_proj_name (subst_constant s p) + | Reloc_proj_name p -> Reloc_proj_name (subst_proj_repr s p) let subst_patches subst p = let infos = CArray.map (fun (r, pos) -> (subst_reloc subst r, pos)) p.reloc_infos in diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index 696721c375..9009926bdb 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -5,7 +5,7 @@ type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant | Reloc_getglobal of Constant.t - | Reloc_proj_name of Constant.t + | Reloc_proj_name of Projection.Repr.t type patches type emitcodes diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli index f42c46175c..171ca38830 100644 --- a/kernel/cinstr.mli +++ b/kernel/cinstr.mli @@ -36,7 +36,7 @@ and lambda = | Lval of structured_constant | Lsort of Sorts.t | Lind of pinductive - | Lproj of int * Constant.t * lambda + | Lproj of Projection.Repr.t * lambda | Luint of uint (* Cofixpoints have to be in eta-expanded form for their call-by-need evaluation diff --git a/kernel/clambda.ml b/kernel/clambda.ml index f1b6f3dffc..7c00e40fb0 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -111,9 +111,9 @@ let rec pp_lam lam = (str "(PRIM " ++ pr_con kn ++ spc() ++ prlist_with_sep spc pp_lam (Array.to_list args) ++ str")") - | Lproj(i,kn,arg) -> + | Lproj(p,arg) -> hov 1 - (str "(proj#" ++ int i ++ spc() ++ pr_con kn ++ str "(" ++ pp_lam arg + (str "(proj " ++ Projection.Repr.print p ++ str "(" ++ pp_lam arg ++ str ")") | Luint _ -> str "(uint)" @@ -205,9 +205,9 @@ let rec map_lam_with_binders g f n lam = | Lprim(kn,ar,op,args) -> let args' = Array.Smart.map (f n) args in if args == args' then lam else Lprim(kn,ar,op,args') - | Lproj(i,kn,arg) -> + | Lproj(p,arg) -> let arg' = f n arg in - if arg == arg' then lam else Lproj(i,kn,arg') + if arg == arg' then lam else Lproj(p,arg') | Luint u -> let u' = map_uint g f n u in if u == u' then lam else Luint u' @@ -376,7 +376,7 @@ let rec occurrence k kind lam = let kind = occurrence_args k kind ltypes in let _ = occurrence_args (k+Array.length ids) false lbodies in kind - | Lproj(_,_,arg) -> + | Lproj(_,arg) -> occurrence k kind arg | Luint u -> occurrence_uint k kind u @@ -708,10 +708,8 @@ let rec lambda_of_constr env c = Lcofix(init, (names, ltypes, lbodies)) | Proj (p,c) -> - let pb = lookup_projection p env.global_env in - let n = pb.proj_arg in let lc = lambda_of_constr env c in - Lproj (n,Projection.constant p,lc) + Lproj (Projection.repr p,lc) and lambda_of_app env f args = match Constr.kind f with diff --git a/kernel/context.ml b/kernel/context.ml index 831dc850fb..4a7204b75c 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -149,6 +149,10 @@ struct | LocalAssum (na, ty) -> na, None, ty | LocalDef (na, v, ty) -> na, Some v, ty + let drop_body = function + | LocalAssum _ as d -> d + | LocalDef (na, v, ty) -> LocalAssum (na, ty) + end (** Rel-context is represented as a list of declarations. @@ -211,6 +215,8 @@ struct | Declaration.LocalAssum _ :: ctx -> aux (false::l) ctx in aux [] l + let drop_bodies l = List.Smart.map Declaration.drop_body l + (** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] with n = |Δ| and with the {e local definitions} of [Γ] skipped in [args]. Example: for [x:T, y:=c, z:U] and [n]=2, it gives [Rel 5, Rel 3]. *) @@ -348,6 +354,10 @@ struct | id, None, ty -> LocalAssum (id, ty) | id, Some v, ty -> LocalDef (id, v, ty) + let drop_body = function + | LocalAssum _ as d -> d + | LocalDef (id, v, ty) -> LocalAssum (id, ty) + let of_rel_decl f = function | Rel.Declaration.LocalAssum (na,t) -> LocalAssum (f na, t) @@ -403,6 +413,8 @@ struct let to_vars l = List.fold_left (fun accu decl -> Id.Set.add (Declaration.get_id decl) accu) Id.Set.empty l + let drop_bodies l = List.Smart.map Declaration.drop_body l + (** [instance_from_named_context Ω] builds an instance [args] such that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it diff --git a/kernel/context.mli b/kernel/context.mli index 957ac4b3d6..2b0d36cb8c 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -85,6 +85,9 @@ sig val fold_constr : ('c -> 'a -> 'a) -> ('c, 'c) pt -> 'a -> 'a val to_tuple : ('c, 't) pt -> Name.t * 'c option * 't + + (** Turn [LocalDef] into [LocalAssum], identity otherwise. *) + val drop_body : ('c, 't) pt -> ('c, 't) pt end (** Rel-context is represented as a list of declarations. @@ -129,6 +132,9 @@ sig and each {e local definition} is mapped to [false]. *) val to_tags : ('c, 't) pt -> bool list + (** Turn all [LocalDef] into [LocalAssum], leave [LocalAssum] unchanged. *) + val drop_bodies : ('c, 't) pt -> ('c, 't) pt + (** [extended_list mk n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] with n = |Δ| and with the {e local definitions} of [Γ] skipped in [args] where [mk] is used to build the corresponding variables. @@ -202,6 +208,9 @@ sig val to_tuple : ('c, 't) pt -> Id.t * 'c option * 't val of_tuple : Id.t * 'c option * 't -> ('c, 't) pt + (** Turn [LocalDef] into [LocalAssum], identity otherwise. *) + val drop_body : ('c, 't) pt -> ('c, 't) pt + (** Convert [Rel.Declaration.t] value to the corresponding [Named.Declaration.t] value. The function provided as the first parameter determines how to translate "names" to "ids". *) val of_rel_decl : (Name.t -> Id.t) -> ('c, 't) Rel.Declaration.pt -> ('c, 't) pt @@ -249,6 +258,9 @@ sig (** Return the set of all identifiers bound in a given named-context. *) val to_vars : ('c, 't) pt -> Id.Set.t + (** Turn all [LocalDef] into [LocalAssum], leave [LocalAssum] unchanged. *) + val drop_bodies : ('c, 't) pt -> ('c, 't) pt + (** [to_instance Ω] builds an instance [args] such that [Ω ⊢ args:Ω] where [Ω] is a named-context and with the local definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 094609b963..c06358054e 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -126,16 +126,13 @@ let expmod_constr cache modlist c = | Not_found -> Constr.map substrec c) | Proj (p, c') -> - (try - (** No need to expand parameters or universes for projections *) - let map cst = - let _ = Cmap.find cst (fst modlist) in - pop_con cst - in - let p = Projection.map map p in - let c' = substrec c' in - mkProj (p, c') - with Not_found -> Constr.map substrec c) + let map cst npars = + let _, newpars = Mindmap.find cst (snd modlist) in + pop_mind cst, npars + Array.length newpars + in + let p' = try Projection.map_npars map p with Not_found -> p in + let c'' = substrec c' in + if p == p' && c' == c'' then c else mkProj (p', c'') | _ -> Constr.map substrec c diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index bbe0937820..bb9231d000 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -77,11 +77,7 @@ module AnnotTable = Hashtbl.Make (struct let hash = hash_annot_switch end) -module ProjNameTable = Hashtbl.Make (struct - type t = Constant.t - let equal = Constant.equal - let hash = Constant.hash -end) +module ProjNameTable = Hashtbl.Make (Projection.Repr) let str_cst_tbl : int SConstTable.t = SConstTable.create 31 diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 95078800e7..0811eb72fd 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -46,16 +46,6 @@ type inline = int option (** A constant can have no body (axiom/parameter), or a transparent body, or an opaque one *) -(** Projections are a particular kind of constant: - always transparent. *) - -type projection_body = { - proj_ind : inductive; - proj_npars : int; - proj_arg : int; (** Projection index, starting from 0 *) - proj_type : types; (* Type under params *) -} - (* Global declarations (i.e. constants) can be either: *) type constant_def = | Undef of inline (** a global assumption *) @@ -114,7 +104,7 @@ v} If it is a primitive record, for every type in the block, we get: - The identifier for the binder name of the record in primitive projections. - The constants associated to each projection. - - The checked projection bodies. + - The projection types (under parameters). The kernel does not exploit the difference between [NotRecord] and [FakeRecord]. It is mostly used by extraction, and should be extruded from @@ -124,7 +114,7 @@ v} type record_info = | NotRecord | FakeRecord -| PrimRecord of (Id.t * Constant.t array * projection_body array) array +| PrimRecord of (Id.t * Label.t array * types array) array type regular_inductive_arity = { mind_user_arity : types; diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 3e6c4858e0..bbe4bc0dcb 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -83,11 +83,6 @@ let subst_const_def sub def = match def with | Def c -> Def (subst_constr sub c) | OpaqueDef o -> OpaqueDef (Opaqueproof.subst_opaque sub o) -let subst_const_proj sub pb = - { pb with proj_ind = subst_ind sub pb.proj_ind; - proj_type = subst_mps sub pb.proj_type; - } - let subst_const_body sub cb = assert (List.is_empty cb.const_hyps); (* we're outside sections *) if is_empty_subst sub then cb @@ -213,10 +208,9 @@ let subst_mind_record sub r = match r with | FakeRecord -> FakeRecord | PrimRecord infos -> let map (id, ps, pb as info) = - let ps' = Array.Smart.map (subst_constant sub) ps in - let pb' = Array.Smart.map (subst_const_proj sub) pb in - if ps' == ps && pb' == pb then info - else (id, ps', pb') + let pb' = Array.Smart.map (subst_mps sub) pb in + if pb' == pb then info + else (id, ps, pb') in let infos' = Array.Smart.map map infos in if infos' == infos then r else PrimRecord infos' @@ -254,6 +248,25 @@ let inductive_is_cumulative mib = | Polymorphic_ind ctx -> false | Cumulative_ind cumi -> true +let inductive_make_projection ind mib ~proj_arg = + match mib.mind_record with + | NotRecord | FakeRecord -> None + | PrimRecord infos -> + Some (Names.Projection.Repr.make ind + ~proj_npars:mib.mind_nparams + ~proj_arg + (pi2 infos.(snd ind)).(proj_arg)) + +let inductive_make_projections ind mib = + match mib.mind_record with + | NotRecord | FakeRecord -> None + | PrimRecord infos -> + let projs = Array.mapi (fun proj_arg lab -> + Names.Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg lab) + (pi2 infos.(snd ind)) + in + Some projs + (** {6 Hash-consing of inductive declarations } *) let hcons_regular_ind_arity a = diff --git a/kernel/declareops.mli b/kernel/declareops.mli index fb46112ea7..f91e69807f 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -66,6 +66,11 @@ val inductive_is_polymorphic : mutual_inductive_body -> bool (** Is the inductive cumulative? *) val inductive_is_cumulative : mutual_inductive_body -> bool +val inductive_make_projection : Names.inductive -> mutual_inductive_body -> proj_arg:int -> + Names.Projection.Repr.t option +val inductive_make_projections : Names.inductive -> mutual_inductive_body -> + Names.Projection.Repr.t array option + (** {6 Kernel flags} *) (** A default, safe set of flags for kernel type-checking *) diff --git a/kernel/environ.ml b/kernel/environ.ml index 4ab4698031..e7efa5e2c9 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -52,7 +52,6 @@ type mind_key = mutual_inductive_body * link_info ref type globals = { env_constants : constant_key Cmap_env.t; - env_projections : projection_body Cmap_env.t; env_inductives : mind_key Mindmap_env.t; env_modules : module_body MPmap.t; env_modtypes : module_type_body MPmap.t; @@ -110,7 +109,6 @@ let empty_rel_context_val = { let empty_env = { env_globals = { env_constants = Cmap_env.empty; - env_projections = Cmap_env.empty; env_inductives = Mindmap_env.empty; env_modules = MPmap.empty; env_modtypes = MPmap.empty}; @@ -490,11 +488,24 @@ let polymorphic_pconstant (cst,u) env = let type_in_type_constant cst env = not (lookup_constant cst env).const_typing_flags.check_universes -let lookup_projection cst env = - Cmap_env.find (Projection.constant cst) env.env_globals.env_projections - -let is_projection cst env = - Cmap_env.mem cst env.env_globals.env_projections +let lookup_projection p env = + let mind,i = Projection.inductive p in + let mib = lookup_mind mind env in + (if not (Int.equal mib.mind_nparams (Projection.npars p)) + then anomaly ~label:"lookup_projection" Pp.(str "Bad number of parameters on projection.")); + match mib.mind_record with + | NotRecord | FakeRecord -> anomaly ~label:"lookup_projection" Pp.(str "not a projection") + | PrimRecord infos -> + let _,_,typs = infos.(i) in + typs.(Projection.arg p) + +let get_projection env ind ~proj_arg = + let mib = lookup_mind (fst ind) env in + Declareops.inductive_make_projection ind mib ~proj_arg + +let get_projections env ind = + let mib = lookup_mind (fst ind) env in + Declareops.inductive_make_projections ind mib (* Mutual Inductives *) let polymorphic_ind (mind,i) env = @@ -518,17 +529,9 @@ let template_polymorphic_pind (ind,u) env = let add_mind_key kn (mind, _ as mind_key) env = let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in - let new_projections = match mind.mind_record with - | NotRecord | FakeRecord -> env.env_globals.env_projections - | PrimRecord projs -> - Array.fold_left (fun accu (id, kns, pbs) -> - Array.fold_left2 (fun accu kn pb -> - Cmap_env.add kn pb accu) accu kns pbs) - env.env_globals.env_projections projs - in let new_globals = { env.env_globals with - env_inductives = new_inds; env_projections = new_projections; } in + env_inductives = new_inds; } in { env with env_globals = new_globals } let add_mind kn mib env = diff --git a/kernel/environ.mli b/kernel/environ.mli index 0259dbbdda..f45b7be821 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -217,8 +217,11 @@ val constant_opt_value_in : env -> Constant.t puniverses -> constr option (** {6 Primitive projections} *) -val lookup_projection : Names.Projection.t -> env -> projection_body -val is_projection : Constant.t -> env -> bool +(** Checks that the number of parameters is correct. *) +val lookup_projection : Names.Projection.t -> env -> types + +val get_projection : env -> inductive -> proj_arg:int -> Names.Projection.Repr.t option +val get_projections : env -> inductive -> Names.Projection.Repr.t array option (** {5 Inductive types } *) val lookup_mind_key : MutInd.t -> env -> mind_key diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 5d45c2c1ad..d7eb865e0a 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -796,7 +796,6 @@ let compute_projections (kn, i as ind) mib = let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in - let mp, dp, l = MutInd.repr3 kn in (** We build a substitution smashing the lets in the record parameters so that typechecking projections requires just a substitution and not matching with a parameter context. *) @@ -810,7 +809,7 @@ let compute_projections (kn, i as ind) mib = mkRel 1 :: List.map (lift 1) subst in subst in - let projections decl (i, j, kns, pbs, letsubst) = + let projections decl (i, j, labs, pbs, letsubst) = match decl with | LocalDef (na,c,t) -> (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)] @@ -822,11 +821,12 @@ let compute_projections (kn, i as ind) mib = (* From [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj)] to [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj+1)] *) let letsubst = c2 :: letsubst in - (i, j+1, kns, pbs, letsubst) + (i, j+1, labs, pbs, letsubst) | LocalAssum (na,t) -> match na with | Name id -> - let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in + let lab = Label.of_id id in + let kn = Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg:i lab in (* from [params, field1,..,fieldj |- t(params,field1,..,fieldj)] to [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj] *) let t = liftn 1 j t in @@ -836,15 +836,13 @@ let compute_projections (kn, i as ind) mib = (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)] to [params, x:I |- t(proj1 x,..,projj x)] *) let fterm = mkProj (Projection.make kn false, mkRel 1) in - let body = { proj_ind = ind; proj_npars = mib.mind_nparams; - proj_arg = i; proj_type = projty; } in - (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: letsubst) + (i + 1, j + 1, lab :: labs, projty :: pbs, fterm :: letsubst) | Anonymous -> raise UndefinableExpansion in - let (_, _, kns, pbs, letsubst) = + let (_, _, labs, pbs, letsubst) = List.fold_right projections ctx (0, 1, [], [], paramsletsubst) in - Array.of_list (List.rev kns), + Array.of_list (List.rev labs), Array.of_list (List.rev pbs) let abstract_inductive_universes iu = @@ -954,8 +952,8 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r (** The elimination criterion ensures that all projections can be defined. *) if Array.for_all is_record packets then let map i id = - let kn, projs = compute_projections (kn, i) mib in - (id, kn, projs) + let labs, projs = compute_projections (kn, i) mib in + (id, labs, projs) in try PrimRecord (Array.mapi map rid) with UndefinableExpansion -> FakeRecord diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 7c36dac67d..cb09cfa827 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -42,6 +42,3 @@ val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_induct val enforce_indices_matter : unit -> unit val is_indices_matter : unit -> bool - -val compute_projections : inductive -> - mutual_inductive_body -> (Constant.t array * projection_body array) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 88b00600e4..4d13a5fcb8 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -798,8 +798,7 @@ let rec subterm_specif renv stack t = (* We take the subterm specs of the constructor of the record *) let wf_args = (dest_subterms wf).(0) in (* We extract the tree of the projected argument *) - let pb = lookup_projection p renv.env in - let n = pb.proj_arg in + let n = Projection.arg p in spec_of_tree (List.nth wf_args n) | Dead_code -> Dead_code | Not_subterm -> Not_subterm) diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index a47af56ca5..b35b9dda31 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -332,6 +332,12 @@ let subst_constant sub con = try fst (subst_con0 sub (con,Univ.Instance.empty)) with No_subst -> con +let subst_proj_repr sub p = + Projection.Repr.map (subst_mind sub) p + +let subst_proj sub p = + Projection.map (subst_mind sub) p + (* Here the semantics is completely unclear. What does "Hint Unfold t" means when "t" is a parameter? Does the user mean "Unfold X.t" or does she mean "Unfold y" @@ -346,11 +352,7 @@ let rec map_kn f f' c = match kind c with | Const kn -> (try snd (f' kn) with No_subst -> c) | Proj (p,t) -> - let p' = - try - Projection.map (fun kn -> fst (f' (kn,Univ.Instance.empty))) p - with No_subst -> p - in + let p' = Projection.map f p in let t' = func t in if p' == p && t' == t then c else mkProj (p', t') diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 76a1d173b9..2e5211c770 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -147,6 +147,9 @@ val subst_con_kn : val subst_constant : substitution -> Constant.t -> Constant.t +val subst_proj_repr : substitution -> Projection.Repr.t -> Projection.Repr.t +val subst_proj : substitution -> Projection.t -> Projection.t + (** Here the semantics is completely unclear. What does "Hint Unfold t" means when "t" is a parameter? Does the user mean "Unfold X.t" or does she mean "Unfold y" diff --git a/kernel/names.ml b/kernel/names.ml index 1d2a7c4ce5..e1d70e8111 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -771,29 +771,141 @@ type module_path = ModPath.t = module Projection = struct - type t = Constant.t * bool + module Repr = struct + type t = + { proj_ind : inductive; + proj_npars : int; + proj_arg : int; + proj_name : Label.t; } + + let make proj_ind ~proj_npars ~proj_arg proj_name = + {proj_ind;proj_npars;proj_arg;proj_name} + + let inductive c = c.proj_ind + + let mind c = fst c.proj_ind + + let constant c = KerPair.change_label (mind c) c.proj_name + + let label c = c.proj_name + + let npars c = c.proj_npars + + let arg c = c.proj_arg + + let equal a b = + eq_ind a.proj_ind b.proj_ind && Int.equal a.proj_arg b.proj_arg + + let hash p = + Hashset.Combine.combinesmall p.proj_arg (ind_hash p.proj_ind) + + module SyntacticOrd = struct + let compare a b = + let c = ind_syntactic_ord a.proj_ind b.proj_ind in + if c == 0 then Int.compare a.proj_arg b.proj_arg + else c + + let equal a b = + a.proj_arg == b.proj_arg && eq_syntactic_ind a.proj_ind b.proj_ind + + let hash p = + Hashset.Combine.combinesmall p.proj_arg (ind_hash p.proj_ind) + end + module CanOrd = struct + let compare a b = + let c = ind_ord a.proj_ind b.proj_ind in + if c == 0 then Int.compare a.proj_arg b.proj_arg + else c + + let equal a b = + a.proj_arg == b.proj_arg && eq_ind a.proj_ind b.proj_ind + + let hash p = + Hashset.Combine.combinesmall p.proj_arg (ind_hash p.proj_ind) + end + module UserOrd = struct + let compare a b = + let c = ind_user_ord a.proj_ind b.proj_ind in + if c == 0 then Int.compare a.proj_arg b.proj_arg + else c + + let equal a b = + a.proj_arg == b.proj_arg && eq_user_ind a.proj_ind b.proj_ind + + let hash p = + Hashset.Combine.combinesmall p.proj_arg (ind_user_hash p.proj_ind) + end + + let compare a b = + let c = ind_ord a.proj_ind b.proj_ind in + if c == 0 then Int.compare a.proj_arg b.proj_arg + else c + + module Self_Hashcons = struct + type nonrec t = t + type u = (inductive -> inductive) * (Id.t -> Id.t) + let hashcons (hind,hid) p = + { proj_ind = hind p.proj_ind; + proj_npars = p.proj_npars; + proj_arg = p.proj_arg; + proj_name = hid p.proj_name } + let eq p p' = + p == p' || (p.proj_ind == p'.proj_ind && p.proj_npars == p'.proj_npars && p.proj_arg == p'.proj_arg && p.proj_name == p'.proj_name) + let hash = hash + end + module HashRepr = Hashcons.Make(Self_Hashcons) + let hcons = Hashcons.simple_hcons HashRepr.generate HashRepr.hcons (hcons_ind,Id.hcons) + + let map_npars f p = + let ind = fst p.proj_ind in + let npars = p.proj_npars in + let ind', npars' = f ind npars in + if ind == ind' && npars == npars' then p + else {p with proj_ind = (ind',snd p.proj_ind); proj_npars = npars'} + + let map f p = map_npars (fun mind n -> f mind, n) p + + let to_string p = Constant.to_string (constant p) + let print p = Constant.print (constant p) + end + + type t = Repr.t * bool let make c b = (c, b) - let constant = fst + let mind (c,_) = Repr.mind c + let inductive (c,_) = Repr.inductive c + let npars (c,_) = Repr.npars c + let arg (c,_) = Repr.arg c + let constant (c,_) = Repr.constant c + let label (c,_) = Repr.label c + let repr = fst let unfolded = snd let unfold (c, b as p) = if b then p else (c, true) - let equal (c, b) (c', b') = Constant.equal c c' && b == b' - let hash (c, b) = (if b then 0 else 1) + Constant.hash c + let equal (c, b) (c', b') = Repr.equal c c' && b == b' + + let hash (c, b) = (if b then 0 else 1) + Repr.hash c module SyntacticOrd = struct let compare (c, b) (c', b') = - if b = b' then Constant.SyntacticOrd.compare c c' else -1 + if b = b' then Repr.SyntacticOrd.compare c c' else -1 + let equal (c, b as x) (c', b' as x') = + x == x' || b = b' && Repr.SyntacticOrd.equal c c' + let hash (c, b) = (if b then 0 else 1) + Repr.SyntacticOrd.hash c + end + module CanOrd = struct + let compare (c, b) (c', b') = + if b = b' then Repr.CanOrd.compare c c' else -1 let equal (c, b as x) (c', b' as x') = - x == x' || b = b' && Constant.SyntacticOrd.equal c c' - let hash (c, b) = (if b then 0 else 1) + Constant.SyntacticOrd.hash c + x == x' || b = b' && Repr.CanOrd.equal c c' + let hash (c, b) = (if b then 0 else 1) + Repr.CanOrd.hash c end module Self_Hashcons = struct type nonrec t = t - type u = Constant.t -> Constant.t + type u = Repr.t -> Repr.t let hashcons hc (c,b) = (hc c,b) let eq ((c,b) as x) ((c',b') as y) = x == y || (c == c' && b == b') @@ -802,15 +914,19 @@ struct module HashProjection = Hashcons.Make(Self_Hashcons) - let hcons = Hashcons.simple_hcons HashProjection.generate HashProjection.hcons hcons_con + let hcons = Hashcons.simple_hcons HashProjection.generate HashProjection.hcons Repr.hcons let compare (c, b) (c', b') = - if b == b' then Constant.CanOrd.compare c c' + if b == b' then Repr.compare c c' else if b then 1 else -1 let map f (c, b as x) = - let c' = f c in - if c' == c then x else (c', b) + let c' = Repr.map f c in + if c' == c then x else (c', b) + + let map_npars f (c, b as x) = + let c' = Repr.map_npars f c in + if c' == c then x else (c', b) let to_string p = Constant.to_string (constant p) let print p = Constant.print (constant p) diff --git a/kernel/names.mli b/kernel/names.mli index 4eb5adb62f..1cdf5c2402 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -549,17 +549,68 @@ type module_path = ModPath.t = [@@ocaml.deprecated "Alias type"] module Projection : sig - type t + module Repr : sig + type t + + val make : inductive -> proj_npars:int -> proj_arg:int -> Label.t -> t + + module SyntacticOrd : sig + val compare : t -> t -> int + val equal : t -> t -> bool + val hash : t -> int + end + module CanOrd : sig + val compare : t -> t -> int + val equal : t -> t -> bool + val hash : t -> int + end + module UserOrd : sig + val compare : t -> t -> int + val equal : t -> t -> bool + val hash : t -> int + end + + val constant : t -> Constant.t + (** Don't use this if you don't have to. *) + + val inductive : t -> inductive + val mind : t -> MutInd.t + val npars : t -> int + val arg : t -> int + val label : t -> Label.t + + val equal : t -> t -> bool + val hash : t -> int + val compare : t -> t -> int + + val map : (MutInd.t -> MutInd.t) -> t -> t + val map_npars : (MutInd.t -> int -> MutInd.t * int) -> t -> t + + val print : t -> Pp.t + val to_string : t -> string + end + type t (* = Repr.t * bool *) - val make : Constant.t -> bool -> t + val make : Repr.t -> bool -> t + val repr : t -> Repr.t module SyntacticOrd : sig val compare : t -> t -> int val equal : t -> t -> bool val hash : t -> int end + module CanOrd : sig + val compare : t -> t -> int + val equal : t -> t -> bool + val hash : t -> int + end val constant : t -> Constant.t + val mind : t -> MutInd.t + val inductive : t -> inductive + val npars : t -> int + val arg : t -> int + val label : t -> Label.t val unfolded : t -> bool val unfold : t -> t @@ -570,7 +621,8 @@ module Projection : sig val compare : t -> t -> int - val map : (Constant.t -> Constant.t) -> t -> t + val map : (MutInd.t -> MutInd.t) -> t -> t + val map_npars : (MutInd.t -> int -> MutInd.t * int) -> t -> t val to_string : t -> string val print : t -> Pp.t diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 39f7de9426..cc35a70cbf 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -278,7 +278,6 @@ type primitive = | Mk_rel of int | Mk_var of Id.t | Mk_proj - | Is_accu | Is_int | Cast_accu | Upd_cofix @@ -319,7 +318,6 @@ let eq_primitive p1 p2 = | Mk_cofix i1, Mk_cofix i2 -> Int.equal i1 i2 | Mk_rel i1, Mk_rel i2 -> Int.equal i1 i2 | Mk_var id1, Mk_var id2 -> Id.equal id1 id2 - | Is_accu, Is_accu -> true | Cast_accu, Cast_accu -> true | Upd_cofix, Upd_cofix -> true | Force_cofix, Force_cofix -> true @@ -345,7 +343,6 @@ let primitive_hash = function combinesmall 8 (Int.hash i) | Mk_var id -> combinesmall 9 (Id.hash id) - | Is_accu -> 10 | Is_int -> 11 | Cast_accu -> 12 | Upd_cofix -> 13 @@ -396,6 +393,7 @@ type mllambda = | MLsetref of string * mllambda | MLsequence of mllambda * mllambda | MLarray of mllambda array + | MLisaccu of string * inductive * mllambda and mllam_branches = ((constructor * lname option array) list * mllambda) array @@ -467,7 +465,12 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 = | MLarray arr1, MLarray arr2 -> Array.equal (eq_mllambda gn1 gn2 n env1 env2) arr1 arr2 - | _, _ -> false + | MLisaccu (s1, ind1, ml1), MLisaccu (s2, ind2, ml2) -> + String.equal s1 s2 && eq_ind ind1 ind2 && + eq_mllambda gn1 gn2 n env1 env2 ml1 ml2 + | (MLlocal _ | MLglobal _ | MLprimitive _ | MLlam _ | MLletrec _ | MLlet _ | + MLapp _ | MLif _ | MLmatch _ | MLconstruct _ | MLint _ | MLuint _ | + MLsetref _ | MLsequence _ | MLarray _ | MLisaccu _), _ -> false and eq_letrec gn1 gn2 n env1 env2 defs1 defs2 = let eq_def (_,args1,ml1) (_,args2,ml2) = @@ -542,6 +545,8 @@ let rec hash_mllambda gn n env t = combinesmall 14 (combine hml hml') | MLarray arr -> combinesmall 15 (hash_mllambda_array gn n env 1 arr) + | MLisaccu (s, ind, c) -> + combinesmall 16 (combine (String.hash s) (combine (ind_hash ind) (hash_mllambda gn n env c))) and hash_mllambda_letrec gn n env init defs = let hash_def (_,args,ml) = @@ -608,6 +613,7 @@ let fv_lam l = | MLsetref(_,l) -> aux l bind fv | MLsequence(l1,l2) -> aux l1 bind (aux l2 bind fv) | MLarray arr -> Array.fold_right (fun a fv -> aux a bind fv) arr fv + | MLisaccu (_, _, body) -> aux body bind fv in aux l LNset.empty LNset.empty @@ -1142,7 +1148,7 @@ let ml_of_instance instance u = mkMLapp (MLapp (MLglobal cn, fv_args env fvn fvr)) [|force|] | Lif(t,bt,bf) -> MLif(ml_of_lam env l t, ml_of_lam env l bt, ml_of_lam env l bf) - | Lfix ((rec_pos,start), (ids, tt, tb)) -> + | Lfix ((rec_pos, inds, start), (ids, tt, tb)) -> (* let type_f fvt = [| type fix |] let norm_f1 fv f1 .. fn params1 = body1 .. @@ -1211,8 +1217,9 @@ let ml_of_instance instance u = let paramsi = t_params.(i) in let reci = MLlocal (paramsi.(rec_pos.(i))) in let pargsi = Array.map (fun id -> MLlocal id) paramsi in + let (prefix, ind) = inds.(i) in let body = - MLif(MLapp(MLprimitive Is_accu,[|reci|]), + MLif(MLisaccu (prefix, ind, reci), mkMLapp (MLapp(MLprimitive (Mk_fix(rec_pos,i)), [|mk_type; mk_norm|])) @@ -1374,6 +1381,7 @@ let subst s l = | MLsetref(s,l1) -> MLsetref(s,aux l1) | MLsequence(l1,l2) -> MLsequence(aux l1, aux l2) | MLarray arr -> MLarray (Array.map aux arr) + | MLisaccu (s, ind, l) -> MLisaccu (s, ind, aux l) in aux l @@ -1471,7 +1479,7 @@ let optimize gdef l = let b1 = optimize s b1 in let b2 = optimize s b2 in begin match t, b2 with - | MLapp(MLprimitive Is_accu,[| l1 |]), MLmatch(annot, l2, _, bs) + | MLisaccu (_, _, l1), MLmatch(annot, l2, _, bs) when eq_mllambda l1 l2 -> MLmatch(annot, l1, b1, bs) | _, _ -> MLif(t, b1, b2) end @@ -1483,6 +1491,7 @@ let optimize gdef l = | MLsetref(r,l) -> MLsetref(r, optimize s l) | MLsequence(l1,l2) -> MLsequence(optimize s l1, optimize s l2) | MLarray arr -> MLarray (Array.map (optimize s) arr) + | MLisaccu (pf, ind, l) -> MLisaccu (pf, ind, optimize s l) in optimize LNmap.empty l @@ -1645,7 +1654,11 @@ let pp_mllam fmt l = pp_mllam fmt arr.(len-1) end; Format.fprintf fmt "|]@]" - + | MLisaccu (prefix, (mind, i), c) -> + let accu = Format.sprintf "%sAccu_%s_%i" prefix (string_of_mind mind) i in + Format.fprintf fmt + "@[begin match Obj.magic (%a) with@\n| %s _ ->@\n true@\n| _ ->@\n false@\nend@]" + pp_mllam c accu and pp_letrec fmt defs = let len = Array.length defs in @@ -1738,7 +1751,6 @@ let pp_mllam fmt l = | Mk_var id -> Format.fprintf fmt "mk_var_accu (Names.id_of_string \"%s\")" (string_of_id id) | Mk_proj -> Format.fprintf fmt "mk_proj_accu" - | Is_accu -> Format.fprintf fmt "is_accu" | Is_int -> Format.fprintf fmt "is_int" | Cast_accu -> Format.fprintf fmt "cast_accu" | Upd_cofix -> Format.fprintf fmt "upd_cofix" @@ -1884,7 +1896,7 @@ let compile_constant env sigma prefix ~interactive con cb = let t = Mod_subst.force_constr t in let code = lambda_of_constr env sigma t in if !Flags.debug then Feedback.msg_debug (Pp.str "Generated lambda code"); - let is_lazy = is_lazy prefix t in + let is_lazy = is_lazy env prefix t in let code = if is_lazy then mk_lazy code else code in let name = if interactive then LinkedInteractive prefix @@ -1968,8 +1980,7 @@ let compile_mind mb mind stack = (MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc in let constructors = Array.fold_left_i add_construct [] ob.mind_reloc_tbl in - let add_proj j acc pb = - let () = assert (eq_ind ind pb.proj_ind) in + let add_proj proj_arg acc pb = let tbl = ob.mind_reloc_tbl in (* Building info *) let ci = { ci_ind = ind; ci_npar = nparams; @@ -1983,14 +1994,14 @@ let compile_mind mb mind stack = let _, arity = tbl.(0) in let ci_uid = fresh_lname Anonymous in let cargs = Array.init arity - (fun i -> if Int.equal i pb.proj_arg then Some ci_uid else None) + (fun i -> if Int.equal i proj_arg then Some ci_uid else None) in let i = push_symbol (SymbProj (ind, j)) in let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in let accu_br = MLapp (MLprimitive Mk_proj, [|get_proj_code i;accu|]) in let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in - let gn = Gproj ("", ind, pb.proj_arg) in + let gn = Gproj ("", ind, proj_arg) in Glet (gn, mkMLlam [|c_uid|] code) :: acc in let projs = match mb.mind_record with @@ -2058,8 +2069,7 @@ let compile_deps env sigma prefix ~interactive init t = comp_stack, (mind_updates, const_updates) | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind | Proj (p,c) -> - let pb = lookup_projection p env in - let init = compile_mind_deps env prefix ~interactive init (fst pb.proj_ind) in + let init = compile_mind_deps env prefix ~interactive init (Projection.mind p) in aux env lvl init c | Case (ci, p, c, ac) -> let mind = fst ci.ci_ind in diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index e97dbd0d67..931b8bbc86 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -135,7 +135,18 @@ and conv_fix env lvl t1 f1 t2 f2 cu = else aux (i+1) (conv_val env CONV flvl fi1 fi2 cu) in aux 0 cu +let warn_no_native_compiler = + let open Pp in + CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler" + (fun () -> strbrk "Native compiler is disabled," ++ + strbrk " falling back to VM conversion test.") + let native_conv_gen pb sigma env univs t1 t2 = + if not Coq_config.native_compiler then begin + warn_no_native_compiler (); + Vconv.vm_conv_gen pb env univs t1 t2 + end + else let ml_filename, prefix = get_ml_filename () in let code, upds = mk_conv_code env sigma prefix t1 t2 in match compile ml_filename code ~profile:false with @@ -152,19 +163,8 @@ let native_conv_gen pb sigma env univs t1 t2 = end | _ -> anomaly (Pp.str "Compilation failure.") -let warn_no_native_compiler = - let open Pp in - CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler" - (fun () -> strbrk "Native compiler is disabled," ++ - strbrk " falling back to VM conversion test.") - (* Wrapper for [native_conv] above *) let native_conv cv_pb sigma env t1 t2 = - if not Coq_config.native_compiler then begin - warn_no_native_compiler (); - Vconv.vm_conv cv_pb env t1 t2 - end - else let univs = Environ.universes env in let b = if cv_pb = CUMUL then Constr.leq_constr_univs univs t1 t2 diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index eaad8ee0c2..5075bd3d14 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -36,7 +36,7 @@ and lambda = | Lcase of annot_sw * lambda * lambda * lam_branches (* annotations, term being matched, accu, branches *) | Lif of lambda * lambda * lambda - | Lfix of (int array * int) * fix_decl + | Lfix of (int array * (string * inductive) array * int) * fix_decl | Lcofix of int * fix_decl (* must be in eta-expanded form *) | Lmakeblock of prefix * pconstructor * int * lambda array (* prefix, constructor name, constructor tag, arguments *) diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 5843cd5434..cec0ee57d5 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -333,54 +333,13 @@ let rec get_alias env (kn, u as p) = (*i Global environment *) -let global_env = ref empty_env - -let set_global_env env = global_env := env - 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 Int.equal 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 invalid_arg "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 invalid_arg "Vect.get:index out of bounds"; - v.elems.(v.size - n - 1) - - end - let empty_args = [||] -module Renv = +module Cache = struct module ConstrHash = @@ -394,45 +353,20 @@ module Renv = type constructor_info = tag * int * int (* nparam nrealargs *) - type t = { - name_rel : Name.t Vect.t; - construct_tbl : constructor_info ConstrTable.t; - - } - - - let make () = { - name_rel = Vect.make 16 Anonymous; - construct_tbl = ConstrTable.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 ConstrTable.find env.construct_tbl c + let get_construct_info cache env c : constructor_info = + try ConstrTable.find cache c with Not_found -> let ((mind,j), i) = c in - let oib = lookup_mind mind !global_env in + let oib = lookup_mind mind env in let oip = oib.mind_packets.(j) in let tag,arity = oip.mind_reloc_tbl.(i-1) in let nparams = oib.mind_nparams in let r = (tag, nparams, arity) in - ConstrTable.add env.construct_tbl c r; + ConstrTable.add cache c r; r end -let is_lazy prefix t = +let is_lazy env prefix t = match kind t with | App (f,args) -> begin match kind f with @@ -440,7 +374,7 @@ let is_lazy prefix t = let entry = mkInd (fst c) in (try let _ = - Retroknowledge.get_native_before_match_info (!global_env).retroknowledge + Retroknowledge.get_native_before_match_info env.retroknowledge entry prefix c Llazy; in false @@ -463,73 +397,84 @@ let empty_evars = let empty_ids = [||] -let rec lambda_of_constr env sigma c = +(** Extract the inductive type over which a fixpoint is decreasing *) +let rec get_fix_struct env i t = match kind (Reduction.whd_all env t) with +| Prod (na, dom, t) -> + if Int.equal i 0 then + let dom = Reduction.whd_all env dom in + let (dom, _) = decompose_appvect dom in + match kind dom with + | Ind (ind, _) -> ind + | _ -> assert false + else + let env = Environ.push_rel (RelDecl.LocalAssum (na, dom)) env in + get_fix_struct env (i - 1) t +| _ -> assert false + +let rec lambda_of_constr cache env sigma c = match kind c with | Meta mv -> let ty = meta_type sigma mv in - Lmeta (mv, lambda_of_constr env sigma ty) + Lmeta (mv, lambda_of_constr cache env sigma ty) | Evar (evk,args as ev) -> (match evar_value sigma ev with | None -> let ty = evar_type sigma ev in - let args = Array.map (lambda_of_constr env sigma) args in - Levar(evk, lambda_of_constr env sigma ty, args) - | Some t -> lambda_of_constr env sigma t) + let args = Array.map (lambda_of_constr cache env sigma) args in + Levar(evk, lambda_of_constr cache env sigma ty, args) + | Some t -> lambda_of_constr cache env sigma t) - | Cast (c, _, _) -> lambda_of_constr env sigma c + | Cast (c, _, _) -> lambda_of_constr cache env sigma c - | Rel i -> Renv.get env i + | Rel i -> Lrel (RelDecl.get_name (Environ.lookup_rel i env), i) | Var id -> Lvar id | Sort s -> Lsort s | Ind (ind,u as pind) -> - let prefix = get_mind_prefix !global_env (fst ind) in + let prefix = get_mind_prefix env (fst ind) in Lind (prefix, pind) | Prod(id, dom, codom) -> - let ld = lambda_of_constr env sigma dom in - Renv.push_rel env id; - let lc = lambda_of_constr env sigma codom in - Renv.pop env; + let ld = lambda_of_constr cache env sigma dom in + let env = Environ.push_rel (RelDecl.LocalAssum (id, dom)) env in + let lc = lambda_of_constr cache env sigma codom in Lprod(ld, Llam([|id|], lc)) | Lambda _ -> let params, body = Term.decompose_lam c in + let fold (na, t) env = Environ.push_rel (RelDecl.LocalAssum (na, t)) env in + let env = List.fold_right fold params env in + let lb = lambda_of_constr cache env sigma body in let ids = get_names (List.rev params) in - Renv.push_rels env ids; - let lb = lambda_of_constr env sigma body in - Renv.popn env (Array.length ids); mkLlam ids lb - | LetIn(id, def, _, body) -> - let ld = lambda_of_constr env sigma def in - Renv.push_rel env id; - let lb = lambda_of_constr env sigma body in - Renv.pop env; + | LetIn(id, def, t, body) -> + let ld = lambda_of_constr cache env sigma def in + let env = Environ.push_rel (RelDecl.LocalDef (id, def, t)) env in + let lb = lambda_of_constr cache env sigma body in Llet(id, ld, lb) - | App(f, args) -> lambda_of_app env sigma f args + | App(f, args) -> lambda_of_app cache env sigma f args - | Const _ -> lambda_of_app env sigma c empty_args + | Const _ -> lambda_of_app cache env sigma c empty_args - | Construct _ -> lambda_of_app env sigma c empty_args + | Construct _ -> lambda_of_app cache env sigma c empty_args | Proj (p, c) -> - let pb = lookup_projection p !global_env in - let ind = pb.proj_ind in - let prefix = get_mind_prefix !global_env (fst ind) in - mkLapp (Lproj (prefix, ind, pb.proj_arg)) [|lambda_of_constr env sigma c|] + let ind = Projection.inductive p in + let prefix = get_mind_prefix env (fst ind) in + mkLapp (Lproj (prefix, ind, Projection.arg p)) [|lambda_of_constr cache env sigma c|] | Case(ci,t,a,branches) -> let (mind,i as ind) = ci.ci_ind in - let mib = lookup_mind mind !global_env in + let mib = lookup_mind mind env in let oib = mib.mind_packets.(i) in let tbl = oib.mind_reloc_tbl in (* Building info *) - let prefix = get_mind_prefix !global_env mind in + let prefix = get_mind_prefix env mind in let annot_sw = { asw_ind = ind; asw_ci = ci; @@ -538,21 +483,21 @@ let rec lambda_of_constr env sigma c = asw_prefix = prefix} in (* translation of the argument *) - let la = lambda_of_constr env sigma a in + let la = lambda_of_constr cache env sigma a in let entry = mkInd ind in let la = try - Retroknowledge.get_native_before_match_info (!global_env).retroknowledge + Retroknowledge.get_native_before_match_info (env).retroknowledge entry prefix (ind,1) la with Not_found -> la in (* translation of the type *) - let lt = lambda_of_constr env sigma t in + let lt = lambda_of_constr cache env sigma t in (* translation of branches *) let mk_branch i b = let cn = (ind,i+1) in let _, arity = tbl.(i) in - let b = lambda_of_constr env sigma b in + let b = lambda_of_constr cache env sigma b in if Int.equal arity 0 then (cn, empty_ids, b) else match b with @@ -565,86 +510,90 @@ let rec lambda_of_constr env sigma c = let bs = Array.mapi mk_branch branches in Lcase(annot_sw, lt, la, bs) - | Fix(rec_init,(names,type_bodies,rec_bodies)) -> - let ltypes = lambda_of_args env sigma 0 type_bodies in - Renv.push_rels env names; - let lbodies = lambda_of_args env sigma 0 rec_bodies in - Renv.popn env (Array.length names); - Lfix(rec_init, (names, ltypes, lbodies)) + | Fix((pos, i), (names,type_bodies,rec_bodies)) -> + let ltypes = lambda_of_args cache env sigma 0 type_bodies in + let map i t = + let ind = get_fix_struct env i t in + let prefix = get_mind_prefix env (fst ind) in + (prefix, ind) + in + let inds = Array.map2 map pos type_bodies in + let env = Environ.push_rec_types (names, type_bodies, rec_bodies) env in + let lbodies = lambda_of_args cache env sigma 0 rec_bodies in + Lfix((pos, inds, i), (names, ltypes, lbodies)) | CoFix(init,(names,type_bodies,rec_bodies)) -> - let rec_bodies = Array.map2 (Reduction.eta_expand !global_env) rec_bodies type_bodies in - let ltypes = lambda_of_args env sigma 0 type_bodies in - Renv.push_rels env names; - let lbodies = lambda_of_args env sigma 0 rec_bodies in - Renv.popn env (Array.length names); + let rec_bodies = Array.map2 (Reduction.eta_expand env) rec_bodies type_bodies in + let ltypes = lambda_of_args cache env sigma 0 type_bodies in + let env = Environ.push_rec_types (names, type_bodies, rec_bodies) env in + let lbodies = lambda_of_args cache env sigma 0 rec_bodies in Lcofix(init, (names, ltypes, lbodies)) -and lambda_of_app env sigma f args = +and lambda_of_app cache env sigma f args = match kind f with | Const (kn,u as c) -> - let kn,u = get_alias !global_env c in - let cb = lookup_constant kn !global_env in + let kn,u = get_alias env c in + let cb = lookup_constant kn env in (try - let prefix = get_const_prefix !global_env kn in + let prefix = get_const_prefix env kn in (* We delay the compilation of arguments to avoid an exponential behavior *) let f = Retroknowledge.get_native_compiling_info - (!global_env).retroknowledge (mkConst kn) prefix in - let args = lambda_of_args env sigma 0 args in + (env).retroknowledge (mkConst kn) prefix in + let args = lambda_of_args cache env sigma 0 args in f args with Not_found -> begin match cb.const_body with | Def csubst -> (* TODO optimize if f is a proj and argument is known *) if cb.const_inline_code then - lambda_of_app env sigma (Mod_subst.force_constr csubst) args + lambda_of_app cache env sigma (Mod_subst.force_constr csubst) args else - let prefix = get_const_prefix !global_env kn in + let prefix = get_const_prefix env kn in let t = - if is_lazy prefix (Mod_subst.force_constr csubst) then + if is_lazy env prefix (Mod_subst.force_constr csubst) then mkLapp Lforce [|Lconst (prefix, (kn,u))|] else Lconst (prefix, (kn,u)) in - mkLapp t (lambda_of_args env sigma 0 args) + mkLapp t (lambda_of_args cache env sigma 0 args) | OpaqueDef _ | Undef _ -> - let prefix = get_const_prefix !global_env kn in - mkLapp (Lconst (prefix, (kn,u))) (lambda_of_args env sigma 0 args) + let prefix = get_const_prefix env kn in + mkLapp (Lconst (prefix, (kn,u))) (lambda_of_args cache env sigma 0 args) end) | Construct (c,u) -> - let tag, nparams, arity = Renv.get_construct_info env c in + let tag, nparams, arity = Cache.get_construct_info cache env c in let expected = nparams + arity in let nargs = Array.length args in - let prefix = get_mind_prefix !global_env (fst (fst c)) in + let prefix = get_mind_prefix env (fst (fst c)) in if Int.equal nargs expected then try try Retroknowledge.get_native_constant_static_info - (!global_env).retroknowledge + (env).retroknowledge f args with NotClosed -> assert (Int.equal nparams 0); (* should be fine for int31 *) - let args = lambda_of_args env sigma nparams args in + let args = lambda_of_args cache env sigma nparams args in Retroknowledge.get_native_constant_dynamic_info - (!global_env).retroknowledge f prefix c args + (env).retroknowledge f prefix c args with Not_found -> - let args = lambda_of_args env sigma nparams args in - makeblock !global_env c u tag args + let args = lambda_of_args cache env sigma nparams args in + makeblock env c u tag args else - let args = lambda_of_args env sigma 0 args in + let args = lambda_of_args cache env sigma 0 args in (try Retroknowledge.get_native_constant_dynamic_info - (!global_env).retroknowledge f prefix c args + (env).retroknowledge f prefix c args with Not_found -> mkLapp (Lconstruct (prefix, (c,u))) args) | _ -> - let f = lambda_of_constr env sigma f in - let args = lambda_of_args env sigma 0 args in + let f = lambda_of_constr cache env sigma f in + let args = lambda_of_args cache env sigma 0 args in mkLapp f args -and lambda_of_args env sigma start args = +and lambda_of_args cache env sigma start args = let nargs = Array.length args in if start < nargs then Array.init (nargs - start) - (fun i -> lambda_of_constr env sigma args.(start + i)) + (fun i -> lambda_of_constr cache env sigma args.(start + i)) else empty_args let optimize lam = @@ -657,11 +606,8 @@ let optimize lam = lam let lambda_of_constr env sigma c = - set_global_env env; - let env = Renv.make () in - let ids = List.rev_map RelDecl.get_name (rel_context !global_env) in - Renv.push_rels env (Array.of_list ids); - let lam = lambda_of_constr env sigma c in + let cache = Cache.ConstrTable.create 91 in + let lam = lambda_of_constr cache env sigma c in (* if Flags.vm_draw_opt () then begin (msgerrnl (str "Constr = \n" ++ pr_constr c);flush_all()); (msgerrnl (str "Lambda = \n" ++ pp_lam lam);flush_all()); diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 26bfeb7e0e..efe1700cd7 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -23,7 +23,7 @@ val empty_evars : evars val decompose_Llam : lambda -> Name.t array * lambda val decompose_Llam_Llet : lambda -> (Name.t * lambda option) array * lambda -val is_lazy : prefix -> constr -> bool +val is_lazy : env -> prefix -> constr -> bool val mk_lazy : lambda -> lambda val get_mind_prefix : env -> MutInd.t -> string diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 31ad364911..f784509b6f 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -67,6 +67,7 @@ let warn_native_compiler_failed = CWarnings.create ~name:"native-compiler-failed" ~category:"native-compiler" print let call_compiler ?profile:(profile=false) ml_filename = + let () = assert Coq_config.native_compiler in let load_path = !get_load_paths () in let load_path = List.map (fun dn -> dn / output_dir) load_path in let include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (include_dirs () @ load_path)) in diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 3901cb9ce4..91f6add1c3 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -68,28 +68,29 @@ type atom = let accumulate_tag = 0 -let accumulate_code (k:accumulator) (x:t) = - let o = Obj.repr k in - let osize = Obj.size o in - let r = Obj.new_block accumulate_tag (osize + 1) in - for i = 0 to osize - 1 do - Obj.set_field r i (Obj.field o i) - done; - Obj.set_field r osize (Obj.repr x); - (Obj.obj r:t) - -let rec accumulate (x:t) = - accumulate_code (Obj.magic accumulate) x - -let mk_accu_gen rcode (a:atom) = -(* Format.eprintf "size rcode =%i\n" (Obj.size (Obj.magic rcode)); *) - let r = Obj.new_block 0 3 in - Obj.set_field r 0 (Obj.field (Obj.magic rcode) 0); - Obj.set_field r 1 (Obj.field (Obj.magic rcode) 1); - Obj.set_field r 2 (Obj.magic a); - (Obj.magic r:t);; - -let mk_accu (a:atom) = mk_accu_gen accumulate a +(** Unique pointer used to drive the accumulator function *) +let ret_accu = Obj.repr (ref ()) + +type accu_val = { mutable acc_atm : atom; acc_arg : Obj.t list } + +let mk_accu (a : atom) : t = + let rec accumulate data x = + if x == ret_accu then Obj.repr data + else + let data = { data with acc_arg = x :: data.acc_arg } in + let ans = Obj.repr (accumulate data) in + let () = Obj.set_tag ans accumulate_tag in + ans + in + let acc = { acc_atm = a; acc_arg = [] } in + let ans = Obj.repr (accumulate acc) in + (** FIXME: use another representation for accumulators, this causes naked + pointers. *) + let () = Obj.set_tag ans accumulate_tag in + (Obj.obj ans : t) + +let get_accu (k : accumulator) = + (Obj.magic k : Obj.t -> accu_val) ret_accu let mk_rel_accu i = mk_accu (Arel i) @@ -141,31 +142,27 @@ let mk_proj_accu kn c = mk_accu (Aproj (kn,c)) let atom_of_accu (k:accumulator) = - (Obj.magic (Obj.field (Obj.magic k) 2) : atom) + (get_accu k).acc_atm let set_atom_of_accu (k:accumulator) (a:atom) = - Obj.set_field (Obj.magic k) 2 (Obj.magic a) + (get_accu k).acc_atm <- a let accu_nargs (k:accumulator) = - let nargs = Obj.size (Obj.magic k) - 3 in -(* if nargs < 0 then Format.eprintf "nargs = %i\n" nargs; *) - assert (nargs >= 0); - nargs + List.length (get_accu k).acc_arg let args_of_accu (k:accumulator) = - let nargs = accu_nargs k in - let f i = (Obj.magic (Obj.field (Obj.magic k) (nargs-i+2)) : t) in - Array.init nargs f + let acc = (get_accu k).acc_arg in + (Obj.magic (Array.of_list acc) : t array) let is_accu x = let o = Obj.repr x in Obj.is_block o && Int.equal (Obj.tag o) accumulate_tag let mk_fix_accu rec_pos pos types bodies = - mk_accu_gen accumulate (Afix(types,bodies,rec_pos, pos)) + mk_accu (Afix(types,bodies,rec_pos, pos)) let mk_cofix_accu pos types norm = - mk_accu_gen accumulate (Acofix(types,norm,pos,(Obj.magic 0 : t))) + mk_accu (Acofix(types,norm,pos,(Obj.magic 0 : t))) let upd_cofix (cofix :t) (cofix_fun : t) = let atom = atom_of_accu (Obj.magic cofix) in diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 649853f069..6bbf15160c 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -110,9 +110,6 @@ type kind_of_value = val kind_of_value : t -> kind_of_value -(* *) -val is_accu : t -> bool - val str_encode : 'a -> string val str_decode : string -> 'a diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 3228a155f3..c701b53fe4 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -53,7 +53,7 @@ let compare_stack_shape stk1 stk2 = | (_, (Zupdate _|Zshift _)::s2) -> compare_rec bal stk1 s2 | (Zapp l1::s1, _) -> compare_rec (bal+Array.length l1) s1 stk2 | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2 - | (Zproj (n1,m1,p1)::s1, Zproj (n2,m2,p2)::s2) -> + | (Zproj p1::s1, Zproj p2::s2) -> Int.equal bal 0 && compare_rec 0 s1 s2 | (ZcaseT(c1,_,_,_)::s1, ZcaseT(c2,_,_,_)::s2) -> Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 @@ -66,7 +66,7 @@ let compare_stack_shape stk1 stk2 = type lft_constr_stack_elt = Zlapp of (lift * fconstr) array - | Zlproj of Constant.t * lift + | Zlproj of Projection.Repr.t * lift | Zlfix of (lift * fconstr) * lft_constr_stack | Zlcase of case_info * lift * fconstr * fconstr array and lft_constr_stack = lft_constr_stack_elt list @@ -96,8 +96,8 @@ let pure_stack lfts stk = | (Zshift n,(l,pstk)) -> (el_shft n l, pstk) | (Zapp a, (l,pstk)) -> (l,zlapp (map_lift l a) pstk) - | (Zproj (n,m,c), (l,pstk)) -> - (l, Zlproj (c,l)::pstk) + | (Zproj p, (l,pstk)) -> + (l, Zlproj (p,l)::pstk) | (Zfix(fx,a),(l,pstk)) -> let (lfx,pa) = pure_rec l a in (l, Zlfix((lfx,fx),pa)::pstk) @@ -297,7 +297,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv = | (Zlapp a1,Zlapp a2) -> Array.fold_right2 f a1 a2 cu1 | (Zlproj (c1,l1),Zlproj (c2,l2)) -> - if not (Constant.equal c1 c2) then + if not (Projection.Repr.equal c1 c2) then raise NotConvertible else cu1 | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> @@ -408,7 +408,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | Some s2 -> eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv | None -> - if Constant.equal (Projection.constant p1) (Projection.constant p2) + if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2) && compare_stack_shape v1 v2 then let el1 = el_stack lft1 v1 in let el2 = el_stack lft2 v2 in diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index d76b05a8bb..34f62defb8 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -25,22 +25,6 @@ open Constr (* aliased type for clarity purpose*) type entry = Constr.t -(* [field]-s are the roles the kernel can learn of. *) -type nat_field = - | NatType - | NatPlus - | NatTimes - -type n_field = - | NPositive - | NType - | NTwice - | NTwicePlusOne - | NPhi - | NPhiInv - | NPlus - | NTimes - type int31_field = | Int31Bits | Int31Type @@ -69,9 +53,6 @@ type int31_field = | Int31Lxor type field = - (* | KEq - | KNat of nat_field - | KN of n_field *) | KInt31 of string*int31_field diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 281c37b851..02d961d893 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -18,21 +18,6 @@ type entry = Constr.t (** the following types correspond to the different "things" the kernel can learn about.*) -type nat_field = - | NatType - | NatPlus - | NatTimes - -type n_field = - | NPositive - | NType - | NTwice - | NTwicePlusOne - | NPhi - | NPhiInv - | NPlus - | NTimes - type int31_field = | Int31Bits | Int31Type @@ -61,13 +46,8 @@ type int31_field = | Int31Lxor type field = - -(** | KEq - | KNat of nat_field - | KN of n_field *) | KInt31 of string*int31_field - (** This type represent an atomic action of the retroknowledge. It is stored in the compiled libraries As per now, there is only the possibility of registering things diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 7c0057696e..7f36f3813f 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -296,13 +296,13 @@ let type_of_case env ci p pt c ct lf lft = rslty let type_of_projection env p c ct = - let pb = lookup_projection p env in + let pty = lookup_projection p env in let (ind,u), args = try find_rectype env ct with Not_found -> error_case_not_inductive env (make_judge c ct) in - assert(eq_ind pb.proj_ind ind); - let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in + assert(eq_ind (Projection.inductive p) ind); + let ty = Vars.subst_instance_constr u pty in substl (c :: CList.rev args) ty diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 4e4168922d..d19bea5199 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -139,7 +139,7 @@ and conv_stack env k stk1 stk2 cu = conv_stack env k stk1 stk2 !rcu else raise NotConvertible | Zproj p1 :: stk1, Zproj p2 :: stk2 -> - if Constant.equal p1 p2 then conv_stack env k stk1 stk2 cu + if Projection.Repr.equal p1 p2 then conv_stack env k stk1 stk2 cu else raise NotConvertible | [], _ | Zapp _ :: _, _ | Zfix _ :: _, _ | Zswitch _ :: _, _ | Zproj _ :: _, _ -> raise NotConvertible diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 8524c44d21..d6d9312938 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -150,7 +150,7 @@ type zipper = | Zapp of arguments | Zfix of vfix*arguments (* Possibly empty *) | Zswitch of vswitch - | Zproj of Constant.t (* name of the projection *) + | Zproj of Projection.Repr.t (* name of the projection *) type stack = zipper list @@ -354,7 +354,7 @@ 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" -external val_of_proj_name : Constant.t -> values = "%identity" +external val_of_proj_name : Projection.Repr.t -> values = "%identity" (*************************************************) (** Operations manipulating data types ***********) @@ -553,4 +553,4 @@ and pr_zipper z = | Zapp args -> str "Zapp(len = " ++ int (nargs args) ++ str ")" | Zfix (f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")" | Zswitch s -> str "Zswitch(...)" - | Zproj c -> str "Zproj(" ++ Constant.print c ++ str ")") + | Zproj c -> str "Zproj(" ++ Projection.Repr.print c ++ str ")") diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index 08d05a038c..6eedcf1d37 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -81,7 +81,7 @@ type zipper = | Zapp of arguments | Zfix of vfix * arguments (** might be empty *) | Zswitch of vswitch - | Zproj of Constant.t (* name of the projection *) + | Zproj of Projection.Repr.t (* name of the projection *) type stack = zipper list @@ -108,11 +108,11 @@ 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_proj : Projection.Repr.t -> values -> values val val_of_atom : atom -> values external val_of_annot_switch : annot_switch -> values = "%identity" -external val_of_proj_name : Constant.t -> values = "%identity" +external val_of_proj_name : Projection.Repr.t -> values = "%identity" (** Destructors *) |