Commit 359f388e authored by Sylvain Dailler's avatar Sylvain Dailler

Disambiguation of infix and prefix symbol + -> +^ -> +^^ ...

Should solve issue 71.
parent 7bc5d591
module M
use import int.Int
function (+) (x: int) (y : int) : int = x * y
goal g: 2 + 3 = Int.(+) 3 3
end
module M1
use import real.RealInfix
use import int.Int
constant x: int = 0 + 0
(* constant y: real = 0.0 + 0.0 typing error*)
goal g: True
end
module M2
use import real.RealInfix
(* constant y: real = 0.0 + 0.0 typing error*)
goal g: True
end
module M3
use import real.RealInfix
(*constant x: int = 0 + 0 'unbound symbol infix +' *)
goal g: True
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../71_disambiguation.mlw">
<theory name="M" proved="true" sum="bc734e8ea460fb0a12336599478f2cd1">
<goal name="g" proved="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<transf name="compute_in_goal" proved="true" >
</transf>
</goal>
</theory>
<theory name="M1" proved="true" sum="03a869518d4c28a7d6c15bc9acecb5cd">
<goal name="g" proved="true">
<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)">
<goal name="g.0.0">
</goal>
<goal name="g.0.1">
</goal>
</transf>
</goal>
<goal name="g.1">
</goal>
</transf>
</goal>
</theory>
<theory name="M2" sum="85517374ec06b4406222c7e84e769b16">
<goal name="g">
</goal>
</theory>
<theory name="M3" sum="85517374ec06b4406222c7e84e769b16">
<goal name="g">
</goal>
</theory>
</file>
</why3session>
......@@ -191,8 +191,26 @@ type ident_printer = {
blacklist : string list;
}
(* name is already sanitized *)
let find_unique indices name =
let specname ind = name ^ string_of_int ind in
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
in
let testname ind = Hstr.mem indices (specname ind) in
let rec advance ind =
if testname ind then advance (succ ind) else ind in
......
......@@ -79,8 +79,8 @@ let forget_var vs = forget_id iprinter vs.vs_name
(* pretty-print infix and prefix logic symbols *)
let extract_op ls =
let s = ls.ls_name.id_string in
let extract_op s =
(*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
......@@ -109,9 +109,10 @@ let print_ts fmt ts =
let print_ls fmt ls =
if ls.ls_name.id_string = "mixfix []" then fprintf fmt "([])" else
if ls.ls_name.id_string = "mixfix [<-]" then fprintf fmt "([<-])" else
match extract_op ls with
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" (id_unique iprinter ls.ls_name)
| None -> fprintf fmt "%s" s
let print_cs fmt ls =
let sanitizer = Strings.capitalize in
......@@ -212,7 +213,9 @@ and print_lterm pri fmt t =
else print_tlab pri fmt t in
print_tloc pri fmt t
and print_app pri ls fmt tl = match extract_op ls, tl with
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 ->
......@@ -567,12 +570,11 @@ let print_sequent fmt task =
module LegacyPrinter =
(val (let iprinter,aprinter,tprinter,pprinter =
let isanitize = sanitizer char_to_alpha char_to_alnumus in
let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
create_ident_printer why3_keywords ~sanitizer:isanitize,
create_ident_printer why3_keywords ~sanitizer:lsanitize,
create_ident_printer why3_keywords ~sanitizer:lsanitize,
create_ident_printer why3_keywords ~sanitizer:isanitize
let same = fun x -> x in
create_ident_printer why3_keywords ~sanitizer:same,
create_ident_printer why3_keywords ~sanitizer:same,
create_ident_printer why3_keywords ~sanitizer:same,
create_ident_printer why3_keywords ~sanitizer:same
in
create iprinter aprinter tprinter pprinter true))
......
......@@ -144,10 +144,7 @@ let add (d: decl) (tables: naming_table): naming_table =
add_unsafe s (Pr pr) tables
let build_naming_tables task : naming_table =
(** FIXME: using sanitizer here breaks the printing of infix symbols
because it replaces "infix +" by "infix_+", which forbids to
parse transformation arguments containing "+" such as "cut 1+2=3" *)
let isanitizer = None (* Some (sanitizer char_to_alpha char_to_alnumus) *) in
let isanitizer = None (* sanitizer do not seem to be necessary *) in
let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
let pr = create_ident_printer Pretty.why3_keywords ?sanitizer:isanitizer in
let apr = create_ident_printer Pretty.why3_keywords ~sanitizer:lsanitize in
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment