Commit 7487f2a1 authored by Clément Fumex's avatar Clément Fumex

Syntax converter for theories

parent e7298595
...@@ -196,7 +196,7 @@ theory bv.BV32 ...@@ -196,7 +196,7 @@ theory bv.BV32
(* (bv2nat %1) *) (* (bv2nat %1) *)
(* (- (bv2nat %1) 4294967296))" *) (* (- (bv2nat %1) 4294967296))" *)
(* syntax function of_int "((_ int2bv 32) %1)" *) (* syntax function of_int "((_ int2bv 32) %1)" *)
syntax function of_int_const "((_ int2bv 32) %1)" syntax converter of_int_const "((_ int2bv 32) %1)"
(* syntax function nth "(= ((_ extract 0 0) (bvlshr %1 ((_ int2bv 32) %2))) #b1)" *) (* syntax function nth "(= ((_ extract 0 0) (bvlshr %1 ((_ int2bv 32) %2))) #b1)" *)
(* syntax function nth_bv "(= ((_ extract 0 0) (bvlshr %1 %2)) #b1)" *) (* syntax function nth_bv "(= ((_ extract 0 0) (bvlshr %1 %2)) #b1)" *)
syntax predicate eq "(= %1 %2)" syntax predicate eq "(= %1 %2)"
...@@ -266,7 +266,7 @@ theory bv.BV32Ax ...@@ -266,7 +266,7 @@ theory bv.BV32Ax
(* (bv2nat %1) *) (* (bv2nat %1) *)
(* (- (bv2nat %1) 4294967296))" *) (* (- (bv2nat %1) 4294967296))" *)
(* syntax function of_int "((_ int2bv 32) %1)" *) (* syntax function of_int "((_ int2bv 32) %1)" *)
syntax function of_int_const "((_ int2bv 32) %1)" syntax converter of_int_const "((_ int2bv 32) %1)"
(* syntax function nth "(= ((_ extract 0 0) (bvlshr %1 ((_ int2bv 32) %2))) #b1)" *) (* syntax function nth "(= ((_ extract 0 0) (bvlshr %1 ((_ int2bv 32) %2))) #b1)" *)
(* syntax function nth_bv "(= ((_ extract 0 0) (bvlshr %1 %2)) #b1)" *) (* syntax function nth_bv "(= ((_ extract 0 0) (bvlshr %1 %2)) #b1)" *)
syntax predicate eq "(= %1 %2)" syntax predicate eq "(= %1 %2)"
...@@ -330,7 +330,7 @@ theory bv.BV64 ...@@ -330,7 +330,7 @@ theory bv.BV64
syntax function lsr_bv "(bvlshr %1 %2)" syntax function lsr_bv "(bvlshr %1 %2)"
syntax function lsl_bv "(bvshl %1 %2)" syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)" syntax function asr_bv "(bvashr %1 %2)"
syntax function of_int_const "((_ int2bv 64) %1)" syntax converter of_int_const "((_ int2bv 64) %1)"
syntax predicate eq "(= %1 %2)" syntax predicate eq "(= %1 %2)"
syntax predicate slt "(bvslt %1 %2)" syntax predicate slt "(bvslt %1 %2)"
...@@ -372,7 +372,7 @@ theory bv.BV16 ...@@ -372,7 +372,7 @@ theory bv.BV16
syntax function lsr_bv "(bvlshr %1 %2)" syntax function lsr_bv "(bvlshr %1 %2)"
syntax function lsl_bv "(bvshl %1 %2)" syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)" syntax function asr_bv "(bvashr %1 %2)"
syntax function of_int_const "((_ int2bv 16) %1)" syntax converter of_int_const "((_ int2bv 16) %1)"
syntax predicate eq "(= %1 %2)" syntax predicate eq "(= %1 %2)"
syntax predicate slt "(bvslt %1 %2)" syntax predicate slt "(bvslt %1 %2)"
...@@ -414,7 +414,7 @@ theory bv.BV8 ...@@ -414,7 +414,7 @@ theory bv.BV8
syntax function lsr_bv "(bvlshr %1 %2)" syntax function lsr_bv "(bvlshr %1 %2)"
syntax function lsl_bv "(bvshl %1 %2)" syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)" syntax function asr_bv "(bvashr %1 %2)"
syntax function of_int_const "((_ int2bv 8) %1)" syntax converter of_int_const "((_ int2bv 8) %1)"
syntax predicate eq "(= %1 %2)" syntax predicate eq "(= %1 %2)"
syntax predicate slt "(bvslt %1 %2)" syntax predicate slt "(bvslt %1 %2)"
......
...@@ -206,6 +206,7 @@ let print_prelude_for_theory th fmt pm = ...@@ -206,6 +206,7 @@ let print_prelude_for_theory th fmt pm =
exception KnownTypeSyntax of tysymbol exception KnownTypeSyntax of tysymbol
exception KnownLogicSyntax of lsymbol exception KnownLogicSyntax of lsymbol
exception KnownConverterSyntax of lsymbol
let meta_syntax_type = register_meta "syntax_type" [MTtysymbol; MTstring] let meta_syntax_type = register_meta "syntax_type" [MTtysymbol; MTstring]
~desc:"Specify@ the@ syntax@ used@ to@ pretty-print@ a@ type@ symbol.@ \ ~desc:"Specify@ the@ syntax@ used@ to@ pretty-print@ a@ type@ symbol.@ \
...@@ -217,9 +218,14 @@ let meta_syntax_logic = register_meta "syntax_logic" [MTlsymbol; MTstring] ...@@ -217,9 +218,14 @@ let meta_syntax_logic = register_meta "syntax_logic" [MTlsymbol; MTstring]
Can@ be@ specified@ in@ the@ driver@ with@ the@ 'syntax function'@ \ Can@ be@ specified@ in@ the@ driver@ with@ the@ 'syntax function'@ \
or@ 'syntax predicate'@ rules." or@ 'syntax predicate'@ rules."
let meta_syntax_converter = register_meta "syntax_converter" [MTlsymbol; MTstring]
~desc:"Specify@ the@ syntax@ used@ to@ pretty-print@ a@ converter@ \ symbol.@ \
Can@ be@ specified@ in@ the@ driver@ with@ the@ 'syntax converter'@ \
rules."
let meta_remove_prop = register_meta "remove_prop" [MTprsymbol] let meta_remove_prop = register_meta "remove_prop" [MTprsymbol]
~desc:"Remove@ a@ logical@ proposition@ from@ proof@ obligations.@ \ ~desc:"Remove@ a@ logical@ proposition@ from@ proof@ obligations.@ \
Can@ be@ specified@ in@ the@ driver@ with@ the@ 'remove prop'@ rule." Can@ be@ specified@ in@ the@ driver@ with@ the@ 'remove prop'@ rule."
let meta_remove_type = register_meta "remove_type" [MTtysymbol] let meta_remove_type = register_meta "remove_type" [MTtysymbol]
~desc:"Remove@ a@ type@ symbol@ from@ proof@ obligations.@ \ ~desc:"Remove@ a@ type@ symbol@ from@ proof@ obligations.@ \
...@@ -243,10 +249,15 @@ let syntax_logic ls s = ...@@ -243,10 +249,15 @@ let syntax_logic ls s =
check_syntax_logic ls s; check_syntax_logic ls s;
create_meta meta_syntax_logic [MAls ls; MAstr s] create_meta meta_syntax_logic [MAls ls; MAstr s]
let syntax_converter ls s =
check_syntax_logic ls s;
create_meta meta_syntax_converter [MAls ls; MAstr s]
let remove_prop pr = let remove_prop pr =
create_meta meta_remove_prop [MApr pr] create_meta meta_remove_prop [MApr pr]
type syntax_map = string Mid.t type syntax_map = string Mid.t
type converter_map = string Mls.t
let sm_add_ts sm = function let sm_add_ts sm = function
| [MAts ts; MAstr rs] -> Mid.add_new (KnownTypeSyntax ts) ts.ts_name rs sm | [MAts ts; MAstr rs] -> Mid.add_new (KnownTypeSyntax ts) ts.ts_name rs sm
...@@ -260,6 +271,10 @@ let sm_add_pr sm = function ...@@ -260,6 +271,10 @@ let sm_add_pr sm = function
| [MApr pr] -> Mid.add pr.pr_name "" sm | [MApr pr] -> Mid.add pr.pr_name "" sm
| _ -> assert false | _ -> assert false
let cm_add_ls cm = function
| [MAls ls; MAstr rs] -> Mls.add_new (KnownConverterSyntax ls) ls rs cm
| _ -> assert false
let get_syntax_map task = let get_syntax_map task =
let sm = Mid.empty in let sm = Mid.empty in
let sm = Task.on_meta meta_syntax_type sm_add_ts sm task in let sm = Task.on_meta meta_syntax_type sm_add_ts sm task in
...@@ -267,14 +282,23 @@ let get_syntax_map task = ...@@ -267,14 +282,23 @@ let get_syntax_map task =
let sm = Task.on_meta meta_remove_prop sm_add_pr sm task in let sm = Task.on_meta meta_remove_prop sm_add_pr sm task in
sm sm
let get_converter_map task =
Task.on_meta meta_syntax_converter cm_add_ls Mls.empty task
let add_syntax_map td sm = match td.td_node with let add_syntax_map td sm = match td.td_node with
| Meta (m, args) when meta_equal m meta_syntax_type -> sm_add_ts sm args | Meta (m, args) when meta_equal m meta_syntax_type -> sm_add_ts sm args
| Meta (m, args) when meta_equal m meta_syntax_logic -> sm_add_ls sm args | Meta (m, args) when meta_equal m meta_syntax_logic -> sm_add_ls sm args
| Meta (m, args) when meta_equal m meta_remove_prop -> sm_add_pr sm args | Meta (m, args) when meta_equal m meta_remove_prop -> sm_add_pr sm args
| _ -> sm | _ -> 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 query_syntax sm id = Mid.find_opt id sm let query_syntax sm id = Mid.find_opt id sm
let query_converter cm ls = Mls.find_opt ls cm
let on_syntax_map fn = let on_syntax_map fn =
Trans.on_meta meta_syntax_type (fun sts -> Trans.on_meta meta_syntax_type (fun sts ->
Trans.on_meta meta_syntax_logic (fun sls -> Trans.on_meta meta_syntax_logic (fun sls ->
...@@ -285,6 +309,10 @@ let on_syntax_map fn = ...@@ -285,6 +309,10 @@ let on_syntax_map fn =
let sm = List.fold_left sm_add_pr sm spr in let sm = List.fold_left sm_add_pr sm spr in
fn sm))) 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 sprint_tdecl (fn : 'a -> Format.formatter -> tdecl -> 'a * string list) =
let buf = Buffer.create 2048 in let buf = Buffer.create 2048 in
let fmt = Format.formatter_of_buffer buf in let fmt = Format.formatter_of_buffer buf in
...@@ -341,6 +369,9 @@ let () = Exn_printer.register (fun fmt exn -> match exn with ...@@ -341,6 +369,9 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
| KnownLogicSyntax ls -> | KnownLogicSyntax ls ->
fprintf fmt "Syntax for logical symbol %a is already defined" fprintf fmt "Syntax for logical symbol %a is already defined"
Pretty.print_ls ls Pretty.print_ls ls
| KnownConverterSyntax ls ->
fprintf fmt "Converter syntax for logical symbol %a is already defined"
Pretty.print_ls ls
| BadSyntaxIndex i -> | BadSyntaxIndex i ->
fprintf fmt "Bad argument index %d, must start with 1" i fprintf fmt "Bad argument index %d, must start with 1" i
| BadSyntaxArity (i1,i2) -> | BadSyntaxArity (i1,i2) ->
...@@ -359,4 +390,3 @@ let () = Exn_printer.register (fun fmt exn -> match exn with ...@@ -359,4 +390,3 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
| NotImplemented (s) -> | NotImplemented (s) ->
fprintf fmt "@[<hov 3> Unimplemented feature:@\n%s@]" s fprintf fmt "@[<hov 3> Unimplemented feature:@\n%s@]" s
| e -> raise e) | e -> raise e)
...@@ -46,6 +46,7 @@ val print_th_prelude : task -> prelude_map pp ...@@ -46,6 +46,7 @@ val print_th_prelude : task -> prelude_map pp
val meta_syntax_type : meta val meta_syntax_type : meta
val meta_syntax_logic : meta val meta_syntax_logic : meta
val meta_syntax_converter : meta
val meta_remove_prop : meta val meta_remove_prop : meta
val meta_remove_logic : meta val meta_remove_logic : meta
val meta_remove_type : meta val meta_remove_type : meta
...@@ -53,6 +54,7 @@ val meta_realized_theory : meta ...@@ -53,6 +54,7 @@ val meta_realized_theory : meta
val syntax_type : tysymbol -> string -> tdecl val syntax_type : tysymbol -> string -> tdecl
val syntax_logic : lsymbol -> string -> tdecl val syntax_logic : lsymbol -> string -> tdecl
val syntax_converter : lsymbol -> string -> tdecl
val remove_prop : prsymbol -> tdecl val remove_prop : prsymbol -> tdecl
val check_syntax_type: tysymbol -> string -> unit val check_syntax_type: tysymbol -> string -> unit
...@@ -60,12 +62,17 @@ val check_syntax_logic: lsymbol -> string -> unit ...@@ -60,12 +62,17 @@ val check_syntax_logic: lsymbol -> string -> unit
type syntax_map = string Mid.t type syntax_map = string Mid.t
(* [syntax_map] maps the idents of removed props to "" *) (* [syntax_map] maps the idents of removed props to "" *)
type converter_map = string Mls.t
val get_syntax_map : task -> syntax_map val get_syntax_map : task -> syntax_map
val add_syntax_map : tdecl -> syntax_map -> syntax_map val add_syntax_map : tdecl -> syntax_map -> syntax_map
(* interprets a declaration as a syntax rule, if any *) (* interprets a declaration as a syntax rule, if any *)
val get_converter_map : task -> converter_map
val add_converter_map : tdecl -> converter_map -> converter_map
val query_syntax : syntax_map -> ident -> string option val query_syntax : syntax_map -> ident -> string option
val query_converter : converter_map -> lsymbol -> string option
val syntax_arguments : string -> 'a pp -> 'a list pp val syntax_arguments : string -> 'a pp -> 'a list pp
(** (syntax_arguments templ print_arg fmt l) prints in the formatter fmt (** (syntax_arguments templ print_arg fmt l) prints in the formatter fmt
...@@ -83,6 +90,8 @@ val syntax_arguments_typed : ...@@ -83,6 +90,8 @@ val syntax_arguments_typed :
val on_syntax_map : (syntax_map -> 'a Trans.trans) -> 'a Trans.trans 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 : val sprint_tdecl :
('a -> Format.formatter -> Theory.tdecl -> 'a * string list) -> ('a -> Format.formatter -> Theory.tdecl -> 'a * string list) ->
Theory.tdecl -> 'a * string list -> 'a * string list Theory.tdecl -> 'a * string list -> 'a * string list
...@@ -123,4 +132,3 @@ val catch_unsupportedTerm : (term -> 'a) -> (term -> 'a) ...@@ -123,4 +132,3 @@ val catch_unsupportedTerm : (term -> 'a) -> (term -> 'a)
val catch_unsupportedDecl : (decl -> 'a) -> (decl -> 'a) val catch_unsupportedDecl : (decl -> 'a) -> (decl -> 'a)
(** same as {! catch_unsupportedType} but use [UnsupportedDecl] (** same as {! catch_unsupportedType} but use [UnsupportedDecl]
instead of [UnsupportedType] *) instead of [UnsupportedType] *)
...@@ -33,7 +33,7 @@ type driver = { ...@@ -33,7 +33,7 @@ type driver = {
drv_blacklist : string list; drv_blacklist : string list;
drv_meta : (theory * Stdecl.t) Mid.t; drv_meta : (theory * Stdecl.t) Mid.t;
drv_res_parser : prover_result_parser; drv_res_parser : prover_result_parser;
drv_tag : int drv_tag : int;
} }
(** parse a driver file *) (** parse a driver file *)
...@@ -106,9 +106,9 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files -> ...@@ -106,9 +106,9 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
let f = load_file file in let f = load_file file in
List.iter add_global f.f_global; List.iter add_global f.f_global;
let thprelude = ref Mid.empty in let thprelude = ref Mid.empty in
let meta = ref Mid.empty in let meta = ref Mid.empty in
let qualid = ref [] in let qualid = ref [] in
let find_pr th (loc,q) = try ns_find_pr th.th_export q let find_pr th (loc,q) = try ns_find_pr th.th_export q
with Not_found -> raise (Loc.Located (loc, UnknownProp (!qualid,q))) with Not_found -> raise (Loc.Located (loc, UnknownProp (!qualid,q)))
...@@ -145,6 +145,9 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files -> ...@@ -145,6 +145,9 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
| Rremovepr (q) -> | Rremovepr (q) ->
let td = remove_prop (find_pr th q) in let td = remove_prop (find_pr th q) in
add_meta th td meta add_meta th td meta
| Rconverter (q,s) ->
let cs = syntax_converter (find_ls th q) s in
add_meta th cs meta
| Rmeta (s,al) -> | Rmeta (s,al) ->
let rec ty_of_pty = function let rec ty_of_pty = function
| PTyvar x -> | PTyvar x ->
...@@ -190,13 +193,13 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files -> ...@@ -190,13 +193,13 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
drv_thprelude = Mid.map List.rev !thprelude; drv_thprelude = Mid.map List.rev !thprelude;
drv_blacklist = Queue.fold (fun l s -> s :: l) [] blacklist; drv_blacklist = Queue.fold (fun l s -> s :: l) [] blacklist;
drv_meta = !meta; drv_meta = !meta;
drv_res_parser = drv_res_parser =
{ {
prp_regexps = List.rev !regexps; prp_regexps = List.rev !regexps;
prp_timeregexps = List.rev !timeregexps; prp_timeregexps = List.rev !timeregexps;
prp_exitcodes = List.rev !exitcodes; prp_exitcodes = List.rev !exitcodes;
}; };
drv_tag = !driver_tag drv_tag = !driver_tag;
} }
let syntax_map drv = let syntax_map drv =
...@@ -338,4 +341,3 @@ let () = Exn_printer.register (fun fmt exn -> match exn with ...@@ -338,4 +341,3 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
| PSymExpected ls -> Format.fprintf fmt | PSymExpected ls -> Format.fprintf fmt
"%a is not a predicate symbol" Pretty.print_ls ls "%a is not a predicate symbol" Pretty.print_ls ls
| e -> raise e) | e -> raise e)
...@@ -27,12 +27,13 @@ type metarg = ...@@ -27,12 +27,13 @@ type metarg =
| PMAint of int | PMAint of int
type th_rule = type th_rule =
| Rprelude of string | Rprelude of string
| Rsyntaxts of qualid * string | Rsyntaxts of qualid * string
| Rsyntaxfs of qualid * string | Rsyntaxfs of qualid * string
| Rsyntaxps of qualid * string | Rsyntaxps of qualid * string
| Rremovepr of qualid | Rconverter of qualid * string
| Rmeta of string * metarg list | Rremovepr of qualid
| Rmeta of string * metarg list
type theory_rules = { type theory_rules = {
thr_name : qualid; thr_name : qualid;
...@@ -43,7 +44,6 @@ type mo_rule = ...@@ -43,7 +44,6 @@ type mo_rule =
| MRtheory of th_rule | MRtheory of th_rule
| MRexception of qualid * string | MRexception of qualid * string
| MRval of qualid * string | MRval of qualid * string
| MRconverter of qualid * string
type module_rules = { type module_rules = {
mor_name : qualid; mor_name : qualid;
......
...@@ -74,14 +74,15 @@ theory: ...@@ -74,14 +74,15 @@ theory:
{ { thr_name = $2; thr_rules = $3 } } { { thr_name = $2; thr_rules = $3 } }
trule: trule:
| PRELUDE STRING { Rprelude ($2) } | PRELUDE STRING { Rprelude ($2) }
| SYNTAX TYPE qualid STRING { Rsyntaxts ($3, $4) } | SYNTAX TYPE qualid STRING { Rsyntaxts ($3, $4) }
| SYNTAX CONSTANT qualid STRING { Rsyntaxfs ($3, $4) } | SYNTAX CONSTANT qualid STRING { Rsyntaxfs ($3, $4) }
| SYNTAX FUNCTION qualid STRING { Rsyntaxfs ($3, $4) } | SYNTAX FUNCTION qualid STRING { Rsyntaxfs ($3, $4) }
| SYNTAX PREDICATE qualid STRING { Rsyntaxps ($3, $4) } | SYNTAX PREDICATE qualid STRING { Rsyntaxps ($3, $4) }
| REMOVE PROP qualid { Rremovepr ($3) } | SYNTAX CONVERTER qualid STRING { Rconverter ($3, $4) }
| META ident meta_args { Rmeta ($2, $3) } | REMOVE PROP qualid { Rremovepr ($3) }
| META STRING meta_args { Rmeta ($2, $3) } | META ident meta_args { Rmeta ($2, $3) }
| META STRING meta_args { Rmeta ($2, $3) }
meta_args: separated_nonempty_list(COMMA,meta_arg) { $1 } meta_args: separated_nonempty_list(COMMA,meta_arg) { $1 }
...@@ -188,6 +189,5 @@ mrule: ...@@ -188,6 +189,5 @@ mrule:
| trule { MRtheory $1 } | trule { MRtheory $1 }
| SYNTAX EXCEPTION qualid STRING { MRexception ($3, $4) } | SYNTAX EXCEPTION qualid STRING { MRexception ($3, $4) }
| SYNTAX VAL qualid STRING { MRval ($3, $4) } | SYNTAX VAL qualid STRING { MRval ($3, $4) }
| SYNTAX CONVERTER qualid STRING { MRconverter ($3, $4) }
loc(X): X { Loc.extract ($startpos,$endpos), $1 } loc(X): X { Loc.extract ($startpos,$endpos), $1 }
...@@ -73,7 +73,8 @@ let print_ident fmt id = ...@@ -73,7 +73,8 @@ let print_ident fmt id =
fprintf fmt "%s" (id_unique ident_printer id) fprintf fmt "%s" (id_unique ident_printer id)
type info = { type info = {
info_syn : syntax_map; info_syn : syntax_map;
info_converters : converter_map;
} }
(** type *) (** type *)
...@@ -127,7 +128,19 @@ let rec print_term info fmt t = match t.t_node with ...@@ -127,7 +128,19 @@ let rec print_term info fmt t = match t.t_node with
} in } in
Number.print number_format fmt c Number.print number_format fmt c
| Tvar v -> print_var fmt v | Tvar v -> print_var fmt v
| Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with | Tapp (ls, tl) ->
(* let's check if a converter applies *)
begin try
match tl with
| [ { t_node = Tconst _} ] ->
begin match query_converter info.info_converters ls with
| None -> raise Exit
| Some s -> syntax_arguments s (print_term info) fmt tl
end
| _ -> raise Exit
with Exit ->
(* non converter applies, then ... *)
match query_syntax info.info_syn ls.ls_name with
| Some s -> syntax_arguments_typed s (print_term info) | Some s -> syntax_arguments_typed s (print_term info)
(print_type info) t fmt tl (print_type info) t fmt tl
| None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *) | None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
...@@ -270,12 +283,14 @@ let print_decl info fmt d = match d.d_node with ...@@ -270,12 +283,14 @@ let print_decl info fmt d = match d.d_node with
print_prop_decl info fmt k pr f print_prop_decl info fmt k pr f
let print_decls = let print_decls =
let print_decl sm fmt d = let print_decl (sm, cm) fmt d =
try print_decl {info_syn = sm} fmt d; sm, [] try print_decl {info_syn = sm; info_converters = cm} fmt d; (sm, cm), []
with Unsupported s -> raise (UnsupportedDecl (d,s)) in with Unsupported s -> raise (UnsupportedDecl (d,s)) in
let print_decl = Printer.sprint_decl print_decl in let print_decl = Printer.sprint_decl print_decl in
let print_decl task acc = print_decl task.Task.task_decl acc in let print_decl task acc = print_decl task.Task.task_decl acc in
Discriminate.on_syntax_map (fun sm -> Trans.fold print_decl (sm,[])) Discriminate.on_syntax_map (fun sm ->
Printer.on_converter_map (fun cm ->
Trans.fold print_decl ((sm, cm),[])))
let print_task args ?old:_ fmt task = let print_task args ?old:_ fmt task =
(* In trans-based p-printing [forget_all] is a no-no *) (* In trans-based p-printing [forget_all] is a no-no *)
......
...@@ -111,6 +111,8 @@ let load_driver env file extra_files = ...@@ -111,6 +111,8 @@ let load_driver env file extra_files =
let ps = find_ps th q in let ps = find_ps th q in
check_syntax_logic ps s; check_syntax_logic ps s;
add_syntax ps.ls_name s add_syntax ps.ls_name s
| Rconverter _ ->
Loc.errorm "Syntax converter cannot be used in pure theories"
| Rremovepr (q) -> | Rremovepr (q) ->
ignore (find_pr th q) ignore (find_pr th q)
| Rmeta (s,al) -> | Rmeta (s,al) ->
...@@ -151,16 +153,17 @@ let load_driver env file extra_files = ...@@ -151,16 +153,17 @@ let load_driver env file extra_files =
with Not_found -> raise (Loc.Located (loc, UnknownExn (!qualid,q))) with Not_found -> raise (Loc.Located (loc, UnknownExn (!qualid,q)))
in in
let add_local_module loc m = function let add_local_module loc m = function
| MRtheory trule -> add_local m.mod_theory (loc,trule)
| MRexception (q,s) -> | MRexception (q,s) ->
let xs = find_xs m q in let xs = find_xs m q in
add_syntax xs.xs_name s add_syntax xs.xs_name s
| MRval (q,s) -> | MRval (q,s) ->
let id = find_val m q in let id = find_val m q in
add_syntax id s add_syntax id s
| MRconverter (q,s) -> | MRtheory (Rconverter (q,s)) ->
let id = find_val m q in let id = find_val m q in
add_converter id s add_converter id s
| MRtheory trule ->
add_local m.mod_theory (loc,trule)
in in
let add_local_module m (loc,rule) = let add_local_module m (loc,rule) =
Loc.try3 ~loc add_local_module loc m rule Loc.try3 ~loc add_local_module loc m rule
...@@ -217,5 +220,3 @@ let () = Exn_printer.register (fun fmt exn -> match exn with ...@@ -217,5 +220,3 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
| PSymExpected ls -> Format.fprintf fmt | PSymExpected ls -> Format.fprintf fmt
"%a is not a predicate symbol" Pretty.print_ls ls "%a is not a predicate symbol" Pretty.print_ls ls
| e -> raise e) | e -> raise e)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter bv : Type.
Parameter nth: bv -> Z -> bool.
Parameter bvzero: bv.
Axiom Nth_zero : forall (n:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) ->
((nth bvzero n) = false).
Parameter bvone: bv.
Axiom Nth_one : forall (n:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) -> ((nth bvone
n) = true).
Definition eq(v1:bv) (v2:bv): Prop := forall (n:Z), ((0%Z <= n)%Z /\
(n < 32%Z)%Z) -> ((nth v1 n) = (nth v2 n)).
Axiom extensionality : forall (v1:bv) (v2:bv), (eq v1 v2) -> (v1 = v2).
Parameter bw_and: bv -> bv -> bv.
Axiom Nth_bw_and : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
(n < 32%Z)%Z) -> ((nth (bw_and v1 v2) n) = (andb (nth v1 n) (nth v2 n))).
Parameter bw_or: bv -> bv -> bv.
Axiom Nth_bw_or : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
(n < 32%Z)%Z) -> ((nth (bw_or v1 v2) n) = (orb (nth v1 n) (nth v2 n))).
Parameter bw_xor: bv -> bv -> bv.
Axiom Nth_bw_xor : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
(n < 32%Z)%Z) -> ((nth (bw_xor v1 v2) n) = (xorb (nth v1 n) (nth v2 n))).
Parameter bw_not: bv -> bv.
Axiom Nth_bw_not : forall (v:bv) (n:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) ->
((nth (bw_not v) n) = (negb (nth v n))).
Parameter lsr: bv -> Z -> bv.
Axiom lsr_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
(n < 32%Z)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z < 32%Z)%Z -> ((nth (lsr b
s) n) = (nth b (n + s)%Z)))).
Axiom lsr_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
(n < 32%Z)%Z) -> ((0%Z <= s)%Z -> ((32%Z <= (n + s)%Z)%Z -> ((nth (lsr b
s) n) = false))).
Parameter asr: bv -> Z -> bv.
Axiom asr_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
(n < 32%Z)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z < 32%Z)%Z -> ((nth (asr b
s) n) = (nth b (n + s)%Z)))).
Axiom asr_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
(n < 32%Z)%Z) -> ((0%Z <= s)%Z -> ((32%Z <= (n + s)%Z)%Z -> ((nth (asr b
s) n) = (nth b (32%Z - 1%Z)%Z)))).