text:
module Reviewer

import Data.Nat
import Data.String
import Data.List
import Data.List.DeleteBy
import Data.List1
import System.Random.Node
import Text.PrettyPrint.Prettyprinter
import Text.PrettyPrint.Prettyprinter.Symbols
import Text.PrettyPrint.Prettyprinter.Render.Terminal
import Util

%default total

record Score login where
  constructor MkScore
  user          : login
  partialScore  : Nat
  combinedScore : Nat

loginScore : Score login -> (login, Nat)
loginScore (MkScore l s c) = (l, c)

||| Get scored reviewers sorted from lowest to highest score.
||| A low score indicates less review work (a better candidate for
||| assigning a new PR to).
|||
||| The resulting `Score` contains both a partial score (the score
||| based only on open reivews) and also a combined score (the score
||| after negatively weighting closed reviews).
|||
||| Closed reviews are negatively scored because they are review requests
||| that were not answered.
scoredReviewers : Ord login =>
                  (closedReviews : List login)
               -> (openReviews : List login)
               -> (candidates : List login)
               -> List (Score login)
scoredReviewers closedReviews openReviews candidates =
  let closedReviewsWeighted = weightReviews 1 closedReviews
      openReviewsWeighted   = weightReviews 4 openReviews
      allReviews            = zipReviews openReviewsWeighted closedReviewsWeighted Subtract False
  in sort' $ zipReviews allReviews (weightReviews 0 candidates) Add True
  where
      -- The number of appearances is multiplied by the supplied weight which
      -- allows us to weight some lists more heavily than others.
      weightReviews : (weight : Nat) -> List login -> List (Score login)
      weightReviews weight reviews =
        let grouped = groupAllWith id reviews
        in  grouped <&> (\xs => let score = (* weight) . length $ forget xs in (MkScore (head xs) score score))

      -- Sort logins by the number of times each login was requested for review.
      sort' : List (Score login) -> List (Score login)
      sort' = sortBy $ compare `on` combinedScore

      data Op = Add | Subtract

      -- Add or subtract the scores for any equal logins.
      -- If `filterToSecondList` then no elements in the first list
      -- but not the second list will be kept.
      zipReviews : List (Score login) -> List (Score login) -> Op -> (filterToSecondList : Bool) -> List (Score login)
      zipReviews [] [] _ _     = []
      zipReviews [] ys Add _   = ys
      zipReviews [] ys Subtract _ = { combinedScore := 0 } <$> ys
      zipReviews xs [] _ True  = []
      zipReviews xs [] _ False = xs
      zipReviews (x@(MkScore l1 s1 c1) :: xs) ys op filter =
        case (deleteBy' ((==) `on` user) x ys, filter) of
             ((Nothing      , ys'), False)      => (MkScore l1 s1 c1             ) :: zipReviews xs ys' op filter
             ((Nothing      , ys'), True )      =>                                    zipReviews xs ys' op filter
             ((Just (MkScore _ _ c2'), ys'), _) => (MkScore l1 s1 (c1 `calc` c2')) :: zipReviews xs ys' op filter
        where
          calc : Nat -> Nat -> Nat
          calc k j with (op)
            _ | Add      = k + j
            _ | Subtract = k `minus` j

||| Choose reviewers that maintain harmony in the review world.
||| Returns the logins of all reviewers that would work equally well.
|||
||| @ closedReviews   The logins of each reviewer of each closed PR (duplicates intact).
||| @ openReviews     The logins of each reviewer of each open PR (duplicates intact).
||| @ candidates      The logins of all potential reviewers that should be considered.
||| @ forcedReviewers The logins of all reviewers that are being forced (not chosen by harmony).
||| @ author          The author of the PR for which a reviewer is being picked.
export
chooseReviewers : Ord login =>
                  (closedReviews : List login)
               -> (openReviews : List login)
               -> (candidates : List login)
               -> (forcedReviewers : List login)
               -> (author : login)
               -> List (login, Nat)
chooseReviewers closedReviews openReviews candidates forcedReviewers author =
  let remainingOptions = (nub candidates) \\ (author :: forcedReviewers)
      scoredOptions    = scoredReviewers closedReviews openReviews remainingOptions
  in  case scoredOptions of
           [] => []
           ((MkScore l s c) :: xs) =>
             let rest  = takeWhile ((== c) . combinedScore) xs
                 rest' = loginScore <$> rest
             in  (l, c) :: rest'

export
randomReviewer : HasIO io => List (login, Nat) -> io (Maybe login)
randomReviewer [] = pure Nothing
randomReviewer (x :: xs) = (Just . fst) <$> rndSelect (x :: xs)

||| Produce a graph of relative review workload for all developers matching the given
||| filter.
||| @ closedReviews The logins of each reviewer of each closed PR (duplicates intact).
||| @ openReviews   The logins of each reviewer of each open PR (duplicates intact).
||| @ candidates    The logins of all potential reviewers that should be considered.
export
reviewsGraph : Ord login => Pretty login =>
               (closedReviews : List login)
            -> (openReviews : List login)
            -> (candidates : List login)
            -> Doc AnsiStyle
reviewsGraph closedReviews openReviews candidates =
  let scoredOptions = reverse $ scoredReviewers closedReviews openReviews (sort $ nub candidates)
  in  case scoredOptions of
           [] => emptyDoc
           ((MkScore _ s c) :: _) =>
             let highScore = c + (s `minus` c)
             in  header <+> graph (if highScore > 0 then highScore else 1) scoredOptions <+> line
  where
    yellowDot : Doc AnsiStyle
    yellowDot = annotate (color Yellow) "·"

    redDot : Doc AnsiStyle
    redDot = annotate (color Red) "◦"

    header : Doc AnsiStyle
    header = vsep [ emptyDoc
                  , pretty "Weighted review workload."
                  , pretty "4x the numbewr of open review requests" <++> parens yellowDot
                  , pretty "1x the number of closed PRs with unanswered review requests" <++> parens redDot
                  , parens $ redDot <++> pretty "overlayed on" <++> yellowDot
                  , emptyDoc
                  , emptyDoc
                  ]

    -- The "detractor" is an indication of the amount of the score that was taken
    -- away by the heuristic in `scoredReviewers` that weights closed reviews with
    -- unanswered review requests negatively.
    bar : (indentation : Nat) -> (score : Nat) -> (detractor : Nat) -> Doc AnsiStyle
    bar idt score detractor = indent (cast idt) . hcat $
                                [ annotate (color Red) . pretty $ replicate detractor '◦'
                                , annotate (color Yellow) . pretty $ replicate score '·'
                                ]

    graphOne : (highScore : Nat) -> (Score login) -> Doc AnsiStyle
    graphOne highScore (MkScore user partialScore combinedScore) =
      let idt    = highScore `minus` partialScore
          user   = annotate italic $ pretty user
          detractor = (partialScore `minus` combinedScore)
          remainingSpace = highScore `minus` combinedScore
          -- we create a bar with the combinedScore and then fill in any
          -- remaining space with an indication of the detractor. We cap
          -- the detractor representation at the high score to make everything
          -- line up nicely. The detractor is just there to give some indication
          -- of review requests that did not count positively toward the score.
      in  bar idt combinedScore (min remainingSpace detractor) <++> user

    graph : (highScore : Nat) -> List (Score login) -> Doc AnsiStyle
    graph highScore = vsep . map (graphOne highScore)

max_stars_repo_name: mattpolzin/harmony

max_issues_repo_name: mattpolzin/harmony

max_forks_repo_name: mattpolzin/harmony


text:
module Backprop.MathUtils

||| when x < 0, return -1
||| when x > 0, return +1
||| otherwise, return 0
export
signum_zero : (Neg a, Ord a) => a -> a
signum_zero x = if x > 0 then 1 else if x < 0 then -1 else 0

ext: idr


text:
||| System console terminal
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module System.IO.Terminal

import Data.Buffer
import System.Info

import System.IO.Handle.Unix as U
import System.IO.Handle.Windows as W
import System.IO.Util.GetLine

%default total

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

%foreign "scheme,chez:(foreign-procedure #f \"GetConsoleMode\" (void* u32*) int)"
         "C:GetConsoleMode,kernel32.dll"
         "javascript:lambda:(x, y) => 0"
prim__win_GetConsoleMode : AnyPtr -> Buffer -> PrimIO Int

%foreign "scheme,chez:(foreign-procedure #f \"GetConsoleMode\" (void* unsigned-32) int)"
         "C:SetConsoleMode,kernel32.dll"
         "javascript:lambda:(x, y) => 0"
prim__win_SetConsoleMode : AnyPtr -> (mode:Int) -> PrimIO Int

%foreign "scheme,chez:(foreign-procedure #f \"GetConsoleScreenBufferInfo\" (void* void*) int)"
         "C:GetConsoleScreenBufferInfo,kernel32.dll"
         "javascript:lambda:(x, y) => 0"
prim__win_GetConsoleScreenBufferInfo : AnyPtr -> Buffer -> PrimIO Int

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

%foreign "C:ioctl,libc 6"
         "javascript:lambda:(x, y, z) => 0"
prim__ioctl_ptr : Int -> Bits32 -> Buffer -> PrimIO Int

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

export setup : HasIO io => io Bool
setup =
  if elem codegen ["refc", "chez"] && os == "windows"
     then do
       Just b <- newBuffer 4
         | Nothing => pure False
       W.MkHandle h <- W.getStdout
       _ <- primIO $ prim__win_GetConsoleMode h b
       b' <- getInt32 b 0 >>= pure . prim__or_Int 0x0004
       _ <- primIO $ prim__win_SetConsoleMode h b'
       pure True
     else pure True

export getScreenSize : HasIO io => io (Maybe (Int, Int))
getScreenSize =
  if elem codegen ["refc", "chez"]
     then case os of
       "windows" => do
         Just b <- newBuffer 32
           | Nothing => pure Nothing
         W.MkHandle h <- W.getStdout
         _ <- primIO $ prim__win_GetConsoleScreenBufferInfo h b
         left   <- getBits16 b (5 * 2)
         top    <- getBits16 b (6 * 2)
         right  <- getBits16 b (7 * 2)
         bottom <- getBits16 b (8 * 2)
         pure $ Just (cast right - cast left + 1, cast bottom - cast top + 1)
       "unix" => do
         Just b <- newBuffer 8
           | Nothing => pure Nothing
         _ <- primIO $ prim__ioctl_ptr 0 (0x5413 {- TIOCGWINSZ -} ) b
         r <- getBits16 b 0
         c <- getBits16 b 2
         pure $ Just (cast c, cast r)
       _ => pure Nothing
     else pure Nothing

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

export getChar : HasIO io => io (Maybe Char)
getChar = U.hGetChar U.stdin

export putChar : HasIO io => Char -> io ()
putChar ch = do
  _ <- U.hPutChar U.stdout ch
  pure ()

export getLine : HasIO io => io (Maybe String)
getLine = mkGetLine getChar 4096

export putStr : HasIO io => String -> io ()
putStr str = do
  _ <- U.hPutStr U.stdout str
  pure ()

export putStrLn : HasIO io => String -> io ()
putStrLn str = do
  _ <- U.hPutStrLn U.stdout str
  pure ()

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


text:
module Goldbach

import Data.DPair
import Data.Nat

public export
data Even : Nat -> Type where
  EvZ  : Even Z
  EvSS : Even n -> Even $ S $ S n

public export
half : (n : Nat) -> {auto ev : Even n} -> Subset Nat (\k => n = k + k) -- like `(k ** n = k + k)` but with compile-time right argument.
half Z = Element Z Refl
half (S $ S k) {ev=EvSS _} = let Element halfK halfKPrf = half k in
                             Element (S halfK) rewrite sym $ plusSuccRightSucc halfK halfK in
                                               rewrite halfKPrf in
                                               Refl

export
gte1nz : (k : Nat) -> {auto gte : k `GTE` S x} -> Not (k = 0)
gte1nz 0     Refl impossible
gte1nz (S _) Refl impossible

public export
Prime : Nat -> Type
Prime n = (k : Nat) -> {auto gt2 : k `GTE` 2} -> {auto ltn : k `LT` n} -> Not (modNatNZ n k (gte1nz k {x=1}) = 0)

export
goldbach : (x : Nat) -> {auto ev : Even x} -> {auto gt2 : x `GT` 2} -> (y ** z ** (Prime y, Prime z, x = y + z))

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Subst

import FinCmp
import Term

%default total

--------------------------------------------------------------
-- Begin: WEAKENING, I.E. ADDING UNUSED VARIABLES TO THE SCOPE

-- Abbreviate the name of the function 'weakenN'
-- from 'Data.Fin' (for better readability):
wkN : (n : Nat) -> Fin m -> Fin (m + n)
wkN = Data.Fin.weakenN

weakenContext : (m : Nat) -> (n : Nat) -> Term m -> Term (m + n)
weakenContext m n (TVar i)     = TVar (wkN n i)
weakenContext m n (TAbs x)     = TAbs (weakenContext (S m) n x)
weakenContext m n (TApp x y)   = TApp (weakenContext m n x)
                                      (weakenContext m n y)
weakenContext _ _ TZero         = TZero
weakenContext m n (TSucc x)     = TSucc (weakenContext m n x)
weakenContext m n (TPred x)     = TPred (weakenContext m n x)
weakenContext m n (TIfz x y z)  = TIfz (weakenContext m n x)
                                       (weakenContext m n y)
                                       (weakenContext m n z)

-- End: WEAKENING, I.E. ADDING UNUSED VARIABLES TO THE SCOPE
------------------------------------------------------------

-------------------------
-- Begin: TECHNICAL LEMMA

tightenBound :  {n : Nat} ->
                (j : Fin (S n)) -> (i : Fin (S n)) ->
                j :<: i ->
                (j_ : Fin n ** (finToNat j_ = finToNat j))
--
tightenBound             _         FZ      lt = absurd $ finNotLtZ lt
--
tightenBound {n = (S k)} FZ        (FS i') lt = (FZ ** Refl)
--
tightenBound {n = (S k)} (FS j') (FS i') lt =
  let (j'_ ** eq') = tightenBound {n = k} j' i' (finLtPred lt)
  in (FS j'_ ** cong eq')

-- End: TECHNICAL LEMMA
-----------------------

------------------------------------------------------------------------------
-- Begin: SUBSTITUTION PRESERVES SCOPING OF EXPRESSIONS IN THE LAMBDA CALCULUS

subst_var : Term 0 ->           -- Term that is subtituted in.
            (i : Fin (S n)) ->  -- The i-th variable (Var i) is substituted for.
            (j : Fin (S n)) ->  -- Substitution takes place inside the term (Var j).
            Term n
-- An actual substitution occurs only if "i = j".
subst_var {n} ts i j = case finCmpDec i j of
  CmpEq eq => weakenContext 0 n ts
  CmpLt lt => case j of
                   FZ    => absurd $ finNotLtZ lt
                   FS j' => TVar j'
  CmpGt gt => case i of
                   FZ    => absurd $ finNotLtZ gt
                   FS i' => let (j_ ** _) = tightenBound j (FS i') gt
                            in TVar j_

export subst : Term 0 ->           -- Term that is substituted in.
               (i : Fin (S n)) ->  -- The i-th varibale (Var i) is substituted for.
               Term (S n) ->       -- Substitution takes place inside this term.
               Term n
--
-- The hard part is substitution in expressions that
-- are variables, i.e. substitution in 'Var j'.
subst ts i (TVar j) = subst_var ts i j
--
-- Substitution in expressions that are not variables
-- is handled by recursing over (and substituting in)
-- subexpressions:
subst ts i (TAbs e)        = TAbs (subst ts (FS i) e)
subst ts i (TApp e1 e2)    = TApp (subst ts i e1) (subst ts i e2)
subst _  _ TZero           = TZero
subst ts i (TSucc e)       = TSucc (subst ts i e)
subst ts i (TPred e)       = TPred (subst ts i e)
subst ts i (TIfz e1 e2 e3) = TIfz (subst ts i e1) (subst ts i e2) (subst ts i e3)

-- End: SUBSTITUTION PRESERVES SCOPING OF EXPRESSIONS IN THE LAMBDA CALCULUS
----------------------------------------------------------------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
||| Module for parsing and handling of URIs.
|||
||| References:
|||   [1] https://tools.ietf.org/html/rfc3986
|||   [2] https://tools.ietf.org/html/rfc6874
|||   [3] https://tools.ietf.org/html/rfc7320
|||   [4] https://tools.ietf.org/html/rfc8820
|||
||| (C) The Idris Community, 2021
module Data.URI

import Data.List
import Data.List1
import Data.Maybe
import Data.String
import Data.String.Extra
import Data.String.Parser
import Data.Vect
import Libraries.Utils.Hex

foldSeq : (Applicative f, Traversable t, Monoid m) => t (f m) -> f m
foldSeq = map concat . sequence

||| Type of an authority within URIs.
public export
record URIAuthority where
  constructor MkURIAuthority
  userInfo : Maybe String
  regName : String
  port : Maybe Nat

export
Show URIAuthority where
  show authority = fromMaybe "" ((+> '@') <$> authority.userInfo)
                     ++ authority.regName
                     ++ fromMaybe "" (((<+) ':' . show) <$> authority.port)

export
Eq URIAuthority where
  x == y = show x == show y

export
Ord URIAuthority where
  compare x y = compare (show x) (show y)

||| Type for a general URI.
public export
record URI where
  constructor MkURI
  scheme : String
  authority : Maybe URIAuthority
  path : String
  query : String
  fragment : String

export
Show URI where
  show uri = uri.scheme
               ++ ":"
               ++ fromMaybe "" ((++) "//" . show <$> uri.authority)
               ++ uri.path
               ++ if uri.query == "" then "" else '?' <+ uri.query
               ++ if uri.fragment == "" then "" else '#' <+ uri.fragment

export
Eq URI where
  x == y = show x == show y

export
Ord URI where
  compare x y = compare (show x) (show y)

||| Returns true for characters that are allowed in a URI but do not have a reserved purpose.
|||
||| @see RFC 3986, section 2.3
isUnreserved : Char -> Bool
isUnreserved c = isAlphaNum c || (c `Prelude.elem` ['-', '.', '_', '~'])

||| Returns true for reserved characters that requires to be percent escaped.
|||
||| @see RFC 3986, section 2.2
isSubDelim : Char -> Bool
isSubDelim c = c `Prelude.elem` ['!', '$', '&', '\'', '(', ')', '*', '+', ',', ';', '=']

||| Parser for percent encoded characters.
|||
||| @see RFC 3986, section 2.1
pctEncoded : Parser Char
pctEncoded = do
  ignore $ char '%'
  x <- satisfy isHexDigit
  y <- satisfy isHexDigit
  let Just d = fromHexChars [y, x]
    | Nothing => fail $ "Cannot convert " ++ show (the (List Char) [x, y]) ++ " to a hex number"
  pure (chr (cast d))

||| Parser for a URI scheme.
|||
||| @see RFC 3986, section 3.1
schemeParser : Parser String
schemeParser = pack <$> [| alphaNum :: many (satisfy isValidForScheme) |]
  where isValidForScheme : Char -> Bool
        isValidForScheme c = isAlphaNum c || (c `Prelude.elem` ['+', '-', '.'])

||| Parser for a URI userinfo subcomponent.
|||
||| @see RFC 3986, section 3.2.1
userInfoParser : Parser String
userInfoParser = pack <$> many (satisfy isUnreserved <|> char ':' <|> pctEncoded <|> satisfy isSubDelim)

||| Parser for potentially future version of IPs.
|||
||| @see RFC 3986, section 3.2.2
ipVFutureParser : Parser String
ipVFutureParser = with Prelude.(::)
  foldSeq [ string "v"
          , pack <$> some (satisfy isHexDigit)
          , string "."
          , pack <$> some (satisfy (\c => isUnreserved c || isSubDelim c || c == ':'))
          ]

||| Parser for an IPv4 address.
|||
||| @see RFC 3986, section 3.2.2
ipV4AddressParser : Parser String
ipV4AddressParser = with Prelude.(::) foldSeq [octet, string ".", octet, string ".", octet, string ".", octet]
  where
    octet : Parser String
    octet = integer >>= (\v => guard (0 <= v && v <= 255) *> pure (show v))

||| Parser for an IPv6 address.
|||
||| @see RFC 3986, section 3.2.2
ipV6AddressParser : Parser String
ipV6AddressParser = with Prelude.(::)
    -- This implementation follows closely the definition in the RFC 3986, so is a mess and surely can be improved :(
        multipleH16LS32 6
    <|> foldSeq [string "::", multipleH16LS32 5]
    <|> foldSeq [optionMap "" id h16, string "::", multipleH16LS32 4]
    <|> foldSeq [optionMap "" id (multipleH16 1), string "::", multipleH16LS32 3]
    <|> foldSeq [optionMap "" id (multipleH16 2), string "::", multipleH16LS32 2]
    <|> foldSeq [optionMap "" id (multipleH16 3), string "::", [| h16 +> char ':' |], ls32]
    <|> foldSeq [optionMap "" id (multipleH16 4), string "::", ls32]
    <|> foldSeq [optionMap "" id (multipleH16 5), string "::", h16]
    <|> foldSeq [optionMap "" id (multipleH16 6), string "::"]
  where
    h16 : Parser String
    h16 = do
      c <- satisfy isHexDigit
      o1 <- optional (satisfy isHexDigit)
      o2 <- optional (satisfy isHexDigit)
      o3 <- optional (satisfy isHexDigit)
      pure (pack (c :: fromMaybe [] (sequence [o1, o2, o3])))

    ls32 : Parser String
    ls32 = [| [| h16 +> char ':' |] ++ h16 |] <|> ipV4AddressParser

    multipleH16 : Nat -> Parser String
    multipleH16 n = [| (concat . toList <$> ntimes n [| h16 +> char ':' |]) ++ h16 |]

    multipleH16LS32 : Nat -> Parser String
    multipleH16LS32 n = [| (concat . toList <$> ntimes n [| h16 +> char ':' |]) ++ ls32 |]

||| Parser for a zone indentifier for a IPv6 Scoped Address.
|||
||| @see RFC 6874, section 2
zoneIDParser : Parser String
zoneIDParser = pack <$> some (satisfy isUnreserved <|> pctEncoded)

||| Parser for a IPv6 Scoped Address.
|||
||| @see RFC 6874, section 2
ipV6AddrzParser : Parser String
ipV6AddrzParser = with Prelude.(::) concat <$> sequence [ipV6AddressParser, string "%25", zoneIDParser]

||| Parser for a IPv6 Scoped Address.
|||
||| @see RFC 3986, section 3.2.2
||| @see RFC 6874, section 2
ipLiteralParser : Parser String
ipLiteralParser = char '[' *> (ipV6AddressParser <|> ipV6AddrzParser <|> ipVFutureParser) <* char ']'

||| Parser for a registered name.
|||
||| @see RFC 3986, section 3.2.2
regNameParser : Parser String
regNameParser = pack <$> many (satisfy isUnreserved <|> pctEncoded <|> satisfy isSubDelim)

||| Parser for a URI authority.
|||
||| @see RFC 3986, section 3.2
authorityParser : Parser URIAuthority
authorityParser = do
  ignore $ string "//"
  userInfo <- optional (userInfoParser <* char '@')
  host <- ipLiteralParser <|> ipV4AddressParser <|> regNameParser
  port <- optional (char ':' *> natural)
  pure (MkURIAuthority userInfo host port)

||| Parser for a valid character in a path.
|||
||| @see RFC 3986, section 3.3
pchar : Parser Char
pchar = satisfy (\c => isUnreserved c || isSubDelim c) <|> pctEncoded <|> char ':' <|> char '@'

||| Parser for a segment in a path.
|||
||| @see RFC 3986, section 3.3
segment : Parser String
segment = pack <$> many pchar

||| Parser for a non-empty segment in a path.
|||
||| @see RFC 3986, section 3.3
segmentNZ : Parser String
segmentNZ = pack <$> some pchar

||| Parser for a non-empty segment in a path that does not start with a colon.
|||
||| @see RFC 3986, section 3.3
segmentNZNC : Parser String
segmentNZNC = pack <$> some (satisfy (\c => isUnreserved c || isSubDelim c) <|> pctEncoded <|> char '@')

||| Parser for an absolute or empty path.
|||
||| @see RFC 3986, section 3.3
abempty : Parser String
abempty = concat <$> many [| char '/' <+ segment |]

||| Parser for an absolute path.
|||
||| @see RFC 3986, section 3.3
absolute : Parser String
absolute = [| char '/' <+ optionMap "" id [| segmentNZ ++ (concat <$> many [| char '/' <+ segment |]) |] |]

||| Parser for path that starts without a colon.
|||
||| @see RFC 3986, section 3.3
noscheme : Parser String
noscheme = [| segmentNZNC ++ (concat <$> many [| char '/' <+ segment |]) |]

||| Parser for path that starts with a segment.
|||
||| @see RFC 3986, section 3.3
rootless : Parser String
rootless = [| segmentNZ ++ (concat <$> many [| char '/' <+ segment |]) |]

||| Parser for a, possibly empty, path.
|||
||| @see RFC 3986, section 3.3
pathParser : Parser String
pathParser = absolute <|> noscheme <|> rootless <|> abempty <|> pure ""

||| Parser for a query component.
|||
||| @see RFC 3986, section 3.4
queryParser : Parser String
queryParser = pack <$> many (pchar <|> char '/' <|> char '?')

||| Parser for a fragment identifier component.
|||
||| @see RFC 3986, section 3.5
fragmentParser : Parser String
fragmentParser = pack <$> many (pchar <|> char '/' <|> char '?')

||| Parser for a generic URI.
|||
||| @see RFC 3986, section 3
export
uriParser : Parser URI
uriParser = do
  scheme <- schemeParser
  ignore $ char ':'
  (authority, path) <- [| MkPair ((Just <$> authorityParser)) abempty |] <|> ((Nothing,) <$> (absolute <|> rootless <|> empty))
  query <- optionMap "" id (char '?' *> queryParser)
  fragment <- optionMap "" id (char '#' *> fragmentParser)
  pure (MkURI scheme authority path query fragment)

||| Parser for a URI relative reference.
|||
||| @see RFC 3986, section 4.2
relativeReferenceParser : Parser URI
relativeReferenceParser = do
  (authority, path) <- [| MkPair ((Just <$> authorityParser)) abempty |] <|> ((Nothing,) <$> (absolute <|> noscheme <|> empty))
  query <- optionMap "" id (char '?' *> queryParser)
  fragment <- optionMap "" id (char '#' *> fragmentParser)
  pure (MkURI "" authority path query fragment)

||| Parser for a URI reference.
|||
||| @see RFC 3986, section 4.1
export
uriReferenceParser : Parser URI
uriReferenceParser = uriParser <|> relativeReferenceParser

||| Parser for an absolute URI without a fragment identifier.
|||
||| @see RFC 3986, section 4.3
export
uriAbsoluteParser : Parser URI
uriAbsoluteParser = do
  scheme <- schemeParser
  ignore $ char ':'
  (authority, path) <- [| MkPair ((Just <$> authorityParser)) abempty |] <|> ((Nothing,) <$> (absolute <|> rootless <|> empty))
  query <- optionMap "" id (char '?' *> queryParser)
  pure (MkURI scheme authority path query "")


text:
parameters (eq : a -> a -> Bool)
  lookup : a -> List (a, b) -> Maybe b
  lookup x [] = Nothing
  lookup x ((k, v) :: ys)
      = if eq x k
           then Just v
           else lookup x ys

  data Dict : Type -> Type where
       MkDict : List (a, b) -> Dict b

  lookupK : a -> Dict b -> Maybe b
  lookupK k (MkDict xs) = lookup k xs

testDict : Dict {a=Int} (==) String
testDict = MkDict _ [(0, "foo"), (1, "bar")]

parameters (y : ?) -- test that the type of 'y' can be inferred
  foo : (x : Int) -> x = y -> Int
  foo x@_ Refl = 42


text:
module Text.WebIDL.Types.Definition

import Generics.Derive
import Text.WebIDL.Types.Attribute
import Text.WebIDL.Types.Argument
import Text.WebIDL.Types.Identifier
import Text.WebIDL.Types.Member
import Text.WebIDL.Types.StringLit
import Text.WebIDL.Types.Type

%hide Language.Reflection.TT.Namespace
%language ElabReflection

||| CallbackRest ::
|||     identifier = Type ( ArgumentList ) ;
public export
record Callback where
  constructor MkCallback
  attributes : ExtAttributeList
  name       : Identifier
  type       : IdlType
  args       : ArgumentList

%runElab derive "Callback" [Generic,Meta,Eq,Show,HasAttributes]

||| CallbackRestOrInterface ::
|||     CallbackRest
|||     interface identifier { CallbackInterfaceMembers } ;
public export
record CallbackInterface where
  constructor MkCallbackInterface
  attributes : ExtAttributeList
  name       : Identifier
  members    : CallbackInterfaceMembers

%runElab derive "CallbackInterface" [Generic,Meta,Eq,Show,HasAttributes]

||| Dictionary ::
|||     dictionary identifier Inheritance { DictionaryMembers } ;
public export
record Dictionary where
  constructor MkDictionary
  attributes : ExtAttributeList
  name       : Identifier
  inherits   : Inheritance
  members    : DictionaryMembers

%runElab derive "Dictionary" [Generic,Meta,Eq,Show,HasAttributes]

||| Enum ::
|||     enum identifier { EnumValueList } ;
|||
||| EnumValueList ::
|||     string EnumValueListComma
|||
||| EnumValueListComma ::
|||     , EnumValueListString
|||     ε
|||
||| EnumValueListString ::
|||     string EnumValueListComma
|||     ε
public export
record Enum where
  constructor MkEnum
  attributes : ExtAttributeList
  name       : Identifier
  values     : List1 StringLit

%runElab derive "Enum" [Generic,Meta,Eq,Show,HasAttributes]

||| IncludesStatement ::
|||     identifier includes identifier ;
public export
record Includes where
  constructor MkIncludes
  attributes : ExtAttributeList
  name       : Identifier
  includes   : Identifier

%runElab derive "Includes" [Generic,Meta,Eq,Show,HasAttributes]

||| InterfaceRest ::
|||     identifier Inheritance { InterfaceMembers } ;
public export
record Interface where
  constructor MkInterface
  attributes : ExtAttributeList
  name       : Identifier
  inherits   : Inheritance
  members    : InterfaceMembers

%runElab derive "Interface" [Generic,Meta,Eq,Show,HasAttributes]

||| MixinRest ::
|||     mixin identifier { MixinMembers } ;
public export
record Mixin where
  constructor MkMixin
  attributes : ExtAttributeList
  name       : Identifier
  members    : MixinMembers

%runElab derive "Mixin" [Generic,Meta,Eq,Show,HasAttributes]

||| Namespace ::
|||     namespace identifier { NamespaceMembers } ;
public export
record Namespace where
  constructor MkNamespace
  attributes : ExtAttributeList
  name       : Identifier
  members    : NamespaceMembers

%runElab derive "Namespace" [Generic,Meta,Eq,Show,HasAttributes]

||| Typedef ::
|||     typedef TypeWithExtendedAttributes identifier ;
public export
record Typedef where
  constructor MkTypedef
  attributes     : ExtAttributeList
  typeAttributes : ExtAttributeList
  type           : IdlType
  name           : Identifier

%runElab derive "Typedef" [Generic,Meta,Eq,Show,HasAttributes]

||| PartialDictionary ::
|||     dictionary identifier { DictionaryMembers } ;
public export
record PDictionary where
  constructor MkPDictionary
  attributes : ExtAttributeList
  name       : Identifier
  members    : DictionaryMembers

%runElab derive "PDictionary" [Generic,Meta,Eq,Show,HasAttributes]

||| PartialInterfaceRest ::
|||     identifier { PartialInterfaceMembers } ;
public export
record PInterface where
  constructor MkPInterface
  attributes : ExtAttributeList
  name       : Identifier
  members    : PartialInterfaceMembers

%runElab derive "PInterface" [Generic,Meta,Eq,Show,HasAttributes]

||| MixinRest ::
|||     mixin identifier { MixinMembers } ;
public export
record PMixin where
  constructor MkPMixin
  attributes : ExtAttributeList
  name       : Identifier
  members    : MixinMembers

%runElab derive "PMixin" [Generic,Meta,Eq,Show,HasAttributes]

||| Namespace ::
|||     namespace identifier { NamespaceMembers } ;
public export
record PNamespace where
  constructor MkPNamespace
  attributes : ExtAttributeList
  name       : Identifier
  members    : NamespaceMembers

%runElab derive "PNamespace" [Generic,Meta,Eq,Show,HasAttributes]

public export
DefTypes : List Type
DefTypes = [ Callback
           , CallbackInterface
           , Dictionary
           , Enum
           , Includes
           , Interface
           , Mixin
           , Namespace
           , Typedef
           ]

public export
PartTypes : List Type
PartTypes = [PDictionary, PInterface, PMixin, PNamespace]

||| Definition ::
|||     CallbackOrInterfaceOrMixin
|||     Namespace
|||     Partial
|||     Dictionary
|||     Enum
|||     Typedef
|||     IncludesStatement
||| CallbackOrInterfaceOrMixin ::
|||     callback CallbackRestOrInterface
|||     interface InterfaceOrMixin
|||
||| InterfaceOrMixin ::
|||     InterfaceRest
|||     MixinRest
public export
Definition : Type
Definition = NS I DefTypes

public export
0 Definitions : Type
Definitions = NP List DefTypes

||| PartialDefinition ::
|||     interface PartialInterfaceOrPartialMixin
|||     PartialDictionary
|||     Namespace
|||
||| PartialInterfaceOrPartialMixin ::
|||     PartialInterfaceRest
|||     MixinRest
public export
Part : Type
Part = NS I PartTypes

public export
accumNs : {ts : _} -> List (NS I ts) -> NP List ts
accumNs = foldl (\np,ns => hliftA2 (++) (toNP ns) np) hempty

public export
0 PartOrDef : Type
PartOrDef = NS I [Part,Definition]

public export
0 PartsAndDefs : Type
PartsAndDefs = NP List [Part,Definition]

public export
defs : PartsAndDefs -> Definitions
defs = accumNs . get Definition

--------------------------------------------------------------------------------
--          Domain
--------------------------------------------------------------------------------

update : Eq k => (b -> b) -> k -> (b -> k) -> List b -> List b
update f k bk = map (\b => if bk b == k then f b else b)

mergeDict : PDictionary -> Dictionary -> Dictionary
mergeDict d = record { members $= (++ d.members) }

mergeIface : PInterface -> Interface -> Interface
mergeIface i = record { members $= (++ map to i.members) }
  where to : (a,b) -> (a, NS I [c,b])
        to (x, y) = (x, inject y)

mergeMixin : PMixin -> Mixin -> Mixin
mergeMixin m = record { members $= (++ m.members) }

mergeNamespace : PNamespace -> Namespace -> Namespace
mergeNamespace n = record { members $= (++ n.members) }

public export
record Domain where
  constructor MkDomain
  domain              : String
  callbacks           : List Callback
  callbackInterfaces  : List CallbackInterface
  dictionaries        : List Dictionary
  enums               : List Enum
  includeStatements   : List Includes
  interfaces          : List Interface
  mixins              : List Mixin
  namespaces          : List Namespace
  typedefs            : List Typedef

%runElab derive "Domain" [Generic,Meta,Eq,Show,HasAttributes]

applyPart : Domain -> Part -> Domain
applyPart d (Z v) =
  record { dictionaries $= update (mergeDict v) v.name name } d
applyPart d (S $ Z v) =
  record { interfaces $= update (mergeIface v) v.name name } d
applyPart d (S $ S $ Z v) =
  record { mixins $= update (mergeMixin v) v.name name } d
applyPart d (S $ S $ S $ Z v) =
  record { namespaces $= update (mergeNamespace v) v.name name } d

export
toDomains : List (String,PartsAndDefs) -> List Domain
toDomains ps =
  let defs = map (\(s,pad) => fromNP s (defs pad)) ps
      prts = concatMap (\(_,pad) => get Part pad) ps
   in map (\d => foldl applyPart d prts) defs

  where fromNP : String -> Definitions -> Domain
        fromNP s [c,ci,d,e,ic,it,m,n,t] = MkDomain s c ci d e ic it m n t


text:
main : IO ()
main = do
  printLn $ the Nat $ fromInteger (-1)
  printLn $ the Nat $ fromInteger 1000000000


text:
module Group

import Monoid
%access public export

||| The proof that b is inverse of a
total
IsInverse : (typ : Type) -> ((*) : typ -> typ -> typ) -> (IdentityExists typ (*)) -> (a : typ) -> (b : typ) -> Type
IsInverse typ (*) pfid a b = ((a*b = fst(pfid)),(b*a = fst(pfid)))

||| Given a type and a binary operation the type of proofs that each element has its inverse
total
InverseExists : (typ : Type) -> ((*) : typ -> typ -> typ) -> Type
InverseExists typ (*) = (pfid : (IdentityExists typ (*)) ** ((a : typ) -> (a_inv ** (IsInverse typ (*) pfid a a_inv))))
--(pfid : (IdentityExists typ (*)) ** ((a : typ) -> (a_inv : typ ** ((a*a_inv = fst(pfid)),(a_inv*a = fst(pfid))))))

||| Given a type and a binary operation the type of proofs that the type along with the
||| operation is a group
total
IsGroup : (grp : Type) -> ((*) : grp -> grp -> grp) -> Type
IsGroup grp (*) = (Associative grp (*), (IdentityExists grp (*), InverseExists grp (*)))

||| Given a group gives it's identity with proof
total
Group_id : (grp : Type) -> ((*) : grp -> grp -> grp) -> (IsGroup grp (*)) -> (IdentityExists grp (*))
Group_id grp (*) pfgrp = (fst (snd pfgrp))

||| Generates inverses with proofs
total
Inv_with_pf : (grp : Type) -> ((*) : grp -> grp -> grp) -> (pfgrp : IsGroup grp (*)) -> (x : grp)
              -> (y : grp ** (IsInverse grp (*) (fst (snd (snd pfgrp))) x y))
Inv_with_pf grp (*) pfgrp x = (snd (snd (snd pfgrp))) x

||| Generates inverses
total
Inv: (grp : Type) -> ((*) : grp -> grp -> grp) -> IsGroup grp (*) -> (x: grp) -> grp
Inv grp (*) pf x = fst (Inv_with_pf grp (*) pf x)
-- fst(snd(snd(snd(pf))) x)

||| Given a group, the type of proofs that it is abelian
total
IsAbelianGrp:  (grp : Type) -> ((*) : grp -> grp -> grp) -> Type
IsAbelianGrp grp (*)  = (IsGroup grp (*), Commutative grp (*))
--- (a:grp) -> (b:grp) -> (a*b = b*a)

||| The type of proofs that a given function f between x and y is injective
total
Inj: (x: Type) -> (y: Type) -> (f: x-> y) -> Type
Inj x y f = (a : x) -> (b : x) -> (f a = f b) -> (a = b)

|||The Group data type, with a single constructor
data Group: (g: Type) -> Type where
  MkGroup: (grp : Type) -> ((*) : grp -> grp -> grp) -> (IsGroup grp (*))  -> Group grp

||| The type of proofs that a function between groups is a group homomorphism
total
Hom: (grp : Type) -> Group grp -> (g: Type) -> Group g -> (f : grp -> g) -> Type
Hom grp (MkGroup grp (*) pf1) g (MkGroup g (+) pf2) f  = ((IsIdentity g (+) e) , (
                               (a : grp) -> (b : grp) -> ((f (a*b)) = ((f a) + (f b))))) where
                               e = f(fst (Group_id grp (*) pf1))

||| The type of proofs that a given group is a subgroup of another, via injective homorphisms
total
Subgroup: (h: Type) -> Group h -> (g: Type) -> Group g -> Type
Subgroup h pfh g pfg = DPair (h -> g) (\f => (Hom h pfh g pfg f , Inj h g f))
--- DPair (h->g) (\f => ((Hom h (+) pfh g (*) pfg f), (Inj h g f)))

||| The type of proofs that a given subgroup is normal/self-conjugate
total
NSub: (h: Type) -> (pfh: Group h) -> (g: Type) -> (pfg: Group g) ->
      (Subgroup h pfh g pfg) -> Type
NSub  h (MkGroup h (+) pfh) g (MkGroup g (*) pfg) (f ** pff) = (a : h) -> (b : g) -> (x : h ** (b*(f a)*(inv b) = (f x))) where
     inv = Inv g (*) pfg


text:
module Typing.Unification

import Typing.Common
import Typing.Util
import Typing.Equate

-- oYYYo _YYY_ 0    0   0 8YYYY
-- %___  0   0 0    0   0 8___
-- `"""p 0   0 0    "o o" 8"""
-- YoooY "ooo" 8ooo  "8"  8oooo

solve : List Equation -> TypeChecker Substitution
solve eqs0 = go eqs0 []
where
	go : List Equation -> Substitution -> TypeChecker Substitution

	go [] subs' = pure subs'

	go ((Meta x ~~ Meta y) :: eqs) subs' with (x == y)
		| True = go eqs subs'
		| False = do
			eqs' <- traverse (evalWithSubs ((x, Meta y)::subs')) eqs
			go eqs' ((x, Meta y)::subs')

	go ((Meta x ~~ t2) :: eqs) subs' = do
		unless (not (occurs x t2))
			$ throw $ "Cannot unify because " ++ show (Meta x)
				++ " occurs in " ++ show t2
		eqs' <- traverse (evalWithSubs ((x,t2) :: subs')) eqs
		go eqs' ((x,t2) :: subs')

	go ((t1 ~~ Meta y) :: eqs) subs' = do
		unless (not (occurs y t1))
			$ throw $ "Cannot unify because " ++ show (Meta y)
				++ " occurs in " ++ show t1
		eqs' <- traverse (evalWithSubs ((y,t1) :: subs')) eqs
		go eqs' ((y,t1) :: subs')

	go ((Var x ~~ Var y) :: eqs) subs' = do
		unless (x == y)
			$ throw $ "Cannot unify variables " ++ show (Var x)
				++ " and " ++ show (Var y)
		go eqs subs'

	go ((DottedVar m1 x1 ~~ DottedVar m2 x2) :: eqs) subs' = do
		unless (m1 == m2 && x1 == x2)
			$ throw $ "Cannot unify symbols " ++ show (DottedVar m1 x1)
				++ " and " ++ show (DottedVar m2 x2)
		go eqs subs'

	go ((AbsoluteDottedVar m1 x1 ~~ AbsoluteDottedVar m2 x2) :: eqs) subs' = do
		unless (m1 == m2 && x1 == x2)
			$ throw $ "Cannot unify symbols " ++ show (AbsoluteDottedVar m1 x1)
				++ " and " ++ show (AbsoluteDottedVar m2 x2)
		go eqs subs'
	go ((Ann m1 t1 ~~ Ann m2 t2) :: eqs) subs' = go ((m1 ~~ m2) :: (t1 ~~ t2) :: eqs) subs'

	go ((Star ~~ Star) :: eqs) subs' = go eqs subs'

	go ((Pi plic1 a1 sc1 ~~ Pi plic2 a2 sc2) :: eqs) subs' = do
		unless (plic1 == plic2)
			$ throw $ "Mismatched plicities when trying to unify "
						++ show (Pi plic1 a1 sc1) ++ " with "
						++ show (Pi plic2 a2 sc2)
		i <- newName
		case (head' (names sc1), head' (names sc2)) of
			(Just h1, Just h2) => do
				let b1 = instantiate sc1 [Var (Generated h1 i)]
				let b2 = instantiate sc2 [Var (Generated h2 i)]
				go ((a1 ~~ a2) :: (b1 ~~ b2) :: eqs) subs'
			_ => throw "should not happen"

	go ((Lam plic1 sc1 ~~ Lam plic2 sc2) :: eqs) subs' = do
		unless (plic1 == plic2)
			$ throw $ "Mismatched plicities when trying to unify "
						++ show (Lam plic1 sc1) ++ " with "
						++ show (Lam plic2 sc2)
		i <- newName
		case (head' (names sc1), head' (names sc2)) of
			(Just h1, Just h2) => do
				let b1 = instantiate sc1 [Var (Generated h1 i)]
				let b2 = instantiate sc2 [Var (Generated h2 i)]
				go ((b1 ~~ b2) :: eqs) subs'
			_ => throw "should not happen"

	go ((App plic1 f1 a1 ~~ App plic2 f2 a2) :: eqs) subs' = do
		unless (plic1 == plic2)
			$ throw $ "Mismatched plicities when trying to unify "
						++ show (App plic1 f1 a1) ++ " with "
						++ show (App plic2 f2 a2)
		-- we should not assume all functions are injective
		-- so we will drop this equation simply, and check whether all
		-- holes are filled afterwards
		-- go ((f1 ~~ f2) :: (a1 ~~ a2) :: eqs) subs'
		go eqs subs'

	go ((Con c1 as1 ~~ Con c2 as2) :: eqs) subs' = do
		unless (c1 == c2)
			$ throw $ "Mismatching constructors " ++ show c1 ++ " and " ++ show c2
		unless (length as1 == length as2)
			$ throw $ "Mismatching number of arguments in "
						++ show (Con c1 as1) ++ " and "
						++ show (Con c2 as2)
		eqs' <- zipConArgs as1 as2
		go (eqs' ++ eqs) subs'
	where
		zipConArgs : List (Plict, Term) -> List (Plict, Term) -> TypeChecker (List Equation)
		zipConArgs [] [] = pure []
		zipConArgs ((plic1',a1')::as1') ((plic2',a2')::as2') = if plic1' == plic2'
				then do
					eqs' <- zipConArgs as1' as2'
					pure $ (a1' ~~ a2') :: eqs'
				else
					throw "Mismatching plicity."
		zipConArgs _ _ = throw "Mismatching number of arguments."

	go ((Case as1 mot1 cs1 ~~ Case as2 mot2 cs2) :: eqs) subs' = do
		unless(length as1 == length as2)
			$ throw $ "Mismatching number of case arguments in "
						++ show (Case as1 mot1 cs1) ++ " and "
						++ show (Case as2 mot2 cs2)
		unless (length cs1 == length cs2)
			$ throw $ "Mismatching number of clauses in "
						++ show (Case as1 mot1 cs1) ++ " and "
						++ show (Case as2 mot2 cs2)
		let argEqs = zipWith (~~) as1 as2
		motEqs <- compareCaseMotive mot1 mot2
		clauseEqs <- compareClauses cs1 cs2
		go (argEqs ++ motEqs ++ clauseEqs ++ eqs) subs'

	go ((RecordType tele1 ~~ RecordType tele2) :: eqs) subs' = do
		eqs' <- compareTelescope tele1 tele2
		go (eqs' ++ eqs) subs'

	go ((RecordCon fields1 ~~ RecordCon fields2) :: eqs) subs' = do
		eqs' <- compareFields fields1 fields2
		go (eqs' ++ eqs) subs'

	go ((Project m1 x1 ~~ Project m2 x2) :: eqs) subs' = do
		unless (x1 == x2)
			$ throw $ "Field names not equal: " ++ x1 ++ " and " ++ x2
		go ((m1 ~~ m2) :: eqs) subs'

	go ((m ~~ m') :: _) _ = throw $ "Terms not equal: " ++ show m ++ " and " ++ show m'

export
addSubstitutions : Substitution -> TypeChecker ()
addSubstitutions subs0 = do
	completeSubstitution subs0
	substituteContext
where
	completeSubstitution : Substitution -> TypeChecker ()
	completeSubstitution subs' = do
		subs <- substitution
		let subs2 = subs' ++ subs
		let subs2' = nubBy (\(a,_) => \(b,_) => a == b) (map (\(k,v) => (k, instantiateMetas subs2 v)) subs2)
		putSubstitution subs2'
	substituteContext : TypeChecker ()
	substituteContext = do
		ctx <- context
		subs <- substitution
		let ctx' = map (instCtx subs) ctx
		putContext ctx'
	where
		instCtx : Substitution -> ContextEntry -> ContextEntry
		instCtx subs (i, x, t) = (i, x, instantiateMetas subs t)

-- 0   0 8o  0 Y8Y 8YYYY 0   0
-- 0   0 8Yo 8  0  8___  "o o"
-- 0   0 8 Yo8  0  8"""    0
-- "ooo" 0   8 o8o 0       0

export
unify : Term -> Term -> TypeChecker ()
unify p q = do
	subs <- solve [p ~~ q]
	equate [p ~~ q] subs
	addSubstitutions subs

max_stars_repo_name: totalscript/totalscript

max_issues_repo_name: totalscript/totalscript

max_forks_repo_name: totalscript/totalscript


text:
module Example.Qtt.Problems

-- This module typechecks only with Idris 2 @fe602caa2, not newer. --

A : Type
B : Type
C : Type

k : A -> (1 _ : B) -> C

-- Typecheks with newer Idris (without linearity subtyping)
--mapK : List A -> List $ (1 _ : B) -> C
--mapK = map k

zipWith : (a -> b -> c) -> List a -> List b -> List c

-- Should compile when there was a linearity subtyping.
zipWithK : List A -> List B -> List C
zipWithK = zipWith k

-- Contra --

namespace InterfaceEdition

  interface Con w where
    constructor MkCon
    con : Nat -> w

  -- Instance первого порядка
  mkCon : (a -> b) -> Con (a -> b)
  mkCon f = MkCon {con = \_ => f}

  -- Would typecheck when linearity subtyping.
  bang : (a -> b) -> (1 _ : a) -> b
  bang f = let cc = mkCon f in con 5

-- Contra (record edition) --

namespace RecordEdition

  record Con w where
    constructor MkCon
    con : Nat -> w       -- `w` в контравариантной позиции

  conn : Con w => Nat -> w
  conn @{x} = con x

  mkCon : (a -> b) -> Con (a -> b)
  mkCon f = MkCon {con = \_ => f}

  -- Would typecheck when linearity subtyping.
  bang : (a -> b) -> (1 _ : a) -> b
  bang f = let cc = mkCon f in conn 5

max_stars_repo_name: buzden/code-in-lectures

max_issues_repo_name: buzden/code-in-lectures

max_forks_repo_name: buzden/code-in-lectures


text:
module BioFasta.Sequence

import Data.List
import Data.Maybe
import Data.Strings
import BioCore.Sequence
import BioFasta.Common
import BioFasta.Helpers
import System.File

public export
data Sequence = ||| A data type representing a fasta sequence.
                Seq SeqLabel SeqData (Maybe QualData)

public export
Eq Sequence where
  (==) (Seq l d mqd) (Seq l' d' mqd') = l == l' && d == d' && mqd == mqd'
  (==) _             _                = False

public export
Show Sequence where
  show (Seq l d mpd) = (show l) ++
                       (show d) ++
                       (show mpd)

public export
extractSeqLabel : Sequence -> SeqLabel
extractSeqLabel (Seq seqlabel _ _) = seqlabel

public export
extractSeqData : Sequence -> SeqData
extractSeqData (Seq _ seqdata _) = seqdata

public export
extractQualData : Sequence -> Maybe QualData
extractQualData (Seq _ _ qualdata) = qualdata

--Read FASTA file.--

export
||| Convert a FASTA-formatted line into a sequence.
mkSeq : List (List Char) -> Sequence
mkSeq []      = Seq (UnSL "") (UnSD "") Nothing
mkSeq (s::ss) = Seq (UnSL (pack (drop 1 s)))
                    (UnSD (pack (filter (not . isSpace) $ concat $ takeWhile isSeq ss)))
                    Nothing
                      where
                        isSeq : List Char -> Bool
                        isSeq s = if (not . isNil) s &&
                                     (all (isAlpha) s)
                                    then True
                                    else False

export
||| Convert a list of FASTA-formatted lines into a list of sequences.
||| Combines functionality of blocks and mkSeq.
mkSeqs : List (List Char) -> List Sequence
mkSeqs [] = []
mkSeqs s  = map mkSeq (map (lines') s)

public export
||| Read sequences from a FASTA-formatted file.
readFasta : String -> IO (List Sequence)
readFasta f = do Right fasta <- readFile f | Left err => do putStrLn "Could not read in FASTA file: " *> printLn err
                                                            pure []
                 pure (mkSeqs (smallBlocks (unpack fasta)))

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

--Write FASTA file.--

export
wHead : File -> SeqLabel -> IO ()
wHead f l = do Right addheadersign <- fPutStr f ">" | Left err => putStrLn "Could not add seqlabel header sign." *> printLn err
               Right addseqlabel <- fPutStr f (extractUnSL l) | Left err => putStrLn "Could not add sequence label." *> printLn err
               Right addnewline <- fPutStr f "\n" | Left err => putStrLn "Could not add newline following sequence label." *> printLn err
               pure ()

export
wFasta : File -> Sequence -> IO ()
wFasta f (Seq l d _) = do wHead f l
                          let ls          = splitsAt 59 (unpack (extractUnSD d))
                                                        (unpack (extractUnSD d))
                          let mappedls    = intersperse ['\n'] ls
                          let mappedlsstr = pack (concat mappedls)
                          Right addseqdata <- fPutStr f mappedlsstr | Left err => putStrLn "Could not add sequence data following the sequence label." *> printLn err
                          Right addnewline <- fPutStr f "\n" | Left err => putStrLn "Could not add newline following the sequence data." *> printLn err
                          pure ()

export
prepareWriteFasta : File -> List Sequence -> IO ()
prepareWriteFasta f = traverse_ (wFasta f)

public export
||| Write sequences to a FASTA-formatted file.
||| Line length is 60.
writeFasta : String -> List Sequence -> IO ()
writeFasta f ss = do Right hfastaout <- openFile f WriteTruncate | Left err => putStrLn "Could not open FASTA output file: " *> printLn err
                     prepareWriteFasta hfastaout ss
                     closeFile hfastaout

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


text:
module Vectors

import Data.Vect

%default total

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

sixInts : Vect 6 Int
sixInts = [5, 6, 7, 8, 9, 10]

tenInts : Vect 10 Int
tenInts = fourInts ++ sixInts

allLengths : Vect len String -> Vect len Nat
allLengths [] = []
allLengths (x :: xs) = length x :: allLengths xs

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
||| Ugly code for calculating and rendering a dragon curve
||| in SVG. TODO: Cleanup, document.
module Examples.Fractals.Dragon

import Data.DPair
import Data.List
import Data.List.TR
import Data.String

record Point where
  constructor P
  x,y : Int32

Num Point where
  fromInteger n = P (fromInteger n) 0
  P x1 y1 + P x2 y2 = P (x1 + x2) (y1 + y2)
  P x1 y1 * P x2 y2 = P (x1 * x2 - y1 * y2) (x1 * y2 + x2 * y1)

Neg Point where
  negate (P x y) = P (-x) (-y)
  P x1 y1 - P x2 y2 = P (x1 - x2) (y1 - y2)

rotate90 : Point -> Point
rotate90 (P x y) = P y (-x)

rotateAround90 : (origin : Point) -> Point -> Point
rotateAround90 o p = rotate90 (p - o) + o

Dragon : Type
Dragon = Subset (List Point) NonEmpty

0 lemma :  (as : List a)
        -> (v : a)
        -> (as2 : List a)
        -> NonEmpty (as ++ v :: as2)
lemma []       v as2 = IsNonEmpty
lemma (h :: t) v as2 = IsNonEmpty

firstDragon : Dragon
firstDragon = Element [0,800] IsNonEmpty

nextDragon : Dragon -> Dragon
nextDragon (Element (h :: t) prf) =
  let new = mapTR (rotateAround90 h) (reverse t)
   in Element (new ++ h :: t) (lemma new h t)

dragonSVG : (n : Nat) -> Dragon -> String
dragonSVG n (Element ps _) =
  let fact = pow 2 (cast (n + 2) / 2.0)
      scale = 1.0 / fact

      attr = fastConcat $ mapTR (\(P x y) => #"\#{show x}, \#{show y} "#) ps
      header =
        the String #"""
                   <svg version="1.1"
                        width="100%"
                        viewBox="0 0 1000 1000"
                        xmlns="http://www.w3.org/2000/svg">
                   """#
   in #"""
      \#{header}
        <polyline points="\#{attr}"
                  fill="none"
                  stroke="red"
                  vector-effect="non-scaling-stroke"
                  transform="translate (500,500) scale(\#{show scale})"
                  stroke-width="1"/>
      </svg>
      """#

export
mkDragons : (n : Nat) -> Subset (List String) NonEmpty
mkDragons n =
  let fd   = firstDragon
   in Element (dragonSVG 0 fd :: go fd n 1) IsNonEmpty
  where go : Dragon -> (rem : Nat) -> (iter : Nat) -> List String
        go _  0     _ = Nil
        go dr (S k) n =
          let nextDr = nextDragon dr
           in dragonSVG n nextDr :: go nextDr k (n+1)


text:
module GameState

import IdrisNet.Socket

import Effect.SDL
import Effect.State

import Data.Floats

PADDLE_DELTA : Int
PADDLE_DELTA = 2 -- How much to change Y-pos by

Width : Type
Width = Int

Height : Type
Height = Int

DEFAULT_WIDTH : Width
DEFAULT_WIDTH = 640

DEFAULT_HEIGHT : Height
DEFAULT_HEIGHT = 480

PADDLE_WIDTH : Width
PADDLE_WIDTH = 10

PADDLE_HEIGHT : Height
PADDLE_HEIGHT = 90

BALL_DIAMETER : Int
BALL_DIAMETER = 7

LAUNCH_VELOCITY : Int
LAUNCH_VELOCITY = 3

MAX_ANGLE : Float
MAX_ANGLE = (5 * pi) / 12

-- Network mode: Either a client, in which case we need the remote
data PongNetworkMode = PongClient
                     | PongServer

instance Eq PongNetworkMode where
  PongClient == PongClient = True
  PongServer == PongServer = True
  _ == _ = False

record PongBall : Type where
  MkPongBall :
  (pongBallPos : (Int, Int)) ->
  (pongBallXVel : Int) -> -- X Velocity
  (pongBallYVel : Int) -> -- Y Velocity
  (pongBallStuck : Bool) -> -- Whether the ball is attached to a paddle or not
  (pongBallHitLeft : Bool) -> -- Whether the ball last hit the left paddle
  PongBall

instance Show PongBall where
  show (MkPongBall pos xv yv stuck left) =
    "Pong ball: Position " ++ show pos ++ ", x vel: " ++
    show xv ++ ", stuck: " ++ show stuck ++ ", left: " ++ show left

-- Bookkeeping for current game state.
record GameState : Type where
  MkGameState :
   (pongWidth : Width) -> -- Canvas width
   (pongHeight : Height) -> -- Canvas height
   (pongBall : PongBall) ->
   (pongLeftPaddlePos : (Int, Int)) -> -- Position of the left paddle
   (pongRightPaddlePos : (Int, Int)) -> -- Position of the right paddle
   (pongIsUpPressed : Bool) -> -- Is up pressed? If so, decrease Y pos
   (pongIsDownPressed : Bool) -> -- Is down pressed? If so, increase Y pos
   (pongToLaunch : Bool) -> -- Has the launch button been pressed?
   (pongIsPaddleChanged : Bool) -> -- Has the direction of the paddle changed?
   (pongRemotePaddleUp : Bool) ->
   (pongRemotePaddleDown : Bool) ->
   (pongNetworkMode : PongNetworkMode) ->
   (pongRemoteAddr : SocketAddress) ->
   (pongRemotePort : Port) ->
   GameState

isServer : GameState -> Bool
isServer st = (pongNetworkMode st) == PongServer

initLPaddlePos : Width -> Height -> (Int, Int)
initLPaddlePos w h = (20, h `div` 2)

initRPaddlePos : Width -> Height -> (Int, Int)
initRPaddlePos w h = (w - (PADDLE_WIDTH + 20), h `div` 2)

newPaddlePos : (Int, Int) -> Bool -> Bool -> Width -> Height -> (Int, Int)
newPaddlePos (x, y) True _ w h = (x, (max (y - PADDLE_DELTA) 0))
newPaddlePos (x, y) _ True w h = (x, (min (y + PADDLE_DELTA) (h - PADDLE_HEIGHT)))
newPaddlePos (x, y) _ _ _ _ = (x, y)

initBall : Int -> Int -> PongBall
initBall lp_x lp_y = MkPongBall (ball_x, ball_y) 0 0 True True
  where ball_x = lp_x + PADDLE_WIDTH + (BALL_DIAMETER `div` 2)
        ball_y = lp_y + (PADDLE_HEIGHT `div` 2)

getLocalPaddlePos : { [STATE GameState] } Eff (Int, Int)
getLocalPaddlePos = do
  st <- get
  if isServer st then
    return $ pongLeftPaddlePos st
  else
    return $ pongRightPaddlePos st

updateRemotePaddlePos : { [STATE GameState] } Eff ()
updateRemotePaddlePos = do
  st <- get
  let lpp = pongLeftPaddlePos st
  let rpp = pongRightPaddlePos st
  let up = pongRemotePaddleUp st
  let down = pongRemotePaddleDown st
  let w = pongWidth st
  let h = pongHeight st
  if (isServer st) then do
    let new_pos = newPaddlePos rpp up down w h
    put $ record { pongRightPaddlePos = new_pos } st
  else do
    let new_pos = newPaddlePos lpp up down w h
    put $ record { pongLeftPaddlePos = new_pos } st

updateLocalPaddlePos : { [STATE GameState] } Eff Bool
updateLocalPaddlePos = do
  st <- get
  let lpp = pongLeftPaddlePos st
  let rpp = pongRightPaddlePos st
  let w = pongWidth st
  let h = pongHeight st
  let up = pongIsUpPressed st
  let down = pongIsDownPressed st
  let paddle_changed = pongIsPaddleChanged st
  if isServer st then do
    let new_pos = newPaddlePos lpp up down w h
    put $ record { pongLeftPaddlePos = new_pos,
                   pongIsPaddleChanged = False} st
    return paddle_changed
  else do
    let new_pos = newPaddlePos rpp up down w h
    put $ record { pongRightPaddlePos = new_pos,
                   pongIsPaddleChanged = False } st
    return paddle_changed

drawPaddles : { [SDL_ON, STATE GameState] } Eff ()
drawPaddles = do st <- get
                 drawPaddle (pongLeftPaddlePos st)
                 drawPaddle (pongRightPaddlePos st)
  where drawPaddle : (Int, Int) -> { [SDL_ON] } Eff ()
        drawPaddle (x, y) = rectangle black x y PADDLE_WIDTH PADDLE_HEIGHT

drawBall : { [SDL_ON, STATE GameState] } Eff ()
drawBall = do
  st <- get
  let (MkPongBall (x, y) _ _ _ _) = pongBall st
  ellipse blue x y BALL_DIAMETER BALL_DIAMETER

initState : Width -> Height -> PongNetworkMode -> SocketAddress -> Port -> GameState
initState w h = let (lp_x, lp_y) = initLPaddlePos w h in
  MkGameState w h (initBall lp_x lp_y)  (lp_x, lp_y) (initRPaddlePos w h)
    False False False False False False

-- Update communication:
--  * Ball: The server does collision detection and so on, and only sends details of changes:
--          that is, if the direction of the ball changes due to a collision, or if it goes out of bounds.
--
--          The client updates the local ball position based on the latest information from the server.
--    (aside: it might also be prudent to periodically (ie, every 200ms or so) send a "back on track" msg
--
--  * Paddle: I think we can get away with sending an update every time the paddle moves. If not, that's
--            fine: we can probably just send the deltas again.

launchBall : { [STATE GameState] } Eff ()
launchBall = do
  st <- get
  let ball' = record { pongBallXVel = LAUNCH_VELOCITY, pongBallStuck = False } (pongBall st)
  put $ record { pongBall = ball' } st

requiresLaunching : { [STATE GameState] } Eff Bool
requiresLaunching = do
  st <- get
  let ball = pongBall st
  -- In either case, reset the toLaunch flag
  put $ record { pongToLaunch = False } st
  return (pongToLaunch st && (pongBallStuck ball))

updateBallPos : { [STATE GameState] } Eff ()
updateBallPos = do
  st <- get
  let ball = pongBall st
  let (bp_x, bp_y) = pongBallPos ball
  let ball' =
    if (pongBallStuck ball) then
      (uncurry initBall) (pongLeftPaddlePos st)
    else
      record { pongBallPos = (bp_x + (pongBallXVel ball),
                              bp_y + (pongBallYVel ball)) } ball
  put $ record { pongBall = ball' } st

inBox : PongBall -> (Int, Int) -> Width -> Height -> Bool
inBox (MkPongBall (pb_x, pb_y) _ _ _ _) (x, y) w h =
  pb_x > x && pb_x < (x + w) && pb_y > y && pb_y < (y + h)

hitPaddle : PongBall -> (Int, Int) -> Bool
hitPaddle pb pos = inBox pb pos PADDLE_WIDTH PADDLE_HEIGHT

-- Takes paddle position, ball position, returns movement velocities.
-- Funky angle logic from here: http://gamedev.stackexchange.com/questions/4253/how-do-you-calculate-where-a-ball-should-go-when-it-bounces-off-the-bar
paddleBounceVelocities : (Int, Int) -> (Int, Int) -> (Int, Int)
paddleBounceVelocities (p_x, p_y) (b_x, b_y) = (x_vel, y_vel)
  where rel_intersect : Float
        rel_intersect = (cast p_y) + ((cast PADDLE_HEIGHT) / 2) - (cast b_y)
        normalised_intersect : Float
        normalised_intersect = rel_intersect / ((cast PADDLE_HEIGHT) / 2)
        bounce_angle : Float
        bounce_angle = normalised_intersect * MAX_ANGLE
        x_vel : Int
        x_vel = cast $ (cos bounce_angle) * (cast LAUNCH_VELOCITY)
        y_vel : Int
        y_vel = (-(cast $ (sin bounce_angle) * (cast LAUNCH_VELOCITY)))

-- Only check the opposite paddle to the one that was last hit.
checkPaddleCollisions : { [STATE GameState] } Eff Bool
checkPaddleCollisions = do
  st <- get
  let ball = pongBall st
  let bp = pongBallPos ball
  let lpp = pongLeftPaddlePos st
  let rpp = pongRightPaddlePos st
  let left = pongBallHitLeft ball
  if (left && hitPaddle ball rpp) then do
    let (x_vel, y_vel) = paddleBounceVelocities rpp bp
    let ball' = record { pongBallXVel = -x_vel,
                         pongBallYVel = y_vel,
                         pongBallHitLeft = False } ball
    put $ record { pongBall = ball' } st
    return True
  else if ((not left) && hitPaddle ball lpp) then do
    let (x_vel, y_vel) = paddleBounceVelocities lpp bp
    let ball' = record { pongBallXVel = x_vel,
                         pongBallYVel = y_vel,
                         pongBallHitLeft = True } ball
    put $ record { pongBall = ball' } st
    return True
  else
    return False

-- Check the left and right walls
checkLRBounds : { [STATE GameState] } Eff Bool
checkLRBounds = do
  st <- get
  let (lp_x, lp_y) = pongLeftPaddlePos st
  let (MkPongBall (x, y) _ _ _ _) = pongBall st
  if (x < 0 || x > (pongWidth st)) then do
    put $ record { pongBall = initBall lp_x lp_y } st
    return True
  else
    return False

-- Check top and bottom walls
checkTBBounds : { [STATE GameState] } Eff Bool
checkTBBounds = do
  st <- get
  let ball = pongBall st
  let (x, y) = pongBallPos ball
  let yvel = pongBallYVel ball

  if (y < 0) then do
    let ball' = record { pongBallPos = (x, 0), pongBallYVel = yvel * -1 } ball
    put $ record { pongBall = ball' } st
    return True
  else if (y > pongHeight st) then do
    let ball' = record { pongBallPos = (x, pongHeight st), pongBallYVel = yvel * -1 } ball
    put $ record { pongBall = ball' } st
    return True
  else return False
 -- if (y < 0 || y > (pongHeight st)) then do

-- Updating ball position on the server peer: what we'll need to do here is firstly check if
-- the ball needs "launching" -- that is, it's on a paddle, and space has been pressed.
-- If so, we launch it (launchBall).
-- If not, we do collision checking: checking that the ball has hit the t&b walls --> reverse Y velocity
--                                   checking that the ball has hit the paddles --> crazy paddle stuff
--                                   checking that the ball has hit the R&L walls --> reset
updateBallServer : { [STATE GameState] } Eff Bool
updateBallServer = do
  requires_launching <- requiresLaunching
  when requires_launching launchBall
  -- TEMP: Just so we know the basics work...
  paddle_collision <- checkPaddleCollisions
  lr_bounds <- checkLRBounds
  tb_bounds <- checkTBBounds
  updateBallPos -- Apply X and Y velocities to move the ball
  return $ requires_launching ||  paddle_collision ||  lr_bounds || tb_bounds


text:
module Idris.IDEMode.Pretty

import Protocol.IDE
import Idris.Pretty
import Idris.Doc.Annotations

------------------------------------------------------------------------
-- Text properties supported by the IDE mode
------------------------------------------------------------------------

export
syntaxToProperties : IdrisSyntax -> Maybe Properties
syntaxToProperties syn = mkDecor <$> syntaxToDecoration syn

export
annToProperties : IdrisAnn -> Maybe Properties
annToProperties Warning       = Just $ MkProperties
                                 { decor = Just Postulate
                                 , format = Just Bold
                                 }
annToProperties Error         = Just $ MkProperties
                                 { decor = Just $ Postulate
                                 , format = Just Bold
                                 }
annToProperties ErrorDesc     = Nothing
annToProperties FileCtxt      = Just $ mkDecor Typ
annToProperties Code          = Just $ mkDecor Bound
annToProperties Meta          = Just $ mkDecor Function
annToProperties (Syntax syn)  = syntaxToProperties syn
annToProperties UserDocString = Just $ mkDecor Comment

export
docToProperties : IdrisDocAnn -> Maybe Properties
docToProperties Header        = pure $ mkFormat Underline
docToProperties Deprecation   = pure $ mkFormat Bold
docToProperties Declarations  = Nothing
docToProperties (Decl _)      = Nothing
docToProperties DocStringBody = Nothing
docToProperties UserDocString = Nothing
docToProperties (Syntax syn)  = syntaxToProperties syn


text:
-- ---------------------------------------------------------------- [ Time.idr ]
--
-- This RFC specifies a standard for the ARPA Internet community.
-- Hosts on the ARPA Internet that choose to implement a Time Protocol
-- are expected to adopt and implement this standard.
--
-- This protocol provides a site-independent, machine readable date
-- and time.  The Time service sends back to the originating source
-- the time in seconds since midnight on January first 1900.
--
-- One motivation arises from the fact that not all systems have a
-- date/time clock, and all are subject to occasional human or machine
-- error.  The use of time-servers makes it possible to quickly
-- confirm or correct a system's idea of the time, by making a brief
-- poll of several independent sites on the network.
--
-- http://tools.ietf.org/html/rfc868
--
-- --------------------------------------------------------------------- [ EOH ]
module RFC.Time

import Effects

import Effect.Default
import Effect.StdIO

import System.Protocol

||| This protocol provides a site-independent, machine readable date
||| and time.  The Time service sends back to the originating source
||| the time in seconds since midnight on January first 1900.
|||
||| Enhanced version of the protocol.
total
timeProtocol : Protocol ['Client, 'Server] ()
timeProtocol = do
    'Client ==> 'Server | Maybe String
    'Server ==> 'Client | Either String Int
    Done

||| This protocol provides a site-independent, machine readable date
||| and time.  The Time service sends back to the originating source
||| the time in seconds since midnight on January first 1900.
|||
||| A naive version of the protocol.
total
timeProtocol' : Protocol ['Client, 'Server] ()
timeProtocol' = do
    'Server ==> 'Client | Either String Int
    Done

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

max_stars_repo_name: jfdm/idris-protocol-examples

max_issues_repo_name: jfdm/idris-protocol-examples

max_forks_repo_name: jfdm/idris-protocol-examples


text:
||| Additional properties/lemmata of Nats involving order
module Data.Nat.Order.Properties

import Syntax.PreorderReasoning
import Syntax.PreorderReasoning.Generic
import Data.Nat
import Data.Nat.Order
import Data.Nat.Order.Strict
import Decidable.Equality
import Decidable.Order.Strict
import Data.Bool.Decidable

%default total
export
LTESuccInjectiveMonotone : (m, n : Nat) -> Reflects (m `LTE` n) b -> Reflects (S m `LTE` S n) b
LTESuccInjectiveMonotone m n (RTrue      m_lte_n) = RTrue  $ LTESucc m_lte_n
LTESuccInjectiveMonotone m n (RFalse not_m_lte_n) = RFalse $ \case
                                                               LTESucc m_lte_n => not_m_lte_n m_lte_n

export
lteReflection : (a, b : Nat) -> Reflects (a `LTE` b) (a `lte` b)
lteReflection 0 b = RTrue LTEZero
lteReflection (S k) 0 = RFalse $ \sk_lte_z => absurd sk_lte_z
lteReflection (S a) (S b) = LTESuccInjectiveMonotone a b (lteReflection a b)

export
ltReflection : (a, b : Nat) -> Reflects (a `LT` b) (a `lt` b)
ltReflection a = lteReflection (S a)

-- For example:
export
lteIsLTE : (a, b : Nat) -> a `lte` b = True -> a `LTE` b
lteIsLTE  a b prf = invert (replace {p = Reflects (a `LTE` b)} prf (lteReflection a b))

export
ltIsLT : (a, b : Nat) -> a `lt` b = True -> a `LT` b
ltIsLT  a = lteIsLTE (S a)

export
notlteIsNotLTE : (a, b : Nat) -> a `lte` b = False -> Not (a `LTE` b)
notlteIsNotLTE a b prf = invert (replace {p = Reflects (a `LTE` b)} prf (lteReflection a b))

export
notltIsNotLT : (a, b : Nat) -> a `lt` b = False -> Not (a `LT` b)
notltIsNotLT a = notlteIsNotLTE (S a)

export
notlteIsLT : (a, b : Nat) -> a `lte` b = False -> b `LT` a
notlteIsLT a b prf = notLTImpliesGTE $
                       \prf' =>
                         (invert $ replace {p = Reflects (S a `LTE` S b)} prf
                                 $ lteReflection (S a) (S b)) prf'

export
notltIsGTE : (a, b : Nat) -> (a `lt` b) === False -> a `GTE` b
notltIsGTE a b p = notLTImpliesGTE (notlteIsNotLTE (S a) b p)

-- The converse to lteIsLTE:
export
LteIslte : (a, b : Nat) -> a `LTE` b -> a `lte` b = True
LteIslte  a b a_lt_b = reflect (lteReflection a b) a_lt_b

-- The converse to lteIsLTE with negation
export
notLteIsnotlte : (a, b : Nat) -> Not (a `LTE` b) -> a `lte` b = False
notLteIsnotlte a b not_a_lte_b = reflect (lteReflection a b) not_a_lte_b

-- The converse to lteIsLTE:
export
GTIsnotlte : (a, b : Nat) -> b `LT` a -> a `lte` b = False
GTIsnotlte a b prf =
  notLteIsnotlte a b $ \contra =>
    succNotLTEpred $ transitive {rel = LTE} prf contra

||| Subtracting a number gives a smaller number
export
minusLTE : (a,b : Nat) -> (b `minus` a) `LTE` b
minusLTE a      0    = LTEZero
minusLTE 0     (S b) = reflexive {rel = LTE}
minusLTE (S a) (S b) =
  transitive {rel = LTE}
    (minusLTE a b)
    (lteSuccRight (reflexive {rel = LTE}))

||| Subtracting a positive number gives a strictly smaller number
export
minusPosLT : (a,b : Nat) -> 0 `LT` a -> a `LTE` b -> (b `minus` a) `LT` b
minusPosLT 0     b     z_lt_z           a_lte_b impossible
minusPosLT (S a) 0     z_lt_sa          a_lte_b impossible
minusPosLT (S a) (S b) z_lt_sa          a_lte_b = LTESucc (minusLTE a b)

-- This is the opposite of the convention in `Data.Nat`, but 'monotone on the left' means the below
export
multLteMonotoneRight : (l, a, b : Nat) -> a `LTE` b -> l*a `LTE` l*b
multLteMonotoneRight  0    a b _ = LTEZero
multLteMonotoneRight (S k) a b a_lte_b = CalcWith {leq = LTE} $
  |~ (1 + k) * a
  ~~ a +  k*a    ...(Refl)
  <~ b +  k*a    ...(plusLteMonotoneRight (k*a) a b a_lte_b)
  <~ b +  k*b    ...(plusLteMonotoneLeft  b (k*a) (k*b) $
                     multLteMonotoneRight k    a     b   a_lte_b)
  ~~ (1 + k) * b ...(Refl)

export
multLteMonotoneLeft : (a, b, r : Nat) -> a `LTE` b -> a*r `LTE` b*r
multLteMonotoneLeft a b r a_lt_b =
  rewrite multCommutative a r in
  rewrite multCommutative b r in
  multLteMonotoneRight r a b a_lt_b


text:
module Bltnat

howdy : Nat
howdy = 25

public export
beq_nat : Nat -> Nat -> Bool
beq_nat Z Z = True
beq_nat Z (S k) = False
beq_nat (S k) Z = False
beq_nat (S k) (S j) = beq_nat k j

leb : Nat -> Nat -> Bool
leb Z _ = True
leb (S k) (S j) = leb k j
leb _ _ = False
-- alternate and with better ordering: leb (S k) Z = False

tl1 : leb 2 2 = True
tl1 = Refl
tl2 : leb 2 4 = True
tl2 = Refl
tl3 : leb 2555 1 = False
tl3 = Refl

blt_nat : Nat -> Nat -> Bool
blt_nat k j = case beq_nat k j of
                   False => leb k j
                   True => False

tblt1 : blt_nat 2 2 = False
tblt1 = Refl
tblt2 : blt_nat 2 4 = True
tblt2 = Refl
tblt3 : blt_nat 2342 2 = False
tblt3 = Refl


text:
import Data.Vect

-- Exercise 1
Matrix : Nat -> Nat -> Type
Matrix rows cols = Vect rows (Vect cols Double)

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

--Exercise 2
data Format = Number Format
            | Str Format
            | Lit String Format
            | Chr Format
            | Dbl Format
            | End

PrintfType : Format -> Type
PrintfType (Number fmt)  = (i : Int) -> PrintfType fmt
PrintfType (Str fmt)     = (str : String) -> PrintfType fmt
PrintfType (Lit str fmt) = PrintfType fmt
PrintfType (Chr fmt)     = (chr : Char) -> PrintfType fmt
PrintfType (Dbl fmt)     = (dbl : Double) -> PrintfType fmt
PrintfType End           = String

printfFmt : (fmt : Format) -> (acc : String) -> PrintfType fmt
printfFmt (Number fmt) acc = \i => printfFmt fmt (acc ++ show i)
printfFmt (Str fmt) acc = \str => printfFmt fmt (acc ++ str)
printfFmt (Lit lit fmt) acc = printfFmt fmt (acc ++ lit)
printfFmt (Chr fmt) acc = \c => printfFmt fmt (acc ++ show c)
printfFmt (Dbl fmt) acc = \d => printfFmt fmt (acc ++ show d)
printfFmt End acc = acc

toFormat : (xs : List Char) -> Format
toFormat [] = End
toFormat ('%' :: 'd' :: chars) = Number (toFormat chars)
toFormat ('%' :: 's' :: chars) = Str (toFormat chars)
toFormat ('%' :: 'c' :: chars) = Chr (toFormat chars)
toFormat ('%' :: 'f' :: chars) = Dbl (toFormat chars)
toFormat ('%' :: chars) = Lit "%" (toFormat chars)
toFormat (c :: chars) = case toFormat chars of
                             (Lit lit chars') => Lit (strCons c lit) chars'
                             fmt => Lit (strCons c "") fmt

printf : (fmt : String) -> PrintfType (toFormat (unpack fmt))
printf fmt = printfFmt _ ""

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

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


text:
import Data.String

import System
import System.Info

main : IO ()
main = do
    (contents, 0) <- run $ "echo " ++ escapeArg "Hello, world"
        | (_, err) => printLn err
    printLn $ trim contents

    let cmd : List String = if not isWindows
                               then ["printf", "Hello, %s", "$PATH"]
                               else ["echo", "Hello, $PATH"]
    (contents, 0) <- run cmd
        | (_, err) => printLn err
    printLn $ trim contents

    printLn !(run ["exit", "17"])


text:
module Algebra.Solver.Semiring.Prod

import Algebra.Solver.Semiring.Expr
import public Algebra.Solver.Prod
import Algebra.Solver.Semiring.Util

%default total

||| Evaluate products of variables each raised to
||| given exponent.
|||
||| Every arithmetic expression in a commutative ring
||| can be represented as a sum of products of the variables
||| each raised by an exponent and multiplied by a constant
||| factor. For instance, expression `x + x * (y + z + z)`
||| gets normalized to `x + x * y + 2 * x * z`.
public export
eprod : Semiring a => {as : List a} -> Prod a as -> a
eprod {as = []}      []        = 1
eprod {as = x :: xs} (e :: es) = pow x e * eprod es

--------------------------------------------------------------------------------
--          Proofs
--------------------------------------------------------------------------------

||| Proof that `one` evaluates to 1.
export
0 pone : Semiring a => (as : List a) -> eprod (one {as}) === 1
pone []        = Refl
pone (x :: xs) = Calc $
  |~ 1 * eprod (one {as = xs})
  ~~ 1 * 1                     ... cong (1 * ) (pone xs)
  ~~ 1                         ... multOneRightNeutral

||| Proof that `fromVar x` evaluates to `x`.
export
0 pvar :  Semiring a
       => (as : List a)
       -> (e  : Elem x as)
       -> eprod (fromVar {as} e) === x
pvar (x :: vs) Here      = Calc $
  |~ (x * 1) * eprod (one {as = vs})
  ~~ (x * 1) * 1                     ... cong ((x*1) *) (pone vs)
  ~~ x * 1                           ... multOneRightNeutral
  ~~ x                               ... multOneRightNeutral

pvar (v :: vs) (There y) = Calc $
  |~ 1 * eprod (fromVar {as = vs} y)
  ~~ 1 * x                           ... cong (1*) (pvar vs y)
  ~~ x                               ... multOneLeftNeutral

pvar [] Here impossible
pvar [] (There y) impossible

||| Proof that evaluation of a multiplication of products
||| is the same as multiplying the results of evaluating each
||| of them.
export
0 pmult :  Semiring a
        => (p,q : Prod a as)
        -> eprod (mult p q) === eprod p * eprod q
pmult []        []        = sym multOneLeftNeutral
pmult {as = h :: t} (x :: xs) (y :: ys) = Calc $
  |~ pow h (x + y) * eprod (mult xs ys)
  ~~ (pow h x * pow h y) * eprod (mult xs ys)
     ... cong (* eprod (mult xs ys)) (ppow x y h)
  ~~ (pow h x * pow h y) * (eprod xs * eprod ys)
     ... cong ((pow h x * pow h y) *) (pmult xs ys)
  ~~ (pow h x * eprod xs) * (pow h y * eprod ys)
     ... Util.m1324


text:
module Markdown

import Markdown.Lexer
import Markdown.Parser

import Text.Bounded

import public Markdown.Data

%default covering

||| Parse a Markdown string
export
parse : String -> Maybe Markdown
parse x = parseMarkdown !(lexMarkdown x)

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Test.PP

import Text.PrettyPrint.Prettyprinter
import Text.Show.Pretty
import Test.Mini

doPP : String -> String
doPP s = maybe "" (show . valToDoc {ann = ()}) $ parseValue s

testPP : String -> List (String,String) -> IO Bool
testPP s ps = do putStrLn ("Pretty printing " ++ s)
                 report $ runEq doPP ps

pair : a -> (a,a)
pair x = (x, x)

export
ppTest : IO Bool
ppTest = testAll
  [ testPP "naturals" $ map pair ["0","123","10000"]

  , testPP "chars" $ map pair ["'a'", "'0'", "'Z'"]

  , testPP "doubles" $ map pair ["1.232", "1.0e-12", "16.5E3"]

  , testPP "strings" $ map pair ["\"1.232\"", "\"ab cde\"", "\"foo\""]

  , testPP "negative" $ map pair ["-12", "-1.233e12", "-0"]

  , testPP "lists" [ ("[1,2,3]", "[ 1 , 2 , 3 ]")
                   , ("[]", "[]")
                   , ("['a','b','c']", "[ 'a' , 'b' , 'c' ]")
                   ]
  , testPP "identifiers" $
      map pair ["Ident", "Foo", "H", "_foo"]

  , testPP "arity 1 cons" $
      map pair ["Ident 12", "Foo 'a'", "H ()", "_foo 1.22"]

  , testPP "arity 2 cons" $
      map pair ["Ident 12 'a'", "Foo 'a' \"bar\"", "H () 12", "_foo 1.22 (-1)"]

  , testPP "nested cons" $
      map pair ["Ident 12 (Foo 'a') (Maybe 12)"
               , "Foo (Left 'a') (MkPair \"bar \" 1.20)"
               , "Bracket (TH 12) (Element 12 _) (-12.1)"
               ]
  ]


text:
-- ReadNum.idr

-- Reading and validating a number from stdin

module ReadNum

export
readNumber : IO (Maybe Nat)
readNumber = do
  input <- getLine
  if all isDigit (unpack input)
     then pure (Just (cast input))
     else pure Nothing

readNumbers : IO (Maybe (Nat, Nat))
readNumbers =
  do Just num1_ok <- readNumber | Nothing => pure Nothing
     Just num2_ok <- readNumber | Nothing => pure Nothing
     pure (Just (num1_ok, num2_ok))

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
data BNat = BZ | O BNat | E BNat

bnat_ind : {0 p : BNat -> Type}
        -> p BZ
        -> ((bn : BNat) -> p bn -> p (O bn))
        -> ((bn : BNat) -> p bn -> p (E bn))
        -> (bn : BNat) -> p bn
bnat_ind pbz po pe = go
 where
  go : (bn : BNat) -> p bn
  go BZ = ?pbz_hole
  go (O x) = po x (go x)
  go (E x) = pe x (go x)


text:
module Flexidisc.Record.Connection

import Data.Fun
import Data.Vect

import Flexidisc.Function
import Flexidisc.Record.Read
import Flexidisc.Record.Transformation
import Flexidisc.Record.Type

%default total
%access export

||| A type alias for `RecordM` that can be use to inject a given type in a record
public export
Injector : (k : Type) -> Header k -> Type -> Type
Injector k header ty = RecordM ((|->) ty) k header

||| Use an injector to transform a rigid record into a flexible one
toRecord : Injector k header src -> src -> Record k header
toRecord = unwrap . sequence

||| A `TypeList` describe how to build a vector of type from a record
data TypeList : Vect n k -> Vect n Type -> Header k -> Type where
  Nil  : TypeList [] [] header
  (::) : Row x ty header -> TypeList xs ts header -> TypeList (x::xs) (ty::ts) header

||| Transform a flexible Record into a rigid one
fromRecord : Fun ts a -> (xs : Vect n k) -> Record k header -> {auto prf : TypeList xs ts header} -> a
fromRecord f [] r {prf = []} = f
fromRecord f (_ :: xs) r {prf = loc::_} = fromRecord (f $ r `atRow` loc) xs r

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module Sub04Apply54x48

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total
-- %language ElabReflection

-- 3(18x+16) --A[6,-4]->B[1,-2]--> 3(4x+3)
ab54x30To12x9 :
  (l:Nat) -> P (S (S (S (S (plus (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                                  (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                            (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l)))))))))))) 2
    -> P (S (S (S (plus (plus l l) (plus l l))))) 2
ab54x30To12x9 l prf =
  let prf2 = lvDown (S (S (S (S (plus (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                                  (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                            (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l)))))))))))) 2
                    prf in
    let prf3 = ab54x30To12x9' l prf2 in lvDown (S (S (S (plus (plus l l) (plus l l))))) 3 prf3

export
apply54x48 : P (S (S (S (S (plus (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                                  (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                            (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l)))))))))))) 2
  -> (m : Nat **
        (LTE (S m)
             (S (S (S (S (plus (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l)))) (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                               (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l)))))))))))),
         P m 2))
apply54x48 {l} col = let col2 = ab54x30To12x9 l col in ((S (S (S (plus (plus l l) (plus l l))))) ** (lte54x48 l, col2)) where
  lte54x48 : (l:Nat) -> LTE (S (S (S (S (plus (plus l l) (plus l l))))))
                            (S (S (S (S (plus (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l)))) (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                                              (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))))))
  lte54x48 Z = (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc) LTEZero
  lte54x48 (S k) = let lemma = lte54x48 k in
    rewrite (sym (plusSuccRightSucc k k)) in
    rewrite (sym (plusSuccRightSucc (plus k k) (S (plus k k)))) in
    rewrite (sym (plusSuccRightSucc (plus k k) (plus k k))) in
    rewrite (sym (plusSuccRightSucc (plus k k) k)) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) k) (S (S (S (S (plus (plus k k) k))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) k) (S (S (S (plus (plus k k) k)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) k) (S (S (plus (plus k k) k))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))  (S (S (S (S (S (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k)))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))  (S (S (S (S (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))  (S (S (S (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))  (S (S (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))  (S (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))  (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (S (S (plus (plus k k) k)))) (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))))))  (S (S (S (S (S (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k)))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (S (S (plus (plus k k) k)))) (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))))))  (S (S (S (S (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (S (S (plus (plus k k) k)))) (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))))))  (S (S (S (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (S (S (plus (plus k k) k)))) (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))))))  (S (S (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (S (S (plus (plus k k) k)))) (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))))))  (S (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (S (S (plus (plus k k) k)))) (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))))))  (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))))))) in
      (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc) lemma


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

import System.File

data Bracket = P | S | B | L
Eq Bracket where
  P == P = True
  S == S = True
  B == B = True
  L == L = True
  _ == _ = False
data Chunk = Open Bracket | Close Bracket

findMissing : List Bracket -> List Chunk -> List Bracket
findMissing s [] = s
findMissing s ((Open x) :: xs) = findMissing (x :: s)  xs
findMissing [] ((Close x) :: xs) = []
findMissing (y :: ys) ((Close x) :: xs) = if x == y
                                       then findMissing ys xs
                                       else []

parseChunk : Char -> Maybe Chunk
parseChunk '(' = Just $ Open P
parseChunk ')' = Just $ Close P
parseChunk '[' = Just $ Open S
parseChunk ']' = Just $ Close S
parseChunk '{' = Just $ Open B
parseChunk '}' = Just $ Close B
parseChunk '<' = Just $ Open L
parseChunk '>' = Just $ Close L
parseChunk _ = Nothing
parseChunks : List Char -> List (Maybe Chunk)
parseChunks l = parseChunk <$> l

score : Bracket -> Nat
score P = 1
score S = 2
score B = 3
score L = 4

run : String -> IO ()
run s = do let l = filter (\l => length l > 0) $ findMissing [] . catMaybes . parseChunks . unpack <$> lines s
           let s = sort $ (\bs => foldl (\a => \n => 5 * a + n ) 0 $ score <$> bs) <$> l
           let h = (div (length s) 2) + 1
           putStrLn $ show $ head' $ reverse $ take h s

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


text:
{-
Copyright 2020, Mokshasoft AB (mokshasoft.com)

This software may be distributed and modified according to the terms of
the BSD 2-Clause license. Note that NO WARRANTY is provided.
See "LICENSE_BSD2.txt" for details.
-}

module Main

import FreeRTOS.Queue
import FreeRTOS.Task.Control as TC
import FreeRTOS.Task.Utils
import Utils

{-
 - Printer loop
 -}

printer : Int -> IO ()
printer 0 = do
    vDirectPrintMsg "Stopping printer thread\n"
    TC.delete
printer n = do
    vDirectPrintMsg "Printing from printer..\n"
    delay 2000
    printer (n - 1)

{-
 - Receiver of items from Queue
 -}

receiver : Int -> QueueHandle Int -> IO ()
receiver 0 handle = do
    vDirectPrintMsg "Stopping receiver thread\n"
    delete handle
    TC.delete
receiver n handle = do
    val <- get handle
    vDirectPrintMsg $ "received: " ++ show val ++ "\n"
    delay 1000
    receiver (n - 1) handle

{-
 - Sender of items to Queue
 -}

sender : Int -> QueueHandle Int -> IO ()
sender 0 _ = do
    vDirectPrintMsg "Stopping sender thread\n"
    TC.delete
sender n handle = do
    let val = 123
    vDirectPrintMsg $ "sending " ++ show val ++ "\n"
    put handle val
    delay 1000
    sender (n - 1) handle

{-
 - Main program
 -}

main : IO ()
main = do
    vDirectPrintMsg "Hello, Idris Unikernel\n"
    -- Start printer
    Just pidPrinter <- TC.create (printer 5) |
        Nothing => vDirectPrintMsg "starting printer failed\n"
    -- Create queue
    Just handle <- create Int 2 |
        Nothing => vDirectPrintMsg "Could not create queue\n"
    -- Start receiver
    Just pidRec <- TC.create (receiver 3 handle) |
        Nothing => vDirectPrintMsg "starting receiver failed\n"
    -- Start sender
    Just pidSend <- TC.create (sender 3 handle) |
        Nothing => vDirectPrintMsg "starting sender failed\n"
    vDirectPrintMsg "sender and receiver started\n"

max_stars_repo_name: mokshasoft/FreeRTOS-community-ports

max_issues_repo_name: mokshasoft/FreeRTOS-community-ports

max_forks_repo_name: mokshasoft/FreeRTOS-community-ports


text:
||| Spec: https://webassembly.github.io/spec/core/syntax/modules.html#element-segments
module WebAssembly.Structure.Modules.ElementSegments

import WebAssembly.Structure.Types
import WebAssembly.Structure.Instructions
import WebAssembly.Structure.Modules.Indices

import Decidable.Equality

-- Definition

public export
record Elem where
  constructor MkElem
  table   : TableIdx
  offset : Expr
  init   : List FuncIdx

-- Equality

total public export
lemma_elem__table_injective : ((t1 = t2) -> Void) -> (MkElem t1 o1 i1 = MkElem t2 o2 i2) -> Void
lemma_elem__table_injective t1_not_t2 Refl = t1_not_t2 Refl

total public export
lemma_elem__offset_injective : ((o1 = o2) -> Void) -> (MkElem t1 o1 i1 = MkElem t2 o2 i2) -> Void
lemma_elem__offset_injective o1_not_o2 Refl = o1_not_o2 Refl

total public export
lemma_elem__init_injective : ((i1 = i2) -> Void) -> (MkElem t1 o1 i1 = MkElem t2 o2 i2) -> Void
lemma_elem__init_injective i1_not_i2 Refl = i1_not_i2 Refl

-- Dedidable Equality

public export
implementation DecEq Elem where
  decEq (MkElem t1 o1 i1) (MkElem t2 o2 i2) = case decEq t1 t2 of
    No t1_not_t2 => No $ lemma_elem__table_injective t1_not_t2
    Yes Refl     => case decEq o1 o2 of
      No o1_not_o2 => No $ lemma_elem__offset_injective o1_not_o2
      Yes Refl     => case decEq i1 i2 of
        No i1_not_i2 => No $ lemma_elem__init_injective i1_not_i2
        Yes Refl     => Yes Refl

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module GRIN.Opts.UnusedFunctionElim

import Data.List as List
import Data.Maybe
import Data.SortedSet
import Data.SortedMap as Map

import GRIN.AST
import GRIN.GrinM

export
unusedFuncElim : Ord name => Monad m => GrinT name m ()
unusedFuncElim = do
    used <- getCalls
    MkProg exts defs main <- gets prog
    let isUsed : name -> Bool
        isUsed = \n => isJust $ lookup n used
        addUsed : name -> a -> SortedMap name a -> SortedMap name a
        addUsed = \n => if isUsed n then insert n else const id
        usedDefs : SortedMap name (Def name)
        usedDefs = foldr (uncurry addUsed) empty $ toList defs
        usedExts : SortedMap name (Extern name)
        usedExts = foldr (uncurry addUsed) empty $ toList exts
    putProg $ MkProg usedExts usedDefs main