text:
module Graph.API

import Graph.Core

%access export

noNodes : Graph a b -> Nat
noNodes = length . labNodes

-- Not very useful, labNodes is enough
nodes : Graph a b -> List NodeID
nodes = map fst . labNodes

-- Same as nodes, labEdges is enough
-- edges

nodeRange : Graph a b -> (NodeID, NodeID)
nodeRange g = let vs = nodes g in (foldl1 min vs, foldl1 max vs)

labEdges : Graph a b -> List (LEdge b)
labEdges = ufold (\(p, node, _, s), acc =>
             (map (\(label, target) => (node, target, label)) s) ++
             (map (\(label, source) => (source, node, label)) p) ++
             acc) []

namespace Edge
  source : LEdge b -> NodeID
  source (s, _, _) = s
  target : LEdge b -> NodeID
  target (_, t, _) = t
  label : LEdge b -> b
  label (_, _, ec) = ec

namespace Node
  identifier : LNode b -> NodeID
  identifier (i, _) = i
  label : LNode b -> b
  label (_, nc) = nc

gmap : (Context a b -> Context c d) -> Graph a b -> Graph c d
gmap f = ufold (\c, g => (f c) & g) empty

nmap : (a -> c) -> Graph a b -> Graph c b
nmap f = gmap (\(ps, node, label, ss) => (ps, node, f label, ss))

private
map1 : (b -> c) -> List (b, Int) -> List (c, Int)
map1 f = map (\(label, node) => (f label, node))

emap : (b -> c) -> Graph a b -> Graph a c
emap f = gmap (\(ps, n, nc, ss) => (map1 f ps, n, nc, map1 f ss))

nemap : (a -> c) -> (b -> d) -> Graph a b -> Graph c d
nemap fn fe = gmap (\(ps, n, nc, ss) => (map1 fe ps, n, fn nc, map1 fe ss))

infixr 10 .: -- TODO choose right fixity

(.:) : (c -> d) -> (a -> b -> c) -> a -> b -> d
(.:) = (.) . (.)

mcontext : Graph a b -> NodeID -> MContext a b
mcontext = fst .: flip match

context4l : Graph a b -> NodeID -> Adj b
context4l = maybe [] context4l' .: mcontext where
  context4l' : Context a b -> Adj b
  context4l' (p, v, _, s) = s ++ filter ((==v) . snd) p

out : Graph a b -> NodeID -> List (LEdge b)
out graph node = map (\(label, succ) => (node, succ, label))
                     (context4l graph node)

max_stars_repo_name: gpyh/idris-graph

max_issues_repo_name: gpyh/idris-graph

max_forks_repo_name: gpyh/idris-graph


text:
module Data.Functor.Representable

import Data.Vect
import Data.Vect.Extra

%default total

public export
interface Functor f => Representable f rep | f where
  index : f a -> rep -> a
  tabulate : (rep -> a) -> f a

public export
[Compose] Representable f rep => Representable g rep' => Representable (f . g) (rep, rep') using Functor.Compose where
  index x (i, j) = (x `index` i) `index` j
  tabulate = map tabulate . tabulate . curry

public export
{n : Nat} -> Representable (Vect n) (Fin n) where
  index = flip index
  tabulate f = mapWithIndex (\i, () => f i) $ replicate n ()

ext: idr

max_stars_repo_name: pnotequalnp/game-of-life

max_issues_repo_name: pnotequalnp/game-of-life

max_forks_repo_name: pnotequalnp/game-of-life


text:
import Data.List

maybeAdd : Maybe Int -> Int -> Int
maybeAdd x y = maybe id (+) x y


text:
module Utils.Handle.C

import Control.Linear.LIO
import Control.Monad.Error.Either
import Data.Nat
import Data.Vect
import Network.Socket
import Utils.Handle

-- Needed for some reason, sometimes the socket does not read enough bytes
recv_n_bytes : HasIO m => Socket -> Nat -> List Bits8 -> m (Either SocketError (List Bits8))
recv_n_bytes sock Z buf = pure (Right [])
recv_n_bytes sock size buf = do
  Right response <- recvBytes sock $ cast $ minus size $ length buf
  | error => pure error
  let buf = buf <+> response
  if (length buf) >= size
    then pure $ Right buf
    else recv_n_bytes sock size buf

||| Turning a non-linear socket from Network.Socket into a Handle tailored for Network.TLS.Handle
export
socket_to_handle : Socket -> Handle' Socket ()
socket_to_handle sock = MkHandle
  sock
  (\(MkSocket _ _ _ _), wanted => do
    Right output <- recv_n_bytes sock wanted []
    | Left code => pure1 $ False # ("recv_bytes failed with code " <+> show code # ())
    pure1 $ True # (output # sock)
  )
  (\(MkSocket _ _ _ _), input => do
    Right _ <- sendBytes sock input
    | Left code => pure1 $ False # ("send_bytes failed with code " <+> show code # ())
    pure1 $ True # sock
  )
  (\(MkSocket _ _ _ _) => do
    Socket.close sock
    pure1 ()
  )


text:
module NewEden.Algebra

%default total

data AssociativeFunction : (t:Type) -> (f:(t -> t -> t)) -> Type where
  MkAssociativeFunction :
      (f:(t -> t -> t))
   -> (prf:((a:t) -> (b:t) -> (c:t) -> f a (f b c) = f (f a b) c))
   -> AssociativeFunction t f

data CommutativeFunction : (t:Type) -> (f:(t -> t -> t)) -> Type where
  MkCommutativeFunction :
      (f:(t -> t -> t))
   -> (prf:((a:t) -> (b:t) -> f a b = f b a))
   -> CommutativeFunction t f

data MonomorphicFunction : (t1 -> t2) -> Type where
  MkMonomorphicFunction :
      (f:(t1 -> t2))
   -> ((a:t1) -> (b:t1) -> f a = f b -> a = b)
   -> MonomorphicFunction f

data Monoid : (t:Type) -> (f:(t -> t -> t)) -> (zero:t) -> Type where
  MkMonoid :
      (lemma:AssociativeFunction t f)
   -> (zero:t)
   -> (prf1:((a:t) -> f a zero = a))
   -> (prf2:((a:t) -> f zero a = a))
   -> Monoid t f zero

-- monoid which is strictly not strong enough to be a group (proven lack of inverses)
data StrictMonoid : (m:Monoid t f z) -> Type where
  MkStrictMonoid :
      (m:Monoid t f z)
   -> (prfNoInverses:((a:t) -> (b:t) -> (p:(f a b = z)) -> (a = z)))
   -> StrictMonoid m

data Group : Monoid t f z -> Type where
  MkGroup :
      (m:Monoid t f z)
   -> (prfInverse:((a:t) -> (b : t ** (f a b = z))))
   -> Group m

