Friday, January 1, 2010

Hello 2010!

Small steps, next result, which always is good for a smile. The next 'hello world' program compiled to C and ran.


import "system.hi"

using system

def main: unit =
    _ = print "Hello 2010!";
    nop 


Which for most scripting languages would be totally uninteresting, but in this case is somewhat more interesting, since I linked it with this:


namespace system (

    using string

    interface Text = \=> #where (
        def to_text: t -> text
    )

    def print: ::Text t => t -> unit =
        [ t -> print_text (t.to_text t) ]

    def txt: ::Text t => t -> text =
        [ t -> t.to_text t ]

    def print_text: text -> unit =
        [ t ->
            f = get_stdout nop;
            u = file_print f (str t);
              u ]
)

namespace system (

    interface Length = \=> #where (
        def to_length: a -> int
    )

    def length: ::Length t => t -> int =
        \-> x.to_length x
)

namespace list (

    using system

    type list = \=> [nil | cons a (list a)]

    def list_compare: ::Ord a => list a -> list a -> int =
        [ nil      , nil       ->   0 
        | nil      , _         -> 0-1
        | _        , nil       ->   1
        | cons x xx, cons y yy -> 
            if x == y then xx.compare xx yy
            else x.compare x y ]

    def list_length: list a -> int =
        [ nil       -> 0
        | cons x xx -> 1 + (list_length xx) ]

    instance ::Ord a => Ord (list a) where (
        def compare: list a -> list a -> int = list_compare
    )

    def list_to_text: ::Text t => list t -> text = 
        u = [_txt cc -> cc];
        c = [ x -> u (x.to_text x) ];
        m = fix [ m, f, nil -> nil
                | m, f, cons x xx -> cons (f x) (m f xx) ];
        p = fix [ p, nil, yy       -> yy
                | p, cons x xx, yy -> cons x (p xx yy) ];
        f = fix [ f, nil -> nil
                | f, cons x xx -> p x (f xx) ];
        x = cons '[' nil; y = cons ',' nil; z = cons ']' nil;
        // x = u "["; // y = u ", "; z = u "]";
        t = fix [ t, nil -> nil
                | t, cons x nil -> cons x nil
                | t, cons x0 (cons x1 xx) 
                    -> cons x0 (cons y ((cons x1 xx))) ];
        [ xx -> 
            yy = m c xx;
            yy = t yy;
            yy = f yy;
            yy = f (cons x (cons yy (cons z nil)));
                _txt yy ]

    instance ::Text t => Text (list t) where (
        def to_text: list t -> text = list_to_text
    )

    instance Length (list t) where (
        def to_length: list t -> int = list_length
    )
)

namespace string (

    using system
    using list

    type string = list char

    def text_to_string: text -> string =
        [ _txt cc -> cc ]

    def string_to_text: string -> text =
        [ cc -> _txt cc ]

    def lift: (string -> string) -> text -> text =
        [ f, _txt cc -> _txt (f cc) ]

    interface Str = \=> #where (
        def to_string: t -> string
    )

    def str: ::Str t => t -> string =
        [ t -> t.to_string t ]

    instance Str bool where (
        def to_string: bool -> string = 
            [ b -> text_to_string (txt b) ]
    )

    instance Str char where (
        def to_string: char -> string = 
            [ c -> text_to_string (txt c) ]
    )

    instance Str int where (
        def to_string: int -> string = 
            [ i -> text_to_string (txt i) ]
    )

    instance Str text where (
        def to_string: text -> string = 
            [ t -> text_to_string t ]
    )

)

namespace system (

    using string

    def trace: ::Text t => t -> t =
        [ t ->
            _ = print "(trace:";
            _ = print t;
            _ = print ")\n";
            t ]

    def trace_application: ::Text a ::Text b => (-> b) -> a -> b =
        [ f, x -> [ x, y ->
            _ = print "(trace:";
            _ = print x;
            _ = print " -> ";
            _ = print y;
            _ = print ")\n";
                y ] x (f x) ]

    def banner: ::Text a => a -> unit =
        stars = fix 
            [ st, 0 -> list.nil
            | st, n -> list.cons '*' (st (- 1)) ];
        p = fix 
            [ p, list.nil,       xx -> xx
            | p, list.cons y yy, xx -> list.cons y (p yy xx) ];
        [ t ->
            t = str (txt t);
            l = length (text_to_string (txt t));
            l0 = 70 - l; l1 = l0 / 2; l2 = l0 - l1;
            t = p (stars l1) (p t (stars l2));
            print (string_to_text t) ]
)

