text:
module Commands

import Data.Strings

import Language.Reflection

import Libraries.Utils.Hex

import public Idris.IDEMode.Commands

import Foreign

%language ElabReflection

public export
data IDEResult
  = OK Int SExp
  | Warning Int SExp
  | Error Int SExp
  | WriteString Int String
  | Output Int SExp
  | Version SExp

export
Show IDEResult where
  show (OK i x) = show i ++ " OK: " ++ show x
  show (Warning i x) = show i ++ " Warning: " ++ show x
  show (Error i x) = show i ++ " Error: " ++ show x
  show (WriteString i x) = show i ++ " WriteString: " ++ show x
  show (Output i x) = show i ++ " Output: " ++ show x
  show (Version x) = "Version: " ++ show x

export
Show IDECommand where
  showPrec p (Interpret x) = showCon p "Interpret" $ showArg x
  showPrec p (LoadFile x y) = showCon p "LoadFile" $ showArg x ++ showArg y
  showPrec p (TypeOf x y) = showCon p "TypeOf" $ showArg x ++ showArg y
  showPrec p (CaseSplit x y z) = showCon p "CaseSplit" $ showArg x ++ showArg y ++ showArg z
  showPrec p (AddClause x y) = showCon p "AddClause" $ showArg x ++ showArg y
  showPrec p (AddMissing x y) = showCon p "AddMissing" $ showArg x ++ showArg y
  showPrec p (ExprSearch x y xs z) = showCon p "ExprSearch" $ showArg x ++ showArg y ++ showArg xs ++ showArg z
  showPrec p ExprSearchNext = "ExprSearchNext"
  showPrec p (GenerateDef x y) = showCon p "GenerateDef" $ showArg x ++ showArg y
  showPrec p GenerateDefNext = "GenerateDefNext"
  showPrec p (MakeLemma x y) = showCon p "MakeLemma" $ showArg x ++ showArg y
  showPrec p (MakeCase x y) = showCon p "MakeCase" $ showArg x ++ showArg y
  showPrec p (MakeWith x y) = showCon p "MakeWith" $ showArg x ++ showArg y
  showPrec p (DocsFor x y) = showCon p "DocsFor" $ showArg x
  showPrec p (Directive x) = showCon p "Directive" $ showArg x
  showPrec p (Apropos x) = showCon p "Apropos" $ showArg x
  showPrec p (Metavariables x) = showCon p "Metavariables" $ showArg x
  showPrec p (WhoCalls x) = showCon p "WhoCalls" $ showArg x
  showPrec p (CallsWho x) = showCon p "CallsWho" $ showArg x
  showPrec p (BrowseNamespace x) = showCon p "BrowseNamespace" $ showArg x
  showPrec p (NormaliseTerm x) = showCon p "NormaliseTerm" $ showArg x
  showPrec p (ShowTermImplicits x) = showCon p "ShowTermImplicits" $ showArg x
  showPrec p (HideTermImplicits x) = showCon p "HideTermImplicits" $ showArg x
  showPrec p (ElaborateTerm x) = showCon p "ElaborateTerm" $ showArg x
  showPrec p (PrintDefinition x) = showCon p "PrintDefinition" $ showArg x
  showPrec p (ReplCompletions x) = showCon p "ReplCompletions" $ showArg x
  showPrec p (EnableSyntax x) = showCon p "EnableSyntax" $ showArg x
  showPrec p (NameAt name _) = showCon p "NameAt" $ showArg name
  showPrec p Version = "Version"
  showPrec p GetOptions = "GetOptions"

export
getResult : SExp -> Maybe IDEResult
getResult (SExpList [SymbolAtom "return", SExpList (SymbolAtom "ok" :: xs), IntegerAtom idx]) =
  Just $ OK (cast idx) (SExpList xs)
getResult (SExpList [SymbolAtom "return", SExpList (SymbolAtom "warning" :: xs), IntegerAtom idx]) =
  Just $ Warning (cast idx) (SExpList xs)
getResult (SExpList [SymbolAtom "warning", xs, IntegerAtom idx]) =
  Just $ Warning (cast idx) xs
getResult (SExpList [SymbolAtom "return", SExpList (SymbolAtom "error" :: xs), IntegerAtom idx]) =
  Just $ Error (cast idx) (SExpList xs)
getResult (SExpList [SymbolAtom "write-string", StringAtom xs, IntegerAtom idx]) =
  Just $ WriteString (cast idx) xs
getResult (SExpList [SymbolAtom "output", xs, IntegerAtom idx]) =
  Just $ Output (cast idx) xs
getResult (SExpList (SymbolAtom "protocol-version" :: xs)) =
  Just $ Version (SExpList xs)
getResult _ = Nothing

export
buildCommand : IDECommand -> IO String
buildCommand cmd = do
  idx <- primIO genHistoryIndex
  ignore $ primIO $ putCmdInHistory idx cmd
  let s = show $ SExpList [toSExp cmd, IntegerAtom (cast idx)]
  pure $ leftPad '0' 6 (asHex $ cast $ length s) ++ s

extractName : String -> String
extractName name = case strM name of
                        StrCons '?' name' => name'
                        _ =>
                          case name of
                            "="    => "Equal"
                            "()"   => "MkUnit"
                            "(,)"  => "MkPair"
                            "(**)" => "MkDPair"
                            "**"   => "MkDPair"
                            "[]"   => "Nil"
                            _      => name
export
interpret : IO ()
interpret = do
  client <- primIO getGlobalClient
  sel <- extractName <$> getSelection
  write client !(buildCommand $ Interpret sel)

export
loadCurrent : IO ()
loadCurrent = do
  saveBuffer
  client <- primIO getGlobalClient
  path <- filePath
  write client !(buildCommand $ LoadFile path Nothing)

export
typeOf : IO ()
typeOf = do
  when !isBufferModified loadCurrent
  client <- primIO getGlobalClient
  name <- extractName <$> cursorWord
  line <- cast <$> cursorLine
  col <- cast <$> cursorColumn
  write client !(buildCommand $ TypeOf name (Just (line, col)))

export
typeOfPrompt : IO ()
typeOfPrompt = do
  when !isBufferModified loadCurrent
  client <- primIO getGlobalClient
  name <- extractName <$> nvimEval "input('> ')"
  write client !(buildCommand $ TypeOf name Nothing)

export
typeOfSel : IO ()
typeOfSel = do
  when !isBufferModified loadCurrent
  client <- primIO getGlobalClient
  sel <- extractName <$> getSelection
  line <- cast <$> cursorLine
  col <- cast <$> cursorColumn
  write client !(buildCommand $ TypeOf sel (Just (line, col)))

export
nameAt : IO ()
nameAt = do
  when !isBufferModified loadCurrent
  client <- primIO getGlobalClient
  name <- extractName <$> cursorWord
  write client !(buildCommand $ NameAt name Nothing)

export
nameAtPrompt : IO ()
nameAtPrompt = do
  when !isBufferModified loadCurrent
  client <- primIO getGlobalClient
  name <- extractName <$> nvimEval "input('> ')"
  write client !(buildCommand $ NameAt name Nothing)

export
nameAtSel : IO ()
nameAtSel = do
  when !isBufferModified loadCurrent
  client <- primIO getGlobalClient
  sel <- extractName <$> getSelection
  write client !(buildCommand $ NameAt sel Nothing)

export
docOverview : IO ()
docOverview = do
  when !isBufferModified loadCurrent
  client <- primIO getGlobalClient
  name <- extractName <$> cursorWord
  write client !(buildCommand $ DocsFor name (Just Overview))

export
docFull : IO ()
docFull = do
  when !isBufferModified loadCurrent
  client <- primIO getGlobalClient
  name <- extractName <$> cursorWord
  write client !(buildCommand $ DocsFor name (Just Full))

export
caseSplit : IO ()
caseSplit = do
  when !isBufferModified loadCurrent
  client <- primIO getGlobalClient
  line <- cast <$> cursorLine
  col <- cast <$> cursorColumn
  name <- extractName <$> cursorWord
  write client !(buildCommand $ CaseSplit line col name)

export
addClause : IO ()
addClause = do
  when !isBufferModified loadCurrent
  client <- primIO getGlobalClient
  line <- cast <$> cursorLine
  name <- extractName <$> cursorWord
  write client !(buildCommand $ AddClause line name)

-- NOT IMPLEMENTED YET: addMissing : IO ()

export
exprSearch : IO ()
exprSearch = do
  when !isBufferModified loadCurrent
  client <- primIO getGlobalClient
  line <- cast <$> cursorLine
  name <- extractName <$> cursorWord
  -- TODO: add hints option
  write client !(buildCommand $ ExprSearch line name [] False)

export
exprSearchNext : IO ()
exprSearchNext = do
  when !isBufferModified loadCurrent
  client <- primIO getGlobalClient
  -- TODO: add hints option
  write client !(buildCommand ExprSearchNext)

export
generateDef : IO ()
generateDef = do
  when !isBufferModified loadCurrent
  client <- primIO getGlobalClient
  line <- cast <$> cursorLine
  name <- extractName <$> cursorWord
  write client !(buildCommand $ GenerateDef line name)

export
generateDefNext : IO ()
generateDefNext = do
  when !isBufferModified loadCurrent
  client <- primIO getGlobalClient
  write client !(buildCommand GenerateDefNext)

export
makeLemma : IO ()
makeLemma = do
  when !isBufferModified loadCurrent
  client <- primIO getGlobalClient
  line <- cast <$> cursorLine
  name <- extractName <$> cursorWord
  write client !(buildCommand $ MakeLemma line name)

export
makeCase : IO ()
makeCase = do
  when !isBufferModified loadCurrent
  client <- primIO getGlobalClient
  -- TODO: replace in code
  line <- cast <$> cursorLine
  name <- extractName <$> cursorWord
  write client !(buildCommand $ MakeCase line name)

export
makeWith : IO ()
makeWith = do
  when !isBufferModified loadCurrent
  client <- primIO getGlobalClient
  -- TODO: replace in code
  line <- cast <$> cursorLine
  name <- extractName <$> cursorWord
  write client !(buildCommand $ MakeWith line name)

-- NOT IMPLEMENTED YET: directive : IO ()
-- NOT IMPLEMENTED YET: apropos : IO ()

export
metavariables : IO ()
metavariables = do
  when !isBufferModified loadCurrent
  client <- primIO getGlobalClient
  write client !(buildCommand $ Metavariables 1)

-- NOT IMPLEMENTED YET: whocalls : IO ()
-- NOT IMPLEMENTED YET: callswho : IO ()

export
browseNamespace : IO ()
browseNamespace = do
  when !isBufferModified loadCurrent
  client <- primIO getGlobalClient
  name <- extractName <$> cursorWord'
  write client !(buildCommand $ BrowseNamespace name)

-- NOT IMPLEMENTED YET: normaliseTerm : IO ()
-- NOT IMPLEMENTED YET: showTermImplicits : IO ()
-- NOT IMPLEMENTED YET: hideTermImplicits : IO ()
-- NOT IMPLEMENTED YET: elaborateTerm : IO ()
-- NOT IMPLEMENTED YET: printDefinition : IO ()
-- NOT IMPLEMENTED YET: replCompletions : IO ()

-- export
-- enableSyntax : Bool -> IO ()
-- enableSyntax b = do
--   client <- primIO getGlobalClient
--   write client !(buildCommand $ EnableSyntax b)

export
getOptions : IO ()
getOptions = do
  client <- primIO getGlobalClient
  write client !(buildCommand GetOptions)

%foreign "_, _ => 0"
export
loadRef : a -> IO ()

export
loadCommands : IO ()
loadCommands = do
  loadRef interpret
  loadRef loadCurrent
  loadRef typeOf
  loadRef typeOfPrompt
  loadRef typeOfSel
  loadRef nameAt
  loadRef nameAtPrompt
  loadRef nameAtSel
  loadRef docOverview
  loadRef docFull
  loadRef caseSplit
  loadRef addClause
  loadRef exprSearch
  loadRef exprSearchNext
  loadRef generateDef
  loadRef generateDefNext
  loadRef makeLemma
  loadRef makeCase
  loadRef makeWith
  loadRef metavariables
  loadRef browseNamespace
  -- loadRef enableSyntax
  loadRef getOptions

export %macro
commandBinding : Bool -> Name -> Elab String
commandBinding b n = do
  [(name, _)] <- getType n
    | _ => fail $ show n ++ " is not unique in scope"
  if b
     then pure $ ":lua idris['" ++ show name ++ "'](W)<CR>"
     else pure $ "lua idris['" ++ show name ++ "'](W)"


text:
module Bezout

import Data.Vect
import Data.Fin

