text:
module Network.TLS.HelloExtension

import Data.List1
import Data.Vect
import Network.TLS.Magic
import Network.TLS.Parsing
import Utils.Bytes
import Utils.Misc
import Utils.Show

public export
KeyBytes : Type
KeyBytes = List Bits8

-- TODO: even more stuff
public export
data ServerNameEntry : Type where
  DNS : String -> ServerNameEntry

public export
Show ServerNameEntry where
  show (DNS x) = show_record "DNS" [("name", show x)]

XServerNameEntry : Type
XServerNameEntry = Eithers [String]

hack_server_name_entry : ServerNameEntry -> XServerNameEntry
hack_server_name_entry (DNS x) = x

fix_server_name_entry : XServerNameEntry -> ServerNameEntry
fix_server_name_entry x = (DNS x)

namespace ClientExtension
  public export
  data ClientExtension : ExtensionType -> Type where
    ServerName : List1 ServerNameEntry -> ClientExtension ServerName
    SupportedGroups : List1 SupportedGroup -> ClientExtension SupportedGroups
    SignatureAlgorithms : List1 SignatureAlgorithm -> ClientExtension SignatureAlgorithms
    SupportedVersions : List1 TLSVersion -> ClientExtension SupportedVersions
    KeyShare : List1 (SupportedGroup, KeyBytes) -> ClientExtension KeyShare
    -- TODO: PSK

  public export
  Show (ClientExtension type) where
    show (ServerName entries) = show_record "ServerName" [("entries", show entries)]
    show (SupportedGroups entries) = show_record "SupportedGroups" [("entries", show entries)]
    show (SignatureAlgorithms entries) = show_record "SignatureAlgorithms" [("entries", show entries)]
    show (SupportedVersions entries) = show_record "SupportedVersions" [("entries", show entries)]
    show (KeyShare entries) = show_record "KeyShare" [("entries", show entries)]

XClientExtension : Type
XClientExtension = Eithers
  [ ClientExtension ServerName
  , ClientExtension SupportedGroups
  , ClientExtension SignatureAlgorithms
  , ClientExtension SupportedVersions
  , ClientExtension KeyShare
  ]

hack_client_extension : DPair _ ClientExtension -> XClientExtension
hack_client_extension (ServerName ** x) = Left x
hack_client_extension (SupportedGroups ** x) = Right (Left x)
hack_client_extension (SignatureAlgorithms ** x) = Right (Right (Left x))
hack_client_extension (SupportedVersions ** x) = Right (Right (Right (Left x)))
hack_client_extension (KeyShare ** x) = Right (Right (Right (Right x)))

fix_client_extension : XClientExtension -> DPair _ ClientExtension
fix_client_extension (Left x) = (_ ** x)
fix_client_extension (Right (Left x)) = (_ ** x)
fix_client_extension (Right (Right (Left x))) = (_ ** x)
fix_client_extension (Right (Right (Right (Left x)))) = (_ ** x)
fix_client_extension (Right (Right (Right (Right x)))) = (_ ** x)

namespace ServerExtension
  public export
  data ServerExtension : ExtensionType -> Type where
    SupportedGroups : SupportedGroup -> ServerExtension SupportedGroups
    SignatureAlgorithms : SignatureAlgorithm -> ServerExtension SignatureAlgorithms
    SupportedVersions : TLSVersion -> ServerExtension SupportedVersions
    KeyShare : (SupportedGroup, KeyBytes) -> ServerExtension KeyShare
    Unknown : (id : (Bits8, Bits8)) -> List Bits8 -> ServerExtension (Unknown id)

  public export
  Show (ServerExtension type) where
    show (SupportedGroups entries) = show_record "SupportedGroups" [("entry", show entries)]
    show (SignatureAlgorithms entries) = show_record "SignatureAlgorithms" [("entry", show entries)]
    show (SupportedVersions entries) = show_record "SupportedVersions" [("entry", show entries)]
    show (KeyShare entries) = show_record "KeyShare" [("entry", show entries)]
    show (Unknown (a, b) body) = show_record "Unknown" [("id", xxd $ the (List Bits8) [a, b]), ("body", xxd body)]

XServerExtension : Type
XServerExtension = Eithers
  [ ServerExtension SupportedGroups
  , ServerExtension SignatureAlgorithms
  , ServerExtension SupportedVersions
  , ServerExtension KeyShare
  , (a ** ServerExtension (Unknown a))
  ]

hack_server_extension : DPair _ ServerExtension -> XServerExtension
hack_server_extension (SupportedGroups ** x)     = Left x
hack_server_extension (SignatureAlgorithms ** x) = Right (Left x)
hack_server_extension (SupportedVersions ** x)   = Right (Right (Left x))
hack_server_extension (KeyShare ** x)            = Right (Right (Right (Left x)))
hack_server_extension ((Unknown id) ** x)        = Right (Right (Right (Right (id ** x))))

fix_server_extension : XServerExtension -> DPair _ ServerExtension
fix_server_extension (Left x) = (_ ** x)
fix_server_extension (Right (Left x)) = (_ ** x)
fix_server_extension (Right (Right (Left x))) = (_ ** x)
fix_server_extension (Right (Right (Right (Left x)))) = (_ ** x)
fix_server_extension (Right (Right (Right (Right (x ** y))))) = (_ ** y)

namespace Parsing
  namespace Client
    export
    with_id : (Cons (Posed Bits8) i, Monoid i) => {type : ExtensionType} -> Parserializer Bits8 i (SimpleError String) (ClientExtension type) -> Parserializer Bits8 i (SimpleError String) (ClientExtension type)
    with_id pser = under (show type <+> " extension") $ is (pair_to_vect $ extension_type_to_id type) *> pser

    -- TODO: generalize
    export
    server_name_dns_entry : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) String
    server_name_dns_entry = is [0x00] *> map ascii_to_string string_to_ascii (lengthed_list 2 token)

    export
    server_name_entry : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) ServerNameEntry
    server_name_entry = map fix_server_name_entry hack_server_name_entry $ server_name_dns_entry

    export
    no_id_server_name : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (ClientExtension ServerName)
    no_id_server_name = lengthed 2 $ map ServerName (\(ServerName x) => x) $ lengthed_list1 2 server_name_entry

    export
    no_id_supported_groups : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (ClientExtension SupportedGroups)
    no_id_supported_groups = lengthed 2 $ map SupportedGroups (\(SupportedGroups x) => x) $ lengthed_list1 2 supported_group

    export
    no_id_signature_algorithms : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (ClientExtension SignatureAlgorithms)
    no_id_signature_algorithms = lengthed 2 $ map SignatureAlgorithms (\(SignatureAlgorithms x) => x) $ lengthed_list1 2 signature_algorithm

    export
    no_id_supported_versions : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (ClientExtension SupportedVersions)
    no_id_supported_versions = lengthed 2 $ map SupportedVersions (\(SupportedVersions x) => x) $ lengthed_list1 1 tls_version

    export
    no_id_key_share : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (ClientExtension KeyShare)
    no_id_key_share = lengthed 2 $ map KeyShare (\(KeyShare x) => x) $ lengthed_list1 2 (supported_group <*>> lengthed_list 2 token)

    export
    extension : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (DPair _ ClientExtension)
    extension = map fix_client_extension hack_client_extension
      $ (with_id no_id_server_name)
      <|> (with_id no_id_supported_groups)
      <|> (with_id no_id_signature_algorithms)
      <|> (with_id no_id_supported_versions)
      <|> (with_id no_id_key_share)

  namespace Server
    export
    no_id_supported_groups : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (ServerExtension SupportedGroups)
    no_id_supported_groups = lengthed 2 $ map SupportedGroups (\(SupportedGroups x) => x) $ supported_group

    export
    no_id_signature_algorithms : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (ServerExtension SignatureAlgorithms)
    no_id_signature_algorithms = lengthed 2 $ map SignatureAlgorithms (\(SignatureAlgorithms x) => x) $ signature_algorithm

    export
    no_id_supported_versions : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (ServerExtension SupportedVersions)
    no_id_supported_versions = lengthed 2 $ map SupportedVersions (\(SupportedVersions x) => x) $ tls_version

    export
    no_id_key_share : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (ServerExtension KeyShare)
    no_id_key_share = lengthed 2 $ map KeyShare (\(KeyShare x) => x) $ (supported_group <*>> lengthed_list 2 token)

    export
    with_id : (Cons (Posed Bits8) i, Monoid i) => {type : ExtensionType} -> Parserializer Bits8 i (SimpleError String) (ServerExtension type) -> Parserializer Bits8 i (SimpleError String) (ServerExtension type)
    with_id pser = under (show type <+> " extension") $ is (pair_to_vect $ extension_type_to_id type) *> pser

    export
    with_id_unknown : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (rid ** ServerExtension (Unknown rid))
    with_id_unknown = MkParserializer serialize deserialize
      where
        serialize : (rid ** ServerExtension (Unknown rid)) -> List Bits8
        serialize ((a,b) ** (Unknown _ body)) = [a,b] <+> (prepend_length 2 body)
        deserialize : Parser i (SimpleError String) (rid ** ServerExtension (Unknown rid))
        deserialize = do
          [a, b] <- count 2 p_get
          body <- (lengthed_list 2 token).decode
          pure ((a,b) ** Unknown (a,b) body)

    export
    extension : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (DPair _ ServerExtension)
    extension = map fix_server_extension hack_server_extension
      $ (with_id no_id_supported_groups)
      <|> (with_id no_id_signature_algorithms)
      <|> (with_id no_id_supported_versions)
      <|> (with_id no_id_key_share)
      <|> (with_id_unknown)


