author | wenzelm |
Wed, 07 Aug 2024 12:50:22 +0200 | |
changeset 80657 | c6dca9d3af4e |
parent 80643 | 11b8f2e4c3d2 |
child 80734 | 7054a1bc8347 |
permissions | -rw-r--r-- |
79490 | 1 |
|
2 |
signature TIMING_FUNCTIONS = |
|
3 |
sig |
|
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 | 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 | 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 | 14 |
val fun_pretty': Proof.context -> pfunc -> Pretty.T |
15 |
val fun_pretty: Proof.context -> Function.info -> Pretty.T |
|
16 |
val print_timing': Proof.context -> pfunc -> pfunc -> unit |
|
17 |
val print_timing: Proof.context -> Function.info -> Function.info -> unit |
|
18 |
||
79969 | 19 |
val reg_and_proove_time_func: theory -> term list -> term list |
79490 | 20 |
-> bool -> Function.info * theory |
79969 | 21 |
val reg_time_func: theory -> term list -> term list |
22 |
-> bool -> theory |
|
79490 | 23 |
|
24 |
val time_dom_tac: Proof.context -> thm -> thm list -> int -> tactic |
|
25 |
||
26 |
end |
|
27 |
||
28 |
structure Timing_Functions : TIMING_FUNCTIONS = |
|
29 |
struct |
|
30 |
(* Configure config variable to adjust the prefix *) |
|
31 |
val bprefix = Attrib.setup_config_string @{binding "time_prefix"} (K "T_") |
|
32 |
||
33 |
(* some default values to build terms easier *) |
|
34 |
val zero = Const (@{const_name "Groups.zero"}, HOLogic.natT) |
|
35 |
val one = Const (@{const_name "Groups.one"}, HOLogic.natT) |
|
36 |
(* Extracts terms from function info *) |
|
37 |
fun terms_of_info (info: Function.info) = |
|
38 |
let |
|
39 |
val {simps, ...} = info |
|
40 |
in |
|
41 |
map Thm.prop_of (case simps of SOME s => s | NONE => error "No terms of function found in info") |
|
42 |
end; |
|
43 |
||
44 |
type pfunc = { |
|
79494
c7536609bb9b
translation to time functions now with canonical let.
nipkow
parents:
79490
diff
changeset
|
45 |
names : string list, |
79490 | 46 |
terms : term list, |
79494
c7536609bb9b
translation to time functions now with canonical let.
nipkow
parents:
79490
diff
changeset
|
47 |
typs : typ list |
79490 | 48 |
} |
49 |
fun info_pfunc (info: Function.info): pfunc = |
|
50 |
let |
|
51 |
val {defname, fs, ...} = info; |
|
52 |
val T = case hd fs of (Const (_,T)) => T | _ => error "Internal error: Invalid info to print" |
|
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 | 55 |
end |
56 |
||
57 |
(* Auxiliary functions for printing functions *) |
|
58 |
fun fun_pretty' ctxt (pfunc: pfunc) = |
|
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 | 67 |
fun separate sep prts = |
68 |
flat (Library.separate [Pretty.str sep] (map single prts)); |
|
69 |
val ptrms = (separate "\n| " (map (Syntax.pretty_term ctxt) terms)); |
|
70 |
in |
|
71 |
Pretty.text_fold (header @ ptrms) |
|
72 |
end |
|
73 |
fun fun_pretty ctxt = fun_pretty' ctxt o info_pfunc |
|
74 |
fun print_timing' ctxt (opfunc: pfunc) (tpfunc: pfunc) = |
|
75 |
let |
|
79494
c7536609bb9b
translation to time functions now with canonical let.
nipkow
parents:
79490
diff
changeset
|
76 |
val {names, ...} = opfunc; |
79490 | 77 |
val poriginal = Pretty.item [Pretty.str "Original function:\n", fun_pretty' ctxt opfunc] |
78 |
val ptiming = Pretty.item [Pretty.str ("Running time function:\n"), fun_pretty' ctxt tpfunc] |
|
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 | 81 |
end |
82 |
fun print_timing ctxt (oinfo: Function.info) (tinfo: Function.info) = |
|
83 |
print_timing' ctxt (info_pfunc oinfo) (info_pfunc tinfo) |
|
84 |
||
85 |
val If_name = @{const_name "HOL.If"} |
|
86 |
val Let_name = @{const_name "HOL.Let"} |
|
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 | 96 |
(* returns true if it's an if term *) |
97 |
fun is_if (Const (n,_)) = (n = If_name) |
|
98 |
| is_if _ = false |
|
99 |
(* returns true if it's a case term *) |
|
100 |
fun is_case (Const (n,_)) = String.isPrefix "case_" (List.last (String.fields (fn s => s = #".") n)) |
|
101 |
| is_case _ = false |
|
102 |
(* returns true if it's a let term *) |
|
103 |
fun is_let (Const (n,_)) = (n = Let_name) |
|
104 |
| is_let _ = false |
|
105 |
(* change type of original function to new type (_ \<Rightarrow> ... \<Rightarrow> _ to _ \<Rightarrow> ... \<Rightarrow> nat) |
|
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 | 114 |
(* Convert string name of function to its timing equivalent *) |
115 |
fun fun_name_to_time ctxt name = |
|
116 |
let |
|
117 |
val prefix = Config.get ctxt bprefix |
|
118 |
fun replace_last_name [n] = [prefix ^ n] |
|
119 |
| replace_last_name (n::ns) = n :: (replace_last_name ns) |
|
120 |
| replace_last_name _ = error "Internal error: Invalid function name to convert" |
|
121 |
val parts = String.fields (fn s => s = #".") name |
|
122 |
in |
|
123 |
String.concatWith "." (replace_last_name parts) |
|
124 |
end |
|
125 |
(* Count number of arguments of a function *) |
|
126 |
fun count_args (Type (n, [_,res])) = (if n = "fun" then 1 + count_args res else 0) |
|
127 |
| count_args _ = 0 |
|
128 |
(* Check if number of arguments matches function *) |
|
129 |
fun check_args s (Const (_,T), args) = |
|
130 |
(if length args = count_args T then () else error ("Partial applications/Lambdas not allowed (" ^ s ^ ")")) |
|
131 |
| check_args s (Free (_,T), args) = |
|
132 |
(if length args = count_args T then () else error ("Partial applications/Lambdas not allowed (" ^ s ^ ")")) |
|
133 |
| check_args s _ = error ("Partial applications/Lambdas not allowed (" ^ s ^ ")") |
|
134 |
(* Removes Abs *) |
|
135 |
fun rem_abs f (Abs (_,_,t)) = rem_abs f t |
|
136 |
| rem_abs f t = f t |
|
137 |
(* Map right side of equation *) |
|
138 |
fun map_r f (pT $ (eq $ l $ r)) = (pT $ (eq $ l $ f r)) |
|
139 |
| map_r _ _ = error "Internal error: No right side of equation found" |
|
140 |
(* Get left side of equation *) |
|
141 |
fun get_l (_ $ (_ $ l $ _)) = l |
|
142 |
| get_l _ = error "Internal error: No left side of equation found" |
|
143 |
(* Get right side of equation *) |
|
144 |
fun get_r (_ $ (_ $ _ $ r)) = r |
|
145 |
| get_r _ = error "Internal error: No right side of equation found" |
|
146 |
(* Return name of Const *) |
|
147 |
fun Const_name (Const (nm,_)) = SOME nm |
|
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 | 151 |
|
152 |
fun time_term ctxt (Const (nm,T)) = |
|
153 |
let |
|
154 |
val T_nm = fun_name_to_time ctxt nm |
|
155 |
val T_T = change_typ T |
|
156 |
in |
|
157 |
(SOME (Syntax.check_term ctxt (Const (T_nm,T_T)))) |
|
158 |
handle (ERROR _) => |
|
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 | 169 |
| _ => error ("Timing function of " ^ nm ^ " is not defined") |
170 |
end |
|
171 |
| time_term _ _ = error "Internal error: No valid function given" |
|
172 |
||
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 | 179 |
}; |
180 |
||
181 |
(* Walks over term and calls given converter *) |
|
182 |
fun walk_func (t1 $ t2) ts = walk_func t1 (t2::ts) |
|
183 |
| walk_func t ts = (t, ts) |
|
184 |
fun build_func (f, []) = f |
|
185 |
| build_func (f, (t::ts)) = build_func (f$t, ts) |
|
186 |
fun walk_abs (Abs (nm,T,t)) nms Ts = walk_abs t (nm::nms) (T::Ts) |
|
187 |
| walk_abs t nms Ts = (t, nms, Ts) |
|
188 |
fun build_abs t (nm::nms) (T::Ts) = build_abs (Abs (nm,T,t)) nms Ts |
|
189 |
| build_abs t [] [] = t |
|
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 | 192 |
let |
193 |
val (f, args) = walk_func t [] |
|
194 |
val this = (walk ctxt origin conv) |
|
195 |
val _ = (case f of Abs _ => error "Lambdas not supported" | _ => ()) |
|
196 |
in |
|
197 |
(if is_if f then |
|
198 |
(case f of (Const (_,T)) => |
|
199 |
(case args of [cond, t, f] => ifc ctxt origin this T cond t f |
|
200 |
| _ => error "Partial applications not supported (if)") |
|
201 |
| _ => error "Internal error: invalid if term") |
|
202 |
else if is_case f then casec ctxt origin this f args |
|
203 |
else if is_let f then |
|
204 |
(case f of (Const (_,lT)) => |
|
205 |
(case args of [exp, t] => |
|
206 |
let val (t,nms,Ts) = walk_abs t [] [] in letc ctxt origin this lT exp nms Ts t end |
|
207 |
| _ => error "Partial applications not allowed (let)") |
|
208 |
| _ => error "Internal error: invalid let term") |
|
209 |
else funcc ctxt origin this f args) |
|
210 |
end |
|
211 |
| walk ctxt origin (conv as {constc, ...}) c = |
|
212 |
constc ctxt origin (walk ctxt origin conv) c |
|
213 |
||
214 |
(* 1. Fix all terms *) |
|
215 |
(* Exchange Var in types and terms to Free *) |
|
216 |
fun fixTerms (Var(ixn,T)) = Free (fst ixn, T) |
|
217 |
| fixTerms t = t |
|
218 |
fun fixTypes (TVar ((t, _), T)) = TFree (t, T) |
|
219 |
| fixTypes t = t |
|
79542 | 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 | 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 | 228 |
| _ => error "Internal error: could not fix variable") |
79714 | 229 |
| casecAbs _ f n _ t = f (casecBuildBounds n (Term.incr_bv n 0 t)) |
79490 | 230 |
fun fixCasecCases _ _ _ [t] = [t] |
231 |
| fixCasecCases ctxt f (Type (_,[T,Tr])) (t::ts) = casecAbs ctxt f 0 T t :: fixCasecCases ctxt f Tr ts |
|
232 |
| fixCasecCases _ _ _ _ = error "Internal error: invalid case types/terms" |
|
79542 | 233 |
fun fixCasec ctxt _ f (t as Const (_,T)) args = |
234 |
(check_args "cases" (t,args); build_func (t,fixCasecCases ctxt f T args)) |
|
79490 | 235 |
| fixCasec _ _ _ _ _ = error "Internal error: invalid case term" |
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 | 238 |
let |
239 |
val _ = check_args "args" (walk_func (get_l t) []) |
|
240 |
in |
|
241 |
map_r (walk ctxt term { |
|
242 |
funcc = (fn _ => fn _ => fn f => fn t => fn args => |
|
243 |
(check_args "func" (t,args); build_func (t, map f args))), |
|
244 |
constc = (fn _ => fn _ => fn _ => fn c => (case c of Abs _ => error "Lambdas not supported" | _ => c)), |
|
245 |
ifc = (fn _ => fn _ => fn f => fn T => fn cond => fn tt => fn tf => |
|
246 |
((Const (If_name, T)) $ f cond $ (f tt) $ (f tf))), |
|
247 |
casec = fixCasec, |
|
248 |
letc = (fn _ => fn _ => fn f => fn expT => fn exp => fn nms => fn Ts => fn t => |
|
249 |
let |
|
250 |
val f' = if length nms = 0 then |
|
251 |
(case f (t$exp) of t$_ => t | _ => error "Internal error: case could not be fixed (let)") |
|
252 |
else f t |
|
79542 | 253 |
in (Const (Let_name,expT) $ (f exp) $ build_abs f' nms Ts) end) |
79490 | 254 |
}) t |
255 |
end |
|
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 | 259 |
fun or f (a,b) = f a orelse b |
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 | 262 |
constc = (K o K o K o K) false, |
263 |
ifc = (fn _ => fn _ => fn f => fn _ => fn cond => fn tt => fn tf => f cond orelse f tt orelse f tf), |
|
264 |
casec = (fn _ => fn _ => fn f => fn t => fn cs => f t orelse List.foldr (or (rem_abs f)) false cs), |
|
265 |
letc = (fn _ => fn _ => fn f => fn _ => fn exp => fn _ => fn _ => fn t => f exp orelse f t) |
|
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 | 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 | 301 |
(* 3. Convert equations *) |
302 |
(* Some Helper *) |
|
303 |
val plusTyp = @{typ "nat => nat => nat"} |
|
304 |
fun plus (SOME a) (SOME b) = SOME (Const (@{const_name "Groups.plus"}, plusTyp) $ a $ b) |
|
305 |
| plus (SOME a) NONE = SOME a |
|
306 |
| plus NONE (SOME b) = SOME b |
|
307 |
| plus NONE NONE = NONE |
|
308 |
fun opt_term NONE = HOLogic.zero |
|
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 | 312 |
|
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 | 315 |
let |
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 | 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 | 320 |
if Zero_Funcs.is_zero (Proof_Context.theory_of ctxt) (nm,T) then NONE else |
321 |
time_term ctxt func |
|
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 | 328 |
|
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 | 337 |
|
338 |
(* Handle function calls *) |
|
339 |
fun build_zero (Type ("fun", [T, R])) = Abs ("x", T, build_zero R) |
|
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 | 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 | 374 |
(map f args) |
80624
9f8034d29365
time_function T_map can now be generated automatically.
nipkow
parents:
80036
diff
changeset
|
375 |
end |
79490 | 376 |
|
377 |
(* Handle case terms *) |
|
378 |
fun casecIsCase (Type (n1, [_,Type (n2, _)])) = (n1 = "fun" andalso n2 = "fun") |
|
379 |
| casecIsCase _ = false |
|
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 | 382 |
fun casecTyp (Type (n, [T1, T2])) = |
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 | 385 |
fun casecAbs f (Abs (v,Ta,t)) = (case casecAbs f t of (nconst,t) => (nconst,Abs (v,Ta,t))) |
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 | 388 |
| casecArgs f (t::ar) = |
389 |
(case casecAbs f t of (nconst, tt) => |
|
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 | 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 | 394 |
let val (nconst, args') = casecArgs f args in |
395 |
plus |
|
79969 | 396 |
(f (List.last args)) |
79490 | 397 |
(if nconst then |
398 |
SOME (build_func (Const (t,casecTyp T), args')) |
|
399 |
else NONE) |
|
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 | 402 |
|
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 | 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 | 407 |
val tt = f tt |
408 |
val ft = f ft |
|
409 |
in |
|
79969 | 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 | 412 |
(SOME ((Const (If_name, @{typ "bool \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"})) $ rcond $ (opt_term tt) $ (opt_term ft)))) |
79490 | 413 |
end |
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 | 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 | 419 |
(if length nms = 0 (* In case of "length nms = 0" the expression got reducted |
420 |
Here we need Bound 0 to gain non-partial application *) |
|
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 | 423 |
(* Expression is not used and can therefore let be dropped *) |
424 |
| SOME t' => SOME t' |
|
425 |
| NONE => NONE) |
|
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 | 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 | 430 |
|
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 | 433 |
constc = fn _ => fn _ => fn _ => fn t => |
434 |
(case t of Const ("HOL.undefined", _) => SOME (Const ("HOL.undefined", @{typ "nat"})) |
|
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 | 437 |
ifc = ifc, |
438 |
casec = casec, |
|
439 |
letc = letc |
|
440 |
} |
|
79665 | 441 |
fun top_converter is_rec _ _ = opt_term o (fn exp => plus exp (if is_rec then SOME one else NONE)) |
79490 | 442 |
|
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 | 446 |
|
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 | 456 |
pT |
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 | 462 |
|
463 |
(* 4. Tactic to prove "f_dom n" *) |
|
464 |
fun time_dom_tac ctxt induct_rule domintros = |
|
465 |
(Induction.induction_tac ctxt true [] [[]] [] (SOME [induct_rule]) [] |
|
466 |
THEN_ALL_NEW ((K (auto_tac ctxt)) THEN' (fn i => FIRST' ( |
|
467 |
(if i <= length domintros then [Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN ctxt [List.nth (domintros, i-1)]] else []) @ |
|
468 |
[Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN ctxt domintros]) i))) |
|
469 |
||
470 |
||
471 |
fun get_terms theory (term: term) = |
|
472 |
Spec_Rules.retrieve_global theory term |
|
473 |
|> hd |> #rules |
|
474 |
|> map Thm.prop_of |
|
475 |
handle Empty => error "Function or terms of function not found" |
|
476 |
||
477 |
(* Register timing function of a given function *) |
|
79969 | 478 |
fun reg_and_proove_time_func (theory: theory) (term: term list) (terms: term list) print = |
479 |
reg_time_func theory term terms false |
|
79490 | 480 |
|> proove_termination term terms print |
79969 | 481 |
and reg_time_func (theory: theory) (term: term list) (terms: term list) print = |
79490 | 482 |
let |
483 |
val lthy = Named_Target.theory_init theory |
|
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 | 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 | 488 |
| NONE => () |
489 |
||
490 |
(* 1. Fix all terms *) |
|
491 |
(* Exchange Var in types and terms to Free and check constraints *) |
|
79969 | 492 |
val terms = map |
79542 | 493 |
(map_aterms fixTerms |
494 |
#> map_types (map_atyps fixTypes) |
|
495 |
#> fixPartTerms lthy term) |
|
496 |
terms |
|
79490 | 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 | 500 |
val is_rec = is_rec lthy term terms |
501 |
||
502 |
(* 3. Convert every equation |
|
503 |
- Change type of toplevel equation from _ \<Rightarrow> _ \<Rightarrow> bool to nat \<Rightarrow> nat \<Rightarrow> bool |
|
504 |
- On left side change name of function to timing function |
|
505 |
- Convert right side of equation with conversion schema |
|
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 | 517 |
|
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 | 522 |
fun pat_completeness_auto ctxt = |
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 | 525 |
|
526 |
(* For partial functions sequential=true is needed in order to support them |
|
527 |
We need sequential=false to support the automatic proof of termination over dom |
|
528 |
*) |
|
529 |
fun register seq = |
|
530 |
let |
|
531 |
val _ = (if seq then warning "Falling back on sequential function..." else ()) |
|
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 | 534 |
in |
535 |
Function.add_function bindings specs fun_config pat_completeness_auto lthy |
|
536 |
end |
|
537 |
||
538 |
(* Context for printing without showing question marks *) |
|
539 |
val print_ctxt = lthy |
|
540 |
|> Config.put show_question_marks false |
|
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 | 543 |
(* Print result if print *) |
544 |
val _ = if not print then () else |
|
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 | 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 | 551 |
end |
552 |
||
553 |
(* Register function *) |
|
554 |
val (_, lthy) = |
|
555 |
register false |
|
556 |
handle (ERROR _) => |
|
557 |
register true |
|
558 |
| Match => |
|
559 |
register true |
|
560 |
in |
|
561 |
Local_Theory.exit_global lthy |
|
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 | 564 |
let |
565 |
val lthy = Named_Target.theory_init theory |
|
566 |
||
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 | 570 |
|
571 |
(* Proof by lexicographic_order_tac *) |
|
572 |
val (time_info, lthy') = |
|
573 |
(Function.prove_termination NONE |
|
574 |
(Lexicographic_Order.lexicographic_order_tac false lthy) lthy) |
|
575 |
handle (ERROR _) => |
|
576 |
let |
|
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 | 580 |
fun args (a$(Var ((nm,_),T))) = args a |> (fn ar => (nm,T)::ar) |
581 |
| args (a$(Const (_,T))) = args a |> (fn ar => ("x",T)::ar) |
|
582 |
| args _ = [] |
|
583 |
val dom_args = |
|
584 |
terms |> hd |> get_l |> args |
|
585 |
|> Variable.variant_frees lthy [] |
|
586 |
|> map fst |
|
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 | 589 |
val induct = (Option.valOf inducts |> hd) |
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 | 593 |
|> Syntax.read_prop lthy |
594 |
||
595 |
(* Prove a helper lemma *) |
|
596 |
val dom_lemma = Goal.prove lthy dom_args [] prop |
|
597 |
(fn {context, ...} => HEADGOAL (time_dom_tac context induct domintros)) |
|
598 |
(* Add dom_lemma to simplification set *) |
|
599 |
val simp_lthy = Simplifier.add_simp dom_lemma lthy |
|
600 |
in |
|
601 |
(* Use lemma to prove termination *) |
|
602 |
Function.prove_termination NONE |
|
603 |
(auto_tac simp_lthy) lthy |
|
604 |
end |
|
605 |
||
606 |
(* Context for printing without showing question marks *) |
|
607 |
val print_ctxt = lthy' |
|
608 |
|> Config.put show_question_marks false |
|
609 |
|> Config.put show_sorts false (* Change it for debugging *) |
|
610 |
(* Print result if print *) |
|
611 |
val _ = if not print then () else |
|
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 | 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 | 617 |
end |
618 |
in |
|
619 |
(time_info, Local_Theory.exit_global lthy') |
|
620 |
end |
|
621 |
||
79969 | 622 |
fun fix_definition (Const ("Pure.eq", _) $ l $ r) = Const ("HOL.Trueprop", @{typ "bool \<Rightarrow> prop"}) |
623 |
$ (Const ("HOL.eq", @{typ "bool \<Rightarrow> bool \<Rightarrow> bool"}) $ l $ r) |
|
624 |
| fix_definition t = t |
|
625 |
fun check_definition [t] = [t] |
|
626 |
| check_definition _ = error "Only a single defnition is allowed" |
|
627 |
||
79490 | 628 |
(* Convert function into its timing function (called by command) *) |
79969 | 629 |
fun reg_time_fun_cmd (funcs, thms) (theory: theory) = |
79490 | 630 |
let |
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 | 635 |
| SOME thms => thms |> Attrib.eval_thms ctxt |> List.map Thm.prop_of) |
79969 | 636 |
true |
79490 | 637 |
in lthy' |
638 |
end |
|
639 |
||
640 |
(* Convert function into its timing function (called by command) with termination proof provided by user*) |
|
79969 | 641 |
fun reg_time_function_cmd (funcs, thms) (theory: theory) = |
79490 | 642 |
let |
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 | 647 |
| SOME thms => thms |> Attrib.eval_thms ctxt |> List.map Thm.prop_of) |
79969 | 648 |
true |
79490 | 649 |
in theory |
650 |
end |
|
651 |
||
79969 | 652 |
(* Convert function into its timing function (called by command) *) |
653 |
fun reg_time_definition_cmd (funcs, thms) (theory: theory) = |
|
654 |
let |
|
655 |
val ctxt = Proof_Context.init_global theory |
|
656 |
val fterms = map (Syntax.read_term ctxt) funcs |
|
657 |
val (_, lthy') = reg_and_proove_time_func theory fterms |
|
658 |
(case thms of NONE => get_terms theory (hd fterms) |> check_definition |> map fix_definition |
|
659 |
| SOME thms => thms |> Attrib.eval_thms ctxt |> List.map Thm.prop_of) |
|
660 |
true |
|
661 |
in lthy' |
|
662 |
end |
|
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 | 665 |
|
79969 | 666 |
val _ = Outer_Syntax.command @{command_keyword "time_fun"} |
79490 | 667 |
"Defines runtime function of a function" |
79969 | 668 |
(parser >> (fn p => Toplevel.theory (reg_time_fun_cmd p))) |
79490 | 669 |
|
79969 | 670 |
val _ = Outer_Syntax.command @{command_keyword "time_function"} |
79490 | 671 |
"Defines runtime function of a function" |
79969 | 672 |
(parser >> (fn p => Toplevel.theory (reg_time_function_cmd p))) |
673 |
||
674 |
val _ = Outer_Syntax.command @{command_keyword "time_definition"} |
|
675 |
"Defines runtime function of a definition" |
|
676 |
(parser >> (fn p => Toplevel.theory (reg_time_definition_cmd p))) |
|
79490 | 677 |
|
678 |
end |