src/HOL/Tools/Function/function_common.ML
author wenzelm
Sat Mar 22 18:19:57 2014 +0100 (2014-03-22)
changeset 56254 a2dd9200854d
parent 56245 84fc7dfa3cd4
child 57959 1bfed12a7646
permissions -rw-r--r--
more antiquotations;
krauss@34232
     1
(*  Title:      HOL/Tools/Function/function_common.ML
krauss@33099
     2
    Author:     Alexander Krauss, TU Muenchen
krauss@33099
     3
krauss@41114
     4
Common definitions and other infrastructure for the function package.
krauss@33099
     5
*)
krauss@33099
     6
krauss@34230
     7
signature FUNCTION_DATA =
krauss@34230
     8
sig
krauss@34230
     9
krauss@34230
    10
type info =
krauss@34230
    11
 {is_partial : bool,
krauss@34230
    12
  defname : string,
krauss@34230
    13
    (* contains no logical entities: invariant under morphisms: *)
krauss@34230
    14
  add_simps : (binding -> binding) -> string -> (binding -> binding) ->
krauss@34230
    15
    Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
Manuel@53603
    16
  fnames : string list,
krauss@34230
    17
  case_names : string list,
krauss@34230
    18
  fs : term list,
krauss@34230
    19
  R : term,
krauss@52384
    20
  dom: term,
krauss@34230
    21
  psimps: thm list,
krauss@34230
    22
  pinducts: thm list,
krauss@34231
    23
  simps : thm list option,
krauss@34231
    24
  inducts : thm list option,
krauss@52383
    25
  termination : thm,
Manuel@53603
    26
  cases : thm list,
Manuel@53603
    27
  pelims: thm list list,
Manuel@53603
    28
  elims: thm list list option}
krauss@34230
    29
krauss@34230
    30
end
krauss@34230
    31
krauss@34230
    32
structure Function_Data : FUNCTION_DATA =
krauss@34230
    33
struct
krauss@34230
    34
krauss@34230
    35
type info =
krauss@34230
    36
 {is_partial : bool,
krauss@34230
    37
  defname : string,
krauss@34230
    38
    (* contains no logical entities: invariant under morphisms: *)
krauss@34230
    39
  add_simps : (binding -> binding) -> string -> (binding -> binding) ->
krauss@34230
    40
    Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
Manuel@53603
    41
  fnames : string list,
krauss@34230
    42
  case_names : string list,
krauss@34230
    43
  fs : term list,
krauss@34230
    44
  R : term,
krauss@52384
    45
  dom: term,
krauss@34230
    46
  psimps: thm list,
krauss@34230
    47
  pinducts: thm list,
krauss@34231
    48
  simps : thm list option,
krauss@34231
    49
  inducts : thm list option,
krauss@52383
    50
  termination : thm,
Manuel@53603
    51
  cases : thm list,
Manuel@53603
    52
  pelims : thm list list,
Manuel@53603
    53
  elims : thm list list option}
krauss@34230
    54
krauss@34230
    55
end
krauss@34230
    56
wenzelm@49965
    57
signature FUNCTION_COMMON =
wenzelm@49965
    58
sig
wenzelm@49965
    59
  include FUNCTION_DATA
wenzelm@49965
    60
  val profile : bool Unsynchronized.ref
wenzelm@49965
    61
  val PROFILE : string -> ('a -> 'b) -> 'a -> 'b
wenzelm@49965
    62
  val mk_acc : typ -> term -> term
wenzelm@49965
    63
  val function_name : string -> string
wenzelm@49965
    64
  val graph_name : string -> string
wenzelm@49965
    65
  val rel_name : string -> string
wenzelm@49965
    66
  val dom_name : string -> string
wenzelm@49965
    67
  val apply_termination_rule : Proof.context -> int -> tactic
wenzelm@49965
    68
  datatype function_result = FunctionResult of
