author  krauss 
Wed, 05 Dec 2007 14:36:58 +0100  
changeset 25545  21cd20c1ce98 
parent 25538  58e8ba3b792b 
child 26529  03ad378ed5f0 
permissions  rwrr 
21131  1 
(* Title: HOL/Tools/function_package/lexicographic_order.ML 
21201  2 
ID: $Id$ 
21131  3 
Author: Lukas Bulwahn, TU Muenchen 
4 

5 
Method for termination proofs with lexicographic orderings. 

6 
*) 

7 

8 
signature LEXICOGRAPHIC_ORDER = 

9 
sig 

23056  10 
val lexicographic_order : thm list > Proof.context > Method.method 
21510
7e72185e4b24
exported mk_base_funs for use by sizechange tools
krauss
parents:
21319
diff
changeset

11 

7e72185e4b24
exported mk_base_funs for use by sizechange tools
krauss
parents:
21319
diff
changeset

12 
(* exported for use by sizechange termination prototype. 
7e72185e4b24
exported mk_base_funs for use by sizechange tools
krauss
parents:
21319
diff
changeset

13 
FIXME: provide a common interface later *) 
23074  14 
val mk_base_funs : theory > typ > term list 
22309  15 
(* exported for debugging *) 
21237  16 
val setup: theory > theory 
21131  17 
end 
18 

19 
structure LexicographicOrder : LEXICOGRAPHIC_ORDER = 

20 
struct 

21 

25509
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

22 
(** Userdeclared size functions **) 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

23 

e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

24 
structure SizeFunsData = GenericDataFun 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

25 
( 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

26 
type T = term NetRules.T; 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

27 
val empty = NetRules.init (op aconv) I 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

28 
val copy = I 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

29 
val extend = I 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

30 
fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2) 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

31 
); 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

32 

e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

33 
fun add_sfun f ctxt = 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

34 
SizeFunsData.map (NetRules.insert (singleton (Variable.polymorphic (Context.proof_of ctxt)) f)) ctxt 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

35 
val add_sfun_attr = Attrib.syntax (Args.term >> (fn f => Thm.declaration_attribute (K (add_sfun f)))) 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

36 

e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

37 
fun get_sfuns T thy = 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

38 
map_filter (fn f => SOME (Envir.subst_TVars (Type.typ_match (Sign.tsig_of thy) 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

39 
(domain_type (fastype_of f), T) 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

40 
Vartab.empty) 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

41 
f) 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

42 
handle Type.TYPE_MATCH => NONE) 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

43 
(NetRules.rules (SizeFunsData.get (Context.Theory thy))) 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

44 

23074  45 
(** General stuff **) 
46 

47 
fun mk_measures domT mfuns = 

24576
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset

48 
let 
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset

49 
val relT = HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) 
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset

50 
val mlexT = (domT > HOLogic.natT) > relT > relT 
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset

51 
fun mk_ms [] = Const (@{const_name "{}"}, relT) 
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset

52 
 mk_ms (f::fs) = 
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset

53 
Const (@{const_name "Wellfounded_Relations.mlex_prod"}, mlexT) $ f $ mk_ms fs 
23074  54 
in 
24576
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset

55 
mk_ms mfuns 
23074  56 
end 
57 

58 
fun del_index n [] = [] 

59 
 del_index n (x :: xs) = 

23633  60 
if n > 0 then x :: del_index (n  1) xs else xs 
21131  61 

62 
fun transpose ([]::_) = [] 

63 
 transpose xss = map hd xss :: transpose (map tl xss) 

64 

23074  65 
(** Matrix cell datatype **) 
66 

24576
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset

67 
datatype cell = Less of thm LessEq of (thm * thm)  None of (thm * thm)  False of thm; 
23633  68 

23074  69 
fun is_Less (Less _) = true 
70 
 is_Less _ = false 

23633  71 

23074  72 
fun is_LessEq (LessEq _) = true 
73 
 is_LessEq _ = false 

23633  74 

75 
fun thm_of_cell (Less thm) = thm 

76 
 thm_of_cell (LessEq (thm, _)) = thm 

77 
 thm_of_cell (False thm) = thm 

78 
 thm_of_cell (None (thm, _)) = thm 

79 

23437  80 
fun pr_cell (Less _ ) = " < " 
23633  81 
 pr_cell (LessEq _) = " <=" 
23437  82 
 pr_cell (None _) = " ? " 
83 
 pr_cell (False _) = " F " 

23074  84 

85 

86 
(** Generating Measure Functions **) 

87 