namespace system (

    interface Num = \=> #where (
        def plus: a -> a -> a
        def min: a -> a -> a
        def mul: a -> a -> a
        def div: a -> a -> a
    )

    def +: ::Num a => a -> a -> a = 
        \x,y -> x.plus x y

    def -: ::Num a => a -> a -> a = 
        \x,y -> x.min x y
    
    def *: ::Num a => a -> a -> a = 
        \x,y -> x.mul x y

    def /: ::Num a => a -> a -> a = 
        \x,y -> x.div x y

)


namespace system (

    interface Ord = \=> #where (
        def compare: a -> a -> int
    )

    def ==: ::Ord a => a -> a -> bool =
        \x,y -> int_eq (x.compare x y) 0

    def !=: ::Ord a => a -> a -> bool =
        \x,y -> int_eq (x.compare x y) 1

    def <: ::Ord a => a -> a -> bool =
        \x,y -> int_less (x.compare x y) 0

    def <=: ::Ord a => a -> a -> bool =
        \x,y -> int_less (x.compare x y) 1

    def >: ::Ord a => a -> a -> bool =
        \x,y -> int_less (x.compare y x) 0

    def >=: ::Ord a => a -> a -> bool =
        \x,y -> int_less (x.compare y x) 1

    def comp1: ::Ord a => a -> a -> int =
        [ x0,x1 -> x0.compare x0 x1 ]

    def comp2: ::Ord a => ::Ord b => 
        a -> a -> b -> b -> int =
        [ x0,x1,y0,y1 -> 
            c = x0.compare x0 x1;
            if c == 0 then y0.compare y0 y1 else c ]

    def comp3: ::Ord a ::Ord b ::Ord c => 
        a -> a -> b -> b -> c -> c -> int =
        [ x0,x1,y0,y1,z0,z1 -> 
            c =  x0.compare x0 x1;
            if c == 0 then comp2 y0 y1 z0 z1 else c ]

    def comp4: ::Ord a ::Ord b ::Ord c ::Ord d =>
        a -> a -> b -> b -> c -> c -> d -> d -> int =
        [ x0,x1,y0,y1,z0,z1,p0,p1 -> 
            c = comp2 x0 x1 y0 y1;
            if c == 0 then comp2 z0 z1 p0 p1 else c ]

    def comp5: ::Ord a ::Ord b ::Ord c ::Ord d ::Ord e =>
        a -> a -> b -> b -> c -> c -> d -> d -> e -> e -> int =
        [ x0,x1,y0,y1,z0,z1,p0,p1,q0,q1 -> 
            c = comp2 x0 x1 y0 y1;
            if c == 0 then comp3 z0 z1 p0 p1 q0 q1 else c ]

    def comp6: ::Ord a ::Ord b ::Ord c ::Ord d ::Ord e ::Ord f =>
        a -> a -> b -> b -> c -> c -> d -> d -> e -> e -> f -> f -> int =
        [ x0,x1,y0,y1,z0,z1,p0,p1,q0,q1,r0,r1 -> 
            c = comp3 x0 x1 y0 y1 z0 z1;
            if c == 0 then comp3 p0 p1 q0 q1 r0 r1 else c ]
)

namespace system (

    def fix: ((-> b) -> a -> b) -> a -> b =
        [ f -> f [-> (fix f) x] ]

    def id: t -> t = [ x -> x ]

)

namespace system (

    type unit = [ nop ]

    def voiden: a -> unit = [ _ -> nop ]

)

namespace system (

    using system

    using Num

    type bool = [ true | false ]

    def not: bool -> bool =
    [ true -> false 
    | _    -> true ]

    def and: bool -> bool -> bool =
    [ truetrue  -> true 
    | _   , __    -> false ]

    def or: bool -> bool -> bool =
    [ falsefalse -> false 
    | _   , __     -> true ]

    def eq: bool -> bool -> bool =
    [ falsefalse -> true 
    | true , true  -> true 
    | _   , __     -> false ]

    instance Ord bool where (
        def compare: bool -> bool -> int =
        [ falsefalse -> 0
        | truetrue   -> 0
        | false, _     -> 0-1 ]
    )

    instance Text bool where (
        def to_text: bool -> text = 
        [ false -> "false"
        | _     -> "true" ]
    )

)

namespace system (

    using list

    // type int = [ MININT | ... | -1 | 0 | 1 | 2 | ... | MAXINT ]
    type int = {system.int}

    def int_monadic_min: int -> int = 
        \v0 -> {math.int_mon:int[v0:int]}

    def int_dyadic_min: int -> int -> int = 
        \v0,v1 -> {math.int_sub:int[v0:int,v1:int]}

    def int_add: int -> int -> int = 
        \v0,v1 -> {math.int_add:int[v0:int,v1:int]}

    def int_mul: int -> int -> int =
        \v0,v1 -> {math.int_mul:int[v0:int,v1:int]}

    def int_div: int -> int -> int = 
        \v0,v1 -> {math.int_div:int[v0:int,v1:int]}

    def int_compare: int -> int -> int = 
        \v0,v1 -> {math.int_compare:int[v0:int,v1:int]}

    def int_eq: int -> int -> bool = 
        \v0,v1 -> [-> true | _ -> false] (int_compare v0 v1)

    def int_less: int -> int -> bool = 
        \v0,v1 -> {math.int_less:int[v0:int,v1:bool]}

    def int_magic_tick: unit -> int = 
        \v0 -> [ v1 -> {math.int_magic_tick:int[v1:void]} ] 0

    instance Num int where (
        def plus: int -> int -> int = int_add
        def min:  int -> int -> int = int_dyadic_min
        def mul:  int -> int -> int = int_mul
        def div:  int -> int -> int = int_div
    )

    instance Ord int where (
        def compare: int -> int -> int = int_compare
    )

    def int_to_text: int -> text = 
        c = [ 0 -> '0' | 1 -> '1' | 2 -> '2' | 3 -> '3' | 4 -> '4'
            | 5 -> '5' | 6 -> '6' | 7 -> '7' | 8 -> '8' | 9 -> '9' ];
        p = fix [ p, nil,       x -> cons x nil
                | p, cons y yy, x -> cons y (p yy x) ];
        s = fix [ s, n ? n < 0    -> cons '-' ((0-n))
                | s, n ? n < 10   -> cons (c n) nil
                | s, n            ->
                    n0 = n / 10; n1 = n - (n0 * 10);
                    p (s n0) (c n1) ];
        [ n -> _txt (s n) ]

    def text_to_int: text -> int =
        dg = [ '0' -> 0 | '1' -> 1 | '2' -> 2 | '3' -> 3
             | '4' -> 4 | '5' -> 5 | '6' -> 6 | '7' -> 7
             | '8' -> 8 | '9' -> 9 | _ -> (0-1) ];
        ti = fix
            [ ti, acc, nil           -> acc
            | ti, acc, cons '-' dd   -> 0 - (ti acc dd)
            | ti, acc, cons d dd     ->
                d = dg d;
                if d < 0 then ti acc dd 
                else ti ((10 * acc) + d) dd ];
        [ _txt cc -> ti 0 cc ]

    instance Text int where (
        def to_text: int -> text = int_to_text
    )

)

namespace system (

    type char = {system.char}

    def char_ascii_code: char -> int =
        \c0 -> {math.char_ascii_code:int[c0:char]}

    def char_ascii_char: int -> char =
        \c0 -> {math.char_ascii_char:char[c0:int]}

    def char_compare: char -> char -> int = 
        \c0,c1 -> int_compare (char_ascii_code c0) (char_ascii_code c1)

    instance Ord char where (
        def compare: char -> char -> int = char_compare
    )

    instance Text char where (
        def to_text: char -> text = 
            [ c -> _txt (list.cons c list.nil) ]
    )

)

namespace system (

    using system

    using list

    using string

    type chars = { chars }

    def chars_allocate: int -> chars =
        [ sz -> {mem.allocate:pointer[sz:int]} ]

    def chars_free: chars -> unit =
        [ p -> {mem.free:void[p:pointer]} ]

    def chars_set: chars -> int -> char -> unit =
        [ p, n, v -> {mem.set_char:char[p:pointer, n:int, v:char]} ]

    def chars_get: chars -> int -> char =
        [ p, n -> {mem.get_char:char[p:pointer, n:int]} ]

    def chars_blank: chars -> int -> unit =
        [ p, n -> v = 0 ; {mem.set_byte:void[p:pointer, n:int, v:int]} ]

    def chars_is_blank: chars -> int -> bool =
        [ p, n -> 
            [ 0 -> true | _ -> false ] 
            {mem.get_byte:int[p:pointer, n:int]} ]

    def string_to_chars: list char -> chars =
        cf = fix 
            [ cf, s, n, nil -> chars_blank s n
            | cf, s, n, cons c cc -> 
                _ = chars_set s n c; cf s (int_add 1 n) cc ];
        [ cc ->
            l = length cc;
            s = chars_allocate (int_add l 1);
            _ = cf s 0 cc;
            s ]

    def chars_to_string: chars -> list char =
        cs = fix
            [ cs, p, n ->
                if chars_is_blank p n then nil 
                else cons (chars_get p n) (cs p (int_add n 1)) ];
        [ p -> cs p 0 ]

    def text_to_chars: text -> chars =
        [ t -> string_to_chars (text_to_string t) ]

    def chars_to_text: chars -> text =
        [ t -> string_to_text (chars_to_string t) ]

)

namespace system (

    using system

    using string

    using list

    type file = { file }

    def get_stdin: unit -> file =
        [ u -> {io.get_stdin:pointer[u:void]} ]

    def get_stderr: unit -> file =
        [ u -> {io.get_stderr:pointer[u:void]} ]

    def get_stdout: unit -> file =
        [ u -> {io.get_stdout:pointer[u:void]} ]

    def fgetc: file -> int =
        [ f -> {io.fgetc:int[f:pointer]} ]

    def fputc: file -> int -> unit =
        [ f, c -> {io.fputc:void[f:pointer, c:int]} ]

    def fputs: file -> chars -> unit =
        [ f, c -> {io.fputs:void[c:pointer, f:pointer]} ]

    def fput_char: file -> char -> unit =
        [ f, c -> {io.fput_char:void[f:pointer, c:char]} ]

    def fget_char: file -> char =
        [ f -> {io.fget_char:char[f:pointer]} ]

    def feof: file -> int =
        [ f -> {io.feof:int[f:pointer]} ]

    def fis: file -> int =
        [ f -> {io.fis:int[f:pointer]} ]

    def fopen: chars -> chars -> file =
        [ f, m -> {io.fopen:pointer[f:pointer, m:pointer]} ]

    def fclose: file -> int =
        [ f -> {io.fclose:int[f:pointer]} ]

    def fend: file -> bool =
        [ f -> [ 0 -> false | _ -> true ] (feof f) ]

    def mode_read: text = "r"

    def mode_read_write: text = "r+"

    def mode_write: text = "w"

    def mode_write_read: text = "w+"

    def mode_append: text = "a"

    def mode_append_read: text = "a+"

    def file_is: file -> bool =
        [ f -> [ 0 -> false | _ -> true ] (fis f) ]

    def file_open: text -> text -> file =
        [ ff, mm ->
            n = text_to_chars ff;
            m = text_to_chars mm;
            f = fopen n m;
            _ = chars_free n;
            _ = chars_free m;
                f ]

    // XXX: should be fstat, unsafe - but portable
    def file_exists: text -> bool =
        [ fn -> 
            f = file_open fn mode_read;
            _ = fclose f;
                file_is f ]

    def file_close: file -> unit =
        [ f -> n = fclose f; nop ] // XXX:should throw an exception here

    def file_input: file -> list char =
        [ f -> 
            c = fget_char f;
            if fend f then nil else cons c (file_input f) ]

    def file_print: file -> list char -> unit =
        [ f, nil        -> nop
        | f, cons c cc  -> _ = fput_char f c; file_print f cc ]

    def file_read: text -> text =
        [ ff ->
            f  = file_open ff mode_read;
            cc = file_input f;
            u  = file_close f;
                string_to_text cc ]

    def file_write: text -> text -> unit =
        [ fn, t ->
            f  = file_open fn mode_write;
            _  = file_print f (str t);
            u  = file_close f;
                u ]

    def file_scribe: text -> list text -> unit =
        fp = fix 
            [ fp, f, nil        -> nop
            | fp, f, cons t tt  -> 
                _ = file_print f (str t); fp f tt ];
        [ fn, tt ->
            f  = file_open fn mode_write;
            _  = fp f tt;
            u  = file_close f;
                u ]

    def argc: unit -> int =
        [ u -> {io.get_argc:int[u:void]} ]

    def argv: int -> text =
        [ n -> 
            s = {io.get_argv:pointer[n:int]}; 
            t = chars_to_text s;
                t ]

    def args: unit -> list text  = 
        aa = fix
            [ aa, n ->
                if n >= (argc nop) then nil 
                else cons (argv n) (aa (n+1))];
        [-> aa 0 ]

)

