diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 68 | ||||
| -rw-r--r-- | proofs/clenv.mli | 8 | ||||
| -rw-r--r-- | proofs/logic.ml | 35 | ||||
| -rw-r--r-- | proofs/proof_bullet.ml | 2 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 2 |
5 files changed, 65 insertions, 50 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 387f0f6f5f..44d3b44077 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -37,15 +37,28 @@ type clausenv = { env : env; evd : evar_map; templval : constr freelisted; - templtyp : constr freelisted } + templtyp : constr freelisted; + cache : Reductionops.meta_instance_subst; +} + +let mk_clausenv env evd templval templtyp = { + env; evd; templval; templtyp; cache = create_meta_instance_subst evd; +} + +let update_clenv_evd clenv evd = + mk_clausenv clenv.env evd clenv.templval clenv.templtyp let cl_env ce = ce.env let cl_sigma ce = ce.evd -let clenv_term clenv c = meta_instance clenv.env clenv.evd c -let clenv_meta_type clenv mv = Typing.meta_type clenv.env clenv.evd mv -let clenv_value clenv = meta_instance clenv.env clenv.evd clenv.templval -let clenv_type clenv = meta_instance clenv.env clenv.evd clenv.templtyp +let clenv_term clenv c = meta_instance clenv.env clenv.cache c +let clenv_meta_type clenv mv = + let ty = + try Evd.meta_ftype clenv.evd mv + with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in + meta_instance clenv.env clenv.cache ty +let clenv_value clenv = meta_instance clenv.env clenv.cache clenv.templval +let clenv_type clenv = meta_instance clenv.env clenv.cache clenv.templtyp let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t @@ -67,7 +80,8 @@ let clenv_push_prod cl = { templval = mk_freelisted def; templtyp = mk_freelisted concl; evd = e'; - env = cl.env } + env = cl.env; + cache = create_meta_instance_subst e' } | _ -> raise NotExtensibleClause in clrec typ @@ -109,7 +123,8 @@ let mk_clenv_from_env env sigma n (c,cty) = { templval = mk_freelisted (applist (c,args)); templtyp = mk_freelisted concl; evd = evd; - env = env } + env = env; + cache = create_meta_instance_subst evd } let mk_clenv_from_n gls n (c,cty) = let env = Proofview.Goal.env gls in @@ -158,7 +173,7 @@ let clenv_assign mv rhs clenv = clenv else let st = (Conv,TypeNotProcessed) in - {clenv with evd = meta_assign mv (rhs_fls.rebus,st) clenv.evd} + update_clenv_evd clenv (meta_assign mv (rhs_fls.rebus,st) clenv.evd) with Not_found -> user_err Pp.(str "clenv_assign: undefined meta") @@ -202,19 +217,19 @@ let clenv_assign mv rhs clenv = In any case, we respect the order given in A. *) -let clenv_metas_in_type_of_meta env evd mv = - (mk_freelisted (meta_instance env evd (meta_ftype evd mv))).freemetas +let clenv_metas_in_type_of_meta clenv mv = + (mk_freelisted (meta_instance clenv.env clenv.cache (meta_ftype clenv.evd mv))).freemetas let dependent_in_type_of_metas clenv mvs = List.fold_right - (fun mv -> Metaset.union (clenv_metas_in_type_of_meta clenv.env clenv.evd mv)) + (fun mv -> Metaset.union (clenv_metas_in_type_of_meta clenv mv)) mvs Metaset.empty let dependent_closure clenv mvs = let rec aux mvs acc = Metaset.fold (fun mv deps -> - let metas_of_meta_type = clenv_metas_in_type_of_meta clenv.env clenv.evd mv in + let metas_of_meta_type = clenv_metas_in_type_of_meta clenv mv in aux metas_of_meta_type (Metaset.union deps metas_of_meta_type)) mvs acc in aux mvs mvs @@ -253,7 +268,7 @@ let meta_reducible_instance env evd b = let rec irec u = let u = whd_betaiota env Evd.empty u (* FIXME *) in match EConstr.kind evd u with - | Case (ci,p,iv,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) -> + | Case (ci,u,pms,p,iv,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) -> let m = destMeta evd (strip_outer_cast evd c) in (match try @@ -262,8 +277,10 @@ let meta_reducible_instance env evd b = if isConstruct evd g || not is_coerce then Some g else None with Not_found -> None with - | Some g -> irec (mkCase (ci,p,iv,g,bl)) - | None -> mkCase (ci,irec p,iv,c,Array.map irec bl)) + | Some g -> irec (mkCase (ci,u,pms,p,iv,g,bl)) + | None -> + let on_ctx (na, c) = (na, irec c) in + mkCase (ci,u,Array.map irec pms,on_ctx p,iv,c,Array.map on_ctx bl)) | App (f,l) when EConstr.isMeta evd (strip_outer_cast evd f) -> let m = destMeta evd (strip_outer_cast evd f) in (match @@ -297,11 +314,10 @@ let meta_reducible_instance env evd b = else irec b.rebus let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv = - { clenv with - evd = w_unify ~flags clenv.env clenv.evd cv_pb t1 t2 } + update_clenv_evd clenv (w_unify ~flags clenv.env clenv.evd cv_pb t1 t2) let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv = - { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd } + update_clenv_evd clenv (w_unify_meta_types ~flags:flags clenv.env clenv.evd) let clenv_unique_resolver_gen ?(flags=default_unify_flags ()) clenv concl = if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.env clenv.evd clenv.templtyp.rebus))) then @@ -414,11 +430,13 @@ let fchain_flags () = let clenv_fchain ?with_univs ?(flags=fchain_flags ()) mv clenv nextclenv = (* Add the metavars of [nextclenv] to [clenv], with their name-environment *) + let evd = meta_merge ?with_univs nextclenv.evd clenv.evd in let clenv' = { templval = clenv.templval; templtyp = clenv.templtyp; - evd = meta_merge ?with_univs nextclenv.evd clenv.evd; - env = nextclenv.env } in + evd; + env = nextclenv.env; + cache = create_meta_instance_subst evd } in (* unify the type of the template of [nextclenv] with the type of [mv] *) let clenv'' = clenv_unify ~flags CUMUL @@ -538,7 +556,7 @@ let clenv_assign_binding clenv k c = let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in let c_typ = nf_betaiota clenv.env clenv.evd (clenv_get_type_of clenv c) in let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in - { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd } + update_clenv_evd clenv' (meta_assign k (c,(Conv,status)) clenv'.evd) let clenv_match_args bl clenv = if List.is_empty bl then @@ -611,8 +629,10 @@ let clenv_cast_meta clenv = else mkCast (mkMeta mv, DEFAULTcast, b) with Not_found -> u) | App(f,args) -> mkApp (crec_hd f, Array.map crec args) - | Case(ci,p,iv,c,br) -> - mkCase (ci, crec_hd p, map_invert crec_hd iv, crec_hd c, Array.map crec br) + | Case(ci,u,pms,p,iv,c,br) -> + (* FIXME: we only change c because [p] is always a lambda and [br] is + most of the time??? *) + mkCase (ci, u, pms, p, iv, crec_hd c, br) | Proj (p, c) -> mkProj (p, crec_hd c) | _ -> u in @@ -640,7 +660,7 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = Typeclasses.make_unresolvables (fun x -> true) evd' else clenv.evd in - let clenv = { clenv with evd = evd' } in + let clenv = update_clenv_evd clenv evd' in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS (Evd.clear_metas evd')) (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv)))) diff --git a/proofs/clenv.mli b/proofs/clenv.mli index a72c8c5e1f..6e472da452 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -22,14 +22,18 @@ open Tactypes (** {6 The Type of Constructions clausale environments.} *) -type clausenv = { +type clausenv = private { env : env; (** the typing context *) evd : evar_map; (** the mapping from metavar and evar numbers to their types and values *) templval : constr freelisted; (** the template which we are trying to fill out *) - templtyp : constr freelisted (** its type *)} + templtyp : constr freelisted; (** its type *) + cache : Reductionops.meta_instance_subst; (* Reductionops.create_meta_instance_subst evd) *) +} +val mk_clausenv : env -> evar_map -> constr freelisted -> types freelisted -> clausenv +val update_clenv_evd : clausenv -> evar_map -> clausenv (** subject of clenv (instantiated) *) val clenv_value : clausenv -> constr diff --git a/proofs/logic.ml b/proofs/logic.ml index f159395177..8b31c07f5e 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -265,15 +265,12 @@ let collect_meta_variables c = let rec collrec deep acc c = match kind c with | Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc | Cast(c,_,_) -> collrec deep acc c - | Case(ci,p,iv,c,br) -> - (* Hack assuming only two situations: the legacy one that branches, - if with Metas, are Meta, and the new one with eta-let-expanded - branches *) - let br = Array.map2 (fun n b -> try snd (Term.decompose_lam_n_decls n b) with UserError _ -> b) ci.ci_cstr_ndecls br in - let acc = Constr.fold (collrec deep) acc p in + | Case(ci,u,pms,p,iv,c,br) -> + let acc = Array.fold_left (collrec deep) acc pms in + let acc = Constr.fold (collrec deep) acc (snd p) in let acc = Constr.fold_invert (collrec deep) acc iv in let acc = Constr.fold (collrec deep) acc c in - Array.fold_left (collrec deep) acc br + Array.fold_left (fun accu (_, br) -> collrec deep accu br) acc br | App _ -> Constr.fold (collrec deep) acc c | Proj (_, c) -> collrec deep acc c | _ -> Constr.fold (collrec true) acc c @@ -369,15 +366,16 @@ let rec mk_refgoals ~check env sigma goalacc conclty trm = let ty = EConstr.Unsafe.to_constr ty in (acc',ty,sigma,c) - | Case (ci,p,iv,c,lf) -> + | Case (ci, u, pms, p, iv, c, lf) -> (* XXX Is ignoring iv OK? *) + let (ci, p, iv, c, lf) = Inductive.expand_case env (ci, u, pms, p, iv, c, lf) in let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals ~check env sigma goalacc p c in let sigma = check_conv_leq_goal ~check env sigma trm conclty' conclty in let (acc'',sigma,rbranches) = treat_case ~check env sigma ci lbrty lf acc' in let lf' = Array.rev_of_list rbranches in let ans = if p' == p && c' == c && Array.equal (==) lf' lf then trm - else mkCase (ci,p',iv,c',lf') + else mkCase (Inductive.contract_case env (ci,p',iv,c',lf')) in (acc'',conclty',sigma, ans) @@ -418,14 +416,15 @@ and mk_hdgoals ~check env sigma goalacc trm = let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in (acc'',conclty',sigma, ans) - | Case (ci,p,iv,c,lf) -> + | Case (ci, u, pms, p, iv, c, lf) -> (* XXX is ignoring iv OK? *) + let (ci, p, iv, c, lf) = Inductive.expand_case env (ci, u, pms, p, iv, c, lf) in let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals ~check env sigma goalacc p c in let (acc'',sigma,rbranches) = treat_case ~check env sigma ci lbrty lf acc' in let lf' = Array.rev_of_list rbranches in let ans = if p' == p && c' == c && Array.equal (==) lf' lf then trm - else mkCase (ci,p',iv,c',lf') + else mkCase (Inductive.contract_case env (ci,p',iv,c',lf')) in (acc'',conclty',sigma, ans) @@ -479,13 +478,7 @@ and treat_case ~check env sigma ci lbrty lf acc' = | App (f,cl) -> (f, cl) | _ -> (c,[||]) in Array.fold_left3 - (fun (lacc,sigma,bacc) ty fi l -> - if isMeta (strip_outer_cast fi) then - (* Support for non-eta-let-expanded Meta as found in *) - (* destruct/case with an non eta-let expanded elimination scheme *) - let (r,_,s,fi') = mk_refgoals ~check env sigma lacc ty fi in - r,s,(fi'::bacc) - else + (fun (lacc,sigma,bacc) ty fi n -> (* Deal with a branch in expanded form of the form Case(ci,p,c,[|eta-let-exp(Meta);...;eta-let-exp(Meta)|]) as if it were not so, so as to preserve compatibility with when @@ -494,7 +487,6 @@ and treat_case ~check env sigma ci lbrty lf acc' = CAUTION: it does not deal with the general case of eta-zeta reduced branches having a form different from Meta, as it would be theoretically the case with third-party code *) - let n = List.length l in let ctx, body = Term.decompose_lam_n_decls n fi in let head, args = decompose_app_vect body in (* Strip cast because clenv_cast_meta adds a cast when the branch is @@ -503,8 +495,7 @@ and treat_case ~check env sigma ci lbrty lf acc' = let head = strip_outer_cast head in if isMeta head then begin assert (args = Context.Rel.to_extended_vect mkRel 0 ctx); - let head' = lift (-n) head in - let (r,_,s,head'') = mk_refgoals ~check env sigma lacc ty head' in + let (r,_,s,head'') = mk_refgoals ~check env sigma lacc ty head in let fi' = it_mkLambda_or_LetIn (mkApp (head'',args)) ctx in (r,s,fi'::bacc) end @@ -513,7 +504,7 @@ and treat_case ~check env sigma ci lbrty lf acc' = let sigma, t'ty = goal_type_of ~check env sigma fi in let sigma = check_conv_leq_goal ~check env sigma fi t'ty ty in (lacc,sigma,fi::bacc)) - (acc',sigma,[]) lbrty lf ci.ci_pp_info.cstr_tags + (acc',sigma,[]) lbrty lf ci.ci_cstr_ndecls let convert_hyp ~check ~reorder env sigma d = let id = NamedDecl.get_id d in diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index 41cb7399da..dc5a1b0ac2 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -68,7 +68,7 @@ module Strict = struct match sugg with | NeedClosingBrace -> Pp.(str"Try unfocusing with \"}\".") | NoBulletInUse -> assert false (* This should never raise an error. *) - | ProofFinished -> Pp.(str"No more subgoals.") + | ProofFinished -> Pp.(str"No more goals.") | Suggest b -> Pp.(str"Expecting " ++ pr_bullet b ++ str".") | Unfinished b -> Pp.(str"Current bullet " ++ pr_bullet b ++ str" is not finished.") diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 08f88d46c1..6a6dd783e4 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -69,7 +69,7 @@ val pf_reduce_to_atomic_ind : Goal.goal sigma -> types -> (inductive * EInst [@@ocaml.deprecated "Use Tacred.pf_reduce_to_atomic_ind"] val pf_compute : Goal.goal sigma -> constr -> constr [@@ocaml.deprecated "Use the version in Tacmach.New"] -val pf_unfoldn : (occurrences * evaluable_global_reference) list +val pf_unfoldn : (occurrences * Tacred.evaluable_global_reference) list -> Goal.goal sigma -> constr -> constr [@@ocaml.deprecated "Use Tacred.unfoldn"] |