{-Copied from Chinmaya's code. Gives quotient and remainder on divison-}
{-This just computes the qoutient and the remainder, but it doesn't prove that they indeed satisfy the conditions a = b*q + r and r < b -}
Eucl: (a: Nat) -> (b: Nat) -> (Nat, Nat)
Eucl Z b = (Z,Z)
Eucl (S k) b = case (lte (S (S k)) b) of
                    False => (S(fst(Eucl (minus (S k) b) b)), snd(Eucl (minus (S k) b) b))
                    True => (Z, S k)
{-Just a slight modification of the Euclid's division function to give the remainder -}
rem : (a : Nat) -> (b : Nat) -> Nat
rem Z b = Z
rem (S k) b = case (lte (S (S k)) b) of
                    False => (rem (minus (S k) b) b)
                    True => (S k)
{-Let rk be the remainder in the Euclidean algorithm at the k-2th step.
Let rk = ak*r0 + bk*r1 where r0 and r1 are the original inputs.Correspondingly  rsk = ask*r0 + bsk*r1 where sk = k+1
Then the I am going to the next step in the Euclid algorithm and changing the coefficients.
These formulas can be easily derived.-}
Euclnos: (Int,Int,Int,Int,Int,Int)->(Int,Int,Int,Int,Int,Int)
Euclnos (rk, rsk ,ak ,ask, bk ,bsk) = (rsk,rssk,ask,assk,bsk,bssk) where
  rssk = cast(snd (Eucl (cast rk) (cast rsk)))
  bssk =bk-bsk* (cast(fst (Eucl (cast rk) (cast rsk))))
  assk =ak-ask* (cast(fst (Eucl (cast rk) (cast rsk))))
{-Does the Euclnos repeatedy until the remainder is zero. Then the previous remainder is the GCD.-}
Bezouttuple: (Int,Int,Int,Int,Int,Int)->(Int,Int,Int,Int,Int,Int)
Bezouttuple (rk, rsk ,ak ,ask, bk, bsk) = case rsk of
                                        0 => (rk, rsk, ak, ask, bk, bsk)
                                        _ => (Bezouttuple (Euclnos (rk ,rsk, ak ,ask ,bk ,bsk)))
{-Returns 2 particular integers out of a 6 tuple-}
returnab: (Int,Int,Int,Int,Int,Int)->(Int,Int)
returnab (a ,b ,c ,d, e ,f)  = (c,e)
{-Returns the Bezout coefficients-}
Bezout : Nat ->Nat ->(Int, Int)
Bezout k j =  (returnab(Bezouttuple((cast k) , (cast j),1, 0 ,0 ,1)))

{-}
just the functions to compute the GCD in two different ways.
{-}

gcd2 : Nat -> Nat -> Nat
gcd2 a b = (cast (((cast a)*(snd (Bezout a b))) + ((cast b)*(fst (Bezout a b)))))

gcdab : Nat -> Nat -> Nat
gcdab b Z = b
gcdab a b = gcdab b (snd (Eucl a b))

{-}
given below are the auxilary functions to the proof that given a and b, there exist q and r such that a = b*q + r.
The algorithm above just computes these two numbers, but it doesn't prove that (a = b*q + r and r < b)

f1 is the proof that a + 1 = b*q + (r + 1) given that a = b*q + r

aux1f2 is the proof that given a + 1 <= b, a <= b
aux2f2 is the proof that given a and b, either a <= b or a >= b + 1

aux1f3 is the proof that given a <= b and b <= a, a = b
aux2f3 proves that a = b + c and c = d together imply a = b + d
aux3f3 is the proof that given a = b*c + b, a = b*(c + 1) + 0

All these proofs (except maybe aux2f3) were necessary to avoid various type mismatch errors.
{-}

apNat2 : (a : Nat) -> (b : Nat) -> (a = b) -> (S a = S b)
apNat2 a a Refl = Refl

aux1f2 : (a : Nat) -> (b : Nat) -> (LTE (S a) b) -> (LTE a b)
aux1f2 Z Z LTEZero impossible
aux1f2 Z Z (LTESucc _) impossible
aux1f2 Z (S k) x = LTEZero
aux1f2 (S a) (S k) (LTESucc x) = (LTESucc (aux1f2 a k x))

aux2f2 : (a : Nat) -> (b : Nat) -> (Either (LTE a b) (LTE (S b) a))
aux2f2 Z Z  = Left LTEZero
aux2f2 Z (S b) = Left LTEZero
aux2f2 (S k) Z = Right (LTESucc LTEZero)
aux2f2 (S k) (S b) = step where
                  step = case (aux2f2 k b) of
                    (Left l) => (Left (LTESucc l))
                    (Right r) => (Right (LTESucc r))

f1 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (a = b + c) -> ((S a) = b + (S c))
f1 a c k pf = (trans (apNat2 a (c + k) pf) (plusSuccRightSucc c k))

aux1f3 : (a : Nat) -> (b : Nat) -> (LTE a b) -> (LTE b a) -> (a = b)
aux1f3 Z Z LTEZero LTEZero = Refl
aux1f3 Z (S _) LTEZero LTEZero impossible
aux1f3 Z (S _) LTEZero (LTESucc _) impossible
aux1f3 (S _) Z LTEZero LTEZero impossible
aux1f3 (S _) Z (LTESucc _) LTEZero impossible
aux1f3 (S k) (S j) (LTESucc x) (LTESucc y) = (apNat2 k j (aux1f3 k j x y))

aux2f3 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (d : Nat) -> (a = b + c) -> (c = d) -> (a = b + d)
aux2f3 a b Z Z prf Refl = prf
aux2f3 _ _ Z (S _) _ Refl impossible
aux2f3 _ _ (S _) Z _ Refl impossible
aux2f3 (b + (S j)) b (S j) (S j) Refl Refl = Refl

aux3f3 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (a = (b*c) + b) -> (a = b*(S c) + Z)
aux3f3 a b k prf = (trans (trans (trans (prf) (plusCommutative (b*k) b)) (sym (multRightSuccPlus b k))) (sym (plusZeroRightNeutral (b*(S k)))))

{-Caveat : the function elemproof hasn't been programmed for the divisor b being equal to zero -}
{-replacig b with (S b) everywhere in the proof has been done to avoid the case b = 0-}

elemproof1 : (a : Nat) -> (b : Nat) -> (x : (Nat, Nat) ** ((a = (b*(fst x)) + (snd x)) , (LTE (S (snd x)) b)))
elemproof1 Z (S b) = ((0,0) ** ((sym (trans (trans (plusCommutative ((S b)*Z) Z) (sym (multLeftSuccPlus (S b) Z))) (multZeroRightZero (S (S b))))), (LTESucc LTEZero)))
elemproof1 (S k) (S b) = step where
                     step = case (elemproof1 k (S b)) of
                       ((q,r) ** (pf , pff)) => case (aux2f2 (S (S r)) (S b)) of
                                                  Left l => ((q , (S r)) ** ((f1 k ((S b)*q) r pf) , l))
                                                  Right (LTESucc ri) => (((S q) , Z) ** ((aux3f3 (S k) (S b) q (aux2f3 (S k) ((S b)*q) (S r) (S b) (f1 k ((S b)*q) r pf) (aux1f3 (S r) (S b) pff ri))) , (LTESucc LTEZero)))

{-proof of existence of remainders and quotients is necessary to define the concept of divisibilty -}
{-The next step ahead might be to proof the uniqueness of these remainders and quotients probably -}

ext: idr


text:
module Test.Functors

import Test.Assert
import Data.Bifunctor

foo : Either String Int
foo = Right 123

bar : Either String Int
bar = Left "hi"

fooIdentity : IO ()
fooIdentity = assertEq "`foo` satisfies the identity property" (bimap id id foo) foo

fooComposition : IO ()
fooComposition = assertEq "`foo` satisfies the composition property"
  (bimap id (show . (+ 3)) foo) ((bimap id show . bimap id (+ 3)) foo)

barIdentity : IO ()
barIdentity = assertEq "`bar` satisfies the identity property" (bimap id id bar) bar

barComposition : IO ()
barComposition = assertEq "`bar` satisfies the composition property"
  (bimap ((++ "!") . (++ "there")) id bar) ((bimap (++ "!") id . bimap (++ "there") id) bar)

fooRmap : IO ()
fooRmap = assertEq "`rmap (+ 3) foo` returns `Right 126`" (rmap (+ 3) foo) (Right 126)

fooLmap : IO ()
fooLmap = assertEq "`lmap` has no effect on a `Right` value" (lmap (++ "!") foo) foo

barRmap : IO ()
barRmap = assertEq "`rmap` has no effect on a `Left` value" (rmap (+ 3) bar) bar

barLmap : IO ()
barLmap = assertEq "`lmap (++ \"!\") bar` returns `Left \"hi!\"`" (lmap (++ "!") bar) (Left "hi!")

export
main : IO ()
main = do
  putStrLn "Testing Bifunctor..."
  fooIdentity
  fooComposition
  barIdentity
  barComposition
  fooRmap
  fooLmap
  barRmap
  barLmap
  putStrLn "Done.\n"

max_stars_repo_name: Risto-Stevcev/idris-functors

max_issues_repo_name: Risto-Stevcev/idris-functors

max_forks_repo_name: Risto-Stevcev/idris-functors


text:
%default total

--changing codata to dat would make "ones" non-total
codata Stream' : Type -> Type where
  (::) : (e : a) -> Stream' a -> Stream' a

ones : Stream' Nat
ones = 1 :: ones


text:
module Flexidisc.Function

import Flexidisc.TaggedValue

%default total
%access public export

infixr 8 |->
infix 7 ~~

||| A wrapper for functions to allow definition of typeclasses
record (|->) (a : Type) (b : Type) where
  constructor F
  unwrap : (a -> b)

Functor ((|->) a) where
  map g (F f) = F (g . f)

Applicative ((|->) a) where
  pure x = F (const x)
  (<*>) (F f) (F x) = F (\y => f y (x y))

(~~) : (l : k) -> (a -> b) -> TaggedValue l (a |-> b)
(~~) l f = l := F f

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module Sub01Apply18x3

import ProofColDivSeqBase
import ProofColDivSeqPostulate
import ProofColDivSeqPostuProof

%default total
-- %language ElabReflection

-- 3(6x+1) --B[1,-2]--> 3x
export
apply18x3 : (Not . P) (S (plus (plus (plus k k) (plus k k)) (plus k k)))
  -> (m : Nat **
      (LTE (S m) (S (plus (plus (plus k k) (plus k k)) (plus k k))), (Not . P) m))
apply18x3 {k} col = (k ** (lte18x3 k, b18x3To3x k col)) where
  lte18x3 : (k:Nat) -> LTE (S k) (S (plus (plus (plus k k) (plus k k)) (plus k k)))
  lte18x3 Z = LTESucc LTEZero
  lte18x3 (S k) = 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 (plus k k) (plus k k)) (S (plus k k)))) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) (plus k k)) (plus k k))) in
      (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc) (lte18x3 k)


text:
module RandomUtilities

import System.Random
import Data.Vect

||| Generate a vector of random doubles
export
randomVect : (n : Nat) -> IO (Vect n Double)
randomVect 0 = pure []
randomVect (S k)  = do
  r <- randomRIO (0,2*pi)
  v <- randomVect k
  pure (r :: v)

max_stars_repo_name: zamdzhiev/Qimaera

max_issues_repo_name: zamdzhiev/Qimaera

max_forks_repo_name: zamdzhiev/Qimaera


text:
module GameServer.Protocol.Messages

import Network.Socket.Raw

import GameServer.Protocol.Binary

%cg chez libidris_net.so

public export
data Message : Type where
  ListGames : Message
  NewGame :  (numHumans, numRobots : Int ) -> Message
  JoinGame : (playerName : String) -> (gameId : String) -> Message
  Action : (payload : String) -> Message
  Bye : Message

export
Show Message where
  show ListGames = "ListGames"
  show (NewGame numHumans numRobots) = "NewGame " ++ show numHumans ++ " " ++ show numRobots
  show (JoinGame playerName gameId) = "JoinGame " ++ playerName ++ " " ++ gameId
  show (Action payload) = "Action " ++ payload
  show Bye = "Bye"

public export
data Result : Type where
  PlayerRegistered : ( playerKey , gameId : String )  -> Result
  NewGameStarted : (gameId : String ) -> Result
  GameStarts : (gameId : String ) -> Result
  GamesList : (games : List String) -> Result
  InputRequired : ( payload : String ) -> Result
  ErrorMessage : (reason : String ) -> Result

export
Show Result where
  show (PlayerRegistered playerKey gameId) = "PlayerRegistered " ++ playerKey ++ " " ++ gameId
  show (NewGameStarted gameId) = "NewGameStarted " ++ gameId
  show (GameStarts gameId) = "GameStarts " ++ gameId
  show (GamesList games) = "GamesList " ++ show games
  show (InputRequired payload) = "InputRequired " ++ show payload
  show (ErrorMessage reason) = "ErrorMessage " ++ show reason

-- Encoder

export
encodeMessage : (prt:BufPtr) -> (offset:Int) -> (msg : Message) -> IO ()
encodeMessage ptr offset ListGames = sock_poke ptr offset 0
encodeMessage ptr offset (NewGame numHumans numRobots) =
  do sock_poke ptr offset 1
     write32be (cast numHumans) (offset + 1) ptr
     write32be (cast numRobots) (offset + 5) ptr
encodeMessage ptr offset (JoinGame playerName gameId) =
  do sock_poke ptr offset 2
     off <- writeString ptr (cast offset + 1) playerName
     _ <- writeString ptr off gameId
     pure ()
encodeMessage ptr offset (Action payload) =
  do sock_poke ptr offset 3
     writeString ptr (cast offset + 1) payload
     pure ()
encodeMessage ptr offset Bye = sock_poke ptr offset 4

export
prepareMessage : (msg : Message) -> IO (BufPtr, Int)
prepareMessage ListGames =
  do buf <- sock_alloc 9
     write64be 1 buf
     sock_poke buf 8 0
     pure (buf, 9)
prepareMessage (NewGame numHumans numRobots) =
  do buf <- sock_alloc (8 + 1 + 4 + 4)
     write64be 9 buf
     sock_poke buf 8 1
     write32be (cast numHumans) 9 buf
     write32be (cast numRobots) 13 buf
     pure (buf, 17)
prepareMessage (JoinGame playerName gameId) =
  do let len = (8 + 1 + (length playerName + 4) + (length gameId + 4))
     buf <- sock_alloc (cast len)
     write64be (cast len - 8) buf
     sock_poke buf 8 2
     off <- writeString buf 9 playerName
     writeString buf off gameId
     pure (buf, cast len)
prepareMessage (Action payload) =
  do let len = 8 + 1 + (length payload + 4)
     buf <- sock_alloc (cast len)
     write64be (cast len - 8) buf
     sock_poke buf 8 3
     off <- writeString buf 9 payload
     pure (buf, cast len)
prepareMessage Bye =
  do buf <- sock_alloc 9
     write64be 1 buf
     sock_poke buf 8 4
     pure (buf, 9)

-- Decoder

