# global Tag -> Class map, mutable
tag-to-class-index := (: StrTEOF StringTypeList);
# global Tag -> Fields map, mutable
tag-to-fields-index := (: StrTEOF StringTypeList);
# global Tag -> IsFragment? map, mutable
tag-is-fragment-index := (: SLEOF StringList);
# global Class -> Size map, mutable
class-to-size-index := (: SUEOF StringU64List);
# global Tag -> Index map, mutable
tag-to-index-index := (: SUEOF StringU64List);
unknown-index-of-tag := 99999_u64;
# has typechecking finished? boolean, mutable
types-have-changed := True_u8;
index-of-tag := λ(: tag String). (: (tail(
(let r unknown-index-of-tag)
(let index tag-to-index-index)
(while (non-zero index) (match index (
()
( (SUSeq( rst tag-name tag-index )) (
(if (==( tag tag-name )) (tail(
(set r tag-index)
(set index SUEOF)
)) (set index rst))
))
)))
r
)) U64);
index-index-of-tag := λ(: tag String)(: index U64). (: (
(set tag-to-index-index (SUSeq(
(close tag-to-index-index) tag index
)))
) Nil);
index-size-of-class := λ(: class String)(: size U64). (: (
(if (size-of-class class) () (
(set class-to-size-index (SUSeq(
(close class-to-size-index)
class
size
)))
))
) Nil);
size-of-class := λ(: class String). (: (tail(
(let sz 0_u64)
(let index class-to-size-index)
(while (non-zero index) (match index (
()
( (SUSeq( rst kclass ksize )) (
(if (==( kclass class )) (tail(
(set sz ksize)
(set index SUEOF)
)) (set index rst))
))
)))
sz
)) U64);
index-tag-is-fragment := λ(: tag String). (: (
(set tag-is-fragment-index (SLSeq(
(close tag-is-fragment-index) tag
)))
) Nil);
is-fragment := λ(: tag String). (: (tail(
(let index tag-is-fragment-index)
(let rt 0_u64)
(while (non-zero index) (match index (
()
( (SLSeq( rst itag )) (
(if (==( tag itag )) (tail(
(set rt 1_u64)
(set index SLEOF)
)) (set index rst))
))
)))
rt
)) U64);
is-fragment := λ(: tt Type). (: (tail(
(let r (is-fragment(tag-of tt)))
r
)) U64);
tag-of := λ(: tt Type). (: (tail(
(let tag '_s)
(match tt (
()
( (TAnd( lt rt )) (tail(
(let ltag (tag-of lt))
(if (non-zero ltag) (set tag ltag) ())
(let rtag (tag-of rt))
(if (non-zero rtag) (set tag rtag) ())
)))
( (TGround( tg _ )) (set tag tg) )
( _ () )
))
tag
)) String);
index-class-of-tag := λ(: tag String)(: class Type). (: (
(set tag-to-class-index (StrTSeq(
(close tag-to-class-index) tag class
)))
) Nil);
class-of-tag := λ(: tag String). (: (tail(
(let index tag-to-class-index)
(let rt TAny)
(while (non-zero index) (match index (
()
( (StrTSeq( rst itag iclass )) (
(if (==( tag itag )) (tail(
(set rt iclass)
(set index StrTEOF)
)) (set index rst))
))
)))
rt
)) Type);
is-class := λ(: tag String). (: (tail(
(let index tag-to-class-index)
(let rt 0_u64)
(while (non-zero index) (match index (
()
( (StrTSeq( rst itag (TGround( ctag _ )) )) (
(if (==( tag ctag )) (tail(
(set rt 1_u64)
(set index StrTEOF)
)) (set index rst))
))
)))
rt
)) U64);
index-fields-of-tag := λ(: tag String)(: fields Type). (: (
(set tag-to-fields-index (StrTSeq(
(close tag-to-fields-index) tag fields
)))
) Nil);
fields-of-tag := λ(: tag String). (: (tail(
(let index tag-to-fields-index)
(let rt TAny)
(while (non-zero index) (match index (
()
( (StrTSeq( rst itag ifields )) (
(if (==( tag itag )) (tail(
(set rt ifields)
(set index StrTEOF)
)) (set index rst))
))
)))
rt
)) Type);
slot := λ(: tt Type)(: sl String). (: (tail(
(let rt TAny)
(match tt (
()
( (TGround( bt _ )) (
(if (==( bt sl )) (set rt tt) ())
))
( (TAnd( ltt rtt )) (tail(
(let lt2 (slot( ltt sl )))
(if (non-zero lt2) (
(set rt lt2)
) (tail(
(let rt2 (slot( rtt sl )))
(set rt rt2)
)))
)))
( _ () )
))
rt
)) Type);
domain := λ(: tt Type). (: (tail(
(let r TAny)
(match (slot( tt 'Arrow_s )) (
()
( (TGround( 'Arrow_s (TypeSeq( (TypeSeq( TypeEOF p1 )) p2 )) )) (set r p1) )
( _ () )
))
r
)) Type);
range := λ(: tt Type). (: (tail(
(let r TAny)
(match (slot( tt 'Arrow_s )) (
()
( (TGround( 'Arrow_s (TypeSeq( (TypeSeq( TypeEOF p1 )) p2 )) )) (set r p2) )
( _ () )
))
r
)) Type);
is-open := λ(: tt Type). (: (tail(
(let r 0_u64)
(match tt (
()
( TAny () )
( (TVar _) (set r 1_u64) )
( (TAnd( lt rt )) (tail(
(if (is-open lt) (set r 1_u64) ())
(if (is-open rt) (set r 1_u64) ())
)))
( (TGround( _ pars )) (
(while (non-zero pars) (match pars (
()
( (TypeSeq( rst p1 )) (tail(
(if (is-open p1) (set r 1_u64) ())
(set pars rst)
)))
)))
))
))
r
)) U64);
is-arrow := λ(: tt Type). (: (tail(
(let r 0_u64)
(match (slot( tt 'Arrow_s )) (
()
( (TGround( 'Arrow_s _ )) (set r 1_u64) )
( _ () )
))
r
)) U64);
t3 := λ(: tag String)(: p1 Type)(: p2 Type). (: (tail(
(let tt (TGround(
tag
(close(TypeSeq( (close(TypeSeq( (close TypeEOF) p1 ))) p2 )))
)))
tt
)) Type);
t2 := λ(: tag String)(: p1 Type). (: (tail(
(let tt (TGround(
tag
(close(TypeSeq( (close TypeEOF) p1 )))
)))
tt
)) Type);
t1 := λ(: tag String). (: (tail(
(let tt (TGround(
tag
(close TypeEOF)
)))
tt
)) Type);
tsized := λ(: tag String). (: (tail(
(let tt (t2( 'Sized_s (t1 tag) )))
tt
)) Type);
substitute := λ(: tctx TContext)(: tt TypeList). (: (tail(
(match tt (
()
( TypeEOF () )
( (TypeSeq( rst par )) (
(set tt (TypeSeq(
(close(substitute( tctx rst )))
(substitute( tctx par ))
)))
))
))
tt
)) TypeList);
substitute := λ(: tctx TContext)(: tt Type). (: (tail(
(match tt (
()
( (TVar v) (
(while (non-zero tctx) (match tctx (
()
( TCtxNil (set tctx TCtxEOF) )
( (TCtxBind( rst tk tv _ )) (
(if (==( tk v )) (tail(
(set tt tv)
(set tctx TCtxEOF)
)) (set tctx rst))
))
)))
))
( (TGround( tag pars )) (
(set tt (TGround(
tag
(close(substitute( tctx pars )))
)))
))
( (TAnd( lt rt )) (
(set tt (TAnd(
(close(substitute( tctx lt )))
(close(substitute( tctx rt )))
)))
))
( _ () )
))
tt
)) Type);
union := λ(: lctx TContext)(: rctx TContext). (: (tail(
(match rctx (
()
( TCtxNil (set rctx TCtxEOF) )
( (TCtxBind( rst k v t )) (tail(
(set lctx (union( lctx rst )))
(set lctx (TCtxBind( (close lctx) k v t )))
)))
( _ () )
))
lctx
)) TContext);
without-tag := λ(: tt Type). (: (tail(
(match tt (
()
( (TAnd( lt rt )) (tail(
(let lt1 (without-tag lt))
(let rt1 (without-tag 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( possibly-tag-name ps )) (tail(
(set tt (TGround( possibly-tag-name (close(without-tag ps)) )))
(let class (class-of-tag possibly-tag-name))
(if (non-zero class) ( # This tag has a class
(if (!=( (tag-of class) possibly-tag-name )) ( # This tag is not a class
(set tt TAny) # So remove this tag
) ())
) ())
)))
( tt () )
))
tt
)) Type);
without-tag := λ(: tt TypeList). (: (tail(
(match tt (
()
( (TypeSeq( rst p1 )) (
(set tt (TypeSeq( (close(without-tag rst)) (without-tag p1) )))
))
( TypeEOF () )
))
tt
)) TypeList);
with-only-tag := λ(: tt Type). (: (tail(
(let rt TAny)
(match tt (
()
( (TAnd( lt1 rt1 )) (tail(
(let lc (with-only-tag lt1))
(if (non-zero lc) (set rt lc) ())
(let rc (with-only-tag rt1))
(if (non-zero rc) (set rt rc) ())
)))
( (TGround( tag _ )) (tail(
(let class (class-of-tag tag))
(if (non-zero class) (
(if (not(is-fragment tag)) (
(set rt tt)
) ())
) ())
)))
( _ () )
))
rt
)) Type);
with-only-class := λ(: tt Type). (: (tail(
(let rt TAny)
(match tt (
()
( (TAnd( lt1 rt1 )) (tail(
(let lc (with-only-class lt1))
(if (non-zero lc) (set rt lc) ())
(let rc (with-only-class rt1))
(if (non-zero rc) (set rt rc) ())
)))
( (TGround( tag _ )) (
(if (is-class tag) (
(if (not(is-fragment tag)) (
(set rt tt)
) ())
) ())
))
( _ () )
))
rt
)) Type);
without-representation := λ(: tt TypeList). (: (tail(
(match tt (
()
( (TypeSeq( rst p1 )) (
(set tt (TypeSeq(
(close(without-representation rst))
(without-representation p1)
)))
))
( TypeEOF () )
))
tt
)) TypeList);
without-representation := λ(: tt Type). (: (tail(
(match tt (
()
( (TAnd( lt rt )) (tail(
(let lt2 (without-representation lt))
(let rt2 (without-representation rt))
(if (non-zero lt2) (
(if (non-zero rt2) (
(set tt (TAnd( (close lt2) (close rt2) )))
) (
(set tt lt2)
))
) (
(if (non-zero rt2) (
(set tt rt2)
) (
(set tt TAny)
))
))
)))
( (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) )
( (TGround( 'Reg8_s TypeEOF )) (set tt TAny) )
( (TGround( 'Reg16_s TypeEOF )) (set tt TAny) )
( (TGround( 'Reg32_s TypeEOF )) (set tt TAny) )
( (TGround( 'Reg64_s TypeEOF )) (set tt TAny) )
( (TGround( tag ps )) (
(set tt (TGround( tag (close(without-representation ps)) )))
))
( TAny () )
( (TVar _) () )
))
tt
)) Type);
without-size := λ(: tt TypeList). (: (tail(
(match tt (
()
( (TypeSeq( rst p1 )) (
(set tt (TypeSeq(
(close(without-size rst))
(without-size p1)
)))
))
( TypeEOF () )
))
tt
)) TypeList);
without-size := λ(: tt Type). (: (tail(
(match tt (
()
( (TAnd( lt rt )) (tail(
(let lt2 (without-size lt))
(let rt2 (without-size rt))
(if (non-zero lt2) (
(if (non-zero rt2) (
(set tt (TAnd( (close lt2) (close rt2) )))
) (
(set tt lt2)
))
) (
(if (non-zero rt2) (
(set tt rt2)
) (
(set tt TAny)
))
))
)))
( (TGround( 'Sized_s sz )) (set tt TAny) )
( (TGround( tag ps )) (
(set tt (TGround( tag (close(without-size ps)) )))
))
( TAny () )
( (TVar _) () )
))
tt
)) Type);
without-size-unless-class := λ(: tt TypeList). (: (tail(
(match tt (
()
( (TypeSeq( rst p1 )) (
(set tt (TypeSeq(
(close(without-size-unless-class rst))
(without-size-unless-class p1)
)))
))
( TypeEOF () )
))
tt
)) TypeList);
without-size-unless-class := λ(: tt Type). (: (tail(
(match tt (
()
( (TAnd( lt rt )) (tail(
(let lt2 (without-size-unless-class-inner lt))
(let rt2 (without-size-unless-class-inner rt))
(if (non-zero lt2) (
(if (non-zero rt2) (
(set tt (TAnd( (close lt2) (close rt2) )))
) (
(set tt lt2)
))
) (
(if (non-zero rt2) (
(set tt rt2)
) (
(set tt TAny)
))
))
)))
( (TGround( tag ps )) (
(set tt (TGround( tag (close(without-size-unless-class ps)) )))
))
( TAny () )
( (TVar _) () )
))
tt
)) Type);
without-size-unless-class-inner := λ(: tt Type). (: (tail(
(match tt (
()
( (TAnd( lt rt )) (tail(
(let lt2 (without-size-unless-class-inner lt))
(let rt2 (without-size-unless-class-inner rt))
(if (non-zero lt2) (
(if (non-zero rt2) (
(set tt (TAnd( (close lt2) (close rt2) )))
) (
(set tt lt2)
))
) (
(if (non-zero rt2) (
(set tt rt2)
) (
(set tt TAny)
))
))
)))
( (TGround( 'Sized_s _ )) (set tt TAny) )
( (TGround( tag ps )) (
(set tt (TGround( tag (close(without-size-unless-class ps)) )))
))
( TAny () )
( (TVar _) () )
))
tt
)) Type);
normalize := λ(: tt Type). (: (tail(
(let rt tt)
(set rt (without-representation rt))
(set rt (without-tag rt))
# Sized can serve as a datatype if nothing else is available
(set rt (without-size-unless-class rt))
rt
)) Type);
print := λ(: tt Type). (: (match tt (
()
( TAny (print '?_s) )
( (TVar( vn )) (print vn) )
( (TGround( tag TypeEOF )) (print tag) )
( (TAnd( lt rt )) (tail(
(print lt)
(print '\s+\s_s)
(print rt)
)))
( (TGround( tag ps )) (tail(
(print tag)
(print '<_s)
(print ps)
(print '>_s)
)))
)) Nil);
print := λ(: tt TypeList). (: (match tt (
()
( TypeEOF () )
( (TypeSeq( TypeEOF p1 )) (print p1) )
( (TypeSeq( rst p1 )) (tail(
(print rst)
(print ',_s)
(print p1)
)))
)) Nil);
== := λ(: 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 lps )) (TGround( rn rps )) )) (
(if (==( ln rn )) (
(if (==( lps rps )) (
(set r 1_u64)
) ())
) ())
))
( _ () )
))
r
)) U64);
== := λ(: lt TypeList)(: rt TypeList). (: (tail(
(let r 0_u64)
(match (TLPair( lt rt )) (
()
( (TLPair( TypeEOF TypeEOF )) (set r 1_u64) )
( (TLPair( (TypeSeq( ltr lt1 )) (TypeSeq( rtr rt1 )) )) (
(if (==( lt1 rt1 )) (
(if (==( ltr rtr )) (
(set r 1_u64)
) ())
) ())
))
( _ () )
))
r
)) U64);
can-unify := λ(: fpt TypeList)(: pt TypeList). (: (tail(
(let r 0_u64)
(match (TLPair( fpt pt )) (
()
( (TLPair( TypeEOF TypeEOF )) (set r 1_u64) )
( (TLPair( (TypeSeq( lpr lp1 )) (TypeSeq( rpr rp1 )) )) (
(if (can-unify( lp1 rp1 )) (
(if (can-unify( lpr rpr )) (
(set r 1_u64)
) ())
) ())
))
( _ () )
))
r
)) U64);
can-unify := λ(: fpt Type)(: pt Type). (: (tail(
(let r 0_u64)
(match (TPair( fpt pt )) (
()
( (TPair( TAny _ )) (set r 1_u64) )
( (TPair( (TVar( ltv )) rt )) (set r 1_u64) )
( (TPair( (TAnd( lt1 lt2 )) rt )) (
(if (can-unify( lt1 rt )) (
(if (can-unify( lt2 rt )) (
(set r 1_u64)
) ())
) ())
))
( (TPair( lt (TAnd( rt1 rt2 )) )) (tail(
(if (can-unify( lt rt1 )) (set r 1_u64) ())
(if (can-unify( lt rt2 )) (set r 1_u64) ())
)))
( (TPair( (TGround( 'GT_s (TypeSeq( TypeEOF (TGround( lbase TypeEOF )) )) )) (TGround( rbase TypeEOF )) )) (
(if (>( (to-i64 rbase) (to-i64 lbase) )) (
(set r 1_u64)
) ())
))
( (TPair( (TGround( ltn lps )) (TGround( rtn rps )) )) (
(if (==( ltn rtn )) (
(if (can-unify( lps rps )) (
(set r 1_u64)
) ())
) ())
))
( _ () )
))
r
)) U64);
to-string := λ(: tt Type). (: (tail(
(let r (to-string-impl tt))
(clone-rope r)
)) String);
to-string := λ(: tt TypeList). (: (tail(
(let r SNil)
(match tt (
()
( TypeEOF () )
( (TypeSeq( TypeEOF p1 )) (set r (to-string-impl p1)) )
( (TypeSeq( rst p1 )) (
(set r (SCons(
(close(to-string rst))
(close(SCons(
(close(SAtom ',_s))
(close(to-string-impl p1))
)))
)))
))
))
r
)) S);
to-string-impl := λ(: tt Type). (: (tail(
(let r SNil)
(match tt (
()
( TAny (set r (SAtom '?_s)) )
( (TVar v) (set r (SAtom v)) )
( (TAnd( lt rt )) (tail(
(let ls (to-string-impl lt))
(let rs (to-string-impl rt))
(set r (SCons(
(close ls)
(close(SCons(
(close(SAtom '+_s))
(close rs)
)))
)))
)))
( (TGround( tag TypeEOF )) (
(set r (SAtom tag))
))
( (TGround( tag ps )) (tail(
(set r (SAtom tag))
(set r (SCons( (close r) (close(SAtom '<_s)) )))
(set r (SCons( (close r) (close(to-string ps)) )))
(set r (SCons( (close r) (close(SAtom '>_s)) )))
)))
))
r
)) S);
type-of-s := λ(: compound AST). (: (tail(
(let r TAny)
(match compound (
()
( (Lit tt) (tail(
(let nt (parse-type tt))
(set r nt)
)))
( (Var tt) (tail(
(let nt (parse-type tt))
(set r nt)
)))
( (App( (App( lt (Lit ',_s) )) rt )) (tail(
(let ltt (type-of-s lt))
(let rtt (type-of-s rt))
(set r (TGround(
'Cons_s
(close(TypeSeq(
(close(TypeSeq(
(close TypeEOF)
ltt
)))
rtt
)))
)))
)))
( _ (exit-error( 'Malformed\sType\sDefinition_s compound )))
))
r
)) Type);
normalize := λ(: tctx TContext). (: (tail(
(match tctx (
()
( TCtxEOF () )
( TCtxNil (set tctx TCtxEOF) )
( (TCtxBind( rst k kt t )) (tail(
(set rst (normalize rst))
(set tctx (TCtxBind(
(close rst)
k (normalize kt) t
)))
)))
))
tctx
)) TContext);
with-only-representation := λ(: tt TypeList). (: (tail(
(let rt tt)
(match tt (
()
( (TypeSeq( rst p1 )) (
(set rt (TypeSeq(
(close(with-only-representation rst))
(with-only-representation p1)
)))
))
( TypeEOF () )
))
rt
)) TypeList);
with-only-representation := λ(: tt Type). (: (tail(
(let return tt)
(match tt (
()
( (TAnd( lt rt )) (tail(
(let lt2 (with-only-representation lt))
(let rt2 (with-only-representation rt))
(if (non-zero lt2) (
(if (non-zero rt2) (
(set return (TAnd( (close lt2) (close rt2) )))
) (
(set return lt2)
))
) (
(if (non-zero rt2) (
(set return rt2)
) (
(set return TAny)
))
))
)))
( (TGround( 'Constant_s TypeEOF )) () )
( (TGround( 'Literal_s TypeEOF )) () )
( (TGround( 'StackVariable_s TypeEOF )) () )
( (TGround( 'LocalVariable_s TypeEOF )) () )
( (TGround( 'GlobalVariable_s TypeEOF )) () )
( (TGround( 'Reg8_s TypeEOF )) () )
( (TGround( 'Reg16_s TypeEOF )) () )
( (TGround( 'Reg32_s TypeEOF )) () )
( (TGround( 'Reg64_s TypeEOF )) () )
( (TGround( tag ps )) (set return TAny) )
( TAny () )
( (TVar _) (set return TAny) )
))
return
)) Type);
unify := λ(: fpt Type)(: pt Type). (: (tail(
(let ctx TCtxEOF)
(if (can-unify( fpt pt )) (
(set ctx (unify-inner( fpt pt )))
) ())
ctx
)) TContext);
unify-inner := λ(: fpt Type)(: pt Type). (: (tail(
(let ctx TCtxEOF)
(match (TPair( fpt pt )) (
()
( (TPair( TAny _ )) (
(set ctx TCtxNil)
))
( (TPair( (TVar( ltv )) rt )) (
(set ctx (TCtxBind(
(close TCtxEOF)
ltv
rt
ASTEOF
)))
))
( (TPair( (TAnd( lt1 lt2 )) rt )) (
(match (TCPair( (unify-inner( lt1 rt )) (unify-inner( lt2 rt )) )) (
()
( (TCPair( TCtxEOF _ )) () )
( (TCPair( _ TCtxEOF )) () )
( (TCPair( lctx rctx )) (
(set ctx (union( lctx rctx )))
))
))
))
( (TPair( lt (TAnd( rt1 rt2 )) )) (
(match (TCPair( (unify-inner( lt rt1 )) (unify-inner( lt rt2 )) )) (
()
( (TCPair( TCtxEOF TCtxEOF )) () )
( (TCPair( lctx TCtxEOF )) (set ctx lctx) )
( (TCPair( TCtxEOF rctx )) (set ctx rctx) )
( (TCPair( lctx rctx )) (
(set ctx (union( lctx rctx )))
))
))
))
( (TPair( (TGround( 'GT_s (TypeSeq( TypeEOF (TGround( lbase TypeEOF )) )) )) (TGround( rbase TypeEOF )) )) (
(if (>( (to-i64 rbase) (to-i64 lbase) )) (
(set ctx TCtxNil)
) ())
))
( (TPair( (TGround( ltn lps )) (TGround( rtn rps )) )) (
(if (==( ltn rtn )) (
(set ctx (unify( lps rps )))
) ())
))
( _ () )
))
ctx
)) TContext);
unify := λ(: fpt TypeList)(: pt TypeList). (: (tail(
(let ctx TCtxEOF)
(match (TLPair( fpt pt )) (
()
( (TLPair( TypeEOF TypeEOF )) (set ctx TCtxNil) )
( (TLPair( (TypeSeq( lps lp1 )) (TypeSeq( rps rp1 )) )) (tail(
(set ctx (unify( lp1 rp1 )))
(if (non-zero ctx) (
(set ctx (union( ctx (unify( lps rps )) )))
) ())
)))
( _ () )
))
ctx
)) TContext);
fields-of-tag := λ(: tag Type)(: class Type). (: (tail(
(let rhst TAny)
(match tag (
()
( (TGround( ts _ )) (match (fields-of-tag ts) (
()
( (TGround( 'Cons_s (TypeSeq( (TypeSeq( TypeEOF fields-lhs )) fields-rhs )) )) (
(set rhst (substitute( (unify( fields-lhs class )) fields-rhs )))
))
)))
( _ (tail(
(print 'Invalid\sTag\sIn\sfields-of-tag\s_s)
(print tag)(print '\n_s)
(exit 1_u64)
)))
))
(set rhst (with-size rhst))
(let rt (TGround( 'Fields_s (close(TypeSeq(
(close TypeEOF)
(fields-of-type( (t3( 'Cons_s rhst (TAnd( (close(t1 'U64_s)) (close(t2( 'Sized_s (t1 '8_s) ))) )) )) ))
))))))
rt
)) Type);
fields-of-type := λ(: tt Type). (: (tail(
(match tt (
()
( TAny (set tt (t1 'Nil_s)) )
( (TGround( 'Cons_s (TypeSeq( (TypeSeq( TypeEOF p1 )) p2 )) )) (
(set tt (TGround(
'Cons_s
(close(TypeSeq(
(close(TypeSeq(
(close TypeEOF)
(fields-of-type p1)
)))
p2
)))
)))
))
( _ (
(set tt (TGround(
'Cons_s
(close(TypeSeq(
(close(TypeSeq(
(close TypeEOF)
(t1 'Nil_s)
)))
tt
)))
)))
))
))
tt
)) Type);
s-type-list := (: STEOF STypeList);
ascript := λ(: t S)(: tt Type). (: (
(set s-type-list (STSeq(
(close s-type-list)
t tt
)))
) Nil);
typeof := λ(: term S). (: (tail(
(let found TAny)
(let tctx s-type-list)
(while (non-zero tctx) (match tctx (
()
( (STSeq( rst s tt )) (
(if (is( s term )) (tail(
(set found tt)
(set tctx STEOF)
)) (
(set tctx rst)
))
))
)))
found
)) Type);
to-s := λ(: term AST). (: (tail(
(let s SNil)
(match term (
()
( (Var v) (
(set s (SCons(
(close(SAtom 'Var_s))
(close(SAtom v))
)))
))
( (Lit v) (
(set s (SCons(
(close(SAtom 'Lit_s))
(close(SAtom v))
)))
))
( (App( lt rt )) (
(set s (SCons(
(close(SAtom 'App_s))
(close(SCons(
(close(to-s lt))
(close(to-s rt))
)))
)))
))
( (Abs( lt rt tlt )) (
(set s (SCons(
(close(SAtom 'Abs_s))
(close(SCons(
(close(to-s lt))
(close(to-s rt))
)))
)))
))
( (Sizeof( tt )) (tail(
(set s (SAtom( (clone-rope(SAtom('Sizeof_s))) )))
(ascript( s tt ))
)))
( (Asc( t tt )) (tail(
(set s (to-s t))
(ascript( s tt ))
)))
( (As( t tt )) (tail(
(set s (to-s t))
(ascript( s tt ))
)))
( (As( t tt )) (tail(
(set s (to-s t))
(ascript( s tt ))
)))
( _ () )
))
s
)) S);
ascript-normal := λ(: t AST)(: tt Type). (: (
(if (non-zero tt) (tail(
(let prev-tt (normalize(typeof t)))
(if (non-zero prev-tt) (
(if (is-arrow tt) () (tail(
(let norm-tt (normalize tt))
(if (==( prev-tt norm-tt )) () (tail(
(print prev-tt)
(print '\s!=\s_s)
(print norm-tt)
(print '\n_s)
(exit-error( 'Type\sAscription\sInequality_s t ))
)))
)))
) (tail(
(let sized-tt (with-size tt))
(ascript( t sized-tt ))
(set types-have-changed True_u8)
)))
)) ())
) Nil)