index-typedefs := λ(: program AST). (: (
   (while (non-zero program) (match program (
      ()
      ( (Seq( rst (Typedef( lhs rhs )) )) (
         (index-typedefs( rhs 0_u64 ))
         (set program rst)
      ))
      ( (Seq( rst _ )) (
         (set program rst)
      ))
      ( _ (set program ASTEOF) )
   )))
) Nil);

index-typedefs := λ(: def AST)(: index U64) . (: (
   (match def (
      ()
      ( (App( (App( tds (Var( '|_s _ )) )) (Lit( tag _ )) )) (
         (index-index-of-tag( tag index ))
         (index-lone-tag( tag ))
         (index-typedefs( tds (+( index 1_u64 )) ))
      ))
      ( (App( (App( tds (Var( '|_s _ )) )) (App( (Lit( tag _ )) _ )) )) (
         (index-index-of-tag( tag index ))
         (index-typedefs( tds (+( index 1_u64 )) ))
      ))
      ( (Lit( tag _ )) (
         (index-index-of-tag( tag index ))
         (index-lone-tag( tag ))
      ))
      ( (App( (Lit( tag _ )) _ )) (
         (index-index-of-tag( tag index ))
      ))
      ( ASTEOF () )
      ( _ (exit-error( 'Invalid\sTypedef_s def )) )
   ))
) Nil);

preprocess := λ. (: (
   (index-typedefs ast-parsed-program)
   (set ast-parsed-program (preprocess-apply-literals ast-parsed-program))
   (set ast-parsed-program (preprocess-apply ast-parsed-program))
   (set ast-parsed-program (preprocess-apply-locations ast-parsed-program))
) Nil);

union := λ(: l Context)(: r Context). (: (
   (let return l)
   (if (not(non-zero r)) (set return CtxEOF) ())
   (if (non-zero return) (
      (match r (
         ()
         ( (CtxBind( rst k v )) (
            (set return (CtxBind(
               (close(union( l rst ))) k v
            )))
         ))
         ( _ (set r CtxEOF) )
      ))
   ) ())
   return
) Context);

is-macro-head := λ(: s String)(: arity U64). (: (
   (let macros preprocess-macros)
   (let found 0_u64)
   (while (non-zero macros) (match macros (
      ()
      ( (MSeq( rst (Macro( (App( (Lit( mv _ )) p1 )) mrhs )) )) (
         (if (&&( (==( arity 1_u64 )) (==( s mv )) )) (
            (set found 1_u64)
         ) ())
         (set macros rst)
      ))
      ( (MSeq( rst (Macro( (App( (App( (Lit( mv _ )) p1 )) p2 )) mrhs )) )) (
         (if (&&( (==( arity 2_u64 )) (==( s mv )) )) (
            (set found 1_u64)
         ) ())
         (set macros rst)
      ))
      ( (MSeq( rst (Macro( mlhs mrhs )) )) (
         (exit-error( 'Unrecognized\sMacro\sPattern\n_s mlhs ))
      ))
   )))
   found
) U64);

preprocess-apply-literals := λ(: program AST). (: (
   (let r program)
   (match program (
      ()
      ( (App( (App( (Lit( ':_s ctk )) mvar )) (Lit( mtype _ )) )) (
         (set r (App( (close(Lit( ':_s (unique ctk) ))) (close(App( (close(preprocess-apply-literals mvar)) (close(AType(parse-type mtype))) ))) )))
      ))
      ( (App( (App( (Lit( ':_s ctk )) mvar )) (Var( mtype _ )) )) (
         (set r (App( (close(Lit( ':_s (unique ctk) ))) (close(App( (close(preprocess-apply-literals mvar)) (close(AType(parse-type mtype))) ))) )))
      ))
      ( (Lit( l ltk )) (
         (if (has-suffix( l '_t_s )) (
            (let lpfx (remove-suffix( l '_t_s )))
            (set r (App(
               (close(Lit( 'Token_s (with-key( ltk 'Token_s )) )))
               (close(App(
                  (close(App(
                     (close(App(
                        (close(Lit( ':_s (with-key( ltk ':_s )) )))
                        (close(App( (close(Lit( lpfx (with-key( ltk lpfx )) ))) (close(AType(parse-type 'Literal+Constant+String_s))) )))
                     )))
                     (close(Var( '__s (with-key( ltk '__s )) )))
                  )))
                  (close(Var( '__s (with-key( ltk '__s )) )))
               )))
            )))
         ) ())
      ))
      ( (Var( l ltk )) (
         (if (has-suffix( l '_t_s )) (
            (let lpfx (remove-suffix( l '_t_s )))
            (set r (App(
               (close(Lit( 'Token_s (with-key( ltk 'Token_s )) )))
               (close(App(
                  (close(App(
                     (close(Var( lpfx (with-key( ltk lpfx )) )))
                     (close(Var( '__s (with-key( ltk '__s )) )))
                  )))
                  (close(Var( '__s (with-key( ltk '__s )) )))
               )))
            )))
         ) ())
      ))
      ( (App( t1 t2 )) (
         (set r (App(
            (close(preprocess-apply-literals t1))
            (close(preprocess-apply-literals t2))
         )))
      ))
      ( (Seq( al ar )) (set r (Seq(
         (close(preprocess-apply-literals al))
         (close(preprocess-apply-literals ar))
      ))))
      ( (App( al ar )) (set r (App(
         (close(preprocess-apply-literals al))
         (close(preprocess-apply-literals ar))
      ))))
      ( (Abs( al ar tlt )) (set r (Abs(
         (close(preprocess-apply-literals al))
         (close(preprocess-apply-literals ar))
         tlt
      ))))
      ( (Frg( al ar )) (
         (set r (Frg(
            (unique al)
            (close(preprocess-apply-literals ar))
         )))
      ))
      ( (Glb( k ar )) (set r (Glb(
         (unique k)
         (close(preprocess-apply-literals ar))
      ))))
      ( u (set r u))
   ))
   r
) AST);

preprocess-apply-locations := λ(: program AST). (: (
   (let r program)
   (match program (
      ()
      ( (App( (Var( 'p_s _ )) (Lit( ':Location:_s ltk )) )) (
         (let l 'Location\sUnknown_s)
         (match (location-of ltk) (
            ()
            ( (SourceLocation( fp ln cl )) (
               (set l (clone-rope(SCons(
                  (close(SCons(
                     (close(SAtom 'File:\s_s))
                     (close(SAtom fp))
                  )))
                  (close(SCons(
                     (close(SCons(
                        (close(SAtom '\sLine:\s_s))
                        (close(SAtom(to-string ln)))
                     )))
                     (close(SCons(
                        (close(SAtom '\sColumn:\s_s))
                        (close(SAtom(to-string cl)))
                     )))
                  )))
               ))))
            ))
         ))
         (set r (Lit( l (unique ltk) )))
      ))
      ( (Lit( l ltk )) (
         (set r (Lit( l (unique ltk) )))
      ))
      ( (Var( l ltk )) (
         (set r (Var( l (unique ltk) )))
      ) )
      ( (App( t1 t2 )) (
         (set r (App(
            (close(preprocess-apply-locations t1))
            (close(preprocess-apply-locations t2))
         )))
      ))
      ( (Seq( al ar )) (set r (Seq(
         (close(preprocess-apply-locations al))
         (close(preprocess-apply-locations ar))
      ))))
      ( (App( al ar )) (set r (App(
         (close(preprocess-apply-locations al))
         (close(preprocess-apply-locations ar))
      ))))
      ( (Abs( al ar tlt )) (set r (Abs(
         (close(preprocess-apply-locations al))
         (close(preprocess-apply-locations ar))
         tlt
      ))))
      ( (Frg( al ar )) (
         (set r (Frg(
            (unique al)
            (close(preprocess-apply-locations ar))
         )))
      ))
      ( (Glb( k ar )) (set r (Glb(
         (unique k)
         (close(preprocess-apply-locations ar))
      ))))
      ( u (set r u))
   ))
   r
) AST);

preprocess-apply := λ(: program AST). (: (
   (let r program)
   (match program (
      ()
      ( (App( (App( (Lit( ':_s ctk )) (App( t (AType tt) )) )) nt )) (
         (set r (App(
            (close(App( (close(Lit( ':_s (unique ctk) ))) (close(App( (close(preprocess-apply t)) (close(AType tt)) ))) )))
            (close(preprocess-apply( nt )))
         )))
      ))
      ( (App( (App( (Lit( ':_s ctk )) mvar )) (Lit( mtype _ )) )) (
         (set r (App( (close(Lit( ':_s (unique ctk) ))) (close(App( (close(preprocess-apply mvar)) (close(AType(parse-type mtype))) ))) )))
      ))
      ( (App( (App( (Lit( ':_s ctk )) mvar )) (Var( mtype _ )) )) (
         (set r (App( (close(Lit( ':_s (unique ctk) ))) (close(App( (close(preprocess-apply mvar)) (close(AType(parse-type mtype))) ))) )))
      ))
      ( (App( (App( (Var( 'as_s atk )) (App( t (AType tt) )) )) nt )) (
         (set r (App(
            (close(App( (close(Var( 'as_s (unique atk) ))) (close(App( (close(preprocess-apply t)) (close(AType tt)) ))) )))
            (close(preprocess-apply( nt )))
         )))
      ))
      ( (App( (App( (Var( 'as_s atk )) mvar )) (Lit( mtype _ )) )) (
         (set r (App( (close(Var( 'as_s (unique atk) ))) (close(App( (close(preprocess-apply mvar)) (close(AType(parse-type mtype))) ))) )))
      ))
      ( (App( (App( (Var( 'as_s atk )) mvar )) (Var( mtype _ )) )) (
         (set r (App( (close(Var( 'as_s (unique atk) ))) (close(App( (close(preprocess-apply mvar)) (close(AType(parse-type mtype))) ))) )))
      ))
      ( (App( (Var( 'sizeof_s stk )) (Var( mtype _ )) )) (
         (set r (App( (close(Var( 'sizeof_s (unique stk) ))) (close(AType(parse-type mtype))) )))
      ))
      ( (App( (Var( 'sizeof_s stk )) (Lit( mtype _ )) )) (
         (set r (App( (close(Var( 'sizeof_s (unique stk) ))) (close(AType(parse-type mtype))) )))
      ))
      ( (Lit( l ltk )) (
         (let suffixes parse-suffixes)
         (while (non-zero suffixes) (match suffixes (
            ()
            ( (SfxSeq( rst sfxs sfxtt )) (
               (if (has-suffix( l sfxs )) (
                  (let lpfx (remove-suffix( l sfxs )))
                  (set r (App(
                     (close(Lit( ':_s (with-key( ltk ':_s )) )))
                     (close(App( (close(Lit( lpfx (with-key( ltk lpfx )) ))) (close(AType sfxtt)) )))
                  )))
                  (set suffixes SfxEOF)
               ) (
                  (set suffixes rst)
               ))
            ))
         )))
      ))
      ( (Var( l ltk )) (
         (let suffixes parse-suffixes)
         (while (non-zero suffixes) (match suffixes (
            ()
            ( (SfxSeq( rst sfxs sfxtt )) (
               (if (has-suffix( l sfxs )) (
                  (let lpfx (remove-suffix( l sfxs )))
                  (set r (App(
                     (close(Lit( ':_s (with-key( ltk ':_s )) )))
                     (close(App( (close(Lit( lpfx (with-key( ltk lpfx )) ))) (close(AType sfxtt)) )))
                  )))
                  (set suffixes SfxEOF)
               ) (
                  (set suffixes rst)
               ))
            ))
         )))
      ))
      ( (App( (Var( vn vntk )) vt )) (
         if (is-macro-head( vn 1_u64 )) (
            (let applied (preprocess-apply-hard( vn 1_u64 program )))
            (set r applied)
         ) (
            (set r (App(
               (close(preprocess-apply(Var( vn (unique vntk) ))))
               (close(preprocess-apply vt))
            )))
         )
      ))
      ( (App( (App( (Var( vn vntk )) vt1 )) vt2 )) (
         if (is-macro-head( vn 2_u64 )) (
            (let applied (preprocess-apply-hard( vn 2_u64 program )))
            (set r applied)
         ) (
            (set r (App(
               (close(preprocess-apply(App(
                  (close(Var( vn (unique vntk) )))
                  (close vt1)
               ))))
               (close(preprocess-apply vt2))
            )))
         )
      ))
      ( (Seq( al ar )) (set r (+(
         (preprocess-apply al)
         (preprocess-apply ar)
      ))))
      ( (App( al ar )) (set r (App(
         (close(preprocess-apply al))
         (close(preprocess-apply ar))
      ))))
      ( (Abs( al ar tlt )) (set r (Abs(
         (close(preprocess-apply al))
         (close(preprocess-apply ar))
         tlt
      ))))
      ( (Frg( al ar )) (
         (set r (Frg(
            (unique al)
            (close(preprocess-apply ar))
         )))
      ))
      ( (Glb( k ar )) (set r (Glb(
         (unique k)
         (close(preprocess-apply ar))
      ))))
      ( u (set r u))
   ))
   r
) AST);

preprocess-is-suffixed := λ(: l String). (: (
   (let r 0_u64)
   (let suffixes parse-suffixes)
   (while (non-zero suffixes) (match suffixes (
      ()
      ( (SfxSeq( rst sfxs sfxtt )) (
         (if (has-suffix( l sfxs )) (set r 1_u64) ())
         (set suffixes rst)
      ))
   )))
   r
) U64);

preprocess-apply-hard := λ(: macro-name String)(: arity U64)(: program AST). (: (
   (let return program)
   (let macros preprocess-macros)
   (let matched False_u8)
   (while (non-zero macros) (match macros (
      ()
      ( (MSeq( rst (Macro( lhs rhs )) )) (
         (set macros rst)
         (let go False_u8)
         (match lhs (
            ()
            ( (App( (Lit( m _ )) _ )) (
               (if (&&( (==( macro-name m)) (==( arity 1_u64 )) )) (
                  (set go True_u8)
               ) ())
            ))
            ( (App( (App( (Lit( m _ )) _ )) _ )) (
               (if (&&( (==( macro-name m)) (==( arity 2_u64 )) )) (
                  (set go True_u8)
               ) ())
            ))
         ))
         (if (==( go True_u8 )) (
            (match (try-destructure-macro( (location-of program) lhs program )) (
               ()
               ( CtxEOF (set macros rst) )
               ( ctx (
                  (set rhs (with-location( rhs (location-of program) )))
                  (set rhs (preprocess-apply-literals( rhs )))
                  (let p (apply( ctx rhs )))
                  (let c (extract-uuids( (location-of program) CtxEOF p )))
                  (if (non-zero c) (
                     (set p (substitute-uuids( c p )))
                  ) ())
                  (set return (preprocess-apply p))
                  (set macros MEOF)
                  (set matched True_u8)
               ))
            ))
         ) ())
      ))
      ( _ (set macros MEOF) )
   )))
   (if (not matched) (
      (exit-error( 'Invalid\sMacro\sApplication\n_s program ))
   ) ())
   return
) AST);

apply := λ(: ctx Context)(: term AST). (: (
   (let return term)
   (match term (
      ()
      ( ASTEOF () )
      ( ASTNil () )
      ( (Lit( _ _ )) () )
      ( (AType tt) (
         (set return (AType( (substitute( ctx tt )) )))
      ))
      ( (Var( n _ )) (
         (while (non-zero ctx) (match ctx (
            ()
            ( (CtxBind( rst k v )) (
               (if (==( k n )) (
                  (set return v)
                  (set ctx CtxEOF)
               ) (
                  (set ctx rst)
               ))
            ))
            ( _ (set ctx CtxEOF))
         )))
      ))
      ( (App( vl vr )) (
         (set return (App(
            (close(apply( ctx vl )))
            (close(apply( ctx vr )))
         )))
      ))
      ( (Abs( vl vr tlt )) (
         (set return (Abs(
            (close(apply( ctx vl )))
            (close(apply( ctx vr )))
            tlt
         )))
      ))
      ( (Seq( vl vr )) (
         (set return (Seq(
            (close(apply( ctx vl )))
            (close(apply( ctx vr )))
         )))
      ))
      ( (Typedef( vl vr )) (
         (set return (Typedef(
            (close(apply( ctx vl )))
            (close(apply( ctx vr )))
         )))
      ))
      ( (Glb( k vr )) (
         (set return (Glb(
            (substitute( ctx k ))
            (close(apply( ctx vr )))
         )))
      ))
      ( (Frg( k vr )) (
         (set return (Frg(
            (substitute( ctx k ))
            (close(apply( ctx vr )))
         )))
      ))
   ))
   return
) AST);

try-destructure-macro := λ(: loc SourceLocation)(: lhs AST)(: term AST). (: (
   (let r CtxEOF)
   (match (Tuple( lhs term )) (
      ()
      ( (Tuple( ASTNil ASTNil )) (set r CtxNil) )
      ( (Tuple( (App( (App( (Var( _ _ )) (Var( _ _ )) )) (Var( _ _ )) )) (App( (App( (Lit( possibly-tag _ )) _ )) _ )) )) () )
      ( (Tuple( (App( (Lit( ':Literal:_s _ )) (Var( pv _ )) )) (App( (Lit( ':_s ctk )) (App( (Lit( _ _ )) (AType _) )) )) )) (
         (set r (CtxBind( (close CtxNil) pv (with-location( term (location-of ctk) )) )))
      ))
      ( (Tuple( (App( (Var( _ _ )) (Var( _ _ )) )) (App( (Lit( tag _ )) _ )) )) (
         (if (||( (is-lone-tag tag) (preprocess-is-suffixed tag) )) (
            (match (Tuple( lhs term )) (
               ()
               ( (Tuple( (App(pl pr)) (App(el er)) )) (
                  (let ll (try-destructure-macro( loc pl el )))
                  (if (non-zero ll) (
                     (let rl (try-destructure-macro( loc pr er )))
                     (if (non-zero rl) (
                        (set r (union( ll rl )))
                     ) ())
                  ) ())
               ))
            ))
         ) ())
      ))
      ( (Tuple( (App(pl pr)) (App(el er)) )) (
         (let ll (try-destructure-macro( loc pl el )))
         (if (non-zero ll) (
            (let rl (try-destructure-macro( loc pr er )))
            (if (non-zero rl) (
               (set r (union( ll rl )))
            ) ())
         ) ())
      ))
      ( (Tuple( (Abs(pl pr ptlt)) (Abs(el er etlt)) )) (
         (let ll (try-destructure-macro( loc pl el )))
         (if (non-zero ll) (
            (let rl (try-destructure-macro( loc pr er )))
            (if (non-zero rl) (
               (set r (union( ll rl )))
            ) ())
         ) ())
      ))
      ( (Tuple( (Lit( ':Any:_s _ )) (Var( '__s _ )) )) (
         (set r CtxNil)
      ))
      ( (Tuple( (Lit( pl _ )) (Var( el _ )) )) (
         (if (==( pl el )) (set r CtxNil) ())
      ))
      ( (Tuple( (Lit( pl _ )) (Lit( el _ )) )) (
         (if (==( pl el )) (set r CtxNil) ())
      ))
      ( (Tuple( (App( (Lit( ':Literal:_s _ )) (Var( pv _ )) )) (Lit( el eltk )) )) (
         (if (==( (index-of-tag el) unknown-index-of-tag ))
             (set r (CtxBind( (close CtxNil) pv (with-location( term (location-of eltk) )) )))
             ()
         )
      ))
      ( (Tuple( (App( (Lit( ':Variable:_s _ )) (Var( _ _ )) )) (Var( '__s _ )) )) (
         ()
      ))
      ( (Tuple( (App( (Lit( ':Variable:_s _ )) (Var( pv _ )) )) (Var( el eltk )) )) (
         (set r (CtxBind( (close CtxNil) pv (with-location( term (location-of eltk) )) )))
      ))
      ( (Tuple( (App( (App( (Lit( ':Tag:_s _ )) (Var( pv _ )) )) (Var( pt _ )) )) (Lit( el eltk )) )) (
         (if (==( (index-of-tag el) unknown-index-of-tag )) () (
            (set r CtxNil)
            (let tag-i (to-string(index-of-tag el)))
            (set r (CtxBind( (close r) pv (
               (App(
                  (close(Lit( ':_s (with-key( eltk ':_s )) )))
                  (close(App(
                     (close(Lit( tag-i (with-key( eltk tag-i )) )))
                     (close(AType(parse-type 'Constant+Literal+U64_s)))
                  )))
               ))
            ) )))
            (let tag-tt (clone-rope(SCons(
               (close(SAtom 'Tag<_s))
               (close(SCons(
                  (close(SAtom el))
                  (close(SAtom '>_s))
               )))
            ))))
            (set r (CtxBind( (close r) pt (Lit( tag-tt (with-key( eltk tag-tt )) )) )))
         ))
      ))
      ( (Tuple( (Var( pv _ )) t )) (
         (set r (CtxBind( (close CtxNil) pv (with-location( term (location-of t) )) )))
      ))
      ( _ () )
   ))
   r
) Context);

with-location := λ(: term AST)(: loc SourceLocation). (: (
   (let return term)
   (match term (
      ()
      ( ASTEOF () )
      ( ASTNil () )
      ( (Var( v vtk )) (
         (if (non-zero(location-of vtk)) () (
            (set return (Var( v (with-location( vtk loc )) )))
         ))
      ))
      ( (Lit( v vtk )) (
         (if (non-zero(location-of vtk)) () (
            (set return (Lit( v (with-location( vtk loc )) )))
         ))
      ))
      ( (AType _) () )
      ( (App( lt rt )) (
         (set return (App(
            (close(with-location( lt loc )))
            (close(with-location( rt loc )))
         )))
      ))
      ( (Abs( lt rt tlt )) (
         (set return (Abs(
            (close(with-location( lt loc )))
            (close(with-location( rt loc )))
            tlt
         )))
      ))
      ( (Seq( lt rt )) (
         (set return (Seq(
            (close(with-location( lt loc )))
            (close(with-location( rt loc )))
         )))
      ))
      ( (Typedef( lt rt )) (
         (set return (Typedef(
            (close(with-location( lt loc )))
            (close(with-location( rt loc )))
         )))
      ))
      ( (Glb( k t )) (
         (if (non-zero(location-of t)) () (
            (set k (with-location( k loc )))
            (set t (with-location( t loc )))
         ))
         (set return (Glb( k (close t) )))
      ))
      ( (Frg( k t )) (
         (if (non-zero(location-of t)) () (
            (set k (with-location( k loc )))
            (set t (with-location( t loc )))
         ))
         (set return (Frg( k (close t) )))
      ))
   ))
   return
) AST);

without-location := λ(: term AST). (: (
   (let return term)
   (match term (
      ()
      ( ASTEOF () )
      ( ASTNil () )
      ( (Var( v vtk )) (
         (set return (Var( v (without-location( vtk )) )))
      ))
      ( (Lit( v vtk )) (
         (set return (Lit( v (without-location( vtk )) )))
      ))
      ( (AType _) () )
      ( (App( lt rt )) (
         (set return (App(
            (close(without-location( lt )))
            (close(without-location( rt )))
         )))
      ))
      ( (Abs( lt rt tlt )) (
         (set return (Abs(
            (close(without-location( lt )))
            (close(without-location( rt )))
            tlt
         )))
      ))
      ( (Seq( lt rt )) (
         (set return (Seq(
            (close(without-location( lt )))
            (close(without-location( rt )))
         )))
      ))
      ( (Typedef( lt rt )) (
         (set return (Typedef(
            (close(without-location( lt )))
            (close(without-location( rt )))
         )))
      ))
      ( (Glb( k t )) (
         (set return (Glb(
            (without-location( k ))
            (close(without-location( t )))
         )))
      ))
      ( (Frg( k t )) (
         (set return (Frg(
            (without-location( k ))
            (close(without-location( t )))
         )))
      ))
   ))
   return
) AST);

substitute-uuids := λ(: ctx Context)(: term AST). (: (
   (let return term)
   (match return (
      ()
      ( (App( (Var( 'uuid_s _ )) (Var( x _ )) )) (
         (while (non-zero ctx) (match ctx (
            ()
            ( (CtxBind( rst k v )) (
               (if (==( x k )) (
                  (set return v)
                  (set ctx rst)
               ) (
                  (set ctx rst)
               ))
            ))
            ( _ (set ctx CtxEOF) )
         )))
      ))
      ( (App( l r )) (
         (set return (App(
            (close(substitute-uuids( ctx l )))
            (close(substitute-uuids( ctx r )))
         )))
      ))
      ( (Abs( l r tlt )) (
         (set return (Abs(
            (close(substitute-uuids( ctx l )))
            (close(substitute-uuids( ctx r )))
            tlt
         )))
      ))
      ( ASTEOF () )
      ( ASTNil () )
      ( (AType _) () )
      ( (Var( v _ )) () )
      ( (Lit( v _ )) () )
      ( (Seq( lt rt )) (
         (set return (Seq(
            (close(substitute-uuids( ctx lt )))
            (close(substitute-uuids( ctx rt )))
         )))
      ))
      ( (Typedef( lt rt )) (
         (set return (Typedef(
            (close(substitute-uuids( ctx lt )))
            (close(substitute-uuids( ctx rt )))
         )))
      ))
      ( (Glb( k t )) (
         (set return (Glb(
            k
            (close(substitute-uuids( ctx t )))
         )))
      ))
      ( (Frg( k t )) (
         (set return (Frg(
            k
            (close(substitute-uuids( ctx t )))
         )))
      ))
   ))
   return
) AST);

extract-uuids := λ(: loc SourceLocation)(: ctx Context)(: term AST). (: (
   (let return ctx)
   (match term (
      ()
      ( (App( (Var( 'uuid_s _ )) (Var( x xtk )) )) (
         (let id (uuid()))
         (let lctx (CtxBind( (close ctx) x (Var( id (with-key( xtk id )) )) )))
         (set return lctx)
      ))
      ( (App( l r )) (
         (let lctx (extract-uuids( loc ctx l )))
         (let rctx (extract-uuids( loc lctx r )))
         (set return rctx)
      ))
      ( (Abs( l r tlt )) (
         (let lctx (extract-uuids( loc ctx l )))
         (let rctx (extract-uuids( loc lctx r )))
         (set return rctx)
      ))
      ( ASTEOF () )
      ( ASTNil () )
      ( (AType _) () )
      ( (Var( v _ )) () )
      ( (Lit( v _ )) () )
      ( (Seq( lt rt )) (
         (let lctx (extract-uuids( loc ctx lt )))
         (let rctx (extract-uuids( loc lctx rt )))
         (set return rctx)
      ))
      ( (Typedef( lt rt )) (
         (let lctx (extract-uuids( loc ctx lt )))
         (let rctx (extract-uuids( loc lctx rt )))
         (set return rctx)
      ))
      ( (Glb( k t )) (
         (let rctx (extract-uuids( loc ctx t )))
         (set return rctx)
      ))
      ( (Frg( k t )) (
         (let rctx (extract-uuids( loc ctx t )))
         (set return rctx)
      ))
   ))
   return
) Context);

substitute := λ(: ctx Context)(: v Token). (: (
   (let vk (key-of v))
   (while (non-zero ctx) (match ctx (
      ()
      ( CtxNil (set ctx CtxEOF) )
      ( (CtxBind( rst tk (Lit( _ tv )) )) (
         (if (==( tk vk )) (
            (set v tv)
            (set ctx CtxEOF)
         ) (set ctx rst))
      ))
      ( (CtxBind( rst tk (Var( _ tv )) )) (
         (if (==( tk vk )) (
            (set v tv)
            (set ctx CtxEOF)
         ) (set ctx rst))
      ))
      ( (CtxBind( rst tk tv )) (
         (set ctx rst)
      ))
   )))
   v
) Token);