Add support for precedence and associativity in driver symbols

src/driver/driver_ast.ml

@@ -42,11 +42,13 @@ type theory_rules = {
   thr_rules : (loc * th_rule) list;
 }
 
+type assoc_dir = Left | Right
+                      
 type mo_rule =
   | MRtheory    of th_rule
   | MRinterface of string
   | MRexception of qualid * string
-  | MRval       of qualid * string
+  | MRval       of qualid * string * int option * assoc_dir option
 
 type module_rules = {
   mor_name  : qualid;

src/driver/driver_lexer.mll

@@ -46,6 +46,10 @@
         "transformation", TRANSFORM;
         "plugin", PLUGIN;
         "blacklist", BLACKLIST;
+        "prec", PREC;
+        "assoc", ASSOC;
+        "left", LEFT;
+        "right", RIGHT;
         (* WhyML *)
         "module", MODULE;
         "exception", EXCEPTION;

src/driver/driver_parser.mly

@@ -11,7 +11,6 @@
 
 %{
   open Driver_ast
-
 %}
 
 %token <int> INTEGER
@@ -31,6 +30,7 @@
 %token FUNCTION PREDICATE TYPE PROP ALL FILENAME TRANSFORM PLUGIN
 %token COMMA CONSTANT
 %token LEFTSQ RIGHTSQ LARROW
+%token PREC ASSOC LEFT RIGHT
 
 %nonassoc SYNTAX REMOVE PRELUDE INTERFACE
 %nonassoc prec_pty
@@ -211,6 +211,14 @@ mrule:
 | trule                          { MRtheory $1 }
 | INTERFACE STRING               { MRinterface ($2) }
 | SYNTAX EXCEPTION qualid STRING { MRexception ($3, $4) }
-| SYNTAX VAL qualid STRING       { MRval ($3, $4) }
+| SYNTAX VAL qualid STRING precedence? associativity?
+                                 { MRval ($3, $4, $5, $6) }
+
+precedence:
+| PREC INTEGER { $2 }
+
+associativity:
+| ASSOC LEFT  { Left }
+| ASSOC RIGHT { Right }
 
 loc(X): X { Loc.extract ($startpos,$endpos), $1 }

src/mlw/pdriver.ml

@@ -28,6 +28,8 @@ type driver = {
   drv_blacklist   : Printer.blacklist;
   drv_syntax      : Printer.syntax_map;
   drv_literal     : Printer.syntax_map;
+  drv_prec        : (int option) Mid.t;
+  drv_assoc       : (assoc_dir option) Mid.t;
 }
 
 type printer_args = {
@@ -38,6 +40,8 @@ type printer_args = {
   blacklist   : Printer.blacklist;
   syntax      : Printer.syntax_map;
   literal     : Printer.syntax_map;
+  prec        : (int option) Mid.t;
+  assoc       : (assoc_dir option) Mid.t;
 }
 
 let load_file file =
@@ -88,6 +92,8 @@ let load_driver env file extra_files =
   let thinterface = ref Mid.empty in
   let syntax_map = ref Mid.empty in
   let literal_map = ref Mid.empty in
+  let prec_map  = ref Mid.empty in
+  let assoc_map = ref Mid.empty in
   let qualid    = ref [] in
 
   let find_pr th (loc,q) = try Theory.ns_find_pr th.th_export q
@@ -184,9 +190,11 @@ let load_driver env file extra_files =
     | MRexception (q,s) ->
         let xs = find_xs m q in
         add_syntax xs.Ity.xs_name s false
-    | MRval (q,s) ->
+    | MRval (q,s,p,a) ->
         let id = find_val m q in
-        add_syntax id s false
+        add_syntax id s false;
+        prec_map := Mid.add id p !prec_map;
+        assoc_map := Mid.add id a !assoc_map;                   
     | MRtheory trule ->
         add_local m.mod_theory (loc,trule)
   in
@@ -222,6 +230,8 @@ let load_driver env file extra_files =
     drv_blacklist   = Queue.fold (fun l s -> s :: l) [] blacklist;
     drv_syntax      = !syntax_map;
     drv_literal     = !literal_map;
+    drv_prec        = !prec_map;
+    drv_assoc       = !assoc_map;
   }
 
 (* registering printers for programs *)
@@ -277,6 +287,8 @@ let lookup_printer drv =
       blacklist   = drv.drv_blacklist;
       syntax      = drv.drv_syntax;
       literal     = drv.drv_literal;
+      prec        = drv.drv_prec;
+      assoc       = drv.drv_assoc;
     }
   in
   try

src/mlw/pdriver.mli

@@ -20,6 +20,8 @@ type driver = private {
   drv_blacklist   : Printer.blacklist;
   drv_syntax      : Printer.syntax_map;
   drv_literal     : Printer.syntax_map;
+  drv_prec        : (int option) Ident.Mid.t;
+  drv_assoc       : (Driver_ast.assoc_dir option) Ident.Mid.t;
 }
 
 
@@ -31,6 +33,8 @@ type printer_args = private {
   blacklist   : Printer.blacklist;
   syntax      : Printer.syntax_map;
   literal     : Printer.syntax_map;
+  prec        : (int option) Ident.Mid.t;
+  assoc       : (Driver_ast.assoc_dir option) Ident.Mid.t;
 }
 
 val load_driver : Env.env -> string -> string list -> driver