text:
-- SPDX-FileCopyrightText: 2021 The toml-idr developers
--
-- SPDX-License-Identifier: CC0-1.0

module Parser

import Tester
import Language.Reflection
import Control.ANSI

import Text.Lexer

import Language.TOML
import Language.TOML.Tokens
import Language.TOML.Parser as P
import Language.TOML.Lexer as L
import Language.TOML.ConcreteSyntax
import Language.TOML.Value

%language ElabReflection

parseToItems : String -> TestFunc (List Item)
parseToItems src = do
    Just toks <- pure $ L.lexTOML src
        | Nothing => throw "lexing failed"
    Right items <- pure $ P.parseItems toks
        | Left err => throw (show (colored Red "parsing failed: ") ++ show err)
    pure items

parse : String -> TestFunc Table
parse src = do
    Right table <- pure $ parseTOML src
        | Left err => throw (show err)
    pure table

namespace Concrete
    export
    kvNoNewline : Test
    kvNoNewline = test "parse key-value no newline" $ do
        items <- parseToItems "x = 12"
        assertEq (show items) "[keyval: x = 12]"

    export
    kvComment : Test
    kvComment = test "parse key-value with comment" $ do
        items <- parseToItems "x = 12 # this is a key value pair"
        assertEq (show items) "[keyval: x = 12]"

    export
    kvNewline : Test
    kvNewline = test "parse key-value with newline" $ do
        items <- parseToItems "x = 12\n"
        assertEq (show items) "[keyval: x = 12]"

    export
    tableHeader : Test
    tableHeader = test "parse table header" $ do
        items <- parseToItems "[package]"
        assertEq (show items) "[table: package]"

    export
    tableHeaderDotted : Test
    tableHeaderDotted = test "parse table header with dotted key" $ do
        items <- parseToItems "[dependencies.test]"
        assertEq (show items) "[table: dependencies.test]"

    export
    tableArray : Test
    tableArray = test "parse table array header" $ do
        items <- parseToItems "[[bin]]"
        assertEq (show items) "[tablearr: bin]"

    export
    tableArrayDotted : Test
    tableArrayDotted = test "parse table array header with dotted key" $ do
        items <- parseToItems "[[bin.tags]]"
        assertEq (show items) "[tablearr: bin.tags]"

    export
    emptyFile : Test
    emptyFile = test "parse empty file" $ do
        items <- parseToItems ""
        assertEq (show items) "[]"

    export
    kvArrayNewLine : Test
    kvArrayNewLine = test "key-val with array with newlines" $ do
        items <- parseToItems "x = [\n\t1,\n\t2,\n\t3\n]"
        assertEq (show items) "[keyval: x = [1, 2, 3]]"

    export
    kvInlineTable : Test
    kvInlineTable = test "key-val with inline table" $ do
        items <- parseToItems "test = { path = \"../test-idr\" }"
        -- TODO strings are not interspreted *and* are `show`n
        assertEq (show items) "[keyval: test = {path = \"../test-idr\"}]"

namespace Abstract
    export
    kvGlobal : Test
    kvGlobal = test "global key-val" $ do
        table <- parse "x = 12"
        assertEq [("x", VInteger 12)] (toList table)

    export
    kvNested : Test
    kvNested = test "global nested key-val" $ do
        table <- parse "x.y = 12"
        assertEq (lookupNested ["x", "y"] table) (Just $ VInteger 12)

    export
    tableSectionKv : Test
    tableSectionKv = test "parse table section key-val" $ do
        table <- parse "[table-name]\nx = 12"
        assertEq (lookupNested ["table-name", "x"] table) (Just $ VInteger 12)

    export
    tableSectionNestedKv : Test
    tableSectionNestedKv = test "parse table section nested key-val" $ do
        table <- parse "[table-name]\nx.y = 12"
        assertEq (lookupNested ["table-name", "x", "y"] table) (Just $ VInteger 12)

    export
    inlineTable : Test
    inlineTable = test "parse inline table" $ do
        table <- parse "test = { x = 12, y = 21 }"
        assertEq (lookupNested ["test", "x"] table) (Just $ VInteger 12)

    export
    array : Test
    array = test "parse array" $ do
        table <- parse "x = [1, 3, 7]"
        assertEq {loc = here `(())} (lookup "x" table) (Just $ VArray [VInteger 1, VInteger 3, VInteger 7])

    export
    integers : Test
    integers = test "parsing integers" $ do
        integers <- parse "x = [2, 42, -78, +47, 0x123, 0x1005, 0o55, 0o006, 0b11011]"
        assertEq {loc = here `(())}
            (lookup "x" integers)
            (Just $ VArray (map VInteger [2, 42, -78, 47, 0x123, 0x1005, 0o55, 0o6, 0b11011]))

    export
    floats : Test
    floats = test "parsing floats" $ do
        floats <- parse "x = [0.0, 0.1, 1.0, 42.84, 5e4, 2.12e3]"
        assertEq {loc = here `(())}
            (lookup "x" floats)
            (Just $ VArray $ map VFloat [0.0, 0.1, 1.0, 42.84, 50000, 2120])

    nan : Double
    nan = sqrt (-1)

    inf : Double
    inf = 1.0 / 0.0

    export
    specialFloats : Test
    specialFloats = test "parsing special floats" $ do
        nans <- parse "x = [nan, +nan, -nan]"
        infs <- parse "x = [inf, +inf, -inf]"
        assertEq {loc = here `(())}
            (lookup "x" infs)
            (Just $ VArray $ map VFloat [inf, inf, -inf])
        case lookup "x" nans of
            Just (VArray nans) => assert $ all isNan nans
            _ => throw "not an array"
      where
        isNan : Value -> Bool
        isNan (VFloat x) = x /= x
        isNan _ = False

    export
    strings : Test
    strings = test "parsing strings" $ do
        hello_world <- parse #"x = "hello world""#
        assertEq {loc = here `(())} (lookup "x" hello_world) (Just $ VString "hello world")

    export
    tableArray : Test
    tableArray = test "parsing table arrays" $ do
        array <- parse """
            [[depends]]
            name = "toml"
            version = "1.2"

            [[depends]]
            name = "hashable"
            version = "9.7"
            """

        case lookup "depends" array of
            Just (VArray [VTable toml, VTable hashable]) => do
                let loc = here `(())
                assertEq {loc} (lookup "name" toml) (Just $ VString "toml")
                assertEq {loc} (lookup "name" hashable) (Just $ VString "hashable")
                assertEq {loc} (lookup "version" toml) (Just $ VString "1.2")
                assertEq {loc} (lookup "version" hashable) (Just $ VString "9.7")
            Just (VArray xs) => throw "expected array of 2 tables, got: \{show xs}"
            Just val => throw "expected array, got: \{show val}"
            Nothing => throw "missing 'depends'"

public export
tests : List Test
tests = [
    Concrete.kvNoNewline,
    Concrete.kvComment,
    Concrete.kvNewline,
    Concrete.tableHeader,
    Concrete.tableHeaderDotted,
    Concrete.tableArray,
    Concrete.tableArrayDotted,
    Concrete.emptyFile,
    Concrete.kvArrayNewLine,
    Concrete.kvInlineTable,

    Abstract.kvGlobal,
    Abstract.kvNested,
    Abstract.tableSectionKv,
    Abstract.tableSectionNestedKv,
    Abstract.inlineTable,
    Abstract.array,
    Abstract.integers,
    Abstract.floats,
    Abstract.specialFloats,
    Abstract.strings,
    Abstract.tableArray
]

max_stars_repo_name: sepiina/toml-idr

max_issues_repo_name: sepiina/toml-idr

max_forks_repo_name: sepiina/toml-idr


text:
module NormalInput

import Data.Fuel
import State
import Cursor
import Document
import Data.Fin
import Parser

%default total

public export
data NormalInput : Type where
  NormalUp : NormalInput
  NormalLeft : NormalInput
  NormalRight : NormalInput
  NormalDown : NormalInput
  NormalInsert : NormalInput
  NormalSave : NormalInput
  NormalQuit : NormalInput
  NormalDeleteAt : NormalInput
  NormalDeleteLine : NormalInput
  NormalTop : NormalInput
  NormalBottom : NormalInput
  NormalBeginningOfLine : NormalInput
  NormalEndOfLine : NormalInput
  NormalEndOfWord : NormalInput
  NormalBeginningOfNextWord : NormalInput
  NormalDeleteUntilNextWord : NormalInput
  NormalDeleteAWord : NormalInput
  NormalChangeAWord : NormalInput
  NormalChangeUntilNextWord : NormalInput
  NormalBeginningOfWord : NormalInput
  NormalPageUp : NormalInput
  NormalPageDown : NormalInput
  NormalInsertNewLine : NormalInput
  NormalInsertRight : NormalInput
  NormalInsertBeginningOfLine : NormalInput
  NormalInsertEndOfLine : NormalInput
  NormalInsertNewLineUp : NormalInput

deleteParser : Parser Char NormalInput
deleteParser =
  Continuation $ \c2 => case c2 of
                          'a' => Continuation $ \c3 => Finished $ if c3 == 'w' then Just NormalDeleteAWord else Nothing
                          'd' => Finished $ Just NormalDeleteLine
                          'w' => Finished $ Just NormalDeleteUntilNextWord
                          _   => Finished Nothing

changeParser : Parser Char NormalInput
changeParser =
  Continuation $ \c2 => case c2 of
                          'a' => Continuation $ \c3 => Finished $ if c3 == 'w' then Just NormalChangeAWord else Nothing
                          'w' => Finished $ Just NormalChangeUntilNextWord
                          _ => Finished Nothing

parser : Parser Char NormalInput
parser = Continuation $ \c1 => case (ord c1) of
    104 => Finished $ Just NormalLeft
    106 => Finished $ Just NormalDown
    107 => Finished $ Just NormalUp
    108 => Finished $ Just NormalRight
    105 => Finished $ Just NormalInsert
    111 => Finished $ Just NormalInsertNewLine
    79 => Finished $ Just NormalInsertNewLineUp
    97 => Finished $ Just NormalInsertRight
    73 => Finished $ Just NormalInsertBeginningOfLine
    65 => Finished $ Just NormalInsertEndOfLine
    115 => Finished $ Just NormalSave
    113 => Finished $ Just NormalQuit
    120 => Finished $ Just NormalDeleteAt
    71 => Finished $ Just NormalBottom
    103 => Continuation $ \c2 => Finished $ if c2 == 'g' then Just NormalTop else Nothing
    100 => deleteParser
    124 => Finished $ Just NormalBeginningOfLine
    36 => Finished $ Just NormalEndOfLine
    101 => Finished $ Just NormalEndOfWord
    119 => Finished $ Just NormalBeginningOfNextWord
    98 => Finished $ Just NormalBeginningOfWord
    21 => Finished $ Just NormalPageUp
    4 => Finished $ Just NormalPageDown
    99 => changeParser
    _ => Finished Nothing

export
getNormalInput : IO (Maybe NormalInput)
getNormalInput = runParser (limit 4) getChar parser

ext: idr

max_stars_repo_name: PeterHajdu/peti

max_issues_repo_name: PeterHajdu/peti

max_forks_repo_name: PeterHajdu/peti


text:
||| Functions for accessing file metadata.
module System.File.Meta

import System.File.Handle
import System.File.Support
import public System.File.Types

%default total

%foreign support "idris2_fileSize"
         "node:lambda:fp=>require('fs').fstatSync(fp.fd).size"
prim__fileSize : FilePtr -> PrimIO Int

%foreign support "idris2_fileSize"
prim__fPoll : FilePtr -> PrimIO Int

%foreign support "idris2_fileAccessTime"
prim__fileAccessTime : FilePtr -> PrimIO Int

%foreign support "idris2_fileModifiedTime"
         "node:lambda:fp=>require('fs').fstatSync(fp.fd).mtimeMs / 1000"
prim__fileModifiedTime : FilePtr -> PrimIO Int

%foreign support "idris2_fileStatusTime"
prim__fileStatusTime : FilePtr -> PrimIO Int

%foreign support "idris2_fileIsTTY"
         "node:lambda:fp=>Number(require('tty').isatty(fp.fd))"
prim__fileIsTTY : FilePtr -> PrimIO Int

||| Check if a file exists for reading.
export
exists : HasIO io => String -> io Bool
exists f
    = do Right ok <- openFile f Read
             | Left err => pure False
         closeFile ok
         pure True

||| Pick the first existing file
export
firstExists : HasIO io => List String -> io (Maybe String)
firstExists [] = pure Nothing
firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs

||| Get the File's atime.
export
fileAccessTime : HasIO io => (h : File) -> io (Either FileError Int)
fileAccessTime (FHandle f)
    = do res <- primIO (prim__fileAccessTime f)
         if res > 0
            then ok res
            else returnError

||| Get the File's mtime.
export
fileModifiedTime : HasIO io => (h : File) -> io (Either FileError Int)
fileModifiedTime (FHandle f)
    = do res <- primIO (prim__fileModifiedTime f)
         if res > 0
            then ok res
            else returnError

||| Get the File's ctime.
export
fileStatusTime : HasIO io => (h : File) -> io (Either FileError Int)
fileStatusTime (FHandle f)
    = do res <- primIO (prim__fileStatusTime f)
         if res > 0
            then ok res
            else returnError

||| Get the File's size.
export
fileSize : HasIO io => (h : File) -> io (Either FileError Int)
fileSize (FHandle f)
    = do res <- primIO (prim__fileSize f)
         if res >= 0
            then ok res
            else returnError

||| Check whether the given File's size is non-zero.
export
fPoll : HasIO io => File -> io Bool
fPoll (FHandle f)
    = do p <- primIO (prim__fPoll f)
         pure (p > 0)

||| Check whether the given File is a terminal device.
export
isTTY : HasIO io => (h : File) -> io Bool
isTTY (FHandle f) = (/= 0) <$> primIO (prim__fileIsTTY f)


text:
{--
Copyright 2021 Joel Berkeley

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.
--}
||| This module contains common library types.
module Types

import public Data.Nat
import public Data.Vect

||| Describes the shape of a `Tensor`. For example, a `Tensor` of `Double`s with contents
||| `[[0, 1, 2], [3, 4, 5]]` has two elements in its outer-most axis, and each of those elements
||| has three `Double`s in it, so this has shape [2, 3]. A `Tensor` can have axes of zero length,
||| though the shape cannot be unambiguously inferred by visualising it. For example, `[[], []]`
||| can have shape [2, 0], [2, 0, 5] or etc. A scalar `Tensor` has shape `[]`.
|||
||| The rank is the number of elements in the shape, or equivalently the number of axes.
public export 0
Shape : {0 rank: Nat} -> Type
Shape = Vect rank Nat

||| An `Array shape` is either:
|||
||| * a single value of an implicitly inferred type `dtype` (for `shape` `[]`), or
||| * an arbitrarily nested array of `Vect`s of such values (for any other `shape`)
|||
||| @shape The shape of this array.
public export 0
Array : {0 dtype : Type} -> (0 shape : Shape) -> Type
Array {dtype} [] = dtype
Array {dtype} (d :: ds) = Vect d (Array ds {dtype=dtype})

max_stars_repo_name: joelberkeley/spidr

max_issues_repo_name: joelberkeley/spidr

max_forks_repo_name: joelberkeley/spidr


text:
module Network.HTTP.Pool.ConnectionPool

import Network.HTTP.Error
import Network.HTTP.Scheduler
import Network.HTTP.Protocol
import Network.HTTP.Message
import Network.HTTP.Header
import Network.HTTP.URL
import Network.HTTP.Pool.Worker
import Network.HTTP.Pool.Common
import Network.TLS
import Network.TLS.Signature
import Network.TLS.Verify
import Network.Socket
import Data.IORef
import Data.Bits
import Data.List
import Data.List1
import System
import System.Random
import System.Future
import System.Concurrency
import Utils.Queue

mutual
  record Pool (e : Type) where
    constructor MkPool
    workers : IORef (List (Worker e))
    ||| Increase everytime there is a new worker
    counter : IORef Bits32
    scheduled : Queue (Event e)
    last_called : IORef Integer

  export
  record PoolManager (e : Type) where
    constructor MkPoolManager
    pools : IORef (List (Hostname, Pool e))
    max_per_site_connections : Nat
    max_total_connections : Nat
    certificate_checker : (String -> CertificateCheck IO)

  record Worker (e : Type) where
    constructor MkWorker
    idle : IORef Bool
    ||| Unique id of the pool for identification
    uuid : Bits64
    protocol : Protocol
    ||| Kept in case we need to close externally
    socket : Socket
    parent : Pool e

Show (Worker e) where
  show worker = "Worker: \{show worker.protocol} \{show worker.uuid}"

export
new_pool_manager : HasIO io => Nat -> Nat -> (String -> CertificateCheck IO) -> io (PoolManager e)
new_pool_manager max_per_site_connections max_total_connections cert_check = liftIO $ do
  ref <- newIORef []
  pure (MkPoolManager ref max_per_site_connections max_total_connections cert_check)

pool_new_worker_id : Pool e -> IO Bits64
pool_new_worker_id pool = do
  r <- the (IO Int32) randomIO
  modifyIORef pool.counter (+ 1)
  c <- readIORef pool.counter
  pure $ (shiftL (cast r) 32) .|. cast c

find_or_create_pool : RawHttpMessage -> PoolManager e -> IO (Either (HttpError e) (Hostname, Pool e))
find_or_create_pool message manager = do
  pools <- readIORef manager.pools
  case lookup_header message.headers Host of
    Just host =>
      case lookup host pools of
        Just pool =>
          pure (Right (host, pool))
        Nothing => do
          pool <- pure $ MkPool !(newIORef []) !(newIORef 0) !(mk_queue) !(time >>= newIORef)
          modifyIORef manager.pools ((host, pool) ::)
          pure (Right (host, pool))
    Nothing => pure (Left UnknownHost)

single_pool_active_connections : Protocol -> Pool e -> IO Nat
single_pool_active_connections protocol pool = length . filter (\x => protocol == x.protocol) <$> readIORef pool.workers

export
total_active_connections : Protocol -> PoolManager e -> IO Nat
total_active_connections protocol manager = do
  pools <- readIORef manager.pools
  let pools = map snd pools
  foldlM (\a,b => (a+) <$> single_pool_active_connections protocol b) 0 pools

close_worker : Worker e -> IO ()
close_worker worker = do
  -- putStrLn "closing \{show worker}"
  close worker.socket
  let f = \w => w.uuid /= worker.uuid
  modifyIORef worker.parent.workers (filter f)

close_pool : {e : _} -> Condition -> Pool e -> IO ()
close_pool cond pool = do
  let queue = pool.scheduled
  remaining <- mapMaybe (\case Request x => Just x; _ => Nothing) <$> recv_all queue
  -- feed all awaiting requests with errors
  traverse_ (flip channelPut (Left ConnectionClosed) . response) remaining

  -- close all sockets
  workers <- readIORef pool.workers
  traverse_ (close . socket) workers

  -- broadcast kill event
  broadcast queue (Kill $ Just cond)

wait_for_worker_close : {e : _} -> Mutex -> Condition -> List (Pool e) -> IO ()
wait_for_worker_close mutex cond pools = do
  conditionWaitTimeout cond mutex 1000000
  workers <- traverse (\p => readIORef p.workers) pools
  -- putStrLn "waiting for pool close: \{show workers}"
  if null (join workers) then pure () else wait_for_worker_close mutex cond pools

has_idle_worker : Pool e -> IO Bool
has_idle_worker pool = readIORef pool.workers >>= loop where
  loop : List (Worker e) -> IO Bool
  loop [] = pure False
  loop (x :: xs) = readIORef x.idle >>= (\b => if b then pure True else loop xs)

pools_last_called : PoolManager e -> IO (List (Integer, Pool e))
pools_last_called manager = do
  pools <- readIORef manager.pools
  let pools = map snd pools
  flip traverse pools $ \pool => do
    t <- readIORef pool.last_called
    pure (t, pool)

spawn_worker : {e : _} -> Queue (Event e) -> (HttpError e -> IO ()) -> (String -> CertificateCheck IO) -> Protocol -> Hostname -> Pool e -> IO ()
spawn_worker fetcher throw cert_check protocol hostname pool = do
  worker_id <- pool_new_worker_id pool
  Right sock <- socket AF_INET Stream 0
  | Left err => throw $ SocketError "error when creating socket: \{show err}"
  idle_ref <- newIORef True
  let worker = MkWorker idle_ref worker_id protocol sock pool
  modifyIORef pool.workers (worker ::)
  let hostname_str = hostname_string hostname
  let port = case hostname.port of Just p => p; Nothing => protocol_port_number protocol
  0 <- connect sock (Hostname hostname.domain) (cast port)
  | err => throw $ SocketError "unable to connect to \{hostname_str}: \{show err}"
  let closer = close_worker worker
  worker_handle sock idle_ref closer fetcher throw cert_check protocol hostname_str

min_by : (ty -> ty -> Ordering) -> List1 ty -> ty
min_by compare (x ::: xs) = loop x xs where
  loop : ty -> List ty -> ty
  loop x [] = x
  loop x (y :: ys) =
    case compare x y of
      LT => loop x ys
      _  => loop y ys

export
{e : _} -> Scheduler e IO (PoolManager e) where
  schedule_request manager protocol request = do
    let throw = \err => channelPut request.response (Left err)
    Right (host, pool) <- find_or_create_pool request.raw_http_message manager
    | Left err => throw err

    -- update last called
    time >>= writeIORef pool.last_called

    signal pool.scheduled $ Request request

    {-
    1. if total connection is maxed and no local connection
      send kill to the last called pool
      spawn new thread
    2. else if local connection is not maxed and no idle
      spawn new thread
    -}

    local <- single_pool_active_connections protocol pool
    all <- total_active_connections protocol manager
    has_idle <- has_idle_worker pool

    let first_condition = (all >= manager.max_per_site_connections) && (local == Z)
    let second_condition = not first_condition && ((local < manager.max_per_site_connections) && not has_idle)

    when {f=IO} first_condition $ do
      pools_to_kill <- pools_last_called manager
      let Just pools_to_kill = fromList pools_to_kill
      | Nothing => pure () -- why is pool empty

      let (_, pool_to_kill) = min_by (\a,b => compare (fst a) (fst b)) pools_to_kill
      signal pool_to_kill.scheduled (Kill Nothing)
      _ <- forkIO $ spawn_worker pool.scheduled throw manager.certificate_checker protocol host pool
      pure ()

    when {f=IO} second_condition $ do
      _ <- forkIO $ spawn_worker pool.scheduled throw manager.certificate_checker protocol host pool
      pure ()

  evict_all manager = do
    pools <- readIORef manager.pools
    condition <- makeCondition
    mutex <- makeMutex
    writeIORef manager.pools []
    let pools = map snd pools
    mutexAcquire mutex
    traverse_ (close_pool condition) pools
    wait_for_worker_close mutex condition pools
    mutexRelease mutex


text:
import Data.Either
import Data.List
import Data.List1
import Data.Maybe
import Data.String
import Data.String.Parser

import System.File

Pipe : Type
Pipe = (Nat, Nat, Nat, Nat)

pipeParser : Parser Pipe
pipeParser = do x1 <- natural
                token ","
                y1 <- natural
                spaces1
                token "->"
                x2 <- natural
                token ","
                y2 <- natural
                pure (x1, y1, x2, y2)

parsePipe : String -> Maybe Pipe
parsePipe s = case parse pipeParser s of
                   Left _ => Nothing
                   Right (p, _) => Just p

parseLines : (String -> Maybe a) -> String -> List a
parseLines f s = catMaybes $ f <$> lines s

pipeToCoords : Pipe -> List (Nat, Nat)
pipeToCoords (x1, y1, x2, y2) = case (x1 == x2, y1 == y2) of
                                     (True, True) => (x1, y1) :: []
                                     (True, False) => (x1, y1) :: pipeToCoords (x1, if y1 < y2 then y1 + 1 else minus y1 1, x2, y2)
                                     (False, True) => (x1, y1) :: pipeToCoords (if x1 < x2 then x1 + 1 else minus x1 1, y1, x2, y2)
                                     (False, False) => (x1, y1) :: pipeToCoords (if x1 < x2 then x1 + 1 else minus x1 1, if y1 < y2 then y1 + 1 else minus y1 1, x2, y2)

run : String -> IO ()
run s = do let g = group $ sort $ join $ pipeToCoords <$> parseLines parsePipe s
           let c = (length . forget) <$> g
           let r = length $ filter (> 1) c
           putStrLn $ show r

main : IO ()
main = do Right s <- readFile "input.txt"
            | Left err => putStrLn $ show err
          run s


text:
module CIL.Elab.Enums

import CIL.FFI

import Language.Reflection.Utils

fullyQualify : TTName -> Elab TTName
fullyQualify name = NS name <$> currentNamespace

||| ~name : Type
||| ~name = TEnum ~cilTy ~reprTy
defEnumType : TTName -> Raw -> Raw -> Elab ()
defEnumType name cilTy reprTy = do
  declareType $
    Declare name [] RType
  defineFunction $
    DefineFun name [MkFunClause (Var name) `(CILEnum ~cilTy ~reprTy)]

||| ~fieldName : ~typeName
||| ~fieldName = theEnum {cilTy=~cilTy} {reprTy=~reprTy} ~fieldValue
defEnumField : TTName -> Raw -> Raw -> TTName -> Raw -> Elab ()
defEnumField typeName cilTy reprTy fieldName fieldValue = do
  fqn <- fullyQualify fieldName
  declareType $
    Declare fqn [] (Var typeName)
  defineFunction $
    DefineFun fqn [MkFunClause (Var fqn)
                              `(theEnum {cilTy=~cilTy} {reprTy=~reprTy} ~fieldValue)]

constOf : NativeTy -> Integer -> Elab Const
constOf IT32 = pure . B32 . fromInteger
constOf IT16 = pure . B16 . fromInteger
constOf ty   = const $ fail [TextPart ("Invalid enum native type: " ++ show ty)]

defEnumFields : TTName -> (cilTy : Raw) -> Raw -> NativeTy -> List (TTName, Integer) -> Elab ()
defEnumFields name cilTy reprTy nativeTy fields =
  for_ {b = Unit} fields $ \(fieldName, value) => do
    nativeValue <- constOf nativeTy value
    defEnumField name cilTy reprTy fieldName (RConstant nativeValue)

export
defEnum : TTName -> (cilTy : Raw) -> Raw -> List (TTName, Integer) -> Elab ()
defEnum name cilTy reprTy@(RConstant (AType (ATInt (ITFixed nativeTy)))) fields = do
  fqn <- fullyQualify name
  defEnumType fqn cilTy reprTy
  defEnumFields fqn cilTy reprTy nativeTy fields
defEnum _ _ reprTy _ =
  fail [TextPart ("Invalid enum representation type (must be either Bits16 or Bits32): " ++ show reprTy)]

syntax cilEnum {x} [cilTy] [reprTy] [fs] = defEnum `{{x}} `(cilTy) `(reprTy) fs

syntax cilField {x} [value] = (`{{x}}, value)

max_stars_repo_name: alaendle/idris-cil

max_issues_repo_name: alaendle/idris-cil

max_forks_repo_name: alaendle/idris-cil


text:
> module SequentialDecisionProblems.Utils

> import Data.Fin
> import Control.Isomorphism

> import SequentialDecisionProblems.CoreTheory

> import Finite.Predicates
> import Finite.Operations
> import Finite.Properties
> import Sigma.Sigma
> import Sigma.Operations
> import Sigma.Properties
> import Fun.Operations
> import Decidable.Predicates
> import Decidable.Properties

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

* Finiteness notions

> |||
> FiniteViable : Type
> FiniteViable = {t : Nat} ->
>                (n : Nat) -> (x : State t) -> Finite (Viable {t} n x)

> |||
> FiniteAll : Type
> FiniteAll = {A : Type} -> {P : A -> Type} ->
>             Finite1 P -> (ma : M A) -> Finite (All P ma)

> |||
> FiniteAllViable : Type
> FiniteAllViable = {t : Nat} ->
>                   (n : Nat) -> (mx : M (State t)) -> Finite (All (Viable n) mx)

> |||
> FiniteNotEmpty : Type
> FiniteNotEmpty = {A : Type} ->
>                  (ma : M A) -> Finite (NotEmpty ma)

> |||
> FiniteGood : Type
> FiniteGood = {t : Nat} -> {n : Nat} ->
>              (x : State t) -> (y : Ctrl t x) ->
>              Finite (Good t x n y)

> |||
> FiniteCtrl : Type
> FiniteCtrl = {t : Nat} ->
>              (x : State t) -> Finite (Ctrl t x)

> |||
> FiniteGoodCtrl : Type
> FiniteGoodCtrl = {t : Nat} -> {n : Nat} ->
>                  (x : State t) -> Viable {t = t} (S n) x ->
>                  Finite (GoodCtrl t x n)

* Decidability notions

> |||
> DecidableViable : Type
> DecidableViable = {t : Nat} ->
>                   (n : Nat) -> (x : State t) -> Dec (Viable {t} n x)

> |||
> DecidableAll : Type
> DecidableAll = {A : Type} -> {P : A -> Type} ->
>                Dec1 P -> (ma : M A) -> Dec (All P ma)

> |||
> DecidableAllViable : Type
> DecidableAllViable = {t : Nat} ->
>                      (n : Nat) -> (mx : M (State t)) -> Dec (All (Viable n) mx)

> |||
> DecidableNotEmpty : Type
> DecidableNotEmpty = {A : Type} ->
>                     (ma : M A) -> Dec (NotEmpty ma)

> |||
> DecidableGood : Type
> DecidableGood = {t : Nat} -> {n : Nat} ->
>                 (x : State t) -> (y : Ctrl t x) ->
>                 Dec (Good t x n y)

> |||
> DecidableGoodCtrl : Type
> DecidableGoodCtrl = {t : Nat} -> {n : Nat} ->
>                     (x : State t) -> Viable {t = t} (S n) x ->
>                     Dec (GoodCtrl t x n)

* Standard deduction patterns in the implementation of specific SDPs

We would like to provide users with a function

< finiteAllViable : FiniteAll -> FiniteViable -> FiniteAllViable

but, as it turns out, implementing this function is not trivial (see
issues 3135 and 3136). Thus, for the time being, we introduce 2
additional assumptions in the global context. If users can prove that
|All| is finite

> |||
> finiteAll : {A : Type} -> {P : A -> Type} ->
>             Finite1 P -> (ma : M A) -> Finite (All P ma)

and that |Viable| is finite,

> |||
> finiteViable : {t : Nat} ->
>                (n : Nat) -> (x : State t) -> Finite (Viable n x)

we deduce finiteness of |All Viable|:

> |||
> finiteAllViable : {t : Nat} ->
>                   (n : Nat) -> (mx : M (State t)) -> Finite (All (Viable n) mx)
> finiteAllViable n mx = finiteAll (finiteViable n) mx

Similarly, if users are able to prove that |NotEmpty| is finite

> finiteNotEmpty : {t : Nat} ->
>                  (mx : M (State t)) -> Finite (NotEmpty mx)

we can deduce finiteness of |Good|

> |||
> finiteGood : {t : Nat} ->
>              (n : Nat) -> (x : State t) ->
>              (y : Ctrl t x) -> Finite (Good t x n y)
> finiteGood {t} n x y = finiteProduct (finiteNotEmpty  {t = S t}   (nexts t x y ))
>                                      (finiteAllViable {t = S t} n (nexts t x y ))

and, assuming finiteness of controls, finiteness of |GoodCtrl|

> |||
> finiteCtrl : {t : Nat} -> (x : State t) -> Finite (Ctrl t x)

, finiteness of good controls:

> |||
> finiteGoodCtrl : {t : Nat} ->
>                  (n : Nat) -> (x : State t) -> Finite (GoodCtrl t x n)
> finiteGoodCtrl n x = finiteSigmaLemma0 (finiteCtrl x) (finiteGood n x)

Finally, we can show that, for states which are viable for more than
zero steps, good controls are not empty:

> |||
> cardNotZGoodCtrl : {t : Nat} ->
>                    (n : Nat) -> (x : State t) -> (v : Viable {t = t} (S n) x) ->
>                    CardNotZ (finiteGoodCtrl {t} n x)
> cardNotZGoodCtrl n x v = cardNotZLemma (finiteGoodCtrl n x) (viableSpec1 x v)

Similarly, we can provide standard deduction patterns for
decidability. If users can prove that |All| is decidable

> |||
> decidableAll : {A : Type} -> {P : A -> Type} ->
>                ((a : A) -> Dec (P a)) -> (ma : M A) -> Dec (All P ma)

and that |Viable| is decidable

> |||
> decidableViable : {t : Nat} ->
>                   (n : Nat) -> (x : State t) -> Dec (Viable n x)

we can deduce decidability of |All Viable|:

> |||
> decidableAllViable : {t : Nat} ->
>                      (n : Nat) -> (mx : M (State t)) -> Dec (All (Viable n) mx)
> decidableAllViable n mx = decidableAll (decidableViable n) mx

Further, if users are able to prove that |NotEmpty| is decidable

> |||
> decidableNotEmpty : {t : Nat} ->
>                     (mx : M (State t)) -> Dec (NotEmpty mx)

we can deduce decidability of |Good|

> |||
> decidableGood : {t : Nat} ->
>                 (n : Nat) -> (x : State t) ->
>                 (y : Ctrl t x) -> Dec (Good t x n y)
> decidableGood {t} n x y = decPair (decidableNotEmpty  {t = S t}   (nexts t x y))
>                                   (decidableAllViable {t = S t} n (nexts t x y))

and, assuming finiteness of controls, decidability of |GoodCtrl|:

> |||
> decidableGoodCtrl : {t : Nat} ->
>                     (n : Nat) -> (x : State t) -> Dec (GoodCtrl t x n)
> decidableGoodCtrl n x = finiteDecSigmaLemma (finiteCtrl x) (decidableGood n x)

We apply these patterns, for instance, in |ViabilityDefaults|.

* Show states and controls

> |||
> showState : {t : Nat} -> State t -> String

> |||
> showCtrl : {t : Nat} -> {x : State t} -> Ctrl t x -> String

> |||
> showStateCtrl : {t : Nat} -> Sigma (State t) (Ctrl t) -> String
> showStateCtrl {t} (MkSigma x y) = "(" ++ showState {t} x ++ " ** " ++ showCtrl {t} {x} y ++ ")"

* Sequences of state-control pairs

> |||
> data StateCtrlSeq : (t : Nat) -> (n : Nat) -> Type where
>   Nil   :  {t : Nat} -> (x : State t) -> StateCtrlSeq t Z
>   (::)  :  {t, n : Nat} -> Sigma (State t) (Ctrl t) -> StateCtrlSeq (S t) n -> StateCtrlSeq t (S n)

> using (t : Nat, n : Nat)
>   implementation Show (StateCtrlSeq t n) where
>     show = show' where
>       show' : {t : Nat} -> {n : Nat} -> StateCtrlSeq t n -> String
>       show' xys = "[" ++ show'' "" xys ++ "]" where
>         show'' : {t' : Nat} -> {n' : Nat} -> String -> StateCtrlSeq t' n' -> String
>         show'' {t'} {n' = Z}    acc (Nil x)     =
>           acc ++ "(" ++ showState x ++ " ** " ++ " " ++ ")"
>         show'' {t'} {n' = S m'} acc (xy :: xys) =
>           show'' {t' = S t'} {n' = m'} (acc ++ showStateCtrl xy ++ ", ") xys

> |||
> valStateCtrlSeq : (t : Nat) -> (n : Nat) -> StateCtrlSeq t n -> Val
> valStateCtrlSeq t       Z   (Nil x) =
>   zero
> valStateCtrlSeq t    (S Z)  ((MkSigma x y) :: (Nil x')) =
>   reward t x y x'
> valStateCtrlSeq t (S (S m)) ((MkSigma x y) :: (MkSigma x' y') :: xys) =
>   reward t x y x' `plus` valStateCtrlSeq (S t) (S m) ((MkSigma x' y') :: xys)

* Trajectories

> ||| The monadic operations
> ret   :  {A : Type} -> A -> M A
> bind  :  {A, B : Type} -> M A -> (A -> M B) -> M B
> postulate monadSpec1   :  {A, B : Type} -> {f : A -> B} ->
>                           (fmap f) . ret = ret . f
> postulate monadSpec21  :  {A, B : Type} -> {f : A -> M B} -> {a : A} ->
>                           bind (ret a) f = f a
> postulate monadSpec22  :  {A : Type} -> {ma : M A} ->
>                           bind ma ret = ma
> postulate monadSpec23  :  {A, B, C : Type} -> {f : A -> M B} -> {g : B -> M C} -> {ma : M A} ->
>                           bind (bind ma f) g = bind ma (\ a => bind (f a) g)

> |||
> possibleStateCtrlSeqs  :  {t, n : Nat} -> (x : State t) -> (r : Reachable x) -> (v : Viable n x) ->
>                           (ps : PolicySeq t n) -> M (StateCtrlSeq t n)
> possibleStateCtrlSeqs {t} {n = Z}    x r v Nil         =  ret (Nil x)
> {-
> possibleStateCtrlSeqs {t} {n = S m}  x r v (p :: ps')  =
>   fmap g (bind (tagElem mx') f) where
>     y   :  Ctrl t x
>     y   =  ctrl (p x r v)
>     mx' :  M (State (S t))
>     mx' =  nexts t x y
>     av  :  All (Viable m) mx'
>     av  =  allViable (p x r v)
>     g   :  StateCtrlSeq (S t) m -> StateCtrlSeq t (S m)
>     g   =  ((MkSigma x y) ::)
>     f   :  Sigma (State (S t)) (\ x' => x' `Elem` mx') -> M (StateCtrlSeq (S t) m)
>     f (MkSigma x' x'emx') = possibleStateCtrlSeqs {n = m} x' r' v' ps' where
>       ar  :  All Reachable mx'
>       ar  =  reachableSpec1 x r y
>       r'  :  Reachable x'
>       r'  =  allElemSpec0 x' mx' ar x'emx'
>       v'  :  Viable m x'
>       v'  =  allElemSpec0 x' mx' av x'emx'
> -}
> possibleStateCtrlSeqs {t} {n = S m}  x r v (p :: ps')  =
>   let y   :  Ctrl t x
>           =  ctrl (p x r v) in
>   let mx' :  M (State (S t))
>           =  nexts t x y in
>   let av  :  All (Viable m) mx'
>           =  allViable (p x r v) in
>   let g   :  (StateCtrlSeq (S t) m -> StateCtrlSeq t (S m))
>           =  ((MkSigma x y) ::) in
>   let ar  :  All Reachable mx'
>           =  reachableSpec1 x r y in
>   let r'  :  ((x' : State (S t)) -> x' `Elem` mx' -> Reachable x')
>           =  \ x' => \ x'emx' => allElemSpec0 x' mx' ar x'emx' in
>   let v'  :  ((x' : State (S t)) -> x' `Elem` mx' -> Viable m x')
>           =  \ x' => \ x'emx' => allElemSpec0 x' mx' av x'emx' in
>   let f   :  (Sigma (State (S t)) (\ x' => x' `Elem` mx') -> M (StateCtrlSeq (S t) m))
>           =  \ (MkSigma x' x'emx') => possibleStateCtrlSeqs {n = m} x' (r' x' x'emx') (v' x' x'emx') ps' in
>   fmap g (bind (tagElem mx') f)

> |||
> morePossibleStateCtrlSeqs  :  {t, n : Nat} -> (mx : M (State t)) ->
>                               All Reachable mx -> All (Viable n) mx ->
>                               (ps : PolicySeq t n) -> M (StateCtrlSeq t n)
> morePossibleStateCtrlSeqs {t} {n}  mx ar av ps  =  bind (tagElem mx) f where
>   f : Sigma (State t) (\ x => x `Elem` mx) -> M (StateCtrlSeq t n)
>   f (MkSigma x xemx) = possibleStateCtrlSeqs x r v ps where
>       r  :  Reachable x
>       r  =  allElemSpec0 x mx ar xemx
>       v  :  Viable n x
>       v  =  allElemSpec0 x mx av xemx

> |||
> possibleStateCtrlSeqsRewards : {t : Nat} -> {n : Nat} ->
>                                (x : State t) -> (r : Reachable x) -> (v : Viable n x) ->
>                                (ps : PolicySeq t n) -> M (StateCtrlSeq t n, Val)
> possibleStateCtrlSeqsRewards {t} {n} x r v ps =
>   fmap (pair (id, valStateCtrlSeq t n)) (possibleStateCtrlSeqs {t} {n} x r v ps)

> |||
> possibleStateCtrlSeqsRewards' : {t : Nat} -> {n : Nat} ->
>                                 M (StateCtrlSeq t n) -> M (StateCtrlSeq t n, Val)
> possibleStateCtrlSeqsRewards' {t} {n} xys = fmap (pair (id, valStateCtrlSeq t n)) xys

> |||
> possibleRewards : {t : Nat} -> {n : Nat} ->
>                   (x : State t) -> (r : Reachable x) -> (v : Viable n x) ->
>                   (ps : PolicySeq t n) -> M Val
> possibleRewards {t} {n} x r v ps =
>   fmap (valStateCtrlSeq t n) (possibleStateCtrlSeqs {t} {n} x r v ps)

> |||
> possibleRewards' : {t : Nat} -> {n : Nat} -> M (StateCtrlSeq t n) -> M Val
> possibleRewards' {t} {n} xys = fmap (valStateCtrlSeq t n) xys

* Computation of specific trajectories via selection function

> {-
> |||
> stateCtrlSeq : {t, n : Nat} ->
>                (x : State t) -> (r : Reachable x) -> (v : Viable n x) ->
>                (ps : PolicySeq t n) ->
>                (eps : {A : Type} -> M A -> A) ->
>                StateCtrlSeq t n
> stateCtrlSeq {t} {n = Z}    x r v Nil        eps =  Nil x
> stateCtrlSeq {t} {n = S m}  x r v (p :: ps') eps =
>   (MkSigma x y) :: (eps (fmap f (tagElem mx'))) where
>     y   :  Ctrl t x
>     y   =  ctrl (p x r v)
>     mx' :  M (State (S t))
>     mx' =  nexts t x y
>     av  :  All (Viable m) mx'
>     av  =  allViable (p x r v)
>     f   :  Sigma (State (S t)) (\ x' => x' `Elem` mx') -> StateCtrlSeq (S t) m
>     f (MkSigma x' x'emx') = res where -- stateCtrlSeq {t = S t} {n = m} x' r' v' ps' eps where
>       ar  :  All Reachable mx'
>       ar  =  reachableSpec1 x r y
>       r'  :  Reachable x'
>       r'  =  allElemSpec0 x' mx' ar x'emx'
>       v'  :  Viable m x'
>       v'  =  allElemSpec0 x' mx' av x'emx'
>       res :  StateCtrlSeq (S t) m
>       res =  ?kika
> -}

* Alternative computation of trajectories

> |||
> app : {t, m, n : Nat} ->
>       StateCtrlSeq t m -> Policy (t + m) (S n) -> M (StateCtrlSeq t (S m))
> app {t} {m = Z} {n} (Nil {t} x) p = fmap (f . g) (nexts t x y) where
>   postulate r : Reachable x
>   postulate v : Viable (S n) x
>   q : Policy t (S n)
>   q = replace {P = \ X => Policy X (S n)} (plusZeroRightNeutral t) p
>   y : Ctrl t x
>   y = ctrl (q x r v)
>   f : StateCtrlSeq (S t) Z -> StateCtrlSeq t (S Z)
>   f nx' = (MkSigma x y) :: nx'
>   g : State (S t) -> StateCtrlSeq (S t) Z
>   g x' = Nil x'
> app {t} {m = S m'} {n} (xy :: xys) p = fmap f (app xys q) where
>   f : StateCtrlSeq (S t) (S m') -> StateCtrlSeq t (S (S m'))
>   f = (xy ::)
>   q : Policy (S t + m') (S n)
>   q = replace {P = \ X => Policy X (S n)} (sym (plusSuccRightSucc t m')) p

> |||
> extend : {t, m, n : Nat} ->
>          M (StateCtrlSeq t m) -> PolicySeq (t + m) n -> M (StateCtrlSeq t (m + n))
> extend mxys {t} {m} {n = Z}         Nil  =
>   replace {P = \ X => M (StateCtrlSeq t X)} (sym (plusZeroRightNeutral m)) mxys
> extend mxys {t} {m} {n = S n'} (p :: ps) = s2 where
>   s1 : M (StateCtrlSeq t (plus (S m) n'))
>   s1 = extend mxys' (replace {P = \ X => PolicySeq X n'} (plusSuccRightSucc t m) ps) where
>     mxys' : M (StateCtrlSeq t (S m))
>     mxys' = bind mxys f where
>       f : StateCtrlSeq t m ->  M (StateCtrlSeq t (S m))
>       f xys = app xys p
>   s2 : M (StateCtrlSeq t (plus m (S n')))
>   s2 = replace {P = \ X => M (StateCtrlSeq t X)} (plusSuccRightSucc m n') s1

> possibleStateCtrlSeqs1 : {t, n : Nat} -> (x : State t) -> (r : Reachable x) -> (v : Viable n x) ->
>                          (ps : PolicySeq t n) -> M (StateCtrlSeq t n)
> possibleStateCtrlSeqs1 {t} {n} x r v ps = s2 where
>   s1 : M (StateCtrlSeq t (Z + n))
>   s1 = extend (ret (Nil {t} x)) (replace {P = \ X => PolicySeq X n} (sym (plusZeroRightNeutral t)) ps)
>   s2 : M (StateCtrlSeq t n)
>   s2 = replace {P = \ X => M (StateCtrlSeq t X)} (plusZeroLeftNeutral n) s1

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
> module Nat.GCDEuclid

> import Nat.GCD
> import Nat.Divisor
> import Nat.DivisorProperties
> import Nat.Operations
> import Nat.LTEProperties
> import Nat.OperationsProperties
> import Sigma.Sigma
> import Pairs.Operations

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

Euclid's greatest common divisor algorithm

> euclidGCD1 : GCD m m Z
> euclidGCD1 {m} = MkGCD (anyDivisorAny m) (anyDivisorZ m) (\ d' => \ d'Dm => \ d'DZ => d'Dm)

> euclidGCD2 : GCD m Z m
> euclidGCD2 {m} = MkGCD (anyDivisorZ m) (anyDivisorAny m) (\ d' => \ d'DZ => \ d'Dm => d'Dm)

> euclidGCD3 : m `LTE` n -> GCD d m (n - m) -> GCD d m n
> euclidGCD3 {m} {n} {d} p (MkGCD dDm dDnmm q) = MkGCD dDm dDn q' where
>   dDnmmpm : d `Divisor` ((n - m) + m)
>   dDnmmpm = divisorPlusLemma2 m (n - m) d dDm dDnmm
>   dDn : d `Divisor` n
>   dDn = replace {x = (n - m) + m}
>                 {y = n}
>                 {P = \ ZUZU => d `Divisor` ZUZU}
>                 (plusRightInverseMinus m n p)
>                 dDnmmpm
>   q' : (d' : Nat) -> d' `Divisor` m -> d' `Divisor` n -> d' `Divisor` d
>   q' d' d'Dm d'Dn = q d' d'Dm d'Dnmm where
>     d'Dnmm : d' `Divisor` (n - m)
>     d'Dnmm = divisorMinusLemma m n d' d'Dm d'Dn

> euclidGCD4 : Not (m `LTE` n) -> GCD d (m - n) n -> GCD d m n
> euclidGCD4 {m} {n} {d} p (MkGCD dDmmn dDn q) = MkGCD dDm dDn q' where
>   dDmmnpn : d `Divisor` ((m - n) + n)
>   dDmmnpn = divisorPlusLemma1 (m - n) n d dDmmn dDn
>   dDm : d `Divisor` m
>   dDm = replace {x = (m - n) + n}
>                 {y = m}
>                 {P = \ ZUZU => d `Divisor` ZUZU}
>                 (plusRightInverseMinus n m (notLTELemma1 m n p))
>                 dDmmnpn
>   q' : (d' : Nat) -> d' `Divisor` m -> d' `Divisor` n -> d' `Divisor` d
>   q' d' d'Dm d'Dn = q d' d'Dmmn d'Dn where
>     d'Dmmn : d' `Divisor` (m - n)
>     d'Dmmn = divisorMinusLemma n m d' d'Dn d'Dm

> euclidGCD : (m : Nat) -> (n : Nat) -> Sigma Nat (\ d => GCD d m n)
> euclidGCD    m   Z    = assert_total (MkSigma m euclidGCD1)
> euclidGCD  Z       n  = assert_total (MkSigma n euclidGCD2)
> euclidGCD (S m) (S n) with (decLTE (S m) (S n))
>   | (Yes p) = assert_total (MkSigma gcd (euclidGCD3 p P)) where
>     gcdP : Sigma Nat (\ d => GCD d (S m) (S n - S m))
>     gcdP = euclidGCD (S m) (S n - S m)
>     gcd  : Nat
>     gcd  = getWitness gcdP
>     P    : GCD gcd (S m) (S n - S m)
>     P    = getProof gcdP
>   | (No  p) = assert_total (MkSigma gcd (euclidGCD4 p P)) where
>     gcdP : Sigma Nat (\ d => GCD d (S m - S n) (S n))
>     gcdP = euclidGCD (S m - S n) (S n)
>     gcd  : Nat
>     gcd  = getWitness gcdP
>     P    : GCD gcd (S m - S n) (S n)
>     P    = getProof gcdP


text:
-- --------------------------------------------------------------- [ LaTeX.idr ]
-- Module    : LaTeX.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Text.Markup.Edda.Writer.LaTeX

import Data.AVL.Dict

import Effects
import Effect.File
import Effect.Exception

import Text.Markup.Edda.Model

import Text.Markup.Edda.Writer.Common

-- -------------------------------------------------------------- [ Directives ]
%default total
%access private

-- ------------------------------------------------------------ [ Misc Writing ]

macro : String -> String -> String
macro c s = concat ["\\", c, "{", s, "}"]

-- ----------------------------------------------------------- [ Write Inlines ]

mutual
  export
  inlines : List (Edda INLINE) -> String
  inlines xs = assert_total (concatMap inline xs)

  parens : String -> String -> List (Edda INLINE) -> String
  parens l r ts = concat [l, inlines ts, r]

  link : String -> List (Edda INLINE) -> String
  link uri Nil  = macro "url"  uri
  link uri desc = concat [macro "href" uri, "{", inlines desc, "}"]

  inline : Edda INLINE -> String
  inline (Text t) = t
  inline (Sans t) = macro "textsf" t
  inline (Scap t) = macro "textsc" t
  inline (Mono t) = macro "texttt" t
  inline (Verb v)     = "\\verb!" ++ v ++ "!"
  inline (Code v)     = macro "texttt" v
  inline (Math v)     = "$" ++ v ++ "$"
  inline (Emph t)     = macro "emph"      (inlines t)
  inline (Bold t)     = macro "textbf"    (inlines t )
  inline (Strike t)   = macro "sout"      (inlines t)
  inline (Uline t)    = macro "underline" (inlines t)
  inline (Quote ty t) =
    case ty of
      SQuote => macro "squote" (inlines t)
      DQuote => macro "dquote" (inlines t)
  inline (Parens ty t) =
    case ty of
      Parents  => parens "("   ")"   t
      Brackets => parens "["   "]"   t
      Braces   => parens "\\{" "\\}" t
  inline (Ref url)        = link url Nil
  inline (Hyper uri desc) = link uri desc
  inline (FNote l d)   = macro "footnote" (inlines d)
  inline (Cite ty uri) =
    case ty of
      ParenSty => (macro "cite"  uri)
      TextSty  => (macro "citet" uri)
  inline (MiscPunc c) =
    case c of
      '%' => "\\%"
      '_' => "\\_"
      '^' => "\\^"
      '~' => "\\~"
      c   => cast c
  inline Space      = " "
  inline Newline    = "\n"
  inline Tab        = "\t"
  inline LBrace     = "\\{"
  inline RBrace     = "\\}"
  inline LParen     = "("
  inline RParen     = ")"
  inline LBrack     = "["
  inline RBrack     = "]"
  inline LAngle     = "\\textless"
  inline RAngle     = "\\textgreater"
  inline Dollar     = "\\$"
  inline Colon      = ":"
  inline Semi       = ";"
  inline EnDash     = "--"
  inline EmDash     = "---"
  inline FSlash     = "/"
  inline BSlash     = "\\"
  inline Apostrophe = "'"
  inline SMark      = "\""
  inline Comma      = ","
  inline Plus       = "+"
  inline Ellipsis   = "\\ldots"
  inline Hyphen     = "-"
  inline Bang       = "!"
  inline Period     = "."
  inline QMark      = "?"
  inline Hash       = "\\#"
  inline Equals     = "="
  inline Pipe       = "$\\mid$"

-- ----------------------------------------------------- [ Write Generic Block ]
env : String -> String -> String
env n body = unlines
    [ macro "begin" (toLower n)
    , body
    , macro "end" (toLower n)]

thm : String
   -> Maybe String
   -> List (Edda INLINE)
   -> List (Edda INLINE)
   -> String
thm e l c b = env (toLower e) body
  where
    body : String
    body = unlines
      [ "[" ++ inlines c ++ "]"
      , strFromMaybe (macro "label") l
      , inlines b
      ]

figure : Maybe String
      -> List (Edda INLINE)
      -> String
      -> String
figure l c body = env ("figure") body'
  where
    body' : String
    body' = unlines
      [ body
      , macro "caption" $ inlines c
      , macro "label"   $ fromMaybe "missing" l
      ]

-- Make generic
list : String -> List (List (Edda INLINE)) -> String
list s is = env s (unlines $ map item is)
  where
    item : List (Edda INLINE) -> String
    item bs = unwords ["\\item", inlines bs, "\n"]

dlist : List (Pair (List (Edda INLINE)) (List (Edda INLINE))) -> String
dlist kvs = env "description" (unlines $ map descItem kvs)
  where
    descItem : (List (Edda INLINE), List (Edda INLINE)) -> String
    descItem (k,v) = unwords ["\\item[" ++ inlines k ++ "]", inlines v]

secLvl : Nat -> List (Edda INLINE) -> String
secLvl Z                 t = macro "section"       (inlines t)
secLvl (S Z)             t = macro "subsection"    (inlines t)
secLvl (S (S Z))         t = macro "subsubsection" (inlines t)
secLvl (S (S (S Z)))     t = macro "paragraph"     (inlines t)
secLvl (S (S (S (S Z)))) t = macro "subparagraph"  (inlines t)
secLvl _                 t = inlines t ++ " % Depth not recognised\n"

-- ------------------------------------------------------------- [ Write Block ]
-- deal with attrs
||| Write block to LaTeX version.
export
block : Edda BLOCK -> String
block (HRule) = "\\hrulefill"
block (Empty) = "\n"
block (Section lvl label title as body) = assert_total $
    unlines $ unwords [ secLvl lvl title
                      , strFromMaybe (macro "label") label
                      , "\n"]
              :: map block body

block (Figure l c as fig) = figure l c (inline fig)
block (DList kvs)         = dlist kvs
block (OList bs)          = list "itemize"  bs
block (BList bs)          = list "enumerate" bs

block (Para txt) = inlines txt ++ "\n\n"

block (Listing l c lang langopts as src) = figure l c (env "verbatim" src)

block (Comment ss)          = env "comment" ss
block (Equation l eq)       = env "equation" eq  -- Add support for caption and label
block (Literal l c src)     = env "verbatim" src -- Add support for caption and label

block (Quotation l txt)     = thm "QUOTE" l Nil txt
block (Theorem l c txt)     = thm "Theorem" l c txt
block (Corollary l c txt)   = thm "COROLLARY" l c txt
block (Lemma l c txt)       = thm "LEMMA" l c txt
block (Proposition l c txt) = thm "PROPOSITION" l c txt
block (Proof l c txt)       = thm "PROOF" l c txt
block (Definition l c txt)  = thm "DEFINITION" l c txt
block (Exercise l c txt)    = thm "EXERCISE" l c txt
block (Note l c txt)        = thm "NOTE" l c txt
block (Remark l c txt)      = thm "REMARK" l c txt
block (Problem l c txt)     = thm "PROBLEM" l c txt
block (Question l c txt)    = thm "QUESTION" l c txt
block (Solution l c txt)    = thm "SOLUTION" l c txt
block (Example l c txt)     = thm "EXAMPLE" l c txt

export
blocks : (List (Edda BLOCK)) -> String
blocks = concatMap block
-- -------------------------------------------------------- [ Write List (String, String) ]

properties : List (Edda INLINE) -> Dict String String -> String
properties t ps  = unlines
    [ macro "title"  $ inlines t
    , macro "author" $ fromMaybe "author missing" (lookup "AUTHOR" ps)
    , macro "date"   $ fromMaybe "date missing"   (lookup "DATE" ps)
    , "\n"
    ]

-- --------------------------------------------------------------- [ Write Org ]

namespace Doc
  --@ TODO Add customisable preamble, and standalone
  ||| Convert document to LaTeX instance.
  export
  toLaTeX : Edda DOC -> String
  toLaTeX (Doc title ps body) = unlines
      [ """\documentclass{article}
  \usepackage{thmtools}
  \usepackage[normelem]{ulem}
  \usepackage{hyperref}

  \declaretheoremstyle[%
    spaceabove=6pt, spacebelow=6pt,
    headfont=\normalfont\bfseries,
    bodyfont=\normalfont\em,
    postheadspace=1em
  ]{thmstyle}

  \declaretheoremstyle[%
    spaceabove=6pt, spacebelow=6pt,
    headfont=\normalfont\bfseries,
    bodyfont=\normalfont,
    postheadspace=1em
  ]{notestyle}

  \newcommand{\squote}[1]{`#1'}
  \newcommand{\dquote}[1]{``#1''}

  \declaretheorem[style=notestyle, starred, name={\textbf{Note}}]{note}
  \declaretheorem[style=notestyle, starred, name={\textbf{Remark}}]{remark}
  \declaretheorem[style=thmstyle, name={Definition}]{definition}
  \declaretheorem[style=thmstyle, name={Example}]{example}
  \declaretheorem[style=thmstyle, name={Exercise}]{exercise}
  \declaretheorem[style=thmstyle, name={Problem}]{problem}
  \declaretheorem[style=thmstyle, name={Question}]{question}
  \declaretheorem[style=thmstyle, name={Solution}]{solution}

  \declaretheorem[style=thmstyle, name={Corollary}]{corollary}
  \declaretheorem[style=thmstyle, name={Lemma}]{lemma}
  \declaretheorem[style=thmstyle, name={Proposition}]{proposition}
  \declaretheorem[style=thmstyle, name={Theorem}]{theorem}
  """
      , properties title ps
      , "\\begin{document}\n\\maketitle"
      , concatMap block body
      , "\\end{document}"
      ]

namespace File

  ||| Write LaTeX representation to file.
  export
  toLaTeXE : String
            -> Edda DOC
            -> Eff (FileOpSuccess) [FILE ()]
  toLaTeXE fn doc = writeEddaFileE toLaTeX fn doc

  ||| Write LaTeX representation to file.
  export
  toLaTeX : String
           -> Edda DOC
           -> IO (Either FileError ())
  toLaTeX fn doc = writeEddaFile toLaTeX fn doc

namespace Snippet
  ||| Convert edda document to latex.
  export
  toLaTeX : Edda SNIPPET -> String
  toLaTeX (Snippet snippet prf) with (prf)
    toLaTeX (Snippet snippet prf) | IsInLine = inlines snippet
    toLaTeX (Snippet snippet prf) | IsBlock = blocks snippet

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

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
module Compo

import Service
import Numeric
import Halfer
import Twicer
import Incrementer

%default total

-- composition of Twicer and Incrementer
compo1 : Integer -> Service (Integer)
compo1 a = do
            n <- twicerService a
            incrementerService n

-- composition of Twicer, Halfer, and Incrementer
compo2 : Integer -> Service (Integer)
compo2 a = do
            i <- twicerService a
    -- Because twicerService does not provide its own proof that its
    -- output is always even, we use a Promise to provide a soft proof
    -- of this property.
            p <- Promise ?con
            j <- halferService (cast i ** p)
            incrementerService j

-- invalid composition of Twicer, Incrementer, and Halfer
compo3 : Integer -> Service (Integer)
compo3 a = do
            i <- twicerService a
            j <- incrementerService i
    -- The `resolve` hole shows that the programmer must create apply some logic
    -- of type Integer -> EvenNumber to resolve the mismatch here.
            halferService $ ?resolve j

-- A potential method to resolve the above mismatch
compo3sol : Integer -> Service (Integer)
compo3sol a = do
            i <- twicerService a
            j <- incrementerService i
    -- Because this function contains the actual composition of the various
    -- Services, this is the point where the programmer is best able to decide
    -- which measures are acceptable to resolve type mismatches.
    -- In this case, forceEven is used.
            halferService $ forceEven j

-- In this composition, we have no way to statically prove that
-- halferService is being passed an even number.
compo4 : Integer -> Service (Integer)
compo4 a = do
    -- i could be even or odd, depending on the value of a
            i <- incrementerService a
    -- We can pattern match on the result of a runtime test
    -- to create a branch in the logic of this Service.
            Just j <- pure $ maybeEven i
                 | Nothing => twicerService i
    -- If there is a Just EvenNumber, run the halferService on it.
    -- If there is no EvenNumber value to be found, run the twicerService on i.
            halferService j

-- Because all of the above examples are Integer -> Service (Integer),
-- it is relatively trivial to compose them.
compo5 : Integer -> Service (Integer)
compo5 a = (compo1 a) >>= compo2 >>= compo3 >>= compo4

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
module Unitary

import Data.Vect
import Data.Nat
import System.File
import Injection
import Lemmas

infixr 9 .
infixr 10 #

%default total

------------------------QUANTUM CIRCUITS-----------------------

public export
data Unitary : Nat -> Type where
  IdGate : Unitary n
  H      : (j : Nat) -> {auto prf : (j < n) = True} -> Unitary n -> Unitary n
  P      : (p : Double) -> (j : Nat) -> {auto prf : (j < n) = True} -> Unitary n -> Unitary n
  CNOT   : (c : Nat) -> (t : Nat) ->
            {auto prf1 : (c < n) = True} -> {auto prf2 : (t < n) = True} -> {auto prf3 : (c /= t) = True} ->
            Unitary n -> Unitary n

-- P p = [[1,0],[0,e^ip]]

-------------------------------APPLY---------------------------
|||Apply a smaller circuit of size i to a bigger one of size n
|||The vector of wires on which we apply the circuit must follow some constraints:
|||All the indices must be smaller than n, and they must be all different
public export
apply : {i : Nat} -> {n : Nat} ->
        Unitary i -> Unitary n ->
        (v : Vect i Nat) ->
        {auto prf : (isInjective n v) = True} ->
        Unitary n
apply IdGate g2 _ = g2
apply (H j g1) g2 v =
  let prf1 = indexInjectiveVect j n v {prf}
  in H (index j v) {prf = prf1} (apply g1 g2 v)
apply (P p j g1) g2 v =
  let prf1 = indexInjectiveVect j n v {prf}
  in P p (index j v) {prf = prf1} (apply g1 g2 v)
apply {i} {n} (CNOT c t {prf1} {prf2} {prf3} g1) g2 v =
  let prf4 = indexInjectiveVect c n v {prf = prf}
      prf5 = indexInjectiveVect t n v {prf = prf}
      prf6 = differentIndexInjectiveVect c t n {prf1 = prf3} v {prf2 = prf} {prf3 = prf1} {prf4 = prf2}
  in CNOT (index c v) (index t v) {prf1 = prf4} {prf2 = prf5} {prf3 = prf6} (apply g1 g2 v)

---------------------------COMPOSE-----------------------------
|||Compose 2 circuits of the same size
public export
compose : Unitary n -> Unitary n -> Unitary n
compose IdGate g1 = g1
compose (H j g1) g2 = H j (compose g1 g2)
compose (P p j g1) g2 = P p j (compose g1 g2)
compose (CNOT c t g1) g2 = CNOT c t (compose g1 g2)

public export
(.) : Unitary n -> Unitary n -> Unitary n
(.) = compose

---------------------------ADJOINT-----------------------------
|||Find the adjoint of a circuit
public export
adjoint : Unitary n -> Unitary n
adjoint IdGate = IdGate
adjoint (H j g) = (adjoint g) . (H j IdGate)
adjoint (P p j g) = (adjoint g) . (P (-p) j IdGate)
adjoint (CNOT c t g) = (adjoint g) . (CNOT c t IdGate)

---------------------TENSOR PRODUCT----------------------------
|||Make the tensor product of two circuits
public export
tensor : {n : Nat} -> {p : Nat} -> Unitary n -> Unitary p -> Unitary (n + p)
tensor g1 g2 =
  let p1 = (allSmallerRangeVect 0 n)
      p2 = lemmaAnd (allSmallerRangeVect n p) (allDiffRangeVect n p)
      p3 = allSmallerPlus n p (rangeVect 0 n) p1
      p4 = lemmaAnd p3 (allDiffRangeVect 0 n)
      g' = apply {i=n} {n = n+p} g1 (IdGate {n = n+p}) (rangeVect 0 n) {prf = p4}
  in apply {i = p} {n = n + p} g2 g' (rangeVect n p) {prf = p2}

public export
(#) : {n : Nat} -> {p : Nat} -> Unitary n -> Unitary p -> Unitary (n + p)
(#) = tensor

----------------------CLASSICAL GATES--------------------------
public export
HGate : Unitary 1
HGate = H 0 IdGate

public export
PGate : Double -> Unitary 1
PGate r = P r 0 IdGate

public export
CNOTGate : Unitary 2
CNOTGate = CNOT 0 1 IdGate

public export
T : (j : Nat) -> {auto prf : (j < n) = True} -> Unitary n -> Unitary n
T j g = P (pi/4) j {prf} g

public export
TGate : Unitary 1
TGate = T 0 IdGate

public export
TAdj : (j : Nat) -> {auto prf : (j < n) = True} -> Unitary n -> Unitary n
TAdj j g = P (-pi/4) j {prf} g

public export
TAdjGate : Unitary 1
TAdjGate = TAdj 0 IdGate

public export
S : (j : Nat) -> {auto prf : (j < n) = True} -> Unitary n -> Unitary n
S j g = P (pi/2) j {prf} g

public export
SGate : Unitary 1
SGate = S 0 IdGate

public export
SAdj : (j : Nat) -> {auto prf : (j < n) = True} -> Unitary n -> Unitary n
SAdj j g = P (-pi/2) j {prf} g

public export
SAdjGate : Unitary 1
SAdjGate = SAdj 0 IdGate

public export
Z : (j : Nat) -> {auto prf : (j < n) = True} -> Unitary n -> Unitary n
Z j g = P pi j {prf} g

public export
ZGate : Unitary 1
ZGate = Z 0 IdGate

public export
X : (j : Nat) -> {auto prf : (j < n) = True} -> Unitary n -> Unitary n
X j g = H j (Z j (H j g))

public export
XGate : Unitary 1
XGate = X 0 IdGate

public export
RxGate : Double -> Unitary 1
RxGate p = HGate . PGate p . HGate

public export
RyGate : Double -> Unitary 1
RyGate p = SAdjGate . HGate . PGate (-p) . HGate . SGate

public export
RzGate : Double -> Unitary 1
RzGate p = PGate p

---------------------CONTROLLED VERSIONS-----------------------
|||Toffoli gate
public export
toffoli : Unitary 3
toffoli =
  let g1 = CNOT 1 2 (H 2 IdGate)
      g2 = CNOT 0 2 (TAdj 2 g1)
      g3 = CNOT 1 2 (T 2 g2)
      g4 = CNOT 0 2 (TAdj 2 g3)
      g5 = CNOT 0 1 (T 1 (H 2 (T 2 g4)))
  in CNOT 0 1 (T 0 (TAdj 1 g5))

|||Controlled Hadamard gate
public export
controlledH : Unitary 2
controlledH =
  let h1 = (IdGate {n=1}) # (SAdjGate . HGate . TGate . HGate . SGate)
      h2 = (IdGate {n=1}) # (SAdjGate . HGate . TAdjGate . HGate . SGate)
  in h1 . CNOTGate . h2

|||Controlled phase gate
public export
controlledP : Double -> Unitary 2
controlledP p =
  let p1 = CNOT 0 1 (P (p/2) 1 IdGate)
  in CNOT 0 1 (P (-p/2) 1 p1)

|||Make the controlled version of a gate
public export
controlled : {n : Nat} -> Unitary n -> Unitary (S n)
controlled IdGate = IdGate
controlled (H j g) =
  let p = lemmaControlledInj n j
  in apply {i = 2} {n = S n} controlledH (controlled g) [0, S j] {prf = p}
controlled (P p j g) =
  let p1 = lemmaControlledInj n j
  in apply {i = 2} {n = S n} (controlledP p) (controlled g) [0, S j] {prf = p1}
controlled (CNOT c t g) =
  let p = lemmaControlledInj2 n c t
  in apply {i = 3} {n = S n} toffoli (controlled g) [0, S c, S t] {prf = p}

------------SOME USEFUL FUNCTIONS FOR CREATING GATES-----------

|||Make n tensor products of the same unitary of size 1
public export
tensorn : (n : Nat) -> Unitary 1 -> Unitary n
tensorn 0 _ = IdGate
tensorn (S k) g = g # (tensorn k g)

|||Controls on the n-1 first qubits, target on the last
public export
multipleQubitControlledNOT : (n : Nat) -> Unitary n
multipleQubitControlledNOT 0 = IdGate
multipleQubitControlledNOT 1 = IdGate
multipleQubitControlledNOT 2 = CNOT 0 1 IdGate
multipleQubitControlledNOT (S k) = controlled (multipleQubitControlledNOT k)

||| Tensor product of a Vector of Unitary operators
export
tensorMap : {n : Nat} -> {m : Nat} -> (gates : Vect n (Unitary m)) -> Unitary (n*m)
tensorMap [] = IdGate
tensorMap (gate :: gates) = gate # (tensorMap gates)

||| Tensor product of a Vector of single-qubit Unitary operators
export
tensorMapSimple : {n : Nat} -> (gates : Vect n (Unitary 1)) -> Unitary n
tensorMapSimple g = rewrite sym $ multOneRightNeutral n in tensorMap g

---------------------------------------------------------------
-- count the total number of atomic gates in a unitary circuit
export
gateCount : Unitary n -> Nat
gateCount IdGate = 0
gateCount (H j x) = S (gateCount x)
gateCount (P p j x) = S (gateCount x)
gateCount (CNOT c t x) = S (gateCount x)

--count the number of H gates in a unitary circuit
export
Hcount : Unitary n -> Nat
Hcount IdGate = 0
Hcount (H j x) = S (Hcount x)
Hcount (P p j x) = Hcount x
Hcount (CNOT c t x) = Hcount x

--count the number of P gates in a unitary circuit
export
Pcount : Unitary n -> Nat
Pcount IdGate = 0
Pcount (H j x) = Pcount x
Pcount (P p j x) = S (Pcount x)
Pcount (CNOT c t x) = Pcount x

--count the number of CNOT gates in a unitary circuit
export
CNOTcount : Unitary n -> Nat
CNOTcount IdGate = 0
CNOTcount (H j x) = CNOTcount x
CNOTcount (P p j x) = CNOTcount x
CNOTcount (CNOT c t x) = S (CNOTcount x)

----------------------------DEPTH------------------------------
|||Compute the depth of  circuit

addDepth : Nat -> (j : Nat) -> Vect n Nat -> {auto prf : j < n = True} -> Vect n Nat
addDepth j 0 (x :: xs) = j :: xs
addDepth j (S k) (x :: xs) = x :: addDepth j k xs

findValue : (j : Nat) -> Vect n Nat -> {auto prf : j < n = True} -> Nat
findValue 0 (x::xs) = x
findValue (S k) (x::xs) = findValue k xs

depth' : {n : Nat} -> Unitary n -> Vect n Nat
depth' IdGate = replicate n 0
depth' (H j x) =
  let v = depth' x
      k = findValue j v
  in addDepth (S k) j v
depth' (P p j x) =
  let v = depth' x
      k = findValue j v
  in addDepth (S k) j v
depth' (CNOT c t x) =
  let v = depth' x
      k = findValue c v
      m = findValue t v
  in if k < m then
              let w = addDepth (S m) c v
              in addDepth (S m) t w
     else
              let w = addDepth (S k) c v
              in addDepth (S k) t w

export
depth : {n : Nat} -> Unitary n -> Nat
depth g =
  let v = depth' g
  in foldl max 0 v

----------------------------SHOW-------------------------------
|||For printing the phase gate (used for show, export to Qiskit and draw in the terminal)
|||printPhase : phase -> precision -> string for pi -> String
private
printPhase : Double -> Double -> String -> String
printPhase x epsilon s =
  if x >= pi - epsilon && x <= pi + epsilon then s
  else if x >= pi/2 - epsilon && x <= pi/2 + epsilon then s ++ "/2"
  else if x >= pi/3 - epsilon && x <= pi/3 + epsilon then s ++ "/3"
  else if x >= pi/4 - epsilon && x <= pi/4 + epsilon then s ++ "/4"
  else if x >= pi/6 - epsilon && x <= pi/6 + epsilon then s ++ "/6"
  else if x >= pi/8 - epsilon && x <= pi/8 + epsilon then s ++ "/8"
  else if x >= -pi - epsilon && x <= -pi + epsilon then "-" ++ s
  else if x >= -pi/2 - epsilon && x <= -pi/2 + epsilon then "-" ++ s ++ "/2"
  else if x >= -pi/3 - epsilon && x <= -pi/3 + epsilon then "-" ++ s ++ "/3"
  else if x >= -pi/4 - epsilon && x <= -pi/4 + epsilon then "-" ++ s ++ "/4"
  else if x >= -pi/6 - epsilon && x <= -pi/6 + epsilon then "-" ++ s ++ "/6"
  else if x >= -pi/8 - epsilon && x <= -pi/8 + epsilon then "-" ++ s ++ "/8"
  else show x

public export
Show (Unitary n) where
  show IdGate = ""
  show (H j x) = "(H " ++ show j ++ ") " ++ show x
  show (P p j x) = "(P " ++ printPhase p 0.001 "π" ++ " " ++ show j ++ ") " ++ show x
  show (CNOT c t x) = "(CNOT " ++ show c ++ " " ++ show t ++ ") " ++ show x

-----------------DRAW CIRCUITS IN THE TERMINAL-----------------

private
newWireQVect : (n : Nat) -> Vect n String
newWireQVect Z = []
newWireQVect (S k) = "" :: newWireQVect k

private
addSymbol : Nat -> Bool -> (String, String) -> Vect n String -> Vect n String
addSymbol _ _ _ [] = []
addSymbol 0 False (s1, s2) (x :: xs) = (x ++ s1) :: addSymbol 0 True  (s1, s2) xs
addSymbol 0 True  (s1, s2) (x :: xs) = (x ++ s2) :: addSymbol 0 True  (s1, s2) xs
addSymbol (S k) _ (s1, s2) (x :: xs) = (x ++ s2) :: addSymbol k False (s1, s2) xs

private
addSymbolCNOT : (Nat, Nat) -> Bool -> Bool -> Vect n String -> Vect n String
addSymbolCNOT _ _ _ [] = []
addSymbolCNOT (0,0)    False b (x :: xs) = (x ++ "- • -") :: addSymbolCNOT (0, 0) True b xs
addSymbolCNOT (0, S k) False b (x :: xs) = (x ++ "- • -") :: addSymbolCNOT (0, k) True b xs
addSymbolCNOT (0, 0)   b False (x :: xs) = (x ++ "- Θ -") :: addSymbolCNOT (0, 0) b True xs
addSymbolCNOT (S k, 0) b False (x :: xs) = (x ++ "- Θ -") :: addSymbolCNOT (k, 0) b True xs
addSymbolCNOT (0, 0) True True (x :: xs) = (x ++ "-----") :: addSymbolCNOT (0, 0) True True xs
addSymbolCNOT (S j, S k) _ _   (x :: xs) = (x ++ "-----") :: addSymbolCNOT (j, k) False False xs
addSymbolCNOT (0, S k) True _  (x :: xs) = (x ++ "--|--") :: addSymbolCNOT (0, k) True False xs
addSymbolCNOT (S k, 0) _ True  (x :: xs) = (x ++ "--|--") :: addSymbolCNOT (k, 0) False True xs

private
drawWirePhase : Nat -> String
drawWirePhase 0 = ""
drawWirePhase (S n) = "-" ++ drawWirePhase n

private
drawGate : {n : Nat} -> Unitary n -> Vect n String
drawGate {n} IdGate = newWireQVect n
drawGate (H i g) = addSymbol i False ("- H -", "-----") (drawGate g)
drawGate (P p i g) =
  let epsilon = 0.001 in
  if pi/4 - epsilon <= p && pi/4 + epsilon >= p
    then addSymbol i False ("- T -", "-----") (drawGate g)
  else if -pi/4 - epsilon <= p && -pi/4 + epsilon >= p
    then addSymbol i False ("- T+ -", "------") (drawGate g)
  else if pi/2 - epsilon <= p && pi/2 + epsilon >= p
    then addSymbol i False ("- S -", "-----") (drawGate g)
  else if -pi/2 - epsilon <= p && -pi/2 + epsilon >= p
    then addSymbol i False ("- S+ -", "------") (drawGate g)
  else if pi - epsilon <= p && pi + epsilon >= p
    then addSymbol i False ("- Z -", "-----") (drawGate g)
  else let s = printPhase p epsilon "π"
  in addSymbol i False ("- P(" ++ s ++ ") -", drawWirePhase (length s + 7)) (drawGate g)
drawGate (CNOT i j g) = addSymbolCNOT (i,j) False False (drawGate g)

private
drawVect : Vect n String -> String
drawVect [] = ""
drawVect (x :: xs) = x ++ "\n" ++ drawVect xs

|||Draw a circuit in the terminal
public export
draw : {n : Nat} ->  Unitary n -> IO ()
draw g =
  let vs1 = drawGate {n} g in
  let s = drawVect vs1 in
  putStrLn s

--------------------------EXPORT TO QISKIT---------------------

private
unitarytoQiskit : Unitary n -> String
unitarytoQiskit IdGate = ""
unitarytoQiskit (H i g) = unitarytoQiskit g ++  "qc.h(qr[" ++ show i ++ "])\n"
unitarytoQiskit (P p i g) = unitarytoQiskit g ++ "qc.p(" ++ printPhase p 0.001 "np.pi" ++ ", qr[" ++ show i ++ "])\n"
unitarytoQiskit (CNOT c t g) = unitarytoQiskit g ++ "qc.cx(qr[" ++ show c ++ "], qr[" ++ show t ++ "])\n"

private
toQiskit : {n : Nat} -> Unitary n -> String
toQiskit g =
  let s = unitarytoQiskit g in
  ("import numpy as np\n" ++
  "from qiskit import QuantumCircuit\n" ++
  "from qiskit import QuantumRegister\n" ++
  "qr = QuantumRegister(" ++ show n ++ ")\n" ++
  "qc = QuantumCircuit(qr)\n\n" ++ s ++
  "\nqc.draw('mpl')")

|||Export a circuit to Qiskit code
public export
exportToQiskit : {n : Nat} -> String -> Unitary n -> IO ()
exportToQiskit str g =
  let s = toQiskit g in
      do
        a <- writeFile str s
        case a of
             Left e1 => putStrLn "Error when writing file"
             Right io1 => pure ()

max_stars_repo_name: zamdzhiev/Qimaera

max_issues_repo_name: zamdzhiev/Qimaera

max_forks_repo_name: zamdzhiev/Qimaera


text:
module Effect.StdIO

import Effects
import Control.IOExcept

data StdIO : Effect where
     PutStr : String -> { () } StdIO ()
     GetStr : { () } StdIO String

instance Handler StdIO IO where
    handle () (PutStr s) k = do putStr s; k () ()
    handle () GetStr     k = do x <- getLine; k x ()

{-
instance Handler StdIO (IOExcept a) where
    handle () (PutStr s) k = do ioe_lift (putStr s); k () ()
    handle () GetStr     k = do x <- ioe_lift getLine; k () x

-- Handle effects in a pure way, for simulating IO for unit testing/proof

data IOStream a = MkStream (List String -> (a, List String))

instance Handler StdIO IOStream where
    handle () (PutStr s) k
       = MkStream (\x => case k () () of
                         MkStream f => let (res, str) = f x in
                                           (res, s :: str))
    handle {a} () GetStr k
       = MkStream (\x => case x of
                              [] => cont "" []
                              (t :: ts) => cont t ts)
        where
            cont : String -> List String -> (a, List String)
            cont t ts = case k () t of
                             MkStream f => f ts

-}

--- The Effect and associated functions

STDIO : EFFECT
STDIO = MkEff () StdIO

putStr : Handler StdIO e => String -> { [STDIO] } Eff e ()
putStr s = PutStr s

putStrLn : Handler StdIO e => String -> { [STDIO] } Eff e ()
putStrLn s = putStr (s ++ "\n")

getStr : Handler StdIO e => { [STDIO] } Eff e String
getStr = GetStr

-- mkStrFn : Env IOStream xs ->
--           Eff IOStream xs a ->
--           List String -> (a, List String)
-- mkStrFn {a} env p input = case mkStrFn' of
--                                MkStream f => f input
--   where injStream : a -> IOStream a
--         injStream v = MkStream (\x => (v, []))
--         mkStrFn' : IOStream a
--         mkStrFn' = runWith injStream env p
--
--

max_stars_repo_name: edwinb/Eff-new

max_issues_repo_name: edwinb/Eff-new

max_forks_repo_name: edwinb/Eff-new


text:
module Main
import Cgi
import Effects

sayHello : Maybe String -> FormHandler [CGI (InitialisedCGI TaskRunning)]
sayHello (Just name) = output ("Hello, " ++ name ++ "!")

handlers : HandlerList
handlers = [(handler args=[FormString], effects=[CgiEffect], fn=sayHello, name="sayHello")]

showHelloForm : UserForm
showHelloForm = do
  addTextBox "Name" FormString Nothing
  useEffects [CgiEffect]
  addSubmit sayHello handlers

cgiHello : CGIProg [] ()
cgiHello = do
  handler_set <- isHandlerSet
  if handler_set then do
    handleForm handlers
    return ()
  else do
    addForm "nameform" "helloform" showHelloForm
    return ()

main : IO ()
main = runCGI [initCGIState] cgiHello

max_stars_repo_name: idris-hackers/IdrisWeb

max_issues_repo_name: idris-hackers/IdrisWeb

max_forks_repo_name: idris-hackers/IdrisWeb


text:
> module FastSimpleProb.Functor

> import FastSimpleProb.SimpleProb
> import FastSimpleProb.MonadicOperations

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

> ||| |SimpleProb| is a functor:
> implementation Functor SimpleProb where
>   map = fmap

> {-

> ---}


text:
module Main

double : Int -> Int
double x = 2 * x

triple : Int -> Int
triple x = 10 * x

multiply : Int -> Int -> Int
multiply x y = x * y

IntFun : Type
IntFun = (Int -> Int)

data TheAlt : Type where
  MyCon : IntFun -> Lazy IntFun -> TheAlt

runCon : TheAlt -> Int -> Int
runCon (MyCon a b) i = let x = a i in if x > 5 then x else (b i)

main : IO ()
main = do
  let obj = MyCon double (multiply 100)
  --let obj = MyCon double triple
  printLn $ runCon obj 1
  printLn $ runCon obj 2
  printLn $ runCon obj 3

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module Data.List.Quantifiers

import Data.DPair

import Data.List.Elem

%default total

------------------------------------------------------------------------
-- Types and basic properties

namespace Any

  ||| A proof that some element of a list satisfies some property
  |||
  ||| @ p the property to be satisfied
  public export
  data Any : (0 p : a -> Type) -> List a -> Type where
    ||| A proof that the satisfying element is the first one in the `List`
    Here  : {0 xs : List a} -> p x -> Any p (x :: xs)
    ||| A proof that the satisfying element is in the tail of the `List`
    There : {0 xs : List a} -> Any p xs -> Any p (x :: xs)

  export
  Uninhabited (Any p Nil) where
    uninhabited (Here _) impossible
    uninhabited (There _) impossible

  export
  {0 p : a -> Type} -> Uninhabited (p x) => Uninhabited (Any p xs) => Uninhabited (Any p $ x::xs) where
    uninhabited (Here y) = uninhabited y
    uninhabited (There y) = uninhabited y

  ||| Modify the property given a pointwise function
  export
  mapProperty : (f : {0 x : a} -> p x -> q x) -> Any p l -> Any q l
  mapProperty f (Here p) = Here (f p)
  mapProperty f (There p) = There (mapProperty f p)

  ||| Given a decision procedure for a property, determine if an element of a
  ||| list satisfies it.
  |||
  ||| @ p the property to be satisfied
  ||| @ dec the decision procedure
  ||| @ xs the list to examine
  export
  any : (dec : (x : a) -> Dec (p x)) -> (xs : List a) -> Dec (Any p xs)
  any _ Nil = No uninhabited
  any p (x::xs) with (p x)
    any p (x::xs) | Yes prf = Yes (Here prf)
    any p (x::xs) | No ctra =
      case any p xs of
        Yes prf' => Yes (There prf')
        No ctra' => No $ \case
          Here px => ctra px
          There pxs => ctra' pxs

  ||| Forget the membership proof
  export
  toExists : Any p xs -> Exists p
  toExists (Here prf) = Evidence _ prf
  toExists (There prf) = toExists prf

namespace All

  ||| A proof that all elements of a list satisfy a property. It is a list of
  ||| proofs, corresponding element-wise to the `List`.
  public export
  data All : (0 p : a -> Type) -> List a -> Type where
    Nil  : All p Nil
    (::) : {0 xs : List a} -> p x -> All p xs -> All p (x :: xs)

  Either (Uninhabited $ p x) (Uninhabited $ All p xs) => Uninhabited (All p $ x::xs) where
    uninhabited @{Left  _} (px::pxs) = uninhabited px
    uninhabited @{Right _} (px::pxs) = uninhabited pxs

  ||| Modify the property given a pointwise function
  export
  mapProperty : (f : {0 x : a} -> p x -> q x) -> All p l -> All q l
  mapProperty f [] = []
  mapProperty f (p::pl) = f p :: mapProperty f pl

  ||| Modify the property given a pointwise interface function
  public export
  imapProperty : (0 i : Type -> Type)
              -> (f : {0 a : Type} -> i a => p a -> q a)
              -> {0 types : List Type}
              -> All i types => All p types -> All q types
  imapProperty i f @{[]} [] = []
  imapProperty i f @{ix :: ixs} (x :: xs) = f @{ix} x :: imapProperty i f @{ixs} xs

  ||| Forget property source for a homogeneous collection of properties
  public export
  forget : All (const type) types -> List type
  forget [] = []
  forget (x :: xs) = x :: forget xs

  ||| Given a decision procedure for a property, decide whether all elements of
  ||| a list satisfy it.
  |||
  ||| @ p the property
  ||| @ dec the decision procedure
  ||| @ xs the list to examine
  export
  all : (dec : (x : a) -> Dec (p x)) -> (xs : List a) -> Dec (All p xs)
  all _ Nil = Yes Nil
  all d (x::xs) with (d x)
    all d (x::xs) | No ctra = No $ \(p::_) => ctra p
    all d (x::xs) | Yes prf =
      case all d xs of
        Yes prf' => Yes (prf :: prf')
        No ctra' => No $ \(_::ps) => ctra' ps

  export
  zipPropertyWith : (f : {0 x : a} -> p x -> q x -> r x) ->
                    All p xs -> All q xs -> All r xs
  zipPropertyWith f [] [] = []
  zipPropertyWith f (px :: pxs) (qx :: qxs)
    = f px qx :: zipPropertyWith f pxs qxs

  export
  All Show (map p xs) => Show (All p xs) where
    show pxs = "[" ++ show' "" pxs ++ "]"
      where
        show' : String -> All Show (map p xs') => All p xs' -> String
        show' acc @{[]} [] = acc
        show' acc @{[_]} [px] = acc ++ show px
        show' acc @{_ :: _} (px :: pxs) = show' (acc ++ show px ++ ", ") pxs

  ||| A heterogeneous list of arbitrary types
  public export
  HList : List Type -> Type
  HList = All id

------------------------------------------------------------------------
-- Relationship between all and any

||| If there does not exist an element that satifies the property, then it is
||| the case that all elements do not satisfy it.
export
negAnyAll : {xs : List a} -> Not (Any p xs) -> All (Not . p) xs
negAnyAll {xs=Nil}   _ = Nil
negAnyAll {xs=x::xs} f = (f . Here) :: negAnyAll (f . There)

||| If there exists an element that doesn't satify the property, then it is
||| not the case that all elements satisfy it.
export
anyNegAll : Any (Not . p) xs -> Not (All p xs)
anyNegAll (Here ctra) (p::_)  = ctra p
anyNegAll (There np)  (_::ps) = anyNegAll np ps

||| If none of the elements satisfy the property, then not any single one can.
export
allNegAny : All (Not . p) xs -> Not (Any p xs)
allNegAny [] p = absurd p
allNegAny (np :: npxs) (Here p) = absurd (np p)
allNegAny (np :: npxs) (There p) = allNegAny npxs p

||| Given a proof of membership for some element, extract the property proof for it
public export
indexAll : Elem x xs -> All p xs -> p x
indexAll  Here     (p::_  ) = p
indexAll (There e) ( _::ps) = indexAll e ps

--- Relations between listwise `All` and elementwise `Subset` ---

||| Push in the property from the list level with element level
public export
pushIn : (xs : List a) -> (0 _ : All p xs) -> List $ Subset a p
pushIn []      []      = []
pushIn (x::xs) (p::ps) = Element x p :: pushIn xs ps

||| Pull the elementwise property out to the list level
public export
pullOut : (xs : List $ Subset a p) -> Subset (List a) (All p)
pullOut [] = Element [] []
pullOut (Element x p :: xs) = let Element ss ps = pullOut xs in Element (x::ss) (p::ps)

export
pushInOutInverse : (xs : List a) -> (0 prf : All p xs) -> pullOut (pushIn xs prf) = Element xs prf
pushInOutInverse [] [] = Refl
pushInOutInverse (x::xs) (p::ps) = rewrite pushInOutInverse xs ps in Refl

export
pushOutInInverse : (xs : List $ Subset a p) -> uncurry Quantifiers.pushIn (pullOut xs) = xs
pushOutInInverse [] = Refl
pushOutInInverse (Element x p :: xs) with (pushOutInInverse xs)
  pushOutInInverse (Element x p :: xs) | subprf with (pullOut xs)
    pushOutInInverse (Element x p :: xs) | subprf | Element ss ps = rewrite subprf in Refl


text:
> module FastSimpleProb.BasicOperations

> import Data.List
> import Data.So
> import Syntax.PreorderReasoning

> import FastSimpleProb.SimpleProb
> import Double.Predicates
> import NonNegDouble.NonNegDouble
> import NonNegDouble.Constants
> import NonNegDouble.BasicOperations
> import NonNegDouble.Operations
> import NonNegDouble.Properties
> import NonNegDouble.Postulates
> import List.Operations
> import List.Properties
> import Fun.Operations
> import Pairs.Operations

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

> using implementation NumNonNegDouble
>   |||
>   mkSimpleProb : {A : Type} ->
>                  (aps : List (A, NonNegDouble)) ->
>                  {auto prf : Positive (toDouble (sumMapSnd aps))} ->
>                  SimpleProb A
>   mkSimpleProb aps {prf} = MkSimpleProb aps prf

> |||
> toList : {A : Type} -> SimpleProb A -> List (A, NonNegDouble)
> toList (MkSimpleProb aps _) = aps

> |||
> support : {A : Type} -> SimpleProb A -> List A
> support = (map fst) . toList

> using implementation NumNonNegDouble
>   |||
>   rescale : {A : Type} ->
>             (p : NonNegDouble) -> Positive (toDouble p) -> SimpleProb A -> SimpleProb A
>   rescale {A} p pp (MkSimpleProb aps psum) = MkSimpleProb aps' psum' where
>     aps'  : List (A, NonNegDouble)
>     aps'  = mapIdRightMult (aps, p)
>     psum' : Positive (toDouble (sumMapSnd aps'))
>     psum' = mapIdRightMultPreservesPositivity aps psum p pp

> using implementation NumNonNegDouble
>   using implementation FractionalNonNegDouble
>     |||
>     normalize : {A : Type} ->
>                 SimpleProb A -> SimpleProb A
>     normalize (MkSimpleProb aps psum) =
>       let p  : NonNegDouble
>              = one / (sumMapSnd aps) in
>       let pp : Positive (toDouble p)
>              = divPreservesPositivity positiveOne psum in
>       rescale p pp (MkSimpleProb aps psum)

> |||
> weights : {A : Type} -> SimpleProb A -> List NonNegDouble
> weights = (map snd) . toList

> using implementation NumNonNegDouble
>   ||| 'weight sp a' is the weight of 'a' according to 'sp'
>   weight : {A : Type} -> (Eq A) => SimpleProb A -> A -> NonNegDouble
>   weight sp a = foldr f (fromInteger 0) (toList sp) where
>     f : (A, NonNegDouble) -> NonNegDouble -> NonNegDouble
>     f (a', w') w = if (a == a') then w + w' else w

> using implementation FractionalNonNegDouble
>   ||| 'prob sp a' is the probability of 'a' according to 'sp'
>   prob : {A : Type} -> (Eq A) => SimpleProb A -> A -> NonNegDouble
>   prob sp a = (weight sp a) / (sum (weights sp))

> {-
> ||| 'prob sp a' is the probability of 'a' according to 'sp'
> prob : {A : Type} -> (Eq A) => SimpleProb A -> A -> Double
> prob sp a = fst pq / snd pq where
>   f : (A, Double) -> (Double, Double) -> (Double, Double)
>   f (a', p') (p, q) = if (a == a') then (p + p', q + p') else (p, q + p')
>   pq : (Double, Double)
>   pq = foldr f (0.0, 0.0) (toList sp)
> -}

> using implementation NumNonNegDouble
>   ||| Make a SimpleProb in which all elements of a list have the same
>   ||| probablility. If the list has no duplicates, this results in a
>   ||| uniform probability distribution
>   mkFlatSimpleProb : {A : Type} -> (as : List A) -> List.Operations.NonEmpty as -> SimpleProb A
>   mkFlatSimpleProb      Nil              prf = absurd prf
>   mkFlatSimpleProb {A} (a :: Nil)        _   = MkSimpleProb [(a, one)] positiveOne
>   mkFlatSimpleProb {A} (a :: (a' :: as)) _   = MkSimpleProb aps prf where
>     ps' : SimpleProb A
>     ps' = assert_total (mkFlatSimpleProb (a' :: as) ())
>     aps : List (A, NonNegDouble)
>     aps = (a, one) :: (toList ps')
>     prf : Positive (toDouble (sumMapSnd aps))
>     prf = sumMapSndConsLemma1 a 1.0 positiveOne (MkLTE Oh) (toList ps')

> using implementation NumNonNegDouble
>   using implementation EqNonNegDouble
>     |||
>     trim : {A : Type} -> (Eq A) =>
>            SimpleProb A -> SimpleProb A
>     trim {A} (MkSimpleProb aps psum) = MkSimpleProb aps' psum' where
>       aps'  : List (A, NonNegDouble)
>       aps'  = discardBySndZeroEq aps
>       psum' : Positive (toDouble (sumMapSnd aps'))
>       psum' = replace {P = \ X => Positive (toDouble X)} (sym (discardBySndZeroLemmaEq aps)) psum

> using implementation ShowNonNegDouble
>   |||
>   showlong : {A : Type} -> Show A => SimpleProb A -> String
>   showlong sp = showlong (toList sp)

> {-

> ---}


text:
||| This module is inspired by the open union used in the paper
||| Freer Monads, More Extensible Effects
||| by Oleg Kiselyov and Hiromi Ishii
|||
||| By using an AtIndex proof, we are able to get rid of all of the unsafe
||| coercions in the original module.

module Data.OpenUnion

import Data.DPair
import Data.List.AtIndex
import Data.List.HasLength
import Data.Nat
import Data.Nat.Order.Properties
import Decidable.Equality
import Syntax.WithProof

%default total

||| An open union of families is an index picking a family out together with
||| a value in the family thus picked.
public export
data Union : (elt : a -> Type) -> (ts : List a) -> Type where
  Element : (k : Nat) -> (0 _ : AtIndex t ts k) -> elt t -> Union elt ts

||| An empty open union of families is empty
public export
Uninhabited (Union elt []) where
  uninhabited (Element _ p _) = void (uninhabited p)

||| Injecting a value into an open union, provided we know the index of
||| the appropriate type family.
inj' : (k : Nat) -> (0 _ : AtIndex t ts k) -> elt t -> Union elt ts
inj' = Element

||| Projecting out of an open union, provided we know the index of the
||| appropriate type family. This may obviously fail if the value stored
||| actually corresponds to another family.
prj' : (k : Nat) -> (0 _ : AtIndex t ts k) -> Union elt ts -> Maybe (elt t)
prj' k p (Element k' q t) with (decEq k  k')
  prj' k p (Element k q t) | Yes Refl = rewrite atIndexUnique p q in Just t
  prj' k p (Element k' q t) | No neq = Nothing

||| Given that equality of type families is not decidable, we have to
||| rely on the interface `Member` to automatically find the index of a
||| given family.
public export
inj : Member t ts => elt t -> Union elt ts
inj = let (Element n p) = isMember t ts in inj' n p

||| Given that equality of type families is not decidable, we have to
||| rely on the interface `Member` to automatically find the index of a
||| given family.
public export
prj : Member t ts => Union elt ts -> Maybe (elt t)
prj = let (Element n p) = isMember t ts in prj' n p

||| By doing a bit of arithmetic we can figure out whether the union's value
||| came from the left or the right list used in the index.
public export
split : Subset Nat (HasLength ss) ->
        Union elt (ss ++ ts) -> Either (Union elt ss) (Union elt ts)
split m (Element n p t) with (@@ lt n (fst m))
  split m (Element n p t) | (True ** lt)
    = Left (Element n (strengthenL m lt p) t)
  split m (Element n p t) | (False ** notlt)
    = let 0 lte : lte (fst m) n === True
                = LteIslte (fst m) n (notltIsGTE n (fst m) notlt)
      in Right (Element (minus n (fst m)) (strengthenR m lte p) t)

||| We can inspect an open union over a non-empty list of families to check
||| whether the value it contains belongs either to the first family or any
||| other in the tail.
public export
decomp : Union elt (t :: ts) -> Either (Union elt ts) (elt t)
decomp (Element 0     (Z)   t) = Right t
decomp (Element (S n) (S p) t) = Left (Element n p t)

||| An open union over a singleton list is just a wrapper
public export
decomp0 : Union elt [t] -> elt t
decomp0 elt = case decomp elt of
  Left t => absurd t
  Right t => t

||| Inserting new union members on the right leaves the index unchanged.
public export
weakenR : Union elt ts -> Union elt (ts ++ us)
weakenR (Element n p t) = Element n (weakenR p) t

||| Inserting new union members on the left, requires shifting the index by
||| the number of members introduced. Note that this number is the only
||| thing we need to keep around at runtime.
public export
weakenL : Subset Nat (HasLength ss) -> Union elt ts -> Union elt (ss ++ ts)
weakenL m (Element n p t) = Element (fst m + n) (weakenL m p) t


text:
module Test.Inigo.Package.PackageDepsTest

import IdrTest.Test
import IdrTest.Expectation

import Data.List
import Inigo.Async.Promise
import Inigo.Package.PackageDeps
import SemVar.Data
import Test.Inigo.Package.PackageTest
import Toml

exampleDepsToml : String
exampleDepsToml = """
['1.2.3']
deps.a='=5.0.0'
dev.b='=6.0.0'

['1.2.4']
deps.a='=5.1.0'
dev.b='=6.1.0'
"""

exampleDepsExp : PackageDeps
exampleDepsExp =
  [ ((MkVersion 1 2 3 Nothing Nothing), (
      MkPackageDep
        [(["a"], (EQ (MkVersion 5 0 0 Nothing Nothing)))]
        [(["b"], (EQ (MkVersion 6 0 0 Nothing Nothing)))]
    ))
  , ((MkVersion 1 2 4 Nothing Nothing), (
      MkPackageDep
        [(["a"], (EQ (MkVersion 5 1 0 Nothing Nothing)))]
        [(["b"], (EQ (MkVersion 6 1 0 Nothing Nothing)))]
    ))
  ]

exampleDepsExpExt : PackageDeps
exampleDepsExpExt =
  [ ((MkVersion 1 2 3 Nothing Nothing), (
      MkPackageDep [] []
    ))
  , ((MkVersion 0 0 1 (Just "pre") Nothing), (
      MkPackageDep [] []
    ))
  , ((MkVersion 1 2 4 Nothing Nothing), (
      MkPackageDep [] []
    ))
  ]

toTomlTest : Test
toTomlTest =
  test "To Toml" (\_ => assertEq
    (toToml exampleDepsExp)
    [ ( ["1.2.3", "deps", "a"], Str "=5.0.0" )
    , ( ["1.2.3", "dev", "b"], Str "=6.0.0" )
    , ( ["1.2.4", "deps", "a"], Str "=5.1.0" )
    , ( ["1.2.4", "dev", "b"], Str "=6.1.0" )
    ]
  )

encodePackageDepsTest : Test
encodePackageDepsTest =
  test "Encode package index" (\_ => assertEq
    (encodePackageDeps exampleDepsExp)
    "\"1.2.3\".deps.a=\"=5.0.0\"\n\"1.2.3\".dev.b=\"=6.0.0\"\n\"1.2.4\".deps.a=\"=5.1.0\"\n\"1.2.4\".dev.b=\"=6.1.0\""
  )

toPackageDepTest : Test
toPackageDepTest =
  test "fromPackage" (\_ => assertEq
    (fromPackage examplePackage)
    (MkPackageDep
      [
        (["MyDep"], (
          AND
            (GTE $ MkVersion 1 2 3 Nothing Nothing)
            (LT $ MkVersion 2 0 0 Nothing Nothing)
        ))
      ]
      [
        (["MyDevDep"], (
          EQ (MkVersion 2 0 0 Nothing Nothing)
        ))
      ]
    )
  )

exampleDep : (Version, PackageDep)
exampleDep =
  (
    (MkVersion 0 0 1 (Just "pre") Nothing),
    (
      MkPackageDep
        [
          (["MyDep"], (
            AND
              (GTE $ MkVersion 1 2 3 Nothing Nothing)
              (LT $ MkVersion 2 0 0 Nothing Nothing)
          ))
        ]
        [
          (["MyDevDep"], (
            EQ (MkVersion 2 0 0 Nothing Nothing)
          ))
        ]
    )
  )

updatePackageDepNewTest : Test
updatePackageDepNewTest =
  test "updatePackageDep New Dep" (\_ => assertEq
    (
      updatePackageDep
        exampleDepsExp
        examplePackage
    )
    (snoc exampleDepsExp exampleDep)
  )

updatePackageDepExistingTest : Test
updatePackageDepExistingTest =
  test "updatePackageDep Existing Dep" (\_ => assertEq
    (
      updatePackageDep
        exampleDepsExpExt
        examplePackage
    )
    [ ((MkVersion 1 2 3 Nothing Nothing), (
        MkPackageDep [] []
      ))
    , ((MkVersion 0 0 1 (Just "pre") Nothing), (
        MkPackageDep
        [
          (["MyDep"], (
            AND
              (GTE $ MkVersion 1 2 3 Nothing Nothing)
              (LT $ MkVersion 2 0 0 Nothing Nothing)
          ))
        ]
        [
          (["MyDevDep"], (
            EQ (MkVersion 2 0 0 Nothing Nothing)
          ))
        ]
      ))
    , ((MkVersion 1 2 4 Nothing Nothing), (
        MkPackageDep [] []
      ))
    ]
  )

export
suite : Test
suite =
  describe "PackageDeps"
    [ test "Parse Deps" (\_ => assertEq
        (parsePackageDeps exampleDepsToml)
        (Right exampleDepsExp)
      )
    , toTomlTest
    , encodePackageDepsTest
    , toPackageDepTest
    , updatePackageDepNewTest
    , updatePackageDepExistingTest
    ]

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Example.Inject

import Data.Fun
import Data.Vect

import Flexidisc

record Person where
  constructor MkPerson
  firstname, lastname: String
  age : Nat

relaxPerson : Person -> Record String ["firstname" ::: String, "lastname" ::: String, "age" ::: Nat]
relaxPerson = toRecord ["firstname" ~~ firstname, "lastname" ~~ lastname, "age" ~~ age]

freezePerson : Record String ["firstname" ::: String, "lastname" ::: String, "age" ::: Nat] -> Person
freezePerson r = fromRecord MkPerson ["firstname", "lastname", "age"] r

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
import Data.Vect

search : String -> Vect m String -> List String
search pat [] = []
search pat (x :: xs) = if isInfixOf pat x then x :: search pat xs
                       else search pat xs


text:
module Main

import Control.ST
import Control.ST.ImplicitCall

data Access = LoggedOut | LoggedIn
data LoginResult = OK | BadPassword

interface DataStore (m : Type -> Type) where
  Store : Access -> Type
  connect : ST m Var [add (Store LoggedOut)]
  disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
  readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
  login : (store : Var) ->
          ST m LoginResult [store ::: Store LoggedOut :->
                             (\res => Store (case res of
                                                  OK => LoggedIn
                                                  BadPassword => LoggedOut))]
  logout : (store : Var) -> ST m () [tore ::: Store LoggedIn :-> Store LoggedOut]

getData : (ConsoleIO m, DataStore m) =>
          (failcount : Var)-> ST m () [failcount ::: State Integer]
getData failcount
        = do st <- connect
             OK <- login st
                | BadPassword => do putStrLn "Failure"
                                    fc <- read failcount
                                    write failcount (fc + 1)
                                    putStrLn ("Number of failures:" ++ show (fc + 1))
                                    disconnect st
                                    getData failcount
             secret <- readSecret st
             putStrLn ("Secret is: " ++ show secret)
             logout st
             disconnect st
             getData failcount

implementation DataStore IO where
  Store x = State String
  connect = new "Seret Data"
  disconnect store = delete store
  readSecret store = read store
  login store = do putStr "Enter password: "
                   p <- getStr
                   if p == "p123"
                      then pure OK
                      else pure BadPassword
  logout store = pure ()

main : IO ()
main = run (do fc <- new 0
               getData fc
               delete fc)

max_stars_repo_name: aztecrex/try-idris

max_issues_repo_name: aztecrex/try-idris

max_forks_repo_name: aztecrex/try-idris