text:
module Idrlisp.Value

import Data.SortedMap
import public Idrlisp.Sexp
import public Idrlisp.Pattern
import public Idrlisp.Signature
import public Idrlisp.Code
import Idrlisp.Env
import Idrlisp.Vec

%default covering

mutual
  public export
  Value : Type
  Value = Sexp Native

  public export
  ValueList : Type
  ValueList = SList Native

  public export
  data Native
    = NBuiltin Builtin
    | NSyntax Syntax
    | NFun Closure
    | NMacro Closure
    | NVec (Vec Value)
    | NPort File

  public export
  record Builtin where
    constructor MkBuiltin
    run : List Value -> VM ()

  public export
  record Syntax where
    constructor MkSyntax
    macroExpand : List Value -> MacroExpand (List Value)
    compile : List Value -> Compile ()

  public export
  record Closure where
    constructor MkClosure
    env : Env Value
    pattern : Pattern
    body : Code Value

  namespace VM
    public export
    data VM : Type -> Type where
      -- S
      Push : Value -> VM ()
      Pop : VM (Maybe Value)

      -- E
      Get : String -> VM (Either String Value)
      Define : String -> Value -> VM (Either String ())
      Set : String -> Value -> VM (Either String ())
      CaptureEnv : VM (Env Value)

      -- C
      Next : VM (Maybe (Inst Value))

      -- D
      Enter : Env Value -> Code Value -> VM ()
      Leave : VM (Either () (Env Value, Code Value))

      -- for continuation support
      DropCont : VM ()
      RestoreCont : Cont -> VM ()
      CaptureCont : VM Cont

      -- for eval/macroexpand support
      CaptureContext : VM Context

      LoadBuiltin : String -> VM (Maybe Builtin)
      Action : IO a -> VM a

      Pure : a -> VM a
      Bind : VM a -> (a -> VM b) -> VM b
      Fail : String -> VM a

    public export
    record Cont where
      constructor MkCont
      stack : List Value
      env : Env Value
      code : Code Value
      dump : List (Env Value, Code Value)

  namespace MacroExpander
    public export
    data MacroExpand : Type -> Type where
      Refer : String -> MacroExpand (Maybe Value)
      Execute : VM a -> MacroExpand a

      Pure : a -> MacroExpand a
      Bind : MacroExpand a -> (a -> MacroExpand b) -> MacroExpand b
      Fail : String -> MacroExpand a

  namespace Compiler
    public export
    data Compile : Type -> Type where
      Do : Inst Value -> Compile ()
      Refer : String -> Compile (Maybe Value)
      Block : Compile () -> Compile (Code Value)

      Pure : a -> Compile a
      Bind : Compile a -> (a -> Compile b) -> Compile b
      Fail : String -> Compile a

  public export
  record Context where
    constructor MkContext
    topLevel : Env Value
    builtins : SortedMap String Builtin

namespace Show
  export
  Show Native where
    show (NBuiltin x) = "<builtin>"
    show (NSyntax x) = "<syntax>"
    show (NFun x) = "<fun>"
    show (NMacro x) = "<macro>"
    show (NPort x) = "<port>"
    show (NVec x) = "<vec>"

  data ShowId = MkShowId String

  Show ShowId where
    show (MkShowId s) = s

  export
  showIO : Value -> IO String
  showIO value = show <$> traverse showNativeIO value
    where
      showNativeIO : Native -> IO ShowId
      showNativeIO (NBuiltin _) = pure $ MkShowId "<builtin>"
      showNativeIO (NSyntax _) = pure $ MkShowId "<syntax>"
      showNativeIO (NFun _) = pure $ MkShowId "<fun>"
      showNativeIO (NMacro _) = pure $ MkShowId "<macro>"
      showNativeIO (NPort _) = pure $ MkShowId "<port>"
      showNativeIO (NVec vec) = do
        xs <- Vec.toList vec
        ss <- traverse (traverse showNativeIO) xs
        pure $ MkShowId $ show (Sym "vec" :: foldr (::) Sexp.Nil ss)

namespace Signature
  public export
  data NativeSignature
    = NBuiltin
    | NSyntax
    | NFun
    | NMacro
    | NPort
    | NVec

  public export
  Match NativeSignature Native where
    SignatureType NBuiltin = Builtin
    SignatureType NSyntax = Syntax
    SignatureType NFun = Closure
    SignatureType NMacro = Closure
    SignatureType NPort = File
    SignatureType NVec = Vec Value

    match NBuiltin (NBuiltin x) = Just x
    match NBuiltin _ = Nothing
    match NSyntax (NSyntax x) = Just x
    match NSyntax _ = Nothing
    match NFun (NFun x) = Just x
    match NFun _ = Nothing
    match NMacro (NMacro x) = Just x
    match NMacro _ = Nothing
    match NPort (NPort x) = Just x
    match NPort _ = Nothing
    match NVec (NVec x) = Just x
    match NVec _ = Nothing

  public export
  ValueSignature : Type
  ValueSignature = Signature NativeSignature

  public export
  ValueArgsSignature : Type
  ValueArgsSignature = ArgsSignature NativeSignature

namespace VM
  export
  Functor VM where
    map f a = Bind a (\a' => Pure (f a'))

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

  export
  Monad VM where
    (>>=) = Bind

  export
  pop : VM Value
  pop =
    case !Pop of
      Just value => Pure value
      Nothing => Fail "Internal error: inconsistent stack"

  export
  define : String -> Value -> VM ()
  define name value =
    case !(Define name value) of
      Left err => Fail $ "Evaluation error: cannot define variable: " ++ err
      Right () => pure ()

  export
  set : String -> Value -> VM ()
  set name value =
    case !(Set name value) of
      Left err => Fail $ "Evaluation error: cannot set variable: " ++ err
      Right () => pure ()

  export
  applyClosure : Closure -> List Value -> VM ()
  applyClosure closure args = do
    Enter (env closure) (body closure)
    case Pattern.bind (pattern closure) args of
      Left err => Fail $ "Evaluation error: cannot call closure: " ++ err
      Right mapping => traverse_ (uncurry define) mapping

  export
  apply : Value -> List Value -> VM ()
  apply (Pure (NBuiltin builtin)) args = run builtin args
  apply (Pure (NFun closure)) args = applyClosure closure args
  apply f args = Fail $ "Evaluation error: cannot call " ++ show f

  export
  inst : Inst Value -> VM ()
  inst (Ldc constant) = Push constant
  inst (Ldv variable) =
    case !(Get variable) of
      Right x => Push x
      Left err => Fail $ "Evaluation error: undefined variable: " ++ err
  inst (Ldf pat code) = Push $ Pure $ NFun $ MkClosure !CaptureEnv pat code
  inst (Ldm pat code) = Push $ Pure $ NMacro $ MkClosure !CaptureEnv pat code
  inst (Ldb name) =
    case !(LoadBuiltin name) of
      Just builtin => Push $ Pure $ NBuiltin builtin
      Nothing => Fail $ "Evaluation error: unsupported builtin: " ++ name
  inst (Sel thenc elsec) =
    case !pop of
      Bool False => Enter !CaptureEnv elsec
      _ => Enter !CaptureEnv thenc
  inst (App argc) = do
    revArgs <- sequence $ replicate argc pop
    f <- pop
    apply f (reverse revArgs)
  inst Leave =
    case !Leave of
      Right _ => pure ()
      Left () => Fail "Internal error: inconsistent dump"
  inst Pop = ignore pop
  inst (Def name) = define name !pop
  inst (Set name) = set name !pop

  export
  instCycle : VM Value
  instCycle =
    case !Next of
      Just i => do inst i; instCycle
      Nothing => pop

namespace MacroExpander
  export
  Functor MacroExpand where
    map f a = Bind a (\a' => Pure (f a'))

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

  export
  Monad MacroExpand where
    (>>=) = Bind

  export
  refer : Value -> MacroExpand (Maybe Value)
  refer (Sym sym) = Refer sym
  refer _ = pure Nothing

  mutual
    export
    expand : Bool -> Value -> MacroExpand Value
    expand recurse expr with (cast {to = ValueList} expr)
      | Proper (m :: args) =
          case !(refer m) of
            Just (Pure (NSyntax syn)) =>
              if recurse
                then pure $ m :: foldr (::) Nil !(macroExpand syn args)
                else ifThenElse recurse expandChildren pure expr
            Just (Pure (NMacro closure)) => do
              expr <- Execute (applyClosure closure args *> instCycle)
              ifThenElse recurse (expand True) pure expr
            _ => ifThenElse recurse expandChildren pure expr
      | _ = ifThenElse recurse expandChildren pure expr

    export
    expandChildren : Value -> MacroExpand Value
    expandChildren (car :: cdr) = [| expand True car :: expandChildren cdr |]
    expandChildren expr = pure expr

namespace Compiler
  export
  Functor Compile where
    map f a = Bind a (\a' => Pure (f a'))

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

  export
  Monad Compile where
    (>>=) = Bind

  export
  refer : Value -> Compile (Maybe Value)
  refer (Sym sym) = Refer sym
  refer _ = pure Nothing

  mutual
    export
    load : Value -> Compile ()
    load (Sym sym) = Do $ Ldv sym
    load (f :: xs) with (cast {to = ValueList} xs)
      | Proper args =
          case !(refer f) of
            Just (Pure (NSyntax syn)) => compile syn args
            _ => do
              load f
              traverse_ load args
              Do $ App (length args)
      | Improper _ = Fail $ "Compile error: improper list: " ++ show (f :: xs)
    load x = Do $ Ldc x

max_stars_repo_name: yubrot/idrlisp

max_issues_repo_name: yubrot/idrlisp

max_forks_repo_name: yubrot/idrlisp


text:
natElim : (p : Nat -> Type) -> p Z -> ((k : Nat) -> p k -> p (S k)) ->
          (x : Nat) -> p x

natElim2 : (p : Nat -> Type) -> p Z -> ((k : Nat) -> p k -> p (S k)) ->
           (x : Nat) -> p x
natElim2 p x f Z = x
natElim2 p x f (S k) = ?foo

listElim : (p : List a -> Type) ->
           (mnil : p []) ->
           (mcons : (x : _) -> (xs : List a) -> p xs -> p (x :: xs)) ->
           (xs : List a) -> p xs

ext: idr


text:
module OTP

data Bit : Type where
    ZeroBit : Bit
    OneBit : Bit

xor : Bit -> Bit -> Bit
xor ZeroBit ZeroBit = ZeroBit
xor ZeroBit OneBit = OneBit
xor OneBit ZeroBit = OneBit
xor OneBit OneBit = ZeroBit

data BitVector : Nat -> Type where
    Nil : BitVector Z
    Cons : Bit -> BitVector n -> BitVector (S n)
%name BitVector xs, ys -- hint for automatic naming

bitwiseXor : (n : Nat) -> BitVector n -> BitVector n -> BitVector n
bitwiseXor 0 [] [] = Nil
bitwiseXor (S k) (Cons x xs) (Cons y ys) = Cons (xor x y) (bitwiseXor k xs ys)

otpEncrypt : (n : Nat) -> (message : BitVector n) -> (key : BitVector n) -> BitVector n
otpEncrypt n message key = bitwiseXor n message key

otpDecrypt : (n : Nat) -> (cipherText : BitVector n) -> (key : BitVector n) -> BitVector n
otpDecrypt n cipherText key = bitwiseXor n cipherText key

-- proof below

total xorCancel : (x : Bit) -> (y : Bit) -> xor (xor x y) y = x
xorCancel ZeroBit ZeroBit = Refl
xorCancel ZeroBit OneBit = Refl
xorCancel OneBit ZeroBit = Refl
xorCancel OneBit OneBit = Refl

total
otpCorrect : (n : Nat) -> (msg : BitVector n) -> (ky : BitVector n) -> otpDecrypt n (otpEncrypt n msg ky) ky = msg
otpCorrect 0 [] [] = Refl
otpCorrect (S n) (Cons x xs) (Cons y ys) =
    let xor_eq = xorCancel x y in
    rewrite xor_eq in
    let ih = otpCorrect n xs ys in
    rewrite ih in
    Refl

max_stars_repo_name: DejanMilicic/IdrisPlayground

max_issues_repo_name: DejanMilicic/IdrisPlayground

max_forks_repo_name: DejanMilicic/IdrisPlayground


text:
module Dart.String

export
%foreign "Dart:.padLeft"
padLeft : String -> Int -> String -> String


text:
import Data.Vect

takeFromStream : List (n ** Vect n Int)
takeFromStream = [(n ** take n [3..]) | n <- [0, 1, 5]]

main : IO ()
main = do printLn takeFromStream


text:
-- test that bufferAndSignal doesn't block

import System.Concurrency.BufferedChannel

main : IO ()
main = do bcRef <- makeBufferedChannel
          (MkDPair bc buffer) <- becomeBuffer bcRef
          buffer Signal bc [1,2,3]
          putStrLn "Success!"


text:
data Vect : Nat -> Type -> Type where
  Nil  : Vect 0 a
  (::) : a -> Vect n a -> Vect (S n) a

-- Recursion works fine:
--exactLength Z [] = Just []
--exactLength Z (x :: y) = Nothing
--exactLength (S k) [] = Nothing
--exactLength (S k) (x :: y) = map (x ::) $ exactLength k y

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

natEqSucc : EqNat k j -> EqNat (S k) (S j)
natEqSucc (Same k) = Same (S k)

