text:
module Network

import Streaming
import Streaming.Bytes as BS

import System.File
import Network.Socket

import Control.Monad.Trans

import Control.Monad.Either
import Control.Monad.Managed

import Data.LazyList as LL
import Util -- Either instances

-------------------------------------------------
-- Streaming Network Example
--
-- NB This file is a work in progress, I just wanted to get it put out before I
-- forget to. Exercises task is subject to change.
--
-- NB This example has not been tested to make sure it's running in constant
-- space.
{- Let's read the text from example.com! We're going to do some parsing here to
   find the text we're after but in real life you'd use a proper parsing lib.
   That could be a good next project, streaming to a parsing lib.
   This example is a little more involved to make use of some extra tooling to
   be expanded on later.
   In a real program you'd want to enforce that connecting has been done before
   sending or receiving, consider Control.Linear.Network for your own tests.

   I expect network primitives to eventually provide Bits8 rather than Char as
   they do now, in the mean time we cast to Bits8. This is currently correct to
   do as these are really a 'c char' which is 8 bits.
-}
-------------------------------------------------

%foreign "C:strerror,libc,string.h"
strerror : Int -> String
-- No reason to PrimIO, right? It's just a lookup.

||| A sum Error type for this example, for making EitherT use direct.
data Error = SocketError Int
           | ConnectError Int
           | SendError Int
           | RecvError Int
           | FileError FileError

showError : Error -> String
showError (SocketError err) = "Socket error: " ++ strerror err
showError (ConnectError err) = "Connect error: " ++ strerror err
showError (SendError err) = "Send error: " ++ strerror err
showError (RecvError err) = "Recv error: " ++ strerror err
showError (FileError err) = "File error: " ++ show err

-- While this is really Maybe Error, writing it as Either Error () plays nicer
-- with the EitherT setup used here.
streamnet : (Monad m, HasIO m) => Socket -> Stream (Of Bits8) m (Either Error ())
streamnet sock = Effect $ do
  let chunkLen = 1024
  Right (res,len) <- recv sock chunkLen
    | Left err => pure $ Return (Left (RecvError err))
  pure $ if len == 0
    then Return (Right ())
    else each (map (cast . cast {to=Int}) . LL.unpack $ res) *>
           if len < chunkLen
              then Return (Right ())
              else streamnet sock

withFile : HasIO io => String -> Mode
        -> (Either Error File -> io b) -> io b
withFile file mode act = do
  f <- first FileError <$> openFile file mode
  res <- act f
  traverse closeFile f
  pure res

withSocket : HasIO io => SocketFamily -> SocketType -> ProtocolNumber
          -> (Either Error Socket -> io b) -> io b
withSocket fam ty proto act = do
  sock <- first SocketError <$> socket fam ty proto
  res <- act sock
  traverse close sock
  pure res

main : IO ()
main = runManaged $ do
    let filename = "out.txt"
        addr = Hostname "www.example.com"
        msg = makeHeader ["GET / HTTP/1.0"
                         ,"Host: www.example.com"
                         ,"User-Agent: idris2-test"]
    res <- runEitherT $ do
      file <- MkEitherT . use . managed $ withFile "out.txt" WriteTruncate
      sock <- MkEitherT . use . managed $ withSocket AF_INET Stream 0
      0 <- lift $ connect sock addr 80
        | err => throwE (ConnectError err)
      lift $ first SendError <$> send sock msg
      lift $ streamnet sock
          &$ maps charCast
          |> S.stdoutChrLn'
      pure () -- helps type inferrence
    either (putStrLn . showError) pure res
  where
    makeHeader : List String -> String
    makeHeader xs = concatMap (++ "\r\n") xs ++ "\r\n"


text:
-- Matrix.idr
--
-- Matrix arithmetics with dependent types

module Matrix

import Data.Vect

||| A type alias for nested Vect
||| @ n number of rows
||| @ m number of columns
Matrix : (n : Nat) -> (m : Nat) -> Type -> Type
Matrix n m elem = Vect n (Vect m elem)

testMatrix : Matrix 2 3 Int
testMatrix = [[0, 0, 0], [0, 0, 0]]

-- matrix addition
addMatrix : Num numType =>
            Vect rows (Vect cols numType) ->
            Vect rows (Vect cols numType) ->
            Vect rows (Vect cols numType)

-- matrix multiplication
multMatrix : Num numType =>
             Vect n (Vect m numType) ->
             Vect m (Vect p numType) ->
             Vect n (Vect p numType)

-- transpose matrix
createEmpties : Vect n (Vect 0 elem)
createEmpties = replicate _ []

transposeHelper : (x : Vect n elem) -> (xsTrans : Vect n (Vect len elem)) ->
                  Vect n (Vect (S len) elem)
transposeHelper [] [] = []
transposeHelper (x :: xs) (y :: ys) = (x :: y) :: transposeHelper xs ys

transposeMat : Vect m (Vect n elem) -> Vect n (Vect m elem)
transposeMat [] = createEmpties
transposeMat (x :: xs) = let xsTrans = transposeMat xs in
                             transposeHelper x xsTrans

ext: idr

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
%default total

tailRecId : (a -> Either a b) -> a -> b
tailRecId f a = case f a of
  Left a2 => tailRecId f a2
  Right b => b

iamvoid : Void
iamvoid = tailRecId go ()
  where go : () -> Either () Void
        go () = Left ()


text:
module AppendInjective

%access export
%default total

appendInjectiveRight : (a, b, c : List x) -> a ++ b = a ++ c -> b = c
appendInjectiveRight []      _ _ = id
appendInjectiveRight (y::ys) b c = appendInjectiveRight ys b c . snd . consInjective

lemma_bad_nat : (a, b : Nat) -> S a + b = b -> Void
lemma_bad_nat a Z     = rewrite plusZeroRightNeutral a in SIsNotZ
lemma_bad_nat a (S k) = rewrite sym $ plusSuccRightSucc a k in
                        lemma_bad_nat a k . succInjective (S (a + k)) k

lemma_bad_append : (x : a) -> (xs, ys : List a) -> (x::xs) ++ ys = ys -> Void
lemma_bad_append x xs ys = lemma_bad_nat (length xs) (length ys) . rewrite sym $ lengthAppend xs ys in cong {f=length}

appendInjectiveLeft : (a, b, c : List x) -> a ++ c = b ++ c -> a = b
appendInjectiveLeft [] [] _ _ = Refl
appendInjectiveLeft (y::ys) (z::zs) c prf with (consInjective prf)
  | (p1, p2) = rewrite p1 in cong $ appendInjectiveLeft ys zs c p2
appendInjectiveLeft [] (z::zs) c prf = absurd $ lemma_bad_append z zs c $ sym prf
appendInjectiveLeft (y::ys) [] c prf = absurd $ lemma_bad_append y ys c prf

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Main

import GrinFFI

fn : Int -> Int
fn x = if x > 0
  then x + fn (x - 1)
  else 0

lazy_fn : Int -> Lazy Int
lazy_fn x = if x > 0
  then (x + Force (lazy_fn (x - 1)))
  else 0

{-
test_int_op : Int -> Int -> Int -> Int
test_int_op op 0 y = y
test_int_op op x y = case op of
  0 => x + y
  1 => x - y
  2 => x * y
--  3 => div x y -- It needs support for SError
  _ => y

test_int_comp : Int -> Int -> Int -> Bool
test_int_comp 0 _ _  = False
test_int_comp op x y = case op of
  1 => x < y
  2 => x <= y
  3 => x == y
  4 => x >= y
  5 => x > y
  _ => True
-}

main : IO ()
main = do
  int_print (fn (fn 10))
--  int_print (test_int_op 0 10 10)
--  bool_print (test_int_comp 0 10 10)
  int_print $ Force $ lazy_fn (Force (lazy_fn 10))
  pure ()

max_stars_repo_name: pdani/idris-grin

max_issues_repo_name: pdani/idris-grin

max_forks_repo_name: pdani/idris-grin


text:
module Minecraft.Core.Tangible.Export

import public Minecraft.Core.Tangible

%default total

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
-- ---------------------------------------------------------------- [ Dict.idr ]
-- Module    : Dict.idr
-- Copyright : (c) 2015,2016 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| A Dictionary based upon an AVL Key-Value AVL.API.
module Data.AVL.API.Dict

import Data.AVL

%default total
%access export

data Dict : (k : Type) -> Type -> Type where
  MkDict : AVLTree h k v -> Dict k v

||| Empty
empty : (Ord k) => Dict k v
empty = MkDict (Element Empty AVLEmpty)

insert : (Ord k) => k -> v -> Dict k v -> Dict k v
insert key val (MkDict d) = MkDict $ snd (AVL.API.insert key val d)

||| Update the value for the given key.
update : (Ord k) => k -> (v -> v) -> Dict k v -> Dict k v
update x ufunc (MkDict d) = MkDict $ AVL.API.update x ufunc d

-- -------------------------------------------------------------------- [ List ]

toList : Dict k v -> List (k,v)
toList (MkDict d) = AVL.API.toList d

fromList : Ord k => List (k,v) -> Dict k v
fromList kvs = MkDict $ snd $ AVL.API.fromList kvs

-- ----------------------------------------------------------------- [ Queries ]

isEmpty : Dict k v -> Bool
isEmpty (MkDict d) = AVL.API.isEmpty d

foldr : (k -> v -> p -> p) -> p -> Dict k v -> p
foldr f init (MkDict d) = AVL.API.foldr f init d

lookup : (Ord k) => k -> Dict k v -> Maybe v
lookup k (MkDict d) = AVL.API.lookup k d

keys : Dict k v -> List k
keys (MkDict d) = AVL.API.keys d

values : Dict k v -> List v
values (MkDict d) = AVL.API.values d

size : Dict k v -> Nat
size (MkDict d) = AVL.API.size d

hasKey : (Ord k) => k -> Dict k v -> Bool
hasKey key (MkDict d) = AVL.API.hasKey key d

hasValue : (Eq v) => v -> Dict k v -> Bool
hasValue val (MkDict d) = AVL.API.hasValue val d

hasValueUsing : (v -> Bool) -> Dict k v -> Bool
hasValueUsing f (MkDict d) = AVL.API.any (\k,v => (f v)) d

findKey : (pred : v -> Bool) -> Dict k v -> Maybe k
findKey pred (MkDict d) = AVL.API.findKey pred d

