src/HOL/Tools/Function/fun.ML
author wenzelm
Sun Oct 21 22:12:22 2012 +0200 (2012-10-21)
changeset 49965 ee25a04fa06a
parent 48099 e7e647949c95
child 54407 e95831757903
permissions -rw-r--r--
proper signatures;
krauss@33098
     1
(*  Title:      HOL/Tools/Function/fun.ML
krauss@33098
     2
    Author:     Alexander Krauss, TU Muenchen
krauss@33098
     3
krauss@41114
     4
Command "fun": Function definitions with pattern splitting/completion
krauss@41114
     5
and automated termination proofs.
krauss@33098
     6
*)
krauss@33098
     7
krauss@33098
     8
signature FUNCTION_FUN =
krauss@33098
     9
sig
wenzelm@44237
    10
  val fun_config : Function_Common.function_config
krauss@36523
    11
  val add_fun : (binding * typ option * mixfix) list ->
krauss@36523
    12
    (Attrib.binding * term) list -> Function_Common.function_config ->
krauss@36523
    13
    local_theory -> Proof.context
krauss@36523
    14
  val add_fun_cmd : (binding * string option * mixfix) list ->
krauss@36523
    15
    (Attrib.binding * string) list -> Function_Common.function_config ->
wenzelm@44239
    16
    bool -> local_theory -> Proof.context
krauss@33098
    17
krauss@34232
    18
  val setup : theory -> theory
krauss@33098
    19
end
krauss@33098
    20
krauss@33098
    21
structure Function_Fun : FUNCTION_FUN =
krauss@33098
    22
struct
krauss@33098
    23
krauss@33099
    24
open Function_Lib
krauss@33099
    25
open Function_Common
krauss@33098
    26
krauss@33098
    27
krauss@33098
    28
fun check_pats ctxt geq =
krauss@34232
    29
  let
krauss@34232
    30
    fun err str = error (cat_lines ["Malformed definition:",
krauss@34232
    31
      str ^ " not allowed in sequential mode.",
krauss@34232
    32
      Syntax.string_of_term ctxt geq])
wenzelm@42361
    33
    val thy = Proof_Context.theory_of ctxt
krauss@34232
    34
krauss@34232
    35
    fun check_constr_pattern (Bound _) = ()
krauss@34232
    36
      | check_constr_pattern t =
krauss@34232
    37
      let
krauss@34232
    38
        val (hd, args) = strip_comb t
krauss@34232
    39
      in
krauss@34232
    40
        (((case Datatype.info_of_constr thy (dest_Const hd) of
krauss@34232
    41
             SOME _ => ()
krauss@34232
    42
           | NONE => err "Non-constructor pattern")
krauss@34232
    43
          handle TERM ("dest_Const", _) => err "Non-constructor patterns");
krauss@34232
    44
         map check_constr_pattern args;
krauss@34232
    45
         ())
krauss@34232
    46
      end
krauss@34232
    47
krauss@39276
    48
    val (_, qs, gs, args, _) = split_def ctxt (K true) geq
krauss@34232
    49
krauss@34232
    50
    val _ = if not (null gs) then err "Conditional equations" else ()
krauss@34232
    51
    val _ = map check_constr_pattern args
krauss@34232
    52
krauss@34232
    53
    (* just count occurrences to check linearity *)
krauss@34232
    54
    val _ = if fold (fold_aterms (fn Bound _ => Integer.add 1 | _ => I)) args 0 > length qs
krauss@34232
    55
      then err "Nonlinear patterns" else ()
krauss@34232
    56
  in
krauss@34232
    57
    ()
krauss@34232
    58
  end
krauss@34232
    59
krauss@33098
    60
fun mk_catchall fixes arity_of =
krauss@34232
    61
  let
krauss@34232
    62
    fun mk_eqn ((fname, fT), _) =
krauss@34232
    63
      let
krauss@34232
    64
        val n = arity_of fname
krauss@34232
    65
        val (argTs, rT) = chop n (binder_types fT)
krauss@34232
    66
          |> apsnd (fn Ts => Ts ---> body_type fT)
krauss@34232
    67
wenzelm@43329
    68
        val qs = map Free (Name.invent Name.context "a" n ~~ argTs)
krauss@34232
    69
      in
krauss@34232
    70
        HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
krauss@34232
    71
          Const ("HOL.undefined", rT))
krauss@34232
    72
        |> HOLogic.mk_Trueprop
krauss@34232
    73
        |> fold_rev Logic.all qs
krauss@34232
    74
      end
krauss@34232
    75
  in
krauss@34232
    76
    map mk_eqn fixes
krauss@34232
    77
  end
krauss@33098
    78
krauss@33098
    79
fun add_catchall ctxt fixes spec =
krauss@39276
    80
  let val fqgars = map (split_def ctxt (K true)) spec
krauss@33098
    81
      val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars
krauss@33098
    82
                     |> AList.lookup (op =) #> the
krauss@33098
    83
  in
krauss@33098
    84
    spec @ mk_catchall fixes arity_of
krauss@33098
    85
  end
krauss@33098
    86
krauss@48099
    87
fun further_checks ctxt origs tss =
krauss@34232
    88
  let
krauss@48099
    89
    fun fail_redundant t =