checkEqNat : (a : Nat) -> (b : Nat) -> Maybe (EqNat a b)
checkEqNat Z Z = Just $ Same Z
checkEqNat Z (S k) = Nothing
checkEqNat (S k) Z = Nothing
checkEqNat (S k) (S j) = [| natEqSucc (checkEqNat k j) |]

replaceLength : EqNat m n -> Vect m a -> Vect n a
replaceLength (Same m) y = y

exactLength : (len : Nat) -> Vect n Nat -> Maybe (Vect len Nat)
exactLength {n} len v = [| replaceLength (checkEqNat n len) (pure v) |]

checkEqNat' : (a : Nat) -> (b : Nat) -> Maybe (a = b)
checkEqNat' Z Z = Just Refl
checkEqNat' Z (S k) = Nothing
checkEqNat' (S k) Z = Nothing
checkEqNat' (S k) (S j) = [| cong $ checkEqNat' k j |]

sameCons : {xs : List a} -> {ys : List a} -> xs = ys -> x :: xs = x :: ys
sameCons Refl = Refl

sameLists : {xs : List a} -> {ys : List a} -> x = y -> xs = ys -> x :: xs = y :: ys
sameLists Refl Refl = Refl

data ThreeEq : a -> b -> c -> Type where
  ThreeSame : ThreeEq a a a

allSameS : (x, y, z : Nat) -> ThreeEq x y z -> ThreeEq (S x) (S y) (S z)
allSameS z z z ThreeSame = ThreeSame

--append : (x : a) -> Vect n a -> Vect (S n) a
--append x [] = [x]
--append x (y :: z) = y :: append x z


text:
module IdrisNet.TCP.TCPCommon
import Network.Socket

data SocketOperationRes a = OperationSuccess a
                          | FatalError SocketError -- Most socket errors are fatal.
                          | RecoverableError SocketError -- EAGAIN / EWOULDBLOCK
                          | ConnectionClosed


text:
module Chapter2

average : (str : String) -> Double
average str = let numWords = length (words str)
                  totalLength = sum (lengths (words str)) in ((cast totalLength) / (cast numWords))
  where lengths : List String -> List Nat
        lengths xs = map length xs

main : IO ()
main = repl "Enter a string: " showAverage
  where showAverage : String -> String
        showAverage s = "Avg word length: "
                        ++ (show (average s))
                        ++ "\n"

-- using 'the' to explicitly annotate the type of things:
-- note this NOT cast.  `the` has the type (t : Type) -> (value : t) -> t
-- the Double 4 gives 4.0

integerval : Integer
integerval = 4

doubleval : Double
doubleval = 0.1

intsumval : Integer
--intsumval = integerval + (the Integer doubleval)  -- this still type errors
intsumval = integerval + (cast doubleval)  -- OK

-- type of cast is (Cast from to) => from -> to  -- notice the => meaning there needs
-- to be a definition of Cast from to to be able to convert from from to to :)

-- idris has eager evaluation but also has Lazy type to support Lazy evaluations.
-- in idris we need to annotate function as we can not do type inference on them
-- (as opposed to Haskell)

identity : ty -> ty  -- here, ty is an actual VARIABLE (type variable)
identity x = x

mythe : (ty : Type) -> ty -> ty
mythe t x = x  -- this is fine, the t here is the same as ty in the type definition

-- generic types (remember from Cast from to)
double : Num ty => ty -> ty  -- Num ty can also be seen as a type "constraint" or *Interface*
double x = x + x

-- Higher order functions
twice : (a -> a) -> a -> a
twice f x = f (f x)

Shape : Type
rotate : Shape -> Shape
-- I like how we don't have to define rotate

turn_around : Shape -> Shape
turn_around s = twice rotate s

turn_around' : Shape -> Shape
turn_around' = twice rotate  -- 'point-free' notation

-- Anon functions
myanonexample : Integer -> Integer
myanonexample = \x => x * x  -- note the => instead of -> (as in Haskell)

unit_type_example : ()  -- unit TYPE
unit_type_example = ()  -- unit VALUE  (overloaded syntax)

-- multi-tuples are nested pairs (which seems kind of awkward if you think about it)
-- (1,2,3) == (1, (2, 3))  -- note there is no unit type

-- Note: Idris does have type inference in the REPL.  You can type [1,2,3] and
-- it will know it is List Integer

-- Modules
-- See Average.idr

-- Whitespace rule:
-- same column, new definition
-- indented: continuation of previous expression

-- Documentation comments:
||| This is a documentation comment for myAwesomeFunction
||| (which is not very awesome)
||| @arg an awesome and totally irrelevant argument
myAwesomeFunction : arg -> ()
myAwesomeFunction x = ()  -- note that arg in documentation is one in type defintion

-- see AveMain.idr

{-
Exercises:
1: (String, String, String)
   List String
   ((Char, String), String)  -- nesting normally occures on rhs
-}
-- ex 2
palindrome : String -> Bool
palindrome s = s == (reverse s)

-- ex 3
ipalindrome : String -> Bool
ipalindrome s = let lower = toLower s in
                    palindrome lower

-- ex 4
palindrome10 : String -> Bool
palindrome10 s = ((length s) > 10) && (palindrome s)

-- ex 5
palindromen : Nat -> String -> Bool
palindromen k s = ((length s) > k) && (palindrome s)

-- ex 6
counts : String -> (Nat, Nat)
counts s = (length (words s), length s)

-- ex 7
top_ten : Ord a => List a -> List a
top_ten = List.take 10 . reverse . sort   -- point-free notation ftw

-- ex 8
over_length : Nat -> List String -> Nat
over_length k xs = length (filter (> k) (map length xs))

-- bonus:
over_length' : Nat -> List String -> Nat
over_length' k = length . filter (> k) . map length  -- point-free version

-- ex 9
-- too lazy
generic_repl : Show a => (String -> a) -> IO ()
generic_repl f = repl "Enter a string " ((++ "\n") . show . f)

max_stars_repo_name: neduard/type-driven-development

max_issues_repo_name: neduard/type-driven-development

max_forks_repo_name: neduard/type-driven-development


text:
module Minesweeper.Game

import Minesweeper.Board
import Control.Monad.State

public export
data Difficulty = Easy | Medium | Hard

public export
data GState = Playing String | Won | Lost

-- | Get board dimensions and number of mines
--   for the given difficulty level
export
getSetupDetails : Difficulty -> (Pos, Nat)
getSetupDetails Easy = ((MkPos 8 8), 10)
getSetupDetails Medium = ((MkPos 16 16), 40)
getSetupDetails Hard = ((MkPos 30 16), 99)

-- | Attempt to reveal the given position
-- returns the GameState after this move
export
revealPos : Pos -> State (Board m n) GState
revealPos pos@(MkPos x y) = do
  board <- get
  case (reveal pos board) of
    (Left err) => pure $ Playing err
    (Right newBoard) => do
      put newBoard
      if checkWin newBoard then pure Won
      else if checkLose newBoard then pure Lost
      else pure $ Playing $ "Revealed square in row:" ++ show y ++ " col:" ++  show x ++ "\n"

max_stars_repo_name: RossMeikleham/Idris-Minesweeper

max_issues_repo_name: RossMeikleham/Idris-Minesweeper

max_forks_repo_name: RossMeikleham/Idris-Minesweeper


text:
import Data.Vect

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

my_reverse : List a -> List a
my_reverse [] = []
my_reverse (x :: xs) = xs ++ [x]

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

my_vect_map : (a -> b) -> Vect n a -> Vect n b
my_vect_map f [] = []
my_vect_map f (x :: xs) = f x :: my_vect_map f xs

max_stars_repo_name: DimaSamoz/idris-book

max_issues_repo_name: DimaSamoz/idris-book

max_forks_repo_name: DimaSamoz/idris-book


text:
import Data.List

[myord] Ord Nat where
   compare Z (S n)     = GT
   compare (S n) Z     = LT
   compare Z Z         = EQ
   compare (S x) (S y) = compare @{myord} x y

testList : List Nat
testList = [3,4,1]


text:
module Test.FileSystem

import Control.Monad.Free
import Control.Monad.AsyncJS_IO
import Node.Free.FileSystem
import Node.Sync.FileSystem
import Node.Async.FileSystem

exclaimHello : FileSystem Unit
exclaimHello = do
  writeFile "foo.txt" "hello, world!"
  contents <- readFile "foo.txt"
  writeFile "foo.txt" (contents <+> "!")

copyHello : FileSystem Unit
copyHello = do
  contents <- readFile "foo.txt"
  writeFile "bar.txt" contents

