Commit 6b90ebf2 authored by Clément Fumex's avatar Clément Fumex

Add the possibility to override syntax in drivers.

To do so, add "overriding" keyword in front of "syntax" in the driver file as in, e.g.,
  overriding syntax function to_uint "(bv2int %1)"

One can only have one overriding for a specific function/type.
parent babc08d3
(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
have the same name for the function to_int *)
theory bv.BV64
syntax converter of_int "(_ bv%1 64)"
syntax function to_uint "(bv2nat %1)"
......
......@@ -279,18 +279,21 @@ 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]
let meta_syntax_type = register_meta "syntax_type" [MTtysymbol; MTstring; MTint]
~desc:"Specify@ the@ syntax@ used@ to@ pretty-print@ a@ type@ symbol.@ \
Can@ be@ specified@ in@ the@ driver@ with@ the@ 'syntax type'@ rule."
let meta_syntax_logic = register_meta "syntax_logic" [MTlsymbol; MTstring]
let meta_syntax_logic = register_meta "syntax_logic" [MTlsymbol; MTstring; MTint]
~desc:"Specify@ the@ syntax@ used@ to@ pretty-print@ a@ function/predicate@ \
symbol.@ \
Can@ be@ specified@ in@ the@ driver@ with@ the@ 'syntax function'@ \
or@ 'syntax predicate'@ rules."
let meta_syntax_converter = register_meta "syntax_converter" [MTlsymbol; MTstring]
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."
......@@ -313,38 +316,64 @@ let meta_realized_theory = register_meta "realized_theory" [MTstring; MTstring]
let check_syntax_type ts s = check_syntax s (List.length ts.ts_args)
let syntax_type ts s =
let syntax_type ts s b =
check_syntax_type ts s;
create_meta meta_syntax_type [MAts ts; MAstr s]
create_meta meta_syntax_type [MAts ts; MAstr s; MAint (if b then 1 else 0)]
let syntax_logic ls s =
let syntax_logic ls s b =
check_syntax_logic ls s;
create_meta meta_syntax_logic [MAls ls; MAstr s]
create_meta meta_syntax_logic [MAls ls; MAstr s; MAint (if b then 1 else 0)]
let syntax_converter ls s =
let syntax_converter ls s b =
check_syntax_logic ls s;
create_meta meta_syntax_converter [MAls ls; MAstr s]
create_meta meta_syntax_converter [MAls ls; MAstr s; MAint (if b then 1 else 0)]
let remove_prop pr =
create_meta meta_remove_prop [MApr pr]
type syntax_map = string Mid.t
type converter_map = string Mls.t
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)
| Some (_,0) ->
begin match ov with
| 0 -> raise e
| 1 -> Some (rs, 2)
| _ -> assert false
end
| Some (rs',1) ->
begin match ov with
| 0 -> Some (rs',2)
| 1 -> raise e'
| _ -> assert false
end
| Some (_,2) -> raise e'
| _ -> assert false
let sm_add_ts sm = function
| [MAts ts; MAstr rs] -> Mid.add_new (KnownTypeSyntax ts) ts.ts_name rs sm
| [MAts ts; MAstr rs; MAint ov] ->
Mid.change
(change_override (KnownTypeSyntax ts) (TooManyTypeOverride ts)
rs ov) ts.ts_name sm
| _ -> assert false
let sm_add_ls sm = function
| [MAls ls; MAstr rs] -> Mid.add_new (KnownLogicSyntax ls) ls.ls_name rs sm
| [MAls ls; MAstr rs; MAint ov] ->
Mid.change
(change_override (KnownLogicSyntax ls) (TooManyLogicOverride ls)
rs ov) ls.ls_name sm
| _ -> assert false
let sm_add_pr sm = function
| [MApr pr] -> Mid.add pr.pr_name "" sm
| [MApr pr] -> Mid.add pr.pr_name ("",0) sm
| _ -> assert false
let cm_add_ls cm = function
| [MAls ls; MAstr rs] -> Mls.add_new (KnownConverterSyntax ls) ls rs cm
| [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 =
......@@ -367,9 +396,11 @@ 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 =
try Some (fst (Mid.find id sm)) with Not_found -> None
let query_converter cm ls = Mls.find_opt ls cm
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 ->
......@@ -446,6 +477,15 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
| 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) ->
......
......@@ -66,17 +66,17 @@ val meta_remove_logic : meta
val meta_remove_type : meta
val meta_realized_theory : meta
val syntax_type : tysymbol -> string -> tdecl
val syntax_logic : lsymbol -> string -> tdecl
val syntax_converter : lsymbol -> string -> tdecl
val syntax_type : tysymbol -> string -> bool -> tdecl
val syntax_logic : lsymbol -> string -> bool -> tdecl
val syntax_converter : lsymbol -> string -> bool -> tdecl
val remove_prop : prsymbol -> tdecl
val check_syntax_type: tysymbol -> string -> unit
val check_syntax_logic: lsymbol -> string -> unit
type syntax_map = string Mid.t
type syntax_map = (string*int) Mid.t
(* [syntax_map] maps the idents of removed props to "" *)
type converter_map = string Mls.t
type converter_map = (string*int) Mls.t
val get_syntax_map : task -> syntax_map
val add_syntax_map : tdecl -> syntax_map -> syntax_map
......
......@@ -142,20 +142,20 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
| Rprelude s ->
let l = Mid.find_def [] th.th_name !thprelude in
thprelude := Mid.add th.th_name (s::l) !thprelude
| Rsyntaxts (q,s) ->
let td = syntax_type (find_ts th q) s in
| Rsyntaxts (q,s,b) ->
let td = syntax_type (find_ts th q) s b in
add_meta th td meta
| Rsyntaxfs (q,s) ->
let td = syntax_logic (find_fs th q) s in
| Rsyntaxfs (q,s,b) ->
let td = syntax_logic (find_fs th q) s b in
add_meta th td meta
| Rsyntaxps (q,s) ->
let td = syntax_logic (find_ps th q) s in
| Rsyntaxps (q,s,b) ->
let td = syntax_logic (find_ps th q) s b in
add_meta th td meta
| Rremovepr (q) ->
let td = remove_prop (find_pr th q) in
add_meta th td meta
| Rconverter (q,s) ->
let cs = syntax_converter (find_ls th q) s in
| Rconverter (q,s,b) ->
let cs = syntax_converter (find_ls th q) s b in
add_meta th cs meta
| Rmeta (s,al) ->
let rec ty_of_pty = function
......
......@@ -28,10 +28,10 @@ type metarg =
type th_rule =
| Rprelude of string
| Rsyntaxts of qualid * string
| Rsyntaxfs of qualid * string
| Rsyntaxps of qualid * string
| Rconverter of qualid * string
| Rsyntaxts of qualid * string * bool
| Rsyntaxfs of qualid * string * bool
| Rsyntaxps of qualid * string * bool
| Rconverter of qualid * string * bool
| Rremovepr of qualid
| Rmeta of string * metarg list
......
......@@ -27,6 +27,7 @@
[ "theory", THEORY;
"end", END;
"syntax", SYNTAX;
"overriding", OVERRIDING;
"remove", REMOVE;
"meta", META;
"prelude", PRELUDE;
......
......@@ -22,7 +22,7 @@
%token <string> STRING
%token <string> OPERATOR
%token <string> INPUT (* never reaches the parser *)
%token THEORY END SYNTAX REMOVE META PRELUDE PRINTER MODEL_PARSER
%token THEORY END SYNTAX REMOVE META PRELUDE PRINTER MODEL_PARSER OVERRIDING
%token VALID INVALID UNKNOWN FAIL
%token TIMEOUT OUTOFMEMORY STEPLIMITEXCEEDED TIME STEPS
%token UNDERSCORE LEFTPAR RIGHTPAR DOT QUOTE EOF
......@@ -78,16 +78,20 @@ theory:
| THEORY loc(tqualid) list(loc(trule)) END
{ { thr_name = $2; thr_rules = $3 } }
syntax:
| OVERRIDING SYNTAX { true }
| SYNTAX { false }
trule:
| PRELUDE STRING { Rprelude ($2) }
| SYNTAX TYPE qualid STRING { Rsyntaxts ($3, $4) }
| SYNTAX CONSTANT qualid STRING { Rsyntaxfs ($3, $4) }
| SYNTAX FUNCTION qualid STRING { Rsyntaxfs ($3, $4) }
| SYNTAX PREDICATE qualid STRING { Rsyntaxps ($3, $4) }
| SYNTAX CONVERTER qualid STRING { Rconverter ($3, $4) }
| REMOVE PROP qualid { Rremovepr ($3) }
| META ident meta_args { Rmeta ($2, $3) }
| META STRING meta_args { Rmeta ($2, $3) }
| PRELUDE STRING { Rprelude ($2) }
| syntax TYPE qualid STRING { Rsyntaxts ($3, $4, $1) }
| 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) }
| REMOVE PROP qualid { Rremovepr ($3) }
| META ident meta_args { Rmeta ($2, $3) }
| META STRING meta_args { Rmeta ($2, $3) }
meta_args: separated_nonempty_list(COMMA,meta_arg) { $1 }
......
......@@ -24,7 +24,7 @@ let syntactic_transform transf =
Trans.on_meta meta_syntax_logic (fun metas ->
let symbols = List.fold_left (fun acc meta_arg ->
match meta_arg with
| [MAls ls; MAstr _] -> Sls.add ls acc
| [MAls ls; MAstr _; MAint _] -> Sls.add ls acc
| _ -> assert false) Sls.empty metas in
transf (fun ls -> Sls.mem ls symbols))
......
......@@ -75,6 +75,7 @@ module type S =
(key -> 'a option -> 'b option -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
val translate : (key -> key) -> 'a t -> 'a t
val add_new : exn -> key -> 'a -> 'a t -> 'a t
val replace : exn -> key -> 'a -> 'a t -> 'a t
val keys: 'a t -> key list
val values: 'a t -> 'a list
val of_list : (key * 'a) list -> 'a t
......@@ -580,6 +581,10 @@ module type S =
| Some _ -> raise e
| None -> Some v) x m
let replace e x v m = change (function
| Some _ -> Some v
| None -> raise e) x m
let is_num_elt n m =
try
fold (fun _ _ n -> if n < 0 then raise Exit else n-1) m n = 0
......
......@@ -256,6 +256,10 @@ module type S =
(** [add_new e x v m] binds [x] to [v] in [m] if [x] is not bound,
and raises [e] otherwise. *)
val replace : exn -> key -> 'a -> 'a t -> 'a t
(** [replace e x v m] binds [x] to [v] in [m] if [x] is already bound,
and raises [e] otherwise. *)
val keys: 'a t -> key list
(** Return the list of all keys of the given map.
The returned list is sorted in increasing order with respect
......
......@@ -93,24 +93,26 @@ let load_driver env file extra_files =
let find_ps th q =
let ls = find_ls th q in
if ls.ls_value <> None then raise (PSymExpected ls) else ls in
let add_syntax id s = syntax_map := Mid.add id s !syntax_map in
let add_converter id s = converter_map := Mid.add id s !converter_map 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_local th = function
| Rprelude s ->
let l = Mid.find_def [] th.th_name !thprelude in
thprelude := Mid.add th.th_name (s::l) !thprelude
| Rsyntaxts (q,s) ->
| Rsyntaxts (q,s,b) ->
let ts = find_ts th q in
check_syntax_type ts s;
add_syntax ts.ts_name s
| Rsyntaxfs (q,s) ->
add_syntax ts.ts_name s b
| Rsyntaxfs (q,s,b) ->
let fs = find_fs th q in
check_syntax_logic fs s;
add_syntax fs.ls_name s
| Rsyntaxps (q,s) ->
add_syntax fs.ls_name s b
| Rsyntaxps (q,s,b) ->
let ps = find_ps th q in
check_syntax_logic ps s;
add_syntax ps.ls_name s
add_syntax ps.ls_name s b
| Rconverter _ ->
Loc.errorm "Syntax converter cannot be used in pure theories"
| Rremovepr (q) ->
......@@ -155,13 +157,13 @@ let load_driver env file extra_files =
let add_local_module loc m = function
| MRexception (q,s) ->
let xs = find_xs m q in
add_syntax xs.xs_name s
add_syntax xs.xs_name s false
| MRval (q,s) ->
let id = find_val m q in
add_syntax id s
| MRtheory (Rconverter (q,s)) ->
add_syntax id s false
| MRtheory (Rconverter (q,s,b)) ->
let id = find_val m q in
add_converter id s
add_converter id s b
| MRtheory trule ->
add_local m.mod_theory (loc,trule)
in
......
......@@ -497,7 +497,7 @@ module Translate = struct
{ e_node = Eapp ({ e_node = Earrow a }, pv', _) })
when pv_equal pv' pv
&& Mid.mem a.ps_name info.converters && is_int_constant e1 ->
let s = Mid.find a.ps_name info.converters in
let s = fst (Mid.find a.ps_name info.converters) in
let n = Number.compute_int (get_int_constant e1) in
let e1 = ML.Esyntax (BigInt.to_string n, []) in
ML.Esyntax (s, [e1])
......
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