Quelle  g_zify.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)         *)
(************************************************************************)

{

open Ltac_plugin
open Stdarg
open Tacarg

let locality = Zify.zify_register_locality

}

DECLARE PLUGIN "rocq-runtime.plugins.zify"

VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF
| #[ locality ] ["Add" "Zify" "InjTyp"   reference(t) ] -> { Zify.InjTable.register locality t }
| #[ locality ] ["Add" "Zify" "BinOp"     reference(t) ] -> { Zify.BinOp.register locality t }
| #[ locality ] ["Add" "Zify" "UnOp"      reference(t) ] -> { Zify.UnOp.register locality t }
| #[ locality ] ["Add" "Zify" "CstOp"     reference(t) ] -> { Zify.CstOp.register locality t }
| #[ locality ] ["Add" "Zify" "BinRel"    reference(t) ] -> { Zify.BinRel.register locality t }
| #[ locality ] ["Add" "Zify" "PropOp"    reference(t) ] -> { Zify.PropBinOp.register locality t }
| #[ locality ] ["Add" "Zify" "PropBinOp"    reference(t) ] -> { Zify.PropBinOp.register locality t }
| #[ locality ] ["Add" "Zify" "PropUOp"   reference(t) ] -> { Zify.PropUnOp.register locality t }
| #[ locality ] ["Add" "Zify" "BinOpSpec" reference(t) ] -> { Zify.BinOpSpec.register locality t }
| #[ locality ] ["Add" "Zify" "UnOpSpec"  reference(t) ] -> { Zify.UnOpSpec.register locality t }
| #[ locality ] ["Add" "Zify" "Saturate"  reference(t) ] -> { Zify.Saturate.register locality t }
END

TACTIC EXTEND ITER
| [ "zify_iter_specs"] -> { Zify.iter_specs}
END

TACTIC EXTEND TRANS
| [ "zify_op"  ] -> { Zify.zify_tac }
| [ "zify_saturate"  ] -> { Zify.saturate }
| [ "zify_iter_let" tactic(t)] -> { Zify.iter_let t }
| [ "zify_elim_let" ] -> { Zify.elim_let }
END

VERNAC COMMAND EXTEND ZifyPrint CLASSIFIED AS SIDEFF
|[ "Show" "Zify" "InjTyp" ] -> { Zify.InjTable.print () }
|[ "Show" "Zify" "BinOp" ]  -> { Zify.BinOp.print () }
|[ "Show" "Zify" "UnOp" ]   -> { Zify.UnOp.print () }
|[ "Show" "Zify" "CstOp"]   -> { Zify.CstOp.print () }
|[ "Show" "Zify" "BinRel"]  -> { Zify.BinRel.print () }
|[ "Show" "Zify" "UnOpSpec"] -> { Zify.UnOpSpec.print() }
|[ "Show" "Zify" "BinOpSpec"] -> { Zify.BinOpSpec.print() }
END