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 )