|
(************************************************************************)
(* * The Rocq Prover / The Rocq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
{
let defaultCast = Constr.DEFAULTcast
open Names
open Pp
open Procq
open Ltac_plugin
open Stdarg
open Tacarg
open Libnames
open Util
open Locus
open Tacexpr
open Pltac
open Ppconstr
open Namegen
open Tactypes
open Constrexpr
open Constrexpr_ops
open Proofview.Notations
open Ssrmatching_plugin.Ssrmatching
open Ssrprinters
open Ssrcommon
open Ssrequality
open Ssripats
open Libobject
(** Ssreflect load check. *)
(* To allow ssrcoq to be fully compatible with the "plain" Rocq, 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 = Summary.ref ~name:"SSR:loaded" false
let is_ssr_loaded () =
!ssr_loaded ||
(if CLexer.is_keyword (Procq.get_keyword_state()) "SsrSyntax_is_Imported" then ssr_loaded:=true;
!ssr_loaded)
let () = Pptactic.ssr_loaded_hook is_ssr_loaded
}
DECLARE PLUGIN "rocq-runtime.plugins.ssreflect"
{
let ssrtac_name name = {
mltac_plugin = "rocq-runtime.plugins.ssreflect";
mltac_tactic = "ssr" ^ name;
}
let ssrtac_entry name = {
mltac_name = ssrtac_name name;
mltac_index = 0;
}
let cache_tactic_notation (key, body, parule) =
Tacenv.register_alias key body;
Pptactic.declare_notation_tactic_pprule key parule
type tactic_grammar_obj = KerName.t * Tacenv.alias_tactic * Pptactic.pp_tactic
let inSsrGrammar : tactic_grammar_obj -> obj =
declare_object {(default_object "SsrGrammar") with
load_function = (fun _ -> cache_tactic_notation);
cache_function = cache_tactic_notation;
classify_function = (fun x -> Keep)}
let path = MPfile (DirPath.make @@ List.map Id.of_string ["ssreflect"; "ssr"; "Corelib"])
let register_ssrtac name f prods =
let open Pptactic in
Tacenv.register_ml_tactic (ssrtac_name name) [|f|];
let map id = Reference (Locus.ArgVar (CAst.make id)) in
let get_id = function
| TacTerm s -> None
| TacNonTerm (_, (_, ido)) -> ido in
let ids = List.map_filter get_id prods in
let tac = CAst.make (TacML (ssrtac_entry name, List.map map ids)) in
let key = KerName.make path (Label.make ("ssrparser_" ^ name)) in
let body = Tacenv.{ alias_args = ids; alias_body = tac; alias_deprecation = None } in
let parule = {
pptac_level = 0;
pptac_prods = prods
} in
let obj () =
Lib.add_leaf (inSsrGrammar (key, body, parule)) in
Mltop.declare_cache_obj obj "rocq-runtime.plugins.ssreflect";
key
let cast_arg wit v = Taccoerce.Value.cast (Genarg.topwit wit) v
}
{
(* Defining grammar rules with "xx" in it automatically declares keywords too,
* we thus save the lexer to restore it at the end of the file *)
let frozen_lexer = ref None ;;
let () = Mltop.add_init_function "rocq-runtime.plugins.ssreflect" (fun () ->
frozen_lexer := Some (Procq.freeze ()))
let tacltop = (LevelLe 5)
let pr_ssrtacarg env sigma _ _ prt = prt env sigma tacltop
}
ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma }
END
GRAMMAR EXTEND Gram
GLOBAL: ssrtacarg;
ssrtacarg: TOP [[ tac = ltac_expr LEVEL "5" -> { tac } ]];
END
(* Copy of ssrtacarg with LEVEL "3", useful for: "under ... do ..." *)
ARGUMENT EXTEND ssrtac3arg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma }
END
GRAMMAR EXTEND Gram
GLOBAL: ssrtac3arg;
ssrtac3arg: TOP [[ tac = ltac_expr LEVEL "3" -> { tac } ]];
END
{
(* Lexically closed tactic for tacticals. *)
let pr_ssrtclarg env sigma _ _ prt tac = prt env sigma tacltop tac
}
ARGUMENT EXTEND ssrtclarg TYPED AS ssrtacarg
PRINTED BY { pr_ssrtclarg env sigma }
| [ ssrtacarg(tac) ] -> { tac }
END
{
open Genarg
(** Adding a new uninterpreted generic argument type *)
let add_genarg tag pr =
let wit = Genarg.make0 tag in
let tag = Geninterp.Val.create tag in
let glob ist x = (ist, x) in
let subst _ x = x in
let interp ist x = Ftactic.return (Geninterp.Val.Dyn (tag, x)) in
let gen_pr env sigma _ _ _ = pr env sigma in
let () = Genintern.register_intern0 wit glob in
let () = Gensubst.register_subst0 wit subst in
let () = Geninterp.register_interp0 wit interp in
let () = Geninterp.register_val0 wit (Some (Geninterp.Val.Base tag)) in
Pptactic.declare_extra_genarg_pprule wit gen_pr gen_pr gen_pr;
wit
open Ssrast
let pr_id = Ppconstr.pr_id
let pr_name = function Name id -> pr_id id | Anonymous -> str "_"
let pr_spc () = str " "
let pr_list = prlist_with_sep
(**************************** ssrhyp **************************************)
let pr_ssrhyp _ _ _ = pr_hyp
let wit_ssrhyprep = add_genarg "ssrhyprep" (fun env sigma -> pr_hyp)
let intern_hyp ist (SsrHyp (loc, id) as hyp) =
let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_hyp) CAst.(make ?loc id)) in
if not_section_id id then hyp else
hyp_err ?loc "Can't clear section hypothesis " id
open Procq.Prim
}
ARGUMENT EXTEND ssrhyp TYPED AS ssrhyprep PRINTED BY { pr_ssrhyp }
INTERPRETED BY { interp_hyp }
GLOBALIZED BY { intern_hyp }
| [ ident(id) ] -> { SsrHyp (Loc.tag ~loc id) }
END
{
let pr_hoi = hoik pr_hyp
let pr_ssrhoi _ _ _ = pr_hoi
let wit_ssrhoirep = add_genarg "ssrhoirep" (fun env sigma -> pr_hoi)
let intern_ssrhoi ist = function
| Hyp h -> Hyp (intern_hyp ist h)
| Id (SsrHyp (_, id)) as hyp ->
let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_ident) id) in
hyp
let interp_ssrhoi ist env sigma = function
| Hyp h -> let h' = interp_hyp ist env sigma h in Hyp h'
| Id (SsrHyp (loc, id)) ->
let id' = Tacinterp.interp_ident ist env sigma id in
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.tag ~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.tag ~loc id)) }
END
(** Rewriting direction *)
{
let wit_ssrdir = add_genarg "ssrdir" (fun env sigma -> pr_dir)
(** Simpl switch *)
let pr_ssrsimpl _ _ _ = pr_simpl
let wit_ssrsimplrep = add_genarg "ssrsimplrep" (fun env sigma -> pr_simpl)
let test_ssrslashnum b1 b2 kwstate strm =
match LStream.peek_nth kwstate 0 strm with
| Tok.KEYWORD "/" ->
(match LStream.peek_nth kwstate 1 strm with
| Tok.NUMBER _ when b1 ->
(match LStream.peek_nth kwstate 2 strm with
| Tok.KEYWORD "=" | Tok.KEYWORD "/=" when not b2 -> ()
| Tok.KEYWORD "/" ->
if not b2 then () else begin
match LStream.peek_nth kwstate 3 strm with
| Tok.NUMBER _ -> ()
| _ -> raise Stream.Failure
end
| _ -> raise Stream.Failure)
| Tok.KEYWORD "/" when not b1 ->
(match LStream.peek_nth kwstate 2 strm with
| Tok.KEYWORD "=" when not b2 -> ()
| Tok.NUMBER _ when b2 ->
(match LStream.peek_nth kwstate 3 strm with
| Tok.KEYWORD "=" -> ()
| _ -> raise Stream.Failure)
| _ when not b2 -> ()
| _ -> raise Stream.Failure)
| Tok.KEYWORD "=" when not b1 && not b2 -> ()
| _ -> raise Stream.Failure)
| Tok.KEYWORD "//" when not b1 ->
(match LStream.peek_nth kwstate 1 strm with
| Tok.KEYWORD "=" when not b2 -> ()
| Tok.NUMBER _ when b2 ->
(match LStream.peek_nth kwstate 2 strm with
| Tok.KEYWORD "=" -> ()
| _ -> raise Stream.Failure)
| _ when not b2 -> ()
| _ -> raise Stream.Failure)
| _ -> raise Stream.Failure
let test_ssrslashnum10 = test_ssrslashnum true false
let test_ssrslashnum11 = test_ssrslashnum true true
let test_ssrslashnum01 = test_ssrslashnum false true
let test_ssrslashnum00 = test_ssrslashnum false false
let negate_parser f x y =
let rc = try Some (f x y) with Stream.Failure -> None in
match rc with
| None -> ()
| Some _ -> raise Stream.Failure
let test_not_ssrslashnum =
Procq.Entry.(of_parser
"test_not_ssrslashnum" { parser_fun = negate_parser test_ssrslashnum10 })
let test_ssrslashnum00 =
Procq.Entry.(of_parser "test_ssrslashnum01" { parser_fun = test_ssrslashnum00 })
let test_ssrslashnum10 =
Procq.Entry.(of_parser "test_ssrslashnum10" { parser_fun = test_ssrslashnum10 })
let test_ssrslashnum11 =
Procq.Entry.(of_parser "test_ssrslashnum11" { parser_fun = test_ssrslashnum11 })
let test_ssrslashnum01 =
Procq.Entry.(of_parser "test_ssrslashnum01" { parser_fun = test_ssrslashnum01 })
}
ARGUMENT EXTEND ssrsimpl_ne TYPED AS ssrsimplrep PRINTED BY { pr_ssrsimpl }
| [ "//=" ] -> { SimplCut (~-1,~-1) }
| [ "/=" ] -> { Simpl ~-1 }
END
(* Procq.Prim. *)
GRAMMAR EXTEND Gram
GLOBAL: ssrsimpl_ne;
ssrsimpl_ne: TOP [
[ test_ssrslashnum11; "/"; n = natural; "/"; m = natural; "=" -> { SimplCut(n,m) }
| test_ssrslashnum10; "/"; n = natural; "/" -> { Cut n }
| test_ssrslashnum10; "/"; n = natural; "=" -> { Simpl n }
| test_ssrslashnum10; "/"; n = natural; "/=" -> { SimplCut (n,~-1) }
| test_ssrslashnum10; "/"; n = natural; "/"; "=" -> { SimplCut (n,~-1) }
| test_ssrslashnum01; "//"; m = natural; "=" -> { SimplCut (~-1,m) }
| test_ssrslashnum00; "//" -> { Cut ~-1 }
]];
END
{
let pr_ssrclear _ _ _ = pr_clear mt
}
ARGUMENT EXTEND ssrclear_ne TYPED AS ssrhyp list 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
(** 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. *)
{
let pr_index = function
| ArgVar {CAst.v=id} -> pr_id id
| ArgArg n when n > 0 -> int n
| _ -> mt ()
let pr_ssrindex _ _ _ = pr_index
let noindex = ArgArg 0
let check_index ?loc i =
if i > 0 then i else CErrors.user_err ?loc (str"Index not positive")
let mk_index ?loc = function
| ArgArg i -> ArgArg (check_index ?loc i)
| iv -> iv
let interp_index ist env sigma idx =
match idx with
| ArgArg _ -> idx
| ArgVar id ->
let i =
try
let v = Id.Map.find id.CAst.v ist.Tacinterp.lfun in
begin match Tacinterp.Value.to_int v with
| Some i -> i
| None ->
begin match Tacinterp.Value.to_constr v with
| Some c ->
let rc = Detyping.detype Detyping.Now env sigma c in
begin match Notation.uninterp_prim_token rc ([], []) with
| Constrexpr.Number n, _ when NumTok.Signed.is_int n ->
int_of_string (NumTok.Signed.to_string n)
| _ -> raise Not_found
end
| None -> raise Not_found
end end
with e when CErrors.noncritical e -> CErrors.user_err ?loc:id.CAst.loc (str"Index not a number") in
ArgArg (check_index ?loc:id.CAst.loc i)
open Pltac
}
ARGUMENT EXTEND ssrindex PRINTED BY { pr_ssrindex }
INTERPRETED BY { interp_index }
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. *)
{
let pr_ssrocc _ _ _ = pr_occ
open Procq.Prim
}
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
(* modality *)
{
let pr_mmod = function May -> str "?" | Must -> str "!" | Once -> mt ()
let wit_ssrmmod = add_genarg "ssrmmod" (fun env sigma -> pr_mmod)
let ssrmmod = Procq.create_generic_entry2 "ssrmmod" (Genarg.rawwit wit_ssrmmod);;
}
GRAMMAR EXTEND Gram
GLOBAL: ssrmmod;
ssrmmod: [[ "!" -> { Must } | LEFTQMARK -> { May } | "?" -> { May } ]];
END
(** Rewrite multiplier: !n ?n *)
{
let pr_mult (n, m) =
if n > 0 && m <> Once then 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
{
(** Discharge occ switch (combined occurrence / clear switch *)
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 }
| [ "{" ssrocc(occ) "}" ] -> { mkocc occ }
| [ "{" ssrhyp_list(clr) "}" ] -> { mkclr clr }
END
{
(* Old kinds of terms *)
let input_ssrtermkind kwstate strm = match LStream.peek_nth kwstate 0 strm with
| Tok.KEYWORD "(" -> InParens
| Tok.KEYWORD "@" -> WithAt
| _ -> NoFlag
let ssrtermkind = Procq.Entry.(of_parser "ssrtermkind" { parser_fun = input_ssrtermkind })
(* New kinds of terms *)
let input_term_annotation kwstate strm =
match LStream.npeek kwstate 2 strm with
| Tok.KEYWORD "(" :: Tok.KEYWORD "(" :: _ -> `DoubleParens
| Tok.KEYWORD "(" :: _ -> `Parens
| Tok.KEYWORD "@" :: _ -> `At
| _ -> `None
let term_annotation =
Procq.Entry.(of_parser "term_annotation" { parser_fun = input_term_annotation })
(* terms *)
(** 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. *)
(* Old terms *)
let pr_ssrterm _ _ _ = pr_term
let glob_ssrterm gs = function
| k, (_, Some c) -> k, Tacintern.intern_constr gs c
| ct -> ct
let subst_ssrterm s (k, c) = k, Tacsubst.subst_glob_constr_and_expr s c
let interp_ssrterm _ _ _ t = t
open Procq.Constr
}
ARGUMENT EXTEND ssrterm
PRINTED BY { pr_ssrterm }
INTERPRETED BY { interp_ssrterm }
GLOBALIZED BY { glob_ssrterm } SUBSTITUTED BY { subst_ssrterm }
RAW_PRINTED BY { pr_ssrterm }
GLOB_PRINTED BY { pr_ssrterm }
END
GRAMMAR EXTEND Gram
GLOBAL: ssrterm;
ssrterm: TOP [[ k = ssrtermkind; c = Procq.Constr.constr -> { mk_term k c } ]];
END
(* New terms *)
{
let pp_ast_closure_term _ _ _ = pr_ast_closure_term
}
ARGUMENT EXTEND ast_closure_term
PRINTED BY { pp_ast_closure_term }
INTERPRETED BY { interp_ast_closure_term }
GLOBALIZED BY { glob_ast_closure_term }
SUBSTITUTED BY { subst_ast_closure_term }
RAW_PRINTED BY { pp_ast_closure_term }
GLOB_PRINTED BY { pp_ast_closure_term }
| [ term_annotation(a) constr(c) ] -> { mk_ast_closure_term a c }
END
ARGUMENT EXTEND ast_closure_lterm
PRINTED BY { pp_ast_closure_term }
INTERPRETED BY { interp_ast_closure_term }
GLOBALIZED BY { glob_ast_closure_term }
SUBSTITUTED BY { subst_ast_closure_term }
RAW_PRINTED BY { pp_ast_closure_term }
GLOB_PRINTED BY { pp_ast_closure_term }
| [ term_annotation(a) lconstr(c) ] -> { mk_ast_closure_term a c }
END
(* Old Views *)
{
let pr_view = pr_list mt (fun c -> str "/" ++ pr_term c)
let pr_ssrbwdview _ _ _ = pr_view
}
ARGUMENT EXTEND ssrbwdview TYPED AS ssrterm list
PRINTED BY { pr_ssrbwdview }
END
(* Procq *)
GRAMMAR EXTEND Gram
GLOBAL: ssrbwdview;
ssrbwdview: TOP [
[ test_not_ssrslashnum; "/"; c = Procq.Constr.constr -> { [mk_term NoFlag c] }
| test_not_ssrslashnum; "/"; c = Procq.Constr.constr; w = ssrbwdview -> {
(mk_term NoFlag c) :: w } ]];
END
(* New Views *)
{
type ssrfwdview = ast_closure_term list
let pr_ssrfwdview _ _ _ = pr_view2
}
ARGUMENT EXTEND ssrfwdview TYPED AS ast_closure_term list
PRINTED BY { pr_ssrfwdview }
END
(* Procq *)
GRAMMAR EXTEND Gram
GLOBAL: ssrfwdview;
ssrfwdview: TOP [
[ test_not_ssrslashnum; "/"; c = ast_closure_term -> { [c] }
| test_not_ssrslashnum; "/"; c = ast_closure_term; w = ssrfwdview -> { c :: w } ]];
END
(* ipats *)
{
let remove_loc x = x.CAst.v
let ipat_of_intro_pattern p = Tactypes.(
let rec ipat_of_intro_pattern = function
| IntroNaming (IntroIdentifier id) -> IPatId id
| IntroAction IntroWildcard -> IPatAnon Drop
| IntroAction (IntroOrAndPattern (IntroOrPattern iorpat)) ->
IPatCase (Regular(
List.map (List.map ipat_of_intro_pattern)
(List.map (List.map remove_loc) iorpat)))
| IntroAction (IntroOrAndPattern (IntroAndPattern iandpat)) ->
IPatCase
(Regular [List.map ipat_of_intro_pattern (List.map remove_loc iandpat)])
| IntroNaming IntroAnonymous -> IPatAnon (One None)
| IntroAction (IntroRewrite b) -> IPatRewrite (allocc, if b then L2R else R2L)
| IntroNaming (IntroFresh id) -> IPatAnon (One None)
| IntroAction (IntroApplyOn _) -> (* to do *) CErrors.user_err (Pp.str "TO DO")
| IntroAction (IntroInjection ips) ->
IPatInj [List.map ipat_of_intro_pattern (List.map remove_loc ips)]
| IntroForthcoming _ ->
(* Unable to determine which kind of ipat interp_introid could
* return [HH] *)
assert false
in
ipat_of_intro_pattern p
)
let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function
| (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop | IPatFastNondep) as x -> x
| IPatId id -> IPatId (map_id id)
| IPatAbstractVars l -> IPatAbstractVars (List.map map_id l)
| IPatClear clr -> IPatClear (List.map map_ssrhyp clr)
| IPatCase (Regular iorpat) -> IPatCase (Regular (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat))
| IPatCase (Block(hat)) -> IPatCase (Block(map_block map_id hat))
| IPatDispatch (Regular iorpat) -> IPatDispatch (Regular (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat))
| IPatDispatch (Block (hat)) -> IPatDispatch (Block(map_block map_id hat))
| IPatInj iorpat -> IPatInj (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)
| IPatView v -> IPatView (List.map map_ast_closure_term v)
and map_block map_id = function
| Prefix id -> Prefix (map_id id)
| SuffixId id -> SuffixId (map_id id)
| SuffixNum _ as x -> x
type ssripatrep = ssripat
let wit_ssripatrep = add_genarg "ssripatrep" (fun env sigma -> pr_ipat)
let pr_ssripat _ _ _ = pr_ipat
let pr_ssripats _ _ _ = pr_ipats
let pr_ssriorpat _ _ _ = pr_iorpat
let intern_ipat ist =
map_ipat
(fun id -> id)
(intern_hyp ist)
(glob_ast_closure_term ist)
let intern_ipats ist = List.map (intern_ipat ist)
let interp_intro_pattern = Tacinterp.interp_intro_pattern
let interp_introid ist env sigma id =
try IntroNaming (IntroIdentifier (hyp_id (interp_hyp ist env sigma (SsrHyp (Loc.tag id)))))
with e when CErrors.noncritical e ->
(interp_intro_pattern ist env sigma (CAst.make @@ IntroNaming (IntroIdentifier id))).CAst.v
let get_intro_id = function
| IntroNaming (IntroIdentifier id) -> id
| _ -> assert false
let rec add_intro_pattern_hyps ipat hyps =
let {CAst.loc; v=ipat} = ipat in
match ipat with
| IntroNaming (IntroIdentifier id) ->
if not_section_id id then SsrHyp (loc, id) :: hyps else
hyp_err ?loc "Can't delete section hypothesis " id
| IntroAction IntroWildcard -> hyps
| IntroAction (IntroOrAndPattern (IntroOrPattern iorpat)) ->
List.fold_right (List.fold_right add_intro_pattern_hyps) iorpat hyps
| IntroAction (IntroOrAndPattern (IntroAndPattern iandpat)) ->
List.fold_right add_intro_pattern_hyps iandpat hyps
| IntroNaming IntroAnonymous -> []
| IntroNaming (IntroFresh _) -> []
| IntroAction (IntroRewrite _) -> hyps
| IntroAction (IntroInjection ips) -> List.fold_right add_intro_pattern_hyps ips hyps
| IntroAction (IntroApplyOn (c,pat)) -> add_intro_pattern_hyps pat hyps
| IntroForthcoming _ ->
(* As in ipat_of_intro_pattern, was unable to determine which kind
of ipat interp_introid could return [HH] *) assert false
(* We interp the ipat using the standard ltac machinery for ids, since
* we have no clue what a name could be bound to (maybe another ipat) *)
let interp_ipat ist env sigma =
let ltacvar id = Id.Map.mem id ist.Tacinterp.lfun in
let interp_block = function
| Prefix id when ltacvar id ->
begin match interp_introid ist env sigma id with
| IntroNaming (IntroIdentifier id) -> Prefix id
| _ -> Ssrcommon.errorstrm Pp.(str"Variable " ++ Id.print id ++ str" in block intro pattern should be bound to an identifier.")
end
| SuffixId id when ltacvar id ->
begin match interp_introid ist env sigma id with
| IntroNaming (IntroIdentifier id) -> SuffixId id
| _ -> Ssrcommon.errorstrm Pp.(str"Variable " ++ Id.print id ++ str" in block intro pattern should be bound to an identifier.")
end
| x -> x in
let rec interp = function
| IPatId id when ltacvar id ->
ipat_of_intro_pattern (interp_introid ist env sigma id)
| IPatId _ as x -> x
| IPatClear clr ->
let add_hyps (SsrHyp (loc, id) as hyp) hyps =
if not (ltacvar id) then hyp :: hyps else
add_intro_pattern_hyps CAst.(make ?loc (interp_introid ist env sigma id)) hyps in
let clr' = List.fold_right add_hyps clr [] in
check_hyps_uniq [] clr';
IPatClear clr'
| IPatCase(Regular iorpat) ->
IPatCase(Regular(List.map (List.map interp) iorpat))
| IPatCase(Block(hat)) -> IPatCase(Block(interp_block hat))
| IPatDispatch(Regular iorpat) ->
IPatDispatch(Regular (List.map (List.map interp) iorpat))
| IPatDispatch(Block(hat)) -> IPatDispatch(Block(interp_block hat))
| IPatInj iorpat -> IPatInj (List.map (List.map interp) iorpat)
| IPatAbstractVars l ->
IPatAbstractVars (List.map get_intro_id (List.map (interp_introid ist env sigma) l))
| IPatView l -> IPatView (List.map (fun x -> interp_ast_closure_term ist
env sigma x) l)
| (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop | IPatFastNondep) as x -> x
in
interp
let interp_ipats ist env sigma l = List.map (interp_ipat ist env sigma) l
let pushIPatRewrite = function
| pats :: orpat -> (IPatRewrite (allocc, L2R) :: pats) :: orpat
| [] -> []
let pushIPatNoop = function
| pats :: orpat -> (IPatNoop :: pats) :: orpat
| [] -> []
let test_ident_no_do =
let open Procq.Lookahead in
to_entry "test_ident_no_do" begin
lk_ident_except ["do"]
end
}
ARGUMENT EXTEND ident_no_do PRINTED BY { fun _ _ _ -> Names.Id.print }
END
GRAMMAR EXTEND Gram
GLOBAL: ident_no_do;
ident_no_do: TOP [ [ test_ident_no_do; id = IDENT -> { Id.of_string id } ] ];
END
ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY { pr_ssripats }
INTERPRETED BY { interp_ipats }
GLOBALIZED BY { intern_ipats }
| [ "_" ] -> { [IPatAnon Drop] }
| [ "*" ] -> { [IPatAnon All] }
| [ ">" ] -> { [IPatFastNondep] }
| [ ident_no_do(id) ] -> { [IPatId id] }
| [ "?" ] -> { [IPatAnon (One None)] }
| [ "+" ] -> { [IPatAnon Temporary] }
| [ "++" ] -> { [IPatAnon Temporary; IPatAnon Temporary] }
| [ ssrsimpl_ne(sim) ] -> { [IPatSimpl sim] }
| [ ssrdocc(occ) "->" ] -> { match occ with
| Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected")
| None, occ -> [IPatRewrite (occ, L2R)]
| Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, L2R)] }
| [ ssrdocc(occ) "<-" ] -> { match occ with
| Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected")
| None, occ -> [IPatRewrite (occ, R2L)]
| Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, R2L)] }
| [ ssrdocc(occ) ] -> { match occ with
| Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl]
| _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here") }
| [ "->" ] -> { [IPatRewrite (allocc, L2R)] }
| [ "<-" ] -> { [IPatRewrite (allocc, R2L)] }
| [ "-" ] -> { [IPatNoop] }
| [ "-/" "=" ] -> { [IPatNoop;IPatSimpl(Simpl ~-1)] }
| [ "-/=" ] -> { [IPatNoop;IPatSimpl(Simpl ~-1)] }
| [ "-/" "/" ] -> { [IPatNoop;IPatSimpl(Cut ~-1)] }
| [ "-//" ] -> { [IPatNoop;IPatSimpl(Cut ~-1)] }
| [ "-/" integer(n) "/" ] -> { [IPatNoop;IPatSimpl(Cut n)] }
| [ "-/" "/=" ] -> { [IPatNoop;IPatSimpl(SimplCut (~-1,~-1))] }
| [ "-//" "=" ] -> { [IPatNoop;IPatSimpl(SimplCut (~-1,~-1))] }
| [ "-//=" ] -> { [IPatNoop;IPatSimpl(SimplCut (~-1,~-1))] }
| [ "-/" integer(n) "/=" ] -> { [IPatNoop;IPatSimpl(SimplCut (n,~-1))] }
| [ "-/" integer(n) "/" integer (m) "=" ] ->
{ [IPatNoop;IPatSimpl(SimplCut(n,m))] }
| [ ssrfwdview(v) ] -> { [IPatView v] }
| [ "[" ":" ident_list(idl) "]" ] -> { [IPatAbstractVars idl] }
| [ "[:" ident_list(idl) "]" ] -> { [IPatAbstractVars 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 :: pushIPatRewrite orpat }
| [ ssripats(pats) "|-" ssriorpat(orpat) ] -> { pats :: pushIPatNoop orpat }
| [ ssripats(pats) "|->" ssriorpat(orpat) ] -> { pats :: pushIPatRewrite orpat }
| [ ssripats(pats) "||" ssriorpat(orpat) ] -> { pats :: [] :: orpat }
| [ ssripats(pats) "|||" ssriorpat(orpat) ] -> { pats :: [] :: [] :: orpat }
| [ ssripats(pats) "||||" ssriorpat(orpat) ] -> { [pats; []; []; []] @ orpat }
| [ ssripats(pats) ] -> { [pats] }
END
{
let test_leftsquarebracket_equal =
let open Procq.Lookahead in
to_entry "test_leftsquarebracket_equal" begin
lk_kw "[" >> lk_kw "=" >> check_no_space
end
let reject_ssrhid kwstate strm =
match LStream.peek_nth kwstate 0 strm with
| Tok.KEYWORD "[" ->
(match LStream.peek_nth kwstate 1 strm with
| Tok.KEYWORD ":" -> raise Stream.Failure
| _ -> ())
| _ -> ()
let test_nohidden = Procq.Entry.(of_parser "test_ssrhid" { parser_fun = reject_ssrhid })
let rec reject_binder crossed_paren k kwstate s =
match
try Some (LStream.peek_nth kwstate k s)
with Stream.Failure -> None
with
| Some (Tok.KEYWORD "(") when not crossed_paren -> reject_binder true (k+1) kwstate s
| Some (Tok.IDENT _) when crossed_paren -> reject_binder true (k+1) kwstate s
| Some (Tok.KEYWORD ":" | Tok.KEYWORD ":=") when crossed_paren ->
raise Stream.Failure
| Some (Tok.KEYWORD ")") when crossed_paren -> raise Stream.Failure
| _ -> if crossed_paren then () else raise Stream.Failure
let _test_nobinder = Procq.Entry.(of_parser "test_nobinder" { parser_fun = reject_binder false 0 })
}
ARGUMENT EXTEND ssrcpat TYPED AS ssripatrep PRINTED BY { pr_ssripat }
INTERPRETED BY { interp_ipat }
GLOBALIZED BY { intern_ipat }
END
(* Procq *)
GRAMMAR EXTEND Gram
GLOBAL: ssrcpat;
hat: [
[ "^"; id = ident -> { Prefix id }
| "^"; "~"; id = ident -> { SuffixId id }
| "^"; "~"; n = natural -> { SuffixNum n }
| "^~"; id = ident -> { SuffixId id }
| "^~"; n = natural -> { SuffixNum n }
]];
ssrcpat: TOP [
[ test_leftsquarebracket_equal; test_nohidden; "["; "="; iorpat = ssriorpat; "]" -> {
IPatInj iorpat }
| test_nohidden; "["; hat_id = hat; "]" -> {
IPatCase (Block(hat_id)) }
| test_nohidden; "["; iorpat = ssriorpat; "]" -> {
IPatCase (Regular iorpat) } ]];
END
GRAMMAR EXTEND Gram
GLOBAL: ssripat;
ssripat: TOP [[ 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 *)
{
(* TODO: review what this function does, it looks suspicious *)
let check_ssrhpats loc w_binders ipats =
let err_loc s = CErrors.user_err ~loc s in
let clr, ipats =
let opt_app = function None -> fun l -> Some l
| Some l1 -> fun l2 -> Some (l1 @ l2) in
let rec aux clr = function
| IPatClear cl :: tl -> aux (opt_app clr cl) tl
| tl -> clr, tl
in aux None 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 _ | IPatDispatch _ | IPatRewrite _ 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 pr_clear_opt sep = function None -> mt () | Some x -> pr_clear sep x
let pr_hpats (((clr, ipat), binders), simpl) =
pr_clear_opt 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 option * ssripat) * ssripat) * ssripat)
PRINTED BY { pr_ssrhpats }
| [ ssripats(i) ] -> { check_ssrhpats loc true i }
END
ARGUMENT EXTEND ssrhpats_wtransp
TYPED AS (bool * (((ssrclear option * ssripats) * ssripats) * ssripats))
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 option * ssripats) * ssripats) * ssripats) PRINTED BY { pr_ssrhpats }
| [ ssripats(i) ] -> { check_ssrhpats loc false i }
END
ARGUMENT EXTEND ssrrpat TYPED AS ssripatrep PRINTED BY { pr_ssripat }
| [ "->" ] -> { IPatRewrite (allocc, L2R) }
| [ "<-" ] -> { IPatRewrite (allocc, R2L) }
END
{
let pr_intros sep intrs =
if intrs = [] then mt() else sep () ++ str "=>" ++ sep () ++ pr_ipats intrs
let pr_ssrintros _ _ _ = pr_intros mt
}
ARGUMENT EXTEND ssrintros_ne TYPED AS ssripat
PRINTED BY { pr_ssrintros }
| [ "=>" ssripats_ne(pats) ] -> { pats }
(* TODO | [ "=>" ">" ssripats_ne(pats) ] -> { IPatFastMode :: pats }
| [ "=>>" ssripats_ne(pats) ] -> [ IPatFastMode :: pats ] *)
END
ARGUMENT EXTEND ssrintros TYPED AS ssrintros_ne PRINTED BY { pr_ssrintros }
| [ ssrintros_ne(intrs) ] -> { intrs }
| [ ] -> { [] }
END
{
let pr_ssrintrosarg env sigma _ _ prt (tac, ipats) =
prt env sigma tacltop tac ++ pr_intros spc ipats
}
ARGUMENT EXTEND ssrintrosarg TYPED AS (tactic * ssrintros)
PRINTED BY { pr_ssrintrosarg env sigma }
END
{
(** Defined identifier *)
let pr_ssrfwdid id = pr_spc () ++ pr_id id
let pr_ssrfwdidx _ _ _ = pr_ssrfwdid
}
(* We use a primitive parser for the head identifier of forward *)
(* tactis to avoid syntactic conflicts with basic Rocq tactics. *)
ARGUMENT EXTEND ssrfwdid TYPED AS ident PRINTED BY { pr_ssrfwdidx }
END
{
let test_ssrfwdid =
let open Procq.Lookahead in
to_entry "test_ssrfwdid" begin
lk_ident >> (lk_ident <+> lk_kws [":"; ":="; "("])
end
}
GRAMMAR EXTEND Gram
GLOBAL: ssrfwdid;
ssrfwdid: TOP [[ test_ssrfwdid; id = Prim.ident -> { id } ]];
END
(* by *)
(** 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. *)
{
let pr_ortacs env sigma prt =
let rec pr_rec = function
| [None] -> spc() ++ str "|" ++ spc()
| None :: tacs -> spc() ++ str "|" ++ pr_rec tacs
| Some tac :: tacs -> spc() ++ str "| " ++ prt env sigma tacltop tac ++ pr_rec tacs
| [] -> mt() in
function
| [None] -> spc()
| None :: tacs -> pr_rec tacs
| Some tac :: tacs -> prt env sigma tacltop tac ++ pr_rec tacs
| [] -> mt()
let pr_ssrortacs env sigma _ _ = pr_ortacs env sigma
}
ARGUMENT EXTEND ssrortacs TYPED AS tactic option list PRINTED BY { pr_ssrortacs env sigma }
| [ 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 env sigma prt = function
| true, tacs -> hv 0 (str "[ " ++ pr_ortacs env sigma prt tacs ++ str " ]")
| false, [Some tac] -> prt env sigma tacltop tac
| _, _ -> mt()
let pr_ssrhintarg env sigma _ _ = pr_hintarg env sigma
}
ARGUMENT EXTEND ssrhintarg TYPED AS (bool * ssrortacs) PRINTED BY { pr_ssrhintarg env sigma }
| [ "[" "]" ] -> { nullhint }
| [ "[" ssrortacs(tacs) "]" ] -> { mk_orhint tacs }
| [ ssrtacarg(arg) ] -> { mk_hint arg }
END
(* Copy of ssrhintarg with LEVEL "3", useful for: "under ... do ..." *)
ARGUMENT EXTEND ssrhint3arg TYPED AS (bool * ssrortacs) PRINTED BY { pr_ssrhintarg env sigma }
| [ "[" "]" ] -> { nullhint }
| [ "[" ssrortacs(tacs) "]" ] -> { mk_orhint tacs }
| [ ssrtac3arg(arg) ] -> { mk_hint arg }
END
ARGUMENT EXTEND ssrortacarg TYPED AS ssrhintarg PRINTED BY { pr_ssrhintarg env sigma }
| [ "[" ssrortacs(tacs) "]" ] -> { mk_orhint tacs }
END
{
let pr_hint env sigma prt arg =
if arg = nohint then mt() else spc () ++ str "by" ++ spc () ++ pr_hintarg env sigma prt arg
let pr_ssrhint env sigma _ _ = pr_hint env sigma
}
ARGUMENT EXTEND ssrhint TYPED AS ssrhintarg PRINTED BY { pr_ssrhint env sigma }
| [ ] -> { nohint }
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. *)
{
open Ssrmatching_plugin.G_ssrmatching
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
{
let pr_clseq = function
| InGoal | InHyps -> mt ()
| InSeqGoal -> str "|- *"
| InHypsSeqGoal -> str " |- *"
| InHypsGoal -> str " *"
| InAll -> str "*"
| InHypsSeq -> str " |-"
| InAllHyps -> str "* |-"
let wit_ssrclseq = add_genarg "ssrclseq" (fun env sigma -> 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
{
(** 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. *)
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
let rec format_local_binders h0 bl0 = match h0, bl0 with
| BFvar :: h, CLocalAssum ([{CAst.v=x}], _, _, _) :: bl ->
Bvar x :: format_local_binders h bl
| BFdecl _ :: h, CLocalAssum (lxs, _, _, t) :: bl ->
Bdecl (List.map (fun x -> x.CAst.v) lxs, t) :: format_local_binders h bl
| BFdef :: h, CLocalDef ({CAst.v=x}, _, v, oty) :: bl ->
Bdef (x, oty, v) :: format_local_binders h bl
| _ -> []
let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with
| BFvar :: h, { v = CLambdaN ([CLocalAssum([{CAst.v=x}], _, _, _)], c) } ->
let bs, c' = format_constr_expr h c in
Bvar x :: bs, c'
| BFdecl _:: h, { v = CLambdaN ([CLocalAssum(lxs, _, _, t)], c) } ->
let bs, c' = format_constr_expr h c in
Bdecl (List.map (fun x -> x.CAst.v) lxs, t) :: bs, c'
| BFdef :: h, { v = CLetIn({CAst.v=x}, v, oty, c) } ->
let bs, c' = format_constr_expr h c in
Bdef (x, oty, v) :: bs, c'
| [BFcast], { v = CCast (c, defaultCast, t) } ->
[Bcast t], c
| BFrec (has_str, has_cast) :: h,
{ v = CFix ( _, [_, _, Some {CAst.v = CStructRec locn}, bl, t, c]) } ->
let bs = format_local_binders h bl in
let bstr = if has_str then [Bstruct (Name locn.CAst.v)] else [] in
bs @ bstr @ (if has_cast then [Bcast t] else []), c
| BFrec (_, has_cast) :: h, { v = CCoFix ( _, [_, _, bl, t, c]) } ->
format_local_binders h bl @ (if has_cast then [Bcast t] else []), c
| _, 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. *)
let pr_fwdkind = function
| FwdHint (s,_) -> str (s ^ " ") | _ -> str " :=" ++ spc ()
let pr_fwdfmt (fk, _ : ssrfwdfmt) = pr_fwdkind fk
let wit_ssrfwdfmt = add_genarg "ssrfwdfmt" (fun env sigma -> pr_fwdfmt)
(* type ssrfwd = ssrfwdfmt * ssrterm *)
let mkFwdVal fk c = ((fk, []), c)
let mkssrFwdVal fk c = ((fk, []), (c,None))
let same_ist { interp_env = x } { interp_env = y } =
match x,y with
| None, None -> true
| Some a, Some b -> a == b
| _ -> false
let mkFwdCast fk ?loc ?c t =
let c = match c with
| None -> mkCHole loc
| Some c -> assert (same_ist t c); c.body in
((fk, [BFcast]),
{ t with annotation = `None;
body = (CAst.make ?loc @@ CCast (c, Some defaultCast, t.body)) })
let mkssrFwdCast fk loc t c = ((fk, [BFcast]), (c, Some t))
let mkFwdHint s t =
let loc = Constrexpr_ops.constr_loc t.body in
mkFwdCast (FwdHint (s,false)) ?loc t
let mkFwdHintNoTC s t =
let loc = Constrexpr_ops.constr_loc t.body in
mkFwdCast (FwdHint (s,true)) ?loc t
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), c ->
pr_gen_fwd prval pr_constr_expr prl_constr_expr fk (format_constr_expr h c.body)
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 * ast_closure_lterm) PRINTED BY { pr_ssrfwd }
| [ ":=" ast_closure_lterm(c) ] -> { mkFwdVal FwdPose c }
| [ ":" ast_closure_lterm (t) ":=" ast_closure_lterm(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 env sigma prc _ _ v = prc env sigma v
}
ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY { pr_ssrbvar env sigma }
| [ ident(id) ] -> { mkCVar ~loc id }
| [ "_" ] -> { mkCHole (Some loc) }
END
{
let bvar_lname = let open CAst in function
| { v = CRef (qid, _) } when qualid_is_ident qid ->
CAst.make ?loc:qid.CAst.loc @@ Name (qualid_basename qid)
| { loc = loc } -> CAst.make ?loc Anonymous
let pr_ssrbinder env sigma prc _ _ (_, c) = prc env sigma c
}
ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinder env sigma }
| [ ssrbvar(bv) ] ->
{ let { CAst.loc=xloc } as x = bvar_lname bv in
(FwdPose, [BFvar]),
CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],None,Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) }
| [ "(" ssrbvar(bv) ")" ] ->
{ let { CAst.loc=xloc } as x = bvar_lname bv in
(FwdPose, [BFvar]),
CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],None,Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) }
| [ "(" ssrbvar(bv) ":" lconstr(t) ")" ] ->
{ let x = bvar_lname bv in
(FwdPose, [BFdecl 1]),
CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], None, Default Glob_term.Explicit, t)], mkCHole (Some loc)) }
| [ "(" 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]),
CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, None, Default Glob_term.Explicit, t)], mkCHole (Some loc)) }
| [ "(" ssrbvar(id) ":" lconstr(t) ":=" lconstr(v) ")" ] ->
{ (FwdPose,[BFdef]), CAst.make ~loc @@ CLetIn (bvar_lname id, v, Some t, mkCHole (Some loc)) }
| [ "(" ssrbvar(id) ":=" lconstr(v) ")" ] ->
{ (FwdPose,[BFdef]), CAst.make ~loc @@ CLetIn (bvar_lname id, v, None, mkCHole (Some loc)) }
END
GRAMMAR EXTEND Gram
GLOBAL: ssrbinder;
ssrbinder: TOP [
[ ["of" -> { () } | "&" -> { () } ]; c = term LEVEL "99" -> {
(FwdPose, [BFvar]),
CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],None,Default Glob_term.Explicit,c)],mkCHole (Some loc)) } ]
];
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 = Loc.merge_opt loc1 loc2 in
let open CAst in
let rec loop ty c = function
| (_, { loc = loc1; v = CLambdaN (b, _) } ) :: bs when ty ->
CAst.make ?loc:(mkloc loc1) @@ CProdN (b, loop ty c bs)
| (_, { loc = loc1; v = CLambdaN (b, _) } ) :: bs ->
CAst.make ?loc:(mkloc loc1) @@ CLambdaN (b, loop ty c bs)
| (_, { loc = loc1; v = CLetIn (x, v, oty, _) } ) :: bs ->
CAst.make ?loc:(mkloc loc1) @@ CLetIn (x, v, oty, loop ty c bs)
| [] -> c
| _ -> anomaly "binder not a lambda nor a let in" in
match c2 with
| { loc; v = CCast (ct, defaultCast, cty) } ->
CAst.make ?loc @@ (CCast (loop false ct bs, defaultCast, (loop true cty bs)))
| ct -> loop false ct bs
let rec fix_binders = let open CAst in function
| (_, { v = CLambdaN ([CLocalAssum(xs, _, _, t)], _) } ) :: bs ->
CLocalAssum (xs, None, Default Glob_term.Explicit, t) :: fix_binders bs
| (_, { v = CLetIn (x, v, oty, _) } ) :: bs ->
CLocalDef (x, None, v, oty) :: 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 ((fk, h), c) =
(fk,binders_fmts bs @ h), { c with body = push_binders c.body bs }
}
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
| { CAst.v = CRef (qid, _) } when qualid_is_ident qid ->
CAst.make ?loc:qid.CAst.loc (qualid_basename qid)
| _ -> CErrors.user_err (Pp.str "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 { CAst.v=id } as lid = bvar_locid bv in
let (fk, h), ac = fwd in
let c = ac.body in
let has_cast, t', c' = match format_constr_expr h c with
| [Bcast t'], c' -> true, t', c'
| _ -> false, mkCHole (constr_loc c), c in
let lb = fix_binders bs in
let has_struct, i =
let rec loop = function
| {CAst.loc=l'; v=Name id'} :: _ when Option.equal Id.equal sid (Some id') ->
true, CAst.make ?loc:l' id'
| [{CAst.loc=l';v=Name id'}] when sid = None ->
false, CAst.make ?loc:l' id'
| _ :: bn -> loop bn
| [] -> CErrors.user_err (Pp.str "Bad structural argument") in
loop (names_of_local_assums lb) in
let h' = BFrec (has_struct, has_cast) :: binders_fmts bs in
let fix = CAst.make ~loc @@ CFix (lid, [lid, None, (Some (CAst.make (CStructRec i))), lb, t', c']) in
id, ((fk, h'), { ac with body = fix }) }
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 { CAst.v=id } as lid = bvar_locid bv in
let (fk, h), ac = fwd in
let c = ac.body in
let has_cast, t', c' = match format_constr_expr h c with
| [Bcast t'], c' -> true, t', c'
| _ -> false, mkCHole (constr_loc c), c in
let h' = BFrec (false, has_cast) :: binders_fmts bs in
let cofix = CAst.make ~loc @@ CCoFix (lid, [lid, None, fix_binders bs, t', c']) in
id, ((fk, h'), { ac with body = cofix })
}
END
{
let pr_ssrsetfwd _ _ _ (((fk,_),(c,t)), docc) =
let t = Option.default [] @@ Option.map (fun t -> [Bcast t]) t in
pr_gen_fwd (fun _ _ c -> Pp.(pr_docc docc ++ pr_cpattern c))
(fun _ -> mt()) pr_ast_closure_term fk (t, c)
}
ARGUMENT EXTEND ssrsetfwd
TYPED AS ((ssrfwdfmt * (lcpattern * ast_closure_lterm option)) * ssrdocc)
PRINTED BY { pr_ssrsetfwd }
| [ ":" ast_closure_lterm(t) ":=" "{" ssrocc(occ) "}" cpattern(c) ] ->
{ mkssrFwdCast FwdPose loc t c, mkocc occ }
| [ ":" ast_closure_lterm(t) ":=" lcpattern(c) ] ->
{ mkssrFwdCast FwdPose loc t c, nodocc }
| [ ":=" "{" ssrocc(occ) "}" cpattern(c) ] ->
{ mkssrFwdVal FwdPose c, mkocc occ }
| [ ":=" lcpattern(c) ] -> { mkssrFwdVal FwdPose c, nodocc }
END
{
let pr_ssrhavefwd env sigma _ _ prt (fwd, hint) = pr_fwd fwd ++ pr_hint env sigma prt hint
}
ARGUMENT EXTEND ssrhavefwd TYPED AS (ssrfwd * ssrhint) PRINTED BY { pr_ssrhavefwd env sigma }
| [ ":" ast_closure_lterm(t) ssrhint(hint) ] -> { mkFwdHint ":" t, hint }
| [ ":" ast_closure_lterm(t) ":=" ast_closure_lterm(c) ] -> { mkFwdCast FwdHave ~loc t ~c, nohint }
| [ ":" ast_closure_lterm(t) ":=" ] -> { mkFwdHintNoTC ":" t, nohint }
| [ ":=" ast_closure_lterm(c) ] -> { mkFwdVal FwdHave c, nohint }
END
{
let intro_id_to_binder = List.map (function
| IPatId id ->
let { CAst.loc=xloc } as x = bvar_lname (mkCVar id) in
(FwdPose, [BFvar]),
CAst.make @@ CLambdaN ([CLocalAssum([x], None, Default Glob_term.Explicit, mkCHole xloc)],
mkCHole None)
| _ -> anomaly "non-id accepted as binder")
let binder_to_intro_id = CAst.(List.map (function
| (FwdPose, [BFvar]), { v = CLambdaN ([CLocalAssum(ids,_,_,_)],_) }
| (FwdPose, [BFdecl _]), { v = CLambdaN ([CLocalAssum(ids,_,_,_)],_) } ->
List.map (function {v=Name id} -> IPatId id | _ -> IPatAnon (One None)) ids
| (FwdPose, [BFdef]), { v = CLetIn ({v=Name id},_,_,_) } -> [IPatId id]
| (FwdPose, [BFdef]), { v = CLetIn ({v=Anonymous},_,_,_) } -> [IPatAnon (One None)]
| _ -> anomaly "ssrbinder is not a binder"))
let pr_ssrhavefwdwbinders env sigma _ _ prt (tr,((hpats, (fwd, hint)))) =
pr_hpats hpats ++ pr_fwd fwd ++ pr_hint env sigma prt hint
}
ARGUMENT EXTEND ssrhavefwdwbinders
TYPED AS (bool * (ssrhpats * (ssrfwd * ssrhint)))
PRINTED BY { pr_ssrhavefwdwbinders env sigma }
| [ 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
{
let pr_ssrdoarg env sigma prc _ prt (((n, m), tac), clauses) =
pr_index n ++ pr_mmod m ++ pr_hintarg env sigma prt tac ++ pr_clauses clauses
}
ARGUMENT EXTEND ssrdoarg
TYPED AS (((ssrindex * ssrmmod) * ssrhintarg) * ssrclauses)
PRINTED BY { pr_ssrdoarg env sigma }
END
{
(* type ssrseqarg = ssrindex * (ssrtacarg * ssrtac option) *)
let pr_seqtacarg env sigma prt = function
| (is_first, []), _ -> str (if is_first then "first" else "last")
| tac, Some dtac ->
hv 0 (pr_hintarg env sigma prt tac ++ spc() ++ str "|| " ++ prt env sigma tacltop dtac)
| tac, _ -> pr_hintarg env sigma prt tac
let pr_ssrseqarg env sigma _ _ prt = function
| ArgArg 0, tac -> pr_seqtacarg env sigma prt tac
| i, tac -> pr_index i ++ str " " ++ pr_seqtacarg env sigma 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 env sigma }
END
{
let sq_brace_tacnames =
["first"; "solve"; "do"; "rewrite"; "have"; "suffices"; "wlog"]
(* "by" is a keyword *)
let test_ssrseqvar =
let open Procq.Lookahead in
to_entry "test_ssrseqvar" begin
lk_ident_except sq_brace_tacnames >> (lk_kws ["[";"first";"last"])
end
let swaptacarg (loc, b) = (b, []), Some (CAst.make ~loc (TacId []))
let ssrorelse = Entry.make "ssrorelse"
}
GRAMMAR EXTEND Gram
GLOBAL: ssrorelse ssrseqarg;
ssrseqidx: [
[ test_ssrseqvar; id = Prim.ident -> { ArgVar (CAst.make ~loc id) }
| n = Prim.natural -> { ArgArg (check_index ~loc n) }
] ];
ssrswap: [[ IDENT "first" -> { loc, true } | IDENT "last" -> { loc, false } ]];
ssrorelse: [[ "||"; tac = ltac_expr LEVEL "2" -> { tac } ]];
ssrseqarg: TOP [
[ arg = ssrswap -> { noindex, swaptacarg arg }
| i = ssrseqidx; tac = ssrortacarg; def = OPT ssrorelse -> { i, (tac, def) }
| i = ssrseqidx; arg = ssrswap -> { i, swaptacarg arg }
| tac = ltac_expr LEVEL "3" -> { noindex, (mk_hint tac, None) }
] ];
END
{
let ltac_expr = Pltac.ltac_expr
}
(** 1. Utilities *)
(** Name generation *)
(* Since Rocq 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 { Goptions.get = ssr_reserved_ids } =
Goptions.declare_bool_option_and_ref ~stage:Synterp ~key:["SsrIdents"] ~value:true ()
let is_ssr_reserved s =
let n = String.length s in n > 2 && s.[0] = '_' && s.[n - 1] = '_'
let ssr_id_of_string loc s =
if is_ssr_reserved s && is_ssr_loaded () then begin
if ssr_reserved_ids() then
CErrors.user_err ~loc (str ("The identifier " ^ s ^ " is reserved."))
else if is_internal_name s then
Feedback.msg_warning (str ("Conflict between " ^ s ^ " and ssreflect internal names."))
else Feedback.msg_warning (str (
"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 = Procq.Entry.(of_parser "ssr_null" { parser_fun = fun _ _ -> () })
}
GRAMMAR EXTEND Gram
GLOBAL: Prim.ident;
Prim.ident: TOP [[ s = IDENT; ssr_null_entry -> { ssr_id_of_string loc s } ]];
END
{
let perm_tag = "_perm_Hyp_"
let _ = add_internal_name (is_tagged perm_tag)
}
(* We must not anonymize context names discharged by the "in" tactical. *)
(** Tactical extensions. *)
{
let ssrtac_expr ?loc key args =
CAst.make ?loc (TacAlias (key, (List.map (fun x -> Tacexpr.TacGeneric (None, x)) args)))
let mk_non_term wit id =
let open Pptactic in
TacNonTerm (None, (Extend.Uentry (Genarg.ArgT.Any (Genarg.get_arg_tag wit)), Some id))
let tclintroskey =
let prods =
[ mk_non_term wit_ssrintrosarg (Names.Id.of_string "arg") ] in
let tac = begin fun args ist -> match args with
| [arg] ->
let arg = cast_arg wit_ssrintrosarg arg in
let tac, intros = arg in
ssrevaltac ist tac <*> tclIPATssr intros
| _ -> assert false
end in
register_ssrtac "tclintros" tac prods
let tclintros_expr ?loc tac ipats =
let args = [in_gen (rawwit wit_ssrintrosarg) (tac, ipats)] in
ssrtac_expr ?loc tclintroskey args
}
GRAMMAR EXTEND Gram
GLOBAL: ltac_expr;
ltac_expr: LEVEL "3" [
[ tac = ltac_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros }
] ];
ltac_expr: LEVEL "4" [
[ tac = ltac_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros }
] ];
END
(** 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). *)
GRAMMAR EXTEND Gram
GLOBAL: ltac_expr;
ssrparentacarg: [[ "("; tac = ltac_expr; ")" -> { CAst.make ~loc (Tacexp tac) } ]];
ltac_expr: LEVEL "0" [[ arg = ssrparentacarg -> { CAst.make ~loc (TacArg CAst.(arg.v)) } ]];
END
{
type ssreqid = ssripatrep option
type ssrarg = ssrfwdview * (ssreqid * (cpattern ssragens * ssripats))
}
{
(* 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 () = Mltop.add_init_function "rocq-runtime.plugins.ssreflect" (fun () ->
Procq.unfreeze_only_keywords (Option.get !frozen_lexer);
frozen_lexer := None) ;;
module Internal = struct
let register_ssrtac = register_ssrtac
let mk_index = mk_index
let noindex = noindex
let tclintros_expr = tclintros_expr
let intern_ipat = intern_ipat
let interp_ipat = interp_ipat
let pr_intros = pr_intros
let pr_view = pr_view
let pr_mult = pr_mult
let is_ssr_loaded = is_ssr_loaded
let pr_hpats = pr_hpats
let pr_fwd = pr_fwd
let pr_hint = pr_hint
let intro_id_to_binder = intro_id_to_binder
let binder_to_intro_id = binder_to_intro_id
let mkFwdHint = mkFwdHint
let bind_fwd = bind_fwd
let pr_wgen = pr_wgen
end
}
(* vim: set filetype=ocaml foldmethod=marker: *)
[ Dauer der Verarbeitung: 0.25 Sekunden
(vorverarbeitet)
]
|