wenzelm@49965
    69
   {fs: term list,
wenzelm@49965
    70
    G: term,
wenzelm@49965
    71
    R: term,
krauss@52384
    72
    dom: term,
wenzelm@49965
    73
    psimps : thm list,
wenzelm@49965
    74
    simple_pinducts : thm list,
Manuel@53603
    75
    cases : thm list,
Manuel@53603
    76
    pelims : thm list list,
wenzelm@49965
    77
    termination : thm,
wenzelm@49965
    78
    domintros : thm list option}
wenzelm@49965
    79
  val transform_function_data : info -> morphism -> info
wenzelm@49965
    80
  val get_function : Proof.context -> (term * info) Item_Net.T
wenzelm@49965
    81
  val import_function_data : term -> Proof.context -> info option
wenzelm@49965
    82
  val import_last_function : Proof.context -> info option
wenzelm@49965
    83
  val add_function_data : info -> Context.generic -> Context.generic
wenzelm@49965
    84
  structure Termination_Simps: NAMED_THMS
wenzelm@49965
    85
  val set_termination_prover : (Proof.context -> tactic) -> Context.generic -> Context.generic
wenzelm@49965
    86
  val get_termination_prover : Proof.context -> tactic
urbanc@49979
    87
  val store_termination_rule : thm -> Context.generic -> Context.generic
wenzelm@49965
    88
  datatype function_config = FunctionConfig of
wenzelm@49965
    89
   {sequential: bool,
wenzelm@49965
    90
    default: string option,
wenzelm@49965
    91
    domintros: bool,
wenzelm@49965
    92
    partials: bool}
wenzelm@49965
    93
  val default_config : function_config