decodeNewGame : (ptr : BufPtr) -> (offset : Integer) -> (len : Integer) -> IO (Either String Message)
decodeNewGame ptr offset len =
  do numHumans <- sock_peek ptr (cast offset)
     numRobots <- sock_peek ptr (cast $ offset + 1)
     pure $ Right $ NewGame numHumans numRobots

decodeJoinGame : (ptr : BufPtr) -> (offset : Integer) -> (len : Integer) -> IO (Either String Message)
decodeJoinGame ptr offset len =
  do (playerName, off) <- readString ptr offset
     (gameId, off') <- readString ptr off
     pure $ Right $ JoinGame playerName gameId

decodeAction : (ptr : BufPtr) -> (offset : Integer) -> (len : Integer) -> IO (Either String Message)
decodeAction ptr offset len =
  do (payload, _) <- readString ptr offset
     pure $ Right $ Action payload

export
decodeMessage : (ptr : BufPtr) -> (len : Integer) -> IO (Either String Message)
decodeMessage ptr len =
  do tag <- sock_peek ptr 0
     case tag of
       0 => pure $ Right ListGames
       1 => decodeNewGame ptr 1 len
       2 => decodeJoinGame ptr 1 len
       3 => decodeAction ptr 1 len
       4 => pure $ Right Bye
       _ => pure $ Left $ "unknown tag " ++ show tag

namespace Test

  export
  test_parseMessage : IO ()
  test_parseMessage = do
    (buf,len) <- prepareMessage (Action "payload")
    Right msg <- decodeMessage buf (cast len)
      | Left err => putStrLn ("error " ++ err)
    putStrLn $ show msg

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
module Compiler.Erlang.IR.AbstractFormat

import public Data.Vect

import public Compiler.Erlang.Utils.PrimTerm

%default total

-- This file contain representations of Erlang's Abstract Format,
-- as described here: https://erlang.org/doc/apps/erts/absform.html

public export
Line : Type
Line = Int

public export
data Literal : Type where
  ALAtom : Line -> String -> Literal
  ALChar : Line -> Char -> Literal
  ALFloat : Line -> Double -> Literal
  ALInteger : Line -> Integer -> Literal
  ALCharlist : Line -> String -> Literal

public export
data MapFieldAssoc : Type -> Type where
  MkAssoc : Line -> (key : a) -> (value : a) -> MapFieldAssoc a

public export
data MapFieldExact : Type -> Type where
  MkExact : Line -> (key : a) -> (value : a) -> MapFieldExact a

public export
data BitType = ABInteger | ABFloat | ABBinary | ABBytes | ABBitstring | ABBits | ABUtf8 | ABUtf16 | ABUtf32

public export
data BitSignedness = ABUnsigned | ABSigned

public export
data BitEndianness = ABBig | ABLittle | ABNative

-- Unit is a value from 1-256 where `FZ` is representing the value 1
public export
data BitUnit = MkBitUnit (Fin 256)

public export
data BitSize : Type where
  ABSDefault : BitSize
  ABSInteger : Line -> Integer -> BitSize
  ABSVar : Line -> String -> BitSize

public export
record TypeSpecifierList where
  constructor MkTSL
  signedness : Maybe BitSignedness
  endianness : Maybe BitEndianness
  type : Maybe BitType
  unit : Maybe BitUnit

public export
data BitSegment : Type -> Type where
  MkBitSegment : Line -> a -> (size : BitSize) -> TypeSpecifierList -> BitSegment a

public export
data BitPattern : Type where
  ABPInteger : Line -> Integer -> BitPattern
  ABPFloat : Line -> Double -> BitPattern
  ABPCharlist : Line -> String -> BitPattern
  ABPUniversal : Line -> BitPattern -- Wildcard matching
  ABPVar : Line -> (name : String) -> BitPattern

public export
data Pattern : Type where
  APLiteral : Literal -> Pattern
  APBitstring : Line -> List (BitSegment BitPattern) -> Pattern
  -- Compound pattern
  APCons : Line -> Pattern -> Pattern -> Pattern
  APMap : Line -> List (MapFieldExact Pattern) -> Pattern
  APNil : Line -> Pattern
  -- Operator pattern
  -- Paranthesized pattern
  -- Record field index pattern
  -- Record pattern
  APTuple : Line -> List Pattern -> Pattern
  APUniversal : Line -> Pattern -- Wildcard matching
  APVar : Line -> (name : String) -> Pattern

public export
data Guard : Type where
  AGLiteral : Literal -> Guard
  -- Bitstring constructor
  AGCons : Line -> Guard -> Guard -> Guard
  AGFunCall : Line -> (fnName : String) -> List Guard -> Guard -- NOTE: Function calls are restricted to the 'erlang' module
  -- Map creation
  -- Map update
  AGNil : Line -> Guard
  AGOp : Line -> (op : String) -> Guard -> Guard -> Guard
  -- Paranthesized guard
  -- Record creation
  -- Record field access
  -- Record field index
  AGTuple : Line -> List Guard -> Guard
  AGVar : Line -> (name : String) -> Guard

-- A guard sequence `Gd1, Gd2; Gd3, Gd4` has the same meaning as:
-- `(Gd1 andalso Gd2) orelse (Gd3 andalso Gd4)`
--
-- A guard sequence is represented by the type `List GuardAlt`:
-- * You can have zero or more `GuardAlt` expressions.
-- * Each `GuardAlt` needs to have at least one `Guard` expression.
public export
data GuardAlt : Type where
  MkGuardAlt : (guards : Vect (S k) Guard) -> GuardAlt

mutual
  public export
  data Expr : Type where
    AELiteral : Literal -> Expr
    AEBitstring : Line -> List (BitSegment Expr) -> Expr
    -- Bitstring comprehension
    AEBlock : Line -> (body : Vect (S k) Expr) -> Expr
    AECase : Line -> Expr -> (clauses : Vect (S k) CaseClause) -> Expr
    -- Catch expression
    AECons : Line -> Expr -> Expr -> Expr
    -- Function reference
    AEFun : Line -> (arity : Nat) -> (clauses : Vect (S k) (FunClause arity)) -> Expr
    AEFunCall : Line -> (fn : Expr) -> (args : List Expr) -> Expr
    AERemoteRef : Line -> (modName : Expr) -> (fnName : Expr) -> Expr
    -- If expression
    -- List comprehension
    AEMapNew : Line -> List (MapFieldAssoc Expr) -> Expr
    -- Map update
    AEMatch : Line -> (lhs : Pattern) -> (rhs : Expr) -> Expr
    AENil : Line -> Expr
    AEOp : Line -> (op : String) -> (lhs : Expr) -> (rhs : Expr) -> Expr
    -- Paranthesized expression
    AEReceive : Line -> List CaseClause -> ReceiveTimeout -> Expr
    -- Record creation expression
    -- Record update expression
    AETuple : Line -> List Expr -> Expr
    AETry : Line -> (sc : Vect (S k) Expr) -> List CaseClause -> List CatchClause -> (afterBody : List Expr) -> Expr
    AEVar : Line -> (name : String) -> Expr

  public export
  data FunClause : Nat -> Type where
    MkFunClause : Line -> Vect arity Pattern -> List GuardAlt -> (body : Vect (S k) Expr) -> FunClause arity

  public export
  data CaseClause : Type where
    MkCaseClause : Line -> Pattern -> List GuardAlt -> (body : Vect (S k) Expr) -> CaseClause

  public export
  data CatchClause : Type where
    MkCatchClause : Line -> (class : Pattern) -> (reason : Pattern) -> (stacktrace : Pattern) -> List GuardAlt -> (body : Vect (S k) Expr) -> CatchClause

  public export
  data ReceiveTimeout : Type where
    NoTimeout : ReceiveTimeout
    TimeoutAfter : (ms : Expr) -> (body : Vect (S k) Expr) -> ReceiveTimeout

public export
data Decl : Type where
  ADExport : Line -> List (String, Nat) -> Decl
  -- ADImport
  ADModule : Line -> (name : String) -> Decl
  -- ADFile
  ADFunDef : Line -> (name : String) -> (arity : Nat) -> (clauses : Vect (S k) (FunClause arity)) -> Decl
  -- ADFunSpec
  -- ADRecord
  -- ADType
  ADAttribute : Line -> (attr : String) -> (value : PrimTerm) -> Decl

-- LINE HELPERS

export
getLiteralLine : Literal -> Line
getLiteralLine (ALAtom l _) = l
getLiteralLine (ALChar l _) = l
getLiteralLine (ALFloat l _) = l
getLiteralLine (ALInteger l _) = l
getLiteralLine (ALCharlist l _) = l

export
getGuardLine : Guard -> Line
getGuardLine (AGLiteral lit) = getLiteralLine lit
getGuardLine (AGCons l _ _) = l
getGuardLine (AGFunCall l _ _) = l
getGuardLine (AGNil l) = l
getGuardLine (AGOp l _ _ _) = l
getGuardLine (AGTuple l _) = l
getGuardLine (AGVar l _) = l


text:
module Streaming

import public Streaming.Streams as S
import public Streaming.API as S


text:
module Deque

%default total
%access private

public export
interface Deque (q : Type -> Type) where
  empty : q a
  isEmpty : q a -> Bool

  cons : a -> q a -> q a
  head : q a -> a
  tail : q a -> q a

  snoc : q a -> a -> q a
  last : q a -> a
  init : q a -> q a


text:
module ProofColDivSeqMain

import ProofColDivSeqBase
import ProofColDivSeqPostulate
import ProofColDivSeqLvDown
import Sub01Apply18x3
import Sub02Apply54x12
import Sub03Apply54x30
import Sub04Apply54x48
import Sub05Apply9x6
import Sub06Apply36x9
import Sub07Apply108x27
import Sub08Apply108x63
import Sub09Apply108x99
import Sub10Apply108x18
import Sub11Apply108x54
import Sub12Apply108x90
import Sub13Apply108x36
import Sub14Apply108x72
import Sub15Apply108x108

%default total
-- %language ElabReflection

-- 無限降下法の十分条件
unifi : (n:Nat) -> P (S n) 2 -> (m ** (LTE (S m) (S n), P m 2))
unifi n prf with (mod3 n)
  unifi (j + j + j)         prf | ThreeZero with (parity j)
    unifi ((k+k) + (k+k) + (k+k))       prf | ThreeZero | Even = apply18x3 prf
    unifi (S (k+k) + S (k+k) + S (k+k)) prf | ThreeZero | Odd with (mod3 k)
      unifi (S ((l+l+l)+(l+l+l)) + S ((l+l+l)+(l+l+l)) + S ((l+l+l)+(l+l+l))) prf | ThreeZero | Odd | ThreeZero = apply54x12 prf
      unifi (S ((S (l+l+l))+(S (l+l+l))) + S ((S (l+l+l))+(S (l+l+l))) + S ((S (l+l+l))+(S (l+l+l)))) prf | ThreeZero | Odd | ThreeOne = apply54x30 prf
      unifi (S ((S (S (l+l+l)))+(S (S (l+l+l)))) + S ((S (S (l+l+l)))+(S (S (l+l+l)))) + S ((S (S (l+l+l)))+(S (S (l+l+l))))) prf | ThreeZero | Odd | ThreeTwo = apply54x48 prf
  unifi (S (j + j + j))     prf | ThreeOne = apply9x6 prf
  unifi (S (S (j + j + j))) prf | ThreeTwo with (parity j)
    unifi (S (S ((k+k) + (k+k) + (k+k)))) prf | ThreeTwo | Even with (parity k)
      unifi (S (S (((l+l)+(l+l)) + ((l+l)+(l+l)) + ((l+l)+(l+l))))) prf | ThreeTwo | Even | Even = apply36x9 prf
      unifi (S (S ((S (l+l)+S (l+l)) + (S (l+l)+S (l+l)) + (S (l+l)+S (l+l))))) prf | ThreeTwo | Even | Odd with (mod3 l)
        unifi (S (S ((S ((o+o+o)+(o+o+o))+S ((o+o+o)+(o+o+o))) + (S ((o+o+o)+(o+o+o))+S ((o+o+o)+(o+o+o))) + (S ((o+o+o)+(o+o+o))+S ((o+o+o)+(o+o+o)))))) prf | ThreeTwo | Even | Odd | ThreeZero = apply108x27 prf
        unifi (S (S ((S (S (o+o+o)+S (o+o+o))+S (S (o+o+o)+ S (o+o+o))) + (S (S (o+o+o)+ S (o+o+o))+S (S (o+o+o)+ S (o+o+o))) + (S (S (o+o+o)+ S (o+o+o))+S (S (o+o+o)+ S (o+o+o)))))) prf | ThreeTwo | Even | Odd | ThreeOne = apply108x63 prf
        unifi (S (S ((S (S (S (o+o+o))+S (S (o+o+o)))+S (S (S (o+o+o))+ S (S (o+o+o))) + (S (S (S (o+o+o))+ S (S (o+o+o)))+S (S (S (o+o+o))+ S (S (o+o+o)))) + (S (S (S (o+o+o))+ S (S (o+o+o)))+S (S (S (o+o+o))+ S (S (o+o+o)))))))) prf | ThreeTwo | Even | Odd | ThreeTwo = apply108x99 prf
    unifi (S (S (S (k+k) + S (k+k) + S (k+k)))) prf | ThreeTwo | Odd with (parity k)
      unifi (S (S (S ((l+l)+(l+l)) + S ((l+l)+(l+l)) + S ((l+l)+(l+l))))) prf | ThreeTwo | Odd | Even with (mod3 l)
        unifi (S (S (S (((o+o+o)+(o+o+o))+((o+o+o)+(o+o+o))) + S (((o+o+o)+(o+o+o))+((o+o+o)+(o+o+o))) + S (((o+o+o)+(o+o+o))+((o+o+o)+(o+o+o)))))) prf | ThreeTwo | Odd | Even | ThreeZero = apply108x18 prf
        unifi (S (S (S ((S (o+o+o)+S (o+o+o))+(S (o+o+o)+S (o+o+o))) + S ((S (o+o+o)+S (o+o+o))+(S (o+o+o)+S (o+o+o))) + S ((S (o+o+o)+S (o+o+o))+(S (o+o+o)+S (o+o+o)))))) prf | ThreeTwo | Odd | Even | ThreeOne = apply108x54 prf
        unifi (S (S (S ((S (S (o+o+o))+S (S (o+o+o)))+(S (S (o+o+o))+S (S (o+o+o)))) + S ((S (S (o+o+o))+S (S (o+o+o)))+(S (S (o+o+o))+S (S (o+o+o)))) + S ((S (S (o+o+o))+S (S (o+o+o)))+(S (S (o+o+o))+S (S (o+o+o))))))) prf | ThreeTwo | Odd | Even | ThreeTwo = apply108x90 prf
      unifi (S (S (S (S (l+l)+ S (l+l)) + S (S (l+l)+S (l+l)) + S (S (l+l)+S (l+l))))) prf | ThreeTwo | Odd | Odd with (mod3 l)
        unifi (S (S (S (S ((o+o+o)+(o+o+o))+ S ((o+o+o)+(o+o+o))) + S (S ((o+o+o)+(o+o+o))+S ((o+o+o)+(o+o+o))) + S (S ((o+o+o)+(o+o+o))+S ((o+o+o)+(o+o+o)))))) prf | ThreeTwo | Odd | Odd | ThreeZero = apply108x36 prf
        unifi (S (S (S (S (S (o+o+o)+S (o+o+o))+ S (S (o+o+o)+S (o+o+o))) + S (S (S (o+o+o)+S (o+o+o))+S (S (o+o+o)+S (o+o+o))) + S (S (S (o+o+o)+S (o+o+o))+S (S (o+o+o)+S (o+o+o)))))) prf | ThreeTwo | Odd | Odd | ThreeOne = apply108x72 prf
        unifi (S (S (S (S (S (S (o+o+o))+S (S (o+o+o)))+ S (S (S (o+o+o))+S (S (o+o+o)))) + S (S (S (S (o+o+o))+S (S (o+o+o)))+S (S (S (o+o+o))+S (S (o+o+o)))) + S (S (S (S (o+o+o))+S (S (o+o+o)))+S (S (S (o+o+o))+S (S (o+o+o))))))) prf | ThreeTwo | Odd | Odd | ThreeTwo = apply108x108 prf

allDivSeqInfFalse' : All Limited (allDivSeq (n+n+n) 2)
allDivSeqInfFalse' = infiniteDescent unifi base0

-- レベルを下げる関数2
lvDown2 : (n, lv:Nat)
  -> All Limited (allDivSeq (n+n+n) lv)
    -> All Limited (allDivSeq (n+n+n) (pred lv))
lvDown2 n Z = id
lvDown2 n (S lv) = rewrite defini (n+n+n) lv in \y =>
  all2 (allDivSeq  (n+n+n) lv)
       (allDivSeqA (n+n+n) lv ++
        allDivSeqB (n+n+n) lv ++
        allDivSeqC (n+n+n) lv ++
        allDivSeqD (n+n+n) lv ++
        allDivSeqE (n+n+n) lv ++
        allDivSeqF (n+n+n) lv ++
        allDivSeqG (n+n+n) lv)
       y

-- 最終的な定理
allDivSeqInfFalse : (n:Nat)
  -> All Limited (allDivSeq (n+n+n) 0)
allDivSeqInfFalse n = lvDown2 n 1 $ lvDown2 n 2 allDivSeqInfFalse'


text:
module Data.Bool.Decidable

import Data.Void

public export
data Reflects : Type -> Bool -> Type where
  RTrue  :     p -> Reflects p True
  RFalse : Not p -> Reflects p False

public export
recompute : Dec a -> (0 x : a) -> a
recompute (Yes x) _ = x
recompute (No contra) x = absurdity $ contra x

public export
invert : {0 b : Bool} -> {0 p : Type} -> Reflects p b -> if b then p else Not p
invert {b = True} (RTrue  x ) = x
invert {b = False} (RFalse nx) = nx

public export
remember : {b : Bool} -> {0 p : Type} -> (if b then p else Not p) -> Reflects p b
remember {b = True } = RTrue
remember {b = False} = RFalse

public export
reflect : {c : Bool} -> Reflects p b -> (if c then p else Not p) -> b = c
reflect {c = True } (RTrue   x)  _ = Refl
reflect {c = True } (RFalse nx)  x = absurd $ nx x
reflect {c = False} (RTrue   x) nx = absurd $ nx x
reflect {c = False} (RFalse nx)  _ = Refl


text:
module Main

import Data.Bytes as B
import Data.ByteArray as BA

-- %flag C "-g3 -ggdb -O0"
%link C "array.o"

initialBuf : Bytes
initialBuf = pack . concat $ replicate 128 block
  where
    block : List Byte
    block = [10,32,1,10,100,32,1,10,255,32,1,10,1,10,255,32,1,10,255,32,1,10,255,32,1,10]

unRLE : Bytes -> Bytes
unRLE = fst . iterateL phi (empty, Nothing)
  where
    phi : (Bytes, Maybe Byte) -> Byte -> Result (Bytes, Maybe Byte)
    phi (bs, Nothing)  b = Cont (bs, Just b)
    phi (bs, Just cnt) b = Cont (bs ++ pack (replicate (cast $ prim__zextB8_Int cnt) b), Nothing)

unit : Int -> Byte -> IO ()
unit n b =
    let expanded = unRLE initialBuf
      in let elines = map (flip snoc b) (asciiLines expanded)
        in printLn $ (show b ++ "/" ++ show n, length expanded, length elines)

alloc : Int -> Int -> IO Int
alloc x 0 = pure x
alloc x i = do
  -- allocate an array
  arr <- BA.allocate (64 * 1024 * 1024)
  -- write "i" at offset 63M
  BA.pokeInt (63*1024*1024) i arr
  -- read number from offset 63M
  j <- BA.peekInt (63*1024*1024) arr
  -- count matches
  alloc (x + if i == j then 1 else 0) (i - 1)

main : IO ()
main = do
    -- First allocate 1024 64M arrays to break the C heap if there's a bug
    alloc 0 1024 >>= printLn

    -- Then, test Bytes
    traverse_ (unit n . prim__truncInt_B8) [1..n]
  where
    n = 8

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
-- Write the signature of a function, typeNamed, that will take the name of a type and return that type. For example, typeNamed "Int" would return the type Int.
-- Implement your typeNamed function for a few different types.
-- Add the keyword total to the beginning of your typeNamed function signature from the Easy section—that is, total typeNamed : .... Reload your file, and see that your function is not total (defined for all inputs). Make your function total by giving it behavior for bad inputs such as "ThisIsNotAType".

total typeNamed : String -> Type
typeNamed "String" = String
typeNamed "Int" = Int
typeNamed _ = String

max_stars_repo_name: hemslo/seven-in-seven

max_issues_repo_name: hemslo/seven-in-seven

max_forks_repo_name: hemslo/seven-in-seven


text:
module InputOutput

main : IO ()
main = do
    putStr "Enter your name: "
    x <- getLine
    putStrLn ("Halo " ++ x ++ "!")

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


text:
-- Code modified from Alex Zhukovsky's one from DepTyp telegram chat (https://t.me/c/1062361327/39965)
-- Code modifiation is mostly a further usage of function extensionality.

record State s a where
 constructor MkState
 runState : s -> (a,s)

funext : {0 f, g : a -> b} -> ((x : a) -> f x = g x) -> f = g
funext = believe_me

injectiveProjections : (0 ab : (a,b)) -> (fst ab, snd ab) = ab
injectiveProjections {ab=(x,y)} = Refl

stateMap : (a -> b) -> (s -> (a, s)) -> s -> (b, s)
stateMap f = (mapFst f .)

stateMapIdIsId : stateMap Prelude.id rs = rs
stateMapIdIsId = funext \x => rewrite sym $ injectiveProjections $ rs x in Refl

Functor (State s) where
 map f (MkState rs) = MkState $ stateMap f rs

interface Functor f => VerifiedFunctor (0 f : Type -> Type) where
  functorIdentity : {0 a : Type} -> map {f} {a} Prelude.id = Prelude.id

VerifiedFunctor (State s) where
  functorIdentity = funext \(MkState _) => cong MkState stateMapIdIsId

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
||| Copyright 2016 Google Inc.
|||
||| Licensed under the Apache License, Version 2.0 (the "License");
||| you may not use this file except in compliance with the License.
||| You may obtain a copy of the License at
|||
|||     http://www.apache.org/licenses/LICENSE-2.0
|||
||| Unless required by applicable law or agreed to in writing, software
||| distributed under the License is distributed on an "AS IS" BASIS,
||| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
||| See the License for the specific language governing permissions and
||| limitations under the License.

module Protobuf.TextFormat

import Data.String

import Lightyear
import Lightyear.Char
import Lightyear.Strings

import Protobuf.Core
import Protobuf.Printer
import Protobuf.ParseUtils
import Protobuf.Util

printEnum : interpEnum d -> Printer ()
printEnum {d=MkEnumDescriptor {k=k} _ values} i = print (name (index i values))

mutual
  printMessage : InterpMessage d -> Printer ()
  printMessage {d=MkMessageDescriptor _ _} (MkMessage fields) =
    printFields fields

  printFields : InterpFields d -> Printer ()
  printFields {d=Nil} Nil = return ()
  printFields {d=f::fs} (x::xs) = do {
    printField x
    printFields xs
  }

  printField : interpField d -> Printer ()
  printField {d=MkFieldDescriptor Optional _ name number} =
    maybe (return ()) (printSingleFieldValue name)
  printField {d=MkFieldDescriptor Required _ name number} =
    (printSingleFieldValue name)
  printField {d=MkFieldDescriptor Repeated _ name number} =
    forEach (printSingleFieldValue name)

  ||| Prints in the form
  ||| <indent>field_name: <contents>\n
  printSingleFieldValue : (name: String) -> interpFieldValue d -> Printer ()
  printSingleFieldValue name x = do {
    printIndent
    print name
    print ": "
    printFieldValue x
    print "\n"
  }

  printFieldValue : interpFieldValue d -> Printer ()
  printFieldValue {d=PBDouble} = print . show
  printFieldValue {d=PBFloat} = print . show
  printFieldValue {d=PBInt32} = print . show
  printFieldValue {d=PBInt64} = print . show
  printFieldValue {d=PBUInt32} = print . show
  printFieldValue {d=PBUInt64} = print . show
  printFieldValue {d=PBSInt32} = print . show
  printFieldValue {d=PBSInt64} = print . show
  printFieldValue {d=PBFixed32} = print . show
  printFieldValue {d=PBFixed64} = print . show
  printFieldValue {d=PBSFixed32} = print . show
  printFieldValue {d=PBSFixed64} = print . show
  printFieldValue {d=PBBool} = print . toLower . show
  printFieldValue {d=PBString} = print . show
  printFieldValue {d=PBBytes} = print . show
  printFieldValue {d=PBMessage _} = braces . printMessage
  printFieldValue {d=PBEnum _} = printEnum

export printToTextFormat : InterpMessage d -> String
printToTextFormat x = assert_total $ runPrinter (printMessage x)

export implementation Show (InterpMessage d) where
  show = printToTextFormat

--- Deserialization

--- Deserialization is implemented using the Lightyear monadic parser package.
--- TODO: commit to more paths to give a better error stack and faster parsing.

-- TODO: handle escape codes including \"
parseString : Parser String
parseString = do {
  char '"'
  chars <- many (satisfy (\c => c /= '"'))
  char '"'
  spaces
  return (pack chars)
}

parseInteger : Parser Integer
parseInteger = do {
  chars <- many (satisfy (\c => c /= '}' && not (isSpace c)))
  spaces
  case parseInteger (pack chars) of
    Nothing => fail $ "Could not parse " ++ (pack chars) ++ " as an integer"
    Just x => return x
}

parseDouble : Parser Double
parseDouble = do {
  chars <- many (satisfy (\c => c /= '}' && not (isSpace c)))
  spaces
  case parseDouble (pack chars) of
    Nothing => fail $ "Could not parse " ++ (pack chars) ++ " as a double"
    Just x => return x
}

parseBool : Parser Bool
parseBool = ((char 't' *!> token "rue" *> return True)
        <|> (char 'f' *!> token "alse" *> return False))
        <?> "A boolean value (\"true\" or \"false\")"

parseEnum : Parser (interpEnum d)
parseEnum {d=MkEnumDescriptor enumName values} = do {
  chars <- many (satisfy isAlpha)
  spaces
  case findIndex (\v => name v == pack chars) values of
    Nothing => fail (
      "An field in the enum " ++ enumName ++ " (no field named " ++
      (show (pack chars)) ++ ")")
    Just i => return i
}

mutual
  parseMessage : Parser (InterpMessage d)
  parseMessage {d=MkMessageDescriptor msgName fields} = do {
    xs <- parseFields msgName
    case messageFromFieldList {fields=fields} xs of
      Left err => fail ("A valid message (" ++ err ++ ")")
      Right fs => return (MkMessage fs)
  }

  parseFields : (msgName : String) -> Parser (FieldList d)
  parseFields {d=d} msgName = many (do {
    chars <- some (satisfy (\c => isDigit c || isAlpha c || c == '_'))
    commitTo (do {
      spaces
      token ":"
      case Data.Vect.findIndex (\v => name v == pack chars) d of
        Nothing => fail (
          "An field in the message " ++ msgName ++ " (no field named " ++
          (show (pack chars)) ++ ")")
        Just i => do {
          v <- parseField
          return (i ** v)
        }
    })
  })

  parseField : Parser (singularTypeForField d)
  parseField {d=MkFieldDescriptor _ ty _ _} = parseFieldValue {d=ty}

  parseFieldValue : Parser (interpFieldValue d)
  parseFieldValue {d=PBDouble} = parseDouble
  parseFieldValue {d=PBFloat} = parseDouble
  parseFieldValue {d=PBInt32} = parseInteger
  parseFieldValue {d=PBInt64} = parseInteger
  parseFieldValue {d=PBUInt32} = parseInteger
  parseFieldValue {d=PBUInt64} = parseInteger
  parseFieldValue {d=PBSInt32} = parseInteger
  parseFieldValue {d=PBSInt64} = parseInteger
  parseFieldValue {d=PBFixed32} = parseInteger
  parseFieldValue {d=PBFixed64} = parseInteger
  parseFieldValue {d=PBSFixed32} = parseInteger
  parseFieldValue {d=PBSFixed64} = parseInteger
  parseFieldValue {d=PBBool} = parseBool
  parseFieldValue {d=PBString} = parseString
  parseFieldValue {d=PBBytes} = parseString
  parseFieldValue {d=PBMessage m} = braces parseMessage
  parseFieldValue {d=PBEnum e} = parseEnum

export parseFromTextFormat : String -> Either String (InterpMessage d)
parseFromTextFormat {d=d} = assert_total $ parse (spaces *> parseMessage {d=d})

max_stars_repo_name: google/idris-protobuf

max_issues_repo_name: google/idris-protobuf

max_forks_repo_name: google/idris-protobuf


text:
module Flexidisc.Header.Label

import Flexidisc.Header.Type
import Flexidisc.OrdList

%default total
%access public export

||| Proof that a label is in an `Header'`
data Label : (l : k) -> (xs : Header' k a) -> Type where
  ||| A wrapper for an `OrdLabel`
  L : {xs : OrdList k o a} -> OrdLabel l xs -> Label l (H xs)

%name Label lbl, loc, prf, e, elem

||| Decide whether a label is in a list or not
decLabel : DecEq k => (l : k) -> (xs : Header' k a) -> Dec (Label l xs)
decLabel l (H xs) with (decLabel l xs)
  | (Yes prf) = Yes (L prf)
  | (No contra) = No (\(L p) => contra p)

||| Given a proof that a label is in the list, get the corresponding value back
atLabel : (xs : Header' l a) -> (loc : Label k xs) -> a
atLabel (H xs) (L loc) = atLabel xs loc

||| Given a proof that an element is in a vector, remove it
dropLabel : (xs : Header' k a) -> (loc : Label l xs) -> Header' k a
dropLabel (H xs) (L loc) = H (dropLabel xs loc)

||| Update a value in the `Header'` given it's location and a new value
changeType : (xs : Header' k a) -> (loc : Label l xs) -> (new : a) ->
             Header' k a
changeType (H xs) (L loc) = H . changeValue xs loc


text:
module Control.App

import Data.IORef

public export
Error : Type
Error = Type

public export
Environment : Type
Environment = List Error

public export
data HasErr : Error -> List Error -> Type where
     Here : HasErr e (e :: es)
     There : HasErr e es -> HasErr e (e' :: es)

public export
data Path : Type where
     [noHints]
     MayThrow : Path
     NoThrow : Path

%hint public export
dpath : Path
dpath = MayThrow

public export
data Usage : Type where
     [noHints]
     One : Usage
     Any : Usage

%hint public export
dusage : Usage
dusage = One

public export
0 Has : List (a -> Type) -> a -> Type
Has [] es = ()
Has [e] es = e es
Has (e :: es') es = (e es, Has es' es)

public export
0 excTy : List Error -> List Type
excTy [] = []
excTy (e :: es) = e :: excTy es

data OneOf : List Type -> Path -> Type where
     First : e -> OneOf (e :: es) MayThrow
     Later : OneOf es MayThrow -> OneOf (e :: es) MayThrow

public export
data SafeBind : Path -> (l' : Path) -> Type where
     [search l']
     SafeSame : SafeBind l l
     SafeToThrow : SafeBind NoThrow MayThrow

updateP : SafeBind p p' => OneOf es p -> OneOf es p'
updateP @{SafeSame} x = x
updateP @{SafeToThrow} x impossible

Uninhabited (OneOf [] p) where
  uninhabited (First x) impossible
  uninhabited (Later x) impossible

Uninhabited (OneOf es NoThrow) where
  uninhabited (First x) impossible
  uninhabited (Later x) impossible

0 execTy : Path -> List Error -> Type -> Type
execTy p es ty = Either (OneOf (excTy es) p) ty

data AppRes : Type -> Type where
     MkAppRes : (result : a) -> (1 x : %World) -> AppRes a

data App1Res : Usage -> Type -> Type where
     MkApp1Res1 : (1 result : a) -> (1 x : %World) -> App1Res One a
     MkApp1ResW : (result : a) -> (1 x : %World) -> App1Res Any a

PrimApp : Type -> Type
PrimApp a = (1 x : %World) -> AppRes a

prim_app_pure : a -> PrimApp a
prim_app_pure x = \w => MkAppRes x w

prim_app_bind : (1 act : PrimApp a) -> (1 k : a -> PrimApp b) -> PrimApp b
prim_app_bind fn k w
    = let MkAppRes x' w' = fn w in k x' w'

toPrimApp : IO a -> PrimApp a
toPrimApp x
    = \w => case toPrim x w of
                 MkIORes r w => MkAppRes r w

PrimApp1 : Usage -> Type -> Type
PrimApp1 u a = (1 x : %World) -> App1Res u a

toPrimApp1 : {u : _} -> IO a -> PrimApp1 u a
toPrimApp1 x
    = \w => case toPrim x w of
                 MkIORes r w =>
                     case u of
                          One => MkApp1Res1 r w
                          Any => MkApp1ResW r w

export
data App : (l : Path) => (e : Environment) -> Type -> Type where
     MkApp : (1 prog : (1 w : %World) -> AppRes (execTy l e t)) -> App {l} e t

export
data App1 : (u : Usage) => (e : Environment) -> Type -> Type where
     MkApp1 : (1 prog : (1 w : %World) -> App1Res u t) -> App1 {u} e t

bindApp : SafeBind l l' =>
          App {l} e a -> (a -> App {l=l'} e b) -> App {l=l'} e b
bindApp (MkApp prog) next
    = MkApp $ \world =>
          let MkAppRes x' world' = prog world in
              case x' of
                   Right res =>
                         let MkApp r = next res in
                             r world'
                   Left err => MkAppRes (Left (updateP err)) world'

public export
Cont1Type : Usage -> Type -> Usage -> List Error -> Type -> Type
Cont1Type One a u e b = (1 x : a) -> App1 {u} e b
Cont1Type Any a u e b = (x : a) -> App1 {u} e b

export
bindApp1 : {u : _} -> (1 act : App1 {u} e a) ->
           (1 k : Cont1Type u a u' e b) -> App1 {u=u'} e b
bindApp1 {u=One} (MkApp1 fn)
    = \k => MkApp1 (\w => let MkApp1Res1 x' w' = fn w
                              MkApp1 res = k x' in
                              res w')
bindApp1 {u=Any} (MkApp1 fn)
    = \k => MkApp1 (\w => let MkApp1ResW x' w' = fn w
                              MkApp1 res = k x' in
                              res w')

absurdWith1 : (1 w : b) -> OneOf e NoThrow -> any
absurdWith1 w (First p) impossible

absurdWith2 : (1 x : a) -> (1 w : b) -> OneOf e NoThrow -> any
absurdWith2 x w (First p) impossible

export
bindL : App {l=NoThrow} e a -> (1 k : a -> App {l} e b) -> App {l} e b
bindL (MkApp prog) next
    = MkApp $ \world =>
          let MkAppRes x' world' = prog world in
              case x' of
                   Right res =>
                         let MkApp r = next res in
                             r world'
                   Left err => absurdWith2 next world' err

export
app : (1 p : App {l=NoThrow} e a) -> App1 {u=Any} e a
app (MkApp prog)
    = MkApp1 $ \world =>
          let MkAppRes x' world' = prog world in
              case x' of
                   Left err => absurdWith1 world' err
                   Right res => MkApp1ResW res world'

export
app1 : (1 p : App1 {u=Any} e a) -> App {l} e a
app1 (MkApp1 prog)
    = MkApp $ \world =>
          let MkApp1ResW x' world' = prog world in
              MkAppRes (Right x') world'

pureApp : a -> App {l} e a
pureApp x = MkApp $ \w => MkAppRes (Right x) w

export
Functor (App {l} es) where
  map f ap = bindApp ap $ \ap' => pureApp (f ap')

export
Applicative (App {l} es) where
  pure = pureApp
  (<*>) f a = bindApp f $ \f' =>
              bindApp a $ \a' => pure (f' a')

export
Monad (App es) where
  (>>=) = bindApp -- won't get used, but handy to have the instance

export
(>>=) : SafeBind l l' =>
        App {l} e a -> (k : a -> App {l=l'} e b) -> App {l=l'} e b
(>>=) = bindApp

namespace App1
  export
  (>>=) : {u : _} -> (1 act : App1 {u} e a) ->
          (1 k : Cont1Type u a u' e b) -> App1 {u=u'} e b
  (>>=) = bindApp1

  export
  pure : (x : a) -> App1 {u=Any} e a
  pure x =  MkApp1 $ \w => MkApp1ResW x w

  export
  pure1 : (1 x : a) -> App1 e a
  pure1 x =  MkApp1 $ \w => MkApp1Res1 x w

export
data State : (tag : a) -> Type -> List Error -> Type where
     [search tag]
     MkState : IORef t -> State tag t e

%hint export
mapState : State tag t e -> State tag t (eff :: e)
mapState (MkState s) = MkState s

export
get : (0 tag : _) -> State tag t e => App {l} e t
get tag @{MkState r}
    = MkApp $
          prim_app_bind (toPrimApp $ readIORef r) $ \val =>
          MkAppRes (Right val)

export
put : (0 tag : _) -> State tag t e => t -> App {l} e ()
put tag @{MkState r} val
    = MkApp $
          prim_app_bind (toPrimApp $ writeIORef r val) $ \val =>
          MkAppRes (Right ())

export
modify : (0 tag : _) -> State tag t e => (t -> t) -> App {l} e ()
modify tag f
    = do x <- get tag
         put tag (f x)

export
new : t -> (State tag t e => App {l} e a) -> App {l} e a
new val prog
    = MkApp $
         prim_app_bind (toPrimApp $ newIORef val) $ \ref =>
            let st = MkState ref
                MkApp res = prog @{st} in
                res

public export
interface Exception err e where
  throw : err -> App e a
  catch : App e a -> (err -> App e a) -> App e a

findException : HasErr e es -> e -> OneOf (excTy es) MayThrow
findException Here err = First err
findException (There p) err = Later $ findException p err

findError : HasErr e es -> OneOf (excTy es) MayThrow -> Maybe e
findError Here (First err) = Just err
findError (There p) (Later q) = findError p q
findError _ _ = Nothing

export
HasErr e es => Exception e es where
  throw err = MkApp $ MkAppRes (Left (findException %search err))
  catch (MkApp prog) handler
      = MkApp $
           prim_app_bind prog $ \res =>
              case res of
                   Left err =>
                        case findError %search err of
                             Nothing => MkAppRes (Left err)
                             Just err' =>
                                  let MkApp e' = handler err' in
                                      e'
                   Right ok => MkAppRes (Right ok)

export
handle : App (err :: e) a ->
         (onok : a -> App e b) ->
         (onerr : err -> App e b) -> App e b
handle (MkApp prog) onok onerr
    = MkApp $
           prim_app_bind prog $ \res =>
             case res of
                  Left (First err) =>
                        let MkApp err' = onerr err in
                            err'
                  Left (Later p) =>
                        -- different exception, so rethrow
                        MkAppRes (Left p)
                  Right ok =>
                        let MkApp ok' = onok ok in
                            ok'

export
lift : App e a -> App (err :: e) a
lift (MkApp prog)
    = MkApp $
           prim_app_bind prog $ \res =>
            case res of
                 Left err => MkAppRes (Left (Later err))
                 Right ok => MkAppRes (Right ok)

public export
Init : List Error
Init = [Void]

export
run : App {l} Init a -> IO a
run (MkApp prog)
    = primIO $ \w =>
           case (prim_app_bind prog $ \r =>
                   case r of
                        Right res => MkAppRes res
                        Left (First err) => absurd err) w of
                MkAppRes r w => MkIORes r w

public export
interface PrimIO e where
  primIO : IO a -> App {l} e a
  -- fork starts a new environment, so that any existing state can't get
  -- passed to it (since it'll be tagged with the wrong environment)
  fork : (forall e' . PrimIO e' => App {l} e' ()) -> App e ()

export
HasErr Void e => PrimIO e where
  primIO op =
        MkApp $ \w =>
            let MkAppRes r w = toPrimApp op w in
                MkAppRes (Right r) w
  fork thread
      = MkApp $
            prim_app_bind
                (toPrimApp $ Prelude.fork $
                      do run thread
                         pure ())
                    $ \_ =>
               MkAppRes (Right ())

public export
data FileEx = GenericFileEx Int -- errno
            | FileReadError
            | FileWriteError
            | FileNotFound
            | PermissionDenied
            | FileExists

export
Show FileEx where
  show (GenericFileEx errno) = "File error: " ++ show errno
  show FileReadError = "File Read Error"
  show FileWriteError = "File Write Error"
  show FileNotFound = "File Not Found"
  show PermissionDenied = "Permission Denied"
  show FileExists = "File Exists"

public export
data IOError
     = GenericErr String
     | FileErr FileEx

export
Show IOError where
  show (GenericErr str) = "IO error: " ++ str
  show (FileErr f) = "File error: " ++ show f


text:
module System.Random.SplitMix32

import System.Random
import Data.IORef

||| Generator for splitmix PRNG
export
data SMGen
    = MkGen
        Bits32 -- seed
        Bits32 -- gamma (odd)

||| Create a SMGen with specific seed and gamma (gamma is forced to be odd)
export
makeSMGen : Int -> Int -> SMGen
makeSMGen seed gamma = MkGen (cast seed) (cast gamma `prim__or_Bits32` 1)

{-
================
Helper Functions
================
-}

succBits32 : Bits32 -> Bits32
succBits32 x = if x == 0xffffffff
    then x
    else x + 1

neg : Bits32 -> Bits32
neg x = cast $ the Int 0x100000000 - cast x

xor : Bits32 -> Bits32 -> Bits32
xor = prim__xor_Bits32

and : Bits32 -> Bits32 -> Bits32
and = prim__and_Bits32

shiftR : Bits32 -> Bits32 -> Bits32
shiftR = prim__shr_Bits32

m1 : Bits32
m1 = 0x55555555

m2 : Bits32
m2 = 0x33333333

m4 : Bits32
m4 = 0x0f0f0f0f

popCount : Bits32 -> Bits32
popCount x0 = -- feel free to add this as a primitive
    let x1 = (x0 `shiftR` 1) `and` m1
        x2 = (x1 `and` m2) + ((x1 `shiftR` 2) `and` m2)
        x3 = (x2 + (x2 `shiftR` 4)) `and` m4
        x4 = x3 + (x3 `shiftR` 8)
        x5 = x4 + (x4 `shiftR` 16)
        x6 = x5 + (x5 `shiftR` 32)
    in x6 `and` 0x7f

shiftXor : Bits32 -> Bits32 -> Bits32
shiftXor n w = w `xor` (w `shiftR` n)

shiftXorMult : Bits32 -> Bits32 -> Bits32 -> Bits32
shiftXorMult n k w = shiftXor n w * k

mix32 : Bits32 -> Bits32
mix32 z0 =
    let z1 = shiftXorMult 16 0x85ebca6b z0
        z2 = shiftXorMult 13 0xc2b2ae35 z1
        z3 = shiftXor 16 z2
    in z3

mix32variant13 : Bits32 -> Bits32
mix32variant13 z0 =
    let z1 = shiftXorMult 16 0x69ad6ccb z0
        z2 = shiftXorMult 13 0xcd9ab5b3 z1
        z3 = shiftXor 16 z2
    in z3

mixGamma : Bits32 -> Bits32
mixGamma z0 =
    let z1 = mix32variant13 z0 `xor` 1
        n = popCount (z1 `xor` (z1 `shiftR` 1))
    in if n >= 12
        then z1
        else z1 `xor` 0xaaaaaaaa

{-
==========
Operations
==========
-}

||| Return the next Bits32 and the updated SMGen
export
nextBits32 : SMGen -> (Bits32, SMGen)
nextBits32 (MkGen seed gamma) = (mix32 seed', MkGen seed' gamma)
  where
    seed' : Bits32
    seed' = seed + gamma

||| Return the next Bits32 in range (lo, hi) inclusive and the updated SMGen
export
nextBits32Range : (Bits32, Bits32) -> SMGen -> (Bits32, SMGen)
nextBits32Range (lo, hi) = mapFst (+ lo) . nextBits32R (succBits32 $ cast $ the Int (cast hi - cast lo))
  where
    nextBits32R : Bits32 -> SMGen -> (Bits32, SMGen)
    nextBits32R 0 gen0 = (0, snd (nextBits32 gen0))
    nextBits32R range gen0 =
        let t = assert_total prim__mod_Bits32 (neg range) range
            go : Bits64 -> SMGen -> (Bits32, SMGen)
            go m gen = if (the Bits32 $ cast m) < t
                then (the Bits32 $ cast $ m `prim__shr_Bits64` 32, gen)
                else
                    let (x, gen') = nextBits32 gen
                        m' = the Bits64 $ cast x * cast range
                    in go m' gen'
            xgen : (Bits32, SMGen)
            xgen = nextBits32 gen0
        in go (cast $ fst xgen) (snd xgen)

||| Return the next Bits64 and the updated SMGen
export
nextBits64 : SMGen -> (Bits64, SMGen)
nextBits64 gen0 =
    let (bottom, gen1) = nextBits32 gen0
        (top, gen2) = nextBits32 gen1
    in (cast top `prim__shl_Bits64` 32 + cast bottom, gen2)

||| Return the next Int and the updated SMGen
export
nextInt : SMGen -> (Int, SMGen)
nextInt gen =
    let (bits64, gen') = nextBits64 gen
    in (if bits64 >= 0x7fffffffffffffff
        then negate $ cast $ bits64 + 0x7fffffffffffffff
        else cast bits64
        , gen')

{-
=========
Splitting
=========
-}

||| Return an unrelated SMGen and the updated SMGen
export
splitSMGen : SMGen -> (SMGen, SMGen)
splitSMGen (MkGen seed gamma) =
    (MkGen seed'' gamma, MkGen (mix32 seed') (mixGamma seed''))
  where
    seed' : Bits32
    seed' = seed + gamma
    seed'' : Bits32
    seed'' = seed + gamma

{-
==========
Generation
==========
-}

||| Deterministically create a new SMGen from a seed
export
mkSMGen : Bits32 -> SMGen
mkSMGen seed = MkGen (mix32 seed) goldenGamma -- different from haskell version
  where
    goldenGamma : Bits32
    goldenGamma = 0x9e3779b9

theSMGen : IORef SMGen
theSMGen = unsafePerformIO $ do
    init <- cast <$> randomRIO (the Int 0, 0xffffffff)
    newIORef (mkSMGen init)

||| Randomly create an SMGen
export
newSMGen : HasIO io => io SMGen
newSMGen = do
    (newThe, new) <- splitSMGen <$> readIORef theSMGen
    writeIORef theSMGen newThe
    pure new


text:
module Derive.Prim

import public Derive.Common
%language ElabReflection

-- Derivations for common prim creation needs Use of this module automatically
-- imports Language.Reflection and requires %language ElabReflection to be
-- enabled below your imports.
-- Examples at module bottom

{-
   makeHasIO "what" Private ["c:foo","javascript:borp"]
                          `[ prim_gob : Int -> Int -> PrimIO Int ]
   This generates:
   %foreign "c:foo" "javascript:borp"
   prim_gob : Int -> Int -> PrimIO Int
   And:
   private
   what : HasIO io => Int -> Int -> io Int
   what x y = primIO $ prim_gob x y
   This is not as useful as is it looks since often you'll be wanting to supply
   specific arguments to your `prim_gob` or pattern match on `what`'s arguments,
   this doesn't do that and is a direct translation/application.
   Still it can alleviate some of the write-twice burden PrimIO can introduce.
-}
export
makeHasIO : String -> Visibility -> List Decl -> Elab ()
makeHasIO funname0 vis ys = do
    [pclaim@(IClaim pfc pmw pvis _ pty@(MkTy tyfc namefc primname primty))] <- pure ys
      | _ => fail "bad format"
    let funty = IPi eFC MW AutoImplicit Nothing
               `(HasIO ~(IBindVar eFC "io"))
               (spiderType primty)
        funname = UN funname0
        funclaim = IClaim eFC pmw vis [] (MkTy tyfc namefc funname funty)
        varnames = map (("var" ++) . show) [0..]
        lvars = IBindVar eFC <$> take (argCount primty) varnames
        rvars = toIVar . UN <$> take (argCount primty) varnames
        lhs = foldl (\xs,x => `(~xs ~x)) (toIVar funname) lvars
        rhs = `(primIO ~(foldl (\xs,x => `(~xs ~x)) (toIVar primname) rvars))
        patclause = PatClause eFC lhs rhs
        funbody = IDef eFC funname [patclause]
    declare [pclaim] -- declare the primitive as-given
    declare [funclaim, funbody] -- declare our HasIO version
    pure ()
  where
    spiderType : TTImp -> TTImp -- replace 'PrimIO' with 'io'
    spiderType (IPi a b c d e retty) = IPi a b c d e (spiderType retty)
    spiderType (IApp _ `(PrimIO) retty) = `(~(toIBindVar "io") ~retty)
    spiderType ty = ty

%runElab makeHasIO "what" Private
  `[ %foreign "C:div,libc,math.h"
     private
     prim_gob : Int -> Int -> PrimIO Int ] --`

gob_exists : PrimIO Int
gob_exists = prim_gob 1 2

what_exists : HasIO io => io Int
what_exists = what 1 2


text:
module Data.Nat.Factor

import Control.WellFounded
import Data.Fin
import Data.Fin.Extra
import Data.Nat
import Data.Nat.Equational
import Syntax.PreorderReasoning

%default total

||| Factor n p is a witness that p is indeed a factor of n,
||| i.e. there exists a q such that p * q = n.
public export
data Factor : Nat -> Nat -> Type where
    CofactorExists : {p, n : Nat} -> (q : Nat) -> n = p * q -> Factor p n

||| NotFactor n p is a witness that p is NOT a factor of n,
||| i.e. there exist a q and an r, greater than 0 but smaller than p,
||| such that p * q + r = n.
public export
data NotFactor : Nat -> Nat -> Type where
    ZeroNotFactorS : (n : Nat) -> NotFactor Z (S n)
    ProperRemExists : {p, n : Nat} -> (q : Nat) ->
        (r : Fin (pred p)) ->
        n = p * q + S (finToNat r) ->
        NotFactor p n

||| DecFactor n p is a result of the process which decides
||| whether or not p is a factor on n.
public export
data DecFactor : Nat -> Nat -> Type where
    ItIsFactor : Factor p n -> DecFactor p n
    ItIsNotFactor : NotFactor p n -> DecFactor p n

||| CommonFactor n m p is a witness that p is a factor of both n and m.
public export
data CommonFactor : Nat -> Nat -> Nat -> Type where
    CommonFactorExists : {a, b : Nat} -> (p : Nat) -> Factor p a -> Factor p b -> CommonFactor p a b

||| GCD n m p is a witness that p is THE greatest common factor of both n and m.
||| The second argument to the constructor is a function which for all q being
||| a factor of both n and m, proves that q is a factor of p.
|||
||| This is equivalent to a more straightforward definition, stating that for
||| all q being a factor of both n and m, q is less than or equal to p, but more
||| powerful and therefore more useful for further proofs. See below for a proof
||| that if q is a factor of p then q must be less than or equal to p.
public export
data GCD : Nat -> Nat -> Nat -> Type where
    MkGCD : {a, b, p : Nat} ->
        {auto notBothZero : NotBothZero a b} ->
        (CommonFactor p a b) ->
        ((q : Nat) -> CommonFactor q a b -> Factor q p) ->
        GCD p a b

Uninhabited (Factor Z (S n)) where
    uninhabited (CofactorExists q prf) = uninhabited prf

||| Given a statement that p is factor of n, return its cofactor.
export
cofactor : Factor p n -> (q : Nat ** Factor q n)
cofactor (CofactorExists q prf) =
        (q ** CofactorExists p $ rewrite multCommutative q p in prf)

||| 1 is a factor of any natural number.
export
oneIsFactor : (n : Nat) -> Factor 1 n
oneIsFactor Z = CofactorExists Z Refl
oneIsFactor (S k) = CofactorExists (S k) (rewrite plusZeroRightNeutral k in Refl)

||| 1 is the only factor of itself
export
oneSoleFactorOfOne : (a : Nat) -> Factor a 1 -> a = 1
oneSoleFactorOfOne 0 (CofactorExists _ prf) = sym prf
oneSoleFactorOfOne 1 _ = Refl
oneSoleFactorOfOne (S (S k)) (CofactorExists Z prf) =
  absurd . uninhabited $ trans prf $ multCommutative k 0
oneSoleFactorOfOne (S (S k)) (CofactorExists (S j) prf) =
  absurd . uninhabited $
    trans
      (succInjective 0 (j + S (j + (k * S j))) prf)
      (plusCommutative j (S (j + (k * S j))))

||| Every natural number is factor of itself.
export
Reflexive Nat Factor where
  reflexive = CofactorExists 1 $ rewrite multOneRightNeutral x in Refl

||| Factor relation is transitive. If b is factor of a and c is b factor of c
||| is also a factor of a.
export
Transitive Nat Factor where
  transitive (CofactorExists qb prfAB) (CofactorExists qc prfBC) =
    CofactorExists (qb * qc) $
        rewrite prfBC in
        rewrite prfAB in
        rewrite multAssociative x qb qc in
        Refl

export
Preorder Nat Factor where

multOneSoleNeutral : (a, b : Nat) -> S a = S a * b -> b = 1
multOneSoleNeutral Z b prf =
        rewrite sym $ plusZeroRightNeutral b in
        sym prf
multOneSoleNeutral (S k) Z prf =
        absurd . uninhabited $ trans prf $ multCommutative k 0
multOneSoleNeutral (S k) (S Z) prf = Refl
multOneSoleNeutral (S k) (S (S j)) prf =
        absurd . uninhabited .
        subtractEqLeft k {c = S j + S (j + (k * S j))} $
        rewrite plusSuccRightSucc j (S (j + (k * S j))) in
        rewrite plusZeroRightNeutral k in
        rewrite plusAssociative k j (S (S (j + (k * S j)))) in
        rewrite sym $ plusCommutative j k in
        rewrite sym $ plusAssociative j k (S (S (j + (k * S j)))) in
        rewrite sym $ plusSuccRightSucc k (S (j + (k * S j))) in
        rewrite sym $ plusSuccRightSucc k (j + (k * S j)) in
        rewrite plusAssociative k j (k * S j) in
        rewrite plusCommutative k j in
        rewrite sym $ plusAssociative j k (k * S j) in
        rewrite sym $ multRightSuccPlus k (S j) in
        succInjective k (j + (S (S (j + (k * (S (S j))))))) $
        succInjective (S k) (S (j + (S (S (j + (k * (S (S j)))))))) prf

||| If a is a factor of b and b is a factor of a, then a = b.
public export
Antisymmetric Nat Factor where
  antisymmetric {x = Z} (CofactorExists _ prfAB) _ = sym prfAB
  antisymmetric {y = Z} _ (CofactorExists _ prfBA) = prfBA
  antisymmetric {x = S a} {y = S _} (CofactorExists qa prfAB) (CofactorExists qb prfBA) =
      let qIs1 = multOneSoleNeutral a (qa * qb) $
              rewrite multAssociative (S a) qa qb in
              rewrite sym prfAB in
              prfBA
      in
      rewrite prfAB in
      rewrite oneSoleFactorOfOne qa . CofactorExists qb $ sym qIs1 in
      rewrite multOneRightNeutral a in
      Refl

PartialOrder Nat Factor where

||| No number can simultaneously be and not be a factor of another number.
export
factorNotFactorAbsurd : Factor p n -> Not (NotFactor p n)
factorNotFactorAbsurd (CofactorExists _ prf) (ZeroNotFactorS _) =
        uninhabited prf
factorNotFactorAbsurd (CofactorExists q prf) (ProperRemExists q' r contra) with (cmp q q')
    factorNotFactorAbsurd (CofactorExists q prf) (ProperRemExists (q + S d) r contra) | CmpLT d =
        SIsNotZ .
        subtractEqLeft (p * q) {b = S ((p * S d) + finToNat r)} $
        rewrite plusZeroRightNeutral (p * q) in
        rewrite plusSuccRightSucc (p * S d) (finToNat r) in
        rewrite plusAssociative (p * q) (p * S d) (S (finToNat r)) in
        rewrite sym $ multDistributesOverPlusRight p q (S d) in
        rewrite sym contra in
        rewrite sym prf in
        Refl
    factorNotFactorAbsurd (CofactorExists q prf) (ProperRemExists q r contra) | CmpEQ =
      SIsNotZ $ sym $
        plusLeftCancel (p * q) 0 (S (finToNat r)) $
          trans (plusZeroRightNeutral (p * q)) $
            trans (sym prf) contra
    factorNotFactorAbsurd (CofactorExists (q + S d) prf) (ProperRemExists q r contra) | CmpGT d =
        let srEQpPlusPD = the (p + (p * d) = S (finToNat r)) $
                rewrite sym $ multRightSuccPlus p d in
                subtractEqLeft (p * q) $
                    rewrite sym $ multDistributesOverPlusRight p q (S d) in
                    rewrite sym contra in
                    sym prf
        in
        case p of
            Z => uninhabited srEQpPlusPD
            (S k) =>
                succNotLTEzero .
                subtractLteLeft k {b = S (d + (k * d))} $
                rewrite sym $ plusSuccRightSucc k (d + (k * d)) in
                rewrite plusZeroRightNeutral k in
                rewrite srEQpPlusPD in
                elemSmallerThanBound r

||| Anything is a factor of 0.
export
anythingFactorZero : (a : Nat) -> Factor a 0
anythingFactorZero a = CofactorExists 0 (sym $ multZeroRightZero a)

||| For all natural numbers p and q, p is a factor of (p * q).
export
multFactor : (p, q : Nat) -> Factor p (p * q)
multFactor p q = CofactorExists q Refl

||| If n > 0 then any factor of n must be less than or equal to n.
export
factorLteNumber : Factor p n -> {auto positN : LTE 1 n} -> LTE p n
factorLteNumber (CofactorExists Z prf) =
        let nIsZero = trans prf $ multCommutative p 0
            oneLteZero = replace {p = LTE 1} nIsZero positN
        in
        absurd $ succNotLTEzero oneLteZero
factorLteNumber (CofactorExists (S k) prf) =
        rewrite prf in
        leftFactorLteProduct p k

||| If p is a factor of n, then it is also a factor of (n + p).
export
plusDivisorAlsoFactor : Factor p n -> Factor p (n + p)
plusDivisorAlsoFactor (CofactorExists q prf) =
        CofactorExists (S q) $
            rewrite plusCommutative n p in
            rewrite multRightSuccPlus p q in
            cong (plus p) prf

||| If p is NOT a factor of n, then it also is NOT a factor of (n + p).
export
plusDivisorNeitherFactor : NotFactor p n -> NotFactor p (n + p)
plusDivisorNeitherFactor (ZeroNotFactorS k) =
        rewrite plusZeroRightNeutral k in
        ZeroNotFactorS k
plusDivisorNeitherFactor (ProperRemExists q r remPrf) =
        ProperRemExists (S q) r $
            rewrite multRightSuccPlus p q in
            rewrite sym $ plusAssociative p (p * q) (S $ finToNat r) in
            rewrite plusCommutative p ((p * q) + S (finToNat r)) in
            rewrite remPrf in
            Refl

||| If p is a factor of n, then it is also a factor of any multiply of n.
export
multNAlsoFactor : Factor p n -> (a : Nat) -> {auto aok : LTE 1 a} -> Factor p (n * a)
multNAlsoFactor _ Z = absurd $ succNotLTEzero aok
multNAlsoFactor (CofactorExists q prf) (S a) =
        CofactorExists (q * S a) $
            rewrite prf in
            sym $ multAssociative p q (S a)

||| If p is a factor of both n and m, then it is also a factor of their sum.
export
plusFactor : Factor p n -> Factor p m -> Factor p (n + m)
plusFactor (CofactorExists qn prfN) (CofactorExists qm prfM) =
        rewrite prfN in
        rewrite prfM in
        rewrite sym $ multDistributesOverPlusRight p qn qm in
        multFactor p (qn + qm)

||| If p is a factor of a sum (n + m) and a factor of n, then it is also
||| a factor of m. This could be expressed more naturally with minus, but
||| it would be more difficult to prove, since minus lacks certain properties
||| that one would expect from decent subtraction.
export
minusFactor : {b : Nat} -> Factor p (a + b) -> Factor p a -> Factor p b
minusFactor (CofactorExists qab prfAB) (CofactorExists qa prfA) =
        CofactorExists (minus qab qa) $
            rewrite multDistributesOverMinusRight p qab qa in
            rewrite sym prfA in
            rewrite sym prfAB in
            replace {p = \x => b = minus (a + b) x} (plusZeroRightNeutral a) $
            rewrite plusMinusLeftCancel a b 0 in
            rewrite minusZeroRight b in
            Refl

||| A decision procedure for whether of not p is a factor of n.
export
decFactor : (n, d : Nat) -> DecFactor d n
decFactor Z Z = ItIsFactor $ reflexive {x = Z}
decFactor (S k) Z = ItIsNotFactor $ ZeroNotFactorS k
decFactor n (S d) =
        let Fraction n (S d) q r prf = Data.Fin.Extra.divMod n (S d) in
        case r of
            FZ =>
              ItIsFactor $ CofactorExists q $
                rewrite sym prf in
                  rewrite plusCommutative (q * (S d)) 0 in
                    multCommutative q (S d)

            (FS pr) =>
                ItIsNotFactor $ ProperRemExists q pr (
                        rewrite multCommutative d q in
                        rewrite sym $ multRightSuccPlus q d in
                        sym prf
                    )

||| For all p greater than 1, if p is a factor of n, then it is NOT a factor
||| of (n + 1).
export
factNotSuccFact : {p : Nat} -> GT p 1 -> Factor p n -> NotFactor p (S n)
factNotSuccFact {p = Z} pGt1 (CofactorExists q prf) =
        absurd $ succNotLTEzero pGt1
factNotSuccFact {p = S Z} pGt1 (CofactorExists q prf) =
        absurd . succNotLTEzero $ fromLteSucc pGt1
factNotSuccFact {p = S (S k)} pGt1 (CofactorExists q prf) =
        ProperRemExists q FZ (
            rewrite sym prf in
            rewrite plusCommutative n 1 in
            Refl
        )

using (p : Nat)
  ||| The relation of common factor is symmetric, that is if p is a
  ||| common factor of n and m, then it is also a common factor of
  ||| m and n.
  public export
  Symmetric Nat (CommonFactor p) where
    symmetric (CommonFactorExists p pfx pfy) = CommonFactorExists p pfy pfx

  ||| The relation of greatest common divisor is symmetric.
  public export
  Symmetric Nat (GCD p) where
    symmetric {x = Z} {y = Z} (MkGCD _ _) impossible
    symmetric {x = S _} (MkGCD cf greatest) =
            MkGCD (symmetric {ty = Nat} cf) $
            \q, cf => greatest q (symmetric {ty = Nat} cf)
    symmetric {y = S _} (MkGCD cf greatest) =
            MkGCD (symmetric {ty = Nat} cf) $
            \q, cf => greatest q (symmetric {ty = Nat} cf)

||| If p is a common factor of a and b, then it is also a factor of their GCD.
||| This actually follows directly from the definition of GCD.
export
commonFactorAlsoFactorOfGCD : {p : Nat} -> Factor p a -> Factor p b -> GCD q a b -> Factor p q
commonFactorAlsoFactorOfGCD pfa pfb (MkGCD _ greatest) =
        greatest p (CommonFactorExists p pfa pfb)

||| 1 is a common factor of any pair of natural numbers.
export
oneCommonFactor : (a, b : Nat) -> CommonFactor 1 a b
oneCommonFactor a b = CommonFactorExists 1
        (CofactorExists a (rewrite plusZeroRightNeutral a in Refl))
        (CofactorExists b (rewrite plusZeroRightNeutral b in Refl))

||| Any natural number is a common factor of itself and itself.
export
selfIsCommonFactor : (a : Nat) -> {auto ok : LTE 1 a} -> CommonFactor a a a
selfIsCommonFactor a =
  let prf = reflexive {x = a} in
    CommonFactorExists a prf prf

-- Some helpers for the gcd function.
data Search : Type where
    SearchArgs : (a, b : Nat) -> LTE b a -> {auto bNonZero : LTE 1 b} -> Search

left : Search -> Nat
left (SearchArgs l _ _) = l

right : Search -> Nat
right (SearchArgs _ r _) = r

Sized Search where
    size (SearchArgs a b _) = a + b

notLteAndGt : (a, b : Nat) -> LTE a b -> Not (GT a b)
notLteAndGt Z _ _ aGtB = succNotLTEzero aGtB
notLteAndGt (S _) Z aLteB _ = succNotLTEzero aLteB
notLteAndGt (S k) (S j) aLteB aGtB = notLteAndGt k j (fromLteSucc aLteB) (fromLteSucc aGtB)

gcd_step : (x : Search) ->
           (rec : (y : Search) -> Smaller y x ->
                  (f : Nat ** GCD f (left y) (right y))) ->
           (f : Nat ** GCD f (left x) (right x))
gcd_step (SearchArgs Z _ bLteA {bNonZero}) _ = absurd . succNotLTEzero $ transitive {ty = Nat} bNonZero bLteA
gcd_step (SearchArgs _ Z _ {bNonZero}) _ = absurd $ succNotLTEzero bNonZero
gcd_step (SearchArgs (S a) (S b) bLteA) rec =
  case divMod (S a) (S b) of
    Fraction (S a) (S b) q FZ prf =>
        let sbIsFactor =
                rewrite multCommutative b q in
                rewrite sym $ multRightSuccPlus q b in
                replace {p = \x => S a = x} (plusZeroRightNeutral (q * S b)) $ sym prf
            skDividesA = CofactorExists q sbIsFactor
            skDividesB = reflexive {x = S b}
        in
        (S b ** MkGCD (CommonFactorExists (S b) skDividesA skDividesB)
                      (\q', (CommonFactorExists q' _ qfb) => qfb))

    Fraction (S a) (S b) q (FS r) prf =>
            let rLtSb = lteSuccRight $ elemSmallerThanBound r
                _ = the (LTE 1 q) $ case q of
                    Z => absurd . notLteAndGt (S $ finToNat r) b (elemSmallerThanBound r) $
                        replace {p = LTE (S b)} (sym prf) bLteA
                    (S k) => LTESucc LTEZero
                (f ** MkGCD (CommonFactorExists f prfSb prfRem) greatestSbSr) =
                    rec (SearchArgs (S b) (S $ finToNat r) rLtSb) $
                      rewrite plusCommutative a (S b) in
                        LTESucc . LTESucc . plusLteLeft b . fromLteSucc $
                          transitive {rel = LTE} (elemSmallerThanBound $ FS r) bLteA

                prfSa =
                    rewrite sym prf in
                    rewrite multCommutative q (S b) in
                    plusFactor (multNAlsoFactor prfSb q) prfRem
                greatest = the
                    ((q' : Nat) -> CommonFactor q' (S a) (S b) -> Factor q' f)
                    (\q', (CommonFactorExists q' qfa qfb) =>
                        let sbfqSb =
                                rewrite multCommutative q (S b) in
                                multFactor (S b) q
                            rightPrf = minusFactor {a = q * S b}
                                (rewrite prf in qfa)
                                (transitive {ty = Nat} qfb sbfqSb)
                        in
                        greatestSbSr q' (CommonFactorExists q' qfb rightPrf)
                    )
            in
            (f ** MkGCD (CommonFactorExists f prfSa prfSb) greatest)

||| An implementation of Euclidean Algorithm for computing greatest common
||| divisors. It is proven correct and total; returns a proof that computed
||| number actually IS the GCD. Unfortunately it's very slow, so improvements
||| in terms of efficiency would be welcome.
export
gcd : (a, b : Nat) -> {auto ok : NotBothZero a b} -> (f : Nat ** GCD f a b)
gcd Z Z impossible
gcd Z b =
    (b ** MkGCD (CommonFactorExists b (anythingFactorZero b) (reflexive {x = b})) $
        \q, (CommonFactorExists q _ prf) => prf
    )
gcd a Z =
    (a ** MkGCD (CommonFactorExists a (reflexive {x = a}) (anythingFactorZero a)) $
        \q, (CommonFactorExists q prf _) => prf
    )
gcd (S a) (S b) with (cmp (S a) (S b))
    gcd (S (b + S d)) (S b) | CmpGT d =
        sizeInd gcd_step $
          SearchArgs (S (b + S d)) (S b) $
            rewrite sym $ plusSuccRightSucc b d in
              LTESucc . lteSuccRight $ lteAddRight b

    gcd (S a) (S a)         | CmpEQ =
        (S a ** MkGCD (selfIsCommonFactor (S a))
                      (\q, (CommonFactorExists q qfa _) => qfa))

    gcd (S a) (S (a + S d)) | CmpLT d =
        let (f ** MkGCD prf greatest) =
              sizeInd gcd_step $
                SearchArgs (S (a + S d)) (S a) $
                  rewrite sym $ plusSuccRightSucc a d in
                    LTESucc . lteSuccRight $ lteAddRight a
        in
        (f ** MkGCD (symmetric {ty = Nat} prf)
                    (\q, cf => greatest q $ symmetric {ty = Nat} cf))

||| For every two natural numbers there is a unique greatest common divisor.
export
gcdUnique : GCD p a b -> GCD q a b -> p = q
gcdUnique (MkGCD pCFab greatestP) (MkGCD qCFab greatestQ) =
    antisymmetric (greatestQ p pCFab) (greatestP q qCFab)

divByGcdHelper : (a, b, c : Nat) -> GCD (S a) (S a * S b) (S a * c) -> GCD 1 (S b) c
divByGcdHelper a b c (MkGCD _ greatest) =
    MkGCD (CommonFactorExists 1 (oneIsFactor (S b)) (oneIsFactor c)) $
    \q, (CommonFactorExists q (CofactorExists qb prfQB) (CofactorExists qc prfQC)) =>
        let qFab = CofactorExists qb $
                rewrite multCommutative q (S a) in
                rewrite sym $ multAssociative (S a) q qb in
                rewrite sym $ prfQB in
                Refl
            qFac = CofactorExists qc $
                rewrite multCommutative q (S a) in
                rewrite sym $ multAssociative (S a) q qc in
                rewrite sym $ prfQC in
                Refl
            CofactorExists f prfQAfA =
                greatest (q * S a) (CommonFactorExists (q * S a) qFab qFac)
            qf1 = multOneSoleNeutral a (f * q) $
                rewrite multCommutative f q in
                rewrite multAssociative (S a) q f in
                rewrite sym $ multCommutative q (S a) in
                prfQAfA
        in
        CofactorExists f $
            rewrite multCommutative q f in
            sym qf1

||| For every two natural numbers, if we divide both of them by their GCD,
||| the GCD of resulting numbers will always be 1.
export
divByGcdGcdOne : {a, b, c : Nat} -> GCD a (a * b) (a * c) -> GCD 1 b c
divByGcdGcdOne {a = Z} (MkGCD _ _) impossible
divByGcdGcdOne {a = S a} {b = Z} {c = Z} (MkGCD {notBothZero} _ _) =
        case replace {p = \x => NotBothZero x x} (multZeroRightZero (S a)) notBothZero of
            LeftIsNotZero impossible
            RightIsNotZero impossible
divByGcdGcdOne {a = S a} {b = Z} {c = S c} gcdPrf@(MkGCD {notBothZero} _ _) =
        case replace {p = \x => NotBothZero x (S a * S c)} (multZeroRightZero (S a)) notBothZero of
            LeftIsNotZero impossible
            RightIsNotZero => symmetric {ty = Nat} $ divByGcdHelper a c Z $ symmetric {ty = Nat} gcdPrf
divByGcdGcdOne {a = S a} {b = S b} {c = Z} gcdPrf@(MkGCD {notBothZero} _ _) =
        case replace {p = \x => NotBothZero (S a * S b) x} (multZeroRightZero (S a)) notBothZero of
            RightIsNotZero impossible
            LeftIsNotZero => divByGcdHelper a b Z gcdPrf
divByGcdGcdOne {a = S a} {b = S b} {c = S c} gcdPrf =
        divByGcdHelper a b (S c) gcdPrf


text:
module Main

import System
import Data.Vect

printLength : IO ()
printLength = getLine >>= \line => let len = length line in
                                   putStrLn $ show len

-- 5.1.4 Exercises
-- Using do notation, write a program which reads two strings then displays the length of the longer string
lenghtOfLonger : IO ()
lenghtOfLonger = do
                    line1 <- getLine
                    line2 <- getLine
                    let l1 = length line1
                    let l2 = length line2
                    putStrLn $ show $ if l1 > l2 then l1 else l2

-- Write the same program using >>= instead of do notation
lenghtOfLonger' : IO ()
lenghtOfLonger' = getLine >>=
                    \line1 => let l1 = length line1 in
                              getLine >>=
                                \line2 => let l2 = length line2 in
                                          putStrLn $ show $ if l1 > l2 then l1 else l2

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

-- 5.2.4 Exercises
-- Write a function which implements a simple "guess the number" game.
guess : (target : Nat) -> IO ()
guess target = do
                  putStrLn "your guess : "
                  Just ok <- readNumber | Nothing => do
                                                      putStrLn "number please"
                                                      guess target
                  case compare ok target of
                    LT => do
                            putStrLn "too low"
                            guess target
                    GT => do
                            putStrLn "too high"
                            guess target
                    EQ => putStrLn "bingo!"

read_vect : IO (len ** Vect len String)
read_vect = do l <- getLine
               if l == ""
                  then pure (_ ** [])
                  else do (_ ** ls) <- read_vect
                          pure (_ ** l :: ls)

zipInputs : IO ()
zipInputs = do putStrLn "Enter first vector (blank line to end):"
               (len1 ** vec1) <- read_vect
               putStrLn "Enter second vector (blank line to end):"
               (len2 ** vec2) <- read_vect
               case exactLength len1 vec2 of
                    Nothing => putStrLn "Vectors are different lengths"
                    Just vec2' => printLn (zip vec1 vec2')

-- 5.3.5 Exercises
-- openFile, closeFile, fEOF, fGetLine, writeFile
readToBlank : IO (List String)
readToBlank = do l <- getLine
                 if l == ""
                    then pure []
                    else do ls <- readToBlank
                            pure $ l :: ls

-- *chap05> :exec readToBlank >>= printLn
-- first
-- second
--
-- ["first", "second"]

-- openFile	 : 	(f : String) -> (m : Mode) -> IO File
-- openFile	 : 	(f : String) -> (m : Mode) -> IO (Either FileError File)
-- writeFile	 : 	(filepath : String) -> (contents : String) -> IO (Either FileError ())

readAndSave : IO ()
readAndSave =
  do ls <- readToBlank
     filename <- getLine
     Right result <- writeFile filename (unwords ls)
      | Left err => putStrLn (show err)
     pure result

 -- fEOF	 : 	File -> IO Bool
 -- Check if a file handle has reached the end
 -- fGetLine	 : 	(h : File) -> IO (Either FileError String)

read : (h : File) -> IO (n ** Vect n String)
read h =
  do
    eof <- fEOF h
    if eof
       then pure (_ ** [])
       else
         do
           Right line <- fGetLine h
           (_ ** lines) <- read h
           pure (_ ** line :: lines)

readVectFile : (filename : String) -> IO (n ** Vect n String)
readVectFile filename =
  do Right f <- openFile filename Read
      | Left err => do
                      pure (_ ** [])
     read f

main : IO ()
main = do
        v <- readVectFile "test.txt"
        putStrLn $ show v

-- *chap05> :exec zipInputs
-- Enter first vector (blank line to end):
-- 1
-- 2
-- 3
--
-- Enter second vector (blank line to end):
-- a
-- b
-- c
--
-- [("1", "a"), ("2", "b"), ("3", "c")]

-- *chap05> :exec read_vect >>= printLn
-- hi
-- howdy
--
-- (2 ** ["hi", "howdy"])

-- main : IO ()
-- main = do
--         r <- random
--         putStrLn r

-- *chap05> :exec lenghtOfLonger'
-- long
-- longer
-- 6

-- *chap05> :exec lenghtOfLonger
-- short
-- longer
-- 6

--  ~/W/i/starting git:master λ →  ~/idris-install/.cabal-sandbox/bin/idris chap05.idr                                                                                ⬆ ✖ ◼
--       ____    __     _
--      /  _/___/ /____(_)____
--      / // __  / ___/ / ___/     Version 0.12
--    _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
--   /___/\__,_/_/  /_/____/       Type :? for help
 --
--  Idris is free software with ABSOLUTELY NO WARRANTY.
--  For details type :warranty.
--  Type checking ./chap05.idr
--  *chap05> :exec printLength
--  haha
--  4
--  *chap05> :q
--  Bye bye


text:
module Http.Error

import public Network.Socket

%access public export

data HttpError : Type where
  HttpSocketError : SocketError -> HttpError
  HttpParseError : String -> HttpError

implementation Show HttpError where
  show (HttpSocketError err) = show err
  show (HttpParseError err) = err

max_stars_repo_name: unthingable/idris-https

max_issues_repo_name: unthingable/idris-https

max_forks_repo_name: unthingable/idris-https


text:
module Main
import Data.List

myTriple : Double -> Double
myTriple x = 3 * x

ms : List Double
ms = [1.0, 2.0, 3.0]

main : IO ()
main = do printLn $ map myTriple ms


text:
import Data.Vect
import Control.Monad.State

-- Page 332

-- Exercise 1
update : (stateType -> stateType) -> State stateType ()
update f = do current <- get
              put (f current)

-- Exercise 2
data Tree a = Empty | Node (Tree a) a (Tree a)

testTree : Tree String
testTree = Node (Node (Node Empty "Jim" Empty) "Fred"
                     (Node Empty "Sheila" Empty)) "Alice"
               (Node Empty "Bob" (Node Empty "Eve" Empty))

countEmpty : Tree a -> State Nat ()
countEmpty Empty = do
  current <- get
  put (S current)

countEmpty (Node left val right) = do
  countEmpty left
  countEmpty right

-- Exercise 3
countEmptyNode : Tree a -> State (Nat, Nat) ()
countEmptyNode Empty = do
  (empties, nodes) <- get
  put (S empties, nodes)
countEmptyNode (Node left val right) = do
  countEmptyNode left
  (empties, nodes) <- get
  put (empties, S nodes)
  countEmptyNode right

-- Page 350
record Score where
       constructor MkScore
       correct : Nat
       attempted : Nat

record GameState where
       constructor MkGameState
       score : Score
       difficulty : Int

data Command : Type -> Type where
  PutStr : String -> Command ()
  GetLine : Command String

  GetRandom : Command Int
  GetGameState : Command GameState
  PutGameState : GameState -> Command ()

  Pure : ty -> Command ty
  Bind : Command a -> (a -> Command b) -> Command b

-- Exercise 1

-- Exercise 2
mutual
  Functor Command where
    map func x = Bind x (\a => Pure (func a))

  Applicative Command where
    pure = Pure
    (<*>) f x = do f' <- f
                   x' <- x
                   Pure (f' x')

  Monad Command where
    (>>=) = Bind

-- Exercise 3
record Votes where
      constructor MkVotes
      upvotes : Integer
      downvotes : Integer

record Article where
      constructor MkArticle
      title : String
      url : String
      score : Votes

initPage : (title : String) -> (url : String) -> Article
initPage title url = MkArticle title url (MkVotes 0 0)

getScore : Article -> Integer
getScore (MkArticle title url (MkVotes upvotes downvotes)) = upvotes - downvotes

badSite : Article
badSite = MkArticle "Bad Page" "http://example.com/bad" (MkVotes 5 47)
goodSite : Article
goodSite = MkArticle "Good Page" "http://example.com/good" (MkVotes 101 7)

-- Exercise 4
addUpvote : Article -> Article
addUpvote = record {score->upvotes $= (+1)}

addDownvote : Article -> Article
addDownvote = record {score -> downvotes $= (+1)}

-- Page 362

-- Exercise 1
namespace ex1
  data DoorState = DoorClosed | DoorOpen

  data DoorCmd : Type -> DoorState -> DoorState -> Type where
    Open : DoorCmd     () DoorClosed DoorOpen
    Close : DoorCmd    () DoorOpen   DoorClosed
    RingBell : DoorCmd () ds         ds

    -- Pure : ty -> DoorCmd ty state state
    (>>=) : DoorCmd a state1 state2
            -> (a -> DoorCmd b state2 state3)
            -> DoorCmd b state1 state3

  doorProg : DoorCmd () DoorClosed DoorClosed
  doorProg = do RingBell
                Open
                RingBell
                Close

-- Exercise 2
namespace ex2
  data GuessCmd : Type -> Nat -> Nat -> Type where
    Try : Integer -> GuessCmd Ordering (S k) k
    Pure : ty -> GuessCmd ty state state
    (>>=) : GuessCmd a state1 state2
            -> (a -> GuessCmd b state2 state3)
            -> GuessCmd b state1 state3

  threeGuesses: GuessCmd () 3 0
  threeGuesses = do Try 10
                    Try 20
                    Try 15
                    Pure ()

  -- This shouldn't compile
  -- noGuesses : GuessCmd () 0 0
  -- noGuesses = do Try 10
  --                Pure ()

-- Exercise 3
namespace ex3
  data Matter = Solid | Liquid | Gas

  data MatterCmd : Type -> Matter -> Matter -> Type where
    Melt :     MatterCmd () Solid  Liquid
    Boil :     MatterCmd () Liquid Gas
    Condense : MatterCmd () Gas    Liquid
    Freeze :   MatterCmd () Liquid Solid

    Pure : ty -> MatterCmd ty state state
    (>>=) : MatterCmd a m1 m2
            -> (a -> MatterCmd b m2 m3)
            -> MatterCmd b m1 m3

  iceSteam : MatterCmd () Solid Gas
  iceSteam = do Melt
                Boil
  steamIce : MatterCmd () Gas Solid
  steamIce = do Condense
                Freeze

max_stars_repo_name: JnxF/advanced-software-analysis

max_issues_repo_name: JnxF/advanced-software-analysis

max_forks_repo_name: JnxF/advanced-software-analysis