diff options
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 46 |
1 files changed, 28 insertions, 18 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index b6e4c8011c..f3117db170 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -9,7 +9,7 @@ open Pp open Names open Namegen -open Errors +open CErrors open Util open Constrexpr open Tacexpr @@ -151,7 +151,8 @@ module Make exception ComplexRedFlag let pr_short_red_flag pr r = - if not r.rBeta || not r.rIota || not r.rZeta then raise ComplexRedFlag + if not r.rBeta || not r.rMatch || not r.rFix || not r.rCofix || not r.rZeta then + raise ComplexRedFlag else if List.is_empty r.rConst then if r.rDelta then mt () else raise ComplexRedFlag else (if r.rDelta then str "-" else mt ()) ++ @@ -161,9 +162,12 @@ module Make try pr_short_red_flag pr r with complexRedFlags -> (if r.rBeta then pr_arg str "beta" else mt ()) ++ - (if r.rIota then pr_arg str "iota" else mt ()) ++ - (if r.rZeta then pr_arg str "zeta" else mt ()) ++ - (if List.is_empty r.rConst then + (if r.rMatch && r.rFix && r.rCofix then pr_arg str "iota" else + (if r.rMatch then pr_arg str "match" else mt ()) ++ + (if r.rFix then pr_arg str "fix" else mt ()) ++ + (if r.rCofix then pr_arg str "cofix" else mt ())) ++ + (if r.rZeta then pr_arg str "zeta" else mt ()) ++ + (if List.is_empty r.rConst then if r.rDelta then pr_arg str "delta" else mt () else @@ -180,7 +184,8 @@ module Make | Simpl (f,o) -> keyword "simpl" ++ (pr_short_red_flag pr_ref f) ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o | Cbv f -> - if f.rBeta && f.rIota && f.rZeta && f.rDelta && List.is_empty f.rConst then + if f.rBeta && f.rMatch && f.rFix && f.rCofix && + f.rZeta && f.rDelta && List.is_empty f.rConst then keyword "compute" else hov 1 (keyword "cbv" ++ pr_red_flag pr_ref f) @@ -368,20 +373,25 @@ module Make in str "<" ++ name ++ str ">" ++ args + let rec pr_user_symbol = function + | Extend.Ulist1 tkn -> "ne_" ^ pr_user_symbol tkn ^ "_list" + | Extend.Ulist1sep (tkn, _) -> "ne_" ^ pr_user_symbol tkn ^ "_list" + | Extend.Ulist0 tkn -> pr_user_symbol tkn ^ "_list" + | Extend.Ulist0sep (tkn, _) -> pr_user_symbol tkn ^ "_list" + | Extend.Uopt tkn -> pr_user_symbol tkn ^ "_opt" + | Extend.Uentry tag -> + let ArgT.Any tag = tag in + ArgT.repr tag + | Extend.Uentryl (tkn, lvl) -> "tactic" ^ string_of_int lvl + let pr_alias_key key = try let prods = (KNmap.find key !prnotation_tab).pptac_prods in - (* First printing strategy: only the head symbol *) - match prods with - | TacTerm s :: prods -> str s - | _ -> - (* Second printing strategy; if ever Tactic Notation is eventually *) - (* accepting notations not starting with an identifier *) let rec pr = function - | [] -> [] - | TacTerm s :: prods -> s :: pr prods - | TacNonTerm (_,_,id) :: prods -> ".." :: pr prods in - str (String.concat " " (pr prods)) + | TacTerm s -> primitive s + | TacNonTerm (_, symb, _) -> str (Printf.sprintf "(%s)" (pr_user_symbol symb)) + in + pr_sequence pr prods with Not_found -> KerName.print key @@ -792,7 +802,7 @@ module Make let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in - let pr_constrarg c = spc () ++ pr.pr_constr c in + let _pr_constrarg c = spc () ++ pr.pr_constr c in let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in let pr_intarg n = spc () ++ int n in @@ -840,7 +850,7 @@ module Make prlist pr_binder_fix bll ++ annot ++ str" :" ++ pr_lconstrarg ty ++ str")") in (* spc() ++ - hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg + hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ _pr_constrarg c) *) let pr_cofix_tac (id,c) = |