From d72e5c154faeea1d55387bc8c039d97f63ebd1c4 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 3 Mar 2019 21:03:37 +0100 Subject: Change the representation of kernel case. We store bound variable names instead of functions for both branches and predicate, and we furthermore add the parameters in the node. Let bindings are not taken into account and require an environment lookup for retrieval. --- proofs/clenv.ml | 14 +++++++++----- proofs/logic.ml | 21 ++++++++++----------- 2 files changed, 19 insertions(+), 16 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 00ac5a0624..44d3b44077 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -268,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 @@ -277,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 @@ -627,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 diff --git a/proofs/logic.ml b/proofs/logic.ml index f159395177..cb67d42bdc 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) -- cgit v1.2.3 From b6d5332c6e3127ba3fec466abe502ee40c031ed2 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 19 Mar 2019 00:22:14 +0100 Subject: Fix behaviour of destruct after change of case representation. We ensure not to generate dummy beta-cuts in case branches generated by destruct. There was seemingly code trying to perform this but in an akward way. --- proofs/logic.ml | 14 +++----------- 1 file changed, 3 insertions(+), 11 deletions(-) (limited to 'proofs') diff --git a/proofs/logic.ml b/proofs/logic.ml index cb67d42bdc..8b31c07f5e 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -478,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 @@ -493,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 @@ -502,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 @@ -512,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 -- cgit v1.2.3