(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq 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 warn_deprecated_Spec =
  CWarnings.create ~name:"deprecated-Zify-Spec" ~category:"deprecated"
    (fun () ->
      Pp.strbrk ("Show Zify Spec is deprecated. Use either \"Show Zify BinOpSpec\" or \"Show Zify UnOpSpec\"."))

}

DECLARE PLUGIN "zify_plugin"

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