text:
module Compiler.Jvm.Optimizer

import Compiler.Common
import Compiler.CompileExpr
import Compiler.Inline

import Control.Monad.State

import Core.Context
import Core.Name
import Core.TT

import Libraries.Data.SortedMap
import Libraries.Data.SortedSet
import Data.List
import Data.Maybe
import Data.String
import Data.Vect

import Compiler.Jvm.Asm
import Compiler.Jvm.ExtPrim
import Compiler.Jvm.Foreign
import Compiler.Jvm.InferredType
import Compiler.Jvm.Jname
import Compiler.Jvm.ShowUtil

%hide Core.Context.Context.Constructor.arity

mutual
    hasTailCall : (predicate: Name -> Bool) -> NamedCExp -> Bool
    hasTailCall predicate (NmLet _ _ _ expr) = hasTailCall predicate expr
    hasTailCall predicate (NmApp _ (NmRef _ name) _) = predicate name
    hasTailCall predicate (NmApp _ lambdaVariable _) = predicate (UN $ Basic "")
    hasTailCall predicate (NmExtPrim fc p args) = predicate (UN $ Basic "")
    hasTailCall predicate (NmConCase _ _ conAlts def) =
        maybe False (\defExp => hasTailCall predicate defExp) def || hasTailCallConAlt predicate conAlts
    hasTailCall predicate (NmConstCase _ _ constAlts def) =
        maybe False (\defExp => hasTailCall predicate defExp) def || hasTailCallConstAlt predicate constAlts
    hasTailCall _ _ = False

    hasTailCallConAlt : (predicate: Name -> Bool) -> List NamedConAlt -> Bool
    hasTailCallConAlt predicate [] = False
    hasTailCallConAlt predicate ((MkNConAlt _ _ _ _ expr) :: alts) =
        hasTailCall predicate expr || hasTailCallConAlt predicate alts

    hasTailCallConstAlt : (predicate: Name -> Bool) -> List NamedConstAlt -> Bool
    hasTailCallConstAlt predicate [] = False
    hasTailCallConstAlt predicate ((MkNConstAlt _ expr) :: alts) =
        hasTailCall predicate expr || hasTailCallConstAlt predicate alts

export
thunkParamName : Name
thunkParamName = UN $ Basic "$jvm$thunk"

thunkExpr : NamedCExp -> NamedCExp
thunkExpr expr = NmLam (getFC expr) thunkParamName expr

isBoolTySpec : String -> Name -> Bool
isBoolTySpec "Prelude" (UN (Basic "Bool")) = True
isBoolTySpec "Prelude.Basics" (UN (Basic "Bool")) = True
isBoolTySpec _ _ = False

export
tySpec : NamedCExp -> Asm InferredType
tySpec (NmCon fc (UN (Basic "Int")) _ _ []) = pure IInt
tySpec (NmCon fc (UN (Basic "Integer")) _ _ []) = pure inferredBigIntegerType
tySpec (NmCon fc (UN (Basic "String")) _ _ []) = pure inferredStringType
tySpec (NmCon fc (UN (Basic "Double")) _ _ []) = pure IDouble
tySpec (NmCon fc (UN (Basic "Char")) _ _ []) = pure IChar
tySpec (NmCon fc (UN (Basic "Bool")) _ _ []) = pure IBool
tySpec (NmCon fc (UN (Basic "long")) _ _ []) = pure ILong
tySpec (NmCon fc (UN (Basic "void")) _ _ []) = pure IVoid
tySpec (NmCon fc (UN (Basic ty)) _ _ []) = pure $ IRef ty
tySpec (NmCon fc (NS namespaces n) _ _ []) = cond
    [(n == UN (Basic "Unit"), pure IVoid),
      (isBoolTySpec (show namespaces) n, pure IBool)] (pure inferredObjectType)
tySpec ty = pure inferredObjectType

export
getFArgs : NamedCExp -> Asm (List (NamedCExp, NamedCExp))
getFArgs (NmCon fc _ _ (Just 0) _) = pure []
getFArgs (NmCon fc _ _ (Just 1) [ty, val, rest]) = pure $ (ty, val) :: !(getFArgs rest)
getFArgs arg = Throw (getFC arg) ("Badly formed jvm call argument list " ++ show arg)

getLineNumbers : FilePos -> FilePos -> (Int, Int)
getLineNumbers (lineStart, _) (lineEnd, colEnd) =
    (lineStart + 1, if colEnd == 1 then lineEnd else lineEnd + 1)

getFileName : OriginDesc -> String
getFileName (PhysicalIdrSrc moduleIdent) = case unsafeUnfoldModuleIdent moduleIdent of
  (moduleName :: _) => moduleName ++ ".idr"
  _ => "(unknown-source)"
getFileName (PhysicalPkgSrc fname) = fname
getFileName (Virtual Interactive) = "(Interactive)"

getSourceLocationFromOriginDesc : OriginDesc -> FilePos -> FilePos -> (String, Int, Int)
getSourceLocationFromOriginDesc originDesc startPos endPos = (getFileName originDesc, getLineNumbers startPos endPos)

export
getSourceLocation : NamedCExp -> (String, Int, Int)
getSourceLocation expr = case getFC expr of
    EmptyFC => case expr of
        (NmExtPrim _ _ (arg :: args)) => getSourceLocation arg
        (NmOp _ _ (arg :: _)) => getSourceLocation arg
        _ => ("Main.idr", 1, 1)
    (MkVirtualFC originDesc startPos endPos) => getSourceLocationFromOriginDesc originDesc startPos endPos
    (MkFC originDesc startPos endPos) => getSourceLocationFromOriginDesc originDesc startPos endPos

export
getSourceLocationFromFc : FC -> (String, Int, Int)
getSourceLocationFromFc EmptyFC = ("Main.idr", 1, 1)
getSourceLocationFromFc (MkVirtualFC originDesc startPos endPos) =
    getSourceLocationFromOriginDesc originDesc startPos endPos
getSourceLocationFromFc (MkFC originDesc startPos endPos) =
    getSourceLocationFromOriginDesc originDesc startPos endPos

mutual
    export
    used : String -> NamedCExp -> Bool
    used n (NmLocal fc var) = n == jvmSimpleName var
    used n (NmRef _ _) = False
    used n (NmLam _ param sc) = n == jvmSimpleName param || used n sc
    used n (NmLet _ var value sc) = n == jvmSimpleName var || used n value || used n sc
    used n (NmApp _ f args) = used n f || any (used n) args
    used n (NmCon _ _ _ _ args) = any (used n) args
    used n (NmOp _ _ args) = any (used n) $ toList args
    used n (NmExtPrim _ _ args) = any (used n) args
    used n (NmForce _ _ t) = used n t
    used n (NmDelay _ _ t) = used n t
    used n (NmConCase _ sc alts def)
        = used n sc || any (usedCon n) alts
              || maybe False (used n) def
    used n (NmConstCase _ sc alts def)
        = used n sc || any (usedConst n) alts
              || maybe False (used n) def
    used n _ = False

    usedCon : String -> NamedConAlt -> Bool
    usedCon n (MkNConAlt _ _ _ _ sc) = used n sc

    usedConst : String -> NamedConstAlt -> Bool
    usedConst n (MkNConstAlt _ sc) = used n sc

export
extractedMethodArgumentName : Name
extractedMethodArgumentName = UN (Basic "$jvm$arg")

%inline
maxCasesInMethod : Int
maxCasesInMethod = 5

appliedLambdaSwitchIndicator : FC
appliedLambdaSwitchIndicator = MkFC (PhysicalPkgSrc "$jvmAppliedLambdaSwitch$") (0, 0) (0, 0)

appliedLambdaLetIndicator : FC
appliedLambdaLetIndicator = MkFC (PhysicalPkgSrc "$jvmAppliedLambdaLet$") (0, 0) (0, 0)

data AppliedLambdaType = AppliedLambdaSwitch | AppliedLambdaLet | AppliedLambdaUnknown

Eq AppliedLambdaType where
    AppliedLambdaSwitch == AppliedLambdaSwitch = True
    AppliedLambdaLet == AppliedLambdaLet = True
    AppliedLambdaUnknown == AppliedLambdaUnknown = True
    _ == _ = False

getAppliedLambdaType : FC -> AppliedLambdaType
getAppliedLambdaType fc =
    if fc == appliedLambdaSwitchIndicator then AppliedLambdaSwitch
    else if fc == appliedLambdaLetIndicator then AppliedLambdaLet
    else AppliedLambdaUnknown

mutual
    goLiftToLambda : (isTailPosition: Bool) -> NamedCExp -> State Int NamedCExp
    goLiftToLambda False (NmLet fc var value sc) = do
        let extractedMethodArgumentVarName = extractedMethodArgumentName
        let extractedMethodArgumentVar = NmLocal fc extractedMethodArgumentVarName
        liftedValue <- goLiftToLambda False value
        liftedSc <- goLiftToLambda True sc
        let body = NmLet fc var extractedMethodArgumentVar liftedSc
        pure $ NmApp appliedLambdaLetIndicator (NmLam fc extractedMethodArgumentVarName body) [liftedValue]
    goLiftToLambda True (NmLet fc var value sc) =
        pure $ NmLet fc var !(goLiftToLambda False value) !(goLiftToLambda True sc)
    goLiftToLambda False (NmConCase fc sc alts def) = do
        put $ succ !get
        let var = extractedMethodArgumentName
        liftedSc <- goLiftToLambda False sc
        liftedAlts <- traverse liftToLambdaCon alts
        liftedDef <- traverse liftToLambdaDefault def
        pure $ NmApp appliedLambdaSwitchIndicator
            (NmLam fc var (NmConCase fc (NmLocal fc var) liftedAlts liftedDef)) [liftedSc]
    goLiftToLambda True expr@(NmConCase fc sc alts def) = do
        cases <- get
        put $ succ cases
        if cases > maxCasesInMethod
            then do
                put $ the Int 0
                goLiftToLambda False expr
            else do
                liftedAlts <- traverse liftToLambdaCon alts
                liftedDef <- traverse liftToLambdaDefault def
                pure $ NmConCase fc !(goLiftToLambda False sc) liftedAlts liftedDef
    goLiftToLambda False (NmConstCase fc sc alts def) = do
        put $ succ !get
        let var = extractedMethodArgumentName
        liftedAlts <- traverse liftToLambdaConst alts
        liftedDef <- traverse liftToLambdaDefault def
        liftedSc <- goLiftToLambda False sc
        pure $ NmApp appliedLambdaSwitchIndicator
            (NmLam fc var $ NmConstCase fc (NmLocal fc var) liftedAlts liftedDef) [liftedSc]
    goLiftToLambda True expr@(NmConstCase fc sc alts def) = do
        cases <- get
        put $ succ cases
        if cases > maxCasesInMethod
            then do
                put $ the Int 0
                goLiftToLambda False expr
            else do
                liftedSc <- goLiftToLambda False sc
                liftedAlts <- traverse liftToLambdaConst alts
                liftedDef <- traverse liftToLambdaDefault def
                pure $ NmConstCase fc liftedSc liftedAlts liftedDef
    goLiftToLambda _ (NmLam fc param sc) = pure $ NmLam fc param !(goLiftToLambda True sc)
    goLiftToLambda _ (NmApp fc f args) =
        pure $ NmApp fc !(goLiftToLambda False f) !(traverse (goLiftToLambda False) args)
    goLiftToLambda _ expr@(NmCon fc name conInfo tag args) =
        pure $ NmCon fc name conInfo tag !(traverse (goLiftToLambda False) args)
    goLiftToLambda _ (NmOp fc f args) = pure $ NmOp fc f !(traverse (goLiftToLambda False) args)
    goLiftToLambda _ (NmExtPrim fc f args) = pure $ NmExtPrim fc f !(traverse (goLiftToLambda False) args)
    goLiftToLambda _ (NmForce fc reason t) = pure $ NmForce fc reason !(goLiftToLambda False t)
    goLiftToLambda _ (NmDelay fc reason t) = pure $ NmDelay fc reason !(goLiftToLambda True t)
    goLiftToLambda _ expr = pure expr

    liftToLambdaDefault : NamedCExp -> State Int NamedCExp
    liftToLambdaDefault body = goLiftToLambda True body

    liftToLambdaCon : NamedConAlt -> State Int NamedConAlt
    liftToLambdaCon (MkNConAlt n conInfo tag args body) =
      pure $ MkNConAlt n conInfo tag args !(goLiftToLambda True body)

    liftToLambdaConst : NamedConstAlt -> State Int NamedConstAlt
    liftToLambdaConst (MkNConstAlt constant body) = pure $ MkNConstAlt constant !(goLiftToLambda True body)

liftToLambda : NamedCExp -> NamedCExp
liftToLambda expr = evalState 0 (goLiftToLambda True expr)

