diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/inv.ml | 8 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 7 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 13 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 8 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 89 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 18 | ||||
| -rw-r--r-- | tactics/tactics.ml | 41 |
7 files changed, 120 insertions, 64 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index 3574990f6..01124e867 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -296,17 +296,17 @@ let get_names (allow_conj,issimple) (loc, pat as x) = match pat with error "Discarding pattern not allowed for inversion equations." | IntroAction (IntroRewrite _) -> error "Rewriting pattern not allowed for inversion equations." - | IntroAction (IntroOrAndPattern [[]]) when allow_conj -> (None, []) - | IntroAction (IntroOrAndPattern [(_,IntroNaming (IntroIdentifier id)) :: _ as l]) + | IntroAction (IntroOrAndPattern (IntroAndPattern [])) when allow_conj -> (None, []) + | IntroAction (IntroOrAndPattern (IntroAndPattern ((_,IntroNaming (IntroIdentifier id)) :: _ as l))) when allow_conj -> (Some id,l) - | IntroAction (IntroOrAndPattern [_]) -> + | IntroAction (IntroOrAndPattern (IntroAndPattern _)) -> if issimple then error"Conjunctive patterns not allowed for simple inversion equations." else error"Nested conjunctive patterns not allowed for inversion equations." | IntroAction (IntroInjection l) -> error "Injection patterns not allowed for inversion equations." - | IntroAction (IntroOrAndPattern l) -> + | IntroAction (IntroOrAndPattern (IntroOrPattern _)) -> error "Disjunctive patterns not allowed for inversion equations." | IntroAction (IntroApplyOn (c,pat)) -> error "Apply patterns not allowed for inversion equations." diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 14e0fed31..f92213da8 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -258,8 +258,11 @@ and intern_intro_pattern_action lf ist = function | IntroApplyOn (c,pat) -> IntroApplyOn (intern_constr ist c, intern_intro_pattern lf ist pat) -and intern_or_and_intro_pattern lf ist = - List.map (List.map (intern_intro_pattern lf ist)) +and intern_or_and_intro_pattern lf ist = function + | IntroAndPattern l -> + IntroAndPattern (List.map (intern_intro_pattern lf ist) l) + | IntroOrPattern ll -> + IntroOrPattern (List.map (List.map (intern_intro_pattern lf ist)) ll) let intern_or_and_intro_pattern_loc lf ist = function | ArgVar (_,id) as x -> diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 8db91c07f..a6991691f 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -511,7 +511,9 @@ let extract_ltac_constr_values ist env = (* Extract the identifier list from lfun: join all branches (what to do else?)*) let rec intropattern_ids (loc,pat) = match pat with | IntroNaming (IntroIdentifier id) -> [id] - | IntroAction (IntroOrAndPattern ll) -> + | IntroAction (IntroOrAndPattern (IntroAndPattern l)) -> + List.flatten (List.map intropattern_ids l) + | IntroAction (IntroOrAndPattern (IntroOrPattern ll)) -> List.flatten (List.map intropattern_ids (List.flatten ll)) | IntroAction (IntroInjection l) -> List.flatten (List.map intropattern_ids l) @@ -940,8 +942,13 @@ and interp_intro_pattern_action ist env sigma = function sigma, IntroApplyOn (c,ipat) | IntroWildcard | IntroRewrite _ as x -> sigma, x -and interp_or_and_intro_pattern ist env sigma = - List.fold_map (interp_intro_pattern_list_as_list ist env) sigma +and interp_or_and_intro_pattern ist env sigma = function + | IntroAndPattern l -> + let sigma, l = List.fold_map (interp_intro_pattern ist env) sigma l in + sigma, IntroAndPattern l + | IntroOrPattern ll -> + let sigma, ll = List.fold_map (interp_intro_pattern_list_as_list ist env) sigma ll in + sigma, IntroOrPattern ll and interp_intro_pattern_list_as_list ist env sigma = function | [loc,IntroNaming (IntroIdentifier id)] as l -> diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index c74f6093a..e09360a6a 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -54,10 +54,16 @@ and subst_intro_pattern_action subst = function | IntroApplyOn (t,pat) -> IntroApplyOn (subst_glob_constr subst t,subst_intro_pattern subst pat) | IntroOrAndPattern l -> - IntroOrAndPattern (List.map (List.map (subst_intro_pattern subst)) l) + IntroOrAndPattern (subst_intro_or_and_pattern subst l) | IntroInjection l -> IntroInjection (List.map (subst_intro_pattern subst) l) | IntroWildcard | IntroRewrite _ as x -> x +and subst_intro_or_and_pattern subst = function + | IntroAndPattern l -> + IntroAndPattern (List.map (subst_intro_pattern subst) l) + | IntroOrPattern ll -> + IntroOrPattern (List.map (List.map (subst_intro_pattern subst)) ll) + let subst_induction_arg subst = function | clear,ElimOnConstr c -> clear,ElimOnConstr (subst_glob_with_bindings subst c) | clear,ElimOnAnonHyp n as x -> x diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 061c05b9b..4029d1fcc 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -147,51 +147,85 @@ type branch_args = { largs : constr list; (* its arguments *) branchnum : int; (* the branch number *) pred : constr; (* the predicate we used *) - nassums : int; (* the number of assumptions to be introduced *) + nassums : int; (* number of assumptions/letin to be introduced *) branchsign : bool list; (* the signature of the branch. - true=recursive argument, false=constant *) + true=assumption, false=let-in *) branchnames : Tacexpr.intro_patterns} type branch_assumptions = { ba : branch_args; (* the branch args *) assums : Context.Named.t} (* the list of assumptions introduced *) +open Misctypes + let fix_empty_or_and_pattern nv l = (* 1- The syntax does not distinguish between "[ ]" for one clause with no names and "[ ]" for no clause at all *) (* 2- More generally, we admit "[ ]" for any disjunctive pattern of arbitrary length *) match l with - | [[]] -> List.make nv [] + | IntroOrPattern [[]] -> IntroOrPattern (List.make nv []) | _ -> l -let check_or_and_pattern_size loc names n = - if not (Int.equal (List.length names) n) then - if Int.equal n 1 then - user_err_loc (loc,"",str "Expects a conjunctive pattern.") - else - user_err_loc (loc,"",str "Expects a disjunctive pattern with " ++ int n - ++ str " branches.") - -let compute_induction_names n = function +let check_or_and_pattern_size loc names branchsigns = + let n = Array.length branchsigns in + let msg p1 p2 = strbrk "a conjunctive pattern made of " ++ int p1 ++ (if p1 == p2 then mt () else str " or " ++ int p2) ++ str " patterns" in + let err1 p1 p2 = + user_err_loc (loc,"",str "Expects " ++ msg p1 p2 ++ str ".") in + let errn n = + user_err_loc (loc,"",str "Expects a disjunctive pattern with " ++ int n + ++ str " branches.") in + let err1' p1 p2 = + user_err_loc (loc,"",strbrk "Expects a disjunctive pattern with 1 branch or " ++ msg p1 p2 ++ str ".") in + match names with + | IntroAndPattern l -> + if not (Int.equal n 1) then errn n; + let p1 = List.count (fun x -> x) branchsigns.(0) in + let p2 = List.length branchsigns.(0) in + let p = List.length l in + if not (Int.equal p p1 || Int.equal p p2) || + not (List.for_all (function _,IntroNaming _ | _,IntroAction _ -> true | _,IntroForthcoming _ -> false) l) then err1 p1 p2; + if Int.equal p p1 then + IntroAndPattern + (List.extend branchsigns.(0) (Loc.ghost,IntroNaming IntroAnonymous) l) + else + names + | IntroOrPattern ll -> + if not (Int.equal n (List.length ll)) then + if Int.equal n 1 then + let p1 = List.count (fun x -> x) branchsigns.(0) in + let p2 = List.length branchsigns.(0) in + err1' p1 p2 else errn n; + names + +let get_and_check_or_and_pattern loc names branchsigns = + let names = check_or_and_pattern_size loc names branchsigns in + match names with + | IntroAndPattern l -> [|l|] + | IntroOrPattern l -> Array.of_list l + +let compute_induction_names branchletsigns = function | None -> - Array.make n [] + Array.make (Array.length branchletsigns) [] | Some (loc,names) -> - let names = fix_empty_or_and_pattern n names in - check_or_and_pattern_size loc names n; - Array.of_list names + let names = fix_empty_or_and_pattern (Array.length branchletsigns) names in + get_and_check_or_and_pattern loc names branchletsigns -let compute_construtor_signatures isrec ((_,k as ity),u) = +(* Compute the let-in signature of case analysis or standard induction scheme *) +let compute_constructor_signatures isrec ((_,k as ity),u) = let rec analrec c recargs = match kind_of_term c, recargs with | Prod (_,_,c), recarg::rest -> - let b = match Declareops.dest_recarg recarg with - | Norec | Imbr _ -> false - | Mrec (_,j) -> isrec && Int.equal j k - in b :: (analrec c rest) - | LetIn (_,_,_,c), rest -> false :: (analrec c rest) + let rest = analrec c rest in + begin match Declareops.dest_recarg recarg with + | Norec | Imbr _ -> true :: rest + | Mrec (_,j) -> + if isrec && Int.equal j k then true :: true :: rest + else true :: rest + end + | LetIn (_,_,_,c), rest -> false :: analrec c rest | _, [] -> [] - | _ -> anomaly (Pp.str "compute_construtor_signatures") + | _ -> anomaly (Pp.str "compute_constructor_signatures") in let (mib,mip) = Global.lookup_inductive ity in let n = mib.mind_nparams in @@ -596,8 +630,8 @@ module New = struct (str "The elimination combinator " ++ str name_elim ++ str " is unknown.") in let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in - let branchsigns = compute_construtor_signatures isrec ind in - let brnames = compute_induction_names (Array.length branchsigns) allnames in + let branchsigns = compute_constructor_signatures isrec ind in + let brnames = compute_induction_names branchsigns allnames in let flags = Unification.elim_flags () in let elimclause' = match predicate with @@ -609,10 +643,7 @@ module New = struct let (hd,largs) = decompose_app clenv'.templtyp.Evd.rebus in let ba = { branchsign = branchsigns.(i); branchnames = brnames.(i); - nassums = - List.fold_left - (fun acc b -> if b then acc+2 else acc+1) - 0 branchsigns.(i); + nassums = List.length branchsigns.(i); branchnum = i+1; ity = ind; largs = List.map (clenv_nf_meta clenv') largs; diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 147f1f0f2..4f6f87f69 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -102,28 +102,32 @@ type branch_args = { largs : constr list; (** its arguments *) branchnum : int; (** the branch number *) pred : constr; (** the predicate we used *) - nassums : int; (** the number of assumptions to be introduced *) + nassums : int; (** number of assumptions/letin to be introduced *) branchsign : bool list; (** the signature of the branch. - true=recursive argument, false=constant *) + true=assumption, false=let-in *) branchnames : intro_patterns} type branch_assumptions = { ba : branch_args; (** the branch args *) assums : Context.Named.t} (** the list of assumptions introduced *) -(** [check_disjunctive_pattern_size loc pats n] returns an appropriate - error message if |pats| <> n *) -val check_or_and_pattern_size : - Loc.t -> delayed_open_constr or_and_intro_pattern_expr -> int -> unit +(** [check_disjunctive_pattern_size loc pats n] returns an appropriate + error message if |pats| <> n; extends them if no pattern is given + for let-ins in the case of a conjunctive pattern *) +val get_and_check_or_and_pattern : + Loc.t -> delayed_open_constr or_and_intro_pattern_expr -> + bool list array -> intro_patterns array (** Tolerate "[]" to mean a disjunctive pattern of any length *) val fix_empty_or_and_pattern : int -> delayed_open_constr or_and_intro_pattern_expr -> delayed_open_constr or_and_intro_pattern_expr +val compute_constructor_signatures : rec_flag -> pinductive -> bool list array + (** Useful for [as intro_pattern] modifier *) val compute_induction_names : - int -> or_and_intro_pattern option -> intro_patterns array + bool list array -> or_and_intro_pattern option -> intro_patterns array val elimination_sort_of_goal : goal sigma -> sorts_family val elimination_sort_of_hyp : Id.t -> goal sigma -> sorts_family diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f0f46c14d..796cea98f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2089,14 +2089,15 @@ let intro_or_and_pattern loc bracketed ll thin tac id = Proofview.Goal.enter { enter = begin fun gl -> let c = mkVar id in let t = Tacmach.New.pf_unsafe_type_of gl c in - let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in - let nv = constructors_nrealdecls ind in - let ll = fix_empty_or_and_pattern (Array.length nv) ll in - check_or_and_pattern_size loc ll (Array.length nv); + let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in + let branchsigns = compute_constructor_signatures false ind in + let nv_with_let = Array.map List.length branchsigns in + let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in + let ll = get_and_check_or_and_pattern loc ll branchsigns in Tacticals.New.tclTHENLASTn (Tacticals.New.tclTHEN (simplest_case c) (Proofview.V82.tactic (clear [id]))) (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l) - nv (Array.of_list ll)) + nv_with_let ll) end } let rewrite_hyp assert_style l2r id = @@ -2137,7 +2138,8 @@ let prepare_naming loc = function let rec explicit_intro_names = function | (_, IntroForthcoming _) :: l -> explicit_intro_names l | (_, IntroNaming (IntroIdentifier id)) :: l -> id :: explicit_intro_names l -| (_, IntroAction (IntroOrAndPattern ll)) :: l' -> +| (_, IntroAction (IntroOrAndPattern l)) :: l' -> + let ll = match l with IntroAndPattern l -> [l] | IntroOrPattern ll -> ll in List.flatten (List.map (fun l -> explicit_intro_names (l@l')) ll) | (_, IntroAction (IntroInjection l)) :: l' -> explicit_intro_names (l@l') @@ -2842,8 +2844,8 @@ let induct_discharge dests avoid' tac (avoid,ra) names = let avoid = avoid @ avoid' in let rec peel_tac ra dests names thin = match ra with - | (RecArg,deprec,recvarname) :: - (IndArg,depind,hyprecname) :: ra' -> + | (RecArg,_,deprec,recvarname) :: + (IndArg,_,depind,hyprecname) :: ra' -> Proofview.Goal.enter { enter = begin fun gl -> let (recpat,names) = match names with | [loc,IntroNaming (IntroIdentifier id) as pat] -> @@ -2860,7 +2862,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names = peel_tac ra' (update_dest dests ids') names thin) end }) end } - | (IndArg,dep,hyprecname) :: ra' -> + | (IndArg,_,dep,hyprecname) :: ra' -> Proofview.Goal.enter { enter = begin fun gl -> (* Rem: does not happen in Coq schemes, only in user-defined schemes *) let pat,names = @@ -2868,7 +2870,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names = dest_intro_patterns avoid thin MoveLast [pat] (fun ids thin -> peel_tac ra' (update_dest dests ids) names thin) end } - | (RecArg,dep,recvarname) :: ra' -> + | (RecArg,_,dep,recvarname) :: ra' -> Proofview.Goal.enter { enter = begin fun gl -> let (pat,names) = consume_pattern avoid (Name recvarname) dep gl names in @@ -2876,7 +2878,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names = dest_intro_patterns avoid thin dest [pat] (fun ids thin -> peel_tac ra' dests names thin) end } - | (OtherArg,dep,_) :: ra' -> + | (OtherArg,_,dep,_) :: ra' -> Proofview.Goal.enter { enter = begin fun gl -> let (pat,names) = consume_pattern avoid Anonymous dep gl names in let dest = get_recarg_dest dests in @@ -3682,9 +3684,9 @@ let compute_scheme_signature scheme names_info ind_type_guess = let rec check_branch p c = match kind_of_term c with | Prod (_,t,c) -> - (is_pred p t, dependent (mkRel 1) c) :: check_branch (p+1) c + (is_pred p t, true, dependent (mkRel 1) c) :: check_branch (p+1) c | LetIn (_,_,_,c) -> - (OtherArg, dependent (mkRel 1) c) :: check_branch (p+1) c + (OtherArg, false, dependent (mkRel 1) c) :: check_branch (p+1) c | _ when is_pred p c == IndArg -> [] | _ -> raise Exit in @@ -3694,12 +3696,12 @@ let compute_scheme_signature scheme names_info ind_type_guess = (try let lchck_brch = check_branch p t in let n = List.fold_left - (fun n (b,_) -> if b == RecArg then n+1 else n) 0 lchck_brch in + (fun n (b,_,_) -> if b == RecArg then n+1 else n) 0 lchck_brch in let recvarname, hyprecname, avoid = make_up_names n scheme.indref names_info in let namesign = - List.map (fun (b,dep) -> - (b, dep, if b == IndArg then hyprecname else recvarname)) + List.map (fun (b,is_assum,dep) -> + (b,is_assum,dep,if b == IndArg then hyprecname else recvarname)) lchck_brch in (avoid,namesign) :: find_branches (p+1) brs with Exit-> error_ind_scheme "the branches of") @@ -3744,7 +3746,7 @@ let given_elim hyp0 (elimc,lbind as e) gl = Tacmach.New.project gl, (e, Tacmach.New.pf_unsafe_type_of gl elimc), ind_type_guess type scheme_signature = - (Id.t list * (elim_arg_kind * bool * Id.t) list) array + (Id.t list * (elim_arg_kind * bool * bool * Id.t) list) array type eliminator_source = | ElimUsing of (eliminator * types) * scheme_signature @@ -3865,7 +3867,10 @@ let apply_induction_in_context hyp0 inhyps elim indvars names induct_tac = List.fold_left (fun a (id,b,_) -> if Option.is_empty b then (mkVar id)::a else a) [] deps in let (sigma, isrec, elim, indsign) = get_eliminator elim dep s (Proofview.Goal.assume gl) in - let names = compute_induction_names (Array.length indsign) names in + let branchletsigns = + let f (_,is_not_let,_,_) = is_not_let in + Array.map (fun (_,l) -> List.map f l) indsign in + let names = compute_induction_names branchletsigns names in let tac = (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn) (Tacticals.New.tclTHENLIST [ |