src/HOL/Tools/function_package/fundef_common.ML
author krauss
Fri Jun 01 15:57:45 2007 +0200 (2007-06-01)
changeset 23189 4574ab8f3b21
parent 22903 95ad1a91ecef
child 23203 a5026e73cfcf
permissions -rw-r--r--
simplified interfaces, some restructuring
krauss@19564
     1
(*  Title:      HOL/Tools/function_package/fundef_common.ML
krauss@19564
     2
    ID:         $Id$
krauss@19564
     3
    Author:     Alexander Krauss, TU Muenchen
krauss@19564
     4
krauss@19564
     5
A package for general recursive function definitions. 
krauss@19564
     6
Common type definitions and other infrastructure.
krauss@19564
     7
*)
krauss@19564
     8
krauss@19564
     9
structure FundefCommon =
krauss@19564
    10
struct
krauss@19564
    11
krauss@22498
    12
(* Profiling *)
krauss@21255
    13
val profile = ref false;
krauss@21255
    14
krauss@21255
    15
fun PROFILE msg = if !profile then timeap_msg msg else I
krauss@21255
    16
krauss@22498
    17
krauss@22498
    18
val acc_const_name = "Accessible_Part.acc"
krauss@20523
    19
fun mk_acc domT R =
krauss@22733
    20
    Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 
krauss@19564
    21
krauss@21319
    22
val function_name = suffix "C"
krauss@21319
    23
val graph_name = suffix "_graph"
krauss@21319
    24
val rel_name = suffix "_rel"
krauss@21319
    25
val dom_name = suffix "_dom"
krauss@21319
    26
krauss@19564
    27
type depgraph = int IntGraph.T
krauss@19564
    28
krauss@19564
    29
datatype ctx_tree 
krauss@19564
    30
  = Leaf of term
krauss@19564
    31
  | Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list)
krauss@19564
    32
  | RCall of (term * ctx_tree)
krauss@19564
    33
krauss@19564
    34
krauss@19564
    35
krauss@19583
    36
datatype fundef_result =
krauss@19583
    37
  FundefResult of
krauss@19564
    38
     {
krauss@22733
    39
      fs: term list,
krauss@20523
    40
      G: term,
krauss@20523
    41
      R: term,
krauss@19770
    42
krauss@20523
    43
      psimps : thm list, 
krauss@22166
    44
      trsimps : thm list option, 
krauss@22166
    45
krauss@19770
    46
      subset_pinducts : thm list, 
krauss@19770
    47
      simple_pinducts : thm list, 
krauss@19770
    48
      cases : thm,
krauss@19770
    49
      termination : thm,
krauss@22166
    50
      domintros : thm list option
krauss@19770
    51
     }
krauss@19770
    52
krauss@22733
    53
krauss@21255
    54
datatype fundef_context_data =
krauss@21255
    55
  FundefCtxData of
krauss@21255
    56
     {
krauss@22733
    57
      defname : string,
krauss@22733
    58
krauss@22166
    59
      add_simps : string -> Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
krauss@19770
    60
krauss@22733
    61
      fs : term list,
krauss@21255
    62
      R : term,
krauss@21255
    63
      
krauss@21255
    64
      psimps: thm list,
krauss@21255
    65
      pinducts: thm list,
krauss@21255
    66
      termination: thm
krauss@21255
    67
     }
krauss@21255
    68
krauss@22733
    69
fun morph_fundef_data phi (FundefCtxData {add_simps, fs, R, psimps, pinducts, termination, defname}) =
krauss@22623
    70
    let
krauss@22733
    71
      val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
krauss@22733
    72
      val name = Morphism.name phi
krauss@22623
    73
    in
krauss@22733
    74
      FundefCtxData { add_simps = add_simps (* contains no logical entities *), 
krauss@22733
    75
                      fs = map term fs, R = term R, psimps = fact psimps, 
krauss@22733
    76
                      pinducts = fact pinducts, termination = thm termination,
krauss@22733
    77
                      defname = name defname }
krauss@22623
    78
    end
krauss@22623
    79
krauss@20523
    80
structure FundefData = GenericDataFun
wenzelm@22846
    81
(
wenzelm@22846
    82
  type T = (term * fundef_context_data) NetRules.T;
haftmann@22760
    83
  val empty = NetRules.init
haftmann@22760
    84
    (op aconv o pairself fst : (term * fundef_context_data) * (term * fundef_context_data) -> bool)
haftmann@22760
    85
    fst;
krauss@19564
    86
  val copy = I;
krauss@19564
    87
  val extend = I;
krauss@22733
    88
  fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2)
wenzelm@22846
    89
);
krauss@19564
    90
krauss@19564
    91
krauss@19564
    92
structure FundefCongs = GenericDataFun
wenzelm@22846
    93
(
wenzelm@22846
    94
  type T = thm list
wenzelm@22846
    95
  val empty = []
wenzelm@22846
    96
  val extend = I
wenzelm@22846
    97
  fun merge _ = Drule.merge_rules
wenzelm@22846
    98
);
krauss@19564
    99
krauss@19564
   100
krauss@22733
   101
(* Generally useful?? *)
krauss@22733
   102
