Factorize the naming convention for prefix infix mixfix

doc/api.tex

@@ -300,7 +300,7 @@ let four : Term.term =
 let int_theory : Theory.theory =
   Env.read_theory env ["int"] "Int"
 let plus_symbol : Term.lsymbol =
-  Theory.ns_find_ls int_theory.Theory.th_export ["infix +"]
+  Theory.ns_find_ls int_theory.Theory.th_export [Ident.infix "+"]
 let two_plus_two : Term.term =
   Term.t_app_infer plus_symbol [two;two]
 let fmla3 : Term.term = Term.t_equ two_plus_two four
@@ -332,9 +332,9 @@ obtain the symbols from \texttt{Int}.
 let zero : Term.term =
   Term.t_const (Number.ConstInt (Number.int_const_dec "0"))
 let mult_symbol : Term.lsymbol =
-  Theory.ns_find_ls int_theory.Theory.th_export ["infix *"]
+  Theory.ns_find_ls int_theory.Theory.th_export [Ident.infix "*"]
 let ge_symbol : Term.lsymbol =
-  Theory.ns_find_ls int_theory.Theory.th_export ["infix >="]
+  Theory.ns_find_ls int_theory.Theory.th_export [Ident.infix ">="]
 \end{ocamlcode}
 The next step is to introduce the variable $x$ with the type int.
 \begin{ocamlcode}

plugins/python/py_main.ml

@@ -22,9 +22,9 @@ let () = Debug.set_flag Dterm.debug_ignore_unused_var
 let mk_id ~loc name =
   { id_str = name; id_lab = []; id_loc = loc }
 
-let infix  ~loc s = Qident (mk_id ~loc ("infix "  ^ s))
-let prefix ~loc s = Qident (mk_id ~loc ("prefix " ^ s))
-let mixfix ~loc s = Qident (mk_id ~loc ("mixfix " ^ s))
+let infix  ~loc s = Qident (mk_id ~loc (Ident.infix s))
+let prefix ~loc s = Qident (mk_id ~loc (Ident.prefix s))
+let mixfix ~loc s = Qident (mk_id ~loc (Ident.mixfix s))
 
 let mk_expr ~loc d =
   { expr_desc = d; expr_loc = loc }

plugins/python/py_parser.mly

@@ -34,12 +34,8 @@
   let empty_annotation =
     { loop_invariant = []; loop_variant = [] }
 
-  let infix  s = "infix "  ^ s
-  let prefix s = "prefix " ^ s
-  let mixfix s = "mixfix " ^ s
-
-  let get_op s e = Qident (mk_id (mixfix "[]") s e)
-  let set_op s e = Qident (mk_id (mixfix "[<-]") s e)
+  let get_op s e = Qident (mk_id (Ident.mixfix "[]") s e)
+  let set_op s e = Qident (mk_id (Ident.mixfix "[<-]") s e)
 
   let empty_spec = {
     sp_pre     = [];    sp_post    = [];  sp_xpost   = [];
@@ -328,9 +324,9 @@ term_sub_:
 | AND     { Tand }
 
 %inline infix_op:
-| PLUS   { mk_id (infix "+") $startpos $endpos }
-| MINUS  { mk_id (infix "-") $startpos $endpos }
-| TIMES  { mk_id (infix "*") $startpos $endpos }
+| PLUS   { mk_id (Ident.infix "+") $startpos $endpos }
+| MINUS  { mk_id (Ident.infix "-") $startpos $endpos }
+| TIMES  { mk_id (Ident.infix "*") $startpos $endpos }
 | c=CMP  { let op = match c with
           | Beq -> "="
           | Bneq -> "<>"
@@ -339,10 +335,10 @@ term_sub_:
           | Bgt  -> ">"
           | Bge  -> ">="
           | Badd|Bsub|Bmul|Bdiv|Bmod|Band|Bor -> assert false in
-           mk_id (infix op) $startpos $endpos }
+           mk_id (Ident.infix op) $startpos $endpos }
 
 %inline prefix_op:
