text:
module Text.Parser.Core

import Data.Bool.Extra
import Data.List
import public Control.Delayed
import public Text.Bounded

%default total

-- TODO: Add some primitives for helping with error messages.
-- e.g. perhaps set a string to state what we're currently trying to
-- parse, or to say what the next expected token is in words

||| Description of a language's grammar. The `tok` parameter is the type
||| of tokens, and the `consumes` flag is True if the language is guaranteed
||| to be non-empty - that is, successfully parsing the language is guaranteed
||| to consume some input.
export
data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where
     Empty : (val : ty) -> Grammar tok False ty
     Terminal : String -> (WithBounds tok -> Maybe a) -> Grammar tok True a
     NextIs : String -> (WithBounds tok -> Bool) -> Grammar tok False tok
     EOF : Grammar tok False ()

     Fail : Bool -> String -> Grammar tok c ty
     Commit : Grammar tok False ()
     MustWork : Grammar tok c a -> Grammar tok c a

     SeqEat : {c2 : Bool} ->
              Grammar tok True a -> Inf (a -> Grammar tok c2 b) ->
              Grammar tok True b
     SeqEmpty : {c1, c2 : Bool} ->
                Grammar tok c1 a -> (a -> Grammar tok c2 b) ->
                Grammar tok (c1 || c2) b
     Alt : {c1, c2 : Bool} ->
           Grammar tok c1 ty -> Lazy (Grammar tok c2 ty) ->
           Grammar tok (c1 && c2) ty
     Bounds : Grammar tok c ty -> Grammar tok c (WithBounds ty)

||| Sequence two grammars. If either consumes some input, the sequence is
||| guaranteed to consume some input. If the first one consumes input, the
||| second is allowed to be recursive (because it means some input has been
||| consumed and therefore the input is smaller)
export %inline
(>>=) : {c1, c2 : Bool} ->
        Grammar tok c1 a ->
        inf c1 (a -> Grammar tok c2 b) ->
        Grammar tok (c1 || c2) b
(>>=) {c1 = False} = SeqEmpty
(>>=) {c1 = True}  = SeqEat

||| Sequence two grammars. If either consumes some input, the sequence is
||| guaranteed to consume input. This is an explicitly non-infinite version
||| of `>>=`.
export %inline
seq : {c1,c2 : Bool} ->
      Grammar tok c1 a ->
      (a -> Grammar tok c2 b) ->
      Grammar tok (c1 || c2) b
seq = SeqEmpty

||| Sequence a grammar followed by the grammar it returns.
export %inline
join : {c1,c2 : Bool} ->
       Grammar tok c1 (Grammar tok c2 a) ->
       Grammar tok (c1 || c2) a
join {c1 = False} p = SeqEmpty p id
join {c1 = True} p = SeqEat p id

||| Give two alternative grammars. If both consume, the combination is
||| guaranteed to consume.
export %inline
(<|>) : {c1,c2 : Bool} ->
        Grammar tok c1 ty ->
        Lazy (Grammar tok c2 ty) ->
        Grammar tok (c1 && c2) ty
(<|>) = Alt

||| Allows the result of a grammar to be mapped to a different value.
export
{c : _} ->
Functor (Grammar tok c) where
  map f (Empty val)  = Empty (f val)
  map f (Fail fatal msg) = Fail fatal msg
  map f (MustWork g) = MustWork (map f g)
  map f (Terminal msg g) = Terminal msg (map f . g)
  map f (Alt x y)    = Alt (map f x) (map f y)
  map f (SeqEat act next)
      = SeqEat act (\val => map f (next val))
  map f (SeqEmpty act next)
      = SeqEmpty act (\val => map f (next val))
  map {c} f (Bounds act) = rewrite sym $ orFalseNeutral c in SeqEmpty (Bounds act) (Empty . f) -- Bounds (map f act)
  -- The remaining constructors (NextIs, EOF, Commit) have a fixed type,
  -- so a sequence must be used.
  map {c = False} f p = SeqEmpty p (Empty . f)

||| Sequence a grammar with value type `a -> b` and a grammar
||| with value type `a`. If both succeed, apply the function
||| from the first grammar to the value from the second grammar.
||| Guaranteed to consume if either grammar consumes.
export %inline
(<*>) : {c1, c2 : Bool} ->
        Grammar tok c1 (a -> b) ->
        Grammar tok c2 a ->
        Grammar tok (c1 || c2) b
(<*>) x y = SeqEmpty x (\f => map f y)

||| Sequence two grammars. If both succeed, use the value of the first one.
||| Guaranteed to consume if either grammar consumes.
export %inline
(<*) : {c1,c2 : Bool} ->
       Grammar tok c1 a ->
       Grammar tok c2 b ->
       Grammar tok (c1 || c2) a
(<*) x y = map const x <*> y

||| Sequence two grammars. If both succeed, use the value of the second one.
||| Guaranteed to consume if either grammar consumes.
export %inline
(*>) : {c1,c2 : Bool} ->
       Grammar tok c1 a ->
       Grammar tok c2 b ->
       Grammar tok (c1 || c2) b
(*>) x y = map (const id) x <*> y

||| Produce a grammar that can parse a different type of token by providing a
||| function converting the new token type into the original one.
export
mapToken : (a -> b) -> Grammar b c ty -> Grammar a c ty
mapToken f (Empty val) = Empty val
mapToken f (Terminal msg g) = Terminal msg (g . map f)
mapToken f (NextIs msg g) = SeqEmpty (NextIs msg (g . map f)) (Empty . f)
mapToken f EOF = EOF
mapToken f (Fail fatal msg) = Fail fatal msg
mapToken f (MustWork g) = MustWork (mapToken f g)
mapToken f Commit = Commit
mapToken f (SeqEat act next) = SeqEat (mapToken f act) (\x => mapToken f (next x))
mapToken f (SeqEmpty act next) = SeqEmpty (mapToken f act) (\x => mapToken f (next x))
mapToken f (Alt x y) = Alt (mapToken f x) (mapToken f y)
mapToken f (Bounds act) = Bounds (mapToken f act)

||| Always succeed with the given value.
export %inline
pure : (val : ty) -> Grammar tok False ty
pure = Empty

||| Check whether the next token satisfies a predicate
export %inline
nextIs : String -> (WithBounds tok -> Bool) -> Grammar tok False tok
nextIs = NextIs

||| Look at the next token in the input
export %inline
peek : Grammar tok False tok
peek = nextIs "Unrecognised token" (const True)

||| Succeeds if running the predicate on the next token returns Just x,
||| returning x. Otherwise fails.
export %inline
terminal : String -> (WithBounds tok -> Maybe a) -> Grammar tok True a
terminal = Terminal

||| Always fail with a message
export %inline
fail : String -> Grammar tok c ty
fail = Fail False

export %inline
fatalError : String -> Grammar tok c ty
fatalError = Fail True

||| Succeed if the input is empty
export %inline
eof : Grammar tok False ()
eof = EOF

||| Commit to an alternative; if the current branch of an alternative
||| fails to parse, no more branches will be tried
export %inline
commit : Grammar tok False ()
commit = Commit

||| If the parser fails, treat it as a fatal error
export %inline
mustWork : {c : Bool} -> Grammar tok c ty -> Grammar tok c ty
mustWork = MustWork

export %inline
bounds : Grammar tok c ty -> Grammar tok c (WithBounds ty)
bounds = Bounds

data ParseResult : Type -> Type -> Type where
     Failure : (committed : Bool) -> (fatal : Bool) ->
               (err : String) -> (rest : List (WithBounds tok)) -> ParseResult tok ty
     Res : (committed : Bool) ->
           (val : WithBounds ty) -> (more : List (WithBounds tok)) -> ParseResult tok ty

mutual
  doParse : (commit : Bool) ->
            (act : Grammar tok c ty) ->
            (xs : List (WithBounds tok)) ->
            ParseResult tok ty
  doParse com (Empty val) xs = Res com (irrelevantBounds val) xs
  doParse com (Fail fatal str) xs = Failure com fatal str xs
  doParse com Commit xs = Res True (irrelevantBounds ()) xs
  doParse com (MustWork g) xs =
    case assert_total (doParse com g xs) of
         Failure com' _ msg ts => Failure com' True msg ts
         res => res
  doParse com (Terminal err f) [] = Failure com False "End of input" []
  doParse com (Terminal err f) (x :: xs) =
    case f x of
         Nothing => Failure com False err (x :: xs)
         Just a => Res com (const a <$> x) xs
  doParse com EOF [] = Res com (irrelevantBounds ()) []
  doParse com EOF (x :: xs) = Failure com False "Expected end of input" (x :: xs)
  doParse com (NextIs err f) [] = Failure com False "End of input" []
  doParse com (NextIs err f) (x :: xs)
        = if f x
             then Res com x (x :: xs)
             else Failure com False err (x :: xs)
  doParse com (Alt {c1} {c2} x y) xs
      = case doParse False x xs of
             Failure com' fatal msg ts
                => if com' || fatal
                          -- If the alternative had committed, don't try the
                          -- other branch (and reset commit flag)
                     then Failure com fatal msg ts
                     else assert_total (doParse False y xs)
-- Successfully parsed the first option, so use the outer commit flag
             Res _ val xs => Res com val xs
  doParse com (SeqEmpty act next) xs
      = case assert_total (doParse com act xs) of
             Failure com fatal msg ts => Failure com fatal msg ts
             Res com v xs =>
               case assert_total (doParse com (next v.val) xs) of
                    Failure com' fatal msg ts => Failure com' fatal msg ts
                    Res com' v' xs => Res com' (mergeBounds v v') xs
  doParse com (SeqEat act next) xs
      = case assert_total (doParse com act xs) of
             Failure com fatal msg ts => Failure com fatal msg ts
             Res com v xs =>
                   case assert_total (doParse com (next v.val) xs) of
                        Failure com' fatal msg ts => Failure com' fatal msg ts
                        Res com' v' xs => Res com' (mergeBounds v v') xs
  doParse com (Bounds act) xs
      = case assert_total (doParse com act xs) of
             Failure com fatal msg ts => Failure com fatal msg ts
             Res com v xs => Res com (const v <$> v) xs

public export
data ParsingError tok = Error String (List (WithBounds tok))

||| Parse a list of tokens according to the given grammar. If successful,
||| returns a pair of the parse result and the unparsed tokens (the remaining
||| input).
export
parse : {c : Bool} -> (act : Grammar tok c ty) -> (xs : List (WithBounds tok)) ->
        Either (ParsingError tok) (ty, List (WithBounds tok))
parse act xs
    = case doParse False act xs of
           Failure _ _ msg ts => Left (Error msg ts)
           Res _ v rest => Right (v.val, rest)


text:
main : IO ()
main = putStrLn ?something

ext: idr


text:
module Network.TLS.AEAD

import Data.Stream
import Data.Bits
import Data.Vect
import Data.List
import Utils.Misc
import Utils.Bytes
import Crypto.AES.Big
import Crypto.AES.Common
import Crypto.Hash
import Crypto.Hash.GHash
import Crypto.Hash.Poly1305
import Crypto.ChaCha

public export
interface AEAD (0 a : Type) where
  ||| IV generated during key exchange
  fixed_iv_length : Nat
  enc_key_length : Nat
  mac_length : Nat
  mac_key_length : Nat
  ||| Part of IV that is sent along with the ciphertext, should always be 0 in TLS 1.3
  record_iv_length : Nat

  encrypt : Vect enc_key_length Bits8 -> Vect fixed_iv_length Bits8 -> Vect mac_key_length Bits8 -> Nat ->
            (plaintext : List Bits8) -> (aad : List Bits8) -> (Vect record_iv_length Bits8, List Bits8, Vect mac_length Bits8)
  decrypt : Vect enc_key_length Bits8 -> Vect fixed_iv_length Bits8 -> Vect record_iv_length Bits8 -> Vect mac_key_length Bits8 -> Nat ->
            (ciphertext : List Bits8) -> (plaintext_to_aad : List Bits8 -> List Bits8) -> (mac_tag : List Bits8) -> (List Bits8, Bool)

aes_pad_iv_block : {iv : Nat} -> Vect iv Bits8 -> Stream (Vect (iv+4) Bits8)
aes_pad_iv_block iv = map ((iv ++) . to_be . (cast {to=Bits32})) $ drop 2 nats

aes_keystream : (mode : Mode) -> Vect ((get_n_k mode) * 4) Bits8 -> Vect 12 Bits8 -> Stream Bits8
aes_keystream mode key iv =
  stream_concat $ map (toList . encrypt_block mode key) (aes_pad_iv_block iv)

aes_gcm_create_aad : (mode : Mode) -> Vect ((get_n_k mode) * 4) Bits8 -> Vect 12 Bits8 -> List Bits8 -> List Bits8 -> Vect 16 Bits8
aes_gcm_create_aad mode key iv aad ciphertext =
  let a = toList $ to_be {n=8} $ cast {to=Bits64} $ 8 * (length aad)
      c = toList $ to_be {n=8} $ cast {to=Bits64} $ 8 * (length ciphertext)
      input = pad_zero 16 aad <+> pad_zero 16 ciphertext <+> a <+> c
      h = encrypt_block mode key (replicate _ 0)
      output = mac GHash h input
      j0 = encrypt_block mode key (iv ++ (to_be $ the Bits32 1))
  in zipWith xor j0 output

public export
data TLS13_AES_128_GCM : Type where

public export
AEAD TLS13_AES_128_GCM where
  fixed_iv_length = 12
  enc_key_length = 16
  mac_length = 16
  mac_key_length = 0
  record_iv_length = 0

  encrypt key iv mac_key seq_no plaintext aad =
    let iv' = zipWith xor iv $ integer_to_be _ $ natToInteger seq_no
        ciphertext = zipWith xor plaintext (toList $ Stream.take (length plaintext) $ aes_keystream AES128 key iv')
        mac_tag = aes_gcm_create_aad AES128 key iv' aad ciphertext
    in ([], ciphertext, mac_tag)

  decrypt key iv [] mac_key seq_no ciphertext aadf mac_tag' =
    let iv' = zipWith xor iv $ integer_to_be _ $ natToInteger seq_no
        plaintext = zipWith xor ciphertext (toList $ Stream.take (length ciphertext) $ aes_keystream AES128 key iv')
        mac_tag = aes_gcm_create_aad AES128 key iv' (aadf plaintext) ciphertext
    in (plaintext, s_eq' (toList mac_tag) mac_tag')

public export
data TLS12_AES_128_GCM : Type where

public export
AEAD TLS12_AES_128_GCM where
  fixed_iv_length = 4
  enc_key_length = 16
  mac_length = 16
  mac_key_length = 0
  record_iv_length = 8

  encrypt key iv mac_key seq_no plaintext aad =
    let explicit_iv = to_be {n=8} $ cast {to=Bits64} seq_no
        iv' = iv ++ explicit_iv
        ciphertext = zipWith xor plaintext (toList $ Stream.take (length plaintext) $ aes_keystream AES128 key iv')
        mac_tag = aes_gcm_create_aad AES128 key iv' aad ciphertext
    in (explicit_iv, ciphertext, mac_tag)

  decrypt key iv explicit_iv mac_key seq_no ciphertext aadf mac_tag' =
    let iv' = iv ++ explicit_iv
        plaintext = zipWith xor ciphertext (toList $ Stream.take (length ciphertext) $ aes_keystream AES128 key iv')
        mac_tag = aes_gcm_create_aad AES128 key iv' (aadf plaintext) ciphertext
    in (plaintext, s_eq' (toList mac_tag) mac_tag')

public export
data TLS13_AES_256_GCM : Type where

public export
AEAD TLS13_AES_256_GCM where
  fixed_iv_length = 12
  enc_key_length = 32
  mac_length = 16
  mac_key_length = 0
  record_iv_length = 0

  encrypt key iv mac_key seq_no plaintext aad =
    let iv' = zipWith xor iv $ integer_to_be _ $ natToInteger seq_no
        ciphertext = zipWith xor plaintext (toList $ Stream.take (length plaintext) $ aes_keystream AES256 key iv')
        mac_tag = aes_gcm_create_aad AES256 key iv' aad ciphertext
    in ([], ciphertext, mac_tag)

  decrypt key iv [] mac_key seq_no ciphertext aadf mac_tag' =
    let iv' = zipWith xor iv $ integer_to_be _ $ natToInteger seq_no
        plaintext = zipWith xor ciphertext (toList $ Stream.take (length ciphertext) $ aes_keystream AES256 key iv')
        mac_tag = aes_gcm_create_aad AES256 key iv' (aadf plaintext) ciphertext
    in (plaintext, s_eq' (toList mac_tag) mac_tag')

public export
data TLS12_AES_256_GCM : Type where

public export
AEAD TLS12_AES_256_GCM where
  fixed_iv_length = 4
  enc_key_length = 32
  mac_length = 16
  mac_key_length = 0
  record_iv_length = 8

  encrypt key iv mac_key seq_no plaintext aad =
    let explicit_iv = to_be {n=8} $ cast {to=Bits64} seq_no
        iv' = iv ++ explicit_iv
        ciphertext = zipWith xor plaintext (toList $ Stream.take (length plaintext) $ aes_keystream AES256 key iv')
        mac_tag = aes_gcm_create_aad AES256 key iv' aad ciphertext
    in (explicit_iv, ciphertext, mac_tag)

  decrypt key iv explicit_iv mac_key seq_no ciphertext aadf mac_tag' =
    let iv' = iv ++ explicit_iv
        plaintext = zipWith xor ciphertext (toList $ Stream.take (length ciphertext) $ aes_keystream AES256 key iv')
        mac_tag = aes_gcm_create_aad AES256 key iv' (aadf plaintext) ciphertext
    in (plaintext, s_eq' (toList mac_tag) mac_tag')

chacha_create_aad : Vect 64 Bits8 -> List Bits8 -> List Bits8 -> Vect 16 Bits8
chacha_create_aad polykey aad ciphertext =
  let key = take 32 polykey
      length_aad = toList $ to_le {n=8} $ cast {to=Bits64} $ length aad
      length_ciphertext = toList $ to_le {n=8} $ cast {to=Bits64} $ length ciphertext
      input = pad_zero 16 aad ++ pad_zero 16 ciphertext ++ length_aad ++ length_ciphertext
  in mac Poly1305 key input

public export
data TLS1213_ChaCha20_Poly1305 : Type where

public export
AEAD TLS1213_ChaCha20_Poly1305 where
  fixed_iv_length = 12
  enc_key_length = 32
  mac_length = 16
  mac_key_length = 0
  record_iv_length = 0

  encrypt key iv [] seq_no plaintext aad =
    let k' = from_le {n=4} <$> group 8 4 key
        iv' = zipWith xor iv $ integer_to_be _ $ natToInteger seq_no
        i' = from_le {n=4} <$> group 3 4 iv'
        (polykey :: keystream) = map (\c => chacha_rfc8439_block 10 (cast c) k' i') nats
        ciphertext = zipWith xor plaintext (toList $ Stream.take (length plaintext) $ stream_concat keystream)
        auth_tag = chacha_create_aad polykey aad ciphertext
    in ([], ciphertext, auth_tag)

  decrypt key iv [] [] seq_no ciphertext aadf mac_tag' =
    let k' = from_le {n=4} <$> group 8 4 key
        iv' = zipWith xor iv $ integer_to_be _ $ natToInteger seq_no
        i' = from_le {n=4} <$> group 3 4 iv'
        (polykey :: keystream) = map (\c => chacha_rfc8439_block 10 (cast c) k' i') nats
        plaintext = zipWith xor ciphertext (toList $ Stream.take (length ciphertext) $ stream_concat keystream)
        auth_tag = chacha_create_aad polykey (aadf plaintext) ciphertext
    in (plaintext, toList auth_tag `s_eq'` mac_tag')


text:
module Main

%include C "hotp.h"
-- %link C "libhotp.a"
%link C "libhotp.dylib"

%access public export
-- %default total

namespace Operators
  infixl 8 .:
  infixr 9 >>>

  ||| Binary function composition.
  ||| @f an "outer" unary function.
  ||| @g an "inner" binary function.
  |||
  ||| ```idris
  ||| lemma : (f .: g) x y = f (g x y)
  ||| lemma = Refl
  ||| ```
  (.:) : (f : c -> d) -> (g : a -> b -> c) -> (x : a) -> (y : b) -> d
  (.:) = (.) . (.)

  ||| Left-to-right function composition.
  (>>>) : (a -> b) -> (b -> c) -> a -> c
  (>>>) = flip (.)

newline : String -> String
newline = (++ "\n")

namespace Experiment
  ||| Print `2 + 2 = ` via Rust (via `FFI_C`).
  twoPlusTwoIs : IO ()
  twoPlusTwoIs = foreign FFI_C "two_plus_two_is" (IO ())

  ||| Add two to `x` via Rust FFI (via `FFI_C`).
  ||| @x an `Int` to add two to.
  addTwo : (x : Int) -> IO Int
  addTwo = foreign FFI_C "add_two" (Int -> IO Int)

namespace HMAC
  cons : (secret, input : String) -> String
  cons = unsafePerformIO .:
    foreign FFI_C "hmac_cons" (String -> String -> IO String)

namespace SHA256
  digest : String -> String
  digest = unsafePerformIO . foreign FFI_C "sha256_digest" (String -> IO String)

main : IO ()
main = repl "> " (digest >>> newline)
-- main = repl "> " (hmac_cons "secret" >>> newline)
-- main = digest "testing" >>= putStrLn
--      *> twoPlusTwoIs
--      *> addTwo 2 >>= printLn

max_stars_repo_name: yurrriq/idris-hotp

max_issues_repo_name: yurrriq/idris-hotp

max_forks_repo_name: yurrriq/idris-hotp


text:
module Web.Internal.ClipboardPrim

import JS
import Web.Internal.Types

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

namespace Clipboard

  export
  %foreign "browser:lambda:x=>x.read()"
  prim__read : Clipboard -> PrimIO (Promise (Array ClipboardItem))

  export
  %foreign "browser:lambda:x=>x.readText()"
  prim__readText : Clipboard -> PrimIO (Promise String)

  export
  %foreign "browser:lambda:(x,a)=>x.write(a)"
  prim__write : Clipboard -> Array ClipboardItem -> PrimIO (Promise Undefined)

  export
  %foreign "browser:lambda:(x,a)=>x.writeText(a)"
  prim__writeText : Clipboard -> String -> PrimIO (Promise Undefined)

namespace ClipboardEvent

  export
  %foreign "browser:lambda:(a,b)=> new ClipboardEvent(a,b)"
  prim__new : String -> UndefOr ClipboardEventInit -> PrimIO ClipboardEvent

  export
  %foreign "browser:lambda:x=>x.clipboardData"
  prim__clipboardData : ClipboardEvent -> PrimIO (Nullable DataTransfer)

namespace ClipboardItem

  export
  %foreign "browser:lambda:(a,b)=> new ClipboardItem(a,b)"
  prim__new :  Record String (Promise (Union2 String Blob))
            -> UndefOr ClipboardItemOptions
            -> PrimIO ClipboardItem

  export
  %foreign "browser:lambda:(a,b)=>ClipboardItem.createDelayed(a,b)"
  prim__createDelayed :  Record String ClipboardItemDelayedCallback
                      -> UndefOr ClipboardItemOptions
                      -> PrimIO ClipboardItem

  export
  %foreign "browser:lambda:x=>x.delayed"
  prim__delayed : ClipboardItem -> PrimIO Boolean

  export
  %foreign "browser:lambda:x=>x.lastModified"
  prim__lastModified : ClipboardItem -> PrimIO JSInt64

  export
  %foreign "browser:lambda:x=>x.presentationStyle"
  prim__presentationStyle : ClipboardItem -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.types"
  prim__types : ClipboardItem -> PrimIO (Array String)

  export
  %foreign "browser:lambda:(x,a)=>x.getType(a)"
  prim__getType : ClipboardItem -> String -> PrimIO (Promise Blob)

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

namespace ClipboardEventInit

  export
  %foreign "browser:lambda:(a)=> {clipboardData: a}"
  prim__new : UndefOr (Nullable DataTransfer) -> PrimIO ClipboardEventInit

  export
  %foreign "browser:lambda:x=>x.clipboardData"
  prim__clipboardData :  ClipboardEventInit
                      -> PrimIO (UndefOr (Nullable DataTransfer))

  export
  %foreign "browser:lambda:(x,v)=>{x.clipboardData = v}"
  prim__setClipboardData :  ClipboardEventInit
                         -> UndefOr (Nullable DataTransfer)
                         -> PrimIO ()

namespace ClipboardItemOptions

  export
  %foreign "browser:lambda:(a)=> {presentationStyle: a}"
  prim__new : UndefOr String -> PrimIO ClipboardItemOptions

  export
  %foreign "browser:lambda:x=>x.presentationStyle"
  prim__presentationStyle : ClipboardItemOptions -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.presentationStyle = v}"
  prim__setPresentationStyle :  ClipboardItemOptions
                             -> UndefOr String
                             -> PrimIO ()

namespace ClipboardPermissionDescriptor

  export
  %foreign "browser:lambda:(a)=> {allowWithoutGesture: a}"
  prim__new : UndefOr Boolean -> PrimIO ClipboardPermissionDescriptor

  export
  %foreign "browser:lambda:x=>x.allowWithoutGesture"
  prim__allowWithoutGesture :  ClipboardPermissionDescriptor
                            -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.allowWithoutGesture = v}"
  prim__setAllowWithoutGesture :  ClipboardPermissionDescriptor
                               -> UndefOr Boolean
                               -> PrimIO ()

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

namespace ClipboardItemDelayedCallback

  export
  %foreign "browser:lambda:x=>()=>x()()"
  prim__toClipboardItemDelayedCallback :  (() -> IO (Promise (Union2 String
                                                                     Blob)))
                                       -> PrimIO ClipboardItemDelayedCallback


text:
module Control.Monad.Dom

import public Control.Monad.Dom.DomIO
import public Control.Monad.Dom.Event
import public Control.Monad.Dom.Interface


text:
module Libgit

import Prelude
import System.FFI

import public Libgit.Clone
import Libgit.FFI
import public Libgit.Git
import public Libgit.Remote
import public Libgit.Repository
import public Libgit.Object
import public Libgit.Oid
import public Libgit.Types

max_forks_repo_name: bigs/libgit-idris


text:
||| Drawing a Sierpinski triangle
||| Ported from https://www.linuxjournal.com/content/getting-started-ncurses

module Sierpinski

import Data.Fin
import Data.Nat
import Data.Vect
import Data.String
import NCurses
import System.Random

%default total

main : IO ()
main = runNCurses $ NCurses.do
  -- Initialise curses
  cBreak
  noEcho
  clear
  setCursorVisibility CInvisible

  -- Initialise triangle
  size <- getSize
  let maxlines = pred size.height
  let maxcols = pred size.width

  let p0 = MkPosition { row = 0, col = 0 }
  let p1 = MkPosition { row = maxlines, col = half maxcols }
  let p2 = MkPosition { row = 0, col = maxcols }
  let ps : Vect 3 ? = [p0,p1,p2]
  for_ @{NCURSES} Fin.range $ \ k => do
    let char = assert_total (show k `strIndex` 0)
    mvAddCh (index k ps) char

  -- Initialise position with random values
  let p = MkPosition { row = !(lift $ randNat maxlines)
                     , col = !(lift $ randNat maxcols) }
  -- Iterate the triangle
  loop ps 200000 p
  -- Done
  mvPrint (MkRow maxlines) "Press any key to quit"
  refresh
  ignore $ getCh

  where

    half : Nat -> Nat
    half n = (n `divNatNZ` 2) %search

    -- The bound better be smaller than MAX_INT32
    randNat : Nat -> IO Nat
    randNat bnd = do let i : Int32 = !randomIO
                     pure $ cast (abs i `mod` cast bnd)

    randIndex : (n : Nat) -> {auto 0 _ : NonZero n} -> IO (Fin n)
    randIndex (S n) = do k <- randNat (S n)
                         pure (restrict n $ cast k)

    loop : Vect 3 Position -> Nat -> Position ->
           NCurses Config.init Config.init ()
    loop ps Z     pi = pure ()
    loop ps (S n) pi = do
      k <- lift $ randIndex 3
      let pk = index k ps
      let pi' = { row $= \ xi => half (xi + pk.row)
                , col $= \ yi => half (yi + pk.col)
                } pi
      mvAddCh pi' '*'
      refresh
      loop ps n pi'

max_stars_repo_name: gallais/ncurses-idris

max_issues_repo_name: gallais/ncurses-idris

max_forks_repo_name: gallais/ncurses-idris


text:
module Linear

import public Linear.Optics
import public Linear.V
import public Linear.Math


text:
module India.Language.Core.Parser

import Data.Bool

import Text.Lexer
import Text.Parser

import India.Language.Core.Lexer
import India.Language.Core.Types
import India.Union

export
isToken : Eq t => t -> Member t ts => IndianToken ts -> Bool
isToken x (MkToken line col (Tok kind text))
  = maybe False (x ==) $ prj kind

export
matchWithData : Eq t =>
                TokenKind t =>
                Member t ts =>
                (k : t) -> Grammar (IndianToken ts) True (TokenData (TokType k))
matchWithData k = terminal "Unexpected token" \(MkToken l c (Tok  uk v)) => do
  k' <- prj uk
  guard (k == k')
  pure $ MkToken l c $ tokValue k v

export
indianParser : TokenMap $ Token $ Union Prelude.id ts ->
               Grammar (IndianToken ts) True a ->
               String -> Either String a
indianParser lexer parser str =
  let (tokens, (_,_,"")) = lex lexer str
        | (_, (_,_,remains)) => Left $ "Cannot lex content: " ++ remains
      (Right (res, [])) = parse parser tokens
        | Right (_,remains)  => Left $ "Can't parse content, left: " ++ show (map (text . tok) remains)
        | Left (Error err _) => Left $ "Can't parse content: " ++ err
        in Right res

export
wordParser : IndianCore TokenData indian =>
             Member Lexer.Word ts =>
             Grammar (IndianToken ts) True (indian Content)
wordParser = map content $ matchWithData W

export
spaceParser : IndianCore TokenData indian =>
              Member Lexer.Space ts =>
              Grammar (IndianToken ts) True (indian Content)
spaceParser =  map (content . record {tok = " "}) $ matchWithData SP <* many (matchWithData SP)

export
newlineParser : IndianCore TokenData indian =>
                Member Newline ts =>
                Grammar (IndianToken ts) True (indian Content)
newlineParser = map (content . record {tok = "\n"}) $ matchWithData NL

export
asParagraph : {cond : Bool} ->
              (builder : b -> d) ->
              (start : Grammar (IndianToken ts) cond a) ->
              (main : Grammar (IndianToken ts) True b) ->
              (end: List  (Grammar (IndianToken ts) True c)) ->
              Grammar (IndianToken ts) True d
asParagraph builder start main end = rewrite sym (orTrueTrue cond)
  in map builder $ start *> (main <* many (choice end))

export
paragraphParser : IndianCore TokenData indian =>
                  (en : Member Space ts) =>
                  (parts : List (Grammar (IndianToken ts) True (indian Content))) ->
                  (end: List  (Grammar (IndianToken ts) True (indian Content))) ->
                  Grammar (IndianToken ts) True (indian Paragraph)
paragraphParser = asParagraph paragraph (optional $ spaceParser {indian}) . some . choice

export
simpleParser : IndianCore TokenData indian =>
               String -> Either String (indian Paragraph)
simpleParser = indianParser coreLexer $
  paragraphParser [wordParser, spaceParser] [newlineParser]

max_stars_repo_name: berewt/india

max_issues_repo_name: berewt/india

max_forks_repo_name: berewt/india


text:
||| TODO : This was interduced after v0.5.1. After the next minor release,
|||        this can be removed and the instances from `base` can be used.
module Libraries.Data.Primitives

import public Decidable.Equality.Core as Decidable.Equality

%default total

public export
[FromEq] Eq a => DecEq a where
    decEq x y = case x == y of -- Blocks if x or y not concrete
                     True => Yes primitiveEq
                     False => No primitiveNotEq
       where primitiveEq : forall x, y . x = y
             primitiveEq = believe_me (Refl {x})
             primitiveNotEq : forall x, y . Not (x = y)
             primitiveNotEq prf = believe_me {b = Void} ()

--------------------------------------------------------------------------------
-- Bits8
--------------------------------------------------------------------------------

public export
[TempB8] DecEq Bits8 where
    decEq = decEq @{FromEq}

--------------------------------------------------------------------------------
-- Bits16
--------------------------------------------------------------------------------

public export
[TempB16] DecEq Bits16 where
    decEq = decEq @{FromEq}

--------------------------------------------------------------------------------
-- Bits32
--------------------------------------------------------------------------------

public export
[TempB32] DecEq Bits32 where
    decEq = decEq @{FromEq}

--------------------------------------------------------------------------------
-- Bits64
--------------------------------------------------------------------------------

public export
[TempB64] DecEq Bits64 where
    decEq = decEq @{FromEq}

--------------------------------------------------------------------------------
-- Int8
--------------------------------------------------------------------------------

public export
[TempI8] DecEq Int8 where
    decEq = decEq @{FromEq}

--------------------------------------------------------------------------------
-- Int16
--------------------------------------------------------------------------------

public export
[TempI16] DecEq Int16 where
    decEq = decEq @{FromEq}

--------------------------------------------------------------------------------
-- Int32
--------------------------------------------------------------------------------

public export
[TempI32] DecEq Int32 where
    decEq = decEq @{FromEq}

--------------------------------------------------------------------------------
-- Int64
--------------------------------------------------------------------------------

public export
[TempI64] DecEq Int64 where
    decEq = decEq @{FromEq}


text:
module TypedContainers.In

import Data.List
import Data.List.Elem
import Data.DPair

%default total

lemma0 : ([x] = [y]) -> (x = y)
lemma0 Refl = Refl

lemma1 : {0 xs : List a} -> {0 ys : List a} -> ((x :: xs) = (y :: ys)) -> (xs = ys)
lemma1 Refl = Refl

lemma2 : {0 xs : List a} -> {0 ys : List a} -> ((x :: xs) = (y :: ys)) -> (x = y)
lemma2 Refl = Refl

public export
data In : (a -> Bool) -> List a -> Type where
  MkIn : (x : a) -> (f x = True) -> (xs : List a) -> In f (x :: xs)
  MkInCons : (x : a) -> (0 xs : List a) -> In f xs -> In f (x :: xs)

public export
inFilter : (f : a -> Bool) -> (g : a -> Bool) -> ((x : a) -> (g x = True) -> f x = True) -> (l : List a) -> In g l -> In g (filter f l)
inFilter f g p1 [] p2 impossible
inFilter f g p1 (x :: xs) (MkIn x p2 xs) =
  let p3 = p1 x p2 in
  rewrite p3 in MkIn x p2 (filter f xs) {f = g}
inFilter f g p1 (x :: xs) (MkInCons x xs p2) =
  let r = inFilter f g p1 xs p2 in
  let MkDPair p2 p3 : DPair Bool (f x ===) = MkDPair (f x) Refl in
  case p2 of
    True => rewrite p3 in MkInCons x (filter f xs) r
    False => rewrite p3 in r

fromFilter : {f : a -> Bool} -> {l : List a} -> {lEq : l' === filter f l} -> Elem x l' -> (f x = True)
fromFilter (Here {x, xs}) = case l of
  [] impossible
  y :: ys =>
    let (MkDPair p0 p1) : DPair Bool ((f y) ===) = MkDPair (f y) Refl in
    case p0 of
      True =>
        let p2 : (y :: filter f ys = filter f (y :: ys)) = rewrite p1 in Refl in
        let p3 : (x :: xs = y :: filter f ys) = rewrite p2 in lEq in
        let p4 = lemma2 p3 in
        rewrite p4 in p1
      False =>
        let p2 : (filter f ys = filter f (y :: ys)) = rewrite p1 in Refl in
        let p3 : (x :: xs = filter f ys) = rewrite p2 in lEq in
        fromFilter {f, l = ys, lEq = p3} (Here {x, xs})
fromFilter (There p {x, y, xs}) =
  case l of
    [] impossible
    z :: zs =>
      let (MkDPair p0 p1) : DPair Bool ((f z) ===) = MkDPair (f z) Refl in
      case p0 of
        True =>
          let p2 : (z :: filter f zs = filter f (z :: zs)) = rewrite p1 in Refl in
          let p3 : (y :: xs = z :: filter f zs) = rewrite p2 in lEq in
          let p4 = lemma1 p3 in
          fromFilter {f, lEq = p4} p
        False =>
          let p2 : (filter f zs = filter f (z :: zs)) = rewrite p1 in Refl in
          let p3 : (y :: xs = filter f zs) = rewrite p2 in lEq in
          fromFilter {f, lEq = p3} (There p {x, y, xs})

extractIn' : {f : a -> Bool} -> {g : a -> Bool} -> {l : List a} -> {l' : List a} -> {lEq : l' = filter g l} -> In f l' -> DPair a (\x => (f x = True, g x = True))
extractIn' (MkIn x p0 xs) =
  let p1 = Here {x, xs} in
  let p2 = fromFilter {f = g, l, l' = x :: xs, lEq} p1 in
  MkDPair x (p0, p2)
extractIn' (MkInCons x xs rec) =
  case l of
    [] impossible
    y :: ys =>
      let (MkDPair p2 p3) : DPair Bool ((g y) ===) = MkDPair (g y) Refl in
      case p2 of
        True =>
          let p4 : (y :: filter g ys = filter g (y :: ys)) = rewrite p3 in Refl in
          let p5 : (x :: xs = y :: filter g ys) = rewrite p4 in lEq in
          extractIn' {f, g, l = ys, l' = xs, lEq = lemma1 p5} rec
        False =>
          let p4 : (filter g ys = filter g (y :: ys)) = rewrite p3 in Refl in
          let p5 : (x :: xs = filter g ys) = rewrite p4 in lEq in
          extractIn' {f, g, l = ys, l' = x :: xs, lEq = p5} (MkInCons x xs rec)

public export
extractIn : {f : a -> Bool} -> {g : a -> Bool} -> {l : List a} -> In f (filter g l) -> DPair a (\x => (f x = True, g x = True))
extractIn = extractIn' {lEq = Refl}

outFilter' : {0 f : a -> Bool} -> {g : a -> Bool} -> (xxs : List a) -> (pl : yys = filter g xxs) -> In f yys -> In f xxs
outFilter' [] pl (MkIn _ _ _) impossible
outFilter' [] pl (MkInCons _ _ _) impossible
outFilter' (x :: xs) pl (MkIn y py ys) with (g x)
  outFilter' (x :: xs) pl (MkIn y py ys) | True =
    let pl' = lemma2 pl in
    let px : (f x = True) = rewrite sym pl' in py in
    MkIn x px xs
  outFilter' (x :: xs) pl (MkIn y py ys) | False = MkInCons x xs $ outFilter' {f, g} xs pl (MkIn {f} y py ys)
outFilter' (x :: xs) pl (MkInCons y ys py) with (g x)
  outFilter' (x :: xs) pl (MkInCons y ys py) | True = MkInCons x xs $ outFilter' {f, g} xs (lemma1 pl) py
  outFilter' (x :: xs) pl (MkInCons y ys py) | False = MkInCons x xs $ outFilter' {f, g} xs pl (MkInCons y ys py)

public export
outFilter : {g : a -> Bool} -> {l : List a} -> In f (filter g l) -> In f l
outFilter p = outFilter' {f, g} l Refl p

max_stars_repo_name: L-as/idris-rbtree

max_issues_repo_name: L-as/idris-rbtree

max_forks_repo_name: L-as/idris-rbtree


text:
module Chapter4
import Data.Vect

data Bool = False | True

-- Enumeration types.  Literally an enum from C.
{-
From wiki:
> An enumerated type can be seen as a degenerate case: a tagged union of unit
> types. It corresponds to a set of nullary constructors and may be implemented
> as a simple tag variable, since it holds no additional data besides the value
> of the tag.
-}
data Direction = North
               | East
               | South
               | West

turnClockwise : Direction -> Direction
turnClockwise North = East
turnClockwise East = South
turnClockwise South = West
turnClockwise West = North

-- Union types.  Why are they called union?  This is different
-- from a union in C.
-- From above, we see that this is basically a union of 'product types'.
{-
From wiki:
> The expression of an instance of a product type will be a tuple, and
> is called a "tuple type" of expression. A product of types is a direct
> product of two or more types.
In other words it is an union of structs (which it is).
-}
-- With documentation.  Note that we first have the | separator
-- and right after we have the ||| for documentation.
data Shape = ||| Triangle with base and height
             Triangle Double Double
           | ||| Rectangle with width and height
             Rectangle Double Double
           | ||| Circle with radius.
             Circle Double

area : Shape -> Double
area (Triangle base height) = (base * height) / 2
area (Rectangle width height) = width * height
area (Circle radius) = pi * radius * radius

data Shape2 : Type where
  -- need to use 2 suffix else we get a conflict with above.
  Triangle2 : Double -> Double -> Shape2
  Rectangle2 : Double -> Double -> Shape2
  Circle2 : Double -> Shape2

-- Recursive types
data MyNat = MyZ | MyS MyNat  -- Peano arithmetic <3

data Picture = Primitive Shape
             | Combine Picture Picture
             | Rotate Double Picture
             | Translate Double Double Picture

testPicture : Picture
testPicture = Combine
                (Translate 5 5 (Primitive (Rectangle 20 10)))
                (Combine (Translate 35 5 (Primitive (Circle 5)))
                         (Translate 15 25 (Primitive (Triangle 10 10))))

pictureArea : Picture -> Double
pictureArea (Primitive s) = area s
pictureArea (Combine p1 p2) = pictureArea p1 + pictureArea p2
pictureArea (Rotate r p) = pictureArea p  -- pictureArea ?h  will be autocompleted
pictureArea (Translate x y p) = pictureArea p

data Infinite = Forever Infinite  -- this typechecks though!  why?

-- Generic data types
-- These are "templates" in C++ world.  They don't exist in C land, except
-- for maybe arrays/pointers of type T.

data Biggest = NoTriangle | Size Double  -- really this is maybe.

biggestTriangle : Picture -> Biggest
-- would have been nice to introduce the @ syntax before.  I knew it from Haskell.
biggestTriangle (Primitive (t@(Triangle x y))) = Size (area t)
biggestTriangle (Primitive (Rectangle x y)) = NoTriangle
biggestTriangle (Primitive (Circle x)) = NoTriangle
-- Holly carp that is manual!
-- need to use >>=
biggestTriangle (Combine x y) = case biggestTriangle x of
                                     NoTriangle => case biggestY of
                                                        NoTriangle => NoTriangle
                                                        Size size2 => Size size2
                                     Size size => case biggestY of
                                                       NoTriangle => Size size
                                                       Size size2 => Size (max size size2)
                                where
                                    biggestY : Biggest
                                    biggestY = biggestTriangle y
biggestTriangle (Rotate r p) = biggestTriangle p
biggestTriangle (Translate x y p) = biggestTriangle p

--data Maybe type = Nothing | Just type

safeDivide : Double -> Double -> Maybe Double
safeDivide x y = if y /= 0 then Just (x / y)
                           else Nothing

data Tree elem = Empty
               | Node (Tree elem) elem (Tree elem)
%name Tree tree, tree1

insert : Ord a => a -> Tree a -> Tree a
insert x Empty = Node Empty x Empty
insert x orig@(Node left y right) = case compare x y of
                                    LT => Node (insert x left) y right
                                    EQ => orig  -- now we introduce @ patterns
                                    GT => Node left y (insert x right)

data BSTree : Type -> Type where
  BEmpty : Ord a => BSTree a
  BNode  : Ord a => (left : BSTree a) -> (val : a) -> (right : BSTree a) -> BSTree a

insert2 : a -> BSTree a -> BSTree a
insert2 x BEmpty = BNode BEmpty x BEmpty
insert2 x orig@(BNode left val right) = case compare x val of
                                             LT => BNode (insert2 x left) val right
                                             EQ => orig
                                             GT => BNode left val (insert2 x right)

-- Exercises!
-- Ex1
listToTree : Ord a => List a -> Tree a
listToTree [] = Empty
listToTree (x :: xs) = insert x (listToTree xs)

-- Ex2
treeToList : Tree a -> List a
treeToList Empty = []
treeToList (Node left x right) = treeToList left
                                 ++
                                 x :: treeToList right

-- Ex3 (classic)
data Expr : Type where
  Val : Int -> Expr
  Add : (t1 : Expr) -> (t2 : Expr) -> Expr
  Sub : (s1 : Expr) -> (s2 : Expr) -> Expr
  Mul : (f1 : Expr) -> (f2 : Expr) -> Expr

evaluate : Expr -> Int
evaluate (Val x) = x
evaluate (Add t1 t2) = evaluate t1 + evaluate t2
evaluate (Sub s1 s2) = evaluate s1 - evaluate s2
evaluate (Mul f1 f2) = evaluate f1 * evaluate f2

maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe Nothing y = y
maxMaybe (Just x) Nothing = Just x
maxMaybe (Just x) (Just y) = Just (max x y)

biggestTriangle2 : Picture -> Maybe Double
biggestTriangle2 (Primitive t@(Triangle x y)) = Just (area t)
biggestTriangle2 (Primitive (Rectangle x y)) = Nothing
biggestTriangle2 (Primitive (Circle x)) = Nothing
biggestTriangle2 (Combine p1 p2) = maxMaybe (biggestTriangle2 p1) (biggestTriangle2 p2)
biggestTriangle2 (Rotate r p) = biggestTriangle2 p
biggestTriangle2 (Translate x y p) = biggestTriangle2 p

-- Dependent types.  Woot!
-- Redefined in ex1
--data PowerSource = Petrol | Pedal

-- How is this type fundamentally different from Maybe a?
--data Vehicle : PowerSource -> Type where
--  Bicycle : Vehicle Pedal
--  Car     : (fuel : Nat) -> Vehicle Petrol
--  Bus     : (fuel : Nat) -> Vehicle Petrol
--
--wheels : Vehicle power -> Nat
--wheels Bicycle = 2
--wheels (Car fuel) = 4
--wheels (Bus fuel) = 4
--
--refuel : Vehicle Petrol -> Vehicle Petrol
--refuel (Car fuel) = Car (fuel + 20)
--refuel (Bus fuel) = Car (fuel + 10)
--refuel Bicycle impossible

data MyWeirdType : Type -> Type where
  A : MyWeirdType (Maybe Int)
  B : Nat -> MyWeirdType Double
  C : Nat -> MyWeirdType (Maybe Double)

myWeirdFunction1 : MyWeirdType Double
myWeirdFunction1 = B 5

myWeirdFunction2 : a -> MyWeirdType a
myWeirdFunction2 x = ?myWeirdFunction2_rhs  -- can this be defined in any way?

-- See Vect.idr

-- Ex1,2
data PowerSource = Pedal | Petrol | Electric
data Vehicle : PowerSource -> Type where
  Bicycle : Vehicle Pedal
  Unicycle : Vehicle Pedal
  Motorcycle : (fuel : Nat) -> Vehicle Petrol
  PetrolCar : (fuel : Nat) -> Vehicle Petrol
  Bus : (fuel : Nat) -> Vehicle Petrol
  Tram : Vehicle Electric
  ElectricCar : Vehicle Electric
-- Feels like a slightly contrived example...
-- there is power in it in terms of how depending on the PowerSource
-- Vehicle has a different definition (i.e. in terms of fuel).

wheels : Vehicle p -> Nat
wheels Bicycle = 2
wheels Unicycle = 1
wheels (Motorcycle fuel) = 2
wheels (PetrolCar fuel) = 4
wheels (Bus fuel) = 4

-- Ex 3,4
vectTake : (k : Fin n) -> Vect n a -> Vect (finToNat k) a
vectTake FZ xs = []
--vectTake (FS k') xs = ?vectTake_rhs_2  -- case on xs (it can't be [])
--vectTake (FS k') (x :: xs) = ?vectTake_rhs_1  -- search on ?rhs
vectTake (FS k') (x :: xs) = x :: vectTake k' xs  -- BAM programs that write themselves.

-- Remember, types are proofs so you can freely substitute 'proof'
-- with the word type
data LT : Nat -> Nat -> Type where
  LTZero : Chapter4.LT Z (S n)
  LTSucc : Chapter4.LT a b -> Chapter4.LT a (S b)

-- I like this version since it clearly shows what we need.
-- It is not as easy to workwith though.
vectTake' : LTE k n -> Vect n a -> Vect k a
vectTake' LTEZero xs = []
vectTake' (LTESucc k') (x :: xs) = x :: vectTake' k' xs

-- Ex5
sumEntries : Num a => (pos : Integer) -> Vect n a -> Vect n a -> Maybe a
sumEntries {n} pos xs ys = map (\i => (Data.Vect.index i xs) + (Data.Vect.index i ys))
                               (integerToFin pos n)

-- Now go to DataStore.idr

max_stars_repo_name: neduard/type-driven-development

max_issues_repo_name: neduard/type-driven-development

max_forks_repo_name: neduard/type-driven-development


text:
module Ray

import Vec3
-- import Hittable

%access export

public export

record Ray where
    constructor MkRay
    orig, dir : Vec3

at : Ray -> Double -> Vec3
at ray t = orig ray + t * dir ray

hitSphere : Vec3 -> Double -> Ray -> Double
hitSphere center radius ray = if discriminant < 0
    then -1.0
    else (-half_b - sqrt discriminant) / a
            where
                oc : Vec3
                oc = orig ray - center

                a : Double
                a = lengthSquared (dir ray)

                half_b : Double
                half_b = dot oc (dir ray)

                c : Double
                c = lengthSquared oc - radius * radius

                discriminant : Double
                discriminant = half_b*half_b - a*c

max_stars_repo_name: MarkMarkyMarkus/YART

max_issues_repo_name: MarkMarkyMarkus/YART

max_forks_repo_name: MarkMarkyMarkus/YART


text:
-- -------------------------------------------------------------- [ Parser.idr ]
-- Module    : Parser.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Common Parsers
module GRL.Lang.Common.Parser

import Lightyear
import Lightyear.Char
import Lightyear.Strings

import GRL.Common

%access export

-- ------------------------------------------------------ [ Parsing Lang Utils ]

comment : String -> String -> String -> Parser ()
comment l b e = (line l    *> pure ())
            <|> (block b e *> pure ())
            <|> spaces
            <?> "Comment"
    where
      line : String -> Parser String
      line l = do
          token l
          doc <- manyTill anyChar endOfLine
          spaces
          pure $ pack doc
        <?> "Line comment"

      block : String -> String -> Parser String
      block b e = do
          token b
          doc <- manyTill anyChar (token e)
          spaces
          pure $ pack doc
        <?> "Block Comment"

keyword : String -> Parser ()
keyword s = do
    string s
    spaces
    pure ()
  <?> "Keywords"

ident : Parser String
ident = lexeme (map pack $ some identChar) <?> "Identity"
  where
    identChar : Parser Char
    identChar = alphaNum <?> "Ident Char"

-- ------------------------------------------------------------ [ GLang Parser ]

gComment : Parser ()
gComment = comment "--" "{-" "-}" <?> "Comment"

cValue : Parser CValue
cValue = (keyword "Makes"   *> return MAKES)
     <|> (keyword "Helps"   *> return HELPS)
     <|> (keyword "SomePos" *> return SOMEPOS)
     <|> (keyword "Unknown" *> return UNKNOWN)
     <|> (keyword "SomeNeg" *> return SOMENEG)
     <|> (keyword "Breaks"  *> return BREAK)
     <|> (keyword "Hurts"   *> return HURTS)
     <?> "CValue"

sValue : Parser SValue
sValue = (keyword "Denied"    *> return DENIED)
     <|> (keyword "WeakDen"   *> return WEAKDEN)
     <|> (keyword "WeakSatis" *> return WEAKSATIS)
     <|> (keyword "Satisfied" *> return SATISFIED)
     <|> (keyword "Undecided" *> return UNDECIDED)
     <|> (keyword "None"      *> return NONE)
     <?> "Trait Type"

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
||| How to rename things
|||
||| Module    : Renaming.idr
||| Copyright : (c) Jan de Muijnck-Hughes
||| License   : see LICENSE
|||
module Toolkit.DeBruijn.Renaming

import Decidable.Equality
import Data.DPair

import Toolkit.Decidable.Informative

import Toolkit.Data.List.AtIndex
import Toolkit.Data.DList
import Toolkit.Data.DList.AtIndex

import Toolkit.DeBruijn.Context.Item
import Toolkit.DeBruijn.Context

%default total

public export
data IsVar : (ctxt : List kind)
          -> (type :      kind)
                  -> Type
  where
    V : (  pos : Nat)
     -> (0 prf : AtIndex type ctxt pos)
              -> IsVar   ctxt type

public export
%inline
shift : IsVar ctxt type -> IsVar (ctxt += a) type
shift (V pos prf) = V (S pos) (There prf)

public export
%inline
weaken : (func : IsVar old type
              -> IsVar new type)
      -> (IsVar (old += type') type
       -> IsVar (new += type') type)
weaken f (V Z Here)
  = V Z Here
weaken f (V (S idx) (There later)) with (f (V idx later))
  weaken f (V (S idx) (There later)) | (V pos prf)
    = V (S pos) (There prf)

public export
interface Rename (type : Type) (term : List type -> type -> Type) | term where
  rename : {old, new : List type}
        -> (f : {ty : type} -> IsVar old ty
                            -> IsVar new ty)
        -> ({ty : type} -> term old ty
                        -> term new ty)

  %inline
  embed : {ty   : type}
       -> {ctxt : List type}
               -> IsVar ctxt ty
               -> term  ctxt ty

public export
%inline
weakens : {type : Type}
       -> {term : List type -> type -> Type}
       -> Rename type term
       => {old, new : List type}
       -> (f : {ty  : type}
                   -> IsVar old ty
                   -> term  new ty)
       -> ({ty,type' : type}
              -> IsVar (old += type') ty
              -> term  (new += type') ty)

weakens f (V 0 Here)
  = embed (V Z Here)
weakens f (V (S idx) (There later))
  = rename shift (f (V idx later))

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
main : IO ()
main = putStrLn "Running Jvm program located in folder with spaces"


text:
module Markdown.Tokens

import Data.String
import Markdown.String
import Extra.String
import public Text.Token

safeSub : Nat -> Nat -> Nat
safeSub _ Z = Z
safeSub Z v = v
safeSub (S n) (S k) = safeSub n k

getLinkDesc : String -> (String, String)
getLinkDesc text =
  let
    (linkPart, descPart) = break (== ']') text
    linkLenFinal = safeSub 1 (length linkPart)
    descLenFinal = safeSub 3 (length descPart)
  in
    (
      substr 1 linkLenFinal linkPart,
      substr 2 descLenFinal descPart
    )

public export
data MarkdownTokenKind
  = HeadingSym
  | MdText
  | MdPre
  | MdCodeBlock
  | NewLine
  | ItalicsSym
  | BoldSym
  | ImageSym
  | MdLink
  | HtmlOpenTag
  | HtmlCloseTag

public export
Eq MarkdownTokenKind where
  (==) HeadingSym HeadingSym = True
  (==) MdText MdText = True
  (==) MdPre MdPre = True
  (==) MdCodeBlock MdCodeBlock = True
  (==) NewLine NewLine = True
  (==) ItalicsSym ItalicsSym = True
  (==) BoldSym BoldSym = True
  (==) ImageSym ImageSym = True
  (==) MdLink MdLink = True
  (==) HtmlOpenTag HtmlOpenTag = True
  (==) HtmlCloseTag HtmlCloseTag = True
  (==) _ _ = False

public export
MarkdownToken : Type
MarkdownToken = Token MarkdownTokenKind

dropEnds : Int -> String -> String
dropEnds n str =
  let
    len : Int
    len = cast $ length str
  in
    strSubstr n (len - 2 * n) str

public export
TokenKind MarkdownTokenKind where
  TokType HeadingSym = Nat
  TokType MdText = String
  TokType MdPre = String
  TokType MdCodeBlock = (String, Maybe String)
  TokType NewLine = ()
  TokType ItalicsSym = ()
  TokType BoldSym = ()
  TokType ImageSym = ()
  TokType MdLink = (String, String)
  TokType HtmlOpenTag = String
  TokType HtmlCloseTag = String

  tokValue HeadingSym x = length x
  tokValue MdText txt = txt
  tokValue MdPre txt = dropEnds 1 txt
  tokValue MdCodeBlock txt =
    case Extra.String.split '\n' (dropEnds 3 txt) of
      [] =>
        ("", Nothing)

      ("\n" :: x) =>
        (join "\n" x, Nothing)

      hd :: x =>
        (join "\n" x, Just hd)

  tokValue NewLine _ = ()
  tokValue ItalicsSym _ = ()
  tokValue BoldSym _ = ()
  tokValue ImageSym _ = ()
  tokValue MdLink text = getLinkDesc text
  tokValue HtmlOpenTag tag = (filter isAlphaNum tag) -- TODO: Improve quality
  tokValue HtmlCloseTag tag = (filter isAlphaNum tag) -- how to do this?

export
Show MarkdownToken where
  show (Tok HeadingSym l) = "HeadingSym " ++ (show l)
  show (Tok MdText txt) = "MdText " ++ (quote txt)
  show (Tok MdPre txt) = "MdPre " ++ (quote txt)
  show (Tok MdCodeBlock txt) = "MdCodeBlock " ++ (quote txt)
  show (Tok NewLine _) = "NewLine"
  show (Tok ItalicsSym _) = "ItalicsSym"
  show (Tok BoldSym _) = "BoldSym"
  show (Tok ImageSym _) = "ImageSym"
  show (Tok MdLink txt) = "MdLink " ++ (quote txt)
  show (Tok HtmlOpenTag tag) = "StartTag " ++ quote tag
  show (Tok HtmlCloseTag tag) = "EndTag " ++ quote tag

export
Eq MarkdownToken where
  (Tok HeadingSym l0) == (Tok HeadingSym l1) = l0 == l1
  (Tok MdText txt0) == (Tok MdText txt1) = txt0 == txt1
  (Tok MdPre txt0) == (Tok MdPre txt1) = txt0 == txt1
  (Tok MdCodeBlock txt0) == (Tok MdCodeBlock txt1) = txt0 == txt1
  (Tok NewLine _) == (Tok NewLine _) = True
  (Tok ItalicsSym _) == (Tok ItalicsSym _) = True
  (Tok BoldSym _) == (Tok BoldSym _) = True
  (Tok ImageSym _) == (Tok ImageSym _) = True
  (Tok MdLink txt0) == (Tok MdLink txt1) = txt0 == txt1
  (Tok HtmlOpenTag tag0) == (Tok HtmlOpenTag tag1) = tag0 == tag1
  (Tok HtmlCloseTag tag0) == (Tok HtmlCloseTag tag1) = tag0 == tag1
  _ == _ = False

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo