text:
module Control.Monad.Coop

import public System.Time

import Data.List
import Data.Queue1
import Data.SortedMap
import Data.SortedSet
import public Data.Zippable

import public Control.Applicative.Concurrent

import Control.Monad.Coop.Sync
import public Control.Monad.Spawn
import Control.Monad.State
import Control.Monad.State.Tuple
import public Control.Monad.Trans

%default total

------------
--- Data ---
------------

data SyncKind = Join | Race

export
data Coop : (m : Type -> Type) -> (a : Type) -> Type where
  Point       : m a -> Coop m a
  Sequential  : Coop m a -> (a -> Coop m b) -> Coop m b
  Interleaved : Coop m a -> Coop m b -> Coop m (a, b)
  Racing      : Coop m a -> Coop m a -> Coop m a
  RaceFence   : (prevRaceSync : Maybe $ Sync Race) -> Coop m Unit
  DelayedTill : Time -> Coop m Unit
  Spawn       : Coop m Unit -> Coop m Unit
  Empty       : Coop m a

-----------------------
--- Implementations ---
-----------------------

export
Timed m => Timed (Coop m) where
  currentTime = Point currentTime

export
Applicative m => Functor (Coop m) where
  map f (Point a)           = Point (map f a)
  map f (Sequential a b)    = Sequential a $ \ar => map f $ b ar
  map f x@(Interleaved _ _) = Sequential x $ Point . pure . f
  map f x@(Racing _ _)      = Sequential x $ Point . pure . f
  map f x@(RaceFence _)     = Sequential x $ Point . pure . f
  map f x@(DelayedTill _)   = Sequential x $ Point . pure . f
  map f x@(Spawn _)         = Sequential x $ Point . pure . f
  map _ Empty               = Empty

export
Applicative m => Applicative (Coop m) where
  pure    = Point . pure
  l <*> r = Sequential l (<$> r)
  -- This could be `(<*>) = Interleaved <&> uncurry apply`, but it must be consistent with `(>>=)` definition.
  -- Consider code `doSmth *> sleepFor 100 *> doMore` comparing to `(doSmth `zip` sleepFor 100) *> doMore`.
  -- Having parallel semantics for the `Applicative`'s `<*>`, those two examples above will mean the same, which seems to be unexpected.
  -- We have a special name instance `Concurrent` below for that case.

export
race : Applicative m => Coop m a -> Coop m b -> Coop m $ Either a b
race l r = Racing (l <&> Left) (r <&> Right)

export
Applicative m => Alternative (Coop m) where
  -- `empty` computation is like an infinite computation (i.e. no computation goes *after* it and its result cannot be analysed),
  -- but in contrast, if it is the only what is left during the execution, computation simply finishes.
  empty = Empty
  l <|> r = l `Racing` r

export
Applicative m => Monad (Coop m) where
  (>>=) = Sequential

export
Applicative m => Zippable (Coop m) where
  zip = Interleaved
  zipWith f = map (uncurry f) .: Interleaved

  zip3 a b c = a `Interleaved` (b `Interleaved` c)
  zipWith3 f a b c = zip3 a b c <&> \(x, y, z) => f x y z

  unzipWith f ab = (fst . f <$> ab, snd . f <$> ab)
  unzipWith3 f abc = (fst . f <$> abc, fst . snd . f <$> abc, snd . snd . f <$> abc)

[Conc] Applicative m => Applicative (Coop m) where
  pure  = Point . pure
  (<*>) = zipWith apply

export
Applicative m => ConcurrentApplicative (Coop m) where
  Concurrent = Conc

export
Timed m => Applicative m => CanSleep (Coop m) where
  sleepTill = DelayedTill

export
Applicative m => CanSpawn (Coop m) where
  -- Runs the given computation in parallel with the monadic continuation.
  -- In contrast with `zip`, the continuations executes immediately, without waiting to the end of spawned computation.
  -- Spawned computation will continue to work (if it needs) even if continuation has ended.
  -- For example, running the following code
  --
  -- ```idris
  -- x : HasIO m => Coop m Nat
  -- x = do
  --   spawn $ do
  --     sleepFor 4.seconds
  --     putStrLn "spawned"
  --   putStrLn "main"
  --   pure 1
  -- ```
  --
  -- will result in returning `1` as the computation result **and** printing "spawned" in four seconds after funning the whole computation `x`.
  spawn = Spawn

export
HasIO (Coop IO) where
  liftIO = Point

export
MonadTrans Coop where
  lift = Point

-------------------
--- Interpreter ---
-------------------

--- Data types describing discrete events ---

data LeftOrRight = Left | Right

record Event (m : Type -> Type) where
  constructor Ev
  time : Time
  coop : Coop m actionRetTy
  -- Two present postponed events with the same sync are meant to be blocking each other.
  -- Postponed event needs to be sheduled only when all events with its sync are over.
  -- `Sync` type is a comparable type and is a workaround of uncomparability of `Coop`.
  joinSync : Maybe (Sync Join, LeftOrRight)
  raceSync : Maybe $ Sync Race

--- List of events ---

0 Events : (Type -> Type) -> Type
Events = SortedMap Time . Queue1 . Event

insertTimed : Event m -> Events m -> Events m
insertTimed ev evs = insert ev.time (maybe (singleton ev) (add ev) (lookup ev.time evs)) evs

-- Must be equivalent to `insertTimed ev empty`
singleEvent : Event m -> Events m
singleEvent ev = singleton ev.time $ singleton ev

addEvents : MonadState (Events m) n => Event m -> List (Event m -> Event m) -> n Unit
addEvents ev = modify . foldl (\acc, modF => acc . insertTimed (modF ev)) id

-- Psrticular case for `addEvents ev [modF]`
addEvent : MonadState (Events m) n => Event m -> (Event m -> Event m) -> n Unit
addEvent ev modF = modify $ insertTimed $ modF ev

-- Psrticular case for `addEvents ev [modF1, modF2]`
addEvent2 : MonadState (Events m) n => Event m -> (Event m -> Event m) -> (Event m -> Event m) -> n Unit
addEvent2 ev modF1 modF2 = modify $ insertTimed (modF1 ev) . insertTimed (modF2 ev)

earliestEvent : Events m -> Maybe (Event m, Lazy (Events m))
earliestEvent evs = leftMost evs <&> \(t, tEvs) =>
  let (currEv, restTEvs) = remove tEvs in
  (currEv,) $ maybe (delete t evs) (\r => insert t r evs) restTEvs

filterEvents : (Event m -> Bool) -> Events m -> Events m
filterEvents f = fromList . mapMaybe (\(t, evs) => (t,) <$> filter f evs) . SortedMap.toList

--- Join synchronisation stuff ---

record Postponed (m : Type -> Type) where
  constructor Postpone
  postCoop : (contLTy, contRTy) -> Coop m contRetTy
  postJoinSync : Maybe (Sync Join, LeftOrRight)
  -- This postponed continuation is waiting for two executions.
  -- When one of them is completed, the result should be present in this field.
  completedHalf : Maybe completedHalfTy

0 JoinSyncs : (Type -> Type) -> Type
JoinSyncs = SortedMap (Sync Join) . Postponed

--- Race synchronisation stuff ---

-- Map from one race sync to all child syncs (i.e. those which are cancelled when a series with the parent sync finished)
0 RaceSyncs : Type
RaceSyncs = SortedMap (Sync Race) $ List $ Sync Race

transitiveLookup : Foldable f => Ord a => SortedMap a (f a) -> a -> SortedSet a
transitiveLookup mp x = let x1 = singleton x in go x1 x1 where
  go : (curr : SortedSet a) -> (new : SortedSet a) -> SortedSet a
  go curr new = if null new then curr else do
    let allNexts = fromList $ SortedSet.toList new >>= maybe [] toList . flip SortedMap.lookup mp
    let nextNew = allNexts `difference` curr
    assert_total $ go (curr `union` nextNew) nextNew -- first argument is growing and has maximum bound (all `a` in the `mp`)

--- The run loop ---

%inline
runEvent : Monad m => MonadTrans t => Monad (t m) =>
           MonadState (Events m) (t m) =>
           MonadState (JoinSyncs m) (t m) =>
           MonadState RaceSyncs (t m) =>
           Event m -> t m Unit
runEvent ev = case ev.coop of
  Point x          => lift x >>= awakePostponed
  Sequential lhs f => case lhs of
    Point x         => lift x >>= \r => addEvent ev {coop := f r}
    Sequential x g  => addEvent ev {coop := Sequential x $ g >=> f}
    DelayedTill d   => addEvent ev {time := d, coop := f ()}
    Spawn s         => addEvent2 ev {coop := s, joinSync := Nothing} {coop := f ()}
    Interleaved l r => do uniqueSync <- newUniqueSync <$> get
                          modify $ insert uniqueSync $ Postpone f ev.joinSync $ Nothing {ty=Unit}
                          addEvent2 ev
                            {coop := l, joinSync := Just (uniqueSync, Left )}
                            {coop := r, joinSync := Just (uniqueSync, Right)}
    RaceFence prevS => finishRaces *> addEvent ev {coop := f (), raceSync := prevS}
    Racing Empty r  => addEvent ev {coop := r >>= f}
    Racing l Empty  => addEvent ev {coop := l >>= f}
    Racing l r      => do uniqueSync <- newUniqueSync <$> get
                          modify $ insert uniqueSync [] -- to prevent generation of the same sync
                          whenJust ev.raceSync $ \parent => modify $ merge $ singleton parent [uniqueSync]
                          addEvent2 ev
                            {coop := l >>= (RaceFence ev.raceSync *>) . f, raceSync := Just uniqueSync}
                            {coop := r >>= (RaceFence ev.raceSync *>) . f, raceSync := Just uniqueSync}
    Empty           => pure ()
  nonSeqNonPoint   => addEvent ev {coop := nonSeqNonPoint >>= pure}       -- manage as `Sequential _ Point`

  where

    awakePostponed : forall a. a -> t m Unit
    awakePostponed myHalf =
      whenJust ev.joinSync $ \(sy, iAmLOrR) => do
        syncs <- get
        whenJust (SortedMap.lookup sy syncs) $ \pp =>
          case pp.completedHalf of
            Just theirHalf => do
              let awakenCoop = pp.postCoop $ case iAmLOrR of
                    Left  => believe_me (myHalf, theirHalf)
                    Right => believe_me (theirHalf, myHalf)
              addEvent ev {coop := awakenCoop, joinSync := pp.postJoinSync}
              put $ delete sy syncs
            Nothing =>
              put $ insert sy ({completedHalf := Just myHalf} pp) syncs

    finishRaces : t m Unit
    finishRaces = whenJust ev.raceSync $ \currRaceSync => do
      raceSyncs <- get
      let syncsToRemove = transitiveLookup raceSyncs currRaceSync
      modify $ filterEvents $ maybe True (not . flip contains syncsToRemove) . raceSync
      put $ foldl (flip SortedMap.delete) raceSyncs syncsToRemove

export covering
runCoop : CanSleep m => Monad m => Coop m Unit -> m Unit
runCoop co = do
  let initEvents = singleEvent $ Ev !currentTime co Nothing Nothing
      initJoinSyncs : JoinSyncs m = empty
      initRaceSyncs : RaceSyncs = empty
  evalStateT (initEvents, initJoinSyncs, initRaceSyncs) runLeftEvents where

  runLeftEvents : MonadTrans t => Monad (t m) =>
                  MonadState (Events m) (t m) =>
                  MonadState (JoinSyncs m) (t m) =>
                  MonadState RaceSyncs (t m) =>
                  t m Unit
  runLeftEvents =
    whenJust (earliestEvent !get) $ \(currEv, restEvs) => do
      currTime <- lift currentTime
      if currTime >= currEv.time
        then put restEvs *> runEvent ({time := currTime} currEv)
        else lift $ sleepTill currEv.time -- TODO to support and perform permanent tasks
      runLeftEvents


text:
||| Spec: http://webassembly.github.io/spec/core/syntax/types.html#limits
module WebAssembly.Structure.Types.Limits

import WebAssembly.Structure.Values

import Decidable.Equality

-- Definition

public export
data Limits : Type where
  MkLimits : (n: U32) -> (m: Maybe U32) -> Limits

-- Equality

total public export
lemma_limits__lowerbound_injective : (lb1_not_lb2 : (lb1 = lb2) -> Void) -> (MkLimits lb1 up1 = MkLimits lb2 up2) -> Void
lemma_limits__lowerbound_injective lb1_not_lb2 Refl = lb1_not_lb2 Refl

total public export
lemma_limits__upperbound_injective : (up1_not_up2 : (up1 = up2) -> Void) -> (MkLimits lb1 up1 = MkLimits lb1 up2) -> Void
lemma_limits__upperbound_injective up1_not_up2 Refl = up1_not_up2 Refl

-- Decidable Equality

public export
implementation DecEq Limits where
  decEq (MkLimits lb1 up1) (MkLimits lb2 up2) = case (decEq lb1 lb2) of
    No lb1_not_lb2 => No (lemma_limits__lowerbound_injective lb1_not_lb2)
    Yes Refl       => case (decEq up1 up2) of
      No up1_not_up2 => No (lemma_limits__upperbound_injective up1_not_up2)
      Yes Refl       => Yes Refl

ext: idr

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module Main

main : IO ()
main = putStrLn "Hello world"

--Run:
--$ idris hello-world.idr -o hello
--$ ./hello

max_stars_repo_name: coyote-dev/Hello-World

max_issues_repo_name: coyote-dev/Hello-World

max_forks_repo_name: coyote-dev/Hello-World


text:
module Inequiv

import Equiv
import Expr
import Imp
import Maps

%access public export

%default total

subst_aexp : (x : Id) -> (u : AExp) -> (a : AExp) -> AExp
subst_aexp x u (ANum k) = ANum k
subst_aexp x u (AId y) = case decEq x y of
  Yes prf => u
  No contra => AId y
subst_aexp x u (APlus a1 a2) = APlus (subst_aexp x u a1) (subst_aexp x u a2)
subst_aexp x u (AMinus a1 a2) = AMinus (subst_aexp x u a1) (subst_aexp x u a2)
subst_aexp x u (AMult a1 a2) = AMult (subst_aexp x u a1) (subst_aexp x u a2)

subst_aexp_example : subst_aexp X (42 + 53) (AId Y + AId X) = AId Y + (42 + 53)
subst_aexp_example = Refl

FaultySubstEquivProperty : Type
FaultySubstEquivProperty = (x1, x2 : Id) -> (a1, a2 : AExp) ->
                           CEquiv (do x1 ::= a1; x2 ::= a2)
                                  (do x1 ::= a1; x2 ::= subst_aexp x1 a1 a2)

subst_inequiv : Not FaultySubstEquivProperty
subst_inequiv equiv =
  let -- c1 and c2 are defined only for illustration
      c1 = do X ::= AId X + 1
              Y ::= AId X
      c2 = do X ::= AId X + 1
              Y ::= AId X + 1
      c1_equiv_c2 = equiv X Y (AId X + 1) (AId X)
      st1 = t_update Y 1 $ t_update X 1 $ empty_state
      st2 = t_update Y 2 $ t_update X 1 $ empty_state
      h1 = fst (c1_equiv_c2 empty_state st1)
               (E_Seq (E_Ass Refl) (E_Ass Refl))
      h2 = snd (c1_equiv_c2 empty_state st2)
               (E_Seq (E_Ass Refl) (E_Ass Refl))
      h = snd (c1_equiv_c2 empty_state st1) h1
      st1_eq_st2 = ceval_deterministic h h2
      contra = cong {f=\st => st Y} st1_eq_st2
  in absurd $ succInjective 0 1 contra

data VarNotUsedInAExp : (x : Id) -> AExp -> Type where
  VNUNum : (n : Nat) -> VarNotUsedInAExp x (ANum n)
  VNUId : (y : Id) -> Not (x = y) -> VarNotUsedInAExp x (AId y)
  VNUPlus : (a1, a2 : AExp) ->
            VarNotUsedInAExp x a1 ->
            VarNotUsedInAExp x a2 ->
            VarNotUsedInAExp x (a1 + a2)
  VNUMinus : (a1, a2 : AExp) ->
             VarNotUsedInAExp x a1 ->
             VarNotUsedInAExp x a2 ->
             VarNotUsedInAExp x (AMinus a1 a2)
  VNUMult : (a1, a2 : AExp) ->
            VarNotUsedInAExp x a1 ->
            VarNotUsedInAExp x a2 ->
            VarNotUsedInAExp x (a1 * a2)

aeval_weakening : VarNotUsedInAExp x a ->
                  aeval (t_update x n st) a = aeval st a
aeval_weakening (VNUNum _) = Refl
aeval_weakening (VNUId _ contra) =
  rewrite snd beq_id_false_iff contra
  in Refl
aeval_weakening {x} {st} {n} (VNUPlus _ _ vnua1 vnua2) =
  rewrite aeval_weakening {x=x} {st=st} {n=n} vnua1
  in rewrite aeval_weakening {x=x} {st=st} {n=n} vnua2
  in Refl
aeval_weakening {x} {st} {n} (VNUMinus _ _ vnua1 vnua2) =
  rewrite aeval_weakening {x=x} {st=st} {n=n} vnua1
  in rewrite aeval_weakening {x=x} {st=st} {n=n} vnua2
  in Refl
aeval_weakening {x} {st} {n} (VNUMult _ _ vnua1 vnua2) =
  rewrite aeval_weakening {x=x} {st=st} {n=n} vnua1
  in rewrite aeval_weakening {x=x} {st=st} {n=n} vnua2
  in Refl

subst_aexp_equiv : VarNotUsedInAExp x a -> AEquiv a (subst_aexp x u a)
subst_aexp_equiv (VNUNum _) _ = Refl
subst_aexp_equiv {x} {u} (VNUId y contra) _ with (decEq x y)
  subst_aexp_equiv (VNUId y contra) _ | Yes prf = absurd $ contra prf
  subst_aexp_equiv (VNUId y contra) _ | No _ = Refl
subst_aexp_equiv {u} (VNUPlus _ _ xnua1 xnua2) st =
  let a1_equiv = subst_aexp_equiv {u=u} xnua1 st
      a2_equiv = subst_aexp_equiv {u=u} xnua2 st
  in rewrite a1_equiv
  in rewrite a2_equiv
  in Refl
subst_aexp_equiv {u} (VNUMinus _ _ xnua1 xnua2) st =
  let a1_equiv = subst_aexp_equiv {u=u} xnua1 st
      a2_equiv = subst_aexp_equiv {u=u} xnua2 st
  in rewrite a1_equiv
  in rewrite a2_equiv
  in Refl
subst_aexp_equiv {u} (VNUMult _ _ xnua1 xnua2) st =
  let a1_equiv = subst_aexp_equiv {u=u} xnua1 st
      a2_equiv = subst_aexp_equiv {u=u} xnua2 st
  in rewrite a1_equiv
  in rewrite a2_equiv
  in Refl

SubstEquivProperty : Type
SubstEquivProperty = (x1, x2 : Id) -> (a1, a2 : AExp) ->
                     VarNotUsedInAExp x1 a2 ->
                     CEquiv (do x1 ::= a1; x2 ::= a2)
                            (do x1 ::= a1; x2 ::= subst_aexp x1 a1 a2)

subst_equiv_property : SubstEquivProperty
subst_equiv_property _ _ _ _ x1nua2 =
  cSeq_congruence refl_cequiv (cAss_congruence (subst_aexp_equiv x1nua2))

inequiv_exercise : Not (CEquiv (CWhile BTrue CSkip) CSkip)
inequiv_exercise equiv =
  let nonterm_prf = while_true_nonterm refl_bequiv
      nonterm_equiv_skip = equiv empty_state empty_state
  in nonterm_prf $ snd nonterm_equiv_skip E_Skip


text:
%default total

data Wrap : Type -> Type where
  MkWrap : a -> Wrap a

unwrap : Wrap a -> a
unwrap (MkWrap v) = v

data F : Type where
  MkF : Wrap (Not F) -> F

yesF : Not F -> F
yesF = MkF . MkWrap

notF : Not F
notF (MkF f) = unwrap f (yesF $ unwrap f)

argh : Void
argh = notF (yesF notF)


text:
-- ------------------------------------------------------------- [ Helpers.idr ]
-- Module      : Test.Helpers
-- Description : Helper functions for writing tests.
-- --------------------------------------------------------------------- [ EOH ]
module Test.Helpers

import public Test.Generic

import Data.Vect

%access export

||| Like Test.Assertions.assertEqual but with `given` and `expected` swapped.
assertEqual' : (Eq a, Show a) =>
               (title : String) ->
               (expected, given : a) ->
               IO Bool
assertEqual' title expected given = genericTest (Just title) given expected (==)

namespace SingleResult
  summaryLine : Bool -> String
  summaryLine True  = succLine
  summaryLine False = errLine

namespace ManyResults
  summaryLine : Foldable t => t Bool -> String
  summaryLine = summaryLine . all id

printSummary : Vect n Bool -> IO ()
printSummary = putStrLn . unlines . ([summaryLine, summary] <*>) . pure

testChapter : (label : String) ->
              (tests : List (IO Bool)) ->
              IO (Vect (length tests) Bool)
testChapter label tests =
    do putStrLn $ "Testing Chapter " ++ label
       putStrLn infoLine
       results <- sequence (fromList tests)
       printSummary results
       pure results

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

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
import Data.So

record Newtype where
  constructor
  MkNewtype
  wrapped : Double

FromDouble Newtype where
  fromDouble = MkNewtype

Show Newtype where
  showPrec p (MkNewtype v) = showCon p "MkNewtype" $ showArg v

record InUnit where
  constructor MkInUnit
  value      : Double
  0 inBounds : So (0 <= value && value <= 1)

Show InUnit where
  showPrec p (MkInUnit v _) = showCon p "MkInUnit" $ showArg v ++ " _"

namespace InUnit
  public export
  fromDouble :  (v : Double)
             -> {auto 0 prf : So (0 <= v && v <= 1)}
             -> InUnit
  fromDouble v = MkInUnit v prf

main : IO ()
main = do printLn $ the InUnit 0.25
          printLn $ the Newtype 123.456


text:
module Toml.Tokens

import public Text.Token

import Data.List
import Extra.String

public export
data TomlTokenKind
  = Keyword
  | Dot
  | StringLit
  | Number
  | Equals
  | LeftBracket
  | RightBracket
  | Comma
  | Comment
  | Whitespace

public export
Eq TomlTokenKind where
  Keyword == Keyword = True
  Dot == Dot = True
  StringLit == StringLit = True
  Number == Number = True
  Equals == Equals = True
  LeftBracket == LeftBracket = True
  RightBracket == RightBracket = True
  Comma == Comma = True
  Comment == Comment = True
  Whitespace == Whitespace = True
  _ == _ = False

public export
TomlToken : Type
TomlToken = Token TomlTokenKind

public export
TokenKind TomlTokenKind where
  TokType Keyword = String
  TokType Dot = ()
  TokType StringLit = String
  TokType Number = Int
  TokType Equals = ()
  TokType LeftBracket = ()
  TokType RightBracket = ()
  TokType Comma = ()
  TokType Comment = ()
  TokType Whitespace = ()

  tokValue Keyword str = str
  tokValue Dot x = ()
  tokValue StringLit str = unquote str
  tokValue Number x = cast x
  tokValue Equals x = ()
  tokValue LeftBracket x = ()
  tokValue RightBracket x = ()
  tokValue Comma x = ()
  tokValue Comment x = ()
  tokValue Whitespace x = ()

export
Show TomlToken where
  show (Tok Keyword x) = "Keyword " ++ (quote x)
  show (Tok Dot x) = "Dot " ++ (quote x)
  show (Tok StringLit str) = "StringLit " ++ (quote str)
  show (Tok Number x) = "Number " ++ (show x)
  show (Tok Equals x) = "Equals " ++ (quote x)
  show (Tok LeftBracket x) = "LeftBracket " ++ (quote x)
  show (Tok RightBracket x) = "RightBracket " ++ (quote x)
  show (Tok Comma x) = "Comma " ++ (quote x)
  show (Tok Comment x) = "Comment " ++ (quote x)
  show (Tok Whitespace x) = "Whitespace " ++ (quote x)

export
Eq TomlToken where
  (Tok Keyword x0) == (Tok Keyword x1) = x0 == x1
  (Tok Dot x0) == (Tok Dot x1) = True
  (Tok StringLit x0) == (Tok StringLit x1) = x0 == x1
  (Tok Number x0) == (Tok Number x1) = x0 == x1
  (Tok Equals x0) == (Tok Equals x1) = True
  (Tok LeftBracket x0) == (Tok LeftBracket x1) = True
  (Tok RightBracket x0) == (Tok RightBracket x1) = True
  (Tok Comma x0) == (Tok Comma x1) = True
  (Tok Comment x0) == (Tok Comment x1) = x0 == x1
  (Tok Whitespace x0) == (Tok Whitespace x1) = True
  _ == _ = False

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
||| An order is a particular kind of binary relation. The order
||| relation is intended to proceed in some direction, though not
||| necessarily with a unique path.
|||
||| Orders are often defined simply as bundles of binary relation
||| properties.
|||
||| A prominent example of an order relation is LTE over Nat.

module Control.Order

import Control.Relation

||| A preorder is reflexive and transitive.
public export
interface (Reflexive ty rel, Transitive ty rel) => Preorder ty rel where

||| A partial order is an antisymmetrics preorder.
public export
interface (Preorder ty rel, Antisymmetric ty rel) => PartialOrder ty rel where

||| A relation is connex if for any two distinct x and y, either x ~ y or y ~ x.
|||
||| This can also be stated as a trichotomy: x ~ y or x = y or y ~ x.
public export
interface Connex ty rel where
  connex : {x, y : ty} -> Not (x = y) -> Either (rel x y) (rel y x)

||| A relation is strongly connex if for any two x and y, either x ~ y or y ~ x.
public export
interface StronglyConnex ty rel where
  order : (x, y : ty) -> Either (rel x y) (rel y x)

||| A linear order is a connex partial order.
public export
interface (PartialOrder ty rel, Connex ty rel) => LinearOrder ty rel where

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

||| Every equivalence relation is a preorder.
public export
[EP] Equivalence ty rel => Preorder ty rel where


text:
module Data.Profunctor

import public Data.Profunctor.Class
import public Data.Profunctor.Choice
import public Data.Morphisms


text:
module A.Path.Of.Dires.Second

import public A.Path.Of.Dires.First

%default total

export
example : Tree Nat
example = Node (Node (Leaf 0) (Leaf 1)) (Leaf 2)


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

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

{-
  ported from file kernel/libsel4/include/sel4/bootinfo_types.h
-}

module seL4.BootinfoTypes

import seL4.Types
import seL4.SharedTypes

%access public export
%default total

-- caps with fixed slot positions in the root CNode
data SeL4Cap =
    SeL4_CapNull                -- null cap
  | SeL4_CapInitThreadTCB       -- initial thread's TCB cap
  | SeL4_CapInitThreadCNode     -- initial thread's root CNode cap
  | SeL4_CapInitThreadVSpace    -- initial thread's VSpace cap
  | SeL4_CapIRQControl          -- global IRQ controller cap
  | SeL4_CapASIDControl         -- global ASID controller cap
  | SeL4_CapInitThreadASIDPool  -- initial thread's ASID pool cap
  | SeL4_CapIOPort              -- global IO port cap (null cap if not supported)
  | SeL4_CapIOSpace             -- global IO space cap (null cap if no IOMMU support)
  | SeL4_CapBootInfoFrame       -- bootinfo frame cap
  | SeL4_CapInitThreadIPCBuffer -- initial thread's IPC buffer frame cap
  | SeL4_CapDomain              -- global domain controller cap
  | SeL4_NumInitialCaps

Cast SeL4Cap Int where
    cast SeL4_CapNull                = 0
    cast SeL4_CapInitThreadTCB       = 1
    cast SeL4_CapInitThreadCNode     = 2
    cast SeL4_CapInitThreadVSpace    = 3
    cast SeL4_CapIRQControl          = 4
    cast SeL4_CapASIDControl         = 5
    cast SeL4_CapInitThreadASIDPool  = 6
    cast SeL4_CapIOPort              = 7
    cast SeL4_CapIOSpace             = 8
    cast SeL4_CapBootInfoFrame       = 9
    cast SeL4_CapInitThreadIPCBuffer = 10
    cast SeL4_CapDomain              = 11
    cast SeL4_NumInitialCaps         = 12

