|
(************************************************************************)
(* * 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) *)
(************************************************************************)
(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
{
open Ltac_plugin
open Procq.Constr
open Ssrmatching
open Ssrmatching.Internal
(* 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 ()))
}
DECLARE PLUGIN "rocq-runtime.plugins.ssrmatching"
{
let pr_rpattern _ _ _ = pr_rpattern
}
ARGUMENT EXTEND rpattern
TYPED AS rpatternty
PRINTED BY { pr_rpattern }
INTERPRETED BY { interp_rpattern }
GLOBALIZED BY { glob_rpattern }
SUBSTITUTED BY { subst_rpattern }
| [ lconstr(c) ] -> { mk_rpattern (T (mk_lterm c None)) }
| [ "in" lconstr(c) ] -> { mk_rpattern (In_T (mk_lterm c None)) }
| [ lconstr(x) "in" lconstr(c) ] ->
{ mk_rpattern (X_In_T (mk_lterm x None, mk_lterm c None)) }
| [ "in" lconstr(x) "in" lconstr(c) ] ->
{ mk_rpattern (In_X_In_T (mk_lterm x None, mk_lterm c None)) }
| [ lconstr(e) "in" lconstr(x) "in" lconstr(c) ] ->
{ mk_rpattern (E_In_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None)) }
| [ lconstr(e) "as" lconstr(x) "in" lconstr(c) ] ->
{ mk_rpattern (E_As_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None)) }
END
{
let pr_ssrterm _ _ _ = pr_ssrterm
}
ARGUMENT EXTEND cpattern
PRINTED BY { pr_ssrterm }
INTERPRETED BY { interp_ssrterm }
GLOBALIZED BY { glob_cpattern } SUBSTITUTED BY { subst_ssrterm }
RAW_PRINTED BY { pr_ssrterm }
GLOB_PRINTED BY { pr_ssrterm }
| [ "Qed" constr(c) ] -> { mk_lterm c None }
END
{
let input_ssrtermkind kwstate strm = match Gramlib.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 })
}
GRAMMAR EXTEND Gram
GLOBAL: cpattern;
cpattern: TOP [[ k = ssrtermkind; c = constr -> {
let pattern = mk_term k c None in
if loc_of_cpattern pattern <> Some loc && k = InParens
then mk_term Cpattern c None
else pattern } ]];
END
ARGUMENT EXTEND lcpattern
TYPED AS cpattern
PRINTED BY { pr_ssrterm }
INTERPRETED BY { interp_ssrterm }
GLOBALIZED BY { glob_cpattern } SUBSTITUTED BY { subst_ssrterm }
RAW_PRINTED BY { pr_ssrterm }
GLOB_PRINTED BY { pr_ssrterm }
| [ "Qed" lconstr(c) ] -> { mk_lterm c None }
END
GRAMMAR EXTEND Gram
GLOBAL: lcpattern;
lcpattern: TOP [[ k = ssrtermkind; c = lconstr -> {
let pattern = mk_term k c None in
if loc_of_cpattern pattern <> Some loc && k = InParens
then mk_term Cpattern c None
else pattern } ]];
END
ARGUMENT EXTEND ssrpatternarg TYPED AS rpattern PRINTED BY { pr_rpattern }
| [ rpattern(pat) ] -> { pat }
END
TACTIC EXTEND ssrinstoftpat
| [ "ssrinstancesoftpat" cpattern(arg) ] -> { ssrinstancesof arg }
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 () = Mltop.add_init_function "rocq-runtime.plugins.ssreflect" (fun () ->
Procq.unfreeze_only_keywords (Option.get !frozen_lexer);
frozen_lexer := None) ;;
}
[ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
]
|
