more fine grained debug printing

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index 0bda688469725924a983aa1ecce547ffa9181c94..4183d003feb9bd8e366ea27e06d20df4b8c05e5f 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationPp.ml
+++ b/helm/ocaml/cic_notation/cicNotationPp.ml
@@ -52,6 +52,12 @@ let pp_literal =
       | `Keyword s
       | `Number s -> s)
 
+let pp_assoc =
+  function
+  | Gramext.NonA -> "N"
+  | Gramext.LeftA -> "L"
+  | Gramext.RightA -> "R"
+
 let rec pp_term ?(pp_parens = true) t =
   let t_pp =
     match t with
@@ -62,8 +68,14 @@ let rec pp_term ?(pp_parens = true) t =
           (String.concat ";"
             (List.map (fun (_, n, v) -> sprintf "%s=%s" n v) attrs))
           (pp_term ~pp_parens:false term)
-    | Ast.AttributedTerm (_, term) when debug_printing ->
+    | Ast.AttributedTerm (`Level (prec, assoc), term) when debug_printing ->
+        sprintf "L(%d%s)[%s]" prec (pp_assoc assoc)
+          (pp_term ~pp_parens:false term)
+    | Ast.AttributedTerm (`Raw _, term) when debug_printing ->
+        sprintf "R[%s]" (pp_term ~pp_parens:false term)
+    | Ast.AttributedTerm (`Loc _, term) when debug_printing ->
         sprintf "@[%s]" (pp_term ~pp_parens:false term)
+
     | Ast.AttributedTerm (`Raw text, _) -> text
     | Ast.AttributedTerm (_, term) -> pp_term ~pp_parens:false term