The Anubis project. Predefined types and data ('secret' part). Copyright (c) Alain Prouté 2000-today. Contributions by: Cedric Ricard This file is part of the very source of the Anubis compiler. It is the private part of: read ../../library/predefined.anubis Note: since version 1.13, the 'pound currency' symbol (which creates displaying problems because it is not ASCII) is replaced by the sequence +++. public define inline One forget($T x) = unique. define macro Bool +++non_equal($T x, $T y) = if x = y then false else true. *** (2.6) The types 'Word4', 'Word8', 'Word16', 'Word32', 'Word64', 'Word128'. public define String to_hexa(Word4 x) = +++avm{ (word_to_hexa . 4) }. 1 digit public define String to_hexa(Word8 x) = +++avm{ (word_to_hexa . 8) }. 2 digits public define String to_hexa(Word16 x) = +++avm{ (word_to_hexa . 16) }. 4 digits public define String to_hexa(Word32 x) = +++avm{ (word_to_hexa . 32) }. 8 digits public define String to_hexa(Word64 x) = +++avm{ (word_to_hexa . 64) }. 16 digits public define String to_hexa(Word128 x) = +++avm{ (word_to_hexa . 128) }. 32 digits public define String to_decimal(Word4 x) = +++avm{ (word_to_decimal . 4) }. public define String to_decimal(Word8 x) = +++avm{ (word_to_decimal . 8) }. public define String to_decimal(Word16 x) = +++avm{ (word_to_decimal . 16) }. public define String to_decimal(Word32 x) = +++avm{ (word_to_decimal . 32) }. public define String to_decimal(Word64 x) = +++avm{ (word_to_decimal . 64) }. public define String to_decimal(Word128 x) = +++avm{ (word_to_decimal . 128) }. public define Word4 Word4 x << Int nb = +++avm{ (left_shift . 4) }. public define Word8 Word8 x << Int nb = +++avm{ (left_shift . 8) }. public define Word16 Word16 x << Int nb = +++avm{ (left_shift . 16) }. public define Word32 Word32 x << Int nb = +++avm{ (left_shift . 32) }. public define Word64 Word64 x << Int nb = +++avm{ (left_shift . 64) }. public define Word128 Word128 x << Int nb = +++avm{ (left_shift . 128) }. public define Word4 Word4 x >> Int nb = +++avm{ (right_shift . 4) }. public define Word8 Word8 x >> Int nb = +++avm{ (right_shift . 8) }. public define Word16 Word16 x >> Int nb = +++avm{ (right_shift . 16) }. public define Word32 Word32 x >> Int nb = +++avm{ (right_shift . 32) }. public define Word64 Word64 x >> Int nb = +++avm{ (right_shift . 64) }. public define Word128 Word128 x >> Int nb = +++avm{ (right_shift . 128) }. public define Word4 Word4 x | Word4 y = +++avm{ (bit_or . 4)}. public define Word8 Word8 x | Word8 y = +++avm{ (bit_or . 8)}. public define Word16 Word16 x | Word16 y = +++avm{ (bit_or . 16)}. public define Word32 Word32 x | Word32 y = +++avm{ (bit_or . 32)}. public define Word64 Word64 x | Word64 y = +++avm{ (bit_or . 64)}. public define Word128 Word128 x | Word128 y = +++avm{ (bit_or . 128)}. public define Word4 Word4 x : Word4 y = +++avm{ (bit_xor . 4)}. public define Word8 Word8 x : Word8 y = +++avm{ (bit_xor . 8)}. public define Word16 Word16 x : Word16 y = +++avm{ (bit_xor . 16)}. public define Word32 Word32 x : Word32 y = +++avm{ (bit_xor . 32)}. public define Word64 Word64 x : Word64 y = +++avm{ (bit_xor . 64)}. public define Word128 Word128 x : Word128 y = +++avm{ (bit_xor . 128)}. public define Word4 Word4 x & Word4 y = +++avm{ (bit_and . 4)}. public define Word8 Word8 x & Word8 y = +++avm{ (bit_and . 8)}. public define Word16 Word16 x & Word16 y = +++avm{ (bit_and . 16)}. public define Word32 Word32 x & Word32 y = +++avm{ (bit_and . 32)}. public define Word64 Word64 x & Word64 y = +++avm{ (bit_and . 64)}. public define Word128 Word128 x & Word128 y = +++avm{ (bit_and . 128)}. public define Word4 ~ Word4 y = +++avm{ (bit_not . 4)}. public define Word8 ~ Word8 y = +++avm{ (bit_not . 8)}. public define Word16 ~ Word16 y = +++avm{ (bit_not . 16)}. public define Word32 ~ Word32 y = +++avm{ (bit_not . 32)}. public define Word64 ~ Word64 y = +++avm{ (bit_not . 64)}. public define Word128 ~ Word128 y = +++avm{ (bit_not . 128)}. public define Bool Word4 x +=< Word4 y = +++avm{ (bit_lessoreq . 4)}. public define Bool Word8 x +=< Word8 y = +++avm{ (bit_lessoreq . 8)}. public define Bool Word16 x +=< Word16 y = +++avm{ (bit_lessoreq . 16)}. public define Bool Word32 x +=< Word32 y = +++avm{ (bit_lessoreq . 32)}. public define Bool Word64 x +=< Word64 y = +++avm{ (bit_lessoreq . 64)}. public define Bool Word128 x +=< Word128 y = +++avm{ (bit_lessoreq . 128)}. public define Bool Word4 x +< Word4 y = +++avm{ (bit_less . 4)}. public define Bool Word8 x +< Word8 y = +++avm{ (bit_less . 8)}. public define Bool Word16 x +< Word16 y = +++avm{ (bit_less . 16)}. public define Bool Word32 x +< Word32 y = +++avm{ (bit_less . 32)}. public define Bool Word64 x +< Word64 y = +++avm{ (bit_less . 64)}. public define Bool Word128 x +< Word128 y = +++avm{ (bit_less . 128)}. public define Bool Word4 x -=< Word4 y = +++avm{ (bit_slessoreq . 4)}. public define Bool Word8 x -=< Word8 y = +++avm{ (bit_slessoreq . 8)}. public define Bool Word16 x -=< Word16 y = +++avm{ (bit_slessoreq . 16)}. public define Bool Word32 x -=< Word32 y = +++avm{ (bit_slessoreq . 32)}. public define Bool Word64 x -=< Word64 y = +++avm{ (bit_slessoreq . 64)}. public define Bool Word128 x -=< Word128 y = +++avm{ (bit_slessoreq . 128)}. public define Bool Word4 x -< Word4 y = +++avm{ (bit_sless . 4)}. public define Bool Word8 x -< Word8 y = +++avm{ (bit_sless . 8)}. public define Bool Word16 x -< Word16 y = +++avm{ (bit_sless . 16)}. public define Bool Word32 x -< Word32 y = +++avm{ (bit_sless . 32)}. public define Bool Word64 x -< Word64 y = +++avm{ (bit_sless . 64)}. public define Bool Word128 x -< Word128 y = +++avm{ (bit_sless . 128)}. public define Word4 Word4 x + Word4 y = +++avm{ (bit_plus . 4)}. public define Word8 Word8 x + Word8 y = +++avm{ (bit_plus . 8)}. public define Word16 Word16 x + Word16 y = +++avm{ (bit_plus . 16)}. public define Word32 Word32 x + Word32 y = +++avm{ (bit_plus . 32)}. public define Word64 Word64 x + Word64 y = +++avm{ (bit_plus . 64)}. public define Word128 Word128 x + Word128 y = +++avm{ (bit_plus . 128)}. public define Word4 Word4 x - Word4 y = +++avm{ (bit_minus . 4)}. public define Word8 Word8 x - Word8 y = +++avm{ (bit_minus . 8)}. public define Word16 Word16 x - Word16 y = +++avm{ (bit_minus . 16)}. public define Word32 Word32 x - Word32 y = +++avm{ (bit_minus . 32)}. public define Word64 Word64 x - Word64 y = +++avm{ (bit_minus . 64)}. public define Word128 Word128 x - Word128 y = +++avm{ (bit_minus . 128)}. public define Word4 Word4 x * Word4 y = +++avm{ (bit_times . 4)}. public define Word8 Word8 x * Word8 y = +++avm{ (bit_times . 8)}. public define Word16 Word16 x * Word16 y = +++avm{ (bit_times . 16)}. public define Word32 Word32 x * Word32 y = +++avm{ (bit_times . 32)}. public define Word64 Word64 x * Word64 y = +++avm{ (bit_times . 64)}. public define Word128 Word128 x * Word128 y = +++avm{ (bit_times . 128)}. public define Word4 - Word4 y = +++avm{ (bit_opp . 4)}. public define Word8 - Word8 y = +++avm{ (bit_opp . 8)}. public define Word16 - Word16 y = +++avm{ (bit_opp . 16)}. public define Word32 - Word32 y = +++avm{ (bit_opp . 32)}. public define Word64 - Word64 y = +++avm{ (bit_opp . 64)}. public define Word128 - Word128 y = +++avm{ (bit_opp . 128)}. ---> saved from predefined.anubis You may also want to know the number of significant bits in a word. public define Int significant_bits(Word4 x). public define Int significant_bits(Word8 x). public define Int significant_bits(Word16 x). public define Int significant_bits(Word32 x). public define Int significant_bits(Word64 x). public define Int significant_bits(Word128 x). Examples: significant_bits((Word8) 0x10) is 5 significant_bits((Word64) 0x7a6453de54) is 40 significant_bits((Word8) 0x7a6453de54) is 7 (because considered modulo 2^8) <--- public define Int significant_bits(Word4 x) = +++avm{ (word_significant_bits . 4) }. public define Int significant_bits(Word8 x) = +++avm{ (word_significant_bits . 8) }. public define Int significant_bits(Word16 x) = +++avm{ (word_significant_bits . 16) }. public define Int significant_bits(Word32 x) = +++avm{ (word_significant_bits . 32) }. public define Int significant_bits(Word64 x) = +++avm{ (word_significant_bits . 64) }. public define Int significant_bits(Word128 x) = +++avm{ (word_significant_bits . 128) }. *** Sorting lists. max and min for lists of integers. define Int max // auxiliary function ( Int x, List(Int) l ) = if l is { [ ] then x, [h . t] then if x < h then max(h,t) else max(x,t) }. public define Int max ( List(Int) l, Int default ) = max(default,l). public define inline Int // must not be macro because x and y are always computed // and one of them would be computed twice max ( Int x, Int y ) = if x < y then y else x. public define inline Int min ( Int x, Int y ) = if x < y then x else y. define Int min // auxiliary function ( Int x, List(Int) l ) = if l is { [ ] then x, [h . t] then if x < h then min(x,t) else min(h,t) }. public define Int min ( List(Int) l, Int default, ) = min(default,l). public define One iprint(String s) = print(s); forget(flush(stdout)). public define macro Bool Bool x | Bool y = if x then true else y. public define macro Bool Bool x & Bool y = if x then y else false. *** Transforming lists of Words to Int. public define Int to_Int(List(Word32) x) = +++avm{ list_word32_to_int }. Separating the first two elements from a list (a default value is provided for non existing elements). define ($T,$T,List($T)) // first two elements and rest of the list +++first_two ( List($T) l, $T default ) = if l is { [ ] then (default,default,[]), [h1 . t1] then if t1 is { [ ] then (h1,default,[]), [h2 . t2] then (h1,h2,t2) } }. define List(Word32) +++group_to_word32(List(Word4) x) = if x is [] then [] else if +++first_two(x,0) is (w1,w2,t1) then if +++first_two(t1,0) is (w3,w4,t2) then if +++first_two(t2,0) is (w5,w6,t3) then if +++first_two(t3,0) is (w7,w8,t4) then [word32(word16(word8(w1,w2),word8(w3,w4)),word16(word8(w5,w6),word8(w7,w8))) . +++group_to_word32(t4)]. define List(Word32) +++group_to_word32(List(Word8) x) = if x is [] then [] else if +++first_two(x,0) is (w1,w2,t1) then if +++first_two(t1,0) is (w3,w4,t2) then [word32(word16(w1,w2),word16(w3,w4)) . +++group_to_word32(t2)]. define List(Word32) +++group_to_word32(List(Word16) x) = if x is [] then [] else if +++first_two(x,0) is (w1,w2,t) then [word32(w1,w2) . +++group_to_word32(t)]. define List(Word32) +++group_to_word32(List(Word64) x) = if x is { [ ] then [ ], [h . t] then if h is word64(w1,w2) then [w1,w2 . +++group_to_word32(t)] }. define List(Word32) +++group_to_word32(List(Word128) x) = if x is { [ ] then [ ], [h . t] then if h is word128(w1,w2,w3,w4) then [w1,w2,w3,w4 . +++group_to_word32(t)] }. public define Int to_Int (List(Word4) x) = to_Int(+++group_to_word32(x)). public define Int to_Int (List(Word8) x) = to_Int(+++group_to_word32(x)). public define Int to_Int (List(Word16) x) = to_Int(+++group_to_word32(x)). public define Int to_Int (List(Word64) x) = to_Int(+++group_to_word32(x)). public define Int to_Int (List(Word128) x) = to_Int(+++group_to_word32(x)). *** Transforming Int to lists of Words. define List($T) +++remove_trailing($T a, List($T) l) = if l is { [ ] then [ ], [h . t] then if +++remove_trailing(a,t) is { [ ] then if h = a then [ ] else [h], [u . v] then [h, u . v] } }. define Word32 +++number_of_bigits(Int x) = +++avm{ number_of_bigits }. Get the n-th bigit of x (zero if out of bounds) define Word32 +++nth_bigit(Word32 n, Int x) = +++avm{ nth_bigit }. Get the list of bigits from the i-th (included) to the n-th (excluded) define List(Word32) +++to_Word32(Word32 n, Word32 i, Int x) = if i >=+ n then [] else [+++nth_bigit(i,x) . +++to_Word32(n,i+1,x)]. public define List(Word32) to_Word32(Int x) = +++remove_trailing(0,+++to_Word32(+++number_of_bigits(x),0,x)). define List($T) +++flat(List(List($T)) l) = if l is { [ ] then [ ], [h . t] then append(h,+++flat(t)) }. define List(Word4) +++split_word(Word32 x) = if x is word32(h1,h2) then if h1 is word16(u1,u2) then if h2 is word16(u3,u4) then if u1 is word8(w1,w2) then if u2 is word8(w3,w4) then if u3 is word8(w5,w6) then if u4 is word8(w7,w8) then [w1,w2,w3,w4,w5,w6,w7,w8]. define List(Word8) +++split_word(Word32 x) = if x is word32(h1,h2) then if h1 is word16(u1,u2) then if h2 is word16(u3,u4) then [u1,u2,u3,u4]. define List(Word16) +++split_word(Word32 x) = if x is word32(h1,h2) then [h1,h2]. define List(Word64) +++group_by_two(List(Word32) l) = if +++first_two(l,0) is (w1,w2,t) then [word64(w1,w2) . +++group_by_two(t)]. define List(Word128) +++group_by_four(List(Word32) l) = if +++first_two(l,0) is (w1,w2,t1) then if +++first_two(t1,0) is (w3,w4,t2) then [word128(w1,w2,w3,w4) . +++group_by_four(t2)]. public define List(Word4) to_Word4(Int x) = +++remove_trailing(0,+++flat(map(+++split_word,to_Word32(x)))). public define List(Word8) to_Word8(Int x) = +++remove_trailing(0,+++flat(map(+++split_word,to_Word32(x)))). public define List(Word16) to_Word16(Int x) = +++remove_trailing(0,+++flat(map(+++split_word,to_Word32(x)))). public define List(Word64) to_Word64(Int x) = +++remove_trailing(0,+++group_by_two(to_Word32(x))). public define List(Word128) to_Word128(Int x) = +++remove_trailing(0,+++group_by_four(to_Word32(x))). Euclidian division for words. public define Maybe((Word4,Word4)) Word4 x / Word4 y = +++avm{ (word_euclid . 4)}. public define Maybe((Word8,Word8)) Word8 x / Word8 y = +++avm{ (word_euclid . 8)}. public define Maybe((Word16,Word16)) Word16 x / Word16 y = +++avm{ (word_euclid . 16)}. public define Maybe((Word32,Word32)) Word32 x / Word32 y = +++avm{ (word_euclid . 32)}. define Word64 +++to_w64 ( Int x ) = if to_Word64(x) is { [ ] then 0, [h . _] then h }. define Word128 +++to_w128 ( Int x ) = if to_Word128(x) is { [ ] then 0, [h . _] then h }. public define Maybe((Word64,Word64)) Word64 x / Word64 y = if to_Int([x]) / to_Int([y]) is { failure then failure, success(p) then if p is (q,r) then success((+++to_w64(q),+++to_w64(r))) }. public define Maybe((Word128,Word128)) Word128 x / Word128 y = if to_Int([x]) / to_Int([y]) is { failure then failure, success(p) then if p is (q,r) then success((+++to_w128(q),+++to_w128(r))) }. public define Int to_Int(Word32 x) = +++avm{ word32_to_int }. public define Word32 truncate_to_Word32(Int n) = +++avm{ int_to_word32 }. public define Word8 truncate_to_Word8 ( Int n ) = if truncate_to_Word32(n) is word32(low1,_) then if low1 is word16(low2,_) then low2. *** (3.1) Determination of the host system. public define HostSystem host_system = +++avm{ host_system }. public define HostArchitecture host_arch = +++avm{ host_arch }. public define Endianness system_endianness = +++avm{ endianness }. *** (3.2) Version numbers of your Anubis system. public define Word32 major_version_number = +++avm{ major_version_number }. public define Word32 minor_version_number = +++avm{ minor_version_number }. *** (3.3) Anubis directories (where the system is installed). public define String anubis_directory = +++avm{ get_anubis_directory }. public define String my_anubis_directory = +++avm{ get_my_anubis_directory }. *** (3.4) Getting and setting environment variables. public define Maybe(String) get_environment_variable(String name) = +++avm{ getenvvar }. public define Maybe(One) set_environment_variable(String name, String value) = +++avm{ setenvvar }. *** (formerly 3.5) Alert. public define $T +++alert_handler ( String file_name, Word32 line, Word32 column ) = +++avm{ do_alert }. public define $T +++todo_handler ( String file_name, Word32 line, Word32 column, String text ) = +++avm{ do_todo }. *** `should_not_happen' mecanism. public define $T +++should_not_happen ( String file_path, Word32 line, (String,Word32)->One callback, $T value ) = callback(file_path,line); value. public define One +++default_snh_callback ( String file_path, Word32 line ) = print("Something should not have happened in file '"+file_path+"' at line "+to_decimal(line)+".\n"). *** (3.6) Informations on virtual machines. public define Word32 virtual_machine_id = +++avm{ virtual_machine_id }. public define Word32 virtual_machine_count = +++avm{ machine_count }. type +++VirtualMachineInfo: +++vm_info (Word32 virtual_machine_id, VirtualMachineState state, VirtualMachineWorkSort work_sort, Word32 instruction_pointer, // current offset in the module Word32 stack_size, // in 32 bits words Word32 stack_pointer, // number of 32 bits words in the stack Word32 loadav1, // load average for the past 1 minute Word32 loadav5, // load average for the past 5 minutes Word32 loadav15). // load average for the past 15 minutes type +++VMI_Request: by_index (Word32), by_id (Word32). define Maybe(+++VirtualMachineInfo) +++vm_info ( +++VMI_Request req ) = +++avm{ vm_info }. define Maybe(VirtualMachineInfo) +++virtual_machine_info ( +++VMI_Request req ) = if +++vm_info(req) is { failure then failure, success(mi) then if mi is +++vm_info(vmid, state, ws, ip, ss, sp, loadav1, loadav5, loadav15) then success(vm_info(vmid, state, ws, ip, ss, sp, if to_Float(loadav1) / 0x800 is success(v) then v else 0, if to_Float(loadav5) / 0x800 is success(v) then v else 0, if to_Float(loadav15) / 0x800 is success(v) then v else 0)) }. public define Maybe(VirtualMachineInfo) virtual_machine_info ( Word32 mid ) = +++virtual_machine_info(by_id(mid)). define List(VirtualMachineInfo) +++machines_info ( Word32 index, List(VirtualMachineInfo) so_far ) = if +++virtual_machine_info(by_index(index)) is { failure then reverse(so_far), success(i) then +++machines_info(index + 1, [i . so_far]) }. public define SystemInfo system_info = sys_info(get_load_average, +++machines_info(0, [])). public define VirtualMachineInfo virtual_machine_info = if virtual_machine_info(virtual_machine_id) is { failure then vm_info((Word32)0,not_used,computing, (Word32)0, (Word32)0, (Word32)0, (Float)0, (Float)0, (Float)0), success(mi) then mi }. type +++LoadAverage: +++load_average (Word32 loadav1, // load average for the past 1 minute in 11 bits fixed point Word32 loadav5, // load average for the past 5 minutes in 11 bits fixed point Word32 loadav15). // load average for the past 15 minutes in 11 bits fixed point define +++LoadAverage +++get_load_average = +++avm { get_load_average }. public define LoadAverage get_load_average = if +++get_load_average is +++load_average (loadav1, loadav5, loadav15) then load_average(if to_Float(loadav1) / 0x800 is success(v) then v else 0, if to_Float(loadav5) / 0x800 is success(v) then v else 0, if to_Float(loadav15) / 0x800 is success(v) then v else 0). public define One wait_for_event = +++avm { wait_for_event }. *** (3.7) Informations on the memory allocator. public define AllocatorInfo allocator_info = +++avm{ allocator_info }. *** (3.8) Automatic restarting of 'anbexec'. public define One restart(Bool b) = +++avm{ must_restart }. public define Bool will_restart = +++avm{ will_restart }. *** (4.1) Strings (type 'String'). public define String constant_string(Int n, Word8 c) = +++avm{ constant_string }. public define Bool string_less(String x, String y) = +++avm{ string_less }. define Word32 length(String s) = +++avm{ string_length }. public define Int length(String s) = to_Int(length(s)). public define Maybe(Word8) nth(Int n, String s) = +++avm{ string_nth }. public define Maybe(Int) decimal_scan(String s) = +++avm{ decimal_scan }. public define Maybe(Float) string_to_float(String s) = +++avm{ string_to_float }. define Maybe(String) sub_string(String s, Word32 start, Word32 length) = +++avm{ sub_string }. public define Maybe(String) sub_string(String s, Int start, Int length) = sub_string(s, truncate_to_Word32(start), truncate_to_Word32(length)). public define Maybe(Int) find_string(String s, String looking_for, Int start) = +++avm{ find_string }. public define String String x + String y = +++avm{ strconcat }. public define String concat(List(String) l) = +++avm{ str_list_concat }. public define String implode(List(Word8) l) = +++avm{ implode }. public define List(Word8) explode(String s) = +++avm{ explode }. public define One print(String x) = +++avm{ print_string }. define One print ( WStream file, String s, Int from ) = if nth(from,s) is { failure then unique, success(c) then if file <- c is { failure then unique, success(_) then print(file,s,from+1) } }. public define One print ( WStream file, String s ) = print(file,s,0). public define String toCRLF(String s) = +++avm{ string_toCRLF }. public define String toLF(String s) = +++avm{ string_toLF }. *** (4.3) Byte arrays (type 'ByteArray'). public define Int length(ByteArray s) = +++avm{ byte_array_length_int }. public define Word32 length32(ByteArray s) = +++avm{ byte_array_length_word32 }. public define Maybe(Word8) nth(Int n, ByteArray s) = +++avm{ byte_array_nth }. public define Word8 force_nth ( Int n, ByteArray b ) = if nth(n,b) is { failure then 0, success(c) then c }. public define Maybe(One) put(ByteArray s, Int n, Word8 c) = +++avm{ byte_array_put }. public define ByteArray constant_byte_array(Int n, Word8 c) = +++avm{ constant_byte_array }. public define ByteArray constant_byte_array_16(Int n, Word16 w) = +++avm{ constant_byte_array_16 }. public define One truncate(ByteArray s, Int size) = +++avm{ truncate_byte_array }. public define ByteArray extract(ByteArray s, Int start, Int end) = +++avm{ extract_byte_array }. public define ByteArray ByteArray s + ByteArray t = +++avm{ concat_byte_array }. public define String to_ascii(ByteArray s) = +++avm{ byte_array_to_ascii }. public define String to_string(ByteArray s) = +++avm{ byte_array_to_string }. public define String to_hexa(ByteArray s) = +++avm{ byte_array_to_ascii }. public define ByteArray to_byte_array(String s) = +++avm{ string_to_byte_array }. public define ByteArray to_text_mode(ByteArray s) = +++avm{ byte_array_to_text_mode }. public define ByteArray toCRLF(ByteArray s) = +++avm{ byte_array_toCRLF }. public define ByteArray toLF(ByteArray s) = +++avm{ byte_array_toLF }. public define Maybe(Int) find_byte_array(ByteArray text, ByteArray pattern, Int start) = +++avm{ find_bytearray }. *** (4.4) True integers (type 'Int'). public define Bool Int x < Int y = +++avm{ int_less }. public define Bool Int x =< Int y = +++avm{ int_lessoreq }. public define Int Int x + Int y = +++avm{ int_plus }. public define Int Int x - Int y = +++avm{ int_minus }. public define Int - Int x = 0 - x. public define Int Int x * Int y = +++avm{ int_times }. public define Maybe((Int,Int)) Int x / Int y = +++avm{ int_euclid }. public define String abs_to_decimal(Int x) = +++avm{ int_to_decimal }. public define String abs_to_hexa(Int x) = +++avm{ int_to_hexa }. *** (4.5) Floating point numbers (type 'Float'). public define Maybe(Float) Float x + Float y = +++avm{ float_plus }. public define Maybe(Float) Float x - Float y = +++avm{ float_minus }. public define Maybe(Float) Float x * Float y = +++avm{ float_times }. public define Maybe(Float) Float x ^ Float y = +++avm{ float_power }. public define Maybe(Float) Float x / Float y = +++avm{ float_div }. public define Float sin(Float x) = +++avm{ float_sin }. public define Float cos(Float x) = +++avm{ float_cos }. public define Maybe(Float) tan(Float x) = +++avm{ float_tan }. public define Maybe(Float) asin(Float x) = +++avm{ float_asin }. public define Maybe(Float) acos(Float x) = +++avm{ float_acos }. public define Float atan(Float x) = +++avm{ float_atan }. public define Maybe(Float) exp(Float x) = +++avm{ float_exp }. public define Maybe(Float) log(Float x) = +++avm{ float_log }. public define Maybe(Float) sqrt(Float x) = +++avm{ float_sqrt }. public define Bool Float x < Float y = +++avm{ float_less }. public define Bool Float x =< Float y = +++avm{ float_lessoreq }. to do: float_to_string(Float,Word32 prec) should become to_String(Float,Int). define String +++float_to_string(Float n, Word32 prec) = +++avm{ float_to_string }. public define String float_to_string(Float n, Int prec) = +++float_to_string(n, truncate_to_Word32(prec)). public define Word32 integral_part_to_Word32(Float n) = +++avm{ float_integral_part }. public define Int integral_part(Float n) = +++avm{ float_to_int }. public define Float to_Float(Word32 x) = +++avm{ integer_to_float }. public define Float to_Float(Int n) = +++avm{ int_to_float }. *** (4.6) Floating point numbers. (Float32 and Float64) public type Float32Value: float32value(Word32). public type Float64Value: float64value(Word32,Word32). *** (5) Files. *** (5.1) Opening files. public define Maybe(RStream) file(String filename, ReadFileMode mode) = +++avm{ open_file_for_reading }. public define Maybe(RWStream) file(String filename, ReadWriteFileMode mode) = +++avm{ open_file_for_writing }. *** (5.2) Unix file system interface. public define Maybe(FileMode) get_file_mode(String file_name) = +++avm{ get_file_mode }. public define Maybe(One) set_file_mode(String file_name, FileMode mode) = +++avm{ set_file_mode }. public define Maybe(FileTimes) get_file_times(String filename) = +++avm{ get_file_times }. public define Maybe(One) set_file_times(String filename, FileTimes times) = +++avm{ set_file_times }. *** (5.3) Standard files. public define RStream stdin = +++avm{ anb_stdin }. // standard input (keyboard) public define WStream stdout = +++avm{ anb_stdout }. // standard output (console) public define WStream stderr = +++avm{ anb_stderr }. // standard error output // (console unless redirected) *** (5.4) Getting the size of a file. public define Int file_size(RStream file) = +++avm{ file_size }. public define Int file_size(WStream file) = +++avm{ file_size }. public define Int file_size(RWStream file) = +++avm{ file_size }. *** (5.5) Weakening file modes. public define RStream weaken(RWStream f) = +++avm{ (copy_stack_ptr . 0) }. public define WStream weaken(RWStream f) = +++avm{ (copy_stack_ptr . 0) }. *** (5.6) Managing directories. public define String get_current_directory = +++avm{ getcurdir }. public define Bool set_current_directory(String name) = +++avm{ setcurdir }. public define MakeDirectoryResult make_directory (String name, DirectoryMode mode) = +++avm{ do_mkdir }. public define RemoveDirectoryResult remove_directory (String directory_name) = +++avm{ do_rmdir }. public define List(String) directory_list ( String directory_name, String file_name_mask ) = +++avm{ do_ls }. define List(FileDescription) directory_full_list_reverse ( String directory_name, String file_name_mask, String link_name_mask, String directory_name_mask ) = +++avm{ do_full_ls }. public define List(FileDescription) directory_full_list ( String directory_name, String file_name_mask, String link_name_mask, String directory_name_mask ) = reverse(directory_full_list_reverse(directory_name, file_name_mask, link_name_mask, directory_name_mask)). *** (5.7) Creating symbolic links. public define Bool create_symbolic_link ( String file_path, String link_name ) = +++avm{ create_symbolic_link }. *** (5.8) Reading and writing files (and also TCP/IP connections). public define ReadResult read ( RStream file, Int n, Int timeout // in seconds ) = +++avm{ read_file }. define Maybe(Word32) // number of bytes written +++write ( WStream file, ByteArray data ) = +++avm{ write_file }. public define Maybe(Int) // number of bytes written write ( WStream file, ByteArray data ) = if +++write(file, data) is success(n) then success(to_Int(n)) else failure. public define ReadLineResult read_line ( RStream file, Int n, Int timeout // in seconds ) = +++avm{ read_line }. define ReadFileResult +++read_from_file ( RStream file, Int size, ByteArray so_far ) = if length(so_far) = size then ok(so_far) else if read(file, 100000, 1000) is { error then read_error(so_far), timeout then read_error(so_far), ok(more) then +++read_from_file(file,size,so_far+more) }. public define ReadFileResult read_from_file ( String file_name ) = if file(file_name,read) is { failure then cannot_find_file, success(file) then +++read_from_file(file, file_size(file), constant_byte_array(0,0)) }. define WriteFileResult +++write_to_file ( WStream file, ByteArray data, Int written ) = if (Maybe(Int))write(file,data) is { failure then write_error(truncate_to_Word32(written)), success(n) then if length(data) = n then ok else +++write_to_file(file,extract(data,n,length(data)-n),written+n) }. public define WriteFileResult write_to_file ( String file_name, ByteArray data ) = if file(file_name,new) is { failure then cannot_open_file, success(file) then +++write_to_file(weaken(file),data,0) }. to do: 'seek' and 'tell' should use Int instead of Word32. //define Bool +++seek(RStream file, Word32 where) = +++avm{ file_seek }. //define Bool +++seek(RWStream file, Word32 where) = +++avm{ file_seek }. //define Int tell(RStream file) = +++avm{ file_tell }. //define Int tell(RWStream file) = +++avm{ file_tell }. //public define Bool seek(RStream file, Int where) = +++seek(file, truncate_to_Word32(where)). //public define Bool seek(RWStream file, Int where) = +++seek(file, truncate_to_Word32(where)). public define Bool seek(RStream file, Int where) = +++avm{ file_seek }. public define Bool seek(RWStream file, Int where) = +++avm{ file_seek }. public define Int tell(RStream file) = +++avm{ file_tell }. public define Int tell(RWStream file) = +++avm{ file_tell }. *** (5.9) Removing and renaming files. public define Bool remove(String file_name) = +++avm{ do_remove }. public define Bool rename(String old_name, String new_name) = +++avm{ do_rename }. *** (5.10) Flushing. public define Bool flush (RWStream file) = +++avm{ do_flush }. public define Bool flush (WStream file) = +++avm{ do_flush }. *** (6) Network interface. public define Result(NetworkConnectError,RWStream) connect(Word32 ip_address, Word32 port) = +++avm{ open_tcp_ip_connection }. *** (6.2) Querying IP addresses. public define (Word32,Word32) local_IP_address_and_port (RWStream connection) = +++avm{ local_IP_addr_port }. public define (Word32,Word32) remote_IP_address_and_port (RWStream connection) = +++avm{ remote_IP_addr_port }. *** (6.3) Querying a name server ('dns'). public define DNS_Result dns(String host_name) = +++avm { dns }. *** (6.4) Creating a TCP/IP network server ('start_server'). public type +++ListenerResult: +++cannot_create_the_socket, +++cannot_bind_to_port, +++cannot_listen_on_port, +++ok(+++Listener). define +++ListenerResult +++listener ( Word32 ip_addr, Word32 ip_port ) = +++avm{ listener }. public type +++AcceptConnectionResult: +++listener_is_down, +++cannot_open_pending_connection, +++ok(RWStream). define +++AcceptConnectionResult +++accept_connection ( +++Listener l ) = +++avm{ accept_connection }. define One +++run_server ( +++Listener l, // the listening socket Var(Int) num_conn, // current number of connections (RWStream) -> Bool can_accept, // returns false if connection undesirable (RWStream) -> One handler, // the function handling the requests Var(Bool) shutdown_required, Word8 handler_priority ) = if *shutdown_required then unique else checking every 1 millisecond, wait for true then if +++accept_connection(l) is // the virtual machine is waiting until one of the three things below happens: { +++listener_is_down then unique, /* exit the 'infinite' loop */ +++cannot_open_pending_connection then +++run_server(l,num_conn,can_accept,handler,shutdown_required,handler_priority), /* continue to listen */ +++ok(conn) then (if can_accept(conn) then /* the connection is accepted */ (delegate (handler_priority) ( /* start a virtual machine to handle the connection */ num_conn <- *num_conn + 1; handler(conn); num_conn <- *num_conn - 1 ), unique) else unique); +++run_server(l,num_conn,can_accept,handler,shutdown_required,handler_priority) /* continue to listen */ }. public type Server: +++server(+++Listener, Var(Int) num_conn). Current number of accepted connections public define StartServerResult start_server ( Word32 ip_addr, Word32 ip_port, (RWStream) -> Bool can_accept, Server -> ((RWStream) -> One) handler, Var(Bool) shutdown_required, Word8 listener_priority, Word8 handler_priority ) = if +++listener(ip_addr,ip_port) is { +++cannot_create_the_socket then cannot_create_the_socket, +++cannot_bind_to_port then cannot_bind_to_port, +++cannot_listen_on_port then cannot_listen_on_port, +++ok(l) then with num_conn = var((Int)0), s = +++server(l,num_conn), delegate (listener_priority) +++run_server(l,num_conn,can_accept,handler(s),shutdown_required,handler_priority), ok(s) }. public define StartServerResult start_server ( Word32 ip_addr, Word32 ip_port, (RWStream) -> Bool can_accept, Server -> ((RWStream) -> One) handler, (One) -> One notify, Var(Bool) shutdown_required ) = start_server(ip_addr,ip_port,can_accept,handler,shutdown_required,255,255). public define StartServerResult start_server ( Word32 ip_addr, Word32 ip_port, Server -> ((RWStream) -> One) handler, (One) -> One notify, Var(Bool) shutdown_required ) = start_server(ip_addr,ip_port,(RWStream s) |-> true, handler,notify,shutdown_required). public define StartServerResult start_server ( Word32 ip_addr, Word32 ip_port, Server -> ((RWStream) -> One) handler, (One) -> One notify ) = start_server(ip_addr,ip_port,(RWStream s) |-> true,handler,notify,var((Bool)false)). define One +++shutdown(+++Listener l) = +++avm{ listener_shutdown }. public define One shutdown(Server s) = if s is +++server(l,_) then +++shutdown(l). define Bool +++is_down(+++Listener l) = +++avm{ listener_is_down }. public define Bool is_down(Server s) = if s is +++server(l,_) then +++is_down(l). public define Int number_of_connections(Server s) = if s is +++server(_,v) then *v. *** (6.5) Creating an UDP client socket ('create_udp_client_socket'). public type UDP_Socket: +++udp_socket(RWStream). define Maybe(RWStream) +++create_udp_client_socket = +++avm{ create_udp_client_socket }. public define Create_UDP_Client_Socket_Result create_udp_client_socket = if +++create_udp_client_socket is { failure then cannot_create_the_socket, success(a) then ok(+++udp_socket(a)) }. define Maybe(RWStream) +++create_udp_client_broadcast_socket = +++avm{ create_udp_client_broadcast_socket }. public define Create_UDP_Client_Socket_Result create_udp_client_broadcast_socket = if +++create_udp_client_broadcast_socket is { failure then cannot_create_the_socket, success(a) then ok(+++udp_socket(a)) }. *** (6.6) Sending and receiving UDP packets. public define UDP_Send_Result udp_send ( UDP_Socket socket, Word32 ip_address, // where you want to send the data Word32 ip_port, ByteArray data ) = +++avm{ udp_send }. public define UDP_Receive_Result udp_receive ( UDP_Socket socket, Word32 max_packet_size, Word32 timeout // seconds ) = +++avm{ udp_receive }. *** (6.7) Starting an UDP server ('start_udp_server'). public type UDP_Server: +++udp_server(Var(Bool)). public type +++Create_UDP_Server_Socket_Result: +++cannot_create_the_socket, +++cannot_bind_address_port, +++access_denied, +++ok(RWStream). define +++Create_UDP_Server_Socket_Result +++create_udp_server_socket ( Word32 ip_address, Word32 ip_port ) = +++avm{ create_udp_server_socket }. define One +++run_udp_server ( UDP_Socket socket, (UDP_Socket, ByteArray, Truncation, Word32 ip_address, Word32 ip_port) -> One handler, Word32 max_packet_size, Var(Bool) state_var, // 'true' at the beginning. Becomes 'false' when // the server is shutdown. One -> One notify ) = if *state_var then if udp_receive(socket,max_packet_size,1) is { out_of_time then +++run_udp_server(socket,handler,max_packet_size,state_var,notify), network_unreachable then notify(unique); +++run_udp_server(socket,handler,max_packet_size,state_var,notify), ok(data,trunc,ip_address,ip_port) then delegate handler(socket,data,trunc,ip_address,ip_port), +++run_udp_server(socket,handler,max_packet_size,state_var,notify) } else unique. public define Start_UDP_Server_Result start_udp_server ( Word32 ip_address, // address on which the server will listen // 0 means: 'listen on all interfaces' Word32 ip_port, // port on which the server will listen (UDP_Socket, ByteArray, Truncation, Word32 ip_address, Word32 ip_port) -> One handler, // the function for handling the queries Word32 max_packet_size, // maximal size of queries One -> One notify // used when something wrong happens ) = if +++create_udp_server_socket(ip_address,ip_port) is { +++cannot_create_the_socket then cannot_create_the_socket, +++cannot_bind_address_port then cannot_bind_address_port, +++access_denied then access_denied, +++ok(socket) then with state_var = var((Bool)true), udp_socket = +++udp_socket(socket), delegate +++run_udp_server(udp_socket,handler,max_packet_size,state_var,notify), ok(+++udp_server(state_var)) }. public define Bool is_down ( UDP_Server server ) = if server is +++udp_server(v) then if *v then false else true. public define One shutdown ( UDP_Server server ) = if server is +++udp_server(v) then v <- false. // ----------------------------------------------------------------------------- // ----------------------------------------------------------------------------- *** (6.8) Low level sockets. // ----------------------------------------------------------------------------- // ----------------------------------------------------------------------------- *** (6.8.1) Packet sockets types. // ----------------------------------------------------------------------------- public type PacketSocket: packetSocket(PacketSocketType type, PacketSocketProtocol protocol, RWStream sock). type +++PacketSocketAddress: packet_sockaddr(Word16 protocol, /* Physical layer protocol */ Word32 ifindex, /* Interface number */ Word16 hatype, /* Header type */ Word8 pkttype, /* Packet type */ Word8 halen, /* Length of address */ Word64 addr). /* Physical layer address */ public type PhysicalAddress: physical_address(Word8 phys_halen, Word64 phys_address). // ----------------------------------------------------------------------------- *** (6.8.2) Internet sockets types. // ----------------------------------------------------------------------------- public type Socket: socket(SocketType type, RWStream sock). public define IpAddress inaddr_loopback = ip_address(0x0100007f). public define IpAddress inaddr_any = ip_address(0x00000000). public define IpAddress inaddr_broadcast = ip_address(0xffffffff). type +++InternetSocketAddress: // this will avoid an indirection +++inet_sockaddr(Word32 ip, Word16 port). // ----------------------------------------------------------------------------- *** (6.8.3) VM types and functions for low level sockets. // ----------------------------------------------------------------------------- type +++SocketFamily: af_packet, af_inet. //af_inet6, type +++SocketOptionEnum: // Socket level so_broadcast, // Allows transmission of broadcast messages on the socket. so_debug, // Records debugging information. so_dontroute, // Does not route: sends directly to interface. // Not supported on ATM sockets (results in an error). so_keepaline, // Sends keep-alives. Not supported on ATM sockets (results in an error). so_linger, // Lingers on close if unsent data is present. so_rcvbuf, // Specifies the total per-socket buffer space reserved for receives. // This is unrelated to SO_MAX_MSG_SIZE or the size of a TCP window. so_reuseaddr, // Allows the socket to be bound to an address that is already in use. // (See bind.) Not applicable on ATM sockets. so_sndbuf, // Specifies the total per-socket buffer space reserved for sends. // This is unrelated to SO_MAX_MSG_SIZE or the size of a TCP window. // TCP level tcp_nodelay. // Disables the Nagle algorithm for send coalescing. type +++SocketAddr: none, sockaddr_in(+++InternetSocketAddress), sockaddr_ll(+++PacketSocketAddress). type +++AllSocketType: sock_raw, sock_dgram, sock_stream. define Word16 +++socket_proto_to_value ( PacketSocketProtocol proto ) = if proto is { eth_p_all then 0x0003, /* Every packet (be careful!!!) */ eth_p_loop then 0x0060, /* Ethernet Loopback packet */ eth_p_ip then 0x0800, /* Internet Protocol packet */ eth_p_arp then 0x0806, /* Address Resolution packet */ eth_p_rarp then 0x8035, /* Reverse Addr Res packet */ eth_p_8021Q then 0x8100, /* 802.1Q VLAN Extended Header */ eth_p_ipx then 0x8137, /* IPX over DIX */ eth_p_ipv6 then 0x86dd, /* IPv6 over bluebook */ eth_p_ppp_disc then 0x8863, /* PPPoE discovery messages */ eth_p_ppp_ses then 0x8864, /* PPPoE session messages */ eth_p_mpls_uc then 0x8847, /* MPLS Unicast traffic */ eth_p_mpls_mc then 0x8848, /* MPLS Multicast traffic */ eth_p_atmmpoa then 0x884c, /* MultiProtocol Over ATM */ eth_p_atmfate then 0x8884, /* Frame-based ATM Transport over Ethernet */ eth_p_aoe then 0x88a2, /* ATA over Ethernet */ eth_p_tipc then 0x88ca, /* TIPC */ eth_p_802_3 then 0x0001, /* Dummy type for 802.3 frames */ eth_p_ax25 then 0x0002, /* Dummy protocol id for AX.25 */ eth_h_802_2 then 0x0004, /* 802.2 frames */ eth_h_tr_802_2 then 0x0011, /* 802.2 frames */ }. define PacketSocketProtocol +++value_to_socket_proto ( Word16 proto ) = if proto = 0x0003 then eth_p_all else if proto = 0x0060 then eth_p_loop else if proto = 0x0800 then eth_p_ip else if proto = 0x0806 then eth_p_arp else if proto = 0x8035 then eth_p_rarp else if proto = 0x8100 then eth_p_8021Q else if proto = 0x8137 then eth_p_ipx else if proto = 0x86dd then eth_p_ipv6 else if proto = 0x8863 then eth_p_ppp_disc else if proto = 0x8864 then eth_p_ppp_ses else if proto = 0x8847 then eth_p_mpls_uc else if proto = 0x8848 then eth_p_mpls_mc else if proto = 0x884c then eth_p_atmmpoa else if proto = 0x8884 then eth_p_atmfate else if proto = 0x88a2 then eth_p_aoe else if proto = 0x88ca then eth_p_tipc else if proto = 0x0001 then eth_p_802_3 else if proto = 0x0002 then eth_p_ax25 else if proto = 0x0004 then eth_h_802_2 else if proto = 0x0011 then eth_h_tr_802_2 else eth_p_all. define Result(SocketError, RWStream) +++bsd_create_socket ( +++SocketFamily domain, +++AllSocketType type, Word32 protocol ) = +++avm{ bsd_create_socket }. define Result(SocketOptionError, One) +++bsd_setsockopt ( RWStream socket, SocketOption option ) = +++avm{ bsd_setsockopt }. define Result(SocketOptionError, SocketOption) +++bsd_getsockopt ( RWStream socket, +++SocketOptionEnum option ) = +++avm{ bsd_getsockopt }. define Result(BindError, One) +++bsd_bind ( RWStream socket, +++SocketAddr sockname ) = +++avm{ bsd_bind }. define Result(RecvError, (ByteArray, +++SocketAddr)) +++bsd_recvfrom ( RWStream socket, Word32 size, +++SocketFamily family, // this parameter is need only to known which C struct to use // for recvfrom() call and wich alternative of +++SocketAddr to return. RecvFlags flags ) = +++avm{ bsd_recvfrom }. define Result(SendError, Word32) +++bsd_sendto ( RWStream socket, ByteArray data, +++SocketAddr dest, SendFlags flags ) = +++avm{ bsd_sendto }. // ----------------------------------------------------------------------------- *** (6.8.4) Definition and implementation of public types and functions // ----------------------------------------------------------------------------- public type RecvFlags: recv_flags(Word8). implementation identical to Word8 public type SendFlags: send_flags(Word8). public define SendFlags no_flag = send_flags(0). public define SendFlags msg_dontroute = send_flags(1). public define SendFlags msg_more = send_flags(2). public define SendFlags msg_nosignal = send_flags(4). public define SendFlags msg_out_of_band = send_flags(8). public define RecvFlags no_flag = recv_flags(0). public define RecvFlags msg_peek = recv_flags(1). public define RecvFlags msg_out_of_band = recv_flags(2). public define RecvFlags RecvFlags x | RecvFlags y = +++avm{ (bit_or . 8) }. public define SendFlags SendFlags x | SendFlags y = +++avm{ (bit_or . 8) }. // ----------------------------------------------------------------------------- *** (6.8.5) Packet sockets functions. // ----------------------------------------------------------------------------- public define PhysicalAddress mac_address(Word8 b0, Word8 b1, Word8 b2, Word8 b3, Word8 b4, Word8 b5) = physical_address(6, word64(word32(word16(b0, b1), word16(b2, b3)), word32(word16(b4, b5), 0))). public define PhysicalAddress generic_address(Word8 b0, Word8 b1, Word8 b2, Word8 b3, Word8 b4, Word8 b5, Word8 b6, Word8 b7) = physical_address(8, word64(word32(word16(b0, b1), word16(b2, b3)), word32(word16(b4, b5), word16(b6, b7)))). define Result(SocketOptionError, One) +++apply_socket_options ( RWStream sock, List(SocketOption) options, ) = if options is { [] then ok(unique), [h . t] then if +++bsd_setsockopt(sock, h) is { error(e) then error(e), ok(_) then +++apply_socket_options(sock, t) } }. public define Result(CreateSocketError, PacketSocket) create_packet_socket ( PacketSocketType type, PacketSocketProtocol proto, List(SocketOption) options, Maybe(PacketSocketAddress) mb_addr, ) = with sock_type = (+++AllSocketType)if type is { sock_raw then sock_raw, sock_dgram then sock_dgram, }, if +++bsd_create_socket(af_packet, sock_type, word32(0, +++socket_proto_to_value(proto))) is { error(e) then error(socket_error(e)), ok(sock) then if +++apply_socket_options(sock, options) is { error(e) then error(option_error(e)), ok(_) then if mb_addr is { failure then ok(packetSocket(type, proto, sock)), success(addr) then if physaddr(addr) is physical_address(halen, the_addr) then if +++bsd_bind(sock, sockaddr_ll(packet_sockaddr(+++socket_proto_to_value(protocol(addr)), ifindex(addr), hatype(addr), pkttype(addr), halen, the_addr))) is { error(e) then error(bind_error(e)), ok(_) then ok(packetSocket(type, proto, sock)) } } } }. public define Result(RecvError, (ByteArray, PacketSocketAddress)) recvfrom ( PacketSocket socket, Word32 size, RecvFlags flags ) = if +++bsd_recvfrom(sock(socket), size, af_packet, flags) is { error(e) then error(e), ok(r) then if r is (ba, sa) then if sa is { none then error(other_error), sockaddr_in(_) then error(other_error), sockaddr_ll(ppsa) then with psa = packet_sockaddr(+++value_to_socket_proto(protocol(ppsa)), ifindex(ppsa), hatype(ppsa), pkttype(ppsa), physical_address(halen(ppsa), addr(ppsa))), ok((ba, psa)) } }. public define Result(SendError, Word32) sendto ( PacketSocket socket, ByteArray data, Maybe(PacketSocketAddress) mb_dest, SendFlags flags ) = with sa = if mb_dest is { failure then none, success(dest) then with paddr = physaddr(dest), sockaddr_ll(packet_sockaddr(+++socket_proto_to_value(protocol(dest)), ifindex(dest), hatype(dest), pkttype(dest), phys_halen(paddr), phys_address(paddr))) }, +++bsd_sendto(sock(socket), data, sa, flags). // ----------------------------------------------------------------------------- *** (6.8.6) Internet sockets functions. // ----------------------------------------------------------------------------- // TODO // ----------------------------------------------------------------------------- // ----------------------------------------------------------------------------- *** (7) Miscellaneous tools. *** (7.1) Executing an operating system command ('execute'). public define Maybe(Word8) execute ( Maybe(String) mb_execution_directory, String program_name, List(String) operands ) = +++avm{ do_execute }. public define Maybe(Word8) execute ( String program_name, List(String) operands ) = execute(failure,program_name,operands). public define Maybe(Word8) execute ( String execution_directory, String program_name, List(String) operands ) = execute(success(execution_directory),program_name,operands). *** (7.1) Capturing the output of 'execute'. public type ExecuteControl: +++execute_control(WStream process_stdin, RStream process_stdout, RStream process_stderr, +++StructPtr(Exec)). public define Maybe(ExecuteControl) execute ( Maybe(String) mb_execution_directory, String program_name, List(String) operands ) = +++avm{ do_execute_capture }. public define ExecuteStatus check_execute_status ( ExecuteControl ec ) = +++avm{ check_execute_status }. *** (7.2) Random numbers ('random'). public define Word32 random(Word32 n) = +++avm{ do_random }. *** (7.3) Dynamic Variables ('Var(T)', 'MVar(T)', 'var', 'mvar' and monitoring). *** (7.3.1) Creating, reading and writing. public define Var($T) var($T init) = +++avm{ create_var kill_next_instr }. public define Word32 var_id(Var($T) v) = +++avm{ var_id }. *** (7.3.2) Multiple dynamic variables. define MVar($T) +++mvar(Word32 n, $T init, Word32 bw) = +++avm{ create_mvar kill_next_instr kill_next_instr kill_next_instr }. public define MVar($T) mvar ( Word32 n, // number of slots in the variable you want to create $T init // initial value for all slots ) = if n +< 1 then +++mvar(1,init,bit_width($T)) else +++mvar(n,+++vcopy(n-1,init),bit_width($T)). public define Word32 length(MVar($T) mv) = +++avm{ mvar_length }. public define Word32 mvar_id(MVar($T) mv) = +++avm{ var_id }. *** (7.3.3) Monitoring. public type MonitoringTicket($T): +++ticket(Var($T) +++variable, One -> One +++monitor, Word32 +++index). +++ticket(MVar($T) +++variable, Word32 -> One +++monitor, Word32 +++index). public define MonitoringTicket($T) register_monitor ( Var($T) variable, One -> One monitor ) = +++avm{ register_monitor (mcollapse 2 . 0) kill_next_instr kill_next_instr }. public define MonitoringTicket($T) register_monitor ( MVar($T) multiple_variable, Word32 -> One monitor ) = +++avm{ register_mmonitor (mcollapse 2 . 0) kill_next_instr kill_next_instr }. *** (7.4) Date and time ('Date_and_Time', 'now', 'convert_time'). define Word32 +++now = +++avm{ now }. public define Int now = to_Int(+++now ). type OldUTime: old_utime(Word32 seconds, Word32 microseconds). define OldUTime +++unow = +++avm{ now64 }. public define UTime unow = if +++unow is old_utime(a, b) then utime(to_Int(a), to_Int(b)). type Old_Date_and_Time: old_date_and_time(Word32 year, Word32 month, // from 1 = January to 12 = December Word32 day, // from 1 to 31 Word32 hour, // from 0 to 23 Word32 minute, // from 0 to 59 Word32 second, // from 0 to 59 Word32 week_day, // from 0 = sunday to 6 = saturday Word32 year_day, // from 0 = January 1st, to at most 365 Bool daylight_saving_time). // if 'true' daylight saving time is applied define Old_Date_and_Time +++convert_time(Word32 t) = +++avm{ convert_time_from_int }. define Word32 +++convert_time(Old_Date_and_Time d) = +++avm{ convert_time_to_int }. public define Date_and_Time convert_time(Int t) = with dt = +++convert_time(truncate_to_Word32(t)), if dt is old_date_and_time(y, m, d, h, mn, s, w, yd, dst) then date_and_time(to_Int(y), to_Int(m), to_Int(d), to_Int(h), to_Int(mn), to_Int(s), to_Int(w), to_Int(yd), dst). public define Int convert_time(Date_and_Time dt) = if dt is date_and_time(y, m, d, h, mn, s, w, yd, dst) then to_Int(+++convert_time(old_date_and_time(truncate_to_Word32(y), truncate_to_Word32(m), truncate_to_Word32(d), truncate_to_Word32(h), truncate_to_Word32(mn), truncate_to_Word32(s), truncate_to_Word32(w), truncate_to_Word32(yd), dst))). define One set_time(OldUTime time) = +++avm{ set_time }. public define One set_time(UTime time) = if time is utime(a, b) then set_time(old_utime(truncate_to_Word32(a), truncate_to_Word32(b))) . public define One set_time_zone(String time_zone_name) = +++avm{ set_time_zone }. *** (7.5) Other tools ('print', boolean '&', 'append', 'reverse'). public define Bool Bool x & Bool y = if x then y else false. public define List($T) reverse_append ( List($T) l1, List($T) l2, ) = if l1 is { [ ] then l2, [h . t] then reverse_append(t,[h . l2]) }. public define List($T) reverse ( List($T) l ) = reverse_append(l,[]). public define List($T) append ( List($T) l1, List($T) l2 ) = if l1 is { [ ] then l2, [h . t] then [h . append(t,l2)] }. public define Bool member ( List($T) l, $T x ) = if l is { [ ] then false, [first . others] then if x = first then true else member(others,x) }. *** (7.6) Mapping a function to all elements of a list ('map'). public define List($B) map ( $A -> $B f, // C equivalent: $B (*f)($A) List($A) l ) = if l is { [ ] then [ ], [first_arg . others_args] then with x = f(first_arg), // this is to force order of execution in the case // f makes a side effect. [x . map(f,others_args)] }. *** (7.7) Reading a password from standard input ('get_password'). public define String get_password = +++avm{ get_password }. *** (7.8) Loading .adm modules dynamically. Extracting a Word32 which is at a given position within a byte array. define Word32 +++extract_Word32 ( ByteArray b, Int position ) = if system_endianness is { little_endian then word32(word16(force_nth(position,b),force_nth(position+1,b)), word16(force_nth(position+2,b),force_nth(position+3,b))) big_endian then word32(word16(force_nth(position+3,b),force_nth(position+2,b)), word16(force_nth(position+1,b),force_nth(position,b))) }. define Word32 +++condensed_version_number = +++avm{ condensed_version_number }. define String +++format_condensed_version_number // see include/AnubisSupport.h ( Word32 cvn ) = to_decimal(cvn&0xF)+"."+to_decimal((cvn>>4)&0xFF)+"."+to_decimal((cvn>>12)&0xFF)+"."+to_decimal((cvn>>20)&0xFFF). Three syscalls and one instruction needed by load_adm (+++type_desc is not a syscall because $T is not a term). +++relocate_code returns the index of the newly created module. define Word32 +++relocate_code (Word32 flags, ByteArray code, Word32 starting_point) = +++avm{ relocate_code }. define Word32 +++byte_array_count(ByteArray b) = +++avm{ byte_array_count }. define $T +++execute_module (ByteArray module, Word32 starting_point) = +++avm{ execute_module }. public define LoadAdm($T) load_adm ( String adm_file_name // path ) = load_adm(adm_file_name,10). define Maybe(RStream) +++module_file ( String path, ReadFileMode mode ) = if file(path,mode) is { failure then file(my_anubis_directory+"/modules/"+path,mode) success(f) then success(f) }. define One +++remove_zombie_module(Word32 index) = +++avm{ remove_zombie_module }. +++remove_zombie_module (applied to the index of a module) is necessary for the following reason. In case the execution of the secondary module does not produce any reference to the module, the counter of the byte array in the module is decremented to 0 by a 'del_stack_ptr' instruction at the end of +++load_adm. However, this instruction does not see the module itself (as a slot of the 'modules' array; see 'dynamic_module.cpp'), i.e. the module is not removed from the array. In this case, we get a 'zombie' module which must be eliminated immediately after the execution of +++load_adm, otherwise illegal things can happen. In the case the execution of the module creates at least one reference to the module, the counter of the byte array does not decrement to 0. In this case, there is no problem since from this point, the byte array is never again seen as a byte array. Only the module is visible to the system. The module will be collected by a normal 'del_function' instruction, indeed able to see the module itself. public define (Maybe((Word32,Word32)), // index of module if any and byte array count LoadAdm($T)) +++load_adm ( String adm_file_name, // path Int timeout_val // value of timeout ) = with type_desc = +++type_desc($T), // compute the expected type description // // open the module file // if +++module_file(adm_file_name,read) is { failure then (failure,file_not_found), // // read 28 + 6*4 + 20 bytes (see compiler/src/output.cpp for explanations) // // 28 + 6*4 + 20 = 72 // success(f) then if read(f,72,timeout_val) is // read { error then (failure,read_error), timeout then (failure,timeout), ok(preambule) then if +++non_equal(length(preambule),72) then (failure,read_error) // // check version numbers // else with read_version_number = +++extract_Word32(preambule,28), if +++non_equal(+++condensed_version_number,read_version_number) then (failure,bad_version(+++format_condensed_version_number(+++condensed_version_number), +++format_condensed_version_number(read_version_number))) // // get size of type description // else with type_desc_size = +++extract_Word32(preambule,40), // 40 = 28 + 3*4 // // read type description // if read(f,to_Int(type_desc_size),timeout_val) is { error then (failure,read_error), timeout then (failure,timeout), ok(read_desc) then if +++non_equal(length(read_desc),to_Int(type_desc_size)) then (failure,read_error) else with rd = to_string(read_desc), if +++non_equal(rd,type_desc) then (failure,wrong_type(type_desc,rd)) else with code_size = to_Int(+++extract_Word32(preambule,44)), // 44 = 28 + 4*4 // // read code of module // if read(f,code_size,timeout_val) is { error then (failure,read_error), timeout then (failure,timeout), ok(code) then // // read checksum // if read(f,20,timeout_val) is { error then (failure,read_error), timeout then (failure,timeout), ok(chksum) then // // compare checksums // if +++non_equal(sha1(extract(preambule,28,72)+read_desc+code),chksum) then (failure,file_damaged) else // // relocate code and install it into the modules array // with flags = +++extract_Word32(preambule,36), // 36 = 28 + 2*4 start = +++extract_Word32(preambule,48), // 48 = 28 + 5*4 index = +++relocate_code(flags,code,start), // // execute the module from the starting point // with datum = +++execute_module(code,start), (success((index,+++byte_array_count(code))),ok(datum)) // at least ! } } } } }. public define LoadAdm($T) load_adm ( String adm_file_name, // path without the '.adm' extension Int timeout_val // value of timeout ) = if +++load_adm(adm_file_name,timeout_val) is (mb_index_count,result) then if mb_index_count is { failure then result, success(ic) then if ic is (index,count) then if count = 2 then (+++remove_zombie_module(index); result) else result }. *** (8) Serialization, saving and transmitting data. *** (8.1) Serializing and unserializing. public define ByteArray serialize($T d) = +++serialize(d). public define Maybe($T) unserialize(ByteArray s) = +++unserialize(s). *** (8.2) Saving and retrieving data ('save' and 'retrieve'). public define SaveResult save ( $T datum, String file_name ) = if write_to_file(file_name,serialize(datum)) is { cannot_open_file then cannot_open_file, write_error(_) then write_error, ok then ok }. public define RetrieveResult($T) retrieve ( String file_name ) = if read_from_file(file_name) is { cannot_find_file then cannot_find_file, read_error(_) then read_error, ok(ba) then if (Maybe($T))unserialize(ba) is { failure then type_error, success(d) then ok(d) } }. *** (8.3) Transmitting data. *** (9) Built-in cryptography. *** (9.1) Secure hash functions ('md5' and 'sha1'). define ByteArray +++md5(ByteArray s) = +++avm{ md5_hash }. define ByteArray +++sha1(ByteArray s) = +++avm{ sha1_hash }. public define ByteArray md5($T d) = +++md5(serialize(d)). public define ByteArray sha1($T d) = +++sha1(serialize(d)). *** (9.2) Symmetric cryptography ('blowfish_encrypt', 'blowfish_decrypt'). to do: make unit tests for blowfish (various sizes). public type +++BlowfishKey: +++blowfish_key(ByteArray). define +++BlowfishKey +++create_blowfish_key ( String key ) = +++avm { create_blowfish_key }. define One +++blowfish_encrypt_block ( +++BlowfishKey key, ByteArray source, ByteArray dest, Word32 offset ) = +++avm { blowfish_encrypt_block }. define One +++blowfish_decrypt_block ( +++BlowfishKey key, ByteArray source, ByteArray dest, Word32 offset ) = +++avm { blowfish_decrypt_block }. define ByteArray +++make_blowfish_dest_for_encryption ( Word32 size ) = with remainder = size&7, // size (mod 8), new_size = (if remainder = 0 then size else size + (8 - remainder)) + 1, constant_byte_array(to_Int([new_size]),0). Notice that the size of the encrypted byte array is always 1 mod 8. This is to be interpreted as an array of 8 bytes blocks, plus an extra byte whose value indicates the number of bytes in the last block of the original. Encrypting and decrypting byte arrays: define Word8 +++bytes_in_last_block ( Word32 s ) = with rem = s&7, if rem = 0 // (s (mod 8)) = 0 then (Word8)8 else if rem is word32(l,_) then if l is word16(l1,_) then l1. // truncate_to_word8(s (mod 8)). define ByteArray +++blowfish_encrypt ( +++BlowfishKey key, ByteArray source, ByteArray dest, Word32 i ) = if i >=+ truncate_to_Word32(length(source)) then ( forget(put(dest,to_Int([i]),+++bytes_in_last_block(truncate_to_Word32(length(source))))); dest) else ( +++blowfish_encrypt_block(key,source,dest,i); +++blowfish_encrypt(key,source,dest,i+8)). define Word32 word8_to_word32 ( Word8 x ) = word32(word16(x,0),0). define ByteArray +++blowfish_decrypt ( +++BlowfishKey key, ByteArray source, ByteArray dest, Word32 i, ) = if i >=+ (truncate_to_Word32(length(source)) - 1) then ( truncate(dest,to_Int(i+word8_to_word32(force_nth(to_Int(i),source))-8)); dest) else ( +++blowfish_decrypt_block(key,source,dest,i); +++blowfish_decrypt(key,source,dest,i+8)). We provide two public functions, one for encryption and one for decryption: public define ByteArray blowfish_encrypt ( String key, $T datum ) = with source = serialize(datum), dest = +++make_blowfish_dest_for_encryption(truncate_to_Word32(length(source))), +++blowfish_encrypt(+++create_blowfish_key(key),source,dest,0). public define Maybe($T) blowfish_decrypt ( String key, ByteArray source, ) = if (truncate_to_Word32(length(source))&7) = 1 // (length(source) (mod 8)) = 1 then ( with dest = constant_byte_array(length(source),0), unserialize(+++blowfish_decrypt(+++create_blowfish_key(key),source,dest,0)) ) else failure. *** (9.3) SSL ('Secure Sockets Layer'). *** (9.3.1) SSL connections. public type SSL_Connection: +++ssl_connection(+++StructPtr(SSL), // encapsulated SSL object from OpenSSL RWStream, // underlying TCP/IP socket String hostname). // 'common name' of host we are connected to *** (9.3.2) X.509 Certificates. public type X509: +++x509(+++StructPtr(X509)). define String +++to_string ( +++StructPtr(X509) ptr ) = +++avm{ print_X509 }. public define String to_string ( X509 certificate ) = if certificate is +++x509(ptr) then +++to_string(ptr). define Result_trust_X509_for_ever +++trust_for_ever ( +++StructPtr(X509) ptr ) = +++avm{ trust_X509_for_ever }. public define Result_trust_X509_for_ever trust_for_ever ( X509 cert ) = if cert is +++x509(ptr) then +++trust_for_ever(ptr). *** (9.3.3) Opening an SSL connection. public type +++SSL_client_wrap_Result: +++cannot_create_SSL_object, +++cannot_connect_under_SSL, +++ok(+++StructPtr(SSL)). define +++SSL_client_wrap_Result +++ssl_client_wrap ( RWStream tcp_conn ) = +++avm{ ssl_client_wrap }. define Bool +++check_certificate_chain ( +++StructPtr(SSL) ssl_obj, String server_name ) = +++avm{ check_certificate_chain }. define Maybe(X509) +++get_ssl_certificate ( +++StructPtr(SSL) ssl_obj ) = +++avm{ get_ssl_certificate }. public define Result(SSLConnectError,SSL_Connection) open_SSL_connection ( String server_name, // 'common name' of server (such as "www.mybank.com") // this is required for certificate checking RWStream tcp_connection, (Maybe(X509)) -> Bool accept_policy // your policy for accepting the server certificate in // case of an invalid, non trusted or missing certificate ) = if +++ssl_client_wrap(tcp_connection) is { +++cannot_create_SSL_object then error(cannot_create_SSL_object), +++cannot_connect_under_SSL then error(cannot_connect_under_SSL), +++ok(ssl_obj) then if +++check_certificate_chain(ssl_obj,server_name) then ok(+++ssl_connection(ssl_obj,tcp_connection,server_name)) else if accept_policy(+++get_ssl_certificate(ssl_obj)) then ok(+++ssl_connection(ssl_obj,tcp_connection,server_name)) else error(cannot_trust_server_certificate) }. public define Result(SSLConnectError,SSL_Connection) open_SSL_connection ( String server_name, // 'common name' of server (such as "www.mybank.com") // this is required for certificate checking Word32 ip_address, // numeric IP address of server Word32 ip_port, // for example 443 for HTTPS (Maybe(X509)) -> Bool accept_policy // your policy for accepting the server certificate in // case of an invalid, non trusted or missing certificate ) = if connect(ip_address,ip_port) is { error(msg) then error(tcp_error(msg)), ok(tcp_conn) then open_SSL_connection(server_name,tcp_conn,accept_policy) }. *** (9.3.4) Reading and writing with SSL connections. to do: 'read' Word32 --> Int and Word32 --> Time. define Maybe(ByteArray) +++read ( SSL_Connection conn, Word32 n, // maximum number of bytes to read Word32 timeout // in seconds ) = +++avm{ ssl_read_byte_array }. define Maybe(String) +++read ( SSL_Connection conn, Word32 n, Word32 timeout ) = +++avm{ ssl_read_string }. public define Maybe(ByteArray) read ( SSL_Connection conn, Int n, // maximum number of bytes to read Int timeout // in seconds ) = +++read(conn, truncate_to_Word32(n), truncate_to_Word32(timeout)). public define Maybe(String) read ( SSL_Connection conn, Int n, Int timeout ) = +++read(conn, truncate_to_Word32(n), truncate_to_Word32(timeout)). to do: 'write' should return Maybe(Int). define Maybe(Word32) +++write ( SSL_Connection conn, ByteArray data ) = +++avm{ ssl_write_byte_array }. define Maybe(Word32) +++write ( SSL_Connection conn, String data ) = +++avm{ ssl_write_string }. public define Maybe(Int) write ( SSL_Connection conn, ByteArray data ) = if +++write(conn, data) is success(v) then success(to_Int(v)) else failure. public define Maybe(Int) write ( SSL_Connection conn, String data ) = if +++write(conn, data) is success(v) then success(to_Int(v)) else failure. *** (9.3.5) Creating an SSL server. define Maybe(+++StructPtr(SSL)) +++ssl_server_wrap ( RWStream tcp_conn ) = +++avm{ ssl_server_wrap }. define One +++handle_ssl_request ( RWStream tcp_conn, String server_name, (SSL_Connection) -> One handler ) = if +++ssl_server_wrap(tcp_conn) is { failure then unique, success(ssl_obj) then handler(+++ssl_connection(ssl_obj,tcp_conn,server_name)) }. define One +++run_ssl_server ( +++Listener l, Var(Int) num_conn, (RWStream) -> Bool can_accept, String server_name, (SSL_Connection) -> One handler, Var(Bool) shutdown_required, Word8 handler_priority ) = if *shutdown_required then unique else if +++accept_connection(l) is { +++listener_is_down then unique, /* exit the 'infinite' loop */ +++cannot_open_pending_connection then +++run_ssl_server(l,num_conn,can_accept,server_name,handler, shutdown_required,handler_priority), /* continue to listen */ +++ok(tcp_conn) then /* TCP connection accepted */ (if can_accept(tcp_conn) then (delegate (handler_priority) ( /* delegate SSL stuff and client servicing */ num_conn <- *num_conn + 1; +++handle_ssl_request(tcp_conn,server_name,handler); num_conn <- *num_conn - 1 ), unique) else unique); +++run_ssl_server(l,num_conn,can_accept,server_name, handler,shutdown_required,handler_priority) /* and continue to listen */ }. public define StartServerResult start_ssl_server ( Word32 ip_addr, Word32 ip_port, (RWStream) -> Bool can_accept, String server_name, Server -> ((SSL_Connection) -> One) handler, Var(Bool) shutdown_required, Word8 listener_priority, Word8 handler_priority ) = if +++listener(ip_addr,ip_port) is { +++cannot_create_the_socket then cannot_create_the_socket, +++cannot_bind_to_port then cannot_bind_to_port, +++cannot_listen_on_port then cannot_listen_on_port, +++ok(l) then with num_conn = var((Int)0), s = +++server(l,num_conn), delegate (listener_priority) +++run_ssl_server(l,num_conn,can_accept,server_name,handler(s),shutdown_required,handler_priority), ok(s) }. These are just for backwards compatibility: public define StartServerResult start_ssl_server ( Word32 ip_addr, Word32 ip_port, (RWStream) -> Bool can_accept, String server_name, Server -> ((SSL_Connection) -> One) handler, (One) -> One notify, Var(Bool) shutdown_required ) = start_ssl_server(ip_addr,ip_port,can_accept,server_name,handler,shutdown_required,255,255). public define StartServerResult start_ssl_server ( Word32 ip_addr, Word32 ip_port, String server_name, Server -> ((SSL_Connection) -> One) handler, (One) -> One notify, Var(Bool) shutdown_required ) = start_ssl_server(ip_addr,ip_port,(RWStream s) |-> true,server_name,handler,notify,var((Bool)false)). public define StartServerResult start_ssl_server ( Word32 ip_addr, Word32 ip_port, String server_name, Server -> ((SSL_Connection) -> One) handler, (One) -> One notify ) = start_ssl_server(ip_addr,ip_port,(RWStream s) |-> true,server_name,handler,notify,var((Bool)false)). public define (Word32,Word32) local_SSL_address_and_port (SSL_Connection connection) = +++avm{ local_SSL_addr_port }. public define (Word32,Word32) remote_SSL_address_and_port (SSL_Connection connection) = +++avm{ remote_SSL_addr_port }. *** (9.4) Simple (non cryptographic) hashing. define Word32 +++simple_hash(Word32 n, ByteArray b) = +++avm { simple_hash }. public define Word32 simple_hash ( Word32 number_of_bits, $T datum ) = +++simple_hash(number_of_bits,serialize(datum)). *** (10) Images. *** (10.1) Types of images. public type RGBAImage: +++image(Word32 width, Word32 height, ByteArray). public type BitMapImage: +++image(Word32 width, Word32 height, ByteArray). *** (10.2) Creating images. define RGBAImage +++create_rgba_image(Word32 width, Word32 height, RGBA background) = +++avm{ create_rgba }. define BitMapImage +++create_bitmap_image(Word32 width, Word32 height, Bit background) = +++avm{ create_bitmap }. public define RGBAImage create_rgba_image(Int width, Int height, RGBA background) = +++create_rgba_image(truncate_to_Word32(width), truncate_to_Word32(height), background). public define BitMapImage create_bitmap_image(Int width, Int height, Bit background) = +++create_bitmap_image(truncate_to_Word32(width), truncate_to_Word32(height), background). *** (10.3) Drawing into images. *** (10.3.1) Drawing pixels. define One +++draw_pixel ( RGBAImage image, Word32 x, Word32 y, RGBA color ) = +++avm{ draw_pixel_rgba }. define One +++draw_pixel ( BitMapImage image, Word32 x, Word32 y, BitPaintMode how ) = +++avm{ draw_pixel_bitmap }. public define One draw_pixel ( RGBAImage image, Int x, Int y, RGBA color ) = +++draw_pixel(image, truncate_to_Word32(x), truncate_to_Word32(y), color). public define One draw_pixel ( BitMapImage image, Int x, Int y, BitPaintMode how ) = +++draw_pixel(image, truncate_to_Word32(x), truncate_to_Word32(y), how). *** (10.3.2) Getting pixels. define RGBA +++get_pixel ( RGBAImage image, Word32 x, Word32 y ) = +++avm{ get_pixel_rgba }. define Bit +++get_pixel ( BitMapImage image, Word32 x, Word32 y ) = +++avm{ get_pixel_bitmap }. public define RGBA get_pixel ( RGBAImage image, Int x, Int y ) = +++get_pixel(image, truncate_to_Word32(x), truncate_to_Word32(y)). public define Bit get_pixel ( BitMapImage image, Int x, Int y ) = +++get_pixel(image, truncate_to_Word32(x), truncate_to_Word32(y)). *** (10.3.3) Drawing rectangles. // Helper public define Rectangle rect ( Int x, Int y, Int u, Int v ) = rect(truncate_to_Word32(x), truncate_to_Word32(y), truncate_to_Word32(u), truncate_to_Word32(v)). public define One draw_rectangle ( RGBAImage destination, Rectangle rect, RGBA color_of_rectangle ) = +++avm{ draw_rectangle_to_rgba }. public define One draw_rectangle ( BitMapImage destination, Rectangle rect, BitPaintMode how ) = +++avm{ draw_rectangle_to_bitmap }. *** (10.3.4) Cropping and encrusting, rotating and flipping. define One +++crop_and_encrust // encrusting an RGBA image into an RGBA image ( RGBAImage source, RGBAImage destination, Rectangle cropped, Word32 a, // position in destination Word32 b, Dihedral4 t ) = +++avm{ crop_and_encrust_rgba_rgba }. define One +++crop_and_encrust // encrusting a BitMap image into an RGBA image ( BitMapImage source, RGBA filter, RGBAImage destination, Rectangle cropped, Word32 a, // position in destination Word32 b, Dihedral4 t ) = +++avm{ crop_and_encrust_bitmap_rgba }. define One +++crop_and_encrust ( BitMapImage source, BitMapImage destination, Rectangle cropped, Word32 a, // position in destination Word32 b, BitPaintMode paint_mode, Dihedral4 t ) = +++avm{ crop_and_encrust_bitmap_bitmap }. public define One crop_and_encrust // encrusting an RGBA image into an RGBA image ( RGBAImage source, RGBAImage destination, Rectangle cropped, Int a, // position in destination Int b, Dihedral4 t ) = +++crop_and_encrust(source, destination, cropped, truncate_to_Word32(a), truncate_to_Word32(b), t). public define One crop_and_encrust // encrusting a BitMap image into an RGBA image ( BitMapImage source, RGBA filter, RGBAImage destination, Rectangle cropped, Int a, // position in destination Int b, Dihedral4 t ) = +++crop_and_encrust(source, filter, destination, cropped, truncate_to_Word32(a), truncate_to_Word32(b), t). public define One crop_and_encrust ( BitMapImage source, BitMapImage destination, Rectangle cropped, Int a, // position in destination Int b, BitPaintMode paint_mode, Dihedral4 t ) = +++crop_and_encrust(source, destination, cropped, truncate_to_Word32(a), truncate_to_Word32(b), paint_mode, t). *** (10.3.5) Drawing system characters. public type SystemFont: sys_font(+++StructPtr(SysFont)). public define Maybe(SystemFont) load_system_font ( String font_name ) = +++avm{ load_system_font }. public define Word32 draw_system_character ( RGBAImage destination, // where to draw the character Rectangle clip, // clipping rectangle on destination Word32 x, // position of reference point of Word32 y, // characters in destination SystemFont font, Word32 character_code, RGBA character_color ) = +++avm{ draw_system_char_rgba }. public define Word32 draw_system_character ( BitMapImage destination, // where to draw the character Rectangle clip, // clipping rectangle on destination Word32 x, // position of reference point of Word32 y, // characters in destination SystemFont font, Word32 character_code, BitPaintMode paint_mode ) = +++avm{ draw_system_char_bitmap }. *** (10.3.6) System characters and fonts informations. public define SystemFontInfo get_font_info(SystemFont font) = +++avm{ get_font_info }. public define SystemCharacterInfo get_char_info(SystemFont font, Word8 code) = +++avm{ get_char_info }. *** (10.1) The type 'HostImage'. public type HostImage: +++image(+++StructPtr(HostImage)). public define (Word32,Word32) size ( HostImage im ) = +++avm{ host_image_size }. public define HostImage to_host_image ( RGBAImage image, Word32 reduction_factor ) = +++avm{ rgba_to_host_image }. public define One draw_pixel ( HostImage image, Word32 x, Word32 y, RGB color ) = +++avm{ draw_pixel_host_image }. public define One draw_rectangle ( HostImage destination, Rectangle rect, RGB color_of_rectangle ) = +++avm{ draw_rectangle_to_host_image }. public define Word32 draw_system_character ( HostImage destination, // where to draw the character Rectangle clip, // clipping rectangle on destination Word32 x, // position of reference point of Word32 y, // characters in destination SystemFont font, Word32 character_code, RGB character_color ) = +++avm{ draw_system_char_host_image }. *** (10.2) Handling JPEG/JFIF image files. *** (10.2.1) Converting to 'HostImage'. public define HostImage to_host_image ( JPEG_BitMapImage image, Word32 reducing_factor ) = +++avm{ jpeg_bitmap_to_host_image }. *** (10.2.2) Converting to 'RGBAImage'. public define RGBAImage to_RGBA ( JPEG_BitMapImage image, Word32 reducing_factor ) = +++avm{ jpeg_bitmap_to_rgba_image }. public define JPEG_BitMapImage to_JPEG ( RGBAImage image ) = +++avm{ rgba_image_to_jpeg_bitmap }. *** (10.2.2) Writing (creating) a JPEG file. public type +++JPEG_compress_info: +++jpeg_compress_info(ByteArray jpeg_compress_struct, ByteArray jpeg_error_mgr). define Maybe(+++JPEG_compress_info) +++create_JPEG_compress_info ( Word32 image_width, Word32 image_height, JPEG_ImageFormat format, Word32 quality, WStream output_file ) = +++avm{ create_JPEG_compress_info }. define One +++jpeg_write_scanline ( +++JPEG_compress_info cinfo, ByteArray samples, Word32 start // starting point in 'samples' ) = +++avm{ jpeg_write_scanline }. define One +++jpeg_write_scanlines ( +++JPEG_compress_info cinfo, ByteArray samples, Word32 row_stride, // length of line in bytes (actually: width or 3*width) Word32 height, Word32 i // local variable ) = if i >=- height then unique else +++jpeg_write_scanline(cinfo,samples,row_stride*i); +++jpeg_write_scanlines(cinfo,samples,row_stride,height,i+1). define One +++jpeg_finish_compress ( +++JPEG_compress_info cinfo ) = +++avm{ jpeg_finish_compress }. public define Result_JPEG_write write_image_to_JPEG_file ( JPEG_BitMapImage image, String file_name, Word32 quality // from 0 (poorest) to 100 (best) ) = with qual = if quality -< 0 then 0 else if quality >- 100 then 100 else quality, if file(file_name,new) is { failure then cannot_create_file, success(output_file) then if image is img(format,nw,nh,samples) then if +++create_JPEG_compress_info(nw,nh,format,qual,weaken(output_file)) is { failure then compression_error, success(cinfo) then with row_stride = nw*(if format is {rgb then 3, greyscale then 1}), +++jpeg_write_scanlines(cinfo,samples,row_stride,nh,0); +++jpeg_finish_compress(cinfo); ok } }. *** (10.2.3) Reading a JPEG file. public type +++JPEG_decompress_info: +++jpeg_decompress_info(ByteArray jpeg_decompress_struct, ByteArray jpeg_error_mgr). define Maybe(+++JPEG_decompress_info) +++create_JPEG_decompress_info ( RStream source_file ) = +++avm{ create_JPEG_decompress_info }. define (Word32, // width of image Word32, // height of image JPEG_ImageFormat) +++jpeg_image_parameters ( +++JPEG_decompress_info cinfo ) = +++avm{ jpeg_image_parameters }. define Maybe(One) +++jpeg_read_scanline ( +++JPEG_decompress_info cinfo, ByteArray dest, Word32 offset ) = +++avm{ jpeg_read_scanline }. define One +++jpeg_read_scanlines ( Word32 n, // number of lines to decompress +++JPEG_decompress_info cinfo, ByteArray dest, Word32 row_stride, Word32 offset ) = if n -=< 0 then unique else if +++jpeg_read_scanline(cinfo,dest,offset) is { failure then unique, // last lines may be missing success(_) then +++jpeg_read_scanlines(n-1,cinfo,dest,row_stride,offset+row_stride) }. define One +++jpeg_finish_decompress ( +++JPEG_decompress_info cinfo ) = +++avm{ jpeg_finish_decompress }. public define Result_JPEG_read read_image_from_JPEG_file ( String file_name ) = if file(file_name,read) is { failure then cannot_open_file, success(source_file) then if +++create_JPEG_decompress_info(source_file) is { failure then decompress_error, success(cinfo) then if +++jpeg_image_parameters(cinfo) is (w,h,f) then with sw = (Word32)(if f is {rgb then 3, greyscale then 1}), dest = constant_byte_array(to_Int([w*h*sw]),0), +++jpeg_read_scanlines(h,cinfo,dest,w*sw,0); +++jpeg_finish_decompress(cinfo); ok(img(f,w,h,dest)) } }. *** (11) Managing the graphic screen. *** (11.1) Types for screen, mouse and keyboard handling. public type HostWindow: +++window(+++StructPtr(HostWindow) +++handle, +++StructPtr(HostGC) +++gc). *** (11.2) Tools. public define (Word32,Word32) size ( HostWindow hw ) = +++avm{ host_window_size }. public define One resize ( HostWindow hw, Word32 width, Word32 height ) = +++avm{ resize_host_window }. public define (Word32,Word32) screen_size = +++avm{ screen_size }. public define One change_title ( HostWindow hw, String new_title ) = +++avm{ change_host_window_title }. *** (11.3) Generic host window handler. define Bool +++window_event_pending ( +++StructPtr(HostWindow) handle ) = +++avm{ window_event_pending }. define HostWindowEvent($E) +++get_host_window_event ( +++StructPtr(HostWindow) handle ) = +++avm{ get_host_window_event }. define List(HostWindowEvent($E)) +++get_host_window_events ( +++StructPtr(HostWindow) handle, Word32 max // maximal number of events to get ) = if max +=< 0 then [] else if +++window_event_pending(handle) then with first = +++get_host_window_event(handle), others = +++get_host_window_events(handle,max-1), [first . others] else [ ]. define Bool +++default_host_window_handling ( HostWindowEvent($E) e, List(HostWindowEvent($E)) l, HostWindow window, (HostWindow,List(Rectangle)) -> One paint_method, (HostWindow,HostWindowEvent($E)) -> List(Rectangle) event_handler ). define One +++begin_paint ( HostWindow window, ) = +++avm{ begin_paint }. define One +++end_paint ( HostWindow window, ) = +++avm{ end_paint }. define Bool // 'true' means 'quit' +++handle_host_window_events ( List(HostWindowEvent($E)) list, HostWindow window, (HostWindow,List(Rectangle)) -> One pm, (HostWindow,HostWindowEvent($E)) -> List(Rectangle) eh ) = if list is { [ ] then false, [e1 . es] then if e1 is { quit then forget(eh(window,quit)); true, expose then with result = +++default_host_window_handling(e1,es,window,pm,eh), +++begin_paint(window); pm(window, if size(window) is (winw,winh) then [rect(0,0,winw,winh)]); +++end_paint(window); result, pointer_entering then +++default_host_window_handling(e1,es,window,pm,eh), pointer_leaving then +++default_host_window_handling(e1,es,window,pm,eh), key_down(_,_) then +++default_host_window_handling(e1,es,window,pm,eh), mouse_move(_,_,_) then +++default_host_window_handling(e1,es,window,pm,eh), mouse_click(_,_,_,_) then +++default_host_window_handling(e1,es,window,pm,eh), mouse_wheel(_,_,_,_) then +++default_host_window_handling(e1,es,window,pm,eh), tick then +++default_host_window_handling(e1,es,window,pm,eh), repaint(l) then (pm(window,l); +++handle_host_window_events(es,window,pm,eh)), specific(_) then +++default_host_window_handling(e1,es,window,pm,eh) } }. define Bool +++default_host_window_handling ( HostWindowEvent($E) e, List(HostWindowEvent($E)) l, HostWindow window, (HostWindow,List(Rectangle)) -> One paint_method, (HostWindow,HostWindowEvent($E)) -> List(Rectangle) event_handler ) = with rects = event_handler(window,e), if rects is { [ ] then unique, [_ . _] then paint_method(window,rects) }; +++handle_host_window_events(l,window,paint_method,event_handler). public define One generic_host_window_handler ( HostWindow window, (HostWindow,List(Rectangle)) -> One paint_method, (HostWindow,HostWindowEvent($E)) -> List(Rectangle) event_handler, List(HostWindowEvent($E)) -> List(HostWindowEvent($E)) compress ) = if +++handle_host_window_events(compress(+++get_host_window_events(+++handle(window),200)), window,paint_method,event_handler) then unique else wait_for_event; generic_host_window_handler(window,paint_method,event_handler,compress). *** (11.4) Opening a host window. define Maybe((+++StructPtr(HostWindow),+++StructPtr(HostGC))) +++open_host_window ( Word32 x, Word32 y, Word32 w, Word32 h, String title, HostWindowSort sort ) = +++avm{ open_host_window }. public define Maybe(HostWindow) open_host_window ( Rectangle r, // the rectangle occupied by the window String title, HostWindowSort sort, (HostWindow,List(Rectangle)) -> One paint_method, (HostWindow,HostWindowEvent($E)) -> List(Rectangle) event_handler, List(HostWindowEvent($E)) -> List(HostWindowEvent($E)) compress ) = if r is rect(x,y,u,v) then if +++open_host_window(x,y,u-x,v-y,title,sort) is { failure then failure, success(p) then if p is (handle,gc) then with win = +++window(handle,gc), delegate generic_host_window_handler(win, paint_method, event_handler, compress), success(win) }. public define One show ( HostWindow win ) = +++avm{ show_host_window }. You can also hide the window with: public define One hide ( HostWindow win ) = +++avm{ hide_host_window }. *** (11.5) Queuing an event to a host window. public define Bool queue_event ( HostWindow w, HostWindowEvent($E) e ) = +++avm{ queue_event }. *** (11.6) Basic paint functions. public define One paint_rectangle ( HostWindow hw, Rectangle r, RGB color ) = +++avm{ paint_rectangle }. public define One paint_rectangle ( HostImage buffer, Rectangle r, RGB color ) = +++avm{ paint_rectangle_to_buffer }. public define One paint_image ( HostWindow hw, Rectangle clip, // rect(a,b,u,v) above Word32 x, // position of image in the window Word32 y, HostImage image ) = +++avm{ paint_host_image }. public define One paint_image ( HostImage buffer, Rectangle clip, Word32 x, // position of image in buffer Word32 y, HostImage image ) = +++avm{ paint_host_image_to_buffer }. public define One map_to_host_window ( RGBAImage image, HostWindow hw, Rectangle clip, Word32 a, // (a,b) = upper-left corner of rectangle in 'image' Word32 b, Word32 w, // (w,h) = size of rectangle in 'image' Word32 h, Word32 x, // (x,y) = where upper-left corner of rectangle is mapped Word32 y // in the host window ) = +++avm{ map_RGBA_to_host_window }. *** (12) SQLite3 interface. *** (12.1) Errors. *** (12.2) Opening a data base. public type SQLite3DataBase: +++database(+++StructPtr(SQLite3)). public define Result(SQLite3Error,SQLite3DataBase) sqlite3_open ( String filename ). public define One +++extension_loading ( +++StructPtr(SQLite3) ptr, SQLite3ExtensionEnable e ) = +++avm{ sqlite3_extension_enable }. public define One sqlite3_extension_loading ( SQLite3DataBase db, SQLite3ExtensionEnable e ) = if db is +++database(ptr) then +++extension_loading(ptr,e). define +++StructPtr(SQLite3) +++sqlite3_open ( String filename ) = +++avm{ sqlite3_open }. define Word32 +++sqlite3_errcode ( +++StructPtr(SQLite3) s ) = +++avm{ sqlite3_errcode }. define String +++sqlite3_errmsg ( +++StructPtr(SQLite3) s ) = +++avm{ sqlite3_errmsg }. public define Result(SQLite3Error,SQLite3DataBase) sqlite3_open ( String filename ) = with handle = +++sqlite3_open(filename), code = +++sqlite3_errcode(handle), if code = 0 then ok(+++database(handle)) else error(sqlite3(code,+++sqlite3_errmsg(handle))). public type +++SQLite3DatumType: +++integer, +++float, +++text, +++blob, +++null. define +++SQLite3DatumType +++get_cell_type ( +++StructPtr(SQLite3Stmt) stmt, Word32 iCol ) = +++avm{ sqlite3_column_type }. define String +++get_cell_name ( +++StructPtr(SQLite3Stmt) stmt, Word32 iCol ) = +++avm{ sqlite3_column_name }. define Int +++sqlite3_column_int ( +++StructPtr(SQLite3Stmt) stmt, Word32 iCol ) = +++avm{ sqlite3_column_int }. define Float +++sqlite3_column_double ( +++StructPtr(SQLite3Stmt) stmt, Word32 iCol ) = +++avm{ sqlite3_column_double }. define String +++sqlite3_column_text ( +++StructPtr(SQLite3Stmt) stmt, Word32 iCol ) = +++avm{ sqlite3_column_text }. define ByteArray +++sqlite3_column_blob ( +++StructPtr(SQLite3Stmt) stmt, Word32 iCol ) = +++avm{ sqlite3_column_blob }. define SQLite3Datum +++get_cell_value ( +++StructPtr(SQLite3Stmt) stmt, Word32 iCol ) = if +++get_cell_type(stmt,iCol) is { +++integer then integer (+++sqlite3_column_int(stmt,iCol)), +++float then float (+++sqlite3_column_double(stmt,iCol)), +++text then text (+++sqlite3_column_text(stmt,iCol)), +++blob then blob (+++sqlite3_column_blob(stmt,iCol)), +++null then null }. define Int -> SQLite3Datum +++make_row ( +++StructPtr(SQLite3Stmt) stmt, Int column_count ) = (Int i) |-> if i < 0 then no_such_column else if i >= column_count then no_such_column else +++get_cell_value(stmt, truncate_to_Word32(i)). define Int -> SQLite3Datum +++make_cols ( +++StructPtr(SQLite3Stmt) stmt, Int column_count ) = (Int i) |-> if i < 0 then no_such_column else if i >= column_count then no_such_column else text(+++get_cell_name(stmt,truncate_to_Word32(i))). define Word32 +++column_count ( +++StructPtr(SQLite3Stmt) stmt ) = +++avm{ sqlite3_column_count }. public type +++SQLite3NextRowResult: no_more_row, row, error(Word32 error_code, String error_msg). define +++SQLite3NextRowResult +++go_to_next_row ( +++StructPtr(SQLite3Stmt) stmt ) = +++avm{ sqlite3_go_to_next_row }. define SQLite3HeadersOrRow -> SQLite3Row +++make_cursor ( +++StructPtr(SQLite3) db, +++StructPtr(SQLite3Stmt) stmt, Var(Bool) first ) = with num_columns = to_Int(+++column_count(stmt)), (SQLite3HeadersOrRow askFor) |-> if askFor is { headers then row(+++make_cols(stmt, num_columns)), next_row then if *first then (first <- false; row(+++make_row(stmt,num_columns))) else if +++go_to_next_row(stmt) is { no_more_row then no_more_row, row then row(+++make_row(stmt,num_columns)), error(c,m) then error(sqlite3(c,m)) } }. define Result(Word32,+++StructPtr(SQLite3Stmt)) +++prepare ( +++StructPtr(SQLite3) db, String sql_command ) = +++avm{ sqlite3_prepare }. public define Result(SQLite3Error, SQLite3HeadersOrRow -> SQLite3Row) sql_query ( SQLite3DataBase db, String sql_command ) = if db is +++database(db1) then protect if +++prepare(db1,sql_command) is { error(i) then error(sqlite3(i,+++sqlite3_errmsg(db1))), ok(stmt) then if +++go_to_next_row(stmt) is { no_more_row then ok((SQLite3HeadersOrRow h) |-> no_more_row), row then with first = var((Bool)true), ok(+++make_cursor(db1,stmt,first)), error(c,m) then error(sqlite3(c,m)) } }. *** New Sqlite3 Interface (August 2008). (section 12.4) define One -> SQLite3NextRow +++make_list_cursor ( +++StructPtr(SQLite3) db, +++StructPtr(SQLite3Stmt) stmt, ) = (One u) |-> if +++go_to_next_row(stmt) is { no_more_row then no_more_row, row then if +++make_row_list(stmt,+++column_count(stmt),1) is { error(msg) then error(msg), ok(l) then row(l) }, error(c,m) then error(sqlite3(c,m)) }. define One -> SQLite3Row +++make_new_cursor ( +++StructPtr(SQLite3Stmt) stmt, Bool first_row_cached, ) = with num_columns = to_Int(+++column_count(stmt)), row_in_cache = var(first_row_cached), (One u) |-> if *row_in_cache then row_in_cache <- false; row(+++make_row(stmt,num_columns)) // first row already retrieved else if +++go_to_next_row(stmt) is { no_more_row then no_more_row, row then row(+++make_row(stmt,num_columns)), error(c,m) then error(sqlite3(c,m)) }. Get the list of headers. define List(String) +++list_headers ( +++StructPtr(SQLite3Stmt) stmt, Word32 num_col, // number of columns Word32 i // current column index (starts at 0) ) = if i >=+ num_col then [ ] else [+++get_cell_name(stmt,i) . +++list_headers(stmt,num_col,i+1)]. Reseting a statement. type +++SQLite3ResetResult: error(Word32 error_code, String error_msg), ok. define SQLite3Result +++do_reset ( +++StructPtr(SQLite3Stmt) stmt, ) = +++avm{ sqlite3_reset }. Binding values to parameters. define SQLite3Result +++bind_Int ( +++StructPtr(SQLite3Stmt) stmt, Word32 index, Int value ) = +++avm{ sqlite3_bind_Int }. define SQLite3Result +++bind_Float ( +++StructPtr(SQLite3Stmt) stmt, Word32 index, Float value ) = +++avm{ sqlite3_bind_Float }. define SQLite3Result +++bind_String ( +++StructPtr(SQLite3Stmt) stmt, Word32 index, String value ) = +++avm{ sqlite3_bind_String }. define SQLite3Result +++bind_ByteArray ( +++StructPtr(SQLite3Stmt) stmt, Word32 index, ByteArray value ) = +++avm{ sqlite3_bind_ByteArray }. define SQLite3Result +++bind_NULL ( +++StructPtr(SQLite3Stmt) stmt, Word32 index ) = +++avm{ sqlite3_bind_NULL }. define Word32 +++parameter_index ( +++StructPtr(SQLite3Stmt) stmt, String name ) = +++avm{ sqlite3_parameter_index }. define SQLite3Result +++do_bind ( +++StructPtr(SQLite3Stmt) stmt, List(SQLite3Bind) bindings ) = if bindings is { [ ] then ok, [h . t] then if h is { bind_Int(name,value) then with index = +++parameter_index(stmt,name), if index = 0 then error(sqlite3(12,"Parameter name not found: '"+name+"'.")) else if(+++bind_Int(stmt,index,value)) is { error(e) then error(e), ok then +++do_bind(stmt,t) }, bind_Float(name,value) then with index = +++parameter_index(stmt,name), if index = 0 then error(sqlite3(12,"Parameter name not found: '"+name+"'.")) else if +++bind_Float(stmt,index,value) is { error(e) then error(e), ok then +++do_bind(stmt,t) }, bind_String(name,value) then with index = +++parameter_index(stmt,name), if index = 0 then error(sqlite3(12,"Parameter name not found: '"+name+"'.")) else if +++bind_String(stmt,index,value) is { error(e) then error(e), ok then +++do_bind(stmt,t) }, bind_ByteArray(name,value) then with index = +++parameter_index(stmt,name), if index = 0 then error(sqlite3(12,"Parameter name not found: '"+name+"'.")) else if +++bind_ByteArray(stmt,index,value) is { error(e) then error(e), ok then +++do_bind(stmt,t) }, bind_NULL(name) then with index = +++parameter_index(stmt,name), if index = 0 then error(sqlite3(12,"Parameter name not found: '"+name+"'.")) else if +++bind_NULL(stmt,index) is { error(e) then error(e), ok then +++do_bind(stmt,t) }, } }. define Result(SQLite3Error,List(SQLite3Datum)) +++make_row_list ( +++StructPtr(SQLite3Stmt) stmt, Word32 col_num, Word32 i ) = if i >+ col_num then ok([ ]) else if +++make_row_list(stmt,col_num,i+1) is { error(msg) then error(msg), ok(t) then if +++get_cell_type(stmt,i) is { +++integer then ok([integer(+++sqlite3_column_int(stmt,i)) . t]), +++float then ok([float(+++sqlite3_column_double(stmt,i)) . t]), +++text then ok([text(+++sqlite3_column_text(stmt,i)) . t]), +++blob then ok([blob(+++sqlite3_column_blob(stmt,i)) . t]), +++null then ok([null . t]) } }. define SQLite3QueryResult +++make_SQLite3QueryResult ( +++StructPtr(SQLite3Stmt) stmt, ) = if +++go_to_next_row(stmt) is { /* no row at all in the result */ no_more_row then ok((One u) |-> +++list_headers(stmt,+++column_count(stmt),0), (One u) |-> no_more_row, (List(SQLite3Bind) bindings) |-> forget(+++do_reset(stmt)); +++do_bind(stmt,bindings)), /* the first row exists */ row then ok((One u) |-> +++list_headers(stmt,+++column_count(stmt),0), +++make_new_cursor(stmt,true), (List(SQLite3Bind) bindings) |-> forget(+++do_reset(stmt)); +++do_bind(stmt,bindings)), /* error */ error(c,m) then error(sqlite3(c,m)) }. public define SQLite3QueryResult sqlite3_query ( SQLite3DataBase db, String sql_command ) = sqlite3_query(db,sql_command,[]). public define SQLite3QueryResult sqlite3_query ( SQLite3DataBase db, // the database String sql_command, // the SQL query List(SQLite3Bind) initial_bindings // initial parameter bindings ) = if db is +++database(db1) then protect if +++prepare(db1,sql_command) is { error(i) then error(sqlite3(i,+++sqlite3_errmsg(db1))), ok(stmt) then if +++do_bind(stmt,initial_bindings) is { error(msg) then error(msg), ok then +++make_SQLite3QueryResult(stmt) } }. *** Low level Sqlite3 Interface (August 2008). public type SQLite3Stmt: +++statement(+++StructPtr(SQLite3Stmt)). public define Result(SQLite3Error, SQLite3Stmt) sqlite3_prepare ( SQLite3DataBase db, // the database String sql_command // the SQL query ) = if db is +++database(db1) then protect if +++prepare(db1,sql_command) is { error(i) then error(sqlite3(i, +++sqlite3_errmsg(db1))), ok(stmt) then ok(+++statement(stmt)) }. public define SQLite3Result sqlite3_bind ( SQLite3Stmt stmt, List(SQLite3Bind) bindings ) = if stmt is +++statement(stmt1) then protect +++do_bind(stmt1, bindings). public define SQLite3Row sqlite3_step ( SQLite3Stmt stmt, ) = if stmt is +++statement(stmt1) then with num_columns = to_Int(+++column_count(stmt1)), if +++go_to_next_row(stmt1) is { no_more_row then no_more_row, row then row(+++make_row(stmt1, num_columns)), error(c,m) then error(sqlite3(c,m)) }. public define SQLite3Result sqlite3_reset ( SQLite3Stmt stmt, ) = if stmt is +++statement(stmt1) then +++do_reset(stmt1). public define SQLite3QueryResult make_SQLite3QueryResult ( SQLite3Stmt stmt, ) = if stmt is +++statement(stmt1) then +++make_SQLite3QueryResult(stmt1). *** Fast lexical analysis. The automaton is made of two byte arrays. Let 'ns' be the number of states in the automaton. The first byte array has 'ns' bytes, and each byte is either 0 (the corresponding state is rejecting) or 1 (the corresponding state is accepting) or 2 (the corresponding state is ignoring). The second byte array has 256*ns*2 bytes, and is to be considered as an array of Word16. If a character 'c' is read in state number 's', the automaton jumps to state 'table[256*s+c]', except if this gives (Word16)(-1) ('no transition'). When the automaton reaches either 'no transition' or the end of the input, it determines if the pattern accepted up to here must be rejected, accepted or ignored using the first byte array. The automaton is run in a single Anubis instruction on a given input. Given the automaton in the form of a 'List(FastLexerState)', we first check that it is correct. Check that all transitions in a given state are to existing states: define Result(Word16,One) +++check_transitions ( List(FastLexerTransition) l, Word16 ns // number of states ) = if l is { [ ] then ok(unique), [a . b] then with c = state_name(a), if c >=+ ns then error(c) else +++check_transitions(b,ns) }. type +++CheckLexerResult: unknown_state(Word16), too_many_states, ok. Check the above for all states: define +++CheckLexerResult +++check_states ( List(FastLexerState) l, Word16 ns // number of states ) = if l is { [ ] then ok, [s . t] then if s is { rejecting(tr) then if +++check_transitions(tr,ns) is { error(j) then unknown_state(j) ok(_) then +++check_states(t,ns) }, accepting(tr) then if +++check_transitions(tr,ns) is { error(j) then unknown_state(j) ok(_) then +++check_states(t,ns) }, ignoring(tr) then if +++check_transitions(tr,ns) is { error(j) then unknown_state(j) ok(_) then +++check_states(t,ns) } } }. A classical tool not existing at that point: define Int +++length ( List($T) l, Int n ) = if l is { [ ] then n, [_ . t] then +++length(t,n+1) }. public define Int length ( List($T) l ) = +++length(l,0). Checking a whole lexer. We check that transitions in all states are to existing states. define Word16 truncate_to_Word16 ( Int x ) = if truncate_to_Word32(x) is word32(l,_) then l. define +++CheckLexerResult +++check_lexer ( List(FastLexerState) l ) = if l is [] then unknown_state(0) else with n = length(l), if n > 65530 then too_many_states else +++check_states(l,truncate_to_Word16(n)). We construct the first byte arrays: define One +++record_accepting // record accepting and ignoring states in first byte array ( List(FastLexerState) l, ByteArray fba, Int i ) = if l is { [ ] then unique, [h . t] then if h is { rejecting(_) then forget(put(fba,i,0)), accepting(_) then forget(put(fba,i,1)), ignoring(_) then forget(put(fba,i,2)), }; +++record_accepting(t,fba,i+1) }. define ByteArray +++make_first_byte_array ( List(FastLexerState) l ) = with fba = constant_byte_array(length(l),0), // all rejecting by default +++record_accepting(l,fba,0); fba. We construct the second byte array: define One +++put16 ( ByteArray ba, Int i, // position mesured in bytes from beginning of byte array Word16 w ) = if w is word16(b0,b1) then if system_endianness is { little_endian then forget(put(ba,i,b0)); forget(put(ba,i+1,b1)), big_endian then forget(put(ba,i,b1)); forget(put(ba,i+1,b0)) }. public define Word16 get16 ( ByteArray ba, Int i ) = if nth(i,ba) is { failure then 0, success(b0) then if nth(i+1,ba) is { failure then 0, success(b1) then if system_endianness is { little_endian then word16(b0,b1), big_endian then word16(b1,b0) } } }. define Word32 +++get32 ( ByteArray ba, Int i ) = if nth(i,ba) is { failure then 0, success(b0) then if nth(i+1,ba) is { failure then 0, success(b1) then if nth(i+2,ba) is { failure then 0, success(b2) then if nth(i+3,ba) is { failure then 0, success(b3) then if system_endianness is { little_endian then word32(word16(b0,b1),word16(b2,b3)), big_endian then word32(word16(b3,b2),word16(b1,b0)) } } } } }. define One +++fill_transitions_one_state ( List(FastLexerTransition) l, ByteArray sba, Int i // starting offset in sba for this state ) = if l is { [ ] then unique, [h . t] then if h is { transition(c,s) then +++put16(sba,i+2*to_Int([c]),s), }; +++fill_transitions_one_state(t,sba,i) // same 'i' because same state }. define One +++fill_transitions ( List(FastLexerState) l, ByteArray sba, Int i ) = if l is { [ ] then unique, [h . t] then if h is { rejecting(tr) then +++fill_transitions_one_state(tr,sba,i), accepting(tr) then +++fill_transitions_one_state(tr,sba,i), ignoring(tr) then +++fill_transitions_one_state(tr,sba,i) }; +++fill_transitions(t,sba,i+256*2) }. define ByteArray +++make_second_byte_array ( List(FastLexerState) l ) = with ns = length(l), sba = constant_byte_array(256*ns*2,-1), +++fill_transitions(l,sba,0); sba. The primitive running a fast lexer on a given input. define FastLexerOutput +++run_fast_lexer ( ByteArray states_behaviors, // first byte array ByteArray lexer_table, // second byte array ByteArray input, // input FastLexerLastAccepted last_accepted, // state and position of last accepted Int current_position, // starting reading point within input Int token_start, // where currently read token starts Word16 start_state // starting state within automaton ) = +++avm{ run_fast_lexer }. public define MakeFastLexerResult make_fast_lexer ( List(FastLexerState) l ) = if +++check_lexer(l) is { unknown_state(n) then unknown_state(n), too_many_states then too_many_states, ok then with fba = +++make_first_byte_array(l), sba = +++make_second_byte_array(l), ok((ByteArray input, FastLexerLastAccepted last_accepted, Int current_position, Int token_start, Word16 starting_state) |-> +++run_fast_lexer(fba,sba,input,last_accepted, current_position,token_start,starting_state)) }. public define PrecompiledFastLexerResult precompile_fast_lexer ( List(FastLexerState) l ) = if +++check_lexer(l) is { unknown_state(n) then unknown_state(n), too_many_states then too_many_states, ok then with fba = +++make_first_byte_array(l), sba = +++make_second_byte_array(l), ok(precompiled_fast_lexer(fba,sba)) }. public define (ByteArray input, FastLexerLastAccepted last_accepted, Int current_position, Int token_start, Word16 starting_state) -> FastLexerOutput retrieve_fast_lexer ( PrecompiledFastLexer pl ) = if pl is precompiled_fast_lexer(fba,sba) then (ByteArray input, FastLexerLastAccepted last_accepted, Int current_position, Int token_start, Word16 starting_state) |-> +++run_fast_lexer(fba,sba,input,last_accepted, current_position,token_start,starting_state). *** Linking an external library. public type Library: +++library(+++StructPtr(Library)). define Result((Word32, String), +++StructPtr(Library)) +++dl_load ( String name ) = +++avm{ dl_load }. define Maybe(Word32) +++dl_find_symbol ( +++StructPtr(Library) library, String name ) = +++avm{ dl_find_symbol }. define Maybe(ByteArray) +++dl_call_extension ( Word32 function_ptr, ByteArray parameters, Int default_output_size ) = +++avm{ dl_call_extension }. public define Result((Word32, String), Library) load_library ( String library_name ) = if +++dl_load(library_name) is { error(err) then error(err), ok(handle) then ok(+++library(handle)) }. public define Result(LibraryError, ByteArray) extension_library_call ( Library library, String name_of_function, ByteArray arguments, Int ideal_output_size ) = if library is +++library(lib) then if +++dl_find_symbol(lib, name_of_function) is { failure then error(symbol_not_found), success(sym) then if +++dl_call_extension(sym, arguments, ideal_output_size) is { failure then error(external_call_failed), success(ba) then ok(ba) } }. Temporary serialization/unserialization. public define TempByteArray tempserialize($T d) = +++tempserialize(d). public define Maybe($T) tempunserialize(TempByteArray s) = +++tempunserialize(s). *** Making a segment violation. This was used by the author for debugging purpose. Now inhibited. public define One make_segment_violation = +++avm{ make_segment_violation }. *** (15) DBAPI interface. *** (15.1) Errors. *** (15.2) Opening a data base. public type Database: +++database(+++StructPtr(DB)). public type DbStmt: +++statement(+++StructPtr(DbStmt), +++StructPtr(DB)). define Result(DbError, +++StructPtr(DB)) +++db_connect ( String dbstring, String user, String password, DbClient client ) = +++avm{ db_connect }. public define Result(DbError,Database) db_connect ( String dbstring, String user, String password, DbClient client ) = //print("db_connect\n"); if +++db_connect(dbstring, user, password, client) is { error(err) then error(err), ok(handle) then ok(+++database(handle)) }. define DbVersion +++db_server_version ( +++StructPtr(DB) db, ) = +++avm{ db_server_version }. define DbVersion +++db_client_version ( +++StructPtr(DB) db, ) = +++avm{ db_client_version }. public define DbVersion db_server_version( Database db ) = if db is +++database(handle) then +++db_server_version( handle ). public define DbVersion db_client_version( Database db ) = if db is +++database(handle) then +++db_client_version( handle ). public type +++DbNextRowResult: error(DbError), no_more_row, row. define Result(DbError, +++StructPtr(DbStmt)) +++db_prepare ( +++StructPtr(DB) db, String sql_command ) = +++avm{ db_prepare }. define DbResult +++db_bind ( DbStmt stmt, String name, DbDatum value ) = +++avm{ db_bind }. define DbResult +++db_execute ( DbStmt stmt, ) = +++avm{ db_execute }. define +++DbNextRowResult +++db_fetch ( DbStmt stmt ) = +++avm{ db_fetch }. define Word32 +++column_count ( DbStmt stmt ) = +++avm{ db_field_count }. define String +++db_get_field_name ( DbStmt stmt, Word32 iCol ) = +++avm{ db_get_field_name }. define Result(DbError, DbDatum) +++db_get_field ( DbStmt stmt, Word32 iCol ) = +++avm{ db_get_field_by_index }. define Result(DbError, DbDatum) +++db_get_field ( DbStmt stmt, String col ) = +++avm{ db_get_field_by_name }. define DbResult +++db_reset ( DbStmt stmt, ) = +++avm{ db_reset }. define Int -> DbDatum +++make_row ( DbStmt stmt, Int column_count ) = (Int i) |-> if i < 0 then no_such_column else if i >= column_count then no_such_column else if +++db_get_field(stmt, truncate_to_Word32(i)) is ok(datum) then datum else no_such_column. define One -> DbRow +++make_new_cursor ( DbStmt stmt, Bool first_row_cached, ) = //print("make_new_cursor\n"); with num_columns = to_Int(+++column_count(stmt)), row_in_cache = var(first_row_cached), //print(" num_columns="+abs_to_decimal(num_columns)+"\n"); (One u) |-> if *row_in_cache then row_in_cache <- false; row(+++make_row(stmt,num_columns)) // first row already retrieved else if +++db_fetch(stmt) is { error(err) then error(err), no_more_row then no_more_row, row then row(+++make_row(stmt,num_columns)), }. Get the list of headers. define List(String) +++list_headers ( DbStmt stmt, Word32 num_col, // number of columns Word32 i // current column index (starts at 0) ) = //print("list_headers " + to_decimal(num_col) + "\n"); if i >=+ num_col then [ ] else [+++db_get_field_name(stmt,i) . +++list_headers(stmt,num_col,i+1)]. Binding values to parameters. define DbResult +++db_make_bindings ( DbStmt stmt, List(DbBind) bindings ) = if bindings is { [ ] then ok, [h . t] then if h is db_bind(name, datum) then if(+++db_bind(stmt, name, datum)) is { error(e) then error(e), ok then +++db_make_bindings(stmt,t) } }. define DbQueryResult +++make_DbQueryResult ( DbStmt stmt, ) = //print("make_DbQueryResult\n"); if +++db_execute(stmt) is { error(err) then error(err), ok then if +++db_fetch(stmt) is { /* error */ error(err) then error(err), /* no row at all in the result */ no_more_row then ok((One u) |-> +++list_headers(stmt,+++column_count(stmt),0), (One u) |-> no_more_row, (List(DbBind) bindings) |-> if +++db_reset(stmt) is { error(err) then error(err), ok then if +++db_make_bindings(stmt,bindings) is { error(err) then error(err), ok then +++db_execute(stmt) } }), /* the first row exists */ row then //print("ROW\n"); ok(//print(" cols\n"); (One u) |-> +++list_headers(stmt,+++column_count(stmt),0), //print(" cursor\n"); +++make_new_cursor(stmt,true), //print(" reset\n"); (List(DbBind) bindings) |-> if +++db_reset(stmt) is { error(err) then error(err), ok then if +++db_make_bindings(stmt,bindings) is { error(err) then error(err), ok then +++db_execute(stmt) } }), } }. public define DbQueryResult db_query ( Database db, String sql_command ) = db_query(db,sql_command,[]). public define DbQueryResult db_query ( Database db, // the database String sql_command, // the SQL query List(DbBind) initial_bindings // initial parameter bindings ) = //print("db_query\n"); if db is +++database(db1) then protect if +++db_prepare(db1,sql_command) is { error(err) then error(err), ok(stmt1) then with stmt = +++statement(stmt1, db1), if +++db_make_bindings(stmt,initial_bindings) is { error(msg) then error(msg), ok then +++make_DbQueryResult(stmt) } }. *** Low level DBAPI Interface . public define Result(DbError, DbStmt) db_prepare ( Database db, // the database String sql_command // the SQL query ) = if db is +++database(db1) then protect if +++db_prepare(db1,sql_command) is { error(err) then error(err), ok(stmt) then ok(+++statement(stmt, db1)) }. public define DbResult db_make_bindings ( DbStmt stmt, List(DbBind) bindings ) = protect +++db_make_bindings(stmt, bindings). public define DbResult db_execute ( DbStmt stmt, ) = protect +++db_execute(stmt). public define DbRow db_step ( DbStmt stmt, ) = with num_columns = to_Int(+++column_count(stmt)), if +++db_fetch(stmt) is { error(err) then error(err), no_more_row then no_more_row, row then row(+++make_row(stmt, num_columns)), }. public define Int db_column_count ( DbStmt stmt ) = to_Int(+++column_count(stmt)). public define DbResult db_reset ( DbStmt stmt, ) = +++db_reset(stmt). public define DbQueryResult make_DbQueryResult ( DbStmt stmt, ) = +++make_DbQueryResult(stmt). *** (17) Manipulating types and terms as data. *** (18) Find and replace. A 'certified dictionary' is of type: public type FR_CertifiedDict: +++cdict (OneNonSerial +++dummy, // this makes the type 'non serializable' ByteArray +++auto, // the atomaton proper ByteArray +++jump_tables, // an array of jump tables Int +++nkeys, // number of keys (used by change_values) ByteArray +++values). // the array of replacement values for keys *** (18.1) Format of the three byte arrays above. *** (18.1.1) The automaton '+++auto'. The byte array '+++auto' is just an array of states. Each state is encoded as a sequence of 14 bytes as follows: +----+----+---------+---------+---------+---------+---------+---------+ | st | ch | kid | jm | nm | jnm | nnm | disp | +----+----+---------+---------+---------+---------+---------+---------+ offset: 0 1 2 4 6 8 10 12 where: st (1 byte) (state type) 0 = continue, 1 = accept, 2 = continue/table jump, 3 = accept/table jump ch (1 byte) (character) kid (2 bytes) (key identifier) meaningful only for accepting states jm (2 bytes) (jump if match) number of bytes of jump in the text if character matches nm (2 bytes) (next if match) next state if character matches jnm (2 bytes) (jump if no match) if character does'nt match, number of bytes of jump within the text if no table jump, the id of the jump table otherwise nnm (2 bytes) (next if match) next state if character does'nt match disp (2 bytes) the displacement of the character pointer relative to the begining of the current search zone. The character is not meaningful for the initial state (id = 0), but we dont have to worry about that because in this state (coded as a 'continue' state) jm = jnm = ij ('initial jump') and nm = nnm = 1 ('after-init' state). The record for state number 'n' is at offset 14*n in the byte array. The field 'disp' is not used by the automaton. It is used by the 'certify' function below. *** (18.1.2) The array of jump tables '+++jump_tables'. Each jump table is an array of 256 Word16, and these arrays are gathered into the byte array '+++jump_tables', the jump table number 'n' being at offset n*512. Given a character 'c' and a jump table number 'j', the value of the jump is the Word16 at offset 512*j+2*c in '+++jump_tables'. *** (18.1.3) The array of values '+++values'. The array of values is a byte array constructed as follows: offset | size | type | content ------------------------------------------------------------------------------- 0 | 2 | Word16 | number of entries (denoted as 'n' below) 2 | 4*n | Word32s | array of offsets of entries 4n+2 | 4 | Word32 | size of first value (denoted as 's1' below) 4n+6 | s1 | Word8s | first value and similarly for other values ... The function '+++is_array_of_values' checks if a given byte array is a correct array of values for a given number of keys. define Bool +++is_array_of_values_aux ( Int nkeys, // number of keys and of values (already checked equal) ByteArray ba, Int i, // initial value 0 Int end_of_previous // end of previous entry = offset of next entry ) = if i = nkeys then end_of_previous = length(ba) else with offset = to_Int(+++get32(ba,2+4*i)), if offset > length(ba)-4 then false else with size = to_Int(+++get32(ba,offset)), next = offset+4+size, if length(ba) < next then false else +++is_array_of_values_aux(nkeys,ba,i+1,next). define Bool +++is_array_of_values ( Int nkeys, // number of keys ByteArray ba ) = with nvals = to_Int(word32(get16(ba,0),0)), if nvals = nkeys then if length(ba) < 2+8*nkeys // must contain at least n offsets + n sizes then false else +++is_array_of_values_aux(nkeys,ba,0,2+4*nkeys) else false. *** (18.2) Certifying a compiled dictionary. The process described below does not check if the compiled dictionary is correct for the purpose of finding and replacing. It only checks that it cannot produce a crash or a deadlock in anbexec. The automaton constructed by the program in 'library/tools/find_and_replace.anubis' has the following properties: - Each state has two successors states (whose ids are given as 'nm' and 'nnm') and the ids of these two states must be strictly greater than the id of the state, except in one case: if st is 2 or 3 and then nnm must be state number 1. This ensures that any loop in the automaton passes through state number 1. So, what we have to check in order to ensure that the automaton will not run indefinitely, is that the current offset in the text increases strictly at each passage in state 1. To this end, each state has a field 'disp' which gives the 'displacement' of the character pointer relative to the offset of (the beginning of) the current 'search zone'. - State number 0, satisfies jm = jnm = ij (aka. initial jump) and nm = nnm = 1. In other word, the behavior of the automaton in this state does not depend on the character pointed to. The role of this state number 0 is just to start reading at the right position in the text. Actually, this position is just the maximum of the lengths of the keys minus one. For example, if the longuest key has 5 characters, this initial jump will be +4. (This strategy is part of the Boyer-Moore method of search). State number 0 is never reentered (state number 1 is used instead, and the jump is computed accordingly, i.e. by adding the initial jump). - When a state has type 2 or 3, it has a 'jump table'. The id of this jump table is stored in jnm, and the value of the jump is to be found in this table (at the index corresponding to the character just read, in fact it is the Word16 at 512*j+2*c, where 'j' is the index of the jump table, and where 'c' is the character just read). - For the automaton to be coherent, the value of the 'disp' field in a successor of a state must be the value of the disp field in the state itself plus the value of the jump, except in one case: if state type is 2 or 3 and if we consider the 'nomatch' successor state (which is always state 1). Hence, the condition for avoiding infinite loops is just that if 's' is a state of type 2 or 3, with displacement 'd', and if 'j' is any jump value in the corresponding jump table, we must have d+j-ij > 0, where ij is the initial jump. Indeed, since state number 0 is short-circuited during the jump, the destination of the jump is the new search zone offset plus the initial jump, and what matters is just that the search zone offset increases strictly. Also notice that all these values are signed 16 bit integers. No error can occur because all absolute values are less than 32000. The automaton itself considers these values as 32 bits integers, so that the text itself can be much bigger. text-text-text-text-text-text-text- ^ ^ ^ | | | | | d+j-ij = new search zone offset after transition to state 1 (must be > 0) | d = displacement in state of type 2 or 3 0 = beginning of current search zone Remark: d and ij are always >= 0, but j can be negative. define Maybe(Word16) // returns the number of jump tables +++precheck_jmp_tables // verifies only that the size of the byte array is divisible by 512 and not too big ( ByteArray jtabs ) = if length(jtabs)/512 is { failure then should_not_happen(failure), success(p) then if p is (q,r) then if r = 0 then if q =< 0 | q >= 32000 then failure else success(truncate_to_Word16(q)) else failure }. define macro Word16 +++maxunsigned(Word16 x, Word16 y) = if x +=< y then y else x. define Word16 +++max_key_id ( ByteArray auto, Int i, // must be initialized to 0 Word16 so_far // must be initialized to 0 ) = if nth(i,auto) is { failure then so_far, success(st) then if st = 1 | st = 3 then +++max_key_id(auto,i+14,+++maxunsigned(so_far,get16(auto,i+2))) else +++max_key_id(auto,i+14,so_far) }. define Word16 +++disp // get the displacement in a given state ( ByteArray auto, Word16 state_name ) = get16(auto,to_Int([state_name])*14+12). define Bool +++bad_jump_to_state_1 // returns 'true' if there is a bad jump to state 1 ( ByteArray jtabs, Word16 disp_minus_initial_jump, Int j, // offset of jump table in 'jtabs' Int i // initialized to 0 ) = if i = 256 then false else if get16(jtabs,j+2*i)+disp_minus_initial_jump -=< 0 then true else +++bad_jump_to_state_1(jtabs,disp_minus_initial_jump,j,i+1). The macro below for debugging purpose: define macro Maybe($T) trace(Word32 l) = print("===> "+to_decimal(l)+"\n"); failure. define macro Maybe($T) trace(Word32 l) = failure. define Maybe(Word16) // returns the number of states +++check_auto_aux ( ByteArray auto, // automaton Word16 nstates, // number of states as determined by the size of 'auto' (which is a multiple of 14) Word16 sname, // name of current state Int i, // offset of current state (decreasing) ByteArray jtabs, // array of jump tables Word16 ntabs, // number of jump tables Word16 nkeys, // number of keys Word16 ij // initial jump ) = if i = 0-14 then success(nstates) else // finished if i < 0 then should_not_happen(failure) else // because the original i is a multiple of 12 with st = force_nth(i,auto), kid = get16(auto,i+2), jm = get16(auto,i+4), nm = get16(auto,i+6), jnm = get16(auto,i+8), nnm = get16(auto,i+10), disp = get16(auto,i+12), // possible sorts of states are 0, 1, 2 and 3 if st >+ 3 then trace(__LINE__) else // kid must be the index of a dictionary entry (even if non significant) if kid >=+ nkeys then //print("===> kid: "+to_hexa(kid)+" nkeys: "+to_hexa(nkeys)+"\n"); trace(__LINE__) else // nm must be the name of a state if nm >=+ nstates then trace(__LINE__) else // nnm must be the name of a state if nnm >=+ nstates then trace(__LINE__) else // next 'char matching' state must have bigger name (except is st = 3) if st /= 3 & nm +=< sname then trace(__LINE__) else // displacement in next 'char matching' state must be 'disp+jm' if +++disp(auto,nm) /= disp+jm then print("===> jm: "+to_hexa(jm)+"\n"); trace(__LINE__) else // if there is a jump table ... if st >=+ 2 then // jump table state ( // next 'non char matching' state must be 1 if nnm /= 1 then trace(__LINE__) else // if accepting/jump table state, next 'char matching' state must be 1 if st = 3 & nm /= 1 then trace(__LINE__) else // the index of the jump table must be correct if jnm >=+ ntabs then trace(__LINE__) else // all the jumps to state number 1 must be correct if +++bad_jump_to_state_1(jtabs,disp-ij,to_Int([jnm]),0) then trace(__LINE__) else +++check_auto_aux(auto,nstates,sname-14,i-14,jtabs,ntabs,nkeys,ij) ) else // non jump table state ( // displacement in next 'non char matching' state must be 'disp+jnm' if +++disp(auto,nnm) /= disp+jnm then trace(__LINE__) else +++check_auto_aux(auto,nstates,sname-14,i-14,jtabs,ntabs,nkeys,ij) ). define Maybe(Word16) // returns the initial jump +++state_0 ( ByteArray auto ) = with ij = get16(auto,4), if ij /= get16(auto,8) then trace(__LINE__) else if get16(auto,6) /= 1 then trace(__LINE__) else if get16(auto,10) /= 1 then trace(__LINE__) else if get16(auto,12) /= 0 then trace(__LINE__) else success(ij). define Maybe(Word16) // returns the number of states +++check_auto ( ByteArray auto, ByteArray jtabs, Word16 ntabs, Word16 nkeys ) = if +++state_0(auto) is { failure then trace(__LINE__), success(initial_jump) then with l = length(auto), if l/14 is { failure then should_not_happen(failure), success(p) then if p is (nstates,r) then if r = 0 then if nstates =< 0 then trace(__LINE__) else +++check_auto_aux(auto, truncate_to_Word16(nstates), truncate_to_Word16(l-14), l-14, jtabs, ntabs, nkeys, initial_jump) else trace(__LINE__) } }. public define Maybe(FR_CertifiedDict) certify ( FR_CompiledDict d ) = if d is cdict(auto,jtabs,vals) then with nkeys = +++max_key_id(auto,0,0)+1, if +++precheck_jmp_tables(jtabs) is { failure then trace(__LINE__), success(ntabs) then if +++check_auto(auto,jtabs,ntabs,nkeys) is { failure then trace(__LINE__), success(nstates) then with nkeys_int = to_Int([nkeys]), if +++is_array_of_values(nkeys_int,vals) is { false then trace(__LINE__), true then success(+++cdict(dummy_non_serial,auto,jtabs,nkeys_int,vals)) } } }. *** (18.3) Changing the array of values. Since the automaton and jump tables do not depend on the values associated to the key, it is possible to change the array of values without modifying the other two byte arrays. This is performed by: public define Maybe(FR_CertifiedDict) change_values ( FR_CertifiedDict d, ByteArray new_values ) = since d is +++cdict(o,a,j,nkeys,_), if +++is_array_of_values(nkeys,new_values) then success(+++cdict(o,a,j,nkeys,new_values)) else failure. *** (18.4) Finding and replacing. public define ByteArray find_and_replace(FR_CertifiedDict d, ByteArray text) = +++avm{ b_far_b }. public define ByteArray find_and_replace(FR_CertifiedDict d, String text) = +++avm{ b_far_s }. public define String find_and_replace(FR_CertifiedDict d, ByteArray text) = +++avm{ s_far_b }. public define String find_and_replace(FR_CertifiedDict d, String text) = +++avm{ s_far_s }. *** (18.5) Finding and replacing by chunks. public define (Int,ByteArray) chunk_not_last(FR_CertifiedDict d, ByteArray chunk) = +++avm{ b_cnl_b }. public define (Int,ByteArray) chunk_not_last(FR_CertifiedDict d, String chunk) = +++avm{ b_cnl_s }. public define (Int,String) chunk_not_last(FR_CertifiedDict d, ByteArray chunk) = +++avm{ s_cnl_b }. public define (Int,String) chunk_not_last(FR_CertifiedDict d, String chunk) = +++avm{ s_cnl_s }.