text:
import Interfaces

-- State Definition

data State : Type -> Type -> Type where
  stateFunc : (s -> (a, s)) -> State s a

getStateFunc : (state : State s a) -> (s -> (a, s))
getStateFunc (stateFunc f) = f

-- Define state equality

data StateEq : state1 -> state2 -> Type where
  stateEq : {u : State s a} -> {v : State s a} -> (getStateFunc u `FuncEqType` getStateFunc v) -> StateEq u v

stateEqTransitiveLemma : {f : a -> b} -> {g : a -> b} -> {h : a -> b} -> FuncEqType f g -> FuncEqType g h -> (x : a) -> f x = h x
stateEqTransitiveLemma (funcEqType f g f_eq_g) (funcEqType g h g_eq_h) x = rewrite f_eq_g x in g_eq_h x

stateEqTransitive : {f : State s a} -> {g : State s a} -> {h : State s a} -> StateEq f g -> StateEq g h ->  StateEq f h
stateEqTransitive (stateEq x) (stateEq y) = stateEq (funcEqType (getStateFunc f) (getStateFunc h) (stateEqTransitiveLemma x y))

stateEqReflexive : {f : State s a} -> StateEq f f
stateEqReflexive = stateEq (funcEqType (getStateFunc f) (getStateFunc f) (\x => Refl))

stateEqSymmetryLemma : {f : a -> b} -> {g : a -> b} -> FuncEqType f g -> (x : a) -> g x = f x
stateEqSymmetryLemma (funcEqType f g f_eq_g) x = sym (f_eq_g x)

stateEqSymmetry : {f : State s a} -> {g : State s a} -> StateEq f g -> StateEq g f
stateEqSymmetry (stateEq x) = stateEq (funcEqType (getStateFunc g) (getStateFunc f) (stateEqSymmetryLemma x))

-- map for State

mapFirst : (f : a -> c) -> (a, b) -> (c, b)
mapFirst f (x, y) = (f x, y)

mapState : (f : a -> b) -> (state : State s a) -> State s b
mapState f (stateFunc g) = stateFunc (mapFirst f . g)

-- Verify that State is Functor

mapFirstIdLemma : (x : (a, b)) -> mapFirst Prelude.id x = x
mapFirstIdLemma (p, q) = Refl

stateFunctorLawIdentityLemma : (state : State s a) -> (x : s) -> getStateFunc (mapState Prelude.id state) x = getStateFunc state x
stateFunctorLawIdentityLemma (stateFunc f) x = mapFirstIdLemma (f x)

stateFunctorLawIdentity : (state : State s a) -> mapState Prelude.id state `StateEq` state
stateFunctorLawIdentity state = stateEq $ funcEqType (getStateFunc $ mapState Prelude.id state) (getStateFunc state) (stateFunctorLawIdentityLemma state)

mapFirstCompositionLemma : (g : b -> c) -> (h : a -> b) -> (x : (a, s)) -> mapFirst (g . h) x = mapFirst g (mapFirst h x)
mapFirstCompositionLemma g h (p, q) = Refl

stateFunctorLawCompositionLemma : (state : State s a) -> (g : (b -> c)) -> (h : (a -> b)) -> (x : s) -> getStateFunc (mapState (g . h) state) x = getStateFunc (mapState g (mapState h state)) x
stateFunctorLawCompositionLemma (stateFunc f) g h x = rewrite mapFirstCompositionLemma g h (f x)in Refl

stateFunctorLawComposition : (g : (b -> c)) -> (h : (a -> b)) -> (state : State s a) -> mapState (g . h) state `StateEq` mapState g (mapState h state)
stateFunctorLawComposition g h state = stateEq $ funcEqType (getStateFunc $ mapState (g . h) state) (getStateFunc $ mapState g $ mapState h state) (stateFunctorLawCompositionLemma state g h)

MyFunctor (State s) where
  equalsTo = StateEq
  eqReflexive = stateEqReflexive
  eqSymmetry = stateEqSymmetry
  eqTransitive = stateEqTransitive
  myMap = mapState
  functorLawIdentity = stateFunctorLawIdentity
  functorLawComposition = stateFunctorLawComposition

-- Applicative functions

pureState : (s : Type) -> (x : a) -> State s a
pureState s x = stateFunc (\state => (x, state))

infixl 3 <<**>>

(<<**>>) : State s (a -> b) -> State s a -> State s b
(<<**>>) (stateFunc ff) (stateFunc gg) = stateFunc newStateFunc
where
  newStateFunc : (ss : s) -> (b, s)
  newStateFunc ss = mapFirst (fst $ ff ss) (gg $ snd (ff ss))

-- Applicative laws

stateApplicativeLawIdentityLemma : (u : State s a) -> (x : s) -> getStateFunc (stateFunc (\s => (Prelude.id, s)) <<**>> u) x = getStateFunc u x
stateApplicativeLawIdentityLemma (stateFunc f) x = mapFirstIdLemma (f x)

stateApplicativeLawIdentity : (s : Type) -> (u : State s a) -> (pureState s Prelude.id <<**>> u) `StateEq` u
stateApplicativeLawIdentity s u = stateEq $ funcEqType (getStateFunc $ pureState s Prelude.id <<**>> u) (getStateFunc u) (stateApplicativeLawIdentityLemma u)

stateApplicativeLawHomomorphism : (s : Type) -> (x : a) -> (func : a -> b) ->
                                  (pureState s func <<**>> pureState s x) `StateEq` (pureState s (func x))
stateApplicativeLawHomomorphism s x func = stateEq $ funcEqType (getStateFunc $ pureState s func <<**>> pureState s x)
                                                                (getStateFunc $ pureState s (func x))
                                                                (\z => Refl)

mapFirstAppLemma : (f : (a -> b, s)) -> (x : a) -> (fst f x, snd f) = mapFirst ($ x) f
mapFirstAppLemma (func, state) x = Refl

stateApplicativeLawInterchangeLemma : (f : (s -> (a -> b, s))) -> (x : a) -> (state : s) -> (fst (f state) x, snd (f state)) = mapFirst ($ x) (f state)
stateApplicativeLawInterchangeLemma f x state = rewrite mapFirstAppLemma (f state) x in Refl

stateApplicativeLawInterchange : (s : Type) -> (u : State s (a -> b)) -> (x : a) ->
                                 (u <<**>> pureState s x) `StateEq` (pureState s ($ x) <<**>> u)
stateApplicativeLawInterchange s (stateFunc f) x = stateEq $ funcEqType (getStateFunc $ (stateFunc f) <<**>> pureState s x)
                                                                   (getStateFunc $ pureState s ($ x) <<**>> (stateFunc f))
                                                                   (stateApplicativeLawInterchangeLemma f x)

composeStateFunc : (u : State s (b -> c)) -> (v : State s (a -> b)) -> State s (a -> c)
composeStateFunc (stateFunc f) (stateFunc g) = stateFunc h
  where
    h : s -> ((a -> c), s)
    h s = let p = (f s)
              q = g (snd p)
           in (fst p . fst q, snd q)

-- proof of Applicative is incomplete
(s : Type) => MyApplicative (State s) where
  myPure = pureState s
  (<<*>>) = (<<**>>)

  applicativeLawIdentity = stateApplicativeLawIdentity s
  applicativeLawHomomorphism = stateApplicativeLawHomomorphism s
  applicativeLawInterchange = stateApplicativeLawInterchange s
  applicativeLawComposition = ?stateApplicativeLawComposition

-- Monad

infixl 1 >>>==

(>>>==) : (n : State s a) -> (f : a -> State s b) -> State s b
(>>>==) (stateFunc g) f = stateFunc (\state => let x = g state in getStateFunc (f $ fst x) (snd x))

stateReturn : (x : a) -> State s a
stateReturn x = stateFunc (\state => (x, state))

stateMonadLawIdentityLeft : (x : a) -> (f : a -> State s b) -> (stateReturn x >>>== f) `equalsTo` (f x)
stateMonadLawIdentityLeft x f = stateEq $ funcEqType (getStateFunc $ stateReturn x >>>== f) (getStateFunc (f x)) (\z => Refl)

stateMonadLawIdentityRightLemma2 : (z : (a, s)) -> (fst z, snd z) = z
stateMonadLawIdentityRightLemma2 (x, y) = Refl

stateMonadLawIdentityRightLemma : (f : (s -> (a, s))) -> (x : s) -> (fst (f x), snd (f x)) = f x
stateMonadLawIdentityRightLemma f x = stateMonadLawIdentityRightLemma2 (f x)

stateMonadLawIdentityRight : (n : State s a) -> (n >>>== (\x => stateFunc \state => (x, state))) `equalsTo` n
stateMonadLawIdentityRight (stateFunc f) = stateEq $ funcEqType (\state => (fst (f state), snd (f state)))
                                                                f
                                                                (stateMonadLawIdentityRightLemma f)

stateMonadLawCompositionLemma3 : (z : State s b) -> (y : s)  -> (g : (b -> State s c)) -> getStateFunc (g (fst (getStateFunc z y))) (snd (getStateFunc z y)) = getStateFunc (z >>>== g) y
stateMonadLawCompositionLemma3 (stateFunc f) y g = Refl

stateMonadLawCompositionLemma2 : (result : (a, s)) -> (g : (b -> State s c)) -> (f : (a -> State s b)) -> getStateFunc (g (fst (getStateFunc (f (fst result)) (snd result)))) (snd (getStateFunc (f (fst result)) (snd result))) = getStateFunc (f (fst result) >>>== g) (snd result)
stateMonadLawCompositionLemma2 (x, y) g f = stateMonadLawCompositionLemma3 (f x) y g

stateMonadLawCompositionLemma : (e : (s -> (a, s))) -> (g : (b -> State s c)) -> (f : (a -> State s b)) -> (x : s) -> getStateFunc (g (fst (getStateFunc (f (fst (e x))) (snd (e x))))) (snd (getStateFunc (f (fst (e x))) (snd (e x)))) = getStateFunc (f (fst (e x)) >>>== g) (snd (e x))
stateMonadLawCompositionLemma e g f x = stateMonadLawCompositionLemma2 (e x) g f

stateMonadLawComposition : (n : State s a) -> (f : a -> State s b) -> (g : b -> State s c) ->
                           ((n >>>== f) >>>== g) `equalsTo` (n >>>== \x => f x >>>== g)
stateMonadLawComposition (stateFunc e) f g = stateEq $ funcEqType (getStateFunc $ (stateFunc e >>>== f) >>>== g)
                                                                  (getStateFunc $ stateFunc e >>>== \x => f x >>>== g)
                                                                  (stateMonadLawCompositionLemma e g f)

(s : Type) => MyMonad (State s) where
  myReturn = stateReturn
  (>>>=) = (>>>==)
  monadLawIdentityLeft = stateMonadLawIdentityLeft
  monadLawIdentityRight = stateMonadLawIdentityRight
  monadLawComposition = stateMonadLawComposition

max_stars_repo_name: yutaro-sakamoto/prove-monad

max_issues_repo_name: yutaro-sakamoto/prove-monad

max_forks_repo_name: yutaro-sakamoto/prove-monad


text:
||| A Reversed List
module Data.SnocList

import Decidable.Equality
import Data.List

%default total

infixl 7 <><
infixr 6 <>>

||| 'fish': Action of lists on snoc-lists
public export
(<><) : SnocList a -> List a -> SnocList a
sx <>< [] = sx
sx <>< (x :: xs) = sx :< x <>< xs

||| 'chips': Action of snoc-lists on lists
public export
(<>>) : SnocList a -> List a -> List a
Lin       <>> xs = xs
(sx :< x) <>> xs = sx <>> x :: xs

Cast (SnocList a) (List a) where
  cast sx = sx <>> []

Cast (List a) (SnocList a) where
  cast xs = Lin <>< xs

||| Transform to a list but keeping the contents in the spine order (term depth).
public export
asList : SnocList type -> List type
asList = (reverse . cast)

public export
Eq a => Eq (SnocList a) where
  (==) Lin Lin = True
  (==) (sx :< x) (sy :< y) = x == y && sx == sy
  (==) _ _ = False

public export
Ord a => Ord (SnocList a) where
  compare Lin Lin = EQ
  compare Lin (sx :< x) = LT
  compare (sx :< x) Lin = GT
  compare (sx :< x) (sy :< y)
    = case compare sx sy of
        EQ => compare x y
        c  => c

||| True iff input is Lin
public export
isLin : SnocList a -> Bool
isLin Lin = True
isLin (sx :< x) = False

||| True iff input is (:<)
public export
isSnoc : SnocList a -> Bool
isSnoc Lin     = False
isSnoc (sx :< x) = True

public export
(++) : (sx, sy : SnocList a) -> SnocList a
(++) sx Lin = sx
(++) sx (sy :< y) = (sx ++ sy) :< y

public export
length : SnocList a -> Nat
length Lin = Z
length (sx :< x) = length sx + 1

export
Show a => Show (SnocList a) where
  show xs = "[< " ++ show' "" xs ++ "]"
    where
      show' : String -> SnocList a -> String
      show' acc Lin       = acc
      show' acc (Lin :< x)= show x ++ acc
      show' acc (xs :< x) = show' (", " ++ show x ++ acc) xs

public export
Functor SnocList where
  map f Lin = Lin
  map f (sx :< x) = (map f sx) :< (f x)

public export
Semigroup (SnocList a) where
  (<+>) = (++)

public export
Monoid (SnocList a) where
  neutral = Lin

||| Check if something is a member of a list using the default Boolean equality.
public export
elem : Eq a => a -> SnocList a -> Bool
elem x Lin = False
elem x (sx :< y) = x == y || elem x sx

ext: idr

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
||| Implements verified regular expressions.
|||
||| Implementation is based on https://www.ccs.neu.edu/home/turon/re-deriv.pdf
module RegExp

import Data.List
import Decidable.Equality

import RegExp.Equivalences
import public RegExp.Types

||| Given a regular expression `r` and a string `xs`, determines whether `r` _matches_ `[]` (i.e.
||| whether empty is in the language of `r`).
matchEmpty : (r : RegExp a) -> Dec (Matches r [])
matchEmpty Null = No absurd
matchEmpty Empty = Yes InEmpty
matchEmpty (Lit x) = No absurd
matchEmpty (Cat r s) = case (matchEmpty r, matchEmpty s) of
                            (Yes pr, Yes ps) => Yes $ InCat Refl pr ps
                            (No contra, _)   => No  $ contra . fst . catNotEmpty
                            (_, No contra)   => No  $ contra . snd . catNotEmpty
matchEmpty (Disj r s) = case (matchEmpty r, matchEmpty s) of
                             (Yes p, _)               => Yes $ InDisjL p
                             (_, Yes p)               => Yes $ InDisjR p
                             (No contraR, No contraS) => No  $ absurd . either contraR contraS . disjNotEmpty
matchEmpty (Conj r s) = case (matchEmpty r, matchEmpty s) of
                             (Yes pr, Yes ps) => Yes $ InConj pr ps
                             (No contra, _)   => No  $ contra . fst . conjNotEmpty
                             (_, No contra)   => No  $ contra . snd . conjNotEmpty
matchEmpty (Star r) = Yes InStarZ

||| Computes the derivative of a regular expression `r` with respect to a symbol `x`.
derive : (DecEq a) => (r : RegExp a) -> (x : a) -> RegExp a
derive Null _ = Null
derive Empty _ = Null
derive (Lit y) x with (decEq y x)
  derive (Lit x) x | (Yes Refl) = Empty
  derive (Lit y) x | (No _)     = Null
derive (Cat r s) x with (matchEmpty r)
  derive (Cat r s) x | (Yes _) = normDisj (normCat (derive r x) s) (derive s x)
  derive (Cat r s) x | (No _) = normCat (derive r x) s
derive (Disj r s) x = normDisj (derive r x) (derive s x)
derive (Conj r s) x = normConj (derive r x) (derive s x)
derive (Star r) x = normCat (derive r x) (Star r)

||| Proof that the derivation-based match algorithm is sound
derive_isSound : DecEq a =>
                 {r : RegExp a} ->
                 {x : a} ->
                 {xs : List a} ->
                 Matches (derive r x) xs ->
                 Matches r (x::xs)
derive_isSound {r=Null}  _ impossible
derive_isSound {r=Empty} _ impossible
derive_isSound {r=(Lit y)} {x} p with (decEq y x)
  derive_isSound {r=(Lit x)} {x} p | (Yes Refl) = rewrite emptyMatch_implies_emptyList p in InLit
  derive_isSound {r=(Lit y)} {x} p | (No _)     = absurd p
derive_isSound {r=(Cat r s)} {x} p with (matchEmpty r)
  derive_isSound {r=(Cat r s)} {x} p | (Yes pEmpty) with (normDisj_isSound p)
    derive_isSound {r=(Cat r s)} {x} p | (Yes pEmpty) | (InDisjL t) with (normCat_isSound t)
      derive_isSound {r=(Cat r s)} {x} p | (Yes pEmpty) | (InDisjL t) | (InCat pCat u v) = rewrite pCat in InCat Refl (derive_isSound u) v
    derive_isSound {r=(Cat r s)} {x} p | (Yes pEmpty) | (InDisjR t) = InCat Refl pEmpty (derive_isSound t)
  derive_isSound {r=(Cat r s)} {x} p | (No contra) with (normCat_isSound p)
    derive_isSound {r=(Cat r s)} {x} p | (No contra) | (InCat prf t u) = InCat (cong (x::) prf) (derive_isSound t) u
derive_isSound {r=(Disj r s)}  p with (normDisj_isSound p)
  derive_isSound {r=(Disj r s)} p | (InDisjL pr) = InDisjL $ derive_isSound pr
  derive_isSound {r=(Disj r s)} p | (InDisjR ps) = InDisjR $ derive_isSound ps
derive_isSound {r=(Conj r s)} p with (normConj_isSound p)
  derive_isSound {r=(Conj r s)} p | (InConj pr ps) = InConj (derive_isSound pr) (derive_isSound ps)
derive_isSound {r=(Star r)} p with (normCat_isSound {s=(Star r)} p)
  derive_isSound {r=(Star r)} p | (InCat prf pr prs) = rewrite prf in InStarS (cong (x::) prf) (derive_isSound pr) prs

mutual
  ||| Proof that the derivation-based match algorithm is complete for `Star`
  deriveStar_isComplete : DecEq a =>
                          {r: RegExp a} ->
                          {xs' : List a} ->
                          (x : a) ->
                          (xs : List a) ->
                          xs = x :: xs' ->
                          Matches (Star r) xs ->
                          Matches (normCat (derive r x) (Star r)) xs'
  deriveStar_isComplete _ [] p _ = absurd p
  deriveStar_isComplete {xs'} x _ p (InStarS {xs=[]} {ys} Refl pr ps) =
    deriveStar_isComplete x ys p ps
  deriveStar_isComplete x _ p (InStarS {xs=y::ys} pCat pr ps) =
    let (Refl, Refl) = consInjective p in
        normCat_isComplete $ InCat Refl (derive_isComplete pr) ps

  ||| Proof that the derivation-based match algorithm is complete
  derive_isComplete : DecEq a =>
                      {r : RegExp a} ->
                      {x : a} ->
                      {xs : List a} ->
                      Matches r (x::xs) ->
                      Matches (derive r x) xs
  derive_isComplete {r=Null}       p               = absurd p
  derive_isComplete {r=Empty}      p               = absurd p
  derive_isComplete {r=(Lit y)}    p with (decEq y x)
    derive_isComplete {r=(Lit x)} p | (Yes Refl)  = rewrite litMatchesCons_implies_restEmpty p in InEmpty
    derive_isComplete {r=(Lit y)} p | (No contra) = absurd $ contra $ litMatches_implies_headEqual p
  derive_isComplete {r=(Cat r s)} {x} {xs} p with (matchEmpty r)
    derive_isComplete {r=(Cat r s)} {x} {xs}         (InCat {xs=[]}    {ys=x::xs} Refl pr ps) | (Yes pEmpty) =
      normDisj_isComplete $ InDisjR $ derive_isComplete ps
    derive_isComplete {r=(Cat r s)} {x} {xs=xs++ys'} (InCat {xs=x::xs} {ys=ys'}   Refl pr ps) | (Yes pEmpty) =
      normDisj_isComplete $ InDisjL $ normCat_isComplete $ InCat Refl (derive_isComplete pr) ps
    derive_isComplete {r=(Cat r s)} {x} {xs}         (InCat {xs=[]}    {ys=x::xs} Refl pr ps) | (No contra)  =
      normCat_isComplete $ absurd $ contra pr
    derive_isComplete {r=(Cat r s)} {x} {xs=xs++ys'} (InCat {xs=x::xs} {ys=ys'}   Refl pr ps) | (No contra)  =
      normCat_isComplete $ InCat Refl (derive_isComplete pr) ps
  derive_isComplete {r=(Disj r s)} (InDisjL p) =
    normDisj_isComplete $ InDisjL $ derive_isComplete p
  derive_isComplete {r=(Disj r s)} (InDisjR p) =
    normDisj_isComplete $ InDisjR $ derive_isComplete p
  derive_isComplete {r=(Conj r s)} (InConj pr ps) =
    normConj_isComplete $ InConj (derive_isComplete pr) (derive_isComplete ps)
  derive_isComplete {r=(Star r)} {x} {xs} p = deriveStar_isComplete x (x::xs) Refl p

||| Given a regular expression `r` and a string `xs`, determines whether `r` _matches_ `u` (i.e.
||| whether `xs` is in the language of `r`).
export
matches : DecEq a => (r : RegExp a) -> (xs : List a) -> Dec (Matches r xs)
matches r [] = matchEmpty r
matches r (x::xs) =
  case matches (derive r x) xs of
    Yes prf => Yes $ derive_isSound prf
    No contra => No $ contra . derive_isComplete

max_stars_repo_name: polendri/idris-regex

max_issues_repo_name: polendri/idris-regex

max_forks_repo_name: polendri/idris-regexp


text:
-- ----------------------------------------------------------- [ Component.idr ]
-- Module      : UML.Component
-- Description : Component diagrams.
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module UML.Component

import public UML.Component.Model
import public UML.Component.Parser
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-uml

max_issues_repo_name: jfdm/idris-uml

max_forks_repo_name: jfdm/idris-uml


text:
module LuaGen

import Compiler.Common
import Compiler.CompileExpr

import Core.Context
import Core.Directory

import Libraries.Utils.Hex
import Libraries.Utils.Path

import Idris.Driver

import Data.Buffer
import Data.List
import Data.List1
import Data.Maybe
import Data.SortedMap
import Data.SortedSet
import Data.String.Extra
import Data.String
import Data.Vect

import Debug.Trace

import System
import System.Clock
import System.File

import LuaCommon
import OrderDefs
import LuaAst

data Stack : Type where
data Preamble : Type where
data LuaCode : Type where

logTopic : String
logTopic = "idris2-lua"

data WithDefault : (0 a : Type) -> Maybe a -> Type where
   MkWithDefault : {0 a : Type} -> (x : a) -> (mbdef : Maybe a) -> WithDefault a mbdef

namespace WithDefault
   export
   get : WithDefault a mba -> a
   get (MkWithDefault x _) = x

   export
   getDefault : {x : a} -> WithDefault a (Just x) -> a
   getDefault _ = x

   export
   thisOrDefault : {def : a} -> (Maybe a) -> WithDefault a (Just def)
   thisOrDefault (Just this) = MkWithDefault this _
   thisOrDefault Nothing = MkWithDefault def _

public export
record COpts where
   constructor MkCOptsInfo
   storeConstructorName : WithDefault Bool (Just False)  --StoreConsName
   dynamicSupportLib    : WithDefault Bool (Just True)   --DynSupport
   luaVersion           : WithDefault LuaVersion Nothing --LuaVersion
   noRequire            : WithDefault Bool (Just False)  --NoRequire
   debugOutput          : WithDefault Bool (Just False)  --DebugOutput
   omitEntryCall        : WithDefault Bool (Just False)  --OmitEntryCall
                    --omit 'require' statements in the header of the support script
                    --useful when you want to run idris in environment where not all libraries
                    --are supported or dynamic library loading is turned off
                    --as an example you can use Idris do develop for iOS or android using third party tools

