diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 8cdbf561e..f95da60df 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -99,6 +99,8 @@ let gstate_bool_flags = [ EcGState.pp_showtvi; EcGState.circuit_timing; EcGState.circuit_debug_smt; + EcGState.warn_uninit; + EcGState.warn_unused_unfold; ] exception InvalidPragma of string diff --git a/src/ecGState.ml b/src/ecGState.ml index e9fe2b29b..f7534cf7e 100644 --- a/src/ecGState.ml +++ b/src/ecGState.ml @@ -82,6 +82,18 @@ let circuit_debug_smt = "Circuit:debug_smt" let get_circuit_debug_smt (g : gstate) : bool = getflag ~default:false circuit_debug_smt g +(* -------------------------------------------------------------------- *) +let warn_uninit = "Warn:uninit" + +let get_warn_uninit (g : gstate) : bool = + getflag ~default:true warn_uninit g + +(* -------------------------------------------------------------------- *) +let warn_unused_unfold = "Warn:unused_unfold" + +let get_warn_unused_unfold (g : gstate) : bool = + getflag ~default:true warn_unused_unfold g + (* -------------------------------------------------------------------- *) let add_notifier (notifier : loglevel -> string Lazy.t -> unit) (gs : gstate) = let notifier = { nt_id = EcUid.unique (); nt_cb = notifier; } in diff --git a/src/ecGState.mli b/src/ecGState.mli index 8069b68b0..6f47b66d1 100644 --- a/src/ecGState.mli +++ b/src/ecGState.mli @@ -40,6 +40,14 @@ val get_circuit_timing : gstate -> bool val circuit_debug_smt : string val get_circuit_debug_smt : gstate -> bool +(* --------------------------------------------------------------------- *) +val warn_uninit : string +val get_warn_uninit : gstate -> bool + +(* --------------------------------------------------------------------- *) +val warn_unused_unfold : string +val get_warn_unused_unfold : gstate -> bool + (* --------------------------------------------------------------------- *) type nid_t type loglevel = [`Debug | `Info | `Warning | `Critical] diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml index c2ce31e9a..c478d7f2e 100644 --- a/src/ecHiGoal.ml +++ b/src/ecHiGoal.ml @@ -696,7 +696,8 @@ let process_delta ?target ((s :rwside), o, p) tc = EcReduction.delta_h = check_id; } in let redform = EcReduction.simplify ri hyps target in - if EcFol.f_equal target redform then + if EcGState.get_warn_unused_unfold (EcEnv.gstate env) + && EcFol.f_equal target redform then EcEnv.notify env `Warning "unused unfold: /%s" x; t_change ~ri:{ ri with eta = true; beta = true; } ?target:idtg redform tc diff --git a/src/ecOptions.ml b/src/ecOptions.ml index bd21a69aa..a78822aaf 100644 --- a/src/ecOptions.ml +++ b/src/ecOptions.ml @@ -90,6 +90,7 @@ type ini_options = { ini_timeout : int option; ini_idirs : (string option * string) list; ini_rdirs : (string option * string) list; + ini_pragmas : string list; } type ini_context = { @@ -116,6 +117,8 @@ module Ini : sig val get_rdirs : ini_context -> (string option * string) list + val get_pragmas : ini_context -> string list + (* ------------------------------------------------------------------ *) val get_all_ppwidth : ini_context list -> int option @@ -132,6 +135,8 @@ module Ini : sig val get_all_idirs : ini_context list -> (string option * string) list val get_all_rdirs : ini_context list -> (string option * string) list + + val get_all_pragmas : ini_context list -> string list end = struct (* ------------------------------------------------------------------ *) let absolute ?(root : string option) (filename : string) = @@ -174,6 +179,9 @@ end = struct (snd_map (absolute ?root:ini.inic_root)) ini.inic_ini.ini_rdirs + let get_pragmas (ini : ini_context) = + ini.inic_ini.ini_pragmas + (* ------------------------------------------------------------------ *) let get_all_ppwidth (ini : ini_context list) = List.find_map_opt get_ppwidth ini @@ -198,6 +206,9 @@ end = struct let get_all_rdirs (ini : ini_context list) = List.flatten (List.map get_rdirs ini) + + let get_all_pragmas (ini : ini_context list) = + List.flatten (List.map get_pragmas ini) end (* -------------------------------------------------------------------- *) @@ -525,7 +536,8 @@ let prv_options_of_values ini values = | None -> Ini.get_all_quorum ini | Some _ as i -> i end; - prvo_pragmas = get_string_list "pragmas" values; + prvo_pragmas = + (Ini.get_all_pragmas ini) @ (get_string_list "pragmas" values); prvo_ppwidth = begin match get_int "pp-width" values with | None -> Ini.get_all_ppwidth ini @@ -747,7 +759,8 @@ let read_ini_file (filename : string) = ini_quorum = tryint "quorum" ; ini_timeout = tryint "timeout" ; ini_idirs = List.map parse_idir (trylist "idirs"); - ini_rdirs = List.map parse_idir (trylist "rdirs"); } in + ini_rdirs = List.map parse_idir (trylist "rdirs"); + ini_pragmas = trylist "pragmas"; } in { ini_ppwidth = ini.ini_ppwidth; ini_why3 = omap expand ini.ini_why3; @@ -756,4 +769,5 @@ let read_ini_file (filename : string) = ini_quorum = ini.ini_quorum; ini_timeout = ini.ini_timeout; ini_idirs = ini.ini_idirs; - ini_rdirs = ini.ini_rdirs; } + ini_rdirs = ini.ini_rdirs; + ini_pragmas = ini.ini_pragmas; } diff --git a/src/ecOptions.mli b/src/ecOptions.mli index a5c09b11d..0fb1fc3c2 100644 --- a/src/ecOptions.mli +++ b/src/ecOptions.mli @@ -86,6 +86,7 @@ type ini_options = { ini_timeout : int option; ini_idirs : (string option * string) list; ini_rdirs : (string option * string) list; + ini_pragmas : string list; } type ini_context = { diff --git a/src/ecScope.ml b/src/ecScope.ml index 65a3fc1b2..dd9d47053 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -1761,7 +1761,10 @@ module Mod = struct in let m = TT.transmod (env scope) ~attop:true ptm in - let ur = EcModules.get_uninit_read_of_module (path scope) m in + let ur = + if EcGState.get_warn_uninit (EcEnv.gstate (env scope)) then + EcModules.get_uninit_read_of_module (path scope) m + else [] in if not (List.is_empty ur) then begin let ppe = EcPrinting.PPEnv.ofenv (env scope) in