23633  88 
fun mk_comp g f = 
89 
let 

90 
val fT = fastype_of f 

23074  91 
val gT as (Type ("fun", [xT, _])) = fastype_of g 
92 
val comp = Abs ("f", fT, Abs ("g", gT, Abs ("x", xT, Bound 2 $ (Bound 1 $ Bound 0)))) 

93 
in 

94 
Envir.beta_norm (comp $ f $ g) 

95 
end 

96 

97 
fun mk_base_funs thy (T as Type("*", [fT, sT])) = (* products *) 

98 
map (mk_comp (Const ("fst", T > fT))) (mk_base_funs thy fT) 

99 
@ map (mk_comp (Const ("snd", T > sT))) (mk_base_funs thy sT) 

22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset

100 

23074  101 
 mk_base_funs thy T = (* default: size function, if available *) 
102 
if Sorts.of_sort (Sign.classes_of thy) (T, [HOLogic.class_size]) 

25509
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

103 
then (HOLogic.size_const T) :: get_sfuns T thy 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

104 
else get_sfuns T thy 
23074  105 

106 
fun mk_sum_case f1 f2 = 

107 
let 

23633  108 
val Type ("fun", [fT, Q]) = fastype_of f1 
23074  109 
val Type ("fun", [sT, _]) = fastype_of f2 
110 
in 

111 
Const (@{const_name "Sum_Type.sum_case"}, (fT > Q) > (sT > Q) > Type("+", [fT, sT]) > Q) $ f1 $ f2 

112 
end 

23633  113 

23074  114 
fun constant_0 T = Abs ("x", T, HOLogic.zero) 
115 
fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero) 

22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset

116 

23074  117 
fun mk_funorder_funs (Type ("+", [fT, sT])) = 
118 
map (fn m => mk_sum_case m (constant_0 sT)) (mk_funorder_funs fT) 

119 
@ map (fn m => mk_sum_case (constant_0 fT) m) (mk_funorder_funs sT) 

23633  120 
 mk_funorder_funs T = [ constant_1 T ] 
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset

121 

23074  122 
fun mk_ext_base_funs thy (Type("+", [fT, sT])) = 
25538  123 
map_product mk_sum_case (mk_ext_base_funs thy fT) (mk_ext_base_funs thy sT) 
23074  124 
 mk_ext_base_funs thy T = mk_base_funs thy T 
125 

126 
fun mk_all_measure_funs thy (T as Type ("+", _)) = 

127 
mk_ext_base_funs thy T @ mk_funorder_funs T 

128 
 mk_all_measure_funs thy T = mk_base_funs thy T 

129 

130 

131 
(** Proof attempts to build the matrix **) 

23633  132 

21131  133 
fun dest_term (t : term) = 
134 
let 

23074  135 
val (vars, prop) = FundefLib.dest_all_all t 
21237  136 
val prems = Logic.strip_imp_prems prop 
23074  137 
val (lhs, rhs) = Logic.strip_imp_concl prop 
23633  138 
> HOLogic.dest_Trueprop 
23074  139 
> HOLogic.dest_mem > fst 
23633  140 
> HOLogic.dest_prod 
21131  141 
in 
23074  142 
(vars, prems, lhs, rhs) 
21131  143 
end 
23633  144 

21131  145 
fun mk_goal (vars, prems, lhs, rhs) rel = 
23633  146 
let 
21237  147 
val concl = HOLogic.mk_binrel rel (lhs, rhs) > HOLogic.mk_Trueprop 
23633  148 
in 
149 
Logic.list_implies (prems, concl) 

23074  150 
> fold_rev FundefLib.mk_forall vars 
21131  151 
end 
23633  152 

153 
fun prove thy solve_tac t = 

154 
cterm_of thy t > Goal.init 

23055
34158639dc12
Method "lexicographic_order" now takes the same arguments as "auto"
krauss
parents:
22997
diff
changeset

155 
> SINGLE solve_tac > the 
23633  156 

157 
fun mk_cell (thy : theory) solve_tac (vars, prems, lhs, rhs) mfun = 

158 
let 

159 
val goals = mk_goal (vars, prems, mfun $ lhs, mfun $ rhs) 

23881  160 
val less_thm = goals @{const_name HOL.less} > prove thy solve_tac 
21131  161 
in 
21237  162 
if Thm.no_prems less_thm then 
163 
Less (Goal.finish less_thm) 

164 
else 

165 
let 

23881  166 
val lesseq_thm = goals @{const_name HOL.less_eq} > prove thy solve_tac 
21237  167 
in 
168 
if Thm.no_prems lesseq_thm then 

