text:
module Sat

import Data.List
import Data.Maybe
import Data.Strings

import Data.Linear.Array

import Control.Linear
import Control.Linear.LState

%default total

public export
data Var = MkVar Int
export
Show Var where
  show (MkVar n) = show n

export
Eq Var where
  (MkVar a) == (MkVar b) = a == b
export
Ord Var where
  compare (MkVar a) (MkVar b) = compare a b

public export
data Lit = MkPos Var | MkNeg Var
export
Show Lit where
  show (MkPos v) = " " ++ show v
  show (MkNeg v) = "~" ++ show v

isPos : Lit -> Bool
isPos (MkPos _) = True
isPos (MkNeg _) = False

getVar : Lit -> Var
getVar (MkPos v) = v
getVar (MkNeg v) = v

export
data Clause : Type where
  MkClause : (l : List Lit) -> {auto ok : NonEmpty l} -> Clause

export
toClause : (l : List Lit) -> {auto ok : NonEmpty l} -> Clause
toClause l {ok} = MkClause l {ok}

export
Show Clause where
  show (MkClause l) = show l

Watchlist : Type
Watchlist = LinArray (List Clause)

litIndex : Lit -> Int
litIndex (MkPos (MkVar n)) = 2 * n
litIndex (MkNeg (MkVar n)) = 2 * n + 1

