diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-06-25 18:26:55 +0200 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-06-25 18:26:55 +0200 |
commit | a1fc621b943dbf904705dc88ed27c26daf4c5e72 (patch) | |
tree | 2649ab1a1480b17b74c7207113d5ae8783f2ee42 /checker | |
parent | 24279abf43cfbd65e2fc29f171eb8705fdf61a3e (diff) | |
parent | 1311a2bf08ac1deb16f0b3064bc1164d75858a97 (diff) |
Merge PR #7798: Remove hack skipping comparison of algebraic universes in subtyping.
Diffstat (limited to 'checker')
-rw-r--r-- | checker/mod_checking.ml | 27 | ||||
-rw-r--r-- | checker/subtyping.ml | 83 | ||||
-rw-r--r-- | checker/univ.ml | 42 | ||||
-rw-r--r-- | checker/univ.mli | 2 |
4 files changed, 7 insertions, 147 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index ca9581167..6b2af71f3 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -2,7 +2,6 @@ open Pp open Util open Names open Cic -open Term open Reduction open Typeops open Indtypes @@ -13,17 +12,6 @@ open Environ (** {6 Checking constants } *) -let refresh_arity ar = - let ctxt, hd = decompose_prod_assum ar in - match hd with - Sort (Type u) when not (Univ.is_univ_variable u) -> - let ul = Univ.Level.make DirPath.empty 1 in - let u' = Univ.Universe.make ul in - let cst = Univ.enforce_leq u u' Univ.empty_constraint in - let ctx = Univ.ContextSet.make (Univ.LSet.singleton ul) cst in - mkArity (ctxt,Prop Null), ctx - | _ -> ar, Univ.ContextSet.empty - let check_constant_declaration env kn cb = Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ prcon kn); (** Locally set the oracle for further typechecking *) @@ -37,18 +25,13 @@ let check_constant_declaration env kn cb = let ctx = Univ.AUContext.repr auctx in push_context ~strict:false ctx env in - let envty, ty = - let ty = cb.const_type in - let ty', cu = refresh_arity ty in - let envty = push_context_set cu env' in - let _ = infer_type envty ty' in - envty, ty - in - let () = + let ty = cb.const_type in + let _ = infer_type env' ty in + let () = match body_of_constant cb with | Some bd -> - let j = infer envty bd in - conv_leq envty j ty + let j = infer env' bd in + conv_leq env' j ty | None -> () in let env = diff --git a/checker/subtyping.ml b/checker/subtyping.ml index a22af4e0f..6d0d6f6c6 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -9,7 +9,6 @@ (************************************************************************) (*i*) -open CErrors open Util open Names open Cic @@ -132,40 +131,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= check (eq_constr) (fun x -> x.proj_type); true in - let check_inductive_type 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 *) Prop Null, Prop Null - | (Prop _, Type _) | (Type _,Prop _) -> error () - | _ -> (s1, s2) in - check_conv conv_leq env - (mkArity (ctx1,s1)) (mkArity (ctx2,s2)) - in + let check_inductive_type t1 t2 = check_conv conv_leq env t1 t2 in let check_packet p1 p2 = let check eq f = if not (eq (f p1) (f p2)) then error () in @@ -254,52 +220,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let error () = error_not_match l spec2 in let check_conv f = check_conv_error error f in - let check_type env t1 t2 = - - (* 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 (Univ.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 (Univ.is_univ_variable u) -> - (* Both types are inferred, no need to recheck them. We - cheat and collapse the types to Prop *) - mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null) - | 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,Prop Null), mkArity (ctx2,Prop Null) - | 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 () - with UserError _ (* "not an arity" *) -> - error () end - | _ -> t1,t2 - else - (t1,t2) in - check_conv conv_leq env t1 t2 - in + let check_type env t1 t2 = check_conv conv_leq env t1 t2 in match info1 with | Constant cb1 -> let cb1 = subst_const_body subst1 cb1 in diff --git a/checker/univ.ml b/checker/univ.ml index 15673736f..e50e883ad 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -190,13 +190,6 @@ struct (let (u,n) = x and (v,n') = y in Int.equal n n' && Level.equal u v) - let leq (u,n) (v,n') = - let cmp = Level.compare u v in - if Int.equal cmp 0 then n <= n' - else if n <= n' then - (Level.is_prop u && Level.is_small v) - else false - let successor (u,n) = if Level.is_prop u then type1 else (u, n + 1) @@ -833,41 +826,6 @@ type 'a constrained = 'a * constraints type 'a constraint_function = 'a -> 'a -> constraints -> constraints -let constraint_add_leq v u c = - (* We just discard trivial constraints like u<=u *) - if Expr.equal v u then c - else - match v, u with - | (x,n), (y,m) -> - let j = m - n in - if j = -1 (* n = m+1, v+1 <= u <-> v < u *) then - Constraint.add (x,Lt,y) c - else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then - if Level.equal x y then (* u+(k+1) <= u *) - raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u)) - else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints.") - else if j = 0 then - Constraint.add (x,Le,y) 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.") - -let check_univ_leq_one u v = Universe.exists (Expr.leq u) v - -let check_univ_leq u v = - Universe.for_all (fun u -> check_univ_leq_one u v) u - -let enforce_leq u v c = - match v with - | [v] -> - List.fold_right (fun u -> constraint_add_leq u v) u c - | _ -> anomaly (Pp.str"A universe bound can only be a variable.") - -let enforce_leq u v c = - if check_univ_leq u v then c - else enforce_leq u v c - let check_constraint g (l,d,r) = match d with | Eq -> check_equal g l r diff --git a/checker/univ.mli b/checker/univ.mli index 6cd3b3638..3b29b158f 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -109,8 +109,6 @@ type 'a constrained = 'a * constraints type 'a constraint_function = 'a -> 'a -> constraints -> constraints -val enforce_leq : universe constraint_function - (** {6 ... } *) (** Merge of constraints in a universes graph. The function [merge_constraints] merges a set of constraints in a given |