Permalink
Browse files

Fix [change] forgeting about universes in the right-hand-side (#36) a…

…nd better fix for #35 and #37,

disallowing only Set/Set+1 <= Prop constraints.
  • Loading branch information...
mattam82 committed May 8, 2013
1 parent c74db8e commit 3745dbaf1fbca106d8fb0ce6a6690e64dc50e022
Showing with 37 additions and 20 deletions.
  1. +7 −2 kernel/univ.ml
  2. +2 −2 parsing/g_vernac.ml4
  3. +9 −6 pretyping/evd.ml
  4. +2 −0 pretyping/evd.mli
  5. +12 −8 proofs/logic.ml
  6. +5 −2 tactics/tacinterp.ml
View
@@ -1633,13 +1633,18 @@ let constraint_add_leq v u c =
| (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
+ if Level.is_small y then (* Set+1 <= Prop/Set *)
+ raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u, []))
+ else Constraint.add (x,Lt,y) c
else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then
if Level.eq 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
+ if Level.is_small y (* Set/Prop <= Prop/Set *)
+ && Level.is_set x && Level.is_prop y then
+ raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u, []))
+ else Constraint.add (x,Le,y) c
else (* j >= 1 *) (* m = n + k, u <= v+k *)
if Level.eq x y then c (* u <= u+k, trivial *)
else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *)
View
@@ -180,7 +180,7 @@ GEXTEND Gram
let poly = use_poly () in
VernacDefinition ((l, poly, k), id, b)
| IDENT "Let"; id = identref; b = def_body ->
- VernacDefinition ((Discharge, false, Definition), id, b)
+ VernacDefinition ((Discharge, use_poly (), Definition), id, b)
(* Gallina inductive declarations *)
| f = finite_token;
indl = LIST1 inductive_definition SEP "with" ->
@@ -746,7 +746,7 @@ GEXTEND Gram
| IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":";
expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200";
pri = OPT [ "|"; i = natural -> i ] ->
- VernacInstance (true, not (use_section_locality ()), false,
+ VernacInstance (true, not (use_section_locality ()), use_poly (),
snd namesup, (fst namesup, expl, t),
None, pri)
View
@@ -279,17 +279,15 @@ let process_universe_constraints univs postponed vars alg local cstrs =
if d = Univ.ULe then
if Univ.is_small_univ r then
(match varinfo l with
- | Inl _ -> errorlabstrm "add_constraints"
- (str"Trying to lower global universe " ++ Univ.Universe.pr l
- ++ str" to " ++ Univ.Universe.pr r)
+ | Inl _ ->
+ Univ.enforce_leq l r local, postponed
| Inr (lev, var, alg) ->
if Univ.Level.is_small lev then
if Univ.is_type0m_univ l && Univ.is_type0_univ r then
local, postponed
else (raise (Univ.UniverseInconsistency (Univ.Le, l, r, [])))
- else if var then
- Univ.enforce_leq l r local, postponed
- else (raise (Univ.UniverseInconsistency (Univ.Le, l, r, []))))
+ else
+ Univ.enforce_leq l r local, postponed)
else if Univ.check_leq univs l r then
(** Keep Prop <= var around if var might be instantiated by prop later. *)
if Univ.is_type0m_univ l && not (Univ.is_small_univ r) then
@@ -1046,6 +1044,11 @@ let test_conversion env d pb t u =
ignore(add_universe_constraints d cst); true
with _ -> false
+let e_test_conversion env d pb t u =
+ try let cst = conversion_gen env !d pb t u in
+ d := add_universe_constraints !d cst; true
+ with _ -> false
+
(**********************************************************)
(* Accessing metas *)
View
@@ -341,6 +341,8 @@ val conversion : env -> evar_map -> conv_pb -> constr -> constr -> evar_map
(** This one forgets about the assignemts of universes. *)
val test_conversion : env -> evar_map -> conv_pb -> constr -> constr -> bool
+val e_test_conversion : env -> evar_map ref -> conv_pb -> constr -> constr -> bool
+
(********************************************************************
constr with holes *)
type open_constr = evar_map * constr
View
@@ -472,17 +472,20 @@ and mk_casegoals sigma goal goalacc p c =
let convert_hyp sign sigma (id,b,bt as d) =
let env = Global.env() in
let reorder = ref [] in
+ let evd = ref sigma in
let sign' =
apply_to_hyp sign id
(fun _ (_,c,ct) _ ->
let env = Global.env_of_context sign in
- if !check && not (is_conv env sigma bt ct) then
- error ("Incorrect change of the type of "^(Id.to_string id)^".");
- if !check && not (Option.equal (is_conv env sigma) b c) then
- error ("Incorrect change of the body of "^(Id.to_string id)^".");
- if !check then reorder := check_decl_position env sign d;
- d) in
- reorder_val_context env sign' !reorder
+ if not !check then d
+ else
+ (if not (Evd.e_test_conversion env evd Reduction.CONV bt ct) then
+ error ("Incorrect change of the type of "^(Id.to_string id)^".");
+ if not (Option.equal (Evd.e_test_conversion env evd Reduction.CONV) b c) then
+ error ("Incorrect change of the body of "^(Id.to_string id)^".");
+ reorder := check_decl_position env sign d;
+ d)) in
+ !evd, reorder_val_context env sign' !reorder
@@ -648,7 +651,8 @@ let prim_refiner r sigma goal =
([sg], sigma)
| Convert_hyp (id,copt,ty) ->
- let (gl,ev,sigma) = mk_goal (convert_hyp sign sigma (id,copt,ty)) cl in
+ let sigma, hyps = convert_hyp sign sigma (id,copt,ty) in
+ let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps cl (Goal.V82.extra sigma goal) in
let sigma = Goal.V82.partial_solution sigma goal ev in
([gl], sigma)
View
@@ -1782,8 +1782,11 @@ and interp_atomic ist gl tac =
extend_gl_hyps) is incorrect. This means that evar
instantiated by pf_interp_constr may be lost, there. *)
let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
- let (_,c_interp) =
- try pf_interp_constr ist (extend_gl_hyps gl sign) c
+ let (sigma,c_interp) =
+ try
+ let sigma', c = pf_interp_constr ist (extend_gl_hyps gl sign) c in
+ let sigma = Evd.merge_universe_context sigma (Evd.evar_universe_context sigma') in
+ sigma, c
with e when to_catch e (* Hack *) ->
errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
in

0 comments on commit 3745dba

Please sign in to comment.