SeL4_SlotPos : Type
SeL4_SlotPos = SeL4_Word

record SeL4_SlotRegion where
    constructor MKSeL4_SlotRegion
    start : SeL4_SlotPos
    end : SeL4_SlotPos

record SeL4_UntypedDesc where
    constructor MKSeL4_UntypedDesc
    paddr : SeL4_Word     -- physical address of untyped cap
    padding1 : SeL4_Uint8
    padding2 : SeL4_Uint8
    sizeBits : SeL4_Uint8 -- size (2^n) bytes of each untyped
    isDevice : SeL4_Uint8 -- whether the untyped is a device

record SeL4_BootInfo where
    constructor MKSeL4_BootInfo
    extraLen : SeL4_Word              -- length of any additional bootinfo information
    nodeID : SeL4_NodeId              -- ID [0..numNodes-1] of the seL4 node (0 if uniprocessor)
    numNodes : SeL4_Word              -- number of seL4 nodes (1 if uniprocessor)
    numIOPTLevels : SeL4_Word         -- number of IOMMU PT levels (0 if no IOMMU support)
    ipcBuffer : SeL4_IPCBufferP       -- pointer to initial thread's IPC buffer
    empty : SeL4_SlotRegion           -- empty slots (null caps)
    sharedFrames : SeL4_SlotRegion    -- shared-frame caps (shared between seL4 nodes)
    userImageFrames : SeL4_SlotRegion -- userland-image frame caps
    userImagePaging : SeL4_SlotRegion -- userland-image paging structure caps
    ioSpaceCaps : SeL4_SlotRegion     -- IOSpace caps for ARM SMMU
    extraBIPages : SeL4_SlotRegion    -- caps for any pages used to back the additional bootinfo information
    initThreadCNodeSizeBits : SeL4_Uint8 -- initial thread's root CNode size (2^n slots)
    initThreadDomain : SeL4_Domain    -- Initial thread's domain ID
    archInfo : SeL4_Word              -- tsc freq on x86, unused on arm
    untyped : SeL4_SlotRegion         -- untyped-object caps (untyped caps)
    -- seL4_UntypedDesc  untypedList[CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; -- information about each untyped

record SeL4_BootInfoHeader where
    constructor MKSeL4_BootInfoHeader
    -- identifier of the following chunk. IDs are arch/platform specific
    id : SeL4_Word
    -- length of the chunk, including this header
    len : SeL4_Word

Show SeL4_SlotRegion where
    show sl =
        "[" ++ show (start sl) ++ " --> " ++ show (end sl) ++ ")"

Show SeL4_BootInfo where
    show bi =
        "Node " ++ show (nodeID bi) ++ " of " ++ show (numNodes bi) ++ "\n" ++
        "IOPT levels:     " ++ show (numIOPTLevels bi) ++ "\n" ++
        "IPC buffer:      " ++ show (ipcBuffer bi) ++ "\n" ++
        "Empty slots:     " ++ show (empty bi) ++ "\n" ++
        "sharedFrames:    " ++ show (sharedFrames bi) ++ "\n" ++
        "userImageFrames: " ++ show (userImageFrames bi) ++ "\n" ++
        "userImagePaging: " ++ show (userImagePaging bi) ++ "\n" ++
        "untyped:         " ++ show (untyped bi) ++ "\n" ++
        "Initial thread domain: " ++ show (initThreadDomain bi) ++ "\n" ++
        "Initial thread cnode size: " ++ show (initThreadCNodeSizeBits bi) ++ "\n" ++
        "List of untypeds\n" ++
        "------------------\n" ++
        "Paddr    | Size   | Device\n" ++
        "unimplemented...\n"

-- A function to create a dummy BootInfo before reading the proper one from the system.
createDummyBootInfo : SeL4_BootInfo
createDummyBootInfo =
    MKSeL4_BootInfo
        0
        1
        2
        3
        4
        (MKSeL4_SlotRegion 5 6)
        (MKSeL4_SlotRegion 6 7)
        (MKSeL4_SlotRegion 8 9)
        (MKSeL4_SlotRegion 9 10)
        (MKSeL4_SlotRegion 10 11)
        (MKSeL4_SlotRegion 11 12)
        13
        14
        15
        (MKSeL4_SlotRegion 16 17)


text:
%!PS-Adobe-2.0 EPSF-1.2
%%Creator: idraw
%%DocumentFonts:
%%Pages: 1
%%BoundingBox: 13 401 559 475
%%EndComments

%%BeginIdrawPrologue
/arrowhead {
0 begin
transform originalCTM itransform
/taily exch def
/tailx exch def
transform originalCTM itransform
/tipy exch def
/tipx exch def
/dy tipy taily sub def
/dx tipx tailx sub def
/angle dx 0 ne dy 0 ne or { dy dx atan } { 90 } ifelse def
gsave
originalCTM setmatrix
tipx tipy translate
angle rotate
newpath
arrowHeight neg arrowWidth 2 div moveto
0 0 lineto
arrowHeight neg arrowWidth 2 div neg lineto
patternNone not {
originalCTM setmatrix
/padtip arrowHeight 2 exp 0.25 arrowWidth 2 exp mul add sqrt brushWidth mul
arrowWidth div def
/padtail brushWidth 2 div def
tipx tipy translate
angle rotate
padtip 0 translate
arrowHeight padtip add padtail add arrowHeight div dup scale
arrowheadpath
ifill
} if
brushNone not {
originalCTM setmatrix
tipx tipy translate
angle rotate
arrowheadpath
istroke
} if
grestore
end
} dup 0 9 dict put def

/arrowheadpath {
newpath
arrowHeight neg arrowWidth 2 div moveto
0 0 lineto
arrowHeight neg arrowWidth 2 div neg lineto
} def

/leftarrow {
0 begin
y exch get /taily exch def
x exch get /tailx exch def
y exch get /tipy exch def
x exch get /tipx exch def
brushLeftArrow { tipx tipy tailx taily arrowhead } if
end
} dup 0 4 dict put def

/rightarrow {
0 begin
y exch get /tipy exch def
x exch get /tipx exch def
y exch get /taily exch def
x exch get /tailx exch def
brushRightArrow { tipx tipy tailx taily arrowhead } if
end
} dup 0 4 dict put def

%%EndIdrawPrologue

/arrowHeight 11 def
/arrowWidth 5 def

/IdrawDict 50 dict def
IdrawDict begin

/none null def
/numGraphicParameters 17 def
/stringLimit 65535 def

/Begin {
save
numGraphicParameters dict begin
} def

/End {
end
restore
} def

/SetB {
dup type /nulltype eq {
pop
false /brushRightArrow idef
false /brushLeftArrow idef
true /brushNone idef
} {
/brushDashOffset idef
/brushDashArray idef
0 ne /brushRightArrow idef
0 ne /brushLeftArrow idef
/brushWidth idef
false /brushNone idef
} ifelse
} def

/SetCFg {
/fgblue idef
/fggreen idef
/fgred idef
} def

/SetCBg {
/bgblue idef
/bggreen idef
/bgred idef
} def

/SetF {
/printSize idef
/printFont idef
} def

/SetP {
dup type /nulltype eq {
pop true /patternNone idef
} {
dup -1 eq {
/patternGrayLevel idef
/patternString idef
} {
/patternGrayLevel idef
} ifelse
false /patternNone idef
} ifelse
} def

/BSpl {
0 begin
storexyn
newpath
n 1 gt {
0 0 0 0 0 0 1 1 true subspline
n 2 gt {
0 0 0 0 1 1 2 2 false subspline
1 1 n 3 sub {
/i exch def
i 1 sub dup i dup i 1 add dup i 2 add dup false subspline
} for
n 3 sub dup n 2 sub dup n 1 sub dup 2 copy false subspline
} if
n 2 sub dup n 1 sub dup 2 copy 2 copy false subspline
patternNone not brushLeftArrow not brushRightArrow not and and { ifill } if
brushNone not { istroke } if
0 0 1 1 leftarrow
n 2 sub dup n 1 sub dup rightarrow
} if
end
} dup 0 4 dict put def

/Circ {
newpath
0 360 arc
closepath
patternNone not { ifill } if
brushNone not { istroke } if
} def

/CBSpl {
0 begin
dup 2 gt {
storexyn
newpath
n 1 sub dup 0 0 1 1 2 2 true subspline
1 1 n 3 sub {
/i exch def
i 1 sub dup i dup i 1 add dup i 2 add dup false subspline
} for
n 3 sub dup n 2 sub dup n 1 sub dup 0 0 false subspline
n 2 sub dup n 1 sub dup 0 0 1 1 false subspline
patternNone not { ifill } if
brushNone not { istroke } if
} {
Poly
} ifelse
end
} dup 0 4 dict put def

/Elli {
0 begin
newpath
4 2 roll
translate
scale
0 0 1 0 360 arc
closepath
patternNone not { ifill } if
brushNone not { istroke } if
end
} dup 0 1 dict put def

/Line {
0 begin
2 storexyn
newpath
x 0 get y 0 get moveto
x 1 get y 1 get lineto
brushNone not { istroke } if
0 0 1 1 leftarrow
0 0 1 1 rightarrow
end
} dup 0 4 dict put def

/MLine {
0 begin
storexyn
newpath
n 1 gt {
x 0 get y 0 get moveto
1 1 n 1 sub {
/i exch def
x i get y i get lineto
} for
patternNone not brushLeftArrow not brushRightArrow not and and { ifill } if
brushNone not { istroke } if
0 0 1 1 leftarrow
n 2 sub dup n 1 sub dup rightarrow
} if
end
} dup 0 4 dict put def

/Poly {
3 1 roll
newpath
moveto
-1 add
{ lineto } repeat
closepath
patternNone not { ifill } if
brushNone not { istroke } if
} def

/Rect {
0 begin
/t exch def
/r exch def
/b exch def
/l exch def
newpath
l b moveto
l t lineto
r t lineto
r b lineto
closepath
patternNone not { ifill } if
brushNone not { istroke } if
end
} dup 0 4 dict put def

/Text {
ishow
} def

/idef {
dup where { pop pop pop } { exch def } ifelse
} def

/ifill {
0 begin
gsave
patternGrayLevel -1 ne {
fgred bgred fgred sub patternGrayLevel mul add
fggreen bggreen fggreen sub patternGrayLevel mul add
fgblue bgblue fgblue sub patternGrayLevel mul add setrgbcolor
eofill
} {
eoclip
originalCTM setmatrix
pathbbox /t exch def /r exch def /b exch def /l exch def
/w r l sub ceiling cvi def
/h t b sub ceiling cvi def
/imageByteWidth w 8 div ceiling cvi def
/imageHeight h def
bgred bggreen bgblue setrgbcolor
eofill
fgred fggreen fgblue setrgbcolor
w 0 gt h 0 gt and {
l w add b translate w neg h scale
w h true [w 0 0 h neg 0 h] { patternproc } imagemask
} if
} ifelse
grestore
end
} dup 0 8 dict put def

/istroke {
gsave
brushDashOffset -1 eq {
[] 0 setdash
1 setgray
} {
brushDashArray brushDashOffset setdash
fgred fggreen fgblue setrgbcolor
} ifelse
brushWidth setlinewidth
originalCTM setmatrix
stroke
grestore
} def

/ishow {
0 begin
gsave
fgred fggreen fgblue setrgbcolor
/fontDict printFont printSize scalefont dup setfont def
/descender fontDict begin 0 /FontBBox load 1 get FontMatrix end
transform exch pop def
/vertoffset 1 printSize sub descender sub def {
0 vertoffset moveto show
/vertoffset vertoffset printSize sub def
} forall
grestore
end
} dup 0 3 dict put def
/patternproc {
0 begin
/patternByteLength patternString length def
/patternHeight patternByteLength 8 mul sqrt cvi def
/patternWidth patternHeight def
/patternByteWidth patternWidth 8 idiv def
/imageByteMaxLength imageByteWidth imageHeight mul
stringLimit patternByteWidth sub min def
/imageMaxHeight imageByteMaxLength imageByteWidth idiv patternHeight idiv
patternHeight mul patternHeight max def
/imageHeight imageHeight imageMaxHeight sub store
/imageString imageByteWidth imageMaxHeight mul patternByteWidth add string def
0 1 imageMaxHeight 1 sub {
/y exch def
/patternRow y patternByteWidth mul patternByteLength mod def
/patternRowString patternString patternRow patternByteWidth getinterval def
/imageRow y imageByteWidth mul def
0 patternByteWidth imageByteWidth 1 sub {
/x exch def
imageString imageRow x add patternRowString putinterval
} for
} for
imageString
end
} dup 0 12 dict put def

/min {
dup 3 2 roll dup 4 3 roll lt { exch } if pop
} def

/max {
dup 3 2 roll dup 4 3 roll gt { exch } if pop
} def

/midpoint {
0 begin
/y1 exch def
/x1 exch def
/y0 exch def
/x0 exch def
x0 x1 add 2 div
y0 y1 add 2 div
end
} dup 0 4 dict put def

/thirdpoint {
0 begin
/y1 exch def
/x1 exch def
/y0 exch def
/x0 exch def
x0 2 mul x1 add 3 div
y0 2 mul y1 add 3 div
end
} dup 0 4 dict put def

/subspline {
0 begin
/movetoNeeded exch def
y exch get /y3 exch def
x exch get /x3 exch def
y exch get /y2 exch def
x exch get /x2 exch def
y exch get /y1 exch def
x exch get /x1 exch def
y exch get /y0 exch def
x exch get /x0 exch def
x1 y1 x2 y2 thirdpoint
/p1y exch def
/p1x exch def
x2 y2 x1 y1 thirdpoint
/p2y exch def
/p2x exch def
x1 y1 x0 y0 thirdpoint
p1x p1y midpoint
/p0y exch def
/p0x exch def
x2 y2 x3 y3 thirdpoint
p2x p2y midpoint
/p3y exch def
/p3x exch def
movetoNeeded { p0x p0y moveto } if
p1x p1y p2x p2y p3x p3y curveto
end
} dup 0 17 dict put def

/storexyn {
/n exch def
/y n array def
/x n array def
n 1 sub -1 0 {
/i exch def
y i 3 2 roll put
x i 3 2 roll put
} for
} def

/SSten {
fgred fggreen fgblue setrgbcolor
dup true exch 1 0 0 -1 0 6 -1 roll matrix astore
} def

/FSten {
dup 3 -1 roll dup 4 1 roll exch
newpath
0 0 moveto
dup 0 exch lineto
exch dup 3 1 roll exch lineto
0 lineto
closepath
bgred bggreen bgblue setrgbcolor
eofill
SSten
} def

/Rast {
exch dup 3 1 roll 1 0 0 -1 0 6 -1 roll matrix astore
} def

%%EndProlog

%I Idraw 13 Grid 8 8

%%Page: 1 1

Begin
%I b u
%I cfg u
%I cbg u
%I f u
%I p u
%I t
[ 0.770999 0 0 0.770999 0 0 ] concat
/originalCTM matrix currentmatrix def

Begin %I Elli
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg LtGray
0.762951 0.762951 0.762951 SetCBg
%I p
1 SetP
%I t
[ 0.383486 0 0 0.383486 5.31061 372.248 ] concat
%I
337 492 110 78 Elli
End

Begin %I Line
%I b 3855
2 0 0 [4 4 4 4] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.743234 0 0 0.743234 -103.713 95.1738 ] concat
%I
175 586 456 623 Line
%I 1
End

