src/HOL/Tools/recdef_package.ML
author wenzelm
Mon May 24 21:57:13 1999 +0200 (1999-05-24)
changeset 6723 f342449d73ca
parent 6576 7e0b35bed503
child 6729 b6e167580a32
permissions -rw-r--r--
outer syntax keyword classification;
no open OuterParse;
wenzelm@6429
     1
(*  Title:      HOL/Tools/recdef_package.ML
wenzelm@6429
     2
    ID:         $Id$
wenzelm@6429
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6429
     4
wenzelm@6429
     5
Wrapper module for Konrad Slind's TFL package.
wenzelm@6429
     6
*)
wenzelm@6429
     7
wenzelm@6429
     8
signature RECDEF_PACKAGE =
wenzelm@6429
     9
sig
wenzelm@6429
    10
  val quiet_mode: bool ref
wenzelm@6439
    11
  val print_recdefs: theory -> unit
wenzelm@6439
    12
  val get_recdef: theory -> string -> {rules: thm list, induct: thm, tcs: term list}
wenzelm@6576
    13
  val add_recdef: xstring -> string -> string list -> simpset option
wenzelm@6576
    14
    -> (xstring * Args.src list) list -> theory
wenzelm@6576
    15
    -> theory * {rules: thm list, induct: thm, tcs: term list}
wenzelm@6576
    16
  val add_recdef_i: xstring -> term -> term list -> simpset option
wenzelm@6576
    17
    -> (thm * theory attribute list) list
wenzelm@6429
    18
    -> theory -> theory * {rules: thm list, induct: thm, tcs: term list}
wenzelm@6557
    19
  val defer_recdef: xstring -> string list -> (xstring * Args.src list) list
wenzelm@6557
    20
    -> theory -> theory * {induct_rules: thm}
wenzelm@6557
    21
  val defer_recdef_i: xstring -> term list -> (thm * theory attribute list) list
wenzelm@6557
    22
    -> theory -> theory * {induct_rules: thm}
wenzelm@6439
    23
  val setup: (theory -> theory) list
wenzelm@6429
    24
end;
wenzelm@6429
    25
wenzelm@6429
    26
structure RecdefPackage: RECDEF_PACKAGE =
wenzelm@6429
    27
struct
wenzelm@6429
    28
wenzelm@6429
    29
val quiet_mode = Tfl.quiet_mode;
wenzelm@6429
    30
val message = Tfl.message;
wenzelm@6429
    31
wenzelm@6429
    32
wenzelm@6439
    33
wenzelm@6439
    34
(** theory data **)
wenzelm@6439
    35
wenzelm@6439
    36
(* data kind 'HOL/recdef' *)
wenzelm@6439
    37
wenzelm@6439
    38
type recdef_info = {rules: thm list, induct: thm, tcs: term list};
wenzelm@6439
    39
wenzelm@6439
    40
structure RecdefArgs =
wenzelm@6439
    41
struct
wenzelm@6439
    42
  val name = "HOL/recdef";
wenzelm@6439
    43
  type T = recdef_info Symtab.table;
wenzelm@6439
    44
wenzelm@6439
    45
  val empty = Symtab.empty;
wenzelm@6557
    46
  val copy = I;
wenzelm@6439
    47
  val prep_ext = I;
wenzelm@6439
    48
  val merge: T * T -> T = Symtab.merge (K true);
wenzelm@6439
    49
wenzelm@6439
    50
  fun print sg tab =
wenzelm@6439
    51
    Pretty.writeln (Pretty.strs ("recdefs:" ::
wenzelm@6439
    52
      map (Sign.cond_extern sg Sign.constK o fst) (Symtab.dest tab)));
wenzelm@6439
    53
end;
wenzelm@6439
    54
wenzelm@6439
    55
structure RecdefData = TheoryDataFun(RecdefArgs);
wenzelm@6439
    56
val print_recdefs = RecdefData.print;
wenzelm@6429
    57
wenzelm@6439
    58
wenzelm@6439
    59
(* get and put data *)
wenzelm@6439
    60
wenzelm@6439
    61
fun get_recdef thy name =
wenzelm@6439
    62
  (case Symtab.lookup (RecdefData.get thy, name) of
wenzelm@6439
    63
    Some info => info
wenzelm@6439
    64
  | None => error ("Unknown recursive function " ^ quote name));
wenzelm@6439
    65
wenzelm@6439
    66
fun put_recdef name info thy =
wenzelm@6429
    67
  let
wenzelm@6439
    68
    val tab = Symtab.update_new ((name, info), RecdefData.get thy)
wenzelm@6439
    69
      handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name);
wenzelm@6439
    70
  in RecdefData.put tab thy end;
wenzelm@6439
    71
wenzelm@6439
    72
wenzelm@6439
    73
wenzelm@6439
    74
(** add_recdef(_i) **)
wenzelm@6439
    75
wenzelm@6557
    76
fun requires_recdef thy = Theory.requires thy "Recdef" "recursive functions";
wenzelm@6557
    77
wenzelm@6576
    78
fun gen_add_recdef tfl_fn prep_ss app_thms raw_name R eqs raw_ss raw_congs thy =
wenzelm@6439
    79
  let
wenzelm@6439
    80
    val name = Sign.intern_const (Theory.sign_of thy) raw_name;
wenzelm@6439
    81
    val bname = Sign.base_name name;
wenzelm@6439
    82
