Commit 295cacf4 authored by Andrei Paskevich's avatar Andrei Paskevich

Ident: disambiguated symbolic notation

It is possible to append an arbitary number of quote symbols
at the end of an prefix/infix/mixfix operator:

            applied form      standalone form

              -' 42               (-'_)
              x +' y              (+')
              a[0]' <- 1          ([]'<-)

Pretty-printing will use the quote symbols for disambiguation.

The derived symbols can be produced by Why3 by appending
a suffix of the form "_toto" or "'toto". These symbols can
be parsed/printed as "(+)_toto" or "(+)'toto", respectively.
parent 4bfdab0d
......@@ -591,7 +591,7 @@
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Pow2_int_real.0.1" expl="recursive case" proved="true">
<transf name="replace" proved="true" arg1="x" arg2="((x-^1)+^1)">
<transf name="replace" proved="true" arg1="x" arg2="((x-'1)+'1)">
<goal name="Pow2_int_real.0.1.0" expl="recursive case" proved="true">
<proof prover="7" timelimit="1"><result status="valid" time="0.12" steps="135"/></proof>
</goal>
......
......@@ -16,7 +16,7 @@
<proof prover="0"><result status="valid" time="0.00"/></proof>
<transf name="cut" arg1="(0 + 0 = 2)">
<goal name="g.0">
<transf name="cut" arg1="(1.0 +^ 1.3 = 2.2)">
<transf name="cut" arg1="(1.0 +' 1.3 = 2.2)">
<goal name="g.0.0">
</goal>
<goal name="g.0.1">
......
......@@ -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.op_get]
let array_get = mk_qid ["Array"; Ident.op_get ""]
let array_set = mk_qid ["Array"; Ident.op_set]
let array_set = mk_qid ["Array"; Ident.op_set ""]
let d3 =
let id_a = mk_ident "a" in
......
......@@ -29,8 +29,8 @@ let mk_id ~loc name =
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 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 }
......
......@@ -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.op_get s e)
let upd_op s e = Qident (mk_id Ident.op_upd 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_update "") s e)
let empty_spec = {
sp_pre = []; sp_post = []; sp_xpost = [];
......
......@@ -53,130 +53,100 @@ type notation =
| SNword of string
| SNinfix of string
| SNprefix of string
| SNget (* [] *)
| SNset (* []<- *)
| SNupd (* [<-] *)
| SNcut (* [..] *)
| SNlcut (* [.._] *)
| SNrcut (* [_..] *)
| SNget of string (* [] *)
| SNset of string (* []<- *)
| SNupdate of string (* [<-] *)
| SNcut of string (* [..] *)
| SNlcut of string (* [.._] *)
| SNrcut of string (* [_..] *)
(* current encoding *)
let op_infix s = "infix " ^ s
let op_prefix s = "prefix " ^ s
let op_get s = "mixfix []" ^ s
let op_set s = "mixfix []<-" ^ s
let op_update s = "mixfix [<-]" ^ s
let op_cut s = "mixfix [..]" ^ s
let op_lcut s = "mixfix [.._]" ^ s
let op_rcut s = "mixfix [_..]" ^ 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 <= 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 <> "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
| 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 -> "([_..])"
| SNget s -> op_get s
| SNset s -> op_set s
| SNupdate s -> op_update s
| SNcut s -> op_cut s
| SNlcut s -> op_lcut s
| SNrcut s -> op_rcut s
| SNword s -> s
let print_sn fmt w =
let lspace p = if p.[0] = '*' then " " else "" in
let rspace p = if p.[String.length p - 1] = '*' then " " else "" in
match w with (* infix/prefix never empty, mixfix never have stars *)
| SNinfix p -> Format.fprintf fmt "(%s%s%s)" (lspace p) p (rspace p)
| SNprefix p when p.[0] = '!' || p.[0] = '?' ->
Format.fprintf fmt "(%s%s)" p (rspace p)
| SNprefix p -> Format.fprintf fmt "(%s%s_)" (lspace p) p
| SNget p -> Format.fprintf fmt "([]%s)" p
| SNset p -> Format.fprintf fmt "([]%s<-)" p
| SNupdate p -> Format.fprintf fmt "([<-]%s)" p
| SNcut p -> Format.fprintf fmt "([..]%s)" p
| SNlcut p -> Format.fprintf fmt "([.._]%s)" p
| SNrcut p -> Format.fprintf fmt "([_..]%s)" p
| SNword p -> Format.pp_print_string fmt p
(* The function below recognizes the following strings as notations:
"infix " (opchar+ [']* as p) (['_] [^'_] .* as q)
"prefix " (opchar+ [']* as p) (['_] [^'_] .* as q)
"mixfix [" .* "]" opchar* ([']* as p) (['_] [^'_] .* as q)
It will fail if you add a mixfix that contains a non-opchar after
the closing square bracket, or a mixfix that does have brackets.
Be careful when working with this code, it may eat your brain. *)
let sn_decode s =
let len = String.length s in
if len <= 6 then SNword s else
let k = let prf = String.sub s 0 6 in
if prf = "infix " then 6 else
if len <= 7 || s.[6] <> ' ' then 0 else
if prf = "prefix" then 7 else
if len <= 8 || s.[7] <> '[' then 0 else
if prf <> "mixfix" then 0 else
try succ (String.index_from s 8 ']')
with Not_found -> 0 in
if k = 0 then SNword s else
let rec skip_opchar i =
if i = len then i else match s.[i] with
| '@' | '!' | '^' | '$' | '=' | '%' | '>' | '#'
| '.' | '<' | '-' | '&' | '/' | '+' | '?' | ':'
| '*' | '~' | '|' | '\\' -> skip_opchar (succ i)
| _ -> i in
let l = skip_opchar k in
if l = k && k < 8 then SNword s else
let rec skip_quote i =
if i = len || s.[i] <> '\'' then i else skip_quote (succ i) in
let m = skip_quote l in
let m = if l < m && m < len && s.[m] <> '_' then pred m else m in
let w = if k = 6 then SNinfix (String.sub s 6 (m - 6)) else
if k = 7 then SNprefix (String.sub s 7 (m - 7)) else
let p = if l < m then String.sub s l (m - l) else "" in
match String.sub s 8 (l - 8) with
| "]" -> SNget p | "]<-" -> SNset p | "<-]" -> SNupdate p
| "..]" -> SNcut p | ".._]" -> SNlcut p | "_..]" -> SNrcut p
| _ -> SNword (if m = len then s else String.sub s 0 m) in
if m = len then w (* no appended suffix *) else
if s.[m] <> '\'' && s.[m] <> '_' then SNword s else
let p = print_sn Format.str_formatter w;
Format.flush_str_formatter () in
SNword (p ^ String.sub s m (len - m))
let print_decoded fmt s = print_sn fmt (sn_decode s)
(** Identifiers *)
......@@ -254,29 +224,20 @@ type ident_printer = {
let find_unique indices name =
let specname 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 =
sanitized for provers, 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
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
*)
match sn_decode name with
| SNinfix s -> op_infix (s ^ String.make ind '\'')
| SNprefix s -> op_prefix (s ^ String.make ind '\'')
| SNget s -> op_get (s ^ String.make ind '\'')
| SNset s -> op_set (s ^ String.make ind '\'')
| SNupdate s -> op_update (s ^ String.make ind '\'')
| SNcut s -> op_cut (s ^ String.make ind '\'')
| SNlcut s -> op_lcut (s ^ String.make ind '\'')
| SNrcut s -> op_rcut (s ^ String.make ind '\'')
| SNword _ -> 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
......
......@@ -35,12 +35,12 @@ type notation =
| SNword of string
| SNinfix of string
| SNprefix of string
| SNget (* [] *)
| SNset (* []<- *)
| SNupd (* [<-] *)
| SNcut (* [..] *)
| SNlcut (* [.._] *)
| SNrcut (* [_..] *)
| SNget of string (* [] *)
| SNset of string (* []<- *)
| SNupdate of string (* [<-] *)
| SNcut of string (* [..] *)
| SNlcut of string (* [.._] *)
| SNrcut of string (* [_..] *)
val sn_encode : notation -> string
(* encode the symbol name as a string *)
......@@ -48,22 +48,21 @@ val sn_encode : notation -> string
val sn_decode : string -> notation
(* decode the string as a symbol name *)
val str_decode : string -> string
val print_decoded : Format.formatter -> string -> unit
(* 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
val op_get : string -> string
val op_set : string -> string
val op_update : string -> string
val op_cut : string -> string
val op_lcut : string -> string
val op_rcut : string -> string
val op_equ : string
val op_neq : string
(** {2 Identifiers} *)
......
......@@ -136,12 +136,6 @@ let forget_var vs = forget_id iprinter vs.vs_name
let tight_op s =
s <> "" && (let c = String.get s 0 in c = '!' || c = '?')
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
......@@ -151,28 +145,15 @@ let print_ts fmt ts =
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
pp_print_string fmt (id_unique iprinter ~sanitizer ls.ls_name)
let print_ls fmt ls =
Ident.print_decoded fmt (id_unique iprinter ls.ls_name)
let print_pr fmt pr =
pp_print_string fmt (id_unique pprinter pr.pr_name)
Ident.print_decoded fmt (id_unique pprinter pr.pr_name)
(** Types *)
......@@ -271,9 +252,10 @@ and print_lterm pri fmt t =
else print_tattr pri fmt t in
print_tloc pri fmt t
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
and print_app pri ls fmt tl =
if tl = [] then print_ls fmt ls else
let s = id_unique iprinter ls.ls_name in
match Ident.sn_decode s, tl with
| Ident.SNprefix s, [t1] when tight_op s ->
fprintf fmt (protect_on (pri > 8) "@[%s%a@]")
s (print_lterm 8) t1
......@@ -283,27 +265,30 @@ and print_app pri ({ls_name = id} as ls) fmt tl =
| Ident.SNinfix s, [t1;t2] ->
fprintf fmt (protect_on (pri > 5) "@[%a@ %s %a@]")
(print_lterm 6) t1 s (print_lterm 6) t2
| Ident.SNget, [t1;t2] ->
fprintf fmt (protect_on (pri > 7) "@[%a@,[%a]@]")
(print_lterm 7) t1 print_term t2
| 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
| 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
| Ident.SNrcut, [t1;t2] ->
fprintf fmt (protect_on (pri > 7) "%a[%a..]")
(print_lterm 7) t1 print_term t2
| Ident.SNlcut, [t1;t2] ->
fprintf fmt (protect_on (pri > 7) "%a[..%a]")
(print_lterm 7) t1 print_term t2
| _, tl -> (* do not fail if not SNword, just print the string *)
fprintf fmt (protect_on (pri > 6) "@[%a@ %a@]")
print_raw_ls ls (print_list space (print_lterm 7)) tl
| Ident.SNget s, [t1;t2] ->
fprintf fmt (protect_on (pri > 7) "@[%a@,[%a]%s@]")
(print_lterm 7) t1 print_term t2 s
| Ident.SNupdate s, [t1;t2;t3] ->
fprintf fmt (protect_on (pri > 7) "@[%a@,[%a <-@ %a]%s@]")
(print_lterm 7) t1 (print_lterm 6) t2 (print_lterm 6) t3 s
| Ident.SNset s, [t1;t2;t3] ->
fprintf fmt (protect_on (pri > 5) "@[%a@,[%a]%s <-@ %a@]")
(print_lterm 6) t1 print_term t2 s (print_lterm 6) t3
| Ident.SNcut s, [t1;t2;t3] ->
fprintf fmt (protect_on (pri > 7) "%a[%a..%a]%s")
(print_lterm 7) t1 (print_lterm 6) t2 (print_lterm 6) t3 s
| Ident.SNrcut s, [t1;t2] ->
fprintf fmt (protect_on (pri > 7) "%a[%a..]%s")
(print_lterm 7) t1 print_term t2 s
| Ident.SNlcut s, [t1;t2] ->
fprintf fmt (protect_on (pri > 7) "%a[..%a]%s")
(print_lterm 7) t1 print_term t2 s
| Ident.SNword s, tl ->
fprintf fmt (protect_on (pri > 6) "@[%s@ %a@]")
s (print_list space (print_lterm 7)) tl
| _, tl -> (* do not fail, just print the string *)
fprintf fmt (protect_on (pri > 6) "@[%s@ %a@]")
s (print_list space (print_lterm 7)) tl
and print_tnode pri fmt t = match t.t_node with
| Tvar v ->
......@@ -754,20 +739,20 @@ 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" (Ident.str_decode id.id_string)
fprintf fmt "Ident %a is defined twice" Ident.print_decoded id.id_string
| Decl.EmptyDecl ->
fprintf fmt "Empty declaration"
| Decl.EmptyAlgDecl ts ->
fprintf fmt "Algebraic type %a has no constructors" print_ts ts
| Decl.EmptyIndDecl ls ->
fprintf fmt "Inductive predicate %a has no constructors" print_ls ls
| Decl.KnownIdent id ->
fprintf fmt "Ident %s is already declared" (Ident.str_decode id.id_string)
| Decl.UnknownIdent id ->
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"
(Ident.str_decode id.id_string)
| Decl.KnownIdent {id_string = s} ->
fprintf fmt "Ident %a is already declared" Ident.print_decoded s
| Decl.UnknownIdent {id_string = s} ->
fprintf fmt "Ident %a is not yet declared" Ident.print_decoded s
| Decl.RedeclaredIdent {id_string = s} ->
fprintf fmt "Ident %a is already declared, with a different declaration"
Ident.print_decoded s
| Decl.NoTerminationProof ls ->
fprintf fmt "Cannot prove the termination of %a" print_ls ls
| _ -> raise exn
......
......@@ -448,8 +448,7 @@ 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.pp_print_string fmt (Ident.str_decode id.id_string)
let print_id fmt id = Ident.print_decoded fmt id.id_string
let warn_dubious_axiom uc k p syms =
match k with
......@@ -962,14 +961,11 @@ 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"
(Ident.str_decode id.id_string)
Format.fprintf fmt "Non-local symbol: %a" print_id id
| CannotInstantiate id ->
Format.fprintf fmt "Cannot instantiate a defined symbol %s"
(Ident.str_decode id.id_string)
Format.fprintf fmt "Cannot instantiate a defined symbol %a" print_id id
| BadInstance id ->
Format.fprintf fmt "Illegal instantiation for symbol %s"
(Ident.str_decode id.id_string)
Format.fprintf fmt "Illegal instantiation for symbol %a" print_id id
| CloseTheory ->
Format.fprintf fmt "Cannot close theory: some namespaces are still open"
| NoOpenedNamespace ->
......
......@@ -61,7 +61,7 @@ let alpha = ['a'-'z' 'A'-'Z' '_']
let digit = ['0'-'9']
let ident = alpha (alpha | digit | '\'')*
let op_char = ['=' '<' '>' '~' '+' '-' '*' '/' '%'
let op_char = ['=' '<' '>' '~' '+' '-' '*' '/' '%' '\\'
'!' '$' '&' '?' '@' '^' '.' ':' '|' '#']
rule token = parse
......@@ -97,11 +97,15 @@ rule token = parse
{ COMMA }
| "'"
{ QUOTE }
| op_char+ as op
| "]" ("'"+ as s)
{ RIGHTSQ_QUOTE s }
| ")" (['\'' '_'] ident as s)
{ RIGHTPAR_QUOTE s }
| op_char+ "'"* as op
{ OPERATOR op }
| "\""
| '"'
{ STRING (Lexlib.string lexbuf) }
| "import" space* "\""
| "import" space* '"'
{ INPUT (Lexlib.string lexbuf) }
| eof
{ EOF }
......
......@@ -18,6 +18,8 @@
%token <string> IDENT
%token <string> STRING
%token <string> OPERATOR
%token <string> RIGHTSQ_QUOTE
%token <string> RIGHTPAR_QUOTE
%token <string> INPUT (* never reaches the parser *)
%token THEORY END SYNTAX REMOVE META PRELUDE PRINTER MODEL_PARSER OVERRIDING USE
%token INTERFACE
......@@ -135,18 +137,24 @@ ident:
| PLUGIN { "plugin" }
ident_rich:
| ident { $1 }
| LEFTPAR operator RIGHTPAR { $2 }
| ident { $1 }
| LEFTPAR operator RIGHTPAR { $2 }
| LEFTPAR operator RIGHTPAR_QUOTE { $2 ^ $3 }
operator:
| OPERATOR { Ident.op_infix $1 }
| o = OPERATOR { if o.[0] <> '!' && o.[0] <> '?' then
Ident.op_infix o else Ident.op_prefix o }
| OPERATOR UNDERSCORE { Ident.op_prefix $1 }
| LEFTSQ RIGHTSQ { Ident.op_get }
| LEFTSQ LARROW RIGHTSQ { Ident.op_upd }
| LEFTSQ RIGHTSQ LARROW { Ident.op_set }
| LEFTSQ DOTDOT RIGHTSQ { Ident.op_cut }
| LEFTSQ UNDERSCORE DOTDOT RIGHTSQ { Ident.op_rcut }
| LEFTSQ DOTDOT UNDERSCORE RIGHTSQ { Ident.op_lcut }
| LEFTSQ rightsq { Ident.op_get $2 }
| LEFTSQ rightsq LARROW { Ident.op_set $2 }
| LEFTSQ LARROW rightsq { Ident.op_update $3 }
| LEFTSQ DOTDOT rightsq { Ident.op_cut $3 }
| LEFTSQ UNDERSCORE DOTDOT rightsq { Ident.op_rcut $4 }
| LEFTSQ DOTDOT UNDERSCORE rightsq { Ident.op_lcut $4 }
rightsq:
| RIGHTSQ { "" }
| RIGHTSQ_QUOTE { $1 }
(* Types *)
......
......@@ -272,10 +272,10 @@ let array_module : Pmodule.pmodule =
let array_type : Ity.itysymbol =
Pmodule.ns_find_its array_module.Pmodule.mod_export ["array"]
let array_get : Term.lsymbol = find array_module Ident.op_get
let array_get : Term.lsymbol = find array_module (Ident.op_get "")
let array_length : Term.lsymbol = find array_module "length"
let array_get_fun : Expr.rsymbol = find_rs array_module Ident.op_get
let array_set_fun : Expr.rsymbol = find_rs array_module Ident.op_set
let array_get_fun : Expr.rsymbol = find_rs array_module (Ident.op_get "")
let array_set_fun : Expr.rsymbol = find_rs array_module (Ident.op_set "")
(*********)
......
......@@ -1154,8 +1154,7 @@ let ls_decr_of_rec_defn = function
open Format
open Pretty
let sprinter = create_ident_printer []
~sanitizer:(sanitizer char_to_alpha char_to_alnumus)
let sprinter = create_ident_printer [] ~sanitizer:(fun x -> x)
let id_of_rs s = match s.rs_logic with
| RLnone | RLlemma -> s.rs_name
......@@ -1175,30 +1174,12 @@ let forget_let_defn = function
let tight_op s =
s <> "" && (let c = String.get s 0 in c = '!' || c = '?')
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
let print_normal_rs fmt s = match s.rs_logic with
| RLnone | RLlemma -> pp_print_string fmt (id_unique sprinter s.rs_name)
let print_rs fmt s = match s.rs_logic with
| RLnone | RLlemma ->
Ident.print_decoded fmt (id_unique sprinter s.rs_name)
| RLpv v -> print_pv fmt v
| RLls s -> print_ls fmt s
let print_rs fmt ({rs_name = id} as s) =
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_normal_rs fmt s
let print_rs_head fmt s = fprintf fmt "%s%s%a%a"
(if s.rs_cty.cty_effect.eff_ghost then "ghost " else "")
(match s.rs_logic with
......@@ -1246,9 +1227,10 @@ let ambig_ls s =
let ht_rs = Hrs.create 7 (* rec_rsym -> rec_sym *)
let print_capp pri ({rs_name = id} as s) fmt vl =
if vl = [] then print_normal_rs fmt s else
match Ident.sn_decode id.id_string, vl with
let print_capp pri s fmt vl =
if vl = [] then print_rs fmt s else
let p = id_unique sprinter s.rs_name in
match Ident.sn_decode p, vl with
| Ident.SNprefix o, [t1] when tight_op o ->
fprintf fmt (protect_on (pri > 7) "%s%a") o print_pv t1
| Ident.SNprefix o, [t1] ->
......@@ -1256,24 +1238,27 @@ let print_capp pri ({rs_name = id} as s) fmt vl =
| Ident.SNinfix o, [t1;t2] ->
fprintf fmt (protect_on (pri > 4) "@[<hov 1>%a %s@ %a@]")
print_pv t1 o print_pv t2
| Ident.SNget, [t1;t2] ->
fprintf fmt (protect_on (pri > 6) "%a[%a]") print_pv t1 print_pv t2
| Ident.SNupd, [t1;t2;t3] ->
fprintf fmt (protect_on (pri > 6) "%a[%a <- %a]")
print_pv t1 print_pv t2 print_pv t3
| Ident.SNset, [t1;t2;t3] ->
fprintf fmt (protect_on (pri > 0) "%a[%a] <- %a")
print_pv t1 print_pv t2 print_pv t3
| Ident.SNcut, [t1;t2;t3] ->
fprintf fmt (protect_on (pri > 6) "%a[%a..%a]")
print_pv t1 print_pv t2 print_pv t3
| Ident.SNrcut, [t1;t2] ->
fprintf fmt (protect_on (pri > 6) "%a[%a..]") print_pv t1 print_pv t2
| Ident.SNlcut, [t1;t2] ->
fprintf fmt (protect_on (pri > 6) "%a[..%a]") print_pv t1 print_pv t2