diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-05 20:27:37 +0200 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-05 20:27:37 +0200 |
commit | 66acf05f6fd0a35b7d9a0d425983c36dbe2cc992 (patch) | |
tree | d67a1ead218ca15becb33b605426cb5429323b60 | |
parent | 0d7cd6eebd5b681f7dcb243e3cda4466e735e025 (diff) |
Fix checker treatment of inductives using subst_instances instead of subst_univs_levels.
-rw-r--r-- | checker/cic.mli | 4 | ||||
-rw-r--r-- | checker/environ.ml | 12 | ||||
-rw-r--r-- | checker/inductive.ml | 87 | ||||
-rw-r--r-- | checker/inductive.mli | 2 | ||||
-rw-r--r-- | checker/term.ml | 46 | ||||
-rw-r--r-- | checker/term.mli | 4 | ||||
-rw-r--r-- | checker/typeops.ml | 8 | ||||
-rw-r--r-- | checker/univ.ml | 60 | ||||
-rw-r--r-- | checker/univ.mli | 16 | ||||
-rw-r--r-- | kernel/univ.ml | 1 |
10 files changed, 151 insertions, 89 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index c1d7b0d73..2f33c60f5 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -170,7 +170,7 @@ type engagement = ImpredicativeSet type template_arity = { - template_param_levels : Univ.universe option list; + template_param_levels : Univ.universe_level option list; template_level : Univ.universe; } @@ -212,8 +212,6 @@ type constant_body = { const_body : constant_def; const_type : constant_type; const_body_code : to_patch_substituted; - const_constraints : Univ.constraints; - const_native_name : native_name ref; const_polymorphic : bool; (** Is it polymorphic or not *) const_universes : constant_universes; const_proj : projection_body option; diff --git a/checker/environ.ml b/checker/environ.ml index a04e95cfc..710ebc712 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -108,10 +108,9 @@ type const_evaluation_result = NoBody | Opaque (* Constant types *) -let universes_and_subst_of cb u = +let constraints_of cb u = let univs = cb.const_universes in - let subst = Univ.make_universe_subst u univs in - subst, Univ.instantiate_univ_context subst univs + Univ.subst_instance_constraints u (Univ.UContext.constraints univs) let map_regular_arity f = function | RegularArity a as ar -> @@ -123,8 +122,8 @@ let map_regular_arity f = function let constant_type env (kn,u) = let cb = lookup_constant kn env in if cb.const_polymorphic then - let subst, csts = universes_and_subst_of cb u in - (map_regular_arity (subst_univs_level_constr subst) cb.const_type, csts) + let csts = constraints_of cb u in + (map_regular_arity (subst_instance_constr u) cb.const_type, csts) else cb.const_type, Univ.Constraint.empty exception NotEvaluableConst of const_evaluation_result @@ -135,8 +134,7 @@ let constant_value env (kn,u) = | Def l_body -> let b = force_constr l_body in if cb.const_polymorphic then - let subst = Univ.make_universe_subst u cb.const_universes in - subst_univs_level_constr subst b + subst_instance_constr u (force_constr l_body) else b | OpaqueDef _ -> raise (NotEvaluableConst Opaque) | Undef _ -> raise (NotEvaluableConst NoBody) diff --git a/checker/inductive.ml b/checker/inductive.ml index adb9e0347..c23b2578b 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -54,29 +54,20 @@ let inductive_params (mib,_) = mib.mind_nparams (** Polymorphic inductives *) -let make_inductive_subst mib u = - if mib.mind_polymorphic then - Univ.make_universe_subst u mib.mind_universes - else Univ.empty_level_subst - -let inductive_paramdecls (mib,u) = - let subst = make_inductive_subst mib u in - subst_univs_level_context subst mib.mind_params_ctxt - let inductive_instance mib = - if mib.mind_polymorphic then - Univ.UContext.instance mib.mind_universes - else Univ.Instance.empty + if mib.mind_polymorphic then + UContext.instance mib.mind_universes + else Instance.empty let inductive_context mib = if mib.mind_polymorphic then - mib.mind_universes - else Univ.UContext.empty + instantiate_univ_context mib.mind_universes + else UContext.empty -let instantiate_inductive_constraints mib subst = +let instantiate_inductive_constraints mib u = if mib.mind_polymorphic then - Univ.instantiate_univ_context subst mib.mind_universes - else Univ.Constraint.empty + subst_instance_constraints u (UContext.constraints mib.mind_universes) + else Constraint.empty (************************************************************************) @@ -88,9 +79,9 @@ let ind_subst mind mib u = List.init ntypes make_Ik (* Instantiate inductives in constructor type *) -let constructor_instantiate mind u subst mib c = +let constructor_instantiate mind u mib c = let s = ind_subst mind mib u in - substl s (subst_univs_level_constr subst c) + substl s (subst_instance_constr u c) let instantiate_params full t args sign = let fail () = @@ -112,13 +103,11 @@ let instantiate_params full t args sign = let full_inductive_instantiate mib u params sign = let dummy = Prop Null in let t = mkArity (sign,dummy) in - let subst = make_inductive_subst mib u in let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in - subst_univs_level_context subst ar + subst_instance_context u ar let full_constructor_instantiate ((mind,_),u,(mib,_),params) = - let subst = make_inductive_subst mib u in - let inst_ind = constructor_instantiate mind u subst mib in + let inst_ind = constructor_instantiate mind u mib in (fun t -> instantiate_params true (inst_ind t) params mib.mind_params_ctxt) @@ -155,8 +144,8 @@ let sort_as_univ = function let cons_subst u su subst = try - (u, Univ.sup su (List.assoc_f Univ.Universe.equal u subst)) :: - List.remove_assoc_f Univ.Universe.equal u subst + (u, Univ.sup su (List.assoc_f Univ.Level.equal u subst)) :: + List.remove_assoc_f Univ.Level.equal u subst with Not_found -> (u, su) :: subst let actualize_decl_level env lev t = @@ -225,30 +214,11 @@ let is_prop_sort = function | Prop Null -> true | _ -> false -let type_of_inductive_subst ?(polyprop=true) env ((mib,mip),u) paramtyps = - match mip.mind_arity with - | RegularArity a -> - if not mib.mind_polymorphic then (a.mind_user_arity, Univ.LMap.empty) - else - let subst = make_inductive_subst mib u in - (subst_univs_level_constr subst a.mind_user_arity, subst) - | TemplateArity ar -> - let ctx = List.rev mip.mind_arity_ctxt in - let ctx,s = instantiate_universes env ctx ar paramtyps in - (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e. - the situation where a non-Prop singleton inductive becomes Prop - when applied to Prop params *) - if not polyprop && not (Univ.is_type0m_univ ar.template_level) && is_prop_sort s - then raise (SingletonInductiveBecomesProp mip.mind_typename); - mkArity (List.rev ctx,s), Univ.LMap.empty - let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = match mip.mind_arity with | RegularArity a -> if not mib.mind_polymorphic then a.mind_user_arity - else - let subst = make_inductive_subst mib u in - (subst_univs_level_constr subst a.mind_user_arity) + else subst_instance_constr u a.mind_user_arity | TemplateArity ar -> let ctx = List.rev mip.mind_arity_ctxt in let ctx,s = instantiate_universes env ctx ar paramtyps in @@ -263,13 +233,13 @@ let type_of_inductive env pind = type_of_inductive_gen env pind [||] let constrained_type_of_inductive env ((mib,mip),u as pind) = - let ty, subst = type_of_inductive_subst env pind [||] in - let cst = instantiate_inductive_constraints mib subst in + let ty = type_of_inductive_gen env pind [||] in + let cst = instantiate_inductive_constraints mib u in (ty, cst) let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) args = - let ty, subst = type_of_inductive_subst env pind args in - let cst = instantiate_inductive_constraints mib subst in + let ty = type_of_inductive_gen env pind args in + let cst = instantiate_inductive_constraints mib u in (ty, cst) let type_of_inductive_knowing_parameters env mip args = @@ -293,36 +263,33 @@ let max_inductive_sort = (************************************************************************) (* Type of a constructor *) -let type_of_constructor_subst cstr u subst (mib,mip) = +let type_of_constructor_subst cstr u (mib,mip) = let ind = inductive_of_constructor cstr in let specif = mip.mind_user_lc in let i = index_of_constructor cstr in let nconstr = Array.length mip.mind_consnames in if i > nconstr then error "Not enough constructors in the type."; - let c = constructor_instantiate (fst ind) u subst mib specif.(i-1) in - c + constructor_instantiate (fst ind) u mib specif.(i-1) let type_of_constructor_gen (cstr,u) (mib,mip as mspec) = - let subst = make_inductive_subst mib u in - type_of_constructor_subst cstr u subst mspec, subst + type_of_constructor_subst cstr u mspec let type_of_constructor cstru mspec = - fst (type_of_constructor_gen cstru mspec) + type_of_constructor_gen cstru mspec let type_of_constructor_in_ctx cstr (mib,mip as mspec) = let u = Univ.UContext.instance mib.mind_universes in let c = type_of_constructor_gen (cstr, u) mspec in - (fst c, mib.mind_universes) + (c, mib.mind_universes) let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) = - let ty, subst = type_of_constructor_gen cstru ind in - let cst = instantiate_inductive_constraints mib subst in + let ty = type_of_constructor_gen cstru ind in + let cst = instantiate_inductive_constraints mib u in (ty, cst) let arities_of_specif (kn,u) (mib,mip) = let specif = mip.mind_nf_lc in - let subst = make_inductive_subst mib u in - Array.map (constructor_instantiate kn u subst mib) specif + Array.map (constructor_instantiate kn u mib) specif diff --git a/checker/inductive.mli b/checker/inductive.mli index d2f6788c5..50dd343ee 100644 --- a/checker/inductive.mli +++ b/checker/inductive.mli @@ -22,8 +22,6 @@ type mind_specif = mutual_inductive_body * one_inductive_body Raises [Not_found] if the inductive type is not found. *) val lookup_mind_specif : env -> inductive -> mind_specif -val make_inductive_subst : mutual_inductive_body -> Univ.universe_instance -> - Univ.universe_level_subst val inductive_instance : mutual_inductive_body -> Univ.universe_instance val type_of_inductive : env -> mind_specif puniverses -> constr diff --git a/checker/term.ml b/checker/term.ml index e8cdb03e9..3438f497a 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -24,6 +24,11 @@ let family_of_sort = function let family_equal = (==) +let sort_of_univ u = + if Univ.is_type0m_univ u then Prop Null + else if Univ.is_type0_univ u then Prop Pos + else Type u + (********************************************************************) (* Constructions as implemented *) (********************************************************************) @@ -469,3 +474,44 @@ let subst_univs_level_constr subst c = let subst_univs_level_context s = map_rel_context (subst_univs_level_constr s) + +let subst_instance_constr subst c = + if Univ.Instance.is_empty subst then c + else + let f u = Univ.subst_instance_instance subst u in + let changed = ref false in + let rec aux t = + match t with + | Const (c, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (changed := true; Const (c, u')) + | Ind (i, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (changed := true; Ind (i, u')) + | Construct (c, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (changed := true; Construct (c, u')) + | Sort (Type u) -> + let u' = Univ.subst_instance_universe subst u in + if u' == u then t else + (changed := true; Sort (sort_of_univ u')) + | _ -> map_constr aux t + in + let c' = aux c in + if !changed then c' else c + +(* let substkey = Profile.declare_profile "subst_instance_constr";; *) +(* let subst_instance_constr inst c = Profile.profile2 substkey subst_instance_constr inst c;; *) + +let subst_instance_context s ctx = + if Univ.Instance.is_empty s then ctx + else map_rel_context (fun x -> subst_instance_constr s x) ctx diff --git a/checker/term.mli b/checker/term.mli index 5e98885fa..3c4835dbb 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -56,3 +56,7 @@ val eq_constr : constr -> constr -> bool val subst_univs_constr : Univ.universe_subst -> constr -> constr val subst_univs_level_constr : Univ.universe_level_subst -> constr -> constr val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_context + +(** Instance substitution for polymorphism. *) +val subst_instance_constr : Univ.universe_instance -> constr -> constr +val subst_instance_context : Univ.universe_instance -> rel_context -> rel_context diff --git a/checker/typeops.ml b/checker/typeops.ml index 77fc4af73..f69f10295 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -224,8 +224,7 @@ let judge_of_projection env p c ct = with Not_found -> error_case_not_inductive env (c, ct) in assert(eq_mind pb.proj_ind (fst ind)); - let usubst = make_inductive_subst (fst (lookup_mind_specif env ind)) u in - let ty = subst_univs_level_constr usubst pb.proj_type in + let ty = subst_instance_constr u pb.proj_type in substl (c :: List.rev args) ty (* Fixpoints. *) @@ -392,8 +391,9 @@ let check_ctxt env rels = (* Polymorphic arities utils *) let check_kind env ar u = - if snd (dest_prod env ar) = Sort(Type u) then () - else failwith "not the correct sort" + match (snd (dest_prod env ar)) with + | Sort (Type u') when Univ.Universe.equal u' (Univ.Universe.make u) -> () + | _ -> failwith "not the correct sort" let check_polymorphic_arity env params par = let pl = par.template_param_levels in diff --git a/checker/univ.ml b/checker/univ.ml index e2e40ddc9..04897e85c 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -246,6 +246,7 @@ struct | Prop | Set | Level of int * DirPath.t + | Var of int (* Hash-consing *) @@ -256,6 +257,7 @@ struct | Set, Set -> true | Level (n,d), Level (n',d') -> Int.equal n n' && DirPath.equal d d' + | Var n, Var n' -> Int.equal n n' | _ -> false let compare u v = @@ -270,6 +272,9 @@ struct if i1 < i2 then -1 else if i1 > i2 then 1 else DirPath.compare dp1 dp2 + | Level _, _ -> -1 + | _, Level _ -> 1 + | Var n, Var m -> Int.compare n m let hcons = function | Prop as x -> x @@ -277,13 +282,15 @@ struct | Level (n,d) as x -> let d' = Names.DirPath.hcons d in if d' == d then x else Level (n,d') + | Var n as x -> x open Hashset.Combine let hash = function | Prop -> combinesmall 1 0 | Set -> combinesmall 1 1 - | Level (n, d) -> combinesmall 2 (combine n (Names.DirPath.hash d)) + | Var n -> combinesmall 2 n + | Level (n, d) -> combinesmall 3 (combine n (Names.DirPath.hash d)) end module Level = struct @@ -294,6 +301,7 @@ module Level = struct | Prop | Set | Level of int * DirPath.t + | Var of int (** Embed levels with their hash value *) type t = { @@ -357,6 +365,7 @@ module Level = struct | Prop -> "Prop" | Set -> "Set" | Level (n,d) -> Names.DirPath.to_string d^"."^string_of_int n + | Var i -> "Var("^string_of_int i^")" let pr u = str (to_string u) @@ -1149,13 +1158,9 @@ let remove_large_constraint u v min = | None -> Huniv.remove (Universe.Expr.make u) v let subst_large_constraint u u' v = - match level u with - | Some u -> - (* if is_direct_constraint u v then *) - Universe.sup u' (remove_large_constraint u v type0m_univ) - (* else v *) - | _ -> - anomaly (Pp.str "expect a universe level") + (* if is_direct_constraint u v then *) + Universe.sup u' (remove_large_constraint u v type0m_univ) + (* else v *) let subst_large_constraints = List.fold_right (fun (u,u') -> subst_large_constraint u u') @@ -1181,7 +1186,7 @@ let level_subst_of f = with Not_found -> l module Instance : sig - type t + type t = Level.t array val empty : t val is_empty : t -> bool @@ -1329,9 +1334,42 @@ let subst_univs_level_constraints subst csts = (fun c -> Option.fold_right Constraint.add (subst_univs_level_constraint subst c)) csts Constraint.empty +(* let instantiate_univ_context subst (_, csts) = *) +(* subst_univs_level_constraints subst csts *) + (** Substitute instance inst for ctx in csts *) -let instantiate_univ_context subst (_, csts) = - subst_univs_level_constraints subst csts + +let subst_instance_level s l = + match l.Level.data with + | Level.Var n -> s.(n) + | _ -> l + +let subst_instance_instance s i = + Array.smartmap (fun l -> subst_instance_level s l) i + +let subst_instance_universe s u = + let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in + let u' = Universe.smartmap f u in + if u == u' then u + else Universe.sort u' + +let subst_instance_constraint s (u,d,v as c) = + let u' = subst_instance_level s u in + let v' = subst_instance_level s v in + if u' == u && v' == v then c + else (u',d,v') + +let subst_instance_constraints s csts = + Constraint.fold + (fun c csts -> Constraint.add (subst_instance_constraint s c) csts) + csts Constraint.empty + +(** Substitute instance inst for ctx in csts *) +let instantiate_univ_context (ctx, csts) = + (ctx, subst_instance_constraints ctx csts) + +let instantiate_univ_constraints u (_, csts) = + subst_instance_constraints u csts (** With level to universe substitutions. *) type universe_subst_fn = universe_level -> universe diff --git a/checker/univ.mli b/checker/univ.mli index b2f2c9c18..27f4c9a6e 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -18,6 +18,7 @@ sig (** Create a new universe level from a unique identifier and an associated module path. *) + val equal : t -> t -> bool end type universe_level = Level.t @@ -122,7 +123,7 @@ val check_constraints : constraints -> universes -> bool (** {6 Support for old-style sort-polymorphism } *) val subst_large_constraints : - (universe * universe) list -> universe -> universe + (universe_level * universe) list -> universe -> universe (** {6 Support for universe polymorphism } *) @@ -209,6 +210,19 @@ val make_subst : universe_subst -> universe_subst_fn val subst_univs_universe : universe_subst_fn -> universe -> universe val subst_univs_constraints : universe_subst_fn -> constraints -> constraints + +(** Substitution of instances *) +val subst_instance_instance : universe_instance -> universe_instance -> universe_instance +val subst_instance_universe : universe_instance -> universe -> universe +val subst_instance_constraints : universe_instance -> constraints -> constraints + +(* val make_instance_subst : universe_instance -> universe_level_subst *) +(* val make_inverse_instance_subst : universe_instance -> universe_level_subst *) + +(** Get the instantiated graph. *) +val instantiate_univ_context : universe_context -> universe_context +val instantiate_univ_constraints : universe_instance -> universe_context -> constraints + (** {6 Pretty-printing of universes. } *) val pr_universes : universes -> Pp.std_ppcmds diff --git a/kernel/univ.ml b/kernel/univ.ml index 202f6232d..fd65d7de5 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -2003,7 +2003,6 @@ let subst_univs_constraints subst csts = (fun c cstrs -> subst_univs_constraint subst c cstrs) csts Constraint.empty - let subst_instance_level s l = match l.Level.data with | Level.Var n -> s.(n) |