Begin %I Elli
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
%I p
1 SetP
%I t
[ 0.766506 0 0 0.766506 -48.9699 24.6608 ] concat
%I
99 660 8 8 Elli
End

Begin %I Elli
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
%I p
1 SetP
%I t
[ 0.371617 0 0 0.371617 149.17 396.372 ] concat
%I
230 435 16 16 Elli
End

Begin %I Line
%I b 65535
3 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg Black
0 0 0 SetCBg
none SetP %I p n
%I t
[ 0.484819 0 0 0.484819 85.3282 326.768 ] concat
%I
806 476 631 426 Line
%I 2
End

Begin %I Line
%I b 65535
3 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg Black
0 0 0 SetCBg
none SetP %I p n
%I t
[ 0.484819 0 0 0.484819 85.3282 326.768 ] concat
%I
376 420 583 422 Line
%I 2
End

Begin %I Elli
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg LtGray
0.762951 0.762951 0.762951 SetCBg
%I p
1 SetP
%I t
[ 0.383486 0 0 0.383486 246.024 372.491 ] concat
%I
337 492 110 78 Elli
End

Begin %I Elli
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
%I p
1 SetP
%I t
[ 0.766506 0 0 0.766506 191.743 24.9038 ] concat
%I
99 660 8 8 Elli
End

Begin %I Elli
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
%I p
1 SetP
%I t
[ 0.371617 0 0 0.371617 389.883 396.615 ] concat
%I
230 435 16 16 Elli
End

Begin %I BSpl
%I b 65535
3 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg Black
0 0 0 SetCBg
none SetP %I p n
%I t
[ 0.484819 0 0 0.484819 85.3282 326.768 ] concat
%I 4
579 422
604 422
623 424
643 430
4 BSpl
%I 2
End

Begin %I Line
%I b 3855
2 0 0 [4 4 4 4] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg Black
0 0 0 SetCBg
none SetP %I p n
%I t
[ 0.484819 0 0 0.484819 292.346 469.305 ] concat
%I
445 126 556 286 Line
%I 2
End

Begin %I Line
%I b 3855
2 0 0 [4 4 4 4] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg Black
0 0 0 SetCBg
none SetP %I p n
%I t
[ 0.484819 0 0 0.484819 292.346 469.305 ] concat
%I
739 290 875 183 Line
%I 2
End

Begin %I Line
%I b 65535
3 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg Black
0 0 0 SetCBg
none SetP %I p n
%I t
[ 0.484819 0 0 0.484819 292.346 326.768 ] concat
%I
875 478 699 542 Line
%I 2
End

Begin %I Line
%I b 65535
3 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg Black
0 0 0 SetCBg
none SetP %I p n
%I t
[ 0.484819 0 0 0.484819 292.346 326.768 ] concat
%I
446 419 607 528 Line
%I 2
End

Begin %I Elli
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg LtGray
0.762951 0.762951 0.762951 SetCBg
%I p
1 SetP
%I t
[ 0.383486 0 0 0.383486 486.738 372.734 ] concat
%I
337 492 110 78 Elli
End

Begin %I Elli
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
%I p
1 SetP
%I t
[ 0.766506 0 0 0.766506 432.457 25.1467 ] concat
%I
99 660 8 8 Elli
End

Begin %I Elli
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
%I p
1 SetP
%I t
[ 0.371617 0 0 0.371617 630.597 396.858 ] concat
%I
230 435 16 16 Elli
End

Begin %I BSpl
%I b 65535
3 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg Black
0 0 0 SetCBg
none SetP %I p n
%I t
[ 0.484819 0 0 0.484819 292.346 326.768 ] concat
%I 5
606 527
626 538
653 545
681 544
701 541
5 BSpl
%I 2
End

Begin %I Elli
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg Black
0 0 0 SetCBg
%I p
1 SetP
%I t
[ 0.511004 0 0 0.511004 511.439 270.139 ] concat
%I
99 660 8 8 Elli
End

Begin %I Elli
%I b 3855
2 0 0 [4 4 4 4] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg Black
0 0 0 SetCBg
%I p
1 SetP
%I t
[ 0.511004 0 0 0.511004 599.892 272.537 ] concat
%I
99 660 8 8 Elli
End

Begin %I Line
%I b 3855
2 0 0 [4 4 4 4] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg Black
0 0 0 SetCBg
none SetP %I p n
%I t
[ 0.484819 0 0 0.484819 292.346 469.305 ] concat
%I
557 284 739 290 Line
%I 2
End

End %I eop

showpage

%%Trailer

end


text:
module lib.Library1

import lib.Library2

export
salute : String
salute = "Hello, I'm library 1, and there is someone who wants to say something\n" ++ salute2


text:
import Data.Fin

data Vect : Nat -> Type -> Type where
  VNil : Vect 0 a
  VCons : a -> Vect n a -> Vect (S n) a

vecToList : Vect n a -> List a
vecToList VNil = []
vecToList (VCons x xs) = x :: (vecToList xs)

listToVec : (xs : List a) -> Vect (length xs) a
listToVec [] = VNil
listToVec (x :: xs) = VCons x (listToVec xs)

restN : (n : Fin) -> Type
restN FZ  = Nat
restN (FS FZ) = Nat -> Nat
restN _ = Nat -> Nat -> Nat

foo : (n : Fin) -> restN n
foo FZ = 0
foo (FS FZ) = \x => x + 1
foo _ = \x, y => x + y

max_stars_repo_name: shouya/thinking-dumps

max_issues_repo_name: shouya/thinking-dumps

max_forks_repo_name: shouya/thinking-dumps


text:
module Interfaces

%access public export

interface Updatable ty where
  -- TODO: update : u -> input -> u
  update : ty -> JS_IO ty

interface FrameRequest ty where
  requestFrame : ty -> (Double -> JS_IO ()) -> JS_IO ()


text:
module Main

import System

main : IO ()
main = do
    threadID <- fork $ do
        sleep 1
        putStrLn "Hello"
    threadWait threadID
    putStrLn "Goodbye"


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

record MyDPair a (p : a -> Type) where
  constructor MkMyDPair
  dfst : a
  dsnd : p dfst

record DVect a where
  constructor MkDVect
  test : Int
  {n : Nat}
  vec : Vect n a

record Person where
  constructor MkPerson
  name : String
  age, shoesize : Int
  some_fn : b -> b -- 'b' bound as an argument to MkPerson

testPair : MyDPair Nat (\n => Vect n Int)
testPair = MkMyDPair _ [1,2,3,4,5]

testDVect : DVect Int
testDVect = MkDVect 94 [1,2,3,4,5]

testPerson : Person
testPerson = MkPerson "Wowbagger" 1337 10 (\x => S x)


text:
module Elem

data Elem : a -> List a -> Type where
     Here : Elem x (x :: xs)
     There : Elem x xs -> Elem x (y :: xs)

elem_test : Elem 2 [1..4]
elem_test = There Here

isElem : DecEq a => (x : a) -> (xs : List a) -> Maybe (Elem x xs)
isElem x [] = Nothing
isElem x (y :: xs) = case decEq x y of
                          Yes Refl => Just Here
                          No contra => do p <- isElem x xs
                                          Just (There p)

max_stars_repo_name: idris-hackers/idris-demos

max_issues_repo_name: idris-hackers/idris-demos

max_forks_repo_name: idris-hackers/idris-demos


text:
module Flexidisc.OrdList.HereOrNot

import Flexidisc.Dec.IsYes
import Flexidisc.OrdList.Fresh
import Flexidisc.OrdList.Label
import Flexidisc.OrdList.Nub
import Flexidisc.OrdList.Row
import Flexidisc.OrdList.Sub
import Flexidisc.OrdList.Type

%default total

||| A proof that labels that are in both lists have the same values
public export
data HereOrNot : (xs, ys : OrdList k v o) -> Type where
  ||| It holds for two empty `OrdList`
  Empty : HereOrNot [] []
  ||| If an element of the first list is not in the second list, it holds
  Skip  : DecEq k => {xs : OrdList k v o} -> HereOrNot xs ys -> IsFresh l ys -> HereOrNot ((l, ty) :: xs) ys
  ||| If an element of the second list is not in the first list, it holds
  Extra : DecEq k => {xs : OrdList k v o} -> HereOrNot xs ys -> IsFresh l xs -> HereOrNot xs ((l, ty) :: ys)
  ||| If an element is in both list, the values should be the same
  Keep  : HereOrNot xs ys -> HereOrNot ((l, ty) :: xs) ((l, ty) :: ys)

export
toRow : HereOrNot [(k, v)] ys -> Maybe (OrdRow k v ys)
toRow (Skip compat fresh)  = Nothing
toRow (Extra compat fresh) = There <$> toRow compat
toRow (Keep compat)        = Just Here

%name HereOrNot compat, can, prf

export
toSub : HereOrNot xs ys -> Maybe (Sub xs ys)
toSub Empty                = Just Empty
toSub (Skip compat fresh)  = Nothing
toSub (Extra compat fresh) = map Skip $ toSub compat
toSub (Keep compat)        = map Keep $ toSub compat

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module Data.IORef

-- Implemented externally
-- e.g., in Scheme, passed around as a box
data Mut : Type -> Type where [external]

%extern prim__newIORef : forall a . a -> (1 x : %World) -> IORes (Mut a)
%extern prim__readIORef : forall a . Mut a -> (1 x : %World) -> IORes a
%extern prim__writeIORef : forall a . Mut a -> (1 val : a) -> (1 x : %World) -> IORes ()

export
data IORef : Type -> Type where
     MkRef : Mut a -> IORef a

export
newIORef : HasIO io => a -> io (IORef a)
newIORef val
    = do m <- primIO (prim__newIORef val)
         pure (MkRef m)

%inline
export
readIORef : HasIO io => IORef a -> io a
readIORef (MkRef m) = primIO (prim__readIORef m)

%inline
export
writeIORef : HasIO io => IORef a -> (1 val : a) -> io ()
writeIORef (MkRef m) val = primIO (prim__writeIORef m val)

export
modifyIORef : HasIO io => IORef a -> (a -> a) -> io ()
modifyIORef ref f
    = do val <- readIORef ref
         writeIORef ref (f val)


text:
||| mutable array
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module Data.Container.Mutable.Array

import Data.IOArray.Prims as Prim

import Decidable.Equality
import Data.Fin
import Data.So

%default total

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

||| IOArray0 is same to Data.IOArray.Prims.ArrayData. But it's type-safe
||| on index-access.
export
data IOArray0 : (capacity:Nat) -> Type -> Type where
  MkIOArray0 : Prim.ArrayData t -> IOArray0 (S ubound) t

export newIOArray0 : HasIO io => (capacity:Nat)
    -> {auto 0 capacity_isnt_zero: So (capacity /= 0)}
    -> t
    -> io (IOArray0 capacity t)
newIOArray0 c@(S _) x =
  pure $ MkIOArray0 !(primIO $ Prim.prim__newArray (cast c) x)

namespace Zero

  export %inline readIOArray : HasIO io => Fin c -> IOArray0 c t -> io t
  readIOArray i (MkIOArray0 xs)
    = primIO $ Prim.prim__arrayGet xs (cast $ finToNat i)

  export %inline writeIOArray : HasIO io => Fin c -> t -> IOArray0 c t -> io ()
  writeIOArray i x (MkIOArray0 xs)
    = primIO $ Prim.prim__arraySet xs (cast $ finToNat i) x

  namespace List

    export writeIOArray : HasIO io
        => {c:Nat} -> (from:Fin c) -> List t -> IOArray0 c t -> io ()
    writeIOArray _ [] _ = pure ()
    writeIOArray {c=c} i (x::xs) ys = do
      writeIOArray i x ys
      case natToFin (S $ finToNat i) c of
           Nothing => pure ()
           Just i' => writeIOArray i' xs ys

  export fromList : HasIO io
      => (xs:List t)
      -> io (Maybe (IOArray0 (length xs) t))
  fromList [] = pure Nothing
  fromList (x::xs) = do
    arr <- newIOArray0 (S $ length xs) x
    writeIOArray 0 xs arr
    pure $ Just arr

  export toList : HasIO io => {n:_} -> IOArray0 (S n) t -> io (List t)
  toList {n=n} xs = go last []
    where
      go : Fin (S n) -> List t -> io (List t)
      go i ys = do
        y <- readIOArray i xs
        case i of
             FZ    => pure  (y::ys)
             FS i' => assert_total $ go (weaken i') (y::ys)

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

||| IOArray has runtime boundary check
export
record IOArray t where
  constructor MkIOArray
  ub : Nat
  content : IOArray0 (S ub) t

export %inline ubound : IOArray t -> Nat
ubound xs = xs.ub

export %inline capacity : IOArray t -> Nat
capacity xs = S $ ubound xs

export capacity_is_ubound_plus1 : forall xs. (S (ubound xs)) = capacity xs
capacity_is_ubound_plus1 = Refl

export newIOArray : HasIO io
    => (capacity:Nat) -> {auto capacity_isnt_zero: So (capacity /= 0)}
    -> t
    -> io (IOArray t)
newIOArray capacity@(S u) x = pure $ MkIOArray u !(newIOArray0 capacity x)

namespace Fin
  export %inline readIOArray : HasIO io => (xs:IOArray t) -> Fin (S $ ubound xs) -> io t
  readIOArray xs i = pure $ !(readIOArray i xs.content)

  export %inline writeIOArray : HasIO io => (xs:IOArray t) -> Fin (S $ ubound xs) -> t -> io ()
  writeIOArray xs i x = writeIOArray i x xs.content

  export %inline restrict : (xs:IOArray t) -> Integer -> Fin (S $ ubound xs)
  restrict xs i = restrict (ubound xs) i

namespace Nat
  export readIOArray : HasIO io => Nat -> IOArray t -> io (Maybe t)
  readIOArray i xs with (integerToFin (cast i) (capacity xs))
    readIOArray i xs | Just i' = pure $ Just $ !(readIOArray i' xs.content)
    readIOArray i xs | Nothing = pure Nothing

  export writeIOArray : HasIO io => Nat -> t -> IOArray t -> io Bool
  writeIOArray i x xs with (integerToFin (cast i) (capacity xs))
    writeIOArray i x xs | Just i' = writeIOArray i' x xs.content >> pure True
    writeIOArray i x xs | Nothing = pure False

namespace List
  export fromList : HasIO io => List t -> io (Maybe (IOArray t))
  fromList [] = pure Nothing
  fromList (x::xs) = do
    arr <- newIOArray (S $ length xs) x
    writeIOArray arr 0 x
    pure $ Just arr

  export toList : HasIO io => IOArray t -> io (List t)
  toList xs = go last []
    where
      go : Fin (S $ ubound xs) -> List t -> io (List t)
      go i ys = do
        y <- readIOArray xs i
        case i of
             FZ    => pure  (y::ys)
             FS i' => assert_total $ go (weaken i') (y::ys)

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


text:
module Deriving.Eq

import Deriving.Utils
import Language.Reflection.Utils
import Debug.Trace

ifc : TTName
ifc = `{{Prelude.Interfaces.Eq}}

genClause : TTName -> Datatype -> (TTName, List CtorArg, Raw) -> Elab (FunClause Raw)
genClause fname dt (cname, ctorArgs, _) = do
  let NS (UN cnameStr) _ = cname
  let ctorArgs1 = map getFunArg ctorArgs
  renamed <- renameAll (argsExceptTyConArgs ctorArgs1 dt)
  let ctorArgs2 = (argsOfTyConArgs ctorArgs1 dt) ++ renamed
  tyParams <- makeTypeParametersFrom ifc $ argsOfTyConArgs ctorArgs1 dt
  let tyVars = tyParams ++ (argsExceptTyConArgs ctorArgs1 dt) ++ (argsExceptTyConArgs ctorArgs2 dt)
  -- (Ctor x y ...)
  let ctor1 = wrapWithParameters (Var cname) ctorArgs1
  let ctor2 = wrapWithParameters (Var cname) ctorArgs2
  -- (=) (Ctor x y ...) (Ctor x y ...)
  let funClause = wrapWithPatBind (RApp (RApp (wrapWithParameters (Var fname) tyParams) ctor1) ctor2) tyVars
  -- perhaps we should test if the arg isn't erased too
  let effectiveArgs1 = filter (\arg => (type arg) /= RType) ctorArgs1
  let effectiveArgs2 = filter (\arg => (type arg) /= RType) ctorArgs2
  let effectiveArgs1 = map (\arg => (findIndex (\t => (type arg) == (Var (name t))) ctorArgs1, arg)) effectiveArgs1
  let effectiveArgs2 = map (\arg => (findIndex (\t => (type arg) == (Var (name t))) ctorArgs2, arg)) effectiveArgs2
  -- = "Ctor" ++ " " ++ (show x) ++ " " ++ (show y) ...
  eqedArgs <- sequence $ map (\((i, arg1), (_, arg2)) => eqArg i tyParams arg1 arg2) (zip effectiveArgs1 effectiveArgs2)
  let funBody = foldr (\arg, acc => land arg acc) (Var `{{Prelude.Bool.True}}) eqedArgs
  let funBody = wrapWithPatBind funBody tyVars
  pure $ MkFunClause funClause funBody
