Not Quite Four but Hello World

Example.idr

module Example

import Ola

public export
example : Prog Nil Nil UNIT
example
  = DefType TyStr
  $ DefFunc (TyFunc TyUnit (TyVar Here))
            (Fun (Return (S "Hello World")
            ))
  $ Main
  $ Let TyStr
        (Call (Var Here) U)
  $ Print (Var Here)
  $ Return U

public export
example1 : Prog Nil Nil UNIT
example1
  = DefFunc (TyFunc (TyUnion TyStr TyInt)
                    TyStr)
            (Fun (Return $ Match (Var Here)
                                 (Var Here)
                                 (S "Hello")
            ))
  $ Main
  $ Let (TyUnion TyStr TyInt)
        (Left (S "AA"))
  $ Print (Call (Var (There Here))
                (Var Here))
  $ Return U

public export
example2 : Prog Nil Nil UNIT
example2
  = Main
  $ Let (TyRef TyStr)
        (Alloc (S "HelloWorld"))
  $ Print (Fetch $ Var Here)
  $ Discard (Mutate (Var Here)
                    (S "Goodbye World"))
  $ Print (Fetch $ Var Here)
  $ Return U

Main.idr

module Main

import Ola
import Example

main : IO ()
main
  = do Ola.run (exec example)
       Ola.run (exec example1)
       Ola.run (exec example2)

Run.sh

$ idris2 --build ola.ipkg
$ ./build/exec/ola
"Hello World"
"AA"
"HelloWorld"
"Goodbye World"