diff options
Diffstat (limited to 'kernel')
37 files changed, 402 insertions, 377 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 1d8861cbc..1d5142a5c 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -587,78 +587,95 @@ let mk_clos_deep clos_fun env t = let mk_clos2 = mk_clos_deep mk_clos (* The inverse of mk_clos_deep: move back to constr *) -let rec to_constr constr_fun lfts v = +let rec to_constr lfts v = match v.term with | FRel i -> mkRel (reloc_rel i lfts) | FFlex (RelKey p) -> mkRel (reloc_rel p lfts) | FFlex (VarKey x) -> mkVar x | FAtom c -> exliftn lfts c | FCast (a,k,b) -> - mkCast (constr_fun lfts a, k, constr_fun lfts b) + mkCast (to_constr lfts a, k, to_constr lfts b) | FFlex (ConstKey op) -> mkConstU op | FInd op -> mkIndU op | FConstruct op -> mkConstructU op | FCaseT (ci,p,c,ve,env) -> - mkCase (ci, constr_fun lfts (mk_clos env p), - constr_fun lfts c, - Array.map (fun b -> constr_fun lfts (mk_clos env b)) ve) - | FFix ((op,(lna,tys,bds)),e) -> + if is_subs_id env && is_lift_id lfts then + mkCase (ci, p, to_constr lfts c, ve) + else + let subs = comp_subs lfts env in + mkCase (ci, subst_constr subs p, + to_constr lfts c, + Array.map (fun b -> subst_constr subs b) ve) + | FFix ((op,(lna,tys,bds)) as fx, e) -> + if is_subs_id e && is_lift_id lfts then + mkFix fx + else let n = Array.length bds in - let ftys = Array.Fun1.map mk_clos e tys in - let fbds = Array.Fun1.map mk_clos (subs_liftn n e) bds in - let lfts' = el_liftn n lfts in - mkFix (op, (lna, Array.Fun1.map constr_fun lfts ftys, - Array.Fun1.map constr_fun lfts' fbds)) - | FCoFix ((op,(lna,tys,bds)),e) -> + let subs_ty = comp_subs lfts e in + let subs_bd = comp_subs (el_liftn n lfts) (subs_liftn n e) in + let tys = Array.Fun1.map subst_constr subs_ty tys in + let bds = Array.Fun1.map subst_constr subs_bd bds in + mkFix (op, (lna, tys, bds)) + | FCoFix ((op,(lna,tys,bds)) as cfx, e) -> + if is_subs_id e && is_lift_id lfts then + mkCoFix cfx + else let n = Array.length bds in - let ftys = Array.Fun1.map mk_clos e tys in - let fbds = Array.Fun1.map mk_clos (subs_liftn n e) bds in - let lfts' = el_liftn (Array.length bds) lfts in - mkCoFix (op, (lna, Array.Fun1.map constr_fun lfts ftys, - Array.Fun1.map constr_fun lfts' fbds)) + let subs_ty = comp_subs lfts e in + let subs_bd = comp_subs (el_liftn n lfts) (subs_liftn n e) in + let tys = Array.Fun1.map subst_constr subs_ty tys in + let bds = Array.Fun1.map subst_constr subs_bd bds in + mkCoFix (op, (lna, tys, bds)) | FApp (f,ve) -> - mkApp (constr_fun lfts f, - Array.Fun1.map constr_fun lfts ve) + mkApp (to_constr lfts f, + Array.Fun1.map to_constr lfts ve) | FProj (p,c) -> - mkProj (p,constr_fun lfts c) + mkProj (p,to_constr lfts c) - | FLambda _ -> - let (na,ty,bd) = destFLambda mk_clos2 v in - mkLambda (na, constr_fun lfts ty, - constr_fun (el_lift lfts) bd) + | FLambda (len, tys, f, e) -> + if is_subs_id e && is_lift_id lfts then + Term.compose_lam (List.rev tys) f + else + let subs = comp_subs lfts e in + let tys = List.mapi (fun i (na, c) -> na, subst_constr (subs_liftn i subs) c) tys in + let f = subst_constr (subs_liftn len subs) f in + Term.compose_lam (List.rev tys) f | FProd (n,t,c) -> - mkProd (n, constr_fun lfts t, - constr_fun (el_lift lfts) c) + mkProd (n, to_constr lfts t, + to_constr (el_lift lfts) c) | FLetIn (n,b,t,f,e) -> - let fc = mk_clos2 (subs_lift e) f in - mkLetIn (n, constr_fun lfts b, - constr_fun lfts t, - constr_fun (el_lift lfts) fc) + let subs = comp_subs (el_lift lfts) (subs_lift e) in + mkLetIn (n, to_constr lfts b, + to_constr lfts t, + subst_constr subs f) | FEvar ((ev,args),env) -> - mkEvar(ev,Array.map (fun a -> constr_fun lfts (mk_clos2 env a)) args) - | FLIFT (k,a) -> to_constr constr_fun (el_shft k lfts) a + let subs = comp_subs lfts env in + mkEvar(ev,Array.map (fun a -> subst_constr subs a) args) + | FLIFT (k,a) -> to_constr (el_shft k lfts) a | FCLOS (t,env) -> - let fr = mk_clos2 env t in - let unfv = update v fr.norm fr.term in - to_constr constr_fun lfts unfv + if is_subs_id env && is_lift_id lfts then t + else + let subs = comp_subs lfts env in + subst_constr subs t | FLOCKED -> assert false (*mkVar(Id.of_string"_LOCK_")*) +and subst_constr subst c = match Constr.kind c with +| Rel i -> + begin match expand_rel i subst with + | Inl (k, lazy v) -> Vars.lift k v + | Inr (m, _) -> mkRel m + end +| _ -> + Constr.map_with_binders Esubst.subs_lift subst_constr subst c + +and comp_subs el s = + Esubst.lift_subst (fun el c -> lazy (to_constr el c)) el s + (* This function defines the correspondance between constr and fconstr. When we find a closure whose substitution is the identity, then we directly return the constr to avoid possibly huge reallocation. *) -let term_of_fconstr = - let rec term_of_fconstr_lift lfts v = - match v.term with - | FCLOS(t,env) when is_subs_id env && is_lift_id lfts -> t - | FLambda(_,tys,f,e) when is_subs_id e && is_lift_id lfts -> - Term.compose_lam (List.rev tys) f - | FFix(fx,e) when is_subs_id e && is_lift_id lfts -> mkFix fx - | FCoFix(cfx,e) when is_subs_id e && is_lift_id lfts -> mkCoFix cfx - | _ -> to_constr term_of_fconstr_lift lfts v in - term_of_fconstr_lift el_id - - +let term_of_fconstr c = to_constr el_id c (* fstrong applies unfreeze_fun recursively on the (freeze) term and * yields a term. Assumes that the unfreeze_fun never returns a @@ -803,10 +820,12 @@ let drop_parameters depth n argstk = constructor is partially applied. *) 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 - | Some (Some (_,projs,pbs)) when + | PrimRecord infos when mib.Declarations.mind_finite == Declarations.BiFinite -> + let (_, projs, _) = infos.(snd ind) in (* (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 @@ -817,7 +836,7 @@ let eta_expand_ind_stack env ind m s (f, s') = 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] - | _ -> raise Not_found (* disallow eta-exp for non-primitive records *) + | PrimRecord _ | NotRecord | FakeRecord -> raise Not_found (* disallow eta-exp for non-primitive records *) let rec project_nth_arg n argstk = match argstk with diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 63daa4a7c..f8f98f0ab 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -244,6 +244,6 @@ 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 +val to_constr : lift -> fconstr -> constr (** End of cbn debug section i*) diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 521f540d2..3095ce148 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -217,6 +217,7 @@ type vm_env = { type comp_env = { + arity : int; (* arity of the current function, 0 if none *) nb_uni_stack : int ; (* number of universes on the stack, *) (* universes are always at the bottom. *) nb_stack : int; (* number of variables on the stack *) @@ -235,8 +236,8 @@ open Util let pp_sort s = let open Sorts in match s with - | Prop Null -> str "Prop" - | Prop Pos -> str "Set" + | Prop -> str "Prop" + | Set -> str "Set" | Type u -> str "Type@{" ++ Univ.pr_uni u ++ str "}" let rec pp_struct_const = function diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 238edc0af..de21401b3 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -159,6 +159,7 @@ type vm_env = { type comp_env = { + arity : int; (* arity of the current function, 0 if none *) nb_uni_stack : int ; (** number of universes on the stack *) nb_stack : int; (** number of variables on the stack *) in_stack : int list; (** position in the stack *) diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 7a27a3d20..6677db2fd 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -112,8 +112,9 @@ let push_fv d e = { let fv r = !(r.in_env) -let empty_comp_env ?(univs=0) ()= - { nb_uni_stack = univs; +let empty_comp_env ()= + { arity = 0; + nb_uni_stack = 0; nb_stack = 0; in_stack = []; nb_rec = 0; @@ -148,7 +149,8 @@ let rec add_param n sz l = if Int.equal n 0 then l else add_param (n - 1) sz (n+sz::l) let comp_env_fun ?(univs=0) arity = - { nb_uni_stack = univs ; + { arity; + nb_uni_stack = univs ; nb_stack = arity; in_stack = add_param arity 0 []; nb_rec = 0; @@ -159,7 +161,8 @@ let comp_env_fun ?(univs=0) arity = let comp_env_fix_type rfv = - { nb_uni_stack = 0; + { arity = 0; + nb_uni_stack = 0; nb_stack = 0; in_stack = []; nb_rec = 0; @@ -173,7 +176,8 @@ let comp_env_fix ndef curr_pos arity rfv = for i = ndef downto 1 do prec := Koffsetclosure (2 * (ndef - curr_pos - i)) :: !prec done; - { nb_uni_stack = 0; + { arity; + nb_uni_stack = 0; nb_stack = arity; in_stack = add_param arity 0 []; nb_rec = ndef; @@ -183,7 +187,8 @@ let comp_env_fix ndef curr_pos arity rfv = } let comp_env_cofix_type ndef rfv = - { nb_uni_stack = 0; + { arity = 0; + nb_uni_stack = 0; nb_stack = 0; in_stack = []; nb_rec = 0; @@ -197,7 +202,8 @@ let comp_env_cofix ndef arity rfv = for i = 1 to ndef do prec := Kenvacc i :: !prec done; - { nb_uni_stack = 0; + { arity; + nb_uni_stack = 0; nb_stack = arity; in_stack = add_param arity 0 []; nb_rec = ndef; @@ -249,8 +255,15 @@ let pos_rel i r sz = Kenvacc(r.offset + pos) let pos_universe_var i r sz = - if i < r.nb_uni_stack then - Kacc (sz - r.nb_stack - (r.nb_uni_stack - i)) + (* Compilation of a universe variable can happen either at toplevel (the + current closure correspond to a constant and has local universes) or in a + local closure (which has no local universes). *) + if r.nb_uni_stack != 0 then + (* Universe variables are represented by De Bruijn levels (not indices), + starting at 0. The shape of the stack will be [v1|..|vn|u1..up|arg1..argq] + with size = n + p + q, and q = r.arity. So Kacc (sz - r.arity - 1) will access + the last universe. *) + Kacc (sz - r.arity - (r.nb_uni_stack - i)) else let env = !(r.in_env) in let db = FVuniv_var i in @@ -498,7 +511,7 @@ let rec compile_lam env cenv lam sz cont = else comp_app compile_structured_constant compile_universe cenv (Const_ind ind) (Univ.Instance.to_array u) sz cont - | Lsort (Sorts.Prop _ as s) -> + | Lsort (Sorts.Prop | Sorts.Set as s) -> compile_structured_constant cenv (Const_sort s) sz cont | Lsort (Sorts.Type u) -> (* We represent universes as a global constant with local universes diff --git a/kernel/clambda.ml b/kernel/clambda.ml index b722e4200..f1b6f3dff 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -814,7 +814,7 @@ let optimize_lambda 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 + let ids = List.rev_map Context.Rel.Declaration.get_name (rel_context genv) 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 diff --git a/kernel/constr.ml b/kernel/constr.ml index 418229330..45812b5a1 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -130,8 +130,8 @@ let mkProp = Sort Sorts.prop let mkSet = Sort Sorts.set let mkType u = Sort (Sorts.Type u) let mkSort = function - | Sorts.Prop Sorts.Null -> mkProp (* Easy sharing *) - | Sorts.Prop Sorts.Pos -> mkSet + | Sorts.Prop -> mkProp (* Easy sharing *) + | Sorts.Set -> mkSet | s -> Sort s (* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *) @@ -260,17 +260,17 @@ let isSort c = match kind c with | _ -> false let rec isprop c = match kind c with - | Sort (Sorts.Prop _) -> true + | Sort (Sorts.Prop | Sorts.Set) -> true | Cast (c,_,_) -> isprop c | _ -> false let rec is_Prop c = match kind c with - | Sort (Sorts.Prop Sorts.Null) -> true + | Sort Sorts.Prop -> true | Cast (c,_,_) -> is_Prop c | _ -> false let rec is_Set c = match kind c with - | Sort (Sorts.Prop Sorts.Pos) -> true + | Sort Sorts.Set -> true | Cast (c,_,_) -> is_Set c | _ -> false @@ -828,8 +828,10 @@ let leq_constr_univs_infer univs m n = let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in if UGraph.check_leq univs u1 u2 then true else - (cstrs := Univ.enforce_leq u1 u2 !cstrs; - true) + (try let c, _ = UGraph.enforce_leq_alg u1 u2 univs in + cstrs := Univ.Constraint.union c !cstrs; + true + with Univ.UniverseInconsistency _ -> false) in let rec eq_constr' nargs m n = m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 68057b389..c7a84f617 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -126,16 +126,15 @@ let expmod_constr cache modlist c = | Not_found -> Constr.map substrec c) | Proj (p, c') -> - (try - let p' = share_univs (ConstRef (Projection.constant p)) Univ.Instance.empty modlist in - let make c = Projection.make c (Projection.unfolded p) in - match kind p' with - | Const (p',_) -> mkProj (make p', substrec c') - | App (f, args) -> - (match kind f with - | Const (p', _) -> mkProj (make p', substrec c') - | _ -> assert false) - | _ -> assert false + (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) | _ -> Constr.map substrec c diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 7bd7d6c9c..58fb5d66b 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -50,7 +50,7 @@ type inline = int option always transparent. *) type projection_body = { - proj_ind : MutInd.t; + proj_ind : inductive; proj_npars : int; proj_arg : int; (** Projection index, starting from 0 *) proj_type : types; (* Type under params *) @@ -109,13 +109,22 @@ v} *) (** Record information: - If the record is not primitive, then None - Otherwise, we get: + If the type is not a record, then NotRecord + If the type is a non-primitive record, then FakeRecord + 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 checked projection bodies. -type record_body = (Id.t * Constant.t array * projection_body array) option + The kernel does not exploit the difference between [NotRecord] and + [FakeRecord]. It is mostly used by extraction, and should be extruded from + the kernel at some point. +*) + +type record_info = +| NotRecord +| FakeRecord +| PrimRecord of (Id.t * Constant.t array * projection_body array) array type regular_inductive_arity = { mind_user_arity : types; @@ -181,7 +190,7 @@ type mutual_inductive_body = { mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) - mind_record : record_body option; (** The record information *) + mind_record : record_info; (** The record information *) mind_finite : recursivity_kind; (** Whether the type is inductive or coinductive *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 1b73096f7..3e6c4858e 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -84,7 +84,7 @@ let subst_const_def sub def = match def with | OpaqueDef o -> OpaqueDef (Opaqueproof.subst_opaque sub o) let subst_const_proj sub pb = - { pb with proj_ind = subst_mind sub pb.proj_ind; + { pb with proj_ind = subst_ind sub pb.proj_ind; proj_type = subst_mps sub pb.proj_type; } @@ -208,14 +208,21 @@ let subst_mind_packet sub mbp = mind_nb_args = mbp.mind_nb_args; mind_reloc_tbl = mbp.mind_reloc_tbl } -let subst_mind_record sub (id, ps, pb as r) = - 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 r +let subst_mind_record sub r = match r with +| NotRecord -> NotRecord +| 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') + in + let infos' = Array.Smart.map map infos in + if infos' == infos then r else PrimRecord infos' let subst_mind_body sub mib = - { mind_record = Option.Smart.map (Option.Smart.map (subst_mind_record sub)) mib.mind_record ; + { mind_record = subst_mind_record sub mib.mind_record ; mind_finite = mib.mind_finite ; mind_ntypes = mib.mind_ntypes ; mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false); diff --git a/kernel/entries.ml b/kernel/entries.ml index 3c555f8c7..724ed9ec7 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -49,9 +49,9 @@ type one_inductive_entry = { mind_entry_lc : constr list } type mutual_inductive_entry = { - mind_entry_record : (Id.t option) option; - (** Some (Some id): primitive record with id the binder name of the record - in projections. + mind_entry_record : (Id.t array option) option; + (** Some (Some ids): primitive records with ids the binder name of each + record in their respective projections. Not used by the kernel. Some None: non-primitive record *) mind_entry_finite : Declarations.recursivity_kind; mind_entry_params : (Id.t * local_entry) list; diff --git a/kernel/environ.ml b/kernel/environ.ml index 2d6c9117b..224b6d5b8 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -55,7 +55,8 @@ type globals = { 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} + env_modtypes : module_type_body MPmap.t; +} type stratification = { env_universes : UGraph.t; @@ -86,7 +87,7 @@ type rel_context_val = { } type env = { - env_globals : globals; (* globals = constants + inductive types + modules + module-types *) + env_globals : globals; env_named_context : named_context_val; (* section variables *) env_rel_context : rel_context_val; env_nb_rel : int; @@ -208,6 +209,9 @@ let lookup_named_val id env = let lookup_named_ctxt id ctxt = fst (Id.Map.find id ctxt.env_named_map) +let fold_constants f env acc = + Cmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_constants acc + (* Global constants *) let lookup_constant_key kn env = @@ -515,11 +519,12 @@ 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 - | None | Some None -> env.env_globals.env_projections - | Some (Some (id, kns, pbs)) -> - Array.fold_left2 (fun projs kn pb -> - Cmap_env.add kn pb projs) - env.env_globals.env_projections kns pbs + | 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 diff --git a/kernel/environ.mli b/kernel/environ.mli index 8928b32f1..084d3c4de 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -46,13 +46,8 @@ type constant_key = constant_body * (link_info ref * key) 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 -} +type globals +(** globals = constants + projections + inductive types + modules + module-types *) type stratification = { env_universes : UGraph.t; @@ -70,7 +65,7 @@ type rel_context_val = private { } type env = private { - env_globals : globals; (* globals = constants + inductive types + modules + module-types *) + env_globals : globals; env_named_context : named_context_val; (* section variables *) env_rel_context : rel_context_val; env_nb_rel : int; @@ -175,6 +170,9 @@ val reset_with_named_context : named_context_val -> env -> env (** This removes the [n] last declarations from the rel context *) val pop_rel_context : int -> env -> env +(** Useful for printing *) +val fold_constants : (Constant.t -> constant_body -> 'a -> 'a) -> env -> 'a -> 'a + (** {5 Global constants } {6 Add entries to global environment } *) @@ -320,6 +318,7 @@ open Retroknowledge (** functions manipulating the retroknowledge @author spiwack *) val retroknowledge : (retroknowledge->'a) -> env -> 'a +[@@ocaml.deprecated "Use the record projection."] val registered : env -> field -> bool diff --git a/kernel/esubst.ml b/kernel/esubst.ml index 4b8edf63f..9fc3b11d7 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -134,6 +134,29 @@ let rec exp_rel lams k subs = let expand_rel k subs = exp_rel 0 k subs +let rec subs_map f = function +| ESID _ as s -> s +| CONS (x, s) -> CONS (Array.map f x, subs_map f s) +| SHIFT (n, s) -> SHIFT (n, subs_map f s) +| LIFT (n, s) -> LIFT (n, subs_map f s) + +let rec lift_subst mk_cl s1 s2 = match s1 with +| ELID -> subs_map (fun c -> mk_cl ELID c) s2 +| ELSHFT(s, k) -> subs_shft(k, lift_subst mk_cl s s2) +| ELLFT (k, s) -> + match s2 with + | CONS(x,s') -> + CONS(CArray.Fun1.map mk_cl s1 x, lift_subst mk_cl s1 s') + | ESID n -> lift_subst mk_cl s (ESID (n + k)) + | SHIFT(k',s') -> + if k<k' + then subs_shft(k, lift_subst mk_cl s (subs_shft(k'-k, s'))) + else subs_shft(k', lift_subst mk_cl (el_liftn (k-k') s) s') + | LIFT(k',s') -> + if k<k' + then subs_liftn k (lift_subst mk_cl s (subs_liftn (k'-k) s')) + else subs_liftn k' (lift_subst mk_cl (el_liftn (k-k') s) s') + let rec comp mk_cl s1 s2 = match (s1, s2) with | _, ESID _ -> s1 diff --git a/kernel/esubst.mli b/kernel/esubst.mli index a674c425a..475b64f47 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.mli @@ -72,3 +72,10 @@ val el_liftn : int -> lift -> lift val el_lift : lift -> lift val reloc_rel : int -> lift -> int val is_lift_id : lift -> bool + +(** Lift applied to substitution: [lift_subst mk_clos el s] computes a + substitution equivalent to applying el then s. Argument + mk_clos is used when a closure has to be created, i.e. when + el is applied on an element of s. +*) +val lift_subst : (lift -> 'a -> 'b) -> lift -> 'a subs -> 'b subs diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 14f2a3d8f..e63f43849 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -797,15 +797,23 @@ exception UndefinableExpansion build an expansion function. The term built is expecting to be substituted first by a substitution of the form [params, x : ind params] *) -let compute_projections ((kn, _ as ind), u) nparamargs params - mind_consnrealdecls mind_consnrealargs paramslet ctx = +let compute_projections (kn, i as ind) mib = + let pkt = mib.mind_packets.(i) in + let u = match mib.mind_universes with + | Monomorphic_ind _ -> Univ.Instance.empty + | Polymorphic_ind auctx -> Univ.make_abstract_instance auctx + | Cumulative_ind acumi -> Univ.make_abstract_instance (Univ.ACumulativityInfo.univ_context acumi) + in + 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. *) let paramsletsubst = (* [Ind inst] is typed in context [params-wo-let] *) - let inst' = rel_list 0 nparamargs in + let inst' = rel_list 0 mib.mind_nparams in (* {params-wo-let |- subst:params] *) let subst = subst_of_rel_context_instance paramslet inst' in (* {params-wo-let, x:Ind inst' |- subst':(params,x:Ind inst)] *) @@ -839,7 +847,7 @@ let compute_projections ((kn, _ as ind), u) nparamargs params (* 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 = fst ind; proj_npars = nparamargs; + 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) | Anonymous -> raise UndefinableExpansion @@ -932,33 +940,9 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r mind_reloc_tbl = rtbl; } in let packets = Array.map2 build_one_packet inds recargs in - let pkt = packets.(0) in - let isrecord = - match isrecord with - | Some (Some rid) when pkt.mind_kelim == all_sorts - && Array.length pkt.mind_consnames == 1 - && pkt.mind_consnrealargs.(0) > 0 -> - (** The elimination criterion ensures that all projections can be defined. *) - let u = - match aiu with - | Monomorphic_ind _ -> Univ.Instance.empty - | Polymorphic_ind auctx -> Univ.make_abstract_instance auctx - | Cumulative_ind acumi -> Univ.make_abstract_instance (Univ.ACumulativityInfo.univ_context acumi) - in - let indsp = ((kn, 0), u) in - let rctx, indty = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in - (try - let fields, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in - let kns, projs = - compute_projections indsp nparamargs paramsctxt - pkt.mind_consnrealdecls pkt.mind_consnrealargs paramslet fields - in Some (Some (rid, kns, projs)) - with UndefinableExpansion -> Some None) - | Some _ -> Some None - | None -> None - in - (* Build the mutual inductive *) - { mind_record = isrecord; + let mib = + (* Build the mutual inductive *) + { mind_record = NotRecord; mind_ntypes = ntypes; mind_finite = isfinite; mind_hyps = hyps; @@ -970,6 +954,27 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r mind_private = prv; mind_typing_flags = Environ.typing_flags env; } + in + let record_info = match isrecord with + | Some (Some rid) -> + let is_record pkt = + pkt.mind_kelim == all_sorts + && Array.length pkt.mind_consnames == 1 + && pkt.mind_consnrealargs.(0) > 0 + in + (** 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) + in + try PrimRecord (Array.mapi map rid) + with UndefinableExpansion -> FakeRecord + else FakeRecord + | Some None -> FakeRecord + | None -> NotRecord + in + { mib with mind_record = record_info } (************************************************************************) (************************************************************************) diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 45228e35e..7c36dac67 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -43,7 +43,5 @@ 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 : pinductive -> - int -> Context.Rel.t -> int array -> int array -> - Context.Rel.t -> Context.Rel.t -> - (Constant.t array * projection_body array) +val compute_projections : inductive -> + mutual_inductive_body -> (Constant.t array * projection_body array) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 090acdf16..584c1af03 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -130,11 +130,6 @@ where Remark: Set (predicative) is encoded as Type(0) *) -let sort_as_univ = let open Sorts in function -| Type u -> u -| Prop Null -> Universe.type0m -| Prop Pos -> Universe.type0 - (* Template polymorphism *) (* cons_subst add the mapping [u |-> su] in subst if [u] is not *) @@ -168,7 +163,7 @@ let make_subst env = (* arity is a global level which, at typing time, will be enforce *) (* to be greater than the level of the argument; this is probably *) (* a useless extra constraint *) - let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in + let s = Sorts.univ_of_sort (snd (dest_arity env (Lazy.force a))) in make (cons_subst u s subst) (sign, exp, args) | LocalAssum (na,t) :: sign, Some u::exp, [] -> (* No more argument here: we add the remaining universes to the *) @@ -236,8 +231,8 @@ let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args = (* The max of an array of universes *) let cumulate_constructor_univ u = let open Sorts in function - | Prop Null -> u - | Prop Pos -> Universe.sup Universe.type0 u + | Prop -> u + | Set -> Universe.sup Universe.type0 u | Type u' -> Universe.sup u u' let max_inductive_sort = @@ -293,8 +288,8 @@ let elim_sorts (_,mip) = mip.mind_kelim let is_private (mib,_) = mib.mind_private = Some true let is_primitive_record (mib,_) = match mib.mind_record with - | Some (Some _) -> true - | _ -> false + | PrimRecord _ -> true + | NotRecord | FakeRecord -> false let build_dependent_inductive ind (_,mip) params = let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in diff --git a/kernel/modops.ml b/kernel/modops.ml index 22f523a9a..02bab581a 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -47,7 +47,6 @@ type signature_mismatch_error = | RecordFieldExpected of bool | RecordProjectionsExpected of Name.t list | NotEqualInductiveAliases - | NoTypeConstraintExpected | IncompatibleInstances | IncompatibleUniverses of Univ.univ_inconsistency | IncompatiblePolymorphism of env * types * types diff --git a/kernel/modops.mli b/kernel/modops.mli index ac76d28cf..8e7e618fc 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -106,7 +106,6 @@ type signature_mismatch_error = | RecordFieldExpected of bool | RecordProjectionsExpected of Name.t list | NotEqualInductiveAliases - | NoTypeConstraintExpected | IncompatibleInstances | IncompatibleUniverses of Univ.univ_inconsistency | IncompatiblePolymorphism of env * types * types diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 8257dc8b8..1748e98a4 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -71,6 +71,8 @@ let eq_gname gn1 gn2 = String.equal s1 s2 && eq_constructor c1 c2 | Gconstant (s1, c1), Gconstant (s2, c2) -> String.equal s1 s2 && Constant.equal c1 c2 + | Gproj (s1, ind1, i1), Gproj (s2, ind2, i2) -> + String.equal s1 s2 && eq_ind ind1 ind2 && Int.equal i1 i2 | Gcase (None, i1), Gcase (None, i2) -> Int.equal i1 i2 | Gcase (Some l1, i1), Gcase (Some l2, i2) -> Int.equal i1 i2 && Label.equal l1 l2 | Gpred (None, i1), Gpred (None, i2) -> Int.equal i1 i2 @@ -86,7 +88,9 @@ let eq_gname gn1 gn2 = | Ginternal s1, Ginternal s2 -> String.equal s1 s2 | Grel i1, Grel i2 -> Int.equal i1 i2 | Gnamed id1, Gnamed id2 -> Id.equal id1 id2 - | _ -> false + | (Gind _| Gconstruct _ | Gconstant _ | Gproj _ | Gcase _ | Gpred _ + | Gfixtype _ | Gnorm _ | Gnormtbl _ | Ginternal _ | Grel _ | Gnamed _), _ -> + false let dummy_gname = Grel 0 @@ -1841,7 +1845,7 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = in let auxdefs = List.fold_right get_rel_val fv_rel auxdefs in let auxdefs = List.fold_right get_named_val fv_named auxdefs in - let lvl = Context.Rel.length env.env_rel_context.env_rel_ctx in + let lvl = Context.Rel.length (rel_context env) in let fv_rel = List.map (fun (n,_) -> MLglobal (Grel (lvl-n))) fv_rel in let fv_named = List.map (fun (id,_) -> MLglobal (Gnamed id)) fv_named in let aux_name = fresh_lname Anonymous in @@ -1850,7 +1854,7 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = and compile_rel env sigma univ auxdefs n = let open Context.Rel.Declaration in let decl = lookup_rel n env in - let n = List.length env.env_rel_context.env_rel_ctx - n in + let n = List.length (rel_context env) - n in match decl with | LocalDef (_,t,_) -> let code = lambda_of_constr env sigma t in @@ -1965,6 +1969,7 @@ let compile_mind prefix ~interactive mb mind stack = 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 tbl = ob.mind_reloc_tbl in (* Building info *) let ci = { ci_ind = ind; ci_npar = nparams; @@ -1985,12 +1990,14 @@ let compile_mind prefix ~interactive mb mind stack = 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 ("", (pb.proj_ind, j), pb.proj_arg) in + let gn = Gproj ("", ind, pb.proj_arg) in Glet (gn, mkMLlam [|c_uid|] code) :: acc in let projs = match mb.mind_record with - | None | Some None -> [] - | Some (Some (id, kns, pbs)) -> Array.fold_left_i add_proj [] pbs + | NotRecord | FakeRecord -> [] + | PrimRecord info -> + let _, _, pbs = info.(i) in + Array.fold_left_i add_proj [] pbs in projs @ constructors @ gtype :: accu :: stack in @@ -2052,7 +2059,7 @@ let compile_deps env sigma prefix ~interactive init t = | 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 pb.proj_ind in + let init = compile_mind_deps env prefix ~interactive init (fst pb.proj_ind) in aux env lvl init c | Case (ci, p, c, ac) -> let mind = fst ci.ci_ind in diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 0325a00b4..5843cd543 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -432,7 +432,6 @@ module Renv = r end -(* What about pattern matching ?*) let is_lazy prefix t = match kind t with | App (f,args) -> @@ -448,7 +447,7 @@ let is_lazy prefix t = with Not_found -> true) | _ -> true end - | LetIn _ -> true + | LetIn _ | Case _ | Proj _ -> true | _ -> false let evar_value sigma ev = sigma.evars_val ev @@ -520,8 +519,7 @@ let rec lambda_of_constr env sigma c = | Proj (p, c) -> let pb = lookup_projection p !global_env in - (** FIXME: handle mutual records *) - let ind = (pb.proj_ind, 0) 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|] @@ -661,7 +659,7 @@ let optimize 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 !global_env.env_rel_context.env_rel_ctx 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 (* if Flags.vm_draw_opt () then begin diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index da4413a0a..3901cb9ce 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -116,7 +116,7 @@ let mk_ind_accu ind u = let mk_sort_accu s u = let open Sorts in match s with - | Prop _ -> mk_accu (Asort s) + | Prop | Set -> mk_accu (Asort s) | Type s -> let u = Univ.Instance.of_array u in let s = Univ.subst_instance_universe u s in diff --git a/kernel/reduction.ml b/kernel/reduction.ml index f4af31386..3228a155f 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -649,23 +649,19 @@ let check_leq univs u u' = let check_sort_cmp_universes env pb s0 s1 univs = let open Sorts in if not (type_in_type env) then + let check_pb u0 u1 = + match pb with + | CUMUL -> check_leq univs u0 u1 + | CONV -> check_eq univs u0 u1 + in match (s0,s1) with - | (Prop c1, Prop c2) when is_cumul pb -> - begin match c1, c2 with - | Null, _ | _, Pos -> () (* Prop <= Set *) - | _ -> raise NotConvertible - end - | (Prop c1, Prop c2) -> if c1 != c2 then raise NotConvertible - | (Prop c1, Type u) -> - let u0 = univ_of_sort s0 in - (match pb with - | CUMUL -> check_leq univs u0 u - | CONV -> check_eq univs u0 u) - | (Type u, Prop c) -> raise NotConvertible - | (Type u1, Type u2) -> - (match pb with - | CUMUL -> check_leq univs u1 u2 - | CONV -> check_eq univs u1 u2) + | Prop, Prop | Set, Set -> () + | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible + | Set, Prop -> raise NotConvertible + | Set, Type u -> check_pb Univ.type0_univ u + | Type u, Prop -> raise NotConvertible + | Type u, Set -> check_pb u Univ.type0_univ + | Type u0, Type u1 -> check_pb u0 u1 let checked_sort_cmp_universes env pb s0 s1 univs = check_sort_cmp_universes env pb s0 s1 univs; univs @@ -693,30 +689,27 @@ let infer_eq (univs, cstrs as cuniv) u u' = let infer_leq (univs, cstrs as cuniv) u u' = if UGraph.check_leq univs u u' then cuniv else - let cstrs' = Univ.enforce_leq u u' cstrs in - univs, cstrs' + let cstrs', _ = UGraph.enforce_leq_alg u u' univs in + univs, Univ.Constraint.union cstrs cstrs' let infer_cmp_universes env pb s0 s1 univs = - let open Sorts in - if type_in_type env then univs + if type_in_type env + then univs else + let open Sorts in + let infer_pb u0 u1 = + match pb with + | CUMUL -> infer_leq univs u0 u1 + | CONV -> infer_eq univs u0 u1 + in match (s0,s1) with - | (Prop c1, Prop c2) when is_cumul pb -> - begin match c1, c2 with - | Null, _ | _, Pos -> univs (* Prop <= Set *) - | _ -> raise NotConvertible - end - | (Prop c1, Prop c2) -> if c1 == c2 then univs else raise NotConvertible - | (Prop c1, Type u) -> - let u0 = univ_of_sort s0 in - (match pb with - | CUMUL -> infer_leq univs u0 u - | CONV -> infer_eq univs u0 u) - | (Type u, Prop c) -> raise NotConvertible - | (Type u1, Type u2) -> - (match pb with - | CUMUL -> infer_leq univs u1 u2 - | CONV -> infer_eq univs u1 u2) + | Prop, Prop | Set, Set -> univs + | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible else univs + | Set, Prop -> raise NotConvertible + | Set, Type u -> infer_pb Univ.type0_univ u + | Type u, Prop -> raise NotConvertible + | Type u, Set -> infer_pb u Univ.type0_univ + | Type u0, Type u1 -> infer_pb u0 u1 let infer_convert_instances ~flex u u' (univs,cstrs) = let cstrs' = diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 12c82e20d..f87ec9e02 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -897,9 +897,11 @@ let typing senv = Typeops.infer (env_of_senv senv) (** {6 Retroknowledge / native compiler } *) +[@@@ocaml.warning "-3"] (** universal lifting, used for the "get" operations mostly *) let retroknowledge f senv = Environ.retroknowledge f (env_of_senv senv) +[@@@ocaml.warning "+3"] let register field value by_clause senv = (* todo : value closed, by_clause safe, by_clause of the proper type*) @@ -918,7 +920,7 @@ let register_inline kn senv = if not (evaluable_constant kn senv.env) then CErrors.user_err Pp.(str "Register inline: an evaluable constant is expected"); let env = senv.env in - let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in + let cb = lookup_constant kn env in let cb = {cb with const_inline_code = true} in let env = add_constant kn cb env in { senv with env} diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 4078a9092..aca77ccd1 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -221,6 +221,7 @@ val delta_of_senv : open Retroknowledge val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a +[@@ocaml.deprecated "Use the projection of Environ.env"] val register : field -> Retroknowledge.entry -> Constr.constr -> safe_transformer0 diff --git a/kernel/sorts.ml b/kernel/sorts.ml index daeb90be7..a7bb08f5b 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -10,22 +10,21 @@ open Univ -type contents = Pos | Null - type family = InProp | InSet | InType type t = - | Prop of contents (* proposition types *) + | Prop + | Set | Type of Universe.t -let prop = Prop Null -let set = Prop Pos +let prop = Prop +let set = Set let type1 = Type type1_univ let univ_of_sort = function | Type u -> u - | Prop Pos -> Universe.type0 - | Prop Null -> Universe.type0m + | Set -> Universe.type0 + | Prop -> Universe.type0m let sort_of_univ u = if is_type0m_univ u then prop @@ -34,36 +33,34 @@ let sort_of_univ u = let compare s1 s2 = if s1 == s2 then 0 else - match s1, s2 with - | Prop c1, Prop c2 -> - begin match c1, c2 with - | Pos, Pos | Null, Null -> 0 - | Pos, Null -> -1 - | Null, Pos -> 1 - end - | Type u1, Type u2 -> Universe.compare u1 u2 - | Prop _, Type _ -> -1 - | Type _, Prop _ -> 1 + match s1, s2 with + | Prop, Prop -> 0 + | Prop, _ -> -1 + | Set, Prop -> 1 + | Set, Set -> 0 + | Set, _ -> -1 + | Type u1, Type u2 -> Universe.compare u1 u2 + | Type _, _ -> -1 let equal s1 s2 = Int.equal (compare s1 s2) 0 let is_prop = function - | Prop Null -> true + | Prop -> true | Type u when Universe.equal Universe.type0m u -> true | _ -> false let is_set = function - | Prop Pos -> true + | Set -> true | Type u when Universe.equal Universe.type0 u -> true | _ -> false let is_small = function - | Prop _ -> true + | Prop | Set -> true | Type u -> is_small_univ u let family = function - | Prop Null -> InProp - | Prop Pos -> InSet + | Prop -> InProp + | Set -> InSet | Type u when is_type0m_univ u -> InProp | Type u when is_type0_univ u -> InSet | Type _ -> InType @@ -73,15 +70,11 @@ let family_equal = (==) open Hashset.Combine let hash = function -| Prop p -> - let h = match p with - | Pos -> 0 - | Null -> 1 - in - combinesmall 1 h -| Type u -> - let h = Univ.Universe.hash u in - combinesmall 2 h + | Prop -> combinesmall 1 0 + | Set -> combinesmall 1 1 + | Type u -> + let h = Univ.Universe.hash u in + combinesmall 2 h module List = struct let mem = List.memq @@ -101,7 +94,7 @@ module Hsorts = if u' == u then c else Type u' | s -> s let eq s1 s2 = match (s1,s2) with - | (Prop c1, Prop c2) -> c1 == c2 + | Prop, Prop | Set, Set -> true | (Type u1, Type u2) -> u1 == u2 |_ -> false diff --git a/kernel/sorts.mli b/kernel/sorts.mli index 1bbde2608..cac6229b9 100644 --- a/kernel/sorts.mli +++ b/kernel/sorts.mli @@ -10,13 +10,12 @@ (** {6 The sorts of CCI. } *) -type contents = Pos | Null - type family = InProp | InSet | InType type t = -| Prop of contents (** Prop and Set *) -| Type of Univ.Universe.t (** Type *) + | Prop + | Set + | Type of Univ.Universe.t val set : t val prop : t diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 8cf588c3e..1e58f5c24 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -17,7 +17,6 @@ open Names open Univ open Util -open Term open Constr open Declarations open Declareops @@ -138,39 +137,8 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 in let mib2 = Declareops.subst_mind_body subst2 mib2 in let check_inductive_type cst name t1 t2 = - - (* Due to template polymorphism, the conclusions of - t1 and t2, if in Type, are generated as the least upper bounds - of the types of the constructors. - - By monotonicity of the infered l.u.b. wrt subtyping (i.e. if X:U - |- T(X):s and |- M:U' and U'<=U then infer_type(T(M))<=s), each - universe in the conclusion of t1 has an bounding universe in - the conclusion of t2, so that we don't need to check the - subtyping of the conclusions of t1 and t2. - - Even if we'd like to recheck it, the inference of constraints - is not designed to deal with algebraic constraints of the form - max-univ(u1..un) <= max-univ(u'1..u'n), so that it is not easy - to recheck it (in short, we would need the actual graph of - constraints as input while type checking is currently designed - to output a set of constraints instead) *) - - (* So we cheat and replace the subtyping problem on algebraic - constraints of the form max-univ(u1..un) <= max-univ(u'1..u'n) - (that we know are necessary true) by trivial constraints that - the constraint generator knows how to deal with *) - - let (ctx1,s1) = dest_arity env t1 in - let (ctx2,s2) = dest_arity env t2 in - let s1,s2 = - match s1, s2 with - | Type _, Type _ -> (* shortcut here *) Sorts.prop, Sorts.prop - | (Prop _, Type _) | (Type _,Prop _) -> - error (NotConvertibleInductiveField name) - | _ -> (s1, s2) in check_conv (NotConvertibleInductiveField name) - cst (inductive_is_polymorphic mib1) infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2)) + cst (inductive_is_polymorphic mib1) infer_conv_leq env t1 t2 in let check_packet cst p1 p2 = @@ -226,8 +194,9 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 else error NotEqualInductiveAliases end; (* we check that records and their field names are preserved. *) - check (fun mib -> mib.mind_record <> None) (==) (fun x -> RecordFieldExpected x); - if mib1.mind_record <> None then begin + (** FIXME: this check looks nonsense *) + check (fun mib -> mib.mind_record <> NotRecord) (==) (fun x -> RecordFieldExpected x); + if mib1.mind_record <> NotRecord then begin let rec names_prod_letin t = match kind t with | Prod(n,_,t) -> n::(names_prod_letin t) | LetIn(n,_,_,t) -> n::(names_prod_letin t) @@ -259,53 +228,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let error why = error_signature_mismatch l spec2 why in let check_conv cst poly f = check_conv_error error cst poly f in let check_type poly cst env t1 t2 = - let err = NotConvertibleTypeField (env, t1, t2) in - - (* If the type of a constant is generated, it may mention - non-variable algebraic universes that the general conversion - algorithm is not ready to handle. Anyway, generated types of - constants are functions of the body of the constant. If the - bodies are the same in environments that are subtypes one of - the other, the types are subtypes too (i.e. if Gamma <= Gamma', - Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T'). - Hence they don't have to be checked again *) - - let t1,t2 = - if isArity t2 then - let (ctx2,s2) = destArity t2 in - match s2 with - | Type v when not (is_univ_variable v) -> - (* The type in the interface is inferred and is made of algebraic - universes *) - begin try - let (ctx1,s1) = dest_arity env t1 in - match s1 with - | Type u when not (is_univ_variable u) -> - (* Both types are inferred, no need to recheck them. We - cheat and collapse the types to Prop *) - mkArity (ctx1,Sorts.prop), mkArity (ctx2,Sorts.prop) - | Prop _ -> - (* The type in the interface is inferred, it may be the case - that the type in the implementation is smaller because - the body is more reduced. We safely collapse the upper - type to Prop *) - mkArity (ctx1,Sorts.prop), mkArity (ctx2,Sorts.prop) - | Type _ -> - (* The type in the interface is inferred and the type in the - implementation is not inferred or is inferred but from a - more reduced body so that it is just a variable. Since - constraints of the form "univ <= max(...)" are not - expressible in the system of algebraic universes: we fail - (the user has to use an explicit type in the interface *) - error NoTypeConstraintExpected - with NotArity -> - error err end - | _ -> - t1,t2 - else - (t1,t2) in - check_conv err cst poly infer_conv_leq env t1 t2 + check_conv err cst poly infer_conv_leq env t1 t2 in match info1 with | Constant cb1 -> diff --git a/kernel/term.ml b/kernel/term.ml index b44e038e9..81e344e73 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -16,14 +16,11 @@ open Vars open Constr (* Deprecated *) -type contents = Sorts.contents = Pos | Null -[@@ocaml.deprecated "Alias for Sorts.contents"] - type sorts_family = Sorts.family = InProp | InSet | InType [@@ocaml.deprecated "Alias for Sorts.family"] type sorts = Sorts.t = - | Prop of Sorts.contents (** Prop and Set *) + | Prop | Set | Type of Univ.Universe.t (** Type *) [@@ocaml.deprecated "Alias for Sorts.t"] diff --git a/kernel/term.mli b/kernel/term.mli index f651d1a58..4d340399d 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -190,13 +190,10 @@ type ('constr, 'types) kind_of_type = val kind_of_type : types -> (constr, types) kind_of_type (* Deprecated *) -type contents = Sorts.contents = Pos | Null -[@@ocaml.deprecated "Alias for Sorts.contents"] - type sorts_family = Sorts.family = InProp | InSet | InType [@@ocaml.deprecated "Alias for Sorts.family"] type sorts = Sorts.t = - | Prop of Sorts.contents (** Prop and Set *) + | Prop | Set | Type of Univ.Universe.t (** Type *) [@@ocaml.deprecated "Alias for Sorts.t"] diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 37bf679c5..bad449731 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -179,36 +179,36 @@ let rec is_nth_suffix n l suf = | _ :: l -> is_nth_suffix (pred n) l suf (* Given the list of signatures of side effects, checks if they match. - * I.e. if they are ordered descendants of the current revstruct *) + * I.e. if they are ordered descendants of the current revstruct. + Returns the number of effects that can be trusted. *) let check_signatures curmb sl = - let is_direct_ancestor (sl, curmb) (mb, how_many) = - match curmb with - | None -> None, None - | Some curmb -> + let is_direct_ancestor accu (mb, how_many) = + match accu with + | None -> None + | Some (n, curmb) -> try let mb = CEphemeron.get mb in - match sl with - | None -> sl, None - | Some n -> - if is_nth_suffix how_many mb curmb - then Some (n + how_many), Some mb - else None, None - with CEphemeron.InvalidKey -> None, None in - let sl, _ = List.fold_left is_direct_ancestor (Some 0,Some curmb) sl in - sl + if is_nth_suffix how_many mb curmb + then Some (n + how_many, mb) + else None + with CEphemeron.InvalidKey -> None in + let sl = List.fold_left is_direct_ancestor (Some (0, curmb)) sl in + match sl with + | None -> 0 + | Some (n, _) -> n let skip_trusted_seff sl b e = let rec aux sl b e acc = let open Context.Rel.Declaration in - match sl, kind b with - | (None|Some 0), _ -> b, e, acc - | Some sl, LetIn (n,c,ty,bo) -> - aux (Some (sl-1)) bo + if Int.equal sl 0 then b, e, acc + else match kind b with + | LetIn (n,c,ty,bo) -> + aux (sl - 1) bo (Environ.push_rel (LocalDef (n,c,ty)) e) (`Let(n,c,ty)::acc) - | Some sl, App(hd,arg) -> + | App(hd,arg) -> begin match kind hd with | Lambda (n,ty,bo) -> - aux (Some (sl-1)) bo + aux (sl - 1) bo (Environ.push_rel (LocalAssum (n,ty)) e) (`Cut(n,ty,arg)::acc) | _ -> assert false end @@ -522,23 +522,24 @@ let export_side_effects mb env c = end in let rec translate_seff sl seff acc env = - match sl, seff with - | _, [] -> List.rev acc, ce - | (None | Some 0), cbs :: rest -> + match seff with + | [] -> List.rev acc, ce + | cbs :: rest -> + if Int.equal sl 0 then let env, cbs = List.fold_left (fun (env,cbs) (kn, ocb, u, r) -> let ce = constant_entry_of_side_effect ocb u in let cb = translate_constant Pure env kn ce in (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,r) :: cbs)) (env,[]) cbs in - translate_seff sl rest (cbs @ acc) env - | Some sl, cbs :: rest -> + translate_seff 0 rest (cbs @ acc) env + else let cbs_len = List.length cbs in let cbs = List.map turn_direct cbs in let env = List.fold_left push_seff env cbs in let ecbs = List.map (fun (kn,cb,u,r) -> kn, cb, r) cbs in - translate_seff (Some (sl-cbs_len)) rest (ecbs @ acc) env + translate_seff (sl - cbs_len) rest (ecbs @ acc) env in translate_seff trusted seff [] env ;; diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 325d5cecd..7c0057696 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -69,7 +69,7 @@ let type_of_type u = mkType uu let type_of_sort = function - | Prop c -> type1 + | Prop | Set -> type1 | Type u -> type_of_type u (*s Type of a de Bruijn index. *) @@ -178,11 +178,11 @@ let type_of_apply env func funt argsv argstv = let sort_of_product env domsort rangsort = match (domsort, rangsort) with (* Product rule (s,Prop,Prop) *) - | (_, Prop Null) -> rangsort + | (_, Prop) -> rangsort (* Product rule (Prop/Set,Set,Set) *) - | (Prop _, Prop Pos) -> rangsort + | ((Prop | Set), Set) -> rangsort (* Product rule (Type,Set,?) *) - | (Type u1, Prop Pos) -> + | (Type u1, Set) -> if is_impredicative_set env then (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) rangsort @@ -190,9 +190,9 @@ let sort_of_product env domsort rangsort = (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) Type (Universe.sup Universe.type0 u1) (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Pos, Type u2) -> Type (Universe.sup Universe.type0 u2) + | (Set, Type u2) -> Type (Universe.sup Universe.type0 u2) (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Null, Type _) -> rangsort + | (Prop, Type _) -> rangsort (* Product rule (Type_i,Type_i,Type_i) *) | (Type u1, Type u2) -> Type (Universe.sup u1 u2) @@ -301,7 +301,7 @@ let type_of_projection env p c ct = try find_rectype env ct with Not_found -> error_case_not_inductive env (make_judge c ct) in - assert(MutInd.equal pb.proj_ind (fst ind)); + assert(eq_ind pb.proj_ind ind); let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in substl (c :: CList.rev args) ty @@ -481,10 +481,6 @@ let judge_of_prop = make_judge mkProp type1 let judge_of_set = make_judge mkSet type1 let judge_of_type u = make_judge (mkType u) (type_of_type u) -let judge_of_prop_contents = function - | Null -> judge_of_prop - | Pos -> judge_of_set - let judge_of_relative env k = make_judge (mkRel k) (type_of_relative env k) let judge_of_variable env x = make_judge (mkVar x) (type_of_variable env x) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 546f2d2b4..3b2abc777 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -43,7 +43,6 @@ val type1 : types val type_of_sort : Sorts.t -> types val judge_of_prop : unsafe_judgment val judge_of_set : unsafe_judgment -val judge_of_prop_contents : Sorts.contents -> unsafe_judgment val judge_of_type : Universe.t -> unsafe_judgment (** {6 Type of a bound variable. } *) diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 4a9467de5..bc624ba56 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -747,6 +747,45 @@ let check_constraint g (l,d,r) = let check_constraints c g = Constraint.for_all (check_constraint g) c +let leq_expr (u,m) (v,n) = + let d = match m - n with + | 1 -> Lt + | diff -> assert (diff <= 0); Le + in + (u,d,v) + +let enforce_leq_alg u v g = + let enforce_one (u,v) = function + | Inr _ as orig -> orig + | Inl (cstrs,g) as orig -> + if check_smaller_expr g u v then orig + else + (let c = leq_expr u v in + match enforce_constraint c g with + | g -> Inl (Constraint.add c cstrs,g) + | exception (UniverseInconsistency _ as e) -> Inr e) + in + (* max(us) <= max(vs) <-> forall u in us, exists v in vs, u <= v *) + let c = Universe.map (fun u -> Universe.map (fun v -> (u,v)) v) u in + let c = List.cartesians enforce_one (Inl (Constraint.empty,g)) c in + (* We pick a best constraint: smallest number of constraints, not an error if possible. *) + let order x y = match x, y with + | Inr _, Inr _ -> 0 + | Inl _, Inr _ -> -1 + | Inr _, Inl _ -> 1 + | Inl (c,_), Inl (c',_) -> + Int.compare (Constraint.cardinal c) (Constraint.cardinal c') + in + match List.min order c with + | Inl x -> x + | Inr e -> raise e + +(* sanity check wrapper *) +let enforce_leq_alg u v g = + let _,g as cg = enforce_leq_alg u v g in + assert (check_leq g u v); + cg + (* Normalization *) (** [normalize_universes g] returns a graph where all edges point diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index e6dd629e4..8c2d877b0 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -42,6 +42,9 @@ val merge_constraints : Constraint.t -> t -> t val check_constraint : t -> univ_constraint -> bool val check_constraints : Constraint.t -> t -> bool +(** Picks an arbitrary set of constraints sufficient to ensure [u <= v]. *) +val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t + (** Adds a universe to the graph, ensuring it is >= or > Set. @raise AlreadyDeclared if the level is already declared in the graph. *) diff --git a/kernel/univ.ml b/kernel/univ.ml index 9782312ca..311477dac 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -666,7 +666,7 @@ let constraint_add_leq v u c = else (* j >= 1 *) (* m = n + k, u <= v+k *) if Level.equal x y then c (* u <= u+k, trivial *) else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *) - else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints.") + else Constraint.add (x,Le,y) c (* u <= v implies u <= v+k *) let check_univ_leq_one u v = Universe.exists (Expr.leq u) v @@ -674,12 +674,7 @@ let check_univ_leq u v = Universe.for_all (fun u -> check_univ_leq_one u v) u let enforce_leq u v c = - let rec aux acc v = - match v with - | v :: l -> - aux (List.fold_right (fun u -> constraint_add_leq u v) u c) l - | [] -> acc - in aux c v + List.fold_left (fun c v -> (List.fold_left (fun c u -> constraint_add_leq u v c) c u)) c v let enforce_leq u v c = if check_univ_leq u v then c |