initWatchlist : Int -> List Clause -> Watchlist
initWatchlist maxLit clauses = newArray maxLit (initWatchlist' clauses)
  where
    initWatchlist' : List Clause -> (1 a : Watchlist) -> Watchlist
    initWatchlist' [] a = a
    initWatchlist' (c@(MkClause ls {ok})::cs) a =
      let firstLit = head ls
          idx = litIndex firstLit
          (r # arr') = mread a idx in
          initWatchlist' cs $ write arr' idx (c::(fromMaybe [] r))

getWatched : Lit -> LState Watchlist (List Clause)
getWatched lit = do
  v <- run (\wl => mread wl (litIndex lit))
  pure $ fromMaybe [] v

removeWatches : Lit -> LState Watchlist ()
removeWatches lit = do
  change $ \wl => write wl (litIndex lit) []

addWatch : Lit -> Clause -> LState Watchlist ()
addWatch l c = do
  clauses <- getWatched l
  change $ \wl => write wl (litIndex l) (c::clauses)

addWatches : List (Lit, Clause) -> LState Watchlist ()
addWatches ls = traverse_ (uncurry addWatch) ls

Assignments : Type
Assignments = LinArray (Maybe Bool)

varIndex : Var -> Int
varIndex (MkVar n) = n

value : Var -> LState Assignments (Maybe Bool)
value var = do
  val <- run $ (\as => mread as (varIndex var))
  pure $ fromMaybe Nothing val

assign : Var -> Bool -> LState Assignments ()
assign var v = change (\as => write as (varIndex var) (Just v))

unassign : Var -> LState Assignments ()
unassign var = change (\as => write as (varIndex var) Nothing)

SolverState : Type -> Type
SolverState = LState (Watchlist, Assignments)

dumpAs' : Array arr => Int -> List (Var, Maybe Bool) -> arr (Maybe Bool) -> List (Var, Maybe Bool)
dumpAs' i s as =
  let sz = size as in
      if i >= sz then reverse s
                 else case read as i of
                           Nothing => dumpAs' (assert_smaller i (i+1)) ((MkVar i, Nothing)::s) as
                           Just e => dumpAs' (assert_smaller i (i+1)) ((MkVar i, e)::s) as

dumpArr : (1 _ : Assignments) -> List (Var, Maybe Bool)
dumpArr as = toIArray as (dumpAs' 0 [])

initAssignments : Int -> Assignments
initAssignments n = newArray n (initAssignments' (integerToNat $ cast n)) where
  initAssignments' : Nat -> (1 _ : Assignments) -> Assignments
  initAssignments' Z as = as
  initAssignments' (S n) as = write (initAssignments' n as) (cast n) Nothing

updateWatchlist : Lit -> SolverState Bool
updateWatchlist assignFalse = do
  needUpdate <- liftSt $ getWatched assignFalse
  case needUpdate of
       [] => pure True
       needUpdate => do
         (Just alts) <- liftSt $ lfoldlM findAlt (Just []) needUpdate
         | Nothing => pure False
         liftSt $ removeWatches assignFalse
         liftSt $ addWatches alts
         pure True

    where

  altOk : List Lit -> LState Assignments (Maybe Lit)
  altOk [] = pure Nothing
  altOk (l::ls) = case !(value (getVar l)) of
                         Just x => if x == isPos l then pure $ Just l
                                                   else altOk ls
                         Nothing => pure $ Just l

  findAlt : (Maybe (List (Lit, Clause))) -> (_ : Clause) -> LState Assignments (Maybe (List (Lit, Clause)))
  findAlt Nothing _ = pure Nothing
  findAlt (Just acc) (MkClause ls) = do
    (Just foundAlt) <- altOk ls
    | Nothing => pure Nothing
    pure $ Just ((foundAlt, MkClause ls)::acc)

mutual
  solveTry : Bool -> Var -> SolverState Bool
  solveTry a var = do
    liftSt $ assign var a
    ok <- updateWatchlist (if a then MkNeg var else MkPos var)
    if ok then pure True
          else do liftSt $ unassign var
                  pure False

  solve : List Var -> SolverState Bool
  solve [] = pure True
  solve (var::ds) = do
    tryValues [False, True]
    where
      tryValues : List Bool -> SolverState Bool
      tryValues [] = pure False
      tryValues (val::rest) = do
        couldBe <- solveTry val var
        if couldBe
           then do
             whenIsVal <- solve ds
             if whenIsVal then pure True
                          else do
                            liftSt $ unassign var
                            if val then pure False
                                   else tryValues rest
           else if val then pure False
           else tryValues rest

prepareAndSolve : Int -> List Clause -> SolverState Bool
prepareAndSolve numVars clauses = let vars = map MkVar [0 .. (numVars - 1)] in do
  let varsFreq = map countVarNew vars
  let mostFrequentVars = reverse $ sort varsFreq
  solve $ map snd mostFrequentVars
    where
      countInClause : Int -> Var -> List Lit -> Int
      countInClause acc v [] = acc
      countInClause acc v (MkPos cv::rest) = if cv == v then countInClause (acc+1) v rest
                                                        else countInClause acc v rest
      countInClause acc v (MkNeg cv::rest) = if cv == v then countInClause (acc+1) v rest
                                                        else countInClause acc v rest

      countVarNew : Var -> (Int, Var)
      countVarNew v = (sum $ map (\(MkClause ls) => countInClause 0 v ls) clauses, v)

      countVar : Var -> SolverState (Int, Var)
      countVar v = do watchingFalse <- liftSt $ getWatched (MkPos v)
                      watchingTrue <- liftSt $ getWatched (MkNeg v)
                      let count = the Int ((cast $ length watchingFalse) + (cast $ length watchingTrue))
                      pure (count, v)

export
sat : Int -> List Clause -> Maybe (List (Var, Bool))
sat numVars clauses =
  let wl = initWatchlist (2 * numVars) clauses
      as = initAssignments numVars
      (r # (wl', as')) = runLState (wl, as) (prepareAndSolve numVars clauses) in
      if r then traverse result (dumpArr as')
           else Nothing
  where
    result : (Var, Maybe Bool) -> Maybe (Var, Bool)
    result (v, Just a) = Just (v, a)
    result (_, Nothing) = Nothing


text:
import Data.Buffer

main : IO ()
main = do Just buf <- newBuffer 40
          printLn (size buf)
          setByte buf 5 42
          setString buf 20 "Hello world!"
          printLn !(bufferData buf)
          Just buf2 <- resizeBuffer buf 50
          putStrLn "Resized"
          printLn !(bufferData buf2)

          putStrLn "Writing to file"
          Right h <- openFile "test.buf" WriteTruncate
          writeBufferToFile h buf (size buf)
          closeFile h

          putStrLn "Reading from file twice"
          Just buf3 <- newBuffer 80

          Right h <- openFile "test.buf" Read
          buf3 <- readBufferFromFile h buf3 (size buf3)
          closeFile h

          Right h <- openFile "test.buf" Read
          readBufferFromFile h buf3 (size buf3)
          closeFile h

          printLn !(bufferData buf3)

          -- Small buffer, tests issue #3828
          Just small <- newBuffer 3
          setByte small 0 0
          setByte small 2 1

ext: idr

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module SimpleFFI

import public SimpleFFI.Spec
import public SimpleFFI.Renderer


text:
module India.Interpreter.AST

import India.Language.Core

import India.Union
import India.Wrapper

import Data.String

%default total

public export
record AST a where
  constructor MkAST
  content : String

export
Wrapper f => IndianCore f AST where
  content x    = MkAST $ "Content: \{show $ unwrap x}"
  paragraph xs = MkAST $ "Paragraph:" ++ (unlines $ map (("  " ++) . content) xs)

max_stars_repo_name: berewt/india

max_issues_repo_name: berewt/india

max_forks_repo_name: berewt/india


text:
module Stream.Util

import Data.Colist
import Data.SnocList
import Data.Vect
import Stream.Internal

public export
data Of : (v,r : Type) -> Type where
  MkOf : (val : v) -> Of v ()

public export
fromOf : Of a b -> a
fromOf (MkOf val) = val

--------------------------------------------------------------------------------
--          Producers
--------------------------------------------------------------------------------

export %inline
yield : a -> Stream (Of a) m ()
yield = yields . MkOf

export
list : List a -> Stream (Of a) m ()
list []        = pure ()
list (x :: xs) = yield x >> list xs

export
stream : Stream a -> Stream (Of a) m Void
stream (x :: y) = yield x >> stream y

export
colist : Colist a -> Stream (Of a) m ()
colist []       = pure ()
colist (x :: y) = yield x >> colist y

||| Generates the sequence (ini, f ini, f $ f ini, ...)
export
iterate : (fun : a -> a) -> (ini : a) -> Stream (Of a) m Void
iterate f ini = yield ini >> iterate f (f ini)

export
generate : (s -> (s,a)) -> s -> Stream (Of a) m Void
generate f ini = let (vs,va) = f ini in yield va >> generate f vs

export
tillRight : m (Either a r) -> Stream (Of a) m r
tillRight x = lift x >>= next
  where next : Either a r -> Stream (Of a) m r
        next (Left v)  = yield v >> tillRight x
        next (Right r) = pure r

--------------------------------------------------------------------------------
--          Consuming Streams
--------------------------------------------------------------------------------

export
mapM_ : (a -> m x) -> Stream (Of a) m r -> Stream Empty m r
mapM_ f y = case toView y of
  BindP val      w => pure val >>= \v => mapM_ f (w v)
  BindF (MkOf v) w => lift (f v) >>= \_ => mapM_ f (w ())
  BindM act      w => lift act >>= \v => mapM_ f (w v)
  VP val           => pure val
  VF (MkOf v)      => ignore $ lift (f v)
  VM act           => lift act

export %inline
effects : Applicative m => Stream (Of a) m r -> Stream Empty m r
effects = mapM_ (const $ pure ())

--------------------------------------------------------------------------------
--          Folds
--------------------------------------------------------------------------------

export
fold :  (x -> a -> x)
     -> x
     -> (x -> b)
     -> Stream (Of a) m r
     -> Stream Empty m (b,r)
fold step ini done x = case toView x of
  BindP val      z => pure val >>= \v => fold step ini done (z v)
  BindF (MkOf v) z => pure () >> fold step (step ini v) done (z ())
  BindM act      z => lift act >>= \v => fold step ini done (z v)
  VP val           => pure (done ini, val)
  VF (MkOf v)      => pure (done $ step ini v, ())
  VM act           => (done ini,) <$> lift act

export %inline
fold_ :  (x -> a -> x)
      -> x
      -> (x -> b)
      -> Stream (Of a) m r
      -> Stream Empty m b
fold_ step ini done = map fst . fold step ini done

export %inline
foldMap : Monoid mo => (a -> mo) -> Stream (Of a) m r -> Stream Empty m (mo,r)
foldMap f = fold (\vmo,va => vmo <+> f va) neutral id

export %inline
foldMap_ : Monoid mo => (a -> mo) -> Stream (Of a) m r -> Stream Empty m mo
foldMap_ f = map fst . foldMap f

export %inline
sum : Num a => Stream (Of a) m r -> Stream Empty m (a,r)
sum = fold (+) 0 id

export %inline
sum_ : Num a => Stream (Of a) m r -> Stream Empty m a
sum_ = map fst . sum

export %inline
product : Num a => Stream (Of a) m r -> Stream Empty m (a,r)
product = fold (*) 0 id

export %inline
product_ : Num a => Stream (Of a) m r -> Stream Empty m a
product_ = map fst . product

export %inline
length : Stream (Of a) m r -> Stream Empty m (Nat,r)
length = fold (\x,_ => S x) 0 id

export %inline
length_ : Stream (Of a) m r -> Stream Empty m Nat
length_ = map fst . length

export %inline
count : (a -> Bool) -> Stream (Of a) m r -> Stream Empty m (Nat,r)
count p = fold (\x,va => if p va then S x else x) 0 id

export %inline
count_ : (a -> Bool) -> Stream (Of a) m r -> Stream Empty m Nat
count_ p = map fst . count p

export %inline
first : Stream (Of a) m r -> Stream Empty m (Maybe a,r)
first = fold (\acc,va => acc <|> Just va) Nothing id

export %inline
first_ : Stream (Of a) m r -> Stream Empty m (Maybe a)
first_ = map fst . first

export %inline
last : Stream (Of a) m r -> Stream Empty m (Maybe a,r)
last = fold (\_,va => Just va) Nothing id

export %inline
last_ : Stream (Of a) m r -> Stream Empty m (Maybe a)
last_ = map fst . last

export %inline
minimum : Ord a => Stream (Of a) m r -> Stream Empty m (Maybe a,r)
minimum = fold (\acc,va => map (min va) acc <|> Just va) Nothing id

export %inline
minimum_ : Ord a => Stream (Of a) m r -> Stream Empty m (Maybe a)
minimum_ = map fst . minimum

export %inline
maximum : Ord a => Stream (Of a) m r -> Stream Empty m (Maybe a,r)
maximum = fold (\acc,va => map (max va) acc <|> Just va) Nothing id

export %inline
maximum_ : Ord a => Stream (Of a) m r -> Stream Empty m (Maybe a)
maximum_ = map fst . maximum

export %inline
all : (a -> Bool) -> Stream (Of a) m r -> Stream Empty m (Bool,r)
all p = fold (\acc,va => acc && p va) True id

export %inline
all_ : (a -> Bool) -> Stream (Of a) m r -> Stream Empty m Bool
all_ p = map fst . all p

export %inline
any : (a -> Bool) -> Stream (Of a) m r -> Stream Empty m (Bool,r)
any p = fold (\acc,va => acc || p va) False id

export %inline
any_ : (a -> Bool) -> Stream (Of a) m r -> Stream Empty m Bool
any_ p = map fst . any p

export %inline
elem : Eq a => a -> Stream (Of a) m r -> Stream Empty m (Bool, r)
elem va = any (va ==)

export %inline
elem_ : Eq a => a -> Stream (Of a) m r -> Stream Empty m Bool
elem_ va = map fst . elem va

export %inline
toSnocList : Stream (Of a) m r -> Stream Empty m (SnocList a, r)
toSnocList = fold (:<) Lin id

export %inline
toSnocList_ : Stream (Of a) m r -> Stream Empty m (SnocList a)
toSnocList_ = map fst . toSnocList

export %inline
toList : Stream (Of a) m r -> Stream Empty m (List a, r)
toList = map (\(sx,vr) => (sx <>> Nil, vr)) . toSnocList

export %inline
toList_ : Stream (Of a) m r -> Stream Empty m (List a)
toList_ = map fst . toList

export
foldM :  (x -> a -> m x)
      -> m x
      -> (x -> m b)
      -> Stream (Of a) m r
      -> Stream Empty m (b,r)
foldM step ini done x = case toView x of
  BindF (MkOf v) z => do
    vx <- lift ini
    foldM step (step vx v) done (z ())

  BindP val      z => pure val >>= \v => foldM step ini done (z v)
  BindM act      z => lift act >>= \v => foldM step ini done (z v)

  VP val        => do
    vx <- lift ini
    vb <- lift (done vx)
    pure (vb, val)

  VF (MkOf v)   => do
    vx  <- lift ini
    vx2 <- lift (step vx v)
    vb  <- lift (done vx2)
    pure (vb,())

  VM act        => do
    vr <- lift act
    vx <- lift ini
    vb <- lift (done vx)
    pure (vb, vr)

export
scan :  (x -> a -> x)
     -> x
     -> (x -> b)
     -> Stream (Of a) m r
     -> Stream (Of b) m r
scan step ini done str = yield (done ini) >>= \_ => go ini str
  where go : x -> Stream (Of a) m r -> Stream (Of b) m r
        go vx s = case toView s of
          BindF (MkOf v) z =>
            let vx2 = step vx v
             in yield (done vx2) >> go vx2 (z ())
          BindP val      z => pure val >>= \v => go vx (z v)
          BindM act      z => lift act >>= \v => go vx (z v)
          VP val           => pure val
          VF (MkOf v)      => yield (done $ step vx v)
          VM act           => lift act

--------------------------------------------------------------------------------
--          Filters and Stream Transformers
--------------------------------------------------------------------------------

export
for : Stream (Of a) m r -> (a -> Stream f m x) -> Stream f m r
for str fun = case toView str of
  BindF (MkOf va) z => fun va   >>= \_ => for (z ()) fun
  BindP val       z => pure val >>= \v => for (z v) fun
  BindM act       z => lift act >>= \v => for (z v) fun
  VF (MkOf va)      => ignore $ fun va
  VP val            => pure val
  VM act            => lift act

export
mapVals : (a -> b) -> Stream (Of a) m r -> Stream (Of b) m r
mapVals f str = for str (yield . f)

export %inline
castVals : Cast from to => Stream (Of from) m r -> Stream (Of to) m r
castVals = mapVals cast

export
mapValsM : (a -> m b) -> Stream (Of a) m r -> Stream (Of b) m r
mapValsM f str = for str $ \va => lift (f va) >>= yield

export
drain : Stream (Of a) m r -> Stream (Of a) m r
drain str = for str (\_ => pure ())

export %inline
with_ : Stream (Of a) m r -> (a -> f x) -> Stream f m r
with_ str fun = for str (yields . fun)

export %inline
subst : (a -> f x) -> Stream (Of a) m r -> Stream f m r
subst fun str = for str (yields . fun)

export
filter : (a -> Bool) -> Stream (Of a) m r -> Stream (Of a) m r
filter p x = case toView x of
  BindF (MkOf val) z =>
    if p val
       then yield val >> filter p (z ())
       else pure ()   >> filter p (z ())
  BindP val z    => pure val >>= \v => filter p (z v)
  BindM act z    => lift act >>= \v => filter p (z v)
  VP val         => pure val
  VF (MkOf v)    => if p v then yield v else pure ()
  VM act         => lift act

export
mapMaybe : (a -> Maybe b) -> Stream (Of a) m r -> Stream (Of b) m r
mapMaybe f x = case toView x of
  BindF (MkOf val) z => case f val of
    Just vb => yield vb >> mapMaybe f (z ())
    Nothing => pure ()  >> mapMaybe f (z ())
  BindP val z    => pure val >>= \v => mapMaybe f (z v)
  BindM act z    => lift act >>= \v => mapMaybe f (z v)
  VF (MkOf v)    => case f v of
    Just vb => yield vb
    Nothing => pure ()
  VP val         => pure val
  VM act         => lift act

export
span :  (a -> Bool)
     -> Stream (Of a) m r
     -> Stream (Of a) m (Stream (Of a) m r)
span p x = case toView x of
  BindF (MkOf val) z =>
    if p val
       then pure (yield val >> z ())
       else yield val >> span p (z ())
  BindP val z => pure val >>= \v => span p (z v)
  BindM act z => lift act >>= \v => span p (z v)
  VP val      => pure (pure val)
  VF (MkOf v) => if p v then pure (yield v) else yield v >> (pure $ pure ())
  VM act      => pure $ lift act

export %inline
takeUntil : (a -> Bool) -> Stream (Of a) m r -> Stream (Of a) m ()
takeUntil p = ignore . span p

export %inline
takeWhile : (a -> Bool) -> Stream (Of a) m r -> Stream (Of a) m ()
takeWhile p = takeUntil (not . p)

export
dropUntil : (a -> Bool) -> Stream (Of a) m r -> Stream (Of a) m r
dropUntil p str = drain (span p str) >>= id

export
dropWhile : (a -> Bool) -> Stream (Of a) m r -> Stream (Of a) m r
dropWhile p = dropUntil (not . p)

export
drop : Nat -> Stream (Of a) m r -> Stream (Of a) m r
drop n str = drain (splitsAt n str) >>= id

export
slidingWindow :  (n : Nat)
              -> {auto 0 prf : IsSucc n}
              -> Stream (Of a) m r
              -> Stream (Of $ Vect n a) m r
slidingWindow (S k) =
  mapMaybe sequence .
  scan (\prev,va => Just va :: init prev) (replicate (S k) Nothing) id

export
breakWith :  (a -> Maybe (a,a))
          -> Stream (Of a) m r
          -> Stream (Of a) m (Stream (Of a) m r)
breakWith f x = case toView x of
  BindF (MkOf y) g => case f y of
    Just (yh,yt) => yield yh >>= \v => pure (yield yt >>= \_ => g v)
    Nothing      => yield y >>= \v => breakWith f (g v)
  BindP y g => pure y >>= \v => breakWith f (g v)
  BindM y g => lift y >>= \v => breakWith f (g v)
  VF (MkOf y) => case f y of
    Just (yh,yt) => yield yh >> pure (yield yt)
    Nothing      => yield y  >> pure (pure ())
  VP y => pure (pure y)
  VM y => pure (lift y)

export
splitWith :  (a -> Maybe (a,a))
          -> Stream (Of a) m r
          -> Stream (Stream (Of a) m) m r
splitWith f s = F (breakWith f s) >>=
  \case P r => P r
        M y => M y
        x   => splitWith f x


text:
-- --------------------------------------------------------- [ Readability.idr ]
-- Module    : Readability.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]

module Readability

import public Readability.WordTypes
import public Readability.Stats
import public Readability.Metrics

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

max_stars_repo_name: jfdm/idris-read

max_issues_repo_name: jfdm/idris-read

max_forks_repo_name: jfdm/idris-read


text:
module Data.SortedMap

import Data.SortedMap.Dependent

%hide Prelude.toList

export
record SortedMap k v where
  constructor M
  unM : SortedDMap k $ const v

-- Helper function
unDPair : (x : a ** const b x) -> (a, b)
unDPair (k ** v) = (k, v)

export
empty : Ord k => SortedMap k v
empty = M empty

export
lookup : k -> SortedMap k v -> Maybe v
lookup k = map snd . lookup k . unM

export
insert : k -> v -> SortedMap k v -> SortedMap k v
insert k v = M . insert k v . unM

export
singleton : Ord k => k -> v -> SortedMap k v
singleton = M .: singleton

export
insertFrom : Foldable f => f (k, v) -> SortedMap k v -> SortedMap k v
insertFrom = flip $ foldl $ flip $ uncurry insert

export
delete : k -> SortedMap k v -> SortedMap k v
delete k = M . delete k . unM

export
fromList : Ord k => List (k, v) -> SortedMap k v
fromList = flip insertFrom empty

export
toList : SortedMap k v -> List (k, v)
toList = map unDPair . toList . unM

||| Gets the keys of the map.
export
keys : SortedMap k v -> List k
keys = map fst . toList

||| Gets the values of the map. Could contain duplicates.
export
values : SortedMap k v -> List v
values = map snd . toList

export
implementation Functor (SortedMap k) where
  map f = M . map f . unM

export
implementation Foldable (SortedMap k) where
  foldr f z = foldr f z . values
  foldl f z = foldl f z . values

  null = delay . null . unM

  foldMap f = foldMap f . values

export
implementation Traversable (SortedMap k) where
  traverse f = map M . traverse f . unM

||| Merge two maps. When encountering duplicate keys, using a function to combine the values.
||| Uses the ordering of the first map given.
export
mergeWith : (v -> v -> v) -> SortedMap k v -> SortedMap k v -> SortedMap k v
mergeWith f x y = insertFrom inserted x where
  inserted : List (k, v)
  inserted = do
    (k, v) <- toList y
    let v' = (maybe id f $ lookup k x) v
    pure (k, v')

||| Merge two maps using the Semigroup (and by extension, Monoid) operation.
||| Uses mergeWith internally, so the ordering of the left map is kept.
export
merge : Semigroup v => SortedMap k v -> SortedMap k v -> SortedMap k v
merge = mergeWith (<+>)

||| Left-biased merge, also keeps the ordering specified  by the left map.
export
mergeLeft : SortedMap k v -> SortedMap k v -> SortedMap k v
mergeLeft = mergeWith const

||| looks up a key in map, returning the left and right closest values, so that
|||  k1 <= k < k2. If at the end of the beginning and/or end of the sorted map, returns
||| nothing appropriately
export
lookupBetween : key -> SortedMap key val -> (Maybe (key,val), Maybe (key,val))
lookupBetween k = bimap (map unDPair) (map unDPair) . lookupBetween k . unM

||| Returns the leftmost (least) key and value
export
leftMost : SortedMap key val -> Maybe (key,val)
leftMost = map unDPair . leftMost . unM

||| Returns the rightmost (greatest) key and value
export
rightMost : SortedMap key val -> Maybe (key,val)
rightMost = map unDPair . rightMost . unM

export
(Show k, Show v) => Show (SortedMap k v) where
   show m = "fromList " ++ (show $ toList m)

export
(Eq k, Eq v) => Eq (SortedMap k v) where
  (==) = (==) `on` toList

-- TODO: is this the right variant of merge to use for this? I think it is, but
-- I could also see the advantages of using `mergeLeft`. The current approach is
-- strictly more powerful I believe, because `mergeLeft` can be emulated with
-- the `First` monoid. However, this does require more code to do the same
-- thing.
export
Semigroup v => Semigroup (SortedMap k v) where
  (<+>) = merge

||| For `neutral <+> y`, y is rebuilt in `Ord k`, so this is not a "strict" Monoid.
||| However, semantically, it should be equal.
export
(Ord k, Semigroup v) => Monoid (SortedMap k v) where
  neutral = empty


text:
module Data.Binary

import Data.Nat.Properties
import Data.Binary.Digit
import Syntax.PreorderReasoning

%default total

||| Bin represents binary numbers right-to-left.
||| For instance `4` can be represented as `OOI`.
||| Note that representations are not unique: one may append arbitrarily
||| many Os to the right of the representation without changing the meaning.
public export
Bin : Type
Bin = List Digit

||| Conversion from lists of bits to natural number.
public export
toNat : Bin -> Nat
toNat = foldr (\ b, acc => toNat b + 2 * acc) 0

||| Successor function on binary numbers.
||| Amortised constant time.
public export
suc : Bin -> Bin
suc [] = [I]
suc (O :: bs) = I :: bs
suc (I :: bs) = O :: (suc bs)

||| Correctness proof of `suc` with respect to the semantics in terms of Nat
export
sucCorrect : {bs : Bin} -> toNat (suc bs) === S (toNat bs)
sucCorrect {bs = []} = Refl
sucCorrect {bs = O :: bs} = Refl
sucCorrect {bs = I :: bs} = Calc $
  |~ toNat (suc (I :: bs))
  ~~ toNat (O :: suc bs) ...( Refl )
  ~~ 2 * toNat (suc bs)  ...( Refl )
  ~~ 2 * S (toNat bs)    ...( cong (2 *) sucCorrect )
  ~~ 2 + 2 * toNat bs    ...( unfoldDoubleS )
  ~~ S (toNat (I :: bs)) ...( Refl )


text:
module Replica.RunEnv

%default total

public export
record RunEnv where
  constructor MkRunEnv
  interactive : Bool
  path : String

max_stars_repo_name: xvw/REPLica

max_issues_repo_name: xvw/REPLica

max_forks_repo_name: xvw/REPLica


text:
module biswajitnag.Odds

import Evens

import Intro

-- Define an inductive type family IsOdd : Nat -> Type such that IsOdd n is inhabited if and only if n is odd.

data IsOdd : Nat -> Type where
  OneOdd : IsOdd 1
  SSOdd : (n: Nat) -> IsOdd n -> IsOdd ( S ( S ( n ) ) )

-- Show that 3 is odd.

Q2: IsOdd 3
Q2 = SSOdd 1 OneOdd

-- Show that 2 is not odd.

Q3: IsOdd 2 -> Void
Q3 (SSOdd Z OneOdd) impossible
Q3 (SSOdd Z (SSOdd _ _)) impossible

-- Show that if n: Nat is odd, then its successor S n is even.

Q4: (n: Nat) -> IsOdd n -> IsEven (S n)
Q4 (S Z) OneOdd = SSEven Z ZEven
Q4 (S (S n)) (SSOdd n x) = SSEven (S n) (Q4 n x)

-- Show that if n: Nat is even, then its successor S n is odd.

Q5: (n: Nat) -> IsEven n -> IsOdd (S n)
Q5 Z ZEven = OneOdd
Q5 (S (S n)) (SSEven n x) = SSOdd (S n) (Q5 n x)

-- Show that every number n : Nat is either even or odd.

Q6: (n: Nat) -> Either (IsEven n) (IsOdd n)
Q6 Z = Left ZEven
Q6 (S k) = case (Q6 k) of
                (Left l) => Right (Q5 k l)
                (Right r) => Left (Q4 k r)

-- Show that no number n: Nat is both even and odd.

Q7: (n: Nat) -> IsEven n -> IsOdd n -> Void
Q7 Z ZEven OneOdd impossible
Q7 Z ZEven (SSOdd _ _) impossible
Q7 (S (S k)) (SSEven k x) (SSOdd k y) = Q7 k x y

-- Show that if n: Nat and m: Nat are odd, then add n m is even (here add is from the intro).

Q8: (n: Nat) -> IsOdd n -> (m: Nat) -> IsOdd m -> IsEven (add n m)
Q8 (S Z) OneOdd m y = Q4 m y
Q8 (S (S k)) (SSOdd k x) m y = SSEven (add k m) (Q8 k x m y)

-- Show that if n: Nat is odd, then there exists m: Nat such that n = S (double m).

apNat : (f: Nat -> Nat) -> (n: Nat) -> (m: Nat) -> n = m -> f n = f m
apNat f m m Refl = Refl

Q9: (n: Nat) -> IsOdd n -> (m: Nat ** n = S (double m))
Q9 (S Z) OneOdd = (Z ** Refl)
Q9 (S (S k)) (SSOdd k x) = case (Q9 k x) of
                                (m ** y) => ((S m) ** (apNat (\n: Nat => (S (S n))) k (S(double m)) y))


text:
import System.FFI

libsmall : String -> String
libsmall fn = "C:" ++ fn ++ ",libsmallc"

Point : Type
Point = Struct "point" [("x", Int), ("y", Int)]

%foreign (libsmall "mkPoint")
mkPoint : Int -> Int -> Point

%foreign (libsmall "freePoint")
prim__freePoint : Point -> PrimIO ()

freePoint : Point -> IO ()
freePoint p = primIO $ prim__freePoint p

showPoint : Point -> String
showPoint pt
    = let x : Int = getField pt "x"
          y : Int = getField pt "y" in
          show (x, y)

main : IO ()
main
    = do let pt = mkPoint 20 30
         setField pt "x" (the Int 40)
         putStrLn $ showPoint pt
         freePoint pt


text:
{------------------------------------------------------------------------------
    SimpleArray.idr
------------------------------------------------------------------------------}

||| A simple mutable array type built on `Data.IOArray`.

module SimpleArray

import Data.IOArray

%default total

||| A wrapper around `Data.IOArray` that also stores the number of elements in
||| the array.
public export
record SimpleArray (elem : Type) where
  constructor MkSimpleArray
  inner : IOArray elem
  size  : Int

||| Creates a new `SimpleArray` of the given size with all elements initialized
||| to the given default value.
export
new : Int -> elem -> IO (SimpleArray elem)
new n e = do
  inner <- newArray n e
  pure $ MkSimpleArray inner n

||| get an element from the array; yields `Nothing` if index is negative or
||| larger than the array size.
export
get : SimpleArray elem -> Int -> IO (Maybe elem)
get array@(MkSimpleArray inner size) i =
  pure $ if size <= i then Nothing else Just !(unsafeReadArray inner i)

||| Write a value into the array, yielding `Nothing` if the index is negative
||| or larger than the array size.
export
put : SimpleArray elem -> Int -> elem -> IO (Maybe ())
put array@(MkSimpleArray inner size) i e =
  pure $ if size <= i then Nothing else Just !(unsafeWriteArray inner i e)

||| Map a function over the given array, creating a new array holding the
||| results.
export
map : Monoid b => (a -> b) -> SimpleArray a -> IO (SimpleArray b)
map f array@(MkSimpleArray from size) = do
  to <- newArray size neutral
  for (take (toNat size) $ iterate (+1) 0) (\i => do
    e <- unsafeReadArray from i
    unsafeWriteArray to i $ f e
  )
  pure $ MkSimpleArray to size

||| Map an IO function over the given array, creating a new array holding the
||| results.
export
mapIO : Monoid b => (a -> IO b) -> SimpleArray a -> IO (SimpleArray b)
mapIO f array@(MkSimpleArray from size) = do
  to <- newArray size neutral
  for (take (toNat size) $ iterate (+1) 0) (\i => do
    e <- unsafeReadArray from i
    unsafeWriteArray to i $ !(f e)
  )
  pure $ MkSimpleArray to size

||| Map a function over the given array, writing the result values directly
||| into the array.
export
mapInplace : (elem -> elem) -> SimpleArray elem -> IO (SimpleArray elem)
mapInplace f array@(MkSimpleArray inner size) = do
  for (take (toNat size) $ iterate (+1) 0) (\i => do
    e <- unsafeReadArray inner i
    unsafeWriteArray inner i $ f e
  )
  pure array

||| Fill array elements with result of applying the given function to each
||| element index.
export
fromIndex : SimpleArray elem -> (Int -> elem) -> IO (SimpleArray elem)
fromIndex array@(MkSimpleArray inner size) f = do
  for (take (toNat size) $ iterate (+1) 0) (\i => do
    unsafeWriteArray inner i $ f i
  )
  pure array

||| Check if a given element is contained in this array.
export
covering
contains : Eq elem => SimpleArray elem -> elem -> IO Bool
contains (MkSimpleArray inner size) e = rec 0 where
  covering
  rec : Int -> IO Bool
  rec i = if i == size then pure False else
    if e == !(unsafeReadArray inner i) then pure True else rec (i+1)

||| Array contents on a single line.
export
show : Show elem => SimpleArray elem -> IO String
show (MkSimpleArray inner size) = do
  elems <- for (take (toNat size) $ iterate (+1) 0) (\i =>
    pure $ show !(unsafeReadArray inner i)
      ++ if i < (size - 1) then "," else ""
  )
  pure $ "[" ++ (concat elems) ++ "]"

||| Array contents with a single element per line.
export
showPretty : Show elem => SimpleArray elem -> IO String
showPretty (MkSimpleArray inner size) = do
  elems <- for (take (toNat size) $ iterate (+1) 0) (\i =>
    pure $ show !(unsafeReadArray inner i)
      ++ if i < (size - 1) then ",\n  " else "\n"
  )
  pure $ "[\n  " ++ (concat elems) ++ "]"

export
covering
test : IO ()
test = do
  array <- new 5 9
  putStrLn !(show array)
  putStrLn $ "contains  9: " ++ show !(contains array  9)
  putStrLn $ "contains 10: " ++ show !(contains array 10)
  _ <- fromIndex array (\i => i * 3)
  putStrLn !(show array)
  _ <- mapInplace (+1) array
  putStrLn !(show array)
  _ <- mapInplace (*2) array
  putStrLn !(showPretty array)

max_stars_repo_name: spearman/simple-array

max_issues_repo_name: spearman/simple-array

max_forks_repo_name: spearman/simple-array


text:
%default total

data F : Type where
  MkFix : ((0 g : Type -> Type) -> g === Not -> g F) -> F

yesF : Not F -> F
yesF nf = MkFix (\ g, Refl => nf)

notF : Not F
notF (MkFix f) =
  let g = f Not Refl in
  g (yesF g)

argh : Void
argh = notF (yesF notF)


text:
module Core.Binary.Prims

import Core.Context.Context
import Core.Core

import Data.Buffer
import Data.List
import Data.List.Elem
import Data.List1
import Data.Nat
import Data.String
import Data.Vect

import Libraries.Data.PosMap
import public Libraries.Utils.Binary
import public Libraries.Utils.String

import System.Info
import System.File

-- A label for binary states
export
data Bin : Type where

-- A label for storing resolved name ids
export
data ResID : Type where

public export
interface TTC a where -- TTC = TT intermediate code/interface file
  -- Add binary data representing the value to the given buffer
  toBuf : Ref Bin Binary -> a -> Core ()
  -- Return the data representing a thing of type 'a' from the given buffer.
  -- Throws if the data can't be parsed as an 'a'
  fromBuf : Ref Bin Binary -> Core a

-- Create a new list of chunks, initialised with one 64k chunk
export
initBinary : Core (Ref Bin Binary)
initBinary
    = do Just buf <- coreLift $ newBuffer blockSize
             | Nothing => throw (InternalError "Buffer creation failed")
         newRef Bin (newBinary buf blockSize)

export
initBinaryS : Int -> Core (Ref Bin Binary)
initBinaryS s
    = do Just buf <- coreLift $ newBuffer s
             | Nothing => throw (InternalError "Buffer creation failed")
         newRef Bin (newBinary buf s)

extendBinary : Int -> Binary -> Core Binary
extendBinary need (MkBin buf l s u)
    = do let newsize = s * 2
         let s' = if (newsize - l) < need
                     then newsize + need
                     else newsize
         Just buf' <- coreLift $ resizeBuffer buf s'
             | Nothing => throw (InternalError "Buffer expansion failed")
         pure (MkBin buf' l s' u)

export
corrupt : String -> Core a
corrupt ty = throw (TTCError (Corrupt ty))

-- tag and getTag assume the Int is in the range 0-255 (we don't have
-- Bits8 yet!)
export
tag : {auto b : Ref Bin Binary} -> Int -> Core ()
tag {b} val
    = do chunk <- get Bin
         if avail chunk >= 1
            then
              do coreLift $ setByte (buf chunk) (loc chunk) val
                 put Bin (appended 1 chunk)
            else do chunk' <- extendBinary 1 chunk
                    coreLift $ setByte (buf chunk') (loc chunk') val
                    put Bin (appended 1 chunk')

export
getTag : {auto b : Ref Bin Binary} -> Core Int
getTag {b}
    = do chunk <- get Bin
         if toRead chunk >= 1
            then
              do val <- coreLift $ getByte (buf chunk) (loc chunk)
                 put Bin (incLoc 1 chunk)
                 pure val
              else throw (TTCError (EndOfBuffer "Byte"))

-- Primitives; these are the only things that have to deal with growing
-- the buffer list

-- Some useful types from the prelude

export
[Wasteful] TTC Int where
  toBuf b val
    = do chunk <- get Bin
         if avail chunk >= 8
            then
              do coreLift $ setInt (buf chunk) (loc chunk) val
                 put Bin (appended 8 chunk)
            else do chunk' <- extendBinary 8 chunk
                    coreLift $ setInt (buf chunk') (loc chunk') val
                    put Bin (appended 8 chunk')

  fromBuf b
    = do chunk <- get Bin
         if toRead chunk >= 8
            then
              do val <- coreLift $ getInt (buf chunk) (loc chunk)
                 put Bin (incLoc 8 chunk)
                 pure val
              else throw (TTCError (EndOfBuffer ("Int " ++ show (loc chunk, size chunk))))

export
TTC Int where
  toBuf b val
    = if val >= -127 && val < 128
         then tag (val + 127)
         else do tag 255
                 chunk <- get Bin
                 if avail chunk >= 8
                    then
                      do coreLift $ setInt (buf chunk) (loc chunk) val
                         put Bin (appended 8 chunk)
                    else do chunk' <- extendBinary 8 chunk
                            coreLift $ setInt (buf chunk') (loc chunk') val
                            put Bin (appended 8 chunk')

  fromBuf b
    = case !getTag of
           255 => do chunk <- get Bin
                     if toRead chunk >= 8
                       then
                         do val <- coreLift $ getInt (buf chunk) (loc chunk)
                            put Bin (incLoc 8 chunk)
                            pure val
                       else throw (TTCError (EndOfBuffer ("Int " ++ show (loc chunk, size chunk))))
           t => pure (t - 127)

export
TTC String where
  toBuf b val
      -- To support UTF-8 strings, this has to get the length of the string
      -- in bytes, not the length in characters.
      = do let req = stringByteLength val
           toBuf b req
           chunk <- get Bin
           if avail chunk >= req
              then
                do coreLift $ setString (buf chunk) (loc chunk) val
                   put Bin (appended req chunk)
              else do chunk' <- extendBinary req chunk
                      coreLift $ setString (buf chunk') (loc chunk') val
                      put Bin (appended req chunk')

  fromBuf b
      = do len <- fromBuf {a = Int} b
           chunk <- get Bin
           when (len < 0) $ corrupt "String"
           if toRead chunk >= len
              then
                do val <- coreLift $ getString (buf chunk) (loc chunk) len
                   put Bin (incLoc len chunk)
                   pure val
              else throw (TTCError (EndOfBuffer ("String length " ++ show len ++
                                                 " at " ++ show (loc chunk))))

export
TTC Binary where
  toBuf b val
    = do let len = used val
         toBuf b len
         chunk <- get Bin
         if avail chunk >= len
            then
              do coreLift $ copyData (buf val) 0 len
                                     (buf chunk) (loc chunk)
                 put Bin (appended len chunk)
            else do chunk' <- extendBinary len chunk
                    coreLift $ copyData (buf val) 0 len
                                        (buf chunk') (loc chunk')
                    put Bin (appended len chunk')

  fromBuf b
    = do len <- fromBuf b
         chunk <- get Bin
         if toRead chunk >= len
            then
              do Just newbuf <- coreLift $ newBuffer len
                      | Nothing => corrupt "Binary"
                 coreLift $ copyData (buf chunk) (loc chunk) len
                                     newbuf 0
                 put Bin (incLoc len chunk)
                 pure (MkBin newbuf 0 len len)
            else throw (TTCError (EndOfBuffer "Binary"))

export
TTC Bool where
  toBuf b False = tag 0
  toBuf b True = tag 1
  fromBuf b
      = case !getTag of
             0 => pure False
             1 => pure True
             _ => corrupt "Bool"

export
TTC Char where
  toBuf b c = toBuf b (cast {to=Int} c)
  fromBuf b
      = do i <- fromBuf b
           pure (cast {from=Int} i)

export
TTC Double where
  toBuf b val
    = do chunk <- get Bin
         if avail chunk >= 8
            then
              do coreLift $ setDouble (buf chunk) (loc chunk) val
                 put Bin (appended 8 chunk)
            else do chunk' <- extendBinary 8 chunk
                    coreLift $ setDouble (buf chunk') (loc chunk') val
                    put Bin (appended 8 chunk')

  fromBuf b
    = do chunk <- get Bin
         if toRead chunk >= 8
            then
              do val <- coreLift $ getDouble (buf chunk) (loc chunk)
                 put Bin (incLoc 8 chunk)
                 pure val
              else throw (TTCError (EndOfBuffer "Double"))

export
(TTC a, TTC b) => TTC (a, b) where
  toBuf b (x, y)
     = do toBuf b x
          toBuf b y
  fromBuf b
     = do x <- fromBuf b
          y <- fromBuf b
          pure (x, y)

export
TTC () where
  toBuf b () = pure ()
  fromBuf b = pure ()

export
(TTC a, {y : a} -> TTC (p y)) => TTC (DPair a p) where
  toBuf b (vs ** tm)
      = do toBuf b vs
           toBuf b tm

  fromBuf b
      = do x <- fromBuf b
           p <- fromBuf b
           pure (x ** p)

export
TTC a => TTC (Maybe a) where
  toBuf b Nothing
     = tag 0
  toBuf b (Just val)
     = do tag 1
          toBuf b val

  fromBuf b
     = case !getTag of
            0 => pure Nothing
            1 => do val <- fromBuf b
                    pure (Just val)
            _ => corrupt "Maybe"

export
(TTC a, TTC b) => TTC (Either a b) where
  toBuf b (Left val)
     = do tag 0
          toBuf b val
  toBuf b (Right val)
     = do tag 1
          toBuf b val

  fromBuf b
     = case !getTag of
            0 => do val <- fromBuf b
                    pure (Left val)
            1 => do val <- fromBuf b
                    pure (Right val)
            _ => corrupt "Either"

export
TTC a => TTC (List a) where
  toBuf b xs
      = do toBuf b (TailRec_length xs)
           traverse_ (toBuf b) xs
    where
      ||| Tail-recursive length as buffer sizes can get large
      |||
      ||| Once we port to Idris2, can use Data.List.TailRec.length instead
      length_aux : List a -> Int -> Int
      length_aux [] len = len
      length_aux (_::xs) len = length_aux xs (1 + len)

      TailRec_length : List a -> Int
      TailRec_length xs = length_aux xs 0

  fromBuf b
      = do len <- fromBuf b {a = Int}
           readElems [] (integerToNat (cast len))
    where
      readElems : List a -> Nat -> Core (List a)
      readElems xs Z = pure (reverse xs)
      readElems xs (S k)
          = do val <- fromBuf b
               readElems (val :: xs) k

export
TTC a => TTC (List1 a) where
  toBuf b xxs
     = do toBuf b (head xxs)
          toBuf b (tail xxs)

  fromBuf b = do
    x <- fromBuf b
    xs <- fromBuf b
    pure (x ::: xs)

export
{n : Nat} -> TTC a => TTC (Vect n a) where
  toBuf b xs = writeAll xs
    where
      writeAll : forall n . Vect n a -> Core ()
      writeAll [] = pure ()
      writeAll (x :: xs) = do toBuf b x; writeAll xs

  fromBuf {n} b = rewrite sym (plusZeroRightNeutral n) in readElems [] n
    where
      readElems : Vect done a -> (todo : Nat) -> Core (Vect (todo + done) a)
      readElems {done} xs Z
          = pure (reverse xs)
      readElems {done} xs (S k)
          = do val <- fromBuf b
               rewrite (plusSuccRightSucc k done)
               readElems (val :: xs) k

export
(TTC a, Measure a) => TTC (PosMap a) where
  toBuf b = toBuf b . toList
  fromBuf b = fromList <$> fromBuf b

%hide Fin.fromInteger

count : List.Elem.Elem x xs -> Int
count Here = 0
count (There p) = 1 + count p

toLimbs : Integer -> List Int
toLimbs x
    = if x == 0
         then []
         else if x == -1 then [-1]
              else fromInteger (prim__and_Integer x 0xffff) ::
                   toLimbs (prim__shr_Integer x 16)

fromLimbs : List Int -> Integer
fromLimbs [] = 0
fromLimbs (x :: xs) = cast x + prim__shl_Integer (fromLimbs xs) 16

export
TTC Integer where
  toBuf b val
    = assert_total $ if val < 0
         then do tag 0
                 toBuf b (toLimbs (-val))
         else do tag 1
                 toBuf b (toLimbs val)
  fromBuf b
    = do val <- getTag
         case val of
              0 => do val <- fromBuf b
                      pure (-(fromLimbs val))
              1 => do val <- fromBuf b
                      pure (fromLimbs val)
              _ => corrupt "Integer"

export
TTC Nat where
  toBuf b val = toBuf b (cast {to=Integer} val)
  fromBuf b
     = do val <- fromBuf b
          pure (fromInteger val)

||| Get a file's modified time. If it doesn't exist, return 0 (UNIX Epoch)
export
modTime : String -> Core Int
modTime fname
  = do Right f <- coreLift $ openFile fname Read
         | Left err => pure 0 -- Beginning of Time :)
       Right t <- coreLift $ fileModifiedTime f
         | Left err => do coreLift $ closeFile f
                          pure 0
       coreLift $ closeFile f
       pure t

export
hashFileWith : Maybe String -> String -> Core (Maybe String)
hashFileWith Nothing _ = pure Nothing
hashFileWith (Just sha256sum) fileName
  = do Right fileHandle <- coreLift $ popen
            (sha256sum ++ " \"" ++ osEscape fileName ++ "\"") Read
         | Left _ => err
       Right hashLine <- coreLift $ fGetLine fileHandle
         | Left _ =>
           do coreLift $ pclose fileHandle
              err
       coreLift $ pclose fileHandle
       let w@(_::_) = words hashLine
         | Nil => err
       pure $ Just $ last w
  where
    err : Core a
    err = coreFail $ InternalError ("Can't get " ++ sha256sum ++ " of " ++ fileName)
    osEscape : String -> String
    osEscape = if isWindows
      then id
      else escapeStringUnix


text:
module Compiler.RefC.CC

import Core.Context
import Core.Context.Log
import Core.Options

import System

import Idris.Version
import Libraries.Utils.Path

%default total

findCC : IO String
findCC
    = do Nothing <- getEnv "IDRIS2_CC"
           | Just cc => pure cc
         Nothing <- getEnv "CC"
           | Just cc => pure cc
         pure "cc"

fullprefix_dir : Dirs -> String -> String
fullprefix_dir dirs sub
    = prefix_dir dirs </> "idris2-" ++ showVersion False version </> sub

export
compileCObjectFile : {auto c : Ref Ctxt Defs}
                  -> {default False asLibrary : Bool}
                  -> (sourceFile : String)
                  -> (objectFile : String)
                  -> Core (Maybe String)
compileCObjectFile {asLibrary} sourceFile objectFile =
  do cc <- coreLift findCC
     dirs <- getDirs

     let libraryFlag = if asLibrary then "-fpic " else ""

     let runccobj = cc ++ " -Werror -c " ++ libraryFlag ++ sourceFile ++
                       " -o " ++ objectFile ++ " " ++
                       "-I" ++ fullprefix_dir dirs "refc " ++
                       "-I" ++ fullprefix_dir dirs "include"

     log "compiler.refc.cc" 10 runccobj
     0 <- coreLift $ system runccobj
       | _ => pure Nothing

     pure (Just objectFile)

export
compileCFile : {auto c : Ref Ctxt Defs}
            -> {default False asShared : Bool}
            -> (objectFile : String)
            -> (outFile : String)
            -> Core (Maybe String)
compileCFile {asShared} objectFile outFile =
  do cc <- coreLift findCC
     dirs <- getDirs

     let sharedFlag = if asShared then "-shared " else ""

     let runcc = cc ++ " -Werror " ++ sharedFlag ++ objectFile ++
                       " -o " ++ outFile ++ " " ++
                       (fullprefix_dir dirs "lib" </> "libidris2_support.a") ++ " " ++
                       "-lidris2_refc " ++
                       "-L" ++ fullprefix_dir dirs "refc " ++
                       clibdirs (lib_dirs dirs) ++
                       "-lgmp -lm"

     log "compiler.refc.cc" 10 runcc
     0 <- coreLift $ system runcc
       | _ => pure Nothing

     pure (Just outFile)

  where
    clibdirs : List String -> String
    clibdirs ds = concat (map (\d => "-L" ++ d ++ " ") ds)


text:
module Data.Schema

import public Control.Delayed

import public Data.Bool
import public Data.List1
import public Data.List

import public Data.Schema.Restricted

%default total

public export
data Valid : Type -> Type where
  IsString : Valid String
  IsChar   : Valid Char
  IsNat    : Valid Nat

public export
data Atom : (name : Type) -> Type where
  MkAtom : (n           : name)
        -> (v           : Type)
        -> (restriction : Schema.Restriction type)
        -> (prf         : Valid type)
                       -> Atom name

public export
data Schema : (name : Type) -> Bool -> Type where
  ||| The empty schema.
  Empty : Schema n False

  ||| A schema with a single component.
  Simple : Atom n -> Schema n True

  ||| A named schema with sub-schema.
  Complex : (name   : n)
         -> (schema : Schema n a)
                   -> Schema n a

  ||| Sequence two schemas where `that` might be infinite.
  SeqEat : (this :      Schema n True)
        -> (that : Inf (Schema n b))
                 ->     Schema n True

  ||| Sequence two schemas where `that` is not infinite.
  SeqEmpty : (this : Schema n  a)
          -> (that : Schema n       b)
                  -> Schema n (a || b)

  ||| Choice between two schemas.
  Alt : (this : Schema n  a)
     -> (that : Schema n       b)
             -> Schema n (a && b)

namespace API
  public export
  Schema : Type -> Type
  Schema n = Schema n True

--public export %inline
--(<+>) : {a : Bool}
--     -> (this :        Schema n  a)
--     -> (that : inf a (Schema n       b))
--             ->        Schema n (a || b)
--(<+>) {a = False} = SeqEmpty
--(<+>) {a = True}  = SeqEat

%allow_overloads (<|>)

public export %inline
(<|>) : Schema n  a
     -> Schema n       b
     -> Schema n (a && b)
(<|>) = Alt

public export
opt : (s : Schema n True) -> Schema n False
opt s = s <|> Empty

mutual
  public export
  some : Schema n -> Schema n
  some l = SeqEat l (many l)

  public export
  many : Schema n -> Schema n False
  many l = opt (some l)

public export
select : (xs  : List (Schema n b))
      -> (prf : NonEmpty xs) -- so we can use prettier list notation.
             => Schema n b
select (x :: xs) {prf = IsNonEmpty}
    = foldl build x xs
  where
    build : Schema n b -> Schema n b -> Schema n b
    build acc x = rewrite sym (andSameNeutral b) in (acc <|> x)

public export
concat : (xs  : List (Schema n b))
      -> (prf : NonEmpty xs) -- so we can use prettier list notation.
             => Schema n (b && True)
concat (x :: xs) {prf = IsNonEmpty}
      = concat' (x::xs)

  where
    concat' : (xs : List (Schema n b))
                 ->       Schema n (b && isCons xs)
    concat' []
      = rewrite andFalseFalse b in Empty

    concat' (x :: xs)
      = rewrite andTrueNeutral b in
        rewrite sym (orSameAndRightNeutral b (isCons xs)) in
          SeqEmpty x (concat' xs)

-- [ EOF ]

max_stars_repo_name: jfdm/idris-shaped

max_issues_repo_name: jfdm/idris-shaped

max_forks_repo_name: jfdm/idris-shaped


text:
module Y

import X

X.f x = x + 1

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
||| A general purpose Hashing library (not cryptographic)
|||
|||   The core hash is djb2, which is very fast but does not have the best distribution
|||   Source: http://www.cse.yorku.ca/~oz/hash.html
|||
|||   The salted version and the magic salt are copied from Haskell's bloomfilter library
|||   Source: https://hackage.haskell.org/package/bloomfilter-2.0.0.0/docs/src/Data-BloomFilter-Hash.html#Hashable
|||
|||   Portedd from Idris1 by HATTORI, Hiroki 2021.
module Data.Hash

import Data.Vect

%default total

||| A type that can be hashed
public export
interface Hashable a where
  saltedHash64 : a -> Bits64 -> Bits64 -- value to hash, salt, hash

||| Computes a non cryptographic hash
export hash : Hashable a => a -> Bits64
hash x = saltedHash64 x 0x16fc397cf62f64d3

||| Given a user provided salt, computes a non cryptographic hash.
||| This version is meant to mitigate hash-flooding DoS attacks.
export saltedHash : Hashable a => Bits64 -> a -> Bits64
saltedHash salt x = saltedHash64 x salt

||| Nth byte of a Bits64
byte : Int -> Bits64 -> Bits64
byte n w = prim__and_Bits64 (prim__shr_Bits64 w $ fromInteger $ cast (n * 8)) 0xff

mod64 : Integer -> Bits64
mod64 i = fromInteger $ (abs i `mod` 0xffffffffffffffff)

export
Hashable Bits64 where
  saltedHash64 w salt = foldr (\b,acc => (acc `prim__shl_Bits64` 10) + acc + b)
                              salt
                              [byte (fromInteger n) w | n <- [7,6..0]] -- djb2 hash function. Not meant for crypto

export
Hashable a => Hashable (Maybe a) where
  saltedHash64 Nothing  salt = salt
  saltedHash64 (Just k) salt = saltedHash64 k salt

export
(Hashable a, Hashable b) => Hashable (a, b) where
  saltedHash64 (a,b) salt = saltedHash64 b (saltedHash64 a salt)

export
Hashable a => Hashable (List a) where
  saltedHash64 l salt = foldr (\c,acc => saltedHash64 c acc) salt l

export
Hashable a => Hashable (Vect n a) where
  saltedHash64 l salt = foldr (\c,acc => saltedHash64 c acc) salt l

export Hashable Integer where saltedHash64 = saltedHash64 . mod64
export Hashable () where      saltedHash64 _ salt = salt

export
Hashable Bool where
  saltedHash64 True  = saltedHash64 (the Bits64 1)
  saltedHash64 False = saltedHash64 (the Bits64 0)

export Hashable Int where     saltedHash64 = saltedHash64 . the Integer . cast
export Hashable Char where    saltedHash64 = saltedHash64 . the Integer . cast
export Hashable Bits8 where   saltedHash64 = saltedHash64 . prim__cast_Bits8Int
export Hashable Bits16 where  saltedHash64 = saltedHash64 . prim__cast_Bits16Int
export Hashable Bits32 where  saltedHash64 = saltedHash64 . prim__cast_Bits32Int
export Hashable String where  saltedHash64 s = saltedHash64 (unpack s)


text:
import Data.Vect

someVect : (n ** Vect n Int)
-- someVect = (_ ** [])

someVectLen : Nat
someVectLen = someVect.fst


text:
module RevRev

namespace Preloaded
  %access public export
  %default total

  rev : List x -> List x
  rev [] = []
  rev (y :: xs) = rev xs ++ [y]

%access export
%default total

lemma : (xs : List x) -> (y : x) -> rev (xs ++ [y]) = y :: rev xs
lemma []      _ = Refl
lemma (_::as) y = rewrite lemma as y in Refl

revrevid : (a : List x) -> (rev (rev a)) = a
revrevid []      = Refl
revrevid (a::as) = rewrite lemma (rev as) a in
                   rewrite revrevid as in
                   Refl


text:
data SimpleData = PtrAndSize AnyPtr Int

record Complicated where
  constructor MkComplicated
  simple : SimpleData

record MoreComplicated where
    constructor MkMoreComplicated
    something : Complicated

record EvenMoreComplicated where
    constructor MkEvenMoreComplicated
    somethingEven : MoreComplicated

data TooComplicatedToBeTrue : (something : EvenMoreComplicated) -> Type where
    SomethingVeryComplicatedIs :
        TooComplicatedToBeTrue
            (MkEvenMoreComplicated (MkMoreComplicated (MkComplicated (PtrAndSize addr len))))

showing  :  (something : EvenMoreComplicated) -> (TooComplicatedToBeTrue something) -> Void
showing _ SomethingVeryComplicatedIs impossible


text:
module Main
import Data.SnocList

|||Abstract Syntax Tree for Integer with addition, subtraction and multiplication
data ASTExpr
    = EIntLit Int
    | EAddition ASTExpr ASTExpr
    | ESubtraction ASTExpr ASTExpr
    | EMultiplication ASTExpr ASTExpr

|||Usng the Num interface to define basic numerical arithmetic
Num (ASTExpr) where
    (+) = EAddition
    (*) = EMultiplication
    fromInteger = EIntLit . fromInteger

|||Using the Neg interface to define operations on numbers which can be negative.
Neg (ASTExpr) where
    negate x = 0 - x
    (-) = ESubtraction

|||Instruction syntax
data Instruction = Push Int | Add | Sub | Mult

|||Compile expression to a list of instruction
total
compile : ASTExpr -> List Instruction
compile (EIntLit a) =  [Push a]
compile (EAddition a b) = compile a ++ compile b ++ [Add]
compile (ESubtraction a b) = compile a ++ compile b ++ [Sub]
compile (EMultiplication a b) = compile a ++ compile b ++ [Mult]

|||Writing the instructions to a file for the stack machine to execute
total
print : Instruction -> String
print (Push a) = "Push " ++ show a
print Add = "Add"
print Sub = "Sub"
print Mult = "Mult"

|||Helper function for printList (tail recursive and linear time by using stringMap)
total
stringMap : (a -> String) -> List a -> String
stringMap f = go Lin
  where go : SnocList String -> List a -> String
        go sx []         = concat (sx <>> Nil)
        go sx (x :: Nil) = go (sx :< f x) Nil
        go sx (x :: xs)  = go (sx :< f x :< "\n") xs

|||Writing the List instructions to a file for the stack machine to execute
total
printList : List Instruction -> String
printList = stringMap print

--Taking a machine configuration to the next one by executing a single step of computations
total
runInstruction : List Int -> Instruction -> Maybe (List Int)
runInstruction xs (Push a) = Just (a :: xs)
runInstruction (x :: y :: xs) Add = Just ((x + y) :: xs)
runInstruction (x :: y :: xs) Sub = Just ((y - x) :: xs)
runInstruction (x :: y :: xs) Mult = Just ((x * y) :: xs)
runInstruction _ _ = Nothing

|||Taking a machine configuration to the next one by executing multiple step of computations
total
runInstructions: List Instruction -> List Int -> Maybe (List Int)
runInstructions xs ys = foldlM runInstruction ys xs

|||Evaluate Abstract Syntax Tree and return value
total
evaluate : ASTExpr -> Int
evaluate (EIntLit a) = a
evaluate (EAddition a b) = evaluate a + evaluate b
evaluate (ESubtraction a b) = evaluate a - evaluate b
evaluate (EMultiplication a b) = evaluate a * evaluate b

|||Universal statement linking the evaluation path via compile followed by RunInstructions
total
runAll: (e : ASTExpr) -> Maybe (List Int)
runAll e = runInstructions(compile(e)) []

|||Universal statement linking the evaluation path via evaluate
total
runAll2: (e : ASTExpr) -> Maybe (List Int)
runAll2 e = Just([evaluate(e)])

-- Testing all functions invidually and against each other

--runInstruction
test_runInstruction_add : runInstruction [1, 2] Add = Just [3]
test_runInstruction_add = Refl

test_runInstruction_sub : runInstruction [2, 1] Sub = Just [-1]
test_runInstruction_sub = Refl

test_runInstruction_mult : runInstruction [10, 2] Mult = Just [20]
test_runInstruction_mult = Refl

--runInstructions
test_runInstructions_add : runInstructions [Push 1, Push 2, Add] [] = Just [3]
test_runInstructions_add = Refl

test_runInstructions_sub : runInstructions [Push 1, Push 2, Sub] [] = Just [-1]
test_runInstructions_sub = Refl

test_runInstructions_mult : runInstructions [Push 10, Push 2, Mult] [] = Just [20]
test_runInstructions_mult = Refl

--runAll
test_runAll_add : runAll (EAddition (EIntLit 2) (EIntLit 3))  = Just [5]
test_runAll_add = Refl

test_runAll_sub : runAll (ESubtraction (EIntLit 2) (EIntLit 3))  = Just [-1]
test_runAll_sub = Refl

test_runAll_mul : runAll (EMultiplication (EIntLit 10) (EIntLit 2))  = Just [20]
test_runAll_mul = Refl

--runAll2
test_runAll2_add : runAll2 (EAddition (EIntLit 2) (EIntLit 3))  = Just [5]
test_runAll2_add = Refl

test_runAll2_sub : runAll2 (ESubtraction (EIntLit 2) (EIntLit 3))  = Just [-1]
test_runAll2_sub = Refl

test_runAll2_mul : runAll2 (EMultiplication (EIntLit 10) (EIntLit 2))  = Just [20]
test_runAll2_mul = Refl

--equality between runAll and runAll2
test_both_RunAlls_add : runAll (EAddition (EIntLit 2) (EIntLit 3)) = runAll2 (EAddition (EIntLit 2) (EIntLit 3))
test_both_RunAlls_add = Refl

test_both_RunAlls_sub : runAll (ESubtraction (EIntLit 2) (EIntLit 3)) = runAll2 (ESubtraction (EIntLit 2) (EIntLit 3))
test_both_RunAlls_sub = Refl

test_both_RunAlls_mul : runAll (EMultiplication (EIntLit 10) (EIntLit 2)) = runAll2 (EMultiplication (EIntLit 10) (EIntLit 2))
test_both_RunAlls_mul = Refl

-- Testing the two evaluation paths
test3_allFunc_add : runInstructions (compile (EAddition (EIntLit 2) (EIntLit 3))) [] === Just [evaluate (EAddition (EIntLit 2) (EIntLit 3))]
test3_allFunc_add = Refl

test3_allFunc_sub : runInstructions (compile (ESubtraction (EIntLit 2) (EIntLit 3))) [] === Just [evaluate (ESubtraction (EIntLit 2) (EIntLit 3))]
test3_allFunc_sub = Refl

test3_allFunc_mul : runInstructions (compile (EMultiplication (EIntLit 10) (EIntLit 2))) [] === Just [evaluate (EMultiplication (EIntLit 10) (EIntLit 2))]
test3_allFunc_mul = Refl

main : IO ()
main = ?hole

max_stars_repo_name: DejanMilicic/IdrisPlayground

max_issues_repo_name: DejanMilicic/IdrisPlayground

max_forks_repo_name: DejanMilicic/IdrisPlayground


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 3

import Data.Vect

-- check that all functions are total
%default total

--
-- section 3.2
--

-- exercise 3.2.1
my_length : List a -> Nat
my_length [] = 0
my_length (x :: xs) = 1 + my_length xs

-- exercise 3.2.2
my_reverse : List a -> List a
my_reverse [] = []
my_reverse (x :: xs) = my_reverse xs ++ [x]

-- exercise 3.2.3
my_map : (a -> b) -> List a -> List b
my_map f [] = []
my_map f (x :: xs) = f x :: my_map f xs

-- exercise 3.2.4
my_vect_map : (a -> b) -> Vect n a -> Vect n b
my_vect_map f [] = []
my_vect_map f (x :: xs) = f x :: my_vect_map f xs

--
-- section 3.3
-- see Matrix.idr
--

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
||| `OrdList` is a "labelled" list that ensure that inserted elements are ordered.
module Flexidisc.OrdList

import public Flexidisc.OrdList.CompWithKeys
import public Flexidisc.OrdList.Diff
import public Flexidisc.OrdList.Disjoint
import public Flexidisc.OrdList.HereOrNot
import public Flexidisc.OrdList.Fresh
import public Flexidisc.OrdList.Label
import public Flexidisc.OrdList.Nub
import public Flexidisc.OrdList.Permute
import public Flexidisc.OrdList.Sub
import public Flexidisc.OrdList.SubWithKeys
import public Flexidisc.OrdList.Type
import public Flexidisc.OrdList.Row

%default total
%access public export

||| A witness that two OrdList are using the same order
||| (as well as the same key and value type, but this is more obvious)
data SameOrd : (xs, ys : OrdList k v o) -> Type where
  Same : SameOrd xs ys

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
{- Ctrl-Alt-A: Add definition
   Ctrl-Alt-C: Case split
   Ctrl-Alt-D: Documentation
   Ctrl-Alt-L: Lift hole: Lifts a hole to the top level as a new function definition
   Ctrl-Alt-M: Match: Replaces a hole with a case expression that matches on an intermediate result
   Ctrl-Alt-R: Reloads and typechecks the current buffer
   Ctrl-Alt-S: Search
   Ctrl-Alt-T: Type-check: Displays the type under cursor
   Ctrl-Alt-W: Add With View -}
module Main

data InfIO : Type where
  Do : IO a -> (a -> Inf InfIO) -> InfIO

total
loopPrint0 : String -> InfIO
loopPrint0 msg = Do (putStrLn msg) (\_ => loopPrint0 msg)

data Fuel = Dry | More (Lazy Fuel)

tank : Nat -> Fuel
tank Z = Dry
tank (S n) = More (tank n)

forever : Fuel
forever = More forever

run : Fuel -> InfIO -> IO ()
run Dry _ = putStrLn "Out of fuel"
run (More fuel) (Do action cont) = do
  res <- action
  run fuel (cont res)

(>>=) : IO a -> (a -> Inf InfIO) -> InfIO
(>>=) = Do

total
loopPrint1 : String -> InfIO
loopPrint1 msg = do
  putStrLn msg
  loopPrint1 msg

main : IO ()
main = do
  run (tank 5) (loopPrint0 "vroom")
  run (tank 5) (loopPrint1 "broom")

max_stars_repo_name: luc-tielen/idris-grin

max_issues_repo_name: luc-tielen/idris-grin

max_forks_repo_name: luc-tielen/idris-grin


text:
module DataStore

import Data.Strings
import Data.Vect
import System.REPL

%default total

data DataStore : Type where
  MkData : (size : Nat) -> (items : Vect size String) -> DataStore

size : DataStore -> Nat
size (MkData size' _) = size'

items : (store : DataStore) -> Vect (size store) String
items (MkData _ items') = items'

addToStore : (store : DataStore) -> String -> DataStore
addToStore (MkData size items) newItem = MkData _ (addToData items)
  where
    addToData : Vect old String -> Vect (S old) String
    addToData [] = [newItem]
    addToData (item :: items) = item :: addToData items

data Command = Add String
             | Get Integer
             | Quit

parseCommand : (cmd : String) -> (args : String) -> Maybe Command
parseCommand "add" str = Just (Add str)
parseCommand "get" val = case all isDigit (unpack val) of
                              False => Nothing
                              True => Just (Get (cast val))
parseCommand "quit" "" = Just Quit
parseCommand _ _ = Nothing

parse : (input : String) -> Maybe Command
parse input = case span (/= ' ') input of
                   (cmd, args) => parseCommand cmd (ltrim args)

getEntry : (store : DataStore) -> (pos : Integer) -> Maybe (String, DataStore)
getEntry store pos = case integerToFin pos (size store) of
                          Nothing => Just ("Invalid index: " ++ show pos ++ "\n", store)
                          Just idx => Just (show (index idx (items store)) ++ "\n", store)

processCommand : (store : DataStore) -> (cmd : Command) -> Maybe (String, DataStore)
processCommand store (Add item) = Just ("ID" ++ show (size store) ++ "\n", addToStore store item)
processCommand store (Get idx) = getEntry store idx
processCommand store Quit = Nothing

processInput : (store : DataStore) -> String -> Maybe (String, DataStore)
processInput store inp =
  case parse inp of
       Nothing => Just ("Invalid command\n", store)
       Just cmd => processCommand store cmd

partial
main : IO ()
main = replWith (MkData _ []) "Command: " processInput

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module IdrisJvm.Data.IORef

import IdrisJvm.IO

export
data IORef a = MkIORef a

public export
interface HasReference (ffi : FFI) where
  newIORef' : a -> IO' ffi (IORef a)
  readIORef' : IORef a -> IO' ffi a
  writeIORef' : IORef a -> a -> IO' ffi ()

export
modifyIORef': HasReference ffi => IORef a -> (a -> a) -> IO' ffi ()
modifyIORef' ref fn =
  do
    val <- readIORef' ref
    writeIORef' ref (fn val)

export
Ref : Type
Ref = JVM_Native (Class ("io/github/mmhelloworld/idrisjvm/runtime/Ref"))

export
implementation HasReference FFI_JVM where
  newIORef' val = (MkIORef . believe_me) <$> FFI.new (Object -> JVM_IO Ref) (believe_me val)

  readIORef' (MkIORef ref) = believe_me <$> invokeInstance "getValue" (Ref -> JVM_IO Object) (believe_me ref)

  writeIORef' (MkIORef ref) val = invokeInstance "setValue" (Ref -> Object -> JVM_IO ()) (believe_me ref) (believe_me val)

||| Build a new IORef
export
newIORef : a -> JVM_IO (IORef a)
newIORef = newIORef'

||| read the value of an IORef
export
readIORef : IORef a -> JVM_IO a
readIORef = readIORef'

||| write the value of an IORef
export
writeIORef : IORef a -> a -> JVM_IO ()
writeIORef = writeIORef'

||| mutate the contents of an IORef
export
modifyIORef : IORef a -> (a -> a) -> JVM_IO ()
modifyIORef = modifyIORef'


text:
module Group

import Monoid
%access public export

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

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

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

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

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

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

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

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

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

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

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

--The type of proofs that a type trav traverses a given coset only once, if at all
CosetInj: (h: Type) -> ((+) : h -> h -> h) -> (pf1: IsGroup h (+)) -> (g: Type) -> ((*) : g -> g -> g) -> (pf2: IsGroup g (*)) -> (sbgrp: Subgroup h (+) pf1 g (*) pf2) -> (trav: Type) -> (f: trav -> g) -> Type
CosetInj  h (+) pf1 g (*) pf2 sbgrp trav f = ((x: trav) -> (y: trav) -> (p: h ** (f x) = (incl p)*(f y)) -> (x = y)) where
  incl = (fst sbgrp)

--The type of proofs that a type trav traverses every coset of a given group g wrt a subgroup h
CosetAll: (h: Type) -> ((+) : h -> h -> h) -> (pf1: IsGroup h (+)) -> (g: Type) -> ((*) : g -> g -> g) -> (pf2: IsGroup g (*)) -> (sbgrp: Subgroup h (+) pf1 g (*) pf2) -> (trav: Type) -> (f: trav -> g) -> Type
CosetAll h (+) pf1 g (*) pf2 sbgrp trav f = ((a: g) -> (p: h ** (t: trav ** ((f t)*(incl p) = a)))) where
  incl = (fst sbgrp)

-- Traversal type - the type of proofs that a given type traverses each coset exactly once
IsTraversal: (h: Type) -> ((+) : h -> h -> h) -> (pf1: IsGroup h (+)) -> (g: Type) -> ((*) : g -> g -> g) -> (pf2: IsGroup g (*)) -> (sbgrp: Subgroup h (+) pf1 g (*) pf2) -> (trav: Type) -> Type
IsTraversal h (+) pf1 g (*) pf2 sbgrp trav = DPair (trav -> g) (\f => (CosetInj h (+) pf1 g (*) pf2 sbgrp trav f, CosetAll h (+) pf1 g (*) pf2 sbgrp trav f))

--Defining the multiplication operation between elements of a traversal
MulTrav: (h: Type) -> ((+) : h -> h -> h) -> (pf1: IsGroup h (+)) -> (g: Type) -> ((*) : g -> g -> g) -> (pf2: IsGroup g (*)) -> (sbgrp: Subgroup h (+) pf1 g (*) pf2) -> (trav: Type) -> (IsTraversal h (+) pf1 g (*) pf2 sbgrp trav) -> trav -> trav -> trav
MulTrav h (+) pf1 g (*) pf2 sbgrp trav pftrav y z = (fst (snd ((snd (snd pftrav)) ((f y)*(f z))))) where
  f: trav -> g
  f = (fst pftrav)

--Proof of uniqueness of the coset representative in trav, in the following sense
--Proof that the operation that generates coset representative in trav for an element of g (from CosetAll) inverts the function generating a coset representative by going from trav to g (from IsTraversal)
corepfinv: (h: Type) -> ((+) : h -> h -> h) -> (pf1: IsGroup h (+)) -> (g: Type) -> ((*) : g -> g -> g) -> (pf2: IsGroup g (*)) -> (sbgrp: Subgroup h (+) pf1 g (*) pf2) -> (trav: Type) -> (pftrav: IsTraversal h (+) pf1 g (*) pf2 sbgrp trav) -> (y: trav) -> (((fst (snd ((snd (snd pftrav)) ((fst pftrav) y) ) )) ) = y)
corepfinv h (+) pf1 g (*) pf2 sbgrp trav pftrav y = (sym ((fst (snd pftrav)) y t (p ** (sym (snd (snd  ((snd (snd pftrav)) (f y)) )))) )) where
  t: trav
  t = (fst (snd ((snd (snd pftrav)) ((fst pftrav) y) ) ))
  f: trav -> g
  f = (fst pftrav)
  p: h
  p = (fst ((snd (snd pftrav)) (f y)))

--Proof that the definitional equality for traversal multiplication holds
MulTravDefPf: (h: Type) -> ((+) : h -> h -> h) -> (pf1: IsGroup h (+)) -> (g: Type) -> ((*) : g -> g -> g) -> (pf2: IsGroup g (*)) -> (sbgrp: Subgroup h (+) pf1 g (*) pf2) -> (trav: Type) -> (pftrav: IsTraversal h (+) pf1 g (*) pf2 sbgrp trav) -> (y: trav) -> (z: trav) -> (MulTrav h (+) pf1 g (*) pf2 sbgrp trav pftrav y z) = ((fst (snd ((snd (snd pftrav)) (((fst pftrav) y)*((fst pftrav) z))) )))
MulTravDefPf h (-) pf1 g (*) pf2 sbgrp trav pftrav y z = Refl

--Proof that the function from g to trav recovered from CosetAll is in some sense a magma homorphism
MulTravHomPf: (h: Type) -> ((+) : h -> h -> h) -> (pf1: IsGroup h (+)) -> (g: Type) -> ((*) : g -> g -> g) -> (pf2: IsGroup g (*)) -> (sbgrp: Subgroup h (+) pf1 g (*) pf2) -> (trav: Type) -> (pftrav: IsTraversal h (+) pf1 g (*) pf2 sbgrp trav) -> (y: trav) -> (z: trav) -> ((fst (snd ((snd (snd pftrav)) (((fst pftrav) y)*((fst pftrav) z))) ))) = (MulTrav h (+) pf1 g (*) pf2 sbgrp trav pftrav ((fst (snd ((snd (snd pftrav)) ((fst pftrav) y)) ))) ((fst (snd ((snd (snd pftrav)) ((fst pftrav) z)) ))))
MulTravHomPf h (-) pf1 g (*) pf2 sbgrp trav pftrav y z = trans (sym (MulTravDefProof)) (trans (cong {f = f1} (sym CorepFInverseY)) (cong {f = f2} (sym CorepFInverseZ))) where

  MulTravDefProof: (MulTrav h (-) pf1 g (*) pf2 sbgrp trav pftrav y z) = ((fst (snd ((snd (snd pftrav)) (((fst pftrav) y)*((fst pftrav) z))) )))
  MulTravDefProof = (MulTravDefPf h (-) pf1 g (*) pf2 sbgrp trav pftrav y z )

  f1: trav -> trav
  f1 x = MulTrav h (-) pf1 g (*) pf2 sbgrp trav pftrav x z

  f2: trav -> trav
  f2 x = MulTrav h (-) pf1 g (*) pf2 sbgrp trav pftrav ((fst (snd ((snd (snd pftrav)) ((fst pftrav) y) ) )) ) x

  CorepFInverseY: (((fst (snd ((snd (snd pftrav)) ((fst pftrav) y) ) )) ) = y)
  CorepFInverseY = CorepFInv h (-) pf1 g (*) pf2 sbgrp trav pftrav y

  CorepFInverseZ: (((fst (snd ((snd (snd pftrav)) ((fst pftrav) z) ) )) ) = z)
  CorepFInverseZ = CorepFInv h (-) pf1 g (*) pf2 sbgrp trav pftrav z


text:
module Control.Monad.Syntax

%default total

infixr 1 =<<, <=<, >=>

||| Left-to-right Kleisli composition of monads.
public export
(>=>) : Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
(>=>) f g = \x => f x >>= g

public export
||| Right-to-left Kleisli composition of monads, flipped version of `>=>`.
(<=<) : Monad m => (b -> m c) -> (a -> m b) -> (a -> m c)
(<=<) = flip (>=>)

public export
||| Right-to-left monadic bind, flipped version of `>>=`.
(=<<) : Monad m => (a -> m b) -> m a -> m b
(=<<) = flip (>>=)