1(*****************************************************************************) 2(* File: testEncode.sml *) 3(* Author: James Reynolds *) 4(* *) 5(* Runs some simple tests of encodeLib *) 6(*****************************************************************************) 7 8quietdec := true; 9 10val _ = loadPath := "../ml/" :: !loadPath; 11 12load "encodeLib"; 13open encodeLib arithmeticTheory listTheory; 14 15quietdec := false; 16 17(*****************************************************************************) 18(* Some simple tests of different data types *) 19(*****************************************************************************) 20 21val _ = Hol_datatype `test1 = Pair of 'a # 'b`; 22val _ = Hol_datatype `test2 = Curry of 'a => 'b`; 23val _ = Hol_datatype `test2b = Curry3 of 'a => 'b => 'c`; 24val _ = Hol_datatype `test2c = Curry2 of 'a => 'b # 'c`; 25val _ = Hol_datatype `test3 = Sum1 of 'a | Sum2 of 'b`; 26val _ = Hol_datatype `test4 = Recursive of test4 | End`; 27val _ = Hol_datatype `test5 = RecursiveList of test5 list | EndList`; 28val _ = Hol_datatype `test6 = DoubleList of test6 list => test6 list | EndD`; 29val _ = Hol_datatype `test7 = Node of test7 # test7 | Leaf of 'a`; 30val _ = Hol_datatype `test8 = Double of test8 test7 # test8 list | End8`; 31val _ = Hol_datatype `test9l = R9 of test9r | EndL ; 32 test9r = L9 of test9l | EndR`; 33val _ = Hol_datatype `testA = <| Reg1 : num; Reg2 : num; Waiting : bool |>`; 34val _ = Hol_datatype `testBa = Aa of num | Ba of testBb | Ca of testBc ; 35 testBb = Bb of int | Ab of testBa | Cb of testBc ; 36 testBc = Cc of rat | Bc of testBb | Ac of testBa`; 37val _ = Hol_datatype `labels = l1 | l2 | l3 | l4 | l5`; 38val _ = Hol_datatype `noalpha = CurryNA of num => num => num # num`; 39val _ = Hol_datatype `threecons = ConsNone 40 | CurryTC of 'a => 'b => 'c 41 | CurryNTC of num => num => num # num`; 42val _ = Hol_datatype `rose_tree = Branch of ('a # rose_tree) list`; 43val _ = Hol_datatype `mlistL = Left of 'a => mlistR | endL ; 44 mlistR = Right of 'b => mlistL | endR`; 45 46 47(*****************************************************************************) 48(* Black - Red trees *) 49(*****************************************************************************) 50 51val _ = Hol_datatype `colour = R | B`; 52val _ = Hol_datatype `tree = LEAF | NODE of colour => num => tree => tree`; 53 54(*****************************************************************************) 55(* Some examples from src/datatype/jrh.test *) 56(*****************************************************************************) 57 58val _ = Hol_datatype `One = Single_contructor`; 59 60val _ = Hol_datatype 61 `Term = Var of 'A => 'B 62 | App of bool => Termlist; 63 Termlist = Emp 64 | Consp of Term => Termlist`; 65 66val _ = Hol_datatype 67 `List = Nil 68 | Cons of 'A => List`;; 69 70val _ = Hol_datatype 71 `Btree = Lf of 'A 72 | Nd of 'B => Btree => Btree`;; 73 74val _ = Hol_datatype 75 `Command = Assign of num => Express 76 | If of Express => Command 77 | Ite of Express => Command => Command 78 | While of Express => Command 79 | Do of Command => Express; 80 81 Express = Constant of num 82 | Variable of num 83 | Summ of Express => Express 84 | Product of Express => Express`; 85 86val _ = Hol_datatype 87 `atexp = Varb of num 88 | Let of dec => exp; 89 90 exp = Exp1 of atexp 91 | Exp2 of exp => atexp 92 | Exp3 of match; 93 94 match = Match1 of rule 95 | Matches of rule => match; 96 97 rule = Rule of pat => exp; 98 dec = Val of valbind 99 | Local of dec => dec 100 | Decs of dec => dec; 101 102 valbind = Single of pat => exp 103 | Multi of pat => exp => valbind 104 | Rec of valbind; 105 106 pat = Wild 107 | Varpat of num`; 108 109val _ = Hol_datatype 110 `tri = ONE | TWO | THREE`; 111 112Hol_datatype 113 `Steve0 = X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | 114 X11 | X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | 115 X21 | X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | 116 X31 | X32 | X33 | X34`;; 117 118Hol_datatype 119 `TY1 = NoF__ 120 | Fk__ of 'A => TY2; 121 122 TY2 = Ta__ of bool 123 | Td__ of bool 124 | Tf__ of TY1 125 | Tk__ of bool 126 | Tp__ of bool 127 | App__ of 'A => TY1 => TY2 => TY3 128 | Pair__ of TY2 => TY2; 129 130 TY3 = NoS__ 131 | Fresh__ of TY2 132 | Trustworthy__ of 'A 133 | PrivateKey__ of 'A => 'B => 'C 134 | PublicKey__ of 'A => 'B => 'C 135 | Conveyed__ of 'A => TY2 136 | Possesses__ of 'A => TY2 137 | Received__ of 'A => TY2 138 | Recognizes__ of 'A => TY2 139 | Sends__ of 'A => TY2 => 'B 140 | SharedSecret__ of 'A => TY2 => 'B 141 | Believes__ of 'A => TY3 142 | And__ of TY3 => TY3 143 | NeverMalFromSelf__ of 'A => 'B => TY2`;; 144 145(*****************************************************************************) 146(* Example from Myra: part of the syntax of SML. *) 147(*****************************************************************************) 148 149Hol_datatype 150 `String = EMPTY_STRING 151 | CONS_STRING of num => String`; 152 153Hol_datatype 154 `strid = STRID of String; 155 var = VAR of String; 156 con = CON of String; 157 scon = SCINT of num (* was int *) 158 | SCSTR of String; 159 excon = EXCON of String; 160 label = LABEL of String`;; 161 162Hol_datatype 163 `nonemptylist = Head_and_tail of 'A => 'A list`;; 164 165Hol_datatype 166 `long = BASE of 'A | QUALIFIED of strid => long`;; 167 168 169(* runtime on sole: 1251.940s, gctime: 176.740s, systime: 1.080s. *) 170 171Hol_datatype 172 `atpat_e = WILDCARDatpat_e 173 | SCONatpat_e of scon 174 | VARatpat_e of var 175 | CONatpat_e of con long 176 | EXCONatpat_e of excon long 177 | RECORDatpat_e of patrow_e option 178 | PARatpat_e of pat_e; 179 180 patrow_e = DOTDOTDOT_e 181 | PATROW_e of num => pat_e => patrow_e option; 182 183 pat_e = ATPATpat_e of atpat_e 184 | CONpat_e of con long => atpat_e 185 | EXCONpat_e of excon long => atpat_e 186 | LAYEREDpat_e of var => pat_e; 187 188 conbind_e = CONBIND_e of con => conbind_e option; 189 190 datbind_e = DATBIND_e of conbind_e => datbind_e option; 191 192 exbind_e = EXBIND1_e of excon => exbind_e option 193 | EXBIND2_e of excon => excon long => exbind_e option; 194 195 atexp_e = SCONatexp_e of scon 196 | VARatexp_e of var long 197 | CONatexp_e of con long 198 | EXCONatexp_e of excon long 199 | RECORDatexp_e of exprow_e option 200 | LETatexp_e of dec_e => exp_e 201 | PARatexp_e of exp_e; 202 203 exprow_e = EXPROW_e of num => exp_e => exprow_e option; 204 205 exp_e = ATEXPexp_e of atexp_e 206 | APPexp_e of exp_e => atexp_e 207 | HANDLEexp_e of exp_e => match_e 208 | RAISEexp_e of exp_e 209 | FNexp_e of match_e; 210 211 match_e = MATCH_e of mrule_e => match_e option; 212 213 mrule_e = MRULE_e of pat_e => exp_e; 214 215 dec_e = VALdec_e of valbind_e 216 | DATATYPEdec_e of datbind_e 217 | ABSTYPEdec_e of datbind_e => dec_e 218 | EXCEPTdec_e of exbind_e 219 | LOCALdec_e of dec_e => dec_e 220 | OPENdec_e of (strid long) nonemptylist 221 | EMPTYdec_e 222 | SEQdec_e of dec_e => dec_e; 223 224 valbind_e = PLAINvalbind_e of pat_e => exp_e => valbind_e option 225 | RECvalbind_e of valbind_e`;; 226 227set_trace "EncodeLib.TypeEncoding" 1; 228 229val types = [``:('a,'b) test1``,``:('a,'b) test2``,``:('a,'b,'c) test2b``,``:('a,'b,'c) test2c``,``:('a,'b) test3``,``:labels``,``:noalpha``,``:('a,'b,'c) threecons``, 230 ``:test4``,``:test5``,``:test6``,``:test8``,``:'a test7``,``:test9l``,``:test9r``,``:'a rose_tree``,``:testBa``,``:('a,'b) mlistL``,``:tree``, 231 ``:One``,``:('a,'b) Term``,``:'a List``,``:('a,'b) Btree``,``:Command``,``:tri``,``:exp``,``:Steve0``,``:('a,'b,'c) TY1``,``:atpat_e``]; 232 233fun test_types types = 234let fun timeit t = 235 let val _ = print "Encoding Type: " 236 val _ = print_type t 237 val _ = print "\n" 238 val start = Time.now() 239 val res = encode_type t 240 in 241 (print ("Time taken: " ^ (Time.toString (Time.- (Time.now(),start)) handle e => "0.000") ^ "s\n\n") ; res) 242 end; 243 val (passed,failed) = partition (can timeit) types 244 fun concat f [] = "" 245 | concat f [x] = f x 246 | concat f (x::xs) = (f x) ^ "," ^ (concat f xs) 247 val _ = print ("Passed: [" ^ (concat type_to_string passed) ^ "]\n") 248 val _ = print ("Failed: [" ^ (concat type_to_string failed) ^ "]\n") 249in 250 (print "\nTheorems:\n" ; 251 app (fn x => ( print_thm (get_encode_decode_thm x) ; print "\n" ; 252 print_thm (get_decode_encode_thm x) ; print "\n" ; 253 print_thm (get_detect_encode_thm x) ; print "\n\n")) passed) 254end; 255 256time test_types types; 257 258 259(*****************************************************************************) 260(* Example, originating from Matt Kaufmann, showing the flow *) 261(* from HOL to HOL/SEXP and then to ACL2. *) 262(*****************************************************************************) 263 264(*****************************************************************************) 265(* The example is a machine that processes read and write instructions *) 266(* N.B. Maybe write should be curried -- will change if necessary? *) 267(*****************************************************************************) 268 269val _ = Hol_datatype `instruction = Read of num | Write of num # num`; 270 271(*****************************************************************************) 272(* read_step addr [(a1,v1);...;(an,vn)] returns vi where addr=ai, *) 273(* scanning from left (i.e. from i=1) *) 274(*****************************************************************************) 275val read_step_def = 276 Define 277 `(read_step (addr:num) [] = 0n) 278 /\ 279 (read_step addr ((addr',v)::alist) = 280 if addr = addr' then v else read_step addr alist)`; 281 282(*****************************************************************************) 283(* write_step addr v [(a1,v1);...;(ai,vi);...;(an,vn)] = *) 284(* [(a1,v1);...;(ai,v);...;(an,vn)] *) 285(* *) 286(* where addr=ai, scanning from left (i.e. from i=1) *) 287(*****************************************************************************) 288val write_step_def = 289 Define 290 `(write_step (addr:num) (v:num) [] = [(addr,v)]) 291 /\ 292 (write_step addr v ((addr',v')::alist) = 293 if addr = addr' 294 then (addr,v)::alist 295 else (addr',v')::(write_step addr v alist))`; 296 297(*****************************************************************************) 298(* run [ins1;...;insn] [(a1,v1);...;(ai,vi);...;(an,vn)] [v1;...;vp] = *) 299(* [v1;...;vp;vq...;vr] *) 300(* *) 301(* where [vq;...;vr] is the reversed list of values Read (by a Read *) 302(* instruction) when executing [ins1;...;insn] (in that order) *) 303(* *) 304(* Example: *) 305(* *) 306(* |- run *) 307(* [Write (92,1); Read 38; Write (79,3); Read 21; Write (66,5); *) 308(* Read 4; Write (53,7); Read 87; Write (40,9); Read 70; *) 309(* Write (27,11); Read 53; Write (14,13); Read 36; Write (1,15); *) 310(* Read 19; Write (88,17); Read 2; Write (75,19); Read 85; *) 311(* Write (62,21); Read 68; Write (49,23); Read 51; Write (36,25); *) 312(* Read 34; Write (23,27); Read 17; Write (10,29); Read 0] [] [] *) 313(* [0; 0; 0; 0; 0; 0; 0; 0; 0; 7; 0; 0; 0; 0; 0] : thm *) 314(*****************************************************************************) 315val run_def = 316 Define 317 `(run [] alist reversed_values_read = reversed_values_read) 318 /\ 319 (run (Write (addr,v)::instrs) alist reversed_values_read = 320 run instrs (write_step addr v alist) reversed_values_read) 321 /\ 322 (run (Read (addr)::instrs) alist reversed_values_read = 323 run instrs alist (read_step addr alist::reversed_values_read))`; 324 325(*****************************************************************************) 326(* The function make_instrs generates a program to run. For example: *) 327(* *) 328(* |- make_instrs 0 10 F 10 [] = *) 329(* [Write (62,1); Read 68; Write (49,3); Read 51; *) 330(* Write (36,5); Read 34; Write (23,7); Read 17; *) 331(* Write (10,9); Read 0] *) 332(* *) 333(* This was generated by EVAL ``make_instrs 0 10 F 10 []``. *) 334(* *) 335(* Note that as an accumulator is used, the list returned is the list of *) 336(* instructions in the reverse order to which they were created. *) 337(*****************************************************************************) 338val write_increment_def = 339 Define `write_increment = 13n`; 340 341val read_increment_def = 342 Define `read_increment = 17n`; 343 344val max_addr_def = 345 Define `max_addr = 100n`; 346 347val fix_address_def = Define `fix_address a b = if a >= b /\ ~(b = 0) then fix_address (a - b) b else a:num`; 348 349val make_instrs_def = 350 Define 351 `(make_instrs read_start write_start flag 0 acc = acc) 352 /\ 353 (make_instrs read_start write_start flag (SUC n) acc = 354 if flag 355 then make_instrs read_start 356 (fix_address (write_start + write_increment) max_addr) 357 (~flag) 358 n 359 (Write(write_start,SUC n) :: acc) 360 else make_instrs (fix_address (read_start + read_increment) max_addr) 361 write_start 362 (~flag) 363 n 364 (Read read_start :: acc))`; 365 366(*****************************************************************************) 367(* Version using a conditional rather than pattern matching on ``0`` and *) 368(* ``SUC n`` (needed to make computeLib.EVAL happy) *) 369(*****************************************************************************) 370val make_instrs_def = 371 prove 372 (``make_instrs read_start write_start flag n acc = 373 if n=0 374 then acc 375 else if flag 376 then make_instrs read_start 377 (fix_address (write_start + write_increment) max_addr) 378 (~flag) 379 (n - 1) 380 (Write(write_start,n) :: acc) 381 else make_instrs (fix_address (read_start + read_increment) max_addr) 382 write_start 383 (~flag) 384 (n - 1) 385 (Read read_start :: acc)``, 386 Cases_on `n` 387 THEN RW_TAC arith_ss [make_instrs_def]); 388 389val _ = computeLib.add_funs[make_instrs_def]; 390 391 392(**** Examples *************************************************************** 393 394val basic_result = time EVAL ``run (make_instrs 0 10 F 100 []) [] []``; 395runtime: 2.405s, gctime: 0.224s, systime: 0.000s. 396> val basic_result = 397 |- run (make_instrs 0 10 F 100 []) [] [] = 398 [39; 21; 3; 0; 0; 0; 0; 0; 0; 77; 59; 41; 23; 5; 0; 0; 0; 0; 0; 0; 0; 399 0; 43; 25; 7; 0; 0; 0; 0; 0; 0; 0; 0; 0; 27; 9; 0; 0; 0; 0; 0; 0; 0; 400 0; 0; 0; 0; 0; 0; 0] : thm 401 402Example that is too big (segmentation fault on trout). 403 404val medium_instr_list = time EVAL ``make_instrs 0 10 F 1000 []``; 405 406val medium_instr_list_def = 407 Define 408 `medium_instr_list = ^(rhs(concl(time EVAL ``make_instrs 0 10 F 1000 []``)))`; 409 410val medium_result = time EVAL ``run medium_instr_list [] []``; 411 412val medium_result = time EVAL ``run (make_instrs 0 10 F 1000 []) [] []``; 413 414val big_instr_list = time EVAL ``make_instrs 0 10 F 1000000 []``; 415 416val big_instr_list_def = 417 Define 418 `big_instr_list = ^(rhs(concl(time EVAL ``make_instrs 0 10 F 1000000 []``)))`; 419 420val basic_result = time EVAL ``run big_instr_list [] []``; 421 422******************************************************************************) 423 424set_trace "EncodeLib.FunctionEncoding" 1; 425 426(*****************************************************************************) 427(* Some simple arithmetic functions: *) 428(*****************************************************************************) 429 430val (divsub_def,divsub_ind) = 431 (RIGHT_CONV_RULE (ONCE_DEPTH_CONV (HO_REWR_CONV 432 (prove(`` (let c = a * b:num in let d = a + b in e c d) = 433 (let c = a * b and d = a + b in e c d)``, 434 REWRITE_TAC [LET_THM] THEN BETA_TAC THEN REFL_TAC)))) ## I) 435 (Defn.tprove 436 (Hol_defn "divsub" `divsub a b = 437 if 0 < a \/ 0 < b then let c = a * b in let d = a + b in 1 + divsub (c DIV d) (c - d) else 0n`, 438 WF_REL_TAC `measure (\ (a,b). if 0 < a then a else b)` THEN 439 RW_TAC arith_ss [DIV_LT_X,LEFT_ADD_DISTRIB,RIGHT_ADD_DISTRIB,X_LT_DIV])); 440 441val acl2_exp_def = convert_definition EXP; 442val acl2_fact_def = convert_definition FACT; 443val acl2_findq_def = convert_definition findq_thm; 444val acl2_divmod_def = convert_definition DIVMOD_THM; 445val acl2_divsub_def = convert_definition_full NONE 446 [DECIDE ``0 < a \/ 0 < b ==> ~(a + b = 0n)``] divsub_def; 447 448 449(*****************************************************************************) 450(* Encoding of Matt's example given earlier: *) 451(*****************************************************************************) 452 453val acl2_read_step_def = convert_definition read_step_def; 454val acl2_write_step_def = convert_definition write_step_def; 455val acl2_run_def = convert_definition run_def; 456val acl2_write_increment_def = convert_definition write_increment_def; 457val acl2_read_increment_def = convert_definition read_increment_def; 458val acl2_max_addr_def = convert_definition max_addr_def; 459val acl2_fix_address_def = convert_definition fix_address_def; 460val acl2_make_instrs_def = convert_definition make_instrs_def; 461 462(*****************************************************************************) 463(* Encoding of rose_tree and red-black tree functions... *) 464(*****************************************************************************) 465 466 467val count_def = Define ` (count (Branch []) = 0n) /\ 468 (count (Branch ((x,hd)::tl)) = 1 + count (hd:num rose_tree) + count (Branch tl))`; 469val acl2_count_def = convert_definition count_def; 470 471val member_def = Define ` (member key LEAF = F) /\ 472 (member key (NODE col k left right) = if key < k then member key left else if k < key then member key right else T)`; 473val acl2_member_def = convert_definition member_def; 474 475(*****************************************************************************) 476(* Restricting the input domain of a function: *) 477(*****************************************************************************) 478 479val modpow_def = Define `(modpow a 0 n = 1) /\ (modpow a (SUC b) n = a * (modpow a b n) MOD n)`; 480val acl2_modpow_def = convert_definition_full (SOME ``\a b c. ~(c = 0n)``) [] modpow_def; 481 482(*****************************************************************************) 483(* Addition of a termination helper theorem: *) 484(*****************************************************************************) 485 486val (log2_def,log2_ind) = Defn.tprove(Hol_defn "log2" `(log2 0 = 0) /\ (log2 a = SUC (log2 (a DIV 2)))`,WF_REL_TAC `measure (\a.a)` THEN RW_TAC arith_ss [DIV_LT_X]); 487val acl2_log2_def = convert_definition_full (SOME ``\a. 0 < a ==> a DIV 2 < a``) 488 [prove(``!a. 0 < a ==> a DIV 2 < a``,RW_TAC arith_ss [DIV_LT_X]), 489 DECIDE ``~(2 = 0n)``] log2_def; 490 491(*****************************************************************************) 492(* Theorem encoding... *) 493(*****************************************************************************) 494 495val acl2_division = convert_theorem [DECIDE ``0 < a ==> ~(a = 0n)``] DIVISION; 496val acl2_divmod_calc = convert_theorem [DECIDE ``0 < a ==> ~(a = 0n)``] DIVMOD_CALC; 497 498(*****************************************************************************) 499(* HO function encoding... *) 500(*****************************************************************************) 501 502val (acl2_filter_correct,acl2_filter_def) = convert_definition (INST_TYPE [``:'a`` |-> ``:num``] FILTER); 503 504val filter_zero_def = Define `filter_zero x = FILTER (\x. ~(x = 0n)) x`; 505 506val (acl2_filter_zero_correct,acl2_filter_zero_def) = convert_definition filter_zero_def; 507 508val (filter0_rewrite,filter0_def) = flatten_HO_definition "filter0" acl2_filter_def ``(acl2_FILTER (\x. ite (natp x) (not (equal x (nat 0))) (not (equal (nat 0) (nat 0)))) X)``; 509 510val acl2_filter_zero_def' = REWRITE_RULE [filter0_rewrite] acl2_filter_zero_def; 511 512(*****************************************************************************) 513(* Encoding functions with missing clauses: *) 514(*****************************************************************************) 515 516val acl2_firstn_def = convert_definition_full (SOME ``\n l. n <= LENGTH l``) 517 [prove(``!n (l:num list). n <= LENGTH l ==> (n = 0) \/ ?t h. l = h :: t``, 518 Cases_on `l` THEN Cases_on `n` THEN RW_TAC std_ss [LENGTH]), 519 prove(``!n (l:num list) x. SUC n <= LENGTH (x::l) ==> n <= LENGTH l``, 520 RW_TAC std_ss [LENGTH])] (INST_TYPE [``:'a`` |-> ``:num``] rich_listTheory.FIRSTN); 521val acl2_tl_def = convert_definition (INST_TYPE [``:'a`` |-> ``:num``] TL); 522val acl2_hd_def = convert_definition (INST_TYPE [``:'a`` |-> ``:num``] HD); 523 524(*****************************************************************************) 525(* A long example from red-black trees (most likely 4+ hours...) *) 526(*****************************************************************************) 527 528val make_black = 529 Define 530 ` (make_black (NODE R e l r) = NODE B e l r) 531 /\ (make_black x = x)`; 532 533val balance = 534 Mosml.time 535 Define 536 ` (balance B z (NODE R y (NODE R x a b) c) d 537 = NODE R y (NODE B x a b) (NODE B z c d)) /\ 538 (balance B z (NODE R x a (NODE R y b c)) d 539 = NODE R y (NODE B x a b) (NODE B z c d)) /\ 540 (balance B x a (NODE R z (NODE R y b c) d) 541 = NODE R y (NODE B x a b) (NODE B z c d)) /\ 542 (balance B x a (NODE R y b (NODE R z c d)) 543 = NODE R y (NODE B x a b) (NODE B z c d)) /\ 544 (balance col x left right 545 = NODE col x left right)`; 546 547val ins = 548 Define 549 ` (ins e LEAF = NODE R e LEAF LEAF) 550 /\ (ins e (NODE c n left right) = 551 if e < n then balance c n (ins e left) right else 552 if n < e then balance c n left (ins e right) 553 else NODE c n left right)`; 554 555val insert = 556 Define 557 `insert e set = make_black(ins e set)`; 558 559val isRed = (* A leaf is considered black *) 560 Define 561 ` (isRed (NODE R k l r) = T) 562 /\ (isRed otherwise = F)`; 563 564val redRed = 565 Define 566 ` (redRed LEAF = F) 567 /\ (redRed (NODE R k left right) = 568 isRed left \/ isRed right \/ redRed left \/ redRed right) 569 /\ (redRed (NODE c k left right) = 570 redRed left \/ redRed right)`; 571 572val BH = 573 Define 574 `(BH LEAF = SOME 0n) /\ 575 (BH (NODE c _ l r) = 576 case (BH l,BH r) of 577 (NONE,o2) -> NONE 578 || (SOME m,NONE) -> NONE 579 || (SOME m,SOME n) -> 580 (if m = n then SOME (m + (if c = R then 0 else 1)) else NONE))`; 581 582 583val acl2_make_black_def = convert_definition make_black; 584val acl2_isRed_def = convert_definition isRed; 585val acl2_redRed_def = convert_definition redRed; 586val acl2_BH_def = convert_definition BH; 587val acl2_balance_def = try convert_definition balance; 588val acl2_ins_def = convert_definition ins; 589val acl2_insert_def = convert_definition insert; 590