mutual
    doGetFreeVariables : SortedSet String -> SortedSet String -> NamedCExp -> SortedSet String
    doGetFreeVariables freeVariables boundVariables (NmLocal fc var) =
        let varName = jvmSimpleName var
        in
            if SortedSet.contains varName boundVariables
                then freeVariables
                else SortedSet.insert varName freeVariables
    doGetFreeVariables freeVariables boundVariables (NmLam _ parameterName body) =
        doGetFreeVariables freeVariables (SortedSet.insert (jvmSimpleName parameterName) boundVariables) body
    doGetFreeVariables freeVariables boundVariables (NmLet _ var value body) =
        let newFreeVariables = doGetFreeVariables freeVariables boundVariables value
            newBoundVariables = SortedSet.insert (jvmSimpleName var) boundVariables
        in doGetFreeVariables newFreeVariables newBoundVariables body
    doGetFreeVariables freeVariables boundVariables (NmApp _ (NmRef _ _) args) =
        getExpressionsFreeVariables freeVariables boundVariables args
    doGetFreeVariables freeVariables boundVariables (NmApp _ f args) =
        getExpressionsFreeVariables freeVariables boundVariables (f :: args)
    doGetFreeVariables freeVariables boundVariables (NmCon _ _ _ _ args) =
        getExpressionsFreeVariables freeVariables boundVariables args
    doGetFreeVariables freeVariables boundVariables (NmOp _ _ args) =
        getExpressionsFreeVariables freeVariables boundVariables $ toList args
    doGetFreeVariables freeVariables boundVariables (NmExtPrim _ _ args) =
        getExpressionsFreeVariables freeVariables boundVariables args
    doGetFreeVariables freeVariables boundVariables (NmForce _ _ t) =
        doGetFreeVariables freeVariables boundVariables t
    doGetFreeVariables freeVariables boundVariables (NmDelay _ _ t) =
        doGetFreeVariables freeVariables boundVariables t
    doGetFreeVariables freeVariables boundVariables (NmConCase _ sc alts def) =
        let switchExprFreeVariables = doGetFreeVariables freeVariables boundVariables sc
            altsFreeVariables = doGetFreeVariablesCon switchExprFreeVariables boundVariables alts
        in maybe altsFreeVariables (doGetFreeVariables altsFreeVariables boundVariables) def
    doGetFreeVariables freeVariables boundVariables (NmConstCase _ sc alts def) =
        let switchExprFreeVariables = doGetFreeVariables freeVariables boundVariables sc
            altsFreeVariables = doGetFreeVariablesConst switchExprFreeVariables boundVariables alts
        in maybe altsFreeVariables (doGetFreeVariables altsFreeVariables boundVariables) def
    doGetFreeVariables freeVariables _ _ = freeVariables

    getExpressionsFreeVariables : SortedSet String -> SortedSet String -> List NamedCExp -> SortedSet String
    getExpressionsFreeVariables freeVariables boundVariables expressions = go freeVariables expressions where
        go : SortedSet String -> List NamedCExp -> SortedSet String
        go freeVariables [] = freeVariables
        go freeVariables (arg :: args) = go (doGetFreeVariables freeVariables boundVariables arg) args

    doGetFreeVariablesCon : SortedSet String -> SortedSet String -> List NamedConAlt -> SortedSet String
    doGetFreeVariablesCon freeVariables _ [] = freeVariables
    doGetFreeVariablesCon freeVariables boundVariables ((MkNConAlt _ _ _ properties sc) :: rest) =
        let newBoundVariables = SortedSet.union boundVariables (SortedSet.fromList (jvmSimpleName <$> properties))
        in doGetFreeVariablesCon (doGetFreeVariables freeVariables newBoundVariables sc) boundVariables rest

    doGetFreeVariablesConst : SortedSet String -> SortedSet String -> List NamedConstAlt -> SortedSet String
    doGetFreeVariablesConst freeVariables _ [] = freeVariables
    doGetFreeVariablesConst freeVariables boundVariables ((MkNConstAlt _ sc) :: rest) =
        doGetFreeVariablesConst (doGetFreeVariables freeVariables boundVariables sc) boundVariables rest

getFreeVariables : SortedSet String -> NamedCExp -> SortedSet String
getFreeVariables boundVariables expr = doGetFreeVariables SortedSet.empty boundVariables expr

jvmTailRecName : Name
jvmTailRecName = UN $ Basic "$jvmTailRec"

mutual
    markTailRecursion : NamedCExp -> Asm NamedCExp
    markTailRecursion expr@(NmApp fc (NmRef nameFc idrisName) args) =
        let jname = jvmName idrisName
            functionName = getIdrisFunctionName !getProgramName (className jname) (methodName jname)
        in if functionName == !getRootMethodName
               then Pure (NmApp fc (NmRef nameFc jvmTailRecName) args)
               else Pure expr
    markTailRecursion expr@(NmLet fc var value body) =
        NmLet fc var value <$> markTailRecursion body
    markTailRecursion expr@(NmConCase fc sc alts def) = do
        tailRecursionMarkedAlts <- traverse markTailRecursionConAlt alts
        tailRecursionMarkedDefault <- traverse markTailRecursion def
        Pure (NmConCase fc sc tailRecursionMarkedAlts tailRecursionMarkedDefault)
    markTailRecursion (NmConstCase fc sc alts def) = do
        tailRecursionMarkedAlts <- traverse markTailRecursionConstAlt alts
        tailRecursionMarkedDefault <- traverse markTailRecursion def
        Pure (NmConstCase fc sc tailRecursionMarkedAlts tailRecursionMarkedDefault)
    markTailRecursion expr = Pure expr

    markTailRecursionConAlt : NamedConAlt -> Asm NamedConAlt
    markTailRecursionConAlt (MkNConAlt name conInfo tag args caseBody) =
        MkNConAlt name conInfo tag args <$> markTailRecursion caseBody

    markTailRecursionConstAlt : NamedConstAlt -> Asm NamedConstAlt
    markTailRecursionConstAlt (MkNConstAlt constant caseBody) = MkNConstAlt constant <$> markTailRecursion caseBody

optThunkExpr : Bool -> NamedCExp -> NamedCExp
optThunkExpr True = thunkExpr
optThunkExpr _ = id

mutual
    trampolineExpression : (isTailRec: Bool) -> NamedCExp -> NamedCExp
    -- Do not trampoline as tail recursion will be eliminated
    trampolineExpression _ (NmApp fc (NmRef nameFc (UN (Basic "$jvmTailRec"))) args) =
      NmApp fc (NmRef nameFc jvmTailRecName) (trampolineExpression False <$> args)
    trampolineExpression isTailRec (NmApp fc f args) =
      optThunkExpr isTailRec $ NmApp fc (trampolineExpression False f) (trampolineExpression False <$> args)
    trampolineExpression _ (NmLam fc param body) = NmLam fc param $ trampolineExpression False body
    trampolineExpression isTailRec (NmLet fc var value body) =
        NmLet fc var (trampolineExpression False value) $ trampolineExpression isTailRec body
    trampolineExpression _ (NmConCase fc sc alts def) =
        let trampolinedAlts = trampolineExpressionConAlt <$> alts
            trampolinedDefault = trampolineExpression True <$> def
        in NmConCase fc sc trampolinedAlts trampolinedDefault
    trampolineExpression _ (NmConstCase fc sc alts def) =
        let trampolinedAlts = trampolineExpressionConstAlt <$> alts
            trampolinedDefault = trampolineExpression True <$> def
        in NmConstCase fc sc trampolinedAlts trampolinedDefault
    trampolineExpression _ expr = expr

    trampolineExpressionConAlt : NamedConAlt -> NamedConAlt
    trampolineExpressionConAlt (MkNConAlt name conInfo tag args caseBody) =
        MkNConAlt name conInfo tag args $ trampolineExpression True caseBody

    trampolineExpressionConstAlt : NamedConstAlt -> NamedConstAlt
    trampolineExpressionConstAlt (MkNConstAlt constant caseBody) =
      MkNConstAlt constant $ trampolineExpression True caseBody

exitInferenceScope : Int -> Asm ()
exitInferenceScope scopeIndex = updateCurrentScopeIndex scopeIndex

enterInferenceScope : Int -> Int -> Asm ()
enterInferenceScope lineNumberStart lineNumberEnd = do
    parentScopeIndex <- getCurrentScopeIndex
    scopeIndex <- newScopeIndex
    parentScope <- getScope parentScopeIndex
    variableTypes <- LiftIo $ Map.newTreeMap {key=String} {value=InferredType}
    allVariableTypes <- LiftIo $ Map.newTreeMap {key=Int} {value=InferredType}
    variableIndices <- LiftIo $ Map.newTreeMap {key=String} {value=Int}
    allVariableIndices <- LiftIo $ Map.newTreeMap {key=String} {value=Int}
    let newScope =
        MkScope scopeIndex (Just parentScopeIndex) variableTypes allVariableTypes variableIndices
            allVariableIndices IUnknown (nextVariableIndex parentScope) (lineNumberStart, lineNumberEnd) ("", "") []
    addScopeChild parentScopeIndex scopeIndex
    saveScope newScope
    updateCurrentScopeIndex scopeIndex

createLambdaClosureScope : Int -> Int -> List String -> Scope -> Asm Scope
createLambdaClosureScope scopeIndex childScopeIndex closureVariables parentScope = do
    lambdaClosureVariableIndices <- LiftIo $ Map.fromList $ getLambdaClosureVariableIndices [] 0 closureVariables
    variableTypes <- LiftIo $ Map.newTreeMap {key=String} {value=InferredType}
    allVariableTypes <- LiftIo $ Map.newTreeMap {key=Int} {value=InferredType}
    allVariableIndices <- LiftIo $ Map.newTreeMap {key=String} {value=Int}
    Pure $ MkScope scopeIndex (Just $ index parentScope) variableTypes allVariableTypes
        lambdaClosureVariableIndices allVariableIndices IUnknown (cast $ length closureVariables)
        (lineNumbers parentScope) ("", "") [childScopeIndex]
  where
    getLambdaClosureVariableIndices : List (String, Int) -> Int -> List String -> List (String, Int)
    getLambdaClosureVariableIndices acc _ [] = acc
    getLambdaClosureVariableIndices acc index (var :: vars) =
        getLambdaClosureVariableIndices ((var, index) :: acc) (index + 1) vars

enterInferenceLambdaScope : Int -> Int -> Maybe Name -> NamedCExp -> Asm ()
enterInferenceLambdaScope lineNumberStart lineNumberEnd parameterName expr = do
        parentScopeIndex <- getCurrentScopeIndex
        scopeIndex <- newScopeIndex
        let boundVariables = maybe SortedSet.empty (flip SortedSet.insert SortedSet.empty . jvmSimpleName) parameterName
        let freeVariables = getFreeVariables boundVariables expr
        let usedVariables = filter (flip SortedSet.contains freeVariables) !(retrieveVariables parentScopeIndex)
        variableTypes <- LiftIo $ Map.newTreeMap {key=String} {value=InferredType}
        allVariableTypes <- LiftIo $ Map.newTreeMap {key=Int} {value=InferredType}
        variableIndices <- LiftIo $ Map.newTreeMap {key=String} {value=Int}
        allVariableIndices <- LiftIo $ Map.newTreeMap {key=String} {value=Int}
        newScope <- case usedVariables  of
            nonEmptyUsedVariables@(_ :: _) => do
                parentScope <- getScope parentScopeIndex
                lambdaParentScopeIndex <- newScopeIndex
                closureScope <- createLambdaClosureScope lambdaParentScopeIndex scopeIndex nonEmptyUsedVariables
                    parentScope
                saveScope closureScope
                let closureVariableCount = nextVariableIndex closureScope
                Pure $ MkScope scopeIndex (Just lambdaParentScopeIndex) variableTypes allVariableTypes
                    variableIndices allVariableIndices IUnknown closureVariableCount (lineNumberStart, lineNumberEnd)
                    ("", "") []
            [] => Pure $ MkScope scopeIndex Nothing variableTypes allVariableTypes variableIndices allVariableIndices
                IUnknown 0 (lineNumberStart, lineNumberEnd) ("", "") []
        saveScope newScope
        updateCurrentScopeIndex scopeIndex

withInferenceScope : Int -> Int -> Asm result -> Asm result
withInferenceScope lineNumberStart lineNumberEnd op = do
    scopeIndex <- getCurrentScopeIndex
    enterInferenceScope lineNumberStart lineNumberEnd
    result <- op
    exitInferenceScope scopeIndex
    Pure result

withInferenceLambdaScope : Int -> Int -> Maybe Name -> NamedCExp -> Asm result -> Asm result
withInferenceLambdaScope lineNumberStart lineNumberEnd parameterName expr op = do
    scopeIndex <- getCurrentScopeIndex
    enterInferenceLambdaScope lineNumberStart lineNumberEnd parameterName expr
    result <- op
    exitInferenceScope scopeIndex
    Pure result

public export
data LambdaType = ThunkLambda | DelayedLambda | FunctionLambda | Function2Lambda | Function3Lambda | Function4Lambda |
                    Function5Lambda

export
Eq LambdaType where
    ThunkLambda == ThunkLambda = True
    DelayedLambda == DelayedLambda = True
    FunctionLambda == FunctionLambda = True
    Function2Lambda == Function2Lambda = True
    Function3Lambda == Function3Lambda = True
    Function4Lambda == Function4Lambda = True
    Function5Lambda == Function5Lambda = True
    _ == _ = False

export
getLambdaTypeByParameter : (parameterName: Maybe Name) -> LambdaType
getLambdaTypeByParameter (Just (UN (Basic "$jvm$thunk"))) = ThunkLambda
getLambdaTypeByParameter Nothing = DelayedLambda
getLambdaTypeByParameter _ = FunctionLambda

export
getLambdaInterfaceMethodName : LambdaType -> String
getLambdaInterfaceMethodName ThunkLambda = "evaluate"
getLambdaInterfaceMethodName DelayedLambda = "evaluate"
getLambdaInterfaceMethodName _ = "apply"

export
getSamDesc : LambdaType -> String
getSamDesc ThunkLambda = "()" ++ getJvmTypeDescriptor thunkType
getSamDesc DelayedLambda = "()Ljava/lang/Object;"
getSamDesc FunctionLambda = getMethodDescriptor $ MkInferredFunctionType inferredObjectType [inferredObjectType]
getSamDesc Function2Lambda =
  getMethodDescriptor $ MkInferredFunctionType inferredObjectType $ replicate 2 inferredObjectType
getSamDesc Function3Lambda =
  getMethodDescriptor $ MkInferredFunctionType inferredObjectType $ replicate 3 inferredObjectType
getSamDesc Function4Lambda =
  getMethodDescriptor $ MkInferredFunctionType inferredObjectType $ replicate 4 inferredObjectType
getSamDesc Function5Lambda =
  getMethodDescriptor $ MkInferredFunctionType inferredObjectType $ replicate 5 inferredObjectType

export
getLambdaInterfaceType : LambdaType -> InferredType -> InferredType
getLambdaInterfaceType ThunkLambda returnType = getThunkType returnType
getLambdaInterfaceType DelayedLambda returnType = delayedType
getLambdaInterfaceType _ returnType = inferredLambdaType

export
getLambdaImplementationMethodReturnType : LambdaType -> InferredType
getLambdaImplementationMethodReturnType ThunkLambda = thunkType
getLambdaImplementationMethodReturnType _ = inferredObjectType

export
getConstantType : List NamedConstAlt -> Asm InferredType
getConstantType [] = Throw emptyFC "Unknown constant switch type"
getConstantType ((MkNConstAlt constant _) :: _) = case constant of
    I _ => Pure IInt
    B8 _ => Pure IInt
    B16 _ => Pure IInt
    B32 _ => Pure IInt
    Ch _ => Pure IInt
    Str _ => Pure inferredStringType
    BI _ => Pure inferredBigIntegerType
    B64 _ => Pure inferredBigIntegerType
    unsupportedConstant => Throw emptyFC $ "Unsupported constant switch " ++ show unsupportedConstant

export
isTypeConst : TT.Constant -> Bool
isTypeConst Bits8Type   = True
isTypeConst Bits16Type  = True
isTypeConst Bits32Type  = True
isTypeConst Bits64Type  = True
isTypeConst IntType     = True
isTypeConst IntegerType = True
isTypeConst StringType  = True
isTypeConst CharType    = True
isTypeConst DoubleType  = True
isTypeConst WorldType   = True
isTypeConst _           = False

export
getIntConstantValue : FC -> TT.Constant -> Asm Int
getIntConstantValue _ (I i) = Pure i
getIntConstantValue _ (B8 i) = Pure i
getIntConstantValue _ (B16 i) = Pure i
getIntConstantValue _ (B32 i) = Pure i
getIntConstantValue _ (Ch c) = Pure $ ord c
getIntConstantValue _ WorldVal = Pure 0
getIntConstantValue fc x =
    if isTypeConst x
        then Pure 0
        else Throw fc ("Constant " ++ show x ++ " cannot be converted to integer.")

getConstructorTag : ConInfo -> Maybe Int -> Int
getConstructorTag conInfo tag = case conInfo of
  NOTHING => 0
  NIL => 0
  JUST => 1
  CONS => 1
  _ => fromMaybe 0 tag

sortConCases : List NamedConAlt -> List NamedConAlt
sortConCases alts = sortBy (comparing getTag) alts where
    getTag : NamedConAlt -> Int
    getTag (MkNConAlt _ conInfo tag _ _) = getConstructorTag conInfo tag

export
isTypeCase : NamedConAlt -> Bool
isTypeCase (MkNConAlt _ _ Nothing _ _) = True
isTypeCase _ = False

export
substituteVariableSubMethodBody : NamedCExp -> NamedCExp -> NamedCExp
substituteVariableSubMethodBody variable (NmConCase fc _ alts def) = NmConCase fc variable alts def
substituteVariableSubMethodBody variable (NmConstCase fc _ alts def) = NmConstCase fc variable alts def
substituteVariableSubMethodBody value (NmLet fc var _ sc) = NmLet fc var value sc
substituteVariableSubMethodBody _ expr = expr

combineSwitchTypes : Maybe InferredType -> List InferredType -> InferredType
combineSwitchTypes defaultTy [] = fromMaybe IUnknown defaultTy
combineSwitchTypes defaultTy altTypes@(altTy :: rest) = maybe (go altTy rest) (flip go altTypes) defaultTy where
  go : InferredType -> List InferredType -> InferredType
  go prevTy [] = prevTy
  go prevTy (currTy :: rest) = if prevTy == currTy then go currTy rest else inferredObjectType

createNewVariable : (variablePrefix: String) -> InferredType -> Asm ()
createNewVariable variablePrefix ty = do
    variable <- generateVariable variablePrefix
    ignore $ addVariableType variable ty

mutual
    inferExpr : InferredType -> NamedCExp -> Asm InferredType
    inferExpr exprTy (NmDelay _ _ expr) = inferExprLam AppliedLambdaUnknown Nothing Nothing expr
    inferExpr exprTy expr@(NmLocal _ var) = addVariableType (jvmSimpleName var) exprTy
    inferExpr exprTy (NmRef _ _) = pure exprTy
    inferExpr _ (NmApp fc (NmLam _ var body) [expr]) =
        inferExprLam (getAppliedLambdaType fc) (Just expr) (Just var) body
    inferExpr _ (NmLam _ var body) = inferExprLam AppliedLambdaUnknown Nothing (Just var) body
    inferExpr exprTy (NmLet fc var value expr) = inferExprLet fc exprTy var value expr
    inferExpr exprTy app@(NmApp _ _ _) = inferExprApp exprTy app
    inferExpr exprTy expr@(NmCon fc name _ tag args) =
        inferExprCon exprTy (fst $ getSourceLocation expr) name args
    inferExpr exprTy (NmOp _ fn args) = inferExprOp fn args
    inferExpr exprTy (NmExtPrim fc fn args) = inferExtPrim fc exprTy (toPrim fn) args
    inferExpr exprTy (NmForce _ _ expr) = do
        ignore $ inferExpr delayedType expr
        Pure inferredObjectType

    inferExpr exprTy (NmConCase _ sc [] Nothing) = Pure IUnknown
    inferExpr exprTy (NmConCase _ sc [] (Just def)) = do
        inferConstructorSwitchExpr sc
        inferExpr exprTy def
    inferExpr exprTy (NmConCase _ sc [MkNConAlt _ _ _ args expr] Nothing) = do
        inferConstructorSwitchExpr sc
        inferConCaseExpr exprTy args expr
    inferExpr exprTy (NmConCase _ sc alts def) = do
        inferConstructorSwitchExpr sc
        let hasTypeCase = any isTypeCase alts
        when hasTypeCase $ do
            createNewVariable "constructorCaseExpr" inferredStringType
            createNewVariable "hashCodePosition" IInt
        let sortedAlts = if hasTypeCase then alts else sortConCases alts
        altTypes <- traverse (inferExprConAlt exprTy) sortedAlts
        defaultTy <- traverse (inferExprWithNewScope exprTy) def
        Pure $ combineSwitchTypes defaultTy altTypes

    inferExpr exprTy (NmConstCase fc sc [] Nothing) = Pure IUnknown
    inferExpr exprTy (NmConstCase fc sc [] (Just expr)) = inferExpr exprTy expr
    inferExpr exprTy (NmConstCase fc sc alts def) = do
        constantType <- getConstantType alts
        ignore $ inferExpr constantType sc
        when (constantType /= IInt) $ do
            constantExprVariable <- generateVariable "constantCaseExpr"
            ignore $ addVariableType constantExprVariable constantType
            hashCodePositionVariable <- generateVariable "hashCodePosition"
            ignore $ addVariableType hashCodePositionVariable IInt
        sortedAlts <- sortConstCases constantType alts
        altTypes <- traverse (inferExprConstAlt exprTy) sortedAlts
        defaultTy <- traverse (inferExprWithNewScope exprTy) def
        Pure $ combineSwitchTypes defaultTy altTypes
      where
        getConstant : NamedConstAlt -> TT.Constant
        getConstant (MkNConstAlt constant _) = constant

        sortConstCases : InferredType -> List NamedConstAlt -> Asm (List NamedConstAlt)
        sortConstCases IInt alts = do
            constValues <- traverse (getIntConstantValue fc . getConstant) alts
            Pure $ fst <$> (sortBy (comparing snd) $ zip alts constValues)
        sortConstCases _ alts = Pure alts

    inferExpr _ (NmPrimVal fc (B8 _)) = pure IInt
    inferExpr _ (NmPrimVal fc (B16 _)) = pure IInt
    inferExpr _ (NmPrimVal fc (B32 _)) = pure IInt
    inferExpr _ (NmPrimVal fc (B64 _)) = pure ILong
    inferExpr _ (NmPrimVal fc (I _)) = pure IInt
    inferExpr _ (NmPrimVal fc (BI _)) = pure inferredBigIntegerType
    inferExpr _ (NmPrimVal fc (Str _)) = pure inferredStringType
    inferExpr _ (NmPrimVal fc (Ch _)) = pure IChar
    inferExpr _ (NmPrimVal fc (Db _)) = pure IDouble
    inferExpr _ (NmPrimVal fc WorldVal) = pure IInt
    inferExpr exprTy (NmErased fc) = pure exprTy
    inferExpr exprTy (NmCrash fc msg) = pure exprTy
    inferExpr exprTy expr = Throw (getFC expr) ("Unsupported expr " ++ show expr)

    inferConstructorSwitchExpr : NamedCExp -> Asm ()
    inferConstructorSwitchExpr (NmLocal _ var) = do
        let idrisObjectVariable = jvmSimpleName var
        ignore $ addVariableType idrisObjectVariable idrisObjectType
    inferConstructorSwitchExpr sc = do
        idrisObjectVariable <- generateVariable "constructorSwitchValue"
        ignore $ inferExpr idrisObjectType sc
        ignore $ addVariableType idrisObjectVariable idrisObjectType

    inferExprConstAlt : InferredType -> NamedConstAlt -> Asm InferredType
    inferExprConstAlt returnType (MkNConstAlt _ expr) = inferExprWithNewScope returnType expr

    inferExprWithNewScope : InferredType -> NamedCExp -> Asm InferredType
    inferExprWithNewScope returnType expr = do
         let fc = getFC expr
         let (lineStart, lineEnd) = getLineNumbers (startPos (toNonEmptyFC fc)) (endPos (toNonEmptyFC fc))
         withInferenceScope lineStart lineEnd $ inferExpr returnType expr

    inferConCaseExpr : InferredType -> List Name -> NamedCExp -> Asm InferredType
    inferConCaseExpr exprTy args expr = do
            traverse_ inferArg args
            inferExpr exprTy expr
        where
            inferArg : Name -> Asm ()
            inferArg var =
                let variableName = jvmSimpleName var
                in when (used variableName expr) $ createVariable variableName

    inferExprConAlt : InferredType -> NamedConAlt -> Asm InferredType
    inferExprConAlt exprTy (MkNConAlt _ _ _ args expr) = do
            let fc = getFC expr
            let (lineStart, lineEnd) = getLineNumbers (startPos (toNonEmptyFC fc)) (endPos (toNonEmptyFC fc))
            withInferenceScope lineStart lineEnd $ inferConCaseExpr exprTy args expr

    inferParameter : (NamedCExp, InferredType) -> Asm InferredType
    inferParameter (param, ty) = inferExpr ty param

    inferBinaryOp : InferredType -> NamedCExp -> NamedCExp -> Asm InferredType
    inferBinaryOp ty x y = do
        ignore $ inferExpr ty x
        ignore $ inferExpr ty y
        pure ty

    inferBoolOp : InferredType -> NamedCExp -> NamedCExp -> Asm InferredType
    inferBoolOp ty x y = do
        ignore $ inferExpr ty x
        ignore $ inferExpr ty y
        pure IBool

    inferUnaryOp : InferredType -> NamedCExp -> Asm InferredType
    inferUnaryOp ty x = do
      ignore $ inferExpr ty x
      Pure ty

    inferExtPrimArg : (NamedCExp, InferredType) -> Asm InferredType
    inferExtPrimArg (arg, ty) = inferExpr ty arg

    inferExtPrim : FC -> InferredType -> ExtPrim -> List NamedCExp -> Asm InferredType
    inferExtPrim fc returnType JvmInstanceMethodCall descriptors =
        inferExtPrim fc returnType JvmStaticMethodCall descriptors
    inferExtPrim _ returnType JvmStaticMethodCall [ret, NmPrimVal fc (Str fn), fargs, world]
      = do args <- getFArgs fargs
           argTypes <- traverse tySpec (map fst args)
           methodReturnType <- tySpec ret
           traverse_ inferExtPrimArg $ zip (map snd args) argTypes
           pure $ if methodReturnType == IVoid then inferredObjectType else methodReturnType
    inferExtPrim _ returnType NewArray [_, size, val, world] = do
        ignore $ inferExpr IInt size
        ignore $ inferExpr IUnknown val
        pure arrayListType
    inferExtPrim _ returnType ArrayGet [_, arr, pos, world] = do
        ignore $ inferExpr arrayListType arr
        ignore $ inferExpr IInt pos
        pure IUnknown
    inferExtPrim _ returnType ArraySet [_, arr, pos, val, world] = do
        ignore $ inferExpr arrayListType arr
        ignore $ inferExpr IInt pos
        ignore $ inferExpr IUnknown val
        pure inferredObjectType
    inferExtPrim _ returnType NewIORef [_, val, world] = do
        ignore $ inferExpr IUnknown val
        pure refType
    inferExtPrim _ returnType ReadIORef [_, ref, world] = do
        ignore $ inferExpr refType ref
        pure IUnknown
    inferExtPrim _ returnType WriteIORef [_, ref, val, world] = do
        ignore $ inferExpr refType ref
        ignore $ inferExpr IUnknown val
        pure inferredObjectType
    inferExtPrim _ returnType SysOS [] = pure inferredStringType
    inferExtPrim _ returnType SysCodegen [] = pure inferredStringType
    inferExtPrim _ returnType VoidElim _ = pure inferredObjectType
    inferExtPrim _ returnType MakeFuture [_, action] = do
        ignore $ inferExpr delayedType action
        pure inferredForkJoinTaskType
    inferExtPrim fc _ prim args = Throw fc $ "Unsupported external function " ++ show prim ++ "(" ++
        (show $ showNamedCExp 0 <$> args) ++ ")"

    inferExprLamWithParameterType : Maybe (Name, InferredType) -> (parameterValueExpr: Maybe (Asm ())) ->
        NamedCExp -> Asm InferredType
    inferExprLamWithParameterType parameterNameAndType parameterValueExpr expr = do
        let hasParameterValue = isJust parameterValueExpr
        let (_, lineStart, lineEnd) = getSourceLocation expr
        let jvmParameterNameAndType = (\(name, ty) => (jvmSimpleName name, ty)) <$> parameterNameAndType
        let lambdaType = getLambdaTypeByParameter (fst <$> parameterNameAndType)
        lambdaBodyReturnType <- withInferenceLambdaScope lineStart lineEnd (fst <$> parameterNameAndType) expr $ do
            when (lambdaType /= ThunkLambda) $
                traverse_ createAndAddVariable jvmParameterNameAndType
            maybe (Pure ()) id parameterValueExpr
            lambdaBodyReturnType <- inferExpr IUnknown expr
            currentScope <- getScope !getCurrentScopeIndex
            saveScope $ record {returnType = lambdaBodyReturnType} currentScope
            Pure lambdaBodyReturnType
        Pure $ if hasParameterValue
            then lambdaBodyReturnType
            else getLambdaInterfaceType lambdaType lambdaBodyReturnType
      where
        createAndAddVariable : (String, InferredType) -> Asm ()
        createAndAddVariable (name, ty) = do
            createVariable name
            ignore $ addVariableType name ty

    inferExprLamWithParameterType1 : (isCached : Bool) -> Maybe Name -> NamedCExp -> Asm InferredType
    inferExprLamWithParameterType1 True _ _ = Pure inferredLambdaType
    inferExprLamWithParameterType1 False parameterName expr =
      inferExprLamWithParameterType ((\name => (name, inferredObjectType)) <$> parameterName) Nothing expr

    inferExprLam : AppliedLambdaType -> (parameterValue: Maybe NamedCExp) -> (parameterName : Maybe Name) ->
                    NamedCExp -> Asm InferredType
    inferExprLam appliedLambdaType parameterValue@(Just value) (Just parameterName) lambdaBody = do
        valueType <-
            if appliedLambdaType == AppliedLambdaSwitch
                then case lambdaBody of
                    (NmConstCase _ _ alts _) => getConstantType alts
                    (NmConCase _ _ _ _) => Pure idrisObjectType
                    _ => Pure IUnknown
                else if appliedLambdaType == AppliedLambdaLet
                        then Pure inferredObjectType
                        else Pure IUnknown
        let shouldGenerateVariable = parameterName == extractedMethodArgumentName
        generatedJvmVariableName <-
            if shouldGenerateVariable
                then Pure $ jvmSimpleName parameterName ++ show !newDynamicVariableIndex
                else Pure $ jvmSimpleName parameterName
        let generatedVariableName =
            if shouldGenerateVariable
                then UN $ Basic generatedJvmVariableName
                else parameterName
        let valueExpr = NmLocal (getFC lambdaBody) generatedVariableName
        parentScope <- getScope !getCurrentScopeIndex
        inferExprLamWithParameterType (Just (generatedVariableName, valueType))
            (Just (inferValue parentScope shouldGenerateVariable generatedJvmVariableName valueType))
            (if appliedLambdaType == AppliedLambdaSwitch || appliedLambdaType == AppliedLambdaLet
                then substituteVariableSubMethodBody valueExpr lambdaBody
                else lambdaBody)
      where
        inferValue : Scope -> Bool -> String -> InferredType -> Asm ()
        inferValue enclosingScope shouldGenerateVariable variableName valueType = do
            lambdaScopeIndex <- getCurrentScopeIndex
            updateCurrentScopeIndex (index enclosingScope)
            when shouldGenerateVariable $ createVariable variableName
            ignore $ inferExpr valueType value
            ignore $ addVariableType variableName valueType
            updateCurrentScopeIndex lambdaScopeIndex
    inferExprLam _ _ p0 expr@(NmLam _ p1 (NmLam _ p2 (NmLam _ p3 (NmLam _ p4 (NmApp _ (NmRef _ name)
      [NmLocal _ arg0, NmLocal _ arg1, NmLocal _ arg2, NmLocal _ arg3, NmLocal _ arg4]))))) =
        inferExprLamWithParameterType1
          (maybe False ((==) arg0) p0 && p1 == arg1 && p2 == arg2 && p3 == arg3 && p4 == arg4) p0 expr
    inferExprLam _ _ p0 expr@(NmLam _ p1 (NmLam _ p2 (NmLam _ p3 (NmApp _ (NmRef _ name)
      [NmLocal _ arg0, NmLocal _ arg1, NmLocal _ arg2, NmLocal _ arg3])))) =
        inferExprLamWithParameterType1
          (maybe False ((==) arg0) p0 && p1 == arg1 && p2 == arg2 && p3 == arg3) p0 expr
    inferExprLam _ _ p0 expr@(NmLam _ p1 (NmLam _ p2 (NmApp _ (NmRef _ name)
      [NmLocal _ arg0, NmLocal _ arg1, NmLocal _ arg2]))) =
        inferExprLamWithParameterType1 (maybe False ((==) arg0) p0 && p1 == arg1 && p2 == arg2) p0 expr
    inferExprLam _ _ p0 expr@(NmLam _ p1 (NmApp _ (NmRef _ name) [NmLocal _ arg0, NmLocal _ arg1])) =
        inferExprLamWithParameterType1 (maybe False ((==) arg0) p0 && p1 == arg1) p0 expr
    inferExprLam _ _ p0 expr@(NmApp _ (NmRef _ _) [NmLocal _ b]) =
      inferExprLamWithParameterType1 (maybe False ((==) b) p0) p0 expr
    inferExprLam _ _ p0 expr@(NmLam _ c (NmLam _ a (NmLocal _ b))) =
      inferExprLamWithParameterType1 (isJust p0 && (c == b || a == b)) p0 expr
    inferExprLam _ _ p0 expr@(NmLam _ a (NmLocal _ b)) =
      inferExprLamWithParameterType1 (maybe False ((==) b) p0 || (isJust p0 && a == b)) p0 expr
    inferExprLam _ _ p0 expr@(NmLocal _ b) =
      inferExprLamWithParameterType1 (maybe False ((==) b) p0) p0 expr
    inferExprLam _ _ p0 expr = inferExprLamWithParameterType1 False p0 expr

    inferExprLet : FC -> InferredType -> (x : Name) -> NamedCExp -> NamedCExp -> Asm InferredType
    inferExprLet fc exprTy var value expr = do
        let (lineStart, lineEnd) = getLineNumbers (startPos (toNonEmptyFC fc)) (endPos (toNonEmptyFC fc))
        let varName = jvmSimpleName var
        createVariable varName
        let (_, lineStart, lineEnd) = getSourceLocation value
        valueTy <- withInferenceScope lineStart lineEnd $ inferExpr IUnknown value
        ignore $ addVariableType varName (if isThunkType valueTy then inferredObjectType else valueTy)
        let (_, lineStart, lineEnd) = getSourceLocation expr
        withInferenceScope lineStart lineEnd $ inferExpr exprTy expr

    inferSelfTailCallParameter : Map Int InferredType -> Map Int String -> (NamedCExp, Int) -> Asm ()
    inferSelfTailCallParameter types argumentNameByIndices (arg, index) = do
        optTy <- LiftIo $ Map.get types index
        let variableType = fromMaybe IUnknown optTy
        ty <- inferExpr variableType arg
        optName <- LiftIo $ Map.get {value=String} argumentNameByIndices index
        maybe (Pure ()) (doAddVariableType ty) optName
      where
        doAddVariableType : InferredType -> String -> Asm ()
        doAddVariableType ty name = do
            ignore $ addVariableType name ty
            case arg of
                NmLocal _ loc => do
                    let valueVariableName = jvmSimpleName loc
                    valueVariableIndex <- retrieveVariableIndex valueVariableName
                    when (index /= valueVariableIndex) $ createNewVariable "tailRecArg" ty
                _ => createNewVariable "tailRecArg" ty

    inferExprApp : InferredType -> NamedCExp -> Asm InferredType
    inferExprApp exprTy app@(NmApp _ (NmRef _ (UN (Basic "$jvmTailRec"))) args) =
        case args of
            [] => Pure exprTy
            args@(_ :: argsTail) => do
                types <- retrieveVariableTypesAtScope !getCurrentScopeIndex
                argumentNameByIndices <- LiftIo $ Map.transpose $ variableIndices !(getScope 0)
                traverse_ (inferSelfTailCallParameter types argumentNameByIndices) $
                    zip args [0 .. the Int $ cast $ length argsTail]
                Pure exprTy
    inferExprApp exprTy (NmApp _ (NmRef _ idrisName) args) = do
        let functionName = jvmName idrisName
        functionType <- case !(findFunctionType functionName) of
            Just ty => Pure ty
            Nothing => Pure $ MkInferredFunctionType inferredObjectType $ replicate (length args) inferredObjectType
        let argsWithTypes = zip args (parameterTypes functionType)
        traverse_ inferParameter argsWithTypes
        Pure $ returnType functionType
    inferExprApp exprTy (NmApp _ lambdaVariable args) = do
        ignore $ inferExpr inferredLambdaType lambdaVariable
        let argsWithTypes = zip args (replicate (length args) IUnknown)
        traverse_ inferParameter argsWithTypes
        pure IUnknown
    inferExprApp _ _ = Throw emptyFC "Not a function application"

    inferExprCon : InferredType -> String -> Name -> List NamedCExp -> Asm InferredType
    inferExprCon exprTy fileName name args = do
        let argsWithTypes = zip args (replicate (length args) inferredObjectType)
        traverse_ inferParameter argsWithTypes
        pure idrisObjectType

    inferExprCast : InferredType -> InferredType -> NamedCExp -> Asm InferredType
    inferExprCast sourceType targetType expr = do
        ignore $ inferExpr sourceType expr
        pure targetType

    inferExprOp : PrimFn arity -> Vect arity NamedCExp -> Asm InferredType
    inferExprOp (Add Bits8Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (Sub Bits8Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (Mul Bits8Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (Div Bits8Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (Mod Bits8Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (Neg Bits8Type) [x] = inferUnaryOp IInt x
    inferExprOp (ShiftL Bits8Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (ShiftR Bits8Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (BAnd Bits8Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (BOr Bits8Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (BXOr Bits8Type) [x, y] = inferBinaryOp IInt x y

    inferExprOp (Add Bits16Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (Sub Bits16Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (Mul Bits16Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (Div Bits16Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (Mod Bits16Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (Neg Bits16Type) [x] = inferUnaryOp IInt x
    inferExprOp (ShiftL Bits16Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (ShiftR Bits16Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (BAnd Bits16Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (BOr Bits16Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (BXOr Bits16Type) [x, y] = inferBinaryOp IInt x y

    inferExprOp (Add Bits32Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (Sub Bits32Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (Mul Bits32Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (Div Bits32Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (Mod Bits32Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (Neg Bits32Type) [x] = inferUnaryOp IInt x
    inferExprOp (ShiftL Bits32Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (ShiftR Bits32Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (BAnd Bits32Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (BOr Bits32Type) [x, y] = inferBinaryOp IInt x y
    inferExprOp (BXOr Bits32Type) [x, y] = inferBinaryOp IInt x y

    inferExprOp (Add Bits64Type) [x, y] = inferBinaryOp ILong x y
    inferExprOp (Sub Bits64Type) [x, y] = inferBinaryOp ILong x y
    inferExprOp (Mul Bits64Type) [x, y] = inferBinaryOp ILong x y
    inferExprOp (Div Bits64Type) [x, y] = inferBinaryOp ILong x y
    inferExprOp (Mod Bits64Type) [x, y] = inferBinaryOp ILong x y
    inferExprOp (Neg Bits64Type) [x] = inferUnaryOp ILong x
    inferExprOp (ShiftL Bits64Type) [x, y] = inferBinaryOp ILong x y
    inferExprOp (ShiftR Bits64Type) [x, y] = inferBinaryOp ILong x y
    inferExprOp (BAnd Bits64Type) [x, y] = inferBinaryOp ILong x y
    inferExprOp (BOr Bits64Type) [x, y] = inferBinaryOp ILong x y
    inferExprOp (BXOr Bits64Type) [x, y] = inferBinaryOp ILong x y

    inferExprOp (Add IntType) [x, y] = inferBinaryOp IInt x y
    inferExprOp (Sub IntType) [x, y] = inferBinaryOp IInt x y
    inferExprOp (Mul IntType) [x, y] = inferBinaryOp IInt x y
    inferExprOp (Div IntType) [x, y] = inferBinaryOp IInt x y
    inferExprOp (Mod IntType) [x, y] = inferBinaryOp IInt x y
    inferExprOp (Neg IntType) [x] = inferUnaryOp IInt x
    inferExprOp (ShiftL IntType) [x, y] = inferBinaryOp IInt x y
    inferExprOp (ShiftR IntType) [x, y] = inferBinaryOp IInt x y
    inferExprOp (BAnd IntType) [x, y] = inferBinaryOp IInt x y
    inferExprOp (BOr IntType) [x, y] = inferBinaryOp IInt x y
    inferExprOp (BXOr IntType) [x, y] = inferBinaryOp IInt x y

    inferExprOp (Add IntegerType) [x, y] = inferBinaryOp inferredBigIntegerType x y
    inferExprOp (Sub IntegerType) [x, y] = inferBinaryOp inferredBigIntegerType x y
    inferExprOp (Mul IntegerType) [x, y] = inferBinaryOp inferredBigIntegerType x y
    inferExprOp (Div IntegerType) [x, y] = inferBinaryOp inferredBigIntegerType x y
    inferExprOp (Mod IntegerType) [x, y] = inferBinaryOp inferredBigIntegerType x y
    inferExprOp (Neg IntegerType) [x] = inferUnaryOp inferredBigIntegerType x
    inferExprOp (ShiftL IntegerType) [x, y] = inferBinaryOp inferredBigIntegerType x y
    inferExprOp (ShiftR IntegerType) [x, y] = inferBinaryOp inferredBigIntegerType x y
    inferExprOp (BAnd IntegerType) [x, y] = inferBinaryOp inferredBigIntegerType x y
    inferExprOp (BOr IntegerType) [x, y] = inferBinaryOp inferredBigIntegerType x y
    inferExprOp (BXOr IntegerType) [x, y] = inferBinaryOp inferredBigIntegerType x y

    inferExprOp (Add DoubleType) [x, y] = inferBinaryOp IDouble x y
    inferExprOp (Sub DoubleType) [x, y] = inferBinaryOp IDouble x y
    inferExprOp (Mul DoubleType) [x, y] = inferBinaryOp IDouble x y
    inferExprOp (Div DoubleType) [x, y] = inferBinaryOp IDouble x y
    inferExprOp (Neg DoubleType) [x] = inferUnaryOp IDouble x

    inferExprOp (LT Bits8Type) [x, y] = inferBoolOp IInt x y
    inferExprOp (LT Bits16Type) [x, y] = inferBoolOp IInt x y
    inferExprOp (LT Bits32Type) [x, y] = inferBoolOp IInt x y
    inferExprOp (LT Bits64Type) [x, y] = inferBoolOp ILong x y
    inferExprOp (LT IntType) [x, y] = inferBoolOp IInt x y
    inferExprOp (LT CharType) [x, y] = inferBoolOp IChar x y
    inferExprOp (LT IntegerType) [x, y] = inferBoolOp inferredBigIntegerType x y
    inferExprOp (LT DoubleType) [x, y] = inferBoolOp IDouble x y
    inferExprOp (LT StringType) [x, y] = inferBoolOp inferredStringType x y

    inferExprOp (LTE Bits8Type) [x, y] = inferBoolOp IInt x y
    inferExprOp (LTE Bits16Type) [x, y] = inferBoolOp IInt x y
    inferExprOp (LTE Bits32Type) [x, y] = inferBoolOp IInt x y
    inferExprOp (LTE Bits64Type) [x, y] = inferBoolOp ILong x y
    inferExprOp (LTE IntType) [x, y] = inferBoolOp IInt x y
    inferExprOp (LTE CharType) [x, y] = inferBoolOp IChar x y
    inferExprOp (LTE IntegerType) [x, y] = inferBoolOp inferredBigIntegerType x y
    inferExprOp (LTE DoubleType) [x, y] = inferBoolOp IDouble x y
    inferExprOp (LTE StringType) [x, y] = inferBoolOp inferredStringType x y

    inferExprOp (EQ Bits8Type) [x, y] = inferBoolOp IInt x y
    inferExprOp (EQ Bits16Type) [x, y] = inferBoolOp IInt x y
    inferExprOp (EQ Bits32Type) [x, y] = inferBoolOp IInt x y
    inferExprOp (EQ Bits64Type) [x, y] = inferBoolOp ILong x y
    inferExprOp (EQ IntType) [x, y] = inferBoolOp IInt x y
    inferExprOp (EQ CharType) [x, y] = inferBoolOp IChar x y
    inferExprOp (EQ IntegerType) [x, y] = inferBoolOp inferredBigIntegerType x y
    inferExprOp (EQ DoubleType) [x, y] = inferBoolOp IDouble x y
    inferExprOp (EQ StringType) [x, y] = inferBoolOp inferredStringType x y

    inferExprOp (GT Bits8Type) [x, y] = inferBoolOp IInt x y
    inferExprOp (GT Bits16Type) [x, y] = inferBoolOp IInt x y
    inferExprOp (GT Bits32Type) [x, y] = inferBoolOp IInt x y
    inferExprOp (GT Bits64Type) [x, y] = inferBoolOp ILong x y
    inferExprOp (GT IntType) [x, y] = inferBoolOp IInt x y
    inferExprOp (GT CharType) [x, y] = inferBoolOp IChar x y
    inferExprOp (GT IntegerType) [x, y] = inferBoolOp inferredBigIntegerType x y
    inferExprOp (GT DoubleType) [x, y] = inferBoolOp IDouble x y
    inferExprOp (GT StringType) [x, y] = inferBoolOp inferredStringType x y

    inferExprOp (GTE Bits8Type) [x, y] = inferBoolOp IInt x y
    inferExprOp (GTE Bits16Type) [x, y] = inferBoolOp IInt x y
    inferExprOp (GTE Bits32Type) [x, y] = inferBoolOp IInt x y
    inferExprOp (GTE Bits64Type) [x, y] = inferBoolOp ILong x y
    inferExprOp (GTE IntType) [x, y] = inferBoolOp IInt x y
    inferExprOp (GTE CharType) [x, y] = inferBoolOp IChar x y
    inferExprOp (GTE IntegerType) [x, y] = inferBoolOp inferredBigIntegerType x y
    inferExprOp (GTE DoubleType) [x, y] = inferBoolOp IDouble x y
    inferExprOp (GTE StringType) [x, y] = inferBoolOp inferredStringType x y

    inferExprOp StrLength [x] = do
        ignore $ inferExpr inferredStringType x
        pure IInt
    inferExprOp StrHead [x] = do
        ignore $ inferExpr inferredStringType x
        pure IChar
    inferExprOp StrTail [x] = do
        ignore $ inferExpr inferredStringType x
        pure inferredStringType
    inferExprOp StrIndex [x, i] = do
        ignore $ inferExpr inferredStringType x
        ignore $ inferExpr IInt i
        pure IChar
    inferExprOp StrCons [x, y] = do
        ignore $ inferExpr IChar x
        ignore $ inferExpr inferredStringType y
        pure inferredStringType
    inferExprOp StrAppend [x, y] = inferBinaryOp inferredStringType x y
    inferExprOp StrReverse [x] = do
        ignore $ inferExpr inferredStringType x
        pure inferredStringType
    inferExprOp StrSubstr [offset, len, str] = do
        ignore $ inferExpr IInt offset
        ignore $ inferExpr IInt len
        ignore $ inferExpr inferredStringType str
        pure inferredStringType
    inferExprOp DoubleExp [x] = inferUnaryOp IDouble x
    inferExprOp DoubleLog [x] = inferUnaryOp IDouble x
    inferExprOp DoubleSin [x] = inferUnaryOp IDouble x
    inferExprOp DoubleCos [x] = inferUnaryOp IDouble x
    inferExprOp DoubleTan [x] = inferUnaryOp IDouble x
    inferExprOp DoubleASin [x] = inferUnaryOp IDouble x
    inferExprOp DoubleACos [x] = inferUnaryOp IDouble x
    inferExprOp DoubleATan [x] = inferUnaryOp IDouble x
    inferExprOp DoubleSqrt [x] = inferUnaryOp IDouble x
    inferExprOp DoubleFloor [x] = inferUnaryOp IDouble x
    inferExprOp DoubleCeiling [x] = inferUnaryOp IDouble x

    inferExprOp (Cast Bits8Type Bits16Type) [x] = inferExprCast IInt IInt x
    inferExprOp (Cast Bits8Type Bits32Type) [x] = inferExprCast IInt IInt x
    inferExprOp (Cast Bits8Type IntType) [x] = inferExprCast IInt IInt x
    inferExprOp (Cast Bits8Type Bits64Type) [x] = inferExprCast IInt ILong x
    inferExprOp (Cast Bits8Type IntegerType) [x] = inferExprCast IInt inferredBigIntegerType x
    inferExprOp (Cast Bits8Type StringType) [x] = inferExprCast IInt inferredStringType x

    inferExprOp (Cast Bits16Type Bits8Type) [x] = inferExprCast IInt IInt x
    inferExprOp (Cast Bits16Type Bits32Type) [x] = inferExprCast IInt IInt x
    inferExprOp (Cast Bits16Type IntType) [x] = inferExprCast IInt IInt x
    inferExprOp (Cast Bits16Type Bits64Type) [x] = inferExprCast IInt ILong x
    inferExprOp (Cast Bits16Type IntegerType) [x] = inferExprCast IInt inferredBigIntegerType x
    inferExprOp (Cast Bits16Type StringType) [x] = inferExprCast IInt inferredStringType x

    inferExprOp (Cast Bits32Type Bits8Type) [x] = inferExprCast IInt IInt x
    inferExprOp (Cast Bits32Type Bits16Type) [x] = inferExprCast IInt IInt x
    inferExprOp (Cast Bits32Type IntType) [x] = inferExprCast IInt IInt x
    inferExprOp (Cast Bits32Type Bits64Type) [x] = inferExprCast IInt ILong x
    inferExprOp (Cast Bits32Type IntegerType) [x] = inferExprCast IInt inferredBigIntegerType x
    inferExprOp (Cast Bits32Type StringType) [x] = inferExprCast IInt inferredStringType x

    inferExprOp (Cast Bits64Type Bits8Type) [x] = inferExprCast ILong IInt x
    inferExprOp (Cast Bits64Type Bits16Type) [x] = inferExprCast ILong IInt x
    inferExprOp (Cast Bits64Type Bits32Type) [x] = inferExprCast ILong IInt x
    inferExprOp (Cast Bits64Type IntType) [x] = inferExprCast ILong IInt x
    inferExprOp (Cast Bits64Type IntegerType) [x] = inferExprCast ILong inferredBigIntegerType x
    inferExprOp (Cast Bits64Type StringType) [x] = inferExprCast ILong inferredStringType x

    inferExprOp (Cast IntType Bits8Type) [x] = inferExprCast IInt IInt x
    inferExprOp (Cast IntType Bits16Type) [x] = inferExprCast IInt IInt x
    inferExprOp (Cast IntType Bits32Type) [x] = inferExprCast IInt IInt x
    inferExprOp (Cast IntType Bits64Type) [x] = inferExprCast IInt ILong x
    inferExprOp (Cast IntType IntegerType) [x] = inferExprCast IInt inferredBigIntegerType x
    inferExprOp (Cast IntType StringType) [x] = inferExprCast IInt inferredStringType x

    inferExprOp (Cast IntegerType Bits8Type)  [x] = inferExprCast inferredBigIntegerType IInt x
    inferExprOp (Cast IntegerType Bits16Type) [x] = inferExprCast inferredBigIntegerType IInt x
    inferExprOp (Cast IntegerType Bits32Type) [x] = inferExprCast inferredBigIntegerType IInt x
    inferExprOp (Cast IntegerType IntType) [x] = inferExprCast inferredBigIntegerType IInt x
    inferExprOp (Cast IntegerType Bits64Type) [x] = inferExprCast inferredBigIntegerType ILong x
    inferExprOp (Cast IntegerType StringType) [x] = inferExprCast inferredBigIntegerType inferredStringType x

    inferExprOp (Cast DoubleType StringType) [x] = inferExprCast IDouble inferredStringType x
    inferExprOp (Cast CharType StringType) [x] = inferExprCast IChar inferredStringType x
    inferExprOp (Cast DoubleType IntegerType) [x] = inferExprCast IDouble inferredBigIntegerType x
    inferExprOp (Cast CharType IntegerType) [x] = inferExprCast IChar inferredBigIntegerType x
    inferExprOp (Cast StringType IntegerType) [x] = inferExprCast inferredStringType inferredBigIntegerType x
    inferExprOp (Cast DoubleType IntType) [x] = inferExprCast IDouble IInt x
    inferExprOp (Cast StringType IntType) [x] = inferExprCast inferredStringType IInt x
    inferExprOp (Cast CharType IntType) [x] = inferExprCast IChar IInt x
    inferExprOp (Cast IntegerType DoubleType) [x] = inferExprCast inferredBigIntegerType IDouble x
    inferExprOp (Cast IntType DoubleType) [x] = inferExprCast IInt IDouble x
    inferExprOp (Cast StringType DoubleType) [x] = inferExprCast inferredStringType IDouble x
    inferExprOp (Cast IntType CharType) [x] = inferExprCast IInt IChar x

    inferExprOp BelieveMe [_, _, x] = Pure IUnknown
    inferExprOp Crash [_, msg] = Pure IUnknown
    inferExprOp op _ = Throw emptyFC ("Unsupported primitive function " ++ show op)

optimize : Jname -> TailCallCategory -> NamedCExp -> Asm NamedCExp
optimize jname tailCallCategory expr = do
  inlinedAndTailRecursionMarkedExpr <- markTailRecursion . liftToLambda $ expr
  shouldTrampoline <- LiftIo $ AsmGlobalState.shouldTrampoline !getGlobalState (show jname)
  Pure $ if shouldTrampoline && hasNonSelfTailCall tailCallCategory
    then trampolineExpression True inlinedAndTailRecursionMarkedExpr
    else inlinedAndTailRecursionMarkedExpr

export
%inline
emptyFunction : NamedCExp
emptyFunction = NmCrash emptyFC "uninitialized function"

showScopes : Int -> Asm ()
showScopes n = do
    scope <- getScope n
    debug $ show scope
    when (n > 0) $ showScopes (n - 1)

export
inferDef : String -> Name -> FC -> NamedDef -> Asm ()
inferDef programName idrisName fc (MkNmFun args body) = do
    let jname = jvmName idrisName
    let hasSelfTailCall = hasTailCall (== idrisName) body
    let hasNonSelfTailCall = hasTailCall (/= idrisName) body
    let jvmClassAndMethodName = getIdrisFunctionName programName (className jname) (methodName jname)
    let tailCallCategory = MkTailCallCategory hasSelfTailCall hasNonSelfTailCall
    let arity = length args
    let arityInt = the Int $ cast arity
    let expr = if arityInt == 0 then NmDelay fc LLazy body else body
    let argumentNames = jvmSimpleName <$> args
    argIndices <- LiftIo $ getArgumentIndices arityInt argumentNames
    let initialArgumentTypes = replicate arity inferredObjectType
    let inferredFunctionType = MkInferredFunctionType inferredObjectType initialArgumentTypes
    argumentTypesByName <- LiftIo $ Map.fromList $ zip argumentNames initialArgumentTypes
    scopes <- LiftIo $ JList.new {a=Scope}
    let function = MkFunction jname inferredFunctionType scopes 0 jvmClassAndMethodName emptyFunction
    setCurrentFunction function
    LiftIo $ AsmGlobalState.addFunction !getGlobalState jname function
    let shouldDebugExpr = shouldDebug &&
        (fromMaybe True $ ((\name => name `isInfixOf` (getSimpleName jname)) <$> debugFunction))
    when shouldDebugExpr $
      debug $ "Inferring " ++ (className jvmClassAndMethodName) ++ "." ++ (methodName jvmClassAndMethodName) ++
        ":\n" ++ showNamedCExp 0 expr
    optimizedExpr <- optimize jname tailCallCategory expr
    updateCurrentFunction $ record { optimizedBody = optimizedExpr }

    resetScope
    scopeIndex <- newScopeIndex
    let (_, lineStart, lineEnd) = getSourceLocation expr
    allVariableTypes <- LiftIo $ Map.newTreeMap {key=Int} {value=InferredType}
    allVariableIndices <- LiftIo $ Map.newTreeMap {key=String} {value=Int}
    let functionScope =
        MkScope scopeIndex Nothing argumentTypesByName allVariableTypes argIndices
            allVariableIndices IUnknown arityInt (lineStart, lineEnd) ("", "") []

    saveScope functionScope
    retTy <- inferExpr IUnknown optimizedExpr
    updateScopeVariableTypes arity
    updateCurrentFunction $ record { inferredFunctionType = inferredFunctionType }
  where
    getArgumentTypes : List String -> Asm (List InferredType)
    getArgumentTypes argumentNames = do
        argumentIndicesByName <- getVariableIndicesByName 0
        argumentTypesByIndex <- getVariableTypesAtScope 0
        LiftIo $ go argumentIndicesByName argumentTypesByIndex argumentNames
      where
        go : Map String Int -> Map Int InferredType -> List String -> IO (List InferredType)
        go argumentIndicesByName argumentTypesByIndex argumentNames = do
            types <- go1 [] argumentNames
            pure $ reverse types
          where
            go1 : List InferredType -> List String -> IO (List InferredType)
            go1 acc [] = pure acc
            go1 acc (arg :: args) = do
                optIndex <- Map.get {value=Int} argumentIndicesByName arg
                ty <- case optIndex of
                    Just index => do
                        optTy <- Map.get argumentTypesByIndex index
                        pure $ fromMaybe IUnknown optTy
                    Nothing => pure IUnknown
                go1 (ty :: acc) args

inferDef programName n fc (MkNmError expr) = inferDef programName n fc (MkNmFun [] expr)

inferDef programName idrisName fc def@(MkNmForeign foreignDescriptors argumentTypes returnType) =
    inferForeign programName idrisName fc foreignDescriptors argumentTypes returnType

inferDef _ _ _ _ = Pure ()


text:
module Data.HashMap

import Data.Array16
import public Data.Hashable
import Data.HashMap.Internal as Internal
import Data.List
import Data.String

||| Hash map implemented with Hash-array mapped tries
export
data HashMap : Type -> Type -> Type where
    MkHM : (eq : k -> k -> Bool) -> (hws : Bits64 -> k -> Bits64) -> HashArrayMapTrie k v -> HashMap k v

||| Unsafely get the internals of a HashMap.
export
unsafeFoldHashMap : ((eq : k -> k -> Bool) -> (hws : Bits64 -> k -> Bits64) -> HashArrayMapTrie k v -> r) -> HashMap k v -> r
unsafeFoldHashMap f (MkHM eq hws m) = f eq hws m

||| Lookup the value at `k` if it exists.
export
lookup : k -> HashMap k v -> Maybe v
lookup k (MkHM eq hws m) = Internal.lookup eq hws bitMask0 (hws defaultSalt k) k m

||| Insert a value at a key, replacing it if it already exists.
export
insert : k -> v -> HashMap k v -> HashMap k v
insert k v (MkHM eq hws m) = MkHM eq hws $ Internal.insert eq hws defaultSalt bitMask0 (hws defaultSalt k) k v m

||| Delete the value at a key.
export
delete : k -> HashMap k v -> HashMap k v
delete k (MkHM eq hws m) = MkHM eq hws $ Internal.delete eq hws bitMask0 (hws defaultSalt k) k m

||| Alter the value at a key.
-- TODO: Make faster.
export
alter : k -> (Maybe v -> Maybe v) -> HashMap k v -> HashMap k v
alter k f m = case f (lookup k m) of
    Nothing => delete k m
    Just v => insert k v m

||| Empty HashMap.
export
empty : Eq k => Hashable k => HashMap k v
empty = MkHM (==) hashWithSalt Internal.empty

||| Construct a HashMap from a single key and value.
export
singleton : Eq k => Hashable k => k -> v -> HashMap k v
singleton k v = MkHM (==) hashWithSalt $ Internal.singleton (hashWithSalt defaultSalt k) k v

||| Construct a HashMap from a `Foldable` structure of key-value pairs.
export
fromFoldable : Foldable f => Eq k => Hashable k => f (k, v) -> HashMap k v
fromFoldable kvs =
    MkHM (==) hashWithSalt
        $ foldr (\(k, v) =>
            Internal.insert (==) hashWithSalt defaultSalt bitMask0 (hashWithSalt defaultSalt k) k v)
            Internal.empty kvs

||| Construct a HashMap from a List of key-value pairs.
||| Specialised and inlined for speed.
export
fromList : Eq k => Hashable k => List (k, v) -> HashMap k v
fromList kvs = MkHM (==) hashWithSalt (go kvs Internal.empty)
  where
    go : List (k, v) -> HashArrayMapTrie k v -> HashArrayMapTrie k v
    go [] m = m
    go ((k, v) :: kvs) m =
        go kvs
            $ Internal.insert (==) hashWithSalt defaultSalt bitMask0
                (hashWithSalt defaultSalt k) k v m

||| Fold a hashmap with the key.
||| Note: Due to hashing keys and values are stored in an arbitrary order.
export
foldWithKey : (k -> v -> acc -> acc) -> acc -> HashMap k v -> acc
foldWithKey f z (MkHM _ _ m) = Internal.foldWithKey f z m

-- Should this exist given the lack of order?
export
Foldable (HashMap k) where
    foldl f = foldWithKey (const $ flip f)
    foldr f = foldWithKey (const f)

||| Convert a HashMap to a List of key-value pairs.
export
toList : HashMap k v -> List (k, v)
toList = foldWithKey (\k, v, acc => (k, v) :: acc) []

export
Show k => Show v => Show (HashMap k v) where
    showPrec d hm = showCon d "fromList" $ showArg $ Data.HashMap.toList hm

||| Merge 2 hashmaps with a preference for entries in the left map.
export
mergeL : HashMap k v -> HashMap k v -> HashMap k v
mergeL m0 m1 = foldWithKey insert m1 m0

||| Merge 2 hashmaps with a preference for entries in the right map.
export
mergeR : HashMap k v -> HashMap k v -> HashMap k v
mergeR m0 m1 = foldWithKey insert m0 m1

||| Merges 2 hashmaps with a preference for entries in the left map.
Semigroup (HashMap k v) where
    (<+>) = mergeL

||| Merges 2 hashmaps with a preference for entries in the right map.
[HMRightSemigroup] Semigroup (HashMap k v) where
    (<+>) = mergeR

Eq k => Hashable k => Monoid (HashMap k v) where
    neutral = empty

[HMRightMonoid] Eq k => Hashable k => Monoid (HashMap k v) using HMRightSemigroup where
    neutral = empty

ext: idr


text:
module Network.Curl.Global

import Network.Curl.Types
import Network.Curl.Prim.Global

||| We use CURL_GLOBAL_ALL since that's the only useful flag in this libcurl
||| version. CURL_GLOBAL_ALL = 3 on my system
export
curlGlobalInit : HasIO io => io CurlECode
curlGlobalInit = curl_global_init

export
curlGlobalCleanup : HasIO io => io ()
curlGlobalCleanup = curl_global_cleanup


text:
module Shape

public export
data Shape = Triangle Double Double
           | Rectangle Double Double
           | Circle Double

private
rectangle_area : Double -> Double -> Double
rectangle_area width height = width * height

export
area : Shape -> Double
area (Triangle base height) = 0.5 * rectangle_area base height
area (Rectangle length height) = rectangle_area length height
area (Circle radius) = pi * radius * radius


text:
module Decidable.Finite.Fin

import Data.Nat
import Data.Nat.Order
import Data.Fin
import Decidable.Decidable.Extra
import Data.Fin.Extra

||| Given a decidable predicate on Fin n,
||| it's decidable whether any number in Fin n satisfies it.
public export
finiteDecEx : {n : Nat} -> {0 p : Fin n -> Type} ->
  (pdec : (k : Fin n) -> Dec (p k)) ->
  Dec (k ** p k)
finiteDecEx {n = Z} pdec = No (absurd . fst)
finiteDecEx {n = S n} pdec =
  case pdec FZ of
    Yes pz => Yes (FZ ** pz)
    No npz => case finiteDecEx {n = n} (\ k => pdec (FS k)) of
      Yes (k ** pk) => Yes (FS k ** pk)
      No npk => No $ \case
        (FZ ** pz) => absurd (npz pz)
        (FS k ** pk) => absurd (npk (k ** pk))

||| Given a decidable predicate on Fin n,
||| it's decidable whether all numbers in Fin n satisfy it.
public export
finiteDecAll : {n : Nat} -> {0 p : Fin n -> Type} ->
  (pdec : (k : Fin n) -> Dec (p k)) ->
  Dec ((k : Fin n) -> p k)
finiteDecAll pdec  = notExistsNotForall pdec $ finiteDecEx (\ x => negateDec (pdec x))


text:
module IdrisJvm.Core.Constant

import IdrisJvm.Core.Asm
import IdrisJvm.Core.Common
import IdrisJvm.IR.Types

import IdrisJvm.Core.Common

%access public export

newBigInteger : String -> Asm ()
newBigInteger "0" = Field FGetStatic "java/math/BigInteger" "ZERO" "Ljava/math/BigInteger;"
newBigInteger "1" = Field FGetStatic "java/math/BigInteger" "ONE" "Ljava/math/BigInteger;"
newBigInteger "10" = Field FGetStatic "java/math/BigInteger" "TEN" "Ljava/math/BigInteger;"
newBigInteger i = do
  New "java/math/BigInteger"
  Dup
  Ldc $ StringConst i
  InvokeMethod InvokeSpecial "java/math/BigInteger" "<init>" "(Ljava/lang/String;)V" False

cgConst : (InferredType -> Asm ()) -> Const -> Asm ()
cgConst ret (B8 i) = do Iconst $ prim__zextB8_Int i; ret IInt
cgConst ret (B16 i) = do Iconst $ prim__zextB16_Int i; ret IInt
cgConst ret (B32 i) = do Iconst i; ret IInt
cgConst ret (B64 i) = do Ldc $ LongConst i; ret ILong
cgConst ret (I i) = do Iconst i; ret IInt
cgConst ret (Fl d) = do Ldc $ DoubleConst d; ret IDouble
cgConst ret (Ch c) = do Iconst (cast c); ret IChar
cgConst ret (BI i) = do newBigInteger i; ret inferredBigIntegerType
cgConst ret (Str s) = do Ldc $ StringConst s; ret inferredStringType
cgConst ret TheWorld = do Iconst 0; ret IInt
cgConst ret x = if isTypeConst x
              then do Iconst 0; ret IInt
              else jerror $ "Constant " ++ show x ++ " not compilable yet"


text:
module AwesomeLib

data Awesome : Type -> Type where
  MkAwesome : a -> Awesome a

max_stars_repo_name: sualitu/thesis

max_issues_repo_name: sualitu/thesis

max_forks_repo_name: sualitu/thesis


text:
module Twist

import Control.Algebra
import Data.Fin
import Data.Vect

import Twist.Cycle
import Twist.Face
import Twist.Move
import Twist.Rotation
import Twist.Util

%default total

Face' : Type
Face' = Face 6

Rotation' : Face' -> Type
Rotation' = Rotation Face' (Cycle 4)

data MoveSeq : Type where
  Nil : MoveSeq
  (::) : Rotation' f -> MoveSeq -> MoveSeq

Show MoveSeq where
  show Nil = ""
  show (x :: Nil) = show x
  show (x :: xs) = show xs ++ " " ++ show x

||| Concatenate two MoveSeqs together (in reverse order!)
(++) : MoveSeq -> MoveSeq -> MoveSeq
Nil ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

reverse : MoveSeq -> MoveSeq
reverse m = reverse' Nil m where
  reverse' : MoveSeq -> MoveSeq -> MoveSeq
  reverse' acc Nil = acc
  reverse' acc (x :: xs) = reverse' (x :: acc) xs

inverseEach : MoveSeq -> MoveSeq
inverseEach Nil = Nil
inverseEach (x :: xs) = inverse x :: inverseEach xs

||| Construct a MoveSeq from a single Rotation'.
move : Rotation' f -> MoveSeq
move r = r :: Nil

twist : Face' -> MoveSeq
twist f = move (rotate f)

twist' : Face' -> MoveSeq
twist' f = move (rotate' f)

||| Combine two Rotation's into a MoveSeq.
combine : (Rotation' f) -> (Rotation' g) -> MoveSeq
combine {f=R} {g=R} first second = (first <+> second) :: Nil
combine {f=L} {g=L} first second = (first <+> second) :: Nil
combine {f=U} {g=U} first second = (first <+> second) :: Nil
combine {f=D} {g=D} first second = (first <+> second) :: Nil
combine {f=F} {g=F} first second = (first <+> second) :: Nil
combine {f=B} {g=B} first second = (first <+> second) :: Nil
combine {f=Dbg n} {g=Dbg m} first second =  second :: first :: Nil
combine {f=_} {g=_} first second = second :: first :: Nil

simplify : MoveSeq -> MoveSeq
simplify Nil = Nil
simplify (r :: Nil) = r :: Nil
simplify (last :: prev :: xs) = (combine prev last) ++ xs

Semigroup MoveSeq where
  xs <+> Nil = xs
  xs <+> (last :: ys) = simplify (last :: (xs <+> ys))

Monoid MoveSeq where
  neutral = Nil

Group MoveSeq where
  inverse m = inverse' Nil m where
    inverse' : MoveSeq -> MoveSeq -> MoveSeq
    inverse' acc Nil = acc
    inverse' acc (x :: xs) = inverse' (inverse x :: acc) xs

conjugate : MoveSeq -> MoveSeq -> MoveSeq
conjugate a b = a <+> b <+> (inverse a)

commutator : MoveSeq -> MoveSeq -> MoveSeq
commutator a b = a <+> b <+> (inverse a) <+> (inverse b)

namespace Moves
  rur_ : MoveSeq
  rur_ = conjugate (twist R) (twist U)

  r_ur : MoveSeq
  r_ur = inverseEach rur_

  rur_u_ : MoveSeq
  rur_u_ = commutator (twist R) (twist U)

  r_u_ru : MoveSeq
  r_u_ru = commutator (twist' R) (twist' U)

  r_frf_ : MoveSeq
  r_frf_ = commutator (twist' R) (twist F)

  fru_ : MoveSeq
  fru_ = twist F <+> twist R <+> twist' U

  fr : MoveSeq
  fr = move (rotate F) <+> move (rotate R)

  namespace OLL
    fish_4 : MoveSeq
    fish_4 = conjugate fru_ r_ur
    oll_37 : MoveSeq
    oll_37 = conjugate (twist U) fish_4

    t_1 : MoveSeq
    t_1 = rur_u_ <+> r_frf_
    oll_33 : MoveSeq
    oll_33 = t_1

  namespace PLL
    yPerm : MoveSeq
    yPerm = OLL.fish_4 <+> OLL.t_1

    tPerm : MoveSeq
    tPerm = OLL.t_1 <+> OLL.fish_4

[zipList] Applicative List where
  pure x = [x]
  fns <*> values = zipWith id fns values

{-
data Move : Type where
  Nil : Move
  Twist : Face' -> Rotation' -> Move -> Move

-- FIXME: use proofs to make this more elegant
simplify : Move -> Move
simplify Nil = Nil
simplify final@(Twist f CW (Twist g CCW initial))             = if f == g then initial else final
simplify final@(Twist f CCW (Twist g CW initial))             = if f == g then initial else final
simplify final@(Twist f CW (Twist g CW (Twist h CW initial))) = if f == g && f == h
                                                                   then Twist f CCW initial
                                                                   else final
simplify final@(Twist f CW (Twist g CW (Twist h CW initial))) = if f == g && f == h
                                                                   then Twist f CCW initial
                                                                   else final

Semigroup Move where
  (<+>) Nil Nil = Nil
  (<+>) Nil m = m
  (<+>) m Nil = m

-}

max_stars_repo_name: msmorgan/idris-twist

max_issues_repo_name: msmorgan/idris-twist

max_forks_repo_name: msmorgan/idris-twist


text:
module Test.FmtTest

import IdrTest.Test
import IdrTest.Expectation

import Fmt

simpleTest : Test
simpleTest =
  test "Simple test" (\_ => assertEq
    (fmt "Hello")
    "Hello"
  )

stringTest : Test
stringTest =
  test "String test" (\_ => assertEq
    (fmt "Hello %s" "world")
    "Hello world"
  )

intTest : Test
intTest =
  test "String test" (\_ => assertEq
    (fmt "Health %d" 99)
    "Health 99"
  )

mixedTest : Test
mixedTest =
  test "String test" (\_ => assertEq
    (fmt "Name %s Age %d" "Thomas" 50)
    "Name Thomas Age 50"
  )

export
suite : Test
suite =
  describe "Fmt Tests"
    [ simpleTest
    , stringTest
    , intTest
    , mixedTest
    ]

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module System.REPL

import System.File

||| A basic read-eval-print loop, maintaining a state
||| @ state the input state
||| @ prompt the prompt to show
||| @ onInput the function to run on reading input, returning a String to
||| output and a new state. Returns Nothing if the repl should exit
export
replWith : HasIO io =>
           (state : a) -> (prompt : String) ->
           (onInput : a -> String -> Maybe (String, a)) -> io ()
replWith acc prompt fn
   = do eof <- fEOF stdin
        if eof
          then pure ()
          else do putStr prompt
                  fflush stdout
                  x <- getLine
                  case fn acc x of
                       Just (out, acc') =>
                           do putStr out
                              replWith acc' prompt fn
                       Nothing => pure ()

||| A basic read-eval-print loop
||| @ prompt the prompt to show
||| @ onInput the function to run on reading input, returning a String to
||| output
export
repl : HasIO io =>
       (prompt : String) -> (onInput : String -> String) -> io ()
repl prompt fn
   = replWith () prompt (\x, s => Just (fn s, ()))


text:
module Flexidisc.Header

import public Flexidisc.Dec.IsYes
import public Flexidisc.Header.Label
import public Flexidisc.Header.Row
import public Flexidisc.Header.Sub
import public Flexidisc.Header.Type
import public Flexidisc.OrdList

%default total
%access public export

||| A proof that a header some keys added to an given header leads to another one
||| @skipped keys of the original header that are not in the subset
||| @subset part of thecoriginal header
||| @subset the original header
data CompWithKeys : (skipped : List k) ->
                    (subset, orig : Header' k a) ->
                     Type where
  ||| Wrap `OrdList.CompWithKeys`
  S : {xs : OrdList k o a} -> {ys : OrdList k o a} ->
      CompWithKeys keys xs ys -> CompWithKeys keys (H xs) (H ys)

||| A proof that two `Header'` don't share a key.
data Disjoint : (xs, ys : Header' k a) -> Type where
  D : {xs : OrdList k o a} -> {ys : OrdList k o a} ->
      Disjoint xs ys -> Disjoint (H xs) (H ys)

||| A proof that a label is not already in a `Header'`
data Fresh : (l : label) -> (xs : Header' label a) -> Type where
  F : {xs : OrdList k o a} -> Fresh l xs -> Fresh l (H xs)

%name Header.Fresh fresh, prf, new

||| Decision procedure for freshness
decFresh : (DecEq label) => (l : label) -> (xs : Header' label a) ->
           Dec (Fresh l xs)
decFresh l (H xs) with (decFresh l xs)
  | (Yes prf) = Yes (F prf)
  | (No contra) = No (\(F x) => contra x)

||| Move the `decFresh` procedure to the type level
IsFresh : (DecEq label) => (l : label) -> (xs : Header' label a) -> Type
IsFresh l xs = IsYes (decFresh l xs)

||| A proof that labels that are in both lists have the same values
data HereOrNot : (xs, ys : Header' k a) -> Type where
  HN : {xs, ys : OrdList k o a} ->
       HereOrNot xs ys -> HereOrNot (H xs) (H ys)

toSub : {xs : Header k} -> HereOrNot xs ys -> Maybe (Sub xs ys)
toSub (HN compat) = map S (toSub compat)

||| A proof that a Header' has no duplicated key
data Nub : (Header' label a) -> Type where
  N : {xs : OrdList k o a} -> Nub xs -> Nub (H xs)

IsNub : DecEq label => (xs : Header' label a) -> Type
IsNub (H xs) = IsYes (decNub xs)

namespace SubWithKeys

  ||| Proof that an `Header'` has some given `keys` and is a subset of an other
  data SubWithKeys : (List k) -> (xs, ys : Header' k a) -> Type where
    S : {xs, ys : OrdList k o a} ->
        SubWithKeys keys xs ys -> SubWithKeys keys (H xs) (H ys)

namespace SameOrd

  ||| Both Header' are ordered with the same Ord typeclass
  ||| (thank you non unique typeclasses)
  data SameOrd : (xs, ys : Header' k a) -> Type where
    S : {xs, ys : OrdList k o a} -> SameOrd xs ys -> SameOrd (H xs) (H ys)

namespace Decomp

  ||| A Decomposition of a Header' into
  ||| a set of required values and a set of optional values
  ||| @required the set keys and types that must be in the original header
  ||| @optional the set keys and types that can be in the original header
  ||| @xs the original header
  data Decomp : (required, optional : Header k) -> (xs : Header k) -> Type where
    D : Header.Sub.Sub required xs -> HereOrNot optional xs -> Decomp required optional xs

||| Output the keys of the first Header' that are not in the second Header'
diffKeys : DecEq k => (xs, ys : Header' k a) -> Header' k a
diffKeys (H xs) (H ys) = H (diffKeys xs ys)

||| Apply a patch `xs` to an `Header'` `ys`.
||| The label of `ys` that are in `xs` are updated,
||| and the fresh element of `xs` are added
patch : DecEq k => (xs, ys : Header' k a) -> Header' k a
patch (H xs) (H ys) = H (patch xs ys)

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module System.Random

import Data.Fin
import Data.Vect
import Data.List

public export
interface Random a where
  randomIO : HasIO io => io a

  ||| Takes a range (lo, hi), and returns a random value uniformly
  ||| distributed in the closed interval [lo, hi]. It is unspecified what
  ||| happens if lo > hi.
  randomRIO : HasIO io => (a, a) -> io a

%foreign "scheme:blodwen-random"
         "javascript:lambda:(max)=>Math.floor(Math.random() * max)"
prim__randomBits32 : Bits32 -> PrimIO Bits32

randomBits32 : Bits32 -> IO Bits32
randomBits32 upperBound = fromPrim (prim__randomBits32 upperBound)

public export
Random Int32 where
  -- Generate a random value within [-2^31, 2^31-1].
  randomIO = do
    let maxInt : Bits32    = 2147483647 -- shiftL 1 31 - 1
        negMinInt : Bits32 = 2147483648 -- negate $ shiftL 1 31
        magnitude : Bits32 = maxInt + negMinInt
    bits32 <- liftIO $ randomBits32 magnitude
    let int : Integer = cast bits32
    pure . cast $ int - (cast negMinInt)

  -- Generate a random value within [lo, hi].
  randomRIO (lo, hi) =
    let range : Integer = (cast hi) - (cast lo) + 1
     in pure . cast $ !(liftIO . randomBits32 $ cast range) + cast lo

%foreign "scheme:blodwen-random"
         "javascript:lambda:()=>Math.random()"
prim__randomDouble : PrimIO Double

randomDouble : IO Double
randomDouble = fromPrim prim__randomDouble

public export
Random Double where
  -- Generate a random value within [0, 1].
  randomIO = liftIO randomDouble

  -- Generate a random value within [lo, hi].
  randomRIO (lo, hi) = map ((+ lo) . (* (hi - lo))) (liftIO randomDouble)

%foreign "scheme:blodwen-random-seed"
prim__srand : Bits64 -> PrimIO ()

||| Sets the random seed
export
srand : Bits64 -> IO ()
srand n = fromPrim (prim__srand n)

||| Generate a random number in Fin (S `k`)
|||
||| Note that rndFin k takes values 0, 1, ..., k.
public export
rndFin : HasIO io => (n : Nat) -> io (Fin (S n))
rndFin 0 = pure FZ
rndFin (S k) = do
  let intBound = the Int32 (cast (S k))
  randomInt <- randomRIO (0, intBound)
  pure $ restrict (S k) (cast randomInt)

||| Select a random element from a vector
public export
rndSelect' : HasIO io => {k : Nat} -> Vect (S k) a -> io a
rndSelect' xs = pure $ Vect.index !(rndFin k) xs

||| Select a random element from a non-empty list
public export
rndSelect : HasIO io => (elems : List a) -> (0 _ : NonEmpty elems) => io a
rndSelect (x :: xs) = rndSelect' $ fromList (x :: xs)


text:
record Nat2 where
  nat : Nat

f : Nat2 -> Nat2
f = { nat $= floor }


text:
module Main

import Text.PrettyPrint.WL

%default total

myDoc : Doc
myDoc = fold (|//|) $ map text $ words "this is a long sentence."

myString : String
myString = toString 0 15 $ myDoc

main : IO ()
main = putStrLn myString

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Bits

%access public export
%default total

||| Ceiling of log_2 for `Nat`s.
||| This is a bit module, so for convenience, we say clog2 0 = 0
clog2 : Nat -> Nat
clog2 Z = 0
clog2 (S Z) = 0
clog2 (S (S n)) = let y1 = log2NZ (S (S n)) SIsNotZ
                      y2 = log2NZ (S n) SIsNotZ in
                  if y1 == y2 then y1+1 else y1

||| Floor of log_2 for `Nat`s.
||| This is a bit module, so for convenience, we say flog2 0 = 0
flog2 : Nat -> Nat
flog2  Z    = 0
flog2 (S z) = log2NZ (S z) SIsNotZ

||| Round a `Double` to the closest `Nat`
round : Double -> Nat
round x = cast $ cast {to=Integer} (x+0.5)

||| Version of flog2 for `Double`
flog2Approx : Double -> Nat
flog2Approx = flog2 . round

||| Conversion of maximum unsigned value, to minimum number of bits
maxToBits : Nat -> Nat
maxToBits = clog2 . (+1)

||| Conversion of bits to maximum unsigned value
bitsToMax : Nat -> Nat
bitsToMax = Nat.pred . power 2


text:
identity : (a : Type) -> a -> a
identity a = id

identityL :
  (a, b : Type )
  -> (f : a -> b)
  -> (identity b) . f = f
identityL a b f = Refl

identityR :
  (a, b : Type )
  -> (f : a -> b)
  -> f = (identity b) . f
identityR a b f = Refl


text:
module TyTTP.Core.Response

public export
record Response s h a where
  constructor MkResponse
  status : s
  headers : h
  body : a

export
Functor (Response s h) where
  map f res = { body $= f } res

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
||| An strict preorder (sometimes known as a quasi-order, or an
||| ordering) is what you get when you remove the diagonal `{(a,b) | a
||| r b , b r a}` from a preorder. For example a < b is an ordering.
||| This module extends base's Control.Order with the strict versions.
||| The interface system seems to struggle a bit with some of the constructions,
||| so I hacked them a bit. Sorry.
module Decidable.Order.Strict

import Control.Relation
import Control.Order
import Decidable.Equality

%default total

public export
interface Irreflexive ty rel where
  irreflexive : {x : ty} -> Not (rel x x)

public export
interface (Transitive ty rel, Irreflexive ty rel) => StrictPreorder  ty rel where

public export
interface Asymmetric ty rel where
  asymmetric : {x, y : ty} -> rel x y -> Not (rel y x)

public export
[SPA] StrictPreorder ty rel => Asymmetric ty rel where
  asymmetric xy yx = irreflexive {rel} $ transitive {rel} xy yx

-- We make this completion a record type so that we do not need to name the
-- interface implementations for fear of them interfering with other
-- `Either`-based constructions.

public export
record EqOr {0 t : Type} (spo : Rel t) (a, b : t) where
  constructor MkEqOr
  runEqOr : Either (a = b) (a `spo` b)

public export
Transitive ty rel => Transitive ty (EqOr rel) where

  transitive (MkEqOr (Left  Refl)) bLTEc                 = bLTEc
  transitive aLTEb                 (MkEqOr (Left  Refl)) = aLTEb
  transitive (MkEqOr (Right aLTb)) (MkEqOr (Right bLTc))
    = MkEqOr $ Right $ transitive {rel} aLTb bLTc

public export
Reflexive ty (EqOr rel) where
  reflexive = MkEqOr $ Left Refl

public export
Transitive ty rel => Preorder ty (EqOr rel) where

public export
(Irreflexive ty rel, Asymmetric ty rel) => Antisymmetric ty (EqOr rel) where

  antisymmetric (MkEqOr p) (MkEqOr q) = go p q where

    go : {a, b : ty} ->
         Either (a = b) (a `rel` b) ->
         Either (b = a) (b `rel` a) ->
         a = b
    go (Left  Refl) (Left  Refl) = Refl
    go (Left  Refl) (Right bLTa) = absurd (irreflexive {rel} bLTa)
    go (Right aLTb) (Left  Refl) = absurd (irreflexive {rel} aLTb)
    go (Right aLTb) (Right bLTa) = absurd (asymmetric {rel} aLTb bLTa)

public export
(Irreflexive ty rel, Asymmetric ty rel, Transitive ty rel) =>
  PartialOrder ty (EqOr rel) where

public export
data DecOrdering : {lt : t -> t -> Type} -> (a,b : t) -> Type where
  DecLT : forall lt . (a `lt` b) -> DecOrdering {lt = lt} a b
  DecEQ : forall lt . (a  =   b) -> DecOrdering {lt = lt} a b
  DecGT : forall lt . (b `lt` a) -> DecOrdering {lt = lt} a b

public export
interface StrictPreorder t spo => StrictOrdered t spo where
  order : (a,b : t) -> DecOrdering {lt = spo} a b

public export
Connex ty rel => Connex ty (EqOr rel) where
  connex neq = bimap (MkEqOr . Right) (MkEqOr . Right) (connex neq)

public export
(Connex ty rel, DecEq ty) => StronglyConnex ty (EqOr rel) where
  order a b = case decEq a b of
    Yes eq => Left $ MkEqOr (Left eq)
    No neq => connex neq


text:
module Main

main : IO ()
main = do
  putStrLn "Hello, world!"

max_stars_repo_name: simnalamburt/snippets

max_issues_repo_name: simnalamburt/snippets

max_forks_repo_name: simnalamburt/snippets


text:
module Main

import Fs
import Control.Monad.Free
import Data.Vect
import Data.Functor.Coproduct

%hide Prelude.File.readFile

data FileSystemF next
  = WriteFile FilePath String next
  | ReadFile FilePath (String -> next)

FileSystem : Type -> Type
FileSystem = Free FileSystemF

data ConsoleF next
  = ConsoleLog String next
  | ConsoleError String next

Console : Type -> Type
Console = Free ConsoleF

Functor FileSystemF where
  map f (WriteFile filePath contents next) = WriteFile filePath contents (f next)
  map f (ReadFile filePath fNext) = ReadFile filePath (f . fNext)

Functor ConsoleF where
  map f (ConsoleLog string next) = ConsoleLog string (f next)
  map f (ConsoleError string next) = ConsoleError string (f next)

AppF : Type -> Type
AppF = Coproduct FileSystemF ConsoleF

App : Type -> Type
App = Free AppF

-- | Some helper functions
liftFileSystem : FileSystemF a -> App a
liftFileSystem = liftFree . left

liftConsole : ConsoleF a -> App a
liftConsole = liftFree . right

-- | Helper functions for FileSystem
writeFile : FilePath -> Contents -> App Unit
writeFile filePath contents = liftFileSystem $ WriteFile filePath contents ()

readFile : FilePath -> App String
readFile filePath = liftFileSystem $ ReadFile filePath id

-- | Helper functions for Console
consoleLog : String -> App Unit
consoleLog string = liftConsole $ ConsoleLog string ()

consoleError : String -> App Unit
consoleError string = liftConsole $ ConsoleError string ()

-- | The FileSystem interpreter
interpretFs : FileSystemF a -> JS_IO a
interpretFs (WriteFile filePath contents next) = writeFileSync filePath contents *> pure next
interpretFs (ReadFile filePath fNext) = do
  contents <- readFileSync filePath
  pure (fNext contents)

-- | The Console interpreter
interpretConsole : ConsoleF a -> JS_IO a
interpretConsole (ConsoleLog string next) = putStrLn' string *> pure next
interpretConsole (ConsoleError string next) = putStrLn' string *> pure next

-- | The App interpreter that composes Console and FileSystem
interpretApp : AppF a -> JS_IO a
interpretApp (MkCoproduct (Left l)) = interpretFs l
interpretApp (MkCoproduct (Right r)) = interpretConsole r

-- | This program just reads foo.txt and prints its contents to stdout
catFoo : App Unit
catFoo = do
  contents <- readFile "foo.txt"
  consoleLog contents

main : JS_IO ()
main = foldFree interpretApp catFoo

max_stars_repo_name: idris-industry/idris-free

max_issues_repo_name: idris-industry/idris-free

max_forks_repo_name: idris-industry/idris-free


text:
module Main

import Effect.StdIO
import VectMissing

-----------------------------------------------------------------------
-- GAME STATE
-----------------------------------------------------------------------

{- First, the game state, HState, where the type specifies how many guesses
are left and how many missing letters there are still to get. -}

data HState : Nat -> Nat -> Type where
     MkH : (word : String) ->
           (guesses : Nat) ->
           (got : List Char) ->
           (missing : Vect m Char) ->
           HState guesses m

instance Default (HState 0 0) where
    default = MkH "" 0 [] []

instance Show (HState guesses m) where
    show (MkH w _ got missing)
         = let w' = pack (map showGot (unpack w)) in
               w' ++ "\n\n" ++ show guesses ++ " guesses left"
      where showGot : Char -> Char
            showGot ' ' = '/'
            showGot c = if ((not (isAlpha c)) || (c `elem` got)) then c else '-'

{- Initialise the state with the missing letters in a word -}

total
letters : String -> List Char
letters x with (strM x)
  letters "" | StrNil = []
  letters (strCons y xs) | (StrCons y xs)
          = let xs' = assert_total (letters xs) in
                if ((not (isAlpha y)) || (y `elem` xs')) then xs' else y :: xs'

initState : (x : String) -> HState 6 (length (letters x))
initState w = let xs = letters w in
                  MkH w _ [] (fromList (letters w))

-----------------------------------------------------------------------
-- RULES
-----------------------------------------------------------------------

{- Now, the rules of the game, written as an Effect.
We can think of the rules as giving a protocol that the game player and
the machine must follow for an implementation of the game to make sense.
-}

data Hangman : Effect where

-- Rule:
-- Precondition: we can make a guess if we have one or more guess available
-- (S g) and one or more letters are still missing (S w)

-- Postcondition: return whether the character was in the word. If so, reduce
-- the number of missing letters, if not, reduce the number of guesses left

     Guess : (x : Char) ->
             { HState (S g) (S w) ==>
               {inword} if inword then HState (S g) w
                                  else HState g (S w) }
                Hangman Bool

-- The 'Won' operation requires that there are no missing letters

     Won  : { HState g 0 ==> HState 0 0 } Hangman ()

-- The 'Lost' operation requires that there are no guesses left

     Lost : { HState 0 w ==> HState 0 0 } Hangman ()

-- Set up a new game, initialised with 6 guesses and the missing letters in
-- the given word. Note that if there are no letters in the word, we won't
-- be able to run 'Guess'!

     NewWord : (w : String) ->
               { h ==> HState 6 (length (letters w)) } Hangman ()

-- Finally, allow us to get the current game state

     Get  : { h } Hangman h

HANGMAN : Nat -> Nat -> EFFECT
HANGMAN g v = MkEff (HState g v) Hangman

-----------------------------------------------------------------------
-- IMPLEMENTATION OF THE RULES
-----------------------------------------------------------------------

{- This effect handler simply updates the game state as necessary for
each operation. 'Guess' is slightly tricky, in that it needs to check
whether the letter is in the word, and branch accordingly (and if it
is in the word, update the vector of missing letters to be the right
length). -}

using (m : Type -> Type)
  instance Handler Hangman m where
    handle (MkH w g got []) Won k = k () (MkH w 0 got [])
    handle (MkH w Z got m) Lost k = k () (MkH w 0 got [])

    handle st Get k = k st st
    handle st (NewWord w) k = k () (initState w)

    handle (MkH w (S g) got m) (Guess x) k =
      case isElem x m of
           Nothing => k False (MkH w _ got m)
           (Just p) => k True (MkH w _ (x :: got) (shrink m p))

-----------------------------------------------------------------------
-- USER INTERFACE
-----------------------------------------------------------------------

{- Finally, an implementation of the game which reads user input and calls
the operations we defined above when appropriate -}

game : { [HANGMAN (S g) (S w), STDIO] ==> [HANGMAN 0 0, STDIO] } Eff IO ()
game = do putStrLn (show !Get)
          putStr "Enter guess: "
          let guess = trim !getStr
          case choose (not (guess == "")) of
               (Left p) => processGuess (strHead' guess p)
               (Right p) => do putStrLn "Invalid input!"
                               game
  where
    processGuess : Char -> { [HANGMAN (S g) (S w), STDIO] ==>
                             [HANGMAN 0 0, STDIO] }
                           Eff IO ()
    processGuess {g} {w} c
      = case !(Main.Guess c) of
             True => do putStrLn "Good guess!"
                        case w of
                             Z => Won
                             (S k) => game
             False => do putStrLn "No, sorry"
                         case g of
                              Z => Lost
                              (S k) => game

{- It typechecks! Ship it! -}

runGame : { [HANGMAN 0 0, STDIO] } Eff IO ()
runGame = do NewWord "sausage machine"
             game

{- I made a couple of mistakes while writing this. For example, the following
were caught by the type checker:

* Forgetting to check the 'Won' state before continuing with 'game'
* Accidentally checking the number of missing letters rather than the number
  of guesses when checking if 'Lost' was callable

-}

main : IO ()
main = run runGame

max_stars_repo_name: silky/idris-demos

max_issues_repo_name: silky/idris-demos

max_forks_repo_name: silky/idris-demos


text:
module Generics.Newtype.Abs

import Generics.Newtype.Num

import Generics.Derive
%language ElabReflection

--------------------------------------------------------------------------------
--          Abs
--------------------------------------------------------------------------------

public export %hint
AbsToNumNP : NP (Abs . f) ks -> NP (Num . f) ks
AbsToNumNP = mapNP (\_ => materialize Num)

public export %hint
AbsToNumPOP : POP (Abs . f) kss -> POP (Num . f) kss
AbsToNumPOP = mapPOP (\_ => materialize Num)

-- Derivation of Abs for n-ary products or newtypes
-- e.g. `(a,b,c)` or `data Foo a = MkFoo a`  or  `data Foo = Foo Int`

-- n-ary products, e.g. (a,b,c)   (data Foo x y = MkFoo x y)
public export
NP (Abs . f) ks => Abs (NP f ks) where
  abs = hcliftA (Abs . f) abs

-- This type of deriving is for newtypes so we restrict oursellves to single constructor types.
public export
(all : NP (Abs . f) [k']) => Abs (NS f [k']) where
  abs {all = _::_} (Z x) = Z $ abs x

public export
POP (Abs . f) kss => Abs (POP f kss) where
  abs = hcliftA (Abs . f) abs

public export
POP (Abs . f) [ks] => Abs (SOP_ k f [ks]) where
  abs (MkSOP n) = MkSOP $ abs n

export
genericAbs : Generic t [code] => POP Abs [code] => t -> t
genericAbs = to . abs . from

export
||| Derives a `Abs` implementation for the given data type
||| and visibility.
AbsVis : Visibility -> DeriveUtil -> InterfaceImpl
AbsVis vis g = MkInterfaceImpl "Abs" vis []
                       `(MkAbs genericAbs)
                       (implementationType `(Abs) g)

export
||| Alias for `EncodeVis Public`.
Abs : DeriveUtil -> InterfaceImpl
Abs = AbsVis Public