src/HOL/Tools/SMT/smt_datatypes.ML
author blanchet
Wed, 24 Sep 2014 15:46:40 +0200
changeset 58430 73df5884edcf
parent 58429 0b94858325a5
child 58460 a88eb33058f7
permissions -rw-r--r--
allow homogeneous nesting for SMT (co)datatypes
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57229
diff changeset
     1
(*  Title:      HOL/Tools/SMT/smt_datatypes.ML
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     3
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     4
Collector functions for common type declarations and their representation
58361
7f2b3b6f6ad1 added codatatype support for CVC4
blanchet
parents: 58360
diff changeset
     5
as (co)algebraic datatypes.
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     6
*)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     7
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57229
diff changeset
     8
signature SMT_DATATYPES =
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     9
sig
58429
0b94858325a5 interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents: 58428
diff changeset
    10
  val add_decls: BNF_Util.fp_kind list -> typ ->
0b94858325a5 interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents: 58428
diff changeset
    11
    (BNF_Util.fp_kind * (typ * (term * term list) list)) list list * Proof.context ->
0b94858325a5 interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents: 58428
diff changeset
    12
    (BNF_Util.fp_kind * (typ * (term * term list) list)) list list * Proof.context
57229
blanchet
parents: 57226
diff changeset
    13
end;
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    14
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57229
diff changeset
    15
structure SMT_Datatypes: SMT_DATATYPES =
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    16
struct
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    17
58362
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    18
fun mk_selectors T Ts sels =
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    19
  if null sels then
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    20
    Variable.variant_fixes (replicate (length Ts) "select")
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    21
    #>> map2 (fn U => fn n => Free (n, T --> U)) Ts
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    22
  else
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    23
    pair sels
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    24
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    25
57226
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    26
(* free constructor type declarations *)
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    27
58362
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    28
fun get_ctr_sugar_decl ({ctrs = ctrs0, selss = selss0, ...} : Ctr_Sugar.ctr_sugar) T Ts ctxt =
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    29
  let
58362
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    30
    fun mk_constr ctr0 sels0 =
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    31
      let
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    32
        val sels = map (Ctr_Sugar.mk_disc_or_sel Ts) sels0
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    33
        val ctr = Ctr_Sugar.mk_ctr Ts ctr0
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    34
        val binder_Ts = binder_types (fastype_of ctr)
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    35
      in
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    36
        mk_selectors T binder_Ts sels #>> pair ctr
57226
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    37
      end
58362
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    38
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    39
    val selss = if has_duplicates (op aconv) (flat selss0) then [] else selss0
57226
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    40
  in
58362
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    41
    Ctr_Sugar_Util.fold_map2 mk_constr ctrs0 (Ctr_Sugar_Util.pad_list [] (length ctrs0) selss) ctxt
57226
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    42
    |>> (pair T #> single)
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    43
  end
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    44
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    45
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    46
(* typedef declarations *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    47
57213
9daec42f6784 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents: 56078
diff changeset
    48
fun get_typedef_decl (({Abs_name, Rep_name, abs_type, rep_type, ...}, {Abs_inverse, ...})
9daec42f6784 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents: 56078
diff changeset
    49
    : Typedef.info) T Ts =
9daec42f6784 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents: 56078
diff changeset
    50
  if can (curry (op RS) @{thm UNIV_I}) Abs_inverse then
9daec42f6784 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents: 56078
diff changeset
    51
    let
9daec42f6784 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents: 56078
diff changeset
    52
      val env = snd (Term.dest_Type abs_type) ~~ Ts
9daec42f6784 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents: 56078
diff changeset
    53
      val instT = Term.map_atyps (perhaps (AList.lookup (op =) env))
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    54
57213
9daec42f6784 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents: 56078
diff changeset
    55
      val constr = Const (Abs_name, instT (rep_type --> abs_type))
9daec42f6784 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents: 56078
diff changeset
    56
      val select = Const (Rep_name, instT (abs_type --> rep_type))
9daec42f6784 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents: 56078
diff changeset
    57
    in [(T, [(constr, [select])])] end
9daec42f6784 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents: 56078
diff changeset
    58
  else
9daec42f6784 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents: 56078
diff changeset
    59
    []
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    60
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    61
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    62
(* collection of declarations *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    63
58427
cc1bab5558b0 gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
blanchet
parents: 58364
diff changeset
    64
val extN = "_ext" (* cf. "HOL/Tools/typedef.ML" *)
58361
7f2b3b6f6ad1 added codatatype support for CVC4
blanchet
parents: 58360
diff changeset
    65
58429
0b94858325a5 interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents: 58428
diff changeset
    66
fun get_decls fps T n Ts ctxt =
58361
7f2b3b6f6ad1 added codatatype support for CVC4
blanchet
parents: 58360
diff changeset
    67
  let
58427
cc1bab5558b0 gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
blanchet
parents: 58364
diff changeset
    68
    fun maybe_typedef () =
57226
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    69
      (case Typedef.get_info ctxt n of
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    70
        [] => ([], ctxt)
58429
0b94858325a5 interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents: 58428
diff changeset
    71
      | info :: _ => (map (pair (hd fps)) (get_typedef_decl info T Ts), ctxt))
58361
7f2b3b6f6ad1 added codatatype support for CVC4
blanchet
parents: 58360
diff changeset
    72
  in
58427
cc1bab5558b0 gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
blanchet
parents: 58364
diff changeset
    73
    (case BNF_FP_Def_Sugar.fp_sugar_of ctxt n of
58429
0b94858325a5 interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents: 58428
diff changeset
    74
      SOME {fp, fp_res = {Ts = fp_Ts, ...}, ctr_sugar, ...} =>
0b94858325a5 interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents: 58428
diff changeset
    75
      if member (op =) fps fp then
58428
e4e34dfc3e68 rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents: 58427
diff changeset
    76
        let
e4e34dfc3e68 rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents: 58427
diff changeset
    77
          val ns = map (fst o dest_Type) fp_Ts
e4e34dfc3e68 rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents: 58427
diff changeset
    78
          val mutual_fp_sugars = map_filter (BNF_FP_Def_Sugar.fp_sugar_of ctxt) ns
e4e34dfc3e68 rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents: 58427
diff changeset
    79
          val Xs = map #X mutual_fp_sugars
e4e34dfc3e68 rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents: 58427
diff changeset
    80
          val ctrXs_Tsss = map #ctrXs_Tss mutual_fp_sugars
e4e34dfc3e68 rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents: 58427
diff changeset
    81
58430
73df5884edcf allow homogeneous nesting for SMT (co)datatypes
blanchet
parents: 58429
diff changeset
    82
          (* Datatypes nested through datatypes and codatatypes nested through codatatypes are
73df5884edcf allow homogeneous nesting for SMT (co)datatypes
blanchet
parents: 58429
diff changeset
    83
             allowed. So are mutually (co)recursive (co)datatypes. *)
73df5884edcf allow homogeneous nesting for SMT (co)datatypes
blanchet
parents: 58429
diff changeset
    84
          fun is_same_fp s =
73df5884edcf allow homogeneous nesting for SMT (co)datatypes
blanchet
parents: 58429
diff changeset
    85
            (case BNF_FP_Def_Sugar.fp_sugar_of ctxt s of
73df5884edcf allow homogeneous nesting for SMT (co)datatypes
blanchet
parents: 58429
diff changeset
    86
              SOME {fp = fp', ...} => fp' = fp
73df5884edcf allow homogeneous nesting for SMT (co)datatypes
blanchet
parents: 58429
diff changeset
    87
            | NONE => false)
73df5884edcf allow homogeneous nesting for SMT (co)datatypes
blanchet
parents: 58429
diff changeset
    88
          fun is_homogenously_nested_co_recursive (Type (s, Ts)) =
73df5884edcf allow homogeneous nesting for SMT (co)datatypes
blanchet
parents: 58429
diff changeset
    89
              forall (if is_same_fp s then is_homogenously_nested_co_recursive
73df5884edcf allow homogeneous nesting for SMT (co)datatypes
blanchet
parents: 58429
diff changeset
    90
                else not o BNF_FP_Rec_Sugar_Util.exists_subtype_in Xs) Ts
73df5884edcf allow homogeneous nesting for SMT (co)datatypes
blanchet
parents: 58429
diff changeset
    91
            | is_homogenously_nested_co_recursive _ = true
58428
e4e34dfc3e68 rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents: 58427
diff changeset
    92
        in
58430
73df5884edcf allow homogeneous nesting for SMT (co)datatypes
blanchet
parents: 58429
diff changeset
    93
          if forall (forall (forall is_homogenously_nested_co_recursive)) ctrXs_Tsss then
73df5884edcf allow homogeneous nesting for SMT (co)datatypes
blanchet
parents: 58429
diff changeset
    94
            get_ctr_sugar_decl ctr_sugar T Ts ctxt |>> map (pair fp)
73df5884edcf allow homogeneous nesting for SMT (co)datatypes
blanchet
parents: 58429
diff changeset
    95
          else
73df5884edcf allow homogeneous nesting for SMT (co)datatypes
blanchet
parents: 58429
diff changeset
    96
            maybe_typedef ()
58428
e4e34dfc3e68 rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents: 58427
diff changeset
    97
        end
e4e34dfc3e68 rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents: 58427
diff changeset
    98
      else
e4e34dfc3e68 rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents: 58427
diff changeset
    99
        ([], ctxt)
58427
cc1bab5558b0 gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
blanchet
parents: 58364
diff changeset
   100
    | NONE =>
58429
0b94858325a5 interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents: 58428
diff changeset
   101
      if String.isSuffix extN n then
0b94858325a5 interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents: 58428
diff changeset
   102
        (* for records (FIXME: hack) *)
0b94858325a5 interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents: 58428
diff changeset
   103
        (case Ctr_Sugar.ctr_sugar_of ctxt n of
0b94858325a5 interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents: 58428
diff changeset
   104
          SOME ctr_sugar =>
0b94858325a5 interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents: 58428
diff changeset
   105
          get_ctr_sugar_decl ctr_sugar T Ts ctxt |>> map (pair (hd fps))
0b94858325a5 interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents: 58428
diff changeset
   106
        | NONE => maybe_typedef ())
58427
cc1bab5558b0 gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
blanchet
parents: 58364
diff changeset
   107
      else
58429
0b94858325a5 interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents: 58428
diff changeset
   108
        maybe_typedef ())
58361
7f2b3b6f6ad1 added codatatype support for CVC4
blanchet
parents: 58360
diff changeset
   109
  end
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   110
58429
0b94858325a5 interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents: 58428
diff changeset
   111
fun add_decls fps T (declss, ctxt) =
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   112
  let
58429
0b94858325a5 interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents: 58428
diff changeset
   113
    fun declared T = exists (exists (equal T o fst o snd))
0b94858325a5 interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents: 58428
diff changeset
   114
    fun declared' T = exists (exists (equal T o fst o snd) o snd)
0b94858325a5 interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents: 58428
diff changeset
   115
    fun depends ds = exists (member (op =) (map (fst o snd) ds))
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   116
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   117
    fun add (TFree _) = I
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   118
      | add (TVar _) = I
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   119
      | add (T as Type (@{type_name fun}, _)) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   120
          fold add (Term.body_type T :: Term.binder_types T)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   121
      | add @{typ bool} = I
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   122
      | add (T as Type (n, Ts)) = (fn (dss, ctxt1) =>
58429
0b94858325a5 interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents: 58428
diff changeset
   123
          if declared T declss orelse declared' T dss then
0b94858325a5 interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents: 58428
diff changeset
   124
            (dss, ctxt1)
0b94858325a5 interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents: 58428
diff changeset
   125
          else if SMT_Builtin.is_builtin_typ_ext ctxt1 T then
0b94858325a5 interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents: 58428
diff changeset
   126
            (dss, ctxt1)
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   127
          else
58429
0b94858325a5 interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents: 58428
diff changeset
   128
            (case get_decls fps T n Ts ctxt1 of
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   129
              ([], _) => (dss, ctxt1)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   130
            | (ds, ctxt2) =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   131
                let
58429
0b94858325a5 interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents: 58428
diff changeset
   132
                  val constrTs = maps (map (snd o Term.dest_Const o fst) o snd o snd) ds
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   133
                  val Us = fold (union (op =) o Term.binder_types) constrTs []
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   134
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   135
                  fun ins [] = [(Us, ds)]
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   136
                    | ins ((Uds as (Us', _)) :: Udss) =
58364
blanchet
parents: 58362
diff changeset
   137
                        if depends ds Us' then (Us, ds) :: Uds :: Udss else Uds :: ins Udss
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   138
            in fold add Us (ins dss, ctxt2) end))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   139
  in add T ([], ctxt) |>> append declss o map snd end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   140
57229
blanchet
parents: 57226
diff changeset
   141
end;