wenzelm@49965
    94
  val split_def : Proof.context -> (string -> 'a) -> term ->
wenzelm@49965
    95
    string * (string * typ) list * term list * term list * term
wenzelm@49965
    96
  val check_defs : Proof.context -> ((string * typ) * 'a) list -> term list -> unit
wenzelm@49965
    97
  type fixes = ((string * typ) * mixfix) list
wenzelm@49965
    98
  type 'a spec = (Attrib.binding * 'a list) list
wenzelm@49965
    99
  type preproc = function_config -> Proof.context -> fixes -> term spec ->
wenzelm@49965
   100
    (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
wenzelm@49965
   101
  val fname_of : term -> string
wenzelm@49965
   102
  val mk_case_names : int -> string -> int -> string list
wenzelm@49965
   103
  val empty_preproc : (Proof.context -> ((string * typ) * mixfix) list -> term list -> 'c) -> preproc
wenzelm@49965
   104
  val get_preproc: Proof.context -> preproc
wenzelm@49965
   105
  val set_preproc: preproc -> Context.generic -> Context.generic
wenzelm@49965
   106
  val function_parser : function_config ->
wenzelm@49965
   107
    ((function_config * (binding * string option * mixfix) list) * (Attrib.binding * string) list) parser
wenzelm@49965
   108
end
wenzelm@49965
   109
wenzelm@49965
   110
structure Function_Common : FUNCTION_COMMON =
krauss@33099
   111
struct
krauss@33099
   112
krauss@34230
   113
open Function_Data
krauss@34230
   114
krauss@33099
   115
local open Function_Lib in
krauss@33099
   116
krauss@33099
   117
(* Profiling *)
krauss@33099
   118
val profile = Unsynchronized.ref false;
krauss@33099
   119
krauss@33099
   120
fun PROFILE msg = if !profile then timeap_msg msg else I
krauss@33099
   121
haftmann@54295
   122
val acc_const_name = @{const_name Wellfounded.accp}
krauss@33099
   123
fun mk_acc domT R =
krauss@34232
   124
  Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 
krauss@33099
   125
krauss@33099
   126
val function_name = suffix "C"
krauss@33099
   127
val graph_name = suffix "_graph"
krauss@33099
   128
val rel_name = suffix "_rel"
krauss@33099
   129
val dom_name = suffix "_dom"
krauss@33099
   130
krauss@33099
   131
(* Termination rules *)
krauss@33099
   132
wenzelm@46042
   133
(* FIXME just one data slot (record) per program unit *)
wenzelm@33519
   134
structure TerminationRule = Generic_Data
krauss@33099
   135
(
krauss@33099
   136
  type T = thm list
krauss@33099
   137
  val empty = []
krauss@33099
   138
  val extend = I
wenzelm@33519
   139
  val merge = Thm.merge_thms
krauss@33099
   140
);
krauss@33099
   141
krauss@33099
   142
val get_termination_rules = TerminationRule.get
krauss@33099
   143
val store_termination_rule = TerminationRule.map o cons
krauss@33099
   144
val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof
krauss@33099
   145
krauss@33099
   146
krauss@33099
   147
(* Function definition result data *)
krauss@33099
   148
krauss@34232
   149
datatype function_result = FunctionResult of
krauss@34232
   150
 {fs: term list,
krauss@34232
   151
  G: term,
krauss@34232
   152
  R: term,
krauss@52384
   153
  dom: term,
krauss@34232
   154
  psimps : thm list,
krauss@34232
   155
  simple_pinducts : thm list,
Manuel@53603
   156
  cases : thm list,
Manuel@53603
   157
  pelims : thm list list,
krauss@34232
   158
  termination : thm,
krauss@34232
   159
  domintros : thm list option}
krauss@33099
   160
Manuel@53603
   161
fun transform_function_data ({add_simps, case_names, fnames, fs, R, dom, psimps, pinducts,
Manuel@53603
   162
  simps, inducts, termination, defname, is_partial, cases, pelims, elims} : info) phi =
krauss@33099
   163
    let
wenzelm@45290
   164
      val term = Morphism.term phi
wenzelm@45290
   165
      val thm = Morphism.thm phi
wenzelm@45290
   166
      val fact = Morphism.fact phi
krauss@33099
   167
      val name = Binding.name_of o Morphism.binding phi o Binding.name
krauss@33099
   168
    in
Manuel@53603
   169
      { add_simps = add_simps, case_names = case_names, fnames = fnames,
krauss@52384
   170
        fs = map term fs, R = term R, dom = term dom, psimps = fact psimps,
krauss@34231
   171
        pinducts = fact pinducts, simps = Option.map fact simps,
krauss@34231
   172
        inducts = Option.map fact inducts, termination = thm termination,
Manuel@53603
   173
        defname = name defname, is_partial=is_partial, cases = fact cases,
Manuel@53603
   174
        elims = Option.map (map fact) elims, pelims = map fact pelims }
krauss@33099
   175
    end
krauss@33099
   176
wenzelm@46042
   177
(* FIXME just one data slot (record) per program unit *)
wenzelm@33519
   178
structure FunctionData = Generic_Data
krauss@33099
   179
(
krauss@34230
   180
  type T = (term * info) Item_Net.T;
wenzelm@33373
   181
  val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
krauss@33099
   182
  val extend = I;
wenzelm@33519
   183
  fun merge tabs : T = Item_Net.merge tabs;
krauss@34232
   184
)
krauss@33099
   185
krauss@33099
   186
val get_function = FunctionData.get o Context.Proof;
krauss@33099
   187
krauss@34232
   188
fun lift_morphism thy f =
krauss@34232
   189
  let
wenzelm@46496
   190
    fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of thy t))
krauss@34232
   191
  in
wenzelm@54740
   192
    Morphism.morphism "lift_morphism"
wenzelm@54740
   193
      {binding = [],
wenzelm@54740
   194
       typ = [Logic.type_map term],
wenzelm@54740
   195
       term = [term],
wenzelm@54740
   196
       fact = [map f]}
krauss@34232
   197
  end
krauss@33099
   198
krauss@33099
   199
fun import_function_data t ctxt =
krauss@34232
   200
  let
wenzelm@42361
   201
    val thy = Proof_Context.theory_of ctxt
krauss@34232
   202
    val ct = cterm_of thy t
krauss@34232
   203
    val inst_morph = lift_morphism thy o Thm.instantiate
krauss@33099
   204
krauss@34232
   205
    fun match (trm, data) =
wenzelm@45290
   206
      SOME (transform_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
krauss@34232
   207
      handle Pattern.MATCH => NONE
krauss@34232
   208
  in
krauss@34232
   209
    get_first match (Item_Net.retrieve (get_function ctxt) t)
krauss@34232
   210
  end
krauss@33099
   211
krauss@33099
   212
fun import_last_function ctxt =
krauss@34232
   213
  case Item_Net.content (get_function ctxt) of
krauss@34232
   214
    [] => NONE
wenzelm@49966
   215
  | (t, _) :: _ =>
krauss@34232
   216
    let
krauss@34232
   217
      val ([t'], ctxt') = Variable.import_terms true [t] ctxt
krauss@34232
   218
    in
krauss@34232
   219
      import_function_data t' ctxt'
krauss@34232
   220
    end
krauss@33099
   221
krauss@34230
   222
fun add_function_data (data : info as {fs, termination, ...}) =
krauss@34232
   223
  FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs)
krauss@34232
   224
  #> store_termination_rule termination
krauss@33099
   225
krauss@33099
   226
krauss@33099
   227
(* Simp rules for termination proofs *)
krauss@33099
   228
krauss@33099
   229
structure Termination_Simps = Named_Thms
krauss@33099
   230
(
wenzelm@45294
   231
  val name = @{binding termination_simp}
wenzelm@38764
   232
  val description = "simplification rules for termination proofs"
krauss@34232
   233
)
krauss@33099
   234
krauss@33099
   235
krauss@33099
   236
(* Default Termination Prover *)
krauss@33099
   237
wenzelm@46042
   238
(* FIXME just one data slot (record) per program unit *)
wenzelm@33519
   239
structure TerminationProver = Generic_Data
krauss@33099
   240
(
krauss@36521
   241
  type T = Proof.context -> tactic
krauss@33099
   242
  val empty = (fn _ => error "Termination prover not configured")
krauss@33099
   243
  val extend = I
wenzelm@38761
   244
  fun merge (a, _) = a
krauss@34232
   245
)
krauss@33099
   246
krauss@33099
   247
val set_termination_prover = TerminationProver.put
wenzelm@49965
   248
fun get_termination_prover ctxt = TerminationProver.get (Context.Proof ctxt) ctxt
krauss@33099
   249
krauss@33099
   250
krauss@33099
   251
(* Configuration management *)
krauss@34232
   252
datatype function_opt
krauss@33099
   253
  = Sequential
krauss@33099
   254
  | Default of string
krauss@33099
   255
  | DomIntros
krauss@33101
   256
  | No_Partials
krauss@33099
   257
krauss@34232
   258
datatype function_config = FunctionConfig of
krauss@34232
   259
 {sequential: bool,
krauss@41417
   260
  default: string option,
krauss@34232
   261
  domintros: bool,
krauss@41846
   262
  partials: bool}
krauss@33099
   263
krauss@41846
   264
fun apply_opt Sequential (FunctionConfig {sequential, default, domintros, partials}) =
krauss@41846
   265
    FunctionConfig {sequential=true, default=default, domintros=domintros, partials=partials}
krauss@41846
   266
  | apply_opt (Default d) (FunctionConfig {sequential, default, domintros, partials}) =
krauss@41846
   267
    FunctionConfig {sequential=sequential, default=SOME d, domintros=domintros, partials=partials}
krauss@41846
   268
  | apply_opt DomIntros (FunctionConfig {sequential, default, domintros, partials}) =
krauss@41846
   269
    FunctionConfig {sequential=sequential, default=default, domintros=true, partials=partials}
krauss@41846
   270
  | apply_opt No_Partials (FunctionConfig {sequential, default, domintros, partials}) =
krauss@41846
   271
    FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=false}
krauss@33099
   272
krauss@33099
   273
val default_config =
krauss@41417
   274
  FunctionConfig { sequential=false, default=NONE,
krauss@41846
   275
    domintros=false, partials=true}
krauss@33099
   276
krauss@33099
   277
krauss@33099
   278
(* Analyzing function equations *)
krauss@33099
   279
krauss@39276
   280
fun split_def ctxt check_head geq =
krauss@34232
   281
  let
krauss@34232
   282
    fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
wenzelm@56245
   283
    val qs = Term.strip_qnt_vars @{const_name Pure.all} geq
wenzelm@56245
   284
    val imp = Term.strip_qnt_body @{const_name Pure.all} geq
krauss@34232
   285
    val (gs, eq) = Logic.strip_horn imp
krauss@33099
   286
krauss@34232
   287
    val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
krauss@34232
   288
      handle TERM _ => error (input_error "Not an equation")
krauss@33099
   289
krauss@34232
   290
    val (head, args) = strip_comb f_args
krauss@33099
   291
krauss@39276
   292
    val fname = fst (dest_Free head) handle TERM _ => ""
krauss@39276
   293
    val _ = check_head fname
krauss@34232
   294
  in
krauss@34232
   295
    (fname, qs, gs, args, rhs)
krauss@34232
   296
  end
krauss@33099
   297
krauss@33099
   298
(* Check for all sorts of errors in the input *)
krauss@33099
   299
fun check_defs ctxt fixes eqs =
krauss@34232
   300
  let
krauss@34232
   301
    val fnames = map (fst o fst) fixes
krauss@34232
   302
krauss@34232
   303
    fun check geq =
krauss@34232
   304
      let
krauss@34232
   305
        fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq])
