Quelle g_ssrmatching.mlg Sprache: unbekannt

(************************************************************************)
(*         *      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) ;;

}

Quelle g_ssrmatching.mlg Sprache: unbekannt

[ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ]