From 52a37da6b9e5d4e2024e31710df4e39cbd372865 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 19 Oct 2016 15:23:40 +0200 Subject: Fix a bug in error printing of unif constraints Conversion problems are in a de Bruijn environment that may include references to unbound rels (because of the way evars are created), we patch the env to named all de Bruijn variables so that error printing does not raise an anomaly. Also fix a minor printing bug in unsatisfiable constraints error reporting. HoTT_coq_117.v tests all of this. --- pretyping/evarconv.ml | 15 +++++++++------ pretyping/evd.ml | 11 +++++++++++ 2 files changed, 20 insertions(+), 6 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index d82d555f84..c538a137f2 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1158,9 +1158,14 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = (* Some head evar have been instantiated, or unknown kind of problem *) evar_conv_x ts env evd pbty t1 t2 +let error_cannot_unify env evd pb ?reason t1 t2 = + Pretype_errors.error_cannot_unify_loc + (loc_of_conv_pb evd pb) env + evd ?reason (t1, t2) + let check_problems_are_solved env evd = match snd (extract_all_conv_pbs evd) with - | (pbty,env,t1,t2)::_ -> Pretype_errors.error_cannot_unify env evd (t1, t2) + | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb t1 t2 | _ -> () let max_undefined_with_candidates evd = @@ -1229,17 +1234,15 @@ let consider_remaining_unif_problems env aux evd pbs progress (pb :: stuck) end | UnifFailure (evd,reason) -> - Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb) - env evd ~reason (t1, t2)) + error_cannot_unify env evd pb ~reason t1 t2) | _ -> if progress then aux evd stuck false [] else match stuck with | [] -> (* We're finished *) evd | (pbty,env,t1,t2 as pb) :: _ -> - (* There remains stuck problems *) - Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb) - env evd (t1, t2) + (* There remains stuck problems *) + error_cannot_unify env evd pb t1 t2 in let (evd,pbs) = extract_all_conv_pbs evd in let heuristic_solved_evd = aux evd pbs false [] in diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 0bc688aacf..2f4b8fc12f 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -840,6 +840,7 @@ let set_universe_context evd uctx' = { evd with universes = uctx' } let add_conv_pb ?(tail=false) pb d = + (** MS: we have duplicates here, why? *) if tail then {d with conv_pbs = d.conv_pbs @ [pb]} else {d with conv_pbs = pb::d.conv_pbs} @@ -1888,6 +1889,16 @@ let print_env_short env = let pr_evar_constraints pbs = let pr_evconstr (pbty, env, t1, t2) = + let env = + (** We currently allow evar instances to refer to anonymous de + Bruijn indices, so we protect the error printing code in this + case by giving names to every de Bruijn variable in the + rel_context of the conversion problem. MS: we should rather + stop depending on anonymous variables, they can be used to + indicate independency. Also, this depends on a strategy for + naming/renaming. *) + Namegen.make_all_name_different env + in print_env_short env ++ spc () ++ str "|-" ++ spc () ++ print_constr_env env t1 ++ spc () ++ str (match pbty with -- cgit v1.2.3 From 5da679d276e106a62cc3368ceb7358da289ea10a Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 24 Oct 2016 01:25:40 +0200 Subject: Complete overhaul of the Arguments vernacular. The main point of this change is to fix #3035: Avoiding trailing arguments in the Arguments command, and related issues occurring in HoTT for instance. When the "assert" flag is not specified, we now accept prefixes of the list of arguments. The semantics of _ w.r.t. to renaming has changed. Previously, it meant "restore the original name inferred from the type". Now it means "don't change the current name". The syntax of arguments is now restricted. Modifiers like /, ! and scopes are allowed only in the first arguments list. We also add *a lot* of missing checks on input values and fix various bugs. Note that this code is still way too complex for what it does, due to the complexity of the implicit arguments, reduction behaviors and renaming APIs. --- pretyping/arguments_renaming.ml | 8 ++++---- pretyping/arguments_renaming.mli | 6 +++--- 2 files changed, 7 insertions(+), 7 deletions(-) (limited to 'pretyping') diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index ca1d0b7fba..e18aece090 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -16,12 +16,12 @@ open Libobject (*i*) let name_table = - Summary.ref (Refmap.empty : Name.t list list Refmap.t) + Summary.ref (Refmap.empty : Name.t list Refmap.t) ~name:"rename-arguments" type req = | ReqLocal - | ReqGlobal of global_reference * Name.t list list + | ReqGlobal of global_reference * Name.t list let load_rename_args _ (_, (_, (r, names))) = name_table := Refmap.add r names !name_table @@ -49,7 +49,7 @@ let discharge_rename_args = function let vars,_,_ = section_segment_of_reference c in let c' = pop_global_reference c in let var_names = List.map (fun (id, _,_,_) -> Name id) vars in - let names' = List.map (fun l -> var_names @ l) names in + let names' = var_names @ names in Some (ReqGlobal (c', names), (c', names')) with Not_found -> Some req) | _ -> None @@ -83,7 +83,7 @@ let rec rename_prod c = function | _ -> c let rename_type ty ref = - try rename_prod ty (List.hd (arguments_names ref)) + try rename_prod ty (arguments_names ref) with Not_found -> ty let rename_type_of_constant env c = diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli index a334055011..e123e77862 100644 --- a/pretyping/arguments_renaming.mli +++ b/pretyping/arguments_renaming.mli @@ -11,10 +11,10 @@ open Globnames open Environ open Term -val rename_arguments : bool -> global_reference -> Name.t list list -> unit +val rename_arguments : bool -> global_reference -> Name.t list -> unit -(** [Not_found] is raised is no names are defined for [r] *) -val arguments_names : global_reference -> Name.t list list +(** [Not_found] is raised if no names are defined for [r] *) +val arguments_names : global_reference -> Name.t list val rename_type_of_constant : env -> pconstant -> types val rename_type_of_inductive : env -> pinductive -> types -- cgit v1.2.3 From 0827cf4c6de1df1ab5cdb457c2ca8de6001427f4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 29 Oct 2016 14:18:43 +0200 Subject: Fixing error localisation bug introduced in fixing #5142 (21e1d501e17c). (May it fell in the case mentioned in the inner comment of Exninfo.info?) --- pretyping/cases.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 5c9ce2624c..aa24733d9f 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -64,10 +64,11 @@ let error_wrong_numarg_inductive_loc loc env c n = let list_try_compile f l = let rec aux errors = function - | [] -> if errors = [] then anomaly (str "try_find_f") else raise (List.last errors) + | [] -> if errors = [] then anomaly (str "try_find_f") else iraise (List.last errors) | h::t -> try f h with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e -> + let e = CErrors.push e in aux (e::errors) t in aux [] l -- cgit v1.2.3