diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/micromega/g_zify.mlg | 50 | ||||
| -rw-r--r-- | plugins/micromega/zify.ml | 13 |
2 files changed, 44 insertions, 19 deletions
diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg index 80a40c4315..0e5cac2d4a 100644 --- a/plugins/micromega/g_zify.mlg +++ b/plugins/micromega/g_zify.mlg @@ -14,23 +14,44 @@ 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\".")) + +let warn_deprecated_Add = + CWarnings.create ~name:"deprecated-Zify-Add" ~category:"deprecated" + (fun () -> + Pp.strbrk ("Add <X> is deprecated. Use instead Add Zify <X>.")) + } DECLARE PLUGIN "zify_plugin" VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF -| ["Add" "InjTyp" constr(t) ] -> { Zify.InjTable.register t } -| ["Add" "BinOp" constr(t) ] -> { Zify.BinOp.register t } -| ["Add" "UnOp" constr(t) ] -> { Zify.UnOp.register t } -| ["Add" "CstOp" constr(t) ] -> { Zify.CstOp.register t } -| ["Add" "BinRel" constr(t) ] -> { Zify.BinRel.register t } -| ["Add" "PropOp" constr(t) ] -> { Zify.PropBinOp.register t } -| ["Add" "PropBinOp" constr(t) ] -> { Zify.PropBinOp.register t } -| ["Add" "PropUOp" constr(t) ] -> { Zify.PropUnOp.register t } -| ["Add" "BinOpSpec" constr(t) ] -> { Zify.BinOpSpec.register t } -| ["Add" "UnOpSpec" constr(t) ] -> { Zify.UnOpSpec.register t } -| ["Add" "Saturate" constr(t) ] -> { Zify.Saturate.register t } +| ["Add" "Zify" "InjTyp" constr(t) ] -> { Zify.InjTable.register t } +| ["Add" "Zify" "BinOp" constr(t) ] -> { Zify.BinOp.register t } +| ["Add" "Zify" "UnOp" constr(t) ] -> { Zify.UnOp.register t } +| ["Add" "Zify" "CstOp" constr(t) ] -> { Zify.CstOp.register t } +| ["Add" "Zify" "BinRel" constr(t) ] -> { Zify.BinRel.register t } +| ["Add" "Zify" "PropOp" constr(t) ] -> { Zify.PropBinOp.register t } +| ["Add" "Zify" "PropBinOp" constr(t) ] -> { Zify.PropBinOp.register t } +| ["Add" "Zify" "PropUOp" constr(t) ] -> { Zify.PropUnOp.register t } +| ["Add" "Zify" "BinOpSpec" constr(t) ] -> { Zify.BinOpSpec.register t } +| ["Add" "Zify" "UnOpSpec" constr(t) ] -> { Zify.UnOpSpec.register t } +| ["Add" "Zify" "Saturate" constr(t) ] -> { Zify.Saturate.register t } +| ["Add" "InjTyp" constr(t) ] -> { warn_deprecated_Add (); Zify.InjTable.register t } +| ["Add" "BinOp" constr(t) ] -> { warn_deprecated_Add (); Zify.BinOp.register t } +| ["Add" "UnOp" constr(t) ] -> { warn_deprecated_Add (); Zify.UnOp.register t } +| ["Add" "CstOp" constr(t) ] -> { warn_deprecated_Add (); Zify.CstOp.register t } +| ["Add" "BinRel" constr(t) ] -> { warn_deprecated_Add (); Zify.BinRel.register t } +| ["Add" "PropOp" constr(t) ] -> { warn_deprecated_Add (); Zify.PropBinOp.register t } +| ["Add" "PropBinOp" constr(t) ] -> { warn_deprecated_Add (); Zify.PropBinOp.register t } +| ["Add" "PropUOp" constr(t) ] -> { warn_deprecated_Add (); Zify.PropUnOp.register t } +| ["Add" "BinOpSpec" constr(t) ] -> { warn_deprecated_Add (); Zify.BinOpSpec.register t } +| ["Add" "UnOpSpec" constr(t) ] -> { warn_deprecated_Add (); Zify.UnOpSpec.register t } +| ["Add" "Saturate" constr(t) ] -> { warn_deprecated_Add (); Zify.Saturate.register t } END TACTIC EXTEND ITER @@ -50,6 +71,9 @@ VERNAC COMMAND EXTEND ZifyPrint CLASSIFIED AS SIDEFF |[ "Show" "Zify" "UnOp" ] -> { Zify.UnOp.print () } |[ "Show" "Zify" "CstOp"] -> { Zify.CstOp.print () } |[ "Show" "Zify" "BinRel"] -> { Zify.BinRel.print () } -|[ "Show" "Zify" "Spec"] -> { (* This prints both UnOpSpec and BinOpSpec *) - Zify.UnOpSpec.print() } +|[ "Show" "Zify" "UnOpSpec"] -> { Zify.UnOpSpec.print() } +|[ "Show" "Zify" "BinOpSpec"] -> { Zify.BinOpSpec.print() } +|[ "Show" "Zify" "Spec"] -> { + warn_deprecated_Spec () ; + Zify.UnOpSpec.print() ; Zify.BinOpSpec.print ()} END diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index ec0f278326..4e1f9a66ac 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -320,7 +320,8 @@ type decl_kind = | UnOp of EUnOpT.t decl | CstOp of ECstOpT.t decl | Saturate of ESatT.t decl - | Spec of ESpecT.t decl + | UnOpSpec of ESpecT.t decl + | BinOpSpec of ESpecT.t decl type term_kind = Application of EConstr.constr | OtherTerm of EConstr.constr @@ -664,8 +665,8 @@ module EUnopSpec = struct let name = "UnopSpec" let table = specs - let cast x = Spec x - let dest = function Spec x -> Some x | _ -> None + let cast x = UnOpSpec x + let dest = function UnOpSpec x -> Some x | _ -> None let mk_elt evd i a = {spec = a.(4)} let get_key = 2 end @@ -677,8 +678,8 @@ module EBinOpSpec = struct let name = "BinOpSpec" let table = specs - let cast x = Spec x - let dest = function Spec x -> Some x | _ -> None + let cast x = BinOpSpec x + let dest = function BinOpSpec x -> Some x | _ -> None let mk_elt evd i a = {spec = a.(5)} let get_key = 3 end @@ -1419,7 +1420,7 @@ let rec spec_of_term env evd (senv : spec_env) t = with Not_found -> ( try match snd (HConstr.find c !specs_cache) with - | Spec s -> + | UnOpSpec s | BinOpSpec s -> let thm = EConstr.mkApp (s.deriv.ESpecT.spec, a') in register_constr senv' t' thm | _ -> (get_name t' senv', senv') |