text:
module Invincy.Parsing
import Data.Vect
import Invincy.Core

%access public export

mutual
  data Result : (i, r : Type) -> Type where
    Done : Stream t s => s -> r -> Result s r
    Partial : Stream t s => Inf (Parser s r) -> Result s r
    Failure : Stream t s => String -> Result s r

  data Parser : (i, r : Type) -> Type  where
    MkParser : Stream t s => (s -> Result s r) -> Parser s r

runParser : Parser s r -> s -> Result s r
runParser (MkParser f) = f

implementation Stream t s => Functor (Result s) where
  map f (Done i r) = Done i (f r)
  map f (Partial k) = assert_total (Partial (MkParser $ map f . runParser k))
  map _ f@(Failure s) = f

implementation Functor (Parser s) where
  map f (MkParser k) = MkParser $ (\x => map f $ k x)

implementation Stream t s => Applicative (Parser s) where
  pure x = MkParser (\i => Done i x)
  (MkParser f) <*> g = MkParser $ \i => case f i of
    Done i' f' => case runParser g i' of
      Done i'' r => Done i'' (f' r)
      Partial k => Partial (MkParser $ map f' . runParser k)
      Failure f => Failure f
    Partial k => Partial $ k <*> g
    Failure f => Failure f

infixl 2 <*>|
(<*>|) : Stream t s => Parser s (a -> b) -> Lazy (Parser s a) -> Parser s b
(<*>|) f g = f <*> g

implementation Stream t s => Monad (Parser s) where
  f >>= g = MkParser $ \i => case runParser f i of
    Done i' f' => runParser (g f') i'
    Partial k => Partial $ k >>= g
    f@(Failure s) => f

interface Applicative f => LazyAlternative (f : Type -> Type) where
  empty : f a
  (<|>) : f a -> Lazy (f a) -> f a

implementation Stream t s => LazyAlternative (Parser s) where
  empty = MkParser . const $ Failure "an alternative is empty"
  f <|> g = MkParser $ \i => case (runParser f i) of
    Failure _ => runParser g i
    -- this could probably be improved
    Partial k => Partial $
      let cont = MkParser (\i' => runParser k i');
          next = MkParser (\i' => runParser g (i <+> i'))
      in cont <|> next
    done => done

fail : Stream t s => String -> Parser s r
fail = MkParser . const . Failure

infixl 3 <?>
(<?>) : Stream t s => Parser s a -> String -> Parser s a
(<?>) p s = p <|> fail s

item : Stream t s => Parser s t
item = MkParser $ \i => case uncons i of
  Nothing => Partial item
  Just (x, xs) => Done xs x

sat : Stream t s => (t -> Bool) -> Parser s t
sat p = do
  i <- item
  if p i then pure i else fail "sat"

ignore : Stream t s => Parser s a -> Parser s ()
ignore p = p *> pure ()

val : (Eq t, Stream t s) => t -> Parser s ()
val x = ignore (sat (== x))

raw : (Eq t, Stream t s) => s -> Parser s ()
raw l = case uncons l of
  Nothing => pure ()
  Just (x, xs) => do
    sat (== x)
    raw xs
    pure ()

oneOf : (Eq t, Stream t s) => List t -> Parser s t
oneOf l = sat (flip elem l)

option : Stream t s => Parser s a -> Parser s (Maybe a)
option p = (Just <$> p) <|> (pure Nothing)

manyTill : Stream t s => Parser s a -> Parser s b -> Parser s (List a)
manyTill p t = option t >>= maybe ((<+>) . pure <$> p <*>| manyTill p t) (const $ pure neutral)

many : Stream t s => Parser s a -> Parser s (List a)
many p = option p >>= maybe (pure neutral) (\x => (<+>) . pure <$> pure x <*>| many p)

some : Stream t s => Parser s a -> Parser s (x:List a ** NonEmpty x)
some p = do
  first <- p
  rest <- many p
  pure $ (first :: rest ** IsNonEmpty)

sepBy1 : Stream t s => Parser s a -> Parser s () -> Parser s (x:List a ** NonEmpty x)
sepBy1 x s = do
  first <- x
  rest <- many (s *> x)
  pure $ (first :: rest ** IsNonEmpty)

sepBy : Stream t s => Parser s a -> Parser s () -> Parser s (List a)
sepBy x s = maybe [] getWitness <$> option (sepBy1 x s)

match : Stream t s => Parser s a -> Parser s (s, a)
match p = MkParser $ \i => match' i $ runParser p i
  where
    match' : s -> Result s a -> Result s (s, a)
    match' raw (Done i r) =
      let il = toList i
          rawl = toList raw
      in Done i (fromList (take (minus (length rawl) (length il)) rawl), r)
    match' raw (Failure e) = Failure e
    match' raw (Partial k) = Partial $ (\(raw', x) => (raw <+> raw', x)) <$> match k

feed : Stream t s => Result s r -> s -> Result s r
feed (Partial k) i = runParser k i
feed (Done i r) i' = Done (i <+> i') r
feed (Failure s) _ = Failure s

digit : Stream Char s => Parser s Char
digit = oneOf ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9']

integer : Stream Char s => Parser s Integer
integer = cast . pack . getWitness <$> some digit

-- feed (feed (runParser ((list ['f', 'o', 'o'] *> pure False) <|> (list ['f', 'o', 'r'] *> pure True)) ['f']) ['o']) ['o']
-- feed (feed (runParser ((list ['f', 'o', 'o'] *> pure False) <|> (list ['f', 'o', 'r'] *> pure True)) ['f']) ['o']) ['r']

parseWith : Monad m => Parser s r -> m s -> m (Result s r)
parseWith p r = do
  v <- r
  case runParser p v of
    Partial k => parseWith k r
    other => pure other

max_stars_repo_name: defanor/invincy

max_issues_repo_name: defanor/invincy

max_forks_repo_name: defanor/invincy


text:
module Term

-- Simply-typed lambda calculus with
--   (1) natural numbers as the only base type, and
--   (2) primitive recursion.
--
-- Terms in the lambda calculus are initially untyped.
-- The usual typing judgement is defined as a separate
-- data type in a separate module.
-- Note that meta-theory developed in yet other modules
-- will rely on the typing judgement.
--
-- Note that variables in the lambda calculus are not
-- named but identified by their de Bruijn index.
-- Since terms in our lambda calculus are initially
-- untyped, they may therefore also be ill-scoped.
-- Hence, de Bruijn indices are represented simply
-- by natural numbers (since they will only be
-- required to be valid in a context that is chosen
-- later, during typing of a term).

%default total
%access public export

------------------------------------------------
-- Begin: (UNTYPED) TERMS OF THE LAMBDA CALCULUS

data Term : Type where
  TVar  : (i : Nat) -> Term
  TAbs  : Term -> Term
  TApp  : Term -> Term -> Term
  TRec  : Term -> Term -> Term ->
          Term
  TZero : Term
  TSucc : Term -> Term
  TPred : Term -> Term
  TIfz  : Term -> Term -> Term ->
          Term

-- Construction of terms is a congruence for equality.
-- The following straightforward lemmas are often useful
-- for writing shorter proofs.

congVar : i = j -> TVar i = TVar j
congVar Refl = Refl

congAbs : e = e' -> TAbs e = TAbs e'
congAbs Refl = Refl

congApp : e1 = e1' -> e2 = e2' -> TApp e1 e2 = TApp e1' e2'
congApp Refl Refl = Refl

congRec : e1 = e1' -> e2 = e2' -> e3 = e3' ->
          TRec e1 e2 e3 = TRec e1' e2' e3'
congRec Refl Refl Refl = Refl

congZero : TZero = TZero
congZero = Refl

congSucc : e = e' -> TSucc e = TSucc e'
congSucc Refl = Refl

congPred : e = e' -> TPred e = TPred e'
congPred Refl = Refl

congIfz : e1 = e1' -> e2 = e2' -> e3 = e3' ->
          TIfz e1 e2 e3 = TIfz e1' e2' e3'
congIfz Refl Refl Refl = Refl

-- End: (UNTYPED) TERMS OF THE LAMBDA CALCULUS
----------------------------------------------

---------------------------------------
-- Begin: VALUES IN THE LAMBDA CALCULUS

-- The following lambda calculus terms
-- are values (i.e. normal forms for
-- reduction under the "Step" relation):
--   (1) lambda abstractions (that are
--       not applied),
--   (2) the constant 'Zero',
--   (3) the natural number constants
--       (formed by applying 'Succ' to
--       another value).
data Value : Term -> Type where
  VZero : Value TZero
  VSucc : Value e -> Value (TSucc e)
  VAbs  : Value (TAbs e)

-- End: VALUES IN THE LAMBDA CALCULUS
-------------------------------------

ext: idr

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
{--
Copyright 2021 Joel Berkeley

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
--}
||| This module contains definitions for and implementations of mean functions, particularly for
||| use in Gaussian processes.
module Model.MeanFunction

import Tensor

||| A `MeanFunction` maps a point in feature space to the mean value of a corresponding
||| distribution in target space.
|||
||| @features The shape of the feature domain.
public export 0
MeanFunction : (0 features : Shape) -> Type
MeanFunction features = {sm : _} -> Tensor (sm :: features) Double -> Tensor [sm] Double

||| A mean function where the mean is zero in all target dimensions.
export
zero : MeanFunction features
zero _ = fill 0

max_stars_repo_name: joelberkeley/spidr

max_issues_repo_name: joelberkeley/spidr

max_forks_repo_name: joelberkeley/spidr


text:
module Main

import Data.Vect
import Data.Fin

import Effects
import Effect.Exception
import Effect.StdIO
import Effect.System
import Effect.State
import Effect.Random

shiftVec : Vect 4 (Integer, Integer)
shiftVec = [(-1, 0), (0, 1), (0, -1), (1, 0)]

data Vertex : Nat -> Nat -> Type where
  MkVertex : (i : Fin n) -> (j : Fin m) -> Vertex n m

implementation Eq (Vertex n m) where
  (==) (MkVertex i j) (MkVertex q w) = i == q && j == w

data GenericEdge : Type -> Type where
  MkEdge : a -> a -> GenericEdge a

GridEdge : Nat -> Nat -> Type
GridEdge n m = GenericEdge (Vertex n m)

implementation Eq a => Eq (GenericEdge a) where
  (==) (MkEdge x y) (MkEdge u v) = x == u && y == v

implementation Show (Vertex n m) where
  show (MkVertex i j) = "[" ++ (show $ finToNat i) ++ ", " ++ (show $ finToNat j) ++ "]"

implementation Show a => Show (GenericEdge a) where
  show (MkEdge x y) = "(" ++ show x ++ ", " ++ show y ++ ")"

||| An n x m Maze is a graph.
||| It has n * m vertices.
||| Numeration goes from 0.
|||
||| Example of 1x2 maze (along with indices of rows\columns):
|||       0 1
|||         _
|||  0   |. .|
|||       _
|||
data MazeGrid : (n : Nat) -> (m : Nat) -> Type where
  Grid : (n : Nat) -> (m : Nat) -> (edges : List (GridEdge n m)) -> MazeGrid n m

DistVector : Nat -> Nat -> Type
DistVector n m = Vect (m * n + m) Integer

getEdges : MazeGrid n m -> List (GridEdge n m)
getEdges (Grid n m edges) = edges

isLT : (m : Nat) -> (n : Nat) -> Dec (LT m n)
isLT m n = isLTE (S m) n

shiftByFin : Fin n -> Fin x -> Fin (x + n)
shiftByFin {n=Z} FZ y impossible
shiftByFin {n=(S k)} {x} FZ y = weakenN (S k) y
shiftByFin {n=Z} (FS a) b impossible
shiftByFin {n=(S k)} {x} (FS a) b = rewrite sym (plusSuccRightSucc x k) in shift 1 $ shiftByFin a b

mulFin : Fin n -> (m : Nat) -> Fin (m * n)
mulFin x Z = absurd $ mulFin x Z
mulFin {n} x (S Z) = rewrite plusZeroRightNeutral n in x
mulFin {n=Z} x (S k) impossible
mulFin {n=(S t)} x (S k) = rewrite plusCommutative t (k * (S t)) in
                                   rewrite plusSuccRightSucc (k * (S t)) t in shiftByFin x (mulFin x k)

-- Every vertex is a pair (i, j), where i < n, j < m.
-- We can map pairs to natural numbers: i * m + j < (n - 1) * m + m - 1 = n * m.
vertexToFin : Vertex n m -> Fin (m * n + m)
vertexToFin {n} {m} (MkVertex i j) = shiftByFin j $ mulFin i m

reversedEdge : GridEdge n m -> GridEdge n m
reversedEdge (MkEdge u v) = MkEdge v u

whereEdgePoints : GridEdge n m -> Vertex n m
whereEdgePoints (MkEdge u v) = v

whereEdgeStarts : GridEdge n m -> Vertex n m
whereEdgeStarts (MkEdge u v) = u

rotate : Vect n a -> Nat -> Vect n a
rotate xs Z = xs
rotate {n=(S len)} (x :: xs) (S k) = rewrite plusCommutative 1 len in (rotate xs k) ++ [x]

rotateRandom : Vect n a -> Eff (Vect n a) [RND]
rotateRandom [] = pure []
rotateRandom xs = do
  idx <- rndInt 0 ((the Integer $ cast $ length xs) - 1)
  pure $ rotate xs (cast idx)

myNatToFin : (x : Nat) -> (up : Nat) -> LT x up -> Fin up
myNatToFin Z Z y impossible
myNatToFin Z (S k) y = FZ
myNatToFin (S k) Z y impossible
myNatToFin (S k) (S j) y = shift 1 $ myNatToFin k j (fromLteSucc y)

createVertex : (n : Nat) -> (m : Nat) -> (i : Nat) -> (j : Nat) ->
               {auto iOk: LT i n} ->
               {auto jOk: LT j m} ->
               Vertex n m
createVertex n m i j {iOk} {jOk} = MkVertex (myNatToFin i n iOk) (myNatToFin j m jOk)

getIthNeighbour : Vertex n m -> (i : Fin 4) -> Maybe (Vertex n m)
getIthNeighbour {n} {m} (MkVertex xFin yFin) i =
    let (dx, dy) = index i shiftVec in
    let newX = x + dx in
    let newY = y + dy in (case newX < 0 || newY < 0 of
         False => (let natNewX = the Nat $ cast newX in
                   let natNewY = the Nat $ cast newY in (case isLT natNewX n of
                               (Yes prfX) => (case isLT natNewY m of
                                                  (Yes prfY) => Just $ createVertex n m _ _ {iOk=prfX} {jOk=prfY}
                                                  (No contra) => Nothing)
                               (No contra) => Nothing))
         True => Nothing)
    where x : Integer
          x = the Integer $ cast $ finToNat xFin
          y : Integer
          y = the Integer $ cast $ finToNat yFin

neighbours : Vertex n m -> List (Vertex n m)
neighbours v = catMaybes [ getIthNeighbour v i | i <- [FZ, FS FZ, FS $ FS FZ, FS $ FS $ FS FZ] ]

neighboursInGrid : Vertex n m -> MazeGrid n m -> List (Vertex n m)
neighboursInGrid x (Grid n m edges) = map whereEdgePoints $ filter (\edge => (whereEdgeStarts edge) == x) edges

genEdgesFromVertex : Vertex n m -> (p : Nat ** (Vect p (GridEdge n m)))
genEdgesFromVertex v = (_ ** fromList [ MkEdge v u | u <- neighbours v])

edgeNotPontsToAnyVertex : GridEdge n m -> List (Vertex n m) -> Bool
edgeNotPontsToAnyVertex (MkEdge x y) xs = not $ Prelude.List.elem y xs

-- already added vertices -> list of unprocessed edges -> list of resulting edges
genEdges : List (Vertex n m) -> Vect len (GridEdge n m) -> Eff (List (GridEdge n m)) [RND, STDIO]
genEdges _ [] = pure []
genEdges {len=(S r)} addedVertices edgesPool = do
    edgesRotated <- rotateRandom edgesPool
    let (chosenEdge :: remainingPool) = edgesRotated
    pure (chosenEdge :: (reversedEdge chosenEdge) ::
      !(genEdges (calcNewVertices addedVertices chosenEdge) (snd $ calcNewEdgesPool remainingPool chosenEdge addedVertices)))

  where calcNewVertices : List (Vertex n m) -> GridEdge n m -> List (Vertex n m)
        calcNewVertices xs (MkEdge x y) = y :: xs

        calcNewEdgesPool : Vect len1 (GridEdge n m) -> GridEdge n m -> List (Vertex n m) -> (p : Nat ** Vect p (GridEdge n m))
        calcNewEdgesPool pool (MkEdge fr to) vertices =
          let newEdges = snd $ filter (\edge => edgeNotPontsToAnyVertex edge vertices) (snd $ genEdgesFromVertex to) in
          let filteredOldEdges = snd $ filter (\edge => (whereEdgePoints edge) /= to) pool in
              (_ ** (newEdges ++ filteredOldEdges))

generateGrid : (n : Nat) -> (m : Nat) -> LT 0 n -> LT 0 m -> Eff (MazeGrid n m) [RND, STDIO]
generateGrid n m prfN prfM = do
    edgeList <- genEdges [initialVertex] $ snd $ genEdgesFromVertex initialVertex
    pure $ Grid n m edgeList
  where initialVertex : Vertex n m
        initialVertex = createVertex n m 0 0 {iOk=prfN} {jOk=prfM}

bfs : MazeGrid n m -> List (Vertex n m) -> Effects.SimpleEff.Eff (DistVector n m) [STATE (DistVector n m)]
bfs _ [] = get
bfs gr@(Grid n m edges) (x :: xs) = do
    curDist <- get
    let unvisitedNeighbours = filter (\vert => (index (vertexToFin vert) curDist) == -1) $ neighboursInGrid x gr
    update $ updUnvisited ((index (vertexToFin x) curDist) + 1) unvisitedNeighbours
    bfs gr (xs ++ unvisitedNeighbours)
  where updUnvisited : Integer -> List (Vertex n m) -> DistVector n m -> DistVector n m
        updUnvisited x [] y = y
        updUnvisited x (z :: xs) y = updUnvisited x xs (updateAt (vertexToFin z) (const x) y)

getDistFrom : MazeGrid n m -> Vertex n m -> DistVector n m
getDistFrom {n} {m} grid v = runPureInit [genInitialList] $ bfs grid [v]
    where genInitialList : DistVector n m
          genInitialList = updateAt (vertexToFin v) (const 0) $ replicate (m * n + m) (-1)

parseDimension : Integer -> Eff ((n : Nat ** LT 0 n)) [EXCEPTION String]
parseDimension x = case isLT 0 xNat of
                        (Yes prf) => pure (xNat ** prf)
                        (No contra) => raise ("Invalid maze dimension " ++ show x)
    where xNat : Nat
          xNat = the Nat $ cast x

printMaze : MazeGrid n m -> Vertex n m -> Vertex n m -> DistVector n m -> DistVector n m -> Integer -> Eff () [STDIO]
printMaze (Grid n m edges) start end distFromStart distFromEnd distStartToEnd = printRow 0
    where printRow : Nat -> Eff () [STDIO]
          printRow rowIdx =
              case isLT rowIdx n of
                  (Yes prfRow) => do
                      printColAtRow 0 rowIdx prfRow
                      printColBetweenRows 0 rowIdx prfRow
                      printRow (rowIdx + 1)
                  (No contra) => putStrLn "End"
            where printColBetweenRows : Nat -> (row : Nat) -> LT row n -> Eff () [STDIO]
                  printColBetweenRows colIdx rowIdx prfRow =
                      case isLT (S rowIdx) n of
                          (Yes prfRowNext) => (case isLT colIdx m of
                                                (Yes prfCol) => do
                                                  let curVert = createVertex n m rowIdx colIdx {iOk=prfRow} {jOk=prfCol}
                                                  let nextVert = createVertex n m (S rowIdx) colIdx {iOk=prfRowNext} {jOk=prfCol}
                                                  putChar (if elem (MkEdge curVert nextVert) edges then ' ' else '_')
                                                  putChar '|'
                                                  printColBetweenRows (colIdx + 1) rowIdx prfRow
                                                (No contra) => putChar '\n')
                          (No contra) => pure ()

                  printColAtRow : Nat -> (row : Nat) -> LT row n -> Eff () [STDIO]
                  printColAtRow colIdx rowIdx prfRow =
                      case isLT colIdx m of
                           (Yes prfCol) => do
                             putChar (decideCellCharacter prfCol)
                             let curVertex = createVertex n m rowIdx colIdx {iOk=prfRow} {jOk=prfCol}
                             case isLT (S colIdx) m  of
                                  (Yes prfNextCol) => do
                                    let nextVertex = createVertex n m rowIdx (S colIdx) {iOk=prfRow} {jOk=prfNextCol}
                                    putChar (if elem (MkEdge curVertex nextVertex) edges then ' ' else '|')
                                  (No contra) => pure ()
                             printColAtRow (S colIdx) rowIdx prfRow
                           (No contra) => putChar '\n'
                      where decideCellCharacter : LT colIdx m -> Char
                            decideCellCharacter prfCol =
                              let curVertex = createVertex n m rowIdx colIdx {iOk=prfRow} {jOk=prfCol} in
                              let distToStart = index (vertexToFin curVertex) distFromStart in
                              let distToEnd = index (vertexToFin curVertex) distFromEnd
                              in
                                  if curVertex == start then 'S'
                                  else if curVertex == end then 'E'
                                  else
                                    if distStartToEnd == distToStart + distToEnd
                                    then 'o'
                                    else '.'

genProvableBoundedNat : (m : Nat) -> Eff ((n : Nat ** LT n m)) [RND, EXCEPTION String]
genProvableBoundedNat m = let nNat = the Nat $ cast $ !(rndInt 0 ((the Integer $ cast m) - 1)) in
                              case isLTE (S nNat) m of
                               (Yes prf) => pure (nNat ** prf)
                               (No contra) => raise "Number generated by rndInt was not in bounds"

lteMinusPrf : (n : Nat) -> LT 0 n -> LT (minus n 1) n
lteMinusPrf n nPrf with (nPrf)
  lteMinusPrf (S right) nPrf | (LTESucc x) = rewrite minusZeroRight right in lteRefl

-- debug output
printAligned : Show a => Nat -> Nat -> List a -> Eff () [STDIO]
printAligned n m [] = putChar '\n'
printAligned n m (x :: xs) = do
  if (((Prelude.List.length xs) + 1) `mod` m) == 0
     then putChar '\n'
     else pure ()
  putStr $ show x
  putChar ' '
  printAligned n m xs

generatePrintMaze : Eff () [STDIO, SYSTEM, RND, EXCEPTION String]
generatePrintMaze = do
  [prog, nStr, mStr] <- getArgs | [] => putStrLn "Can't happen"
                          | [prog] => putStrLn "No arguments"
                          | [prog, n] => putStrLn "Not enough arguments"
                          | _ => putStrLn "Too many arguments"

  (n ** nPrf) <- parseDimension (the Integer $ cast nStr)
  (m ** mPrf) <- parseDimension (the Integer $ cast mStr)

  t <- time
  srand t

  grid <- generateGrid n m nPrf mPrf

  (enterColumn ** enterColumnPrf) <- genProvableBoundedNat m
  let startVertex = createVertex n m 0 enterColumn {jOk=enterColumnPrf}
  (exitColumn ** exitColumnPrf) <- genProvableBoundedNat m
  let endVertex = createVertex n m (n - 1) exitColumn {jOk=exitColumnPrf} {iOk=lteMinusPrf n nPrf}

  let distFromStart = getDistFrom grid startVertex
  let distFromEnd = getDistFrom grid endVertex
  let distStartToEnd = index (vertexToFin endVertex) distFromStart

  printMaze grid startVertex endVertex distFromStart distFromEnd distStartToEnd
  pure ()

main : IO ()
main = run generatePrintMaze

max_stars_repo_name: ItsLastDay/idris-a-mazing

max_issues_repo_name: ItsLastDay/idris-a-mazing

max_forks_repo_name: ItsLastDay/idris-a-mazing


text:
module Commons.Text.Lexer.Test

import Text.PrettyPrint.WL
import Text.Lexer

import Commons.Data.Location
import Commons.Text.Lexer.Run

%default total
%access export

data TestReport : Type -> Type where
  ExpectedSuccess : (title : String) -> TestReport a

  Failure : (Eq a, Show a)
         => (title : String)
         -> (input : String)
         -> LexError
         -> TestReport a

  UnexpectedSuccess : (Eq a, Show a)
                   => (title, input : String)
                   -> (given : List (TokenData a))
                   -> TestReport a

  FailureCmp : (Eq a, Show a)
            => (title, input : String)
            -> (given, expected : List (TokenData a))
            -> TestReport a

isSuccess : TestReport a -> Bool
isSuccess (ExpectedSuccess _) = True
isSuccess _ = False

lexerTest : (Eq a, Show a)
         => (title : String)
         -> (lex   : String -> Either LexError (List (TokenData a)))
         -> (input : String)
         -> TestReport a
lexerTest t l i =
  case l i of
    Left err => Failure t i err
    Right ts => ExpectedSuccess t

lexerTestNot : (Eq a, Show a)
            => (title : String)
            -> (lex   : String -> Either LexError (List (TokenData a)))
            -> (input : String)
            -> TestReport a
lexerTestNot t l i =
  case l i of
    Left err => ExpectedSuccess t
    Right ts => UnexpectedSuccess t i ts

lexerTestAssert : (Eq a, Show a)
            => (title : String)
            -> (lex   : String -> Either LexError (List (TokenData a)))
            -> (input : String)
            -> (expected : List (TokenData a))
            -> TestReport a
lexerTestAssert t l i e =
  case l i of
    Right ts =>
      if map tok ts == map tok e
        then ExpectedSuccess t
        else FailureCmp t i ts e

    Left err => Failure t i err

showReport : Show a => TestReport a -> Doc
showReport (ExpectedSuccess t) = text "[PASS]" <+> text t
showReport (Failure t i err) =
  vcat [ text "[FAIL]" <+> text t
       , indent 2 $ text "This input:"
       , indent 4 $ text i
       , indent 2 $ text "gave this error:"
       , indent 4 $ (text . show) err]
showReport (UnexpectedSuccess t i g) =
   vcat [ text "[FAIL] [RESULT]" <+> text t
       , indent 2 $ text "This input:"
       , indent 4 $ text i
       , indent 2 $ text "unexpectedly gave this result:"
       , indent 4 $ list (map (text . show . tok) g)
       ]

showReport (FailureCmp t i g e) =
  vcat [ text "[FAIL]" <+> text t
       , indent 2 $ text "Expected to lex:"
       , indent 4 $ list (map (text . show . tok) e)
       , indent 2 $ text "But gave this:"
       , indent 4 $ list (map (text . show . tok) g)]

runLexTest : Show a => TestReport a -> IO Bool
runLexTest r = do putStrLn ((toString . showReport) r)
                  pure (isSuccess r)

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module IdrisJvm.System

import public Data.So
import IdrisJvm.IO
import Java.Util
import Java.Math
import Java.Lang

public export
getArgs : JVM_IO (List String)
getArgs = do
    argsList <- invokeStatic RuntimeClass "getProgramArgs" (JVM_IO JList)
    Iterator.toList !(JList.iterator argsList)

public export
time : JVM_IO Integer
time = believe_me <$> invokeStatic RuntimeClass "time" (JVM_IO BigInteger)

public export
getEnv : String -> JVM_IO (Maybe String)
getEnv = System.getenv

public export
system : String -> JVM_IO Int
system = invokeStatic RuntimeClass "runCommand" (String -> JVM_IO Int)

public export
usleep : (i : Int) -> { auto prf : So (i >= 0 && i <= 1000000) } -> JVM_IO ()
usleep interval = invokeStatic RuntimeClass "usleep" (Int -> JVM_IO ()) interval

public export
exit : Int -> JVM_IO a
exit = believe_me . Java.Lang.System.exit

max_stars_repo_name: alaendle/idris-jvm

max_issues_repo_name: alaendle/idris-jvm

max_forks_repo_name: alaendle/idris-jvm


text:
module Minecraft.Base.PreClassic.GrassBlock.ItemEntity

import public Minecraft.Base.PreClassic.GrassBlock
import public Minecraft.Core.Entity.Pickup.Export
import public Minecraft.Data.Type.Vtbl

%default total

namespace Export
  public export %hint grassBlockItemEntity : Pickup GrassBlock.ItemEntity
  public export %hint grassBlockVtbl       : Vtbl   GrassBlock.ItemEntity

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module Data.Compress.Utils.FiniteBuffer

import Data.Seq.Unsized

export
record FiniteBuffer a where
  constructor FB
  max_size : Int
  size : Int
  buffer : Seq a

export
empty : Nat -> FiniteBuffer a
empty n = FB (cast n) 0 empty

export
take_last : Nat -> FiniteBuffer a -> Maybe (List a)
take_last n fb = guard (cast n <= fb.size) $> (toList $ take n $ drop (cast (fb.size - cast n)) fb.buffer)

infixr 5 +<
infixr 5 +<><

export
(+<) : FiniteBuffer a -> a -> FiniteBuffer a
(FB max_size size buffer) +< x =
  let
    len = size + 1
    buf = snoc buffer x
  in
    if len > max_size then FB max_size max_size $ tail buf else FB max_size len buf

export
(+<><) : Foldable f => FiniteBuffer a -> f a -> FiniteBuffer a
buf +<>< elems = foldl (+<) buf elems

export
length : FiniteBuffer a -> Nat
length = cast . size


text:
import Control.Monad.Either
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Writer

record Unlift (0 t : (Type -> Type) -> Type -> Type) where
  constructor MkUnlift
  unlifter : forall n, a. Monad n => t n a -> n a

-- inlining `Unlift` type to its the only field make the code to not to typecheck somewhy O_O

interface MonadTransUnlift t where
  askUnlift : Monad m => t m $ Unlift t

MonadTransUnlift (ReaderT r) where
  askUnlift = MkReaderT $ \r => pure $ MkUnlift $ runReaderT r

-- those below are somewhat bad...

MonadTransUnlift (StateT s) where
  askUnlift = ST $ \s => pure (s, MkUnlift $ evalStateT s)

Monoid w => MonadTransUnlift (WriterT w) where
  askUnlift = MkWriterT $ \w => pure (MkUnlift $ map fst . runWriterT, w)

MonadTransUnlift (EitherT e) where
  askUnlift = MkEitherT $ pure $ Right $ MkUnlift $ ?foo

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Sortable

%default total
%access private

public export
interface Sortable (s : Type -> Type) where
  empty : Ord a => s a
  add : Ord a => a -> s a -> s a
  sort : Ord a => s a -> List a


text:
module Parser.Source

import public Parser.Lexer.Source
import public Parser.Rule.Source
import public Parser.Unlit

import Core.Core
import Core.Name
import Core.Metadata
import Core.FC

import System.File

%default total

export
runParserTo : {e : _} ->
              (origin : OriginDesc) ->
              Maybe LiterateStyle -> Lexer ->
              String -> Grammar State Token e ty ->
              Either Error (List Warning, State, ty)
runParserTo origin lit reject str p
    = do str        <- mapFst (fromLitError origin) $ unlit lit str
         (cs, toks) <- mapFst (fromLexError origin) $ lexTo reject str
         (decs, ws, (parsed, _)) <- mapFst (fromParsingErrors origin) $ parseWith p toks
         let cs : SemanticDecorations
                = cs <&> \ c => ((origin, start c, end c), Comment, Nothing)
         let ws = ws <&> \ (mb, warn) =>
                    let mkFC = \ b => MkFC origin (startBounds b) (endBounds b)
                    in ParserWarning (maybe EmptyFC mkFC mb) warn
         Right (ws, { decorations $= (cs ++) } decs, parsed)

export
runParser : {e : _} ->
            (origin : OriginDesc) -> Maybe LiterateStyle -> String ->
            Grammar State Token e ty ->
            Either Error (List Warning, State, ty)
runParser origin lit = runParserTo origin lit (pred $ const False)

export covering
parseFile : (fname : String)
         -> (origin : OriginDesc)
         -> Rule ty
         -> IO (Either Error (List Warning, State, ty))
parseFile fname origin p
    = do Right str <- readFile fname
             | Left err => pure (Left (FileErr fname err))
         pure (runParser origin (isLitFile fname) str p)


text:
import Data.Buffer

%default total

public export
interface Singleton (n : Nat) where
  sing : (m : Nat ** m === n)
  sing = (n ** Refl)

Singleton 3 where
Singleton 5 where

export
data ForeignPtr : Type -> Type where
  MkFP : Buffer -> ForeignPtr a

public export
interface Storable (0 a : Type) (n : Nat) | a where
  constructor MkStorable
  peekByteOff : HasIO io => ForeignPtr a -> Int -> io a

  peekElemOff : HasIO io => ForeignPtr a -> Int -> io a
  peekElemOff fp off = peekByteOff fp (off * cast n)

Storable Bits8 8 where
  peekByteOff (MkFP b) off = getBits8 b off


text:
module Python.Lib.Numpy.Matrix

import Python
import Python.Prim
import Python.Lib.Numpy

import Data.Vect

%access public export
%default total

-- private
np : Obj Numpy
np = unsafePerformIO Numpy.import_

-- private
nda : Obj NDArrayT
nda = np /. "ndarray"

record DType (ty : Type) where
  constructor MkDType
  dtName : String
  dtFromInteger : Integer -> ty
  dtFromDouble   : Double -> ty

DDouble : DType Double
DDouble = MkDType "float" fromInteger id

-- abstract
record Matrix (rows : Nat) (cols : Nat) (dtype : DType a) where
  constructor MkM
  arr : Obj NDArray

-- private
unsafeNp : PIO (Obj NDArray) -> Matrix r c dt
unsafeNp = MkM . unsafePerformIO

-- private
op : (f : String)
  -> {auto pf : NDArrayT f = [Obj NDArray, Obj NDArray] ~~> Obj NDArray}
  -> Matrix r c dt -> Matrix r c dt -> Matrix r c dt
op f (MkM x) (MkM y) = unsafeNp $ nda /. f $. [x, y]

-- abstract
fill : {dt : DType a} -> a -> Matrix r c dt
fill {r=r} {c=c} x = unsafeNp $ np /. "tile" $. [toDyn x, (r,c)]

fromInteger : Integer -> Matrix r c dt
fromInteger {dt=dt} = fill . dtFromInteger dt

fromDouble : Double -> Matrix r c dt
fromDouble {dt=dt} = fill . dtFromDouble dt

-- abstract
singleton : {dt : DType a} -> a -> Matrix 1 1 dt
singleton {a=a} {dt=dt} x =
  unsafeNp $
    np //. FP "array" a $. [pyList [pyList [x]], dtName dt]

-- abstract
dot : Matrix r c dt -> Matrix c k dt -> Matrix r k dt
dot (MkM x) (MkM y) = unsafeNp $ np /. "dot" $. [x,y]

-- abstract
transpose : Matrix r c dt -> Matrix c r dt
transpose (MkM x) = unsafeNp $ np /. "transpose" $. [x]

-- abstract
array : (dt : DType a) -> Vect r (Vect c a) -> Matrix r c dt
array {a=a} dt xs = unsafeNp $ np //. FP "array" a $. [c (map c xs), dtName dt]
  where
    c : {a : Type} -> Vect n a -> Obj (PyList a)
    c xs = pyList $ toList xs

-- abstract
reshape : Matrix r c dt -> {auto pf : r*c = r'*c'} -> Matrix r' c' dt
reshape {r'=r'} {c'=c'} (MkM x) =
  unsafeNp $
    np /. "reshape" $. [x, (r', c')]

-- abstract
(/) : Matrix r c dt -> Matrix r c dt -> Matrix r c dt
(/) = op "__div__"

-- abstract
minus : Matrix r c dt -> Matrix r c dt -> Matrix r c dt
minus = op "__sub__"

-- abstract
abs : Matrix r c dt -> Matrix r c dt
abs (MkM x) = unsafeNp $ np /. "abs" $. [x]

implementation Num (Matrix r c dt) where
  (+) = op "__add__"
  (*) = op "__mul__"
  fromInteger = Matrix.fromInteger

implementation Show (Matrix r c dt) where
  show (MkM x) = unsafePerformIO $ x /. "__str__" $. []

max_stars_repo_name: ziman/idris-py

max_issues_repo_name: ziman/idris-py

max_forks_repo_name: ziman/idris-py


text:
module Replica.Command.Help

import Data.List
import Data.List1

import Replica.Command.Info
import Replica.Command.Run
import public Replica.Help
import Replica.Option.Types
import Replica.Other.Validation

export
help : Help
help = MkHelp
  "replica"
  (Just "replica COMMAND [COMMAND_OPTIONS]")
  "Integration testing for command line interfaces"
  [ ("Commands", helpRun ::: [helpInfo])
  ]
  (Just "Run 'replica help COMMAND' for more information on a command.")

export
parseHelp : List1 String -> ParseResult Help
parseHelp ("help" ::: []) = Done help
parseHelp ("help" ::: [command]) = maybe
  (InvalidMix "Help unavailable, \{show command} is not a valid command")
  Done $ do
    commands <- "Commands" `lookup` help.chapter
    lookup command $ map (\h => (h.name, h)) $ forget commands
parseHelp ("help" ::: xs) = InvalidMix $ "Too many arguments for help"
parseHelp xs = InvalidOption xs

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica


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

data Elem : a -> Vect k a -> Type where
    Here : Elem x (x :: xs)
    There : (later : Elem x xs) -> Elem x (y :: xs)

notInNil : Elem value [] -> Void
notInNil Here impossible
notInNil (There _) impossible

notInTail : (notHere : (value = x) -> Void) -> (notThere : Elem value xs -> Void) -> Elem value (x :: xs) -> Void
notInTail notHere notThere Here = notHere Refl
notInTail notHere notThere (There later) = notThere later

isElem : DecEq a => (value : a) -> (xs : Vect n a) -> Dec (Elem value xs)
isElem value [] = No notInNil
isElem value (x :: xs) =
    case decEq value x of
        Yes Refl => Yes Here
        No notHere =>
            case isElem value xs of
                Yes prf => Yes (There prf)
                No notThere => No (notInTail notHere notThere)


text:
{-
 SnocList and fast reverse examples from 10.2.1 and 10.2.2
 "snoc" == reverse "cons"
 The book claims linear cost but my experiments suggest quadratic.
 I think the cost of snocListHelp append proofs causes it.
-}

module Part2.Sez10_2a_snoc

%default total

public export
data SnocList : List a -> Type where
     Empty : SnocList []
     Snoc : (rec : SnocList xs) -> SnocList (xs ++ [x])

export
snocList : (xs : List a) -> SnocList xs

snocListHelp : (snoc : SnocList input) -> (rest : List a) ->
               SnocList (input ++ rest)
snocListHelp {input} snoc [] = rewrite appendNilRightNeutral input in snoc
snocListHelp {input} snoc (x :: xs) = rewrite appendAssociative input [x] xs in
                     snocListHelp (Snoc snoc {x}) xs

snocList xs = snocListHelp Empty xs

||| reverse based on SnocList view, implementation that avoids using Helper function
export
myReverse : List a -> List a
-- with argument is not recreated in recursive step
myReverse input with (snocList input)
  myReverse [] | Empty = []
  myReverse (xs ++ [x]) | (Snoc rec) = x :: myReverse xs | rec -- passed with argument

test1 : List Int
test1 = myReverse [1..50]

test2 : List Int
test2 = myReverse [1..100]

{-
idris repl:
*Part2/Sec10_2a> myReverse [1..10]
[10, 9, 8, 7, 6, 5, 4, 3, 2, 1] : List Integer
*Part2/Sec10_2a> :t appendNilRightNeutral
appendNilRightNeutral : (l : List a) -> l ++ [] = l
*Part2/Sec10_2a> :t appendAssociative
appendAssociative : (l : List a) ->
                    (c : List a) -> (r : List a) -> l ++ c ++ r = (l ++ c) ++ r
-}

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes


text:
module equality

import Data.Vect

-- 8.1.7 Exercises
same_cons : {xs : List a}
            -> {ys : List a}
            -> xs = ys
            -> x :: xs = x :: ys
same_cons Refl = Refl

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

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

-- Functions as Proofs: Manipulating Equalities
sameS : (k : Nat) -> (j : Nat) -> (eq : EqNat k j) -> EqNat (S k) (S j)
sameS j j (Same j) = Same (S j)

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

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

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

reverseProof : Vect (k + 1) elem -> Vect (S k) elem
reverseProof {k} ys = rewrite plusCommutative 1 k in ys

my_reverse : Vect n elem -> Vect n elem
my_reverse [] = []
my_reverse (x :: xs) = reverseProof (my_reverse xs ++ [x])


text:
module Der

import Generics.Derive

import Language.Reflection.Derive

%language ElabReflection

data X = A | B Int

%runElab derive "X" [Generic]

record Y (a : Type) (p : a -> Type) where
  constructor MkX
  x : a
  s : p x

-- %runElab derive "Y" [Generic]

Generic (Y a p) [[a, ?dependent]] where


text:
import Js.ASync

tst : String
tst =
  let x = ("stra", "strb")
      (y,z) = x
  in y

main : JS_IO ()
main = do
  putStr' $ show tst

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
namespace A
  export
  x : Bool -> Bool
  x = not

namespace B
  export
  x : Nat -> Bool
  x Z = True
  x _ = False

%ambiguity_depth 1000

-- There's an undefined name very deep here - if we don't take a shortcut,
-- this shows all the ambiguous branches with the undefined named!
test : Nat -> Bool
test val
    = x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
      x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ va


text:
module Extra.Nat

import Data.Fin
import Data.Nat
import Data.Nat.Equational
import Data.Nat.Division

||| Subtract a `Nat` by a `Fin`
public export
subtract : (n : Nat) -> Fin (S n) -> Nat
subtract n FZ = n
subtract (S n) (FS k) = subtract n k

||| `Data.Nat.lteRefl` but different symbols
public export
lteAsymRefl : {a, b : Nat} -> a = b -> LTE a b
lteAsymRefl Refl = lteRefl

||| Proof of forall a, b where b /= 0, a/b <= a
public export
divNatNZLteNumer : (numer : Nat) -> (denom : Nat) -> (prf : Not (denom = 0)) -> LTE (divNatNZ numer denom prf) numer
divNatNZLteNumer a Z prf = void $ prf Refl
divNatNZLteNumer a (S b) prf =
  let lte1 = lteAddRight {m = (snd (divmodNatNZ a (S b) prf))} (mult (fst (divmodNatNZ a (S b) prf)) (S b)) in
  let a1 = lteAsymRefl $ sym (DivisionTheoremDivMod a (S b) prf) in
  let a2 = lteTransitive lte1 (rewrite plusCommutative (mult (fst (divmodNatNZ a (S b) prf)) (S b)) (snd (divmodNatNZ a (S b) prf)) in a1) in
  let lte2 = leftFactorLteProduct (fst (divmodNatNZ a (S b) prf)) b in
  let a3 = lteTransitive lte2 a2 in
  rewrite sym $ fstDivmodNatNZeqDiv a (S b) prf prf in a3


text:
module Country

public export
record Country where
  constructor CreateCountry
  id : Integer
  title : String

max_stars_repo_name: GrandArchTemplar/IdrisVKAPI

max_issues_repo_name: GrandArchTemplar/IdrisVKAPI

max_forks_repo_name: GrandArchTemplar/IdrisVKAPI


text:
||| Interfaces of basic containers.
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module Data.Container.Interfaces

import Data.Maybe

%default total

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

namespace Immutable

  public export
  interface Container a where
    0 KeyTy : Type
    null     : a -> Bool
    count    : a -> Nat
    contains : KeyTy -> a -> Bool
    delete   : KeyTy -> a -> a

  namespace Set
    public export
    interface Container a => Set a where
      0 KeyTy : Type
      insert   : KeyTy -> a -> a

  namespace Map
    public export
    interface Container a => Map a where
      0 KeyTy : Type
      0 ValTy : Type
      lookup   : KeyTy -> a -> Maybe ValTy
      insert   : KeyTy -> ValTy -> a -> a

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

namespace Mutable

  public export
  interface MutableContainer m a where
    0 KeyTy : Type
    null     : a -> m Bool
    count    : a -> m Nat
    contains : KeyTy -> a -> m Bool
    delete   : KeyTy -> a -> m ()

  namespace Set
    public export
    interface MutableContainer m a => MutableSet m a where
      0 KeyTy : Type
      insert   : KeyTy -> a -> m ()

  namespace Map
    public export
    interface MutableContainer m a => MutableMap m a where
      0 KeyTy : Type
      0 ValTy : Type
      lookup   : KeyTy -> a -> m (Maybe ValTy)
      insert   : KeyTy -> ValTy -> a -> m ()

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


text:
module Main

import Core.Name.Namespace
import Core.Options
import Core.Context
import Compiler.Common
import Core.CompileExpr
import Compiler.ANF
import Compiler.VMCode
import Idris.Driver
import Data.List
import Data.String
import Data.Vect
import Data.Either
import Data.SortedSet
import Data.SortedMap
import Protocol.Hex
import System
import System.File
import Libraries.Utils.Path
import CommonDef
import CairoCode.CairoCode
import CairoCode.CairoCodeUtils
import CairoCode.Traversal.Base
import CodeGen.CodeGen
import CodeGen.CurryingBasedClosures

import CodeGen.RegAlloc
import Optimisation.DeadCodeElimination
import Optimisation.DeadArgumentEliminator
import Optimisation.StaticProcessing.StaticTransformer
import Optimisation.GlobalStaticOptimizer
import Optimisation.Inliner
import Optimisation.OrderAndEliminateDefinitions

import Optimisation.Untupling
import CodeGen.InjectLinearImplicits
import RewriteRules.EqChainInline
import Primitives.Primitives

import Debug.Trace

generateMainCall : CairoDef -> CairoReg -> CairoReg -> List CairoInst
generateMainCall (FunDef [_] _ [_] _) resReg stateReg = [CALL [resReg] empty cairo_main [stateReg]]
generateMainCall (FunDef Nil _ [_] _) resReg stateReg = [CALL [reg 0] empty cairo_main [], APPLY resReg empty (reg 0) stateReg]
    where reg : Int -> CairoReg
          reg i = Unassigned (Just "main_call") i 0
generateMainCall _ _ _ = assert_total $ idris_crash "Unsupported Main signature"

genericEntryDef : LinearImplicit -> CairoDef -> (Name, CairoDef)
genericEntryDef io_implicit main_def = (entry_name, FunDef [] (singleton io_implicit io_ptr_reg) [] body)
    where
          io_ptr_reg : CairoReg
          io_ptr_reg = implicitReg io_implicit
          reg : Int -> CairoReg
          reg i = Unassigned (Just "main") i 0
          body : List CairoInst
          {- Version without new type optimisation
          body = ((MKCON (reg 0) Nothing [io_ptr_reg])::(generateMainCall main_def (reg 1) (reg 0))) ++ [
              (PROJECT (reg 2) (reg 1) 0),
              (PROJECT (reg 3) (reg 2) 0),
              (RETURN [] (singleton io_implicit (reg 3)))
            ]
          -}
          -- new type optimized version (because Cairo Monad has only 1 field at the moment (output_ptr)
          body = (generateMainCall main_def (reg 0) (io_ptr_reg)) ++ [
            (PROJECT (reg 1) (reg 0) 0),
            (RETURN [] (singleton io_implicit (reg 1)))
          ]

-- Note: we treat output_ptr as implicit only to ensure that the parameter order and names ends up correctly
--       This is ok as this is the entry point (which has a fixed signature) and no one has to provide output_ptr implicitly
entryDef : CairoDef -> (Name, CairoDef)
entryDef = genericEntryDef output_builtin

entryDefStarknet : CairoDef -> (Name, CairoDef)
entryDefStarknet = genericEntryDef syscall_builtin

-- Debuging helper Phases
trace_code_selective : ((Name, CairoDef) -> Bool) -> CairoCodePass
trace_code_selective fn cairocode = trace (show (filter fn cairocode)) cairocode

trace_code : CairoCodePass
trace_code cairocode = trace_code_selective (\_ => True) cairocode

-- Compilation Phases
parse_anf_code : List (Name, ANFDef) -> Core (List (Name, CairoDef))
parse_anf_code anfcode = map concat (traverse fromANFDef anfcode)

addRequiredPrimFnHelpers : CairoCodePass
addRequiredPrimFnHelpers cairocode = cairocode ++ findPrimFnDeps cairocode

{-
replace_primfns : CairoCodePass
replace_primfns cairocode = snd $ runVisitTransformCairoDefs (pureTraversal rewritePrimFns) cairocode
    where rewritePrimFns : InstVisit CairoReg -> List (InstVisit CairoReg)
          rewritePrimFns inst@(VisitOp res linearImplicits (Add Bits8Type) args) = fromCairoInsts $ generatePrimFnCode (Add Bits8Type) res args linearImplicits
          rewritePrimFns inst = [inst]
-}

eliminate_unused_and_order_topological : CairoCodePass
eliminate_unused_and_order_topological cairocode = orderUsedDefs entry_name cairocode

eq_chain_inline : CairoCodePass
eq_chain_inline cairocode = eqChainInline cairocode

tupled_returns : CairoCodePass
tupled_returns cairocode = untupling cairocode

implicit_injection : CairoCodePass
implicit_injection cairocode = injectLinearImplicitsDefs cairocode

constant_folding : CairoCodePass
constant_folding cairocode = localStaticOptimizeDefs cairocode

dead_code_eliminator : CairoCodePass
dead_code_eliminator cairocode = map eliminateDeadCode cairocode

data CleanupMode : Type where
     Full : CleanupMode
     Partial : CleanupMode
     Essential : CleanupMode

cleanup : CleanupMode -> CairoCodePass
cleanup Full cairocode = dead_code_eliminator $ constant_folding $ eliminate_unused_and_order_topological cairocode
cleanup Partial cairocode = dead_code_eliminator $ constant_folding cairocode
cleanup Essential cairocode = map orderUnassignedRegIndexes cairocode

global_constant_folding : CairoCodePass
global_constant_folding cairocode = globalStaticOptimize entry_name cairocode

inlining_temporary : CairoCodePass
inlining_temporary cairocode = inlineDefs entry_name cairocode

dead_argument_eliminator : CairoCodePass
dead_argument_eliminator cairocode = eliminateDeadArgumentsDefs cairocode

closure_gen : CairoCodePass
closure_gen cairocode = preprocessClosures cairocode

allocate_registers : CairoCodePass
allocate_registers cairocode = reverse (snd (foldl allocateCairoDef (empty, []) cairocode))
     where allocateCairoDef : (SortedSet Name, List (Name, CairoDef)) -> (Name, CairoDef) -> (SortedSet Name, List (Name, CairoDef))
           allocateCairoDef (safeCalls, acc) (name, cairodef) = let (ncdef, newSafeCalls) = allocateCairoDefRegisters safeCalls (name, cairodef) in (newSafeCalls , (name,ncdef)::acc)

generate_code : Bool -> List (Name, CairoDef) -> String
generate_code isLib cairocode = generateCairoCode isLib entry_name cairocode

{-
debug : List (Name, CairoDef) -> List String
debug strs = strs >>= extract
    where extract : (Name, CairoDef) -> List String
          extract (name, ForeignDef (MkForeignInfo True _ _ _) _ _) = [cairoName name]
          extract _ = []
-}

executePhase : Bool -> List (Name, CairoDef) -> (String, CairoCodePass) -> IO (List (Name, CairoDef))
executePhase isVerbose cairocode (phaseName, phaseFunction) = do
  when isVerbose $ putStrLn phaseName
  pure $ phaseFunction cairocode

compile : Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) -> ClosedTerm -> (outfile : String) -> Core (Maybe String)
compile defs tmpDir outputDir term outfile =
  do
     ds <- getDirectives (Other "cairo")
     let isStarknetLib = elem "starknetlib" ds
     let isVerbose = elem "verbose" ds

     cd <- getCompileData False ANF term
     -- Compile ANF to CairoCode
     blank_cairocode <- parse_anf_code cd.anf
     let main_def = fromMaybe (assert_total $ idris_crash "Cairo main is missing") (lookup	cairo_main blank_cairocode)
     let cairocode = (if isStarknetLib then (entryDefStarknet main_def) else (entryDef main_def))::blank_cairocode

     -- config
     let phases: List (String,CairoCodePass) = [
          -- Prepare Section & Initial Pass Section
          ("eliminate_unused_and_order_topological", eliminate_unused_and_order_topological),
          ("global_constant_folding", global_constant_folding), -- includes a local constant folding pass
          ("dead_argument_eliminator", dead_argument_eliminator), -- includes a dead code elimination pass
          ("dead_code_eliminator", dead_code_eliminator),
          ("eliminate_unused_and_order_topological", eliminate_unused_and_order_topological),
          -- Common Pattern Rewrites Section --
          ("eq_chain_inline", eq_chain_inline),
          ("partial_cleanup", cleanup Partial),
          -- Inlining Section
          ("inlining_temporary", inlining_temporary),
          ("full_cleanup", cleanup Full),
          ("dead_argument_eliminator", dead_argument_eliminator), -- inlining may reveal new dead arguments
          -- Untupling Section --
          ("tupled_returns", tupled_returns),
          ("full_cleanup", cleanup Full),
          -- Implicit Injection Section --
          ("implicit_injection", implicit_injection),
          ("partial_cleanup", cleanup Partial),
          -- Closure Gen Preparation Section --
          ("closure_gen", closure_gen),
          ("full_cleanup", cleanup Full),
          -- Primitives --
          ("addRequiredPrimFnHelpers", addRequiredPrimFnHelpers),
          -- ("replace_primfns", replace_primfns),
          -- Register Allocation Section --
          ("allocate_registers", allocate_registers)
     ]

     -- execute
     -- coreLift $ putStrLn (show cairocode)
     processed_code <- coreLift $ foldlM (executePhase isVerbose) cairocode phases
     -- coreLift $ putStrLn (show processed_code)
     let res = generate_code isStarknetLib processed_code

     -- produce output file
     let out = outputDir </> outfile
     Right () <- coreLift (writeFile out res)
       | Left err => throw (FileErr out err)
     when isVerbose $ coreLift $ putStrLn "Idris Compile Done"
     -- call formatter
     -- compile cairo file
     pure (Just out)

execute : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
execute defs tmpDir term = do coreLift $ putStrLn "Maybe in an hour."

cairoCodegen : Codegen
cairoCodegen = MkCG compile execute Nothing Nothing

main : IO ()
main = mainWithCodegens [("cairo", cairoCodegen)]

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module Data.BinarySearchTree

import Decidable.Order

%default total

contraSym : ((lhs = rhs) -> Void) -> (rhs = lhs) -> Void
contraSym contra eq = contra $ sym eq

strictRel : Ordered ty rel => {lhs : ty} -> {rhs : ty} ->
  lhs `rel` rhs -> (lhs = rhs -> Void ) -> (rhs `rel` lhs -> Void)
strictRel {lhs} {rhs} smaller notEq assumption =
  notEq $ antisymmetric lhs rhs smaller assumption

revStrictRel : {auto constraint : Ordered ty rel} -> {lhs : ty} -> {rhs : ty} ->
  (lhs `rel` rhs -> Void) -> (rhs `rel` lhs)
revStrictRel {rel} {lhs} {rhs} gt =
  case order {to = rel} lhs rhs of
    Left lte => absurd $ gt lte
    Right gte => gte

using (constraint : Ordered ty rel)
  export
  data Bounded : Ordered ty rel -> Maybe ty -> ty -> Maybe ty -> Type where
    WithinBounds : {lbound, ubound : Maybe ty} -> {pivot : ty} ->
      (gt : (x ** (lbound = Just x, rel pivot x)) -> Void) ->
      (lt : (x ** (ubound = Just x, rel x pivot)) -> Void) ->
      Bounded constraint lbound pivot ubound

  GTNothing : {auto constraint : Ordered ty rel} -> {value: ty} -> Type
  GTNothing {ty} {rel} {value} = (x : ty ** (Nothing = Just x, rel value x))

  anythingGTNothing : {auto constraint : Ordered ty rel} -> GTNothing -> Void
  anythingGTNothing (_ ** (Refl, _)) impossible

  LTNothing : {auto constraint : Ordered ty rel} -> {value: ty} -> Type
  LTNothing {ty} {rel} {value} = (x : ty ** (Nothing = Just x, rel x value))

  anythingLTNothing : {auto constraint : Ordered ty rel} -> LTNothing -> Void
  anythingLTNothing (_ ** (Refl, _)) impossible

  export
  WithinUnconstrainedBounds : {pivot : ty} -> Bounded _ Nothing pivot Nothing
  WithinUnconstrainedBounds {pivot} =
    WithinBounds {pivot} anythingGTNothing anythingLTNothing

  export
  changeLbound : Bounded constraint _ pivot ubound -> (rel pivot v -> Void) ->
    Bounded constraint (Just v) pivot ubound
  changeLbound {v} (WithinBounds _ lt) gt = WithinBounds {pivot} gt' lt
    where gt' : (x ** (Just v = Just x, rel pivot x)) -> Void
          gt' (x ** (prf, gte)) = gt $ rewrite justInjective prf in gte

  export
  changeUbound : Bounded constraint lbound pivot _ -> (rel v pivot -> Void) ->
    Bounded constraint lbound pivot (Just v)
  changeUbound {v} (WithinBounds gt _) lt = WithinBounds {pivot} gt lt'
    where lt' : (x ** (Just v = Just x, rel x pivot)) -> Void
          lt' (x ** (prf, lte)) = lt $ rewrite justInjective prf in lte

  public export
  data BinarySearchTree_ : Ordered ty rel -> Maybe ty -> Maybe ty -> Nat -> Type where
    Empty : BinarySearchTree_ _ _ _ Z
    Node : (v : ty) ->
      .{bounded : Bounded constraint lbound v ubound} ->
      {leftCount, rightCount : Nat} ->
      (left : BinarySearchTree_ constraint lbound (Just v) leftCount) ->
      (right : BinarySearchTree_ constraint (Just v) ubound rightCount) ->
      BinarySearchTree_ constraint lbound ubound (S $ leftCount + rightCount)

  value : BinarySearchTree_ constraint _ _ (S _) -> ty
  value (Node v _ _) = v

  leftCount : BinarySearchTree_ constraint _ _ (S _) -> Nat
  leftCount (Node {leftCount = len} _ _ _) = len

  left : {constraint : Ordered ty rel} ->
    (orig : BinarySearchTree_ constraint lbound _ (S _)) ->
      BinarySearchTree_ constraint lbound (Just (value orig)) (leftCount orig)
  left (Node _ l _) = l

  rightCount : BinarySearchTree_ constraint _ _ (S _) -> Nat
  rightCount (Node {rightCount = len} _ _ _) = len

  right : {constraint : Ordered ty rel} ->
    (orig : BinarySearchTree_ constraint _ ubound (S _)) ->
      BinarySearchTree_ constraint (Just (value orig)) ubound (rightCount orig)
  right (Node _ _ r) = r

  export
  data Elem : ty -> BinarySearchTree_ constraint _ _ _ -> Type where
    Here : Elem v (Node {constraint} v _ _)
    Left : Elem v l -> Elem v (Node _ l _)
    Right : Elem v r -> Elem v (Node _ _ r)

  export
  noEmptyElem : Elem _ Empty -> Void
  noEmptyElem _ impossible

  export
  lboundRespected :
    {lbound : ty} -> {tree : BinarySearchTree_ constraint (Just lbound) _ _} ->
    Elem pivot tree -> rel pivot lbound -> Void
  lboundRespected {rel} {lbound} {tree} elem {pivot} prf =
    let Node {bounded = WithinBounds gt _} v _ _ = tree in
      case elem of
        Here => gt (lbound ** (Refl, prf))
        Left elemL => lboundRespected elemL prf
        Right elemR => case order {to = rel} lbound v of
                         Left lte => let prf' = transitive pivot _ _ prf lte in
                                       lboundRespected elemR prf'
                         Right gte => gt (lbound ** (Refl, gte))

  export
  uboundRespected :
    {ubound : ty} -> {tree : BinarySearchTree_ constraint _ (Just ubound) _} ->
    Elem pivot tree -> rel ubound pivot -> Void
  uboundRespected {rel} {ubound} {tree} elem {pivot} prf =
    let Node {bounded = WithinBounds _ lt} v _ _ = tree in
      case elem of
        Here => lt (ubound ** (Refl, prf))
        Left elemL => case order {to = rel} v ubound of
                        Left lte => let prf' = transitive v _ _ lte prf in
                                      uboundRespected elemL prf'
                        Right gte => lt (ubound ** (Refl, gte))
        Right elemR => uboundRespected elemR prf

  data SearchSpace : Type where
    MkSearchSpace : Bounded constraint lbound pivot ubound ->
      BinarySearchTree_ constraint lbound ubound len -> SearchSpace

  data Finding : SearchSpace -> (SearchSpace -> Type) -> Type where
    GoLeft : .{retCalc : SearchSpace -> Type} ->
      .{bounded : Bounded constraint lbound pivot ubound} ->
      {orig : BinarySearchTree_ constraint lbound ubound (S _)} ->
      {leftBounded : Bounded constraint lbound pivot (Just (value orig))} ->
      (rel (value orig) pivot -> Void) ->
      retCalc (MkSearchSpace leftBounded (left orig)) ->
      Finding (MkSearchSpace bounded orig) retCalc
    GoRight : .{retCalc : SearchSpace -> Type} ->
      .{bounded : Bounded constraint lbound pivot ubound} ->
      {orig : BinarySearchTree_ constraint lbound ubound (S _)} ->
      {rightBounded : Bounded constraint (Just (value orig)) pivot ubound} ->
      (rel pivot (value orig) -> Void) ->
      retCalc (MkSearchSpace rightBounded (right orig)) ->
      Finding (MkSearchSpace bounded orig) retCalc
    Found : .{bounded : Bounded constraint lbound pivot ubound} ->
      {orig : BinarySearchTree_ constraint lbound ubound (S _)} ->
      (pivot = value orig) -> Finding (MkSearchSpace bounded orig) _
    DeadEnd : .{bounded : Bounded constraint lbound pivot ubound} ->
      {orig : BinarySearchTree_ constraint lbound ubound Z} ->
      Finding (MkSearchSpace bounded orig) _

  FindingTransform : Ordered ty _ -> ty -> (SearchSpace -> Type) -> Type
  FindingTransform {ty} constraint pivot retCalc =
    (lbound', ubound': Maybe ty) ->
    (bounded' : Bounded constraint lbound' pivot ubound') ->
    {len' : Nat} ->
    (tree' : BinarySearchTree_ constraint lbound' ubound' len') ->
    Finding (MkSearchSpace bounded' tree') retCalc ->
    retCalc (MkSearchSpace bounded' tree')

  find_ : DecEq ty => (pivot : ty) ->
    {lbound, ubound : Maybe ty} -> {len : Nat} ->
    (tree : BinarySearchTree_ constraint lbound ubound len) ->
    (bounded : Bounded constraint lbound pivot ubound) ->
    FindingTransform constraint pivot retCalc ->
    Finding (MkSearchSpace bounded tree) retCalc
  find_ _ Empty _ _ = DeadEnd
  find_ {rel} {len = S _} pivot (Node v l r) pivotBounded extract =
    case decEq pivot v of
      Yes Refl => Found Refl
      No contra => case order {to = rel} pivot v of
                     Left prf => let lt = strictRel prf contra
                                     bounded = changeUbound pivotBounded lt
                                     finding = find_ pivot l bounded extract
                                     ret = extract _ _ _ _ finding in
                                   GoLeft lt ret
                     Right prf => let gt = strictRel prf (contraSym contra)
                                      bounded = changeLbound pivotBounded gt
                                      finding = find_ pivot r bounded extract
                                      ret = extract _ _ _ _ finding in
                                    GoRight gt ret

  public export
  BinarySearchTree : Ordered ty rel -> Nat -> Type
  BinarySearchTree constraint len =
    BinarySearchTree_ constraint Nothing Nothing len

  public export
  CountedBinarySearchTree : Ordered ty rel -> Type
  CountedBinarySearchTree constraint =
    (len : Nat ** BinarySearchTree constraint len)

  find : DecEq ty => (pivot : ty) ->
    (ct : CountedBinarySearchTree constraint) ->
    FindingTransform constraint pivot retCalc ->
    retCalc $ MkSearchSpace (WithinUnconstrainedBounds {pivot}) (snd ct)
  find pivot (_ ** tree) transform =
    transform _ _ _ _ $ find_ pivot tree _ transform

  export
  decElem : DecEq ty => (v : ty) ->
    (ct : CountedBinarySearchTree constraint) ->
    Dec (Elem v (snd ct))
  decElem {constraint} value ct = find value ct transform
    where retCalc : SearchSpace -> Type
          retCalc (MkSearchSpace (WithinBounds {pivot} _ _) tree') =
            Dec (Elem pivot tree')
          transform : FindingTransform constraint value retCalc
          transform lbound' ubound' (WithinBounds {pivot = value} _ _) len tree' finding =
            case finding of
              GoLeft {orig = Node _ _ _} {leftBounded} contra prev =>
                let WithinBounds _ _ = leftBounded in
                case prev of
                  Yes prf => Yes $ Left prf
                  No contra' => No $ \prop => case prop of
                                                Here => contra $ reflexive value
                                                Left elem => contra' elem
                                                Right elem => lboundRespected elem (revStrictRel contra)
              GoRight {orig = Node _ _ _} {rightBounded} contra prev =>
                let WithinBounds _ _ = rightBounded in
                case prev of
                  Yes prf => Yes $ Right prf
                  No contra' => No $ \prop => case prop of
                                                Here => contra $ reflexive value
                                                Left elem => uboundRespected elem (revStrictRel contra)
                                                Right elem => contra' elem
              Found {orig = Node _ _ _} Refl => Yes Here
              DeadEnd {orig = Empty} => No noEmptyElem

  export
  elem : DecEq ty => ty -> CountedBinarySearchTree constraint -> Bool
  elem v ct = decAsBool $ decElem v ct

  export
  insert : DecEq ty => CountedBinarySearchTree constraint -> ty ->
    CountedBinarySearchTree constraint
  insert {constraint} ct value = find value ct transform
    where retCalc : SearchSpace -> Type
          retCalc (MkSearchSpace {constraint} (WithinBounds {pivot} {lbound} {ubound} _ _) tree') =
            (len : Nat ** BinarySearchTree_ constraint lbound ubound len)
          transform : FindingTransform constraint value retCalc
          transform lbound' ubound' (WithinBounds {pivot = value} gt lt) len tree' finding =
            case finding of
              GoLeft {orig} {leftBounded} _ prev =>
                let Node {bounded} v _ r = orig
                    WithinBounds _ _ = leftBounded
                    (_ ** l') = prev in
                  (_ ** Node {bounded} v l' r)
              GoRight {orig} {rightBounded} _ prev =>
                let Node {bounded} v l _ = orig
                    WithinBounds _ _ = rightBounded
                    (_ ** r') = prev in
                  (_ ** Node {bounded} v l r')
              Found {orig} Refl => (_ ** orig)
              DeadEnd {orig = Empty} =>
                let bounded = WithinBounds gt lt in
                  (_ ** Node {bounded} value Empty Empty)

max_stars_repo_name: jdevuyst/idris-data

max_issues_repo_name: jdevuyst/idris-data

max_forks_repo_name: jdevuyst/idris-data


text:
module Attributes

import Data.String

quote : String -> String
quote string = fastConcat ["\"", string, "\""]

public export
data Attribute = Class (List String)
               | Accept String
               | AcceptCharSet String
               | AcessKey String
               | Action String
               | Async
               | Cols Integer
               | Attr String String
               | Id String

attr : Show ty => String -> {auto value : ty} -> String
attr name = fastConcat [name, "=", show $ value]

Show Attribute where
  show (Class x) = "class=\"" ++ (unwords x) ++ "\""
  show (Accept x) = attr "accept"
  show (AcceptCharSet x) = attr "accept-char-set"
  show (AcessKey x) = attr "attr accesskey"
  show (Action x) = attr "action"
  show (Cols x) = attr "cols"
  show (Id x) = attr "id"
  show (Attr name value) = attr name {value = value}
  show Async = "async"

export
Show (List Attribute) where
  show [] = ""
  show props = " " ++ (unwords . map show) props ++ " "

export
Eq Attribute where
  (==) (Class left) (Class right)                 = left == right
  (==) (Accept left) (Accept right)               = left == right
  (==) (AcceptCharSet left) (AcceptCharSet right) = left == right
  (==) (AcessKey left) (AcessKey right)           = left == right
  (==) (Action left) (Action right)               = left == right
  (==) (Cols left) (Cols right)                   = left == right
  (==) (Id left) (Id right)                       = left == right
  (==) (Attr leftName leftValue) (Attr rightName rightValue) =
    leftName == rightName && leftValue == rightValue
  (==) Async Async = True
  (==) _ _ = False

max_stars_repo_name: Stinners/alder

max_issues_repo_name: Stinners/alder

max_forks_repo_name: Stinners/alder


text:
module WebAssembly.Validation.Modules.Globals

import WebAssembly.Structure
import WebAssembly.Validation.Conventions
import WebAssembly.Validation.Instructions
import WebAssembly.Validation.Types

||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/modules.html#globals)
|||
||| ```
||| ⊢ mut t ok    C ⊢ expr : [t]    C ⊢ expr const
||| ----------------------------------------------
||| C ⊢ {type mut t, init expr} : mut t
||| ```
public export
data ValidGlobal : Context -> Global -> GlobalType -> Type where
  MkValidGlobal : (c : Context)
               -> (mut : Mut)
               -> (t : ValType)
               -> (expr : Expr)
               -> ValidGlobalType (mut, t)
               -> ValidSequence c expr ([] ->> [t])
               -> ConstExpr c expr
               -> ValidGlobal c (MkGlobal (mut, t) expr) (mut, t)

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module Sec15b_ProcessList

import Part3.Sec15a_ProcessLib

data ListAction : Type where
     Length : List elem -> ListAction
     Append : List elem -> List elem -> ListAction

||| Note: this is not directly representable in Haskell
||| ListType can be represented as TypeFamily but TypeFamily is not
||| first class (cannot be used with partially applied type variables in type signatures).
ListType : ListAction -> Type
ListType (Length xs) = Nat
ListType (Append {elem} xs ys) = List elem

-- Definitions:
-- Service iface a = Process iface a Ready Looping
-- Client a = Process NoRecv a Ready Ready

total
procList : Service ListType ()
procList = do Respond (\msg => case msg of
                                    Length xs => Pure (length xs)
                                    Append xs ys => Pure (xs ++ ys))
              Loop procList

procMain : Client ()
procMain = do Just list <- Spawn procList
                      | Nothing => Action (putStrLn "Spawn failed")
              len <- Request list (Length [1,2,3])
              Action (printLn len)

              app <- Request list (Append [1,2,3] [4,5,6])
              Action (printLn app)


text:
module Ch05.VarArg

import Data.Vect

--------------------------------------------------------------------------------
-- Auxillary stuff for defining functions with a variable # of args
--------------------------------------------------------------------------------

||| Type of vectors of fixed length of elements of varying types
data VarVect : (n : Nat) -> Vect n Type -> Type where
  VarNil : VarVect Z []
  VarCons : (a : Type) ->
            (x : a) ->
            VarVect n as ->
            VarVect (S n) (a :: as)

VarArgType : (numArgs : Nat) ->
             Vect numArgs Type ->
             Type
VarArgType Z [] = ?VarArgType_rhs_1
VarArgType (S k) (a :: as) = a -> VarArgType k as

-- Suppose we want to define a function
--
--     f : a_1 -> a_2 -> ... -> a_n -> b
--
-- for some [a_1, ..., a_n] : Vect n Type. Then there are two ways to do that:
--
-- One: Starting from the knowledge of
--
--     \x1, ... x(n-1) => f x1 ... x(n-1) xn
--
-- for arbitrary but fixed `xn`, we define `f`.

max_stars_repo_name: mr-infty/tapl

max_issues_repo_name: mr-infty/tapl

max_forks_repo_name: mr-infty/tapl


text:
module Main

-- base
import Control.Monad.State
import Data.List
import System.File

-- contrib
import Data.SortedMap
import Text.Lexer
import Text.Lexer.Core
import Text.Parser
import Text.Parser.Core

namespace Input
  data Token = TComma
             | TUnknown
             | TNat Nat

  readDigit : Char -> Maybe Nat
  readDigit '0' = Just 0
  readDigit '1' = Just 1
  readDigit '2' = Just 2
  readDigit '3' = Just 3
  readDigit '4' = Just 4
  readDigit '5' = Just 5
  readDigit '6' = Just 6
  readDigit '7' = Just 7
  readDigit '8' = Just 8
  readDigit '9' = Just 9
  readDigit _ = Nothing

  combineReversedDigits : List Nat -> Nat
  combineReversedDigits [] = 0
  combineReversedDigits (n :: ns) = n + 10 * combineReversedDigits ns

  reverseNaturalGrammar : Grammar Char False Nat
  reverseNaturalGrammar =
    map combineReversedDigits $ many $ terminal "Can't parse digit" readDigit

  readTNat : String -> Token
  readTNat str = do
    let eithNat = parse reverseNaturalGrammar $ unpack $ reverse str
    case eithNat of
         Left _ => TUnknown
         Right (nat,_) => TNat nat

  toTokenData : String -> List (TokenData Token)
  toTokenData str = fst $
                    [ (is ',' , const TComma)
                    , (digits , readTNat)
                    ] `lex` str

  export
  readInput : String -> List Nat
  readInput str = reverse $ toNatList $ map tok $ toTokenData str where
    toNatList : List Token -> List Nat
    toNatList [] = []
    toNatList (TComma :: xs) = toNatList xs
    toNatList (TUnknown :: xs) = toNatList xs
    toNatList (TNat n :: xs) = n :: toNatList xs

namespace Part1
  findIndex : Eq a => a -> List a -> Maybe Nat
  findIndex y [] = Nothing
  findIndex y (x :: xs) =
    if x == y
       then Just 0
       else (1 +) <$> findIndex y xs

  nextNumber : List Nat -> Nat
  nextNumber [] = 0
  nextNumber (x :: xs) =
    case findIndex x xs of
         Nothing => 0
         Just n => 1 + n

  turn : List Nat -> List Nat
  turn ns = nextNumber ns :: ns

  doTimes : Nat -> (a -> a) -> a -> a
  doTimes Z _ x = x
  doTimes (S k) f x = doTimes k f $ f x

  minus : Nat -> Nat -> Maybe Nat
  minus Z Z = Just Z
  minus (S k) Z = Just $ S k
  minus Z (S k) = Nothing
  minus (S k) (S k') = k `minus` k'

  times : List Nat -> Maybe Nat
  times ns = 2020 `minus` length ns

  export
  turns : List Nat -> Maybe Nat
  turns ns = (doTimes <$> times ns <*> pure turn <*> pure ns) >>= head'

  times2 : List Nat -> Maybe Nat
  times2 ns = 30000000 `minus` length ns

namespace Part2
  record Game where
    constructor MkGame
    lookupTable : SortedMap Nat Nat
    lastNumber : Nat
    counter : Nat

  Show Game where
    show (MkGame lookupTable lastNumber counter) =
      "Game { lookupTable = " ++ show lookupTable
            ++ ", lastNumber = " ++ show lastNumber
            ++ ", counter = " ++ show counter
            ++ " }"

  scriptedTurn : Monad m => Nat -> StateT Game m ()
  scriptedTurn n = do
    game <- get
    let newLookupTable = (1 +) <$> insert game.lastNumber 0 game.lookupTable
        newCounter = 1 + game.counter
    put $ record { lookupTable = newLookupTable
                 , lastNumber = n
                 , counter = newCounter
               } game

  turn : Monad m => StateT Game m ()
  turn = do
    game <- get
    let mbDistance = lookup game.lastNumber game.lookupTable
        newLookupTable = (1 +) <$> insert game.lastNumber 0 game.lookupTable
        newCounter = 1 + game.counter
    put $ record { lookupTable = newLookupTable
                 , lastNumber = case mbDistance of
                                     Nothing => 0
                                     Just n => n
                 , counter = newCounter
               } game

  log : StateT Game IO ()
  log = do
    game <- get
    if natToInteger game.counter `mod` 10000 == 0
       then lift $ putStrLn $ show $ game.lookupTable
       else pure ()

  export
  turns : Nat -> StateT Game IO ()
  turns n = do
    n' <- gets counter
    --log
    if n == n'
       then do
         game <- get
         lift $ putStrLn $ show $ game.lastNumber
       else do
         turn
         turns n

  export
  initialGame : List Nat -> Game
  initialGame xs = removeWrongZero $ execState scriptedTurns startVal where
    removeWrongZero : Game -> Game
    removeWrongZero (MkGame lookupTable lastNumber counter) =
      MkGame newLookupTable lastNumber counter where
        newLookupTable : SortedMap Nat Nat
        newLookupTable = case lookup 0 lookupTable of
                              Nothing => lookupTable
                              Just n => if n == counter
                                           then delete 0 lookupTable
                                           else lookupTable
    scriptedTurns : Monad m => StateT Game m ()
    scriptedTurns = sequence_ $ map scriptedTurn $ xs
    startVal : Game
    startVal = MkGame empty 0 0 -- TODO: doesn't work unless the first number is 0; get's fixed in removeWrongZero

main : IO ()
main = do
  inputData <- readFile "./data"
  case inputData of
       Left err => print err
       Right dat => do
         let startingNumbers = readInput dat
         --traverse_ (putStrLn . show) $ turns startingNumbers
         let startingNumbers' = reverse startingNumbers
             maxCounter = 30000000
         _ <- runStateT (turns 300000) (initialGame startingNumbers')
         pure ()
  pure ()


text:
module Linear.Math

import public Data.Floating
import public Data.Num

export
sigmoid : (Neg a, Floating a) => a -> a
sigmoid x = 1 / (1 + exp (-x))

export
relu : (Num a, Ord a) => a -> a
relu x = max 0 x


text:
||| OrdList are labelled list (key/value store) that embed a order relation on keys
||| to sort its elements.
module Flexidisc.OrdList.Type

%default total
%access public export

||| The OrdList consturctors are exported publicly as they need to be used at
||| the type level.
||| It's better not to use the constructor for something else that just pattern
||| matching, as they dont guarantee that the keys are ordered.
||| @k Type of the keys
||| @v Type of the values
||| @o The order relation used to compared keys
data OrdList : (k : Type) ->  (o : Ord k) -> (v : Type) -> Type where
  Nil  : OrdList k o v
  (::) : (k, v) -> OrdList k o v -> OrdList k o v

%name OrdList xs, ys, zs

keys : OrdList k o v -> List k
keys [] = []
keys (kv :: xs) = fst kv :: keys xs

implementation Functor (OrdList k o) where

  map f [] = []
  map f (kv :: xs) = map f kv :: map f xs

||| Insert an element in the list before the first element that is greater than
||| the given one., according to the order `o`
insert : (x : (k, v)) -> (xs : OrdList k o v) -> OrdList k o v
insert x []= [x]
insert (k, v) ((k', v') :: xs) with (k < k')
  | False = (k',v') :: (insert (k, v) xs)
  | True  = (k,v)   :: (k',v') :: xs

||| Merge two `OrdList`, preserving the order if the initial list are ordered.
merge :  (xs, ys : OrdList k o v) -> OrdList k o v
merge [] ys = ys
merge xs [] = xs
merge ((k, v) :: hs) ((k', v') :: xs) with (k < k')
  | False = (k', v') :: merge ((k, v) :: hs) xs
  | True  = (k , v)  :: merge hs ((k', v') :: xs)

||| Sort a list.
toOrdList : (o : Ord k) => List (k, v) -> OrdList k o v
toOrdList = foldl (flip insert) Nil

||| Morphism to a list.
toList : OrdList k o v -> List (k, v)
toList [] = []
toList (x :: xs) = x :: toList xs

namespace properties

  mapPreservesKeys : (xs : OrdList k o v) -> (f : v-> v') ->
                     keys xs = keys (map f xs)
  mapPreservesKeys [] f = Refl
  mapPreservesKeys ((a, b) :: xs) f = cong $ mapPreservesKeys xs f

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
boolean : a && b || c = (a && b) || c
boolean = Refl


text:
module Replica.App.System

import Control.App
import System

%default covering

public export
data SystemError = Err Int

public export
interface Has [Exception SystemError] e => SystemIO e where
  system : String -> App e ()

export
Has [PrimIO, Exception SystemError] e => SystemIO e where
  system exec = do
    0 <- primIO $ system exec
      | n => throw (Err n)
    pure ()