consoleLog : String -> AsyncJS_IO ()
consoleLog s = liftJS_IO (putStrLn' s)

namespace Main
  export
  main : JS_IO ()
  main = do
    runAsync $ do
      foldFree interpret exclaimHello
      foldFree interpret copyHello
      c <- foldFree interpret (readFile "bar.txt")
      consoleLog c

max_stars_repo_name: Risto-Stevcev/idris-node-fs

max_issues_repo_name: Risto-Stevcev/idris-node-fs

max_forks_repo_name: Risto-Stevcev/idris-node-fs


text:
import Data.Vect

%default total

interface ArrayM where
  Array : (n : Nat) -> (a : Type) -> Type
  create : (n : Nat) -> a -> Array n a

  lkp : (i : Nat) -> (prf : LTE (S i) n) -> Array n a -> a
  upd : a -> (i : Nat) -> (prf : LT i n) -> Array n a -> Array n a

using (ArrayM)
  sumArrayHelp : Num a => (k : Nat) -> LT k (S n) -> Array n a -> a
  sumArrayHelp Z x y = 0
  sumArrayHelp (S k) (LTESucc prf) y
    = lkp k prf y + sumArrayHelp k (lteSuccRight prf) y

  sumArray : Array n Int -> Int
  sumArray {n} x = sumArrayHelp n lteRefl x

implementation ArrayM where
  Array = Vect

  create n x = replicate n x

  lkp Z (LTESucc x) (y :: xs) = y
  lkp (S k) (LTESucc x) (y :: xs) = lkp k x xs

  upd val Z (LTESucc p) (_ :: xs) = val :: xs
  upd val (S k) (LTESucc p) (x :: xs) = x :: upd val k p xs

-- using (ArrayM as vectArray)

testSum : Array n Int -> Int
testSum = sumArray

main : IO ()
main = printLn (testSum (upd 11 1 (LTESucc (LTESucc LTEZero)) (create 4 10)))

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Main

import ErlPrelude

print_raw : a -> EIO ()
print_raw x = do print_raw' (MkERaw x)
                 return ()
  where print_raw' : (ErlRaw a) -> EIO ()
        print_raw' r = foreign FFI_Erl "io:format" (String -> List (ErlRaw a) -> EIO ()) "~p~n" [r]

lists_reverse : List Int -> EIO (List Int)
lists_reverse = foreign FFI_Erl "lists:reverse" (List Int -> EIO (List Int))

lists_map : (Int -> EIO Char) -> List Int -> EIO (List Char)
lists_map f = foreign FFI_Erl "lists:map" ((ErlFn (Int -> EIO Char)) -> List Int -> EIO (List Char)) (MkErlFun f)

main : EIO ()
main = do printLn (the (List Int) [])
          print_raw (the (List Int) [1,2,3,4])
          x <- lists_reverse [1,2,3,4]
          print_raw x

          print_raw "astring"
          print_raw 3
          print_raw 3.54

          print_raw ()

          y <- lists_map (\x => getChar) x
          print_raw y

max_stars_repo_name: lenary/idris-erlang

max_issues_repo_name: yurrriq/idris-erlang

max_forks_repo_name: yurrriq/idris-erlang


text:
module Compiler.Jvm.MockAsm

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

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

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

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

%foreign "jvm:toString(java/lang/Object java/lang/String),java/util/Objects"
prim_objectToString : AnyPtr -> PrimIO String

export
objectToString : a -> String
objectToString value = unsafePerformIO $ primIO (prim_objectToString (believe_me value))

export
mockRunAsm : AsmState -> Asm a -> IO (a, AsmState)
mockRunAsm state Aaload = assemble state $ putStrLn "aaload"
mockRunAsm state Aastore = assemble state $ putStrLn "aastore"
mockRunAsm state Aconstnull = assemble state $ putStrLn "aconstnull"
mockRunAsm state (Aload n) = assemble state $
    putStrLn $ "aload " ++ show n
mockRunAsm state (Anewarray desc) = assemble state $
    putStrLn $ "anewarray " ++ desc
mockRunAsm state Anewintarray     = assemble state $
    putStrLn "anewintarray"
mockRunAsm state Anewbooleanarray = assemble state $
    putStrLn "anewbooleanarray"
mockRunAsm state Anewbytearray    = assemble state $
    putStrLn "anewbytearray"
mockRunAsm state Anewchararray    = assemble state $
    putStrLn "anewchararray"
mockRunAsm state Anewshortarray   = assemble state $
    putStrLn "anewshortarray"
mockRunAsm state Anewlongarray    = assemble state $
    putStrLn "anewlongarray"
mockRunAsm state Anewfloatarray   = assemble state $
    putStrLn "anewfloatarray"
mockRunAsm state Anewdoublearray  = assemble state $
    putStrLn "anewdoublearray"
mockRunAsm state Arraylength      = assemble state $ putStrLn "arraylength"
mockRunAsm state Areturn          = assemble state $ putStrLn "areturn"
mockRunAsm state (Astore n)       = assemble state $
    putStrLn $ "astore " ++ show n
mockRunAsm state Baload           = assemble state $ putStrLn "baload"
mockRunAsm state Bastore          = assemble state $ putStrLn "bastore"
mockRunAsm state Caload           = assemble state $ putStrLn "caload"
mockRunAsm state Castore          = assemble state $ putStrLn "castore"
mockRunAsm state (Checkcast desc) = assemble state $
    putStrLn $ "checkcast " ++ desc
mockRunAsm state (ClassCodeStart version access className sig parent intf anns) = assemble state $
  putStrLn $ unwords [
    "classCodeStart",
    show version,
    show (accessNum access),
    className,
    (fromMaybe "" sig),
    parent]

mockRunAsm state (CreateClass opts) = assemble state $ putStrLn $ "createClass " ++ show opts
mockRunAsm state (CreateField accs sourceFileName className fieldName desc sig fieldInitialValue) = assemble state $ do
  let jaccs = sum $ accessNum <$> accs
  putStrLn $ unwords [
    "createField",
    show jaccs,
    sourceFileName,
    className,
    fieldName,
    desc,
    fromMaybe "" sig,
    (objectToString $ maybeToNullable (toJFieldInitialValue <$> fieldInitialValue))]

mockRunAsm state (CreateLabel label) = assemble state $ pure ()

mockRunAsm state (CreateMethod accs sourceFileName className methodName desc sig exceptions anns paramAnns) =
    let newState = record { currentMethodName = Jqualified className methodName } state
    in assemble newState $ do
        putStrLn $ "**************** " ++ methodName ++ " ******************"
        putStrLn $ unwords [
            "createMethod",
            show accs,
            sourceFileName,
            className,
            methodName,
            desc]

mockRunAsm state (CreateIdrisConstructorClass className isStringConstructor constructorParameterCount) =
    assemble state $ putStrLn ("CreateIdrisConstructorClass " ++ className ++ " " ++
        show isStringConstructor ++ " " ++ show constructorParameterCount)

mockRunAsm state D2i = assemble state $ putStrLn "d2i"
mockRunAsm state D2f = assemble state $ putStrLn "d2f"
mockRunAsm state Dadd = assemble state $ putStrLn "dadd"
mockRunAsm state Dcmpl = assemble state $ putStrLn "dcmpl"
mockRunAsm state Dcmpg = assemble state $ putStrLn "dcmpg"
mockRunAsm state (Dconst n) = assemble state $ putStrLn $ "dconst " ++ show n
mockRunAsm state Daload = assemble state $ putStrLn "daload"
mockRunAsm state Dastore = assemble state $ putStrLn "dastore"
mockRunAsm state Ddiv = assemble state $ putStrLn "ddiv"

mockRunAsm state (Debug message) = assemble state $ putStrLn message

mockRunAsm state (Dload n) =
    assemble state $ putStrLn $ "dload " ++ show n
mockRunAsm state Dmul = assemble state $ putStrLn "dmul"
mockRunAsm state Dneg = assemble state $ putStrLn "dneg"
mockRunAsm state Drem = assemble state $ putStrLn "drem"
mockRunAsm state Dreturn = assemble state $ putStrLn "dreturn"
mockRunAsm state (Dstore n) =
    assemble state $ putStrLn $ "dstore " ++ show n
mockRunAsm state Dsub = assemble state $ putStrLn "dsub"
mockRunAsm state Dup = assemble state $ putStrLn "dup"
mockRunAsm state (Error err) =
    assemble state $ putStrLn $ "error " ++ err
mockRunAsm state F2d = assemble state $ putStrLn "f2d"
mockRunAsm state Faload = assemble state $ putStrLn "faload"
mockRunAsm state Fastore = assemble state $ putStrLn "fastore"
mockRunAsm state (Fconst n) =
    assemble state $ putStrLn $ "fconst " ++ show n
mockRunAsm state (Field finsType cname fname desc) = assemble state $ do
  let finsTypeNum = fieldInsTypeNum finsType
  putStrLn $ unwords [
    "field",
    show finsTypeNum,
    cname,
    fname,
    desc]

mockRunAsm state FieldEnd = assemble state $ putStrLn "fieldEnd"

mockRunAsm state (Fload n) =
    assemble state $ putStrLn $ "fload " ++ show n

mockRunAsm state (Frame frameType nLocal localSigs nStack stackSigs) = assemble state $ do
  let ftypeNum = frameTypeNum frameType
  putStrLn $ unwords [
    "frame",
    show ftypeNum,
    show nLocal,
    show nStack]

mockRunAsm state Freturn = assemble state $ putStrLn "freturn"
mockRunAsm state (Fstore n) =
    assemble state $ putStrLn $ "fstore " ++ show n

mockRunAsm state (Goto label) =
    assemble state $ putStrLn $ "goto " ++ label

mockRunAsm state I2b = assemble state $ putStrLn "i2b"
mockRunAsm state I2c = assemble state $ putStrLn "i2c"
mockRunAsm state I2d = assemble state $ putStrLn "i2d"
mockRunAsm state I2l = assemble state $ putStrLn "i2l"
mockRunAsm state I2s = assemble state $ putStrLn "i2s"
mockRunAsm state Iadd = assemble state $ putStrLn "iadd"
mockRunAsm state Iaload = assemble state $ putStrLn "iaload"
mockRunAsm state Iand = assemble state $ putStrLn "iand"
mockRunAsm state Iastore = assemble state $ putStrLn "iastore"
mockRunAsm state Ior = assemble state $ putStrLn "ior"
mockRunAsm state Ixor = assemble state $ putStrLn "ixor"
mockRunAsm state Icompl = assemble state $ putStrLn "icompl"
mockRunAsm state (Iconst n) = assemble state $ putStrLn $ "iconst " ++ show n
mockRunAsm state Idiv = assemble state $ putStrLn "idiv"
mockRunAsm state (Ifeq label) =
    assemble state $ putStrLn $ "ifeq " ++ label
mockRunAsm state (Ifge label) =
    assemble state $ putStrLn $ "ifge " ++ label
mockRunAsm state (Ifgt label) =
    assemble state $ putStrLn $ "ifgt " ++ label
mockRunAsm state (Ificmpeq label) =
    assemble state $ putStrLn $ "ificmpeq " ++ label
mockRunAsm state (Ificmpge label) =
    assemble state $ putStrLn $ "ificmpge " ++ label
mockRunAsm state (Ificmpgt label) =
    assemble state $ putStrLn $ "ificmpgt " ++ label
mockRunAsm state (Ificmple label) =
    assemble state $ putStrLn $ "ificmple " ++ label
mockRunAsm state (Ificmplt label) =
    assemble state $ putStrLn $ "ificmplt " ++ label
mockRunAsm state (Ificmpne label) =
    assemble state $ putStrLn $ "ificmpne " ++ label
mockRunAsm state (Ifle label) =
    assemble state $ putStrLn $ "ifle " ++ label
mockRunAsm state (Iflt label) =
    assemble state $ putStrLn $ "iflt " ++ label
mockRunAsm state (Ifne label) =
    assemble state $ putStrLn $ "ifne " ++ label
mockRunAsm state (Ifnonnull label) =
    assemble state $ putStrLn $ "ifnonnull " ++ label
mockRunAsm state (Ifnull label) =
    assemble state $ putStrLn $ "ifnull " ++ label
mockRunAsm state (Iload n) =
    assemble state $ putStrLn $ "iload " ++ show n
mockRunAsm state Imul = assemble state $ putStrLn "imul"
mockRunAsm state Ineg = assemble state $ putStrLn "ineg"
mockRunAsm state (InstanceOf className) =
    assemble state $ putStrLn $ "instanceOf " ++ className
mockRunAsm state (InvokeMethod invocType cname mname desc isIntf) = assemble state $ do
  putStrLn $ unwords [
    "invokeMethod",
    show invocType,
    cname,
    mname,
    desc,
    show isIntf]

mockRunAsm state (InvokeDynamic mname desc handle bsmArgs) = assemble state $ do
  jbsmArgs <- sequence $ toJbsmArg <$> bsmArgs
  jhandle <- toJHandle handle
  putStrLn $ unwords [
    "invokeDynamic",
    mname,
    desc,
    (objectToString $ the Object $ believe_me jhandle),
    (objectToString $ the Object $ believe_me jbsmArgs)]

mockRunAsm state Irem = assemble state $ putStrLn "irem"
mockRunAsm state Ireturn = assemble state $ putStrLn "ireturn"
mockRunAsm state Ishl = assemble state $ putStrLn "ishl"
mockRunAsm state Ishr = assemble state $ putStrLn "ishr"
mockRunAsm state (Istore n) = assemble state $
    putStrLn $ "istore " ++ show n
mockRunAsm state Isub = assemble state $ putStrLn "isub"
mockRunAsm state Iushr = assemble state $ putStrLn "iushr"
mockRunAsm state L2i = assemble state $ putStrLn "l2i"
mockRunAsm state (LabelStart label) = assemble state $ putStrLn (label ++ ":")
mockRunAsm state Ladd = assemble state $ putStrLn "ladd"
mockRunAsm state Land = assemble state $ putStrLn "land"
mockRunAsm state Laload = assemble state $ putStrLn "laload"
mockRunAsm state Lastore = assemble state $ putStrLn "lastore"
mockRunAsm state Lor = assemble state $ putStrLn "lor"
mockRunAsm state Lxor = assemble state $ putStrLn "lxor"
mockRunAsm state Lcompl = assemble state $ putStrLn "lcompl"

mockRunAsm state (Ldc (TypeConst ty)) =
    assemble state $ putStrLn $ "ldcType " ++ ty
mockRunAsm state (Ldc constant) = assemble state $ do
    putStrLn ("ldc " ++ (objectToString (constantToObject constant)))

mockRunAsm state Ldiv = assemble state $ putStrLn "ldiv"

mockRunAsm state (LineNumber lineNumber label) = assemble state $
    putStrLn $ unwords [
        "lineNumber",
        show lineNumber,
        label]

mockRunAsm state (Lload n) = assemble state $
    putStrLn $ "lload " ++ show n
mockRunAsm state Lmul = assemble state $ putStrLn "lmul"
mockRunAsm state Lneg = assemble state $ putStrLn "lneg"
mockRunAsm state (LookupSwitch defaultLabel labels cases) = assemble state $ do
  let jcases = integerValueOf <$> cases
  putStrLn $ unwords [
    "lookupSwitch",
    defaultLabel,
    (objectToString (the Object $ believe_me labels)),
    (objectToString (the Object $ believe_me jcases))]

mockRunAsm state (LocalVariable name descriptor signature startLabel endLabel index) = assemble state $
    putStrLn $ unwords [
        "localVariable",
        name,
        descriptor,
        (fromMaybe "null" signature),
        startLabel,
        endLabel,
        show index]

mockRunAsm state Lrem = assemble state $ putStrLn "lrem"
mockRunAsm state Lreturn = assemble state $ putStrLn "lreturn"
mockRunAsm state Lshl = assemble state $ putStrLn "lshl"
mockRunAsm state Lshr = assemble state $ putStrLn "lshr"
mockRunAsm state (Lstore n) = assemble state $
    putStrLn $ "lstore " ++ show n
mockRunAsm state Lsub = assemble state $ putStrLn "lsub"
mockRunAsm state Lushr = assemble state $ putStrLn "lushr"
mockRunAsm state (MaxStackAndLocal stack local) = assemble state $
    putStrLn $ "maxStackAndLocal " ++ show stack ++ " " ++ show local
mockRunAsm state MethodCodeStart = assemble state $
    putStrLn "methodCodeStart"
mockRunAsm state MethodCodeEnd = assemble state $ do
    putStrLn "methodCodeEnd"
    putStrLn $ "***********************************"
mockRunAsm state (Multianewarray desc dims) = assemble state $
    putStrLn $ unwords ["multiANewArray", desc, show dims]
mockRunAsm state (New cname) = assemble state $
    putStrLn $ "asmNew " ++ cname
mockRunAsm state Pop = assemble state $ putStrLn "pop"
mockRunAsm state Pop2 = assemble state $ putStrLn "pop2"
mockRunAsm state Return = assemble state $ putStrLn "voidReturn"
mockRunAsm state Saload = assemble state $ putStrLn "saload"
mockRunAsm state Sastore = assemble state $ putStrLn "sastore"
mockRunAsm state (SourceInfo sourceFileName)
  = assemble state $ putStrLn $ "sourceInfo " ++ sourceFileName
mockRunAsm state (LiftIo action) = assemble state action

mockRunAsm state (Throw fc message) = pure (believe_me $ crash $ show fc ++ ": " ++ message, state)
mockRunAsm state GetState = pure (state, state)
mockRunAsm state (SetState newState) = pure ((), newState)

mockRunAsm st (Pure value) = pure (value, st)
mockRunAsm st (Bind action f) = do
  (result, nextSt) <- mockRunAsm st action
  mockRunAsm nextSt $ f result
mockRunAsm state action = pure (believe_me $ crash "Unsupported action", state)


text:
module Idris.REPLCommon

import Core.Context
import Core.InitPrimitives
import Core.Metadata
import Core.Options
import Core.Unify

import Idris.Error
import Idris.IDEMode.Commands
import public Idris.REPLOpts
import Idris.Syntax
import Idris.Pretty

import Data.List
import Text.PrettyPrint.Prettyprinter
import Text.PrettyPrint.Prettyprinter.Render.Terminal

%default covering

-- Output informational messages, unless quiet flag is set
export
iputStrLn : {auto o : Ref ROpts REPLOpts} ->
            Doc IdrisAnn -> Core ()
iputStrLn msg
    = do opts <- get ROpts
         case idemode opts of
              REPL False => coreLift $ putStrLn !(render msg)
              REPL _ => pure ()
              IDEMode i _ f =>
                send f (SExpList [SymbolAtom "write-string",
                                 toSExp !(renderWithoutColor msg), toSExp i])

printWithStatus : {auto o : Ref ROpts REPLOpts} ->
                  Doc IdrisAnn -> Doc IdrisAnn -> Core ()
printWithStatus status msg
    = do opts <- get ROpts
         case idemode opts of
              REPL _ => coreLift $ putStrLn !(render msg)
              _      => pure () -- this function should never be called in IDE Mode

export
printResult : {auto o : Ref ROpts REPLOpts} ->
              Doc IdrisAnn -> Core ()
printResult msg = printWithStatus (pretty "ok") msg

-- Return that a protocol request failed somehow
export
printError : {auto o : Ref ROpts REPLOpts} ->
             Doc IdrisAnn -> Core ()
printError msg = printWithStatus (pretty "error") msg

-- Display an error message from checking a source file
export
emitError : {auto c : Ref Ctxt Defs} ->
            {auto o : Ref ROpts REPLOpts} ->
            {auto s : Ref Syn SyntaxInfo} ->
            Error -> Core ()
emitError err
    = do opts <- get ROpts
         case idemode opts of
              REPL _ =>
                  do msg <- display err >>= render
                     coreLift $ putStrLn msg
              IDEMode i _ f =>
                  do msg <- perror err
                     case getErrorLoc err of
                          Nothing => iputStrLn msg
                          Just fc =>
                            send f (SExpList [SymbolAtom "warning",
                                   SExpList [toSExp (file fc),
                                            toSExp (addOne (startPos fc)),
                                              toSExp (addOne (endPos fc)),
                                              toSExp !(renderWithoutColor msg),
                                              -- highlighting; currently blank
                                              SExpList []],
                                    toSExp i])
  where
    addOne : (Int, Int) -> (Int, Int)
    addOne (l, c) = (l + 1, c + 1)

export
emitWarning : {auto c : Ref Ctxt Defs} ->
              {auto o : Ref ROpts REPLOpts} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Warning -> Core ()
emitWarning w
    = do opts <- get ROpts
         case idemode opts of
              REPL _ =>
                  do msg <- displayWarning w >>= render
                     coreLift $ putStrLn msg
              IDEMode i _ f =>
                  do msg <- pwarning w
                     case getWarningLoc w of
                          Nothing => iputStrLn msg
                          Just fc =>
                            send f (SExpList [SymbolAtom "warning",
                                   SExpList [toSExp (file fc),
                                            toSExp (addOne (startPos fc)),
                                              toSExp (addOne (endPos fc)),
                                              toSExp !(renderWithoutColor msg),
                                              -- highlighting; currently blank
                                              SExpList []],
                                    toSExp i])
  where
    addOne : (Int, Int) -> (Int, Int)
    addOne (l, c) = (l + 1, c + 1)

export
emitWarnings : {auto c : Ref Ctxt Defs} ->
               {auto o : Ref ROpts REPLOpts} ->
               {auto s : Ref Syn SyntaxInfo} ->
               Core ()
emitWarnings
    = do defs <- get Ctxt
         traverse_ emitWarning (reverse (warnings defs))
         put Ctxt (record { warnings = [] } defs)

getFCLine : FC -> Int
getFCLine fc = fst (startPos fc)

export
updateErrorLine : {auto o : Ref ROpts REPLOpts} ->
                  List Error -> Core ()
updateErrorLine []
    = do opts <- get ROpts
         put ROpts (record { errorLine = Nothing } opts)
updateErrorLine (e :: _)
    = do opts <- get ROpts
         put ROpts (record { errorLine = map getFCLine (getErrorLoc e) } opts)

export
resetContext : {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               {auto s : Ref Syn SyntaxInfo} ->
               {auto m : Ref MD Metadata} ->
               Core ()
resetContext
    = do defs <- get Ctxt
         put Ctxt (record { options = clearNames (options defs) } !initDefs)
         addPrimitives
         put UST initUState
         put Syn initSyntax
         put MD initMetadata


text:
module Data.Tree

%default total
%access public export

||| A key-value tree data structure.
|||
||| This structure doesn't encode the invariants of the tree and is
||| *simply* a container. This structure ideally shouldn't be exposed
||| to the user at all. This structure should be used to build other
||| data structures.  See the modules alongside this for appropriate
||| interfaces for using the tree.
|||
||| @keyTy The type associated with the key.
||| @valTy The type associated with the value.
data Tree : (keyTy : Type)
         -> (valTy : Type)
         -> Type
  where
    ||| An empty Tree node.
    Empty : Tree k v

    ||| A Key Value node in the Tree.
    |||
    ||| @key   The key.
    ||| @val   The value associated with the key.
    ||| @left  The left child of the Node
    ||| @right THe right child of the Node.
    Node : (key   : k)
        -> (val   : v)
        -> (left  : Tree k v)
        -> (right : Tree k v)
        -> Tree k v

%name Tree t, tree

namespace Keys

  ||| A proof that some key is found in a Tree
  data IsKeyIn : k -> Tree k v -> Type where
    Here : IsKeyIn key (Node key _ _ _)
    InRight : (later : IsKeyIn key r) -> IsKeyIn key (Node not_key _ _ r)
    InLeft :  (later : IsKeyIn key l) -> IsKeyIn key (Node not_key _ l _)

  ||| An empty tree has no key
  emptyTreeHasNoKey : {key : k} -> IsKeyIn key Empty -> Void
  emptyTreeHasNoKey Here impossible
  emptyTreeHasNoKey (InRight _) impossible
  emptyTreeHasNoKey (InLeft _) impossible

  Uninhabited (IsKeyIn key Empty) where
    uninhabited = emptyTreeHasNoKey

  ||| An item that is not in the root, not in the left child and not in the
  ||| right child is not in the Tree at all
  noKeyFound : {key : k}
            -> {val : v}
            -> {key' : k}
            -> {l : Tree k v}
            -> {r : Tree k v}
            -> Not (key = key')
            -> Not (IsKeyIn key l)
            -> Not (IsKeyIn key r)
            -> Not (IsKeyIn key (Node key' val l r))
  noKeyFound notHere notInLeft notInRight Here = notHere Refl
  noKeyFound notHere notInLeft notInRight (InLeft later) = notInLeft later
  noKeyFound notHere notInLeft notInRight (InRight later) = notInRight later

  ||| A decision procedure for Key
  isKey : DecEq k
       => (key : k)
       -> (tree : Tree k v)
       -> Dec (IsKeyIn key tree)
  isKey key Empty = No emptyTreeHasNoKey
  isKey key (Node key' _ l r) with (decEq key key')
    isKey key (Node key  _ l r) | (Yes Refl) = Yes Here
    isKey key (Node key' _ l r) | (No notHere) with (isKey key l)
      isKey key (Node key' _ l r) | (No notHere) | (Yes inLeft) = Yes (InLeft inLeft)
      isKey key (Node key' _ l r) | (No notHere) | (No notInLeft) with (isKey key r)
        isKey key (Node key' _ l r) | (No notHere) | (No notInLeft) | (Yes inRight) = Yes (InRight inRight)
        isKey key (Node key' _ l r) | (No notHere) | (No notInLeft) | (No notInRight) = No (noKeyFound notHere notInLeft notInRight)

  public export
  data All : (predicate : typeKey -> Type)
          -> (tree      : Tree typeKey typeValue)
          -> Type
    where
      Leaf : All p Empty
      Node : (prf : p key)
          -> (leftBranch  : All p left)
          -> (rightBranch : All p right)
          -> All p (Node key _ left right)

namespace Values
  public export
  data IsValueIn : (value : typeValue)
                -> (tree  : Tree typeKey typeValue)
                -> Type
    where
      Here    : IsValueIn value (Node _ value _ _)
      InRight : (later : IsValueIn value r) -> IsValueIn value (Node _ not_value _ r)
      InLeft  : (later : IsValueIn value l) -> IsValueIn value (Node _ not_value l _)

  emptyTreeHasNoValue : IsValueIn value Empty -> Void
  emptyTreeHasNoValue Here impossible
  emptyTreeHasNoValue (InRight _) impossible
  emptyTreeHasNoValue (InLeft _) impossible

  Uninhabited (IsValueIn value Empty) where
    uninhabited Here impossible
    uninhabited (InRight _) impossible
    uninhabited (InLeft _) impossible

  ||| A decision procedure for Value
  valueNotFound : (notHere : (value = val) -> Void)
               -> (isNotLeft : IsValueIn value left -> Void)
               -> (isNotRight : IsValueIn value right -> Void)
               -> IsValueIn value (Node key val left right)
               -> Void
  valueNotFound notHere isNotLeft isNotRight Here = notHere Refl
  valueNotFound notHere isNotLeft isNotRight (InRight later) = isNotRight later
  valueNotFound notHere isNotLeft isNotRight (InLeft later) = isNotLeft later

  isValue : DecEq typeValue
         => (value : typeValue)
         -> (tree : Tree typeKey typeValue)
         -> Dec (IsValueIn value tree)
  isValue value Empty = No emptyTreeHasNoValue
  isValue value (Node key val left right) with (decEq value val)
    isValue val (Node key val left right) | (Yes Refl) = Yes Here
    isValue value (Node key val left right) | (No notHere) with (isValue value left)
      isValue value (Node key val left right) | (No notHere) | (Yes prf) = Yes (InLeft prf)
      isValue value (Node key val left right) | (No notHere) | (No isNotLeft) with (isValue value right)
              isValue value (Node key val left right) | (No notHere) | (No isNotLeft) | (Yes prf) = Yes (InRight prf)
              isValue value (Node key val left right) | (No notHere) | (No isNotLeft) | (No isNotRight) = No (valueNotFound notHere isNotLeft isNotRight)

  public export
  data All : (predicate : typeValue -> Type)
          -> (tree      : Tree typeKey typeValue)
          -> Type
    where
      Leaf : Values.All p Empty
      Node : (prf : p value)
          -> (leftBranch  : Values.All p left)
          -> (rightBranch : Values.All p right)
          -> Values.All p (Node _ value left right)

namespace KVPairs
  public export
  data All : (predicate : typeKey -> typeValue -> Type)
          -> (tree      : Tree typeKey typeValue)
          -> Type
    where
      Leaf : KVPairs.All p Empty
      Node : (prf : p key value)
          -> (leftBranch  : KVPairs.All p left)
          -> (rightBranch : KVPairs.All p right)
          -> KVPairs.All p (Node key value left right)


text:
import Control.Monad.Coop
import Control.Monad.State

-------------------------------
--- Preparation for testing ---
-------------------------------

Timed (State $ List String) where
  currentTime = cast <$> length <$> get

-- Awfully inefficient implementation, but will work for small tests.
append : MonadState (List a) m => a -> m ()
append x = modify (++ [x])

exec : Coop (State $ List String) Unit -> List String
exec = execState [] . runCoop

(===) : (Eq a, Show a, HasIO io) => a -> a -> io ()
x === y = if x == y
            then printLn "- [ok]"
            else printLn $ "- [VIOLATION] got " ++ show x ++ " but expected " ++ show y

MonadState st m => MonadState st (Coop m) where
  get = lift get
  put = lift . put

-----------------------
--- Unit test cases ---
-----------------------

main : HasIO io => io ()
main = do
  printLn "test: do nothing"
  (exec $ pure ()) === []

  printLn "test: return time at the start"
  (exec $ currentTime >>= append . show) === ["0"]

  printLn "test: return time at the start and then just a string"
  (exec $ currentTime >>= append . show >>= \() => append "test") === ["0", "test"]

  printLn "test: consequent appends"
  (exec $ append "test1" *> append "test2") === ["test1", "test2"]

  printLn "test: return time after some message"
  (exec $ append "before time" *> currentTime >>= append . show) === ["before time", "1"]

max_stars_repo_name: buzden/idris-arduino-lib

max_issues_repo_name: buzden/idris-arduino-lib

max_forks_repo_name: buzden/idris-arduino-lib


text:
import Data.Nat
import Data.Fin
import Data.Fin.Extra
import Data.Vect
import Data.List
import Data.List1

inf : Nat
inf = 1000000

data Amphipod = A | B | C | D

Eq Amphipod where
  A == A = True
  B == B = True
  C == C = True
  D == D = True
  _ == _ = False

energy : Amphipod -> Nat
energy A = 1
energy B = 10
energy C = 100
energy D = 1000

roomOf : Amphipod -> Fin 4
roomOf A = 0
roomOf B = 1
roomOf C = 2
roomOf D = 3

Room : Nat -> Type
Room n = Vect n (Maybe Amphipod)

roomToHall : Fin 4 -> Fin 11
roomToHall 0 = 2
roomToHall 1 = 4
roomToHall 2 = 6
roomToHall 3 = 8

record State (s : Nat) where
  constructor MkState
  hall : Room 11
  rooms : Vect 4 (Room s)
  energy : Nat

isPod : Amphipod -> Maybe Amphipod -> Bool
isPod a Nothing = False
isPod a (Just b) = a == b

isSolved : State n -> Bool
isSolved (MkState hall [r1,r2,r3,r4] _) =
  all isNothing hall &&
  all (isPod A) r1 &&
  all (isPod B) r2 &&
  all (isPod C) r3 &&
  all (isPod D) r4

validPlaces : Vect 7 (Fin 11)
validPlaces = [0,1,3,5,7,9,10]

moveToHall : State n -> List (State n)
moveToHall s = join $ moveFromRoom <$> (forget $ allFins 3)
  where
    getToMove : Fin 4 -> Maybe (Fin n)
    getToMove r = do let room = index r s.rooms
                     if any (not . (==) r . roomOf) $ catMaybes $ toList room
                        then findIndex isJust room
                        else Nothing

    pathToHall : Fin 4 -> Fin 11 -> Maybe Nat
    pathToHall r to = do let from = finToNat $ roomToHall r
                         let to = finToNat $ to
                         let (min, max) = if from > to
                                             then (to, from)
                                             else (from + 1, to + 1)
                         let dist = minus max min
                         if any isJust $ take dist $ drop min $ toList s.hall
                            then Nothing
                            else Just dist

    moveFromRoom : Fin 4 -> List (State n)
    moveFromRoom r = do case getToMove r of
                          Nothing => []
                          (Just i) => let a = index i $ index r s.rooms
                                          en = maybe 0 energy a
                                          ps = catMaybes $ (\p => (p,) <$> pathToHall r p) <$> toList validPlaces in
                                          ps <&> \(p,n) => {
                                            hall $= replaceAt p a,
                                            rooms $= updateAt r (replaceAt i Nothing),
                                            energy $= (+) (en * (n + (finToNat i) + 1))
                                          } s

moveToRoom : {n : Nat} -> State n -> List (State n)
moveToRoom s = catMaybes $ toList $ moveToRoom' s <$> validPlaces
  where
    pathToRoom : State n -> Fin 11 -> Fin 4 -> Maybe Nat
    pathToRoom s from r = do let to = finToNat $ roomToHall r
                             let from = finToNat $ from
                             let (min, max) = if from > to
                                                 then (to, from)
                                                 else (from + 1, to + 1)
                             let dist = minus max min
                             if any isJust $ take dist $ drop min $ toList s.hall
                                then Nothing
                                else Just dist

    moveInRoom : State n -> Fin 11 -> Fin 4 -> Maybe (Fin n)
    moveInRoom s h r = do let room = index r s.rooms
                          if all ((==) r . roomOf) $ catMaybes $ toList room
                             then do map invFin $ findIndex isNothing $ reverse $ room
                             else Nothing

    moveToRoom' : State n -> Fin 11 -> Maybe (State n)
    moveToRoom' s p = do a <- index p s.hall
                         let r = roomOf a
                         toRoom <- pathToRoom s p r
                         inRoom <- moveInRoom s p r
                         let en = energy a
                         pure $ {
                           hall $= replaceAt p Nothing,
                           rooms $= updateAt r (replaceAt inRoom (Just a)),
                           energy $= (+) (en * (toRoom + (finToNat inRoom) + 1))
                         } s

solve : {n : Nat} -> Nat -> State n -> Nat
solve m s = if s.energy > m
                 then m
                 else if isSolved s
                         then s.energy
                         else let m = foldl solve m (moveToHall s) in
                                  foldl solve m (moveToRoom s)

input1 : Vect 4 (Room 2)
input1 = [
  [Just D, Just C],
  [Just B, Just A],
  [Just C, Just D],
  [Just A, Just B]
  ]

part1 : State 2 -> IO String
part1 a = pure $ show $ solve inf a

input2 : Vect 4 (Room 4)
input2 = [
  [Just D, Just D, Just D, Just C],
  [Just B, Just C, Just B, Just A],
  [Just C, Just B, Just A, Just D],
  [Just A, Just A, Just C, Just B]
  ]

part2 : State 4 -> IO String
part2 a = pure $ show $ solve inf a

main : IO ()
main = do let s1 = MkState (replicate 11 Nothing) input1 0
          part1 s1 >>= putStrLn
          let s2 = MkState (replicate 11 Nothing) input2 0
          part2 s2 >>= putStrLn


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 10

import DataStore

-- check that all functions are total
%default total

testStore : DataStore (SString .+. SString .+. SInt)
testStore = addToStore ("Mercury", "Mariner 10", 1974) $
            addToStore ("Venus", "Venera", 1961) $
            addToStore ("Uranus", "Voyager 2", 1986) $
            addToStore ("Pluto", "New Horizons", 2015) $
            empty

listItems : DataStore schema -> List (SchemaType schema)
listItems input with (storeView input)
  listItems input | SNil = []
  listItems (addToStore value store) | (SAdd rec)
    = value :: listItems store | rec

filterKeys : (test : SchemaType val_schema -> Bool) ->
             DataStore (SString .+. val_schema) -> List String
filterKeys test input with (storeView input)
  filterKeys test input | SNil = []
  filterKeys test (addToStore (key, value) store) | (SAdd rec)
    = if test value
        then key :: filterKeys test store | rec
        else filterKeys test store | rec

getValues : DataStore (SString .+. val_schema) ->
            List (SchemaType val_schema)
getValues input with (storeView input)
  getValues input | SNil = []
  getValues (addToStore (key, value) store) | (SAdd rec)
    = value :: getValues store | rec

testStore2 : DataStore (SString .+. SInt)
testStore2 = addToStore ("First", 1) $
             addToStore ("Second", 2) $
             empty

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Solutions.DPair

import Control.Monad.State

import Data.DPair
import Data.Either
import Data.HList
import Data.List
import Data.List1
import Data.Singleton
import Data.String
import Data.Vect

import Text.CSV

import System.File

%default total

--------------------------------------------------------------------------------
--          Dependent Pairs
--------------------------------------------------------------------------------

-- 1

filterVect : (a -> Bool) -> Vect m a -> (n ** Vect n a)
filterVect f []        = (_ ** [])
filterVect f (x :: xs) = case f x of
  True  => let (_ ** ys) = filterVect f xs in (_ ** x :: ys)
  False => filterVect f xs

-- 2

mapMaybeVect : (a -> Maybe b) -> Vect m a -> (n ** Vect n b)
mapMaybeVect f []        = (_ ** [])
mapMaybeVect f (x :: xs) = case f x of
  Just v  => let (_ ** vs) = mapMaybeVect f xs in (_ ** v :: vs)
  Nothing => mapMaybeVect f xs

-- 3

dropWhileVect : (a -> Bool) -> Vect m a -> Exists (\n => Vect n a)
dropWhileVect f []        = Evidence _ []
dropWhileVect f (x :: xs) = case f x of
  True  => dropWhileVect f xs
  False => Evidence _ (x :: xs)

-- 4

vectLength : Vect n a -> Singleton n
vectLength []        = Val 0
vectLength (x :: xs) = let Val k = vectLength xs in Val (S k)

dropWhileVect' : (a -> Bool) -> Vect m a -> (n ** Vect n a)
dropWhileVect' f xs =
  let Evidence _ ys = dropWhileVect f xs
      Val n         = vectLength ys
   in (n ** ys)

--------------------------------------------------------------------------------
--          Use Case: Nucleic Acids
--------------------------------------------------------------------------------

-- 1

data BaseType = DNABase | RNABase

data Nucleobase' : BaseType -> Type where
  Adenine'  : Nucleobase' b
  Cytosine' : Nucleobase' b
  Guanine'  : Nucleobase' b
  Thymine'  : Nucleobase' DNABase
  Uracile'  : Nucleobase' RNABase

RNA' : Type
RNA' = List (Nucleobase' RNABase)

DNA' : Type
DNA' = List (Nucleobase' DNABase)

Acid1 : Type
Acid1 = (b ** List (Nucleobase' b))

record Acid2 where
  constructor MkAcid2
  baseType : BaseType
  sequence : List (Nucleobase' baseType)

data Acid3 : Type where
  SomeRNA : RNA' -> Acid3
  SomeDNA : DNA' -> Acid3

nb12 : Acid1 -> Acid2
nb12 (fst ** snd) = MkAcid2 fst snd

nb21 : Acid2 -> Acid1
nb21 (MkAcid2 bt seq) = (bt ** seq)

nb13 : Acid1 -> Acid3
nb13 (DNABase ** snd) = SomeDNA snd
nb13 (RNABase ** snd) = SomeRNA snd

nb31 : Acid3 -> Acid1
nb31 (SomeRNA xs) = (RNABase ** xs)
nb31 (SomeDNA xs) = (DNABase ** xs)

-- 2

data Dir = Sense | Antisense

data Nucleobase : BaseType -> Dir -> Type where
  Adenine  : Nucleobase b d
  Cytosine : Nucleobase b d
  Guanine  : Nucleobase b d
  Thymine  : Nucleobase DNABase d
  Uracile  : Nucleobase RNABase d

RNA : Dir -> Type
RNA d = List (Nucleobase RNABase d)

DNA : Dir -> Type
DNA d = List (Nucleobase DNABase d)

-- 3

inverse : Dir -> Dir
inverse Sense     = Antisense
inverse Antisense = Sense

complementBase :  (b : BaseType)
               -> Nucleobase b dir
               -> Nucleobase b (inverse dir)
complementBase DNABase Adenine  = Thymine
complementBase RNABase Adenine  = Uracile
complementBase _       Cytosine = Guanine
complementBase _       Guanine  = Cytosine
complementBase _       Thymine  = Adenine
complementBase _       Uracile  = Adenine

complement :  (b : BaseType)
           -> List (Nucleobase b dir)
           -> List (Nucleobase b $ inverse dir)
complement b = map (complementBase b)

transcribeBase : Nucleobase DNABase Antisense -> Nucleobase RNABase Sense
transcribeBase Adenine  = Uracile
transcribeBase Cytosine = Guanine
transcribeBase Guanine  = Cytosine
transcribeBase Thymine  = Adenine

transcribe : DNA Antisense -> RNA Sense
transcribe = map transcribeBase

transcribeAny : (dir : Dir) -> DNA dir -> RNA Sense
transcribeAny Antisense = transcribe
transcribeAny Sense     = transcribe . complement _

-- 4

record NucleicAcid where
  constructor MkNucleicAcid
  baseType : BaseType
  dir      : Dir
  sequence : List (Nucleobase baseType dir)

-- 5

readAnyBase : {0 dir : _} -> Char -> Maybe (Nucleobase b dir)
readAnyBase 'A' = Just Adenine
readAnyBase 'C' = Just Cytosine
readAnyBase 'G' = Just Guanine
readAnyBase _   = Nothing

readRNABase : {0 dir : _} -> Char -> Maybe (Nucleobase RNABase dir)
readRNABase 'U' = Just Uracile
readRNABase c   = readAnyBase c

readDNABase : {0 dir : _} -> Char -> Maybe (Nucleobase DNABase dir)
readDNABase 'T' = Just Thymine
readDNABase c   = readAnyBase c

readRNA : String -> Maybe (dir : Dir ** RNA dir)
readRNA str = case forget $ split ('-' ==) str of
  ["5´",s,"3´"] => MkDPair Sense     <$> traverse readRNABase (unpack s)
  ["3´",s,"5´"] => MkDPair Antisense <$> traverse readRNABase (unpack s)
  _             => Nothing

readDNA : String -> Maybe (dir : Dir ** DNA dir)
readDNA str = case forget $ split ('-' ==) str of
  ["5´",s,"3´"] => MkDPair Sense     <$> traverse readDNABase (unpack s)
  ["3´",s,"5´"] => MkDPair Antisense <$> traverse readDNABase (unpack s)
  _             => Nothing

-- 6

preSuf : Dir -> (String,String)
preSuf Sense     = ("5´-", "-3´")
preSuf Antisense = ("3´-", "-5´")

encodeBase : Nucleobase c d -> Char
encodeBase Adenine  = 'A'
encodeBase Cytosine = 'C'
encodeBase Guanine  = 'G'
encodeBase Thymine  = 'T'
encodeBase Uracile  = 'U'

encode : (dir : Dir) -> List (Nucleobase b dir) -> String
encode dir seq =
  let (pre,suf) = preSuf dir
   in pre ++ pack (map encodeBase seq) ++ suf

-- 7

public export
data InputError : Type where
  UnknownBaseType : String -> InputError
  InvalidSequence : String -> InputError

readAcid :  (b : BaseType)
         -> String
         -> Either InputError (d ** List $ Nucleobase b d)
readAcid b str =
  let err = InvalidSequence str
   in case b of
        DNABase => maybeToEither err $ readDNA str
        RNABase => maybeToEither err $ readRNA str

toAcid : (b : BaseType) -> (d ** List $ Nucleobase b d) -> NucleicAcid
toAcid b (d ** seq) = MkNucleicAcid b d seq

getNucleicAcid : IO (Either InputError NucleicAcid)
getNucleicAcid = do
  baseString <- getLine
  case baseString of
    "DNA" => map (toAcid _) . readAcid DNABase <$> getLine
    "RNA" => map (toAcid _) . readAcid RNABase <$> getLine
    _     => pure $ Left (UnknownBaseType baseString)

printRNA : RNA Sense -> IO ()
printRNA = putStrLn . encode _

transcribeProg : IO ()
transcribeProg = do
  Right (MkNucleicAcid b d seq) <- getNucleicAcid
    | Left (InvalidSequence str) => putStrLn $ "Invalid sequence: " ++ str
    | Left (UnknownBaseType str) => putStrLn $ "Unknown base type: " ++ str
  case b of
    DNABase => printRNA $ transcribeAny d seq
    RNABase => case d of
      Sense     => printRNA seq
      Antisense => printRNA $ complement _ seq

--------------------------------------------------------------------------------
--          Use Case: CSV Files with a Schema
--------------------------------------------------------------------------------

-- A lot of code was copy-pasted from the chapter's text and is, therefore
-- not very interesting. I tried to annotate the new parts with some hints
-- for better understanding. Also, instead of grouping code by exercise number,
-- I organized it thematically.

--   *** Types ***

-- I used an indexed type here to make sure, data
-- constructor `Optional` takes only non-nullary types
-- as arguments. As noted in exercise 3, having a nesting
-- of nullary types does not make sense without a way to
-- distinguish between a `Nothing` and a `Just Nothing`,
-- both of which would be encoded as the empty string.
-- For `Finite`, we have to add `n` as an argument to the
-- data constructor, so we can use it to decode values
-- of type `Fin n`.
data ColType0 : (nullary : Bool) -> Type where
  I64      : ColType0 b
  Str      : ColType0 b
  Boolean  : ColType0 b
  Float    : ColType0 b
  Natural  : ColType0 b
  BigInt   : ColType0 b
  Finite   : Nat -> ColType0 b
  Optional : ColType0 False -> ColType0 True

-- This is the type used in schemata, where nullary types
-- are explicitly allowed.
ColType : Type
ColType = ColType0 True

Schema : Type
Schema = List ColType

-- The only interesting new parts are the last two
-- lines. They should be pretty self-explanatory.
IdrisType : ColType0 b -> Type
IdrisType I64          = Int64
IdrisType Str          = String
IdrisType Boolean      = Bool
IdrisType Float        = Double
IdrisType Natural      = Nat
IdrisType BigInt       = Integer
IdrisType (Finite n)   = Fin n
IdrisType (Optional t) = Maybe $ IdrisType t

Row : Schema -> Type
Row = HList . map IdrisType

record Table where
  constructor MkTable
  schema : Schema
  size   : Nat
  rows   : Vect size (Row schema)

data Error : Type where
  ExpectedEOI    : (pos : Nat) -> String -> Error
  ExpectedLine   : Error
  InvalidCell    : (row, col : Nat) -> ColType0 b -> String -> Error
  NoNat          : String -> Error
  OutOfBounds    : (size : Nat) -> (index : Nat) -> Error
  ReadError      : (path : String) -> FileError -> Error
  UnexpectedEOI  : (pos : Nat) -> String -> Error
  UnknownCommand : String -> Error
  UnknownType    : (pos : Nat) -> String -> Error
  WriteError     : (path : String) -> FileError -> Error

-- Oh, the type of `Query` is a nice one. :-)
-- `PrintTable`, on the other hand, is trivial.
-- The save and load commands are special: They will
-- already have carried out their tasks after parsing.
-- This allow us to keep `applyCommand` pure.
data Command : (t : Table) -> Type where
  PrintSchema : Command t
  PrintSize   : Command t
  PrintTable  : Command t
  Load        : Table -> Command t
  Save        : Command t
  New         : (newSchema : Schema) -> Command t
  Prepend     : Row (schema t) -> Command t
  Get         : Fin (size t) -> Command t
  Delete      : Fin (size t) -> Command t
  Quit        : Command t
  Query       :  (ix  : Fin (length $ schema t))
              -> (val : IdrisType $ indexList (schema t) ix)
              -> Command t

--   *** Core Functionality ***

-- Compares two values for equality.
eq : (c : ColType0 b) -> IdrisType c -> IdrisType c -> Bool
eq I64          x        y        = x == y
eq Str          x        y        = x == y
eq Boolean      x        y        = x == y
eq Float        x        y        = x == y
eq Natural      x        y        = x == y
eq BigInt       x        y        = x == y
eq (Finite k)   x        y        = x == y
eq (Optional z) (Just x) (Just y) = eq z x y
eq (Optional z) Nothing  Nothing  = True
eq (Optional z) _        _        = False

-- Note: It would have been quite a bit easier to type and
-- implement this, had we used a heterogeneous vector instead
-- of a heterogeneous list for encoding table rows. However,
-- I still think it's pretty cool that this type checks!
eqAt :  (ts  : Schema)
     -> (ix  : Fin $ length ts)
     -> (val : IdrisType $ indexList ts ix)
     -> (row : Row ts)
     -> Bool
eqAt (x :: _)  FZ     val (v :: _)  = eq x val v
eqAt (_ :: xs) (FS y) val (_ :: vs) = eqAt xs y val vs
eqAt []        _      _   _ impossible

-- Most new commands don't change the table,
-- so their cases are trivial. The exception is
-- `Load`, which replaces the table completely.
applyCommand : (t : Table) -> Command t -> Table
applyCommand t                 PrintSchema    = t
applyCommand t                 PrintSize      = t
applyCommand t                 PrintTable     = t
applyCommand t                 Save           = t
applyCommand _                 (Load t')      = t'
applyCommand _                 (New ts)       = MkTable ts _ []
applyCommand (MkTable ts n rs) (Prepend r)    = MkTable ts _ $ r :: rs
applyCommand t                 (Get x)        = t
applyCommand t                 Quit           = t
applyCommand t                 (Query ix val) = t
applyCommand (MkTable ts n rs) (Delete x)  = case n of
  S k => MkTable ts k (deleteAt x rs)
  Z   => absurd x

--   *** Parsers ***

zipWithIndex : Traversable t => t a -> t (Nat, a)
zipWithIndex = evalState 1 . traverse pairWithIndex
  where pairWithIndex : a -> State Nat (Nat,a)
        pairWithIndex v = (,v) <$> get <* modify S

fromCSV : String -> List String
fromCSV = forget . split (',' ==)

-- Reads a primitive (non-nullary) type. This is therefore
-- universally quantified over parameter `b`.
-- The only interesting part is the parsing of `finXYZ`,
-- where we `break` the string at the occurrence of
-- the first digit.
readPrim : Nat -> String -> Either Error (ColType0 b)
readPrim _ "i64"      = Right I64
readPrim _ "str"      = Right Str
readPrim _ "boolean"  = Right Boolean
readPrim _ "float"    = Right Float
readPrim _ "natural"  = Right Natural
readPrim _ "bigint"   = Right BigInt
readPrim n s          =
  let err = Left $ UnknownType n s
   in case break isDigit s of
        ("fin",r) => maybe err (Right . Finite) $ parsePositive r
        _         => err

-- This is the parser for (possibly nullary) column types.
-- A nullary type is encoded as the corresponding non-nullary
-- type with a question mark appended. We therefore first check
-- for the presence of said question mark at the end of the string.
readColType : Nat -> String -> Either Error ColType
readColType n s = case reverse (unpack s) of
  '?' :: t => Optional <$> readPrim n (pack $ reverse t)
  _        => readPrim n s

readSchema : String -> Either Error Schema
readSchema = traverse (uncurry readColType) . zipWithIndex . fromCSV

readSchemaList : List String -> Either Error Schema
readSchemaList [s] = readSchema s
readSchemaList _   = Left ExpectedLine

-- For all except nullary types we can just use the `CSVField`
-- implementation for reading values.
-- For values of nullary types, we treat the empty string specially.
decodeF : (c : ColType0 b) -> String -> Maybe (IdrisType c)
decodeF I64          s  = read s
decodeF Str          s  = read s
decodeF Boolean      s  = read s
decodeF Float        s  = read s
decodeF Natural      s  = read s
decodeF BigInt       s  = read s
decodeF (Finite k)   s  = read s
decodeF (Optional y) "" = Just Nothing
decodeF (Optional y) s  = Just <$> decodeF y s

decodeField : (row,col : Nat) -> (c : ColType0 b) -> String -> Either Error (IdrisType c)
decodeField row k c s = maybeToEither (InvalidCell row k c s) $ decodeF c s

decodeRow : {ts : _} -> (row : Nat) -> String -> Either Error (Row ts)
decodeRow row s = go 1 ts $ fromCSV s
  where go : Nat -> (cs : Schema) -> List String -> Either Error (Row cs)
        go k []       []         = Right []
        go k []       (_ :: _)   = Left $ ExpectedEOI k s
        go k (_ :: _) []         = Left $ UnexpectedEOI k s
        go k (c :: cs) (s :: ss) = [| decodeField row k c s :: go (S k) cs ss |]

decodeRows : {ts : _} -> List String -> Either Error (List $ Row ts)
decodeRows = traverse (uncurry decodeRow) . zipWithIndex

readFin : {n : _} -> String -> Either Error (Fin n)
readFin s = do
  S k <- maybeToEither (NoNat s) $ parsePositive {a = Nat} s
    | Z => Left $ OutOfBounds n Z
  maybeToEither (OutOfBounds n $ S k) $ natToFin k n

readCommand :  (t : Table) -> String -> Either Error (Command t)
readCommand _                "schema"  = Right PrintSchema
readCommand _                "size"    = Right PrintSize
readCommand _                "table"   = Right PrintTable
readCommand _                "quit"    = Right Quit
readCommand (MkTable ts n _) s         = case words s of
  ["new",    str]    => New     <$> readSchema str
  "add" ::   ss      => Prepend <$> decodeRow 1 (unwords ss)
  ["get",    str]    => Get     <$> readFin str
  ["delete", str]    => Delete  <$> readFin str
  "query" :: n :: ss => do
    ix  <- readFin n
    val <- decodeField 1 1 (indexList ts ix) (unwords ss)
    pure $ Query ix val
  _                  => Left $ UnknownCommand s

--   *** Printers ***

toCSV : List String -> String
toCSV = concat . intersperse ","

-- We mark optional type by appending a question
-- mark after the corresponding non-nullary type.
showColType : ColType0 b -> String
showColType I64          = "i64"
showColType Str          = "str"
showColType Boolean      = "boolean"
showColType Float        = "float"
showColType Natural      = "natural"
showColType BigInt       = "bigint"
showColType (Finite n)   = "fin\{show n}"
showColType (Optional t) = showColType t ++ "?"

-- Again, only nullary values are treated specially. This
-- is another case of a dependent pattern match: We use
-- explicit pattern matches on the value to encode based
-- on the type calculated from the `ColType0 b` parameter.
-- There are few languages capable of expressing this as
-- cleanly as Idris does.
encodeField : (t : ColType0 b) -> IdrisType t -> String
encodeField I64          x        = show x
encodeField Str          x        = x
encodeField Boolean      True     = "t"
encodeField Boolean      False    = "f"
encodeField Float        x        = show x
encodeField Natural      x        = show x
encodeField BigInt       x        = show x
encodeField (Finite k)   x        = show x
encodeField (Optional y) (Just v) = encodeField y v
encodeField (Optional y) Nothing  = ""

encodeFields : (ts : Schema) -> Row ts -> Vect (length ts) String
encodeFields []        []        = []
encodeFields (c :: cs) (v :: vs) = encodeField c v :: encodeFields cs vs

encodeTable : Table -> String
encodeTable (MkTable ts _ rows) =
  unlines . toList $ map (toCSV . toList . encodeFields ts) rows

encodeSchema : Schema -> String
encodeSchema = toCSV . map showColType

-- Pretty printing a table plus header. All cells are right-padded
-- with spaces to adjust their size to the cell with the longest
-- entry for each colum.
-- Value `ls` is a `Vect n Nat` holding these lengths.
-- Here is an example of how the output looks like:
--
-- fin100 | boolean | natural | str         | bigint?
-- --------------------------------------------------
-- 88     | f       | 10      | stefan      |
-- 13     | f       | 10      | hock        | -100
-- 58     | t       | 1000    | hello world | -1234
--
-- Ideally, numeric values would be right-aligned, but since this
-- whole exercise is already quite long and complex, I refrained
-- from adding this luxury.
prettyTable :  {n : _}
            -> (header : Vect n String)
            -> (table  : Vect m (Vect n String))
            -> String
prettyTable h t =
  let -- vector holding the maximal length of each column
      ls  = foldl (zipWith $ \k => max k . length) (replicate n Z) (h::t)

      -- horizontal bar used to separate the header from the rows
      bar = concat . intersperse "---" $ map (`replicate` '-') ls
   in unlines . toList $ line ls h :: bar :: map (line ls) t

  where pad : Nat -> String -> String
        pad v = padRight v ' '

        -- given a vector of lengths, pads each string to the
        -- desired length, separating cells with a vertical bar.
        line : Vect n Nat -> Vect n String -> String
        line lengths = concat . intersperse " | " . zipWith pad lengths

printTable :  (cs   : List ColType)
           -> (rows : Vect n (Row cs))
           -> String
printTable cs rows =
  let header  = map showColType $ fromList cs
      table   = map (encodeFields cs) rows
   in prettyTable header table

allTypes : String
allTypes = concat
         . List.intersperse ", "
         . map (showColType {b = True})
         $ [I64,Str,Boolean,Float]

showError : Error -> String
showError ExpectedLine = """
  Error when reading schema.
  Expected a single line of content.
  """

showError (UnknownCommand x) = """
  Unknown command: \{x}.
  Known commands are: clear, schema, size, table, new, add, get, delete, quit.
  """

showError (UnknownType pos x) = """
  Unknown type at position \{show pos}: \{x}.
  Known types are: \{allTypes}.
  """

showError (InvalidCell row col tpe x) = """
  Invalid value at row \{show row}, column \{show col}.
  Expected type: \{showColType tpe}.
  Value found: \{x}.
  """

showError (ExpectedEOI k x) = """
  Expected end of input.
  Position: \{show k}
  Input: \{x}
  """

showError (UnexpectedEOI k x) = """
  Unxpected end of input.
  Position: \{show k}
  Input: \{x}
  """

showError (OutOfBounds size index) = """
  Index out of bounds.
  Size of table: \{show size}
  Index: \{show index}
  Note: Indices start at zero.
  """

showError (WriteError path err) = """
  Error when writing file \{path}.
  Message: \{show err}
  """

showError (ReadError path err) = """
  Error when reading file \{path}.
  Message: \{show err}
  """

showError (NoNat x) = "Not a natural number: \{x}"

result :  (t : Table) -> Command t -> String
result t PrintSchema    = "Current schema: \{encodeSchema t.schema}"
result t PrintSize      = "Current size: \{show t.size}"
result t PrintTable     = "Table:\n\n\{printTable t.schema t.rows}"
result _ Save           = "Table written to disk."
result _ (Load t)       = "Table loaded. Schema: \{encodeSchema t.schema}"
result _ (New ts)       = "Created table. Schema: \{encodeSchema ts}"
result t (Prepend r)    = "Row prepended:\n\n\{printTable t.schema [r]}"
result _ (Delete x)     = "Deleted row: \{show $ FS x}."
result _ Quit           = "Goodbye."
result t (Query ix val) =
  let (_ ** rs) = filter (eqAt t.schema ix val) t.rows
   in "Result:\n\n\{printTable t.schema rs}"
result t (Get x)        =
  "Row \{show $ FS x}:\n\n\{printTable t.schema [index x t.rows]}"

--   *** File IO ***

-- We use partial function `readFile` for simplicity here.
partial
load :  (path   : String)
     -> (decode : List String -> Either Error a)
     -> IO (Either Error a)
load path decode = do
  Right ls <- readFile path
    | Left err        => pure $ Left (ReadError path err)
  pure $ decode (filter (not . null) $ lines ls)

write : (path : String) -> (content : String) -> IO (Either Error ())
write path content = mapFst (WriteError path) <$> writeFile path content

namespace IOEither
  export
  (>>=) : IO (Either err a) -> (a -> IO (Either err b)) -> IO (Either err b)
  ioa >>= f = Prelude.(>>=) ioa (either (pure . Left) f)

  export
  (>>) : IO (Either err ()) -> IO (Either err a) -> IO (Either err a)
  (>>) x y = x >>= const y

  export
  pure : a -> IO (Either err a)
  pure = Prelude.pure . Right

partial
readCommandIO : (t : Table) -> String -> IO (Either Error (Command t))
readCommandIO t s = case words s of
  ["save", pth] => IOEither.do
    write (pth ++ ".schema") (encodeSchema t.schema)
    write (pth ++ ".csv") (encodeTable t)
    pure Save

  ["load", pth] => IOEither.do
    schema <- load (pth ++ ".schema") readSchemaList
    rows   <- load (pth ++ ".csv") (decodeRows {ts = schema})
    pure . Load $ MkTable schema (length rows) (fromList rows)

  _ => Prelude.pure $ readCommand t s

--   *** Main Loop ***

partial
runProg : Table -> IO ()
runProg t = do
  putStr "Enter a command: "
  str <- getLine
  cmd <- readCommandIO t str
  case cmd of
    Left err   => putStrLn (showError err) >> runProg t
    Right Quit => putStrLn (result t Quit)
    Right cmd  => putStrLn (result t cmd) >>
                  runProg (applyCommand t cmd)

partial
main : IO ()
main = runProg $ MkTable [] _ []


text:
module Ch05.Exercise_5_2_4

import Ch05.LambdaCalculus

%default total

||| `pow m n` is `m` raised to the power `n`
pow : Term
pow = Abs 0 (Abs 1 ((Var 1) . (times . (Var 0))) . church_one)

max_stars_repo_name: mr-infty/tapl

max_issues_repo_name: mr-infty/tapl

max_forks_repo_name: mr-infty/tapl


text:
module ReadVect

import Data.Vect

data VectUnknown : Type -> Type where
     MkVect : (len : Nat) -> Vect len a -> VectUnknown a

readVectLen : (len : Nat) -> IO (Vect len String)
readVectLen Z = pure []
readVectLen (S k) = do s <- getLine
                       rest <- readVectLen k
                       pure (s :: rest)

-- Personal blind attempt #1 to build a readVectUnknownLen function using DPair
readVectUnknownLenAttempt1 : IO (l : Nat ** Vect l String)
readVectUnknownLenAttempt1 = do n <- putStrLn "How many vects?" >>= \_ => getLine
                                v <- readVectLen (cast n)
                                pure $ ((cast n) ** v)

-- Personal blind attempt #2 to build a readVectUnknownLen function with tail recursion & DPairs
-- Sucess, though a little verbose
readVectUnknownLenAttempt2 : IO (l : Nat ** Vect l String)
readVectUnknownLenAttempt2 = go $ pure $ MkDPair _ []
                            where go : IO (l : Nat ** Vect l String) -> IO (n : Nat ** Vect n String)
                                  go iocdp = do inp <- getLine
                                                cdp <- iocdp
                                                case inp /= "" of
                                                    False => iocdp
                                                    True => go $ pure $ MkDPair _ ((snd cdp) ++ [inp])

readVect : IO (VectUnknown String)
readVect = do inp <- getLine
              case inp /= "" of
                   False => pure (MkVect _ [])
                   True => do MkVect _ xs <- readVect
                              pure $ MkVect _ (inp :: xs)

printVect : Show a => VectUnknown a -> IO ()
printVect (MkVect l xs) = putStrLn (show xs ++ " (length " ++ show l ++ ")")

readVectUnknownLen : IO (len ** Vect len String)
readVectUnknownLen = do inp <- getLine
                        if (inp == "")
                           then pure (_ ** [])
                           else do (_ ** xs) <- readVectUnknownLen
                                   pure (_ ** inp :: xs)

zipInputs : IO ()
zipInputs = do putStrLn "Input first vector: "
               (l1 ** v1) <- readVectUnknownLen
               putStrLn "Input second vector: "
               (l2 ** v2) <- readVectUnknownLen
               case exactLength l1 v2 of
                    Nothing => putStrLn "Error: The two vectors are different sizes"
                    (Just cv2) => putStrLn $ show $ Data.Vect.zip v1 cv2

readToBlank : IO (List String)
readToBlank = do inp <- getLine
                 case inp /= "" of
                      False => pure []
                      True => do sl <- readToBlank
                                 pure (inp :: sl)

readAndSave : IO ()
readAndSave = do inps <- concat <$> readToBlank
                 writeFile "ras.txt" inps
                 pure ()

parseFile : (r : File) -> IO (n : Nat ** Vect n String)
parseFile f = do isEOF <- fEOF f
                 case isEOF of
                      True => pure $ MkDPair _ []
                      False => do Right l <- fGetLine f | Left err => pure (_ ** [])
                                  MkDPair _ xs <- parseFile f
                                  pure (MkDPair _ (l :: xs))

readVectFile : (filename : String) -> IO (n ** Vect n String)
readVectFile filename = do Right f <- openFile "ras.txt" Read | Left err => pure (MkDPair _ [])
                           parseFile f


text:
module System.Bindings.LibUSB.Decriptors

import System.Bindings.LibUSB.Data
import System.Bindings.LibUSB.Devices

data UsbClass = PerInterface
              | Audio
              | Comm
              | HID
              | Physical
              | Printer
              | PTP
              | Image
              | MassStorage
              | Data
              | SmartCard
              | ContentSecurity
              | Video
              | PersonalHealthCare
              | DiagnosticDevice
              | Wireless
              | Application
              | VendorSpec

-- int  libusb_get_device_descriptor (libusb_device *dev, struct libusb_device_descriptor *desc)
-- int   libusb_get_active_config_descriptor (libusb_device *dev, struct libusb_config_descriptor **config)
-- int   libusb_get_config_descriptor (libusb_device *dev, uint8_t config_index, struct libusb_config_descriptor **config)
-- int   libusb_get_config_descriptor_by_value (libusb_device *dev, uint8_t bConfigurationValue, struct libusb_config_descriptor **config)
-- void  libusb_free_config_descriptor (struct libusb_config_descriptor *config)

-- int   libusb_get_string_descriptor_ascii (libusb_device_handle *dev, uint8_t desc_index, unsigned char *data, int length)
libusb_get_string_descriptor_ascii : DeviceHandle -> Bits8 -> Buffer -> IO Int
libusb_get_string_descriptor_ascii (MkDeviceHandle h) i (MkBuffer s b) =
  mkForeign (FFun "libusb_get_string_descriptor_ascii" [FPtr, FBits8, FPtr, FInt] FInt) h i b (fromNat s)

libusb_get_string_descriptor' : DeviceHandle -> Bits8 -> IO String
libusb_get_string_descriptor' h i = do
  b <- allocate 256
  r <- libusb_get_string_descriptor_ascii h i b
  s <- string_from_buffer b
  free b
  return s

-- static int  libusb_get_descriptor (libusb_device_handle *dev, uint8_t desc_type, uint8_t desc_index, unsigned char *data, int length)
--static int  libusb_get_string_descriptor (libusb_device_handle *dev, uint8_t desc_index, uint16_t langid, unsigned char *data, int length)

max_stars_repo_name: idris-hackers/usb

max_issues_repo_name: idris-hackers/usb

max_forks_repo_name: idris-hackers/usb


text:
module Main

import IdrisJvm.FFI
import IdrisJvm.IO

%access public export

-- Returning an additional Nat to test that `par` returns a complex type correctly
fibonacci : Integer -> (Nat, Integer)
fibonacci 0 = (0, 0)
fibonacci 1 = (1, 1)
fibonacci n =
  let (fibNat1, fib1) = par $ fibonacci (n - 1) -- Evaluate in parallel using Java's ForkJoin
      (fibNat2, fib2) = par $ fibonacci (n - 2) -- Evaluate in parallel
      fibNat = fibNat1 + fibNat2
  in (fibNat * 2, fib1 + fib2)

TimeUnitClass : JVM_NativeTy
TimeUnitClass = Class "java/util/concurrent/TimeUnit"

TimeUnit : Type
TimeUnit = JVM_Native TimeUnitClass

ConcurrentClass : JVM_NativeTy
ConcurrentClass = Class "io/github/mmhelloworld/idrisjvm/runtime/Concurrent"

seconds : TimeUnit
seconds = unsafePerformIO $ getStaticField TimeUnitClass "SECONDS" (JVM_IO TimeUnit)

shutdownExecutor : JVM_IO ()
shutdownExecutor = invokeStatic ConcurrentClass "shutdownExecutor" (JVM_IO ())

awaitTermination : Bits64 -> TimeUnit -> JVM_IO ()
awaitTermination = invokeStatic ConcurrentClass "executorAwaitTermination" (Bits64 -> TimeUnit -> JVM_IO ())

main : JVM_IO ()
main = do
  fork $ printLn "a" -- Run in a new thread using Java's ExecutorService
  fork $ printLn "b" -- Run in another thread
  fork $ printLn $ fibonacci 10
  fork $ printLn "cde"
  fork $ printLn "fg"
  printLn "h"
  shutdownExecutor
  awaitTermination 5 seconds


text:
foo : String
foo = "ällo"

ällo : Int
ällo = 42

main : IO ()
main = do printLn ällo
          putStrLn "ällo"
          putStrLn "Clef: 𝄞"
          putStrLn "Snowman: ☃"
          putStrLn "Wikipedia: $¢ह€한𐍈"

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
%default partial

onlyOne : Int -> Int
onlyOne 1 = 2

covered : Int -> Int
covered 1 = 2
covered 2 = 3
covered _ = 94

data IntNat : Integer -> Nat -> Type where
     IsZero : IntNat 0 Z
     IsSuc : IntNat 1 (S k)

-- Only identified as covering if 'x' has multiplicity 0 because then it
-- doesn't show up in the case tree!
matchInt : (0 x : Integer) -> (n : Nat) -> IntNat x n -> String
matchInt 0 Z IsZero = "Zero"
matchInt 1 (S k) IsSuc = "Non Zero"

-- Should be identified as covering but isn't yet since the checker requires
-- a catch all case. This does at least test that the declared 'impossible'
-- case really is impossible; we can update it when the checker improves!
matchInt' : (x : Integer) -> (n : Nat) -> IntNat x n -> String
matchInt' 0 Z IsZero = "Zero"
matchInt' 1 (S k) IsSuc = "Non Zero"
matchInt' 0 (S k) x impossible


text:
import Data.Vect

readVectLen : (len : Nat) -> IO (Vect len String)
readVectLen Z = pure []
readVectLen (S k) = do x <- getLine
                       xs <- readVectLen k
                       pure (x :: xs)

data VectUnknown : Type -> Type where
  MkVect : (len : Nat) -> Vect len a -> VectUnknown a

readVect : IO (VectUnknown String)
readVect = do x <- getLine
              if (x == "")
                 then pure (MkVect _ [])
                 else do MkVect _ xs <- readVect
                         pure (MkVect _ (x :: xs))

printVect : Show a => VectUnknown a -> IO ()
printVect (MkVect len xs) = putStrLn (show xs ++ " (length " ++ show len ++ ")")

readVectDep : IO (len ** Vect len String)
readVectDep = do x <- getLine
                 if (x == "")
                    then pure (_ ** [])
                    else do (_ ** xs) <- readVectDep
                            pure (_ ** x :: xs)


text:
module Circuits.NetList.Check

import Decidable.Equality

import Data.Nat
import Data.String
import Data.List.Elem
import Data.List.Quantifiers
import Data.Fin

import Toolkit.Decidable.Informative

import Toolkit.Data.Location
import Toolkit.Data.Whole
import Toolkit.Data.List.DeBruijn

import Ref

import Circuits.NetList.Types
import Circuits.NetList.Terms
import Circuits.NetList.AST

%default total

data Entry : (String,Ty) -> Type where
  MkEntry : (name : String)
         -> (type : Ty)
                 -> Entry (MkPair name type)

Env : List (String,Ty) -> Type
Env = Env (String,Ty) Entry

export
data Error = Mismatch Ty Ty
           | MismatchD DType DType
           | NotBound String
           | VectorExpected
           | PortChanExpected
           | PortExpected
           | OOB Nat Nat
           | ErrI String
           | Err FileContext Error
export
Show Error where
  show (Mismatch x y)
    = "Type Mismatch:\n\n"
      <+>
      unlines [unwords ["\tExpected:",show x], unwords ["\tGiven:", show y]]

  show (MismatchD x y)
    = "Type Mismatch:\n\n"
      <+>
      unlines [unwords ["\tExpected:",show x], unwords ["\tGiven:", show y]]

  show (NotBound x)
    = unwords ["Undeclared variable:", x]

  show (VectorExpected)
    = "Vector Expected"

  show (PortChanExpected)
    = "Port or Wire Expected"

  show (PortExpected)
    = "Port Expected"

  show (ErrI msg)
    = "Internal Err: " <+> msg
  show (OOB x y)
    = unwords ["Out of Bounds:" , show x, "is not within", show y]

  show (Err x y) = unwords [show x, show y]

strip : {ctxt : List (String, Ty)}
     -> Elem (s,type) ctxt -> Elem type (map Builtin.snd ctxt)
strip Here = Here
strip (There x) = There (strip x)

public export
TyCheck : Type -> Type
TyCheck = Either Error

lift : Dec a -> Error -> TyCheck a
lift (Yes prf) _ = Right prf
lift (No contra) e = Left e

namespace Elab

  export
  getDataType : FileContext
             -> (term : (type ** Term ctxt type))
                     -> TyCheck DType
  getDataType fc (MkDPair (TyPort (d,x)) snd) = pure x
  getDataType fc (MkDPair (TyChan x) snd) = pure x
  getDataType fc (MkDPair type snd)
    = Left (Err fc PortChanExpected)

  ||| Need to make sure that the indices are in the correct direction.
  rewriteTerm : Cast flow expected
             -> Index INOUT
             -> Term ctxt (TyPort (flow,type))
             -> Term ctxt (TyPort (flow,type))
  rewriteTerm c d (Var prf) = Var prf

  rewriteTerm BI (UP UB) (Index idir what idx)
    = Index (UP UB) (rewriteTerm BI (UP UB) what) idx

  rewriteTerm BI (DOWN DB) (Index idir what idx)
    = Index (DOWN DB) (rewriteTerm BI (DOWN DB) what) idx

  rewriteTerm BO (UP UB) (Index idir what idx)
    = Index (UP UB) (rewriteTerm BI (UP UB) what) idx

  rewriteTerm BO (DOWN DB) (Index idir what idx)
    = Index (DOWN DB) (rewriteTerm BI (DOWN DB) what) idx

  rewriteTerm BI _ (Project WRITE _) impossible
  rewriteTerm BO _ (Project WRITE _) impossible
  rewriteTerm BI _ (Project READ _) impossible
  rewriteTerm BO _ (Project READ _) impossible

  rewriteTerm BI _ (Cast BI _) impossible
  rewriteTerm BO _ (Cast BI _) impossible
  rewriteTerm BI _ (Cast BO _) impossible
  rewriteTerm BO _ (Cast BO _) impossible

  ||| When casting we finally know which direction indexing should go, so lets fix that.
  shouldCast : {type : DType}
            -> (flow,expected : Direction)
            -> (term : Term ctxt (TyPort (flow,type)))
                    -> Dec ( Cast flow expected
                           , Term ctxt (TyPort (expected,type))
                           )
  shouldCast flow expected term with (Cast.cast flow expected)
    shouldCast INOUT INPUT term | (Yes BI) with (dirFromCast BI)
      shouldCast INOUT INPUT term | (Yes BI) | idir
        = Yes $ MkPair BI (Cast BI (rewriteTerm BI idir term))

    shouldCast INOUT OUTPUT term | (Yes BO) with (dirFromCast BO)
      shouldCast INOUT OUTPUT term | (Yes BO) | idir
        = Yes $ MkPair BO (Cast BO (rewriteTerm BO idir term))

    shouldCast flow expected term | (No contra)
      = No (\(prf,t) => contra prf)

  portCast : {type : DType}
        -> {flow : Direction}
        -> FileContext
        -> (expected : Direction)
        -> (term : Term ctxt (TyPort (flow,type)))
                -> TyCheck (Term ctxt (TyPort (expected,type)))

  portCast {type} {flow = flow} fc exp term with (shouldCast flow exp term)
    portCast {type} {flow = flow} fc exp term | Yes (p,e)
      = Right e
    portCast {type} {flow = flow} fc exp term | No contra with (decEq flow exp)
      portCast {type} {flow = exp} fc exp term | No contra | (Yes Refl)
        = Right term
      portCast {type} {flow = flow} fc exp term | No contra | (No f)
        = Left (Err fc (Mismatch (TyPort (exp,type)) (TyPort (flow,type))))

  export
  checkPort : (fc    : FileContext)
           -> (exdir : Direction)
           -> (expty : DType)
           -> (term  : (type ** Term ctxt type))
                    -> TyCheck (Term ctxt (TyPort (exdir,expty)))

  -- [ NOTE ]
  --
  checkPort fc exdir exty (MkDPair (TyPort (given,x)) term)
    = do Refl <- lift (decEq exty x)
                      (Err fc (MismatchD exty x))

         portCast fc exdir term

  -- [ NOTE ]
  --
  -- READ implies INPUT
  checkPort fc INPUT exty (MkDPair (TyChan x) term)
    = do Refl <- lift (decEq exty x)
                      (Err fc (MismatchD exty x))

         pure (Project READ term)

  -- [ NOTE ]
  --
  -- WRITE implies OUTPUT
  checkPort fc OUTPUT exty (MkDPair (TyChan x) term)
    = do Refl <- lift (decEq exty x)
                      (Err fc (MismatchD exty x))

         Right (Project WRITE term)

  -- [ NOTE ]
  --
  -- INOUT Chan's impossible.
  checkPort fc INOUT exty (MkDPair (TyChan x) term)
     = Left (Err fc (ErrI "INOUT CHAN not expected"))

  -- [ NOTE ]
  --
  -- Gates/TyUnit not expected
  checkPort fc exdir exty (MkDPair type term)
     = Left (Err fc (Mismatch (TyPort (exdir,exty)) type))

  export
  indexDir : {flow : Direction}
          -> (fc   : FileContext)
          -> (term : Term ctxt (TyPort (flow,BVECT (W (S n) ItIsSucc) type)))
                  -> TyCheck (Index flow)
  indexDir {flow} fc term with (flow)
    indexDir {flow = flow} fc term | INPUT
      = pure (DOWN DI)
    indexDir {flow = flow} fc term | OUTPUT
      = pure (UP UO)
    indexDir {flow = flow} fc (Var prf) | INOUT
      = pure (UP UB)
    indexDir {flow = flow} fc (Index idir what idx) | INOUT
      = pure idir
    indexDir {flow = flow} fc (Project how what) | INOUT
      = Left (Err fc (ErrI "Shouldn't happen impossible indexing a projection with inout"))
    indexDir {flow = flow} fc (Cast x what) | INOUT
      = Left (Err fc (ErrI "Shouldn't happen impossible indexing a cast with inout"))

namespace TypeCheck
  export
  typeCheck : {ctxt : List (String,Ty)}
           -> (curr : Env ctxt)
           -> (ast  : AST)
                    -> TyCheck (DPair Ty (Term (map Builtin.snd ctxt)))

  typeCheck {ctxt} curr (Var x)
    = do (ty ** prf) <- lift (isIndex (get x) ctxt)
                             (Err (span x) (NotBound (get x)))

         pure (ty ** Var (strip prf))

  typeCheck curr (Port fc flow ty n body)
    = do (TyUnit ** term) <- typeCheck (MkEntry (get n) (TyPort (flow,ty))::curr) body
           | (type ** _) => Left (Err fc (Mismatch TyUnit type))

         pure (_ ** Port flow ty term)

  typeCheck curr (Wire fc ty n body)
    = do (TyUnit ** term) <- typeCheck (MkEntry (get n) (TyChan ty)::curr) body
           | (type ** _) => Left (Err fc (Mismatch TyUnit type))

         pure (_ ** Wire ty term)

  typeCheck curr (GateDecl fc n g body)
    = do (TyGate ** gate) <- typeCheck curr g
           | (type ** _) => Left (Err fc (Mismatch TyGate type))

         (TyUnit ** term) <- typeCheck (MkEntry (get n) (TyGate)::curr) body
           | (type ** _) => Left (Err fc (Mismatch TyUnit type))

         pure (_ ** GateDecl gate term)

  typeCheck curr (Assign fc i o rest)
    =  do termI <- typeCheck curr i

          ity <- getDataType fc termI

          termO <- typeCheck curr o
          oty <- getDataType fc termO

          Refl <- lift (decEq ity oty)
                       (Err fc (MismatchD ity oty))

          i' <- checkPort fc INPUT  ity termI
          o' <- checkPort fc OUTPUT ity termO

          (TyUnit ** r') <- typeCheck curr rest
           | (type ** _) => Left (Err fc (Mismatch TyUnit type))

          pure (_ ** Assign i' o' r')

  typeCheck curr (Mux fc o c l r)
    = do termO <- typeCheck curr o
         termC <- typeCheck curr c
         termL <- typeCheck curr l
         termR <- typeCheck curr r

         o' <- checkPort fc OUTPUT LOGIC termO
         c' <- checkPort fc INPUT  LOGIC termC
         l' <- checkPort fc INPUT  LOGIC termL
         r' <- checkPort fc INPUT  LOGIC termR

         pure (_ ** Mux o' c' l' r')

  typeCheck curr (GateU fc k o i)
    = do termO <- typeCheck curr o
         termI <- typeCheck curr i

         o' <- checkPort fc OUTPUT LOGIC termO
         i' <- checkPort fc INPUT  LOGIC termI

         pure (_ ** GateU k o' i')

  typeCheck curr (GateB fc k o l r)

    = do termO <- typeCheck curr o
         termL <- typeCheck curr l
         termR <- typeCheck curr r

         o' <- checkPort fc OUTPUT LOGIC termO
         l' <- checkPort fc INPUT  LOGIC termL
         r' <- checkPort fc INPUT  LOGIC termR

         pure (_ ** GateB k o' l' r')

  typeCheck curr (Index fc idx t)

    = do (TyPort (flow,BVECT (W (S n) ItIsSucc) type) ** term) <- typeCheck curr t
           | (type ** term)
               => Left (Err fc VectorExpected)

         case natToFin idx (S n) of
           Nothing => Left (OOB idx (S n))
           Just idx' => do idir <- indexDir fc term
                           pure (_ ** Index idir term idx')

  typeCheck curr (Split fc a b i)

    = do termA <- typeCheck curr a
         termB <- typeCheck curr b
         termI <- typeCheck curr i

         a' <- checkPort fc OUTPUT LOGIC termA
         b' <- checkPort fc OUTPUT LOGIC termB
         i' <- checkPort fc INPUT  LOGIC termI

         pure (_ ** Split a' b' i')

  typeCheck curr (Collect fc o l r)
    = do (TyPort (OUTPUT,BVECT (W (S (S Z)) ItIsSucc) type) ** o') <- typeCheck curr o
           | (TyPort (flow,BVECT (W (S (S n)) ItIsSucc) type) ** term)
               => Left (Err fc (Mismatch (TyPort (OUTPUT, BVECT (W (S (S Z)) ItIsSucc) type))
                                         (TyPort (flow,   BVECT (W (S (S n)) ItIsSucc) type))
                                         ))
           | (type ** term)
               => Left (Err fc VectorExpected)

         termL <- typeCheck curr l
         termR <- typeCheck curr r

         l' <- checkPort fc INPUT  type termL
         r' <- checkPort fc INPUT  type termR

         pure (_ ** Collect o' l' r')

  typeCheck curr (Shim fc dir thing)

    = do t <- typeCheck curr thing

         dtype <- getDataType fc t

         term <- checkPort fc dir dtype t

         pure (_ ** term)

  typeCheck curr (Stop x)
    = pure (_ ** Stop)

namespace Design
  export
  typeCheck : (ast : AST) -> TyCheck (Term Nil TyUnit)
  typeCheck ast with (typeCheck Nil ast)
    typeCheck ast | (Left x) = Left x
    typeCheck ast | (Right (MkDPair TyUnit term)) = Right term
    typeCheck ast | (Right (MkDPair ty snd)) = Left (Mismatch TyUnit ty)

  export
  typeCheckIO : (ast : AST) -> IO (TyCheck (Term Nil TyUnit))
  typeCheckIO ast = pure (typeCheck ast)

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits