X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_notation%2FcicNotationPp.ml;h=bc9f33f51963bacd821efb8e6e130844925f26c4;hb=e9e3089b886e88a07267743cae79d6a9cabdd3c3;hp=5befd8ed2787d745ab125d3cf71943c958ab7ab9;hpb=9230a8085102cd39258c047949e87001be6ffcf0;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index 5befd8ed2..bc9f33f51 100644
--- a/helm/ocaml/cic_notation/cicNotationPp.ml
+++ b/helm/ocaml/cic_notation/cicNotationPp.ml
@@ -28,6 +28,8 @@ open Printf
 open CicNotationEnv
 open CicNotationPt
 
+let print_attributes = true
+
 let pp_binder = function
   | `Lambda -> "lambda"
   | `Pi -> "Pi"
@@ -42,6 +44,8 @@ let pp_literal l =
     | `Number s -> s)
 
 let rec pp_term = function
+  | AttributedTerm (_, term) when print_attributes ->
+      sprintf "@[%s]" (pp_term term)
   | AttributedTerm (_, term) -> pp_term term
 
   | Appl terms ->
@@ -132,10 +136,21 @@ and pp_layout = function
       sprintf "\\VBOX [%s]" (String.concat " " (List.map pp_term terms))
 
 and pp_magic = function
-  | List0 (t, sep_opt) -> sprintf "\\LIST0 %s%s" (pp_term t) (pp_sep_opt sep_opt)
-  | List1 (t, sep_opt) -> sprintf "\\LIST1 %s%s" (pp_term t) (pp_sep_opt sep_opt)
+  | List0 (t, sep_opt) ->
+      sprintf "\\LIST0 %s%s" (pp_term t) (pp_sep_opt sep_opt)
+  | List1 (t, sep_opt) ->
+      sprintf "\\LIST1 %s%s" (pp_term t) (pp_sep_opt sep_opt)
   | Opt t -> sprintf "\\OPT %s" (pp_term t)
-  | _ -> failwith "magic not implemented"
+  | Fold (k, p_base, names, p_rec) ->
+      let acc = match names with acc :: _ -> acc | _ -> assert false in
+      sprintf "\\FOLD %s \\[%s\\] \\LAMBDA %s \\[%s\\]"
+        (pp_fold_kind k) (pp_term p_base) acc (pp_term p_rec)
+  | Default (p_some, p_none) ->
+      sprintf "\\DEFAULT \\[%s\\] \\[%s\\]" (pp_term p_some) (pp_term p_none)
+
+and pp_fold_kind = function
+  | `Left -> "left"
+  | `Right -> "right"
 
 and pp_sep_opt = function
   | None -> ""