From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- proofs/logic.ml | 97 ++++++++++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 78 insertions(+), 19 deletions(-) (limited to 'proofs/logic.ml') diff --git a/proofs/logic.ml b/proofs/logic.ml index e5294715..613581ad 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -23,7 +23,6 @@ open Typing open Proof_type open Type_errors open Retyping -open Misctypes module NamedDecl = Context.Named.Declaration @@ -63,6 +62,7 @@ let is_unification_error = function let catchable_exception = function | CErrors.UserError _ | TypeError _ + | Notation.NumeralNotationError _ | RefinerError _ | Indrec.RecursionSchemeError _ | Nametab.GlobalizationError _ (* reduction errors *) @@ -185,6 +185,22 @@ let check_decl_position env sigma sign d = * on the right side [right] if [toleft=false]. * If [with_dep] then dependent hypotheses are moved accordingly. *) +(** Move destination for hypothesis *) + +type 'id move_location = + | MoveAfter of 'id + | MoveBefore of 'id + | MoveFirst + | MoveLast (** can be seen as "no move" when doing intro *) + +(** Printing of [move_location] *) + +let pr_move_location pr_id = function + | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id + | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id + | MoveFirst -> str " at top" + | MoveLast -> str " at bottom" + let move_location_eq m1 m2 = match m1, m2 with | MoveAfter id1, MoveAfter id2 -> Id.equal id1 id2 | MoveBefore id1, MoveBefore id2 -> Id.equal id1 id2 @@ -236,7 +252,7 @@ let move_hyp sigma toleft (left,declfrom,right) hto = (first, d::middle) else user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++ - Miscprint.pr_move_location Id.print hto ++ + pr_move_location Id.print hto ++ str (if toleft then ": it occurs in the type of " else ": it depends on ") ++ Id.print hyp ++ str ".") else @@ -289,7 +305,15 @@ 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 - | (App _| Case _) -> Constr.fold (collrec deep) acc c + | Case(ci,p,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 + Array.fold_left (collrec deep) + (Constr.fold (collrec deep) (Constr.fold (collrec deep) acc p) c) + br + | App _ -> Constr.fold (collrec deep) acc c | Proj (_, c) -> collrec deep acc c | _ -> Constr.fold (collrec true) acc c in @@ -301,9 +325,10 @@ let check_meta_variables env sigma c = let check_conv_leq_goal env sigma arg ty conclty = if !check then - let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in - if b then evm - else raise (RefinerError (env, sigma, BadType (arg,ty,conclty))) + let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in + match ans with + | Some evm -> evm + | None -> raise (RefinerError (env, sigma, BadType (arg,ty,conclty))) else sigma exception Stop of EConstr.t list @@ -387,12 +412,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | Case (ci,p,c,lf) -> let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in let sigma = check_conv_leq_goal env sigma trm conclty' conclty in - let (acc'',sigma, rbranches) = - Array.fold_left2 - (fun (lacc,sigma,bacc) ty fi -> - let (r,_,s,b') = mk_refgoals sigma goal lacc ty fi in r,s,(b'::bacc)) - (acc',sigma,[]) lbrty lf - in + let (acc'',sigma,rbranches) = treat_case sigma goal 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 @@ -440,12 +460,7 @@ and mk_hdgoals sigma goal goalacc trm = | Case (ci,p,c,lf) -> let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in - let (acc'',sigma,rbranches) = - Array.fold_left2 - (fun (lacc,sigma,bacc) ty fi -> - let (r,_,s,b') = mk_refgoals sigma goal lacc ty fi in r,s,(b'::bacc)) - (acc',sigma,[]) lbrty lf - in + let (acc'',sigma,rbranches) = treat_case sigma goal 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 @@ -483,7 +498,7 @@ and mk_arggoals sigma goal goalacc funty allargs = let env = Goal.V82.env sigma goal in raise (RefinerError (env,sigma,CannotApply (t, harg))) in - Array.smartfoldmap foldmap (goalacc, funty, sigma) allargs + Array.Smart.fold_left_map foldmap (goalacc, funty, sigma) allargs and mk_casegoals sigma goal goalacc p c = let env = Goal.V82.env sigma goal in @@ -497,6 +512,50 @@ and mk_casegoals sigma goal goalacc p c = let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in (acc'',lbrty,conclty,sigma,p',c') +and treat_case sigma goal ci lbrty lf acc' = + let rec strip_outer_cast c = match kind c with + | Cast (c,_,_) -> strip_outer_cast c + | _ -> c in + let decompose_app_vect c = match kind c with + | App (f,cl) -> (f, cl) + | _ -> (c,[||]) in + let env = Goal.V82.env sigma goal 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 sigma goal lacc ty fi in + r,s,(fi'::bacc) + else + (* 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 + destruct/case generated schemes of the form + Case(ci,p,c,[|Meta;...;Meta|]; + 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 + eta-expanded but when not when the branch has the single-meta + form [Meta] *) + 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 sigma goal lacc ty head' in + let fi' = it_mkLambda_or_LetIn (mkApp (head'',args)) ctx in + (r,s,fi'::bacc) + end + else + (* Supposed to be meta-free *) + let sigma, t'ty = goal_type_of env sigma fi in + let sigma = check_conv_leq_goal env sigma fi t'ty ty in + (lacc,sigma,fi::bacc)) + (acc',sigma,[]) lbrty lf ci.ci_pp_info.cstr_tags let convert_hyp check sign sigma d = let id = NamedDecl.get_id d in -- cgit v1.2.3