krauss@33099
   306
krauss@39276
   307
        fun check_head fname =
krauss@39276
   308
          member (op =) fnames fname orelse
krauss@39276
   309
          input_error ("Illegal equation head. Expected " ^ commas_quote fnames)
krauss@34232
   310
krauss@39276
   311
        val (fname, qs, gs, args, rhs) = split_def ctxt check_head geq
krauss@34232
   312
krauss@34232
   313
        val _ = length args > 0 orelse input_error "Function has no arguments:"
krauss@34232
   314
krauss@34232
   315
        fun add_bvs t is = add_loose_bnos (t, 0, is)
wenzelm@42081
   316
        val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs []))
wenzelm@42081
   317
                    |> map (fst o nth (rev qs))
krauss@34232
   318
krauss@34232
   319
        val _ = null rvs orelse input_error
krauss@34232
   320
          ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs ^
krauss@34232
   321
           " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
krauss@34232
   322
krauss@34232
   323
        val _ = forall (not o Term.exists_subterm
haftmann@36692
   324
          (fn Free (n, _) => member (op =) fnames n | _ => false)) (gs @ args)
krauss@34232
   325
          orelse input_error "Defined function may not occur in premises or arguments"
krauss@33099
   326
krauss@34232
   327
        val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
krauss@34232
   328
        val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
