type TypeConstructorList (TConEOF) | (TConSeq( TypeConstructorList[] , String , Type ));
typecheck-type-constructors := (: TConEOF TypeConstructorList);
non-zero := λ(: t TypeConstructorList). (: (tail(
(let r 1_u64)
(match t (
()
( TConEOF (set r 0_u64))
( _ () )
))
r
)) U64);
close := λ(: x TypeConstructorList). (: (tail(
(mov( (malloc(sizeof TypeConstructorList)) R8 ))
(mov( x 0_u64 (as R8 TypeConstructorList[]) ))
(as R8 TypeConstructorList[])
)) TypeConstructorList[]);
merge := λ(: lctx TContext)(: rctx TContext). (: (tail(
(match rctx (
()
( (TCtxBind( rst (*( k v )) )) (tail(
(let lctx2 (TCtxBind( (close lctx) k v )))
(let lctx3 (merge( lctx2 rst )))
(set lctx lctx3)
)))
( _ () )
))
(close lctx)
)) TContext[]);
print := λ(: tt Type). (: (match tt (
()
( TAny (print '?_s) )
( (TVar( vn )) (print vn) )
( (TGround( tag TypeEOF )) (print tag) )
( (TGround( tag (TypeSeq( TypeEOF p1 )) )) (tail(
(print tag)
(print '<_s)
(print p1)
(print '>_s)
)))
( (TGround( tag (TypeSeq( (TypeSeq( TypeEOF p1 )) p2 )) )) (tail(
(print tag)
(print '<_s)
(print p1)
(print ',_s)
(print p2)
(print '>_s)
)))
( (TGround( tag (TypeSeq( (TypeSeq( (TypeSeq( TypeEOF p1 )) p2 )) p3 )) )) (tail(
(print tag)
(print '<_s)
(print p1)
(print ',_s)
(print p2)
(print ',_s)
(print p3)
(print '>_s)
)))
( (TAnd( lt rt )) (tail(
(print lt)
(print '\s+\s_s)
(print rt)
)))
)) Nil);
serialize-ast := λ(: tt Type). (: (match tt (
()
( TAny (print '\[Variable\s?\]_s) )
( (TVar( vn )) (tail(
(print '\[Variable\s_s)
(print vn)
(print '\]_s)
)))
( (TGround( tag TypeEOF )) (tail(
(print '\[Literal\s_s)
(print tag)
(print '\]_s)
)))
( (TGround( tag (TypeSeq( TypeEOF p1 )) )) (tail(
(print '\[App\s\[_s)
(print '\[Literal\s_s)
(print tag)
(print '\]\s_s)
(serialize-ast p1)
(print '\]\]_s)
)))
( (TGround( tag (TypeSeq( (TypeSeq( TypeEOF p1 )) p2 )) )) (tail(
(print '\[App\s\[_s)
(print '\[Literal\s_s)
(print tag)
(print '\]\s_s)
(print '\[App\s\[_s)
(serialize-ast p1)
(print '\s_s)
(serialize-ast p2)
(print '\]\]_s)
(print '\]\]_s)
)))
( (TGround( tag (TypeSeq( (TypeSeq( (TypeSeq( TypeEOF p1 )) p2 )) p3 )) )) (tail(
(print '\[App\s\[_s)
(print '\[Literal\s_s)
(print tag)
(print '\]\s_s)
(print '\[App\s\[_s)
(print '\[App\s\[_s)
(serialize-ast p1)
(print '\s_s)
(serialize-ast p2)
(print '\]\]\s_s)
(serialize-ast p3)
(print '\]\]_s)
(print '\]\]_s)
)))
( (TAnd( lt rt )) (tail(
(print '\[App\s\[_s)
(print '\[Literal\sAnd\]\s_s)
(print '\[App\s\[_s)
(serialize-ast lt)
(print '\s_s)
(serialize-ast rt)
(print '\]\]_s)
(print '\]\]_s)
)))
)) Nil);
close := λ(: x Type). (: (tail(
(mov( (malloc(sizeof Type)) R8 ))
(mov( x 0_u64 (as R8 Type[]) ))
(as R8 Type[])
)) Type[]);
tnil := λ. (: (tail(
()
(close (TGround(
'Nil_s
(close TypeEOF)
)))
)) Type[]);
type TermTypeList TTEOF | (TTSeq( TermTypeList[] , AST , Type ));
non-zero := λ(: t TermTypeList). (: (tail(
(let r 1_u64)
(match t (
()
( TTEOF (set r 0_u64))
( _ () )
))
r
)) U64);
non-zero := λ(: t Type). (: (tail(
(let r 1_u64)
(match t (
()
( TAny (set r 0_u64))
( _ () )
))
r
)) U64);
close := λ(: x TermTypeList). (: (tail(
(mov( (malloc(sizeof TermTypeList)) R8 ))
(mov( x 0_u64 (as R8 TermTypeList[]) ))
(as R8 TermTypeList[])
)) TermTypeList[]);
typecheck-typeof-lhs := λ(: lhs AST). (: (tail(
(let r TAny)
(match lhs (
()
( (Asc( _ tt )) (
(set r tt)
))
( (App( ps (Asc( _ tt )) )) (
(set r (TGround(
'Cons_s
(close(TypeSeq(
(close(TypeSeq(
(close TypeEOF)
(maybe-deref(typecheck-typeof-lhs( ps )))
)))
tt
)))
)))
))
( ASTNil (tail(
(let r2 (maybe-deref(tnil())))
(set r r2)
)))
( _ (exit-error( 'Unknown\sLHS_s lhs )))
))
(close r)
)) Type[]);
typecheck-term-type-list := (: TTEOF TermTypeList);
typecheck-types-have-changed := True_u8;
typecheck := λ. (: (tail(
(let p ast-parsed-program)
(let ordered-type-exprs ASTEOF)
(while (non-zero p) (match p (
()
( (Seq( rst r )) (tail(
(set ordered-type-exprs (Seq( (close ordered-type-exprs) (close r) )))
(set p rst)
)))
)))
(while (non-zero ordered-type-exprs) (match ordered-type-exprs (
()
( (Seq( rst r )) (tail(
(typecheck-infer-global-context( r ))
(set ordered-type-exprs rst)
)))
)))
(while (==( typecheck-types-have-changed True_u8 )) (
(print 'Typecheck\sIter\n_s)
(set typecheck-types-have-changed False_u8)
(typecheck-infer-expr( global-type-context ast-parsed-program Unused))
))
(typecheck-assert-complete ast-parsed-program)
)) Nil);
global-type-context := (: TCtxEOF TContext);
typecheck-infer-type-definition := λ(: base-type Type)(: body AST). (: (
(match body (
()
( (App( (App( tds (Var '|_s) )) case )) (tail(
(typecheck-infer-type-definition( base-type tds ))
(typecheck-infer-type-constructor( base-type case ))
)))
( case (
(typecheck-infer-type-constructor( base-type case ))
))
))
) Nil);
typecheck-infer-type-constructor := λ(: base-type Type)(: body AST). (: (
(match body (
()
( (Lit tag) (tail(
(let rtype (TAnd( (close base-type) (parse-type tag) )) )
(set typecheck-type-constructors (TConSeq(
(close typecheck-type-constructors)
tag
rtype
)))
)))
( (App( (Lit tag) args )) (tail(
(let atype (maybe-deref(typecheck-infer-type-compound args)))
(let rtype (TAnd( (close base-type) (parse-type tag) )))
(typecheck-annotate-head-accessor( base-type ))
(typecheck-annotate-accessors( (maybe-deref(parse-type tag)) atype ))
(set typecheck-type-constructors (TConSeq(
(close typecheck-type-constructors)
tag
(maybe-deref(tarrow( atype rtype )))
)))
)))
( _ () )
))
) Nil);
typecheck-annotate-head-accessor := λ(: base-type Type). (: (
(set global-type-context (TCtxBind(
(close global-type-context)
'.0_s
(maybe-deref(tarrow( base-type (maybe-deref(parse-type 'U64_s)) )))
)))
) Nil);
typecheck-annotate-accessors := λ(: base-type Type)(: args-type Type). (: (tail(
(let field-number 1_u64)
(while (non-zero args-type) (match args-type (
()
( (TGround( 'Cons_s (TypeSeq( (TypeSeq( TypeEOF lt )) rt )) )) (tail(
(let accessor-name (clone-rope(SCons(
(close (SAtom '._s))
(close (SAtom (to-string field-number)))
))))
(set global-type-context (TCtxBind(
(close global-type-context)
accessor-name
(maybe-deref(tarrow( base-type rt )))
)))
(set field-number (+( field-number 1_u64 )))
(set args-type lt)
)))
( tt (tail(
(let accessor-name (clone-rope(SCons(
(close (SAtom '._s))
(close (SAtom (to-string field-number)))
))))
(set global-type-context (TCtxBind(
(close global-type-context)
accessor-name
(maybe-deref(tarrow( base-type tt )))
)))
(set args-type TAny)
)))
)))
)) Nil);
typecheck-infer-type-compound := λ(: compound AST). (: (tail(
(let r TAny)
(match compound (
()
( (Lit tt) (tail(
(let nt (maybe-deref(parse-type tt)))
(set r nt)
)))
( (Var tt) (tail(
(let nt (maybe-deref(parse-type tt)))
(set r nt)
)))
( (App( (Lit 'And_s) (App( lt rt )) )) (tail(
(let ltt (maybe-deref(typecheck-infer-type-compound lt)))
(let rtt (maybe-deref(typecheck-infer-type-compound rt)))
(set r (TAnd( (close ltt) (close rtt) )))
)))
( (App( (App( lt (Lit ',_s) )) rt )) (tail(
(let ltt (maybe-deref(typecheck-infer-type-compound lt)))
(let rtt (maybe-deref(typecheck-infer-type-compound rt)))
(set r (TGround(
'Cons_s
(close(TypeSeq(
(close(TypeSeq(
(close TypeEOF)
ltt
)))
rtt
)))
)))
)))
( _ (exit-error( 'Malformed\sType\sDefinition_s compound )))
))
(close r)
)) Type[]);
typecheck-infer-global-context := λ(: td AST). (: (tail(
(match td (
()
( (ASTType( (Lit base-type) case-constructors )) (tail(
(let bt (maybe-deref(parse-type base-type)))
(typecheck-infer-type-definition( bt case-constructors ))
)))
( (Glb( k (Abs( lhs (Asc( rhs rhst )) )) )) (tail(
(let lt (maybe-deref(typecheck-typeof-lhs lhs)))
(let ft (maybe-deref(tarrow( lt rhst ))))
(set global-type-context (TCtxBind(
(close global-type-context)
k
ft
)))
)))
( (Fragment( k (Abs( lhs (Asc( rhs rhst )) )) )) (tail(
(let lt (maybe-deref(typecheck-typeof-lhs lhs)))
(let ft (maybe-deref(tarrow( lt rhst ))))
(set global-type-context (TCtxBind(
(close global-type-context)
k
ft
)))
)))
( (Glb( k (Asc( rhs rhst )) )) (
(set global-type-context (TCtxBind(
(close global-type-context)
k
rhst
)))
))
( (Fragment( k (Asc( rhs rhst )) )) (
(set global-type-context (TCtxBind(
(close global-type-context)
k
rhst
)))
))
( (Glb( k _ )) (
(exit-error( 'Global\sBindings\sMust\sBe\sAscripted_s td ))
))
( (Fragment( k _ )) (
(exit-error( 'Global\sBindings\sMust\sBe\sAscripted_s td ))
))
( _ () )
))
()
)) Nil);
typecheck-assert-complete := λ(: term AST). (: (
(match term (
()
( ASTEOF (typecheck-assert-one term) )
( ASTNil (typecheck-assert-one term) )
( (Glb( k v )) (
(typecheck-assert-complete v)
))
( (ASTType( _ _ )) () )
( (Fragment( _ _ )) () )
( (App( (Abs( (Var lname) ASTNil )) rhs )) (tail(
(typecheck-assert-complete rhs)
(typecheck-assert-one term)
)))
( (App( (Var 'gensym-label_s) _ )) () )
( (App( (Var 'label_s) (Var _) )) () )
( (App( (App( (Var 'while_s) cond )) body )) (tail(
(typecheck-assert-complete cond)
(typecheck-assert-complete body)
(typecheck-assert-one term)
)))
( (App( (App( (App( (Var 'if_s) cond )) t )) f )) (tail(
(typecheck-assert-complete cond)
(typecheck-assert-complete t)
(typecheck-assert-complete f)
(typecheck-assert-one term)
)))
( (App( (App( (Var 'set_s) lhs )) rhs )) (tail(
(typecheck-assert-complete rhs)
(typecheck-assert-one term)
)))
( (Asc( t tt )) (tail(
(typecheck-assert-complete t)
(typecheck-assert-one term)
)))
( (Lit l) (typecheck-assert-one term) )
( (Var l) (typecheck-assert-one term) )
( (Abs( lhs rhs )) (tail(
(typecheck-assert-complete rhs)
(typecheck-assert-one term)
)))
( (App( l r )) (tail(
(typecheck-assert-complete l)
(typecheck-assert-complete r)
(typecheck-assert-one term)
)))
( (Seq( l r )) (tail(
(typecheck-assert-complete l)
(typecheck-assert-complete r)
)))
))
) Nil);
typecheck-assert-one := λ(: term AST). (: (
(if (non-zero(maybe-deref(typecheck-lookup term))) () (tail(
(print 'Unable\sto\sinfer\stype\sof\sexpression:\n_s)
(print term)
(print '\n_s)
(exit 1_u64)
)))
) Nil);
typecheck-lookup := λ(: term AST). (: (tail(
(let found TAny)
(let tctx typecheck-term-type-list)
(while (non-zero tctx) (match tctx (
()
( (TTSeq( rst (*( t tt )) )) (
(if (==( t term )) (tail(
(set found tt)
(set tctx TTEOF)
)) (
(set tctx rst)
))
))
)))
(close found)
)) Type[]);
exit-error := λ(: msg String)(: t AST). (: (tail(
(print msg)
(print '\n_s)
(print (maybe-deref(location( t ))))
(print '\n_s)
(print t)
(print '\n_s)
(exit 1_u64)
)) Nil);
normalize := λ(: tt Type). (: (tail(
(match tt (
()
( (TGround( 'Constant_s TypeEOF )) (set tt TAny) )
( (TGround( 'Literal_s TypeEOF )) (set tt TAny) )
( (TGround( 'StackVariable_s TypeEOF )) (set tt TAny) )
( (TGround( 'LocalVariable_s TypeEOF )) (set tt TAny) )
( (TGround( 'GlobalVariable_s TypeEOF )) (set tt TAny) )
( (TAnd( lt rt )) (tail(
(let lt1 (maybe-deref(normalize lt )))
(let rt1 (maybe-deref(normalize rt )))
(match (TPair( lt1 rt1 )) (
()
( (TPair( TAny rt2 )) (set tt rt2) )
( (TPair( lt2 TAny )) (set tt lt2) )
( (TPair( lt2 rt2 )) (set tt (TAnd( (close lt2) (close rt2) ))) )
))
)))
( (TGround( tag _ )) (
(if (non-zero(maybe-deref(typecheck-typeof-tag tag))) (
(set tt TAny)
) ())
))
( _ () )
))
(close tt)
)) Type[]);
nonnormal := λ(: tt Type). (: (tail(
(let rt TAny)
(match tt (
()
( (TGround( 'Constant_s TypeEOF )) (set rt tt) )
( (TGround( 'Literal_s TypeEOF )) (set rt tt) )
( (TGround( 'StackVariable_s TypeEOF )) (set rt tt) )
( (TGround( 'LocalVariable_s TypeEOF )) (set rt tt) )
( (TGround( 'GlobalVariable_s TypeEOF )) (set rt tt) )
( (TAnd( ltt rtt )) (tail(
(let lt1 (maybe-deref(nonnormal ltt )))
(let rt1 (maybe-deref(nonnormal rtt )))
(match (TPair( lt1 rt1 )) (
()
( (TPair( TAny rt2 )) (set rt rt2) )
( (TPair( lt2 TAny )) (set rt lt2) )
( (TPair( lt2 rt2 )) (set rt (TAnd( (close lt2) (close rt2) ))) )
))
)))
( _ () )
))
(close rt)
)) Type[]);
typecheck-ascript := λ(: t AST)(: tt Type). (: (
(if (non-zero tt) (tail(
(let ot-normal (maybe-deref(normalize(maybe-deref(typecheck-lookup t)))))
(if (non-zero ot-normal) (
(if (is-arrow tt) () (tail(
(let tt-normal (maybe-deref(normalize( tt ))))
(if (==( ot-normal tt-normal )) () (tail(
(print ot-normal)
(print '\s!=\s_s)
(print tt-normal)
(print '\n_s)
(exit-error( 'Type\sAscription\sInequality_s t ))
)))
)))
) (tail(
(set typecheck-term-type-list (TTSeq(
(close typecheck-term-type-list)
t tt
)))
(set typecheck-types-have-changed True_u8)
)))
)) ())
) Nil);
typecheck-infer-expr := λ(: tctx TContext)(: term AST)(: used Used). (: (tail(
(match term (
()
( ASTNil (typecheck-ascript( term (maybe-deref(tnil())) )) )
( ASTEOF (typecheck-ascript( term (maybe-deref(tnil())) )) )
( (Seq( l r )) (tail(
(typecheck-infer-expr( tctx l used ))
(typecheck-infer-expr( tctx r used ))
)))
( (ASTType( _ _ )) () )
( (Glb( k v )) (tail(
(typecheck-ascript( v (maybe-deref(typecheck-lookup term)) ))
(typecheck-infer-expr( tctx v Used ))
)))
( (Fragment( k (Abs( lhs (Asc( rhs rhst )) )) )) (
(typecheck-ascript( term rhst ))
))
( (Asc( (Lit _) tt )) (tail(
(typecheck-ascript( term tt ))
(match term (
()
( (Asc( t _ )) (typecheck-ascript( t tt )) )
))
)))
( (Asc( t tt )) (tail(
(let tctx2 (maybe-deref(typecheck-infer-expr( tctx t used ))))
(set tctx tctx2)
(let inner-tt (maybe-deref(typecheck-lookup t)))
(if (non-zero inner-tt) (tail(
(let nn (maybe-deref(nonnormal inner-tt)))
(if (non-zero nn) (
(set tt (TAnd(
(close tt)
(close nn)
)))
) ())
(typecheck-ascript( t tt ))
(typecheck-ascript( term tt ))
)) ())
)))
( (App( (Var 'gensym-label_s) (Var lname) )) (tail(
(let tctx2 (TCtxBind(
(close tctx)
lname
(maybe-deref(tlabel()))
)))
(set tctx tctx2)
(typecheck-ascript( term (maybe-deref(tnil())) ))
)))
( (App( (App( (Var 'set_s) (Var v) )) rhs )) (tail(
(typecheck-infer-expr( tctx rhs Used ))
(typecheck-ascript( rhs (maybe-deref(typecheck-typeof-var( term tctx v ))) ))
(typecheck-ascript( term (maybe-deref(tnil())) ))
)))
( (App( (Var 'label_s) (Var lname) )) (
(typecheck-ascript( term (maybe-deref(tnil())) ))
))
( (App( (App( (App( (Var 'if_s) cond )) t )) f )) (tail(
(let tctx2 (maybe-deref(typecheck-infer-expr( tctx cond Used ))))
(let tctx3 (maybe-deref(typecheck-infer-expr( tctx2 t Used ))))
(set tctx tctx3)
(typecheck-infer-expr( tctx f Used ))
(typecheck-ascript( term (maybe-deref(typecheck-lookup t)) ))
)))
( (App( (App( (Var 'while_s) cond )) body )) (tail(
(let tctx2 (maybe-deref(typecheck-infer-expr( tctx cond Used ))))
(set tctx tctx2)
(typecheck-infer-expr( tctx body Used ))
(typecheck-ascript( term (maybe-deref(tnil())) ))
)))
( (App( (Var 'tail_s) (App( l r )) )) (tail(
(let tctx2 (maybe-deref(typecheck-infer-expr( tctx l Unused ))))
(let tctx3 (maybe-deref(typecheck-infer-expr( tctx2 r used ))))
(set tctx tctx3)
(typecheck-ascript( term (maybe-deref(typecheck-lookup r)) ))
)))
( (App( (App( (Var 'as_s) t )) (Lit lt) )) (tail(
(let tctx2 (maybe-deref(typecheck-infer-expr( tctx t used ))))
(set tctx tctx2)
(let inner-tt (maybe-deref(typecheck-lookup t)))
(if (non-zero inner-tt) (tail(
(let tt (maybe-deref(parse-type lt)))
(let nn (maybe-deref(nonnormal inner-tt)))
(if (non-zero nn) (
(set tt (TAnd(
(close tt)
(close nn)
)))
) ())
(typecheck-ascript( term tt ))
)) ())
)))
( (App( (App( (Var 'as_s) t )) (Var lt) )) (tail(
(let tctx2 (maybe-deref(typecheck-infer-expr( tctx t used ))))
(set tctx tctx2)
(let inner-tt (maybe-deref(typecheck-lookup t)))
(if (non-zero inner-tt) (tail(
(let tt (maybe-deref(parse-type lt)))
(let nn (maybe-deref(nonnormal inner-tt)))
(if (non-zero nn) (
(set tt (TAnd(
(close tt)
(close nn)
)))
) ())
(typecheck-ascript( term tt ))
)) ())
)))
( (App( (Var 'sizeof_s) _ )) (
(typecheck-ascript( term (maybe-deref(parse-type 'U64_s)) ))
))
( (App( (Var 'maybe-deref_s) r )) (tail(
(let tctx2 (maybe-deref(typecheck-infer-expr( tctx r used ))))
(set tctx tctx2)
(let deref-type (maybe-deref(typecheck-lookup r)))
(match (typecheck-slot( deref-type 'Array_s )) (
()
( (TGround( 'Array_s (TypeSeq( (TypeSeq( TypeEOF array-base )) TAny )) )) (
(set deref-type array-base)
))
( _ () )
))
(typecheck-ascript( term deref-type ))
)))
( (App( (Abs( (Var lname) ASTNil )) rhs )) (tail(
(typecheck-infer-expr( tctx rhs Used ))
(let rt (maybe-deref(as-local-variable(maybe-deref(typecheck-lookup rhs)))))
(set tctx (TCtxBind(
(close tctx)
lname
rt
)))
(print 'Let\s_s)
(print lname)
(print '\s:\s_s)
(print rt)
(print '\n_s)
(typecheck-ascript( term (maybe-deref(tnil())) ))
)))
( (App( l r )) (tail(
(let tctx2 (maybe-deref(typecheck-infer-expr( tctx l Used ))))
(let tctx3 (maybe-deref(typecheck-infer-expr( tctx2 r Used ))))
(set tctx tctx3)
(let rt (maybe-deref(typecheck-apply(
term
(maybe-deref(typecheck-lookup l))
(maybe-deref(typecheck-lookup r))
))))
(typecheck-ascript( term rt ))
)))
( (Abs( lhs rhs )) (tail(
(let tctx2 (maybe-deref(typecheck-infer-ctx( tctx lhs ))))
(set tctx tctx2)
(typecheck-infer-expr( tctx rhs Used ))
(let lt (maybe-deref(typecheck-typeof-lhs rhs)))
(let rt (maybe-deref(typecheck-lookup rhs)))
(typecheck-ascript( term (maybe-deref(tarrow( lt rt ))) ))
)))
( (Var v) (
(typecheck-ascript( term (maybe-deref(typecheck-typeof-var( term tctx v ))) ))
))
( (Lit l) (tail(
(let tt (maybe-deref(typecheck-typeof-tag l)))
(if (non-zero tt) (
(typecheck-ascript( term tt ))
) ())
)))
( _ (tail(
(print 'Unknown\sTerm\sIn\sType\sInference\n_s)
(print term)
(print '\n_s)
(exit 1_u64)
)))
))
(close tctx)
)) TContext[]);
typecheck-slot := λ(: tt Type)(: slot String). (: (tail(
(let rt (maybe-deref(typecheck-slot-inner( tt slot ))))
(if (non-zero rt) () (
(set rt tt)
))
(close rt)
)) Type[]);
typecheck-slot-inner := λ(: tt Type)(: slot String). (: (tail(
(let rt TAny)
(match tt (
()
( (TGround( bt _ )) (
(if (==( bt slot )) (set rt tt) ())
))
( (TAnd( lt rt )) (tail(
(let lt2 (maybe-deref(typecheck-slot-inner( lt slot ))))
(if (non-zero lt2) (
(set rt lt2)
) (tail(
(let rt2 (maybe-deref(typecheck-slot-inner( rt slot ))))
(set rt rt2)
)))
)))
( _ () )
))
(close rt)
)) Type[]);
typecheck-typeof-tag := λ(: tag String). (: (tail(
(let r TAny)
(let tag-list typecheck-type-constructors)
(while (non-zero tag-list) (match tag-list (
()
( (TConSeq( rst (*( k kt )) )) (
(if (==( k tag )) (tail(
(set r kt)
(set tag-list TConEOF)
)) (
(set tag-list rst)
))
))
)))
(close r)
)) Type[]);
as-local-variable := λ(: tt Type). (: (tail(
(let tt2 (maybe-deref(normalize tt)))
(if (non-zero tt2) (tail(
(let tt3 (TAnd( (close tt2) (close(TGround( 'LocalVariable_s (close TypeEOF) ))) )))
(set tt2 tt3)
)) ())
(close tt2)
)) Type[]);
is-arrow := λ(: tt Type). (: (tail(
(let r 0_u64)
(match tt (
()
( (TAnd( lt rt )) (
(if (is-arrow lt) (
(set r 1_u64)
) (
(set r (is-arrow rt))
))
))
( (TGround( '->_s _ )) (set r 1_u64) )
( _ () )
))
r
)) U64);
typecheck-apply := λ(: sloc AST)(: ft Type)(: pt Type). (: (tail(
(let rt TAny)
(if (is-arrow ft) (
(match ft (
()
( (TAnd( ft1 ft2 )) (tail(
(let rt1 (maybe-deref(typecheck-apply( sloc ft1 pt ))))
(if (non-zero rt1) (
(set rt rt1)
) (tail(
(let rt2 (maybe-deref(typecheck-apply( sloc ft2 pt ))))
(set rt rt2)
)))
)))
( (TGround( '->_s (TypeSeq( (TypeSeq( TypeEOF fpt )) frt )) )) (tail(
(let ctx (maybe-deref(typecheck-unify-args( fpt pt ))))
(if (non-zero ctx) (tail(
(let rt1 (maybe-deref(typecheck-unify-ctx( ctx frt ))))
(set rt rt1)
)) ())
)))
( _ () )
))
) (
(if (non-zero ft) (
(if (non-zero pt) (tail(
(let rt2 (TGround(
'Cons_s
(close(TypeSeq(
(close(TypeSeq(
(close TypeEOF)
ft
)))
pt
)))
)))
(set rt rt2)
)) ())
) ())
))
(print 'Apply:\n_s)
(print ft)
(print '\n_s)
(print pt)
(print '\n_s)
(print rt)
(print '\n_s)
(close rt)
)) Type[]);
typecheck-unify-ctx := λ(: ctx TContext)(: tt Type). (: (tail(
()
(close tt)
)) Type[]);
tcontext-accept := λ. (: (tail(
(let r (TCtxBind(
(close TCtxEOF)
'Accept_s
(maybe-deref(tnil()))
)))
(close r)
)) TContext[]);
typecheck-unify-args := λ(: fpt Type)(: pt Type). (: (tail(
(let ctx TCtxEOF)
(match (TPair( fpt pt )) (
()
( (TPair( (TVar( ltv )) rt )) (
(set ctx (TCtxBind(
(close TCtxEOF)
ltv
rt
)))
))
( (TPair( (TAnd( lt1 lt2 )) rt )) (
(match (TCPair( (maybe-deref(typecheck-unify-args( lt1 rt ))) (maybe-deref(typecheck-unify-args( lt2 rt ))) )) (
()
( (TCPair( TCtxEOF _ )) () )
( (TCPair( _ TCtxEOF )) () )
( (TCPair( lctx rctx )) (tail(
(let nctx (maybe-deref(merge( lctx rctx ))))
(set ctx nctx)
)))
))
))
( (TPair( lt (TAnd( rt1 rt2 )) )) (
(match (TCPair( (maybe-deref(typecheck-unify-args( lt rt1 ))) (maybe-deref(typecheck-unify-args( lt rt2 ))) )) (
()
( (TCPair( TCtxEOF TCtxEOF )) () )
( (TCPair( lctx TCtxEOF )) (set ctx lctx) )
( (TCPair( TCtxEOF rctx )) (set ctx rctx) )
( (TCPair( lctx rctx )) (tail(
(let nctx (maybe-deref(merge( lctx rctx ))))
(set ctx nctx)
)))
))
))
( (TPair( (TGround( ltn TypeEOF )) (TGround( rtn TypeEOF )) )) (
(if (==( ltn rtn )) (tail(
(let ctx2 (maybe-deref(tcontext-accept())))
(set ctx ctx2)
)) ())
))
( (TPair( (TGround( ltn (TypeSeq( TypeEOF lt1 )) )) (TGround( rtn (TypeSeq( TypeEOF rt1 )) )) )) (
(if (==( ltn rtn )) (tail(
(let ctx2 (maybe-deref(typecheck-unify-args( lt1 rt1 ))))
(set ctx ctx2)
)) ())
))
( (TPair( (TGround( ltn (TypeSeq( (TypeSeq( TypeEOF lt1 )) lt2 )) )) (TGround( rtn (TypeSeq( (TypeSeq( TypeEOF rt1 )) rt2 )) )) )) (
(if (==( ltn rtn )) (tail(
(let ctx2 (maybe-deref(typecheck-unify-args( lt1 rt1 ))))
(if (non-zero ctx2) (tail(
(let ctx3 (maybe-deref(typecheck-unify-args( lt2 rt2 ))))
(set ctx ctx3)
)) ())
)) ())
))
( _ () )
))
(close ctx)
)) TContext[]);
tarrow := λ(: lt Type)(: rt Type). (: (tail(
()
(close(TGround( '->_s
(close(TypeSeq( (close(TypeSeq( (close TypeEOF) lt ))) rt )))
)))
)) Type[]);
tarray := λ(: lt Type)(: rt Type). (: (tail(
()
(close(TGround( 'Array_s
(close(TypeSeq( (close(TypeSeq( (close TypeEOF) lt ))) rt )))
)))
)) Type[]);
tlabel := λ. (: (tail(
()
(close(TGround( 'Label_s (close TypeEOF) )))
)) Type[]);
typecheck-infer-ctx := λ(: tctx TContext)(: lhs AST). (: (tail(
(match lhs (
()
( (Asc( (Var v) tt )) (
(set tctx (TCtxBind(
(close tctx)
v
tt
)))
))
( (App( ps (Asc( (Var v) tt )) )) (tail(
(set tctx (TCtxBind(
(close tctx)
v
tt
)))
(let tctx2 (maybe-deref(typecheck-infer-ctx( tctx ps ))))
(set tctx tctx2)
)))
( _ () )
))
(close tctx)
)) TContext[]);
typecheck-typeof-var := λ(: sloc AST)(: tctx TContext)(: vname String). (: (tail(
(let found TAny)
(while (non-zero tctx) (match tctx (
()
( (TCtxBind( rst (*( k vt )) )) (tail(
(if (==( k vname )) (
(if (non-zero found) (
(if (is-arrow vt) (
(set found (TAnd(
(close found)
(close vt)
)))
) (
(set found vt)
))
) (
(set found vt)
))
) ())
(set tctx rst)
)))
)))
(if (non-zero found) () (
(exit-error( 'Unknown\sReferenced\sVariable_s sloc ))
))
(close found)
)) Type[]);