findKeyOf : (Eq v) => v -> Dict k v -> Maybe k
findKeyOf v (MkDict d) = AVL.API.findKeyOf v d

-- --------------------------------------------------------- [ Implementations ]

(Eq k, Eq v) => Eq (Dict k v) where
   (==) (MkDict {h = h} x) (MkDict {h = h'} y) with (decEq h h')
     (==) (MkDict {h = h} x) (MkDict {h = h} y)  | Yes Refl = x == y
     (==) (MkDict {h = h} x) (MkDict {h = h'} y) | No _     = False

(Show k, Show v) => Show (Dict k v) where
  show (MkDict d) = show d

Ord a => Functor (Dict a) where
  map func x = fromList $ (\(a, b) => (a, func b)) <$> toList x

Ord a => Foldable (Dict a) where
  foldr func = foldr $ const func

Ord a => Traversable (Dict a) where
  traverse f x = fromList <$> (traverse (\(a, b) => (MkPair a) <$> f b) $ Data.AVL.API.Dict.toList x)

namespace Predicates

  export
  data HasKey : (key  : typeKey)
             -> (dict : Dict typeKey typeValue)
             -> Type
    where
      IsKey : (prf : HasKey key tree)
           -> HasKey key (MkDict tree)

  private
  keyNotInDict : (contra : HasKey key tree -> Void)
              -> HasKey key (MkDict tree)
              -> Void
  keyNotInDict contra (IsKey x) = contra x

  isKey : DecEq typeKey
       => (key  : typeKey)
       -> (dict : Dict typeKey typeValue)
       -> Dec (HasKey key dict)
  isKey key (MkDict tree) with (isKey key tree)
    isKey key (MkDict tree) | (Yes x) = Yes (IsKey x)
    isKey key (MkDict tree) | (No contra) = No (keyNotInDict contra)

  export
  data HasValue : (value : typeValue)
               -> (dict  : Dict typeKey typeValue)
               -> Type
    where
      IsValue : (prf : HasValue value tree)
             -> HasValue value (MkDict tree)

  private
  valueNotInDict : (contra : HasValue value tree -> Void)
                -> HasValue value (MkDict tree)
                -> Void
  valueNotInDict contra (IsValue prf) = contra prf

  isValue : DecEq typeValue
         => (value : typeValue)
         -> (dict  : Dict typeKey typeValue)
         -> Dec (HasValue value dict)
  isValue value (MkDict tree) with (isValue value tree)
    isValue value (MkDict tree) | (Yes x) = Yes (IsValue x)
    isValue value (MkDict tree) | (No contra) = No (valueNotInDict contra)

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

max_stars_repo_name: elba/idris-containers

max_issues_repo_name: elba/idris-containers

max_forks_repo_name: elba/idris-containers


text:
module Program

import CommonTestingStuff

export
beforeString : String
beforeString = "before coop"

long : PrintString m => CanSleep m => Zippable m => (offset : Time) -> m String
long offset = do
  printTime offset "long proc, first"
  for 5 $ do
    printTime offset "long proc, before 1000"
    sleepFor 1.seconds
    printTime offset "long proc, before 2000"
    sleepFor 2.seconds
  printTime offset "long proc, last"
  pure "long"

infinite : CanSleep m => m a
infinite = forever $ sleepFor 1.millis

export
program : PrintString m => CanSleep m => Zippable m => Alternative m => m Unit
program = do
  offset <- currentTime
  printTime offset "start"

  res <- long offset <|> infinite
  printTime offset "top: \{res}"

  sleepFor 1.seconds
  printTime offset "------"

  res <- infinite <|> long offset
  printTime offset "top: \{res}"

  printTime offset "end"


text:
module ExactLength

%default total

data Vect : Nat -> Type -> Type where
  Nil : Vect Z a
  (::) : a -> Vect k a -> Vect (S k) a

{-
exactLength :  { m : _ } -> (len : Nat) -> Vect m a -> Maybe (Vect len a)
exactLength len input = case m == len of
                             False => Nothing
                             True => Just input
-}

-- build-up: equality of Nats (EqNat.idr)

data EqNat : Nat -> Nat -> Type where
  Same : (num : Nat) -> EqNat num num

sameS : (eq : EqNat k j) -> EqNat (S k) (S j)
sameS (Same l) = Same (S l)

checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (EqNat num1 num2)
checkEqNat Z Z = Just (Same Z)
checkEqNat Z _  = Nothing
checkEqNat _ Z = Nothing
checkEqNat (S k) (S l) = case checkEqNat k l of
                              Nothing => Nothing
                              Just eq => Just (sameS eq)

exactLength : { m : Nat } -> (len : Nat) -> Vect m a -> Maybe (Vect len a)
exactLength len input = case checkEqNat m len of
                             Nothing => Nothing
                             Just (Same len) => Just input

-- implementation of checkEqNat using the generic equality type

{-
  data (=) : a -> b -> Type where
    Refl : x = x

  Synonym: Equal
-}

checkEqNat' : (num1 : Nat) -> (num2 : Nat) -> Maybe (num1 = num2)
checkEqNat' Z Z = Just Refl
checkEqNat' Z _  = Nothing
checkEqNat' _ Z = Nothing
checkEqNat' (S k) (S l) = case checkEqNat' k l of
                               Nothing => Nothing
                               Just eq => Just (cong S eq)

exactLength' :  { m : Nat } -> (len : Nat) -> Vect m a -> Maybe (Vect len a)
exactLength' len input = case checkEqNat' m len of
                              Nothing => Nothing
                              Just Refl => Just input

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


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.SortedSet as SortedSet
import Data.String.Extra
import Data.StringMap
import Data.Strings
import Idris.Driver
import Printer
import System
import System.File
import Utils.Hex

data Dart : Type where

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

Statement : Type
Statement = ImperativeStatement

Expression : Type
Expression = ImperativeExp

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 (dartIdent lib)
      put Dart (record { imports $= insert lib alias } s)
      pure alias
    Just alias =>
      pure alias

include : {auto ctx : Ref Dart DartT} -> String -> Core ()
include code = do
  s <- get Dart
  put Dart (record { includes $= insert code } s)

keywordSafe : String -> String
keywordSafe s = case s of
  "var" => "var_"
  _ => 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 <+> "*/"

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 <+> "})()"

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"

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"

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

---- 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 : Doc -> FunctionType -> Doc
makeCallback c (args, ret) =
  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 n (uncurriedSignature a b))
  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

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)

parseForeignTypeName : {auto ctx : Ref Dart DartT}
  -> String -> Core Doc
parseForeignTypeName 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 =
  put Dart (record { foreignTypeNames $= insert ty doc } !(get Dart))

foreignTypeName : {auto ctx : Ref Dart DartT}
  -> String -> Core Doc
foreignTypeName ty = do
  case !(lookupForeignType ty) of
    Just doc => pure doc
    Nothing => do
      doc <- parseForeignTypeName 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"

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() ?? \"\";"))
  _ => case mapMaybe foreignDartSpecFrom ss of
    [s] => dartForeign n s args ret
    _ => pure (dartName n <+> "([a, b, c, d, e, f, g, h, i, j, k])" <+> block (unsupportedError ss))

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 arity
  -> Vect arity 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 (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)

useDelay : {auto ctx : Ref Dart DartT} -> Core ()
useDelay = do
  s <- get Dart
  put Dart (record { usesDelay = True } s)

