text:
module Compiler.RefC.RefC

import Compiler.RefC.CC

import Compiler.Common
import Compiler.CompileExpr
import Compiler.ANF
import Compiler.Generated

import Core.Context
import Core.Context.Log
import Core.Directory

import Data.List
import Libraries.Data.DList
import Data.Nat
import Data.String
import Libraries.Data.SortedSet
import Data.Vect

import System
import System.File

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

%default covering

showcCleanStringChar : Char -> String -> String
showcCleanStringChar '+' = ("_plus" ++)
showcCleanStringChar '-' = ("__" ++)
showcCleanStringChar '*' = ("_star" ++)
showcCleanStringChar '/' = ("_slash" ++)
showcCleanStringChar '\\' = ("_backslash" ++)
showcCleanStringChar '<' = ("_lt" ++)
showcCleanStringChar '>' = ("_gt" ++)
showcCleanStringChar '=' = ("_eq" ++)
showcCleanStringChar '&' = ("_and" ++)
showcCleanStringChar '|' = ("_or" ++)
showcCleanStringChar '\'' = ("_tick" ++)
showcCleanStringChar '"' = ("_quotation" ++)
showcCleanStringChar '(' = ("_parenOpen" ++)
showcCleanStringChar ')' = ("_parenClose" ++)
showcCleanStringChar '{' = ("_braceOpen" ++)
showcCleanStringChar '}' = ("_braceClose" ++)
showcCleanStringChar ' ' = ("_" ++)
showcCleanStringChar ':' = ("_colon" ++)
showcCleanStringChar '.' = ("_dot" ++)
showcCleanStringChar '$' = ("_dollar" ++)
showcCleanStringChar ',' = ("_comma" ++)
showcCleanStringChar '#' = ("_number" ++)
showcCleanStringChar '%' = ("_percent" ++)
showcCleanStringChar '~' = ("_tilde" ++)
showcCleanStringChar c
   = if c < chr 32 || c > chr 126
        then (("u" ++ leftPad '0' 4 (asHex (cast c))) ++)
        else strCons c

showcCleanString : List Char -> String -> String
showcCleanString [] = id
showcCleanString (c ::cs) = (showcCleanStringChar c) . showcCleanString cs

cCleanString : String -> String
cCleanString cs = showcCleanString (unpack cs) ""

export
cUserName : UserName -> String
cUserName (Basic n) = cCleanString n
cUserName (Field n) = "rec__" ++ cCleanString n
cUserName Underscore = cCleanString "_"

export
cName : Name -> String
cName (NS ns n) = cCleanString (showNSWithSep "_" ns) ++ "_" ++ cName n
cName (UN n) = cUserName n
cName (MN n i) = cCleanString n ++ "_" ++ cCleanString (show i)
cName (PV n d) = "pat__" ++ cName n
cName (DN _ n) = cName n
cName (Nested i n) = "n__" ++ cCleanString (show i) ++ "_" ++ cName n
cName (CaseBlock x y) = "case__" ++ cCleanString (show x) ++ "_" ++ cCleanString (show y)
cName (WithBlock x y) = "with__" ++ cCleanString (show x) ++ "_" ++ cCleanString (show y)
cName (Resolved i) = "fn__" ++ cCleanString (show i)
cName n = assert_total $ idris_crash ("INTERNAL ERROR: Unsupported name in C backend " ++ show n)
-- not really total but this way this internal error does not contaminate everything else

escapeChar : Char -> String
escapeChar c = if isAlphaNum c || isNL c
                  then show c
                  else "(char)" ++ show (ord c)

cStringQuoted : String -> String
cStringQuoted cs = strCons '"' (showCString (unpack cs) "\"")
where
    showCChar : Char -> String -> String
    showCChar '\\' = ("\\\\" ++)
    showCChar c
       = if c < chr 32
            then (("\\x" ++ leftPad '0' 2 (asHex (cast c))) ++ "\"\"" ++)
            else if c < chr 127 then strCons c
            else if c < chr 65536 then (("\\u" ++ leftPad '0' 4 (asHex (cast c))) ++ "\"\"" ++)
            else (("\\U" ++ leftPad '0' 8 (asHex (cast c))) ++ "\"\"" ++)

    showCString : List Char -> String -> String
    showCString [] = id
    showCString ('"'::cs) = ("\\\"" ++) . showCString cs
    showCString (c ::cs) = (showCChar c) . showCString cs

cConstant : Constant -> String
cConstant (I x) = "(Value*)makeInt64("++ show x ++")"
cConstant (I8 x) = "(Value*)makeInt8("++ show x ++")"
cConstant (I16 x) = "(Value*)makeInt16("++ show x ++")"
cConstant (I32 x) = "(Value*)makeInt32("++ show x ++")"
cConstant (I64 x) = "(Value*)makeInt64("++ show x ++")"
cConstant (BI x) = "(Value*)makeIntegerLiteral(\""++ show x ++"\")"
cConstant (Db x) = "(Value*)makeDouble("++ show x ++")"
cConstant (Ch x) = "(Value*)makeChar("++ escapeChar x ++")"
cConstant (Str x) = "(Value*)makeString("++ cStringQuoted x ++")"
cConstant WorldVal = "(Value*)makeWorld()"
cConstant IntType = "Int64"
cConstant Int8Type = "Int8"
cConstant Int16Type = "Int16"
cConstant Int32Type = "Int32"
cConstant Int64Type = "Int64"
cConstant IntegerType = "Integer"
cConstant StringType = "string"
cConstant CharType = "char"
cConstant DoubleType = "double"
cConstant WorldType = "f32"
cConstant (B8 x)   = "(Value*)makeBits8("++ show x ++")"
cConstant (B16 x)  = "(Value*)makeBits16("++ show x ++")"
cConstant (B32 x)  = "(Value*)makeBits32("++ show x ++")"
cConstant (B64 x)  = "(Value*)makeBits64("++ show x ++")"
cConstant Bits8Type = "Bits8"
cConstant Bits16Type = "Bits16"
cConstant Bits32Type = "Bits32"
cConstant Bits64Type = "Bits64"
cConstant n = assert_total $ idris_crash ("INTERNAL ERROR: Unknonw constant in C backend: " ++ show n)
-- not really total but this way this internal error does not contaminate everything else

extractConstant : Constant -> String
extractConstant (I x) = show x
extractConstant (I8 x) = show x
extractConstant (I16 x) = show x
extractConstant (I32 x) = show x
extractConstant (I64 x) = show x
extractConstant (BI x) = show x
extractConstant (Db x) = show x
extractConstant (Ch x) = show x
extractConstant (Str x) = cStringQuoted x
extractConstant (B8 x)  = show x
extractConstant (B16 x)  = show x
extractConstant (B32 x)  = show x
extractConstant (B64 x)  = show x
extractConstant c = assert_total $ idris_crash ("INTERNAL ERROR: Unable to extract constant: " ++ cConstant c)
-- not really total but this way this internal error does not contaminate everything else

||| Generate scheme for a plain function.
plainOp : String -> List String -> String
plainOp op args = op ++ "(" ++ (showSep ", " args) ++ ")"

||| Generate scheme for a primitive function.
cOp : {0 arity : Nat} -> PrimFn arity -> Vect arity String -> String
cOp (Neg ty)      [x]       = "negate_"  ++  cConstant ty ++ "(" ++ x ++ ")"
cOp StrLength     [x]       = "stringLength(" ++ x ++ ")"
cOp StrHead       [x]       = "head(" ++ x ++ ")"
cOp StrTail       [x]       = "tail(" ++ x ++ ")"
cOp StrReverse    [x]       = "reverse(" ++ x ++ ")"
cOp (Cast i o)    [x]       = "cast_" ++ (cConstant i) ++ "_to_" ++ (cConstant o) ++ "(" ++ x ++ ")"
cOp DoubleExp     [x]       = "(Value*)makeDouble(exp(unpackDouble(" ++ x ++ ")))"
cOp DoubleLog     [x]       = "(Value*)makeDouble(log(unpackDouble(" ++ x ++ ")))"
cOp DoublePow     [x, y]    = "(Value*)makeDouble(pow(unpackDouble(" ++ x ++ "), unpackDouble(" ++ y ++ ")))"
cOp DoubleSin     [x]       = "(Value*)makeDouble(sin(unpackDouble(" ++ x ++ ")))"
cOp DoubleCos     [x]       = "(Value*)makeDouble(cos(unpackDouble(" ++ x ++ ")))"
cOp DoubleTan     [x]       = "(Value*)makeDouble(tan(unpackDouble(" ++ x ++ ")))"
cOp DoubleASin    [x]       = "(Value*)makeDouble(asin(unpackDouble(" ++ x ++ ")))"
cOp DoubleACos    [x]       = "(Value*)makeDouble(acos(unpackDouble(" ++ x ++ ")))"
cOp DoubleATan    [x]       = "(Value*)makeDouble(atan(unpackDouble(" ++ x ++ ")))"
cOp DoubleSqrt    [x]       = "(Value*)makeDouble(sqrt(unpackDouble(" ++ x ++ ")))"
cOp DoubleFloor   [x]       = "(Value*)makeDouble(floor(unpackDouble(" ++ x ++ ")))"
cOp DoubleCeiling [x]       = "(Value*)makeDouble(ceil(unpackDouble(" ++ x ++ ")))"
cOp (Add ty)      [x, y]    = "add_" ++  cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
cOp (Sub ty)      [x, y]    = "sub_" ++  cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
cOp (Mul ty)      [x, y]    = "mul_" ++  cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
cOp (Div ty)      [x, y]    = "div_" ++  cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
cOp (Mod ty)      [x, y]    = "mod_" ++  cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
cOp (ShiftL ty)   [x, y]    = "shiftl_" ++  cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
cOp (ShiftR ty)   [x, y]    = "shiftr_" ++  cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
cOp (BAnd ty)     [x, y]    = "and_" ++  cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
cOp (BOr ty)      [x, y]    = "or_" ++  cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
cOp (BXOr ty)     [x, y]    = "xor_" ++  cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
cOp (LT ty)       [x, y]    = "lt_" ++  cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
cOp (GT ty)       [x, y]    = "gt_" ++  cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
cOp (EQ ty)       [x, y]    = "eq_" ++  cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
cOp (LTE ty)      [x, y]    = "lte_" ++  cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
cOp (GTE ty)      [x, y]    = "gte_" ++  cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
cOp StrIndex      [x, i]    = "strIndex(" ++ x ++ ", " ++ i ++ ")"
cOp StrCons       [x, y]    = "strCons(" ++ x ++ ", " ++ y ++ ")"
cOp StrAppend     [x, y]    = "strAppend(" ++ x ++ ", " ++ y ++ ")"
cOp StrSubstr     [x, y, z] =  "strSubstr(" ++ x ++ ", " ++ y  ++ ", " ++ z ++ ")"
cOp BelieveMe     [_, _, x] = "newReference(" ++ x ++ ")"
cOp Crash         [_, msg]  = "idris2_crash(" ++ msg ++ ");"
cOp fn args = plainOp (show fn) (toList args)

data ExtPrim = NewIORef | ReadIORef | WriteIORef
             | NewArray | ArrayGet | ArraySet
             | GetField | SetField
             | VoidElim
             | SysOS | SysCodegen
             | OnCollect
             | OnCollectAny
             | Unknown Name

export
Show ExtPrim where
  show NewIORef = "newIORef"
  show ReadIORef = "readIORef"
  show WriteIORef = "writeIORef"
  show NewArray = "newArray"
  show ArrayGet = "arrayGet"
  show ArraySet = "arraySet"
  show GetField = "getField"
  show SetField = "setField"
  show VoidElim = "voidElim"
  show SysOS = "sysOS"
  show SysCodegen = "sysCodegen"
  show OnCollect = "onCollect"
  show OnCollectAny = "onCollectAny"
  show (Unknown n) = "Unknown " ++ show n

||| Match on a user given name to get the scheme primitive
toPrim : Name -> ExtPrim
toPrim pn@(NS _ n)
    = cond [(n == UN (Basic "prim__newIORef"), NewIORef),
            (n == UN (Basic "prim__readIORef"), ReadIORef),
            (n == UN (Basic "prim__writeIORef"), WriteIORef),
            (n == UN (Basic "prim__newArray"), NewArray),
            (n == UN (Basic "prim__arrayGet"), ArrayGet),
            (n == UN (Basic "prim__arraySet"), ArraySet),
            (n == UN (Basic "prim__getField"), GetField),
            (n == UN (Basic "prim__setField"), SetField),
            (n == UN (Basic "void"), VoidElim), -- DEPRECATED. TODO: remove when bootstrap has been updated
            (n == UN (Basic "prim__void"), VoidElim),
            (n == UN (Basic "prim__os"), SysOS),
            (n == UN (Basic "prim__codegen"), SysCodegen),
            (n == UN (Basic "prim__onCollect"), OnCollect),
            (n == UN (Basic "prim__onCollectAny"), OnCollectAny)
            ]
           (Unknown pn)