namespace system (

    using list

    using string

    type text = [ _txt (list char) ]

    instance Text text where (
        def to_text: text -> text = [ t -> t ]
    )

    instance Ord text where (
        def compare: text -> text -> int = 
        [ _txt t0, _txt t1 -> list_compare t0 t1 ]
    )

    def concat: text -> text -> text =
        c = fix [ c, nil, yy       -> yy
                | c, cons x xx, yy -> cons x (c xx yy) ];
        [ _txt cc0, _txt cc1 -> _txt (c cc0 cc1) ]

    def text_to_string: text -> list char = 
        [ _txt cc -> cc ]

    def squash: list text -> text =
        [ nil       -> ""
        | cons t tt -> concat t (squash tt) ]

    instance Length text where (
        def to_length: text -> int = \-> length (str t)
    )


)

namespace system (

    type tuple_t0 =  
        [ tuple_0 ]

    type tuple_t1 = \t0 => 
        [ tuple_1 t0 ]

    type tuple_t2 = \t0 \t1 => 
        [ tuple_2 t0 t1 ]

    type tuple_t3 = \t0 \t1 \t2 => 
        [ tuple_3 t0 t1 t2 ]

    type tuple_t4 = \t0 \t1 \t2 \t3 => 
        [ tuple_4 t0 t1 t2 t3 ]

    type tuple_t5 = \t0 \t1 \t2 \t3 \t4 => 
        [ tuple_5 t0 t1 t2 t3 t4 ]

    type tuple_t6 = \t0 \t1 \t2 \t3 \t4 \t5 => 
        [ tuple_6 t0 t1 t2 t3 t4 t5 ]

    type tuple_t7 = \t0 \t1 \t2 \t3 \t4 \t5 \t6 => 
        [ tuple_7 t0 t1 t2 t3 t4 t5 t6 ]

    type tuple_t8 = \t0 \t1 \t2 \t3 \t4 \t5 \t6 \t7 => 
        [ tuple_8 t0 t1 t2 t3 t4 t5 t6 t7 ]

    type tuple_t9 = \t0 \t1 \t2 \t3 \t4 \t5 \t6 \t7 \t8 => 
        [ tuple_9 t0 t1 t2 t3 t4 t5 t6 t7 t8 ]

    instance 
        Text tuple_t0 where (
        def to_text: tuple_t0 -> text =
            [ tuple_0 -> "()" ]
    )

    instance 
        ::Text t0 =>
        Text (tuple_t1 t0) where (
        def to_text: tuple_t1 t0 -> text =
            [ tuple_1 t0 -> 
                t = concat (txt t0) ")";
                t = concat "(" t;
                t
            ]
    )

    instance 
        ::Text t0 ::Text t1 =>
        Text (tuple_t2 t0 t1) where (
        def to_text: tuple_t2 t0 t1 -> text =
            [ tuple_2 t0 t1 -> 
                t = concat (txt t1) ")";
                t = concat ", " t;
                t = concat (txt t0) t;
                t = concat "(" t;
                t
            ]
    )

    instance 
        ::Text t0 ::Text t1 ::Text t2 =>
        Text (tuple_t3 t0 t1 t2) where (
        def to_text: tuple_t3 t0 t1 t2 -> text =
            [ tuple_3 t0 t1 t2 -> 
                t = concat (txt t2) ")";
                t = concat ", " t;
                t = concat (txt t1) t;
                t = concat ", " t;
                t = concat (txt t0) t;
                t = concat "(" t;
                t
            ]
    )

    instance 
        ::Text t0 ::Text t1 ::Text t2 ::Text t3 =>
        Text (tuple_t4 t0 t1 t2 t3) where (
        def to_text: tuple_t4 t0 t1 t2 t3 -> text =
            [ tuple_4 t0 t1 t2 t3 -> 
                t = concat (txt t3) ")";
                t = concat ", " t;
                t = concat (txt t2) t;
                t = concat ", " t;
                t = concat (txt t1) t;
                t = concat ", " t;
                t = concat (txt t0) t;
                t = concat "(" t;
                t
            ]
    )

    instance 
        ::Text t0 ::Text t1 ::Text t2 ::Text t3 ::Text t4 =>
        Text (tuple_t5 t0 t1 t2 t3 t4) where (
        def to_text: tuple_t5 t0 t1 t2 t3 t4 -> text =
            [ tuple_5 t0 t1 t2 t3 t4 -> 
                t = concat (txt t4) ")";
                t = concat ", " t;
                t = concat (txt t3) t;
                t = concat ", " t;
                t = concat (txt t2) t;
                t = concat ", " t;
                t = concat (txt t1) t;
                t = concat ", " t;
                t = concat (txt t0) t;
                t = concat "(" t;
                t
            ]
    )

    instance 
        ::Text t0 ::Text t1 ::Text t2 ::Text t3 ::Text t4 
        ::Text t5 =>
        Text (tuple_t6 t0 t1 t2 t3 t4 t5) where (
        def to_text: tuple_t6 t0 t1 t2 t3 t4 t5 -> text =
            [ tuple_6 t0 t1 t2 t3 t4 t5 -> 
                t = concat (txt t5) ")";
                t = concat ", " t;
                t = concat (txt t4) t;
                t = concat ", " t;
                t = concat (txt t3) t;
                t = concat ", " t;
                t = concat (txt t2) t;
                t = concat ", " t;
                t = concat (txt t1) t;
                t = concat ", " t;
                t = concat (txt t0) t;
                t = concat "(" t;
                t
            ]
    )

    instance 
        ::Text t0 ::Text t1 ::Text t2 ::Text t3 ::Text t4 
        ::Text t5 ::Text t6 =>
        Text (tuple_t7 t0 t1 t2 t3 t4 t5 t6) where (
        def to_text: tuple_t7 t0 t1 t2 t3 t4 t5 t6 -> text =
            [ tuple_7 t0 t1 t2 t3 t4 t5 t6 -> 
                t = concat (txt t6) ")";
                t = concat ", " t;
                t = concat (txt t5) t;
                t = concat ", " t;
                t = concat (txt t4) t;
                t = concat ", " t;
                t = concat (txt t3) t;
                t = concat ", " t;
                t = concat (txt t2) t;
                t = concat ", " t;
                t = concat (txt t1) t;
                t = concat ", " t;
                t = concat (txt t0) t;
                t = concat "(" t;
                t
            ]
    )

    instance 
        ::Text t0 ::Text t1 ::Text t2 ::Text t3 ::Text t4 
        ::Text t5 ::Text t6 ::Text t7 =>
        Text (tuple_t8 t0 t1 t2 t3 t4 t5 t6 t7) where (
        def to_text: tuple_t8 t0 t1 t2 t3 t4 t5 t6 t7 -> text =
            [ tuple_8 t0 t1 t2 t3 t4 t5 t6 t7 -> 
                t = concat (txt t7) ")";
                t = concat ", " t;
                t = concat (txt t6) t;
                t = concat ", " t;
                t = concat (txt t5) t;
                t = concat ", " t;
                t = concat (txt t4) t;
                t = concat ", " t;
                t = concat (txt t3) t;
                t = concat ", " t;
                t = concat (txt t2) t;
                t = concat ", " t;
                t = concat (txt t1) t;
                t = concat ", " t;
                t = concat (txt t0) t;
                t = concat "(" t;
                t
            ]
    )

    instance 
        ::Text t0 ::Text t1 ::Text t2 ::Text t3 ::Text t4 
        ::Text t5 ::Text t6 ::Text t7 ::Text t8 =>
        Text (tuple_t9 t0 t1 t2 t3 t4 t5 t6 t7 t8) where (
        def to_text: tuple_t9 t0 t1 t2 t3 t4 t5 t6 t7 t8 -> text =
            [ tuple_9 t0 t1 t2 t3 t4 t5 t6 t7 t8 -> 
                t = concat (txt t8) ")";
                t = concat ", " t;
                t = concat (txt t7) t;
                t = concat ", " t;
                t = concat (txt t6) t;
                t = concat ", " t;
                t = concat (txt t5) t;
                t = concat ", " t;
                t = concat (txt t4) t;
                t = concat ", " t;
                t = concat (txt t3) t;
                t = concat ", " t;
                t = concat (txt t2) t;
                t = concat ", " t;
                t = concat (txt t1) t;
                t = concat ", " t;
                t = concat (txt t0) t;
                t = concat "(" t;
                t
            ]
    )

    instance 
        Ord tuple_t0 where (
        def compare: tuple_t0 -> tuple_t0 -> int =
            [ tuple_0, tuple_0 -> 0 ]
    )

    instance 
        ::Ord t0 =>
        Ord (tuple_t1 t0) where (
        def compare: tuple_t1 t0 -> tuple_t1 t0 -> int =
            [ tuple_1 t0, tuple_1 t1 -> 
                comp1 t0 t1
            ]
    )

    instance 
        ::Ord t0 ::Ord t1 =>
        Ord (tuple_t2 t0 t1) where (
        def compare: tuple_t2 t0 t1 -> tuple_t2 t0 t1 -> int =
            [ tuple_2 t0 t1, tuple_2 t2 t3 -> 
                comp2 t0 t2 t1 t3
            ]
    )

    instance 
        ::Ord t0 ::Ord t1 ::Ord t2 =>
        Ord (tuple_t3 t0 t1 t2) where (
        def compare: tuple_t3 t0 t1 t2 -> tuple_t3 t0 t1 t2 -> int =
            [ tuple_3 t0 t1 t2, tuple_3 t3 t4 t5 -> 
                comp3 t0 t3 t1 t4 t2 t5
            ]
    )
)

