adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

cleanup: reduce warnings 

This mostly refactors ML code to avoid non-exhaustive matches, restore
the (op infix) syntax that got lost in a previous Isabelle update, and
removes some unused functions/parameters.

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This commit is contained in:
Gerwin Klein 2021-01-25 10:03:25 +11:00 committed by Gerwin Klein
parent 42e174ce1f
commit 4bf1635b2f
11 changed files with 35 additions and 38 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
lib/Apply_Debug.thy
View File

@ -70,7 +70,6 @@ struct
type break_opts = { tags : string list, trace : (string * Position.T) option, show_running : bool }
fun do_markup range m = Output.report [Markup.markup (Markup.properties (Position.properties_of_range range) m) ""];
fun do_markup_pos pos m = Output.report [Markup.markup (Markup.properties (Position.properties_of pos) m) ""];
type markup_queue = { cur : Position.range option, next : Position.range option, clear_cur : bool }
@ -192,9 +191,6 @@ fun add_debug ctxt (Method.Source src) = (Method.Basic (traceify_method ctxt src
| add_debug ctxt (Method.Combinator (x,y,txts)) = (Method.Combinator (x,y, map (add_debug ctxt) txts))
| add_debug _ x = x
fun st_eq (ctxt : Proof.context,st) (ctxt',st') =
pointer_eq (ctxt,ctxt') andalso Thm.eq_thm (st,st')
type result =
{ pre_state : thm,
post_state : thm,
@ -339,7 +335,7 @@ fun debug_print (id : debug_state Synchronized.var) =
(@{print} (Synchronized.value id));
(* Trigger a restart if an existing nth entry differs from the given one *)
fun maybe_restart id n st =
fun maybe_restart id n =
let
val gen = guarded_read id (fn e => SOME (#trans_id e));
@ -413,7 +409,6 @@ fun set_break_opts opts = Debug_Data.map (@{apply 5 (4)} (fn _ => opts))
val get_break_opts = #4 o Debug_Data.get;
fun set_last_tag tags = Debug_Data.map (@{apply 5 (5)} (fn _ => tags))
val get_last_tag = #5 o Debug_Data.get;
val is_debug_ctxt = is_some o #1 o Debug_Data.get;
@ -432,7 +427,7 @@ fun set_continuation i ctxt = if get_continuation ctxt = i then ctxt else
fun set_can_break b ctxt = if get_can_break ctxt = b then ctxt else
Debug_Data.map (@{apply 5 (3)} (fn _ => b)) ctxt;
fun has_break_tag (SOME tag) tags = member (=) tags tag
fun has_break_tag (SOME tag) tags = member (op =) tags tag
| has_break_tag NONE _ = true;
fun break ctxt tag = (fn thm =>
@ -461,7 +456,7 @@ structure Data = Generic_Data
type T = (morphism * Proof.context * static_info) option;
val empty: T = NONE;
val extend = K NONE;
fun merge data : T = NONE;
fun merge _ : T = NONE;
);
(* Present Eisbach/Match variable binding context as normal context elements.
@ -565,7 +560,7 @@ let
val query = if tr = "" then NONE else SOME (tr, pos);
val pr = Apply_Trace.pretty_deps false query ctxt st deps;
in Pretty.writeln pr end
| maybe_trace NONE (ctxt, st) = ()
| maybe_trace NONE _ = ()
val active_debug_threads = Synchronized.var "active_debug_threads" ([] : unit future list);
@ -593,14 +588,14 @@ fun continue i_opt m_opt =
val start_cont = get_continuation ctxt; (* how many breakpoints so far *)
val trans_id = maybe_restart id start_cont (ctxt,thm);
val trans_id = maybe_restart id start_cont;
(* possibly restart if the thread has made too much progress.
trans_id is the current number of restarts, used to avoid manipulating
stale states *)
val _ = nth_pre_result id start_cont; (* block until we've hit the start of this continuation *)
fun get_final n (st as (ctxt,_)) =
fun get_final n st =
case (i_opt,m_opt) of
(SOME i,NONE) => if i < 1 then error "Can only continue a positive number of breakpoints" else
if n = start_cont + i then SOME st else NONE
@ -655,16 +650,16 @@ fun continue i_opt m_opt =
in st'' end))
fun do_apply pos rng opts m =
fun do_apply rng opts m =
let
val {tags, trace, show_running} = opts;
val show_running = #show_running opts;
val batch_mode = is_some (Position.line_of (fst rng));
val show_running = if batch_mode then false else show_running;
val _ = if batch_mode then () else update_max_threads 1;
in
(fn st => map_state (fn (ctxt,thm) =>
(fn st => map_state (fn (ctxt,_) =>
let
val ident = Synchronized.var "debug_state" init_state;
val markup_id = if show_running then SOME (Synchronized.var "markup_state" init_markup_state)
@ -762,9 +757,8 @@ fun apply_debug opts (m', rng) =
val m'' = (fn ctxt => add_debug ctxt m')
val m = (m'',rng)
val pos = Position.thread_data ();
in do_apply pos rng opts m end;
in do_apply rng opts m end;
fun quasi_keyword x = Scan.trace (Args.$$$ x) >>
(fn (s,[tok]) => (Position.reports [(Token.pos_of tok, Markup.quasi_keyword)]; s))

12
lib/Insulin.thy
View File

@ -106,6 +106,7 @@ fun unescape_const s =
let val cs = String.extract (s, String.size desugar_random_tag, NONE) |> String.explode
fun readDelim d (#"_" :: cs) = (d, cs)
| readDelim d (c :: cs) = readDelim (d @ [c]) cs
| readDelim _ [] = raise Match
val (delim, cs) = readDelim [] cs
val delimlen = length delim
fun splitDelim name cs =
@ -180,6 +181,7 @@ fun term_to_unconst (Const (name, typ)) =
fun term_from_unconst (UCConst typ) (name :: consts) =
((if unescape_const name = name then Const else Free) (name, typ), consts)
| term_from_unconst (UCConst _) [] = raise Match
| term_from_unconst (UCAbs (var, typ, body)) consts = let
val (body', consts) = term_from_unconst body consts
in (Abs (var, typ, body'), consts) end
@ -214,14 +216,14 @@ fun focus_list (xs: 'a list): ('a list * 'a * 'a list) list =
(* Do one rewrite pass: try every constant in sequence, then collect the ones which
* reduced the occurrences of bad strings *)
fun rewrite_pass ctxt (t: term) (improved: term -> bool) (escape_const: string -> string): term =
fun rewrite_pass (t: term) (improved: term -> bool) (escape_const: string -> string): term =
let val (ucterm, consts) = term_to_unconst t
fun rewrite_one (prev, const, rest) =
let val (t', []) = term_from_unconst ucterm (prev @ [escape_const const] @ rest)
let val (t', _) = term_from_unconst ucterm (prev @ [escape_const const] @ rest)
in improved t' end
val consts_to_rewrite = focus_list consts |> map rewrite_one
val consts' = map2 (fn rewr => fn const => if rewr then escape_const const else const) consts_to_rewrite consts
val (t', []) = term_from_unconst ucterm consts'
val (t', _) = term_from_unconst ucterm consts'
in t' end
(* Do rewrite passes until bad strings are gone or no more rewrites are possible *)
@ -230,8 +232,8 @@ fun desugar ctxt (t0: term) (bads: string list): term =
val _ = if null bads then error "Nothing to desugar" else ()
fun rewrite t = let
val counts0 = count t
fun improved t' = exists (<) (count t' ~~ counts0)
val t' = rewrite_pass ctxt t improved escape_const
fun improved t' = exists (op <) (count t' ~~ counts0)
val t' = rewrite_pass t improved escape_const
in if forall (fn c => c = 0) (count t') (* bad strings gone *)
then t'
else if t = t' (* no more rewrites *)

4
lib/Match_Abbreviation.thy
View File

@ -49,10 +49,10 @@ fun find_term ctxt get pat t = find_term1 ctxt get t
fun lambda_frees_vars ctxt ord_t t = let
fun is_free t = is_Free t andalso not (Variable.is_fixed ctxt (Term.term_name t))
fun is_it t = is_free t orelse is_Var t
val get = fold_aterms (fn t => if is_it t then insert (=) t else I)
val get = fold_aterms (fn t => if is_it t then insert (op =) t else I)
val all_vars = get ord_t []
val vars = get t []
val ord_vars = filter (member (=) vars) all_vars
val ord_vars = filter (member (op =) vars) all_vars
in fold lambda ord_vars t end
fun parse_pat_fixes ctxt fixes pats = let

7
lib/Monad_WP/Datatype_Schematic.thy
View File

@ -120,7 +120,7 @@ fun get_action ctxt prop = let
val (fname, T) = dest_Const c
val acts = Symtab.lookup_list actions fname
fun interesting arg = not (member Term.aconv_untyped xs arg)
andalso exists (fn i => not (member (=) xs (Bound i)))
andalso exists (fn i => not (member (op =) xs (Bound i)))
(Term.loose_bnos arg)
in the (sfirst acts (fn (i, selname, thms) => if interesting (nth ys i)
then SOME (var, idx, mk_sel selname T i, thms) else NONE))
@ -209,7 +209,8 @@ local
val rhs_var = rhs |> Term.dest_Var |> fst;
val data_name = Term.dest_Const data_const |> fst;
val rhs_idx = ListExtras.find_index (curry op = rhs_var) data_vars |> the;
in (fun_name, data_name, rhs_idx) end;
in (fun_name, data_name, rhs_idx) end
| t => raise TERM("unexpected", [t]);
in
fun dest_accessor ctxt thm =
case try dest_accessor' thm of
@ -276,7 +277,7 @@ datatype foo =
| another nat
primrec get_basic_0 where
"get_basic_0 (basic x0 x1) = x0"
"get_basic_0 (basic x0 x1) = x0"
primrec get_nat where
"get_nat (basic x _) = x"

1
lib/Monad_WP/NonDetMonad.thy
View File

@ -116,6 +116,7 @@ definition
select :: "'a set \<Rightarrow> ('s,'a) nondet_monad" where
"select A \<equiv> \<lambda>s. (A \<times> {s}, False)"
(* FIXME isa: at the end of the update, retire "OR", use \<sqinter> everywhere instead *)
definition
alternative :: "('s,'a) nondet_monad \<Rightarrow> ('s,'a) nondet_monad \<Rightarrow>
('s,'a) nondet_monad"

2
lib/Monad_WP/wp/WPC.thy
View File

@ -152,7 +152,7 @@ end;
(* give each rule in the list one possible resolution outcome *)
fun resolve_each_once_tac ctxt thms i
= fold (curry (APPEND'))
= fold (curry (op APPEND'))
(map (DETERM oo resolve_tac ctxt o single) thms)
(K no_tac) i

3
lib/ShowTypes.thy
View File

@ -49,8 +49,7 @@ fun pretty_markup_to_string no_markup =
#> (if no_markup then XML.content_of else YXML.string_of_body)
fun term_show_types no_markup ctxt term =
let val keywords = Thy_Header.get_keywords' ctxt
val ctxt' = ctxt
let val ctxt' = ctxt
|> Config.put show_markup false
|> Config.put Printer.show_type_emphasis false

8
lib/Trace_Schematic_Insts.thy
View File

@ -342,7 +342,7 @@ fun instantiate_terms ctxt bounds var_insts term =
to above, to deal with bound variables we first need to drop any binders
that had been added to the instantiations.
\<close>
fun instantiate_types ctxt bounds_num tvar_insts term =
fun instantiate_types ctxt _ tvar_insts term =
let
fun instantiateT tvar_inst typ =
let
@ -357,10 +357,10 @@ fun instantiate_types ctxt bounds_num tvar_insts term =
\<comment> \<open>
Instantiate a given thm with the supplied instantiations, returning a term.
\<close>
fun instantiate_thm ctxt thm {bounds, terms as var_insts, typs as tvar_insts} =
fun instantiate_thm ctxt thm {bounds, terms, typs} =
Thm.prop_of thm
|> instantiate_terms ctxt bounds var_insts
|> instantiate_types ctxt (length bounds) tvar_insts
|> instantiate_terms ctxt bounds terms
|> instantiate_types ctxt (length bounds) typs
fun filtered_instantiation_lines ctxt {bounds, terms, typs} =
let

2
lib/Try_Methods.thy
View File

@ -69,7 +69,7 @@ fun independent_subgoals goal verbose = let
t Termtab.empty
val goals = Thm.prems_of goal
val goal_vars = map get_vars goals
val count_vars = fold (fn t1 => fn t2 => Termtab.join (K (+))
val count_vars = fold (fn t1 => fn t2 => Termtab.join (K (op +))
(Termtab.map (K (K 1)) t1, t2)) goal_vars Termtab.empty
val indep_vars = Termtab.forall (fst #> Termtab.lookup count_vars
#> (fn n => n = SOME 1))

4
lib/ml-helpers/TermPatternAntiquote.thy
View File

@ -51,9 +51,9 @@ fun gen_term_pattern (Var (("_dummy_", _), _)) = "_"
(* Create term pattern. All Var names must be distinct in order to generate ML variables. *)
fun term_pattern_antiquote ctxt s =
let val pat = Proof_Context.read_term_pattern ctxt s
val add_var_names' = fold_aterms (fn Var (v, _) => curry (::) v | _ => I);
val add_var_names' = fold_aterms (fn Var (v, _) => curry (op ::) v | _ => I);
val vars = add_var_names' pat [] |> filter (fn (n, _) => n <> "_dummy_")
val _ = if vars = distinct (=) vars then () else
val _ = if vars = distinct (op =) vars then () else
raise TERM ("Pattern contains duplicate vars", [pat])
in "(" ^ gen_term_pattern pat ^ ")" end

4
spec/abstract/ARM/Machine_A.thy
View File

@ -82,11 +82,11 @@ definition
definition
combine_ntfn_badges :: "data \<Rightarrow> data \<Rightarrow> data" where
"combine_ntfn_badges \<equiv> (OR)"
"combine_ntfn_badges \<equiv> semiring_bit_operations_class.or"
definition
combine_ntfn_msgs :: "data \<Rightarrow> data \<Rightarrow> data" where
"combine_ntfn_msgs \<equiv> (OR)"
"combine_ntfn_msgs \<equiv> semiring_bit_operations_class.or"
text \<open>These definitions will be unfolded automatically in proofs.\<close>