-| MINUS { mk_id (prefix "-")  $startpos $endpos }
+| MINUS { mk_id (Ident.prefix "-")  $startpos $endpos }
 
 %inline div_mod_op:
 | DIV  { mk_id "div" $startpos $endpos }

src/core/ident.ml

@@ -99,6 +99,24 @@ let get_model_trace_string ~labels =
   | _ -> ""
 
 
+(** Naming convention *)
+
+let infix  s = "infix "  ^ s
+let prefix s = "prefix " ^ s
+let mixfix s = "mixfix " ^ s
+
+let kind_of_fix s =
+  let len = String.length s in
+  if len < 7 then `None else
+  let inf = String.sub s 0 6 in
+  if inf = "infix "  then `Infix (String.sub s 6 (len - 6)) else
+  let prf = String.sub s 0 7 in
+  if prf = "prefix " then `Prefix (String.sub s 7 (len - 7)) else
+  let prf = String.sub s 0 7 in
+  if prf = "mixfix " then `Mixfix (String.sub s 7 (len - 7)) else
+  `None
+
+
 (** Identifiers *)
 
 type ident = {

src/core/ident.mli

@@ -60,6 +60,22 @@ val get_model_trace_label : labels : Slab.t -> Slab.elt
 (** Return a label of the form ["model_trace:*"].
     Throws [Not_found] if there is no such label. *)
 
+(** {2 Naming convention } *)
+
+val infix: string -> string
+(** Apply the naming convention for infix operator (+) *)
+
+val prefix: string -> string
+(** Apply the naming convention for prefix operator *)
+
+val mixfix: string -> string
+(** Apply the naming convention for mixfix operator *)
+
+val kind_of_fix: string -> [ `None
+                           | `Prefix of string
+                           | `Infix  of string
+                           | `Mixfix of string ]
+
 (** {2 Identifiers} *)
 
 type ident = private {

src/core/pretty.ml

@@ -76,13 +76,9 @@ let forget_var vs = forget_id iprinter vs.vs_name
 
 let extract_op ls =
   let s = ls.ls_name.id_string in
-  let len = String.length s in
-  if len < 7 then None else
-  let inf = String.sub s 0 6 in
-  if inf = "infix "  then Some (String.sub s 6 (len - 6)) else
-  let prf = String.sub s 0 7 in
-  if prf = "prefix " then Some (String.sub s 7 (len - 7)) else
-  None
+  match Ident.kind_of_fix s with
+  | `None | `Mixfix _ -> None
+  | `Prefix s | `Infix s -> Some s
 
 let tight_op s = let c = String.sub s 0 1 in c = "!" || c = "?"
 

src/driver/driver_parser.mly

@@ -12,9 +12,6 @@
 %{
   open Driver_ast
 
-  let infix s  = "infix " ^ s
-  let prefix s = "prefix " ^ s
-  let mixfix s = "mixfix " ^ s
 %}
 
 %token <int> INTEGER
@@ -136,15 +133,15 @@ ident:
 
 ident_rich:
 | ident                     { $1 }
-| LEFTPAR_STAR_RIGHTPAR     { infix "*" }
+| LEFTPAR_STAR_RIGHTPAR     { Ident.infix "*" }
 | LEFTPAR operator RIGHTPAR { $2 }
 
 operator:
-| OPERATOR              { infix $1 }
-| OPERATOR UNDERSCORE   { prefix $1 }
-| LEFTSQ RIGHTSQ        { mixfix "[]" }
-| LEFTSQ LARROW RIGHTSQ { mixfix "[<-]" }
-| LEFTSQ RIGHTSQ LARROW { mixfix "[]<-" }
+| OPERATOR              { Ident.infix $1 }
+| OPERATOR UNDERSCORE   { Ident.prefix $1 }
+| LEFTSQ RIGHTSQ        { Ident.mixfix "[]" }
+| LEFTSQ LARROW RIGHTSQ { Ident.mixfix "[<-]" }
+| LEFTSQ RIGHTSQ LARROW { Ident.mixfix "[]<-" }
 
 (* Types *)
 

src/mlw/expr.ml

@@ -866,20 +866,16 @@ let forget_let_defn = function
 
 let extract_op s =
   let s = s.rs_name.id_string in
-  let len = String.length s in
-  if len < 7 then None else
-  let inf = String.sub s 0 6 in
-  if inf = "infix "  then Some (String.sub s 6 (len - 6)) else
-  let prf = String.sub s 0 7 in
-  if prf = "prefix " then Some (String.sub s 7 (len - 7)) else
-  None
+  match Ident.kind_of_fix s with
+  | `None | `Mixfix _ -> None
+  | `Prefix s | `Infix s -> Some s
 
 let tight_op s = let c = String.sub s 0 1 in c = "!" || c = "?"
 
 let print_rs fmt s =
-  if s.rs_name.id_string = "mixfix []" then pp_print_string fmt "([])" else
-  if s.rs_name.id_string = "mixfix []<-" then pp_print_string fmt "([]<-)" else
-  if s.rs_name.id_string = "mixfix [<-]" then pp_print_string fmt "([<-])" else
+  if s.rs_name.id_string = Ident.mixfix "[]" then pp_print_string fmt "([])" else
+  if s.rs_name.id_string = Ident.mixfix "[]<-" then pp_print_string fmt "([]<-)" else
+  if s.rs_name.id_string = Ident.mixfix "[<-]" then pp_print_string fmt "([<-])" else
   match extract_op s, s.rs_logic with
   | Some s, _ ->
       let s = Str.replace_first (Str.regexp "^\\*.") " \\0" s in

src/parser/parser.mly

@@ -27,10 +27,6 @@ end
 
   open Ptree
 
-  let infix  s = "infix "  ^ s
-  let prefix s = "prefix " ^ s
-  let mixfix s = "mixfix " ^ s
-
   let qualid_last = function Qident x | Qdot (_, x) -> x.id_str
 
   let floc s e = Loc.extract (s,e)
@@ -90,11 +86,11 @@ end
 
   let mk_id id s e = { id_str = id; id_lab = []; id_loc = floc s e }
 
-  let get_op s e = Qident (mk_id (mixfix "[]") s e)
-  let set_op s e = Qident (mk_id (mixfix "[<-]") s e)
-  let sub_op s e = Qident (mk_id (mixfix "[_.._]") s e)
-  let above_op s e = Qident (mk_id (mixfix "[_..]") s e)
-  let below_op s e = Qident (mk_id (mixfix "[.._]") s e)
+  let get_op s e = Qident (mk_id (Ident.mixfix "[]") s e)
+  let set_op s e = Qident (mk_id (Ident.mixfix "[<-]") s e)
+  let sub_op s e = Qident (mk_id (Ident.mixfix "[_.._]") s e)
+  let above_op s e = Qident (mk_id (Ident.mixfix "[_..]") s e)
+  let below_op s e = Qident (mk_id (Ident.mixfix "[.._]") s e)
 
   let mk_pat  d s e = { pat_desc  = d; pat_loc  = floc s e }
   let mk_term d s e = { term_desc = d; term_loc = floc s e }
@@ -729,8 +725,8 @@ expr_:
 | expr LARROW expr
     { match $1.expr_desc with
       | Eidapp (q, [e1]) -> Eassign (e1, q, $3)
-      | Eidapp (Qident id, [e1;e2]) when id.id_str = mixfix "[]" ->
-          Eidapp (Qident {id with id_str = mixfix "[]<-"}, [e1;e2;$3])
+      | Eidapp (Qident id, [e1;e2]) when id.id_str = Ident.mixfix "[]" ->
+          Eidapp (Qident {id with id_str = Ident.mixfix "[]<-"}, [e1;e2;$3])
       | _ -> raise Error }
 | LET top_ghost pattern EQUAL seq_expr IN seq_expr
     { match $3.pat_desc with
@@ -993,21 +989,21 @@ lident_op_id:
     { (* parentheses are removed from the location *)
       let s = let s = $startpos in { s with Lexing.pos_cnum = s.Lexing.pos_cnum + 1 } in
       let e = let e = $endpos   in { e with Lexing.pos_cnum = e.Lexing.pos_cnum - 1 } in
-      mk_id (infix "*") s e }
+      mk_id (Ident.infix "*") s e }
 
 lident_op:
-| op_symbol               { infix $1 }
-| op_symbol UNDERSCORE    { prefix $1 }
-| MINUS     UNDERSCORE    { prefix "-" }
-| EQUAL                   { infix "=" }
-| MINUS                   { infix "-" }
-| OPPREF                  { prefix $1 }
-| LEFTSQ RIGHTSQ          { mixfix "[]" }
-| LEFTSQ LARROW RIGHTSQ   { mixfix "[<-]" }
-| LEFTSQ RIGHTSQ LARROW   { mixfix "[]<-" }
-| LEFTSQ UNDERSCORE DOTDOT UNDERSCORE RIGHTSQ { mixfix "[_.._]" }
-| LEFTSQ            DOTDOT UNDERSCORE RIGHTSQ { mixfix "[.._]" }
-| LEFTSQ UNDERSCORE DOTDOT            RIGHTSQ { mixfix "[_..]" }
+| op_symbol               { Ident.infix $1 }
+| op_symbol UNDERSCORE    { Ident.prefix $1 }
+| MINUS     UNDERSCORE    { Ident.prefix "-" }
+| EQUAL                   { Ident.infix "=" }
+| MINUS                   { Ident.infix "-" }
+| OPPREF                  { Ident.prefix $1 }
+| LEFTSQ RIGHTSQ          { Ident.mixfix "[]" }
+| LEFTSQ LARROW RIGHTSQ   { Ident.mixfix "[<-]" }
+| LEFTSQ RIGHTSQ LARROW   { Ident.mixfix "[]<-" }
+| LEFTSQ UNDERSCORE DOTDOT UNDERSCORE RIGHTSQ { Ident.mixfix "[_.._]" }
+| LEFTSQ            DOTDOT UNDERSCORE RIGHTSQ { Ident.mixfix "[.._]" }
+| LEFTSQ UNDERSCORE DOTDOT            RIGHTSQ { Ident.mixfix "[_..]" }
 
 op_symbol:
 | OP1 { $1 }
@@ -1018,22 +1014,22 @@ op_symbol:
 | GT  { ">" }
 
 %inline oppref:
-| o = OPPREF { mk_id (prefix o)  $startpos $endpos }
+| o = OPPREF { mk_id (Ident.prefix o)  $startpos $endpos }
 
 prefix_op:
-| op_symbol { mk_id (prefix $1)  $startpos $endpos }
-| MINUS     { mk_id (prefix "-") $startpos $endpos }
+| op_symbol { mk_id (Ident.prefix $1)  $startpos $endpos }
+| MINUS     { mk_id (Ident.prefix "-") $startpos $endpos }
 
 %inline infix_op:
-| o = OP1   { mk_id (infix o)    $startpos $endpos }
-| o = OP2   { mk_id (infix o)    $startpos $endpos }
-| o = OP3   { mk_id (infix o)    $startpos $endpos }
-| o = OP4   { mk_id (infix o)    $startpos $endpos }
-| EQUAL     { mk_id (infix "=")  $startpos $endpos }
-| LTGT      { mk_id (infix "<>") $startpos $endpos }
-| LT        { mk_id (infix "<")  $startpos $endpos }
-| GT        { mk_id (infix ">")  $startpos $endpos }
-| MINUS     { mk_id (infix "-")  $startpos $endpos }
+| o = OP1   { mk_id (Ident.infix o)    $startpos $endpos }
+| o = OP2   { mk_id (Ident.infix o)    $startpos $endpos }
+| o = OP3   { mk_id (Ident.infix o)    $startpos $endpos }
+| o = OP4   { mk_id (Ident.infix o)    $startpos $endpos }
+| EQUAL     { mk_id (Ident.infix "=")  $startpos $endpos }
+| LTGT      { mk_id (Ident.infix "<>") $startpos $endpos }
+| LT        { mk_id (Ident.infix "<")  $startpos $endpos }
+| GT        { mk_id (Ident.infix ">")  $startpos $endpos }
+| MINUS     { mk_id (Ident.infix "-")  $startpos $endpos }
 
 (* Qualified idents *)