namespace opt (

    using system

    type opt = \=> [ just t | nothing ]

    def nothing_test: opt t -> bool =
        [ nothing -> true
        | _       -> false ]

    def value: opt t -> t =
        [ just x -> x ]
 
    def sequential: (-> opt b) -> (-> opt c) -> (-> opt c) =
        [ f, g, x ->
            [ nothing -> nothing | just y -> g y ] 
                (f x) 
        ]

)

namespace memory (

    using system

    type pointer = { pointer }

    def allocate: int -> pointer =
        [ sz -> {mem.allocate:pointer[sz:int]} ]

    def free: pointer -> unit =
        [ p -> {mem.free:void[p:pointer]} ]

    def sizeof_int: unit -> int =
        [ u -> {mem.sizeof_int:int[u:void]} ]

    def get_int: pointer -> int -> int =
        [ p, n -> {mem.get_int:int[p:pointer, n:int]} ]

    def set_int: pointer -> int -> int -> unit =
        [ p, n, v -> {mem.set_int:int[p:pointer, n:int, v:int]} ]

    def sizeof_char: unit -> int =
        [ u -> {mem.sizeof_char:int[u:void]} ]

    def get_char: pointer -> int -> char =
        [ p, n -> {mem.get_char:char[p:pointer, n:int]} ]

    def set_char: pointer -> int -> char -> unit =
        [ p, n, v -> {mem.set_char:char[p:pointer, n:int, v:char]} ]

    def sizeof_byte: unit -> int =
        [ u -> {mem.sizeof_char:int[u:void]} ]

    def get_byte: pointer -> int -> int =
        [ p, n -> {mem.get_byte:int[p:pointer, n:int]} ]

    def set_byte: pointer -> int -> int -> unit =
        [ p, n, v -> {mem.set_byte:int[p:pointer, n:int, v:int]} ]

    def is_null: pointer -> bool =
        [ p -> {mem.is_null:int[p:pointer]} ]
 


I spotted two bugs just by putting it here, time for that documentation generator.

No comments:

Post a Comment