wenzelm@6557
    83
    val _ = requires_recdef thy;
wenzelm@6429
    84
    val _ = message ("Defining recursive function " ^ quote name ^ " ...");
wenzelm@6429
    85
wenzelm@6429
    86
    val ss = (case raw_ss of None => Simplifier.simpset_of thy | Some x => prep_ss x);
wenzelm@6429
    87
    val (thy1, congs) = thy |> app_thms raw_congs;
wenzelm@6557
    88
    val (thy2, pats) = tfl_fn thy1 name R eqs;
wenzelm@6429
    89
    val (result as {rules, induct, tcs}) = Tfl.simplify_defn (ss, congs) (thy2, (name, pats));
wenzelm@6429
    90
    val thy3 =
wenzelm@6429
    91
      thy2
wenzelm@6439
    92
      |> Theory.add_path bname
wenzelm@6429
    93
      |> PureThy.add_thmss [(("rules", rules), [])]
wenzelm@6576
    94
      |> PureThy.add_thms [(("induct", induct), [])]
wenzelm@6439
    95
      |> put_recdef name result
wenzelm@6429
    96
      |> Theory.parent_path;
wenzelm@6429
    97
  in (thy3, result) end;
wenzelm@6429
    98
wenzelm@6576
    99
val add_recdef = gen_add_recdef Tfl.define I IsarThy.apply_theorems;
wenzelm@6576
   100
val add_recdef_x = gen_add_recdef Tfl.define (Simplifier.simpset_of o ThyInfo.get_theory)
wenzelm@6576
   101
  IsarThy.apply_theorems;
wenzelm@6576
   102
val add_recdef_i = gen_add_recdef Tfl.define_i I IsarThy.apply_theorems_i;
wenzelm@6429
   103
wenzelm@6429
   104
wenzelm@6557
   105
wenzelm@6557
   106
(** defer_recdef(_i) **)
wenzelm@6557
   107
wenzelm@6557
   108
fun gen_defer_recdef tfl_fn app_thms raw_name eqs raw_congs thy =
wenzelm@6557
   109
  let
wenzelm@6557
   110
    val name = Sign.intern_const (Theory.sign_of thy) raw_name;
wenzelm@6557
   111
    val bname = Sign.base_name name;
wenzelm@6557
   112
wenzelm@6557
   113
    val _ = requires_recdef thy;
wenzelm@6557
   114
    val _ = message ("Deferred recursive function " ^ quote name ^ " ...");
wenzelm@6557
   115
wenzelm@6557
   116
    val (thy1, congs) = thy |> app_thms raw_congs;
wenzelm@6557
   117
    val (thy2, induct_rules) = tfl_fn thy1 name congs eqs;
wenzelm@6557
   118
    val thy3 =
wenzelm@6557
   119
      thy2
wenzelm@6557
   120
      |> Theory.add_path bname
wenzelm@6557
   121
      |> PureThy.add_thms [(("induct_rules", induct_rules), [])]
wenzelm@6557
   122
      |> Theory.parent_path;
wenzelm@6557
   123
  in (thy3, {induct_rules = induct_rules}) end;
wenzelm@6557
   124
wenzelm@6557
   125
val defer_recdef = gen_defer_recdef Tfl.defer IsarThy.apply_theorems;
wenzelm@6557
   126
val defer_recdef_i = gen_defer_recdef Tfl.defer_i IsarThy.apply_theorems_i;
wenzelm@6557
   127
wenzelm@6557
   128
wenzelm@6557
   129
wenzelm@6439
   130
(** package setup **)
wenzelm@6439
   131
wenzelm@6439
   132
(* setup theory *)
wenzelm@6439
   133
wenzelm@6439
   134
val setup = [RecdefData.init];
wenzelm@6439
   135
wenzelm@6439
   136
wenzelm@6429
   137
(* outer syntax *)
wenzelm@6429
   138
wenzelm@6723
   139
local structure P = OuterParse and K = OuterSyntax.Keyword in
wenzelm@6429
   140
wenzelm@6429
   141
val recdef_decl =
wenzelm@6723
   142
  P.name -- P.term -- Scan.repeat1 P.term --
wenzelm@6723
   143
  Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) [] --
wenzelm@6723
   144
  Scan.option (P.$$$ "(" |-- P.$$$ "simpset" |-- P.!!! (P.name --| P.$$$ ")"))
wenzelm@6576
   145
  >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef_x f R eqs ss congs);
wenzelm@6429
   146
wenzelm@6429
   147
val recdefP =
wenzelm@6723
   148
  OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl
wenzelm@6429
   149
    (recdef_decl >> Toplevel.theory);
wenzelm@6429
   150
wenzelm@6557
   151
wenzelm@6557
   152
val defer_recdef_decl =
wenzelm@6723
   153
  P.name -- Scan.repeat1 P.term --
wenzelm@6723
   154
  Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) []
wenzelm@6557
   155
  >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
wenzelm@6557
   156
wenzelm@6557
   157
val defer_recdefP =
wenzelm@6723
   158
  OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl
wenzelm@6557
   159
    (defer_recdef_decl >> Toplevel.theory);
wenzelm@6557
   160
wenzelm@6429
   161
val _ = OuterSyntax.add_keywords ["congs", "simpset"];
wenzelm@6557
   162
val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP];
wenzelm@6429
   163
wenzelm@6429
   164
end;
wenzelm@6429
   165
wenzelm@6429
   166
wenzelm@6429
   167
end;