where
  eqArg : Maybe Nat -> List FunArg -> FunArg -> FunArg -> Elab Raw
  eqArg i tyParams arg1 arg2 = do
    -- get the instance of `Show type`
    inst <- case findInstanceFor i tyParams dt of
        Just name => pure (Var name)
        Nothing   => lookupInstanceFor fname ifc (type arg1)
    -- `(==) type (instance of Show type) arg`
    pure (RApp (RApp (RApp (RApp (Var `{{Prelude.Interfaces.(==)}}) (type arg1)) inst) (Var (name arg1))) (Var (name arg2)))
  delay : Raw -> Raw
  delay t =
    (RApp (RApp (RApp (Var `{{Delay}}) (Var `{{LazyValue}})) (Var `{{Prelude.Bool.Bool}})) t)
  land : Raw -> Raw -> Raw
  land l r =
    let fand = (Var `{{Prelude.Bool.(&&)}}) in
    (RApp (RApp fand l) (delay r))

genEq : TTName -> Datatype -> List FunArg -> Elab TTName
genEq tname dt tyParams = do
  feq <- gensym $ (showFQN tname) ++ ".(==)"
  let feq = SN $ MethodN feq
  x <- gensym "x"
  y <- gensym "y"
  -- (==) : (x: name) -> (y: name) -> Bool
  let ty = tyParams ++ [MkFunArg x (resultType dt) Explicit NotErased, MkFunArg y (resultType dt) Explicit NotErased]
  let tyDecl = Declare feq ty (Var `{{Prelude.Bool.Bool}})
  clauses <- sequence $ map (genClause feq dt) $ constructors dt
  -- (==) _ _ = False
  let params = ty
  let defaultClause = MkFunClause (wrapWithPatBind (wrapWithParameters (Var feq) params) params) (wrapWithPatBind (Var `{{Prelude.Bool.False}}) params)
  let f = DefineFun feq (clauses ++ [defaultClause])
  declareType tyDecl
  defineFunction f
  pure feq

genNeq : TTName -> TTName -> Datatype -> List FunArg -> Elab TTName
genNeq tname feq dt tyParams = do
  fneq <- gensym $ (showFQN tname) ++ ".(/=)"
  let fneq = SN $ MethodN fneq
  x <- gensym "x"
  y <- gensym "y"
  -- (/=) : (x: name) -> (y: name) -> Bool
  let funParam = tyParams ++ [MkFunArg x (resultType dt) Explicit NotErased, MkFunArg y (resultType dt) Explicit NotErased]
  let ty = Declare fneq funParam (Var `{{Prelude.Bool.Bool}})
  -- (/=) x y =
  let clauseArg  = wrapWithPatBind (wrapWithParameters (Var feq) funParam) funParam
  -- = not (x == y)
  let clauseBody = wrapWithPatBind (RApp (Var `{{Prelude.Bool.not}}) (RApp (RApp (wrapWithParameters (Var feq) tyParams) (Var x)) (Var y))) funParam
  let clause = MkFunClause clauseArg clauseBody
  let f = DefineFun fneq [clause]
  declareType ty
  defineFunction f
  pure fneq

export
deriveEq : TTName -> Datatype -> Elab ()
deriveEq name dt = do
  let inst = SN $ ImplementationN ifc [showFQN name]
  tyParams <- makeTypeParameters ifc dt

  -- define (==)
  feq <- genEq name dt tyParams
  -- define (/==)
  fneq <- genNeq name feq dt tyParams

  -- get the constructor of Eq
  ctor <- lookupCtorExact ifc
  -- eqInst : Eq name
  let instTy = Declare inst tyParams (RApp (Var ifc) (resultType dt))
  let clauseArg = (Var inst)
  let clauseArg = wrapWithPatBind (wrapWithParameters clauseArg tyParams) tyParams
  let feq  = wrapWithParameters (Var feq) tyParams
  let fneq = wrapWithParameters (Var fneq) tyParams
  let clauseBody = RApp (RApp (RApp (Var ctor) (resultType dt)) feq) fneq
  let clauseBody = wrapWithPatBind clauseBody tyParams
  let instClause = MkFunClause clauseArg clauseBody
  let instF = DefineFun inst [instClause]
  declareType instTy
  defineFunction instF
  -- register the instance to the interface DB
  addImplementation ifc inst

max_stars_repo_name: KeenS/idris-deriving

max_issues_repo_name: KeenS/idris-deriving

max_forks_repo_name: KeenS/idris-deriving


text:
-- --------------------------------------------------------------- [ Queue.idr ]
-- Module    : Queue.idr
-- Copyright : (c) 2015,2016 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| A simple Queue made from two instances of `Stack`.
|||
||| An interesting exercise will be to redfine the Queue using two
||| Vectors such that properties of the Queue during a reversal can be
||| held.
module Data.Queue

-- TODO Make popQ and peekQ 'safe' using the magic of proofs
-- TODO Make popQ total

%access export
%default total

||| A Queue of items of type `ty`.
|||
||| @ty The type of elements in the queue.
data Queue : (ty : Type) -> Type where
  MkQ : List a -> List a -> Queue a

setQueue : List a -> List a -> Queue a
setQueue inq outq = MkQ inq outq

||| Create an empty queue
mkQueue : Queue ty
mkQueue = MkQ Nil Nil

||| Is the Queue empty.
isQEmpty : Queue a -> Bool
isQEmpty (MkQ inq outq) = isNil inq && isNil outq

||| Is the queue cons
isQCons : Queue a -> Bool
isQCons (MkQ inq outq) = isCons inq || isCons outq

||| Push an element onto the queue.
pushQ : a -> Queue a -> Queue a
pushQ e (MkQ inq outq) = MkQ (e::inq) outq

||| Initialise the queue with the given element.
initQ : ty -> Queue ty
initQ e = pushQ e $ mkQueue

||| Mass push a list of things onto the queue.
pushQThings : List a -> Queue a -> Queue a
pushQThings xs q = foldl (flip pushQ) q xs

||| Remove an element from the queue, returning the pair (head, tail)
||| @q The Q
partial
popQ : (q : Queue ty) -> {auto prf : isQCons q = True} ->  (ty, Queue ty)
popQ (MkQ Nil Nil) {prf=Refl} impossible
popQ (MkQ Nil [x])            = (x, MkQ Nil Nil)
popQ (MkQ (x :: xs) (y :: (z :: ys))) = (y, MkQ (x::xs) ys)
popQ (MkQ (x :: xs) Nil) = case (reverse (x::xs)) of
  (y::ys) => (y, MkQ Nil ys)
popQ (MkQ (x :: xs) [y]) = (y, MkQ Nil (reverse (x::xs)))
popQ (MkQ Nil (x :: (y :: xs))) = (x, MkQ Nil (y::xs))

||| See what is at the top of the Queue
|||
||| @q the Q
partial
peekQ : (q : Queue ty) -> {auto prf : isQCons q = True} -> ty
peekQ qu = fst $ popQ qu

||| Remove an element from the queue, returning the pair (head, tail)
||| @q The Q
partial
popQ' : (q : Queue ty) -> Maybe (ty, Queue ty)
popQ' (MkQ Nil Nil)  = Nothing
popQ' (MkQ inq xs)   with (xs)
  | Nil       = popQ' (MkQ Nil (reverse inq))
  | (x::outq) = Just (x, MkQ inq outq)

||| See what is at the top of the Queue
|||
||| @q the Q
peekQ' : (q : Queue ty) -> Maybe ty
peekQ' (MkQ Nil Nil)       = Nothing
peekQ' (MkQ inq (x::outq)) = Just x
peekQ' (MkQ inq Nil)       = head' (reverse inq)

clearQ : Queue a -> Queue a
clearQ _ = mkQueue

implementation Eq ty => Eq (Queue ty) where
  (==) (MkQ inx outx) (MkQ iny outy) = inx == iny && outx == outy

implementation Show ty => Show (Queue ty) where
  show (MkQ inq outq) = unwords ["[Q", show inq, show outq, "]"]
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


text:
import Control.Indexed

data State = One | Two | Three

data Transition : Type -> State -> State -> Type where
  Pure : (x : a) -> Transition a s s
  First : Transition () One Two
  Second : Transition () Two Three
  Third : Transition () Three One
  Bind : Transition a x y -> (a -> Transition b y z) -> Transition b x z

IndexedFunctor State State Transition where
  map f (Pure x)   = Pure (f x)
  map f First      = Bind First  (Pure . f)
  map f Second     = Bind Second (Pure . f)
  map f Third      = Bind Third  (Pure . f)
  map f (Bind x g) = Bind x (\x' => map f (g x'))

IndexedApplicative State Transition where
  pure = Pure
  ap (Pure f) x = map f x
  ap (Bind y f) x =
    Bind y $ \y' =>
      Bind (f y') $ \f' =>
        Bind x (\x' => Pure (f' x'))

IndexedMonad State Transition where
  bind = Bind

main : Transition () One One
main =
  do First
     Second
     Indexed.ignore $ Pure "hello"
     Third

max_stars_repo_name: mattpolzin/idris-indexed

max_issues_repo_name: mattpolzin/idris-indexed

max_forks_repo_name: mattpolzin/idris-indexed


text:
module Recordname

namespace Foo
  export
  record Name where
    constructor MkName
    foo : Int

  x : Name -> Int
  x = foo

test : Recordname.Foo.Name


text:
module Set

import public Data.AVL.Set

export
Ord a => Semigroup (Set a) where
  (<+>) = union

export
Ord a => Monoid (Set a) where
  neutral = empty

max_stars_repo_name: gpyh/idris-graph

max_issues_repo_name: gpyh/idris-graph

max_forks_repo_name: gpyh/idris-graph


text:
||| An example implementation for the Tolerance relation.

module Data.Nat.Order.Relation

import Control.Relation

Adjacent : (a, b : Nat) -> Type
Adjacent a b = Either (a = b) $ Either (a = S b) (b = S a)

Reflexive Nat Adjacent where
  reflexive = Left Refl

Symmetric Nat Adjacent where
  symmetric (Left x_eq_y) = Left $ sym x_eq_y
  symmetric (Right $  Left prf) = Right $ Right prf
  symmetric (Right $ Right prf) = Right $  Left prf

Tolerance Nat Adjacent where


text:
module Crypto.ECDH

import Crypto.Random
import Crypto.Curve.XCurves
import Crypto.Curve
import Data.Vect
import Utils.Misc
import Utils.Bytes

public export
interface ECDHCyclicGroup (0 a : Type) where
  Scalar : Type
  Element : Type
  diffie_hellman : Scalar -> Element -> Maybe (List Bits8)
  generate_key_pair : MonadRandom m => m (Scalar,Element)

  deserialize_pk : List Bits8 -> Maybe Element
  serialize_pk : Element -> List Bits8

public export
deserialize_then_dh : ECDHCyclicGroup dh => Scalar {a=dh} -> List Bits8 -> Maybe (List Bits8)
deserialize_then_dh sk pk = (deserialize_pk {a=dh} pk) >>= (diffie_hellman sk)

public export
data X25519_DH : Type where

public export
ECDHCyclicGroup X25519_DH where
  Scalar = Vect 32 Bits8
  Element = Vect 32 Bits8
  diffie_hellman sk pk = map toList (XCurves.mul x25519 sk pk)
  generate_key_pair = do
    sk <- random_bytes 32
    let Just pk = derive_public_key x25519 sk
    | Nothing => generate_key_pair {a=X25519_DH}
    pure (sk,pk)
  deserialize_pk content = exactLength 32 $ fromList content
  serialize_pk = toList

public export
data X448_DH : Type where

public export
ECDHCyclicGroup X448_DH where
  Scalar = Vect 56 Bits8
  Element = Vect 56 Bits8
  diffie_hellman sk pk = map toList (XCurves.mul x448 sk pk)
  generate_key_pair = do
    sk <- random_bytes 56
    let Just pk = derive_public_key x448 sk
    | Nothing => generate_key_pair {a=X448_DH}
    pure (sk,pk)
  deserialize_pk content = exactLength 56 $ fromList content
  serialize_pk = toList

public export
{p : _} -> Point p => ECDHCyclicGroup p where
  Scalar = Integer
  Element = p
  diffie_hellman sk pk =
    let (x, _) = to_affine $ mul sk pk
        bytes = divCeilNZ (bits {p=p}) 8 SIsNonZero
    in Just $ toList $ integer_to_be bytes x
  generate_key_pair = do
    sk <- uniform_random' 2 (order {p=p} - 1)
    let pk = mul sk $ generator {p=p}
    pure (sk,pk)
  deserialize_pk = decode {p=p}
  serialize_pk = encode {p=p}


text:
module Minecraft.Core.Univ.Level.Pos

%default total

public export
record Pos where
  constructor At
  {chunk : Bits64}
  x, y, z : Bits8

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
data Bool = True | False

data Li : (a : Type) -> Type where
  Ni : Li a
  Co : a -> Li a -> Li a

myprod : Li Type -> Type
myprod li = Int

t : Li Type -> Type
t li = Type

hej : (Li Type -> Type) -> Type
hej f = f (Co (Li Type) Ni)

-- data Cart : (a : Type) -> (b : Type) -> Type where
--   Mul : a -> b -> Cart a b

-- v : Cart Type Type
-- v = Mul Int Int

-- -- Prod : Li Type -> Cart a a
-- -- Prod (Co b (Co a nil)) = Mul a b
-- -- Prod : Li Type -> Type
-- -- Prod (Co a rest) = Mul a rest

-- -- data Top : Type where
-- --   qwer : Top

-- Prod : Li Type -> Type
-- Prod Ni = Type
-- Prod (Co q qs) = Mul q (Prod qs)

-- -- myid : (a : Type) -> a -> a
-- -- myid _ x = x

-- id2 : a -> a
-- id2 x = x

-- idid : {a : Type} -> a -> a
-- idid = id2

-- q : Type -> Type
-- q a = id2 (id2 a)

-- test : Type -> Type
-- test x = x

-- a : Type
-- a = test Int

-- b : Type
-- b = test Type

max_stars_repo_name: hjorthjort/IdrisToAgda

max_issues_repo_name: hjorthjort/IdrisToAgda

max_forks_repo_name: hjorthjort/IdrisToAgda


text:
module MsV

import Data.Fin

%default total
%access public export

||| Encode a rational number as a fraction of a numerator and a decremental
||| denominator, thereby structural eliminating the possible of division by
||| zero.
record Frac where
  constructor Fract
  numerat : Nat
  decrDen : Nat

Fraction : Nat -> (d : Nat) -> { auto prf : IsSucc d } -> Frac
Fraction k Z {prf=ItIsSucc} impossible
Fraction k (S j) = Fract k j

Num Frac where
  (Fract n d) + (Fract m e) =
    if d == e
    then Fract (n + m) d
    else
      let d' = S d in
      let e' = S e in
      Fraction (n * e' + m * d') (d' * e')

  (Fract n d) * (Fract m e) =
    let d' = S d in
    let e' = S e in
    Fraction (n * m) (d' * e')

  fromInteger x = Fraction (fromInteger x) 1

intDiv : Frac -> Nat
intDiv (Fract n d) = intDiv' d n d where
  intDiv' : Nat -> Nat -> Nat -> Nat
  intDiv' _ Z _ = Z
  intDiv' Z n _ = n
  intDiv' origD (S n) Z = S (intDiv' origD n origD)
  intDiv' origD (S n) (S d) = intDiv' origD n d

Digit : Type
Digit = Fin 10

||| Whether we are carrying a digit during addition
data Carry = CarryOne | CarryNone

natToDigit : Nat -> Maybe Digit
natToDigit n = natToFin n 10

||| Add two fins
addFins : Fin (S n) -> Fin (S m) -> Fin (S n + S m)
addFins {n} {m} FZ x = rewrite plusCommutative (S n) (S m) in weakenN (S n) x
addFins {n} {m} x FZ = weakenN (S m) x
addFins {n = (S _)} {m = (S _)} (FS x) y@(FS _) = FS $ addFins x y

checkForCarry : Fin 20 -> (Carry, Digit)
checkForCarry FZ = (CarryNone, 0)
checkForCarry (FS FZ) = (CarryNone, 1)
checkForCarry (FS (FS FZ)) = (CarryNone, 2)
checkForCarry (FS (FS (FS FZ))) = (CarryNone, 3)
checkForCarry (FS (FS (FS (FS FZ)))) = (CarryNone, 4)
checkForCarry (FS (FS (FS (FS (FS FZ))))) = (CarryNone, 5)
checkForCarry (FS (FS (FS (FS (FS (FS FZ)))))) = (CarryNone, 6)
checkForCarry (FS (FS (FS (FS (FS (FS (FS FZ))))))) = (CarryNone, 7)
checkForCarry (FS (FS (FS (FS (FS (FS (FS (FS FZ)))))))) = (CarryNone, 8)
checkForCarry (FS (FS (FS (FS (FS (FS (FS (FS (FS x))))))))) = (CarryNone, 9)
checkForCarry (FS (FS (FS (FS (FS (FS (FS (FS (FS (FS x)))))))))) = (CarryOne, x)

addDigits : Digit -> Digit -> (Carry, Digit)
addDigits x y = checkForCarry $ addFins x y

||| Enode a rational number as either a terminating or repeating decimal
record Dec where
  constructor Decimal
  integPart : Nat
  nonrepeat : List Digit
  repeating : List Digit

infixr 5 +++

(+++) : Dec -> Dec -> Dec

-- 0.25 + 0.^3^ = 0.58^3^

fracToDec : Frac -> Dec

decToFrac : Dec -> Frac

OneNinth : Frac
OneNinth = Fraction 1 9

EightNinths : Frac
EightNinths = Fraction 8 9

NineNinths : Frac
NineNinths = Fraction 9 9

One : Dec
One = Decimal 1 [] []

DotOnesRepeating : Dec
DotOnesRepeating = Decimal 0 [] [1]

DotEightsRepeating : Dec
DotEightsRepeating = Decimal 0 [] [8]

DotNinesRepeating : Dec
DotNinesRepeating = Decimal 0 [] [9]

lemma1 : fracToDec OneNinth = DotOnesRepeating

lemma8 : fracToDec EightNinths = DotEightsRepeating

lemmaAddFrac : OneNinth + EightNinths = NineNinths

lemmaAddDec : DotOnesRepeating +++ DotEightsRepeating = DotNinesRepeating

theoremFD : fracToDec NineNinths = DotNinesRepeating

theoremDF : decToFrac DotNinesRepeating = NineNinths

||| Are the two decimals different encodings of the same number?
iso : Dec -> Dec -> Bool

theorem : iso One DotNinesRepeating = True

max_stars_repo_name: Kazark/nineninths

max_issues_repo_name: Kazark/nineninths

max_forks_repo_name: Kazark/nineninths


text:
module Main

||| Calculate the average length of words in a string.
||| @str a string containing words separated by whitespace.
average : (str : String) -> Double
average str = let numWords = wordCount str
                  totalLength = sum (allLengths (words str)) in
                  cast totalLength / cast numWords
    where
        wordCount : String -> Nat
        wordCount str = length (words str)

        allLengths : List String -> List Nat
        allLengths strs = map length strs

showAverage : String -> String
showAverage str = "The average word length is: " ++
                    show (average str) ++ "\n"

main : IO ()
main = repl "Enter a string: " showAverage

max_stars_repo_name: DimaSamoz/idris-book

max_issues_repo_name: DimaSamoz/idris-book

max_forks_repo_name: DimaSamoz/idris-book


text:
import Data.Vect

{-myReverse : Vect n elem -> Vect n elem
myReverse [] = []
myReverse {n = S k} (x :: xs) = let result = myReverse xs ++ [x] in
                                    rewrite plusCommutative 1 k in result-}

{-myReverse : Vect n elem -> Vect n elem
myReverse [] = []
myReverse (x :: xs) = reverseProof (myReverse xs ++ [x])
  where
    reverseProof : Vect (len + 1) elem -> Vect (S len) elem
    reverseProof {len} result = rewrite plusCommutative 1 len in result-}

myAppend_nil : Vect m elem -> Vect (plus m 0) elem
myAppend_nil {m} xs = rewrite plusZeroRightNeutral m in xs

myAppend_xs : Vect (S (m + len)) elem -> Vect (plus m (S len)) elem
myAppend_xs {m} {len} xs = rewrite sym (plusSuccRightSucc m len) in xs

myAppend : Vect n elem -> Vect m elem -> Vect (m + n) elem
myAppend [] ys = myAppend_nil ys
myAppend (x :: xs) ys = myAppend_xs (x :: myAppend xs ys)

myPlusCommutes : (n : Nat) -> (m : Nat) -> n + m = m + n
myPlusCommutes Z m = sym (plusZeroRightNeutral m)
myPlusCommutes (S k) m = rewrite myPlusCommutes k m in plusSuccRightSucc m k

myReverse : Vect n a -> Vect n a
myReverse xs = reverse' [] xs
  where reverse' : Vect n a -> Vect m a -> Vect (n + m) a
        reverse' {n} acc [] = rewrite (plusZeroRightNeutral n) in acc
        reverse' {n} {m = S k} acc (x :: xs) =
          rewrite sym (plusSuccRightSucc n k) in (reverse' (x::acc) xs)


text:
data Tree elem = Empty
               | Node (Tree elem) elem (Tree elem)

Functor Tree where
  map func Empty = Empty
  map func (Node left e right)
    = Node (map func left)
           (func e)
           (map func right)

Foldable Tree where
  foldr func acc Empty = acc
  foldr func acc (Node left e right)
    = let leftfold = foldr func acc left
          rightfold = foldr func leftfold right in
          func e rightfold


text:
{------------------------------------------------------------------------------
    Example.idr
------------------------------------------------------------------------------}
|||  Example: creating a 3x3 BMP image and writing to `stdout`.
module Main

import Debug.Error

import Data.IOArray

import SimpleBmp

%default total

%language ElabReflection -- for Data.Error.error

-------------------------------------------------------------------------------
--  main                                                                     --
-------------------------------------------------------------------------------
||| Write example bitmap data to `stdout`.
main : IO ()
main = do
  bmp <- SimpleBmp.newBmp 3 3
  SimpleBmp.setPixel bmp 0 0 (255,0,0,255)
  SimpleBmp.setPixel bmp 0 1 (0,255,0,255)
  SimpleBmp.setPixel bmp 0 2 (0,0,255,255)
  SimpleBmp.setPixel bmp 1 0 (0,255,255,255)
  SimpleBmp.setPixel bmp 1 1 (255,0,255,255)
  SimpleBmp.setPixel bmp 1 2 (255,255,0,255)
  SimpleBmp.setPixel bmp 2 0 (255,255,255,255)
  SimpleBmp.setPixel bmp 2 1 (127,127,127,255)
  SimpleBmp.setPixel bmp 2 2 (0,0,0,255)
  Just () <- SimpleBmp.writeBmpToFile stdout bmp
    | Nothing => error "write bmp failed"
  pure ()

max_stars_repo_name: spearman/simple-bmp

max_issues_repo_name: spearman/simple-bmp

max_forks_repo_name: spearman/simple-bmp


text:
data Foo : Type where
 Fee : Main.foo


text:
{-
Implement the following function, which states that if you add the same value onto the front of
equal lists, the resulting lists are also equal:
 -}
same_cons : {xs : List a} -> {ys : List a} -> xs = ys -> x :: xs = x :: ys
same_cons prf = cong (x ::) prf

{-
Because this function represents an equality proof, it’s sufficient to know that your definition type-checks and is total:

*ex_8_1> :total same_cons
Main.same_cons is Total
 -}

same_lists : {xs : List a} -> {ys : List a} -> x = y -> xs = ys -> x :: xs = y :: ys
same_lists Refl prf = cong (x ::) prf

data ThreeEq : a -> b -> c -> Type where
     Same : (a : ty)  -> ThreeEq a a a

allSameS : (x, y, z : Nat) -> ThreeEq x y z -> ThreeEq (S x) (S y) (S z)
allSameS x x x (Same x) = Same (S x)


text:
import Aoc
import Data.Strings
import Data.SortedMap

band : Integer -> Integer -> Integer
band = prim__and_Integer

bor : Integer -> Integer -> Integer
bor = prim__or_Integer

bxor : Integer -> Integer -> Integer
bxor i j = cast $ prim__xor_Int (cast i) (cast j)

||| surrounded "[" "]" "[abcd]" == Just "abcd"
||| surrounded "[" "]" "[abc" == Nothing
surrounded : String -> String -> String -> Maybe String
surrounded l r s =
  let le = cast . length
  in if (l `isPrefixOf` s) && (r `isSuffixOf` s)
    then Just $ strSubstr (le l) (le s - le l - le r) s
    else Nothing

record Mask where
  constructor mkMask
  nonZeros : Integer
  ones : Integer
  floatXors : List Integer

mask0 : Mask
mask0 = mkMask 0 0 [0]

applyMask : Mask -> Integer -> Integer
applyMask m = bor m.ones . band m.nonZeros

applyMaskIndex : Mask -> Integer -> List Integer
applyMaskIndex m i = map (bxor (bor m.ones i)) m.floatXors

record State where
  constructor mkState
  mask : Mask
  memory : SortedMap Integer Integer

state0 : State
state0 = mkState mask0 empty

data Instruction = SetMask Mask | SetMem Integer Integer

parseMask : String -> Maybe Mask
parseMask = map (foldl go mask0) . traverse parseChar . unpack
  where
    data MaskChar = X | Zero | One
    parseChar : Char -> Maybe MaskChar
    parseChar 'X' = Just X
    parseChar '0' = Just Zero
    parseChar '1' = Just One
    parseChar _ = Nothing
    go : Mask -> MaskChar -> Mask
    go (mkMask nz o fx) X    = mkMask (2*nz+1) (2*o)   [2*x+i | x<-fx, i<-[0,1]]
    go (mkMask nz o fx) Zero = mkMask (2*nz)   (2*o)   (map (2*) fx)
    go (mkMask nz o fx) One  = mkMask (2*nz+1) (2*o+1) (map (2*) fx)

parseInstruction : String -> Maybe Instruction
parseInstruction s =
  case words s of
    ["mask","=",v] => SetMask <$> parseMask v
    [i,"=",v] => SetMem <$> (surrounded "mem[" "]" i >>= parseInteger) <*> parseInteger v
    _ => Nothing

runInstruction1 : State -> Instruction -> State
runInstruction1 s (SetMask m) = record { mask = m } s
runInstruction1 s (SetMem i v) =
  record { memory $= insert i (applyMask s.mask v) } s

runInstruction2 : State -> Instruction -> State
runInstruction2 s (SetMask m) = record { mask = m } s
runInstruction2 s (SetMem i v) =
  let js = applyMaskIndex s.mask i
      memory' = foldl (\m, j => insert j v m) s.memory js
  in record { memory = memory' } s

main : IO ()
main = do
  instructions <- parseLines parseInstruction
  let sumWith = (\f => sum $ .memory $ foldl f state0 instructions)
  putStr "*   "; printLn (sumWith runInstruction1)
  putStr "**  "; printLn (sumWith runInstruction2)


text:
import Data.Vect

{- 5 -}

sumEntries : Num a => (pos : Integer) -> Vect n a -> Vect n a -> Maybe a
sumEntries {n} pos xs ys = case integerToFin pos n of
                                Nothing => Nothing
                                Just idx => Just (index idx xs + index idx ys)

max_stars_repo_name: PiotrJander/TypeDD-Samples

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
module Generics.Newtype.Integral

import Generics.Newtype.Num

import Generics.Derive
%language ElabReflection

--------------------------------------------------------------------------------
--          Integral
--------------------------------------------------------------------------------

public export %hint
IntegralToNumNP : NP (Integral . f) ks -> NP (Num . f) ks
IntegralToNumNP = mapNP (\_ => materialize Num)

public export %hint
IntegralToNumPOP : POP (Integral . f) kss -> POP (Num . f) kss
IntegralToNumPOP = mapPOP (\_ => materialize Num)

-- Derivation of Integral for n-ary products or newtypes
-- e.g. `(a,b,c)` or `data Foo a = MkFoo a`  or  `data Foo = Foo Int`

-- n-ary products, e.g. (a,b,c)   (data Foo x y = MkFoo x y)
public export
NP (Integral . f) ks => Integral (NP f ks) where
  div = hcliftA2 (Integral . f) div
  mod = hcliftA2 (Integral . f) mod

-- This type of deriving is for newtypes so we restrict oursellves to single constructor types.
public export
(all : NP (Integral . f) [k']) => Integral (NS f [k']) where
  div {all = _::_} (Z x) (Z y) = Z $ div x y
  mod {all = _::_} (Z x) (Z y) = Z $ mod x y

public export
POP (Integral . f) kss => Integral (POP f kss) where
  div = hcliftA2 (Integral . f) div
  mod = hcliftA2 (Integral . f) mod

public export
POP (Integral . f) [ks] => Integral (SOP_ k f [ks]) where
  MkSOP x `div` MkSOP y = MkSOP $ div x y
  MkSOP x `mod` MkSOP y = MkSOP $ mod x y

export
genericDivIntegral : Generic t [code] => POP Integral [code] => t -> t -> t
genericDivIntegral x y = to $ div (from x) (from y)

export
genericMod : Generic t [code] => POP Integral [code] => t -> t -> t
genericMod x y = to $ mod (from x) (from y)

export
||| Derives a `Integral` implementation for the given data type
||| and visibility.
IntegralVis : Visibility -> DeriveUtil -> InterfaceImpl
IntegralVis vis g = MkInterfaceImpl "Integral" vis []
                       `(MkIntegral genericDivIntegral genericMod)
                       (implementationType `(Integral) g)

export
||| Alias for `EncodeVis Public`.
Integral : DeriveUtil -> InterfaceImpl
Integral = IntegralVis Public


text:
module Idris.ModTree

import Core.Binary
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Directory
import Core.Metadata
import Core.Options
import Core.Primitives
import Core.InitPrimitives
import Core.UnifyState

import Idris.Desugar
import Idris.Error
import Idris.Parser
import Idris.ProcessIdr
import Idris.REPL.Common
import Idris.Syntax
import Idris.Pretty

import Data.List
import Data.Either
import Data.String

import System
import System.Directory
import System.File

import Libraries.Data.StringMap
import Libraries.Data.String.Extra as Extra

import Debug.Trace

%default covering

record ModTree where
  constructor MkModTree
  nspace : ModuleIdent
  sourceFile : Maybe String
  deps : List ModTree

Show ModTree where
  show t = show (sourceFile t) ++ " " ++ show (nspace t) ++ "<-" ++ show (deps t)

-- A module file to build, and its list of dependencies
-- From this we can work out if the source file needs rebuilding, assuming
-- things are build in dependency order. A source file needs rebuilding
-- if:
--  + Its corresponding ttc is older than the source file
--  + Any of the import ttcs are *newer* than the corresponding ttc
--    (If so: also any imported ttc's fingerprint is different from the one
--    stored in the source file's ttc)
public export
record BuildMod where
  constructor MkBuildMod
  buildFile : String
  buildNS : ModuleIdent
  imports : List ModuleIdent

export
Show BuildMod where
  show t = buildFile t ++ " [" ++ showSep ", " (map show (imports t)) ++ "]"

data AllMods : Type where

mkModTree : {auto c : Ref Ctxt Defs} ->
            {auto o : Ref ROpts REPLOpts} ->
            {auto a : Ref AllMods (List (ModuleIdent, ModTree))} ->
            FC ->
            (done : List ModuleIdent) -> -- if 'mod' is here we have a cycle
            (modFP : Maybe FileName) -> -- Sometimes we know already know what the file name is
            (mod : ModuleIdent) ->      -- Otherwise we'll compute it from the module name
            Core ModTree
mkModTree loc done modFP mod
  = if mod `elem` done
       then throw (CyclicImports (done ++ [mod]))
       else
          -- Read imports from source file. If the source file isn't
          -- available, it's not our responsibility
          catch (do all <- get AllMods
                    -- If we've seen it before, reuse what we found
                    case lookup mod all of
                         Nothing =>
                           do file <- maybe (nsToSource loc mod) pure modFP
                              modInfo <- readHeader file mod
                              let imps = map path (imports modInfo)
                              ms <- traverse (mkModTree loc (mod :: done) Nothing) imps
                              let mt = MkModTree mod (Just file) ms
                              all <- get AllMods
                              put AllMods ((mod, mt) :: all)
                              pure mt
                         Just m => pure m)
                -- Couldn't find source, assume it's in a package directory
                (\err =>
                    case err of
                         CyclicImports _ => throw err
                         ParseFail _ => throw err
                         LexFail _ _ => throw err
                         LitFail _ => throw err
                         _ => pure (MkModTree mod Nothing []))

data DoneMod : Type where
data BuildOrder : Type where

-- Given a module tree, returns the modules in the reverse order they need to
-- be built, including their dependencies
mkBuildMods : {auto d : Ref DoneMod (StringMap ())} ->
              {auto o : Ref BuildOrder (List BuildMod)} ->
              ModTree -> Core ()
mkBuildMods mod
    = whenJust (sourceFile mod) $ \ sf =>
            do done <- get DoneMod
               case lookup sf done of
                    Just _ => pure ()
                    Nothing =>
                       do -- build dependencies
                          traverse_ mkBuildMods (deps mod)
                          -- build it now
                          bo <- get BuildOrder
                          put BuildOrder
                                (MkBuildMod sf (nspace mod)
                                            (map nspace (deps mod)) :: bo)
                          done <- get DoneMod
                          put DoneMod (insert sf () done)

-- Given a main file name, return the list of modules that need to be
-- built for that main file, in the order they need to be built
-- Return an empty list if it turns out it's in the 'done' list
export
getBuildMods : {auto c : Ref Ctxt Defs} ->
               {auto o : Ref ROpts REPLOpts} ->
               FC -> (done : List BuildMod) ->
               (mainFile : String) ->
               Core (List BuildMod)
getBuildMods loc done fname
    = do a <- newRef AllMods []
         fname_ns <- ctxtPathToNS fname
         if fname_ns `elem` map buildNS done
            then pure []
            else
              do t <- mkModTree {a} loc [] (Just fname) fname_ns
                 dm <- newRef DoneMod empty
                 o <- newRef BuildOrder []
                 mkBuildMods {d=dm} {o} t
                 pure (reverse !(get BuildOrder))

needsBuildingTime : (sourceFile : String) -> (ttcFile : String) ->
                    (depFiles : List String) -> Core Bool
needsBuildingTime sourceFile ttcFile depFiles
  = do ttcTime  <- modTime ttcFile
       srcTime  <- modTime sourceFile
       depTimes <- traverse modTime depFiles
       pure $ any (>= ttcTime) (srcTime :: depTimes)

checkTotalReq : {auto c : Ref Ctxt Defs} ->
                String -> String -> TotalReq -> Core Bool
checkTotalReq sourceFile ttcFile expected
  = catch (do log "totality.requirement" 20 $
                "Reading totalReq from " ++ ttcFile
              Just got <- readTotalReq ttcFile
                | Nothing => pure False
              log "totality.requirement" 20 $ unwords
                [ "Got", show got, "and expected", show expected ++ ":"
                , "we", ifThenElse (got < expected) "should" "shouldn't"
                , "rebuild" ]
              -- if what we got (i.e. what we used when we checked the file the
              -- first time around) was strictly less stringent than what we
              -- expect now then we need to rebuild.
              pure (got < expected))
          (\error => pure False)

checkDepHashes : {auto c : Ref Ctxt Defs} ->
                 String -> Core Bool
checkDepHashes depFileName
  = catch (do defs                   <- get Ctxt
              Just depCodeHash       <- hashFileWith (defs.options.hashFn) depFileName
                    | _ => pure False
              depTTCFileName         <- getTTCFileName depFileName "ttc"
              (Just depStoredCodeHash, _) <- readHashes depTTCFileName
                    | _ => pure False
              pure $ depCodeHash /= depStoredCodeHash)
          (\error => pure False)

||| Build from source if any of the dependencies, or the associated source file,
||| have been modified from the stored hashes.
needsBuildingHash : {auto c : Ref Ctxt Defs} ->
                    (sourceFile : String) -> (ttcFile : String) ->
                    (depFiles : List String) -> Core Bool
needsBuildingHash sourceFile ttcFile depFiles
  = do defs                <- get Ctxt
       -- If there's no hash available, either in the TTC or from the
       -- current source, then it needs building
       Just codeHash       <- hashFileWith (defs.options.hashFn) sourceFile
             | _ => pure True
       (Just storedCodeHash, _) <- readHashes ttcFile
             | _ => pure True
       depFilesHashDiffers <- any id <$> traverse checkDepHashes depFiles
       pure $ codeHash /= storedCodeHash || depFilesHashDiffers

export
needsBuilding :
  {auto c : Ref Ctxt Defs} ->
  {auto o : Ref ROpts REPLOpts} ->
  (sourceFile, ttcFile : String) -> List String -> Core Bool
needsBuilding sourceFile ttcFile depFiles
  = do -- if the ttc file does not exist there is no point in asking
       -- whether we need to rebuild it
       True <- coreLift $ exists ttcFile
         | False => pure True
       -- check if hash match
       False <- ifThenElse (checkHashesInsteadOfModTime !getSession)
                           needsBuildingHash
                           needsBuildingTime
                  sourceFile ttcFile depFiles
         | True => pure True

       log "import" 20 $ "Hashes still valid for " ++ sourceFile

       -- in case we're loading the main file, make sure the TTC is
       -- using the appropriate default totality requirement
       Just f <- mainfile <$> get ROpts
         | Nothing => pure False
       log "totality.requirement" 10 $ concat {t = List}
         [ "Checking totality requirement of "
         , sourceFile
         , " (main file is "
         , f
         , ")"
         ]
       let True = sourceFile == f
         | False => pure False
       True <- checkTotalReq sourceFile ttcFile !(totalReq <$> getSession)
         | False => pure False
       -- if it needs rebuilding then remove the buggy .ttc file to avoid going
       -- into an infinite loop!
       Right () <- coreLift $ removeFile ttcFile
         | Left err => throw (FileErr ttcFile err)
       pure True

buildMod : {auto c : Ref Ctxt Defs} ->
           {auto s : Ref Syn SyntaxInfo} ->
           {auto o : Ref ROpts REPLOpts} ->
           FC -> Nat -> Nat -> BuildMod ->
           Core (List Error)
buildMod loc num len mod
   = do clearCtxt; addPrimitives
        lazyActive True; setUnboundImplicits True

        let sourceFile = buildFile mod
        let modNamespace = buildNS mod
        ttcFile <- getTTCFileName sourceFile "ttc"
        -- We'd expect any errors in nsToPath to have been caught by now
        -- since the imports have been built! But we still have to check.
        depFilesE <- traverse (nsToPath loc) (imports mod)
        let (ferrs, depFiles) = partitionEithers depFilesE

        log "import" 20 $ unwords
          [ "Checking whether to rebuild "
          , sourceFile
          , "(" ++ ttcFile ++ ")"
          ]
        rebuild <- needsBuilding sourceFile ttcFile depFiles

        u <- newRef UST initUState
        m <- newRef MD (initMetadata (PhysicalIdrSrc modNamespace))
        put Syn initSyntax

        errs <- ifThenElse (not rebuild) (pure []) $
           do let pad = minus (length $ show len) (length $ show num)
              let msg : Doc IdrisAnn
                  = pretty (Extra.replicate pad ' ') <+> pretty num
                    <+> slash <+> pretty len <+> colon
                    <++> pretty "Building" <++> pretty mod.buildNS
                    <++> parens (pretty sourceFile)
              log "import.file" 10 $ "Processing " ++ sourceFile
              process {u} {m} msg sourceFile modNamespace

        defs <- get Ctxt
        ws <- emitWarningsAndErrors (if null errs then ferrs else errs)
        pure (ws ++ if null errs then ferrs else ferrs ++ errs)

export
buildMods : {auto c : Ref Ctxt Defs} ->
            {auto s : Ref Syn SyntaxInfo} ->
            {auto o : Ref ROpts REPLOpts} ->
            FC -> Nat -> Nat -> List BuildMod ->
            Core (List Error)
buildMods fc num len [] = pure []
buildMods fc num len (m :: ms)
    = case !(buildMod fc num len m) of
           [] => buildMods fc (1 + num) len ms
           errs => pure errs

export
buildDeps : {auto c : Ref Ctxt Defs} ->
            {auto s : Ref Syn SyntaxInfo} ->
            {auto m : Ref MD Metadata} ->
            {auto u : Ref UST UState} ->
            {auto o : Ref ROpts REPLOpts} ->
            (mainFile : String) ->
            Core (List Error)
buildDeps fname
    = do mods <- getBuildMods EmptyFC [] fname
         log "import" 20 $ "Needs to rebuild: " ++ show mods
         ok <- buildMods EmptyFC 1 (length mods) mods
         case ok of
              [] => do -- On success, reload the main ttc in a clean context
                       clearCtxt; addPrimitives
                       modIdent <- ctxtPathToNS fname
                       put MD (initMetadata (PhysicalIdrSrc modIdent))
                       mainttc <- getTTCFileName fname "ttc"
                       log "import" 10 $ "Reloading " ++ show mainttc ++ " from " ++ fname
                       readAsMain mainttc

                       -- Load the associated metadata for interactive editing
                       mainttm <- getTTCFileName fname "ttm"
                       log "import" 10 $ "Reloading " ++ show mainttm
                       readFromTTM mainttm
                       pure []
              errs => pure errs -- Error happened, give up

getAllBuildMods : {auto c : Ref Ctxt Defs} ->
                  {auto s : Ref Syn SyntaxInfo} ->
                  {auto o : Ref ROpts REPLOpts} ->
                  FC -> (done : List BuildMod) ->
                  (allFiles : List String) ->
                  Core (List BuildMod)
getAllBuildMods fc done [] = pure done
getAllBuildMods fc done (f :: fs)
    = do ms <- getBuildMods fc done f
         getAllBuildMods fc (ms ++ done) fs

export
buildAll : {auto c : Ref Ctxt Defs} ->
           {auto s : Ref Syn SyntaxInfo} ->
           {auto o : Ref ROpts REPLOpts} ->
           (allFiles : List String) ->
           Core (List Error)
buildAll allFiles
    = do mods <- getAllBuildMods EmptyFC [] allFiles
         -- There'll be duplicates, so if something is already built, drop it
         let mods' = dropLater mods
         buildMods EmptyFC 1 (length mods') mods'
  where
    dropLater : List BuildMod -> List BuildMod
    dropLater [] = []
    dropLater (b :: bs)
        = b :: dropLater (filter (\x => buildFile x /= buildFile b) bs)


text:
||| Why do we have to do this?
||| https://stackoverflow.com/q/51529100/834176
module ListExt

%default total
%access public export

splitOnL' : Eq a => (delim : List a)    -> {auto dprf : NonEmpty delim   }
              -> (matching : List a) -> {auto mprf : NonEmpty matching}
              -> List a -> (List a, List (List a))
splitOnL' _ _ [] = ([], [])
splitOnL' delim m@(_::m') list@(x::xs) =
  if isPrefixOf m list
  then
    case m' of
      [] => ([], uncurry (::) $ splitOnL' delim delim xs)
      (m_ :: ms) => splitOnL' delim (m_ :: ms) xs
  else
    let (l, ls) = splitOnL' delim delim xs in
    (x :: l, ls)

splitOnL : Eq a => (delim : List a) -> {auto dprf : NonEmpty delim}
             -> List a -> List (List a)
splitOnL delim [] = []
splitOnL delim list@(_::_) = uncurry (::) $ splitOnL' delim delim list

substitute : Eq a => List a -> List a -> List a -> List a
substitute [] replacement = id
substitute (n :: ns) replacement = intercalate replacement . splitOnL (n :: ns)

strReplace : String -> String -> String -> String
strReplace needle replacement = pack . substitute (unpack needle) (unpack replacement) . unpack

max_stars_repo_name: Kazark/fspp

max_issues_repo_name: Kazark/fspp

max_forks_repo_name: Kazark/fspp


text:
||| A replacement for Control.Linear.Network and use `Ptr`s instead of `String`s
module Extra.C.Network

import Control.Linear.LIO
import Extra.C.CPtr
import Extra.Proof
import Data.Nat
import Network.Socket
import Network.Socket.Raw
import public Network.Socket.Data

||| libc `send` in idris2
export
%foreign "C:send,libc"
prim__socket_send : SocketDescriptor -> (ptr : Ptr CUInt8) -> (nbytes : SizeT) -> (flags : Bits32) -> PrimIO SSizeT

||| libc `recv` in idris2
export
%foreign "C:recv,libc"
prim__socket_recv : SocketDescriptor -> (ptr : Ptr CUInt8) -> (nbytes : SizeT) -> (flags : Bits32) -> PrimIO SSizeT

||| `prim__socket_send` with higher level primitives in idris2
export
socket_send : HasIO io => Socket.Data.Socket -> (data_ptr : Ptr CUInt8) -> (data_size : SizeT) -> io SSizeT
socket_send sock ptr nbytes = do
  ret <- primIO $ prim__socket_send sock.descriptor ptr nbytes 0
  pure ret

||| `prim__socket_recv` with higher level primitives in idris2
export
socket_recv : HasIO io => Socket.Data.Socket -> (data_ret_ptr : Ptr CUInt8) -> SizeT -> io SSizeT
socket_recv sock ptr nbytes = do
  ret <- primIO $ prim__socket_recv sock.descriptor ptr nbytes 0
  pure ret

||| Assumed states of a socket. Keep in mind that unintentional tempering can fundamentally destroy the premise
public export
data SocketState = Ready | Bound | Listening | Open | Closed

||| Used to specify which states enables the socket be called with `connect`
public export
data CanConnect : SocketState -> Type where
  CanConnect_Ready : CanConnect Ready
  CanConnect_Bound : CanConnect Bound

||| Possible protocols of a socket, usually you use `Default`
public export
data Protocol : Type where
  TCP : Protocol
  UDP : Protocol
  Default : Protocol

||| An auxiliary function to convert Protocol into its corresponding magic number
export
protocolNumber : Protocol -> ProtocolNumber
protocolNumber Default = 0
protocolNumber TCP = 6
protocolNumber UDP = 17

||| The `Socket`, I don't expose the constructor in order to prevent incorrect usages
export
data Socket : SocketFamily -> SocketType -> Protocol -> SocketState -> Type where
     MkSocket : Socket.Data.Socket -> Socket family type protocol state

||| Construct a socket
export
newSocket
  : LinearIO io
  => (family  : SocketFamily)
  -> (type : SocketType)
  -> (protocol : Protocol)
  -> L io {use=1}
    ( Res (Maybe SocketError) (\case
      Just err => ()
      Nothing  => Socket family type protocol Ready
    ))
newSocket family type protocol = do
  Right sock <- socket family type (protocolNumber protocol)
    | Left err => pure1 $ Just err # ()
  pure1 $ Nothing # (MkSocket sock)

||| Close a socket, you may want to call `done` too to kill the socket
export
close : LinearIO io => (1 _ : Socket family type protocol state) -> L io {use=1} (Socket family type protocol Closed)
close (MkSocket sock) = do
  Socket.close sock
  pure1 (MkSocket sock)

||| Finish a socket
export
done : LinearIO io => (1 _ : Socket family type protocol Closed) -> L io ()
done (MkSocket sock) = pure ()

||| Bind a socket
export
bind
  : LinearIO io
  => (1 _ : Socket family type protocol Ready)
  -> (addr : Maybe SocketAddress)
  -> (port : Port)
  -> L io {use=1} (Res Bool (\res => Socket family type protocol (case res of {False => Closed; True => Bound})))
bind (MkSocket sock) addr port = do
  ok <- Socket.bind sock addr port
  pure1 $ ok == 0 # MkSocket sock

||| Connect a socket to an address
export
connect
  : LinearIO io
  => (1 _ : Socket family type protocol state)
  -> {auto 0 can_connect : CanConnect state}
  -> (addr : SocketAddress)
  -> (port : Port)
  -> L io {use=1} (Res Bool (\res => Socket family type protocol (case res of {False => Closed; True => Open})))
connect (MkSocket sock) addr port = do
  ok <- Socket.connect sock addr port
  pure1 $ ok == 0 # MkSocket sock

||| Put a socket into listen mode
export
listen :
  LinearIO io
  => (1 _ : Socket family type protocol Bound)
  -> L io {use=1} (Res Bool (\res => Socket family type protocol (case res of {False => Closed; True => Listening})))
listen (MkSocket sock) = do
  ok <- Socket.listen sock
  pure1 $ ok == 0 # MkSocket sock

||| Put a socket into accept mode and blocks until a client connects to it
export
accept :
  LinearIO io
  => (1 _ : Socket family type protocol Listening)
  -> L io {use=1} (Res Bool (\case
    False => Socket family type protocol Listening
    True => (LPair (Socket family type protocol Listening) (Socket family type protocol Open))))
accept (MkSocket sock) = do
  Right (sock', sockaddr) <- Socket.accept sock
    | Left err => pure1 (False # (MkSocket sock))
  pure1 $ True # (MkSocket sock # MkSocket sock')

-- TODO: handle return error
||| Send some data via a socket
export
send : (LinearIO io)
  => (1 sock : Socket family type protocol Open)
  -> {length : Nat}
  -> (1 _ : CPtr (Bytes can_free True can_write length))
  -> L io {use=1}
      ( LPair
        ( CPtr (Bytes can_free True can_write length)
        )
        ( Res Bool
          ( \case
            False => Socket family type protocol Closed
            True  => Socket family type protocol Open
          )
        )
      )
send (MkSocket sock) (MkCPtr ptr) = do
  _ <- liftIO1 $ socket_send sock ptr (cast $ natToInteger length)
  pure1 $ MkCPtr ptr # (True # MkSocket sock)

-- TODO: handle return error
||| Receive some data from a socket
export
recv
  : LinearIO io
  => (1 _ : Socket family type protocol Open)
  -> {max_length : Nat}
  -> (1 _ : CPtr (Bytes can_free can_read True max_length))
  -> L io {use=1}
       ( LPair
         ( CPtr (Bytes can_free can_read True max_length) )
         ( Res (Maybe (DPair Nat (\length => LTE length max_length))) ( \case
           Nothing => Socket family type protocol Closed
           Just _  => Socket family type protocol Open
         ))
       )
recv (MkSocket sock) (MkCPtr ptr) = do
  length <- socket_recv sock ptr (cast $ natToInteger max_length)
  let length = integerToNat (cast length)
  let cptr = MkCPtr ptr
  pure1 $ cptr # (Just (length ** believe_me ()) # MkSocket sock)

-- TODO: implement udp stuff

-- export
-- recvAll : LinearIO io =>
--           (1 _ : Socket Open) ->
--           L io {use=1} (Res (Maybe String)
--                             (\res => Socket (case res of
--                                                   Nothing => Closed
--                                                   Just msg => Open)))
-- recvAll (MkSocket sock)
--     = do Right msg <- Socket.recvAll sock
--              | Left err => pure1 (Nothing # MkSocket sock)
--          pure1 (Just msg # MkSocket sock)

-- recv : LinearIO io
--   => Socket family type protocol Open
--   -> Buffer
--   -> ByteLength
--   -> (on_fail    : (Socket family type protocol Closed) -> L io {use=1} ())
--   -> (on_success : (Socket family type protocol Open  ) -> L io () )
-- recv sock buf len = do
--   ptr <- sock_alloc len
--   recvBuf sock ptr len