stg.bend checks

type SExp source · line 13 · raw

Data

• SVar

  @i:U32 -> SExp

• SLit

  @v:Nat -> SExp

• SAdd

  @a:SExp -> @b:SExp -> SExp

• SLet

  @b:SExp -> @e:SExp -> SExp

• SApp

  @f:SExp -> @x:SExp -> SExp

• SCase

  @e:SExp -> @z:SExp -> @s:SExp -> SExp

type SVal source · line 21 · raw

Data

• VNum

  @v:Nat -> SVal

• VAddr

  @a:Nat -> SVal

• VClos

  @body:SExp -> @env:List<&2, SVal> -> SVal

• VThunk

  @body:SExp -> @env:List<&2, SVal> -> SVal

type SK source · line 27 · raw

Data

• KDone

  SK

• KAddR

  @a:SVal -> @k:SK -> SK

• KAppA

  @x:SExp -> @env:List<&2, SVal> -> @k:SK -> SK

• KCaseK

  @z:SExp -> @s:SExp -> @env:List<&2, SVal> -> @k:SK -> SK

• KUpd

  @a:Nat -> @k:SK -> SK

type STask source · line 34 · raw

Data

• SEval

  @e:SExp -> @env:List<&2, SVal> -> @heap:List<&2, SVal> -> @k:SK -> STask

• SRet

  @k:SK -> @v:SVal -> @heap:List<&2, SVal> -> STask

• SLook

  @n:Nat -> @env:List<&2, SVal> -> @heap:List<&2, SVal> -> @k:SK -> STask

• SLoad

  @cur:Nat -> @orig:Nat -> @rest:List<&2, SVal> -> @full:List<&2, SVal> -> @k:SK -> STask

def s_len source · line 40 · raw

@+h:List<&2, SVal> -> Nat

def s_nth source · line 47 · raw

@+a:Nat -> @+h:List<&2, SVal> -> SVal

def s_upd source · line 56 · raw

@+a:Nat -> @+v:SVal -> @+h:List<&2, SVal> -> List<&2, SVal>

def s_num_add source · line 65 · raw

@+a:SVal -> @+b:SVal -> SVal

def s_run source · line 72 · raw

@+f:Nat -> @+t:STask -> SVal

def s_eval source · line 148 · raw

@+f:Nat -> @+e:SExp -> SVal

def s_batch source · line 151 · raw

@+f:Nat -> @+es:List<&2, SExp> -> List<&2, SVal>

def s_batch_gpu source · line 159 · raw

@+f:Nat -> @+es:List<&2, SExp> -> List<&2, SVal>

def main source · line 162 · raw

List<&2, SVal>