X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationPp.ml;h=b5a2e04f22a9b9e837ce4694a4d1a6234c815949;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=d51d1a65ec37dd14aaac2cd8307370bda65a7926;hpb=1ca0ec89cfc2c3f85af95d5b1bdad07597d976bd;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index d51d1a65e..b5a2e04f2 100644
--- a/helm/ocaml/cic_notation/cicNotationPp.ml
+++ b/helm/ocaml/cic_notation/cicNotationPp.ml
@@ -32,7 +32,7 @@ module Env = CicNotationEnv
    * be added to the output of pp_term.
    * set to false if you need, for example, cut and paste from matitac output to
    * matitatop *)
-let debug_printing = false
+let debug_printing = true
 
 let pp_binder = function
   | `Lambda -> "lambda"
@@ -40,28 +40,50 @@ let pp_binder = function
   | `Exists -> "exists"
   | `Forall -> "forall"
 
-let pp_literal = function  (* debugging version *)
-  | `Symbol s -> sprintf "symbol(%s)" s
-  | `Keyword s -> sprintf "keyword(%s)" s
-  | `Number s -> sprintf "number(%s)" s
+let pp_literal =
+  if debug_printing then
+    (function (* debugging version *)
+      | `Symbol s -> sprintf "symbol(%s)" s
+      | `Keyword s -> sprintf "keyword(%s)" s
+      | `Number s -> sprintf "number(%s)" s)
+  else
+    (function
+      | `Symbol s
+      | `Keyword s
+      | `Number s -> s)
 
-(* let pp_literal = function
-  | `Symbol s
-  | `Keyword s
-  | `Number s -> s *)
+let pp_assoc =
+  function
+  | Gramext.NonA -> "NonA"
+  | Gramext.LeftA -> "LeftA"
+  | Gramext.RightA -> "RightA"
+
+let pp_pos =
+  function
+(*      `None -> "`None" *)
+    | `Left -> "`Left"
+    | `Right -> "`Right"
+    | `Inner -> "`Inner"
+
+let pp_attribute =
+  function
+  | `IdRef id -> sprintf "x(%s)" id
+  | `XmlAttrs attrs ->
+      sprintf "X(%s)"
+        (String.concat ";"
+          (List.map (fun (_, n, v) -> sprintf "%s=%s" n v) attrs))
+  | `Level (prec, assoc) -> sprintf "L(%d%s)" prec (pp_assoc assoc)
+  | `Raw _ -> "R"
+  | `Loc _ -> "@"
+  | `ChildPos p -> sprintf "P(%s)" (pp_pos p)
 
 let rec pp_term ?(pp_parens = true) t =
   let t_pp =
     match t with
-    | Ast.AttributedTerm (`Href _, term) when debug_printing ->
-        sprintf "#[%s]" (pp_term ~pp_parens:false term)
-    | Ast.AttributedTerm (`IdRef id, term) when debug_printing ->
-        sprintf "x(%s)[%s]" id (pp_term ~pp_parens:false term)
-    | Ast.AttributedTerm (_, term) when debug_printing ->
-        sprintf "@[%s]" (pp_term ~pp_parens:false term)
+    | Ast.AttributedTerm (attr, term) when debug_printing ->
+        sprintf "%s[%s]" (pp_attribute attr) (pp_term ~pp_parens:false term)
     | Ast.AttributedTerm (`Raw text, _) -> text
     | Ast.AttributedTerm (_, term) -> pp_term ~pp_parens:false term
-
     | Ast.Appl terms ->
         sprintf "%s" (String.concat " " (List.map pp_term terms))
     | Ast.Binder (`Forall, (Ast.Ident ("_", None), typ), body)
@@ -73,9 +95,18 @@ let rec pp_term ?(pp_parens = true) t =
         sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable var)
           (pp_term body)
     | Ast.Case (term, indtype, typ, patterns) ->
-        sprintf "%smatch %s with %s"
+        sprintf "%smatch %s%s with %s"
           (match typ with None -> "" | Some t -> sprintf "[%s]" (pp_term t))
-          (pp_term term) (pp_patterns patterns)
+          (pp_term term)
+          (match indtype with
+          | None -> ""
+          | Some (ty, href_opt) ->
+              sprintf " in %s%s" ty
+              (match debug_printing, href_opt with
+              | true, Some uri ->
+                  sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
+              | _ -> ""))
+          (pp_patterns patterns)
     | Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term t1) (pp_term t2)
     | Ast.LetIn (var, t1, t2) ->
         sprintf "let %s = %s in %s" (pp_capture_variable var) (pp_term t1)
@@ -103,7 +134,7 @@ let rec pp_term ?(pp_parens = true) t =
     | Ast.Num (num, _) -> num
     | Ast.Sort `Set -> "Set"
     | Ast.Sort `Prop -> "Prop"
-    | Ast.Sort `Type -> "Type"
+    | Ast.Sort (`Type _) -> "Type"
     | Ast.Sort `CProp -> "CProp"
     | Ast.Symbol (name, _) -> "'" ^ name
 
@@ -120,12 +151,18 @@ let rec pp_term ?(pp_parens = true) t =
 and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term)
 and pp_substs substs = String.concat "; " (List.map pp_subst substs)
 
-and pp_pattern ((head, vars), term) =
+and pp_pattern ((head, href, vars), term) =
+  let head_pp =
+    head ^
+    (match debug_printing, href with
+    | true, Some uri -> sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
+    | _ -> "")
+  in
   sprintf "%s \\Rightarrow %s"
     (match vars with
-    | [] -> head
+    | [] -> head_pp
     | _ ->
-        sprintf "(%s %s)" head
+        sprintf "(%s %s)" head_pp
           (String.concat " " (List.map pp_capture_variable vars)))
     (pp_term term)