diff --git a/drivers/cvc4_bv.gen b/drivers/cvc4_bv.gen index ecae3f0dc42eccebee6ddf4c984099d307365d6d..4d4f8618384c4509908ff724910862d7fc50cc16 100644 --- a/drivers/cvc4_bv.gen +++ b/drivers/cvc4_bv.gen @@ -1,5 +1,6 @@ (* 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)" diff --git a/src/core/printer.ml b/src/core/printer.ml index 673cd6355fc251cfeb1d75318a5b2d0d98897fa3..a2328eb140ada42f03f1f6e49687ae6d4455cb7b 100644 --- a/src/core/printer.ml +++ b/src/core/printer.ml @@ -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) -> diff --git a/src/core/printer.mli b/src/core/printer.mli index e29a2a223a5948836eb6002b5504bd844bfaaa38..8abde303f4a90ce82c4324d2f58b87980e7e616b 100644 --- a/src/core/printer.mli +++ b/src/core/printer.mli @@ -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 diff --git a/src/driver/driver.ml b/src/driver/driver.ml index c6f1953efd8e7ec07cd96dbb41dd46a4520c7e6b..f7c1a3b2aacb5045326c91b3266ab3ed278235b9 100644 --- a/src/driver/driver.ml +++ b/src/driver/driver.ml @@ -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 diff --git a/src/driver/driver_ast.ml b/src/driver/driver_ast.ml index f2ff69b6d4092edf3ba462c8798e708d1b9f8f9e..dc3c2fe31011e8354302e4ca6bae1658e37afc87 100644 --- a/src/driver/driver_ast.ml +++ b/src/driver/driver_ast.ml @@ -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 diff --git a/src/driver/driver_lexer.mll b/src/driver/driver_lexer.mll index 4fd81a47951768ad059ae3c7af32a5d81c4fec66..d78521bc65251f7a5ccad0faf6fddcf9f999adb7 100644 --- a/src/driver/driver_lexer.mll +++ b/src/driver/driver_lexer.mll @@ -27,6 +27,7 @@ [ "theory", THEORY; "end", END; "syntax", SYNTAX; + "overriding", OVERRIDING; "remove", REMOVE; "meta", META; "prelude", PRELUDE; diff --git a/src/driver/driver_parser.mly b/src/driver/driver_parser.mly index 46ce872dbb2aa4a24696c10a0d52dbdeca6a084f..c722a9fde885cb749544890c2c64bb3a88bf4d00 100644 --- a/src/driver/driver_parser.mly +++ b/src/driver/driver_parser.mly @@ -22,7 +22,7 @@ %token STRING %token OPERATOR %token 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 } diff --git a/src/printer/gappa.ml b/src/printer/gappa.ml index 59da32484b1080417e2a7e7e1b706216ae63380f..16a6944e209182eafb5a5e7eb9212bf5e21e3089 100644 --- a/src/printer/gappa.ml +++ b/src/printer/gappa.ml @@ -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)) diff --git a/src/util/extmap.ml b/src/util/extmap.ml index 64e669b6b7279dface6028fe7c5a86b650879709..3ba7eca47c90db722639458bce15427f3e1b31d0 100644 --- a/src/util/extmap.ml +++ b/src/util/extmap.ml @@ -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 diff --git a/src/util/extmap.mli b/src/util/extmap.mli index 190376667b4f2710281818ed9d9ecc1ebf3782d4..c46af73f5c9b104b330fb0184aa99ede4e3568db 100644 --- a/src/util/extmap.mli +++ b/src/util/extmap.mli @@ -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 diff --git a/src/whyml/mlw_driver.ml b/src/whyml/mlw_driver.ml index 0789c63998a12de33019d472e0b79bad419af81d..12ca5f5780df315419b11c7acedc29f00c0f9f72 100644 --- a/src/whyml/mlw_driver.ml +++ b/src/whyml/mlw_driver.ml @@ -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 diff --git a/src/whyml/mlw_ocaml.ml b/src/whyml/mlw_ocaml.ml index f752205e3448962281ce8ebd33ddaf88a75ff565..fca9b35a78f4f1fe51dd33ecb7fb5c38f618f26c 100644 --- a/src/whyml/mlw_ocaml.ml +++ b/src/whyml/mlw_ocaml.ml @@ -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])