23437  169 
LessEq (Goal.finish lesseq_thm, less_thm) 
23633  170 
else 
21237  171 
if prems_of lesseq_thm = [HOLogic.Trueprop $ HOLogic.false_const] then False lesseq_thm 
23437  172 
else None (lesseq_thm, less_thm) 
21237  173 
end 
21131  174 
end 
23074  175 

176 

177 
(** Search algorithms **) 

22309  178 

23074  179 
fun check_col ls = forall (fn c => is_Less c orelse is_LessEq c) ls andalso not (forall (is_LessEq) ls) 
22309  180 

23074  181 
fun transform_table table col = table > filter_out (fn x => is_Less (nth x col)) > map (del_index col) 
22309  182 

23074  183 
fun transform_order col order = map (fn x => if x >= col then x + 1 else x) order 
23633  184 

21131  185 
(* simple depthfirst search algorithm for the table *) 
186 
fun search_table table = 

187 
case table of 

21237  188 
[] => SOME [] 
189 
 _ => 

190 
let 

191 
val col = find_index (check_col) (transpose table) 

192 
in case col of 

23633  193 
~1 => NONE 
21237  194 
 _ => 
195 
let 

22309  196 
val order_opt = (table, col) > transform_table > search_table 
21237  197 
in case order_opt of 
198 
NONE => NONE 

23074  199 
 SOME order =>SOME (col :: transform_order col order) 
21237  200 
end 
201 
end 

22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset

202 

23633  203 
(* find all positions of elements in a list *) 
23074  204 
fun find_index_list P = 
205 
let fun find _ [] = [] 

206 
 find n (x :: xs) = if P x then n :: find (n + 1) xs else find (n + 1) xs 

207 
in find 0 end 

22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset

208 

23633  209 
(* simple breadthfirst search algorithm for the table *) 
22309  210 
fun bfs_search_table nodes = 
211 
case nodes of 

23633  212 
[] => sys_error "INTERNAL ERROR IN lexicographic order termination tactic  fun search_table (breadth search finished)" 
22309  213 
 (node::rnodes) => let 
23633  214 
val (order, table) = node 
22309  215 
in 
216 
case table of 

23074  217 
[] => SOME (foldr (fn (c, order) => c :: transform_order c order) [] (rev order)) 
22309  218 
 _ => let 
23633  219 
val cols = find_index_list (check_col) (transpose table) 
22309  220 
in 
221 
case cols of 

23633  222 
[] => NONE 
223 
 _ => let 

224 
val newtables = map (transform_table table) cols 

23074  225 
val neworders = map (fn c => c :: order) cols 
22309  226 
val newnodes = neworders ~~ newtables 
227 
in 

228 
bfs_search_table (rnodes @ newnodes) 

23633  229 
end 
22309  230 
end 
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset

231 
end 
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset

232 

23633  233 
fun nsearch_table table = bfs_search_table [([], table)] 
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset

234 

23074  235 
(** Proof Reconstruction **) 
236 

237 
(* prove row :: cell list > tactic *) 

238 
fun prove_row (Less less_thm :: _) = 

24576
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset

239 
(rtac @{thm "mlex_less"} 1) 
24977
9f98751c9628
replaced (flip Thm.implies_elim) by Thm.elim_implies;
wenzelm
parents:
24961
diff
changeset

240 
THEN PRIMITIVE (Thm.elim_implies less_thm) 
23437  241 
 prove_row (LessEq (lesseq_thm, _) :: tail) = 
24576
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset

242 
(rtac @{thm "mlex_leq"} 1) 
24977
9f98751c9628
replaced (flip Thm.implies_elim) by Thm.elim_implies;
wenzelm
parents:
24961
diff
changeset

243 
THEN PRIMITIVE (Thm.elim_implies lesseq_thm) 
23074  244 
THEN prove_row tail 
245 
 prove_row _ = sys_error "lexicographic_order" 

246 

247 

248 
(** Error reporting **) 

249 

250 
fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table)) 

23633  251 

252 
fun pr_goals ctxt st = 

24961  253 
Display.pretty_goals_aux (Syntax.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st 
23437  254 
> Pretty.chunks 
255 
> Pretty.string_of 

256 

257 
fun row_index i = chr (i + 97) 

258 
fun col_index j = string_of_int (j + 1) 

259 

23633  260 
fun pr_unprovable_cell _ ((i,j), Less _) = "" 
261 
 pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) = 

262 
"(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st 

