diff options
Diffstat (limited to 'pretyping')
56 files changed, 172 insertions, 117 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 5e2284e1..a145508a 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli index a484ecf7..a4121623 100644 --- a/pretyping/arguments_renaming.mli +++ b/pretyping/arguments_renaming.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 9ed28f8b..1819dc52 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/cases.mli b/pretyping/cases.mli index f773da0e..566c172d 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index ad33bae1..9429086c 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index acaf7e49..08e52ff7 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 62d774bd..ddc99e0e 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 66bb5c6c..675ccbbc 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index bfa0034f..bdf94e0d 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index 5d814b29..4c4725b3 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index aae003b8..69ff2af9 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 40e3d0f8..cd017ba7 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index fa45f6fb..14f35941 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -579,8 +579,8 @@ let choose_less_dependent_instance evk evd term args = let evi = Evd.find_undefined evd evk in let subst = make_pure_subst evi args in let subst' = List.filter (fun (id,c) -> eq_constr c term) subst in - if subst' = [] then error "Too complex unification problem." else - Evd.define evk (mkVar (fst (List.hd subst'))) evd + if subst' = [] then evd, false else + Evd.define evk (mkVar (fst (List.hd subst'))) evd, true let apply_on_subterm f c t = let rec applyrec (k,c as kc) t = @@ -733,12 +733,12 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = & array_for_all (fun a -> eq_constr a term2 or isEvar a) args1 -> (* The typical kind of constraint coming from pattern-matching return type inference *) - choose_less_dependent_instance evk1 evd term2 args1, true + choose_less_dependent_instance evk1 evd term2 args1 | (Rel _|Var _), Evar (evk2,args2) when l1 = [] & l2 = [] & array_for_all (fun a -> eq_constr a term1 or isEvar a) args2 -> (* The typical kind of constraint coming from pattern-matching return type inference *) - choose_less_dependent_instance evk2 evd term1 args2, true + choose_less_dependent_instance evk2 evd term1 args2 | Evar (evk1,args1), Evar (evk2,args2) when evk1 = evk2 -> let f env evd pbty x y = (evd,is_trans_fconv pbty ts env evd x y) in solve_refl ~can_drop:true f env evd evk1 args1 args2, true @@ -818,14 +818,30 @@ let solve_unconstrained_impossible_cases evd = | _,ImpossibleCase -> Evd.define evk (j_type (coq_unit_judge ())) evd' | _ -> evd') evd evd + let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd = let evd = solve_unconstrained_evars_with_canditates evd in - let (evd,pbs) = extract_all_conv_pbs evd in - let heuristic_solved_evd = List.fold_left - (fun evd (pbty,env,t1,t2) -> + let rec aux evd pbs progress stuck = + match pbs with + | (pbty,env,t1,t2 as pb) :: pbs -> let evd', b = apply_conversion_problem_heuristic ts env evd pbty t1 t2 in - if b then evd' else Pretype_errors.error_cannot_unify env evd (t1, t2)) - evd pbs in + if b then + let (evd', rest) = extract_all_conv_pbs evd' in + if rest = [] then aux evd' pbs true stuck + else (* Unification got actually stuck, postpone *) + aux evd pbs progress (pb :: stuck) + else Pretype_errors.error_cannot_unify env evd (t1, t2) + | _ -> + if progress then aux evd stuck false [] + else + match stuck with + | [] -> (* We're finished *) evd + | (pbty,env,t1,t2) :: _ -> + (* There remains stuck problems *) + Pretype_errors.error_cannot_unify env evd (t1, t2) + in + let (evd,pbs) = extract_all_conv_pbs evd in + let heuristic_solved_evd = aux evd pbs false [] in check_problems_are_solved env heuristic_solved_evd; solve_unconstrained_impossible_cases heuristic_solved_evd diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 3e2ca7ae..dd68f16f 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 689fab50..fa29243a 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -145,6 +145,11 @@ let noccur_evar evd evk c = in try occur_rec c; true with Occur -> false +let normalize_evar evd ev = + match kind_of_term (whd_evar evd (mkEvar ev)) with + | Evar (evk,args) -> (evk,args) + | _ -> assert false + (**********************) (* Creating new metas *) (**********************) @@ -1591,6 +1596,8 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs = let ty = get_type_of env' !evdref t in let (evd,evar'',ev'') = materialize_evar (evar_define conv_algo) env' !evdref k ev ty in + (* materialize_evar may instantiate ev' by another evar; adjust it *) + let (evk',args' as ev') = normalize_evar evd ev' in let evd = (* Try to project (a restriction of) the left evar ... *) try @@ -1772,44 +1779,50 @@ let evars_of_term c = in evrec Intset.empty c -(* spiwack: a few functions to gather the existential variables - that occur in the types of goals present or past. *) -let add_evars_of_evars_of_term acc evm c = - let evars = evars_of_term c in - Intset.fold begin fun e r -> - let body = (Evd.find evm e).evar_body in - let subevars = - match body with - | Evar_empty -> None - | Evar_defined c' -> Some (evars_of_term c') - in - Intmap.add e subevars r - end evars acc - -let evars_of_evars_of_term = add_evars_of_evars_of_term Intmap.empty +(* spiwack: a few functions to gather evars on which goals depend. *) +let queue_set q is_dependent set = + Intset.iter (fun a -> Queue.push (is_dependent,a) q) set +let queue_term q is_dependent c = + queue_set q is_dependent (evars_of_term c) -let add_evars_of_evars_in_type acc evm e = +let process_dependent_evar q acc evm is_dependent e = let evi = Evd.find evm e in - let acc_with_concl = add_evars_of_evars_of_term acc evm evi.evar_concl in - let hyps = Environ.named_context_of_val evi.evar_hyps in - List.fold_left begin fun r (_,b,t) -> - let r = add_evars_of_evars_of_term r evm t in + (* Queues evars appearing in the types of the goal (conclusion, then + hypotheses), they are all dependent. *) + queue_term q true evi.evar_concl; + List.iter begin fun (_,b,t) -> + queue_term q true t; match b with - | None -> r - | Some b -> add_evars_of_evars_of_term r evm b - end acc_with_concl hyps - -let rec add_evars_of_evars_in_types_of_set acc evm s = - Intset.fold begin fun e r -> - let r = add_evars_of_evars_in_type r evm e in - match (Evd.find evm e).evar_body with - | Evar_empty -> r - | Evar_defined b -> add_evars_of_evars_in_types_of_set r evm (evars_of_term b) - end s acc - -let evars_of_evars_in_types_of_list evm l = - let set_of_l = List.fold_left (fun x y -> Intset.add y x) Intset.empty l in - add_evars_of_evars_in_types_of_set Intmap.empty evm set_of_l + | None -> () + | Some b -> queue_term q true b + end (Environ.named_context_of_val evi.evar_hyps); + match evi.evar_body with + | Evar_empty -> + if is_dependent then Intmap.add e None acc else acc + | Evar_defined b -> + let subevars = evars_of_term b in + (* evars appearing in the definition of an evar [e] are marked + as dependent when [e] is dependent itself: if [e] is a + non-dependent goal, then, unless they are reach from another + path, these evars are just other non-dependent goals. *) + queue_set q is_dependent subevars; + if is_dependent then Intmap.add e (Some subevars) acc else acc + +let gather_dependent_evars q evm = + let acc = ref Intmap.empty in + while not (Queue.is_empty q) do + let (is_dependent,e) = Queue.pop q in + (* checks if [e] has already been added to [!acc] *) + begin if not (Intmap.mem e !acc) then + acc := process_dependent_evar q !acc evm is_dependent e + end + done; + !acc + +let gather_dependent_evars evm l = + let q = Queue.create () in + List.iter (fun a -> Queue.add (false,a) q) l; + gather_dependent_evars q evm (* /spiwack *) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index d3f6845c..2b326fd1 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -119,21 +119,19 @@ val solve_pattern_eqn : env -> constr list -> constr -> constr val evars_of_term : constr -> Intset.t -(** returns the evars contained in the term associated with - the evars they contain themselves in their body, if any. - If the evar has no body, [None] is associated to it. *) -val evars_of_evars_of_term : evar_map -> constr -> (Intset.t option) Intmap.t val evars_of_named_context : named_context -> Intset.t val evars_of_evar_info : evar_info -> Intset.t -(** returns the evars which can be found in the typing context of the argument evars, - in the same format as {!evars_of_evars_of_term}. - It explores recursively the evars in the body of the argument evars -- but does - not return them. *) -(* spiwack: tongue in cheek: it should have been called - [evars_of_evars_in_types_of_list_and_recursively_in_bodies] *) -val evars_of_evars_in_types_of_list : evar_map -> evar list -> (Intset.t option) Intmap.t - +(** [gather_dependent_evars evm seeds] classifies the evars in [evm] + as dependent_evars and goals (these may overlap). A goal is an + evar in [seeds] or an evar appearing in the (partial) definition + of a goal. A dependent evar is an evar appearing in the type + (hypotheses and conclusion) of a goal, or in the type or (partial) + definition of a dependent evar. The value return is a map + associating to each dependent evar [None] if it has no (partial) + definition or [Some s] if [s] is the list of evars appearing in + its (partial) definition. *) +val gather_dependent_evars : evar_map -> evar list -> (Intset.t option) Intmap.t (** The following functions return the set of undefined evars contained in the object, the defined evars being traversed. diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 3cfad524..6d5c98ce 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 194880e2..4813d3b9 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index a4113671..24c5ba5b 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli index 7fb995a8..798a960f 100644 --- a/pretyping/glob_term.mli +++ b/pretyping/glob_term.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index a0976029..18d30bfd 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index a421ae7d..1bf5fd90 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 0b59fc40..bb0a0e92 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index f361e8b8..91662fd9 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 7a745118..89ca95cb 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/matching.mli b/pretyping/matching.mli index 49033286..9b412692 100644 --- a/pretyping/matching.mli +++ b/pretyping/matching.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index 23af7a63..e5dd75c0 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli index 6ca03146..e23c6dad 100644 --- a/pretyping/namegen.mli +++ b/pretyping/namegen.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 65f342d8..7e486956 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index cde6d4dc..f6d55bc6 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 2cf16791..672debfa 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 3a3dccb4..68ea67f7 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index d0c9df51..d8678371 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -319,6 +319,18 @@ module Pretyping_F (Coercion : Coercion.S) = struct let pretype_ref evdref env ref = let c = constr_of_global ref in make_judge c (Retyping.get_type_of env Evd.empty c) + let pretype_ref loc evdref env = function + | VarRef id -> + (* Section variable *) + (try let (_,_,ty) = lookup_named id env in make_judge (mkVar id) ty + with Not_found -> + (* This may happen if env is a goal env and section variables have + been cleared - section variables should be different from goal + variables *) + Pretype_errors.error_var_not_found_loc loc id) + | ref -> + let c = constr_of_global ref in + make_judge c (Retyping.get_type_of env Evd.empty c) let pretype_sort evdref = function | GProp c -> judge_of_prop_contents c @@ -335,7 +347,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let rec pretype (tycon : type_constraint) env evdref lvar = function | GRef (loc,ref) -> inh_conv_coerce_to_tycon loc env evdref - (pretype_ref evdref env ref) + (pretype_ref loc evdref env ref) tycon | GVar (loc, id) -> diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index b79e9489..761e1641 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index b3be7afd..0f04549f 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 6165fac2..1c19ef6c 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index e8acd67c..fddc7fc7 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 3ffc587e..6f7f9de3 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 502e238b..f16eed6c 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 445f623a..62bda6ef 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 6a26027c..b43b9adb 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 8fd14dcc..f2a4c303 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml index 98091087..3340dbe2 100644 --- a/pretyping/term_dnet.ml +++ b/pretyping/term_dnet.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/term_dnet.mli b/pretyping/term_dnet.mli index a2c535d1..bf4557fc 100644 --- a/pretyping/term_dnet.mli +++ b/pretyping/term_dnet.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 6371fd3a..0e31ee2d 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 5448d97c..0e384829 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 4471e68d..b78850d3 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 4e6081e2..c458e5d5 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index ab7bb9dc..19e18489 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index 79f0678f..cb67c73d 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index efcdff9d..665491e7 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 224fd995..88dc895e 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index eaa83146..c92c183d 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -37,6 +37,15 @@ let occur_meta_or_undefined_evar evd c = | _ -> iter_constr occrec c in try occrec c; false with Occur | Not_found -> true +let occur_meta_evd sigma mv c = + let rec occrec c = + (* Note: evars are not instantiated by terms with metas *) + let c = whd_evar sigma (whd_meta sigma c) in + match kind_of_term c with + | Meta mv' when mv = mv' -> raise Occur + | _ -> iter_constr occrec c + in try occrec c; false with Occur -> true + (* if lname_typ is [xn,An;..;x1,A1] and l is a list of terms, gives [x1:A1]..[xn:An]c' such that c converts to ([x1:A1]..[xn:An]c' l) *) @@ -388,7 +397,8 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag check_compatibility curenv substn tyM tyN); if k2 < k1 then sigma,(k1,cN,stN)::metasubst,evarsubst else sigma,(k2,cM,stM)::metasubst,evarsubst - | Meta k, _ when not (dependent cM cN) -> + | Meta k, _ + when not (dependent cM cN) (* helps early trying alternatives *) -> if wt && flags.check_applied_meta_types then (let tyM = Typing.meta_type sigma k in let tyN = get_type_of curenv sigma cN in @@ -401,7 +411,8 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag (k,lift (-nb) cN,snd (extract_instance_status pb))::metasubst, evarsubst) else error_cannot_unify_local curenv sigma (m,n,cN) - | _, Meta k when not (dependent cN cM) -> + | _, Meta k + when not (dependent cN cM) (* helps early trying alternatives *) -> if wt && flags.check_applied_meta_types then (let tyM = get_type_of curenv sigma cM in let tyN = Typing.meta_type sigma k in @@ -904,8 +915,13 @@ let w_merge env with_types flags (evd,metas,evars) = in w_merge_rec evd' (metas'@metas@metas'') (evars'@evars'') eqns else - let evd' = meta_assign mv (c,(status,TypeProcessed)) evd in - w_merge_rec evd' (metas''@metas) evars'' eqns + let evd' = + if occur_meta_evd evd mv c then + if isMetaOf mv (whd_betadeltaiota env evd c) then evd + else error_cannot_unify env evd (mkMeta mv,c) + else + meta_assign mv (c,(status,TypeProcessed)) evd in + w_merge_rec evd' (metas''@metas) evars'' eqns | [] -> (* Process type eqns *) let rec process_eqns failures = function diff --git a/pretyping/unification.mli b/pretyping/unification.mli index e4bca4d3..e3fd46af 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index ac3df714..00efa981 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli index ee946e53..ca370b55 100644 --- a/pretyping/vnorm.mli +++ b/pretyping/vnorm.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |