text:
module Main

import Compiler.Common
import Compiler.ES.Imperative
import Core.CompileExpr
import Core.Context
import Core.Name.Namespace
import Data.List
import Data.List1
import Data.SortedSet as SortedSet
import Data.String
import Data.String.Extra
import Idris.Driver
import Libraries.Data.StringMap
import Libraries.Utils.Hex
import Primitives
import Printer
import System
import System.File

data Dart : Type where

record DartT where
  constructor MkDartT
  imports : StringMap Doc
  nextImportId : Int
  includes : SortedSet String
  foreignTypeNames : StringMap Doc
  usesDelay : Bool
  usesArgs : Bool

modify : {auto ctx : Ref Dart DartT} -> (DartT -> DartT) -> Core ()
modify = Core.update Dart

useDelay : {auto ctx : Ref Dart DartT} -> Core ()
useDelay = modify { usesDelay := True }

useArgs : {auto ctx : Ref Dart DartT} -> Core ()
useArgs = modify { usesArgs := True }

include : {auto ctx : Ref Dart DartT} -> String -> Core ()
include code = modify { includes $= insert code }

Statement : Type
Statement = ImperativeStatement

Expression : Type
Expression = ImperativeExp

splitAtFirst : Char -> String -> (String, String)
splitAtFirst ch s =
  let (before, rest) = break (== ch) s
  in (before, drop 1 rest)

dartIdent : String -> String
dartIdent s = concatMap okChar (unpack s)
  where
    okChar : Char -> String
    okChar c =
      if isAlphaNum c || c == '_'
        then cast c
        else "$" ++ asHex (cast c)

addImport : {auto ctx : Ref Dart DartT} -> String -> Core Doc
addImport lib = do
  s <- get Dart
  case lookup lib (imports s) of
    Nothing => do
      let alias = text ("$" ++ show (nextImportId s))
      put Dart (record { imports $= insert lib alias, nextImportId $= (+1) } s)
      pure alias
    Just alias =>
      pure alias

keywordSafe : String -> String
keywordSafe s = case s of
  "var" => "var_"
  _ => s

data DartNameKind
  = TopLevelName
  | MemberName
  | InfixOperator
  | PrefixOperator
  | GetAtOperator
  | PutAtOperator

dartOperators : List (String, DartNameKind)
dartOperators = [
  ("==", InfixOperator),
  ("<", InfixOperator),
  (">", InfixOperator),
  ("<=", InfixOperator),
  (">=", InfixOperator),
  ("+", InfixOperator),
  ("-", InfixOperator),
  ("*", InfixOperator),
  ("/", InfixOperator),
  ("~/", InfixOperator),
  ("|", InfixOperator),
  ("&", InfixOperator),
  ("^", InfixOperator),
  (">>", InfixOperator),
  ("<<", InfixOperator),
  ("~", PrefixOperator),
  ("[]", GetAtOperator),
  ("[]=", PutAtOperator)
]

parseDartOperator : String -> Maybe DartNameKind
parseDartOperator s = lookup s dartOperators

isMemberName : String -> Bool
isMemberName = isPrefixOf "."

dartNameKindOf : String -> DartNameKind
dartNameKindOf s =
  if isMemberName s
    then MemberName
    else fromMaybe TopLevelName (parseDartOperator s)

dartNameString : Name -> String
dartNameString n = case n of
  NS ns n => showNSWithSep "_" ns ++ "_" ++ dartNameString n
  UN n => keywordSafe (dartIdent n)
  MN n i => dartIdent n ++ "_" ++ show i
  PV n d => "pat__" ++ dartNameString n
  DN _ n => dartNameString n
  Nested (i, x) n => "n__" ++ show i ++ "_" ++ show x ++ "_" ++ dartNameString n
  CaseBlock x y => "case__" ++ dartIdent x ++ "_" ++ show y
  WithBlock x y => "with__" ++ dartIdent x ++ "_" ++ show y
  Resolved i => "fn__" ++ show i
  RF n => "rf__" ++ dartIdent n

dartName : Name -> Doc
dartName = text . dartNameString

dartString : String -> String
dartString s = "\"" ++ (concatMap okChar (unpack s)) ++ "\""
  where
    okChar : Char -> String
    okChar c = case c of
      '\0' => "\\0"
      '"' => "\\\""
      '\r' => "\\r"
      '\n' => "\\n"
      '$' => "\\$"
      '\\' => "\\\\"
      c => if (c >= ' ') && (c <= '~')
        then cast c
        else "\\u{" ++ asHex (cast c) ++ "}"

dartStringDoc : String -> Doc
dartStringDoc = text . dartString

debug : Show e => e -> Doc
debug = dartStringDoc . show

comment : String -> Doc
comment c = "/* " <+> text c <+> "*/"

surroundWith : Doc -> Doc -> Doc
surroundWith s d = s <+> d <+> s

mdCode : Doc -> Doc
mdCode = surroundWith "`"

mdItalic : Doc -> Doc
mdItalic = surroundWith "_"

docCommentFor : FC -> Name -> Doc
docCommentFor fc n = "/// " <+> mdCode (shown n) <+> " from " <+> mdItalic (shown fc) <+> "." <+> line

argList : List Doc -> Doc
argList [] = text "()"
argList args = paren (commaSep args <+> ",")

assertionError : Doc -> Doc
assertionError e = "throw $.AssertionError" <+> paren e <+> semi

unsupportedError : Show a => a -> Doc
unsupportedError e = "throw $.UnsupportedError" <+> paren (debug e) <+> semi

unsupported : Show a => a -> Doc
unsupported e = "(() {" <+> unsupportedError e <+> "})()"

genericTypeArgs : List Doc -> Doc
genericTypeArgs args = "<" <+> commaSep args <+> ">"

null' : Doc
null' = text "null"

dynamic' : Doc
dynamic' = text "$.dynamic "

final' : Doc
final' = text "final "

var' : Doc
var' = text "var "

