Skip to content

GitLab

why3
why3
Commit 24d15965 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

getting rid of converters, seriously

parent aeecf16b
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 171 additions and 279 deletions
drivers/c.drv
View file @ 24d15965
......@@ -25,7 +25,7 @@ module mach.int.Int32
syntax type int32 "int32_t"
syntax literal int32 "0x%8x"
syntax val of_int "(int32_t)%1"
(* syntax val of_int "(int32_t)%1" *)
syntax val (+) "%1 + %2"
syntax val (-) "%1 - %2"
syntax val (-_) "-%1"
......@@ -226,7 +226,7 @@ module mach.int.Int64
syntax type int64 "int64_t"
syntax literal int64 "0x%16xLL"
syntax val of_int "(int64_t)%1"
(* syntax val of_int "(int64_t)%1" *)
syntax val (+) "%1 + %2"
syntax val (-) "%1 - %2"
syntax val (-_) "-%1"
......@@ -507,9 +507,11 @@ static struct __lsld64_result lsld64(uint64_t x, uint64_t cnt)
return result;
}
"
syntax literal "0x%16xULL"
syntax literal uint64 "0x%16xULL"
(* syntax converter of_int "%1ULL" *)
syntax val uint64_max "0xffffffffffffffffULL"
syntax val (+) "%1 + %2"
syntax val (-) "%1 - %2"
syntax val ( * ) "%1 * %2"
......
drivers/cvc4_bv.gen
View file @ 24d15965
......@@ -6,21 +6,21 @@ theory bv.BV_Gen
end
theory bv.BV64
syntax converter of_int "((_ int2bv 64) %1)"
(*syntax converter of_int "((_ int2bv 64) %1)"*)
syntax function t'int "(bv2nat %1)"
end
theory bv.BV32
syntax converter of_int "((_ int2bv 32) %1)"
(*syntax converter of_int "((_ int2bv 32) %1)"*)
syntax function t'int "(bv2nat %1)"
end
theory bv.BV16
syntax converter of_int "((_ int2bv 16) %1)"
(*syntax converter of_int "((_ int2bv 16) %1)"*)
syntax function t'int "(bv2nat %1)"
end
theory bv.BV8
syntax converter of_int "((_ int2bv 8) %1)"
(*syntax converter of_int "((_ int2bv 8) %1)"*)
syntax function t'int "(bv2nat %1)"
end
drivers/z3_bv.gen
View file @ 24d15965
......@@ -6,7 +6,7 @@ theory bv.BV_Gen
end
theory bv.BV64
syntax converter of_int "((_ int2bv 64) %1)"
(* syntax converter of_int "((_ int2bv 64) %1)" *)
syntax function t'int "(bv2int %1)"
remove prop Nth_bv_is_nth
......@@ -14,7 +14,7 @@ theory bv.BV64
end
theory bv.BV32
syntax converter of_int "((_ int2bv 32) %1)"
(* syntax converter of_int "((_ int2bv 32) %1)" *)
syntax function t'int "(bv2int %1)"
remove prop Nth_bv_is_nth
......@@ -22,7 +22,7 @@ theory bv.BV32
end
theory bv.BV16
syntax converter of_int "((_ int2bv 16) %1)"
(* syntax converter of_int "((_ int2bv 16) %1)" *)
syntax function t'int "(bv2int %1)"
remove prop Nth_bv_is_nth
......@@ -30,7 +30,7 @@ theory bv.BV16
end
theory bv.BV8
syntax converter of_int "((_ int2bv 8) %1)"
(* syntax converter of_int "((_ int2bv 8) %1)" *)
syntax function t'int "(bv2int %1)"
remove prop Nth_bv_is_nth
......
examples/in_progress/multiprecision/mp2.mlw
View file @ 24d15965
This diff is collapsed.
examples/multiprecision/div.mlw
View file @ 24d15965
......@@ -47,8 +47,8 @@ module Div
requires { d >= div radix 2 }
ensures { reciprocal result d }
=
let v = div2by1 (Limb.of_int max_uint64)
((Limb.of_int max_uint64) - d)
let v = div2by1 Limb.uint64_max
(Limb.uint64_max - d)
d in
fact_div (radix * radix - 1) (l2i d) (- radix);
assert { v = (div (radix*radix - 1) (d)) - radix
......@@ -1559,7 +1559,7 @@ let wmpn_divrem_1 (q x:t) (y:limb) (sz:int32) : limb
let nx0 = C.get_ofs !xp 1 in
if [@ex:unlikely] (!x1 = dh && nx0 = dl)
then begin
ql := Limb.of_int Limb.max_uint64;
ql := Limb.uint64_max;
value_sub_concat (pelts x) x.offset xd.offset (xd.offset + p2i sy);
value_sub_tail (pelts xd) xd.offset (xd.offset + p2i sy - 1);
let ghost vlx = value xd (p2i sy - 1) in
......
examples/multiprecision/logical.mlw
View file @ 24d15965
......@@ -259,7 +259,7 @@ module Logical
ensures { result + radix * value r sz
= value x sz * (power 2 (Limb.length - cnt)) }
=
let tnc = (Limb.of_int Limb.length) - cnt in
let tnc = (64:uint64) - cnt in
let msb = sz - 1 in
let xp = ref (C.incr x 0) in
let rp = ref (C.incr r 0) in
......@@ -436,7 +436,7 @@ module Logical
ensures { result + radix * value x sz
= value (old x) sz * (power 2 (Limb.length - cnt)) }
=
let tnc = (Limb.of_int Limb.length) - cnt in
let tnc = (64:uint64) - cnt in
let msb = sz - 1 in
let xp = ref (C.incr x 0) in
let ghost ox = { x } in
......
examples/multiprecision/util.mlw
View file @ 24d15965
......@@ -17,8 +17,8 @@ module Util
ensures { forall j. (j < offset r \/ offset r + sz <= j) ->
(pelts r)[j] = old (pelts r)[j] }
=
let zero = Int32.of_int 0 in
let one = Int32.of_int 1 in
let zero = (0:int32) in
let one = (1:int32) in
let i = ref zero in
let xp = ref (C.incr x zero) in
let rp = ref (C.incr r zero) in
......@@ -49,15 +49,15 @@ module Util
ensures { Int32.to_int result = 1 <-> value x sz = 0 }
=
let i = ref sz in
let uzero = Limb.of_int 0 in
let uzero = (0:uint64) in
let lx = ref uzero in
try
while Int32.(>=) !i (Int32.of_int 1) do
while Int32.(>=) !i (1:int32) do
variant { p2i !i }
invariant { 0 <= !i <= sz }
invariant { value_sub (pelts x) (x.offset + !i) (x.offset + sz)=0 }
let ghost k = p2i !i in
i := Int32.(-) !i (Int32.of_int 1);
i := Int32.(-) !i (1:int32);
assert { 0 <= !i < sz };
lx := get_ofs x !i;
if not (Limb.(=) !lx uzero)
......@@ -65,13 +65,13 @@ module Util
value_sub_concat (pelts x) x.offset (x.offset+k) (x.offset + p2i sz);
value_sub_lower_bound_tight (pelts x) x.offset (x.offset+k);
value_sub_lower_bound (pelts x) (x.offset+k) (x.offset + p2i sz);
raise Return32 (Int32.of_int 0);
raise Return32 (0:int32);
end
else begin
assert { 1+2=3 };
end
done;
Int32.of_int 1
(1:int32)
with Return32 r -> r
end
......@@ -82,8 +82,8 @@ module Util
ensures { forall j. (j < offset r \/ offset r + sz <= j)
-> (pelts r)[j] = old (pelts r)[j] }
=
let i = ref (Int32.of_int 0) in
let lzero = Limb.of_int 0 in
let i = ref (0:int32) in
let lzero = (0:uint64) in
while Int32.(<) !i sz do
invariant { 0 <= !i <= sz }
variant { sz - !i }
......@@ -92,7 +92,7 @@ module Util
-> (pelts r)[j] = old (pelts r)[j] }
set_ofs r !i lzero;
value_sub_tail (pelts r) r.offset (r.offset + p2i !i);
i := Int32.(+) !i (Int32.of_int 1);
i := Int32.(+) !i (1:int32);
done
end
src/core/printer.ml
View file @ 24d15965
......@@ -351,10 +351,8 @@ let print_prelude_for_theory th fmt pm =
exception KnownTypeSyntax of tysymbol
exception KnownLogicSyntax of lsymbol
exception KnownConverterSyntax of lsymbol
exception TooManyTypeOverride of tysymbol
exception TooManyLogicOverride of lsymbol
exception TooManyConverterOverride of lsymbol
let meta_syntax_type = register_meta "syntax_type" [MTtysymbol; MTstring; MTint]
~desc:"Specify@ the@ syntax@ used@ to@ pretty-print@ a@ type@ symbol.@ \
......@@ -366,11 +364,6 @@ let meta_syntax_logic = register_meta "syntax_logic" [MTlsymbol; MTstring; MTint
Can@ be@ specified@ in@ the@ driver@ with@ the@ 'syntax function'@ \
or@ 'syntax predicate'@ rules."
let meta_syntax_converter = register_meta "syntax_converter" [MTlsymbol; MTstring; MTint]
~desc:"Specify@ the@ syntax@ used@ to@ pretty-print@ a@ converter@ \ symbol.@ \
Can@ be@ specified@ in@ the@ driver@ with@ the@ 'syntax converter'@ \
rules."
let meta_syntax_literal = register_meta "syntax_literal" [MTtysymbol; MTstring; MTint]
~desc:"Specify@ the@ syntax@ used@ to@ pretty-print@ a@ range@ literal.@ \
Can@ be@ specified@ in@ the@ driver@ with@ the@ 'syntax literal'@ \
......@@ -402,10 +395,6 @@ let syntax_logic ls s b =
check_syntax_logic ls s;
create_meta meta_syntax_logic [MAls ls; MAstr s; MAint (if b then 1 else 0)]
let syntax_converter ls s b =
check_syntax_logic ls s;
create_meta meta_syntax_converter [MAls ls; MAstr s; MAint (if b then 1 else 0)]
let syntax_literal ts s b =
check_syntax_literal ts s;
create_meta meta_syntax_literal [MAts ts; MAstr s; MAint (if b then 1 else 0)]
......@@ -414,7 +403,6 @@ let remove_prop pr =
create_meta meta_remove_prop [MApr pr]
type syntax_map = (string * int) Mid.t
type converter_map = (string * int) Mls.t
let change_override e e' rs ov = function
| None -> Some (rs,ov)
......@@ -451,13 +439,6 @@ let sm_add_pr sm = function
| [MApr pr] -> Mid.add pr.pr_name ("",0) sm
| _ -> assert false
let cm_add_ls cm = function
| [MAls ls; MAstr rs; MAint ov] ->
Mls.change
(change_override (KnownConverterSyntax ls) (TooManyConverterOverride ls)
rs ov) ls cm
| _ -> assert false
let get_syntax_map task =
let sm = Mid.empty in
let sm = Task.on_meta meta_syntax_type sm_add_ts sm task in
......@@ -465,9 +446,6 @@ let get_syntax_map task =
let sm = Task.on_meta meta_remove_prop sm_add_pr sm task in
sm
let get_converter_map task =
Task.on_meta meta_syntax_converter cm_add_ls Mls.empty task
let get_rliteral_map task =
Task.on_meta meta_syntax_literal sm_add_ts Mid.empty task
......@@ -480,11 +458,6 @@ let add_syntax_map td sm = match td.td_node with
sm_add_pr sm args
| _ -> sm
(*let add_converter_map td cm = match td.td_node with
| Meta (m, args) when meta_equal m meta_syntax_converter ->
cm_add_ls cm args
| _ -> cm*)
let add_rliteral_map td sm = match td.td_node with
| Meta (m, args) when meta_equal m meta_syntax_literal ->
sm_add_ts sm args
......@@ -493,9 +466,6 @@ let add_rliteral_map td sm = match td.td_node with
let query_syntax sm id =
try Some (fst (Mid.find id sm)) with Not_found -> None
let query_converter cm ls =
try Some (fst (Mls.find ls cm)) with Not_found -> None
let on_syntax_map fn =
Trans.on_meta meta_syntax_type (fun sts ->
Trans.on_meta meta_syntax_logic (fun sls ->
......@@ -506,10 +476,6 @@ let on_syntax_map fn =
let sm = List.fold_left sm_add_pr sm spr in
fn sm)))
let on_converter_map fn =
Trans.on_meta meta_syntax_converter (fun scs ->
fn (List.fold_left cm_add_ls Mls.empty scs))
let sprint_tdecl (fn : 'a -> Format.formatter -> tdecl -> 'a * string list) =
let buf = Buffer.create 2048 in
let fmt = Format.formatter_of_buffer buf in
......@@ -568,18 +534,12 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
| KnownLogicSyntax ls ->
fprintf fmt "Syntax for logical symbol %a is already defined"
Pretty.print_ls ls
| KnownConverterSyntax ls ->
fprintf fmt "Converter syntax for logical symbol %a is already defined"
Pretty.print_ls ls
| TooManyTypeOverride ts ->
fprintf fmt "Too many syntax overriding for type symbol %a"
Pretty.print_ts ts
| TooManyLogicOverride ls ->
fprintf fmt "Too many syntax overriding for logic symbol %a"
Pretty.print_ls ls
| TooManyConverterOverride ls ->
fprintf fmt "Too many syntax converter overriding for logic symbol %a"
Pretty.print_ls ls
| BadSyntaxIndex i ->
fprintf fmt "Bad argument index %d, must start with 1" i
| BadSyntaxArity (i1,i2) ->
......
src/core/printer.mli
View file @ 24d15965
......@@ -65,7 +65,6 @@ val print_interface : interface Pp.pp
val meta_syntax_type : meta
val meta_syntax_logic : meta
val meta_syntax_converter : meta
val meta_syntax_literal : meta
val meta_remove_prop : meta
val meta_remove_logic : meta
......@@ -74,7 +73,6 @@ val meta_realized_theory : meta
val syntax_type : tysymbol -> string -> bool -> tdecl
val syntax_logic : lsymbol -> string -> bool -> tdecl
val syntax_converter : lsymbol -> string -> bool -> tdecl
val syntax_literal : tysymbol -> string -> bool -> tdecl
val remove_prop : prsymbol -> tdecl
......@@ -83,19 +81,15 @@ val check_syntax_logic: lsymbol -> string -> unit
type syntax_map = (string*int) Mid.t
(* [syntax_map] maps the idents of removed props to "" *)
type converter_map = (string*int) Mls.t
val get_syntax_map : task -> syntax_map
val add_syntax_map : tdecl -> syntax_map -> syntax_map
(* interprets a declaration as a syntax rule, if any *)
val get_converter_map : task -> converter_map
val get_rliteral_map : task -> syntax_map
val add_rliteral_map : tdecl -> syntax_map -> syntax_map
val query_syntax : syntax_map -> ident -> string option
val query_converter : converter_map -> lsymbol -> string option
val syntax_arguments : string -> 'a Pp.pp -> 'a list Pp.pp
(** (syntax_arguments templ print_arg fmt l) prints in the formatter fmt
......@@ -119,8 +113,6 @@ val syntax_float_literal :
val on_syntax_map : (syntax_map -> 'a Trans.trans) -> 'a Trans.trans
val on_converter_map : (converter_map -> 'a Trans.trans) -> 'a Trans.trans
val sprint_tdecl :
('a -> Format.formatter -> Theory.tdecl -> 'a * string list) ->
Theory.tdecl -> 'a * string list -> 'a * string list
......
src/driver/driver.ml
View file @ 24d15965
......@@ -172,10 +172,6 @@ let load_driver_absolute = let driver_tag = ref (-1) in fun env file extra_files
in
Mid.iter it th.th_local;
th_uc
| Rconverter (q,s,b) ->
let cs = syntax_converter (find_ls th q) s b in
add_meta th cs meta;
th_uc
| Rliteral (q,s,b) ->
let cs = syntax_literal (find_ts th q) s b in
add_meta th cs meta;
......
src/driver/driver_ast.ml
View file @ 24d15965
......@@ -31,7 +31,6 @@ type th_rule =
| Rsyntaxts of qualid * string * bool
| Rsyntaxfs of qualid * string * bool
| Rsyntaxps of qualid * string * bool
| Rconverter of qualid * string * bool
| Rliteral of qualid * string * bool
| Rremovepr of qualid
| Rremoveall
......
src/driver/driver_lexer.mll
View file @ 24d15965
......@@ -50,7 +50,6 @@
"module", MODULE;
"exception", EXCEPTION;
"val", VAL;
"converter", CONVERTER;
"literal", LITERAL;
"use", USE;
]
......
src/driver/driver_parser.mly
View file @ 24d15965
......@@ -27,7 +27,7 @@
%token TIMEOUT OUTOFMEMORY STEPLIMITEXCEEDED TIME STEPS
%token UNDERSCORE LEFTPAR RIGHTPAR DOT DOTDOT QUOTE EOF
%token BLACKLIST
%token MODULE EXCEPTION VAL CONVERTER LITERAL
%token MODULE EXCEPTION VAL LITERAL
%token FUNCTION PREDICATE TYPE PROP ALL FILENAME TRANSFORM PLUGIN
%token COMMA CONSTANT
%token LEFTSQ RIGHTSQ LARROW
......@@ -88,7 +88,6 @@ trule:
| syntax CONSTANT qualid STRING { Rsyntaxfs ($3, $4, $1) }
| syntax FUNCTION qualid STRING { Rsyntaxfs ($3, $4, $1) }
| syntax PREDICATE qualid STRING { Rsyntaxps ($3, $4, $1) }
| syntax CONVERTER qualid STRING { Rconverter ($3, $4, $1) }
| syntax LITERAL qualid STRING { Rliteral ($3, $4, $1) }
| REMOVE PROP qualid { Rremovepr ($3) }
| REMOVE ALL { Rremoveall }
......
src/mlw/cakeml_printer.ml
View file @ 24d15965
......@@ -145,18 +145,15 @@ module Print = struct
List.exists (rs_equal rs) its.itd_constructors in
List.exists is_constructor its
| _ -> false in
match query_syntax info.info_convert rs.rs_name,
query_syntax info.info_syn rs.rs_name, pvl with
| Some s, _, [{e_node = Econst _}] ->
syntax_arguments s print_constant fmt pvl
| _, Some s, _ (* when is_local_id info rs.rs_name *)->
match query_syntax info.info_syn rs.rs_name, pvl with
| Some s, _ (* when is_local_id info rs.rs_name *)->
syntax_arguments s (print_expr ~paren:true info) fmt pvl;
| _, None, tl when is_rs_tuple rs ->
| None, tl when is_rs_tuple rs ->
fprintf fmt "@[(%a)@]"
(print_list comma (print_expr info)) tl
| _, None, [t1] when isfield ->
| None, [t1] when isfield ->
fprintf fmt "%a.%a" (print_expr info) t1 (print_lident info) rs.rs_name
| _, None, tl when isconstructor () -> let pjl = get_record info rs in
| None, tl when isconstructor () -> let pjl = get_record info rs in
begin match pjl, tl with
| [], [] ->
(print_uident info) fmt rs.rs_name
......@@ -171,9 +168,9 @@ module Print = struct
fprintf fmt "@[<hov 2>{ @[%a@] }@]"
(print_list2 semi equal (print_rs info) (print_expr info))
(pjl, tl) end
| _, None, [] ->
| None, [] ->
(print_lident info) fmt rs.rs_name
| _, _, tl ->
| _, tl ->
fprintf fmt "@[<hov 2>%a %a@]" (print_lident info) rs.rs_name
(print_apply_args info) (tl, rs.rs_cty.cty_args)
......@@ -252,12 +249,8 @@ module Print = struct
| Eapp (rs, []) -> (* avoids parenthesis around values *)
fprintf fmt "%a" (print_apply info rs) []
| Eapp (rs, pvl) ->
begin match query_syntax info.info_convert rs.rs_name, pvl with
| Some s, [{e_node = Econst _}] ->
syntax_arguments s print_constant fmt pvl
| _ ->
fprintf fmt (protect_on paren "%a")
(print_apply info rs) pvl end
fprintf fmt (protect_on paren "%a")
(print_apply info rs) pvl
| Ematch (e1, [p, e2], []) ->
fprintf fmt (protect_on paren "let %a =@ %a in@ %a")
(print_pat info) p (print_expr info) e1 (print_expr info) e2
......
src/mlw/cprinter.ml
View file @ 24d15965
......@@ -383,7 +383,6 @@ type info = Pdriver.printer_args = private {
thinterface : Printer.interface_map;
blacklist : Printer.blacklist;
syntax : Printer.syntax_map;
converter : Printer.syntax_map;
literal : Printer.syntax_map; (*TODO handle literals*)
}
......@@ -797,11 +796,8 @@ module MLToC = struct
end
else
let e' =
match
(query_syntax info.syntax rs.rs_name,
query_syntax info.converter rs.rs_name) with
| _, Some s
| Some s, _ ->
match query_syntax info.syntax rs.rs_name with
| Some s ->
begin
try
let _ =
......@@ -823,8 +819,7 @@ module MLToC = struct
| Tyapp (_,args) ->
Array.of_list (List.map (ty_of_ty info) args)
in
C.Esyntax(s,ty_of_ty info rty, rtyargs, params,
Mid.mem rs.rs_name info.converter)
C.Esyntax(s,ty_of_ty info rty, rtyargs, params, false)
with Not_found ->
let args =
List.filter
......@@ -884,6 +879,7 @@ module MLToC = struct
Debug.dprintf debug_c_extraction "propagate constant %s for var %s@."
(BigInt.to_string n) (pv_name pv).id_string;
C.propagate_in_block (pv_name pv) ce (expr info env e)
(*
| Eapp (rs,_) when Mid.mem rs.rs_name info.converter ->
begin match expr info {env with computes_return_value = false} le
with
......@@ -891,6 +887,7 @@ module MLToC = struct
C.propagate_in_block (pv_name pv) se (expr info env e)
| _ -> assert false
end
*)
| _->
let t = ty_of_ty info (ty_of_ity pv.pv_ity) in
match expr info {env with computes_return_value = false} le with
......@@ -1045,9 +1042,8 @@ module MLToC = struct
| Eabsurd -> assert false
| Eassign ([pv, ({rs_field = Some _} as rs), v]) ->
let t =
match (query_syntax info.syntax rs.rs_name,
query_syntax info.converter rs.rs_name) with
| _, Some s | Some s, _ ->
match query_syntax info.syntax rs.rs_name with
| Some s ->
let _ =
try
Str.search_forward
......@@ -1061,9 +1057,8 @@ module MLToC = struct
| Tyapp (_,args) ->
Array.of_list (List.map (ty_of_ty info) args)
in
C.Esyntax(s,ty_of_ty info rty, rtyargs, params,
Mid.mem rs.rs_name info.converter)
| None, None -> raise (Unsupported ("assign not in driver")) in
C.Esyntax(s,ty_of_ty info rty, rtyargs, params, false)
| None -> raise (Unsupported ("assign not in driver")) in
[], C.(Sexpr(Ebinop(Bassign, t, C.Evar v.pv_vs.vs_name)))
| Eassign _ -> raise (Unsupported "assign")
| Ehole | Eany _ -> assert false
......
src/mlw/ml_printer.ml
View file @ 24d15965
......@@ -28,7 +28,6 @@ open Mltree
type info = {
info_syn : syntax_map;
info_convert : syntax_map;
info_literal : syntax_map;
info_current_th : Theory.theory;
info_current_mo : Pmodule.pmodule option;
......@@ -41,7 +40,6 @@ type info = {
let create_info pargs fname ~flat ({mod_theory = th} as m) = {
info_syn = pargs.syntax;
info_convert = pargs.converter;
info_literal = pargs.literal;
info_current_th = th;
info_current_mo = Some m;
......@@ -71,9 +69,8 @@ let rec print_list2 sep sep_m print1 print2 fmt (l1, l2) =
let check_val_in_drv info ({rs_name = {id_loc = loc}} as rs) =
(* here [rs] refers to a [val] declaration *)
match query_syntax info.info_convert rs.rs_name,
query_syntax info.info_syn rs.rs_name with
| None, None (* when info.info_flat *) ->
match query_syntax info.info_syn rs.rs_name with
| None (* when info.info_flat *) ->
Loc.errorm ?loc "Function %a cannot be extracted" Expr.print_rs rs
| _ -> ()
......@@ -185,9 +182,8 @@ module MLPrinter (K: sig val keywords: string list end) = struct
fprintf fmt "%a" (print_lident info) rs.rs_name
let check_type_in_drv info ({id_loc = loc} as ty_id) =
match query_syntax info.info_convert ty_id,
query_syntax info.info_syn ty_id with
| None, None ->
match query_syntax info.info_syn ty_id with
| None ->
Loc.errorm ?loc "Type %a cannot be extracted" (print_lident info) ty_id
| _ -> ()
......
src/mlw/ml_printer.mli
View file @ 24d15965
......@@ -22,7 +22,6 @@ val print_list2 : unit pp -> unit pp -> 'a pp -> 'b pp -> ('a list * 'b list) pp
type info = private {
info_syn : syntax_map;
info_convert : syntax_map;
info_literal : syntax_map;
info_current_th : Theory.theory;
info_current_mo : Pmodule.pmodule option;
......
src/mlw/ocaml_printer.ml
View file @ 24d15965
......@@ -27,7 +27,6 @@ open Printer
type info = {
info_syn : syntax_map;
info_convert : syntax_map;
info_literal : syntax_map;
info_current_th : Theory.theory;
info_current_mo : Pmodule.pmodule option;
......@@ -278,9 +277,8 @@ module Print = struct
let check_val_in_drv info ({rs_name = {id_loc = loc}} as rs) =
(* here [rs] refers to a [val] declaration *)
match query_syntax info.info_convert rs.rs_name,
query_syntax info.info_syn rs.rs_name with
| None, None (* when info.info_flat *) ->
match query_syntax info.info_syn rs.rs_name with
| None (* when info.info_flat *) ->
Loc.errorm ?loc "Function %a cannot be extracted" Expr.print_rs rs
| _ -> ()
......@@ -332,19 +330,16 @@ module Print = struct
List.exists (rs_equal rs) its.itd_constructors in
List.exists is_constructor its
| _ -> false in
match query_syntax info.info_convert rs.rs_name,
query_syntax info.info_syn rs.rs_name, pvl with
| Some s, _, [{e_node = Econst _}] ->
syntax_arguments s print_constant fmt pvl
| _, Some s, _ (* when is_local_id info rs.rs_name *)->
match query_syntax info.info_syn rs.rs_name, pvl with
| Some s, _ (* when is_local_id info rs.rs_name *)->
syntax_arguments s (print_expr ~paren:true info) fmt pvl;
| _, None, [t] when is_rs_tuple rs ->
| None, [t] when is_rs_tuple rs ->
fprintf fmt "@[%a@]" (print_expr info) t
| _, None, tl when is_rs_tuple rs ->
| None, tl when is_rs_tuple rs ->
fprintf fmt "@[(%a)@]" (print_list comma (print_expr info)) tl
| _, None, [t1] when isfield ->
| None, [t1] when isfield ->
fprintf fmt "%a.%a" (print_expr info) t1 (print_lident info) rs.rs_name
| _, None, tl when isconstructor () ->
| None, tl when isconstructor () ->
let pjl = get_record info rs in
begin match pjl, tl with
| [], [] ->
......@@ -359,9 +354,9 @@ module Print = struct
fprintf fmt "@[<hov 2>{ %a }@]"
(print_list2 semi equal (print_rs info)
(print_expr ~paren:true info)) (pjl, tl) end
| _, None, [] ->
| None, [] ->
(print_lident info) fmt rs.rs_name
| _, _, tl ->
| _, tl ->
fprintf fmt "@[<hov 2>%a %a@]"
(print_lident info) rs.rs_name
(print_apply_args info) (tl, rs.rs_cty.cty_args)
......@@ -456,12 +451,8 @@ module Print = struct
| Eapp (rs, []) -> (* avoids parenthesis around values *)
fprintf fmt "%a" (print_apply info rs) []
| Eapp (rs, pvl) ->
begin match query_syntax info.info_convert rs.rs_name, pvl with
| Some s, [{e_node = Econst _}] ->
syntax_arguments s print_constant fmt pvl
| _ ->
fprintf fmt (protect_on paren "%a")
(print_apply info rs) pvl end
fprintf fmt (protect_on paren "%a")
(print_apply info rs) pvl
| Ematch (e1, [p, e2], []) ->
fprintf fmt (protect_on paren "let %a =@ %a in@ %a")
(print_pat info) p (print_expr info) e1 (print_expr info) e2
......@@ -679,7 +670,6 @@ let print_decl =
ignore (old);
let info = {
info_syn = pargs.Pdriver.syntax;
info_convert = pargs.Pdriver.converter;
info_literal = pargs.Pdriver.literal;
info_current_th = th;
info_current_mo = Some m;
......
src/mlw/pdriver.ml
View file @ 24d15965
......@@ -27,7 +27,6 @@ type driver = {
drv_thinterface : Printer.interface_map;
drv_blacklist : Printer.blacklist;
drv_syntax : Printer.syntax_map;
drv_converter : Printer.syntax_map;
drv_literal : Printer.syntax_map;
}
......@@ -38,7 +37,6 @@ type printer_args = {
thinterface : Printer.interface_map;
blacklist : Printer.blacklist;
syntax : Printer.syntax_map;
converter : Printer.syntax_map;
literal : Printer.syntax_map;
}
......@@ -89,7 +87,6 @@ let load_driver env file extra_files =
let thprelude = ref Mid.empty in
let thinterface = ref Mid.empty in
let syntax_map = ref Mid.empty in
let converter_map = ref Mid.empty in
let literal_map = ref Mid.empty in
let qualid = ref [] in
......@@ -110,8 +107,6 @@ let load_driver env file extra_files =
if ls.ls_value <> None then raise (PSymExpected ls) else ls in
let add_syntax id s b =
syntax_map := Mid.add id (s,if b then 1 else 0) !syntax_map in
let add_converter id s b =
converter_map := Mid.add id (s,if b then 1 else 0) !converter_map in
let add_literal id s b =
literal_map := Mid.add id (s,if b then 1 else 0) !literal_map in
let add_local th = function
......@@ -130,8 +125,6 @@ let load_driver env file extra_files =
let ps = find_ps th q in
Printer.check_syntax_logic ps s;
add_syntax ps.ls_name s b
| Rconverter _ ->
Loc.errorm "Syntax converter cannot be used in pure theories"
| Rliteral (q,s,b) ->
let ts = find_ts th q in
add_literal ts.ts_name s b
......@@ -194,9 +187,6 @@ let load_driver env file extra_files =
| MRval (q,s) ->