From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 1 Feb 2009 00:54:40 +0100 Subject: Imported Upstream version 8.2~rc2+dfsg --- pretyping/cases.ml | 9 +- pretyping/evarconv.ml | 25 ++--- pretyping/evarutil.ml | 170 ++++++++++++++++++++++------ pretyping/evarutil.mli | 13 ++- pretyping/evd.ml | 9 +- pretyping/evd.mli | 10 +- pretyping/indrec.ml | 15 ++- pretyping/indrec.mli | 5 +- pretyping/inductiveops.ml | 54 ++++++++- pretyping/inductiveops.mli | 7 +- pretyping/matching.ml | 268 +++++++++++++++++++++++++-------------------- pretyping/matching.mli | 42 +++++-- pretyping/pretyping.ml | 39 ++++--- pretyping/rawterm.ml | 4 +- pretyping/recordops.ml | 19 ++-- pretyping/recordops.mli | 13 ++- pretyping/reductionops.ml | 40 +++++-- pretyping/retyping.ml | 28 ++++- pretyping/retyping.mli | 4 +- pretyping/tacred.ml | 155 ++++++++++++++++++++------ pretyping/termops.ml | 43 ++++++-- pretyping/termops.mli | 16 ++- pretyping/typeclasses.ml | 109 +++++++++--------- pretyping/typeclasses.mli | 22 ++-- pretyping/unification.ml | 189 ++++++++++++++++++++------------ pretyping/vnorm.ml | 19 ++-- 26 files changed, 905 insertions(+), 422 deletions(-) (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 9482bf92..52b73535 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cases.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: cases.ml 11708 2008-12-20 10:50:20Z msozeau $ *) open Util open Names @@ -150,8 +150,11 @@ let mkSpecialLetInJudge j (na,(deppat,nondeppat,d,t)) = then (* The body of pat is not needed to type j - see *) (* insert_aliases - and both deppat and nondeppat have the *) - (* same type, then one can freely substitute one by the other *) - subst1 nondeppat j.uj_val + (* same type, then one can freely substitute one by the other. *) + (* We use nondeppat only if it's a Rel to preserve sharing. *) + if isRel nondeppat then + subst1 nondeppat j.uj_val + else subst1 deppat j.uj_val else (* The body of pat is not needed to type j but its value *) (* is dependent in the type of j; our choice is to *) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 323cd06f..58369811 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarconv.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: evarconv.ml 11745 2009-01-04 18:43:08Z herbelin $ *) open Pp open Util @@ -164,10 +164,9 @@ let rec evar_conv_x env evd pbty term1 term2 = (* Maybe convertible but since reducing can erase evars which [evar_apprec] could have found, we do it only if the terms are free of evar. Note: incomplete heuristic... *) - if is_ground_term evd term1 && is_ground_term evd term2 & - is_fconv pbty env (evars_of evd) term1 term2 - then - (evd,true) + if is_ground_term evd term1 && is_ground_term evd term2 + && is_ground_env evd env + then (evd, is_fconv pbty env (evars_of evd) term1 term2) else let term1 = apprec_nohdbeta env evd term1 in let term2 = apprec_nohdbeta env evd term2 in @@ -211,7 +210,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = | Flexible ev1, MaybeFlexible flex2 -> let f1 i = if - is_unification_pattern_evar env ev1 l1 & + is_unification_pattern_evar env ev1 l1 (applist appr2) & not (occur_evar (fst ev1) (applist appr2)) then (* Miller-Pfenning's patterns unification *) @@ -243,7 +242,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = | MaybeFlexible flex1, Flexible ev2 -> let f1 i = if - is_unification_pattern_evar env ev2 l2 & + is_unification_pattern_evar env ev2 l2 (applist appr1) & not (occur_evar (fst ev2) (applist appr1)) then (* Miller-Pfenning's patterns unification *) @@ -311,7 +310,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = | Flexible ev1, Rigid _ -> if - is_unification_pattern_evar env ev1 l1 & + is_unification_pattern_evar env ev1 l1 (applist appr2) & not (occur_evar (fst ev1) (applist appr2)) then (* Miller-Pfenning's patterns unification *) @@ -326,7 +325,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = | Rigid _, Flexible ev2 -> if - is_unification_pattern_evar env ev2 l2 & + is_unification_pattern_evar env ev2 l2 (applist appr1) & not (occur_evar (fst ev2) (applist appr1)) then (* Miller-Pfenning's patterns unification *) @@ -514,15 +513,15 @@ let apply_conversion_problem_heuristic env evd pbty t1 t2 = let (term1,l1 as appr1) = decompose_app t1 in let (term2,l2 as appr2) = decompose_app t2 in match kind_of_term term1, kind_of_term term2 with - | Evar (evk1,args1), (Rel _|Var _) when l1 = [] & l2 = [] -> + | Evar (evk1,args1), (Rel _|Var _) when l1 = [] & l2 = [] + & array_for_all (fun a -> a = term2 or isEvar a) args1 -> (* The typical kind of constraint coming from pattern-matching return type inference *) - assert (array_for_all (fun a -> a = term2 or isEvar a) args1); choose_less_dependent_instance evk1 evd term2 args1, true - | (Rel _|Var _), Evar (evk2,args2) when l1 = [] & l2 = [] -> + | (Rel _|Var _), Evar (evk2,args2) when l1 = [] & l2 = [] + & array_for_all (fun a -> a = term1 or isEvar a) args2 -> (* The typical kind of constraint coming from pattern-matching return type inference *) - assert (array_for_all ((=) term1) args2); choose_less_dependent_instance evk2 evd term1 args2, true | Evar ev1,_ when List.length l1 <= List.length l2 -> (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 130e23b8..b418f996 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarutil.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: evarutil.ml 11819 2009-01-20 20:04:50Z herbelin $ *) open Util open Pp @@ -258,13 +258,19 @@ let e_new_evar evdref env ?(src=(dummy_loc,InternalHole)) ?filter ty = * operations on the evar constraints * *------------------------------------*) +let is_pattern inst = + array_for_all (fun a -> isRel a || isVar a) inst && + array_distinct inst + (* Pb: defined Rels and Vars should not be considered as a pattern... *) +(* let is_pattern inst = let rec is_hopat l = function [] -> true | t :: tl -> (isRel t or isVar t) && not (List.mem t l) && is_hopat (t::l) tl in is_hopat [] (Array.to_list inst) +*) let evar_well_typed_body evd ev evi body = try @@ -431,7 +437,7 @@ let rec check_and_clear_in_constr evdref err ids c = has dependencies in another hyp of the context of ev and transitively remember the dependency *) match List.filter (fun (id,_) -> occur_var_in_decl (Global.env()) id h) ri with - | rid' :: _ -> (hy,ar,(rid,List.assoc rid ri)::ri) + | (_,id') :: _ -> (hy,ar,(rid,id')::ri) | _ -> (* No dependency at all, we can keep this ev's context hyp *) (h::hy,a::ar,ri)) @@ -484,24 +490,42 @@ let clear_hyps_in_evi evdref hyps concl ids = dependencies in variables are canonically associated to the most ancient variable in its family of aliased variables *) -let rec expand_var env x = match kind_of_term x with +let expand_var_once env x = match kind_of_term x with | Rel n -> - begin try match pi2 (lookup_rel n env) with - | Some t when isRel t -> expand_var env (lift n t) - | _ -> x - with Not_found -> x + begin match pi2 (lookup_rel n env) with + | Some t when isRel t or isVar t -> lift n t + | _ -> raise Not_found end | Var id -> begin match pi2 (lookup_named id env) with - | Some t when isVar t -> expand_var env t - | _ -> x + | Some t when isVar t -> t + | _ -> raise Not_found end - | _ -> x + | _ -> + raise Not_found + +let rec expand_var_at_least_once env x = + let t = expand_var_once env x in + try expand_var_at_least_once env t + with Not_found -> t + +let expand_var env x = + try expand_var_at_least_once env x with Not_found -> x + +let expand_var_opt env x = + try Some (expand_var_at_least_once env x) with Not_found -> None let rec expand_vars_in_term env t = match kind_of_term t with | Rel _ | Var _ -> expand_var env t | _ -> map_constr_with_full_binders push_rel expand_vars_in_term env t +let rec expansions_of_var env x = + try + let t = expand_var_once env x in + t :: expansions_of_var env t + with Not_found -> + [x] + (* [find_projectable_vars env sigma y subst] finds all vars of [subst] * that project on [y]. It is able to find solutions to the following * two kinds of problems: @@ -540,16 +564,16 @@ type evar_projection = | ProjectVar | ProjectEvar of existential * evar_info * identifier * evar_projection -let rec find_projectable_vars env sigma y subst = +let rec find_projectable_vars with_evars env sigma y subst = let is_projectable (id,(idc,y')) = let y' = whd_evar sigma y' in if y = y' or expand_var env y = expand_var env y' then (idc,(y'=y,(id,ProjectVar))) - else if isEvar y' then + else if with_evars & isEvar y' then let (evk,argsv as t) = destEvar y' in let evi = Evd.find sigma evk in let subst = make_projectable_subst sigma evi argsv in - let l = find_projectable_vars env sigma y subst in + let l = find_projectable_vars with_evars env sigma y subst in match l with | [id',p] -> (idc,(true,(id,ProjectEvar (t,evi,id',p)))) | _ -> failwith "" @@ -568,7 +592,7 @@ let filter_solution = function | [id,p] -> (mkVar id, p) let project_with_effects env sigma effects t subst = - let c, p = filter_solution (find_projectable_vars env sigma t subst) in + let c, p = filter_solution (find_projectable_vars false env sigma t subst) in effects := p :: !effects; c @@ -690,8 +714,8 @@ let do_restrict_hyps_virtual evd evk filter = unsolvable. Computing whether y is erasable or not may be costly and the interest for this early detection in practice is not obvious. We let - it for future work. Anyway, thanks to the use of filters, the whole - context remains consistent. *) + it for future work. In any case, thanks to the use of filters, the whole + (unrestricted) context remains consistent. *) let evi = Evd.find (evars_of evd) evk in let env = evar_unfiltered_env evi in let oldfilter = evar_filter evi in @@ -822,7 +846,7 @@ let rec invert_definition env evd (evk,argsv as ev) rhs = let project_variable t = (* Evar/Var problem: unifiable iff variable projectable from ev subst *) try - let sols = find_projectable_vars env (evars_of !evdref) t subst in + let sols = find_projectable_vars true env (evars_of !evdref) t subst in let c, p = filter_solution sols in let ty = lazy (Retyping.get_type_of env (evars_of !evdref) t) in let evd = do_projection_effects evar_define env ty !evdref p in @@ -833,7 +857,9 @@ let rec invert_definition env evd (evk,argsv as ev) rhs = | NotUnique -> if not !progress then raise NotEnoughInformationToProgress; (* No unique projection but still restrict to where it is possible *) - let filter = array_map_to_list (fun c -> isEvar c or c = t) argsv in + let ts = expansions_of_var env t in + let test c = isEvar c or List.mem c ts in + let filter = array_map_to_list test argsv in let args' = filter_along (fun x -> x) filter argsv in let evd,evar = do_restrict_hyps_virtual !evdref evk filter in let evk',_ = destEvar evar in @@ -891,6 +917,12 @@ let rec invert_definition env evd (evk,argsv as ev) rhs = * context "hyps" and not referring to itself. *) +and occur_existential evm c = + let rec occrec c = match kind_of_term c with + | Evar (e, _) -> if not (is_defined evm e) then raise Occur + | _ -> iter_constr occrec c + in try occrec c; false with Occur -> true + and evar_define env (evk,_ as ev) rhs evd = try let (evd',body) = invert_definition env evd ev rhs in @@ -934,6 +966,13 @@ let has_undefined_evars evd t = let is_ground_term evd t = not (has_undefined_evars evd t) +let is_ground_env evd env = + let is_ground_decl = function + (_,Some b,_) -> is_ground_term evd b + | _ -> true in + List.for_all is_ground_decl (rel_context env) && + List.for_all is_ground_decl (named_context env) + let head_evar = let rec hrec c = match kind_of_term c with | Evar (evk,_) -> evk @@ -948,16 +987,50 @@ let head_evar = that we don't care whether args itself contains Rel's or even Rel's distinct from the ones in l *) -let is_unification_pattern_evar env (_,args) l = - let l' = Array.to_list args @ l in - let l' = List.map (expand_var env) l' in - List.for_all (fun a -> isRel a or isVar a) l' & list_distinct l' - -let is_unification_pattern env f l = +let rec expand_and_check_vars env = function + | [] -> [] + | a::l -> + if isRel a or isVar a then + let l = expand_and_check_vars env l in + match expand_var_opt env a with + | None -> a :: l + | Some a' when isRel a' or isVar a' -> list_add_set a' l + | _ -> raise Exit + else + raise Exit + +let is_unification_pattern_evar env (_,args) l t = + List.for_all (fun x -> isRel x || isVar x) l (* common failure case *) + && + let l' = Array.to_list args @ l in + let l'' = try Some (expand_and_check_vars env l') with Exit -> None in + match l'' with + | Some l -> + let deps = + if occur_meta_or_existential t then + (* Probably no restrictions on allowed vars in presence of evars *) + l + else + (* Probably strong restrictions coming from t being evar-closed *) + let fv_rels = free_rels t in + let fv_ids = global_vars env t in + List.filter (fun c -> + match kind_of_term c with + | Var id -> List.mem id fv_ids + | Rel n -> Intset.mem n fv_rels + | _ -> assert false) l in + list_distinct deps + | None -> false + +let is_unification_pattern (env,nb) f l t = match kind_of_term f with - | Meta _ -> array_for_all isRel l & array_distinct l - | Evar ev -> is_unification_pattern_evar env ev (Array.to_list l) - | _ -> false + | Meta _ -> + array_for_all (fun c -> isRel c && destRel c <= nb) l + && array_distinct l + | Evar ev -> + is_unification_pattern_evar env ev (Array.to_list l) t + | _ -> + false (* From a unification problem "?X l1 = term1 l2" such that l1 is made of distinct rel's, build "\x1...xn.(term1 l2)" (patterns unification) *) @@ -1045,16 +1118,47 @@ let solve_simple_eqn conv_algo env evd (pbty,(evk1,args1 as ev1),t2) = then solve_evar_evar evar_define env evd ev1 ev2 else add_conv_pb (pbty,env,mkEvar ev1,t2) evd | _ -> - evar_define env ev1 t2 evd in + let evd = evar_define env ev1 t2 evd in + let evm = evars_of evd in + let evi = Evd.find evm evk1 in + if occur_existential evm evi.evar_concl then + let evenv = evar_env evi in + let evc = nf_isevar evd evi.evar_concl in + let body = match evi.evar_body with Evar_defined b -> b | Evar_empty -> assert false in + let ty = nf_isevar evd (Retyping.get_type_of_with_meta evenv evm (metas_of evd) body) in + add_conv_pb (Reduction.CUMUL,evenv,ty,evc) evd + else evd + in let (evd,pbs) = extract_changed_conv_pbs evd status_changed in - List.fold_left - (fun (evd,b as p) (pbty,env,t1,t2) -> - if b then conv_algo env evd pbty t1 t2 else p) (evd,true) - pbs + List.fold_left + (fun (evd,b as p) (pbty,env,t1,t2) -> + if b then conv_algo env evd pbty t1 t2 else p) (evd,true) + pbs with e when precatchable_exception e -> (evd,false) - +let evars_of_term c = + let rec evrec acc c = + match kind_of_term c with + | Evar (n, _) -> Intset.add n acc + | _ -> fold_constr evrec acc c + in + evrec Intset.empty c + +let evars_of_named_context nc = + List.fold_right (fun (_, b, t) s -> + Option.fold_left (fun s t -> + Intset.union s (evars_of_term t)) + s b) nc Intset.empty + +let evars_of_evar_info evi = + Intset.union (evars_of_term evi.evar_concl) + (Intset.union + (match evi.evar_body with + | Evar_empty -> Intset.empty + | Evar_defined b -> evars_of_term b) + (evars_of_named_context (named_context_of_val evi.evar_hyps))) + (* [check_evars] fails if some unresolved evar remains *) (* it assumes that the defined existentials have already been substituted *) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index ca446c01..a687fdf0 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: evarutil.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) +(*i $Id: evarutil.mli 11745 2009-01-04 18:43:08Z herbelin $ i*) (*i*) open Util @@ -73,6 +73,7 @@ val non_instantiated : evar_map -> (evar * evar_info) list (* Unification utils *) val is_ground_term : evar_defs -> constr -> bool +val is_ground_env : evar_defs -> env -> bool val solve_refl : (env -> evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool) -> env -> evar_defs -> existential_key -> constr array -> constr array -> @@ -90,10 +91,16 @@ val define_evar_as_product : evar_defs -> existential -> evar_defs * types val define_evar_as_lambda : evar_defs -> existential -> evar_defs * types val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts -val is_unification_pattern_evar : env -> existential -> constr list -> bool -val is_unification_pattern : env -> constr -> constr array -> bool +val is_unification_pattern_evar : env -> existential -> constr list -> + constr -> bool +val is_unification_pattern : env * int -> constr -> constr array -> + constr -> bool val solve_pattern_eqn : env -> constr list -> constr -> constr +val evars_of_term : constr -> Intset.t +val evars_of_named_context : named_context -> Intset.t +val evars_of_evar_info : evar_info -> Intset.t + (***********************************************************) (* Value/Type constraints *) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index bf3cd623..af070d7e 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evd.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: evd.ml 11865 2009-01-28 17:34:30Z herbelin $ *) open Pp open Util @@ -300,6 +300,9 @@ let is_defined (sigma,_) = is_defined sigma let existential_value (sigma,_) = existential_value sigma let existential_type (sigma,_) = existential_type sigma let existential_opt_value (sigma,_) = existential_opt_value sigma +let eq_evar_map x y = x == y || + (Evarmap.equal eq_evar_info (fst x) (fst y) && + UniverseMap.equal (=) (snd x) (snd y)) let merge e e' = fold (fun n v sigma -> add sigma n v) e' e @@ -400,10 +403,12 @@ let metamap_to_list m = (*************************) (* Unification state *) +type obligation_definition_status = Define of bool | Expand + type hole_kind = | ImplicitArg of global_reference * (int * identifier option) | BinderType of name - | QuestionMark of bool + | QuestionMark of obligation_definition_status | CasesType | InternalHole | TomatchTypeParameter of inductive * int diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 5810f93d..b9cb2142 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: evd.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) +(*i $Id: evd.mli 11865 2009-01-28 17:34:30Z herbelin $ i*) (*i*) open Util @@ -52,6 +52,7 @@ val evar_unfiltered_env : evar_info -> env val evar_env : evar_info -> env type evar_map +val eq_evar_map : evar_map -> evar_map -> bool val empty : evar_map @@ -166,11 +167,16 @@ val empty_evar_defs : evar_defs val evars_of : evar_defs -> evar_map val evars_reset_evd : evar_map -> evar_defs -> evar_defs +(* Should the obligation be defined (opaque or transparent (default)) or + defined transparent and expanded in the term? *) + +type obligation_definition_status = Define of bool | Expand + (* Evars *) type hole_kind = | ImplicitArg of global_reference * (int * identifier option) | BinderType of name - | QuestionMark of bool (* Can it be turned into an obligation ? *) + | QuestionMark of obligation_definition_status | CasesType | InternalHole | TomatchTypeParameter of inductive * int diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index b4b8f0b8..d3123eb6 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: indrec.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: indrec.ml 11735 2009-01-02 17:22:31Z herbelin $ *) open Pp open Util @@ -29,8 +29,7 @@ open Sign (* Errors related to recursors building *) type recursion_scheme_error = - | NotAllowedCaseAnalysis of bool * sorts * inductive - | BadInduction of bool * identifier * sorts + | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * inductive | NotMutualInScheme of inductive * inductive exception RecursionSchemeError of recursion_scheme_error @@ -57,8 +56,7 @@ let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind = if not (List.mem kind (elim_sorts specif)) then raise (RecursionSchemeError - (NotAllowedCaseAnalysis - (dep,(new_sort_in_family kind),ind))); + (NotAllowedCaseAnalysis (false,new_sort_in_family kind,ind))); let ndepar = mip.mind_nrealargs + 1 in @@ -502,10 +500,10 @@ let instantiate_type_indrec_scheme sort npars term = let check_arities listdepkind = let _ = List.fold_left (fun ln ((_,ni as mind),mibi,mipi,dep,kind) -> - let id = mipi.mind_typename in let kelim = elim_sorts (mibi,mipi) in if not (List.exists ((=) kind) kelim) then raise - (RecursionSchemeError (BadInduction (dep,id,new_sort_in_family kind))) + (RecursionSchemeError + (NotAllowedCaseAnalysis (true,new_sort_in_family kind,mind))) else if List.mem ni ln then raise (RecursionSchemeError (NotMutualInScheme (mind,mind))) else ni::ln) @@ -593,7 +591,8 @@ let lookup_eliminator ind_sp s = errorlabstrm "default_elim" (strbrk "Cannot find the elimination combinator " ++ pr_id id ++ strbrk ", the elimination of the inductive definition " ++ - pr_id id ++ strbrk " on sort " ++ pr_sort_family s ++ + pr_global_env Idset.empty (IndRef ind_sp) ++ + strbrk " on sort " ++ pr_sort_family s ++ strbrk " is probably not allowed.") diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index 6f177474..102c7c7f 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: indrec.mli 9831 2007-05-17 18:55:42Z herbelin $ i*) +(*i $Id: indrec.mli 11562 2008-11-09 11:30:10Z herbelin $ i*) (*i*) open Names @@ -20,8 +20,7 @@ open Evd (* Errors related to recursors building *) type recursion_scheme_error = - | NotAllowedCaseAnalysis of bool * sorts * inductive - | BadInduction of bool * identifier * sorts + | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * inductive | NotMutualInScheme of inductive * inductive exception RecursionSchemeError of recursion_scheme_error diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 127cd0f2..9f8c06da 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: inductiveops.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: inductiveops.ml 11436 2008-10-07 13:56:55Z barras $ *) open Util open Names @@ -392,6 +392,58 @@ let arity_of_case_predicate env (ind,params) dep k = let concl = if dep then mkArrow mind (mkSort k) else mkSort k in it_mkProd_or_LetIn concl arsign +(***********************************************) +(* Inferring the sort of parameters of a polymorphic inductive type + knowing the sort of the conclusion *) + +(* Check if u (sort of a parameter) appears in the sort of the + inductive (is). This is done by trying to enforce u > u' >= is + in the empty univ graph. If an inconsistency appears, then + is depends on u. *) +let is_constrained is u = + try + let u' = fresh_local_univ() in + let _ = + merge_constraints + (enforce_geq u (super u') + (enforce_geq u' is Constraint.empty)) + initial_universes in + false + with UniverseInconsistency _ -> true + +(* Compute the inductive argument types: replace the sorts + that appear in the type of the inductive by the sort of the + conclusion, and the other ones by fresh universes. *) +let rec instantiate_universes env scl is = function + | (_,Some _,_ as d)::sign, exp -> + d :: instantiate_universes env scl is (sign, exp) + | d::sign, None::exp -> + d :: instantiate_universes env scl is (sign, exp) + | (na,None,ty)::sign, Some u::exp -> + let ctx,_ = Reduction.dest_arity env ty in + let s = + if is_constrained is u then + scl (* constrained sort: replace by scl *) + else + (* unconstriained sort: replace by fresh universe *) + new_Type_sort() in + (na,None,mkArity(ctx,s)):: instantiate_universes env scl is (sign, exp) + | sign, [] -> sign (* Uniform parameters are exhausted *) + | [], _ -> assert false + +(* Does not deal with universes, but only with Set/Type distinction *) +let type_of_inductive_knowing_conclusion env mip conclty = + match mip.mind_arity with + | Monomorphic s -> + s.mind_user_arity + | Polymorphic ar -> + let _,scl = Reduction.dest_arity env conclty in + let ctx = List.rev mip.mind_arity_ctxt in + let ctx = + instantiate_universes + env scl ar.poly_level (ctx,ar.poly_param_levels) in + mkArity (List.rev ctx,scl) + (***********************************************) (* Guard condition *) diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 1d24659c..1cf940cb 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: inductiveops.mli 11301 2008-08-04 19:41:18Z herbelin $ i*) +(*i $Id: inductiveops.mli 11436 2008-10-07 13:56:55Z barras $ i*) open Names open Term @@ -112,6 +112,11 @@ val make_case_info : env -> inductive -> case_style -> case_info val make_default_case_info : env -> case_style -> inductive -> case_info i*) +(********************) + +val type_of_inductive_knowing_conclusion : + env -> one_inductive_body -> types -> types + (********************) val control_only_guard : env -> types -> unit diff --git a/pretyping/matching.ml b/pretyping/matching.ml index d066a58d..93bac98e 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: matching.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: matching.ml 11735 2009-01-02 17:22:31Z herbelin $ *) (*i*) open Util @@ -44,15 +44,37 @@ open Pattern *) +type bound_ident_map = (identifier * identifier) list + exception PatternMatchingFailure -let constrain (n,m) sigma = - if List.mem_assoc n sigma then - if eq_constr m (List.assoc n sigma) then sigma +let constrain (n,m) (names,terms as subst) = + try + if eq_constr m (List.assoc n terms) then subst else raise PatternMatchingFailure - else - (n,m)::sigma - + with + Not_found -> + if List.mem_assoc n names then + Flags.if_verbose Pp.warning + ("Collision between bound variable "^string_of_id n^ + " and a metavariable of same name."); + (names,(n,m)::terms) + +let add_binders na1 na2 (names,terms as subst) = + match na1, na2 with + | Name id1, Name id2 -> + if List.mem_assoc id1 names then + (Flags.if_verbose Pp.warning + ("Collision between bound variables of name"^string_of_id id1); + (names,terms)) + else + (if List.mem_assoc id1 terms then + Flags.if_verbose Pp.warning + ("Collision between bound variable "^string_of_id id1^ + " and another bound variable of same name."); + ((id1,id2)::names,terms)); + | _ -> subst + let build_lambda toabstract stk (m : constr) = let rec buildrec m p_0 p_1 = match p_0,p_1 with | (_, []) -> m @@ -77,7 +99,10 @@ let same_case_structure (_,cs1,ind,_) ci2 br1 br2 = | None -> cs1 = ci2.ci_cstr_nargs let matches_core convert allow_partial_app pat c = - let rec sorec stk sigma p t = + let conv = match convert with + | None -> eq_constr + | Some (env,sigma) -> is_conv env sigma in + let rec sorec stk subst p t = let cT = strip_outer_cast t in match p,kind_of_term cT with | PSoApp (n,args),m -> @@ -89,7 +114,7 @@ let matches_core convert allow_partial_app pat c = args in let frels = Intset.elements (free_rels cT) in if list_subset frels relargs then - constrain (n,build_lambda relargs stk cT) sigma + constrain (n,build_lambda relargs stk cT) subst else raise PatternMatchingFailure @@ -97,66 +122,63 @@ let matches_core convert allow_partial_app pat c = let depth = List.length stk in if depth = 0 then (* Optimisation *) - constrain (n,cT) sigma + constrain (n,cT) subst else let frels = Intset.elements (free_rels cT) in if List.for_all (fun i -> i > depth) frels then - constrain (n,lift (-depth) cT) sigma + constrain (n,lift (-depth) cT) subst else raise PatternMatchingFailure - | PMeta None, m -> sigma + | PMeta None, m -> subst - | PRef (VarRef v1), Var v2 when v1 = v2 -> sigma + | PRef (VarRef v1), Var v2 when v1 = v2 -> subst - | PVar v1, Var v2 when v1 = v2 -> sigma + | PVar v1, Var v2 when v1 = v2 -> subst - | PRef ref, _ when constr_of_global ref = cT -> sigma + | PRef ref, _ when conv (constr_of_global ref) cT -> subst - | PRel n1, Rel n2 when n1 = n2 -> sigma + | PRel n1, Rel n2 when n1 = n2 -> subst - | PSort (RProp c1), Sort (Prop c2) when c1 = c2 -> sigma + | PSort (RProp c1), Sort (Prop c2) when c1 = c2 -> subst - | PSort (RType _), Sort (Type _) -> sigma + | PSort (RType _), Sort (Type _) -> subst - | PApp (p, [||]), _ -> sorec stk sigma p t + | PApp (p, [||]), _ -> sorec stk subst p t | PApp (PApp (h, a1), a2), _ -> - sorec stk sigma (PApp(h,Array.append a1 a2)) t + sorec stk subst (PApp(h,Array.append a1 a2)) t | PApp (PMeta (Some n),args1), App (c2,args2) when allow_partial_app -> let p = Array.length args2 - Array.length args1 in if p>=0 then let args21, args22 = array_chop p args2 in - let sigma = + let subst = let depth = List.length stk in let c = mkApp(c2,args21) in let frels = Intset.elements (free_rels c) in if List.for_all (fun i -> i > depth) frels then - constrain (n,lift (-depth) c) sigma + constrain (n,lift (-depth) c) subst else raise PatternMatchingFailure in - array_fold_left2 (sorec stk) sigma args1 args22 + array_fold_left2 (sorec stk) subst args1 args22 else raise PatternMatchingFailure | PApp (c1,arg1), App (c2,arg2) -> - (try array_fold_left2 (sorec stk) (sorec stk sigma c1 c2) arg1 arg2 + (try array_fold_left2 (sorec stk) (sorec stk subst c1 c2) arg1 arg2 with Invalid_argument _ -> raise PatternMatchingFailure) | PProd (na1,c1,d1), Prod(na2,c2,d2) -> - sorec ((na2,c2)::stk) (sorec stk sigma c1 c2) d1 d2 + sorec ((na2,c2)::stk) + (add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2 | PLambda (na1,c1,d1), Lambda(na2,c2,d2) -> - sorec ((na2,c2)::stk) (sorec stk sigma c1 c2) d1 d2 + sorec ((na2,c2)::stk) + (add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2 | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) -> - sorec ((na2,t2)::stk) (sorec stk sigma c1 c2) d1 d2 - - | PRef (ConstRef _ as ref), _ when convert <> None -> - let (env,evars) = Option.get convert in - let c = constr_of_global ref in - if is_conv env evars c cT then sigma - else raise PatternMatchingFailure + sorec ((na2,t2)::stk) + (add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2 | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) -> let ctx,b2 = decompose_lam_n_assum ci.ci_cstr_nargs.(0) b2 in @@ -167,118 +189,128 @@ let matches_core convert allow_partial_app pat c = let s = List.fold_left (fun l (na,_,t) -> (na,t)::l) stk ctx in let s' = List.fold_left (fun l (na,_,t) -> (na,t)::l) stk ctx' in let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in - sorec s' (sorec s (sorec stk sigma a1 a2) b1 b2) b1' b2' + sorec s' (sorec s (sorec stk subst a1 a2) b1 b2) b1' b2' else raise PatternMatchingFailure | PCase (ci1,p1,a1,br1), Case (ci2,p2,a2,br2) -> if same_case_structure ci1 ci2 br1 br2 then array_fold_left2 (sorec stk) - (sorec stk (sorec stk sigma a1 a2) p1 p2) br1 br2 + (sorec stk (sorec stk subst a1 a2) p1 p2) br1 br2 else raise PatternMatchingFailure - | PFix c1, Fix _ when eq_constr (mkFix c1) cT -> sigma - | PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> sigma + | PFix c1, Fix _ when eq_constr (mkFix c1) cT -> subst + | PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> subst | _ -> raise PatternMatchingFailure - in - Sort.list (fun (a,_) (b,_) -> a a closed0 c) (fst mres)) then - raise PatternMatchingFailure; - if nocc = 0 then mres - else raise (NextOccurrence nocc) - -let special_meta = (-1) +let authorized_occ partial_app closed pat c mk_ctx next = + try + let sigma = matches_core None partial_app pat c in + if closed && not (List.for_all (fun (_,c) -> closed0 c) (snd sigma)) + then next () + else sigma, mk_ctx (mkMeta special_meta), next + with + PatternMatchingFailure -> next () (* Tries to match a subterm of [c] with [pat] *) -let rec sub_match nocc pat c = +let sub_match ?(partial_app=false) ?(closed=true) pat c = + let rec aux c mk_ctx next = match kind_of_term c with | Cast (c1,k,c2) -> - (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with - | PatternMatchingFailure -> - let (lm,lc) = try_sub_match nocc pat [c1] in - (lm,mkCast (List.hd lc, k,c2)) - | NextOccurrence nocc -> - let (lm,lc) = try_sub_match (nocc - 1) pat [c1] in - (lm,mkCast (List.hd lc, k,c2))) - | Lambda (x,c1,c2) -> - (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with - | PatternMatchingFailure -> - let (lm,lc) = try_sub_match nocc pat [c1;c2] in - (lm,mkLambda (x,List.hd lc,List.nth lc 1)) - | NextOccurrence nocc -> - let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in - (lm,mkLambda (x,List.hd lc,List.nth lc 1))) + authorized_occ partial_app closed pat c mk_ctx (fun () -> + let mk_ctx lc = mk_ctx (mkCast (List.hd lc, k,c2)) in + try_aux [c1] mk_ctx next) + | Lambda (x,c1,c2) -> + authorized_occ partial_app closed pat c mk_ctx (fun () -> + let mk_ctx lc = mk_ctx (mkLambda (x,List.hd lc,List.nth lc 1)) in + try_aux [c1;c2] mk_ctx next) | Prod (x,c1,c2) -> - (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with - | PatternMatchingFailure -> - let (lm,lc) = try_sub_match nocc pat [c1;c2] in - (lm,mkProd (x,List.hd lc,List.nth lc 1)) - | NextOccurrence nocc -> - let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in - (lm,mkProd (x,List.hd lc,List.nth lc 1))) - | LetIn (x,c1,t2,c2) -> - (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with - | PatternMatchingFailure -> - let (lm,lc) = try_sub_match nocc pat [c1;t2;c2] in - (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2)) - | NextOccurrence nocc -> - let (lm,lc) = try_sub_match (nocc - 1) pat [c1;t2;c2] in - (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2))) + authorized_occ partial_app closed pat c mk_ctx (fun () -> + let mk_ctx lc = mk_ctx (mkProd (x,List.hd lc,List.nth lc 1)) in + try_aux [c1;c2] mk_ctx next) + | LetIn (x,c1,t,c2) -> + authorized_occ partial_app closed pat c mk_ctx (fun () -> + let mk_ctx = function [c1;c2] -> mkLetIn (x,c1,t,c2) | _ -> assert false + in try_aux [c1;c2] mk_ctx next) | App (c1,lc) -> - (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with - | PatternMatchingFailure -> - let (lm,le) = try_sub_match nocc pat (c1::(Array.to_list lc)) in - (lm,mkApp (List.hd le, Array.of_list (List.tl le))) - | NextOccurrence nocc -> - let (lm,le) = try_sub_match (nocc - 1) pat (c1::(Array.to_list lc)) in - (lm,mkApp (List.hd le, Array.of_list (List.tl le)))) + authorized_occ partial_app closed pat c mk_ctx (fun () -> + let topdown = true in + if partial_app then + if topdown then + let lc1 = Array.sub lc 0 (Array.length lc - 1) in + let app = mkApp (c1,lc1) in + let mk_ctx = function + | [app';c] -> mk_ctx (mkApp (app',[|c|])) + | _ -> assert false in + try_aux [app;array_last lc] mk_ctx next + else + let rec aux2 app args next = + match args with + | [] -> + let mk_ctx le = + mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in + try_aux (c1::Array.to_list lc) mk_ctx next + | arg :: args -> + let app = mkApp (app,[|arg|]) in + let next () = aux2 app args next in + let mk_ctx ce = mk_ctx (mkApp (ce, Array.of_list args)) in + aux app mk_ctx next in + aux2 c1 (Array.to_list lc) next + else + let mk_ctx le = + mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in + try_aux (c1::Array.to_list lc) mk_ctx next) | Case (ci,hd,c1,lc) -> - (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with - | PatternMatchingFailure -> - let (lm,le) = try_sub_match nocc pat (c1::Array.to_list lc) in - (lm,mkCase (ci,hd,List.hd le,Array.of_list (List.tl le))) - | NextOccurrence nocc -> - let (lm,le) = try_sub_match (nocc - 1) pat (c1::Array.to_list lc) in - (lm,mkCase (ci,hd,List.hd le,Array.of_list (List.tl le)))) + authorized_occ partial_app closed pat c mk_ctx (fun () -> + let mk_ctx le = + mk_ctx (mkCase (ci,hd,List.hd le,Array.of_list (List.tl le))) in + try_aux (c1::Array.to_list lc) mk_ctx next) | Construct _ | Fix _ | Ind _|CoFix _ |Evar _|Const _ | Rel _|Meta _|Var _|Sort _ -> - (try authorized_occ nocc ((matches pat c),mkMeta special_meta) with - | PatternMatchingFailure -> raise (NextOccurrence nocc) - | NextOccurrence nocc -> raise (NextOccurrence (nocc - 1))) - -(* Tries [sub_match] for all terms in the list *) -and try_sub_match nocc pat lc = - let rec try_sub_match_rec nocc pat lacc = function - | [] -> raise (NextOccurrence nocc) - | c::tl -> - (try - let (lm,ce) = sub_match nocc pat c in - (lm,lacc@(ce::tl)) - with - | NextOccurrence nocc -> try_sub_match_rec nocc pat (lacc@[c]) tl) in - try_sub_match_rec nocc pat [] lc - -let match_subterm nocc pat c = - try sub_match nocc pat c - with NextOccurrence _ -> raise PatternMatchingFailure - -let is_matching pat n = - try let _ = matches pat n in true + authorized_occ partial_app closed pat c mk_ctx next + + (* Tries [sub_match] for all terms in the list *) + and try_aux lc mk_ctx next = + let rec try_sub_match_rec lacc = function + | [] -> next () + | c::tl -> + let mk_ctx ce = mk_ctx (List.rev_append lacc (ce::tl)) in + let next () = try_sub_match_rec (c::lacc) tl in + aux c mk_ctx next in + try_sub_match_rec [] lc in + aux c (fun x -> x) (fun () -> raise PatternMatchingFailure) + +type subterm_matching_result = + (bound_ident_map * patvar_map) * constr * (unit -> subterm_matching_result) + +let match_subterm pat c = sub_match pat c + +let match_appsubterm pat c = sub_match ~partial_app:true pat c + +let match_subterm_gen app pat c = sub_match ~partial_app:app pat c + +let is_matching pat c = + try let _ = matches pat c in true + with PatternMatchingFailure -> false + +let is_matching_appsubterm ?(closed=true) pat c = + try let _ = sub_match ~partial_app:true ~closed pat c in true with PatternMatchingFailure -> false -let matches_conv env sigma = matches_core (Some (env,sigma)) false +let matches_conv env sigma c p = + snd (matches_core (Some (env,sigma)) false c p) let is_matching_conv env sigma pat n = try let _ = matches_conv env sigma pat n in true diff --git a/pretyping/matching.mli b/pretyping/matching.mli index e6065c68..b54a17b7 100644 --- a/pretyping/matching.mli +++ b/pretyping/matching.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: matching.mli 6616 2005-01-21 17:18:23Z herbelin $ i*) +(*i $Id: matching.mli 11739 2009-01-02 19:33:19Z herbelin $ i*) (*i*) open Names @@ -22,30 +22,58 @@ exception PatternMatchingFailure val special_meta : metavariable +type bound_ident_map = (identifier * identifier) list + (* [matches pat c] matches [c] against [pat] and returns the resulting assignment of metavariables; it raises [PatternMatchingFailure] if not matchable; bindings are given in increasing order based on the numbers given in the pattern *) val matches : constr_pattern -> constr -> patvar_map -(* [is_matching pat c] just tells if [c] matches against [pat] *) +(* [extended_matches pat c] also returns the names of bound variables + in [c] that matches the bound variables in [pat]; if several bound + variables or metavariables have the same name, the metavariable, + or else the rightmost bound variable, takes precedence *) +val extended_matches : + constr_pattern -> constr -> bound_ident_map * patvar_map +(* [is_matching pat c] just tells if [c] matches against [pat] *) val is_matching : constr_pattern -> constr -> bool (* [matches_conv env sigma] matches up to conversion in environment [(env,sigma)] when constants in pattern are concerned; it raises [PatternMatchingFailure] if not matchable; bindings are given in increasing order based on the numbers given in the pattern *) - val matches_conv :env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map +(* The type of subterm matching results: a substitution + a context + (whose hole is denoted with [special_meta]) + a continuation that + either returns the next matching subterm or raise PatternMatchingFailure *) +type subterm_matching_result = + (bound_ident_map * patvar_map) * constr * (unit -> subterm_matching_result) + (* [match_subterm n pat c] returns the substitution and the context - corresponding to the [n+1]th **closed** subterm of [c] matching [pat]; - It raises PatternMatchingFailure if no such matching exists *) -val match_subterm : int -> constr_pattern -> constr -> patvar_map * constr + corresponding to the first **closed** subterm of [c] matching [pat], and + a continuation that looks for the next matching subterm. + It raises PatternMatchingFailure if no subterm matches the pattern *) +val match_subterm : constr_pattern -> constr -> subterm_matching_result + +(* [match_appsubterm pat c] returns the substitution and the context + corresponding to the first **closed** subterm of [c] matching [pat], + considering application contexts as well. It also returns a + continuation that looks for the next matching subterm. + It raises PatternMatchingFailure if no subterm matches the pattern *) +val match_appsubterm : constr_pattern -> constr -> subterm_matching_result + +(* [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *) +val match_subterm_gen : bool (* true = with app context *) -> + constr_pattern -> constr -> subterm_matching_result + +(* [is_matching_appsubterm pat c] tells if a subterm of [c] matches + against [pat] taking partial subterms into consideration *) +val is_matching_appsubterm : ?closed:bool -> constr_pattern -> constr -> bool (* [is_matching_conv env sigma pat c] tells if [c] matches against [pat] up to conversion for constants in patterns *) - val is_matching_conv : env -> Evd.evar_map -> constr_pattern -> constr -> bool diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index a3246bc8..1cac9011 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pretyping.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: pretyping.ml 11576 2008-11-10 19:13:15Z msozeau $ *) open Pp open Util @@ -586,7 +586,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in { uj_val = v; uj_type = p } - + | RCases (loc,sty,po,tml,eqns) -> Cases.compile_cases loc sty ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref) @@ -605,8 +605,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct (* ... except for Correctness *) let v = mkCast (cj.uj_val, k, tj.utj_val) in { uj_val = v; uj_type = tj.utj_val } - in - inh_conv_coerce_to_tycon loc env evdref cj tycon + in inh_conv_coerce_to_tycon loc env evdref cj tycon | RDynamic (loc,d) -> if (tag d) = "constr" then @@ -657,12 +656,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct | IsType -> (pretype_type empty_valcon env evdref lvar c).utj_val in let evd,_ = consider_remaining_unif_problems env !evdref in - evdref := evd; c' + evdref := evd; + nf_isevar !evdref c' let pretype_gen evdref env lvar kind c = let c = pretype_gen_aux evdref env lvar kind c in evdref := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env !evdref; - nf_evar (evars_of !evdref) c + nf_isevar !evdref c (* TODO: comment faire remonter l'information si le typage a resolu des variables du sigma original. il faudrait que la fonction de typage @@ -691,14 +691,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct let ise_pretype_gen fail_evar sigma env lvar kind c = let evdref = ref (Evd.create_evar_defs sigma) in - let c = pretype_gen evdref env lvar kind c in - let evd,_ = consider_remaining_unif_problems env !evdref in + let c = pretype_gen_aux evdref env lvar kind c in if fail_evar then - let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in + let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env !evdref in let c = Evarutil.nf_isevar evd c in check_evars env Evd.empty evd c; evd, c - else evd, c + else !evdref, c (** Entry points of the high-level type synthesis algorithm *) @@ -716,17 +715,17 @@ module Pretyping_F (Coercion : Coercion.S) = struct let understand_tcc_evars evdref env kind c = pretype_gen evdref env ([],[]) kind c - + let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c = let evd, t = - if resolve_classes then - ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c - else - let evdref = ref (Evd.create_evar_defs sigma) in - let c = pretype_gen_aux evdref env ([],[]) (OfType exptyp) c in - !evdref, nf_isevar !evdref c - in - Evd.evars_of evd, t + let evdref = ref (Evd.create_evar_defs sigma) in + let c = + if resolve_classes then + pretype_gen evdref env ([],[]) (OfType exptyp) c + else + pretype_gen_aux evdref env ([],[]) (OfType exptyp) c + in !evdref, c + in Evd.evars_of evd, t end - + module Default : S = Pretyping_F(Coercion.Default) diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 3726b8df..30b62ea8 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: rawterm.ml 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: rawterm.ml 11576 2008-11-10 19:13:15Z msozeau $ *) (*i*) open Util @@ -219,7 +219,7 @@ let free_rawvars = | RLambda (loc,na,_,ty,c) | RProd (loc,na,_,ty,c) | RLetIn (loc,na,ty,c) -> let vs' = vars bounded vs ty in let bounded' = add_name_to_ids bounded na in - vars bounded' vs' c + vars bounded' vs' c | RCases (loc,sty,rtntypopt,tml,pl) -> let vs1 = vars_option bounded vs rtntypopt in let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 06289434..7c4023b9 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: recordops.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: recordops.ml 11576 2008-11-10 19:13:15Z msozeau $ *) open Util open Pp @@ -32,9 +32,9 @@ open Reductionops projection ou bien une fonction constante (associée à un LetIn) *) type struc_typ = { - s_CONST : identifier; + s_CONST : constructor; s_EXPECTEDPARAM : int; - s_PROJKIND : bool list; + s_PROJKIND : (name * bool) list; s_PROJ : constant option list } let structure_table = ref (Indmap.empty : struc_typ Indmap.t) @@ -61,8 +61,9 @@ let subst_structure (_,subst,((kn,i),id,kl,projs as obj)) = (Option.smartmap (fun kn -> fst (subst_con subst kn))) projs in - if projs' == projs && kn' == kn then obj else - ((kn',i),id,kl,projs') + let id' = fst (subst_constructor subst id) in + if projs' == projs && kn' == kn && id' == id then obj else + ((kn',i),id',kl,projs') let discharge_structure (_,(ind,id,kl,projs)) = Some (Lib.discharge_inductive ind, id, kl, @@ -88,6 +89,10 @@ let find_projection_nparams = function | ConstRef cst -> (Cmap.find cst !projection_table).s_EXPECTEDPARAM | _ -> raise Not_found +let find_projection = function + | ConstRef cst -> Cmap.find cst !projection_table + | _ -> raise Not_found + (************************************************************************) (*s A canonical structure declares "canonical" conversion hints between *) @@ -135,7 +140,7 @@ let canonical_projections () = !object_table [] let keep_true_projections projs kinds = - map_succeed (function (p,true) -> p | _ -> failwith "") + map_succeed (function (p,(_,true)) -> p | _ -> failwith "") (List.combine projs kinds) let cs_pattern_of_constr t = @@ -237,7 +242,7 @@ let check_and_decompose_canonical_structure ref = | Construct (indsp,1) -> indsp | _ -> error_not_structure ref in let s = try lookup_structure indsp with Not_found -> error_not_structure ref in - let ntrue_projs = List.length (List.filter (fun x -> x) s.s_PROJKIND) in + let ntrue_projs = List.length (List.filter (fun (_, x) -> x) s.s_PROJKIND) in if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then error_not_structure ref; (sp,indsp) diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 74f6a9ce..ea960aa9 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: recordops.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) +(*i $Id: recordops.mli 11576 2008-11-10 19:13:15Z msozeau $ i*) (*i*) open Names @@ -21,8 +21,14 @@ open Library (*s A structure S is a non recursive inductive type with a single constructor (the name of which defaults to Build_S) *) +type struc_typ = { + s_CONST : constructor; + s_EXPECTEDPARAM : int; + s_PROJKIND : (name * bool) list; + s_PROJ : constant option list } + val declare_structure : - inductive * identifier * bool list * constant option list -> unit + inductive * constructor * (name * bool) list * constant option list -> unit (* [lookup_projections isp] returns the projections associated to the inductive path [isp] if it corresponds to a structure, otherwise @@ -32,6 +38,9 @@ val lookup_projections : inductive -> constant option list (* raise [Not_found] if not a projection *) val find_projection_nparams : global_reference -> int +(* raise [Not_found] if not a projection *) +val find_projection : global_reference -> struc_typ + (*s A canonical structure declares "canonical" conversion hints between *) (* the effective components of a structure and the projections of the *) (* structure *) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 21e881b9..a1603d69 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: reductionops.ml 11343 2008-09-01 20:55:13Z herbelin $ *) +(* $Id: reductionops.ml 11796 2009-01-18 13:41:39Z herbelin $ *) open Pp open Util @@ -537,6 +537,8 @@ let nf_evar sigma = local_strong (whd_evar sigma) (* lazy reduction functions. The infos must be created for each term *) +(* Note by HH [oct 08] : why would it be the job of clos_norm_flags to add + a [nf_evar] here *) let clos_norm_flags flgs env sigma t = norm_val (create_clos_infos flgs env) (inject (nf_evar sigma t)) @@ -625,8 +627,23 @@ let pb_equal = function let sort_cmp = sort_cmp + +let nf_red_env sigma env = + let nf_decl = function + (x,Some t,ty) -> (x,Some (nf_evar sigma t),ty) + | d -> d in + let sign = named_context env in + let ctxt = rel_context env in + let env = reset_context env in + let env = Sign.fold_named_context + (fun d env -> push_named (nf_decl d) env) ~init:env sign in + Sign.fold_rel_context + (fun d env -> push_rel (nf_decl d) env) ~init:env ctxt + + let test_conversion f env sigma x y = - try let _ = f env (nf_evar sigma x) (nf_evar sigma y) in true + try let _ = + f (nf_red_env sigma env) (nf_evar sigma x) (nf_evar sigma y) in true with NotConvertible -> false let is_conv env sigma = test_conversion Reduction.conv env sigma @@ -652,11 +669,11 @@ let whd_meta metamap c = match kind_of_term c with (* Try to replace all metas. Does not replace metas in the metas' values * Differs from (strong whd_meta). *) let plain_instance s c = - let rec irec u = match kind_of_term u with - | Meta p -> (try List.assoc p s with Not_found -> u) + let rec irec n u = match kind_of_term u with + | Meta p -> (try lift n (List.assoc p s) with Not_found -> u) | App (f,l) when isCast f -> let (f,_,t) = destCast f in - let l' = Array.map irec l in + let l' = Array.map (irec n) l in (match kind_of_term f with | Meta p -> (* Don't flatten application nodes: this is used to extract a @@ -669,12 +686,13 @@ let plain_instance s c = mkLetIn (Name h,g,t,mkApp(mkRel 1,Array.map (lift 1) l')) | _ -> mkApp (g,l') with Not_found -> mkApp (f,l')) - | _ -> mkApp (irec f,l')) + | _ -> mkApp (irec n f,l')) | Cast (m,_,_) when isMeta m -> - (try List.assoc (destMeta m) s with Not_found -> u) - | _ -> map_constr irec u + (try lift n (List.assoc (destMeta m) s) with Not_found -> u) + | _ -> + map_constr_with_binders succ irec n u in - if s = [] then c else irec c + if s = [] then c else irec 0 c (* [instance] is used for [res_pf]; the call to [local_strong whd_betaiota] has (unfortunately) different subtle side effects: @@ -706,8 +724,8 @@ let plain_instance s c = If a lemma has the type "(fun x => p) t" then rewriting t may fail if the type of the lemma is first beta-reduced (this typically happens when rewriting a single variable and the type of the lemma is obtained - by meta_instance (with empty map) which itself call instance with this - empty map. + by meta_instance (with empty map) which itself calls instance with this + empty map). *) let instance s c = diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 82c2668c..2465bd1e 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: retyping.ml 11077 2008-06-09 11:26:32Z herbelin $ *) +(* $Id: retyping.ml 11778 2009-01-13 13:17:39Z msozeau $ *) open Util open Term @@ -49,7 +49,7 @@ let retype sigma metamap = match kind_of_term cstr with | Meta n -> (try strip_outer_cast (List.assoc n metamap) - with Not_found -> anomaly "type_of: this is not a well-typed term") + with Not_found -> anomaly ("type_of: unknown meta " ^ string_of_int n)) | Rel n -> let (_,_,ty) = lookup_rel n env in lift n ty @@ -111,9 +111,15 @@ let retype sigma metamap = | Cast (c,_, s) when isSort s -> family_of_sort (destSort s) | Sort (Prop c) -> InType | Sort (Type u) -> InType - | Prod (name,t,c2) -> sort_family_of (push_rel (name,None,t) env) c2 + | Prod (name,t,c2) -> + let s2 = sort_family_of (push_rel (name,None,t) env) c2 in + if Environ.engagement env <> Some ImpredicativeSet && + s2 = InSet & sort_family_of env t = InType then InType else s2 + | App(f,args) when isGlobalRef f -> + let t = type_of_global_reference_knowing_parameters env f args in + family_of_sort (sort_of_atomic_type env sigma t args) | App(f,args) -> - family_of_sort (sort_of_atomic_type env sigma (type_of env f) args) + family_of_sort (sort_of_atomic_type env sigma (type_of env f) args) | Lambda _ | Fix _ | Construct _ -> anomaly "sort_of: Not a type (1)" | _ -> family_of_sort (decomp_sort env sigma (type_of env t)) @@ -139,6 +145,20 @@ let get_sort_family_of env sigma c = let _,_,f,_ = retype sigma [] in f env c let type_of_global_reference_knowing_parameters env sigma c args = let _,_,_,f = retype sigma [] in f env c args +let type_of_global_reference_knowing_conclusion env sigma c conclty = + let conclty = nf_evar sigma conclty in + match kind_of_term c with + | Ind ind -> + let (_,mip) = Inductive.lookup_mind_specif env ind in + type_of_inductive_knowing_conclusion env mip conclty + | Const cst -> + let t = constant_type env cst in + (* TODO *) + Typeops.type_of_constant_knowing_parameters env t [||] + | Var id -> type_of_var env id + | Construct cstr -> type_of_constructor env cstr + | _ -> assert false + (* We are outside the kernel: we take fresh universes *) (* to avoid tactics and co to refresh universes themselves *) let get_type_of env sigma c = diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 733cb4b1..ec1fc827 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: retyping.mli 9314 2006-10-29 20:11:08Z herbelin $ i*) +(*i $Id: retyping.mli 11436 2008-10-07 13:56:55Z barras $ i*) (*i*) open Names @@ -37,3 +37,5 @@ val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment val type_of_global_reference_knowing_parameters : env -> evar_map -> constr -> constr array -> types +val type_of_global_reference_knowing_conclusion : + env -> evar_map -> constr -> types -> types diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 57fdbb09..88a6f499 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacred.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: tacred.ml 11654 2008-12-03 18:39:40Z barras $ *) open Pp open Util @@ -99,10 +99,11 @@ let reference_value sigma env c = (* One reuses the name of the function after reduction of the fixpoint *) type constant_evaluation = - | EliminationFix of int * (int * (int * constr) list * int) + | EliminationFix of int * int * (int * (int * constr) list * int) | EliminationMutualFix of int * evaluable_reference * - (evaluable_reference option array * (int * (int * constr) list * int)) + ((int*evaluable_reference) option array * + (int * (int * constr) list * int)) | EliminationCases of int | NotAnElimination @@ -171,24 +172,24 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) = | _ -> raise Elimconst) args in - if list_distinct (List.map fst li) then - let k = lv.(i) in - if k < nargs then + if not (list_distinct (List.map fst li)) then + raise Elimconst; + let k = lv.(i) in + if k < nargs then (* Such an optimisation would need eta-expansion let p = destRel (List.nth args k) in EliminationFix (n-p+1,(nbfix,li,n)) *) - EliminationFix (n,(nbfix,li,n)) - else - EliminationFix (n-nargs+lv.(i)+1,(nbfix,li,n)) - else - raise Elimconst + EliminationFix (n,nargs,(nbfix,li,n)) + else + EliminationFix (n-nargs+k+1,nargs,(nbfix,li,n)) (* Heuristic to look if global names are associated to other components of a mutual fixpoint *) let invert_name labs l na0 env sigma ref = function | Name id -> + let minfxargs = List.length l in if na0 <> Name id then let refi = match ref with | EvalRel _ | EvalEvar _ -> None @@ -205,9 +206,10 @@ let invert_name labs l na0 env sigma ref = function let labs',ccl = decompose_lam c in let _, l' = whd_betalet_stack ccl in let labs' = List.map snd labs' in - if labs' = labs & l = l' then Some ref else None + if labs' = labs & l = l' then Some (minfxargs,ref) + else None with Not_found (* Undefined ref *) -> None - else Some ref + else Some (minfxargs,ref) | Anonymous -> None (* Actually, should not occur *) (* [compute_consteval_direct] expand all constant in a whole, but @@ -242,7 +244,7 @@ let compute_consteval_mutual_fix sigma env ref = (match compute_consteval_direct sigma env ref with | NotAnElimination -> (*Above const was eliminable but this not!*) NotAnElimination - | EliminationFix (minarg',infos) -> + | EliminationFix (minarg',minfxargs,infos) -> let refs = Array.map (invert_name labs l names.(i) env sigma ref) names in @@ -263,7 +265,7 @@ let compute_consteval_mutual_fix sigma env ref = let compute_consteval sigma env ref = match compute_consteval_direct sigma env ref with - | EliminationFix (_,(nbfix,_,_)) when nbfix <> 1 -> + | EliminationFix (_,_,(nbfix,_,_)) when nbfix <> 1 -> compute_consteval_mutual_fix sigma env ref | elim -> elim @@ -323,28 +325,107 @@ let make_elim_fun (names,(nbfix,lv,n)) largs = fun i -> match names.(i) with | None -> None - | Some ref -> + | Some (minargs,ref) -> let body = applistc (mkEvalRef ref) la in let g = list_fold_left_i (fun q (* j from comment is n+1-q *) c (ij,tij) -> let subst = List.map (lift (-q)) (list_firstn (n-ij) la) in let tij' = substl (List.rev subst) tij in mkLambda (x,tij',c)) 1 body (List.rev lv) - in Some g + in Some (minargs,g) (* [f] is convertible to [Fix(recindices,bodynum),bodyvect)]: do so that the reduction uses this extra information *) -let contract_fix_use_function f +let dummy = mkProp +let vfx = id_of_string"_expanded_fix_" +let vfun = id_of_string"_elimminator_function_" + +(* Mark every occurrence of substituted vars (associated to a function) + as a problem variable: an evar that can be instantiated either by + vfx (expanded fixpoint) or vfun (named function). *) +let substl_with_function subst constr = + let cnt = ref 0 in + let evd = ref Evd.empty in + let minargs = ref Intmap.empty in + let v = Array.of_list subst in + let rec subst_total k c = + match kind_of_term c with + Rel i when k + if i <= k + Array.length v then + match v.(i-k-1) with + | (fx,Some(min,ref)) -> + decr cnt; + evd := Evd.add !evd !cnt + (Evd.make_evar + (val_of_named_context + [(vfx,None,dummy);(vfun,None,dummy)]) + dummy); + minargs := Intmap.add !cnt min !minargs; + lift k (mkEvar(!cnt,[|fx;ref|])) + | (fx,None) -> lift k fx + else mkRel (i - Array.length v) + | _ -> + map_constr_with_binders succ subst_total k c in + let c = subst_total 0 constr in + (c,!evd,!minargs) + +exception Partial + +(* each problem variable that cannot be made totally applied even by + reduction is solved by the expanded fix term. *) +let solve_arity_problem env sigma fxminargs c = + let evm = ref sigma in + let set_fix i = evm := Evd.define !evm i (mkVar vfx) in + let rec check strict c = + let c' = whd_betaiotazeta c in + let (h,rcargs) = decompose_app c' in + match kind_of_term h with + Evar(i,_) when Intmap.mem i fxminargs && not (Evd.is_defined !evm i) -> + let minargs = Intmap.find i fxminargs in + if List.length rcargs < minargs then + if strict then set_fix i + else raise Partial; + List.iter (check strict) rcargs + | (Var _|Const _) when isEvalRef env h -> + (match reference_opt_value sigma env (destEvalRef h) with + Some h' -> + let bak = !evm in + (try List.iter (check false) rcargs + with Partial -> + evm := bak; + check strict (applist(h',rcargs))) + | None -> List.iter (check strict) rcargs) + | _ -> iter_constr (check strict) c' in + check true c; + !evm + +let substl_checking_arity env subst c = + (* we initialize the problem: *) + let body,sigma,minargs = substl_with_function subst c in + (* we collect arity constraints *) + let sigma' = solve_arity_problem env sigma minargs body in + (* we propagate the constraints: solved problems are substituted; + the other ones are replaced by the function symbol *) + let rec nf_fix c = + match kind_of_term c with + Evar(i,[|fx;f|] as ev) when Intmap.mem i minargs -> + (match Evd.existential_opt_value sigma' ev with + Some c' -> c' + | None -> f) + | _ -> map_constr nf_fix c in + nf_fix body + + + +let contract_fix_use_function env f ((recindices,bodynum),(_names,_types,bodies as typedbodies)) = let nbodies = Array.length recindices in - let make_Fi j = match f j with - | None -> mkFix((recindices,j),typedbodies) - | Some c -> c in + let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in let lbodies = list_tabulate make_Fi nbodies in - substl (List.rev lbodies) bodies.(bodynum) + substl_checking_arity env (List.rev lbodies) (nf_beta bodies.(bodynum)) -let reduce_fix_use_function f whfun fix stack = +let reduce_fix_use_function env f whfun fix stack = match fix_recarg fix stack with | None -> NotReducible | Some (recargnum,recarg) -> @@ -357,16 +438,15 @@ let reduce_fix_use_function f whfun fix stack = let stack' = stack_assign stack recargnum (app_stack recarg') in (match kind_of_term recarg'hd with | Construct _ -> - Reduced (contract_fix_use_function f fix,stack') + Reduced (contract_fix_use_function env f fix,stack') | _ -> NotReducible) -let contract_cofix_use_function f (bodynum,(_names,_,bodies as typedbodies)) = +let contract_cofix_use_function env f + (bodynum,(_names,_,bodies as typedbodies)) = let nbodies = Array.length bodies in - let make_Fi j = match f j with - | None -> mkCoFix(j,typedbodies) - | Some c -> c in + let make_Fi j = (mkCoFix(j,typedbodies), f j) in let subbodies = list_tabulate make_Fi nbodies in - substl (List.rev subbodies) bodies.(bodynum) + substl_checking_arity env (List.rev subbodies) (nf_beta bodies.(bodynum)) let reduce_mind_case_use_function func env mia = match kind_of_term mia.mconstr with @@ -377,8 +457,9 @@ let reduce_mind_case_use_function func env mia = let build_cofix_name = if isConst func then let (mp,dp,_) = repr_con (destConst func) in + let minargs = List.length mia.mcargs in fun i -> - if i = bodynum then Some func + if i = bodynum then Some (minargs,func) else match names.(i) with | Anonymous -> None | Name id -> @@ -389,11 +470,13 @@ let reduce_mind_case_use_function func env mia = let kn = make_con mp dp (label_of_id id) in try match constant_opt_value env kn with | None -> None - | Some _ -> Some (mkConst kn) + (* TODO: check kn is correct *) + | Some _ -> Some (minargs,mkConst kn) with Not_found -> None else fun _ -> None in - let cofix_def = contract_cofix_use_function build_cofix_name cofix in + let cofix_def = + contract_cofix_use_function env build_cofix_name cofix in mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf) | _ -> assert false @@ -432,12 +515,12 @@ let rec red_elim_const env sigma ref largs = let c', lrest = whd_betadelta_state env sigma (c,largs) in let whfun = whd_simpl_state env sigma in (special_red_case sigma env whfun (destCase c'), lrest) - | EliminationFix (min,infos) when stack_args_size largs >=min -> + | EliminationFix (min,minfxargs,infos) when stack_args_size largs >=min -> let c = reference_value sigma env ref in let d, lrest = whd_betadelta_state env sigma (c,largs) in - let f = make_elim_fun ([|Some ref|],infos) largs in + let f = make_elim_fun ([|Some (minfxargs,ref)|],infos) largs in let whfun = whd_construct_state env sigma in - (match reduce_fix_use_function f whfun (destFix d) lrest with + (match reduce_fix_use_function env f whfun (destFix d) lrest with | NotReducible -> raise Redelimination | Reduced (c,rest) -> (nf_beta c, rest)) | EliminationMutualFix (min,refgoal,refinfos) @@ -453,7 +536,7 @@ let rec red_elim_const env sigma ref largs = let d, lrest = whd_betadelta_state env sigma s in let f = make_elim_fun refinfos midargs in let whfun = whd_construct_state env sigma in - (match reduce_fix_use_function f whfun (destFix d) lrest with + (match reduce_fix_use_function env f whfun (destFix d) lrest with | NotReducible -> raise Redelimination | Reduced (c,rest) -> (nf_beta c, rest)) | _ -> raise Redelimination diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 1ce53e88..f93212f8 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: termops.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: termops.ml 11639 2008-11-27 17:48:32Z barras $ *) open Pp open Util @@ -425,11 +425,11 @@ let fold_constr_with_binders g f n acc c = match kind_of_term c with | Fix (_,(lna,tl,bl)) -> let n' = iterate g (Array.length tl) n in let fd = array_map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n (f n' acc t) b) acc fd + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd | CoFix (_,(lna,tl,bl)) -> let n' = iterate g (Array.length tl) n in let fd = array_map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n (f n' acc t) b) acc fd + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd (* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate subterms of [c]; it carries an extra data [acc] which is processed by [g] at @@ -473,6 +473,13 @@ let occur_existential c = | _ -> iter_constr occrec c in try occrec c; false with Occur -> true +let occur_meta_or_existential c = + let rec occrec c = match kind_of_term c with + | Evar _ -> raise Occur + | Meta _ -> raise Occur + | _ -> iter_constr occrec c + in try occrec c; false with Occur -> true + let occur_const s c = let rec occur_rec c = match kind_of_term c with | Const sp when sp=s -> raise Occur @@ -671,10 +678,18 @@ let subst_term_occ (nowhere_except_in,locs as plocs) c t = if rest <> [] then error_invalid_occurrence rest; t' -let subst_term_occ_decl (nowhere_except_in,locs as plocs) c (id,bodyopt,typ as d) = - match bodyopt with - | None -> (id,None,subst_term_occ plocs c typ) - | Some body -> +type hyp_location_flag = (* To distinguish body and type of local defs *) + | InHyp + | InHypTypeOnly + | InHypValueOnly + +let subst_term_occ_decl ((nowhere_except_in,locs as plocs),hloc) c (id,bodyopt,typ as d) = + match bodyopt,hloc with + | None, InHypValueOnly -> errorlabstrm "" (pr_id id ++ str " has no value") + | None, _ -> (id,None,subst_term_occ plocs c typ) + | Some body, InHypTypeOnly -> (id,Some body,subst_term_occ plocs c typ) + | Some body, InHypValueOnly -> (id,Some (subst_term_occ plocs c body),typ) + | Some body, InHyp -> if locs = [] then if nowhere_except_in then d else (id,Some (subst_term c body),subst_term c typ) @@ -685,7 +700,6 @@ let subst_term_occ_decl (nowhere_except_in,locs as plocs) c (id,bodyopt,typ as d if rest <> [] then error_invalid_occurrence rest; (id,Some body',t') - (* First character of a constr *) let lowercase_first_char id = @@ -1040,6 +1054,19 @@ let global_vars_set_of_decl env = function Idset.union (global_vars_set env t) (global_vars_set env c) +let dependency_closure env sign hyps = + if Idset.is_empty hyps then [] else + let (_,lh) = + Sign.fold_named_context_reverse + (fun (hs,hl) (x,_,_ as d) -> + if Idset.mem x hs then + (Idset.union (global_vars_set_of_decl env d) (Idset.remove x hs), + x::hl) + else (hs,hl)) + ~init:(hyps,[]) + sign in + List.rev lh + let default_x = id_of_string "x" let rec next_name_away_in_cases_pattern id avoid = diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 645b7d72..d44c762e 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: termops.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) +(*i $Id: termops.mli 11639 2008-11-27 17:48:32Z barras $ i*) open Util open Pp @@ -93,6 +93,7 @@ val strip_head_cast : constr -> constr exception Occur val occur_meta : types -> bool val occur_existential : types -> bool +val occur_meta_or_existential : types -> bool val occur_const : constant -> types -> bool val occur_evar : existential_key -> types -> bool val occur_in_global : env -> identifier -> constr -> unit @@ -147,8 +148,15 @@ val subst_term_occ : occurrences -> constr -> constr -> constr (* [subst_term_occ_decl occl c decl] replaces occurrences of [c] at positions [occl] by [Rel 1] in [decl] *) + +type hyp_location_flag = (* To distinguish body and type of local defs *) + | InHyp + | InHypTypeOnly + | InHypValueOnly + val subst_term_occ_decl : - occurrences -> constr -> named_declaration -> named_declaration + occurrences * hyp_location_flag -> constr -> named_declaration -> + named_declaration val error_invalid_occurrence : int list -> 'a @@ -244,6 +252,10 @@ val make_all_name_different : env -> env val global_vars : env -> constr -> identifier list val global_vars_set_of_decl : env -> named_declaration -> Idset.t +(* Gives an ordered list of hypotheses, closed by dependencies, + containing a given set *) +val dependency_closure : env -> named_context -> Idset.t -> identifier list + (* Test if an identifier is the basename of a global reference *) val is_section_variable : identifier -> bool diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 86168a1f..8680e578 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: typeclasses.ml 11282 2008-07-28 11:51:53Z msozeau $ i*) +(*i $Id: typeclasses.ml 11576 2008-11-10 19:13:15Z msozeau $ i*) (*i*) open Names @@ -35,25 +35,24 @@ type typeclass = { cl_impl : global_reference; (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *) - cl_context : ((global_reference * bool) option * rel_declaration) list; + cl_context : (global_reference * bool) option list * rel_context; (* Context of definitions and properties on defs, will not be shared *) cl_props : rel_context; (* The method implementaions as projections. *) - cl_projs : (identifier * constant) list; + cl_projs : (identifier * constant option) list; } type typeclasses = (global_reference, typeclass) Gmap.t -type globality = int option - type instance = { is_class: global_reference; is_pri: int option; - is_global: globality; (* Sections where the instance should be redeclared, - Some n for n sections, None for discard at end of section. *) + -1 for discard, 0 for none, mutable to avoid redeclarations + when multiple rebuild_object happen. *) + is_global: int ref; is_impl: constant; } @@ -64,13 +63,13 @@ let instance_impl is = is.is_impl let new_instance cl pri glob impl = let global = if Lib.sections_are_opened () then - if glob then Some (Lib.sections_depth ()) - else None - else Some 0 + if glob then Lib.sections_depth () + else -1 + else 0 in { is_class = cl.cl_impl; is_pri = pri ; - is_global = global ; + is_global = ref global ; is_impl = impl } let classes : typeclasses ref = ref Gmap.empty @@ -112,7 +111,7 @@ let gmap_cmap_merge old ne = ne Gmap.empty in Gmap.fold (fun cl insts acc -> - if Gmap.mem cl ne' then acc + if Gmap.mem cl acc then acc else Gmap.add cl insts acc) old ne' @@ -138,23 +137,21 @@ let subst (_,subst,(cl,m,inst)) = and do_subst c = Mod_subst.subst_mps subst c and do_subst_gr gr = fst (subst_global subst gr) in - let do_subst_named ctx = + let do_subst_ctx ctx = list_smartmap (fun (na, b, t) -> (na, Option.smartmap do_subst b, do_subst t)) ctx in - let do_subst_ctx ctx = - list_smartmap (fun (cl, (na, b, t)) -> - (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b) cl, - (na, Option.smartmap do_subst b, do_subst t))) - ctx + let do_subst_context (grs,ctx) = + list_smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs, + do_subst_ctx ctx in - let do_subst_projs projs = list_smartmap (fun (x, y) -> (x, do_subst_con y)) projs in + let do_subst_projs projs = list_smartmap (fun (x, y) -> (x, Option.smartmap do_subst_con y)) projs in let subst_class k cl classes = let k = do_subst_gr k in let cl' = { cl_impl = k; - cl_context = do_subst_ctx cl.cl_context; - cl_props = do_subst_named cl.cl_props; + cl_context = do_subst_context cl.cl_context; + cl_props = do_subst_ctx cl.cl_props; cl_projs = do_subst_projs cl.cl_projs; } in let cl' = if cl' = cl then cl else cl' in @@ -173,14 +170,18 @@ let subst (_,subst,(cl,m,inst)) = let instances = Gmap.fold subst_inst inst Gmap.empty in (classes, m, instances) +let rel_of_variable_context ctx = + List.fold_right (fun (n,_,b,t) (ctx', subst)-> + let decl = (Name n, Option.map (substn_vars 1 subst) b, substn_vars 1 subst t) in + (decl :: ctx', n :: subst)) ctx ([], []) + let discharge (_,(cl,m,inst)) = - let discharge_context subst rel = + let discharge_rel_context subst n rel = let ctx, _ = List.fold_right - (fun (gr, (id, b, t)) (ctx, k) -> - let gr' = Option.map (fun (gr, b) -> Lib.discharge_global gr, b) gr in - ((gr', (id, Option.map (substn_vars k subst) b, substn_vars k subst t)) :: ctx), succ k) - rel ([], 0) + (fun (id, b, t) (ctx, k) -> + (id, Option.smartmap (substn_vars k subst) b, substn_vars k subst t) :: ctx, succ k) + rel ([], n) in ctx in let abs_context cl = @@ -189,17 +190,22 @@ let discharge (_,(cl,m,inst)) = | ConstRef cst -> Lib.section_segment_of_constant cst | IndRef (ind,_) -> Lib.section_segment_of_mutual_inductive ind in + let discharge_context ctx' subst (grs, ctx) = + let grs' = List.map (fun _ -> None) subst @ + list_smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs + in grs', discharge_rel_context subst 1 ctx @ ctx' + in let subst_class k cl acc = let cl_impl' = Lib.discharge_global cl.cl_impl in let cl' = if cl_impl' == cl.cl_impl then cl else let ctx = abs_context cl in - { cl with cl_impl = cl_impl'; - cl_context = - List.map (fun (na,impl,b,t) -> None, (Name na,b,t)) ctx @ - (discharge_context (List.map (fun (na, _, _, _) -> na) ctx) cl.cl_context); - cl_projs = list_smartmap (fun (x, y) -> x, Lib.discharge_con y) cl.cl_projs } + let ctx', subst = rel_of_variable_context ctx in + { cl_impl = cl_impl'; + cl_context = discharge_context ctx' subst cl.cl_context; + cl_props = discharge_rel_context subst (succ (List.length (fst cl.cl_context))) cl.cl_props; + cl_projs = list_smartmap (fun (x, y) -> x, Option.smartmap Lib.discharge_con y) cl.cl_projs } in Gmap.add cl_impl' cl' acc in let classes = Gmap.fold subst_class cl Gmap.empty in @@ -220,13 +226,13 @@ let rebuild (cl,m,inst) = let inst = Gmap.map (fun insts -> Cmap.fold (fun k is insts -> - match is.is_global with - | None -> insts - | Some 0 -> Cmap.add k is insts - | Some n -> + match !(is.is_global) with + | -1 -> insts + | 0 -> Cmap.add k is insts + | n -> add_instance_hint is.is_impl is.is_pri; - let is' = { is with is_global = Some (pred n) } - in Cmap.add k is' insts) insts Cmap.empty) + is.is_global := pred n; + Cmap.add k is insts) insts Cmap.empty) inst in (cl, m, inst) @@ -247,7 +253,10 @@ let update () = let add_class c = classes := Gmap.add c.cl_impl c !classes; - methods := List.fold_left (fun acc x -> Gmap.add (snd x) c.cl_impl acc) !methods c.cl_projs; + methods := List.fold_left (fun acc x -> + match snd x with + | Some m -> Gmap.add m c.cl_impl acc + | None -> acc) !methods c.cl_projs; update () let class_info c = @@ -255,7 +264,7 @@ let class_info c = with _ -> not_a_class (Global.env()) (constr_of_global c) let instance_constructor cl args = - let pars = fst (list_chop (List.length cl.cl_context) args) in + let pars = fst (list_chop (List.length (fst cl.cl_context)) args) in match cl.cl_impl with | IndRef ind -> applistc (mkConstruct (ind, 1)) args, applistc (mkInd ind) pars @@ -319,19 +328,15 @@ let is_implicit_arg k = | InternalHole -> true | _ -> false -let class_of_constr c = - let extract_cl c = - try Some (class_info (global_of_constr c)) with _ -> None - in - match kind_of_term c with - App (c, _) -> extract_cl c - | _ -> extract_cl c - -let dest_class_app c = - let cl c = class_info (global_of_constr c) in - match kind_of_term c with - App (c, args) -> cl c, args - | _ -> cl c, [||] +let global_class_of_constr env c = + try class_info (global_of_constr c) + with Not_found -> not_a_class env c + +let dest_class_app env c = + let cl, args = decompose_app c in + global_class_of_constr env cl, args + +let class_of_constr c = try Some (fst (dest_class_app (Global.env ()) c)) with _ -> None (* To embed a boolean for resolvability status. This is essentially a hack to mark which evars correspond to diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index fdbb78a9..d8e15895 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: typeclasses.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) +(*i $Id: typeclasses.mli 11576 2008-11-10 19:13:15Z msozeau $ i*) (*i*) open Names @@ -25,18 +25,20 @@ open Util (* This module defines type-classes *) type typeclass = { (* The class implementation: a record parameterized by the context with defs in it or a definition if - the class is a singleton. This acts as the classe's global identifier. *) + the class is a singleton. This acts as the class' global identifier. *) cl_impl : global_reference; (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. - The boolean indicates if the typeclass argument is a direct superclass. *) - cl_context : ((global_reference * bool) option * rel_declaration) list; + The boolean indicates if the typeclass argument is a direct superclass and the global reference + gives a direct link to the class itself. *) + cl_context : (global_reference * bool) option list * rel_context; (* Context of definitions and properties on defs, will not be shared *) cl_props : rel_context; - (* The methods implementations of the typeclass as projections. *) - cl_projs : (identifier * constant) list; + (* The methods implementations of the typeclass as projections. Some may be undefinable due to + sorting restrictions. *) + cl_projs : (identifier * constant option) list; } type instance @@ -52,9 +54,13 @@ val add_instance : instance -> unit val class_info : global_reference -> typeclass (* raises a UserError if not a class *) -val class_of_constr : constr -> typeclass option -val dest_class_app : constr -> typeclass * constr array (* raises a UserError if not a class *) +(* These raise a UserError if not a class. *) +val dest_class_app : env -> constr -> typeclass * constr list + +(* Just return None if not a class *) +val class_of_constr : constr -> typeclass option + val instance_impl : instance -> constant val is_class : global_reference -> bool diff --git a/pretyping/unification.ml b/pretyping/unification.ml index b3c920a2..981a5605 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: unification.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: unification.ml 11819 2009-01-20 20:04:50Z herbelin $ *) open Pp open Util @@ -86,18 +86,22 @@ let rec subst_meta_instances bl c = | Meta i -> (try assoc_pair i bl with Not_found -> c) | _ -> map_constr (subst_meta_instances bl) c -let solve_pattern_eqn_array env f l c (metasubst,evarsubst) = +let solve_pattern_eqn_array (env,nb) sigma f l c (metasubst,evarsubst) = match kind_of_term f with | Meta k -> let c = solve_pattern_eqn env (Array.to_list l) c in let n = Array.length l - List.length (fst (decompose_lam c)) in let pb = (ConvUpToEta n,TypeNotProcessed) in - (k,c,pb)::metasubst,evarsubst + if noccur_between 1 nb c then + (k,lift (-nb) c,pb)::metasubst,evarsubst + else error_cannot_unify_local env sigma (mkApp (f, l),c,c) | Evar ev -> (* Currently unused: incompatible with eauto/eassumption backtracking *) metasubst,(ev,solve_pattern_eqn env (Array.to_list l) c)::evarsubst | _ -> assert false +let push d (env,n) = (push_rel_assum d env,n+1) + (*******************************) (* Unification à l'ordre 0 de m et n: [unify_0 env sigma cv_pb m n] @@ -136,28 +140,47 @@ let default_no_delta_unify_flags = { modulo_delta = empty_transparent_state; } -let expand_constant env flags c = - match kind_of_term c with +let expand_key env = function + | Some (ConstKey cst) -> constant_opt_value env cst + | Some (VarKey id) -> named_body id env + | Some (RelKey _) -> None + | None -> None + +let key_of flags f = + match kind_of_term f with | Const cst when is_transparent (ConstKey cst) && - Cpred.mem cst (snd flags.modulo_delta) -> - constant_opt_value env cst + Cpred.mem cst (snd flags.modulo_delta) -> + Some (ConstKey cst) | Var id when is_transparent (VarKey id) && - Idpred.mem id (fst flags.modulo_delta) -> - named_body id env + Idpred.mem id (fst flags.modulo_delta) -> + Some (VarKey id) | _ -> None - + +let oracle_order env cf1 cf2 = + match cf1 with + | None -> + (match cf2 with + | None -> None + | Some k2 -> Some false) + | Some k1 -> + match cf2 with + | None -> Some true + | Some k2 -> Some (Conv_oracle.oracle_order k1 k2) + let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n = - let nb = nb_rel env in - let trivial_unify pb (metasubst,_) m n = + let trivial_unify curenv pb (metasubst,_) m n = let subst = if flags.use_metas_eagerly then metasubst else fst subst in match subst_defined_metas subst m with - | Some m -> - (match flags.modulo_conv_on_closed_terms with + | Some m1 -> + if (match flags.modulo_conv_on_closed_terms with Some flags -> - is_trans_fconv (conv_pb_of pb) flags env sigma m n - | None -> constr_cmp (conv_pb_of cv_pb) m n) - | _ -> constr_cmp (conv_pb_of cv_pb) m n in - let rec unirec_rec curenv pb b ((metasubst,evarsubst) as substn) curm curn = + is_trans_fconv (conv_pb_of pb) flags env sigma m1 n + | None -> false) then true else + if (not (is_ground_term (create_evar_defs sigma) m1)) + || occur_meta_or_existential n then false else + error_cannot_unify curenv sigma (m, n) + | _ -> false in + let rec unirec_rec (curenv,nb as curenvnb) pb b ((metasubst,evarsubst) as substn) curm curn = let cM = Evarutil.whd_castappevar sigma curm and cN = Evarutil.whd_castappevar sigma curn in match (kind_of_term cM,kind_of_term cN) with @@ -167,41 +190,48 @@ let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n = then (k1,cN,stN)::metasubst,evarsubst else if k1 = k2 then substn else (k2,cM,stM)::metasubst,evarsubst - | Meta k, _ -> + | Meta k, _ when not (dependent cM cN) -> (* Here we check that [cN] does not contain any local variables *) - if (closedn nb cN) - then (k,cN,snd (extract_instance_status pb))::metasubst,evarsubst + if nb = 0 then + (k,cN,snd (extract_instance_status pb))::metasubst,evarsubst + else if noccur_between 1 nb cN then + (k,lift (-nb) cN,snd (extract_instance_status pb))::metasubst, + evarsubst else error_cannot_unify_local curenv sigma (m,n,cN) - | _, Meta k -> + | _, Meta k when not (dependent cN cM) -> (* Here we check that [cM] does not contain any local variables *) - if (closedn nb cM) - then (k,cM,fst (extract_instance_status pb))::metasubst,evarsubst + if nb = 0 then + (k,cM,snd (extract_instance_status pb))::metasubst,evarsubst + else if noccur_between 1 nb cM + then + (k,lift (-nb) cM,fst (extract_instance_status pb))::metasubst, + evarsubst else error_cannot_unify_local curenv sigma (m,n,cM) | Evar ev, _ -> metasubst,((ev,cN)::evarsubst) | _, Evar ev -> metasubst,((ev,cM)::evarsubst) | Lambda (na,t1,c1), Lambda (_,t2,c2) -> - unirec_rec (push_rel_assum (na,t1) curenv) topconv true - (unirec_rec curenv topconv true substn t1 t2) c1 c2 + unirec_rec (push (na,t1) curenvnb) topconv true + (unirec_rec curenvnb topconv true substn t1 t2) c1 c2 | Prod (na,t1,c1), Prod (_,t2,c2) -> - unirec_rec (push_rel_assum (na,t1) curenv) (prod_pb pb) true - (unirec_rec curenv topconv true substn t1 t2) c1 c2 - | LetIn (_,a,_,c), _ -> unirec_rec curenv pb b substn (subst1 a c) cN - | _, LetIn (_,a,_,c) -> unirec_rec curenv pb b substn cM (subst1 a c) + unirec_rec (push (na,t1) curenvnb) (prod_pb pb) true + (unirec_rec curenvnb topconv true substn t1 t2) c1 c2 + | LetIn (_,a,_,c), _ -> unirec_rec curenvnb pb b substn (subst1 a c) cN + | _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb b substn cM (subst1 a c) | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) -> - array_fold_left2 (unirec_rec curenv topconv true) - (unirec_rec curenv topconv true - (unirec_rec curenv topconv true substn p1 p2) c1 c2) cl1 cl2 + array_fold_left2 (unirec_rec curenvnb topconv true) + (unirec_rec curenvnb topconv true + (unirec_rec curenvnb topconv true substn p1 p2) c1 c2) cl1 cl2 | App (f1,l1), _ when - isMeta f1 & is_unification_pattern curenv f1 l1 & + isMeta f1 & is_unification_pattern curenvnb f1 l1 cN & not (dependent f1 cN) -> - solve_pattern_eqn_array curenv f1 l1 cN substn + solve_pattern_eqn_array curenvnb sigma f1 l1 cN substn | _, App (f2,l2) when - isMeta f2 & is_unification_pattern curenv f2 l2 & + isMeta f2 & is_unification_pattern curenvnb f2 l2 cM & not (dependent f2 cM) -> - solve_pattern_eqn_array curenv f2 l2 cM substn + solve_pattern_eqn_array curenvnb sigma f2 l2 cM substn | App (f1,l1), App (f2,l2) -> let len1 = Array.length l1 @@ -216,43 +246,66 @@ let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n = let extras,restl1 = array_chop (len1-len2) l1 in (appvect (f1,extras), restl1, f2, l2) in let pb = ConvUnderApp (len1,len2) in - array_fold_left2 (unirec_rec curenv topconv true) - (unirec_rec curenv pb true substn f1 f2) l1 l2 + array_fold_left2 (unirec_rec curenvnb topconv true) + (unirec_rec curenvnb pb true substn f1 f2) l1 l2 with ex when precatchable_exception ex -> - expand curenv pb b substn cM f1 l1 cN f2 l2) + expand curenvnb pb b substn cM f1 l1 cN f2 l2) - | _ -> + | _ -> + if constr_cmp (conv_pb_of cv_pb) cM cN then substn else let (f1,l1) = match kind_of_term cM with App (f,l) -> (f,l) | _ -> (cM,[||]) in let (f2,l2) = match kind_of_term cN with App (f,l) -> (f,l) | _ -> (cN,[||]) in - expand curenv pb b substn cM f1 l1 cN f2 l2 + expand curenvnb pb b substn cM f1 l1 cN f2 l2 - and expand curenv pb b substn cM f1 l1 cN f2 l2 = - if trivial_unify pb substn cM cN then substn + and expand (curenv,_ as curenvnb) pb b substn cM f1 l1 cN f2 l2 = + if trivial_unify curenv pb substn cM cN then substn else if b then - match expand_constant curenv flags f1 with - | Some c -> - unirec_rec curenv pb b substn (whd_betaiotazeta (mkApp(c,l1))) cN - | None -> - match expand_constant curenv flags f2 with - | Some c -> - unirec_rec curenv pb b substn cM (whd_betaiotazeta (mkApp(c,l2))) - | None -> - error_cannot_unify curenv sigma (cM,cN) + let cf1 = key_of flags f1 and cf2 = key_of flags f2 in + match oracle_order curenv cf1 cf2 with + | None -> error_cannot_unify curenv sigma (cM,cN) + | Some true -> + (match expand_key curenv cf1 with + | Some c -> + unirec_rec curenvnb pb b substn (whd_betaiotazeta (mkApp(c,l1))) cN + | None -> + (match expand_key curenv cf2 with + | Some c -> + unirec_rec curenvnb pb b substn cM (whd_betaiotazeta (mkApp(c,l2))) + | None -> + error_cannot_unify curenv sigma (cM,cN))) + | Some false -> + (match expand_key curenv cf2 with + | Some c -> + unirec_rec curenvnb pb b substn cM (whd_betaiotazeta (mkApp(c,l2))) + | None -> + (match expand_key curenv cf1 with + | Some c -> + unirec_rec curenvnb pb b substn (whd_betaiotazeta (mkApp(c,l1))) cN + | None -> + error_cannot_unify curenv sigma (cM,cN))) else error_cannot_unify curenv sigma (cM,cN) in - if (not(occur_meta m)) && - (match flags.modulo_conv_on_closed_terms with + if (if occur_meta m then false else + if (match flags.modulo_conv_on_closed_terms with Some flags -> is_trans_fconv (conv_pb_of cv_pb) flags env sigma m n - | None -> constr_cmp (conv_pb_of cv_pb) m n) - then + | None -> constr_cmp (conv_pb_of cv_pb) m n) then true else + if (not (is_ground_term (create_evar_defs sigma) m)) + || occur_meta_or_existential n then false else + if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with + | Some (cv_id, cv_k), (dl_id, dl_k) -> + Idpred.subset dl_id cv_id && Cpred.subset dl_k cv_k + | None,(dl_id, dl_k) -> + Idpred.is_empty dl_id && Cpred.is_empty dl_k) + then error_cannot_unify env sigma (m, n) else false) + then subst else - unirec_rec env cv_pb conv_at_top subst m n + unirec_rec (env,0) cv_pb conv_at_top subst m n let unify_0 = unify_0_with_initial_metas ([],[]) true @@ -428,7 +481,7 @@ let w_coerce_to_type env evd c cty mvty = try_to_coerce env evd c cty tycon let w_coerce env evd mv c = - let cty = get_type_of env (evars_of evd) c in + let cty = get_type_of_with_meta env (evars_of evd) (metas_of evd) c in let mvty = Typing.meta_type evd mv in w_coerce_to_type env evd c cty mvty @@ -443,7 +496,7 @@ let unify_to_type env evd flags c u = let unify_type env evd flags mv c = let mvty = Typing.meta_type evd mv in - if occur_meta mvty then + if occur_meta_or_existential mvty then unify_to_type env evd flags c mvty else ([],[]) @@ -490,9 +543,9 @@ let w_merge env with_types flags (metas,evars) evd = let evd' = mimick_evar evd flags f (Array.length cl) evn in w_merge_rec evd' metas evars eqns | _ -> - w_merge_rec (solve_simple_evar_eqn env evd ev rhs') - metas evars' eqns - end + w_merge_rec (solve_simple_evar_eqn env evd ev rhs') + metas evars' eqns + end | [] -> (* Process metas *) @@ -536,7 +589,7 @@ let w_merge env with_types flags (metas,evars) evd = let (evd', c) = applyHead sp_env evd nargs hdc in let (mc,ec) = unify_0 sp_env (evars_of evd') Cumul flags - (Retyping.get_type_of sp_env (evars_of evd') c) ev.evar_concl in + (Retyping.get_type_of_with_meta sp_env (evars_of evd') (metas_of evd') c) ev.evar_concl in let evd'' = w_merge_rec evd' mc ec [] in if (evars_of evd') == (evars_of evd'') then Evd.evar_define sp c evd'' @@ -559,10 +612,10 @@ let w_unify_meta_types env ?(flags=default_unify_flags) evd = [clenv_typed_unify M N clenv] expects in addition that expected types of metavars are unifiable with the types of their instances *) -let check_types env evd subst m n = +let check_types env evd flags subst m n = if isEvar (fst (whd_stack m)) or isEvar (fst (whd_stack n)) then unify_0_with_initial_metas subst true env (evars_of evd) topconv - default_unify_flags + flags (Retyping.get_type_of_with_meta env (evars_of evd) (metas_of evd) m) (Retyping.get_type_of_with_meta env (evars_of evd) (metas_of evd) n) else @@ -570,7 +623,7 @@ let check_types env evd subst m n = let w_unify_core_0 env with_types cv_pb flags m n evd = let (mc1,evd') = retract_coercible_metas evd in - let subst1 = check_types env evd (mc1,[]) m n in + let subst1 = check_types env evd flags (mc1,[]) m n in let subst2 = unify_0_with_initial_metas subst1 true env (evars_of evd') cv_pb flags m n in @@ -659,7 +712,7 @@ let w_unify_to_subterm_list env flags allow_K oplist t evd = if isMeta op then if allow_K then (evd,op::l) else error "Match_subterm" - else if occur_meta op then + else if occur_meta_or_existential op then let (evd',cl) = try (* This is up to delta for subterms w/o metas ... *) diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 465c062b..5d09570e 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vnorm.ml 11017 2008-05-29 13:00:24Z barras $ i*) +(*i $Id: vnorm.ml 11424 2008-09-30 12:10:28Z jforest $ i*) open Names open Declarations @@ -20,7 +20,7 @@ open Vm (* Calcul de la forme normal d'un terme *) (*******************************************) -let crazy_type = mkSet +let crazy_type = mkSet let decompose_prod env t = let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in @@ -178,7 +178,7 @@ and nf_stk env c t stk = nf_stk env (mkApp(c,args)) t stk | Zfix (f,vargs) :: stk -> let fa, typ = nf_fix_app env f vargs in - let _,_,codom = decompose_prod env typ in + let _,_,codom = try decompose_prod env typ with _ -> exit 120 in nf_stk env (mkApp(fa,[|c|])) (subst1 c codom) stk | Zswitch sw :: stk -> let (mind,_ as ind),allargs = find_rectype_a env t in @@ -187,6 +187,7 @@ and nf_stk env c t stk = let params,realargs = Util.array_chop nparams allargs in let pT = hnf_prod_applist env (type_of_ind env ind) (Array.to_list params) in + let pT = whd_betadeltaiota env pT in let dep, p = nf_predicate env ind mip params (type_of_switch sw) pT in (* Calcul du type des branches *) let btypes = build_branches_type env ind mib mip params dep p in @@ -210,7 +211,7 @@ and nf_predicate env ind mip params v pT = | Vfun f, Prod _ -> let k = nb_rel env in let vb = body_of_vfun k f in - let name,dom,codom = decompose_prod env pT in + let name,dom,codom = try decompose_prod env pT with _ -> exit 121 in let dep,body = nf_predicate (push_rel (name,None,dom) env) ind mip params vb codom in dep, mkLambda(name,dom,body) @@ -232,7 +233,7 @@ and nf_args env vargs t = let args = Array.init len (fun i -> - let _,dom,codom = decompose_prod env !t in + let _,dom,codom = try decompose_prod env !t with _ -> exit 123 in let c = nf_val env (arg vargs i) dom in t := subst1 c codom; c) in !t,args @@ -243,7 +244,7 @@ and nf_bargs env b t = let args = Array.init len (fun i -> - let _,dom,codom = decompose_prod env !t in + let _,dom,codom = try decompose_prod env !t with _ -> exit 124 in let c = nf_val env (bfield b i) dom in t := subst1 c codom; c) in args @@ -251,7 +252,11 @@ and nf_bargs env b t = and nf_fun env f typ = let k = nb_rel env in let vb = body_of_vfun k f in - let name,dom,codom = decompose_prod env typ in + let name,dom,codom = + try decompose_prod env typ + with _ -> + raise (Type_errors.TypeError(env,Type_errors.ReferenceVariables typ)) + in let body = nf_val (push_rel (name,None,dom) env) vb codom in mkLambda(name,dom,body) -- cgit v1.2.3