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