]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_content/cicNotationPp.ml
initial support for notation that specifies the precedence of term variables, that...
[helm.git] / helm / software / components / acic_content / cicNotationPp.ml
index 6ea839ce322afff694ad1af077b2253a31730aba..7fbc9f492225c1db508e1241c73eddcf81e6f07c 100644 (file)
@@ -56,9 +56,9 @@ let pp_literal =
 
 let pp_assoc =
   function
-  | Gramext.NonA -> "NonA"
-  | Gramext.LeftA -> "LeftA"
-  | Gramext.RightA -> "RightA"
+  | Gramext.NonA -> "N"
+  | Gramext.LeftA -> "L"
+  | Gramext.RightA -> "R"
 
 let pp_pos =
   function
@@ -256,7 +256,8 @@ and pp_sep_opt = function
 and pp_variable = function
   | Ast.NumVar s -> "number " ^ s
   | Ast.IdentVar s -> "ident " ^ s
-  | Ast.TermVar s -> "term " ^ s
+  | Ast.TermVar (s,None) -> s
+  | Ast.TermVar (s,Some (l,a)) -> "term " ^string_of_int l ^ " " ^ pp_assoc a ^ " " ^ s
   | Ast.Ascription (t, n) -> assert false
   | Ast.FreshVar n -> "fresh " ^ n
 
@@ -333,7 +334,8 @@ let rec pp_value = function
 
 let rec pp_value_type =
   function
-  | Env.TermType -> "Term"
+  | Env.TermType None -> "Term"
+  | Env.TermType (Some (l,a)) -> "Term "^string_of_int l ^ " " ^ pp_assoc a 
   | Env.StringType -> "String"
   | Env.NumType -> "Number"
   | Env.OptType t -> "Maybe " ^ pp_value_type t