krauss@48099
    90
      error (cat_lines ["Equation is redundant (covered by preceding clauses):", Syntax.string_of_term ctxt t])
krauss@42947
    91
    fun warn_missing strs =
wenzelm@43277
    92
      warning (cat_lines ("Missing patterns in function definition:" :: strs))
krauss@42947
    93
krauss@42947
    94
    val (tss', added) = chop (length origs) tss
krauss@33098
    95
krauss@42947
    96
    val _ = case chop 3 (flat added) of
krauss@42947
    97
       ([], []) => ()
krauss@42947
    98
     | (eqs, []) => warn_missing (map (Syntax.string_of_term ctxt) eqs)
krauss@42947
    99
     | (eqs, rest) => warn_missing (map (Syntax.string_of_term ctxt) eqs
krauss@42947
   100
         @ ["(" ^ string_of_int (length rest) ^ " more)"])
krauss@42947
   101
krauss@42947
   102
    val _ = (origs ~~ tss')
krauss@48099
   103
      |> map (fn (t, ts) => if null ts then fail_redundant t else ())
krauss@34232
   104
  in
krauss@42947
   105
    ()
krauss@34232
   106
  end
krauss@33098
   107
krauss@33099
   108
fun sequential_preproc (config as FunctionConfig {sequential, ...}) ctxt fixes spec =
krauss@34232
   109
  if sequential then
krauss@34232
   110
    let
krauss@34232
   111
      val (bnds, eqss) = split_list spec
krauss@34232
   112
krauss@34232
   113
      val eqs = map the_single eqss
krauss@33098
   114
krauss@34232
   115
      val feqs = eqs
krauss@34232
   116
        |> tap (check_defs ctxt fixes) (* Standard checks *)
krauss@34232
   117
        |> tap (map (check_pats ctxt)) (* More checks for sequential mode *)
krauss@34232
   118
krauss@34232
   119
      val compleqs = add_catchall ctxt fixes feqs (* Completion *)
krauss@33098
   120
krauss@42947
   121
      val spliteqs = Function_Split.split_all_equations ctxt compleqs
krauss@48099
   122
        |> tap (further_checks ctxt feqs)
krauss@34232
   123
krauss@34232
   124
      fun restore_spec thms =
krauss@34232
   125
        bnds ~~ take (length bnds) (unflat spliteqs thms)
krauss@33098
   126
krauss@34232
   127
      val spliteqs' = flat (take (length bnds) spliteqs)
krauss@34232
   128
      val fnames = map (fst o fst) fixes
krauss@34232
   129
      val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs'
krauss@33098
   130
krauss@34232
   131
      fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs)
krauss@34232
   132
        |> map (map snd)
krauss@33098
   133
krauss@33098
   134
krauss@34232
   135
      val bnds' = bnds @ replicate (length spliteqs - length bnds) Attrib.empty_binding
krauss@33098
   136
krauss@34232
   137
      (* using theorem names for case name currently disabled *)
krauss@34232
   138
      val case_names = map_index (fn (i, (_, es)) => mk_case_names i "" (length es)) 
krauss@34232
   139
        (bnds' ~~ spliteqs) |> flat
krauss@34232
   140
    in
krauss@34232
   141
      (flat spliteqs, restore_spec, sort, case_names)
krauss@34232
   142
    end
krauss@34232
   143
  else
krauss@34232
   144
    Function_Common.empty_preproc check_defs config ctxt fixes spec
krauss@33098
   145
krauss@33098
   146
val setup =
krauss@33099
   147
  Context.theory_map (Function_Common.set_preproc sequential_preproc)
krauss@33098
   148
krauss@33098
   149
krauss@41417
   150
val fun_config = FunctionConfig { sequential=true, default=NONE,
krauss@41846
   151
  domintros=false, partials=false }
krauss@33098
   152
wenzelm@44239
   153
fun gen_add_fun add lthy =
krauss@36523
   154
  let
krauss@36523
   155
    fun pat_completeness_auto ctxt =
krauss@36523
   156
      Pat_Completeness.pat_completeness_tac ctxt 1
wenzelm@42793
   157
      THEN auto_tac ctxt
krauss@36523
   158
    fun prove_termination lthy =
krauss@36523
   159
      Function.prove_termination NONE
wenzelm@49965
   160
        (Function_Common.get_termination_prover lthy) lthy
krauss@36523
   161
  in
krauss@36523
   162
    lthy
wenzelm@44239
   163
    |> add pat_completeness_auto |> snd
krauss@36547
   164
    |> prove_termination |> snd
krauss@36523
   165
  end
krauss@33098
   166
wenzelm@44239
   167
fun add_fun a b c = gen_add_fun (Function.add_function a b c)
wenzelm@44239
   168
fun add_fun_cmd a b c int = gen_add_fun (fn tac => Function.add_function_cmd a b c tac int)
krauss@33098
   169
krauss@33098
   170
krauss@33098
   171
krauss@33098
   172
val _ =
wenzelm@46961
   173
  Outer_Syntax.local_theory' @{command_spec "fun"}
wenzelm@46961
   174
    "define general recursive functions (short version)"
wenzelm@46961
   175
    (function_parser fun_config
wenzelm@46961
   176
      >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))
krauss@33098
   177
krauss@33098
   178
end