text:
import Control.Isomorphism

%default total

-- probably useless
data Morphism : (a : Type) -> (b : Type) -> (f : a -> b) -> Type where
  MkMorphism : (f : a -> b) ->
               Morphism a b f

-- retraction for f
data Retraction : (a : Type) -> (b : Type) -> (f : a -> b) -> (r : b -> a) -> Type where
  MkRetraction : (f : a -> b) ->
                 (r : b -> a) ->
                 (v : (x : a) -> r (f x) = x) ->
                 Retraction a b f r

-- section for f
data Section : (a : Type) -> (b : Type) -> (f : a -> b) -> (s : b -> a) -> Type where
  MkSection : (f : a -> b) ->
              (s : b -> a) ->
              (v : (y : b) -> f (s y) = y) ->
              Section a b f s

-- retraction + section
data Isomorphism : (a : Type) -> (b : Type) -> Type where
  MkIsomorphism : {f : a -> b} ->
                  (r : Retraction a b f r') ->
                  (s : Section a b f s') ->
                  Isomorphism a b

uniquenessOfInverses : Retraction a b f r -> Section a b f s -> (x : b) -> r x = s x
uniquenessOfInverses (MkRetraction f r rv) (MkSection f s sv) x =
  -- s x = r x
  rewrite (sym $ sv x) in
  -- r (f (s x)) = s (f (s x))
  rewrite (rv (s x)) in
  -- s x = s (f (s x))
  rewrite (sv x) in
  -- s x = s x
  Refl

toIso : Isomorphism a b -> Iso a b
toIso (MkIsomorphism (MkRetraction f r rv) (MkSection f s sv)) =
  MkIso f s sv (\x => rewrite (sym $ uniquenessOfInverses (MkRetraction f r rv) (MkSection f s sv) (f x)) in (rv x))

data Inspect : a -> Type where
  wi : {A : Type} -> (x : A) -> (y : A) -> (eq: x = y) -> Inspect x

inspect : {A : Type} -> (x : A) -> Inspect x
inspect x = wi x _ Refl

match : {A : Type} -> {x : A} -> (y : A) -> {eq : x = y} -> Inspect x
match y {eq} = wi _ y eq

appIso : Iso a b -> a -> b
appIso (MkIso to _ _ _) x = to x

unappIso : Iso a b -> b -> a
unappIso (MkIso _ from _ _) x = from x

ext: idr

max_stars_repo_name: defanor/morphisms

max_issues_repo_name: defanor/morphisms

max_forks_repo_name: defanor/morphisms


text:
module SourceLoc

import Data.Vect
import Data.Fin
import Language.Reflection
import Language.Reflection.Utils

%default total
%language DSLNotation

||| A "function" that returns where it is called in the source
getLoc : {default tactics { sourceLocation } x : SourceLocation} -> SourceLocation
getLoc {x} = x

||| A test of getLoc
fromRHS : SourceLocation
fromRHS = getLoc

||| Testing getting source locations from RHS proof scripts
fromProofScript : SourceLocation
fromProofScript = proof sourceLocation

||| Testing getting source locations from deferred proofs.
fromMetavar : SourceLocation
fromMetavar = ?meta

--- Testing that getting source locations in ASTs constructed with DSL notation
data Ty = U | Arr Ty Ty

interp : Ty -> Type
interp U         = ()
interp (Arr x y) = interp x -> Either SourceLocation (interp y)

using (ctxt : Vect n Ty)
  data Tm : Vect n Ty -> Ty -> Type where
    MkU : Tm ctxt U
    Var : (i : Fin n) -> Tm ctxt (index i ctxt)
    Lam : Tm (t::ctxt) t' -> Tm ctxt (Arr t t')
    App : Tm ctxt (Arr t t') -> Tm ctxt t -> Tm ctxt t'
    ||| A term that makes the program halt and printLn where it halted
    Die : {default tactics { sourceLocation } loc : SourceLocation} -> Tm ctxt t

  data Env : Vect n Ty -> Type where
    Nil : Env []
    (::) : interp t -> Env ctxt -> Env (t::ctxt)

  index : (i : Fin n) -> Env ctxt -> interp (index i ctxt)
  index FZ     (x::env) = x
  index (FS i) (x::env) = index i env

  run : Tm ctxt t -> Env ctxt -> Either SourceLocation (interp t)
  run MkU         _   = pure ()
  run (Var i)     env = pure $ index i env
  run (Lam bdy)   env = pure $ \x => run bdy (x::env)
  run (App f x)   env = !(run f env) !(run x env)
  run (Die {loc}) _   = Left loc

  lam_ : _ -> Tm (t::ctxt) t' -> Tm ctxt (Arr t t')
  lam_ _ = Lam

exec : Tm [] t -> IO ()
exec tm = case run tm [] of
            Left loc  => putStrLn $ "Error at " ++ show loc
            Right _   => putStrLn $ "Success!"

dsl lang
  variable = Var
  index_first = FZ
  index_next = FS
  lambda = lam_

testTerm1 : Tm [] (Arr U U)
testTerm1 = lang (\x=>Die)

testTerm2 : Tm [] U
testTerm2 = App testTerm1 MkU

testTerm3 : Tm [] (Arr U U)
testTerm3 = lang (\x => MkU)

testTerm4 : Tm [] U
testTerm4 = App testTerm3 MkU

namespace Main
  main : IO ()
  main = do putStrLn "Testing using definition"
            printLn fromRHS
            putStrLn "Testing using inline tactics"
            printLn fromProofScript
            putStrLn "Testing using metavariable with later definition"
            printLn fromMetavar
            putStrLn "-----------------------"
            sequence_ $ with List [ exec testTerm1
                                  , exec testTerm2
                                  , exec testTerm3
                                  , exec testTerm4
                                  ]
---------- Proofs ----------
SourceLoc.meta = proof
  sourceLocation

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Core.Hash

import Core.CaseTree
import Core.TT

import Data.List
import Data.List1
import Data.Strings

%default covering

-- This is so that we can store a hash of the interface in ttc files, to avoid
-- the need for reloading modules when no interfaces have changed in imports.
-- As you can probably tell, I know almost nothing about writing good hash
-- functions, so better implementations will be very welcome...

public export
interface Hashable a where
  hash : a -> Int
  hashWithSalt : Int -> a -> Int

  hash = hashWithSalt 5381
  hashWithSalt h i = h * 33 + hash i

infixl 5 `hashWithSalt`

export
Hashable Int where
  hash = id

export
Hashable Integer where
  hash = fromInteger

export
Hashable Nat where
  hash = cast

export
Hashable Char where
  hash = cast

export
Hashable a => Hashable (List a) where
  hashWithSalt h [] = abs h
  hashWithSalt h (x :: xs) = hashWithSalt (h * 33 + hash x) xs

export
Hashable a => Hashable (List1 a) where
  hashWithSalt h (x ::: xs) = hashWithSalt (h * 33 + hash x) xs

export
Hashable a => Hashable (Maybe a) where
  hashWithSalt h Nothing = abs h
  hashWithSalt h (Just x) = hashWithSalt h x

export
Hashable String where
  hashWithSalt h str = hashChars h 0 (cast (length str)) str
    where
      hashChars : Int -> Int -> Int -> String -> Int
      hashChars h p len str
          = assert_total $
              if p == len
                 then h
                 else hashChars (h * 33 + cast (strIndex str p))
                                (p + 1) len str

export
Hashable Namespace where
  hashWithSalt h ns = hashWithSalt h (unsafeUnfoldNamespace ns)

export
Hashable Name where
  hashWithSalt h (MN s _) = hashWithSalt h s
  hashWithSalt h (DN _ n) = hashWithSalt h n
  hashWithSalt h (NS ns n) = hashWithSalt (hashWithSalt h ns) n
  hashWithSalt h (Resolved i) = hashWithSalt h i
  hashWithSalt h n = hashWithSalt h (show n)

export
Hashable RigCount where
  hashWithSalt h = elimSemi
                     (hashWithSalt h 0)
                     (hashWithSalt h 1)
                     (const $ hashWithSalt h 2)

export
Hashable t => Hashable (PiInfo t) where
  hashWithSalt h Implicit = hashWithSalt h 0
  hashWithSalt h Explicit = hashWithSalt h 1
  hashWithSalt h AutoImplicit = hashWithSalt h 2
  hashWithSalt h (DefImplicit t) = h `hashWithSalt` 3 `hashWithSalt` t

export
Hashable ty => Hashable (Binder ty) where
  hashWithSalt h (Lam _ c p ty)
      = h `hashWithSalt` 0 `hashWithSalt` c `hashWithSalt` p `hashWithSalt` ty
  hashWithSalt h (Let _ c val ty)
      = h `hashWithSalt` 1 `hashWithSalt` c `hashWithSalt` val `hashWithSalt` ty
  hashWithSalt h (Pi _ c p ty)
      = h `hashWithSalt` 2 `hashWithSalt` c `hashWithSalt` p `hashWithSalt` ty
  hashWithSalt h (PVar _ c p ty)
      = h `hashWithSalt` 3 `hashWithSalt` c `hashWithSalt` p `hashWithSalt` ty
  hashWithSalt h (PLet _ c val ty)
      = h `hashWithSalt` 4 `hashWithSalt` c `hashWithSalt` val `hashWithSalt` ty
  hashWithSalt h (PVTy _ c ty)
      = h `hashWithSalt` 5 `hashWithSalt` c `hashWithSalt` ty

Hashable (Var vars) where
  hashWithSalt h (MkVar {i} _) = hashWithSalt h i

mutual
  export
  Hashable (Term vars) where
    hashWithSalt h (Local fc x idx y)
        = h `hashWithSalt` 0 `hashWithSalt` idx
    hashWithSalt h (Ref fc x name)
        = h `hashWithSalt` 1 `hashWithSalt` name
    hashWithSalt h (Meta fc x y xs)
        = h `hashWithSalt` 2 `hashWithSalt` y `hashWithSalt` xs
    hashWithSalt h (Bind fc x b scope)
        = h `hashWithSalt` 3 `hashWithSalt` b `hashWithSalt` scope
    hashWithSalt h (App fc fn arg)
        = h `hashWithSalt` 4 `hashWithSalt` fn `hashWithSalt` arg
    hashWithSalt h (As fc _ nm pat)
        = h `hashWithSalt` 5 `hashWithSalt` nm `hashWithSalt` pat
    hashWithSalt h (TDelayed fc x y)
        = h `hashWithSalt` 6 `hashWithSalt` y
    hashWithSalt h (TDelay fc x t y)
        = h `hashWithSalt` 7 `hashWithSalt` t `hashWithSalt` y
    hashWithSalt h (TForce fc r x)
        = h `hashWithSalt` 8 `hashWithSalt` x
    hashWithSalt h (PrimVal fc c)
        = h `hashWithSalt` 9 `hashWithSalt` (show c)
    hashWithSalt h (Erased fc _)
        = hashWithSalt h 10
    hashWithSalt h (TType fc)
        = hashWithSalt h 11

  export
  Hashable Pat where
    hashWithSalt h (PAs fc nm pat)
        = h `hashWithSalt` 0 `hashWithSalt` nm `hashWithSalt` pat
    hashWithSalt h (PCon fc x tag arity xs)
        = h `hashWithSalt` 1 `hashWithSalt` x `hashWithSalt` xs
    hashWithSalt h (PTyCon fc x arity xs)
        = h `hashWithSalt` 2 `hashWithSalt` x `hashWithSalt` xs
    hashWithSalt h (PConst fc c)
        = h `hashWithSalt` 3 `hashWithSalt` (show c)
    hashWithSalt h (PArrow fc x s t)
        = h `hashWithSalt` 4 `hashWithSalt` s `hashWithSalt` t
    hashWithSalt h (PDelay fc r t p)
        = h `hashWithSalt` 5 `hashWithSalt` t `hashWithSalt` p
    hashWithSalt h (PLoc fc x)
        = h `hashWithSalt` 6 `hashWithSalt` x
    hashWithSalt h (PUnmatchable fc x)
        = h `hashWithSalt` 7 `hashWithSalt` x

  export
  Hashable (CaseTree vars) where
    hashWithSalt h (Case idx x scTy xs)
        = h `hashWithSalt` 0 `hashWithSalt` idx `hashWithSalt` xs
    hashWithSalt h (STerm _ x)
        = h `hashWithSalt` 1 `hashWithSalt` x
    hashWithSalt h (Unmatched msg)
        = h `hashWithSalt` 2
    hashWithSalt h Impossible
        = h `hashWithSalt` 3

  export
  Hashable (CaseAlt vars) where
    hashWithSalt h (ConCase x tag args y)
        = h `hashWithSalt` 0 `hashWithSalt` x `hashWithSalt` args
            `hashWithSalt` y
    hashWithSalt h (DelayCase t x y)
        = h `hashWithSalt` 2 `hashWithSalt` (show t)
            `hashWithSalt` (show x) `hashWithSalt` y
    hashWithSalt h (ConstCase x y)
        = h `hashWithSalt` 3 `hashWithSalt` (show x) `hashWithSalt` y
    hashWithSalt h (DefaultCase x)
        = h `hashWithSalt` 4 `hashWithSalt` x


text:
-- SPDX-FileCopyrightText: 2021 The ipkg-idr developers
--
-- SPDX-License-Identifier: MPL-2.0

module Language.IPKG

import public Language.IPKG.Value
import Language.IPKG.Lexer
import Language.IPKG.Parser

export
parseIPKG : (source : String) -> Either String PkgDesc
parseIPKG source = do
    Just toks <- pure $ lexIPKG source
        | Nothing => Left "Lexer error"

    parseIPKGFromToks toks

max_stars_repo_name: tiatomee/ipkg-idr

max_issues_repo_name: tiatomee/ipkg-idr

max_forks_repo_name: tiatomee/ipkg-idr


text:
module Main

import System

readNumber : IO (Maybe Nat)
readNumber = do
  input <- getLine
  if all isDigit (unpack input)
     then pure (Just (cast input))
     else pure Nothing

countdown : (secs : Nat) -> IO ()
countdown Z = putStrLn "Lift off!"
countdown (S secs) = do putStrLn (show (S secs))
                        usleep 1000000
                        countdown secs

countdowns : IO ()
countdowns = do putStr "Enter starting number: "
                Just startNum <- readNumber
                    | Nothing => do putStrLn "Invalid input"
                                    countdowns
                countdown startNum
                putStrLn "Another (y/n)? "
                yn <- getLine
                if yn == "y" then countdowns
                             else pure ()


text:
module DecompressionTest

import Data.Compress.GZip
import Data.Compress.CRC
import System.File
import System.File.Mode
import Control.Monad.Error.Either
import Control.Monad.Trans
import Data.Buffer
import Data.List
import Data.Compress.Utils.Parser
import Data.Compress.Utils.Bytes
import Data.Compress.Interface
import Data.Vect
import Data.SnocList
import Crypto.Hash
import Utils.Bytes

%default partial

maybe_to_either : Lazy b -> Maybe a -> Either b a
maybe_to_either b Nothing = Left $ Force b
maybe_to_either _ (Just a) = Right a

new_buffer : Nat -> IO Buffer
new_buffer n = case !(newBuffer (cast n)) of Just buf => pure buf; Nothing => idris_crash "cannot make buffer"

gzmd5 : String -> IO (Either String (List Bits8))
gzmd5 path = withFile path Read (pure . show) $ \file => runEitherT $ (lift $ new_buffer 128) >>= loop file init (Hash.init MD5) where
  loop : File -> GZipState -> MD5 -> Buffer -> EitherT String IO (List Bits8)
  loop file state hash_state buffer = do
    False <- lift $ fEOF file
    | True => case state of MkState [] (_ ** AtGHeader) => pure (toList $ finalize hash_state); _ => throwE "gzip stream not complete"
    buffer_size <- lift (rawSize buffer)
    len <- bimapEitherT show id $ MkEitherT $ readBufferData file buffer 0 buffer_size
    data' <- traverse (getBits8 buffer) [0..(len-1)]
    let Right (uncompressed, state) = feed state data'
    | Left err => throwE "error while decompressing: \{err}"
    loop file state (update uncompressed hash_state) buffer

gzmd5_check : String -> String -> EitherT String IO ()
gzmd5_check expected_checksum filename = do
  checksum <- MkEitherT (gzmd5 filename)
  let checksum_str = concat $ map show_hex checksum
  if checksum_str == expected_checksum
    then pure ()
    else throwE "checksum error: expected \{expected_checksum}, got \{checksum_str}"

-- Compressed data that is gzip + 1 single deflate uncompressed block
export
test_gzip_uncompressed : EitherT String IO ()
test_gzip_uncompressed = gzmd5_check "66bd413f7a853c4fe78bddede9e8c5d7" "files/random.bin.gz"

-- Compressed data using only fixed huffman encoding
export
test_gzip_fixed_huffman : EitherT String IO ()
test_gzip_fixed_huffman = gzmd5_check "0eb38a55ee9ab4f5d3283f6a33e0529e" "files/hello.gz"

-- General gzip compressed text
export
test_gzip_text : EitherT String IO ()
test_gzip_text = gzmd5_check "00c77291948ef959cb472e2935ca8963" "files/jabberwock.txt.gz"

-- General gzip compressed image
export
test_gzip_jpg : EitherT String IO ()
test_gzip_jpg = gzmd5_check "3a8f86011336fa59fe49618a05d34b83" "files/jabberwocky.jpg.gz"

-- Two gzip body concated into one file (allowed by the RFC for some reason)
export
test_gzip_concated : EitherT String IO ()
test_gzip_concated = gzmd5_check "ffe16dc45c35a1c3a0aa40875eca747e" "files/concatenated.gz"


text:
module UML.Types

import UML.Class.Model
import UML.Sequence.Model
import UML.Deployment.Model
import UML.Component.Model

data UMLTy = CLAZZ | SEQUENCE | DEPLOYMENT | COMPONENT

data UML : Type where
  Class      : ClassModel MODEL      -> UML
  Component  : ComponentModel MODEL  -> UML
  Sequence   : SequenceModel MODEL   -> UML
  Deployment : DeploymentModel MODEL -> UML

instance Show UMLTy where
  show CLAZZ      = "Clazz"
  show SEQUENCE   = "Sequence"
  show DEPLOYMENT = "Deployment"
  show COMPONENT  = "Component"

instance Eq UMLTy where
  (==) CLAZZ      CLAZZ      = True
  (==) SEQUENCE   SEQUENCE   = True
  (==) DEPLOYMENT DEPLOYMENT = True
  (==) COMPONENT  COMPONENT  = True
  (==) _          _          = False

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

max_stars_repo_name: jfdm/idris-uml

max_issues_repo_name: jfdm/idris-uml

max_forks_repo_name: jfdm/idris-uml


text:
module Sub08LTE108t99

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total

-- 6(18t+16)+3 --EF[2,1,-2]--> 6(8t+3)+3
export
lte108t99 : (l : Nat) -> LTE (S (S (S (S ((l+l)+(l+l))))))
  (S ((S ((S (S (l+l+l)))+(S (S (l+l+l))))) + (S ((S (S (l+l+l)))+(S (S (l+l+l))))) + (S ((S (S (l+l+l)))+(S (S (l+l+l)))))))
lte108t99 Z     = (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc) LTEZero
lte108t99 (S l) =
  let lemma = lte108t99 l in

  rewrite (sym (plusSuccRightSucc l l)) in

  rewrite (sym (plusSuccRightSucc (plus l l) l)) in

  rewrite (sym (plusSuccRightSucc (plus l l) (S (plus l l)))) in
  rewrite (sym (plusSuccRightSucc (plus l l)    (plus l l))) in

  rewrite (sym (plusSuccRightSucc (plus (plus l l) l)
                                  (S (S (S (S (plus (plus l l) l))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus l l) l)
                                     (S (S (S (plus (plus l l) l)))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus l l) l)
                                        (S (S (plus (plus l l) l))))) in

  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                                  (S (S (S (S (S (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l)
                                           l)))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                                     (S (S (S (S (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l)
                                           l))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                                        (S (S (S (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l)
                                           l)))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                                           (S (S (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l)
                                           l))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                                              (S (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l)
                                           l)))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                                                 (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l)
                                           l))))))))) in

  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                        (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                                  (S (S (S (S (S (S (S (S (plus (plus (plus l l) l)
                        (S (S (plus (plus l l) l)))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                        (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                                     (S (S (S (S (S (S (S (plus (plus (plus l l) l)
                        (S (S (plus (plus l l) l))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                        (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                                        (S (S (S (S (S (S (plus (plus (plus l l) l)
                        (S (S (plus (plus l l) l)))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                        (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                                           (S (S (S (S (S (plus (plus (plus l l) l)
                        (S (S (plus (plus l l) l))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                        (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                                              (S (S (S (S (plus (plus (plus l l) l)
                        (S (S (plus (plus l l) l)))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                        (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                                                 (S (S (S (plus (plus (plus l l) l)
                        (S (S (plus (plus l l) l))))))))) in

    (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc) lemma


text:
-- -------------------------------------------------------------- [ Parser.idr ]
-- Module      : UML.Sequence.Parser
-- Description : Parser for textual UML sequence diagrams.
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module UML.Sequence.Parser

import Lightyear
import Lightyear.Strings

import UML.Types

import UML.Code.Model
import UML.Code.Parser

import UML.Sequence.Model
import UML.Utils.Parsing

%access private

||| Parse a single step.
step : Parser $ SequenceModel SEND
step = do
    from <- ident <* space
    token "->"
    to <- ident <* space
    colon
    ms <- parens $ commaSep1 attr
    pure $ Send from to ms
  <?> "Step"

||| Parse a sequence diagram, a series of steps.
public
sequenceModel : Parser UML
sequenceModel = do
    ds <- some (dtype <* space)
    space
    ss <- some (step <* space)
    pure $ Sequence $ MkSeqModel ds (mkStep ss)
  <?> "Sequence Model"
-- --------------------------------------------------------------------- [ EOF ]


text:
||| [specification](http://csrc.nist.gov/publications/fips/fips180-4/fips-180-4.pdf)
module Data.Crypto.Hash.SHS

import Data.Bits
import Data.Crypto.Hash
import Data.Crypto.Util
import Data.Fin
import Data.Mod
import Data.Vect

-- Functions

ch : Bits n -> Bits n -> Bits n -> Bits n
ch x y z = (x `and` y) `xor` (complement x `and` z)

parity : Bits n -> Bits n -> Bits n -> Bits n
parity x y z = (x `xor` y) `xor` z

maj : Bits n -> Bits n -> Bits n -> Bits n
maj x y z = ((x `and` y) `xor` (x `and` z)) `xor` (y `and` z)

f : Fin 80 -> Bits 32 -> Bits 32 -> Bits 32 -> Bits 32
f t = if t <= 19 then ch
 else if t <= 39 then parity
 else if t <= 59 then maj
                 else parity

Σ256_0 : Bits 32 -> Bits 32
Σ256_0 x = (rotateRight 2 x `xor` rotateRight 13 x) `xor` rotateRight 22 x

Σ256_1 : Bits 32 -> Bits 32
Σ256_1 x = (rotateRight 6 x `xor` rotateRight 11 x) `xor` rotateRight 25 x

σ256_0 : Bits 32 -> Bits 32
σ256_0 x = (rotateRight 7 x `xor` rotateRight 18 x) `xor` shiftRightLogical x (intToBits 3)

σ256_1 : Bits 32 -> Bits 32
σ256_1 x = (rotateRight 17 x `xor` rotateRight 19 x) `xor` shiftRightLogical x (intToBits 10)

Σ512_0 : Bits 64 -> Bits 64
Σ512_0 x = (rotateRight 28 x `xor` rotateRight 34 x) `xor` rotateRight 39 x

Σ512_1 : Bits 64 -> Bits 64
Σ512_1 x = (rotateRight 14 x `xor` rotateRight 18 x) `xor` rotateRight 41 x

σ512_0 : Bits 64 -> Bits 64
σ512_0 x = (rotateRight 1 x `xor` rotateRight 8 x) `xor` shiftRightLogical x (intToBits 7)

σ512_1 : Bits 64 -> Bits 64
σ512_1 x = (rotateRight 19 x `xor` rotateRight 61 x) `xor` shiftRightLogical x (intToBits 6)

-- Constants

const1 : Vect 80 (Bits 32)
const1 = concat (map (replicate 20 . intToBits)
                     [0x5a827999, 0x6ed9eba1, 0x8f1bbcdc, 0xca62c1d6])

const256 : Vect 64 (Bits 32)
const256 = map intToBits
               [0x428a2f98, 0x71374491, 0xb5c0fbcf, 0xe9b5dba5, 0x3956c25b, 0x59f111f1, 0x923f82a4, 0xab1c5ed5,
                0xd807aa98, 0x12835b01, 0x243185be, 0x550c7dc3, 0x72be5d74, 0x80deb1fe, 0x9bdc06a7, 0xc19bf174,
                0xe49b69c1, 0xefbe4786, 0x0fc19dc6, 0x240ca1cc, 0x2de92c6f, 0x4a7484aa, 0x5cb0a9dc, 0x76f988da,
                0x983e5152, 0xa831c66d, 0xb00327c8, 0xbf597fc7, 0xc6e00bf3, 0xd5a79147, 0x06ca6351, 0x14292967,
                0x27b70a85, 0x2e1b2138, 0x4d2c6dfc, 0x53380d13, 0x650a7354, 0x766a0abb, 0x81c2c92e, 0x92722c85,
                0xa2bfe8a1, 0xa81a664b, 0xc24b8b70, 0xc76c51a3, 0xd192e819, 0xd6990624, 0xf40e3585, 0x106aa070,
                0x19a4c116, 0x1e376c08, 0x2748774c, 0x34b0bcb5, 0x391c0cb3, 0x4ed8aa4a, 0x5b9cca4f, 0x682e6ff3,
                0x748f82ee, 0x78a5636f, 0x84c87814, 0x8cc70208, 0x90befffa, 0xa4506ceb, 0xbef9a3f7, 0xc67178f2]

const512 : Vect 80 (Bits 64)
const512 = map intToBits
               [0x428a2f98d728ae22, 0x7137449123ef65cd, 0xb5c0fbcfec4d3b2f, 0xe9b5dba58189dbbc,
                0x3956c25bf348b538, 0x59f111f1b605d019, 0x923f82a4af194f9b, 0xab1c5ed5da6d8118,
                0xd807aa98a3030242, 0x12835b0145706fbe, 0x243185be4ee4b28c, 0x550c7dc3d5ffb4e2,
                0x72be5d74f27b896f, 0x80deb1fe3b1696b1, 0x9bdc06a725c71235, 0xc19bf174cf692694,
                0xe49b69c19ef14ad2, 0xefbe4786384f25e3, 0x0fc19dc68b8cd5b5, 0x240ca1cc77ac9c65,
                0x2de92c6f592b0275, 0x4a7484aa6ea6e483, 0x5cb0a9dcbd41fbd4, 0x76f988da831153b5,
                0x983e5152ee66dfab, 0xa831c66d2db43210, 0xb00327c898fb213f, 0xbf597fc7beef0ee4,
                0xc6e00bf33da88fc2, 0xd5a79147930aa725, 0x06ca6351e003826f, 0x142929670a0e6e70,
                0x27b70a8546d22ffc, 0x2e1b21385c26c926, 0x4d2c6dfc5ac42aed, 0x53380d139d95b3df,
                0x650a73548baf63de, 0x766a0abb3c77b2a8, 0x81c2c92e47edaee6, 0x92722c851482353b,
                0xa2bfe8a14cf10364, 0xa81a664bbc423001, 0xc24b8b70d0f89791, 0xc76c51a30654be30,
                0xd192e819d6ef5218, 0xd69906245565a910, 0xf40e35855771202a, 0x106aa07032bbd1b8,
                0x19a4c116b8d2d0c8, 0x1e376c085141ab53, 0x2748774cdf8eeb99, 0x34b0bcb5e19b48a8,
                0x391c0cb3c5c95a63, 0x4ed8aa4ae3418acb, 0x5b9cca4f7763e373, 0x682e6ff3d6b2b8a3,
                0x748f82ee5defb2fc, 0x78a5636f43172f60, 0x84c87814a1f0ab72, 0x8cc702081a6439ec,
                0x90befffa23631e28, 0xa4506cebde82bde9, 0xbef9a3f7b2c67915, 0xc67178f2e372532b,
                0xca273eceea26619c, 0xd186b8c721c0c207, 0xeada7dd6cde0eb1e, 0xf57d4f7fee6ed178,
                0x06f067aa72176fba, 0x0a637dc5a2c898a6, 0x113f9804bef90dae, 0x1b710b35131c471b,
                0x28db77f523047d84, 0x32caab7b40c72493, 0x3c9ebe0a15c9bebc, 0x431d67c49c100d4c,
                0x4cc5d4becb3e42b6, 0x597f299cfc657e2a, 0x5fcb6fab3ad6faec, 0x6c44198c4a475817]

-- Preprocessing

pad512 : Bits l -> Bits ((div l 512 + 1) * 512)
pad512 {l=l} message = append message
                              (append (intToBits 1)
                                      (append (the (Bits (modToNat (the (Mod 512) (448 - (natToMod l + 1))))) (intToBits 0))
                                              (the (Bits 64) (intToBits (cast l)))))

pad1024 : Bits l -> Bits ((div l 1024 + 1) * 1024)
pad1024 {l=l} message = append message
                               (append (intToBits 1)
                                       (append (the (Bits (modToNat (the (Mod 1024) (896 - (natToMod l + 1))))) (intToBits 0))
                                               (the (Bits 128) (intToBits (cast l)))))

parse512 : Bits (n * 512) -> Vect n (Bits 512)
parse512 = partition

parse1024 : Bits (n * 1024) -> Vect n (Bits 1024)
parse1024 = partition

-- Algorithms

data SecureHashAlgorithm1 : Type where
  SHA1 : Vect 5 (Bits 32) -> SecureHashAlgorithm1

vectIndex : (i : Nat) -> Vect (S n) a -> LTE i n -> a
vectIndex i v lte = index (natToFi i lte) v

sha1sched' : Vect 16 (Bits 32) -> Vect t (Bits 32) -> Bits 32
sha1sched' {t=t} M W =
  case isLTE t 15 of
    Yes lte => vectIndex t M lte
    No gt => rotateLeft 1 (foldl1 xor
                          --         (map (\off -> index (weakenN' (strMinus (natToFi t lteRefl) off)) W)
                          --              [3, 8, 14, 16]))
            [Vect.index (weakenN' (strMinus (natToFi t lteRefl)  3)) W,
             Vect.index (weakenN' (strMinus (natToFi t lteRefl)  8)) W,
             Vect.index (weakenN' (strMinus (natToFi t lteRefl) 14)) W,
             Vect.index (weakenN' (strMinus (natToFi t lteRefl) 16)) W])

-- NB: `foldl` doesn’t work here. Can we make something like `foldl`, but each
--      step is one element, and we get a Vect of elements back at the end?
sha1sched : Vect 16 (Bits 32) -> Vect 80 (Bits 32)
sha1sched mpart = foldl (\W, t => sha1sched' {t=t} mpart W) [] [0..79]

implementation Hash SecureHashAlgorithm1 512 160 where
  initialize _ = toList . parse512 . pad512 . Util.concat
  initialContext _ = SHA1 (map intToBits
                               [0x67452301,
                                0xefcdab89,
                                0x98badcfe,
                                0x10325476,
                                0xc3d2e1f0])
  updateContext (SHA1 v) block = SHA1 (zipWith plus (foldl for v [0..79]) v) where
    -- seems like we could do this in one pass
    W : Vect 80 (Bits 32)
    W = sha1sched (partition block)
    for : Vect 5 (Bits 32) -> Fin 80 -> Vect 5 (Bits 32)
    for [a, b, c, d, e] t =
      [Vect.foldl1 plus [rotateLeft 5 a, f t b c d, e, index t const1, index t W],
       a,
       rotateLeft 30 b,
       c,
       d]
  finalize (SHA1 v) = concat v

data SecureHashAlgorithm256 : Type where
  SHA256 : Vect 8 (Bits 32) -> SecureHashAlgorithm256

hash256 : Vect 8 (Bits 32) -> Bits 512 -> Vect 8 (Bits 32)

implementation Hash SecureHashAlgorithm256 512 256 where
  initialize _ = toList . parse512 . pad512 . Util.concat
  initialContext _ = SHA256 (map intToBits
                                 [0x6a09e667,
                                  0xbb67ae85,
                                  0x3c6ef372,
                                  0xa54ff53a,
                                  0x510e527f,
                                  0x9b05688c,
                                  0x1f83d9ab,
                                  0x5be0cd19])
  updateContext (SHA256 v) = SHA256 . hash256 v
  finalize (SHA256 v) = concat v

data SecureHashAlgorithm224 : Type where
  SHA224 : Vect 8 (Bits 32) -> SecureHashAlgorithm224

implementation Hash SecureHashAlgorithm224 512 224 where
  initialize _ = toList . parse512 . pad512 . Util.concat
  initialContext _ = SHA224 (map intToBits
                                 [0xc1059ed8,
                                  0x367cd507,
                                  0x3070dd17,
                                  0xf70e5939,
                                  0xffc00b31,
                                  0x68581511,
                                  0x64f98fa7,
                                  0xbefa4fa4])
  updateContext (SHA224 v) = SHA224 . hash256 v
  finalize (SHA224 v) = concat (take 7 v)

data SecureHashAlgorithm512 : Type where
  SHA512 : Vect 8 (Bits 64) -> SecureHashAlgorithm512

hash512 : Vect 8 (Bits 64) -> Bits 1024 -> Vect 8 (Bits 64)

implementation Hash SecureHashAlgorithm512 1024 512 where
  initialize _ = toList . parse1024 . pad1024 . Util.concat
  initialContext _ = SHA512 (map intToBits
                                 [0x6a09e667f3bcc908,
                                  0xbb67ae8584caa73b,
                                  0x3c6ef372fe94f82b,
                                  0xa54ff53a5f1d36f1,
                                  0x510e527fade682d1,
                                  0x9b05688c2b3e6c1f,
                                  0x1f83d9abfb41bd6b,
                                  0x5be0cd19137e2179])
  updateContext (SHA512 v) = SHA512 . hash512 v
  finalize (SHA512 v) = concat v

data SecureHashAlgorithm512_224 : Type where
  SHA512_224 : Vect 8 (Bits 64) -> SecureHashAlgorithm512_224

implementation Hash SecureHashAlgorithm512_224 1024 224 where
  initialize _ = toList . parse1024 . pad1024 . Util.concat
  initialContext _ = SHA512_224 (map intToBits
                                     [0x8C3D37C819544DA2,
                                      0x73E1996689DCD4D6,
                                      0x1DFAB7AE32FF9C82,
                                      0x679DD514582F9FCF,
                                      0x0F6D2B697BD44DA8,
                                      0x77E36F7304C48942,
                                      0x3F9D85A86A1D36C8,
                                      0x1112E6AD91D692A1])
  updateContext (SHA512_224 v) = SHA512_224 . hash512 v
  finalize (SHA512_224 v) = truncate (concat (take 4 v))

data SecureHashAlgorithm512_256 : Type where
  SHA512_256 : Vect 8 (Bits 64) -> SecureHashAlgorithm512_256

implementation Hash SecureHashAlgorithm512_256 1024 256 where
  initialize _ = toList . parse1024 . pad1024 . Util.concat
  initialContext _ = SHA512_256 (map intToBits
                                     [0x22312194FC2BF72C,
                                      0x9F555FA3C84C64C2,
                                      0x2393B86B6F53B151,
                                      0x963877195940EABD,
                                      0x96283EE2A88EFFE3,
                                      0xBE5E1E2553863992,
                                      0x2B0199FC2C85B8AA,
                                      0x0EB72DDC81C52CA2])
  updateContext (SHA512_256 v) = SHA512_256 . hash512 v
  finalize (SHA512_256 v) = concat (take 4 v)

data SecureHashAlgorithm384 : Type where
  SHA384 : Vect 8 (Bits 64) -> SecureHashAlgorithm384

implementation Hash SecureHashAlgorithm384 1024 384 where
  initialize _ = toList . parse1024 . pad1024 . Util.concat
  initialContext _ = SHA384 (map intToBits
                                 [0xcbbb9d5dc1059ed8,
                                  0x629a292a367cd507,
                                  0x9159015a3070dd17,
                                  0x152fecd8f70e5939,
                                  0x67332667ffc00b31,
                                  0x8eb44a8768581511,
                                  0xdb0c2e0d64f98fa7,
                                  0x47b5481dbefa4fa4])
  updateContext (SHA384 v) = SHA384 . hash512 v
  finalize (SHA384 v) = concat (take 6 v)

max_stars_repo_name: idris-hackers/idris-crypto

max_issues_repo_name: idris-hackers/idris-crypto

max_forks_repo_name: idris-hackers/idris-crypto


text:
module Language.LSP.CodeAction.AddClause

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.UnifyState
import Data.List
import Data.List1
import Data.String
import Idris.IDEMode.CaseSplit
import Idris.REPL.Opts
import Idris.Syntax
import Idris.Resugar
import Language.JSON
import Language.LSP.Message
import Libraries.Data.List.Extra
import Libraries.Data.PosMap
import Parser.Unlit
import Server.Configuration
import Server.Log
import Server.Utils
import TTImp.TTImp

buildCodeAction : URI -> List TextEdit -> CodeAction
buildCodeAction uri edits =
  let workspaceEdit = MkWorkspaceEdit { changes           = Just (singleton uri edits)
                                      , documentChanges   = Nothing
                                      , changeAnnotations = Nothing
                                      }
   in MkCodeAction { title       = "Add clause"
                   , kind        = Just RefactorRewrite
                   , diagnostics = Just []
                   , isPreferred = Just False
                   , disabled    = Nothing
                   , edit        = Just workspaceEdit
                   , command     = Nothing
                   , data_       = Nothing
                   }

export
addClause : Ref LSPConf LSPConfiguration
         => Ref MD Metadata
         => Ref Ctxt Defs
         => Ref UST UState
         => Ref Syn SyntaxInfo
         => Ref ROpts REPLOpts
         => CodeActionParams -> Core (Maybe CodeAction)
addClause params = do
  let True = params.range.start.line == params.range.end.line
    | _ => do logString Debug "addClause: start and end line were different"
              pure Nothing

  let line = params.range.start.line
  Just clause <- getClause (line + 1) (UN "")
    | Nothing => do logString Debug "addClause: not defined here"
                    pure Nothing

  let range = MkRange (MkPosition (line + 1) 0) (MkPosition (line + 1) 0)
  let edit = MkTextEdit range (clause ++ "\n")

  pure $ Just $ buildCodeAction params.textDocument.uri [edit]


text:
data Direction = North
               | East
               | South
               | West

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

||| Represents shapes
data Shape = ||| A triangle, with its base length and height
             Triangle Double Double
           | ||| A rectangle, with its length and height
             Rectangle Double Double
           | ||| A circle, with its radius
             Circle Double

area : Shape -> Double
area (Triangle base height) = 0.5 * base * height
area (Rectangle length height) = length * height
area (Circle radius) = pi * radius * radius

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

rectangle : Picture
rectangle = Primitive (Rectangle 20 10)

circle : Picture
circle = Primitive (Circle 5)

triangle : Picture
triangle = Primitive (Triangle 10 10)

testPicture : Picture
testPicture = Combine (Translate 5 5 rectangle)
              (Combine (Translate 35 5 circle)
              (Translate 15 25 triangle))

%name Shape shape, shape1, shape2
%name Picture pic, pic1, pic2

pictureArea : Picture -> Double
pictureArea (Primitive shape) = area shape
pictureArea (Combine pic pic1) = pictureArea pic + pictureArea pic1
pictureArea (Rotate x pic) = pictureArea pic
pictureArea (Translate x y pic) = pictureArea pic

data Biggest = NoTriangle | Size Double

computeTriangle : (shape : Shape) -> Biggest
computeTriangle (Triangle x y) = Size (0.5 * x * y)
computeTriangle (Rectangle x y) = NoTriangle
computeTriangle (Circle x) = NoTriangle

findBigger : Biggest -> Biggest -> Biggest
findBigger NoTriangle NoTriangle = NoTriangle
findBigger NoTriangle (Size x) = (Size x)
findBigger (Size x) NoTriangle = (Size x)
findBigger (Size x) (Size y) = if x >= y then (Size x)
                                         else (Size y)

biggestTriangle : Picture -> Biggest
biggestTriangle (Primitive shape) = computeTriangle shape
biggestTriangle (Combine pic pic1) = findBigger (biggestTriangle pic) (biggestTriangle pic1)
biggestTriangle (Rotate x pic) = biggestTriangle pic
biggestTriangle (Translate x y pic) = biggestTriangle pic

triangle1 : Picture
triangle1 = Primitive (Triangle 50 50)

triangle2 : Picture
triangle2 = Primitive (Triangle 10 10)

triangle3 : Picture
triangle3 = Primitive (Triangle 1 1)

testPicture2 : Picture
testPicture2 = Combine (Translate 5 5 triangle1)
              (Combine (Translate 35 5 triangle2)
              (Translate 15 25 triangle3))


text:
module Server.InigoServer.KVOps

import Inigo.Async.Promise

import Data.List
import Data.Maybe
import Data.SortedSet as Set
import Extra.String
import Fmt
import Inigo.Account.Account as Account
import Inigo.Async.Base
import Inigo.Async.CloudFlare.KV
import Inigo.Async.SubtleCrypto.SubtleCrypto
import Inigo.Package.Package
import Inigo.Package.PackageDeps
import Inigo.Package.PackageIndex
import SemVar.Data
import Server.InigoServer.Util

||| TODO: Should package technically be a list of strings?
||| TODO: We should be able to rebuild if any of the redundant stores becomes corrupted

sessionTTL : Int
sessionTTL = 60 * 60 * 24 * 10 -- 10 days

packageIndexKey : (String, String)
packageIndexKey = ("index", "index")

packageKey : String -> String -> Version -> (String, String)
packageKey ns package version = ("packages", fmt "%s.%s@%s" ns package (show version))

readmeKey : String -> String -> Version -> (String, String)
readmeKey ns package version = ("readme", fmt "%s.%s@%s" ns package (show version))

archiveKey : String -> String -> Version -> (String, String)
archiveKey ns package version = ("archives", fmt "%s.%s@%s" ns package (show version))

packageDepKey : String -> String -> (String, String)
packageDepKey ns package = ("deps", fmt "%s.%s" ns package)

accountKey : String -> (String, String)
accountKey ns = ("accounts", ns)

sessionKey : String -> (String, String)
sessionKey session = ("sessions", session)

pkgVerKey : Package -> (String -> String -> Version -> a) -> a
pkgVerKey pkg f =
  f (ns pkg) (package pkg) (version pkg)

pkgKey : Package -> (String -> String -> a) -> a
pkgKey pkg f =
  f (ns pkg) (package pkg)

read : (String, String) -> Promise (Maybe String)
read key =
  do
    res <- (uncurry KV.read key)
    if res == ""
      then pure $ Nothing
      else pure $ Just res

write : (String, String) -> String -> Promise ()
write key val = (uncurry KV.write key) val

writeTTL : (String, String) -> String -> Int -> Promise ()
writeTTL key val ttl = (uncurry KV.writeTTL key) val ttl

export
readIndex : Promise PackageIndex
readIndex =
  do
    indexRes <- read packageIndexKey
    log ("Package Index: " ++ show indexRes)
    expectResult $ fromMaybe (Right []) $ map parsePackageIndex indexRes

export
writeIndex : PackageIndex -> Promise ()
writeIndex index =
  write packageIndexKey (encodePackageIndex index)

export
readArchive : String -> String -> Version -> Promise (Maybe String)
readArchive packageNS packageName version =
  read (archiveKey packageNS packageName version)

export
writeArchive : String -> String -> Version -> String -> Promise ()
writeArchive packageNS packageName version body =
  write (archiveKey packageNS packageName version) body

export
readReadme : String -> String -> Version -> Promise (Maybe String)
readReadme packageNS packageName version =
  read (readmeKey packageNS packageName version)

export
writeReadme : String -> String -> Version -> String -> Promise ()
writeReadme packageNS packageName version body =
  write (readmeKey packageNS packageName version) body

-- TODO: This logic is a little complex to be here
export
readAllDeps : String -> String -> Promise (List (List String, PackageDeps))
readAllDeps packageNS packageName =
  readAllDeps_ Set.empty [packageNS, packageName]
  where
    readDep : List String -> Promise PackageDeps
    readDep [packageNS, packageName] =
      do
        depsRes <- read (packageDepKey packageNS packageName)
        log ("Package Deps: " ++ show depsRes)
        expectResult $ fromMaybe (Right []) $ map parsePackageDeps depsRes

    readDep els =
      reject ("Invalid package name: " ++ show els)

    readAllDeps_ : SortedSet (List String) -> List String -> Promise (List (List String, PackageDeps))
    readAllDeps_ curr q =
      do
        packageDeps <- readDep q
        let allDeps = concat $ map (\(_, packageDep) => deps packageDep ++ dev packageDep) packageDeps
        let subDeps = foldl (\acc, (pkgName, _) => Set.insert pkgName acc) (the (SortedSet (List String)) Set.empty) allDeps
        let newDeps = difference subDeps curr
        let nextSet = Set.insert q curr
        res <- all $ map (readAllDeps_ (union nextSet newDeps)) (Set.toList newDeps)
        pure $ (q, packageDeps) :: (concat res)

export
readDeps : Package -> Promise PackageDeps
readDeps pkg =
  do
    depsRes <- read (pkgKey pkg packageDepKey)
    log ("Package Deps: " ++ show depsRes)
    expectResult $ fromMaybe (Right []) $ map parsePackageDeps depsRes

export
writeDeps : Package -> PackageDeps -> Promise ()
writeDeps pkg packageDeps =
  write (pkgKey pkg packageDepKey) (encodePackageDeps packageDeps)

export
writePackage : Package -> Promise ()
writePackage pkg =
  write (pkgVerKey pkg packageKey) (encodePackage pkg)

export
readPackage : String -> String -> Version -> Promise (Either String Package)
readPackage packageNS packageName version =
  do
    Just contents <- read (packageKey packageNS packageName version)
      | Nothing => pure $ Left "package not found"
    pure $ parsePackage contents

export
readVersions : String -> String -> Promise (List Version)
readVersions packageNS packageName =
  do
    depsRes <- read (packageDepKey packageNS packageName)
    deps <- expectResult $ fromMaybe (Right []) $ map parsePackageDeps depsRes
    pure $ map fst deps

export
latestVersion : String -> String -> Promise (Maybe Version)
latestVersion packageNS packageName =
  do
    versions <- readVersions packageNS packageName
    pure $ head' $ reverse $ sort $ versions --'

-- Note: there could be race conditions, and since this
--       is EV, it would be difficult to prevent overall
-- TODO: Validate account details on server-side
export
newAccount : Account -> Promise (Maybe (Int, String))
newAccount account =
  do
    Nothing <- read (accountKey (ns account))
      | Just _ => pure $ Just (400, "account already exists")
    write (accountKey (ns account)) (encode account)
    pure Nothing

export
readAccountHash : String -> Promise (Maybe (Algorithm, String))
readAccountHash ns =
  do
    Just accountToml <- read (accountKey ns)
      | Nothing => pure Nothing
    let Just account = Account.decode accountToml
      | Nothing => pure Nothing
    pure (Just $ (kdf account, hash account))

export
readSession : String -> Promise (Maybe String)
readSession session =
  read (sessionKey session)

||| TODO: write session should have an expiration
export
writeSession : String -> String -> Promise ()
writeSession session ns =
  writeTTL (sessionKey session) ns sessionTTL

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Range

%access public export
%default total

||| Generic Type for Non-inclusive, ordered ranges
data Range : Type -> a -> a -> Type where
  MkRange : (Ord a) =>
            (min : a) ->
            (max : a) ->
            { auto prf : Dec( min < max = True ) } ->
            Range a min max

inRange : Range t a b -> (value : t) -> Type
inRange (MkRange a b) y = Dec (a < y = y < b)

interface Distance a b where
  distance : Range { a = a } t x y -> b

max_stars_repo_name: ostera/idris-coda

max_issues_repo_name: ostera/idris-coda

max_forks_repo_name: ostera/idris-coda


text:
module BinaryFormats.Data.List

%default total

export
trySplitAt : {a : Type} -> Nat -> List a -> Maybe (List a, List a)
trySplitAt offset bits =
    toMaybe (length bits < offset) (splitAt offset bits)

export
tryDrop : {a : Type} -> Nat -> List a -> Maybe (List a)
tryDrop offset bits =
    toMaybe (length bits < offset) (drop offset bits)

max_stars_repo_name: brendanzab/idris-power-of-pi

max_issues_repo_name: brendanzab/idris-power-of-pi

max_forks_repo_name: brendanzab/idris-power-of-pi


text:
module SignedSetoid
import SignedInt
import Setoid

%default total
%access public export

signedReflx : Reflx SignedEq
signedReflx (SInt p n) = SignedRefl Refl

signedSymm : Symm SignedEq
signedSymm (SInt p1 n1) (SInt p2 n2) (SignedRefl sr) = SignedRefl (sym sr)

signedTrans : Trans SignedEq
signedTrans (SInt p1 n1) (SInt p2 n2) (SInt p3 n3) (SignedRefl sr12) (SignedRefl sr23) = SignedRefl sr13
  where
    _1 : (p1 + n2) + (p2 + n3) = ((p2 + n1) + p3) + n2
    _1  = trans (rewrite sr12 in rewrite sr23 in Refl) (plusAssociative (p2 + n1) p3 n2)

    _2 : ((p2 + n3) + p1) + n2 = (p1 + n2) + (p2 + n3)
    _2 = trans (sym (plusAssociative (p2 + n3) p1 n2)) (sym (plusCommutative (p1 + n2) (p2 + n3)))

    _3 : (p2 + n3) + p1 = (p2 + n1) + p3
    _3 = plusRightCancel _ _ n2 (trans _2 _1)

    _4 : (n3 + p1) + p2 = (p2 + n3) + p1
    _4 = trans (plusCommutative (n3 + p1) p2) (plusAssociative p2 n3 p1)

    _5 : (p2 + n1) + p3 = (n1 + p3) + p2
    _5 = sym (trans (plusCommutative (n1 + p3) p2) (plusAssociative p2 n1 p3))

    _6 : n3 + p1 = n1 + p3
    _6 = plusRightCancel _ _ p2 (trans (trans _4 _3) _5)

    sr13 : p1 + n3 = p3 + n1
    sr13 = trans (trans (plusCommutative p1 n3) _6) (plusCommutative n1 p3)

SignedSetoid : Setoid
SignedSetoid = MkSetoid SignedInt SignedEq (EqProof SignedEq signedReflx signedSymm signedTrans)


text:
||| Basic types of IO Handle
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module System.IO.Handle.Types

%default total

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

public export data Permission = Readable | Writable
public export
Eq Permission where
  Readable == Readable = True
  Writable == Writable = True
  _ == _ = False

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