--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Jan 04 23:22:53 2019 +0100
@@ -94,23 +94,23 @@
val name_of = fst o dest_Const
val thy = Proof_Context.theory_of ctxt
val (unrep_s, thy) = thy
- |> Sign.declare_const_global ((@{binding nitpick_unrep}, @{typ 'a}),
+ |> Sign.declare_const_global ((\<^binding>\<open>nitpick_unrep\<close>, \<^typ>\<open>'a\<close>),
mixfix (unrep_mixfix (), [], 1000))
|>> name_of
val (maybe_s, thy) = thy
- |> Sign.declare_const_global ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
+ |> Sign.declare_const_global ((\<^binding>\<open>nitpick_maybe\<close>, \<^typ>\<open>'a => 'a\<close>),
mixfix (maybe_mixfix (), [1000], 1000))
|>> name_of
val (abs_s, thy) = thy
- |> Sign.declare_const_global ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
+ |> Sign.declare_const_global ((\<^binding>\<open>nitpick_abs\<close>, \<^typ>\<open>'a => 'b\<close>),
mixfix (abs_mixfix (), [40], 40))
|>> name_of
val (base_s, thy) = thy
- |> Sign.declare_const_global ((@{binding nitpick_base}, @{typ "'a => 'a"}),
+ |> Sign.declare_const_global ((\<^binding>\<open>nitpick_base\<close>, \<^typ>\<open>'a => 'a\<close>),
mixfix (base_mixfix (), [1000], 1000))
|>> name_of
val (step_s, thy) = thy
- |> Sign.declare_const_global ((@{binding nitpick_step}, @{typ "'a => 'a"}),
+ |> Sign.declare_const_global ((\<^binding>\<open>nitpick_step\<close>, \<^typ>\<open>'a => 'a\<close>),
mixfix (step_mixfix (), [1000], 1000))
|>> name_of
in
@@ -145,7 +145,7 @@
Type (s, _) =>
let val s' = shortest_name s in
prefix ^
- (if T = @{typ string} then "s"
+ (if T = \<^typ>\<open>string\<close> then "s"
else if String.isPrefix "\\" s' then s'
else substring (s', 0, 1)) ^ atom_suffix s m
end
@@ -156,7 +156,7 @@
fun nth_atom thy atomss pool T j =
Const (nth_atom_name thy atomss pool "" T j, T)
-fun extract_real_number (Const (@{const_name divide}, _) $ t1 $ t2) =
+fun extract_real_number (Const (\<^const_name>\<open>divide\<close>, _) $ t1 $ t2) =
real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
| extract_real_number t = real (snd (HOLogic.dest_number t))
@@ -192,14 +192,14 @@
fun tuple_list_for_name rel_table bounds name =
the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
-fun unarize_unbox_etc_term (Const (@{const_name FunBox}, _) $ t1) =
+fun unarize_unbox_etc_term (Const (\<^const_name>\<open>FunBox\<close>, _) $ t1) =
unarize_unbox_etc_term t1
| unarize_unbox_etc_term
- (Const (@{const_name PairBox},
- Type (@{type_name fun}, [T1, Type (@{type_name fun}, [T2, _])]))
+ (Const (\<^const_name>\<open>PairBox\<close>,
+ Type (\<^type_name>\<open>fun\<close>, [T1, Type (\<^type_name>\<open>fun\<close>, [T2, _])]))
$ t1 $ t2) =
let val Ts = map uniterize_unarize_unbox_etc_type [T1, T2] in
- Const (@{const_name Pair}, Ts ---> Type (@{type_name prod}, Ts))
+ Const (\<^const_name>\<open>Pair\<close>, Ts ---> Type (\<^type_name>\<open>prod\<close>, Ts))
$ unarize_unbox_etc_term t1 $ unarize_unbox_etc_term t2
end
| unarize_unbox_etc_term (Const (s, T)) =
@@ -214,27 +214,27 @@
| unarize_unbox_etc_term (Abs (s, T, t')) =
Abs (s, uniterize_unarize_unbox_etc_type T, unarize_unbox_etc_term t')
-fun factor_out_types (T1 as Type (@{type_name prod}, [T11, T12]))
- (T2 as Type (@{type_name prod}, [T21, T22])) =
+fun factor_out_types (T1 as Type (\<^type_name>\<open>prod\<close>, [T11, T12]))
+ (T2 as Type (\<^type_name>\<open>prod\<close>, [T21, T22])) =
let val (n1, n2) = apply2 num_factors_in_type (T11, T21) in
if n1 = n2 then
let
val ((T11', opt_T12'), (T21', opt_T22')) = factor_out_types T12 T22
in
- ((Type (@{type_name prod}, [T11, T11']), opt_T12'),
- (Type (@{type_name prod}, [T21, T21']), opt_T22'))
+ ((Type (\<^type_name>\<open>prod\<close>, [T11, T11']), opt_T12'),
+ (Type (\<^type_name>\<open>prod\<close>, [T21, T21']), opt_T22'))
end
else if n1 < n2 then
case factor_out_types T1 T21 of
(p1, (T21', NONE)) => (p1, (T21', SOME T22))
| (p1, (T21', SOME T22')) =>
- (p1, (T21', SOME (Type (@{type_name prod}, [T22', T22]))))
+ (p1, (T21', SOME (Type (\<^type_name>\<open>prod\<close>, [T22', T22]))))
else
swap (factor_out_types T2 T1)
end
- | factor_out_types (Type (@{type_name prod}, [T11, T12])) T2 =
+ | factor_out_types (Type (\<^type_name>\<open>prod\<close>, [T11, T12])) T2 =
((T11, SOME T12), (T2, NONE))
- | factor_out_types T1 (Type (@{type_name prod}, [T21, T22])) =
+ | factor_out_types T1 (Type (\<^type_name>\<open>prod\<close>, [T21, T22])) =
((T1, NONE), (T21, SOME T22))
| factor_out_types T1 T2 = ((T1, NONE), (T2, NONE))
@@ -245,19 +245,19 @@
fun aux T1 T2 [] =
Const (if maybe_opt then opt_flag else non_opt_flag, T1 --> T2)
| aux T1 T2 ((t1, t2) :: tps) =
- Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
+ Const (\<^const_name>\<open>fun_upd\<close>, (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
$ aux T1 T2 tps $ t1 $ t2
in aux T1 T2 o rev end
fun is_plain_fun (Const (s, _)) = (s = opt_flag orelse s = non_opt_flag)
- | is_plain_fun (Const (@{const_name fun_upd}, _) $ t0 $ _ $ _) =
+ | is_plain_fun (Const (\<^const_name>\<open>fun_upd\<close>, _) $ t0 $ _ $ _) =
is_plain_fun t0
| is_plain_fun _ = false
val dest_plain_fun =
let
fun aux (Abs (_, _, Const (s, _))) = (s <> irrelevant, ([], []))
| aux (Const (s, _)) = (s <> non_opt_flag, ([], []))
- | aux (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
+ | aux (Const (\<^const_name>\<open>fun_upd\<close>, _) $ t0 $ t1 $ t2) =
let val (maybe_opt, (ts1, ts2)) = aux t0 in
(maybe_opt, (t1 :: ts1, t2 :: ts2))
end
@@ -272,10 +272,10 @@
val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut
in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end
-fun pair_up (Type (@{type_name prod}, [T1', T2']))
- (t1 as Const (@{const_name Pair},
- Type (@{type_name fun},
- [_, Type (@{type_name fun}, [_, T1])]))
+fun pair_up (Type (\<^type_name>\<open>prod\<close>, [T1', T2']))
+ (t1 as Const (\<^const_name>\<open>Pair\<close>,
+ Type (\<^type_name>\<open>fun\<close>,
+ [_, Type (\<^type_name>\<open>fun\<close>, [_, T1])]))
$ t11 $ t12) t2 =
if T1 = T1' then HOLogic.mk_prod (t1, t2)
else HOLogic.mk_prod (t11, pair_up T2' t12 t2)
@@ -306,8 +306,8 @@
in make_plain_fun maybe_opt T1 T2 tps end
and do_arrow T1' T2' _ _ (Const (s, _)) = Const (s, T1' --> T2')
| do_arrow T1' T2' T1 T2
- (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
- Const (@{const_name fun_upd},
+ (Const (\<^const_name>\<open>fun_upd\<close>, _) $ t0 $ t1 $ t2) =
+ Const (\<^const_name>\<open>fun_upd\<close>,
(T1' --> T2') --> T1' --> T2' --> T1' --> T2')
$ do_arrow T1' T2' T1 T2 t0 $ do_term T1' T1 t1 $ do_term T2' T2 t2
| do_arrow _ _ _ _ t =
@@ -320,13 +320,13 @@
| ((T1a', SOME T1b'), (_, NONE)) =>
t |> do_arrow T1a' (T1b' --> T2') T1 T2 |> do_uncurry T1' T2'
| _ => raise TYPE ("Nitpick_Model.format_fun.do_fun", [T1, T1'], [])
- and do_term (Type (@{type_name fun}, [T1', T2']))
- (Type (@{type_name fun}, [T1, T2])) t =
+ and do_term (Type (\<^type_name>\<open>fun\<close>, [T1', T2']))
+ (Type (\<^type_name>\<open>fun\<close>, [T1, T2])) t =
do_fun T1' T2' T1 T2 t
- | do_term (T' as Type (@{type_name prod}, Ts' as [T1', T2']))
- (Type (@{type_name prod}, [T1, T2]))
- (Const (@{const_name Pair}, _) $ t1 $ t2) =
- Const (@{const_name Pair}, Ts' ---> T')
+ | do_term (T' as Type (\<^type_name>\<open>prod\<close>, Ts' as [T1', T2']))
+ (Type (\<^type_name>\<open>prod\<close>, [T1, T2]))
+ (Const (\<^const_name>\<open>Pair\<close>, _) $ t1 $ t2) =
+ Const (\<^const_name>\<open>Pair\<close>, Ts' ---> T')
$ do_term T1' T1 t1 $ do_term T2' T2 t2
| do_term T' T t =
if T = T' then t
@@ -337,7 +337,7 @@
| truth_const_sort_key @{const False} = "2"
| truth_const_sort_key _ = "1"
-fun mk_tuple (Type (@{type_name prod}, [T1, T2])) ts =
+fun mk_tuple (Type (\<^type_name>\<open>prod\<close>, [T1, T2])) ts =
HOLogic.mk_prod (mk_tuple T1 ts,
mk_tuple T2 (List.drop (ts, length (HOLogic.flatten_tupleT T1))))
| mk_tuple _ (t :: _) = t
@@ -375,7 +375,7 @@
let
fun value_of_bits jss =
let
- val j0 = offset_of_type ofs @{typ unsigned_bit}
+ val j0 = offset_of_type ofs \<^typ>\<open>unsigned_bit\<close>
val js = map (Integer.add (~ j0) o the_single) jss
in
fold (fn j => Integer.add (reasonable_power 2 j |> j = bits ? op ~))
@@ -384,7 +384,7 @@
val all_values =
all_values_of_type pool wacky_names scope atomss sel_names rel_table
bounds 0
- fun postprocess_term (Type (@{type_name fun}, _)) = I
+ fun postprocess_term (Type (\<^type_name>\<open>fun\<close>, _)) = I
| postprocess_term T =
case Data.get (Context.Proof ctxt) of
[] => I
@@ -402,8 +402,8 @@
fun make_set maybe_opt T tps =
let
val set_T = HOLogic.mk_setT T
- val empty_const = Const (@{const_abbrev Set.empty}, set_T)
- val insert_const = Const (@{const_name insert}, T --> set_T --> set_T)
+ val empty_const = Const (\<^const_abbrev>\<open>Set.empty\<close>, set_T)
+ val insert_const = Const (\<^const_name>\<open>insert\<close>, T --> set_T --> set_T)
fun aux [] =
if maybe_opt andalso not (is_complete_type data_types false T) then
insert_const $ Const (unrep_name, T) $ empty_const
@@ -426,26 +426,26 @@
end
fun make_map maybe_opt T1 T2 T2' =
let
- val update_const = Const (@{const_name fun_upd},
+ val update_const = Const (\<^const_name>\<open>fun_upd\<close>,
(T1 --> T2) --> T1 --> T2 --> T1 --> T2)
- fun aux' [] = Const (@{const_abbrev Map.empty}, T1 --> T2)
+ fun aux' [] = Const (\<^const_abbrev>\<open>Map.empty\<close>, T1 --> T2)
| aux' ((t1, t2) :: tps) =
(case t2 of
- Const (@{const_name None}, _) => aux' tps
+ Const (\<^const_name>\<open>None\<close>, _) => aux' tps
| _ => update_const $ aux' tps $ t1 $ t2)
fun aux tps =
if maybe_opt andalso not (is_complete_type data_types false T1) then
update_const $ aux' tps $ Const (unrep_name, T1)
- $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
+ $ (Const (\<^const_name>\<open>Some\<close>, T2' --> T2) $ Const (unknown, T2'))
else
aux' tps
in aux end
fun polish_funs Ts t =
(case fastype_of1 (Ts, t) of
- Type (@{type_name fun}, [T1, T2]) =>
+ Type (\<^type_name>\<open>fun\<close>, [T1, T2]) =>
if is_plain_fun t then
case T2 of
- Type (@{type_name option}, [T2']) =>
+ Type (\<^type_name>\<open>option\<close>, [T2']) =>
let
val (maybe_opt, ts_pair) =
dest_plain_fun t ||> apply2 (map (polish_funs Ts))
@@ -456,13 +456,13 @@
| _ => raise SAME ())
handle SAME () =>
case t of
- (t1 as Const (@{const_name fun_upd}, _) $ t11 $ _)
+ (t1 as Const (\<^const_name>\<open>fun_upd\<close>, _) $ t11 $ _)
$ (t2 as Const (s, _)) =>
if s = unknown then polish_funs Ts t11
else polish_funs Ts t1 $ polish_funs Ts t2
| t1 $ t2 => polish_funs Ts t1 $ polish_funs Ts t2
| Abs (s, T, t') => Abs (s, T, polish_funs (T :: Ts) t')
- | Const (s, Type (@{type_name fun}, [T1, T2])) =>
+ | Const (s, Type (\<^type_name>\<open>fun\<close>, [T1, T2])) =>
if s = opt_flag orelse s = non_opt_flag then
Abs ("x", T1,
Const (if is_complete_type data_types false T1 then
@@ -476,7 +476,7 @@
ts1 ~~ ts2
|> sort (nice_term_ord o apply2 fst)
|> (case T of
- Type (@{type_name set}, _) =>
+ Type (\<^type_name>\<open>set\<close>, _) =>
sort_by (truth_const_sort_key o snd)
#> make_set maybe_opt T'
| _ =>
@@ -499,11 +499,11 @@
signed_string_of_int j ^ " for " ^
string_for_rep (Vect (k1, Atom (k2, 0))))
end
- and term_for_atom seen (T as Type (@{type_name fun}, _)) T' j _ =
+ and term_for_atom seen (T as Type (\<^type_name>\<open>fun\<close>, _)) T' j _ =
term_for_fun_or_set seen T T' j
- | term_for_atom seen (T as Type (@{type_name set}, _)) T' j _ =
+ | term_for_atom seen (T as Type (\<^type_name>\<open>set\<close>, _)) T' j _ =
term_for_fun_or_set seen T T' j
- | term_for_atom seen (Type (@{type_name prod}, [T1, T2])) _ j k =
+ | term_for_atom seen (Type (\<^type_name>\<open>prod\<close>, [T1, T2])) _ j k =
let
val k1 = card_of_type card_assigns T1
val k2 = k div k1
@@ -513,9 +513,9 @@
(* ### k2 or k1? FIXME *)
[j div k2, j mod k2] [k1, k2])
end
- | term_for_atom seen @{typ prop} _ j k =
+ | term_for_atom seen \<^typ>\<open>prop\<close> _ j k =
HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j k)
- | term_for_atom _ @{typ bool} _ j _ =
+ | term_for_atom _ \<^typ>\<open>bool\<close> _ j _ =
if j = 0 then @{const False} else @{const True}
| term_for_atom seen T _ j k =
if T = nat_T then
@@ -524,7 +524,7 @@
HOLogic.mk_number int_T (int_for_atom (k, 0) j)
else if is_fp_iterator_type T then
HOLogic.mk_number nat_T (k - j - 1)
- else if T = @{typ bisim_iterator} then
+ else if T = \<^typ>\<open>bisim_iterator\<close> then
HOLogic.mk_number nat_T j
else case data_type_spec data_types T of
NONE => nth_atom thy atomss pool T j
@@ -567,9 +567,9 @@
if co andalso not (null seen) andalso
member (op =) (seen |> unfold ? (fst o split_last)) (T, j) then
cyclic_var ()
- else if constr_s = @{const_name Word} then
+ else if constr_s = \<^const_name>\<open>Word\<close> then
HOLogic.mk_number
- (if T = @{typ "unsigned_bit word"} then nat_T else int_T)
+ (if T = \<^typ>\<open>unsigned_bit word\<close> then nat_T else int_T)
(value_of_bits (the_single arg_jsss))
else
let
@@ -583,14 +583,14 @@
|> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts)
|> dest_n_tuple (length uncur_arg_Ts)
val t =
- if constr_s = @{const_name Abs_Frac} then
+ if constr_s = \<^const_name>\<open>Abs_Frac\<close> then
case ts of
- [Const (@{const_name Pair}, _) $ t1 $ t2] =>
+ [Const (\<^const_name>\<open>Pair\<close>, _) $ t1 $ t2] =>
frac_from_term_pair (body_type T) t1 t2
| _ => raise TERM ("Nitpick_Model.reconstruct_term.\
\term_for_atom (Abs_Frac)", ts)
else if is_abs_fun ctxt constr_x orelse
- constr_s = @{const_name Quot} then
+ constr_s = \<^const_name>\<open>Quot\<close> then
Const (abs_name, constr_T) $ the_single ts
else
list_comb (Const constr_x, ts)
@@ -599,9 +599,9 @@
let val var = cyclic_var () in
if exists_subterm (curry (op =) var) t then
if co then
- Const (@{const_name The}, (T --> bool_T) --> T)
+ Const (\<^const_name>\<open>The\<close>, (T --> bool_T) --> T)
$ Abs (cyclic_co_val_name (), T,
- Const (@{const_name HOL.eq}, T --> T --> bool_T)
+ Const (\<^const_name>\<open>HOL.eq\<close>, T --> T --> bool_T)
$ Bound 0 $ abstract_over (var, t))
else
cyclic_atom ()
@@ -625,7 +625,7 @@
and term_for_rep _ seen T T' (R as Atom (k, j0)) [[j]] =
if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k
else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R])
- | term_for_rep _ seen (Type (@{type_name prod}, [T1, T2])) _
+ | term_for_rep _ seen (Type (\<^type_name>\<open>prod\<close>, [T1, T2])) _
(Struct [R1, R2]) [js] =
let
val arity1 = arity_of_rep R1
@@ -857,8 +857,8 @@
(** Model reconstruction **)
-fun unfold_outer_the_binders (t as Const (@{const_name The}, _)
- $ Abs (s, T, Const (@{const_name HOL.eq}, _)
+fun unfold_outer_the_binders (t as Const (\<^const_name>\<open>The\<close>, _)
+ $ Abs (s, T, Const (\<^const_name>\<open>HOL.eq\<close>, _)
$ Bound 0 $ t')) =
betapply (Abs (s, T, t'), t) |> unfold_outer_the_binders
| unfold_outer_the_binders t = t
@@ -886,7 +886,7 @@
fun add_fake_const s =
Symbol_Pos.is_identifier s
- ? (#2 o Sign.declare_const_global ((Binding.name s, @{typ 'a}), NoSyn))
+ ? (#2 o Sign.declare_const_global ((Binding.name s, \<^typ>\<open>'a\<close>), NoSyn))
val globals = Term.add_const_names t []
|> filter_out (String.isSubstring Long_Name.separator)
@@ -961,7 +961,7 @@
| _ => raise NUT ("Nitpick_Model.reconstruct_hol_model.\
\pretty_for_assign", [name])
val t2 = if rep_of name = Any then
- Const (@{const_name undefined}, T')
+ Const (\<^const_name>\<open>undefined\<close>, T')
else
tuple_list_for_name rel_table bounds name
|> term_for_rep (not (is_fully_representable_set name)) false
@@ -975,8 +975,8 @@
Pretty.block (Pretty.breaks
(pretty_for_type ctxt typ ::
(case typ of
- Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"]
- | Type (@{type_name pair_box}, _) => [Pretty.str "[boxed]"]
+ Type (\<^type_name>\<open>fun_box\<close>, _) => [Pretty.str "[boxed]"]
+ | Type (\<^type_name>\<open>pair_box\<close>, _) => [Pretty.str "[boxed]"]
| _ => []) @
[Pretty.str "=",
Pretty.enum "," "{" "}"
@@ -1017,8 +1017,8 @@
val (eval_names, noneval_nonskolem_nonsel_names) =
List.partition (String.isPrefix eval_prefix o nickname_of)
nonskolem_nonsel_names
- ||> filter_out (member (op =) [@{const_name bisim},
- @{const_name bisim_iterator_max}]
+ ||> filter_out (member (op =) [\<^const_name>\<open>bisim\<close>,
+ \<^const_name>\<open>bisim_iterator_max\<close>]
o nickname_of)
||> append (map_filter (free_name_for_term false) pseudo_frees)
val real_free_names = map_filter (free_name_for_term true) real_frees