diff options
Diffstat (limited to 'plugins/ssr/ssripats.ml')
| -rw-r--r-- | plugins/ssr/ssripats.ml | 1023 |
1 files changed, 662 insertions, 361 deletions
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index b3be31b7b..1a964bd50 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -6,395 +6,696 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open Ssrmatching_plugin -open Names -open Pp -open Term -open Tactics -open Tacticals -open Tacmach -open Coqlib open Util -open Evd -open Printer +open Names + +open Proofview +open Proofview.Notations -open Ssrmatching_plugin -open Ssrmatching open Ssrast -open Ssrprinters -open Ssrcommon -open Ssrequality -open Ssrview -open Ssrelim -open Ssrbwd - -module RelDecl = Context.Rel.Declaration -(** Extended intro patterns {{{ ***********************************************) - - -(* There are two ways of "applying" a view to term: *) -(* 1- using a view hint if the view is an instance of some *) -(* (reflection) inductive predicate. *) -(* 2- applying the view if it coerces to a function, adding *) -(* implicit arguments. *) -(* They require guessing the view hints and the number of *) -(* implicits, respectively, which we do by brute force. *) - -let apply_type x xs = Proofview.V82.of_tactic (apply_type ~typecheck:false x xs) - -let new_tac = Proofview.V82.of_tactic - -let with_top tac gl = - tac_ctx - (tclTHENLIST [ introid top_id; tac (EConstr.mkVar top_id); new_tac (clear [top_id])]) - gl - -let tclTHENS_nonstrict tac tacl taclname gl = - let tacres = tac gl in - let n_gls = List.length (sig_it tacres) in - let n_tac = List.length tacl in - if n_gls = n_tac then tclTHENS_a (fun _ -> tacres) tacl gl else - if n_gls = 0 then tacres else - let pr_only n1 n2 = if n1 < n2 then str "only " else mt () in - let pr_nb n1 n2 name = - pr_only n1 n2 ++ int n1 ++ str (" " ^ String.plural n1 name) in - errorstrm (pr_nb n_tac n_gls taclname ++ spc () - ++ str "for " ++ pr_nb n_gls n_tac "subgoal") - -let rec nat_of_n n = - if n = 0 then EConstr.mkConstruct path_of_O - else EConstr.mkApp (EConstr.mkConstruct path_of_S, [|nat_of_n (n-1)|]) - -let ssr_abstract_id = Summary.ref ~name:"SSR:abstractid" 0 - -let mk_abstract_id () = incr ssr_abstract_id; nat_of_n !ssr_abstract_id - -let ssrmkabs id gl = - let env, concl = pf_env gl, Tacmach.pf_concl gl in + +module IpatMachine : sig + + (* the => tactical. ?eqtac is a tactic to be eventually run + * after the first [..] block. first_case_is_dispatch is the + * ssr exception to elim: and case: *) + val main : ?eqtac:unit tactic -> first_case_is_dispatch:bool -> + ssripats -> unit tactic + +end = struct (* {{{ *) + +module State : sig + + (* to_clear API *) + val isCLR_PUSH : Id.t -> unit tactic + val isCLR_PUSHL : Id.t list -> unit tactic + val isCLR_CONSUME : unit tactic + + (* Some data may expire *) + val isTICK : ssripat -> unit tactic + + val isPRINT : Proofview.Goal.t -> Pp.t + +end = struct (* {{{ *) + +type istate = { + + (* Delayed clear *) + to_clear : Id.t list; + +} + +let empty_state = { + to_clear = []; +} + +include Ssrcommon.MakeState(struct + type state = istate + let init = empty_state +end) + +let isPRINT g = + let state = get g in + Pp.(str"{{ to_clear: " ++ + prlist_with_sep spc Id.print state.to_clear ++ spc () ++ + str" }}") + + +let isCLR_PUSH id = + tclGET (fun { to_clear = ids } -> + tclSET { to_clear = id :: ids }) + +let isCLR_PUSHL more_ids = + tclGET (fun { to_clear = ids } -> + tclSET { to_clear = more_ids @ ids }) + +let isCLR_CONSUME = + tclGET (fun { to_clear = ids } -> + tclSET { to_clear = [] } <*> + Tactics.clear ids) + + +let isTICK _ = tclUNIT () + +end (* }}} *************************************************************** *) + +open State + +(** [=> *] ****************************************************************) +(** [nb_assums] returns the number of dependent premises *) +(** Warning: unlike [nb_deps_assums], it does not perform reduction *) +let rec nb_assums cur env sigma t = + match EConstr.kind sigma t with + | Term.Prod(name,ty,body) -> + nb_assums (cur+1) env sigma body + | Term.LetIn(name,ty,t1,t2) -> + nb_assums (cur+1) env sigma t2 + | Term.Cast(t,_,_) -> + nb_assums cur env sigma t + | _ -> cur +let nb_assums = nb_assums 0 + +let intro_anon_all = Goal.enter begin fun gl -> + let env = Goal.env gl in + let sigma = Goal.sigma gl in + let g = Goal.concl gl in + let n = nb_assums env sigma g in + Tacticals.New.tclDO n Ssrcommon.tclINTRO_ANON +end + +(** [intro_drop] behaves like [intro_anon] but registers the id of the + introduced assumption for a delayed clear. *) +let intro_drop = + Ssrcommon.tclINTRO ~id:None + ~conclusion:(fun ~orig_name:_ ~new_name -> isCLR_PUSH new_name) + +(** [intro_end] performs the actions that have been delayed. *) +let intro_end = + Ssrcommon.tcl0G (isCLR_CONSUME) + +(** [=> _] *****************************************************************) +let intro_clear ids future_ipats = + Goal.enter begin fun gl -> + let _, clear_ids, ren = + List.fold_left (fun (used_ids, clear_ids, ren) id -> + if not(Ssrcommon.is_name_in_ipats id future_ipats) then begin + used_ids, id :: clear_ids, ren + end else + let new_id = Ssrcommon.mk_anon_id (Id.to_string id) used_ids in + (new_id :: used_ids, new_id :: clear_ids, (id, new_id) :: ren)) + (Tacmach.New.pf_ids_of_hyps gl, [], []) ids + in + Tactics.rename_hyp ren <*> + isCLR_PUSHL clear_ids +end + +(** [=> []] *****************************************************************) +let tac_case t = + Goal.enter begin fun _ -> + Ssrcommon.tacTYPEOF t >>= fun ty -> + Ssrcommon.tacIS_INJECTION_CASE ~ty t >>= fun is_inj -> + if is_inj then + V82.tactic ~nf_evars:false (Ssrelim.perform_injection t) + else + Ssrelim.ssrscasetac t +end + +(** [=> [: id]] ************************************************************) +let mk_abstract_id = + let open Coqlib in + let ssr_abstract_id = Summary.ref ~name:"SSR:abstractid" 0 in +begin fun () -> + let rec nat_of_n n = + if n = 0 then EConstr.mkConstruct path_of_O + else EConstr.mkApp (EConstr.mkConstruct path_of_S, [|nat_of_n (n-1)|]) in + incr ssr_abstract_id; nat_of_n !ssr_abstract_id +end + +let tcltclMK_ABSTRACT_VAR id = Goal.enter begin fun gl -> + let env, concl = Goal.(env gl, concl gl) in let step = begin fun sigma -> let (sigma, (abstract_proof, abstract_ty)) = let (sigma, (ty, _)) = Evarutil.new_type_evar env sigma Evd.univ_flexible_alg in - let (sigma, ablock) = mkSsrConst "abstract_lock" env sigma in + let (sigma, ablock) = Ssrcommon.mkSsrConst "abstract_lock" env sigma in let (sigma, lock) = Evarutil.new_evar env sigma ablock in - let (sigma, abstract) = mkSsrConst "abstract" env sigma in - let abstract_ty = EConstr.mkApp(abstract, [|ty;mk_abstract_id ();lock|]) in - let (sigma, m) = Evarutil.new_evar env sigma abstract_ty in - (sigma, (m, abstract_ty)) in + let (sigma, abstract) = Ssrcommon.mkSsrConst "abstract" env sigma in + let abstract_ty = + EConstr.mkApp(abstract, [|ty;mk_abstract_id ();lock|]) in + let sigma, m = Evarutil.new_evar env sigma abstract_ty in + sigma, (m, abstract_ty) in let sigma, kont = - let rd = RelDecl.LocalAssum (Name id, abstract_ty) in - let (sigma, ev) = Evarutil.new_evar (EConstr.push_rel rd env) sigma concl in - (sigma, ev) + let rd = Context.Rel.Declaration.LocalAssum (Name id, abstract_ty) in + let sigma, ev = Evarutil.new_evar (EConstr.push_rel rd env) sigma concl in + sigma, ev in -(* pp(lazy(pr_econstr concl)); *) - let term = EConstr.(mkApp (mkLambda(Name id,abstract_ty,kont) ,[|abstract_proof|])) in + let term = + EConstr.(mkApp (mkLambda(Name id,abstract_ty,kont),[|abstract_proof|])) in let sigma, _ = Typing.type_of env sigma term in - (sigma, term) + sigma, term end in - Proofview.V82.of_tactic - (Proofview.tclTHEN - (Tactics.New.refine ~typecheck:false step) - (Proofview.tclFOCUS 1 3 Proofview.shelve)) gl - -let ssrmkabstac ids = - List.fold_right (fun id tac -> tclTHENFIRST (ssrmkabs id) tac) ids tclIDTAC - -(* introstac: for "move" and "clear", tclEQINTROS: for "case" and "elim" *) -(* This block hides the spaghetti-code needed to implement the only two *) -(* tactics that should be used to process intro patters. *) -(* The difficulty is that we don't want to always rename, but we can *) -(* compute needeed renamings only at runtime, so we theread a tree like *) -(* imperativestructure so that outer renamigs are inherited by inner *) -(* ipts and that the cler performed at the end of ipatstac clears hyps *) -(* eventually renamed at runtime. *) -let delayed_clear force rest clr gl = - let gl, ctx = pull_ctx gl in - let hyps = pf_hyps gl in - let () = if not force then List.iter (check_hyp_exists hyps) clr in - if List.exists (fun x -> force || is_name_in_ipats (hyp_id x) rest) clr then - let ren_clr, ren = - List.split (List.map (fun x -> - let x = hyp_id x in - let x' = mk_anon_id (Id.to_string x) gl in - x', (x, x')) clr) in - let ctx = { ctx with delayed_clears = ren_clr @ ctx.delayed_clears } in - let gl = push_ctx ctx gl in - tac_ctx (Proofview.V82.of_tactic (rename_hyp ren)) gl - else - let ctx = { ctx with delayed_clears = hyps_ids clr @ ctx.delayed_clears } in - let gl = push_ctx ctx gl in - tac_ctx tclIDTAC gl - -(* Common code to handle generalization lists along with the defective case *) + Tactics.New.refine ~typecheck:false step <*> + tclFOCUS 1 3 Proofview.shelve +end + +let tclMK_ABSTRACT_VARS ids = + List.fold_right (fun id tac -> + Tacticals.New.tclTHENFIRST (tcltclMK_ABSTRACT_VAR id) tac) ids (tclUNIT ()) + +(* Debugging *) +let tclLOG p t = + tclUNIT () >>= begin fun () -> + Ssrprinters.ppdebug (lazy Pp.(str "exec: " ++ Ssrprinters.pr_ipat p)); + tclUNIT () + end <*> + Goal.enter begin fun g -> + Ssrprinters.ppdebug (lazy Pp.(str" on state:" ++ spc () ++ + isPRINT g ++ + str" goal:" ++ spc () ++ Printer.pr_goal (Goal.print g))); + tclUNIT () + end + <*> + t p + <*> + Goal.enter begin fun g -> + Ssrprinters.ppdebug (lazy Pp.(str "done: " ++ isPRINT g)); + tclUNIT () + end + +let rec ipat_tac1 future_ipats ipat : unit tactic = + match ipat with + | IPatView l -> + Ssrview.tclIPAT_VIEWS ~views:l + ~conclusion:(fun ~to_clear:clr -> intro_clear clr future_ipats) + | IPatDispatch ipatss -> + tclEXTEND (List.map ipat_tac ipatss) (tclUNIT ()) [] + + | IPatId id -> Ssrcommon.tclINTRO_ID id + + | IPatCase ipatss -> + tclIORPAT (Ssrcommon.tclWITHTOP tac_case) ipatss + | IPatInj ipatss -> + tclIORPAT (Ssrcommon.tclWITHTOP + (fun t -> V82.tactic ~nf_evars:false (Ssrelim.perform_injection t))) ipatss + + | IPatAnon Drop -> intro_drop + | IPatAnon One -> Ssrcommon.tclINTRO_ANON + | IPatAnon All -> intro_anon_all + + | IPatNoop -> tclUNIT () + | IPatSimpl Nop -> tclUNIT () + + | IPatClear ids -> intro_clear (List.map Ssrcommon.hyp_id ids) future_ipats + + | IPatSimpl (Simpl n) -> + V82.tactic ~nf_evars:false (Ssrequality.simpltac (Simpl n)) + | IPatSimpl (Cut n) -> + V82.tactic ~nf_evars:false (Ssrequality.simpltac (Cut n)) + | IPatSimpl (SimplCut (n,m)) -> + V82.tactic ~nf_evars:false (Ssrequality.simpltac (SimplCut (n,m))) + + | IPatRewrite (occ,dir) -> + Ssrcommon.tclWITHTOP + (fun x -> V82.tactic ~nf_evars:false (Ssrequality.ipat_rewrite occ dir x)) + + | IPatAbstractVars ids -> tclMK_ABSTRACT_VARS ids + + | IPatTac t -> t + +and ipat_tac pl : unit tactic = + match pl with + | [] -> tclUNIT () + | pat :: pl -> + Ssrcommon.tcl0G (tclLOG pat (ipat_tac1 pl)) <*> + isTICK pat <*> + ipat_tac pl + +and tclIORPAT tac = function + | [[]] -> tac + | p -> Tacticals.New.tclTHENS tac (List.map ipat_tac p) -let with_defective maintac deps clr ist gl = - let top_id = - match EConstr.kind_of_type (project gl) (pf_concl gl) with - | ProdType (Name id, _, _) - when has_discharged_tag (Id.to_string id) -> id - | _ -> top_id in - let top_gen = mkclr clr, cpattern_of_id top_id in - tclTHEN (introid top_id) (maintac deps top_gen ist) gl - -let with_defective_a maintac deps clr ist gl = - let sigma = sig_sig gl in - let top_id = - match EConstr.kind_of_type sigma (without_ctx pf_concl gl) with - | ProdType (Name id, _, _) - when has_discharged_tag (Id.to_string id) -> id - | _ -> top_id in - let top_gen = mkclr clr, cpattern_of_id top_id in - tclTHEN_a (tac_ctx (introid top_id)) (maintac deps top_gen ist) gl - -let with_dgens (gensl, clr) maintac ist = match gensl with - | [deps; []] -> with_defective maintac deps clr ist - | [deps; gen :: gens] -> - tclTHEN (genstac (gens, clr) ist) (maintac deps gen ist) - | [gen :: gens] -> tclTHEN (genstac (gens, clr) ist) (maintac [] gen ist) - | _ -> with_defective maintac [] clr ist - -let viewmovetac_aux ?(next=ref []) clear name_ref (_, vl as v) _ gen ist gl = - let cl, c, clr, gl, gen_pat = - let gl, ctx = pull_ctx gl in - let _, gen_pat, a, b, c, ucst, gl = pf_interp_gen_aux ist gl false gen in - a, b ,c, push_ctx ctx (pf_merge_uc ucst gl), gen_pat in - let clr = if clear then clr else [] in - name_ref := (match id_of_pattern gen_pat with Some id -> id | _ -> top_id); - let clr = if clear then clr else [] in - if vl = [] then tac_ctx (genclrtac cl [c] clr) gl - else - let _, _, gl = - pfa_with_view ist ~next v cl c - (fun cl c -> tac_ctx (genclrtac cl [c] clr)) clr gl in - gl +let split_at_first_case ipats = + let rec loop acc = function + | (IPatSimpl _ | IPatClear _) as x :: rest -> loop (x :: acc) rest + | IPatCase _ as x :: xs -> CList.rev acc, Some x, xs + | pats -> CList.rev acc, None, pats + in + loop [] ipats -let move_top_with_view ~next c r v = - with_defective_a (viewmovetac_aux ~next c r v) [] [] +let ssr_exception is_on = function + | Some (IPatCase l) when is_on -> Some (IPatDispatch l) + | x -> x -type block_names = (int * EConstr.types array) option +let option_to_list = function None -> [] | Some x -> [x] -let (introstac : ?ist:Tacinterp.interp_sign -> ssripats -> Tacmach.tactic), - (tclEQINTROS : ?ind:block_names ref -> ?ist:Tacinterp.interp_sign -> - Tacmach.tactic -> Tacmach.tactic -> ssripats -> - Tacmach.tactic) -= +let main ?eqtac ~first_case_is_dispatch ipats = + let ip_before, case, ip_after = split_at_first_case ipats in + let case = ssr_exception first_case_is_dispatch case in + let case = option_to_list case in + let eqtac = option_to_list (Option.map (fun x -> IPatTac x) eqtac) in + Ssrcommon.tcl0G (ipat_tac (ip_before @ case @ eqtac @ ip_after) <*> intro_end) - let rec ipattac ?ist ~next p : tac_ctx tac_a = fun gl -> -(* pp(lazy(str"ipattac: " ++ pr_ipat p)); *) - match p with - | IPatAnon Drop -> - let id, gl = with_ctx new_wild_id gl in - tac_ctx (introid id) gl - | IPatAnon All -> tac_ctx intro_all gl - (* TODO - | IPatAnon Temporary -> - let (id, orig), gl = with_ctx new_tmp_id gl in - introid_a ~orig id gl - *) - | IPatCase(iorpat) -> - tclIORPAT ?ist (with_top (ssrscasetac false)) iorpat gl - | IPatInj iorpat -> - tclIORPAT ?ist (with_top (ssrscasetac true)) iorpat gl - | IPatRewrite (occ, dir) -> - with_top (ipat_rewrite occ dir) gl - | IPatId id -> tac_ctx (introid id) gl - | IPatNewHidden idl -> tac_ctx (ssrmkabstac idl) gl - | IPatSimpl sim -> - tac_ctx (simpltac sim) gl - | IPatClear clr -> - delayed_clear false !next clr gl - | IPatAnon One -> tac_ctx intro_anon gl - | IPatNoop -> tac_ctx tclIDTAC gl - | IPatView v -> - let ist = - match ist with Some x -> x | _ -> anomaly "ipat: view with no ist" in - let next_keeps = - match !next with (IPatCase _ | IPatRewrite _)::_ -> false | _ -> true in - let top_id = ref top_id in - tclTHENLIST_a [ - (move_top_with_view ~next next_keeps top_id (next_keeps,v) ist); - (fun gl -> - let hyps = without_ctx pf_hyps gl in - if not next_keeps && test_hypname_exists hyps !top_id then - delayed_clear true !next [SsrHyp (Loc.tag !top_id)] gl - else tac_ctx tclIDTAC gl)] - gl - - and tclIORPAT ?ist tac = function - | [[]] -> tac - | orp -> tclTHENS_nonstrict tac (List.map (ipatstac ?ist) orp) "intro pattern" - - and ipatstac ?ist ipats gl = - let rec aux ipats gl = - match ipats with - | [] -> tac_ctx tclIDTAC gl - | p :: ps -> - let next = ref ps in - let gl = ipattac ?ist ~next p gl in - tac_on_all gl (aux !next) - in - aux ipats gl - in +end (* }}} *) + +let tclIPAT_EQ eqtac ip = + Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip)); + IpatMachine.main ~eqtac ~first_case_is_dispatch:true ip + +let tclIPATssr ip = + Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip)); + IpatMachine.main ~first_case_is_dispatch:true ip - let rec split_itacs ?ist ~ind tac' = function - | (IPatSimpl _ | IPatClear _ as spat) :: ipats' -> - let tac = ipattac ?ist ~next:(ref ipats') spat in - split_itacs ?ist ~ind (tclTHEN_a tac' tac) ipats' - | IPatCase iorpat :: ipats' -> - tclIORPAT ?ist tac' iorpat, ipats' - | ipats' -> tac', ipats' in - - let combine_tacs tac eqtac ipats ?ist ~ind gl = - let tac1, ipats' = split_itacs ?ist ~ind tac ipats in - let tac2 = ipatstac ?ist ipats' in - tclTHENLIST_a [ tac1; eqtac; tac2 ] gl in - - (* Exported code *) - let introstac ?ist ipats gl = - with_fresh_ctx (tclTHENLIST_a [ - ipatstac ?ist ipats; - gen_tmp_ids ?ist; - clear_wilds_and_tmp_and_delayed_ids - ]) gl in - - let tclEQINTROS ?(ind=ref None) ?ist tac eqtac ipats gl = - with_fresh_ctx (tclTHENLIST_a [ - combine_tacs (tac_ctx tac) (tac_ctx eqtac) ipats ?ist ~ind; - gen_tmp_ids ?ist; - clear_wilds_and_tmp_and_delayed_ids; - ]) gl in - - introstac, tclEQINTROS -;; - -(* Intro patterns processing for elim tactic*) -let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr gl = - (* Utils of local interest only *) - let iD s ?t gl = let t = match t with None -> pf_concl gl | Some x -> x in - ppdebug(lazy Pp.(str s ++ pr_econstr_env (pf_env gl) (project gl) t)); Tacticals.tclIDTAC gl in - let protectC, gl = pf_mkSsrConst "protect_term" gl in - let eq, gl = pf_fresh_global (Coqlib.build_coq_eq ()) gl in - let eq = EConstr.of_constr eq in - let fire_subst gl t = Reductionops.nf_evar (project gl) t in - let intro_eq = - match eqid with - | Some (IPatId ipat) when not is_rec -> - let rec intro_eq gl = match EConstr.kind_of_type (project gl) (pf_concl gl) with - | ProdType (_, src, tgt) -> - (match EConstr.kind_of_type (project gl) src with - | AtomicType (hd, _) when EConstr.eq_constr (project gl) hd protectC -> - Tacticals.tclTHENLIST [unprotecttac; introid ipat] gl - | _ -> Tacticals.tclTHENLIST [ iD "IA"; Ssrcommon.intro_anon; intro_eq] gl) - |_ -> errorstrm (Pp.str "Too many names in intro pattern") in - intro_eq - | Some (IPatId ipat) -> - let name gl = mk_anon_id "K" gl in - let intro_lhs gl = +(* Common code to handle generalization lists along with the defective case *) +let with_defective maintac deps clr = Goal.enter begin fun g -> + let sigma, concl = Goal.(sigma g, concl g) in + let top_id = + match EConstr.kind_of_type sigma concl with + | Term.ProdType (Name id, _, _) + when Ssrcommon.is_discharged_id id -> id + | _ -> Ssrcommon.top_id in + let top_gen = Ssrequality.mkclr clr, Ssrmatching.cpattern_of_id top_id in + Ssrcommon.tclINTRO_ID top_id <*> maintac deps top_gen +end + +let with_dgens { dgens; gens; clr } maintac = match gens with + | [] -> with_defective maintac dgens clr + | gen :: gens -> + V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, clr)) <*> maintac dgens gen + +let mkCoqEq env sigma = + let eq = Coqlib.((build_coq_eq_data ()).eq) in + let sigma, eq = EConstr.fresh_global env sigma eq in + eq, sigma + +let mkCoqRefl t c env sigma = + let refl = Coqlib.((build_coq_eq_data()).refl) in + let sigma, refl = EConstr.fresh_global env sigma refl in + EConstr.mkApp (refl, [|t; c|]), sigma + +(** Intro patterns processing for elim tactic, in particular when used in + conjunction with equation generation as in [elim E: x] *) +let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr = + let intro_eq = + match eqid with + | Some (IPatId ipat) when not is_rec -> + let rec intro_eq () = Goal.enter begin fun g -> + let sigma, env, concl = Goal.(sigma g, env g, concl g) in + match EConstr.kind_of_type sigma concl with + | Term.ProdType (_, src, tgt) -> begin + match EConstr.kind_of_type sigma src with + | Term.AtomicType (hd, _) when Ssrcommon.is_protect hd env sigma -> + V82.tactic ~nf_evars:false Ssrcommon.unprotecttac <*> + Ssrcommon.tclINTRO_ID ipat + | _ -> Ssrcommon.tclINTRO_ANON <*> intro_eq () + end + |_ -> Ssrcommon.errorstrm (Pp.str "Too many names in intro pattern") + end in + intro_eq () + | Some (IPatId ipat) -> + let intro_lhs = Goal.enter begin fun g -> + let sigma = Goal.sigma g in let elim_name = match clr, what with | [SsrHyp(_, x)], _ -> x - | _, `EConstr(_,_,t) when EConstr.isVar (project gl) t -> EConstr.destVar (project gl) t - | _ -> name gl in - if is_name_in_ipats elim_name ipats then introid (name gl) gl - else introid elim_name gl - in - let rec gen_eq_tac gl = - let concl = pf_concl gl in - let ctx, last = EConstr.decompose_prod_assum (project gl) concl in - let args = match EConstr.kind_of_type (project gl) last with - | AtomicType (hd, args) -> assert(EConstr.eq_constr (project gl) hd protectC); args + | _, `EConstr(_,_,t) when EConstr.isVar sigma t -> + EConstr.destVar sigma t + | _ -> Ssrcommon.mk_anon_id "K" (Tacmach.New.pf_ids_of_hyps g) in + let elim_name = + if Ssrcommon.is_name_in_ipats elim_name ipats then + Ssrcommon.mk_anon_id "K" (Tacmach.New.pf_ids_of_hyps g) + else elim_name + in + Ssrcommon.tclINTRO_ID elim_name + end in + let rec gen_eq_tac () = Goal.enter begin fun g -> + let sigma, env, concl = Goal.(sigma g, env g, concl g) in + let sigma, eq = + EConstr.fresh_global env sigma (Coqlib.build_coq_eq ()) in + let ctx, last = EConstr.decompose_prod_assum sigma concl in + let args = match EConstr.kind_of_type sigma last with + | Term.AtomicType (hd, args) -> + assert(Ssrcommon.is_protect hd env sigma); + args | _ -> assert false in let case = args.(Array.length args-1) in - if not(EConstr.Vars.closed0 (project gl) case) then Tacticals.tclTHEN Ssrcommon.intro_anon gen_eq_tac gl + if not(EConstr.Vars.closed0 sigma case) + then Ssrcommon.tclINTRO_ANON <*> gen_eq_tac () else - let gl, case_ty = pfe_type_of gl case in - let refl = EConstr.mkApp (eq, [|EConstr.Vars.lift 1 case_ty; EConstr.mkRel 1; EConstr.Vars.lift 1 case|]) in - let new_concl = fire_subst gl - EConstr.(mkProd (Name (name gl), case_ty, mkArrow refl (Vars.lift 2 concl))) in - let erefl, gl = mkRefl case_ty case gl in - let erefl = fire_subst gl erefl in - apply_type new_concl [case;erefl] gl in - Tacticals.tclTHENLIST [gen_eq_tac; intro_lhs; introid ipat] - | _ -> Tacticals.tclIDTAC in - let unprot = if eqid <> None && is_rec then unprotecttac else Tacticals.tclIDTAC in - tclEQINTROS ?ist ssrelim (Tacticals.tclTHENLIST [intro_eq; unprot]) ipats gl - -(* General case *) -let tclINTROS ist t ip = tclEQINTROS ~ist (t ist) tclIDTAC ip - -(* }}} *) - -let viewmovetac ?next v deps gen ist gl = - with_fresh_ctx - (tclTHEN_a - (viewmovetac_aux ?next true (ref top_id) v deps gen ist) - clear_wilds_and_tmp_and_delayed_ids) - gl - -let mkCoqEq gl = - let sigma = project gl in - let (sigma, eq) = EConstr.fresh_global (pf_env gl) sigma (build_coq_eq_data()).eq in - let gl = { gl with sigma } in - eq, gl - -let mkEq dir cl c t n gl = - let open EConstr in - let eqargs = [|t; c; c|] in eqargs.(dir_org dir) <- mkRel n; - let eq, gl = mkCoqEq gl in - let refl, gl = mkRefl t c gl in - mkArrow (mkApp (eq, eqargs)) (EConstr.Vars.lift 1 cl), refl, gl - -let pushmoveeqtac cl c gl = + Ssrcommon.tacTYPEOF case >>= fun case_ty -> + let open EConstr in + let refl = + mkApp (eq, [|Vars.lift 1 case_ty; mkRel 1; Vars.lift 1 case|]) in + let name = Ssrcommon.mk_anon_id "K" (Tacmach.New.pf_ids_of_hyps g) in + + let new_concl = + mkProd (Name name, case_ty, mkArrow refl (Vars.lift 2 concl)) in + let erefl, sigma = mkCoqRefl case_ty case env sigma in + Proofview.Unsafe.tclEVARS sigma <*> + Tactics.apply_type ~typecheck:true new_concl [case;erefl] + end in + gen_eq_tac () <*> + intro_lhs <*> + Ssrcommon.tclINTRO_ID ipat + | _ -> tclUNIT () in + let unprot = + if eqid <> None && is_rec + then V82.tactic ~nf_evars:false Ssrcommon.unprotecttac else tclUNIT () in + V82.of_tactic begin + V82.tactic ~nf_evars:false ssrelim <*> + tclIPAT_EQ (intro_eq <*> unprot) ipats + end + +let mkEq dir cl c t n env sigma = let open EConstr in - let x, t, cl1 = destProd (project gl) cl in - let cl2, eqc, gl = mkEq R2L cl1 c t 1 gl in - apply_type (mkProd (x, t, cl2)) [c; eqc] gl - -let eqmovetac _ gen ist gl = - let cl, c, _, gl = pf_interp_gen ist gl false gen in pushmoveeqtac cl c gl - -let movehnftac gl = match EConstr.kind (project gl) (pf_concl gl) with - | Prod _ | LetIn _ -> tclIDTAC gl - | _ -> new_tac hnf_in_concl gl + let eqargs = [|t; c; c|] in + eqargs.(Ssrequality.dir_org dir) <- mkRel n; + let eq, sigma = mkCoqEq env sigma in + let refl, sigma = mkCoqRefl t c env sigma in + mkArrow (mkApp (eq, eqargs)) (Vars.lift 1 cl), refl, sigma + +(** in [tac/v: last gens..] the first (last to be run) generalization is + "special" in that is it also the main argument of [tac] and is eventually + to be processed forward with view [v]. The behavior implemented is + very close to [tac: (v last) gens..] but: + - [v last] may use a view adaptor + - eventually clear for [last] is taken into account + - [tac/v {clr}] is also supported, and [{clr}] is to be run later + The code here does not "grab" [v last] nor apply [v] to [last], see the + [tacVIEW_THEN_GRAB] combinator. *) +let tclLAST_GEN ~to_ind ((oclr, occ), t) conclusion = tclINDEPENDENTL begin + Ssrcommon.tacSIGMA >>= fun sigma0 -> + Goal.enter_one begin fun g -> + let pat = Ssrmatching.interp_cpattern sigma0 t None in + let cl0, env, sigma, hyps = Goal.(concl g, env g, sigma g, hyps g) in + let cl = EConstr.to_constr sigma cl0 in + let (c, ucst), cl = + try Ssrmatching.fill_occ_pattern ~raise_NoMatch:true env sigma cl pat occ 1 + with Ssrmatching.NoMatch -> Ssrmatching.redex_of_pattern env pat, cl in + let sigma = Evd.merge_universe_context sigma ucst in + let c, cl = EConstr.of_constr c, EConstr.of_constr cl in + let clr = + Ssrcommon.interp_clr sigma (oclr, (Ssrmatching.tag_of_cpattern t,c)) in + (* Historically in Coq, and hence in ssr, [case t] accepts [t] of type + [A.. -> Ind] and opens new goals for [A..] as well as for the branches + of [Ind], see the [~to_ind] argument *) + if not(Termops.occur_existential sigma c) then + if Ssrmatching.tag_of_cpattern t = Ssrprinters.xWithAt then + if not (EConstr.isVar sigma c) then + Ssrcommon.errorstrm Pp.(str "@ can be used with variables only") + else match Context.Named.lookup (EConstr.destVar sigma c) hyps with + | Context.Named.Declaration.LocalAssum _ -> + Ssrcommon.errorstrm Pp.(str "@ can be used with let-ins only") + | Context.Named.Declaration.LocalDef (name, b, ty) -> + Unsafe.tclEVARS sigma <*> + tclUNIT (true, EConstr.mkLetIn (Name name,b,ty,cl), c, clr) + else + Unsafe.tclEVARS sigma <*> + Ssrcommon.tacMKPROD c cl >>= fun ccl -> + tclUNIT (false, ccl, c, clr) + else + if to_ind && occ = None then + let _, p, _, ucst' = + (* TODO: use abs_evars2 *) + Ssrcommon.pf_abs_evars sigma0 (fst pat, c) in + let sigma = Evd.merge_universe_context sigma ucst' in + Unsafe.tclEVARS sigma <*> + Ssrcommon.tacTYPEOF p >>= fun pty -> + (* TODO: check bug: cl0 no lift? *) + let ccl = EConstr.mkProd (Ssrcommon.constr_name sigma c, pty, cl0) in + tclUNIT (false, ccl, p, clr) + else + Ssrcommon.errorstrm Pp.(str "generalized term didn't match") +end end >>= begin + fun infos -> tclDISPATCH (infos |> List.map conclusion) +end + +(** a typical mate of [tclLAST_GEN] doing the job of applying the views [cs] + to [c] and generalizing the resulting term *) +let tacVIEW_THEN_GRAB ?(simple_types=true) + vs ~conclusion (is_letin, new_concl, c, clear) += + Ssrview.tclWITH_FWD_VIEWS ~simple_types ~subject:c ~views:vs + ~conclusion:(fun t -> + Ssrcommon.tacCONSTR_NAME c >>= fun name -> + Goal.enter_one ~__LOC__ begin fun g -> + let sigma, env = Goal.sigma g, Goal.env g in + Ssrcommon.tacMKPROD t ~name + (Termops.subst_term sigma t (* NOTE: we grab t here *) + (Termops.prod_applist sigma new_concl [c])) >>= + conclusion is_letin t clear + end) + +(* Elim views are elimination lemmas, so the eliminated term is not added *) +(* to the dependent terms as for "case", unless it actually occurs in the *) +(* goal, the "all occurrences" {+} switch is used, or the equation switch *) +(* is used and there are no dependents. *) + +let ssrelimtac (view, (eqid, (dgens, ipats))) = + let ndefectelimtac view eqid ipats deps gen = + match view with + | [v] -> + Ssrcommon.tclINTERP_AST_CLOSURE_TERM_AS_CONSTR v >>= fun cs -> + tclDISPATCH (List.map (fun elim -> + V82.tactic ~nf_evars:false + (Ssrelim.ssrelim deps (`EGen gen) ~elim eqid (elim_intro_tac ipats))) + cs) + | [] -> + tclINDEPENDENT + (V82.tactic ~nf_evars:false + (Ssrelim.ssrelim deps (`EGen gen) eqid (elim_intro_tac ipats))) + | _ -> + Ssrcommon.errorstrm + Pp.(str "elim: only one elimination lemma can be provided") + in + with_dgens dgens (ndefectelimtac view eqid ipats) + +let ssrcasetac (view, (eqid, (dgens, ipats))) = + let ndefectcasetac view eqid ipats deps ((_, occ), _ as gen) = + tclLAST_GEN ~to_ind:true gen (fun (_, cl, c, clear as info) -> + let conclusion _ vc _clear _cl = + Ssrcommon.tacIS_INJECTION_CASE vc >>= fun inj -> + let simple = (eqid = None && deps = [] && occ = None) in + if simple && inj then + V82.tactic ~nf_evars:false (Ssrelim.perform_injection vc) <*> + Tactics.clear (List.map Ssrcommon.hyp_id clear) <*> + tclIPATssr ipats + else + (* macro for "case/v E: x" ---> "case E: x / (v x)" *) + let deps, clear, occ = + if view <> [] && eqid <> None && deps = [] + then [gen], [], None + else deps, clear, occ in + V82.tactic ~nf_evars:false + (Ssrelim.ssrelim ~is_case:true deps (`EConstr (clear, occ, vc)) + eqid (elim_intro_tac ipats)) + in + if view = [] then conclusion false c clear c + else tacVIEW_THEN_GRAB ~simple_types:false view ~conclusion info) + in + with_dgens dgens (ndefectcasetac view eqid ipats) + +let ssrscasetoptac = Ssrcommon.tclWITHTOP Ssrelim.ssrscase_or_inj_tac +let ssrselimtoptac = Ssrcommon.tclWITHTOP Ssrelim.elimtac + +(** [move] **************************************************************) +let pushmoveeqtac cl c = Goal.enter begin fun g -> + let env, sigma = Goal.(env g, sigma g) in + let x, t, cl1 = EConstr.destProd sigma cl in + let cl2, eqc, sigma = mkEq R2L cl1 c t 1 env sigma in + Unsafe.tclEVARS sigma <*> + Tactics.apply_type ~typecheck:true (EConstr.mkProd (x, t, cl2)) [c; eqc] +end + +let eqmovetac _ gen = Goal.enter begin fun g -> + Ssrcommon.tacSIGMA >>= fun gl -> + let cl, c, _, gl = Ssrcommon.pf_interp_gen gl false gen in + Unsafe.tclEVARS (Tacmach.project gl) <*> + pushmoveeqtac cl c +end let rec eqmoveipats eqpat = function - | (IPatSimpl _ | IPatClear _ as ipat) :: ipats -> ipat :: eqmoveipats eqpat ipats - | (IPatAnon All :: _ | []) as ipats -> IPatAnon One :: eqpat :: ipats - | ipat :: ipats -> ipat :: eqpat :: ipats - -let ssrmovetac ist = function - | _::_ as view, (_, (dgens, ipats)) -> - let next = ref ipats in - let dgentac = with_dgens dgens (viewmovetac ~next (true, view)) ist in - tclTHEN dgentac (fun gl -> introstac ~ist !next gl) + | (IPatSimpl _ | IPatClear _ as ipat) :: ipats -> + ipat :: eqmoveipats eqpat ipats + | (IPatAnon All :: _ | []) as ipats -> + IPatAnon One :: eqpat :: ipats + | ipat :: ipats -> + ipat :: eqpat :: ipats + +let ssrsmovetac = Goal.enter begin fun g -> + let sigma, concl = Goal.(sigma g, concl g) in + match EConstr.kind sigma concl with + | Term.Prod _ | Term.LetIn _ -> tclUNIT () + | _ -> Tactics.hnf_in_concl +end + +let tclIPAT ip = + Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip)); + IpatMachine.main ~first_case_is_dispatch:false ip + +let ssrmovetac = function + | _::_ as view, (_, ({ gens = lastgen :: gens; clr }, ipats)) -> + let gentac = V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, [])) in + let conclusion _ t clear ccl = + Tactics.apply_type ~typecheck:true ccl [t] <*> + Tactics.clear (List.map Ssrcommon.hyp_id clear) in + gentac <*> + tclLAST_GEN ~to_ind:false lastgen + (tacVIEW_THEN_GRAB view ~conclusion) <*> + tclIPAT (IPatClear clr :: ipats) + | _::_ as view, (_, ({ gens = []; clr }, ipats)) -> + tclIPAT (IPatView view :: IPatClear clr :: ipats) | _, (Some pat, (dgens, ipats)) -> - let dgentac = with_dgens dgens eqmovetac ist in - tclTHEN dgentac (introstac ~ist (eqmoveipats pat ipats)) - | _, (_, (([gens], clr), ipats)) -> - let gentac = genstac (gens, clr) ist in - tclTHEN gentac (introstac ~ist ipats) - | _, (_, ((_, clr), ipats)) -> - tclTHENLIST [movehnftac; cleartac clr; introstac ~ist ipats] - -let ssrcasetac ist (view, (eqid, (dgens, ipats))) = - let ndefectcasetac view eqid ipats deps ((_, occ), _ as gen) ist gl = - let simple = (eqid = None && deps = [] && occ = None) in - let cl, c, clr, gl = pf_interp_gen ist gl true gen in - let _,vc, gl = - if view = [] then c,c, gl else pf_with_view_linear ist gl (false, view) cl c in - if simple && is_injection_case vc gl then - tclTHENLIST [perform_injection vc; cleartac clr; introstac ~ist ipats] gl - else - (* macro for "case/v E: x" ---> "case E: x / (v x)" *) - let deps, clr, occ = - if view <> [] && eqid <> None && deps = [] then [gen], [], None - else deps, clr, occ in - ssrelim ~is_case:true ~ist deps (`EConstr (clr,occ, vc)) eqid (elim_intro_tac ipats) gl + let dgentac = with_dgens dgens eqmovetac in + dgentac <*> tclIPAT (eqmoveipats pat ipats) + | _, (_, ({ gens = (_ :: _ as gens); dgens = []; clr}, ipats)) -> + let gentac = V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, clr)) in + gentac <*> tclIPAT ipats + | _, (_, ({ clr }, ipats)) -> + Tacticals.New.tclTHENLIST [ssrsmovetac; Tactics.clear (List.map Ssrcommon.hyp_id clr); tclIPAT ipats] + +(** [abstract: absvar gens] **************************************************) +let rec is_Evar_or_CastedMeta sigma x = + EConstr.isEvar sigma x || + EConstr.isMeta sigma x || + (EConstr.isCast sigma x && + is_Evar_or_CastedMeta sigma (pi1 (EConstr.destCast sigma x))) + +let occur_existential_or_casted_meta sigma c = + let rec occrec c = match EConstr.kind sigma c with + | Term.Evar _ -> raise Not_found + | Term.Cast (m,_,_) when EConstr.isMeta sigma m -> raise Not_found + | _ -> EConstr.iter sigma occrec c in - with_dgens dgens (ndefectcasetac view eqid ipats) ist - -let ssrapplytac ist (views, (_, ((gens, clr), intros))) = - tclINTROS ist (inner_ssrapplytac views gens clr) intros - + try occrec c; false + with Not_found -> true + +let tacEXAMINE_ABSTRACT id = Ssrcommon.tacTYPEOF id >>= begin fun tid -> + Ssrcommon.tacMK_SSR_CONST "abstract" >>= fun abstract -> + Goal.enter_one ~__LOC__ begin fun g -> + let sigma, env = Goal.(sigma g, env g) in + let err () = + Ssrcommon.errorstrm + Pp.(strbrk"not a proper abstract constant: "++ + Printer.pr_econstr_env env sigma id) in + if not (EConstr.isApp sigma tid) then err (); + let hd, args_id = EConstr.destApp sigma tid in + if not (EConstr.eq_constr_nounivs sigma hd abstract) then err (); + if Array.length args_id <> 3 then err (); + if not (is_Evar_or_CastedMeta sigma args_id.(2)) then + Ssrcommon.errorstrm Pp.(strbrk"abstract constant "++ + Printer.pr_econstr_env env sigma id++str" already used"); + tclUNIT (tid, args_id) +end end + +let tacFIND_ABSTRACT_PROOF check_lock abstract_n = + Ssrcommon.tacMK_SSR_CONST "abstract" >>= fun abstract -> + Goal.enter_one ~__LOC__ begin fun g -> + let sigma, env = Goal.(sigma g, env g) in + let l = Evd.fold_undefined (fun e ei l -> + match EConstr.kind sigma (EConstr.of_constr ei.Evd.evar_concl) with + | Term.App(hd, [|ty; n; lock|]) + when (not check_lock || + (occur_existential_or_casted_meta sigma ty && + is_Evar_or_CastedMeta sigma lock)) && + EConstr.eq_constr_nounivs sigma hd abstract && + EConstr.eq_constr_nounivs sigma n abstract_n -> e :: l + | _ -> l) sigma [] in + match l with + | [e] -> tclUNIT e + | _ -> Ssrcommon.errorstrm + Pp.(strbrk"abstract constant "++ + Printer.pr_econstr_env env sigma abstract_n ++ + strbrk" not found in the evar map exactly once. "++ + strbrk"Did you tamper with it?") +end + +let ssrabstract dgens = + let main _ (_,cid) = Goal.enter begin fun g -> + Ssrcommon.tacMK_SSR_CONST "abstract" >>= fun abstract -> + Ssrcommon.tacMK_SSR_CONST "abstract_key" >>= fun abstract_key -> + Ssrcommon.tacINTERP_CPATTERN cid >>= fun cid -> + let id = EConstr.mkVar (Option.get (Ssrmatching.id_of_pattern cid)) in + tacEXAMINE_ABSTRACT id >>= fun (idty, args_id) -> + let abstract_n = args_id.(1) in + tacFIND_ABSTRACT_PROOF true abstract_n >>= fun abstract_proof -> + let tacFIND_HOLE = Goal.enter_one ~__LOC__ begin fun g -> + let sigma, env, concl = Goal.(sigma g, env g, concl g) in + let t = args_id.(0) in + match EConstr.kind sigma t with + | (Term.Evar _ | Term.Meta _) -> Ssrcommon.tacUNIFY concl t <*> tclUNIT id + | Term.Cast(m,_,_) + when EConstr.isEvar sigma m || EConstr.isMeta sigma m -> + Ssrcommon.tacUNIFY concl t <*> tclUNIT id + | _ -> + Ssrcommon.errorstrm + Pp.(strbrk"abstract constant "++ + Printer.pr_econstr_env env sigma abstract_n ++ + strbrk" has an unexpected shape. Did you tamper with it?") + end in + tacFIND_HOLE >>= fun proof -> + Ssrcommon.tacUNIFY abstract_key args_id.(2) <*> + Ssrcommon.tacTYPEOF idty >>= fun _ -> + Unsafe.tclGETGOALS >>= fun goals -> + (* Here we jump in the proof tree: we move from the current goal to + the evar that inhabits the abstract variable with the current goal *) + Unsafe.tclSETGOALS + (goals @ [Proofview_monad.with_empty_state abstract_proof]) <*> + tclDISPATCH [ + Tacticals.New.tclSOLVE [Tactics.apply proof]; + Ssrcommon.unfold[abstract;abstract_key] + ] + end in + let interp_gens { gens } ~conclusion = Goal.enter begin fun g -> + Ssrcommon.tacSIGMA >>= fun gl0 -> + let open Ssrmatching in + let ipats = List.map (fun (_,cp) -> + match id_of_pattern (interp_cpattern gl0 cp None) with + | None -> IPatAnon One + | Some id -> IPatId id) + (List.tl gens) in + conclusion ipats + end in + interp_gens dgens ~conclusion:(fun ipats -> + with_dgens dgens main <*> + tclIPATssr ipats) + +module Internal = struct + + let pf_find_abstract_proof b gl t = + let res = ref None in + let _ = V82.of_tactic (tacFIND_ABSTRACT_PROOF b (EConstr.of_constr t) >>= fun x -> res := Some x; tclUNIT ()) gl in + match !res with + | None -> assert false + | Some x -> x + + let examine_abstract t gl = + let res = ref None in + let _ = V82.of_tactic (tacEXAMINE_ABSTRACT t >>= fun x -> res := Some x; tclUNIT ()) gl in + match !res with + | None -> assert false + | Some x -> x + +end (* vim: set filetype=ocaml foldmethod=marker: *) |