paramList : List Name -> Doc
paramList ps = tupled ((dynamic' <+>) . dartName <$> ps)

castTo : Doc -> Doc -> Doc
castTo ty e = paren (e <+> " as " <+> ty)

world' : Doc
world' = text "#World"

intTy : Doc
intTy = text "$.int"

bigIntTy : Doc
bigIntTy = text "$.BigInt"

stringTy : Doc
stringTy = text "$.String"

doubleTy : Doc
doubleTy = text "$.double"

refTy : Doc
refTy = text "Ref"

maxDartInt : Integer
maxDartInt = 9223372036854775807

bigIntConstant : Integer -> Doc
bigIntConstant = \case
  0 => text "$.BigInt.zero"
  1 => text "$.BigInt.one"
  i => if i > maxDartInt
    then "$.BigInt.parse(\"" <+> shown i <+> "\")"
    else "$.BigInt.from(" <+> shown i <+> ")"

dartConstant : Constant -> Doc
dartConstant c = case c of
  B8 i => shown i
  B16 i => shown i
  B32 i => shown i
  B64 i => bigIntConstant i
  BI i => bigIntConstant i
  I i => shown i
  Ch c => shown (cast {to=Int} c)
  Str s => dartStringDoc s
  Db d => shown d
  WorldVal => world'
  _ => unsupported c

runtimeTypeOf : Constant -> Doc
runtimeTypeOf ty = case ty of
  StringType => stringTy
  IntegerType => bigIntTy
  Bits64Type => bigIntTy
  DoubleType => doubleTy
  _ => "$.int"

---- Dart FFI -------------------------------------
Lib : Type
Lib = String

data ForeignDartSpec
  = ForeignFunction String Lib
  | ForeignConst String Lib
  | ForeignMethod String

dropPrefix : String -> String -> Maybe String
dropPrefix p s =
  if p `isPrefixOf` s
    then Just (drop (length p) s)
    else Nothing

foreignDartSpecFrom : String -> Maybe ForeignDartSpec
foreignDartSpecFrom s = do
  (name, lib) <- dartNameAndLib s
  method name <|> const name lib <|> function name lib
  where
    dartNameAndLib : String -> Maybe (String, Lib)
    dartNameAndLib s = splitAtFirst ',' <$> dropPrefix "Dart:" s

    method : String -> Maybe ForeignDartSpec
    method m = ForeignMethod <$> dropPrefix "." m

    const : String -> Lib -> Maybe ForeignDartSpec
    const n lib = (`ForeignConst` lib) <$> dropPrefix "const " n

    function : String -> Lib -> Maybe ForeignDartSpec
    function n lib = Just (ForeignFunction n lib)

FunctionType : Type
FunctionType = (List CFType, CFType)

mkFunctionType : List Expression -> CFType -> FunctionType
mkFunctionType ps ret = (const CFPtr <$> ps, ret)

uncurriedSignature : CFType -> CFType -> FunctionType
uncurriedSignature a b = go [a] b
  where
    go : List CFType -> CFType -> FunctionType
    go ps (CFFun a b) = go (a :: ps) b
    go ps ret = (reverse ps, ret)

argNamesFor : List a -> String -> List Doc
argNamesFor args p = text . (p ++) . show <$> [1..length args]

||| Adapts the foreign callback [c] so that it can be
||| invoked from Dart with the expected signature.
makeCallback : FunctionType -> Doc -> Doc
makeCallback (args, ret) c =
  let
    argNames = argNamesFor args "c$"
    params = mapMaybe callbackParam (zip argNames args)
    worldArg = case ret of
      CFIORes _ => paren world'
      _ => empty
    callbackArgs = hcat (paren <$> params) <+> worldArg
  in
    tupled params <+> " => " <+> c <+> callbackArgs
  where
    callbackParam : (Doc, CFType) -> Maybe Doc
    callbackParam (p, ty) = case ty of
      CFWorld => Nothing
      _ => Just p

foreignArg : {auto fc : FC} -> (Doc, CFType) -> Core (Maybe Doc)
foreignArg (n, ty) = case ty of
  CFWorld => pure Nothing
  CFFun a b => pure $ Just (makeCallback (uncurriedSignature a b) n)
  CFUser (UN "Type") [] => pure Nothing
  CFUser (UN "__") [] => pure Nothing
  CFUser (NS ns (UN "Bool")) [] =>
    if ns == basicsNS
      then throw (GenericMsg fc "'Bool' is not a valid foreign type, use 'DartBool' from 'Dart.Core` instead!")
      else pure $ Just n
  _ => pure $ Just n

singleExpFunction : Doc -> List Doc -> Doc -> Doc
singleExpFunction n ps e =
  n <+> tupled ps <+> block ("return " <+> e <+> semi)

convertForeignReturnType : CFType -> Doc -> Doc
convertForeignReturnType retTy e = case retTy of
  CFUser (NS ns (UN "Bool")) [] =>
    if ns == basicsNS
      then e <+> " ? 0 : 1"
      else e
  _ => e

traverseMaybes : (a -> Core (Maybe b)) -> List a -> Core (List b)
traverseMaybes f as = catMaybes <$> traverse f as

collectPositional : Expression -> List Expression
collectPositional e = go [] e
  where
    go : List Expression -> Expression -> List Expression
    go acc ({- HVect.:: -} IEConstructor (Left 1) (e :: es :: _)) = go (e :: acc) es
    go acc _ = reverse acc

parseList : Expression -> Maybe (List Expression)
parseList e = case e of
  IEConstructor _ _ => Just (collectPositional e)
  _ => Nothing

foreignFunctionProxy : {auto fc : FC} -> Doc -> Doc -> List CFType -> CFType -> Core Doc
foreignFunctionProxy n ff args ret = do
  let argNames = argNamesFor args "a$"
  fArgs <- traverseMaybes foreignArg (zip argNames args)
  let call = ff <+> tupled fArgs
  pure (singleExpFunction n argNames (convertForeignReturnType ret call))

foreignName : {auto ctx : Ref Dart DartT}
  -> Lib -> String -> Core Doc
foreignName lib n =
  case fastUnpack lib of
    ('\n' :: rest) => do
      include lib
      pure (text n)
    [] => pure (text n)
    _ => pure (!(addImport lib) <+> dot <+> text n)

parseForeignName : {auto ctx : Ref Dart DartT}
  -> String -> Core Doc
parseForeignName ty =
  let (tyN, lib) = splitAtFirst ',' ty
  in foreignName lib tyN

lookupForeignType : {auto ctx : Ref Dart DartT} -> String -> Core (Maybe Doc)
lookupForeignType ty = lookup ty . foreignTypeNames <$> get Dart

putForeignType : {auto ctx : Ref Dart DartT} -> String -> Doc -> Core ()
putForeignType ty doc = modify { foreignTypeNames $= insert ty doc }

foreignTypeName : {auto ctx : Ref Dart DartT} -> String -> Core Doc
foreignTypeName ty = do
  case !(lookupForeignType ty) of
    Just doc => pure doc
    Nothing => do
      doc <- parseForeignName ty
      putForeignType ty doc
      pure doc

foreignTypeOf : {auto ctx : Ref Dart DartT} -> CFType -> Core Doc
foreignTypeOf e = case e of
  CFString => pure stringTy
  CFDouble => pure doubleTy
  CFChar => pure intTy
  CFInt => pure intTy
  CFUnsigned8 => pure intTy
  CFUnsigned16 => pure intTy
  CFUnsigned32 => pure intTy
  CFUnsigned64 => pure intTy
  CFStruct name _ => foreignTypeName name
  _ => pure "$.dynamic"

foreignMethodProxy : {auto ctx : Ref Dart DartT}
  -> Doc -> Doc -> List CFType -> CFType -> Core Doc
foreignMethodProxy n m args@(thisTy :: _) ret = do
  let argNames = argNamesFor args "a$"
  case !(traverseMaybes foreignArg (zip argNames args)) of
    fThis :: fArgs => do
      let mc = castTo !(foreignTypeOf thisTy) fThis <+> dot <+> m <+> tupled fArgs
      pure (singleExpFunction n argNames (convertForeignReturnType ret mc))
    _ => pure (unsupported (m, args))
foreignMethodProxy n m args ret =
  pure (unsupported (m, args))

dartForeign : {auto ctx : Ref Dart DartT}
  -> {auto fc : FC}
  -> Name -> ForeignDartSpec
  -> List CFType -> CFType
  -> Core Doc
dartForeign n (ForeignFunction f lib) args ret = do
  ff <- foreignName lib f
  foreignFunctionProxy (dartName n) ff args ret
dartForeign n (ForeignConst c lib) _ _ = do
  fc <- foreignName lib c
  pure (singleExpFunction (dartName n) [] fc)
dartForeign n (ForeignMethod m) args ret = do
  foreignMethodProxy (dartName n) (text m) args ret

parseFunctionType : Expression -> Maybe FunctionType
parseFunctionType e =
  case e of
    IEConstructor (Right "->") [a, b] => Just (go [a] b)
    IEConstructor (Right "PrimIO.IO") [_] => Just (mkFunctionType [] (CFIORes CFPtr))
    _ => Nothing
  where
    go : List Expression -> Expression -> FunctionType
    go ps (IELambda _ (ReturnStatement (IEConstructor (Right ty) args))) =
      case (ty, args) of
        ("->", [a, b]) => go (a :: ps) b
        ("PrimIO.IO", _) => mkFunctionType ps (CFIORes CFPtr)
        _ => mkFunctionType ps CFPtr
    go ps _ = mkFunctionType ps CFPtr

dartStdout : {auto ctx : Ref Dart DartT} -> Core Doc
dartStdout = foreignName "dart:io" "stdout"

dartStdin : {auto ctx : Ref Dart DartT} -> Core Doc
dartStdin = foreignName "dart:io" "stdin"

unknownForeignDecl : {auto ctx : Ref Dart DartT}
  -> Name -> List String
  -> Core Doc
unknownForeignDecl n ss =
  pure (dartName n <+> "([a, b, c, d, e, f, g, h, i, j, k])" <+> block (unsupportedError (n, ss)))

maybeForeignDartDecl : {auto ctx : Ref Dart DartT}
  ->  {auto fc : FC}
  -> Name -> List String
  -> List CFType -> CFType
  -> Core Doc
maybeForeignDartDecl n ss args ret =
  case mapMaybe foreignDartSpecFrom ss of
    [s] => dartForeign n s args ret
    _ => unknownForeignDecl n ss

foreignDecl : {auto ctx : Ref Dart DartT}
  ->  {auto fc : FC}
  -> Name -> List String
  -> List CFType -> CFType
  -> Core Doc
foreignDecl n ss args ret = case n of
  NS _ (UN "prim__putStr") =>
    pure (dartName n <+> "(s, w)" <+> block (!dartStdout <+> ".write(s);" <+> line <+> "return w;"))
  NS _ (UN "prim__putChar") =>
    pure (dartName n <+> "(c, w)" <+> block (!dartStdout <+> ".writeCharCode(c);" <+> line <+> "return w;"))
  NS _ (UN "prim__getStr") =>
    pure (dartName n <+> "(w)" <+> block ("return " <+> !dartStdin <+> ".readLineSync() ?? \"\";"))
  NS _ (UN "prim__getArgCount") =>
    useArgs *> pure (dartName n <+> "(w) => $args.length;")
  NS _ (UN "prim__getArg") =>
    useArgs *> pure (dartName n <+> "(i, w) => $args[i];")
  NS ns (UN "fastConcat") => if ns == typesNS
    then pure (text primDartFastConcat)
    else maybeForeignDartDecl n ss args ret
  NS ns (UN "fastUnpack") => if ns == typesNS
    then pure (text primDartFastUnpack)
    else maybeForeignDartDecl n ss args ret
  NS ns (UN "fastPack") => if ns == typesNS
    then pure (text primDartFastPack)
    else maybeForeignDartDecl n ss args ret
  _ => maybeForeignDartDecl n ss args ret

binOp : Doc -> Doc -> Doc -> Doc
binOp o lhs rhs = paren (lhs <+> o <+> rhs)

binOpOf' : Doc -> Doc -> Doc -> Doc -> Doc
binOpOf' ty op lhs rhs = binOp op (castTo ty lhs) (castTo ty rhs)

binOpOf : Constant -> Doc -> Doc -> Doc -> Doc
binOpOf ty = binOpOf' (runtimeTypeOf ty)

idrisBoolFrom : Doc -> Doc
idrisBoolFrom e = paren (e <+> " ? 1 : 0")

boolOpOf : Constant -> Doc -> Doc -> Doc -> Doc
boolOpOf ty o lhs rhs = idrisBoolFrom (binOpOf ty o lhs rhs)

stringOp : Doc -> Doc -> Doc
stringOp s m = (castTo stringTy s) <+> dot <+> m

doubleOp : Doc -> Doc -> Doc
doubleOp e m = (castTo doubleTy e) <+> dot <+> m

bigIntFrom : Doc -> Doc
bigIntFrom num = "$.BigInt.from" <+> paren num

toUnsigned : Int -> Doc -> Doc
toUnsigned width num = num <+> ".toUnsigned" <+> paren (shown width)

bigIntToBits : Int -> Doc -> Doc
bigIntToBits 64 i = toUnsigned 64 (castTo bigIntTy i)
bigIntToBits width i = toUnsigned width (castTo bigIntTy i) <+> ".toInt()"

bigIntToInt : Doc -> Doc
bigIntToInt i = toUnsigned 64 (castTo bigIntTy i) <+> ".toInt()"

intToBits : Int -> Doc -> Doc
intToBits 64 i = bigIntFrom i
intToBits width i = bigIntToBits width (bigIntFrom i)

boundedUIntOp : Int -> Doc -> Doc -> Doc -> Doc
boundedUIntOp 64 op x y = toUnsigned 64 (binOpOf' bigIntTy op x y)
boundedUIntOp width op x y = toUnsigned width (binOpOf' intTy op x y )

boundedShiftOp : Int -> Doc -> Doc -> Doc -> Doc
boundedShiftOp 64 op x y = toUnsigned 64 (bigIntFrom x <+> op <+> y)
boundedShiftOp width op x y = bigIntToBits width (bigIntFrom x <+> op <+> y)

stringCompare : Doc -> Doc -> Doc -> Doc
stringCompare zeroComparison lhs rhs =
  idrisBoolFrom (stringOp lhs "compareTo" <+> paren rhs <+> zeroComparison)

runtimeCastOf : Constant -> Doc -> Doc
runtimeCastOf ty e = castTo (runtimeTypeOf ty) e

dartOp : {auto ctx : Ref Dart DartT}
  -> PrimFn argCount
  -> Vect argCount Doc
  -> Doc
dartOp (LT StringType) [x, y] = stringCompare " < 0" x y
dartOp (LTE StringType) [x, y] = stringCompare " <= 0" x y
dartOp (EQ StringType) [x, y] = stringCompare " == 0" x y
dartOp (GTE StringType) [x, y] = stringCompare " >= 0" x y
dartOp (GT StringType) [x, y] = stringCompare " > 0" x y
dartOp (LT ty) [x, y] = boolOpOf ty "<" x y
dartOp (LTE ty) [x, y] = boolOpOf ty "<=" x y
dartOp (EQ ty) [x, y] = boolOpOf ty "==" x y
dartOp (GTE ty) [x, y] = boolOpOf ty ">=" x y
dartOp (GT ty) [x, y] = boolOpOf ty ">" x y
dartOp (Add Bits8Type) [x, y] = boundedUIntOp 8 "+" x y
dartOp (Sub Bits8Type) [x, y] = boundedUIntOp 8 "-" x y
dartOp (Mul Bits8Type) [x, y] = boundedUIntOp 8 "*" x y
dartOp (Div Bits8Type) [x, y] = boundedUIntOp 8 "~/" x y
dartOp (Mod Bits8Type) [x, y] = boundedUIntOp 8 "%" x y
dartOp (Add Bits16Type) [x, y] = boundedUIntOp 16 "+" x y
dartOp (Sub Bits16Type) [x, y] = boundedUIntOp 16 "-" x y
dartOp (Mul Bits16Type) [x, y] = boundedUIntOp 16 "*" x y
dartOp (Div Bits16Type) [x, y] = boundedUIntOp 16 "~/" x y
dartOp (Mod Bits16Type) [x, y] = boundedUIntOp 16 "%" x y
dartOp (Add Bits32Type) [x, y] = boundedUIntOp 32 "+" x y
dartOp (Sub Bits32Type) [x, y] = boundedUIntOp 32 "-" x y
dartOp (Mul Bits32Type) [x, y] = boundedUIntOp 32 "*" x y
dartOp (Div Bits32Type) [x, y] = boundedUIntOp 32 "~/" x y
dartOp (Mod Bits32Type) [x, y] = boundedUIntOp 32 "%" x y
dartOp (Add Bits64Type) [x, y] = boundedUIntOp 64 "+" x y
dartOp (Sub Bits64Type) [x, y] = boundedUIntOp 64 "-" x y
dartOp (Mul Bits64Type) [x, y] = boundedUIntOp 64 "*" x y
dartOp (Div Bits64Type) [x, y] = boundedUIntOp 64 "~/" x y
dartOp (Mod Bits64Type) [x, y] = boundedUIntOp 64 "%" x y
dartOp (ShiftL Bits8Type) [x, y] = boundedShiftOp 8 "<<" x y
dartOp (ShiftL Bits16Type) [x, y] = boundedShiftOp 16 "<<" x y
dartOp (ShiftL Bits32Type) [x, y] = boundedShiftOp 32 "<<" x y
dartOp (ShiftL Bits64Type) [x, y] = boundedShiftOp 64 "<<" x y
dartOp (ShiftL ty) [x, y] = binOpOf ty "<<" x y
dartOp (ShiftR Bits8Type) [x, y] = boundedShiftOp 8 ">>" x y
dartOp (ShiftR Bits16Type) [x, y] = boundedShiftOp 16 ">>" x y
dartOp (ShiftR Bits32Type) [x, y] = boundedShiftOp 32 ">>" x y
dartOp (ShiftR Bits64Type) [x, y] = boundedShiftOp 64 ">>" x y
dartOp (ShiftR ty) [x, y] = binOpOf ty ">>" x y
dartOp (BAnd ty) [x, y] = binOpOf ty "&" x y
dartOp (BOr ty) [x, y] = binOpOf ty "|" x y
dartOp (BXOr ty) [x, y] = binOpOf ty "^" x y
dartOp (Add ty) [x, y] = binOpOf ty "+" x y
dartOp (Sub ty) [x, y] = binOpOf ty "-" x y
dartOp (Mul ty) [x, y] = binOpOf ty "*" x y
dartOp (Div ty@DoubleType) [x, y] = binOpOf ty "/" x y
dartOp (Div ty) [x, y] = binOpOf ty "~/" x y
dartOp (Mod ty) [x, y] = binOpOf ty "%" x y
dartOp (Neg ty) [x] = paren ("-" <+> runtimeCastOf ty x)
dartOp StrLength [x] = stringOp x "length"
dartOp StrHead [x] = stringOp x "codeUnitAt(0)"
dartOp StrIndex [x, y] = stringOp x "codeUnitAt" <+> paren y
dartOp StrTail [x] = stringOp x "substring(1)"
dartOp StrCons [x, y] = binOp "+" ("$.String.fromCharCode" <+> paren x) (castTo stringTy y)
dartOp StrAppend [x, y] = binOpOf' stringTy "+" x y
dartOp StrSubstr [offset, length, str] = (castTo stringTy str) <+> ".substring" <+> tupled [offset, binOpOf IntType "+" offset length]
dartOp (Cast StringType IntegerType) [x] = paren (bigIntTy <+> ".tryParse" <+> castTo stringTy x <+> " ?? " <+> bigIntTy <+> ".zero")
dartOp (Cast StringType DoubleType) [x] = paren (doubleTy <+> ".tryParse" <+> castTo stringTy x <+> " ?? 0.0")
dartOp (Cast StringType IntType) [x] = paren (intTy <+> ".tryParse" <+> castTo stringTy x <+> " ?? 0")
dartOp (Cast DoubleType IntType) [x] = doubleOp x "toInt()"
dartOp (Cast IntegerType IntType) [x] = bigIntToInt x
dartOp (Cast IntegerType Bits8Type) [x] = bigIntToBits 8 x
dartOp (Cast IntegerType Bits16Type) [x] = bigIntToBits 16 x
dartOp (Cast IntegerType Bits32Type) [x] = bigIntToBits 32 x
dartOp (Cast IntegerType Bits64Type) [x] = bigIntToBits 64 x
dartOp (Cast Bits8Type Bits16Type) [x] = x
dartOp (Cast Bits8Type Bits32Type) [x] = x
dartOp (Cast Bits8Type IntType) [x] = x
dartOp (Cast Bits16Type IntType) [x] = x
dartOp (Cast Bits16Type Bits32Type) [x] = x
dartOp (Cast Bits32Type IntType) [x] = x
dartOp (Cast Bits64Type IntegerType) [x] = x
dartOp (Cast Bits64Type IntType) [x] = bigIntToInt x
dartOp (Cast Bits64Type Bits8Type) [x] = bigIntToBits 8 x
dartOp (Cast Bits64Type Bits16Type) [x] = bigIntToBits 16 x
dartOp (Cast Bits64Type Bits32Type) [x] = bigIntToBits 32 x
dartOp (Cast CharType IntType) [x] = x
dartOp (Cast IntType CharType) [x] = x
dartOp (Cast ty Bits8Type) [x] = intToBits 8 x
dartOp (Cast ty Bits16Type) [x] = intToBits 16 x
dartOp (Cast ty Bits32Type) [x] = intToBits 32 x
dartOp (Cast ty Bits64Type) [x] = intToBits 64 x
dartOp (Cast ty IntegerType) [x] = bigIntFrom x
dartOp (Cast ty DoubleType) [x] = runtimeCastOf ty x <+> ".toDouble()"
dartOp (Cast ty StringType) [x] = x <+> ".toString()"
dartOp DoubleFloor [x] = doubleOp x "floorToDouble()"
dartOp DoubleCeiling [x] = doubleOp x "ceilToDouble()"
dartOp BelieveMe [_, _, x] = x
dartOp Crash [_, m] = assertionError m
dartOp e args = unsupported ("dartOp", e, args)

dartTypeFromExpression : {auto ctx : Ref Dart DartT} -> Expression -> Core Doc
dartTypeFromExpression ty = case ty of
  IEConstructor (Right "String") _ => pure stringTy
  IEConstructor (Right "Int") _ => pure intTy
  IEConstructor (Right "Integer") _ => pure bigIntTy
  IEConstructor (Right "Double") _ => pure doubleTy
  IEConstructor (Right "Prelude.Basics.Bool") _ => pure intTy -- Idris Bool is represented as int at runtime
  IEConstructor (Right "System.FFI.Struct") (IEConstant (Str ty) :: _) =>
    foreignTypeName ty
  IEConstructor (Right "Dart.FFI.Types.GenericType") [IEConstant (Str baseType), args] => do
    baseType' <- foreignTypeName baseType
    let Just argList = parseList args
      | _ => pure baseType'
    argList' <- traverse dartTypeFromExpression argList
    pure (baseType' <+> genericTypeArgs argList')
  _ => pure dynamic'

mutual
  dartBlock : {auto ctx : Ref Dart DartT} -> Statement -> Core Doc
  dartBlock s = block <$> dartStatement s

  dartLambda : {auto ctx : Ref Dart DartT} -> List Name -> Statement -> Core Doc
  dartLambda ps s = (paramList ps <+>) <$> dartBlock s

  commaSepExps : {auto ctx : Ref Dart DartT}
    -> List Expression
    -> Core Doc
  commaSepExps es = do
    es' <- traverse dartExp es
    pure (commaSep es')

  dartApp : {auto ctx : Ref Dart DartT} -> Expression -> List Expression -> Core Doc
  dartApp f args = do
    f' <- dartExp f
    args' <- traverse dartExp args
    pure (f' <+> argList args')

  dartConstructor : {auto ctx : Ref Dart DartT}
    -> Doc
    -> List Expression
    -> Core Doc
  dartConstructor tag args = case args of
    [] => pure (text "const [" <+> tag <+> "]")
    args => pure ("[" <+> tag <+> ", " <+> !(commaSepExps args) <+> "]")

  dartExp : {auto ctx : Ref Dart DartT}
    -> Expression
    -> Core Doc
  dartExp e = case e of
    IENull => pure null'
    IEConstant c => pure (dartConstant c)
    IEVar v => pure (dartName v)
    IELambda ps s => dartLambda ps s
    IEApp f@(IEVar (NS ns (UN "believe_me"))) args@[arg] =>
      if ns == builtinNS
        then dartExp arg
        else dartApp f args
    IEApp f args =>
      dartApp f args
    IEPrimFn f args =>
      pure (dartOp f !(traverseVect dartExp args))
    IEPrimFnExt n args =>
      dartPrimFnExt n args
    IEConstructor (Left tag) args =>
      dartConstructor (shown tag) args
    IEConstructor (Right tag) args =>
      dartConstructor (dartStringDoc tag) args
    IEConstructorHead e =>
      pure (castTo "$.List" !(dartExp e) <+> "[0]")
    IEConstructorTag (Left tag) =>
      pure (shown tag)
    IEConstructorTag (Right tag) =>
      pure (shown tag)
    IEConstructorArg i e =>
      pure (castTo "$.List" !(dartExp e) <+> "[" <+> shown i <+> "]")
    IEDelay e =>
      useDelay *> pure ("$Delayed" <+> paren ("() => " <+> !(dartExp e)))
    IEForce e =>
      pure (castTo "$Delayed" !(dartExp e) <+> ".force()")
    _ => pure (debug e)

  maybeCastTo : Maybe Doc -> Doc -> Doc
  maybeCastTo ty e = maybe e (flip castTo e) ty

  dartPrimNew : {auto ctx : Ref Dart DartT}
   -> Expression -> Expression -> String -> Expression -> Expression -> Core Doc
  dartPrimNew ty positionalTys ctorName positional named = do
    let posTys = collectPositional positionalTys
    let pos' = collectPositional positional
    let named' = collectNamed named
    let typedPos = zip posTys pos'
    posArgs <- traverse (uncurry dartForeignArg) typedPos
    namedArgs <- traverse dartNamedArg named'
    fTy <- dartTypeFromExpression ty
    let ctorName' = if length ctorName > 0 then text ("." ++ ctorName) else empty
    pure (fTy <+> ctorName' <+> argList (posArgs ++ namedArgs))

  dartPrimInvoke : {auto ctx : Ref Dart DartT}
    -> String -> Expression -> Expression -> Expression -> Expression -> Core Doc
  dartPrimInvoke fn typeArgs positionalTys positional named = do
    let posTys = collectPositional positionalTys
    let pos' = collectPositional positional
    let named' = collectNamed named
    let typedPos = zip posTys pos'
    posArgs <- traverse (uncurry dartForeignArg) typedPos
    namedArgs <- traverse dartNamedArg named'
    typeArgs' <- traverse dartTypeFromExpression (collectPositional typeArgs)
    let typeArgs'' = if null typeArgs' then empty else genericTypeArgs typeArgs'
    case (dartNameKindOf fn, posArgs) of
      (MemberName, this :: args) => do -- Method call
        thisTy <- methodReceiverTypeFrom positionalTys
        pure $ maybeCastTo thisTy this <+> text fn <+> typeArgs'' <+> argList (args ++ namedArgs)
      (TopLevelName, args) => do -- Static / Global function call
        fn' <- parseForeignName fn
        pure $ fn' <+> typeArgs'' <+> argList (args ++ namedArgs)
      (InfixOperator, [x, y]) => do
        xTy <- methodReceiverTypeFrom positionalTys
        pure $ binOp (text fn) (maybeCastTo xTy x) y
      _ =>
        pure $ unsupported ("prim__dart_invoke", fn, positional, named)

  dartPrimFnExt : {auto ctx : Ref Dart DartT}
    -> Name -> List Expression -> Core Doc
  dartPrimFnExt
    (NS _ (UN "prim__newIORef"))
    [IENull, e, _] = include refTyDef *> pure (refTy <+> paren !(dartExp e))
  dartPrimFnExt
    (NS _ (UN "prim__writeIORef"))
    [IENull, ref, e, _] = pure $ castTo refTy !(dartExp ref) <+> ".v = " <+> !(dartExp e)
  dartPrimFnExt
    (NS _ (UN "prim__readIORef"))
    [IENull, ref, _] = pure $ castTo refTy !(dartExp ref) <+> ".v"
  dartPrimFnExt
    (NS _ (UN "prim__setField"))
    (IEConstant (Str ty) :: _ :: _ :: e :: IEConstant (Str f) :: _ :: rhs :: _) = do
      fTy <- foreignTypeName ty
      pure (castTo fTy !(dartExp e) <+> dot <+> text f <+> " = " <+> !(dartExp rhs))
  dartPrimFnExt
    (NS _ (UN "prim__getField"))
    (IEConstant (Str ty) :: _ :: _ :: e :: IEConstant (Str f) :: _) = do
      fTy <- foreignTypeName ty
      pure (castTo fTy !(dartExp e) <+> dot <+> text f)
  dartPrimFnExt
    (NS _ (UN "prim__dart_set"))
    [ thisTy
      , valueTy
      , IEConstant (Str propertyName)
      , value
      , this
      , _
    ] = case isMemberName propertyName of
      True => pure (castTo !(dartTypeFromExpression thisTy) !(dartExp this) <+> text propertyName <+> " = " <+> !(dartExp value))
      False => pure (!(foreignTypeName propertyName) <+> " = " <+> !(dartExp value))
  dartPrimFnExt
    (NS _ (UN "prim__dart_get"))
    [ IENull
      , thisTy
      , IEConstant (Str propertyName)
      , this
      , _
    ] = case isMemberName propertyName of
      True => pure (castTo !(dartTypeFromExpression thisTy) !(dartExp this) <+> text propertyName)
      False => foreignTypeName propertyName
  dartPrimFnExt
    (NS _ (UN "prim__dart_get_pure"))
    [ IENull
      , thisTy
      , IEConstant (Str propertyName)
      , this
    ] = case isMemberName propertyName of
      True => pure (castTo !(dartTypeFromExpression thisTy) !(dartExp this) <+> text propertyName)
      False => foreignTypeName propertyName
  dartPrimFnExt
    (NS _ (UN "prim__dart_invoke"))
    [ IENull, IENull, IENull, IENull -- erased type arguments
      , positionalTys
      , IEConstant (Str fn)
      , typeArguments
      , positional
      , named
      , rest
    ] = dartPrimInvoke fn typeArguments positionalTys positional named
  dartPrimFnExt
    (NS _ (UN "prim__dart_invoke_pure"))
    [ IENull, IENull, IENull, IENull -- erased type arguments
      , positionalTys
      , IEConstant (Str fn)
      , typeArguments
      , positional
      , named
    ] = dartPrimInvoke fn typeArguments positionalTys positional named
  dartPrimFnExt
    (NS _ (UN "prim__dart_new_const"))
    [ IENull, IENull, IENull -- erased type arguments
      , ty
      , positionalTys
      , IEConstant (Str ctorName)
      , positional
      , named
    ] = dartPrimNew ty positionalTys ctorName positional named
  dartPrimFnExt
    (NS _ (UN "prim__dart_new"))
    [ IENull, IENull, IENull -- erased type arguments
      , ty
      , positionalTys
      , IEConstant (Str ctorName)
      , positional
      , named
      , _
    ] = dartPrimNew ty positionalTys ctorName positional named
  dartPrimFnExt
    (NS _ (UN "prim__dart_List_new"))
    [ elementTy
    , _
    ] = do
      elementTy' <- dartTypeFromExpression elementTy
      pure (text "<" <+> elementTy' <+> text ">[]")
  dartPrimFnExt
    (NS _ (UN "prim__dart_List_empty"))
    [ elementTy
    ] = do
      elementTy' <- dartTypeFromExpression elementTy
      pure (text "$.List<" <+> elementTy' <+> text ">.empty()")
  dartPrimFnExt
    (NS _ (UN "prim__dart_List_fromList"))
    [ elementTy
    , elements
    ] = do
      elementTy' <- dartTypeFromExpression elementTy
      case parseList elements of
        Just es => pure ("<" <+> elementTy' <+> ">" <+> bracket !(commaSepExps es))
        Nothing => do
          include primDartIterableFromList
          pure $
            text "$.List<" <+> elementTy' <+> ">.unmodifiable" <+> paren (
              "Dart_Iterable_fromList" <+> paren !(dartExp elements)
            )
  dartPrimFnExt
    (NS _ (UN "prim__dart_if"))
    [ IENull, condition, thenValue, elseValue ] =
    pure (!(dartExp condition) <+> " ? " <+> !(dartExp thenValue) <+> " : " <+> !(dartExp elseValue))
  dartPrimFnExt
    (NS _ (UN "prim__dart_unsafe_null"))
    _ = pure null'
  dartPrimFnExt n args = pure (unsupported (n, args))

  uncurryCallback : (hasIO : Bool) -> (args : List CFType) -> Expression -> Maybe (List Name, Statement)
  uncurryCallback = go []
    where
      go : List Name -> Bool -> List CFType -> Expression -> Maybe (List Name, Statement)
      go acc hasIO (_ :: as) (IELambda [n] (ReturnStatement e)) = go (n :: acc) hasIO as e
      go acc True  []        (IELambda [n] e) = Just (n :: acc, e)
      go acc False (_ :: as) (IELambda [n] e) = Just (n :: acc, e)
      go acc False []        e = Just (acc, ReturnStatement e)
      go _   _     _         _ = Nothing

  dartForeignArg : {auto ctx : Ref Dart DartT} -> Expression -> Expression -> Core Doc
  dartForeignArg _ (IEPrimFnExt (NS _ (UN "prim__dart_unsafe_null")) _) =
    pure null'
  dartForeignArg ty value =
    case parseFunctionType ty of
      -- Optimize curried IO callbacks
      Just fTy@(args, CFIORes _) =>
        case uncurryCallback True args value of
          -- TODO: Optimize partial applications
          Just (worldP :: ps, e) => do
            e' <- dartStatement e
            let ignoreWarning = "// ignore: unused_local_variable"
            let world = "const " <+> dartName worldP <+> " = " <+> world' <+> semi
            pure $ tupled (dartName <$> reverse ps) <+> block (vcat [ignoreWarning, world, e'])
          _ => makeCallback fTy <$> dartExp value
      -- Optimize curried pure callbacks
      Just (args, _) =>
        case uncurryCallback False args value of
          Just (ps, e) => pure $ tupled (dartName <$> reverse ps) <+> !(dartBlock e)
          _ => dartExp value
      _ => dartExp value

  dartNamedArg : {auto ctx : Ref Dart DartT} -> (Expression, String, Expression) -> Core Doc
  dartNamedArg (ty, name, value) =
    pure (text name <+> ": " <+> !(dartForeignArg ty value))

  methodReceiverTypeFrom : {auto ctx : Ref Dart DartT} -> Expression -> Core (Maybe Doc)
  methodReceiverTypeFrom (IEConstructor (Left 1) (ty :: _)) =
    Just <$> dartTypeFromExpression ty
  methodReceiverTypeFrom _ =
    pure Nothing

  ||| Collects the parameter name and value pairs from the expression
  ||| representing a `ParamList _`.
  collectNamed : Expression -> List (Expression, String, Expression)
  collectNamed e = go [] e
    where
      go : List (Expression, String, Expression) -> Expression -> List (Expression, String, Expression)
      go acc ({- ParamList.:: -} IEConstructor (Left 1) [{- Assign key value -} IEConstructor (Left 0) [ty, IEConstant (Str key), value],  es]) = go ((ty, key, value) :: acc) es
      go acc _ = reverse acc

  dartCase : {auto ctx : Ref Dart DartT}
    -> (Expression, Statement)
    -> Core Doc
  dartCase (e, s) = do
    e' <- case e of
      IEConstant (BI i) => pure (shown i)
      _ => dartExp e
    s' <- dartStatement s
    pure ("case " <+> e' <+> ":" <+> block s' <+> line <+> "break;")

  defaultDartCase : {auto ctx : Ref Dart DartT}
    -> Maybe Statement
    -> Core Doc
  defaultDartCase dc = case dc of
    Just s => do
      s' <- dartStatement s
      pure (line <+> "default:" <+> block s' <+> line <+> "break;")
    Nothing => pure empty

  dartSwitch : {auto ctx : Ref Dart DartT}
    -> Doc
    -> List (Expression, Statement)
    -> Maybe Statement
    -> Core Doc
  dartSwitch e cases def = do
    cases' <- traverse dartCase cases
    def' <- defaultDartCase def
    pure ("switch " <+> paren e <+> block (vcat cases' <+> def'))

  dartStatement : {auto ctx : Ref Dart DartT}
    -> Statement
    -> Core Doc
  dartStatement s = case s of
    FunDecl fc n ps body =>
      pure (line <+> docCommentFor fc n <+> dartName n <+> !(dartLambda ps body))
    ForeignDecl fc n ss args ret =>
      pure (line <+> !(foreignDecl n ss args ret))
    SwitchStatement e cases@((IEConstant (BI _), _) :: _) maybeDefault =>
      dartSwitch (bigIntToInt !(dartExp e)) cases maybeDefault
    SwitchStatement e cases maybeDefault =>
      dartSwitch !(dartExp e) cases maybeDefault
    SeqStatement a b =>
      pure (!(dartStatement a) <+> line <+> !(dartStatement b))
    ReturnStatement e =>
      pure ("return " <+> !(dartExp e) <+> semi)
    EvalExpStatement e =>
      pure (!(dartExp e) <+> semi)
    ConstDecl n e =>
      dartVar final' n (Just e)
    LetDecl n maybeE =>
      dartVar var' n maybeE
    MutateStatement n e =>
      pure (dartName n <+> " = " <+> !(dartExp e) <+> semi)
    ErrorStatement s =>
      pure (assertionError (dartStringDoc s))
    ForEverLoop s =>
      pure ("while (true)" <+> block !(dartStatement s))
    CommentStatement c =>
      pure (comment c)
    DoNothing => pure empty

  dartVar : {auto ctx : Ref Dart DartT}
    -> (keyword : Doc)
    -> Name
    -> Maybe Expression
    -> Core Doc
  dartVar kw n init = case init of
    Just e => pure (kw <+> dartName n <+> " = " <+> !(dartExp e) <+> semi)
    Nothing => pure (kw <+> dartName n <+> semi)

dartImport : (String, Doc) -> Doc
dartImport (lib, alias) =
  "import \"" <+> text lib <+> "\" as " <+> alias <+> semi

header : List Doc
header = [
  text "// @dart = 2.6",
  text "// DO NOT CHANGE THIS FILE!",
  text "// It has been generated by idris2dart.",
  text "// ignore_for_file: non_constant_identifier_names",
  text "// ignore_for_file: unnecessary_cast"
]

delayClass : Doc
delayClass = text """
class $Delayed {
  $.dynamic Function() e;
  $.dynamic value;
  $Delayed(this.e);
  $.dynamic force() {
    final e = this.e;
    if (e != null) {
      this.value = e();
      this.e = null;
    }
    return this.value;
  }
}
"""

nubSort : Ord a => List a -> List a
nubSort = SortedSet.toList . SortedSet.fromList

mainFunctionFor : Doc -> (usesArgs : Bool) -> Doc
mainFunctionFor mainBody = \case
  False => "void main()" <+> block mainBody
  True => vcat [
    "$.List<$.String> $args;",
    emptyLine,
    "void main($.List<$.String> $$args)" <+> block (vcat ["$args = $$args;", mainBody])
  ]

compileToDart : Ref Ctxt Defs -> ClosedTerm -> Core Doc
compileToDart defs term = do
  (impDefs, impMain) <- compileToImperative defs term
  ctx <- newRef Dart (MkDartT (fromList [("dart:core", "$")]) 1 empty empty False False)
  dartDefs <- dartStatement impDefs
  dartMain <- dartStatement impMain
  finalState <- get Dart
  let includeLines = concatMap (toList . lines) (SortedSet.toList finalState.includes)
  let (importLines, nonImportLines) = partition ("import " `isPrefixOf`) includeLines
  let includeImports' = text <$> nubSort importLines
  let includes' = text (unlines nonImportLines)
  let imports' = dartImport <$> toList finalState.imports
  let header' = vcat (header ++ imports' ++ includeImports')
  let mainDecl = mainFunctionFor dartMain finalState.usesArgs
  let footer = if finalState.usesDelay then delayClass else empty
  pure $
    header'
      <+> emptyLine
      <+> mainDecl
      <+> line
      <+> dartDefs
      <+> line
      <+> delayClass
      <+> includes'

compileToDartFile : String -> Ref Ctxt Defs -> ClosedTerm -> Core ()
compileToDartFile file defs term = do
  dartDoc <- compileToDart defs term
  Right _ <- coreLift (writeDocToFile file dartDoc)
    | Left err => throw (FileErr file err)
  pure ()

compile : Ref Ctxt Defs
  -> (tmpDir : String)
  -> (outputDir : String)
  -> ClosedTerm
  -> (outfile : String)
  -> Core (Maybe String)
compile defs tmpDir outputDir term file = do
  compileToDartFile (outputDir ++ "/" ++ file) defs term
  pure Nothing

execute : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
execute defs tmpDir term = do
  let tempDartFile = tmpDir ++ "/temp.dart"
  compileToDartFile tempDartFile defs term
  ignore $ coreLift $ system ("dart" ++ " " ++ tempDartFile)
  pure ()

dartCodegen : Codegen
dartCodegen = MkCG compile execute Nothing Nothing

main : IO ()
main = mainWithCodegens [("dart", dartCodegen)]


text:
module Effect.Memory

import Effects
import Control.IOExcept

%access public

abstract
data MemoryChunk : Nat -> Nat -> Type where
     CH : Ptr -> MemoryChunk size initialized

abstract
data RawMemory : Effect where
     Allocate   : (n : Nat) ->
                  RawMemory () () (\v => MemoryChunk n 0)
     Free       : RawMemory () (MemoryChunk n i) (\v => ())
     Initialize : Bits8 ->
                  (size : Nat) ->
                  so (i + size <= n) ->
                  RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (i + size))
     Peek       : (offset : Nat) ->
                  (size : Nat) ->
                  so (offset + size <= i) ->
                  RawMemory (Vect size Bits8)
                            (MemoryChunk n i) (\v => MemoryChunk n i)
     Poke       :  (offset : Nat) ->
                  (Vect size Bits8) ->
                  so (offset <= i && offset + size <= n) ->
                  RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (max i (offset + size)))
     Move       : (src : MemoryChunk src_size src_init) ->
                  (dst_offset : Nat) ->
                  (src_offset : Nat) ->
                  (size : Nat) ->
                  so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
                  so (src_offset + size <= src_init) ->
                  RawMemory () (MemoryChunk dst_size dst_init)
                            (\v => MemoryChunk dst_size (max dst_init (dst_offset + size)))
     GetRawPtr  : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i)

private
do_malloc : Nat -> IOExcept String Ptr
do_malloc size with (fromInteger (cast size) == size)
  | True  = do ptr <- ioe_lift $ mkForeign (FFun "malloc" [FInt] FPtr) (fromInteger $ cast size)
               fail  <- ioe_lift $ nullPtr ptr
               if fail then ioe_fail "Cannot allocate memory"
               else return ptr
  | False = ioe_fail "The target architecture does not support adressing enough memory"

private
do_memset : Ptr -> Nat -> Bits8 -> Nat -> IO ()
do_memset ptr offset c size
  = mkForeign (FFun "idris_memset" [FPtr, FInt, FByte, FInt] FUnit)
              ptr (fromInteger $ cast offset) c (fromInteger $ cast size)

private
do_free : Ptr -> IO ()
do_free ptr = mkForeign (FFun "free" [FPtr] FUnit) ptr

private
do_memmove : Ptr -> Ptr -> Nat -> Nat -> Nat -> IO ()
do_memmove dest src dest_offset src_offset size
  = mkForeign (FFun "idris_memmove" [FPtr, FPtr, FInt, FInt, FInt] FUnit)
              dest src (fromInteger $ cast dest_offset) (fromInteger $ cast src_offset) (fromInteger $ cast size)

private
do_peek : Ptr -> Nat -> (size : Nat) -> IO (Vect size Bits8)
do_peek _   _       Z = return (Prelude.Vect.Nil)
do_peek ptr offset (S n)
  = do b <- mkForeign (FFun "idris_peek" [FPtr, FInt] FByte) ptr (fromInteger $ cast offset)
       bs <- do_peek ptr (S offset) n
       Prelude.Monad.return (Prelude.Vect.(::) b bs)

private
do_poke : Ptr -> Nat -> Vect size Bits8 -> IO ()
do_poke _   _      []     = return ()
do_poke ptr offset (b::bs)
  = do mkForeign (FFun "idris_poke" [FPtr, FInt, FByte] FUnit) ptr (fromInteger $ cast offset) b
       do_poke ptr (S offset) bs

instance Handler RawMemory (IOExcept String) where
  handle () (Allocate n) k
    = do ptr <- do_malloc n
         k () (CH ptr)
  handle {-{res = MemoryChunk _ offset}-} (CH ptr) (Initialize {i} c size _) k
    = ioe_lift (do_memset ptr i c size) $> k () (CH ptr)
  handle (CH ptr) (Free) k
    = ioe_lift (do_free ptr) $> k () ()
  handle (CH ptr) (Peek offset size _) k
    = do res <- ioe_lift (do_peek ptr offset size)
         k res (CH ptr)
  handle (CH ptr) (Poke offset content _) k
    = do ioe_lift (do_poke ptr offset content)
         k () (CH ptr)
  handle (CH dest_ptr) (Move (CH src_ptr) dest_offset src_offset size _ _) k
    = do ioe_lift (do_memmove dest_ptr src_ptr dest_offset src_offset size)
         k () (CH dest_ptr)
  handle chunk (GetRawPtr) k
    = k chunk chunk

RAW_MEMORY : Type -> EFFECT
RAW_MEMORY t = MkEff t RawMemory

allocate : (n : Nat) ->
           Eff m () [RAW_MEMORY ()] (\v => [RAW_MEMORY (MemoryChunk n 0)])
allocate size = Allocate size

initialize : {i : Nat} ->
             {n : Nat} ->
             Bits8 ->
             (size : Nat) ->
             so (i + size <= n) ->
             Eff m () [RAW_MEMORY (MemoryChunk n i)]
                       (\v => [RAW_MEMORY (MemoryChunk n (i + size))])
initialize c size prf = Initialize c size prf

free : Eff m () [RAW_MEMORY (MemoryChunk n i)] (\v => [RAW_MEMORY ()])
free = Free

peek : {i : Nat} ->
       (offset : Nat) ->
       (size : Nat) ->
       so (offset + size <= i) ->
       { [RAW_MEMORY (MemoryChunk n i)] } Eff m (Vect size Bits8)
peek offset size prf = Peek offset size prf

poke : {n : Nat} ->
       {i : Nat} ->
       (offset : Nat) ->
       Vect size Bits8 ->
       so (offset <= i && offset + size <= n) ->
       Eff m () [RAW_MEMORY (MemoryChunk n i)]
              (\v => [RAW_MEMORY (MemoryChunk n (max i (offset + size)))])
poke offset content prf = Poke offset content prf

private
getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff m (MemoryChunk n i)
getRawPtr = GetRawPtr

private
move' : {dst_size : Nat} ->
        {dst_init : Nat} ->
        {src_init : Nat} ->
        (src_ptr : MemoryChunk src_size src_init) ->
        (dst_offset : Nat) ->
        (src_offset : Nat) ->
        (size : Nat) ->
        so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
        so (src_offset + size <= src_init) ->
        Eff m () [RAW_MEMORY (MemoryChunk dst_size dst_init)]
               (\v => [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))])
move' src_ptr dst_offset src_offset size dst_bounds src_bounds
  = Move src_ptr dst_offset src_offset size dst_bounds src_bounds

data MoveDescriptor = Dst | Src

move : {dst_size : Nat} ->
       {dst_init : Nat} ->
       {src_size : Nat} ->
       {src_init : Nat} ->
       (dst_offset : Nat) ->
       (src_offset : Nat) ->
       (size : Nat) ->
       so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
       so (src_offset + size <= src_init) ->
       Eff m ()
              [ Dst ::: RAW_MEMORY (MemoryChunk dst_size dst_init)
              , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)]
              (\v =>
                [ Dst ::: RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))
                , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)])
move dst_offset src_offset size dst_bounds src_bounds
  = do src_ptr <- Src :- getRawPtr
       Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds
       return ()

ext: idr

max_stars_repo_name: edwinb/Eff-new

max_issues_repo_name: edwinb/Eff-new

max_forks_repo_name: edwinb/Eff-new


text:
module Data.Time.Calendar

import Data.Time.Calendar.Days

export
data DayOfWeek
  = Monday
  | Tuesday
  | Wednesday
  | Thursday
  | Friday
  | Saturday
  | Sunday

export
Enum DayOfWeek where
  pred Monday = Tuesday
  pred Tuesday = Wednesday
  pred Wednesday = Thursday
  pred Thursday = Friday
  pred Friday = Saturday
  pred Saturday = Sunday
  pred Sunday = Monday
  toNat Monday = 1
  toNat Tuesday = 2
  toNat Wednesday = 3
  toNat Thursday = 4
  toNat Friday = 5
  toNat Saturday = 6
  toNat Sunday = 7

  -- this is really slow!! and unusable. I am not able to get a total function out of this using (fromNat : x -> Int)
  fromNat x = case x of
                   Z => Sunday
                   (S (S (S (S (S (S (S k))))))) => fromNat k
                   (S (S (S (S (S (S k)))))) => Saturday
                   (S (S (S (S (S k))))) => Friday
                   (S (S (S (S k)))) => Thursday
                   (S (S (S k))) => Wednesday
                   (S (S k)) => Tuesday
                   (S k) => Monday

dayOfWeek : Day -> DayOfWeek
dayOfWeek (MkModifiedJulianDay d) = let x = fromInteger (d + 3)
  in
    case mod x 7 of
         0 => Sunday
         1 => Monday
         2 => Tuesday
         3 => Wednesday
         4 => Thursday
         5 => Friday
         _ => Saturday

--dayOfWeek (MkModifiedJulianDay d)

max_stars_repo_name: gdevanla/idris-time

max_issues_repo_name: gdevanla/idris-time

max_forks_repo_name: gdevanla/idris-time


text:
module Test.Spec

import Specdris.Spec
import Text.Parse.Tibetan
import Text.Show.Tibetan

export

specSuite : IO ()
specSuite = do
  spec $ do
    describe "readTest" $ do
      it "should parse Latin numerals" $ do
        readTest "126" `shouldBe` Right 126
        --readBo "༡༢༦" `shouldBe` Right 126
    describe "showTest" $ do
      it "should display numerals" $ do
        showTest 123 `shouldBe` "123"
        --showBo 123 `shouldBe` "༡༢༣"


text:
module Data.Sign

%default total

||| A representation of signs for signed datatypes such as `ZZ`
public export
data Sign = Plus | Zero | Minus

public export
opposite : Sign -> Sign
opposite Plus  = Minus
opposite Zero  = Zero
opposite Minus = Plus

public export
multiply : Sign -> Sign -> Sign
multiply Zero  _    = Zero
multiply _     Zero = Zero
multiply Plus  x    = x
multiply Minus x    = opposite x

||| Discover the sign of some type
public export
interface Signed t where
  sign : t -> Sign

public export
Signed Int where
  sign x with (compare x 0)
    sign x | LT = Minus
    sign x | EQ = Zero
    sign x | GT = Plus

public export
Signed Integer where
  sign x with (compare x 0)
    sign x | LT = Minus
    sign x | EQ = Zero
    sign x | GT = Plus

public export
Signed Double where
  sign x with (compare x 0.0)
    sign x | LT = Minus
    sign x | EQ = Zero
    sign x | GT = Plus

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
module Leap

export
isLeap : Int -> Bool
isLeap year =
  (divBy 4 && not (divBy 100)) || divBy 400
  where divBy : Int -> Bool
        divBy n = (year `mod` n) == 0

export
version : String
version = "1.0.0"


text:
main : IO()
main = putStrLn "elz compiler"

max_stars_repo_name: dannypsnl/languages-learn

max_issues_repo_name: dannypsnl/languages-learn

max_forks_repo_name: dannypsnl/languages-learn


text:
import Data.Vect

word_lengths : Vect len String -> Vect len Nat
word_lengths [] = []
word_lengths (x :: xs) = length x :: word_lengths xs

-- insertion sort
insert : Ord elem =>
         (x : elem) -> (xs_sorted : Vect k elem) -> Vect (S k) elem
insert x [] = [x]
insert x (y :: xs) = case x < y of
                          False => y :: insert x xs
                          True => x :: y :: xs

ins_sort : Ord elem => Vect n elem -> Vect n elem
ins_sort [] = []
ins_sort (x :: xs) = let xs_sorted = ins_sort xs in
                         insert x xs_sorted

-- 3.2.4 excercises

my_length : List a -> Nat
my_length [] = 0
my_length (x :: xs) = 1 + (my_length xs)

||| length using type var
my_length_vect : Vect n a -> Nat
my_length_vect {n} xs = n

my_reverse : List a -> List a
my_reverse = foldl (flip (::)) []

mymap : (a -> b) -> List a -> List b
mymap f [] = []
mymap f (x :: xs) = f x :: mymap f xs

-- this one generated itself!!
mymapv : (a -> b) -> Vect n a -> Vect n b
mymapv f [] = []
mymapv f (x :: xs) = f x :: mymapv f xs

-- 3.3

create_empties : Vect n (Vect 0 elem)
create_empties = replicate _ []

transpose_helper : (x : Vect n elem) -> (xs_trans : Vect n (Vect k elem)) ->
                    Vect n (Vect (S k) elem)
transpose_helper [] [] = []
transpose_helper (x :: xs) (y :: ys) = (x :: y) :: transpose_helper xs ys
-- usage replaced by zipWith

transpose_mat : Vect m (Vect n elem) -> Vect n (Vect m elem)
transpose_mat [] = create_empties
transpose_mat (x :: xs) = let xs_trans = transpose_mat xs in
                              zipWith (::) x xs_trans

addMatrix : Num a => Vect n (Vect m a) -> Vect n (Vect m a) ->
            Vect n (Vect m a)
addMatrix [] [] = []
addMatrix (x :: xs) (y :: ys) = zipWith (+) x y :: addMatrix xs ys

max_stars_repo_name: minimal/idris-experiments

max_issues_repo_name: minimal/idris-experiments

max_forks_repo_name: minimal/idris-experiments


text:
module Fractions

%default total

record Fraction : Type where
  F : (top : Nat) -> (bottom : Nat) -> Fraction

corecord Tree : Type -> Type where
  value : Tree a -> a
  left : Tree a -> Tree a
  right : Tree a -> Tree a
  constructor MkTree

fracSum : Fraction -> Nat
fracSum (F top bottom) = top + bottom

leftFrac : Fraction -> Fraction
leftFrac f = F (top f) (fracSum f)

rightFrac : Fraction -> Fraction
rightFrac f = F (fracSum f) (bottom f)

total causal flattenTree : Tree a -> Stream a
flattenTree t = ft []
  where
    total causal ft : List (Tree a) -> Stream a
    ft [] = (value t) :: (ft [left t, right t])
    ft (tree :: xs) = (value tree) :: (ft (xs ++ [left tree, right tree]))

total causal rationalTree : Tree Fraction
rationalTree = rt $ F (S Z) (S Z)
  where
    total causal rt : Fraction -> Tree Fraction
    rt f = MkTree f (rt $ leftFrac f) (rt $ rightFrac f)

--total causal rationals : Stream Fraction
--rationals = flattenTree $ rationalTree

max_stars_repo_name: sualitu/thesis

max_issues_repo_name: sualitu/thesis

max_forks_repo_name: sualitu/thesis


text:
module Imperative.Parser

import DataStructures as DS
import Lexer
import Lightyear.Core
import Lightyear.Combinators
import Lightyear.Char
import Lightyear.Strings

identifier : Parser DS.AExpr
identifier = do f <- satisfy (isAlpha)
                i <- many letter
                pure (Var (pack (f :: i)))

intConst : Parser DS.AExpr
intConst = do i <- integer
              pure (IntConst i)

infixOp : Parser () -> (a -> a -> a) -> Parser (a -> a -> a)
infixOp l ctor = do
  _ <- l
  pure ctor

addOp : Parser (AExpr -> AExpr -> AExpr)
addOp = infixOp (rPlus) (ABinary Add) <|> infixOp (rMinus) (ABinary Subtract)
mulOp : Parser (AExpr -> AExpr -> AExpr)
mulOp = infixOp (rTimes) (ABinary Multiply) <|> infixOp (rDivide) (ABinary Divide)

mutual
  aExpression : Parser AExpr
  aExpression = chainl1 term addOp

  term : Parser DS.AExpr
  term = chainl1 factor mulOp

  factor : Parser DS.AExpr
  factor = intConst
    <|> identifier
    <|> negate
    <|> subExpr

  negate : Parser DS.AExpr
  negate = do (token "-")
              f <- factor
              pure $ Neg f

  subExpr : Parser DS.AExpr
  subExpr = do
    _ <- token "("
    expr <- aExpression
    _ <- token ")"
    pure expr

-- relational
relationalOp : Parser (AExpr -> AExpr -> BExpr)
relationalOp = (rGT) *> pure (RBinary Greater) <|> (rLT) *> pure (RBinary Less)

rExpression : Parser BExpr
rExpression =
  do a1 <- aExpression
     op <- relationalOp
     a2 <- aExpression
     pure (op a1 a2)

-- come back for parens bExpression
mutual
  bTerm : Parser BExpr
  bTerm = spaces *> ((rTrue *> pure (BoolConst True)) <|> (rFalse *> pure (BoolConst False)) <|> rExpression <|> subBExpr) <* spaces

  boolOp : Parser (BExpr -> BExpr -> BExpr)
  boolOp = infixOp (rAnd) (BBinary And) <|> infixOp (rOr) (BBinary Or)

  notOp : Parser (BExpr)
  notOp = do rNot
             b <- bExpression
             pure (BNot b)

  bExpression : Parser BExpr
  bExpression = notOp <|> chainl1 bTerm boolOp

  subBExpr : Parser BExpr
  subBExpr = do
    _ <- token "("
    expr <- bExpression
    _ <- token ")"
    pure expr

-- statements

-- If there's only one statement return it without using Seq.
statementFromList : List Stmt -> Stmt
statementFromList (x :: []) = x
statementFromList xs = Seq xs

mutual
  statement' : Parser Stmt
  statement' =
    ifStmt
    <|> whileStmt
    <|> skipStmt
    <|> assignStmt

  sequenceOfStmt : Parser Stmt
  sequenceOfStmt =
    do list <- (sepBy1 statement' (token ";"))
       pure (statementFromList list)

  statement : Parser Stmt
  statement = sequenceOfStmt <|>| parens statement

  ifStmt : Parser Stmt
  ifStmt = do
    rIf
    cond  <- bExpression
    rThen
    stmt1 <- statement
    rElse
    stmt2 <- statement
    pure (If cond stmt1 stmt2)

  whileStmt : Parser Stmt
  whileStmt = do
    rWhile
    cond <- bExpression
    rDo
    stmt <- statement
    pure (While cond stmt)

  assignStmt : Parser Stmt
  assignStmt =
    do var  <- identifier
       rAssign
       expr <- aExpression
       pure (Assign var expr)

  skipStmt : Parser Stmt
  skipStmt = do rSkip ; pure Skip

max_stars_repo_name: alexhumphreys/pl-playground

max_issues_repo_name: alexhumphreys/pl-playground

max_forks_repo_name: alexhumphreys/pl-playground


text:
||| Spec: https://webassembly.github.io/spec/core/syntax/types.html#external-types
module WebAssembly.Structure.Types.ExternalTypes

import WebAssembly.Structure.Types.ValueTypes
import WebAssembly.Structure.Types.FunctionTypes
import WebAssembly.Structure.Types.TableTypes
import WebAssembly.Structure.Types.Limits
import WebAssembly.Structure.Types.MemoryTypes
import WebAssembly.Structure.Types.GlobalTypes

import Decidable.Equality

-- Definition

public export
data ExternType : Type where
  Func   : FuncType    -> ExternType
  Table  : TableType   -> ExternType
  Mem    : MemType     -> ExternType
  Global : GlobalType  -> ExternType

-- Equality

total public export
lemma_externtype__func_injective : ((x = y) -> Void) -> (Func x = Func y) -> Void
lemma_externtype__func_injective func_types_neq Refl = func_types_neq Refl

total public export
lemma_externtype__table_injective : ((x = y) -> Void) -> (Table x = Table y) -> Void
lemma_externtype__table_injective table_tables_neq Refl = table_tables_neq Refl

total public export
lemma_externtype__mem_injective : ((x = y) -> Void) -> (Mem x = Mem y) -> Void
lemma_externtype__mem_injective mem_types_neq Refl = mem_types_neq Refl

total public export
lemma_externtype__global_injective : ((x = y) -> Void) -> (Global x = Global y) -> Void
lemma_externtype__global_injective global_types_neq Refl = global_types_neq Refl

total public export
lemma_func_not_table : (Func x = Table y) -> Void
lemma_func_not_table Refl impossible

total public export
lemma_func_not_mem : (Func x = Mem y) -> Void
lemma_func_not_mem Refl impossible

total public export
lemma_func_not_global : (Func x = Global y) -> Void
lemma_func_not_global Refl impossible

total public export
lemma_table_not_func : (Table x = Func y) -> Void
lemma_table_not_func Refl impossible

total public export
lemma_table_not_mem : (Table x = Mem y) -> Void
lemma_table_not_mem Refl impossible

total public export
lemma_table_not_global : (Table x = Global y) -> Void
lemma_table_not_global Refl impossible

total public export
lemma_mem_not_func : (Mem x = Func y) -> Void
lemma_mem_not_func Refl impossible

total public export
lemma_mem_not_table : (Mem x = Table y) -> Void
lemma_mem_not_table Refl impossible

total public export
lemma_mem_not_global : (Mem x = Global y) -> Void
lemma_mem_not_global Refl impossible

total public export
lemma_global_not_func : (Global x = Func y) -> Void
lemma_global_not_func Refl impossible

total public export
lemma_global_not_table : (Global x = Table y) -> Void
lemma_global_not_table Refl impossible

total public export
lemma_global_not_mem : (Global x = Mem y) -> Void
lemma_global_not_mem Refl impossible

-- Decidable Equality

public export
implementation DecEq ExternType where
  decEq (Func x)   (Func y)   = case decEq x y of
    No func_types_neq => No (lemma_externtype__func_injective func_types_neq)
    Yes Refl          => Yes Refl
  decEq (Table x)  (Table y)  = case decEq x y of
    No table_tables_neq => No (lemma_externtype__table_injective table_tables_neq)
    Yes Refl            => Yes Refl
  decEq (Mem x)    (Mem y)    = case decEq x y of
    No mem_types_neq => No (lemma_externtype__mem_injective mem_types_neq)
    Yes Refl         => Yes Refl
  decEq (Global x) (Global y) = case decEq x y of
    No global_types_neq => No (lemma_externtype__global_injective global_types_neq)
    Yes Refl            => Yes Refl
  decEq (Func x)   (Table y)  = No lemma_func_not_table
  decEq (Func x)   (Mem y)    = No lemma_func_not_mem
  decEq (Func x)   (Global y) = No lemma_func_not_global
  decEq (Table x)  (Func y)   = No lemma_table_not_func
  decEq (Table x)  (Mem y)    = No lemma_table_not_mem
  decEq (Table x)  (Global y) = No lemma_table_not_global
  decEq (Mem x)    (Func y)   = No lemma_mem_not_func
  decEq (Mem x)    (Table y)  = No lemma_mem_not_table
  decEq (Mem x)    (Global y) = No lemma_mem_not_global
  decEq (Global x) (Func y)   = No lemma_global_not_func
  decEq (Global x) (Table y)  = No lemma_global_not_table
  decEq (Global x) (Mem y)    = No lemma_global_not_mem

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module TicTacToe.Player

%default total
%access export

public export
data Player = Cross
            | Nought

public export
Eq Player where
  Cross  == Cross  = True
  Nought == Nought = True
  _ == _ = False

Show Player where
  show Cross  = "X"
  show Nought = "O"

showCell : Maybe Player -> String
showCell Nothing  = " "
showCell (Just c) = show c

public export
switch : Player -> Player
switch Cross = Nought
switch Nought = Cross

max_stars_repo_name: ShinKage/DT-TicTacToe

max_issues_repo_name: ShinKage/DT-TicTacToe

max_forks_repo_name: ShinKage/DT-TicTacToe


text:
module Leibniz
import Control.Monad.Identity

data Eq : (a : Type) -> (b : Type) -> Type where
  Subs : ({f : Type -> Type} -> f a -> f b) -> Eq a b

refl : Eq a a
refl = Subs id

subst : {f : Type -> Type} -> Eq a b -> f a -> f b
subst (Subs subs) fa = subs fa

trans : Eq a b -> Eq b c -> Eq a c
trans ab bc = subst bc ab

cast : Eq a b -> a -> b
cast eq = runIdentity . subst eq . Id

Flip : (Type -> Type -> Type) -> Type -> Type -> Type
Flip f a b = f b a

symm : Eq a b -> Eq b a
symm eq = subst {f = Flip Eq a} eq refl

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Main

import Control.Monad.State
import Data.Fin
import Lightyear
import Lightyear.Char
import Lightyear.Position
import Lightyear.Strings as LS

-- data structures

data Seat = NoSeat
          | EmptySeat
          | OccupiedSeat

Eq Seat where
  (==) NoSeat NoSeat = True
  (==) NoSeat EmptySeat = False
  (==) NoSeat OccupiedSeat = False
  (==) EmptySeat NoSeat = False
  (==) EmptySeat EmptySeat = True
  (==) EmptySeat OccupiedSeat = False
  (==) OccupiedSeat NoSeat = False
  (==) OccupiedSeat EmptySeat = False
  (==) OccupiedSeat OccupiedSeat = True

Show Seat where
  show NoSeat = "NoSeat"
  show EmptySeat = "EmptySeat"
  show OccupiedSeat = "OccupiedSeat"

data WaitingArea : Nat -> Nat -> Type where
  MkWaitingArea : Vect y (Vect x Seat) -> WaitingArea x y

Eq (WaitingArea x y) where
  (==) (MkWaitingArea a) (MkWaitingArea b) = a == b

Show (WaitingArea x y) where
  show (MkWaitingArea seats) = show "WaitingArea " ++ show seats

record Coordinate (x : Nat) (y : Nat) where
  constructor MkCoordinate
  xCoord : Fin x
  yCoord : Fin y

Show (Fin n) where
  show {n=n} fin = "Fin " ++ show n ++ " " ++ show (finToNat fin)

Show (Coordinate x y) where
  show (MkCoordinate xCoord yCoord) = show "Coordinate "  ++ show xCoord ++ " " ++ show yCoord

-- parsing

pSeat : Parser Seat
pSeat = do
  s <- oneOf ".L#"
  pure $ case s of
              '.' => NoSeat
              'L' => EmptySeat
              '#' => OccupiedSeat

pLine : Parser (Vect x Seat)
pLine {x=n} = ntimes n pSeat <* newline

pData : Parser (Vect y (Vect x Seat))
pData {y=n} = ntimes n pLine <* eof

parseCountX : String -> Either String Nat
parseCountX = LS.parse $ (Prelude.Nat.pred . colNo) <$> (many pSeat *> getPosition)

parseCountY : String -> Either String Nat
parseCountY = LS.parse $ (Prelude.Nat.pred . lineNo) <$> (many ((many pSeat) <* newline) *> getPosition)

parseCountXY : String -> Either String (Nat,Nat)
parseCountXY str = do
  x <- parseCountX str
  y <- parseCountY str
  pure (x,y)

parseWaitingArea : (x : Nat) -> (y : Nat) -> String -> Either String (WaitingArea x y)
parseWaitingArea x y str = MkWaitingArea <$> LS.parse pData str

-- updating

-- Helper function for adjacentCoordinates.
-- This function looks complicated to cover n = 1, because succ and pred are annoying then.
adjacentFin : Fin n -> List (Fin n)
adjacentFin {n = Z} _ impossible
adjacentFin {n = S Z} FZ = []
adjacentFin {n = S Z} (FS _) impossible
adjacentFin FZ = [ FZ, succ FZ ]
adjacentFin (FS x) with ((FS x) == Data.Fin.last)
  adjacentFin (FS x) | False = [ pred (FS x), FS x, succ (FS x) ]
  adjacentFin (FS x) | True = [ pred (FS x), FS x ]

adjacentCoordinates : Coordinate x y -> List (Coordinate x y)
adjacentCoordinates (MkCoordinate xCoord yCoord) =
  [ MkCoordinate x y | x <- adjacentFin xCoord, y <- adjacentFin yCoord, x /= xCoord || y /= yCoord ]

getSeat : WaitingArea x y -> Coordinate x y -> Seat
getSeat (MkWaitingArea seats) (MkCoordinate xCoord yCoord) =
  index xCoord $ index yCoord seats

newSeat : WaitingArea x y -> Coordinate x y -> Seat
newSeat waitingArea coord = case oldSeat of
  NoSeat => NoSeat
  EmptySeat => if 0 == length occupiedNeighbors
                  then OccupiedSeat
                  else EmptySeat
  OccupiedSeat => if 4 <= length occupiedNeighbors
                     then EmptySeat
                     else OccupiedSeat
where
  oldSeat = getSeat waitingArea coord
  occupiedNeighbors : List Seat
  occupiedNeighbors = filter (== OccupiedSeat) $ getSeat waitingArea <$> adjacentCoordinates coord

allFins : Vect n (Fin n)
allFins {n=n} with (n)
  allFins {n=n} | Z = []
  allFins {n=n} | (S k) = FZ :: map FS allFins

allCoordinates : Vect y (Vect x (Coordinate x y))
allCoordinates = row <$> allFins where
  row y = MkCoordinate <$> allFins <*> pure y

updateWaitingArea : WaitingArea x y -> WaitingArea x y
updateWaitingArea waitingArea = MkWaitingArea $ map (newSeat waitingArea) <$> allCoordinates

-- updating (part 2)

data Direction = N
               | NE
               | E
               | SE
               | S
               | SW
               | W
               | NW

nextCoordInDirection : Coordinate x y -> Direction -> Maybe (Coordinate x y)
nextCoordInDirection {x=xx} {y=yy} (MkCoordinate x y) N = do
  newY <- integerToFin (finToInteger y + 1) yy
  pure $ MkCoordinate x newY
nextCoordInDirection {x=xx} {y=yy} (MkCoordinate x y) NE = do
  newY <- integerToFin (finToInteger y + 1) yy
  newX <- integerToFin (finToInteger x + 1) xx
  pure $ MkCoordinate newX newY
nextCoordInDirection {x=xx} {y=yy} (MkCoordinate x y) E = do
  newX <- integerToFin (finToInteger x + 1) xx
  pure $ MkCoordinate newX y
nextCoordInDirection {x=xx} {y=yy} (MkCoordinate x y) SE = do
  newY <- integerToFin (finToInteger y - 1) yy
  newX <- integerToFin (finToInteger x + 1) xx
  pure $ MkCoordinate newX newY
nextCoordInDirection {x=xx} {y=yy} (MkCoordinate x y) S = do
  newY <- integerToFin (finToInteger y - 1) yy
  pure $ MkCoordinate x newY
nextCoordInDirection {x=xx} {y=yy} (MkCoordinate x y) SW = do
  newY <- integerToFin (finToInteger y - 1) yy
  newX <- integerToFin (finToInteger x - 1) xx
  pure $ MkCoordinate newX newY
nextCoordInDirection {x=xx} {y=yy} (MkCoordinate x y) W = do
  newX <- integerToFin (finToInteger x - 1) xx
  pure $ MkCoordinate newX y
nextCoordInDirection {x=xx} {y=yy} (MkCoordinate x y) NW = do
  newY <- integerToFin (finToInteger y + 1) yy
  newX <- integerToFin (finToInteger x - 1) xx
  pure $ MkCoordinate newX newY

getNextSeatInDirection : WaitingArea x y -> Coordinate x y -> Direction -> Maybe Seat
getNextSeatInDirection waitingArea coord dir =
  getSeat waitingArea <$> nextCoordInDirection coord dir

isNextSeatInDirectionOccupied : WaitingArea x y -> Coordinate x y -> Direction -> Bool
isNextSeatInDirectionOccupied waitingArea coord dir with (getNextSeatInDirection waitingArea coord dir)
  isNextSeatInDirectionOccupied waitingArea coord dir | Nothing = False
  isNextSeatInDirectionOccupied waitingArea coord dir | (Just NoSeat) with (nextCoordInDirection coord dir)
    isNextSeatInDirectionOccupied waitingArea coord dir | (Just NoSeat) | Nothing = False -- actually impossible
    isNextSeatInDirectionOccupied waitingArea coord dir | (Just NoSeat) | (Just nextCoord) =
      isNextSeatInDirectionOccupied waitingArea nextCoord dir
  isNextSeatInDirectionOccupied waitingArea coord dir | (Just EmptySeat) = False
  isNextSeatInDirectionOccupied waitingArea coord dir | (Just OccupiedSeat) = True

countNextOccupiedSeats : WaitingArea x y -> Coordinate x y -> Nat
countNextOccupiedSeats waitingArea coord =
  length $ filter id $ isNextSeatInDirectionOccupied waitingArea coord <$> [N, NE, E, SE, S, SW, W, NW]

newSeat2 : WaitingArea x y -> Coordinate x y -> Seat
newSeat2 waitingArea coord = case oldSeat of
  NoSeat => NoSeat
  EmptySeat => if 0 == occupiedNeighbors
                  then OccupiedSeat
                  else EmptySeat
  OccupiedSeat => if 5 <= occupiedNeighbors
                     then EmptySeat
                     else OccupiedSeat
where
  oldSeat = getSeat waitingArea coord
  occupiedNeighbors : Nat
  occupiedNeighbors = countNextOccupiedSeats waitingArea coord

updateWaitingArea2 : WaitingArea x y -> WaitingArea x y
updateWaitingArea2 waitingArea = MkWaitingArea $ map (newSeat2 waitingArea) <$> allCoordinates

-- counting

countOccupiedSeats : WaitingArea x y -> Nat
countOccupiedSeats (MkWaitingArea seats) =
  length $ elemIndices OccupiedSeat $ concat seats

-- main

upd : StateT (WaitingArea x y) IO ()
upd = do
  wa <- get
  lift $ print $ countOccupiedSeats wa
  lift $ putStr "\n"
  --let waNew = updateWaitingArea wa
  let waNew = updateWaitingArea2 wa
  put waNew
  upd

main : IO ()
main = do
  inputData' <- readFile "./data"
  case inputData' of
       Right inputData => case parseCountXY inputData of
                               Right (x,y) => case parseWaitingArea x y inputData of
                                                   Right w0 => do
                                                     runStateT upd w0
                                                     pure ()


text:
module SplayHeap

import Heap

%default total
%access private

export
data SplayHeap a = E | T (SplayHeap a) a (SplayHeap a)

partition : Ord a => a -> SplayHeap a -> (SplayHeap a, SplayHeap a)
partition pivot E = (E, E)
partition pivot t@(T a x b) =
  if x <= pivot then
    case b of
      E         => (t, E)
      T b1 y b2 =>
        if y <= pivot then
          let (small, big) = partition pivot $ assert_smaller t b2
          in (T (T a x b1) y small, big)
        else
          let (small, big) = partition pivot $ assert_smaller t b1
          in (T a x small, T big y b2)
  else
    case a of
      E         => (E, t)
      T a1 y a2 =>
        if y <= pivot then
          let (small, big) = partition pivot $ assert_smaller t a2
          in (T a1 y small, T big x b)
        else
          let (small, big) = partition pivot $ assert_smaller t a1
          in (small, T (T big y a2) x b)

export
Heap SplayHeap where
  empty = E
  isEmpty E = True
  isEmpty _ = False

  insert x t = let (a, b) = partition x t in T a x b

  merge E t = t
  merge (T a x b) t = let (ta, tb) = partition x t
    in T (assert_total $ merge ta a) x (assert_total $ merge tb b)

  findMin E = idris_crash "empty heap"
  findMin (T E x b) = x
  findMin (T a x b) = findMin a

  deleteMin E = idris_crash "empty heap"
  deleteMin (T E x b) = b
  deleteMin (T (T E x b) y c) = T b y c
  deleteMin (T (T a x b) y c) = T (deleteMin a) x (T b y c)


text:
module Idris.Codegen.ExtSTG.GHCPrimOp

import Idris.Codegen.ExtSTG.Prelude
import Idris.Codegen.ExtSTG.Representation

public export
data PrimOp : (name: String) -> (args : List PrimRep) -> (ret : PrimRep) -> Type where
  PlusInt      : PrimOp "+#"            [IntRep   , IntRep   ] IntRep
  PlusWord8    : PrimOp "plusWord8#"    [Word8Rep , Word8Rep ] Word8Rep
  PlusWord16   : PrimOp "plusWord16#"   [Word16Rep, Word16Rep] Word16Rep
  PlusWord     : PrimOp "plusWord3"     [WordRep  , WordRep  ] WordRep
  PlusDouble   : PrimOp "+##"           [DoubleRep, DoubleRep] DoubleRep
  SubInt       : PrimOp "-#"            [IntRep   , IntRep   ] IntRep
  SubWord8     : PrimOp "subWord8#"     [Word8Rep , Word8Rep ] Word8Rep
  SubWord16    : PrimOp "subWord16#"    [Word16Rep, Word16Rep] Word16Rep
  SubWord      : PrimOp "subWord#"      [WordRep  , WordRep  ] WordRep
  SubDouble    : PrimOp "-##"           [DoubleRep, DoubleRep] DoubleRep
  TimesInt     : PrimOp "*#"            [IntRep   , IntRep   ] IntRep
  TimesWord8   : PrimOp "timesWord8#"   [Word8Rep , Word8Rep ] Word8Rep
  TimesWord16  : PrimOp "timesWord16#"  [Word16Rep, Word16Rep] Word16Rep
  TimesWord    : PrimOp "timesWord#"    [WordRep  , WordRep  ] WordRep
  TimesDouble  : PrimOp "timesDouble#"  [DoubleRep, DoubleRep] DoubleRep
  QuotInt      : PrimOp "qoutInt#"      [IntRep   , IntRep   ] IntRep
  QuotWord8    : PrimOp "quotWord8#"    [Word8Rep , Word8Rep ] Word8Rep
  QuotWord16   : PrimOp "quotWord16#"   [Word16Rep, Word16Rep] Word16Rep
  QuotWord     : PrimOp "quotWord#"     [WordRep  , WordRep  ] WordRep
  QuotDouble   : PrimOp "/##"           [DoubleRep, DoubleRep] DoubleRep
  RemInt       : PrimOp "remInt#"       [IntRep   , IntRep   ] IntRep
  RemWord8     : PrimOp "remWord8#"     [Word8Rep , Word8Rep ] Word8Rep
  RemWord16    : PrimOp "remWord16#"    [Word16Rep, Word16Rep] Word16Rep
  RemWord      : PrimOp "remWord#"      [WordRep  , WordRep  ] WordRep
  AndInt       : PrimOp "andI#"         [IntRep   , IntRep   ] IntRep
  AndWord      : PrimOp "and#"          [WordRep  , WordRep  ] WordRep
  OrInt        : PrimOp "orI#"          [IntRep   , IntRep   ] IntRep
  OrWord       : PrimOp "or#"           [WordRep  , WordRep  ] WordRep
  XOrInt       : PrimOp "xorI#"         [IntRep   , IntRep   ] IntRep
  XOrWord      : PrimOp "xor#"          [WordRep  , WordRep  ] WordRep
  LTInt        : PrimOp "<#"            [IntRep   , IntRep   ] IntRep
  LTWord8      : PrimOp "ltWord8#"      [Word8Rep , Word8Rep ] IntRep
  LTWord16     : PrimOp "ltWord16#"     [Word16Rep, Word16Rep] IntRep
  LTWord       : PrimOp "ltWord#"       [WordRep  , WordRep  ] IntRep
  LTDouble     : PrimOp "<##"           [DoubleRep, DoubleRep] IntRep
  LTEInt       : PrimOp "<=#"           [IntRep   , IntRep   ] IntRep
  LTEWord8     : PrimOp "leWord8#"      [Word8Rep , Word8Rep ] IntRep
  LTEWord16    : PrimOp "leWord16#"     [Word16Rep, Word16Rep] IntRep
  LTEWord      : PrimOp "leWord#"       [WordRep  , WordRep  ] IntRep
  LTEDouble    : PrimOp "<=##"          [DoubleRep, DoubleRep] IntRep
  EQInt        : PrimOp "==#"           [IntRep   , IntRep   ] IntRep
  EQWord8      : PrimOp "eqWord8#"      [Word8Rep , Word8Rep ] IntRep
  EQWord16     : PrimOp "eqWord16#"     [Word16Rep, Word16Rep] IntRep
  EQWord       : PrimOp "eqWord"        [WordRep  , WordRep  ] IntRep
  EQDouble     : PrimOp "==##"          [DoubleRep, DoubleRep] IntRep
  GTEInt       : PrimOp ">=#"           [IntRep   , IntRep   ] IntRep
  GTEWord8     : PrimOp "geWord8#"      [Word8Rep , Word8Rep ] IntRep
  GTEWord16    : PrimOp "geWord16#"     [Word16Rep, Word16Rep] IntRep
  GTEWord      : PrimOp "geWord"        [WordRep  , WordRep  ] IntRep
  GTEDouble    : PrimOp ">=##"          [DoubleRep, DoubleRep] IntRep
  GTInt        : PrimOp ">#"            [IntRep   , IntRep   ] IntRep
  GTWord8      : PrimOp "gtWord8#"      [Word8Rep , Word8Rep ] IntRep
  GTWord16     : PrimOp "gtWord16#"     [Word16Rep, Word16Rep] IntRep
  GTWord       : PrimOp "gtWord"        [WordRep  , WordRep  ] IntRep
  GTDouble     : PrimOp ">##"           [DoubleRep, DoubleRep] IntRep
  NegateInt    : PrimOp "negateInt#"    [IntRep   ] IntRep
  NegateDouble : PrimOp "negateDouble#" [DoubleRep] DoubleRep
  ExpDouble    : PrimOp "expDouble"     [DoubleRep] DoubleRep
  LogDouble    : PrimOp "logDouble"     [DoubleRep] DoubleRep
  SinDouble    : PrimOp "sinDouble"     [DoubleRep] DoubleRep
  CosDouble    : PrimOp "cosDouble"     [DoubleRep] DoubleRep
  TanDouble    : PrimOp "tanDouble"     [DoubleRep] DoubleRep
  ASinDouble   : PrimOp "asinDouble"    [DoubleRep] DoubleRep
  ACosDouble   : PrimOp "acosDouble"    [DoubleRep] DoubleRep
  ATanDouble   : PrimOp "atanDouble"    [DoubleRep] DoubleRep
  SqrtDouble   : PrimOp "sqrtDouble"    [DoubleRep] DoubleRep
  IShiftLInt   : PrimOp "uncheckedIShiftL#"  [IntRep, IntRep] IntRep
  IShiftLRInt  : PrimOp "uncheckedIShiftRL#" [IntRep, IntRep] IntRep

  IndexWord8OffAddr : PrimOp "indexWord8OffAddr#" [AddrRep, IntRep] Word8Rep
  IndexWord8Array   : PrimOp "indexWord8Array#" [ByteArrayRep, IntRep] Word8Rep
  SizeOfByteArray   : PrimOp "sizeofByteArray#" [ByteArrayRep] IntRep
  ByteArrayContents : PrimOp "byteArrayContents#" [ByteArrayRep] AddrRep

  -- State ignoring PrimOps:
  -- Int# -> State# s -> (# State# s, MutableByteArray# s #)
  NewByteArray : PrimOp "newByteArray#" [IntRep] MutableByteArrayRep
  -- Addr# -> MutableByteArray# s -> Int# -> Int# -> State# s -> State# s
  CopyAddrToByteArray : PrimOp "copyAddrToByteArray#" [AddrRep, MutableByteArrayRep, IntRep, IntRep] VoidRep
  -- MutableByteArray# s -> State# s -> (# State# s, ByteArray# #)
  UnsafeFreezeByteArray : PrimOp "unsafeFreezeByteArray#" [MutableByteArrayRep] ByteArrayRep
  -- MutableByteArray# s -> Int# -> Word# -> State# s -> State# s
  WriteWord8Array : PrimOp "writeWord8Array#" [MutableByteArrayRep,IntRep,Word8Rep] VoidRep

namespace PrimOp

  export
  name : {n : String} -> PrimOp n args r -> String
  name {n} _ = n

  export
  args : {as : List PrimRep} -> PrimOp n as r -> List PrimRep
  args {as} _ = as

max_stars_repo_name: andorp/IdrisExtSTGCodegen

max_issues_repo_name: andorp/IdrisExtSTGCodegen

max_forks_repo_name: andorp/IdrisExtSTGCodegen


text:
module Main

import Data.Vect

%default total

data CoNat
    = Co Nat
    | Infinity

S : CoNat -> CoNat
S (Co n)   = Co (S n)
S Infinity = Infinity

Sn_notzero : Main.S n = Co 0 -> Void
Sn_notzero = believe_me

S_Co_not_Inf : Main.S (Co n) = Infinity -> Void
S_Co_not_Inf = believe_me

S_inj : (n : CoNat) -> (m : CoNat) -> Main.S n = Main.S m -> n = m
S_inj (Co n)   (Co _)   Refl = Refl
S_inj (Co n)   Infinity p    = void (S_Co_not_Inf p)
S_inj Infinity (Co m)   p    = void (S_Co_not_Inf (sym p))
S_inj Infinity Infinity Refl = Refl

swap : {n : Nat} -> Vect n a -> Vect n a
swap Nil            = Nil
swap (x :: Nil)     = x :: Nil
swap (x :: y :: xs) = (y :: x :: (swap xs))

main : IO ()
main = printLn (swap [1,2,3,4,5])

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 TTImp.Unelab

import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Env
import Core.Normalise
import Core.Options
import Core.Value
import Core.TT

import TTImp.TTImp
import TTImp.Utils

import Data.List
import Data.String

%default covering

used : (idx : Nat) -> Term vars -> Bool
used idx (Local _ _ var _) = idx == var
used {vars} idx (Bind _ x b sc) = usedBinder b || used (1 + idx) sc
  where
    usedBinder : Binder (Term vars) -> Bool
    usedBinder (Let _ _ val ty) = used idx val || used idx ty
    usedBinder b = used idx (binderType b)
used idx (Meta _ _ _ args) = any (used idx) args
used idx (App _ f a) = used idx f || used idx a
used idx (As _ _ _ pat) = used idx pat
used idx (TDelayed _ _ tm) = used idx tm
used idx (TDelay _ _ _ tm) = used idx tm
used idx (TForce _ _ tm) = used idx tm
used idx _ = False

data IArg
   = Exp FC IRawImp
   | Auto FC IRawImp
   | Named FC Name IRawImp

unIArg : IArg -> IRawImp
unIArg (Exp _ t) = t
unIArg (Auto _ t) = t
unIArg (Named _ _ t) = t

Show IArg where
  show (Exp fc t) = show t
  show (Auto fc t) = "@{" ++ show t ++ "}"
  show (Named fc n t) = "{" ++ show n ++ " = " ++ show t ++ "}"

getFnArgs : IRawImp -> List IArg -> (IRawImp, List IArg)
getFnArgs (IApp fc f arg) args = getFnArgs f (Exp fc arg :: args)
getFnArgs (INamedApp fc f n arg) args = getFnArgs f (Named fc n arg :: args)
getFnArgs (IAutoApp fc f arg) args = getFnArgs f (Auto fc arg :: args)
getFnArgs tm args = (tm, args)

data UnelabMode
     = Full
     | NoSugar Bool -- uniqify names
     | ImplicitHoles

Eq UnelabMode where
   Full == Full = True
   NoSugar t == NoSugar u = t == u
   ImplicitHoles == ImplicitHoles = True
   _ == _ = False

mutual
  unelabCase : {auto c : Ref Ctxt Defs} ->
               List (Name, Nat) ->
               Name -> List IArg -> IRawImp ->
               Core IRawImp
  unelabCase nest n args orig
      = do defs <- get Ctxt
           Just glob <- lookupCtxtExact n (gamma defs)
                | Nothing => pure orig
           let PMDef _ pargs treect _ pats = definition glob
                | _ => pure orig
           let Just argpos = findArgPos treect
                | _ => pure orig
           if length args == length pargs
              then mkCase pats argpos 0 args
              else pure orig
    where
      -- Need to find the position of the scrutinee to rebuild original
      -- case correctly
      findArgPos : CaseTree as -> Maybe Nat
      findArgPos (Case idx p _ _) = Just idx
      findArgPos _ = Nothing

      idxOrDefault : Nat -> a -> List a -> a
      idxOrDefault Z def (x :: xs) = x
      idxOrDefault (S k) def (_ :: xs) = idxOrDefault k def xs
      idxOrDefault _ def [] = def

      getNth : Nat -> Term vars -> Term vars
      getNth n tm
          = case getFnArgs tm of
                 (f, as) => idxOrDefault n f as

      nthArg : FC -> Nat -> Term vars -> Term vars
      nthArg fc drop (App afc f a) = getNth drop (App afc f a)
      nthArg fc drop tm = Erased fc False

      mkClause : FC -> Nat ->
                 (vs ** (Env Term vs, Term vs, Term vs)) ->
                 Core IImpClause
      mkClause fc dropped (vs ** (env, lhs, rhs))
          = do let pat = nthArg fc dropped lhs
               logTerm "unelab.case" 20 "Unelaborating LHS" pat
               lhs' <- unelabTy Full nest env pat
               logTerm "unelab.case" 20 "Unelaborating RHS" rhs
               logEnv "unelab.case" 20 "In Env" env
               rhs' <- unelabTy Full nest env rhs
               pure (PatClause fc (fst lhs') (fst rhs'))

      mkCase : List (vs ** (Env Term vs, Term vs, Term vs)) ->
               Nat -> Nat -> List IArg -> Core IRawImp
      mkCase pats (S k) dropped (_ :: args) = mkCase pats k (S dropped) args
      mkCase pats Z dropped (Exp fc tm :: _)
          = do pats' <- traverse (mkClause fc dropped) pats
               pure $ ICase fc tm (Implicit fc False) pats'
      mkCase _ _ _ _ = pure orig

  unelabSugar : {auto c : Ref Ctxt Defs} ->
                (umode : UnelabMode) ->
                (nest : List (Name, Nat)) ->
                (IRawImp, Glued vars) ->
                Core (IRawImp, Glued vars)
  unelabSugar (NoSugar _) nest res = pure res
  unelabSugar ImplicitHoles nest res = pure res
  unelabSugar _ nest (tm, ty)
      = let (f, args) = getFnArgs tm [] in
            case f of
             IVar fc (MkKindedName _ _ (NS ns (CaseBlock n i))) =>
               do log "unelab.case" 20 $ unlines
                         [ "Unelaborating case " ++ show (n, i)
                         , "with arguments: " ++ show args
                         ]
                  tm <- unelabCase nest (NS ns (CaseBlock n i)) args tm
                  log "unelab.case" 20 $ "Unelaborated to: " ++ show tm
                  pure (tm, ty)
             _ => pure (tm, ty)

  dropParams : {auto c : Ref Ctxt Defs} ->
               List (Name, Nat) -> (IRawImp, Glued vars) ->
               Core (IRawImp, Glued vars)
  dropParams nest (tm, ty)
     = case getFnArgs tm [] of
            (IVar fc n, args) =>
                case lookup (rawName n) nest of
                     Nothing => pure (tm, ty)
                     Just i => pure $ (apply (IVar fc n) (drop i args), ty)
            _ => pure (tm, ty)
    where
      apply : IRawImp -> List IArg -> IRawImp
      apply tm [] = tm
      apply tm (Exp fc a :: args) = apply (IApp fc tm a) args
      apply tm (Auto fc a :: args) = apply (IAutoApp fc tm a) args
      apply tm (Named fc n a :: args) = apply (INamedApp fc tm n a) args

  -- Turn a term back into an unannotated TTImp. Returns the type of the
  -- unelaborated term so that we can work out where to put the implicit
  -- applications
  -- NOTE: There is *no guarantee* that this will elaborate back successfully!
  -- It's only intended for display
  unelabTy : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             (umode : UnelabMode) ->
             (nest : List (Name, Nat)) ->
             Env Term vars -> Term vars ->
             Core (IRawImp, Glued vars)
  unelabTy umode nest env tm
      = unelabSugar umode nest !(dropParams nest !(unelabTy' umode nest env tm))

  unelabTy' : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              (umode : UnelabMode) ->
              (nest : List (Name, Nat)) ->
              Env Term vars -> Term vars ->
              Core (IRawImp, Glued vars)
  unelabTy' umode nest env (Local fc _ idx p)
      = do let nm = nameAt p
           log "unelab.case" 20 $ "Found local name: " ++ show nm
           let ty = gnf env (binderType (getBinder p env))
           pure (IVar fc (MkKindedName (Just Bound) nm nm), ty)
  unelabTy' umode nest env (Ref fc nt n)
      = do defs <- get Ctxt
           Just ty <- lookupTyExact n (gamma defs)
               | Nothing => case umode of
                                 ImplicitHoles => pure (Implicit fc True, gErased fc)
                                 _ => pure (IVar fc (MkKindedName (Just nt) n n), gErased fc)
           fn <- getFullName n
           n' <- case umode of
                      NoSugar _ => pure fn
                      _ => aliasName fn
           log "unelab.var" 50 $
             unwords [ "Found name:", show n
                     , " (aka " ++ show fn ++ ")"
                     , "sugared to", show n'
                     ]

           pure (IVar fc (MkKindedName (Just nt) fn n'), gnf env (embed ty))
  unelabTy' umode nest env (Meta fc n i args)
      = do defs <- get Ctxt
           let mkn = nameRoot n
           Just ty <- lookupTyExact (Resolved i) (gamma defs)
               | Nothing => case umode of
                                 ImplicitHoles => pure (Implicit fc True, gErased fc)
                                 _ => pure (IHole fc mkn, gErased fc)
           pure (IHole fc mkn, gnf env (embed ty))
  unelabTy' umode nest env (Bind fc x b sc)
      = do (sc', scty) <- unelabTy umode nest (b :: env) sc
           case umode of
                NoSugar True =>
                   let x' = uniqueLocal vars x in
                       unelabBinder umode nest fc env x' b
                                    (renameVars (CompatExt CompatPre) sc) sc'
                                    (renameVars (CompatExt CompatPre) !(getTerm scty))
                _ => unelabBinder umode nest fc env x b sc sc' !(getTerm scty)
    where
      next : Name -> Name
      next (MN n i) = MN n (i + 1)
      next (UN n) = MN (show n) 0
      next (NS ns n) = NS ns (next n)
      next n = MN (show n) 0

      uniqueLocal : List Name -> Name -> Name
      uniqueLocal vs n
         = if n `elem` vs
              then uniqueLocal vs (next n)
              else n
  unelabTy' umode nest env (App fc fn arg)
      = do (fn', gfnty) <- unelabTy umode nest env fn
           (arg', gargty) <- unelabTy umode nest env arg
           fnty <- getNF gfnty
           defs <- get Ctxt
           case fnty of
                NBind _ x (Pi _ rig Explicit ty) sc
                  => do sc' <- sc defs (toClosure defaultOpts env arg)
                        pure (IApp fc fn' arg',
                                glueBack defs env sc')
                NBind _ x (Pi _ rig p ty) sc
                  => do sc' <- sc defs (toClosure defaultOpts env arg)
                        pure (INamedApp fc fn' x arg',
                                glueBack defs env sc')
                _ => pure (IApp fc fn' arg', gErased fc)
  unelabTy' umode nest env (As fc s p tm)
      = do (p', _) <- unelabTy' umode nest env p
           (tm', ty) <- unelabTy' umode nest env tm
           case p' of
                IVar _ n =>
                    case umode of
                         NoSugar _ => pure (IAs fc (getLoc p) s n.rawName tm', ty)
                         _ => pure (tm', ty)
                _ => pure (tm', ty) -- Should never happen!
  unelabTy' umode nest env (TDelayed fc r tm)
      = do (tm', ty) <- unelabTy' umode nest env tm
           defs <- get Ctxt
           pure (IDelayed fc r tm', gErased fc)
  unelabTy' umode nest env (TDelay fc r _ tm)
      = do (tm', ty) <- unelabTy' umode nest env tm
           defs <- get Ctxt
           pure (IDelay fc tm', gErased fc)
  unelabTy' umode nest env (TForce fc r tm)
      = do (tm', ty) <- unelabTy' umode nest env tm
           defs <- get Ctxt
           pure (IForce fc tm', gErased fc)
  unelabTy' umode nest env (PrimVal fc c) = pure (IPrimVal fc c, gErased fc)
  unelabTy' umode nest env (Erased fc _) = pure (Implicit fc True, gErased fc)
  unelabTy' umode nest env (TType fc) = pure (IType fc, gType fc)
  unelabTy' umode nest _ tm
      = let fc = getLoc tm in
            pure (Implicit fc False, gErased fc)

  unelabPi : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             (umode : UnelabMode) ->
             (nest : List (Name, Nat)) ->
             Env Term vars -> PiInfo (Term vars) ->
             Core (PiInfo IRawImp)
  unelabPi umode nest env Explicit = pure Explicit
  unelabPi umode nest env Implicit = pure Implicit
  unelabPi umode nest env AutoImplicit = pure AutoImplicit
  unelabPi umode nest env (DefImplicit t)
      = do (t', _) <- unelabTy umode nest env t
           pure (DefImplicit t')

  unelabBinder : {vars : _} ->
                 {auto c : Ref Ctxt Defs} ->
                 (umode : UnelabMode) ->
                 (nest : List (Name, Nat)) ->
                 FC -> Env Term vars -> (x : Name) ->
                 Binder (Term vars) -> Term (x :: vars) ->
                 IRawImp -> Term (x :: vars) ->
                 Core (IRawImp, Glued vars)
  unelabBinder umode nest fc env x (Lam fc' rig p ty) sctm sc scty
      = do (ty', _) <- unelabTy umode nest env ty
           p' <- unelabPi umode nest env p
           pure (ILam fc rig p' (Just x) ty' sc,
                    gnf env (Bind fc x (Pi fc' rig p ty) scty))
  unelabBinder umode nest fc env x (Let fc' rig val ty) sctm sc scty
      = do (val', vty) <- unelabTy umode nest env val
           (ty', _) <- unelabTy umode nest env ty
           pure (ILet fc EmptyFC rig x ty' val' sc,
                    gnf env (Bind fc x (Let fc' rig val ty) scty))
  unelabBinder umode nest fc env x (Pi _ rig p ty) sctm sc scty
      = do (ty', _) <- unelabTy umode nest env ty
           p' <- unelabPi umode nest env p
           let nm = if used 0 sctm || isNoSugar umode
                       then Just x
                       else if rig /= top || isDefImp p
                               then Just (UN Underscore)
                               else Nothing
           pure (IPi fc rig p' nm ty' sc, gType fc)
    where
      isNoSugar : UnelabMode -> Bool
      isNoSugar (NoSugar _) = True
      isNoSugar _ = False
      isDefImp : PiInfo t -> Bool
      isDefImp (DefImplicit _) = True
      isDefImp _ = False
  unelabBinder umode nest fc env x (PVar fc' rig _ ty) sctm sc scty
      = do (ty', _) <- unelabTy umode nest env ty
           pure (sc, gnf env (Bind fc x (PVTy fc' rig ty) scty))
  unelabBinder umode nest fc env x (PLet fc' rig val ty) sctm sc scty
      = do (val', vty) <- unelabTy umode nest env val
           (ty', _) <- unelabTy umode nest env ty
           pure (ILet fc EmptyFC rig x ty' val' sc,
                    gnf env (Bind fc x (PLet fc' rig val ty) scty))
  unelabBinder umode nest fc env x (PVTy _ rig ty) sctm sc scty
      = do (ty', _) <- unelabTy umode nest env ty
           pure (sc, gType fc)

export
unelabNoSugar : {vars : _} ->
                {auto c : Ref Ctxt Defs} ->
                Env Term vars -> Term vars -> Core IRawImp
unelabNoSugar env tm
    = do tm' <- unelabTy (NoSugar False) [] env tm
         pure $ fst tm'

export
unelabUniqueBinders : {vars : _} ->
                {auto c : Ref Ctxt Defs} ->
                Env Term vars -> Term vars -> Core IRawImp
unelabUniqueBinders env tm
    = do tm' <- unelabTy (NoSugar True) [] env tm
         pure $ fst tm'

export
unelabNoPatvars : {vars : _} ->
                  {auto c : Ref Ctxt Defs} ->
                  Env Term vars -> Term vars -> Core IRawImp
unelabNoPatvars env tm
    = do tm' <- unelabTy ImplicitHoles [] env tm
         pure $ fst tm'

export
unelabNest : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             List (Name, Nat) ->
             Env Term vars ->
             Term vars -> Core IRawImp
unelabNest nest env (Meta fc n i args)
    = do let mkn = nameRoot n ++ showScope args
         pure (IHole fc mkn)
  where
    toName : Term vars -> Maybe Name
    toName (Local _ _ idx p) = Just (nameAt p)
    toName _ = Nothing

    showNScope : List Name -> String
    showNScope [] = "[no locals in scope]"
    showNScope ns = "[locals in scope: " ++ showSep ", " (map show (nub ns)) ++ "]"

    showScope : List (Term vars) -> String
    showScope ts = " " ++ showNScope (mapMaybe toName ts)

unelabNest nest env tm
    = do tm' <- unelabTy Full nest env tm
         pure $ fst tm'

export
unelab : {vars : _} ->
         {auto c : Ref Ctxt Defs} ->
         Env Term vars ->
         Term vars -> Core IRawImp
unelab = unelabNest []


text:
module Int2Str

export
int2str : Int -> String
int2str = cast

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
module BankersQueue

import Queue
import OStream

%default total
%access private

export
data BankersQueue a = BQ Int (OStream a) Int (OStream a)

check : Int -> OStream a -> Int -> OStream a -> BankersQueue a
check lenf f lenr r =
  if lenr <= lenf then BQ lenf f lenr r
  else BQ (lenf+lenr) (OStream.append f (OStream.reverse r)) 0 []

export
Queue BankersQueue where
  empty = BQ 0 [] 0 []
  isEmpty (BQ lenf f lenr r) = lenf == 0

  snoc (BQ lenf f lenr r) x = check lenf f (lenr + 1) (x :: r)

  head (BQ lenf []        lenr r) = idris_crash "empty queue"
  head (BQ lenf (x :: f') lenr r) = x

  tail (BQ lenf []        lenr r) = idris_crash "empty queue"
  tail (BQ lenf (x :: f') lenr r) = check (lenf - 1) f' lenr r