diff options
Diffstat (limited to 'pretyping')
44 files changed, 900 insertions, 621 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index ca1d0b7fba..e18aece090 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -16,12 +16,12 @@ open Libobject (*i*) let name_table = - Summary.ref (Refmap.empty : Name.t list list Refmap.t) + Summary.ref (Refmap.empty : Name.t list Refmap.t) ~name:"rename-arguments" type req = | ReqLocal - | ReqGlobal of global_reference * Name.t list list + | ReqGlobal of global_reference * Name.t list let load_rename_args _ (_, (_, (r, names))) = name_table := Refmap.add r names !name_table @@ -49,7 +49,7 @@ let discharge_rename_args = function let vars,_,_ = section_segment_of_reference c in let c' = pop_global_reference c in let var_names = List.map (fun (id, _,_,_) -> Name id) vars in - let names' = List.map (fun l -> var_names @ l) names in + let names' = var_names @ names in Some (ReqGlobal (c', names), (c', names')) with Not_found -> Some req) | _ -> None @@ -83,7 +83,7 @@ let rec rename_prod c = function | _ -> c let rename_type ty ref = - try rename_prod ty (List.hd (arguments_names ref)) + try rename_prod ty (arguments_names ref) with Not_found -> ty let rename_type_of_constant env c = diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli index a334055011..e123e77862 100644 --- a/pretyping/arguments_renaming.mli +++ b/pretyping/arguments_renaming.mli @@ -11,10 +11,10 @@ open Globnames open Environ open Term -val rename_arguments : bool -> global_reference -> Name.t list list -> unit +val rename_arguments : bool -> global_reference -> Name.t list -> unit -(** [Not_found] is raised is no names are defined for [r] *) -val arguments_names : global_reference -> Name.t list list +(** [Not_found] is raised if no names are defined for [r] *) +val arguments_names : global_reference -> Name.t list val rename_type_of_constant : env -> pconstant -> types val rename_type_of_inductive : env -> pinductive -> types diff --git a/pretyping/cases.ml b/pretyping/cases.ml index b8fb61e35d..aa24733d9f 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Nameops @@ -62,13 +62,15 @@ let error_wrong_numarg_constructor_loc loc env c n = let error_wrong_numarg_inductive_loc loc env c n = raise_pattern_matching_error (loc, env, Evd.empty, WrongNumargInductive(c,n)) -let rec list_try_compile f = function - | [a] -> f a - | [] -> anomaly (str "try_find_f") +let list_try_compile f l = + let rec aux errors = function + | [] -> if errors = [] then anomaly (str "try_find_f") else iraise (List.last errors) | h::t -> try f h - with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ -> - list_try_compile f t + with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e -> + let e = CErrors.push e in + aux (e::errors) t in + aux [] l let force_name = let nx = Name default_dependent_ident in function Anonymous -> nx | na -> na @@ -1329,14 +1331,6 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn *) -let mk_case pb (ci,pred,c,brs) = - let mib = lookup_mind (fst ci.ci_ind) pb.env in - match mib.mind_record with - | Some (Some (_, cs, pbs)) -> - Reduction.beta_appvect brs.(0) - (Array.map (fun p -> mkProj (Projection.make p true, c)) cs) - | _ -> mkCase (ci,pred,c,brs) - (**********************************************************************) (* Main compiling descent *) let rec compile pb = @@ -1383,7 +1377,9 @@ and match_current pb (initial,tomatch) = pred current indt (names,dep) tomatch in let ci = make_case_info pb.env (fst mind) pb.casestyle in let pred = nf_betaiota !(pb.evdref) pred in - let case = mk_case pb (ci,pred,current,brvals) in + let case = + make_case_or_project pb.env indf ci pred current brvals + in Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred; { uj_val = applist (case, inst); uj_type = prod_applist typ inst } @@ -1708,7 +1704,7 @@ let build_inversion_problem loc env sigma tms t = let id = next_name_away (named_hd env t Anonymous) avoid in PatVar (Loc.ghost,Name id), ((id,t)::subst, id::avoid) in let rec reveal_pattern t (subst,avoid as acc) = - match kind_of_term (whd_betadeltaiota env sigma t) with + match kind_of_term (whd_all env sigma t) with | Construct (cstr,u) -> PatCstr (Loc.ghost,cstr,[],Anonymous), acc | App (f,v) when isConstruct f -> let cstr,u = destConstruct f in @@ -1801,14 +1797,10 @@ let build_inversion_problem loc env sigma tms t = it = None } } ] in (* [pb] is the auxiliary pattern-matching serving as skeleton for the return type of the original problem Xi *) - (* let sigma, s = Evd.new_sort_variable sigma in *) -(*FIXME TRY *) - (* let sigma, s = Evd.new_sort_variable univ_flexible sigma in *) let s' = Retyping.get_sort_of env sigma t in let sigma, s = Evd.new_sort_variable univ_flexible_alg sigma in let sigma = Evd.set_leq_sort env sigma s' s in let evdref = ref sigma in - (* let ty = evd_comb1 (refresh_universes false) evdref ty in *) let pb = { env = pb_env; evdref = evdref; @@ -1881,7 +1873,7 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon = (* We put the tycon inside the arity signature, possibly discovering dependencies. *) let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = - let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in + let nar = List.fold_left (fun n sign -> Context.Rel.nhyps sign + n) 0 arsign in let subst, len = List.fold_right2 (fun (tm, tmtype) sign (subst, len) -> let signlen = List.length sign in @@ -1944,7 +1936,7 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = let preds = match pred, tycon with - (* No type annotation *) + (* No return clause *) | None, Some t when not (noccur_with_meta 0 max_int t) -> (* If the tycon is not closed w.r.t real variables, we try *) (* two different strategies *) @@ -1981,12 +1973,6 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = let evdref = ref sigma in let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref rtntyp in let sigma = !evdref in - (* let sigma = Option.cata (fun tycon -> *) - (* let na = Name (Id.of_string "x") in *) - (* let tms = List.map (fun tm -> Pushed(tm,[],na)) tomatchs in *) - (* let predinst = extract_predicate predcclj.uj_val tms in *) - (* Coercion.inh_conv_coerce_to loc env !evdref predinst tycon) *) - (* !evdref tycon in *) let predccl = (j_nf_evar sigma predcclj).uj_val in [sigma, predccl] in @@ -2032,7 +2018,9 @@ let mk_JMeq evdref typ x typ' y = let mk_JMeq_refl evdref typ x = papp evdref coq_JMeq_refl [| typ; x |] -let hole = GHole (Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define true), Misctypes.IntroAnonymous, None) +let hole = + GHole (Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false), + Misctypes.IntroAnonymous, None) let constr_of_pat env evdref arsign pat avoid = let rec typ env (ty, realargs) pat avoid = @@ -2434,7 +2422,7 @@ let compile_program_cases loc style (typing_function, evdref) tycon env match tycon' with | None -> let ev = mkExistential env evdref in ev, ev | Some t -> - let pred = + let pred = match prepare_predicate_from_arsign_tycon env !evdref loc tomatchs sign t with | Some (evd, pred) -> evdref := evd; pred | None -> @@ -2513,11 +2501,11 @@ let compile_program_cases loc style (typing_function, evdref) tycon env (* Main entry of the matching compilation *) let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) = - if predopt == None && Flags.is_program_mode () then - compile_program_cases loc style (typing_fun, evdref) + if predopt == None && Flags.is_program_mode () && Program.is_program_cases () then + compile_program_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) else - + (* We build the matrix of patterns and right-hand side *) let matx = matx_of_eqns env eqns in @@ -2579,6 +2567,9 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e typing_function = typing_fun } in let j = compile pb in + + (* We coerce to the tycon (if an elim predicate was provided) *) + let j = inh_conv_coerce_to_tycon loc env myevdref j tycon in evdref := !myevdref; j in @@ -2589,6 +2580,4 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e (* We check for unused patterns *) List.iter (check_unused_pattern env) matx; - (* We coerce to the tycon (if an elim predicate was provided) *) - inh_conv_coerce_to_tycon loc env evdref j tycon - + j diff --git a/pretyping/cases.mli b/pretyping/cases.mli index d7fff8af4b..ba566f3744 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -121,4 +121,3 @@ val prepare_predicate : Loc.t -> Context.Rel.t list -> Constr.constr option -> 'a option -> (Evd.evar_map * Names.name list * Term.constr) list - diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index afd86420e9..84bf849e76 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -10,7 +10,7 @@ open Util open Names open Term open Vars -open Closure +open CClosure open Esubst (**** Call by value reduction ****) @@ -156,7 +156,7 @@ let strip_appl head stack = (* Tests if fixpoint reduction is possible. *) let fixp_reducible flgs ((reci,i),_) stk = - if red_set flgs fIOTA then + if red_set flgs fFIX then match stk with | APP(appl,_) -> Array.length appl > reci.(i) && @@ -168,7 +168,7 @@ let fixp_reducible flgs ((reci,i),_) stk = false let cofixp_reducible flgs _ stk = - if red_set flgs fIOTA then + if red_set flgs fCOFIX then match stk with | (CASE _ | APP(_,CASE _)) -> true | _ -> false @@ -296,19 +296,19 @@ and cbv_stack_value info env = function (* constructor in a Case -> IOTA *) | (CONSTR(((sp,n),u),[||]), APP(args,CASE(_,br,ci,env,stk))) - when red_set (info_flags info) fIOTA -> + when red_set (info_flags info) fMATCH -> let cargs = Array.sub args ci.ci_npar (Array.length args - ci.ci_npar) in cbv_stack_term info (stack_app cargs stk) env br.(n-1) (* constructor of arity 0 in a Case -> IOTA *) | (CONSTR(((_,n),u),[||]), CASE(_,br,_,env,stk)) - when red_set (info_flags info) fIOTA -> + when red_set (info_flags info) fMATCH -> cbv_stack_term info stk env br.(n-1) (* constructor in a Projection -> IOTA *) | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,pi,stk))) - when red_set (info_flags info) fIOTA && Projection.unfolded p -> + when red_set (info_flags info) fMATCH && Projection.unfolded p -> let arg = args.(pi.Declarations.proj_npars + pi.Declarations.proj_arg) in cbv_stack_value info env (strip_appl arg stk) diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index de37d1fc5e..87a03abbd9 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -9,7 +9,7 @@ open Names open Term open Environ -open Closure +open CClosure open Esubst (*********************************************************************** diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 55220f44c0..4f265e76c9 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Pp open Flags @@ -297,7 +297,7 @@ let lookup_path_to_sort_from env sigma s = let get_coercion_constructor env coe = let c, _ = - Reductionops.whd_betadeltaiota_stack env Evd.empty coe.coe_value + Reductionops.whd_all_stack env Evd.empty coe.coe_value in match kind_of_term c with | Construct (cstr,u) -> @@ -387,7 +387,7 @@ let add_coercion_in_graph (ic,source,target) = end; let is_ambig = match !ambig_paths with [] -> false | _ -> true in if is_ambig && is_verbose () then - Feedback.msg_warning (message_ambig !ambig_paths) + Feedback.msg_info (message_ambig !ambig_paths) type coercion = { coercion_type : coe_typ; diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 5c7adf1aa7..913e80f399 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -14,7 +14,7 @@ Corbineau, Feb 2008 *) (* Turned into an abstract compilation unit by Matthieu Sozeau, March 2006 *) -open Errors +open CErrors open Util open Names open Term @@ -63,7 +63,7 @@ let apply_coercion_args env evd check isproj argl funj = { uj_val = applist (j_val funj,argl); uj_type = typ } | h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *) - match kind_of_term (whd_betadeltaiota env evd typ) with + match kind_of_term (whd_all env evd typ) with | Prod (_,c1,c2) -> if check && not (e_cumul env evdref (Retyping.get_type_of env evd h) c1) then raise NoCoercion; @@ -90,8 +90,9 @@ let inh_pattern_coerce_to loc env pat ind1 ind2 = open Program -let make_existential loc ?(opaque = Evar_kinds.Define true) env evdref c = - Evarutil.e_new_evar env evdref ~src:(loc, Evar_kinds.QuestionMark opaque) c +let make_existential loc ?(opaque = not (get_proofs_transparency ())) env evdref c = + let src = (loc, Evar_kinds.QuestionMark (Evar_kinds.Define opaque)) in + Evarutil.e_new_evar env evdref ~src c let app_opt env evdref f t = whd_betaiota !evdref (app_opt f t) @@ -115,7 +116,7 @@ let disc_subset x = exception NoSubtacCoercion -let hnf env evd c = whd_betadeltaiota env evd c +let hnf env evd c = whd_all env evd c let hnf_nodelta env evd c = whd_betaiota evd c let lift_args n sign = @@ -191,7 +192,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) let term = co x in Typing.e_solve_evars env evdref term) in - if isEvar c || isEvar c' then + if isEvar c || isEvar c' || not (Program.is_program_generalized_coercion ()) then (* Second-order unification needed. *) raise NoSubtacCoercion; aux [] typ typ' 0 (fun x -> x) @@ -279,7 +280,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) let c1 = coerce_unify env a a' in let c2 = coerce_unify env b b' in match c1, c2 with - None, None -> None + | None, None -> None | _, _ -> Some (fun x -> @@ -369,11 +370,11 @@ let apply_coercion env sigma p hj typ_cl = (hj,typ_cl,sigma) p in evd, j with NoCoercion as e -> raise e - | e when Errors.noncritical e -> anomaly (Pp.str "apply_coercion") + | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion") (* Try to coerce to a funclass; raise NoCoercion if not possible *) let inh_app_fun_core env evd j = - let t = whd_betadeltaiota env evd j.uj_type in + let t = whd_all env evd j.uj_type in match kind_of_term t with | Prod (_,_,_) -> (evd,j) | Evar ev -> @@ -414,7 +415,7 @@ let inh_tosort_force loc env evd j = error_not_a_type_loc loc env evd j let inh_coerce_to_sort loc env evd j = - let typ = whd_betadeltaiota env evd j.uj_type in + let typ = whd_all env evd j.uj_type in match kind_of_term typ with | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s }) | Evar ev when not (is_defined evd (fst ev)) -> @@ -466,8 +467,8 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = try inh_coerce_to_fail env evd rigidonly v t c1 with NoCoercion -> match - kind_of_term (whd_betadeltaiota env evd t), - kind_of_term (whd_betadeltaiota env evd c1) + kind_of_term (whd_all env evd t), + kind_of_term (whd_all env evd c1) with | Prod (name,t1,t2), Prod (_,u1,u2) -> (* Conversion did not work, we may succeed with a coercion. *) @@ -513,7 +514,7 @@ let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj t = error_actual_type_loc loc env best_failed_evd cj t e else inh_conv_coerce_to_fail loc env evd' rigidonly (Some cj.uj_val) cj.uj_type t - with NoCoercionNoUnifier (best_failed_evd,e) -> + with NoCoercionNoUnifier (_evd,_error) -> error_actual_type_loc loc env best_failed_evd cj t e in let val' = match val' with Some v -> v | None -> assert(false) in diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 129725c6d2..886a982634 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -8,7 +8,7 @@ (*i*) open Pp -open Errors +open CErrors open Util open Names open Globnames @@ -49,12 +49,12 @@ type bound_ident_map = Id.t Id.Map.t exception PatternMatchingFailure -let warn_bound_meta name = - Feedback.msg_warning (str "Collision between bound variable " ++ pr_id name ++ - str " and a metavariable of same name.") +let warn_meta_collision = + CWarnings.create ~name:"meta-collision" ~category:"ltac" + (fun name -> + strbrk "Collision between bound variable " ++ pr_id name ++ + strbrk " and a metavariable of same name.") -let warn_bound_bound name = - Feedback.msg_warning (str "Collision between bound variables of name " ++ pr_id name) let constrain n (ids, m as x) (names, terms as subst) = try @@ -62,18 +62,19 @@ let constrain n (ids, m as x) (names, terms as subst) = if List.equal Id.equal ids ids' && eq_constr m m' then subst else raise PatternMatchingFailure with Not_found -> - let () = if Id.Map.mem n names then warn_bound_meta n in + let () = if Id.Map.mem n names then warn_meta_collision n in (names, Id.Map.add n x terms) let add_binders na1 na2 binding_vars (names, terms as subst) = match na1, na2 with | Name id1, Name id2 when Id.Set.mem id1 binding_vars -> if Id.Map.mem id1 names then - let () = warn_bound_bound id1 in + let () = Glob_ops.warn_variable_collision id1 in (names, terms) else let names = Id.Map.add id1 id2 names in - let () = if Id.Map.mem id1 terms then warn_bound_meta id1 in + let () = if Id.Map.mem id1 terms then + warn_meta_collision id1 in (names, terms) | _ -> subst diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 86921c49b0..85125a502e 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Term @@ -323,7 +323,7 @@ let is_nondep_branch c l = (* FIXME: do better using tags from l *) let sign,ccl = decompose_lam_n_decls (List.length l) c in noccur_between 1 (Context.Rel.length sign) ccl - with e when Errors.noncritical e -> (* Not eta-expanded or not reduced *) + with e when CErrors.noncritical e -> (* Not eta-expanded or not reduced *) false let extract_nondep_branches test c b l = @@ -620,7 +620,7 @@ and share_names flags n l avoid env sigma c t = share_names flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c' (* If built with the f/n notation: we renounce to share names *) | _ -> - if n>0 then Feedback.msg_warning (strbrk "Detyping.detype: cannot factorize fix enough"); + if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough"); let c = detype flags avoid env sigma c in let t = detype flags avoid env sigma t in (List.rev l,c,t) @@ -631,7 +631,7 @@ and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl = let mat = build_tree Anonymous (snd flags) (avoid,env) ci bl in List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype flags avoid env sigma c)) mat - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> Array.to_list (Array.map3 (detype_eqn flags avoid env sigma) constructs consnargsl bl) @@ -689,7 +689,7 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = | BLetIn -> let c = detype (lax,false) avoid env sigma (Option.get body) in (* Heuristic: we display the type if in Prop *) - let s = Retyping.get_sort_family_of (snd env) sigma ty in + let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in let c = if s != InProp then c else GCast (dl, c, CastConv (detype (lax,false) avoid env sigma ty)) in GLetIn (dl, na', c, r) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 912fd198b6..9fd55a488e 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -6,12 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Term open Vars -open Closure +open CClosure open Reduction open Reductionops open Termops @@ -42,12 +42,7 @@ let _ = Goptions.declare_bool_option { let unfold_projection env evd ts p c = let cst = Projection.constant p in if is_transparent_constant ts cst then - let c' = Some (mkProj (Projection.make cst true, c)) in - match ReductionBehaviour.get (Globnames.ConstRef cst) with - | None -> c' - | Some (recargs, nargs, flags) -> - if (List.mem `ReductionNeverUnfold flags) then None - else c' + Some (mkProj (Projection.make cst true, c)) else None let eval_flexible_term ts env evd c = @@ -102,19 +97,19 @@ let position_problem l2r = function | CONV -> None | CUMUL -> Some l2r -let occur_rigidly ev evd t = +let occur_rigidly (evk,_ as ev) evd t = let rec aux t = match kind_of_term (whd_evar evd t) with | App (f, c) -> if aux f then Array.exists aux c else false | Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ -> true | Proj (p, c) -> not (aux c) - | Evar (ev',_) -> if Evar.equal ev ev' then raise Occur else false + | Evar (evk',_) -> if Evar.equal evk evk' then raise Occur else false | Cast (p, _, _) -> aux p | Lambda _ | LetIn _ -> false | Const _ -> false | Prod (_, b, t) -> ignore(aux b || aux t); true | Rel _ | Var _ -> false - | Case _ -> false + | Case (_,_,c,_) -> if eq_constr (mkEvar ev) c then raise Occur else false in try ignore(aux t); false with Occur -> true (* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose @@ -314,7 +309,7 @@ let exact_ise_stack2 env evd f sk1 sk2 = if Reductionops.Stack.compare_shape sk1 sk2 then ise_stack2 evd (List.rev sk1) (List.rev sk2) else UnifFailure (evd, (* Dummy *) NotSameHead) - + let rec evar_conv_x ts env evd pbty term1 term2 = let term1 = whd_head_evar evd term1 in let term2 = whd_head_evar evd term2 in @@ -432,7 +427,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty else quick_fail i and delta i = switch (evar_eqappr_x ts env i pbty) (apprF,cstsF) - (whd_betaiota_deltazeta_for_iota_state (fst ts) env i cstsM (vM,skM)) + (whd_betaiota_deltazeta_for_iota_state + (fst ts) env i cstsM (vM,skM)) in let default i = ise_try i [f1; consume apprF apprM; delta] in @@ -449,7 +445,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty try let termM' = Retyping.expand_projection env evd p c [] in let apprM', cstsM' = - whd_betaiota_deltazeta_for_iota_state (fst ts) env evd cstsM (termM',skM) + whd_betaiota_deltazeta_for_iota_state + (fst ts) env evd cstsM (termM',skM) in let delta' i = switch (evar_eqappr_x ts env i pbty) (apprF,cstsF) (apprM',cstsM') @@ -481,7 +478,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [eta;(* Postpone the use of an heuristic *) (fun i -> - if not (occur_rigidly (fst ev) i tR) then + if not (occur_rigidly ev i tR) then let i,tF = if isRel tR || isVar tR then (* Optimization so as to generate candidates *) @@ -766,7 +763,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty in Success evd' with Univ.UniverseInconsistency p -> UnifFailure (evd,UnifUnivInconsistency p) - | e when Errors.noncritical e -> UnifFailure (evd,NotSameHead)) + | e when CErrors.noncritical e -> UnifFailure (evd,NotSameHead)) | Prod (n1,c1,c'1), Prod (n2,c2,c'2) when app_empty -> ise_and evd @@ -1084,7 +1081,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = match evar_conv_x ts env_evar evd CUMUL idty evty with | UnifFailure _ -> error "Cannot find an instance" | Success evd -> - match reconsider_conv_pbs (evar_conv_x ts) evd with + match reconsider_unif_constraints (evar_conv_x ts) evd with | UnifFailure _ -> error "Cannot find an instance" | Success evd -> evd @@ -1150,7 +1147,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in Success (solve_refl ~can_drop:true f env evd (position_problem true pbty) evk1 args1 args2) - | Evar ev1, Evar ev2 -> + | Evar ev1, Evar ev2 when app_empty -> Success (solve_evar_evar ~force:true (evar_define (evar_conv_x ts) ~choose:true) (evar_conv_x ts) env evd (position_problem true pbty) ev1 ev2) @@ -1178,9 +1175,14 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = (* Some head evar have been instantiated, or unknown kind of problem *) evar_conv_x ts env evd pbty t1 t2 +let error_cannot_unify env evd pb ?reason t1 t2 = + Pretype_errors.error_cannot_unify_loc + (loc_of_conv_pb evd pb) env + evd ?reason (t1, t2) + let check_problems_are_solved env evd = match snd (extract_all_conv_pbs evd) with - | (pbty,env,t1,t2)::_ -> Pretype_errors.error_cannot_unify env evd (t1, t2) + | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb t1 t2 | _ -> () let max_undefined_with_candidates evd = @@ -1211,7 +1213,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd = let conv_algo = evar_conv_x ts in let evd = check_evar_instance evd evk a conv_algo in let evd = Evd.define evk a evd in - match reconsider_conv_pbs conv_algo evd with + match reconsider_unif_constraints conv_algo evd with | Success evd -> solve_unconstrained_evars_with_candidates ts evd | UnifFailure _ -> aux l with @@ -1225,16 +1227,16 @@ let rec solve_unconstrained_evars_with_candidates ts evd = let solve_unconstrained_impossible_cases env evd = Evd.fold_undefined (fun evk ev_info evd' -> match ev_info.evar_source with - | _,Evar_kinds.ImpossibleCase -> + | loc,Evar_kinds.ImpossibleCase -> let j, ctx = coq_unit_judge () in - let evd' = Evd.merge_context_set Evd.univ_flexible_alg evd' ctx in + let evd' = Evd.merge_context_set Evd.univ_flexible_alg ~loc evd' ctx in let ty = j_type j in let conv_algo = evar_conv_x full_transparent_state in let evd' = check_evar_instance evd' evk ty conv_algo in Evd.define evk ty evd' | _ -> evd') evd evd -let consider_remaining_unif_problems env +let solve_unif_constraints_with_heuristics env ?(ts=Conv_oracle.get_transp_state (Environ.oracle env)) evd = let evd = solve_unconstrained_evars_with_candidates ts evd in let rec aux evd pbs progress stuck = @@ -1249,23 +1251,23 @@ let consider_remaining_unif_problems env aux evd pbs progress (pb :: stuck) end | UnifFailure (evd,reason) -> - Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb) - env evd ~reason (t1, t2)) + error_cannot_unify env evd pb ~reason t1 t2) | _ -> if progress then aux evd stuck false [] else match stuck with | [] -> (* We're finished *) evd | (pbty,env,t1,t2 as pb) :: _ -> - (* There remains stuck problems *) - Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb) - env evd (t1, t2) + (* There remains stuck problems *) + error_cannot_unify env evd pb t1 t2 in let (evd,pbs) = extract_all_conv_pbs evd in let heuristic_solved_evd = aux evd pbs false [] in check_problems_are_solved env heuristic_solved_evd; solve_unconstrained_impossible_cases env heuristic_solved_evd +let consider_remaining_unif_problems = solve_unif_constraints_with_heuristics + (* Main entry points *) exception UnableToUnify of evar_map * unification_error diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 14947c8927..2231e5bc30 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -33,7 +33,10 @@ val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr - (** Try heuristics to solve pending unification problems and to solve evars with candidates *) +val solve_unif_constraints_with_heuristics : env -> ?ts:transparent_state -> evar_map -> evar_map + val consider_remaining_unif_problems : env -> ?ts:transparent_state -> evar_map -> evar_map +(** @deprecated Alias for [solve_unif_constraints_with_heuristics] *) (** Check all pending unification problems are solved and raise an error otherwise *) diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index d349cf8216..f9ab75cea9 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -78,7 +78,7 @@ let define_pure_evar_as_product evd evk = let evi = Evd.find_undefined evd evk in let evenv = evar_env evi in let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in - let concl = Reductionops.whd_betadeltaiota evenv evd evi.evar_concl in + let concl = Reductionops.whd_all evenv evd evi.evar_concl in let s = destSort concl in let evd1,(dom,u1) = let evd = Sigma.Unsafe.of_evar_map evd in @@ -131,7 +131,7 @@ let define_pure_evar_as_lambda env evd evk = let open Context.Named.Declaration in let evi = Evd.find_undefined evd evk in let evenv = evar_env evi in - let typ = Reductionops.whd_betadeltaiota evenv evd (evar_concl evi) in + let typ = Reductionops.whd_all evenv evd (evar_concl evi) in let evd1,(na,dom,rng) = match kind_of_term typ with | Prod (na,dom,rng) -> (evd,(na,dom,rng)) | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ @@ -169,7 +169,7 @@ let define_evar_as_sort env evd (ev,args) = let evd, u = new_univ_variable univ_rigid evd in let evi = Evd.find_undefined evd ev in let s = Type u in - let concl = Reductionops.whd_betadeltaiota (evar_env evi) evd evi.evar_concl in + let concl = Reductionops.whd_all (evar_env evi) evd evi.evar_concl in let sort = destSort concl in let evd' = Evd.define ev (mkSort s) evd in Evd.set_leq_sort env evd' (Type (Univ.super u)) sort, s @@ -181,10 +181,10 @@ let define_evar_as_sort env evd (ev,args) = let split_tycon loc env evd tycon = let rec real_split evd c = - let t = Reductionops.whd_betadeltaiota env evd c in + let t = Reductionops.whd_all env evd c in match kind_of_term t with | Prod (na,dom,rng) -> evd, (na, dom, rng) - | Evar ev (* ev is undefined because of whd_betadeltaiota *) -> + | Evar ev (* ev is undefined because of whd_all *) -> let (evd',prod) = define_evar_as_product evd ev in let (_,dom,rng) = destProd prod in evd',(Anonymous, dom, rng) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 455a7dbd69..f0aa9b564f 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -7,7 +7,7 @@ (************************************************************************) open Util -open Errors +open CErrors open Names open Term open Vars @@ -47,7 +47,8 @@ let refresh_level evd s = | None -> true | Some l -> not (Evd.is_flexible_level evd l) -let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) pbty env evd t = +let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) + pbty env evd t = let evdref = ref evd in let modified = ref false in let rec refresh status dir t = @@ -62,6 +63,10 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) pbty env evd t = else set_leq_sort env !evdref s s' in modified := true; evdref := evd; mkSort s' + | Sort (Prop Pos as s) when refreshset && not dir -> + let s' = evd_comb0 (new_sort_variable status) evdref in + let evd = set_leq_sort env !evdref s s' in + modified := true; evdref := evd; mkSort s' | Prod (na,u,v) -> mkProd (na,u,refresh status dir v) | _ -> t @@ -140,7 +145,7 @@ let recheck_applications conv_algo env evdref t = let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref x) args in let rec aux i ty = if i < Array.length argsty then - match kind_of_term (whd_betadeltaiota env !evdref ty) with + match kind_of_term (whd_all env !evdref ty) with | Prod (na, dom, codom) -> (match conv_algo env !evdref Reduction.CUMUL argsty.(i) dom with | Success evd -> evdref := evd; @@ -212,30 +217,29 @@ let restrict_instance evd evk filter argsv = open Context.Rel.Declaration let noccur_evar env evd evk c = let cache = ref Int.Set.empty (* cache for let-ins *) in - let rec occur_rec (k, env as acc) c = + let rec occur_rec check_types (k, env as acc) c = match kind_of_term c with | Evar (evk',args' as ev') -> (match safe_evar_value evd ev' with - | Some c -> occur_rec acc c + | Some c -> occur_rec check_types acc c | None -> if Evar.equal evk evk' then raise Occur - else Array.iter (occur_rec acc) args') + else (if check_types then + occur_rec false acc (existential_type evd ev'); + Array.iter (occur_rec check_types acc) args')) | Rel i when i > k -> - if not (Int.Set.mem (i-k) !cache) then - (match Environ.lookup_rel i env with - | LocalAssum _ -> () - | LocalDef (_,b,_) -> cache := Int.Set.add (i-k) !cache; occur_rec acc (lift i b)) - | Proj (p,c) -> - let c = - try Retyping.expand_projection env evd p c [] - with Retyping.RetypeError _ -> - (* Can happen when called from w_unify which doesn't assign evars/metas - eagerly enough *) c - in occur_rec acc c + if not (Int.Set.mem (i-k) !cache) then + let decl = Environ.lookup_rel i env in + if check_types then + (cache := Int.Set.add (i-k) !cache; occur_rec false acc (lift i (get_type decl))); + (match decl with + | LocalAssum _ -> () + | LocalDef (_,b,_) -> cache := Int.Set.add (i-k) !cache; occur_rec false acc (lift i b)) + | Proj (p,c) -> occur_rec true acc c | _ -> iter_constr_with_full_binders (fun rd (k,env) -> (succ k, push_rel rd env)) - occur_rec acc c + (occur_rec check_types) acc c in - try occur_rec (0,env) c; true with Occur -> false + try occur_rec false (0,env) c; true with Occur -> false (***************************************) (* Managing chains of local definitons *) @@ -520,7 +524,7 @@ let solve_pattern_eqn env l c = l c in (* Warning: we may miss some opportunity to eta-reduce more since c' is not in normal form *) - whd_eta c' + shrink_eta c' (*****************************************) (* Refining/solving unification problems *) @@ -609,7 +613,13 @@ let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_si * substitution u1..uq. *) +exception MorePreciseOccurCheckNeeeded + let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = + if Evd.is_defined evd evk1 then + (* Some circularity somewhere (see e.g. #3209) *) + raise MorePreciseOccurCheckNeeeded; + let (evk1,args1) = destEvar (whd_evar evd (mkEvar (evk1,args1))) in let evi1 = Evd.find_undefined evd evk1 in let env1,rel_sign = env_rel_context_chop k env in let sign1 = evar_hyps evi1 in @@ -797,7 +807,7 @@ let rec do_projection_effects define_fun env ty evd = function let evd = Evd.define evk (mkVar id) evd in (* TODO: simplify constraints involving evk *) let evd = do_projection_effects define_fun env ty evd p in - let ty = whd_betadeltaiota env evd (Lazy.force ty) in + let ty = whd_all env evd (Lazy.force ty) in if not (isSort ty) then (* Don't try to instantiate if a sort because if evar_concl is an evar it may commit to a univ level which is not the right @@ -1460,7 +1470,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1) imitate envk t in t::l - with e when Errors.noncritical e -> l in + with e when CErrors.noncritical e -> l in (match candidates with | [x] -> x | _ -> @@ -1549,11 +1559,13 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = postpone_non_unique_projection env evd pbty ev sols rhs | NotEnoughInformationEvarEvar t -> add_conv_oriented_pb (pbty,env,mkEvar ev,t) evd + | MorePreciseOccurCheckNeeeded -> + add_conv_oriented_pb (pbty,env,mkEvar ev,rhs) evd | NotInvertibleUsingOurAlgorithm _ | MetaOccurInBodyInternal as e -> raise e | OccurCheckIn (evd,rhs) -> (* last chance: rhs actually reduces to ev *) - let c = whd_betadeltaiota env evd rhs in + let c = whd_all env evd rhs in match kind_of_term c with | Evar (evk',argsv2) when Evar.equal evk evk' -> solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma c c') @@ -1591,7 +1603,7 @@ let status_changed lev (pbty,_,t1,t2) = (try Evar.Set.mem (head_evar t1) lev with NoHeadEvar -> false) || (try Evar.Set.mem (head_evar t2) lev with NoHeadEvar -> false) -let reconsider_conv_pbs conv_algo evd = +let reconsider_unif_constraints conv_algo evd = let (evd,pbs) = extract_changed_conv_pbs evd status_changed in List.fold_left (fun p (pbty,env,t1,t2 as x) -> @@ -1604,6 +1616,8 @@ let reconsider_conv_pbs conv_algo evd = (Success evd) pbs +let reconsider_conv_pbs = reconsider_unif_constraints + (* Tries to solve problem t1 = t2. * Precondition: t1 is an uninstantiated evar * Returns an optional list of evars that were instantiated, or None @@ -1614,7 +1628,7 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1) try let t2 = whd_betaiota evd t2 in (* includes whd_evar *) let evd = evar_define conv_algo ~choose env evd pbty ev1 t2 in - reconsider_conv_pbs conv_algo evd + reconsider_unif_constraints conv_algo evd with | NotInvertibleUsingOurAlgorithm t -> UnifFailure (evd,NotClean (ev1,env,t)) diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 918ba12f0f..b6bdc07889 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -34,8 +34,12 @@ type conv_fun_bool = val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> bool option -> existential -> constr -> evar_map -val refresh_universes : ?status:Evd.rigid -> - ?onlyalg:bool (* Only algebraic universes *) -> +val refresh_universes : + ?status:Evd.rigid -> + ?onlyalg:bool (* Only algebraic universes *) -> + ?refreshset:bool -> + (* Also refresh Prop and Set universes, so that the returned type can be any supertype + of the original type *) bool option (* direction: true for levels lower than the existing levels *) -> env -> evar_map -> types -> evar_map * types @@ -50,7 +54,10 @@ val solve_evar_evar : ?force:bool -> val solve_simple_eqn : conv_fun -> ?choose:bool -> env -> evar_map -> bool option * existential * constr -> unification_result +val reconsider_unif_constraints : conv_fun -> evar_map -> unification_result + val reconsider_conv_pbs : conv_fun -> evar_map -> unification_result +(** @deprecated Alias for [reconsider_unif_constraints] *) val is_unification_pattern_evar : env -> evar_map -> existential -> constr list -> constr -> constr list option diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index df1fc20f1d..4caa1e9927 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -8,7 +8,7 @@ open Pp open Util -open Errors +open CErrors open Names open Locus open Term diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 04100c8a73..51660818f4 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -334,10 +334,14 @@ let glob_visible_short_qualid c = fold_glob_constr aux acc c in aux [] c +let warn_variable_collision = + let open Pp in + CWarnings.create ~name:"variable-collision" ~category:"ltac" + (fun name -> + strbrk "Collision between bound variables of name " ++ pr_id name) + let add_and_check_ident id set = - if Id.Set.mem id set then - Feedback.msg_warning - Pp.(str "Collision between bound variables of name " ++ Id.print id); + if Id.Set.mem id set then warn_variable_collision id; Id.Set.add id set let bound_glob_vars = @@ -466,6 +470,78 @@ let loc_of_glob_constr = function | GCast (loc,_,_) -> loc (**********************************************************************) +(* Alpha-renaming *) + +let collide_id l id = List.exists (fun (id',id'') -> Id.equal id id' || Id.equal id id'') l +let test_id l id = if collide_id l id then raise Not_found +let test_na l na = name_iter (test_id l) na + +let update_subst na l = + let in_range id l = List.exists (fun (_,id') -> Id.equal id id') l in + let l' = name_fold Id.List.remove_assoc na l in + name_fold + (fun id _ -> + if in_range id l' then + let id' = Namegen.next_ident_away_from id (fun id' -> in_range id' l') in + Name id', (id,id')::l + else na,l) + na (na,l) + +exception UnsoundRenaming + +let rename_var l id = + try + let id' = Id.List.assoc id l in + (* Check that no other earlier binding hide the one found *) + let _,(id'',_) = List.extract_first (fun (_,id) -> Id.equal id id') l in + if Id.equal id id'' then id' else raise UnsoundRenaming + with Not_found -> + if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming + else id + +let rec rename_glob_vars l = function + | GVar (loc,id) as r -> + let id' = rename_var l id in + if id == id' then r else GVar (loc,id') + | GRef (_,VarRef id,_) as r -> + if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming + else r + | GProd (loc,na,bk,t,c) -> + let na',l' = update_subst na l in + GProd (loc,na,bk,rename_glob_vars l t,rename_glob_vars l' c) + | GLambda (loc,na,bk,t,c) -> + let na',l' = update_subst na l in + GLambda (loc,na',bk,rename_glob_vars l t,rename_glob_vars l' c) + | GLetIn (loc,na,b,c) -> + let na',l' = update_subst na l in + GLetIn (loc,na',rename_glob_vars l b,rename_glob_vars l' c) + (* Lazy strategy: we fail if a collision with renaming occurs, rather than renaming further *) + | GCases (loc,ci,po,tomatchl,cls) -> + let test_pred_pat (na,ino) = + test_na l na; Option.iter (fun (_,_,nal) -> List.iter (test_na l) nal) ino in + let test_clause idl = List.iter (test_id l) idl in + let po = Option.map (rename_glob_vars l) po in + let tomatchl = Util.List.map_left (fun (tm,x) -> test_pred_pat x; (rename_glob_vars l tm,x)) tomatchl in + let cls = Util.List.map_left (fun (loc,idl,p,c) -> test_clause idl; (loc,idl,p,rename_glob_vars l c)) cls in + GCases (loc,ci,po,tomatchl,cls) + | GLetTuple (loc,nal,(na,po),c,b) -> + List.iter (test_na l) (na::nal); + GLetTuple (loc,nal,(na,Option.map (rename_glob_vars l) po), + rename_glob_vars l c,rename_glob_vars l b) + | GIf (loc,c,(na,po),b1,b2) -> + test_na l na; + GIf (loc,rename_glob_vars l c,(na,Option.map (rename_glob_vars l) po), + rename_glob_vars l b1,rename_glob_vars l b2) + | GRec (loc,k,idl,decls,bs,ts) -> + Array.iter (test_id l) idl; + GRec (loc,k,idl, + Array.map (List.map (fun (na,k,bbd,bty) -> + test_na l na; (na,k,Option.map (rename_glob_vars l) bbd,rename_glob_vars l bty))) decls, + Array.map (rename_glob_vars l) bs, + Array.map (rename_glob_vars l) ts) + | r -> map_glob_constr (rename_glob_vars l) r + +(**********************************************************************) (* Conversion from glob_constr to cases pattern, if possible *) let rec cases_pattern_of_glob_constr na = function diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index e0a2de0326..55e6b6533f 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -34,6 +34,8 @@ val map_glob_constr : val map_glob_constr_left_to_right : (glob_constr -> glob_constr) -> glob_constr -> glob_constr +val warn_variable_collision : ?loc:Loc.t -> Id.t -> unit + val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit val occur_glob_constr : Id.t -> glob_constr -> bool @@ -42,6 +44,16 @@ val bound_glob_vars : glob_constr -> Id.Set.t val loc_of_glob_constr : glob_constr -> Loc.t val glob_visible_short_qualid : glob_constr -> Id.t list +(* Renaming free variables using a renaming map; fails with + [UnsoundRenaming] if applying the renaming would introduce + collision, as in, e.g., renaming [P x y] using substitution [(x,y)]; + inner alpha-conversion done only for forall, fun, let but + not for cases and fix *) + +exception UnsoundRenaming +val rename_var : (Id.t * Id.t) list -> Id.t -> Id.t +val rename_glob_vars : (Id.t * Id.t) list -> glob_constr -> glob_constr + (** [map_pattern_binders f m c] applies [f] to all the binding names in a pattern-matching expression ({!Glob_term.GCases}) represented here by its relevant components [m] and [c]. It is used to diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 5d36fc78ef..39aeb41f77 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -11,7 +11,7 @@ (* This file builds various inductive schemes *) open Pp -open Errors +open CErrors open Util open Names open Libnames @@ -36,12 +36,14 @@ type dep_flag = bool type recursion_scheme_error = | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive | NotMutualInScheme of inductive * inductive + | NotAllowedDependentAnalysis of (*isrec:*) bool * inductive exception RecursionSchemeError of recursion_scheme_error let make_prod_dep dep env = if dep then mkProd_name env else mkProd let mkLambda_string s t c = mkLambda (Name (Id.of_string s), t, c) + (*******************************************) (* Building curryfied elimination *) (*******************************************) @@ -151,7 +153,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = let nparams = List.length vargs in let process_pos env depK pk = let rec prec env i sign p = - let p',largs = whd_betadeltaiota_nolet_stack env sigma p in + let p',largs = whd_allnolet_stack env sigma p in match kind_of_term p' with | Prod (n,t,c) -> let d = LocalAssum (n,t) in @@ -168,7 +170,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = else base | _ -> - let t' = whd_betadeltaiota env sigma p in + let t' = whd_all env sigma p in if Term.eq_constr p' t' then assert false else prec env i sign t' in @@ -183,9 +185,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = | ra::rest -> (match dest_recarg ra with | Mrec (_,j) when is_rec -> (depPvect.(j),rest) - | Imbr _ -> - Feedback.msg_warning (strbrk "Ignoring recursive call"); - (None,rest) + | Imbr _ -> (None,rest) | _ -> (None, rest)) in (match optionpos with @@ -229,7 +229,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = let process_pos env fk = let rec prec env i hyps p = - let p',largs = whd_betadeltaiota_nolet_stack env sigma p in + let p',largs = whd_allnolet_stack env sigma p in match kind_of_term p' with | Prod (n,t,c) -> let d = LocalAssum (n,t) in @@ -242,7 +242,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = and arg = appvect (mkRel (i+1), Context.Rel.to_extended_vect 0 hyps) in applist(lift i fk,realargs@[arg]) | _ -> - let t' = whd_betadeltaiota env sigma p in + let t' = whd_all env sigma p in if Term.eq_constr t' p' then assert false else prec env i hyps t' in @@ -377,27 +377,9 @@ let mis_make_indrec env sigma listdepkind mib u = (Anonymous,depind',concl)) arsign' in - let obj = - let projs = get_projections env indf in - match projs with - | None -> (mkCase (ci, pred, - mkRel 1, - branches)) - | Some ps -> - let branch = branches.(0) in - let ctx, br = decompose_lam_assum branch in - let n, subst = - List.fold_right (fun decl (i, subst) -> - match decl with - | LocalAssum (na,t) -> - let t = mkProj (Projection.make ps.(i) true, mkRel 1) in - i + 1, t :: subst - | LocalDef (na,b,t) -> - i, mkRel 0 :: subst) - ctx (0, []) - in - let term = substl subst br in - term + let obj = + Inductiveops.make_case_or_project env indf ci pred + (mkRel 1) branches in it_mkLambda_or_LetIn_name env obj (Termops.lift_rel_context nrec deparsign) @@ -485,6 +467,8 @@ let mis_make_indrec env sigma listdepkind mib u = let build_case_analysis_scheme env sigma pity dep kind = let (mib,mip) = lookup_mind_specif env (fst pity) in + if dep && not (Inductiveops.has_dependent_elim mib) then + raise (RecursionSchemeError (NotAllowedDependentAnalysis (false, fst pity))); mis_make_case_com dep env sigma pity (mib,mip) kind let is_in_prop mip = @@ -494,7 +478,7 @@ let is_in_prop mip = let build_case_analysis_scheme_default env sigma pity kind = let (mib,mip) = lookup_mind_specif env (fst pity) in - let dep = not (is_in_prop mip) in + let dep = not (is_in_prop mip || not (Inductiveops.has_dependent_elim mib)) in mis_make_case_com dep env sigma pity (mib,mip) kind (**********************************************************************) @@ -555,6 +539,8 @@ let check_arities env listdepkind = let build_mutual_induction_scheme env sigma = function | ((mind,u),dep,s)::lrecspec -> let (mib,mip) = lookup_mind_specif env mind in + if dep && not (Inductiveops.has_dependent_elim mib) then + raise (RecursionSchemeError (NotAllowedDependentAnalysis (true, mind))); let (sp,tyi) = mind in let listdepkind = ((mind,u),mib,mip,dep,s):: @@ -574,6 +560,8 @@ let build_mutual_induction_scheme env sigma = function let build_induction_scheme env sigma pind dep kind = let (mib,mip) = lookup_mind_specif env (fst pind) in + if dep && not (Inductiveops.has_dependent_elim mib) then + raise (RecursionSchemeError (NotAllowedDependentAnalysis (true, fst pind))); let sigma, l = mis_make_indrec env sigma [(pind,mib,mip,dep,kind)] mib (snd pind) in sigma, List.hd l diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index f0736d2dda..192b64a5ed 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -16,6 +16,7 @@ open Evd type recursion_scheme_error = | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive | NotMutualInScheme of inductive * inductive + | NotAllowedDependentAnalysis of (*isrec:*) bool * inductive exception RecursionSchemeError of recursion_scheme_error @@ -28,13 +29,15 @@ type dep_flag = bool val build_case_analysis_scheme : env -> 'r Sigma.t -> pinductive -> dep_flag -> sorts_family -> (constr, 'r) Sigma.sigma -(** Build a dependent case elimination predicate unless type is in Prop *) +(** Build a dependent case elimination predicate unless type is in Prop + or is a recursive record with primitive projections. *) val build_case_analysis_scheme_default : env -> 'r Sigma.t -> pinductive -> sorts_family -> (constr, 'r) Sigma.sigma (** Builds a recursive induction scheme (Peano-induction style) in the same - sort family as the inductive family; it is dependent if not in Prop *) + sort family as the inductive family; it is dependent if not in Prop + or a recursive record with primitive projections. *) val build_induction_scheme : env -> evar_map -> pinductive -> dep_flag -> sorts_family -> evar_map * constr diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 403dcfd1a3..214e19fecf 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Univ @@ -269,6 +269,11 @@ let projection_nparams_env env p = let projection_nparams p = projection_nparams_env (Global.env ()) p +let has_dependent_elim mib = + match mib.mind_record with + | Some (Some _) -> mib.mind_finite == Decl_kinds.BiFinite + | _ -> true + (* Annotation for cases *) let make_case_info env ind style = let (mib,mip) = Inductive.lookup_mind_specif env ind in @@ -338,6 +343,35 @@ let get_projections env (ind,params) = | Some (Some (id, projs, pbs)) -> Some projs | _ -> None +let make_case_or_project env indf ci pred c branches = + let projs = get_projections env indf in + match projs with + | None -> (mkCase (ci, pred, c, branches)) + | Some ps -> + assert(Array.length branches == 1); + let () = + let _, _, t = destLambda pred in + let (ind, _), _ = dest_ind_family indf in + let mib, _ = Inductive.lookup_mind_specif env ind in + if (* dependent *) not (noccurn 1 t) && + not (has_dependent_elim mib) then + errorlabstrm "make_case_or_project" + Pp.(str"Dependent case analysis not allowed" ++ + str" on inductive type " ++ Names.MutInd.print (fst ind)) + in + let branch = branches.(0) in + let ctx, br = decompose_lam_n_assum (Array.length ps) branch in + let n, subst = + List.fold_right + (fun decl (i, subst) -> + match decl with + | LocalAssum (na, t) -> + let t = mkProj (Projection.make ps.(i) true, c) in + (i + 1, t :: subst) + | LocalDef (na, b, t) -> (i, substl subst b :: subst)) + ctx (0, []) + in substl subst br + (* substitution in a signature *) let substnl_rel_context subst n sign = @@ -417,7 +451,7 @@ let extract_mrectype t = | _ -> raise Not_found let find_mrectype_vect env sigma c = - let (t, l) = decompose_appvect (whd_betadeltaiota env sigma c) in + let (t, l) = decompose_appvect (whd_all env sigma c) in match kind_of_term t with | Ind ind -> (ind, l) | _ -> raise Not_found @@ -426,7 +460,7 @@ let find_mrectype env sigma c = let (ind, v) = find_mrectype_vect env sigma c in (ind, Array.to_list v) let find_rectype env sigma c = - let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in + let (t, l) = decompose_app (whd_all env sigma c) in match kind_of_term t with | Ind (ind,u as indu) -> let (mib,mip) = Inductive.lookup_mind_specif env ind in @@ -436,7 +470,7 @@ let find_rectype env sigma c = | _ -> raise Not_found let find_inductive env sigma c = - let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in + let (t, l) = decompose_app (whd_all env sigma c) in match kind_of_term t with | Ind ind when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> Decl_kinds.CoFinite -> @@ -444,7 +478,7 @@ let find_inductive env sigma c = | _ -> raise Not_found let find_coinductive env sigma c = - let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in + let (t, l) = decompose_app (whd_all env sigma c) in match kind_of_term t with | Ind ind when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == Decl_kinds.CoFinite -> @@ -458,7 +492,7 @@ let find_coinductive env sigma c = let is_predicate_explicitly_dep env pred arsign = let rec srec env pval arsign = - let pv' = whd_betadeltaiota env Evd.empty pval in + let pv' = whd_all env Evd.empty pval in match kind_of_term pv', arsign with | Lambda (na,t,b), (LocalAssum _)::arsign -> srec (push_rel_assum (na,t) env) b arsign diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index d25f8a8378..7bd616591f 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -122,11 +122,16 @@ val inductive_has_local_defs : inductive -> bool val allowed_sorts : env -> inductive -> sorts_family list +(** (Co)Inductive records with primitive projections do not have eta-conversion, + hence no dependent elimination. *) +val has_dependent_elim : mutual_inductive_body -> bool + (** Primitive projections *) val projection_nparams : projection -> int val projection_nparams_env : env -> projection -> int val type_of_projection_knowing_arg : env -> evar_map -> Projection.t -> - constr -> types -> types + constr -> types -> types + (** Extract information from an inductive family *) @@ -175,6 +180,14 @@ val type_case_branches_with_names : (** Annotation for cases *) val make_case_info : env -> inductive -> case_style -> case_info +(** Make a case or substitute projections if the inductive type is a record + with primitive projections. + Fail with an error if the elimination is dependent while the + inductive type does not allow dependent elimination. *) +val make_case_or_project : + env -> inductive_family -> case_info -> + (* pred *) constr -> (* term *) constr -> (* branches *) constr array -> constr + (*i Compatibility val make_default_case_info : env -> case_style -> inductive -> case_info i*) diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index d89aeccd8c..e4fbf8d542 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -50,9 +50,9 @@ let is_nowhere = function let simple_clause_of enum_hyps cl = let error_occurrences () = - Errors.error "This tactic does not support occurrences selection" in + CErrors.error "This tactic does not support occurrences selection" in let error_body_selection () = - Errors.error "This tactic does not support body selection" in + CErrors.error "This tactic does not support body selection" in let hyps = match cl.onhyps with | None -> @@ -84,7 +84,7 @@ let concrete_clause_of enum_hyps cl = (** Miscellaneous functions *) let out_arg = function - | Misctypes.ArgVar _ -> Errors.anomaly (Pp.str "Unevaluated or_var variable") + | Misctypes.ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable") | Misctypes.ArgArg x -> x let occurrences_of_hyp id cls = diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 2a5e999651..0dd64697c6 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Pp -open Errors +open CErrors open Term open Vars open Environ @@ -35,13 +35,13 @@ let invert_tag cst tag reloc_tbl = with Find_at j -> (j+1) let decompose_prod env t = - let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in + let (name,dom,codom as res) = destProd (whd_all env t) in match name with | Anonymous -> (Name (id_of_string "x"),dom,codom) | _ -> res let app_type env c = - let t = whd_betadeltaiota env c in + let t = whd_all env c in try destApp t with DestKO -> (t,[||]) @@ -178,7 +178,7 @@ let rec nf_val env v typ = let name,dom,codom = try decompose_prod env typ with DestKO -> - Errors.anomaly + CErrors.anomaly (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") in let env = push_rel (LocalAssum (name,dom)) env in @@ -224,7 +224,7 @@ and nf_args env accu t = let _,dom,codom = try decompose_prod env t with DestKO -> - Errors.anomaly + CErrors.anomaly (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") in let c = nf_val env arg dom in @@ -241,7 +241,7 @@ and nf_bargs env b t = let _,dom,codom = try decompose_prod env !t with DestKO -> - Errors.anomaly + CErrors.anomaly (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") in let c = nf_val env (block_field b i) dom in @@ -289,7 +289,7 @@ and nf_atom_type env atom = let pT = hnf_prod_applist env (Inductiveops.type_of_inductive env ind) (Array.to_list params) in - let pT = whd_betadeltaiota env pT in + let pT = whd_all env pT in let dep, p = nf_predicate env ind mip params p pT in (* Calcul du type des branches *) let btypes = build_branches_type env (fst ind) mib mip u params dep p in @@ -352,7 +352,7 @@ and nf_predicate env ind mip params v pT = let name,dom,codom = try decompose_prod env pT with DestKO -> - Errors.anomaly + CErrors.anomaly (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") in let dep,body = diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index d6305d81a8..fe73b6105b 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Globnames @@ -317,6 +317,10 @@ let rev_it_mkPLambda = List.fold_right mkPLambda let err loc pp = user_err_loc (loc,"pattern_of_glob_constr", pp) +let warn_cast_in_pattern = + CWarnings.create ~name:"cast-in-pattern" ~category:"automation" + (fun () -> Pp.strbrk "Casts are ignored in patterns") + let rec pat_of_raw metas vars = function | GVar (_,id) -> (try PRel (List.index Name.equal (Name id) vars) @@ -348,7 +352,7 @@ let rec pat_of_raw metas vars = function | GHole _ -> PMeta None | GCast (_,c,_) -> - Feedback.msg_warning (strbrk "Cast not taken into account in constr pattern"); + warn_cast_in_pattern (); pat_of_raw metas vars c | GIf (_,c,(_,None),b1,b2) -> PIf (pat_of_raw metas vars c, diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index b0715af734..00b6100c02 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -60,7 +60,7 @@ type pretype_error = exception PretypeError of env * Evd.evar_map * pretype_error let precatchable_exception = function - | Errors.UserError _ | TypeError _ | PretypeError _ + | CErrors.UserError _ | TypeError _ | PretypeError _ | Nametab.GlobalizationError _ -> true | _ -> false diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index b6a57785a1..4b6d10c640 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -22,7 +22,7 @@ open Pp -open Errors +open CErrors open Util open Names open Evd @@ -68,6 +68,61 @@ open Inductiveops (************************************************************************) +module ExtraEnv = +struct + +type t = { + env : Environ.env; + extra : Evarutil.ext_named_context Lazy.t; + (** Delay the computation of the evar extended environment *) +} + +let get_extra env = + let open Context.Named.Declaration in + let ids = List.map get_id (named_context env) in + let avoid = List.fold_right Id.Set.add ids Id.Set.empty in + Context.Rel.fold_outside push_rel_decl_to_named_context + (Environ.rel_context env) ~init:(empty_csubst, [], avoid, named_context env) + +let make_env env = { env = env; extra = lazy (get_extra env) } +let rel_context env = rel_context env.env + +let push_rel d env = { + env = push_rel d env.env; + extra = lazy (push_rel_decl_to_named_context d (Lazy.force env.extra)); +} + +let pop_rel_context n env = make_env (pop_rel_context n env.env) + +let push_rel_context ctx env = { + env = push_rel_context ctx env.env; + extra = lazy (List.fold_right push_rel_decl_to_named_context ctx (Lazy.force env.extra)); +} + +let lookup_named id env = lookup_named id env.env + +let e_new_evar env evdref ?src ?naming typ = + let subst2 subst vsubst c = csubst_subst subst (replace_vars vsubst c) in + let open Context.Named.Declaration in + let inst_vars = List.map (fun d -> mkVar (get_id d)) (named_context env.env) in + let inst_rels = List.rev (rel_list 0 (nb_rel env.env)) in + let (subst, vsubst, _, nc) = Lazy.force env.extra in + let typ' = subst2 subst vsubst typ in + let instance = inst_rels @ inst_vars in + let sign = val_of_named_context nc in + let sigma = Sigma.Unsafe.of_evar_map !evdref in + let Sigma (e, sigma, _) = new_evar_instance sign sigma typ' ?src ?naming instance in + evdref := Sigma.to_evar_map sigma; + e + +let push_rec_types (lna,typarray,_) env = + let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in + Array.fold_left (fun e assum -> push_rel assum e) env ctxt + +end + +open ExtraEnv + (* An auxiliary function for searching for fixpoint guard indexes *) exception Found of int array @@ -81,7 +136,7 @@ let search_guard loc env possible_indexes fixdefs = let fix = ((indexes, 0),fixdefs) in (try check_fix env fix with reraise -> - let (e, info) = Errors.push reraise in + let (e, info) = CErrors.push reraise in let info = Loc.add_loc info loc in iraise (e, info)); indexes @@ -184,25 +239,34 @@ let interp_elimination_sort = function | GSet -> InSet | GType _ -> InType +type inference_hook = env -> evar_map -> evar -> evar_map * constr + type inference_flags = { use_typeclasses : bool; - use_unif_heuristics : bool; - use_hook : (env -> evar_map -> evar -> constr) option; + solve_unification_constraints : bool; + use_hook : inference_hook option; fail_evar : bool; expand_evars : bool } -let frozen_holes (sigma, sigma') = - (); fun ev -> Evar.Map.mem ev (Evd.undefined_map sigma) - -let pending_holes (sigma, sigma') = - let fold evk _ accu = - if not (Evd.mem sigma evk) then Evar.Set.add evk accu else accu - in - Evd.fold_undefined fold sigma' Evar.Set.empty +(* Compute the set of still-undefined initial evars up to restriction + (e.g. clearing) and the set of yet-unsolved evars freshly created + in the extension [sigma'] of [sigma] (excluding the restrictions of + the undefined evars of [sigma] to be freshly created evars of + [sigma']). Otherwise said, we partition the undefined evars of + [sigma'] into those already in [sigma] or deriving from an evar in + [sigma] by restriction, and the evars properly created in [sigma'] *) + +let frozen_and_pending_holes (sigma, sigma') = + let add_derivative_of evk evi acc = + match advance sigma' evk with None -> acc | Some evk' -> Evar.Set.add evk' acc in + let frozen = Evd.fold_undefined add_derivative_of sigma Evar.Set.empty in + let fold evk _ accu = if not (Evar.Set.mem evk frozen) then Evar.Set.add evk accu else accu in + let pending = Evd.fold_undefined fold sigma' Evar.Set.empty in + (frozen,pending) let apply_typeclasses env evdref frozen fail_evar = - let filter_frozen = frozen in + let filter_frozen evk = Evar.Set.mem evk frozen in evdref := Typeclasses.resolve_typeclasses ~filter:(if Flags.is_program_mode () then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk)) @@ -217,7 +281,7 @@ let apply_inference_hook hook evdref pending = if Evd.is_undefined sigma evk (* in particular not defined by side-effect *) then try - let c = hook sigma evk in + let sigma, c = hook sigma evk in Evd.define evk c sigma with Exit -> sigma @@ -226,10 +290,10 @@ let apply_inference_hook hook evdref pending = let apply_heuristics env evdref fail_evar = (* Resolve eagerly, potentially making wrong choices *) - try evdref := consider_remaining_unif_problems + try evdref := solve_unif_constraints_with_heuristics ~ts:(Typeclasses.classes_transparent_state ()) env !evdref - with e when Errors.noncritical e -> - let e = Errors.push e in if fail_evar then iraise e + with e when CErrors.noncritical e -> + let e = CErrors.push e in if fail_evar then iraise e let check_typeclasses_instances_are_solved env current_sigma frozen = (* Naive way, call resolution again with failure flag *) @@ -270,19 +334,17 @@ let check_evars_are_solved env current_sigma frozen pending = (* Try typeclasses, hooks, unification heuristics ... *) let solve_remaining_evars flags env current_sigma pending = - let frozen = frozen_holes pending in - let pending = pending_holes pending in + let frozen,pending = frozen_and_pending_holes pending in let evdref = ref current_sigma in if flags.use_typeclasses then apply_typeclasses env evdref frozen false; if Option.has_some flags.use_hook then apply_inference_hook (Option.get flags.use_hook env) evdref pending; - if flags.use_unif_heuristics then apply_heuristics env evdref false; + if flags.solve_unification_constraints then apply_heuristics env evdref false; if flags.fail_evar then check_evars_are_solved env !evdref frozen pending; !evdref let check_evars_are_solved env current_sigma pending = - let frozen = frozen_holes pending in - let pending = pending_holes pending in + let frozen,pending = frozen_and_pending_holes pending in check_evars_are_solved env current_sigma frozen pending let process_inference_flags flags env initial_sigma (sigma,c) = @@ -293,26 +355,11 @@ let process_inference_flags flags env initial_sigma (sigma,c) = (* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *) let allow_anonymous_refs = ref false -(* Utilisé pour inférer le prédicat des Cases *) -(* Semble exagérement fort *) -(* Faudra préférer une unification entre les types de toutes les clauses *) -(* et autoriser des ? à rester dans le résultat de l'unification *) - -let evar_type_fixpoint loc env evdref lna lar vdefj = - let lt = Array.length vdefj in - if Int.equal (Array.length lar) lt then - for i = 0 to lt-1 do - if not (e_cumul env evdref (vdefj.(i)).uj_type - (lift lt lar.(i))) then - error_ill_typed_rec_body_loc loc env !evdref - i lna vdefj lar - done - (* coerce to tycon if any *) let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function | None -> j | Some t -> - evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env) evdref j t + evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env.ExtraEnv.env) evdref j t let check_instance loc subst = function | [] -> () @@ -348,9 +395,10 @@ let ltac_interp_name_env k0 lvar env = (* tail is the part of the env enriched by pretyping *) let n = Context.Rel.length (rel_context env) - k0 in let ctxt,_ = List.chop n (rel_context env) in - let env = pop_rel_context n env in - let ctxt = List.map (Context.Rel.Declaration.map_name (ltac_interp_name lvar)) ctxt in - push_rel_context ctxt env + let open Context.Rel.Declaration in + let ctxt' = List.smartmap (map_name (ltac_interp_name lvar)) ctxt in + if List.equal (fun d1 d2 -> Name.equal (get_name d1) (get_name d2)) ctxt ctxt' then env + else push_rel_context ctxt' (pop_rel_context n env) let invert_ltac_bound_name lvar env id0 id = let id' = Id.Map.find id lvar.ltac_idents in @@ -361,7 +409,7 @@ let invert_ltac_bound_name lvar env id0 id = str " which is not bound in current context.") let protected_get_type_of env sigma c = - try Retyping.get_type_of ~lax:true env sigma c + try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c with Retyping.RetypeError _ -> errorlabstrm "" (str "Cannot reinterpret " ++ quote (print_constr c) ++ @@ -444,7 +492,7 @@ let pretype_global loc rigid env evd gr us = str " universe instances must be greater or equal to Set."); evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l'))) in - Evd.fresh_global ~loc ~rigid ?names:instance env evd gr + Evd.fresh_global ~loc ~rigid ?names:instance env.ExtraEnv.env evd gr let pretype_ref loc evdref env ref us = match ref with @@ -459,7 +507,7 @@ let pretype_ref loc evdref env ref us = | ref -> let evd, c = pretype_global loc univ_flexible env !evdref ref us in let () = evdref := evd in - let ty = Typing.unsafe_type_of env evd c in + let ty = Typing.unsafe_type_of env.ExtraEnv.env evd c in make_judge c ty let judge_of_Type loc evd s = @@ -477,7 +525,7 @@ let pretype_sort loc evdref = function let new_type_evar env evdref loc = let sigma = Sigma.Unsafe.of_evar_map !evdref in let Sigma ((e, _), sigma, _) = - Evarutil.new_type_evar env sigma + Evarutil.new_type_evar env.ExtraEnv.env sigma univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole) in evdref := Sigma.to_evar_map sigma; @@ -489,7 +537,7 @@ let (f_genarg_interp, genarg_interp_hook) = Hook.make () (* in environment [env], with existential variables [evdref] and *) (* the type constraint tycon *) -let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t = +let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdref (lvar : ltac_var_map) t = let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in let pretype_type = pretype_type k0 resolve_tc in let pretype = pretype k0 resolve_tc in @@ -515,7 +563,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let hyps = evar_filtered_context (Evd.find !evdref evk) in let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in let c = mkEvar (evk, args) in - let j = (Retyping.get_judgment_of env !evdref c) in + let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in inh_conv_coerce_to_tycon loc env evdref j tycon | GPatVar (loc,(someta,n)) -> @@ -544,7 +592,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | None -> new_type_evar env evdref loc in let ist = lvar.ltac_genargs in - let (c, sigma) = Hook.get f_genarg_interp ty env !evdref ist arg in + let (c, sigma) = Hook.get f_genarg_interp ty env.ExtraEnv.env !evdref ist arg in let () = evdref := sigma in { uj_val = c; uj_type = ty } @@ -578,7 +626,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let fixi = match fixkind with | GFix (vn,i) -> i | GCoFix i -> i - in e_conv env evdref ftys.(fixi) t + in e_conv env.ExtraEnv.env evdref ftys.(fixi) t | None -> true in (* Note: bodies are not used by push_rec_types, so [||] is safe *) @@ -596,7 +644,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) ctxtv vdef in - evar_type_fixpoint loc env evdref names ftys vdefj; + Typing.check_type_fixpoint loc env.ExtraEnv.env evdref names ftys vdefj; let ftys = Array.map (nf_evar !evdref) ftys in let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in let fixj = match fixkind with @@ -617,14 +665,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let fixdecls = (names,ftys,fdefs) in let indexes = search_guard - loc env possible_indexes fixdecls + loc env.ExtraEnv.env possible_indexes fixdecls in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | GCoFix i -> let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env cofix + (try check_cofix env.ExtraEnv.env cofix with reraise -> - let (e, info) = Errors.push reraise in + let (e, info) = CErrors.push reraise in let info = Loc.add_loc info loc in iraise (e, info)); make_judge (mkCoFix cofix) ftys.(i) @@ -652,7 +700,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ if Int.equal npars 0 then [] else try - let IndType (indf, args) = find_rectype env !evdref ty in + let IndType (indf, args) = find_rectype env.ExtraEnv.env !evdref ty in let ((ind',u'),pars) = dest_ind_family indf in if eq_ind ind ind' then pars else (* Let the usual code throw an error *) [] @@ -661,9 +709,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ in let app_f = match kind_of_term fj.uj_val with - | Const (p, u) when Environ.is_projection p env -> + | Const (p, u) when Environ.is_projection p env.ExtraEnv.env -> let p = Projection.make p false in - let pb = Environ.lookup_projection p env in + let pb = Environ.lookup_projection p env.ExtraEnv.env in let npars = pb.Declarations.proj_npars in fun n -> if n == npars + 1 then fun _ v -> mkProj (p, v) @@ -674,8 +722,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | [] -> resj | c::rest -> let argloc = loc_of_glob_constr c in - let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env) evdref resj in - let resty = whd_betadeltaiota env !evdref resj.uj_type in + let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env.ExtraEnv.env) evdref resj in + let resty = whd_all env.ExtraEnv.env !evdref resj.uj_type in match kind_of_term resty with | Prod (na,c1,c2) -> let tycon = Some c1 in @@ -684,7 +732,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ match candargs with | [] -> [], j_val hj | arg :: args -> - if e_conv env evdref (j_val hj) arg then + if e_conv env.ExtraEnv.env evdref (j_val hj) arg then args, nf_evar !evdref (j_val hj) else [], j_val hj in @@ -695,7 +743,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | _ -> let hj = pretype empty_tycon env evdref lvar c in error_cant_apply_not_functional_loc - (Loc.merge floc argloc) env !evdref + (Loc.merge floc argloc) env.ExtraEnv.env !evdref resj [hj] in let resj = apply_rec env 1 fj candargs args in @@ -703,13 +751,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ match evar_kind_of_term !evdref resj.uj_val with | App (f,args) -> let f = whd_evar !evdref f in - if is_template_polymorphic env f then + if is_template_polymorphic env.ExtraEnv.env f then (* Special case for inductive type applications that must be refreshed right away. *) let sigma = !evdref in let c = mkApp (f,Array.map (whd_evar sigma) args) in - let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env) evdref c in - let t = Retyping.get_type_of env !evdref c in + let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env.ExtraEnv.env) evdref c in + let t = Retyping.get_type_of env.ExtraEnv.env !evdref c in make_judge c (* use this for keeping evars: resj.uj_val *) t else resj | _ -> resj @@ -722,11 +770,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ match tycon with | None -> evd, tycon | Some ty -> - let evd, ty' = Coercion.inh_coerce_to_prod loc env evd ty in + let evd, ty' = Coercion.inh_coerce_to_prod loc env.ExtraEnv.env evd ty in evd, Some ty') evdref tycon in - let (name',dom,rng) = evd_comb1 (split_tycon loc env) evdref tycon' in + let (name',dom,rng) = evd_comb1 (split_tycon loc env.ExtraEnv.env) evdref tycon' in let dom_valcon = valcon_of_tycon dom in let j = pretype_type dom_valcon env evdref lvar c1 in (* The name specified by ltac is used also to create bindings. So @@ -735,7 +783,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let var = LocalAssum (name, j.utj_val) in let j' = pretype rng (push_rel var env) evdref lvar c2 in let name = ltac_interp_name lvar name in - let resj = judge_of_abstraction env (orelse_name name name') j j' in + let resj = judge_of_abstraction env.ExtraEnv.env (orelse_name name name') j j' in inh_conv_coerce_to_tycon loc env evdref resj tycon | GProd(loc,name,bk,c1,c2) -> @@ -748,16 +796,16 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let j = pretype_type empty_valcon env evdref lvar c2 in { j with utj_val = lift 1 j.utj_val } | Name _ -> - let var = (name,j.utj_val) in - let env' = push_rel_assum var env in + let var = LocalAssum (name, j.utj_val) in + let env' = push_rel var env in pretype_type empty_valcon env' evdref lvar c2 in let name = ltac_interp_name lvar name in let resj = try - judge_of_product env name j j' + judge_of_product env.ExtraEnv.env name j j' with TypeError _ as e -> - let (e, info) = Errors.push e in + let (e, info) = CErrors.push e in let info = Loc.add_loc info loc in iraise (e, info) in inh_conv_coerce_to_tycon loc env evdref resj tycon @@ -771,7 +819,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | _ -> pretype empty_tycon env evdref lvar c1 in let t = evd_comb1 (Evarsolve.refresh_universes - ~onlyalg:true ~status:Evd.univ_flexible (Some false) env) + ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) evdref j.uj_type in (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are @@ -786,12 +834,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | GLetTuple (loc,nal,(na,po),c,d) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = - try find_rectype env !evdref cj.uj_type + try find_rectype env.ExtraEnv.env !evdref cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in - error_case_not_inductive_loc cloc env !evdref cj + error_case_not_inductive_loc cloc env.ExtraEnv.env !evdref cj in - let cstrs = get_constructors env indf in + let cstrs = get_constructors env.ExtraEnv.env indf in if not (Int.equal (Array.length cstrs) 1) then user_err_loc (loc,"",str "Destructing let is only for inductive types" ++ str " with one constructor."); @@ -800,7 +848,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables."); let fsign, record = - match get_projections env indf with + match get_projections env.ExtraEnv.env indf with | None -> List.map2 set_name (List.rev nal) cs.cs_args, false | Some ps -> @@ -821,36 +869,36 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let nal = List.rev nal in let fsign = List.map2 set_name nal fsign in let f = it_mkLambda_or_LetIn f fsign in - let ci = make_case_info env (fst ind) LetStyle in + let ci = make_case_info env.ExtraEnv.env (fst ind) LetStyle in mkCase (ci, p, cj.uj_val,[|f|]) else it_mkLambda_or_LetIn f fsign in let env_f = push_rel_context fsign env in (* Make dependencies from arity signature impossible *) let arsgn = - let arsgn,_ = get_arity env indf in + let arsgn,_ = get_arity env.ExtraEnv.env indf in if not !allow_anonymous_refs then List.map (set_name Anonymous) arsgn else arsgn in - let psign = LocalAssum (na, build_dependent_inductive env indf) :: arsgn in + let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in let nar = List.length arsgn in (match po with | Some p -> let env_p = push_rel_context psign env in let pj = pretype_type empty_valcon env_p evdref lvar p in let ccl = nf_evar !evdref pj.utj_val in - let psign = make_arity_signature env true indf in (* with names *) + let psign = make_arity_signature env.ExtraEnv.env true indf in (* with names *) let p = it_mkLambda_or_LetIn ccl psign in let inst = (Array.to_list cs.cs_concl_realargs) @[build_dependent_constructor cs] in let lp = lift cs.cs_nargs p in - let fty = hnf_lam_applist env !evdref lp inst in + let fty = hnf_lam_applist env.ExtraEnv.env !evdref lp inst in let fj = pretype (mk_tycon fty) env_f evdref lvar d in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort env !evdref ind cj.uj_val p; + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p; obj ind p cj.uj_val fj.uj_val in { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl } @@ -863,37 +911,37 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ if noccur_between 1 cs.cs_nargs ccl then lift (- cs.cs_nargs) ccl else - error_cant_find_case_type_loc loc env !evdref + error_cant_find_case_type_loc loc env.ExtraEnv.env !evdref cj.uj_val in (* let ccl = refresh_universes ccl in *) let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort env !evdref ind cj.uj_val p; + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p; obj ind p cj.uj_val fj.uj_val in { uj_val = v; uj_type = ccl }) | GIf (loc,c,(na,po),b1,b2) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = - try find_rectype env !evdref cj.uj_type + try find_rectype env.ExtraEnv.env !evdref cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in - error_case_not_inductive_loc cloc env !evdref cj in - let cstrs = get_constructors env indf in + error_case_not_inductive_loc cloc env.ExtraEnv.env !evdref cj in + let cstrs = get_constructors env.ExtraEnv.env indf in if not (Int.equal (Array.length cstrs) 2) then user_err_loc (loc,"", str "If is only for inductive types with two constructors."); let arsgn = - let arsgn,_ = get_arity env indf in + let arsgn,_ = get_arity env.ExtraEnv.env indf in if not !allow_anonymous_refs then (* Make dependencies from arity signature impossible *) List.map (set_name Anonymous) arsgn else arsgn in let nar = List.length arsgn in - let psign = LocalAssum (na, build_dependent_inductive env indf) :: arsgn in + let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in let pred,p = match po with | Some p -> let env_p = push_rel_context psign env in @@ -931,9 +979,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let b2 = f cstrs.(1) b2 in let v = let ind,_ = dest_ind_family indf in - let ci = make_case_info env (fst ind) IfStyle in + let ci = make_case_info env.ExtraEnv.env (fst ind) IfStyle in let pred = nf_evar !evdref pred in - Typing.check_allowed_sort env !evdref ind cj.uj_val pred; + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val pred; mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in let cj = { uj_val = v; uj_type = p } in @@ -941,43 +989,46 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | GCases (loc,sty,po,tml,eqns) -> Cases.compile_cases loc sty - ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref) - tycon env (* loc *) (po,tml,eqns) + ((fun vtyc env evdref -> pretype vtyc (make_env env) evdref lvar),evdref) + tycon env.ExtraEnv.env (* loc *) (po,tml,eqns) | GCast (loc,c,k) -> let cj = match k with | CastCoerce -> let cj = pretype empty_tycon env evdref lvar c in - evd_comb1 (Coercion.inh_coerce_to_base loc env) evdref cj + evd_comb1 (Coercion.inh_coerce_to_base loc env.ExtraEnv.env) evdref cj | CastConv t | CastVM t | CastNative t -> let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in let tj = pretype_type empty_valcon env evdref lvar t in - let tval = nf_evar !evdref tj.utj_val in - let cj = match k with + let tval = evd_comb1 (Evarsolve.refresh_universes + ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) + evdref tj.utj_val in + let tval = nf_evar !evdref tval in + let cj, tval = match k with | VMcast -> let cj = pretype empty_tycon env evdref lvar c in - let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in + let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in if not (occur_existential cty || occur_existential tval) then - let (evd,b) = Reductionops.vm_infer_conv env !evdref cty tval in - if b then (evdref := evd; cj) + let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in + if b then (evdref := evd; cj, tval) else - error_actual_type_loc loc env !evdref cj tval - (ConversionFailed (env,cty,tval)) + error_actual_type_loc loc env.ExtraEnv.env !evdref cj tval + (ConversionFailed (env.ExtraEnv.env,cty,tval)) else user_err_loc (loc,"",str "Cannot check cast with vm: " ++ str "unresolved arguments remain.") | NATIVEcast -> let cj = pretype empty_tycon env evdref lvar c in - let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in + let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in begin - let (evd,b) = Nativenorm.native_infer_conv env !evdref cty tval in - if b then (evdref := evd; cj) + let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in + if b then (evdref := evd; cj, tval) else - error_actual_type_loc loc env !evdref cj tval - (ConversionFailed (env,cty,tval)) + error_actual_type_loc loc env.ExtraEnv.env !evdref cj tval + (ConversionFailed (env.ExtraEnv.env,cty,tval)) end | _ -> - pretype (mk_tycon tval) env evdref lvar c + pretype (mk_tycon tval) env evdref lvar c, tval in let v = mkCast (cj.uj_val, k, tval) in { uj_val = v; uj_type = tval } @@ -995,11 +1046,11 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = with Not_found -> try let (n,_,t') = lookup_rel_id id (rel_context env) in - if is_conv env !evdref t t' then mkRel n, update else raise Not_found + if is_conv env.ExtraEnv.env !evdref t t' then mkRel n, update else raise Not_found with Not_found -> try let t' = lookup_named id env |> get_type in - if is_conv env !evdref t t' then mkVar id, update else raise Not_found + if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found with Not_found -> user_err_loc (loc,"",str "Cannot interpret " ++ pr_existential_key !evdref evk ++ @@ -1010,17 +1061,17 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = Array.map_of_list snd subst (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) -and pretype_type k0 resolve_tc valcon env evdref lvar = function +and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function | GHole (loc, knd, naming, None) -> (match valcon with | Some v -> let s = let sigma = !evdref in - let t = Retyping.get_type_of env sigma v in - match kind_of_term (whd_betadeltaiota env sigma t) with + let t = Retyping.get_type_of env.ExtraEnv.env sigma v in + match kind_of_term (whd_all env.ExtraEnv.env sigma t) with | Sort s -> s | Evar ev when is_Type (existential_type sigma ev) -> - evd_comb1 (define_evar_as_sort env) evdref ev + evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev | _ -> anomaly (Pp.str "Found a type constraint which is not a type") in { utj_val = v; @@ -1033,16 +1084,17 @@ and pretype_type k0 resolve_tc valcon env evdref lvar = function | c -> let j = pretype k0 resolve_tc empty_tycon env evdref lvar c in let loc = loc_of_glob_constr c in - let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in + let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env.ExtraEnv.env) evdref j in match valcon with | None -> tj | Some v -> - if e_cumul env evdref v tj.utj_val then tj + if e_cumul env.ExtraEnv.env evdref v tj.utj_val then tj else error_unexpected_type_loc - (loc_of_glob_constr c) env !evdref tj.utj_val v + (loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v let ise_pretype_gen flags env sigma lvar kind c = + let env = make_env env in let evdref = ref sigma in let k0 = Context.Rel.length (rel_context env) in let c' = match kind with @@ -1053,18 +1105,18 @@ let ise_pretype_gen flags env sigma lvar kind c = | IsType -> (pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val in - process_inference_flags flags env sigma (!evdref,c') + process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c') let default_inference_flags fail = { use_typeclasses = true; - use_unif_heuristics = true; + solve_unification_constraints = true; use_hook = None; fail_evar = fail; expand_evars = true } let no_classes_no_fail_inference_flags = { use_typeclasses = false; - use_unif_heuristics = true; + solve_unification_constraints = true; use_hook = None; fail_evar = false; expand_evars = true } @@ -1085,19 +1137,21 @@ let on_judgment f j = {uj_val = c; uj_type = t} let understand_judgment env sigma c = + let env = make_env env in let evdref = ref sigma in let k0 = Context.Rel.length (rel_context env) in let j = pretype k0 true empty_tycon env evdref empty_lvar c in let j = on_judgment (fun c -> - let evd, c = process_inference_flags all_and_fail_flags env sigma (!evdref,c) in + let evd, c = process_inference_flags all_and_fail_flags env.ExtraEnv.env sigma (!evdref,c) in evdref := evd; c) j in j, Evd.evar_universe_context !evdref let understand_judgment_tcc env evdref c = + let env = make_env env in let k0 = Context.Rel.length (rel_context env) in let j = pretype k0 true empty_tycon env evdref empty_lvar c in on_judgment (fun c -> - let (evd,c) = process_inference_flags all_no_fail_flags env Evd.empty (!evdref,c) in + let (evd,c) = process_inference_flags all_no_fail_flags env.ExtraEnv.env Evd.empty (!evdref,c) in evdref := evd; c) j let ise_pretype_gen_ctx flags env sigma lvar kind c = @@ -1126,7 +1180,7 @@ let understand_ltac flags env sigma lvar kind c = let constr_flags = { use_typeclasses = true; - use_unif_heuristics = true; + solve_unification_constraints = true; use_hook = None; fail_evar = true; expand_evars = true } @@ -1146,3 +1200,9 @@ let type_uconstr ?(flags = constr_flags) let (sigma, c) = understand_ltac flags env sigma vars expected_type term in Sigma.Unsafe.of_pair (c, sigma) end } + +let pretype k0 resolve_tc typcon env evdref lvar t = + pretype k0 resolve_tc typcon (make_env env) evdref lvar t + +let pretype_type k0 resolve_tc valcon env evdref lvar t = + pretype_type k0 resolve_tc valcon (make_env env) evdref lvar t diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 824bb11aa4..0f3f7c3c9a 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -47,10 +47,12 @@ val empty_lvar : ltac_var_map type glob_constr_ltac_closure = ltac_var_map * glob_constr type pure_open_constr = evar_map * constr +type inference_hook = env -> evar_map -> evar -> evar_map * constr + type inference_flags = { use_typeclasses : bool; - use_unif_heuristics : bool; - use_hook : (env -> evar_map -> evar -> constr) option; + solve_unification_constraints : bool; + use_hook : inference_hook option; fail_evar : bool; expand_evars : bool } diff --git a/pretyping/program.ml b/pretyping/program.ml index 0bd121f6f1..62aedcfbf6 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Term @@ -15,10 +15,12 @@ open Term let make_dir l = DirPath.make (List.rev_map Id.of_string l) let find_reference locstr dir s = - let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in + let dp = make_dir dir in + let sp = Libnames.make_path dp (Id.of_string s) in try Nametab.global_of_path sp with Not_found -> - anomaly ~label:locstr (Pp.str "cannot find" ++ spc () ++ Libnames.pr_path sp) + user_err_loc (Loc.ghost, "", str "Library " ++ Libnames.pr_dirpath dp ++ + str " has to be required first.") let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr dir s) @@ -67,3 +69,43 @@ let mk_coq_and l = (fun c conj -> mkApp (and_typ, [| c ; conj |])) l + +(* true = transparent by default, false = opaque if possible *) +let proofs_transparency = ref true +let program_cases = ref true +let program_generalized_coercion = ref true + +let set_proofs_transparency = (:=) proofs_transparency +let get_proofs_transparency () = !proofs_transparency + +let is_program_generalized_coercion () = !program_generalized_coercion +let is_program_cases () = !program_cases + +open Goptions + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "preferred transparency of Program obligations"; + optkey = ["Transparent";"Obligations"]; + optread = get_proofs_transparency; + optwrite = set_proofs_transparency; } + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "program cases"; + optkey = ["Program";"Cases"]; + optread = (fun () -> !program_cases); + optwrite = (:=) program_cases } + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "program generalized coercion"; + optkey = ["Program";"Generalized";"Coercion"]; + optread = (fun () -> !program_generalized_coercion); + optwrite = (:=) program_generalized_coercion } diff --git a/pretyping/program.mli b/pretyping/program.mli index b7ebcbc95c..023ff8ca58 100644 --- a/pretyping/program.mli +++ b/pretyping/program.mli @@ -37,3 +37,7 @@ val mk_coq_not : constr -> constr (** Polymorphic application of delayed references *) val papp : Evd.evar_map ref -> (unit -> global_reference) -> constr array -> constr + +val get_proofs_transparency : unit -> bool +val is_program_cases : unit -> bool +val is_program_generalized_coercion : unit -> bool diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index bbb6a92663..284af0cb15 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -13,7 +13,7 @@ (* This file registers properties of records: projections and canonical structures *) -open Errors +open CErrors open Util open Pp open Names @@ -176,7 +176,7 @@ let cs_pattern_of_constr t = App (f,vargs) -> begin try Const_cs (global_of_constr f) , None, Array.to_list vargs - with e when Errors.noncritical e -> raise Not_found + with e when CErrors.noncritical e -> raise Not_found end | Rel n -> Default_cs, Some n, [] | Prod (_,a,b) when not (Termops.dependent (mkRel 1) b) -> Prod_cs, None, [a; Termops.pop b] @@ -184,11 +184,18 @@ let cs_pattern_of_constr t = | _ -> begin try Const_cs (global_of_constr t) , None, [] - with e when Errors.noncritical e -> raise Not_found + with e when CErrors.noncritical e -> raise Not_found end +let warn_projection_no_head_constant = + CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker" + (fun (t,con_pp,proji_sp_pp) -> + strbrk "Projection value has no head constant: " + ++ Termops.print_constr t ++ strbrk " in canonical instance " + ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") + (* Intended to always succeed *) -let compute_canonical_projections (con,ind) = +let compute_canonical_projections warn (con,ind) = let env = Global.env () in let ctx = Univ.instantiate_univ_context (Environ.constant_context env con) in let u = Univ.UContext.instance ctx in @@ -213,13 +220,10 @@ let compute_canonical_projections (con,ind) = let patt, n , args = cs_pattern_of_constr t in ((ConstRef proji_sp, patt, t, n, args) :: l) with Not_found -> - if Flags.is_verbose () then - (let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) + let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) and proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in - Feedback.msg_warning (strbrk "No global reference exists for projection value" - ++ Termops.print_constr t ++ strbrk " in instance " - ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")); - l + if warn then warn_projection_no_head_constant (t,con_pp,proji_sp_pp); + l end | _ -> l) [] lps in @@ -235,9 +239,15 @@ let pr_cs_pattern = function | Default_cs -> str "_" | Sort_cs s -> Termops.pr_sort_family s -let open_canonical_structure i (_,o) = - if Int.equal i 1 then - let lo = compute_canonical_projections o in +let warn_redundant_canonical_projection = + CWarnings.create ~name:"redundant-canonical-projection" ~category:"typechecker" + (fun (hd_val,prj,new_can_s,old_can_s) -> + strbrk "Ignoring canonical projection to " ++ hd_val + ++ strbrk " by " ++ prj ++ strbrk " in " + ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s) + +let add_canonical_structure warn o = + let lo = compute_canonical_projections warn o in List.iter (fun ((proj,(cs_pat,_ as pat)),s) -> let l = try Refmap.find proj !object_table with Not_found -> [] in let ocs = try Some (assoc_pat cs_pat l) @@ -245,17 +255,18 @@ let open_canonical_structure i (_,o) = in match ocs with | None -> object_table := Refmap.add proj ((pat,s)::l) !object_table; | Some (c, cs) -> - if Flags.is_verbose () then let old_can_s = (Termops.print_constr cs.o_DEF) and new_can_s = (Termops.print_constr s.o_DEF) in let prj = (Nametab.pr_global_env Id.Set.empty proj) and hd_val = (pr_cs_pattern cs_pat) in - Feedback.msg_warning (strbrk "Ignoring canonical projection to " ++ hd_val - ++ strbrk " by " ++ prj ++ strbrk " in " - ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s)) lo + if warn then warn_redundant_canonical_projection (hd_val,prj,new_can_s,old_can_s)) + lo + +let open_canonical_structure i (_, o) = + if Int.equal i 1 then add_canonical_structure false o -let cache_canonical_structure o = - open_canonical_structure 1 o +let cache_canonical_structure (_, o) = + add_canonical_structure true o let subst_canonical_structure (subst,(cst,ind as obj)) = (* invariant: cst is an evaluable reference. Thus we can take *) @@ -317,7 +328,7 @@ let is_open_canonical_projection env sigma (c,args) = (** Check if there is some canonical projection attached to this structure *) let _ = Refmap.find ref !object_table in try - let arg = whd_betadeltaiota env sigma (Stack.nth args n) in + let arg = whd_all env sigma (Stack.nth args n) in let hd = match kind_of_term arg with App (hd, _) -> hd | _ -> arg in not (isConstruct hd) with Failure _ -> false diff --git a/pretyping/redops.ml b/pretyping/redops.ml index c188995a84..7d65925e57 100644 --- a/pretyping/redops.ml +++ b/pretyping/redops.ml @@ -14,25 +14,29 @@ let make_red_flag l = let rec add_flag red = function | [] -> red | FBeta :: lf -> add_flag { red with rBeta = true } lf - | FIota :: lf -> add_flag { red with rIota = true } lf + | FMatch :: lf -> add_flag { red with rMatch = true } lf + | FFix :: lf -> add_flag { red with rFix = true } lf + | FCofix :: lf -> add_flag { red with rCofix = true } lf | FZeta :: lf -> add_flag { red with rZeta = true } lf | FConst l :: lf -> if red.rDelta then - Errors.error + CErrors.error "Cannot set both constants to unfold and constants not to unfold"; add_flag { red with rConst = union_consts red.rConst l } lf | FDeltaBut l :: lf -> if red.rConst <> [] && not red.rDelta then - Errors.error + CErrors.error "Cannot set both constants to unfold and constants not to unfold"; add_flag { red with rConst = union_consts red.rConst l; rDelta = true } lf in add_flag - {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []} + {rBeta = false; rMatch = false; rFix = false; rCofix = false; + rZeta = false; rDelta = false; rConst = []} l let all_flags = - {rBeta = true; rIota = true; rZeta = true; rDelta = true; rConst = []} + {rBeta = true; rMatch = true; rFix = true; rCofix = true; + rZeta = true; rDelta = true; rConst = []} diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 79cb7a2f67..332d4e0b26 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Term @@ -26,6 +26,19 @@ exception Elimconst their parameters in its stack. *) +let refolding_in_reduction = ref false +let _ = Goptions.declare_bool_option { + Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optname = + "Perform refolding of fixpoints/constants like cbn during reductions"; + Goptions.optkey = ["Refolding";"Reduction"]; + Goptions.optread = (fun () -> !refolding_in_reduction); + Goptions.optwrite = (fun a -> refolding_in_reduction:=a); +} + +let get_refolding_in_reduction () = !refolding_in_reduction +let set_refolding_in_reduction = (:=) refolding_in_reduction + (** Machinery to custom the behavior of the reduction *) module ReductionBehaviour = struct open Globnames @@ -153,9 +166,6 @@ module Cst_stack = struct let empty = [] let is_empty = CList.is_empty - let sanity x y = - assert(Term.eq_constr x y) - let drop_useless = function | _ :: ((_,_,[])::_ as q) -> q | l -> l @@ -164,9 +174,9 @@ module Cst_stack = struct let append2cst = function | (c,params,[]) -> (c, h::params, []) | (c,params,((i,t)::q)) when i = pred (Array.length t) -> - let () = sanity h t.(i) in (c, params, q) + (c, params, q) | (c,params,(i,t)::q) -> - let () = sanity h t.(i) in (c, params, (succ i,t)::q) + (c, params, (succ i,t)::q) in drop_useless (List.map append2cst cst_l) @@ -619,36 +629,21 @@ let rec strong_prodspine redfun sigma c = (*** Reduction using bindingss ***) (*************************************) -(* Local *) -let nored = Closure.RedFlags.no_red -let beta = Closure.beta -let eta = Closure.RedFlags.mkflags [Closure.RedFlags.fETA] -let zeta = Closure.RedFlags.mkflags [Closure.RedFlags.fZETA] -let betaiota = Closure.betaiota -let betaiotazeta = Closure.betaiotazeta - -(* Contextual *) -let delta = Closure.RedFlags.mkflags [Closure.RedFlags.fDELTA] -let betalet = Closure.RedFlags.mkflags [Closure.RedFlags.fBETA;Closure.RedFlags.fZETA] -let betaetalet = Closure.RedFlags.red_add betalet Closure.RedFlags.fETA -let betadelta = Closure.RedFlags.red_add betalet Closure.RedFlags.fDELTA -let betadeltaeta = Closure.RedFlags.red_add betadelta Closure.RedFlags.fETA -let betadeltaiota = Closure.RedFlags.red_add betadelta Closure.RedFlags.fIOTA -let betadeltaiota_nolet = Closure.betadeltaiotanolet -let betadeltaiotaeta = Closure.RedFlags.red_add betadeltaiota Closure.RedFlags.fETA +let eta = CClosure.RedFlags.mkflags [CClosure.RedFlags.fETA] (* Beta Reduction tools *) -let apply_subst recfun env cst_l t stack = +let apply_subst recfun env refold cst_l t stack = let rec aux env cst_l t stack = match (Stack.decomp stack,kind_of_term t) with | Some (h,stacktl), Lambda (_,_,c) -> - aux (h::env) (Cst_stack.add_param h cst_l) c stacktl + let cst_l' = if refold then Cst_stack.add_param h cst_l else cst_l in + aux (h::env) cst_l' c stacktl | _ -> recfun cst_l (substl env t, stack) in aux env cst_l t stack let stacklam recfun env t stack = - apply_subst (fun _ -> recfun) env Cst_stack.empty t stack + apply_subst (fun _ -> recfun) env false Cst_stack.empty t stack let beta_applist (c,l) = stacklam Stack.zip [] c (Stack.append_app_list l Stack.empty) @@ -713,11 +708,16 @@ let contract_cofix ?env ?reference (bodynum,(names,types,bodies as typedbodies)) substl closure bodies.(bodynum) (** Similar to the "fix" case below *) -let reduce_and_refold_cofix recfun env cst_l cofix sk = - let raw_answer = contract_cofix ~env ?reference:(Cst_stack.reference cst_l) cofix in +let reduce_and_refold_cofix recfun env refold cst_l cofix sk = + let raw_answer = + let env = if refold then Some env else None in + contract_cofix ?env ?reference:(Cst_stack.reference cst_l) cofix in apply_subst - (fun x (t,sk') -> recfun x (Cst_stack.best_replace (mkCoFix cofix) cst_l t,sk')) - [] Cst_stack.empty raw_answer sk + (fun x (t,sk') -> + let t' = + if refold then Cst_stack.best_replace (mkCoFix cofix) cst_l t else t in + recfun x (t',sk')) + [] refold Cst_stack.empty raw_answer sk let reduce_mind_case mia = match kind_of_term mia.mconstr with @@ -753,11 +753,18 @@ let contract_fix ?env ?reference ((recindices,bodynum),(names,types,bodies as ty replace the fixpoint by the best constant from [cst_l] Other rels are directly substituted by constants "magically found from the context" in contract_fix *) -let reduce_and_refold_fix recfun env cst_l fix sk = - let raw_answer = contract_fix ~env ?reference:(Cst_stack.reference cst_l) fix in +let reduce_and_refold_fix recfun env refold cst_l fix sk = + let raw_answer = + let env = if refold then None else Some env in + contract_fix ?env ?reference:(Cst_stack.reference cst_l) fix in apply_subst - (fun x (t,sk') -> recfun x (Cst_stack.best_replace (mkFix fix) cst_l t,sk')) - [] Cst_stack.empty raw_answer sk + (fun x (t,sk') -> + let t' = + if refold then + Cst_stack.best_replace (mkFix fix) cst_l t + else t + in recfun x (t',sk')) + [] refold Cst_stack.empty raw_answer sk let fix_recarg ((recindices,bodynum),_) stack = assert (0 <= bodynum && bodynum < Array.length recindices); @@ -797,7 +804,7 @@ let equal_stacks (x, l) (y, l') = | None -> false | Some (lft1,lft2) -> f_equal (x, lft1) (y, lft2) -let rec whd_state_gen ?csts tactic_mode flags env sigma = +let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = let open Context.Named.Declaration in let rec whrec cst_l (x, stack as s) = let () = if !debug_RAKAM then @@ -806,21 +813,22 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = (h 0 (str "<<" ++ Termops.print_constr x ++ str "|" ++ cut () ++ Cst_stack.pr cst_l ++ str "|" ++ cut () ++ Stack.pr Termops.print_constr stack ++ - str ">>") ++ fnl ()) + str ">>")) in let fold () = let () = if !debug_RAKAM then - let open Pp in Feedback.msg_notice (str "<><><><><>" ++ fnl ()) in + let open Pp in Feedback.msg_notice (str "<><><><><>") in (s,cst_l) in match kind_of_term x with - | Rel n when Closure.RedFlags.red_set flags Closure.RedFlags.fDELTA -> + | Rel n when CClosure.RedFlags.red_set flags CClosure.RedFlags.fDELTA -> (match lookup_rel n env with | LocalDef (_,body,_) -> whrec Cst_stack.empty (lift n body, stack) | _ -> fold ()) - | Var id when Closure.RedFlags.red_set flags (Closure.RedFlags.fVAR id) -> + | Var id when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fVAR id) -> (match lookup_named id env with - | LocalDef (_,body,_) -> whrec (Cst_stack.add_cst (mkVar id) cst_l) (body, stack) + | LocalDef (_,body,_) -> + whrec (if refold then Cst_stack.add_cst (mkVar id) cst_l else cst_l) (body, stack) | _ -> fold ()) | Evar ev -> (match safe_evar_value sigma ev with @@ -830,12 +838,13 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = (match safe_meta_value sigma ev with | Some body -> whrec cst_l (body, stack) | None -> fold ()) - | Const (c,u as const) when Closure.RedFlags.red_set flags (Closure.RedFlags.fCONST c) -> + | Const (c,u as const) when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) -> (match constant_opt_value_in env const with | None -> fold () | Some body -> if not tactic_mode - then whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack) + then whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l) + (body, stack) else (* Looks for ReductionBehaviour *) match ReductionBehaviour.get (Globnames.ConstRef c) with | None -> whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack) @@ -870,7 +879,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = whrec Cst_stack.empty (arg,Stack.Cst(Stack.Cst_const const,curr,remains,bef,cst_l)::s') ) - | Proj (p, c) when Closure.RedFlags.red_projection flags p -> + | Proj (p, c) when CClosure.RedFlags.red_projection flags p -> (let pb = lookup_projection p env in let kn = Projection.constant p in let npars = pb.Declarations.proj_npars @@ -911,21 +920,21 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = (arg,Stack.Cst(Stack.Cst_proj p,curr,remains, Stack.append_app [|c|] bef,cst_l)::s')) - | LetIn (_,b,_,c) when Closure.RedFlags.red_set flags Closure.RedFlags.fZETA -> - apply_subst whrec [b] cst_l c stack + | LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA -> + apply_subst whrec [b] refold cst_l c stack | Cast (c,_,_) -> whrec cst_l (c, stack) | App (f,cl) -> whrec - (Cst_stack.add_args cl cst_l) + (if refold then Cst_stack.add_args cl cst_l else cst_l) (f, Stack.append_app cl stack) | Lambda (na,t,c) -> (match Stack.decomp stack with - | Some _ when Closure.RedFlags.red_set flags Closure.RedFlags.fBETA -> - apply_subst whrec [] cst_l x stack - | None when Closure.RedFlags.red_set flags Closure.RedFlags.fETA -> + | Some _ when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA -> + apply_subst whrec [] refold cst_l x stack + | None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA -> let env' = push_rel (LocalAssum (na,t)) env in - let whrec' = whd_state_gen tactic_mode flags env' sigma in - (match kind_of_term (Stack.zip ~refold:true (fst (whrec' (c, Stack.empty)))) with + let whrec' = whd_state_gen ~refold ~tactic_mode flags env' sigma in + (match kind_of_term (Stack.zip ~refold (fst (whrec' (c, Stack.empty)))) with | App (f,cl) -> let napp = Array.length cl in if napp > 0 then @@ -950,16 +959,18 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = whrec Cst_stack.empty (arg, Stack.Fix(f,bef,cst_l)::s')) | Construct ((ind,c),u) -> - if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then + let use_match = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in + let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in + if use_match || use_fix then match Stack.strip_app stack with - |args, (Stack.Case(ci, _, lf,_)::s') -> + |args, (Stack.Case(ci, _, lf,_)::s') when use_match -> whrec Cst_stack.empty (lf.(c-1), (Stack.tail ci.ci_npar args) @ s') - |args, (Stack.Proj (n,m,p,_)::s') -> + |args, (Stack.Proj (n,m,p,_)::s') when use_match -> whrec Cst_stack.empty (Stack.nth args (n+m), s') - |args, (Stack.Fix (f,s',cst_l)::s'') -> + |args, (Stack.Fix (f,s',cst_l)::s'') when use_fix -> let x' = Stack.zip(x,args) in let out_sk = s' @ (Stack.append_app [|x'|] s'') in - reduce_and_refold_fix whrec env cst_l f out_sk + reduce_and_refold_fix whrec env refold cst_l f out_sk |args, (Stack.Cst (const,curr,remains,s',cst_l) :: s'') -> let x' = Stack.zip(x,args) in begin match remains with @@ -969,7 +980,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = (match constant_opt_value_in env const with | None -> fold () | Some body -> - whrec (Cst_stack.add_cst (mkConstU const) cst_l) + whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l) (body, s' @ (Stack.append_app [|x'|] s''))) | Stack.Cst_proj p -> let pb = lookup_projection p env in @@ -988,14 +999,14 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = Stack.Cst (const,next,remains',s' @ (Stack.append_app [|x'|] bef),cst_l) :: s''') end |_, (Stack.App _|Stack.Update _|Stack.Shift _)::_ -> assert false - |_, [] -> fold () + |_, _ -> fold () else fold () | CoFix cofix -> - if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then + if CClosure.RedFlags.red_set flags CClosure.RedFlags.fCOFIX then match Stack.strip_app stack with |args, ((Stack.Case _ |Stack.Proj _)::s') -> - reduce_and_refold_cofix whrec env cst_l cofix stack + reduce_and_refold_cofix whrec env refold cst_l cofix stack |_ -> fold () else fold () @@ -1010,15 +1021,15 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = let local_whd_state_gen flags sigma = let rec whrec (x, stack as s) = match kind_of_term x with - | LetIn (_,b,_,c) when Closure.RedFlags.red_set flags Closure.RedFlags.fZETA -> + | LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA -> stacklam whrec [b] c stack | Cast (c,_,_) -> whrec (c, stack) | App (f,cl) -> whrec (f, Stack.append_app cl stack) | Lambda (_,_,c) -> (match Stack.decomp stack with - | Some (a,m) when Closure.RedFlags.red_set flags Closure.RedFlags.fBETA -> + | Some (a,m) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA -> stacklam whrec [a] c m - | None when Closure.RedFlags.red_set flags Closure.RedFlags.fETA -> + | None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA -> (match kind_of_term (Stack.zip (whrec (c, Stack.empty))) with | App (f,cl) -> let napp = Array.length cl in @@ -1034,7 +1045,7 @@ let local_whd_state_gen flags sigma = | _ -> s) | _ -> s) - | Proj (p,c) when Closure.RedFlags.red_projection flags p -> + | Proj (p,c) when CClosure.RedFlags.red_projection flags p -> (let pb = lookup_projection p (Global.env ()) in whrec (c, Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p, Cst_stack.empty) @@ -1059,21 +1070,23 @@ let local_whd_state_gen flags sigma = | None -> s) | Construct ((ind,c),u) -> - if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then + let use_match = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in + let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in + if use_match || use_fix then match Stack.strip_app stack with - |args, (Stack.Case(ci, _, lf,_)::s') -> + |args, (Stack.Case(ci, _, lf,_)::s') when use_match -> whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s') - |args, (Stack.Proj (n,m,p,_) :: s') -> + |args, (Stack.Proj (n,m,p,_) :: s') when use_match -> whrec (Stack.nth args (n+m), s') - |args, (Stack.Fix (f,s',cst)::s'') -> + |args, (Stack.Fix (f,s',cst)::s'') when use_fix -> let x' = Stack.zip(x,args) in whrec (contract_fix f, s' @ (Stack.append_app [|x'|] s'')) |_, (Stack.App _|Stack.Update _|Stack.Shift _|Stack.Cst _)::_ -> assert false - |_, [] -> s + |_, _ -> s else s | CoFix cofix -> - if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then + if CClosure.RedFlags.red_set flags CClosure.RedFlags.fCOFIX then match Stack.strip_app stack with |args, ((Stack.Case _ | Stack.Proj _)::s') -> whrec (contract_cofix cofix, stack) @@ -1085,7 +1098,7 @@ let local_whd_state_gen flags sigma = whrec let raw_whd_state_gen flags env = - let f sigma s = fst (whd_state_gen false flags env sigma s) in + let f sigma s = fst (whd_state_gen (get_refolding_in_reduction ()) false flags env sigma s) in f let stack_red_of_state_red f = @@ -1095,7 +1108,7 @@ let stack_red_of_state_red f = (* Drops the Cst_stack *) let iterate_whd_gen refold flags env sigma s = let rec aux t = - let (hd,sk),_ = whd_state_gen refold flags env sigma (t,Stack.empty) in + let (hd,sk),_ = whd_state_gen refold false flags env sigma (t,Stack.empty) in let whd_sk = Stack.map aux sk in Stack.zip ~refold (hd,whd_sk) in aux s @@ -1105,79 +1118,64 @@ let red_of_state_red f sigma x = (* 0. No Reduction Functions *) -let whd_nored_state = local_whd_state_gen nored +let whd_nored_state = local_whd_state_gen CClosure.nored let whd_nored_stack = stack_red_of_state_red whd_nored_state let whd_nored = red_of_state_red whd_nored_state (* 1. Beta Reduction Functions *) -let whd_beta_state = local_whd_state_gen beta +let whd_beta_state = local_whd_state_gen CClosure.beta let whd_beta_stack = stack_red_of_state_red whd_beta_state let whd_beta = red_of_state_red whd_beta_state -(* Nouveau ! *) -let whd_betaetalet_state = local_whd_state_gen betaetalet -let whd_betaetalet_stack = stack_red_of_state_red whd_betaetalet_state -let whd_betaetalet = red_of_state_red whd_betaetalet_state - -let whd_betalet_state = local_whd_state_gen betalet +let whd_betalet_state = local_whd_state_gen CClosure.betazeta let whd_betalet_stack = stack_red_of_state_red whd_betalet_state let whd_betalet = red_of_state_red whd_betalet_state (* 2. Delta Reduction Functions *) -let whd_delta_state e = raw_whd_state_gen delta e +let whd_delta_state e = raw_whd_state_gen CClosure.delta e let whd_delta_stack env = stack_red_of_state_red (whd_delta_state env) let whd_delta env = red_of_state_red (whd_delta_state env) -let whd_betadelta_state e = raw_whd_state_gen betadelta e -let whd_betadelta_stack env = - stack_red_of_state_red (whd_betadelta_state env) -let whd_betadelta env = - red_of_state_red (whd_betadelta_state env) +let whd_betadeltazeta_state e = raw_whd_state_gen CClosure.betadeltazeta e +let whd_betadeltazeta_stack env = + stack_red_of_state_red (whd_betadeltazeta_state env) +let whd_betadeltazeta env = + red_of_state_red (whd_betadeltazeta_state env) -let whd_betadeltaeta_state e = raw_whd_state_gen betadeltaeta e -let whd_betadeltaeta_stack env = - stack_red_of_state_red (whd_betadeltaeta_state env) -let whd_betadeltaeta env = - red_of_state_red (whd_betadeltaeta_state env) - (* 3. Iota reduction Functions *) -let whd_betaiota_state = local_whd_state_gen betaiota +let whd_betaiota_state = local_whd_state_gen CClosure.betaiota let whd_betaiota_stack = stack_red_of_state_red whd_betaiota_state let whd_betaiota = red_of_state_red whd_betaiota_state -let whd_betaiotazeta_state = local_whd_state_gen betaiotazeta +let whd_betaiotazeta_state = local_whd_state_gen CClosure.betaiotazeta let whd_betaiotazeta_stack = stack_red_of_state_red whd_betaiotazeta_state let whd_betaiotazeta = red_of_state_red whd_betaiotazeta_state -let whd_betadeltaiota_state env = raw_whd_state_gen betadeltaiota env -let whd_betadeltaiota_stack env = - stack_red_of_state_red (whd_betadeltaiota_state env) -let whd_betadeltaiota env = - red_of_state_red (whd_betadeltaiota_state env) - -let whd_betadeltaiotaeta_state env = raw_whd_state_gen betadeltaiotaeta env -let whd_betadeltaiotaeta_stack env = - stack_red_of_state_red (whd_betadeltaiotaeta_state env) -let whd_betadeltaiotaeta env = - red_of_state_red (whd_betadeltaiotaeta_state env) +let whd_all_state env = raw_whd_state_gen CClosure.all env +let whd_all_stack env = + stack_red_of_state_red (whd_all_state env) +let whd_all env = + red_of_state_red (whd_all_state env) -let whd_betadeltaiota_nolet_state env = raw_whd_state_gen betadeltaiota_nolet env -let whd_betadeltaiota_nolet_stack env = - stack_red_of_state_red (whd_betadeltaiota_nolet_state env) -let whd_betadeltaiota_nolet env = - red_of_state_red (whd_betadeltaiota_nolet_state env) +let whd_allnolet_state env = raw_whd_state_gen CClosure.allnolet env +let whd_allnolet_stack env = + stack_red_of_state_red (whd_allnolet_state env) +let whd_allnolet env = + red_of_state_red (whd_allnolet_state env) -(* 4. Eta reduction Functions *) +(* 4. Ad-hoc eta reduction, does not subsitute evars *) -let whd_eta c = Stack.zip (local_whd_state_gen eta Evd.empty (c,Stack.empty)) +let shrink_eta c = Stack.zip (local_whd_state_gen eta Evd.empty (c,Stack.empty)) (* 5. Zeta Reduction Functions *) -let whd_zeta c = Stack.zip (local_whd_state_gen zeta Evd.empty (c,Stack.empty)) +let whd_zeta_state = local_whd_state_gen CClosure.zeta +let whd_zeta_stack = stack_red_of_state_red whd_zeta_state +let whd_zeta = red_of_state_red whd_zeta_state (****************************************************************************) (* Reduction Functions *) @@ -1193,16 +1191,16 @@ let nf_evar = Evarutil.nf_evar let clos_norm_flags flgs env sigma t = try let evars ev = safe_evar_value sigma ev in - Closure.norm_val - (Closure.create_clos_infos ~evars flgs env) - (Closure.inject t) + CClosure.norm_val + (CClosure.create_clos_infos ~evars flgs env) + (CClosure.inject t) with e when is_anomaly e -> error "Tried to normalize ill-typed term" -let nf_beta = clos_norm_flags Closure.beta (Global.env ()) -let nf_betaiota = clos_norm_flags Closure.betaiota (Global.env ()) -let nf_betaiotazeta = clos_norm_flags Closure.betaiotazeta (Global.env ()) -let nf_betadeltaiota env sigma = - clos_norm_flags Closure.betadeltaiota env sigma +let nf_beta = clos_norm_flags CClosure.beta (Global.env ()) +let nf_betaiota = clos_norm_flags CClosure.betaiota (Global.env ()) +let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta (Global.env ()) +let nf_all env sigma = + clos_norm_flags CClosure.all env sigma (********************************************************************) @@ -1233,7 +1231,7 @@ let pb_equal = function let report_anomaly _ = let e = UserError ("", Pp.str "Conversion test raised an anomaly") in - let e = Errors.push e in + let e = CErrors.push e in iraise e let test_trans_conversion (f: constr Reduction.extended_conversion_function) reds env sigma x y = @@ -1397,7 +1395,7 @@ let instance sigma s c = * error message. *) let hnf_prod_app env sigma t n = - match kind_of_term (whd_betadeltaiota env sigma t) with + match kind_of_term (whd_all env sigma t) with | Prod (_,_,b) -> subst1 n b | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product") @@ -1408,7 +1406,7 @@ let hnf_prod_applist env sigma t nl = List.fold_left (hnf_prod_app env sigma) t nl let hnf_lam_app env sigma t n = - match kind_of_term (whd_betadeltaiota env sigma t) with + match kind_of_term (whd_all env sigma t) with | Lambda (_,_,b) -> subst1 n b | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction") @@ -1420,7 +1418,7 @@ let hnf_lam_applist env sigma t nl = let splay_prod env sigma = let rec decrec env m c = - let t = whd_betadeltaiota env sigma c in + let t = whd_all env sigma c in match kind_of_term t with | Prod (n,a,c0) -> decrec (push_rel (LocalAssum (n,a)) env) @@ -1431,7 +1429,7 @@ let splay_prod env sigma = let splay_lam env sigma = let rec decrec env m c = - let t = whd_betadeltaiota env sigma c in + let t = whd_all env sigma c in match kind_of_term t with | Lambda (n,a,c0) -> decrec (push_rel (LocalAssum (n,a)) env) @@ -1442,7 +1440,7 @@ let splay_lam env sigma = let splay_prod_assum env sigma = let rec prodec_rec env l c = - let t = whd_betadeltaiota_nolet env sigma c in + let t = whd_allnolet env sigma c in match kind_of_term t with | Prod (x,t,c) -> prodec_rec (push_rel (LocalAssum (x,t)) env) @@ -1452,7 +1450,7 @@ let splay_prod_assum env sigma = (Context.Rel.add (LocalDef (x,b,t)) l) c | Cast (c,_,_) -> prodec_rec env l c | _ -> - let t' = whd_betadeltaiota env sigma t in + let t' = whd_all env sigma t in if Term.eq_constr t t' then l,t else prodec_rec env l t' in @@ -1468,7 +1466,7 @@ let sort_of_arity env sigma c = snd (splay_arity env sigma c) let splay_prod_n env sigma n = let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else - match kind_of_term (whd_betadeltaiota env sigma c) with + match kind_of_term (whd_all env sigma c) with | Prod (n,a,c0) -> decrec (push_rel (LocalAssum (n,a)) env) (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0 @@ -1478,7 +1476,7 @@ let splay_prod_n env sigma n = let splay_lam_n env sigma n = let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else - match kind_of_term (whd_betadeltaiota env sigma c) with + match kind_of_term (whd_all env sigma c) with | Lambda (n,a,c0) -> decrec (push_rel (LocalAssum (n,a)) env) (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0 @@ -1487,7 +1485,7 @@ let splay_lam_n env sigma n = decrec env n Context.Rel.empty let is_sort env sigma t = - match kind_of_term (whd_betadeltaiota env sigma t) with + match kind_of_term (whd_all env sigma t) with | Sort s -> true | _ -> false @@ -1495,20 +1493,22 @@ let is_sort env sigma t = of case/fix (heuristic used by evar_conv) *) let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s = + let refold = get_refolding_in_reduction () in + let tactic_mode = false in let rec whrec csts s = - let (t, stack as s),csts' = whd_state_gen ~csts false betaiota env sigma s in + let (t, stack as s),csts' = whd_state_gen ~csts ~refold ~tactic_mode CClosure.betaiota env sigma s in match Stack.strip_app stack with |args, (Stack.Case _ :: _ as stack') -> - let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false - (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in + let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode + (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in if reducible_mind_case t_o then whrec csts_o (t_o, stack_o@stack') else s,csts' |args, (Stack.Fix _ :: _ as stack') -> - let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false - (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in + let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode + (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in if isConstruct t_o then whrec csts_o (t_o, stack_o@stack') else s,csts' |args, (Stack.Proj (n,m,p,_) :: stack'') -> - let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false - (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in + let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode + (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in if isConstruct t_o then whrec Cst_stack.empty (Stack.nth stack_o (n+m), stack'') else s,csts' @@ -1517,7 +1517,7 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s = let find_conclusion env sigma = let rec decrec env c = - let t = whd_betadeltaiota env sigma c in + let t = whd_all env sigma c in match kind_of_term t with | Prod (x,t,c0) -> decrec (push_rel (LocalAssum (x,t)) env) c0 | Lambda (x,t,c0) -> decrec (push_rel (LocalAssum (x,t)) env) c0 diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index b38252e971..4cd7a2a869 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -28,6 +28,11 @@ module ReductionBehaviour : sig val print : Globnames.global_reference -> Pp.std_ppcmds end +(** Option telling if reduction should use the refolding machinery of cbn + (off by default) *) +val get_refolding_in_reduction : unit -> bool +val set_refolding_in_reduction : bool -> unit + (** {6 Machinery about a stack of unfolded constant } cst applied to params must convertible to term of the state applied to args @@ -134,21 +139,21 @@ val stack_reduction_of_reduction : i*) val stacklam : (state -> 'a) -> constr list -> constr -> constr Stack.t -> 'a -val whd_state_gen : ?csts:Cst_stack.t -> bool -> Closure.RedFlags.reds -> - Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t +val whd_state_gen : ?csts:Cst_stack.t -> refold:bool -> tactic_mode:bool -> + CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t -val iterate_whd_gen : bool -> Closure.RedFlags.reds -> +val iterate_whd_gen : bool -> CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> Term.constr -> Term.constr (** {6 Generic Optimized Reduction Function using Closures } *) -val clos_norm_flags : Closure.RedFlags.reds -> reduction_function +val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function (** Same as [(strong whd_beta[delta][iota])], but much faster on big terms *) val nf_beta : local_reduction_function val nf_betaiota : local_reduction_function val nf_betaiotazeta : local_reduction_function -val nf_betadeltaiota : reduction_function +val nf_all : reduction_function val nf_evar : evar_map -> constr -> constr (** Lazy strategy, weak head reduction *) @@ -158,9 +163,8 @@ val whd_nored : local_reduction_function val whd_beta : local_reduction_function val whd_betaiota : local_reduction_function val whd_betaiotazeta : local_reduction_function -val whd_betadeltaiota : contextual_reduction_function -val whd_betadeltaiota_nolet : contextual_reduction_function -val whd_betaetalet : local_reduction_function +val whd_all : contextual_reduction_function +val whd_allnolet : contextual_reduction_function val whd_betalet : local_reduction_function (** Removes cast and put into applicative form *) @@ -168,18 +172,16 @@ val whd_nored_stack : local_stack_reduction_function val whd_beta_stack : local_stack_reduction_function val whd_betaiota_stack : local_stack_reduction_function val whd_betaiotazeta_stack : local_stack_reduction_function -val whd_betadeltaiota_stack : contextual_stack_reduction_function -val whd_betadeltaiota_nolet_stack : contextual_stack_reduction_function -val whd_betaetalet_stack : local_stack_reduction_function +val whd_all_stack : contextual_stack_reduction_function +val whd_allnolet_stack : contextual_stack_reduction_function val whd_betalet_stack : local_stack_reduction_function val whd_nored_state : local_state_reduction_function val whd_beta_state : local_state_reduction_function val whd_betaiota_state : local_state_reduction_function val whd_betaiotazeta_state : local_state_reduction_function -val whd_betadeltaiota_state : contextual_state_reduction_function -val whd_betadeltaiota_nolet_state : contextual_state_reduction_function -val whd_betaetalet_state : local_state_reduction_function +val whd_all_state : contextual_state_reduction_function +val whd_allnolet_state : contextual_state_reduction_function val whd_betalet_state : local_state_reduction_function (** {6 Head normal forms } *) @@ -187,18 +189,14 @@ val whd_betalet_state : local_state_reduction_function val whd_delta_stack : stack_reduction_function val whd_delta_state : state_reduction_function val whd_delta : reduction_function -val whd_betadelta_stack : stack_reduction_function -val whd_betadelta_state : state_reduction_function -val whd_betadelta : reduction_function -val whd_betadeltaeta_stack : stack_reduction_function -val whd_betadeltaeta_state : state_reduction_function -val whd_betadeltaeta : reduction_function -val whd_betadeltaiotaeta_stack : stack_reduction_function -val whd_betadeltaiotaeta_state : state_reduction_function -val whd_betadeltaiotaeta : reduction_function - -val whd_eta : constr -> constr -val whd_zeta : constr -> constr +val whd_betadeltazeta_stack : stack_reduction_function +val whd_betadeltazeta_state : state_reduction_function +val whd_betadeltazeta : reduction_function +val whd_zeta_stack : local_stack_reduction_function +val whd_zeta_state : local_state_reduction_function +val whd_zeta : local_reduction_function + +val shrink_eta : constr -> constr (** Various reduction functions *) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 1a6f7832aa..98b36fb92f 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Term open Vars @@ -62,7 +62,7 @@ let get_type_from_constraints env sigma t = let rec subst_type env sigma typ = function | [] -> typ | h::rest -> - match kind_of_term (whd_betadeltaiota env sigma typ) with + match kind_of_term (whd_all env sigma typ) with | Prod (na,c1,c2) -> subst_type env sigma (subst1 h c2) rest | _ -> retype_error NonFunctionalConstruction @@ -71,7 +71,7 @@ let rec subst_type env sigma typ = function let sort_of_atomic_type env sigma ft args = let rec concl_of_arity env n ar args = - match kind_of_term (whd_betadeltaiota env sigma ar), args with + match kind_of_term (whd_all env sigma ar), args with | Prod (na, t, b), h::l -> concl_of_arity (push_rel (LocalDef (na, lift n h, t)) env) (n + 1) b l | Sort s, [] -> s | _ -> retype_error NotASort @@ -83,7 +83,7 @@ let type_of_var env id = with Not_found -> retype_error (BadVariable id) let decomp_sort env sigma t = - match kind_of_term (whd_betadeltaiota env sigma t) with + match kind_of_term (whd_all env sigma t) with | Sort s -> s | _ -> retype_error NotASort @@ -113,7 +113,7 @@ let retype ?(polyprop=true) sigma = in let n = inductive_nrealdecls_env env (fst (fst (dest_ind_family indf))) in let t = betazetaevar_applist sigma n p realargs in - (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with + (match kind_of_term (whd_all env sigma (type_of env t)) with | Prod _ -> whd_beta sigma (applist (t, [c])) | _ -> t) | Lambda (name,c1,c2) -> diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index e4cca2679c..8ca40f829f 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -46,3 +46,5 @@ val type_of_global_reference_knowing_conclusion : val sorts_of_context : env -> evar_map -> Context.Rel.t -> sorts list val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr + +val print_retype_error : retype_error -> Pp.std_ppcmds diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 7d2504004f..820a81b5d2 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Term @@ -18,7 +18,7 @@ open Termops open Find_subterm open Namegen open Environ -open Closure +open CClosure open Reductionops open Cbv open Patternops @@ -257,7 +257,7 @@ let invert_name labs l na0 env sigma ref = function let compute_consteval_direct env sigma ref = let rec srec env n labs onlyproj c = - let c',l = whd_betadelta_stack env sigma c in + let c',l = whd_betadeltazeta_stack env sigma c in match kind_of_term c' with | Lambda (id,t,g) when List.is_empty l && not onlyproj -> let open Context.Rel.Declaration in @@ -870,7 +870,7 @@ let red_product env sigma c = *) let whd_simpl_orelse_delta_but_fix_old env sigma c = - let whd_all = whd_betadeltaiota_state env sigma in + let whd_all = whd_all_state env sigma in let rec redrec (x, stack as s) = match kind_of_term x with | Lambda (na,t,c) -> @@ -1125,7 +1125,7 @@ let cbv_norm_flags flags env sigma t = let cbv_beta = cbv_norm_flags beta empty_env let cbv_betaiota = cbv_norm_flags betaiota empty_env -let cbv_betadeltaiota env sigma = cbv_norm_flags betadeltaiota env sigma +let cbv_betadeltaiota env sigma = cbv_norm_flags all env sigma let compute = cbv_betadeltaiota @@ -1186,7 +1186,7 @@ let reduce_to_ind_gen allow_product env sigma t = | _ -> (* Last chance: we allow to bypass the Opaque flag (as it was partially the case between V5.10 and V8.1 *) - let t' = whd_betadeltaiota env sigma t in + let t' = whd_all env sigma t in match kind_of_term (fst (decompose_app t')) with | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t' l) | _ -> errorlabstrm "" (str"Not an inductive product.") diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 195b21bbf2..f8dfe1adf2 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -66,7 +66,7 @@ val pattern_occs : (occurrences * constr) list -> e_reduction_function (** Rem: Lazy strategies are defined in Reduction *) (** Call by value strategy (uses Closures) *) -val cbv_norm_flags : Closure.RedFlags.reds -> reduction_function +val cbv_norm_flags : CClosure.RedFlags.reds -> reduction_function val cbv_beta : local_reduction_function val cbv_betaiota : local_reduction_function val cbv_betadeltaiota : reduction_function diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index d57eef2e1f..b8da6b6852 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -65,7 +65,8 @@ type typeclass = { cl_props : Context.Rel.t; (* The method implementaions as projections. *) - cl_projs : (Name.t * (direction * int option) option * constant option) list; + cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option + * constant option) list; cl_strict : bool; @@ -76,10 +77,9 @@ type typeclasses = typeclass Refmap.t type instance = { is_class: global_reference; - is_pri: int option; + is_info: Vernacexpr.hint_info_expr; (* Sections where the instance should be redeclared, - -1 for discard, 0 for none, mutable to avoid redeclarations - when multiple rebuild_object happen. *) + -1 for discard, 0 for none. *) is_global: int; is_poly: bool; is_impl: global_reference; @@ -89,15 +89,15 @@ type instances = (instance Refmap.t) Refmap.t let instance_impl is = is.is_impl -let instance_priority is = is.is_pri +let hint_priority is = is.is_info.Vernacexpr.hint_priority -let new_instance cl pri glob poly impl = +let new_instance cl info glob poly impl = let global = if glob then Lib.sections_depth () else -1 in { is_class = cl.cl_impl; - is_pri = pri ; + is_info = info ; is_global = global ; is_poly = poly; is_impl = impl } @@ -150,7 +150,7 @@ let dest_class_arity env c = let class_of_constr c = try Some (dest_class_arity (Global.env ()) c) - with e when Errors.noncritical e -> None + with e when CErrors.noncritical e -> None let is_class_constr c = try let gr, u = Universes.global_of_constr c in @@ -249,7 +249,7 @@ let rebuild_class cl = try let cst = Tacred.evaluable_of_global_reference (Global.env ()) cl.cl_impl in set_typeclass_transparency cst false false; cl - with e when Errors.noncritical e -> cl + with e when CErrors.noncritical e -> cl let class_input : typeclass -> obj = declare_object @@ -272,9 +272,11 @@ let check_instance env sigma c = let (evd, c) = resolve_one_typeclass env sigma (Retyping.get_type_of env sigma c) in not (Evd.has_undefined evd) - with e when Errors.noncritical e -> false + with e when CErrors.noncritical e -> false -let build_subclasses ~check env sigma glob pri = +open Vernacexpr + +let build_subclasses ~check env sigma glob { hint_priority = pri } = let _id = Nametab.basename_of_global glob in let _next_id = let i = ref (-1) in @@ -297,24 +299,24 @@ let build_subclasses ~check env sigma glob pri = match b with | None -> None | Some (Backward, _) -> None - | Some (Forward, pri') -> + | Some (Forward, info) -> let proj = Option.get proj in let body = it_mkLambda_or_LetIn (mkApp (mkConstU (proj,u), projargs)) rels in if check && check_instance env sigma body then None else - let pri = - match pri, pri' with + let newpri = + match pri, info.hint_priority with | Some p, Some p' -> Some (p + p') | Some p, None -> Some (p + 1) | _, _ -> None in - Some (ConstRef proj, pri, body)) tc.cl_projs + Some (ConstRef proj, { info with hint_priority = newpri }, body)) tc.cl_projs in - let declare_proj hints (cref, pri, body) = + let declare_proj hints (cref, info, body) = let path' = cref :: path in let ty = Retyping.get_type_of env sigma body in let rest = aux pri body ty path' in - hints @ (path', pri, body) :: rest + hints @ (path', info, body) :: rest in List.fold_left declare_proj [] projs in let term = Universes.constr_of_global_univ (glob,Univ.UContext.instance ctx) in @@ -368,11 +370,11 @@ let is_local i = Int.equal i.is_global (-1) let add_instance check inst = let poly = Global.is_polymorphic inst.is_impl in add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] (is_local inst) - inst.is_pri poly; + inst.is_info poly; List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path (is_local inst) pri poly) (build_subclasses ~check:(check && not (isVarRef inst.is_impl)) - (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_pri) + (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info) let rebuild_instance (action, inst) = let () = match action with @@ -404,26 +406,22 @@ let remove_instance i = Lib.add_anonymous_leaf (instance_input (RemoveInstance, i)); remove_instance_hint i.is_impl -let declare_instance pri local glob = +let declare_instance info local glob = let ty = Global.type_of_global_unsafe glob in + let info = Option.default {hint_priority = None; hint_pattern = None} info in match class_of_constr ty with | Some (rels, ((tc,_), args) as _cl) -> - add_instance (new_instance tc pri (not local) (Flags.use_polymorphic_flag ()) glob) -(* let path, hints = build_subclasses (not local) (Global.env ()) Evd.empty glob in *) -(* let entries = List.map (fun (path, pri, c) -> (pri, local, path, c)) hints in *) -(* Auto.add_hints local [typeclasses_db] (Auto.HintsResolveEntry entries); *) -(* Auto.add_hints local [typeclasses_db] *) -(* (Auto.HintsCutEntry (PathSeq (PathStar (PathAtom PathAny), path))) *) + add_instance (new_instance tc info (not local) (Flags.use_polymorphic_flag ()) glob) | None -> () let add_class cl = add_class cl; List.iter (fun (n, inst, body) -> match inst with - | Some (Backward, pri) -> + | Some (Backward, info) -> (match body with - | None -> Errors.error "Non-definable projection can not be declared as a subinstance" - | Some b -> declare_instance pri false (ConstRef b)) + | None -> CErrors.error "Non-definable projection can not be declared as a subinstance" + | Some b -> declare_instance (Some info) false (ConstRef b)) | _ -> ()) cl.cl_projs @@ -501,7 +499,7 @@ let is_resolvable evi = Option.is_empty (Store.get evi.evar_extra resolvable) let mark_resolvability_undef b evi = - if is_resolvable evi = b then evi + if is_resolvable evi == (b : bool) then evi else let t = set_resolvable evi.evar_extra b in { evi with evar_extra = t } @@ -548,7 +546,7 @@ let solve_all_instances env evd filter unique split fail = (* let solve_classeskey = Profile.declare_profile "solve_typeclasses" *) (* let solve_problem = Profile.profile5 solve_classeskey solve_problem *) -let resolve_typeclasses ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ()) +let resolve_typeclasses ?(fast_path = true) ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ()) ?(split=true) ?(fail=true) env evd = - if not (has_typeclasses filter evd) then evd + if fast_path && not (has_typeclasses filter evd) then evd else solve_all_instances env evd filter unique split fail diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 25460ef7d3..620bc367bd 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -32,7 +32,7 @@ type typeclass = { Some may be undefinable due to sorting restrictions or simply undefined if no name is provided. The [int option option] indicates subclasses whose hint has the given priority. *) - cl_projs : (Name.t * (direction * int option) option * constant option) list; + cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option * constant option) list; (** Whether we use matching or full unification during resolution *) cl_strict : bool; @@ -50,7 +50,7 @@ val all_instances : unit -> instance list val add_class : typeclass -> unit -val new_instance : typeclass -> int option -> bool -> Decl_kinds.polymorphic -> +val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> Decl_kinds.polymorphic -> global_reference -> instance val add_instance : instance -> unit val remove_instance : instance -> unit @@ -71,7 +71,7 @@ val class_of_constr : constr -> (Context.Rel.t * (typeclass puniverses * constr val instance_impl : instance -> global_reference -val instance_priority : instance -> int option +val hint_priority : instance -> int option val is_class : global_reference -> bool val is_instance : global_reference -> bool @@ -101,7 +101,7 @@ val mark_resolvable : evar_info -> evar_info val is_class_evar : evar_map -> evar_info -> bool val is_class_type : evar_map -> types -> bool -val resolve_typeclasses : ?filter:evar_filter -> ?unique:bool -> +val resolve_typeclasses : ?fast_path:bool -> ?filter:evar_filter -> ?unique:bool -> ?split:bool -> ?fail:bool -> env -> evar_map -> evar_map val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> types -> open_constr @@ -113,21 +113,22 @@ val classes_transparent_state : unit -> transparent_state val add_instance_hint_hook : (global_reference_or_constr -> global_reference list -> - bool (* local? *) -> int option -> Decl_kinds.polymorphic -> unit) Hook.t + bool (* local? *) -> Vernacexpr.hint_info_expr -> Decl_kinds.polymorphic -> unit) Hook.t val remove_instance_hint_hook : (global_reference -> unit) Hook.t val add_instance_hint : global_reference_or_constr -> global_reference list -> - bool -> int option -> Decl_kinds.polymorphic -> unit + bool -> Vernacexpr.hint_info_expr -> Decl_kinds.polymorphic -> unit val remove_instance_hint : global_reference -> unit val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t val solve_one_instance_hook : (env -> evar_map -> types -> bool -> open_constr) Hook.t -val declare_instance : int option -> bool -> global_reference -> unit +val declare_instance : Vernacexpr.hint_info_expr option -> bool -> global_reference -> unit (** Build the subinstances hints for a given typeclass object. check tells if we should check for existence of the subinstances and add only the missing ones. *) -val build_subclasses : check:bool -> env -> evar_map -> global_reference -> int option (* priority *) -> - (global_reference list * int option * constr) list +val build_subclasses : check:bool -> env -> evar_map -> global_reference -> + Vernacexpr.hint_info_expr -> + (global_reference list * Vernacexpr.hint_info_expr * constr) list diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 52afa7f83a..9e9997f73c 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Term open Vars @@ -36,7 +36,7 @@ let inductive_type_knowing_parameters env (ind,u) jl = Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp let e_type_judgment env evdref j = - match kind_of_term (whd_betadeltaiota env !evdref j.uj_type) with + match kind_of_term (whd_all env !evdref j.uj_type) with | Sort s -> {utj_val = j.uj_val; utj_type = s } | Evar ev -> let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in @@ -54,7 +54,7 @@ let e_judge_of_apply env evdref funj argjv = { uj_val = mkApp (j_val funj, Array.map j_val argjv); uj_type = typ } | hj::restjl -> - match kind_of_term (whd_betadeltaiota env !evdref typ) with + match kind_of_term (whd_all env !evdref typ) with | Prod (_,c1,c2) -> if Evarconv.e_cumul env evdref hj.uj_type c1 then apply_rec (n+1) (subst1 hj.uj_val c2) restjl @@ -87,7 +87,7 @@ let e_is_correct_arity env evdref c pj ind specif params = let allowed_sorts = elim_sorts specif in let error () = error_elim_arity env ind allowed_sorts c pj None in let rec srec env pt ar = - let pt' = whd_betadeltaiota env !evdref pt in + let pt' = whd_all env !evdref pt in match kind_of_term pt', ar with | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' -> if not (Evarconv.e_cumul env evdref a1 a1') then error (); @@ -110,22 +110,32 @@ let e_type_case_branches env evdref (ind,largs) pj c = let nparams = inductive_params specif in let (params,realargs) = List.chop nparams largs in let p = pj.uj_val in - let univ = e_is_correct_arity env evdref c pj ind specif params in + let () = e_is_correct_arity env evdref c pj ind specif params in let lc = build_branches_type ind specif params p in let n = (snd specif).Declarations.mind_nrealdecls in let ty = whd_betaiota !evdref (lambda_applist_assum (n+1) p (realargs@[c])) in - (lc, ty, univ) + (lc, ty) let e_judge_of_case env evdref ci pj cj lfj = let indspec = try find_mrectype env !evdref cj.uj_type with Not_found -> error_case_not_inductive env cj in let _ = check_case_info env (fst indspec) ci in - let (bty,rslty,univ) = e_type_case_branches env evdref indspec pj cj.uj_val in + let (bty,rslty) = e_type_case_branches env evdref indspec pj cj.uj_val in e_check_branch_types env evdref (fst indspec) cj (lfj,bty); { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); uj_type = rslty } +let check_type_fixpoint loc env evdref lna lar vdefj = + let lt = Array.length vdefj in + if Int.equal (Array.length lar) lt then + for i = 0 to lt-1 do + if not (Evarconv.e_cumul env evdref (vdefj.(i)).uj_type + (lift lt lar.(i))) then + Pretype_errors.error_ill_typed_rec_body_loc loc env !evdref + i lna vdefj lar + done + (* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = let pj = Retyping.get_judgment_of env sigma p in @@ -263,7 +273,7 @@ and execute_recdef env evdref (names,lar,vdef) = let env1 = push_rec_types (names,lara,vdef) env in let vdefj = execute_array env1 evdref vdef in let vdefv = Array.map j_val vdefj in - let _ = type_fixpoint env1 names lara vdefj in + let _ = check_type_fixpoint Loc.ghost env1 evdref names lara vdefj in (names,lara,vdefv) and execute_array env evdref = Array.map (execute env evdref) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index e524edcca8..04e5e40bc2 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -39,3 +39,8 @@ val e_solve_evars : env -> evar_map ref -> constr -> constr (** (first constr is term to match, second is return predicate) *) val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr -> unit + +(** Raise an error message if bodies have types not unifiable with the + expected ones *) +val check_type_fixpoint : Loc.t -> env -> evar_map ref -> + Names.Name.t array -> types array -> unsafe_judgment array -> unit diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 21cf5548f2..259318693f 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Pp open Util open Names @@ -460,7 +460,7 @@ let use_metas_pattern_unification flags nb l = Array.for_all (fun c -> isRel c && destRel c <= nb) l type key = - | IsKey of Closure.table_key + | IsKey of CClosure.table_key | IsProj of projection * constr let expand_table_key env = function @@ -479,8 +479,8 @@ let unfold_projection env p stk = let expand_key ts env sigma = function | Some (IsKey k) -> expand_table_key env k | Some (IsProj (p, c)) -> - let red = Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma - Cst_stack.empty (c, unfold_projection env p []))) + let red = Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma + Cst_stack.empty (c, unfold_projection env p []))) in if Term.eq_constr (mkProj (p, c)) red then None else Some red | None -> None @@ -572,7 +572,8 @@ let constr_cmp pb sigma flags t u = else sigma, b let do_reduce ts (env, nb) sigma c = - Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma Cst_stack.empty (c, Stack.empty))) + Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state + ts env sigma Cst_stack.empty (c, Stack.empty))) let use_full_betaiota flags = flags.modulo_betaiota && Flags.version_strictly_greater Flags.V8_3 @@ -742,7 +743,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb then Evd.set_leq_sort curenv sigma s1 s2 else Evd.set_eq_sort curenv sigma s1 s2 in (sigma', metasubst, evarsubst) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> error_cannot_unify curenv sigma (m,n)) | Lambda (na,t1,c1), Lambda (_,t2,c2) -> @@ -1080,8 +1081,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb if !debug_unification then Feedback.msg_debug (str "Leaving unification with success"); a with e -> + let e = CErrors.push e in if !debug_unification then Feedback.msg_debug (str "Leaving unification with failure"); - raise e + iraise e let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env @@ -1090,7 +1092,7 @@ let left = true let right = false let rec unify_with_eta keptside flags env sigma c1 c2 = -(* Question: try whd_betadeltaiota on ci if not two lambdas? *) +(* Question: try whd_all on ci if not two lambdas? *) match kind_of_term c1, kind_of_term c2 with | (Lambda (na,t1,c1'), Lambda (_,t2,c2')) -> let env' = push_rel_assum (na,t1) env in @@ -1138,11 +1140,11 @@ let merge_instances env sigma flags st1 st2 c1 c2 = else (right, st2, res) | (IsSuperType,IsSubType) -> (try (left, IsSubType, unify_0 env sigma CUMUL flags c2 c1) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> (right, IsSubType, unify_0 env sigma CUMUL flags c1 c2)) | (IsSubType,IsSuperType) -> (try (left, IsSuperType, unify_0 env sigma CUMUL flags c1 c2) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> (right, IsSuperType, unify_0 env sigma CUMUL flags c2 c1)) (* Unification @@ -1200,7 +1202,7 @@ let applyHead env (type r) (evd : r Sigma.t) n c = if Int.equal n 0 then Sigma (c, evd, p) else - match kind_of_term (whd_betadeltaiota env (Sigma.to_evar_map evd) cty) with + match kind_of_term (whd_all env (Sigma.to_evar_map evd) cty) with | Prod (_,c1,c2) -> let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd' @@ -1210,15 +1212,15 @@ let applyHead env (type r) (evd : r Sigma.t) n c = let is_mimick_head ts f = match kind_of_term f with - | Const (c,u) -> not (Closure.is_transparent_constant ts c) - | Var id -> not (Closure.is_transparent_variable ts id) + | Const (c,u) -> not (CClosure.is_transparent_constant ts c) + | Var id -> not (CClosure.is_transparent_variable ts id) | (Rel _|Construct _|Ind _) -> true | _ -> false let try_to_coerce env evd c cty tycon = let j = make_judge c cty in let (evd',j') = inh_conv_coerce_rigid_to true Loc.ghost env evd j tycon in - let evd' = Evarconv.consider_remaining_unif_problems env evd' in + let evd' = Evarconv.solve_unif_constraints_with_heuristics env evd' in let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in (evd',j'.uj_val) @@ -1268,7 +1270,11 @@ let solve_simple_evar_eqn ts env evd ev rhs = | UnifFailure (evd,reason) -> error_cannot_unify env evd ~reason (mkEvar ev,rhs); | Success evd -> - Evarconv.consider_remaining_unif_problems env evd + if Flags.version_less_or_equal Flags.V8_5 then + (* We used to force solving unrelated problems at arbitrary times *) + Evarconv.solve_unif_constraints_with_heuristics env evd + else (* solve_simple_eqn calls reconsider_unif_constraints itself *) + evd (* [w_merge env sigma b metas evars] merges common instances in metas or in evars, possibly generating new unification problems; if [b] @@ -1295,7 +1301,6 @@ let w_merge env with_types flags (evd,metas,evars) = if is_mimick_head flags.modulo_delta f then let evd' = mimick_undefined_evar evd flags f (Array.length cl) evk in - (* let evd' = Evarconv.consider_remaining_unif_problems env evd' in *) w_merge_rec evd' metas evars eqns else let evd' = @@ -1343,7 +1348,7 @@ let w_merge env with_types flags (evd,metas,evars) = else let evd' = if occur_meta_evd evd mv c then - if isMetaOf mv (whd_betadeltaiota env evd c) then evd + if isMetaOf mv (whd_all env evd c) then evd else error_cannot_unify env evd (mkMeta mv,c) else meta_assign mv (c,(status,TypeProcessed)) evd in @@ -1353,7 +1358,7 @@ let w_merge env with_types flags (evd,metas,evars) = let rec process_eqns failures = function | (mv,status,c)::eqns -> (match (try Inl (unify_type env evd flags mv status c) - with e when Errors.noncritical e -> Inr e) + with e when CErrors.noncritical e -> Inr e) with | Inr e -> process_eqns (((mv,status,c),e)::failures) eqns | Inl (evd,metas,evars) -> @@ -1387,10 +1392,11 @@ let w_merge env with_types flags (evd,metas,evars) = in w_merge_rec evd [] [] eqns in let res = (* merge constraints *) - w_merge_rec evd (order_metas metas) (List.rev evars) [] + w_merge_rec evd (order_metas metas) + (* Assign evars in the order of assignments during unification *) + (List.rev evars) [] in - if with_types then check_types res - else res + if with_types then check_types res else res let w_unify_meta_types env ?(flags=default_unify_flags ()) evd = let metas,evd = retract_coercible_metas evd in @@ -1448,7 +1454,7 @@ let w_typed_unify_array env evd flags f1 l1 f2 l2 = let subst = Array.fold_left2 fold_subst subst l1 l2 in let evd = w_merge env true flags.merge_unify_flags subst in try_resolve_typeclasses env evd flags.resolve_evars - (mkApp(f1,l1)) (mkApp(f2,l2)) + (mkApp(f1,l1)) (mkApp(f2,l2)) (* takes a substitution s, an open term op and a closed term cl try to find a subterm of cl which matches op, if op is just a Meta @@ -1555,7 +1561,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = | PretypeError (_,_,CannotUnify (c1,c2,Some e)) -> raise (NotUnifiable (Some (c1,c2,e))) (** MS: This is pretty bad, it catches Not_found for example *) - | e when Errors.noncritical e -> raise (NotUnifiable None) in + | e when CErrors.noncritical e -> raise (NotUnifiable None) in let merge_fun c1 c2 = match c1, c2 with | Some (evd,c1,x), Some (_,c2,_) -> @@ -1585,7 +1591,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = let x = id_of_name_using_hdchar (Global.env()) t name in let ids = ids_of_named_context (named_context env) in if name == Anonymous then next_ident_away_in_goal x ids else - if mem_named_context x (named_context env) then + if mem_named_context_val x (named_context_val env) then errorlabstrm "Unification.make_abstraction_core" (str "The variable " ++ Nameops.pr_id x ++ str " is already declared.") else @@ -1597,14 +1603,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = let hyp = get_id d in match occurrences_of_hyp hyp occs with | NoOccurrences, InHyp -> - if indirectly_dependent c d depdecls then - (* Told explicitly not to abstract over [d], but it is dependent *) - let id' = indirect_dependency d depdecls in - errorlabstrm "" (str "Cannot abstract over " ++ Nameops.pr_id id' - ++ str " without also abstracting or erasing " ++ Nameops.pr_id hyp - ++ str ".") - else - (push_named_context_val d sign,depdecls) + (push_named_context_val d sign,depdecls) | AllOccurrences, InHyp as occ -> let occ = if likefirst then LikeFirst else AtOccs occ in let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in @@ -1884,21 +1883,14 @@ let secondOrderAbstraction env evd flags typ (p, oplist) = error_wrong_abstraction_type env evd' (Evd.meta_name evd p) pred typp predtyp; w_merge env false flags.merge_unify_flags - (evd',[p,pred,(Conv,TypeProcessed)],[]) - - (* let evd',metas,evars = *) - (* try unify_0 env evd' CUMUL flags predtyp typp *) - (* with NotConvertible -> *) - (* error_wrong_abstraction_type env evd *) - (* (Evd.meta_name evd p) pred typp predtyp *) - (* in *) - (* w_merge env false flags (evd',(p,pred,(Conv,TypeProcessed))::metas,evars) *) + (evd',[p,pred,(Conv,TypeProcessed)],[]) let secondOrderDependentAbstraction env evd flags typ (p, oplist) = let typp = Typing.meta_type evd p in let evd, pred = abstract_list_all_with_dependencies env evd typp typ oplist in w_merge env false flags.merge_unify_flags - (evd,[p,pred,(Conv,TypeProcessed)],[]) + (evd,[p,pred,(Conv,TypeProcessed)],[]) + let secondOrderAbstractionAlgo dep = if dep then secondOrderDependentAbstraction else secondOrderAbstraction diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 7ea9b90635..e281f22df6 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -24,7 +24,7 @@ open Context.Rel.Declaration let crazy_type = mkSet let decompose_prod env t = - let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in + let (name,dom,codom as res) = destProd (whd_all env t) in match name with | Anonymous -> (Name (Id.of_string "x"), dom, codom) | Name _ -> res @@ -46,7 +46,11 @@ let invert_tag cst tag reloc_tbl = with Find_at j -> (j+1) (* Argggg, ces constructeurs de ... qui commencent a 1*) -let find_rectype_a env c = Inductiveops.find_mrectype_vect env Evd.empty c +let find_rectype_a env c = + let (t, l) = decompose_appvect (whd_all env c) in + match kind_of_term t with + | Ind ind -> (ind, l) + | _ -> assert false (* Instantiate inductives and parameters in constructor type *) @@ -234,7 +238,7 @@ and nf_stk ?from:(from=0) env c t stk = let params,realargs = Util.Array.chop nparams allargs in let pT = hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in - let pT = whd_betadeltaiota env pT in + let pT = whd_all env pT in let dep, p = nf_predicate env (ind,u) mip params (type_of_switch sw) pT in (* Calcul du type des branches *) let btypes = build_branches_type env ind mib mip u params dep p in @@ -305,7 +309,7 @@ and nf_fun env f typ = try decompose_prod env typ with DestKO -> (* 27/2/13: Turned this into an anomaly *) - Errors.anomaly + CErrors.anomaly (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") in let body = nf_val (push_rel (LocalAssum (name,dom)) env) vb codom in |