text:
module Data.Bits

import Data.DPair
import public Data.Nat

%default total

infixl 8 `shiftL`, `shiftR`
infixl 7 .&.
infixl 6 `xor`
infixl 5 .|.

||| Utility for using bitwise operations at compile
||| time.
|||
||| ```idris example
||| the Bits8 13 `shiftL` fromNat 3
||| ```
export
fromNat :  (k : Nat)
        -> {n : Nat}
        -> {auto 0 prf : lt k n === True}
        -> Subset Nat (`LT` n)
fromNat k = Element k (ltReflectsLT k n prf)

--------------------------------------------------------------------------------
--          Interface Bits
--------------------------------------------------------------------------------

||| The `Bits` interface defines bitwise operations over integral types.
public export
interface Bits a where
  0 Index : Type

  ||| Bitwise "and"
  (.&.) : a -> a -> a

  ||| Bitwise "or"
  (.|.) : a -> a -> a

  ||| Bitwise "xor".
  xor : a -> a -> a

  ||| Shift the argument left by the specified number of bits.
  shiftL : a -> Index -> a

  ||| Shift the argument right by the specified number of bits.
  shiftR : a -> Index -> a

  ||| Sets the `i`-th bit.
  bit : (i : Index) -> a

  ||| The value with all bits unset.
  zeroBits : a

  ||| Returns the bitwise complement of a value.
  complement : a -> a

  ||| The value with all bits set..
  oneBits : a
  oneBits = complement zeroBits

  ||| `complementBit x i` is the same as `xor x (bit i)`.
  complementBit : (x : a) -> (i : Index) -> a
  complementBit x i = x `xor` bit i

  ||| `clearBit x i` is the same as `x .&. complement (bit i)`
  clearBit : (x : a) -> (i : Index) -> a
  clearBit x i = x `xor` (bit i .&. x)

  ||| Tests, whether the i-th bit is set in the given value.
  testBit : a -> Index -> Bool

  ||| Sets the i-th bit of a value.
  setBit : a -> (i : Index) -> a
  setBit x i = x .|. bit i

public export %inline
Bits Bits8 where
  Index       = Subset Nat (`LT` 8)
  (.&.)       = prim__and_Bits8
  (.|.)       = prim__or_Bits8
  xor         = prim__xor_Bits8
  bit         = (1 `shiftL`)
  zeroBits    = 0
  testBit x i = (x .&. bit i) /= 0
  shiftR x    = prim__shr_Bits8 x . cast . fst
  shiftL x    = prim__shl_Bits8 x . cast . fst
  complement  = xor 0xff
  oneBits     = 0xff

public export %inline
Bits Bits16 where
  Index       = Subset Nat (`LT` 16)
  (.&.)       = prim__and_Bits16
  (.|.)       = prim__or_Bits16
  xor         = prim__xor_Bits16
  bit         = (1 `shiftL`)
  zeroBits    = 0
  testBit x i = (x .&. bit i) /= 0
  shiftR x    = prim__shr_Bits16 x . cast . fst
  shiftL x    = prim__shl_Bits16 x . cast . fst
  complement  = xor 0xffff
  oneBits     = 0xffff

public export %inline
Bits Bits32 where
  Index       = Subset Nat (`LT` 32)
  (.&.)       = prim__and_Bits32
  (.|.)       = prim__or_Bits32
  xor         = prim__xor_Bits32
  bit         = (1 `shiftL`)
  zeroBits    = 0
  testBit x i = (x .&. bit i) /= 0
  shiftR x    = prim__shr_Bits32 x . cast . fst
  shiftL x    = prim__shl_Bits32 x . cast . fst
  complement  = xor 0xffffffff
  oneBits     = 0xffffffff

public export %inline
Bits Bits64 where
  Index       = Subset Nat (`LT` 64)
  (.&.)       = prim__and_Bits64
  (.|.)       = prim__or_Bits64
  xor         = prim__xor_Bits64
  bit         = (1 `shiftL`)
  zeroBits    = 0
  testBit x i = (x .&. bit i) /= 0
  shiftR x    = prim__shr_Bits64 x . cast . fst
  shiftL x    = prim__shl_Bits64 x . cast . fst
  complement  = xor 0xffffffffffffffff
  oneBits     = 0xffffffffffffffff

public export %inline
Bits Int where
  Index       = Subset Nat (`LT` 64)
  (.&.)       = prim__and_Int
  (.|.)       = prim__or_Int
  xor         = prim__xor_Int
  bit         = (1 `shiftL`)
  zeroBits    = 0
  testBit x i = (x .&. bit i) /= 0
  shiftR x    = prim__shr_Int x . cast . fst
  shiftL x    = prim__shl_Int x . cast . fst
  complement  = xor (-1)
  oneBits     = (-1)

public export %inline
Bits Int8 where
  Index       = Subset Nat (`LT` 8)
  (.&.)       = prim__and_Int8
  (.|.)       = prim__or_Int8
  xor         = prim__xor_Int8
  bit         = (1 `shiftL`)
  zeroBits    = 0
  testBit x i = (x .&. bit i) /= 0
  shiftR x    = prim__shr_Int8 x . cast . fst
  shiftL x    = prim__shl_Int8 x . cast . fst
  complement  = xor (-1)
  oneBits     = (-1)

public export %inline
Bits Int16 where
  Index       = Subset Nat (`LT` 16)
  (.&.)       = prim__and_Int16
  (.|.)       = prim__or_Int16
  xor         = prim__xor_Int16
  bit         = (1 `shiftL`)
  zeroBits    = 0
  testBit x i = (x .&. bit i) /= 0
  shiftR x    = prim__shr_Int16 x . cast . fst
  shiftL x    = prim__shl_Int16 x . cast . fst
  complement  = xor (-1)
  oneBits     = (-1)

public export %inline
Bits Int32 where
  Index       = Subset Nat (`LT` 32)
  (.&.)       = prim__and_Int32
  (.|.)       = prim__or_Int32
  xor         = prim__xor_Int32
  bit         = (1 `shiftL`)
  zeroBits    = 0
  testBit x i = (x .&. bit i) /= 0
  shiftR x    = prim__shr_Int32 x . cast . fst
  shiftL x    = prim__shl_Int32 x . cast . fst
  complement  = xor (-1)
  oneBits     = (-1)

public export %inline
Bits Int64 where
  Index       = Subset Nat (`LT` 64)
  (.&.)       = prim__and_Int64
  (.|.)       = prim__or_Int64
  xor         = prim__xor_Int64
  bit         = (1 `shiftL`)
  zeroBits    = 0
  testBit x i = (x .&. bit i) /= 0
  shiftR x    = prim__shr_Int64 x . cast . fst
  shiftL x    = prim__shl_Int64 x . cast . fst
  complement  = xor (-1)
  oneBits     = (-1)

public export %inline
Bits Integer where
  Index       = Nat
  (.&.)       = prim__and_Integer
  (.|.)       = prim__or_Integer
  xor         = prim__xor_Integer
  bit         = (1 `shiftL`)
  zeroBits    = 0
  testBit x i = (x .&. bit i) /= 0
  shiftR x    = prim__shr_Integer x . natToInteger
  shiftL x    = prim__shl_Integer x . natToInteger
  complement  = xor (-1)
  oneBits     = (-1)

--------------------------------------------------------------------------------
--          FiniteBits
--------------------------------------------------------------------------------

public export
interface Bits a => FiniteBits a where
  ||| Return the number of bits in values of type `t`.
  bitSize : Nat

  ||| Properly correlates `bitSize` and `Index`.
  bitsToIndex : Subset Nat (`LT` bitSize) -> Index {a}

  ||| Return the number of set bits in the argument.  This number is
  ||| known as the population count or the Hamming weight.
  popCount : a -> Nat

public export %inline
FiniteBits Bits8 where
  bitSize     = 8
  bitsToIndex = id

  popCount x0 =
    -- see https://stackoverflow.com/questions/109023/how-to-count-the-number-of-set-bits-in-a-32-bit-integer
    let x1 = (x0 .&. 0x55) + ((x0 `shiftR` fromNat 1) .&. 0x55)
        x2 = (x1 .&. 0x33) + ((x1 `shiftR` fromNat 2) .&. 0x33)
        x3 = ((x2 + (x2 `shiftR` fromNat 4)) .&. 0x0F)
     in cast x3

public export %inline
FiniteBits Bits16 where
  bitSize     = 16
  bitsToIndex = id

  popCount x0 =
    -- see https://stackoverflow.com/questions/109023/how-to-count-the-number-of-set-bits-in-a-32-bit-integer
    let x1 = (x0 .&. 0x5555) + ((x0 `shiftR` fromNat 1) .&. 0x5555)
        x2 = (x1 .&. 0x3333) + ((x1 `shiftR` fromNat 2) .&. 0x3333)
        x3 = ((x2 + (x2 `shiftR` fromNat 4)) .&. 0x0F0F)
        x4 = (x3 * 0x0101) `shiftR` fromNat 8
     in cast x4

public export %inline
FiniteBits Bits32 where
  bitSize     = 32
  bitsToIndex = id

  popCount x0 =
    -- see https://stackoverflow.com/questions/109023/how-to-count-the-number-of-set-bits-in-a-32-bit-integer
    let x1 = (x0 .&. 0x55555555) + ((x0 `shiftR` fromNat 1) .&. 0x55555555)
        x2 = (x1 .&. 0x33333333) + ((x1 `shiftR` fromNat 2) .&. 0x33333333)
        x3 = ((x2 + (x2 `shiftR` fromNat 4)) .&. 0x0F0F0F0F)
        x4 = (x3 * 0x01010101) `shiftR` fromNat 24
     in cast x4

public export %inline
FiniteBits Bits64 where
  bitSize     = 64
  bitsToIndex = id

  popCount x0 =
    -- see https://stackoverflow.com/questions/109023/how-to-count-the-number-of-set-bits-in-a-64-bit-integer
    let x1 = (x0 .&. 0x5555555555555555) +
             ((x0 `shiftR` fromNat 1) .&. 0x5555555555555555)
        x2 = (x1 .&. 0x3333333333333333)
             + ((x1 `shiftR` fromNat 2) .&. 0x3333333333333333)
        x3 = ((x2 + (x2 `shiftR` fromNat 4)) .&. 0x0F0F0F0F)
        x4 = (x3 * 0x0101010101010101) `shiftR` fromNat 56
     in cast x4

public export %inline
FiniteBits Int where
  bitSize     = 64
  bitsToIndex = id

  popCount x =
    -- see https://stackoverflow.com/questions/109023/how-to-count-the-number-of-set-bits-in-a-32-bit-integer
    -- We have to treat negative numbers separately in order to
    -- prevent overflows in the first addition.
    -- The top bit is therefore cleared and 1 is added in the end
    -- in case of a negative number
    let x0 = x `clearBit` fromNat 63
        x1 = (x0 .&. 0x5555555555555555)
           + ((x0 `shiftR` fromNat 1) .&. 0x5555555555555555)
        x2 = (x1 .&. 0x3333333333333333)
           + ((x1 `shiftR` fromNat 2) .&. 0x3333333333333333)
        x3 = ((x2 + (x2 `shiftR` fromNat 4)) .&. 0x0F0F0F0F0F0F0F0F)
        x4 = (x3 * 0x0101010101010101) `shiftR` fromNat 56
        x5 = if x < 0 then x4 + 1 else x4
     in cast x5

public export %inline
FiniteBits Int8 where
  bitSize     = 8
  bitsToIndex = id

  popCount x =
    -- see https://stackoverflow.com/questions/109023/how-to-count-the-number-of-set-bits-in-a-32-bit-integer
    -- We have to treat negative numbers separately in order to
    -- prevent overflows in the first addition.
    -- The top bit is therefore cleared and 1 is added in the end
    -- in case of a negative number
    let x0 = x `clearBit` fromNat 7
        x1 = (x0 .&. 0x55) + ((x0 `shiftR` fromNat 1) .&. 0x55)
        x2 = (x1 .&. 0x33) + ((x1 `shiftR` fromNat 2) .&. 0x33)
        x3 = ((x2 + (x2 `shiftR` fromNat 4)) .&. 0x0F)
        x4 = if x < 0 then x3 + 1 else x3
     in cast x4

public export %inline
FiniteBits Int16 where
  bitSize     = 16
  bitsToIndex = id

  popCount x =
    -- see https://stackoverflow.com/questions/109023/how-to-count-the-number-of-set-bits-in-a-32-bit-integer
    -- We have to treat negative numbers separately in order to
    -- prevent overflows in the first addition.
    -- The top bit is therefore cleared and 1 is added in the end
    -- in case of a negative number
    let x0 = x `clearBit` fromNat 15
        x1 = (x0 .&. 0x5555) + ((x0 `shiftR` fromNat 1) .&. 0x5555)
        x2 = (x1 .&. 0x3333) + ((x1 `shiftR` fromNat 2) .&. 0x3333)
        x3 = ((x2 + (x2 `shiftR` fromNat 4)) .&. 0x0F0F)
        x4 = (x3 * 0x0101) `shiftR` fromNat 8
        x5 = if x < 0 then x4 + 1 else x4
     in cast x5

public export %inline
FiniteBits Int32 where
  bitSize     = 32
  bitsToIndex = id

  popCount x =
    -- see https://stackoverflow.com/questions/109023/how-to-count-the-number-of-set-bits-in-a-32-bit-integer
    -- We have to treat negative numbers separately in order to
    -- prevent overflows in the first addition.
    -- The top bit is therefore cleared and 1 is added in the end
    -- in case of a negative number
    let x0 = x `clearBit` fromNat 31
        x1 = (x0 .&. 0x55555555) + ((x0 `shiftR` fromNat 1) .&. 0x55555555)
        x2 = (x1 .&. 0x33333333) + ((x1 `shiftR` fromNat 2) .&. 0x33333333)
        x3 = ((x2 + (x2 `shiftR` fromNat 4)) .&. 0x0F0F0F0F)
        x4 = (x3 * 0x01010101) `shiftR` fromNat 24
        x5 = if x < 0 then x4 + 1 else x4
     in cast x5

public export %inline
FiniteBits Int64 where
  bitSize     = 64
  bitsToIndex = id

  popCount x =
    -- see https://stackoverflow.com/questions/109023/how-to-count-the-number-of-set-bits-in-a-32-bit-integer
    -- We have to treat negative numbers separately in order to
    -- prevent overflows in the first addition.
    -- The top bit is therefore cleared and 1 is added in the end
    -- in case of a negative number
    let x0 = x `clearBit` fromNat 63
        x1 = (x0 .&. 0x5555555555555555)
           + ((x0 `shiftR` fromNat 1) .&. 0x5555555555555555)
        x2 = (x1 .&. 0x3333333333333333)
           + ((x1 `shiftR` fromNat 2) .&. 0x3333333333333333)
        x3 = ((x2 + (x2 `shiftR` fromNat 4)) .&. 0x0F0F0F0F0F0F0F0F)
        x4 = (x3 * 0x0101010101010101) `shiftR` fromNat 56
        x5 = if x < 0 then x4 + 1 else x4
     in cast x5


text:
doPlus : Nat -> Nat -> Nat
doPlus x y = x `plus` y

doMult : Nat -> Nat -> Nat
doMult x y = x `mult` y

doMinus : Nat -> Nat -> Nat
doMinus x y = x `minus` y

ext: idr

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
singleton : Vector xs t ->
            Vector (1::xs) t
singleton t = [t]

invSingleton : Vector (1::xs) t ->
               Vector xs t
invSingleton [t] = t

max_stars_repo_name: RossMeikleham/MSci-Project

max_issues_repo_name: RossMeikleham/MSci-Project

max_forks_repo_name: RossMeikleham/MSci-Project


text:
import Data.Either
import Data.List
import Data.List1
import Data.Maybe
import Data.String

import System.File

data BingoNum = M Nat | U Nat

Show BingoNum where
  show (M k) = "m " ++ show k
  show (U k) = "u " ++ show k

Card : Type
Card = List (List BingoNum)

parseLines : (String -> Maybe a) -> String -> List a
parseLines f s = catMaybes $ f <$> lines s

getNumbers : List String -> Maybe (List Nat, List String)
getNumbers [] = Nothing
getNumbers (x :: xs) = Just (catMaybes $ parsePositive <$> (forget $ split (== ',') x),  xs)

parseCard : List String -> Card
parseCard l = (\s => U <$> (catMaybes $ parsePositive <$> (forget $ split (== ' ') s))) <$> l

parseCards : List String -> List Card
parseCards [] = []
parseCards (_ :: xs) = parseCard (take 5 xs) :: parseCards (drop 5 xs)

isMarked : BingoNum -> Bool
isMarked (M _) = True
isMarked (U _) = False

winRow : Card -> Bool
winRow [] = False
winRow (x :: xs) = all isMarked x || winRow xs

winColumn : Card -> Bool
winColumn c = any id $ foldl (\a => \bs => (\(b1, b2) => b1 && b2) <$> zip a (isMarked <$> bs)) (replicate 5 True) c

wins : Card -> Bool
wins c = winRow c || winColumn c

drawNumber : Nat -> Card -> Card
drawNumber n [] = []
drawNumber n (x :: xs) = ((\d => case d of
                                      M m => M m
                                      U u => if u == n
                                                then M u
                                                else U u) <$> x) :: drawNumber n xs

drawNumbers : List Nat -> List Card -> Maybe (Card, Nat)
drawNumbers [] cs = Nothing
drawNumbers (x :: xs) [] = Nothing
drawNumbers (x :: xs) (c :: []) = let nc = drawNumber x c in
                                      if wins nc
                                         then Just (nc, x)
                                         else drawNumbers xs (nc :: [])
drawNumbers (x :: xs) cs = let ncs = drawNumber x <$> cs
                               losing = filter (not . wins) ncs in
                               drawNumbers xs losing

scoreOf : Card -> Nat
scoreOf [] = 0
scoreOf (x :: xs) = (foldl (\a => \b => case b of
                                             M n => a
                                             U n => n + a) 0 x) + scoreOf xs

run : String -> IO ()
run s = do let lines = lines s
           Just (ns, lines) <- pure $ getNumbers lines
             | Nothing => putStrLn $ "err"
           let cards = parseCards lines
           Just (win, n) <- pure $ drawNumbers ns cards
             | Nothing => putStrLn $ "no win"
           let score = n * scoreOf win
           putStrLn $ show $ score

main : IO ()
main = do Right s <- readFile "input.txt"
            | Left err => putStrLn $ show err
          run s


text:
module Main

main : IO ()
main = putStrLn "Fuck You Github"

max_stars_repo_name: ozcanyarimdunya/FuckYouGithub

max_issues_repo_name: ozcanyarimdunya/FuckYouGithub

max_forks_repo_name: ozcanyarimdunya/FuckYouGithub


text:
import Data.String
import System

readNumber : IO (Maybe Nat)
readNumber =
    do numstr <- getLine
       pure (parsePositive numstr)

-- worst random number generator
rand : (min : Integer) -> (max : Integer) -> IO (Nat)
rand min max = do secs <- time
                  let n = (mod secs (max - min + 1)) + 1
                  pure (integerToNat n)

-- Guess the number game
guess : (target : Nat) -> (guesses : Nat) -> IO ()
guess target guesses =
               do putStrLn ("[Guess count: " ++ show guesses ++ "]")
                  putStrLn "Enter guess: "
                  Just num <- readNumber
                            | Nothing => do putStrLn "Invalid input"
                                            guess target guesses
                  case compare num target of
                       LT => do putStrLn "Too low."
                                guess target (guesses + 1)
                       EQ => putStrLn "Correct!"
                       GT => do putStrLn "Too high."
                                guess target (guesses + 1)

main : IO ()
main = do
        target <- rand 1 100
        guess target 0


text:
module Lines

import Data.Fin
import Data.Vect

import SizedStrings
import MaybeFin

%default total
%access public

data Lines : Vect k Nat -> Type where
  Nil : Lines []
  (::) : SizedString n -> Lines v -> Lines (n :: v)

%name Lines linez -- so as to avoid confusion with lines function

index : {v : Vect k Nat} -> (i : Fin k) -> Lines v -> SizedString (index i v)
index FZ (x :: xs) = x
index (FS y) (x :: xs) = index y xs

replaceAt : { size : Vect (S k) Nat } ->
           (i : Fin (S k)) ->
           SizedString (index i size) ->
           Lines size ->
           Lines size
replaceAt FZ     str (x::xs) = str :: xs
replaceAt (FS i) str (x::[]) = absurd i
replaceAt (FS i) str (x::(y :: z)) = x :: replaceAt i str (y :: z)

replaceAndResizeAt : { size : Vect (S k) Nat } ->
                     (i : Fin (S k)) ->
                     SizedString n ->
                     Lines size ->
                     Lines (replaceAt i n size)
replaceAndResizeAt FZ     str (x::xs) = str :: xs
replaceAndResizeAt (FS i) str (x::[]) = absurd i
replaceAndResizeAt (FS i) str (x::(y :: z)) = x :: replaceAndResizeAt i str (y :: z)

line_length_equals_size_from_type : {v : Vect k Nat} -> (i : Fin k) -> (ll : Lines v) ->
                                    length (index i ll) = index i v
line_length_equals_size_from_type FZ [] impossible
line_length_equals_size_from_type (FS _) [] impossible
line_length_equals_size_from_type FZ (_ :: _) = Refl
line_length_equals_size_from_type (FS _) (_ :: _) = Refl

vectSizeVector : Vect k String -> Vect k Nat
vectSizeVector = map length

readFromVect : (v : Vect k String) -> Lines (vectSizeVector v)
readFromVect [] = []
readFromVect (x :: xs) = sizeString x :: readFromVect xs

listSizeVector : (xs : List String) -> Vect (length xs) Nat
listSizeVector xs = vectSizeVector $ fromList xs

readFromList : (xs : List String) -> Lines (listSizeVector xs)
readFromList xs = readFromVect $ fromList xs

writeLinesToList : Lines v -> List String
writeLinesToList [] = []
writeLinesToList (l :: ls) = cast l :: writeLinesToList ls

deleteLine : {v : Vect (S k) Nat} -> (i : Fin (S k)) -> Lines v -> Lines (deleteAt i v)
deleteLine FZ (str :: strs) = strs
deleteLine {k = Z} (FS i) _ = absurd i
deleteLine {k = S j} (FS i) (str :: strs) = str :: deleteLine i strs

insertLine : {v : Vect k Nat} -> (i : Fin (S k)) -> (s: SizedString n) -> Lines v ->
             Lines (insertAt i n v)
insertLine FZ s ls = s :: ls
insertLine (FS y) s [] = absurd y
insertLine (FS y) s (str :: ls) = str :: insertLine y s ls

replaceChar : {size : Vect (S k) Nat} ->
              (row : Fin (S k)) ->
              (column : MaybeFin (index row size)) ->
              Char ->
              Lines size ->
              Lines size
replaceChar row column c linez =
  replaceAt row (maybeReplaceAt column c $ index row linez) linez

InsertAfterType : (size : Vect (S k) Nat) ->
                  (row : Fin (S k)) ->
                  Nat ->
                  Type
InsertAfterType size row textLength =
  Lines $ replaceAt row (index row size + textLength) size

insertAfter : {size : Vect (S k) Nat} ->
             (row : Fin (S k)) ->
             (column : MaybeFin (index row size)) ->
             SizedString l ->
             Lines size ->
             InsertAfterType size row l
insertAfter row column str linez =
  replaceAndResizeAt row (insertAfter (index row linez) column str) linez

InsertBeforeType : (size : Vect (S k) Nat) ->
                   (row : Fin (S k)) ->
                   Nat ->
                   Type
InsertBeforeType size row textLength =
  Lines $ replaceAt row (textLength + index row size) size

insertBefore : {size : Vect (S k) Nat} ->
             (row : Fin (S k)) ->
             (column : MaybeFin (index row size)) ->
             SizedString l ->
             Lines size ->
             InsertBeforeType size row l
insertBefore row column str linez =
  replaceAndResizeAt row (insertBefore (index row linez) column str) linez

DeleteCharType : (size : Vect (S k) Nat) ->
                 (row : Fin (S k)) ->
                 Type
DeleteCharType size row = Lines $ replaceAt row (Nat.pred $ index row size) size

deleteChar : {size : Vect (S k) Nat} ->
             (row : Fin (S k)) ->
             (column : MaybeFin (index row size)) ->
             Lines size ->
             DeleteCharType size row
deleteChar row column linez =
  replaceAndResizeAt row (deleteAt column $ index row linez) linez

charAt : {size : Vect (S k) Nat} ->
         (row : Fin (S k)) ->
         (column : MaybeFin (index row size)) ->
         Lines size ->
         Maybe Char
charAt row column linez =
  maybeStrIndex (index row linez) column


text:
module Test.Suite

import IdrTest.Test

import Test.SemVar.DataTest
import Test.SemVar.LexerTest
import Test.SemVar.ParserTest
import Test.SemVar.SatTest

suite : IO ()
suite = do
  runSuites
    [ Test.SemVar.LexerTest.suite
    , Test.SemVar.ParserTest.suite
    , Test.SemVar.DataTest.suite
    , Test.SemVar.SatTest.suite
    ]

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module TreesIt

import Control.Monad.Reader
import Control.Monad.State

import Data.List

import MonadTransUniv

record LeftToIterate a where
  constructor MkLeftToIterate
  leftToIterate : List a

record OriginalValues a where
  constructor MkOriginalValues
  originalValues : List a

nothingLeft : LeftToIterate a
nothingLeft = MkLeftToIterate empty

origToLeft : OriginalValues a -> LeftToIterate a
origToLeft = MkLeftToIterate . originalValues

%inline
Iterable'' : Type -> (Type -> Type) -> Type
Iterable'' a m = (MonadState (LeftToIterate a) m, MonadReader (OriginalValues a) m)

next'' : Iterable'' a m => m a
next'' = do
  gg <- get
  case leftToIterate gg of
    []      => asks origToLeft >>= put >> next''
    (x::xs) => put (MkLeftToIterate xs) $> x

%inline
ItT : Type -> (Type -> Type) -> Type -> Type
ItT s m = StateT (LeftToIterate s) (ReaderT (OriginalValues s) m)

runIterableT : Monad m => List s -> ItT s m a -> m a
runIterableT orig = runReaderT (MkOriginalValues orig) . evalStateT nothingLeft

