src/HOL/Data_Structures/Define_Time_Function.ML
author wenzelm
Wed, 07 Aug 2024 12:50:22 +0200
changeset 80657 c6dca9d3af4e
parent 80643 11b8f2e4c3d2
child 80734 7054a1bc8347
permissions -rw-r--r--
recover lost update (see 11b8f2e4c3d2 and 4041e7c8059d);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
     1
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
     2
signature TIMING_FUNCTIONS =
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
     3
sig
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
     4
type 'a converter = {
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
     5
  constc : local_theory -> term list -> (term -> 'a) -> term -> 'a,
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
     6
  funcc : local_theory -> term list -> (term -> 'a) -> term -> term list -> 'a,
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
     7
  ifc : local_theory -> term list -> (term -> 'a) -> typ -> term -> term -> term -> 'a,
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
     8
  casec : local_theory -> term list -> (term -> 'a) -> term -> term list -> 'a,
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
     9
  letc : local_theory -> term list -> (term -> 'a) -> typ -> term -> string list -> typ list -> term -> 'a
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    10
};
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
    11
val walk : local_theory -> term list -> 'a converter -> term -> 'a
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    12
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
    13
type pfunc = { names : string list, terms : term list, typs : typ list }
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    14
val fun_pretty':  Proof.context -> pfunc -> Pretty.T
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    15
val fun_pretty:  Proof.context -> Function.info -> Pretty.T
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    16
val print_timing':  Proof.context -> pfunc -> pfunc -> unit
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    17
val print_timing:  Proof.context -> Function.info -> Function.info -> unit
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    18
79969
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
    19
val reg_and_proove_time_func: theory -> term list -> term list
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    20
      -> bool -> Function.info * theory
79969
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
    21
val reg_time_func: theory -> term list -> term list
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
    22
      -> bool -> theory
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    23
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    24
val time_dom_tac: Proof.context -> thm -> thm list -> int -> tactic
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    25
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    26
end
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    27
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    28
structure Timing_Functions : TIMING_FUNCTIONS =
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    29
struct
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    30
(* Configure config variable to adjust the prefix *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    31
val bprefix = Attrib.setup_config_string @{binding "time_prefix"} (K "T_")
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    32
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    33
(* some default values to build terms easier *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    34
val zero = Const (@{const_name "Groups.zero"}, HOLogic.natT)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    35
val one = Const (@{const_name "Groups.one"}, HOLogic.natT)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    36
(* Extracts terms from function info *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    37
fun terms_of_info (info: Function.info) =
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    38
let
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    39
  val {simps, ...} = info
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    40
in
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    41
  map Thm.prop_of (case simps of SOME s => s | NONE => error "No terms of function found in info")
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    42
end;
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    43
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    44
type pfunc = {
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
    45
  names : string list,
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    46
  terms : term list,
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
    47
  typs : typ list
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    48
}
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    49
fun info_pfunc (info: Function.info): pfunc =
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    50
let
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    51
  val {defname, fs, ...} = info;
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    52
  val T = case hd fs of (Const (_,T)) => T | _ => error "Internal error: Invalid info to print"
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    53
in
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
    54
  { names=[Binding.name_of defname], terms=terms_of_info info, typs=[T] }
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    55
end
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    56
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    57
(* Auxiliary functions for printing functions *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    58
fun fun_pretty' ctxt (pfunc: pfunc) =
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    59
let
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
    60
  val {names, terms, typs} = pfunc;
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
    61
  val header_beg = Pretty.str "fun ";
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
    62
  fun prepHeadCont (nm,T) = [Pretty.str (nm ^ " :: "), (Pretty.quote (Syntax.pretty_typ ctxt T))]
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
    63
  val header_content =
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
    64
     List.concat (prepHeadCont (hd names,hd typs) :: map ((fn l => Pretty.str "\nand " :: l) o prepHeadCont) (ListPair.zip (tl names, tl typs)));
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
    65
  val header_end = Pretty.str " where\n  ";
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
    66
  val header = [header_beg] @ header_content @ [header_end];
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    67
  fun separate sep prts =
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    68
    flat (Library.separate [Pretty.str sep] (map single prts));
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    69
  val ptrms = (separate "\n| " (map (Syntax.pretty_term ctxt) terms));
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    70
in
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    71
  Pretty.text_fold (header @ ptrms)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    72
end
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    73
fun fun_pretty ctxt = fun_pretty' ctxt o info_pfunc
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    74
fun print_timing' ctxt (opfunc: pfunc) (tpfunc: pfunc) =
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    75
let
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
    76
  val {names, ...} = opfunc;
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    77
  val poriginal = Pretty.item [Pretty.str "Original function:\n", fun_pretty' ctxt opfunc]
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    78
  val ptiming = Pretty.item [Pretty.str ("Running time function:\n"), fun_pretty' ctxt tpfunc]
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    79
in
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
    80
  Pretty.writeln (Pretty.text_fold [Pretty.str ("Converting " ^ (hd names) ^ (String.concat (map (fn nm => ", " ^ nm) (tl names))) ^ "\n"), poriginal, Pretty.str "\n", ptiming])
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    81
end
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    82
fun print_timing ctxt (oinfo: Function.info) (tinfo: Function.info) =
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    83
  print_timing' ctxt (info_pfunc oinfo) (info_pfunc tinfo)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    84
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    85
val If_name = @{const_name "HOL.If"}
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    86
val Let_name = @{const_name "HOL.Let"}
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    87
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
    88
fun contains l e = exists (fn e' => e' = e) l
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
    89
fun zip [] [] = []
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
    90
  | zip (x::xs) (y::ys) = (x, y) :: zip xs ys
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
    91
  | zip _ _ = error "Internal error: Cannot zip lists with differing size"
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
    92
fun index [] _ = 0
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
    93
  | index (x::xs) el = (if x = el then 0 else 1 + index xs el)
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
    94
fun used_for_const orig_used t i = orig_used (t,i)
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
    95
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    96
(* returns true if it's an if term *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    97
fun is_if (Const (n,_)) = (n = If_name)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    98
  | is_if _ = false
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
    99
(* returns true if it's a case term *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   100
fun is_case (Const (n,_)) = String.isPrefix "case_" (List.last (String.fields (fn s => s = #".") n))
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   101
  | is_case _ = false
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   102
(* returns true if it's a let term *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   103
fun is_let (Const (n,_)) = (n = Let_name)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   104
  | is_let _ = false
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   105
(* change type of original function to new type (_ \<Rightarrow> ... \<Rightarrow> _ to _ \<Rightarrow> ... \<Rightarrow> nat)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   106
    and replace all function arguments f with (t*T_f) *)
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   107
fun change_typ' used i (Type ("fun", [T1, T2])) = 
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   108
      Type ("fun", [check_for_fun' (used i) T1, change_typ' used (i+1) T2])
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   109
  | change_typ' _ _ _ = HOLogic.natT
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   110
and check_for_fun' true (f as Type ("fun", [_,_])) = HOLogic.mk_prodT (f, change_typ' (K false) 0 f)
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   111
  | check_for_fun' false (f as Type ("fun", [_,_])) = change_typ' (K false) 0 f
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   112
  | check_for_fun' _ t = t
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   113
val change_typ = change_typ' (K false) 0
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   114
(* Convert string name of function to its timing equivalent *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   115
fun fun_name_to_time ctxt name =
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   116
let
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   117
  val prefix = Config.get ctxt bprefix
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   118
  fun replace_last_name [n] = [prefix ^ n]
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   119
    | replace_last_name (n::ns) = n :: (replace_last_name ns)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   120
    | replace_last_name _ = error "Internal error: Invalid function name to convert"
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   121
  val parts = String.fields (fn s => s = #".") name
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   122
in
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   123
  String.concatWith "." (replace_last_name parts)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   124
end
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   125
(* Count number of arguments of a function *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   126
fun count_args (Type (n, [_,res])) = (if n = "fun" then 1 + count_args res else 0)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   127
  | count_args _ = 0
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   128
(* Check if number of arguments matches function *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   129
fun check_args s (Const (_,T), args) =
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   130
    (if length args = count_args T then () else error ("Partial applications/Lambdas not allowed (" ^ s ^ ")"))
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   131
  | check_args s (Free (_,T), args) =
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   132
    (if length args = count_args T then () else error ("Partial applications/Lambdas not allowed (" ^ s ^ ")"))
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   133
  | check_args s _ = error ("Partial applications/Lambdas not allowed (" ^ s ^ ")")
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   134
(* Removes Abs *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   135
fun rem_abs f (Abs (_,_,t)) = rem_abs f t
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   136
  | rem_abs f t = f t
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   137
(* Map right side of equation *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   138
fun map_r f (pT $ (eq $ l $ r)) = (pT $ (eq $ l $ f r))
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   139
  | map_r _ _ = error "Internal error: No right side of equation found"
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   140
(* Get left side of equation *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   141
fun get_l (_ $ (_ $ l $ _)) = l
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   142
  | get_l _ = error "Internal error: No left side of equation found"
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   143
(* Get right side of equation *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   144
fun get_r (_ $ (_ $ _ $ r)) = r
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   145
  | get_r _ = error "Internal error: No right side of equation found"
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   146
(* Return name of Const *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   147
fun Const_name (Const (nm,_)) = SOME nm
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   148
  | Const_name _ = NONE
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   149
fun is_Used (Type ("Product_Type.prod", _)) = true
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   150
  | is_Used _ = false
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   151
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   152
fun time_term ctxt (Const (nm,T)) =
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   153
let
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   154
  val T_nm = fun_name_to_time ctxt nm
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   155
  val T_T = change_typ T
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   156
in
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   157
(SOME (Syntax.check_term ctxt (Const (T_nm,T_T))))
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   158
  handle (ERROR _) =>
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   159
    case Syntax.read_term ctxt (Long_Name.base_name T_nm)
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   160
      of (Const (nm,T_T)) =>
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   161
        let
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   162
          fun col_Used i (Type ("fun", [Type ("fun", _), Ts])) (Type ("fun", [T', Ts'])) =
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   163
            (if is_Used T' then [i] else []) @ col_Used (i+1) Ts Ts'
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   164
            | col_Used i (Type ("fun", [_, Ts])) (Type ("fun", [_, Ts'])) = col_Used (i+1) Ts Ts'
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   165
            | col_Used _ _ _ = []
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   166
        in
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   167
          SOME (Const (nm,change_typ' (contains (col_Used 0 T T_T)) 0 T))
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   168
        end
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   169
       | _ => error ("Timing function of " ^ nm ^ " is not defined")
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   170
end
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   171
  | time_term _ _ = error "Internal error: No valid function given"
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   172
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   173
type 'a converter = {
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   174
  constc : local_theory -> term list -> (term -> 'a) -> term -> 'a,
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   175
  funcc : local_theory -> term list -> (term -> 'a) -> term -> term list -> 'a,
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   176
  ifc : local_theory -> term list -> (term -> 'a) -> typ -> term -> term -> term -> 'a,
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   177
  casec : local_theory -> term list -> (term -> 'a) -> term -> term list -> 'a,
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   178
  letc : local_theory -> term list -> (term -> 'a) -> typ -> term -> string list -> typ list -> term -> 'a
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   179
};
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   180
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   181
(* Walks over term and calls given converter *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   182
fun walk_func (t1 $ t2) ts = walk_func t1 (t2::ts)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   183
  | walk_func t ts = (t, ts)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   184
fun build_func (f, []) = f
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   185
  | build_func (f, (t::ts)) = build_func (f$t, ts)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   186
fun walk_abs (Abs (nm,T,t)) nms Ts = walk_abs t (nm::nms) (T::Ts)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   187
  | walk_abs t nms Ts = (t, nms, Ts)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   188
fun build_abs t (nm::nms) (T::Ts) = build_abs (Abs (nm,T,t)) nms Ts
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   189
  | build_abs t [] [] = t
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   190
  | build_abs _ _ _ = error "Internal error: Invalid terms to build abs"
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   191
fun walk ctxt (origin: term list) (conv as {ifc, casec, funcc, letc, ...} : 'a converter) (t as _ $ _) =
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   192
  let
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   193
    val (f, args) = walk_func t []
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   194
    val this = (walk ctxt origin conv)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   195
    val _ = (case f of Abs _ => error "Lambdas not supported" | _ => ())
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   196
  in
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   197
    (if is_if f then
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   198
      (case f of (Const (_,T)) =>
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   199
        (case args of [cond, t, f] => ifc ctxt origin this T cond t f
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   200
                   | _ => error "Partial applications not supported (if)")
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   201
               | _ => error "Internal error: invalid if term")
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   202
      else if is_case f then casec ctxt origin this f args
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   203
      else if is_let f then
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   204
      (case f of (Const (_,lT)) =>
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   205
         (case args of [exp, t] => 
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   206
            let val (t,nms,Ts) = walk_abs t [] [] in letc ctxt origin this lT exp nms Ts t end
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   207
                     | _ => error "Partial applications not allowed (let)")
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   208
               | _ => error "Internal error: invalid let term")
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   209
      else funcc ctxt origin this f args)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   210
  end
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   211
  | walk ctxt origin (conv as {constc, ...}) c = 
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   212
      constc ctxt origin (walk ctxt origin conv) c
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   213
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   214
(* 1. Fix all terms *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   215
(* Exchange Var in types and terms to Free *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   216
fun fixTerms (Var(ixn,T)) = Free (fst ixn, T)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   217
  | fixTerms t = t
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   218
fun fixTypes (TVar ((t, _), T)) = TFree (t, T)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   219
  | fixTypes t = t
79542
b941924a407d define_time_function: avoid unused let's
nipkow
parents: 79494
diff changeset
   220
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   221
fun noFun (Type ("fun", _)) = error "Functions in datatypes are not allowed in case constructions"
80643
11b8f2e4c3d2 branches of case expressions may need to be eta-expanded
nipkow
parents: 80636
diff changeset
   222
  | noFun T = T
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   223
fun casecBuildBounds n t = if n > 0 then casecBuildBounds (n-1) (t $ (Bound (n-1))) else t
80643
11b8f2e4c3d2 branches of case expressions may need to be eta-expanded
nipkow
parents: 80636
diff changeset
   224
fun casecAbs ctxt f n (Type ("fun",[T,Tr])) (Abs (v,Ta,t)) = ( map_atyps noFun T; Abs (v,Ta,casecAbs ctxt f n Tr t))
11b8f2e4c3d2 branches of case expressions may need to be eta-expanded
nipkow
parents: 80636
diff changeset
   225
  | casecAbs ctxt f n (Type ("fun",[T,Tr])) t =
11b8f2e4c3d2 branches of case expressions may need to be eta-expanded
nipkow
parents: 80636
diff changeset
   226
    (map_atyps noFun T; case Variable.variant_fixes ["x"] ctxt of ([v],ctxt) =>
11b8f2e4c3d2 branches of case expressions may need to be eta-expanded
nipkow
parents: 80636
diff changeset
   227
    (Abs (v,T,casecAbs ctxt f (n + 1) Tr t))
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   228
    | _ => error "Internal error: could not fix variable")
79714
80cb54976c1c timing function generation bug fix by Jonas Stahl
nipkow
parents: 79665
diff changeset
   229
  | casecAbs _ f n _ t = f (casecBuildBounds n (Term.incr_bv n 0 t))
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   230
fun fixCasecCases _ _ _ [t] = [t]
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   231
  | fixCasecCases ctxt f (Type (_,[T,Tr])) (t::ts) = casecAbs ctxt f 0 T t :: fixCasecCases ctxt f Tr ts
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   232
  | fixCasecCases _ _ _ _ = error "Internal error: invalid case types/terms"
79542
b941924a407d define_time_function: avoid unused let's
nipkow
parents: 79494
diff changeset
   233
fun fixCasec ctxt _ f (t as Const (_,T)) args =
b941924a407d define_time_function: avoid unused let's
nipkow
parents: 79494
diff changeset
   234
      (check_args "cases" (t,args); build_func (t,fixCasecCases ctxt f T args))
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   235
  | fixCasec _ _ _ _ _ = error "Internal error: invalid case term"
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   236
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   237
fun fixPartTerms ctxt (term: term list) t =
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   238
  let
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   239
    val _ = check_args "args" (walk_func (get_l t) [])
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   240
  in
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   241
    map_r (walk ctxt term {
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   242
          funcc = (fn _ => fn _ => fn f => fn t => fn args =>
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   243
              (check_args "func" (t,args); build_func (t, map f args))),
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   244
          constc = (fn _ => fn _ => fn _ => fn c => (case c of Abs _ => error "Lambdas not supported" | _ => c)),
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   245
          ifc = (fn _ => fn _ => fn f => fn T => fn cond => fn tt => fn tf =>
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   246
            ((Const (If_name, T)) $ f cond $ (f tt) $ (f tf))),
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   247
          casec = fixCasec,
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   248
          letc = (fn _ => fn _ => fn f => fn expT => fn exp => fn nms => fn Ts => fn t =>
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   249
              let
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   250
                val f' = if length nms = 0 then
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   251
                (case f (t$exp) of t$_ => t | _ => error "Internal error: case could not be fixed (let)")
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   252
                else f t
79542
b941924a407d define_time_function: avoid unused let's
nipkow
parents: 79494
diff changeset
   253
              in (Const (Let_name,expT) $ (f exp) $ build_abs f' nms Ts) end)
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   254
      }) t
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   255
  end
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   256
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   257
(* 2. Check for properties about the function *)
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   258
(* 2.1 Check if function is recursive *)
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   259
fun or f (a,b) = f a orelse b
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   260
fun find_rec ctxt term = (walk ctxt term {
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   261
          funcc = (fn _ => fn _ => fn f => fn t => fn args => List.exists (fn term => Const_name t = Const_name term) term orelse List.foldr (or f) false args),
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   262
          constc = (K o K o K o K) false,
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   263
          ifc = (fn _ => fn _ => fn f => fn _ => fn cond => fn tt => fn tf => f cond orelse f tt orelse f tf),
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   264
          casec = (fn _ => fn _ => fn f => fn t => fn cs => f t orelse List.foldr (or (rem_abs f)) false cs),
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   265
          letc = (fn _ => fn _ => fn f => fn _ => fn exp => fn _ => fn _ => fn t => f exp orelse f t)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   266
      }) o get_r
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   267
fun is_rec ctxt (term: term list) = List.foldr (or (find_rec ctxt term)) false
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   268
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   269
(* 2.2 Check for higher-order function if original function is used *)
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   270
fun find_used' ctxt term t T_t =
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   271
let
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   272
  val (ident, _) = walk_func (get_l t) []
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   273
  val (T_ident, T_args) = walk_func (get_l T_t) []
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   274
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   275
  fun filter_passed [] = []
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   276
    | filter_passed ((f as Free (_, Type ("Product_Type.prod",[Type ("fun",_), Type ("fun", _)])))::args) = 
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   277
        f :: filter_passed args
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   278
    | filter_passed (_::args) = filter_passed args
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   279
  val frees' = (walk ctxt term {
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   280
          funcc = (fn _ => fn _ => fn f => fn t => fn args =>
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   281
              (case t of (Const ("Product_Type.prod.snd", _)) => []
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   282
                  | _ => (if t = T_ident then [] else filter_passed args)
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   283
                    @ List.foldr (fn (l,r) => f l @ r) [] args)),
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   284
          constc = (K o K o K o K) [],
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   285
          ifc = (fn _ => fn _ => fn f => fn _ => fn cond => fn tt => fn tf => f cond @ f tt @ f tf),
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   286
          casec = (fn _ => fn _ => fn f => fn _ => fn cs => List.foldr (fn (l,r) => f l @ r) [] cs),
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   287
          letc = (fn _ => fn _ => fn f => fn _ => fn exp => fn _ => fn _ => fn t => f exp @ f t)
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   288
      }) (get_r T_t)
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   289
  fun build _ [] _ = false
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   290
    | build i (a::args) item =
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   291
        (if item = (ident,i) then contains frees' a else build (i+1) args item)
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   292
in
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   293
  build 0 T_args
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   294
end
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   295
fun find_used ctxt term terms T_terms =
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   296
  zip terms T_terms
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   297
  |> List.map (fn (t, T_t) => find_used' ctxt term t T_t)
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   298
  |> List.foldr (fn (f,g) => fn item => f item orelse g item) (K false)
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   299
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   300
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   301
(* 3. Convert equations *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   302
(* Some Helper *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   303
val plusTyp = @{typ "nat => nat => nat"}
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   304
fun plus (SOME a) (SOME b) = SOME (Const (@{const_name "Groups.plus"}, plusTyp) $ a $ b)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   305
  | plus (SOME a) NONE = SOME a
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   306
  | plus NONE (SOME b) = SOME b
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   307
  | plus NONE NONE = NONE
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   308
fun opt_term NONE = HOLogic.zero
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   309
  | opt_term (SOME t) = t
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   310
fun use_origin (Free (nm, T as Type ("fun",_))) = HOLogic.mk_fst (Free (nm,HOLogic.mk_prodT (T, change_typ T)))
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   311
  | use_origin t = t
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   312
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   313
(* Converting of function term *)
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   314
fun fun_to_time ctxt orig_used _ (origin: term list) (func as Const (nm,T)) =
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   315
let
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   316
  val prefix = Config.get ctxt bprefix
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   317
  val used' = used_for_const orig_used func
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   318
in
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   319
  if contains origin func then SOME (Free (prefix ^ Term.term_name func, change_typ' used' 0 T)) else
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   320
  if Zero_Funcs.is_zero (Proof_Context.theory_of ctxt) (nm,T) then NONE else
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   321
    time_term ctxt func
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   322
end
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   323
  | fun_to_time ctxt _ used _ (f as Free (nm,T)) = SOME (
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   324
      if used f then HOLogic.mk_snd (Free (nm,HOLogic.mk_prodT (T,change_typ T)))
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   325
      else Free (Config.get ctxt bprefix ^ nm, change_typ T)
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   326
      )
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   327
  | fun_to_time _ _ _ _ _ = error "Internal error: invalid function to convert"
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   328
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   329
(* Convert arguments of left side of a term *)
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   330
fun conv_arg ctxt used _ (f as Free (nm,T as Type("fun",_))) =
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   331
    if used f then Free (nm, HOLogic.mk_prodT (T, change_typ' (K false) 0 T))
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   332
    else Free (Config.get ctxt bprefix ^ nm, change_typ' (K false) 0 T)
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   333
  | conv_arg ctxt _ origin (f as Const (_, Type("fun",_))) =
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   334
      (error "weird case i don't understand TODO"; HOLogic.mk_prod (f, fun_to_time ctxt (K false) (K false) origin f |> Option.valOf))
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   335
  | conv_arg _ _ _ x = x
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   336
fun conv_args ctxt used origin = map (conv_arg ctxt used origin)
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   337
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   338
(* Handle function calls *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   339
fun build_zero (Type ("fun", [T, R])) = Abs ("x", T, build_zero R)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   340
  | build_zero _ = zero
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   341
fun funcc_use_origin _ _ used (f as Free (nm, T as Type ("fun",_))) =
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   342
    if used f then HOLogic.mk_fst (Free (nm,HOLogic.mk_prodT (T, change_typ T)))
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   343
    else error "Internal error: Error in used detection"
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   344
  | funcc_use_origin _ _ _ t = t
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   345
fun funcc_conv_arg ctxt origin used _ (t as (_ $ _)) = map_aterms (funcc_use_origin ctxt origin used) t
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   346
  | funcc_conv_arg ctxt _ used u (f as Free (nm, T as Type ("fun",_))) =
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   347
      if used f then
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   348
        if u then Free (nm, HOLogic.mk_prodT (T, change_typ T))
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   349
        else HOLogic.mk_snd (Free (nm,HOLogic.mk_prodT (T,change_typ T)))
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   350
      else Free (Config.get ctxt bprefix ^ nm, change_typ T)
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   351
  | funcc_conv_arg ctxt origin _ true (f as Const (_,T as Type ("fun",_))) =
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   352
  (Const (@{const_name "Product_Type.Pair"},
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   353
      Type ("fun", [T,Type ("fun", [change_typ T, HOLogic.mk_prodT (T,change_typ T)])]))
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   354
    $ f $ (Option.getOpt (fun_to_time ctxt (K false) (K false) origin f, build_zero T)))
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   355
  | funcc_conv_arg ctxt origin _ false (f as Const (_,T as Type ("fun",_))) =
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   356
      Option.getOpt (fun_to_time ctxt (K false) (K false) origin f, build_zero T)
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   357
  | funcc_conv_arg _ _ _ _ t = t
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   358
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   359
fun funcc_conv_args _ _ _ _ [] = []
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   360
  | funcc_conv_args ctxt origin used (Type ("fun", [t, ts])) (a::args) =
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   361
      funcc_conv_arg ctxt origin used (is_Used t) a :: funcc_conv_args ctxt origin used ts args
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   362
  | funcc_conv_args _ _ _ _ _ = error "Internal error: Non matching type"
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   363
fun funcc orig_used used ctxt (origin: term list) f func args =
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   364
let
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   365
  fun get_T (Free (_,T)) = T
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   366
    | get_T (Const (_,T)) = T
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   367
    | get_T (_ $ (Free (_,Type (_, [_, T])))) = T (* Case of snd was constructed *)
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   368
    | get_T _ = error "Internal error: Forgotten type"
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   369
in
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   370
  List.foldr (I #-> plus)
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   371
  (case fun_to_time ctxt orig_used used origin func
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   372
    of SOME t => SOME (build_func (t,funcc_conv_args ctxt origin used (get_T t) args))
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   373
    | NONE => NONE)
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   374
  (map f args)
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   375
end
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   376
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   377
(* Handle case terms *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   378
fun casecIsCase (Type (n1, [_,Type (n2, _)])) = (n1 = "fun" andalso n2 = "fun")
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   379
  | casecIsCase _ = false
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   380
fun casecLastTyp (Type (n, [T1,T2])) = Type (n, [T1, change_typ T2])
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   381
  | casecLastTyp _ = error "Internal error: Invalid case type"
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   382
fun casecTyp (Type (n, [T1, T2])) =
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   383
      Type (n, [change_typ T1, (if casecIsCase T2 then casecTyp else casecLastTyp) T2])
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   384
  | casecTyp _ = error "Internal error: Invalid case type"
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   385
fun casecAbs f (Abs (v,Ta,t)) = (case casecAbs f t of (nconst,t) => (nconst,Abs (v,Ta,t)))
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   386
  | casecAbs f t = (case f t of NONE => (false,HOLogic.zero) | SOME t => (true,t))
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   387
fun casecArgs _ [t] = (false, [map_aterms use_origin t])
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   388
  | casecArgs f (t::ar) =
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   389
    (case casecAbs f t of (nconst, tt) => 
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   390
      casecArgs f ar ||> (fn ar => tt :: ar) |>> (if nconst then K true else I))
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   391
  | casecArgs _ _ = error "Internal error: Invalid case term"
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   392
fun casec _ _ f (Const (t,T)) args =
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   393
  if not (casecIsCase T) then error "Internal error: Invalid case type" else
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   394
    let val (nconst, args') = casecArgs f args in
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   395
      plus
79969
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   396
        (f (List.last args))
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   397
        (if nconst then
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   398
          SOME (build_func (Const (t,casecTyp T), args'))
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   399
         else NONE)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   400
    end
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   401
  | casec _ _ _ _ _ = error "Internal error: Invalid case term"
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   402
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   403
(* Handle if terms -> drop the term if true and false terms are zero *)
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   404
fun ifc _ _ f _ cond tt ft =
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   405
  let
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   406
    val rcond = map_aterms use_origin cond
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   407
    val tt = f tt
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   408
    val ft = f ft
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   409
  in
79969
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   410
    plus (f cond) (case (tt,ft) of (NONE, NONE) => NONE | _ =>
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   411
       if tt = ft then tt else
79969
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   412
       (SOME ((Const (If_name, @{typ "bool \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"})) $ rcond $ (opt_term tt) $ (opt_term ft))))
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   413
  end
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   414
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   415
fun letc_change_typ (Type ("fun", [T1, Type ("fun", [T2, _])])) = (Type ("fun", [T1, Type ("fun", [change_typ T2, HOLogic.natT])]))
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   416
  | letc_change_typ _ = error "Internal error: invalid let type"
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   417
fun letc _ _ f expT exp nms Ts t =
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   418
    plus (f exp)
79542
b941924a407d define_time_function: avoid unused let's
nipkow
parents: 79494
diff changeset
   419
    (if length nms = 0 (* In case of "length nms = 0" the expression got reducted
b941924a407d define_time_function: avoid unused let's
nipkow
parents: 79494
diff changeset
   420
                          Here we need Bound 0 to gain non-partial application *)
b941924a407d define_time_function: avoid unused let's
nipkow
parents: 79494
diff changeset
   421
    then (case f (t $ Bound 0) of SOME (t' $ Bound 0) =>
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   422
                                 (SOME (Const (Let_name, letc_change_typ expT) $ (map_aterms use_origin exp) $ t'))
79542
b941924a407d define_time_function: avoid unused let's
nipkow
parents: 79494
diff changeset
   423
                                  (* Expression is not used and can therefore let be dropped *)
b941924a407d define_time_function: avoid unused let's
nipkow
parents: 79494
diff changeset
   424
                                | SOME t' => SOME t'
b941924a407d define_time_function: avoid unused let's
nipkow
parents: 79494
diff changeset
   425
                                | NONE => NONE)
b941924a407d define_time_function: avoid unused let's
nipkow
parents: 79494
diff changeset
   426
    else (case f t of SOME t' =>
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   427
      SOME (if Term.is_dependent t' then Const (Let_name, letc_change_typ expT) $ (map_aterms use_origin exp) $ build_abs t' nms Ts
79542
b941924a407d define_time_function: avoid unused let's
nipkow
parents: 79494
diff changeset
   428
                                    else Term.subst_bounds([exp],t'))
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   429
    | NONE => NONE))
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   430
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   431
(* The converter for timing functions given to the walker *)
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   432
fun converter orig_used used : term option converter = {
80036
a594d22e69d6 updated time functions for Array_Braun
nipkow
parents: 79969
diff changeset
   433
        constc = fn _ => fn _ => fn _ => fn t =>
a594d22e69d6 updated time functions for Array_Braun
nipkow
parents: 79969
diff changeset
   434
          (case t of Const ("HOL.undefined", _) => SOME (Const ("HOL.undefined", @{typ "nat"}))
a594d22e69d6 updated time functions for Array_Braun
nipkow
parents: 79969
diff changeset
   435
                   | _ => NONE),
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   436
        funcc = (funcc orig_used used),
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   437
        ifc = ifc,
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   438
        casec = casec,
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   439
        letc = letc
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   440
    }
79665
0a152b2f73ae time funs: +1 instead of 1+
nipkow
parents: 79542
diff changeset
   441
fun top_converter is_rec _ _ = opt_term o (fn exp => plus exp (if is_rec then SOME one else NONE))
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   442
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   443
(* Use converter to convert right side of a term *)
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   444
fun to_time ctxt origin is_rec orig_used used term =
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   445
  top_converter is_rec ctxt origin (walk ctxt origin (converter orig_used used) term)
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   446
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   447
(* Converts a term to its running time version *)
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   448
fun convert_term ctxt (origin: term list) is_rec orig_used (pT $ (Const (eqN, _) $ l $ r)) =
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   449
let
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   450
  val (l' as (l_const, l_params)) = walk_func l []
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   451
  val used =
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   452
    l_const
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   453
    |> used_for_const orig_used
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   454
    |> (fn f => fn n => f (index l_params n))
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   455
in
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   456
      pT
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   457
      $ (Const (eqN, @{typ "nat \<Rightarrow> nat \<Rightarrow> bool"})
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   458
        $ (build_func (l' |>> (fun_to_time ctxt orig_used used origin) |>> Option.valOf ||> conv_args ctxt used origin))
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   459
        $ (to_time ctxt origin is_rec orig_used used r))
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   460
end
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   461
  | convert_term _ _ _ _ _ = error "Internal error: invalid term to convert"
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   462
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   463
(* 4. Tactic to prove "f_dom n" *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   464
fun time_dom_tac ctxt induct_rule domintros =
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   465
  (Induction.induction_tac ctxt true [] [[]] [] (SOME [induct_rule]) []
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   466
    THEN_ALL_NEW ((K (auto_tac ctxt)) THEN' (fn i => FIRST' (
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   467
    (if i <= length domintros then [Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN ctxt [List.nth (domintros, i-1)]] else []) @
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   468
    [Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN ctxt domintros]) i)))
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   469
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   470
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   471
fun get_terms theory (term: term) =
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   472
  Spec_Rules.retrieve_global theory term
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   473
      |> hd |> #rules
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   474
      |> map Thm.prop_of
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   475
   handle Empty => error "Function or terms of function not found"
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   476
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   477
(* Register timing function of a given function *)
79969
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   478
fun reg_and_proove_time_func (theory: theory) (term: term list) (terms: term list) print =
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   479
  reg_time_func theory term terms false
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   480
  |> proove_termination term terms print
79969
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   481
and reg_time_func (theory: theory) (term: term list) (terms: term list) print =
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   482
  let
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   483
    val lthy = Named_Target.theory_init theory
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   484
    val _ =
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   485
      case time_term lthy (hd term)
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   486
            handle (ERROR _) => NONE
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   487
        of SOME _ => error ("Timing function already declared: " ^ (Term.term_name (hd term)))
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   488
         | NONE => ()
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   489
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   490
    (* 1. Fix all terms *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   491
    (* Exchange Var in types and terms to Free and check constraints *)
79969
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   492
    val terms = map
79542
b941924a407d define_time_function: avoid unused let's
nipkow
parents: 79494
diff changeset
   493
      (map_aterms fixTerms
b941924a407d define_time_function: avoid unused let's
nipkow
parents: 79494
diff changeset
   494
        #> map_types (map_atyps fixTypes)
b941924a407d define_time_function: avoid unused let's
nipkow
parents: 79494
diff changeset
   495
        #> fixPartTerms lthy term)
b941924a407d define_time_function: avoid unused let's
nipkow
parents: 79494
diff changeset
   496
      terms
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   497
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   498
    (* 2. Find properties about the function *)
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   499
    (* 2.1 Check if function is recursive *)
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   500
    val is_rec = is_rec lthy term terms
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   501
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   502
    (* 3. Convert every equation
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   503
      - Change type of toplevel equation from _ \<Rightarrow> _ \<Rightarrow> bool to nat \<Rightarrow> nat \<Rightarrow> bool
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   504
      - On left side change name of function to timing function
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   505
      - Convert right side of equation with conversion schema
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   506
    *)
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   507
    fun convert used = map (convert_term lthy term is_rec used)
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   508
    fun repeat T_terms =
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   509
      let
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   510
        val orig_used = find_used lthy term terms T_terms
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   511
        val T_terms' = convert orig_used terms
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   512
      in
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   513
        if T_terms' <> T_terms then repeat T_terms' else T_terms'
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   514
      end
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   515
    val T_terms = repeat (convert (K true) terms)
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   516
    val orig_used = find_used lthy term terms T_terms
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   517
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   518
    (* 4. Register function and prove termination *)
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   519
    val names = map Term.term_name term
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   520
    val timing_names = map (fun_name_to_time lthy) names
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   521
    val bindings = map (fn nm => (Binding.name nm, NONE, NoSyn)) timing_names
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   522
    fun pat_completeness_auto ctxt =
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   523
      Pat_Completeness.pat_completeness_tac ctxt 1 THEN auto_tac ctxt
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   524
    val specs = map (fn eq => (((Binding.empty, []), eq), [], [])) T_terms
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   525
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   526
    (* For partial functions sequential=true is needed in order to support them
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   527
       We need sequential=false to support the automatic proof of termination over dom
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   528
    *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   529
    fun register seq =
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   530
      let
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   531
        val _ = (if seq then warning "Falling back on sequential function..." else ())
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   532
        val fun_config = Function_Common.FunctionConfig
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   533
          {sequential=seq, default=NONE, domintros=true, partials=false}
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   534
      in
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   535
        Function.add_function bindings specs fun_config pat_completeness_auto lthy
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   536
      end
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   537
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   538
    (* Context for printing without showing question marks *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   539
    val print_ctxt = lthy
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   540
      |> Config.put show_question_marks false
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   541
      |> Config.put show_sorts false (* Change it for debugging *)
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   542
    val print_ctxt =  List.foldl (fn (term, ctxt) => Variable.add_fixes_implicit term ctxt) print_ctxt (term @ T_terms)
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   543
    (* Print result if print *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   544
    val _ = if not print then () else
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   545
        let
80657
c6dca9d3af4e recover lost update (see 11b8f2e4c3d2 and 4041e7c8059d);
wenzelm
parents: 80643
diff changeset
   546
          val nms = map dest_Const_name term
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   547
          val used = map (used_for_const orig_used) term
80657
c6dca9d3af4e recover lost update (see 11b8f2e4c3d2 and 4041e7c8059d);
wenzelm
parents: 80643
diff changeset
   548
          val typs = map dest_Const_type term
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   549
        in
80624
9f8034d29365 time_function T_map can now be generated automatically.
nipkow
parents: 80036
diff changeset
   550
          print_timing' print_ctxt { names=nms, terms=terms, typs=typs } { names=timing_names, terms=T_terms, typs=map (fn (used, typ) => change_typ' used 0 typ) (zip used typs) }
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   551
        end
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   552
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   553
    (* Register function *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   554
    val (_, lthy) =
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   555
      register false
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   556
      handle (ERROR _) =>
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   557
        register true
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   558
           | Match =>
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   559
        register true
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   560
  in
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   561
    Local_Theory.exit_global lthy
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   562
  end
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   563
and proove_termination (term: term list) terms print (theory: theory) =
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   564
  let
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   565
    val lthy = Named_Target.theory_init theory
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   566
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   567
    (* Start proving the termination *)  
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   568
    val infos = SOME (map (Function.get_info lthy) term) handle Empty => NONE
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   569
    val timing_names = map (fun_name_to_time lthy o Term.term_name) term
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   570
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   571
    (* Proof by lexicographic_order_tac *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   572
    val (time_info, lthy') =
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   573
      (Function.prove_termination NONE
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   574
        (Lexicographic_Order.lexicographic_order_tac false lthy) lthy)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   575
        handle (ERROR _) =>
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   576
        let
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   577
          val _ = warning "Falling back on proof over dom..."
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   578
          val _ = (if length term > 1 then error "Proof over dom not supported for mutual recursive functions" else ())
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   579
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   580
          fun args (a$(Var ((nm,_),T))) = args a |> (fn ar => (nm,T)::ar)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   581
            | args (a$(Const (_,T))) = args a |> (fn ar => ("x",T)::ar)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   582
            | args _ = []
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   583
          val dom_args =
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   584
            terms |> hd |> get_l |> args
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   585
            |> Variable.variant_frees lthy []
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   586
            |> map fst
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   587
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   588
          val {inducts, ...} = case infos of SOME [i] => i | _ => error "Proof over dom failed as no induct rule was found"
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   589
          val induct = (Option.valOf inducts |> hd)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   590
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   591
          val domintros = Proof_Context.get_fact lthy (Facts.named (hd timing_names ^ ".domintros"))
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   592
          val prop = (hd timing_names ^ "_dom (" ^ (String.concatWith "," dom_args) ^ ")")
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   593
                      |> Syntax.read_prop lthy
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   594
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   595
          (* Prove a helper lemma *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   596
          val dom_lemma = Goal.prove lthy dom_args [] prop
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   597
            (fn {context, ...} => HEADGOAL (time_dom_tac context induct domintros))
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   598
          (* Add dom_lemma to simplification set *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   599
          val simp_lthy = Simplifier.add_simp dom_lemma lthy
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   600
        in
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   601
          (* Use lemma to prove termination *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   602
          Function.prove_termination NONE
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   603
            (auto_tac simp_lthy) lthy
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   604
        end
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   605
    
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   606
    (* Context for printing without showing question marks *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   607
    val print_ctxt = lthy'
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   608
      |> Config.put show_question_marks false
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   609
      |> Config.put show_sorts false (* Change it for debugging *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   610
    (* Print result if print *)
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   611
    val _ = if not print then () else
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   612
        let
80643
11b8f2e4c3d2 branches of case expressions may need to be eta-expanded
nipkow
parents: 80636
diff changeset
   613
          val nms = map (fst o dest_Const) term
11b8f2e4c3d2 branches of case expressions may need to be eta-expanded
nipkow
parents: 80636
diff changeset
   614
          val typs = map (snd o dest_Const) term
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   615
        in
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   616
          print_timing' print_ctxt { names=nms, terms=terms, typs=typs } (info_pfunc time_info)
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   617
        end
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   618
  in
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   619
    (time_info, Local_Theory.exit_global lthy')
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   620
  end
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   621
79969
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   622
fun fix_definition (Const ("Pure.eq", _) $ l $ r) = Const ("HOL.Trueprop", @{typ "bool \<Rightarrow> prop"})
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   623
      $ (Const ("HOL.eq", @{typ "bool \<Rightarrow> bool \<Rightarrow> bool"}) $ l $ r)
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   624
  | fix_definition t = t
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   625
fun check_definition [t] = [t]
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   626
  | check_definition _ = error "Only a single defnition is allowed"
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   627
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   628
(* Convert function into its timing function (called by command) *)
79969
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   629
fun reg_time_fun_cmd (funcs, thms) (theory: theory) =
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   630
let
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   631
  val ctxt = Proof_Context.init_global theory
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   632
  val fterms = map (Syntax.read_term ctxt) funcs
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   633
  val (_, lthy') = reg_and_proove_time_func theory fterms
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   634
    (case thms of NONE => get_terms theory (hd fterms)
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   635
                | SOME thms => thms |> Attrib.eval_thms ctxt |> List.map Thm.prop_of)
79969
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   636
    true
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   637
in lthy'
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   638
end
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   639
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   640
(* Convert function into its timing function (called by command) with termination proof provided by user*)
79969
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   641
fun reg_time_function_cmd (funcs, thms) (theory: theory) =
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   642
let
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   643
  val ctxt = Proof_Context.init_global theory
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   644
  val fterms = map (Syntax.read_term ctxt) funcs
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   645
  val theory = reg_time_func theory fterms
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   646
    (case thms of NONE => get_terms theory (hd fterms)
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   647
                | SOME thms => thms |> Attrib.eval_thms ctxt |> List.map Thm.prop_of)
79969
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   648
    true
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   649
in theory
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   650
end
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   651
79969
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   652
(* Convert function into its timing function (called by command) *)
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   653
fun reg_time_definition_cmd (funcs, thms) (theory: theory) =
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   654
let
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   655
  val ctxt = Proof_Context.init_global theory
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   656
  val fterms = map (Syntax.read_term ctxt) funcs
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   657
  val (_, lthy') = reg_and_proove_time_func theory fterms
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   658
    (case thms of NONE => get_terms theory (hd fterms) |> check_definition |> map fix_definition
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   659
                | SOME thms => thms |> Attrib.eval_thms ctxt |> List.map Thm.prop_of)
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   660
    true
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   661
in lthy'
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   662
end
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   663
79494
c7536609bb9b translation to time functions now with canonical let.
nipkow
parents: 79490
diff changeset
   664
val parser = (Scan.repeat1 Parse.prop) -- (Scan.option (Parse.keyword_improper "equations" -- Parse.thms1 >> snd))
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   665
79969
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   666
val _ = Outer_Syntax.command @{command_keyword "time_fun"}
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   667
  "Defines runtime function of a function"
79969
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   668
  (parser >> (fn p => Toplevel.theory (reg_time_fun_cmd p)))
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   669
79969
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   670
val _ = Outer_Syntax.command @{command_keyword "time_function"}
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   671
  "Defines runtime function of a function"
79969
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   672
  (parser >> (fn p => Toplevel.theory (reg_time_function_cmd p)))
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   673
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   674
val _ = Outer_Syntax.command @{command_keyword "time_definition"}
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   675
  "Defines runtime function of a definition"
4aeb25ba90f3 more uniform command names
nipkow
parents: 79714
diff changeset
   676
  (parser >> (fn p => Toplevel.theory (reg_time_definition_cmd p)))
79490
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   677
b287510a4202 Added time function automation
nipkow
parents:
diff changeset
   678
end