From c14f134c00cef3dbca8c4a66f9847094f3fd119c Mon Sep 17 00:00:00 2001 From: msozeau Date: Sun, 7 Mar 2010 18:49:23 +0000 Subject: Fix treatment of remaining unification constraints: raise a more informative exception if some constraints do not unify. All calls except one used to raise a less informative exception when the constraints weren't solved. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12849 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/subtac/subtac_command.ml | 2 +- plugins/subtac/subtac_pretyping.ml | 2 +- plugins/subtac/subtac_pretyping_F.ml | 8 ++++---- pretyping/clenv.ml | 2 +- pretyping/evarconv.ml | 8 ++++---- pretyping/evarconv.mli | 2 +- pretyping/pretyping.ml | 16 +++++++++------- pretyping/unification.ml | 11 +++-------- toplevel/command.ml | 6 +++--- toplevel/record.ml | 2 +- 10 files changed, 28 insertions(+), 31 deletions(-) diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index a2dd7d777..f51dd5409 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -453,7 +453,7 @@ let interp_recursive fixkind l boxed = let fixdefs = List.map out_def fixdefs in (* Instantiate evars and check all are resolved *) - let evd,_ = Evarconv.consider_remaining_unif_problems env_rec !evdref in + let evd = Evarconv.consider_remaining_unif_problems env_rec !evdref in let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:false env_rec evd in diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml index 54f7aff1b..775397124 100644 --- a/plugins/subtac/subtac_pretyping.ml +++ b/plugins/subtac/subtac_pretyping.ml @@ -70,7 +70,7 @@ let merge_evms x y = let interp env isevars c tycon = let j = pretype tycon env isevars ([],[]) c in let _ = isevars := Evarutil.nf_evar_map !isevars in - let evd,_ = consider_remaining_unif_problems env !isevars in + let evd = consider_remaining_unif_problems env !isevars in (* let unevd = undefined_evars evd in *) let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:true env evd in let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:false ~split:true ~fail:false env unevd' in diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml index f909f9e0a..47882e771 100644 --- a/plugins/subtac/subtac_pretyping_F.ml +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -576,11 +576,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (pretype tycon env evdref lvar c).uj_val | IsType -> (pretype_type empty_valcon env evdref lvar c).utj_val in - evdref := fst (consider_remaining_unif_problems env !evdref); + evdref := consider_remaining_unif_problems env !evdref; if resolve_classes then - evdref := - Typeclasses.resolve_typeclasses ~onlyargs:false + (evdref := Typeclasses.resolve_typeclasses ~onlyargs:false ~split:true ~fail:fail_evar env !evdref; + evdref := consider_remaining_unif_problems env !evdref); let c = if expand_evar then nf_evar !evdref c' else c' in if fail_evar then check_evars env Evd.empty !evdref c; c @@ -593,7 +593,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let understand_judgment sigma env c = let evdref = ref (create_evar_defs sigma) in let j = pretype empty_tycon env evdref ([],[]) c in - let evd,_ = consider_remaining_unif_problems env !evdref in + let evd = consider_remaining_unif_problems env !evdref in let j = j_nf_evar evd j in check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); j diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 99e3c4e1d..7cbaf124a 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -128,7 +128,7 @@ let clenv_conv_leq env sigma t c bound = let evd = Evd.create_goal_evar_defs sigma in let evars,args,_ = clenv_environments_evars env evd (Some bound) ty in let evars = Evarconv.the_conv_x_leq env t (applist (c,args)) evars in - let evars,_ = Evarconv.consider_remaining_unif_problems env evars in + let evars = Evarconv.consider_remaining_unif_problems env evars in let args = List.map (whd_evar evars) args in check_evars env sigma evars (applist (c,args)); args diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 10f4db77a..370904a68 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -553,10 +553,10 @@ let apply_conversion_problem_heuristic env evd pbty t1 t2 = let consider_remaining_unif_problems env evd = let (evd,pbs) = extract_all_conv_pbs evd in List.fold_left - (fun (evd,b as p) (pbty,env,t1,t2) -> - if b then apply_conversion_problem_heuristic env evd pbty t1 t2 else p) - (evd,true) - pbs + (fun evd (pbty,env,t1,t2) -> + let evd', b = apply_conversion_problem_heuristic env evd pbty t1 t2 in + if b then evd' else Pretype_errors.error_cannot_unify env evd (t1, t2)) + evd pbs (* Main entry points *) diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 9a4247bc2..28b960bb9 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -34,7 +34,7 @@ val evar_eqappr_x : evar_map * bool (*i*) -val consider_remaining_unif_problems : env -> evar_map -> evar_map * bool +val consider_remaining_unif_problems : env -> evar_map -> evar_map val check_conv_record : constr * types list -> constr * types list -> constr * constr list * (constr list * constr list) * diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index cfe028aa5..bed4d834d 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -674,15 +674,17 @@ module Pretyping_F (Coercion : Coercion.S) = struct let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in (pretype tycon env evdref lvar c).uj_val | IsType -> - (pretype_type empty_valcon env evdref lvar c).utj_val in - evdref := fst (consider_remaining_unif_problems env !evdref); - if resolve_classes then + (pretype_type empty_valcon env evdref lvar c).utj_val + in + if resolve_classes then ( + evdref := consider_remaining_unif_problems env !evdref; evdref := Typeclasses.resolve_typeclasses ~onlyargs:false - ~split:true ~fail:fail_evar env !evdref; + ~split:true ~fail:fail_evar env !evdref); + evdref := consider_remaining_unif_problems env !evdref; let c = if expand_evar then nf_evar !evdref c' else c' in - if fail_evar then check_evars env Evd.empty !evdref c; - c + if fail_evar then check_evars env Evd.empty !evdref c; + c (* TODO: comment faire remonter l'information si le typage a resolu des variables du sigma original. il faudrait que la fonction de typage @@ -692,7 +694,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let understand_judgment sigma env c = let evdref = ref (create_evar_defs sigma) in let j = pretype empty_tycon env evdref ([],[]) c in - let evd,_ = consider_remaining_unif_problems env !evdref in + let evd = consider_remaining_unif_problems env !evdref in let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:false ~fail:true env evd in diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 32b51eac4..438a58469 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -554,12 +554,9 @@ let pose_all_metas_as_evars env evd t = let try_to_coerce env evd c cty tycon = let j = make_judge c cty in let (evd',j') = inh_conv_coerce_rigid_to dummy_loc env evd j tycon in - let (evd',b) = Evarconv.consider_remaining_unif_problems env evd' in - if b then - let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in + let evd' = Evarconv.consider_remaining_unif_problems env evd' in + let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in (evd',j'.uj_val) - else - error "Cannot solve unification constraints" let w_coerce_to_type env evd c cty mvty = let evd,mvty = pose_all_metas_as_evars env evd mvty in @@ -615,9 +612,7 @@ let order_metas metas = let solve_simple_evar_eqn env evd ev rhs = let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (None,ev,rhs) in if not b then error_cannot_unify env evd (mkEvar ev,rhs); - let (evd,b) = Evarconv.consider_remaining_unif_problems env evd in - if not b then error "Cannot solve unification constraints"; - evd + Evarconv.consider_remaining_unif_problems env evd (* [w_merge env sigma b metas evars] merges common instances in metas or in evars, possibly generating new unification problems; if [b] diff --git a/toplevel/command.ml b/toplevel/command.ml index 75f0daa7f..51c7e50a4 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -256,9 +256,9 @@ let interp_mutual_inductive (paramsl,indl) notations finite = () in (* Instantiate evars and check all are resolved *) - let evd,_ = consider_remaining_unif_problems env_params !evdref in + let evd = consider_remaining_unif_problems env_params !evdref in let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env_params evd in - let sigma = evd in + let sigma = evd in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in let arities = List.map (nf_evar sigma) arities in @@ -522,7 +522,7 @@ let interp_recursive isfix fixl notations = () in (* Instantiate evars and check all are resolved *) - let evd,_ = consider_remaining_unif_problems env_rec !evdref in + let evd = consider_remaining_unif_problems env_rec !evdref in let fixdefs = List.map (Option.map (nf_evar evd)) fixdefs in let fixtypes = List.map (nf_evar evd) fixtypes in let fixctxlength = List.map (fun (_,ctx) -> rel_context_nhyps ctx) fixctxs in diff --git a/toplevel/record.ml b/toplevel/record.ml index 0353261b9..c1c1a9671 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -68,7 +68,7 @@ let typecheck_params_and_fields id t ps nots fs = let env2,impls,newfs,data = interp_fields_evars evars env_ar nots (binders_of_decls fs) in - let evars,_ = Evarconv.consider_remaining_unif_problems env_ar !evars in + let evars = Evarconv.consider_remaining_unif_problems env_ar !evars in let evars = Typeclasses.resolve_typeclasses env_ar evars in let sigma = evars in let newps = Evarutil.nf_rel_context_evar sigma newps in -- cgit v1.2.3