'HOL/recdef' theory data;
authorwenzelm
Fri Apr 16 14:49:09 1999 +0200 (1999-04-16)
changeset 64397eea9f25dc49
parent 6438 e55a1869ed38
child 6440 7c59a55bae94
'HOL/recdef' theory data;
src/HOL/Tools/recdef_package.ML
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Fri Apr 16 14:49:06 1999 +0200
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Fri Apr 16 14:49:09 1999 +0200
     1.3 @@ -8,28 +8,71 @@
     1.4  signature RECDEF_PACKAGE =
     1.5  sig
     1.6    val quiet_mode: bool ref
     1.7 +  val print_recdefs: theory -> unit
     1.8 +  val get_recdef: theory -> string -> {rules: thm list, induct: thm, tcs: term list}
     1.9    val add_recdef: xstring -> string -> ((bstring * string) * Args.src list) list
    1.10      -> string option -> (xstring * Args.src list) list
    1.11      -> theory -> theory * {rules: thm list, induct: thm, tcs: term list}
    1.12    val add_recdef_i: xstring -> term -> ((bstring * term) * theory attribute list) list
    1.13      -> simpset option -> (thm * theory attribute list) list
    1.14      -> theory -> theory * {rules: thm list, induct: thm, tcs: term list}
    1.15 +  val setup: (theory -> theory) list
    1.16  end;
    1.17  
    1.18  structure RecdefPackage: RECDEF_PACKAGE =
    1.19  struct
    1.20  
    1.21 -
    1.22 -(* messages *)
    1.23 -
    1.24  val quiet_mode = Tfl.quiet_mode;
    1.25  val message = Tfl.message;
    1.26  
    1.27  
    1.28 -(* add_recdef(_i) *)
    1.29 +
    1.30 +(** theory data **)
    1.31 +
    1.32 +(* data kind 'HOL/recdef' *)
    1.33 +
    1.34 +type recdef_info = {rules: thm list, induct: thm, tcs: term list};
    1.35 +
    1.36 +structure RecdefArgs =
    1.37 +struct
    1.38 +  val name = "HOL/recdef";
    1.39 +  type T = recdef_info Symtab.table;
    1.40 +
    1.41 +  val empty = Symtab.empty;
    1.42 +  val prep_ext = I;
    1.43 +  val merge: T * T -> T = Symtab.merge (K true);
    1.44 +
    1.45 +  fun print sg tab =
    1.46 +    Pretty.writeln (Pretty.strs ("recdefs:" ::
    1.47 +      map (Sign.cond_extern sg Sign.constK o fst) (Symtab.dest tab)));
    1.48 +end;
    1.49 +
    1.50 +structure RecdefData = TheoryDataFun(RecdefArgs);
    1.51 +val print_recdefs = RecdefData.print;
    1.52  
    1.53 -fun gen_add_recdef tfl_def prep_att prep_ss app_thms name R eq_srcs raw_ss raw_congs thy =
    1.54 +
    1.55 +(* get and put data *)
    1.56 +
    1.57 +fun get_recdef thy name =
    1.58 +  (case Symtab.lookup (RecdefData.get thy, name) of
    1.59 +    Some info => info
    1.60 +  | None => error ("Unknown recursive function " ^ quote name));
    1.61 +
    1.62 +fun put_recdef name info thy =
    1.63    let
    1.64 +    val tab = Symtab.update_new ((name, info), RecdefData.get thy)
    1.65 +      handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name);
    1.66 +  in RecdefData.put tab thy end;
    1.67 +
    1.68 +
    1.69 +
    1.70 +(** add_recdef(_i) **)
    1.71 +
    1.72 +fun gen_add_recdef tfl_def prep_att prep_ss app_thms raw_name R eq_srcs raw_ss raw_congs thy =
    1.73 +  let
    1.74 +    val name = Sign.intern_const (Theory.sign_of thy) raw_name;
    1.75 +    val bname = Sign.base_name name;
    1.76 +
    1.77      val _ = message ("Defining recursive function " ^ quote name ^ " ...");
    1.78  
    1.79      val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
    1.80 @@ -40,9 +83,10 @@
    1.81      val (result as {rules, induct, tcs}) = Tfl.simplify_defn (ss, congs) (thy2, (name, pats));
    1.82      val thy3 =
    1.83        thy2
    1.84 -      |> Theory.add_path name
    1.85 +      |> Theory.add_path bname
    1.86        |> PureThy.add_thmss [(("rules", rules), [])]
    1.87        |> PureThy.add_thms ((("induct", induct), []) :: ((eq_names ~~ rules) ~~ eq_atts))
    1.88 +      |> put_recdef name result
    1.89        |> Theory.parent_path;
    1.90    in (thy3, result) end;
    1.91  
    1.92 @@ -52,6 +96,13 @@
    1.93  val add_recdef_i = gen_add_recdef Tfl.define_i (K I) I IsarThy.apply_theorems_i;
    1.94  
    1.95  
    1.96 +(** package setup **)
    1.97 +
    1.98 +(* setup theory *)
    1.99 +
   1.100 +val setup = [RecdefData.init];
   1.101 +
   1.102 +
   1.103  (* outer syntax *)
   1.104  
   1.105  local open OuterParse in
   1.106 @@ -63,7 +114,7 @@
   1.107    >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef f R (map triple_swap eqs) ss congs);
   1.108  
   1.109  val recdefP =
   1.110 -  OuterSyntax.command "recdef" "general recursive function definition (TFL)"
   1.111 +  OuterSyntax.command "recdef" "define general recursive functions (TFL)"
   1.112      (recdef_decl >> Toplevel.theory);
   1.113  
   1.114  val _ = OuterSyntax.add_keywords ["congs", "simpset"];