toPrim pn = assert_total $ idris_crash ("INTERNAL ERROR: Unknown primitive: " ++ cName pn)
-- not really total but this way this internal error does not contaminate everything else

varName : AVar -> String
varName (ALocal i) = "var_" ++ (show i)
varName (ANull)    = "NULL"

data ArgCounter : Type where
data FunctionDefinitions : Type where
data TemporaryVariableTracker : Type where
data IndentLevel : Type where
data HeaderFiles : Type where

------------------------------------------------------------------------
-- Output generation: using a difference list for efficient append

data OutfileText : Type where

Output : Type
Output = DList String

------------------------------------------------------------------------

getNextCounter : {auto a : Ref ArgCounter Nat} -> Core Nat
getNextCounter = do
    c <- get ArgCounter
    put ArgCounter (S c)
    pure c

registerVariableForAutomaticFreeing : {auto t : Ref TemporaryVariableTracker (List (List String))}
                                   -> String
                                   -> Core ()
registerVariableForAutomaticFreeing var
  = update TemporaryVariableTracker $ \case
      [] => [[var]]
      (l :: ls) => ((var :: l) :: ls)

newTemporaryVariableLevel : {auto t : Ref TemporaryVariableTracker (List (List String))} -> Core ()
newTemporaryVariableLevel = update TemporaryVariableTracker ([] ::)

getNewVar : {auto a : Ref ArgCounter Nat} -> {auto t : Ref TemporaryVariableTracker (List (List String))} -> Core String
getNewVar = do
    c <- getNextCounter
    let var = "tmp_" ++ show c
    registerVariableForAutomaticFreeing var
    pure var

getNewVarThatWillNotBeFreedAtEndOfBlock : {auto a : Ref ArgCounter Nat} -> Core String
getNewVarThatWillNotBeFreedAtEndOfBlock = do
    c <- getNextCounter
    pure $ "tmp_" ++ show c

maxLineLengthForComment : Nat
maxLineLengthForComment = 60

lJust : (line:String) -> (fillPos:Nat) -> (filler:Char) -> String
lJust line fillPos filler =
    let n = length line in
    case isLTE n fillPos of
        (Yes prf) =>
            let missing = minus fillPos n
                fillBlock = pack (replicate missing filler)
            in
            line ++ fillBlock
        (No _) => line

increaseIndentation : {auto il : Ref IndentLevel Nat} -> Core ()
increaseIndentation = update IndentLevel S

decreaseIndentation : {auto il : Ref IndentLevel Nat} -> Core ()
decreaseIndentation = update IndentLevel pred

indentation : {auto il : Ref IndentLevel Nat} -> Core String
indentation = do
    iLevel <- get IndentLevel
    pure $ pack $ replicate (4 * iLevel) ' '

emit
  : {auto oft : Ref OutfileText Output} ->
    {auto il : Ref IndentLevel Nat} ->
    FC -> String -> Core ()
emit EmptyFC line = do
    indent <- indentation
    update OutfileText (flip snoc (indent ++ line))
emit fc line = do
    let comment = "// " ++ show fc
    indent <- indentation
    let indentedLine = indent ++ line
    update OutfileText $ case isLTE (length indentedLine) maxLineLengthForComment of
        (Yes _) => flip snoc (lJust indentedLine maxLineLengthForComment ' ' ++ " " ++ comment)
        (No _)  => flip appendR [indentedLine, (lJust ""   maxLineLengthForComment ' ' ++ " " ++ comment)]

freeTmpVars : {auto t : Ref TemporaryVariableTracker (List (List String))}
           -> {auto oft : Ref OutfileText Output}
           -> {auto il : Ref IndentLevel Nat}
           -> Core $ ()
freeTmpVars = do
    lists <- get TemporaryVariableTracker
    case lists of
        (vars :: varss) => do
            traverse_ (\v => emit EmptyFC $ "removeReference(" ++ v ++ ");" ) vars
            put TemporaryVariableTracker varss
        [] => pure ()

addHeader : {auto h : Ref HeaderFiles (SortedSet String)}
         -> String
         -> Core ()
addHeader header = do
    headerFiles <- get HeaderFiles
    put HeaderFiles $ insert header headerFiles

makeArglist : {auto a : Ref ArgCounter Nat}
           -> {auto t : Ref TemporaryVariableTracker (List (List String))}
           -> {auto oft : Ref OutfileText Output}
           -> {auto il : Ref IndentLevel Nat}
           -> Nat
           -> List AVar
           -> Core (String)
makeArglist missing xs = do
    c <- getNextCounter
    let arglist = "arglist_" ++ (show c)
    emit EmptyFC $  "Value_Arglist *"
                 ++ arglist
                 ++ " = newArglist(" ++ show missing
                 ++ "," ++ show (length xs + missing)
                 ++ ");"
    pushArgToArglist arglist xs 0
    pure arglist
where
    pushArgToArglist : String
                    -> List AVar
                    -> Nat
                    -> Core ()
    pushArgToArglist arglist [] k = pure ()
    pushArgToArglist arglist (arg :: args) k = do
        emit EmptyFC $ arglist
                    ++ "->args[" ++ show k ++ "] = "
                    ++ " newReference(" ++ varName arg ++");"
        pushArgToArglist arglist args (S k)

fillConstructorArgs : {auto oft : Ref OutfileText Output}
                   -> {auto il : Ref IndentLevel Nat}
                   -> String
                   -> List AVar
                   -> Nat
                   -> Core ()
fillConstructorArgs _ [] _ = pure ()
fillConstructorArgs cons (v :: vars) k = do
    emit EmptyFC $ cons ++ "->args["++ show k ++ "] = newReference(" ++ varName v ++");"
    fillConstructorArgs cons vars (S k)

showTag : Maybe Int -> String
showTag Nothing = "-1"
showTag (Just i) = show i

cArgsVectANF : {0 arity : Nat} -> Vect arity AVar -> Core (Vect arity String)
cArgsVectANF [] = pure []
cArgsVectANF (x :: xs) = pure $  (varName x) :: !(cArgsVectANF xs)

integer_switch : List AConstAlt -> Bool
integer_switch [] = True
integer_switch (MkAConstAlt c _  :: _) =
    case c of
        (I x) => True
        (I8 x) => True
        (I16 x) => True
        (I32 x) => True
        (I64 x) => True
        (BI x) => True
        (Ch x) => True
        _ => False

const2Integer : Constant -> Integer -> Integer
const2Integer c i =
    case c of
        (I x) => cast x
        (I8 x) => x
        (I16 x) => x
        (I32 x) => x
        (I64 x) => x
        (BI x) => x
        (Ch x) => cast x
        (B8 x) => cast x
        (B16 x) => cast x
        (B32 x) => cast x
        (B64 x) => x
        _ => i

-- we return for each of the ANF a set of statements and two possible return statements
-- The first one for non-tail statements, the second one for tail statements
-- this way, we can deal with tail calls and tail recursion.
-- The higher-level invocation first executes the normal statements and then
-- assign the return value
record ReturnStatement where
    constructor MkRS
    nonTailCall : String
    tailCall : String

mutual
    copyConstructors : {auto a : Ref ArgCounter Nat}
                    -> {auto t : Ref TemporaryVariableTracker (List (List String))}
                    -> {auto oft : Ref OutfileText Output}
                    -> {auto il : Ref IndentLevel Nat}
                    -> String
                    -> List AConAlt
                    -> String
                    -> String
                    -> Nat
                    -> Core $ ()
    copyConstructors _ [] _ _ _ = pure ()
    copyConstructors sc ((MkAConAlt n _ mTag args body) :: xs) constrFieldVar retValVar k = do
        (tag', name') <- getNameTag mTag n
        emit EmptyFC $ constrFieldVar ++ "[" ++ show k ++ "].tag = " ++ tag' ++ ";"
        emit EmptyFC $ constrFieldVar ++ "[" ++ show k ++ "].name = " ++ name' ++ ";"
        copyConstructors sc xs constrFieldVar retValVar (S k)
    where
        getNameTag : {auto a : Ref ArgCounter Nat} -> Maybe Int -> Name -> Core (String, String)
        getNameTag Nothing n = pure ("-1", "\"" ++ cName n ++ "\"")
        getNameTag (Just t) _ = pure (show t, "NULL")

    conBlocks : {auto a : Ref ArgCounter Nat}
             -> {auto t : Ref TemporaryVariableTracker (List (List String))}
             -> {auto oft : Ref OutfileText Output}
             -> {auto il : Ref IndentLevel Nat}
             -> (scrutinee:String)
             -> List AConAlt
             -> (returnValueVariable:String)
             -> (nrConBlock:Nat)
             -> Core ()
    conBlocks _ [] _ _ = pure ()
    conBlocks sc ((MkAConAlt n _ mTag args body) :: xs) retValVar k = do
        emit EmptyFC $ "  case " ++ show k ++ ":"
        emit EmptyFC $ "  {"
        increaseIndentation
        newTemporaryVariableLevel
        varBindLines sc args Z
        assignment <- cStatementsFromANF body
        emit EmptyFC $ retValVar ++ " = " ++ nonTailCall assignment ++ ";"
        freeTmpVars
        emit EmptyFC $ "break;"
        decreaseIndentation
        emit EmptyFC $ "  }"
        conBlocks sc xs retValVar (S k)
    where
        varBindLines : String -> (args : List Int) -> Nat -> Core ()
        varBindLines _ [] _ = pure ()
        varBindLines sc (target :: xs) source = do
            emit EmptyFC $  "Value * var_" ++ show target ++ " = ((Value_Constructor*)" ++ sc ++ ")->args[" ++ show source ++ "];"
            varBindLines sc xs (S source)
            pure ()

    constBlockSwitch : {auto a : Ref ArgCounter Nat}
                       -> {auto t : Ref TemporaryVariableTracker (List (List String))}
                       -> {auto oft : Ref OutfileText Output}
                       -> {auto il : Ref IndentLevel Nat}
                       -> (alts:List AConstAlt)
                       -> (retValVar:String)
                       -> (alternativeIntMatcher:Integer)
                       -> Core ()
    constBlockSwitch [] _ _ = pure ()
    constBlockSwitch ((MkAConstAlt c' caseBody) :: alts) retValVar i = do
        let c = const2Integer c' i
        emit EmptyFC $ "  case " ++ show c ++ " :"
        emit EmptyFC "  {"
        increaseIndentation
        newTemporaryVariableLevel
        assignment <- cStatementsFromANF caseBody
        emit EmptyFC $ retValVar ++ " = " ++ nonTailCall assignment ++ ";"
        freeTmpVars
        emit EmptyFC "break;"
        decreaseIndentation
        emit EmptyFC "  }"
        constBlockSwitch alts retValVar (i+1)

    constDefaultBlock : {auto a : Ref ArgCounter Nat}
                     -> {auto t : Ref TemporaryVariableTracker (List (List String))}
                     -> {auto oft : Ref OutfileText Output}
                     -> {auto il : Ref IndentLevel Nat}
                     -> (def:Maybe ANF)
                     -> (retValVar:String)
                     -> Core ()
    constDefaultBlock Nothing _ = pure ()
    constDefaultBlock (Just defaultBody) retValVar = do
        emit EmptyFC "  default :"
        emit EmptyFC "  {"
        increaseIndentation
        newTemporaryVariableLevel
        assignment <- cStatementsFromANF defaultBody
        emit EmptyFC $ retValVar ++ " = " ++ nonTailCall assignment ++ ";"
        freeTmpVars
        decreaseIndentation
        emit EmptyFC "  }"

    makeNonIntSwitchStatementConst :
                    {auto a : Ref ArgCounter Nat}
                 -> {auto t : Ref TemporaryVariableTracker (List (List String))}
                 -> {auto oft : Ref OutfileText Output}
                 -> {auto il : Ref IndentLevel Nat}
                 -> List AConstAlt
                 -> (k:Int)
                 -> (constantArray:String)
                 -> (compareFct:String)
                 -> Core (String, String)
    makeNonIntSwitchStatementConst [] _ constantArray compareFct  = pure (constantArray, compareFct)
    makeNonIntSwitchStatementConst ((MkAConstAlt constant caseBody) :: alts) 0 _ _ = do
        case constant of
            (Str s) => do
                c <- getNextCounter
                let constantArray = "constantArray_" ++ show c
                emit EmptyFC $ "char **" ++ constantArray ++ " = (char**)malloc(sizeof(char*) * " ++ show (1+(length alts)) ++");"
                makeNonIntSwitchStatementConst ((MkAConstAlt constant caseBody) :: alts) 1 constantArray "multiStringCompare"
            (Db d) => do
                c <- getNextCounter
                let constantArray = "constantArray_" ++ show c
                emit EmptyFC $ "double *" ++ constantArray ++ " = (double*)malloc(sizeof(double) * " ++ show (1+(length alts)) ++");"
                makeNonIntSwitchStatementConst ((MkAConstAlt constant caseBody) :: alts) 1 constantArray "multiDoubleCompare"
            _ => pure ("ERROR_NOT_DOUBLE_OR_STRING", "ERROR_NOT_DOUBLE_OR_STRING")
    makeNonIntSwitchStatementConst ((MkAConstAlt constant caseBody) :: alts) k constantArray compareFct = do
        emit EmptyFC $ constantArray ++ "[" ++ show (k-1) ++ "] = " ++ extractConstant constant ++ ";"
        makeNonIntSwitchStatementConst alts (k+1) constantArray compareFct

    checkTags : List AConAlt -> Core Bool
    checkTags [] = pure False
    checkTags ((MkAConAlt n _ Nothing args sc) :: xs) = pure False
    checkTags _ = pure True

    cStatementsFromANF : {auto a : Ref ArgCounter Nat}
                      -> {auto t : Ref TemporaryVariableTracker (List (List String))}
                      -> {auto oft : Ref OutfileText Output}
                      -> {auto il : Ref IndentLevel Nat}
                      -> ANF
                      -> Core ReturnStatement
    cStatementsFromANF (AV fc x) = do
        let returnLine = "newReference(" ++ varName x  ++ ")"
        pure $ MkRS returnLine returnLine
    cStatementsFromANF (AAppName fc _ n args) = do
        emit fc $ ("// start " ++ cName n ++ "(" ++ showSep ", " (map (\v => varName v) args) ++ ")")
        arglist <- makeArglist 0 args
        c <- getNextCounter
        let f_ptr_name = "fPtr_" ++ show c
        emit fc $ "Value *(*"++ f_ptr_name ++ ")(Value_Arglist*) = "++  cName n ++ "_arglist;"
        let closure_name = "closure_" ++ show c
        emit fc $ "Value *"
               ++ closure_name
               ++ " = (Value*)makeClosureFromArglist("
               ++ f_ptr_name
               ++ ", "
               ++ arglist
               ++ ");"
        emit fc $ ("// end   " ++ cName n ++ "(" ++ showSep ", " (map (\v => varName v) args) ++ ")")
        pure $ MkRS ("trampoline(" ++ closure_name ++ ")") closure_name
    cStatementsFromANF (AUnderApp fc n missing args) = do
        arglist <- makeArglist missing args
        c <- getNextCounter
        let f_ptr_name = "closure_" ++ show c
        let f_ptr = "Value *(*"++ f_ptr_name ++ ")(Value_Arglist*) = "++  cName n ++ "_arglist;"
        emit fc f_ptr
        let returnLine = "(Value*)makeClosureFromArglist(" ++ f_ptr_name  ++ ", " ++ arglist ++ ")"
        pure $ MkRS returnLine returnLine
    cStatementsFromANF (AApp fc _ closure arg) =
        pure $ MkRS ("apply_closure(" ++ varName closure ++ ", " ++ varName arg ++ ")")
                    ("tailcall_apply_closure(" ++ varName closure ++ ", " ++ varName arg ++ ")")
    cStatementsFromANF (ALet fc var value body) = do
        valueAssignment <- cStatementsFromANF value
        emit fc $ "Value * var_" ++ (show var) ++ " = " ++ nonTailCall valueAssignment ++ ";"
        registerVariableForAutomaticFreeing $ "var_" ++ (show var)
        bodyAssignment <- cStatementsFromANF body
        pure $ bodyAssignment
    cStatementsFromANF (ACon fc n _ tag args) = do
        c <- getNextCounter
        let constr = "constructor_" ++ (show c)
        emit fc $ "Value_Constructor* "
                ++ constr ++ " = newConstructor("
                ++ (show (length args))
                ++ ", "  ++ showTag tag  ++ ", "
                ++ "\"" ++ cName n ++ "\""
                ++ ");"
        emit fc $ " // constructor " ++ cName n

        fillConstructorArgs constr args 0
        pure $ MkRS ("(Value*)" ++ constr) ("(Value*)" ++ constr)
    cStatementsFromANF (AOp fc _ op args) = do
        argsVec <- cArgsVectANF args
        let opStatement = cOp op argsVec
        pure $ MkRS opStatement opStatement
    cStatementsFromANF (AExtPrim fc _ p args) = do
        emit fc $ "// call to external primitive " ++ cName p
        let returnLine = (cCleanString (show (toPrim p)) ++ "("++ showSep ", " (map varName args) ++")")
        pure $ MkRS returnLine returnLine
    cStatementsFromANF (AConCase fc sc alts mDef) = do
        c <- getNextCounter
        switchReturnVar <- getNewVarThatWillNotBeFreedAtEndOfBlock
        let newValueLine = "Value * " ++ switchReturnVar ++ " = NULL;"
        let constructorField = "constructorField_" ++ show c
        let constructorFieldLine = "AConAlt * " ++ constructorField
                                ++ "= newConstructorField(" ++ show (length alts) ++ ");"
        let switchLine = "switch(compareConstructors("
                      ++ varName sc
                      ++ ", "
                      ++ constructorField
                      ++ ", "
                      ++ show (length alts)
                      ++ ")){"
        emit fc newValueLine
        emit fc constructorFieldLine
        copyConstructors (varName sc) alts constructorField switchReturnVar 0
        emit fc switchLine
        conBlocks (varName sc) alts switchReturnVar 0
        case mDef of
            Nothing => do
                emit EmptyFC $ "}"
                emit EmptyFC $ "free(" ++ constructorField ++ ");"
                pure $ MkRS switchReturnVar switchReturnVar
            (Just d) => do
                emit EmptyFC $ "  default : {"
                increaseIndentation
                newTemporaryVariableLevel
                defaultAssignment <- cStatementsFromANF d
                emit EmptyFC $ switchReturnVar ++ " = " ++ nonTailCall defaultAssignment ++ ";"
                freeTmpVars
                decreaseIndentation
                emit EmptyFC $ "  }"
                emit EmptyFC $ "}"
                emit EmptyFC $ "free(" ++ constructorField ++ ");"
                pure $ MkRS switchReturnVar switchReturnVar
    cStatementsFromANF (AConstCase fc sc alts def) = do
        switchReturnVar <- getNewVarThatWillNotBeFreedAtEndOfBlock
        let newValueLine = "Value * " ++ switchReturnVar ++ " = NULL;"
        emit fc newValueLine
        case integer_switch alts of
            True => do
                emit fc $ "switch(extractInt(" ++ varName sc ++")){"
                constBlockSwitch alts switchReturnVar 0
                constDefaultBlock def switchReturnVar
                emit EmptyFC "}"
                pure $ MkRS switchReturnVar switchReturnVar
            False => do
                (compareField, compareFunction) <- makeNonIntSwitchStatementConst alts 0 "" ""
                emit fc $ "switch("++ compareFunction ++ "(" ++ varName sc ++ ", " ++ show (length alts) ++ ", " ++ compareField ++ ")){"
                constBlockSwitch alts switchReturnVar 0
                constDefaultBlock def switchReturnVar
                emit EmptyFC "}"
                emit EmptyFC $ "free(" ++ compareField ++ ");"
                pure $ MkRS switchReturnVar switchReturnVar
    cStatementsFromANF (APrimVal fc c) = pure $ MkRS (cConstant c) (cConstant c)
    cStatementsFromANF (AErased fc) = pure $ MkRS "NULL" "NULL"
    cStatementsFromANF (ACrash fc x) = do
        emit fc $ "// CRASH"
        pure $ MkRS "NULL" "NULL"

addCommaToList : List String -> List String
addCommaToList [] = []
addCommaToList (x :: xs) = ("  " ++ x) :: map (", " ++) xs

functionDefSignature : {auto c : Ref Ctxt Defs} -> Name -> (args:List Int) -> Core String
functionDefSignature n [] = do
    let fn = (cName !(getFullName n))
    pure $  "\n\nValue *"  ++ fn ++ "(void)"
functionDefSignature n args = do
    let argsStringList = addCommaToList (map (\i =>  "  Value * var_" ++ (show i)) args)
    let fn = (cName !(getFullName n))
    pure $  "\n\nValue *"  ++ fn ++ "\n(\n" ++ (showSep "\n" (argsStringList)) ++ "\n)"

functionDefSignatureArglist : {auto c : Ref Ctxt Defs} -> Name  -> Core String
functionDefSignatureArglist n = pure $  "Value *"  ++ (cName !(getFullName n)) ++ "_arglist(Value_Arglist* arglist)"

getArgsNrList : List ty -> Nat -> List Nat
getArgsNrList [] _ = []
getArgsNrList (x :: xs) k = k :: getArgsNrList xs (S k)

cTypeOfCFType : CFType -> String
cTypeOfCFType CFUnit          = "void"
cTypeOfCFType CFInt           = "int64_t"
cTypeOfCFType CFUnsigned8     = "uint8_t"
cTypeOfCFType CFUnsigned16    = "uint16_t"
cTypeOfCFType CFUnsigned32    = "uint32_t"
cTypeOfCFType CFUnsigned64    = "uint64_t"
cTypeOfCFType CFString        = "char *"
cTypeOfCFType CFDouble        = "double"
cTypeOfCFType CFChar          = "char"
cTypeOfCFType CFPtr           = "void *"
cTypeOfCFType CFGCPtr         = "void *"
cTypeOfCFType CFBuffer        = "void *"
cTypeOfCFType CFWorld         = "void *"
cTypeOfCFType (CFFun x y)     = "void *"
cTypeOfCFType (CFIORes x)     = "void *"
cTypeOfCFType (CFStruct x ys) = "void *"
cTypeOfCFType (CFUser x ys)   = "void *"
cTypeOfCFType n = assert_total $ idris_crash ("INTERNAL ERROR: Unknonw FFI type in C backend: " ++ show n)

varNamesFromList : List ty -> Nat -> List String
varNamesFromList str k = map (("var_" ++) . show) (getArgsNrList str k)

createFFIArgList : List CFType
                -> Core $ List (String, String, CFType)
createFFIArgList cftypeList = do
    let sList = map cTypeOfCFType cftypeList
    let varList = varNamesFromList cftypeList 1
    pure $ zip3 sList varList cftypeList

emitFDef : {auto oft : Ref OutfileText Output}
        -> {auto il : Ref IndentLevel Nat}
        -> (funcName:Name)
        -> (arglist:List (String, String, CFType))
        -> Core ()
emitFDef funcName [] = emit EmptyFC $ "Value *" ++ cName funcName ++ "(void)"
emitFDef funcName ((varType, varName, varCFType) :: xs) = do
    emit EmptyFC $ "Value *" ++ cName funcName
    emit EmptyFC "("
    increaseIndentation
    emit EmptyFC $ "  Value *" ++ varName
    traverse_ (\(varType, varName, varCFType) => emit EmptyFC $ ", Value *" ++ varName) xs
    decreaseIndentation
    emit EmptyFC ")"

-- Generic C parameter or RefC specific parameter
data CLang = CLangC | CLangRefC

extractValue : (cLang : CLang) -> (cfType:CFType) -> (varName:String) -> String
extractValue _ CFUnit           varName = "void"
extractValue _ CFInt            varName = "((Value_Int64*)" ++ varName ++ ")->i64"
extractValue _ CFInt8           varName = "((Value_Int8*)" ++ varName ++ ")->i8"
extractValue _ CFInt16          varName = "((Value_Int16*)" ++ varName ++ ")->i16"
extractValue _ CFInt32          varName = "((Value_Int32*)" ++ varName ++ ")->i32"
extractValue _ CFInt64          varName = "((Value_Int64*)" ++ varName ++ ")->i64"
extractValue _ CFUnsigned8      varName = "((Value_Bits8*)" ++ varName ++ ")->ui8"
extractValue _ CFUnsigned16     varName = "((Value_Bits16*)" ++ varName ++ ")->ui16"
extractValue _ CFUnsigned32     varName = "((Value_Bits32*)" ++ varName ++ ")->ui32"
extractValue _ CFUnsigned64     varName = "((Value_Bits64*)" ++ varName ++ ")->ui64"
extractValue _ CFString         varName = "((Value_String*)" ++ varName ++ ")->str"
extractValue _ CFDouble         varName = "((Value_Double*)" ++ varName ++ ")->d"
extractValue _ CFChar           varName = "((Value_Char*)" ++ varName ++ ")->c"
extractValue _ CFPtr            varName = "((Value_Pointer*)" ++ varName ++ ")->p"
extractValue _ CFGCPtr          varName = "((Value_GCPointer*)" ++ varName ++ ")->p->p"
extractValue CLangC    CFBuffer varName = "((Value_Buffer*)" ++ varName ++ ")->buffer->data"
extractValue CLangRefC CFBuffer varName = "((Value_Buffer*)" ++ varName ++ ")->buffer"
extractValue _ CFWorld          varName = "(Value_World*)" ++ varName
extractValue _ (CFFun x y)      varName = "(Value_Closure*)" ++ varName
extractValue c (CFIORes x)      varName = extractValue c x varName
extractValue _ (CFStruct x xs)  varName = assert_total $ idris_crash ("INTERNAL ERROR: Struct access not implemented: " ++ varName)
-- not really total but this way this internal error does not contaminate everything else
extractValue _ (CFUser x xs)    varName = "(Value*)" ++ varName
extractValue _ n _ = assert_total $ idris_crash ("INTERNAL ERROR: Unknonw FFI type in C backend: " ++ show n)

packCFType : (cfType:CFType) -> (varName:String) -> String
packCFType CFUnit          varName = "NULL"
packCFType CFInt           varName = "makeInt64(" ++ varName ++ ")"
packCFType CFInt8          varName = "makeInt8(" ++ varName ++ ")"
packCFType CFInt16         varName = "makeInt16(" ++ varName ++ ")"
packCFType CFInt32         varName = "makeInt32(" ++ varName ++ ")"
packCFType CFInt64         varName = "makeInt64(" ++ varName ++ ")"
packCFType CFUnsigned64    varName = "makeBits64(" ++ varName ++ ")"
packCFType CFUnsigned32    varName = "makeBits32(" ++ varName ++ ")"
packCFType CFUnsigned16    varName = "makeBits16(" ++ varName ++ ")"
packCFType CFUnsigned8     varName = "makeBits8(" ++ varName ++ ")"
packCFType CFString        varName = "makeString(" ++ varName ++ ")"
packCFType CFDouble        varName = "makeDouble(" ++ varName ++ ")"
packCFType CFChar          varName = "makeChar(" ++ varName ++ ")"
packCFType CFPtr           varName = "makePointer(" ++ varName ++ ")"
packCFType CFGCPtr         varName = "makePointer(" ++ varName ++ ")"
packCFType CFBuffer        varName = "makeBuffer(" ++ varName ++ ")"
packCFType CFWorld         varName = "makeWorld(" ++ varName ++ ")"
packCFType (CFFun x y)     varName = "makeFunction(" ++ varName ++ ")"
packCFType (CFIORes x)     varName = packCFType x varName
packCFType (CFStruct x xs) varName = "makeStruct(" ++ varName ++ ")"
packCFType (CFUser x xs)   varName = varName
packCFType n _ = assert_total $ idris_crash ("INTERNAL ERROR: Unknonw FFI type in C backend: " ++ show n)

discardLastArgument : List ty -> List ty
discardLastArgument [] = []
discardLastArgument xs@(_ :: _) = init xs

additionalFFIStub : Name -> List CFType -> CFType -> String
additionalFFIStub name argTypes (CFIORes retType) = additionalFFIStub name (discardLastArgument argTypes) retType
additionalFFIStub name argTypes retType =
    cTypeOfCFType retType ++
    " (*" ++ cName name ++ ")(" ++
    (concat $ intersperse ", " $ map cTypeOfCFType argTypes) ++ ") = (void*)missing_ffi;\n"

createCFunctions : {auto c : Ref Ctxt Defs}
                -> {auto a : Ref ArgCounter Nat}
                -> {auto f : Ref FunctionDefinitions (List String)}
                -> {auto t : Ref TemporaryVariableTracker (List (List String))}
                -> {auto oft : Ref OutfileText Output}
                -> {auto il : Ref IndentLevel Nat}
                -> {auto h : Ref HeaderFiles (SortedSet String)}
                -> {default [] additionalFFILangs : List String}
                -> Name
                -> ANFDef
                -> Core ()
createCFunctions n (MkAFun args anf) = do
    fn <- functionDefSignature n args
    fn' <- functionDefSignatureArglist n
    otherDefs <- get FunctionDefinitions
    put FunctionDefinitions ((fn ++ ";\n") :: (fn' ++ ";\n") :: otherDefs)
    newTemporaryVariableLevel
    let argsNrs = getArgsNrList args Z
    emit EmptyFC fn
    emit EmptyFC "{"
    increaseIndentation
    assignment <- cStatementsFromANF anf
    emit EmptyFC $ "Value *returnValue = " ++ tailCall assignment ++ ";"
    freeTmpVars
    emit EmptyFC $ "return returnValue;"
    decreaseIndentation
    emit EmptyFC  "}\n"
    emit EmptyFC  ""
    emit EmptyFC fn'
    emit EmptyFC "{"
    increaseIndentation
    emit EmptyFC $ "return " ++ (cName !(getFullName n))
    increaseIndentation
    emit EmptyFC $ "("
    increaseIndentation
    let commaSepArglist = addCommaToList (map (\a => "arglist->args["++ show a ++"]") argsNrs)
    traverse_ (emit EmptyFC) commaSepArglist
    decreaseIndentation
    emit EmptyFC ");"
    decreaseIndentation
    decreaseIndentation
    emit EmptyFC  "}\n"
    emit EmptyFC  ""
    pure ()

createCFunctions n (MkACon tag arity nt) = do
  emit EmptyFC $ ( "// Constructor tag " ++ show tag ++ " arity " ++ show arity) -- Nothing to compile here

createCFunctions n (MkAForeign ccs fargs ret) = do
  case parseCC (additionalFFILangs ++ ["RefC", "C"]) ccs of
      Just (lang, fctForeignName :: extLibOpts) => do
          let cLang = if lang == "RefC"
                         then CLangRefC
                         else CLangC
          let isStandardFFI = Prelude.elem lang ["RefC", "C"]
          let fctName = if isStandardFFI
                           then UN $ Basic $ fctForeignName
                           else UN $ Basic $ lang ++ "_" ++ fctForeignName
          if isStandardFFI
             then case extLibOpts of
                      [lib, header] => addHeader header
                      _ => pure ()
             else emit EmptyFC $ additionalFFIStub fctName fargs ret
          otherDefs <- get FunctionDefinitions
          let fnDef = "Value *" ++ (cName n) ++ "(" ++ showSep ", " (replicate (length fargs) "Value *") ++ ");"
          fn_arglist <- functionDefSignatureArglist n
          put FunctionDefinitions ((fnDef ++ "\n") :: (fn_arglist ++ ";\n") :: otherDefs)
          typeVarNameArgList <- createFFIArgList fargs

          emit EmptyFC fn_arglist
          emit EmptyFC "{"
          increaseIndentation
          emit EmptyFC $ "return " ++ (cName n)
          increaseIndentation
          emit EmptyFC $ "("
          increaseIndentation
          let commaSepArglist = addCommaToList (map (\a => "arglist->args["++ show a ++"]") (getArgsNrList fargs Z))
          traverse_ (emit EmptyFC) commaSepArglist
          decreaseIndentation
          emit EmptyFC ");"
          decreaseIndentation
          decreaseIndentation
          emit EmptyFC  "}\n"
          emit EmptyFC  ""

          emitFDef n typeVarNameArgList
          emit EmptyFC "{"
          increaseIndentation
          emit EmptyFC $ " // ffi call to " ++ cName fctName
          case ret of
              CFIORes CFUnit => do
                  emit EmptyFC $ cName fctName
                              ++ "("
                              ++ showSep ", " (map (\(_, vn, vt) => extractValue cLang vt vn) (discardLastArgument typeVarNameArgList))
                              ++ ");"
                  emit EmptyFC "return NULL;"
              CFIORes ret => do
                  emit EmptyFC $ cTypeOfCFType ret ++ " retVal = " ++ cName fctName
                              ++ "("
                              ++ showSep ", " (map (\(_, vn, vt) => extractValue cLang vt vn) (discardLastArgument typeVarNameArgList))
                              ++ ");"
                  emit EmptyFC $ "return (Value*)" ++ packCFType ret "retVal" ++ ";"
              _ => do
                  emit EmptyFC $ cTypeOfCFType ret ++ " retVal = " ++ cName fctName
                              ++ "("
                              ++ showSep ", " (map (\(_, vn, vt) => extractValue cLang vt vn) typeVarNameArgList)
                              ++ ");"
                  emit EmptyFC $ "return (Value*)" ++ packCFType ret "retVal" ++ ";"

          decreaseIndentation
          emit EmptyFC "}"
      _ => assert_total $ idris_crash ("INTERNAL ERROR: FFI not found for " ++ cName n)
          -- not really total but this way this internal error does not contaminate everything else

createCFunctions n (MkAError exp) = assert_total $ idris_crash ("INTERNAL ERROR: Error with expression: " ++ show exp)
-- not really total but this way this internal error does not contaminate everything else

header : {auto c : Ref Ctxt Defs}
      -> {auto f : Ref FunctionDefinitions (List String)}
      -> {auto o : Ref OutfileText Output}
      -> {auto il : Ref IndentLevel Nat}
      -> {auto h : Ref HeaderFiles (SortedSet String)}
      -> Core ()
header = do
    let initLines = [ "#include <runtime.h>"
                    , "/* " ++ (generatedString "RefC") ++" */"]
    let headerFiles = Libraries.Data.SortedSet.toList !(get HeaderFiles)
    let headerLines = map (\h => "#include <" ++ h ++ ">\n") headerFiles
    fns <- get FunctionDefinitions
    update OutfileText (appendL (initLines ++ headerLines ++ ["\n// function definitions"] ++ fns))

footer : {auto il : Ref IndentLevel Nat}
      -> {auto f : Ref OutfileText Output}
      -> {auto h : Ref HeaderFiles (SortedSet String)}
      -> Core ()
footer = do
    emit EmptyFC ""
    emit EmptyFC " // main function"
    emit EmptyFC "int main(int argc, char *argv[])"
    emit EmptyFC "{"
    if contains "idris_support.h" !(get HeaderFiles)
       then emit EmptyFC "   idris2_setArgs(argc, argv);"
       else pure ()
    emit EmptyFC "   Value *mainExprVal = __mainExpression_0();"
    emit EmptyFC "   trampoline(mainExprVal);"
    emit EmptyFC "   return 0; // bye bye"
    emit EmptyFC "}"

export
executeExpr : Ref Ctxt Defs -> (execDir : String) -> ClosedTerm -> Core ()
executeExpr c _ tm
    = do coreLift_ $ putStrLn "Execute expression not yet implemented for refc"
         coreLift_ $ system "false"

export
generateCSourceFile : {auto c : Ref Ctxt Defs}
                   -> {default [] additionalFFILangs : List String}
                   -> List (Name, ANFDef)
                   -> (outn : String)
                   -> Core ()
generateCSourceFile defs outn =
  do _ <- newRef ArgCounter 0
     _ <- newRef FunctionDefinitions []
     _ <- newRef TemporaryVariableTracker []
     _ <- newRef OutfileText DList.Nil
     _ <- newRef HeaderFiles empty
     _ <- newRef IndentLevel 0
     traverse_ (uncurry $ createCFunctions {additionalFFILangs}) defs
     header -- added after the definition traversal in order to add all encountered function defintions
     footer
     fileContent <- get OutfileText
     let code = fastAppend (map (++ "\n") (reify fileContent))

     coreLift_ $ writeFile outn code
     log "compiler.refc" 10 $ "Generated C file " ++ outn

export
compileExpr : UsePhase
           -> Ref Ctxt Defs
           -> (tmpDir : String)
           -> (outputDir : String)
           -> ClosedTerm
           -> (outfile : String)
           -> Core (Maybe String)
compileExpr ANF c _ outputDir tm outfile =
  do let outn = outputDir </> outfile ++ ".c"
     let outobj = outputDir </> outfile ++ ".o"
     let outexec = outputDir </> outfile

     coreLift_ $ mkdirAll outputDir
     cdata <- getCompileData False ANF tm
     let defs = anf cdata

     generateCSourceFile defs outn
     Just _ <- compileCObjectFile outn outobj
       | Nothing => pure Nothing
     compileCFile outobj outexec

compileExpr _ _ _ _ _ _ = pure Nothing

export
codegenRefC : Codegen
codegenRefC = MkCG (compileExpr ANF) executeExpr Nothing Nothing


text:
module LightClick.Terms

import Data.Vect
import Data.Vect.Elem

import Toolkit.Data.DList
import Toolkit.Data.DList.DeBruijn
import Toolkit.Data.DVect
import Toolkit.Data.Location

import Language.SystemVerilog.Gates

import LightClick.Types
import LightClick.Error

%default total

namespace Context
   public export
   Context : Type
   Context = List (Pair String MTy)

   public export
   Index : Context -> Pair String MTy -> Type
   Index = DeBruijn.Index (Pair String MTy)

namespace Term

  public export
   data Term : (ctxt : Context) -> MTy -> Type where
      Ref : {label : String}
         -> {type  : MTy}
         -> (fc  : FileContext)
         -> (prf : Index ctxt (label,type))
         -> Term ctxt type

      Let : {typeE : MTy}
         -> (fc     : FileContext)
         -> (label  : String)
         -> (this   : Term ctxt typeE)
         -> (inThis : Term ((label,typeE)::ctxt) typeB)
         -> Term ctxt typeB

      Seq : {typeA,typeB : MTy} -> Term ctxt typeA -> Term ctxt typeB -> Term ctxt typeB

      DataLogic : (fc : FileContext) -> Term ctxt DATA

      DataArray : (fc : FileContext) -> (type : Term ctxt DATA) -> (size : Nat) -> Term ctxt DATA

      DataStruct : {n : Nat}
                -> (fc : FileContext)
                -> (xs : Vect (S n) (Pair String (Term ctxt DATA)))
                -> Term ctxt DATA
      DataUnion : {n : Nat}
               -> (fc : FileContext)
               -> (xs : Vect (S n) (Pair String (Term ctxt DATA)))
               -> Term ctxt DATA

      Port : (fc : FileContext)
          -> (l  : String)
          -> (d  : Direction)
          -> (s  : Sensitivity)
          -> (w  : Wire)
          -> (i  : Term ctxt DATA)
          -> Term ctxt (PORT l)

      Module : {n : Nat}
            -> {names : Vect (S n) String}
            -> (fc : FileContext)
            -> (ports : DVect String
                              (\s => Term ctxt (PORT s))
                              (S n)
                              names)
            -> Term ctxt (MODULE names)

      Index : {label : String}
           -> (fc : FileContext)
           -> (mod : Term ctxt (MODULE names))
           -> Elem label names
           -> Term ctxt (PORT label)

      Connect : (fc    : FileContext)
             -> (left  : Term ctxt (PORT a))
             -> (right : Term ctxt (PORT b))
                      -> Term ctxt CONN

      FanOut : {n      : Nat}
            -> {names  : Vect (S (S n)) String}
            -> (fc     : FileContext)
            -> (input  : Term ctxt (PORT s))
            -> (fan    : DVect String
                               (\s => Term ctxt (PORT s))
                               (S (S n))
                               names)
                      -> Term ctxt CONN

      Mux : {n : Nat}
         -> {c,o : String}
         -> {names : Vect (S (S n)) String}
         -> (fc     : FileContext)
         -> (fan : DVect String
                         (\s => Term ctxt (PORT s))
                         (S (S n))
                         names)
         -> (ctrl   : Term ctxt (PORT c))
         -> (output : Term ctxt (PORT o))
                   -> Term ctxt CONN

      NOT : {a,b : String}
         -> (fc    : FileContext)
         -> (left  : Term ctxt (PORT a))
         -> (right : Term ctxt (PORT b))
                  -> Term ctxt GATE

      GATE : {n : Nat}
          -> {o : String}
          -> {names : Vect (S (S n)) String}
          -> (fc    : FileContext)
          -> (ty    : TyGateComb)
          -> (fan   : DVect String
                            (\s => Term ctxt (PORT s))
                            (S (S n))
                            names)
          -> (output : Term ctxt (PORT o))
                    -> Term ctxt GATE

      End : Term ctxt UNIT

export
getFC : Term ctxt type -> Maybe FileContext
getFC (Ref x y) = Just x
getFC (Let x label this inThis) = Just x
getFC (Seq x y) = Nothing
getFC (DataLogic fc) = Just fc
getFC (DataArray fc type size) = Just fc
getFC (DataStruct fc xs) = Just fc
getFC (DataUnion fc xs) = Just fc
getFC (Port fc l d s w i) = Just fc
getFC (Module fc ports) = Just fc
getFC (Index fc mod x) = Just fc
getFC (Connect fc left right) = Just fc
getFC (FanOut fc input fanOut) = Just fc
getFC (Mux fc fanIn ctrl output) = Just fc
getFC (NOT fc _ _ ) = Just fc
getFC (GATE fc _ _ _) = Just fc
getFC End = Nothing

namespace ErrorFul
 export
 getFC : Term ctxt type -> Either LightClick.Error FileContext
 getFC term =
   case getFC term of
     Nothing => Left (NotSupposedToHappen $ Just "getFC")
     Just fc => Right fc

-- [ EOF ]

ext: idr

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Graphics.Util.Mesh

import Data.Vect

%access public export
%default total
Vec2 : Type
Vec2 = Vect 2 Double

Vec3 : Type
Vec3 = Vect 3 Double

Vec4 : Type
Vec4 = Vect 4 Double

||| a data type for meshes.
|||
||| a mesh is a collection of positions, of UV texture coordinates, vertex normals and indices
|||
data Mesh : Type where
  UvMesh :  (positions: Vect n Vec3)
         -> (normals: Vect n Vec3)
         -> (uvs: Vect n Vec2)
         -> (indices: List Int)
         -> Mesh

positions : Mesh -> List Vec3
positions (UvMesh p _ _ _) = toList p

indices : Mesh -> List Int
indices (UvMesh _ _ _ xs) = xs

max_stars_repo_name: spearman/gl-idris

max_issues_repo_name: spearman/gl-idris

max_forks_repo_name: spearman/gl-idris


text:
module CommandLineParser

import Lightyear
import Lightyear.Combinators
import Lightyear.Core
import Lightyear.Char
import Lightyear.Position
import Lightyear.Strings

%access public export

implementation Stream String (List String) where
    uncons Nil       = Nothing
    uncons (x :: xs) = Just (x, xs)
    updatePos tw pos tk = (Lightyear.Position.Generic.increment tw pos ' ', pos)

||| RK: Taken from Lightyear.
||| Run some parser `p` until the second parser is encountered,
||| collecting a list of success for `p`, and the result of the second
||| parser is dropped.
|||
||| Primarily useful for collecting single line comments and other
||| similar verbatim environments.
manyTill : Monad m => ParserT str m a
                   -> ParserT str m b
                   -> ParserT str m (List a)
manyTill p end = scan
  where
    scan : Monad m => ParserT str m (List a)
    scan = do { end; pure List.Nil } <|>
           do { x <- p; xs <- scan; pure (x::xs)}

||| A command line key
key : Monad m => String -> ParserT (List String) m String
key s = satisfy (== s)

||| A typed value with given string parser
value : Monad m => Parser a -> ParserT (List String) m a
value valueParser = (do
    t <- anyToken
    forward $ parse valueParser t) <?> "a typed value" where
        forward (Left error)   = fail error
        forward (Right result) = pure result

||| Run a parser against an input string assuming that tab-widths are
||| eight characters in length.
parseList : ParserT (List String) (Either String) a -> List String -> Either String a
parseList parser args = do
    state <- execParserT parser (ST args (MkPos Nothing 0 0) 8)
    case state of
        (MkReply _ (Success result)) => Right result
        (MkReply _ (Failure error))  => Left $ concat $ intersperse "\n" $ map display error


text:
module WebServer.Requests

import WebServer.JS

%default total
%access public export

data RequestMethod
  = Delete
  | Get
  | Head
  | Options
  | Post
  | Put

Eq RequestMethod where
  (==) Delete Delete = True
  (==) Get Get = True
  (==) Head Head = True
  (==) Options Options = True
  (==) Post Post = True
  (==) Put Put = True
  (==) _ _ = False

Show RequestMethod where
  show Delete = "DELETE"
  show Get = "GET"
  show Head = "HEAD"
  show Options = "OPTIONS"
  show Post = "POST"
  show Put = "PUT"

Ord RequestMethod where
  compare x y = compare (show x) (show y)

record Request where
  constructor MkRequest
  method : RequestMethod
  path : String
%name Request req

data ContentTypeValue
  = TextHtmlUtf8

data CacheControlValue
  = NoCache

contentType : (filename : String) -> String
contentType filename =
  case reverse (split (== '.') filename) of
    ("asc" :: _) =>
      "application/octet-stream"
    ("css" :: _) =>
      "text/css"
    ("js" :: _) =>
      "application/javascript"
    ("pdf" :: _) =>
      "application/pdf"
    _ =>
      "text/html; charset=utf-8"

mutual
  data Header
    = Custom String String
    | ContentLengthFor String
    | ContentType ContentTypeValue
    | ContentTypeFor String
    | CacheControl CacheControlValue
    | Location String

  parseHeader : Header -> JS_IO (String, String)
  parseHeader (Custom k v) =
    pure (k, v)
  parseHeader (ContentLengthFor body) =
    pure ("Content-Length", show !(byteLength body))
  parseHeader (ContentTypeFor s) =
    pure ("Content-Type", contentType s)
  parseHeader (ContentType TextHtmlUtf8) =
    pure ("Content-Type", contentType "html")
  parseHeader (CacheControl NoCache) =
    pure ("Cache-Control", "no-cache")
  parseHeader (Location uri) =
    pure ("Location", uri)

data Code
  = OK
  | Created
  | NotFound

Cast Code Int where
  cast OK = 200
  cast Created = 201
  cast NotFound = 404

record Response where
  constructor MkResponse
  code : Code
  body : String
  headers : List Header
%name Response res

requestFromRaw : (meth : String) -> (url : String) -> Request
requestFromRaw "DELETE"  = MkRequest Delete
requestFromRaw "GET"     = MkRequest Get
requestFromRaw "HEAD"    = MkRequest Head
requestFromRaw "OPTIONS" = MkRequest Options
requestFromRaw "POST"    = MkRequest Post
requestFromRaw "PUT"     = MkRequest Put
requestFromRaw _         = MkRequest Head

RequestHandler : Type
RequestHandler = Request -> Response

-- Local Variables:
-- idris-load-packages: ("contrib")
-- End:

max_stars_repo_name: camelpunch/idris-web-server

max_issues_repo_name: camelpunch/idris-web-server

max_forks_repo_name: camelpunch/idris-web-server


text:
import System

import System.Concurrency.Pipe

{-- TODO: REWRITE EVERYTHING!
senderError : (senderID : Int) -> (errMsg : String) -> IO ()
senderError senderID errMsg =
  putStrLn $ "S" ++ (show senderID) ++ ": ERROR: " ++ errMsg

receiverError : (receiverID : Int) -> (errMsg : String) -> IO ()
receiverError receiverID errMsg =
  putStrLn $ "R" ++ (show receiverID) ++ ": ERROR: " ++ errMsg

testReceiveEmpty : IO ()
testReceiveEmpty =
  do putStrLn "--- Begin testReceiveEmpty ---"
     cRef <- makeChannel
     chan <- readIORef cRef
     rawMsg <- receive chan
     case rawMsg of
          Nothing => putStrLn "Success."
          Just m =>
             putStrLn "ERROR: Got a message from the void"
     putStrLn "---  End testReceiveEmpty  ---\n"

testSendReceive_SENDER : (chan : Channel) -> IO ()
testSendReceive_SENDER chan =
  do sendAndSignal chan (prepare "Hello")
     putStrLn "S1: Sent 'Hello' and signalled"

testSendReceive_RECEIVER : (chan : Channel) -> IO ()
testSendReceive_RECEIVER chan =
  do rawMsg <- receive chan
     case rawMsg of
          Nothing => receiverError 1 "Received Nothing"
          Just msg => case unsafeOpen msg String of
                           "Hello" => putStrLn "R1: Success."
                           _ => receiverError 1 "Didn't receive 'Hello'"

testSendReceive : IO ()
testSendReceive =
  do putStrLn "--- Begin testSendReceive ---"
     cRef <- makeChannel
     chan_SENDER <- makeSender cRef
     chan_RECEIVER <- makeReceiver cRef
     let sender = testSendReceive_SENDER chan_SENDER
     let receiver = testSendReceive_RECEIVER chan_RECEIVER
     pid_SENDER <- fork sender
     sleep 1
     pid_RECEIVER <- fork receiver
     sleep 1
     putStrLn "---  End testSendReceive  ---\n"

testReceiveReply_SENDER : (chan : Channel) -> IO ()
testReceiveReply_SENDER chan =
  do rawReply <- receive chan
     case rawReply of
          Nothing => senderError 1 "Received Nothing as reply"
          Just msg => case unsafeOpen msg String of
                           "World" => putStrLn "S1: Success."
                           _ => senderError 1 "Didn't receive 'World'"

testReceiveReply_RECEIVER : (chan : Channel) -> IO ()
testReceiveReply_RECEIVER chan =
  do sendAndSignal chan (prepare "World")
     putStrLn "R1: Sent 'World' and signalled"

testReceiveReply : IO ()
testReceiveReply =
  do putStrLn "--- Begin testReceiveReply ---"
     cRef <- makeChannel
     chan_SENDER <- makeSender cRef
     chan_RECEIVER <- makeReceiver cRef
     let sender = testReceiveReply_SENDER chan_SENDER
     let receiver = testReceiveReply_RECEIVER chan_RECEIVER
     -- fork in reverse order for minimal risk of runtime disruption
     pid_RECEIVER <- fork receiver
     sleep 1
     pid_SENDER <- fork sender
     sleep 1
     putStrLn "---  End testReceiveReply  ---\n"

testSendSignalAwait_SENDER : (chan : Channel) -> IO ()
testSendSignalAwait_SENDER chan =
  do sendAndSignal chan (prepare "Hello")
     putStrLn "S1: Sent 'Hello' and signalled"

testSendSignalAwait_RECEIVER : (chan : Channel) -> IO ()
testSendSignalAwait_RECEIVER chan =
  do rawMsg <- await chan
     case rawMsg of
          Nothing => receiverError 1 "Await got Nothing"
          Just msg => case unsafeOpen msg String of
                           "Hello" => putStrLn "R1: Success."
                           _ => receiverError 1 "Await didn't get 'Hello'"

testSendSignalAwait : IO ()
testSendSignalAwait =
  do putStrLn "--- Begin testSendSignalAwait ---"
     cRef <- makeChannel
     chan_SENDER <- makeSender cRef
     chan_RECEIVER <- makeReceiver cRef
     let sender = testSendSignalAwait_SENDER chan_SENDER
     let receiver = testSendSignalAwait_RECEIVER chan_RECEIVER
     pid_SENDER <- fork sender
     pid_RECEIVER <- fork receiver
     sleep 1
     putStrLn "---  End testSendSignalAwait  ---\n"

testSendSignalAwait2_SENDER : (chan : Channel) -> IO ()
testSendSignalAwait2_SENDER chan =
  do sleep 1
     sendAndSignal chan (prepare "Hello")
     putStrLn "S1: Sent 'Hello' and signalled"

testSendSignalAwait2_RECEIVER : (chan : Channel) -> IO ()
testSendSignalAwait2_RECEIVER chan =
  do rawMsg <- await chan
     case rawMsg of
          Nothing => receiverError 1 "Await got Nothing"
          Just msg => case unsafeOpen msg String of
                           "Hello" => putStrLn "R1: Success."
                           _ => receiverError 1 "Got something weird"

-- test that `await` works, as long as there is some update at some point
testSendSignalAwait2 : IO ()
testSendSignalAwait2 =
  do putStrLn "--- Begin testSendSignalAwait2 ---"
     cRef <- makeChannel
     chan_SENDER <- makeSender cRef
     chan_RECEIVER <- makeReceiver cRef
     let sender = testSendSignalAwait2_SENDER chan_SENDER
     let receiver = testSendSignalAwait2_RECEIVER chan_RECEIVER
     pid_SENDER <- fork sender
     pid_RECEIVER <- fork receiver
     sleep 2
     putStrLn "---  End testSendSignalAwait2  ---\n"

testAwaitTimedOut_RECEIVER : (chan : Channel) -> IO ()
testAwaitTimedOut_RECEIVER chan =
  do timeoutRes <- awaitTimeout chan 500000
     case timeoutRes of
          TimedOut => putStrLn "R1: Success."
          Succeeded msg => receiverError 1 "Got a message from the void"

testAwaitTimedOut : IO ()
testAwaitTimedOut =
  do putStrLn "--- Begin testAwaitTimedOut ---"
     cRef <- makeChannel
     chan_RECEIVER <- makeReceiver cRef
     let receiver = testAwaitTimedOut_RECEIVER chan_RECEIVER
     pid_RECEIVER <- fork receiver
     sleep 1
     putStrLn "---  End testAwaitTimedOut  ---\n"

testSendSignalAwaitTimedOut_SENDER : (chan : Channel) -> IO ()
testSendSignalAwaitTimedOut_SENDER chan =
  do sendAndSignal chan (prepare "Hello")
     putStrLn "S1: Sent 'Hello' and signalled"

testSendSignalAwaitTimedOut_RECEIVER : (chan : Channel) -> IO ()
testSendSignalAwaitTimedOut_RECEIVER chan =
  do timeoutRes <- awaitTimeout chan 500000
     case timeoutRes of
          TimedOut => receiverError 1 "Timed out"
          Succeeded rawMsg => case unsafeOpen rawMsg String of
                                   "Hello" => putStrLn "R1: Success."
                                   _ => receiverError 1 "Didn't get 'Hello'"

testSendSignalAwaitTimedOut : IO ()
testSendSignalAwaitTimedOut =
  do putStrLn "--- Begin testSendSignalAwaitTimedOut ---"
     cRef <- makeChannel
     chan_SENDER <- makeSender cRef
     chan_RECEIVER <- makeReceiver cRef
     let sender = testSendSignalAwaitTimedOut_SENDER chan_SENDER
     let receiver = testSendSignalAwaitTimedOut_RECEIVER chan_RECEIVER
     pid_SENDER <- fork sender
     pid_RECEIVER <- fork receiver
     sleep 1
     putStrLn "---  End testSendSignalAwaitTimedOut  ---\n"

testSendSignalAwaitTooSlow_SENDER : (chan : Channel) -> IO ()
testSendSignalAwaitTooSlow_SENDER chan =
  do sleep 1
     sendAndSignal chan (prepare "Sorry I'm late")
     putStrLn "S1: After 1 second, sent \"Sorry I'm late\" and signalled"

testSendSignalAwaitTooSlow_RECEIVER : (chan : Channel) -> IO ()
testSendSignalAwaitTooSlow_RECEIVER chan =
  do timeoutRes <- awaitTimeout chan 500000
     case timeoutRes of
          TimedOut => putStrLn "R1: Success."
          Succeeded rawMsg => receiverError 1 "Somehow got a message."

testSendSignalAwaitTooSlow : IO ()
testSendSignalAwaitTooSlow =
  do putStrLn "--- Begin testSendSignalAwaitTooSlow ---"
     cRef <- makeChannel
     chan_SENDER <- makeSender cRef
     chan_RECEIVER <- makeReceiver cRef
     let sender = testSendSignalAwaitTooSlow_SENDER chan_SENDER
     let receiver = testSendSignalAwaitTooSlow_RECEIVER chan_RECEIVER
     pid_SENDER <- fork sender
     pid_RECEIVER <- fork receiver
     sleep 2
     putStrLn "---  End testSendSignalAwaitTooSlow  ---\n"

testSendSignalPeek_SENDER : (chan : Channel) -> IO ()
testSendSignalPeek_SENDER chan =
  do sendAndSignal chan (prepare "Hello")
     putStrLn "S1: Sent 'Hello' and signalled"

testSendSignalPeek_RECEIVER : (chan : Channel) -> IO ()
testSendSignalPeek_RECEIVER chan =
  do maybePeek <- peek chan
     case maybePeek of
          Nothing => receiverError 1 "Peek got Nothing"
          Just rawMsg => case unsafeOpen rawMsg String of
                              -- `peek` internals, i.e. msg isn't accidentally
                              -- dequeued, tested in MTTestQueues.idr
                              "Hello" => putStrLn "R1: Success."
                              _ => receiverError 1 "Did not get 'Hello'"

testSendSignalPeek : IO ()
testSendSignalPeek =
  do putStrLn "--- Begin testSendSignalPeek ---"
     cRef <- makeChannel
     chan_SENDER <- makeSender cRef
     chan_RECEIVER <- makeReceiver cRef
     let sender = testSendSignalPeek_SENDER chan_SENDER
     let receiver = testSendSignalPeek_RECEIVER chan_RECEIVER
     pid_SENDER <- fork sender
     sleep 1
     pid_RECEIVER <- fork receiver
     sleep 1
     putStrLn "---  End testSendSignalPeek  ---\n"

testSendSignalSpy_SENDER : (chan : Channel) -> IO ()
testSendSignalSpy_SENDER chan =
  do sendAndSignal chan (prepare "Hello")
     putStrLn "S1: Sent 'Hello' and signalled"

testSendSignalSpy_RECEIVER : (chan : Channel) -> IO ()
testSendSignalSpy_RECEIVER chan =
  do rawMsg <- spy chan
     case rawMsg of
          Nothing => receiverError 1 "Spy got Nothing"
          Just msg => case unsafeOpen msg String of
                           "Hello" => putStrLn "R1: Success."
                           _ => receiverError 1 "Spy didn't get 'Hello'"

testSendSignalSpy : IO ()
testSendSignalSpy =
  do putStrLn "--- Begin testSendSignalSpy ---"
     cRef <- makeChannel
     chan_SENDER <- makeSender cRef
     chan_RECEIVER <- makeReceiver cRef
     let sender = testSendSignalSpy_SENDER chan_SENDER
     let receiver = testSendSignalSpy_RECEIVER chan_RECEIVER
     pid_SENDER <- fork sender
     pid_RECEIVER <- fork receiver
     sleep 1
     putStrLn "---  End testSendSignalSpy  ---\n"

testSendSignalSpy2_SENDER : (chan : Channel) -> IO ()
testSendSignalSpy2_SENDER chan =
  do sleep 1
     sendAndSignal chan (prepare "Hello")
     putStrLn "S1: Sent 'Hello' and signalled"

testSendSignalSpy2_RECEIVER : (chan : Channel) -> IO ()
testSendSignalSpy2_RECEIVER chan =
  do maybeMsg <- spy chan
     case maybeMsg of
          Nothing => receiverError 1 "Spy got Nothing"
          Just msg => case unsafeOpen msg String of
                           "Hello" => putStrLn "R1: Success."
                           _ => receiverError 1 "Spy didn't get 'Hello'"

testSendSignalSpy2 : IO ()
testSendSignalSpy2 =
  do putStrLn "--- Begin testSendSignalSpy2 ---"
     cRef <- makeChannel
     chan_SENDER <- makeSender cRef
     chan_RECEIVER <- makeReceiver cRef
     let sender = testSendSignalSpy2_SENDER chan_SENDER
     let receiver = testSendSignalSpy2_RECEIVER chan_RECEIVER
     pid_SENDER <- fork sender
     pid_RECEIVER <- fork receiver
     sleep 2
     putStrLn "---  End testSendSignalSpy2  ---\n"

testSendSignalSpyTimedOut_RECEIVER : (chan : Channel) -> IO ()
testSendSignalSpyTimedOut_RECEIVER chan =
  do timeoutRes <- spyTimeout chan 500000
     case timeoutRes of
          TimedOut => putStrLn "R1: Success."
          Succeeded msg => receiverError 1 "Spy got a message from the void"

testSendSignalSpyTimedOut : IO ()
testSendSignalSpyTimedOut =
  do putStrLn "--- Begin testSendSignalSpyTimedOut ---"
     cRef <- makeChannel
     chan_RECEIVER <- makeReceiver cRef
     let receiver = testSendSignalSpyTimedOut_RECEIVER chan_RECEIVER
     pid_RECEIVER <- fork receiver
     sleep 1
     putStrLn "---  End testSendSignalSpyTimedOut  ---\n"

testSendSignalSpyTooSlow_SENDER : (chan : Channel) -> IO ()
testSendSignalSpyTooSlow_SENDER chan =
  do sleep 1
     sendAndSignal chan (prepare "I'm late! I'm late!")
     putStrLn "S1: After 1 second, sent a message and signalled"

testSendSignalSpyTooSlow_RECEIVER : (chan : Channel) -> IO ()
testSendSignalSpyTooSlow_RECEIVER chan =
  do timeoutRes <- spyTimeout chan 500000
     case timeoutRes of
          TimedOut => putStrLn "R1: Success."
          Succeeded rawMsg => receiverError 1 "Got a message despite impatience"

testSendSignalSpyTooSlow : IO ()
testSendSignalSpyTooSlow =
  do putStrLn "--- Begin testSendSignalSpyTooSlow ---"
     cRef <- makeChannel
     chan_SENDER <- makeSender cRef
     chan_RECEIVER <- makeReceiver cRef
     let sender = testSendSignalSpyTooSlow_SENDER chan_SENDER
     let receiver = testSendSignalSpyTooSlow_RECEIVER chan_RECEIVER
     pid_SENDER <- fork sender
     pid_RECEIVER <- fork receiver
     sleep 2
     putStrLn "---  End testSendSignalSpyTooSlow  ---\n"

runAll : IO ()
runAll = do testReceiveEmpty
            testSendReceive
            testReceiveReply
            testSendSignalAwait
            testSendSignalAwait2
            testAwaitTimedOut
            testSendSignalAwaitTimedOut
            testSendSignalAwaitTooSlow
            testSendSignalPeek
            testSendSignalSpy
            testSendSignalSpy2
            testSendSignalSpyTimedOut
            testSendSignalSpyTooSlow

main : IO ()
main = runAll
-- }


text:
module Chapter2

import Data.List
import Data.Nat

%default total

-- Exercise 2.2

export
add_assoc : (n, m, k : Nat) -> n + (m + k) = (n + m) + k
add_assoc Z     m k = Refl
add_assoc (S n) m k = rewrite add_assoc n m k in Refl

add_z_right : (n : Nat) -> n + 0 = n
add_z_right Z     = Refl
add_z_right (S n) = rewrite add_z_right n in Refl

add_s_right : (n, m : Nat) -> n + S m = S (n + m)
add_s_right Z     m = Refl
add_s_right (S n) m = rewrite add_s_right n m in Refl

export
add_comm : (n, m : Nat) -> n + m = m + n
add_comm Z     m = rewrite add_z_right m in Refl
add_comm (S n) m = rewrite add_comm n m in
                   rewrite add_s_right m n in
                   Refl

public export
double : Nat -> Nat
double Z     = Z
double (S n) = S . S $ double n

export
double_is_add : (m : Nat) -> double m = m + m
double_is_add Z     = Refl
double_is_add (S m) = rewrite double_is_add m in
                      rewrite add_s_right m m in
                      Refl

-- Exercise 2.3

public export
count : Eq a => a -> List a -> Nat
count _ []      = 0
count x (y::xs) = if x == y
                    then S $ count x xs
                    else count x xs

export
count_le_length : Eq a => (x : a) -> (xs : List a) -> count x xs `LTE` length xs
count_le_length x []      = LTEZero
count_le_length x (y::xs) with (x == y)
  count_le_length x (_::xs) | True  = LTESucc $ count_le_length x xs
  count_le_length x (_::xs) | False = lteSuccRight $ count_le_length x xs

-- Exercise 2.4

public export
snoc : List a -> a -> List a
snoc [] n      = [n]
snoc (x::xs) n = x :: Chapter2.snoc xs n

public export
reverse : List a -> List a
reverse []      = []
reverse (x::xs) = Chapter2.snoc (Chapter2.reverse xs) x

reverse_of_snoc : (xs : List a) -> (x : a) -> Chapter2.reverse (Chapter2.snoc xs x) = x :: Chapter2.reverse xs
reverse_of_snoc [] _      = Refl
reverse_of_snoc (_::xs) n = rewrite reverse_of_snoc xs n in Refl

export
double_reverse : (xs : List a) -> Chapter2.reverse (Chapter2.reverse xs) = xs
double_reverse []      = Refl
double_reverse (x::xs) = rewrite reverse_of_snoc (Chapter2.reverse xs) x in
                         rewrite double_reverse xs in
                         Refl

-- Exercise 2.5

public export
sum_upto : Nat -> Nat
sum_upto Z     = Z
sum_upto (S n) = S n + sum_upto n

export
half : Nat -> Nat
half Z         = Z
half (S Z)     = Z
half (S (S n)) = S (half n)

half_of_add : (a : Nat) -> (n : Nat) -> a + half n = half (a + (a + n))
half_of_add Z     n = Refl
half_of_add (S k) n = rewrite sym $ plusSuccRightSucc k (k + n) in
                      rewrite half_of_add k n in
                      Refl

-- Contents of standard `Nat`'s `div` are not enclosed (somewhy), that's why I defined my own recusrive `half`.
public export
sum_upto_formula : (n : Nat) -> sum_upto n = half (n * (n + 1))
sum_upto_formula Z     = Refl
sum_upto_formula (S k) = rewrite sum_upto_formula k in
                         rewrite plusCommutative k 1 in
                         rewrite multRightSuccPlus k (S k) in
                         rewrite half_of_add k (k * S k) in
                         Refl

-- Exercise 2.6

public export
data Tree a = Tip
            | Node (Tree a) a (Tree a)

public export
contents : Tree a -> List a
contents Tip          = []
contents (Node l x r) = x :: contents l ++ contents r

public export
sum_tree : Tree Nat -> Nat
sum_tree Tip          = 0
sum_tree (Node l x r) = x + sum_tree l + sum_tree r

-- We could do this for `Num a => ... List a` asap `Num` would contain the monoid rules (zero elimintation, etc.)
sum_of_concat : (xs, ys : List Nat) -> sum (xs ++ ys) = sum xs + sum ys
sum_of_concat [] ys = rewrite plusZeroLeftNeutral (sum ys) in Refl
sum_of_concat (x::xs) ys = rewrite sum_of_concat xs ys in
                           rewrite plusAssociative x (sum xs) (sum ys) in
                           Refl

export
sum_tree_thru_contents : (tr : Tree Nat) -> sum_tree tr = sum (contents tr)
sum_tree_thru_contents Tip          = Refl
sum_tree_thru_contents (Node l x r) = rewrite sum_tree_thru_contents l in
                                      rewrite sum_tree_thru_contents r in
                                      rewrite sum_of_concat (contents l) (contents r) in
                                      rewrite plusAssociative x (sum $ contents l) (sum $ contents r) in
                                      Refl

-- Exercise 2.7

namespace Ex_2_7

  public export
  data Tree2 a = Tip
               | Leaf a
               | Node (Tree2 a) a (Tree2 a)

public export
mirror : Tree2 a -> Tree2 a
mirror n@Tip        = n
mirror n@(Leaf _)   = n
mirror (Node l x r) = Node (mirror r) x (mirror l)

mirror_of_mirror : (t : Tree2 a) -> mirror (mirror t) = t
mirror_of_mirror Tip          = Refl
mirror_of_mirror (Leaf _)     = Refl
mirror_of_mirror (Node l _ r) = rewrite mirror_of_mirror l in
                                rewrite mirror_of_mirror r in
                                Refl

public export
pre_order : Tree2 a -> List a
pre_order Tip          = []
pre_order (Leaf x)     = [x]
pre_order (Node l x r) = x :: pre_order l ++ pre_order r

public export
post_order : Tree2 a -> List a
post_order Tip          = []
post_order (Leaf x)     = [x]
post_order (Node l x r) = post_order l ++ post_order r ++ [x]

export
pre_n_post_orders : (t : Tree2 a) -> pre_order (mirror t) = Data.List.reverse (post_order t)
pre_n_post_orders Tip          = Refl
pre_n_post_orders (Leaf _)     = Refl
pre_n_post_orders (Node l x r) = rewrite pre_n_post_orders l in
                                 rewrite pre_n_post_orders r in
                                 rewrite sym $ revAppend (post_order l) (post_order r ++ [x]) in
                                 rewrite sym $ revAppend (post_order r) [x] in
                                 Refl

-- Exercise 2.8

public export
intersperse : a -> List a -> List a
intersperse _ []            = []
intersperse _ [x]           = [x]
intersperse s (x::r@(_::_)) = x :: s :: Chapter2.intersperse s r
-- The line above can be written simpler, as `intersperse s (x::y::ys) = x :: s :: Chapter2.intersperse s (y::ys)`
--   but actual definitely does not rebuild the `r`, but simpler one may rebuild this in runtime (thus, less may be effective).

export
intersperse_n_map : (s : a) -> (xs : List a) -> (f : a -> a) -> map f (Chapter2.intersperse s xs) = Chapter2.intersperse (f s) (map f xs)
intersperse_n_map s []            f = Refl
intersperse_n_map s [x]           f = Refl
intersperse_n_map s (x::r@(_::_)) f = rewrite intersperse_n_map s r f in Refl

-- Exercise 2.9

public export
itadd : Nat -> Nat -> Nat
itadd Z     m = m
itadd (S n) m = itadd n (S m)

export
itadd_is_add : (n, m : Nat) -> itadd n m = n + m
itadd_is_add Z     m = Refl
itadd_is_add (S n) m = rewrite itadd_is_add n (S m) in
                       rewrite plusSuccRightSucc n m in
                       Refl

-- Exercise 2.10

namespace Ex_2_10

  public export
  data Tree0 = Tip | Node Tree0 Tree0

public export
nodes : Tree0 -> Nat
nodes Tip        = 1
nodes (Node l r) = nodes l + nodes r + 1

public export
explode : Nat -> Tree0 -> Tree0
explode Z     t = t
explode (S n) t = explode n $ Node t t

export
explode_in_nodes : (n : Nat) -> (t : Tree0) -> nodes (explode n t) = ((2 `power` n) * nodes t + (2 `power` n)) `minus` 1
explode_in_nodes Z t = rewrite plusZeroRightNeutral $ nodes t in
                       rewrite plusCommutative (nodes t) 1 in
                       rewrite minusZeroRight $ nodes t in
                       Refl
explode_in_nodes (S n) t = rewrite explode_in_nodes n (Node t t) in
                           rewrite plusZeroRightNeutral $ 2 `power` n in
                           rewrite plusCommutative (nodes t + nodes t) 1 in
                           rewrite multRightSuccPlus (power 2 n) (nodes t + nodes t) in
                           rewrite plusCommutative (power 2 n) $ power 2 n * (nodes t + nodes t) in
                           rewrite sym $ plusAssociative (power 2 n * (nodes t + nodes t)) (power 2 n) (power 2 n) in
                           rewrite multDistributesOverPlusRight (power 2 n) (nodes t) (nodes t) in
                           rewrite multDistributesOverPlusLeft (power 2 n) (power 2 n) (nodes t) in
                           Refl

-- Exercise 2.11

-- Original `Int` was replaces with `Int` because where are not enough rules for `Int`s.

public export
data Exp = Var
         | Const Nat
         | Add Exp Exp
         | Mult Exp Exp

public export
eval : Exp -> Nat -> Nat
eval Var        x = x
eval (Const n)  _ = n
eval (Add l r)  x = eval l x + eval r x
eval (Mult l r) x = eval l x * eval r x

public export
evalp : Num a => List a -> a -> a
evalp []      _ = 0
evalp (p::ps) x = p + x * evalp ps x

infixr 8 +|+
public export
(+|+) : Num a => List a -> List a -> List a
[]      +|+ r       = r
l       +|+ []      = l
(l::ls) +|+ (r::rs) = l+r :: ls +|+ rs

export
evalp_add_lin : (l, r : List Nat) -> (x : Nat) -> evalp (l +|+ r) x = evalp l x + evalp r x
evalp_add_lin [] r x = Refl
evalp_add_lin l@(_::_) [] x = rewrite plusZeroRightNeutral (evalp l x) in Refl
evalp_add_lin (l::ls) (r::rs) x = rewrite evalp_add_lin ls rs x in
                                  rewrite multDistributesOverPlusRight x (evalp ls x) (evalp rs x) in
                                  rewrite replus l r (mult x (evalp ls x)) (mult x (evalp rs x)) in
                                  Refl
  where
    replus : (l, r, p, q : Nat) -> (l + r) + (p + q) = (l + p) + (r + q)
    replus l r p q = rewrite sym $ plusAssociative l r (p + q) in
                     rewrite plusCommutative p q in
                     rewrite plusAssociative r q p in
                     rewrite plusCommutative (r + q) p in
                     rewrite plusAssociative l p (r + q) in
                     Refl

infixr 9 *|*
public export
(*|*) : Num a => List a -> List a -> List a
[]      *|* _       = []
_       *|* []      = []
(l::ls) *|* (r::rs) = l*r :: (0 :: ls *|* rs) +|+ map (*l) rs +|+ map (*r) ls

evalp_map : (n : Nat) -> (ns : List Nat) -> (x : Nat) -> evalp (map (*n) ns) x = n * evalp ns x
evalp_map n [] x = rewrite multZeroRightZero n in Refl
evalp_map n (m::ms) x = rewrite evalp_map n ms x in
                        rewrite multAssociative x n (evalp ms x) in
                        rewrite multCommutative x n in
                        rewrite multCommutative m n in
                        rewrite multDistributesOverPlusRight n m (x * evalp ms x) in
                        rewrite multAssociative n x (evalp ms x) in
                        Refl

export
evalp_mul_lin : (l, r : List Nat) -> (x : Nat) -> evalp (l *|* r) x = evalp l x * evalp r x
evalp_mul_lin [] r x = Refl
evalp_mul_lin l@(_::_) [] x = rewrite multZeroRightZero (evalp l x) in Refl
evalp_mul_lin (l::ls) (r::rs) x = rewrite evalp_add_lin (0 :: ls *|* rs) (map (*l) rs +|+ map (*r) ls) x in
                                  rewrite evalp_add_lin (map (*l) rs) (map (*r) ls) x in
                                  rewrite evalp_mul_lin ls rs x in
                                  rewrite evalp_map r ls x in
                                  rewrite evalp_map l rs x in
                                  rewrite remult l r (evalp ls x) (evalp rs x) x in
                                  Refl
  where
    remult : (l, r, el, er, x : Nat) -> (l + x*el) * (r + x*er) = l*r + x*(x*(el*er) + (l*er + r*el))
    remult l r el er x =                                                                           -- (l + x*el) * (r + x*er)
                         rewrite multDistributesOverPlusLeft l (x*el) (r + x*er) in                -- l * (r + x*er) + (x*el)*(r + x*er)
                         rewrite multDistributesOverPlusRight l r (x*er) in                        -- (l*r + l*(x*er)) + (x*el)*(r + x*er)
                         rewrite multDistributesOverPlusRight (x*el) r (x*er) in                   -- (l*r + l*(x*er)) + ((x*el)*r + (x*el)*(x*er))
                         rewrite multAssociative l x er in                                         -- (l*r + (l*x)*er) + ((x*el)*r + (x*el)*(x*er))
                         rewrite multCommutative l x in                                            -- (l*r + (x*l)*er) + ((x*el)*r + (x*el)*(x*er))
                         rewrite sym $ multAssociative x l er in                                   -- (l*r + x*(l*er)) + ((x*el)*r + (x*el)*(x*er))
                         rewrite sym $ multAssociative x el r in                                   -- (l*r + x*(l*er)) + (x*(el*r) + (x*el)*(x*er))
                         rewrite sym $ multAssociative x el (x*er) in                              -- (l*r + x*(l*er)) + (x*(el*r) + x*(el*(x*er)))
                         rewrite multAssociative el x er in                                        -- (l*r + x*(l*er)) + (x*(el*r) + x*((el*x)*er))
                         rewrite multCommutative el x in                                           -- (l*r + x*(l*er)) + (x*(el*r) + x*((x*el)*er))
                         rewrite sym $ multAssociative x el er in                                  -- (l*r + x*(l*er)) + (x*(el*r) + x*(x*(el*er)))
                         rewrite multCommutative el r in                                           -- (l*r + x*(l*er)) + (x*(r*el) + x*(x*(el*er)))
                         rewrite sym $ multDistributesOverPlusRight x (r*el) (x*(el*er)) in        -- (l*r + x*(l*er)) + x*(r*el + x*(el*er))
                         rewrite plusCommutative (r*el) (x*(el*er)) in                             -- (l*r + x*(l*er)) + x*(x*(el*er) + r*el)
                         rewrite sym $ plusAssociative (l*r) (x*(l*er)) (x*(x*(el*er) + r*el)) in  -- l*r + (x*(l*er) + x*(x*(el*er) + r*el))
                         rewrite sym $ multDistributesOverPlusRight x (l*er) (x*(el*er) + r*el) in -- l*r + x*(l*er + (x*(el*er) + r*el))
                         rewrite plusAssociative (l*er) (x*(el*er)) (r*el) in                      -- l*r + x*((l*er + x*(el*er)) + r*el)
                         rewrite plusCommutative (l*er) (x*(el*er)) in                             -- l*r + x*((x*(el*er) + l*er) + r*el)
                         rewrite sym $ plusAssociative (x*(el*er)) (l*er) (r*el) in                -- l*r + x*(x*(el*er) + (l*er + r*el))
                         Refl

public export
coeffs : Exp -> List Nat
coeffs Var        = [0, 1]
coeffs (Const n)  = [n]
coeffs (Add l r)  = coeffs l +|+ coeffs r
coeffs (Mult l r) = coeffs l *|* coeffs r

export
evalp_of_coeffs_is_eval : (e : Exp) -> (x : Nat) -> evalp (coeffs e) x = eval e x
evalp_of_coeffs_is_eval Var x = rewrite multZeroRightZero x in
                                rewrite multOneRightNeutral x in
                                Refl
evalp_of_coeffs_is_eval (Const n) x = rewrite multZeroRightZero x in
                                      rewrite plusZeroRightNeutral n in
                                      Refl
evalp_of_coeffs_is_eval (Add l r) x = rewrite evalp_add_lin (coeffs l) (coeffs r) x in
                                      rewrite evalp_of_coeffs_is_eval l x in
                                      rewrite evalp_of_coeffs_is_eval r x in
                                      Refl
evalp_of_coeffs_is_eval (Mult l r) x = rewrite evalp_mul_lin (coeffs l) (coeffs r) x in
                                       rewrite evalp_of_coeffs_is_eval l x in
                                       rewrite evalp_of_coeffs_is_eval r x in
                                       Refl

max_stars_repo_name: buzden/prog-prove-exercises

max_issues_repo_name: buzden/prog-prove-exercises

max_forks_repo_name: buzden/prog-prove-exercises


text:
module Control.Lens.Review
import Data.Contravariant
import Control.Lens.Types
import Control.Lens.Getter
import Control.Monad.Identity
import Data.Profunctor
import Data.Tagged

%default total

infixr 8 #

public export
(#) : AReview t b -> b -> t
(#) p = runIdentity . untag . p . MkTagged . Id

public export
re : AReview t b -> Getter b t
re p = to (p #)


text:
module System.File.Process

import public System.Escape
import public System.File.Error
import public System.File.Mode
import System.File.Support
import public System.File.Types

%foreign "C:fflush,libc 6"
prim__flush : FilePtr -> PrimIO Int
%foreign support "idris2_popen"
prim__popen : String -> String -> PrimIO FilePtr
%foreign support "idris2_pclose"
prim__pclose : FilePtr -> PrimIO Int

||| Force a write of all user-space buffered data for the given `File`.
|||
||| @ h the file handle to flush
export
fflush : HasIO io => (h : File) -> io ()
fflush (FHandle f)
    = ignore $ primIO (prim__flush f)

||| Create a new unidirectional pipe by invoking the shell, which is passed the
||| given command-string using the '-c' flag, in a new process. The pipe is
||| opened with the given mode.
|||
||| @ cmd the command to pass to the shell
||| @ m   the mode the pipe should have
export
popen : HasIO io => (cmd : String) -> (m : Mode) -> io (Either FileError File)
popen cmd m = do
    ptr <- primIO (prim__popen cmd (modeStr m))
    if prim__nullAnyPtr ptr /= 0
        then returnError
        else pure (Right (FHandle ptr))

namespace Escaped
  export
  popen : HasIO io => (cmd : List String) -> (m : Mode) -> io (Either FileError File)
  popen = popen . escapeCmd

||| Wait for the process associated with the pipe to terminate.
|||
||| @ fh the file handle to the stream to close/wait on
export
pclose : HasIO io => (fh : File) -> io Int
pclose (FHandle h) = primIO (prim__pclose h)


text:
||| In a discrete ordered group, distinct elements are at least a
||| fixed `unit` distance apart.  The group is assumed to be abelian.
module Specifications.DiscreteOrderedGroup

import public Specifications.OrderedGroup

%default total
%access public export

||| specification
isDiscreteOrder : Binop s -> Binrel s -> s -> s -> Type
isDiscreteOrder (+) (<=) zero unit = (x : _) ->
  Not (x = zero) -> x <= zero -> unit + x <= zero

||| composed specification
data DiscreteOrderedGroupSpec :
       Binop s -> s -> (s -> s) -> Binrel s -> s -> Type where
  MkDiscreteOrderedGroup :
    OrderedGroupSpec add zero neg leq ->
    isAbelian add ->
    isDiscreteOrder add leq zero unit ->
    DiscreteOrderedGroupSpec add zero neg leq unit

||| forget
orderedGroup : DiscreteOrderedGroupSpec add zero neg leq _ ->
  OrderedGroupSpec add zero neg leq
orderedGroup (MkDiscreteOrderedGroup g _ _) = g

||| forget
partiallyOrderedGroup : DiscreteOrderedGroupSpec add zero neg leq _ ->
  PartiallyOrderedGroupSpec add zero neg leq
partiallyOrderedGroup spec = partiallyOrderedGroup (orderedGroup spec)

||| forget more
group : DiscreteOrderedGroupSpec add zero neg _ _ -> GroupSpec add zero neg
group spec = group (partiallyOrderedGroup spec)

||| forget
discreteOrder : DiscreteOrderedGroupSpec add zero _ leq unit ->
  isDiscreteOrder add leq zero unit
discreteOrder (MkDiscreteOrderedGroup _ _ d) = d

||| forget
totalOrder : DiscreteOrderedGroupSpec _ _ _ leq _ -> TotalOrderSpec leq
totalOrder (MkDiscreteOrderedGroup p _ _) = totalOrder p

||| forget
abelian : DiscreteOrderedGroupSpec add _ _ _ _ -> isAbelian add
abelian (MkDiscreteOrderedGroup _ a _) = a

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
module TestException

import Control.App

throwBoth : Has [Exception String, Exception Int] es => App es ()

throwOne : Has [Exception Int] es => App es Int
throwOne {es} = handle {err = String} {e = es} throwBoth (\r => pure 1) (\e => pure 3)


text:
-- examples in "Type-Driven Development with Idris"
-- chapter 13, section 2, Stack part

import Data.Vect

-- check that all functions are total
%default total

data StackCmd : Type -> Nat -> Nat -> Type where
  Push : Integer -> StackCmd () height (S height)
  Pop : StackCmd Integer (S height) height
  Top : StackCmd Integer (S height) (S height)
  GetStr : StackCmd String height height
  PutStr : String -> StackCmd () height height
  Pure : ty -> StackCmd ty s s
  (>>=) : StackCmd a s1 s2 ->
          (a -> StackCmd b s2 s3) ->
          StackCmd b s1 s3

runStack : (stk : Vect inHeight Integer) ->
           StackCmd ty inHeight outHeight ->
           IO (ty, Vect outHeight Integer)
runStack stk (Push x) = pure ((), x :: stk)
runStack (x :: xs) Pop = pure (x, xs)
runStack (x :: xs) Top = pure (x, x :: xs)
runStack stk (Pure x) = pure (x, stk)
runStack stk (x >>= f) = do (res, stk') <- runStack stk x
                            runStack stk' (f res)
runStack stk GetStr = do val <- getLine
                         pure (val, stk)
runStack stk (PutStr val) = do putStr val
                               pure ((), stk)

doAdd : StackCmd () (S (S height)) (S height)
doAdd = do val1 <- Pop
           val2 <- Pop
           Push $ val1 + val2

data StackIO : Nat -> Type where
  Do : StackCmd a h1 h2 ->
       (a -> Inf (StackIO h2)) -> StackIO h1

namespace StackDo
  (>>=) : StackCmd a h1 h2 ->
          (a -> Inf (StackIO h2)) -> StackIO h1
  (>>=) = Do

data Fuel = Dry | More (Lazy Fuel)

partial
forever : Fuel
forever = More forever

run : Fuel -> Vect h Integer -> StackIO h -> IO ()
run (More fuel) stk (Do c f)
  = do (res, stk') <- runStack stk c
       run fuel stk' (f res)
run Dry stk p = pure ()

data StkInput = Number Integer
              | Add

strToInput : String -> Maybe StkInput
strToInput "" = Nothing
strToInput "add" = Just Add
strToInput x = if all isDigit (unpack x)
                then Just (Number (cast x))
                else Nothing

mutual
  tryAdd : StackIO h
  tryAdd {h = (S (S k))}
    = do doAdd
         result <- Top
         PutStr (show result ++ "\n")
         stackCalc
  tryAdd
    = do PutStr "Fewer than two items on the stack\n"
         stackCalc

  stackCalc : StackIO h
  stackCalc = do PutStr "> "
                 input <- GetStr
                 case strToInput input of
                   Nothing => do PutStr "Invalid input\n"
                                 stackCalc
                   Just (Number x) => do Push x
                                         stackCalc
                   Just Add => tryAdd

partial
main : IO ()
main = run forever [] stackCalc

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
> module FastSimpleProb.Measures

> import FastSimpleProb.SimpleProb
> import FastSimpleProb.BasicOperations
> import FastSimpleProb.MonadicOperations
> import FastSimpleProb.MonadicPostulates
> import FastSimpleProb.MonadicProperties
> import Double.Predicates
> import NonNegDouble.NonNegDouble
> import NonNegDouble.Predicates
> import NonNegDouble.BasicOperations
> import NonNegDouble.Operations
> import NonNegDouble.Properties
> import NonNegDouble.Measures
> import NonNegDouble.LTEProperties
> import List.Operations
> import List.Properties
> import Fun.Operations
> import Rel.TotalPreorder
> import Pairs.Operations

> %default total
> %access public export
> %auto_implicits off

* Measures

> ||| Worst
> worst : SimpleProb NonNegDouble -> NonNegDouble
> worst sp = List.Operations.min totalPreorderLTE xs ne where
>   xs : List NonNegDouble
>   xs = map fst (toList sp)
>   ne : List.Operations.NonEmpty xs
>   ne = mapPreservesNonEmpty fst (toList sp) (nonEmptyLemma1 sp)

> using implementation NumNonNegDouble
>   ||| Sum
>   sum : SimpleProb NonNegDouble -> NonNegDouble
>   sum = Prelude.Foldable.sum . (map (uncurry (*))) . toList

> ||| Expected value
> expectedValue : SimpleProb NonNegDouble -> NonNegDouble
> expectedValue = sum . normalize

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
> module LocalEffect.Exception

> import Effects
> import Effect.Exception

> import Nat.LTProperties
> import BoundedNat.BoundedNat
> import Sigma.Sigma
> import Pairs.Operations

> %default total

> %access public export

> ||| Parses a string for a Nat
> parseNat : String -> { [EXCEPTION String] } Eff Nat
> parseNat str
>   = if all (\x => isDigit x) (unpack str)
>     then pure (cast {to = Nat} (cast {to = Int} str))
>     else raise "Not a Nat!"

> ||| Parses a string for a bounded Nat
> parseLTB : (b : Nat) -> String -> { [EXCEPTION String] } Eff (LTB b)
> {-
> parseLTB b str
>   = if all (\x => isDigit x) (unpack str)
>     then let n = cast {to = Nat} (cast {to = Int} str) in
>          case (decLT n b) of
>            (Yes p) => pure (MkSigma n p)
>            (No _)  => raise "Out of bound!"
>     else raise "Not a Nat!"
> -}
> parseLTB b str
>   = if all (\x => isDigit x) (unpack str)
>     then let m = cast {to = Nat} (cast {to = Int} str) in
>          case (decLT m b) of
>            (Yes p) => pure (MkSigma m p)
>            (No _)  => raise "Out of bound!"
>     else raise "Not a Nat!"

> ||| Parses a string for an Int
> parseInt : String -> { [EXCEPTION String] } Eff Int
> parseInt str
>   = if all (\x => isDigit x || x == '-') (unpack str)
>     then pure (cast {to = Int} str)
>     else raise "Not an Int!"


text:
module Cordial.Model.Common.VLNV

%default total
%access public export

record VLNV where
  constructor MkVLNV
  vendor : String
  library : String
  name    : String
  version : String

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

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial