From bfce815bd1fa2c603141661b209a864c67ae1dbf Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 16 Mar 2016 18:00:25 +0100 Subject: Fix incorrect behavior of CS resolution Due to a change in pretyping, using cast annotations as typing constraints, the canonical structure problems given to the unification could contain non-evar-normalized terms, hence we force evar normalization where necessary to ensure the same CS solutions can be found. Here the dependency test is fooled by an erasable dependency, and the following resolution needs a independent codomain for pop b to be well-scoped. --- pretyping/evarconv.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 690b974be5..b8d92b9be7 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -138,6 +138,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = try match kind_of_term t2 with Prod (_,a,b) -> (* assert (l2=[]); *) + let _, a, b = destProd (Evarutil.nf_evar sigma t2) in if dependent (mkRel 1) b then raise Not_found else lookup_canonical_conversion (proji, Prod_cs), (Stack.append_app [|a;pop b|] Stack.empty) -- cgit v1.2.3 From 4849c8eb1b7a386d2abcbc80c40de34b0a69b8ea Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 16 Mar 2016 18:18:54 +0100 Subject: Test file for #4624, fixed by Matthieu's bfce815bd1. --- test-suite/bugs/4624.v | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 test-suite/bugs/4624.v diff --git a/test-suite/bugs/4624.v b/test-suite/bugs/4624.v new file mode 100644 index 0000000000..a737afcdab --- /dev/null +++ b/test-suite/bugs/4624.v @@ -0,0 +1,7 @@ +Record foo := mkfoo { type : Type }. + +Canonical Structure fooA (T : Type) := mkfoo (T -> T). + +Definition id (t : foo) (x : type t) := x. + +Definition bar := id _ ((fun x : nat => x) : _). \ No newline at end of file -- cgit v1.2.3 From 82b371aceb1ef6b1e15bdace2cf142e65724a3c6 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 17 Mar 2016 17:53:25 +0100 Subject: Fix #4623: set tactic too weak with universes (regression) The regression was introduced by efa1c32a4d178, which replaced unification by conversion when looking for more occurrences of a subterm. The conversion function called was not the right one, as it was not inferring constraints. --- pretyping/unification.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 9b6e856b80..cd0bbfa300 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1532,8 +1532,9 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = | e when Errors.noncritical e -> raise (NotUnifiable None) in let merge_fun c1 c2 = match c1, c2 with - | Some (evd,c1,_) as x, Some (_,c2,_) -> - if is_conv env sigma c1 c2 then x else raise (NotUnifiable None) + | Some (evd,c1,x), Some (_,c2,_) -> + let (evd,b) = infer_conv ~pb:CONV env evd c1 c2 in + if b then Some (evd, c1, x) else raise (NotUnifiable None) | Some _, None -> c1 | None, Some _ -> c2 | None, None -> None in -- cgit v1.2.3 From bcee0b4d6ca113d225fa7df1cbcfa33812b0bd46 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 17 Mar 2016 18:06:50 +0100 Subject: Test file for #4623. --- test-suite/bugs/4623.v | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 test-suite/bugs/4623.v diff --git a/test-suite/bugs/4623.v b/test-suite/bugs/4623.v new file mode 100644 index 0000000000..405d09809c --- /dev/null +++ b/test-suite/bugs/4623.v @@ -0,0 +1,5 @@ +Goal Type -> Type. +set (T := Type). +clearbody T. +refine (@id _). +Qed. \ No newline at end of file -- cgit v1.2.3 From c8dcfc691a649ff6dfb3416809c6ec7b1e629b1f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 17 Mar 2016 20:23:00 +0100 Subject: Fix bug #4627: records with no declared arity can be template polymorphic. As if we were adding : Type. Consistent with inductives with no declared arity. --- test-suite/bugs/closed/4627.v | 49 +++++++++++++++++++++++++++++++++++++++++++ toplevel/record.ml | 6 +++--- 2 files changed, 52 insertions(+), 3 deletions(-) create mode 100644 test-suite/bugs/closed/4627.v diff --git a/test-suite/bugs/closed/4627.v b/test-suite/bugs/closed/4627.v new file mode 100644 index 0000000000..e1206bb37a --- /dev/null +++ b/test-suite/bugs/closed/4627.v @@ -0,0 +1,49 @@ +Class sa (A:Type) := { }. + +Record predicate A (sa:sa A) := + { pred_fun: A->Prop }. +Record ABC : Type := + { abc: Type }. +Record T := + { T_abc: ABC }. + + +(* +sa: forall _ : Type@{Top.179}, Prop +predicate: forall (A : Type@{Top.205}) (_ : sa A), Type@{max(Set+1, Top.205)} +T: Type@{Top.208+1} +ABC: Type@{Top.208+1} +abc: forall _ : ABC, Type@{Top.208} + +Top.205 <= Top.179 predicate <= sa.A +Set < Top.208 Set < abc +Set < Top.205 Set < predicate +*) + +Definition foo : predicate T (Build_sa T) := + {| pred_fun:= fun w => True |}. +(* *) +(* Top.208 < Top.205 <--- added by foo *) +(* *) + +Check predicate nat (Build_sa nat). +(* + +The issue is that the template polymorphic universe of [predicate], Top.205, does not get replaced with the universe of [nat] in the above line. + -Jason Gross + +8.5 -- predicate nat (Build_sa nat): Type@{max(Set+1, Top.205)} +8.5 EXPECTED -- predicate nat (Build_sa nat): Type@{Set+1} +8.4pl4 -- predicate nat {| |}: Type (* max(Set, (Set)+1) *) +*) + +(* This works in 8.4pl4 and SHOULD work in 8.5 *) +Definition bar : ABC := + {| abc:= predicate nat (Build_sa nat) |}. +(* +The term "predicate nat (Build_sa nat)" has type + "Type@{max(Set+1, Top.205)}" +while it is expected to have type "Type@{Top.208}" +(universe inconsistency: Cannot enforce Top.205 <= +Top.208 because Top.208 < Top.205). +*) \ No newline at end of file diff --git a/toplevel/record.ml b/toplevel/record.ml index 200d1a9387..c5ae7e8913 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -114,13 +114,13 @@ let typecheck_params_and_fields def id pl t ps nots fs = (match kind_of_term sred with | Sort s' -> (match Evd.is_sort_variable !evars s' with - | Some l -> evars := Evd.make_flexible_variable !evars true (* (not def) *) l; + | Some l -> evars := Evd.make_flexible_variable !evars true l; sred, true | None -> s, false) | _ -> user_err_loc (constr_loc t,"", str"Sort expected.")) | None -> - let uvarkind = if (* not def *) true then Evd.univ_flexible_alg else Evd.univ_flexible in - mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars), false + let uvarkind = Evd.univ_flexible_alg in + mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars), true in let fullarity = it_mkProd_or_LetIn t' newps in let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in -- cgit v1.2.3 From 09c2011fbdbb2ac1ce33e5abe52d93b907b21a3c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 16:01:52 +0100 Subject: Fixing bug #4630: Some tactics are 20x slower in 8.5 than 8.4. The interpretation of arguments of tactic notations were normalizing the goal beforehand, which incurred an important time penalty. We now do this argumentwise which allows to save time in frequent cases, notably tactic arguments. --- tactics/tacinterp.ml | 56 ++++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 46 insertions(+), 10 deletions(-) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 54adbd937f..5ecc46d670 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1219,34 +1219,53 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return arg) end | _ as tag -> (** Special treatment. TODO: use generic handler *) - Ftactic.nf_enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in - let env = Proofview.Goal.env gl in match tag with | IntOrVarArgType -> + Ftactic.enter begin fun _ -> Ftactic.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x)) + end | IdentArgType -> + Ftactic.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env (Proofview.Goal.assume gl) in Ftactic.return (value_of_ident (interp_ident ist env sigma (out_gen (glbwit wit_ident) x))) + end | VarArgType -> + Ftactic.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env (Proofview.Goal.assume gl) in Ftactic.return (mk_hyp_value ist env sigma (out_gen (glbwit wit_var) x)) - | GenArgType -> f (out_gen (glbwit wit_genarg) x) + end + | GenArgType -> + Ftactic.enter begin fun _ -> + f (out_gen (glbwit wit_genarg) x) + end | ConstrArgType -> + Ftactic.nf_enter begin fun gl -> let (sigma,v) = Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) gl in Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v) + end | OpenConstrArgType -> + Ftactic.nf_enter begin fun gl -> let (sigma,v) = Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) gl in Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v) + end | ConstrMayEvalArgType -> + Ftactic.nf_enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in let (sigma,c_interp) = interp_constr_may_eval ist env sigma (out_gen (glbwit wit_constr_may_eval) x) in Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (Value.of_constr c_interp)) + end | ListArgType ConstrArgType -> + Ftactic.nf_enter begin fun gl -> let wit = glbwit (wit_list wit_constr) in let (sigma,l_interp) = Tacmach.New.of_old begin fun gl -> Evd.MonadR.List.map_right @@ -1255,22 +1274,34 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with (project gl) end gl in Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (in_gen (topwit (wit_list wit_genarg)) l_interp)) + end | ListArgType VarArgType -> + Ftactic.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env (Proofview.Goal.assume gl) in let wit = glbwit (wit_list wit_var) in Ftactic.return ( let ans = List.map (mk_hyp_value ist env sigma) (out_gen wit x) in in_gen (topwit (wit_list wit_genarg)) ans ) + end | ListArgType IntOrVarArgType -> + Ftactic.enter begin fun _ -> let wit = glbwit (wit_list wit_int_or_var) in let ans = List.map (mk_int_or_var_value ist) (out_gen wit x) in Ftactic.return (in_gen (topwit (wit_list wit_genarg)) ans) + end | ListArgType IdentArgType -> + Ftactic.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env (Proofview.Goal.assume gl) in let wit = glbwit (wit_list wit_ident) in let mk_ident x = value_of_ident (interp_ident ist env sigma x) in let ans = List.map mk_ident (out_gen wit x) in Ftactic.return (in_gen (topwit (wit_list wit_genarg)) ans) + end | ListArgType t -> + Ftactic.enter begin fun gl -> let open Ftactic in let list_unpacker wit l = let map x = @@ -1281,17 +1312,22 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with Ftactic.return (in_gen (topwit (wit_list wit)) l) in list_unpack { list_unpacker } x + end | ExtraArgType _ -> (** Special treatment of tactics *) - if has_type x (glbwit wit_tactic) then + if has_type x (glbwit wit_tactic) then + Ftactic.enter begin fun _ -> let tac = out_gen (glbwit wit_tactic) x in val_interp ist tac - else - let goal = Proofview.Goal.goal gl in - let (newsigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} x in - Ftactic.(lift (Proofview.Unsafe.tclEVARS newsigma) <*> return v) + end + else + Ftactic.nf_enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let goal = Proofview.Goal.goal gl in + let (newsigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} x in + Ftactic.(lift (Proofview.Unsafe.tclEVARS newsigma) <*> return v) + end | _ -> assert false - end in let (>>=) = Ftactic.bind in let interp_vars = -- cgit v1.2.3