--- a/src/HOL/SPARK/Tools/spark_vcs.ML Thu Apr 14 15:04:42 2011 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Fri Apr 15 15:33:57 2011 +0200
@@ -7,11 +7,12 @@
signature SPARK_VCS =
sig
- val set_vcs: Fdl_Parser.decls -> Fdl_Parser.rules -> Fdl_Parser.vcs ->
- Path.T -> theory -> theory
+ val set_vcs: Fdl_Parser.decls -> Fdl_Parser.rules ->
+ (string * string) * Fdl_Parser.vcs -> Path.T -> theory -> theory
val add_proof_fun: (typ option -> 'a -> term) ->
string * ((string list * string) option * 'a) ->
theory -> theory
+ val add_type: string * typ -> theory -> theory
val lookup_vc: theory -> string -> (Element.context_i list *
(string * thm list option * Element.context_i * Element.statement_i)) option
val get_vcs: theory ->
@@ -28,8 +29,49 @@
open Fdl_Parser;
+(** theory data **)
+
+fun err_unfinished () = error "An unfinished SPARK environment is still open."
+
+val strip_number = pairself implode o take_suffix Fdl_Lexer.is_digit o raw_explode;
+
+val name_ord = prod_ord string_ord (option_ord int_ord) o
+ pairself (strip_number ##> Int.fromString);
+
+structure VCtab = Table(type key = string val ord = name_ord);
+
+structure VCs = Theory_Data
+(
+ type T =
+ {pfuns: ((string list * string) option * term) Symtab.table,
+ type_map: typ Symtab.table,
+ env:
+ {ctxt: Element.context_i list,
+ defs: (binding * thm) list,
+ types: fdl_type tab,
+ funs: (string list * string) tab,
+ ids: (term * string) Symtab.table * Name.context,
+ proving: bool,
+ vcs: (string * thm list option *
+ (string * expr) list * (string * expr) list) VCtab.table,
+ path: Path.T} option}
+ val empty : T = {pfuns = Symtab.empty, type_map = Symtab.empty, env = NONE}
+ val extend = I
+ fun merge ({pfuns = pfuns1, type_map = type_map1, env = NONE},
+ {pfuns = pfuns2, type_map = type_map2, env = NONE}) =
+ {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2),
+ type_map = Symtab.merge (op =) (type_map1, type_map2),
+ env = NONE}
+ | merge _ = err_unfinished ()
+)
+
+
(** utilities **)
+val to_lower = raw_explode #> map Symbol.to_ascii_lower #> implode;
+
+val lcase_eq = (op =) o pairself (to_lower o Long_Name.base_name);
+
fun mk_unop s t =
let val T = fastype_of t
in Const (s, T --> T) $ t end;
@@ -44,17 +86,22 @@
HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u)
end;
+fun get_type thy ty =
+ let val {type_map, ...} = VCs.get thy
+ in Symtab.lookup type_map ty end;
+
fun mk_type _ "integer" = HOLogic.intT
| mk_type _ "boolean" = HOLogic.boolT
- | mk_type thy ty = Syntax.check_typ (ProofContext.init_global thy)
- (Type (Sign.full_name thy (Binding.name ty), []));
+ | mk_type thy ty =
+ (case get_type thy ty of
+ NONE =>
+ Syntax.check_typ (ProofContext.init_global thy)
+ (Type (Sign.full_name thy (Binding.name ty), []))
+ | SOME T => T);
val booleanN = "boolean";
val integerN = "integer";
-fun mk_qual_name thy s s' =
- Sign.full_name thy (Binding.qualify true s (Binding.name s'));
-
fun define_overloaded (def_name, eq) lthy =
let
val ((c, _), rhs) = eq |> Syntax.check_term lthy |>
@@ -80,17 +127,29 @@
val zs = map (Free o rpair T) ys;
in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end;
+fun get_record_info thy T = (case Record.dest_recTs T of
+ [(tyname, [@{typ unit}])] =>
+ Record.get_info thy (Long_Name.qualifier tyname)
+ | _ => NONE);
+
+fun find_field fname = find_first (curry lcase_eq fname o fst);
+
+fun find_field' fname = get_first (fn (flds, fldty) =>
+ if member (op =) flds fname then SOME fldty else NONE);
+
+fun assoc_ty_err thy T s msg =
+ error ("Type " ^ Syntax.string_of_typ_global thy T ^
+ " associated with SPARK type " ^ s ^ "\n" ^ msg);
+
(** generate properties of enumeration types **)
-fun add_enum_type tyname els (tab, ctxt) thy =
+fun add_enum_type tyname tyname' thy =
let
- val tyb = Binding.name tyname;
- val tyname' = Sign.full_name thy tyb;
+ val {case_name, ...} = the (Datatype_Data.get_info thy tyname');
+ val cs = map Const (the (Datatype_Data.get_constrs thy tyname'));
+ val k = length cs;
val T = Type (tyname', []);
- val case_name = mk_qual_name thy tyname (tyname ^ "_case");
- val cs = map (fn s => Const (mk_qual_name thy tyname s, T)) els;
- val k = length els;
val p = Const (@{const_name pos}, T --> HOLogic.intT);
val v = Const (@{const_name val}, HOLogic.intT --> T);
val card = Const (@{const_name card},
@@ -103,9 +162,6 @@
(f $ Bound 1) $ (f $ Bound 0))));
val (((def1, def2), def3), lthy) = thy |>
- Datatype.add_datatype {strict = true, quiet = true} [tyname]
- [([], tyb, NoSyn,
- map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |>
Class.instantiation ([tyname'], [], @{sort enum}) |>
@@ -195,46 +251,107 @@
val simp_att = [Attrib.internal (K Simplifier.simp_add)]
in
- ((fold (Symtab.update_new o apsnd (rpair tyname)) (els ~~ cs) tab,
- fold Name.declare els ctxt),
- lthy' |>
- Local_Theory.note
- ((Binding.name (tyname ^ "_card_UNIV"), simp_att), [card_UNIV]) ||>>
- Local_Theory.note
- ((Binding.name (tyname ^ "_pos"), simp_att), pos_eqs) ||>>
- Local_Theory.note
- ((Binding.name (tyname ^ "_val"), simp_att), val_eqs) ||>>
- Local_Theory.note
- ((Binding.name (tyname ^ "_first_el"), simp_att), [first_el]) ||>>
- Local_Theory.note
- ((Binding.name (tyname ^ "_last_el"), simp_att), [last_el]) |> snd |>
- Local_Theory.exit_global)
+ lthy' |>
+ Local_Theory.note
+ ((Binding.name (tyname ^ "_card_UNIV"), simp_att), [card_UNIV]) ||>>
+ Local_Theory.note
+ ((Binding.name (tyname ^ "_pos"), simp_att), pos_eqs) ||>>
+ Local_Theory.note
+ ((Binding.name (tyname ^ "_val"), simp_att), val_eqs) ||>>
+ Local_Theory.note
+ ((Binding.name (tyname ^ "_first_el"), simp_att), [first_el]) ||>>
+ Local_Theory.note
+ ((Binding.name (tyname ^ "_last_el"), simp_att), [last_el]) |> snd |>
+ Local_Theory.exit_global
end;
+fun check_no_assoc thy s = case get_type thy s of
+ NONE => ()
+ | SOME _ => error ("Cannot associate a type with " ^ s ^
+ "\nsince it is no record or enumeration type");
+
+fun check_enum [] [] = NONE
+ | check_enum els [] = SOME ("has no element(s) " ^ commas els)
+ | check_enum [] cs = SOME ("has extra element(s) " ^
+ commas (map (Long_Name.base_name o fst) cs))
+ | check_enum (el :: els) ((cname, _) :: cs) =
+ if lcase_eq (el, cname) then check_enum els cs
+ else SOME ("either has no element " ^ el ^
+ " or it is at the wrong position");
+
fun add_type_def (s, Basic_Type ty) (ids, thy) =
- (ids,
- Typedecl.abbrev_global (Binding.name s, [], NoSyn)
- (mk_type thy ty) thy |> snd)
+ (check_no_assoc thy s;
+ (ids,
+ Typedecl.abbrev_global (Binding.name s, [], NoSyn)
+ (mk_type thy ty) thy |> snd))
- | add_type_def (s, Enum_Type els) (ids, thy) = add_enum_type s els ids thy
+ | add_type_def (s, Enum_Type els) ((tab, ctxt), thy) =
+ let
+ val (thy', tyname) = (case get_type thy s of
+ NONE =>
+ let
+ val tyb = Binding.name s;
+ val tyname = Sign.full_name thy tyb
+ in
+ (thy |>
+ Datatype.add_datatype {strict = true, quiet = true} [s]
+ [([], tyb, NoSyn,
+ map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |>
+ add_enum_type s tyname,
+ tyname)
+ end
+ | SOME (T as Type (tyname, [])) =>
+ (case Datatype_Data.get_constrs thy tyname of
+ NONE => assoc_ty_err thy T s "is not a datatype"
+ | SOME cs => (case check_enum els cs of
+ NONE => (thy, tyname)
+ | SOME msg => assoc_ty_err thy T s msg)));
+ val cs = map Const (the (Datatype_Data.get_constrs thy' tyname))
+ in
+ ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,
+ fold Name.declare els ctxt),
+ thy')
+ end
| add_type_def (s, Array_Type (argtys, resty)) (ids, thy) =
- (ids,
- Typedecl.abbrev_global (Binding.name s, [], NoSyn)
- (foldr1 HOLogic.mk_prodT (map (mk_type thy) argtys) -->
- mk_type thy resty) thy |> snd)
+ (check_no_assoc thy s;
+ (ids,
+ Typedecl.abbrev_global (Binding.name s, [], NoSyn)
+ (foldr1 HOLogic.mk_prodT (map (mk_type thy) argtys) -->
+ mk_type thy resty) thy |> snd))
| add_type_def (s, Record_Type fldtys) (ids, thy) =
(ids,
- Record.add_record true ([], Binding.name s) NONE
- (maps (fn (flds, ty) =>
- let val T = mk_type thy ty
- in map (fn fld => (Binding.name fld, T, NoSyn)) flds
- end) fldtys) thy)
+ let val fldTs = maps (fn (flds, ty) =>
+ map (rpair (mk_type thy ty)) flds) fldtys
+ in case get_type thy s of
+ NONE =>
+ Record.add_record true ([], Binding.name s) NONE
+ (map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy
+ | SOME rT =>
+ (case get_record_info thy rT of
+ NONE => assoc_ty_err thy rT s "is not a record type"
+ | SOME {fields, ...} =>
+ (case subtract (lcase_eq o pairself fst) fldTs fields of
+ [] => ()
+ | flds => assoc_ty_err thy rT s ("has extra field(s) " ^
+ commas (map (Long_Name.base_name o fst) flds));
+ map (fn (fld, T) =>
+ case AList.lookup lcase_eq fields fld of
+ NONE => assoc_ty_err thy rT s ("has no field " ^ fld)
+ | SOME U => T = U orelse assoc_ty_err thy rT s
+ ("has field " ^
+ fld ^ " whose type\n" ^
+ Syntax.string_of_typ_global thy U ^
+ "\ndoes not match declared type\n" ^
+ Syntax.string_of_typ_global thy T)) fldTs;
+ thy))
+ end)
| add_type_def (s, Pending_Type) (ids, thy) =
- (ids, Typedecl.typedecl_global (Binding.name s, [], NoSyn) thy |> snd);
+ (check_no_assoc thy s;
+ (ids, Typedecl.typedecl_global (Binding.name s, [], NoSyn) thy |> snd));
fun term_of_expr thy types funs pfuns =
@@ -323,17 +440,16 @@
(case try (unprefix "fld_") s of
SOME fname => (case es of
[e] =>
- let val (t, rcdty) = tm_of vs e
- in case lookup types rcdty of
- SOME (Record_Type fldtys) =>
- (case get_first (fn (flds, fldty) =>
- if member (op =) flds fname then SOME fldty
- else NONE) fldtys of
- SOME fldty =>
- (Const (mk_qual_name thy rcdty fname,
- mk_type thy rcdty --> mk_type thy fldty) $ t,
- fldty)
- | NONE => error ("Record " ^ rcdty ^
+ let
+ val (t, rcdty) = tm_of vs e;
+ val rT = mk_type thy rcdty
+ in case (get_record_info thy rT, lookup types rcdty) of
+ (SOME {fields, ...}, SOME (Record_Type fldtys)) =>
+ (case (find_field fname fields,
+ find_field' fname fldtys) of
+ (SOME (fname', fT), SOME fldty) =>
+ (Const (fname', rT --> fT) $ t, fldty)
+ | _ => error ("Record " ^ rcdty ^
" has no field named " ^ fname))
| _ => error (rcdty ^ " is not a record type")
end
@@ -349,20 +465,20 @@
val rT = mk_type thy rcdty;
val (u, fldty) = tm_of vs e';
val fT = mk_type thy fldty
- in case lookup types rcdty of
- SOME (Record_Type fldtys) =>
- (case get_first (fn (flds, fldty) =>
- if member (op =) flds fname then SOME fldty
- else NONE) fldtys of
- SOME fldty' =>
- if fldty = fldty' then
- (Const (mk_qual_name thy rcdty (fname ^ "_update"),
+ in case get_record_info thy rT of
+ SOME {fields, ...} =>
+ (case find_field fname fields of
+ SOME (fname', fU) =>
+ if fT = fU then
+ (Const (fname' ^ "_update",
(fT --> fT) --> rT --> rT) $
Abs ("x", fT, u) $ t,
rcdty)
- else error ("Type " ^ fldty ^
- " does not match type " ^ fldty' ^ " of field " ^
- fname)
+ else error ("Type\n" ^
+ Syntax.string_of_typ_global thy fT ^
+ "\ndoes not match type\n" ^
+ Syntax.string_of_typ_global thy fU ^
+ "\nof field " ^ fname)
| NONE => error ("Record " ^ rcdty ^
" has no field named " ^ fname))
| _ => error (rcdty ^ " is not a record type")
@@ -431,34 +547,35 @@
end
| tm_of vs (Record (s, flds)) =
- (case lookup types s of
- SOME (Record_Type fldtys) =>
- let
- val flds' = map (apsnd (tm_of vs)) flds;
- val fnames = maps fst fldtys;
- val fnames' = map fst flds;
- val (fvals, ftys) = split_list (map (fn s' =>
- case AList.lookup (op =) flds' s' of
- SOME fval_ty => fval_ty
- | NONE => error ("Field " ^ s' ^ " missing in record " ^ s))
- fnames);
- val _ = (case subtract (op =) fnames fnames' of
- [] => ()
- | xs => error ("Extra field(s) " ^ commas xs ^
- " in record " ^ s));
- val _ = (case duplicates (op =) fnames' of
- [] => ()
- | xs => error ("Duplicate field(s) " ^ commas xs ^
- " in record " ^ s))
- in
- (list_comb
- (Const (mk_qual_name thy s (s ^ "_ext"),
- map (mk_type thy) ftys @ [HOLogic.unitT] --->
- mk_type thy s),
- fvals @ [HOLogic.unit]),
- s)
- end
- | _ => error (s ^ " is not a record type"))
+ let
+ val T = mk_type thy s;
+ val {extension = (ext_name, _), fields, ...} =
+ (case get_record_info thy T of
+ NONE => error (s ^ " is not a record type")
+ | SOME info => info);
+ val flds' = map (apsnd (tm_of vs)) flds;
+ val fnames = map (Long_Name.base_name o fst) fields;
+ val fnames' = map fst flds;
+ val (fvals, ftys) = split_list (map (fn s' =>
+ case AList.lookup lcase_eq flds' s' of
+ SOME fval_ty => fval_ty
+ | NONE => error ("Field " ^ s' ^ " missing in record " ^ s))
+ fnames);
+ val _ = (case subtract lcase_eq fnames fnames' of
+ [] => ()
+ | xs => error ("Extra field(s) " ^ commas xs ^
+ " in record " ^ s));
+ val _ = (case duplicates (op =) fnames' of
+ [] => ()
+ | xs => error ("Duplicate field(s) " ^ commas xs ^
+ " in record " ^ s))
+ in
+ (list_comb
+ (Const (ext_name,
+ map (mk_type thy) ftys @ [HOLogic.unitT] ---> T),
+ fvals @ [HOLogic.unit]),
+ s)
+ end
| tm_of vs (Array (s, default, assocs)) =
(case lookup types s of
@@ -592,44 +709,15 @@
(** the VC store **)
-fun err_unfinished () = error "An unfinished SPARK environment is still open."
-
fun err_vcs names = error (Pretty.string_of
(Pretty.big_list "The following verification conditions have not been proved:"
(map Pretty.str names)))
-val strip_number = pairself implode o take_suffix Fdl_Lexer.is_digit o raw_explode;
-
-val name_ord = prod_ord string_ord (option_ord int_ord) o
- pairself (strip_number ##> Int.fromString);
-
-structure VCtab = Table(type key = string val ord = name_ord);
-
-structure VCs = Theory_Data
-(
- type T =
- {pfuns: ((string list * string) option * term) Symtab.table,
- env:
- {ctxt: Element.context_i list,
- defs: (binding * thm) list,
- types: fdl_type tab,
- funs: (string list * string) tab,
- ids: (term * string) Symtab.table * Name.context,
- proving: bool,
- vcs: (string * thm list option *
- (string * expr) list * (string * expr) list) VCtab.table,
- path: Path.T} option}
- val empty : T = {pfuns = Symtab.empty, env = NONE}
- val extend = I
- fun merge ({pfuns = pfuns1, env = NONE}, {pfuns = pfuns2, env = NONE}) =
- {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2),
- env = NONE}
- | merge _ = err_unfinished ()
-)
-
fun set_env (env as {funs, ...}) thy = VCs.map (fn
- {pfuns, env = NONE} =>
- {pfuns = check_pfuns_types thy funs pfuns, env = SOME env}
+ {pfuns, type_map, env = NONE} =>
+ {pfuns = check_pfuns_types thy funs pfuns,
+ type_map = type_map,
+ env = SOME env}
| _ => err_unfinished ()) thy;
fun mk_pat s = (case Int.fromString s of
@@ -672,28 +760,60 @@
fun add_proof_fun prep (s, (optty, raw_t)) thy =
VCs.map (fn
{env = SOME {proving = true, ...}, ...} => err_unfinished ()
- | {pfuns, env} =>
+ | {pfuns, type_map, env} =>
let
val optty' = (case env of
SOME {funs, ...} => lookup funs s
| NONE => NONE);
val optty'' = NONE |> upd_option optty |> upd_option optty';
- val t = prep (Option.map (pfun_type thy) optty'') raw_t
+ val t = prep (Option.map (pfun_type thy) optty'') raw_t;
+ val _ = (case fold_aterms (fn u =>
+ if is_Var u orelse is_Free u then insert (op =) u else I) t [] of
+ [] => ()
+ | ts => error ("Term\n" ^ Syntax.string_of_term_global thy t ^
+ "\nto be associated with proof function " ^ s ^
+ " contains free variable(s) " ^
+ commas (map (Syntax.string_of_term_global thy) ts)));
in
(check_pfun_type thy s t optty optty';
if is_some optty'' orelse is_none env then
{pfuns = Symtab.update_new (s, (optty'', t)) pfuns,
+ type_map = type_map,
env = env}
handle Symtab.DUP _ => error ("Proof function " ^ s ^
" already associated with function")
else error ("Undeclared proof function " ^ s))
end) thy;
+fun add_type (s, T as Type (tyname, Ts)) thy =
+ thy |>
+ VCs.map (fn
+ {env = SOME _, ...} => err_unfinished ()
+ | {pfuns, type_map, env} =>
+ {pfuns = pfuns,
+ type_map = Symtab.update_new (s, T) type_map,
+ env = env}
+ handle Symtab.DUP _ => error ("SPARK type " ^ s ^
+ " already associated with type")) |>
+ (fn thy' =>
+ case Datatype_Data.get_constrs thy' tyname of
+ NONE => thy'
+ | SOME cs =>
+ if null Ts then
+ (map
+ (fn (_, Type (_, [])) => ()
+ | (cname, _) => assoc_ty_err thy T s
+ ("has illegal constructor " ^
+ Long_Name.base_name cname)) cs;
+ add_enum_type s tyname thy')
+ else assoc_ty_err thy T s "is illegal")
+ | add_type (s, T) thy = assoc_ty_err thy T s "is illegal";
+
val is_closed = is_none o #env o VCs.get;
fun lookup_vc thy name =
(case VCs.get thy of
- {env = SOME {vcs, types, funs, ids, ctxt, ...}, pfuns} =>
+ {env = SOME {vcs, types, funs, ids, ctxt, ...}, pfuns, ...} =>
(case VCtab.lookup vcs name of
SOME vc =>
let val (pfuns', ctxt', ids') =
@@ -703,7 +823,7 @@
| _ => NONE);
fun get_vcs thy = (case VCs.get thy of
- {env = SOME {vcs, types, funs, ids, ctxt, defs, ...}, pfuns} =>
+ {env = SOME {vcs, types, funs, ids, ctxt, defs, ...}, pfuns, ...} =>
let val (pfuns', ctxt', ids') =
declare_missing_pfuns thy funs pfuns vcs ids
in
@@ -714,8 +834,10 @@
| _ => ([], [], []));
fun mark_proved name thms = VCs.map (fn
- {pfuns, env = SOME {ctxt, defs, types, funs, ids, vcs, path, ...}} =>
+ {pfuns, type_map,
+ env = SOME {ctxt, defs, types, funs, ids, vcs, path, ...}} =>
{pfuns = pfuns,
+ type_map = type_map,
env = SOME {ctxt = ctxt, defs = defs,
types = types, funs = funs, ids = ids,
proving = true,
@@ -724,18 +846,21 @@
path = path}}
| x => x);
-fun close thy = VCs.map (fn
- {pfuns, env = SOME {vcs, path, ...}} =>
- (case VCtab.fold_rev (fn vc as (_, (_, p, _, _)) =>
- (if is_some p then apfst else apsnd) (cons vc)) vcs ([], []) of
- (proved, []) =>
- (Thm.join_proofs (maps (the o #2 o snd) proved);
- File.write (Path.ext "prv" path)
- (concat (map (fn (s, _) => snd (strip_number s) ^
- " -- proved by " ^ Distribution.version ^ "\n") proved));
- {pfuns = pfuns, env = NONE})
- | (_, unproved) => err_vcs (map fst unproved))
- | x => x) thy;
+fun close thy =
+ thy |>
+ VCs.map (fn
+ {pfuns, type_map, env = SOME {vcs, path, ...}} =>
+ (case VCtab.fold_rev (fn vc as (_, (_, p, _, _)) =>
+ (if is_some p then apfst else apsnd) (cons vc)) vcs ([], []) of
+ (proved, []) =>
+ (Thm.join_proofs (maps (the o #2 o snd) proved);
+ File.write (Path.ext "prv" path)
+ (concat (map (fn (s, _) => snd (strip_number s) ^
+ " -- proved by " ^ Distribution.version ^ "\n") proved));
+ {pfuns = pfuns, type_map = type_map, env = NONE})
+ | (_, unproved) => err_vcs (map fst unproved))
+ | _ => error "No SPARK environment is currently open") |>
+ Sign.parent_path;
(** set up verification conditions **)
@@ -822,7 +947,8 @@
(remove (op =) d defs) (d :: sdefs)
| NONE => error ("Bad definitions: " ^ rulenames defs));
-fun set_vcs ({types, vars, consts, funs} : decls) (rules, _) vcs path thy =
+fun set_vcs ({types, vars, consts, funs} : decls)
+ (rules, _) ((_, ident), vcs) path thy =
let
val {pfuns, ...} = VCs.get thy;
val (defs, rules') = partition_opt dest_def rules;
@@ -847,7 +973,8 @@
((Symtab.empty |>
Symtab.update ("false", (HOLogic.false_const, booleanN)) |>
Symtab.update ("true", (HOLogic.true_const, booleanN)),
- Name.context), thy) |>
+ Name.context),
+ thy |> Sign.add_path (Long_Name.base_name ident)) |>
fold add_type_def (items types) |>
fold (snd oo add_const) consts' |> (fn ids_thy as ((tab, _), _) =>
ids_thy |>