text:
||| Serialization of simple (non-recursive, but with list as a primitive)
||| algebraic data types to what I call "binary S-Expressions". They are like
||| S-Expressions, but use binary characters instead of parentheses and spaces.
||| Atoms are machine words, minus binary \x00 - \x03, which we reserve; strings
||| (or really, binary blobs) are also supported. Type information is not
||| carried in the serialization; it is assumed that all parties have previously
||| agreed on the type and are in sync concerning the (de)serialization
||| mechanism.
|||
||| In the binary form we substitute \x00 <NUL> for space, \x01 <SOH> for
||| double-quote, \x02 <STX> for left parenthesis, \x03 <ETX> for right
||| parenthesis. Rather than quoting, <SOH> results in an error if it occurs in
||| blobs, for simplicity and speed. Quoting requires unquoting; dropping is a
||| performance hit only on one side. Though the format itself is encoded in
||| binary, we are not focused on transmitting binary data. We could of course
||| quote \x01 by doubling it or some such, but we are more interested in speed
||| than flexibility in this case. If we do need to send binary data, you can do
||| the escaping at an application level.
|||
||| We inject the word "binary" into the middle of the sentence rather than the
||| beginning for propriety's sake if you are one of those people who likes to
||| pronounce abbreviations. ;)
|||
||| This is intended as a reference implementation.
module SBinExpr

%default total
%access export

||| Abstract syntax tree for binary S-expressions
data SBinExpr
  = Atom Char
  | Blob String
  | Pair SBinExpr SBinExpr
  -- Like Pair, but does allow dropping the parens. When printing, if the
  -- top-level is `Bare`, this is technically malformed, and should be formatted
  -- as if it were `Pair`. A parser should never spit out a top-level `Bare`.
  | Bare SBinExpr SBinExpr

data ControlChar = Delim | Init | Term | Quote

controlChar : ControlChar -> Char
-- Deliminator for lists/tuples in binary S-expressions
controlChar Delim = '\NUL'
-- Initialization / start marker for lists/tuples in binary S-expressions
controlChar Init = '\STX'
-- Terminator / end marker for lists/tuples in binary S-expressions
controlChar Term = '\ETX'
-- Quote mark for strings/blobs in binary S-expressions
controlChar Quote = '\SOH'

controlCharMap : List (Char, ControlChar)
controlCharMap = map (\c => (controlChar c, c)) [Delim, Init, Term, Quote]

parseCC : Char -> Maybe ControlChar
parseCC c = lookup c controlCharMap

Show ControlChar where
  show = singleton . controlChar

delim : String
delim = show Delim

init : String
init = show Init

term : String
term = show Term

quote : String
quote = show Quote

data SBEParseError
  = EmptySExprIllegal
  | TopLvlExprMalformed
  | UnexpectedControlChar ControlChar
  | UnterminatedBlob
  | UnterminatedList
  | MissingDeliminator
  | TrailingBytes (l : List Char ** NonEmpty l)
  | MissingSecond
  | MalformedPair

data BrokenSnd : List a -> Type where
  EmptySnd : BrokenSnd []
  -- Perhaps a bit of a misnomer, for l itself can be empty
  NonESnd : (l : List a) -> Smaller l (x :: xs) -> BrokenSnd (x :: xs)

consBrokenSnd : (x : a) -> BrokenSnd xs -> BrokenSnd (x :: xs)
consBrokenSnd _ EmptySnd = NonESnd [] (LTESucc LTEZero)
consBrokenSnd _ (NonESnd l z) = NonESnd l (lteSuccRight z)

tailSmaller : (x : a) -> (xs : List a) -> Smaller xs (x :: xs)
tailSmaller x [] = LTESucc LTEZero
tailSmaller x (y :: xs) = LTESucc $ tailSmaller y xs

break' : (a -> Bool) -> (l : List a) -> (List a, BrokenSnd l)
break' _ []      = ([], EmptySnd)
break' p (x::xs) =
  if p x
  then ([], NonESnd xs $ tailSmaller x xs)
  else let (ys, zs) = break' p xs in (x::ys, consBrokenSnd x zs)

||| The result of a parse
PResult : List Char -> Type -> Type
PResult x a = Either SBEParseError (a, (y : List Char ** Smaller y x))

||| A quotataion marker has already been encountered (and is not included in the
||| input string). Parse until a matching quotation marker is encountered.
parseBlob : (x : List Char) -> PResult x SBinExpr
parseBlob x =
  let (one, two) = break' (== (controlChar Quote)) x in
  case two of
    EmptySnd => Left UnterminatedBlob
    (NonESnd xs prf) => Right (Blob $ pack one, (xs ** prf))

||| Parse out a terminator
parseTerm : (x : List Char) -> PResult x ()
parseTerm [] = Left MalformedPair
parseTerm (x :: xs) =
  case parseCC x of
    Just Term => Right ((), (xs ** lteRefl))
    _ => Left UnterminatedList

||| Because of their beautiful relationship to recursion and thus to Idris'
||| totality checker, we parse from Haskell strings; even though Idris' base
||| string type is primitive. However, since when we print we are recursing on
||| the AST, we go straight to primitive Idris strings.
partial
parse : String -> Either SBEParseError SBinExpr
parse = parseTopLvl . unpack where
  mutual
    ||| Parse a top-level expresion
    partial
    parseTopLvl : List Char -> Either SBEParseError SBinExpr
    parseTopLvl [] = Left EmptySExprIllegal
    parseTopLvl (x :: xs) =
      case parseCC x of
        Nothing => if xs == [] then Right $ Atom x else Left TopLvlExprMalformed
        Just Quote => do
          blob <- parseBlob xs
          case blob of
            (expr, ([] ** _)) => pure expr
            _ => Left UnterminatedBlob
        Just Init => do
          (expr, (rem ** _)) <- parseList xs
          case rem of
            [] => Right expr
            (x' :: xs') => Left $ TrailingBytes (x' :: xs' ** IsNonEmpty)
        Just cc => Left $ UnexpectedControlChar cc

    ||| A pair/list inititializer/"open parenthesis" has already been
    ||| encountered (and is not included in the input string). Parse until
    ||| a matching pair/list terminator/"close parentheiss" is encountered.
    partial
    parseList : (x : List Char) -> PResult x SBinExpr
    parseList [] = Left UnterminatedList
    parseList (x :: xs) = do
      (exprs, (rem ** prf)) <- parseInnerList (x :: xs)
      ((), (rem' ** prf')) <- parseTerm rem
      case exprs of
        (expr1 :: expr2 :: exprs') =>
          let prf'' = lteTransitive prf' (lteSuccLeft prf)
          in Right (foldl Bare expr2 exprs', (rem' ** prf''))
        _ => Left MalformedPair

    ||| Parse out a "list", but without caring about parenthesis, only minding
    ||| deliminators.
    partial
    parseInnerList : (x : List Char) -> {auto prf : NonEmpty x}
                   -> PResult x (List SBinExpr)
    parseInnerList (x :: xs) = do
      (expr, (rem ** prf)) <- parseOne (x :: xs)
      case rem of
        -- Because we are not here parsing a top-level expression (an inner list
        -- will always be parentheized on the outside) to run out of characters
        -- here is to fail to terminate a list.
        [] => Left UnterminatedList
        (x' :: xs') =>
          case parseCC x' of
            Nothing => Left MissingSecond
            Just Term => pure ([expr], ((x' :: xs') ** prf))
            Just Delim =>
              case xs' of
                [] => Left MissingSecond
                (x'' :: xs'') => do
                  (exprs, (rem' ** prf')) <- parseInnerList (x'' :: xs'')
                  let prf'' = lteSuccRight $ lteSuccRight prf'
                  pure (expr :: exprs, (rem' ** lteTransitive prf'' prf))
            Just cc => Left $ UnexpectedControlChar cc

    partial
    parseOne : (x : List Char) -> {auto prf : NonEmpty x} -> PResult x SBinExpr
    parseOne (x :: xs) =
      case parseCC x of
        Nothing => Right (Atom x, (xs ** lteRefl))
        Just Quote => do
          (expr, (rem ** prf)) <- parseBlob xs
          pure (expr, (rem ** lteSuccRight prf))
        Just Init => do
          (expr, (rem ** prf)) <- parseList xs
          pure (expr, (rem ** lteSuccRight prf))
        Just cc => Left $ UnexpectedControlChar cc

data PrintEr
  = ControlCharInAtom ControlChar
  | QuoteInBlob

private printSBE' : SBinExpr -> Either PrintEr String
printSBE' (Atom x) =
  case parseCC x of
    Just c => Left $ ControlCharInAtom c
    Nothing => Right $ singleton x
printSBE' (Blob s) =
  if isInfixOf quote s
  then Left QuoteInBlob
  else Right $ quote ++ s ++ quote
printSBE' (Pair x y) = do
  x' <- printSBE' x
  y' <- printSBE' y
  pure $ init ++ x' ++ delim ++ y' ++ term
printSBE' (Bare x y) = do
  x' <- printSBE' x
  y' <- printSBE' y
  pure $ x' ++ delim ++ y'

printSBE : SBinExpr -> Either PrintEr String
-- Ensure parenthesis at the top level; if we were to permit lacking parenthesis
-- at the top, the parse would be much less simple. Saving two bytes is not
-- worth the complexity.
printSBE (Bare x y) = printSBE' (Pair x y)
printSBE x = printSBE' x

||| Invariants we would enforce if we could:
|||  1. Discriminated unions are serialized by:
|||   i. Assigning each case a unique integer in `[4, MaxInt)`.
|||   ii. If the case has data, packing the data of the particular case into a
|||       Lisp-style list, tagged with the case's specific data.
|||   iii. If the case does not have data, its representation is purely its
|||        unique integer.
|||  2. Records are treated as single-case discriminated unions, where the tag
|||     can therefore be dropped, so really, they are just treated as an ordered
|||     list of fields, for some deterministic ordering of fields.
|||  3. Strings are serialized directly to blobs
|||
||| When serializing a list, `maybeCompact` is tried first; if a data type can
||| be smashed into a char, it can be encoded more efficiently as a string
||| rather than a full-on list.
|||
||| Ultimately, rather than implementing these here, we will implement an IDL
||| and all of this code will be generated in what language desired, and we will
||| trust the IDL compiler to get it right. This is just a spike.
interface ToSBinExpr a where
  toSBE : a -> SBinExpr
  maybeCompact : Maybe (a -> Char)

interface FromSBinExpr a where
  fromSBE : SBinExpr -> Maybe a

serialize : ToSBinExpr a => a -> Either PrintEr String
serialize = printSBE . toSBE

data DeserialEr
  = ParseEr SBEParseError
  | SBinExprDoesntMatchType SBinExpr

partial
deserialize : FromSBinExpr a => String -> Either DeserialEr a
deserialize @{constraint} x =
  case parse x of
    Left e => Left (ParseEr e)
    Right sbe =>
      case fromSBE @{constraint} sbe of
        Nothing => Left (SBinExprDoesntMatchType sbe)
        Just x => Right x

||| This instance is extremely straightforward by desing, as it is assumed that
||| strings and types that will want to serialize as strings will predominant,
||| and therefore the ability to serialize directly will greatly help
||| performance.
ToSBinExpr String where
  toSBE = Blob
  -- String, in the abstract, cannot be smashed into a single char
  maybeCompact = Nothing

ToSBinExpr Char where
  toSBE = Atom
  maybeCompact = Just id

ToSBinExpr Int where
  toSBE = Atom . cast
  maybeCompact = Just cast

boolToChar : Bool -> Char
boolToChar False = '\04'
boolToChar True = '\05'

ToSBinExpr Bool where
  toSBE = Atom . boolToChar
  maybeCompact = Just boolToChar

listToList : (a -> SBinExpr) -> List a -> SBinExpr
listToList _ [] = Atom '\04' -- Nil
listToList f (x :: xs) = Pair (f x) (listToList' f xs) where
  listToList' : (a -> SBinExpr) -> List a -> SBinExpr
  listToList' f [] = Atom '\04' -- Nil
  listToList' f (x :: xs) = Bare (f x) (listToList' f xs)

listToSBE : (inst : ToSBinExpr a) => List a -> SBinExpr
listToSBE @{inst} =
  case maybeCompact @{inst} of
    Nothing => listToList toSBE
    Just compact => Blob . pack . map compact

ToSBinExpr a => ToSBinExpr (List a) where
  toSBE = listToSBE
  -- Foldabes, in the abstract, cannot be smashed into a single char
  maybeCompact = Nothing

ToSBinExpr a => ToSBinExpr (Maybe a) where
  toSBE Nothing = Atom '\04'
  toSBE (Just x) = Pair (Atom '\05') (toSBE x)
  maybeCompact = Nothing

(ToSBinExpr a, ToSBinExpr b) => ToSBinExpr (Either a b) where
  toSBE (Left l) = Pair (Atom '\04') (toSBE l)
  toSBE (Right r) = Pair (Atom '\05') (toSBE r)
  maybeCompact = Nothing

-- The optimization here to potentially serialize to string is not worth the
-- complexity, because tuples are inherently smallish in length, nor to
-- serialize them as lists at all. Serialize directly to S-Expr pairs.
(ToSBinExpr a, ToSBinExpr b) => ToSBinExpr (Pair a b) where
  toSBE (f, s) = Pair (toSBE f) (toSBE s)
  maybeCompact = Nothing

-- TODO: need to be able to convert `SBinExpr` to a plain-text, human-readable
-- format for viewing/debugging.

-- Examples

Example0 : Either String Bool
Example0 = Left "foo"

Example1 : Either String Bool
Example1 = Left "bar"

Example2 : Either String Bool
Example2 = Right True

Example3 : Either String Bool
Example3 = Right False

Example4 : Maybe (Either Int Char)
Example4 = Nothing

Example5 : Maybe (Either Int Char)
Example5 = Just (Right '%')

Example6 : Maybe (Either Int Char)
Example6 = Just (Left 1337)

Example7 : List (Either String (Int, (Bool, Char)))
Example7 =
  [ Left "Random example"
  , Right (5, True, '?')
  , Right (0, False, ' ')
  ]

Example8 : List (Either String (Int, (Bool, Char)))
Example8 =
  [ Left "Random example"
  , Right (5, True, '?')
  , Right (1337, False, ' ')
  ]

max_stars_repo_name: Kazark/SBinExpr

max_issues_repo_name: Kazark/SBinExpr

max_forks_repo_name: Kazark/SBinExpr


text:
module Network.HTTP.Error

import Generics.Derive

%language ElabReflection

public export
data HttpError e
  = UnknownHost
  | UnknownProtocol String
  | ConnectionClosed
  | SocketError String
  | ContentLengthMismatch Integer
  | MissingHeader String
  | UnknownTransferEncoding String
  | DecompressionError String
  | OtherReason e

%runElab derive "HttpError" [Generic, Meta, Eq, Show]

ext: idr


text:
-- examples in "Type-Driven Development with Idris"
-- chapter 15, section 15.2

import ProcessLib

-- check that all functions are total
%default total

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

-- outputs wrt. inputs
ListType : ListAction -> Type
ListType (Length xs) = Nat
ListType (Append {elem} xs ys) = List elem

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

-- client
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)

-- run with:
-- :exec runProc procMain

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Compiler.Erlang.GlobalOpts

import Data.List
import Data.List1
import Data.Strings
import Compiler.Erlang.Name

%default total

public export
data OutputFormat = ErlangSource | ErlangSourcePretty | AbstractFormat | BeamFromErlangSource | BeamFromAbstractFormat

public export
record GlobalOpts where
  constructor MkGlobalOpts
  outputFormat : OutputFormat
  prefixStr : String
  inlineSize : Nat

export
defaultGlobalOpts : GlobalOpts
defaultGlobalOpts = MkGlobalOpts BeamFromErlangSource "Idris" 0

data Flag
  = SetOutputFormat OutputFormat
  | SetPrefix String
  | SetInlineSize Nat

flagToOpts : Flag -> GlobalOpts -> GlobalOpts
flagToOpts (SetOutputFormat outputFormat) opts = record { outputFormat = outputFormat } opts
flagToOpts (SetPrefix prefixStr) opts = record { prefixStr = prefixStr } opts
flagToOpts (SetInlineSize inlineSize) opts = record { inlineSize = inlineSize } opts

flagsToOpts : List Flag -> GlobalOpts
flagsToOpts flags = flagsToOpts' flags defaultGlobalOpts
  where
    flagsToOpts' : List Flag -> GlobalOpts -> GlobalOpts
    flagsToOpts' [] opts = opts
    flagsToOpts' (flag :: flags) opts = flagsToOpts' flags (flagToOpts flag opts)

parseOutputFormat : String -> Maybe OutputFormat
parseOutputFormat "erl" = Just ErlangSource
parseOutputFormat "erl-pretty" = Just ErlangSourcePretty
parseOutputFormat "abstr" = Just AbstractFormat
parseOutputFormat "beam" = Just BeamFromErlangSource
parseOutputFormat "beam-abstr" = Just BeamFromAbstractFormat
parseOutputFormat _ = Nothing

stringToFlags : List String -> List Flag
stringToFlags ds = mapMaybe parseFlag (map (\d => assert_total (words d)) ds) -- TODO: Remove `assert_total` when `words` is total
  where
    parseFlag : List String -> Maybe Flag
    parseFlag ["format", format] = SetOutputFormat <$> parseOutputFormat format
    parseFlag ["prefix", prefixStr] = Just $ SetPrefix prefixStr
    parseFlag ["inline", inlineSize] = Just $ SetInlineSize (integerToNat (cast inlineSize))
    parseFlag _ = Nothing

export
parseOpts : List String -> GlobalOpts
parseOpts str = flagsToOpts (stringToFlags str)


text:
import NewEden.Natural

{- Natural Theorems

   Basic theorems about the natural numbers expressed in
   terms of operations on Natural p.

-}

addToBothSides : (n : Natural p) -> a = b -> a + n = b + n
addToBothSides _ Refl = Refl

addRemoveBothSides : (n : Natural p) -> n + a = n + b -> a = b
addRemoveBothSides {a} {b} n prf =
  let (MkMonomorphicFunction _ mono) = plusMonomorphic p n in
  mono a b prf

multiplyBothSidesBy : (n : Natural p) -> a = b -> a * n = b * n
multiplyBothSidesBy _ Refl = Refl

multiplyRemoveBothSides : (n : Natural p) -> n * a = n * b -> a = b
multiplyRemoveBothSides {a} {b} n prf =
  let (MkMonomorphicFunction _ mono) = multiplyMonomorphic p n in
  mono a b prf

pluscom : {a:Natural p}
        -> a + b = c -> b + a = c
pluscom {p} {a} {b} given =
  let (MkCommutativeFunction _ prf) = plusCommutative p in
  let apply = prf b a in
  transitivity apply given

plusass : {a:Natural p}
        -> a + (b + c) = d -> a + b + c = d
plusass {p} {a} {b} {c} given =
  let (MkAssociativeFunction _ prf) = plusAssociative p in
  let apply = prf a b c in
  transitivity (symmetric apply) given

plusass' : {a:Natural p}
         -> a + b + c = d -> a + (b + c) = d
plusass' {p} {a} {b} {c} given =
  let (MkAssociativeFunction _ prf) = plusAssociative p in
  let apply = prf a b c in
  transitivity apply given

multcom : {a : Natural p}
        -> a * b = c -> b * a = c
multcom {p} {a} {b} given =
  let (MkCommutativeFunction _ prf) = multiplyCommutative p in
  let apply = prf b a in
  transitivity apply given

multass : {a : Natural p}
        -> a * (b * c) = d -> a * b * c = d
multass {p} {a} {b} {c} given =
  let (MkAssociativeFunction _ prf) = multiplyAssociative p in
  let apply = prf a b c in
  transitivity (symmetric apply) given

multass' : {a : Natural p}
        -> a * b * c = d -> a * (b * c) = d
multass' {p} {a} {b} {c} given =
  let (MkAssociativeFunction _ prf) = multiplyAssociative p in
  let apply = prf a b c in
  transitivity apply given

nothingIsLessThanZero : (a:Natural p) -> LessThan a 0 -> Void
nothingIsLessThanZero {p} a (MkLessThan a (Z p) (c ** (prf,cNonZero))) =
  let (MkCommutativeFunction _ comm) = NewEden.Natural.plusCommutative p in
  let equation = symmetric $ comm a c in
  let cPlusAIsZero = transitivity equation prf in
  let (MkStrictMonoid _ noInverses) = NewEden.Natural.plusLacksInverses p in
  let cIsZero = noInverses c a cPlusAIsZero in
  cNonZero cIsZero

lessThanImpliesNotEqual : (a:Natural p) -> (b:Natural p) -> LessThan a b -> a = b -> Void
lessThanImpliesNotEqual a b (MkLessThan a b (c ** (aPlusCIsB,cNonZero))) aEqualsb =
  let step = symmetric aPlusCIsB in
  let step2 = transitivity aEqualsb step in
  let (MkMonoid _ _ mn _) = plusMonoid p in
  let step3 = mn a in
  let step4 = transitivity step3 step2 in
  let mono = plusMonomorphic p in
  let (MkMonomorphicFunction ((+) a) monoprf) = mono a in
  let fin = monoprf 0 c in
  let cIsZero = fin step4 in
  cNonZero $ symmetric cIsZero

lessThanNotSymmetric : {a:Natural p} -> {b:Natural p} -> LessThan a b -> LessThan b a -> Void
lessThanNotSymmetric {p} (MkLessThan a b (c1 ** (prf1,c1NonZero))) (MkLessThan b a (c2 ** (prf2,c2NonZero))) =
  let (MkCommutativeFunction _ comm) = plusCommutative p in
  let (MkMonoid _ _ mon _) = plusMonoid p in
  let (MkMonomorphicFunction _ mono) = plusMonomorphic p $ b in
  let (MkAssociativeFunction _ ass) = plusAssociative p in
  let comm' = symmetric $ comm a c1 in
  let s1 = substitution ((+) c1) (symmetric prf2) (transitivity comm' prf1) in
  let s2 = symmetric $ comm c1 (b + c2) in
  let s3 = transitivity s2 s1 in
  let but4 = mon b in
  let so5 = transitivity but4 $ symmetric s3 in
  let byMono = mono 0 (c2 + c1) in
  let ass' = ass b c2 c1 in
  let prepare = transitivity so5 (symmetric ass') in
  let therefore = byMono prepare in
  let but6 = mon c2 in
  let (MkMonomorphicFunction _ monoc2) = plusMonomorphic p $ c2 in
  let monoapp = monoc2 0 c1 in
  let (MkStrictMonoid _ noInverses) = plusLacksInverses p in
  let so6 = noInverses c2 c1 in
  let c2IsZero = so6 (symmetric therefore) in
  c2NonZero c2IsZero

lessThanIsTransitive : {x:Natural p} -> {y:Natural p} -> {z:Natural p} ->
                       LessThan x y -> LessThan y z -> LessThan x z
lessThanIsTransitive {p} (MkLessThan x y (c1 ** (eq1,c1NonZero))) (MkLessThan y z (c2 ** (eq2,c2NonZero)))=
  case compare x z of
    Left prf => prf
    Middle xIsZ =>
      let sub = pluscom $ substitution ((+) c1) xIsZ (pluscom eq1) in
      let zLessThany = MkLessThan z y (c1 ** (sub,c1NonZero)) in
      let yLessThanz = MkLessThan y z (c2 ** (eq2,c2NonZero)) in
      absurd $ lessThanNotSymmetric yLessThanz zLessThany
    Right (MkLessThan z x (c3 ** (eq3,c3NonZero))) =>
      let sub = substitution ((+) c1) (symmetric eq3) (pluscom eq1) in
      let s0 = pluscom sub in
      let c4 = c3 + c1 in
      let c4e:(c4 = c3 + c1) = Refl in
      let (MkStrictMonoid _ noInverses) = plusLacksInverses p in
      let c4nz = (\c4z => c3NonZero $ noInverses c3 c1 c4z) in
      let s1 = plusass' s0 in
      let zlty = MkLessThan z y ((c3+c1) ** (s1,c4nz)) in
      let yltz = MkLessThan y z (c2 ** (eq2,c2NonZero)) in
      absurd $ lessThanNotSymmetric zlty yltz

lessThanAdditionWeakened : LessThan x y -> (z : Natural p) -> LessThan x (y + z)
lessThanAdditionWeakened {p} {x} {y} (MkLessThan x y (c ** (xpyic,cNotZero))) z =
  let (MkStrictMonoid _ noinv) = plusLacksInverses p in
  let cPlusZIsZeroImpliesCIsZero = noinv c z in
  let cPlusZNotZero = (\sumZero => cNotZero $ cPlusZIsZeroImpliesCIsZero sumZero) in
  let target = addToBothSides z xpyic in
  let target' = plusass' target in
  MkLessThan x (y + z) ((c + z) ** (target',cPlusZNotZero))

max_stars_repo_name: identicalsnowflake/neweden

max_issues_repo_name: identicalsnowflake/neweden

max_forks_repo_name: identicalsnowflake/neweden


text:
-- Local Variables:
-- idris-packages: ("lightyear" "contrib")
-- End:

import Lightyear.Strings
import Network.Socket
import Prelude.Strings
import System
import Control.Monad.State
import Control.Monad.Trans
import System.Concurrency.Process
import Data.Vect

import HydraBot.Types
import HydraBot.IRCParsers
import HydraBot.IRCProcess
import HydraBot.NetworkUtils
import HydraBot.News

||| Slaps
slaps : List (String, String)
slaps = [
  ("rewrites", " in whitespace"),
  ("slaps", ""),
  ("grabs", " and runs away"),
  ("rewrites", "'s code in PHP and removes the original"), -- borrowed from fsbot
  ("attacks", ""),
  ("hugs", " instead"),
  ("beta-reduces", ""),
  ("shows that", " is homotopy equivalent to a point")
  ]

||| Slap people
||| @mn Bot nick, used as a protection against self-slap
||| @u User
||| @c Channel
||| @m Message words
slap : (mn: String) -> (u: String) -> (c: String) ->
     (m: List String) -> StateT (Fin (length slaps)) IO (List String)
slap mn u c ["slap", t] = do
  v <- get
  lift . putStrLn $ u ++ " wants to slap " ++ t ++ " on " ++ c
  put $ incr v
  pure $ [action $ wrap (if mn == t then u else t) $ index v (fromList slaps)]
where
  wrap : String -> (String, String) -> String
  wrap x (y, z) = y ++ " " ++ x ++ z
  incr : Fin (S n) -> Fin (S n)
  incr f = case strengthen (FS f) of
    (Right fs) => fs
    (Left _) => FZ
slap _ _ _ _ = pure []

||| Ping and join
||| @c A list of channels to join
||| @m A message to process
basics : (c: List String) -> (m: Message) -> List Message
basics channels (Msg _ (Right 376) _) = map (msg "JOIN" . pure) channels
basics _ (Msg _ (Left "PING") p) = msgl "PONG" p
basics _ _ = []

||| Common things
common : (u: String) -> (c: String) -> (m: List String) -> StateT () IO (List String)
common u c ["anyone"] = pure . pure $ -- borrowed from fsbot
  "Just ask your question. It's the best way to know if anyone can help."
common _ _ _ = pure []

||| Knowledge base
kb : (u: String) -> (c: String) -> (m: List String) ->
   StateT (List (String, String)) IO (List String)
kb u c (t::"is"::d) = do
  s <- get
  put $ List.(::) (t, unwords d) s
  pure . pure $ u ++ ": added a definition for " ++ t
kb u c ["forget","about",t] = do
  s <- get
  case List.lookup t s of
    Nothing => pure . pure $ u ++ ": I don't know anything about " ++ t ++ " anyway"
    Just _ => do
      put $ List.filter (not . (== t) . fst) s
      pure . pure $ u ++ ": forgot successfully"
kb u c ("forget"::"about"::t::"being"::d) = do
  s <- get
  if List.elem (t, unwords d) s
    then do
      put $ List.filter (not . (== (t, unwords d))) s
      pure . pure $ u ++ ": forgot successfully"
    else pure . pure $ u ++ "I don't even know about " ++ t ++ " being " ++ unwords d
kb u c [t] = do
  s <- get
  case List.filter ((== t) . fst) s of
    [] => pure []
    [x] => pure . pure $ t ++ " is " ++ snd x
    xs => pure $ (u ++ ": " ++ t ++ " could refer to any of these things:") ::
      map ((++) (u ++ ": - ") . snd) xs
kb _ _ _ = pure []

||| Entry point: processes args, connects, runs processes
main : IO ()
main = do
  args <- getArgs
  case args of
    (prog::host::port::n::u::ui::c) => do
      sock <- tcpConnect host (cast port)
      case sock of
        Nothing => putStrLn "Failed to connect"
        Just s => do
          traverse {t=List} (sendLine s) [show $ msg "NICK" [n],
                                          show $ msg "USER" [u, "*", "*", ui]]
          wid <- run . create $ writerProc s
          bid <- run . create $ pureProc wid $ basics c
          tid <- sioCommand wid FZ "," (slap n)
          cid <- sioCommand wid () "," common
          kid <- sioCommand wid List.Nil "," kb
          rid <- run . create $ readerProc [bid, tid, cid, kid] s
          nid <- run . create $ news wid c 300 comics
          getLine
          sendLine s . show $ msg "QUIT" ["Time to sleep"]
          close s
    _ => putStrLn "Arguments: <ipv4 address> <port> <nick> <user> <user info> [#channel1 #channel2...]"

max_stars_repo_name: defanor/hydra-bot

max_issues_repo_name: defanor/hydra-bot

max_forks_repo_name: defanor/hydra-bot


text:
module Main

import Data.Vect as V

readToBlank : IO (List String)
readToBlank = do
            inp <- getLine
            if inp == "" then pure []
            else do nextLines <- readToBlank
                    pure $ inp :: nextLines

readAndSave : IO ()
readAndSave = do
            putStrLn "Please enter the lines to be read:"
            lines <- readToBlank
            putStrLn "Please enter the file name:"
            fileName <- getLine
            Right done <- writeFile fileName (unlines lines)
          | Left err   => putStrLn ("Unable to open file " ++ fileName ++ " for writing")
            pure done

total listToVect : List String -> (len ** Vect len String)
listToVect [] = (_ ** [])
listToVect (x :: xs) = let (_ ** vec) = listToVect xs in
                           (_ ** x :: vec)

readVectFile : (filename : String) -> IO (n ** Vect n String)
readVectFile filename = do
            Right contents <- readFile filename
           | Left err => pure (_ ** V.Nil)
            let lines = lines contents
            pure (listToVect lines)

max_stars_repo_name: balajisivaraman/idris-book

max_issues_repo_name: balajisivaraman/idris-book

max_forks_repo_name: balajisivaraman/idris-book


text:
import Control.Monad.State

increment : Nat -> State Nat ()
increment inc = do current <- get
                   put (current + inc)


text:
> module CoinductiveCalculus.CoinductiveCalculus

> import Syntax.PreorderReasoning

> %default total
> %access public export
> %auto_implicits off

> %hide Stream
> %hide head
> %hide tail
> %hide (+)
> %hide plusZeroRightNeutral

* Streams

For a type |T|, streams of values of type |T| can be described by values
of type |Stream T| with

> Stream : Type -> Type

The idea is that any |Stream T| has a head and a tail

> head : {T : Type} -> Stream T -> T
> tail : {T : Type} -> Stream T -> Stream T

and that piecing together a |T| with a |Stream T| yields a |Stream T|:

> cons : {T : Type} -> T -> Stream T -> Stream T

The stream operations |head|, |tail| and |cons| are required to fulfil
three properties:

> headConsProp : {T : Type} -> (t : T) -> (s : Stream T) -> head (cons t s) = t

> tailConsProp : {T : Type} -> (t : T) -> (s : Stream T) -> tail (cons t s) = s

> consHeadTailProp : {T : Type} -> (s : Stream T) -> cons (head s) (tail s) = s

* Differentiation and integration

We want to look at differentiation and integration of functions of real
variables from the point of view of streams. More specifically, we want
to understand which properties differentiation and integration have to
fulfill when we consider these operations as operations on streams of
type |Stream R = R -> R|. Here

> R : Type

is meant to represent real numbers and

> F : Type
> F = R -> R

are differentiable and integrable functions on |R|. For the time being,
we represent differentiation and integration through functions

> D : F -> F
> S : R -> R -> F -> R

with |D f| and |S a b f| representing the derivative of |f| and the
integral of |f| on |[a,b]|.

* Head, tail and cons for functions/streams

How can we implement |head| for |Stream R = F|? We have

> headF : F -> R

The natural way to compute a real number from a |f : F| is to simply
evaluate |f|. We require our "real numbers" to contain a zero element

> zero : R

and we define

> headF f = f zero

What about the tail of a function |f|?

> tailF : F -> F

The type of |tailF| is |F -> F|, just like the type of |D|. Thus, we
take

> tailF = D

We are left with the implementation of |consF|:

> consF : R -> F -> F

Of course, we want |headF|, |tailF| and |consF| to fulfill the
properties of stream operations. In particular, we want

< consF (headF f) (tailF f) = f

For |f = consF a g| and our definitions of |headF| and |tailF|, this is
equivalent to

< consF (headF f) (tailF f) = f
<
<   ={ def. of f }=
<
< consF (headF (consF a g)) (tailF (consF a g)) = consF a g
<
<   ={ def. of consF, tailF }=
<
< consF ((consF a g) zero) (D (consF a g)) = consF a g

Sufficient conditions for the last equality to hold are

< (consF a g) zero = a

and

< D (consF a g) = g

The first condition could be fulfilled by defining |consF a g| to be
|const a|. But the second condition requires |consF a g| has to be an
anti-derivative of |g|. This suggests the definition

> (+) : R -> R -> R

> consF a f = \ x => a + S zero x f

where we can think of |(+)| as representing the standard addition on
real numbers.

* Properties of |R|, |D| and |S|

Which properties do |R|, |D| and |S| have to satisfy for |headF|,
|tailF| and |consF| to be stream operations? Our definition already
requires |R| to be equipped with a zero element and with a |(+)|:

< R : Type
< zero : R
< (+) : R -> R -> R

If we also require integration to fulfill

> intProp1 : (a : R) -> (f : F) -> S a a f = zero

and |zero| to be a

> plusZeroRightNeutral : (left : R) -> left + zero = left

We can derive a formal proof of |headF (consF a f) = a|:

> headConsPropF : (a : R) -> (f : F) -> headF (consF a f) = a
> headConsPropF a f = ( headF (consF a f) )
>                   ={ Refl }=
>                     ( headF (\ x => a + S zero x f) )
>                   ={ Refl }=
>                     ( a + S zero zero f )
>                   ={ cong (intProp1 zero f) }=
>                     ( a + zero )
>                   ={ plusZeroRightNeutral a }=
>                     ( a )
>                   QED

Satisfying |tailF (consF a f) = f| requires some more assumptions.
Consistently with the interpretation of |D f| representing the
derivative of |f|, we need

> derConstZero : (a : R) -> D (const a) = const zero

and

> derLinear1 : (f, g : F) -> D (\ x => f x + g x) = \ x => (D f) x + (D g) x

Moreover |S| has to be an "anti-derivative"

> intAntiDer : (f : F) -> D (\ x => S zero x f) = f

We also need |zero| to be left-neutral

> plusZeroLeftNeutral : (right : R) -> zero + right = right

and equality on |F| to be extensional:

> extEqF : (f, g : F) -> ((x : R) -> f x = g x) -> f = g

With these assumptions, we can derive

> lemma : (f : F) -> (x : R) -> zero + f x = f x
> lemma f x = ( zero + f x )
>           ={ plusZeroLeftNeutral (f x) }=
>             ( f x )
>           QED

and, finally

> tailConsPropF : (a : R) -> (f : F) -> tailF (consF a f) = f
> tailConsPropF a f = ( tailF (consF a f) )
>                   ={ Refl }=
>                     ( tailF (\ x => a + S zero x f) )
>                   ={ Refl }=
>                     ( D (\ x => a + S zero x f) )
>                   ={ Refl }=
>                     ( D (\ x => (const a) x + (\ y => S zero y f) x) )
>                   ={ derLinear1 (const a) (\ y => S zero y f) }=
>                     ( \ x => (D (const a)) x + (D (\ y => S zero y f)) x )
>                   ={ cong {f = \ h => \ x => h x + (D (\ y => S zero y f)) x } (derConstZero a) }=
>                     ( \ x => (const zero) x + (D (\ y => S zero y f)) x )
>                   ={ cong {f = \ h => \ x => (const zero) x + h x} (intAntiDer f) }=
>                     ( \ x => (const zero) x + f x )
>                   ={ Refl }=
>                     ( \ x => zero + f x )
>                   ={ extEqF (\ x => zero + f x) (\ x => f x) (lemma f) }=
>                     ( \ x => f x )
>                   ={ Refl }=
>                     ( f )
>                   QED

We are left with the last property: |consF (headF f) (tailF f) = f|. To
prove this property, we need three more assumptions

> (-) : R -> R -> R

> plusAnyMinus : (x, y : R) -> x + (y - x) = y

> derAntiInt : (f : F) -> (a : R) -> (b : R) -> S a b (D f) = f b - f a

With these, one has

> lemma1 : (c : R) -> (f : F) -> (x : R) -> (c + (f x - c) = f x)
> lemma1 c f x = plusAnyMinus c (f x)

> lemma2 : (f : F) -> (c : R) -> (a : R) -> (b : R) -> c + S a b (D f) = c + (f b - f a)
> lemma2 f c a b = ( c + S a b (D f) )
>                ={ cong (derAntiInt f a b) }=
>                  ( c + (f b - f a) )
>                QED

> consHeadTailPropF : (f : F) -> consF (headF f) (tailF f) = f
> consHeadTailPropF f = ( consF (headF f) (tailF f) )
>                     ={ Refl }=
>                       ( consF (f zero) (D f) )
>                     ={ Refl }=
>                       ( \ x => f zero + S zero x (D f) )
>                     ={ extEqF (\ x => f zero + S zero x (D f))
>                               (\ x => f zero + (f x - f zero))
>                               (lemma2 f (f zero) zero) }=
>                       ( \ x => f zero + (f x - f zero) )
>                     ={ extEqF (\ x => f zero + (f x - f zero))
>                               (\ x => f x)
>                               (lemma1 (f zero) f) }=
>                       ( \ x => f x )
>                     ={ Refl }=
>                       ( f )
>                     QED

* Properties of |R|, |D| and |S| (wrap up)

  ( 1) R : Type
  ( 2) zero : R
  ( 3) (+)  :  R -> R -> R
  ( 4) (-)  :  R -> R -> R
  ( 5) plusAnyMinus : (x, y : R) -> x + (y - x) = y
  ( 6) plusZeroLeftNeutral   :  (right : R) -> zero + right = right
  ( 7) plusZeroRightNeutral  :  ( left : R) -> left +  zero =  left

  ( 8) derConstZero : (a : R) -> D (const a) = const zero
  ( 9) derLinear1 : (f, g : F) -> D (\ x => f x + g x) = \ x => (D f) x + (D g) x

  (10) intProp1 : (a : R) -> (f : F) -> S a a f = zero
  (11) intAntiDer : (f : F) -> D (\ x => S zero x f) = f
  (12) derAntiInt : (f : F) -> (a : R) -> (b : R) -> S a b (D f) = f b - f a

  (13) extEqF : (f, g : F) -> ((x : R) -> f x = g x) -> f = g

Properties (1-7) follow from standard axioms on real numbers. (8-9)
follow from the standard definition of derivative. (10-12) follows from ?

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
-- ------------------------------------------------- [ InteractivePrograms.idr ]
-- Module      : Exercises.InteractivePrograms
-- Description : Solutions to the Chapter 5 exercises in Edwin Brady's
--               book, "Type-Driven Development with Idris."
-- --------------------------------------------------------------------- [ EOH ]
module Exercises.InteractivePrograms

import Control.Arrow
import Control.Category
import Data.Morphisms
import Data.Vect

import Effects
import Effect.Random

%access export

-- --------------------------------------------------------- [ 5.2.4 Exercises ]

||| Attempt to convert a string to a natural number.
|||
||| If `s` contains only digits, return `Just` the natural number it represents,
||| otherwise `Nothing`.
|||
||| ```idris example
||| stringToNat "123"
||| ```
||| ```idris example
||| stringToNat "bad"
||| ```
|||
||| @ string the string to try to convert
stringToNat : (string : String) -> Maybe Nat
stringToNat s = if all isDigit (unpack s)
                   then Just (cast s)
                   else Nothing

handleGuess : Nat -> IO () -> Maybe Nat -> IO ()
handleGuess _ loop Nothing           = putStrLn "Invalid number" *> loop
handleGuess target loop (Just guess) =
    case compare guess target of
         LT => putStrLn "Too low!"  *> loop
         EQ => putStrLn "Correct!"
         GT => putStrLn "Too high!" *> loop

readNumber : IO (Maybe Nat)
readNumber = stringToNat <$> getLine

namespace Simple

    ||| A simple "guess the number" game.
    |||
    ||| Repeatedly ask the user to guess a number and display whether the guess
    ||| is too high, too low, or correct. When the guess is correct, exit.
    |||
    ||| @ target the number to be guessed
    partial
    guess : (target : Nat) -> IO ()
    guess target = putStrLn "===> Guess the number" *> loop
      where
        partial
        loop : IO ()
        loop = putStr "> " *> handleGuess target loop !readNumber

    partial
    main : IO ()
    main = guess $ fromIntegerNat !(run (rndInt 1 100))

namespace Counting

    partial
    guess : (target, guesses : Nat) -> IO ()
    guess target guesses = putStrLn "===> Guess the number" *> loop
      where
        partial
        loop : IO ()
        loop = do putStrLn $ "Guesses so far: " ++ show guesses
                  putStr "> " *> handleGuess target loop !readNumber

    partial
    main : IO ()
    main = guess $ fromIntegerNat !(run (rndInt 1 100))

namespace DIY

    %hide Prelude.Interactive.replWith

    partial
    replWith : a -> String -> (a -> String -> Maybe (String, a)) -> IO ()
    replWith state prompt func =
        do putStr prompt
           case func state !getLine of
                Just (output, newState) => do putStr output
                                              replWith newState prompt func
                Nothing                 => pure ()

    %hide Prelude.Interactive.repl

    partial
    repl : String -> (String -> String) -> IO ()
    repl prompt func = replWith () prompt (flip (curry go))
      where
        go : (String, a) -> Maybe (String, a)
        go = applyMor $ first (arrow func) >>> arrow pure

-- --------------------------------------------------------- [ 5.3.5 Exercises ]

||| Read input from the console until the user enters a blank line.
partial
readToBlank : IO (List String)
readToBlank = case !getLine of
                   "" => pure []
                   x  => pure (x :: !readToBlank)

||| Read input from the console until the user enters a blank line,
||| then read a file name from the console, and write the input to the file.
partial
readAndSave : IO ()
readAndSave = do putStrLn "Input:"
                 contents <- unlines <$> readToBlank
                 putStr "Filename: "
                 Right file <- writeFile !getLine contents
                   | Left err => printLn err
                 putStrLn "done"

namespace ReadVectFile

    ||| Read the contents of a file into a dependent pair containing a length
    ||| and a `Vect` of that length.
    ||| If there are any errors, return the empty vector.
    partial
    readVectFile : (filename : String) -> IO (n ** Vect n String)
    readVectFile filename = do Right xs <- map lines <$> readFile filename
                                 | Left err => (printLn err *> pure (_ ** []))
                               pure (_ ** fromList xs)

    main : IO ()
    main = putStr "Filename: " *> printLn !(readVectFile !getLine)

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

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
module Main

import System

-countdown : (secs : Nat) -> IO ()
countdown Z = putStrLn "Lift off!"
countdown (S secs) = do putStrLn (show (S secs))
                        usleep 1000000
                        countdown secs-

countdowns : IO ()
countdowns = do putStr "Enter starting number: "
               Just startNum <- readNumber
               | Nothing => do putStrLn "Invalid input"
                               countdowns
               countdown startNum
               putStr "Another (y/n)?"
               yn <- getLine
               if yn == "y" then countdowns
                            else pure ()


text:
||| Spec: https://webassembly.github.io/spec/core/syntax/modules.html#imports
module WebAssembly.Structure.Modules.Imports

import WebAssembly.Structure.Values
import WebAssembly.Structure.Types
import WebAssembly.Structure.Modules.Indices

-- Definition

public export
data ImportDesc : Type where
  FuncImport   : TypeIdx    -> ImportDesc
  TableImport  : TableType  -> ImportDesc
  MemImport    : MemType    -> ImportDesc
  GlobalImport : GlobalType -> ImportDesc

public export
record Import where
  constructor MkImport
  wmodule : Name
  name : Name
  desc : ImportDesc

-- Equality

total public export
lemma_funcimport__injective : ((f1 = f2) -> Void) -> (FuncImport f1 = FuncImport f2) -> Void
lemma_funcimport__injective f1_not_f2 Refl = f1_not_f2 Refl

total public export
lemma_tableimport__injective : ((t1 = t2) -> Void) -> (TableImport t1 = TableImport t2) -> Void
lemma_tableimport__injective t1_not_t2 Refl = t1_not_t2 Refl

total public export
lemma_memimport__injective : ((m1 = m2) -> Void) -> (MemImport m1 = MemImport m2) -> Void
lemma_memimport__injective m1_not_m2 Refl = m1_not_m2 Refl

total public export
lemma_globalimport__injective : ((g1 = g2) -> Void) -> (GlobalImport g1 = GlobalImport g2) -> Void
lemma_globalimport__injective g1_not_g2 Refl = g1_not_g2 Refl

total public export
lemma_funcimport_not_tableexport : (FuncImport f = TableImport t) -> Void
lemma_funcimport_not_tableexport Refl impossible

total public export
lemma_funcimport_not_memexport : (FuncImport f = MemImport m) -> Void
lemma_funcimport_not_memexport Refl impossible

total public export
lemma_funcimport_not_globalexport : (FuncImport f = GlobalImport g) -> Void
lemma_funcimport_not_globalexport Refl impossible

total public export
lemma_tableimport_not_funcexport : (TableImport t = FuncImport f) -> Void
lemma_tableimport_not_funcexport Refl impossible

total public export
lemma_tableimport_not_memexport : (TableImport t = MemImport m) -> Void
lemma_tableimport_not_memexport Refl impossible

total public export
lemma_tableimport_not_globalexport : (TableImport t = GlobalImport g) -> Void
lemma_tableimport_not_globalexport Refl impossible

total public export
lemma_memimport_not_tableexport : (MemImport m = TableImport t) -> Void
lemma_memimport_not_tableexport Refl impossible

total public export
lemma_memimport_not_funcxport : (MemImport m = FuncImport f) -> Void
lemma_memimport_not_funcxport Refl impossible

total public export
lemma_memimport_not_globalexport : (MemImport m = GlobalImport g) -> Void
lemma_memimport_not_globalexport Refl impossible

total public export
lemma_globalimport_not_tableexport : (GlobalImport g = TableImport t) -> Void
lemma_globalimport_not_tableexport Refl impossible

total public export
lemma_globalimport_not_funcxport : (GlobalImport g = FuncImport m) -> Void
lemma_globalimport_not_funcxport Refl impossible

total public export
lemma_globalimport_not_memexport : (GlobalImport g = MemImport m) -> Void
lemma_globalimport_not_memexport Refl impossible

total public export
lemma_import__module_injective : ((m1 = m2) -> Void) -> (MkImport m1 n1 d1 = MkImport m2 n2 d2) -> Void
lemma_import__module_injective m1_not_m2 Refl = m1_not_m2 Refl

total public export
lemma_import__name_injective : ((n1 = n2) -> Void) -> (MkImport m1 n1 d1 = MkImport m2 n2 d2) -> Void
lemma_import__name_injective n1_not_n2 Refl = n1_not_n2 Refl

total public export
lemma_import__desc_injective : ((d1 = d2) -> Void) -> (MkImport m1 n1 d1 = MkImport m2 n2 d2) -> Void
lemma_import__desc_injective d1_not_d2 Refl = d1_not_d2 Refl

-- Decidable Equality

public export
implementation DecEq ImportDesc where
  decEq (FuncImport x)   (FuncImport y)   = case decEq x y of
    No x_not_y => No $ lemma_funcimport__injective x_not_y
    Yes Refl   => Yes Refl
  decEq (FuncImport x)   (TableImport y)  = No lemma_funcimport_not_tableexport
  decEq (FuncImport x)   (MemImport y)    = No lemma_funcimport_not_memexport
  decEq (FuncImport x)   (GlobalImport y) = No lemma_funcimport_not_globalexport
  decEq (TableImport x)  (FuncImport y)   = No lemma_tableimport_not_funcexport
  decEq (TableImport x)  (TableImport y)  = case decEq x y of
    No x_not_y => No $ lemma_tableimport__injective x_not_y
    Yes Refl   => Yes Refl
  decEq (TableImport x)  (MemImport y)    = No lemma_tableimport_not_memexport
  decEq (TableImport x)  (GlobalImport y) = No lemma_tableimport_not_globalexport
  decEq (MemImport x)    (FuncImport y)   = No lemma_memimport_not_funcxport
  decEq (MemImport x)    (TableImport y)  = No lemma_memimport_not_tableexport
  decEq (MemImport x)    (MemImport y)    = case decEq x y of
    No x_not_y => No $ lemma_memimport__injective x_not_y
    Yes Refl   => Yes Refl
  decEq (MemImport x)    (GlobalImport y) = No lemma_memimport_not_globalexport
  decEq (GlobalImport x) (FuncImport y)   = No lemma_globalimport_not_funcxport
  decEq (GlobalImport x) (TableImport y)  = No lemma_globalimport_not_tableexport
  decEq (GlobalImport x) (MemImport y)    = No lemma_globalimport_not_memexport
  decEq (GlobalImport x) (GlobalImport y) = case decEq x y of
    No x_not_y => No $ lemma_globalimport__injective x_not_y
    Yes Refl   => Yes Refl

public export
implementation DecEq Import where
  decEq (MkImport m1 n1 d1) (MkImport m2 n2 d2) = case decEq m1 m2 of
    No m1_not_m2 => No $ lemma_import__module_injective m1_not_m2
    Yes Refl     => case decEq n1 n2 of
      No n1_not_n2 => No $ lemma_import__name_injective n1_not_n2
      Yes Refl     => case decEq d1 d2 of
        No d1_not_d2 => No $ lemma_import__desc_injective d1_not_d2
        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 ContriverText

import Data.SortedSet

orOrd : Ordering -> Ordering -> Ordering
orOrd EQ o2 = o2
orOrd o1 _ = o1

data MyMaybe a = MyNothing | MyJust a

instance Eq a => Eq (MyMaybe a) where
  (==) MyNothing MyNothing = True
  (==) (MyJust v1) (MyJust v2) = (==) v1 v2
  (==) _ _ = False

instance Ord a => Ord (MyMaybe a) where
  compare MyNothing MyNothing = EQ
  compare MyNothing _ = LT
  compare (MyJust v1) (MyJust v2) = compare v1 v2
  compare _ _ = GT

StoryElemId : Type
StoryElemId = String

data Link = LinkTopic StoryElemId

instance Eq Link where
  (==) (LinkTopic s1) (LinkTopic s2) = (==) s1 s2

instance Ord Link where
  compare (LinkTopic s1) (LinkTopic s2) = compare s1 s2

data TextSpan = MkTextSpan String

instance Eq TextSpan where
  (==) (MkTextSpan s1) (MkTextSpan s2) = (==) s1 s2

instance Ord TextSpan where
  compare (MkTextSpan s1) (MkTextSpan s2) = compare s1 s2

data HtextSpan = MkHtextSpan (MyMaybe Link) TextSpan

instance Eq HtextSpan where
  (==) (MkHtextSpan h1 t1) (MkHtextSpan h2 t2) =
    (==) h1 h2 &&
    (==) t1 t2

instance Ord HtextSpan where
  compare (MkHtextSpan h1 t1) (MkHtextSpan h2 t2) =
    compare h1 h2 `orOrd`
    compare t1 t2

data HtextBlock = MkHtextBlock (List HtextSpan)

instance Eq HtextBlock where
  (==) (MkHtextBlock b1) (MkHtextBlock b2) = (==) b1 b2

instance Ord HtextBlock where
  compare (MkHtextBlock b1) (MkHtextBlock b2) = compare b1 b2

-- NOTE: This alternative definition doesn't pan out because the Idris
-- compiler takes way too long to infer the type class instance for
-- (Ord (List (List (MyMaybe Link, TextSpan)))).
--data HtextBlocks = MkHtextBlocks (List (List (MyMaybe Link, TextSpan)))

data HtextBlocks = MkHtextBlocks (List HtextBlock)

instance Eq HtextBlocks where
  (==) (MkHtextBlocks b1) (MkHtextBlocks b2) = (==) b1 b2

instance Ord HtextBlocks where
  compare (MkHtextBlocks b1) (MkHtextBlocks b2) = compare b1 b2

-- TODO: Continue adding more kinds of facts as we need them.
data Fact = ExistsPov StoryElemId
  | ExistsTopic StoryElemId
  | PovWouldDescribe StoryElemId StoryElemId HtextBlocks

instance Eq Fact where
  (==) (ExistsPov p1) (ExistsPov p2) = (==) p1 p2
  (==) (ExistsTopic t1) (ExistsTopic t2) = (==) t1 t2
  (==) (PovWouldDescribe p1 t1 h1) (PovWouldDescribe p2 t2 h2) =
    (==) p1 p2 &&
    (==) t1 t2 &&
    (==) h1 h2
  (==) _ _ = False

instance Ord Fact where
  compare (ExistsPov p1) (ExistsPov p2) = compare p1 p2
  compare (ExistsPov _) _ = LT
  compare (ExistsTopic t1) (ExistsTopic t2) = compare t1 t2
  compare (ExistsTopic _) _ = LT
  compare (PovWouldDescribe p1 t1 h1)
    (PovWouldDescribe p2 t2 h2) =
    foldl orOrd EQ [
      compare p1 p2,
      compare t1 t2,
      compare h1 h2
    ]
  compare _ _ = GT

data StartTime = MkStartTime Nat

instance Eq StartTime where
  (==) (MkStartTime n1) (MkStartTime n2) = (==) n1 n2

instance Ord StartTime where
  compare (MkStartTime n1) (MkStartTime n2) = compare n1 n2

data EndTime = KnownEndTime Nat | AssumeAfter Nat Bool

instance Eq EndTime where
  (==) (KnownEndTime n1) (KnownEndTime n2) = (==) n1 n2
  (==) (AssumeAfter n1 b1) (AssumeAfter n2 b2) =
    (==) n1 n2 &&
    (==) b1 b2
  (==) _ _ = False

instance Ord EndTime where
  compare (KnownEndTime n1) (KnownEndTime n2) = compare n1 n2
  compare (KnownEndTime _) _ = LT
  compare (AssumeAfter n1 b1) (AssumeAfter n2 b2) =
    compare n1 n2 `orOrd`
    compare b1 b2
  compare _ _ = GT

data TemporalFact = MkTemporalFact StartTime EndTime Fact

instance Eq TemporalFact where
  (==) (MkTemporalFact s1 e1 f1) (MkTemporalFact s2 e2 f2) =
    (==) s1 s2 &&
    (==) e1 e2 &&
    (==) f1 f2

instance Ord TemporalFact where
  compare (MkTemporalFact s1 e1 f1) (MkTemporalFact s2 e2 f2) =
    foldl orOrd EQ [
      compare s1 s2,
      compare e1 e2,
      compare f1 f2
    ]

StoryState : Type
StoryState = SortedSet TemporalFact

-- TODO: This EndTime is extremely arbitrary. Once we figure out how
-- we're going to update the game state, we should update this however
-- needed in order for it to persist throughout the game. Maybe this
-- should just have an end time of infinity.
alwaysTrue : Fact -> TemporalFact
alwaysTrue fact =
  MkTemporalFact (MkStartTime 0) (AssumeAfter 10 True) fact

describe : String -> String -> List (List HtextSpan) -> Fact
describe who what how =
  PovWouldDescribe who what (MkHtextBlocks (map MkHtextBlock how))

noLink : String -> HtextSpan
noLink text = MkHtextSpan MyNothing (MkTextSpan text)

initialStoryState : StoryState
initialStoryState = fromList (map alwaysTrue [
  ExistsPov "you",
  ExistsTopic "here",
  describe "you" "here" [[noLink "You are here."]]
])

||| Converts a number to the same number plus one
myInc : Nat -> Nat
myInc x = x + 1

max_stars_repo_name: rocketnia/contrivertext

max_issues_repo_name: rocketnia/contrivertext

max_forks_repo_name: rocketnia/contrivertext


text:
module Main

%default total

%foreign "C:apply_fn,libsmall"
prim_applyFn : String -> Int -> (String -> Int -> String) -> PrimIO String

applyFn : HasIO io => String -> Int -> (String -> Int -> String) -> io String
applyFn s x f = primIO $ prim_applyFn s x f

pluralise : String -> Int -> String
pluralise str x =
  show x ++ " " ++
    if x == 1
       then str
       else str ++ "s"

%foreign "C:apply_fn,libsmall"
prim_applyFnIO : String -> Int -> (String -> Int -> PrimIO String) -> PrimIO String

-- toPrim : IO a -> PrimIO a
applyFnIO : HasIO io => String -> Int -> (String -> Int -> IO String) -> io String
applyFnIO s x f = primIO $ prim_applyFnIO s x (\s, d => toPrim $ f s d)

pluraliseWithMessage : String -> Int -> IO String
pluraliseWithMessage str x =
  do putStrLn "pluralising"
     pure $ show x ++ " " ++
            if x == 1
               then str
               else str ++ "s"

main : IO ()
main = do str1 <- applyFn "Biscuit" 10 pluralise
          putStrLn str1
          str2 <- applyFn "Tree" 1 pluralise
          putStrLn str2
          str3 <- applyFnIO "Human" 5 pluraliseWithMessage
          putStrLn str3
          str4 <- applyFnIO "Dog" 1 pluraliseWithMessage
          putStrLn str4

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

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

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


text:
||| A version of `Dec` that returns a meaningful error message as well as proof of void.
|||
||| When dealing with decidable properties for type-level computations
||| the existing `Dec` data type is useful.  However, when using
||| decidable properties interactively one cannot easily tell why a
||| property failed.  One can always encode failing cases within the
||| property itself but that is not necessarily a advantageous.
|||
||| `DecInfo` provides a data structure to capture decidable properties together with an informative error message for when the property does not hold.
module Toolkit.Decidable.Informative

import Decidable.Equality
%default total

public export
data DecInfo : (errType : Type) -> (prop : Type) -> Type where
   Yes : (prfWhy : prop) -> DecInfo errType prop
   No  : (msgWhyNot : errType) -> (prfWhyNot : prop -> Void) -> DecInfo errType prop

export
otherwise : DecInfo e b -> (a -> b) -> Either (e, Not a) b
otherwise (Yes prfWhy) f = Right prfWhy
otherwise (No msgWhyNot prfWhyNot) f = Left (msgWhyNot, \x => prfWhyNot (f x))

export
try : DecInfo e b -> (a -> b) -> Either (e, Not a) b
try = otherwise

export
decInfoDo : Either (e, Not a) a -> DecInfo e a
decInfoDo (Left (x, y)) = No x y
decInfoDo (Right x) = Yes x

namespace Lift

  export
  otherwise : DecInfo eB b -> (eB -> eA) -> (a -> b) -> Either (eA, Not a) b
  otherwise (Yes prfWhy) _ _ = Right prfWhy
  otherwise (No msgWhyNot prfWhyNot) g f = Left (g msgWhyNot, \x => prfWhyNot (f x))

  export
  try : DecInfo eB b -> (eB -> eA) -> (a -> b) -> Either (eA, Not a) b
  try = otherwise
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Language.LSP.CodeAction.ExprSearch

import Core.CaseTree
import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.UnifyState
import Data.List
import Data.String
import Idris.REPL.Opts
import Idris.Syntax
import Idris.Resugar
import Language.JSON
import Language.LSP.CodeAction
import Language.LSP.Message
import Libraries.Data.PosMap
import Server.Configuration
import Server.Log
import Server.Utils
import TTImp.TTImp
import TTImp.Interactive.ExprSearch

dropLams : Nat -> RawImp -> RawImp
dropLams Z tm = tm
dropLams (S k) (ILam _ _ _ _ _ sc) = dropLams k sc
dropLams _ tm = tm

dropLamsTm : {vars : _} -> Nat -> Env Term vars -> Term vars -> (vars' ** (Env Term vars', Term vars'))
dropLamsTm Z env tm = (_ ** (env, tm))
dropLamsTm (S k) env (Bind _ _ b sc) = dropLamsTm k (b :: env) sc
dropLamsTm _ env tm = (_ ** (env, tm))

buildCodeAction : Name -> URI -> Range -> String -> CodeAction
buildCodeAction name uri range str =
  let textEdit = MkTextEdit range str
      workspaceEdit = MkWorkspaceEdit { changes           = Just (singleton uri [textEdit])
                                      , documentChanges   = Nothing
                                      , changeAnnotations = Nothing
                                      }
   in MkCodeAction { title       = "Expression search on \{show $ dropAllNS name} as ~ \{strSubstr 0 50 str} ..."
                   , kind        = Just RefactorRewrite
                   , diagnostics = Just []
                   , isPreferred = Just False
                   , disabled    = Nothing
                   , edit        = Just workspaceEdit
                   , command     = Nothing
                   , data_       = Nothing
                   }
export
exprSearch : Ref LSPConf LSPConfiguration
          => Ref MD Metadata
          => Ref Ctxt Defs
          => Ref UST UState
          => Ref Syn SyntaxInfo
          => Ref ROpts REPLOpts
          => CodeActionParams -> Core (List CodeAction)
exprSearch params = do
  let True = params.range.start.line == params.range.end.line
    | _ => pure []

  [] <- searchCache params.range ExprSearch
    | actions => do logString Debug "exprSearch: found cached action"
                    pure actions

  fuel <- gets LSPConf searchLimit
  nameLocs <- gets MD nameLocMap
  let line = params.range.start.line
  let col = params.range.start.character
  let Just (loc@(_, nstart, nend), name) = findPointInTreeLoc (line, col) nameLocs
    | Nothing => pure []

  context <- gets Ctxt gamma
  toBrack <- gets Syn (elemBy (\x, y => dropNS x == dropNS y) name . bracketholes)
  let bracket = the (PTerm -> PTerm) $ if toBrack then addBracket replFC else id
  solutions <-
    case !(lookupDefName name context) of
         [(n, nidx, Hole locs _)] =>
           catch (do searchtms <- exprSearchN replFC fuel name []
                     traverse (map (show . bracket) . pterm . dropLams locs) searchtms)
                 (\case Timeout _ => pure []
                        err => do logString Debug "exprSearch: unexpected error while searching"
                                  throw err)
         [(n, nidx, PMDef pi [] (STerm _ tm) _ _)] => case holeInfo pi of
           NotHole => pure []
           SolvedHole locs => do
             let (_ ** (env, tm')) = dropLamsTm locs [] tm
             itm <- resugar env tm'
             pure [show $ bracket itm]
         _ => pure []

  let range = MkRange (uncurry MkPosition nstart) (uncurry MkPosition nend)
  let actions = map (buildCodeAction name params.textDocument.uri range) solutions
  modify LSPConf (record { cachedActions $= insert (cast loc, ExprSearch, actions) })
  pure actions


text:
module Data.LazyPairingHeap

import Decidable.Order

%default total

mutual
  public export
  data LazyPairingHeap : Nat -> Ordered ty to -> Type where
    Empty : .{auto constraint : Ordered ty to} -> LazyPairingHeap Z constraint
    Tree : .{constraint : Ordered ty to}
        -> (x : ty)
        -> {leftCnt : Nat}
        -> (l : LazyPairingHeap leftCnt constraint)
        -> .{auto leftFits : Fits x l}
        -> {rightCnt : Nat}
        -> (r : Lazy $ LazyPairingHeap rightCnt constraint)
        -> .{auto rightFits : Fits x r}
        -> LazyPairingHeap (S (leftCnt + rightCnt)) constraint

  export
  findMin : {constraint : Ordered ty _} -> LazyPairingHeap (S _) constraint -> ty
  findMin (Tree x l r) = x

  export
  Fits : {constraint : Ordered ty to} -> ty -> LazyPairingHeap cnt constraint -> Type
  Fits {cnt = Z} _ _ = ()
  Fits {cnt = S _} {to} x h = to x (findMin h)

mutual
  link : .{constraint : Ordered ty to}
      -> .{cnt1 : Nat} -> (h1 : LazyPairingHeap (S cnt1) constraint)
      -> .{cnt2 : Nat} -> (h2 : LazyPairingHeap (S cnt2) constraint)
      -> .{ltePrf : to (findMin h1) (findMin h2)}
      -> (ret : LazyPairingHeap ((S cnt1) + (S cnt2)) constraint ** findMin ret = findMin h1)
  link {cnt1} {cnt2} {ltePrf} h1@(Tree x Empty r) h2
    = rewrite plusCommutative cnt1 (S cnt2) in
      (Tree (findMin h1) h2 r ** Refl)
  link {constraint} {ltePrf} h1 {cnt2} h2 with (h1)
    | Tree {leftFits} {rightFits} {leftCnt} {rightCnt} x l r
      = rewrite sym $ plusAssociative leftCnt rightCnt (S cnt2) in
        rewrite plusCommutative rightCnt (S cnt2) in
        rewrite plusAssociative leftCnt (S cnt2) rightCnt in
        rewrite plusCommutative leftCnt (S cnt2) in
        rewrite sym $ xFindMin in
        let (merged ** fitsPrf) = merge' {lbound = findMin h1}
                                         {fits1 = rewrite xFindMin in ltePrf}
                                         h2
                                         {fits2 = rewrite xFindMin in leftFits}
                                         l
            (merged' ** fitsPrf') = merge' {lbound = findMin h1}
                                           {fits1 = fitsPrf}
                                           merged
                                           {fits2 = rewrite xFindMin in rightFits}
                                           r
            ret = Tree (findMin h1) Empty merged' in
        (ret ** Refl)
        where xFindMin : findMin h1 = x
              xFindMin = really_believe_me ()

  merge' : .{constraint : Ordered ty to}
        -> {cnt1 : Nat} -> (h1 : LazyPairingHeap cnt1 constraint)
        -> {cnt2 : Nat} -> (h2 : LazyPairingHeap cnt2 constraint)
        -> .{lbound : ty} -> .{fits1 : Fits lbound h1} -> .{fits2 : Fits lbound h2}
        -> (ret : LazyPairingHeap (cnt1 + cnt2) constraint ** Fits lbound ret)
  merge' {fits2} Empty h = (h ** fits2)
  merge' {cnt1} {fits1} h Empty = rewrite plusZeroRightNeutral cnt1 in (h ** fits1)
  merge' {to} {fits1} {fits2} {cnt1 = S n} {cnt2 = S m} h1 h2 with (order {to} (findMin h1) (findMin h2))
    | Left ltePrf = let (ret ** eqPrf) = assert_total $ link {ltePrf} h1 h2 in
                    (ret ** rewrite eqPrf in fits1)
    | Right ltePrf = rewrite plusCommutative n (S m) in
                     rewrite plusSuccRightSucc m n in
                     let (ret ** eqPrf) = assert_total $ link {ltePrf} h2 h1 in
                     (ret ** rewrite eqPrf in fits2)

export
merge : .{constraint : Ordered ty to}
     -> {cnt1 : Nat} -> LazyPairingHeap cnt1 constraint
     -> {cnt2 : Nat} -> LazyPairingHeap cnt2 constraint
     -> LazyPairingHeap (cnt1 + cnt2) constraint
merge Empty h = h
merge {cnt1} h Empty = rewrite plusZeroRightNeutral cnt1 in h
merge {constraint} {ty} {to} {cnt1 = S n} {cnt2 = S m} h1 h2
  = let (lbound ** (fits1, fits2)) = proofs in
        fst $ merge' {lbound} {fits1} {fits2} h1 h2
    where proofs : (lbound : ty ** (Fits lbound h1, Fits lbound h2))
          proofs with (order {to} (findMin h1) (findMin h2))
            | Left ltePrf = let x = findMin h1 in
                            (x ** (reflexive x, ltePrf))
            | Right ltePrf = let x = findMin h2 in
                             (x ** (ltePrf, reflexive x))

export
deleteMin : .{constraint : Ordered ty to} -> LazyPairingHeap (S cnt) constraint -> LazyPairingHeap cnt constraint
deleteMin (Tree _ l r) = merge l r

singleton : {ty : Type} -> {constraint : Ordered ty to} -> ty -> LazyPairingHeap 1 constraint
singleton x = Tree x Empty Empty

export
insert : .{constraint : Ordered ty to} -> {cnt : Nat} -> LazyPairingHeap cnt constraint -> ty -> LazyPairingHeap (S cnt) constraint
insert {cnt} h x = rewrite sym $ plusZeroRightNeutral cnt in
                   rewrite plusSuccRightSucc cnt Z in
                   merge h (singleton x)

namespace CountedPairingHeap
  public export
  CountedPairingHeap : (constraint : Ordered ty to) -> Type
  CountedPairingHeap constraint = (cnt : Nat ** LazyPairingHeap cnt constraint)

  export
  empty : CountedPairingHeap _
  empty = (Z ** Empty)

  export
  findMin : .{constraint : Ordered ty to} -> CountedPairingHeap constraint -> Maybe ty
  findMin (Z ** _) = Nothing
  findMin (S _ ** (Tree x _ _)) = Just x

  export
  deleteMin : CountedPairingHeap constraint -> CountedPairingHeap constraint
  deleteMin (Z ** h) = (Z ** h)
  deleteMin (S cnt ** h) = (cnt ** deleteMin h)

  export
  insert : .{constraint : Ordered ty to} -> CountedPairingHeap constraint -> ty -> CountedPairingHeap constraint
  insert (cnt ** h) x = ((S cnt) ** insert h x)

max_stars_repo_name: jdevuyst/idris-data

max_issues_repo_name: jdevuyst/idris-data

max_forks_repo_name: jdevuyst/idris-data


text:
-- a mini prelude

module Stuff

public export
data Bool = True | False

public export
not : Bool -> Bool
not True = False
not False = True

public export
data Maybe a = Nothing | Just a

infixl 4 &&

public export
(&&) : Bool -> Lazy Bool -> Bool
(&&) True x = x
(&&) False x = False

public export
intToBool : Int -> Bool
intToBool 0 = False
intToBool x = True

public export
ifThenElse : Bool -> Lazy a -> Lazy a -> a
ifThenElse True t e = t
ifThenElse False t e = e

public export
data Nat = Z | S Nat

public export
fromInteger : Integer -> Nat
fromInteger x = ifThenElse (intToBool (prim__eq_Integer x 0))
                      Z (S (fromInteger (prim__sub_Integer x 1)))

public export
plus : Nat -> Nat -> Nat
plus Z y = y
plus (S k) y = S (plus k y)

infixr 5 ::

public export
data List a = Nil | (::) a (List a)

public export
data Equal : a -> b -> Type where
     Refl : {0 x : a} -> Equal x x

public export
data Unit = MkUnit

namespace Builtin -- hardcoded into elaborator!
  public export
  data Pair : Type -> Type -> Type where
       MkPair : {0 a, b : Type} -> (1 x : a) -> (1 y : b) -> Pair a b

public export
fst : {0 a, b : Type} -> (a, b) -> a
fst (x, y) = x

public export
snd : {0 a, b : Type} -> (a, b) -> b
snd (x, y) = y

%pair Pair fst snd

namespace DPair
    public export
    data DPair : (a : Type) -> (a -> Type) -> Type where
         MkDPair : (x : a) -> p x -> DPair a p

    fst : DPair a p -> a
    fst (MkDPair x y) = x

    snd : (x : DPair a p) -> p (fst x)
    snd (MkDPair x y) = y

public export
data Unrestricted : Type -> Type where
     Un : (x : a) -> Unrestricted a

public export
the : (a : Type) -> a -> a
the _ x = x

public export
id : a -> a
id x = x

public export
data Void : Type where

public export
data Dec : Type -> Type where
     Yes : a -> Dec a
     No : (a -> Void) -> Dec a