X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationPp.ml;h=fcb42fd1853a869264b9599faf80aa45d98d240e;hb=619a3a478a4f6b0a50782b620009f6a141c30a53;hp=4f79895164af5ff92e9dcdc16e3f95557cb40a19;hpb=dbcc29c0e46454c7e31b485135900ceab38627e1;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index 4f7989516..fcb42fd18 100644
--- a/helm/ocaml/cic_notation/cicNotationPp.ml
+++ b/helm/ocaml/cic_notation/cicNotationPp.ml
@@ -36,14 +36,14 @@ let pp_binder = function
   | `Exists -> "exists"
   | `Forall -> "forall"
 
-let pp_literal l =
-  sprintf "literal(%s)"
-    (match l with
-    | `Symbol s
-    | `Keyword s
-    | `Number s -> s)
+let pp_literal = function
+  | `Symbol s -> sprintf "symbol(%s)" s
+  | `Keyword s -> sprintf "keyword(%s)" s
+  | `Number s -> sprintf "number(%s)" s
 
 let rec pp_term = function
+  | AttributedTerm (`Href _, term) when print_attributes ->
+      sprintf "#[%s]" (pp_term term)
   | AttributedTerm (_, term) when print_attributes ->
       sprintf "@[%s]" (pp_term term)
   | AttributedTerm (_, term) -> pp_term term
@@ -118,6 +118,13 @@ and pp_capture_variable = function
   | term, None -> pp_term term
   | term, Some typ -> "(" ^ pp_term term ^ ": " ^ pp_term typ ^ ")"
 
+and pp_box_spec (kind, spacing, indent) =
+  let int_of_bool b = if b then 1 else 0 in
+  let kind_string =
+    match kind with H -> "H" | V -> "V" | HV -> "HV" | HOV -> "HOV"
+  in
+  sprintf "%sBOX%d%d" kind_string (int_of_bool spacing) (int_of_bool indent)
+
 and pp_layout = function
   | Sub (t1, t2) -> sprintf "%s \\SUB %s" (pp_term t1) (pp_term t2)
   | Sup (t1, t2) -> sprintf "%s \\SUP %s" (pp_term t1) (pp_term t2)
@@ -130,16 +137,33 @@ and pp_layout = function
   | Root (arg, index) ->
       sprintf "\\ROOT %s \\OF %s" (pp_term index) (pp_term arg)
   | Break -> "\\BREAK"
-  | Box (H, terms) ->
-      sprintf "\\HBOX [%s]" (String.concat " " (List.map pp_term terms))
-  | Box (V, terms) ->
-      sprintf "\\VBOX [%s]" (String.concat " " (List.map pp_term terms))
+(*   | Space -> "\\SPACE" *)
+  | Box (box_spec, terms) ->
+      sprintf "\\%s [%s]" (pp_box_spec box_spec)
+        (String.concat " " (List.map pp_term terms))
+  | Group terms ->
+      sprintf "\\GROUP [%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)
+  | If (p_test, p_true, p_false) ->
+      sprintf "\\IF \\[%s\\] \\[%s\\] \\[%s\\]"
+	(pp_term p_test) (pp_term p_true) (pp_term p_false)
+  | Fail -> "\\FAIL"
+
+and pp_fold_kind = function
+  | `Left -> "left"
+  | `Right -> "right"
 
 and pp_sep_opt = function
   | None -> ""