src/HOL/Tools/BNF/Tools/bnf_fp_rec_sugar_util.ML
author blanchet
Mon Jan 20 18:24:56 2014 +0100 (2014-01-20)
changeset 55058 4e700eb471d4
parent 54979 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML@d7593bfccf25
permissions -rw-r--r--
moved BNF files to 'HOL'
blanchet@53303
     1
(*  Title:      HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
blanchet@53303
     2
    Author:     Lorenz Panny, TU Muenchen
blanchet@53303
     3
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@53303
     4
    Copyright   2013
blanchet@53303
     5
blanchet@53303
     6
Library for recursor and corecursor sugar.
blanchet@53303
     7
*)
blanchet@53303
     8
blanchet@53303
     9
signature BNF_FP_REC_SUGAR_UTIL =
blanchet@53303
    10
sig
blanchet@54246
    11
  val indexed: 'a list -> int -> int list * int
blanchet@54246
    12
  val indexedd: 'a list list -> int -> int list list * int
blanchet@54299
    13
  val indexeddd: 'a list list list -> int -> int list list list * int
blanchet@54246
    14
  val indexedddd: 'a list list list list -> int -> int list list list list * int
blanchet@54246
    15
  val find_index_eq: ''a list -> ''a -> int
blanchet@54246
    16
  val finds: ('a * 'b -> bool) -> 'a list -> 'b list -> ('a * 'b list) list * 'b list
blanchet@53303
    17
blanchet@54979
    18
  val drop_all: term -> term
blanchet@54202
    19
blanchet@54246
    20
  val mk_partial_compN: int -> typ -> term -> term
blanchet@54246
    21
  val mk_partial_comp: typ -> typ -> term -> term
blanchet@54246
    22
  val mk_compN: int -> typ list -> term * term -> term
blanchet@54246
    23
  val mk_comp: typ list -> term * term -> term
blanchet@53878
    24
blanchet@54246
    25
  val get_indices: ((binding * typ) * 'a) list -> term -> int list
blanchet@53303
    26
end;
blanchet@53303
    27
blanchet@53303
    28
structure BNF_FP_Rec_Sugar_Util : BNF_FP_REC_SUGAR_UTIL =
blanchet@53303
    29
struct
blanchet@53303
    30
blanchet@54614
    31
fun indexe _ h = (h, h + 1);
blanchet@54614
    32
fun indexed xs = fold_map indexe xs;
blanchet@53303
    33
fun indexedd xss = fold_map indexed xss;
blanchet@53303
    34
fun indexeddd xsss = fold_map indexedd xsss;
blanchet@53303
    35
fun indexedddd xssss = fold_map indexeddd xssss;
blanchet@53303
    36
blanchet@53303
    37
fun find_index_eq hs h = find_index (curry (op =) h) hs;
blanchet@53303
    38
blanchet@54246
    39
fun finds eq = fold_map (fn x => List.partition (curry eq x) #>> pair x);
blanchet@53303
    40
blanchet@54979
    41
fun drop_all t =
blanchet@54246
    42
  subst_bounds (strip_qnt_vars @{const_name all} t |> map Free |> rev,
blanchet@54246
    43
    strip_qnt_body @{const_name all} t);
blanchet@53303
    44
blanchet@54246
    45
fun mk_partial_comp gT fT g =
blanchet@54246
    46
  let val T = domain_type fT --> range_type gT in
blanchet@54246
    47
    Const (@{const_name Fun.comp}, gT --> fT --> T) $ g
blanchet@53303
    48
  end;
blanchet@53303
    49
blanchet@54246
    50
fun mk_partial_compN 0 _ g = g
blanchet@54246
    51
  | mk_partial_compN n fT g =
blanchet@54246
    52
    let val g' = mk_partial_compN (n - 1) (range_type fT) g in
blanchet@54246
    53
      mk_partial_comp (fastype_of g') fT g'
blanchet@54246
    54
    end;
blanchet@53303
    55
blanchet@54246
    56
fun mk_compN n bound_Ts (g, f) =
blanchet@54246
    57
  let val typof = curry fastype_of1 bound_Ts in
blanchet@54246
    58
    mk_partial_compN n (typof f) g $ f
blanchet@53303
    59
  end;
blanchet@53303
    60
blanchet@54246
    61
val mk_comp = mk_compN 1;
blanchet@54246
    62
blanchet@54246
    63
fun get_indices fixes t = map (fst #>> Binding.name_of #> Free) fixes
blanchet@54246
    64
  |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE)
blanchet@54246
    65
  |> map_filter I;
blanchet@54246
    66
blanchet@53303
    67
end;