From 007baa025031b1decf87b811358b3c2154ee5da4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 13 Apr 2016 16:10:09 +0200 Subject: Adding printers for ring and field commands. --- plugins/setoid_ring/g_newring.ml4 | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) (limited to 'plugins/setoid_ring') diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index f64226e33..767cf7ab7 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -33,7 +33,25 @@ TACTIC EXTEND closed_term [ Proofview.V82.tactic (closed_term t l) ] END +open Pptactic +open Ppconstr + +let pr_ring_mod = function + | Ring_kind (Computational eq_test) -> str "decidable" ++ pr_arg pr_constr_expr eq_test + | Ring_kind Abstract -> str "abstract" + | Ring_kind (Morphism morph) -> str "morphism" ++ pr_arg pr_constr_expr morph + | Const_tac (CstTac cst_tac) -> str "constants" ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]" + | Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_reference l ++ str "]" + | Pre_tac t -> str "preprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]" + | Post_tac t -> str "postprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]" + | Setoid(sth,ext) -> str "setoid" ++ pr_arg pr_constr_expr sth ++ pr_arg pr_constr_expr ext + | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_reference l ++ str "]" + | Pow_spec(CstTac cst_tac,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]" + | Sign_spec t -> str "sign" ++ pr_arg pr_constr_expr t + | Div_spec t -> str "div" ++ pr_arg pr_constr_expr t + VERNAC ARGUMENT EXTEND ring_mod + PRINTED BY pr_ring_mod | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational eq_test) ] | [ "abstract" ] -> [ Ring_kind Abstract ] | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism morph) ] @@ -50,7 +68,10 @@ VERNAC ARGUMENT EXTEND ring_mod | [ "div" constr(div_spec) ] -> [ Div_spec div_spec ] END +let pr_ring_mods l = surround (prlist_with_sep pr_comma pr_ring_mod l) + VERNAC ARGUMENT EXTEND ring_mods + PRINTED BY pr_ring_mods | [ "(" ne_ring_mod_list_sep(mods, ",") ")" ] -> [ mods ] END @@ -74,12 +95,20 @@ TACTIC EXTEND ring_lookup [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t] END +let pr_field_mod = function + | Ring_mod m -> pr_ring_mod m + | Inject inj -> str "completeness" ++ pr_arg pr_constr_expr inj + VERNAC ARGUMENT EXTEND field_mod + PRINTED BY pr_field_mod | [ ring_mod(m) ] -> [ Ring_mod m ] | [ "completeness" constr(inj) ] -> [ Inject inj ] END +let pr_field_mods l = surround (prlist_with_sep pr_comma pr_field_mod l) + VERNAC ARGUMENT EXTEND field_mods + PRINTED BY pr_field_mods | [ "(" ne_field_mod_list_sep(mods, ",") ")" ] -> [ mods ] END -- cgit v1.2.3