fun lift_morphism thy f = 
krauss@22733
   103
    let 
krauss@22733
   104
      val term = Drule.term_rule thy f
krauss@22733
   105
    in
krauss@22733
   106
      Morphism.thm_morphism f $> Morphism.term_morphism term $> Morphism.typ_morphism (Logic.type_map term)
krauss@22733
   107
    end
krauss@22733
   108
krauss@22733
   109
fun import_fundef_data t ctxt =
krauss@22733
   110
    let
krauss@22733
   111
      val thy = Context.theory_of ctxt
krauss@22733
   112
      val ct = cterm_of thy t
krauss@22733
   113
      val inst_morph = lift_morphism thy o Thm.instantiate 
krauss@19564
   114
krauss@22733
   115
      fun match data = 
wenzelm@22903
   116
          SOME (morph_fundef_data (inst_morph (Thm.match (cterm_of thy (fst data), ct))) (snd data))
krauss@22733
   117
          handle Pattern.MATCH => NONE
krauss@22733
   118
    in 
krauss@22733
   119
      get_first match (NetRules.retrieve (FundefData.get ctxt) t)
krauss@22733
   120
    end
krauss@19564
   121
krauss@22733
   122
fun import_last_fundef ctxt =
krauss@22733
   123
    case NetRules.rules (FundefData.get ctxt) of
krauss@22733
   124
      [] => NONE
krauss@22733
   125
    | (t, data) :: _ =>
krauss@22733
   126
      let 
krauss@22733
   127
        val ([t'], ctxt') = Variable.import_terms true [t] (Context.proof_of ctxt)
krauss@22733
   128
      in
krauss@22733
   129
        import_fundef_data t' (Context.Proof ctxt')
krauss@22733
   130
      end
krauss@19564
   131
krauss@22733
   132
val all_fundef_data = NetRules.rules o FundefData.get
krauss@21319
   133
krauss@19564
   134
val map_fundef_congs = FundefCongs.map 
krauss@19564
   135
val get_fundef_congs = FundefCongs.get
krauss@19564
   136
krauss@20654
   137
krauss@21319
   138
krauss@22733
   139
structure TerminationRule = GenericDataFun
wenzelm@22846
   140
(
wenzelm@22846
   141
  type T = thm list
wenzelm@22846
   142
  val empty = []
wenzelm@22846
   143
  val extend = I
wenzelm@22846
   144
  fun merge _ = Drule.merge_rules
wenzelm@22846
   145
);
krauss@21319
   146
krauss@22733
   147
val get_termination_rules = TerminationRule.get
krauss@22733
   148
val store_termination_rule = TerminationRule.map o cons
krauss@22733
   149
val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof
krauss@22733
   150
krauss@22733
   151
fun add_fundef_data (data as FundefCtxData {fs, termination, ...}) =
krauss@22733
   152
    FundefData.map (fold (fn f => NetRules.insert (f, data)) fs)
krauss@22733
   153
    #> store_termination_rule termination
krauss@21319
   154
krauss@21319
   155
krauss@21319
   156
krauss@20654
   157
(* Configuration management *)
krauss@20654
   158
datatype fundef_opt 
krauss@20654
   159
  = Sequential
krauss@20654
   160
  | Default of string
krauss@20654
   161
  | Preprocessor of string
krauss@21051
   162
  | Target of xstring
krauss@21319
   163
  | DomIntros
krauss@22166
   164
  | Tailrec
krauss@20654
   165
krauss@20654
   166
datatype fundef_config
krauss@20654
   167
  = FundefConfig of
krauss@20654
   168
   {
krauss@20654
   169
    sequential: bool,
krauss@20654
   170
    default: string,
krauss@21051
   171
    preprocessor: string option,
krauss@21319
   172
    target: xstring option,
krauss@22166
   173
    domintros: bool,
krauss@22166
   174
    tailrec: bool
krauss@20654
   175
   }
krauss@20654
   176
krauss@20654
   177
krauss@22166
   178
val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE,
krauss@22166
   179
                                    target=NONE, domintros=false, tailrec=false }
krauss@22166
   180
krauss@22166
   181
val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE, 
krauss@22166
   182
                                target=NONE, domintros=false, tailrec=false }
krauss@20654
   183
krauss@22166
   184
fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) = 
krauss@22166
   185
    FundefConfig {sequential=true, default=default, preprocessor=preprocessor, target=target, domintros=domintros, tailrec=tailrec }
krauss@22166
   186
  | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) = 
krauss@22166
   187
    FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor, target=target, domintros=domintros, tailrec=tailrec }
krauss@22166
   188
  | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) = 
krauss@22166
   189
    FundefConfig {sequential=sequential, default=default, preprocessor=SOME p, target=target, domintros=domintros, tailrec=tailrec }
krauss@22166
   190
  | apply_opt (Target t) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) =
krauss@22166
   191
    FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=SOME t, domintros=domintros, tailrec=tailrec }
krauss@22166
   192
  | apply_opt DomIntros (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) =
krauss@22166
   193
    FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=true,tailrec=tailrec }
krauss@22166
   194
  | apply_opt Tailrec (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) =
krauss@22166
   195
    FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=domintros,tailrec=true } 
krauss@20654
   196
krauss@22498
   197
fun target_of (FundefConfig {target, ...}) = target
krauss@21051
   198
krauss@22498
   199
local 
krauss@22498
   200
  structure P = OuterParse and K = OuterKeyword 
krauss@20654
   201
krauss@22498
   202
  val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
krauss@22498
   203
                       
krauss@22498
   204
  val option_parser = (P.$$$ "sequential" >> K Sequential)
krauss@22498
   205
                   || ((P.reserved "default" |-- P.term) >> Default)
krauss@22498
   206
                   || (P.reserved "domintros" >> K DomIntros)
krauss@22498
   207
                   || (P.reserved "tailrec" >> K Tailrec)
krauss@22498
   208
                   || ((P.$$$ "in" |-- P.xname) >> Target)
krauss@20654
   209
krauss@22498
   210
  fun config_parser def = (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 (P.group "option" option_parser)) --| P.$$$ ")") [])
krauss@21051
   211
                          >> (fn opts => fold apply_opt opts def)
krauss@22166
   212
krauss@22498
   213
  fun pipe_list1 s = P.enum1 "|" s
krauss@22498
   214
krauss@22498
   215
  val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
krauss@22498
   216
krauss@22498
   217
  fun pipe_error t = P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t])))
krauss@22498
   218
krauss@22498
   219
  val statement_ow = SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false)
krauss@22498
   220
                     --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("",""))
krauss@22498
   221
krauss@22498
   222
  val statements_ow = pipe_list1 statement_ow
krauss@22498
   223
in
krauss@22498
   224
  fun fundef_parser default_cfg = config_parser default_cfg -- P.fixes --| P.$$$ "where" -- statements_ow
krauss@20654
   225
end
krauss@20654
   226
krauss@23189
   227
krauss@23189
   228
krauss@23189
   229
(* Common operations on equations *)
krauss@23189
   230
krauss@23189
   231
fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b)
krauss@23189
   232
  | open_all_all t = ([], t)
krauss@23189
   233
krauss@23189
   234
exception MalformedEquation of term
krauss@23189
   235
krauss@23189
   236
fun split_def geq =
krauss@23189
   237
    let
krauss@23189
   238
      val (qs, imp) = open_all_all geq
krauss@23189
   239
krauss@23189
   240
      val gs = Logic.strip_imp_prems imp
krauss@23189
   241
      val eq = Logic.strip_imp_concl imp
krauss@23189
   242
krauss@23189
   243
      val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
krauss@23189
   244
          handle TERM _ => raise MalformedEquation geq
krauss@23189
   245
krauss@23189
   246
      val (head, args) = strip_comb f_args
krauss@23189
   247
krauss@23189
   248
      val fname = fst (dest_Free head)
krauss@23189
   249
          handle TERM _ => raise MalformedEquation geq
krauss@23189
   250
    in
krauss@23189
   251
      (fname, qs, gs, args, rhs)
krauss@23189
   252
    end
krauss@23189
   253
krauss@23189
   254
exception ArgumentCount of string
krauss@23189
   255
krauss@23189
   256
fun mk_arities fqgars =
krauss@23189
   257
    let fun f (fname, _, _, args, _) arities =
krauss@23189
   258
            let val k = length args
krauss@23189
   259
            in
krauss@23189
   260
              case Symtab.lookup arities fname of
krauss@23189
   261
                NONE => Symtab.update (fname, k) arities
krauss@23189
   262
              | SOME i => (if i = k then arities else raise ArgumentCount fname)
krauss@23189
   263
            end
krauss@23189
   264
    in
krauss@23189
   265
      fold f fqgars Symtab.empty
krauss@23189
   266
    end
krauss@23189
   267
krauss@23189
   268
krauss@23189
   269
krauss@23189
   270
krauss@23189
   271
krauss@19564
   272
end
krauss@19564
   273
krauss@19564
   274
(* Common Abbreviations *)
krauss@19564
   275
krauss@19564
   276
structure FundefAbbrev =
krauss@19564
   277
struct
krauss@19564
   278
krauss@19564
   279
fun implies_elim_swp x y = implies_elim y x
krauss@19564
   280
krauss@22498
   281
(* HOL abbreviations *)
krauss@19564
   282
val boolT = HOLogic.boolT
krauss@19564
   283
val mk_prod = HOLogic.mk_prod
krauss@19564
   284
val mk_eq = HOLogic.mk_eq
krauss@20523
   285
val eq_const = HOLogic.eq_const
krauss@19564
   286
val Trueprop = HOLogic.mk_Trueprop
krauss@19564
   287
val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT
krauss@19564
   288
krauss@19564
   289
fun free_to_var (Free (v,T)) = Var ((v,0),T)
krauss@19564
   290
  | free_to_var _ = raise Match
krauss@19564
   291
krauss@19564
   292
fun var_to_free (Var ((v,_),T)) = Free (v,T)
krauss@19564
   293
  | var_to_free _ = raise Match
krauss@19564
   294
krauss@19564
   295
krauss@19564
   296
end