The Battle: Declarative versus Imperative

While my pet project is rapidly deteriorating to a project for a good C++ programmer, which I am not, I still need to implement the next pass.

I implemented a general imperative construct which allows me to keep track of bindings. I did it in the straightforward manner in which most impure compilers keep track of an environment: A nested set of declarations. Basically, enter a scope, declare some (unique) variables, pop the scope. I decided not to worry too much about performance issues anymore, there are lots of cycles still to waste and memory is cheap.

It's implemented as a stack (vector) of maps from AST nodes to AST nodes. Entering a scope costs 600 bytes, something which I would have found appalling twenty years ago. Now I guess it's fine. Some testing showed that C++ easily handles scoping depths of 100,000.

The question becomes how to implement the pass below. It does something trivial, it lifts the constructors in a type declaration to typed declarations in the context. E.g., in a type 'type list = \a => [ nil | cons a (list a)]' the record 'cons' becomes a function 'def cons: !a => a -> list a -> list a = [ x, y -> Cons x y]'.

It's a purely syntactic transformation which, I am not entirely content with it, precedes the rest of the semantical analysis. As you can read yourself, it's a transform which passes a map of bindings around. Now to do it imperatively...

namespace records (

    using system

    using list

    using position

    using ast

    using transform

    using bindings

    def transform_rec_search: ast -> transform bindings =
        type_arr = [ t0, t1 -> type_arrow (pos t0) t0 t1 ];
        type_app = [ t0, t1 -> type_application (pos t0) t0 t1 ];
        search_child = 
            [ t, p, e -> 
                transform_child (transform_rec_search t) p e ];
        record_update_type =
            [ f, decl_record p c id aa i t e  -> 
                decl_record p c id aa i (f t) e
            | f, e -> e ];
        to_record_type = fix
            [ to_record_type, nil, t -> t
            | to_record_type, cons t0 tt, t -> 
                type_arr t0 (to_record_type tt t) ];
        record_abstraction =
            [ nil, e -> e
            | cons v vv, e -> 
                p = pos v;
                e = expr_match p (cons v vv) (expr_empty p) e;
                e = expr_abstraction p e;
                e ];
        [ t, rr, e -> 
        [ type_record po e0 t0 tt -> 
            ta = to_record_type tt t;
            type_to_var = [e -> fresh.fresh_expr_variable (pos e)];
            vv = list.map type_to_var tt;
            nn = list.map var_to_name vv;
            r  = record_abstraction vv (expr_record po e0 t0 nn);
            d  = decl_record po (expr_empty po) e0 nil t0 ta r;
            (bindings.insert (txt e0) d rr,e)

        | type_universal po t0 t1 -> 
            (rr0,_) = search_child t bindings.empty e;
            rr0 = map.apply 
                (record_update_type [e -> type_universal po t0 e])
                rr0;
            (bindings.union rr rr0, e)

        | type_abstraction po t0 t1 -> 
            (rr0,_) = search_child (type_app t (var_to_name t0)) 
                    bindings.empty e;
            rr0 = map.apply 
                (record_update_type [e -> type_universal po t0 e])
                rr0;
            (bindings.union rr rr0, e)
        | e -> search_child t rr e ] e ]

    def transform_recintro: transform bindings =
        bindings.to_records =
            [ rr -> list.map [(n,e) -> e] (map.to_list rr) ];
        add_bindings =
            [ rr, decl_space po c id aa dd -> 
                (bindings.empty, decl_space po c id aa 
                    (dd ++ bindings.to_records rr))
            | rr, part po c id im dd -> 
                (bindings.empty, part po c id im
                    (dd ++ bindings.to_records rr))
            | rr, e   -> (rr,e) ];
        [ rr, e -> 
        [ decl_space po c id aa dd -> 
            (rr0, e) = transform_child transform_recintro 
                bindings.empty e;
            (rr0, e) = add_bindings rr0 e;
                (rr,e)
        | part po c id im dd -> 
            (rr0, e) = transform_child transform_recintro
                bindings.empty e;
            (rr0, e) = add_bindings rr0 e;
            (rr,e)
        | decl_type po c id aa t k ->
            transform_rec_search id rr e
        | e   -> (rr,e) ] e ]

    def ast_record_intro: ast -> ast =
        transform_ast transform_recintro bindings.empty

)