type Type TAny | (TVar String) | (TGround( String , TypeList[] )) | (TAnd( Type[] , Type[] ));
type TypeList TypeEOF | (TypeSeq( TypeList[] , Type ));
type AST ASTEOF | ASTNil | (App( AST[] , AST[] )) | (Var( String )) | (Lit( String )) | (Abs( AST[] , AST[] ))
| (Seq( AST[] , AST[] )) | (Glb( String , AST[] )) | (ASTType( AST[] , AST[] )) | (Fragment( String , AST[] ))
| (Asc( AST[] , Type[] ));
type ASTList ASTLEOF | (ASTSeq( ASTList[] , AST ));
type Context CtxEOF | CtxNil | (CtxBind( Context[] , String , AST[] ));
type TContext TCtxEOF | (TCtxBind( TContext[] , String , Type ));
type Pair (Pair( AST , AST ));
type CPair (CPair( Context , Context ));
type TPair (TPair( Type , Type ));
type TCPair (TCPair( TContext , TContext ));
type Used Used | Unused | Tail;
ast-tokenized-program := (: SNil S);
ast-parsed-program := (: ASTEOF AST);
non-zero := λ(: t AST). (: (tail(
(let r 1_u64)
(match t (
()
( ASTEOF (set r 0_u64))
( _ () )
))
r
)) U64);
non-zero := λ(: t TContext). (: (tail(
(let r 1_u64)
(match t (
()
( TCtxEOF (set r 0_u64))
( _ () )
))
r
)) U64);
== := λ(: lt Type)(: rt Type). (: (tail(
(let r 0_u64)
(match (TPair( lt rt )) (
()
( (TPair( TAny TAny )) (set r 1_u64) )
( (TPair( (TVar lv) (TVar rv) )) (set r (==( lv rv ))) )
( (TPair( (TAnd( llt rlt )) (TAnd( lrt rrt )) )) (
(if (==( llt lrt )) (
(if (==( rlt rrt )) (
(set r 1_u64)
) ())
) ())
))
( (TPair( (TGround( ln TypeEOF )) (TGround( rn TypeEOF )) )) (
(set r (==( ln rn )))
))
( (TPair( (TGround( ln (TypeSeq( TypeEOF lt1 )) )) (TGround( rn (TypeSeq( TypeEOF rt1 )) )) )) (
(if (==( ln rn )) (
(if (==( lt1 rt1 )) (
(set r 1_u64)
) ())
) ())
))
( (TPair( (TGround( ln (TypeSeq( (TypeSeq( TypeEOF lt1 )) lt2 )) )) (TGround( rn (TypeSeq( (TypeSeq( TypeEOF rt1 )) rt2 )) )) )) (
(if (==( ln rn )) (
(if (==( lt1 rt1 )) (
(if (==( lt2 rt2 )) (
(set r 1_u64)
) ())
) ())
) ())
))
( _ () )
))
r
)) U64);
== := λ(: lterm AST)(: rterm AST). (: (tail(
(let r 0_u64)
(match (Pair( lterm rterm )) (
()
( (Pair( ASTEOF ASTEOF )) (set r 1_u64) )
( (Pair( ASTNil ASTNil )) (set r 1_u64) )
( (Pair( (Seq( ll lr )) (Seq( rl rr )) )) (
(if (==( (as (.1( (as lterm Seq) )) U64) (as (.1( (as rterm Seq) )) U64) )) (
(if (==( (as (.2( (as lterm Seq) )) U64) (as (.2( (as rterm Seq) )) U64) )) (
(set r 1_u64)
) ())
) ())
))
( (Pair( (App( ll lr )) (App( rl rr )) )) (
(if (==( (as (.1( (as lterm App) )) U64) (as (.1( (as rterm App) )) U64) )) (
(if (==( (as (.2( (as lterm App) )) U64) (as (.2( (as rterm App) )) U64) )) (
(set r 1_u64)
) ())
) ())
))
( (Pair( (Abs( ll lr )) (Abs( rl rr )) )) (
(if (==( (as (.1( (as lterm Abs) )) U64) (as (.1( (as rterm Abs) )) U64) )) (
(if (==( (as (.2( (as lterm Abs) )) U64) (as (.2( (as rterm Abs) )) U64) )) (
(set r 1_u64)
) ())
) ())
))
( (Pair( (Seq( ll lr )) (Seq( rl rr )) )) (
(if (==( (as (.1( (as lterm Seq) )) U64) (as (.1( (as rterm Seq) )) U64) )) (
(if (==( (as (.2( (as lterm Seq) )) U64) (as (.2( (as rterm Seq) )) U64) )) (
(set r 1_u64)
) ())
) ())
))
( (Pair( (ASTType( ll lr )) (ASTType( rl rr )) )) (
(if (==( (as (.1( (as lterm ASTType) )) U64) (as (.1( (as rterm ASTType) )) U64) )) (
(if (==( (as (.2( (as lterm ASTType) )) U64) (as (.2( (as rterm ASTType) )) U64) )) (
(set r 1_u64)
) ())
) ())
))
( (Pair( (Fragment( ll lr )) (Fragment( rl rr )) )) (
(if (==( ll rl )) (
(if (==( (as (.2( (as lterm Fragment) )) U64) (as (.2( (as rterm Fragment) )) U64) )) (
(set r 1_u64)
) ())
) ())
))
( (Pair( (Asc( ll lr )) (Asc( rl rr )) )) (
(if (==( (as (.1( (as lterm Asc) )) U64) (as (.1( (as rterm Asc) )) U64) )) (
(if (==( (as (.2( (as lterm Asc) )) U64) (as (.2( (as rterm Asc) )) U64) )) (
(set r 1_u64)
) ())
) ())
))
( (Pair( (Glb( ll lr )) (Glb( rl rr )) )) (
(if (==( ll rl )) (
(if (==( (as (.2( (as lterm Glb) )) U64) (as (.2( (as rterm Glb) )) U64) )) (
(set r 1_u64)
) ())
) ())
))
( (Pair( (Var lv) (Var rv) )) (
(if (==( (as lv U64) (as rv U64) )) (
(set r 1_u64)
) ())
))
( (Pair( (Lit lv) (Lit rv) )) (
(if (==( (as lv U64) (as rv U64) )) (
(set r 1_u64)
) ())
))
( _ () )
))
r
)) U64);
non-zero := λ(: t ASTList). (: (tail(
(let r 1_u64)
(match t (
()
( ASTLEOF (set r 0_u64))
( _ () )
))
r
)) U64);
non-zero := λ(: t TypeList). (: (tail(
(let r 1_u64)
(match t (
()
( TypeEOF (set r 0_u64))
( _ () )
))
r
)) U64);
non-zero := λ(: t Context). (: (tail(
(let r 1_u64)
(match t (
()
( CtxEOF (set r 0_u64))
( _ () )
))
r
)) U64);
close := λ(: x AST). (: (tail(
(mov( (malloc(sizeof AST)) R8 ))
(mov( x 0_u64 (as R8 AST[]) ))
(as R8 AST[])
)) AST[]);
close := λ(: x ASTList). (: (tail(
(mov( (malloc(sizeof ASTList)) R8 ))
(mov( x 0_u64 (as R8 ASTList[]) ))
(as R8 ASTList[])
)) ASTList[]);
close := λ(: x TypeList). (: (tail(
(mov( (malloc(sizeof TypeList)) R8 ))
(mov( x 0_u64 (as R8 TypeList[]) ))
(as R8 TypeList[])
)) TypeList[]);
close := λ(: x Context). (: (tail(
(mov( (malloc(sizeof Context)) R8 ))
(mov( x 0_u64 (as R8 Context[]) ))
(as R8 Context[])
)) Context[]);
close := λ(: x TContext). (: (tail(
(mov( (malloc(sizeof TContext)) R8 ))
(mov( x 0_u64 (as R8 TContext[]) ))
(as R8 TContext[])
)) TContext[]);
print := λ(: t Context). (: (tail(
(match t (
()
( CtxEOF () )
( CtxNil () )
( (CtxBind( rst (*( k v )) )) (tail(
(print rst)
(print k)
(print '\s=\s_s)
(print v)
(print '\:\n_s)
)))
))
()
)) Nil);
print := λ(: t TContext). (: (tail(
(match t (
()
( TCtxEOF () )
( (TCtxBind( rst (*( k v )) )) (tail(
(print rst)
(print k)
(print '\s=\s_s)
(print v)
(print '\:\n_s)
)))
))
()
)) Nil);
print := λ(: t AST). (: (tail(
(match t (
()
( ASTEOF (print 'EOF_s) )
( ASTNil (print '\[\]_s) )
( (Var a) (print a) )
( (Lit a) (tail( (print '\`_s) (print a) )))
( (ASTType( lhs rhs )) (tail(
(print 'type\s_s)
(print lhs)
(print '\s=\s_s)
(print rhs)
)))
( (Glb( k v )) (tail(
(print k)
(print '\s:=\s_s)
(print v)
)))
( (Fragment( k v )) (tail(
(print 'fragment\s_s)
(print k)
(print '\s:=\s_s)
(print v)
)))
( (App( l r )) (tail(
(print '\[_s)
(print l)
(print '\s_s)
(print r)
(print '\]_s)
)))
( (Abs( lhs rhs )) (tail(
(print '\[_s)
(print '\l_s)
(print lhs)
(print '._s)
(print rhs)
(print '\]_s)
)))
( (Asc( t tt )) (tail(
(print '\[:\s_s)
(print t)
(print '\s_s)
(print tt)
(print '\]_s)
)))
( (Seq( l r )) (tail(
(print l)
(print '\:\n_s)
(print r)
)))
))
()
)) Nil);
serialize-ast := λ(: t AST). (: (tail(
(match t (
()
( ASTEOF (print '\[\]_s) )
( ASTNil (print 'Nil_s) )
( (Var a) (tail(
(print '\[Variable\s_s)
(print a)
(print '\]_s)
)))
( (Lit a) (tail(
(print '\[Literal\s_s)
(print a)
(print '\]_s)
)))
( (ASTType( lhs rhs )) (tail(
(print '\[Type\s\[_s)
(serialize-ast lhs)
(print '\s_s)
(serialize-ast rhs)
(print '\]\]_s)
)))
( (Glb( lhs rhs )) (tail(
(print '\[Global\s\[_s)
(print lhs)
(print '\s_s)
(serialize-ast rhs)
(print '\]\]_s)
)))
( (Fragment( lhs rhs )) (tail(
(print '\[Fragment\s\[_s)
(print lhs)
(print '\s_s)
(serialize-ast rhs)
(print '\]\]_s)
)))
( (App( lhs rhs )) (tail(
(print '\[App\s\[_s)
(serialize-ast lhs)
(print '\s_s)
(serialize-ast rhs)
(print '\]\]_s)
)))
( (Abs( lhs rhs )) (tail(
(print '\[Lambda\s\[_s)
(serialize-ast lhs)
(print '\s_s)
(serialize-ast rhs)
(print '\]\]_s)
)))
( (Seq( ASTEOF r )) (tail(
(serialize-ast r)
(print '\n_s)
)))
( (Seq( l r )) (tail(
(serialize-ast l)
(serialize-ast r)
(print '\n_s)
)))
( (Asc( t tt )) (tail(
(print '\[App\s\[_s)
(print '\[App\s\[_s)
(print '\[Literal\s:\]\s_s)
(serialize-ast t)
(print '\]\]\s_s)
(serialize-ast tt)
(print '\]\]_s)
)))
))
()
)) Nil);