263 
 pr_unprovable_cell ctxt ((i,j), None (st_less, st_leq)) = 

264 
"(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st_less 

265 
^ "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ pr_goals ctxt st_leq 

266 
 pr_unprovable_cell ctxt ((i,j), False st) = 

267 
"(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st 

23437  268 

23633  269 
fun pr_unprovable_subgoals ctxt table = 
23437  270 
table 
271 
> map_index (fn (i,cs) => map_index (fn (j,x) => ((i,j), x)) cs) 

272 
> flat 

23633  273 
> map (pr_unprovable_cell ctxt) 
23437  274 

23633  275 
fun no_order_msg ctxt table tl measure_funs = 
276 
let 

24920  277 
val prterm = Syntax.string_of_term ctxt 
23633  278 
fun pr_fun t i = string_of_int i ^ ") " ^ prterm t 
23074  279 

23633  280 
fun pr_goal t i = 
23074  281 
let 
23633  282 
val (_, _, lhs, rhs) = dest_term t 
23074  283 
in (* also show prems? *) 
23128  284 
i ^ ") " ^ prterm rhs ^ " ~> " ^ prterm lhs 
23074  285 
end 
286 

287 
val gc = map (fn i => chr (i + 96)) (1 upto length table) 

288 
val mc = 1 upto length measure_funs 

23437  289 
val tstr = "Result matrix:" :: " " ^ concat (map (enclose " " " " o string_of_int) mc) 
23074  290 
:: map2 (fn r => fn i => i ^ ": " ^ concat (map pr_cell r)) table gc 
23437  291 
val gstr = "Calls:" :: map2 (prefix " " oo pr_goal) tl gc 
292 
val mstr = "Measures:" :: map2 (prefix " " oo pr_fun) measure_funs mc 

23633  293 
val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals ctxt table 
21131  294 
in 
23437  295 
cat_lines (ustr @ gstr @ mstr @ tstr @ ["", "Could not find lexicographic termination order."]) 
21131  296 
end 
23633  297 

23074  298 
(** The Main Function **) 
23633  299 
fun lexicographic_order_tac ctxt solve_tac (st: thm) = 
21131  300 
let 
21237  301 
val thy = theory_of_thm st 
23074  302 
val ((trueprop $ (wf $ rel)) :: tl) = prems_of st 
303 

304 
val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel)) 

305 

306 
val measure_funs = mk_all_measure_funs thy domT (* 1: generate measures *) 

23633  307 

23074  308 
(* 2: create table *) 
309 
val table = map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl 

310 

311 
val order = the (search_table table) (* 3: search table *) 

23633  312 
handle Option => error (no_order_msg ctxt table tl measure_funs) 
23074  313 

21237  314 
val clean_table = map (fn x => map (nth x) order) table 
23074  315 

316 
val relation = mk_measures domT (map (nth measure_funs) order) 

24920  317 
val _ = writeln ("Found termination order: " ^ quote (Syntax.string_of_term ctxt relation)) 
23074  318 

319 
in (* 4: proof reconstruction *) 

320 
st > (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)]) 

24576
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset

321 
THEN (REPEAT (rtac @{thm "wf_mlex"} 1)) 
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset

322 
THEN (rtac @{thm "wf_empty"} 1) 
23074  323 
THEN EVERY (map prove_row clean_table)) 
21131  324 
end 
325 

25545
21cd20c1ce98
methods "relation" and "lexicographic_order" do not insist on applying the "f.termination" rule of a function.
krauss
parents:
25538
diff
changeset

326 
fun lexicographic_order thms ctxt = 
21cd20c1ce98
methods "relation" and "lexicographic_order" do not insist on applying the "f.termination" rule of a function.
krauss
parents:
25538
diff
changeset

327 
Method.SIMPLE_METHOD (TRY (FundefCommon.apply_termination_rule ctxt 1) 
21cd20c1ce98
methods "relation" and "lexicographic_order" do not insist on applying the "f.termination" rule of a function.
krauss
parents:
25538
diff
changeset

328 
THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt))) 
21201  329 

23633  330 
val setup = Method.add_methods [("lexicographic_order", Method.bang_sectioned_args clasimp_modifiers lexicographic_order, 
23055
34158639dc12
Method "lexicographic_order" now takes the same arguments as "auto"
krauss
parents:
22997
diff
changeset

331 
"termination prover for lexicographic orderings")] 
25509
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

332 
#> Attrib.add_attributes [("measure_function", add_sfun_attr, "declare custom measure function")] 
21131  333 

21590  334 
end 