Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

- Fix handling of universe polymorphism in typeclasses Class/Instance…

… declarations.

- Don't allow lowering a rigid Type universe to Set silently.
  • Loading branch information...
commit 1360b14b879da4362b09b73508d5844be4525fd8 1 parent f0c9b75
@mattam82 mattam82 authored
View
8 kernel/term.ml
@@ -77,8 +77,12 @@ let sorts_ord s1 s2 =
| Type _, Prop _ -> 1
let is_prop_sort = function
-| Prop Null -> true
-| _ -> false
+ | Prop Null -> true
+ | _ -> false
+
+let is_set_sort = function
+ | Prop Pos -> true
+ | _ -> false
type sorts_family = InProp | InSet | InType
View
1  kernel/term.mli
@@ -31,6 +31,7 @@ val type1_sort : sorts
val sorts_ord : sorts -> sorts -> int
val is_prop_sort : sorts -> bool
+val is_set_sort : sorts -> bool
val univ_of_sort : sorts -> Univ.universe
val sort_of_univ : Univ.universe -> sorts
View
6 kernel/univ.ml
@@ -36,6 +36,12 @@ module Level = struct
| Set
| Level of int * Names.dir_path
+ let set = Set
+ let prop = Prop
+ let is_small = function
+ | Level _ -> false
+ | _ -> true
+
(* A specialized comparison function: we compare the [int] part first.
This way, most of the time, the [dir_path] part is not considered.
View
4 kernel/univ.mli
@@ -14,6 +14,10 @@ sig
(** Type of universe levels. A universe level is essentially a unique name
that will be associated to constraints later on. *)
+ val set : t
+ val prop : t
+ val is_small : t -> bool
+
val compare : t -> t -> int
(** Comparison function *)
View
8 library/universes.ml
@@ -93,6 +93,14 @@ let fresh_global_or_constr_instance env = function
| IsConstr c -> c, Univ.empty_universe_context_set
| IsGlobal gr -> fresh_global_instance env gr
+let global_of_constr c =
+ match kind_of_term c with
+ | Const (c, u) -> ConstRef c, u
+ | Ind (i, u) -> IndRef i, u
+ | Construct (c, u) -> ConstructRef c, u
+ | Var id -> VarRef id, []
+ | _ -> raise Not_found
+
open Declarations
let type_of_reference env r =
View
3  library/universes.mli
@@ -48,6 +48,9 @@ val fresh_global_instance : env -> Globnames.global_reference ->
val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr ->
constr in_universe_context_set
+(** Raises [Not_found] if not a global reference. *)
+val global_of_constr : constr -> Globnames.global_reference puniverses
+
val extend_context : 'a in_universe_context_set -> universe_context_set ->
'a in_universe_context_set
View
10 plugins/setoid_ring/Ring_theory.v
@@ -152,7 +152,7 @@ Section DEFINITIONS.
(** Interpretation morphisms definition*)
Section MORPHISM.
- Variable C:Set.
+ Variable C:Type.
Variable (cO cI : C) (cadd cmul csub : C->C->C) (copp : C->C).
Variable ceqb : C->C->bool.
(* [phi] est un morphisme de [C] dans [R] *)
@@ -214,7 +214,7 @@ Section DEFINITIONS.
(** Specification of the power function *)
Section POWER.
- Variable Cpow : Set.
+ Variable Cpow : Type.
Variable Cp_phi : N -> Cpow.
Variable rpow : R -> Cpow -> R.
@@ -304,7 +304,7 @@ Section ALMOST_RING.
(* a semi_morph can be extended to a ring_morph for the almost_ring derived
from a semi_ring, provided the ring is a setoid (we only need
reflexivity) *)
- Variable C : Set.
+ Variable C : Type.
Variable (cO cI : C) (cadd cmul: C->C->C).
Variable (ceqb : C -> C -> bool).
Variable phi : C -> R.
@@ -381,7 +381,7 @@ Section ALMOST_RING.
Ropp_mul_l Ropp_add (Rsub_def Rth)).
(** Every semi morphism between two rings is a morphism*)
- Variable C : Set.
+ Variable C : Type.
Variable (cO cI : C) (cadd cmul csub: C->C->C) (copp : C -> C).
Variable (ceq : C -> C -> Prop) (ceqb : C -> C -> bool).
Variable phi : C -> R.
@@ -521,7 +521,7 @@ Inductive ring_kind : Type :=
(R : Type)
(rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R)
(req : R -> R -> Prop)
- (C : Set)
+ (C : Type)
(cO cI : C) (cadd cmul csub : C->C->C) (copp : C->C)
(ceqb : C->C->bool)
phi
View
1  pretyping/evarutil.ml
@@ -234,6 +234,7 @@ let push_duplicated_evars sigma emap c =
Problem if an evar appears in the type of another one (pops anomaly) *)
let evars_to_metas sigma (emap, c) =
let emap = nf_evar_map_undefined emap in
+ let sigma = Evd.merge_universe_context sigma (Evd.evar_universe_context emap) in
let sigma',emap' = push_dependent_evars sigma emap in
let sigma',emap' = push_duplicated_evars sigma' emap' c in
(* if an evar has been instantiated in [emap] (as part of typing [c])
View
8 pretyping/evd.ml
@@ -265,7 +265,7 @@ let process_constraints vars local cstrs =
let eql, undefl, l' = nf_univ_level vars l
and eqr, undefr, r' = nf_univ_level vars r in
let eqs = Univ.LSet.union eql eqr in
- let can, noncan = if undefl then r', l else l', r in
+ let can, noncan = if undefl then r', l' else l', r' in
if undefl || undefr then
let eqs =
if Univ.Level.eq can noncan then eqs
@@ -279,7 +279,11 @@ let process_constraints vars local cstrs =
if Univ.Level.eq l' r' then local
else Univ.Constraint.add (l',d,r') local
in (vars', local')
- else (vars, Univ.Constraint.add cstr local))
+ else
+ if Univ.Level.is_small r &&
+ not (Univ.Level.is_small l || Univ.LMap.mem l vars) then
+ anomaly ("Trying to lower a rigid Type universe to a small universe")
+ else (vars, Univ.Constraint.add cstr local))
cstrs (vars, local)
let add_constraints_context ctx cstrs =
View
50 pretyping/typeclasses.ml
@@ -115,12 +115,32 @@ let _ =
Summary.unfreeze_function = unfreeze;
Summary.init_function = init }
+open Declarations
+
+let typeclass_univ_instance (cl,u') =
+ let subst =
+ let u =
+ match cl.cl_impl with
+ | ConstRef c ->
+ let cb = Global.lookup_constant c in
+ if cb.const_polymorphic then fst cb.const_universes else []
+ | IndRef c ->
+ let mib,oib = Global.lookup_inductive c in
+ if mib.mind_polymorphic then fst mib.mind_universes else []
+ | _ -> []
+ in List.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) Univ.LMap.empty u u'
+ in
+ let subst_ctx = Sign.map_rel_context (subst_univs_constr subst) in
+ { cl with cl_context = fst cl.cl_context, subst_ctx (snd cl.cl_context);
+ cl_props = subst_ctx cl.cl_props}, u'
+
let class_info c =
try Gmap.find c !classes
with _ -> not_a_class (Global.env()) (printable_constr_of_global c)
let global_class_of_constr env c =
- try class_info (global_of_constr c)
+ try let gr, u = Universes.global_of_constr c in
+ class_info gr, u
with Not_found -> not_a_class env c
let dest_class_app env c =
@@ -198,7 +218,7 @@ let discharge_class (_,cl) =
let newgrs = List.map (fun (_, _, t) ->
match class_of_constr t with
| None -> None
- | Some (_, (tc, _)) -> Some (tc.cl_impl, true))
+ | Some (_, ((tc,_), _)) -> Some (tc.cl_impl, true))
ctx'
in
List.smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs
@@ -255,7 +275,7 @@ let build_subclasses ~check env sigma glob pri =
let ty = Evarutil.nf_evar sigma (Retyping.get_type_of env sigma c) in
match class_of_constr ty with
| None -> []
- | Some (rels, (tc, args)) ->
+ | Some (rels, ((tc,u), args)) ->
let instapp =
Reductionops.whd_beta sigma (appvectc c (Termops.extended_rel_vect 0 rels))
in
@@ -267,7 +287,7 @@ let build_subclasses ~check env sigma glob pri =
| Some (Backward, _) -> None
| Some (Forward, pri') ->
let proj = Option.get proj in
- let body = it_mkLambda_or_LetIn (mkApp (mkConst proj, projargs)) rels in
+ let body = it_mkLambda_or_LetIn (mkApp (mkConstU (proj,u), projargs)) rels in
if check && check_instance env sigma body then None
else
let pri =
@@ -368,7 +388,7 @@ let remove_instance i =
let declare_instance pri local glob =
let ty = Global.type_of_global_unsafe (*FIXME*) glob in
match class_of_constr ty with
- | Some (rels, (tc, args) as _cl) ->
+ | Some (rels, ((tc,_), args) as _cl) ->
add_instance (new_instance tc pri (not local) (Flags.use_polymorphic_flag ()) glob)
(* let path, hints = build_subclasses (not local) (Global.env ()) Evd.empty glob in *)
(* let entries = List.map (fun (path, pri, c) -> (pri, local, path, c)) hints in *)
@@ -419,7 +439,7 @@ let add_inductive_class ind =
* interface functions
*)
-let instance_constructor cl args =
+let instance_constructor (cl,u) args =
let filter (_, b, _) = match b with
| None -> true
| Some _ -> false
@@ -428,16 +448,16 @@ let instance_constructor cl args =
let pars = fst (List.chop lenpars args) in
match cl.cl_impl with
| IndRef ind ->
- let ind, ctx = Universes.fresh_inductive_instance (Global.env ()) ind in
- (Some (applistc (mkConstructUi (ind, 1)) args),
- applistc (mkIndU ind) pars), ctx
+ let ind = ind, u in
+ (Some (applistc (mkConstructUi (ind, 1)) args),
+ applistc (mkIndU ind) pars)
| ConstRef cst ->
- let cst, ctx = Universes.fresh_constant_instance (Global.env ()) cst in
- let term = match args with
- | [] -> None
- | _ -> Some (List.last args)
- in
- (term, applistc (mkConstU cst) pars), ctx
+ let cst = cst, u in
+ let term = match args with
+ | [] -> None
+ | _ -> Some (List.last args)
+ in
+ (term, applistc (mkConstU cst) pars)
| _ -> assert false
let typeclasses () = Gmap.fold (fun _ l c -> l :: c) !classes []
View
15 pretyping/typeclasses.mli
@@ -59,11 +59,16 @@ val remove_instance : instance -> unit
val class_info : global_reference -> typeclass (** raises a UserError if not a class *)
-(** These raise a UserError if not a class. *)
-val dest_class_app : env -> constr -> typeclass * constr list
+(** These raise a UserError if not a class.
+ Caution: the typeclass structures is not instantiated w.r.t. the universe instance.
+ This is done separately by typeclass_univ_instance. *)
+val dest_class_app : env -> constr -> typeclass puniverses * constr list
+
+(** Get the instantiated typeclass structure for a given universe instance. *)
+val typeclass_univ_instance : typeclass puniverses -> typeclass puniverses
(** Just return None if not a class *)
-val class_of_constr : constr -> (rel_context * (typeclass * constr list)) option
+val class_of_constr : constr -> (rel_context * (typeclass puniverses * constr list)) option
val instance_impl : instance -> global_reference
@@ -75,8 +80,8 @@ val is_implicit_arg : Evar_kinds.t -> bool
(** Returns the term and type for the given instance of the parameters and fields
of the type class. *)
-val instance_constructor : typeclass -> constr list ->
- (constr option * types) Univ.in_universe_context_set
+val instance_constructor : typeclass puniverses -> constr list ->
+ constr option * types
(** Resolvability.
Only undefined evars can be marked or checked for resolvability. *)
View
1  theories/Classes/EquivDec.v
@@ -56,6 +56,7 @@ Local Open Scope program_scope.
Program Definition nequiv_dec `{EqDec A} (x y : A) : { x =/= y } + { x === y } :=
swap_sumbool (x == y).
+
(** Overloaded notation for inequality. *)
Infix "<>" := nequiv_dec (no associativity, at level 70) : equiv_scope.
View
4 toplevel/autoinstance.ml
@@ -186,7 +186,9 @@ let declare_record_instance gr ctx params =
let declare_class_instance gr ctx params =
let ident = make_instance_ident gr in
let cl = Typeclasses.class_info gr in
- let (def,typ),uctx = Typeclasses.instance_constructor cl params in
+ let c, uctx = Universes.fresh_global_instance (Global.env ()) gr in
+ let _, u = Universes.global_of_constr c in
+ let (def,typ) = Typeclasses.instance_constructor (cl,u) params in
let (def,typ) = it_mkLambda_or_LetIn (Option.get def) ctx, it_mkProd_or_LetIn typ ctx in
let ce = Entries.DefinitionEntry
{ const_entry_type = Some typ;
View
69 toplevel/classes.ml
@@ -56,7 +56,7 @@ let existing_instance glob g =
let instance = Typing.type_of (Global.env ()) Evd.empty (Universes.constr_of_global c) in
let _, r = decompose_prod_assum instance in
match class_of_constr r with
- | Some (_, (tc, _)) -> add_instance (new_instance tc None glob
+ | Some (_, ((tc,u), _)) -> add_instance (new_instance tc None glob
(*FIXME*) (Flags.use_polymorphic_flag ()) c)
| None -> user_err_loc (loc_of_reference g, "declare_instance",
Pp.str "Constant does not build instances of a declared type class.")
@@ -134,15 +134,24 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
cl
| Explicit -> cl, Idset.empty
in
- let tclass = if generalize then CGeneralization (Loc.ghost, Implicit, Some AbsPi, tclass) else tclass in
- let k, cty, ctx', ctx, len, imps, subst =
+ let tclass =
+ if generalize then CGeneralization (Loc.ghost, Implicit, Some AbsPi, tclass)
+ else tclass
+ in
+ let k, u, cty, ctx', ctx, len, imps, subst =
let impls, ((env', ctx), imps) = interp_context_evars evars env ctx in
let c', imps' = interp_type_evars_impls ~impls ~evdref:evars ~fail_evar:false env' tclass in
+ (** Abstract undefined variables in the type. *)
+ let subst = Evarutil.evd_comb0 Evd.nf_univ_variables evars in
+ let ctx = Sign.map_rel_context (Term.subst_univs_constr subst) ctx in
+ let c' = Term.subst_univs_constr subst c' in
+ let _ = evars := abstract_undefined_variables !evars in
let len = List.length ctx in
let imps = imps @ Impargs.lift_implicits len imps' in
let ctx', c = decompose_prod_assum c' in
let ctx'' = ctx' @ ctx in
- let cl, args = Typeclasses.dest_class_app (push_rel_context ctx'' env) c in
+ let k, args = Typeclasses.dest_class_app (push_rel_context ctx'' env) c in
+ let cl, u = Typeclasses.typeclass_univ_instance k in
let _, args =
List.fold_right (fun (na, b, t) (args, args') ->
match b with
@@ -150,7 +159,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
| Some b -> (args, substl args' b :: args'))
(snd cl.cl_context) (args, [])
in
- cl, c', ctx', ctx, len, imps, args
+ cl, u, c', ctx', ctx, len, imps, args
in
let id =
match snd instid with
@@ -171,8 +180,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
begin
if not (Lib.is_modtype ()) then
error "Declare Instance while not in Module Type.";
- let (_, ty_constr),uctx = instance_constructor k (List.rev subst) in
- evars := Evd.merge_context_set Evd.univ_flexible !evars uctx;
+ let (_, ty_constr) = instance_constructor (k,u) (List.rev subst) in
let termtype =
let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
Evarutil.e_nf_evars_and_universes evars t
@@ -211,28 +219,28 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
let props, rest =
List.fold_left
(fun (props, rest) (id,b,_) ->
- if Option.is_empty b then
- try
- let is_id (id', _) = match id, get_id id' with
- | Name id, (_, id') -> id_eq id id'
- | Anonymous, _ -> false
+ if Option.is_empty b then
+ try
+ let is_id (id', _) = match id, get_id id' with
+ | Name id, (_, id') -> id_eq id id'
+ | Anonymous, _ -> false
in
- let (loc_mid, c) =
- List.find is_id rest
- in
- let rest' =
- List.filter (fun v -> not (is_id v)) rest
- in
- let (loc, mid) = get_id loc_mid in
- List.iter (fun (n, _, x) ->
- if name_eq n (Name mid) then
- Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) x)
- k.cl_projs;
- c :: props, rest'
- with Not_found ->
- (CHole (Loc.ghost, Some Evar_kinds.GoalEvar) :: props), rest
- else props, rest)
- ([], props) k.cl_props
+ let (loc_mid, c) =
+ List.find is_id rest
+ in
+ let rest' =
+ List.filter (fun v -> not (is_id v)) rest
+ in
+ let (loc, mid) = get_id loc_mid in
+ List.iter (fun (n, _, x) ->
+ if name_eq n (Name mid) then
+ Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) x)
+ k.cl_projs;
+ c :: props, rest'
+ with Not_found ->
+ (CHole (Loc.ghost, Some Evar_kinds.GoalEvar) :: props), rest
+ else props, rest)
+ ([], props) k.cl_props
in
match rest with
| (n, _) :: _ ->
@@ -250,10 +258,9 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
(fun subst' s (_, b, _) -> if Option.is_empty b then s :: subst' else subst')
[] subst (k.cl_props @ snd k.cl_context)
in
- let (app, ty_constr),uctx = instance_constructor k subst in
+ let (app, ty_constr) = instance_constructor (k,u) subst in
let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
let term = Termops.it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in
- evars := Evd.merge_context_set Evd.univ_flexible !evars uctx;
Some term, termtype
| Some (Inr (def, subst)) ->
let termtype = it_mkProd_or_LetIn cty ctx in
@@ -340,7 +347,7 @@ let context l =
(ParameterEntry (None,(t,uctx),None), IsAssumption Logical)
in
match class_of_constr t with
- | Some (rels, (tc, args) as _cl) ->
+ | Some (rels, ((tc,_), args) as _cl) ->
add_instance (Typeclasses.new_instance tc None false (*FIXME*)
(Flags.use_polymorphic_flag ()) (ConstRef cst));
status
View
13 toplevel/command.ml
@@ -72,14 +72,13 @@ let interp_definition bl p red_option c ctypopt =
let env = Global.env() in
let evdref = ref (Evd.from_env env) in
let impls, ((env_bl, ctx), imps1) = interp_context_evars evdref env bl in
- let subst = evd_comb0 Evd.nf_univ_variables evdref in
- let ctx = Sign.map_rel_context (Term.subst_univs_constr subst) ctx in
- let env_bl = push_rel_context ctx env in
- (* let _ = evdref := Evd.abstract_undefined_variables !evdref in *)
let nb_args = List.length ctx in
let imps,ce =
match ctypopt with
None ->
+ let subst = evd_comb0 Evd.nf_univ_variables evdref in
+ let ctx = Sign.map_rel_context (Term.subst_univs_constr subst) ctx in
+ let env_bl = push_rel_context ctx env in
let c, imps2 = interp_constr_evars_impls ~impls ~evdref ~fail_evar:false env_bl c in
let nf = e_nf_evars_and_universes evdref in
let body = nf (it_mkLambda_or_LetIn c ctx) in
@@ -92,6 +91,10 @@ let interp_definition bl p red_option c ctypopt =
const_entry_opaque = false }
| Some ctyp ->
let ty, impsty = interp_type_evars_impls ~impls ~evdref ~fail_evar:false env_bl ctyp in
+ let subst = evd_comb0 Evd.nf_univ_variables evdref in
+ let ctx = Sign.map_rel_context (Term.subst_univs_constr subst) ctx in
+ let env_bl = push_rel_context ctx env in
+ let _ = evdref := Evd.abstract_undefined_variables !evdref in
let c, imps2 = interp_casted_constr_evars_impls ~impls ~evdref
~fail_evar:false env_bl c ty in
let nf = e_nf_evars_and_universes evdref in
@@ -356,7 +359,7 @@ let inductive_levels env evdref arities inds =
in
(** Constructors contribute. *)
let evd =
- if is_prop_sort du then
+ if is_set_sort du then
if not (Evd.check_leq evd cu Univ.type0_univ) then
raise (Indtypes.InductiveError Indtypes.LargeNonPropInductiveNotInType)
else evd
View
6 toplevel/record.ml
@@ -343,9 +343,7 @@ let declare_class finite def infer poly ctx id idbuild paramimpls params arity f
let cst = Declare.declare_constant (snd id)
(DefinitionEntry class_entry, IsDefinition Definition)
in
- let env = Global.env () in
- let evd = ref (Evd.from_env env) in
- let cstu = Evarutil.evd_comb1 (Evd.fresh_constant_instance env) evd cst in
+ let cstu = (cst, if poly then fst ctx else []) in
let inst_type = appvectc (mkConstU cstu) (Termops.rel_vect 0 (List.length params)) in
let proj_type = it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in
let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in
@@ -388,7 +386,7 @@ let declare_class finite def infer poly ctx id idbuild paramimpls params arity f
let ctx_context =
List.map (fun (na, b, t) ->
match Typeclasses.class_of_constr t with
- | Some (_, (cl, _)) -> Some (cl.cl_impl, true) (*List.exists (fun (_, n) -> n = na) supnames)*)
+ | Some (_, ((cl,_), _)) -> Some (cl.cl_impl, true) (*FIXME: ignore universes?*)
| None -> None)
params, params
in
Please sign in to comment.
Something went wrong with that request. Please try again.