diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-10 23:33:42 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-11 14:50:47 +0200 |
commit | e1d4ad82b1557a8cf808e0374ece9c39ed349ea2 (patch) | |
tree | 6539da95794f0029d90e60460c1aaca9b8ddafeb /kernel | |
parent | 012f5fb722a9d5dcef82c800aa54ed50c0a58957 (diff) |
Cleaning up the implementation of module subtyping in the kernel.
We export a function in UGraph to check that a polymorphic instance is
a subtype of another, instead of rolling up our own in module code.
We also add a few tests for module subtyping in presence of polymorphic
constants.
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/mod_typing.ml | 27 | ||||
-rw-r--r-- | kernel/subtyping.mli | 2 | ||||
-rw-r--r-- | kernel/uGraph.ml | 12 | ||||
-rw-r--r-- | kernel/uGraph.mli | 4 | ||||
-rw-r--r-- | kernel/univ.ml | 3 | ||||
-rw-r--r-- | kernel/univ.mli | 6 |
6 files changed, 33 insertions, 21 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 71c037008..69fbd0f32 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -92,37 +92,28 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = c, Reduction.infer_conv env' (Environ.universes env') c c' in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx) | Polymorphic_const uctx -> - let uctx = Univ.instantiate_univ_context uctx in - let cus, ccst = Univ.UContext.dest uctx in - let newus, cst = Univ.UContext.dest ctx in - let () = - if not (Univ.Instance.length cus == Univ.Instance.length newus) then - error_incorrect_with_constraint lab - in - let inst = Univ.Instance.append cus newus in - let csti = Univ.enforce_eq_instances cus newus cst in - let csta = Univ.Constraint.union csti ccst in - let env' = Environ.push_context ~strict:false (Univ.UContext.make (inst, csta)) env in - let () = if not (UGraph.check_constraints cst (Environ.universes env')) then - error_incorrect_with_constraint lab - in + let subst, ctx = Univ.abstract_universes ctx in + let c = Vars.subst_univs_level_constr subst c in + let () = + if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then + error_incorrect_with_constraint lab + in + let env' = Environ.push_context ~strict:false (Univ.AUContext.repr uctx) env in let cst = match cb.const_body with | Undef _ | OpaqueDef _ -> let j = Typeops.infer env' c in let typ = Typeops.type_of_constant_type env' cb.const_type in - let typ = Vars.subst_instance_constr cus typ in let cst' = Reduction.infer_conv_leq env' (Environ.universes env') j.uj_type typ in cst' | Def cs -> - let c' = Vars.subst_instance_constr cus (Mod_subst.force_constr cs) in + let c' = Mod_subst.force_constr cs in let cst' = Reduction.infer_conv env' (Environ.universes env') c c' in cst' in if not (Univ.Constraint.is_empty cst) then error_incorrect_with_constraint lab; - let subst, ctx = Univ.abstract_universes ctx in - Vars.subst_univs_level_constr subst c, Polymorphic_const ctx, Univ.ContextSet.empty + c, Polymorphic_const ctx, Univ.ContextSet.empty in let def = Def (Mod_subst.from_val c') in (* let ctx' = Univ.UContext.make (newus, cst) in *) diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli index 6590d7e71..b24c20aa0 100644 --- a/kernel/subtyping.mli +++ b/kernel/subtyping.mli @@ -11,5 +11,3 @@ open Declarations open Environ val check_subtypes : env -> module_type_body -> module_type_body -> constraints - - diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 487257a77..9793dd881 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -830,6 +830,18 @@ let sort_universes g = in normalize_universes g +(** Subtyping of polymorphic contexts *) + +let check_subtype univs ctxT ctx = + if AUContext.size ctx == AUContext.size ctx then + let (inst, cst) = UContext.dest (AUContext.repr ctx) in + let cstT = UContext.constraints (AUContext.repr ctxT) in + let push accu v = add_universe v false accu in + let univs = Array.fold_left push univs (Instance.to_array inst) in + let univs = merge_constraints cstT univs in + check_constraints cst univs + else false + (** Instances *) let check_eq_instances g t1 t2 = diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index 935a3cab4..4de373eb4 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -53,6 +53,10 @@ val check_constraints : constraints -> universes -> bool val check_eq_instances : Instance.t check_function (** Check equality of instances w.r.t. a universe graph *) +val check_subtype : AUContext.t check_function +(** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of + [ctx1]. *) + (** {6 Pretty-printing of universes. } *) val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds diff --git a/kernel/univ.ml b/kernel/univ.ml index cb19761b3..6614d6027 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1060,6 +1060,9 @@ module AUContext = struct include UContext + let repr (inst, cst) = + (Array.mapi (fun i l -> Level.var i) inst, cst) + let instantiate inst (u, cst) = assert (Array.length u = Array.length inst); subst_instance_constraints inst cst diff --git a/kernel/univ.mli b/kernel/univ.mli index 3d0d2234d..9d93ec26c 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -319,11 +319,15 @@ module AUContext : sig type t + val repr : t -> UContext.t + (** [repr ctx] is [(Var(0), ... Var(n-1) |= cstr] where [n] is the length of + the context and [cstr] the abstracted constraints. *) + val empty : t val is_empty : t -> bool val instance : t -> Instance.t - + val size : t -> int (** Keeps the order of the instances *) |