X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent%2FnotationPp.ml;h=a69ca90abe27206bc7dfbac121d3e6b73f1b03e2;hb=647504aa72b84eb49be8177b88a9254174e84d4b;hp=99255465d0fdcff99268d365ad64e274adac50b7;hpb=a2412e41cda18a25d780ae631ee02d6ae05c52b1;p=helm.git

diff --git a/matitaB/components/content/notationPp.ml b/matitaB/components/content/notationPp.ml
index 99255465d..a69ca90ab 100644
--- a/matitaB/components/content/notationPp.ml
+++ b/matitaB/components/content/notationPp.ml
@@ -42,17 +42,17 @@ let pp_binder = function
   | `Exists -> "exists"
   | `Forall -> "forall"
 
-let pp_literal =
+(* XXX: ignoring the optional CSYMBOL
+ * (it's fine if this is only used for pretty printing output notations) *)
+let pp_literal (_,t) =
   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)
+    (match t with (* debugging version *)
+      | `Symbol _ -> 
+          sprintf "symbol(%s)" (NotationUtil.string_of_literal t)
+      | `Keyword _ -> 
+          sprintf "keyword(%s)" (NotationUtil.string_of_literal t)
+      | `Number _ -> sprintf "number(%s)" (NotationUtil.string_of_literal t))
+  else NotationUtil.string_of_literal t
 
 let pp_pos =
   function
@@ -70,7 +70,8 @@ let pp_attribute =
           (List.map (fun (_, n, v) -> sprintf "%s=%s" n v) attrs))
   | `Level (prec) -> sprintf "L(%d)" prec 
   | `Raw _ -> "R"
-  | `Loc _ -> "@"
+  | `Loc l -> let x,y = HExtlib.loc_of_floc l in 
+              "@" ^ (string_of_int x) ^ "," ^ (string_of_int y)
   | `ChildPos p -> sprintf "P(%s)" (pp_pos p)
 
 let pp_capture_variable pp_term = 
@@ -79,6 +80,7 @@ let pp_capture_variable pp_term =
   | term, Some typ -> "(" ^ pp_term (* ~pp_parens:false *) term ^ ": " ^ pp_term typ ^ ")"
 
 let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
+ let debug_printing = true in
   let pp_ident = function
   | Ast.Ident (id,`Ambiguous) -> "A:" ^ id
   | Ast.Ident (id,`Rel) -> "R:" ^ id
@@ -90,7 +92,7 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
     match t with
     | 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 (`Raw text, t) -> "RAW:(" ^ (pp_term t) ^ ")"
     | Ast.AttributedTerm (_, term) -> pp_term ~pp_parens:false term
     | Ast.Appl terms ->
         sprintf "%s" (String.concat " " (List.map pp_term terms))
@@ -114,7 +116,7 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
           | None -> ""
           | Some (ty, href_opt) ->
               sprintf " in %s%s" ty
-              (match debug_printing, href_opt with
+              (match (*debug_printing*) true, href_opt with
               | true, Some uri ->
                   sprintf "(i.e.%s)" (NReference.string_of_reference uri)
               | _ -> ""))	  
@@ -164,14 +166,15 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
     | Ast.Sort `Prop -> "Prop"
     | Ast.Sort (`NType s)-> "Type[" ^ s ^ "]"
     | Ast.Sort (`NCProp s)-> "CProp[" ^ s ^ "]"
-    | Ast.Symbol (name, _) -> "'" ^ name
+    | Ast.Symbol (name, None) -> "'" ^ name
+    | Ast.Symbol (name, Some (_,desc)) -> "'" ^ name ^ ":" ^ desc
 
     | Ast.UserInput -> "%"
 
-    | Ast.Literal l -> pp_literal l
-    | Ast.Layout l -> pp_layout status l
-    | Ast.Magic m -> pp_magic status m
-    | Ast.Variable v -> pp_variable v
+    | Ast.Literal l -> "literal:(" ^ (pp_literal l) ^ ")"
+    | Ast.Layout l -> "layout:(" ^ (pp_layout status l) ^ ")"
+    | Ast.Magic m -> "magic:(" ^ (pp_magic status m) ^ ")"
+    | Ast.Variable v -> "variable:" ^ (pp_variable v)
   in
   match pp_parens, t with
     | false, _ 
@@ -181,17 +184,14 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
     | true, Ast.Ident _    -> t_pp
     | _                    -> sprintf "(%s)" t_pp
 
-and pp_subst status (name, term) =
- sprintf "%s \\Assign %s" name (pp_term status term)
-and pp_substs status substs = String.concat "; " (List.map (pp_subst status) substs)
-
 and pp_pattern status =
  function
     Ast.Pattern (head, href, vars), term ->
      let head_pp =
        head ^
-       (match debug_printing, href with
+       (match (*debug_printing*)true, href with
        | true, Some uri -> sprintf "(i.e.%s)" (NReference.string_of_reference uri)
+       | true, None -> "(i.e.ambiguous)"
        | _ -> "")
      in
      sprintf "%s \\Rightarrow %s"
@@ -273,7 +273,7 @@ and pp_fold_kind = function
 
 and pp_sep_opt = function
   | None -> ""
-  | Some sep -> sprintf " sep %s" (pp_literal sep)
+  | Some sep -> sprintf " sep %s" (pp_literal (None,sep))
 
 and pp_variable = function
   | Ast.NumVar s -> "number " ^ s
@@ -343,6 +343,7 @@ let rec pp_value (status: #NCic.status) = function
   | Env.OptValue (Some v) -> "Some " ^ pp_value status v
   | Env.OptValue None -> "None"
   | Env.ListValue l -> sprintf "[%s]" (String.concat "; " (List.map (pp_value status) l))
+  | Env.DisambiguationValue _ -> sprintf "#"
 
 let rec pp_value_type =
   function
@@ -351,6 +352,7 @@ let rec pp_value_type =
   | Env.NumType -> "Number"
   | Env.OptType t -> "Maybe " ^ pp_value_type t
   | Env.ListType l -> "List " ^ pp_value_type l
+  | Env.NoType -> "NoType"
 
 let pp_env status env =
   String.concat "; "