(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) (* This line is read by the Makefile's dist target: do not remove. *) let ssrversion = "1.6";; let ssrAstVersion = 1;; let () = Mltop.add_known_plugin (fun () -> if Flags.is_verbose () && not !Flags.batch_mode then begin Printf.printf "\nSmall Scale Reflection version %s loaded.\n" ssrversion; Printf.printf "Copyright 2005-2012 Microsoft Corporation and INRIA.\n"; Printf.printf "Distributed under the terms of the CeCILL-B license.\n\n" end) "ssreflect" ;; (* Defining grammar rules with "xx" in it automatically declares keywords too *) let frozen_lexer = Lexer.freeze () ;; (*i camlp4use: "pa_extend.cmo" i*) (*i camlp4deps: "parsing/grammar.cma" i*) open Names open Pp open Pcoq open Genarg open Term open Topconstr open Libnames open Tactics open Tacticals open Termops open Namegen open Recordops open Tacmach open Coqlib open Glob_term open Util open Evd open Extend open Goptions open Tacexpr open Tacinterp open Pretyping.Default open Constr open Tactic open Extraargs open Ppconstr open Printer open Compat open Tok open Ssrmatching (** look up a name in the ssreflect internals module *) let ssrdirpath = make_dirpath [id_of_string "ssreflect"] let ssrqid name = make_qualid ssrdirpath (id_of_string name) let ssrtopqid name = make_short_qualid (id_of_string name) let locate_reference qid = Smartlocate.global_of_extended_global (Nametab.locate_extended qid) let mkSsrRef name = try locate_reference (ssrqid name) with Not_found -> try locate_reference (ssrtopqid name) with Not_found -> error "Small scale reflection library not loaded" let mkSsrRRef name = GRef (dummy_loc, mkSsrRef name) let mkSsrConst name = constr_of_reference (mkSsrRef name) let loc_error loc msg = user_err_loc (loc, msg, str msg) let errorstrm = errorlabstrm "ssreflect" (** Ssreflect load check. *) (* To allow ssrcoq to be fully compatible with the "plain" Coq, we only *) (* turn on its incompatible features (the new rewrite syntax, and the *) (* reserved identifiers) when the theory library (ssreflect.v) has *) (* has actually been required, or is being defined. Because this check *) (* needs to be done often (for each identifier lookup), we implement *) (* some caching, repeating the test only when the environment changes. *) (* We check for protect_term because it is the first constant loaded; *) (* ssr_have would ultimately be a better choice. *) let ssr_loaded = let cache = ref (Global.safe_env (), false) in fun () -> Lexer.is_keyword "is" && let new_lbl = Global.safe_env () in match !cache with | lbl, loaded when lbl == new_lbl -> loaded | _ -> let loaded = (try ignore (mkSsrRef "protect_term"); true with _ -> false) in cache := new_lbl, loaded; loaded (* 0 cost pp function. Active only if env variable SSRDEBUG is set *) (* or if SsrDebug is Set *) let pp_ref = ref (fun _ -> ()) let ssr_pp s = pperrnl (str"SSR: "++Lazy.force s) let _ = try ignore(Sys.getenv "SSRDEBUG"); pp_ref := ssr_pp with Not_found -> () let _ = Goptions.declare_bool_option { Goptions.optsync = false; Goptions.optname = "ssreflect debugging"; Goptions.optkey = ["SsrDebug"]; Goptions.optdepr = false; Goptions.optread = (fun _ -> !pp_ref == ssr_pp); Goptions.optwrite = (fun b -> Ssrmatching.debug b; if b then pp_ref := ssr_pp else pp_ref := fun _ -> ()) } let pp s = !pp_ref s (** Utils {{{ *****************************************************************) let env_size env = List.length (Environ.named_context env) let safeDestApp c = match kind_of_term c with App (f, a) -> f, a | _ -> c, [| |] let get_index = function ArgArg i -> i | _ -> anomaly "Uninterpreted index" (* Toplevel constr must be globalized twice ! *) let glob_constr ist gsigma genv = function | _, Some ce -> let ltacvars = List.map fst ist.lfun, [] in Constrintern.intern_gen false ~ltacvars:ltacvars gsigma genv ce | rc, None -> rc (* Term printing utilities functions for deciding bracketing. *) let pr_paren prx x = hov 1 (str "(" ++ prx x ++ str ")") (* String lexing utilities *) let skip_wschars s = let rec loop i = match s.[i] with '\n'..' ' -> loop (i + 1) | _ -> i in loop let skip_numchars s = let rec loop i = match s.[i] with '0'..'9' -> loop (i + 1) | _ -> i in loop (* We also guard characters that might interfere with the ssreflect *) (* tactic syntax. *) let guard_term ch1 s i = match s.[i] with | '(' -> false | '{' | '/' | '=' -> true | _ -> ch1 = '(' (* The call 'guard s i' should return true if the contents of s *) (* starting at i need bracketing to avoid ambiguities. *) let pr_guarded guard prc c = msg_with Format.str_formatter (prc c); let s = Format.flush_str_formatter () ^ "$" in if guard s (skip_wschars s 0) then pr_paren prc c else prc c (* More sensible names for constr printers *) let prl_constr = pr_lconstr let pr_constr = pr_constr let prl_glob_constr c = pr_lglob_constr_env (Global.env ()) c let pr_glob_constr c = pr_glob_constr_env (Global.env ()) c let prl_constr_expr = pr_lconstr_expr let pr_constr_expr = pr_constr_expr let prl_glob_constr_and_expr = function | _, Some c -> prl_constr_expr c | c, None -> prl_glob_constr c let pr_glob_constr_and_expr = function | _, Some c -> pr_constr_expr c | c, None -> pr_glob_constr c let pr_term (k, c) = pr_guarded (guard_term k) pr_glob_constr_and_expr c let prl_term (k, c) = pr_guarded (guard_term k) prl_glob_constr_and_expr c (** Adding a new uninterpreted generic argument type *) let add_genarg tag pr = let wit, globwit, rawwit as wits = create_arg None tag in let glob _ rarg = in_gen globwit (out_gen rawwit rarg) in let interp _ gl garg = Tacmach.project gl,in_gen wit (out_gen globwit garg) in let subst _ garg = garg in add_interp_genarg tag (glob, interp, subst); let gen_pr _ _ _ = pr in Pptactic.declare_extra_genarg_pprule (rawwit, gen_pr) (globwit, gen_pr) (wit, gen_pr); wits (** Constructors for cast type *) let dC t = CastConv (DEFAULTcast,t) (** Constructors for constr_expr *) let mkCProp loc = CSort (loc, GProp Null) let mkCType loc = CSort (loc, GType None) let mkCVar loc id = CRef (Ident (loc, id)) let isCVar = function CRef (Ident _) -> true | _ -> false let destCVar = function CRef (Ident (_, id)) -> id | _ -> anomaly "not a CRef" let rec mkCHoles loc n = if n <= 0 then [] else CHole (loc, None) :: mkCHoles loc (n - 1) let mkCHole loc = CHole (loc, None) let rec isCHoles = function CHole _ :: cl -> isCHoles cl | cl -> cl = [] let mkCExplVar loc id n = CAppExpl (loc, (None, Ident (loc, id)), mkCHoles loc n) let mkCLambda loc name ty t = CLambdaN (loc, [[loc, name], Default Explicit, ty], t) let mkCLetIn loc name bo t = CLetIn (loc, (loc, name), bo, t) let mkCArrow loc ty t = CProdN (loc, [[dummy_loc,Anonymous], Default Explicit, ty], t) let mkCCast loc t ty = CCast (loc,t, dC ty) (** Constructors for rawconstr *) let mkRHole = GHole (dummy_loc, InternalHole) let rec mkRHoles n = if n > 0 then mkRHole :: mkRHoles (n - 1) else [] let rec isRHoles = function GHole _ :: cl -> isRHoles cl | cl -> cl = [] let mkRApp f args = if args = [] then f else GApp (dummy_loc, f, args) let mkRVar id = GRef (dummy_loc, VarRef id) let mkRltacVar id = GVar (dummy_loc, id) let mkRCast rc rt = GCast (dummy_loc, rc, dC rt) let mkRType = GSort (dummy_loc, GType None) let mkRProp = GSort (dummy_loc, GProp Null) let mkRArrow rt1 rt2 = GProd (dummy_loc, Anonymous, Explicit, rt1, rt2) let mkRConstruct c = GRef (dummy_loc, ConstructRef c) let mkRInd mind = GRef (dummy_loc, IndRef mind) let mkRLambda n s t = GLambda (dummy_loc, n, Explicit, s, t) (** Constructors for constr *) let mkAppRed f c = match kind_of_term f with | Lambda (_, _, b) -> subst1 c b | _ -> mkApp (f, [|c|]) let mkProt t c = mkApp (mkSsrConst "protect_term", [|t; c|]) let mkRefl t c = mkApp ((build_coq_eq_data()).refl, [|t; c|]) (* Application to a sequence of n rels (for building eta-expansions). *) (* The rel indices decrease down to imin (inclusive), unless n < 0, *) (* in which case they're incresing (from imin). *) let mkEtaApp c n imin = if n = 0 then c else let nargs, mkarg = if n < 0 then -n, (fun i -> mkRel (imin + i)) else let imax = imin + n - 1 in n, (fun i -> mkRel (imax - i)) in mkApp (c, Array.init nargs mkarg) (* Same, but optimizing head beta redexes *) let rec whdEtaApp c n = if n = 0 then c else match kind_of_term c with | Lambda (_, _, c') -> whdEtaApp c' (n - 1) | _ -> mkEtaApp (lift n c) n 1 let mkType () = mkType (Univ.fresh_local_univ ()) (* ssrterm conbinators *) let combineCG t1 t2 f g = match t1, t2 with | (x, (t1, None)), (_, (t2, None)) -> x, (g t1 t2, None) | (x, (_, Some t1)), (_, (_, Some t2)) -> x, (mkRHole, Some (f t1 t2)) | _, (_, (_, None)) -> anomaly "have: mixed C-G constr" | _ -> anomaly "have: mixed G-C constr" let loc_ofCG = function | (_, (s, None)) -> loc_of_glob_constr s | (_, (_, Some s)) -> constr_loc s let mk_term k c = k, (mkRHole, Some c) let mk_lterm = mk_term ' ' (* Backport from coq trunk *) let array_smartfoldmap f accu (ar : 'a array) = let len = Array.length ar in let i = ref 0 in let break = ref true in let r = ref accu in (** This variable is never accessed unset *) let temp = ref None in while !break && (!i < len) do let v = Array.unsafe_get ar !i in let (accu, v') = f !r v in r := accu; if v == v' then incr i else begin break := false; temp := Some v'; end done; if !i < len then begin let ans : 'a array = Array.make len (Array.unsafe_get ar 0) in (** TODO: use unsafe_blit in 4.01 *) Array.blit ar 0 ans 0 !i; let v = match !temp with None -> assert false | Some x -> x in Array.unsafe_set ans !i v; incr i; while !i < len do let v = Array.unsafe_get ar !i in let (accu, v') = f !r v in r := accu; Array.unsafe_set ans !i v'; incr i done; !r, ans end else !r, ar let array_for_all2 f v1 v2 = let rec allrec = function | -1 -> true | n -> let ans = f (Array.unsafe_get v1 n) (Array.unsafe_get v2 n) in ans && (allrec (n-1)) in let lv1 = Array.length v1 in lv1 = Array.length v2 && allrec (pred lv1) let fold_left2 f a v1 v2 = let lv1 = Array.length v1 in let rec fold a n = if n >= lv1 then a else fold (f a (Array.unsafe_get v1 n) (Array.unsafe_get v2 n)) (succ n) in if Array.length v2 <> lv1 then invalid_arg "Array.fold_left2"; fold a 0 (* /Backport *) let map_fold_constr g f ctx acc cstr = let array_f ctx acc x = let x, acc = f ctx acc x in acc, x in match kind_of_term cstr with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> cstr, acc | Cast (c,k, t) -> let c', acc = f ctx acc c in let t', acc = f ctx acc t in (if c==c' && t==t' then cstr else mkCast (c', k, t')), acc | Prod (na,t,c) -> let t', acc = f ctx acc t in let c', acc = f (g (na,None,t) ctx) acc c in (if t==t' && c==c' then cstr else mkProd (na, t', c')), acc | Lambda (na,t,c) -> let t', acc = f ctx acc t in let c', acc = f (g (na,None,t) ctx) acc c in (if t==t' && c==c' then cstr else mkLambda (na, t', c')), acc | LetIn (na,b,t,c) -> let b', acc = f ctx acc b in let t', acc = f ctx acc t in let c', acc = f (g (na,Some b,t) ctx) acc c in (if b==b' && t==t' && c==c' then cstr else mkLetIn (na, b', t', c')), acc | App (c,al) -> let c', acc = f ctx acc c in let acc, al' = array_smartfoldmap (array_f ctx) acc al in (if c==c' && array_for_all2 (==) al al' then cstr else mkApp (c', al')), acc | Evar (e,al) -> let acc, al' = array_smartfoldmap (array_f ctx) acc al in (if array_for_all2 (==) al al' then cstr else mkEvar (e, al')), acc | Case (ci,p,c,bl) -> let p', acc = f ctx acc p in let c', acc = f ctx acc c in let acc, bl' = array_smartfoldmap (array_f ctx) acc bl in (if p==p' && c==c' && array_for_all2 (==) bl bl' then cstr else mkCase (ci, p', c', bl')), acc | Fix (ln,(lna,tl,bl)) -> let acc, tl' = array_smartfoldmap (array_f ctx) acc tl in let ctx' = array_fold_left2 (fun l na t -> g (na,None,t) l) ctx lna tl in let acc, bl' = array_smartfoldmap (array_f ctx') acc bl in (if array_for_all2 (==) tl tl' && array_for_all2 (==) bl bl' then cstr else mkFix (ln,(lna,tl',bl'))), acc | CoFix(ln,(lna,tl,bl)) -> let acc, tl' = array_smartfoldmap (array_f ctx) acc tl in let ctx' = array_fold_left2 (fun l na t -> g (na,None,t) l) ctx lna tl in let acc,bl' = array_smartfoldmap (array_f ctx') acc bl in (if array_for_all2 (==) tl tl' && array_for_all2 (==) bl bl' then cstr else mkCoFix (ln,(lna,tl',bl'))), acc (* }}} *) (** Profiling {{{ *************************************************************) type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b; reset : unit -> unit; print : unit -> unit } let profile_now = ref false let something_profiled = ref false let profilers = ref [] let add_profiler f = profilers := f :: !profilers;; let _ = Goptions.declare_bool_option { Goptions.optsync = false; Goptions.optname = "ssreflect profiling"; Goptions.optkey = ["SsrProfiling"]; Goptions.optread = (fun _ -> !profile_now); Goptions.optdepr = false; Goptions.optwrite = (fun b -> Ssrmatching.profile b; profile_now := b; if b then List.iter (fun f -> f.reset ()) !profilers; if not b then List.iter (fun f -> f.print ()) !profilers) } let () = let prof_total = let init = ref 0.0 in { profile = (fun f x -> assert false); reset = (fun () -> init := Unix.gettimeofday ()); print = (fun () -> if !something_profiled then prerr_endline (Printf.sprintf "!! %-39s %10d %9.4f %9.4f %9.4f" "total" 0 (Unix.gettimeofday() -. !init) 0.0 0.0)) } in let prof_legenda = { profile = (fun f x -> assert false); reset = (fun () -> ()); print = (fun () -> if !something_profiled then begin prerr_endline (Printf.sprintf "!! %39s ---------- --------- --------- ---------" (String.make 39 '-')); prerr_endline (Printf.sprintf "!! %-39s %10s %9s %9s %9s" "function" "#calls" "total" "max" "average") end) } in add_profiler prof_legenda; add_profiler prof_total ;; let mk_profiler s = let total, calls, max = ref 0.0, ref 0, ref 0.0 in let reset () = total := 0.0; calls := 0; max := 0.0 in let profile f x = if not !profile_now then f x else let before = Unix.gettimeofday () in try incr calls; let res = f x in let after = Unix.gettimeofday () in let delta = after -. before in total := !total +. delta; if delta > !max then max := delta; res with exc -> let after = Unix.gettimeofday () in let delta = after -. before in total := !total +. delta; if delta > !max then max := delta; raise exc in let print () = if !calls <> 0 then begin something_profiled := true; prerr_endline (Printf.sprintf "!! %-39s %10d %9.4f %9.4f %9.4f" s !calls !total !max (!total /. (float_of_int !calls))) end in let prof = { profile = profile; reset = reset; print = print } in add_profiler prof; prof ;; (* }}} *) let inVersion = Libobject.declare_object { (Libobject.default_object "SSRASTVERSION") with Libobject.load_function = (fun _ (_,v) -> if v <> ssrAstVersion then error "Please recompile your .vo files"); Libobject.classify_function = (fun v -> Libobject.Keep v); } let _ = Goptions.declare_bool_option { Goptions.optsync = false; Goptions.optname = "ssreflect version"; Goptions.optkey = ["SsrAstVersion"]; Goptions.optread = (fun _ -> true); Goptions.optdepr = false; Goptions.optwrite = (fun _ -> Lib.add_anonymous_leaf (inVersion ssrAstVersion)) } let tactic_expr = Tactic.tactic_expr let gallina_ext = Vernac_.gallina_ext let sprintf = Printf.sprintf let tactic_mode = G_vernac.tactic_mode (** 1. Utilities *) let ssroldreworder = ref true let _ = Goptions.declare_bool_option { Goptions.optsync = false; Goptions.optname = "ssreflect 1.3 compatibility flag"; Goptions.optkey = ["SsrOldRewriteGoalsOrder"]; Goptions.optread = (fun _ -> !ssroldreworder); Goptions.optdepr = false; Goptions.optwrite = (fun b -> ssroldreworder := b) } let ssrhaveNOtcresolution = ref false let inHaveTCResolution = Libobject.declare_object { (Libobject.default_object "SSRHAVETCRESOLUTION") with Libobject.cache_function = (fun (_,v) -> ssrhaveNOtcresolution := v); Libobject.load_function = (fun _ (_,v) -> ssrhaveNOtcresolution := v); Libobject.classify_function = (fun v -> Libobject.Keep v); } let _ = Goptions.declare_bool_option { Goptions.optsync = false; Goptions.optname = "have type classes"; Goptions.optkey = ["SsrHave";"NoTCResolution"]; Goptions.optread = (fun _ -> !ssrhaveNOtcresolution); Goptions.optdepr = false; Goptions.optwrite = (fun b -> Lib.add_anonymous_leaf (inHaveTCResolution b)) } (** Primitive parsing to avoid syntax conflicts with basic tactics. *) let accept_before_syms syms strm = match Compat.get_tok (stream_nth 1 strm) with | Tok.KEYWORD sym when List.mem sym syms -> () | _ -> raise Stream.Failure let accept_before_syms_or_any_id syms strm = match Compat.get_tok (stream_nth 1 strm) with | Tok.KEYWORD sym when List.mem sym syms -> () | Tok.IDENT _ -> () | _ -> raise Stream.Failure let accept_before_syms_or_ids syms ids strm = match Compat.get_tok (stream_nth 1 strm) with | Tok.KEYWORD sym when List.mem sym syms -> () | Tok.IDENT id when List.mem id ids -> () | _ -> raise Stream.Failure (** Pretty-printing utilities *) let pr_id = Ppconstr.pr_id let pr_name = function Name id -> pr_id id | Anonymous -> str "_" let pr_spc () = str " " let pr_bar () = Pp.cut() ++ str "|" let pr_list = prlist_with_sep let tacltop = (5,Ppextend.E) (** Tactic-level diagnosis *) let pf_pr_constr gl = pr_constr_env (pf_env gl) let pf_pr_glob_constr gl = pr_glob_constr_env (pf_env gl) (* debug *) let pf_msg gl = let ppgl = pr_lconstr_env (pf_env gl) (pf_concl gl) in msgnl (str "goal is " ++ ppgl) let msgtac gl = pf_msg gl; tclIDTAC gl (** Tactic utilities *) let last_goal gls = let sigma, gll = Refiner.unpackage gls in Refiner.repackage sigma (List.nth gll (List.length gll - 1)) let pf_type_id gl t = id_of_string (hdchar (pf_env gl) t) let not_section_id id = not (is_section_variable id) let is_pf_var c = isVar c && not_section_id (destVar c) let pf_ids_of_proof_hyps gl = let add_hyp (id, _, _) ids = if not_section_id id then id :: ids else ids in Sign.fold_named_context add_hyp (pf_hyps gl) ~init:[] let pf_nf_evar gl e = Reductionops.nf_evar (project gl) e let pf_partial_solution ?(shelve=false) gl t evl = let sigma, g = project gl, sig_it gl in let evars_of_term c = let rec evrec acc c = match kind_of_term c with | Evar (n, l) -> Evd.ExistentialSet.add n (Array.fold_left evrec acc l) | _ -> fold_constr evrec acc c in evrec Evd.ExistentialSet.empty c in let evars_of_named_context nc = List.fold_right (fun (_, b, t) s -> Option.fold_left (fun s t -> Evd.ExistentialSet.union s (evars_of_term t)) (Evd.ExistentialSet.union s (evars_of_term t)) b) nc Evd.ExistentialSet.empty in let evars_of_filtered_evar_info evi = Evd.ExistentialSet.union (evars_of_term evi.evar_concl) (Evd.ExistentialSet.union (match evi.evar_body with | Evar_empty -> Evd.ExistentialSet.empty | Evar_defined b -> evars_of_term b) (evars_of_named_context (evar_filtered_context evi))) in let depends_on src tgt = let evi = Evd.find sigma tgt in Evd.ExistentialSet.mem src (evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi)) in let occurs_in_another_statement ev = List.exists (fun x -> let ev', _ = destEvar x in not (ev = ev') && depends_on ev ev') evl in let sigma = Goal.V82.partial_solution sigma g t in re_sig (Util.list_map_filter (fun x -> let ev, _ = destEvar x in if shelve && occurs_in_another_statement ev then None else Some (Goal.build ev)) evl) sigma let pf_new_evar gl ty = let sigma, env, it = project gl, pf_env gl, sig_it gl in let sigma, extra = Evarutil.new_evar sigma env ty in re_sig it sigma, extra (* Basic tactics *) let convert_concl_no_check t = convert_concl_no_check t DEFAULTcast let convert_concl t = convert_concl t DEFAULTcast let reduct_in_concl t = reduct_in_concl (t, DEFAULTcast) let havetac id = pose_proof (Name id) let settac id c = letin_tac None (Name id) c None let posetac id cl = settac id cl nowhere let basecuttac name c = apply (mkApp (mkSsrConst name, [|c|])) (* we reduce head beta redexes *) let betared env = Closure.create_clos_infos (Closure.RedFlags.mkflags [Closure.RedFlags.fBETA]) env ;; let introid name = tclTHEN (fun gl -> let g, env = pf_concl gl, pf_env gl in match kind_of_term g with | App (hd, _) when isLambda hd -> let g = Closure.whd_val (betared env) (Closure.inject g) in convert_concl_no_check g gl | _ -> tclIDTAC gl) (intro_mustbe_force name) ;; (** Name generation {{{ *******************************************************) (* Since Coq now does repeated internal checks of its external lexical *) (* rules, we now need to carve ssreflect reserved identifiers out of *) (* out of the user namespace. We use identifiers of the form _id_ for *) (* this purpose, e.g., we "anonymize" an identifier id as _id_, adding *) (* an extra leading _ if this might clash with an internal identifier. *) (* We check for ssreflect identifiers in the ident grammar rule; *) (* when the ssreflect Module is present this is normally an error, *) (* but we provide a compatibility flag to reduce this to a warning. *) let ssr_reserved_ids = ref true let _ = Goptions.declare_bool_option { Goptions.optsync = true; Goptions.optname = "ssreflect identifiers"; Goptions.optkey = ["SsrIdents"]; Goptions.optdepr = false; Goptions.optread = (fun _ -> !ssr_reserved_ids); Goptions.optwrite = (fun b -> ssr_reserved_ids := b) } let is_ssr_reserved s = let n = String.length s in n > 2 && s.[0] = '_' && s.[n - 1] = '_' let internal_names = ref [] let add_internal_name pt = internal_names := pt :: !internal_names let is_internal_name s = List.exists (fun p -> p s) !internal_names let ssr_id_of_string loc s = if is_ssr_reserved s && ssr_loaded () then begin if !ssr_reserved_ids then loc_error loc ("The identifier " ^ s ^ " is reserved.") else if is_internal_name s then warning ("Conflict between " ^ s ^ " and ssreflect internal names.") else warning ( "The name " ^ s ^ " fits the _xxx_ format used for anonymous variables.\n" ^ "Scripts with explicit references to anonymous variables are fragile.") end; id_of_string s let ssr_null_entry = Gram.Entry.of_parser "ssr_null" (fun _ -> ()) GEXTEND Gram GLOBAL: Prim.ident; Prim.ident: [[ s = IDENT; ssr_null_entry -> ssr_id_of_string loc s ]]; END let mk_internal_id s = let s' = sprintf "_%s_" s in for i = 1 to String.length s do if s'.[i] = ' ' then s'.[i] <- '_' done; add_internal_name ((=) s'); id_of_string s' let same_prefix s t n = let rec loop i = i = n || s.[i] = t.[i] && loop (i + 1) in loop 0 let skip_digits s = let n = String.length s in let rec loop i = if i < n && is_digit s.[i] then loop (i + 1) else i in loop let mk_tagged_id t i = id_of_string (sprintf "%s%d_" t i) let is_tagged t s = let n = String.length s - 1 and m = String.length t in m < n && s.[n] = '_' && same_prefix s t m && skip_digits s m = n let perm_tag = "_perm_Hyp_" let _ = add_internal_name (is_tagged perm_tag) let mk_perm_id = let salt = ref 1 in fun () -> salt := !salt mod 10000 + 1; mk_tagged_id perm_tag !salt let evar_tag = "_evar_" let _ = add_internal_name (is_tagged evar_tag) let mk_evar_name n = Name (mk_tagged_id evar_tag n) let nb_evar_deps = function | Name id -> let s = string_of_id id in if not (is_tagged evar_tag s) then 0 else let m = String.length evar_tag in (try int_of_string (String.sub s m (String.length s - 1 - m)) with _ -> 0) | _ -> 0 let discharged_tag = "_discharged_" let mk_discharged_id id = id_of_string (sprintf "%s%s_" discharged_tag (string_of_id id)) let has_discharged_tag s = let m = String.length discharged_tag and n = String.length s - 1 in m < n && s.[n] = '_' && same_prefix s discharged_tag m let _ = add_internal_name has_discharged_tag let is_discharged_id id = has_discharged_tag (string_of_id id) let wildcard_tag = "_the_" let wildcard_post = "_wildcard_" let mk_wildcard_id i = id_of_string (sprintf "%s%s%s" wildcard_tag (ordinal i) wildcard_post) let has_wildcard_tag s = let n = String.length s in let m = String.length wildcard_tag in let m' = String.length wildcard_post in n < m + m' + 2 && same_prefix s wildcard_tag m && String.sub s (n - m') m' = wildcard_post && skip_digits s m = n - m' - 2 let _ = add_internal_name has_wildcard_tag let max_suffix m (t, j0 as tj0) id = let s = string_of_id id in let n = String.length s - 1 in let dn = String.length t - 1 - n in let i0 = j0 - dn in if not (i0 >= m && s.[n] = '_' && same_prefix s t m) then tj0 else let rec loop i = if i < i0 && s.[i] = '0' then loop (i + 1) else if (if i < i0 then skip_digits s i = n else le_s_t i) then s, i else tj0 and le_s_t i = let ds = s.[i] and dt = t.[i + dn] in if ds = dt then i = n || le_s_t (i + 1) else dt < ds && skip_digits s i = n in loop m let mk_anon_id t gl = let m, si0, id0 = let s = ref (sprintf "_%s_" t) in if is_internal_name !s then s := "_" ^ !s; let n = String.length !s - 1 in let rec loop i j = let d = !s.[i] in if not (is_digit d) then i + 1, j else loop (i - 1) (if d = '0' then j else i) in let m, j = loop (n - 1) n in m, (!s, j), id_of_string !s in let gl_ids = pf_ids_of_hyps gl in if not (List.mem id0 gl_ids) then id0 else let s, i = List.fold_left (max_suffix m) si0 gl_ids in let n = String.length s - 1 in let rec loop i = if s.[i] = '9' then (s.[i] <- '0'; loop (i - 1)) else if i < m then (s.[n] <- '0'; s.[m] <- '1'; s ^ "_") else (s.[i] <- Char.chr (Char.code s.[i] + 1); s) in id_of_string (loop (n - 1)) (* We must not anonymize context names discharged by the "in" tactical. *) let ssr_anon_hyp = "Hyp" let anontac (x, _, _) gl = let id = match x with | Name id -> if is_discharged_id id then id else mk_anon_id (string_of_id id) gl | _ -> mk_anon_id ssr_anon_hyp gl in introid id gl let rec constr_name c = match kind_of_term c with | Var id -> Name id | Cast (c', _, _) -> constr_name c' | Const cn -> Name (id_of_label (con_label cn)) | App (c', _) -> constr_name c' | _ -> Anonymous (* }}} *) (** Open term to lambda-term coercion {{{ ************************************) (* This operation takes a goal gl and an open term (sigma, t), and *) (* returns a term t' where all the new evars in sigma are abstracted *) (* with the mkAbs argument, i.e., for mkAbs = mkLambda then there is *) (* some duplicate-free array args of evars of sigma such that the *) (* term mkApp (t', args) is convertible to t. *) (* This makes a useful shorthand for local definitions in proofs, *) (* i.e., pose succ := _ + 1 means pose succ := fun n : nat => n + 1, *) (* and, in context of the the 4CT library, pose mid := maps id means *) (* pose mid := fun d : detaSet => @maps d d (@id (datum d)) *) (* Note that this facility does not extend to set, which tries *) (* instead to fill holes by matching a goal subterm. *) (* The argument to "have" et al. uses product abstraction, e.g. *) (* have Hmid: forall s, (maps id s) = s. *) (* stands for *) (* have Hmid: forall (d : dataSet) (s : seq d), (maps id s) = s. *) (* We also use this feature for rewrite rules, so that, e.g., *) (* rewrite: (plus_assoc _ 3). *) (* will execute as *) (* rewrite (fun n => plus_assoc n 3) *) (* i.e., it will rewrite some subterm .. + (3 + ..) to .. + 3 + ... *) (* The convention is also used for the argument of the congr tactic, *) (* e.g., congr (x + _ * 1). *) (* Replace new evars with lambda variables, retaining local dependencies *) (* but stripping global ones. We use the variable names to encode the *) (* the number of dependencies, so that the transformation is reversible. *) let pf_abs_evars gl (sigma, c0) = let sigma0 = project gl in let nenv = env_size (pf_env gl) in let abs_evar n k = let evi = Evd.find sigma k in let dc = list_firstn n (evar_filtered_context evi) in let abs_dc c = function | x, Some b, t -> mkNamedLetIn x b t (mkArrow t c) | x, None, t -> mkNamedProd x t c in let t = Sign.fold_named_context_reverse abs_dc ~init:evi.evar_concl dc in Evarutil.nf_evar sigma t in let rec put evlist c = match kind_of_term c with | Evar (k, a) -> if List.mem_assoc k evlist || Evd.mem sigma0 k then evlist else let n = max 0 (Array.length a - nenv) in let t = abs_evar n k in (k, (n, t)) :: put evlist t | _ -> fold_constr put evlist c in let evlist = put [] c0 in if evlist = [] then 0, c0,[] else let rec lookup k i = function | [] -> 0, 0 | (k', (n, _)) :: evl -> if k = k' then i, n else lookup k (i + 1) evl in let rec get i c = match kind_of_term c with | Evar (ev, a) -> let j, n = lookup ev i evlist in if j = 0 then map_constr (get i) c else if n = 0 then mkRel j else mkApp (mkRel j, Array.init n (fun k -> get i a.(n - 1 - k))) | _ -> map_constr_with_binders ((+) 1) get i c in let rec loop c i = function | (_, (n, t)) :: evl -> loop (mkLambda (mk_evar_name n, get (i - 1) t, c)) (i - 1) evl | [] -> c in List.length evlist, loop (get 1 c0) 1 evlist, List.map fst evlist (* As before but if (?i : T(?j)) and (?j : P : Prop), then the lambda for i * looks like (fun evar_i : (forall pi : P. T(pi))) thanks to "loopP" and all * occurrences of evar_i are replaced by (evar_i evar_j) thanks to "app". * * If P can be solved by ssrautoprop (that defaults to trivial), then * the corresponding lambda looks like (fun evar_i : T(c)) where c is * the solution found by ssrautoprop. *) let ssrautoprop_tac = ref (fun gl -> assert false) (* Thanks to Arnaud Spiwack for this snippet *) let call_on_evar tac e s = let { it = gs ; sigma = s } = tac { it = Goal.build e ; sigma = s } in gs, s let pf_abs_evars_pirrel gl (sigma, c0) = pp(lazy(str"==PF_ABS_EVARS_PIRREL==")); pp(lazy(str"c0= " ++ pr_constr c0)); let sigma0 = project gl in let nenv = env_size (pf_env gl) in let abs_evar n k = let evi = Evd.find sigma k in let dc = list_firstn n (evar_filtered_context evi) in let abs_dc c = function | x, Some b, t -> mkNamedLetIn x b t (mkArrow t c) | x, None, t -> mkNamedProd x t c in let t = Sign.fold_named_context_reverse abs_dc ~init:evi.evar_concl dc in Evarutil.nf_evar sigma t in let rec put evlist c = match kind_of_term c with | Evar (k, a) -> if List.mem_assoc k evlist || Evd.mem sigma0 k then evlist else let n = max 0 (Array.length a - nenv) in let k_ty = Retyping.get_sort_family_of (pf_env gl) sigma (Evd.evar_concl (Evd.find sigma k)) in let is_prop = k_ty = InProp in let t = abs_evar n k in (k, (n, t, is_prop)) :: put evlist t | _ -> fold_constr put evlist c in let evlist = put [] c0 in if evlist = [] then 0, c0 else let pr_constr t = pr_constr (Reductionops.nf_beta (project gl) t) in let evplist = let depev = List.fold_left (fun evs (_,(_,t,_)) -> Intset.union evs (Evarutil.evars_of_term t)) Intset.empty evlist in List.filter (fun (i,(_,_,b)) -> b && Intset.mem i depev) evlist in let evlist, evplist, sigma = if evplist = [] then evlist, [], sigma else List.fold_left (fun (ev, evp, sigma) (i, (_,t,_) as p) -> try let ng, sigma = call_on_evar !ssrautoprop_tac i sigma in if (ng <> []) then errorstrm (str "Should we tell the user?"); List.filter (fun (j,_) -> j <> i) ev, evp, sigma with _ -> ev, p::evp, sigma) (evlist, [], sigma) (List.rev evplist) in let c0 = Evarutil.nf_evar sigma c0 in let evlist = List.map (fun (x,(y,t,z)) -> x,(y,Evarutil.nf_evar sigma t,z)) evlist in let evplist = List.map (fun (x,(y,t,z)) -> x,(y,Evarutil.nf_evar sigma t,z)) evplist in pp(lazy(str"c0= " ++ pr_constr c0)); let rec lookup k i = function | [] -> 0, 0 | (k', (n,_,_)) :: evl -> if k = k' then i,n else lookup k (i + 1) evl in let rec get evlist i c = match kind_of_term c with | Evar (ev, a) -> let j, n = lookup ev i evlist in if j = 0 then map_constr (get evlist i) c else if n = 0 then mkRel j else mkApp (mkRel j, Array.init n (fun k -> get evlist i a.(n - 1 - k))) | _ -> map_constr_with_binders ((+) 1) (get evlist) i c in let rec app extra_args i c = match decompose_app c with | hd, args when isRel hd && destRel hd = i -> let j = destRel hd in mkApp (mkRel j, Array.of_list (List.map (lift (i-1)) extra_args @ args)) | _ -> map_constr_with_binders ((+) 1) (app extra_args) i c in let rec loopP evlist c i = function | (_, (n, t, _)) :: evl -> let t = get evlist (i - 1) t in let n = Name (id_of_string (ssr_anon_hyp ^ string_of_int n)) in loopP evlist (mkProd (n, t, c)) (i - 1) evl | [] -> c in let rec loop c i = function | (_, (n, t, _)) :: evl -> let evs = Evarutil.evars_of_term t in let t_evplist = List.filter (fun (k,_) -> Intset.mem k evs) evplist in let t = loopP t_evplist (get t_evplist 1 t) 1 t_evplist in let t = get evlist (i - 1) t in let extra_args = List.map (fun (k,_) -> mkRel (fst (lookup k i evlist))) (List.rev t_evplist) in let c = if extra_args = [] then c else app extra_args 1 c in loop (mkLambda (mk_evar_name n, t, c)) (i - 1) evl | [] -> c in let res = loop (get evlist 1 c0) 1 evlist in pp(lazy(str"res= " ++ pr_constr res)); List.length evlist, res (* Strip all non-essential dependencies from an abstracted term, generating *) (* standard names for the abstracted holes. *) let pf_abs_cterm gl n c0 = if n <= 0 then c0 else let noargs = [|0|] in let eva = Array.make n noargs in let rec strip i c = match kind_of_term c with | App (f, a) when isRel f -> let j = i - destRel f in if j >= n || eva.(j) = noargs then mkApp (f, Array.map (strip i) a) else let dp = eva.(j) in let nd = Array.length dp - 1 in let mkarg k = strip i a.(if k < nd then dp.(k + 1) - j else k + dp.(0)) in mkApp (f, Array.init (Array.length a - dp.(0)) mkarg) | _ -> map_constr_with_binders ((+) 1) strip i c in let rec strip_ndeps j i c = match kind_of_term c with | Prod (x, t, c1) when i < j -> let dl, c2 = strip_ndeps j (i + 1) c1 in if noccurn 1 c2 then dl, lift (-1) c2 else i :: dl, mkProd (x, strip i t, c2) | LetIn (x, b, t, c1) when i < j -> let _, _, c1' = destProd c1 in let dl, c2 = strip_ndeps j (i + 1) c1' in if noccurn 1 c2 then dl, lift (-1) c2 else i :: dl, mkLetIn (x, strip i b, strip i t, c2) | _ -> [], strip i c in let rec strip_evars i c = match kind_of_term c with | Lambda (x, t1, c1) when i < n -> let na = nb_evar_deps x in let dl, t2 = strip_ndeps (i + na) i t1 in let na' = List.length dl in eva.(i) <- Array.of_list (na - na' :: dl); let x' = if na' = 0 then Name (pf_type_id gl t2) else mk_evar_name na' in mkLambda (x', t2, strip_evars (i + 1) c1) (* if noccurn 1 c2 then lift (-1) c2 else mkLambda (Name (pf_type_id gl t2), t2, c2) *) | _ -> strip i c in strip_evars 0 c0 (* Undo the evar abstractions. Also works for non-evar variables. *) let pf_unabs_evars gl ise n c0 = if n = 0 then c0 else let evv = Array.make n mkProp in let nev = ref 0 in let env0 = pf_env gl in let nenv0 = env_size env0 in let rec unabs i c = match kind_of_term c with | Rel j when i - j < !nev -> evv.(i - j) | App (f, a0) when isRel f -> let a = Array.map (unabs i) a0 in let j = i - destRel f in if j >= !nev then mkApp (f, a) else let ev, eva = destEvar evv.(j) in let nd = Array.length eva - nenv0 in if nd = 0 then mkApp (evv.(j), a) else let evarg k = if k < nd then a.(nd - 1 - k) else eva.(k) in let c' = mkEvar (ev, Array.init (nd + nenv0) evarg) in let na = Array.length a - nd in if na = 0 then c' else mkApp (c', Array.sub a nd na) | _ -> map_constr_with_binders ((+) 1) unabs i c in let push_rel = Environ.push_rel in let rec mk_evar j env i c = match kind_of_term c with | Prod (x, t, c1) when i < j -> mk_evar j (push_rel (x, None, unabs i t) env) (i + 1) c1 | LetIn (x, b, t, c1) when i < j -> let _, _, c2 = destProd c1 in mk_evar j (push_rel (x, Some (unabs i b), unabs i t) env) (i + 1) c2 | _ -> Evarutil.e_new_evar ise env (unabs i c) in let rec unabs_evars c = if !nev = n then unabs n c else match kind_of_term c with | Lambda (x, t, c1) when !nev < n -> let i = !nev in evv.(i) <- mk_evar (i + nb_evar_deps x) env0 i t; incr nev; unabs_evars c1 | _ -> unabs !nev c in unabs_evars c0 (* }}} *) (** Tactical extensions. {{{ **************************************************) (* The TACTIC EXTEND facility can't be used for defining new user *) (* tacticals, because: *) (* - the concrete syntax must start with a fixed string *) (* - the lexical Ltac environment is NOT used to interpret tactic *) (* arguments *) (* The second limitation means that the extended tacticals will *) (* exhibit run-time scope errors if used inside Ltac functions or *) (* pattern-matching constructs. *) (* We use the following workaround: *) (* - We use the (unparsable) "Qed" token for tacticals that *) (* don't start with a token, then redefine the grammar and *) (* printer using GEXTEND and set_pr_ssrtac, respectively. *) (* - We use a global stack and side effects to pass the lexical *) (* Ltac evaluation context to the extended tactical. The context *) (* is grabbed by interpreting an (empty) ltacctx argument, *) (* which should appear last in the grammar rules; the *) (* get_ltacctx function pops the stack and returns the context. *) (* For additional safety, the push returns an integer key that *) (* is checked by the pop; since arguments are interpreted *) (* left-to-right, this checks that only one tactic argument *) (* pushes a context. *) (* - To avoid a spurrious option type, we don't push the context *) (* for a null tag. *) type ssrargfmt = ArgSsr of string | ArgCoq of argument_type | ArgSep of string let set_pr_ssrtac name prec afmt = let fmt = List.map (function ArgSep s -> Some s | _ -> None) afmt in let rec mk_akey = function | ArgSsr s :: afmt' -> ExtraArgType ("ssr" ^ s) :: mk_akey afmt' | ArgCoq a :: afmt' -> a :: mk_akey afmt' | ArgSep _ :: afmt' -> mk_akey afmt' | [] -> [] in let tacname = "ssr" ^ name in Pptactic.declare_extra_tactic_pprule (tacname, mk_akey afmt, (prec, fmt)) let ssrtac_atom loc name args = TacExtend (loc, "ssr" ^ name, args) let ssrtac_expr loc name args = TacAtom (loc, ssrtac_atom loc name args) let ssrevaltac ist gtac = interp_tac_gen ist.lfun [] ist.debug (globTacticIn (fun _ -> gtac)) (* fun gl -> let lfun = [tacarg_id, val_interp ist gl gtac] in interp_tac_gen lfun [] ist.debug tacarg_expr gl *) (** Generic argument-based globbing/typing utilities *) let interp_wit globwit wit ist gl x = let globarg = in_gen globwit x in let sigma, arg = interp_genarg ist gl globarg in sigma, out_gen wit arg let interp_intro_pattern = interp_wit globwit_intro_pattern wit_intro_pattern let interp_constr = interp_wit globwit_constr wit_constr let interp_open_constr ist gl gc = interp_wit globwit_open_constr wit_open_constr ist gl ((), gc) let interp_refine ist gl rc = let roc = (), (rc, None) in interp_wit globwit_casted_open_constr wit_casted_open_constr ist gl roc let pf_match = pf_apply (fun e s c t -> understand_tcc s e ~expected_type:t c) (* Estimate a bound on the number of arguments of a raw constr. *) (* This is not perfect, because the unifier may fail to *) (* typecheck the partial application, so we use a minimum of 5. *) (* Also, we don't handle delayed or iterated coercions to *) (* FUNCLASS, which is probably just as well since these can *) (* lead to infinite arities. *) let splay_open_constr gl (sigma, c) = let env = pf_env gl in let t = Retyping.get_type_of env sigma c in Reductionops.splay_prod env sigma t let nbargs_open_constr gl oc = let pl, _ = splay_open_constr gl oc in List.length pl let interp_nbargs ist gl rc = try let rc6 = mkRApp rc (mkRHoles 6) in let sigma, t = interp_open_constr ist gl (rc6, None) in let si = sig_it gl in let gl = re_sig si sigma in 6 + nbargs_open_constr gl t with _ -> 5 let pf_nbargs gl c = nbargs_open_constr gl (project gl, c) let isAppInd gl c = try ignore (pf_reduce_to_atomic_ind gl c); true with _ -> false let interp_view_nbimps ist gl rc = try let sigma, t = interp_open_constr ist gl (rc, None) in let si = sig_it gl in let gl = re_sig si sigma in let pl, c = splay_open_constr gl t in if isAppInd gl c then List.length pl else ~-(List.length pl) with _ -> 0 (* }}} *) (** Vernacular commands: Prenex Implicits and Search {{{ **********************) (* This should really be implemented as an extension to the implicit *) (* arguments feature, but unfortuately that API is sealed. The current *) (* workaround uses a combination of notations that works reasonably, *) (* with the following caveats: *) (* - The pretty-printing always elides prenex implicits, even when *) (* they are obviously needed. *) (* - Prenex Implicits are NEVER exported from a module, because this *) (* would lead to faulty pretty-printing and scoping errors. *) (* - The command "Import Prenex Implicits" can be used to reassert *) (* Prenex Implicits for all the visible constants that had been *) (* declared as Prenex Implicits. *) let declare_one_prenex_implicit locality f = let fref = try Smartlocate.global_with_alias f with _ -> errorstrm (pr_reference f ++ str " is not declared") in let rec loop = function | a :: args' when Impargs.is_status_implicit a -> (ExplByName (Impargs.name_of_implicit a), (true, true, true)) :: loop args' | args' when List.exists Impargs.is_status_implicit args' -> errorstrm (str "Expected prenex implicits for " ++ pr_reference f) | _ -> [] in let impls = match Impargs.implicits_of_global fref with | [cond,impls] -> impls | [] -> errorstrm (str "Expected some implicits for " ++ pr_reference f) | _ -> errorstrm (str "Multiple implicits not supported") in match loop impls with | [] -> errorstrm (str "Expected some implicits for " ++ pr_reference f) | impls -> Impargs.declare_manual_implicits locality fref ~enriching:false [impls] VERNAC COMMAND EXTEND Ssrpreneximplicits | [ "Prenex" "Implicits" ne_global_list(fl) ] -> [ let locality = Vernacexpr.use_section_locality () in List.iter (declare_one_prenex_implicit locality) fl ] END (* Vernac grammar visibility patch *) GEXTEND Gram GLOBAL: gallina_ext; gallina_ext: [ [ IDENT "Import"; IDENT "Prenex"; IDENT "Implicits" -> Vernacexpr.VernacUnsetOption (None, ["Printing"; "Implicit"; "Defensive"]) ] ] ; END (* Remove the silly restriction that forces coercion classes to be precise *) (* aliases, e.g., allowing notations that specify some class parameters. *) let qualify_ref clref = let loc, qid = qualid_of_reference clref in try match Nametab.locate_extended qid with | TrueGlobal _ -> clref | SynDef kn -> let rec head_of = function | ARef gref -> Qualid (loc, Nametab.shortest_qualid_of_global Idset.empty gref) | AApp (rc, _) -> head_of rc | ACast (rc, _) -> head_of rc | ALetIn (_, _, rc) -> head_of rc | rc -> user_err_loc (loc, "qualify_ref", str "The definition of " ++ Ppconstr.pr_qualid qid ++ str " does not have a head constant") in head_of (snd (Syntax_def.search_syntactic_definition kn)) with _ -> clref let class_rawexpr = G_vernac.class_rawexpr in GEXTEND Gram GLOBAL: class_rawexpr; ssrqref: [[ gref = global -> qualify_ref gref ]]; class_rawexpr: [[ class_ref = ssrqref -> Vernacexpr.RefClass (Genarg.AN class_ref) ]]; END (** Extend Search to subsume SearchAbout, also adding hidden Type coercions. *) (* Main prefilter *) let pr_search_item = function | Search.GlobSearchString s -> str s | Search.GlobSearchSubPattern p -> pr_constr_pattern p let wit_ssr_searchitem, globwit_ssr_searchitem, rawwit_ssr_searchitem = add_genarg "ssr_searchitem" pr_search_item let interp_search_notation loc s opt_scope = try let interp = Notation.interp_notation_as_global_reference loc in let ref = interp (fun _ -> true) s opt_scope in Search.GlobSearchSubPattern (Pattern.PRef ref) with _ -> let diagnosis = try let ntns = Notation.locate_notation pr_glob_constr s opt_scope in let ambig = "This string refers to a complex or ambiguous notation." in str ambig ++ str "\nTry searching with one of\n" ++ ntns with _ -> str "This string is not part of an identifier or notation." in user_err_loc (loc, "interp_search_notation", diagnosis) let pr_ssr_search_item _ _ _ = pr_search_item (* Workaround the notation API that can only print notations *) let is_ident s = try Lexer.check_ident s; true with _ -> false let is_ident_part s = is_ident ("H" ^ s) let interp_search_notation loc tag okey = let err msg = user_err_loc (loc, "interp_search_notation", msg) in let mk_pntn s for_key = let n = String.length s in let s' = String.make (n + 2) ' ' in let rec loop i i' = if i >= n then s', i' - 2 else if s.[i] = ' ' then loop (i + 1) i' else let j = try String.index_from s (i + 1) ' ' with _ -> n in let m = j - i in if s.[i] = '\'' && i < j - 2 && s.[j - 1] = '\'' then (String.blit s (i + 1) s' i' (m - 2); loop (j + 1) (i' + m - 1)) else if for_key && is_ident (String.sub s i m) then (s'.[i'] <- '_'; loop (j + 1) (i' + 2)) else (String.blit s i s' i' m; loop (j + 1) (i' + m + 1)) in loop 0 1 in let trim_ntn (pntn, m) = String.sub pntn 1 (max 0 m) in let pr_ntn ntn = str "(" ++ str ntn ++ str ")" in let pr_and_list pr = function | [x] -> pr x | x :: lx -> pr_list pr_comma pr lx ++ pr_comma () ++ str "and " ++ pr x | [] -> mt () in let pr_sc sc = str (if sc = "" then "independently" else sc) in let pr_scs = function | [""] -> pr_sc "" | scs -> str "in " ++ pr_and_list pr_sc scs in let generator, pr_tag_sc = let ign _ = mt () in match okey with | Some key -> let sc = Notation.find_delimiters_scope loc key in let pr_sc s_in = str s_in ++ spc() ++ str sc ++ pr_comma() in Notation.pr_scope ign sc, pr_sc | None -> Notation.pr_scopes ign, ign in let qtag s_in = pr_tag_sc s_in ++ qstring tag ++ spc()in let ptag, ttag = let ptag, m = mk_pntn tag false in if m <= 0 then err (str "empty notation fragment"); ptag, trim_ntn (ptag, m) in let last = ref "" and last_sc = ref "" in let scs = ref [] and ntns = ref [] in let push_sc sc = match !scs with | "" :: scs' -> scs := "" :: sc :: scs' | scs' -> scs := sc :: scs' in let get s _ _ = match !last with | "Scope " -> last_sc := s; last := "" | "Lonely notation" -> last_sc := ""; last := "" | "\"" -> let pntn, m = mk_pntn s true in if string_string_contains pntn ptag then begin let ntn = trim_ntn (pntn, m) in match !ntns with | [] -> ntns := [ntn]; scs := [!last_sc] | ntn' :: _ when ntn' = ntn -> push_sc !last_sc | _ when ntn = ttag -> ntns := ntn :: !ntns; scs := [!last_sc] | _ :: ntns' when List.mem ntn ntns' -> () | ntn' :: ntns' -> ntns := ntn' :: ntn :: ntns' end; last := "" | _ -> last := s in pp_with (Format.make_formatter get (fun _ -> ())) generator; let ntn = match !ntns with | [] -> err (hov 0 (qtag "in" ++ str "does not occur in any notation")) | ntn :: ntns' when ntn = ttag -> if ntns' <> [] then begin let pr_ntns' = pr_and_list pr_ntn ntns' in msg_warning (hov 4 (qtag "In" ++ str "also occurs in " ++ pr_ntns')) end; ntn | [ntn] -> msgnl (hov 4 (qtag "In" ++ str "is part of notation " ++ pr_ntn ntn)); ntn | ntns' -> let e = str "occurs in" ++ spc() ++ pr_and_list pr_ntn ntns' in err (hov 4 (str "ambiguous: " ++ qtag "in" ++ e)) in let (nvars, body), ((_, pat), osc) = match !scs with | [sc] -> Notation.interp_notation loc ntn (None, [sc]) | scs' -> try Notation.interp_notation loc ntn (None, []) with _ -> let e = pr_ntn ntn ++ spc() ++ str "is defined " ++ pr_scs scs' in err (hov 4 (str "ambiguous: " ++ pr_tag_sc "in" ++ e)) in let sc = Option.default "" osc in let _ = let m_sc = if osc <> None then str "In " ++ str sc ++ pr_comma() else mt() in let ntn_pat = trim_ntn (mk_pntn pat false) in let rbody = glob_constr_of_aconstr loc body in let m_body = hov 0 (Constrextern.without_symbols prl_glob_constr rbody) in let m = m_sc ++ pr_ntn ntn_pat ++ spc () ++ str "denotes " ++ m_body in msgnl (hov 0 m) in if List.length !scs > 1 then let scs' = list_remove sc !scs in let w = pr_ntn ntn ++ str " is also defined " ++ pr_scs scs' in msg_warning (hov 4 w) else if string_string_contains ntn " .. " then err (pr_ntn ntn ++ str " is an n-ary notation"); let nvars = List.filter (fun (_,(_,typ)) -> typ = NtnTypeConstr) nvars in let rec sub () = function | AVar x when List.mem_assoc x nvars -> GPatVar (loc, (false, x)) | c -> glob_constr_of_aconstr_with_binders loc (fun _ x -> (), x) sub () c in let _, npat = Pattern.pattern_of_glob_constr (sub () body) in Search.GlobSearchSubPattern npat ARGUMENT EXTEND ssr_search_item TYPED AS ssr_searchitem PRINTED BY pr_ssr_search_item | [ string(s) ] -> [ if is_ident_part s then Search.GlobSearchString s else interp_search_notation loc s None ] | [ string(s) "%" preident(key) ] -> [ interp_search_notation loc s (Some key) ] | [ constr_pattern(p) ] -> [ try let intern = Constrintern.intern_constr_pattern Evd.empty in Search.GlobSearchSubPattern (snd (intern (Global.env()) p)) with e -> raise (Cerrors.process_vernac_interp_error e) ] END let pr_ssr_search_arg _ _ _ = let pr_item (b, p) = str (if b then "-" else "") ++ pr_search_item p in pr_list spc pr_item ARGUMENT EXTEND ssr_search_arg TYPED AS (bool * ssr_searchitem) list PRINTED BY pr_ssr_search_arg | [ "-" ssr_search_item(p) ssr_search_arg(a) ] -> [ (false, p) :: a ] | [ ssr_search_item(p) ssr_search_arg(a) ] -> [ (true, p) :: a ] | [ ] -> [ [] ] END (* Main type conclusion pattern filter *) let rec splay_search_pattern na = function | Pattern.PApp (fp, args) -> splay_search_pattern (na + Array.length args) fp | Pattern.PLetIn (_, _, bp) -> splay_search_pattern na bp | Pattern.PRef hr -> hr, na | _ -> error "no head constant in head search pattern" let coerce_search_pattern_to_sort hpat = let env = Global.env () and sigma = Evd.empty in let mkPApp fp n_imps args = let args' = Array.append (Array.make n_imps (Pattern.PMeta None)) args in Pattern.PApp (fp, args') in let hr, na = splay_search_pattern 0 hpat in let dc, ht = Reductionops.splay_prod env sigma (Global.type_of_global hr) in let np = List.length dc in if np < na then error "too many arguments in head search pattern" else let hpat' = if np = na then hpat else mkPApp hpat (np - na) [||] in let warn () = msg_warning (str "Listing only lemmas with conclusion matching " ++ pr_constr_pattern hpat') in if isSort ht then begin warn (); true, hpat' end else let filter_head, coe_path = try let _, cp = Classops.lookup_path_to_sort_from (push_rels_assum dc env) sigma ht in warn (); true, cp with _ -> false, [] in let coerce hp coe_index = let coe = Classops.get_coercion_value coe_index in try let coe_ref = reference_of_constr coe in let n_imps = Option.get (Classops.hide_coercion coe_ref) in mkPApp (Pattern.PRef coe_ref) n_imps [|hp|] with _ -> errorstrm (str "need explicit coercion " ++ pr_constr coe ++ spc () ++ str "to interpret head search pattern as type") in filter_head, List.fold_left coerce hpat' coe_path let rec interp_head_pat hpat = let filter_head, p = coerce_search_pattern_to_sort hpat in let rec loop c = match kind_of_term c with | Cast (c', _, _) -> loop c' | Prod (_, _, c') -> loop c' | LetIn (_, _, _, c') -> loop c' | _ -> Matching.is_matching p c in filter_head, loop let all_true _ = true let interp_search_arg a = let hpat, a1 = match a with | (_, Search.GlobSearchSubPattern (Pattern.PMeta _)) :: a' -> all_true, a' | (true, Search.GlobSearchSubPattern p) :: a' -> let filter_head, p = interp_head_pat p in if filter_head then p, a' else all_true, a | _ -> all_true, a in let is_string = function (_, Search.GlobSearchString _) -> true | _ -> false in let a2, a3 = List.partition is_string a1 in hpat, a2 @ a3 (* Module path postfilter *) let pr_modloc (b, m) = if b then str "-" ++ pr_reference m else pr_reference m let wit_ssrmodloc, globwit_ssrmodloc, rawwit_ssrmodloc = add_genarg "ssrmodloc" pr_modloc let pr_ssr_modlocs _ _ _ ml = if ml = [] then str "" else spc () ++ str "in " ++ pr_list spc pr_modloc ml ARGUMENT EXTEND ssr_modlocs TYPED AS ssrmodloc list PRINTED BY pr_ssr_modlocs | [ ] -> [ [] ] END GEXTEND Gram GLOBAL: ssr_modlocs; modloc: [[ "-"; m = global -> true, m | m = global -> false, m]]; ssr_modlocs: [[ "in"; ml = LIST1 modloc -> ml ]]; END let interp_modloc mr = let interp_mod (_, mr) = let (loc, qid) = qualid_of_reference mr in try Nametab.full_name_module qid with Not_found -> user_err_loc (loc, "interp_modloc", str "No Module " ++ pr_qualid qid) in let mr_out, mr_in = List.partition fst mr in let interp_bmod b rmods = if rmods = [] then fun _ _ _ -> true else Search.filter_by_module_from_list (List.map interp_mod rmods, b) in let is_in = interp_bmod false mr_in and is_out = interp_bmod true mr_out in fun gr env -> is_in gr env () && is_out gr env () (* The unified, extended vernacular "Search" command *) let ssrdisplaysearch gr env t = let pr_res = pr_global gr ++ spc () ++ str " " ++ pr_lconstr_env env t in msg (hov 2 pr_res ++ fnl ()) VERNAC COMMAND EXTEND SsrSearchPattern | [ "Search" ssr_search_arg(a) ssr_modlocs(mr) ] -> [ let hpat, a' = interp_search_arg a in let in_mod = interp_modloc mr in let post_filter gr env typ = in_mod gr env && hpat typ in Search.raw_search_about post_filter ssrdisplaysearch a' ] END (* }}} *) (** Alternative notations for "match" and anonymous arguments. {{{ ************) (* Syntax: *) (* if is then ... else ... *) (* if is [in ..] return ... then ... else ... *) (* let: := in ... *) (* let: [in ...] := return ... in ... *) (* The scope of a top-level 'as' in the pattern extends over the *) (* 'return' type (dependent if/let). *) (* Note that the optional "in ..." appears next to the *) (* rather than the in then "let:" syntax. The alternative *) (* would lead to ambiguities in, e.g., *) (* let: p1 := (*v---INNER LET:---v *) *) (* let: p2 := let: p3 := e3 in k return t in k2 in k1 return t' *) (* in b (*^--ALTERNATIVE INNER LET--------^ *) *) (* Caveat : There is no pretty-printing support, since this would *) (* require a modification to the Coq kernel (adding a new match *) (* display style -- why aren't these strings?); also, the v8.1 *) (* pretty-printer only allows extension hooks for printing *) (* integer or string literals. *) (* Also note that in the v8 grammar "is" needs to be a keyword; *) (* as this can't be done from an ML extension file, the new *) (* syntax will only work when ssreflect.v is imported. *) let no_ct = None, None and no_rt = None in let aliasvar = function | [_, [CPatAlias (loc, _, id)]] -> Some (loc,Name id) | _ -> None in let mk_cnotype mp = aliasvar mp, None in let mk_ctype mp t = aliasvar mp, Some t in let mk_rtype t = Some t in let mk_dthen loc (mp, ct, rt) c = (loc, mp, c), ct, rt in let mk_let loc rt ct mp c1 = CCases (loc, LetPatternStyle, rt, ct, [loc, mp, c1]) in GEXTEND Gram GLOBAL: binder_constr; ssr_rtype: [[ "return"; t = operconstr LEVEL "100" -> mk_rtype t ]]; ssr_mpat: [[ p = pattern -> [loc, [p]] ]]; ssr_dpat: [ [ mp = ssr_mpat; "in"; t = lconstr; rt = ssr_rtype -> mp, mk_ctype mp t, rt | mp = ssr_mpat; rt = ssr_rtype -> mp, mk_cnotype mp, rt | mp = ssr_mpat -> mp, no_ct, no_rt ] ]; ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> mk_dthen loc dp c ]]; ssr_elsepat: [[ "else" -> [loc, [CPatAtom (loc, None)]] ]]; ssr_else: [[ mp = ssr_elsepat; c = lconstr -> loc, mp, c ]]; binder_constr: [ [ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else -> let b1, ct, rt = db1 in CCases (loc, MatchStyle, rt, [c, ct], [b1; b2]) | "if"; c = operconstr LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else -> let b1, ct, rt = db1 in let b1, b2 = let (l1, p1, r1), (l2, p2, r2) = b1, b2 in (l1, p1, r2), (l2, p2, r1) in CCases (loc, MatchStyle, rt, [c, ct], [b1; b2]) | "let"; ":"; mp = ssr_mpat; ":="; c = lconstr; "in"; c1 = lconstr -> mk_let loc no_rt [c, no_ct] mp c1 | "let"; ":"; mp = ssr_mpat; ":="; c = lconstr; rt = ssr_rtype; "in"; c1 = lconstr -> mk_let loc rt [c, mk_cnotype mp] mp c1 | "let"; ":"; mp = ssr_mpat; "in"; t = lconstr; ":="; c = lconstr; rt = ssr_rtype; "in"; c1 = lconstr -> mk_let loc rt [c, mk_ctype mp t] mp c1 ] ]; END GEXTEND Gram GLOBAL: closed_binder; closed_binder: [ [ ["of" | "&"]; c = operconstr LEVEL "99" -> [LocalRawAssum ([loc, Anonymous], Default Explicit, c)] ] ]; END (* }}} *) (** Tacticals (+, -, *, done, by, do, =>, first, and last). {{{ ***************) (** Bracketing tactical *) (* The tactic pretty-printer doesn't know that some extended tactics *) (* are actually tacticals. To prevent it from improperly removing *) (* parentheses we override the parsing rule for bracketed tactic *) (* expressions so that the pretty-print always reflects the input. *) (* (Removing user-specified parentheses is dubious anyway). *) GEXTEND Gram GLOBAL: tactic_expr; ssrparentacarg: [[ "("; tac = tactic_expr; ")" -> loc, Tacexp tac ]]; tactic_expr: LEVEL "0" [[ arg = ssrparentacarg -> TacArg arg ]]; END (** The internal "done" and "ssrautoprop" tactics. *) (* For additional flexibility, "done" and "ssrautoprop" are *) (* defined in Ltac. *) (* Although we provide a default definition in ssreflect, *) (* we look up the definition dynamically at each call point, *) (* to allow for user extensions. "ssrautoprop" defaults to *) (* trivial. *) let donetac gl = let tacname = try Nametab.locate_tactic (qualid_of_ident (id_of_string "done")) with Not_found -> try Nametab.locate_tactic (ssrqid "done") with Not_found -> Util.error "The ssreflect library was not loaded" in let tacexpr = dummy_loc, Tacexpr.Reference (ArgArg (dummy_loc, tacname)) in eval_tactic (Tacexpr.TacArg tacexpr) gl let prof_donetac = mk_profiler "donetac";; let donetac gl = prof_donetac.profile donetac gl;; let ssrautoprop gl = try let tacname = try Nametab.locate_tactic (qualid_of_ident (id_of_string "ssrautoprop")) with Not_found -> Nametab.locate_tactic (ssrqid "ssrautoprop") in let tacexpr = dummy_loc, Tacexpr.Reference (ArgArg (dummy_loc, tacname)) in eval_tactic (Tacexpr.TacArg tacexpr) gl with Not_found -> Auto.full_trivial [] gl let () = ssrautoprop_tac := ssrautoprop let tclBY tac = tclTHEN tac donetac (** Tactical arguments. *) (* We have four kinds: simple tactics, [|]-bracketed lists, hints, and swaps *) (* The latter two are used in forward-chaining tactics (have, suffice, wlog) *) (* and subgoal reordering tacticals (; first & ; last), respectively. *) (* Force use of the tactic_expr parsing entry, to rule out tick marks. *) let pr_ssrtacarg _ _ prt = prt tacltop ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY pr_ssrtacarg | [ "Qed" ] -> [ Util.anomaly "Grammar placeholder match" ] END GEXTEND Gram GLOBAL: ssrtacarg; ssrtacarg: [[ tac = tactic_expr LEVEL "5" -> tac ]]; END (* Lexically closed tactic for tacticals. *) let pr_ssrtclarg _ _ prt (tac, _) = prt tacltop tac ARGUMENT EXTEND ssrtclarg TYPED AS ssrtacarg * ltacctx PRINTED BY pr_ssrtclarg | [ ssrtacarg(tac) ] -> [ tac, rawltacctx ] END let eval_tclarg (tac, ctx) = ssrevaltac (get_ltacctx ctx) tac let pr_ortacs prt = let rec pr_rec = function | [None] -> spc() ++ str "|" ++ spc() | None :: tacs -> spc() ++ str "|" ++ pr_rec tacs | Some tac :: tacs -> spc() ++ str "| " ++ prt tacltop tac ++ pr_rec tacs | [] -> mt() in function | [None] -> spc() | None :: tacs -> pr_rec tacs | Some tac :: tacs -> prt tacltop tac ++ pr_rec tacs | [] -> mt() let pr_ssrortacs _ _ = pr_ortacs ARGUMENT EXTEND ssrortacs TYPED AS tactic option list PRINTED BY pr_ssrortacs | [ ssrtacarg(tac) "|" ssrortacs(tacs) ] -> [ Some tac :: tacs ] | [ ssrtacarg(tac) "|" ] -> [ [Some tac; None] ] | [ ssrtacarg(tac) ] -> [ [Some tac] ] | [ "|" ssrortacs(tacs) ] -> [ None :: tacs ] | [ "|" ] -> [ [None; None] ] END let pr_hintarg prt = function | true, tacs -> hv 0 (str "[ " ++ pr_ortacs prt tacs ++ str " ]") | false, [Some tac] -> prt tacltop tac | _, _ -> mt() let pr_ssrhintarg _ _ = pr_hintarg let mk_hint tac = false, [Some tac] let mk_orhint tacs = true, tacs let nullhint = true, [] let nohint = false, [] ARGUMENT EXTEND ssrhintarg TYPED AS bool * ssrortacs PRINTED BY pr_ssrhintarg | [ "[" "]" ] -> [ nullhint ] | [ "[" ssrortacs(tacs) "]" ] -> [ mk_orhint tacs ] | [ ssrtacarg(arg) ] -> [ mk_hint arg ] END ARGUMENT EXTEND ssrortacarg TYPED AS ssrhintarg PRINTED BY pr_ssrhintarg | [ "[" ssrortacs(tacs) "]" ] -> [ mk_orhint tacs ] END let hinttac ist is_by (is_or, atacs) = let dtac = if is_by then donetac else tclIDTAC in let mktac = function | Some atac -> tclTHEN (ssrevaltac ist atac) dtac | _ -> dtac in match List.map mktac atacs with | [] -> if is_or then dtac else tclIDTAC | [tac] -> tac | tacs -> tclFIRST tacs (** The "-"/"+"/"*" tacticals. *) (* These are just visual cues to flag the beginning of the script for *) (* new subgoals, when indentation is not appropriate (typically after *) (* tactics that generate more than two subgoals). *) TACTIC EXTEND ssrtclplus | [ "Qed" "+" ssrtclarg(arg) ] -> [ eval_tclarg arg ] END set_pr_ssrtac "tclplus" 5 [ArgSep "+ "; ArgSsr "tclarg"] TACTIC EXTEND ssrtclminus | [ "Qed" "-" ssrtclarg(arg) ] -> [ eval_tclarg arg ] END set_pr_ssrtac "tclminus" 5 [ArgSep "- "; ArgSsr "tclarg"] TACTIC EXTEND ssrtclstar | [ "Qed" "*" ssrtclarg(arg) ] -> [ eval_tclarg arg ] END set_pr_ssrtac "tclstar" 5 [ArgSep "- "; ArgSsr "tclarg"] let gen_tclarg = in_gen rawwit_ssrtclarg GEXTEND Gram GLOBAL: tactic tactic_mode; tactic: [ [ "+"; tac = ssrtclarg -> ssrtac_expr loc "tclplus" [gen_tclarg tac] | "-"; tac = ssrtclarg -> ssrtac_expr loc "tclminus" [gen_tclarg tac] | "*"; tac = ssrtclarg -> ssrtac_expr loc "tclstar" [gen_tclarg tac] ] ]; tactic_mode: [ [ "+"; tac = G_vernac.subgoal_command -> tac None | "-"; tac = G_vernac.subgoal_command -> tac None | "*"; tac = G_vernac.subgoal_command -> tac None ] ]; END (** The "by" tactical. *) let pr_hint prt arg = if arg = nohint then mt() else str "by " ++ pr_hintarg prt arg let pr_ssrhint _ _ = pr_hint ARGUMENT EXTEND ssrhint TYPED AS ssrhintarg PRINTED BY pr_ssrhint | [ ] -> [ nohint ] END TACTIC EXTEND ssrtclby | [ "Qed" ssrhint(tac) ltacctx(ctx)] -> [ hinttac (get_ltacctx ctx) true tac ] END set_pr_ssrtac "tclby" 0 [ArgSsr "hint"; ArgSsr "ltacctx"] (* We can't parse "by" in ARGUMENT EXTEND because it will only be made *) (* into a keyword in ssreflect.v; so we anticipate this in GEXTEND. *) GEXTEND Gram GLOBAL: ssrhint simple_tactic; ssrhint: [[ "by"; arg = ssrhintarg -> arg ]]; simple_tactic: [ [ "by"; arg = ssrhintarg -> let garg = in_gen rawwit_ssrhint arg in let gctx = in_gen rawwit_ltacctx rawltacctx in ssrtac_atom loc "tclby" [garg; gctx] ] ]; END (* }}} *) (** Bound assumption argument *) (* The Ltac API does have a type for assumptions but it is level-dependent *) (* and therefore impratical to use for complex arguments, so we substitute *) (* our own to have a uniform representation. Also, we refuse to intern *) (* idents that match global/section constants, since this would lead to *) (* fragile Ltac scripts. *) type ssrhyp = SsrHyp of loc * identifier let hyp_id (SsrHyp (_, id)) = id let pr_hyp (SsrHyp (_, id)) = pr_id id let pr_ssrhyp _ _ _ = pr_hyp let wit_ssrhyprep, globwit_ssrhyprep, rawwit_ssrhyprep = add_genarg "ssrhyprep" pr_hyp let hyp_err loc msg id = user_err_loc (loc, "ssrhyp", str msg ++ pr_id id) let intern_hyp ist (SsrHyp (loc, id) as hyp) = let _ = intern_genarg ist (in_gen rawwit_var (loc, id)) in if not_section_id id then hyp else hyp_err loc "Can't clear section hypothesis " id let interp_hyp ist gl (SsrHyp (loc, id)) = let s, id' = interp_wit globwit_var wit_var ist gl (loc, id) in if not_section_id id' then s, SsrHyp (loc, id') else hyp_err loc "Can't clear section hypothesis " id' ARGUMENT EXTEND ssrhyp TYPED AS ssrhyprep PRINTED BY pr_ssrhyp INTERPRETED BY interp_hyp GLOBALIZED BY intern_hyp | [ ident(id) ] -> [ SsrHyp (loc, id) ] END type ssrhyp_or_id = Hyp of ssrhyp | Id of ssrhyp let hoik f = function Hyp x -> f x | Id x -> f x let hoi_id = hoik hyp_id let pr_hoi = hoik pr_hyp let pr_ssrhoi _ _ _ = pr_hoi let wit_ssrhoirep, globwit_ssrhoirep, rawwit_ssrhoirep = add_genarg "ssrhoirep" pr_hoi let intern_ssrhoi ist = function | Hyp h -> Hyp (intern_hyp ist h) | Id (SsrHyp (_, id)) as hyp -> let _ = intern_genarg ist (in_gen rawwit_ident id) in hyp let interp_ssrhoi ist gl = function | Hyp h -> let s, h' = interp_hyp ist gl h in s, Hyp h' | Id (SsrHyp (loc, id)) -> let s, id' = interp_wit globwit_ident wit_ident ist gl id in s, Id (SsrHyp (loc, id')) ARGUMENT EXTEND ssrhoi_hyp TYPED AS ssrhoirep PRINTED BY pr_ssrhoi INTERPRETED BY interp_ssrhoi GLOBALIZED BY intern_ssrhoi | [ ident(id) ] -> [ Hyp (SsrHyp(loc, id)) ] END ARGUMENT EXTEND ssrhoi_id TYPED AS ssrhoirep PRINTED BY pr_ssrhoi INTERPRETED BY interp_ssrhoi GLOBALIZED BY intern_ssrhoi | [ ident(id) ] -> [ Id (SsrHyp(loc, id)) ] END type ssrhyps = ssrhyp list let pr_hyps = pr_list pr_spc pr_hyp let pr_ssrhyps _ _ _ = pr_hyps let hyps_ids = List.map hyp_id let rec check_hyps_uniq ids = function | SsrHyp (loc, id) :: _ when List.mem id ids -> hyp_err loc "Duplicate assumption " id | SsrHyp (_, id) :: hyps -> check_hyps_uniq (id :: ids) hyps | [] -> () let check_hyp_exists hyps (SsrHyp(_, id)) = try ignore(Sign.lookup_named id hyps) with Not_found -> errorstrm (str"No assumption is named " ++ pr_id id) let interp_hyps ist gl ghyps = let hyps = List.map snd (List.map (interp_hyp ist gl) ghyps) in check_hyps_uniq [] hyps; Tacmach.project gl, hyps ARGUMENT EXTEND ssrhyps TYPED AS ssrhyp list PRINTED BY pr_ssrhyps INTERPRETED BY interp_hyps | [ ssrhyp_list(hyps) ] -> [ check_hyps_uniq [] hyps; hyps ] END (** Terms parsing. {{{ ********************************************************) (* Because we allow wildcards in term references, we need to stage the *) (* interpretation of terms so that it occurs at the right time during *) (* the execution of the tactic (e.g., so that we don't report an error *) (* for a term that isn't actually used in the execution). *) (* The term representation tracks whether the concrete initial term *) (* started with an opening paren, which might avoid a conflict between *) (* the ssrreflect term syntax and Gallina notation. *) (* kinds of terms *) type ssrtermkind = char (* print flag *) let input_ssrtermkind strm = match Compat.get_tok (stream_nth 0 strm) with | Tok.KEYWORD "(" -> '(' | Tok.KEYWORD "@" -> '@' | _ -> ' ' let ssrtermkind = Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind (* terms *) let pr_ssrterm _ _ _ = pr_term let pf_intern_term ist gl (_, c) = glob_constr ist (project gl) (pf_env gl) c let intern_term ist sigma env (_, c) = glob_constr ist sigma env c let interp_term ist gl (_, c) = snd (interp_open_constr ist gl c) let force_term ist gl (_, c) = interp_constr ist gl c let glob_ssrterm gs = function | k, (_, Some c) -> k, Tacinterp.intern_constr gs c | ct -> ct let subst_ssrterm s (k, c) = k, Tacinterp.subst_glob_constr_and_expr s c let interp_ssrterm _ gl t = Tacmach.project gl, t ARGUMENT EXTEND ssrterm PRINTED BY pr_ssrterm INTERPRETED BY interp_ssrterm GLOBALIZED BY glob_ssrterm SUBSTITUTED BY subst_ssrterm RAW_TYPED AS cpattern RAW_PRINTED BY pr_ssrterm GLOB_TYPED AS cpattern GLOB_PRINTED BY pr_ssrterm | [ "Qed" constr(c) ] -> [ mk_lterm c ] END GEXTEND Gram GLOBAL: ssrterm; ssrterm: [[ k = ssrtermkind; c = constr -> mk_term k c ]]; END (* }}} *) (** The "in" pseudo-tactical {{{ **********************************************) (* We can't make "in" into a general tactical because this would create a *) (* crippling conflict with the ltac let .. in construct. Hence, we add *) (* explicitly an "in" suffix to all the extended tactics for which it is *) (* relevant (including move, case, elim) and to the extended do tactical *) (* below, which yields a general-purpose "in" of the form do [...] in ... *) (* This tactical needs to come before the intro tactics because the latter *) (* must take precautions in order not to interfere with the discharged *) (* assumptions. This is especially difficult for discharged "let"s, which *) (* the default simpl and unfold tactics would erase blindly. *) (** Clear switch *) type ssrclear = ssrhyps let pr_clear_ne clr = str "{" ++ pr_hyps clr ++ str "}" let pr_clear sep clr = if clr = [] then mt () else sep () ++ pr_clear_ne clr let pr_ssrclear _ _ _ = pr_clear mt ARGUMENT EXTEND ssrclear_ne TYPED AS ssrhyps PRINTED BY pr_ssrclear | [ "{" ne_ssrhyp_list(clr) "}" ] -> [ check_hyps_uniq [] clr; clr ] END ARGUMENT EXTEND ssrclear TYPED AS ssrclear_ne PRINTED BY pr_ssrclear | [ ssrclear_ne(clr) ] -> [ clr ] | [ ] -> [ [] ] END let cleartac clr = check_hyps_uniq [] clr; clear (hyps_ids clr) (* type ssrwgen = ssrclear * ssrhyp * string *) let pr_wgen = function | (clr, Some((id,k),None)) -> spc() ++ pr_clear mt clr ++ str k ++ pr_hoi id | (clr, Some((id,k),Some p)) -> spc() ++ pr_clear mt clr ++ str"(" ++ str k ++ pr_hoi id ++ str ":=" ++ pr_cpattern p ++ str ")" | (clr, None) -> spc () ++ pr_clear mt clr let pr_ssrwgen _ _ _ = pr_wgen (* no globwith for char *) ARGUMENT EXTEND ssrwgen TYPED AS ssrclear * ((ssrhoi_hyp * string) * cpattern option) option PRINTED BY pr_ssrwgen | [ ssrclear_ne(clr) ] -> [ clr, None ] | [ ssrhoi_hyp(hyp) ] -> [ [], Some((hyp, " "), None) ] | [ "@" ssrhoi_hyp(hyp) ] -> [ [], Some((hyp, "@"), None) ] | [ "(" ssrhoi_id(id) ":=" lcpattern(p) ")" ] -> [ [], Some ((id," "),Some p) ] | [ "(" ssrhoi_id(id) ")" ] -> [ [], Some ((id,"("), None) ] | [ "(@" ssrhoi_id(id) ":=" lcpattern(p) ")" ] -> [ [], Some ((id,"@"),Some p) ] | [ "(" "@" ssrhoi_id(id) ":=" lcpattern(p) ")" ] -> [ [], Some ((id,"@"),Some p) ] END type ssrclseq = InGoal | InHyps | InHypsGoal | InHypsSeqGoal | InSeqGoal | InHypsSeq | InAll | InAllHyps let pr_clseq = function | InGoal | InHyps -> mt () | InSeqGoal -> str "|- *" | InHypsSeqGoal -> str " |- *" | InHypsGoal -> str " *" | InAll -> str "*" | InHypsSeq -> str " |-" | InAllHyps -> str "* |-" let wit_ssrclseq, globwit_ssrclseq, rawwit_ssrclseq = add_genarg "ssrclseq" pr_clseq let pr_clausehyps = pr_list pr_spc pr_wgen let pr_ssrclausehyps _ _ _ = pr_clausehyps ARGUMENT EXTEND ssrclausehyps TYPED AS ssrwgen list PRINTED BY pr_ssrclausehyps | [ ssrwgen(hyp) "," ssrclausehyps(hyps) ] -> [ hyp :: hyps ] | [ ssrwgen(hyp) ssrclausehyps(hyps) ] -> [ hyp :: hyps ] | [ ssrwgen(hyp) ] -> [ [hyp] ] END (* type ssrclauses = ssrahyps * ssrclseq *) let pr_clauses (hyps, clseq) = if clseq = InGoal then mt () else str "in " ++ pr_clausehyps hyps ++ pr_clseq clseq let pr_ssrclauses _ _ _ = pr_clauses ARGUMENT EXTEND ssrclauses TYPED AS ssrwgen list * ssrclseq PRINTED BY pr_ssrclauses | [ "in" ssrclausehyps(hyps) "|-" "*" ] -> [ hyps, InHypsSeqGoal ] | [ "in" ssrclausehyps(hyps) "|-" ] -> [ hyps, InHypsSeq ] | [ "in" ssrclausehyps(hyps) "*" ] -> [ hyps, InHypsGoal ] | [ "in" ssrclausehyps(hyps) ] -> [ hyps, InHyps ] | [ "in" "|-" "*" ] -> [ [], InSeqGoal ] | [ "in" "*" ] -> [ [], InAll ] | [ "in" "*" "|-" ] -> [ [], InAllHyps ] | [ ] -> [ [], InGoal ] END let nohide = mkRel 0 let hidden_goal_tag = "the_hidden_goal" (* Reduction that preserves the Prod/Let spine of the "in" tactical. *) let inc_safe n = if n = 0 then n else n + 1 let rec safe_depth c = match kind_of_term c with | LetIn (Name x, _, _, c') when is_discharged_id x -> safe_depth c' + 1 | LetIn (_, _, _, c') | Prod (_, _, c') -> inc_safe (safe_depth c') | _ -> 0 let red_safe r e s c0 = let rec red_to e c n = match kind_of_term c with | Prod (x, t, c') when n > 0 -> let t' = r e s t in let e' = Environ.push_rel (x, None, t') e in mkProd (x, t', red_to e' c' (n - 1)) | LetIn (x, b, t, c') when n > 0 -> let t' = r e s t in let e' = Environ.push_rel (x, None, t') e in mkLetIn (x, r e s b, t', red_to e' c' (n - 1)) | _ -> r e s c in red_to e c0 (safe_depth c0) let check_wgen_uniq gens = let clears = List.flatten (List.map fst gens) in check_hyps_uniq [] clears; let ids = Util.list_map_filter (function (_,Some ((id,_),_)) -> Some (hoi_id id) | _ -> None) gens in let rec check ids = function | id :: _ when List.mem id ids -> errorstrm (str"Duplicate generalization " ++ pr_id id) | id :: hyps -> check (id :: ids) hyps | [] -> () in check [] ids let pf_clauseids gl gens clseq = let keep_clears = List.map (fun (x, _) -> x, None) in if gens <> [] then (check_wgen_uniq gens; gens) else if clseq <> InAll && clseq <> InAllHyps then keep_clears gens else Util.error "assumptions should be named explicitly" let hidden_clseq = function InHyps | InHypsSeq | InAllHyps -> true | _ -> false let hidetacs clseq idhide cl0 = if not (hidden_clseq clseq) then [] else [posetac idhide cl0; convert_concl_no_check (mkVar idhide)] let discharge_hyp (id', (id, mode)) gl = let cl' = subst_var id (pf_concl gl) in match pf_get_hyp gl id, mode with | (_, None, t), _ | (_, Some _, t), "(" -> apply_type (mkProd (Name id', t, cl')) [mkVar id] gl | (_, Some v, t), _ -> convert_concl (mkLetIn (Name id', v, t, cl')) gl let endclausestac id_map clseq gl_id cl0 gl = let not_hyp' id = not (List.mem_assoc id id_map) in let orig_id id = try List.assoc id id_map with _ -> id in let dc, c = Term.decompose_prod_assum (pf_concl gl) in let hide_goal = hidden_clseq clseq in let c_hidden = hide_goal && c = mkVar gl_id in let rec fits forced = function | (id, _) :: ids, (Name id', _, _) :: dc' when id' = id -> fits true (ids, dc') | ids, dc' -> forced && ids = [] && (not hide_goal || dc' = [] && c_hidden) in let rec unmark c = match kind_of_term c with | Var id when hidden_clseq clseq && id = gl_id -> cl0 | Prod (Name id, t, c') when List.mem_assoc id id_map -> mkProd (Name (orig_id id), unmark t, unmark c') | LetIn (Name id, v, t, c') when List.mem_assoc id id_map -> mkLetIn (Name (orig_id id), unmark v, unmark t, unmark c') | _ -> map_constr unmark c in let utac hyp = convert_hyp_no_check (map_named_declaration unmark hyp) in let utacs = List.map utac (pf_hyps gl) in let ugtac gl' = convert_concl_no_check (unmark (pf_concl gl')) gl' in let ctacs = if hide_goal then [clear [gl_id]] else [] in let mktac itacs = tclTHENLIST (itacs @ utacs @ ugtac :: ctacs) in let itac (_, id) = introduction id in if fits false (id_map, List.rev dc) then mktac (List.map itac id_map) gl else let all_ids = ids_of_rel_context dc @ pf_ids_of_hyps gl in if List.for_all not_hyp' all_ids && not c_hidden then mktac [] gl else Util.error "tampering with discharged assumptions of \"in\" tactical" let is_id_constr c = match kind_of_term c with | Lambda(_,_,c) when isRel c -> 1 = destRel c | _ -> false let red_product_skip_id env sigma c = match kind_of_term c with | App(hd,args) when Array.length args = 1 && is_id_constr hd -> args.(0) | _ -> try Tacred.red_product env sigma c with _ -> c let abs_wgen keep_let ist gl f gen (args,c) = let sigma, env = project gl, pf_env gl in let evar_closed t p = if occur_existential t then Util.user_err_loc (loc_of_cpattern p,"ssreflect", pr_constr_pat t ++ str" contains holes and matches no subterm of the goal") in match gen with | _, Some ((x, mode), None) when mode = "@" || (mode = " " && keep_let) -> let x = hoi_id x in let _, bo, ty = pf_get_hyp gl x in (if bo <> None then args else mkVar x :: args), mkProd_or_LetIn (Name (f x),bo,ty) (subst_var x c) | _, Some ((x, _), None) -> let x = hoi_id x in mkVar x :: args, mkProd (Name (f x), pf_get_hyp_typ gl x, subst_var x c) | _, Some ((x, "@"), Some p) -> let x = hoi_id x in let cp = interp_cpattern ist gl p None in let t, c = try fill_occ_pattern ~raise_NoMatch:true env sigma c cp None 1 with NoMatch -> redex_of_pattern env cp, c in evar_closed t p; let ut = red_product_skip_id env sigma t in args, mkLetIn(Name (f x), ut, pf_type_of gl t, c) | _, Some ((x, _), Some p) -> let x = hoi_id x in let cp = interp_cpattern ist gl p None in let t, c = try fill_occ_pattern ~raise_NoMatch:true env sigma c cp None 1 with NoMatch -> redex_of_pattern env cp, c in evar_closed t p; t :: args, mkProd(Name (f x), pf_type_of gl t, c) | _ -> args, c let clr_of_wgen gen clrs = match gen with | clr, Some ((x, _), None) -> let x = hoi_id x in cleartac clr :: cleartac [SsrHyp(Util.dummy_loc,x)] :: clrs | clr, _ -> cleartac clr :: clrs let tclCLAUSES ist tac (gens, clseq) gl = if clseq = InGoal || clseq = InSeqGoal then tac gl else let clr_gens = pf_clauseids gl gens clseq in let clear = tclTHENLIST (List.rev(List.fold_right clr_of_wgen clr_gens [])) in let gl_id = mk_anon_id hidden_goal_tag gl in let cl0 = pf_concl gl in let dtac gl = let c = pf_concl gl in let args, c = List.fold_right (abs_wgen true ist gl mk_discharged_id) gens ([], c) in apply_type c args gl in let endtac = let id_map = Util.list_map_filter (function | _, Some ((x,_),_) -> let id = hoi_id x in Some (mk_discharged_id id, id) | _, None -> None) gens in endclausestac id_map clseq gl_id cl0 in tclTHENLIST (hidetacs clseq gl_id cl0 @ [dtac; clear; tac; endtac]) gl (* }}} *) (** Simpl switch *) type ssrsimpl = Simpl | Cut | SimplCut | Nop let pr_simpl = function | Simpl -> str "/=" | Cut -> str "//" | SimplCut -> str "//=" | Nop -> mt () let pr_ssrsimpl _ _ _ = pr_simpl let wit_ssrsimplrep, globwit_ssrsimplrep, rawwit_ssrsimplrep = add_genarg "ssrsimplrep" pr_simpl ARGUMENT EXTEND ssrsimpl_ne TYPED AS ssrsimplrep PRINTED BY pr_ssrsimpl | [ "/=" ] -> [ Simpl ] | [ "//" ] -> [ Cut ] | [ "//=" ] -> [ SimplCut ] END ARGUMENT EXTEND ssrsimpl TYPED AS ssrsimplrep PRINTED BY pr_ssrsimpl | [ ssrsimpl_ne(sim) ] -> [ sim ] | [ ] -> [ Nop ] END (* We must avoid zeta-converting any "let"s created by the "in" tactical. *) let safe_simpltac gl = let cl' = red_safe Tacred.simpl (pf_env gl) (project gl) (pf_concl gl) in convert_concl_no_check cl' gl let simpltac = function | Simpl -> safe_simpltac | Cut -> tclTRY donetac | SimplCut -> tclTHEN safe_simpltac (tclTRY donetac) | Nop -> tclIDTAC (** Rewriting direction *) let pr_dir = function L2R -> str "->" | R2L -> str "<-" let pr_rwdir = function L2R -> mt() | R2L -> str "-" let rewritetac dir c = (* Due to the new optional arg ?tac, application shouldn't be too partial *) Equality.general_rewrite (dir = L2R) all_occurrences true false c let wit_ssrdir, globwit_ssrdir, rawwit_ssrdir = add_genarg "ssrdir" pr_dir let dir_org = function L2R -> 1 | R2L -> 2 (** Indexes *) (* Since SSR indexes are always positive numbers, we use the 0 value *) (* to encode an omitted index. We reuse the in or_var type, but we *) (* supply our own interpretation function, which checks for non *) (* positive values, and allows the use of constr numerals, so that *) (* e.g., "let n := eval compute in (1 + 3) in (do n!clear)" works. *) type ssrindex = int or_var let pr_index = function | ArgVar (_, id) -> pr_id id | ArgArg n when n > 0 -> pr_int n | _ -> mt () let pr_ssrindex _ _ _ = pr_index let noindex = ArgArg 0 let allocc = Some(false,[]) let check_index loc i = if i > 0 then i else loc_error loc "Index not positive" let mk_index loc = function ArgArg i -> ArgArg (check_index loc i) | iv -> iv let interp_index ist gl idx = Tacmach.project gl, match idx with | ArgArg _ -> idx | ArgVar (loc, id) -> let i = try match List.assoc id ist.lfun with | VInteger i -> i | VConstr ([],c) -> let rc = Detyping.detype false [] [] c in begin match Notation.uninterp_prim_token rc with | _, Numeral bigi -> int_of_string (Bigint.to_string bigi) | _ -> raise Not_found end | _ -> raise Not_found with _ -> loc_error loc "Index not a number" in ArgArg (check_index loc i) ARGUMENT EXTEND ssrindex TYPED AS int_or_var PRINTED BY pr_ssrindex INTERPRETED BY interp_index | [ int_or_var(i) ] -> [ mk_index loc i ] END (** Occurrence switch *) (* The standard syntax of complemented occurrence lists involves a single *) (* initial "-", e.g., {-1 3 5}. An initial *) (* "+" may be used to indicate positive occurrences (the default). The *) (* "+" is optional, except if the list of occurrences starts with a *) (* variable or is empty (to avoid confusion with a clear switch). The *) (* empty positive switch "{+}" selects no occurrences, while the empty *) (* negative switch "{-}" selects all occurrences explicitly; this is the *) (* default, but "{-}" prevents the implicit clear, and can be used to *) (* force dependent elimination -- see ndefectelimtac below. *) type ssrocc = occ let pr_occ = function | Some (true, occ) -> str "{-" ++ pr_list pr_spc int occ ++ str "}" | Some (false, occ) -> str "{+" ++ pr_list pr_spc int occ ++ str "}" | None -> str "{}" let pr_ssrocc _ _ _ = pr_occ ARGUMENT EXTEND ssrocc TYPED AS (bool * int list) option PRINTED BY pr_ssrocc | [ natural(n) natural_list(occ) ] -> [ Some (false, List.map (check_index loc) (n::occ)) ] | [ "-" natural_list(occ) ] -> [ Some (true, occ) ] | [ "+" natural_list(occ) ] -> [ Some (false, occ) ] END let pf_mkprod gl c ?(name=constr_name c) cl = let t = pf_type_of gl c in if name <> Anonymous || noccurn 1 cl then mkProd (name, t, cl) else mkProd (Name (pf_type_id gl t), t, cl) let pf_abs_prod name gl c cl = pf_mkprod gl c ~name (subst_term c cl) (** Discharge occ switch (combined occurrence / clear switch *) type ssrdocc = ssrclear option * ssrocc option let mkocc occ = None, occ let noclr = mkocc None let mkclr clr = Some clr, None let nodocc = mkclr [] let pr_docc = function | None, occ -> pr_occ occ | Some clr, _ -> pr_clear mt clr let pr_ssrdocc _ _ _ = pr_docc ARGUMENT EXTEND ssrdocc TYPED AS ssrclear option * ssrocc PRINTED BY pr_ssrdocc | [ "{" ne_ssrhyp_list(clr) "}" ] -> [ mkclr clr ] | [ "{" ssrocc(occ) "}" ] -> [ mkocc occ ] END (** View hint database and View application. {{{ ******************************) (* There are three databases of lemmas used to mediate the application *) (* of reflection lemmas: one for forward chaining, one for backward *) (* chaining, and one for secondary backward chaining. *) (* View hints *) let rec isCxHoles = function (CHole _, None) :: ch -> isCxHoles ch | _ -> false let pr_raw_ssrhintref prc _ _ = function | CAppExpl (_, (None, r), args) when isCHoles args -> prc (CRef r) ++ str "|" ++ int (List.length args) | CApp (_, (_, CRef _), _) as c -> prc c | CApp (_, (_, c), args) when isCxHoles args -> prc c ++ str "|" ++ int (List.length args) | c -> prc c let pr_rawhintref = function | GApp (_, f, args) when isRHoles args -> pr_glob_constr f ++ str "|" ++ int (List.length args) | c -> pr_glob_constr c let pr_glob_ssrhintref _ _ _ (c, _) = pr_rawhintref c let pr_ssrhintref prc _ _ = prc let mkhintref loc c n = match c with | CRef r -> CAppExpl (loc, (None, r), mkCHoles loc n) | _ -> mkAppC (c, mkCHoles loc n) ARGUMENT EXTEND ssrhintref PRINTED BY pr_ssrhintref RAW_TYPED AS constr RAW_PRINTED BY pr_raw_ssrhintref GLOB_TYPED AS constr GLOB_PRINTED BY pr_glob_ssrhintref | [ constr(c) ] -> [ c ] | [ constr(c) "|" natural(n) ] -> [ mkhintref loc c n ] END (* View purpose *) let pr_viewpos = function | 0 -> str " for move/" | 1 -> str " for apply/" | 2 -> str " for apply//" | _ -> mt () let pr_ssrviewpos _ _ _ = pr_viewpos ARGUMENT EXTEND ssrviewpos TYPED AS int PRINTED BY pr_ssrviewpos | [ "for" "move" "/" ] -> [ 0 ] | [ "for" "apply" "/" ] -> [ 1 ] | [ "for" "apply" "/" "/" ] -> [ 2 ] | [ "for" "apply" "//" ] -> [ 2 ] | [ ] -> [ 3 ] END let pr_ssrviewposspc _ _ _ i = pr_viewpos i ++ spc () ARGUMENT EXTEND ssrviewposspc TYPED AS ssrviewpos PRINTED BY pr_ssrviewposspc | [ ssrviewpos(i) ] -> [ i ] END (* The table and its display command *) let viewtab : glob_constr list array = Array.make 3 [] let _ = let init () = Array.fill viewtab 0 3 [] in let freeze () = Array.copy viewtab in let unfreeze vt = Array.blit vt 0 viewtab 0 3 in Summary.declare_summary "ssrview" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; Summary.init_function = init } let mapviewpos f n k = if n < 3 then f n else for i = 0 to k - 1 do f i done let print_view_hints i = let pp_viewname = str "Hint View" ++ pr_viewpos i ++ str " " in let pp_hints = pr_list spc pr_rawhintref viewtab.(i) in ppnl (pp_viewname ++ hov 0 pp_hints ++ Pp.cut ()) VERNAC COMMAND EXTEND PrintView | [ "Print" "Hint" "View" ssrviewpos(i) ] -> [ mapviewpos print_view_hints i 3 ] END (* Populating the table *) let cache_viewhint (_, (i, lvh)) = let mem_raw h = List.exists (Topconstr.eq_glob_constr h) in let add_hint h hdb = if mem_raw h hdb then hdb else h :: hdb in viewtab.(i) <- List.fold_right add_hint lvh viewtab.(i) let subst_viewhint ( subst, (i, lvh as ilvh)) = let lvh' = list_smartmap (Detyping.subst_glob_constr subst) lvh in if lvh' == lvh then ilvh else i, lvh' let classify_viewhint x = Libobject.Substitute x let in_viewhint = Libobject.declare_object {(Libobject.default_object "VIEW_HINTS") with Libobject.open_function = (fun i o -> if i = 1 then cache_viewhint o); Libobject.cache_function = cache_viewhint; Libobject.subst_function = subst_viewhint; Libobject.classify_function = classify_viewhint } let glob_view_hints lvh = List.map (Constrintern.intern_constr Evd.empty (Global.env ())) lvh let add_view_hints lvh i = Lib.add_anonymous_leaf (in_viewhint (i, lvh)) VERNAC COMMAND EXTEND HintView | [ "Hint" "View" ssrviewposspc(n) ne_ssrhintref_list(lvh) ] -> [ mapviewpos (add_view_hints (glob_view_hints lvh)) n 2 ] END (** Views *) (* Views for the "move" and "case" commands are actually open *) (* terms, but this is handled by interp_view, which is called *) (* by interp_casearg. We use lists, to support the *) (* "double-view" feature of the apply command. *) (* type ssrview = ssrterm list *) let pr_view = pr_list mt (fun c -> str "/" ++ pr_term c) let pr_ssrview _ _ _ = pr_view ARGUMENT EXTEND ssrview TYPED AS ssrterm list PRINTED BY pr_ssrview | [ "/" constr(c) ] -> [ [mk_term ' ' c] ] | [ "/" constr(c) ssrview(w) ] -> [ (mk_term ' ' c) :: w ] END (* 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 view_error s gv = errorstrm (str ("Cannot " ^ s ^ " view ") ++ pr_term gv) let interp_view ist si env sigma gv rid = match intern_term ist sigma env gv with | GApp (loc, GHole _, rargs) -> let rv = GApp (loc, rid, rargs) in snd (interp_open_constr ist (re_sig si sigma) (rv, None)) | rv -> let interp rc rargs = interp_open_constr ist (re_sig si sigma) (mkRApp rc rargs, None) in let rec simple_view rargs n = if n < 0 then view_error "use" gv else try interp rv rargs with _ -> simple_view (mkRHole :: rargs) (n - 1) in let view_nbimps = interp_view_nbimps ist (re_sig si sigma) rv in let view_args = [mkRApp rv (mkRHoles view_nbimps); rid] in let rec view_with = function | [] -> simple_view [rid] (interp_nbargs ist (re_sig si sigma) rv) | hint :: hints -> try interp hint view_args with _ -> view_with hints in snd (view_with (if view_nbimps < 0 then [] else viewtab.(0))) let top_id = mk_internal_id "top assumption" let with_view ist si env gl0 c name cl prune = let c2r ist x = { ist with lfun = (top_id, VConstr ([], x)) :: ist.lfun } in let rec loop (sigma, c') = function | f :: view -> let rid, ist = match kind_of_term c' with | Var id -> mkRVar id, ist | _ -> mkRltacVar top_id, c2r ist c' in loop (interp_view ist si env sigma f rid) view | [] -> let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in let c' = Reductionops.nf_evar sigma c' in let n, c', _ = pf_abs_evars gl0 (sigma, c') in let c' = if not prune then c' else pf_abs_cterm gl0 n c' in pf_abs_prod name gl0 c' (prod_applist cl [c]), c' in loop let pf_with_view ist gl (prune, view) cl c = let env, sigma, si = pf_env gl, project gl, sig_it gl in with_view ist si env gl c (constr_name c) cl prune (sigma, c) view (* }}} *) (** Extended intro patterns {{{ ***********************************************) type ssrtermrep = char * glob_constr_and_expr type ssripat = | IpatSimpl of ssrclear * ssrsimpl | IpatId of identifier | IpatWild | IpatCase of ssripats list | IpatRw of ssrocc * ssrdir | IpatAll | IpatAnon | IpatView of ssrtermrep list | IpatNoop | IpatNewHidden of identifier list and ssripats = ssripat list let remove_loc = snd let rec ipat_of_intro_pattern = function | IntroIdentifier id -> IpatId id | IntroWildcard -> IpatWild | IntroOrAndPattern iorpat -> IpatCase (List.map (List.map ipat_of_intro_pattern) (List.map (List.map remove_loc) iorpat)) | IntroAnonymous -> IpatAnon | IntroRewrite b -> IpatRw (allocc, if b then L2R else R2L) | IntroFresh id -> IpatAnon | IntroForthcoming _ -> (* Unable to determine which kind of ipat interp_introid could return [HH] *) assert false let rec pr_ipat = function | IpatId id -> pr_id id | IpatSimpl (clr, sim) -> pr_clear mt clr ++ pr_simpl sim | IpatCase iorpat -> hov 1 (str "[" ++ pr_iorpat iorpat ++ str "]") | IpatRw (occ, dir) -> pr_occ occ ++ pr_dir dir | IpatAll -> str "*" | IpatWild -> str "_" | IpatAnon -> str "?" | IpatView v -> pr_view v | IpatNoop -> str "-" | IpatNewHidden l -> str "[:" ++ pr_list spc pr_id l ++ str "]" and pr_iorpat iorpat = pr_list pr_bar pr_ipats iorpat and pr_ipats ipats = pr_list spc pr_ipat ipats let wit_ssripatrep, globwit_ssripatrep, rawwit_ssripatrep = add_genarg "ssripatrep" pr_ipat let pr_ssripat _ _ _ = pr_ipat let pr_ssripats _ _ _ = pr_ipats let pr_ssriorpat _ _ _ = pr_iorpat let intern_ipat ist ipat = let rec check_pat = function | IpatSimpl (clr, _) -> ignore (List.map (intern_hyp ist) clr) | IpatCase iorpat -> List.iter (List.iter check_pat) iorpat | _ -> () in check_pat ipat; ipat let intern_ipats ist = List.map (intern_ipat ist) let interp_introid ist gl id = try IntroIdentifier (hyp_id (snd (interp_hyp ist gl (SsrHyp (dummy_loc, id))))) with _ -> snd(snd (interp_intro_pattern ist gl (dummy_loc,IntroIdentifier id))) let rec add_intro_pattern_hyps (loc, ipat) hyps = match ipat with | IntroIdentifier id -> if not_section_id id then SsrHyp (loc, id) :: hyps else hyp_err loc "Can't delete section hypothesis " id | IntroWildcard -> hyps | IntroOrAndPattern iorpat -> List.fold_right (List.fold_right add_intro_pattern_hyps) iorpat hyps | IntroAnonymous -> [] | IntroFresh _ -> [] | IntroRewrite _ -> hyps | IntroForthcoming _ -> (* As in ipat_of_intro_pattern, was unable to determine which kind of ipat interp_introid could return [HH] *) assert false let rec interp_ipat ist gl = let ltacvar id = List.mem_assoc id ist.lfun in let rec interp = function | IpatId id when ltacvar id -> ipat_of_intro_pattern (interp_introid ist gl id) | IpatSimpl (clr, sim) -> let add_hyps (SsrHyp (loc, id) as hyp) hyps = if not (ltacvar id) then hyp :: hyps else add_intro_pattern_hyps (loc, (interp_introid ist gl id)) hyps in let clr' = List.fold_right add_hyps clr [] in check_hyps_uniq [] clr'; IpatSimpl (clr', sim) | IpatCase iorpat -> IpatCase (List.map (List.map interp) iorpat) | IpatNewHidden l -> IpatNewHidden (List.map (function | IntroIdentifier id -> id | _ -> assert false) (List.map (interp_introid ist gl) l)) | ipat -> ipat in interp let interp_ipats ist gl l = project gl, List.map (interp_ipat ist gl) l let pushIpatRw = function | pats :: orpat -> (IpatRw (allocc, L2R) :: pats) :: orpat | [] -> [] let pushIpatNoop = function | pats :: orpat -> (IpatNoop :: pats) :: orpat | [] -> [] ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY pr_ssripats INTERPRETED BY interp_ipats GLOBALIZED BY intern_ipats | [ "_" ] -> [ [IpatWild] ] | [ "*" ] -> [ [IpatAll] ] | [ ident(id) ] -> [ [IpatId id] ] | [ "?" ] -> [ [IpatAnon] ] | [ ssrsimpl_ne(sim) ] -> [ [IpatSimpl ([], sim)] ] | [ ssrdocc(occ) "->" ] -> [ match occ with | None, occ -> [IpatRw (occ, L2R)] | Some clr, _ -> [IpatSimpl (clr, Nop); IpatRw (allocc, L2R)]] | [ ssrdocc(occ) "<-" ] -> [ match occ with | None, occ -> [IpatRw (occ, R2L)] | Some clr, _ -> [IpatSimpl (clr, Nop); IpatRw (allocc, R2L)]] | [ ssrdocc(occ) ] -> [ match occ with | Some cl, _ -> check_hyps_uniq [] cl; [IpatSimpl (cl, Nop)] | _ -> loc_error loc "Only identifiers are allowed here"] | [ "->" ] -> [ [IpatRw (allocc, L2R)] ] | [ "<-" ] -> [ [IpatRw (allocc, R2L)] ] | [ "-" ] -> [ [IpatNoop] ] | [ "-/" "=" ] -> [ [IpatNoop;IpatSimpl([],Simpl)] ] | [ "-/=" ] -> [ [IpatNoop;IpatSimpl([],Simpl)] ] | [ "-/" "/" ] -> [ [IpatNoop;IpatSimpl([],Cut)] ] | [ "-//" ] -> [ [IpatNoop;IpatSimpl([],Cut)] ] | [ "-/" "/=" ] -> [ [IpatNoop;IpatSimpl([],SimplCut)] ] | [ "-//" "=" ] -> [ [IpatNoop;IpatSimpl([],SimplCut)] ] | [ "-//=" ] -> [ [IpatNoop;IpatSimpl([],SimplCut)] ] | [ ssrview(v) ] -> [ [IpatView v] ] | [ "[" ":" ident_list(idl) "]" ] -> [ [IpatNewHidden idl] ] END ARGUMENT EXTEND ssripats TYPED AS ssripat PRINTED BY pr_ssripats | [ ssripat(i) ssripats(tl) ] -> [ i @ tl ] | [ ] -> [ [] ] END ARGUMENT EXTEND ssriorpat TYPED AS ssripat list PRINTED BY pr_ssriorpat | [ ssripats(pats) "|" ssriorpat(orpat) ] -> [ pats :: orpat ] | [ ssripats(pats) "|-" ">" ssriorpat(orpat) ] -> [ pats :: pushIpatRw orpat ] | [ ssripats(pats) "|-" ssriorpat(orpat) ] -> [ pats :: pushIpatNoop orpat ] | [ ssripats(pats) "|->" ssriorpat(orpat) ] -> [ pats :: pushIpatRw orpat ] | [ ssripats(pats) "||" ssriorpat(orpat) ] -> [ pats :: [] :: orpat ] | [ ssripats(pats) "|||" ssriorpat(orpat) ] -> [ pats :: [] :: [] :: orpat ] | [ ssripats(pats) "||||" ssriorpat(orpat) ] -> [ [pats; []; []; []] @ orpat ] | [ ssripats(pats) ] -> [ [pats] ] END let reject_ssrhid strm = match Compat.get_tok (stream_nth 0 strm) with | Tok.KEYWORD "[" -> (match Compat.get_tok (stream_nth 0 strm) with | Tok.KEYWORD ":" -> raise Stream.Failure | _ -> ()) | _ -> () let test_nohidden = Gram.Entry.of_parser "test_ssrhid" reject_ssrhid ARGUMENT EXTEND ssrcpat TYPED AS ssripatrep PRINTED BY pr_ssripat | [ "Qed" ssriorpat(x) ] -> [ IpatCase x ] END GEXTEND Gram GLOBAL: ssrcpat; ssrcpat: [[ test_nohidden; "["; iorpat = ssriorpat; "]" -> IpatCase iorpat ]]; END GEXTEND Gram GLOBAL: ssripat; ssripat: [[ pat = ssrcpat -> [pat] ]]; END ARGUMENT EXTEND ssripats_ne TYPED AS ssripat PRINTED BY pr_ssripats | [ ssripat(i) ssripats(tl) ] -> [ i @ tl ] END (* subsets of patterns *) let check_ssrhpats loc w_binders ipats = let err_loc s = user_err_loc (loc, "ssreflect", s) in let clr, ipats = let rec aux clr = function | IpatSimpl (cl, Nop) :: tl -> aux (clr @ cl) tl | IpatSimpl (cl, sim) :: tl -> clr @ cl, IpatSimpl ([], sim) :: tl | tl -> clr, tl in aux [] ipats in let simpl, ipats = match List.rev ipats with | IpatSimpl ([],_) as s :: tl -> [s], List.rev tl | _ -> [], ipats in if simpl <> [] && not w_binders then err_loc (str "No s-item allowed here: " ++ pr_ipats simpl); let ipat, binders = let rec loop ipat = function | [] -> ipat, [] | ( IpatId _| IpatAnon| IpatCase _| IpatRw _ as i) :: tl -> if w_binders then if simpl <> [] && tl <> [] then err_loc(str"binders XOR s-item allowed here: "++pr_ipats(tl@simpl)) else if not (List.for_all (function IpatId _ -> true | _ -> false) tl) then err_loc (str "Only binders allowed here: " ++ pr_ipats tl) else ipat @ [i], tl else if tl = [] then ipat @ [i], [] else err_loc (str "No binder or s-item allowed here: " ++ pr_ipats tl) | hd :: tl -> loop (ipat @ [hd]) tl in loop [] ipats in ((clr, ipat), binders), simpl let single loc = function [x] -> x | _ -> loc_error loc "Only one intro pattern is allowed" let pr_hpats (((clr, ipat), binders), simpl) = pr_clear mt clr ++ pr_ipats ipat ++ pr_ipats binders ++ pr_ipats simpl let pr_ssrhpats _ _ _ = pr_hpats let pr_ssrhpats_wtransp _ _ _ (_, x) = pr_hpats x ARGUMENT EXTEND ssrhpats TYPED AS ((ssrclear * ssripat) * ssripat) * ssripat PRINTED BY pr_ssrhpats | [ ssripats(i) ] -> [ check_ssrhpats loc true i ] END ARGUMENT EXTEND ssrhpats_wtransp TYPED AS bool * (((ssrclear * ssripat) * ssripat) * ssripat) PRINTED BY pr_ssrhpats_wtransp | [ ssripats(i) ] -> [ false,check_ssrhpats loc true i ] | [ ssripats(i) "@" ssripats(j) ] -> [ true,check_ssrhpats loc true (i @ j) ] END ARGUMENT EXTEND ssrhpats_nobs TYPED AS ((ssrclear * ssripat) * ssripat) * ssripat PRINTED BY pr_ssrhpats | [ ssripats(i) ] -> [ check_ssrhpats loc false i ] END ARGUMENT EXTEND ssrrpat TYPED AS ssripatrep PRINTED BY pr_ssripat | [ "->" ] -> [ IpatRw (allocc, L2R) ] | [ "<-" ] -> [ IpatRw (allocc, R2L) ] END type ssrintros = ssripats * ltacctx let pr_intros sep (intrs, _) = if intrs = [] then mt() else sep () ++ str "=> " ++ pr_ipats intrs let pr_ssrintros _ _ _ = pr_intros mt ARGUMENT EXTEND ssrintros_ne TYPED AS ssripat * ltacctx PRINTED BY pr_ssrintros | [ "=>" ssripats_ne(pats) ] -> [ pats, rawltacctx ] END ARGUMENT EXTEND ssrintros TYPED AS ssrintros_ne PRINTED BY pr_ssrintros | [ ssrintros_ne(intrs) ] -> [ intrs ] | [ ] -> [ [], rawltacctx ] END let injecteq_id = mk_internal_id "injection equation" let pf_nb_prod gl = nb_prod (pf_concl gl) let rev_id = mk_internal_id "rev concl" let revtoptac n0 gl = let n = pf_nb_prod gl - n0 in let dc, cl = decompose_prod_n n (pf_concl gl) in let dc' = dc @ [Name rev_id, compose_prod (List.rev dc) cl] in let f = compose_lam dc' (mkEtaApp (mkRel (n + 1)) (-n) 1) in refine (mkApp (f, [|Evarutil.mk_new_meta ()|])) gl let equality_inj l b id c gl = let msg = ref "" in try Equality.inj l b c gl with Compat.Loc.Exc_located(_,UserError (_,s)) | UserError (_,s) when msg := Pp.string_of_ppcmds s; !msg = "Not a projectable equality but a discriminable one." || !msg = "Nothing to inject." -> msg_warning (str !msg); discharge_hyp (id, (id, "")) gl let injectidl2rtac id c gl = tclTHEN (equality_inj [] true id c) (revtoptac (pf_nb_prod gl)) gl let injectl2rtac c = match kind_of_term c with | Var id -> injectidl2rtac id (mkVar id, NoBindings) | _ -> let id = injecteq_id in tclTHENLIST [havetac id c; injectidl2rtac id (mkVar id, NoBindings); clear [id]] let is_injection_case c gl = let mind, _ = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in mkInd mind = build_coq_eq () let perform_injection c gl = let mind, t = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in let dc, eqt = decompose_prod t in if dc = [] then injectl2rtac c gl else if not (closed0 eqt) then error "can't decompose a quantified equality" else let cl = pf_concl gl in let n = List.length dc in let c_eq = mkEtaApp c n 2 in let cl1 = mkLambda (Anonymous, mkArrow eqt cl, mkApp (mkRel 1, [|c_eq|])) in let id = injecteq_id in let id_with_ebind = (mkVar id, NoBindings) in let injtac = tclTHEN (introid id) (injectidl2rtac id id_with_ebind) in tclTHENLAST (apply (compose_lam dc cl1)) injtac gl let simplest_newcase_ref = ref (fun t gl -> assert false) let simplest_newcase x gl = !simplest_newcase_ref x gl let ssrscasetac c gl = if is_injection_case c gl then perform_injection c gl else simplest_newcase c gl let intro_all gl = let dc, _ = Term.decompose_prod_assum (pf_concl gl) in tclTHENLIST (List.map anontac (List.rev dc)) gl let rec intro_anon gl = try anontac (List.hd (fst (Term.decompose_prod_n_assum 1 (pf_concl gl)))) gl with err0 -> try tclTHEN red_in_concl intro_anon gl with _ -> raise err0 (* with _ -> error "No product even after reduction" *) let with_top tac = tclTHENLIST [introid top_id; tac (mkVar top_id); clear [top_id]] let rec mapLR f = function [] -> [] | x :: s -> let y = f x in y :: mapLR f s let wild_ids = ref [] let new_wild_id () = let i = 1 + List.length !wild_ids in let id = mk_wildcard_id i in wild_ids := id :: !wild_ids; id let clear_wilds wilds gl = clear (List.filter (fun id -> List.mem id wilds) (pf_ids_of_hyps gl)) gl let clear_with_wilds wilds clr0 gl = let extend_clr clr (id, _, _ as nd) = if List.mem id clr || not (List.mem id wilds) then clr else let vars = global_vars_set_of_decl (pf_env gl) nd in let occurs id' = Idset.mem id' vars in if List.exists occurs clr then id :: clr else clr in clear (Sign.fold_named_context_reverse extend_clr ~init:clr0 (pf_hyps gl)) 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 (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 (" " ^ plural n1 name) in errorstrm (pr_nb n_tac n_gls taclname ++ spc () ++ str "for " ++ pr_nb n_gls n_tac "subgoal") (* Forward reference to extended rewrite *) let ipat_rewritetac = ref (fun _ -> rewritetac) let rec is_name_in_ipats name = function | IpatSimpl(clr,_) :: tl -> List.exists (function SsrHyp(_,id) -> id = name) clr || is_name_in_ipats name tl | IpatId id :: tl -> id = name || is_name_in_ipats name tl | IpatCase l :: tl -> is_name_in_ipats name (List.flatten l @ tl) | _ :: tl -> is_name_in_ipats name tl | [] -> false let move_top_with_view = ref (fun _ -> assert false) let rec nat_of_n n = if n = 0 then mkConstruct path_of_O else mkApp (mkConstruct path_of_S, [|nat_of_n (n-1)|]) let ssr_abstract_id = ref 0 let _ = Summary.declare_summary "SSR:abstractid" { Summary.freeze_function = (fun _ -> !ssr_abstract_id); Summary.unfreeze_function = (fun x -> ssr_abstract_id := x); Summary.init_function = (fun () -> ssr_abstract_id := 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, pf_concl gl in let sigma, abstract_proof, abstract_ty = let sigma, ty = Evarutil.new_type_evar Evd.empty env in let sigma,lock = Evarutil.new_evar sigma env (mkSsrConst "abstract_lock") in let abstract_ty = mkApp(mkSsrConst "abstract", [|ty;mk_abstract_id ();lock|]) in let sigma, m = Evarutil.new_evar sigma env abstract_ty in sigma, m, abstract_ty in let sigma, kont = let rd = Name id, None, abstract_ty in Evarutil.new_evar sigma (Environ.push_rel rd env) concl in pp(lazy(pr_constr concl)); let step = mkApp (mkLambda(Name id,abstract_ty,kont) ,[|abstract_proof|]) in Refine.refine (sigma, step) 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. *) (* TODO: hide wild_ids in this block too *) let introstac, tclEQINTROS = let rec map_acc_k f k = function | [] -> (* tricky: we save wilds now, we get to_cler (aka k) later *) let clear_ww = clear_with_wilds !wild_ids in [fun gl -> clear_ww (hyps_ids (List.flatten (List.map (!) k))) gl] | x :: xs -> let k, x = f k xs x in x :: map_acc_k f k xs in let rename force to_clr rest clr gl = let hyps = pf_hyps gl in pp(lazy(str"rename " ++ pr_clear spc clr)); 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 (string_of_id x) gl in SsrHyp (dummy_loc, x'), (x, x')) clr) in let () = to_clr := ren_clr in rename_hyp ren gl else let () = to_clr := clr in tclIDTAC gl in let rec ipattac ?ist k rest = function | IpatWild -> k, introid (new_wild_id ()) | IpatCase iorpat -> k, tclIORPAT ?ist k (with_top ssrscasetac) iorpat | IpatRw (occ, dir) -> k, with_top (!ipat_rewritetac occ dir) | IpatId id -> k, introid id | IpatNewHidden idl -> k, ssrmkabstac idl | IpatSimpl (clr, sim) -> let to_clr = ref [] in to_clr :: k, tclTHEN (rename false to_clr rest clr) (simpltac sim) | IpatAll -> k, intro_all | IpatAnon -> k, intro_anon | IpatNoop -> k, tclIDTAC | IpatView v -> match ist with | None -> anomaly "ipattac with no ist but view" | Some ist -> match rest with | (IpatCase _ | IpatRw _)::_ -> let to_clr = ref [] in let top_id = ref top_id in to_clr :: k, tclTHEN (!move_top_with_view false top_id (false,v) ist) (fun gl -> rename true to_clr rest [SsrHyp (dummy_loc, !top_id)]gl) | _ -> k, !move_top_with_view true (ref top_id) (true,v) ist and tclIORPAT ?ist k tac = function | [[]] -> tac | orp -> tclTHENS_nonstrict tac (mapLR (ipatstac ?ist k) orp) "intro pattern" and ipatstac ?ist k ipats = tclTHENLIST (map_acc_k (ipattac ?ist) k ipats) in let introstac ?ist ipats = wild_ids := []; let tac = ipatstac ?ist [] ipats in tclTHENLIST [tac; clear_wilds !wild_ids] in let tclEQINTROS ?ist tac eqtac ipats = wild_ids := []; let rec split_itacs to_clr tac' = function | (IpatSimpl _ as spat) :: ipats' -> let to_clr, tac = ipattac ?ist to_clr ipats' spat in split_itacs to_clr (tclTHEN tac' tac) ipats' | IpatCase iorpat :: ipats' -> to_clr, tclIORPAT ?ist to_clr tac' iorpat, ipats' | ipats' -> to_clr, tac', ipats' in let to_clr, tac1, ipats' = split_itacs [] tac ipats in let tac2 = ipatstac ?ist to_clr ipats' in tclTHENLIST [tac1; eqtac; tac2; clear_wilds !wild_ids] in introstac, tclEQINTROS ;; let rec eqmoveipats eqpat = function | (IpatSimpl _ as ipat) :: ipats -> ipat :: eqmoveipats eqpat ipats | (IpatAll :: _ | []) as ipats -> IpatAnon :: eqpat :: ipats | ipat :: ipats -> ipat :: eqpat :: ipats (* General case *) let tclINTROS tac (ipats, ctx) = let ist = get_ltacctx ctx in tclEQINTROS ~ist (tac ist) tclIDTAC ipats (** The "=>" tactical *) let ssrintros_sep = let atom_sep = function | TacSplit (_,_, [NoBindings]) -> mt | TacLeft (_, NoBindings) -> mt | TacRight (_, NoBindings) -> mt (* | TacExtend (_, "ssrapply", []) -> mt *) | _ -> spc in function | TacId [] -> mt | TacArg (_, Tacexp _) -> mt | TacArg (_, Reference _) -> mt | TacAtom (_, atom) -> atom_sep atom | _ -> spc let pr_ssrintrosarg _ _ prt (tac, ipats) = prt tacltop tac ++ pr_intros (ssrintros_sep tac) ipats ARGUMENT EXTEND ssrintrosarg TYPED AS tactic * ssrintros PRINTED BY pr_ssrintrosarg | [ "Qed" ssrtacarg(arg) ssrintros_ne(ipats) ] -> [ arg, ipats ] END TACTIC EXTEND ssrtclintros | [ "Qed" ssrintrosarg(arg) ] -> [ let tac, intros = arg in tclINTROS (fun ist -> ssrevaltac ist tac) intros ] END set_pr_ssrtac "tclintros" 0 [ArgSsr "introsarg"] let tclintros_expr loc tac ipats = let args = [in_gen rawwit_ssrintrosarg (tac, ipats)] in ssrtac_expr loc "tclintros" args GEXTEND Gram GLOBAL: tactic_expr; tactic_expr: LEVEL "1" [ RIGHTA [ tac = tactic_expr; intros = ssrintros_ne -> tclintros_expr loc tac intros ] ]; END (* }}} *) (** Multipliers {{{ ***********************************************************) (* modality *) type ssrmmod = May | Must | Once let pr_mmod = function May -> str "?" | Must -> str "!" | Once -> mt () let wit_ssrmmod, globwit_ssrmmod, rawwit_ssrmmod = add_genarg "ssrmmod" pr_mmod let ssrmmod = Gram.Entry.create "ssrmmod" GEXTEND Gram GLOBAL: ssrmmod; ssrmmod: [[ "!" -> Must | LEFTQMARK -> May | "?" -> May]]; END (* tactical *) let tclID tac = tac let tclDOTRY n tac = if n <= 0 then tclIDTAC else let rec loop i gl = if i = n then tclTRY tac gl else tclTRY (tclTHEN tac (loop (i + 1))) gl in loop 1 let tclDO n tac = let prefix i = str"At iteration " ++ int i ++ str": " in let tac_err_at i gl = try tac gl with | UserError (l, s) -> raise (UserError (l, prefix i ++ s)) | Compat.Loc.Exc_located(loc, UserError (l, s)) -> raise (Compat.Loc.Exc_located(loc, UserError (l, prefix i ++ s))) in let rec loop i gl = if i = n then tac_err_at i gl else (tclTHEN (tac_err_at i) (loop (i + 1))) gl in loop 1 let tclMULT = function | 0, May -> tclREPEAT | 1, May -> tclTRY | n, May -> tclDOTRY n | 0, Must -> tclAT_LEAST_ONCE | n, Must when n > 1 -> tclDO n | _ -> tclID (** The "do" tactical. ********************************************************) (* type ssrdoarg = ((ssrindex * ssrmmod) * (ssrhint * ltacctx)) * ssrclauses *) let pr_ssrdoarg prc _ prt (((n, m), (tac, _)), clauses) = pr_index n ++ pr_mmod m ++ pr_hintarg prt tac ++ pr_clauses clauses ARGUMENT EXTEND ssrdoarg TYPED AS ((ssrindex * ssrmmod) * (ssrhintarg * ltacctx)) * ssrclauses PRINTED BY pr_ssrdoarg | [ "Qed" ] -> [ anomaly "Grammar placeholder match" ] END let ssrdotac (((n, m), (tac, ctx)), clauses) = let mul = get_index n, m in let ist = get_ltacctx ctx in tclCLAUSES ist (tclMULT mul (hinttac ist false tac)) clauses TACTIC EXTEND ssrtcldo | [ "Qed" "do" ssrdoarg(arg) ] -> [ ssrdotac arg ] END set_pr_ssrtac "tcldo" 3 [ArgSep "do "; ArgSsr "doarg"] let ssrdotac_expr loc n m tac clauses = let arg = ((n, m), (tac, rawltacctx)), clauses in ssrtac_expr loc "tcldo" [in_gen rawwit_ssrdoarg arg] GEXTEND Gram GLOBAL: tactic_expr; ssrdotac: [ [ tac = tactic_expr LEVEL "3" -> mk_hint tac | tacs = ssrortacarg -> tacs ] ]; tactic_expr: LEVEL "3" [ RIGHTA [ IDENT "do"; m = ssrmmod; tac = ssrdotac; clauses = ssrclauses -> ssrdotac_expr loc noindex m tac clauses | IDENT "do"; tac = ssrortacarg; clauses = ssrclauses -> ssrdotac_expr loc noindex Once tac clauses | IDENT "do"; n = int_or_var; m = ssrmmod; tac = ssrdotac; clauses = ssrclauses -> ssrdotac_expr loc (mk_index loc n) m tac clauses ] ]; END (* }}} *) (** The "first" and "last" tacticals. {{{ *************************************) (* type ssrseqarg = ssrindex * (ssrtacarg * ssrtac option) *) let pr_seqtacarg prt = function | (is_first, []), _ -> str (if is_first then "first" else "last") | tac, Some dtac -> hv 0 (pr_hintarg prt tac ++ spc() ++ str "|| " ++ prt tacltop dtac) | tac, _ -> pr_hintarg prt tac let pr_ssrseqarg _ _ prt = function | ArgArg 0, tac -> pr_seqtacarg prt tac | i, tac -> pr_index i ++ str " " ++ pr_seqtacarg prt tac (* We must parse the index separately to resolve the conflict with *) (* an unindexed tactic. *) ARGUMENT EXTEND ssrseqarg TYPED AS ssrindex * (ssrhintarg * tactic option) PRINTED BY pr_ssrseqarg | [ "Qed" ] -> [ anomaly "Grammar placeholder match" ] END let sq_brace_tacnames = ["first"; "solve"; "do"; "rewrite"; "have"; "suffices"; "wlog"] (* "by" is a keyword *) let accept_ssrseqvar strm = match Compat.get_tok (stream_nth 0 strm) with | Tok.IDENT id when not (List.mem id sq_brace_tacnames) -> accept_before_syms_or_ids ["["] ["first";"last"] strm | _ -> raise Stream.Failure let test_ssrseqvar = Gram.Entry.of_parser "test_ssrseqvar" accept_ssrseqvar let swaptacarg (loc, b) = (b, []), Some (TacAtom (loc, TacRevert [])) let check_seqtacarg dir arg = match snd arg, dir with | ((true, []), Some (TacAtom (loc, _))), L2R -> loc_error loc "expected \"last\"" | ((false, []), Some (TacAtom (loc, _))), R2L -> loc_error loc "expected \"first\"" | _, _ -> arg let ssrorelse = Gram.entry_create "ssrorelse" GEXTEND Gram GLOBAL: ssrorelse ssrseqarg; ssrseqidx: [ [ test_ssrseqvar; id = Prim.ident -> ArgVar (loc, id) | n = Prim.natural -> ArgArg (check_index loc n) ] ]; ssrswap: [[ IDENT "first" -> loc, true | IDENT "last" -> loc, false ]]; ssrorelse: [[ "||"; tac = tactic_expr LEVEL "2" -> tac ]]; ssrseqarg: [ [ arg = ssrswap -> noindex, swaptacarg arg | i = ssrseqidx; tac = ssrortacarg; def = OPT ssrorelse -> i, (tac, def) | i = ssrseqidx; arg = ssrswap -> i, swaptacarg arg | tac = tactic_expr LEVEL "3" -> noindex, (mk_hint tac, None) ] ]; END let tclPERM perm tac gls = let subgls = tac gls in let sigma, subgll = Refiner.unpackage subgls in let subgll' = perm subgll in Refiner.repackage sigma subgll' (* let tclPERM perm tac gls = let mkpft n g r = {Proof_type.open_subgoals = n; Proof_type.goal = g; Proof_type.ref = r} in let mkleaf g = mkpft 0 g None in let mkprpft n g pr a = mkpft n g (Some (Proof_type.Prim pr, a)) in let mkrpft n g c = mkprpft n g (Proof_type.Refine c) in let mkipft n g = let mki pft (id, _, _ as d) = let g' = {g with evar_concl = mkNamedProd_or_LetIn d g.evar_concl} in mkprpft n g' (Proof_type.Intro id) [pft] in List.fold_left mki in let gl = Refiner.sig_it gls in let mkhyp subgl = let rec chop_section = function | (x, _, _ as d) :: e when not_section_id x -> d :: chop_section e | _ -> [] in let lhyps = Environ.named_context_of_val subgl.evar_hyps in mk_perm_id (), subgl, chop_section lhyps in let mkpfvar (hyp, subgl, lhyps) = let mkarg args (lhyp, body, _) = if body = None then mkVar lhyp :: args else args in mkrpft 0 subgl (applist (mkVar hyp, List.fold_left mkarg [] lhyps)) [] in let mkpfleaf (_, subgl, lhyps) = mkipft 1 gl (mkleaf subgl) lhyps in let mkmeta _ = Evarutil.mk_new_meta () in let mkhypdecl (hyp, subgl, lhyps) = hyp, None, it_mkNamedProd_or_LetIn subgl.evar_concl lhyps in let subgls, v as res0 = tac gls in let sigma, subgll = Refiner.unpackage subgls in let n = List.length subgll in if n = 0 then res0 else let hyps = List.map mkhyp subgll in let hyp_decls = List.map mkhypdecl (List.rev (perm hyps)) in let c = applist (mkmeta (), List.map mkmeta subgll) in let pft0 = mkipft 0 gl (v (List.map mkpfvar hyps)) hyp_decls in let pft1 = mkrpft n gl c (pft0 :: List.map mkpfleaf (perm hyps)) in let subgll', v' = Refiner.frontier pft1 in Refiner.repackage sigma subgll', v' *) let tclREV tac gl = tclPERM List.rev tac gl let rot_hyps dir i hyps = let n = List.length hyps in if i = 0 then List.rev hyps else if i > n then error "Not enough subgoals" else let rec rot i l_hyps = function | hyp :: hyps' when i > 0 -> rot (i - 1) (hyp :: l_hyps) hyps' | hyps' -> hyps' @ (List.rev l_hyps) in rot (match dir with L2R -> i | R2L -> n - i) [] hyps let tclSEQAT (atac1, ctx) dir (ivar, ((_, atacs2), atac3)) = let i = get_index ivar in let evtac = ssrevaltac (get_ltacctx ctx) in let tac1 = evtac atac1 in if atacs2 = [] && atac3 <> None then tclPERM (rot_hyps dir i) tac1 else let evotac = function Some atac -> evtac atac | _ -> tclIDTAC in let tac3 = evotac atac3 in let rec mk_pad n = if n > 0 then tac3 :: mk_pad (n - 1) else [] in match dir, mk_pad (i - 1), List.map evotac atacs2 with | L2R, [], [tac2] when atac3 = None -> tclTHENFIRST tac1 tac2 | L2R, [], [tac2] when atac3 = None -> tclTHENLAST tac1 tac2 | L2R, pad, tacs2 -> tclTHENSFIRSTn tac1 (Array.of_list (pad @ tacs2)) tac3 | R2L, pad, tacs2 -> tclTHENSLASTn tac1 tac3 (Array.of_list (tacs2 @ pad)) (* We can't actually parse the direction separately because this *) (* would introduce conflicts with the basic ltac syntax. *) let pr_ssrseqdir _ _ _ = function | L2R -> str ";" ++ spc () ++ str "first " | R2L -> str ";" ++ spc () ++ str "last " ARGUMENT EXTEND ssrseqdir TYPED AS ssrdir PRINTED BY pr_ssrseqdir | [ "Qed" ] -> [ anomaly "Grammar placeholder match" ] END TACTIC EXTEND ssrtclseq | [ "Qed" ssrtclarg(tac) ssrseqdir(dir) ssrseqarg(arg) ] -> [ tclSEQAT tac dir arg ] END set_pr_ssrtac "tclseq" 5 [ArgSsr "tclarg"; ArgSsr "seqdir"; ArgSsr "seqarg"] let tclseq_expr loc tac dir arg = let arg1 = in_gen rawwit_ssrtclarg (tac, rawltacctx) in let arg2 = in_gen rawwit_ssrseqdir dir in let arg3 = in_gen rawwit_ssrseqarg (check_seqtacarg dir arg) in ssrtac_expr loc "tclseq" [arg1; arg2; arg3] GEXTEND Gram GLOBAL: tactic_expr; ssr_first: [ [ tac = ssr_first; ipats = ssrintros_ne -> tclintros_expr loc tac ipats | "["; tacl = LIST0 tactic_expr SEP "|"; "]" -> TacFirst tacl ] ]; ssr_first_else: [ [ tac1 = ssr_first; tac2 = ssrorelse -> TacOrelse (tac1, tac2) | tac = ssr_first -> tac ]]; tactic_expr: LEVEL "4" [ LEFTA [ tac1 = tactic_expr; ";"; IDENT "first"; tac2 = ssr_first_else -> TacThen (tac1,[||], tac2,[||]) | tac = tactic_expr; ";"; IDENT "first"; arg = ssrseqarg -> tclseq_expr loc tac L2R arg | tac = tactic_expr; ";"; IDENT "last"; arg = ssrseqarg -> tclseq_expr loc tac R2L arg ] ]; END (* }}} *) (** 5. Bookkeeping tactics (clear, move, case, elim) *) (* post-interpretation of terms *) let all_ok _ _ = true let pf_abs_ssrterm ?(resolve_typeclasses=false) ist gl t = let sigma, ct as t = interp_term ist gl t in let sigma, _ as t = let env = pf_env gl in if not resolve_typeclasses then t else let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in sigma, Evarutil.nf_evar sigma ct in let n, c, abstracted_away = pf_abs_evars gl t in List.fold_left Evd.remove sigma abstracted_away, pf_abs_cterm gl n c let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty = let n_binders = ref 0 in let ty = match ty with | a, (t, None) -> let rec force_type = function | GProd (l, x, k, s, t) -> incr n_binders; GProd (l, x, k, s, force_type t) | GLetIn (l, x, v, t) -> incr n_binders; GLetIn (l, x, v, force_type t) | ty -> mkRCast ty mkRType in a, (force_type t, None) | _, (_, Some ty) -> let rec force_type = function | CProdN (l, abs, t) -> n_binders := !n_binders + List.length (List.flatten (List.map pi1 abs)); CProdN (l, abs, force_type t) | CLetIn (l, n, v, t) -> incr n_binders; CLetIn (l, n, v, force_type t) | ty -> mkCCast dummy_loc ty (mkCType dummy_loc) in mk_term ' ' (force_type ty) in let strip_cast (sigma, t) = let rec aux t = match kind_of_type t with | CastType (t, ty) when !n_binders = 0 && isSort ty -> t | ProdType(n,s,t) -> decr n_binders; mkProd (n, s, aux t) | LetInType(n,v,ty,t) -> decr n_binders; mkLetIn (n, v, ty, aux t) | _ -> anomaly "pf_interp_ty: ssr Type cast deleted by typecheck" in sigma, aux t in let sigma, cty as ty = strip_cast (interp_term ist gl ty) in let ty = let env = pf_env gl in if not resolve_typeclasses then ty else let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in sigma, Evarutil.nf_evar sigma cty in let n, c, _ = pf_abs_evars gl ty in let lam_c = pf_abs_cterm gl n c in let ctx, c = decompose_lam_n n lam_c in n, compose_prod ctx c, lam_c ;; let whd_app f args = Reductionops.whd_betaiota Evd.empty (mkApp (f, args)) let pr_cargs a = str "[" ++ pr_list pr_spc pr_constr (Array.to_list a) ++ str "]" let pp_term gl t = let t = Reductionops.nf_evar (project gl) t in pr_constr t let pp_concat hd ?(sep=str", ") = function [] -> hd | x :: xs -> hd ++ List.fold_left (fun acc x -> acc ++ sep ++ x) x xs let fake_pmatcher_end () = mkProp, L2R, (Evd.empty, mkProp) (* TASSI: given (c : ty), generates (c ??? : ty[???/...]) with m evars *) exception NotEnoughProducts let prof_saturate_whd = mk_profiler "saturate.whd";; let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_of env sigma c) m = let rec loop ty args sigma n = if n = 0 then let args = List.rev args in (if beta then Reductionops.whd_beta sigma else fun x -> x) (mkApp (c, Array.of_list (List.map snd args))), ty, args, sigma else match kind_of_type ty with | ProdType (_, src, tgt) -> let sigma, x = Evarutil.new_evar (create_evar_defs sigma) env (if bi_types then Reductionops.nf_betaiota sigma src else src) in loop (subst1 x tgt) ((m - n,x) :: args) sigma (n-1) | CastType (t, _) -> loop t args sigma n | LetInType (_, v, _, t) -> loop (subst1 v t) args sigma n | SortType _ -> assert false | AtomicType _ -> let ty = prof_saturate_whd.profile (Reductionops.whd_betadeltaiota env sigma) ty in match kind_of_type ty with | ProdType _ -> loop ty args sigma n | _ -> anomaly "saturate did not find enough products" in loop ty [] sigma m let pf_saturate ?beta ?bi_types gl c ?ty m = let env, sigma, si = pf_env gl, project gl, sig_it gl in let t, ty, args, sigma = saturate ?beta ?bi_types env sigma c ?ty m in t, ty, args, re_sig si sigma (** Rewrite redex switch *) (** Generalization (discharge) item *) (* An item is a switch + term pair. *) (* type ssrgen = ssrdocc * ssrterm *) let pr_gen (docc, dt) = pr_docc docc ++ pr_cpattern dt let pr_ssrgen _ _ _ = pr_gen ARGUMENT EXTEND ssrgen TYPED AS ssrdocc * cpattern PRINTED BY pr_ssrgen | [ ssrdocc(docc) cpattern(dt) ] -> [ docc, dt ] | [ cpattern(dt) ] -> [ nodocc, dt ] END let has_occ ((_, occ), _) = occ <> None let hyp_of_var v = SsrHyp (dummy_loc, destVar v) let interp_clr = function | Some clr, (k, c) when (k = ' ' || k = '@') && is_pf_var c -> hyp_of_var c :: clr | Some clr, _ -> clr | None, _ -> [] (* XXX the k of the redex should percolate out *) let pf_interp_gen_aux ist gl to_ind ((oclr, occ), t) = let pat = interp_cpattern ist gl t None in (* UGLY API *) let cl, env, sigma = pf_concl gl, pf_env gl, project gl in let c = redex_of_pattern env pat in let c, cl = try fill_occ_pattern ~raise_NoMatch:true env sigma cl pat occ 1 with NoMatch -> c, cl in let clr = interp_clr (oclr, (tag_of_cpattern t, c)) in if not(occur_existential c) then if tag_of_cpattern t = '@' then if not (isVar c) then errorstrm (str "@ can be used with variables only") else match pf_get_hyp gl (destVar c) with | _, None, _ -> errorstrm (str "@ can be used with let-ins only") | name, Some bo, ty -> true, pat, mkLetIn (Name name, bo, ty, cl), c, clr else false, pat, pf_mkprod gl c cl, c, clr else if to_ind && occ = None then let nv, p, _ = pf_abs_evars gl (fst pat, c) in if nv = 0 then anomaly "occur_existential but no evars" else false, pat, mkProd (constr_name c, pf_type_of gl p, pf_concl gl), p, clr else loc_error (loc_of_cpattern t) "generalized term didn't match" let genclrtac cl cs clr = let tclmyORELSE tac1 tac2 gl = try tac1 gl with e when Errors.noncritical e -> tac2 e gl in (* apply_type may give a type error, but the useful message is * the one of clear. You type "move: x" and you get * "x is used in hyp H" instead of * "The term H has type T x but is expected to have type T x0". *) tclTHEN (tclmyORELSE (apply_type cl cs) (fun type_err gl -> tclTHEN (tclTHEN (elim_type (build_coq_False ())) (cleartac clr)) (fun gl -> raise type_err) gl)) (cleartac clr) let gentac ist gen gl = let conv, _, cl, c, clr = pf_interp_gen_aux ist gl false gen in if conv then tclTHEN (convert_concl cl) (cleartac clr) gl else genclrtac cl [c] clr gl let pf_interp_gen ist gl to_ind gen = let _, _, a, b ,c = pf_interp_gen_aux ist gl to_ind gen in a, b ,c (** Generalization (discharge) sequence *) (* A discharge sequence is represented as a list of up to two *) (* lists of d-items, plus an ident list set (the possibly empty *) (* final clear switch). The main list is empty iff the command *) (* is defective, and has length two if there is a sequence of *) (* dependent terms (and in that case it is the first of the two *) (* lists). Thus, the first of the two lists is never empty. *) (* type ssrgens = ssrgen list *) (* type ssrdgens = ssrgens list * ssrclear *) let gens_sep = function [], [] -> mt | _ -> spc let pr_dgens pr_gen (gensl, clr) = let prgens s gens = str s ++ pr_list spc pr_gen gens in let prdeps deps = prgens ": " deps ++ spc () ++ str "/" in match gensl with | [deps; []] -> prdeps deps ++ pr_clear pr_spc clr | [deps; gens] -> prdeps deps ++ prgens " " gens ++ pr_clear spc clr | [gens] -> prgens ": " gens ++ pr_clear spc clr | _ -> pr_clear pr_spc clr let pr_ssrdgens _ _ _ = pr_dgens pr_gen let cons_gen gen = function | gens :: gensl, clr -> (gen :: gens) :: gensl, clr | _ -> anomaly "missing gen list" let cons_dep (gensl, clr) = if List.length gensl = 1 then ([] :: gensl, clr) else error "multiple dependents switches '/'" ARGUMENT EXTEND ssrdgens_tl TYPED AS ssrgen list list * ssrclear PRINTED BY pr_ssrdgens | [ "{" ne_ssrhyp_list(clr) "}" cpattern(dt) ssrdgens_tl(dgens) ] -> [ cons_gen (mkclr clr, dt) dgens ] | [ "{" ne_ssrhyp_list(clr) "}" ] -> [ [[]], clr ] | [ "{" ssrocc(occ) "}" cpattern(dt) ssrdgens_tl(dgens) ] -> [ cons_gen (mkocc occ, dt) dgens ] | [ "/" ssrdgens_tl(dgens) ] -> [ cons_dep dgens ] | [ cpattern(dt) ssrdgens_tl(dgens) ] -> [ cons_gen (nodocc, dt) dgens ] | [ ] -> [ [[]], [] ] END ARGUMENT EXTEND ssrdgens TYPED AS ssrdgens_tl PRINTED BY pr_ssrdgens | [ ":" ssrgen(gen) ssrdgens_tl(dgens) ] -> [ cons_gen gen dgens ] END let genstac (gens, clr) ist = tclTHENLIST (cleartac clr :: List.rev_map (gentac ist) gens) (* Common code to handle generalization lists along with the defective case *) let with_defective maintac deps clr ist gl = let top_id = match kind_of_type (pf_concl gl) with | ProdType (Name id, _, _) when has_discharged_tag (string_of_id 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_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 with_deps deps0 maintac cl0 cs0 clr0 ist gl0 = let rec loop gl cl cs clr args clrs = function | [] -> let n = List.length args in maintac (if n > 0 then applist (to_lambda n cl, args) else cl) clrs ist gl0 | dep :: deps -> let gl' = first_goal (genclrtac cl cs clr gl) in let cl', c', clr' = pf_interp_gen ist gl' false dep in loop gl' cl' [c'] clr' (c' :: args) (clr' :: clrs) deps in loop gl0 cl0 cs0 clr0 cs0 [clr0] (List.rev deps0) (** Equations *) (* argument *) type ssreqid = ssripat option let pr_eqid = function Some pat -> str " " ++ pr_ipat pat | None -> mt () let pr_ssreqid _ _ _ = pr_eqid (* We must use primitive parsing here to avoid conflicts with the *) (* basic move, case, and elim tactics. *) ARGUMENT EXTEND ssreqid TYPED AS ssripatrep option PRINTED BY pr_ssreqid | [ "Qed" ] -> [ Util.anomaly "Grammar placeholder match" ] END let accept_ssreqid strm = match Compat.get_tok (Util.stream_nth 0 strm) with | Tok.IDENT _ -> accept_before_syms [":"] strm | Tok.KEYWORD ":" -> () | Tok.KEYWORD pat when List.mem pat ["_"; "?"; "->"; "<-"] -> accept_before_syms [":"] strm | _ -> raise Stream.Failure let test_ssreqid = Gram.Entry.of_parser "test_ssreqid" accept_ssreqid GEXTEND Gram GLOBAL: ssreqid; ssreqpat: [ [ id = Prim.ident -> IpatId id | "_" -> IpatWild | "?" -> IpatAnon | occ = ssrdocc; "->" -> (match occ with | None, occ -> IpatRw (occ, L2R) | _ -> loc_error loc "Only occurrences are allowed here") | occ = ssrdocc; "<-" -> (match occ with | None, occ -> IpatRw (occ, R2L) | _ -> loc_error loc "Only occurrences are allowed here") | "->" -> IpatRw (allocc, L2R) | "<-" -> IpatRw (allocc, R2L) ]]; ssreqid: [ [ test_ssreqid; pat = ssreqpat -> Some pat | test_ssreqid -> None ]]; END (* creation *) let mkEq dir cl c t n = let eqargs = [|t; c; c|] in eqargs.(dir_org dir) <- mkRel n; mkArrow (mkApp (build_coq_eq(), eqargs)) (lift 1 cl), mkRefl t c let pushmoveeqtac cl c = let x, t, cl1 = destProd cl in let cl2, eqc = mkEq R2L cl1 c t 1 in apply_type (mkProd (x, t, cl2)) [c; eqc] let pushcaseeqtac cl gl = let cl1, args = destApplication cl in let n = Array.length args in let dc, cl2 = decompose_lam_n n cl1 in let _, t = List.nth dc (n - 1) in let cl3, eqc = mkEq R2L cl2 args.(0) t n in let cl4 = mkApp (compose_lam dc (mkProt (pf_type_of gl cl) cl3), args) in tclTHEN (apply_type cl4 [eqc]) (convert_concl cl4) gl let pushelimeqtac gl = let _, args = destApplication (pf_concl gl) in let x, t, _ = destLambda args.(1) in let cl1 = mkApp (args.(1), Array.sub args 2 (Array.length args - 2)) in let cl2, eqc = mkEq L2R cl1 args.(2) t 1 in tclTHEN (apply_type (mkProd (x, t, cl2)) [args.(2); eqc]) intro gl (** Bookkeeping (discharge-intro) argument *) (* Since all bookkeeping ssr commands have the same discharge-intro *) (* argument format we use a single grammar entry point to parse them. *) (* the entry point parses only non-empty arguments to avoid conflicts *) (* with the basic Coq tactics. *) (* type ssrarg = ssrview * (ssreqid * (ssrdgens * ssripats)) *) let pr_ssrarg _ _ _ (view, (eqid, (dgens, ipats))) = let pri = pr_intros (gens_sep dgens) in pr_view view ++ pr_eqid eqid ++ pr_dgens pr_gen dgens ++ pri ipats ARGUMENT EXTEND ssrarg TYPED AS ssrview * (ssreqid * (ssrdgens * ssrintros)) PRINTED BY pr_ssrarg | [ ssrview(view) ssreqid(eqid) ssrdgens(dgens) ssrintros(ipats) ] -> [ view, (eqid, (dgens, ipats)) ] | [ ssrview(view) ssrclear(clr) ssrintros(ipats) ] -> [ view, (None, (([], clr), ipats)) ] | [ ssreqid(eqid) ssrdgens(dgens) ssrintros(ipats) ] -> [ [], (eqid, (dgens, ipats)) ] | [ ssrclear_ne(clr) ssrintros(ipats) ] -> [ [], (None, (([], clr), ipats)) ] | [ ssrintros_ne(ipats) ] -> [ [], (None, (([], []), ipats)) ] END (** The "clear" tactic *) (* We just add a numeric version that clears the n top assumptions. *) let poptac ?ist n = introstac ?ist (list_tabulate (fun _ -> IpatWild) n) TACTIC EXTEND ssrclear | [ "clear" natural(n) ltacctx(ctx) ] -> [poptac ~ist:(get_ltacctx ctx) n] END (** The "move" tactic *) let rec improper_intros = function | IpatSimpl _ :: ipats -> improper_intros ipats | (IpatId _ | IpatAnon | IpatCase _ | IpatAll) :: _ -> false | _ -> true let check_movearg = function | view, (eqid, _) when view <> [] && eqid <> None -> Util.error "incompatible view and equation in move tactic" | view, (_, (([gen :: _], _), _)) when view <> [] && has_occ gen -> Util.error "incompatible view and occurrence switch in move tactic" | _, (_, ((dgens, _), _)) when List.length dgens > 1 -> Util.error "dependents switch `/' in move tactic" | _, (eqid, (_, (ipats, _))) when eqid <> None && improper_intros ipats -> Util.error "no proper intro pattern for equation in move tactic" | arg -> arg ARGUMENT EXTEND ssrmovearg TYPED AS ssrarg PRINTED BY pr_ssrarg | [ ssrarg(arg) ] -> [ check_movearg arg ] END let viewmovetac_aux clear name_ref (_, vl as v) _ gen ist gl = let cl, c, clr, gen_pat = let _, gen_pat, a, b, c = pf_interp_gen_aux ist gl false gen in a, b, c, gen_pat in let cl, c = if vl = [] then cl, c else pf_with_view ist gl v cl c in let clr = if clear then clr else [] in name_ref := (match id_of_pattern gen_pat with Some id -> id | _ -> top_id); genclrtac cl [c] clr gl let () = move_top_with_view := (fun c r v -> with_defective (viewmovetac_aux c r v) [] []) let viewmovetac v deps gen ist gl = viewmovetac_aux true (ref top_id) v deps gen ist gl let eqmovetac _ gen ist gl = let cl, c, _ = pf_interp_gen ist gl false gen in pushmoveeqtac cl c gl let movehnftac gl = match kind_of_term (pf_concl gl) with | Prod _ | LetIn _ -> tclIDTAC gl | _ -> hnf_in_concl gl let ssrmovetac ist = function | _::_ as view, (_, (dgens, (ipats, _))) -> let dgentac = with_dgens dgens (viewmovetac (true, view)) ist in tclTHEN dgentac (introstac ~ist 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 ist_of_arg (_, (_, (_, (_, ctx)))) = get_ltacctx ctx TACTIC EXTEND ssrmove | [ "move" ssrmovearg(arg) ssrrpat(pat) ] -> [ let ist = ist_of_arg arg in tclTHEN (ssrmovetac ist arg) (introstac ~ist [pat]) ] | [ "move" ssrmovearg(arg) ssrclauses(clauses) ] -> [ let ist = ist_of_arg arg in tclCLAUSES ist (ssrmovetac ist arg) clauses ] | [ "move" ssrrpat(pat) ltacctx(ctx) ] -> [ introstac ~ist:(get_ltacctx ctx) [pat] ] | [ "move" ] -> [ movehnftac ] END (* TASSI: given the type of an elimination principle, it finds the higher order * argument (index), it computes it's arity and the arity of the eliminator and * checks if the eliminator is recursive or not *) let analyze_eliminator elimty env sigma = let rec loop ctx t = match kind_of_type t with | AtomicType (hd, args) when isRel hd -> ctx, destRel hd, not (noccurn 1 t), Array.length args | CastType (t, _) -> loop ctx t | ProdType (x, ty, t) -> loop ((x,None,ty) :: ctx) t | LetInType (x,b,ty,t) -> loop ((x,Some b,ty) :: ctx) (subst1 b t) | _ -> let env' = Environ.push_rel_context ctx env in let t' = Reductionops.whd_betadeltaiota env' sigma t in if not (eq_constr t t') then loop ctx t' else errorstrm (str"The eliminator has the wrong shape."++spc()++ str"A (applied) bound variable was expected as the conclusion of "++ str"the eliminator's"++Pp.cut()++str"type:"++spc()++pr_constr elimty) in let ctx, pred_id, elim_is_dep, n_pred_args = loop [] elimty in let n_elim_args = rel_context_nhyps ctx in let is_rec_elim = let count_occurn n term = let count = ref 0 in let rec occur_rec n c = match kind_of_term c with | Rel m -> if m = n then incr count | _ -> iter_constr_with_binders succ occur_rec n c in occur_rec n term; !count in let occurr2 n t = count_occurn n t > 1 in not (list_for_all_i (fun i (_,rd) -> pred_id <= i || not (occurr2 (pred_id - i) rd)) 1 (assums_of_rel_context ctx)) in n_elim_args - pred_id, n_elim_args, is_rec_elim, elim_is_dep, n_pred_args (* TASSI: This version of unprotects inlines the unfold tactic definition, * since we don't want to wipe out let-ins, and it seems there is no flag * to change that behaviour in the standard unfold code *) let unprotecttac gl = let prot = destConst (mkSsrConst "protect_term") in onClause (fun idopt -> let hyploc = Option.map (fun id -> id, InHyp) idopt in reduct_option (Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fBETA; Closure.RedFlags.fCONST prot; Closure.RedFlags.fIOTA]), DEFAULTcast) hyploc) allHypsAndConcl gl let dependent_apply_error = try Util.error "Could not fill dependent hole in \"apply\"" with err -> err (* TASSI: Sometimes Coq's apply fails. According to my experience it may be * related to goals that are products and with beta redexes. In that case it * guesses the wrong number of implicit arguments for your lemma. What follows * is just like apply, but with a user-provided number n of implicits. * * Refine.refine function that handles type classes and evars but fails to * handle "dependently typed higher order evars". * * Refiner.refiner that does not handle metas with a non ground type but works * with dependently typed higher order metas. *) let applyn ~with_evars ?beta n t gl = if with_evars then let t, ty, args, gl = pf_saturate ?beta ~bi_types:true gl t n in let gl = pf_unify_HO gl ty (pf_concl gl) in let gs = list_map_filter (fun (_, e) -> if isEvar (pf_nf_evar gl e) then Some e else None) args in pf_partial_solution ~shelve:true gl t gs else let t, gl = if n = 0 then t, gl else let sigma, si = project gl, sig_it gl in let rec loop sigma bo args = function (* saturate with metas *) | 0 -> mkApp (t, Array.of_list (List.rev args)), re_sig si sigma | n -> match kind_of_term bo with | Lambda (_, ty, bo) -> if not (closed0 ty) then raise dependent_apply_error; let m = Evarutil.new_meta () in loop (meta_declare m ty sigma) bo ((mkMeta m)::args) (n-1) | _ -> assert false in loop sigma t [] n in pp(lazy(str"Refiner.refiner " ++ pr_constr t)); Refiner.refiner (Proof_type.Prim (Proof_type.Refine t)) gl let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl = let rec mkRels = function 1 -> [] | n -> mkRel n :: mkRels (n-1) in let n, oc = pf_abs_evars_pirrel gl oc in let oc = if not first_goes_last || n <= 1 then oc else let l, c = decompose_lam oc in if not (list_for_all_i (fun i (_,t) -> closedn ~-i t) (1-n) l) then oc else compose_lam (let xs,y = list_chop (n-1) l in y @ xs) (mkApp (compose_lam l c, Array.of_list (mkRel 1 :: mkRels n))) in pp(lazy(str"after: " ++ pr_constr oc)); try applyn ~with_evars ?beta n oc gl with _ -> raise dependent_apply_error (** The "case" and "elim" tactic *) (* A case without explicit dependent terms but with both a view and an *) (* occurrence switch and/or an equation is treated as dependent, with the *) (* viewed term as the dependent term (the occurrence switch would be *) (* meaningless otherwise). When both a view and explicit dependents are *) (* present, it is forbidden to put a (meaningless) occurrence switch on *) (* the viewed term. *) (* This is both elim and case (defaulting to the former). If ~elim is omitted * the standard eliminator is chosen. The code is made of 4 parts: * 1. find the eliminator if not given as ~elim and analyze it * 2. build the patterns to be matched against the conclusion, looking at * (occ, c), deps and the pattern inferred from the type of the eliminator * 3. build the new predicate matching the patterns, and the tactic to * generalize the equality in case eqid is not None * 4. build the tactic handle intructions and clears as required in ipats and * by eqid *) let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl = (* some sanity checks *) let oc, orig_clr, occ, c_gen = match what with | `EConstr(_,_,t) when isEvar t -> anomaly "elim called on a constr evar" | `EGen _ when ist = None -> anomaly "no ist and non simple elimination" | `EGen (_, g) when elim = None && is_wildcard g -> errorstrm(str"Indeterminate pattern and no eliminator") | `EGen ((Some clr,occ), g) when is_wildcard g -> None, clr, occ, None | `EGen ((None, occ), g) when is_wildcard g -> None,[],occ,None | `EGen ((_, occ), p as gen) -> let _, c, clr = pf_interp_gen (Option.get ist) gl true gen in Some c, clr, occ, Some p | `EConstr (clr, occ, c) -> Some c, clr, occ, None in let orig_gl, concl, env = gl, pf_concl gl, pf_env gl in pp(lazy(str(if is_case then "==CASE==" else "==ELIM=="))); (* Utils of local interest only *) let iD s ?t gl = let t = match t with None -> pf_concl gl | Some x -> x in pp(lazy(str s ++ pr_constr t)); tclIDTAC gl in let eq, protectC = build_coq_eq (), mkSsrConst "protect_term" in let fire_subst gl t = Reductionops.nf_evar (project gl) t in let fire_sigma sigma t = Reductionops.nf_evar sigma t in let is_undef_pat = function | sigma, T t -> (match kind_of_term (fire_sigma sigma t) with Evar _ -> true | _ -> false) | _ -> false in let match_pat env p occ h cl = let sigma0 = project orig_gl in pp(lazy(str"matching: " ++ pp_pattern p)); let c, cl = fill_occ_pattern ~raise_NoMatch:true env sigma0 cl p occ h in pp(lazy(str" got: " ++ pr_constr c)); c, cl in let mkTpat gl t = (* takes a term, refreshes it and makes a T pattern *) let n, t, _ = pf_abs_evars orig_gl (project gl, fire_subst gl t) in let t, _, _, sigma = saturate ~beta:true env (project gl) t n in sigma, T t in let unif_redex gl (sigma, r as p) t = (* t is a hint for the redex of p *) let n, t, _ = pf_abs_evars orig_gl (project gl, fire_subst gl t) in let t, _, _, sigma = saturate ~beta:true env sigma t n in match r with | X_In_T (e, p) -> sigma, E_As_X_In_T (t, e, p) | _ -> try unify_HO env sigma t (redex_of_pattern env p), r with _ -> p in (* finds the eliminator applies it to evars and c saturated as needed *) (* obtaining "elim ??? (c ???)". pred is the higher order evar *) let cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl = match elim with | Some elim -> let elimty = pf_type_of gl elim in let pred_id, n_elim_args, is_rec, elim_is_dep, n_pred_args = analyze_eliminator elimty env (project gl) in let elim, elimty, elim_args, gl = pf_saturate ~beta:is_case gl elim ~ty:elimty n_elim_args in let pred = List.assoc pred_id elim_args in let elimty = Reductionops.whd_betadeltaiota env (project gl) elimty in None, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl | None -> let c = Option.get oc in let c_ty = pf_type_of gl c in let (kn, i) as ind, unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in let sort = elimination_sort_of_goal gl in let elim = if not is_case then Indrec.lookup_eliminator ind sort else pf_apply Indrec.build_case_analysis_scheme gl ind true sort in let elimty = pf_type_of gl elim in let pred_id,n_elim_args,is_rec,elim_is_dep,n_pred_args = analyze_eliminator elimty env (project gl) in let rctx = fst (decompose_prod_assum unfolded_c_ty) in let n_c_args = rel_context_length rctx in let c, c_ty, t_args, gl = pf_saturate gl c ~ty:c_ty n_c_args in let elim, elimty, elim_args, gl = pf_saturate ~beta:is_case gl elim ~ty:elimty n_elim_args in let pred = List.assoc pred_id elim_args in let pc = match n_c_args, c_gen with | 0, Some p -> interp_cpattern (Option.get ist) orig_gl p None | _ -> mkTpat gl c in let cty = Some (c, c_ty, pc) in let elimty = Reductionops.whd_betadeltaiota env (project gl) elimty in cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl in pp(lazy(str"elim= "++ pr_constr_pat elim)); pp(lazy(str"elimty= "++ pr_constr elimty)); let inf_deps_r = match kind_of_type elimty with | AtomicType (_, args) -> List.rev (Array.to_list args) | _ -> assert false in let saturate_until gl c c_ty f = let rec loop n = try let c, c_ty, _, gl = pf_saturate gl c ~ty:c_ty n in let gl' = f c c_ty gl in Some (c, c_ty, gl, gl') with NotEnoughProducts -> None | _ -> loop (n+1) in loop 0 in let elim_is_dep, gl = match cty with | None -> true, gl | Some (c, c_ty, _) -> let res = if elim_is_dep then None else let arg = List.assoc (n_elim_args - 1) elim_args in let arg_ty = pf_type_of gl arg in match saturate_until gl c c_ty (fun c c_ty gl -> pf_unify_HO (pf_unify_HO gl c_ty arg_ty) arg c) with | Some (c, _, _, gl) -> Some (false, gl) | None -> None in match res with | Some x -> x | None -> let inf_arg = List.hd inf_deps_r in let inf_arg_ty = pf_type_of gl inf_arg in match saturate_until gl c c_ty (fun _ c_ty gl -> pf_unify_HO gl c_ty inf_arg_ty) with | Some (c, _, _,gl) -> true, gl | None -> errorstrm (str"Unable to apply the eliminator to the term"++ spc()++pr_constr c++spc()++str"or to unify it's type with"++ pr_constr inf_arg_ty) in pp(lazy(str"elim_is_dep= " ++ bool elim_is_dep)); let predty = pf_type_of gl pred in (* Patterns for the inductive types indexes to be bound in pred are computed * looking at the ones provided by the user and the inferred ones looking at * the type of the elimination principle *) let pp_pat (_,p,_,_) = pp_pattern p in let pp_inf_pat gl (_,_,t,_) = pr_constr_pat (fire_subst gl t) in let patterns, clr, gl = let rec loop patterns clr i = function | [],[] -> patterns, clr, gl | ((oclr, occ), t):: deps, inf_t :: inf_deps -> let ist = match ist with Some x -> x | None -> assert false in let p = interp_cpattern ist orig_gl t None in let clr_t = interp_clr (oclr,(tag_of_cpattern t,redex_of_pattern env p))in (* if we are the index for the equation we do not clear *) let clr_t = if deps = [] && eqid <> None then [] else clr_t in let p = if is_undef_pat p then mkTpat gl inf_t else p in loop (patterns @ [i, p, inf_t, occ]) (clr_t @ clr) (i+1) (deps, inf_deps) | [], c :: inf_deps -> pp(lazy(str"adding inferred pattern " ++ pr_constr_pat c)); loop (patterns @ [i, mkTpat gl c, c, allocc]) clr (i+1) ([], inf_deps) | _::_, [] -> errorstrm (str "Too many dependent abstractions") in let deps, head_p, inf_deps_r = match what, elim_is_dep, cty with | `EConstr _, _, None -> anomaly "Simple welim with no term" | _, false, _ -> deps, [], inf_deps_r | `EGen gen, true, None -> deps @ [gen], [], inf_deps_r | _, true, Some (c, _, pc) -> let occ = if occ = None then allocc else occ in let inf_p, inf_deps_r = List.hd inf_deps_r, List.tl inf_deps_r in deps, [1, pc, inf_p, occ], inf_deps_r in let patterns, clr, gl = loop [] orig_clr (List.length head_p+1) (List.rev deps, inf_deps_r) in head_p @ patterns, Util.list_uniquize clr, gl in pp(lazy(pp_concat (str"patterns=") (List.map pp_pat patterns))); pp(lazy(pp_concat (str"inf. patterns=") (List.map (pp_inf_pat gl) patterns))); (* Predicate generation, and (if necessary) tactic to generalize the * equation asked by the user *) let elim_pred, gen_eq_tac, clr, gl = let error gl t inf_t = errorstrm (str"The given pattern matches the term"++ spc()++pp_term gl t++spc()++str"while the inferred pattern"++ spc()++pr_constr_pat (fire_subst gl inf_t)++spc()++ str"doesn't") in let match_or_postpone (cl, gl, post) (h, p, inf_t, occ) = let p = unif_redex gl p inf_t in if is_undef_pat p then let () = pp(lazy(str"postponing " ++ pp_pattern p)) in cl, gl, post @ [h, p, inf_t, occ] else try let c, cl = match_pat env p occ h cl in let gl = try pf_unify_HO gl inf_t c with _ -> error gl c inf_t in cl, gl, post with | NoMatch | NoProgress -> let e = redex_of_pattern env p in let n, e, _ = pf_abs_evars gl (fst p, e) in let e, _, _, gl = pf_saturate ~beta:true gl e n in let gl = try pf_unify_HO gl inf_t e with _ -> error gl e inf_t in cl, gl, post in let rec match_all concl gl patterns = let concl, gl, postponed = List.fold_left match_or_postpone (concl, gl, []) patterns in if postponed = [] then concl, gl else if List.length postponed = List.length patterns then errorstrm (str "Some patterns are undefined even after all"++spc()++ str"the defined ones matched") else match_all concl gl postponed in let concl, gl = match_all concl gl patterns in let pred_rctx, _ = decompose_prod_assum (fire_subst gl predty) in let concl, gen_eq_tac, clr = match eqid with | Some (IpatId _) when not is_rec -> let k = List.length deps in let c = fire_subst gl (List.assoc (n_elim_args - k - 1) elim_args) in let t = pf_type_of gl c in let gen_eq_tac = let refl = mkApp (eq, [|t; c; c|]) in let new_concl = mkArrow refl (lift 1 (pf_concl orig_gl)) in let new_concl = fire_subst gl new_concl in let erefl = fire_subst gl (mkRefl t c) in apply_type new_concl [erefl] in let rel = k + if elim_is_dep then 1 else 0 in let src = mkProt mkProp (mkApp (eq,[|t; c; mkRel rel|])) in let concl = mkArrow src (lift 1 concl) in let clr = if deps <> [] then clr else [] in concl, gen_eq_tac, clr | _ -> concl, tclIDTAC, clr in let mk_lam t r = mkLambda_or_LetIn r t in let concl = List.fold_left mk_lam concl pred_rctx in let concl = if eqid <> None && is_rec then mkProt (pf_type_of gl concl) concl else concl in concl, gen_eq_tac, clr, gl in pp(lazy(str"elim_pred=" ++ pp_term gl elim_pred)); let pty = Typing.type_of env (project gl) elim_pred in pp(lazy(str"elim_pred_ty=" ++ pp_term gl pty)); let gl = pf_unify_HO gl pred elim_pred in (* check that the patterns do not contain non instantiated dependent metas *) let () = let evars_of_term = Evarutil.evars_of_term in let patterns = List.map (fun (_,_,t,_) -> fire_subst gl t) patterns in let patterns_ev = List.map evars_of_term patterns in let ev = List.fold_left Intset.union Intset.empty patterns_ev in let ty_ev = Intset.fold (fun i e -> let ex = Evd.existential_of_int i in let i_ty = Evd.evar_concl (Evd.find (project gl) ex) in Intset.union e (evars_of_term i_ty)) ev Intset.empty in let inter = Intset.inter ev ty_ev in if not (Intset.is_empty inter) then begin let i = Intset.choose inter in let pat = List.find (fun t -> Intset.mem i (evars_of_term t)) patterns in errorstrm(str"Pattern"++spc()++pr_constr_pat pat++spc()++ str"was not completely instantiated and one of its variables"++spc()++ str"occurs in the type of another non-instantiated pattern variable"); end in (* the elim tactic, with the eliminator and the predicated we computed *) let elim = project gl, fire_subst gl elim in let elim_tac gl = tclTHENLIST [refine_with ~with_evars:false elim; cleartac clr] gl in (* handling of following intro patterns and equation introduction if any *) let elim_intro_tac gl = let intro_eq = match eqid with | Some (IpatId ipat) when not is_rec -> let rec intro_eq gl = match kind_of_type (pf_concl gl) with | ProdType (_, src, tgt) -> (match kind_of_type src with | AtomicType (hd, _) when eq_constr hd protectC -> tclTHENLIST [unprotecttac; introid ipat] gl | _ -> tclTHENLIST [ iD "IA"; introstac [IpatAnon]; intro_eq] gl) |_ -> errorstrm (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 = let elim_name = match orig_clr, what with | [SsrHyp(_, x)], _ -> x | _, `EConstr(_,_,t) when isVar t -> destVar 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 = decompose_prod_assum concl in let args = match kind_of_type last with | AtomicType (hd, args) -> assert(eq_constr hd protectC); args | _ -> assert false in let case = args.(Array.length args-1) in if not(closed0 case) then tclTHEN (introstac [IpatAnon]) gen_eq_tac gl else let case_ty = pf_type_of gl case in let refl = mkApp (eq, [|lift 1 case_ty; mkRel 1; lift 1 case|]) in let new_concl = fire_subst gl (mkProd (Name (name gl), case_ty, mkArrow refl (lift 2 concl))) in let erefl = fire_subst gl (mkRefl case_ty case) in apply_type new_concl [case;erefl] gl in tclTHENLIST [gen_eq_tac; intro_lhs; introid ipat] | _ -> tclIDTAC in let unprot = if eqid <> None && is_rec then unprotecttac else tclIDTAC in tclEQINTROS ?ist elim_tac (tclTHENLIST [intro_eq; unprot]) ipats gl in tclTHENLIST [gen_eq_tac; elim_intro_tac] orig_gl ;; let simplest_newelim x= ssrelim ~is_case:false [] (`EConstr ([],None,x)) None [] let simplest_newcase x= ssrelim ~is_case:true [] (`EConstr ([],None,x)) None [] let _ = simplest_newcase_ref := simplest_newcase let check_casearg = function | view, (_, (([_; gen :: _], _), _)) when view <> [] && has_occ gen -> Util.error "incompatible view and occurrence switch in dependent case tactic" | arg -> arg ARGUMENT EXTEND ssrcasearg TYPED AS ssrarg PRINTED BY pr_ssrarg | [ ssrarg(arg) ] -> [ check_casearg arg ] END 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 = pf_interp_gen ist gl true gen in let vc = if view = [] then c else snd(pf_with_view 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 ipats gl in with_dgens dgens (ndefectcasetac view eqid ipats) ist TACTIC EXTEND ssrcase | [ "case" ssrcasearg(arg) ssrclauses(clauses) ] -> [ let _, (_, (_, (_, ctx))) = arg in let ist = get_ltacctx ctx in tclCLAUSES ist (ssrcasetac ist arg) clauses ] | [ "case" ] -> [ with_top ssrscasetac ] END (** The "elim" tactic *) (* Elim views are elimination lemmas, so the eliminated term is not addded *) (* 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 ist (view, (eqid, (dgens, (ipats, _)))) = let ndefectelimtac view eqid ipats deps gen ist gl = let elim = match view with [v] -> Some (snd(force_term ist gl v)) | _ -> None in ssrelim ~ist deps (`EGen gen) ?elim eqid ipats gl in with_dgens dgens (ndefectelimtac view eqid ipats) ist TACTIC EXTEND ssrelim | [ "elim" ssrarg(arg) ssrclauses(clauses) ] -> [ let _, (_, (_, (_, ctx))) = arg in let ist = get_ltacctx ctx in tclCLAUSES ist (ssrelimtac ist arg) clauses ] | [ "elim" ] -> [ with_top simplest_newelim ] END (** 6. Backward chaining tactics: apply, exact, congr. *) (** The "apply" tactic *) let pr_agen (docc, dt) = pr_docc docc ++ pr_term dt let pr_ssragen _ _ _ = pr_agen let pr_ssragens _ _ _ = pr_dgens pr_agen ARGUMENT EXTEND ssragen TYPED AS ssrdocc * ssrterm PRINTED BY pr_ssragen | [ "{" ne_ssrhyp_list(clr) "}" ssrterm(dt) ] -> [ mkclr clr, dt ] | [ ssrterm(dt) ] -> [ nodocc, dt ] END ARGUMENT EXTEND ssragens TYPED AS ssragen list list * ssrclear PRINTED BY pr_ssragens | [ "{" ne_ssrhyp_list(clr) "}" ssrterm(dt) ssragens(agens) ] -> [ cons_gen (mkclr clr, dt) agens ] | [ "{" ne_ssrhyp_list(clr) "}" ] -> [ [[]], clr] | [ ssrterm(dt) ssragens(agens) ] -> [ cons_gen (nodocc, dt) agens ] | [ ] -> [ [[]], [] ] END let mk_applyarg views agens intros = views, (None, (agens, intros)) let pr_ssraarg _ _ _ (view, (eqid, (dgens, ipats))) = let pri = pr_intros (gens_sep dgens) in pr_view view ++ pr_eqid eqid ++ pr_dgens pr_agen dgens ++ pri ipats ARGUMENT EXTEND ssrapplyarg TYPED AS ssrview * (ssreqid * (ssragens * ssrintros)) PRINTED BY pr_ssraarg | [ ":" ssragen(gen) ssragens(dgens) ssrintros(intros) ] -> [ mk_applyarg [] (cons_gen gen dgens) intros ] | [ ssrclear_ne(clr) ssrintros(intros) ] -> [ mk_applyarg [] ([], clr) intros ] | [ ssrintros_ne(intros) ] -> [ mk_applyarg [] ([], []) intros ] | [ ssrview(view) ":" ssragen(gen) ssragens(dgens) ssrintros(intros) ] -> [ mk_applyarg view (cons_gen gen dgens) intros ] | [ ssrview(view) ssrclear(clr) ssrintros(intros) ] -> [ mk_applyarg view ([], clr) intros ] END let interp_agen ist gl ((goclr, _), (k, gc)) (clr, rcs) = let rc = glob_constr ist (project gl) (pf_env gl) gc in let rcs' = rc :: rcs in match goclr with | None -> clr, rcs' | Some ghyps -> let clr' = snd (interp_hyps ist gl ghyps) @ clr in if k <> ' ' then clr', rcs' else match rc with | GVar (loc, id) when not_section_id id -> SsrHyp (loc, id) :: clr', rcs' | GRef (loc, VarRef id) when not_section_id id -> SsrHyp (loc, id) :: clr', rcs' | _ -> clr', rcs' let interp_agens ist gl gagens = match List.fold_right (interp_agen ist gl) gagens ([], []) with | clr, rlemma :: args -> let n = interp_nbargs ist gl rlemma - List.length args in let rec loop i = if i > n then errorstrm (str "Cannot apply lemma " ++ pf_pr_glob_constr gl rlemma) else try interp_refine ist gl (mkRApp rlemma (mkRHoles i @ args)) with _ -> loop (i + 1) in clr, loop 0 | _ -> assert false let apply_rconstr ?ist t gl = let n = match ist, t with | None, (GVar (_, id) | GRef (_, VarRef id)) -> pf_nbargs gl (mkVar id) | Some ist, _ -> interp_nbargs ist gl t | _ -> anomaly "apply_rconstr without ist and not RVar" in let mkRlemma i = mkRApp t (mkRHoles i) in let cl = pf_concl gl in let rec loop i = if i > n then errorstrm (str"Cannot apply lemma "++pf_pr_glob_constr gl t) else try pf_match gl (mkRlemma i) cl with _ -> loop (i + 1) in refine_with (loop 0) gl let mkRAppView ist gl rv gv = let nb_view_imps = interp_view_nbimps ist gl rv in mkRApp rv (mkRHoles (abs nb_view_imps)) let prof_apply_interp_with = mk_profiler "ssrapplytac.interp_with";; let refine_interp_apply_view i ist gl gv = let pair i = List.map (fun x -> i, x) in let rv = pf_intern_term ist gl gv in let v = mkRAppView ist gl rv gv in let interp_with (i, hint) = interp_refine ist gl (mkRApp hint (v :: mkRHoles i)) in let interp_with x = prof_apply_interp_with.profile interp_with x in let rec loop = function | [] -> (try apply_rconstr ~ist rv gl with _ -> view_error "apply" gv) | h :: hs -> (try refine_with (snd (interp_with h)) gl with _ -> loop hs) in loop (pair i viewtab.(i) @ if i = 2 then pair 1 viewtab.(1) else []) let apply_top_tac gl = tclTHENLIST [introid top_id; apply_rconstr (mkRVar top_id); clear [top_id]] gl let inner_ssrapplytac gviews ggenl gclr ist gl = let _, clr = interp_hyps ist gl gclr in let vtac gv i gl' = refine_interp_apply_view i ist gl' gv in let ggenl, tclGENTAC = if gviews <> [] && ggenl <> [] then let ggenl= List.map (fun (x,g) -> x, cpattern_of_term g) (List.hd ggenl) in [], tclTHEN (genstac (ggenl,[]) ist) else ggenl, tclTHEN tclIDTAC in tclGENTAC (fun gl -> match gviews, ggenl with | v :: tl, [] -> let dbl = if List.length tl = 1 then 2 else 1 in tclTHEN (List.fold_left (fun acc v -> tclTHENLAST acc (vtac v dbl)) (vtac v 1) tl) (cleartac clr) gl | [], [agens] -> let clr', (_, lemma) = interp_agens ist gl agens in tclTHENLIST [cleartac clr; refine_with ~beta:true lemma; cleartac clr'] gl | _, _ -> tclTHEN apply_top_tac (cleartac clr) gl) gl let ssrapplytac (views, (_, ((gens, clr), intros))) = tclINTROS (inner_ssrapplytac views gens clr) intros let prof_ssrapplytac = mk_profiler "ssrapplytac";; let ssrapplytac arg gl = prof_ssrapplytac.profile (ssrapplytac arg) gl;; TACTIC EXTEND ssrapply | [ "apply" ssrapplyarg(arg) ] -> [ ssrapplytac arg ] | [ "apply" ] -> [ apply_top_tac ] END (** The "exact" tactic *) let mk_exactarg views dgens = mk_applyarg views dgens ([], rawltacctx) ARGUMENT EXTEND ssrexactarg TYPED AS ssrapplyarg PRINTED BY pr_ssraarg | [ ":" ssragen(gen) ssragens(dgens) ] -> [ mk_exactarg [] (cons_gen gen dgens) ] | [ ssrview(view) ssrclear(clr) ] -> [ mk_exactarg view ([], clr) ] | [ ssrclear_ne(clr) ] -> [ mk_exactarg [] ([], clr) ] END let vmexacttac pf gl = exact_no_check (mkCast (pf, VMcast, pf_concl gl)) gl TACTIC EXTEND ssrexact | [ "exact" ssrexactarg(arg) ] -> [ tclBY (ssrapplytac arg) ] | [ "exact" ] -> [ tclORELSE donetac (tclBY apply_top_tac) ] | [ "exact" "<:" lconstr(pf) ] -> [ vmexacttac pf ] END (** The "congr" tactic *) type ssrcongrarg = open_constr * (int * constr) let pr_ssrcongrarg _ _ _ (_, ((n, f), dgens)) = (if n <= 0 then mt () else str " " ++ pr_int n) ++ str " " ++ pr_term f ++ pr_dgens pr_gen dgens ARGUMENT EXTEND ssrcongrarg TYPED AS ltacctx * ((int * ssrterm) * ssrdgens) PRINTED BY pr_ssrcongrarg | [ natural(n) constr(c) ssrdgens(dgens) ] -> [ rawltacctx, ((n, mk_term ' ' c), dgens) ] | [ natural(n) constr(c) ] -> [ rawltacctx, ((n, mk_term ' ' c),([[]],[])) ] | [ constr(c) ssrdgens(dgens) ] -> [ rawltacctx, ((0, mk_term ' ' c), dgens) ] | [ constr(c) ] -> [ rawltacctx, ((0, mk_term ' ' c), ([[]],[])) ] END let rec mkRnat n = if n <= 0 then GRef (dummy_loc, glob_O) else mkRApp (GRef (dummy_loc, glob_S)) [mkRnat (n - 1)] let interp_congrarg_at ist gl n rf ty m = pp(lazy(str"===interp_congrarg_at===")); let congrn = mkSsrRRef "nary_congruence" in let args1 = mkRnat n :: mkRHoles n @ [ty] in let args2 = mkRHoles (3 * n) in let rec loop i = if i + n > m then None else try let rt = mkRApp congrn (args1 @ mkRApp rf (mkRHoles i) :: args2) in pp(lazy(str"rt=" ++ pr_glob_constr rt)); Some (interp_refine ist gl rt) with _ -> loop (i + 1) in loop 0 let pattern_id = mk_internal_id "pattern value" let congrtac ((n, t), ty) ist gl = pp(lazy(str"===congr===")); pp(lazy(str"concl=" ++ pr_constr (pf_concl gl))); let _, f, _ = pf_abs_evars gl (interp_term ist gl t) in let ist' = {ist with lfun = [pattern_id, VConstr ([],f)]} in let rf = mkRltacVar pattern_id in let m = pf_nbargs gl f in let _, cf = if n > 0 then match interp_congrarg_at ist' gl n rf ty m with | Some cf -> cf | None -> errorstrm (str "No " ++ pr_int n ++ str "-congruence with " ++ pr_term t) else let rec loop i = if i > m then errorstrm (str "No congruence with " ++ pr_term t) else match interp_congrarg_at ist' gl i rf ty m with | Some cf -> cf | None -> loop (i + 1) in loop 1 in tclTHEN (refine_with cf) (tclTRY reflexivity) gl let newssrcongrtac arg ist gl = pp(lazy(str"===newcongr===")); pp(lazy(str"concl=" ++ pr_constr (pf_concl gl))); (* utils *) let fs gl t = Reductionops.nf_evar (project gl) t in let tclMATCH_GOAL (c, gl_c) proj t_ok t_fail gl = match try Some (pf_unify_HO gl_c (pf_concl gl) c) with _ -> None with | Some gl_c -> tclTHEN (convert_concl (fs gl_c c)) (t_ok (proj gl_c)) gl | None -> t_fail () gl in let mk_evar gl ty = let env, sigma, si = pf_env gl, project gl, sig_it gl in let sigma, x = Evarutil.new_evar (create_evar_defs sigma) env ty in x, re_sig si sigma in let ssr_congr lr = mkApp (mkSsrConst "ssr_congr_arrow",lr) in (* here thw two cases: simple equality or arrow *) let equality, _, eq_args, gl' = pf_saturate gl (build_coq_eq ()) 3 in tclMATCH_GOAL (equality, gl') (fun gl' -> fs gl' (List.assoc 0 eq_args)) (fun ty -> congrtac (arg, Detyping.detype false [] [] ty) ist) (fun () -> let lhs, gl' = mk_evar gl mkProp in let rhs, gl' = mk_evar gl' mkProp in let arrow = mkArrow lhs (lift 1 rhs) in tclMATCH_GOAL (arrow, gl') (fun gl' -> [|fs gl' lhs;fs gl' rhs|]) (fun lr -> tclTHEN (apply (ssr_congr lr)) (congrtac (arg, mkRType) ist)) (fun _ _ -> errorstrm (str"Conclusion is not an equality nor an arrow"))) gl ;; TACTIC EXTEND ssrcongr | [ "congr" ssrcongrarg(arg) ] -> [ let ctx, (arg, dgens) = arg in let ist = get_ltacctx ctx in match dgens with | [gens], clr -> tclTHEN (genstac (gens,clr) ist) (newssrcongrtac arg ist) | _ -> errorstrm (str"Dependent family abstractions not allowed in congr")] END (** 7. Rewriting tactics (rewrite, unlock) *) (** Coq rewrite compatibility flag *) let ssr_strict_match = ref false let _ = Goptions.declare_bool_option { Goptions.optsync = true; Goptions.optname = "strict redex matching"; Goptions.optkey = ["Match"; "Strict"]; Goptions.optread = (fun () -> !ssr_strict_match); Goptions.optdepr = false; Goptions.optwrite = (fun b -> ssr_strict_match := b) } (** Rewrite multiplier *) type ssrmult = int * ssrmmod let notimes = 0 let nomult = 1, Once let pr_mult (n, m) = if n > 0 && m <> Once then pr_int n ++ pr_mmod m else pr_mmod m let pr_ssrmult _ _ _ = pr_mult ARGUMENT EXTEND ssrmult_ne TYPED AS int * ssrmmod PRINTED BY pr_ssrmult | [ natural(n) ssrmmod(m) ] -> [ check_index loc n, m ] | [ ssrmmod(m) ] -> [ notimes, m ] END ARGUMENT EXTEND ssrmult TYPED AS ssrmult_ne PRINTED BY pr_ssrmult | [ ssrmult_ne(m) ] -> [ m ] | [ ] -> [ nomult ] END (** Rewrite clear/occ switches *) let pr_rwocc = function | None, None -> mt () | None, occ -> pr_occ occ | Some clr, _ -> pr_clear_ne clr let pr_ssrrwocc _ _ _ = pr_rwocc ARGUMENT EXTEND ssrrwocc TYPED AS ssrdocc PRINTED BY pr_ssrrwocc | [ "{" ssrhyp_list(clr) "}" ] -> [ mkclr clr ] | [ "{" ssrocc(occ) "}" ] -> [ mkocc occ ] | [ ] -> [ noclr ] END (** Rewrite rules *) type ssrwkind = RWred of ssrsimpl | RWdef | RWeq (* type ssrrule = ssrwkind * ssrterm *) let pr_rwkind = function | RWred s -> pr_simpl s | RWdef -> str "/" | RWeq -> mt () let wit_ssrrwkind, globwit_ssrrwkind, rawwit_ssrrwkind = add_genarg "ssrrwkind" pr_rwkind let pr_rule = function | RWred s, _ -> pr_simpl s | RWdef, r-> str "/" ++ pr_term r | RWeq, r -> pr_term r let pr_ssrrule _ _ _ = pr_rule let noruleterm loc = mk_term ' ' (mkCProp loc) ARGUMENT EXTEND ssrrule_ne TYPED AS ssrrwkind * ssrterm PRINTED BY pr_ssrrule | [ ssrsimpl_ne(s) ] -> [ RWred s, noruleterm loc ] | [ "/" ssrterm(t) ] -> [ RWdef, t ] | [ ssrterm(t) ] -> [ RWeq, t ] END ARGUMENT EXTEND ssrrule TYPED AS ssrrule_ne PRINTED BY pr_ssrrule | [ ssrrule_ne(r) ] -> [ r ] | [ ] -> [ RWred Nop, noruleterm loc ] END (** Rewrite arguments *) (* type ssrrwarg = (ssrdir * ssrmult) * ((ssrdocc * ssrpattern) * ssrrule) *) let pr_option f = function None -> mt() | Some x -> f x let pr_pattern_squarep= pr_option (fun r -> str "[" ++ pr_rpattern r ++ str "]") let pr_ssrpattern_squarep _ _ _ = pr_pattern_squarep let pr_rwarg ((d, m), ((docc, rx), r)) = pr_rwdir d ++ pr_mult m ++ pr_rwocc docc ++ pr_pattern_squarep rx ++ pr_rule r let pr_ssrrwarg _ _ _ = pr_rwarg let mk_rwarg (d, (n, _ as m)) ((clr, occ as docc), rx) (rt, _ as r) = if rt <> RWeq then begin if rt = RWred Nop && not (m = nomult && occ = None && rx = None) && (clr = None || clr = Some []) then anomaly "Improper rewrite clear switch"; if d = R2L && rt <> RWdef then error "Right-to-left switch on simplification"; if n <> 1 && rt = RWred Cut then error "Bad or useless multiplier"; if occ <> None && rx = None && rt <> RWdef then error "Missing redex for simplification occurrence" end; (d, m), ((docc, rx), r) let norwmult = L2R, nomult let norwocc = noclr, None (* let pattern_ident = Prim.pattern_ident in GEXTEND Gram GLOBAL: pattern_ident; pattern_ident: [[c = pattern_ident -> (CRef (Ident (loc,c)), NoBindings)]]; END *) ARGUMENT EXTEND ssrpattern_squarep TYPED AS rpattern option PRINTED BY pr_ssrpattern_squarep | [ "[" rpattern(rdx) "]" ] -> [ Some rdx ] | [ ] -> [ None ] END ARGUMENT EXTEND ssrpattern_ne_squarep TYPED AS rpattern option PRINTED BY pr_ssrpattern_squarep | [ "[" rpattern(rdx) "]" ] -> [ Some rdx ] END ARGUMENT EXTEND ssrrwarg TYPED AS (ssrdir * ssrmult) * ((ssrdocc * rpattern option) * ssrrule) PRINTED BY pr_ssrrwarg | [ "-" ssrmult(m) ssrrwocc(docc) ssrpattern_squarep(rx) ssrrule_ne(r) ] -> [ mk_rwarg (R2L, m) (docc, rx) r ] | [ "-/" ssrterm(t) ] -> (* just in case '-/' should become a token *) [ mk_rwarg (R2L, nomult) norwocc (RWdef, t) ] | [ ssrmult_ne(m) ssrrwocc(docc) ssrpattern_squarep(rx) ssrrule_ne(r) ] -> [ mk_rwarg (L2R, m) (docc, rx) r ] | [ "{" ne_ssrhyp_list(clr) "}" ssrpattern_ne_squarep(rx) ssrrule_ne(r) ] -> [ mk_rwarg norwmult (mkclr clr, rx) r ] | [ "{" ne_ssrhyp_list(clr) "}" ssrrule(r) ] -> [ mk_rwarg norwmult (mkclr clr, None) r ] | [ "{" ssrocc(occ) "}" ssrpattern_squarep(rx) ssrrule_ne(r) ] -> [ mk_rwarg norwmult (mkocc occ, rx) r ] | [ "{" "}" ssrpattern_squarep(rx) ssrrule_ne(r) ] -> [ mk_rwarg norwmult (nodocc, rx) r ] | [ ssrpattern_ne_squarep(rx) ssrrule_ne(r) ] -> [ mk_rwarg norwmult (noclr, rx) r ] | [ ssrrule_ne(r) ] -> [ mk_rwarg norwmult norwocc r ] END let simplintac occ rdx sim gl = let simptac gl = let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in let simp env c _ = red_safe Tacred.simpl env sigma0 c in convert_concl_no_check (eval_pattern env0 sigma0 concl0 rdx occ simp) gl in match sim with | Simpl -> simptac gl | SimplCut -> tclTHEN simptac (tclTRY donetac) gl | _ -> simpltac sim gl let rec get_evalref c = match kind_of_term c with | Var id -> EvalVarRef id | Const k -> EvalConstRef k | App (c', _) -> get_evalref c' | Cast (c', _, _) -> get_evalref c' | _ -> errorstrm (str "The term " ++ pr_constr c ++ str " is not unfoldable") (* Strip a pattern generated by a prenex implicit to its constant. *) let strip_unfold_term ((sigma, t) as p) kt = match kind_of_term t with | App (f, a) when kt = ' ' && array_for_all isEvar a && isConst f -> (sigma, f), true | Const _ | Var _ -> p, true | _ -> p, false let unfoldintac occ rdx t (kt,_) gl = let fs sigma x = Reductionops.nf_evar sigma x in let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in let (sigma, t), const = strip_unfold_term t kt in let body env t c = Tacred.unfoldn [(true, [1]), get_evalref t] env sigma0 c in let easy = occ = None && rdx = None in let red_flags = if easy then Closure.betaiotazeta else Closure.betaiota in let beta env = Reductionops.clos_norm_flags red_flags env sigma0 in let unfold, conclude = match rdx with | Some (_, (In_T _ | In_X_In_T _)) | None -> let ise = create_evar_defs sigma in let ise, u = mk_tpattern env0 sigma0 (ise,t) all_ok L2R t in let find_T, end_T = mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[u]) in (fun env c h -> try find_T env c h (fun env c _ -> body env t c) with NoMatch when easy -> c | NoMatch | NoProgress -> errorstrm (str"No occurrence of " ++ pr_constr_pat t ++ spc() ++ str "in " ++ pr_constr c)), (fun () -> try end_T () with | NoMatch when easy -> fake_pmatcher_end () | NoMatch -> anomaly "unfoldintac") | _ -> (fun env (c as orig_c) h -> if const then let rec aux c = match kind_of_term c with | Const _ when eq_constr c t -> body env t t | App (f,a) when eq_constr f t -> mkApp (body env f f,a) | _ -> let c = Reductionops.whd_betaiotazeta sigma0 c in match kind_of_term c with | Const _ when eq_constr c t -> body env t t | App (f,a) when eq_constr f t -> mkApp (body env f f,a) | Const f -> aux (body env c c) | App (f, a) -> aux (mkApp (body env f f, a)) | _ -> errorstrm (str "The term "++pr_constr orig_c++ str" contains no " ++ pr_constr t ++ str" even after unfolding") in aux c else try body env t (fs (unify_HO env sigma c t) t) with _ -> errorstrm (str "The term " ++ pr_constr c ++spc()++ str "does not unify with " ++ pr_constr_pat t)), fake_pmatcher_end in let concl = try beta env0 (eval_pattern env0 sigma0 concl0 rdx occ unfold) with Option.IsNone -> errorstrm (str"Failed to unfold " ++ pr_constr_pat t) in let _ = conclude () in convert_concl concl gl ;; let foldtac occ rdx ft gl = let fs sigma x = Reductionops.nf_evar sigma x in let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in let sigma, t = ft in let fold, conclude = match rdx with | Some (_, (In_T _ | In_X_In_T _)) | None -> let ise = create_evar_defs sigma in let ut = red_product_skip_id env0 sigma t in let ise, ut = mk_tpattern env0 sigma0 (ise,t) all_ok L2R ut in let find_T, end_T = mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[ut]) in (fun env c h -> try find_T env c h (fun env t _ -> t) with NoMatch -> c), (fun () -> try end_T () with NoMatch -> fake_pmatcher_end ()) | _ -> (fun env c h -> try let sigma = unify_HO env sigma c t in fs sigma t with _ -> errorstrm (str "fold pattern " ++ pr_constr_pat t ++ spc () ++ str "does not match redex " ++ pr_constr_pat c)), fake_pmatcher_end in let concl = eval_pattern env0 sigma0 concl0 rdx occ fold in let _ = conclude () in convert_concl concl gl ;; let converse_dir = function L2R -> R2L | R2L -> L2R let rw_progress rhs lhs ise = not (eq_constr lhs (Evarutil.nf_evar ise rhs)) (* Coq has a more general form of "equation" (any type with a single *) (* constructor with no arguments with_rect_r elimination lemmas). *) (* However there is no clear way of determining the LHS and RHS of *) (* such a generic Leibnitz equation -- short of inspecting the type *) (* of the elimination lemmas. *) let rec strip_prod_assum c = match kind_of_term c with | Prod (_, _, c') -> strip_prod_assum c' | LetIn (_, v, _, c') -> strip_prod_assum (subst1 v c) | Cast (c', _, _) -> strip_prod_assum c' | _ -> c let rule_id = mk_internal_id "rewrite rule" exception PRtype_error exception PRindetermined_rhs of constr let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = let env = pf_env gl in let beta = Reductionops.clos_norm_flags Closure.beta env sigma in let sigma, p = let sigma = create_evar_defs sigma in Evarutil.new_evar sigma env (beta (subst1 new_rdx pred)) in let pred = mkNamedLambda pattern_id rdx_ty pred in let elim = let (kn, i) as ind, unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in let sort = elimination_sort_of_goal gl in let elim = Indrec.lookup_eliminator ind sort in if dir = R2L then elim else (* taken from Coq's rewrite *) let elim = destConst elim in let mp,dp,l = repr_con (constant_of_kn (canonical_con elim)) in let l' = label_of_id (Nameops.add_suffix (id_of_label l) "_r") in let c1' = Global.constant_of_delta_kn (canonical_con (make_con mp dp l')) in mkConst c1' in let proof = mkApp (elim, [| rdx_ty; new_rdx; pred; p; rdx; c |]) in (* We check the proof is well typed *) let proof_ty = try Typing.type_of env sigma proof with _ -> raise PRtype_error in pp(lazy(str"pirrel_rewrite proof term of type: " ++ pr_constr proof_ty)); try refine_with ~first_goes_last:(not !ssroldreworder) ~with_evars:false (sigma, proof) gl with _ -> (* we generate a msg like: "Unable to find an instance for the variable" *) let c = Reductionops.nf_evar sigma c in let hd_ty, miss = match kind_of_term c with | App (hd, args) -> let hd_ty = Retyping.get_type_of env sigma hd in let names = let rec aux t = function 0 -> [] | n -> let t = Reductionops.whd_betadeltaiota env sigma t in match kind_of_type t with | ProdType (name, _, t) -> name :: aux t (n-1) | _ -> assert false in aux hd_ty (Array.length args) in hd_ty, Util.list_map_filter (fun (t, name) -> let evs = Util.Intset.elements (Evarutil.evars_of_term t) in let open_evs = List.filter (fun k -> InProp <> Retyping.get_sort_family_of env sigma (Evd.evar_concl (Evd.find sigma k))) evs in if open_evs <> [] then Some name else None) (List.combine (Array.to_list args) names) | _ -> anomaly "rewrite rule not an application" in errorstrm (Himsg.explain_refiner_error (Logic.UnresolvedBindings miss) ++ (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_constr hd_ty)) ;; let rwcltac cl rdx dir sr gl = let n, r_n,_ = pf_abs_evars gl sr in let r_n' = pf_abs_cterm gl n r_n in let r' = subst_var pattern_id r_n' in let rdxt = Retyping.get_type_of (pf_env gl) (fst sr) rdx in let cvtac, rwtac = if closed0 r' then let env, sigma, c, c_eq = pf_env gl, fst sr, snd sr, build_coq_eq () in let c_ty = Typing.type_of env sigma c in match kind_of_type (Reductionops.whd_betadeltaiota env sigma c_ty) with | AtomicType(e, a) when eq_constr e c_eq -> let new_rdx = if dir = L2R then a.(2) else a.(1) in pirrel_rewrite cl rdx rdxt new_rdx dir sr c_ty, tclIDTAC | _ -> let cl' = mkApp (mkNamedLambda pattern_id rdxt cl, [|rdx|]) in convert_concl cl', rewritetac dir r' else let dc, r2 = decompose_lam_n n r' in let r3, _, r3t = try destCast r2 with _ -> errorstrm (str "no cast from " ++ pr_constr_pat (snd sr) ++ str " to " ++ pr_constr r2) in let cl' = mkNamedProd rule_id (compose_prod dc r3t) (lift 1 cl) in let cl'' = mkNamedProd pattern_id rdxt cl' in let itacs = [introid pattern_id; introid rule_id] in let cltac = clear [pattern_id; rule_id] in let rwtacs = [rewritetac dir (mkVar rule_id); cltac] in (apply_type cl'' [rdx; compose_lam dc r3], tclTHENLIST (itacs @ rwtacs)) in let cvtac' _ = try cvtac gl with | PRtype_error -> if occur_existential (pf_concl gl) then errorstrm (str "Rewriting impacts evars") else errorstrm (str "Dependent type error in rewrite of " ++ pf_pr_constr gl (mkNamedLambda pattern_id rdxt cl)) | Util.UserError _ as e -> raise e | e -> anomaly ("cvtac's exception: " ^ Printexc.to_string e); in tclTHEN cvtac' rwtac gl let prof_rwcltac = mk_profiler "rwrxtac.rwcltac";; let rwcltac cl rdx dir sr gl = prof_rwcltac.profile (rwcltac cl rdx dir sr) gl ;; let lz_coq_prod = let prod = lazy (build_prod ()) in fun () -> Lazy.force prod let lz_setoid_relation = let sdir = ["Classes"; "RelationClasses"] in let last_srel = ref (Environ.empty_env, None) in fun env -> match !last_srel with | env', srel when env' == env -> srel | _ -> let srel = try Some (coq_constant "Class_setoid" sdir "RewriteRelation") with _ -> None in last_srel := (env, srel); srel let ssr_is_setoid env = match lz_setoid_relation env with | None -> fun _ _ _ -> false | Some srel -> fun sigma r args -> Rewrite.is_applied_rewrite_relation env sigma [] (mkApp (r, args)) <> None let prof_rwxrtac_find_rule = mk_profiler "rwrxtac.find_rule";; let closed0_check cl p gl = if closed0 cl then errorstrm (str"No occurrence of redex "++pf_pr_constr gl p) let rwrxtac occ rdx_pat dir rule gl = let env = pf_env gl in let coq_prod = lz_coq_prod () in let is_setoid = ssr_is_setoid env in let r_sigma, rules = let rec loop d sigma r t0 rs red = let t = if red = 1 then Tacred.hnf_constr env sigma t0 else Reductionops.whd_betaiotazeta sigma t0 in match kind_of_term t with | Prod (_, xt, at) -> let ise, x = Evarutil.new_evar (create_evar_defs sigma) env xt in loop d ise (mkApp (r, [|x|])) (subst1 x at) rs 0 | App (pr, a) when pr = coq_prod.Coqlib.typ -> let sr = match kind_of_term (Tacred.hnf_constr env sigma r) with | App (c, ra) when c = coq_prod.Coqlib.intro -> fun i -> ra.(i + 1) | _ -> let ra = Array.append a [|r|] in function 1 -> mkApp (coq_prod.Coqlib.proj1, ra) | _ -> mkApp (coq_prod.Coqlib.proj2, ra) in if a.(0) = build_coq_True () then loop (converse_dir d) sigma (sr 2) a.(1) rs 0 else let sigma2, rs2 = loop d sigma (sr 2) a.(1) rs 0 in loop d sigma2 (sr 1) a.(0) rs2 0 | App (r_eq, a) when Hipattern.match_with_equality_type t != None -> let ind = destInd r_eq and rhs = array_last a in let np, ndep = Inductiveops.inductive_nargs env ind in let ind_ct = Inductiveops.type_of_constructors env ind in let lhs0 = last_arg (strip_prod_assum ind_ct.(0)) in let rdesc = match kind_of_term lhs0 with | Rel i -> let lhs = a.(np - i) in let lhs, rhs = if d = L2R then lhs, rhs else rhs, lhs in (* msgnl (str "RW: " ++ pr_rwdir d ++ str " " ++ pr_constr_pat r ++ str " : " ++ pr_constr_pat lhs ++ str " ~> " ++ pr_constr_pat rhs); *) d, r, lhs, rhs (* let l_i, r_i = if d = L2R then i, 1 - ndep else 1 - ndep, i in let lhs = a.(np - l_i) and rhs = a.(np - r_i) in let a' = Array.copy a in let _ = a'.(np - l_i) <- mkVar pattern_id in let r' = mkCast (r, DEFAULTcast, mkApp (r_eq, a')) in (d, r', lhs, rhs) *) | _ -> let lhs = substl (array_list_of_tl (Array.sub a 0 np)) lhs0 in let lhs, rhs = if d = R2L then lhs, rhs else rhs, lhs in let d' = if Array.length a = 1 then d else converse_dir d in d', r, lhs, rhs in sigma, rdesc :: rs | App (s_eq, a) when is_setoid sigma s_eq a -> let np = Array.length a and i = 3 - dir_org d in let lhs = a.(np - i) and rhs = a.(np + i - 3) in let a' = Array.copy a in let _ = a'.(np - i) <- mkVar pattern_id in let r' = mkCast (r, DEFAULTcast, mkApp (s_eq, a')) in sigma, (d, r', lhs, rhs) :: rs | _ -> if red = 0 then loop d sigma r t rs 1 else errorstrm (str "not a rewritable relation: " ++ pr_constr_pat t ++ spc() ++ str "in rule " ++ pr_constr_pat (snd rule)) in let sigma, r = rule in let t = Retyping.get_type_of env sigma r in loop dir sigma r t [] 0 in let find_rule rdx = let rec rwtac = function | [] -> errorstrm (str "pattern " ++ pr_constr_pat rdx ++ str " does not match " ++ pr_dir_side dir ++ str " of " ++ pr_constr_pat (snd rule)) | (d, r, lhs, rhs) :: rs -> try let ise = unify_HO env (create_evar_defs r_sigma) lhs rdx in if not (rw_progress rhs rdx ise) then raise NoMatch else d, (ise, Reductionops.nf_evar ise r) with _ -> rwtac rs in rwtac rules in let find_rule rdx = prof_rwxrtac_find_rule.profile find_rule rdx in let sigma0, env0, concl0 = project gl, pf_env gl, pf_concl gl in let find_R, conclude = match rdx_pat with | Some (_, (In_T _ | In_X_In_T _)) | None -> let upats_origin = dir, snd rule in let rpat env sigma0 (sigma, pats) (d, r, lhs, rhs) = let sigma, pat = mk_tpattern env sigma0 (sigma,r) (rw_progress rhs) d lhs in sigma, pats @ [pat] in let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in let find_R, end_R = mk_tpattern_matcher sigma0 occ ~upats_origin rpats in find_R ~k:(fun _ _ h -> mkRel h), fun cl -> let rdx,d,r = end_R () in closed0_check cl rdx gl; (d,r),rdx | Some(_, (T e | X_In_T (_,e) | E_As_X_In_T (e,_,_) | E_In_X_In_T (e,_,_))) -> let r = ref None in (fun env c h -> do_once r (fun () -> find_rule c, c); mkRel h), (fun concl -> closed0_check concl e gl; assert_done r) in let concl = eval_pattern env0 sigma0 concl0 rdx_pat occ find_R in let (d, r), rdx = conclude concl in rwcltac concl rdx d r gl ;; let prof_rwxrtac = mk_profiler "rwrxtac";; let rwrxtac occ rdx_pat dir rule gl = prof_rwxrtac.profile (rwrxtac occ rdx_pat dir rule) gl ;; (* Resolve forward reference *) let _ = ipat_rewritetac := fun occ dir c gl -> rwrxtac occ None dir (project gl, c) gl let rwargtac ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl = let fail = ref false in let interp_rpattern ist gl gc = try interp_rpattern ist gl gc with _ when snd mult = May -> fail := true; project gl, T mkProp in let interp gc gl = try interp_term ist gl gc with _ when snd mult = May -> fail := true; (project gl, mkProp) in let rwtac gl = let rx = Option.map (interp_rpattern ist gl) grx in let t = interp gt gl in (match kind with | RWred sim -> simplintac occ rx sim | RWdef -> if dir = R2L then foldtac occ rx t else unfoldintac occ rx t gt | RWeq -> rwrxtac occ rx dir t) gl in let ctac = cleartac (interp_clr (oclr, (fst gt, snd (interp gt gl)))) in if !fail then ctac gl else tclTHEN (tclMULT mult rwtac) ctac gl (** Rewrite argument sequence *) (* type ssrrwargs = ssrrwarg list * ltacctx *) let pr_ssrrwargs _ _ _ (rwargs, _) = pr_list spc pr_rwarg rwargs ARGUMENT EXTEND ssrrwargs TYPED AS ssrrwarg list * ltacctx PRINTED BY pr_ssrrwargs | [ "Qed" ] -> [ anomaly "Grammar placeholder match" ] END let ssr_rw_syntax = ref true let _ = Goptions.declare_bool_option { Goptions.optsync = true; Goptions.optname = "ssreflect rewrite"; Goptions.optkey = ["SsrRewrite"]; Goptions.optread = (fun _ -> !ssr_rw_syntax); Goptions.optdepr = false; Goptions.optwrite = (fun b -> ssr_rw_syntax := b) } let test_ssr_rw_syntax = let test strm = if not !ssr_rw_syntax then raise Stream.Failure else if ssr_loaded () then () else match Compat.get_tok (Util.stream_nth 0 strm) with | Tok.KEYWORD key when List.mem key.[0] ['{'; '['; '/'] -> () | _ -> raise Stream.Failure in Gram.Entry.of_parser "test_ssr_rw_syntax" test GEXTEND Gram GLOBAL: ssrrwargs; ssrrwargs: [[ test_ssr_rw_syntax; a = LIST1 ssrrwarg -> a, rawltacctx ]]; END (** The "rewrite" tactic *) let ssrrewritetac ist rwargs = tclTHENLIST (List.map (rwargtac ist) rwargs) TACTIC EXTEND ssrrewrite | [ "rewrite" ssrrwargs(args) ssrclauses(clauses) ] -> [ let ist = get_ltacctx (snd args) in tclCLAUSES ist (ssrrewritetac ist (fst args)) clauses ] END (** The "unlock" tactic *) let pr_unlockarg (occ, t) = pr_occ occ ++ pr_term t let pr_ssrunlockarg _ _ _ = pr_unlockarg ARGUMENT EXTEND ssrunlockarg TYPED AS ssrocc * ssrterm PRINTED BY pr_ssrunlockarg | [ "{" ssrocc(occ) "}" ssrterm(t) ] -> [ occ, t ] | [ ssrterm(t) ] -> [ None, t ] END let pr_ssrunlockargs _ _ _ (args, _) = pr_list spc pr_unlockarg args ARGUMENT EXTEND ssrunlockargs TYPED AS ssrunlockarg list * ltacctx PRINTED BY pr_ssrunlockargs | [ ssrunlockarg_list(args) ] -> [ args, rawltacctx ] END let unfoldtac occ ko t kt gl = let cl, c = pf_fill_occ_term gl occ (fst (strip_unfold_term t kt)) in let cl' = subst1 (pf_unfoldn [(true, [1]), get_evalref c] gl c) cl in let f = if ko = None then Closure.betaiotazeta else Closure.betaiota in convert_concl (pf_reduce (Reductionops.clos_norm_flags f) gl cl') gl let unlocktac ist args = let utac (occ, gt) gl = unfoldtac occ occ (interp_term ist gl gt) (fst gt) gl in let locked = mkSsrConst "locked" in let key = mkSsrConst "master_key" in let ktacs = [ (fun gl -> unfoldtac None None (project gl,locked) '(' gl); simplest_newcase key ] in tclTHENLIST (List.map utac args @ ktacs) TACTIC EXTEND ssrunlock | [ "unlock" ssrunlockargs(args) ssrclauses(clauses) ] -> [ let ist = get_ltacctx (snd args) in tclCLAUSES ist (unlocktac ist (fst args)) clauses ] END (** 8. Forward chaining tactics (pose, set, have, suffice, wlog) *) (** Defined identifier *) type ssrfwdid = identifier let pr_ssrfwdid _ _ _ id = pr_spc () ++ pr_id id (* We use a primitive parser for the head identifier of forward *) (* tactis to avoid syntactic conflicts with basic Coq tactics. *) ARGUMENT EXTEND ssrfwdid TYPED AS ident PRINTED BY pr_ssrfwdid | [ "Qed" ] -> [ Util.anomaly "Grammar placeholder match" ] END let accept_ssrfwdid strm = match Compat.get_tok (stream_nth 0 strm) with | Tok.IDENT id -> accept_before_syms_or_any_id [":"; ":="; "("] strm | _ -> raise Stream.Failure let test_ssrfwdid = Gram.Entry.of_parser "test_ssrfwdid" accept_ssrfwdid GEXTEND Gram GLOBAL: ssrfwdid; ssrfwdid: [[ test_ssrfwdid; id = Prim.ident -> id ]]; END (** Definition value formatting *) (* We use an intermediate structure to correctly render the binder list *) (* abbreviations. We use a list of hints to extract the binders and *) (* base term from a term, for the two first levels of representation of *) (* of constr terms. *) type 'term ssrbind = | Bvar of name | Bdecl of name list * 'term | Bdef of name * 'term option * 'term | Bstruct of name | Bcast of 'term let pr_binder prl = function | Bvar x -> pr_name x | Bdecl (xs, t) -> str "(" ++ pr_list pr_spc pr_name xs ++ str " : " ++ prl t ++ str ")" | Bdef (x, None, v) -> str "(" ++ pr_name x ++ str " := " ++ prl v ++ str ")" | Bdef (x, Some t, v) -> str "(" ++ pr_name x ++ str " : " ++ prl t ++ str " := " ++ prl v ++ str ")" | Bstruct x -> str "{struct " ++ pr_name x ++ str "}" | Bcast t -> str ": " ++ prl t type 'term ssrbindval = 'term ssrbind list * 'term type ssrbindfmt = | BFvar | BFdecl of int (* #xs *) | BFcast (* final cast *) | BFdef of bool (* has cast? *) | BFrec of bool * bool (* has struct? * has cast? *) let rec mkBstruct i = function | Bvar x :: b -> if i = 0 then [Bstruct x] else mkBstruct (i - 1) b | Bdecl (xs, _) :: b -> let i' = i - List.length xs in if i' < 0 then [Bstruct (List.nth xs i)] else mkBstruct i' b | _ :: b -> mkBstruct i b | [] -> [] let rec format_local_binders h0 bl0 = match h0, bl0 with | BFvar :: h, LocalRawAssum ([_, x], _, _) :: bl -> Bvar x :: format_local_binders h bl | BFdecl _ :: h, LocalRawAssum (lxs, _, t) :: bl -> Bdecl (List.map snd lxs, t) :: format_local_binders h bl | BFdef false :: h, LocalRawDef ((_, x), v) :: bl -> Bdef (x, None, v) :: format_local_binders h bl | BFdef true :: h, LocalRawDef ((_, x), CCast (_, v, CastConv (_, t))) :: bl -> Bdef (x, Some t, v) :: format_local_binders h bl | _ -> [] let rec format_constr_expr h0 c0 = match h0, c0 with | BFvar :: h, CLambdaN (_, [[_, x], _, _], c) -> let bs, c' = format_constr_expr h c in Bvar x :: bs, c' | BFdecl _:: h, CLambdaN (_, [lxs, _, t], c) -> let bs, c' = format_constr_expr h c in Bdecl (List.map snd lxs, t) :: bs, c' | BFdef false :: h, CLetIn(_, (_, x), v, c) -> let bs, c' = format_constr_expr h c in Bdef (x, None, v) :: bs, c' | BFdef true :: h, CLetIn(_, (_, x), CCast (_, v, CastConv (_, t)), c) -> let bs, c' = format_constr_expr h c in Bdef (x, Some t, v) :: bs, c' | [BFcast], CCast (_, c, CastConv (_, t)) -> [Bcast t], c | BFrec (has_str, has_cast) :: h, CFix (_, _, [_, (Some locn, CStructRec), bl, t, c]) -> let bs = format_local_binders h bl in let bstr = if has_str then [Bstruct (Name (snd locn))] else [] in bs @ bstr @ (if has_cast then [Bcast t] else []), c | BFrec (_, has_cast) :: h, CCoFix (_, _, [_, bl, t, c]) -> format_local_binders h bl @ (if has_cast then [Bcast t] else []), c | _, c -> [], c let rec format_glob_decl h0 d0 = match h0, d0 with | BFvar :: h, (x, _, None, _) :: d -> Bvar x :: format_glob_decl h d | BFdecl 1 :: h, (x, _, None, t) :: d -> Bdecl ([x], t) :: format_glob_decl h d | BFdecl n :: h, (x, _, None, t) :: d when n > 1 -> begin match format_glob_decl (BFdecl (n - 1) :: h) d with | Bdecl (xs, _) :: bs -> Bdecl (x :: xs, t) :: bs | bs -> Bdecl ([x], t) :: bs end | BFdef false :: h, (x, _, Some v, _) :: d -> Bdef (x, None, v) :: format_glob_decl h d | BFdef true:: h, (x, _, Some (GCast (_, v, CastConv (_, t))), _) :: d -> Bdef (x, Some t, v) :: format_glob_decl h d | _, (x, _, None, t) :: d -> Bdecl ([x], t) :: format_glob_decl [] d | _, (x, _, Some v, _) :: d -> Bdef (x, None, v) :: format_glob_decl [] d | _, [] -> [] let rec format_glob_constr h0 c0 = match h0, c0 with | BFvar :: h, GLambda (_, x, _, _, c) -> let bs, c' = format_glob_constr h c in Bvar x :: bs, c' | BFdecl 1 :: h, GLambda (_, x, _, t, c) -> let bs, c' = format_glob_constr h c in Bdecl ([x], t) :: bs, c' | BFdecl n :: h, GLambda (_, x, _, t, c) when n > 1 -> begin match format_glob_constr (BFdecl (n - 1) :: h) c with | Bdecl (xs, _) :: bs, c' -> Bdecl (x :: xs, t) :: bs, c' | _ -> [Bdecl ([x], t)], c end | BFdef false :: h, GLetIn(_, x, v, c) -> let bs, c' = format_glob_constr h c in Bdef (x, None, v) :: bs, c' | BFdef true :: h, GLetIn(_, x, GCast (_, v, CastConv (_, t)), c) -> let bs, c' = format_glob_constr h c in Bdef (x, Some t, v) :: bs, c' | [BFcast], GCast (_, c, CastConv(_, t)) -> [Bcast t], c | BFrec (has_str, has_cast) :: h, GRec (_, f, _, bl, t, c) when Array.length c = 1 -> let bs = format_glob_decl h bl.(0) in let bstr = match has_str, f with | true, GFix ([|Some i, GStructRec|], _) -> mkBstruct i bs | _ -> [] in bs @ bstr @ (if has_cast then [Bcast t.(0)] else []), c.(0) | _, c -> [], c (** Forward chaining argument *) (* There are three kinds of forward definitions: *) (* - Hint: type only, cast to Type, may have proof hint. *) (* - Have: type option + value, no space before type *) (* - Pose: binders + value, space before binders. *) type ssrfwdkind = FwdHint of string * bool | FwdHave | FwdPose type ssrfwdfmt = ssrfwdkind * ssrbindfmt list let pr_fwdkind = function | FwdHint (s,_) -> str (s ^ " ") | _ -> str " :=" ++ spc () let pr_fwdfmt (fk, _ : ssrfwdfmt) = pr_fwdkind fk let wit_ssrfwdfmt, globwit_ssrfwdfmt, rawwit_ssrfwdfmt = add_genarg "ssrfwdfmt" pr_fwdfmt (* type ssrfwd = ssrfwdfmt * ssrterm *) let mkFwdVal fk c = ((fk, []), mk_term ' ' c), rawltacctx let mkssrFwdVal fk c = ((fk, []), (c,None)), rawltacctx let mkFwdCast fk loc t c = ((fk, [BFcast]), mk_term ' ' (CCast (loc, c, dC t))), rawltacctx let mkssrFwdCast fk loc t c = ((fk, [BFcast]), (c, Some t)), rawltacctx let mkFwdHint s t = let loc = constr_loc t in mkFwdCast (FwdHint (s,false)) loc t (CHole (loc, None)) let mkFwdHintNoTC s t = let loc = constr_loc t in mkFwdCast (FwdHint (s,true)) loc t (CHole (loc, None)) let pr_gen_fwd prval prc prlc fk (bs, c) = let prc s = str s ++ spc () ++ prval prc prlc c in match fk, bs with | FwdHint (s,_), [Bcast t] -> str s ++ spc () ++ prlc t | FwdHint (s,_), _ -> prc (s ^ "(* typeof *)") | FwdHave, [Bcast t] -> str ":" ++ spc () ++ prlc t ++ prc " :=" | _, [] -> prc " :=" | _, _ -> spc () ++ pr_list spc (pr_binder prlc) bs ++ prc " :=" let pr_fwd_guarded prval prval' = function | ((fk, h), (_, (_, Some c))), _ -> pr_gen_fwd prval pr_constr_expr prl_constr_expr fk (format_constr_expr h c) | ((fk, h), (_, (c, None))), _ -> pr_gen_fwd prval' pr_glob_constr prl_glob_constr fk (format_glob_constr h c) let pr_unguarded prc prlc = prlc let pr_fwd = pr_fwd_guarded pr_unguarded pr_unguarded let pr_ssrfwd _ _ _ = pr_fwd ARGUMENT EXTEND ssrfwd TYPED AS (ssrfwdfmt * ssrterm) * ltacctx PRINTED BY pr_ssrfwd | [ ":=" lconstr(c) ] -> [ mkFwdVal FwdPose c ] | [ ":" lconstr (t) ":=" lconstr(c) ] -> [ mkFwdCast FwdPose loc t c ] END (** Independent parsing for binders *) (* The pose, pose fix, and pose cofix tactics use these internally to *) (* parse argument fragments. *) let pr_ssrbvar prc _ _ v = prc v ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY pr_ssrbvar | [ ident(id) ] -> [ mkCVar loc id ] | [ "_" ] -> [ CHole (loc, None) ] END let bvar_lname = function | CRef (Ident (loc, id)) -> loc, Name id | c -> constr_loc c, Anonymous let pr_ssrbinder prc _ _ (_, c) = prc c ARGUMENT EXTEND ssrbinder TYPED AS ssrfwdfmt * constr PRINTED BY pr_ssrbinder | [ ssrbvar(bv) ] -> [ let xloc, _ as x = bvar_lname bv in (FwdPose, [BFvar]), CLambdaN (loc,[[x],Default Explicit,CHole (xloc,None)],CHole (loc,None)) ] | [ "(" ssrbvar(bv) ")" ] -> [ let xloc, _ as x = bvar_lname bv in (FwdPose, [BFvar]), CLambdaN (loc,[[x],Default Explicit,CHole (xloc,None)],CHole (loc,None)) ] | [ "(" ssrbvar(bv) ":" lconstr(t) ")" ] -> [ let x = bvar_lname bv in (FwdPose, [BFdecl 1]), CLambdaN (loc, [[x], Default Explicit, t], CHole (loc, None)) ] | [ "(" ssrbvar(bv) ne_ssrbvar_list(bvs) ":" lconstr(t) ")" ] -> [ let xs = List.map bvar_lname (bv :: bvs) in let n = List.length xs in (FwdPose, [BFdecl n]), CLambdaN (loc, [xs, Default Explicit, t], CHole (loc, None)) ] | [ "(" ssrbvar(id) ":" lconstr(t) ":=" lconstr(v) ")" ] -> [ let loc' = Util.join_loc (constr_loc t) (constr_loc v) in let v' = CCast (loc', v, dC t) in (FwdPose,[BFdef true]), CLetIn (loc,bvar_lname id, v',CHole (loc,None)) ] | [ "(" ssrbvar(id) ":=" lconstr(v) ")" ] -> [ (FwdPose,[BFdef false]), CLetIn (loc,bvar_lname id, v,CHole (loc,None)) ] END GEXTEND Gram GLOBAL: ssrbinder; ssrbinder: [ [ ["of" | "&"]; c = operconstr LEVEL "99" -> (FwdPose, [BFvar]), CLambdaN (loc,[[loc,Anonymous],Default Explicit,c],CHole (loc,None)) ] ]; END let rec binders_fmts = function | ((_, h), _) :: bs -> h @ binders_fmts bs | _ -> [] let push_binders c2 bs = let loc2 = constr_loc c2 in let mkloc loc1 = Util.join_loc loc1 loc2 in let rec loop ty c = function | (_, CLambdaN (loc1, b, _)) :: bs when ty -> CProdN (mkloc loc1, b, loop ty c bs) | (_, CLambdaN (loc1, b, _)) :: bs -> CLambdaN (mkloc loc1, b, loop ty c bs) | (_, CLetIn (loc1, x, v, _)) :: bs -> CLetIn (mkloc loc1, x, v, loop ty c bs) | [] -> c | _ -> anomaly "binder not a lambda nor a let in" in match c2 with | CCast (x, ct, CastConv (y, cty)) -> (CCast (x, loop false ct bs, CastConv (y, loop true cty bs))) | ct -> loop false ct bs let rec fix_binders = function | (_, CLambdaN (_, [xs, _, t], _)) :: bs -> LocalRawAssum (xs, Default Explicit, t) :: fix_binders bs | (_, CLetIn (_, x, v, _)) :: bs -> LocalRawDef (x, v) :: fix_binders bs | _ -> [] let pr_ssrstruct _ _ _ = function | Some id -> str "{struct " ++ pr_id id ++ str "}" | None -> mt () ARGUMENT EXTEND ssrstruct TYPED AS ident option PRINTED BY pr_ssrstruct | [ "{" "struct" ident(id) "}" ] -> [ Some id ] | [ ] -> [ None ] END (** The "pose" tactic *) (* The plain pose form. *) let bind_fwd bs = function | ((fk, h), (ck, (rc, Some c))), ctx -> ((fk,binders_fmts bs @ h), (ck,(rc,Some (push_binders c bs)))), ctx | fwd -> fwd ARGUMENT EXTEND ssrposefwd TYPED AS ssrfwd PRINTED BY pr_ssrfwd | [ ssrbinder_list(bs) ssrfwd(fwd) ] -> [ bind_fwd bs fwd ] END (* The pose fix form. *) let pr_ssrfixfwd _ _ _ (id, fwd) = str " fix " ++ pr_id id ++ pr_fwd fwd let bvar_locid = function | CRef (Ident (loc, id)) -> loc, id | _ -> Util.error "Missing identifier after \"(co)fix\"" ARGUMENT EXTEND ssrfixfwd TYPED AS ident * ssrfwd PRINTED BY pr_ssrfixfwd | [ "fix" ssrbvar(bv) ssrbinder_list(bs) ssrstruct(sid) ssrfwd(fwd) ] -> [ let (_, id) as lid = bvar_locid bv in let ((fk, h), (ck, (rc, oc))), ctx = fwd in let c = Option.get oc in let has_cast, t', c' = match format_constr_expr h c with | [Bcast t'], c' -> true, t', c' | _ -> false, CHole (constr_loc c, None), c in let lb = fix_binders bs in let has_struct, i = let rec loop = function (l', Name id') :: _ when sid = Some id' -> true, (l', id') | [l', Name id'] when sid = None -> false, (l', id') | _ :: bn -> loop bn | [] -> Util.error "Bad structural argument" in loop (names_of_local_assums lb) in let h' = BFrec (has_struct, has_cast) :: binders_fmts bs in let fix = CFix (loc, lid, [lid, (Some i, CStructRec), lb, t', c']) in id, (((fk, h'), (ck, (rc, Some fix))), ctx) ] END (* The pose cofix form. *) let pr_ssrcofixfwd _ _ _ (id, fwd) = str " cofix " ++ pr_id id ++ pr_fwd fwd ARGUMENT EXTEND ssrcofixfwd TYPED AS ssrfixfwd PRINTED BY pr_ssrcofixfwd | [ "cofix" ssrbvar(bv) ssrbinder_list(bs) ssrfwd(fwd) ] -> [ let _, id as lid = bvar_locid bv in let ((fk, h), (ck, (rc, oc))), ctx = fwd in let c = Option.get oc in let has_cast, t', c' = match format_constr_expr h c with | [Bcast t'], c' -> true, t', c' | _ -> false, CHole (constr_loc c, None), c in let h' = BFrec (false, has_cast) :: binders_fmts bs in let cofix = CCoFix (loc, lid, [lid, fix_binders bs, t', c']) in id, (((fk, h'), (ck, (rc, Some cofix))), ctx) ] END let ssrposetac (id, ((_, t), ctx)) gl = posetac id (snd(pf_abs_ssrterm (get_ltacctx ctx) gl t)) gl let prof_ssrposetac = mk_profiler "ssrposetac";; let ssrposetac arg gl = prof_ssrposetac.profile (ssrposetac arg) gl;; TACTIC EXTEND ssrpose | [ "pose" ssrfixfwd(ffwd) ] -> [ ssrposetac ffwd ] | [ "pose" ssrcofixfwd(ffwd) ] -> [ ssrposetac ffwd ] | [ "pose" ssrfwdid(id) ssrposefwd(fwd) ] -> [ ssrposetac (id, fwd) ] END (** The "set" tactic *) (* type ssrsetfwd = ssrfwd * ssrdocc *) let guard_setrhs s i = s.[i] = '{' let pr_setrhs occ prc prlc c = if occ = nodocc then pr_guarded guard_setrhs prlc c else pr_docc occ ++ prc c let pr_fwd_guarded prval prval' = function | ((fk, h), (_, (_, Some c))), _ -> pr_gen_fwd prval pr_constr_expr prl_constr_expr fk (format_constr_expr h c) | ((fk, h), (_, (c, None))), _ -> pr_gen_fwd prval' pr_glob_constr prl_glob_constr fk (format_glob_constr h c) (* This does not print the type, it should be fixed... *) let pr_ssrsetfwd _ _ _ ((((fk,_),(t,_)),ctx), docc) = pr_gen_fwd (fun _ _ -> pr_cpattern) (fun _ -> mt()) (fun _ -> mt()) fk ([Bcast ()],t) ARGUMENT EXTEND ssrsetfwd TYPED AS ((ssrfwdfmt * (lcpattern * ssrterm option)) * ltacctx) * ssrdocc PRINTED BY pr_ssrsetfwd | [ ":" lconstr(t) ":=" "{" ssrocc(occ) "}" cpattern(c) ] -> [ mkssrFwdCast FwdPose loc (mk_lterm t) c, mkocc occ ] | [ ":" lconstr(t) ":=" lcpattern(c) ] -> [ mkssrFwdCast FwdPose loc (mk_lterm t) c, nodocc ] | [ ":=" "{" ssrocc(occ) "}" cpattern(c) ] -> [ mkssrFwdVal FwdPose c, mkocc occ ] | [ ":=" lcpattern(c) ] -> [ mkssrFwdVal FwdPose c, nodocc ] END let ssrsettac ist id (((_, (pat, pty)), _), (_, occ)) gl = let pat = interp_cpattern ist gl pat (Option.map snd pty) in let cl, sigma, env = pf_concl gl, project gl, pf_env gl in let c, cl = try fill_occ_pattern ~raise_NoMatch:true env sigma cl pat occ 1 with NoMatch -> redex_of_pattern ~resolve_typeclasses:true env pat, cl in if occur_existential c then errorstrm(str"The pattern"++spc()++ pr_constr_pat c++spc()++str"did not match and has holes."++spc()++ str"Did you mean pose?") else let c, cty = match kind_of_term c with | Cast(t, DEFAULTcast, ty) -> t, ty | _ -> c, pf_type_of gl c in let cl' = mkLetIn (Name id, c, cty, cl) in tclTHEN (convert_concl cl') (introid id) gl TACTIC EXTEND ssrset | [ "set" ssrfwdid(id) ssrsetfwd(fwd) ssrclauses(clauses) ] -> [ let (_, ctx), _ = fwd in let ist = get_ltacctx ctx in tclCLAUSES ist (ssrsettac ist id fwd) clauses ] END (** The "have" tactic *) (* type ssrhavefwd = ssrfwd * ssrhint *) let pr_ssrhavefwd _ _ prt (fwd, hint) = pr_fwd fwd ++ pr_hint prt hint ARGUMENT EXTEND ssrhavefwd TYPED AS ssrfwd * ssrhint PRINTED BY pr_ssrhavefwd | [ ":" lconstr(t) ssrhint(hint) ] -> [ mkFwdHint ":" t, hint ] | [ ":" lconstr(t) ":=" lconstr(c) ] -> [ mkFwdCast FwdHave loc t c, nohint ] | [ ":" lconstr(t) ":=" ] -> [ mkFwdHintNoTC ":" t, nohint ] | [ ":=" lconstr(c) ] -> [ mkFwdVal FwdHave c, nohint ] END let intro_id_to_binder = List.map (function | IpatId id -> let xloc, _ as x = bvar_lname (mkCVar dummy_loc id) in (FwdPose, [BFvar]), CLambdaN (dummy_loc, [[x], Default Explicit, CHole (xloc, None)], CHole (dummy_loc, None)) | _ -> anomaly "non-id accepted as binder") let binder_to_intro_id = List.map (function | (FwdPose, [BFvar]), CLambdaN (_,[ids,_,_],_) | (FwdPose, [BFdecl _]), CLambdaN (_,[ids,_,_],_) -> List.map (function (_, Name id) -> IpatId id | _ -> IpatAnon) ids | (FwdPose, [BFdef _]), CLetIn (_,(_,Name id),_,_) -> [IpatId id] | (FwdPose, [BFdef _]), CLetIn (_,(_,Anonymous),_,_) -> [IpatAnon] | _ -> anomaly "ssrbinder is not a binder") let pr_ssrhavefwdwbinders _ _ prt (tr,(hpats, (fwd, hint))) = pr_hpats hpats ++ pr_fwd fwd ++ pr_hint prt hint ARGUMENT EXTEND ssrhavefwdwbinders TYPED AS bool * (ssrhpats * (ssrfwd * ssrhint)) PRINTED BY pr_ssrhavefwdwbinders | [ ssrhpats_wtransp(trpats) ssrbinder_list(bs) ssrhavefwd(fwd) ] -> [ let tr, pats = trpats in let ((clr, pats), binders), simpl = pats in let allbs = intro_id_to_binder binders @ bs in let allbinders = binders @ List.flatten (binder_to_intro_id bs) in let hint = bind_fwd allbs (fst fwd), snd fwd in tr, ((((clr, pats), allbinders), simpl), hint) ] END (* Tactic. *) let examine_abstract id gl = let tid = pf_type_of gl id in let abstract = mkSsrConst "abstract" in if not (isApp tid) || not (eq_constr (fst(destApp tid)) abstract) then errorstrm(strbrk"not an abstract constant: "++pr_constr id); let _, args_id = destApp tid in if Array.length args_id <> 3 then errorstrm(strbrk"not a proper abstract constant: "++pr_constr id); if not (isEvar args_id.(2)) then errorstrm(strbrk"abstract constant "++pr_constr id++str" already used"); args_id let pf_find_abstract_proof check_lock gl abstract_n = let fire gl t = Reductionops.nf_evar (project gl) t in let abstract = mkSsrConst "abstract" in let l = Evd.fold_undefined (fun e ei l -> match kind_of_term ei.Evd.evar_concl with | App(hd, [|ty; n; lock|]) when (not check_lock || (occur_existential (fire gl ty) && isEvar (fire gl lock))) && eq_constr hd abstract && eq_constr n abstract_n -> e::l | _ -> l) (project gl) [] in match l with | [e] -> e | _ -> errorstrm(strbrk"abstract constant "++pr_constr abstract_n++ strbrk" not found in the evar map exactly once. "++ strbrk"Did you tamper with it?") let unfold cl = let module R = Reductionops in let module F = Closure.RedFlags in reduct_in_concl (R.clos_norm_flags (F.mkflags (List.map (fun c -> F.fCONST (destConst c)) cl @ [F.fBETA; F.fIOTA]))) let havegentac ist t gl = let _, c = pf_abs_ssrterm ist gl t in apply_type (mkArrow (pf_type_of gl c) (pf_concl gl)) [c] gl let havetac (transp,((((clr, pats), binders), simpl), ((((fk, _), t), ctx), hint))) suff namefst gl = let ist, concl = get_ltacctx ctx, pf_concl gl in let skols, pats = List.partition (function IpatNewHidden _ -> true | _ -> false) pats in let itac_mkabs = introstac ~ist skols in let itac_c = introstac ~ist (IpatSimpl(clr,Nop) :: pats) in let itac, id, clr = introstac ~ist pats, tclIDTAC, cleartac clr in let binderstac n = let rec aux = function 0 -> [] | n -> IpatAnon :: aux (n-1) in tclTHEN (if binders <> [] then introstac ~ist (aux n) else tclIDTAC) (introstac ~ist binders) in let simpltac = introstac ~ist simpl in let fixtc = not !ssrhaveNOtcresolution && match fk with FwdHint(_,true) -> false | _ -> true in let hint = hinttac ist true hint in let cuttac t gl = if transp then (* The v8.4 refiner is too stupid to deal with a let-in, apparently. * Let's do things by hand... *) let concl = pf_concl gl in let gl, extra = pf_new_evar gl t in let gl, kont = pf_new_evar gl (mkLetIn (Anonymous, extra, t, concl)) in let step = mkApp (mkSsrConst "ssr_have_let", [|concl; t; extra; kont|]) in pf_partial_solution gl step [extra; kont] else basecuttac "ssr_have" t gl in (* Introduce now abstract constants, so that everything sees them *) let abstract_key = mkSsrConst "abstract_key" in let unlock_abs args_id gl = pf_unify_HO gl args_id.(2) abstract_key in tclTHENFIRST itac_mkabs (fun gl -> let mkt t = mk_term ' ' t in let mkl t = (' ', (t, None)) in let interp gl rtc t = pf_abs_ssrterm ~resolve_typeclasses:rtc ist gl t in let interp_ty gl rtc t = let a,b,_ = pf_interp_ty ~resolve_typeclasses:rtc ist gl t in a, b in let ct, cty, hole, loc = match t with | _, (_, Some (CCast (loc, ct, CastConv (_, cty)))) -> mkt ct, mkt cty, mkt (mkCHole dummy_loc), loc | _, (_, Some ct) -> mkt ct, mkt (mkCHole dummy_loc), mkt (mkCHole dummy_loc), dummy_loc | _, (GCast (loc, ct, CastConv (_, cty)), None) -> mkl ct, mkl cty, mkl mkRHole, loc | _, (t, None) -> mkl t, mkl mkRHole, mkl mkRHole, dummy_loc in let gl, cut, sol, itac1, itac2 = match fk, namefst, suff with | FwdHave, true, true -> errorstrm (str"Suff have does not accept a proof term") | FwdHave, false, true -> let cty = combineCG cty hole (mkCArrow loc) mkRArrow in let _, t = interp gl false (combineCG ct cty (mkCCast loc) mkRCast) in let ty = pf_type_of gl t in let ctx, _ = decompose_prod_n 1 ty in let assert_is_conv gl = try convert_concl (compose_prod ctx concl) gl with _ -> errorstrm (str "Given proof term is not of type " ++ pr_constr (mkArrow (mkVar (id_of_string "_")) concl)) in gl, ty, tclTHEN assert_is_conv (apply t), id, itac_c | FwdHave, false, false -> let skols = List.flatten (List.map (function | IpatNewHidden ids -> ids | _ -> assert false) skols) in let skols_args = List.map (fun id -> examine_abstract (mkVar id) gl) skols in let gl = List.fold_right unlock_abs skols_args gl in let sigma, t = interp gl false (combineCG ct cty (mkCCast loc) mkRCast) in let gl = re_sig (sig_it gl) sigma in let gs = List.map (fun a -> pf_find_abstract_proof false gl a.(1)) skols_args in let tacopen_skols gl = let stuff, g = Refiner.unpackage gl in Refiner.repackage stuff ((List.map Goal.build gs) @ [g]) in gl, pf_type_of gl t, apply t, id, tclTHEN (tclTHEN itac_c simpltac) (tclTHEN tacopen_skols (unfold [mkSsrConst "abstract";abstract_key])) | _,true,true -> gl, mkArrow (snd (interp_ty gl fixtc cty)) concl, hint, itac, clr | _,false,true -> gl, mkArrow (snd (interp_ty gl fixtc cty)) concl, hint, id, itac_c | _, false, false -> let n, cty = interp_ty gl fixtc cty in gl, cty, tclTHEN (binderstac n) hint, id, tclTHEN itac_c simpltac | _, true, false -> assert false in tclTHENS (cuttac cut) [ tclTHEN sol itac1; itac2 ] gl) gl ;; (* to extend the abstract value one needs: Utility lemma to partially instantiate an abstract constant type. Lemma use_abstract T n l (x : abstract T n l) : T. Proof. by case: l x. Qed. *) let ssrabstract ctx gens (*last*) gl = let ist = get_ltacctx ctx in let main _ (_,cid) ist gl = (* let proj1, proj2, prod = let pdata = build_prod () in pdata.Coqlib.proj1, pdata.Coqlib.proj2, pdata.Coqlib.typ in *) let concl, env = pf_concl gl, pf_env gl in let fire gl t = Reductionops.nf_evar (project gl) t in let abstract = mkSsrConst "abstract" in let abstract_key = mkSsrConst "abstract_key" in let cid_interpreted = interp_cpattern ist gl cid None in let id = mkVar (Option.get (id_of_pattern cid_interpreted)) in let args_id = examine_abstract id gl in let abstract_n = args_id.(1) in let abstract_proof = pf_find_abstract_proof true gl abstract_n in let gl, proof = let pf_unify_HO gl a b = try pf_unify_HO gl a b with _ -> errorstrm(strbrk"The abstract variable "++pr_constr id++ strbrk" cannot abstract this goal. Did you generalize it?") in let rec find_hole p t = match kind_of_term t with | Evar _ (*when last*) -> pf_unify_HO gl concl t, p (* | Evar _ -> let sigma, it = project gl, sig_it gl in let sigma, ty = Evarutil.new_type_evar sigma env in let gl = re_sig it sigma in let p = mkApp (proj2,[|ty;concl;p|]) in let concl = mkApp(prod,[|ty; concl|]) in pf_unify_HO gl concl t, p | App(hd, [|left; right|]) when eq_constr hd prod -> find_hole (mkApp (proj1,[|left;right;p|])) left *) | _ -> errorstrm(strbrk"abstract constant "++pr_constr abstract_n++ strbrk" has an unexpected shape. Did you tamper with it?") in find_hole ((*if last then*) id (*else mkApp(mkSsrConst "use_abstract",Array.append args_id [|id|])*)) (fire gl args_id.(0)) in let gl = (*if last then*) pf_unify_HO gl abstract_key args_id.(2) (*else gl*) in let proof = fire gl proof in (* if last then *) let tacopen gl = let stuff, g = Refiner.unpackage gl in Refiner.repackage stuff [ g; Goal.build abstract_proof ] in tclTHENS tacopen [tclSOLVE [apply proof];unfold[abstract;abstract_key]] gl (* else apply proof gl *) in let introback ist (gens, _) = introstac ~ist (List.map (fun (_,cp) -> match id_of_pattern (interp_cpattern ist gl cp None) with | None -> IpatAnon | Some id -> IpatId id) (List.tl (List.hd gens))) in tclTHEN (with_dgens gens main ist) (introback ist gens) gl (* The standard TACTIC EXTEND does not work for abstract *) GEXTEND Gram GLOBAL: tactic_expr; tactic_expr: LEVEL "3" [ RIGHTA [ IDENT "abstract"; gens = ssrdgens; ctx = ltacctx -> Tacexpr.TacAtom(loc,Tacexpr.TacExtend (loc, "ssrabstract", [Genarg.in_gen rawwit_ssrdgens gens; Genarg.in_gen rawwit_ltacctx ctx])) ]]; END TACTIC EXTEND ssrabstract | [ "abstract" ssrdgens(gens) ltacctx(ctx) ] -> [ if List.length (fst gens) <> 1 then errorstrm (str"dependents switches '/' not allowed here"); ssrabstract ctx gens ] END let prof_havetac = mk_profiler "havetac";; let havetac arg a b gl = prof_havetac.profile (havetac arg a b) gl;; TACTIC EXTEND ssrhave | [ "have" ssrhavefwdwbinders(fwd) ] -> [ havetac fwd false false ] END TACTIC EXTEND ssrhavesuff | [ "have" "suff" ssrhpats_nobs(pats) ssrhavefwd(fwd) ] -> [ havetac (false,(pats,fwd)) true false ] END TACTIC EXTEND ssrhavesuffices | [ "have" "suffices" ssrhpats_nobs(pats) ssrhavefwd(fwd) ] -> [ havetac (false,(pats,fwd)) true false ] END TACTIC EXTEND ssrsuffhave | [ "suff" "have" ssrhpats_nobs(pats) ssrhavefwd(fwd) ] -> [ havetac (false,(pats,fwd)) true true ] END TACTIC EXTEND ssrsufficeshave | [ "suffices" "have" ssrhpats_nobs(pats) ssrhavefwd(fwd) ] -> [ havetac (false,(pats,fwd)) true true ] END (** The "suffice" tactic *) let pr_ssrsufffwdwbinders _ _ prt (hpats, (fwd, hint)) = pr_hpats hpats ++ pr_fwd fwd ++ pr_hint prt hint ARGUMENT EXTEND ssrsufffwd TYPED AS ssrhpats * (ssrfwd * ssrhint) PRINTED BY pr_ssrsufffwdwbinders | [ ssrhpats(pats) ssrbinder_list(bs) ":" lconstr(t) ssrhint(hint) ] -> [ let ((clr, pats), binders), simpl = pats in let allbs = intro_id_to_binder binders @ bs in let allbinders = binders @ List.flatten (binder_to_intro_id bs) in let fwd = mkFwdHint ":" t in (((clr, pats), allbinders), simpl), (bind_fwd allbs fwd, hint) ] END let sufftac ((((clr, pats),binders),simpl), (((_, c), ctx), hint)) = let ist = get_ltacctx ctx in let htac = tclTHEN (introstac ~ist pats) (hinttac ist true hint) in let c = match c with | (a, (b, Some (CCast (_, _, CastConv (_, cty))))) -> a, (b, Some cty) | (a, (GCast (_, _, CastConv (_, cty)), None)) -> a, (cty, None) | _ -> anomaly "suff: ssr cast hole deleted by typecheck" in let ctac gl = basecuttac "ssr_suff" (pi2 (pf_interp_ty ist gl c)) gl in tclTHENS ctac [htac; tclTHEN (cleartac clr) (introstac ~ist (binders@simpl))] TACTIC EXTEND ssrsuff | [ "suff" ssrsufffwd(fwd) ] -> [ sufftac fwd ] END TACTIC EXTEND ssrsuffices | [ "suffices" ssrsufffwd(fwd) ] -> [ sufftac fwd ] END (** The "wlog" (Without Loss Of Generality) tactic *) (* type ssrwlogfwd = ssrwgen list * ssrfwd *) let pr_ssrwlogfwd _ _ _ (gens, t) = str ":" ++ pr_list mt pr_wgen gens ++ spc() ++ pr_fwd t ARGUMENT EXTEND ssrwlogfwd TYPED AS ssrwgen list * ssrfwd PRINTED BY pr_ssrwlogfwd | [ ":" ssrwgen_list(gens) "/" lconstr(t) ] -> [ gens, mkFwdHint "/" t] END let destProd_or_LetIn c = match kind_of_term c with | Prod (n,ty,c) -> (n,None,ty), c | LetIn (n,bo,ty,c) -> (n,Some bo,ty), c | _ -> raise (Invalid_argument "destProd_or_LetIn") let wlogtac (((clr0, pats),_),_) (gens, ((_, ct), ctx)) hint suff ghave gl = let ist = get_ltacctx ctx in let mkabs gen = abs_wgen false ist gl (fun x -> x) gen in let mkclr gen clrs = clr_of_wgen gen clrs in let mkpats = function | _, Some ((x, _), _) -> fun pats -> IpatId (hoi_id x) :: pats | _ -> fun x -> x in let ct = match ct with | (a, (b, Some (CCast (_, _, CastConv (_, cty))))) -> a, (b, Some cty) | (a, (GCast (_, _, CastConv (_, cty)), None)) -> a, (cty, None) | _ -> anomaly "wlog: ssr cast hole deleted by typecheck" in let cut_implies_goal = not (suff || ghave <> `NoGen) in let c, args, ct = let gens = List.filter (function _, Some _ -> true | _ -> false) gens in let concl = pf_concl gl in let c = mkProp in let c = if cut_implies_goal then mkArrow c concl else c in let args, c = List.fold_right mkabs gens ([],c) in let env, _ = List.fold_left (fun (env, c) _ -> let rd, c = destProd_or_LetIn c in Environ.push_rel rd env, c) (pf_env gl, c) gens in let sigma, ev = Evarutil.new_evar (project gl) env Term.mkProp in let k, _ = Term.destEvar ev in let fake_gl = { Evd.it = Goal.build k; Evd.sigma = sigma } in let _, ct, _ = pf_interp_ty ist fake_gl ct in let rec subst c g s = match kind_of_term c, g with | Prod(Anonymous,_,c), [] -> mkProd(Anonymous, subst_vars s ct, c) | Sort _, [] -> subst_vars s ct | LetIn(Name id as n,b,ty,c), _::g -> mkLetIn (n,b,ty,subst c g (id::s)) | Prod(Name id as n,ty,c), _::g -> mkProd (n,ty,subst c g (id::s)) | _ -> anomaly "SSR: wlog: subst" in let c = subst c gens [] in let rec pired c = function | [] -> c | t::ts as args -> match kind_of_term c with | Prod(_,_,c) -> pired (subst1 t c) ts | LetIn(id,b,ty,c) -> mkLetIn (id,b,ty,pired c args) | _ -> anomaly "SSR: wlog: pired" in c, args, pired c args in let tacipat pats = introstac ~ist pats in let tacigens = tclTHEN (tclTHENLIST(List.rev(List.fold_right mkclr gens [cleartac clr0]))) (introstac ~ist (List.fold_right mkpats gens [])) in let hinttac = hinttac ist true hint in let cut_kind, fst_goal_tac, snd_goal_tac = match suff, ghave with | true, `NoGen -> "ssr_wlog", tclTHEN hinttac (tacipat pats), tacigens | false, `NoGen -> "ssr_wlog", hinttac, tclTHEN tacigens (tacipat pats) | true, `Gen _ -> assert false | false, `Gen id -> if gens = [] then errorstrm(str"gen have requires some generalizations"); let clear0 = cleartac clr0 in let id, name_general_hyp, cleanup, pats = match id, pats with | None, (IpatId id as ip)::pats -> Some id, tacipat [ip], clear0, pats | None, _ -> None, tclIDTAC, clear0, pats | Some (Some id),_ -> Some id, introid id, clear0, pats | Some _,_ -> let id = mk_anon_id "tmp" gl in Some id, introid id, tclTHEN clear0 (clear [id]), pats in let tac_specialize = match id with | None -> tclIDTAC | Some id -> if pats = [] then tclIDTAC else let args = Array.of_list args in pp(lazy(str"specialized="++pr_constr (mkApp (mkVar id,args)))); pp(lazy(str"specialized_ty="++pr_constr ct)); tclTHENS (basecuttac "ssr_have" ct) [apply (mkApp (mkVar id,args)); tclIDTAC] in "ssr_have", (if hint = nohint then tacigens else hinttac), tclTHENLIST [name_general_hyp; tac_specialize; tacipat pats; cleanup] in tclTHENS (basecuttac cut_kind c) [fst_goal_tac; snd_goal_tac] gl TACTIC EXTEND ssrwlog | [ "wlog" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] -> [ wlogtac pats fwd hint false `NoGen ] END TACTIC EXTEND ssrwlogs | [ "wlog" "suff" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] -> [ wlogtac pats fwd hint true `NoGen ] END TACTIC EXTEND ssrwlogss | [ "wlog" "suffices" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ]-> [ wlogtac pats fwd hint true `NoGen ] END TACTIC EXTEND ssrwithoutloss | [ "without" "loss" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] -> [ wlogtac pats fwd hint false `NoGen ] END TACTIC EXTEND ssrwithoutlosss | [ "without" "loss" "suff" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] -> [ wlogtac pats fwd hint true `NoGen ] END TACTIC EXTEND ssrwithoutlossss | [ "without" "loss" "suffices" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ]-> [ wlogtac pats fwd hint true `NoGen ] END (* Generally have *) let pr_idcomma _ _ _ = function | None -> mt() | Some None -> str"_, " | Some (Some id) -> pr_id id ++ str", " ARGUMENT EXTEND ssr_idcomma TYPED AS ident option option PRINTED BY pr_idcomma | [ ] -> [ None ] END let accept_idcomma strm = match Compat.get_tok (stream_nth 0 strm) with | Tok.IDENT _ | Tok.KEYWORD "_" -> accept_before_syms [","] strm | _ -> raise Stream.Failure let test_idcomma = Gram.Entry.of_parser "test_idcomma" accept_idcomma GEXTEND Gram GLOBAL: ssr_idcomma; ssr_idcomma: [ [ test_idcomma; ip = [ id = IDENT -> Some (id_of_string id) | "_" -> None ]; "," -> Some ip ] ]; END let augment_preclr clr1 (((clr0, x),y),z) = (((clr1 @ clr0, x),y),z) TACTIC EXTEND ssrgenhave | [ "gen" "have" ssrclear(clr) ssr_idcomma(id) ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] -> [ let pats = augment_preclr clr pats in wlogtac pats fwd hint false (`Gen id) ] END TACTIC EXTEND ssrgenhave2 | [ "generally" "have" ssrclear(clr) ssr_idcomma(id) ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] -> [ let pats = augment_preclr clr pats in wlogtac pats fwd hint false (`Gen id) ] END (** Canonical Structure alias *) GEXTEND Gram GLOBAL: gallina_ext; gallina_ext: (* Canonical structure *) [[ IDENT "Canonical"; qid = Constr.global -> Vernacexpr.VernacCanonical (AN qid) | IDENT "Canonical"; ntn = Prim.by_notation -> Vernacexpr.VernacCanonical (ByNotation ntn) | IDENT "Canonical"; qid = Constr.global; d = G_vernac.def_body -> let s = coerce_reference_to_id qid in Vernacexpr.VernacDefinition ((Decl_kinds.Global,Decl_kinds.CanonicalStructure), (dummy_loc,s),(d ), (fun _ -> Recordops.declare_canonical_structure)) ]]; END (** 9. Keyword compatibility fixes. *) (* Coq v8.1 notation uses "by" and "of" quasi-keywords, i.e., reserved *) (* identifiers used as keywords. This is incompatible with ssreflect.v *) (* which makes "by" and "of" true keywords, because of technicalities *) (* in the internal lexer-parser API of Coq. We patch this here by *) (* adding new parsing rules that recognize the new keywords. *) (* To make matters worse, the Coq grammar for tactics fails to *) (* export the non-terminals we need to patch. Fortunately, the CamlP5 *) (* API provides a backdoor access (with loads of Obj.magic trickery). *) (* Coq v8.3 defines "by" as a keyword, some hacks are not needed any *) (* longer and thus comment out. Such comments are marked with v8.3 *) let tac_ent = List.fold_left Grammar.Entry.find (Obj.magic simple_tactic) in let hypident_ent = tac_ent ["clause_dft_all"; "in_clause"; "hypident_occ"; "hypident"] in let id_or_meta : Obj.t Gram.Entry.e = Obj.magic (Grammar.Entry.find hypident_ent "id_or_meta") in let hypident : (Obj.t * hyp_location_flag) Gram.Entry.e = Obj.magic hypident_ent in GEXTEND Gram GLOBAL: hypident; hypident: [ [ "("; IDENT "type"; "of"; id = id_or_meta; ")" -> id, InHypTypeOnly | "("; IDENT "value"; "of"; id = id_or_meta; ")" -> id, InHypValueOnly ] ]; END GEXTEND Gram GLOBAL: hloc; hloc: [ [ "in"; "("; "Type"; "of"; id = ident; ")" -> HypLocation ((Util.dummy_loc,id), InHypTypeOnly) | "in"; "("; IDENT "Value"; "of"; id = ident; ")" -> HypLocation ((Util.dummy_loc,id), InHypValueOnly) ] ]; END let constr_eval : (Topconstr.constr_expr,Obj.t,Obj.t) Glob_term.may_eval Gram.Entry.e = Obj.magic (Grammar.Entry.find (Obj.magic constr_may_eval) "constr_eval") GEXTEND Gram GLOBAL: constr_eval; constr_eval: [ [ IDENT "type"; "of"; c = Constr.constr -> ConstrTypeOf c ] ]; END (* From *) let join_reference ns r = Libnames.( match ns , r with Qualid (_, q1), Qualid (loc, q2) -> let (dp1,id1) = repr_qualid q1 in let (dp2,id2) = repr_qualid q2 in Qualid (loc, make_qualid (append_dirpath (append_dirpath dp1 (dirpath_of_string (string_of_id id1))) dp2) id2) | Qualid (_, q1), Ident (loc, id2) -> let (dp1,id1) = repr_qualid q1 in Qualid (loc, make_qualid (append_dirpath dp1 (dirpath_of_string (string_of_id id1))) id2) | Ident (_, id1), Qualid (loc, q2) -> let (dp2,id2) = repr_qualid q2 in Qualid (loc, make_qualid (append_dirpath (dirpath_of_string (string_of_id id1)) dp2) id2) | Ident (_, id1), Ident (loc, id2) -> Qualid (loc, make_qualid (dirpath_of_string (string_of_id id1)) id2) ) GEXTEND Gram GLOBAL: gallina_ext; ssr_export_token: [ [ IDENT "Import" -> Some false | IDENT "Export" -> Some true | -> None ] ] ; gallina_ext: [[ IDENT "From"; ns = Constr.global; IDENT "Require"; export = ssr_export_token; qidl = LIST1 Constr.global -> (* let qidl = List.map (join_reference ns) qidl in *) Vernacexpr.VernacRequire (export, None, qidl) ]]; END (* We wipe out all the keywords generated by the grammar rules we defined. *) (* The user is supposed to Require Import ssreflect or Require ssreflect *) (* and Import ssreflect.SsrSyntax to obtain these keywords and as a *) (* consequence the extended ssreflect grammar. *) let () = Lexer.unfreeze frozen_lexer ;; (* vim: set filetype=ocaml foldmethod=marker: *)