text:
import Data.Vect

NatOrError : Nat -> Type
NatOrError Z = String
NatOrError (S k) = Nat

divide : Nat -> (divisor:Nat) -> NatOrError divisor
divide k Z = "Division by 0 is not defined"
divide k (S j) = div k (S j)

{-
data Vect : (n:Nat) -> (a: Type) -> Type where
  VNil : Vect 0 a
  VCons : (head : a) -> (tail : Vect k a) -> Vect (S k) a

vtake : {m:Nat} -> (n:Nat) -> Vect (n+m) a -> Vect n a
vtake Z x = VNil
vtake (S k) (VCons head tail) = VCons head (vtake k tail)

vtake2 : (n:Nat) -> Vect m a -> { auto prf : LTE n m } -> Vect n a
vtake2 Z x = VNil
vtake2 (S k) (VCons head tail) {prf = (LTESucc y)} = VCons head (vtake2 k tail)

vdrop : (n:Nat) -> Vect (n+m) a -> Vect m a
vdrop Z x = x
vdrop (S k) (VCons head tail) = vdrop k tail
-}

Fun : Nat -> Type
Fun Z = Nat
Fun (S k) = Nat -> (Fun k)

adder : ( n:Nat ) -> (acc:Nat) -> Fun n
adder Z acc = acc
adder (S k) acc = \x => adder k (acc + x)

{-
vappend : Vect n a -> Vect m a -> Vect (n+m) a
vappend VNil y = y
vappend (VCons head tail) y = VCons head (vappend tail y)
-}

Matrix : Nat -> Nat -> Type
Matrix k j = Vect k (Vect j Int)

zipWithV : (f : a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
zipWithV f [] [] = []
zipWithV f (x :: xs) (y :: ys) = f x y :: zipWithV f xs ys

whatever : (row : Vect m Int) -> (transposed : Matrix m len) -> Vect m (Vect (S len) Int)
whatever row transposed = zipWithV (::) row transposed

transposeMat : Matrix n m -> Matrix m n
transposeMat {m} [] = replicate m []
transposeMat (row :: rows) = let transposed = transposeMat rows in
                             whatever row transposed

vectMult : Vect n Int -> Vect n Int -> Int
vectMult [] [] = 0
vectMult (x :: xs) (y :: ys) = x * y + vectMult xs ys

multVectMat : (row : Vect m Int) -> (transposed : Matrix k m) -> Vect k Int
multVectMat row [] = []
multVectMat row (x :: xs) = vectMult row x :: multVectMat row xs

multMat : Matrix n m -> Matrix m k -> Matrix n k
multMat [] [] = []
multMat [] (x :: xs) = []
multMat (row :: rows) y = let transposed = transposeMat y in
                       multVectMat row transposed :: multMat rows y --?x --multVect row transposed

idRow : (i:Nat) -> { auto prf: LT i n } ->  Vect n Int
idRow {n = Z} i = []
idRow {n = (S k)} Z = 1 :: replicate k 0
idRow {n = (S k)} (S j) {prf = (LTESucc x)} = 0 :: idRow j

idMatHelper : (i:Nat) -> ( prf : LTE i n ) ->  Matrix i n
idMatHelper Z LTEZero = []
idMatHelper (S left) (LTESucc x) = idRow left :: idMatHelper left (lteSuccRight x)

idMat : Matrix n n
idMat {n} = reverse $ idMatHelper n lteRefl

--mult : Matrix 2 4 -> Matrix 4 3 -> Matrix 2 3


text:
module Task.Input

import Control.Catchable

import public Data.Surely

import Task.Universe
import Helpers

%default total
%access export

infix 6 =~, /~

-- Paths -----------------------------------------------------------------------

namespace Path

  public export
  data Path
    = GoLeft Path
    | GoHere
    | GoRight Path

  Eq Path where
    (GoLeft x)  == (GoLeft y)  = x == y
    (GoHere)    == (GoHere)    = True
    (GoRight x) == (GoRight y) = x == y
    _           == _           = False

  Show Path where
    show (GoLeft p)  = " l" ++ show p
    show (GoHere)    = ""
    show (GoRight p) = " r" ++ show p

  parse : List String -> Either String Path
  parse ("l" :: rest) = map GoLeft $ parse rest
  parse []            = ok GoHere
  parse ("r" :: rest) = map GoRight $ parse rest
  parse other         = throw $ "!! `" ++ unwords other ++ "` is not a valid path, type `help` for more info"

-- Events ----------------------------------------------------------------------

public export
data Action : Type where
  Change       : {c : Ty} -> Surely (typeOf c) -> Action
  Empty        : Action
  Pick         : Path -> Action
  PickWith     : Label -> Action
  Continue     : Action
  ContinueWith : Label -> Action

Eq Action where
  (Change {c=c1} x) == (Change {c=c2} y) with ( decEq c1 c2 )
    (Change {c=c2} x) == (Change {c=c2} y) | Yes Refl with ( eq c2 )
      | eq_c2                                         = x == y
    (Change {c=c1} x) == (Change {c=c2} y) | No _     = False
  (Empty)           == (Empty)                        = True
  (Pick x)          == (Pick y)                       = x == y
  (PickWith x)      == (PickWith y)                   = x == y
  (Continue)        == (Continue)                     = True
  (ContinueWith x)  == (ContinueWith y)               = x == y
  _                 == _                              = False

public export
data Input
  = ToLeft Input
  | ToHere Action
  | ToRight Input

Eq Input where
  (ToLeft x)  == (ToLeft y)  = x == y
  (ToHere x)  == (ToHere y)  = x == y
  (ToRight x) == (ToRight y) = x == y
  _           == _           = False

-- Conformance -----------------------------------------------------------------

strip : (i : Input) -> Maybe (c : Ty ** typeOf c)
strip (ToHere (Change {c} (Exactly v))) = Just (c ** v)
strip (ToHere (Change Anything))        = Nothing
strip (ToHere _)                        = Nothing
strip (ToLeft i)                        = strip i
strip (ToRight i)                       = strip i

(=~) : Input -> Input -> Bool
--FIXME: Why does a with-view not work?
i1 =~ i2 = case ( strip i1, strip i2 ) of
  ( Just (c1 ** v1), Just (c2 ** v2) ) => case decEq c1 c2 of
    Yes Refl => case eq c1 of
      eq_c1 => v1 == v2
    No contr => False
  _ => True

(/~) : Input -> Input -> Bool
i1 /~ i2 = not (i1 =~ i2)

-- Showing ---------------------------------------------------------------------

Show Action where
  show (Change _)       = "change <val>"
  show (Empty)          = "empty"
  show (Pick p)         = "pick" ++ show p
  show (PickWith l)     = "pick " ++ l
  show (Continue)       = "cont"
  show (ContinueWith l) = "cont " ++ l

Show Input where
  show (ToLeft e)  = "l " ++ show e
  show (ToHere a)   = show a
  show (ToRight e) = "r " ++ show e

-- Parsing ---------------------------------------------------------------------

usage : String
usage = unlines
  [ ":: Possible events are:"
  , "    change <value> : change current editor to <value> "
  , "    empty          : empty current editor"
  , "    pick <path>    : pick amongst the possible options"
  , "    pick <label>   : pick the option labeld with <label>"
  , "    cont           : continue with the next task"
  , "    cont <label>   : continue with the task labeld <label>"
  , "    l <event>      : send <event> to the left task"
  , "    r <event>      : send <event> to the right task"
  , "    help           : show this message"
  , ""
  , "where values can be:"
  , "    ()          : Unit"
  , "    True, False : Booleans"
  , "    1, 32, -42  : Integers"
  , "    \"Hello\"   : Strings"
  , ""
  , "paths are of the form:"
  , "   l <path>? : go left"
  , "   r <path>? : go right"
  , ""
  , "and labels always start with a Capital letter"
  ]

parse : List String -> Either String Input
parse [ "change", val ] with (Universe.parse val)
  | Nothing              = throw $ "!! Error parsing value `" ++ val ++ "`"
  -- NOTE: `c` is the type of `v` in our universe, which is automatically used by implicit of the `Change` constructor.
  | Just (c ** v)        = ok $ ToHere $ Change (Exactly v)
parse [ "empty" ]        = ok $ ToHere $ Empty
parse [ "pick", next ]   =
  if isLabel next then
    ok $ ToHere $ PickWith next
  else
    map (ToHere . Pick) $ Path.parse [ next ]
parse ("pick" :: rest)   = map (ToHere . Pick) $ Path.parse rest
parse [ "cont" ]         = ok $ ToHere $ Continue
parse [ "cont", next ]   =
  if isLabel next then
    ok $ ToHere $ ContinueWith next
  else
    throw $ "!! Could not parse `" ++ next ++ "` as a label, type `help` for more info"
parse ("l" :: rest)      = map ToLeft $ parse rest
parse ("r" :: rest)      = map ToRight $ parse rest
parse [ "help" ]         = throw usage
parse other              = throw $ "!! `" ++ unwords other ++ "` is not a valid command, type `help` for more info"

ext: idr

max_stars_repo_name: mklinik/task-semantics

max_issues_repo_name: mklinik/task-semantics

max_forks_repo_name: mklinik/task-semantics


text:
module School

public export
record School where
  constructor CreateSchool
  id : String
  country : Integer
  city : Integer
  name : String
  yearFrom : Integer
  yearTo : Integer
  yearGraduated : Integer
  clazz : Integer
  speciality : String
  type : Integer
  typeStr : Integer

max_stars_repo_name: GrandArchTemplar/IdrisVKAPI

max_issues_repo_name: GrandArchTemplar/IdrisVKAPI

max_forks_repo_name: GrandArchTemplar/IdrisVKAPI


text:
data Vect : Nat -> Type -> Type where
  Nil : Vect Z a
  (::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a
%name Vect xs, ys, zs

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

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

checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (num1 = num2)
checkEqNat Z Z = Just Refl
checkEqNat Z (S k) = Nothing
checkEqNat (S k) Z = Nothing
checkEqNat (S j) (S k) = do
  eq <- checkEqNat j k
  pure (cong eq)

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

same_cons : (xs : List a) -> (ys : List a) ->
            (xs = ys) -> (x :: xs = x :: ys)
same_cons xs xs Refl = Refl

same_lists : {xs : List a} -> {ys : List a} ->
             (x = y) -> (xs = ys) -> x :: xs = y :: ys
same_lists Refl Refl = Refl

data ThreeEq : (a : ty) -> (b : ty) -> (c : ty) -> Type where
  Same3 : (a : ty) -> ThreeEq a a a

allSameS : ThreeEq x y z -> ThreeEq (S x) (S y) (S z)
allSameS (Same3 j) = Same3 (S j)

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

head_unequal : DecEq a => (xs : Vect n a) -> (ys : Vect n a) ->
  (contra : (x = y) -> Void) -> ((x :: xs) = (y :: ys)) -> Void
head_unequal xs xs contra Refl = contra Refl

tail_unequal : DecEq a => (xs : Vect n a) -> (ys : Vect n a) ->
  (contra : (xs = ys) -> Void) -> ((x :: xs) = (y :: ys)) -> Void
tail_unequal xs xs contra Refl = contra Refl

DecEq a => DecEq (Vect n a) where
  decEq [] [] = Yes Refl
  decEq (x :: xs) (y :: ys) =
    case decEq x y of
         (No contra) => No (head_unequal xs ys contra)
         (Yes Refl) =>
           case decEq xs ys of
                (No contra) => No (tail_unequal xs ys contra)
                (Yes Refl) => Yes Refl

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module Program

import CommonTestingStuff

export
beforeString : String
beforeString = "before coop"

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

export
program : PrintString m => CanSleep m => Alternative m => m Unit
program = do
  printString "\n------\n"

  do
    offset <- currentTime
    printTime offset "start"

    res <- empty <|> s150
    printTime offset "top: \{res}"

    printTime offset "end"

  printString "\n------\n"

  do
    offset <- currentTime
    printTime offset "start"

    res <- s150 <|> empty
    printTime offset "top: \{show res}"

    printTime offset "end"

  printString "\n------"


text:
> module SequentialDecisionProblems.ViabilityDefaults

> import SequentialDecisionProblems.CoreTheory
> import SequentialDecisionProblems.Utils

> import Unit.Properties

> %default total
> %auto_implicits off

This is the default implementation of |Viable|: all states are viable
for 0 steps; a state is viable for |n + 1| steps iff it has a control
such that 1) the set of next possible states is not empty and 2) all
next possible states are viable for |n| steps. These two conditions are
encoded in the notion of "good" control, see |Utils|:

> -- Viable : (n : Nat) -> State t -> Type
> SequentialDecisionProblems.CoreTheory.Viable {t}  Z    _ = Unit
> SequentialDecisionProblems.CoreTheory.Viable {t} (S n) x = GoodCtrl t x n

Trivially, for every state that is viable for |n + 1| steps we can
compute a good control

> -- viableSpec0 : (x : State t) -> Viable Z x
> SequentialDecisionProblems.CoreTheory.viableSpec0 x = ()

> -- viableSpec1 : (x : State t) -> Viable (S n) x -> GoodCtrl t x n
> SequentialDecisionProblems.CoreTheory.viableSpec1 {t} {n} x v = v

> -- viableSpec2 : (x : State t) -> GoodCtrl t x n -> Viable (S n) x
> SequentialDecisionProblems.CoreTheory.viableSpec2 {t} {n} x gy = gy

If users can show that ..., see |Utils|. For |M = List|, for instance,
... are implemented in |NonDeterministic Defaults|:

> -- finiteViable : {t : Nat} ->
> --                (n : Nat) -> (x : State t) -> Finite (Viable n x)
> SequentialDecisionProblems.Utils.finiteViable Z     _ = finiteUnit
> SequentialDecisionProblems.Utils.finiteViable (S m) x = finiteGoodCtrl m x

> -- decidableViable : {t : Nat} ->
> --                   (n : Nat) -> (x : State t) -> Dec (Viable n x)
> SequentialDecisionProblems.Utils.decidableViable  Z    _ = Yes MkUnit
> SequentialDecisionProblems.Utils.decidableViable (S m) x = decidableGoodCtrl m x

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
||| Rules for Supply
||| section 7 of game rules
module Bautzen.Game.Supply

import Bautzen.GameUnit
import Bautzen.ZoC
import Bautzen.Game.Core
import Bautzen.Game.Move
import Bautzen.Pos
import Bautzen.Terrain

import Data.Heap.LeftistHeap

import Data.SortedMap
import Data.List.Extra

import Data.List
import Data.Nat
import Data.Vect

-- section 7.1.2

||| State for a single step of exploration in an instance of A*
record AState where
  constructor MkAState
  ||| Starting position of this path
  src : Pos

  ||| Target position of this path
  tgt : Pos

  ||| The current accumulated path, in reverse order (eg. from `src` to the
  ||| current explored solution
  path : List Pos

  ||| The accumulated path's cost so far
  costSoFar : Nat

Show AState where
  show (MkAState src tgt path costSoFar) = show src ++ ": " ++ show costSoFar

Eq AState where
  (MkAState src tgt path costSoFar) == (MkAState src' tgt' path' costSoFar') =
    src == src' && tgt == tgt' && costSoFar == costSoFar'

Ord AState where
  compare (MkAState src tgt path costSoFar) (MkAState src' tgt' path' costSoFar') =
    case compare costSoFar costSoFar' of
      EQ => case compare tgt tgt' of
        EQ => compare src src'
        ordering => ordering
      ordering => ordering

computeShortestPath : (fuel : Nat) -> (units : List (GameUnit, Pos)) -> (gameMap : Map) -> (unit : GameUnit) ->  (costsMap : SortedMap Pos Nat) -> BinaryHeap AState -> List Pos
computeShortestPath Z _ _ _ _ queue = []
computeShortestPath (S fuel) units gameMap unit costsMap queue =
  if isEmpty queue
  then []
  else let (q, st) = Heap.pop queue
       in case st of
            Nothing => []
            Just cur@(MkAState src tgt path _) =>
              if src == tgt
              then path
              else let (q', costsMap') = foldl (addNeighbours cur) (q, costsMap) (neighbours src)
                   in computeShortestPath fuel units gameMap unit costsMap' q'
  where
    samePos : Pos -> (GameUnit, Pos) -> Bool
    samePos hex (_,p) = p == hex

    -- TODO factor to Move
    enemyIn : Pos -> Bool
    enemyIn hex = case find' (samePos hex) units of
                    Nothing => False
                    (Just (other, _)) => not (friendly (nation unit) (nation other))

    cannotMoveInto : Pos -> Bool
    cannotMoveInto hex =
      (inZoC (side $ nation unit) units hex /= Free) ||
      enemyIn hex

    explore : Pos -> Nat -> AState -> (BinaryHeap AState, SortedMap Pos Nat) -> (BinaryHeap AState, SortedMap Pos Nat)
    explore hex newCost state@(MkAState src tgt path costSoFar) (queue, costsMap) =
      let costEstimate = newCost + (distance hex tgt)
      in (Heap.push (MkAState hex tgt (hex :: path) costEstimate) queue, insert hex newCost costsMap)

    addNeighbours : AState -> (BinaryHeap AState, SortedMap Pos Nat) -> Pos -> (BinaryHeap AState, SortedMap Pos Nat)
    addNeighbours state@(MkAState src tgt path costSoFar) (queue, costsMap) hex =
      if cannotMoveInto hex
      then (queue, costsMap)
      else case movementCost unit units gameMap src hex False of
             (Left l) => (queue, costsMap)
             (Right (x ** _)) =>
               let newCost = costSoFar + toNat x
                   costTox = lookup hex costsMap
               in case costTox of
                    Just oldCost => if newCost < oldCost
                                    then explore hex newCost state (queue, costsMap)
                                    else (queue, costsMap)
                    Nothing => explore hex newCost state (queue, costsMap)

||| Computes a path of adjacent `Pos`itions `from` to one of `srcs`.
|||
||| The path must be free of enemy `ZoC`s and enemy `units`. This function
||| uses the well-known _A*_ algorithm to build a path to _one_ given sources for the
||| given unit. See [path finding](https://www.redblobgames.com/pathfinding/a-star/introduction.html#astar) page
||| for more details.
|||
||| @from the unit and position to start looking from
||| @units all units on the map along with their positions. This is needed to ensure path is
||| free of enemies and ZoCs
||| @gameMap the terrain map
||| @srcs target supply sources, to trace a path to
export
supplyPathTo : (units : List (GameUnit, Pos)) -> (gameMap : Map) -> (srcs : List Pos) -> (from: (GameUnit, Pos)) -> List Pos
supplyPathTo units gameMap srcs (unit, pos) = supplyPathToAcc startStates

  where
    startState : Pos -> AState
    startState tgt = MkAState pos tgt [pos] 0

    on : (a -> a -> b) -> (c -> a) -> (c -> c -> b)
    on f g x y = f (g x) (g y)

    startStates : List (BinaryHeap AState)
    startStates = map (\ st => Heap.push st Heap.empty) $
                  sortBy (compare `on` (Pos.distance pos . tgt)) $
                  map startState srcs

    getFirstNonEmptyPath : List Pos -> BinaryHeap AState -> List Pos
    getFirstNonEmptyPath []   start = computeShortestPath 10000 units gameMap unit empty start
    getFirstNonEmptyPath path _     = path

    supplyPathToAcc : List (BinaryHeap AState) -> List Pos
    supplyPathToAcc = foldl getFirstNonEmptyPath []

||| Check if given `unit` is in supply
||| A unit is in supply if it can trace an enemy and ZoC-free line to
||| a `SupplySource` hex.
||| @unit: the unit to check supply for along with its position
||| @units: position of all units on the `map`
||| @gameMap: the terrain
export
isInSupply : (unit : (GameUnit, Pos)) -> (units : List (GameUnit, Pos)) -> (gameMap : Map) -> Bool
isInSupply (unit, pos) units gameMap =
  let sources = supplySources (nation unit) gameMap -- get all possible supply sources for unit
  in not (isNil $ supplyPathTo units gameMap sources (unit, pos))

-- TODO handle rules for Supply columns
-- section 7.2

-- TODO handle effects of lack of supply on unit
-- section 7.3

-- TODO handle special case of supply path going through hex in ZoC containing
-- a friendly unit

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
module Interfaces

import Data.List
import Data.Strings

%default total

data MyNat = MZ | MS MyNat

Show MyNat where
  show MZ = "Z"
  show (MS k) = "(S " ++ show k ++ ")"

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

Show a => Show (Vect n a) where
  show xs = "[" ++ show' xs ++ "]" where
    show' : Vect m a -> String
    show' Nil = ""
    show' (x :: Nil) = show x
    show' (x :: xs) = show x ++ ", " ++ show' xs

-- default definitions

Eq MyNat where
  MZ == MZ = True
  (MS k) == (MS l) = k == l
  _ == _ = False

-- extending interfaces

sortAndShow : (Ord a, Show a) => List a -> String
sortAndShow = show . sort

-- functors and applicatives

{-
  interface Functor f where
    map : (a -> b) -> f a -> f b
-}

infixr 5 %%

data MyList a = Empty | (%%) a (MyList a)

infixr 5 @@

(@@) : MyList a -> MyList a -> MyList a
Empty @@ ys = ys
(x %% xs) @@ ys = x %% xs @@ ys

Show a => Show (MyList a) where
  show xs = "[" ++ show' xs ++ "]" where
    show' : MyList a -> String
    show' Empty = ""
    show' (x %% Empty) = show x
    show' (x %% xs) = show x ++ ", " ++ show' xs

Functor MyList where
  map f Empty = Empty
  map f (x %% xs) = f x %% map f xs

li : MyList Int
li = 1 %% 2 %% 3 %% 4 %% 5 %% Empty

{-
  infixl 2 <4>

  interface Functor f => Applicative f where
    pure : a -> f a
    (<*>) : f (a -> b) -> f a -> f b
-}

Applicative MyList where
  pure x = x %% Empty

  Empty <*> _ = Empty
  (f %% fs) <*> xs = map f xs @@ (fs <*> xs)

-- monads and the `do` notation

{-
  interface Applicative m => Monad m where
    (>>=) : m a -> (a -> m b) -> m b
-}

Monad MyList where
  Empty >>= f = Empty
  (x %% xs) >>= f = f x @@ (xs >>= f)

mAdd : Maybe Int -> Maybe Int -> Maybe Int
mAdd mx my = do x <- mx
                y <- my
                pure (x + y)

-- pattern-matching bind

readNumber : HasIO io => io (Maybe Int)
readNumber = do input <- getLine
                case all isDigit (unpack input) of
                     False => pure Nothing
                     True => pure $ Just (cast input)

readNumbers : HasIO io => io (Maybe (Int, Int))
readNumbers = do n <- readNumber
                 case n of
                      Nothing => pure Nothing
                      Just nn => do m <- readNumber
                                    case m of
                                         Nothing => pure Nothing
                                         Just mm => pure $ Just (nn, mm)

readNumbersBetter : HasIO io => io (Maybe (Int, Int))
readNumbersBetter = do Just n <- readNumber
                        | Nothing => pure Nothing
                       Just m <- readNumber
                        | Nothing => pure Nothing
                       pure $ Just (n, m)

{-
  (!) : m a -> a

-}

mAddBetter : Maybe Int -> Maybe Int -> Maybe Int
mAddBetter mx my = pure (!mx + !my)

-- monad comprehensions - can be used for any type that implements both Monad and Alterantive.

{-
  interface Applicative f => Alternative f where
    empty : f a
    (<|>) : f a -> f a -> f a
-}

mAddAgain : Maybe Int -> Maybe Int -> Maybe Int
mAddAgain mx my = [x + y | x <- mx, y <- my]

{-
  interface Monad io => HasIO io where
    liftIO : (1 _ : IO a) -> io a
-}

-- idiom brackets

{-
  [| f a1 a2 .. an |] == pure f <*> a1 <*> a2 <*> ... <*> an
-}

applicativeAdd : Maybe Int -> Maybe Int -> Maybe Int
applicativeAdd mx my = pure (+) <*> mx <*> my

-- this can now be rewritten as

applicativeAddBetter : Maybe Int -> Maybe Int -> Maybe Int
applicativeAddBetter mx my = [| mx + my |]

{-
  Determining Parameters: When an interface has multiple parameters, but only some of the parameters are used to find implementations, we can mark with using
  the `| m` notation. For example,

  interface Monad m => MonadState s (m : Type -> Type) | m where
    get : m s
    pur : s -> m ()

  In the interface above, only `m` needs to be known in order to determine concrete implementations for `MonadState` without any dependency on `s`. Hence we mark
  `m` as the dependent parameter using `| m` in the interface definition.
-}

max_stars_repo_name: timmyjose-study/idris-from-the-docs

max_issues_repo_name: timmyjose-study/idris-from-the-docs

max_forks_repo_name: timmyjose-study/idris-from-the-docs


text:
-- --------------------------------------------------------------- [ State.idr ]
-- Module      : Exercises.Test.State
-- Description : Test covering the Chapter 12 exercises in Edwin Brady's
--               book, "Type-Driven Development with Idris."
-- --------------------------------------------------------------------- [ EOH ]
module Exercises.Test.State

import Exercises.State

import Test.Helpers

import Control.Monad.State
import System

import Data.Vect
%hide Data.Vect.overLength

%access export

testIncrease : IO Bool
testIncrease =
  "increase" `assertEqual'` ((), 94) $
  runState (increase 5) 89

testCountEmpty : IO Bool
testCountEmpty =
  "countEmpty" `assertEqual'` 7 $
  execState (countEmpty testTree) 0

testCountEmptyNode : IO Bool
testCountEmptyNode =
  "countEmptyNode" `assertEqual'` (7, 6) $
  execState (countEmptyNode testTree) (0, 0)

testUpdateGameState : IO Bool
testUpdateGameState =
  do let command = updateGameState addCorrect
     rnds <- pure (randoms . fromInteger) <*> time
     (_, _, st) <- runCommand rnds initState command
     "updateGameState" `assertEqual'` 1 $
       record { score->correct } st

goodSite : Article
goodSite = MkArticle "Good Page" "http://example.com/good" (MkVotes 101 7)

badSite : Article
badSite = MkArticle "Bad Page" "http://example.com/bad" (MkVotes 5 47)

testGetScore : (article : Article) -> (expected : Integer) -> IO Bool
testGetScore article expected =
  ("getScore " ++ title article) `assertEqual'` expected $
  getScore article

testAddUpvote : IO Bool
testAddUpvote =
  "addUpvote" `assertEqual'` 102 $
  record { score->upvotes } $ addUpvote goodSite

testAddDownvote : IO Bool
testAddDownvote =
  "addDownvote" `assertEqual'` 48 $
  record { score->downvotes } $ addDownvote badSite

allTests : List (IO Bool)
allTests = [ testIncrease
           , testCountEmpty
           , testCountEmptyNode
           , testUpdateGameState
           , testGetScore goodSite 94
           , testGetScore badSite (-42)
           , testAddUpvote
           , testAddDownvote
           ]

runTests : IO (Vect (length State.allTests) Bool)
runTests = testChapter "12: State" allTests

-- --------------------------------------------------------------------- [ 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:
||| Complex number.
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module Data.Complex

import Generics.Derive
%language ElabReflection

-- --------------------------------------------------------------------------

public export
record Complex t where
  constructor MkComplex
  real : t
  imag : t

export
Show t => Show (Complex t) where
  show x = show x.real ++ " + " ++ show x.imag ++ "i"

export
Functor Complex where
  map f x = MkComplex (f x.real) (f x.imag)

%runElab derive "Complex" [Generic, Meta, Eq]

export
(Neg t, Num t) => Num (Complex t) where
  x + y = MkComplex (x.real + y.real) (x.imag + y.imag)
  x * y = MkComplex (x.real * y.real - x.imag * y.imag)
                    (x.real * y.imag + x.imag * y.real)
  fromInteger x = MkComplex (fromInteger x) (fromInteger 0)

export
Neg t => Neg (Complex t) where
  negate x = MkComplex (negate x.real) (negate x.imag)
  x - y    = MkComplex (x.real - y.real) (x.imag - y.imag)

export
isReal : (Num t, Eq t) => Complex t -> Bool
isReal x = x.imag == fromInteger 0

export
isImage : (Num t, Eq t) => Complex t -> Bool

export
plus_commutative : (Num t, Neg t)
    => {x, y:Complex t}
    -> {comm_t: {a,b:t} -> (a + b) = (b + a)}
    -> (x + y) = (y + x)
plus_commutative = rewrite (comm_t {a=x.real} {b=y.real})
                in rewrite (comm_t {a=x.imag} {b=y.imag})
                in Refl

plus_assosiative : (Num t, Neg t)
    => {x, y:Complex t}
    -> {assoc_t: {a,b,c:t} -> (a + b) + c = a + (b + c)}
    -> (x + y) + z = x + (y + z)
plus_assosiative = rewrite (assoc_t {a=x.real} {b=y.real} {c=z.real})
                in rewrite (assoc_t {a=x.imag} {b=y.imag} {c=z.imag})
                in Refl

mult_commutative : (Num t, Neg t)
    => {x, y:Complex t}
    -> {mult_comm_t: {a,b:t} -> a * b = b * a}
    -> {plus_comm_t: {a,b:t} -> a + b = b + a}
    -> (x * y) = (y * x)
mult_commutative = rewrite (mult_comm_t {a=x.real} {b=y.real})
                in rewrite (mult_comm_t {a=x.imag} {b=y.imag})
                in rewrite (mult_comm_t {a=x.real} {b=y.imag})
                in rewrite (mult_comm_t {a=x.imag} {b=y.real})
                in rewrite (plus_comm_t {a=(y.imag * x.real)} {b=(y.real * x.imag)})
                in Refl

distributive : (Num t, Neg t)
    => {x, y:Complex t}
    -> {dist_t: {a,b,c:t} -> a * (b + c) = a * b + a * c}
    -> {plus_commu_t: {a,b:t} -> a + b = b + a}
    -> x * (y + z) = x * y + x * z
distributive = rewrite (dist_t {a=x.real} {b=y.real} {c=z.real})
            in rewrite (dist_t {a=x.imag} {b=y.imag} {c=z.imag})
            in rewrite (dist_t {a=x.real} {b=y.imag} {c=z.imag})
            in rewrite (dist_t {a=x.imag} {b=y.real} {c=z.real})
            in ?lhs_distributive

-- --------------------------------------------------------------------------

export
conjugate : Neg t => Complex t -> Complex t
conjugate x = MkComplex x.real (negate x.imag)

conjugate_distributive : (Num t, Neg t)
    => {x, y: Complex t}
    -> {pr: {a,b:t} -> negate (a + b) = negate a + negate b}
    -> conjugate (x + y) = conjugate x + conjugate y
conjugate_distributive = rewrite (pr {a =x.imag} {b=y.imag}) in Refl

-- --------------------------------------------------------------------------
-- vim: tw=80 sw=2 expandtab :


text:
module Specdris.ConsoleColor

%access export
%default total

||| Console colors
public export
data Color = Red
           | Green
           | Yellow
           | Blue
           | Magenta
           | Cyan
           | White

Eq Color where
  (==) Red Red         = True
  (==) Green Green     = True
  (==) Yellow Yellow   = True
  (==) Blue Blue       = True
  (==) Magenta Magenta = True
  (==) Cyan Cyan       = True
  (==) White White     = True
  (==) _ _ = False

Show Color where
  show Red     = "red"
  show Green   = "green"
  show Yellow  = "yellow"
  show Blue    = "blue"
  show Magenta = "magenta"
  show Cyan    = "cyan"
  show White   = "white"

private
colorToCode : Color -> Nat
colorToCode Red     = 1
colorToCode Green   = 2
colorToCode Yellow  = 3
colorToCode Blue    = 4
colorToCode Magenta = 5
colorToCode Cyan    = 6
colorToCode White   = 7

private
colorToAnsi : Color -> String
colorToAnsi code = "\ESC[3" ++ show (colorToCode code) ++ "m"

colorise : Color -> String -> String
colorise color str = colorToAnsi color ++ str ++ "\ESC[0m"

indent : (level : Nat) -> String
indent level = foldr (\el, acc => el ++ acc) "" (replicate level "  ")

format : String -> Color -> (level : Nat) -> String
format str color level = colorise color $ indent level ++ str

max_stars_repo_name: pheymann/specdris

max_issues_repo_name: pheymann/specdris

max_forks_repo_name: pheymann/specdris


text:
module Idris.Package

import Compiler.Common

import Core.Context
import Core.Context.Log
import Core.Core
import Core.Directory
import Core.Env
import Core.Metadata
import Core.Name.Namespace
import Core.Options
import Core.Unify

import Data.List
import Data.Maybe
import Data.String
import Data.These

import Parser.Package
import System
import System.Directory
import Libraries.System.Directory.Tree
import System.File

import Libraries.Data.SortedMap
import Libraries.Data.StringMap
import Libraries.Data.StringTrie
import Libraries.Text.Parser
import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Utils.String
import Libraries.Utils.Path

import Idris.CommandLine
import Idris.Doc.HTML
import Idris.Doc.String
import Idris.ModTree
import Idris.ProcessIdr
import Idris.REPL
import Idris.REPL.Common
import Idris.REPL.Opts
import Idris.SetOptions
import Idris.Syntax
import Idris.Version
import IdrisPaths

import public Idris.Package.Types
import Idris.Package.Init

%hide Data.String.lines
%hide Data.String.lines'
%hide Data.String.unlines
%hide Data.String.unlines'

%default covering

installDir : PkgDesc -> String
installDir p = name p
            ++ "-"
            ++ show (fromMaybe (MkPkgVersion (0 ::: [])) (version p))

data DescField : Type where
  PVersion     : FC -> PkgVersion -> DescField
  PVersionDep  : FC -> String -> DescField
  PAuthors     : FC -> String -> DescField
  PMaintainers : FC -> String -> DescField
  PLicense     : FC -> String -> DescField
  PBrief       : FC -> String -> DescField
  PReadMe      : FC -> String -> DescField
  PHomePage    : FC -> String -> DescField
  PSourceLoc   : FC -> String -> DescField
  PBugTracker  : FC -> String -> DescField
  PDepends     : List Depends -> DescField
  PModules     : List (FC, ModuleIdent) -> DescField
  PMainMod     : FC -> ModuleIdent -> DescField
  PExec        : String -> DescField
  POpts        : FC -> String -> DescField
  PSourceDir   : FC -> String -> DescField
  PBuildDir    : FC -> String -> DescField
  POutputDir   : FC -> String -> DescField
  PPrebuild    : FC -> String -> DescField
  PPostbuild   : FC -> String -> DescField
  PPreinstall  : FC -> String -> DescField
  PPostinstall : FC -> String -> DescField
  PPreclean    : FC -> String -> DescField
  PPostclean   : FC -> String -> DescField

field : String -> Rule DescField
field fname
      = strField PAuthors "authors"
    <|> strField PMaintainers "maintainers"
    <|> strField PLicense "license"
    <|> strField PBrief "brief"
    <|> strField PReadMe "readme"
    <|> strField PHomePage "homepage"
    <|> strField PSourceLoc "sourceloc"
    <|> strField PBugTracker "bugtracker"
    <|> strField POpts "options"
    <|> strField POpts "opts"
    <|> strField PSourceDir "sourcedir"
    <|> strField PBuildDir "builddir"
    <|> strField POutputDir "outputdir"
    <|> strField PPrebuild "prebuild"
    <|> strField PPostbuild "postbuild"
    <|> strField PPreinstall "preinstall"
    <|> strField PPostinstall "postinstall"
    <|> strField PPreclean "preclean"
    <|> strField PPostclean "postclean"
    <|> do start <- location
           ignore $ exactProperty "version"
           equals
           vs <- sepBy1 dot' integerLit
           end <- location
           pure (PVersion (MkFC (PhysicalPkgSrc fname) start end)
                          (MkPkgVersion (fromInteger <$> vs)))
    <|> do start <- location
           ignore $ exactProperty "version"
           equals
           v <- stringLit
           end <- location
           pure (PVersionDep (MkFC (PhysicalPkgSrc fname) start end) v)
    <|> do ignore $ exactProperty "depends"
           equals
           ds <- sep depends
           pure (PDepends ds)
    <|> do ignore $ exactProperty "modules"
           equals
           ms <- sep (do start <- location
                         m <- moduleIdent
                         end <- location
                         pure (MkFC (PhysicalPkgSrc fname) start end, m))
           pure (PModules ms)
    <|> do ignore $ exactProperty "main"
           equals
           start <- location
           m <- moduleIdent
           end <- location
           pure (PMainMod (MkFC (PhysicalPkgSrc fname) start end) m)
    <|> do ignore $ exactProperty "executable"
           equals
           e <- (stringLit <|> packageName)
           pure (PExec e)
  where
    data Bound = LT PkgVersion Bool | GT PkgVersion Bool

    bound : Rule (List Bound)
    bound
        = do lte
             vs <- sepBy1 dot' integerLit
             pure [LT (MkPkgVersion (fromInteger <$> vs)) True]
      <|> do gte
             vs <- sepBy1 dot' integerLit
             pure [GT (MkPkgVersion (fromInteger <$> vs)) True]
      <|> do lt
             vs <- sepBy1 dot' integerLit
             pure [LT (MkPkgVersion (fromInteger <$> vs)) False]
      <|> do gt
             vs <- sepBy1 dot' integerLit
             pure [GT (MkPkgVersion (fromInteger <$> vs)) False]
      <|> do eqop
             vs <- sepBy1 dot' integerLit
             pure [LT (MkPkgVersion (fromInteger <$> vs)) True,
                   GT (MkPkgVersion (fromInteger <$> vs)) True]

    mkBound : List Bound -> PkgVersionBounds -> EmptyRule PkgVersionBounds
    mkBound (LT b i :: bs) pkgbs
        = maybe (mkBound bs (record { upperBound = Just b,
                                      upperInclusive = i } pkgbs))
                (\_ => fail "Dependency already has an upper bound")
                pkgbs.upperBound
    mkBound (GT b i :: bs) pkgbs
        = maybe (mkBound bs (record { lowerBound = Just b,
                                      lowerInclusive = i } pkgbs))
                (\_ => fail "Dependency already has a lower bound")
                pkgbs.lowerBound
    mkBound [] pkgbs = pure pkgbs

    depends : Rule Depends
    depends
        = do name <- packageName
             bs <- sepBy andop bound
             pure (MkDepends name !(mkBound (concat bs) anyBounds))

    strField : (FC -> String -> DescField) -> String -> Rule DescField
    strField fieldConstructor fieldName
        = do start <- location
             ignore $ exactProperty fieldName
             equals
             str <- stringLit
             end <- location
             pure $ fieldConstructor (MkFC (PhysicalPkgSrc fname) start end) str

parsePkgDesc : String -> Rule (String, List DescField)
parsePkgDesc fname
    = do ignore $ exactProperty "package"
         name <- packageName
         fields <- many (field fname)
         pure (name, fields)

data ParsedMods : Type where

data MainMod : Type where

addField : {auto c : Ref Ctxt Defs} ->
           {auto s : Ref Syn SyntaxInfo} ->
           {auto o : Ref ROpts REPLOpts} ->
           {auto p : Ref ParsedMods (List (FC, ModuleIdent))} ->
           {auto m : Ref MainMod (Maybe (FC, ModuleIdent))} ->
           DescField -> PkgDesc -> Core PkgDesc
addField (PVersion fc n)     pkg = pure $ record { version = Just n } pkg
addField (PVersionDep fc n)  pkg
    = do emitWarning (Deprecated "version numbers must now be of the form x.y.z")
         pure pkg
addField (PAuthors fc a)     pkg = pure $ record { authors = Just a } pkg
addField (PMaintainers fc a) pkg = pure $ record { maintainers = Just a } pkg
addField (PLicense fc a)     pkg = pure $ record { license = Just a } pkg
addField (PBrief fc a)       pkg = pure $ record { brief = Just a } pkg
addField (PReadMe fc a)      pkg = pure $ record { readme = Just a } pkg
addField (PHomePage fc a)    pkg = pure $ record { homepage = Just a } pkg
addField (PSourceLoc fc a)   pkg = pure $ record { sourceloc = Just a } pkg
addField (PBugTracker fc a)  pkg = pure $ record { bugtracker = Just a } pkg
addField (PDepends ds)       pkg = pure $ record { depends = ds } pkg
-- we can't resolve source files for modules without knowing the source directory,
-- so we save them for the second pass
addField (PModules ms)       pkg = do put ParsedMods ms
                                      pure pkg
addField (PMainMod loc n)    pkg = do put MainMod (Just (loc, n))
                                      pure pkg
addField (PExec e)           pkg = pure $ record { executable = Just e } pkg
addField (POpts fc e)        pkg = pure $ record { options = Just (fc, e) } pkg
addField (PSourceDir fc a)   pkg = pure $ record { sourcedir = Just a } pkg
addField (PBuildDir fc a)    pkg = pure $ record { builddir = Just a } pkg
addField (POutputDir fc a)   pkg = pure $ record { outputdir = Just a } pkg
addField (PPrebuild fc e)    pkg = pure $ record { prebuild = Just (fc, e) } pkg
addField (PPostbuild fc e)   pkg = pure $ record { postbuild = Just (fc, e) } pkg
addField (PPreinstall fc e)  pkg = pure $ record { preinstall = Just (fc, e) } pkg
addField (PPostinstall fc e) pkg = pure $ record { postinstall = Just (fc, e) } pkg
addField (PPreclean fc e)    pkg = pure $ record { preclean = Just (fc, e) } pkg
addField (PPostclean fc e)   pkg = pure $ record { postclean = Just (fc, e) } pkg

addFields : {auto c : Ref Ctxt Defs} ->
            {auto s : Ref Syn SyntaxInfo} ->
            {auto o : Ref ROpts REPLOpts} ->
            List DescField -> PkgDesc -> Core PkgDesc
addFields xs desc = do p <- newRef ParsedMods []
                       m <- newRef MainMod Nothing
                       added <- go {p} {m} xs desc
                       setSourceDir (sourcedir added)
                       ms <- get ParsedMods
                       mmod <- get MainMod
                       pure $ record { modules = !(traverse toSource ms)
                                     , mainmod = !(traverseOpt toSource mmod)
                                     } added
  where
    toSource : (FC, ModuleIdent) -> Core (ModuleIdent, String)
    toSource (loc, ns) = pure (ns, !(nsToSource loc ns))
    go : {auto p : Ref ParsedMods (List (FC, ModuleIdent))} ->
         {auto m : Ref MainMod (Maybe (FC, ModuleIdent))} ->
         List DescField -> PkgDesc -> Core PkgDesc
    go [] dsc = pure dsc
    go (x :: xs) dsc = go xs !(addField x dsc)

runScript : Maybe (FC, String) -> Core ()
runScript Nothing = pure ()
runScript (Just (fc, s))
    = do res <- coreLift $ system s
         when (res /= 0) $
            throw (GenericMsg fc "Script failed")

addDeps : {auto c : Ref Ctxt Defs} ->
          PkgDesc -> Core ()
addDeps pkg
    = do defs <- get Ctxt
         traverse_ (\p => addPkgDir p.pkgname p.pkgbounds) (depends pkg)

processOptions : {auto c : Ref Ctxt Defs} ->
                 {auto o : Ref ROpts REPLOpts} ->
                 Maybe (FC, String) -> Core ()
processOptions Nothing = pure ()
processOptions (Just (fc, opts))
    = do let Right clopts = getOpts (words opts)
                | Left err => throw (GenericMsg fc err)
         ignore $ preOptions clopts

compileMain : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              {auto o : Ref ROpts REPLOpts} ->
              Name -> String -> String -> Core ()
compileMain mainn mfilename exec
    = do modIdent <- ctxtPathToNS mfilename
         m <- newRef MD (initMetadata (PhysicalIdrSrc modIdent))
         u <- newRef UST initUState
         ignore $ loadMainFile mfilename
         ignore $ compileExp (PRef replFC mainn) exec

prepareCompilation : {auto c : Ref Ctxt Defs} ->
                     {auto s : Ref Syn SyntaxInfo} ->
                     {auto o : Ref ROpts REPLOpts} ->
                     PkgDesc ->
                     List CLOpt ->
                     Core (List Error)
prepareCompilation pkg opts =
  do
    defs <- get Ctxt

    processOptions (options pkg)
    addDeps pkg

    ignore $ preOptions opts

    runScript (prebuild pkg)

    let toBuild = maybe (map snd (modules pkg))
                        (\m => snd m :: map snd (modules pkg))
                        (mainmod pkg)
    buildAll toBuild

build : {auto c : Ref Ctxt Defs} ->
        {auto s : Ref Syn SyntaxInfo} ->
        {auto o : Ref ROpts REPLOpts} ->
        PkgDesc ->
        List CLOpt ->
        Core (List Error)
build pkg opts
    = do [] <- prepareCompilation pkg opts
            | errs => pure errs

         case executable pkg of
              Nothing => pure ()
              Just exec =>
                   do let Just (mainNS, mainFile) = mainmod pkg
                               | Nothing => throw (GenericMsg emptyFC "No main module given")
                      let mainName = NS (miAsNamespace mainNS) (UN $ Basic "main")
                      compileMain mainName mainFile exec

         runScript (postbuild pkg)
         pure []

installFrom : {auto o : Ref ROpts REPLOpts} ->
              {auto c : Ref Ctxt Defs} ->
              String -> String -> ModuleIdent -> Core ()
installFrom builddir destdir ns
    = do let ttcfile = ModuleIdent.toPath ns
         let ttcPath = builddir </> "ttc" </> ttcfile <.> "ttc"
         objPaths_in <- traverse
                     (\cg =>
                        do Just cgdata <- getCG cg
                                | Nothing => pure Nothing
                           let Just ext = incExt cgdata
                                | Nothing => pure Nothing
                           let srcFile = builddir </> "ttc" </> ttcfile <.> ext
                           let destFile = destdir </> ttcfile <.> ext
                           let Just (dir, _) = splitParent destFile
                                | Nothing => pure Nothing
                           ensureDirectoryExists dir
                           pure $ Just (srcFile, destFile))
                     (incrementalCGs !getSession)
         let objPaths = mapMaybe id objPaths_in

         let modPath  = reverse $ fromMaybe [] $ tail' $ unsafeUnfoldModuleIdent ns
         let destNest = joinPath modPath
         let destPath = destdir </> destNest
         let destFile = destdir </> ttcfile <.> "ttc"

         Right _ <- coreLift $ mkdirAll $ destNest
             | Left err => throw $ InternalError $ unlines
                             [ "Can't make directories " ++ show modPath
                             , show err ]
         coreLift $ putStrLn $ "Installing " ++ ttcPath ++ " to " ++ destPath
         Right _ <- coreLift $ Tree.copyFile ttcPath destFile
             | Left err => throw $ InternalError $ unlines
                             [ "Can't copy file " ++ ttcPath ++ " to " ++ destPath
                             , show err ]
         -- Copy object files, if any. They don't necessarily get created,
         -- since some modules don't generate any code themselves.
         traverse_ (\ (obj, dest) =>
                      do coreLift $ putStrLn $ "Installing " ++ obj ++ " to " ++ destPath
                         ignore $ coreLift $ Tree.copyFile obj dest)
                   objPaths

         pure ()

installSrcFrom : {auto c : Ref Ctxt Defs} ->
                 String -> String -> (ModuleIdent, FileName) -> Core ()
installSrcFrom wdir destdir (ns, srcRelPath)
    = do let srcfile = ModuleIdent.toPath ns
         let srcPath = wdir </> srcRelPath
         let Just ext = extension srcPath
           | _ => throw (InternalError $
                "Unexpected failure when installing source file:\n"
              ++ srcPath
              ++ "\n"
              ++ "Can't extract file extension.")

         let modPath  = reverse $ fromMaybe [] $ tail' $ unsafeUnfoldModuleIdent ns
         let destNest = joinPath modPath
         let destPath = destdir </> destNest
         let destFile = destdir </> srcfile <.> ext

         Right _ <- coreLift $ mkdirAll $ destNest
             | Left err => throw $ InternalError $ unlines
                             [ "Can't make directories " ++ show modPath
                             , show err ]
         coreLift $ putStrLn $ "Installing " ++ srcPath ++ " to " ++ destPath
         when !(coreLift $ exists destFile) $ do
           -- Grant read/write access to the file we are about to overwrite.
           Right _ <- coreLift $ chmod destFile
             (MkPermissions [Read, Write] [Read, Write] [Read, Write])
             | Left err => throw $ UserError (show err)
           pure ()
         Right _ <- coreLift $ Tree.copyFile srcPath destFile
             | Left err => throw $ InternalError $ unlines
                             [ "Can't copy file " ++ srcPath ++ " to " ++ destPath
                             , show err ]
         -- Make the source read-only
         Right _ <- coreLift $ chmod destFile (MkPermissions [Read] [Read] [Read])
           | Left err => throw $ UserError (show err)
         pure ()

-- Install all the built modules in prefix/package/
-- We've already built and checked for success, so if any don't exist that's
-- an internal error.
install : {auto c : Ref Ctxt Defs} ->
          {auto o : Ref ROpts REPLOpts} ->
          PkgDesc ->
          List CLOpt ->
          (installSrc : Bool) ->
          Core ()
install pkg opts installSrc -- not used but might be in the future
    = do defs <- get Ctxt
         let build = build_dir (dirs (options defs))
         let src = source_dir (dirs (options defs))
         runScript (preinstall pkg)
         let toInstall = maybe (modules pkg)
                               (:: modules pkg)
                               (mainmod pkg)
         wdir <- getWorkingDir
         -- Make the package installation directory
         let targetDir = prefix_dir (dirs (options defs)) </>
                             "idris2-" ++ showVersion False version </>
                             installDir pkg
         Right _ <- coreLift $ mkdirAll targetDir
             | Left err => throw $ InternalError $ unlines
                             [ "Can't make directory " ++ targetDir
                             , show err ]
         True <- coreLift $ changeDir targetDir
             | False => throw $ InternalError $ "Can't change directory to " ++ targetDir

         -- We're in that directory now, so copy the files from
         -- wdir/build into it
         traverse_ (installFrom (wdir </> build) targetDir . fst) toInstall
         when installSrc $ do
           traverse_ (installSrcFrom wdir targetDir) toInstall
         coreLift_ $ changeDir wdir

         runScript (postinstall pkg)

-- Check package without compiling anything.
check : {auto c : Ref Ctxt Defs} ->
        {auto s : Ref Syn SyntaxInfo} ->
        {auto o : Ref ROpts REPLOpts} ->
        PkgDesc ->
        List CLOpt ->
        Core (List Error)
check pkg opts =
  do
    [] <- prepareCompilation pkg opts
      | errs => pure errs

    runScript (postbuild pkg)
    pure []

makeDoc : {auto c : Ref Ctxt Defs} ->
          {auto s : Ref Syn SyntaxInfo} ->
          {auto o : Ref ROpts REPLOpts} ->
          PkgDesc ->
          List CLOpt ->
          Core (List Error)
makeDoc pkg opts =
    do [] <- prepareCompilation pkg opts
         | errs => pure errs

       defs <- get Ctxt
       let build = build_dir (dirs (options defs))
       let docBase = build </> "docs"
       let docDir = docBase </> "docs"
       Right () <- coreLift $ mkdirAll docDir
         | Left err => fileError docDir err
       u <- newRef UST initUState
       setPPrint (MkPPOpts False False False)

       [] <- concat <$> for (modules pkg) (\(mod, filename) => do
           -- load dependencies
           let ns = miAsNamespace mod
           addImport (MkImport emptyFC False mod ns)

           -- generate docs for all visible names
           defs <- get Ctxt
           names <- allNames (gamma defs)
           let allInNamespace = filter (inNS ns) names
           visibleNames <- filterM (visible defs) allInNamespace

           let outputFilePath = docDir </> (show mod ++ ".html")
           allDocs <- for (sort visibleNames) $ \ nm =>
                        getDocsForName emptyFC nm shortNamesConfig
           let allDecls = annotate Declarations $ vcat allDocs

           -- grab module header doc
           syn  <- get Syn
           let modDoc = lookup mod (modDocstrings syn)
           log "doc.module" 10 $ unwords
             [ "Looked up doc for"
             , show mod
             , "and got:"
             , show modDoc
             ]
           log "doc.module" 15 $ "from: " ++ show (modDocstrings syn)

           Right () <- do doc <- renderModuleDoc mod modDoc allDecls
                          coreLift $ writeFile outputFilePath doc
             | Left err => fileError (docBase </> "index.html") err

           pure $ the (List Error) []
         )
         | errs => pure errs

       Right () <- coreLift $ writeFile (docBase </> "index.html") $ renderDocIndex pkg
         | Left err => fileError (docBase </> "index.html") err

       errs <- for cssFiles $ \ cssFile => do
          let fn = cssFile.filename ++ ".css"
          css <- readDataFile ("docs/" ++ fn)
          Right () <- coreLift $ writeFile (docBase </> fn) css
            | Left err => fileError (docBase </> fn) err
          pure (the (List Error) [])

       let [] = concat errs
           | err => pure err

       runScript (postbuild pkg)
       pure []
  where
    visible : Defs -> Name -> Core Bool
    visible defs n
        = do Just def <- lookupCtxtExact n (gamma defs)
                  | Nothing => pure False
             -- TODO: if we can find out, whether a def has been declared as
             -- part of an interface, hide it here
             pure $ case definition def of
                         (DCon _ _ _) => False
                         _ => (visibility def /= Private)

    inNS : Namespace -> Name -> Bool
    inNS ns (NS xns (UN _)) = ns == xns
    inNS _ _ = False

    fileError : String -> FileError -> Core (List Error)
    fileError filename err = pure [FileErr filename err]

-- Data.These.bitraverse hand specialised for Core
bitraverseC : (a -> Core c) -> (b -> Core d) -> These a b -> Core (These c d)
bitraverseC f g (This a)   = [| This (f a) |]
bitraverseC f g (That b)   = [| That (g b) |]
bitraverseC f g (Both a b) = [| Both (f a) (g b) |]

-- Data.StringTrie.foldWithKeysM hand specialised for Core
foldWithKeysC : Monoid b => (List String -> Core b) -> (List String -> a -> Core b) -> StringTrie a -> Core b
foldWithKeysC {a} {b} fk fv = go []
  where
  go : List String -> StringTrie a -> Core b
  go ks (MkStringTrie nd) =
    map bifold $ bitraverseC
                   (fv ks)
                   (\sm => foldlC
                             (\x, (k, vs) =>
                               do let ks' = ks++[k]
                                  y <- assert_total $ go ks' vs
                                  z <- fk ks'
                                  pure $ x <+> y <+> z)
                             neutral
                             (StringMap.toList sm))
                   nd

[semiunit] Semigroup () where
  _ <+> _ = ()

[monoidunit] Monoid () using semiunit where
  neutral = ()

clean : {auto c : Ref Ctxt Defs} ->
        {auto o : Ref ROpts REPLOpts} ->
        PkgDesc ->
        List CLOpt ->
        Core ()
clean pkg opts -- `opts` is not used but might be in the future
    = do defs <- get Ctxt
         runScript (preclean pkg)
         let pkgmods = maybe
                         (map fst (modules pkg))
                         (\m => fst m :: map fst (modules pkg))
                         (mainmod pkg)
         let toClean : List (List String, String)
               = mapMaybe (\ mod => case unsafeUnfoldModuleIdent mod of
                                       [] => Nothing
                                       (x :: xs) => Just(xs, x))
                          pkgmods
         srcdir <- getWorkingDir
         let d = dirs (options defs)
         let builddir = srcdir </> build_dir d </> "ttc"
         let outputdir = srcdir </> outputDirWithDefault d
         -- the usual pair syntax breaks with `No such variable a` here for some reason
         let pkgTrie : StringTrie (List String)
                     = foldl (\trie, ksv =>
                                let ks = Builtin.fst ksv
                                    v = Builtin.snd ksv
                                  in
                                insertWith (reverse ks) (maybe [v] (v::)) trie) empty toClean
         foldWithKeysC @{monoidunit} (deleteFolder builddir)
                       (\ks => map collapse . traverse (deleteBin builddir ks))
                       pkgTrie
         deleteFolder builddir []
         maybe (pure ()) (\e => delete (outputdir </> e))
               (executable pkg)
         runScript (postclean pkg)
  where
    collapse : List () -> ()
    collapse _ = ()

    delete : String -> Core ()
    delete path = do Right () <- coreLift $ removeFile path
                       | Left err => pure ()
                     coreLift $ putStrLn $ "Removed: " ++ path

    deleteFolder : String -> List String -> Core ()
    deleteFolder builddir ns = delete $ builddir </> joinPath ns

    deleteBin : String -> List String -> String -> Core ()
    deleteBin builddir ns mod
        = do let ttFile = builddir </> joinPath ns </> mod
             delete $ ttFile <.> "ttc"
             delete $ ttFile <.> "ttm"

-- Just load the given module, if it exists, which will involve building
-- it if necessary
runRepl : {auto c : Ref Ctxt Defs} ->
          {auto s : Ref Syn SyntaxInfo} ->
          {auto o : Ref ROpts REPLOpts} ->
          Maybe String ->
          Core ()
runRepl fname = do
  u <- newRef UST initUState
  origin <- maybe
    (pure $ Virtual Interactive) (\fname => do
      modIdent <- ctxtPathToNS fname
      pure (PhysicalIdrSrc modIdent)
      ) fname
  m <- newRef MD (initMetadata origin)
  case fname of
      Nothing => pure ()
      Just fn => do
        errs <- loadMainFile fn
        displayErrors errs
  repl {u} {s}

export
parsePkgFile : {auto c : Ref Ctxt Defs} ->
               {auto s : Ref Syn SyntaxInfo} ->
               {auto o : Ref ROpts REPLOpts} ->
               String -> Core PkgDesc
parsePkgFile file = do
  Right (pname, fs) <- coreLift $ parseFile file
                                          (do desc <- parsePkgDesc file
                                              eoi
                                              pure desc)
      | Left err => throw err
  addFields fs (initPkgDesc pname)

||| If the user did not provide a package file we can look in the working
||| directory. If there is exactly one `.ipkg` file then use that!
localPackageFile : Maybe String -> Core String
localPackageFile (Just fp) = pure fp
localPackageFile Nothing
  = do wdir <- getWorkingDir
       tree <- coreLift (explore $ parse wdir)
       let candidates = map fileName tree.files
       case filter (".ipkg" `isSuffixOf`) candidates of
         [fp] => pure fp
         [] => throw $ UserError "No .ipkg file supplied and none could be found in the working directory."
         _ => throw $ UserError "No .ipkg file supplied and the working directory contains more than one."

processPackage : {auto c : Ref Ctxt Defs} ->
                 {auto s : Ref Syn SyntaxInfo} ->
                 {auto o : Ref ROpts REPLOpts} ->
                 List CLOpt ->
                 (PkgCommand, Maybe String) ->
                 Core ()
processPackage opts (cmd, mfile)
    = withCtxt . withSyn . withROpts $ case cmd of
        Init =>
          do pkg <- coreLift interactive
             let fp = fromMaybe (pkg.name ++ ".ipkg") mfile
             False <- coreLift (exists fp)
               | _ => throw (GenericMsg emptyFC ("File " ++ fp ++ " already exists"))
             Right () <- coreLift $ writeFile fp (show $ the (Doc ()) $ pretty pkg)
               | Left err => throw (FileErr fp err)
             pure ()
        _ =>
          do file <- localPackageFile mfile
             let Just (dir, filename) = splitParent file
                 | _ => throw $ InternalError "Tried to split empty string"
             let True = isSuffixOf ".ipkg" filename
                 | _ => do coreLift $ putStrLn ("Packages must have an '.ipkg' extension: " ++ show file ++ ".")
                           coreLift (exitWith (ExitFailure 1))
             setWorkingDir dir
             Right (pname, fs) <- coreLift $ parseFile filename (parsePkgDesc filename <* eoi)
                | Left err => throw err
             pkg <- addFields fs (initPkgDesc pname)
             whenJust (builddir pkg) setBuildDir
             setOutputDir (outputdir pkg)
             case cmd of
                  Build => do [] <- build pkg opts
                                 | errs => coreLift (exitWith (ExitFailure 1))
                              pure ()
                  MkDoc => do [] <- makeDoc pkg opts
                                 | errs => coreLift (exitWith (ExitFailure 1))
                              pure ()
                  Install => do [] <- build pkg opts
                                   | errs => coreLift (exitWith (ExitFailure 1))
                                install pkg opts {installSrc = False}
                  InstallWithSrc =>
                             do [] <- build pkg opts
                                   | errs => coreLift (exitWith (ExitFailure 1))
                                install pkg opts {installSrc = True}
                  Typecheck => do
                    [] <- check pkg opts
                      | errs => coreLift (exitWith (ExitFailure 1))
                    pure ()
                  Clean => clean pkg opts
                  REPL => do
                    [] <- build pkg opts
                       | errs => coreLift (exitWith (ExitFailure 1))
                    runRepl (map snd $ mainmod pkg)
                  Init => pure () -- already handled earlier

record PackageOpts where
  constructor MkPFR
  pkgDetails : List (PkgCommand, Maybe String)
  oopts : List CLOpt
  hasError : Bool

partitionOpts : List CLOpt -> PackageOpts
partitionOpts opts = foldr pOptUpdate (MkPFR [] [] False) opts
  where
    data OptType : Type where
      PPackage : PkgCommand -> Maybe String -> OptType
      POpt : OptType
      PIgnore : OptType
      PErr : OptType
    optType : CLOpt -> OptType
    optType (Package cmd f)        = PPackage cmd f
    optType Quiet                  = POpt
    optType Verbose                = POpt
    optType Timing                 = POpt
    optType (Logging l)            = POpt
    optType CaseTreeHeuristics     = POpt
    optType (DumpCases f)          = POpt
    optType (DumpLifted f)         = POpt
    optType (DumpVMCode f)         = POpt
    optType DebugElabCheck         = POpt
    optType (SetCG f)              = POpt
    optType (Directive d)          = POpt
    optType (BuildDir f)           = POpt
    optType (OutputDir f)          = POpt
    optType WarningsAsErrors       = POpt
    optType HashesInsteadOfModTime = POpt
    optType Profile                = POpt
    optType (ConsoleWidth n)       = PIgnore
    optType (Color b)              = PIgnore
    optType NoBanner               = PIgnore
    optType x                      = PErr

    pOptUpdate : CLOpt -> (PackageOpts -> PackageOpts)
    pOptUpdate opt with (optType opt)
      pOptUpdate opt | (PPackage cmd f) = record {pkgDetails $= ((cmd, f)::)}
      pOptUpdate opt | POpt    = record {oopts $= (opt::)}
      pOptUpdate opt | PIgnore = id
      pOptUpdate opt | PErr    = record {hasError = True}

errorMsg : String
errorMsg = unlines
  [ "Not all command line options can be used to override package options.\n"
  , "Overridable options are:"
  , "    --quiet"
  , "    --verbose"
  , "    --timing"
  , "    --log <log level>"
  , "    --dumpcases <file>"
  , "    --dumplifted <file>"
  , "    --dumpvmcode <file>"
  , "    --debug-elab-check"
  , "    --codegen <cg>"
  , "    --directive <directive>"
  , "    --build-dir <dir>"
  , "    --output-dir <dir>"
  ]

export
processPackageOpts : {auto c : Ref Ctxt Defs} ->
                     {auto s : Ref Syn SyntaxInfo} ->
                     {auto o : Ref ROpts REPLOpts} ->
                     List CLOpt -> Core Bool
processPackageOpts opts
    = do (MkPFR cmds@(_::_) opts' err) <- pure $ partitionOpts opts
             | (MkPFR Nil opts' _) => pure False
         if err
           then coreLift $ putStrLn (errorMsg ++ "\n")
           else traverse_ (processPackage opts') cmds
         pure True

-- find an ipkg file in one of the parent directories
-- If it exists, read it, set the current directory to the root of the source
-- tree, and set the relevant command line options before proceeding
export
findIpkg : {auto c : Ref Ctxt Defs} ->
           {auto r : Ref ROpts REPLOpts} ->
           {auto s : Ref Syn SyntaxInfo} ->
           Maybe String -> Core (Maybe String)
findIpkg fname
   = do Just (dir, ipkgn, up) <- coreLift findIpkgFile
             | Nothing => pure fname
        coreLift_ $ changeDir dir
        setWorkingDir dir
        Right (pname, fs) <- coreLift $ parseFile ipkgn
                                 (do desc <- parsePkgDesc ipkgn
                                     eoi
                                     pure desc)
            | Left err => throw err
        pkg <- addFields fs (initPkgDesc pname)
        maybe (pure ()) setBuildDir (builddir pkg)
        setOutputDir (outputdir pkg)
        processOptions (options pkg)
        loadDependencies (depends pkg)
        case fname of
             Nothing => pure Nothing
             Just srcpath  =>
                do let src' = up </> srcpath
                   setSource src'
                   opts <- get ROpts
                   put ROpts (record { mainfile = Just src' } opts)
                   pure (Just src')
  where
    dropHead : String -> List String -> List String
    dropHead str [] = []
    dropHead str (x :: xs)
        = if x == str then xs else x :: xs

    loadDependencies : List Depends -> Core ()
    loadDependencies = traverse_ (\p => addPkgDir p.pkgname p.pkgbounds)


text:
module Common

import public Common.Felt

data World : Type where [external]

public export
data CairoRes : Type -> Type where
     MkCairoRes : (1 _ : World) -> (result : a) -> CairoRes a

public export
PrimCairo : Type -> Type
PrimCairo a = (1 _ : World) -> CairoRes a

public export
PrimCairoUnit : Type
PrimCairoUnit = (1 _ : World) -> World

public export
data Cairo : Type -> Type where
    MkCairo : (1 _ : PrimCairo a) -> Cairo a

public export %inline
fromPrimCairo : (1 _ : PrimCairo a) -> Cairo a
fromPrimCairo = MkCairo

public export %inline
fromPrimCairoUnit : (1 _ : PrimCairoUnit) -> Cairo ()
fromPrimCairoUnit f = MkCairo (\s => MkCairoRes (f s) ())

public export %inline
toPrimCairo : (1 ca : Cairo a) -> PrimCairo a
toPrimCairo (MkCairo f) = f

%noinline
public export
unsafePerformIO : (ca : Cairo a) -> a
unsafePerformIO ca = let (MkCairoRes _ a) = (toPrimCairo ca (believe_me 0)) in a

-- Specializing Functor for performance
public export -- %spec f,ca
map : (f : (a -> b)) -> (1 ca : Cairo a) -> Cairo b
map f (MkCairo ma) = MkCairo
      (\s => let MkCairoRes s' a = ma s
              in MkCairoRes s' (f a))

-- Specializing Applicative for performance
public export -- %spec v
pure : (v:a) -> Cairo a
pure a = MkCairo (\s => MkCairoRes s a)

public export -- %spec cf,ca
(<*>) : (cf : Cairo (a -> b)) -> (ca : Cairo a) -> Cairo b
(MkCairo mf) <*> (MkCairo ma) =
  MkCairo (\s => let MkCairoRes s' f = mf s
                     MkCairoRes s'' a = ma s'
                  in MkCairoRes s'' (f a))

-- Specializing Monad for performance
public export -- %spec ca,f
(>>=) : (1 ca: Cairo a) -> (1 f: (a -> Cairo b)) -> Cairo b
(MkCairo ma) >>= f =
  MkCairo (\s => let MkCairoRes s' a = ma s
                  in toPrimCairo (f a) s')

-- This is important for performance
public export -- %spec ma,mb
(>>) : (ma: Cairo ()) -> (mb: (Cairo a)) -> Cairo a
(MkCairo ma) >> (MkCairo mb) =
  MkCairo (\s => let MkCairoRes s' _ = ma s in mb s')

{-
export %inline
Functor Cairo where
    map = Main.map

export %inline
Applicative Cairo where
    pure = Main.pure
    (<*>) = Main.(<*>)

export %inline
Monad Cairo where
   (>>=) = Main.(>>=)
   join x = x >>= id
-}

--------------------------------------------
-- Traversable (specialised) halfs the number of steps. why?
public export -- %spec f
traverse : (f: (a -> Cairo b)) -> (la: List a) -> Cairo (List b)
traverse f xs = traverse' xs []
  where
    traverse' : List a -> List b -> Cairo (List b)
    traverse' [] acc = pure (reverse acc)
    traverse' (x :: xs) acc = traverse' xs (!(f x) :: acc)

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module Main

%default total

-- An expensive function.
qib : Nat -> Nat
qib       Z   = 1
qib    (S Z)  = 2
qib (S (S n)) = qib n * qib (S n)

-- An equality whose size reflects the size of numbers.
data Equals : Nat -> Nat -> Type where
    EqZ : Z `Equals` Z
    EqS : m `Equals` n -> S m `Equals` S n

eq_refl : {n : Nat} -> n `Equals` n
eq_refl {n = Z}   = EqZ
eq_refl {n = S n} = EqS eq_refl

-- Here, the proof is very expensive to compute.
-- We add a recursive argument to prevent Idris from inlining the function.
f : (r, n : Nat) -> Subset Nat (\k => qib n `Equals` qib k)
f  Z    n = Element n eq_refl
f (S r) n = f r n

-- A (contrived) relation, just to have something to show.
data Represents : Nat -> Nat -> Type where
  Axiom : (n : Nat) -> qib n `Represents` n

-- Here, the witness is very expensive to compute.
-- We add a recursive argument to prevent Idris from inlining the function.
g : (r, n : Nat) -> Exists (\k : Nat => k `Represents` n)
g  Z    n = Evidence (qib n) (Axiom n)
g (S r) n = g r n

fmt : qib n `Represents` n -> String
fmt (Axiom n) = "Axiom " ++ show n

main : IO ()
main = do
    n <- map (const (the Nat 10000)) (putStrLn "*oink*")
    putStrLn . show $ getWitness (f 4 n)
    putStrLn . fmt  $ getProof   (g 4 n)

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Test.Array

import Data.SOP
import Hedgehog
import JS

ints : Gen (List Int)
ints = list (linear 0 10) (int $ linearFrom 0 (-100) 100)

intss : Gen (List $ List Int)
intss = list (linear 0 10) ints

arrInt : Gen (IArray Int)
arrInt = map fromList ints

prop_sizeEmpty : Property
prop_sizeEmpty =
  property $ do ns <- forAll (pure $ the (List Int32) Nil)
                size (JS.Array.fromList ns) === 0

prop_size : Property
prop_size =
  property $ do ns <- forAll ints
                size (JS.Array.fromList ns) ===
                fromInteger (natToInteger $ length ns)

prop_fromListToList : Property
prop_fromListToList =
  property $ do ns <- forAll ints
                ns === arrayToList (JS.Array.fromList ns)

prop_fromString : Property
prop_fromString =
  property $ do s <- forAll $ string (linear 0 20) ascii
                unpack s === arrayToList (fromString s)

prop_map : Property
prop_map = property $ do arr <- forAll arrInt
                         map id arr === arr

prop_join : Property
prop_join = property $ do iss <- forAll intss
                          join iss ===
                          (arrayToList . JS.Array.concat) (fromList $ map fromList iss)

export
test : IO ()
test = ignore . checkGroup . withTests 100 $ MkGroup "Arrays" [
         ("prop_sizeEmpty", prop_sizeEmpty)
       , ("prop_size", prop_size)
       , ("prop_fromListToList", prop_fromListToList)
       , ("prop_fromString", prop_fromString)
       , ("prop_map", prop_map)
       , ("prop_join", prop_join)
       ]


text:
module Data.List.Predicates.Pairs

import public Data.List
import public Data.Pair.Predicates

import public Data.List.Predicates.Unique

%default total
%access public export

data UniquePairs : (prfSame : a -> a -> Type)
                -> (ps : List (Pair a a))
                -> Type
  where
    MkUniquePairs : (ps  : List (Pair a a))
            -> (prf : Unique (PairEq prfSame) ps)
            -> UniquePairs prfSame ps

pairsNotUnique : (decEq : (x : a) -> (y : a) -> Dec (prfSame x y))
              -> (contra : Unique (PairEq prfSame) ps -> Void)
              -> UniquePairs prfSame ps
              -> Void
pairsNotUnique decEq contra (MkUniquePairs ps prf) = contra prf

uniquePairs : (decEq : (x,y : a) -> Dec (prfSame x y))
           -> (ps : List (Pair a a))
           -> Dec (UniquePairs prfSame ps)
uniquePairs decEq ps with (unique (pairEq decEq) ps)
  uniquePairs decEq ps | (Yes prf) = Yes (MkUniquePairs ps prf)
  uniquePairs decEq ps | (No contra) = No (pairsNotUnique decEq contra)

data PairOrigin : (p : Pair a a)
               -> (src : List a)
               -> Type
  where
    MkPO : Elem a src
        -> Elem b src
        -> PairOrigin (MkPair a b) src

aNotInSrc : (contra : Elem a src -> Void) -> PairOrigin (a, b) src -> Void
aNotInSrc contra (MkPO x y) = contra x

bNotInSrc : (contra : Elem b src -> Void) -> PairOrigin (a, b) src -> Void
bNotInSrc contra (MkPO x y) = contra y

originPair : DecEq a
          => (p : Pair a a)
          -> (src : List a)
          -> Dec (PairOrigin p src)
originPair (a, b) src with (isElem a src)
  originPair (a, b) src | (Yes prfA) with (isElem b src)
    originPair (a, b) src | (Yes prfA) | (Yes prfB) = Yes (MkPO prfA prfB)
    originPair (a, b) src | (Yes prfA) | (No contra) = No (bNotInSrc contra)

  originPair (a, b) src | (No contra) = No (aNotInSrc contra)

data PairsOrigin : (orig  : List a)
                -> (pairs : List (Pair a a))
                -> Type
  where
   First : PairOrigin p orig -> PairsOrigin orig [p]
   Rest : PairOrigin p orig
       -> PairsOrigin orig ps
       -> PairsOrigin orig (p::ps)

listEmpty : PairsOrigin src [] -> Void
listEmpty (First _) impossible
listEmpty (Rest _ _) impossible

headNotRightRestEmpty : (contra : PairOrigin x src -> Void)
                     -> PairsOrigin src [x]
                     -> Void
headNotRightRestEmpty contra (First x) = contra x
headNotRightRestEmpty contra (Rest x y) = contra x

headRightRestNot : (contra : PairsOrigin src (y :: ys) -> Void)
                -> PairsOrigin src (x :: (y :: ys)) -> Void
headRightRestNot contra (Rest x y) = contra y

headNotRight : (contra : PairOrigin x src -> Void)
            -> PairsOrigin src (x :: (y :: ys))
            -> Void
headNotRight contra (Rest x y) = contra x

originPairs : DecEq a
           => (src : List a)
           -> (ps : List (Pair a a))
           -> Dec (PairsOrigin src ps)
originPairs src [] = No listEmpty
originPairs src (x :: xs) with (xs)
  originPairs src (x :: xs) | [] with (originPair x src)
    originPairs src ((a, b) :: xs) | [] | (Yes (MkPO y z)) = Yes (First (MkPO y z))
    originPairs src (x :: xs) | [] | (No contra) = No (headNotRightRestEmpty contra)

  originPairs src (x :: xs) | (y :: ys) with (originPair x src)
    originPairs src (x :: xs) | (y :: ys) | (Yes prfX) with (assert_total $ originPairs src (y::ys))
      originPairs src (x :: xs) | (y :: ys) | (Yes prfX) | (Yes prf) = Yes (Rest prfX prf)
      originPairs src (x :: xs) | (y :: ys) | (Yes prfX) | (No contra) = No (headRightRestNot contra)

    originPairs src (x :: xs) | (y :: ys) | (No contra) = No (headNotRight contra)


text:
module AltRandomBinaryAccessList

import RandomAccessList

%default total
%access private

export
data BinaryList a = Nil | Zero (BinaryList (a, a)) | One a (BinaryList (a,a))

uncons : BinaryList a -> (a, BinaryList a)
uncons Nil = idris_crash "empty list"
uncons (One x Nil) = (x, Nil)
uncons (One x ps) = (x, Zero ps)
uncons (Zero ps) = let ((x, y), ps') = uncons ps in (x, One y ps')

mutual
  fupdate : (a -> a) -> Int -> BinaryList a -> BinaryList a
  fupdate f i Nil = idris_crash "bad subscript"
  fupdate f 0 (One x ps) = One (f x) ps
  fupdate f i (One x ps) = cons x (fupdate f (i - 1) (assert_smaller (One x ps) $ Zero ps))
  fupdate f i (Zero ps) = let i' = assert_total $ i `div` 2
                              r  = assert_total $ i `mod` 2
                              f' = \(x, y) => if 0 == r then (f x, y) else (x, f y)
                          in Zero (fupdate f' i' ps)

  export
  RandomAccessList BinaryList where
    empty = Nil
    isEmpty Nil = True
    isEmpty _   = False

    cons x Nil        = One x Nil
    cons x (Zero ps)  = One x ps
    cons x (One y ps) = Zero (cons (x, y) ps)

    head xs = fst (uncons xs)
    tail xs = snd (uncons xs)

    lookup i Nil = idris_crash "bad subscript"
    lookup 0 (One x ps) = x
    lookup i (One x ps) = lookup (i - 1) (assert_smaller (One x ps) $ Zero ps)
    lookup i (Zero ps) = let i' = assert_total $ i `div` 2
                             r  = assert_total $ i `mod` 2
                             (x, y) = lookup i' ps
                         in if 0 == r then x else y

    update i y xs = fupdate (\x => y) i xs


text:
module Optimisation.Inliner

import Data.SortedSet
import Data.SortedMap
import Core.Context
import CairoCode.CairoCode
import CairoCode.CairoCodeUtils
import Utils.Helpers
import CairoCode.Traversal.Base
import Optimisation.DeadCodeElimination

import Optimisation.StaticProcessing.IterativeBaseTransformer
import Optimisation.StaticProcessing.StaticTracker
import Optimisation.StaticProcessing.StaticTransformer
import Optimisation.OrderAndEliminateDefinitions
import CommonDef

import Debug.Trace

%hide Prelude.toList

isMachineName : Name -> Bool
isMachineName (NS _ innerName) = isMachineName innerName
isMachineName (PV innerName _)  = isMachineName innerName
isMachineName (DN _ innerName)  = isMachineName innerName
isMachineName (Nested _ innerName)  = isMachineName innerName
isMachineName (UN _ ) = False
isMachineName (MN _ _) = True
isMachineName _ = True

containsClosure : StaticInfo -> Bool
containsClosure (MKStaticInfo _ (Closure _ _)) = True
containsClosure (MKStaticInfo _ (Constructed inner)) = any (\infs => any containsClosure infs) (values inner)
containsClosure _ = False

inlineDecider : FunData -> Bool
inlineDecider (MKFunData name (FunDef _ _ _ _) _ _ args rs) = if name == cairo_main
    then True
    else (isMachineName name) || (any containsClosure (args ++ (map snd rs))) --  True

inlineDecider _ = False

inline : RegisterGen -> Name -> FunData -> (RegisterGen, List (InstVisit CairoReg))
inline regGen curName fd@(MKFunData name target@(FunDef params implsTrg _ insts) implsIn implsOut args rets) = (snd splitRegGen, returnElevated)
       where splitRegGen : (RegisterGen, RegisterGen)
             splitRegGen = splitRegisterGen regGen
             inlineRegGen : RegisterGen
             inlineRegGen = fst splitRegGen
             paramRegs : SortedMap CairoReg CairoReg
             paramRegs = fromList $ (zip params (map resolveInfToReg args))
                            ++ (map (\(impl,freg) => (freg, resolveImpl impl)) (toList $implsTrg))
                where resolveImpl : LinearImplicit -> CairoReg
                      resolveImpl lin = fromMaybe (assert_total $ idris_crash "Call is missing linear implicit param") (maybeMap resolveInfToReg (lookup lin implsIn))
             substituted : (Name, CairoDef)
             substituted = substituteDefRegisters subs (name, target)
                where subs : CairoReg -> Maybe CairoReg
                      subs (Const c) = Nothing
                      subs Eliminated = Nothing
                      subs reg = case lookup reg paramRegs of
                        (Just nReg) => Just nReg
                        Nothing => Just $ deriveRegister inlineRegGen reg
             -- todo: Note: For this to work our seamantics must be limited to have returns in tail positions
             --       - This holds for idris code
             --       - However, imperative programmers expect a different return semantic
             returnElevated : List (InstVisit CairoReg)
             returnElevated = snd $ runVisitConcatCairoDef (replaceReturn, ()) substituted
                where replaceReturn : InstVisit CairoReg ->  Traversal () (List (InstVisit CairoReg))
                      replaceReturn (VisitFunction _ _ _ _) = pure []
                      replaceReturn VisitEndFunction= pure []
                      replaceReturn (VisitReturn retRegs retImpls) = pure $ (zipWith (\a,r => VisitAssign (fst a) r) rets retRegs)  ++ map (\(lin,r) => VisitAssign (resolveImpl lin) r) (toList retImpls)
                        where resolveImpl : LinearImplicit -> CairoReg
                              resolveImpl lin = fromMaybe (assert_total $ idris_crash "Call is missing linear implicit return") (maybeMap fst (lookup lin implsOut))
                      replaceReturn inst = pure [inst]
inline regGen _ fd  = (regGen, genFunCall fd)

collectDependencies : (Name, CairoDef) -> SortedSet Name
collectDependencies def = snd $ runVisitConcatCairoDef (pureTraversal dependencyCollector) def
    where dependencyCollector : InstVisit CairoReg -> SortedSet Name
          dependencyCollector (VisitCall _ _ name _) = singleton name
          dependencyCollector _ = empty

isTerminal : (Name, CairoDef) -> Bool
isTerminal def = contains (fst def) (collectDependencies def)

localInlining : RegisterGen -> Name -> List (Name, CairoDef) -> List (Name, CairoDef)
localInlining regGen name allDefs = iterativeCallTransform regGen maybeInline cleanUp name allDefs
    where cleanUp : (Name, CairoDef) ->  (Name, CairoDef)
          cleanUp def = eliminateDeadCode $ localStaticOptimizeDef allDefs def
          maybeInline : RegisterGen -> Name -> FunData -> (RegisterGen, Maybe (List (InstVisit CairoReg)))
          maybeInline regGen intoName fd =  if isTerminal (fd.function, fd.target)
            then (regGen, Nothing)
            else if (inlineDecider fd)
                then let (nRegGen, res) = inline regGen intoName fd in (nRegGen, Just res)
                else (regGen, Nothing)

export
inlineDefs : Name -> List (Name, CairoDef) -> List (Name, CairoDef)
inlineDefs = localInlining (mkRegisterGen "inliner")

-- Note: even with Terminals we need still a upper limit because we mark funs with applies & MKClosures never as terminals
--       Further some crazy trampoline inlining could happen


text:
module IdrisJvm.ClientServerSocket

import IdrisJvm.IO
import Java.Nio

%access public export

namespace ClientServerSocket
  ClientServerSocketClass : JVM_NativeTy
  ClientServerSocketClass = Class "io/github/mmhelloworld/idrisjvm/io/ClientServerSocket"

  ClientServerSocket : Type
  ClientServerSocket = JVM_Native ClientServerSocketClass

  listenAndAccept : String -> Int -> JVM_IO (Either Throwable ClientServerSocket)
  listenAndAccept =
    invokeStatic ClientServerSocketClass "listenAndAccept" (String -> Int -> JVM_IO (Either Throwable ClientServerSocket))

  getChar : ClientServerSocket -> JVM_IO Char
  getChar = invokeInstance "getChar" (ClientServerSocket -> JVM_IO Char)

  getLine : ClientServerSocket -> JVM_IO String
  getLine = invokeInstance "getLine" (ClientServerSocket -> JVM_IO String)

  writeString : ClientServerSocket -> String -> JVM_IO ()
  writeString = invokeInstance "writeString" (ClientServerSocket -> String -> JVM_IO ())

  close : ClientServerSocket -> JVM_IO ()
  close = invokeInstance "close" (ClientServerSocket -> JVM_IO ())

  Inherits Channel ClientServerSocket where {}
  Inherits ReadableByteChannel ClientServerSocket where {}
  Inherits WritableByteChannel ClientServerSocket where {}