krauss@34232
   329
        val _ = null funvars orelse (warning (cat_lines
krauss@34232
   330
          ["Bound variable" ^ plural " " "s " funvars ^
krauss@34232
   331
          commas_quote (map fst funvars) ^ " occur" ^ plural "s" "" funvars ^
krauss@34232
   332
          " in function position.", "Misspelled constructor???"]); true)
krauss@34232
   333
      in
krauss@34232
   334
        (fname, length args)
krauss@34232
   335
      end
krauss@33099
   336
krauss@34232
   337
    val grouped_args = AList.group (op =) (map check eqs)
krauss@34232
   338
    val _ = grouped_args
krauss@34232
   339
      |> map (fn (fname, ars) =>
krauss@34232
   340
        length (distinct (op =) ars) = 1
krauss@34232
   341
        orelse error ("Function " ^ quote fname ^
krauss@34232
   342
          " has different numbers of arguments in different equations"))
krauss@33099
   343
krauss@34232
   344
    val not_defined = subtract (op =) (map fst grouped_args) fnames
krauss@34232
   345
    val _ = null not_defined
krauss@34232
   346
      orelse error ("No defining equations for function" ^
krauss@34232
   347
        plural " " "s " not_defined ^ commas_quote not_defined)
krauss@33751
   348
krauss@34232
   349
    fun check_sorts ((fname, fT), _) =
wenzelm@56254
   350
      Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, @{sort type})
krauss@34232
   351
      orelse error (cat_lines
krauss@34232
   352
      ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
wenzelm@39134
   353
       Syntax.string_of_typ (Config.put show_sorts true ctxt) fT])
krauss@33099
   354
krauss@34232
   355
    val _ = map check_sorts fixes
krauss@34232
   356
  in
krauss@34232
   357
    ()
krauss@34232
   358
  end
krauss@33099
   359
krauss@33099
   360
(* Preprocessors *)
krauss@33099
   361
krauss@33099
   362
type fixes = ((string * typ) * mixfix) list
krauss@33099
   363
type 'a spec = (Attrib.binding * 'a list) list
krauss@34232
   364
type preproc = function_config -> Proof.context -> fixes -> term spec ->
krauss@34232
   365
  (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
krauss@33099
   366
krauss@34232
   367
val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o
krauss@34232
   368
  HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all
krauss@33099
   369
krauss@33099
   370
fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k
krauss@33099
   371
  | mk_case_names _ n 0 = []
krauss@33099
   372
  | mk_case_names _ n 1 = [n]
krauss@33099
   373
  | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k)
krauss@33099
   374
wenzelm@49965
   375
fun empty_preproc check (_: function_config) (ctxt: Proof.context) (fixes: fixes) spec =
krauss@34232
   376
  let
krauss@34232
   377
    val (bnds, tss) = split_list spec
krauss@34232
   378
    val ts = flat tss
krauss@34232
   379
    val _ = check ctxt fixes ts
krauss@34232
   380
    val fnames = map (fst o fst) fixes
krauss@34232
   381
    val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts
krauss@33099
   382
krauss@34232
   383
    fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) 
krauss@34232
   384
      (indices ~~ xs) |> map (map snd)
krauss@33099
   385
krauss@34232
   386
    (* using theorem names for case name currently disabled *)
krauss@34232
   387
    val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat
krauss@34232
   388
  in
krauss@34232
   389
    (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)
krauss@34232
   390
  end
krauss@33099
   391
wenzelm@46042
   392
(* FIXME just one data slot (record) per program unit *)
wenzelm@33519
   393
structure Preprocessor = Generic_Data
krauss@33099
   394
(
krauss@33099
   395
  type T = preproc
krauss@33099
   396
  val empty : T = empty_preproc check_defs
krauss@33099
   397
  val extend = I
wenzelm@33519
   398
  fun merge (a, _) = a
krauss@34232
   399
)
krauss@33099
   400
krauss@33099
   401
val get_preproc = Preprocessor.get o Context.Proof
krauss@33099
   402
val set_preproc = Preprocessor.map o K
krauss@33099
   403
krauss@33099
   404
krauss@33099
   405
krauss@34232
   406
local
wenzelm@44357
   407
  val option_parser = Parse.group (fn () => "option")
wenzelm@36960
   408
    ((Parse.reserved "sequential" >> K Sequential)
wenzelm@36960
   409
     || ((Parse.reserved "default" |-- Parse.term) >> Default)
wenzelm@36960
   410
     || (Parse.reserved "domintros" >> K DomIntros)
krauss@41846
   411
     || (Parse.reserved "no_partials" >> K No_Partials))
krauss@33099
   412
krauss@34232
   413
  fun config_parser default =
wenzelm@46949
   414
    (Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 option_parser) --| @{keyword ")"}) [])
krauss@34232
   415
     >> (fn opts => fold apply_opt opts default)
krauss@33099
   416
in
krauss@34232
   417
  fun function_parser default_cfg =
wenzelm@36960
   418
      config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs
krauss@33099
   419
end
krauss@33099
   420
krauss@33099
   421
krauss@33099
   422
end
krauss@33099
   423
end