Commit 0fea401c authored by Andrei Paskevich's avatar Andrei Paskevich

confine all notation handling inside Ident

This commit removes all hard-coded "infix ..", "prefix ..",
and "mixfix .." from the rest of the code, and handles the
symbolic notation entirely inside Ident. It does not change
the notation itself.
parent 9fbe2a80
......@@ -97,10 +97,10 @@ let mk_evar x = mk_expr(Eident(Qident x))
*)
(* BEGIN{code1} *)
let eq_symb = mk_qid [Ident.infix "="]
let eq_symb = mk_qid [Ident.op_infix "="]
let int_type_id = mk_qid ["int"]
let int_type = PTtyapp(int_type_id,[])
let mul_int = mk_qid ["Int";Ident.infix "*"]
let mul_int = mk_qid ["Int";Ident.op_infix "*"]
let d1 : decl =
let id_x = mk_ident "x" in
......@@ -146,7 +146,7 @@ END{source2}
*)
(* BEGIN{code2} *)
let ge_int = mk_qid ["Int";Ident.infix ">="]
let ge_int = mk_qid ["Int";Ident.op_infix ">="]
let use_ref_Ref = use_import ("ref","Ref")
......@@ -168,7 +168,7 @@ let d2 =
let body =
let e1 = mk_eapp (mk_qid ["Ref";"ref"]) [mk_econst "42"] in
let id_x = mk_ident "x" in
let e2 = mk_eapp (mk_qid ["Ref";Ident.prefix "!"]) [mk_evar id_x] in
let e2 = mk_eapp (mk_qid ["Ref";Ident.op_prefix "!"]) [mk_evar id_x] in
mk_expr(Elet(id_x,false,Expr.RKlocal,e1,e2))
in
let f = Efun(param0,None,Ity.MaskVisible,spec,body)
......@@ -198,9 +198,9 @@ let array_int_type = PTtyapp(mk_qid ["Array";"array"],[int_type])
let length = mk_qid ["Array";"length"]
let array_get = mk_qid ["Array"; Ident.mixfix "[]"]
let array_get = mk_qid ["Array"; Ident.op_get]
let array_set = mk_qid ["Array"; Ident.mixfix "[]<-"]
let array_set = mk_qid ["Array"; Ident.op_set]
let d3 =
let id_a = mk_ident "a" in
......
......@@ -62,10 +62,10 @@ let scanf s =
let read_channel env path filename cin =
(* Find the int theory and the needed operation *)
let th_int = Env.read_theory env ["int"] "Int" in
let leq = ns_find_ls th_int.th_export ["infix <"] in
let plus_symbol = Theory.ns_find_ls th_int.Theory.th_export ["infix +"] in
let neg_symbol = Theory.ns_find_ls th_int.Theory.th_export ["prefix -"] in
let mult_symbol = Theory.ns_find_ls th_int.Theory.th_export ["infix *"] in
let leq = ns_find_ls th_int.th_export [op_infix "<"] in
let plus_symbol = ns_find_ls th_int.th_export [op_infix "+"] in
let neg_symbol = ns_find_ls th_int.th_export [op_prefix "-"] in
let mult_symbol = ns_find_ls th_int.th_export [op_infix "*"] in
let zero = t_nat_const 0 in
let t_int_const n =
......
......@@ -27,9 +27,10 @@ let () = Debug.set_flag Dterm.debug_ignore_unused_var
let mk_id ~loc name =
{ id_str = name; id_ats = []; id_loc = loc }
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 infix ~loc s = Qident (mk_id ~loc (Ident.op_infix s))
let prefix ~loc s = Qident (mk_id ~loc (Ident.op_prefix s))
let get_op ~loc = Qident (mk_id ~loc Ident.op_get)
let set_op ~loc = Qident (mk_id ~loc Ident.op_set)
let mk_expr ~loc d =
{ expr_desc = d; expr_loc = loc }
......@@ -48,7 +49,7 @@ let mk_ref ~loc e =
let deref_id ~loc id =
mk_expr ~loc (Eidapp (prefix ~loc "!", [mk_expr ~loc (Eident (Qident id))]))
let array_set ~loc a i v =
mk_expr ~loc (Eidapp (mixfix ~loc "[]<-", [a; i; v]))
mk_expr ~loc (Eidapp (set_op ~loc, [a; i; v]))
let constant ~loc i =
mk_expr ~loc (Econst (Number.const_of_int i))
let constant_s ~loc s =
......@@ -194,7 +195,7 @@ let rec expr env {Py_ast.expr_loc = loc; Py_ast.expr_desc = d } = match d with
mk_expr ~loc (Esequence (assign, seq)) in
List.fold_left init (mk_var ~loc id) el))
| Py_ast.Eget (e1, e2) ->
mk_expr ~loc (Eidapp (mixfix ~loc "[]", [expr env e1; expr env e2]))
mk_expr ~loc (Eidapp (get_op ~loc, [expr env e1; expr env e2]))
let post env (loc, l) =
loc, List.map (fun (pat, t) -> pat, deref env t) l
......@@ -220,7 +221,7 @@ let rec stmt env ({Py_ast.stmt_loc = loc; Py_ast.stmt_desc = d } as s) =
let e = expr env e in
if Mstr.mem id.id_str env.vars then
let x = let loc = id.id_loc in mk_expr ~loc (Eident (Qident id)) in
mk_expr ~loc (Einfix (x, mk_id ~loc "infix :=", e))
mk_expr ~loc (Einfix (x, mk_id ~loc (Ident.op_infix ":="), e))
else
block env ~loc [Dstmt s]
| Py_ast.Sset (e1, e2, e3) ->
......@@ -272,11 +273,11 @@ let rec stmt env ({Py_ast.stmt_loc = loc; Py_ast.stmt_desc = d } as s) =
let invariant inv =
let loc = inv.term_loc in
let li = mk_term ~loc
(Tidapp (mixfix ~loc "[]", [mk_tvar ~loc l; mk_tvar ~loc i])) in
(Tidapp (get_op ~loc, [mk_tvar ~loc l; mk_tvar ~loc i])) in
mk_term ~loc (Tlet (id, li, deref env inv)) in
mk_expr ~loc (Efor (i, lb, Expr.To, ub, List.map invariant inv,
let li = mk_expr ~loc
(Eidapp (mixfix ~loc "[]", [mk_var ~loc l; mk_var ~loc i])) in
(Eidapp (get_op ~loc, [mk_var ~loc l; mk_var ~loc i])) in
mk_expr ~loc (Elet (id, false, Expr.RKnone, mk_ref ~loc li,
let env = add_var env id in
block ~loc env body
......
......@@ -31,8 +31,8 @@
| _, ({term_loc = loc},_)::_ -> Loc.errorm ~loc
"multiple `variant' clauses are not allowed"
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 get_op s e = Qident (mk_id Ident.op_get s e)
let upd_op s e = Qident (mk_id Ident.op_upd s e)
let empty_spec = {
sp_pre = []; sp_post = []; sp_xpost = [];
......@@ -316,7 +316,7 @@ term_sub_:
| term_arg LEFTSQ term RIGHTSQ
{ Tidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
| term_arg LEFTSQ term LARROW term RIGHTSQ
{ Tidapp (set_op $startpos($2) $endpos($2), [$1;$3;$5]) }
{ Tidapp (upd_op $startpos($2) $endpos($2), [$1;$3;$5]) }
%inline bin_op:
| ARROW { Dterm.DTimplies }
......@@ -333,17 +333,17 @@ term_sub_:
| Bgt -> ">"
| Bge -> ">="
| Badd|Bsub|Bmul|Bdiv|Bmod|Band|Bor -> assert false in
mk_id (Ident.infix op) $startpos $endpos }
mk_id (Ident.op_infix op) $startpos $endpos }
%inline prefix_op:
| MINUS { mk_id (Ident.prefix "-") $startpos $endpos }
| MINUS { mk_id (Ident.op_prefix "-") $startpos $endpos }
%inline infix_op_234:
| DIV { mk_id "div" $startpos $endpos }
| MOD { mk_id "mod" $startpos $endpos }
| PLUS { mk_id (Ident.infix "+") $startpos $endpos }
| MINUS { mk_id (Ident.infix "-") $startpos $endpos }
| TIMES { mk_id (Ident.infix "*") $startpos $endpos }
| PLUS { mk_id (Ident.op_infix "+") $startpos $endpos }
| MINUS { mk_id (Ident.op_infix "-") $startpos $endpos }
| TIMES { mk_id (Ident.op_infix "*") $startpos $endpos }
comma_list1(X):
| separated_nonempty_list(COMMA, X) { $1 }
......@@ -158,11 +158,11 @@ let defined_arith ~loc denv env impl dw tl =
in
add_theory env impl th;
let ls = match dw with
| DF DFumin -> ns_find_ls th.th_export ["prefix -"]
| DF DFsum -> ns_find_ls th.th_export ["infix +"]
| DF DFdiff -> ns_find_ls th.th_export ["infix -"]
| DF DFprod -> ns_find_ls th.th_export ["infix *"]
| DF DFquot -> ns_find_ls th.th_export ["infix /"]
| DF DFumin -> ns_find_ls th.th_export [op_prefix "-"]
| DF DFsum -> ns_find_ls th.th_export [op_infix "+"]
| DF DFdiff -> ns_find_ls th.th_export [op_infix "-"]
| DF DFprod -> ns_find_ls th.th_export [op_infix "*"]
| DF DFquot -> ns_find_ls th.th_export [op_infix "/"]
| DF DFquot_e -> ns_find_ls th.th_export ["div"]
| DF DFquot_t -> ns_find_ls th.th_export ["div_t"]
| DF DFquot_f -> ns_find_ls th.th_export ["div_f"]
......@@ -176,10 +176,10 @@ let defined_arith ~loc denv env impl dw tl =
| DF DFtoint -> ns_find_ls th.th_export ["to_int"]
| DF DFtorat -> ns_find_ls th.th_export ["to_rat"]
| DF DFtoreal -> ns_find_ls th.th_export ["to_real"]
| DP DPless -> ns_find_ls th.th_export ["infix <"]
| DP DPlesseq -> ns_find_ls th.th_export ["infix <="]
| DP DPgreater -> ns_find_ls th.th_export ["infix >"]
| DP DPgreatereq -> ns_find_ls th.th_export ["infix >="]
| DP DPless -> ns_find_ls th.th_export [op_infix "<"]
| DP DPlesseq -> ns_find_ls th.th_export [op_infix "<="]
| DP DPgreater -> ns_find_ls th.th_export [op_infix ">"]
| DP DPgreatereq -> ns_find_ls th.th_export [op_infix ">="]
| DP DPisint -> ns_find_ls th.th_export ["is_int"]
| DP DPisrat -> ns_find_ls th.th_export ["is_rat"]
| DP (DPtrue|DPfalse|DPdistinct) | DT _ -> assert false
......
......@@ -49,21 +49,134 @@ let attr_compare a1 a2 = Pervasives.compare a1.attr_tag a2.attr_tag
(** Naming convention *)
let infix s = "infix " ^ s
let prefix s = "prefix " ^ s
let mixfix s = "mixfix " ^ s
let kind_of_fix s =
type notation =
| SNword of string
| SNinfix of string
| SNprefix of string
| SNget (* [] *)
| SNset (* []<- *)
| SNupd (* [<-] *)
| SNcut (* [..] *)
| SNlcut (* [.._] *)
| SNrcut (* [_..] *)
(* current encoding *)
let op_infix s = "infix " ^ s
let op_prefix s = "prefix " ^ s
let op_equ = op_infix "="
let op_neq = op_infix "<>"
let op_get = "mixfix []"
let op_set = "mixfix []<-"
let op_upd = "mixfix [<-]"
let op_cut = "mixfix [..]"
let op_lcut = "mixfix [.._]"
let op_rcut = "mixfix [_..]"
let check_op = function
| '@' | '!' | '^' | '$' | '=' | '%' | '>' | '#'
| '.' | ',' | '<' | '-' | '&' | '/' | '+' | '?'
| ':' | '*' | '~' | '|' | '\\' -> ()
| _ -> raise Exit
let extract_infix 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
if len <= 6 then None else
let prf = String.sub s 0 6 in
if prf <> "infix " then None else
let suf = String.sub s 6 (len - 6) in
try String.iter check_op suf; Some suf
with Exit -> None
let extract_prefix s =
let len = String.length s in
if len <= 7 then None else
let prf = String.sub s 0 7 in
if prf = "mixfix " then `Mixfix (String.sub s 7 (len - 7)) else
`None
if prf <> "prefix " then None else
let suf = String.sub s 7 (len - 7) in
try String.iter check_op suf; Some suf
with Exit -> None
let sn_decode s =
match extract_infix s with Some op -> SNinfix op | None -> begin
match extract_prefix s with Some op -> SNprefix op | None -> begin
if Strings.has_prefix "mixfix " s then begin
if s = op_get then SNget else
if s = op_set then SNset else
if s = op_upd then SNupd else
if s = op_cut then SNcut else
if s = op_lcut then SNlcut else
if s = op_rcut then SNrcut else
invalid_arg "Ident.sn_decode"
end else SNword s end end
(* NOTE: possible future code, do not remove
let op_to_alpha = function
| '@' -> 'a' | '!' -> 'b' | '^' -> 'c' | '$' -> 'd'
| '=' -> 'e' | '%' -> 'f' | '>' -> 'g' | '#' -> 'h'
| '.' -> 'i' | ',' -> 'j' | '<' -> 'l' | '-' -> 'm'
| '&' -> 'n' | '/' -> 'o' | '+' -> 'p' | '?' -> 'q'
| ':' -> 'r' | '*' -> 's' | '~' -> 't' | '\\' -> 'u'
| '|' -> 'v' | _ -> invalid_arg "Ident.sn_encode"
let alpha_to_op = function
| 'a' -> '@' | 'b' -> '!' | 'c' -> '^' | 'd' -> '$'
| 'e' -> '=' | 'f' -> '%' | 'g' -> '>' | 'h' -> '#'
| 'i' -> '.' | 'j' -> ',' | 'l' -> '<' | 'm' -> '-'
| 'n' -> '&' | 'o' -> '/' | 'p' -> '+' | 'q' -> '?'
| 'r' -> ':' | 's' -> '*' | 't' -> '~' | 'u' -> '\\'
| 'v' -> '|' | _ -> invalid_arg "Ident.sn_decode"
let op_infix s = String.map op_to_alpha s ^ "'i"
let op_prefix s = String.map op_to_alpha s ^ "'p"
let op_equ = op_infix "="
let op_neq = op_infix "<>"
let op_get = "get'm"
let op_set = "set'm"
let op_upd = "upd'm"
let op_cut = "cut'm"
let op_lcut = "lcut'm"
let op_rcut = "rcut'm"
let sn_decode s =
let len = String.length s - 2 in
if len <= 0 || String.get s len <> '\'' then SNword s else
match String.get s (succ len) with
| 'i' -> SNinfix (String.map alpha_to_op (String.sub s 0 len))
| 'p' -> SNprefix (String.map alpha_to_op (String.sub s 0 len))
| 'm' -> if s = op_get then SNget else
if s = op_set then SNset else
if s = op_upd then SNupd else
if s = op_cut then SNcut else
if s = op_lcut then SNlcut else
if s = op_rcut then SNrcut else
invalid_arg "Ident.sn_decode"
| _ -> SNword s
*)
let sn_encode = function
| SNword s -> s
| SNinfix s -> op_infix s
| SNprefix s -> op_prefix s
| SNget -> op_get
| SNset -> op_set
| SNupd -> op_upd
| SNcut -> op_cut
| SNlcut -> op_lcut
| SNrcut -> op_rcut
let str_decode s = match sn_decode s with
| SNword s -> s
| SNinfix s -> "(" ^ s ^ ")"
| SNprefix s -> "(" ^ s ^ "_)"
| SNget -> "([])"
| SNupd -> "([<-])"
| SNset -> "([]<-)"
| SNcut -> "([..])"
| SNlcut -> "([.._])"
| SNrcut -> "([_..])"
(** Identifiers *)
......@@ -140,23 +253,30 @@ type ident_printer = {
(* name is already sanitized *)
let find_unique indices name =
let specname ind =
let rec repeat n s =
if n <= 0 then s else repeat (n-1) (s ^ "^")
in
(* In the case, the symbol is infix/prefix *and* the name has not been
sanitized for provers (the space " " is still there), we don't want to
disambiguate with a number but with a symbol: "+" becomes "+." "+.." etc.
It allows to parse the ident again (for transformations).
*)
if Strings.has_prefix "infix " name ||
Strings.has_prefix "prefix " name then
(repeat ind name)
else
if ind < 0 then
name
else
name ^ string_of_int ind
(* If the symbol is infix/prefix *and* the name has not been
sanitized for provers (the quote is still there), we don't
want to disambiguate with a number but with a symbol:
"+" becomes "+^" "+^^" etc. This allows to parse the
ident again (for transformations). *)
if ind <= 0 then name else
match extract_infix name with
| Some s -> op_infix (s ^ String.make ind '^')
| None -> begin match extract_prefix name with
| Some s -> op_prefix (s ^ String.make ind '^')
| None -> name ^ string_of_int ind end
in
(* NOTE: possible future code, do not remove
let specname ind =
if ind <= 0 then name else
let len = String.length name - 2 in
if len > 0 && String.get name len = '\'' then
match String.get name (succ len) with
| 'i' -> String.sub name 0 len ^ String.make ind 'c' ^ "'i"
| 'p' -> String.sub name 0 len ^ String.make ind 'c' ^ "'p"
| _ -> name ^ string_of_int ind
else name ^ string_of_int ind
in
*)
let testname ind = Hstr.mem indices (specname ind) in
let rec advance ind =
if testname ind then advance (succ ind) else ind in
......@@ -231,7 +351,7 @@ let char_to_alpha c = match c with
| '0' -> "zr" | '1' -> "un" | '2' -> "du"
| '3' -> "tr" | '4' -> "qr" | '5' -> "qn"
| '6' -> "sx" | '7' -> "st" | '8' -> "oc"
| '9' -> "nn" | '\n' -> "br" | _ -> "zz"
| '9' -> "nn" | '\n' -> "nl" | _ -> "zz"
let char_to_lalpha c = Strings.uncapitalize (char_to_alpha c)
let char_to_ualpha c = Strings.capitalize (char_to_alpha c)
......@@ -250,17 +370,17 @@ let char_to_lalnumus c =
let sanitizer' head rest last n =
let lst = ref [] in
let n = if n = "" then "zilch" else n in
let len = String.length n in
let code i c = lst :=
(if i = 0 then head
else if i = String.length n - 1 then last
else if i = len - 1 then last
else rest) c :: !lst in
let n = if n = "" then "zilch" else n in
String.iteri code n;
String.concat "" (List.rev !lst)
let sanitizer head rest n = sanitizer' head rest rest n
(** {2 functions for working with counterexample attributes} *)
let model_attr = create_attribute "model"
......
......@@ -29,21 +29,41 @@ val create_attribute : string -> attribute
val list_attributes : unit -> string list
(** {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 Naming convention} *)
type notation =
| SNword of string
| SNinfix of string
| SNprefix of string
| SNget (* [] *)
| SNset (* []<- *)
| SNupd (* [<-] *)
| SNcut (* [..] *)
| SNlcut (* [.._] *)
| SNrcut (* [_..] *)
val sn_encode : notation -> string
(* encode the symbol name as a string *)
val sn_decode : string -> notation
(* decode the string as a symbol name *)
val str_decode : string -> string
(* decode the string as a symbol name and pretty-print it *)
(* specialized encoders *)
val op_infix : string -> string
val op_prefix : string -> string
val op_equ : string
val op_neq : string
val op_get : string
val op_set : string
val op_upd : string
val op_cut : string
val op_lcut : string
val op_rcut : string
(** {2 Identifiers} *)
......
......@@ -133,45 +133,46 @@ let forget_var vs = forget_id iprinter vs.vs_name
(* pretty-print infix and prefix logic symbols *)
let extract_op s =
(*let s = ls.ls_name.id_string in*)
match Ident.kind_of_fix s with
| `None | `Mixfix _ -> None
| `Prefix s | `Infix s -> Some s
let tight_op s =
s <> "" && (let c = String.get s 0 in c = '!' || c = '?')
let escape_op s =
let s = if Strings.has_prefix "*" s then " " ^ s else s in
let s = if Strings.has_suffix "*" s then s ^ " " else s in
s
let left_escape_op s =
if Strings.has_prefix "*" s then " " ^ s else s
let escape_op s = let s = left_escape_op s in
if Strings.has_suffix "*" s then s ^ " " else s
(* theory names always start with an upper case letter *)
let print_th fmt th =
let sanitizer = Strings.capitalize in
fprintf fmt "%s" (id_unique iprinter ~sanitizer th.th_name)
pp_print_string fmt (id_unique iprinter ~sanitizer th.th_name)
let print_ts fmt ts =
fprintf fmt "%s" (id_unique tprinter ts.ts_name)
let print_ls fmt ({ls_name = {id_string = nm}} as ls) =
if nm = "mixfix []" then pp_print_string fmt "([])" else
if nm = "mixfix [<-]" then pp_print_string fmt "([<-])" else
if nm = "mixfix [..]" then pp_print_string fmt "([..])" else
if nm = "mixfix [_..]" then pp_print_string fmt "([_..])" else
if nm = "mixfix [.._]" then pp_print_string fmt "([.._])" else
let s = id_unique iprinter ls.ls_name in
match extract_op s with
| Some s -> fprintf fmt "(%s)" (escape_op s)
| None -> fprintf fmt "%s" s
if ts_equal ts ts_func then pp_print_string fmt "(->)" else
pp_print_string fmt (id_unique tprinter ts.ts_name)
let print_raw_ls fmt ls =
pp_print_string fmt (id_unique iprinter ls.ls_name)
let print_ls fmt ({ls_name = id} as ls) =
match Ident.sn_decode id.id_string with
| Ident.SNinfix s -> fprintf fmt "(%s)" (escape_op s)
| Ident.SNprefix s when tight_op s -> fprintf fmt "(%s)" (escape_op s)
| Ident.SNprefix s -> fprintf fmt "(%s_)" (left_escape_op s)
| Ident.SNget -> pp_print_string fmt "([])"
| Ident.SNupd -> pp_print_string fmt "([<-])"
| Ident.SNset -> pp_print_string fmt "([]<-)"
| Ident.SNcut -> pp_print_string fmt "([..])"
| Ident.SNlcut -> pp_print_string fmt "([.._])"
| Ident.SNrcut -> pp_print_string fmt "([_..])"
| Ident.SNword _ -> print_raw_ls fmt ls
let print_cs fmt ls =
let sanitizer = Strings.capitalize in
fprintf fmt "%s" (id_unique iprinter ~sanitizer ls.ls_name)
pp_print_string fmt (id_unique iprinter ~sanitizer ls.ls_name)
let print_pr fmt pr =
fprintf fmt "%s" (id_unique pprinter pr.pr_name)
pp_print_string fmt (id_unique pprinter pr.pr_name)
(** Types *)
......@@ -255,7 +256,6 @@ let prio_binop = function
| Timplies -> 1
| Tiff -> 1
let rec print_term fmt t = print_lterm 0 fmt t
and print_lterm pri fmt t =
......@@ -271,38 +271,39 @@ and print_lterm pri fmt t =
else print_tattr pri fmt t in
print_tloc pri fmt t
and print_app pri ls fmt tl =
let s = id_unique iprinter ls.ls_name in
match extract_op s, tl with
| _, [] ->
print_ls fmt ls
| Some s, [t1] when tight_op s ->
and print_app pri ({ls_name = id} as ls) fmt tl =
if tl = [] then print_raw_ls fmt ls else
match Ident.sn_decode id.id_string, tl with
| Ident.SNprefix s, [t1] when tight_op s ->
fprintf fmt (protect_on (pri > 8) "@[%s%a@]")
s (print_lterm 8) t1
| Some s, [t1] ->
| Ident.SNprefix s, [t1] ->
fprintf fmt (protect_on (pri > 5) "@[%s %a@]")
s (print_lterm 6) t1
| Some s, [t1;t2] ->
| Ident.SNinfix s, [t1;t2] ->
fprintf fmt (protect_on (pri > 5) "@[%a@ %s %a@]")
(print_lterm 6) t1 s (print_lterm 6) t2
| _, [t1;t2] when ls.ls_name.id_string = "mixfix []" ->
| Ident.SNget, [t1;t2] ->
fprintf fmt (protect_on (pri > 7) "@[%a@,[%a]@]")
(print_lterm 7) t1 print_term t2
| _, [t1;t2;t3] when ls.ls_name.id_string = "mixfix [<-]" ->
| Ident.SNupd, [t1;t2;t3] ->
fprintf fmt (protect_on (pri > 7) "@[%a@,[%a <-@ %a]@]")
(print_lterm 7) t1 (print_lterm 6) t2 (print_lterm 6) t3
| _, [t1;t2;t3] when ls.ls_name.id_string = "mixfix [..]" ->
| Ident.SNset, [t1;t2;t3] ->
fprintf fmt (protect_on (pri > 5) "@[%a@,[%a] <-@ %a@]")
(print_lterm 6) t1 print_term t2 (print_lterm 6) t3
| Ident.SNcut, [t1;t2;t3] ->
fprintf fmt (protect_on (pri > 7) "%a[%a..%a]")
(print_lterm 7) t1 (print_lterm 6) t2 (print_lterm 6) t3
| _, [t1;t2] when ls.ls_name.id_string = "mixfix [_..]" ->
| Ident.SNrcut, [t1;t2] ->
fprintf fmt (protect_on (pri > 7) "%a[%a..]")
(print_lterm 7) t1 print_term t2
| _, [t1;t2] when ls.ls_name.id_string = "mixfix [.._]" ->
| Ident.SNlcut, [t1;t2] ->
fprintf fmt (protect_on (pri > 7) "%a[..%a]")
(print_lterm 7) t1 print_term t2
| _, tl ->
| _, tl -> (* do not fail if not SNword, just print the string *)
fprintf fmt (protect_on (pri > 6) "@[%a@ %a@]")
print_ls ls (print_list space (print_lterm 7)) tl
print_raw_ls ls (print_list space (print_lterm 7)) tl
and print_tnode pri fmt t = match t.t_node with
| Tvar v ->
......@@ -574,12 +575,12 @@ module NsTree = struct
let k, _ = find_prop_decl kn p in
Leaf (sprint_pkind k ^ " " ^ s) :: acc in
let add_ls s ls acc =
if s = "infix =" && ls_equal ls ps_equ then acc else
if ls_equal ls ps_equ then acc else
Leaf (ls_kind ls ^ " " ^ s) :: acc
in
let add_ts s ts acc =
if s = "int" && ts_equal ts ts_int then acc else
if s = "real" && ts_equal ts ts_real then acc else
if ts_equal ts ts_int then acc else
if ts_equal ts ts_real then acc else
Leaf ("type " ^ s) :: acc
in
let acc = Mstr.fold add_ns ns.ns_ns [] in
......@@ -753,7 +754,7 @@ let () = Exn_printer.register
| Decl.UnboundVar vs ->
fprintf fmt "Unbound variable: %a" print_vsty vs
| Decl.ClashIdent id ->
fprintf fmt "Ident %s is defined twice" id.id_string
fprintf fmt "Ident %s is defined twice" (Ident.str_decode id.id_string)
| Decl.EmptyDecl ->
fprintf fmt "Empty declaration"
| Decl.EmptyAlgDecl ts ->
......@@ -761,12 +762,12 @@ let () = Exn_printer.register
| Decl.EmptyIndDecl ls ->
fprintf fmt "Inductive predicate %a has no constructors" print_ls ls
| Decl.KnownIdent id ->
fprintf fmt "Ident %s is already declared" id.id_string
fprintf fmt "Ident %s is already declared" (Ident.str_decode id.id_string)
| Decl.UnknownIdent id ->
fprintf fmt "Ident %s is not yet declared" id.id_string
fprintf fmt "Ident %s is not yet declared" (Ident.str_decode id.id_string)
| Decl.RedeclaredIdent id ->
fprintf fmt "Ident %s is already declared, with a different declaration"
id.id_string
(Ident.str_decode id.id_string)
| Decl.NoTerminationProof ls ->
fprintf fmt "Cannot prove the termination of %a" print_ls ls
| _ -> raise exn
......
......@@ -966,7 +966,7 @@ let t_eps_close v f = t_eps (t_close_bound v f)
let ps_equ =
let v = ty_var (create_tvsymbol (id_fresh "a")) in
create_psymbol (id_fresh "infix =") [v; v]
create_psymbol (id_fresh (op_infix "=")) [v; v]
let t_equ t1 t2 = ps_app ps_equ [t1; t2]
let t_neq t1 t2 = t_not (ps_app ps_equ [t1; t2])
......@@ -1001,7 +1001,8 @@ let t_tuple tl =
let fs_func_app =
let ty_a = ty_var (create_tvsymbol (id_fresh "a")) in
let ty_b = ty_var (create_tvsymbol (id_fresh "b")) in
create_fsymbol (id_fresh "infix @") [ty_func ty_a ty_b; ty_a] ty_b
let id = id_fresh (op_infix "@") in
create_fsymbol id [ty_func ty_a ty_b; ty_a] ty_b
let t_func_app fn t = t_app_infer fs_func_app [fn; t]
let t_pred_app pr t = t_equ (t_func_app pr t) t_bool_true
......
......@@ -439,7 +439,7 @@ let add_symbol_ts uc ts = add_symbol add_ts ts.ts_name ts uc
let add_symbol_ls uc ({ls_name = id} as ls) =
let {id_string = nm; id_loc = loc} = id in
if (nm = "infix =" || nm = "infix <>") &&
if (nm = Ident.op_equ || nm = Ident.op_neq) &&
uc.uc_path <> ["why3";"BuiltIn"] then
Loc.errorm ?loc "Logical equality cannot be redefined";
add_symbol add_ls id ls uc
......@@ -448,7 +448,8 @@ let add_symbol_pr uc pr = add_symbol add_pr pr.pr_name pr uc
let create_decl d = mk_tdecl (Decl d)
let print_id fmt id = Format.fprintf fmt "%s" id.id_string
let print_id fmt id =
Format.pp_print_string fmt (Ident.str_decode id.id_string)
let warn_dubious_axiom uc k p syms =
match k with
......@@ -961,11 +962,14 @@ let print_meta_arg_type fmt = function
let () = Exn_printer.register
begin fun fmt exn -> match exn with
| NonLocal id ->
Format.fprintf fmt "Non-local symbol: %s" id.id_string
Format.fprintf fmt "Non-local symbol: %s"
(Ident.str_decode id.id_string)
| CannotInstantiate id ->
Format.fprintf fmt "Cannot instantiate a defined symbol %s" id.id_string
Format.fprintf fmt "Cannot instantiate a defined symbol %s"
(Ident.str_decode id.id_string)
| BadInstance id ->
Format.fprintf fmt "Illegal instantiation for symbol %s" id.id_string
Format.fprintf fmt "Illegal instantiation for symbol %s"
(Ident.str_decode id.id_string)
| CloseTheory ->