src/HOL/Library/Old_SMT/old_smt_datatypes.ML
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 58058 1a0b18176548
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     1
(*  Title:      HOL/Library/Old_SMT/old_smt_datatypes.ML
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
     3
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
     4
Collector functions for common type declarations and their representation
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
     5
as algebraic datatypes.
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
     6
*)
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
     7
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     8
signature OLD_SMT_DATATYPES =
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
     9
sig
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    10
  val add_decls: typ ->
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    11
    (typ * (term * term list) list) list list * Proof.context ->
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    12
    (typ * (term * term list) list) list list * Proof.context
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    13
end
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    14
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    15
structure Old_SMT_Datatypes: OLD_SMT_DATATYPES =
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    16
struct
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    17
57226
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    18
fun mk_selectors T Ts =
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    19
  Variable.variant_fixes (replicate (length Ts) "select")
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    20
  #>> map2 (fn U => fn n => Free (n, T --> U)) Ts
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    21
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    22
57226
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    23
(* free constructor type declarations *)
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    24
57226
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    25
fun get_ctr_sugar_decl ({ctrs, ...} : Ctr_Sugar.ctr_sugar) T Ts ctxt =
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    26
  let
57226
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    27
    fun mk_constr ctr0 =
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    28
      let val ctr = Ctr_Sugar.mk_ctr Ts ctr0 in
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    29
        mk_selectors T (binder_types (fastype_of ctr)) #>> pair ctr
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    30
      end
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    31
  in
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    32
    fold_map mk_constr ctrs ctxt
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    33
    |>> (pair T #> single)
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    34
  end
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    35
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    36
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    37
(* typedef declarations *)
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    38
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: 43385
diff changeset
    39
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: 43385
diff changeset
    40
    : 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: 43385
diff changeset
    41
  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: 43385
diff changeset
    42
    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: 43385
diff changeset
    43
      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: 43385
diff changeset
    44
      val instT = Term.map_atyps (perhaps (AList.lookup (op =) env))
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    45
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: 43385
diff changeset
    46
      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: 43385
diff changeset
    47
      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: 43385
diff changeset
    48
    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: 43385
diff changeset
    49
  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: 43385
diff changeset
    50
    []
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    51
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    52
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    53
(* collection of declarations *)
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    54
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    55
fun declared declss T = exists (exists (equal T o fst)) declss
43385
9cd4b4ecb4dd slightly more general treatment of mutually recursive datatypes;
boehmes
parents: 42361
diff changeset
    56
fun declared' dss T = exists (exists (equal T o fst) o snd) dss
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    57
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    58
fun get_decls T n Ts ctxt =
57226
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    59
  (case Ctr_Sugar.ctr_sugar_of ctxt n of
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    60
    SOME ctr_sugar => get_ctr_sugar_decl ctr_sugar T Ts ctxt
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    61
  | NONE =>
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    62
      (case Typedef.get_info ctxt n of
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    63
        [] => ([], ctxt)
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    64
      | info :: _ => (get_typedef_decl info T Ts, ctxt)))
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    65
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    66
fun add_decls T (declss, ctxt) =
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    67
  let
43385
9cd4b4ecb4dd slightly more general treatment of mutually recursive datatypes;
boehmes
parents: 42361
diff changeset
    68
    fun depends Ts ds = exists (member (op =) (map fst ds)) Ts
9cd4b4ecb4dd slightly more general treatment of mutually recursive datatypes;
boehmes
parents: 42361
diff changeset
    69
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    70
    fun add (TFree _) = I
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    71
      | add (TVar _) = I
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    72
      | add (T as Type (@{type_name fun}, _)) =
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    73
          fold add (Term.body_type T :: Term.binder_types T)
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    74
      | add @{typ bool} = I
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    75
      | add (T as Type (n, Ts)) = (fn (dss, ctxt1) =>
43385
9cd4b4ecb4dd slightly more general treatment of mutually recursive datatypes;
boehmes
parents: 42361
diff changeset
    76
          if declared declss T orelse declared' dss T then (dss, ctxt1)
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    77
          else if Old_SMT_Builtin.is_builtin_typ_ext ctxt1 T then (dss, ctxt1)
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    78
          else
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    79
            (case get_decls T n Ts ctxt1 of
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    80
              ([], _) => (dss, ctxt1)
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    81
            | (ds, ctxt2) =>
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    82
                let
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    83
                  val constrTs =
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    84
                    maps (map (snd o Term.dest_Const o fst) o snd) ds
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    85
                  val Us = fold (union (op =) o Term.binder_types) constrTs []
43385
9cd4b4ecb4dd slightly more general treatment of mutually recursive datatypes;
boehmes
parents: 42361
diff changeset
    86
9cd4b4ecb4dd slightly more general treatment of mutually recursive datatypes;
boehmes
parents: 42361
diff changeset
    87
                  fun ins [] = [(Us, ds)]
9cd4b4ecb4dd slightly more general treatment of mutually recursive datatypes;
boehmes
parents: 42361
diff changeset
    88
                    | ins ((Uds as (Us', _)) :: Udss) =
9cd4b4ecb4dd slightly more general treatment of mutually recursive datatypes;
boehmes
parents: 42361
diff changeset
    89
                        if depends Us' ds then (Us, ds) :: Uds :: Udss
9cd4b4ecb4dd slightly more general treatment of mutually recursive datatypes;
boehmes
parents: 42361
diff changeset
    90
                        else Uds :: ins Udss
9cd4b4ecb4dd slightly more general treatment of mutually recursive datatypes;
boehmes
parents: 42361
diff changeset
    91
            in fold add Us (ins dss, ctxt2) end))
9cd4b4ecb4dd slightly more general treatment of mutually recursive datatypes;
boehmes
parents: 42361
diff changeset
    92
  in add T ([], ctxt) |>> append declss o map snd end
9cd4b4ecb4dd slightly more general treatment of mutually recursive datatypes;
boehmes
parents: 42361
diff changeset
    93
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff changeset
    94
end