data Coproduct : (C : Type) -> Type where
  MkCoproduct :
      {C : Type}
   -> (coproduct : C -> C -> C)
   -> ((x1 : C) -> (x2 : C) ->
        (
           i1 : C -> C **
           (
             i2 : C -> C **
             (
               i1 x1 = coproduct x1 x2
             , i2 x2 = coproduct x1 x2
             , (x : C) ->
               (
                 f1 : C -> C **
                 (
                   f2 : C -> C **
                   (
                     f1 x1 = x
                   , f2 x2 = x
                   , (f : C -> C **
                     (
                       f $ coproduct x1 x2 = x
                     , ((c : C) -> f1 c = f (i1 c))
                     , ((c : C) -> f2 c = f (i2 c))
                     , ((f' : C -> C)
                         -> f' $ coproduct x1 x2 = x
                         -> ((c : C) -> f1 c = f' (i1 c))
                         -> ((c : C) -> f2 c = f' (i2 c))
                         -> ((n : C) -> f' c = f c)
                       )
                     ))
                   )
                 )
               )
             )
           )
        )
      )
   -> Coproduct C

data Product : (C : Type) -> Type where
  MkProduct :
      {C : Type}
   -> (product : C -> C -> C)
   -> ((x1 : C) -> (x2 : C) ->
       (
         p1 : C -> C **
         (
           p2 : C -> C **
           ((y : C) ->
            (f1 : C -> C) ->
            f1 y = x1 ->
            (f2 : C -> C) ->
            f2 y = x2 ->
            (
              f : C -> C **
              (
                f y = product x1 x2
              , ((c : C) -> p1 (f c) = f1 c)
              , ((c : C) -> p2 (f c) = f2 c)
              , ((f' : C -> C) ->
                 f' y = product x1 x2 ->
                 ((c : C) -> p1 (f' c) = f1 c) ->
                 ((c : C) -> p2 (f' c) = f2 c) ->
                 ((c : C) -> f' c = f c)
                )
              )
            )
           )
         )
       )
      )
   -> Product C

data InitialObject : (C : Type) -> Type where
  MkInitialObject :
      {C : Type}
   -> (initialObject : C)
   -> ((x : C) ->
       (f : C -> C **
        ( (f initialObject = x)
        , ((f' : C -> C) ->
           f' initialObject = x ->
           ((c : C) -> f' c = f c)
          )
        )
       )
      )
   -> InitialObject C

data TerminalObject : (C : Type) -> Type where
  MkTerminalObject :
      {C : Type}
   -> (terminalObject : C)
   -> ((x : C) ->
       (f : C -> C **
        ((f x = terminalObject)
        , ((f' : C -> C) ->
           f' x = terminalObject ->
           ((c : C) -> f' c = f c)
          )
        )
       )
      )
   -> TerminalObject C

data Isomorphism : (t:Type) -> (u:Type) -> (f:(t -> u)) -> (g:(u -> t)) -> Type where
  MkIsomorphism : (t:Type) -> (u:Type) -> (f:(t -> u)) -> (g:(u -> t)) -> ((a:t) -> g (f a) = a) -> ((a:u) -> f (g a) = a) -> Isomorphism t u f g

equalityMap : (f:(t -> u)) -> a = b -> f a = f b
equalityMap f Refl = Refl

transitivity : a = b -> b = c -> a = c
transitivity Refl Refl = Refl

symmetric : a = b -> b = a
symmetric Refl = Refl

substitution : {t1:Type} -> {t2:Type} -> {a:t1} -> {b:t1} -> {c:t2} -> (f:t1 -> t2) -> a = b -> f a = c -> f b = c
substitution _ Refl Refl = Refl

max_stars_repo_name: identicalsnowflake/neweden

max_issues_repo_name: identicalsnowflake/neweden

max_forks_repo_name: identicalsnowflake/neweden


text:
module Main

-- base
import Data.Fin
import Data.List
import Data.Strings
import Data.Vect
import System.File

--contrib
import Text.Lexer
import Text.Lexer.Core
import Text.Parser
import Text.Parser.Core

record FieldConstraint where
  constructor MkFieldConstraint
  field : String
  isValid : Nat -> Bool

Show FieldConstraint where
  show (MkFieldConstraint field isValid) =
    "FieldConstraint " ++ show field ++ " lambda"

namespace Parsing
  data DataKind = DKWord
                | DKNat
                | DKSpace
                | DKColon
                | DKMinus
                | DKOr
                | DKComma
                | DKNewline

  Eq DataKind where
    DKWord == DKWord = True
    DKNat == DKNat = True
    DKSpace == DKSpace = True
    DKColon == DKColon = True
    DKMinus == DKMinus = True
    DKOr == DKOr = True
    DKComma == DKComma = True
    DKNewline == DKNewline = True
    _ == _ = True

  Show DataKind where
    show DKWord = "DKWord"
    show DKNat = "DKNat"
    show DKSpace = "DKSpace"
    show DKColon = "DKColon"
    show DKMinus = "DKMinus"
    show DKOr = "DKOr"
    show DKComma = "DKComma"
    show DKNewline = "DKNewline"

  TokenKind DataKind where
    TokType DKWord = String
    TokType DKNat = Nat
    TokType _ = ()
    tokValue DKWord x = x
    tokValue DKNat x = integerToNat $ cast x
    tokValue DKSpace _ = ()
    tokValue DKColon _ = ()
    tokValue DKMinus _ = ()
    tokValue DKOr _ = ()
    tokValue DKComma _ = ()
    tokValue DKNewline _ = ()

  export
  tokenMap : TokenMap $ Token DataKind
  tokenMap = toTokenMap
    [ (is ':', DKColon)
    , (is '-', DKMinus)
    , (exact "or", DKOr)
    , (is ',', DKComma)
    , (newline, DKNewline)
    , (spaces, DKSpace)
    , (alphas, DKWord)
    , (digits, DKNat)
    ]

  -- NOTE TO SELF!!!
  -- It's important to keep the consuming Bool of Grammar True, when one want to keep parsing!!!

  -- Needs to end with DKColon
  wordsGrammar : Grammar (Token DataKind) True (List String)
  wordsGrammar = do
    w <- match DKWord
    n <- peek
    case kind n of
         DKSpace => do
           match DKSpace
           ws <- wordsGrammar
           pure $ w :: ws
         DKColon => do
           match DKColon
           pure [ w ]
         _ => fail "Expecting words"

  fieldConstraintGrammar : Grammar (Token DataKind) True FieldConstraint
  fieldConstraintGrammar = do
    field <- unwords <$> wordsGrammar
    match DKSpace
    xMin <- match DKNat
    match DKMinus
    xMax <- match DKNat
    match DKSpace
    match DKOr
    match DKSpace
    yMin <- match DKNat
    match DKMinus
    yMax <- match DKNat
    match DKNewline
    let constraint : Nat -> Bool
        constraint a = a >= xMin && a <= xMax || a >= yMin && a <= yMax
    pure $ MkFieldConstraint field constraint

  ticketGrammar : Grammar (Token DataKind) True (List Nat)
  ticketGrammar = do
    n <- match DKNat
    o <- peek
    case kind o of
         DKComma => do
           match DKComma
           ns <- ticketGrammar
           pure $ n :: ns
         DKNewline => do
           match DKNewline
           pure [ n ]
         _ => fail "Expecting Nats"

  export
  dataGrammar : Grammar (Token DataKind) True (List FieldConstraint, List Nat, List $ List Nat)
  dataGrammar = do
    fieldConstraints <- many fieldConstraintGrammar
    match DKNewline
    wordsGrammar -- match "your ticket:"
    match DKNewline
    myTicket <- ticketGrammar
    match DKNewline
    wordsGrammar -- match "nearby tickets:"
    match DKNewline
    nearbyTickets <- many ticketGrammar
    eof
    pure (fieldConstraints, myTicket, nearbyTickets)

namespace Part1
  zipper : List (a -> b) -> List a -> List b
  zipper [] ys = []
  zipper xs [] = []
  zipper (x::xs) (y::ys) = x y :: zipper xs ys

  export
  countTicketErrors : (fieldConstraints : List FieldConstraint) -> (fields : List Nat) -> List Nat
  countTicketErrors fieldConstraints fields =
    map fst $ filter (not . snd) $ map g $ f (isValid <$> fieldConstraints) <$> fields where
      f : List (Nat -> Bool) -> Nat -> (Nat,List Bool)
      f fs n = (n,fs <*> pure n)
      any : List Bool -> Bool
      any [] = False
      any (True::xs) = True
      any (False::xs) = any xs
      g : (Nat,List Bool) -> (Nat,Bool)
      g (n,bs) = (n, any bs)

  export
  removeWhenTicketError : (fieldConstraints : List FieldConstraint) -> (fieldss : List (List Nat)) -> List (List Nat)
  removeWhenTicketError fieldConstraints fieldss =
    catMaybes $ zipWith removeWhenErr errss fieldss where
      errss : List $ List Nat
      errss = countTicketErrors fieldConstraints <$> fieldss
      removeWhenErr : (err : List Nat) -> (fields : List Nat) -> Maybe (List Nat)
      removeWhenErr [] fields = Just fields
      removeWhenErr _ _ = Nothing

namespace Part2
  fromList : (n : Nat) -> List a -> Maybe (Vect n a)
  fromList Z [] = Just []
  fromList Z (_::_) = Nothing
  fromList (S k) [] = Nothing
  fromList (S k) (x::xs) = [| pure x :: fromList k xs |]

  export
  fromLists : (n : Nat) -> (xss : List (List a)) -> Maybe (List (Vect n a))
  fromLists n [] = Just []
  fromLists n (xs :: xss) = [| fromList n xs :: fromLists n xss  |]

  -- outside Vect for numbers, inside Vect for constraints
  export
  areValid : {n : Nat} -> (fieldConstraints : Vect n FieldConstraint) -> (numbers : Vect n Nat) -> Vect n (Vect n (Bool))
  areValid fieldConstraints numbers =
    ((isValid <$> fieldConstraints) <*>) <$> (pure <$> numbers)

  vectAnd : Vect n Bool -> Vect n Bool -> Vect n Bool
  vectAnd [] [] = []
  vectAnd (True::xs) (True::ys) = True :: vectAnd xs ys
  vectAnd (_::xs) (_::ys) = False :: vectAnd xs ys

  -- outside Vect for constraints, inside Vect for numbers
  vectVectAnd : {n : Nat} -> Vect n (Vect n Bool) -> Vect n (Vect n Bool) -> Vect n (Vect n Bool)
  vectVectAnd xs ys = vectAnd <$> xs <*> ys

  export
  foldVectAnd : {n : Nat} -> List (Vect n (Vect n Bool)) -> Vect n (Vect n Bool)
  foldVectAnd bs = foldl vectVectAnd (pure (pure True)) bs

  allFins : {n : Nat} -> List $ Fin n
  allFins with (n)
    allFins | Z = []
    allFins | (S k) = FZ :: (FS <$> allFins)

  export
  workingIndices : {n : Nat} -> Vect n Bool -> List (Fin n)
  workingIndices [] = []
  workingIndices xs = catMaybes $ zipWith f (toList xs) allFins where
    f : Bool -> Fin n -> Maybe $ Fin n
    f True x = Just x
    f False x = Nothing

  export
  workingIndicess : {n : Nat} -> Vect n (Vect n Bool) -> Vect n (List (Fin n))
  workingIndicess xss = workingIndices <$> xss

  maxByLen : (max : Maybe (Nat,(a,List a))) -> List (Lazy (a,(List a))) -> Maybe (a,List a)
  maxByLen Nothing [] = Nothing
  maxByLen (Just (maxN,maxV)) [] = Just maxV
  maxByLen Nothing ((vv,vl)::vs) = maxByLen (Just (length vl,(vv,vl))) vs
  maxByLen (Just (maxN,maxV)) ((vv,vl)::vs) = if length vl > maxN
                                                 then maxByLen (Just (length vl,(vv,vl))) vs
                                                 else maxByLen (Just (maxN,maxV)) vs

  export
  sudoku : {n : Nat} -> (rows : List (List (Fin n))) -> (taken : List (Fin n)) -> List (Fin n)
  sudoku [] _ = []
  sudoku (row::rows) taken =
    case next of
         Nothing => []
         Just (x,xs) => x :: xs
    where
      f : Fin n -> Maybe (List (Fin n))

      notTaken : Fin n -> Bool
      notTaken x = not $ x `elem` taken

      finsToTry : List (Fin n)
      finsToTry = filter notTaken row

      sudokuNext : Fin n -> Lazy (Fin n,List (Fin n))
      sudokuNext x = (x,sudoku rows (x :: taken))

      nexts : List $ Lazy (Fin n, List $ Fin n)
      nexts = sudokuNext <$> finsToTry

      next : Maybe (Fin n,List (Fin n))
      next = maxByLen Nothing nexts

  export
  indexMaybe : Nat -> List a -> Maybe a
  indexMaybe _ [] = Nothing
  indexMaybe Z (x::xs) = Just x
  indexMaybe (S k) (_::xs) = indexMaybe k xs

main : IO ()
main = do
  inputData <- readFile "./data"
  case inputData of
       (Left err) => print err
       (Right inputData) => do
         let (tokens, debugLexed) = lex tokenMap inputData
             parsed = parse dataGrammar $ tok <$> tokens
         case parsed of
              Left (Error err _) => putStrLn err
              Right ((fieldConstraints, myTicket, nearbyTickets), debugParsed) => do
                let ticketErrors = countTicketErrors fieldConstraints <$> nearbyTickets
                    ans1 = sum $ concat ticketErrors
                --print ans1
                let safeNearbyTickets = removeWhenTicketError fieldConstraints nearbyTickets
                    fieldConstraints' = fromList fieldConstraints
                    safeNearbyTickets' = fromLists (length fieldConstraints) safeNearbyTickets
                case safeNearbyTickets' of
                     Nothing => pure ()
                     Just safeNearbyTickets' => do
                                 -- constraints outside, numbers inside
                       --let valids' = transpose <$> areValid fieldConstraints' <$> safeNearbyTickets'
                       --    valids = foldVectAnd valids'
                       --    validIndices = workingIndicess valids
                       --    --sol2 = sudoku (toList $ map toList validIndices) []
                       let sol2 : List Nat
                           sol2 = [5, 1, 8, 2, 15, 11, 17, 16, 0, 6, 4, 7, 18, 12, 10, 14, 19, 3, 13, 9]
                           inds : List Nat
                           inds = take 6 sol2
                       let nums = indexMaybe <$> inds <*> pure myTicket
                       print $ map product $ sequence $ nums
                       pure ()
                pure ()
         pure ()
  pure ()


text:
module Sif.Pattern.Convert

import Data.GraphViz.SimpleDot

import Edda
import Edda.Writer.Org
import Edda.Writer.LaTeX
import Edda.Writer.CommonMark

import XML.DOM

import Freyja
import Freyja.Convert.XML

import Sif.Types
import Sif.Pattern.Model
import Sif.Pattern.API
import Sif.Pattern.Convert.XML
import Sif.Pattern.Convert.Edda
import Sif.Pattern.Convert.String
import Sif.Pattern.Convert.Freyja

%default partial
%access export

covering
public export
convTy : SifOutFormat -> Type
convTy LATEX   = String
convTy CMARK   = String
convTy ORG     = String
convTy XML     = XMLDoc
convTy DOT     = SimpleDot GRAPH
convTy EDDA    = EddaDoc
convTy COMPACT = String
convTy IDRIS   = String
convTy STRING  = String
convTy FREYJA  = XMLDoc

covering
convTo : (fmt : SifOutFormat) -> PATTERN impl d -> Maybe (convTy fmt)
convTo FREYJA  p = Just $ Freyja.toXML (toFreyja p)

convTo XML     p = Just $ toXML p
convTo EDDA    p = Just $ toEdda p
convTo ORG     p = Just $ org $ toEdda p
convTo LATEX   p = Just $ latex $ toEdda p
convTo CMARK   p = Just $ markdown $ toEdda p

convTo COMPACT p = Just $ Sif.toString p
convTo STRING  p = Just $ Sif.toString p

convTo DOT     p = Nothing

convTo IDRIS   p = Nothing

||| o'rrible code
covering
showConvPattern : SifOutFormat -> PATTERN impl d ->  Maybe String
showConvPattern DOT p =
  case (the (Maybe (convTy DOT)) (convTo DOT p)) of
    Nothing => Nothing
    Just r  => Just (show r)

showConvPattern FREYJA p =
  case (the (Maybe (convTy FREYJA)) (convTo FREYJA p)) of
    Nothing => Nothing
    Just r  => Just (show @{xml} r)

showConvPattern XML p =
  case (the (Maybe (convTy XML)) (convTo XML p)) of
    Nothing => Nothing
    Just r  => Just (show @{xml} r)

showConvPattern ORG p =
  case (the (Maybe (convTy ORG)) (convTo ORG p)) of
    Nothing => Nothing
    Just r  => Just r

showConvPattern CMARK p =
  case (the (Maybe (convTy CMARK)) (convTo CMARK p)) of
    Nothing => Nothing
    Just r  => Just r

showConvPattern LATEX p =
  case (the (Maybe (convTy LATEX)) (convTo LATEX p)) of
    Nothing => Nothing
    Just r  => Just r

showConvPattern COMPACT p =
  case (the (Maybe (convTy COMPACT)) (convTo COMPACT p)) of
    Nothing => Nothing
    Just r  => Just r

showConvPattern STRING p =
  case (the (Maybe (convTy STRING)) (convTo STRING p)) of
    Nothing => Nothing
    Just r  => Just r

showConvPattern _ _ = Nothing

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
||| Various utility combinators.
|||
||| A note on arrow operators: Arrow operators in this module are
||| of the form `i>o`, where `i` is either `>`, `^`, `!`, or `?`.
||| and `o` is either `>`, `^`, `!`, or `-`. Each of these symbols
||| describe a different type of arrow-like function at the
||| corresponding end of the operator:
|||
||| The following table lists the meaning of symbols
|||
||| | Symbol      | Meaning                  | Example                    |
||| |-------------|--------------------------|----------------------------|
||| | `>`         | An MSF                   | arr (*2) >>> arrM printLn  |
||| | `^`         | a pure function          | (*2) ^>> printLn           |
||| | `!`         | an effectful computation | arr (*2) >>! printLn       |
|||
||| In addition, symbol `?` corresponds to an event stream input, and
||| symbol `-` describes fanning out to a list of sinks:
|||
||| ```idris example
||| when (> 10) ?>- [ arrM printLn, put ]
||| ```
module Data.MSF.Util

import Data.List
import Data.MSF.Core
import Data.MSF.Event
import Data.SOP

--------------------------------------------------------------------------------
--          Sequencing Utilities
--------------------------------------------------------------------------------

infixr 1 ^>>, >>^, >>!, !>>, ?>>, >>-, ^>-, !>-, ?>-

||| Sequencing of an MSF and a pure function
export %inline
(>>^) : MSF m i o -> (o -> o2) -> MSF m i o2
sf >>^ f = sf >>> arr f

||| Sequencing of a pure function and an MSF
export %inline
(^>>) : (i -> i2) -> MSF m i2 o -> MSF m i o
f ^>> sf = arr f >>> sf

||| Sequencing of an MSF and an effectful computation
export %inline
(>>!) : MSF m i o -> (o -> m o2) -> MSF m i o2
sf >>! f = sf >>> arrM f

||| Sequencing of an effectful computation and an MSF
export %inline
(!>>) : (i -> m i2) -> MSF m i2 o -> MSF m i o
f !>> sf = arrM f >>> sf

--------------------------------------------------------------------------------
--          Paralellising Utilities
--------------------------------------------------------------------------------

||| Like `fan` but discards the results.
||| This is mainly useful for broadcasting to data sinks
||| (streaming functions that do not produce any interesting
||| output).
|||
||| TODO: Should we require a proof here that `os` is a list
|||       of `Unit`?
export %inline
fan_ : FanList m i os -> MSF m i ()
fan_ sfs = Fan sfs >>> Const ()

||| Broadcasting an MSF to a list of sinks
export %inline
(>>-) : MSF m i x -> FanList m x os -> MSF m i ()
sf >>- sfs = sf >>> fan_ sfs

||| Broadcasting a pure function to a list of sinks
export %inline
(^>-) : (i -> x) -> FanList m x os -> MSF m i ()
f ^>- sfs = arr f >>> fan_ sfs

||| Broadcasting an effectful computation to a list of sinks
export %inline
(!>-) : (i -> m x) -> FanList m x os -> MSF m i ()
f !>- sfs = arrM f >>> fan_ sfs

||| Extract the first argument from an MSF taking a pair
||| of input values.
export
firstArg : MSF m (NP I [x,i]) o -> x -> MSF m i o
firstArg sf vx = fan [const vx, id] >>> sf

||| Extract the second argument from an MSF taking a pair
||| of input values.
export
secondArg : MSF m (NP I [i,x]) o -> x -> MSF m i o
secondArg sf vx = fan [id, const vx] >>> sf

||| Extract the first value of an n-ary product
export
hd : MSF m (NP I (i :: t)) i
hd = arr hd

||| Extract the tail of an n-ary product
export
tl : MSF m (NP I (i :: t)) (NP I t)
tl = arr tl

||| Extract the second value of an n-ary product
export
snd : MSF m (NP I (i :: i2 :: t)) i2
snd = arr $ \(_ :: v :: _) => v

||| Swaps a pair of input values
export
swap : MSF m (NP I [a,b]) (NP I [b,a])
swap = arr $ \[va,vb] => [vb,va]

--------------------------------------------------------------------------------
--          Selecting Utilities
--------------------------------------------------------------------------------

||| Convert an `Either` input to a binary sum, which
||| can then be sequenced with a call to `choice` or `collect`.
export
either : MSF m (Either i1 i2) (NS I [i1,i2])
either = arr $ either Z (S . Z)

||| Run the given MSF only if the input is a `Left`.
export
ifLeft : Monoid o => MSF m i o -> MSF m (Either i a) o
ifLeft sf = either >>> collect [sf, neutral]

||| Run the given MSF only if the input is a `Right`.
export
ifRight : Monoid o => MSF m i o -> MSF m (Either a i) o
ifRight sf = either >>> collect [neutral, sf]

||| Convert an `Maybe` input to a binary sum, which
||| can then be sequenced with a call to `choice` or `collect`.
export
maybe :  MSF m (Maybe i) (NS I [i,()])
maybe = arr $ maybe (S $ Z ()) Z

||| Run the given MSF only if the input is a `Just`.
export
ifJust : Monoid o => MSF m i o -> MSF m (Maybe i) o
ifJust sf = maybe >>> collect [sf, neutral]

||| Run the given MSF only if the input is a `Nothing`.
export
ifNothing : Monoid o => MSF m () o -> MSF m (Maybe i) o
ifNothing sf = maybe >>> collect [neutral, sf]

||| Convert an input to a binary sum, depending on whether
||| the given predicate returns `True` or `False`. The result
||| can then be sequenced with a call to `choice` or `collect`.
export
bool : (f : i -> Bool) -> MSF m i (NS I [i,i])
bool f = arr $ \vi => if f vi then Z vi else (S $ Z vi)

||| Run the given MSF only if the predicate holds for the input.
export
ifTrue : Monoid o => (f : i -> Bool) -> MSF m i o -> MSF m i o
ifTrue f sf = bool f >>> collect [sf, neutral]

||| Run the given MSF only if the predicate does not hold for the input.
export
ifFalse : Monoid o => (f : i -> Bool) -> MSF m i o -> MSF m i o
ifFalse f sf = bool f >>> collect [neutral, sf]

||| Run the given MSF only if the input equlas the given value
export
ifIs : Eq i => Monoid o => (v : i) -> MSF m i o -> MSF m i o
ifIs v = ifTrue (v ==)

||| Run the given MSF only if the input does not equal the given value
export
ifIsNot : Eq i => Monoid o => (v : i) -> MSF m i o -> MSF m i o
ifIsNot v = ifFalse (v ==)

--------------------------------------------------------------------------------
--          Looping Utilities
--------------------------------------------------------------------------------

||| Uses the given value as a seed for feeding back output
||| of the MSF back to its input.
export
feedback_ : s -> MSF m (NP I [s,i]) s -> MSF m i ()
feedback_ v sf = feedback v $ sf >>^ (:: [()])

||| Delay a stream by one sample.
export %inline
iPre : o -> MSF m o o
iPre v = feedback v swap

||| Applies a function to the input and an accumulator,
||| outputting the updated accumulator.
export
accumulateWith : (i -> o -> o) -> o -> MSF m i o
accumulateWith f ini = feedback ini (arr g)
  where g : NP I [o,i] -> NP I [o,o]
        g [acc,inp] = let acc' = f inp acc in [acc',acc']

||| Counts the number of scans of the signal function.
export
count : Num n => MSF m i n
count = const 1 >>> accumulateWith (+) 0

||| Accumulate the inputs, starting from an initial value.
export
appendFrom : Semigroup v => v -> MSF m v v
appendFrom = accumulateWith (<+>)

||| Accumulate the inputs, starting from `neutral`
export
append : Monoid n => MSF m n n
append = appendFrom neutral

||| Applies a transfer function to the input and an accumulator,
||| returning the updated accumulator and output.
export
mealy : (i -> s -> NP I [s,o]) -> s -> MSF m i o
mealy f s0 = feedback s0 (arr $ \[s,i] => f i s)

||| Unfolds a function over an initial state
||| value.
export
unfold : (s -> NP I [s,o]) -> s -> MSF m i o
unfold f ini = feedback ini (arr $ f . hd)

||| Generates output using a step-wise generation function and an initial
||| value. Version of 'unfold' in which the output and the new accumulator
||| are the same.
export
repeatedly : (o -> o) -> o -> MSF m i o
repeatedly f = unfold $ \vo => let vo2 = f vo in [vo2,vo2]

||| Cycles through the given non-empty list of values.
export
cycle : (vs : List o) -> {auto 0 prf : NonEmpty vs} -> MSF m i o
cycle (h :: t) = unfold next (h :: t)
  where next : List o -> NP I [List o, o]
        next Nil        = [t,h]
        next (h' :: t') = [t',h']

--------------------------------------------------------------------------------
--          Observing Streaming Functions
--------------------------------------------------------------------------------

||| Observe input values through the given MSF, discarding
||| its output.
export
observeWith : MSF m i o -> MSF m i i
observeWith sf = fan [id,sf] >>> hd

||| Run the given effectful computation on each input.
export %inline
withEffect : (i -> m ()) -> MSF m i i
withEffect = observeWith . arrM

||| Run the given monadic action on each input.
export %inline
runEffect : m () -> MSF m i i
runEffect = withEffect . const

--------------------------------------------------------------------------------
--          Event Streams
--------------------------------------------------------------------------------

||| The empty event stream that never fires an event
export
never : MSF m i (Event o)
never = const NoEv

||| Convert an event stream to a streaming function
||| holding the value of the last event fired starting
||| from the given initial value.
export
hold : o -> MSF m (Event o) o
hold = accumulateWith (\ev,v => fromEvent v ev)

||| Fire the given event `n` times.
export
ntimes : Nat -> o -> MSF m i (Event o)
ntimes n vo = Switch (feedback n $ arr next) (const never)
  where next : NP I [Nat,i] -> NP I [Nat,Either () (Event o)]
        next [0,_]   = [0, Left ()]
        next [S k,_] = [k, Right $ Ev vo]

||| Fire the given event exactly once on the first
||| evaluation step.
export
once : o -> MSF m i (Event o)
once = ntimes 1

||| Fire an event whenever the given predicate holds.
export
when : (i -> Bool) -> MSF m i (Event i)
when f = arr $ \vi => toEvent (f vi) vi

||| Like `when` but discard the input.
export
when_ : (i -> Bool) -> MSF m i (Event ())
when_ f = arr $ \vi => toEvent (f vi) ()

||| Fire an event whenever the input equals the given value.
export
is : Eq i => i -> MSF m i (Event i)
is v = when (v ==)

||| Fire an event whenever the input does not equal the given value.
export
isNot : Eq i => i -> MSF m i (Event i)
isNot v = when (v /=)

||| Fire an event if the input is a `Left`.
export
whenLeft : MSF m (Either a b) (Event a)
whenLeft = arr $ either Ev (const NoEv)

||| Fire an event if the input is a `Right`.
export
whenRight : MSF m (Either a b) (Event b)
whenRight = arr $ either (const NoEv) Ev

||| Fire an event if the input is a `Just`.
export
whenJust : MSF m (Maybe a) (Event a)
whenJust = arr maybeToEvent

||| Fire an event if the input is a `Nothing`.
export
whenNothing : MSF m (Maybe a) (Event ())
whenNothing = arr $ maybe (Ev ()) (const NoEv)

||| Convert an `Event` input to a binary sum, which
||| can then be sequenced with a call to `choice` or `collect`.
export
event :  MSF m (Event i) (NS I [i,()])
event = arr $ event (S $ Z ()) Z

||| Run the given MSF only if the input fired an event.
export
ifEvent : Monoid o => MSF m i o -> MSF m (Event i) o
ifEvent sf = event >>> collect [sf, const neutral]

||| Broadcast an event to a list of sinks.
export %inline
(?>-) : MSF m i (Event x) -> FanList m x os -> MSF m i ()
ef ?>- sfs = ef >>> ifEvent (fan_ sfs)

||| Run the given MSF if the input stream fires and event.
export %inline
(?>>) : Monoid o => MSF m i (Event x) -> MSF m x o -> MSF m i o
ef ?>> sf = ef >>> ifEvent sf

||| Run the given MSF only if the input fired no event.
export
ifNoEvent : Monoid o => MSF m () o -> MSF m (Event i) o
ifNoEvent sf = event >>> collect [const neutral, sf]

||| Fire an event whenever the input value changed.
||| Always fires on first input.
export
onChange : Eq i => MSF m i (Event i)
onChange = mealy accum  NoEv
  where accum : i -> Event i -> NP I [Event i, Event i]
        accum v old =
          let ev = Ev v
           in if ev == old then [ev,NoEv] else [ev,ev]

||| Fires the first input as an event whenever the
||| second input fires.
export
onEvent : MSF m (NP I [a, Event e]) (Event a)
onEvent = arr $ \case [va,e] => e $> va

||| Combines the first input with the event fired by the
||| second input.
export
onEventWith : (a -> e -> b) -> MSF m (NP I [a, Event e]) (Event b)
onEventWith f = arr $ \case [va,e] => f va <$> e

||| Combines an input event stream with a stream function
||| holding an `Either` trying to extract a `Left` whenever
||| an event is fired.
export
leftOnEvent : MSF m (NP I [Either a b, Event e]) (Event a)
leftOnEvent = arr $ \case [Left va,e] => e $> va
                          _           => NoEv

||| Combines an input event stream with a stream function
||| holding an `Either` trying to extract a `Right` whenever
||| an event is fired.
export
rightOnEvent : MSF m (NP I [Either a b, Event e]) (Event b)
rightOnEvent = arr $ \case [Right vb,e] => e $> vb
                           _            => NoEv

||| Combines an input event stream with a stream function
||| holding a `Maybe` trying to extract the value from a `Just` whenever
||| an event is fired.
export
justOnEvent : MSF m (NP I [Maybe a, Event e]) (Event a)
justOnEvent = arr $ \case [Just va,e] => e $> va
                          _           => NoEv

--------------------------------------------------------------------------------
--          Merging Event Streams
--------------------------------------------------------------------------------

||| Fires an event whenever one of the two given
||| event streams fire. Uses the given function
||| to combine simultaneously occuring events.
export
unionWith : (o -> o -> o)
          -> MSF m i (Event o)
          -> MSF m i (Event o)
          -> MSF m i (Event o)
unionWith = elementwise2 . unionWith

||| Left-biased union of event streams.
||| In case of simultaneously occuring events, the
||| event from the first event stream is fired.
|||
||| This is the same behavior as `(<|>)` from
||| the MSFs `Alternative` implementation
export
unionL : MSF m i (Event o) -> MSF m i (Event o) -> MSF m i (Event o)
unionL = elementwise2 unionL

||| Right-biased union of event streams.
||| In case of simultaneously occuring events, the
||| event from the second event stream is fired.
export
unionR : MSF m i (Event o) -> MSF m i (Event o) -> MSF m i (Event o)
unionR = elementwise2 unionR

||| Union of event streams using a `Semigroup` to
||| merge values in case of simultaneously occuring events.
|||
||| This is an alias for `(<+>)`.
export %inline
union :  Semigroup o
      => MSF m i (Event o)
      -> MSF m i (Event o)
      -> MSF m i (Event o)
union = (<+>)

export
(<|>) : Alternative f => MSF m i (f o) -> MSF m i (f o) -> MSF m i (f o)
x <|> y = fan [x,y] >>> arr (\[vx,vy] => vx <|> vy)

--------------------------------------------------------------------------------
--          Filtering Event Streams
--------------------------------------------------------------------------------

||| Filters an event stream, letting pass only values,
||| fow which the given predicate holds.
export
filter : (o -> Bool) -> MSF m (Event o) (Event o)
filter = arr . filter

||| Filters an event stream, letting pass only values,
||| fow which the given function returns a `Just`.
export
mapMaybe : (i -> Maybe o) -> MSF m (Event i) (Event o)
mapMaybe = arr . mapMaybe

--------------------------------------------------------------------------------
--          Accumulating Events
--------------------------------------------------------------------------------

||| Applies a function to the input and an accumulator,
||| outputting the updated accumulator whenever an
||| event is fire.
export
accumulateWithE : (i -> o -> o) -> o -> MSF m (Event i) (Event o)
accumulateWithE f ini = feedback ini (arr g)
  where g : NP I [o,Event i] -> NP I [o,Event o]
        g [acc,NoEv]  = [acc,NoEv]
        g [acc,Ev vi] = let acc' = f vi acc in [acc',Ev acc']

||| Count the number of occurences of an event
export
countE : MSF m (Event i) (Event Nat)
countE = accumulateWithE (\_,n => n + 1) 0

--------------------------------------------------------------------------------
--          Handling with n-ary Products
--------------------------------------------------------------------------------

||| N-ary function type calculated from a list of n types.
public export
0 Fun : List Type -> Type -> Type
Fun [] r        = r
Fun (t :: ts) r = t -> Fun ts r

||| Converts an n-ary function to one taking an n-ary
||| product as input.
export
uncurryNP : {0 is : _} -> Fun is o -> NP I is -> o
uncurryNP r []        = r
uncurryNP f (v :: vs) = uncurryNP (f v) vs

||| Alias for `arr . uncurryNP`.
export
np : {0 is : _} -> Fun is o -> MSF m (NP I is) o
np = arr . uncurryNP


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

Let's represent towers as towers of one less degree where the highest-degree holes are now contained in the islands.

So

  ^`( ~`( ,( ,( ) ) ) )

is to be represented like so:

  `( something ,( ) something )

Islands must have an overall balanced structure to them. The first "something" island opens the higher-degree hole, and the second "something" closes it. A single island may close and open many holes, and it may even dip into a hole without closing it, like the middle part of this:

  ^`( ~`( ,( ,( ) ) ,( ,( ) ) ) )
   `( ------ ,( ) ---- ,( ) --- )

As a lower-degree example,

  `( ,( ) )

is to be represented like so:

  ( something )

Clearly, everything at that degree will be represented as "( something )" for some value of "something," so that can be the base case of our representation.

exprOf : Nat -> Type -> Type
exprOf d i = Expr d 0 (\_ _ -> ()) i

exprBranchType :
  (d : Nat) -> (c : Nat -> Nat -> Type) -> (i : Type) -> Type
exprBranchType =
  (nextStartingDepth : Nat) *
  (i * exprOf d (Expr (1 + d) nextStartingDepth c i))

exprMap :
  (d : Nat) ->
  (startingDepth : Nat) ->
  (c : Nat -> Nat -> Type) ->
  (i : Type) ->
  (i' : type) ->
  (i -> i') ->
  Expr d startingDepth c i ->
  Expr d startingDepth c i'
exprMap d startingDepth c i i' f expr = case expr of
  exprNil d'' s'' c'' i'' content'' =>
    exprNil d'' s'' c'' i' content''
  exprCons d'' startingDepth'' c'' i'' branches'' content'' =>
    exprCons d'' startingDepth'' c'' i'
      (exprMap d'' startingDepth'' c''
        (exprBranchType d'' c'' i'')
        (exprBranchType d'' c'' i')
        (\(nextStartingDepth * (iVal * branches)) ->
          nextStartingDepth *
          (f iVal *
            exprMap d'' 0 (\_ _ -> ())
              (Expr d nextStartingDepth c'' i'')
              (Expr d nextStartingDepth c'' i')
              (exprMap d nextStartingDepth c'' i'' i' f)
              branches))
        branches'')

type Expr
  (degree : Nat)
  (startingDepth : Nat)
  (content : Nat -> exprOf d Nat -> Type)
  (interpolation : Type)
where
  exprNil :
    (d : Nat) ->
    (s : Nat) ->
    (c : Nat -> exprOf d Nat -> Type) ->
    (i : Type) ->
    c s (exprNil d 0 (\_ _ -> ()) Nat) ->
    Expr (1 + d) s c i
  exprCons :
    (d : Nat) ->
    (startingDepth : Nat) ->
    (c : Nat -> Nat -> Type) ->
    (i : Type) ->
    (branches : exprOf d (exprBranchType d c i)) ->
    c startingDepth
      (exprMap d 0 (\_ _ -> ()) (exprBranchType d c i) Nat
        (\(nextStartingDepth * _) -> nextStartingDepth)
        branches) ->
    Expr (1 + d) startingDepth c i

-- TODO: Whoops, the above `Expr` has no constructors for degree 0,
-- and its constructors for degrees greater than 0 aren't using island
-- content values to represent higher-degree holes. Finish making a
-- version of expr which does this, below.

vec : Nat -> Type -> Type
vec n t = case n of
  0 => () * ()
  1 + n' => t * vec n' t

exprInfoType : Nat -> Type
exprInfoType degree = case degree of
  0 =>
    (balanceStateType : Type) *
    let bl = List balanceStateType in
    (bl -> () -> Type) *
    (bl -> () -> Type)
  1 + degree' =>
    (balanceStateType : Type) *
    let bl = List balanceStateType in
    (bl -> exprOf degree' bl -> Type) *
    (bl -> exprOf degree' bl -> Type)

type List (a : Type) where
  nil : (a : Type) -> List a
  cons : (a : Type) -> a -> List a -> List a

exprInfo :
  (degree : Nat) ->
  (balanceStateType0 : Type) ->
  (List balanceStateType0 -> Type) ->
  (List balanceStateType0 -> Type) ->
  exprInfoType degree
exprInfo degree balanceStateType0 i0 l0 = case degree of
  0 =>
    balanceStateType0 *
    (\currentBalance () -> i0 currentBalance) *
    (\currentBalance () -> l0 currentBalance)
  1 + degree' =>
    let
      balanceStateTypeN * iN * lN =
        exprInfo degree' balanceStateType0 i0 l0
    in
    List balanceStateTypeN *
    (\currentBalance edge ->
      Expr degree'
        (balanceStateTypeN * iN *
          (\currentBalance edge ->
            (case currentBalance of
              nil subBalanceType => Bot
              cons subBalanceType subBalance subBalances =>
                exprOf degree'
                  ( (E) +
                    ())) +
            ())
        (nil balanceStateTypeN)) *
    (\currentBalance edge -> ())

island : Nat -> (balanceStateType : Type) -> balanceStateType -> Type
island degree balanceStateType startingBalance =
  Expr degree Nat c'

type Expr
  (degree : Nat)
  (balanceStateType * i * l * ti : exprInfoType degree)
  List balanceStateType
where
  expr :
    (d : Nat) ->
    (balanceStateType : Type) ->
    (balanceStateType * i * l * ti : exprInfoType d) ->
    (startingBalance : List balanceStateType) ->
    (case d of
      0 => () * i startingBalance ()
      1 + d' =>
        let balanceStateType' * i' * l' * ti' = ti in
        (e : Expr d' ti
          (
          -- TODO: Implement island.
          (island d' balanceStateType c (lakeType * lakeTypes)
            startingBalance)
          lakeTypes
          0) *
        i startingBalance
          -- TODO: Implement exprMap, and pass it whatever other
          -- arguments it needs here.
          (exprMap
            (\newStartingBalance lake -> newStartingBalance)
            e)) ->
    Expr d balanceStateType c (lakeType * lakeTypes) startingBalance

 that degree we only have a single "something" in the representation no

max_stars_repo_name: rocketnia/lexmeta

max_issues_repo_name: rocketnia/lexmeta

max_forks_repo_name: lathe/punctaffy-for-racket


text:
module Toml.Parser

import Data.List
import Data.List1
import Extra.List
import Text.Parser
import Text.Token
import Toml.Data
import Toml.Lexer

import public Toml.Tokens

comment : Grammar _ TomlToken True (Maybe (List String, Value))
comment =
  map (const Nothing) (match Comment)

whitespace : Grammar _ TomlToken True (Maybe (List String, Value))
whitespace =
  map (const Nothing) (match Whitespace)

optWhitespace : Grammar _ TomlToken False ()
optWhitespace = ignore $ optional $ match Whitespace

keyword : Grammar _ TomlToken True (List String)
keyword =
  forget <$> sepBy1 (match Dot) (match Keyword <|> match StringLit <|> (map show $ match Number))

heading : Grammar _ TomlToken True (List String)
heading =
  do
    match LeftBracket
    optWhitespace
    key <- keyword
    optWhitespace
    match RightBracket
    pure key

doubleHeading : Grammar _ TomlToken True (List String)
doubleHeading =
  do
    match LeftBracket
    match LeftBracket
    optWhitespace
    key <- keyword
    optWhitespace
    match RightBracket
    match RightBracket
    pure key

doubleHeadingOf : List String -> Grammar _ TomlToken True String
doubleHeadingOf lookup =
  do
    key <- doubleHeading
    the (Grammar _ _ False _) $
      if key == lookup
        then pure "hi"
        else fail "mismatched double heading"

str : Grammar _ TomlToken True Value
str =
  map Str (match StringLit)

num : Grammar _ TomlToken True Value
num =
  map Num (match Number)

optSpacing : Grammar state TomlToken True a -> Grammar state TomlToken True a
optSpacing inner =
  do
    optWhitespace
    res <- inner
    optWhitespace
    pure res

mutual
  list : Grammar state TomlToken True Value
  list =
    do
      ignore $ match LeftBracket
      values <- sepBy (optSpacing $ match Comma) value
      ignore $ match RightBracket
      pure (Lst values)

  value : Grammar _ TomlToken True Value
  value =
    optSpacing $ str <|> num <|> list

kv : Grammar _ TomlToken True (Maybe (List String, Value))
kv =
  do
    key <- keyword
    optWhitespace
    match Equals
    optWhitespace
    v <- value
    pure $ Just (key, v)

mutual
  subtable : Grammar _ TomlToken True (List (List String, Value))
  subtable =
    do
      key <- doubleHeading
      -- Let's read a table and repeat with the same heading any number of times
      tomls <- sepBy1 (doubleHeadingOf key) (simpleToml key)
      let val = ArrTab $ forget tomls
      pure [(key, val)]

  emptyHeading : Grammar _ TomlToken True (List (List String, Value))
  emptyHeading =
    do
      ignore heading
      pure []

  kvs : Grammar _ TomlToken True (List (List String, Value))
  kvs =
    do
      key <- option [] heading
      inner <- some (
            kv
        <|> comment
        <|> whitespace)
      pure $ map (\(k, v) => (key ++ k, v)) (mapMaybe id $ forget inner)

  simpleToml : List String -> Grammar _ TomlToken False Toml
  simpleToml pre =
    do
      res <- map concat (many (kvs <|> emptyHeading))
      pure $ map (mapFst $ dropPrefix pre) res

  toml : Grammar _ TomlToken False Toml
  toml =
    map concat (many (subtable <|> kvs <|> emptyHeading))

export
parseTomlToks : List (WithBounds TomlToken) -> Maybe Toml
parseTomlToks toks = case parse toml toks of
                      Right (j, []) => Just j
                      _ => Nothing

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module xquant.Spinor.SigKets

import public xquant.Spinor.Sigmas
import public xquant.Core.Types
import public xquant.Math.Hilbert

import Data.Matrix.Algebraic
import Data.Complex
import Data.ZZ

infixl 3 <\>
infixl 3 <|>
infixr 4 </>
infixr 7 <&>

%default total

---- State Data ----

||| Spin orientation datatype - no identity option, unlike Pauli data type,
||| though it could possibly be added to represent a neutral density matrix
data Orient = X | Y | Z

data Spin = Up | Down

instance Eq Spin where
  Up == Up     = True
  Down == Down = True
  Up == Down   = False
  Down == Up   = False

||| basic spin orientation datatype
data EigenSpin = Eigenspin Orient Spin

||| collumn 'ket' vector for multiple spins
data KetSpins : Nat -> Type where
  kPhase : Phase -> KetSpins Z
  kS     : EigenSpin -> KetSpins k -> KetSpins (S k)

||| row 'bra' vector for multiple spins
data BraSpins : Nat -> Type where
  bPhase : Phase -> BraSpins Z
  bS     : EigenSpin -> BraSpins k -> BraSpins (S k)

||| convert a bra to a ket
bk : BraSpins n -> KetSpins n
bk (bPhase p) = kPhase $ star p
bk (bS e bs)  = kS e (bk bs)

||| convert a ket to a bra
kb : KetSpins n -> BraSpins n
kb (kPhase p) = bPhase $ star p
kb (kS e ks)  = bS e (kb ks)

||| easy initialize bra
bra : EigenSpin -> BraSpins 1
bra e = bS e $ bPhase P1

||| easy initialize ket
ket : EigenSpin -> KetSpins 1
ket e = kS e $ kPhase P1

instance Show Orient where
  show X = "X"
  show Y = "Y"
  show Z = "Z"

instance Show Spin where
  show Up   = "Up"
  show Down = "Dn"

instance Show EigenSpin where
  show (Eigenspin o s) = (show o) ++ "-" ++ (show s)

||| EigenSpin shorthands
upX : EigenSpin
upX = Eigenspin X Up
downX : EigenSpin
downX = Eigenspin X Down

upY : EigenSpin
upY = Eigenspin Y Up
downY : EigenSpin
downY = Eigenspin Y Down

upZ : EigenSpin
upZ = Eigenspin Z Up
downZ : EigenSpin
downZ = Eigenspin Z Down

uX : EigenSpin
uX = upX
dX : EigenSpin
dX = downX

uY : EigenSpin
uY = upY
dY : EigenSpin
dY = downY

uZ : EigenSpin
uZ = upZ
dZ : EigenSpin
dZ = downZ

||| Single abstract sigma acting on ket
ObsKet1 : Sigma 1 -> KetSpins 1 -> KetSpins 1
ObsKet1 (Sig SI $ sPhase p1) (kS (Eigenspin o ud)   (kPhase p2)) = kS (Eigenspin o ud)   (kPhase $ p1 <+> p2)
ObsKet1 (Sig SX $ sPhase p1) (kS (Eigenspin X Up)   (kPhase p2)) = kS (Eigenspin X Up)   (kPhase $ p1 <+> p2)
ObsKet1 (Sig SX $ sPhase p1) (kS (Eigenspin X Down) (kPhase p2)) = kS (Eigenspin X Down) (kPhase $ p1 <+> p2 <+> M1)
ObsKet1 (Sig SX $ sPhase p1) (kS (Eigenspin Y Up)   (kPhase p2)) = kS (Eigenspin Y Down) (kPhase $ p1 <+> p2 <+> Pi)
ObsKet1 (Sig SX $ sPhase p1) (kS (Eigenspin Y Down) (kPhase p2)) = kS (Eigenspin Y Up)   (kPhase $ p1 <+> p2 <+> P1)
ObsKet1 (Sig SX $ sPhase p1) (kS (Eigenspin Z Up)   (kPhase p2)) = kS (Eigenspin Z Down) (kPhase $ p1 <+> p2)
ObsKet1 (Sig SX $ sPhase p1) (kS (Eigenspin Z Down) (kPhase p2)) = kS (Eigenspin Z Up)   (kPhase $ p1 <+> p2)
ObsKet1 (Sig SY $ sPhase p1) (kS (Eigenspin X Up)   (kPhase p2)) = kS (Eigenspin Y Up)   (kPhase $ p1 <+> p2)
ObsKet1 (Sig SY $ sPhase p1) (kS (Eigenspin X Down) (kPhase p2)) = kS (Eigenspin Y Down) (kPhase $ p1 <+> p2 <+> M1)
ObsKet1 (Sig SY $ sPhase p1) (kS (Eigenspin Y Up)   (kPhase p2)) = kS (Eigenspin Z Down) (kPhase $ p1 <+> p2 <+> Pi)
ObsKet1 (Sig SY $ sPhase p1) (kS (Eigenspin Y Down) (kPhase p2)) = kS (Eigenspin X Up)   (kPhase $ p1 <+> p2 <+> Mi)
ObsKet1 (Sig SY $ sPhase p1) (kS (Eigenspin Z Up)   (kPhase p2)) = kS (Eigenspin Z Down) (kPhase $ p1 <+> p2 <+> Pi)
ObsKet1 (Sig SY $ sPhase p1) (kS (Eigenspin Z Down) (kPhase p2)) = kS (Eigenspin Z Up)   (kPhase $ p1 <+> p2 <+> M1)
ObsKet1 (Sig SZ $ sPhase p1) (kS (Eigenspin X Up)   (kPhase p2)) = kS (Eigenspin X Down) (kPhase $ p1 <+> p2 <+> M1)
ObsKet1 (Sig SZ $ sPhase p1) (kS (Eigenspin X Down) (kPhase p2)) = kS (Eigenspin X Up)   (kPhase $ p1 <+> p2 <+> M1)
ObsKet1 (Sig SZ $ sPhase p1) (kS (Eigenspin Y Up)   (kPhase p2)) = kS (Eigenspin Y Down) (kPhase $ p1 <+> p2 <+> M1)
ObsKet1 (Sig SZ $ sPhase p1) (kS (Eigenspin Y Down) (kPhase p2)) = kS (Eigenspin Y Up)   (kPhase $ p1 <+> p2 <+> M1)
ObsKet1 (Sig SZ $ sPhase p1) (kS (Eigenspin Z Up)   (kPhase p2)) = kS (Eigenspin Z Up)   (kPhase $ p1 <+> p2)
ObsKet1 (Sig SZ $ sPhase p1) (kS (Eigenspin Z Down) (kPhase p2)) = kS (Eigenspin Z Down) (kPhase $ p1 <+> p2 <+> M1)

timesPhase : Phase -> KetSpins n -> KetSpins n
timesPhase p1 (kPhase p2) = kPhase (p1 <+> p2)
timesPhase p1 (kS e es)   = kS e (timesPhase p1 es)

topOrientation : KetSpins (S n) -> Orient
topOrientation (kS (Eigenspin o s) more) = o

topKetSpin : KetSpins (S n) -> EigenSpin
topKetSpin (kS e es) = e

lastSpin : KetSpins (S k) -> EigenSpin
lastSpin (kS e (kPhase ph)) = e
lastSpin (kS e (kS e2 es))  = lastSpin (kS e2 es)

kPack : EigenSpin -> KetSpins 1
kPack e = kS e (kPhase P1)

kGetPhase : KetSpins n -> Phase
kGetPhase (kPhase p)             = p
kGetPhase (kS (Eigenspin o s) x) = kGetPhase x

||| Apply Sigma operator to abstract multi-qubit states
ObsKet : Sigma n -> KetSpins n -> KetSpins n
ObsKet (sPhase p1)  (kPhase p2)  = kPhase $ p1 <+> p2
ObsKet (Sig pl s) (kS k ks) with (ObsKet1 (pack pl) (kPack k))
  | r = kS (topKetSpin r) (timesPhase (kGetPhase r) (ObsKet s ks))

||| Infix op for Sigma-Ket multiply
(</>) : Sigma n -> KetSpins n -> KetSpins n
(</>) = ObsKet

||| Infix op for Bra-Sigma multiply
(<\>) : BraSpins n -> Sigma n -> BraSpins n
(<\>) b s = kb $ ObsKet s (bk b)

||| Another alias for Bra-Sigma multiply, for maximal harmony with written convention
(<|>) : BraSpins n -> Sigma n -> BraSpins n
(<|>) = (<\>)

instance Show (KetSpins n) where
  show (kPhase phase) = show phase
  show s = (Prefix s) ++ "[" ++ (suffix s) ++ "]" where
    suffix : KetSpins n -> String
    suffix (kPhase ph)        = ""
    suffix (kS p (kPhase ph)) = (show p)
    suffix (kS p s)           = (show p) ++ (suffix s)
    Prefix : KetSpins n -> String
    Prefix (kPhase (Sign a b)) = (if a then "-" else "") ++ (if b then "i " else "")
    Prefix (kS p s)            = Prefix s

||| Tensor product for abstract multi-qubit kets
ox : KetSpins n -> KetSpins m -> KetSpins (n + m)
ox e           (kPhase ph) ?= {Ket_OTimes_Lemma_1} timesPhase ph e
ox (kPhase ph) e            = timesPhase ph e
ox (kS e1 es1) (kS e2 es2) ?= {Ket_OTimes_Lemma_2} ox (dropLast $ kS e1 es1)
                                                      (kS (lastSpin $ kS e1 es1) (kS e2 es2)) where
  dropLast : KetSpins (S k) -> KetSpins k
  dropLast (kS e (kPhase ph)) = kPhase ph
  dropLast (kS e (kS e2 es))  = kS e (dropLast $ kS e2 es)

||| Infix tensor multiply kets
Ket.(<&>) : KetSpins n -> KetSpins m -> KetSpins (n + m)
Ket.(<&>) = ox

||| Infix tensor multiply bras
Bra.(<&>) : BraSpins n -> BraSpins m -> BraSpins (n + m)
Bra.(<&>) b1 b2 = kb $ ox (bk b1) (bk b2)

---- Numeric State & Operator Data ----

||| Phase to complex number
Phase.comZ : Phase -> Complex ZZ
Phase.comZ (Sign False False) = c1
Phase.comZ (Sign False True)  = ci
Phase.comZ (Sign True False)  = m1
Phase.comZ (Sign True True)   = mi

||| Phase to complex float
Phase.comF : Phase -> Complex Float
Phase.comF (Sign False False) = c1
Phase.comF (Sign False True)  = ci
Phase.comF (Sign True False)  = m1
Phase.comF (Sign True True)   = mi

||| Integral Sigma 1's
sx : QubitOp 1 ZZ
sx = [[c0, c1], [c1, c0]]

sy : QubitOp 1 ZZ
sy = [[c0, mi], [ci, c0]]

sz : QubitOp 1 ZZ
sz = [[c1, c0], [c0, m1]]

si : QubitOp 1 ZZ
si = [[c1, c0], [c0, c1]]

Pauli.comZ : Pauli -> QubitOp 1 ZZ
Pauli.comZ SX = sx
Pauli.comZ SY = sy
Pauli.comZ SZ = sz
Pauli.comZ SI = si

||| Floating Sigma 1's
Pauli.comF : Pauli -> QubitOp 1 Float
Pauli.comF SX = (0.5 :+ 0) <#> [[c0, c1], [c1, c0]]
Pauli.comF SY = (0.5 :+ 0) <#> [[c0, mi], [ci, c0]]
Pauli.comF SZ = (0.5 :+ 0) <#> [[c1, c0], [c0, m1]]
Pauli.comF SI = (0.5 :+ 0) <#> [[c1, c0], [c0, c1]]

||| Sigma n to matrix
Sigma.comF : Sigma n -> QubitOp n Float
Sigma.comF (sPhase ph) = [[comF ph]]
Sigma.comF (Sig p s)   = (comF p) <&> (comF s)

||| Sigma n to matrix
Sigma.comZ : Sigma n -> QubitOp n ZZ
Sigma.comZ (sPhase ph) = [[comZ ph]]
Sigma.comZ (Sig p s)   = (comZ p) <&> (comZ s)

||| Numeric KetSpin vectors
xUp : Qubit 1 Float
xUp = normalize [c1, c1]

xDown : Qubit 1 Float
xDown = normalize [m1, c1]

yUp : Qubit 1 Float
yUp = normalize [mi, c1]

yDown : Qubit 1 Float
yDown = normalize [ci, c1]

zUp : Qubit 1 Float
zUp = [c1, c0]

zDown : Qubit 1 Float
zDown = [c0, c1]

||| [single] KetSpin to numeric vector
Spin.matF : EigenSpin -> QubitKet 1 Float
Spin.matF (Eigenspin X Up)   = col xUp
Spin.matF (Eigenspin X Down) = col xDown
Spin.matF (Eigenspin Y Up)   = col yUp
Spin.matF (Eigenspin Y Down) = col yDown
Spin.matF (Eigenspin Z Up)   = col zUp
Spin.matF (Eigenspin Z Down) = col zDown

||| [single] KetSpin to numeric vector
KetSpins.matF : KetSpins n -> QubitKet n Float
KetSpins.matF (kPhase ph) = [[comF ph]]
KetSpins.matF (kS e k)    = (Spin.matF e) <&> (KetSpins.matF k)

||| Bra to row-vector matrix
BraSpins.matF : BraSpins n -> QubitBra n Float
BraSpins.matF (bPhase ph) = [[comF (star ph)]]
BraSpins.matF (bS e b)    = (transpose $ Spin.matF e) <&> (BraSpins.matF b)

||| Bra times Ket to complex number
Bra.(<\>) : Ring a => BraSpins n -> KetSpins n -> Complex Float
Bra.(<\>) b k = index 0 $ index 0 $ (matF b) <> (matF k)

||| Sigma operators commute
data Commutes : Sigma n -> Sigma n -> Type where
  CommZero : (x : Sigma Z) -> (y : Sigma Z) -> Commutes x y
  CommSucc : (a : Sigma 1) -> (b : Sigma 1) -> Commutes x y -> Commutes (a <&> x) (b <&> y)

||| Test for Sigma commutation
commute : Sigma n -> Sigma n -> Bool
commute (sPhase x)  (sPhase y)  = True
commute (Sig p1 s1) (Sig p2 s2) = xor (p1 /= p2) $ commute s1 s2

||| Whether each non-identity Pauli operator occurs an even number of times
qubitParity : List Pauli -> Vect 3 Bool
qubitParity []         = [False, False, False]
qubitParity (SI :: ss) = qubitParity ss
qubitParity (SX :: ss) = updateAt 0 not $ qubitParity ss
qubitParity (SY :: ss) = updateAt 1 not $ qubitParity ss
qubitParity (SZ :: ss) = updateAt 2 not $ qubitParity ss

||| All Sigmas of a given order
allSigmas : (n : Nat) -> List $ Sigma n
allSigmas Z     = [sPhase P1]
allSigmas (S n) = allSigmas n >>= (\s => [Sig SI s, Sig SX s, Sig SY s, Sig SZ s])

||| All pairs of Sigmas at the given order
sigPair : (n : Nat) -> List $ Vect 2 (Sigma n)
sigPair n = [ [s1,s2] | s1 <- (allSigmas n), s2 <- (allSigmas n) ]

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

Ket_OTimes_Lemma_1 = proof
  intro
  rewrite (plusZeroRightNeutral n)
  intros
  trivial

Ket_OTimes_Lemma_2 = proof
  intros
  rewrite sym $ plusSuccRightSucc k (S k1)
  trivial

max_stars_repo_name: fieldstrength/xquant

max_issues_repo_name: fieldstrength/xquant

max_forks_repo_name: fieldstrength/xquant


text:
module Prelude.Show

import Builtin
import Prelude.Basics
import Prelude.EqOrd
import Prelude.Num
import Prelude.Types

%default total

----------
-- SHOW --
----------

||| The precedence of an Idris operator or syntactic context.
public export
data Prec = Open | Equal | Dollar | Backtick | User Nat | PrefixMinus | App

||| Gives the constructor index of the Prec as a helper for writing
||| implementations.
public export
precCon : Prec -> Integer
precCon Open        = 0
precCon Equal       = 1
precCon Dollar      = 2
precCon Backtick    = 3
precCon (User n)    = 4
precCon PrefixMinus = 5
precCon App         = 6

export
Eq Prec where
  (==) (User m) (User n) = m == n
  (==) x        y        = precCon x == precCon y

export
Ord Prec where
  compare (User m) (User n) = compare m n
  compare x        y        = compare (precCon x) (precCon y)

||| Things that have a canonical `String` representation.
public export
interface Show ty where
  constructor MkShow
  ||| Convert a value to its `String` representation.
  ||| @ x the value to convert
  show : (x : ty) -> String
  show x = showPrec Open x

  ||| Convert a value to its `String` representation in a certain precedence
  ||| context.
  |||
  ||| A value should produce parentheses around itself if and only if the given
  ||| precedence context is greater than or equal to the precedence of the
  ||| outermost operation represented in the produced `String`.  *This is
  ||| different from Haskell*, which requires it to be strictly greater.  `Open`
  ||| should thus always produce *no* outermost parens, `App` should always
  ||| produce outermost parens except on atomic values and those that provide
  ||| their own bracketing, like `Pair` and `List`.
  ||| @ d the precedence context.
  ||| @ x the value to convert
  showPrec : (d : Prec) -> (x : ty) -> String
  showPrec _ x = show x

||| Surround a `String` with parentheses depending on a condition.
||| @ b whether to add parentheses
export
showParens : (b : Bool) -> String -> String
showParens False s = s
showParens True  s = "(" ++ s ++ ")"

||| A helper for the common case of showing a non-infix constructor with at
||| least one argument, for use with `showArg`.
|||
||| Apply `showCon` to the precedence context, the constructor name, and the
||| args shown with `showArg` and concatenated.  Example:
||| ```
||| data Ann a = MkAnn String a
|||
||| Show a => Show (Ann a) where
|||   showPrec d (MkAnn s x) = showCon d "MkAnn" $ showArg s ++ showArg x
||| ```
export
showCon : (d : Prec) -> (conName : String) -> (shownArgs : String) -> String
showCon d conName shownArgs = showParens (d >= App) (conName ++ shownArgs)

||| A helper for the common case of showing a non-infix constructor with at
||| least one argument, for use with `showCon`.
|||
||| This adds a space to the front so the results can be directly concatenated.
||| See `showCon` for details and an example.
export
showArg : Show a => (x : a) -> String
showArg x = " " ++ showPrec App x

firstCharIs : (Char -> Bool) -> String -> Bool
firstCharIs p "" = False
firstCharIs p str = p (assert_total (prim__strHead str))

primNumShow : (a -> String) -> Prec -> a -> String
primNumShow f d x = let str = f x in showParens (d >= PrefixMinus && firstCharIs (== '-') str) str

export
Show Int where
  showPrec = primNumShow prim__cast_IntString

export
Show Integer where
  showPrec = primNumShow prim__cast_IntegerString

export
Show Bits8 where
  showPrec = primNumShow prim__cast_Bits8String

export
Show Bits16 where
  showPrec = primNumShow prim__cast_Bits16String

export
Show Bits32 where
  showPrec = primNumShow prim__cast_Bits32String

export
Show Bits64 where
  showPrec = primNumShow prim__cast_Bits64String

export
Show Int8 where
  showPrec = primNumShow prim__cast_Int8String

export
Show Int16 where
  showPrec = primNumShow prim__cast_Int16String

export
Show Int32 where
  showPrec = primNumShow prim__cast_Int32String

export
Show Int64 where
  showPrec = primNumShow prim__cast_Int64String

export
Show Double where
  showPrec = primNumShow prim__cast_DoubleString

protectEsc : (Char -> Bool) -> String -> String -> String
protectEsc p f s = f ++ (if firstCharIs p s then "\\&" else "") ++ s

showLitChar : Char -> String -> String
showLitChar '\a'   = ("\\a" ++)
showLitChar '\b'   = ("\\b" ++)
showLitChar '\f'   = ("\\f" ++)
showLitChar '\n'   = ("\\n" ++)
showLitChar '\r'   = ("\\r" ++)
showLitChar '\t'   = ("\\t" ++)
showLitChar '\v'   = ("\\v" ++)
showLitChar '\SO'  = protectEsc (== 'H') "\\SO"
showLitChar '\DEL' = ("\\DEL" ++)
showLitChar '\\'   = ("\\\\" ++)
showLitChar c
    = case getAt (fromInteger (prim__cast_CharInteger c)) asciiTab of
           Just k => strCons '\\' . (k ++)
           Nothing => if (c > '\DEL')
                         then strCons '\\' . protectEsc isDigit (show (prim__cast_CharInt c))
                         else strCons c
  where
    asciiTab : List String
    asciiTab
        = ["NUL", "SOH", "STX", "ETX", "EOT", "ENQ", "ACK", "BEL",
           "BS",  "HT",  "LF",  "VT",  "FF",  "CR",  "SO",  "SI",
           "DLE", "DC1", "DC2", "DC3", "DC4", "NAK", "SYN", "ETB",
           "CAN", "EM",  "SUB", "ESC", "FS",  "GS",  "RS",  "US"]

showLitString : List Char -> String -> String
showLitString []        = id
showLitString ('"'::cs) = ("\\\"" ++) . showLitString cs
showLitString (c  ::cs) = (showLitChar c) . showLitString cs

export
Show Char where
  show '\'' = "'\\''"
  show c    = strCons '\'' (showLitChar c "'")

export
Show String where
  show cs = strCons '"' (showLitString (unpack cs) "\"")

export
Show Nat where
  show n = show (the Integer (natToInteger n))

export
Show Bool where
  show True = "True"
  show False = "False"

export
Show Void where
  show v impossible

export
Show () where
  show () = "()"

export
(Show a, Show b) => Show (a, b) where
  show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"

export
(Show a, {y : a} -> Show (p y)) => Show (DPair a p) where
    show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"

export
Show a => Show (List a) where
  show xs = "[" ++ show' "" xs ++ "]"
    where
      show' : String -> List a -> String
      show' acc []        = acc
      show' acc [x]       = acc ++ show x
      show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs

export
Show a => Show (Maybe a) where
  showPrec d Nothing  = "Nothing"
  showPrec d (Just x) = showCon d "Just" (showArg x)

export
(Show a, Show b) => Show (Either a b) where
  showPrec d (Left x)  = showCon d "Left" $ showArg x
  showPrec d (Right x) = showCon d "Right" $ showArg x


text:
module NanoParsec

import public NanoParsec.Parser
import public NanoParsec.Combinators
import public NanoParsec.MonadPlus

max_stars_repo_name: stallmanifold/idris-nanoparsec

max_issues_repo_name: lambdaxymox/idris-nanoparsec

max_forks_repo_name: lambdaxymox/idris-nanoparsec


text:
module Client.Action.Register

import Client.Util
import Client.Server
import Data.Buffer
import Inigo.Async.Fetch
import Inigo.Async.Promise
import Inigo.Util.Url.Url
import Toml

registerAccountCall : Server -> String -> String -> String -> Promise ()
registerAccountCall server ns email passphrase =
  do
    let contents = encode [(["email"], Str email), (["passphrase"], Str passphrase)]
    let url = toString (fromHostPath (host server) (accountPostUrl ns))
    ignore $ assertOk url $ request url "POST" contents []

export
registerAccount : Server -> String -> String -> String -> Promise ()
registerAccount =
  registerAccountCall


text:
module Web.Internal.MediastreamTypes

import JS

--------------------------------------------------------------------------------
--          Enums
--------------------------------------------------------------------------------

namespace MediaStreamTrackState

  public export
  data MediaStreamTrackState = Live | Ended

  public export
  Show MediaStreamTrackState where
    show Live = "live"
    show Ended = "ended"

  public export
  Eq MediaStreamTrackState where
    (==) = (==) `on` show

  public export
  Ord MediaStreamTrackState where
    compare = compare `on` show

  public export
  read : String -> Maybe MediaStreamTrackState
  read "live" = Just Live
  read "ended" = Just Ended
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (MediaStreamTrackState.read s)}
             -> MediaStreamTrackState
  fromString s = fromJust $ read s

  export
  ToFFI MediaStreamTrackState String where
    toFFI = show

  export
  FromFFI MediaStreamTrackState String where
    fromFFI = read

namespace VideoFacingModeEnum

  public export
  data VideoFacingModeEnum = User | Environment | Left | Right

  public export
  Show VideoFacingModeEnum where
    show User = "user"
    show Environment = "environment"
    show Left = "left"
    show Right = "right"

  public export
  Eq VideoFacingModeEnum where
    (==) = (==) `on` show

  public export
  Ord VideoFacingModeEnum where
    compare = compare `on` show

  public export
  read : String -> Maybe VideoFacingModeEnum
  read "user" = Just User
  read "environment" = Just Environment
  read "left" = Just Left
  read "right" = Just Right
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (VideoFacingModeEnum.read s)}
             -> VideoFacingModeEnum
  fromString s = fromJust $ read s

  export
  ToFFI VideoFacingModeEnum String where
    toFFI = show

  export
  FromFFI VideoFacingModeEnum String where
    fromFFI = read

namespace VideoResizeModeEnum

  public export
  data VideoResizeModeEnum = None | CropAndScale

  public export
  Show VideoResizeModeEnum where
    show None = "none"
    show CropAndScale = "crop-and-scale"

  public export
  Eq VideoResizeModeEnum where
    (==) = (==) `on` show

  public export
  Ord VideoResizeModeEnum where
    compare = compare `on` show

  public export
  read : String -> Maybe VideoResizeModeEnum
  read "none" = Just None
  read "crop-and-scale" = Just CropAndScale
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (VideoResizeModeEnum.read s)}
             -> VideoResizeModeEnum
  fromString s = fromJust $ read s

  export
  ToFFI VideoResizeModeEnum String where
    toFFI = show

  export
  FromFFI VideoResizeModeEnum String where
    fromFFI = read

namespace MediaDeviceKind

  public export
  data MediaDeviceKind = Audioinput | Audiooutput | Videoinput

  public export
  Show MediaDeviceKind where
    show Audioinput = "audioinput"
    show Audiooutput = "audiooutput"
    show Videoinput = "videoinput"

  public export
  Eq MediaDeviceKind where
    (==) = (==) `on` show

  public export
  Ord MediaDeviceKind where
    compare = compare `on` show

  public export
  read : String -> Maybe MediaDeviceKind
  read "audioinput" = Just Audioinput
  read "audiooutput" = Just Audiooutput
  read "videoinput" = Just Videoinput
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (MediaDeviceKind.read s)}
             -> MediaDeviceKind
  fromString s = fromJust $ read s

  export
  ToFFI MediaDeviceKind String where
    toFFI = show

  export
  FromFFI MediaDeviceKind String where
    fromFFI = read

--------------------------------------------------------------------------------
--          Interfaces
--------------------------------------------------------------------------------

export data ConstrainablePattern : Type where [external]

export
ToFFI ConstrainablePattern ConstrainablePattern where toFFI = id

export
FromFFI ConstrainablePattern ConstrainablePattern where fromFFI = Just

export
SafeCast ConstrainablePattern where
  safeCast = unsafeCastOnPrototypeName "ConstrainablePattern"

export data InputDeviceInfo : Type where [external]

export
ToFFI InputDeviceInfo InputDeviceInfo where toFFI = id

export
FromFFI InputDeviceInfo InputDeviceInfo where fromFFI = Just

export
SafeCast InputDeviceInfo where
  safeCast = unsafeCastOnPrototypeName "InputDeviceInfo"

export data MediaDeviceInfo : Type where [external]

export
ToFFI MediaDeviceInfo MediaDeviceInfo where toFFI = id

export
FromFFI MediaDeviceInfo MediaDeviceInfo where fromFFI = Just

export
SafeCast MediaDeviceInfo where
  safeCast = unsafeCastOnPrototypeName "MediaDeviceInfo"

export data MediaDevices : Type where [external]

export
ToFFI MediaDevices MediaDevices where toFFI = id

export
FromFFI MediaDevices MediaDevices where fromFFI = Just

export
SafeCast MediaDevices where
  safeCast = unsafeCastOnPrototypeName "MediaDevices"

export data MediaStream : Type where [external]

export
ToFFI MediaStream MediaStream where toFFI = id

export
FromFFI MediaStream MediaStream where fromFFI = Just

export
SafeCast MediaStream where
  safeCast = unsafeCastOnPrototypeName "MediaStream"

export data MediaStreamTrack : Type where [external]

export
ToFFI MediaStreamTrack MediaStreamTrack where toFFI = id

export
FromFFI MediaStreamTrack MediaStreamTrack where fromFFI = Just

export
SafeCast MediaStreamTrack where
  safeCast = unsafeCastOnPrototypeName "MediaStreamTrack"

export data MediaStreamTrackEvent : Type where [external]

export
ToFFI MediaStreamTrackEvent MediaStreamTrackEvent where toFFI = id

export
FromFFI MediaStreamTrackEvent MediaStreamTrackEvent where fromFFI = Just

export
SafeCast MediaStreamTrackEvent where
  safeCast = unsafeCastOnPrototypeName "MediaStreamTrackEvent"

export data OverconstrainedError : Type where [external]

export
ToFFI OverconstrainedError OverconstrainedError where toFFI = id

export
FromFFI OverconstrainedError OverconstrainedError where fromFFI = Just

export
SafeCast OverconstrainedError where
  safeCast = unsafeCastOnPrototypeName "OverconstrainedError"

--------------------------------------------------------------------------------
--          Dictionaries
--------------------------------------------------------------------------------

export data Capabilities : Type where [external]

export
ToFFI Capabilities Capabilities where toFFI = id

export
FromFFI Capabilities Capabilities where fromFFI = Just

export data ConstrainBooleanParameters : Type where [external]

export
ToFFI ConstrainBooleanParameters ConstrainBooleanParameters where toFFI = id

export
FromFFI ConstrainBooleanParameters ConstrainBooleanParameters where fromFFI = Just

export data ConstrainDOMStringParameters : Type where [external]

export
ToFFI ConstrainDOMStringParameters ConstrainDOMStringParameters where toFFI = id

export
FromFFI ConstrainDOMStringParameters ConstrainDOMStringParameters where fromFFI = Just

export data ConstrainDoubleRange : Type where [external]

export
ToFFI ConstrainDoubleRange ConstrainDoubleRange where toFFI = id

export
FromFFI ConstrainDoubleRange ConstrainDoubleRange where fromFFI = Just

export data ConstrainULongRange : Type where [external]

export
ToFFI ConstrainULongRange ConstrainULongRange where toFFI = id

export
FromFFI ConstrainULongRange ConstrainULongRange where fromFFI = Just

export data ConstraintSet : Type where [external]

export
ToFFI ConstraintSet ConstraintSet where toFFI = id

export
FromFFI ConstraintSet ConstraintSet where fromFFI = Just

export data Constraints : Type where [external]

export
ToFFI Constraints Constraints where toFFI = id

export
FromFFI Constraints Constraints where fromFFI = Just

export data DoubleRange : Type where [external]

export
ToFFI DoubleRange DoubleRange where toFFI = id

export
FromFFI DoubleRange DoubleRange where fromFFI = Just

export data MediaStreamConstraints : Type where [external]

export
ToFFI MediaStreamConstraints MediaStreamConstraints where toFFI = id

export
FromFFI MediaStreamConstraints MediaStreamConstraints where fromFFI = Just

export data MediaStreamTrackEventInit : Type where [external]

export
ToFFI MediaStreamTrackEventInit MediaStreamTrackEventInit where toFFI = id

export
FromFFI MediaStreamTrackEventInit MediaStreamTrackEventInit where fromFFI = Just

export data MediaTrackCapabilities : Type where [external]

export
ToFFI MediaTrackCapabilities MediaTrackCapabilities where toFFI = id

export
FromFFI MediaTrackCapabilities MediaTrackCapabilities where fromFFI = Just

export data MediaTrackConstraintSet : Type where [external]

export
ToFFI MediaTrackConstraintSet MediaTrackConstraintSet where toFFI = id

export
FromFFI MediaTrackConstraintSet MediaTrackConstraintSet where fromFFI = Just

export data MediaTrackConstraints : Type where [external]

export
ToFFI MediaTrackConstraints MediaTrackConstraints where toFFI = id

export
FromFFI MediaTrackConstraints MediaTrackConstraints where fromFFI = Just

export data MediaTrackSettings : Type where [external]

export
ToFFI MediaTrackSettings MediaTrackSettings where toFFI = id

export
FromFFI MediaTrackSettings MediaTrackSettings where fromFFI = Just

export data MediaTrackSupportedConstraints : Type where [external]

export
ToFFI MediaTrackSupportedConstraints MediaTrackSupportedConstraints where toFFI = id

export
FromFFI MediaTrackSupportedConstraints MediaTrackSupportedConstraints where fromFFI = Just

export data Settings : Type where [external]

export
ToFFI Settings Settings where toFFI = id

export
FromFFI Settings Settings where fromFFI = Just

export data ULongRange : Type where [external]

export
ToFFI ULongRange ULongRange where toFFI = id

export
FromFFI ULongRange ULongRange where fromFFI = Just

--------------------------------------------------------------------------------
--          Callbacks
--------------------------------------------------------------------------------

export data NavigatorUserMediaErrorCallback : Type where [external]

export
ToFFI NavigatorUserMediaErrorCallback NavigatorUserMediaErrorCallback where toFFI = id

export
FromFFI NavigatorUserMediaErrorCallback NavigatorUserMediaErrorCallback where fromFFI = Just

export data NavigatorUserMediaSuccessCallback : Type where [external]

export
ToFFI NavigatorUserMediaSuccessCallback NavigatorUserMediaSuccessCallback where toFFI = id

export
FromFFI NavigatorUserMediaSuccessCallback NavigatorUserMediaSuccessCallback where fromFFI = Just


text:
||| Basic matrix operations with dimensionalities enforced
||| at the type level
module Data.Matrix

import public Data.Vect

%default total

||| Matrix with n rows and m columns
Matrix : Nat -> Nat -> Type -> Type
Matrix n m a = Vect n (Vect m a)

||| Get the specified column of a matrix
getCol : Fin m -> Matrix n m a -> Vect n a
getCol f = map (index f)

||| Get the specified row of a matrix
getRow : Fin n -> Matrix n m a -> Vect m a
getRow = index

||| Delete the specified column of a matrix
deleteCol : Fin (S m) -> Matrix n (S m) a -> Matrix n m a
deleteCol f = map (deleteAt f)

||| Delete the specified row of a matrix
deleteRow : Fin (S n) -> Matrix (S n) m a -> Matrix n m a
deleteRow = deleteAt

insertRow : Fin (S n) -> Vect m a -> Matrix n m a -> Matrix (S n) m a
insertRow = insertAt

insertCol : Fin (S m) -> Vect n a -> Matrix n m a -> Matrix n (S m) a
insertCol f = zipWith (insertAt f)

||| Matrix element at specified row and column indices
indices : Fin n -> Fin m -> Matrix n m a -> a
indices f1 f2 = index f2 . index f1

||| Cast a vector from a standard Vect to a proper n x 1 matrix
col : Vect n a -> Matrix n 1 a
col = map (\x => [x])

||| Cast a row from a standard Vect to a proper 1 x n matrix
row : Vect n a -> Matrix 1 n a
row r = [r]

||| Matrix formed by deleting specified row and col
subMatrix : Fin (S n) -> Fin (S m) -> Matrix (S n) (S m) a -> Matrix n m a
subMatrix r c = deleteRow r . deleteCol c

||| Flatten a matrix of matrices
concatMatrix : Matrix n m (Matrix x y a) -> Matrix (n * x) (m * y) a
concatMatrix = Vect.concat . map (map Vect.concat) . map transpose

||| All finite numbers of the specified level
fins : (n : Nat) -> Vect n (Fin n)
fins Z     = Nil
fins (S n) = FZ :: (map FS $ fins n)

max_stars_repo_name: BlackBrane/xquant


text:
||| A DYI version of 'string interpolation', mimicking Python 3's 'f-string' syntax
||| Not as fancy
module Data.String.Interpolation

import Data.String

namespace Data.String.Interpolation.Basic
  %inline
  public export
  F : List String -> String
  F strs = concat (strs)

namespace Data.String.Interpolation.Nested
  %inline
  public export
  F : List (List String) -> String
  F strss = F (concat strss)

{- Examples:
fstring : String
fstring = let apples = "apples" in
          F["I have some ", apples," here."]                     --- cf. f"I have some {apples} here."

multiline : String
multiline = let name = "Edwin"
                profession = "Hacker"
                affiliation = "the University of St. Andrews" in --- cf.
                F [["Hi ",name,". "             ]                --- f"Hi {name}. "              \
                  ,["You are a ",profession,". "]                --- f"You are a {profession}. " \
                  ,["You were in ",affiliation,"."]              --- f"You were in {affiliation}."
                  ]

-}


text:
module Let0

import Data.Nat
import Data.Vect

go : (_ : Vect n elem) -> (_ : Vect m elem) -> Vect (n + m) elem
go         acc []        = let 0 prf = plusZeroRightNeutral n in ?rhs
go {m=S m} acc (x :: xs) = rewrite sym $ plusSuccRightSucc n m in go (x::acc) xs

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module ListExt2

%default total
%access public export

smallerThanCons : (x : a) -> (xs : List a) -> Smaller xs (x :: xs)
smallerThanCons x [] = lteRefl
smallerThanCons x (y :: xs) = lteRefl

||| If Left True, never bother to call me back
eat : Eq a => (delim : List a) -> {auto prf : NonEmpty delim}
    -> (dish : List a)
    -> Either Bool (rem : List a ** Smaller rem dish)
eat (x :: xs) [] = Left True
eat (x :: xs) (y :: ys) =
  if x == y
  then
    case xs of
      [] => Right (ys ** smallerThanCons y ys)
      (z :: zs) =>
        case eat (z :: zs) ys of
          Left e => Left e
          Right (l ** prf) => Right (l ** lteSuccRight prf)
  else Left False

splitStep : Eq a => (xs : List a)
          -> ((ys : List a) -> Smaller ys xs -> List a
                            -> (List a, List (List a)))
          -> List a -> (List a, List (List a))
splitStep [] _ _ = ([], [])
splitStep xs@(_ :: _) _ [] = (xs, [])
splitStep (x :: xs) f delim@(_::_) =
  case eat delim (x :: xs) of
    Left True => (x :: xs, [])
    Left False =>
      let (l, ls) = f xs (smallerThanCons x xs) delim
      in (x :: l, ls)
    Right (rem ** prf) =>
      let (l, ls) = f rem prf delim
      in ([], l::ls)

splitWith : Eq a => List a -> List a -> List (List a)
splitWith delim splittee =
  let splitter = sizeRec splitStep splittee
  in uncurry (::) $ splitter delim

substitute : Eq a => List a -> List a -> List a -> List a
substitute needle replacement = intercalate replacement . splitWith needle

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:
module Utils.Conjugate

import Data.Complex

%default total
%access public export

interface Conjugate space coSpace where
  conjug : space -> coSpace

implementation Neg a => Conjugate (Complex a) (Complex a) where
  conjug = conjugate

implementation Conjugate Double Double where
  conjug = id

implementation Conjugate Integer Integer where
  conjug = id

implementation Conjugate Nat Nat where
  conjug = id

implementation Conjugate Int Int where
  conjug = id

max_stars_repo_name: GrandArchTemplar/QuantumProgramming

max_issues_repo_name: GrandArchTemplar/QuantumProgramming

max_forks_repo_name: GrandArchTemplar/QuantumProgramming


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

import Sif.Types
import GRL.Lang.GLang

%access export
-- --------------------------------------------------- [ Public Data Structure ]

namespace Sif
  public export
  data EvalResult : Type where
    Good : List (String, Maybe SValue) -> EvalResult
    Bad  : EvalResult

evalResultsToString : EvalResult -> Maybe String
evalResultsToString Bad        = Nothing
evalResultsToString (Good is)  = Just $ unlines $ map (\(t,s) => unwords [showSValue s,"\t==>\t", t]) is
  where
    showSValue : Maybe SValue -> String
    showSValue Nothing  = "Nothing"
    showSValue (Just x) = show x

||| The Meta Model API
interface SifMetaModel a where
  toString : a -> String

public export
data MetaModel : Type where
  MkModel : SifMetaModel a => a -> MetaModel

mkMetaModel : SifMetaModel a => a -> MetaModel
mkMetaModel = MkModel

namespace Pattern

  ||| The Representation API
  export
  interface SifRepAPI (impl : SifTy -> SifDomain -> Type) where
      getTitle  : impl ty d -> {auto prf : HasMData ty} -> String
      getDesc   : impl ty d -> Maybe String
      getRTy    : impl TyREQ     d -> RTy
      getTTy    : impl TyTRAIT   d -> TTy
      getSValue : impl TyTRAIT   d -> SValue
      getCValue : impl TyAFFECTS d -> CValue

      getProblem  : impl TyPATTERN d -> impl TyPROBLEM  d
      getSolution : impl TyPATTERN d -> impl TySOLUTION d

      getReqs       : impl TyPROBLEM  d -> List (impl TyREQ      d)
      getProperties : impl TySOLUTION d -> List (impl TyPROPERTY d)
      getTraits     : impl TyPROPERTY d -> List (impl TyTRAIT    d)
      getAffects    : impl TyTRAIT    d -> List (impl TyAFFECTS  d)
      getReq        : impl TyAFFECTS  d -> impl TyREQ d

      evalPattern    : impl TyPATTERN d -> Sif.EvalResult
      fetchMetaModel : impl TyPATTERN d -> MetaModel

      getDomain : impl ty d -> SifDomain
      getDomain {d} _ = d

SifMetaModel MetaModel where
  toString (MkModel m) = toString m

public export
data SifExpr : SifTy
            -> SifDomain
            -> (impl : SifTy -> SifDomain -> Type)
            -> Type
  where
    MkExpr : SifRepAPI impl => impl ty d -> SifExpr ty d impl

namespace SifExpr
  getTitle : SifExpr ty d impl -> {auto prf : HasMData ty} -> String
  getTitle (MkExpr x) = Pattern.getTitle x

  getDesc : SifExpr ty d impl -> Maybe String
  getDesc (MkExpr x) = Pattern.getDesc x

  getRTy : SifExpr TyREQ d impl -> RTy
  getRTy (MkExpr x) = Pattern.getRTy x

  getTTy : SifExpr TyTRAIT d impl -> TTy
  getTTy (MkExpr x) = Pattern.getTTy x

  getSValue : SifExpr TyTRAIT d impl -> SValue
  getSValue (MkExpr x) = Pattern.getSValue x

  getCValue : SifExpr TyAFFECTS d impl -> CValue
  getCValue (MkExpr x) = Pattern.getCValue x

  getProblem : SifExpr TyPATTERN d impl -> SifExpr TyPROBLEM d impl
  getProblem (MkExpr x) = MkExpr $ Pattern.getProblem x

  getSolution : SifExpr TyPATTERN d impl -> SifExpr TySOLUTION d impl
  getSolution (MkExpr x) = MkExpr $ Pattern.getSolution x

  getReqs : SifExpr TyPROBLEM d impl -> List (SifExpr TyREQ d impl)
  getReqs (MkExpr x) = map MkExpr $ Pattern.getReqs x

  getProperties : SifExpr TySOLUTION d impl -> List (SifExpr TyPROPERTY d impl)
  getProperties (MkExpr x) = map MkExpr $ Pattern.getProperties x

  getTraits : SifExpr TyPROPERTY d impl -> List (SifExpr TyTRAIT d impl)
  getTraits (MkExpr x) = map MkExpr $ Pattern.getTraits x

  getAffects : SifExpr TyTRAIT d impl -> List (SifExpr TyAFFECTS d impl)
  getAffects (MkExpr x) = map MkExpr $ Pattern.getAffects x

  getReq : SifExpr TyAFFECTS d impl -> SifExpr TyREQ d impl
  getReq (MkExpr x) = MkExpr $ Pattern.getReq x

  getDomain : SifExpr ty d impl -> SifDomain
  getDomain {d} _ = d

  evalPattern : SifExpr TyPATTERN d impl -> Sif.EvalResult
  evalPattern (MkExpr x)    = Pattern.evalPattern x

  fetchMetaModel : SifExpr TyPATTERN d impl -> MetaModel
  fetchMetaModel (MkExpr x) = Pattern.fetchMetaModel x

-- Better to parameterise SifBuilder by a SifDomain. the problem is
-- not how to populate the value in the type---a update function that
-- populates a record field and type value at the sametime. Rather the
-- problem is how to have a clean api when defining instances of
-- this data type in later code sans dependent pairs.

||| Factories for building concrete representations
|||
public export
record SifBuilder (impl : SifTy -> SifDomain -> Type) where
  constructor MkSifBuilder
  buildReq : (d : SifDomain)
          -> RTy
          -> String
          -> Maybe String
          -> SifExpr TyREQ d impl

  buildProblem : (d : SifDomain)
              -> String
              -> Maybe String
              -> List (SifExpr TyREQ d impl)
              -> SifExpr TyPROBLEM d impl

  buildAffect : (d : SifDomain)
             -> CValue
             -> SifExpr TyREQ d impl
             -> Maybe String
             -> SifExpr TyAFFECTS d impl

  buildTrait : (d : SifDomain)
            -> TTy
            -> String
            -> Maybe String
            -> SValue
            -> List $ SifExpr TyAFFECTS d impl
            -> SifExpr TyTRAIT d impl

  buildProperty : (d : SifDomain)
               -> String
               -> Maybe String
               -> List $ SifExpr TyTRAIT d impl
               -> SifExpr TyPROPERTY d impl

  buildSolution : (d : SifDomain)
               -> String
               -> Maybe String
               -> List $ SifExpr TyPROPERTY d impl
               -> SifExpr TySOLUTION d impl

  buildPattern : (d : SifDomain)
              -> String
              -> Maybe String
              -> SifExpr TyPROBLEM  d impl
              -> SifExpr TySOLUTION d impl
              -> SifExpr TyPATTERN  d impl

public export
record SifBackend where
    constructor MkBackend
    name    : String
    builder : (SifBuilder impl)

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


text:
module Circuits.NetList.Lexer

import Text.Lexer

import Toolkit.Text.Lexer.Run

%default total

symbols : List String
symbols = ["[", "]", ";", "{", "}", ":", ",", "=", "?", "(", ")", ".", "#", "!", "&", "|", "+"]

keywords : List String
keywords = [ "input", "output", "inout"
           , "module", "endmodule"
           , "wire"
           , "logic"
           , "and", "or", "xor", "nand", "nor", "xnor", "not"
           , "mux"
           , "assign"
           , "split", "collect"
           ]

public export
data Identifier = MkIdentifier String

export
Eq Identifier where
  (==) (MkIdentifier x) (MkIdentifier y) = x == y

namespace Idealised
  public export
  data Token = ID String
               | Keyword String
               | LineComment String
               | BlockComment String
               | Documentation String
               | LitNat Nat
               | Symbol String
               | WS String
               | NotRecognised String
               | EndInput

  export
  Eq Token where
    (==) (ID x) (ID y) = x == y
    (==) (LineComment x) (LineComment y) = x == y
    (==) (BlockComment x) (BlockComment y) = x == y
    (==) (LitNat x) (LitNat y) = x == y
    (==) (Documentation x) (Documentation y) = x == y
    (==) (Keyword x) (Keyword y) = x == y
    (==) (Symbol x) (Symbol y) = x == y
    (==) (WS x) (WS y) = x == y
    (==) (NotRecognised x) (NotRecognised y) = x == y
    (==) EndInput EndInput = True
    (==) _ _ = False

  showToken : Show a => String -> a -> String
  showToken n a = "(" <+> n <+> " " <+> show a <+> ")"

  export
  Show Token where
    show (ID id)             = showToken "ID" id
    show (Keyword str)       = showToken "Keyword" str
    show (LineComment str)   = showToken "LineComment" str
    show (BlockComment str)  = showToken "BlockComment" str
    show (Documentation str) = showToken "Documentation" str

    show (LitNat n) = showToken "Nat" n

    show (Symbol s) = showToken "Symbol" s
    show (WS ws) = "WS"
    show (NotRecognised s) = showToken "Urgh" s
    show EndInput          = "EndInput"

  identifier : Lexer
  identifier = pred startIdent <+> many (pred validIdent)
    where
      startIdent : Char -> Bool
      startIdent x = isAlpha x

      validIdent : Char -> Bool
      validIdent '_' = True
      validIdent x = isAlphaNum x

  export
  tokenMap : TokenMap Idealised.Token
  tokenMap = with List
    [
      (space, WS)
    , (lineComment (exact "//"), LineComment)
    , (blockComment (exact "/*") (exact "*/"), BlockComment)
    , (lineComment (exact "\\\\"), Documentation)
    , (digits, \x => LitNat (integerToNat $ cast {to=Integer} x))
    ]
    ++
       map (\x => (exact x, Symbol)) symbols
    ++
    [
      (identifier, (\x => if elem x keywords then Keyword x else ID x))
    , (any, NotRecognised)
    ]

  keep : WithBounds Idealised.Token -> Bool
  keep (MkBounded t _ _) = case t of
      BlockComment _ => False
      LineComment  _ => False
      WS           _ => False
      _              => True

  export
  Lexer : Lexer Token
  Lexer = MkLexer Idealised.tokenMap (keep) EndInput

  export
  lexString : String -> Either LexError (List (WithBounds Token))
  lexString = lexString Lexer

  export
  lexFile : String -> IO $ Either LexFail (List (WithBounds Token))
  lexFile = lexFile Lexer

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Client.Action.Clean

import Client.Action.Build
import Data.List
import Data.String
import Inigo.Async.Base
import Inigo.Async.Promise
import Inigo.Async.FS
import Inigo.Package.Package
import Inigo.Paths

cleanIPkg : String -> Promise ()
cleanIPkg ipkg =
  ignore $ system "idris2" ["--clean", ipkg] Nothing False True

export
clean : Bool -> Promise ()
clean deps =
  do
    ignore writeIPkgFile
    ignore $ cleanIPkg inigoIPkgPath
    when (deps && !(fs_exists inigoDepDir)) $
      do
        files <- fs_getFilesR inigoDepDir
        let ipkgs = filter (isSuffixOf ".ipkg") files
        ignore $ all $ map cleanIPkg ipkgs