mutual
  dartLambda : {auto ctx : Ref Dart DartT} -> List Name -> Statement -> Core Doc
  dartLambda ps s = pure (paramList ps <+> block !(dartStatement s))

  dartConstructor : {auto ctx : Ref Dart DartT}
    -> Doc
    -> List Expression
    -> Core Doc
  dartConstructor tag args = case args of
    [] => pure (text "const [" <+> tag <+> "]")
    args => do
      args' <- traverse dartExp args
      pure ("[" <+> tag <+> ", " <+> commaSep 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 (IEVar (NS ns (UN "believe_me"))) [_, _, arg] =>
      dartExp arg
    IEApp f args => do
      f' <- dartExp f
      args' <- traverse dartExp args
      pure (f' <+> tupled 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)

  dartPrimFnExt : {auto ctx : Ref Dart DartT}
    -> Name -> List Expression -> Core Doc
  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__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__dart_new"))
    [ IENull, IENull, IENull, IENull -- erased type arguments
      , IEConstructor (Right "System.FFI.Struct") (IEConstant (Str ty) :: _)
      , positional
      , named
      , rest
    ] = do
      let pos' = collectPositional positional
      let named' = collectNamed named
      fTy <- foreignTypeName ty
      posArgs <- traverse dartExp pos'
      namedArgs <- traverse dartNamedParam named'
      pure (fTy <+> tupled (posArgs ++ namedArgs))
  dartPrimFnExt
    (NS _ (UN "prim__dart_list_new"))
    [ IEConstructor (Right "System.FFI.Struct") (IEConstant (Str ty) :: _)
    , _
    ] = do
      fTy <- foreignTypeName ty
      pure (text "$.List<" <+> fTy <+> text ">()")
  dartPrimFnExt (NS _ (UN "prim__dart_true")) _ =
    pure (text "true")
  dartPrimFnExt (NS _ (UN "prim__dart_false")) _ =
    pure (text "false")
  dartPrimFnExt (NS _ (UN "prim__dart_if")) [ IENull, condition, thenValue, elseValue ] =
    pure (!(dartExp condition) <+> " ? " <+> !(dartExp thenValue) <+> " : " <+> !(dartExp elseValue))
  dartPrimFnExt (NS _ (UN "prim__dart_eq")) [ IENull, x, y ] =
    pure (!(dartExp x) <+> " == " <+> !(dartExp y))
  dartPrimFnExt n args = pure (debug (n, args))

  dartNamedParam : {auto ctx : Ref Dart DartT} -> (Expression, String, Expression) -> Core Doc
  dartNamedParam (ty, name, value) = do
    let fTy = parseFunctionType ty
    value' <- dartExp value
    pure (text name <+> ": " <+> maybe value' (makeCallback value') fTy)

  ||| 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

  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

  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 <+> 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

compileToDart : Ref Ctxt Defs -> ClosedTerm -> Core Doc
compileToDart defs term = do
  (impDefs, impMain) <- compileToImperative defs term
  ctx <- newRef Dart (MkDartT (fromList [("dart:core", "$")]) empty empty False)
  dartDefs <- dartStatement impDefs
  dartMain <- dartStatement impMain
  finalState <- get Dart
  let includeLines = concatMap 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 = "void main()" <+> block dartMain
  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 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
  coreLift (system ("dart" ++ " " ++ tempDartFile))
  pure ()

dartCodegen : Codegen
dartCodegen = MkCG compile execute

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


text:
module Compiler.Jvm.Tree

import Data.List
import Data.String

public export
data Tree a = Node a (List (Tree a))

export
displayTree : (a -> String) -> Tree a -> String
displayTree show tree = unlines . reverse $ go [] [] 0 tree where
    indent : Nat -> String
    indent level = concat $ replicate level "  "

    showNodeData : Nat -> a -> String
    showNodeData level d = indent level ++ show d

    go : List String -> List (Nat, Tree a) -> Nat -> Tree a -> List String
    go acc [] level (Node d []) = showNodeData level d :: acc
    go acc ((treeLevel, tree) :: nextTree) nodeLevel (Node d []) =
      go (showNodeData nodeLevel d :: acc) nextTree treeLevel tree
    go acc stack level (Node d (child :: children)) =
      let childrenWithLevel = ((\c => (level + 1, c)) <$> children)
      in go (showNodeData level d :: acc) (childrenWithLevel ++ stack) (level + 1) child

implementation Show a => Show (Tree a) where
  show tree = displayTree show tree

export
traverseDepthFirst : Tree a -> List a
traverseDepthFirst tree = go [] [] tree where
  go : (acc: List a) -> (stack: List (Tree a)) -> Tree a -> List a
  go acc [] (Node d []) = d :: acc
  go acc (next :: rest) (Node d []) = go (d :: acc) rest next
  go acc stack (Node d (child :: children)) = go acc (child :: stack) (Node d children)


text:
module Control.Monad.Writer.Interface

import Control.Monad.Maybe
import Control.Monad.Error.Either
import Control.Monad.Reader.Reader
import Control.Monad.State.State
import Control.Monad.RWS.CPS
import Control.Monad.Trans
import Control.Monad.Writer.CPS

%default total

||| MonadWriter interface
|||
||| tell is like tell on the MUD's it shouts to monad
||| what you want to be heard. The monad carries this 'packet'
||| upwards, merging it if needed (hence the Monoid requirement).
|||
||| listen listens to a monad acting, and returns what the monad "said".
|||
||| pass lets you provide a writer transformer which changes internals of
||| the written object.
public export
interface (Monoid w, Monad m) => MonadWriter w m | m where
  ||| `writer (a,w)` embeds a simple writer action.
  writer : (a,w) -> m a
  writer (a, w) = tell w $> a

  ||| `tell w` is an action that produces the output `w`.
  tell : w -> m ()
  tell w = writer ((),w)

  ||| `listen m` is an action that executes the action `m` and adds
  ||| its output to the value of the computation.
  listen : m a -> m (a, w)

  ||| `pass m` is an action that executes the action `m`, which
  ||| returns a value and a function, and returns the value, applying
  ||| the function to the output.
  pass : m (a, w -> w) -> m a

||| `listens f m` is an action that executes the action `m` and adds
||| the result of applying @f@ to the output to the value of the computation.
public export
listens : MonadWriter w m => (w -> b) -> m a -> m (a, b)
listens f = map (\(a,w) => (a,f w)) . listen

||| `censor f m` is an action that executes the action `m` and
||| applies the function `f` to its output, leaving the return value
||| unchanged.
public export
censor : MonadWriter w m => (w -> w) -> m a -> m a
censor f = pass . map (\a => (a,f))

--------------------------------------------------------------------------------
--          Implementations
--------------------------------------------------------------------------------

public export %inline
(Monoid w, Monad m) => MonadWriter w (WriterT w m) where
  writer   = writerT . pure

  listen m = MkWriterT $ \w =>
               (\(a,w') => ((a,w'),w <+> w')) <$> runWriterT m

  tell w'  = writer ((), w')

  pass m   = MkWriterT $ \w =>
               (\((a,f),w') => (a,w <+> f w')) <$> runWriterT m

public export %inline
(Monoid w, Monad m) => MonadWriter w (RWST r w s m) where
  writer (a,w') = MkRWST $ \_,s,w => pure (a,s,w <+> w')

  tell w' = writer ((), w')

  listen m = MkRWST $ \r,s,w =>
               (\(a,s',w') => ((a,w'),s',w <+> w')) <$> runRWST m r s

  pass m = MkRWST $ \r,s,w =>
             (\((a,f),s',w') => (a,s',w <+> f w')) <$> runRWST m r s

public export %inline
MonadWriter w m => MonadWriter w (EitherT e m) where
  writer = lift . writer
  tell   = lift . tell
  listen = mapEitherT $ \m => do (e,w) <- listen m
                                 pure $ map (\a => (a,w)) e

  pass   = mapEitherT $ \m => pass $ do Right (r,f) <- m
                                          | Left l => pure $ (Left l, id)
                                        pure (Right r, f)

public export %inline
MonadWriter w m => MonadWriter w (MaybeT m) where
  writer = lift . writer
  tell   = lift . tell
  listen = mapMaybeT $ \m => do (e,w) <- listen m
                                pure $ map (\a => (a,w)) e

  pass   = mapMaybeT $ \m => pass $ do Just (r,f) <- m
                                         | Nothing => pure $ (Nothing, id)
                                       pure (Just r, f)
public export %inline
MonadWriter w m => MonadWriter w (ReaderT r m) where
  writer = lift . writer
  tell   = lift . tell
  listen = mapReaderT listen
  pass   = mapReaderT pass

public export %inline
MonadWriter w m => MonadWriter w (StateT s m) where
  writer = lift . writer
  tell   = lift . tell
  listen (ST m) = ST $ \s => do ((s',a),w) <- listen (m s)
                                pure (s',(a,w))

  pass   (ST m) = ST $ \s => pass $ do (s',(a,f)) <- m s
                                       pure ((s',a),f)


text:
module Data.LeftistHeap

import Decidable.Order

%default total

mutual
  export
  data Heap : .(constraint : Ordered a rel) -> .(count : Nat) -> Type where
       Empty : Heap _ Z
       Node : (n : Nat)
           -> (value : a)
           -> {countLeft : Nat}
           -> (left : Heap constraint countLeft)
           -> {countRight : Nat}
           -> (right : Heap constraint countRight)
           -> .{auto fitsLeft : Fits value left}
           -> .{auto fitsRight : Fits value right}
           -> .{auto leftistPrf : LTE (rank right) (rank left)}
           -> .{auto rankPrf : n = S $ rank right}
           -> Heap constraint (S $ countLeft + countRight)

  Fits : {constraint : Ordered a rel} -> a -> Heap constraint cnt -> Type
  Fits {cnt = Z} _ _ = ()
  Fits {cnt = S _} x h = rel x (findMin h)

  rank : Heap _ _ -> Nat
  rank Empty = Z
  rank (Node _ _ _ right) = S $ rank right

  export
  findMin : .{constraint : Ordered a _} -> Heap constraint (S _) -> a
  findMin (Node _ value _ _) = value

export
empty : Heap _ Z
empty = Empty

makeFit : .{constraint : Ordered a rel}
       -> .(fitsValue : a)
       -> (value : a)
       -> {count1 : Nat}
       -> {count2 : Nat}
       -> (h1 : Heap constraint count1)
       -> (h2 : Heap constraint count2)
       -> .{auto fits1 : Fits value h1}
       -> .{auto fits2 : Fits value h2}
       -> .{auto relPrf : rel fitsValue value}
       -> Subset (Heap constraint (S $ count1 + count2)) (Fits fitsValue)
makeFit {count1} {count2} {relPrf} fitsValue value h1 h2 with (order {to = LTE} (rank h1) (rank h2))
  | (Left _) = rewrite plusCommutative count1 count2 in
               Element (Node _ value h2 h1) relPrf
  | (Right _) = Element (Node _ value h1 h2) relPrf

covering
mergeHelper : .{constraint : Ordered a rel}
           -> .{value : a}
           -> {count1 : Nat}
           -> {count2 : Nat}
           -> (h1 : Heap constraint count1)
           -> (h2 : Heap constraint count2)
           -> .{auto fits1 : Fits value h1}
           -> .{auto fits2 : Fits value h2}
           -> Subset (Heap constraint (count1 + count2)) (Fits value)
mergeHelper Empty Empty = Element Empty ()
mergeHelper {fits1} h@(Node {countLeft} {countRight} n _ _ _) Empty = rewrite plusZeroRightNeutral (countLeft + countRight) in Element h fits1
mergeHelper {fits2} Empty h@(Node {countLeft} {countRight} n _ _ _) = Element h fits2
mergeHelper {value} {rel}
            (Node {countLeft = countLeft1} {countRight = countRight1} _ value1 left1 right1)
            (Node {countLeft = countLeft2} {countRight = countRight2} _ value2 left2 right2)
  = case order {to = rel} value1 value2 of
    Left orderPrf => rewrite sym $ plusAssociative countLeft1 countRight1 (S $ countLeft2 + countRight2) in
                     let (Element mergedHeap fitsMergedHeap) = mergeHelper {value = value1} right1 (Node _ value2 left2 right2) in
                     makeFit value value1 left1 mergedHeap
    Right orderPrf => rewrite sym $ plusSuccRightSucc (countLeft1 + countRight1) (countLeft2 + countRight2) in
                      rewrite plusCommutative countLeft2 countRight2 in
                      rewrite plusAssociative (countLeft1 + countRight1) countRight2 countLeft2 in
                      let (Element mergedHeap fitsMergedHeap) = mergeHelper {value = value2} (Node _ value1 left1 right1) right2 in
                      makeFit value value2 mergedHeap left2

export
merge : .{constraint : Ordered a rel}
     -> {count1 : Nat} -> {count2 : Nat}
     -> (h1 : Heap constraint count1) -> (h2 : Heap constraint count2)
     -> Heap constraint (count1 + count2)
merge Empty Empty = Empty
merge {count1} h Empty = rewrite plusZeroRightNeutral count1 in h
merge Empty h = h
merge h1@(Node _ _ _ _) h2@(Node _ _ _ _)
  = assert_total $ case order {to = rel} (findMin h1) (findMin h2) of
    Left orderPrf => case mergeHelper {value = (findMin h1)} h1 h2 {fits1 = reflexive (findMin h1)} of
                     Element h _ => h
    Right orderPrf => case mergeHelper {value = (findMin h2)} h1 h2 {fits2 = reflexive (findMin h2)} of
                      Element h _ => h

export
insert : .{constraint : Ordered a _} -> .{n : Nat} -> a -> Heap constraint n -> Heap constraint (S n)
insert value heap = merge (Node 1 value Empty Empty) heap

export
deleteMin : .{constraint : Ordered a _} -> {n : Nat} -> Heap constraint (S n) -> Heap constraint n
deleteMin (Node _ _ left right) = merge left right

namespace OrderedLeftistHeap
  export
  data CountedHeap : .(constraint : Ordered a rel) -> Type where
       MkCountedHeap : (n : Nat) -> (Heap constraint n) -> CountedHeap constraint

  export
  empty : CountedHeap _
  empty = MkCountedHeap Z empty

  export
  count : CountedHeap _ -> Nat
  count (MkCountedHeap n _) = n

  export
  findMin : .{constraint : Ordered ty _} -> CountedHeap constraint -> Maybe ty
  findMin (MkCountedHeap Z _) = Nothing
  findMin (MkCountedHeap (S _) h) = Just $ findMin h

  export
  merge : .{constraint : Ordered _ _} -> CountedHeap constraint -> CountedHeap constraint -> CountedHeap constraint
  merge (MkCountedHeap count1 h1) (MkCountedHeap count2 h2) = MkCountedHeap (count1 + count2) (merge h1 h2)

  export
  insert : .{constraint : Ordered ty _} -> ty -> CountedHeap constraint -> CountedHeap constraint
  insert a (MkCountedHeap n h) = MkCountedHeap (S n) (insert a h)

  export
  deleteMin : .{constraint : Ordered ty _} -> CountedHeap constraint -> CountedHeap constraint
  deleteMin orig@(MkCountedHeap Z h) = orig
  deleteMin (MkCountedHeap (S n) h) = MkCountedHeap n (deleteMin h)

max_stars_repo_name: jdevuyst/idris-data

max_issues_repo_name: jdevuyst/idris-data

max_forks_repo_name: jdevuyst/idris-data


text:
-- --------------------------------------------------------------- [ Extra.idr ]
-- Module      : String.Extra
-- Description : A port of Elm's string-extra package to Idris.
-- Copyright   : string-extra Copyright (c) 2016, Elm Community
--               String.Extra Copyright (c) 2016, Eric Bailey
-- License     : BSD-3
-- Link        : https://github.com/elm-community/string-extra
-- --------------------------------------------------------------------- [ EOH ]
||| String helper functions for Idris, inspired by Elm's string-extra.
module String.Extra

import Prelude.Strings

%access export

-- --------------------------------------------------------------- [ Splitting ]

private
dropLeft : Nat -> String -> String
dropLeft n = pack . drop n . unpack

private
breaker : Nat -> String -> List String -> List String
breaker width "" acc     = reverse acc
breaker width string acc = breaker width
                                   (dropLeft width string)
                                   (substr 0 width string :: acc)

||| Break a string into a list of strings of at most `width` characters.
|||
||| ```idris example
||| break 10 "The quick brown fox"
||| ```
||| ```idris example
||| break 2 ""
||| ```
|||
||| @ width the maximum length of the resulting strings
break : (width : Nat) -> String -> List String
break Z string     = [string]
break _ ""         = [""]
break width string = breaker width string []

||| Break a string into a list of strings of at most `width` characters, without
||| chopping words.
|||
||| ```idris example
||| softBreak 6 "The quick brown fox"
||| ```
|||
||| @ width the maximum length of the resulting strings
softBreak : (width : Nat) -> String -> List String
softBreak Z _          = []
softBreak width string = go Nothing [] string
  where
  go : Maybe String -> List String -> String -> List String
  go (Just ps) acc ""  = reverse (ps :: acc)
  go Nothing acc ""    = reverse acc
  go Nothing acc str   =
      let (w1, r1) = break isSpace str
          (s1, r2) = span isSpace r1
          str2 = w1 ++ s1 in
          if length str2 >= width
             then go Nothing (str2 :: acc) r2
             else go (Just str2) acc r2
  go (Just ps) acc str =
      let (w1, r1) = break isSpace str
          (s1, r2) = span isSpace r1
          str2 = w1 ++ s1 in
          if length str2 >= width
             then go Nothing (str2 :: ps :: acc) r2
             else let str3 = ps ++ str2 in
                      if length str3 >= width
                         then go (Just str2) (ps :: acc) r2
                         else go (Just str3) acc r2

-- -------------------------------------------------------------- [ Formatting ]

||| Trim the whitespace of both sides of the string and compress repeated
||| whitespace internally to a single character.
|||
||| ```idris example
||| clean " The   quick brown   fox    "
||| ```
clean : String -> String
clean = trim . go
  where
    go : String -> String
    go str with (strM str)
      go ""             | StrNil      = ""
      go (strCons c cs) | StrCons _ _ =
          strCons c $ assert_total $ go $ if isSpace c then ltrim cs else cs

||| Remove surrounding strings from another string.
|||
||| ```idris example
||| unsurround "foo" "foobarfoo"
||| ```
unsurround : String -> String -> String
unsurround wrap string =
  if isPrefixOf wrap string && isPrefixOf wrap string
     then let n = length wrap in
              pack (reverse (drop n (reverse (drop n (unpack string)))))
     else string

||| Remove quotes that surround a string.
|||
||| ```idris example
||| unquote "\"foo\""
||| ```
||| ```idris example
||| unquote "\"foo\"bar\""
||| ```
unquote : String -> String
unquote = unsurround "\""

||| docstring
|||
||| ```idris example
||| unindent "  Hello\n    World"
||| ```
||| ```idris example
||| unindent "\t\tHello\n\t\t\t\tWorld"
||| ```
unindent : String -> String
unindent s = let lines = lines' (unpack s) in
                 pack (unlines' (map (drop (minLead lines)) lines))
  where
    countIndent : Nat -> List Char -> Nat
    countIndent n []           = n
    countIndent n (' ' :: xs)  = countIndent (S n) xs
    countIndent n ('\t' :: xs) = countIndent (S n) xs
    countIndent n (_ :: xs)    = n

    isNotIndent : Char -> Bool
    isNotIndent c = ' ' /= c && '\t' /= c

    minimum : Ord a => List a -> Maybe a
    minimum [] = Nothing
    minimum (x :: xs) = Just $ foldr min x xs

    minLead : List (List Char) -> Nat
    minLead = fromMaybe 0 . minimum .
              map (countIndent 0) .
              filter (any isNotIndent)

||| Given a string longer than `howLong`, truncate it and append the `append`
||| string such that the resulting string is exactly `howLong` in length.
||| Return the string if its length is less than or equal to `howLong`.
|||
||| ```idris example
||| ellipsisWith 5 " .." "Hello World"
||| ```idris example
||| ellipsisWith 10 " .."  "Hello World"
||| ```idris example
||| ellipsisWith 10 " .." "Hello"
||| ```
||| ```idris example
||| ellipsisWith 8 " .." "Hello World"
||| ```
|||
||| @ howLong maximum length of the resulting string
||| @ append string to append to truncated strings, e.g. `"..."`
||| @ smaller proof that `(length append)` is less than or equal to `howLong`
ellipsisWith : (howLong : Nat) -> (append : String) -> String ->
               {auto smaller : LTE (length append) howLong} ->
               String
ellipsisWith howLong append string =
  if length string <= howLong
     then string
     else substr 0 (howLong - (length append)) string ++ append

||| Given a string longer than `howLong`, truncate it and append three dots such
||| that the resulting string is exactly `howLong` in length.
||| Return the string if its length is less than or equal to `howLong`.
|||
||| ```idris example
||| ellipsis 5 "Hello World"
||| ```
||| ```idris example
||| ellipsis 10 "Hello World"
||| ```
||| ```idris example
||| ellipsis 10 "Hello"
||| ```
||| ```idris example
||| ellipsis 8 "Hello World"
||| ```
|||
||| @ howLong maximum length of the resulting string
||| @ smaller proof that 3 is less than or equal to `howLong`
ellipsis : (howLong : Nat) -> String ->
           {auto smaller : LTE 3 howLong} ->
           String
ellipsis howLong = ellipsisWith howLong "..."

||| Truncate a string and append three dots, such that the resulting string is
||| at most `howLong + 3` in length. Return the string if its length is less
||| than or equal to `howLong`.
|||
||| Unlike `ellipsis`, do *not* produce unfinished words, instead, collect as
||| many complete words as meet the length constraint.
|||
||| Additionally, remove any trailing whitespace and punctuation at the end of
||| truncated string.
|||
||| ```idris example
||| softEllipsis 5 "Hello, World"
||| ```
||| ```idris example
||| softEllipsis 8 "Hello, World"
||| ```
||| ```idris example
||| softEllipsis 15 "Hello, cruel world"
||| ```
||| ```idris example
||| softEllipsis 10 "Hello"
||| ```
|||
||| @ howLong maximum length of the resulting string
softEllipsis : (howLong : Nat) -> String -> String
softEllipsis howLong string =
    if length string <= howLong
       then string
       else fromMaybe "" $
            (flip (++) "...") . dropTrailing <$>
            head' (softBreak howLong string)
  where
    p : Char -> Bool
    p c = isSpace c || '.' == c || ',' == c || ';' == c || ':' == c
    dropTrailing : String -> String
    dropTrailing = reverse . snd . span p . reverse

-- TODO: Consider implementing stripTags.
{-
||| Remove all HTML tags from a string, preserving the text inside them.
|||
||| ```idris example
||| stripTags "a <a href=\"#\">link</a>" == "a link"
||| ```
||| ```idris example
||| stripTags "<script>alert('hello world!')</script> == "alert('hello world!')"
||| ```
stripTags : String -> String
-}

||| Given a singular string, a plural string, and number, return the number
||| followed by a space, followed by either the singular string if the number
||| was 1, or the plural string otherwise.
|||
||| ```idris example
||| pluralize "elf" "elves" 2
||| ```
||| ```idris example
||| pluralize "elf" "elves" 1
||| ```
||| ```idris example
||| pluralize "elf" "elves" 0
||| ```
pluralize : String -> String -> Nat -> String
pluralize singular plural count =
  if count == 1
     then "1 " ++ singular
     else (show count) ++ " " ++ plural

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

max_stars_repo_name: yurrriq/idris-string

max_issues_repo_name: yurrriq/idris-string

max_forks_repo_name: yurrriq/idris-string


text:
module Solutions.Functions2

import Data.List

%default total

--------------------------------------------------------------------------------
--          Let Bindings and Where Blocks
--------------------------------------------------------------------------------

-- 1
record Artist where
  constructor MkArtist
  name : String

record Album where
  constructor MkAlbum
  name   : String
  artist : Artist

record Email where
  constructor MkEmail
  value : String

record Password where
  constructor MkPassword
  value : String

record User where
  constructor MkUser
  name     : String
  email    : Email
  password : Password
  albums   : List Album

Eq Artist where (==) = (==) `on` name

Eq Email where (==) = (==) `on` value

Eq Password where (==) = (==) `on` value

Eq Album where (==) = (==) `on` \a => (a.name, a.artist)

record Credentials where
  constructor MkCredentials
  email    : Email
  password : Password

record Request where
  constructor MkRequest
  credentials : Credentials
  album       : Album

data Response : Type where
  UnknownUser     : Email -> Response
  InvalidPassword : Response
  AccessDenied    : Email -> Album -> Response
  Success         : Album -> Response

DB : Type
DB = List User

handleRequest : DB -> Request -> Response
handleRequest xs (MkRequest (MkCredentials e pw) album) =
  case find ((e ==) . email) xs of
    Nothing => UnknownUser e
    Just (MkUser _ _ pw' albums)  =>
      if      pw' /= pw         then InvalidPassword
      else if elem album albums then Success album
      else                           AccessDenied e album

-- 2
data Nucleobase = Adenine | Cytosine | Guanine | Thymine

readBase : Char -> Maybe Nucleobase
readBase 'A' = Just Adenine
readBase 'C' = Just Cytosine
readBase 'G' = Just Guanine
readBase 'T' = Just Thymine
readBase c   = Nothing

-- 3
traverseList : (a -> Maybe b) -> List a -> Maybe (List b)
traverseList _ []        = Just []
traverseList f (x :: xs) =
  case f x of
    Just y  => case traverseList f xs of
      Just ys => Just (y :: ys)
      Nothing => Nothing
    Nothing => Nothing

-- 4
DNA : Type
DNA = List Nucleobase

readDNA : String -> Maybe DNA
readDNA = traverseList readBase . unpack

-- 5
complement : DNA -> DNA
complement = map comp
  where comp : Nucleobase -> Nucleobase
        comp Adenine  = Thymine
        comp Cytosine = Guanine
        comp Guanine  = Cytosine
        comp Thymine  = Adenine


text:
module IdrisJvm.JvmImport

import System
import public IdrisJvm.IO

%dynamic "libc", "msvcrt"

%access public export

data InvType = JStatic JVM_NativeTy
             | JInstance
             | JConstructor
             | JStaticField JVM_NativeTy
             | JInstanceField
             | JStaticFieldSetter JVM_NativeTy
             | JInstanceFieldSetter

-- Type for Elaborator Reflection to generate JVM FFI calls
data EType = EBool
           | EChar
           | EBits8
           | EBits16
           | EBits32
           | EBits64
           | EFloat
           | EDouble
           | EInt
           | EThrowablePrimitive EType

           | EString
           | ENullableString
           | EThrowableString
           | EThrowableNullableString

           | EVoid

           | EArray EType
           | ENullableArray EType
           | EThrowableNullableArray EType

           | EClass String
           | ENullableClass String
           | EThrowableClass String
           | EThrowableNullableClass String

           | EInterface String
           | ENullableInterface String
           | EThrowableNullableInterface String

Eq EType where
  EBool == EBool = True
  EChar == EChar = True
  EBits8 == EBits8 = True
  EBits16 == EBits16 = True
  EBits32 == EBits32 = True
  EBits64 == EBits64 = True
  EFloat == EFloat = True
  EDouble == EDouble = True
  EInt == EInt = True
  (EThrowablePrimitive e1) == (EThrowablePrimitive e2) = e1 == e2

  EString == EString = True
  ENullableString == ENullableString = True
  EThrowableString == EThrowableString = True
  EThrowableNullableString == EThrowableNullableString = True

  EVoid == EVoid = True

  (EArray e1) == (EArray e2) = e1 == e2
  (ENullableArray e1) == (ENullableArray e2) = e1 == e2
  (EThrowableNullableArray e1) == (EThrowableNullableArray e2) = e1 == e2

  (EClass c1) == (EClass c2) = c1 == c2
  (ENullableClass c1) == (ENullableClass c2) = c1 == c2
  (EThrowableClass c1) == (EThrowableClass c2) = c1 == c2
  (EThrowableNullableClass c1) == (EThrowableNullableClass c2) = c1 == c2

  (EInterface i1) == (EInterface i2) = i1 == i2
  (ENullableInterface i1) == (ENullableInterface i2) = i1 == i2
  (EThrowableNullableInterface i1) == (EThrowableNullableInterface i2) = i1 == i2

  _ == _ = False

data JvmFfiDesc = MethodDesc InvType EType String (List EType)
                | ConstructorDesc EType (List EType)

data JSafety = JSafe -- both exception and null safe

             -- Just exception safe, useful for constructors and primitives as those can never return or be `null`.
             | JThrowableSafe

             -- Just null safe, useful for field getters as they cannot throw exceptions
             | JNullableSafe

             | JUnsafe

JvmFfiDescs : Type
JvmFfiDescs = List JvmFfiDesc

createArray : Nat -> EType -> EType
createArray Z ty = ty
createArray (S k) ty = EArray $ createArray k ty

createNullableArray : Nat -> EType -> EType
createNullableArray Z ty = ty
createNullableArray (S k) ty = ENullableArray $ createArray k ty

parseEType : String -> Either String EType
parseEType jtypeStr with (words jtypeStr)
  | ["int"] = pure EInt
  | ["char"] = pure EChar
  | ["byte"] = pure EBits8
  | ["short"] = pure EBits16
  | ["long"] = pure EBits64
  | ["float"] = pure EFloat
  | ["double"] = pure EDouble
  | ["boolean"] = pure EBool
  | ["void"] = pure EVoid

  -- This and some of the following ones are used to parse the types explicitly given by the user.
  -- We don't want the user to have to differentiate between a class and interface so here everything is realized as a
  -- class but later on refined correctly for a class or interface based on type provider information
  | ["?Array", dim, className] = createNullableArray (cast dim) <$> parseEType ("c " ++ className)

  | ("Array" :: dim :: "c" :: className :: []) = createArray (cast dim) <$> parseEType ("c " ++ className)
  | ("Array" :: dim :: "i" :: className :: []) = createArray (cast dim) <$> parseEType ("i " ++ className)
  | ("Array" :: dim :: ty :: []) = createArray (cast dim) <$> parseEType ty

  | ["c", "java/lang/String"] = pure EString
  | ["java/lang/String"] = pure EString
  | ["?java/lang/String"] = pure ENullableString

  | ["c", className] = pure $ EClass className
  | [className] = pure $ if strHead className == '?' then ENullableClass (strTail className) else EClass className

  | ["i", className] = pure $ EInterface className
  | _ = Left $ "Unable to parse Java type: " ++ jtypeStr

parseArgs : List String -> Either String (List EType)
parseArgs args = sequence $ parseEType <$> args

{-
 - Type providers can only run in IO, not in JVM_IO so JVM is launched as an external process setting up correct classpath that
 - includes the classes we want to import into Idris. The JVM program outputs the types of all the methods for the passed classes.
 - This function parses the output and constructs JvmFfiDesc which is then used by a function running in Idris elaborator to generate
 - appropriate FFI call site.
-}
public export
jvmImport : String -> List (String, List String) -> IO (Provider JvmFfiDescs)
jvmImport cmd importList = do
    let args =  unlines $ uncurry createCommandParam <$> importList
    writeFile ".idrisjvmtypesimport" args
    system cmd
    Right str <- readFile ".idrisjvmtypes"
        | Left err => pure (Error $ show err)
    let errOrffiDescs = sequence $ parseJvmOutput <$> (filter (/= "") $ lines str)
    pure $ either Error Provide errOrffiDescs
  where

    quoted : String -> String
    quoted s = "\"" ++ s ++ "\""

    createCommandParam : String -> List String -> String
    createCommandParam clazz clazzItems = clazz ++ " " ++ (unwords clazzItems)

    parseInvType : String -> Either String InvType
    parseInvType invStr with (words invStr)
      | ["s", "c", className] = pure $ JStatic (FFI.Class className)
      | ["s", "i", className] = pure $ JStatic (FFI.Interface className)
      | ["i"] = pure JInstance
      | ["sfg", "c", className] = pure $ JStaticField (FFI.Class className)
      | ["sfs", "c", className] = pure $ JStaticFieldSetter (FFI.Class className)
      | ["ifg"] = pure JInstanceField
      | ["ifs"] = pure JInstanceFieldSetter
      | _ = Left $ "Unable to parse invocation type: " ++ invStr

    parseJvmOutput : String -> Either String JvmFfiDesc
    parseJvmOutput desc = case filter (/= "") $ Strings.split (== ',') desc of
      "c" :: returns :: args => do
        jtype <- parseEType returns
        args <- parseArgs args
        pure $ ConstructorDesc jtype args
      invTypeStr :: retStr :: mname :: args => do
        invType <- parseInvType invTypeStr
        jtype <- parseEType retStr
        args <- parseArgs args
        pure $ MethodDesc invType jtype mname args
      _ => Left $ "Unable to parse JVM type provider output: " ++ desc

public export
jdkImport : List (String, List String) -> IO (Provider JvmFfiDescs)
jdkImport importList = do
  idrisJvmHomeMaybe <- getEnv "IDRIS_JVM_HOME"
  homeMaybe <- getEnv "HOME"
  let Just idrisJvmHome = idrisJvmHomeMaybe <|> homeMaybe
  let typeProviderClass = "io.github.mmhelloworld.idrisjvm.runtime.ffi.TypeProvider"
  let cmd = "java -cp " ++ idrisJvmHome ++ "/idris-jvm-runtime.jar " ++ typeProviderClass
  jvmImport cmd importList

jvmFfiNamespace : List String
jvmFfiNamespace = ["FFI", "IdrisJvm"]

appMaybeRaw : Raw -> Raw
appMaybeRaw ty = RApp (Var (NS (UN "Maybe") ["Maybe", "Prelude"])) ty

appThrowableRaw : Raw -> Raw
appThrowableRaw = RApp (RApp
                            (Var (NS (UN "Either") ["Either", "Prelude"]))
                            (Var (NS (UN "Throwable") jvmFfiNamespace)))

appThrowableNullableRaw : Raw -> Raw
appThrowableNullableRaw = appThrowableRaw . appMaybeRaw

jcallStaticTTName : TTName
jcallStaticTTName = NS (UN "jcallStatic") jvmFfiNamespace

jcallInstanceTTName : TTName
jcallInstanceTTName = NS (UN "jcallInstance") jvmFfiNamespace

jcallNewTTName : TTName
jcallNewTTName = NS (UN "jcallNew") jvmFfiNamespace

jcallGetStaticFieldTTName : TTName
jcallGetStaticFieldTTName = NS (UN "jcallGetStaticField") jvmFfiNamespace

jcallGetInstanceFieldTTName : TTName
jcallGetInstanceFieldTTName = NS (UN "jcallGetInstanceField") jvmFfiNamespace

jcallSetStaticFieldTTName : TTName
jcallSetStaticFieldTTName = NS (UN "jcallSetStaticField") jvmFfiNamespace

jcallSetInstanceFieldTTName : TTName
jcallSetInstanceFieldTTName = NS (UN "jcallSetInstanceField") jvmFfiNamespace

boolTyElab : Raw
boolTyElab = Var (NS (UN "Bool") ["Bool", "Prelude"])

charTyElab : Raw
charTyElab = RConstant (AType (ATInt ITChar))

bits8TyElab : Raw
bits8TyElab = RConstant (AType (ATInt (ITFixed IT8)))

bits16TyElab : Raw
bits16TyElab = RConstant (AType (ATInt (ITFixed IT16)))

bits32TyElab : Raw
bits32TyElab = RConstant (AType (ATInt (ITFixed IT32)))

bits64TyElab : Raw
bits64TyElab = RConstant (AType (ATInt (ITFixed IT64)))

intTyElab : Raw
intTyElab = RConstant (AType (ATInt ITNative))

stringTyElab : Raw
stringTyElab = RConstant StrType

floatTyElab : Raw
floatTyElab = Var (NS (UN "Float") ["FFI", "IdrisJvm"])

doubleTyElab: Raw
doubleTyElab = RConstant (AType ATDouble)

voidTyElab: Raw
voidTyElab = Var (UN "Unit")

jvmNativeElab : Raw
jvmNativeElab = Var (NS (UN "JVM_Native") jvmFfiNamespace)

ffiJvmElab : Raw
ffiJvmElab = Var (NS (UN "FFI_JVM") jvmFfiNamespace)

classRaw : Raw
classRaw = Var (NS (UN "Class") jvmFfiNamespace)

interfaceElab : Raw
interfaceElab = Var (NS (UN "Interface") jvmFfiNamespace)

classNameElab : String -> Raw
classNameElab className = RConstant (Str className)

jvmIOElab : Raw
jvmIOElab = Var (NS (UN "JVM_IO") jvmFfiNamespace)

nilRaw : Raw
nilRaw = RApp (Var (NS (UN "Nil") ["List", "Prelude"])) RType

jtypeElab : EType -> Raw
jtypeElab EBool = boolTyElab
jtypeElab EBits8 = bits8TyElab
jtypeElab EBits16 = bits16TyElab
jtypeElab EBits32 = bits32TyElab
jtypeElab EBits64 = bits64TyElab
jtypeElab EChar = charTyElab
jtypeElab EInt = intTyElab
jtypeElab EFloat = floatTyElab
jtypeElab EDouble = doubleTyElab
jtypeElab (EThrowablePrimitive primitive) = appThrowableRaw $ jtypeElab primitive

jtypeElab EString = stringTyElab
jtypeElab ENullableString = appMaybeRaw $ jtypeElab EString
jtypeElab EThrowableString = appThrowableRaw $ jtypeElab EString
jtypeElab EThrowableNullableString = appThrowableNullableRaw $ jtypeElab EString

jtypeElab (EArray ety) = RApp (Var (NS (UN "JVM_Array") ["FFI", "IdrisJvm"])) (jtypeElab ety)
jtypeElab (ENullableArray ety) = appMaybeRaw $ jtypeElab (EArray ety)
jtypeElab (EThrowableNullableArray ety) = appThrowableNullableRaw $ jtypeElab (EArray ety)

jtypeElab EVoid = voidTyElab

jtypeElab (EClass className) = RApp jvmNativeElab (RApp classRaw (classNameElab className))
jtypeElab (ENullableClass className) = appMaybeRaw $ jtypeElab (EClass className)
jtypeElab (EThrowableClass className) = appThrowableRaw $ jtypeElab (EClass className)
jtypeElab (EThrowableNullableClass className) = appThrowableNullableRaw $ jtypeElab (EClass className)

jtypeElab (EInterface className) = RApp jvmNativeElab (RApp interfaceElab (classNameElab className))
jtypeElab (ENullableInterface className) = appMaybeRaw $ jtypeElab (EInterface className)
jtypeElab (EThrowableNullableInterface className) = appThrowableNullableRaw $ jtypeElab (EInterface className)

jvmIORaw : EType -> Raw
jvmIORaw ty = RApp jvmIOElab (jtypeElab ty)

createSafeType : JSafety -> EType -> EType
createSafeType JThrowableSafe EString = EThrowableString
createSafeType JNullableSafe EString = ENullableString
createSafeType _ EString = EThrowableNullableString

createSafeType JThrowableSafe (EClass name) = EThrowableClass name
createSafeType JNullableSafe (EClass name) = ENullableClass name
createSafeType _ (EClass name) = EThrowableNullableClass name

createSafeType JNullableSafe (EInterface name) = ENullableInterface name
createSafeType _ (EInterface name) = EThrowableNullableInterface name

createSafeType JNullableSafe (EArray ty) = ENullableArray ty
createSafeType _ (EArray ty) = EThrowableNullableArray ty

createSafeType JNullableSafe primitive = primitive
createSafeType _ primitive = EThrowablePrimitive primitive

jvmFunctionTyElab : JSafety -> List EType -> EType -> Elab Raw
jvmFunctionTyElab JUnsafe [] ret = pure $ jvmIORaw ret
jvmFunctionTyElab safety [] ret = pure $ jvmIORaw $ createSafeType safety ret
jvmFunctionTyElab safety (arg :: args) ret = do
  argName <- gensym "arg"
  let argTyElab = jtypeElab arg
  rest <- jvmFunctionTyElab safety args ret
  pure $ RBind argName (Pi argTyElab RType) rest

nativeTyClassName : JVM_NativeTy -> String
nativeTyClassName (Class cname) = cname
nativeTyClassName (Interface cname) = cname

searchFty : Raw -> Elab ()
searchFty f = do
  [fty] <- apply f [True]
  solve
  focus fty
  search

gen : JSafety -> JvmFfiDesc -> Elab ()
gen safety (MethodDesc (JStatic ty) ret fname args) = do
    functionTy <- jvmFunctionTyElab safety args ret
    let cls = RApp classRaw (classNameElab $ nativeTyClassName ty)
    let appInvokeStatic = RApp (Var jcallStaticTTName) cls
    let appFunctionName = RApp appInvokeStatic $ RConstant (Str fname)
    let f = RApp appFunctionName functionTy
    searchFty f

gen safety (MethodDesc JInstance ret fname args) = do
    functionTy <- jvmFunctionTyElab safety args ret
    let appFunctionName = RApp (Var jcallInstanceTTName) $ RConstant (Str fname)
    let f = RApp appFunctionName functionTy
    searchFty f

gen JSafe desc@(ConstructorDesc _ _) = gen JThrowableSafe desc

gen safety (ConstructorDesc ret args) = do
    functionTy <- jvmFunctionTyElab safety args ret
    let f = RApp (Var jcallNewTTName) functionTy
    searchFty f

gen safety (MethodDesc (JStaticField ty) ret fname _) = do
    functionTy <- jvmFunctionTyElab safety [] ret
    let cls = RApp classRaw (classNameElab $ nativeTyClassName ty)
    let appGetStaticField = RApp (Var jcallGetStaticFieldTTName) cls
    let appFunctionName = RApp appGetStaticField $ RConstant (Str fname)
    let f = RApp appFunctionName functionTy
    searchFty f

gen safety (MethodDesc JInstanceField ret fname args) = do
    functionTy <- jvmFunctionTyElab safety args ret
    let appGetInstanceField = RApp (Var jcallGetInstanceFieldTTName) $ RConstant (Str fname)
    let f = RApp appGetInstanceField functionTy
    searchFty f

gen safety (MethodDesc (JStaticFieldSetter ty) ret fname args) = do
    functionTy <- jvmFunctionTyElab safety args ret
    let cls = RApp classRaw (classNameElab $ nativeTyClassName ty)
    let appSetStaticField = RApp (Var jcallSetStaticFieldTTName) cls
    let appFunctionName = RApp appSetStaticField $ RConstant (Str fname)
    let f = RApp appFunctionName functionTy
    searchFty f

gen safety (MethodDesc JInstanceFieldSetter ret fname args) = do
    functionTy <- jvmFunctionTyElab safety args ret
    let appSetInstanceField = RApp (Var jcallSetInstanceFieldTTName) $ RConstant (Str fname)
    let f = RApp appSetInstanceField functionTy
    searchFty f

decl syntax javaimport [cmd] [items] = %provide (jimports: JvmFfiDescs) with jvmImport cmd items
decl syntax jdkimport [items] = %provide (jimports: JvmFfiDescs) with jdkImport items

term syntax java [className] [methodName] = (%runElab (j jimports JSafe className methodName))
term syntax [className] "<.>" [methodName] = (%runElab (j jimports JSafe className methodName))

term syntax javaUnsafe [className] [methodName] = (%runElab (j jimports JUnsafe className methodName))
term syntax [className] "<.!>" [methodName] = (%runElab (j jimports JUnsafe className methodName))

term syntax javaField [className] [fieldName] = (%runElab (jf jimports JNullableSafe className fieldName))
term syntax [className] "<.#>" [fieldName] = (%runElab (jf jimports JNullableSafe className fieldName))

term syntax javaFieldUnsafe [className] [fieldName] = (%runElab (jf jimports JUnsafe className fieldName))
term syntax [className] "<.#!>" [fieldName] = (%runElab (jf jimports JUnsafe className fieldName))

term syntax javaSetField [className] [fieldName] = (%runElab (jfs jimports JUnsafe className fieldName))
term syntax [className] "<.=>" [fieldName] = (%runElab (jfs jimports JUnsafe className fieldName))

j : JvmFfiDescs -> JSafety -> String -> String -> Elab ()
j ffiDescs safety ty fname = do
    (methodName, args) <- argTypes
    maybe err (gen safety . addNullableIfNullableProvided args) $
        findFfiDesc ty methodName ((map stripNullable) <$> args) ffiDescs
  where
      err : Elab ()
      err = fail [TextPart $ "Couldn't find JVM FFI function " ++ fname ++ " in " ++ ty ++
        ". Did you forget to import?"]

      argTypes : Elab (String, Maybe (List EType))
      argTypes = case filter (/= "") $ Strings.split (== '(') fname of
        [methodName] => pure (methodName, Nothing)
        methodName :: rest :: _ => case Strings.split (== ')') rest of
          "" :: _ => pure (methodName, Just [])
          paramsStr :: _ =>
            either (\err => fail [TextPart err]) (\args => pure (methodName, Just args)) $ parseArgs $
              Strings.split (== ',') paramsStr

      stripNullable : EType -> EType
      stripNullable ENullableString = EString
      stripNullable (ENullableInterface ty) = EInterface ty
      stripNullable (ENullableClass ty) = EClass ty
      stripNullable (ENullableArray ty) = EArray ty
      stripNullable ty = ty

      makeTypeAccurate : EType -> EType -> EType
      makeTypeAccurate (ENullableClass _) (EClass ty) = ENullableClass ty
      makeTypeAccurate (ENullableClass _) (EInterface ty) = ENullableInterface ty
      makeTypeAccurate (EClass _)         (EInterface ty) = EInterface ty
      makeTypeAccurate (ENullableArray _) (EArray ty) = ENullableArray ty
      makeTypeAccurate ENullableString _ = ENullableString
      makeTypeAccurate _ ty = ty

      makeTypesAccurate : List EType -> JvmFfiDesc -> JvmFfiDesc
      makeTypesAccurate callsiteArgs (MethodDesc invType@(JStatic otherNativeTy) ret name declaredArgs)
        = MethodDesc invType ret name (uncurry makeTypeAccurate <$> zip callsiteArgs declaredArgs)

      makeTypesAccurate callsiteArgs (MethodDesc JInstance ret name declaredArgs@(EString :: _))
        = let correctedTypes = uncurry makeTypeAccurate <$> zip (EString :: callsiteArgs) declaredArgs
          in MethodDesc JInstance ret name correctedTypes

      makeTypesAccurate callsiteArgs (MethodDesc JInstance ret methodName declaredArgs@(EClass className :: _))
        = let nonNullableInstanceCallsiteArgs = EClass className :: callsiteArgs
              correctedTypes = uncurry makeTypeAccurate <$> zip nonNullableInstanceCallsiteArgs declaredArgs
          in MethodDesc JInstance ret methodName correctedTypes

      makeTypesAccurate callsiteArgs (MethodDesc JInstance ret methodName declaredArgs@(EInterface className :: _))
        = let nonNullableInstanceCallsiteArgs = EInterface className :: callsiteArgs
              correctedTypes = uncurry makeTypeAccurate <$> zip nonNullableInstanceCallsiteArgs declaredArgs
          in MethodDesc JInstance ret methodName correctedTypes

      makeTypesAccurate _ desc = desc

      addNullableIfNullableProvided : Maybe (List EType) -> JvmFfiDesc -> JvmFfiDesc
      addNullableIfNullableProvided (Just callsiteArgs) ffiDesc = makeTypesAccurate callsiteArgs ffiDesc
      addNullableIfNullableProvided Nothing ffiDesc = ffiDesc

      argsMatching : Maybe (List EType) -> List EType -> Bool
      argsMatching Nothing _ = True
      argsMatching (Just []) [] = True
      argsMatching (Just []) _ = False
      argsMatching (Just _) [] = False
      argsMatching (Just callsiteArgs) declaredArgs =
        equalLength && (all (uncurry g) $ zip callsiteArgs declaredArgs) where
            equalLength : Bool
            equalLength = length callsiteArgs == length declaredArgs

            g : EType -> EType -> Bool
            -- callsite type may not be accurate as we don't want user to provide class/interface information so it is
            -- always defaulted to Class and here it gets refined based on type provider information
            g (EClass callsiteTy) (EInterface declaredTy) = callsiteTy == declaredTy
            g (EClass callsiteTy) (EClass declaredTy) = callsiteTy == declaredTy

            g callsiteTy declaredTy = callsiteTy == declaredTy

      findFfiDesc : String -> String -> Maybe (List EType) -> List JvmFfiDesc -> Maybe JvmFfiDesc

      findFfiDesc className "<init>" args ffiDescs = find f ffiDescs where
        f : JvmFfiDesc -> Bool
        f (ConstructorDesc EString declaredArgs)
            = className == "java/lang/String" && argsMatching args declaredArgs
        f (ConstructorDesc (EClass otherClassName) declaredArgs)
            = className == otherClassName && argsMatching args declaredArgs
        f _ = False

      findFfiDesc className methodName args ffiDescs = find f ffiDescs where

        f : JvmFfiDesc -> Bool
        f (MethodDesc (JStatic otherNativeTy) ret otherMethodName declaredArgs)
          = className == nativeTyClassName otherNativeTy && methodName == otherMethodName
                && argsMatching args declaredArgs
        f (MethodDesc JInstance ret otherMethodName (EString :: declaredArgs)) =
          className == "java/lang/String" && methodName == otherMethodName && argsMatching args declaredArgs
        f (MethodDesc JInstance ret otherMethodName (EClass otherClassName :: declaredArgs)) =
          className == otherClassName && methodName == otherMethodName && argsMatching args declaredArgs
        f (MethodDesc JInstance ret otherMethodName (EInterface otherClassName :: declaredArgs)) =
          className == otherClassName && methodName == otherMethodName && argsMatching args declaredArgs
        f _ = False

jf : JvmFfiDescs -> JSafety -> String -> String -> Elab ()
jf ffiDescs safety ty fieldName = do
    maybe err (gen safety) $ findFfiDesc ty ffiDescs
  where
      err : Elab ()
      err = fail [TextPart $ "Couldn't find JVM FFI field " ++ fieldName ++ " in " ++ ty ++
        ". Did you forget to import?"]

      findFfiDesc : String -> List JvmFfiDesc -> Maybe JvmFfiDesc
      findFfiDesc className ffiDescs = find f ffiDescs where

        f : JvmFfiDesc -> Bool
        f (MethodDesc (JStaticField otherNativeTy) ret otherFieldName _)
          = className == nativeTyClassName otherNativeTy && fieldName == otherFieldName
        f (MethodDesc JInstanceField ret otherFieldName [EString]) =
          className == "java/lang/String" && fieldName == otherFieldName
        f (MethodDesc JInstanceField ret otherFieldName [EClass otherClassName]) =
          className == otherClassName && fieldName == otherFieldName
        f _ = False

jfs : JvmFfiDescs -> JSafety -> String -> String -> Elab ()
jfs ffiDescs safety ty fieldName = do
    maybe err (gen safety) $ findFfiDesc ty ffiDescs
  where
      err : Elab ()
      err = fail [TextPart $ "Couldn't find JVM FFI field " ++ fieldName ++ " in " ++ ty ++
        ". Did you forget to import?"]

      findFfiDesc : String -> List JvmFfiDesc -> Maybe JvmFfiDesc
      findFfiDesc className ffiDescs = find f ffiDescs where

        f : JvmFfiDesc -> Bool
        f (MethodDesc (JStaticFieldSetter otherNativeTy) ret otherFieldName _)
          = className == nativeTyClassName otherNativeTy && fieldName == otherFieldName
        f (MethodDesc JInstanceFieldSetter ret otherFieldName (EClass otherClassName :: _)) =
          className == otherClassName && fieldName == otherFieldName
        f _ = False


text:
module BC

-- run with:  idris -i ./idris/libs/pruviloj Learn/ElabSlides.idr

import public Language.Reflection.Utils
import public Pruviloj

%default total

||| Extract the pattern variable bindings from around a term.
patvarArgs : Raw -> (List (TTName, Raw), Raw)
patvarArgs (RBind n (PVar ty) tm) =
    let rest = patvarArgs tm
    in ((n, ty) :: fst rest, snd rest)
patvarArgs tm = ([], tm)

||| Find the conjunction of a context of reflected types, expressed as
||| an iterated sigma type.
conjoin : List (TTName, Raw) -> Raw
conjoin [] = `(() : Type)
conjoin ((h, t) :: ts) = `(DPair ~t ~(RBind h (Lam t) (conjoin ts)) : Type)

||| Get the projections of the tails of an iterated sigma type
proj' : List (TTName, Raw) -> TTName -> Raw -> Elab Raw
proj' [] n _ = fail [NamePart n, TextPart "not in iterated sigma"]
proj' ((f, t) :: fs) n x =
  if f == n
    then pure x
    else do inner <- proj' fs n x
            pure `(DPair.snd {a=~t}
                             {P=~(RBind n (Lam t) (conjoin fs))}
                             ~inner)

||| Get the projection corresponding to a particular assumption that
||| we've wrapped up in an iterated sigma.
proj : List (TTName, Raw) -> TTName -> Raw -> Elab Raw
proj (f::fs) n x =
    do inner <- proj' (f::fs) n x
       pure `(DPair.fst {a=~(snd f)}
                        {P=~(RBind (fst f) (Lam (snd f)) (conjoin fs))}
                        ~inner)
proj [] _ _ = empty

||| Rename a free variable
rename : (from, to : TTName) -> Raw -> Raw
rename from to (Var n) =
    Var $ if n == from then to else n
rename from to (RBind n b tm) =
    if n == from
      then RBind n (assert_total $ map (rename from to) b) tm
      else RBind n (assert_total $ map (rename from to) b) (rename from to tm)
rename from to (RApp tm tm') =
    RApp (rename from to tm) (rename from to tm')
rename from to RType = RType
rename from to (RUType u) = RUType u
rename from to (RConstant c) = RConstant c

mutual
  ||| Compute the free variables of a term.
  fv : Raw -> List TTName
  fv (Var n) = [n]
  fv (RBind n b tm) = nub (assert_total $ fvB b) ++ delete n (fv tm)
  fv (RApp tm tm') = nub $ fv tm ++ fv tm'
  fv RType = []
  fv (RUType x) = []
  fv (RConstant c) = []

  ||| Compute the free variables of a binder.
  fvB : Binder Raw -> List TTName
  fvB (Lam ty) = fv ty
  fvB (Pi ty kind) = nub $ fv ty ++ fv kind
  fvB (Let ty val) = nub $ fv ty ++ fv val
  fvB (Hole ty) = fv ty
  fvB (GHole ty) = fv ty
  fvB (Guess ty val) = nub $ fv ty ++ fv val
  fvB (PVar ty) = fv ty
  fvB (PVTy ty) = fv ty

||| Substitute a free variable, avoiding capture as necessary with gensyms.
subst : (from : TTName) -> (to : Raw) -> Raw -> Elab Raw
subst from to (Var n) =
  if from == n then pure to else pure (Var n)
subst from to (RBind n b tm) =
  do b' <- assert_total $ traverse (subst from to) b
     if from == n
       then do n' <- gensym "bound"
               RBind n' b' <$> assert_total (subst from to (rename n n' tm))
       else RBind n b' <$> subst from to tm
subst from to (RApp tm tm') = [| RApp (subst from to tm) (subst from to tm') |]
subst from to RType = pure RType
subst from to (RUType u) = pure (RUType u)
subst from to (RConstant c) = pure (RConstant c)

||| Perform multiple substitutions.
substs : List (TTName, Raw) -> Raw -> Elab Raw
substs [] tm = pure tm
substs ((n,t)::ss) tm = subst n t tm >>= substs ss

parameters (inFun : TTName, outFun : TTName, accPred : TTName)

  ||| The algorithm from Definition 5 in the paper. Given a pattern
  ||| variable context and a right-hand side, compute the additional
  ||| pattern variables and the new right-hand side to make the
  ||| function total with respect to the accessibility predicate.
  covering
  translate : Nat -> List (TTName, Raw) -> Raw -> Elab (List (TTName, Raw), Raw)
  translate arity gamma (Var n) =
    case lookup n gamma of
      Just _ => pure ([], Var n)
      Nothing =>
        if n == inFun
          then fail [TextPart "Cannot translate when ", NamePart inFun, TextPart "is not fully applied."]
          else pure ([], Var n)

  translate arity gamma (RBind n (Lam ty) tm) =
    do (phi', tm') <- translate arity (gamma ++ [(n, ty)]) tm
       case phi' of
         [] => pure ([], RBind n (Lam ty) tm')
         [(n', t')] =>
           do H <- gensym "H"
              let phi'' = [(H, RBind n (Pi ty `(Type)) t')]
              newBody <- subst n' (RApp (Var H) (Var n)) tm'
              pure (phi'', RBind n (Lam ty) newBody)
         nonempty =>
           do H <- gensym "H"
              let HTy = conjoin nonempty
              let phi'' = [(H, RBind n (Pi ty `(Type)) HTy)]
              toSubst <- for nonempty $ \(n', _) =>
                           do to <- proj nonempty n' (RApp (Var H) (Var n))
                              pure (n', to)
              newBody <- substs toSubst tm'
              pure (phi'', RBind n (Lam ty) newBody)
  translate arity gamma (RBind n b tm) = fail [TextPart "unsupported binding form"]
  translate arity gamma (RApp tm tm') =
    case unApply (RApp tm tm') of
      (Var n, args) =>
        do (phis, args') <- List.unzip <$> traverse (translate arity gamma) args
           (recPhi, recArg) <-
             if n == inFun
               then
                 if length args /= arity
                   then fail [TextPart "Cannot translate when ", NamePart inFun, TextPart "is not fully applied."]
                   else
                     do h <- gensym "h"
                        let hTy = mkApp (Var accPred) args'
                        pure ([(h, hTy)], [Var h])
               else pure ([], [])
           pure (concat phis ++ recPhi, mkApp (Var (if n == inFun then outFun else n)) (args' ++ recArg))
      (op, args) => fail [TextPart "can't apply", RawPart op]
  translate arity gamma RType = pure ([], RType)
  translate arity gamma (RUType u) = pure ([], RUType u)
  translate arity gamma (RConstant c) = pure ([], RConstant c)

  ||| Wrapper around `translate` to create new definitions and constructors suitable for Idris.
  ||| @ which which constructor is this?
  ||| @ clauses remaining pattern-matching clauses
  export covering
  processClauses : (which : Nat) -> (clauses : List (FunClause TT)) -> Elab (List (FunClause Raw, ConstructorDefn))
  processClauses which [] = pure []
  processClauses which (MkImpossibleClause _ :: xs) = processClauses which xs
  processClauses which (MkFunClause lhs rhs :: xs) =
    do (gamma, lhsBody) <- patvarArgs <$> (forget lhs)
       (_,     rhsBody) <- patvarArgs <$> (forget rhs)
       let cn = mkN which accPred
       let pats = snd (unApply lhsBody)
       (phi, newRhs) <- translate (length pats) gamma rhsBody
       let newLhs = mkApp (Var outFun)
                          (pats ++ [mkApp (Var cn) (map (Var . fst) (gamma ++ phi))])
       let ctor = Constructor cn ([MkFunArg n ty Implicit NotErased | (n, ty) <- gamma] ++
                                  [MkFunArg n ty Explicit NotErased | (n, ty) <- phi])
                                 (mkApp (Var accPred) pats)
       let withPats = \tm => foldr (\nty, body : Raw => RBind (fst nty) (PVar (snd nty)) body) tm (gamma ++ phi)
       rest <- processClauses (S which) xs
       pure $ (MkFunClause (withPats newLhs) (withPats newRhs), ctor) :: rest
    where
      mkN : Nat -> TTName -> TTName
      mkN i (NS n ns) = mkN i n
      mkN i (UN n) = UN (n ++ "Case" ++ show i)
      mkN i (MN j str) = MN j (str ++ "Case" ++ show i)
      mkN i _ = UN $ "x_Case" ++ show i

  ||| Perform the Bove-Capretta translation.
  export covering
  bc : Elab ()
  bc =
    do (inFun', Ref, inTy) <- lookupTyExact inFun
         | _ => fail [NamePart inFun, TextPart "does not uniquely determine a function"]
       -- Step one: declare the datatype and function
       -- The datatype will take the same args as the initial function.
       (_, args, res) <- lookupArgsExact inFun'
       declareDatatype $ Declare accPred args `(Type)
       -- The function will recurse over the datatype
       declareType $ Declare outFun (args ++ [MkFunArg `{{acc}} (mkApp (Var accPred) (map (Var . name) args)) Explicit NotErased]) res

       -- step two: for each clause, make a corresponding constructor
       DefineFun _ oldClauses <- lookupFunDefnExact inFun'
       (newClauses, ctors) <- unzip <$> processClauses Z oldClauses
       defineDatatype $ DefineDatatype accPred ctors

       -- step three: define the function by recursion over the datatype
       defineFunction $ DefineFun outFun newClauses
       pure ()

||| Perform the Bove-Capretta transformation, then generate a new
||| version of the function that is total, assuming that a proof
||| obligation is fulfilled.
||| @ inFun the program to transform
||| @ outFun the name for the new underlying function
||| @ wrapper the name for the generated wrapper
||| @ accPred the name for the generated accessibility predicate
||| @ totalProof the name to use for the totality proof obligation
export covering
bc' : (inFun, outFun, wrapper, accPred, totalProof : TTName) -> Elab ()
bc' inFun outFun wrapper accPred totalProof =
    do bc inFun outFun accPred
       (_, args, res) <- lookupArgsExact inFun
       declareType $ Declare wrapper args res
       declareType $ Declare totalProof args (mkApp (Var accPred) (map (Var . name) args))
       let withPats = \tm => foldr (\arg, body : Raw => RBind (name arg) (PVar (type arg)) body)
                                   tm
                                   args
       defineFunction $ DefineFun wrapper [
           MkFunClause (withPats (mkApp (Var wrapper) (map (Var . name) args)))
                       (withPats (mkApp (Var outFun) (map (Var . name) args ++
                                                      [mkApp (Var totalProof)
                                                             (map (Var . name) args)])))
         ]

decl syntax "toBC" {inFun} "==>" {outFun} "|" {pred} =
  %runElab (bc `{inFun} `{{outFun}} `{{pred}})

decl syntax "makeTotal" {inFun} "==>" {outFun} "|" {pred} "as" {wrapper} "by" {totalProof} =
  %runElab (bc' `{inFun} `{{outFun}} `{{wrapper}} `{{pred}} `{{totalProof}})


text:
module Main

import Data.Vect
import Data.Fin
import Unification

f : Term (Fin 2)
f = identifier (MkName "f")

c : Term (Fin 2)
c = identifier (MkName "c")

cc : Term (Fin 2)
cc = app c c

x : Term (Fin 2)
x = var 0

y : Term (Fin 2)
y = var 1

unifyXY : Maybe (Exists (SubstList 2))
unifyXY = unify x y

unifyXFCC : Maybe (Exists (SubstList 2))
unifyXFCC = unify x (app f cc)

toNatPair : Fin n -> (Nat, Nat)
toNatPair (FZ {k=k}) = (1, S k)
toNatPair (FS i {k=k}) = (1 + fst (toNatPair i), S k)

Show (Fin n) where
  showPrec d i = case toNatPair i of
    (i, n) => showCon d "Fin" (" " ++ show i ++ "/" ++ show n)

Show n => Show (Term n) where
  showPrec d = fold
    (\i => showCon d "Var" (showArg i))
    (\c => case c of (MkName n) => showCon d "Identifier" (showArg n))
    (\l, r => showCon d "App" (" " ++ l ++ " " ++ r))

Show (Subst m) where
  showPrec d (MkSubst x t) = showCon d "Subst" ((showArg x) ++ (showArg t))

Show (SubstList m n) where
  show Nil = "[]"
  show (s :: ss) = (show s) ++ " :: " ++ (show ss)

Show (Exists (SubstList n)) where
  show (Evidence _ ss) = show ss

main : IO ()
main = do
  printLn unifyXY
  printLn $ unify (app f (app f c)) (app f y)
  printLn unifyXFCC

max_stars_repo_name: sammthomson/IdrisUnification

max_issues_repo_name: sammthomson/IdrisUnification

max_forks_repo_name: sammthomson/IdrisUnification