--TODO local const table with integer indices of function values for faster calls
--TODO use <const> when targeting lua 5.4 ? (should enable declaration of 200+ local functions which is
--impossible for mutable local varibles (due to lua's own limitation)
--TODO use strings as backend for Int type in lua 5.1 and 5.2 as in these versions maximum integer precision is 52 bits
--even 48bits if you are to use Buffers

export
logLine :
     {auto opts : COpts}
   -> Lazy String
   -> Core ()
logLine str with (opts |> debugOutput |> get)
   logLine str | True = coreLift $ putStrLn ("[Debug] " ++ str)
   logLine str | False = pure ()

export
toMillis : Clock type -> Integer
toMillis (MkClock sec nan) =
   let scale = 1000 in
       scale * sec + (nan `div` 1000000)

export
showMillis : Integer -> String
showMillis n = show n ++ " ms"

%hide Core.TT.Visibility

stringifyVisibility : Visibility -> String
stringifyVisibility Global = ""
stringifyVisibility Local = "local"

|||As lua does not support general expressions with return values
|||We can emulate this with code blocks and local variables
|||Instead of returning a code block we assign its return value to a local variable
|||And pass both along the compilation pipeline
|||Code blocks build up until the pipeline reaches back any function definition
|||Stockpiled block then gets pasted into the body of that nearest containing function
LuaBlock : Type
LuaBlock = (LuaExpr {-Block (may be empty)-}, LuaExpr {-Expr representing the return value of that block-})

mkErrorAst : String -> LuaExpr
mkErrorAst str =
   LApp (LGVar (UN (Basic "error"))) [LString str]

mkCrashAst : LuaExpr -> LuaExpr
mkCrashAst crash =
    LApp (LLambda [] (    LApp (LGVar (UN (Basic "print")))
                               [LPrimFn StrAppend [LString "ERROR: ", crash]]
                      <+> LApp (LGVar (UN (Basic "os.exit"))) [LNumber "1"])) []

luaNull : LuaExpr
luaNull = LGVar (UN (Basic "null"))

stringifyNameGlobal : Name -> String
stringifyNameGlobal (NS ns n) = (show ns) ++ "." ++ stringifyNameGlobal n
stringifyNameGlobal (UN x) = displayUserName x
stringifyNameGlobal (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
stringifyNameGlobal (PV n d) = "{P:" ++ stringifyNameGlobal n ++ ":" ++ show d ++ "}"
stringifyNameGlobal (DN _ n) = stringifyNameGlobal n
stringifyNameGlobal (Nested (outer, idx) inner)
    = show outer ++ ":" ++ show idx ++ ":" ++ stringifyNameGlobal inner
stringifyNameGlobal (CaseBlock outer i) = "case[" ++ show i ++ "]" ++ outer
stringifyNameGlobal (WithBlock outer i) = "with[" ++ show i ++ "]" ++ outer
stringifyNameGlobal (Resolved x) = "$resolved" ++ show x

stringifyNameMangle : Name -> String
stringifyNameMangle (NS ns n) = (validateIdentifier $ show ns) ++ "_" ++ stringifyNameMangle n
stringifyNameMangle (UN x) = validateIdentifier (displayUserName x)
stringifyNameMangle (MN x y) = "__" ++ (validateIdentifier x) ++ show y
stringifyNameMangle (PV n d) = "pat__" ++ stringifyNameMangle n ++ "_" ++ show d
stringifyNameMangle (DN _ n) = stringifyNameMangle n
stringifyNameMangle (Nested (outer, idx) inner)
    = "n__" ++ show outer ++ "_" ++ show idx ++ "_" ++ stringifyNameMangle inner
stringifyNameMangle (CaseBlock outer i) = "case__" ++ (validateIdentifier outer) ++ "_" ++ show i
stringifyNameMangle (WithBlock outer i) = "with__" ++ (validateIdentifier outer) ++ "_" ++ show i
stringifyNameMangle (Resolved x) = "res__" ++ show x

stringifyName : Visibility -> Name -> String
stringifyName Local name = stringifyNameMangle name
stringifyName Global name = "idris[" ++ show (stringifyNameGlobal name) ++ "]"

mutual
  stringifyBinOp : Nat -> String -> LuaExpr -> LuaExpr -> DeferredStr
  stringifyBinOp n op x y = [stringify n x
                            , " "
                            , op
                            , " "
                            ,stringify (S n) y]

  stringifyMethodApp : Nat -> String -> LuaExpr -> LuaExpr -> DeferredStr
  stringifyMethodApp n method x y = [stringify n x
                                    , ":", method
                                    , "("
                                    ,stringify (1 + n) y
                                    , ")"]

  stringifyFnApp :
     Nat
   -> (fn : String)
   -> Vect n LuaExpr
   -> DeferredStr
  stringifyFnApp n fn args =
    [ fn
    , "("
    ,sepBy (stringify (1 + n) <$> args |> toList) ", "
    , ""
    , ")"]

  --TODO add compiler option to throw when it encounters unsupported ops
  opNotSupportedErr : {auto copts : COpts} -> String -> String
  opNotSupportedErr op = "error(\"[Idris2] Operation not supported: '" ++ op ++ "'\")"

  stringifyBitOp : {auto copts : COpts}
     -> Nat
     -> PrimFn n
     -> Vect n LuaExpr
     -> LuaVersion
     -> DeferredStr
  stringifyBitOp n (ShiftL IntType) [x, y] ver with (ver >= Lua53)
     stringifyBitOp n (ShiftL IntType) [x, y] ver | True = stringifyBinOp n "<<" x y
     stringifyBitOp n (ShiftL IntType) [x, y] ver | False = stringifyFnApp n "bit32.lshift" [x, y]
  stringifyBitOp n (ShiftR IntType) [x, y] ver with (ver >= Lua53)
     stringifyBitOp n (ShiftR IntType) [x, y] ver | True = stringifyBinOp n ">>" x y
     stringifyBitOp n (ShiftR IntType) [x, y] ver | False = stringifyFnApp n "bit32.rshift" [x, y]
  stringifyBitOp n (BAnd IntType) [x, y] ver with (ver >= Lua53)
     stringifyBitOp n (BAnd IntType) [x, y] ver | True = stringifyBinOp n "&" x y
     stringifyBitOp n (BAnd IntType) [x, y] ver | False = stringifyFnApp n "bit32.band" [x, y]
  stringifyBitOp n (BOr IntType) [x, y] ver with (ver >= Lua53)
     stringifyBitOp n (BOr IntType) [x, y] ver | True = stringifyBinOp n "|" x y
     stringifyBitOp n (BOr IntType) [x, y] ver | False = stringifyFnApp n "bit32.bor" [x, y]
  stringifyBitOp n (BXOr IntType) [x, y] ver with (ver >= Lua53)
     stringifyBitOp n (BXOr IntType) [x, y] ver | True = stringifyBinOp n "~" x y
     stringifyBitOp n (BXOr IntType) [x, y] ver | False = stringifyFnApp n "bit32.bxor" [x, y]
  stringifyBitOp n (ShiftL IntegerType) [x, y] ver
     = stringifyMethodApp n "shiftleft" x (LPrimFn (Cast IntegerType IntType) [y]) --bigint shifts are only implemented
                                                                                --for 'Int' shift widths

  stringifyBitOp n (ShiftR IntegerType) [x, y] ver
     = stringifyMethodApp n "shiftright" x (LPrimFn (Cast IntegerType IntType) [y]) --bigint shifts are only implemented
                                                                                --for 'Int' shift widths

  stringifyBitOp n (BAnd IntegerType) [x, y] ver = stringifyFnApp n "idris.bandbi" [x, y]
  stringifyBitOp n (BOr IntegerType) [x, y] ver = stringifyFnApp n "idris.borbi" [x, y]
  stringifyBitOp n (BXOr IntegerType) [x, y] ver = stringifyFnApp n "idris.bxorbi" [x, y]
  stringifyBitOp n op _ _ = [opNotSupportedErr (show op)]

  stringifyString : String -> String --this way we do not rely on specific escape patterns of the compiler backend
  stringifyString str =
    let vstr = show str in --unpack is necessary as function stack size is very limited in lua
        fromMaybe ("utf8.char(idris.unpack({" ++ join ", " (show . ord <$> unpack str) ++ "})) --[[ " ++ trimQuotes vstr ++ "--]]")
                  ((\str => fastConcat ["\"", str, "\""]) <$> escapeStringLua str) -- Try to escape simple ascii strings,
                                                                        -- otherwise fall back to `unpack`
                  -- TODO lua 5.3 supports unicode escape sequences, use them

  data AppPrec = Lower | Higher
  appPrec : LuaExpr -> AppPrec
  appPrec (LLVar x) = Higher
  appPrec (LGVar x) = Higher
  appPrec (LLambda xs x) = Lower
  appPrec (LApp x xs) = Higher
  appPrec (LPrimFn x xs) = Lower
  appPrec LTrue = Higher
  appPrec LFalse = Higher
  appPrec LNil = Higher
  appPrec (LNumber x) = Higher
  appPrec (LBigInt x) = Higher
  appPrec (LString x) = Higher
  appPrec (LTable xs) = Lower
  appPrec (LIndex x y) = Higher
  appPrec (LSeq x y) = Lower
  appPrec (LReturn x) = Lower
  appPrec (LAssign x y z) = Lower
  appPrec (LDeclVar x y) = Lower
  appPrec (LIfThenElse x y z) = Lower
  appPrec LBreak = Lower
  appPrec (LWhile x y) = Lower
  appPrec LDoNothing = Lower
  appPrec (LComment x) = Lower

  stringify :
        {auto copts : COpts}
     -> (n : Nat)
     -> LuaExpr
     -> DeferredStr
  stringify _ (LLVar name) =
    [stringifyName Local name]
  stringify _ (LGVar name) =
    [stringifyName Global name]
  stringify _ (LDeclVar Local name) =
    [stringifyVisibility Local, " ", stringifyName Local name]
  stringify n (LDeclVar Global name) =
    [stringifyVisibility Global, stringifyName Global name]
  stringify n (LLambda args body) =
    [ "function("
    , sepBy (pure . stringifyName Local <$> args) ", "
    , ")\n"
    , indent (S n)
    , stringify (S n) body , "\n"
    , indent n
    , "end" ]
  stringify n (LApp f xs) =
    case appPrec f of
      Lower =>
        [ "("
        , stringify n f
        , ")("
        , sepBy (stringify n <$> xs) ","
        , ")"]
      Higher =>
        [ stringify n f
        , "("
        , sepBy (stringify n <$> xs) ","
        , ")" ]
  stringify _ LNil = ["nil"]
  stringify _ LFalse = ["false"]
  stringify _ LTrue = ["true"]
  stringify _ (LNumber num) = [num]
  stringify _ (LBigInt num) = ["bigint:new(" , "\"" , num , "\"" , ")" ]
  stringify _ (LString s) = [stringifyString s]
  stringify _ (LComment s) = ["--[[ ",  s, " --]]"]
  stringify _ (LTable []) = ["{}"]
  stringify n (LTable kvs@(_ :: _)) =
    [ "{\n"
    , sepBy ((\(k, v) =>
            let general = [indent (1 + n), "[", stringify (1 + n) k, "]", " = \n", indent (2 + n), stringify (2 + n) v] in
                case k of
                     LDoNothing => [indent (1 + n), stringify (1 + n) v]
                     (LString str) => let chars = unpack str in
                        case ((\c => c == '_' || isAlpha c)
                              <$> chars |> head' `orElse` False)
                             && forAll (\x => isAlphaNum x || x == '_') chars of --TODO properly look into what lua allows here
                             True => [indent (1 + n), str, " = \n", indent (2 + n), stringify (2 + n) v]                           --lua can do
                             False => general
                     (LNumber num) => [indent (1 + n), show num, " = \n", indent (2 + n), stringify (2 + n) v]                     --better at optimising these
                     _ => general
            ) <$> kvs)
            ",\n"
    , "\n"
    , indent n
    , "}" ]
  stringify n (LIndex e i) =
    [ stringify n e
    , "["
    , the DeferredStr
       $ let general = stringify (1 + n) i in
          case i of
               (LString str) => let chars = unpack str in
                                    if ((\c => c == '_' || isAlpha c)
                                        <$> chars |> head' `orElse` False)
                                       && forAll (\x => isAlphaNum x || x == '_') chars
                                       then
                                          [show str]
                                       else
                                          general
               _ => general
    , "]" ]
  stringify n (LSeq x y) = [stringify n x , "\n" , indent n, stringify n y]
  stringify n (LReturn x) = ["return " , stringify (1 + n) x]
  stringify n (LAssign (Just vis) x y) =
    [ stringifyVisibility vis
    , if vis == Local then " " else ""
    , stringify n x
    , " = "
    , stringify n y
    ]
  stringify n (LAssign Nothing x y) =
    [stringify n x , " = " , stringify n y]
  stringify n (LIfThenElse cond x y) =
    [ "if "
    , stringify (1 + n) cond
    , " then\n"
    , indent (1 + n), stringify (1 + n) x , "\n"
    , indent n
    , "else\n"
    , indent (1 + n), stringify (1 + n) y
    , "\n"
    , indent n
    , "end" ]
  stringify _ LBreak = ["break"]
  stringify n (LWhile cond body) =
    [ "while "
    , stringify (1 + n) cond
    , " do\n"
    , indent (1 + n), stringify (1 + n) body
    , "\n"
    , indent n
    , "end" ]
  stringify _ LDoNothing = [""]
  stringify n (LPrimFn (Add ty) [x, y]) = stringifyBinOp n "+" x y
  stringify n (LPrimFn (Sub ty) [x, y]) = stringifyBinOp n "-" x y
  stringify n (LPrimFn (Mul ty) [x, y]) = stringifyBinOp n "*" x y
  stringify n (LPrimFn (Div IntType) [x, y]) with (copts |> luaVersion |> get >= Lua53)
     stringify n (LPrimFn (Div IntType) [x, y]) | True
       = stringifyBinOp n "//" x y
     stringify n (LPrimFn (Div IntType) [x, y]) | False
       = stringifyFnApp n "idris.div" [x, y]
  stringify n (LPrimFn (Div IntegerType) [x, y]) = stringifyBinOp n "/" x y
  stringify n (LPrimFn (Div DoubleType) [x, y]) = stringifyBinOp n "/" x y
  stringify n (LPrimFn (Mod ty) [x ,y]) = stringifyBinOp n "%" x y
  stringify n (LPrimFn (Neg ty) [x]) = ["- (", stringify n x, ")"]
  stringify n (LPrimFn op@(ShiftL _) args) = stringifyBitOp n op args (copts |> luaVersion |> get)
  stringify n (LPrimFn op@(ShiftR _) args) = stringifyBitOp n op args (copts |> luaVersion |> get)
  stringify n (LPrimFn op@(BAnd _) args)   = stringifyBitOp n op args (copts |> luaVersion |> get)
  stringify n (LPrimFn op@(BOr _) args)    = stringifyBitOp n op args (copts |> luaVersion |> get)
  stringify n (LPrimFn op@(BXOr _) args)   = stringifyBitOp n op args (copts |> luaVersion |> get)
  stringify n (LPrimFn (LT ty) [x, y]) = stringifyBinOp (S n) "<" x y
  stringify n (LPrimFn (LTE ty) [x, y]) = stringifyBinOp (S n) "<=" x y
  stringify n (LPrimFn (EQ ty) [x, y]) = stringifyBinOp (S n) "==" x y
  stringify n (LPrimFn (GTE ty) [x, y]) = stringifyBinOp (S n) ">=" x y
  stringify n (LPrimFn (GT ty) [x, y]) = stringifyBinOp (S n) ">" x y
  stringify n (LPrimFn StrLength [x]) = ["utf8.len(" , stringify (1 + n) x , ")"]
  stringify n (LPrimFn StrHead [x]) = ["utf8.sub(" , stringify (1 + n) x , ", 1, 1)"]
  stringify n (LPrimFn StrTail [x]) = ["utf8.sub(" , stringify (1 + n) x , ", 2)"]
  stringify n (LPrimFn StrIndex [str, i]) =
      let strI = stringify (1 + n) i in
         [ "utf8.sub("
         , stringify (1 + n) str
         , ", "
         , strI
         , ", "
         , strI
         , ")" ]
  stringify n (LPrimFn StrCons [x, xs]) =
    [ "("
    , stringify (1 + n) x
    , ") .. ("
    , stringify (1 + n) xs
    , ")" ]
  stringify n (LPrimFn StrAppend [x, xs]) =
    [ "(" , stringify (1 + n) x
    , ") .. ("
    , stringify (1 + n) xs
    , ")" ]
  stringify n (LPrimFn StrReverse [x]) = ["(" , stringify (1 + n) x , "):reverse()"]
  stringify n (LPrimFn StrSubstr [offset, len, str]) =
     let strOff = stringify (1 + n) offset in
        ["utf8.sub("
        , stringify (1 + n) str
        , ", "
        , strOff
        , ", "
        , strOff
        , " + ("
        , stringify (1 + n) len
        , ") - 1)" ]
  stringify n (LPrimFn DoubleExp args) = stringifyFnApp n "math.pow" args
  stringify n (LPrimFn DoubleLog args) = stringifyFnApp n "math.log" args
  stringify n (LPrimFn DoubleSin args) = stringifyFnApp n "math.sin" args
  stringify n (LPrimFn DoubleCos args) = stringifyFnApp n "math.cos" args     --TODO create local bindings for math functions
  stringify n (LPrimFn DoubleTan args) = stringifyFnApp n "math.tan" args     -- for faster invokation
  stringify n (LPrimFn DoubleASin args) = stringifyFnApp n "math.asin" args
  stringify n (LPrimFn DoubleACos args) = stringifyFnApp n "math.acos" args
  stringify n (LPrimFn DoubleATan args) = stringifyFnApp n "math.atan" args
  stringify n (LPrimFn DoubleSqrt args) = stringifyFnApp n "math.sqrt" args
  stringify n (LPrimFn DoubleFloor args) = stringifyFnApp n "math.floor" args
  stringify n (LPrimFn DoubleCeiling args) = stringifyFnApp n "math.ceil" args

  stringify n (LPrimFn (Cast StringType IntType) [x]) = stringifyFnApp n "idris.strtointeger" [x] --defined in support
  stringify n (LPrimFn (Cast StringType DoubleType) [x]) = stringifyFnApp n "tonumber" [x]
  stringify n (LPrimFn (Cast StringType IntegerType) [x]) = stringifyFnApp n "bigint:new" [x]

  stringify n (LPrimFn (Cast IntType CharType) [x]) = ["utf8.char(" , stringify (1 + n) x , ")"]
  stringify n (LPrimFn (Cast IntType DoubleType) [x]) = stringify n x
  stringify n (LPrimFn (Cast IntType IntegerType) [x]) = stringifyFnApp n "bigint:new" [x]

  stringify n (LPrimFn (Cast CharType IntegerType) [x]) = ["bigint:new(utf8.byte(" , stringify (1 + n) x , "))"]
  stringify n (LPrimFn (Cast CharType IntType) [x]) = ["utf8.byte(" , stringify (1 + n) x , ")"]

  stringify n (LPrimFn (Cast IntegerType DoubleType) [x]) = stringifyFnApp n "bigint.tonumber" [x]
  stringify n (LPrimFn (Cast IntegerType IntType) [x]) = stringifyFnApp n "bigint.tonumber" [x]
  stringify n (LPrimFn (Cast IntegerType StringType) [x]) = stringifyFnApp n "bigint.tostring" [x]

  stringify n (LPrimFn (Cast DoubleType IntType) [x]) = stringifyFnApp n "math.floor" [x]
  stringify n (LPrimFn (Cast DoubleType IntegerType) [x]) =
    ["bigint:new(math.floor(" , stringify (1 + n) x , "))" ]

  stringify n (LPrimFn (Cast ty StringType) [x]) = stringifyFnApp n "tostring" [x]
  stringify n (LPrimFn (Cast from to) [x]) =
    [ stringify n $ mkErrorAst $ "invalid cast: from " ++ show from ++ " to " ++ show to ]
  stringify n (LPrimFn BelieveMe [_, _, x]) = stringify n x
  stringify n (LPrimFn Crash [_, msg])
   = let ast = mkCrashAst msg in
         [stringify n ast]
  stringify n (LPrimFn op args) = stringify n $ mkErrorAst $ "unsupported primitive function: " ++ show op

record StackFrame where   --each function has its own table that represents its stackframe (function arguments not included)
  constructor MkStackFrame--each inner table has a unique (relative to all outer functions) name
  get : Int               --each table is indexed by consecutive integer values starting from 1 (because lua)
                          --each such value represents one local variable of the innermost function
                          --stack emulation is required to bypass lua's local variable limit which is capped at 200 per function
                          --table indexing is not as fast as register access but that is an unevitable trade-off
                          --and you can still theoretically blow 200 locals limitation calling function with excessive amount of arguments

                          --SO using this method: each function has stack size of 1 + number of arguments + number of let bindings
                          --actually each function has one extra local: '_ENV' but I don't think it counts towards the limit

record StackSt where
  constructor MkStackSt
  stack : List Int
  nextFrame : Int
  nextIndex  : Int --if stack is empty, points to the next free index in current thread

frameLowest : Int
frameLowest = 1

indexLowest : Int
indexLowest = 1

frameName : StackFrame -> Name
frameName (MkStackFrame i) = MN "frame" i

declFrameTable : StackFrame -> Int -> LuaExpr
declFrameTable frame numOfVars =
 if numOfVars > 0 then
       LAssign (Just Local) (LLVar (frameName frame)) (LTable (replicate (integerToNat (cast numOfVars)) (LDoNothing, LNil)))
    else
       LDoNothing

record PreambleSt where
  constructor MkPreambleSt
  preamble : SortedMap String String

pushFrame :
      {auto c : Ref Stack StackSt}
   -> Core StackFrame
pushFrame =
  do
    s <- get Stack
    let frame = nextFrame s
    let index = nextIndex s
    put Stack (record{ nextFrame $= (+1)
                     , nextIndex = indexLowest
                     , stack $= (index ::) } s)
    pure (MkStackFrame frame)

pushLocal :
      {auto c : Ref Stack StackSt}
   -> {auto frame : StackFrame}
   -> Core LuaExpr
pushLocal =
  do
    s <- get Stack
    let i = nextIndex s
    put Stack (record{nextIndex $= (+1)} s)
    pure (LIndex (LLVar (frameName frame)) (LNumber (show i)))

||| Returns the number of local variables in the popped frame
popFrame : {auto c : Ref Stack StackSt} -> Core Int
popFrame =
  do
     s <- get Stack
     let i = nextFrame s
     let v = nextIndex s
     case (i <= frameLowest, stack s) of
          (False, (nextIndex :: other)) => do
             put Stack (record{nextFrame $= (\i => i - 1), nextIndex = nextIndex, stack = other} s)
             pure (v - 1)
          (_, _) => throw (UserError "Attempt to pop from an empty stack")

popName : {auto c : Ref Stack StackSt} -> Core ()
popName =
  do
     s <- get Stack
     let i = nextIndex s
     if i <= indexLowest then
           throw (UserError "attempt to pop from an empty stack frame")
        else
           put Stack (record{nextIndex $= (\i => i - 1)} s)

getPreamble :
           {auto p : Ref Preamble PreambleSt}
        -> Core $ SortedMap String String
getPreamble = do
  x <- get Preamble
  pure x.preamble

addDefToPreamble :
           {auto preamble : Ref Preamble PreambleSt}
        -> String
        -> String
        -> Bool
        -> Core ()
addDefToPreamble name def okIfDefined = do
  do
    s <- getPreamble
    let dname = name
    case lookup dname s of
      Nothing =>
        do
          put Preamble (MkPreambleSt $ insert dname def s)
          pure ()
      Just _ =>
          if not okIfDefined then
               throw $ InternalError $ "Attempt to redefine the preamble definition '" ++ name ++ "'"
             else
               pure ()

constantTy : Constant -> Maybe Constant
constantTy (I _)   = Just IntType
constantTy (BI _)  = Just IntegerType
constantTy (B8 _)  = Just Bits8Type
constantTy (B16 _) = Just Bits16Type
constantTy (B32 _) = Just Bits32Type
constantTy (B64 _) = Just Bits64Type
constantTy (Str _) = Just StringType
constantTy (Ch _)  = Just CharType
constantTy (Db _)  = Just DoubleType
constantTy _       = Nothing

processConstant : Constant -> Core LuaExpr
processConstant (I x) = pure $ LNumber (show x)
processConstant (BI x) = pure $ LBigInt (show x)
processConstant (Str x) = pure $ LString x
processConstant (Ch x) = pure $ LString (String.singleton x)
processConstant (Db x) = pure $ LNumber (show x)
processConstant WorldVal = pure $ LString (show WorldVal)
processConstant c = throw $ InternalError ("Unsupported constant '" ++ (show c) ++ "' detected")

justReturn : LuaExpr -> LuaBlock
justReturn expr = (LDoNothing, expr)

curriedApp : LuaExpr -> List LuaExpr -> LuaExpr
curriedApp head [] = head
curriedApp head (x :: xs) = curriedApp (LApp head [x]) xs

mkCaseImpl :
       {auto stack : Ref Stack StackSt}
    -> {auto frame : StackFrame}
    -> {auto opts : COpts}
    -> (retn : LuaExpr)
    -> (branches : List (LuaBlock {-condition-}, (LuaBlock) {-arm-}))
    -> (mbElse : Maybe LuaBlock)
    -> Core LuaExpr
mkCaseImpl retn (((blockA, cond), (blockB, arm)) :: xs) mbElse = do
  blockC <- mkCaseImpl retn xs mbElse
  let ifBranch = LIfThenElse cond (blockB <+> LAssign Nothing retn arm) blockC
  pure $ blockA <+> ifBranch
mkCaseImpl retn [] (Just (blockA, els)) =
  pure $ blockA <+> LAssign Nothing retn els
mkCaseImpl retn [] Nothing =
  pure $ mkErrorAst "Impossible else branch"

mkCase :
       {auto stack : Ref Stack StackSt}
    -> {auto frame : StackFrame}
    -> {auto opts : COpts}
    -> (branches : List (LuaBlock {-condition-}, (LuaBlock) {-arm-}))
    -> (mbElse : Maybe LuaBlock)
    -> Core LuaBlock
mkCase branches mbElse =
  do
    local <- pushLocal
    blockA <- mkCaseImpl local branches mbElse
    pure (blockA, local)

uninhabNS : Namespace
uninhabNS = preludeNS <.> mkNamespace "Uninhabited"

iorefNS : Namespace
iorefNS = mkNamespace "Data.IORef"

bufferNS : Namespace
bufferNS = mkNamespace "Data.Buffer"

stringsNS : Namespace
stringsNS = mkNamespace "Data.Strings"

strIterNS : Namespace
strIterNS = mkNamespace "Data.String.Iterator"

arrayNS : Namespace
arrayNS = mkNamespace "Data.IOArray.Prims"

systemNS : Namespace
systemNS = mkNamespace "System"

dirNS : Namespace
dirNS = mkNamespace "System.Directory"

infoNS : Namespace
infoNS = mkNamespace "System.Info"

fileNS : Namespace
fileNS = mkNamespace "System.File"

readWriteNS : Namespace
readWriteNS = mkNamespace "System.File.Handle"

handleNS : Namespace
handleNS = mkNamespace "System.File.Handle"

permissionsNS : Namespace
permissionsNS = mkNamespace "System.File.Permissions"

virtualNS : Namespace
virtualNS = mkNamespace "System.File.Virtual"

errorNS : Namespace
errorNS = mkNamespace "System.File.Error"

metaNS : Namespace
metaNS = mkNamespace "System.File.Meta"

processNS : Namespace
processNS = mkNamespace "System.File.Process"

termNS : Namespace
termNS = mkNamespace "Libraries.Utils.Term"

primioNS : Namespace
primioNS = mkNamespace "PrimIO"

extNames : List Name
extNames = [
             mkNamespacedName (Just iorefNS)   (Basic "prim__newIORef")
           , mkNamespacedName (Just iorefNS)   (Basic "prim__readIORef")
           , mkNamespacedName (Just iorefNS)   (Basic "prim__writeIORef")
           , mkNamespacedName (Just arrayNS)   (Basic "prim__newArray")
           , mkNamespacedName (Just arrayNS)   (Basic "prim__arrayGet")
           , mkNamespacedName (Just arrayNS)   (Basic "prim__arraySet")
           , mkNamespacedName (Just infoNS)    (Basic "prim__os")
           , mkNamespacedName (Just infoNS)    (Basic "prim__codegen")
           , mkNamespacedName (Just uninhabNS) (Basic "void")
           , mkNamespacedName (Just ioNS)      (Basic "onCollect")
           , mkNamespacedName (Just ioNS)      (Basic "onCollectAny")
           ]

foreignImpls : List Name
foreignImpls = [
                 ------------- Not Implemented -----------
                 mkNamespacedName (Just $ mkNamespace "Network.FFI") (Basic "prim__idrnet_accept")
               , mkNamespacedName (Just $ mkNamespace "Network.FFI") (Basic "prim__idrnet_bind")
               , mkNamespacedName (Just $ mkNamespace "Network.FFI") (Basic "prim__idrnet_create_sockaddr")
               , mkNamespacedName (Just $ mkNamespace "Network.FFI") (Basic "prim__idrnet_free")
               , mkNamespacedName (Just $ mkNamespace "Network.FFI") (Basic "prim__idrnet_sockaddr_family")
               , mkNamespacedName (Just $ mkNamespace "Network.FFI") (Basic "prim__idrnet_sockaddr_ipv4")
               , mkNamespacedName (Just $ mkNamespace "Network.FFI") (Basic "prim__idrnet_socket")
               , mkNamespacedName (Just $ mkNamespace "Network.FFI") (Basic "prim__socket_listen")

               , mkNamespacedName (Just $ mkNamespace "Network.Socket.Data") (Basic "prim__idrnet_af_inet")
               , mkNamespacedName (Just $ mkNamespace "Network.Socket.Data") (Basic "prim__idrnet_af_inet6")
               , mkNamespacedName (Just $ mkNamespace "Network.Socket.Data") (Basic "prim__idrnet_af_unix")
               , mkNamespacedName (Just $ mkNamespace "Network.Socket.Data") (Basic "prim__idrnet_af_unspec")
               , mkNamespacedName (Just $ mkNamespace "Network.Socket.Data") (Basic "prim__idrnet_errno")

               , mkNamespacedName (Just $ mkNamespace "System.Clock") (Basic "prim__clockTimeGcCpu")
               , mkNamespacedName (Just $ mkNamespace "System.Clock") (Basic "prim__clockTimeGcReal")
               , mkNamespacedName (Just $ mkNamespace "System.Clock") (Basic "prim__clockTimeMonotonic")
               , mkNamespacedName (Just $ mkNamespace "System.Clock") (Basic "prim__clockTimeProcess")
               , mkNamespacedName (Just $ mkNamespace "System.Clock") (Basic "prim__clockTimeThread")
               , mkNamespacedName (Just $ mkNamespace "System.Clock") (Basic "prim__clockTimeUtc")
               , mkNamespacedName (Just $ mkNamespace "System.Clock") (Basic "prim__osClockNanosecond")
               , mkNamespacedName (Just $ mkNamespace "System.Clock") (Basic "prim__osClockSecond")
               , mkNamespacedName (Just $ mkNamespace "System.Clock") (Basic "prim__osClockValid")

               , mkNamespacedName (Just ioNS)     (Basic "prim__fork")
               , mkNamespacedName (Just systemNS) (Basic "prim__setEnv")
               , mkNamespacedName (Just systemNS) (Basic "prim__getEnvPair")
               , mkNamespacedName (Just systemNS) (Basic "prim__unsetEnv")
                 -------------------------------------------

               , mkNamespacedName (Just primioNS) (Basic "prim__nullAnyPtr")
               , mkNamespacedName (Just ioNS) (Basic "prim__putStr")
               , mkNamespacedName (Just ioNS) (Basic "prim__putChar")
               , mkNamespacedName (Just ioNS) (Basic "prim__getStr")
               , mkNamespacedName (Just ioNS) (Basic "prim__getChar")
               , mkNamespacedName (Just ioNS) (Basic "prim__getString")
               , mkNamespacedName (Just processNS) (Basic "prim__flush")
               , mkNamespacedName (Just readWriteNS) (Basic "prim__writeLine")
               , mkNamespacedName (Just readWriteNS) (Basic "prim__readLine")
               , mkNamespacedName (Just readWriteNS) (Basic "prim__readChar")
               , mkNamespacedName (Just readWriteNS) (Basic "prim__readChars")
               , mkNamespacedName (Just readWriteNS) (Basic "prim__eof")
               , mkNamespacedName (Just handleNS) (Basic "prim__open")
               , mkNamespacedName (Just handleNS) (Basic "prim__close")
               , mkNamespacedName (Just processNS) (Basic "prim__popen")
               , mkNamespacedName (Just processNS) (Basic "prim__pclose")
               , mkNamespacedName (Just errorNS) (Basic "prim__error")
               , mkNamespacedName (Just errorNS) (Basic "prim__fileErrno")
               , mkNamespacedName (Just readWriteNS) (Basic "prim__removeFile")
               , mkNamespacedName (Just metaNS) (Basic "prim__fileSize")
               , mkNamespacedName (Just metaNS) (Basic "prim__fPoll")
               , mkNamespacedName (Just metaNS) (Basic "prim__fileModifiedTime")
               , mkNamespacedName (Just metaNS) (Basic "prim__fileStatusTime")
               , mkNamespacedName (Just virtualNS) (Basic "prim__stdin")
               , mkNamespacedName (Just virtualNS) (Basic "prim__stdout")
               , mkNamespacedName (Just virtualNS) (Basic "prim__stderr")
               , mkNamespacedName (Just permissionsNS) (Basic "prim__chmod")
               , mkNamespacedName (Just dirNS) (Basic "prim__changeDir")
               , mkNamespacedName (Just dirNS) (Basic "prim__currentDir")
               , mkNamespacedName (Just dirNS) (Basic "prim__createDir")
               , mkNamespacedName (Just dirNS) (Basic "prim__removeDir")
               , mkNamespacedName (Just dirNS) (Basic "prim__openDir")
               , mkNamespacedName (Just dirNS) (Basic "prim__closeDir")
               , mkNamespacedName (Just dirNS) (Basic "prim__dirEntry")
               , mkNamespacedName (Just systemNS) (Basic "prim__getArgCount")
               , mkNamespacedName (Just systemNS) (Basic "prim__getArg")
               , mkNamespacedName (Just systemNS) (Basic "prim__getEnv")
               , mkNamespacedName (Just systemNS) (Basic "prim__exit")
               , mkNamespacedName (Just systemNS) (Basic "prim__system")
               , mkNamespacedName (Just typesNS) (Basic "fastConcat")
               , mkNamespacedName (Just typesNS) (Basic "fastUnpack")
               , mkNamespacedName (Just typesNS) (Basic "fastPack")
               , mkNamespacedName (Just termNS) (Basic "prim__setupTerm")
               , mkNamespacedName (Just termNS) (Basic "prim__getTermCols")
               , mkNamespacedName (Just termNS) (Basic "prim__getTermLines")
               , mkNamespacedName (Just bufferNS) (Basic "prim__newBuffer")
               , mkNamespacedName (Just bufferNS) (Basic "prim__bufferSize")
               , mkNamespacedName (Just bufferNS) (Basic "prim__setByte")
               , mkNamespacedName (Just bufferNS) (Basic "prim__getByte")
               , mkNamespacedName (Just bufferNS) (Basic "prim__setInt32")
               , mkNamespacedName (Just bufferNS) (Basic "prim__getInt32")
               , mkNamespacedName (Just bufferNS) (Basic "prim__setInt")
               , mkNamespacedName (Just bufferNS) (Basic "prim__getInt")
               , mkNamespacedName (Just bufferNS) (Basic "prim__setDouble")
               , mkNamespacedName (Just bufferNS) (Basic "prim__getDouble")
               , mkNamespacedName (Just bufferNS) (Basic "prim__setString")
               , mkNamespacedName (Just bufferNS) (Basic "prim__getstring")
               , mkNamespacedName (Just bufferNS) (Basic "prim__copyData")
               , mkNamespacedName (Just bufferNS) (Basic "prim__readBufferData")
               , mkNamespacedName (Just bufferNS) (Basic "prim__writeBufferData")
               , mkNamespacedName (Just bufferNS) (Basic "stringByteLength")
               , mkNamespacedName (Just strIterNS) (Basic "fromString")
               , mkNamespacedName (Just strIterNS) (Basic "uncons")
               ]

mutual -- TODO try remove in favour of forward declarions ?

  processCustomExtCall :
         {auto stack : Ref Stack StackSt}
      -> {auto frame : StackFrame}
      -> {auto opts : COpts}
      -> Name
      -> List NamedCExp
      -> Core LuaBlock
  processCustomExtCall name args
   = do (blocks, args) <- unzip <$> traverse processExpr args
        pure $ (concat blocks, curriedApp (LGVar $ name) args)

  --fully applied external name
  --Can be inlined ?? Because it *is* inlined at the moment !
  processExtCall :
         {auto stack : Ref Stack StackSt}
      -> {auto frame : StackFrame}
      -> {auto opts : COpts}
      -> Name
      -> List NamedCExp
      -> Core LuaBlock
  processExtCall name@(NS ns (UN n)) args =
    condC [
            ( pure $ ns == iorefNS
            ,
              case (n, args) of
                   (Basic "prim__newIORef", [_, v, _]) =>
                      do (blockA, v) <- processExpr v
                         pure (blockA, LTable [(LString "val", v)])
                   (Basic "prim__readIORef", [_, r, _]) =>
                      do
                        (blockA, r) <- processExpr r
                        pure (blockA, LIndex r (LString "val"))
                   (Basic "prim__writeIORef", [_, r, v, _]) =>
                      do
                        (blockA, r) <- processExpr r
                        (blockB, v) <- processExpr v
                        pure (blockA <+> blockB <+> LAssign Nothing (LIndex r (LString "val")) v, LTable [(LString "tag", LString "0")] {-Unit-})
                   _ => processCustomExtCall name args )
            ,
            ( pure $ ns == arrayNS
            , case (n, args) of
                   (Basic "prim__newArray", [_, len, init, _]) =>
                      do
                        (blockA, len) <- processExpr len
                        (blockB, init) <- processExpr init
                        table <- pushLocal
                        counter <- pushLocal
                        let loop = LWhile
                                 (LPrimFn (LTE IntType) [counter, len]) $
                                 (LAssign Nothing (LIndex table counter) init)
                                 <+> (LAssign Nothing counter (LPrimFn (Add IntType) [counter, LNumber "1"]))
                        pure (blockA <+> blockB <+> LAssign Nothing table (LTable [])
                              <+> LAssign Nothing counter (LNumber "1") <+> loop, table)
                   (Basic "prim__arrayGet", [_, ar, i, _]) =>
                      do
                        (blockA, ar) <- processExpr ar
                        (blockB, i) <- processExpr i
                        pure (blockA <+> blockB, LIndex ar (LPrimFn (Add IntType) [i, LNumber "1"]))
                   (Basic "prim__arraySet", [_, ar, i, v, _]) =>
                      do
                        (blockA, ar) <- processExpr ar
                        (blockB, i) <- processExpr i
                        (blockC, v) <- processExpr v
                        pure ( blockA
                                <+> blockB
                                <+> blockC
                                <+> LAssign Nothing
                                            (LIndex ar (LPrimFn (Add IntType) [i, LNumber "1"]))
                                            v
                             , LTable [(LString "tag", LString "0")] {-Unit-})
                   _ => processCustomExtCall name args )
             ,
             ( pure $ ns == infoNS
             , case n of
                    Basic "prim__os" =>
                       do
                         args' <- traverse processExpr args
                         let (blockA, args) = unzip args'
                         pure (concat blockA, curriedApp (LGVar name) args) --defined in support file
                    _ => processCustomExtCall name args )
             ,
             ( pure $ ns == infoNS
             , case n of
                    Basic "prim__codegen" =>
                       do
                         args' <- traverse processExpr args
                         let (blockA, args) = unzip args'
                         pure (concat blockA, curriedApp (LGVar name) args) --defined in support file
                    _ => processCustomExtCall name args )
             ,
             ( pure $ ns == uninhabNS
             , case n of
                    Basic "void" =>
                       do
                         args' <- traverse processExpr args
                         let (blockA, args) = unzip args'
                         pure (concat blockA, curriedApp (LGVar name) args) --defined in support file
                    _ => processCustomExtCall name args )
             ,
             ( pure $ ns == ioNS
             , case n of
                    Basic "prim__onCollectAny" =>
                       do
                         args' <- traverse processExpr args
                         let (blockA, args) = unzip args'
                         pure (concat blockA, curriedApp (LGVar name) args) --defined in support file
                    Basic "prim__onCollect" =>
                       do
                         args' <- traverse processExpr args
                         let (blockA, args) = unzip args'
                         pure (concat blockA, curriedApp (LGVar name) args) --defined in support file
                    _ => processCustomExtCall name args) ] (processCustomExtCall name args)
  -- where
  --   notDefined : Core a
  --   notDefined          = throw $ InternalError $ "external primitive not implemented: " ++ show name
  processExtCall name args = processCustomExtCall name args

  readCCPart : String -> (String, String)
  readCCPart x =
    let (cc, def) = break (== ':') x
    in (cc, drop 1 def)

  processRequire : String -> (List (String, String))
  processRequire x = let names = split (== ',') x in
                         flip map (forget names) $
                           \name =>
                             let (h, t) = String.break (== '(') name in
                             case trim (drop 1 t) of
                                  "" => (trim h, trim h)
                                  t => (trim h, trim $ fst $ break (== ')') t)

  searchForeign' : List1 String -> Maybe (String, Maybe (List (String, String))) --def, require statements
  searchForeign' (x:::xs) =
    let (cc, def) = readCCPart x
    in  if cc == "lua"
        then
           let (def, req) = break (== '|') def in
               Just (def, if req == "" then Nothing else Just $ processRequire $ drop 1 req)
        else case xs of
                  (x :: xs) => searchForeign' (x ::: xs)
                  [] => Nothing

  -- If there is only one hint line, prefix 'lua:' can be skipped
  -- If there are multiple, find a line prefixed with 'lua:'
  searchForeign : List String -> Maybe (String, Maybe (List (String, String)))
  searchForeign [] = Nothing
  searchForeign (a :: b :: xs) = searchForeign' (a ::: (b :: xs))
  searchForeign [def] =
    let def = trim def
        def = if isPrefixOf "lua:" def then trim (strSubstr 4 (cast $ length def) def) else def
        (def, req) = break (== '|') def in
        Just (def, if req == "" then Nothing else Just $ processRequire $ drop 1 req)

  doCurryTransform : (def : String) -> (erased : List Nat) -> Maybe String
  doCurryTransform def erased =
    case split (toList1 "=>") (fastUnpack def) of
      argsAll ::: [body] =>
        let args = split (toList1 ",") argsAll
            trimmedArgs = (mapMaybe (filter (/= []) . Just . trim) $ forget args) in
          Just $ fastPack $ curryTransform (addErasedArgs trimmedArgs erased) (trim body)
      _ => Nothing
    where
      addErasedArgs : (args : List (List Char)) -> (erased : List Nat) -> List (List Char)
      addErasedArgs xs (0 :: is) = ['_'] :: addErasedArgs xs (map (`minus` 1) is)
      addErasedArgs (x :: xs) ((S i) :: is) = x :: addErasedArgs xs (i :: map (`minus` 1) is)
      addErasedArgs [] is = replicate (length is) ['_']
      addErasedArgs xs [] = xs

  preprocess : {auto defs : Ref Ctxt Defs} -> (foreignName : Name) -> (def : String) -> Core String
  preprocess name def = pure $ doCurryTransform def !(getErased name) `orElse` def

  processForeignDef :
          {auto defs : Ref Ctxt Defs}
       -> {auto opts : COpts}
       -> {auto preamble : Ref Preamble PreambleSt}
       -> Name
       -> List String
       -> List CFType
       -> CFType
       -> Core ()
  processForeignDef name hints argtys retty =
   case find (== name) foreignImpls of
        Just _ => pure () -- implemented internally
        Nothing =>
           do let ((def, maybeReq), replace)
                  = ((\x => (x, True)) <$> (searchForeign hints)) `orElse` ((stringifyName Global name, Nothing), False)
              def <- preprocess name def
              logLine $ "using %foreign " ++ def
              case maybeReq of
                   (Just packs) => do
                     logLine $ "requiring " ++ (show $ map fst packs)
                     for_ packs $ \pack =>
                       addDefToPreamble ("$" ++ snd pack)
                         ((stringifyName Global (UN $ Basic $ snd pack)) ++ " = require('" ++ fst pack ++ "')")
                          True -- its ok to require the same package multiple times, ignore all but first
                                                                              -- '$' makes sure all require statements
                                                                              -- appear above assignments that use them
                   Nothing => pure ()
              if replace then do
                    let strname = stringifyName Global name
                    addDefToPreamble strname (strname ++ " = " ++ def) False
                    pure ()
                 else
                    pure ()

  processPrimCmp :
         {auto stack : Ref Stack StackSt}
      -> {auto frame : StackFrame}
      -> {auto opts : COpts}
      -> PrimFn arity
      -> Vect arity NamedCExp
      -> Core LuaBlock
  processPrimCmp op args = do
      args' <- traverseVect processExpr args
      let (blockA, args) = unzip args'
      (blockB, cas) <- mkCase
                [(justReturn $ LPrimFn op args, justReturn (LNumber "1"))]
                (Just $ justReturn (LNumber "0"))
      pure (concat blockA <+> blockB, cas)

  constCaseIndex : NamedConstAlt -> LuaExpr -> Core LuaExpr
  constCaseIndex (MkNConstAlt const _) index =
     case constantTy const of
          (Just IntegerType) => pure $ LPrimFn (Cast IntegerType StringType) [index]
          (Just other) => pure index
          Nothing => throw $ UserError ("Cannot match on " ++ show const)

  processExpr :
            {auto stack : Ref Stack StackSt}
         -> {auto frame : StackFrame}
         -> {auto opts : COpts}
         -> NamedCExp
         -> Core LuaBlock
  processExpr (NmLocal _ n) = pure (LDoNothing, LLVar n)
  processExpr (NmRef _ n) = pure (LDoNothing, LGVar n)
  processExpr (NmLam _ n e) =
    do
      newFrame <- pushFrame
      (ce, e) <- processExpr {frame = newFrame} e
      vars <- popFrame
      pure (LDoNothing, LLambda [n] (declFrameTable newFrame vars <+> ce <+> LReturn e)) --paste inner block here
  processExpr (NmApp _ f args) =
    do
      (cf, f) <- processExpr f
      args <- traverse processExpr args
      let (cargs, args) = unzip args
      pure (cf <+> concat cargs, curriedApp f args)
  processExpr (NmPrimVal _ c) = pure (LDoNothing, !(processConstant c))
  processExpr (NmOp _ op@(EQ _) args) = processPrimCmp op args
  processExpr (NmOp _ op@(LT _) args) = processPrimCmp op args
  processExpr (NmOp _ op@(LTE _) args) = processPrimCmp op args
  processExpr (NmOp _ op@(GT _) args) = processPrimCmp op args
  processExpr (NmOp _ op@(GTE _) args) = processPrimCmp op args
  processExpr (NmOp _ StrIndex [str, i]) = do
    (blockA, str) <- processExpr str
    (blockB, i) <- processExpr i
    pure (blockA <+> blockB, LPrimFn StrIndex [str, LPrimFn (Add IntType) [i, LNumber "1"]])
  processExpr (NmOp _ StrSubstr [offset, len, str]) =
    do
      (blockA, offset) <- processExpr offset
      (blockB, len) <- processExpr len
      (blockC, str) <- processExpr str
      pure (blockA <+> blockB <+> blockC, LPrimFn StrSubstr [LPrimFn (Add IntType) [offset, LNumber "1"], len, str])
  processExpr (NmOp _ op args) =
    do
      args <- traverseVect processExpr args
      let (block, args) = unzip args
      pure (concat block, LPrimFn op args)
  processExpr (NmConCase _ sc alts def) =
    do
      (blockA, sc) <- processExpr sc
      conVar <- pushLocal
      alts <- traverse (processConsAlt conVar) alts
      let table = LTable (replicate (alts |> length) (LDoNothing, LNil)) --preallocate space
      tableVar <- pushLocal
      let assignments = (\(k, v) => LAssign Nothing (LIndex tableVar k) v) <$> alts
      mdef <- sequenceMaybe $ processExpr <$> def
      let indexed = LIndex tableVar (LIndex conVar (LString "tag"))
      indexedVar <- pushLocal
      (blockB, cas) <- mkCase [(justReturn indexedVar, justReturn (LApp indexedVar []))] mdef
      pure (blockA
           <+> LAssign Nothing conVar sc
           <+> LAssign Nothing tableVar table
           <+> concat assignments
           <+> LAssign Nothing indexedVar indexed
           <+> blockB, cas)
  processExpr (NmConstCase _ sc rawalts def) =
    do
      (blockA, sc) <- processExpr sc
      constVar <- pushLocal
      alts <- traverse processConstAlt rawalts
      let table = LTable (replicate (alts |> length) (LDoNothing, LNil)) --preallocate space
      tableVar <- pushLocal
      let assignments = (\(k, v) => LAssign Nothing (LIndex tableVar k) v) <$> alts
      mdef <- sequenceMaybe $ processExpr <$> def
      index <-
          (\alt => constCaseIndex alt constVar)
          <$> head' rawalts `orElse` pure luaNull --orElse is in case there is only default branch of case clause
      let indexed = LIndex tableVar index
      indexedVar <- pushLocal
      (blockB, cas) <- mkCase [(justReturn indexedVar, justReturn (LApp indexedVar []))] mdef
      pure (blockA
           <+> LAssign Nothing constVar sc
           <+> LAssign Nothing tableVar table
           <+> concat assignments
           <+> LAssign Nothing indexedVar indexed
           <+> blockB, cas)
  processExpr (NmExtPrim _ p args) = do
     processExtCall p args
  processExpr (NmCon _ n _ mbtag args) =
    do
      args <- traverse processExpr args
      let (blockA, args) = unzip args
      tableVar <- pushLocal
      let conArgs = zipWith (\i, arg => (LString $ "arg" ++ (show i), arg)) [1..args |> length] args
      let mbName = if opts |> storeConstructorName |> get then [(LString "cons", LString $ stringifyName Global n), (LString "num", LNumber $ args |> length |> show)] else []
      let kvs = [(LString "tag", LString (processTag n mbtag))] ++ conArgs ++ mbName
      pure (concat blockA
           <+> LAssign Nothing tableVar (LTable [])
           <+> concat ((\(k, v) => LAssign Nothing (LIndex tableVar k) v) <$> kvs)
           , tableVar)
  processExpr (NmDelay _ _ t) =
    do
      newFrame <- pushFrame
      (blockA, t) <- processExpr {frame = newFrame} t
      vars <- popFrame
      pure (LDoNothing, LLambda [] (declFrameTable newFrame vars <+> blockA <+> LReturn t))
  processExpr (NmForce _ _ t) =
    do
      (blockA, t) <- processExpr t
      pure (blockA, LApp t [])
  processExpr (NmLet _ n val sc) =
    do
      (blockA, val) <- processExpr val
      (blockB, cs) <- processExpr sc
      pure (blockA <+> LAssign (Just Local) (LLVar n) val <+> blockB, cs) --TODO replace names, use stack
  processExpr (NmErased _) =
    pure (LDoNothing, LNil)
  processExpr (NmCrash _ msg) =
    pure (LDoNothing, mkErrorAst msg)

  --TODO copy-pasted(whole mutual block) from Compiler.Scheme.Common, PR export flag
  used : Name -> NamedCExp -> Bool
  usedCon : Name -> NamedConAlt -> Bool
  usedConst : Name -> NamedConstAlt -> Bool

  used n (NmLocal fc n') = n == n'
  used n (NmRef _ _) = False
  used n (NmLam _ _ sc) = used n sc
  used n (NmLet _ _ v sc) = used n v || used n sc
  used n (NmApp _ f args) = used n f || any id (map (used n) args)
  used n (NmCon _ _ _ _ args) = any id (map (used n) args)
  used n (NmOp _ _ args) = any id (toList (map (used n) args))
  used n (NmExtPrim _ _ args) = any id (map (used n) args)
  used n (NmForce _ _ t) = used n t
  used n (NmDelay _ _ t) = used n t
  used n (NmConCase _ sc alts def)
        = used n sc || any id (map (usedCon n) alts)
              || maybe False (used n) def
  used n (NmConstCase _ sc alts def)
        = used n sc || any id (map (usedConst n) alts)
              || maybe False (used n) def
  used n _ = False

  usedCon n (MkNConAlt _ _ _ _ sc) = used n sc

  usedConst n (MkNConstAlt _ sc) = used n sc

  processConsAlt :
        {auto stack : Ref Stack StackSt}
     -> {auto frame : StackFrame}
     -> {auto opts : COpts}
     -> (cons : LuaExpr)
     -> (alt : NamedConAlt)
     -> Core (LuaExpr {-tag-}, LuaExpr {-arm-})
  processConsAlt cons (MkNConAlt name _ mbtag args res') =
    do
      newFrame <- pushFrame
      (blockA, res) <- processExpr {frame = newFrame} res'
      let bindings =
       zipWith (\i, n => if used n res' then LAssign (Just Local) (LLVar n) $ LIndex cons (indexConstructorArg i) else LDoNothing)
                [1..args |> length] args --TODO use stack instread of let bindings, replace names
      vars <- popFrame
      pure (LString $ processTag name mbtag, LLambda [] $ declFrameTable newFrame vars
                                                          <+> concat bindings
                                                          <+> blockA {-blockA uses those bindings-}
                                                          <+> LReturn res)

  processConstAlt :
        {auto stack : Ref Stack StackSt}
     -> {auto frame : StackFrame}
     -> {auto opts : COpts}
     -> (alt : NamedConstAlt)
     -> Core (LuaExpr {-const-}, LuaExpr {-arm-})
  processConstAlt alt@(MkNConstAlt c res) =
    do
      const <- processConstant c
      let const =
          case c of
               (BI i) => LString (show i) --all constants are LString or LNumber
               _ => const
      newFrame <- pushFrame
      (blockA, res) <- processExpr {frame = newFrame} res
      vars <- popFrame
      pure (const, LLambda [] $ declFrameTable newFrame vars
                              <+> blockA
                              <+> LReturn res)

  indexConstructorArg : Nat -> LuaExpr
  indexConstructorArg i = LString $ "arg" ++ (show i)

  processTag : Name -> Maybe Int -> String
  processTag n Nothing = stringifyName Global n
  processTag _ (Just i) = show i

  getErased : {auto refs : Ref Ctxt Defs}
           -> Name
           -> Core (List Nat)
  getErased name =
    do Just def <- lookupCtxtExact name (gamma !(get Ctxt))
        | _ => throw (InternalError $ "[Lua] Could not find def: " ++ show !(toFullNames name))
       pure def.eraseArgs

  processDef :
           {auto c: Ref Stack StackSt}
        -> {auto opts : COpts}
        -> {auto refs : Ref Ctxt Defs}
        -> {auto preamble : Ref Preamble PreambleSt}
        -> (Name, NamedDef)
        -> Core LuaExpr {- returns an assignment expression (statement) -}
  processDef (n, MkNmFun args expr) =
   if (find (== n) extNames) |> isJust
      then
         pure LDoNothing --do not gen names for ext fns and foreign fns, done separately
      else do
         newFrame <- pushFrame
         (blockA, expr) <- processExpr {frame = newFrame} expr
         vars <- popFrame
         pure $ mkFnDecl n (reverse args) $ LApp (LLambda [] $ declFrameTable newFrame vars
                                <+> blockA
                                <+> LReturn expr) [] -- paste code block into the function body,
                                                     -- we have to wrap the code in a lambda and then immediately call it
                                                     -- to make sure the block & the return expr form a valid Lua expression
                                                     -- TODO don't do this if the body is already wrapped in at least one function
    where
      mkFnDecl : Name -> List Name -> LuaExpr -> LuaExpr
      mkFnDecl n [] expr = LAssign (Just Global) (LGVar n) expr
      mkFnDecl n (x :: xs) expr = mkFnDecl n xs (LLambda [x] (LReturn expr))

  processDef (n, MkNmError expr) =
    throw $ (InternalError (show expr))
  processDef (n, MkNmForeign hints argsty retty) = --those are added into the preamble
    do
      processForeignDef n hints argsty retty
      pure LDoNothing
  processDef (n, MkNmCon _ _ _) =
    pure LDoNothing  --we do not need to predefine structures in lua

getCOpts : Core COpts --TODO use directives ?
getCOpts =
   do
      opt1 <- coreLift $ getEnv "StoreConsName"
      opt2 <- coreLift $ getEnv "DynSupport"
      (Just opt3) <- coreLift $ do str <- getEnv "LuaVersion"
                                   pure (parseLuaVersion =<< str)
         | _ => throw (UserError "Could not parse Lua version from $LuaVersion, format: X.X[.X]")
      opt4 <- coreLift $ getEnv "NoRequire"
      opt5 <- coreLift $ getEnv "DebugOutput"
      opt6 <- coreLift $ getEnv "OmitEntryCall"
      pure $ MkCOptsInfo
               (thisOrDefault (opt1 >>= parseEnvBool))
               (thisOrDefault (opt2 >>= parseEnvBool))
               (MkWithDefault opt3 _)
               (thisOrDefault (opt4 >>= parseEnvBool))
               (thisOrDefault (opt5 >>= parseEnvBool))
               (thisOrDefault (opt6 >>= parseEnvBool))

translate : Ref Ctxt Defs -> ClosedTerm -> Core StrBuffer
translate defs term = do
  opts <- getCOpts

  clock0 <- coreLift $ clockTime Monotonic

  logLine "Lua compilation started [0/5]"
  logLine ("Using " ++ opts |> luaVersion |> get |> show)
  cdata <- getCompileData False Cases term

  clock1 <- coreLift $ clockTime Monotonic

  logLine $ "Got compile data [1/5] in " ++ showMillis (toMillis $ timeDifference clock1 clock0)
  let ndefs = cdata.namedDefs
  let ctm = forget cdata.mainExpr

  clock2 <- coreLift $ clockTime Monotonic

  logLine $ "Looked up direct names [2/5] in " ++ showMillis (toMillis $ timeDifference clock2 clock1)
  let ndefs = (\(n, _, d) => (n, d)) <$> ndefs
  let ndefs = defsUsedByNamedCExp ctm (defsToUsedMap ndefs) -- work through relevant names only
  let ndefsMap = defsToUsedMap ndefs
  let ndefs = quicksort {defs = ndefsMap} ndefs -- sort names by dependency order
  s <- newRef Stack (MkStackSt [] frameLowest indexLowest)
  pr <- newRef Preamble (MkPreambleSt empty)
  cdefs <- traverse processDef ndefs

  clock3 <- coreLift $ clockTime Monotonic

  logLine $ "Compiled definitions [3/5] in " ++ showMillis (toMillis $ timeDifference clock3 clock2)
  let con_cdefs = concat cdefs
  --TODO tail call optimization
  frame <- pushFrame
  (block, main) <- processExpr {frame} ctm
  vars <- popFrame
  let frameTable = declFrameTable frame vars

  clock4 <- coreLift $ clockTime Monotonic

  logLine $ "Compiled main [4/5] in " ++ showMillis (toMillis $ timeDifference clock4 clock3)
  preamble <- getPreamble

  support <- if opts |> dynamicSupportLib |> get
             then
               pure "require(\"idris2-lua\")"
             else
               readDataFile $ "lua" </> "idris2-lua.lua"

  let returnPlan : DeferredStr =
             if opts |> omitEntryCall |> get
             then
               []
             else
               [
                 "\n--------- RETURN ---------\n"
               , stringify Z frameTable, "\n"
               , stringify Z block     , "\n"
               , stringify Z main
               ]

  let stringPlan : DeferredStr =
             [ " --------- SUPPORT DEFS ---------\n"
             , "idris = {}\n"
             , "idris.null = {}\n"
             , "local null = idris.null\n"
             , "idris.luaVersion = " ++ show (opts |> luaVersion |> get |> index) ++ "\n" --sets target Lua version to be used in support
             , "idris.noRequire  = " ++ (toLower . show) (opts |> noRequire |> get) ++ "\n"
             , support , "\n"
             , "local idris = idris\n"
             , "local W = idris.W\n"
             , "---------- PREAMBLE DEFS ----------\n"
             , join "\n" (preamble |> values)
             , "\n---------- CTX DEFS ----------\n"
             , stringify Z con_cdefs
             ]
          ++ returnPlan
          ++ ["\nreturn idris"]
  let mbyte = 1024 * 1024
  strbuf <- newRef LuaCode !(allocStrBuffer mbyte)
  traverse_ (writeStr LuaCode) stringPlan

  clock5 <- coreLift $ clockTime Monotonic

  logLine $ "Stringified lua [5/5] in " ++ showMillis (toMillis $ timeDifference clock5 clock4)
  logLine $ "All done in " ++ showMillis (toMillis $ timeDifference clock5 clock0)
  strbuf <- get LuaCode
  pure strbuf

bashScript : String -> String -> String
bashScript luaexe scriptname {-with extention-}
 =   "#!/usr/bin/env bash" ++ "\n"
  ++ "BASEDIR=$(dirname \"$0\")" ++ "\n"
  ++ luaexe ++ " $BASEDIR/" ++ scriptname ++ " $@"

getLuaExe : IO String
getLuaExe
 = do
      mbDefined <- getEnv "LuaExe"
      pure $ mbDefined `orElse` "lua"

build : Ref Ctxt Defs --TODO add option to build only the .lua file
     -> String
     -> ClosedTerm
     -> String {-relative-}
     -> Core String
build defs outputDir term file = do

  strbuf <- translate defs term
  let luaFile = file ++ ".lua"
  Right () <- coreLift $ writeBufferToFile (outputDir </> luaFile) strbuf.get strbuf.offset
   | Left err => throw $ FileErr (outputDir </> luaFile) err

  luaExe <- coreLift getLuaExe

  Right () <- coreLift $ writeFile (outputDir </> file) (bashScript luaExe luaFile)
   | Left err => do throw $ FileErr (outputDir </> file) err

  Right () <- coreLift $ chmodRaw (outputDir </> file) 0o755
   | Left err => do throw $ FileErr (outputDir </> file) err

  pure (outputDir </> file)

compile : Ref Ctxt Defs
       -> String
       -> String
       -> ClosedTerm
       -> String
       -> Core (Maybe String)
compile defs tmpDir outputDir term file = Just <$> build defs outputDir term file

execute : Ref Ctxt Defs -> String -> ClosedTerm -> Core ()
execute defs tmpDir term = do
  exe <- build defs tmpDir term "generated"
  coreLift_ $ fflush stdout
  coreLift_ $ system $ "'" ++ exe ++ "' "
  pure ()

luaCodegen : Codegen
luaCodegen = MkCG compile execute Nothing Nothing

export
main : IO ()
main = mainWithCodegens [("lua", luaCodegen)]


text:
module Examples.CSS.Core

import Examples.CSS.Colors
import Rhone.JS
import Text.CSS

--------------------------------------------------------------------------------
--          IDs
--------------------------------------------------------------------------------

||| ID of the `<body>` element. The page content will
||| be placed here.
public export
contentDiv : ElemRef HTMLBodyElement
contentDiv = Id Body "content"

||| The page consists of a static heading with a title an
||| (eventually) a short description of the project.
||| This is followed by a selection box, where visitors can
||| choose an example application.
|||
||| The example application will be dynamicall generated and
||| placed in to a `<div>` with ID `"example"`.
public export
exampleDiv : ElemRef HTMLDivElement
exampleDiv = Id Div "example"

||| ID of a `<style>` element in the page header.
||| The generated CSS rules will go here.
public export
appStyle : ElemRef HTMLStyleElement
appStyle = Id Style "appstyle"

--------------------------------------------------------------------------------
--          Classes
--------------------------------------------------------------------------------

||| a clickable button
public export
btn : String
btn = "btn"

||| a text input
public export
textIn : String
textIn = "textin"

||| a select input
public export
selectIn : String
selectIn = "selectin"

||| an input widget
public export
widget : String
widget = "widget"

||| a list of input widgets,
||| each on its own line, often with a label
||| on the left.
public export
widgetList : String
widgetList = "widgetList"

||| the main content, split into three rows:
||| a title, the example selector, and the
||| currently loaded example application
public export
contentList : String
contentList = "contentList"

||| the header row where the example selector
||| resides
public export
contentHeader : String
contentHeader = "contentHeader"

||| the row with the page title
public export
pageTitle : String
pageTitle = "pageTitle"

||| the select box used to choose an example
||| application
public export
exampleSelector : String
exampleSelector = "example_selector"

||| a single line in a column
||| of input widgets.
public export
widgetLine : String
widgetLine = "widgetline"

||| a label on the left of an input
||| widget.
public export
widgetLabel : String
widgetLabel = "widgetlabel"

--------------------------------------------------------------------------------
--          Rules
--------------------------------------------------------------------------------

export
coreCSS : List (Rule 1)
coreCSS =
  [ elem Html !!
      [ Height          .= perc 100]

  , elem Body !!
      [ BackgroundColor .= black
      , Color           .= base100
      , Display         .= Flex
      , FlexDirection   .= Column
      , FontFamily      .= "Helvetica, Arial, sans-serif"
      , Height          .= perc 100
      , Margin          .= px 0
      ]

  , class contentList !!
      [ AlignSelf       .= Center
      , BackgroundColor .= darker_grey
      , Display         .= Flex
      , Flex            .= "1"
      , FlexDirection   .= Column
      , JustifyContent  .= FlexStart
      , Padding         .= VH (px 0) (pt 20)
      , MinWidth        .= perc 80
      ]

  , class pageTitle !!
      [ BorderStyle     .= Bottom Solid
      , BorderWidth     .= Bottom (px 5)
      , BorderColor     .= Bottom base80
      , FontSize        .= XLarge
      , Padding         .= VH (px 40) (px 0)
      , TextAlign       .= Center
      ]

  , class contentHeader !!
      [ Display             .= Grid
      , ColumnGap           .= px 10
      , GridTemplateColumns .= [px 170, fr 1, fr 3]
      , BorderStyle         .= Bottom Solid
      , BorderWidth         .= Bottom (px 2)
      , BorderColor         .= Bottom base80
      , Padding             .= VH (px 30) (px 10)
      ]

  , class widget !!
      [ BackgroundColor .= lighter_grey
      , BorderRadius    .= px 8
      , BorderStyle     .= All Solid
      , BorderWidth     .= px 2
      , BorderColor     .= All comp100
      , Color           .= darker_grey
      , FontSize        .= Large
      , Padding         .= px 3
      ]

  , Pseudo (class widget) Hover !!
      [ BackgroundColor .= lightest_grey
      , BorderColor     .= All comp60
      ]

  , Pseudo (class widget) Active !!
      [ BackgroundColor .= lightest_grey
      , BorderColor     .= All comp60
      ]

  , Pseudo (class widget) FocusVisible !!
      [ BackgroundColor .= lightest_grey
      , BorderColor     .= All comp60
      ]

  , Pseudo (class widget) Disabled !!
      [ BackgroundColor .= light_grey
      , BorderColor     .= All dark_grey
      ]

  , class textIn  !!
      [ TextAlign       .= End ]

  , class selectIn  !!
      [ TextAlign       .= End ]

  , class exampleSelector  !!
      [ FontSize        .= Large
      , GridColumn      .= At 2
      ]

  , Pseudo (class widget) Invalid !!
      [ BorderColor     .= All red ]

  -- deprecated
  , class widgetList !!
      [ ListStyleType   .= None
      , Display         .= Flex
      , FlexDirection   .= Column
      , JustifyContent  .= FlexStart
      ]

  -- deprecated
  , class widgetLine !!
      [ AlignItems      .= FlexStart
      , Display         .= Flex
      , Margin          .= Bottom (px 5)
      ]

  , class widgetLabel !!
      [ FontSize        .= Large ]
  ]


text:
-- WIP

module Main
import Data.Strings

intToDouble : Int -> Double
intToDouble x = cast x

x1 : Int
x1 = 2

doubleToInt : Double -> Int
doubleToInt y = cast y

x2 : Double
x2 = 5.3

main : IO ()
main = do printLn $ intToDouble x1
          printLn $ doubleToInt x2
          printLn $ stringToNatOrZ ""
          printLn $ stringToNatOrZ "32q4"
          printLn $ stringToNatOrZ "23"


text:
module Numeric
import Data.Nat

%default total

-- Well-founded Integer
-- All Integers are either a natural number
-- or the inversion of a positive number.
public export
data WFInt : Type where
     Nat : (n : Nat) -> WFInt
     Neg : (n : Nat) -> WFInt --Note: In the negative case, n=Z represents -1.

-- Magnitude of an integer
public export
mag : WFInt -> Nat
mag (Nat n) = n
mag (Neg n) = (S n)

-- Implement casting back and forth from normal Integer type
public export
Cast WFInt Integer where
     cast (Nat n) = cast n
     cast (Neg n) = negate $ cast (S n)

public export
Cast Integer WFInt where
     cast n = case (compare n 0) of
           EQ => Nat (fromInteger n)
           GT => Nat (fromInteger n)
           LT => Neg (fromInteger $ negate $ n + 1)

-- For arithmetic operations, cast to Integer and then cast back
public export
Num WFInt where
   (+) a b = cast $ (cast a) + (cast b)
   (*) a b = cast $ (cast a) * (cast b)
   fromInteger a = cast a

public export
Neg WFInt where
    negate a = cast $ negate $ (the Integer $ cast a)
    (-) a b = cast $ (the Integer $ cast a) - (the Integer $ cast b)

public export
partial
Integral WFInt where
         div a b = cast $ the Integer $ div (cast a) (cast b)
         mod a b = cast $ the Integer $ mod (cast a) (cast b)

-- n-parity, i.e. proof that an integer a is evenly divisible by n (or not).
public export
data Parity : (a : WFInt) -> (n : WFInt) -> Type where
     -- a has even n-parity if there exists an integer multiple x s.t. x*n = a.
     Factor    : (x : WFInt ** (x * n) = a) -> Parity a n
     ModIsZero : (mod n a = 0) -> Parity a n

public export
data OddParity : (a : WFInt) -> (n : WFInt) -> Type where
     -- a has odd n-parity if there exists
     Odd : (b : WFInt ** LT = compare (mag b) (mag n)) -> (Parity (a + b) n) ->  OddParity a n

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
module Package.IkanExecute
import Package.IkanAst
import Package.IpkgAst
import Control.Monad.Freer
import Debug.Trace
import Control.Monad.Id
import Data.Fin
import Control.Monad.State

%access public export

ikanExec' : {x : Type} -> IkanData x -> IO x
ikanExec' (AddDependencies xs) = pure ()
ikanExec' (AddSourcepaths xs) = pure ()

ikanExec : {x : Type} -> Freer IkanData x -> IO x
ikanExec x = foldFreer ikanExec' x

{-
ex1:IkanDataT
ex1 = do
  AddDependencies []
  AddSourcepaths []

-}

max_stars_repo_name: marcesquerra/ikan

max_issues_repo_name: marcesquerra/ikan

max_forks_repo_name: marcesquerra/ikan


text:
namespace A
  export
  foo3 : Int -> Int
  foo3 x with (x + 1)
  foo3 x | y = y + x

foo4 : Int
foo4 = A.foo3 5


text:
module Control.App.PrimApp

import Data.List
import Data.IORef

public export
data PEffect : Type where
     St : Type -> PEffect
     Exc : Type -> PEffect
     Sys : PEffect

public export
data HasPEff : PEffect -> List PEffect -> Type where
     Here : HasPEff e (e :: es)
     There : HasPEff e es -> HasPEff e (e' :: es)

public export
data NotException : PEffect -> Type where
     StNotE : NotException (St t)
     SysNotE : NotException Sys

public export
data NotState : PEffect -> Type where
     ExcNotS : NotState (Exc t)
     SysNotS : NotState Sys

public export
data Linear : List PEffect -> Type where
     EmptyLin : Linear []
     RestLin : NotException e => Linear es -> Linear (e :: es)

public export
data Stateless : List PEffect -> Type where
     EmptySt : Stateless []
     RestSt : NotState e => Stateless es -> Stateless (e :: es)

export
data Env : List PEffect -> Type where
     None : Env []
     Ref : IORef t -> Env es -> Env (St t :: es)
     SkipE : Env es -> Env (Exc t :: es)
     SkipP : Env es -> Env (Sys :: es)

getState : Env es -> (p : HasPEff (St t) es) -> IORef t
getState (Ref r env) Here = r
getState (Ref r env) (There p) = getState env p
getState (SkipE env) (There p) = getState env p
getState (SkipP env) (There p) = getState env p

public export
0 execTy : List PEffect -> Type -> Type
execTy [] ty = ty
execTy (St t :: es) ty = execTy es ty
execTy (Exc e :: es) ty = Either e (execTy es ty)
execTy (Sys :: es) ty = execTy es ty

public export
data PApp : List PEffect -> Type -> Type where
     Pure : (x : a) -> PApp es a
     Bind : PApp es a -> (a -> PApp es b) -> PApp es b
     BindL : Linear es =>
             (1 act : PApp es a) ->
             (1 k : a -> PApp es b) -> PApp es b

     New : a -> PApp (St a :: es) t -> PApp es t
     Get : HasPEff (St t) es => PApp es t
     Put : HasPEff (St t) es => t -> PApp es ()

     Throw : HasPEff (Exc e) es => e -> PApp es a
     Catch : HasPEff (Exc e) es =>
             PApp es a ->
             (err : e -> PApp es a) -> PApp es a
     Handle : PApp (Exc e :: es) a ->
              (ok : a -> PApp es b) ->
              (err : e -> PApp es b) -> PApp es b

     GetEnv : PApp es (Env es)
     Fork : HasPEff Sys es => PApp es () -> PApp es ()
     Prim : HasPEff Sys es => PrimIO a -> PApp es a

export
Functor (PApp es) where
  map f ap = Bind ap $ \ap' => Pure (f ap')

export
Applicative (PApp es) where
  pure = Pure
  (<*>) f a
      = Bind f $ \f' =>
        Bind a $ \a' => pure (f' a')

export
Monad (PApp es) where
  (>>=) = Bind

throwIn : Env es -> HasPEff (Exc e) es -> e ->
          IO (execTy (es ++ rest) a)
throwIn (SkipE es) Here e = pure (Left e)
throwIn (Ref r es) (There p) e = throwIn es p e
throwIn (SkipE es) (There p) e
    = do res <- throwIn es p e
         pure (Right res)
throwIn (SkipP es) (There p) e = throwIn es p e

findRes : Env es -> HasPEff (Exc e) es -> execTy es a -> Maybe e
findRes (SkipE env) (There p) (Left _) = Nothing -- wrong exception
findRes (SkipE env) (There p) (Right r) = findRes env p r
findRes (Ref r env) (There p) t = findRes env p t
findRes (SkipP env) (There p) t = findRes env p t
findRes None _ _ = Nothing
findRes _ Here (Left ex) = Just ex
findRes _ Here _ = Nothing

copyEnv : Env es -> IO (Env es)
copyEnv None = pure None
copyEnv (Ref t env)
    = do val <- readIORef t
         t' <- newIORef val
         env' <- copyEnv env
         pure (Ref t' env')
copyEnv (SkipE env)
    = do env' <- copyEnv env
         pure (SkipE env')
copyEnv (SkipP env)
    = do env' <- copyEnv env
         pure (SkipP env')

clearEnv : Env es -> IO (execTy es ())
clearEnv None = pure ()
clearEnv (Ref t env) = clearEnv env
clearEnv (SkipE env)
    = do e' <- clearEnv env
         pure (Right e')
clearEnv (SkipP env) = clearEnv env

exec : Env es -> PApp es t -> (t -> IO (execTy es a)) -> IO (execTy es a)
exec env (Pure val) k = k val
exec env (Bind act next) k
    = exec env act (\res => exec env (next res) k)
exec env (BindL act next) k
    = exec env act (\res => exec env (next res) k)
exec env (New val prog) k
    = do r <- newIORef val
         exec (Ref r env) prog k
exec env (Get @{p}) k
    = do let ref = getState env p
         val <- readIORef ref
         k val
exec env (Put @{p} val) k
    = do let ref = getState env p
         writeIORef ref val
         k ()
exec env (Throw @{p} e) k
    = rewrite sym (appendNilRightNeutral es) in
        throwIn env p e {rest = []}
exec env (Handle prog ok err) k
    = do res <- exec (SkipE env) prog
                     (\res => do res' <- exec env (ok res) k
                                 pure (Right res'))
         case res of
              Left ex => exec env (err ex) k
              Right ok => pure ok
exec env (Catch @{p} prog err) k
    = do res <- exec env prog k
         case findRes env p res of
              Just ex => exec env (err ex) k
              Nothing => pure res
exec env GetEnv k = k env
exec env (Fork proc) k
    = do fork (do env' <- copyEnv env
                  exec env proc (\u => clearEnv env)
                  pure ())
         k ()
exec env (Prim io) k
    = do op <- primIO io
         k op
export
run : PApp [Sys] a -> IO a
run prog = exec (SkipP None) prog pure


text:
-- ---------------------------------------------------------------- [ Main.idr ]
-- Module  : Main
-- --------------------------------------------------------------------- [ EOH ]
module Main

import public {{ Project }}.Lib

-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_path: src/includes/idris/{{ Project }}.idr

max_stars_repo_name: vmchale/project-init

max_issues_repo_path: src/includes/idris/{{ Project }}.idr

max_issues_repo_name: vmchale/project-init

max_forks_repo_path: src/includes/idris/{{ Project }}.idr

max_forks_repo_name: vmchale/project-init