text:
module Opcodes

import Effects
import Effect.Random
import Effect.State
import Data.Bits
import Data.Fin
import Data.Vect

import Cpu
import Screen
import Chip8
import Utilities
import Ram
import MemoryIO

%default total

Register : Type
Register = Fin 16

-- always in position 0x0R00
extractFirstRegister : (value : Bits16) -> Register
extractFirstRegister v = cast $ extractSecondNibble v

-- always in position 0x00R0
extractSecondRegister : (value : Bits16) -> Register
extractSecondRegister v = cast $ extractThirdNibble v

SpriteLength : Type
SpriteLength = Fin 16

-- always in position 0x000S
extractSpriteLength : (value : Bits16) -> SpriteLength
extractSpriteLength v = cast $ extractFourthNibble v

Address : Type
Address = Bits16 -- really a 12 bit value

-- always in position 0x0AAA
extractAddress : (value : Bits16) -> Address
extractAddress = extractMask0xfff

Value : Type
Value = Bits8

-- always in position 0x00VV
extractValue : (value : Bits16) -> Value
extractValue = extractSecondByte

data Opcode =
  Invalid Bits16
  | ClearScreen
  | Return
  | Jump                   Address
  | Call                   Address
  | SkipIfEq               Register Value
  | SkipIfNeq              Register Value
  | SkipIfRegisterEq       Register Register
  | LoadRegister           Register Value
  | AddRegister            Register Value
  | CopyRegister           Register Register
  | OrRegister             Register Register
  | AndRegister            Register Register
  | XorRegister            Register Register
  | AddRegisterCarry       Register Register
  | SubRegister            Register Register
  | ShiftRightRegister     Register Register
  | SubRegisterInverse     Register Register
  | ShiftLeftRegister      Register Register
  | SkipIfRegisterNeq      Register Register
  | LoadRegisterI          Address
  | JumpRegister0          Address
  | Random                 Register Value
  | Display                Register Register SpriteLength
  | SkipIfKeyPressed       Register
  | SkipIfKeyNotPressed    Register
  | LoadRegisterDelay      Register
  | WaitForKeyPress        Register
  | SetDelayFromRegister   Register
  | SetSoundFromRegister   Register
  | AddRegisterI           Register
  | LoadRegisterWithSprite Register
  | StoreBCD               Register
  | DumpRegisters          Register
  | LoadRegisters          Register

Show Register where
  show r = "V" ++ (show $ finToNat r)

Show Opcode where
  show (Invalid op)               = "INVALID " ++ show op
  show ClearScreen                = "CLS"
  show Return                     = "RET"
  show (Jump a)                   = "JP "      ++ show a
  show (Call a)                   = "CALL "    ++ show a
  show (SkipIfEq r v)             = "SE "      ++ show r  ++ ", " ++ show v
  show (SkipIfNeq r v)            = "SNE "     ++ show r  ++ ", " ++ show v
  show (SkipIfRegisterEq r1 r2)   = "SE "      ++ show r1 ++ ", " ++ show r2
  show (LoadRegister r v)         = "LD "      ++ show r  ++ ", " ++ show v
  show (AddRegister r v)          = "ADD "     ++ show r  ++ ", " ++ show v
  show (CopyRegister r1 r2)       = "LD "      ++ show r1 ++ ", " ++ show r2
  show (OrRegister r1 r2)         = "OR "      ++ show r1 ++ ", " ++ show r2
  show (AndRegister r1 r2)        = "AND"      ++ show r1 ++ ", " ++ show r2
  show (XorRegister r1 r2)        = "XOR"      ++ show r1 ++ ", " ++ show r2
  show (AddRegisterCarry r1 r2)   = "ADD "     ++ show r1 ++ ", " ++ show r2
  show (SubRegister r1 r2)        = "SUB "     ++ show r1 ++ ", " ++ show r2
  show (ShiftRightRegister r1 r2) = "SHR "     ++ show r1
  show (SubRegisterInverse r1 r2) = "SUBN "    ++ show r1 ++ ", " ++ show r2
  show (ShiftLeftRegister r1 r2)  = "SHL "     ++ show r1
  show (SkipIfRegisterNeq r1 r2)  = "SNE "     ++ show r1 ++ ", " ++ show r2
  show (LoadRegisterI a)          = "LD I, "   ++ show a
  show (JumpRegister0 a)          = "JP V0, "  ++ show a
  show (Random r v)               = "RND "     ++ show r  ++ ", " ++ show v
  show (Display r1 r2 s)          = "DRW "     ++ show r1 ++ ", " ++ show r2 ++ ", I[" ++ show (finToNat s) ++ "]"
  show (SkipIfKeyPressed r)       = "SKP "     ++ show r
  show (SkipIfKeyNotPressed r)    = "SKNP "    ++ show r
  show (LoadRegisterDelay r)      = "LD "      ++ show r  ++ ", DT"
  show (WaitForKeyPress r)        = "LD "      ++ show r  ++ ", K"
  show (SetDelayFromRegister r)   = "LD DT, "  ++ show r
  show (SetSoundFromRegister r)   = "LD ST, "  ++ show r
  show (AddRegisterI r)           = "ADD I, "  ++ show r
  show (LoadRegisterWithSprite r) = "LD F, "   ++ show r
  show (StoreBCD r)               = "LD B, "   ++ show r
  show (DumpRegisters r)          = "LD [I], " ++ show r
  show (LoadRegisters r)          = "LD "      ++ show r  ++ ", [I]"

extractOpcode : (value : Bits16) -> Opcode
extractOpcode op =
  let family: Int = cast $ extractFirstNibble op in
  opcodeDispatch family op
  where
    opcodeDispatch : (n : Int) -> (op : Bits16) -> Opcode
    opcodeDispatch 0 op =
      case op of
        0x00e0 => ClearScreen
        0x00ee => Return
        _ => Invalid op
    opcodeDispatch 0x1 op = Jump          (extractAddress op)
    opcodeDispatch 0x2 op = Call          (extractAddress op)
    opcodeDispatch 0x3 op = SkipIfEq      (extractFirstRegister op) (extractValue op)
    opcodeDispatch 0x4 op = SkipIfNeq     (extractFirstRegister op) (extractValue op)
    opcodeDispatch 0x5 op =
      case extractFourthNibble op of
        0x0 => SkipIfRegisterEq           (extractFirstRegister op) (extractSecondRegister op)
        _ => Invalid op
    opcodeDispatch 0x6 op = LoadRegister  (extractFirstRegister op) (extractValue op)
    opcodeDispatch 0x7 op = AddRegister   (extractFirstRegister op) (extractValue op)
    opcodeDispatch 0x8 op =
      case extractFourthNibble op of
        0x0 => CopyRegister               (extractFirstRegister op) (extractSecondRegister op)
        0x1 => OrRegister                 (extractFirstRegister op) (extractSecondRegister op)
        0x2 => AndRegister                (extractFirstRegister op) (extractSecondRegister op)
        0x3 => XorRegister                (extractFirstRegister op) (extractSecondRegister op)
        0x4 => AddRegisterCarry           (extractFirstRegister op) (extractSecondRegister op)
        0x5 => SubRegister                (extractFirstRegister op) (extractSecondRegister op)
        0x6 => ShiftRightRegister         (extractFirstRegister op) (extractSecondRegister op)
        0x7 => SubRegisterInverse         (extractFirstRegister op) (extractSecondRegister op)
        0xe => ShiftLeftRegister          (extractFirstRegister op) (extractSecondRegister op)
        _ => Invalid op
    opcodeDispatch 0x9 op =
      case extractFourthNibble op of
        0x0 => SkipIfRegisterNeq          (extractFirstRegister op) (extractSecondRegister op)
        _ => Invalid op
    opcodeDispatch 0xa op = LoadRegisterI (extractAddress op)
    opcodeDispatch 0xb op = JumpRegister0 (extractAddress op)
    opcodeDispatch 0xc op = Random        (extractFirstRegister op) (extractValue op)
    opcodeDispatch 0xd op = Display       (extractFirstRegister op) (extractSecondRegister op) (extractSpriteLength op)
    opcodeDispatch 0xe op =
      case extractSecondByte op of
        0x9e => SkipIfKeyPressed          (extractFirstRegister op)
        0xa1 => SkipIfKeyNotPressed       (extractFirstRegister op)
        _ => Invalid op
    opcodeDispatch 0xf op =
      case extractSecondByte op of
      0x07 => LoadRegisterDelay         (extractFirstRegister op)
      0x0a => WaitForKeyPress           (extractFirstRegister op)
      0x15 => SetDelayFromRegister      (extractFirstRegister op)
      0x18 => SetSoundFromRegister      (extractFirstRegister op)
      0x1e => AddRegisterI              (extractFirstRegister op)
      0x29 => LoadRegisterWithSprite    (extractFirstRegister op)
      0x33 => StoreBCD                  (extractFirstRegister op)
      0x55 => DumpRegisters             (extractFirstRegister op)
      0x65 => LoadRegisters             (extractFirstRegister op)
      _ => Invalid op
    opcodeDispatch _ op = Invalid op

-- opcode implementations

clearScreen : (chip : Chip8) -> Chip8
clearScreen chip =
  let cpu = Computer chip in
  record { Display = newScreen, Computer = incrementPC cpu } chip

jumpDirect : (chip : Chip8) -> (address : Address) -> Chip8
jumpDirect chip addr =
  let cpu = Computer chip in
  if (getPC cpu == addr) then
    record { State = Halted "Infinite loop" } chip
  else
    record { Computer = setPC cpu addr } chip

skipIfRegisterEqual : (cpu : Cpu) -> (register : Register) -> (value : Value) -> Cpu
skipIfRegisterEqual c r v =
  let toCompare = getRegister c r in
  if v == toCompare then
    incrementPC c
  else
    c

skipIfRegisterNotEqual : (cpu : Cpu) -> (register : Register) -> (value : Value) -> Cpu
skipIfRegisterNotEqual c r v =
  let toCompare = getRegister c r in
  if v /= toCompare then
    incrementPC c
  else
    c

skipIfRegistersEqual : (cpu : Cpu) -> (register : Register) -> (register : Register) -> Cpu
skipIfRegistersEqual c r1 r2 =
  let v1 = getRegister c r1 in
  let v2 = getRegister c r2 in
  if v1 == v2 then
    incrementPC c
  else
    c

copyRegisters : (cpu : Cpu) -> (register : Register) -> (register : Register) -> Cpu
copyRegisters c r1 r2 =
  let value = getRegister c r2 in
  setRegister c r1 value

orRegister : (cpu : Cpu) -> (register : Register) -> (register : Register) -> Cpu
orRegister c r1 r2 =
  let v1 = cast $ getRegister c r1 in
  let v2 = cast $ getRegister c r2 in
  let result = cast $ bitsToInt (v1 `or` v2) in
  setRegister c r1 result

andRegister : (cpu : Cpu) -> (register : Register) -> (register : Register) -> Cpu
andRegister c r1 r2 =
  let v1 = cast $ getRegister c r1 in
  let v2 = cast $ getRegister c r2 in
  let result = cast $ bitsToInt (v1 `and` v2) in
  setRegister c r1 result

xorRegister : (cpu : Cpu) -> (register : Register) -> (register : Register) -> Cpu
xorRegister c r1 r2 =
  let v1 = cast $ getRegister c r1 in
  let v2 = cast $ getRegister c r2 in
  let result = cast $ bitsToInt (v1 `xor` v2) in
  setRegister c r1 result

addRegisterCarry : (cpu : Cpu) -> (register : Register) -> (register : Register) -> Cpu
addRegisterCarry c r1 r2 =
  let v1 : Bits16 = cast $ getRegister c r1 in
  let v2 : Bits16 = cast $ getRegister c r2 in
  let result : Bits16 = v1 + v2 in
  let flag = if result > 0xff then 1 else 0 in
  let masked = extractSecondByte result in
  let cpu = setRegister c r1 masked in
  setRegisterFlag cpu flag

subtractRegister : (cpu : Cpu) -> (register : Register) -> (register : Register) -> Cpu
subtractRegister c r1 r2 =
  let v1 : Int = cast $ getRegister c r1 in
  let v2 : Int = cast $ getRegister c r2 in
  let result = cast (v1 - v2) in
  let flag = if v1 > v2 then 1 else 0 in
  let cpu = setRegister c r1 result in
  setRegisterFlag cpu flag

shiftRightRegister : (cpu : Cpu) -> (register : Register) -> (register : Register) -> Cpu
shiftRightRegister c r _ =
  let v = cast $ getRegister c r in
  let one = intToBits 0x1 in
  let result = cast $ bitsToInt (v `shiftRightLogical` one) in
  let flag = cast $ bitsToInt (v `and` one) in
  let cpu = setRegister c r result in
  setRegisterFlag cpu flag

subtractRegisterInverse : (cpu : Cpu) -> (register : Register) -> (register : Register) -> Cpu
subtractRegisterInverse c r1 r2 =
  let v1 : Int = cast $ getRegister c r1 in
  let v2 : Int = cast $ getRegister c r2 in
  let result = cast (v2 - v1) in
  let flag = if v2 > v1 then 1 else 0 in
  let cpu = setRegister c r1 result in
  setRegisterFlag cpu flag

shiftLeftRegister : (cpu : Cpu) -> (register : Register) -> (register : Register) -> Cpu
shiftLeftRegister c r _ =
  let v = getRegister c r in
  let one = intToBits 0x1 in
  let result = cast $ bitsToInt ((cast v) `shiftLeft` one) in
  let flag = if v > 0x7f then 1 else 0 in
  let cpu = setRegister c r result in
  setRegisterFlag cpu flag

skipIfRegistersNotEqual : (cpu : Cpu) -> (register : Register) -> (register : Register) -> Cpu
skipIfRegistersNotEqual c r1 r2 =
  let v1 = getRegister c r1 in
  let v2 = getRegister c r2 in
  if v1 /= v2 then
    incrementPC c
  else
    c

addRegisterDirect : (cpu : Cpu) -> (register : Register) -> (value : Value) -> Cpu
addRegisterDirect c r v =
  let value = getRegister c r in
  setRegister c r (value + v)

jumpRegister0 : (chip : Chip8) -> (address : Address) -> Chip8
jumpRegister0 chip addr =
  let cpu = Computer chip in
  let value : Bits16 = cast $ getRegister cpu 0 in
  let newAddress = addr + value in
  jumpDirect chip newAddress

partial
andRandomValue : (register : Register) -> (value : Value) -> { [Chip8 ::: STATE Chip8, RND] } Eff ()
andRandomValue r v =
  let chip = !(Chip8 :- get) in
  let cpu = Computer chip in
  let mask = cast v in
  let rand = !(rndInt 0x00 0xff) in
  let value = cast rand `and` mask in
  let newCpu = setRegister cpu r $ cast value in
  let newChip = record { Computer = incrementPC newCpu } chip in
  Chip8 :- put newChip

display : (register : Register) -> (register : Register) -> (sprite: SpriteLength) -> { [Chip8 ::: STATE Chip8, RAM] } Eff ()
display r1 r2 s =
  let chip = !(Chip8 :- get) in
  let cpu = Computer chip in
  let screen = Display chip in
  let x = cast $ getRegister cpu r1 in
  let y = cast $ getRegister cpu r2 in
  let loadAddress = cast $ getRegisterI cpu in
  let sprite = !(loadBlock loadAddress s) in
  let newDisplay = writeSpriteToScreen screen sprite x y in
  let newCpu = if wasErased newDisplay then setRegister cpu 0xf 1 else setRegister cpu 0xf 0 in
  let newChip = record { Display = newDisplay, Computer = incrementPC newCpu } chip in
  Chip8 :- put newChip

skipIfKeyPressed : (chip : Chip8) -> (register : Register) -> Chip8
skipIfKeyPressed chip r =
  let cpu = Computer chip in
  let k = cast $ getRegister cpu r in
  let pressed = isKeyPressed chip k in
  if pressed then
    record { Computer = incrementPC $ incrementPC cpu } chip
  else
    record { Computer = incrementPC cpu } chip

skipIfKeyNotPressed : (chip : Chip8) -> (register : Register) -> Chip8
skipIfKeyNotPressed chip r =
  let cpu = Computer chip in
  let k = cast $ getRegister cpu r in
  let pressed = isKeyPressed chip k in
  if pressed then
    record { Computer = incrementPC cpu } chip
  else
    record { Computer = incrementPC $ incrementPC cpu } chip

loadRegisterDelay : (cpu : Cpu) -> (register : Register) -> Cpu
loadRegisterDelay c r =
  let countdown = getDelayTimer c in
  setRegister c r countdown

waitForKeyPress : (chip : Chip8) -> (register : Register) -> Chip8
waitForKeyPress chip r =
  record { State = WaitingForKey r } chip

setDelayFromRegister : (cpu : Cpu) -> (register : Register) -> Cpu
setDelayFromRegister c r =
  let countdown = getRegister c r in
  setDelayTimer c countdown

setSoundFromRegister : (cpu : Cpu) -> (register : Register) -> Cpu
setSoundFromRegister c r =
  let countdown = getRegister c r in
  setSoundTimer c countdown

addRegisterI : (cpu : Cpu) -> (register : Register) -> Cpu
addRegisterI c r =
  let value = getRegister c r in
  let currentI = getRegisterI c in
  let newI = currentI + (cast value) in
  setRegisterI c newI

loadRegisterWithSprite : (cpu : Cpu) -> (register : Register) -> Cpu
loadRegisterWithSprite c r =
  let v : Int = cast $ getRegister c r in
  let index = restrict 15 $ cast v in
  let address = defaultSpriteStartingAddress index in
  setRegisterI c address

partial
storeBCD : (register : Register) -> { [Chip8 ::: STATE Chip8, RAM] } Eff ()
storeBCD r =
  let chip = !(Chip8 :- get) in
  let cpu = Computer chip in
  let value = getRegister cpu r in
  let dumpAddress = cast $ getRegisterI cpu in
  let first = value `div` 100 in
  let second = (value `mod` 100) `div` 10 in
  let third = value `mod` 10 in
  let digits = [first, second, third] in
  do
    dumpBlock dumpAddress digits
    Chip8 :- put (record { Computer = incrementPC cpu } chip)

partial
dumpRegisters : (register : Register) -> { [Chip8 ::: STATE Chip8, RAM] } Eff ()
dumpRegisters r =
  let chip = !(Chip8 :- get) in
  let cpu = Computer chip in
  let dumpAddress = cast $ getRegisterI cpu in
  let value : Int = cast $ getRegister cpu r in
  let len = restrict 15 $ cast value in
  let registers = getRegisters cpu len in
  do
    dumpBlock dumpAddress registers
    Chip8 :- put (record { Computer = incrementPC cpu } chip)

partial
loadRegisters : (register : Register) -> { [Chip8 ::: STATE Chip8, RAM] } Eff ()
loadRegisters r =
  let chip = !(Chip8 :- get) in
  let cpu = Computer chip in
  let loadAddress = cast $ getRegisterI cpu in
  let value : Int = cast $ getRegister cpu r in
  let len = restrict 15 $ cast value in
  let registers = !(loadBlock loadAddress len) in
  let newCpu = setRegisters cpu len registers in
  Chip8 :- put (record { Computer = incrementPC cpu } chip)

-- convenience function for pure opcode functions that operate on the CPU only
updateCPU : (cpu : Cpu) -> { [Chip8 ::: STATE Chip8] } Eff ()
updateCPU cpu =
  let chip = !(Chip8 :- get) in
  let newComputer = incrementPC cpu in
  Chip8 :- put (record { Computer = newComputer } chip)

-- convenience function for pure opcode functions that operate on the chip
updateChip : (chip : Chip8) -> { [Chip8 ::: STATE Chip8] } Eff ()
updateChip newChip = Chip8 :- put newChip

partial
dispatch : (opcode : Opcode) -> { [Chip8 ::: STATE Chip8, RAM, RND] } Eff ()
dispatch ClearScreen                = updateChip $ clearScreen                       !(Chip8 :- get)
dispatch Return                     = updateCPU  $ popStack                (Computer !(Chip8 :- get))
dispatch (Jump addr)                = updateChip $ jumpDirect                        !(Chip8 :- get)  addr
dispatch (Call addr)                = updateCPU  $ pushStack               (Computer !(Chip8 :- get)) addr
dispatch (SkipIfEq r v)             = updateCPU  $ skipIfRegisterEqual     (Computer !(Chip8 :- get)) r  v
dispatch (SkipIfNeq r v)            = updateCPU  $ skipIfRegisterNotEqual  (Computer !(Chip8 :- get)) r  v
dispatch (SkipIfRegisterEq r1 r2)   = updateCPU  $ skipIfRegistersEqual    (Computer !(Chip8 :- get)) r1 r2
dispatch (LoadRegister r v)         = updateCPU  $ setRegister             (Computer !(Chip8 :- get)) r  v
dispatch (AddRegister r v)          = updateCPU  $ addRegisterDirect       (Computer !(Chip8 :- get)) r  v
dispatch (CopyRegister r1 r2)       = updateCPU  $ copyRegisters           (Computer !(Chip8 :- get)) r1 r2
dispatch (OrRegister r1 r2)         = updateCPU  $ orRegister              (Computer !(Chip8 :- get)) r1 r2
dispatch (AndRegister r1 r2)        = updateCPU  $ andRegister             (Computer !(Chip8 :- get)) r1 r2
dispatch (XorRegister r1 r2)        = updateCPU  $ xorRegister             (Computer !(Chip8 :- get)) r1 r2
dispatch (AddRegisterCarry r1 r2)   = updateCPU  $ addRegisterCarry        (Computer !(Chip8 :- get)) r1 r2
dispatch (SubRegister r1 r2)        = updateCPU  $ subtractRegister        (Computer !(Chip8 :- get)) r1 r2
dispatch (ShiftRightRegister r1 r2) = updateCPU  $ shiftRightRegister      (Computer !(Chip8 :- get)) r1 r2
dispatch (SubRegisterInverse r1 r2) = updateCPU  $ subtractRegisterInverse (Computer !(Chip8 :- get)) r1 r2
dispatch (ShiftLeftRegister r1 r2)  = updateCPU  $ shiftLeftRegister       (Computer !(Chip8 :- get)) r1 r2
dispatch (SkipIfRegisterNeq r1 r2)  = updateCPU  $ skipIfRegistersNotEqual (Computer !(Chip8 :- get)) r1 r2
dispatch (LoadRegisterI r)          = updateCPU  $ setRegisterI            (Computer !(Chip8 :- get)) r
dispatch (JumpRegister0 addr)       = updateChip $ jumpRegister0                     !(Chip8 :- get)  addr
dispatch (Random r v)               =              andRandomValue                                     r  v
dispatch (Display r1 r2 s)          =              display                                            r1 r2 s
dispatch (SkipIfKeyPressed r)       = updateChip $ skipIfKeyPressed                  !(Chip8 :- get)  r
dispatch (SkipIfKeyNotPressed r)    = updateChip $ skipIfKeyNotPressed               !(Chip8 :- get)  r
dispatch (LoadRegisterDelay r)      = updateCPU  $ loadRegisterDelay       (Computer !(Chip8 :- get)) r
dispatch (WaitForKeyPress r)        = updateChip $ waitForKeyPress                   !(Chip8 :- get)  r
dispatch (SetDelayFromRegister r)   = updateCPU  $ setDelayFromRegister    (Computer !(Chip8 :- get)) r
dispatch (SetSoundFromRegister r)   = updateCPU  $ setSoundFromRegister    (Computer !(Chip8 :- get)) r
dispatch (AddRegisterI r)           = updateCPU  $ addRegisterI            (Computer !(Chip8 :- get)) r
dispatch (LoadRegisterWithSprite r) = updateCPU  $ loadRegisterWithSprite  (Computer !(Chip8 :- get)) r
dispatch (StoreBCD r)               =              storeBCD                                           r
dispatch (DumpRegisters r)          =              dumpRegisters                                      r
dispatch (LoadRegisters r)          =              loadRegisters                                      r

export
partial
runOneCycle : (tick : Bool) -> { [Chip8 ::: STATE Chip8, RAM, RND] } Eff ()
runOneCycle tick =
  let instruction = extractOpcode !getOpcode in
  case instruction of
    Invalid _ =>
      let errorMessage = "Unknown opcode: " ++ (show instruction) in
      let chip = !(Chip8 :- get) in
      Chip8 :- put (record { State = Halted errorMessage } chip)
    _ =>
      do
        dispatch instruction
        chip <- Chip8 :- get
        newComputer <- pure $ updateCPUTimers (Computer chip) tick
        Chip8 :- put (record { Computer = newComputer } chip)


text:
module Ch6Ex

import Data.Vect

Matrix : Nat -> Nat -> Type
Matrix r c = Vect r (Vect c Double)

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

TupleVect : (numargs : Nat) -> Type -> Type
TupleVect Z ty = ()
TupleVect (S k) ty = (ty, TupleVect k ty)

test : TupleVect 4 Nat
test = (1,2,3,4,())

ext: idr

max_stars_repo_name: balajisivaraman/idris-book

max_issues_repo_name: balajisivaraman/idris-book

max_forks_repo_name: balajisivaraman/idris-book


text:
||| Checking a %builtin pragma is correct.
-- If we get more builtins it might be wise to move each builtin to it's own file.
module TTImp.ProcessBuiltin

import Data.List

import Libraries.Data.Fin as Libs
import Libraries.Data.NameMap

import Core.CaseTree
import Core.Core
import Core.Context
import Core.Context.Log
import Core.CompileExpr
import Core.Env
import Core.Metadata
import Core.TT
import Core.UnifyState

import TTImp.TTImp

%default covering

showDefType : Def -> String
showDefType None = "undefined"
showDefType (PMDef {}) = "function"
showDefType (ExternDef {}) = "external function"
showDefType (ForeignDef {}) = "foreign function"
showDefType (Builtin {}) = "builtin function"
showDefType (DCon {}) = "data constructor"
showDefType (TCon {}) = "type constructor"
showDefType (Hole {}) = "hole"
showDefType (BySearch {}) = "search"
showDefType (Guess {}) = "guess"
showDefType ImpBind = "bound name"
showDefType Delayed = "delayed"

||| Get the return type.
getReturnType : {vars : _} -> Term vars -> Maybe (vars ** Term vars)
getReturnType tm@(Bind _ x b scope) = case b of
    Let _ _ val _ => getReturnType $ subst {x} val scope
    Pi _ _ _ _ => getReturnType scope
    _ => Nothing
getReturnType tm = Just (vars ** tm)

||| Get the top level type constructor if there is one.
getTypeCons : {vars : _} -> Term vars -> Maybe Name
getTypeCons (Local _ _ _ p) = Just $ nameAt p
getTypeCons (Ref _ _ name) = Just name
getTypeCons (Meta {}) = Nothing
getTypeCons (Bind _ x b scope) = case b of
    Let _ _ val _ => getTypeCons $ subst {x} val scope
    _ => Nothing
getTypeCons (App _ fn _) = getTypeCons fn
getTypeCons _ = Nothing

||| Get the arguments of a `Term` representing a type.
getTypeArgs : {vars : _} -> Term vars -> List (vars ** Term vars)
getTypeArgs (Bind _ x b tm) = case b of
    Let _ _ val _ => getTypeArgs $ subst {x} val tm
    Pi _ _ _ arg => (_ ** arg) :: getTypeArgs tm
    _ => []
getTypeArgs _ = []

||| Get all non-erased aruments.
getNEArgs : {vars : _} -> Term vars -> List (vars ** Term vars)
getNEArgs (Bind _ x b tm) = case b of
    Let _ _ val _ => getNEArgs $ subst {x} val tm
    Pi _ mul _ arg => if isErased mul
        then getNEArgs tm
        else (_ ** arg) :: getNEArgs tm
    _ => []
getNEArgs _ = []

||| Get the first non-erased argument type.
getFirstNEType : {vars : _} -> Term vars -> Maybe (vars ** Term vars)
getFirstNEType tm = case getNEArgs tm of
    [] => Nothing
    arg :: _ => Just arg

||| Get the index of the first non-erased argument if it exists.
getNEIndex : Term vars -> Maybe Nat
getNEIndex (Bind _ x b tm) = case b of
    Let _ _ val _ => getNEIndex $ subst {x} val tm
    Pi _ mul _ arg => if isErased mul
        then getNEIndex tm
        else Just 0
    _ => Nothing
getNEIndex _ = Nothing

||| Get the index of all non-erased Integer argument.
getNEIntegerIndex : Term vars -> Maybe (List Nat)
getNEIntegerIndex (Bind _ x b tm) = case b of
    Let _ _ val _ => getNEIntegerIndex $ subst {x} val tm
    Pi _ mul _ arg => if not (isErased mul) && isInteger arg
        then Prelude.(::) 0 . map (+ 1) <$> getNEIntegerIndex tm
        else getNEIntegerIndex tm
    _ => Nothing
  where
    isInteger : forall vars. Term vars -> Bool
    isInteger (PrimVal _ IntegerType) = True
    isInteger _ = False
getNEIntegerIndex _ = Just []

||| Do the terms match ignoring arguments to type constructors.
termConMatch : Term vs -> Term vs' -> Bool
termConMatch (Local _ _ x _) (Local _ _ y _) = x == y
termConMatch (Ref _ _ n) (Ref _ _ m) = n == m
termConMatch (Meta _ _ i args0) (Meta _ _ j args1)
    = i == j && all (uncurry termConMatch) (zip args0 args1)
    -- I don't understand how they're equal if args are different lengths
    -- but this is what's in Core.TT.
termConMatch (Bind _ _ b s) (Bind _ _ c t) = eqBinderBy termConMatch b c && termConMatch s t
termConMatch (App _ f _) (App _ g _) = termConMatch f g
termConMatch (As _ _ a p) (As _ _ b q) = termConMatch a b && termConMatch p q
termConMatch (TDelayed _ _ tm0) tm1 = termConMatch tm0 tm1
termConMatch tm0 (TDelayed _ _ tm1) = termConMatch tm0 tm1
    -- don't check for laziness here to give more accurate error messages.
termConMatch (TDelay _ _ tm0 x0) (TDelay _ _ tm1 x1) = termConMatch tm0 tm1 && termConMatch x0 x1
termConMatch (TForce _ _ tm0) tm1 = termConMatch tm0 tm1
termConMatch tm0 (TForce _ _ tm1) = termConMatch tm0 tm1
termConMatch (PrimVal _ _) (PrimVal _ _) = True -- no constructor to check.
termConMatch (Erased _ _) (Erased _ _) = True -- return type can't erased?
termConMatch (TType _) (TType _) = True
termConMatch _ _ = False

||| Check a type is strict.
isStrict : Term vs -> Bool
isStrict (Local _ _ _ _) = True
isStrict (Ref _ _ _) = True
isStrict (Meta _ _ i args) = all isStrict args
isStrict (Bind _ _ b s) = isStrict (binderType b) && isStrict s
isStrict (App _ f x) = isStrict f && isStrict x
isStrict (As _ _ a p) = isStrict a && isStrict p
isStrict (TDelayed _ _ _) = False
isStrict (TDelay _ _ f x) = isStrict f && isStrict x
isStrict (TForce _ _ tm) = isStrict tm
isStrict (PrimVal _ _) = True
isStrict (Erased _ _) = True
isStrict (TType _) = True

||| Get the name and definition of a list of names.
getConsGDef :
    Ref Ctxt Defs =>
    FC -> (cons : List Name) ->
    Core $ List (Name, GlobalDef)
getConsGDef fc cons = do
    defs <- get Ctxt
    let c = defs.gamma
    for cons $ \n => do
        [(n', _, gdef)] <- lookupCtxtName n c
            | [] => undefinedName fc n
            | ns => throw $ AmbiguousName fc $ (\(n, _, _) => n) <$> ns
        pure (n', gdef)

isNatural : Ref Ctxt Defs => FC ->Name -> Core Bool
isNatural fc n = do
    defs <- get Ctxt
    Just gdef <- lookupCtxtExact n defs.gamma
        | Nothing => undefinedName EmptyFC n
    let TCon _ _ _ _ _ _ cons _ = gdef.definition
        | _ => pure False
    consDefs <- getConsGDef fc cons
    pure $ all hasNatFlag consDefs
  where
    isNatFlag : DefFlag -> Bool
    isNatFlag (ConType ZERO) = True
    isNatFlag (ConType SUCC) = True
    isNatFlag _ = False
    hasNatFlag : (Name, GlobalDef) -> Bool
    hasNatFlag (_, gdef) = any isNatFlag gdef.flags

||| Check a list of constructors has exactly
||| 1 'Z'-like constructor
||| and 1 `S`-like constructor, which has type `ty -> ty` or `ty arg -> `ty (f arg)`.
checkNatCons : Context -> (cons : List (Name, GlobalDef)) -> (dataType : Name) -> FC -> Core ()
checkNatCons c cons ty fc = case !(foldr checkCon (pure (Nothing, Nothing)) cons) of
    (Just zero, Just succ) => pure ()
    (Nothing, _) => throw $ GenericMsg fc $ "No 'Z'-like constructors for " ++ show ty ++ "."
    (_, Nothing) => throw $ GenericMsg fc $ "No 'S'-like constructors for " ++ show ty ++ "."
  where
    ||| Check if a list of names contains a name.
    checkSArgType : List Name -> Core ()
    checkSArgType [] = throw $ GenericMsg fc $ "'S'-like constructor for " ++ show ty ++ " is missing argument of type: " ++ show ty
    checkSArgType (n :: ns) = if nameRoot n == nameRoot ty && (n `matches` ty)
        then checkSArgType ns
        else throw $ GenericMsg fc $ "'S'-like constructor for " ++ show ty ++ " has unexpected argument: " ++ show n

    ||| Check the type of an 'S'-like constructor.
    checkTyS : Name -> GlobalDef -> Core ()
    checkTyS n gdef = do
        let type = gdef.type
            erase = gdef.eraseArgs
        let Just (_ ** arg) = getFirstNEType type
            | Nothing => throw $ InternalError "Expected a non-erased argument, found none."
        let Just (_ ** ret) = getReturnType type
            | Nothing => throw $ InternalError $ "Unexpected type " ++ show type
        unless (termConMatch arg ret) $ throw $ GenericMsg fc $ "Incorrect type for 'S'-like constructor for " ++ show ty ++ "."
        unless (isStrict arg) $ throw $ GenericMsg fc $ "Natural builtin does not support lazy types."
        pure ()

    ||| Check a constructor's arity and type.
    -- 'Z'-like constructor is always first, then 'S'-like constructor.
    checkCon : (Name, GlobalDef) -> Core (Maybe Name, Maybe Name) -> Core (Maybe Name, Maybe Name)
    checkCon (n, gdef) cons = do
        (zero, succ) <- cons
        let DCon _ arity _ = gdef.definition
            | def => throw $ GenericMsg fc $ "Expected data constructor, found:" ++ showDefType def
        case arity `minus` length gdef.eraseArgs of
            0 => case zero of
                Just _ => throw $ GenericMsg fc $ "Multiple 'Z'-like constructors for " ++ show ty ++ "."
                Nothing => pure (Just n, succ)
            1 => case succ of
                Just _ => throw $ GenericMsg fc $ "Multiple 'S'-like constructors for " ++ show ty ++ "."
                Nothing => do
                    checkTyS n gdef
                    pure (zero, Just n)
            _ => throw $ GenericMsg fc $ "Constructor " ++ show n ++ " doesn't match any pattern for Natural."

||| Check a `%builtin Natural` pragma is correct.
processBuiltinNatural :
    Ref Ctxt Defs =>
    FC -> Name -> Core ()
processBuiltinNatural fc name = do
    ds <- get Ctxt
    log "builtin.Natural" 5 $ "Processing %builtin Natural " ++ show name ++ "."
    [(n, _, gdef)] <- lookupCtxtName name ds.gamma
        | [] => undefinedName fc name
        | ns => throw $ AmbiguousName fc $ (\(n, _, _) => n) <$> ns
    False <- isNatural fc n
        | True => pure ()
    let TCon _ _ _ _ _ _ dcons _ = gdef.definition
        | def => throw $ GenericMsg fc
            $ "Expected a type constructor, found " ++ showDefType def ++ "."
    cons <- getConsGDef fc dcons
    checkNatCons ds.gamma cons n fc

||| Check a `%builtin NaturalToInteger` pragma is correct.
processNatToInteger :
    Ref Ctxt Defs =>
    FC -> Name -> Core ()
processNatToInteger fc fn = do
    let show_fn = show fn
    ds <- get Ctxt
    log "builtin.NaturalToInteger" 5 $ "Processing %builtin NaturalToInteger " ++ show_fn ++ "."
    [(_ , i, gdef)] <- lookupCtxtName fn ds.gamma
        | [] => undefinedName fc fn
        | ns => throw $ AmbiguousName fc $ (\(n, _, _) => n) <$> ns
    let PMDef _ args _ cases _ = gdef.definition
        | def => throw $ GenericMsg fc
            $ "Expected function definition, found " ++ showDefType def ++ "."
    type <- toFullNames gdef.type
    logTerm "builtin.NaturalToInteger" 25 ("Type of " ++ show_fn) type
    let [(_ ** arg)] = getNEArgs type
        | [] => throw $ GenericMsg fc $ "No arguments found for " ++ show_fn ++ "."
        | _ => throw $ GenericMsg fc $ "More than 1 non-erased arguments found for " ++ show_fn ++ "."
    let Just tyCon = getTypeCons arg
        | Nothing => throw $ GenericMsg fc
            $ "No type constructor found for non-erased arguement of " ++ show_fn ++ "."
    True <- isNatural fc tyCon
        | False => throw $ GenericMsg fc $ "Non-erased argument is not a 'Nat'-like type."
    let Just natIdx = getNEIndex type
        | Nothing => throw $ InternalError "Couldn't find non-erased argument."
    setFlag fc (Resolved i) $ Identity natIdx

||| Check a `%builtin IntegerToNatural` pragma is correct.
processIntegerToNat :
    Ref Ctxt Defs =>
    FC -> Name -> Core ()
processIntegerToNat fc fn = do
    let show_fn = show fn
    ds <- get Ctxt
    log "builtin.IntegerToNatural" 5 $ "Processing %builtin IntegerToNatural " ++ show_fn ++ "."
    [(_, i, gdef)] <- lookupCtxtName fn ds.gamma
        | [] => undefinedName fc fn
        | ns => throw $ AmbiguousName fc $ (\(n, _, _) => n) <$> ns
    type <- toFullNames gdef.type
    let PMDef _ _ _ _ _ = gdef.definition
        | def => throw $ GenericMsg fc
            $ "Expected function definition, found " ++ showDefType def ++ "."
    logTerm "builtin.IntegerToNatural" 25 ("Type of " ++ show_fn) type
    let Just [intIdx] = getNEIntegerIndex type
        | Just [] => throw $ GenericMsg fc $ "No unrestricted arguments of type `Integer` found for " ++ show_fn ++ "."
        | Just _ => throw $ GenericMsg fc $ "More than one unrestricted arguments of type `Integer` found for " ++ show_fn ++ "."
        | Nothing => throw $ InternalError
            $ "Unexpected arity while processing %builtin IntegerToNatural " ++ show_fn ++ " (getNEIntegerIndex returned Nothing)"
    let Just (_ ** retTy) = getReturnType type
        | Nothing => throw $ InternalError $ "Unexpected type " ++ show type
    let Just retCon = getTypeCons retTy
        | Nothing => throw $ GenericMsg fc
            $ "No type constructor found for return type of " ++ show_fn ++ "."
    True <- isNatural fc retCon
        | False => throw $ GenericMsg fc $ "Return type is not a 'Nat'-like type"
    setFlag fc (Resolved i) $ Identity intIdx

||| Check a `%builtin` pragma is correct.
export
processBuiltin :
    Ref Ctxt Defs =>
    NestedNames vars -> Env Term vars -> FC -> BuiltinType -> Name -> Core ()
processBuiltin nest env fc type name = do
    case type of
        BuiltinNatural => processBuiltinNatural fc name
        NaturalToInteger => processNatToInteger fc name
        IntegerToNatural => processIntegerToNat fc name


text:
module NatTree

import Data.Fin

% access public export

data NatTree : Type where
  Leaf : Nat -> NatTree
  Node : NatTree -> NatTree -> NatTree

tsum : NatTree -> Nat
tsum (Leaf k) = k
tsum (Node x y) = (tsum x) + (tsum y)

recNT : (x: Type) -> (Nat -> x) -> (NatTree -> x -> NatTree -> x -> x)
  -> (NatTree -> x)
recNT x f g (Leaf k) = f k
recNT x f g (Node y z) = g y yValue z zValue where
  yValue =  recNT x f g y
  zValue = recNT x f g z

tsumTheHardWay : NatTree -> Nat
tsumTheHardWay = recNT Nat leafCase nodeCase where
  leafCase = \k : Nat => k
  nodeCase = \t1 => \n1 => \t2 => \n2 => n1 + n2

flattenTree : NatTree -> List Nat
flattenTree = recNT (List Nat) leafCase nodeCase where
  leafCase = \k => k :: []
  nodeCase = \t1 => \l1 => \t2 => \l2 => (l1 ++ l2)

data FinNatTree : Type where
  FLeaf : Nat -> FinNatTree
  FNode : (n: Nat) -> ((Fin (S n)) -> FinNatTree) -> FinNatTree

sumFinNat : (n: Nat) -> (Fin n -> Nat) -> Nat
sumFinNat Z f = Z
sumFinNat (S k) f = (f FZ) + tailsum where
  tailsum = sumFinNat k (\ x : (Fin k) => f (FS x))

finSum : FinNatTree -> Nat
finSum (FLeaf k) = k
finSum (FNode n f) = sumFinNat (S n) treeSums where
  treeSums = \index : Fin (S n) => finSum (f index)

  data Evil : Type where
    Diag : (Evil -> Bool) -> Evil

  evil : Evil -> Bool
  evil (Diag f) = not (f (Diag f))

  contra : Bool
  contra = evil (Diag evil)


text:
namespace Lua
  export
  %foreign "x, y => x + y"
  plus : Int -> Int -> Int

  export -- there is now also a `W` local variable, accessible anywhere from FFI for convenience
         -- `W` is a special table standing for the %MkWorld value
  %foreign "callback, _ => callback('abc')(22)(W)"
  callback : (callback : String -> Int -> PrimIO String) -> PrimIO String

  export
  %foreign "x => idris.inspect(x)|inspect"
  inspect : ty -> String

  export
  %foreign "x, y, f => f(x)(y)"
  apply2 : a -> (0 b : Type {- for demo purposes -}) -> b -> (a -> b -> c) -> c

  export
  %foreign "_ => print(W)"
  printWorld : IO ()

main : IO ()
main = do printLn $ Lua.plus 1 3
          str <- fromPrim $ callback (\str, i => toPrim $ pure $ str ++ " " ++ show i)
          putStrLn str
          putStrLn (inspect $ with List [the Int 1, 2, 3])
          putStrLn $ apply2 "abc" _ "def" (++)
          printWorld


text:
import System.File

import Control.App
import Control.App.FileIO
import Control.App.Console

testFileReadOps : File -> Has [Console, FileIO] e => App e ()
testFileReadOps file = do
    testStr <- fGetChars file 6
    putStrLn testStr
    chr <- fGetChar file
    putStrLn (show chr)
    rest <- fGetStr file
    putStrLn rest

testFileWriteOps : File -> Has [Console, FileIO] e => App e ()
testFileWriteOps file = do
    fPutStr file "Hello "
    fPutStrLn file "Idris!"
    fPutStrLn file "Another line"

runTests : Has [Console, FileIO] e => App e ()
runTests = do
    withFile "test.txt" WriteTruncate
        (\err => putStrLn $ "Failed to open file in write mode: " ++ show err)
        (\file => testFileWriteOps file)
    withFile "test.txt" Read
        (\err => putStrLn $ "Failed to open file in read mode: " ++ show err)
        (\file => testFileReadOps file)

prog : App Init ()
prog =
    handle runTests
        (\() => putStrLn "No exceptions occurred")
        (\err: IOError =>
            putStrLn $ "Caught file error : " ++ show err)

main : IO ()
main = run prog


text:
module Chapter5

import System
import Data.Vect

-- the type IO : (res : Type) -> Type allows us to describe an interaction,
-- encode it in the type and then let the Idris runtime execute it.

main : IO ()
main = do
  putStr "Enter your name: "
  x <- getLine
  putStrLn ("Hello " ++ x ++ "!")

-- Very curious how putStrLn "abc" actually 'returns'
-- io_bind (prim_write "abc\n") (\__bindx => io_pure ()) : IO ()
-- wonder what io_bind, prim_write and io_pure are

printLength : IO ()
printLength = getLine >>= \result => putStrLn (show (length result))

printLength' : IO ()
printLength' = putStr "Input string: " >>= \_ =>
               getLine >>= \input =>
               putStrLn (show (length input))

printLength'' : IO ()
printLength'' = do
  putStr "Input string: "
  input <- getLine
  let len = length input
  putStrLn (show len)

-- exercises
-- ex1
printLonger : IO ()
printLonger = do
  putStr "Enter first string: "
  str1 <- getLine
  putStr "Enter second string: "
  str2 <- getLine
  let longest = if (length str1 > length str2) then str1 else str2
  putStr (longest ++ "\n")

-- ex2
printLonger' : IO ()
printLonger' =
  putStr "Enter first string: " >>=
    \_ => getLine >>=
      \str1 => putStr "Enter second string: " >>=
        \_ => getLine >>=
          \str2 => let longest = if (length str1 > length str2) then str1 else str2 in
                       putStr (longest ++ "\n")

readNumber : IO (Maybe Nat)
readNumber = do
  input <- getLine
  if all isDigit (unpack input) && (length input > 0)
     then pure (Just (cast input))
     else pure Nothing
-- Pure is the same as return in Haskell.  What is the difference?
-- is it that pure is Applicative which is more general than Monad?

readPair : IO (String, String)
readPair = do str1 <- getLine
              str2 <- getLine
              pure (str1, str2)

usePair : IO ()
usePair = do
  (s1, s2) <- readPair
  putStrLn ("You entered " ++ s1 ++ " and " ++ s2 ++ "\n")

readNumbers : IO (Maybe (Nat, Nat))
readNumbers =
  do Just n1 <- readNumber | Nothing => pure Nothing  -- curious syntax.
     Just n2 <- readNumber | Nothing => pure Nothing
     pure (Just (n1, n2))

countdown : (secs : Nat) -> IO ()
countdown Z = putStrLn "liftoff!"
countdown time@(S secs) = do putStrLn (show time)
                             usleep (1000*1000)
                             countdown secs
-- exercises
-- ex1
guess : (target : Nat) -> IO ()
guess n = do putStr "Enter a number: "
             Just x <- readNumber | Nothing => guess n  -- "ideally" doesn't mean "has to"
             case compare x n of
                  LT => do putStrLn "Too small"
                           guess n
                  EQ => do putStrLn "Well done!"
                           pure ()
                  GT => do putStrLn "Too big"
                           guess n

-- ex2
rndGuess : IO ()
rndGuess = do
  t <- time
  guess (mod (cast t) 100)

-- ex3
guess' : (target : Nat) -> (guesses : Nat) -> IO ()
guess' n g = do putStr ("Enter guess no. " ++ (show g) ++ ": ")
                Just x <- readNumber | Nothing => do
                  putStrLn "Invalid input"
                  guess' n g
                case compare x n of
                     LT => do putStrLn "Too small"
                              guess' n (g + 1)
                     EQ => do putStrLn "Well done!"
                              pure ()
                     GT => do putStrLn "Too big"
                              guess' n (g + 1)
rndGuess' : IO ()
rndGuess' = do t <- time
               guess' (mod (cast t) 100) 1

-- I wonder if we can make a 'parser' for IO () functions.
-- The idea being if we can automate the random guessing game.

myRepl : String -> (String -> String) -> IO ()
myRepl prompt f = do putStrLn prompt
                     input <- getLine
                     putStrLn (f input)
                     myRepl prompt f

myReplWith : a -> String -> (a -> String -> Maybe (String, a)) -> IO ()
myReplWith state prompt f = do
  putStrLn prompt
  input <- getLine
  -- this case statement is ugly.  Any way to replace it with a do notation?
  case f state input of
       Nothing => pure ()
       Just (output, newState) => do putStrLn output
                                     myReplWith newState prompt f

myRepl2 : String -> (String -> String) -> IO ()
myRepl2 prompt f = myReplWith () prompt (\_, inp => Just (f inp, ()))

-- Jump to ReadVect.idr

-- exercises
-- ex1
readToBlank : IO (List String)
readToBlank = do
  line <- getLine
  if line == ""
     then pure []
     else do lines <- readToBlank
             pure (line :: lines)

readFileName : IO String
readFileName = do
  putStr "Enter file name: "
  name <- getLine
  if name == ""
     then do putStrLn "Please enter a filename"
             readFileName
     else pure name

-- ex2
readAndSave : IO ()
readAndSave = do
  putStrLn "Enter text.  Enter a blank line to terminate."
  lines <- readToBlank
  filename <- readFileName
  Right _ <- writeFile filename $ concat (map (++ "\n") lines) |
    Left err => printLn err
  pure ()

-- ex3
-- Below is buggy.  Because fGetLine will return empty on the last line of the file.
--readFileLines : (file : File) -> IO (Maybe (n ** Vect n String))
--readFileLines file = do
--  ended <- fEOF file
--  if ended
--     then pure (Just (_ ** []))
--     else do Right line <- fGetLine file
--             | Left err => do printLn err
--                              pure Nothing
--             maybelines <- readFileLines file
--             case maybelines of
--                  Nothing => pure Nothing
--                  Just (_ ** lines) => pure (Just (_ ** line :: lines))
--

readFileLines : (file : File) -> IO (Maybe (n ** Vect n String))
readFileLines file = do
  Right line <- fGetLine file
  | Left err => do printLn err
                   pure Nothing
  iseof <- fEOF file
  if iseof
     then pure (Just (_ ** []))
     else do maybelines <- readFileLines file
             case maybelines of
                  Nothing => pure Nothing
                  Just (_ ** lines) => pure (Just (_ ** line :: lines))

readVectFile : (filename : String) -> IO (n ** Vect n String)
readVectFile filename = do
  Right file <- openFile filename Read
  | Left err => do printLn err
                   pure (_ ** [])
  maybelines <- readFileLines file
  case maybelines of
       Nothing => pure (_ ** [])
       Just res => pure res

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:
import Data.Vect
import Decidable.Equality

myExactLength : {m : _} -> (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
myExactLength len input = case decEq m len of
                                 Yes Refl => Just input
                                 No contra => Nothing


text:
-- ---------------------------------------------- [ DependentStateMachines.idr ]
-- Module      : Chapter.DependentStateMachines
-- Description : Definitions from Chapter 14 of Edwin Brady's book,
--               "Type-Driven Development with Idris."
-- --------------------------------------------------------------------- [ EOH ]
module Chapter.DependentStateMachines

import Data.Vect

-- ------------------------------------------ [ 14.1.1 Refining the Door Model ]

public export
data DoorResult = OK | Jammed

||| A door is either open or closed.
public export
data DoorState = ||| The door is closed.
                 DoorClosed
               | ||| The door is open.
                 DoorOpen

namespace Door

    public export
    data DoorCmd : (ty : Type) -> DoorState -> (ty -> DoorState) -> Type where
         Open : DoorCmd DoorResult DoorClosed
                                   (\res => case res of
                                                 OK     => DoorOpen
                                                 Jammed => DoorClosed)

         Close : DoorCmd () DoorOpen (const DoorClosed)
         RingBell : DoorCmd () DoorClosed (const DoorClosed)

         Display : String -> DoorCmd () state (const state)

         Pure : (res : ty) -> DoorCmd ty (state_fn res) state_fn
         (>>=) : DoorCmd a state1 state2_fn ->
               ((res : a) -> DoorCmd b (state2_fn res) state3_fn) ->
         DoorCmd b state1 state3_fn

logOpen : DoorCmd DoorResult DoorClosed
                             (\res => case res of
                                           OK     => DoorOpen
                                           Jammed => DoorClosed)
logOpen = do Display "Trying to open the door"
             OK <- Open | Jammed => do Display "Jammed"
                                       Pure Jammed
             Display "Success"
             Pure OK

-- -------------------------------------- [ 14.2.2 Defining a Type for the ATM ]

||| A PIN is exactly four characters.
PIN : Type
PIN = Vect 4 Char

||| The possible states of the ATM.
data ATMState = Ready | CardInserted | Session

||| The possible results of checking a PIN, valid or invalid.
data PINCheck = CorrectPIN | IncorrectPIN

data HasCard : ATMState -> Type where
     HasCI      : HasCard CardInserted
     HasSession : HasCard Session

namespace ATM

    data ATMCmd : (ty : Type) -> ATMState -> (ty -> ATMState) -> Type where
         InsertCard : ATMCmd ()   Ready        (const CardInserted)
         EjectCard  : {auto prf : HasCard state} ->
                      ATMCmd () state (const Ready)
         GetPIN     : ATMCmd PIN  CardInserted (const CardInserted)

         CheckPIN   : PIN -> ATMCmd PINCheck CardInserted
                               (\check => case check of
                                               CorrectPIN => Session
                                               IncorrectPIN => CardInserted)
         GetAmount : ATMCmd Nat state (const state)

         Dispense : (amount : Nat) -> ATMCmd () Session (const Session)

         Message : String -> ATMCmd () state (const state)
         Pure  : (res : ty) -> ATMCmd ty (state_fn res) state_fn
         (>>=) : ATMCmd a state1 state2_fn ->
                 ((res : a) -> ATMCmd b (state2_fn res) state3_fn) ->
                 ATMCmd b state1 state3_fn

atm : ATMCmd () Ready (const Ready)
atm = do InsertCard
         Message "Checking Card"
         case !(CheckPIN !GetPIN) of
              CorrectPIN   => do Dispense !GetAmount
                                 EjectCard
                                 Message "Please remove your card and cash"
              IncorrectPIN => do Message "Incorrect PIN"
                                 EjectCard

testPIN : Vect 4 Char
testPIN = ['1', '2', '3', '4']

readVect : (n : Nat) -> IO (Vect n Char)
readVect Z = do discard <- getLine
                pure []
readVect (S k) = do ch <- getChar
                    chs <- readVect k
                    pure (ch :: chs)

runATM : ATMCmd res inState outState_fn -> IO res
runATM InsertCard = do putStrLn "Please insert your card (press enter)"
                       x <- getLine
                       pure ()
runATM EjectCard = putStrLn "Card ejected"
runATM GetPIN = do putStr "Enter PIN: "
                   readVect 4
runATM (CheckPIN pin) = if pin == testPIN
                           then pure CorrectPIN
                           else pure IncorrectPIN
runATM GetAmount = do putStr "How much would you like? "
                      pure (cast !getLine)
runATM (Dispense amount) = putStrLn ("Here is " ++ show amount)

runATM (Message msg) = putStrLn msg
runATM (Pure res) = pure res
runATM (x >>= f) = do x' <- runATM x
                      runATM (f x')

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

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
module QAOA

import Data.Nat
import Data.Vect
import Graph
import Lemmas
import Unitary
import Control.Linear.LIO
import QStateT
import Injection
import LinearTypes
import Complex
import System.Random
import QuantumOp
import RandomUtilities

%default total

||| Vanilla QAOA : we use QAOA with a vanilla optimisation procedure to solve MAXCUT.

-------------------------QUANTUM CIRCUITS----------------------

||| The unitary operator induced by the mixing hamiltonian.
||| n    -- the arity of the operator
||| beta -- the rotation angle parameter
mixingUnitary : (n : Nat) -> (beta : Double) -> Unitary n
mixingUnitary n beta = tensorn n (RxGate beta)

||| Helper function for costUnitary
||| m              -- number of vertices of the input subgraph
||| n              -- number of remaining edges between current vertex and the rest
||| prf            -- proof witness that the number of vertices does not exceed the arity of the operator
||| gamma          -- the rotation parameter
||| edges          -- vector of edges that the current vertex is connected to
||| currentUnitary -- the currently constructed unitary operator
||| output         -- the final unitary operator
costUnitary' : {n : Nat} -> {m : Nat} -> {auto prf : n < m = True} ->
               (gamma : Double) -> (edges : Vect n Bool) -> (currentUnitary : Unitary m) -> Unitary m
costUnitary' _ [] currentUnitary = currentUnitary
costUnitary' {n = S k} gamma (False :: xs) currentUnitary =
  let proof1 = lemmaLTSuccLT k m
  in costUnitary' gamma xs currentUnitary
costUnitary' {n = S k} gamma (True  :: xs) currentUnitary =
  let proof1 = lemmaCompLT0 m (S k)
      proof2 = lemmaLTSuccLT k m
      cx     = CNOT 0 (S k) (IdGate {n = m})
      rzcx   = P gamma (S k) cx
      rest   = costUnitary' gamma xs currentUnitary
  in rest . cx . rzcx

||| The unitary operator induced by the cost hamiltonian.
||| n      -- the number of vertices of the input graph
||| graph  -- the input graph
||| gamma  -- rotation parameter
||| output -- the resulting unitary operator
costUnitary : {n : Nat} -> (graph: Graph n) -> (gamma : Double) -> Unitary n
costUnitary Empty _ = IdGate
costUnitary (AddVertex graph edges) gamma =
  let circuit = (IdGate {n = 1}) # (costUnitary graph gamma)
      proof1 = lemmaLTSucc n
  in costUnitary' gamma edges circuit

||| The iterated cost and mixing unitaries for QAOA_p
||| n       -- the number of vertices of the graph
||| p       -- the "p" parameter of QAOA_p, i.e., the number of iterations of the mixing and cost unitaries
||| betas   -- list of rotation parameters for the mixing hamiltonians
||| gammas  -- list of rotation parameters for the cost hamilitonians
||| graph   -- the input graph
||| output  -- the overall unitary operator of QAOA_p
QAOA_Unitary' : {n : Nat} ->
               (betas : Vect p Double) -> (gammas : Vect p Double) ->
               (graph: Graph n) ->
               Unitary n
QAOA_Unitary' [] [] g = IdGate
QAOA_Unitary' (beta :: betas) (gamma :: gammas) g =
  let circuit = QAOA_Unitary' betas gammas g
  in circuit . mixingUnitary n beta . costUnitary g gamma

||| The overall unitary operator for QAOA_p
||| n       -- the number of vertices of the graph
||| p       -- the "p" parameter of QAOA_p, i.e., the number of iterations of the mixing and cost unitaries
||| betas   -- list of rotation parameters for the mixing hamiltonians
||| gammas  -- list of rotation parameters for the cost hamilitonians
||| graph   -- the input graph
||| output  -- the overall unitary operator of QAOA_p
export
QAOA_Unitary : {n : Nat} ->
               (betas : Vect p Double) -> (gammas : Vect p Double) ->
               (graph: Graph n) ->
               Unitary n
QAOA_Unitary betas gammas graph = (QAOA_Unitary' betas gammas graph) . (tensorn n HGate)

-------------------------CLASSICAL PART------------------------

||| The (probabilistic) classical optimisation procedure for QAOA.
||| IO output allows us to use probabilistic optimisation procedures.
||| Given all previously observed information, determine new rotation angles for the next QAOA run.
||| Remark: we randomly generate the next rotation angles for simplicity.
|||
||| k             -- number of previous iterations of the algorithm
||| p             -- "p" parameter for QAOA_p
||| n             -- number of vertices of the input graph
||| graph         -- the input graph
||| previous_info -- previously used parameters and previously observed cuts from QAOA runs
||| IO output     -- new rotation angles for the next run of QAOA
classicalOptimisation : {p : Nat} ->
                       (graph : Graph n) ->
                       (previous_info : Vect k (Vect p Double, Vect p Double, Cut n)) ->
                       IO (Vect p Double, Vect p Double)
classicalOptimisation g ys = do
  betas <- randomVect p
  gammas <- randomVect p
  pure (betas,gammas)

-----------------------------QAOA------------------------------

||| Helper function for QAOA
|||
||| n      -- number of vertices of the input graph
||| p      -- the "p" parameter of QAOA_p
||| k      -- number of times we sample (the number of times we execute QAOA_p)
||| graph  -- input graph of the problem
||| output -- all observed cuts and all rotation angles from all the runs of QAOA
QAOA' : QuantumOp t =>
        {n : Nat} ->
        (k : Nat) -> (p : Nat) -> (graph : Graph n) ->
        IO (Vect k (Vect p Double, Vect p Double, Cut n))
QAOA' 0 p graph = pure []
QAOA' (S k) p graph = do
  previous_info <- QAOA' {t} k p graph
  (betas, gammas) <- classicalOptimisation graph previous_info
  let circuit = QAOA_Unitary betas gammas graph
  cut <- run (do
              qs <- newQubits {t} n
              qs <- applyUnitary qs circuit
              measureAll qs
              )
  pure $ (betas, gammas, cut) :: previous_info

||| QAOA for the MAXCUT problem. Given an input graph, return the best observed cut after some number of iterations.
|||
||| n      -- number of vertices of the input graph
||| p      -- the "p" parameter of QAOA_p
||| k      -- number of times we sample (the number of times we execute QAOA_p)
||| graph  -- input graph of the problem
||| output -- best observed cut from the execution of the algorithm
export
QAOA : QuantumOp t =>
       {n : Nat} ->
       (k : Nat) -> (p : Nat) -> Graph n ->
       IO (Cut n)
QAOA k p graph = do
  res <- QAOA' {t} k p graph
  let cuts = map (\(_, _, cut) => cut) res
  let (cut,size) = bestCut graph cuts
  pure cut

max_stars_repo_name: zamdzhiev/Qimaera

max_issues_repo_name: zamdzhiev/Qimaera

max_forks_repo_name: zamdzhiev/Qimaera


text:
||| Version of Maybe indexed by an `isJust' boolean
module Data.IMaybe

%default total

public export
data IMaybe : Bool -> Type -> Type where
  Just : a -> IMaybe True a
  Nothing : IMaybe False a

public export
fromJust : IMaybe True a -> a
fromJust (Just a) = a

public export
Functor (IMaybe b) where
  map f (Just a) = Just (f a)
  map f Nothing = Nothing

public export
Applicative (IMaybe True) where
  pure = Just
  Just f <*> Just x = Just (f x)


text:
module Common

public export
data API : Type -> Type -> Type where
  Api :  {input : Type} -> {output : Type} -> API input output

public export
Id : Type -> Type -> Type
Id s t = t


text:
-- ---------------------------------------------------------- [ CommonMark.idr ]
-- Module    : CommonMark.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]

module Text.Markup.Edda.Reader.CommonMark

import Data.AVL.Dict

import Effects
import Effect.File

import public Lightyear
import public Lightyear.Char
import public Lightyear.Strings

import Text.Markup.Edda.Model

import Text.Markup.Edda.Reader.Utils
import Text.Markup.Edda.Reader.Common

%access private
%default partial

-- ------------------------------------------------------------------ [ Inline ]

code : Parser (EddaRaw INLINE)
code = map (Raw CodeTy) (quoted '`') <?> "Code"

markup : MarkupTy -> String -> Parser (EddaRaw INLINE)
markup mTy c = do
    txt <- between (string c) (string c) (some mText)
    pure $ Mark mTy txt
  <?> "Markup"

bold : Parser (EddaRaw INLINE)
bold = markup BoldTy "**" <|> markup BoldTy "__" <?> "Bold"

emph : Parser (EddaRaw INLINE)
emph = markup EmphTy "*" <|> markup EmphTy "_" <?> "Emph"

expLink : Parser (EddaRaw INLINE)
expLink = do
  txt <- angles url
  pure $ Link ExposedTy txt Nil

hyper : Parser (EddaRaw INLINE)
hyper = do
  d <- brackets $ some (text <* spaces)
  uri  <- parens $ url
  let desc = intersperse (Punc ' ') d
  pure $ Link HyperTy uri (desc)

link : Parser (EddaRaw INLINE)
link = hyper <|> expLink <?> "Links"

inline : Parser (EddaRaw INLINE)
inline = text
     <|> link
     <|> bold
     <|> emph
     <|> code
     <|> punc
     <?> "Raw Inline"

figure : Parser (EddaRaw BLOCK)
figure = do
    char '!'
    d <- brackets $ some text
    let desc = intersperse (Punc ' ') d
    uri <- parens url
    let img = Link ExposedTy uri Nil
    endOfLine
    endOfLine
    pure (Figure (Just "") desc empty img)
  <?> "Figure"

-- ------------------------------------------------------------------- [ Lists ]
ulMarker : Parser ()
ulMarker = char' '+' <|> char' '-' <|> char' '*' <?> "UList Marker"

olMarker : Parser ()
olMarker = marker '.' <|> marker ')'
  where
    marker : Char -> Parser ()
    marker c = do
      some $ digit
      char c
      (satisfy isSpace)
      pure ()

-- @TODO Add coninuations
listItem : Parser () -> Parser (List (EddaRaw INLINE))
listItem mark = do
    mark
    space
    line <- manyTill inline endOfLine
    pure $ line

olist : Parser (EddaRaw BLOCK)
olist = do
    is <- some (listItem olMarker)
    endOfLine
    pure $ ListBlock NumberTy is

blist : Parser (EddaRaw BLOCK)
blist = do
    is <- some (listItem ulMarker)
    endOfLine
    pure $ ListBlock BulletTy is

list : Parser (EddaRaw BLOCK)
list = blist <|> olist

-- ------------------------------------------------------------------ [ Blocks ]

indentedcode : Parser (EddaRaw BLOCK)
indentedcode = identcode "\t" <|> identcode "    " <?> "Indented Code Block"
  where
    identcode : String -> Parser (EddaRaw BLOCK)
    identcode m = do
      ss <- some $ (string m *!> manyTill (anyChar) endOfLine)
      endOfLine
      let src = concatMap (\x => pack (List.(++) x ['\n'])) ss
      pure $ VerbBlock LiteralTy Nothing Nil empty src
     <?> "Indented Code"

fencedcode : Parser (EddaRaw BLOCK)
fencedcode = fencedcode' "```" <|> fencedcode' "~~~" <?> "Fenced Code Block"
  where
    fencedcode' : String -> Parser (EddaRaw BLOCK)
    fencedcode' m = do
        string m
        srcopts <- opt $ space *> manyTill (anyChar) endOfLine
        let as = dealWithSrcAttrs (convertOpts srcopts) empty
        src <- manyTill anyChar (string m)
        endOfLine
        pure $ VerbBlock ListingTy Nothing Nil as (pack src)
      <?> "Fenced Code Block: " ++ m

blockquote : Parser (EddaRaw BLOCK)
blockquote = do
    txt <- some $ (token ">" *!> manyTill inline endOfLine)
    endOfLine
    let p = concat txt
    pure $ TextBlock QuotationTy Nothing Nil empty p

-- ------------------------------------------------------------------- [ Paras ]
para : Parser (EddaRaw BLOCK)
para = do
    txt <- manyTill (inline) (endOfLine *> endOfLine)
    pure $ TextBlock ParaTy Nothing Nil empty txt
  <?> "Paragraphs"

paraLast : Parser (EddaRaw BLOCK)
paraLast = do
    txt <- manyTill inline (endOfLine *> spaces)
    pure $ TextBlock ParaTy Nothing Nil empty txt
  <?> "Filthy hack for last para"

hrule : Parser (EddaRaw BLOCK)
hrule = hrule' "***" <|> hrule' "---" <|> hrule' "___" <?> "hrules"
  where
    hrule' m = do
      string m
      endOfLine
      pure $ HRule

empty : Parser (EddaRaw BLOCK)
empty = do
  endOfLine
  endOfLine
  pure $ Empty

header : Parser (EddaRaw BLOCK)
header = char '#' >! do
    depth <- opt (many $ char '#')
    spaces
    title <- manyTill (inline) (endOfLine)
    endOfLine
    let d = length (fromMaybe Nil depth) + 1
    pure (Heading d Nothing title empty)
  <?> "Header"

block : Parser (EddaRaw BLOCK)
block = header
    <|> blockquote <|> indentedcode <|> fencedcode
    <|> list <|> figure <|> hrule <|> para <|> empty
    <?> "Block"

parseCommonMark : Parser (EddaRaw DOC)
parseCommonMark = do
    txt <- some block
    let txt' = intersperse (Empty) txt
    pure $ Doc Nil empty (txt' ++ [Empty])
  <?> "Raw Common Mark"

-- -------------------------------------------------------------------- [ Read ]

namespace Doc
  export
  fromCommonMarkE : String -> Eff (Either String (Edda DOC)) [FILE ()]
  fromCommonMarkE = assert_total $ readEddaFileE parseCommonMark

  export
  fromCommonMark : String -> IO (Either String (Edda DOC))
  fromCommonMark = assert_total $ readEddaFile parseCommonMark

namespace Snippet
  namespace Inline
    export
    fromCommonMark : String -> Either String (Edda SNIPPET)
    fromCommonMark = assert_total $ readEddaSentance inline

  namespace Para
    export
    fromCommonMark : String -> Either String (Edda SNIPPET)
    fromCommonMark s = assert_total $ readEddaBody block (s ++ "\n\n")

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

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
module Main

import Data.Vect

repeat : (n : Nat) -> a -> Vect n a
repeat Z _ = Nil
repeat (S k) x = x :: (repeat k x)

main : IO ()
main = putStrLn (show (repeat 4 "a"))

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
module Main

import Error.Data
import Error.Pretty

import Syntax.Lexer
import Syntax.Reader
import Syntax.Parser
import Syntax.Tokens
import Syntax.Term

import Typing.Infer

import Data.List
import Loc
import System.File

import Control.App
import Control.App.Console
import Control.App.FileIO

compile : String -> String -> IO ()
compile fileName contents =
  let res = (filter (not . isUseless . snd) <$> lex contents)
              >>= readToTerm
              >>= (parseProgram "teste.lsp") in
  case res of
    Left res => print $ (MkErrorData fileName contents res)
    Right (MkProgram s t d r) =>
      let res = traverse runInference d in
      case res of
        Right e => print (map snd e)
        Left e  => print e

main : IO ()
main = do
  res <- readFile "teste.lsp"
  case res of
    Left res  => print "File not found!"
    Right res => compile "teste.lsp" res

max_stars_repo_name: felipegchi/Yurei

max_issues_repo_name: felipegchi/Yurei

max_forks_repo_name: felipegchi/Yurei


text:
{-
  Calulator parser

  number ::= [ "-" ] digit { digit }.
  digit  ::= "0" | "1" | ... | "8" | "9".
  expr   ::= term { addop term }.
  term   ::= factor { mulop factor }.
  factor ::= "(" expr ")" | number.
  addop  ::= "+" | "-".
  mulop  ::= "*".

-}
module Test.Calculator

import NanoParsec.Parser
import NanoParsec.Combinators

data Expr = Add Expr Expr
          | Mul Expr Expr
          | Sub Expr Expr
          | Lit Int
          deriving Show

eval :: Expr -> Int
eval ex = case ex of
    Add a b -> eval a + eval b
    Mul a b -> eval a * eval b
    Sub a b -> eval a - eval b
    Lit n   -> n

int :: Parser Expr
int = number >>= \n -> return (Lit n)

expr :: Parser Expr
expr = term `chainl1` addop

term :: Parser Expr
term = factor `chainl1` mulop

factor :: Parser Expr
factor = int <|> parens expr

infixOp :: String -> (a -> a -> a) -> Parser (a -> a -> a)
infixOp x f = reserved x >>= \_ => return f

addop :: Parser (Expr -> Expr -> Expr)
addop = (infixOp "+" Add) <|> (infixOp "-" Sub)

mulop :: Parser (Expr -> Expr -> Expr)
mulop = infixOp "*" Mul

max_stars_repo_name: stallmanifold/idris-nanoparsec

max_issues_repo_name: lambdaxymox/idris-nanoparsec

max_forks_repo_name: lambdaxymox/idris-nanoparsec


text:
module Main

import Resimp

data Purpose = Reading | Writing

pstring : Purpose -> String
pstring Reading = "r"
pstring Writing = "w"

data FILE : Purpose -> Type where
    OpenH : File -> FILE p

syntax ifM [test] then [t] else [e]
    = test >>= (\b => if b then t else e)

open : String -> (p:Purpose) -> Creator (Either () (FILE p))
open fn p = ioc (do h <- fopen fn (pstring p)
                    ifM validFile h
                        then return (Right (OpenH h))
                        else return (Left ()))

close : FILE p -> Updater ()
close (OpenH h) = iou (closeFile h)

readLine : FILE Reading -> Reader String
readLine (OpenH h) = ior (fread h)

eof : FILE Reading -> Reader Bool
eof (OpenH h) = ior (feof h)

syntax rclose [h]    = Update close h
syntax rreadLine [h] = Use readLine h
syntax reof [h]      = Use eof h

syntax rputStrLn [s] = Lift (putStrLn s)

syntax if opened [f] then [e] else [t] = Check f t e

--------

readH : String -> RES ()
readH fn = res (do let x = open fn Reading
                   if opened x then
                       do While (do e <- reof x
                                    Return (not e))
                                (do str <- rreadLine x
                                    Lift (putStr str))
                          rclose x
                       else rputStrLn "Error")

main : IO ()
main = run (readH "test")

max_stars_repo_name: silky/idris-demos

max_issues_repo_name: silky/idris-demos

max_forks_repo_name: silky/idris-demos


text:
module Text.Markdown.Options

-- Default ----------------------------------------------------------

class Default a where
      def : a

-- ReaderOptions ----------------------------------------------------

record ReaderOptions : Type where
       MkReaderOptions : (readerStandalone : Bool) ->
                         ReaderOptions

instance Default ReaderOptions
         where def = MkReaderOptions
                        {readerStandalone = False}

-- WriterOptions ----------------------------------------------------

record WriterOptions : Type where
       MkWriterOptions : (writerStandalone : Bool) ->
                         WriterOptions

instance Default WriterOptions
         where def = MkWriterOptions
                        {writerStandalone = False}

max_stars_repo_name: soimort/idris-commonmark

max_issues_repo_name: soimort/idris-commonmark

max_forks_repo_name: soimort/idris-commonmark


text:
module System.Info

%default total

%extern prim__os : String
%extern prim__codegen : String

export
os : String
os = prim__os

export
codegen : String
codegen = prim__codegen

export
isWindows : Bool
isWindows = os `elem` ["windows", "mingw32", "cygwin32"]

%foreign "C:idris2_getNProcessors, libidris2_support, idris_support.h"
         "jvm:getAvailableProcessors(int),io/github/mmhelloworld/idrisjvm/runtime/Runtime"
prim__getNProcessors : PrimIO Int

export
getNProcessors : IO (Maybe Nat)
getNProcessors = do
  i <- fromPrim prim__getNProcessors
  pure (if i < 0 then Nothing else Just (integerToNat (cast i)))


text:
module Katalan

import Data.Nat

katalanTheorem : {x, y, z, t : Nat} -> x `GT` 1 -> y `GT` 1 -> z `GT` 1 -> t `GT` 1 ->
                 (x `power` y) = 1 + (z `power` t) -> (x=3, t=3, y=2, z=2)

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module System.REPL.Extra

import System.File

||| Process input from an open file handle, while maintaining a state.
||| @ state the input state
||| @ onRead the function to run on reading a line, returning a String to
||| output and a new state
||| @ onEOF the function to run on reaching end of file, returning a String
||| to output
partial
export
processHandle : File ->
                (state : a) ->
                (onRead : a -> String -> (String, a)) ->
                (onEOF : a -> String) ->
                IO ()
processHandle h acc onRead onEOF
   = fEOF h >>= processHandle'
   where
     processHandle' : Bool -> IO ()
     processHandle' iseof =
       if iseof
       then putStr (onEOF acc)
       else do Right x <- fGetLine h
                   | Left err => putStr (onEOF acc)
               let (out, acc') = onRead acc x
               putStr out
               processHandle h acc' onRead onEOF

||| Process input from the standard input stream, while maintaining a state.
||| @ state the input state
||| @ onRead the function to run on reading a line, returning a String to
||| output and a new state
||| @ onEOI the function to run on reaching end of input, returning a String
||| to output
partial
export
processStdin : (state : a) ->
               (onRead : a -> String -> (String, a)) ->
               (onEOI : a -> String) -> IO ()
processStdin = processHandle stdin

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
module Data.SOP.SOP

import Data.List.Elem

import Data.SOP.NP
import Data.SOP.NS
import Data.SOP.POP
import Data.SOP.Utils
import Data.SOP.Interfaces
import Data.Maybe

import Decidable.Equality

%default total

||| A sum of products.
|||
||| The elements of the (inner) products
||| are applications of the parameter f. The type SOP_ is indexed by the list of
||| lists that determines the sizes of both the (outer) sum and all the (inner)
||| products, as well as the types of all the elements of the inner products.
|||
||| A SOP I reflects the structure of a normal Idris datatype. The sum structure
||| represents the choice between the different constructors, the product structure
||| represents the arguments of each constructor.
public export
data SOP_ : (k : Type) -> (f : k -> Type) -> (kss : List $ List k) -> Type where
  MkSOP : NS_ (List k) (NP_ k f) kss -> SOP_ k f kss

||| Type alias for `SOP_` with type parameter `k` being
||| implicit. This reflects the kind-polymorphic data type
||| in Haskell.
public export
SOP : {k : Type} -> (f : k -> Type) -> (kss : List (List k)) -> Type
SOP = SOP_ k

public export %inline
unSOP : SOP_ k f kss -> NS_ (List k) (NP_ k f) kss
unSOP (MkSOP ns) = ns

--------------------------------------------------------------------------------
--          Specialized Interface Functions
--------------------------------------------------------------------------------

||| Specialiced version of `hmap`
public export
mapSOP : (fun : forall a . f a -> g a) -> SOP f kss -> SOP g kss
mapSOP fun = MkSOP . mapNS (\p => mapNP fun p) . unSOP

||| Specialization of `hap`
public export
hapSOP : POP (\a => f a -> g a) kss -> SOP f kss -> SOP g kss
hapSOP (MkPOP fs) = MkSOP . hliftA2 (\p => hapNP p) fs . unSOP

||| Specialization of `hfoldl`
public export
foldlSOP : (fun : acc -> el -> acc) -> acc -> SOP (K el) kss -> acc
foldlSOP fun acc (MkSOP $ Z vs) = foldlNP fun acc vs
foldlSOP fun acc (MkSOP $ S x)  = foldlSOP fun acc (MkSOP x)

||| Specialization of `hfoldr`
public export %inline
foldrSOP : (fun : el -> Lazy acc -> acc) -> Lazy acc -> SOP (K el) kss -> acc
foldrSOP fun acc (MkSOP $ Z vs) = foldrNP fun acc vs
foldrSOP fun acc (MkSOP $ S x)  = foldrSOP fun acc (MkSOP x)

||| Specialization of `hsequence`
public export
sequenceSOP : Applicative g => SOP (\a => g (f a)) kss -> g (SOP f kss)
sequenceSOP = map MkSOP . sequenceNS . mapNS (\p => sequenceNP p) . unSOP

||| Specialization of `hcollapse`
public export
collapseSOP : SOP (K a) kss -> List a
collapseSOP = collapseNS . mapNS (\v => collapseNP v) . unSOP

--------------------------------------------------------------------------------
--          Injections
--------------------------------------------------------------------------------

||| An injection into an n-ary sum of products takes an n-ary product of
||| the correct type and wraps it in one of the sum's possible choices.
public export
0 InjectionSOP : (f : k -> Type) -> (kss : List $ List k) -> (vs : List k) -> Type
InjectionSOP f kss vs = NP f vs -> K (SOP f kss) vs

||| The set of injections into an n-ary sum `NS f ks` can
||| be wrapped in a corresponding n-ary product.
public export
injectionsSOP : {kss : _} -> NP_ (List k) (InjectionSOP f kss) kss
injectionsSOP = hmap (MkSOP .) $ injections {ks = kss}

||| Applies all injections to a product of products of values.
|||
||| This is not implemented in terms of `injectionsSOP` for the
||| following reason: Since we have access to the structure
||| of the product of products and thus `kss`, we do not need a
||| runtime reference of `kss`. Therefore, when applying
||| injections to a product of products, prefer this function
||| over a combination involving `injectionsSOP`.
public export
apInjsPOP_ : POP f kss -> NP (K $ SOP f kss) kss
apInjsPOP_  = mapNP (\ns => MkSOP ns) . apInjsNP_ . unPOP

||| Alias for `collapseNP . apInjsPOP_`
public export
apInjsPOP : POP f kss -> List (SOP f kss)
apInjsPOP = collapseNP . apInjsPOP_

||| Injects a product into an n-ary sum of products.
public export
injectSOP : {0 ks : List k} -> (v : NP f ks) -> {auto prf : Elem ks kss} -> SOP f kss
injectSOP v = MkSOP $ inject v

||| Tries to extract a product of the given type from an
||| n-ary sum of products.
public export
extractSOP :  (0 ks : List k)
           -> SOP f kss
           -> {auto prf : Elem ks kss}
           -> Maybe (NP f ks)
extractSOP ks (MkSOP ns) = extract ks {prf} ns

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

public export %inline
HFunctor k (List $ List k) (SOP_ k) where hmap = mapSOP

public export %inline
HAp k (List $ List k) (POP_ k) (SOP_ k) where hap = hapSOP

public export %inline
HFold k (List $ List k) (SOP_ k) where
  hfoldl = foldlSOP
  hfoldr = foldrSOP

public export
HSequence k (List $ List k) (SOP_ k) where hsequence = sequenceSOP

public export %inline
HCollapse k (List $ List k) (SOP_ k) List where hcollapse = collapseSOP

public export
POP (Eq . f) kss => Eq (SOP_ k f kss) where
  MkSOP a == MkSOP b = a == b

public export
POP (Ord . f) kss => Ord (SOP_ k f kss) where
  compare (MkSOP a) (MkSOP b) = compare a b

public export
POP (Show . f) kss => Show (SOP_ k f kss) where
  showPrec p (MkSOP ns) = showCon p "MkSOP" (showArg ns)

||| Sums of products have instances of `Semigroup` and `Monoid`
||| only when they consist of a single choice, which must itself be
||| a `Semigroup` or `Monoid`.
public export
POP (Semigroup . f) [ks] => Semigroup (SOP_ k f [ks]) where
  MkSOP a <+> MkSOP b = MkSOP $ a <+> b

||| Sums of products have instances of `Semigroup` and `Monoid`
||| only when they consist of a single choice, which must itself be
||| a `Semigroup` or `Monoid`.
public export
POP (Monoid . f) [ks] => Monoid (SOP_ k f [ks]) where
  neutral = MkSOP neutral

private
mkSOPInjective : MkSOP a = MkSOP b -> a = b
mkSOPInjective Refl = Refl

public export
POP (DecEq . f) kss => DecEq (SOP_ k f kss) where
  decEq (MkSOP a) (MkSOP b) with (decEq a b)
    decEq (MkSOP a) (MkSOP a) | Yes Refl   = Yes $ cong MkSOP Refl
    decEq (MkSOP a) (MkSOP b) | No  contra = No (contra . mkSOPInjective)

--------------------------------------------------------------------------------
--          Examples and Tests
--------------------------------------------------------------------------------

neutralTest : SOP I [[String, Maybe Int],[()]]
neutralTest = hcpure Monoid neutral

hapTest : SOP Maybe [[String,Int]] -> SOP I [[String,Int]]
hapTest = hap (MkPOP $ [[fromMaybe "foo", const 12]])


text:
module System.Info

%extern prim__os : String
%extern prim__codegen : String

export
os : String
os = prim__os

export
codegen : String
codegen = prim__codegen

export
isWindows : Bool
isWindows = os `elem` ["windows", "mingw32", "cygwin32"]


text:
module Parser.Rule.Package

import public Parser.Lexer.Package
import public Parser.Rule.Common

import Data.List

import Core.Name.Namespace

%default total

public export
Rule : Type -> Type
Rule = Rule Token

public export
PackageEmptyRule : Type -> Type
PackageEmptyRule = EmptyRule Token

export
equals : Rule ()
equals = terminal "Expected equals"
                      (\x => case x.val of
                                  Equals => Just ()
                                  _ => Nothing)

export
eoi : Rule ()
eoi = terminal "Expected end of input"
               (\x => case x.val of
                           EndOfInput => Just ()
                           _ => Nothing)

export
exactProperty : String -> Rule String
exactProperty p = terminal ("Expected property " ++ p)
                           (\x => case x.val of
                                       DotSepIdent Nothing p' =>
                                         if p == p' then Just p
                                         else Nothing
                                       _ => Nothing)

export
stringLit : Rule String
stringLit = terminal "Expected string"
                     (\x => case x.val of
                                 StringLit str => Just str
                                 _ => Nothing)

export
namespacedIdent : Rule (Maybe Namespace, String)
namespacedIdent = terminal "Expected namespaced identifier"
                           (\x => case x.val of
                                       DotSepIdent ns n => Just (ns, n)
                                       _ => Nothing)

export
moduleIdent : Rule ModuleIdent
moduleIdent = terminal "Expected module identifier"
                       (\x => case x.val of
                                   DotSepIdent ns m => Just $ nsAsModuleIdent (mkNestedNamespace ns m)
                                   _ => Nothing)

export
packageName : Rule String
packageName = terminal "Expected package name"
                       (\x => case x.val of
                                   DotSepIdent Nothing str =>
                                     if isIdent AllowDashes str then Just str
                                     else Nothing
                                   _ => Nothing)

sep' : Rule ()
sep' = terminal "Expected separator"
                (\x => case x.val of
                            Separator => Just ()
                            _ => Nothing)

export
sep : Rule t -> Rule (List t)
sep rule = sepBy1 sep' rule


text:
-- Idea: use types as first class language construct: i.e. allow them to be passed as arguments,
-- returned from functions and assigned to variables.
-- Idea first-class language constructs:
-- let's start with C:
-- numbers are first-class
-- pointers are first-class
-- arrays are not (can not be returned or assigned)
-- functions are not (you have function pointers but you can not have a
--                    function that returns a function)
-- Python:
-- numbers, lists, functions, but not types.

-- Types are used at multiple levels:
-- in assembley they represent how a register should be interpreted
--   (signed, unsigned, 16, 32 bit, etc, float, double, etc)
-- at compiler level, how different parts of the program interpret data at runtime
--   (how many bytes to push to the stash for another function to act on them)
-- by the programmer: to abstract away various concepts that they use when
--   designing the program (humans don't think in numbers, they think in
--                          abstractions)

-- What is type driven development: use types as a "plan".  In the same way as we
-- use UML diagrams, use types to specify the input and output of functions.

-- Type, define refine loop:
--  start with generic type (say Matrix), define your adder function,
--  notice invalid cases => refine your type.

-- Exercise
-- Vect n elem -> Vect n elem
--  reverse function
-- Vect n elem -> Vect (n * 2) elem
--  duplicate each element?
-- Vect (1 + n) elem -> Vect n elem
--  remove an element
-- Note: this is something we can not do in most other langauges (o.l.):
--  specify Vect (1 + n) elem as a type
-- Bounded n, Vect n elem -> elem
--  get the nth element.
-- Note: this starts illustrating the power of dependent types:
--  Bounded n is a property, meaning it is a type that poves that
--  the number is between 0 and n-1.  We can not express this in o.l.

-- Why pure functions?  Super easy to debug and to reason about:
-- output based only on inputs.

-- Environment setup: vim-idris
-- to open idris-response buffer, <LocalLeader>i
-- if closed, just :b idris-response
-- bindings:
-- t: type
-- e: eval window
-- r: reload and typecheck
-- h: help
--
-- d: define
-- c: case split

module Chapter1

main : IO ()
main = putStrLn "Hello, Idris World!"

-- Holes
main2 : IO ()
main2 = putStrLn ?greeting  -- position cursor on ?greeting and ask for type.

main3 : IO ()
--main3 = putStrLn 'x'  --type error
--main3 = putStrLn (?convert 'x')
main3 = putStrLn (cast 'x')

-- First class types
StringOrInt : Bool -> Type  -- leader_d for define
--StringOfInt x = ?StringOfInt_rhs  -- leader_c for case split
StringOrInt False = String
StringOrInt True = Int  -- leader_c for case split

getStringOrInt : (x : Bool) -> StringOrInt x  -- here we go :)
getStringOrInt False = "Ninety four"
getStringOrInt True = 94

valToString : (x : Bool) -> StringOrInt x -> String
valToString x y = case x of
                       True => cast val
                       False => val


text:
module Term

import Data.Fin

%logging 1
%logging declare.def 3

mutual

  data Bdr : (cut : Bool) -> (vars : Nat) -> Type where
    Lam : Bdr cut vars
    Pi  : Chk cut vars -> Bdr cut vars

  -- Checkable terms (i.e. introduction forms)
  data Chk : (cut : Bool) -> (vars : Nat) -> Type where
    Bnd : Bdr cut vars -> Chk cut (S vars) -> Chk cut vars
    Emb : Syn cut vars -> Chk cut n

  -- Synthesisable terms (i.e. elimination forms)
  data Syn : (cut : Bool) -> (vars : Nat) -> Type where
    Var : Fin vars -> Syn cut vars
    App : Syn cut vars -> Chk cut vars -> Syn cut vars
    Cut : Chk True vars -> Typ True vars -> Syn True vars

  Typ : (cut : Bool) -> (vars : Nat) -> Type
  Typ = Chk

Term : Nat -> Type
Term = Chk True

NF : Nat -> Type
NF = Chk False


text:
module Ord

record Album where
    constructor MkAlbum
    artist : String
    title : String
    year : Integer

Eq Album where
  (==) (MkAlbum a t y) (MkAlbum a' t' y') = a == a' && t == t' && y == y'

Ord Album where
  compare (MkAlbum a t y) (MkAlbum a' t' y') = case compare a a' of
                                                    EQ => case compare y y' of
                                                               EQ => compare t t'
                                                               d_y => d_y
                                                    d_a => d_a

Show Album where
  show (MkAlbum artist title year) = title ++ " by " ++ artist ++ " (Released on: " ++ show year ++ ")"

help : Album
help = MkAlbum "The Beatles" "Help" 1965

rubbersoul : Album
rubbersoul = MkAlbum "The Beatles" "Rubber Soul" 1965

clouds : Album
clouds = MkAlbum "Joni Mitchell" "Clouds" 1969

hunkydory : Album
hunkydory = MkAlbum "David Bowie" "Hunky Dory" 1971

heroes : Album
heroes = MkAlbum "David Bowie" "Heroes" 1977

collection : List Album
collection = [help, rubbersoul, clouds, hunkydory, heroes]

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

-- Ex. 7_1
Eq Shape where
  (==) (Triangle x z) (Triangle y w) = x == y && z == w
  (==) (Rectangle x z) (Rectangle y w) = x == y && z == w
  (==) (Circle x) (Circle y) = x == y
  (==) _ _ = False

-- Ex. 7_2

getArea : Shape -> Double
getArea (Triangle x y) = (x * y) / 2
getArea (Rectangle x y) = x * y
getArea (Circle r) = pi * r * r

Ord Shape where
  compare x y = let sa1 = getArea x
                    sa2 = getArea y
                    in compare sa1 sa2

testShapes : List Shape
testShapes = [Circle 3, Triangle 3 9, Rectangle 2 6, Circle 4, Rectangle 2 7]


text:
module Gen.Env

import Data.SortedMap

||| An Environment is a correspondence between "key" and "value" type
public export
Environment : Type -> Type -> Type
Environment i a = SortedMap i a
-- Environment i a = List $ Pair i a

max_stars_repo_name: totalscript/totalscript

max_issues_repo_name: totalscript/totalscript

max_forks_repo_name: totalscript/totalscript


text:
-- trying to prove that everything is equal to Refl

total
all_is_Refl : (typ : Type) -> (a : typ) -> (p : (a = a)) -> (p = Refl)
all_is_Refl typ a Refl = Refl


text:
module Data.Time.LocalTime.Internal.TimeZone

export
record TimeZone where
  constructor MkTimeZone
  timeZoneMinutes: Int
  timeZoneSummaryOnly: Bool
  timeZoneName: String

-- TODO: Implement TimeZone conversion functions

max_stars_repo_name: gdevanla/idris-time

max_issues_repo_name: gdevanla/idris-time

max_forks_repo_name: gdevanla/idris-time


text:
module Main

import Data.Vect
import Go

%default total

-- XXX why is that required
partial
go : GIO () -> GIO ()
go action = gocall (Function "Go") (Raw (GIO ()) -> GIO ()) (MkRaw action)

-- Some easy string functions to test the FFI

out : String -> GIO ()
out s = gocall (Function "print") (String -> GIO ()) s

-- %include will be translated to imports
%include Go "strings"
upper : String -> String
upper s = unsafePerformIO $
  gocall (Function "strings.ToUpper") (String -> GIO String) s

trim : String -> String -> String
trim s cutset = unsafePerformIO $
  gocall (Function "strings.Trim") (String -> String -> GIO String) s cutset

-- Some other Idris niceties

fourInts : Vect 4 Int
fourInts = [428, 1, 2, 3]

isEven : Nat -> Bool
isEven Z = True
isEven (S k) = not (isEven k)

forLoop : List a -> (a -> GIO ()) -> GIO ()
forLoop [] f = pure ()
forLoop (x :: xs) f = do
  f x
  forLoop xs f

syntax for {x} "in" [xs] ":" [body] = forLoop xs (\x => body)

partial
main : GIO ()
main = do
  go $ for x in [1..10]:
    putStrLn' $ "Hello from goroutine " ++ show x
  out "foo\n"
  print' (isEven 4)
  putStrLn' ""
  print' fourInts

  for x in [1..20]:
    putStrLn' $ "Hello from main " ++ show x

  putStrLn' $ upper "foo"
  putStrLn' $ trim "foobar" "fr"

max_stars_repo_name: Trundle/idris-go

max_issues_repo_name: Trundle/idris-go

max_forks_repo_name: Trundle/idris-go


text:
-- ------------------------------------------------------------ [ Commands.idr ]
-- Module    : Commands.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Sif.Commands

import Lightyear
import Lightyear.Char
import Lightyear.Strings

import Sif.Types
import Sif.DSL.Parser.Common
import Sif.DSL.Parser.Utils

-- -------------------------------------------------------------- [ DIrectives ]

%default partial
%access private

-- ---------------------------------------------------------------- [ Commands ]
public export
data SifCMD : Type where
  ShowPattern : Nat -> Maybe SifOutFormat -> Maybe String -> SifCMD
  ListLib     : SifCMD
  EvalPattern : Nat -> SifCMD
  CheckExtPattern : String -> String -> SifCMD
  PreludeLoad : Maybe String -> SifCMD
  Quit        : SifCMD
  Help        : SifCMD

export
showHelp : String
showHelp = """
Command                 | Description
------------------------|-------------------------------------------------------
:list                   | List library contents
:display n              | Show pattern identified by index.
:eval n                 | Evaluate pattern identified by index.
:convert n fmt          | Show pattern using given format.
:save n fmt "fname"     | Save pattern in given format to file specified.
:chkPattern "probFile"  | Check externally defined pattern.
            "solFile"   |
:load "dirname"         | Replace prelude.
:reload                 | Reload prelude.
:quit :q :exit          | Quit the repl
:? :help                | Show this help
"""

covering
export
getCmdIndex : SifCMD -> Maybe Nat
getCmdIndex Help                  = Nothing
getCmdIndex Quit                  = Nothing
getCmdIndex ListLib               = Nothing
getCmdIndex (ShowPattern n _ _)   = Just n
getCmdIndex (EvalPattern n)       = Just n
getCmdIndex (CheckExtPattern _ _) = Nothing
getCmdIndex (PreludeLoad _)       = Nothing

display : Parser SifCMD
display = do
    string ":display"
    space
    i <- integer
    pure $ ShowPattern (cast $ abs i) (Just COMPACT) Nothing
  <?> "Show Pattern"

convert : Parser SifCMD
convert = do
    string ":convert"
    space
    i <- integer
    space
    fmt <- ident
    pure $ ShowPattern (cast $ abs i) (readOutFMT fmt) Nothing
  <?> "Save Pattern"

list : Parser SifCMD
list = do
    string ":list"
    pure ListLib
  <?> "List libs"

save : Parser SifCMD
save = do
    string ":save"
    space
    i <- integer
    space
    fmt <- ident
    space
    fname <- ident
    pure $ ShowPattern (cast $ abs i) (readOutFMT fmt) (Just fname)
  <?> "Save Pattern"

eval : Parser SifCMD
eval = do
    string ":eval"
    space
    i <- integer
    pure $ EvalPattern (cast $ abs i)
  <?> "Eval Command"

quit : Parser SifCMD
quit = (string ":q"    *> return Quit)
      <|> (string ":quit" *> return Quit)
      <|> (string ":exit" *> return Quit)

help : Parser SifCMD
help = (string ":?"    *> return Help)
   <|> (string ":help" *> return Help)

check : Parser SifCMD
check = do
    keyword ":check"
    p <- quoted '"'
    space
    s <- quoted '"'
    pure $ CheckExtPattern p s

load : Parser SifCMD
load = (do keyword ":load"; dir <- quoted '"'; return (PreludeLoad (Just dir)) )
    <|> (keyword ":r" *> return (PreludeLoad Nothing))
    <|> (keyword ":reload" *> return (PreludeLoad Nothing))
    <?> "Loading"

cmd : Parser SifCMD
cmd = display
  <|> list
  <|> convert
  <|> save
  <|> eval
  <|> quit
  <|> load
  <|> check
  <|> help
  <?> "Command"

export
parseCMD : String -> Either String SifCMD
parseCMD s = parse cmd s

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
{-
  SOURCE:  https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/Complex.idr
  LICENSE: https://raw.githubusercontent.com/idris-lang/Idris-dev/master/LICENSE
  (c) 2012 Copyright Mekeor Melire
-}

module Complex

--%access public export

------------------------------ Rectangular form

infix 6 :+
public export
data Complex a = (:+) a a

public export
realPart : Complex a -> a
realPart (r:+i) = r

public export
imagPart : Complex a -> a
imagPart (r:+i) = i

public export
implementation Eq a => Eq (Complex a) where
    (==) a b = realPart a == realPart b && imagPart a == imagPart b

public export
implementation Show a => Show (Complex a) where
    showPrec d (r :+ i) = showParens (d >= plus_i) $ showPrec plus_i r ++ " :+ " ++ showPrec plus_i i
      where plus_i : Prec
            plus_i = User 6

-- when we have a type class 'Fractional' (which contains Double),
-- we can do:
{-
implementation Fractional a => Fractional (Complex a) where
    (/) (a:+b) (c:+d) = let
                          real = (a*c+b*d)/(c*c+d*d)
                          imag = (b*c-a*d)/(c*c+d*d)
                        in
                          (real:+imag)
-}

------------------------------ Polarform
public export
mkPolar : Double -> Double -> Complex Double
mkPolar radius angle = radius * cos angle :+ radius * sin angle

public export
cis : Double -> Complex Double
cis angle = cos angle :+ sin angle

public export
magnitude : Complex Double -> Double
magnitude (r:+i) = sqrt (r*r+i*i)

public export
atan2 : Double -> Double -> Double
atan2 y x = 2 * atan (y / (sqrt (y*y+x*x) + x))

public export
phase : Complex Double -> Double
phase (x:+y) = atan2 y x

------------------------------ Conjugate
public export
conjugate : Neg a => Complex a -> Complex a
conjugate (r:+i) = (r :+ (0-i))

public export
implementation Functor Complex where
    map f (r :+ i) = f r :+ f i

-- We can't do "implementation Num a => Num (Complex a)" because
-- we need "abs" which needs "magnitude" which needs "sqrt" which needs Double
public export
implementation Num (Complex Double) where
    (+) (a:+b) (c:+d) = ((a+c):+(b+d))
    (*) (a:+b) (c:+d) = ((a*c-b*d):+(b*c+a*d))
    fromInteger x = (fromInteger x:+0)

{-public export
implementation Neg (Complex Double) where
    negate = map negate
    (-) (a:+b) (c:+d) = ((a-c):+(b-d))
    abs (a:+b) = (magnitude (a:+b):+0)
-}


text:
-- ----------------------------------------------------------------- [ Eff.idr ]
-- Module    : Eff.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]

module Data.DList.Eff

import Effects

import Data.DList

%access export

mapDListE : ({a : aTy} -> elemTy a -> {xs} EffM m b)
         -> DList aTy elemTy as
         -> {xs} EffM m (List b)
mapDListE f Nil       = pure List.Nil
mapDListE f (x :: xs) = with List [| f x :: mapDListE f xs |]

foldrE : ({a : aTy} -> elemTy a -> p -> {xs} EffM m p)
     -> p
     -> DList aTy elemTy as
     -> {xs} EffM m p
foldrE f init Nil     = pure init
foldrE f init (x::xs) = do
    ires <- foldrE f init xs
    pure $ !(f x ires)

foldlE : ({a : aTy} -> p -> elemTy a -> {xs} EffM m p)
      -> p
      -> DList aTy elemTy as
      -> {xs} EffM m p
foldlE f init Nil     = pure init
foldlE f init (x::xs) = do
    ires <- f init x
    pure $ !(foldlE f ires xs)

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

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


text:
module BTree

public export
data BTree a = Leaf
             | Node (BTree a) a (BTree a)

export
insert : Ord a => a -> BTree a -> BTree a
insert x Leaf = Node Leaf x Leaf
insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
                                   else (Node l v (insert x r))

export
toList : BTree a -> List a
toList Leaf = []
toList (Node l v r) = BTree.toList l ++ (v :: BTree.toList r)

export
toTree : Ord a => List a -> BTree a
toTree [] = Leaf
toTree (x :: xs) = insert x (toTree xs)

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module Network.Curl.Prim.Global

-------------------------------------------------
-- Global
-------------------------------------------------
-- curl_global_cleanup
-- curl_global_init
-- curl_global_init_mem -- not implemented
-- curl_global_sslset -- not implemented
-------------------------------------------------

import Network.Curl.Types

import System.FFI

import Derive.Prim
%language ElabReflection

export
%foreign "C:curl_global_init,libcurl,curl/curl.h"
prim_curl_global_init : Int -> PrimIO Int

||| We use CURL_GLOBAL_ALL since that's the only useful flag in this libcurl
||| version. CURL_GLOBAL_ALL = 3 on my system
export
curl_global_init : HasIO io => io CurlECode
curl_global_init = unsafeFromCode <$> primIO (prim_curl_global_init 3)

%runElab makeHasIO "curl_global_cleanup" Export
          `[ %foreign "C:curl_global_cleanup,libcurl,curl/curl.h"
             export
             prim_curl_global_cleanup : PrimIO () ] --`