namespace Compositions

  -- Ported from https://hackage.haskell.org/package/combinat-0.2.9.0/docs/src/Math.Combinat.Compositions.html
  -- Copyright of the original code: (c) 2008-2018 Balazs Komuves
  -- Original license is BSD-3-Clause.

  compositions' : List Nat -> Nat -> List $ List Nat
  compositions' []      0 = [[]]
  compositions' []      _ = []
  compositions' (s::ss) n =
    [ x::xs | x <- [0 .. min s n], xs <- compositions' ss (n `minus` x) ]

  compositions : Nat {-length-} -> Nat {-sum-} -> List $ List Nat
  compositions len d = compositions' (replicate len d) d where

  compositions1 : Nat {-len-} -> Nat {-sum-} -> List $ List Nat
  compositions1 len d = if len > d
    then []
    else map (+1) <$> compositions len (d `minus` len)

  export
  allCompositions1 : Nat -> List $ List $ List Nat
  allCompositions1 n = flip compositions1 n <$> [1..n]

namespace T

  public export
  data Tree = Leaf | Node (List Tree)

  export
  treesOfSize : Nat -> List Tree
  treesOfSize 0 = []
  treesOfSize 1 = [Leaf]
  treesOfSize (S n) = concatMap subtrees $ concat $ allCompositions1 n
    where
      combineLists : forall a. List (List a) -> List (List a)
      combineLists = sequence

      subtrees : List Nat -> List Tree
      subtrees = map Node . combineLists . map treesOfSize

data Tree a = Leaf a | Node (List $ Tree a)

Show a => Show (Tree a) where
  show (Leaf x) = "{" ++ show x ++ "}"
  show (Node ts) = "@(" ++ (concat $ map show ts) ++ ")"

decorateTree'' : Iterable'' a m => T.Tree -> m (Tree a)
decorateTree'' T.Leaf      = Leaf <$> next''
decorateTree'' (T.Node ts) = Node <$> traverse decorateTree'' ts

decoratedTreesIterator'' : Iterable'' a m => Iterable'' T.Tree m => Monad m => m (Tree a)
decoratedTreesIterator'' = next'' >>= decorateTree''

takeSome : Monad m => m a -> m $ List a
takeSome = sequence . replicate 6

decoratedTreesExample'' : List $ Tree Int
decoratedTreesExample'' =
  runIdentity $
    runIterableT {s=Int} [1..5] $
      runIterableT (T.treesOfSize 4) $
        takeSome $ decoratedTreesIterator''
          @{(State.Trans, Reader.Trans @{Reader.Trans})}

dtiMain : IO ()
dtiMain = traverse_ putStrLn $ map show decoratedTreesExample''

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Quantities.Units

import Quantities.Core
import Quantities.SIBaseQuantities
import Quantities.SIDerivedQuantities
import Quantities.SIBaseUnits

%default total
%access public export

Radian : Unit PlaneAngle
Radian = One
Rad : Unit PlaneAngle
Rad = One

Steradian : Unit SolidAngle
Steradian = One
Sr : Unit SolidAngle
Sr = Steradian

Hertz : Unit Frequency
Hertz = Second ^^ (-1)
Hz : Unit Frequency
Hz = Hertz

Newton : Unit Force'
Newton = ((Metre <//> Second) <//> Second) <**> Kilogram
N : Unit Force'
N = Newton

Pascal : Unit Pressure
Pascal = Newton <//> (Metre ^^ 2)
Pa : Unit Pressure
Pa = Pascal

Joule : Unit Energy
Joule = Newton <**> Metre
J : Unit Energy
J = Joule

Watt : Unit Power
Watt = Joule <//> Second
W : Unit Power
W = Watt

Coulomb : Unit ElectricCharge
Coulomb = Second <**> Ampere
C : Unit ElectricCharge
C = Coulomb

Volt : Unit ElectricPotentialDifference
Volt = Watt <//> Ampere
V : Unit ElectricPotentialDifference
V = Volt

Farad : Unit Capacitance
Farad = Coulomb <//> Volt
F : Unit Capacitance
F = Farad

Ohm : Unit ElectricResistance
Ohm = Volt <//> Ampere

Siemens : Unit ElectricConductance
Siemens = Ampere <//> Volt
S : Unit ElectricConductance
S = Siemens

Weber : Unit MagneticFlux
Weber = Second <**> Volt
Wb : Unit MagneticFlux
Wb = Weber

Tesla : Unit MagneticFluxDensity
Tesla = Weber <//> (Metre ^^ 2)
T : Unit MagneticFluxDensity
T = Tesla

Henry : Unit Inductance
Henry = Weber <//> Ampere
H : Unit Inductance
H = Henry

-- For relative temperature measurements
Celsius : Unit Temperature
Celsius = Kelvin
DC : Unit Temperature
DC = Celsius

Lumen : Unit LuminousFlux
Lumen = Candela <**> Steradian
Lm : Unit LuminousFlux
Lm = Lumen

Lux : Unit Illuminance
Lux = Lumen <//> (Metre ^^ 2)
Lx : Unit Illuminance
Lx = Lux

Becquerel : Unit ActivityReferredToARadionuclide
Becquerel = Second ^^ (-1)
Bq : Unit ActivityReferredToARadionuclide
Bq = Becquerel

Gray : Unit AbsorbedDose
Gray = Joule <//> Kilogram
Gy : Unit AbsorbedDose
Gy = Gray

Sievert : Unit DoseEquivalent
Sievert = Joule <//> Kilogram
Sv : Unit DoseEquivalent
Sv = Sievert

Katal : Unit CatalyticActivity
Katal = Mol <//> Second
Kat : Unit CatalyticActivity
Kat = Katal

max_stars_repo_name: timjb/quantities

max_issues_repo_name: timjb/quantities

max_forks_repo_name: timjb/quantities


text:
{-
null
not null
-}

import CIL.FFI

putNullableStrLn : Nullable String -> IO ()
putNullableStrLn =
  putStrLn . nullable "null" id

main : IO ()
main = do
  putNullableStrLn null
  putNullableStrLn (asNullable "not null")

-- Local Variables:
-- idris-load-packages: ("cil")
-- End:

max_stars_repo_name: timjs/iris-clean

max_issues_repo_name: timjs/iris-clean

max_forks_repo_name: timjs/iris-clean


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

import public UML.Code.Model
import public UML.Code.Parser
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-uml

max_issues_repo_name: jfdm/idris-uml

max_forks_repo_name: jfdm/idris-uml


text:
record Person (age : Nat) where
  constructor MkPerson
  name : String

record Event where
  constructor MkEvent
  name : String
  organiser : Person a

record Meeting (year : Int) where
  constructor MkMeeting
  event : Event
  organiser : Person a

new_organiser : String -> List (Meeting x) -> List (Meeting x)
new_organiser n = map (record { event->organiser->name = n })

next_year : Meeting x -> Meeting (x+1)
next_year m = record { organiser->param_age
                          = record { organiser->param_age } m + 1,
                       event->organiser->param_age
                          = record { event->organiser->param_age } m + 1,
                       param_year = _ } m

fred : Person 20
fred = MkPerson "Fred"

jim : Person 29
jim = MkPerson {age=29} "Jim"

idm : Event
idm = MkEvent "Idris Developers Meeting" fred

idm_gbg : Meeting 2014
idm_gbg = MkMeeting idm jim

test : Meeting 2015
test = next_year idm_gbg

main : IO ()
main = do printLn (record { event->organiser->name } test)
          printLn (record { event->organiser->param_age } test)
          printLn (record { event->organiser->param_age } idm_gbg)
          printLn (record { organiser->param_age } test)
          printLn (record { organiser->param_age } idm_gbg)
          printLn (record { param_year } idm_gbg)

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:
import Providers
import Data.HVect
import Data.Fin

%default total
%language TypeProviders

-- Playing with reasoning about black boxes here. The goal is not to
-- reconstruct their algorithms (which won't be possible in many
-- cases), but to experiment, make statements about their behaviour,
-- confirm or refute those, and reason using those statements as
-- premises.

-- Confirmations are commented out, because they take a bit too much
-- time and memory to typecheck, but they are fine

-- Not using Dec here, mostly because of laziness, but in some cases
-- it might be much more convenient. Also would be nice to add type
-- aliases for common things.

postulate blackbox : (Bool, Nat, Nat) -> Nat

-- there should be a nicer way to do this, without an additonal type
data MTL : Nat -> Type where
  Nil : MTL Z
  (::) : {ib:Bool} -> {in1, in2, out: Nat} -> (t:Type) ->
       {auto eq: t = (blackbox (ib, in1, in2) = out)} -> {n: Nat} -> MTL n -> MTL (S n)

(++) : MTL m -> MTL n -> MTL (m + n)
(++) [] ys = ys
(++) ((::) x {eq} xs) ys = (::) x {eq} $ xs ++ ys

index : Fin n -> MTL n -> Type
index FZ     (x::xs) = x
index (FS k) (x::xs) = index k xs
index FZ     [] impossible

-- simply turns (f: bb -> Type) into ((x:bb) -> f x)
h : ({ib: Bool} -> {in1, in2, o: Nat} -> blackbox (ib, in1, in2) = o -> Type) -> Type
h f = {ib: Bool} -> {in1, in2, o: Nat} -> (x:(blackbox (ib, in1, in2) = o)) -> f x

-- applies a model to an observation
mt : {ib:Bool} -> {in1, in2, out: Nat} ->
   ({ib: Bool} -> {in1, in2, o: Nat} -> (blackbox (ib, in1, in2) = o) -> Type) ->
   (t:Type) -> {auto eq: t = (blackbox (ib, in1, in2) = out)} -> Type
mt {ib} {in1} {in2} {out} f t = (x:(blackbox (ib, in1, in2) = out)) -> f x

-- same, but for a bunch of observations
confirm : ({ib: Bool} -> {in1, in2, o: Nat} -> (blackbox (ib, in1, in2) = o) -> Type) -> MTL n -> Vect n Type
confirm f [] = []
confirm f ((::) x xs {eq}) = mt f x {eq} :: confirm f xs

-- only one kind of experiment here, in two versions: for single and
-- multiple tests
experiment : (Bool, Nat, Nat) -> IO (Provider Type)
experiment inp@(o, a1, a2) = do
  out <- return $ if o then a1 + a2 else (if lte a2 a1 then a1 - a2 else a1 * a2)
  return (Provide (blackbox inp = out))

experiment' : Vect n (Bool, Nat, Nat) -> IO (MTL n)
experiment' [] = return []
experiment' (inp@(o, a1, a2)::xs) = do
  out <- return $ if o then a1 + a2 else (if lte a2 a1 then a1 - a2 else a1 * a2)
  next <- experiment' xs
  return $ (blackbox inp = out) :: next

experimentV : Vect n (Bool, Nat, Nat) -> IO (Provider (MTL n))
experimentV v = do
  types <- experiment' v
  return (Provide types)

-- beginning to poke the box
%provide (initialTests : MTL 8) with (experimentV [
         (True, 0, 0),  -- 0
         (True, 0, 1),  -- 1
         (True, 1, 0),  -- 1
         (True, 1, 1),  -- 2
         (False, 0, 0), -- 0
         (False, 0, 1), -- 0
         (False, 1, 0), -- 1
         (False, 1, 1)  -- 0
         ])

-- the first guess
tPlusFMinus : {ib: Bool} -> {in1, in2, o: Nat} -> (blackbox (ib, in1, in2) = o) -> Type
tPlusFMinus {ib} {in1} {in2} {o} ob = if ib then o = in1 + in2 else o = in1 - in2

-- confirmTPlusFMinus : HVect (confirm tPlusFMinus initialTests)
-- confirmTPlusFMinus = [\x => Refl, \x => Refl, \x => Refl, \x => Refl, \x => Refl, \x => Refl, \x => Refl, \x => Refl]

%provide (furtherTests : MTL 4) with (experimentV [
         (True, 42, 23),  -- 65
         (True, 23, 42),  -- 65
         (False, 42, 23), -- 19
         (False, 23, 42)  -- 966
         ])

-- confirmTPlusFMinus2 : HVect (confirm tPlusFMinus furtherTests)
-- confirmTPlusFMinus2 = ?mv -- uh oh, 966 = 0!

refuteTPlusFMinus2 : index 3 furtherTests -> HVect (confirm tPlusFMinus furtherTests) -> Void
refuteTPlusFMinus2 f [_,_,_,d] = uninhabited (sym (d f))

-- is it multiplication? why it happened?

%provide (moreTests : MTL 4) with (experimentV [
         (False, 3, 5),  -- 15
         (False, 5, 3),  -- 2
         (False, 7, 13), -- 91
         (False, 13, 7)  -- 6
         ])

-- ok, it happens when the first Nat is lower

tPlusFMinusMult : {ib: Bool} -> {in1, in2, o: Nat} -> (blackbox (ib, in1, in2) = o) -> Type
tPlusFMinusMult {ib} {in1} {in2} {o} ob =
  o = if ib then in1 + in2 else (if lte in2 in1 then in1 - in2 else in1 * in2)

-- confirmTPlusFMinusMult : HVect (confirm tPlusFMinusMult $ initialTests ++ furtherTests ++ moreTests)
-- confirmTPlusFMinusMult = confirmTPlusFMinus ++ [\x => Refl, \x => Refl, \x => Refl, \x => Refl, \x => Refl, \x => Refl, \x => Refl, \x => Refl]

-- now we could reason using this model

tCommutative : {in1, in2, o1, o2: Nat} ->
             -- for any two black box runs with their Nat arguments swapped, and Bool arg = True…
             (blackbox (True, in1, in2) = o1) -> (blackbox (True, in2, in1) = o2) ->
             -- according to tPlusFMinusMult…
             (h tPlusFMinusMult) ->
             -- outputs are equal
             o1 = o2
tCommutative {in1} {in2} {o1} {o2} b1 b2 f with (f b1, f b2)
  | (r1, r2) = rewrite r1 in rewrite r2 in plusCommutative in1 in2

max_stars_repo_name: defanor/black-box-reasoning

max_issues_repo_name: defanor/black-box-reasoning

max_forks_repo_name: defanor/black-box-reasoning


text:
module Erlang.Data.IOArray

import Data.List
import Erlang
import Erlang.Data.IORef

%default total

data ArrayData : Type -> Type where
  MkArrayData : IORef ErlTerm -> ArrayData a

-- 'unsafe' primitive access, backend dependent
-- get and set assume that the bounds have been checked. Behavious is undefined
-- otherwise.

prim__newArray : HasIO io => Int -> a -> io (ArrayData a)
prim__newArray size value = do
  arr <- pure $ erlUnsafeCall ErlTerm "array" "new" [size, MkTuple2 (MkAtom "default") (MkRaw value)]
  ref <- newIORef arr
  pure (MkArrayData ref)

prim__arrayGet : HasIO io => ArrayData a -> Int -> io a
prim__arrayGet (MkArrayData ref) pos = do
  arr <- readIORef ref
  MkRaw value <- pure $ erlUnsafeCall (Raw a) "array" "get" [pos, arr]
  pure value

prim__arraySet : HasIO io => ArrayData a -> Int -> a -> io ()
prim__arraySet (MkArrayData ref) pos value = do
  arr <- readIORef ref
  newArr <- pure $ erlUnsafeCall ErlTerm "array" "set" [pos, MkRaw value, arr]
  writeIORef ref newArr

export
record IOArray elem where
  constructor MkIOArray
  maxSize : Int
  content : ArrayData (Maybe elem)

export
max : IOArray elem -> Int
max = maxSize

export
newArray : Int -> IO (IOArray elem)
newArray size
    = pure (MkIOArray size !(prim__newArray size Nothing))

export
writeArray : IOArray elem -> Int -> elem -> IO ()
writeArray arr pos el
    = if pos < 0 || pos >= max arr
         then pure ()
         else prim__arraySet (content arr) pos (Just el)

export
readArray : IOArray elem -> Int -> IO (Maybe elem)
readArray arr pos
    = if pos < 0 || pos >= max arr
         then pure Nothing
         else prim__arrayGet (content arr) pos

-- Make a new array of the given size with the elements copied from the
-- other array
export
newArrayCopy : (newsize : Int) -> IOArray elem -> IO (IOArray elem)
newArrayCopy newsize arr
    = do let newsize' = if newsize < max arr then max arr else newsize
         arr' <- newArray newsize'
         copyFrom (content arr) (content arr') (max arr - 1)
         pure arr'
  where
    copyFrom : ArrayData (Maybe elem) ->
               ArrayData (Maybe elem) ->
               Int -> IO ()
    copyFrom old new pos
        = if pos < 0
             then pure ()
             else do el <- prim__arrayGet old pos
                     prim__arraySet new pos el
                     assert_total (copyFrom old new (pos - 1))

export
toList : IOArray elem -> IO (List (Maybe elem))
toList arr = iter 0 (max arr) []
  where
    iter : Int -> Int -> List (Maybe elem) -> IO (List (Maybe elem))
    iter pos end acc
         = if pos >= end
              then pure (reverse acc)
              else do el <- readArray arr pos
                      assert_total (iter (pos + 1) end (el :: acc))

export
fromList : List (Maybe elem) -> IO (IOArray elem)
fromList ns
    = do arr <- newArray (cast (length ns))
         addToArray 0 ns arr
         pure arr
  where
    addToArray : Int -> List (Maybe elem) -> IOArray elem -> IO ()
    addToArray loc [] arr = pure ()
    addToArray loc (Nothing :: ns) arr
        = assert_total (addToArray (loc + 1) ns arr)
    addToArray loc (Just el :: ns) arr
        = do prim__arraySet (content arr) loc (Just el)
             assert_total (addToArray (loc + 1) ns arr)


text:
module GRIN.ANFToGRIN

import Libraries.Data.IntMap
import Data.SortedMap
import Data.SortedSet
import Data.Nat
import Data.Vect

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

import Compiler.ANF

import GRIN.AST
import GRIN.Data
import GRIN.PrimOps

%default total

fetchAVar :
    Ref AVars AVarMap =>
    Ref Ptrs PtrSet =>
    AVar ->
    Core (SExp GName)
fetchAVar (ALocal i) = do
    avs <- get AVars
    ptrs <- get Ptrs
    case lookup i avs of
        Nothing => throw $ InternalError "Undefined AVar."
        Just v => if contains v ptrs
            then pure $ Fetch Nothing v
            else pure $ Pure $ VVar v
fetchAVar ANull = pure $ Pure nullVal

storeAVar :
    Ref AVars AVarMap =>
    Ref Ptrs PtrSet =>
    AVar ->
    Core (SExp GName)
storeAVar (ALocal i) = do
    avs <- get AVars
    ptrs <- get Ptrs
    case lookup i avs of
        Nothing => throw $ InternalError "Undefined AVar."
        Just v => if contains v ptrs
            then pure $ Pure $ VVar v
            else pure $ Store $ VVar v
storeAVar ANull = pure $ Store nullVal

newAVar :
    Ref NextVar Var =>
    Ref AVars AVarMap =>
    AVar ->
    Core Var
newAVar (ALocal av) = do
    avs <- get AVars
    case lookup av avs of
        Nothing => do
            v <- newVar
            put AVars (insert av v avs)
            pure v
        Just _ => throw $ InternalError "Already defined AVar."
newAVar ANull = throw $ InternalError "Attempt to generate a new Var for ANull."

setVarPtr :
    Ref Ptrs PtrSet =>
    Var -> Core Var
setVarPtr v = do
    update Ptrs $ insert v
    pure v

storeAVars :
    Ref AVars AVarMap =>
    Ref Ptrs PtrSet =>
    Ref NextVar Var =>
    List AVar ->
    (List Var -> Core (Exp GName)) ->
    Core (Exp GName)
storeAVars [] k = k []
storeAVars (av :: avs) k = do
    v <- newVar
    pure $ Bind (VVar v) !(storeAVar av) !(storeAVars avs (k . (v ::)))

storeAVarsVect :
    Ref AVars AVarMap =>
    Ref Ptrs PtrSet =>
    Ref NextVar Var =>
    Vect k AVar ->
    (Vect k Var -> Core (Exp GName)) ->
    Core (Exp GName)
storeAVarsVect [] k = k []
storeAVarsVect (av :: avs) k = do
    v <- newVar
    pure $ Bind (VVar v) !(storeAVar av) !(storeAVarsVect avs (k . (v ::)))

fetchAVarsVect :
    Ref AVars AVarMap =>
    Ref Ptrs PtrSet =>
    Ref NextVar Var =>
    Vect k AVar ->
    (Vect k Var -> Core (Exp GName)) ->
    Core (Exp GName)
fetchAVarsVect [] k = k []
fetchAVarsVect (av :: avs) k = do
    v <- newVar
    pure $ Bind (VVar v) !(fetchAVar av) !(fetchAVarsVect avs (k . (v ::)))

apply : Var -> Var -> SExp GName
apply clos arg = App (GrinName Apply) [clos, arg]

appU : Var -> Var -> SExp GName
appU clos arg = App (GrinName ApplyU) [clos, arg]

appNU : Var -> Var -> SExp GName
appNU clos arg = App (GrinName ApplyNU) [clos, arg]

appLazy : LazyReason -> Var -> Var -> SExp GName
appLazy LInf = appU
appLazy _ = appNU

mkLazyThunk : LazyReason -> name -> List SVal -> Val name
mkLazyThunk LInf = mkNUThunk
mkLazyThunk _ = mkUThunk

anfToExp :
    Ref AVars AVarMap =>
    Ref Ptrs PtrSet =>
    Ref NextVar Var =>
    ANF ->
    Core (Exp GName)

anfConAlts :
    Ref AVars AVarMap =>
    Ref Ptrs PtrSet =>
    Ref NextVar Var =>
    List AConAlt ->
    Maybe ANF ->
    Core (List (Alt GName))

anfConstAlts :
    Ref AVars AVarMap =>
    Ref Ptrs PtrSet =>
    Ref NextVar Var =>
    List AConstAlt ->
    Maybe ANF ->
    Core (List (Alt GName))

anfToExp (AV _ v) = mkSimpleExp <$> fetchAVar v

anfToExp (AAppName _ Nothing fn args) =
    storeAVars args $ \vs => pure $ mkSimpleExp
        $ App (IdrName fn) vs
anfToExp (AAppName _ (Just LInf) fn args) =
    storeAVars args $ \vs => pure $ mkSimpleExp
        $ Pure $ mkNUThunk (IdrName fn) (SVar <$> vs)
anfToExp (AAppName _ (Just _) fn args) =
    storeAVars args $ \vs => pure $ mkSimpleExp
        $ Pure $ mkNUThunk (IdrName fn) (SVar <$> vs)

anfToExp (AUnderApp _ fn m args) =
    storeAVars args $ \vs => pure $ mkSimpleExp
        $ Pure $ mkPartial (IdrName fn) m (SVar <$> vs)

anfToExp (AApp _ Nothing fn arg) =
    storeAVarsVect [fn, arg] $ \[fnv, argv] => pure $ mkSimpleExp $ apply fnv argv
anfToExp (AApp _ (Just lazy) fn arg) =
    storeAVarsVect [fn, arg] $ \[fnv, argv] => pure $ mkSimpleExp $ appLazy lazy fnv argv

anfToExp (ALet _ av rhs rest) = do
    v <- newAVar (ALocal av)
    pure $ Bind (VVar v) (mkDo !(anfToExp rhs)) !(anfToExp rest)

anfToExp (ACon _ con _ _ args) =
    storeAVars args $ \vs => pure $ mkSimpleExp
        $ Pure $ mkCon (IdrName con) (SVar <$> vs)

anfToExp (AOp _ Nothing op args) =
    storeAVarsVect args $ \vs => pure $ mkSimpleExp
        $ App (PrimName op) (toList vs)
anfToExp (AOp _ (Just lazy) op args) =
    fetchAVarsVect args $ \vs => pure $ mkSimpleExp
        $ Pure $ mkLazyThunk lazy (PrimName op) (SVar <$> toList vs)

anfToExp (AExtPrim fc lazy fn args) = assert_total $ anfToExp (AAppName fc lazy fn args)

anfToExp (AConCase _ av alts def) = do
    vp <- newVar
    v <- newVar
    pure $ Bind (VVar vp) !(storeAVar av)
         $ Bind (VVar v) (App (GrinName Eval) [vp])
         $ Case (VVar v) !(anfConAlts alts def)

anfToExp (AConstCase _ av alts@(MkAConstAlt c _ :: _) def) = do
    vp <- newVar
    v <- newVar
    pure $ Bind (VVar vp) !(storeAVar av)
         $ Bind (unwrapConstant v c) (App (GrinName Eval) [vp])
         $ Case (VVar v) !(anfConstAlts alts def)

anfToExp (AConstCase _ av alts def) = do
    vp <- newVar
    v <- newVar
    pure $ Bind (VVar vp) !(storeAVar av)
         $ Bind (VVar v) (App (GrinName Eval) [vp])
         $ Case (VVar v) !(anfConstAlts alts def)

anfToExp (APrimVal _ (BI x)) = do
    v <- newVar
    pure $ Bind (VVar v) (Pure $ VLit $ LString $ show x)
         $ SimpleExp (App (PrimFunc $ Cast StringType IntegerType) [v])
anfToExp (APrimVal _ c) = pure $ mkSimpleExp $ Pure $ anfConstant c

anfToExp (AErased _) = pure $ mkSimpleExp $ Pure nullVal

anfToExp (ACrash _ msg) = do
    v <- newVar
    pure $ Bind (VVar v) (Pure $ VLit $ LString msg)
         $ SimpleExp $ App (GrinName Crash) [v]

anfConAlt :
    Ref AVars AVarMap =>
    Ref Ptrs PtrSet =>
    Ref NextVar Var =>
    AConAlt ->
    Core (Alt GName)
anfConAlt (MkAConAlt con _ _ avs exp) = do
    as <- traverse (newAVar . ALocal >=> setVarPtr) avs
    MkAlt (NodePat (MkTag Con $ IdrName con) as) <$> anfToExp exp

anfConAlts (alt :: alts) def = [| anfConAlt alt :: anfConAlts alts def |]
anfConAlts [] (Just exp) = pure . MkAlt DefaultPat <$> anfToExp exp
anfConAlts [] Nothing = pure []

anfConstAlt :
    Ref AVars AVarMap =>
    Ref Ptrs PtrSet =>
    Ref NextVar Var =>
    AConstAlt ->
    Core (Alt GName)
anfConstAlt (MkAConstAlt lit exp) =
    pure $ MkAlt (getConstantLitPat lit) !(anfToExp exp)

anfConstAlts (alt :: alts) def = [| anfConstAlt alt :: anfConstAlts alts def |]
anfConstAlts [] (Just exp) = pure . MkAlt DefaultPat <$> anfToExp exp
anfConstAlts [] Nothing = pure []

record BProg where
    constructor MkBProg
    eval : Var -> Core (List (Alt GName))
    apply : Var -> List (Alt GName)
    applyU : Var -> List (Alt GName)
    applyNU : Var -> List (Alt GName)
    defs : List (Def GName)
    externs : List (Extern GName)

initBProg : Ref NextVar Var => Core BProg
initBProg = pure $ MkBProg primCons go go go !primOps externs
  where
    go : _ -> List a
    go _ = []

addEvalAlt :
    Ref Build BProg =>
    (Var -> Core (Alt GName)) ->
    Core ()
addEvalAlt alt = update Build $ record { eval $= \ev, ptr => (::) <$> alt ptr `Core.(<*>)` ev ptr }

addEvalAlts :
    Ref Build BProg =>
    (Var -> Core (List (Alt GName))) ->
    Core ()
addEvalAlts alts = update Build $ record { eval $= \ev, ptr => (++) <$> alts ptr `Core.(<*>)` ev ptr }

addApplyAlt :
    Ref Build BProg =>
    ((arg : Var) -> Alt GName) ->
    Core ()
addApplyAlt alt = update Build $ record { apply $= \app, arg => alt arg :: app arg }

addApplyUAlt :
    Ref Build BProg =>
    ((arg : Var) -> Alt GName) ->
    Core ()
addApplyUAlt alt = update Build $ record { applyU $= \app, arg => alt arg :: app arg }

addApplyNUAlt :
    Ref Build BProg =>
    ((arg : Var) -> Alt GName) ->
    Core ()
addApplyNUAlt alt = update Build $ record { applyNU $= \app, arg => alt arg :: app arg }

addDef :
    Ref Build BProg =>
    Def GName ->
    Core ()
addDef def = update Build $ record { defs $= (def ::) }

addExtern :
    Ref Build BProg =>
    Extern GName ->
    Core ()
addExtern ext = update Build $ record { externs $= (ext ::) }

addFnEval :
    Ref NextVar Var =>
    Ref Build BProg =>
    GName -> Nat -> Core ()
addFnEval fn arity = do
    let uAlt = \ptr => do
            vs <- replicate arity newVar
            res <- newVar
            pure $ MkAlt (NodePat (MkTag UThunk fn) vs)
                 $ Bind (VVar res) (App fn vs)
                 $ Bind VUnit (Update ptr (VVar res))
                 $ SimpleExp $ Pure (VVar res)
    addEvalAlt uAlt
    let nuAlt = \_ => do
            vs <- replicate arity newVar
            pure $ MkAlt (NodePat (MkTag NUThunk fn) vs)
                 $ SimpleExp $ App fn vs
    addEvalAlt nuAlt
    let S ar = arity
        | Z => pure ()
    let pAlts = \_ =>
            traverse addMissing [(ar + 1) .. 1]
    addEvalAlts pAlts
  where
    addMissing : Nat -> Core (Alt GName)
    addMissing missing = do
        vs <- replicate (arity `minus` missing) newVar
        let tag = MkTag (Partial missing) fn
        pure $ MkAlt (NodePat tag vs)
             $ SimpleExp $ Pure $ ConstTagNode tag (SVar <$> vs)

addFnApply :
    Ref NextVar Var =>
    Ref Build BProg =>
    GName -> Nat -> Nat -> Core ()
addFnApply fn _ 0 = pure ()
addFnApply fn ar 1 = do
    vs <- replicate (ar `minus` 1) newVar
    let alt = \arg =>
            MkAlt (NodePat (MkTag (Partial 1) fn) vs)
                $ SimpleExp $ App fn (vs ++ [arg])
    addApplyAlt alt
    vs <- replicate (ar `minus` 1) newVar
    let altU = \arg =>
            MkAlt (NodePat (MkTag (Partial 1) fn) vs)
                $ SimpleExp $ Pure
                    $ ConstTagNode (MkTag UThunk fn) (SVar <$> vs ++ [arg])
    addApplyUAlt altU
    vs <- replicate (ar `minus` 1) newVar
    let altNU = \arg =>
            MkAlt (NodePat (MkTag (Partial 1) fn) vs)
                $ SimpleExp $ Pure
                    $ ConstTagNode (MkTag NUThunk fn) (SVar <$> vs ++ [arg])
    addApplyNUAlt altNU

addFnApply fn ar mis = do
    vs <- replicate (ar `minus` mis) newVar
    let alt = \arg =>
            MkAlt (NodePat (MkTag (Partial mis) fn) vs)
                $ SimpleExp $ Pure
                    $ ConstTagNode (MkTag (Partial $ pred mis) fn) (SVar <$> vs ++ [arg])
    addApplyAlt alt
    vs <- replicate (ar `minus` mis) newVar
    let altU = \arg =>
            MkAlt (NodePat (MkTag (Partial mis) fn) vs)
                $ SimpleExp $ Pure
                    $ ConstTagNode (MkTag (Partial $ pred mis) fn) (SVar <$> vs ++ [arg])
    addApplyUAlt altU
    vs <- replicate (ar `minus` mis) newVar
    let altNU = \arg =>
            MkAlt (NodePat (MkTag (Partial mis) fn) vs)
                $ SimpleExp $ Pure
                    $ ConstTagNode (MkTag (Partial $ pred mis) fn) (SVar <$> vs ++ [arg])
    addApplyNUAlt altNU
    assert_total $ addFnApply fn ar (pred mis)

anfDef :
    Ref NextVar Var =>
    Ref Build BProg =>
    Name -> ANFDef ->
    Core ()

anfDef fn (MkAFun avs exp) = do
    avars <- newRef AVars empty
    ptrs <- newRef Ptrs empty
    vs <- traverse ((newAVar . ALocal) >=> setVarPtr) avs
    addFnEval (IdrName fn) (length avs)
    addFnApply (IdrName fn) (length avs) (length avs)
    addDef !(mkDef (IdrName fn) vs <$> anfToExp exp)

anfDef con (MkACon _ ar _) =
    addEvalAlt $ \_ => do
        vs <- replicate ar newVar
        let tag = (MkTag Con (IdrName con))
        pure $ MkAlt (NodePat tag vs) (mkSimpleExp $ Pure $ ConstTagNode tag (SVar <$> vs))

anfDef fn (MkAForeign ccs args ret) = do
    let Just primFn = getCC ccs
        | Nothing => throw $ InternalError $ "No supported calling conventions."
    let Right type = getFFIType args ret
        | Left err => throw $ InternalError $ "Unsupported ffi type " ++ err ++ "."
    let prim = FFI
    let eff = isEff ret
    addExtern $ MkExtern { extName = FFIName primFn, type, prim, eff }
    wrap <- mkFFIWrapper (IdrName fn) args ret (FFIName primFn)
    addDef wrap

anfDef fn e@(MkAError exp) = anfDef fn (assert_smaller e $ MkAFun [] exp)

mkEvalFn :
    Ref NextVar Var =>
    (Var -> Core (List (Alt GName))) ->
    Core (Def GName)
mkEvalFn k = do
    ptr <- newVar
    val <- newVar
    alts <- k ptr
    pure $ mkDef (GrinName Eval) [ptr]
         $ Bind (VVar val) (fetch ptr)
         $ Case (VVar val) alts

mkApplyFn :
    Ref NextVar Var =>
    GrinFn ->
    ((arg : Var) -> List (Alt GName)) ->
    Core (Def GName)
mkApplyFn fn k = do
    fnPtr <- newVar
    fnVal <- newVar
    arg <- newVar
    let alts = k arg
    pure $ mkDef (GrinName fn) [fnPtr, arg]
         $ Bind (VVar fnVal) (App (GrinName Eval) [fnPtr])
         $ Case (VVar fnVal) alts

export
compileANF : List (Name, ANFDef) -> Core (Prog GName)
compileANF defs = do
    var <- newRef NextVar (MkVar 0)
    build <- newRef Build !initBProg
    traverse_ (uncurry anfDef) defs

    MkBProg eval apply applyU applyNU defs externs <- get Build

    evalFn <- mkEvalFn eval
    applyFn <- mkApplyFn Apply apply
    applyUFn <- mkApplyFn ApplyU applyU
    applyNUFn <- mkApplyFn ApplyNU applyNU

    let main =
        mkDef
            (GrinName Main)
            []
            $ mkSimpleExp
                $ App (IdrName $ MN "__mainExpression" 0) []

    pure $ mkProg externs (main :: evalFn :: applyFn :: applyUFn :: applyNUFn :: defs) (GrinName Main)


text:
test : Not (Nat = String)
test eq impossible

test2 : Not (Char = String)
test2 eq impossible

test3 : Not (Type = String)
test3 eq impossible

test4 : Not (Type = Nat)
test4 eq impossible

test5 : Not (List Nat = Type)
test5 eq impossible

test6 : Not (Bits64 = Type)
test6 eq impossible

test7 : Not ('a' = 'b')
test7 eq impossible

-- The following ones are actually possible

test8 : Not (a = Type)
test8 eq impossible

test9 : Not (a = 'a')
test9 eq impossible

test10 : Not (a = Nat)
test10 eq impossible

test11 : Not (3 = a)
test11 eq impossible


text:
module Edsl
import Data.Vect
import Data.Fin

data Ty = TyInt | TyBool | TyFun Ty Ty
interpTy : Ty -> Type
interpTy TyInt       = Int
interpTy TyBool      = Bool
interpTy (TyFun a t) = interpTy a -> interpTy t

using (G:Vect n Ty)
  data HasType : Fin n -> Vect n Ty -> Ty -> Type where
    Stop : HasType FZ (t :: G) t
    Pop  : HasType k G t -> HasType (FS k) (u :: G) t

  data Expr : Vect n Ty -> Ty -> Type where
    Var : HasType i G t -> Expr G t
    Val : (x : Int) -> Expr G TyInt
    Lam : Expr (a :: G) t -> Expr G (TyFun a t)
    App : Expr G (TyFun a t) -> Expr G a -> Expr G t
    Op  : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b -> Expr G c
    If  : Expr G TyBool -> Lazy (Expr G a) -> Lazy (Expr G a) -> Expr G a

  data Env : Vect n Ty -> Type where
    Nil  : Env Nil
    (::) : interpTy a -> Env G -> Env (a :: G)

  interp : Env G -> Expr G t -> interpTy t
  interp env (Var i)     =  ?sdf2
  interp env (Val x)     = x
  interp env (Lam body)  = \x => interp (x :: env) body
  interp env (App f s)   = (interp env f) (interp env s)
  interp env (Op op x y) = op (interp env x) (interp env y)
  interp env (If x t e)  = if interp env x then interp env t else interp env e

max_stars_repo_name: idris-industry/paradise

max_issues_repo_name: idris-industry/paradise

max_forks_repo_name: idris-industry/paradise


text:
> module NonNegRational.BasicProperties

> import Syntax.PreorderReasoning

> import NonNegRational.NonNegRational
> import NonNegRational.BasicOperations
> import Fraction.Fraction
> import Fraction.BasicOperations
> import Fraction.Predicates
> import Fraction.BasicProperties
> import Fraction.Normalize
> import Fraction.NormalizeProperties
> import Fraction.EqProperties
> import Fraction.Normal
> import Subset.Properties
> import Unique.Predicates
> import Unique.Properties
> import Nat.Positive
> import Nat.Coprime -- used by the implementation of |not1Eq0|!
> import Nat.GCDAlgorithm -- used by the implementation of |not1Eq0|!
> import Num.Refinements
> import Pairs.Operations
> import PNat.PNat
> import PNat.Operations
> import PNat.Properties
> import Basic.Operations

> %default total
> -- %access export
> %access public export

* Properties of |toFraction|:

> ||| toFraction is injective
> toFractionInjective : {x, y : NonNegRational} -> (toFraction x) = (toFraction y) -> x = y
> toFractionInjective {x} {y} p = subsetEqLemma1 x y p NormalUnique

> ||| toFraction preserves equality
> toFractionEqLemma2 : {x, y : NonNegRational} -> x = y -> (toFraction x) = (toFraction y)
> toFractionEqLemma2 {x} {y} p = getWitnessPreservesEq p

* Properties of |fromFraction| and |toFraction|:

> ||| fromFraction is left inverse of toFraction
> fromToId : (x : NonNegRational) -> fromFraction (toFraction x) = x
> fromToId (Element x nx) = ( fromFraction (toFraction (Element x nx)) )
>                         ={ Refl }=
>                           ( fromFraction x )
>                         ={ Refl }=
>                           ( Element (normalize x) (normalNormalize x) )
>                         ={ toFractionInjective (normalizePreservesNormal x nx) }=
>                           ( Element x nx )
>                         QED

> ||| Equivalence of fractions implies equality of non-negative rationals
> fromFractionEqLemma : (x, y : Fraction) -> x `Eq` y -> fromFraction x = fromFraction y
> fromFractionEqLemma x y xEqy = s7 where
>   s1 : normalize x = normalize y
>   s1 = normalizeEqLemma2 x y xEqy
>   s2 : Normal (normalize x) = Normal (normalize y)
>   s2 = cong s1
>   s3 : Normal (normalize x)
>   s3 = normalNormalize x
>   s4 : Normal (normalize y)
>   s4 = normalNormalize y
>   s5 : s3 = s4
>   s5 = uniqueLemma (\ f => NormalUnique {x = f}) (normalize x) (normalize y) s3 s4 s1
>   s6 : Element (normalize x) (normalNormalize x) = Element (normalize y) (normalNormalize y)
>   s6 = depCong2 {alpha = Fraction}
>                 {P = Normal}
>                 {gamma = Subset Fraction Normal}
>                 {a1 = normalize x}
>                 {a2 = normalize y}
>                 {Pa1 = normalNormalize x}
>                 {Pa2 = normalNormalize y}
>                 {f = \ ZUZU => \ ZAZA => Element ZUZU ZAZA} s1 s5
>   s7 : fromFraction x = fromFraction y
>   s7 = s6

> ||| Denominators of non-negative rationals are greater than zero
> denLTLemma : (x : NonNegRational) -> Z `LT` den x
> denLTLemma x = s2 where
>   s1 : Z `LT` den (toFraction x)
>   s1 = Fraction.BasicProperties.denLTLemma (toFraction x)
>   s2 : Z `LT` den x
>   s2 = replace {P = \ ZUZU => Z `LT` ZUZU} Refl s1

> |||
> toFractionFromNatLemma : (n : Nat) -> toFraction (fromNat n) = fromNat n
> toFractionFromNatLemma n =
>     ( toFraction (fromNat n) )
>   ={ Refl }=
>     ( toFraction (fromFraction (fromNat n)) )
>   ={ Refl }=
>     ( toFraction (fromFraction (n, Element (S Z) MkPositive)) )
>   ={ Refl }=
>     ( toFraction (Element (normalize (n, Element (S Z) MkPositive)) (normalNormalize (n, Element (S Z) MkPositive))) )
>   ={ cong (toFractionInjective (normalizePreservesNormal (n, Element (S Z) MkPositive) fromNatNormal)) }=
>     ( toFraction (Element (n, Element (S Z) MkPositive) fromNatNormal) )
>   ={ Refl }=
>     ( (n, Element (S Z) MkPositive) )
>   ={ Refl }=
>     ( fromNat n )
>   QED

* Implementations:

> ||| NonNegRational is an implementation of Show
> implementation Show NonNegRational where
>   show q = if (den q == 1)
>            then show (num q)
>            else show (num q) ++ "/" ++ show (den q)

> ||| NonNegRational is an implementation of Num
> implementation Num NonNegRational where
>   (+) = plus
>   (*) = mult
>   fromInteger = fromNat . fromIntegerNat

> ||| NonNegRational is an implementation of DecEq
> implementation DecEq NonNegRational where
>   decEq x y with (Decidable.Equality.decEq (toFraction x) (toFraction y))
>     | (Yes p) = Yes (toFractionInjective p)
>     | (No contra) = No (\ prf => contra (toFractionEqLemma2 prf))

> ||| NonNegRational is an implementation of Eq
> implementation Eq NonNegRational where
>   (==) x y with (decEq x y)
>     | (Yes _) = True
>     | (No _)  = False

* One is not zero

> num0Eq0 : NonNegRational.BasicOperations.num (fromInteger 0) = 0
> num0Eq0 = ( NonNegRational.BasicOperations.num (fromInteger 0) )
>         ={ Refl }=
>           ( Fraction.BasicOperations.num (toFraction (fromInteger 0)) )
>         ={ Refl }=
>           ( fst (toFraction (fromInteger 0)) )
>         ={ Refl }=
>           ( fst (toFraction (fromNat (fromIntegerNat 0))) )
>         ={ cong (toFractionFromNatLemma (fromIntegerNat 0)) }=
>           ( fst (fromNat (fromIntegerNat 0)) )
>         ={ Refl }=
>           ( fromIntegerNat 0 )
>         ={ Refl }=
>           ( 0 )
>         QED

> num1Eq1 : NonNegRational.BasicOperations.num (fromInteger 1) = 1
> num1Eq1 = ( NonNegRational.BasicOperations.num (fromInteger 1) )
>         ={ Refl }=
>           ( Fraction.BasicOperations.num (toFraction (fromInteger 1)) )
>         ={ Refl }=
>           ( fst (toFraction (fromInteger 1)) )
>         ={ Refl }=
>           ( fst (toFraction (fromNat (fromIntegerNat 1))) )
>         ={ cong (toFractionFromNatLemma (fromIntegerNat 1)) }=
>           ( fst (fromNat (fromIntegerNat 1)) )
>         ={ Refl }=
>           ( fromIntegerNat 1 )
>         ={ Refl }=
>           ( 1 )
>         QED

> not1Eq0 : Not ((=) {A = NonNegRational} {B = NonNegRational} (fromInteger 1) (fromInteger 0))
> not1Eq0 prf = SIsNotZ s3 where
>   s1 : (=) {A = Nat} {B = Nat}
>        (NonNegRational.BasicOperations.num (fromInteger 1))
>        (NonNegRational.BasicOperations.num (fromInteger 0))
>   s1 = cong {f = NonNegRational.BasicOperations.num} prf
>   s2 : (=) {A = Nat} {B = Nat} 1 (NonNegRational.BasicOperations.num (fromInteger 0))
>   s2 = replace {P = \ X => (=) {A = Nat} {B = Nat} X (NonNegRational.BasicOperations.num (fromInteger 0))} num1Eq1 s1
>   s3 : (=) {A = Nat} {B = Nat} 1 0
>   s3 = replace {P = \ X => (=) {A = Nat} {B = Nat} 1 X} num0Eq0 s2

* Further properties of toFraction, fromInteger, etc.:

> |||
> toFractionFromIntegerLemma : (n : Integer) -> toFraction (fromInteger n) = fromInteger n
> toFractionFromIntegerLemma n =
>     ( toFraction (fromInteger n) )
>   ={ Refl }=
>     ( toFraction (fromNat (fromIntegerNat n)) )
>   ={ toFractionFromNatLemma (fromIntegerNat n) }=
>     ( fromNat (fromIntegerNat n) )
>   ={ Refl }=
>     ( fromInteger n )
>   QED

> ||| fromFraction is linear
> fromFractionLinear : (x, y : Fraction) -> fromFraction (x + y) = fromFraction x + fromFraction y
> fromFractionLinear x y =
>   let s1 = Element (normalize (x + y)) (normalNormalize (x + y)) in
>   let s2 = Element (normalize (normalize x + normalize y)) (normalNormalize (normalize x + normalize y)) in
>     ( fromFraction (x + y) )
>   ={ Refl }=
>     ( Element (normalize (x + y)) (normalNormalize (x + y))  )
>   ={ subsetEqLemma1 s1 s2 (sym (normalizePlusElim x y)) NormalUnique }=
>     ( Element (normalize (normalize x + normalize y)) (normalNormalize (normalize x + normalize y)) )
>   ={ Refl }=
>     ( fromFraction (normalize x + normalize y) )
>   ={ Refl }=
>     ( fromFraction (toFraction (Element (normalize x) (normalNormalize x))
>                     +
>                     toFraction (Element (normalize y) (normalNormalize y))) )
>   ={ Refl }=
>     ( fromFraction (toFraction (fromFraction x) + toFraction (fromFraction y)) )
>   ={ Refl }=
>     ( fromFraction x + fromFraction y )
>   QED

* Properties of addition:

> ||| Addition is commutative
> plusCommutative : (x : NonNegRational) -> (y : NonNegRational) -> x + y = y + x
> plusCommutative x y =
>     ( x + y )
>   ={ Refl }=
>     ( fromFraction (toFraction x + toFraction y) )
>   ={ cong {f = fromFraction} (plusCommutative (toFraction x) (toFraction y)) }=
>     ( fromFraction (toFraction y + toFraction x) )
>   ={ Refl }=
>     ( y + x )
>   QED

> ||| 0 is neutral element of addition
> plusZeroRightNeutral : (x : NonNegRational) -> x + 0 = x
> plusZeroRightNeutral x =
>     ( x + 0 )
>   ={ Refl }=
>     ( fromFraction (toFraction x + toFraction 0) )
>   ={ cong {f = fromFraction} (plusZeroRightNeutral (toFraction x)) }=
>     ( fromFraction (toFraction x) )
>   ={ fromToId x }=
>     ( x )
>   QED

> ||| 0 is neutral element of addition
> plusZeroLeftNeutral : (x : NonNegRational) -> 0 + x = x
> plusZeroLeftNeutral x =
>     ( 0 + x )
>   ={ plusCommutative 0 x }=
>     ( x + 0 )
>   ={ plusZeroRightNeutral x }=
>     ( x )
>   QED

> ||| Addition is associative
> plusAssociative : (x, y, z : NonNegRational) -> x + (y + z) = (x + y) + z
> plusAssociative x y z =
>   let x' = toFraction x in
>   let y' = toFraction y in
>   let z' = toFraction z in
>     ( x + (y + z) )
>   ={ Refl }=
>     ( fromFraction (x' + toFraction (fromFraction (y' + z'))) )
>   ={ Refl }=
>     ( fromFraction (x' + normalize (y' + z')) )
>   ={ Refl }=
>     ( Element (normalize (x' + normalize (y' + z'))) (normalNormalize (x' + normalize (y' + z'))) )
>   ={ toFractionInjective (normalizePlusElimRight x' (y' + z')) }=
>     ( Element (normalize (x' + (y' + z'))) (normalNormalize (x' + (y' + z'))) )
>   ={ toFractionInjective (cong (plusAssociative x' y' z')) }=
>     ( Element (normalize ((x' + y') + z')) (normalNormalize ((x' + y') + z')) )
>   ={ sym (toFractionInjective (normalizePlusElimLeft (x' + y') z')) }=
>     ( Element (normalize (normalize (x' + y') + z')) (normalNormalize (normalize (x' + y') + z')) )
>   ={ Refl }=
>     ( fromFraction (normalize (x' + y') + z') )
>   ={ Refl }=
>     ( fromFraction (toFraction (fromFraction (x' + y')) + z') )
>   ={ Refl }=
>     ( (x + y) + z )
>   QED

* Properties of multiplication:

> ||| Multiplication is commutative
> multCommutative : (x : NonNegRational) -> (y : NonNegRational) -> x * y = y * x
> multCommutative x y =
>     ( x * y )
>   ={ Refl }=
>     ( fromFraction ((toFraction x) * (toFraction y)) )
>   ={ cong {f = fromFraction} (multCommutative (toFraction x) (toFraction y)) }=
>     ( fromFraction ((toFraction y) * (toFraction x)) )
>   ={ Refl }=
>     ( y * x )
>   QED

> ||| 1 is neutral element of multiplication
> multOneRightNeutral : (x : NonNegRational) -> x * 1 = x
> multOneRightNeutral x =
>     ( x * 1 )
>   ={ Refl }=
>     ( fromFraction ((toFraction x) * (toFraction 1)) )
>   ={ Refl }=
>     ( fromFraction ((toFraction x) * (toFraction (fromInteger 1))) )
>   ={ cong {f = \ ZUZU => fromFraction ((toFraction x) * ZUZU)} (toFractionFromIntegerLemma 1) }=
>     ( fromFraction ((toFraction x) * (fromInteger 1)) )
>   ={ cong {f = fromFraction} (multOneRightNeutral (toFraction x)) }=
>     ( fromFraction (toFraction x) )
>   ={ fromToId x }=
>     ( x )
>   QED

> ||| 1 is neutral element of multiplication
> multOneLeftNeutral : (x : NonNegRational) -> 1 * x = x
> multOneLeftNeutral x =
>     ( 1 * x )
>   ={ multCommutative 1 x }=
>     ( x * 1 )
>   ={ multOneRightNeutral x }=
>     ( x )
>   QED

> |||
> multZeroRightZero : (x : NonNegRational) -> x * 0 = 0
> multZeroRightZero x =
>   let x' = toFraction x in
>     ( x * 0 )
>   ={ Refl }=
>     ( fromFraction (x' * 0) )
>   ={ Refl }=
>     ( Element (normalize (x' * 0)) (normalNormalize (x' * 0)) )
>   ={ toFractionInjective (normalizeEqLemma2 (x' * 0) 0 (multZeroRightEqZero x')) }=
>     ( Element (normalize 0) (normalNormalize 0) )
>   ={ Refl }=
>     ( fromFraction 0 )
>   ={ fromToId 0 }=
>     ( 0 )
>   QED

> |||
> multZeroLeftZero : (x : NonNegRational) -> 0 * x = 0
> multZeroLeftZero x =
>     ( 0 * x )
>   ={ multCommutative 0 x }=
>     ( x * 0 )
>   ={ multZeroRightZero x }=
>     ( 0 )
>   QED

* Properties of addition and multiplication:

> |||
> multDistributesOverPlusRight : (x, y, z : NonNegRational) -> x * (y + z) = (x * y) + (x * z)
> multDistributesOverPlusRight x y z =
>   let x' = toFraction x in
>   let y' = toFraction y in
>   let z' = toFraction z in
>     ( x * (y + z) )
>   ={ Refl }=
>     ( fromFraction (x' * toFraction (fromFraction (y' + z'))) )
>   ={ Refl }=
>     ( fromFraction (x' * (normalize (y' + z'))) )
>   ={ Refl }=
>     ( Element (normalize (x' * (normalize (y' + z')))) (normalNormalize (x' * (normalize (y' + z')))) )
>   ={ toFractionInjective (normalizeMultElimRight x' (y' + z')) }=
>     ( Element (normalize (x' * (y' + z'))) (normalNormalize (x' * (y' + z'))) )
>   ={ toFractionInjective (normalizeEqLemma2 (x' * (y' + z')) ((x' * y') + (x' * z')) multDistributesOverPlusRightEq) }=
>     ( Element (normalize ((x' * y') + (x' * z'))) (normalNormalize ((x' * y') + (x' * z'))) )
>   ={ toFractionInjective (sym (normalizePlusElim (x' * y') (x' * z'))) }=
>     ( Element (normalize (normalize (x' * y') + normalize (x' * z')))
>               (normalNormalize (normalize (x' * y') + normalize (x' * z'))) )
>   ={ Refl }=
>     ( fromFraction ((normalize (x' * y')) + (normalize (x' * z'))) )
>   ={ Refl }=
>     ( fromFraction ((toFraction (fromFraction (x' * y'))) + (toFraction (fromFraction (x' * z')))) )
>   ={ Refl }=
>     ( (x * y) + (x * z) )
>   QED

> |||
> multDistributesOverPlusLeft  : (x, y, z : NonNegRational) -> (x + y) * z = (x * z) + (y * z)
> multDistributesOverPlusLeft x y z =
>     ( (x + y) * z )
>   ={ multCommutative (x + y) z }=
>     ( z * (x + y) )
>   ={ multDistributesOverPlusRight z x y }=
>     ( z * x + z * y )
>   ={ cong {f = \ ZUZU => ZUZU + z * y} (multCommutative z x) }=
>     ( x * z + z * y )
>   ={ cong {f = \ ZUZU => x * z + ZUZU} (multCommutative z y) }=
>     ( x * z + y * z )
>   QED

* Implementations of refinements of |Num|:

> ||| NonNegRational is an implementation of NumPlusZeroNeutral
> implementation NumPlusZeroNeutral NonNegRational where
>   plusZeroLeftNeutral = NonNegRational.BasicProperties.plusZeroLeftNeutral
>   plusZeroRightNeutral = NonNegRational.BasicProperties.plusZeroRightNeutral

> ||| NonNegRational is an implementation of NumPlusAssociative
> implementation NumPlusAssociative NonNegRational where
>   plusAssociative = NonNegRational.BasicProperties.plusAssociative

> ||| NonNegRational is an implementation of NumMultZeroOne
> implementation NumMultZeroOne NonNegRational where
>   multZeroRightZero   = NonNegRational.BasicProperties.multZeroRightZero
>   multZeroLeftZero    = NonNegRational.BasicProperties.multZeroLeftZero
>   multOneRightNeutral = NonNegRational.BasicProperties.multOneRightNeutral
>   multOneLeftNeutral  = NonNegRational.BasicProperties.multOneLeftNeutral

> ||| NonNegRational is an implementation NumMultDistributesOverPlus
> implementation NumMultDistributesOverPlus NonNegRational where
>   multDistributesOverPlusRight = NonNegRational.BasicProperties.multDistributesOverPlusRight
>   multDistributesOverPlusLeft  = NonNegRational.BasicProperties.multDistributesOverPlusLeft

* Elementary arithmetic properties:

> multElimRight : (m : Nat) -> (n, d : PNat) -> fromFraction (m * (toNat n), d * n) = fromFraction (m, d)
> multElimRight m n d =
>   let s1 = Element (normalize (m * (toNat n), d * n)) (normalNormalize (m * (toNat n), d * n)) in
>   let s2 = Element (normalize (m, d)) (normalNormalize (m, d)) in
>     ( fromFraction (m * (toNat n), d * n) )
>   ={ Refl }=
>     ( Element (normalize (m * (toNat n), d * n)) (normalNormalize (m * (toNat n), d * n)) )
>   ={ subsetEqLemma1 s1 s2 (normalizeUpscaleLemma (m, d) n) NormalUnique }=
>     ( Element (normalize (m, d)) (normalNormalize (m, d)) )
>   ={ Refl }=
>     ( fromFraction (m, d) )
>   QED

> postulate sumOneLemma1 : {n: Nat} ->
>                          fromFraction (n, Element (S n) MkPositive)
>                          +
>                          fromFraction (1, Element (S n) MkPositive)
>                          =
>                          1

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Data.Time.Clock.Internal.DiffTime

import Data.Time.Clock.Internal.Fixed as F

--import Data.Data
--import Data.Fixed
--import Data.Ratio ((%))
--import Data.Typeable

||| This is a length of time, as measured by a clock.
||| Conversion functions will treat it as seconds.
||| It has a precision of 10^-12 s.
public export
data DiffTime = MkDiffTime Pico

export
Enum DiffTime where
  pred (MkDiffTime x) = MkDiffTime (pred x)
  toNat (MkDiffTime x) = toNat x
  fromNat x = MkDiffTime (fromNat x)

export
Show DiffTime where
    show (MkDiffTime t) = show t

export
Eq DiffTime where
  (MkDiffTime a) == (MkDiffTime b) = a == b

export
Ord DiffTime where
  compare (MkDiffTime a) (MkDiffTime b) = compare a b

add: DiffTime -> DiffTime -> DiffTime
add (MkDiffTime x) (MkDiffTime y) = MkDiffTime (x + y)

(+) : DiffTime -> DiffTime -> DiffTime
(+) = add

minus: DiffTime -> DiffTime -> DiffTime
minus (MkDiffTime x) (MkDiffTime y) = MkDiffTime (x - y)

negate: DiffTime -> DiffTime
negate (MkDiffTime x) = MkDiffTime (negate x)

abs : DiffTime-> DiffTime
abs (MkDiffTime x) = MkDiffTime (abs x)

fromInteger : Integer -> DiffTime
fromInteger x = MkDiffTime (MkFixed x)

mult: DiffTime -> DiffTime -> DiffTime
mult (MkDiffTime x) (MkDiffTime y) = MkDiffTime (x * y)

(*): DiffTime -> DiffTime -> DiffTime
(*) = mult

toRational: DiffTime -> Double
toRational (MkDiffTime x) = (toRational x)

fracDiv: DiffTime -> DiffTime -> DiffTime
fracDiv (MkDiffTime x) (MkDiffTime y) = MkDiffTime (fracDiv x y)

(/): DiffTime -> DiffTime -> DiffTime
(/) = fracDiv

recip : DiffTime -> DiffTime
recip (MkDiffTime x) = MkDiffTime (recip x)

secondsToDiffTime: Integer -> DiffTime
secondsToDiffTime = fromInteger

export
picosecondsToDiffTime: Integer -> DiffTime
picosecondsToDiffTime x = MkDiffTime (MkFixed x)

export
diffTimeToPicoseconds : DiffTime -> Integer
diffTimeToPicoseconds (MkDiffTime (MkFixed x)) = x

max_stars_repo_name: gdevanla/idris-time

max_issues_repo_name: gdevanla/idris-time

max_forks_repo_name: gdevanla/idris-time


text:
module Replica.App.Run.Dependencies

import Data.Maybe
import Data.List
import Data.List1
import Data.String

import Replica.Core.Types
import Replica.Other.String

%default total

public export
record SuitePlan where
  constructor SPlan
  name : Maybe String
  now : List Test
  later : List Test
  skipped : List (String, Test)

public export
record TestPlan where
  constructor Plan
  ready : List SuitePlan
  waitingOthers : List SuitePlan

export
displaySuitePlan : SuitePlan -> String
displaySuitePlan x = removeTrailingNL $ unlines
  [ "  Plan:"
  , "    Now: \{show $ map name x.now}"
  , "    Later: \{show $ map name x.later}"
  , "    Skipped: \{show $ map (name . snd) x.skipped}"
  ]

export
displayPlan : TestPlan -> String
displayPlan plan = unlines $ ("Ready:"
  :: (plan.ready >>= go))
  ++ ("Postponed:"
  :: (plan.waitingOthers >>= go))
  where
    go : SuitePlan -> List String
    go p = ["\{fromMaybe "No suite" p.name}:", displaySuitePlan p]

public export
isReady : Test -> Bool
isReady = force . null . require

dependsOnOther : List Test -> Bool
dependsOnOther xs = any (not . flip elem (name <$> xs))  $ xs >>= require

buildSuitePlan : List1 Test -> SuitePlan
buildSuitePlan (x:::xs) = let
  (now, later) = partition (force . null . require) $ x::xs
  in SPlan x.suite now later []

removeRequirements : List String -> Test -> Test
removeRequirements xs y
  = record {require $= filter (not . (`elem` xs))} y

export
buildPlan : (available : List Test) -> (rejected : List Test) -> TestPlan
buildPlan available rejected = uncurry Plan $
  partition (not . dependsOnOther . later) $ namedSuitePlan
  where
    cleantAvailable : List Test
    cleantAvailable
      = removeRequirements (name <$> rejected) <$> available
    suites : List (List1 Test)
    suites = groupBy ((==) `on` suite) $ sortBy (compare `on` suite) cleantAvailable
    namedSuitePlan : List SuitePlan
    namedSuitePlan = map buildSuitePlan suites

export
sortResults : List (Test, Either TestError TestResult) -> (List String, List String)
sortResults
  = bimap (map (Test.name . fst)) (map (Test.name . fst))
    . partition (either (const False) isSuccess . snd)

export
updateSuite : (successes, other : List String) -> SuitePlan -> SuitePlan
updateSuite successes other (SPlan n now later skipped) = let
  (now', later') = partition (force . null . require) $ removeRequirements successes <$> later
  (later'', skipped') = partition (not . any (`elem` other) . require) later'
  in SPlan n (now ++ now') later'' (skipped ++ (map (\t => (fromMaybe "unknown_test" $ head' t.require , t)) skipped'))

export
updateOnBatchResults : List (Test, Either TestError TestResult) -> TestPlan -> TestPlan
updateOnBatchResults xs plan = let
  (successes, other) = sortResults xs
  ready' = updateSuite successes other <$> plan.ready
  waiting' = updateSuite successes other <$> plan.waitingOthers
  (ready'', waitingOthers') =
    partition (not . dependsOnOther . later) waiting'
  in Plan (ready' ++ ready'') waitingOthers'

max_stars_repo_name: claymager/REPLica

max_issues_repo_name: claymager/REPLica

max_forks_repo_name: claymager/REPLica


text:
module Server.InigoServer.Handler

import Data.Buffer
import Data.Either
import Data.List
import Data.Maybe
import Data.String
import Extra.Buffer
import Extra.Either
import Extra.String
import Fmt
import Inigo.Account.Account
import Inigo.Async.Base
import Inigo.Async.CloudFlare.KV as KV
import Inigo.Async.CloudFlare.Worker
import Inigo.Async.Package
import Inigo.Async.Promise
import Inigo.Async.SubtleCrypto.SubtleCrypto
import Inigo.Package.Package
import Inigo.Package.PackageDeps
import Inigo.Package.PackageIndex
import Markdown
import Markdown.Format.Html
import SemVar
import Server.InigoServer.KVOps as KVOps
import Server.InigoServer.Util as Util
import Server.Template.Template as Template
import Toml

limit : Nat
limit = 50

defaultHash : String -> Algorithm
defaultHash salt =
  PBKDF2 Sha256 salt 10000

-- TODO: While this is practical, we should
--       switch the server to use dependent types (e.g. App)
--       in order to clean up the mess of dependencies here
--       Note: this may be hard to do with Promises, but maybe
--       this can assist us in writing cleaner code!

-- TODO: Complete Request Data type
-- TODO: mapError
-- TODO: Parallel requests
handlePage : String -> List (String, String) -> Promise Response
handlePage path vars =
  do
    contents <- KV.read "pages" (Util.withIndex path)
    layout <- KV.read "static" "/layout.html" -- TODO: Request in paralel
    if contents == ""
      then pure (404, "Missing data for page", [])
      else do
        let tmplContents = Template.template contents vars
        case map toHtml $ Markdown.parse tmplContents of
          Nothing =>
            pure (500, "Failed to parse markdown", [])
          Just parsed =>
            pure (html (Util.renderLayout layout parsed))

handleApiArchive : String -> String -> Version -> Promise Response
handleApiArchive packageNS packageName version =
  do
    Just contents <- KVOps.readArchive packageNS packageName version
      | Nothing => pure (404, "not found", [])
    pure (200, contents, [])

handlePackageIndex : Promise Response
handlePackageIndex =
  do
    index <- KVOps.readIndex
    let packageList = map Util.buildPkgLink (take limit index)
    let vars = [("PACKAGES", join "\n" packageList)]
    handlePage "/packageIndex" vars

enumerate : String -> String -> Nat -> String
enumerate sing _ (S Z) = "1 " ++ sing
enumerate _ plur n = fmt "%d %s" (cast n) plur

handleSearch : String -> Promise Response
handleSearch term =
  do
    index <- KVOps.readIndex
    let packages = searchPackageIndex term index
    let packageList = map Util.buildPkgLink packages
    let vars =
      [ ("COUNT", enumerate "package" "packages" (length packageList))
      , ("TERM", term)
      , ("PACKAGES", join "\n" packageList)
      ]
    handlePage "/search" vars

handleApiPackageIndex : Promise Response
handleApiPackageIndex =
  do
    index <- KVOps.readIndex
    pure (200, encodePackageIndex index, [])

orLatestVersion : Maybe Version -> String -> String -> Promise (Maybe Version)
orLatestVersion (Just v) = const $ const $ lift (Just v)
orLatestVersion Nothing = latestVersion

handlePackage : String -> String -> (Maybe Version) -> Promise Response
handlePackage packageNS packageName maybeVersion =
  do
    Just version <- orLatestVersion maybeVersion packageNS packageName
      | Nothing => pure (404, "not found", [])
    Right pkg <- KVOps.readPackage packageNS packageName version
      | Left err => pure (500, err, [])
    readme <- KVOps.readReadme packageNS packageName version
    versions <- readVersions packageNS packageName
    let vars =
      [ ("NS", ns pkg)
      , ("PACKAGE", package pkg)
      , ("DESCRIPTION", fromMaybe "" $ description pkg)
      , ("EXT_DESCRIPTION", fromMaybe "" $ readme)
      , ("VERSION", show version)
      , ("VERSIONS", versionLinks versions)
      , ("LINK", fromMaybe "" $ map asLink (link pkg))
      , ("LICENSE", fromMaybe "" (license pkg))
      ]
    log ("Vars: " ++ show vars)
    handlePage "/package" vars
  where
    versionLink : Version -> String
    versionLink version = fmt " * [%s](/packages/%s/%s/%s)" (show version) packageNS packageName (show version)

    asLink : String -> String
    asLink link =
      fmt "[%s](%s)" link link

    versionLinks : List Version -> String
    versionLinks =
      join "\n" . map versionLink . reverse . sort

handleStatic : String -> Promise Response
handleStatic path =
  do
    contents <- KV.read "static" path
    let contentType = Util.sniffContentType path
    if contents == ""
      then pure (404, "Static page not found", [])
      else pure (200, contents, contentType)

handleAccountPost : String -> String -> Promise Response
handleAccountPost ns body =
  do
    Right (email, passphrase) <- getAccountValues body
      | Left res => pure res
    salt <- getRand 20
    let kdf = defaultHash salt
    hashedPassphrase <- hash kdf passphrase
    let Right account = mkAccount ns email kdf passphrase hashedPassphrase
      | Left err => pure (400, err, [])
    Nothing <- KVOps.newAccount account
      | Just (err, msg) => pure (err, msg, [])
    pure (200, "ok", [])
  where
    getAccountValues : String -> Promise (Either Response (String, String))
    getAccountValues body =
      do
        let Just toml = parseToml body
          | Nothing => pure $ Left (400, "Bad request: invalid body toml", [])
        let Just (Str email) = get ["email"] toml
          | _ => pure $ Left (400, "Bad request: missing email", [])
        let Just (Str passphrase) = get ["passphrase"] toml
          | _ => pure $ Left (400, "Bad request: missing passphrase", [])
        pure $ Right (email, passphrase)

handleAccountLoginPost : String -> String -> Promise Response
handleAccountLoginPost ns passphrase =
  do
    Just (kdf, accountHash) <- KVOps.readAccountHash ns
      | _ => pure (404, "not found", [])
    hashedInput <- hash kdf passphrase
    if accountHash == hashedInput
      then do
        session <- getRand 50
        KVOps.writeSession session ns
        pure (200, session, [])
      else
        pure (500, "unauthorized", [])

authenticate : String -> String -> Promise (Maybe Response)
authenticate session ns =
  do
    Just sessionNS <- KVOps.readSession session
      | Nothing => pure $ Just (500, "unauthorized", [])
    if sessionNS == ns
      then
        pure Nothing
      else
        pure $ Just (500, "unauthorized", [])

handleApiArchivePost : String -> String -> String -> Version -> String -> Promise Response
handleApiArchivePost session packageNS packageName version body =
  do
    Nothing <- authenticate session packageNS
      | Just res => pure res
    KVOps.writeArchive packageNS packageName version body
    pure (200, "ok", [])

handleApiReadmePost : String -> String -> String -> Version -> String -> Promise Response
handleApiReadmePost session packageNS packageName version body =
  do
    Nothing <- authenticate session packageNS
      | Just res => pure res
    KVOps.writeReadme packageNS packageName version body
    pure (200, "ok", [])

handleApiPackagePost : String -> String -> String -> Version -> String -> Promise Response
handleApiPackagePost session packageNS packageName version body =
  do
    Nothing <- authenticate session packageNS
      | Just res => pure res
    pkg <- expectResult (parsePackage body)
    -- Update package deps
    currDeps <- KVOps.readDeps pkg
    let nextDeps = updatePackageDep currDeps pkg
    KVOps.writeDeps pkg nextDeps
    -- Update current package
    KVOps.writePackage pkg
    -- Update index if latest
    let isLatest = (Just version) == (head' $ reverse $ sort $ map fst nextDeps) --'
    if isLatest
      then
        do
          -- Update the global index
          currIndex <- KVOps.readIndex
          let nextIndex = updatePackageMeta currIndex pkg
          KVOps.writeIndex nextIndex
      else pure ()
    pure (200, "ok", [])

handleApiPackageConf : String -> String -> Version -> Promise Response
handleApiPackageConf packageNS packageName version =
  do
    Right pkg <- KVOps.readPackage packageNS packageName version
      | Left err => pure (500, err, [])
    pure (200, encodePackage pkg, [])

handleApiPackageDeps : String -> String -> Promise Response
handleApiPackageDeps packageNS packageName =
  do
    deps <- KVOps.readAllDeps packageNS packageName
    log ("Deps: " ++ show deps)
    -- TODO: Better encoding here
    let res = join "\n\n" $ map (\(pkg, deps) => fmt "['%s']\n%s" (join "." pkg) (encodePackageDeps deps)) deps
    pure (200, res, [])

getVersion : String -> Promise Version
getVersion str =
  case parseVersion str of
    Just version =>
      pure version

    Nothing =>
      reject ("Invalid version: " ++ str)

getSession : List (String, String) -> Promise String
getSession headers =
  case map (split ' ' . snd) $ find ((== "authorization") . fst) headers of
    Just ["Basic", session] =>
      pure session
    _ =>
      reject ("Authorization Required")

export
handler : String -> String -> List (String, String) -> List (String, String) -> Promise Response
handler path body params headers =
  do
    log ("Request Path: " ++ path ++ ", params=" ++ show params)
    case drop 1 (split '/' path) of
      ["api", "archive", ns, package, version] =>
        handleApiArchive ns package !(getVersion version)

      ["api", "archive", ns, package, version, "post"] =>
        handleApiArchivePost !(getSession headers) ns package !(getVersion version) body

      ["api", "readme", ns, package, version, "post"] =>
        handleApiReadmePost !(getSession headers) ns package !(getVersion version) body

      ["api", "packages"] =>
        handleApiPackageIndex

      ["api", "packages", ns, package, version, "post"] =>
        handleApiPackagePost !(getSession headers) ns package !(getVersion version) body

      ["api", "packages", ns, package, version, "conf"] =>
        handleApiPackageConf ns package !(getVersion version)

      ["api", "packages", ns, package, "deps"] =>
        handleApiPackageDeps ns package

      ["search"] =>
        case params of
          ("term", term) :: _ =>
            handleSearch term
          _ =>
            pure (404, "Missing search term", [])

      ["packages"] =>
        handlePackageIndex

      ["packages", ns, package] =>
        handlePackage ns package Nothing

      ["packages", ns, package, version] =>
        handlePackage ns package (Just !(getVersion version))

      ["api", "account", ns, "post"] =>
        handleAccountPost ns body

      ["api", "account", ns, "login"] =>
        handleAccountLoginPost ns body

      _ =>
        do
          staticResponse <- handleStatic path
          case staticResponse of
            (200, _, _) =>
              pure $ staticResponse
            _ =>
              handlePage path []


text:
module Text.CSS.Flexbox

import Text.CSS.Render

%default total

public export
data FlexDirection =
    Row
  | RowReverse
  | Column
  | ColumnReverse

export
Render FlexDirection where
  render Row           = "row"
  render RowReverse    = "row-reverse"
  render Column        = "column"
  render ColumnReverse = "column-reverse"

public export
data FlexAlign =
    Normal
  | Stretch
  | Center
  | Start
  | End
  | FlexStart
  | FlexEnd
  | Baseline
  | FirstBaseline
  | LastBaseline

export
Render FlexAlign where
  render Normal        = "normal"
  render Stretch       = "stretch"
  render Center        = "center"
  render Start         = "start"
  render End           = "end"
  render FlexStart     = "flex-start"
  render FlexEnd       = "flex-end"
  render Baseline      = "baseline"
  render FirstBaseline = "first baseline"
  render LastBaseline  = "last baseline"

namespace FlexJustify
  public export
  data FlexJustify =
      Center
    | Start
    | End
    | FlexStart
    | FlexEnd
    | Left
    | Right
    | Normal
    | SpaceBetween
    | SpaceAround
    | SpaceEvenly
    | Stretch

  export
  Render FlexJustify where
    render Center       = "center"
    render Start        = "start"
    render End          = "end"
    render FlexStart    = "flex-start"
    render FlexEnd      = "flex-end"
    render Left         = "left"
    render Right        = "right"
    render Normal       = "normal"
    render SpaceBetween = "space-between"
    render SpaceAround  = "space-around"
    render SpaceEvenly  = "space-evenly"
    render Stretch      = "stretch"


text:
import OCaml.IO
import OCaml.Lwt

%lib malfunction "cohttp"
%lib malfunction "cohttp-lwt"
%lib malfunction "cohttp-lwt-unix"
%lib malfunction "uri"
%lib malfunction "lwt.unix"

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

Uri : Type
Uri = Ptr

uri_to_string : Uri -> OCaml_IO String
uri_to_string u =
  ocamlCall "Uri.to_string" (Uri -> OCaml_IO String) u

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

Request : Type
Request = Ptr

uri : Request -> OCaml_IO Uri
uri r = ocamlCall "Cohttp.Request.uri" (Request -> OCaml_IO Uri) r

Response : Type
Response = Ptr

Body : Type
Body = Ptr

body_to_string_lwt : Body -> OCaml_IO (Lwt String)
body_to_string_lwt b =
  ocamlCall "Cohttp_lwt.Body.to_string" (Body -> OCaml_IO (Lwt String)) b

Meth : Type
Meth = Ptr

meth : Request -> OCaml_IO Meth
meth r = ocamlCall "Cohttp.Request.meth" (Request -> OCaml_IO Meth) r

string_of_method : Meth -> OCaml_IO String
string_of_method m =
  ocamlCall "Cohttp.Code.string_of_method" (Meth -> OCaml_IO String) m

Header : Type
Header = Ptr

headers : Request -> OCaml_IO Header
headers r =
   ocamlCall "Cohttp.Request.headers" (Request -> OCaml_IO Header) r

header_to_string : Header -> OCaml_IO String
header_to_string h =
  ocamlCall "Cohttp.Header.to_string" (Meth -> OCaml_IO String) h

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

-- Representative of `OK polymorphic variant
OK : Int
OK = 17692

server_respond_string : Maybe Bool -> Maybe Header -> Int ->
                        String -> () ->
                        OCaml_IO (Lwt (Response, Body))
server_respond_string flush headers status body () =
  ocamlCall "Cohttp_lwt_unix.Server.respond_string"
      (Maybe Bool -> Maybe Header -> Int -> String -> () -> OCaml_IO (Lwt (Response, Body)))
      flush headers status body ()

Server : Type
Server = Ptr

server_create : Maybe Int -> -- timeout
                Maybe Int -> -- backlog
                Maybe (Lwt ()) -> -- stop
                Maybe (Ptr -> OCaml_IO ()) -> -- on_exn
                Maybe Ptr -> -- ctx
                Maybe Ptr -> -- mode
                Server ->
                OCaml_IO (Lwt ())
server_create timeout backlog stop on_exn ctx mode server =
  ocamlCall "Cohttp_lwt_unix.Server.create"
    (Maybe Int -> -- timeout
     Maybe Int -> -- backlog
     Maybe (Lwt ()) -> -- stop
     Maybe (Ptr -> OCaml_IO ()) -> -- on_exn
     Maybe Ptr -> -- ctx
     Maybe Ptr -> -- mode
     Server ->
     OCaml_IO (Lwt ()))
    timeout backlog stop on_exn ctx mode server

server_make : Maybe (Ptr -> OCaml_IO ()) -> -- conn_closed
              (Ptr -> Request -> Body -> OCaml_IO (Lwt (Response, Body))) ->
              () ->
              OCaml_IO Server
server_make conn_closed callback () =
  ocamlCall "Cohttp_lwt_unix.Server.make"
     (Maybe (Ptr -> OCaml_IO ()) -> -- conn_closed
      (Ptr -> Request -> Body -> OCaml_IO (Lwt (Response, Body))) ->
      () ->
      OCaml_IO Server)
     conn_closed callback ()

lwtRun : Lwt () -> OCaml_IO ()
lwtRun lwt = ocamlCall "Lwt_main.run" (Lwt () -> OCaml_IO ()) lwt

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

callback : Ptr -> Request -> Body -> OCaml_IO (Lwt (Response, Body))
callback conn req body = do
  uri <- pure req >>= uri >>= uri_to_string
  meth <- pure req >>= meth >>= string_of_method
  headers <- pure req >>= headers >>= header_to_string
  print_endline ("URI: " ++ uri)
  print_endline ("Method: " ++ meth)
  print_endline ("Headers: " ++ headers)
  lwtb <- body_to_string_lwt body
  lwtb `lwtBind`
    (\ body_str =>
        let response =
          unlines [ "
Idris says \"Hello ML Workshop!\"
"
                  , "
"
                  , "Uri: " ++ uri ++ "
"
                  , "Method: " ++ meth ++ "
"
                  , "Headers: " ++ headers ++ "
"
                  , "Body:
" ++ body_str ++ "
"
                  ]
        in
        server_respond_string Nothing Nothing OK response ())

main : OCaml_IO ()
main = do
  server <- server_make Nothing callback ()
  thread <- server_create Nothing Nothing Nothing Nothing Nothing Nothing server
  lwtRun thread

max_stars_repo_name: ioanluca/real-world-idris

max_issues_repo_name: ioanluca/real-world-idris

max_forks_repo_name: ioanluca/real-world-idris


text:
module Main

import Control.Monad.Identity
import Control.Monad.Trans

import Data.Maybe
import Data.String.Parser

%default partial
-- Build this program with '-p contrib'

showRes : Show a => Either String (a, Int) -> IO ()
showRes res = case res of
                Left err => putStrLn err
                Right (xs, rem) => printLn xs

-- test lifting
parseStuff : ParseT IO ()
parseStuff = do a <- string "abc"
                lift $ putStrLn "hiya"
                b <- string "def"
                pure ()

-- test a parsing from a pure function
pureParsing : String -> Either String ((List Char), Int)
pureParsing str = parse (many (satisfy isDigit)) str

-- test option
optParser : ParseT IO String
optParser = do res <- option "" (takeWhile isDigit)
               string "def"
               pure $ res

-- test optional
maybeParser : ParseT IO Bool
maybeParser = do res <- optional (string "abc")
                 string "def"
                 pure $ isJust res

main : IO ()
main = do
    res <- parseT parseStuff "abcdef"
    res <- parseT (string "hi") "hiyaaaaaa"
    case res of
        Left err => putStrLn "NOOOOOOO!"
        Right ((), i) => printLn i
    bad <- parseT (satisfy isDigit) "a"
    showRes bad
    bad2 <- parseT (string "good" <?> "Not good") "bad bad bad"
    showRes bad2
    digs <- parseT (many (satisfy isDigit)) "766775"
    showRes digs
    showRes $ pureParsing "63553"
    s <- parseT (takeWhile isDigit) "887abc8993"
    showRes s
    res <- parseT optParser "123def"
    showRes res
    res <- parseT optParser "def"
    showRes res
    res <- parseT maybeParser "abcdef"
    showRes res
    res <- parseT maybeParser "def"
    showRes res
    pure ()


text:
-- This tests checks, whether toplevel constants are
-- properly memoized. If they are not, this test
-- will perform 10^20 additions and will therefore not
-- finish in reasonable time.
n0 : Nat
n0 = 1

n1 : Nat
n1 = n0 + n0 + n0 + n0 + n0 + n0 + n0 + n0 + n0 + n0

n2 : Nat
n2 = n1 + n1 + n1 + n1 + n1 + n1 + n1 + n1 + n1 + n1

n3 : Nat
n3 = n2 + n2 + n2 + n2 + n2 + n2 + n2 + n2 + n2 + n2

n4 : Nat
n4 = n3 + n3 + n3 + n3 + n3 + n3 + n3 + n3 + n3 + n3

n5 : Nat
n5 = n4 + n4 + n4 + n4 + n4 + n4 + n4 + n4 + n4 + n4

n6 : Nat
n6 = n5 + n5 + n5 + n5 + n5 + n5 + n5 + n5 + n5 + n5

n7 : Nat
n7 = n6 + n6 + n6 + n6 + n6 + n6 + n6 + n6 + n6 + n6

n8 : Nat
n8 = n7 + n7 + n7 + n7 + n7 + n7 + n7 + n7 + n7 + n7

n9 : Nat
n9 = n8 + n8 + n8 + n8 + n8 + n8 + n8 + n8 + n8 + n8

n10 : Nat
n10 = n9 + n9 + n9 + n9 + n9 + n9 + n9 + n9 + n9 + n9

n11 : Nat
n11 = n10 + n10 + n10 + n10 + n10 + n10 + n10 + n10 + n10 + n10

n12 : Nat
n12 = n11 + n11 + n11 + n11 + n11 + n11 + n11 + n11 + n11 + n11

n13 : Nat
n13 = n12 + n12 + n12 + n12 + n12 + n12 + n12 + n12 + n12 + n12

n14 : Nat
n14 = n13 + n13 + n13 + n13 + n13 + n13 + n13 + n13 + n13 + n13

n15 : Nat
n15 = n14 + n14 + n14 + n14 + n14 + n14 + n14 + n14 + n14 + n14

n16 : Nat
n16 = n15 + n15 + n15 + n15 + n15 + n15 + n15 + n15 + n15 + n15

n17 : Nat
n17 = n16 + n16 + n16 + n16 + n16 + n16 + n16 + n16 + n16 + n16

n18 : Nat
n18 = n17 + n17 + n17 + n17 + n17 + n17 + n17 + n17 + n17 + n17

n19 : Nat
n19 = n18 + n18 + n18 + n18 + n18 + n18 + n18 + n18 + n18 + n18

n20 : Nat
n20 = n19 + n19 + n19 + n19 + n19 + n19 + n19 + n19 + n19 + n19

main : IO ()
main = do printLn n20