text:
module Control.Monad.Managed

import Control.Monad.Trans
import Control.Monad.State
import Control.Monad.Either

import System.File

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

-- See README.md

{-
Given some:

example : MonadManaged m => EitherT e m a

Your typical use will likely end up looking like this:
main = runManaged $ do
    Right x <- runEitherT example
      | Left y => ...
    ...
-- More examples at module bottom
-}
-------------------------------------------------

export
data Managed : Type -> Type where
  MkManaged : (1 _ : forall b. (a -> IO b) -> IO b) -> Managed a

getManaged : Managed a -> (forall b. (a -> IO b) -> IO b)
getManaged (MkManaged g) = g

export
%inline
managed : (1 _ : forall r. (a -> IO r) -> IO r) -> Managed a
managed = MkManaged

export
managed_ : (forall r. IO r -> IO r) -> Managed ()
managed_ f = managed $ \g => f (g ())

export
||| This can let you leak the resource through r, be very wary!
||| Best to avoid using.
manageWith : Managed a -> (a -> IO r) -> IO r
manageWith m = getManaged m

export
runManaged : Managed () -> IO ()
runManaged (MkManaged g) = g pure

public export
implementation Functor Managed where
  map f g = MkManaged $ \bmr => getManaged g (\a => bmr (f a))

public export
implementation Applicative Managed where
  pure x = MkManaged (\amr => amr x)
  f <*> x = MkManaged $ \bmr =>
   getManaged f (\ab => getManaged x (\a => bmr (ab a)))

public export
implementation Monad Managed where
  x >>= k = MkManaged $ \bmr => getManaged x (\a => getManaged (k a) bmr)

public export
Semigroup a => Semigroup (Managed a) where
  x <+> y = [| x <+> y |]

public export
Monoid a => Monoid (Managed a) where
  neutral = pure neutral

public export
implementation HasIO Managed where
  liftIO io = MkManaged (io >>=)

public export
interface HasIO m => MonadManaged m where
  use : Managed a -> m a -- bad name

public export
MonadManaged Managed where
  use = id

public export
MonadManaged m => MonadManaged (StateT s m) where
  use x = lift (use x)

public export
MonadManaged m => MonadManaged (EitherT e m) where
  use x = lift (use x)

-- Not in stdlib just yet
withFile' : HasIO io => String -> Mode -> (Either FileError File -> io a) -> io a
withFile' file mode act = do res <- openFile file mode
                             a <- act res
                             either (\_ => pure a)
                                    (\f => pure a <* closeFile f) res

managedFile : String -> Mode -> Managed (Either FileError File)
managedFile file mode = managed (withFile' file mode)

example : MonadManaged m => EitherT FileError m Nat
example = do f <- MkEitherT $ use (managedFile "/dev/urandom" Read)
             r <- MkEitherT $ liftIO $ fGetChars f 20
             pure (length r) -- '\0' ends Strings, this probably won't be 20!

example_main : IO ()
example_main = runManaged $ do
    Right x <- runEitherT example
      | Left y => liftIO (printLn y)
    putStrLn $ show x ++ " chars read from /dev/urandom"

ordering_test : IO ()
ordering_test = runManaged $ do
    managed $ (\f => f () <* printLn "release one")
    printLn 1
    managed $ (\f => f () <* printLn "release two")
    printLn 2
    managed $ (\f => f () <* printLn "release three")
    printLn 3
{-
   Assuming you've written your Managed action in a manner that 'releases' last,
   release is in reverse order of binding:
   :exec ordering_test
   1
   2
   3
   "release three"
   "release two"
   "release one"
-}


text:
module Data.Pair.Predicates

%default total
%access public export

data PairEq : (prfSame : a -> a -> Type)
               -> (l : (a,a))
               -> (r : (a,a))
               -> Type
  where
    AreSame : (ad : prfSame a d)
           -> (bc : prfSame b c)
           -> PairEq prfSame (a,b) (c,d)

fsNotSame : (decEq : (x : a) -> (y : a) -> Dec (prfSame x y))
         -> (contra : prfSame a1 d -> Void)
         -> PairEq prfSame (a1, b) (c, d)
         -> Void
fsNotSame decEq contra (AreSame ad bc) = contra ad

sfNotSame : (decEq : (x : a) -> (y : a) -> Dec (prfSame x y))
         -> (contra : prfSame b c -> Void)
         -> PairEq prfSame (a1, b) (c, d)
         -> Void
sfNotSame decEq contra (AreSame ad bc) = contra bc

pairEq : {a : Type}
      -> {prfSame : a -> a -> Type}
      -> (decEq : (x,y : a) -> Dec (prfSame x y))
      -> (l,r : Pair a a)
      -> Dec (PairEq prfSame l r)
pairEq decEq (a, b) (c, d) with (decEq a d)
  pairEq decEq (a, b) (c, d) | (Yes prfAD) with (decEq b c)
    pairEq decEq (a, b) (c, d) | (Yes prfAD) | (Yes prfBC) = Yes (AreSame prfAD prfBC)
    pairEq decEq (a, b) (c, d) | (Yes prfAD) | (No contra) = No (sfNotSame decEq contra)

  pairEq decEq (a, b) (c, d) | (No contra) = No (fsNotSame decEq contra)

ext: idr


text:
module RunIO

%default total

data RunIO : Type -> Type where
     Quit : a -> RunIO a
     Do : IO a -> (a -> Inf (RunIO b)) -> RunIO b

data Fuel = Dry | More (Lazy Fuel)

(>>=) : IO a -> (a -> Inf (RunIO b)) -> RunIO b
(>>=) = Do

run : Fuel -> RunIO a -> IO (Maybe a)
run f (Quit v) = pure $ Just v
run Dry p = pure Nothing
run (More x) (Do a f) = do res <- a
                           run x $ f res

greet : RunIO ()
greet = do putStr "Thy name: "
           name <- getLine
           case name == "" of
                False => putStrLn ("Hello " ++ show name) >>= \_ => greet
                True => putStrLn "Ciao" >>= \_ => Quit ()

partial
forever : Fuel
forever = More forever

partial
main : IO ()
main = do run forever greet
          pure ()

max_stars_repo_path: Chapter 11/RunIO.idr

max_issues_repo_path: Chapter 11/RunIO.idr

max_forks_repo_path: Chapter 11/RunIO.idr


text:
-- Idris2

import System
import System.Concurrency

-- Test `conditionSignal` wakes 1 thread for 1 main and N child threads

main : IO ()
main =
  let n = 3 in
  do cvMutex <- makeMutex
     cv <- makeCondition
     ts <- for [1..n] $ \_ => fork $ do mutexAcquire cvMutex
                                        conditionWait cv cvMutex
                                        putStrLn "Hello mother"
                                        mutexRelease cvMutex
     putStrLn "Hello child"
     sleep 1
     conditionSignal cv
     -- don't threadWait since we don't know which thread got signalled
     sleep 1


text:
module GeneralRec

-- https://personal.cis.strath.ac.uk/conor.mcbride/TotallyFree.pdf
-- http://okmij.org/ftp/Haskell/extensible/more.pdf

data Freer : (f : Type -> Type) -> Type -> Type where
  Pure : a -> Freer f a
  Bind : f a -> (a -> Freer f b) -> Freer f b

(>>=) : Freer f a -> (a -> Freer f b) -> Freer f b
(>>=) (Pure x) f = f x
(>>=) (Bind x g) f = Bind x (\a => g a >>= f)

data General : (f : a -> Type) -> Type -> Type where
  Rec : (x : a) -> General f (f x)

PiG : (s : Type) -> (f : s -> Type) -> Type
PiG s f = (x : s) -> Freer (General f) (f x)

call : (x : a) -> Freer (General f) (f x)
call x = Bind (Rec x) Pure

runGeneral : {f : a -> Type} -> ((x : a) -> f x) -> Freer (General f) c -> c
runGeneral rec (Pure x) = x
runGeneral rec (Bind (Rec x) k) = runGeneral rec $ k (rec x)

run : {f : a -> Type} -> PiG a f -> (x : a) -> f x
run f x = runGeneral (run f) (f x)

fusc : PiG Nat (\_ => Nat)
fusc Z = Pure Z
fusc (S n) = do fn <- call n
                ffn <- call fn
                Pure $ S ffn

test : Nat
test = run fusc 10

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module CIL.FFI.Single

import public CIL.FFI

%access public export

SingleTy : CILTy
SingleTy = CILTyVal "" "float32"

Single : Type
Single = CIL SingleTy

%extern prim__singleAdd : Single -> Single -> Single
%extern prim__singleSub : Single -> Single -> Single
%extern prim__singleMul : Single -> Single -> Single
%extern prim__singleFromInteger : Integer -> Single
%extern prim__singleFromInt : Int -> Single
%extern prim__singleFromDouble : Double -> Single
%extern prim__singleNeg : Single -> Single
%extern prim__singleAbs : Single -> Single
%extern prim__singleDiv : Single -> Single -> Single
%extern prim__singleCompare : Single -> Single -> Int
%extern prim__singleMax : Single -> Single -> Single
%extern prim__singleMin : Single -> Single -> Single
%extern prim__singleShow : Single -> String

implementation Num Single where
  (+) = prim__singleAdd
  (*) = prim__singleMul
  fromInteger = prim__singleFromInteger

implementation Neg Single where
  negate = prim__singleNeg
  (-) = prim__singleSub

implementation Abs Single where
  abs = prim__singleAbs

implementation Fractional Single where
  (/) = prim__singleDiv

implementation Eq Single where
  (==) x y = prim__singleCompare x y == 0

implementation Ord Single where
  compare x y =
    let ord = prim__singleCompare x y
    in if (ord == 0) then EQ else (if ord < 0 then LT else GT)
  (<) x y = prim__singleCompare x y < 0
  (>) x y = prim__singleCompare x y > 0
  (<=) x y = prim__singleCompare x y <= 0
  (>=) x y = prim__singleCompare x y >= 0
  max = prim__singleMax
  min = prim__singleMin

implementation Show Single where
  show = prim__singleShow

implementation Cast Double Single where
  cast = prim__singleFromDouble

implementation Cast Integer Single where
  cast = prim__singleFromInteger

implementation Cast Int Single where
  cast = prim__singleFromInt

single : Double -> Single
single = cast

max_stars_repo_name: alaendle/idris-cil

max_issues_repo_name: alaendle/idris-cil

max_forks_repo_name: alaendle/idris-cil


text:
module Language.LSP.DocumentSymbol

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.Name
import Data.List
import Idris.Doc.String
import Language.LSP.Message
import Libraries.Data.NameMap
import Server.Configuration
import Server.Log
import Server.Utils

-- NOTE: Structured information should be rendereded from the actual Term of the expressions
-- in a file, that would give a better high-level overview. For now this is more like a placeholder
-- rather than a useful functionality.
-- NOTE: Global symbols considered as functions, meta symbols considered as Variables.

||| Check if the name is visible in the local namespaces, if yes return Just its full name, otherwise Nothing.
||| This function meant to be used with GlobalNames.
checkVisibleName : Ref Ctxt Defs => List Namespace -> Name -> Core (Maybe Name)
checkVisibleName namespaces name = do
  fullName <- toFullNames name
  let True = isUserName fullName
    | False => pure Nothing
  let (Just fullNamespace, _) = displayName fullName
    | _ => pure Nothing
  pure $ if elem fullNamespace namespaces then Just fullName else Nothing

||| Check if the name is visible and returns the associated NonEmpty location.
currentNSNameWithLoc : Ref Ctxt Defs => List Namespace -> Name -> Core (Maybe (Name, FilePos, FilePos))
currentNSNameWithLoc namespaces name = do
  Just visibleName <- checkVisibleName namespaces name
    | Nothing => pure Nothing
  defs <- get Ctxt
  Just gdef <- lookupCtxtExact visibleName defs.gamma
    | Nothing => pure Nothing
  pure $ case gdef.location of
    EmptyFC                 => Nothing
    MkFC        _ start end => Just (gdef.fullname, start, end)
    MkVirtualFC _ start end => Just (gdef.fullname, start, end)

buildSymbolInformation : Name -> URI -> FileRange -> SymbolKind -> Bool -> SymbolInformation
buildSymbolInformation n uri range kind deprecated = MkSymbolInformation
  { name = show $ dropNS n
  , kind = kind
  , tags = if deprecated then Just [Deprecated] else Nothing
  , deprecated = Nothing
  , location = MkLocation uri (cast range)
  , containerName = Nothing
  }

||| Render all names form Meta and current namespace matching Global names as SymbolInformation.
||| The LSP client needs to handle the SymbolInformations correctly.
export
documentSymbol : Ref Ctxt Defs
              => Ref MD Metadata
              => Ref LSPConf LSPConfiguration
              => DocumentSymbolParams -> Core (List SymbolInformation)
documentSymbol params = do
  logI DocumentSymbol "Making for \{show params.textDocument.uri}"
  Just (uri, _) <- gets LSPConf openFile
    | Nothing => logE DocumentSymbol "No open file" >> pure []
  let True = uri == params.textDocument.uri
    | False => do
        logD DocumentSymbol "Expected request for the currently opened file \{show uri}, instead received \{show params.textDocument.uri}"
        pure []
  defs <- get Ctxt
  -- Get the current and visible namespaces from the context
  let currentNamespaces = defs.currentNS :: defs.nestedNS
  -- Get all resolved names, which are in the visible namesspaces
  let knownNames = NameMap.keys $ namesResolvedAs defs.gamma
  -- Render global and meta names as SymbolInformation
  visibleNames <- map catMaybes $ traverse (currentNSNameWithLoc currentNamespaces) knownNames
  let globalDocSymbols = map (\(n, range) => buildSymbolInformation n uri range Function False) visibleNames
  meta <- get MD
  let metaDocSymbols = map (\((_, range), (metaName, _, _)) => buildSymbolInformation metaName uri range Variable False) meta.names
  let docSymbols = globalDocSymbols ++ metaDocSymbols
  logI DocumentSymbol "Found \{show (length globalDocSymbols)} global and \{show (length metaDocSymbols)} meta document symbols."
  pure $ docSymbols


text:
module Dart.FFI

import public System.FFI
import public Dart.FFI.Constructors
import public Dart.FFI.Enums
import public Dart.FFI.Types
import public Dart.FFI.Upcast


text:
module Main

import System
import Data.Vect

data VectUnknown : Type -> Type where
     MkUnknownVect : (len : Nat) -> Vect len a -> VectUnknown a

Show (VectUnknown String) where
     show (MkUnknownVect len v) = show v

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

readNumber : String -> Maybe Nat
readNumber input = case all isDigit (unpack input) of
                   False => Nothing
                   True => Just (cast input)

readVectLen : (len : Nat) -> IO (Vect len String)
readVectLen Z = pure []
readVectLen (S k) = do x <- getLine
                       xs <- readVectLen k
                       pure (x :: xs)

EmptyUnlimitedVect : VectUnknown String
EmptyUnlimitedVect = (MkUnknownVect _ [])

unlimitedVectLen' : VectUnknown String -> IO (VectUnknown String)
unlimitedVectLen' (MkUnknownVect len v) = do x <- getLine
                                             if ( x == "") then pure (MkUnknownVect _ v)
                                                           else unlimitedVectLen' (MkUnknownVect _ (x :: v))

unlimitedVectPrint : VectUnknown String -> IO ()
unlimitedVectPrint x = do (printLn x)

||| (>>=) (unlimitedVectLen' EmptyUnlimitedVect) (\v => unlimitedVectPrint v)
unlimitedVectTest : IO ()
unlimitedVectTest = do putStrLn "Enter the sequentially strings and press Enter when input will be completed:"
                       v <- (unlimitedVectLen' EmptyUnlimitedVect)
                       unlimitedVectPrint v

readVect' : IO (n : Nat ** Vect n String)
readVect' = do x <- getLine
               if (x == "") then pure (_ ** [])
                            else do (n' ** xs) <- readVect'
                                    pure ((S n') ** (x :: xs))

mypair : (Int, String)
mypair = (94, "Pages")

anyVect : (n : Nat ** Vect n String)
anyVect = (3 ** ["Rod", "Jane", "Freddy"])

zipInputs : IO ()
zipInputs = do putStrLn "Input first vector: "
               (len1 ** xs) <- readVect'
               putStrLn "Input second vector: "
               (len2 ** ys) <- readVect'
               case exactLength len1 ys of
                    Nothing => putStrLn ("Vectors has been with equal length. " ++ (show len1) ++ " != " ++ (show len2))
                    Just zs => printLn (zip xs zs)

AdderType : (numargs : Nat) -> Type
AdderType Z = Int
AdderType (S k) = (next : Int) -> AdderType k

adder : (numargs : Nat) -> (acc : Int) -> AdderType numargs
adder Z acc = acc
adder (S k) acc = \next => adder k  (next + acc)

main : IO ()
main = do
     x <- getLine
     case readNumber x of
          Nothing => putStrLn ("Wrong input: " ++ (the String x))
          Just n => putStrLn ("Number is " ++ (show n))


text:
module Data.Vect.Sort

import Data.Vect
import Data.Nat.Views

mutual
  sortBySplit : (n : Nat) -> (a -> a -> Ordering) -> Vect n a -> Vect n a
  sortBySplit Z cmp [] = []
  sortBySplit (S Z) cmp [x] = [x]
  sortBySplit n cmp xs with (half n)
    sortBySplit (k + k) cmp xs     | HalfEven k = sortByMerge k k cmp xs
    sortBySplit (S (k + k)) cmp xs | HalfOdd k = sortByMerge (S k) k cmp xs

  sortByMerge : (n : Nat) -> (m : Nat) -> (a -> a -> Ordering) -> Vect (n + m) a -> Vect (n + m) a
  sortByMerge n m cmp xs =
    let (left, right) = splitAt n xs in
      mergeBy cmp
        (sortBySplit n cmp (assert_smaller xs left))
        (sortBySplit m cmp (assert_smaller xs right))

||| Merge sort implementation for Vect n a
export total
sortBy : {n : Nat} -> (cmp : a -> a -> Ordering) -> (xs : Vect n a) -> Vect n a
sortBy {n} cmp xs = sortBySplit n cmp xs

export total
sort : Ord a => {n : Nat} -> Vect n a -> Vect n a
sort = sortBy compare


text:
import Data.List
import Data.List1
import Data.SortedMap as M
import Data.String.Parser

import System.File

data Cave = Large String | Small String

Eq Cave where
  (Large x) == (Large y) = x == y
  (Small x) == (Small y) = x == y
  _ == _ = False

isSmall : Cave -> Bool
isSmall (Small _) = True
isSmall _ = False

getName : Cave -> String
getName (Large x) = x
getName (Small x) = x

Show Cave where
  show = getName

Ord Cave where
  compare c1 c2 = compare (getName c1) (getName c2)

data Edge : Type where
  CaveEdge : Cave -> Cave -> Edge
  StartFrom : Cave -> Edge
  ToEnd : Cave -> Edge

Show Edge where
  show (CaveEdge x y) = getName x ++ "-" ++ getName y
  show (StartFrom x) = "start-" ++ getName x
  show (ToEnd x) = "end-" ++ getName x

EdgeMap : Type
EdgeMap = SortedMap Cave (List Cave)

record Caves where
  constructor MkCaves
  start : List Cave
  edges : EdgeMap
  end : List Cave

emptyCaves : Caves
emptyCaves = MkCaves [] empty []

lookupCave : Cave -> Caves -> List Cave
lookupCave c cs = maybe [] id $ M.lookup c $ cs.edges

isStart : Cave -> Caves -> Bool
isStart c caves = elem c (caves.start)

caveParser : Parser Cave
caveParser = (Small <$> takeWhile1 isLower) <|> (Large <$> takeWhile1 isUpper)

caveEdgeParser : Parser Edge
caveEdgeParser = do c1 <- caveParser
                    token "-"
                    c2 <- caveParser
                    pure $ CaveEdge c1 c2

startParser : Parser Edge
startParser =
  (token "start" *> token "-" *> StartFrom <$> caveParser) <|>
  (StartFrom <$> caveParser <* token "-" <* token "start")

endParser : Parser Edge
endParser =
  (token "end" *> token "-" *> ToEnd <$> caveParser) <|>
  (ToEnd <$> caveParser <* token "-" <* token "end")

parser : Parser (List Edge)
parser = some ((startParser <|> endParser <|> caveEdgeParser) <* spaces)

insertCave : Cave -> Cave -> EdgeMap -> EdgeMap
insertCave from to m = case lookup from m of
                            Just l  => insert from (to :: l) m
                            Nothing => insert from [to] m

toCaveMap : List Edge -> Caves -> Caves
toCaveMap [] = id
toCaveMap ((CaveEdge x y) :: xs) =
  toCaveMap xs . { edges $= insertCave y x . insertCave x y }
toCaveMap ((StartFrom x) :: xs) = toCaveMap xs . { start $= (::) x }
toCaveMap ((ToEnd x) :: xs) = toCaveMap xs . { end $= (::) x }

hasDuplicate : Eq a => List a -> Bool
hasDuplicate [] = False
hasDuplicate (x :: xs) = hasDuplicate' x xs
  where
    hasDuplicate' : a -> List a -> Bool
    hasDuplicate' y [] = False
    hasDuplicate' y (x :: xs) = y == x || hasDuplicate' x xs

mayVisit : List Cave -> Cave -> Bool
mayVisit l (Large _) = True
mayVisit l c@(Small _) = not (elem c l) || not (hasDuplicate $ sort $ filter isSmall $ l) -- this is second part

mutual
  path : Caves -> List1 Cave -> List (List1 Cave)
  path caves p@(c ::: cs) = let ps = paths' caves $ (\x => cons x p) <$> (filter (mayVisit (c :: cs)) $ lookupCave c caves) in
                                if isStart c caves
                                   then p :: ps
                                   else ps

  paths' : Caves -> List (List1 Cave) -> List (List1 Cave)
  paths' caves ps = join $ path caves <$> ps

paths : Caves -> List (List1 Cave)
paths c = paths' c (singleton <$> c.end)

run : String -> IO ()
run s = do Right (edges, _) <- pure $ parse parser s
             | Left err => putStrLn $ show err
           let caves = toCaveMap edges emptyCaves
           putStrLn $ show $ length $ paths caves

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


text:
> module Fun.Properties

> import Syntax.PreorderReasoning

> import Fun.Operations
> import Fun.Predicates
> import Pair.Properties
> import Finite.Predicates

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

> ||| Functionality of dependent functions
> functionality : {A : Type} -> {B : A -> Type} ->
>                 {f : (a : A) -> B a} -> {g : (a : A) -> B a} ->
>                 f = g -> (a : A) -> f a = g a
> functionality Refl x = Refl

> ||| Injectivity (one direction)
> Injective1 : {A, B : Type} -> (f : A -> B) -> Type
> Injective1 {A} f = (a1 : A) -> (a2 : A) -> f a1 = f a2 -> a1 = a2

> ||| Injectivity (the other direction)
> Injective2 : {A, B : Type} -> (f : A -> B) -> Type
> Injective2 {A} f = (a1 : A) -> (a2 : A) -> Not (a1 = a2) -> Not (f a1 = f a2)

> ||| Non injectivity, constructive
> NonInjective : {A, B : Type} -> (f : A -> B) -> Type
> NonInjective f = Exists (\ a1 => Exists (\ a2 => (Not (a1 = a2) , f a1 = f a2)))

> ||| Surjectivity
> Surjective : {A, B : Type} -> (f : A -> B) -> Type
> Surjective {B} f = (b : B) -> Exists (\ a => f a = b)

> ||| Non surjectivity, constructive
> NonSurjective : {A, B : Type} -> (f : A -> B) -> Type
> NonSurjective {A} f = Exists (\ b => (a : A) -> Not (f a = b))

Relationships of injectivity notions

> ||| Injective1 implies Injective2
> injectiveLemma : {A, B : Type} -> (f : A -> B) -> Injective1 f -> Injective2 f
> injectiveLemma f i1f a1 a2 contra = contra . (i1f a1 a2)
> %freeze injectiveLemma -- frozen

Properties of constructive proofs

> ||| NonInjective => Not Injective
> nonInjectiveNotInjective : {A, B : Type} -> (f : A -> B) -> NonInjective f -> Not (Injective1 f)
> nonInjectiveNotInjective f (Evidence a1 (Evidence a2 (na1eqa2 , fa1eqfa2))) =
>   \ injectivef => na1eqa2 (injectivef a1 a2 fa1eqfa2)
> %freeze nonInjectiveNotInjective -- frozen

> ||| NonSurjective => Not Surjective
> nonSurjectiveNotSurjective : {A, B : Type} -> (f : A -> B) -> NonSurjective f -> Not (Surjective f)
> nonSurjectiveNotSurjective f (Evidence b faanfab) =
>   \ surjectivef => let a = (getWitness (surjectivef b)) in (faanfab a) (getProof (surjectivef b))
> %freeze nonSurjectiveNotSurjective -- frozen

Properties of cross

> |||
> crossAnyIdFstLemma : fst ((cross f Prelude.Basics.id) (a,b)) = f a
> crossAnyIdFstLemma {a} {b} {f} = Refl

> |||
> crossAnyIdFstLemma' : fst ((cross f Prelude.Basics.id) ab) = f (fst ab)
> crossAnyIdFstLemma' {ab} {f} =
>     ( fst ((cross f Prelude.Basics.id) ab) )
>   ={ cong {f = \ ZUZU => fst ((cross f Prelude.Basics.id) ZUZU)} (pairLemma ab) }=
>     ( fst ((cross f Prelude.Basics.id) (fst ab, snd ab)) )
>   ={ Refl }=
>     ( fst (f (fst ab), id (snd ab)) )
>   ={ Refl }=
>     ( f (fst ab) )
>   QED

> |||
> crossAnyIdSndLemma : snd ((cross f Prelude.Basics.id) (a,b)) = b
> crossAnyIdSndLemma {a} {b} {f} = Refl

> |||
> crossAnyIdSndLemma' : snd ((cross f Prelude.Basics.id) ab) = snd ab
> crossAnyIdSndLemma' {ab} {f} =
>     ( snd ((cross f Prelude.Basics.id) ab) )
>   ={ cong {f = \ ZUZU => snd ((cross f Prelude.Basics.id) ZUZU)} (pairLemma ab) }=
>     ( snd ((cross f Prelude.Basics.id) (fst ab, snd ab)) )
>   ={ Refl }=
>     ( snd (f (fst ab), id (snd ab)) )
>   ={ Refl }=
>     ( snd (f (fst ab), snd ab) )
>   ={ Refl }=
>     ( snd ab )
>   QED

> |||
> crossIdAnyFstLemma : fst ((cross Prelude.Basics.id f) (a,b)) = a
> crossIdAnyFstLemma {a} {b} {f} = Refl

* Properties of extensional equality

> {-
> finiteDecidableExtEq : {A, B : Type} ->
>                        (f : A -> B) -> (g : A -> B) ->
>                        Finite A -> DecEq B -> Dec (ExtEq f g)
> -}

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
total
record Bar where
  constructor MkBar
  good : (Int -> Int) -> Bar
  bad  : (Bar -> Int) -> Bar


text:
module LightClick.IR.ChannelCentric

import Data.List
import Data.String
import Data.Vect

import Toolkit.Data.DList
import Toolkit.Data.DVect

import Language.SystemVerilog.Gates

import LightClick.Types
import LightClick.Terms
import LightClick.Error

import LightClick.IR.ModuleCentric

%default total

public export
data ChannelIR : TyIR -> Type where
  CRef  : String -> (type : TyIR) -> ChannelIR type
  CLet  : {term : TyIR}
       -> (bind : String)
       -> (this : ChannelIR term)
       -> (inThis : ChannelIR expr)
                 -> ChannelIR expr

  CSeq  : {a,b : TyIR}
       -> ChannelIR a
       -> ChannelIR b
       -> ChannelIR b

  CEnd : ChannelIR UNIT

  CPort : String
       -> Direction
       -> ChannelIR DATA
       -> ChannelIR PORT

  CModule : {n : Nat} -> Vect (S n) (ChannelIR PORT) -> ChannelIR MODULE

  CDataLogic : ChannelIR DATA
  CDataArray : ChannelIR DATA -> Nat -> ChannelIR DATA
  CDataStruct : {n : Nat} -> Vect (S n) (Pair String (ChannelIR DATA)) -> ChannelIR DATA
  CDataUnion  : {n : Nat} -> Vect (S n) (Pair String (ChannelIR DATA)) -> ChannelIR DATA

  CIDX : (label : String) -- don't exist in the normal form, required for mapping MIDX to something for coverage...
      -> ChannelIR MODULE
      -> ChannelIR PORT
      -> ChannelIR PORT

  CChan : ChannelIR DATA -> ChannelIR CHAN

  CModuleInst : {n : Nat}
              -> (mname : ChannelIR MODULE)
              -> Vect (S n)
                      (Pair String (ChannelIR CHAN))
              -> ChannelIR CONN

  CNot : ChannelIR CHAN
      -> ChannelIR CHAN
      -> ChannelIR GATE

  CGate : {n : Nat}
       -> TyGateComb
       -> ChannelIR CHAN
       -> Vect (S (S n)) (ChannelIR CHAN)
       -> ChannelIR GATE

covering
showC : ChannelIR type -> String
showC (CRef name type) =
  "(CRef " <+> show name <+> " " <+> show type <+> ")"

showC (CLet x y z) =
   "(CLet "
     <+> show x <+> " "
     <+> showC y <+> "\n"
     <+> showC z
     <+> "\n)"

showC (CSeq x y) =
    "(CSeq "
      <+> showC x <+> " "
      <+> showC y
      <+> "\n)"
showC CEnd = "(CEnd)"

showC (CPort x y z) =
    "(CPort "
      <+> show x <+> " "
      <+> show y <+> " "
      <+> showC z <+> " "
      <+> ")"

showC (CModule x) =
    "(CModule "
      <+> show (map showC x)
      <+> ")"

showC CDataLogic = "(CTyLogic)"

showC (CDataArray x k) =
  "(CTyArray "
    <+> showC x <+> " "
    <+> show k
    <+> ")"

showC (CDataStruct {n} xs) = "(CTyStruct " <+> show ps <+> ")"
  where
    covering
    ps : Vect (S n) String
    ps = map (\(l,c) => "(" <+> show l <+> " " <+> showC c <+> ")") xs

showC (CDataUnion {n} xs) = "(TyUnion " <+> show ps <+> ")"
  where
    covering
    ps : Vect (S n) String
    ps = map (\(l,c) => "(" <+> show l <+> " " <+> showC c <+> ")") xs

showC (CChan x) = "(CChan " <+> showC x <+> ")"

showC (CIDX l m p) =
  "(CIDX "
     <+> show l  <+> " "
     <+> showC m <+> " "
     <+> ")"
showC (CModuleInst m {n} params) =
    "(CModuleInst "
      <+> showC m <+> " "
      <+> show ps
      <+> ")"
  where
    covering
    ps : Vect (S n) String
    ps = map (\(l,c) => show l <+> " " <+> showC c) params

showC (CNot o i)
  = unwords ["(CNot", showC o, showC i, ")"]

showC (CGate ty o ins)
    = unwords ["(CGate", show ty, showC o, ins', ")"]

  where
    covering
    ins' : String
    ins' = unwords $ toList $ map (\c => "(" <+> showC c <+> ")") ins

export
Show (ChannelIR type) where
  show expr = assert_total $ showC expr

public export
Convert : Type -> Type
Convert = Either LightClick.Error

covering
convert : ModuleIR type -> Convert (ChannelIR type)

covering
convPort : ModuleIR PORT -> Convert (ChannelIR MODULE, String)
convPort (MRef name PORT) = Left (NotSupposedToHappen (Just "convPort CIR Ref"))
convPort (MLet name beThis inThis) = Left (NotSupposedToHappen (Just "convPort CIR Let"))
convPort (MSeq doThis thenThis) = Left (NotSupposedToHappen (Just "convPort CIR Seq"))
convPort (MPort label dir type) = Left (NotSupposedToHappen (Just "convPort CIR Port"))
convPort (MIDX label x z)
    = do m' <- convert x
         m'' <- convModule m'
         pure (m'',label)

  where

    convModule : ChannelIR MODULE -> Convert (ChannelIR MODULE)
    convModule m@(CRef x MODULE) = Right m
    convModule (CLet x z w)
      = Left (NotSupposedToHappen (Just "convModule CIR let"))

    convModule (CSeq x z)
      = Left (NotSupposedToHappen (Just "convModule CIR CSeq"))

    convModule (CModule xs)
      = Left (NotSupposedToHappen (Just "convModule CIR CMod"))

covering
mkConn : (p : ModuleIR PORT)
      -> (c : ChannelIR CHAN)
           -> Convert (ChannelIR CONN)
mkConn p c =
  do (m,l) <- convPort p
     pure (CModuleInst m [(l,c)])

covering
convPorts : (c    : ChannelIR CHAN)
         -> (outs : Vect (S n) (ModuleIR PORT))
                 -> Convert (ChannelIR CONN)
convPorts c (x :: []) = mkConn x c
convPorts c (x :: (z :: xs)) =
    do con <- mkConn x c
       rest <- convPorts c (z::xs)
       pure (CSeq con rest)

-- [ Definition ]
convert (MRef x t) = Right $ CRef x t
convert (MLet x y z) =
  do y' <- convert y
     z' <- convert z
     pure $ CLet x y' z'
convert (MSeq x y) =
  do x' <- convert x
     y' <- convert y
     pure $ CSeq x' y'
convert MEnd = pure CEnd

convert (MPort x y z) =
  do z' <- convert z
     pure $ CPort x y z'

convert (MModule {n} x) =
    do xs <- traverse convert x
       pure $ CModule xs

convert MDataLogic = Right $ CDataLogic

convert (MDataArray x k) =
  do x' <- convert x
     pure $ CDataArray x' k
convert (MDataStruct xs) =
    do xs' <- traverse (\(l,x) => do {x' <- convert x; pure (l, x')}) xs
       pure $ CDataStruct xs'

convert (MDataUnion xs)  =
    do xs' <- traverse (\(l,x) => do {x' <- convert x; pure (l,x')}) xs
       pure $ CDataUnion xs'

convert (MChan x) =
  do x' <- convert x
     pure (CChan x')

convert (MIDX x s y) =
  do s' <- convert s
     y' <- convert y
     pure (CIDX x s' y')

convert (MConn cname y ps) =
    do c <- convert cname
       i <- mkConn y c
       rest <- convPorts c ps
       pure (CSeq i rest)

convert (MNot o i)
  = do o' <- convert o
       i' <- convert i
       pure (CNot o' i')

convert (MGate ty o ins)
  = do o' <- convert o
       rest <- traverse convert ins
       pure (CGate ty o' rest)

convert (MConnG c idx)
  = do c' <- convert c
       p  <- mkConn idx c'
       pure p

export
covering
runConvert : ModuleIR type -> Convert (ChannelIR type)
runConvert = convert

-- [ EOF ]

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Drahko.Builtins

import Drahko.FFI

%access public export

%inline
msgBox : String -> Promise ()
msgBox = call_command "MsgBox" (String -> Promise ())

%inline
hotkey : String -> Promise () -> Promise ()
hotkey hotkeyString action =
  call_function "__drahko.hotkey"
    (String -> (() -> Promise ()) -> Promise ())
    hotkeyString (\_ => action)

%inline
reload : () -> Promise ()
reload = (call_command "Reload" (() -> Promise ()))

%inline
tooltip : String -> Promise ()
tooltip = call_command "Tooltip" (String -> Promise ())

%inline
sendInput : String -> Promise ()
sendInput = call_command "SendInput" (String -> Promise ())

%inline
sleep : Int -> Promise ()
sleep = call_command "Sleep" (Int -> Promise ())

%inline
loop : Promise () -> Promise ()
loop fun = call_function "__drahko._loop" ((() -> Promise ()) -> Promise ()) (\_ => fun)

max_stars_repo_name: NickSeagull/idris-autohotkey

max_issues_repo_name: NickSeagull/idris-autohotkey

max_forks_repo_name: drahko/drahko


text:
module Libraries.Utils.Scheme

export
data ForeignObj : Type where [external]

%foreign "scheme:blodwen-eval-scheme"
prim__evalScheme : String -> ForeignObj

%foreign "scheme:blodwen-eval-okay"
prim__evalOkay : ForeignObj -> Int

%foreign "scheme:blodwen-get-eval-result"
prim__evalResult : ForeignObj -> ForeignObj

%foreign "scheme:blodwen-debug-scheme"
prim__debugScheme : ForeignObj -> PrimIO ()

%foreign "scheme:blodwen-is-number"
prim_isNumber : ForeignObj -> Int

%foreign "scheme:blodwen-is-integer"
prim_isInteger : ForeignObj -> Int

%foreign "scheme:blodwen-is-float"
prim_isFloat : ForeignObj -> Int

%foreign "scheme:blodwen-is-char"
prim_isChar : ForeignObj -> Int

%foreign "scheme:blodwen-is-string"
prim_isString : ForeignObj -> Int

%foreign "scheme:blodwen-is-procedure"
prim_isProcedure : ForeignObj -> Int

%foreign "scheme:blodwen-is-symbol"
prim_isSymbol : ForeignObj -> Int

%foreign "scheme:blodwen-is-nil"
prim_isNil : ForeignObj -> Int

%foreign "scheme:blodwen-is-pair"
prim_isPair : ForeignObj -> Int

%foreign "scheme:blodwen-is-vector"
prim_isVector : ForeignObj -> Int

%foreign "scheme:blodwen-is-box"
prim_isBox : ForeignObj -> Int

export
isNumber : ForeignObj -> Bool
isNumber x = prim_isNumber x == 1

export
isInteger : ForeignObj -> Bool
isInteger x = prim_isInteger x == 1

export
isFloat : ForeignObj -> Bool
isFloat x = prim_isFloat x == 1

export
isChar : ForeignObj -> Bool
isChar x = prim_isChar x == 1

export
isString : ForeignObj -> Bool
isString x = prim_isString x == 1

export
isProcedure : ForeignObj -> Bool
isProcedure x = prim_isProcedure x == 1

export
isSymbol : ForeignObj -> Bool
isSymbol x = prim_isSymbol x == 1

export
isNil : ForeignObj -> Bool
isNil x = prim_isNil x == 1

export
isPair : ForeignObj -> Bool
isPair x = prim_isPair x == 1

export
isVector : ForeignObj -> Bool
isVector x = prim_isVector x == 1

export
isBox : ForeignObj -> Bool
isBox x = prim_isBox x == 1

-- The below are all 'unsafe' because they rely on having done the relevant
-- check above first
%foreign "scheme:blodwen-id"
export
unsafeGetInteger : ForeignObj -> Integer

%foreign "scheme:blodwen-id"
export
unsafeGetString : ForeignObj -> String

%foreign "scheme:blodwen-id"
export
unsafeGetFloat : ForeignObj -> Double

%foreign "scheme:blodwen-id"
export
unsafeGetChar : ForeignObj -> Char

%foreign "scheme:car"
export
unsafeFst : ForeignObj -> ForeignObj

%foreign "scheme:cdr"
export
unsafeSnd : ForeignObj -> ForeignObj

%foreign "scheme:blodwen-apply"
export
unsafeApply : ForeignObj -> ForeignObj -> ForeignObj

%foreign "scheme:blodwen-force"
export
unsafeForce : ForeignObj -> ForeignObj

%foreign "scheme:blodwen-vector-ref"
export
unsafeVectorRef : ForeignObj -> Integer -> ForeignObj

%foreign "scheme:blodwen-unbox"
export
unsafeUnbox : ForeignObj -> ForeignObj

%foreign "scheme:blodwen-vector-length"
export
unsafeVectorLength : ForeignObj -> Integer

%foreign "scheme:blodwen-vector-list"
export
unsafeVectorToList : ForeignObj -> List ForeignObj

%foreign "scheme:blodwen-make-symbol"
export
makeSymbol : String -> ForeignObj

%foreign "scheme:blodwen-read-symbol"
export
unsafeReadSymbol : ForeignObj -> String

export
evalSchemeStr : String -> IO (Maybe ForeignObj)
evalSchemeStr exp
    = let obj = prim__evalScheme exp in
          if prim__evalOkay obj == 1
             then pure $ Just (prim__evalResult obj)
             else pure Nothing

export
debugScheme : ForeignObj -> IO ()
debugScheme obj = primIO $ prim__debugScheme obj

public export
data Direction = Write | Readback

public export
data SchemeObj : Direction -> Type where
     Null : SchemeObj t
     Cons : SchemeObj t -> SchemeObj t -> SchemeObj t
     IntegerVal : Integer -> SchemeObj t
     FloatVal : Double -> SchemeObj t
     StringVal : String -> SchemeObj t
     CharVal : Char -> SchemeObj t
     Symbol : String -> SchemeObj t
     Box : SchemeObj t -> SchemeObj t
     Vector : Integer -> List (SchemeObj t) -> SchemeObj t
        -- ^ this is convenient for us since all our vectors start with a
        -- tag, but not for a general library

     Procedure : ForeignObj -> SchemeObj Readback

     Define : String -> SchemeObj Write -> SchemeObj Write
     Var : String -> SchemeObj Write
     Lambda : List String -> SchemeObj Write -> SchemeObj Write
     Let : String -> SchemeObj Write -> SchemeObj Write -> SchemeObj Write
     If : SchemeObj Write -> SchemeObj Write -> SchemeObj Write ->
          SchemeObj Write
     Case : SchemeObj Write ->
            List (SchemeObj Write, SchemeObj Write) ->
            Maybe (SchemeObj Write) ->
            SchemeObj Write
     Cond : List (SchemeObj Write, SchemeObj Write) ->
            Maybe (SchemeObj Write) ->
            SchemeObj Write
     Apply : SchemeObj Write -> List (SchemeObj Write) -> SchemeObj Write

export
evalSchemeObj : SchemeObj Write -> IO (Maybe ForeignObj)
evalSchemeObj obj
    = do let str = toString obj
         evalSchemeStr str
  where
    showSep : String -> List String -> String
    showSep sep [] = ""
    showSep sep [x] = x
    showSep sep (x :: xs) = x ++ sep ++ showSep sep xs

    toString : SchemeObj Write -> String
    toString Null = "'()"
    toString (Cons x y) = "(cons " ++ toString x ++ " " ++ toString y ++ ")"
    toString (IntegerVal x) = show x
    toString (FloatVal x) = show x
    toString (StringVal x) = show x
    toString (CharVal x)
       = if (the Int (cast x) >= 32 && the Int (cast x) < 127)
            then "#\\" ++ cast x
            else "(integer->char " ++ show (the Int (cast x)) ++ ")"
    toString (Symbol x) = "'" ++ x
    toString (Vector i xs) = "(vector " ++ show i ++ " " ++ showSep " " (map toString xs) ++ ")"
    toString (Box x) = "(box " ++ toString x ++ ")"
    toString (Define x body) = "(define (" ++ x ++ ") " ++ toString body ++ ")"
    toString (Var x) = x
    toString (Lambda xs x)
        = "(lambda (" ++ showSep " " xs ++ ") " ++ toString x ++ ")"
    toString (Let var val x)
        = "(let ((" ++ var ++ " " ++ toString val ++ ")) " ++ toString x ++ ")"
    toString (If x t e)
        = "(if " ++ toString x ++ " " ++ toString t ++ " " ++ toString e ++ ")"
    toString (Case x alts def)
        = "(case " ++ toString x ++ " " ++
              showSep " " (map showAlt alts) ++
              showDef def ++ ")"
      where
        showAlt : (SchemeObj Write, SchemeObj Write) -> String
        showAlt (opt, go)
           = "((" ++ toString opt ++ ") " ++ toString go ++ ")"

        showDef : Maybe (SchemeObj Write) -> String
        showDef Nothing = ""
        showDef (Just e) = " (else " ++ toString e ++ ")"
    toString (Cond alts def)
        = "(cond " ++
              showSep " " (map showAlt alts) ++
              showDef def ++ ")"
      where
        showAlt : (SchemeObj Write, SchemeObj Write) -> String
        showAlt (opt, go)
           = "(" ++ toString opt ++ " " ++ toString go ++ ")"

        showDef : Maybe (SchemeObj Write) -> String
        showDef Nothing = ""
        showDef (Just e) = " (else " ++ toString e ++ ")"
    toString (Apply x xs)
        = "(" ++ toString x ++ " " ++ showSep " " (map toString xs) ++ ")"

export
decodeObj : ForeignObj -> SchemeObj Readback
decodeObj obj
    = if isInteger obj then IntegerVal (unsafeGetInteger obj)
      else if isVector obj then Vector (unsafeGetInteger (unsafeVectorRef obj 0))
                                       (readVector (unsafeVectorLength obj) 1 obj)
      else if isPair obj then Cons (decodeObj (unsafeFst obj))
                                   (decodeObj (unsafeSnd obj))
      else if isFloat obj then FloatVal (unsafeGetFloat obj)
      else if isString obj then StringVal (unsafeGetString obj)
      else if isChar obj then CharVal (unsafeGetChar obj)
      else if isSymbol obj then Symbol (unsafeReadSymbol obj)
      else if isProcedure obj then Procedure obj
      else if isBox obj then Box (decodeObj (unsafeUnbox obj))
      else Null
  where
    readVector : Integer -> Integer -> ForeignObj -> List (SchemeObj Readback)
    readVector len i obj
        = if len == i
             then []
             else decodeObj (unsafeVectorRef obj i) ::
                     readVector len (i + 1) obj

public export
interface Scheme a where
  toScheme : a -> SchemeObj Write
  fromScheme : SchemeObj Readback -> Maybe a

export
evalScheme : Scheme a => a -> IO (Maybe ForeignObj)
evalScheme = evalSchemeObj . toScheme

export
decode : Scheme a => ForeignObj -> Maybe a
decode = fromScheme . decodeObj

export
Scheme Integer where
  toScheme x = IntegerVal x

  fromScheme (IntegerVal x) = Just x
  fromScheme _ = Nothing

export
Scheme Int where
  toScheme x = IntegerVal (cast x)

  fromScheme (IntegerVal x) = Just (cast x)
  fromScheme _ = Nothing

export
Scheme Int8 where
  toScheme x = IntegerVal (cast x)

  fromScheme (IntegerVal x) = Just (cast x)
  fromScheme _ = Nothing

export
Scheme Int16 where
  toScheme x = IntegerVal (cast x)

  fromScheme (IntegerVal x) = Just (cast x)
  fromScheme _ = Nothing

export
Scheme Int32 where
  toScheme x = IntegerVal (cast x)

  fromScheme (IntegerVal x) = Just (cast x)
  fromScheme _ = Nothing

export
Scheme Int64 where
  toScheme x = IntegerVal (cast x)

  fromScheme (IntegerVal x) = Just (cast x)
  fromScheme _ = Nothing

export
Scheme Bits8 where
  toScheme x = IntegerVal (cast x)

  fromScheme (IntegerVal x) = Just (cast x)
  fromScheme _ = Nothing

export
Scheme Bits16 where
  toScheme x = IntegerVal (cast x)

  fromScheme (IntegerVal x) = Just (cast x)
  fromScheme _ = Nothing

export
Scheme Bits32 where
  toScheme x = IntegerVal (cast x)

  fromScheme (IntegerVal x) = Just (cast x)
  fromScheme _ = Nothing

export
Scheme Bits64 where
  toScheme x = IntegerVal (cast x)

  fromScheme (IntegerVal x) = Just (cast x)
  fromScheme _ = Nothing

export
Scheme String where
  toScheme x = StringVal x

  fromScheme (StringVal x) = Just x
  fromScheme _ = Nothing

export
Scheme Double where
  toScheme x = FloatVal x

  fromScheme (FloatVal x) = Just x
  fromScheme _ = Nothing

export
Scheme Char where
  toScheme x = CharVal x

  fromScheme (CharVal x) = Just x
  fromScheme _ = Nothing

export
Scheme Bool where
  toScheme False = IntegerVal 0
  toScheme True = IntegerVal 1

  fromScheme (IntegerVal 0) = Just False
  fromScheme (IntegerVal 1) = Just True
  fromScheme _ = Nothing

export
Scheme a => Scheme (List a) where
  toScheme [] = Null
  toScheme (x :: xs) = Cons (toScheme x) (toScheme xs)

  fromScheme Null = Just []
  fromScheme (Cons x xs) = Just $ !(fromScheme x) :: !(fromScheme xs)
  fromScheme _ = Nothing

export
(Scheme a, Scheme b) => Scheme (a, b) where
  toScheme (x, y) = Cons (toScheme x) (toScheme y)
  fromScheme (Cons x y) = Just (!(fromScheme x), !(fromScheme y))
  fromScheme _ = Nothing

export
Scheme a => Scheme (Maybe a) where
  toScheme Nothing = Null
  toScheme (Just x) = Box (toScheme x)

  fromScheme Null = Just Nothing
  fromScheme (Box x) = Just $ Just !(fromScheme x)
  fromScheme _ = Nothing


text:
%!PS-Adobe-2.0 EPSF-1.2
%%Creator: idraw
%%DocumentFonts: Helvetica
%%Pages: 1
%%BoundingBox: 73 285 501 613
%%EndComments

%%BeginIdrawPrologue
/arrowhead {
0 begin
transform originalCTM itransform
/taily exch def
/tailx exch def
transform originalCTM itransform
/tipy exch def
/tipx exch def
/dy tipy taily sub def
/dx tipx tailx sub def
/angle dx 0 ne dy 0 ne or { dy dx atan } { 90 } ifelse def
gsave
originalCTM setmatrix
tipx tipy translate
angle rotate
newpath
arrowHeight neg arrowWidth 2 div moveto
0 0 lineto
arrowHeight neg arrowWidth 2 div neg lineto
patternNone not {
originalCTM setmatrix
/padtip arrowHeight 2 exp 0.25 arrowWidth 2 exp mul add sqrt brushWidth mul
arrowWidth div def
/padtail brushWidth 2 div def
tipx tipy translate
angle rotate
padtip 0 translate
arrowHeight padtip add padtail add arrowHeight div dup scale
arrowheadpath
ifill
} if
brushNone not {
originalCTM setmatrix
tipx tipy translate
angle rotate
arrowheadpath
istroke
} if
grestore
end
} dup 0 9 dict put def

/arrowheadpath {
newpath
arrowHeight neg arrowWidth 2 div moveto
0 0 lineto
arrowHeight neg arrowWidth 2 div neg lineto
} def

/leftarrow {
0 begin
y exch get /taily exch def
x exch get /tailx exch def
y exch get /tipy exch def
x exch get /tipx exch def
brushLeftArrow { tipx tipy tailx taily arrowhead } if
end
} dup 0 4 dict put def

/rightarrow {
0 begin
y exch get /tipy exch def
x exch get /tipx exch def
y exch get /taily exch def
x exch get /tailx exch def
brushRightArrow { tipx tipy tailx taily arrowhead } if
end
} dup 0 4 dict put def

%%EndIdrawPrologue

/arrowHeight 11 def
/arrowWidth 5 def

/IdrawDict 51 dict def
IdrawDict begin

/reencodeISO {
dup dup findfont dup length dict begin
{ 1 index /FID ne { def }{ pop pop } ifelse } forall
/Encoding ISOLatin1Encoding def
currentdict end definefont
} def

/ISOLatin1Encoding [
/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef
/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef
/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef
/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef
/space/exclam/quotedbl/numbersign/dollar/percent/ampersand/quoteright
/parenleft/parenright/asterisk/plus/comma/minus/period/slash
/zero/one/two/three/four/five/six/seven/eight/nine/colon/semicolon
/less/equal/greater/question/at/A/B/C/D/E/F/G/H/I/J/K/L/M/N
/O/P/Q/R/S/T/U/V/W/X/Y/Z/bracketleft/backslash/bracketright
/asciicircum/underscore/quoteleft/a/b/c/d/e/f/g/h/i/j/k/l/m
/n/o/p/q/r/s/t/u/v/w/x/y/z/braceleft/bar/braceright/asciitilde
/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef
/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef
/.notdef/dotlessi/grave/acute/circumflex/tilde/macron/breve
/dotaccent/dieresis/.notdef/ring/cedilla/.notdef/hungarumlaut
/ogonek/caron/space/exclamdown/cent/sterling/currency/yen/brokenbar
/section/dieresis/copyright/ordfeminine/guillemotleft/logicalnot
/hyphen/registered/macron/degree/plusminus/twosuperior/threesuperior
/acute/mu/paragraph/periodcentered/cedilla/onesuperior/ordmasculine
/guillemotright/onequarter/onehalf/threequarters/questiondown
/Agrave/Aacute/Acircumflex/Atilde/Adieresis/Aring/AE/Ccedilla
/Egrave/Eacute/Ecircumflex/Edieresis/Igrave/Iacute/Icircumflex
/Idieresis/Eth/Ntilde/Ograve/Oacute/Ocircumflex/Otilde/Odieresis
/multiply/Oslash/Ugrave/Uacute/Ucircumflex/Udieresis/Yacute
/Thorn/germandbls/agrave/aacute/acircumflex/atilde/adieresis
/aring/ae/ccedilla/egrave/eacute/ecircumflex/edieresis/igrave
/iacute/icircumflex/idieresis/eth/ntilde/ograve/oacute/ocircumflex
/otilde/odieresis/divide/oslash/ugrave/uacute/ucircumflex/udieresis
/yacute/thorn/ydieresis
] def
/Helvetica reencodeISO def

/none null def
/numGraphicParameters 17 def
/stringLimit 65535 def

/Begin {
save
numGraphicParameters dict begin
} def

/End {
end
restore
} def

/SetB {
dup type /nulltype eq {
pop
false /brushRightArrow idef
false /brushLeftArrow idef
true /brushNone idef
} {
/brushDashOffset idef
/brushDashArray idef
0 ne /brushRightArrow idef
0 ne /brushLeftArrow idef
/brushWidth idef
false /brushNone idef
} ifelse
} def

/SetCFg {
/fgblue idef
/fggreen idef
/fgred idef
} def

/SetCBg {
/bgblue idef
/bggreen idef
/bgred idef
} def

/SetF {
/printSize idef
/printFont idef
} def

/SetP {
dup type /nulltype eq {
pop true /patternNone idef
} {
dup -1 eq {
/patternGrayLevel idef
/patternString idef
} {
/patternGrayLevel idef
} ifelse
false /patternNone idef
} ifelse
} def

/BSpl {
0 begin
storexyn
newpath
n 1 gt {
0 0 0 0 0 0 1 1 true subspline
n 2 gt {
0 0 0 0 1 1 2 2 false subspline
1 1 n 3 sub {
/i exch def
i 1 sub dup i dup i 1 add dup i 2 add dup false subspline
} for
n 3 sub dup n 2 sub dup n 1 sub dup 2 copy false subspline
} if
n 2 sub dup n 1 sub dup 2 copy 2 copy false subspline
patternNone not brushLeftArrow not brushRightArrow not and and { ifill } if
brushNone not { istroke } if
0 0 1 1 leftarrow
n 2 sub dup n 1 sub dup rightarrow
} if
end
} dup 0 4 dict put def

/Circ {
newpath
0 360 arc
closepath
patternNone not { ifill } if
brushNone not { istroke } if
} def

/CBSpl {
0 begin
dup 2 gt {
storexyn
newpath
n 1 sub dup 0 0 1 1 2 2 true subspline
1 1 n 3 sub {
/i exch def
i 1 sub dup i dup i 1 add dup i 2 add dup false subspline
} for
n 3 sub dup n 2 sub dup n 1 sub dup 0 0 false subspline
n 2 sub dup n 1 sub dup 0 0 1 1 false subspline
patternNone not { ifill } if
brushNone not { istroke } if
} {
Poly
} ifelse
end
} dup 0 4 dict put def

/Elli {
0 begin
newpath
4 2 roll
translate
scale
0 0 1 0 360 arc
closepath
patternNone not { ifill } if
brushNone not { istroke } if
end
} dup 0 1 dict put def

/Line {
0 begin
2 storexyn
newpath
x 0 get y 0 get moveto
x 1 get y 1 get lineto
brushNone not { istroke } if
0 0 1 1 leftarrow
0 0 1 1 rightarrow
end
} dup 0 4 dict put def

/MLine {
0 begin
storexyn
newpath
n 1 gt {
x 0 get y 0 get moveto
1 1 n 1 sub {
/i exch def
x i get y i get lineto
} for
patternNone not brushLeftArrow not brushRightArrow not and and { ifill } if
brushNone not { istroke } if
0 0 1 1 leftarrow
n 2 sub dup n 1 sub dup rightarrow
} if
end
} dup 0 4 dict put def

/Poly {
3 1 roll
newpath
moveto
-1 add
{ lineto } repeat
closepath
patternNone not { ifill } if
brushNone not { istroke } if
} def

/Rect {
0 begin
/t exch def
/r exch def
/b exch def
/l exch def
newpath
l b moveto
l t lineto
r t lineto
r b lineto
closepath
patternNone not { ifill } if
brushNone not { istroke } if
end
} dup 0 4 dict put def

/Text {
ishow
} def

/idef {
dup where { pop pop pop } { exch def } ifelse
} def

/ifill {
0 begin
gsave
patternGrayLevel -1 ne {
fgred bgred fgred sub patternGrayLevel mul add
fggreen bggreen fggreen sub patternGrayLevel mul add
fgblue bgblue fgblue sub patternGrayLevel mul add setrgbcolor
eofill
} {
eoclip
originalCTM setmatrix
pathbbox /t exch def /r exch def /b exch def /l exch def
/w r l sub ceiling cvi def
/h t b sub ceiling cvi def
/imageByteWidth w 8 div ceiling cvi def
/imageHeight h def
bgred bggreen bgblue setrgbcolor
eofill
fgred fggreen fgblue setrgbcolor
w 0 gt h 0 gt and {
l w add b translate w neg h scale
w h true [w 0 0 h neg 0 h] { patternproc } imagemask
} if
} ifelse
grestore
end
} dup 0 8 dict put def

/istroke {
gsave
brushDashOffset -1 eq {
[] 0 setdash
1 setgray
} {
brushDashArray brushDashOffset setdash
fgred fggreen fgblue setrgbcolor
} ifelse
brushWidth setlinewidth
originalCTM setmatrix
stroke
grestore
} def

/ishow {
0 begin
gsave
fgred fggreen fgblue setrgbcolor
/fontDict printFont printSize scalefont dup setfont def
/descender fontDict begin 0 /FontBBox load 1 get FontMatrix end
transform exch pop def
/vertoffset 1 printSize sub descender sub def {
0 vertoffset moveto show
/vertoffset vertoffset printSize sub def
} forall
grestore
end
} dup 0 3 dict put def
/patternproc {
0 begin
/patternByteLength patternString length def
/patternHeight patternByteLength 8 mul sqrt cvi def
/patternWidth patternHeight def
/patternByteWidth patternWidth 8 idiv def
/imageByteMaxLength imageByteWidth imageHeight mul
stringLimit patternByteWidth sub min def
/imageMaxHeight imageByteMaxLength imageByteWidth idiv patternHeight idiv
patternHeight mul patternHeight max def
/imageHeight imageHeight imageMaxHeight sub store
/imageString imageByteWidth imageMaxHeight mul patternByteWidth add string def
0 1 imageMaxHeight 1 sub {
/y exch def
/patternRow y patternByteWidth mul patternByteLength mod def
/patternRowString patternString patternRow patternByteWidth getinterval def
/imageRow y imageByteWidth mul def
0 patternByteWidth imageByteWidth 1 sub {
/x exch def
imageString imageRow x add patternRowString putinterval
} for
} for
imageString
end
} dup 0 12 dict put def

/min {
dup 3 2 roll dup 4 3 roll lt { exch } if pop
} def

/max {
dup 3 2 roll dup 4 3 roll gt { exch } if pop
} def

/midpoint {
0 begin
/y1 exch def
/x1 exch def
/y0 exch def
/x0 exch def
x0 x1 add 2 div
y0 y1 add 2 div
end
} dup 0 4 dict put def

/thirdpoint {
0 begin
/y1 exch def
/x1 exch def
/y0 exch def
/x0 exch def
x0 2 mul x1 add 3 div
y0 2 mul y1 add 3 div
end
} dup 0 4 dict put def

/subspline {
0 begin
/movetoNeeded exch def
y exch get /y3 exch def
x exch get /x3 exch def
y exch get /y2 exch def
x exch get /x2 exch def
y exch get /y1 exch def
x exch get /x1 exch def
y exch get /y0 exch def
x exch get /x0 exch def
x1 y1 x2 y2 thirdpoint
/p1y exch def
/p1x exch def
x2 y2 x1 y1 thirdpoint
/p2y exch def
/p2x exch def
x1 y1 x0 y0 thirdpoint
p1x p1y midpoint
/p0y exch def
/p0x exch def
x2 y2 x3 y3 thirdpoint
p2x p2y midpoint
/p3y exch def
/p3x exch def
movetoNeeded { p0x p0y moveto } if
p1x p1y p2x p2y p3x p3y curveto
end
} dup 0 17 dict put def

/storexyn {
/n exch def
/y n array def
/x n array def
n 1 sub -1 0 {
/i exch def
y i 3 2 roll put
x i 3 2 roll put
} for
} def

/SSten {
fgred fggreen fgblue setrgbcolor
dup true exch 1 0 0 -1 0 6 -1 roll matrix astore
} def

/FSten {
dup 3 -1 roll dup 4 1 roll exch
newpath
0 0 moveto
dup 0 exch lineto
exch dup 3 1 roll exch lineto
0 lineto
closepath
bgred bggreen bgblue setrgbcolor
eofill
SSten
} def

/Rast {
exch dup 3 1 roll 1 0 0 -1 0 6 -1 roll matrix astore
} def

%%EndProlog

%I Idraw 13 Grid 8 8

%%Page: 1 1

Begin
%I b u
%I cfg u
%I cbg u
%I f u
%I p u
%I t
[ 0.74759 0 0 0.74759 0 0 ] concat
/originalCTM matrix currentmatrix def

Begin %I CBSpl
%I b 3855
1 0 0 [4 4 4 4] 0 SetB
%I cfg White
1 1 1 SetCFg
%I cbg LtGray
0.762951 0.762951 0.762951 SetCBg
%I p
< ff 88 88 88 ff 88 88 88 > -1 SetP
%I t
[ 0.989609 -0.292526 0.292526 0.989609 -239.729 188.764 ] concat
%I 6
567 706
417 664
241 540
237 423
292 365
409 391
6 CBSpl
End

Begin %I CBSpl
%I b 3855
1 0 0 [4 4 4 4] 0 SetB
%I cfg White
1 1 1 SetCFg
%I cbg LtGray
0.762951 0.762951 0.762951 SetCBg
%I p
1 SetP
%I t
[ 1.01311 0.196216 -0.196216 1.01311 171.544 -20.8712 ] concat
%I 6
302 690
427 644
557 491
548 377
475 345
334 417
6 CBSpl
End

Begin %I BSpl
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
%I p
1 SetP
%I t
[ 0.257703 -0.0120494 0.0120494 0.257703 273.834 535.079 ] concat
%I 14
465 533
632 679
632 679
653 679
665 672
670 660
671 649
665 635
665 635
505 488
505 488
472 485
461 512
462 516
14 BSpl
%I 4
End

Begin %I Pict
%I b u
%I cfg u
%I cbg u
%I f u
%I p u
%I t
[ 0.971801 -0.235805 0.235805 0.971801 -24.261 16.3265 ] concat

Begin %I Line
%I b 65535
1 0 1 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -78 54 ] concat
%I
539 603 590 538 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 1 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -78 54 ] concat
%I
539 603 582 690 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 1 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -78 54 ] concat
%I
539 603 454 602 Line
%I 1
End

End %I eop

Begin %I Text
%I cfg Black
0 0 0 SetCFg
%I f -*-helvetica-medium-r-normal--24-*
Helvetica 24 SetF
%I t
[ 1 0 0 1 608.893 638.99 ] concat
%I
[
(A)
] Text
End

Begin %I Text
%I cfg Black
0 0 0 SetCFg
%I f -*-helvetica-medium-r-normal--24-*
Helvetica 24 SetF
%I t
[ 1 0 0 1 210.6 653.285 ] concat
%I
[
(B)
] Text
End

Begin %I Pict
%I b u
%I cfg u
%I cbg u
%I f u
%I p u
%I t
[ 0.853926 0.520394 -0.520394 0.853926 196.226 -231.469 ] concat

Begin %I Line
%I b 65535
1 0 1 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -78 54 ] concat
%I
539 603 590 538 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 1 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -78 54 ] concat
%I
539 603 582 690 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 1 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -78 54 ] concat
%I
539 603 454 602 Line
%I 1
End

End %I eop

Begin %I Text
%I cfg Black
0 0 0 SetCFg
%I f -*-helvetica-medium-r-normal--18-*
Helvetica 18 SetF
%I t
[ 1 0 0 1 405.801 798.823 ] concat
%I
[
(D)
] Text
End

Begin %I Elli
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
%I p
1 SetP
%I t
[ 0.515969 -0 -0 0.515969 250.506 316.55 ] concat
%I
298 666 16 16 Elli
End

Begin %I BSpl
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.257985 -0 -0 0.257985 279.913 529.127 ] concat
%I 8
555 603
569 609
583 606
595 596
598 584
597 572
592 562
588 559
8 BSpl
%I 4
End

Begin %I Line
%I b 65535
2 0 1 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.257985 -0 -0 0.257985 280.171 529.385 ] concat
%I
482 504 353 392 Line
%I 4
End

Begin %I Line
%I b 65535
1 0 1 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.257985 -0 -0 0.257985 280.171 529.385 ] concat
%I
591 561 925 326 Line
%I 4
End

Begin %I Line
%I b 65535
1 0 1 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.257985 -0 -0 0.257985 280.171 529.385 ] concat
%I
596 577 1004 578 Line
%I 4
End

Begin %I Line
%I b 65535
1 0 1 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.257985 -0 -0 0.257985 280.171 529.385 ] concat
%I
570 607 570 1012 Line
%I 4
End

Begin %I Line
%I b 65535
1 0 1 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.257985 -0 -0 0.257985 280.171 529.385 ] concat
%I
587 601 826 932 Line
%I 4
End

Begin %I Pict
%I b u
%I cfg u
%I cbg u
%I f u
%I p u
%I t
[ 1 0 0 1 -315.773 2.0639 ] concat

Begin %I Text
%I cfg Black
0 0 0 SetCFg
%I f -*-helvetica-medium-r-normal--24-*
Helvetica 24 SetF
%I t
[ 1 0 0 1 592 681 ] concat
%I
[
(T)
] Text
End

Begin %I Text
%I cfg Black
0 0 0 SetCFg
%I f -*-helvetica-medium-r-normal--18-*
Helvetica 18 SetF
%I t
[ 1 0 0 1 607 667 ] concat
%I
[
(DB)
] Text
End

End %I eop

Begin %I BSpl
%I b 65535
2 0 1 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1.03194 -0 -0 1.03194 -105.258 114.545 ] concat
%I 4
347 446
391 514
447 548
499 550
4 BSpl
%I 1
End

Begin %I BSpl
%I b 65535
2 1 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1.03194 -0 -0 1.03194 -105.258 114.545 ] concat
%I 5
530 543
608 530
645 501
662 462
661 428
5 BSpl
%I 1
End

Begin %I BSpl
%I b 65535
2 1 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1.03194 -0 -0 1.03194 -110.417 59.8525 ] concat
%I 5
352 485
407 397
492 369
593 392
660 463
5 BSpl
%I 1
End

Begin %I Text
%I cfg Black
0 0 0 SetCFg
%I f -*-helvetica-medium-r-normal--24-*
Helvetica 24 SetF
%I t
[ 1 0 0 1 367.814 496.027 ] concat
%I
[
(T)
] Text
End

Begin %I Text
%I cfg Black
0 0 0 SetCFg
%I f -*-helvetica-medium-r-normal--18-*
Helvetica 18 SetF
%I t
[ 1 0 0 1 382.814 482.027 ] concat
%I
[
(BA)
] Text
End

Begin %I Text
%I cfg Black
0 0 0 SetCFg
%I f -*-helvetica-medium-r-normal--24-*
Helvetica 24 SetF
%I t
[ 1 0 0 1 529.825 608.467 ] concat
%I
[
(T)
] Text
End

Begin %I Text
%I cfg Black
0 0 0 SetCFg
%I f -*-helvetica-medium-r-normal--24-*
Helvetica 24 SetF
%I t
[ 1 0 0 1 427.865 761.329 ] concat
%I
[
(T)
] Text
End

Begin %I Text
%I cfg Black
0 0 0 SetCFg
%I f -*-helvetica-medium-r-normal--18-*
Helvetica 18 SetF
%I t
[ 1 0 0 1 473.629 783.988 ] concat
%I
[
(C)
] Text
End

Begin %I Text
%I cfg Black
0 0 0 SetCFg
%I f -*-helvetica-medium-r-normal--18-*
Helvetica 18 SetF
%I t
[ 1 0 0 1 442.865 747.329 ] concat
%I
[
(CD)
] Text
End

Begin %I Text
%I cfg Black
0 0 0 SetCFg
%I f -*-helvetica-medium-r-normal--18-*
Helvetica 18 SetF
%I t
[ 1 0 0 1 544.825 594.467 ] concat
%I
[
(CA)
] Text
End

Begin %I BSpl
%I b 65535
2 0 1 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg LtGray
0.762951 0.762951 0.762951 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -79 73 ] concat
%I 8
499 611
488 641
498 655
518 658
530 653
535 636
528 620
517 611
8 BSpl
%I 1
End

End %I eop

showpage

%%Trailer

end

max_issues_repo_name: gaetanbahl/carapas

max_forks_repo_name: gaetanbahl/carapas


text:
-- Exercises.idr
-- Solutions for exercises of chapter 1

module Exercises

-- Check if words are palindromes

||| Checks whether the given word is a palindrome
||| The check is case-insensitive
||| @str A string to be checked
export
palindrome : (str : String) -> Bool
palindrome str = let lstr = toLower str
                     rev = reverse lstr in
                     lstr == rev

||| Checks whether the given word is a palindrome
||| The check is case-insensitive and a minimum word
||| length is required.
||| @minLen Minimum required word length for palindrome
||| @str A string to be checked
export
palindromeMinLen : (minLen : Nat) -> (str : String) -> Bool
palindromeMinLen minLen str = let wordLength = length str
                                  lstr = toLower str
                                  rev = reverse lstr in
                                  (wordLength > minLen) && (lstr == rev)

-- Count words & characters

||| Counts the number of words and characters of the given string.
||| Whitespace is ignored.
||| @str A string to be counted
export
counts : (str : String) -> (Nat, Nat)
counts str = let ww = words str
                 numWords = length ww
                 numChars = sum (map length ww) in
                 (numWords, numChars)

||| Counts the number of words and characters of the given string.
||| Whitespace is included..
||| @str A string to be counted
export
countWithSpace : (str : String) -> (Nat, Nat)
countWithSpace str = let ww = words str
                         numWords = length ww
                         numChars = length str in
                         (numWords, numChars)

-- Extract top 10 values

||| Extracts the 10 largest values from given list
||| ('top ten')
||| @l List with numeric values
export
top_ten : Ord a => (l : List a) -> List a
top_ten l = take 10 $ reverse $ sort l

-- Count strings over given length

||| Counts the number of strings wiht length
||| larger than given limit
||| @len A Nat of length limit
||| @strs A list of string
export
over_length : (len : Nat) -> (strs : List String) -> Nat
over_length len strs = length $ filter (\w => (length w) > len) strs

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
import Network.DefaultHttpEngine
import Control.ST
import Network.Wai
import Network.ST.TcpSockets
import Network.Socket.Data

specificEngine : HttpEngine IO
specificEngine = defaultHttpEngine IO ioTcpSockets

mainST : ST IO String []
mainST = runApplication specificEngine Nothing 8080 $
           mkApplication specificEngine $ \engineState, req => do
            sendResponse specificEngine engineState (MkHttpResponse http200 [] "It works!")

main : IO ()
main = do
  result <- run mainST
  printLn result


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

module Tester

import public Control.Monad.Either
import Data.String
import Control.ANSI

||| A function which can report test failures.
public export
TestFunc : Type -> Type
TestFunc = EitherT String IO

||| Value representing a test.
|||
||| Use the `test` function to create a value of this type.
public export
record Test where
    constructor MkTest
    description : String
    run : TestFunc ()

red : String -> String
red s = show $ colored Red s

||| Create a new `Test` with a description and function to run.
|||
||| Use `Test.Runner.runTests` to run the tests.
|||
||| ```idris example
||| itWorks = test "it works" $ do
|||     assertEq (1 + 1) 2
||| ```
public export
test : (description : String) -> (run : TestFunc ()) -> Test
test = MkTest

||| Assert that two values are equal.
|||
||| Stops the test and reports a test failure if the values are not equal.
public export
assertEq : (Eq a, Show a) => (left, right : a) -> TestFunc ()
assertEq left right =
    if left /= right then
        let msg = unlines [
                    red "assertEq" ++ " failed:",
                    "  left  `" ++ red (show left) ++ "`",
                    "  right `" ++ red (show right) ++ "`"
                ]
        in throwE msg
    else
        pure ()

||| Assert that two values are not equal.
|||
||| Stops the test and reports a test failure if the values are equal.
public export
assertNotEq : (Eq a, Show a) => (left, right : a) -> TestFunc ()
assertNotEq left right =
    if left == right then
        let msg = unlines [
                    red "assertNotEq" ++ " failed:",
                    "  left  `" ++ red (show left) ++ "`",
                    "  right `" ++ red (show right) ++ "`"
                ]
        in throwE msg
    else
        pure ()

||| Assert that a condition holds.
|||
||| Stops the test and reports a test failure if the condition does not hold.
public export
assert : (cond : Bool) -> TestFunc ()
assert cond =
    if not cond then
        let msg = red "assert" ++ "failed"
        in throwE msg
    else
        pure ()

||| Cause a test failure with a message.
public export
throw : (msg : String) -> TestFunc a
throw = throwE

max_stars_repo_name: tiatomee/tester-idr

max_issues_repo_name: tiatomee/tester-idr

max_forks_repo_name: tiatomee/tester-idr


text:
module Idris.Codegen.ExtSTG.Foreign

import Data.List1
import Data.Strings
import Core.Name
import Core.Context
import Data.List
import Core.TT
import Core.CompileExpr
import System.File

import Idris.Codegen.ExtSTG.Core
import Idris.Codegen.ExtSTG.Prelude
import Idris.Codegen.ExtSTG.STG
import Idris.Codegen.ExtSTG.ExternalTopIds

import Idris.Codegen.ExtSTG.String

%default total

{-
For foreign implementation we use simple Haskell notation, but the foreign string starts with: 'stg:'
-}

{-
-- Argument type descriptors for foreign function calls
public export
data CFType : Type where
     CFUnit : CFType :: ()
     -- Unit type in haskell is represented ()
     CFInt : CFType :: Int
     -- Simple boxed integer
     CFUnsigned8 : CFType :: Word8
     -- Simple boxed word8
     CFUnsigned16 : CFType :: Word16
     -- simple boxed word16
     CFUnsigned32 : CFType :: Word32
     -- simple boxed word32
     CFUnsigned64 : CFType :: Word64
     -- simple boxed word64
     CFString : CFType -- magic
     CFDouble : CFType :: Double
     -- simple boxed double
     CFChar : CFType :: Char
     -- simple boxed char
     CFPtr : CFType -- not supported yet
     CFGCPtr : CFType -- not supported yet
     CFBuffer : CFType -- ???
     CFWorld : CFType -- ()
     -- we don't propagate information between the two worlds
     CFFun : CFType -> CFType -> CFType -- not supported yet
     CFIORes : CFType -> CFType :: IO
     -- IO computation
     CFStruct : String -> List (String, CFType) -> CFType -- not supported yet
     CFUser : Name -> List CFType -> CFType -- plain supported
     -- for the first iteration we need to support simple, non parametric types.
     -- This is mainly for user defined ADTs

     -- An interesting question is how to represent type classes from the Haskell world.
-}

{-
Question: How to represent CFTypes?
I think if these should be Boxed datatypes in Haskell.

The interesting ones are:
CFString : CFType -- Simple string, can't be part of the Struct.
CFPtr : CFType -- Pointer to a complex type AnyPtr is compiled to this one.
CFGCPtr : CFType
  -- Produced by the onCollect : Ptr t -> (Ptr t -> IO ()) -> IO (GCPtr t)
  -- it creates a pointer which has a finaliser assoicated with it.
CFBuffer : CFType
  -- From Data.Buffer A Byte buffer of size N
CFFun : CFType -> CFType -> CFType
  -- Probably lambda function, coming from NBind with something Closure related.
CFIORes : CFType -> CFType
  -- Represents PrimIO operations such as:
  -- %foreign "C:idris2_getStr,libidris2_support"
              "node:support:getStr,support_system_file"
     prim__getStr : PrimIO String
  -- will lead to: IORes String
  -- exprFromString: (Prelude.IO.prim__putStr, ([String, %World], IORes Unit))
  -- exprFromString: (Prelude.IO.prim__getStr, ([%World], IORes String))
  -- pure functions does not include the %World type:
  -- exprFromString: (Data.Strings.fastUnpack, ([String], Prelude.Types.List Char))
  -- In STG there is no difference in IO and pure. primitive functions may operate on
  -- WorldState, this needs more investigation.
CFStruct : String -> List (String, CFType) -> CFType
  -- Comes from System.FFI
CFUser : Name -> List CFType -> CFType
  -- User defined type.
  -- Some types needs to be mapped too. Like Prelude.Types.List
  -- Nat, Pair, Maybe, Dec, Either, List, Stream, (Cast?)

TODO: Find all [external] types, and report them, the foreign implementations
should be the reponsible for creating such parts.
TODO: What is the difference between %foreign and %extern
-}

record Foreign where
  constructor MkForeign
  name     : Name.Name
  fargs    : List CFType
  ret      : CFType
  topLevel : TopBinding

||| Matches and removes the "stg:" prefix
stgForeign : String -> Maybe String
stgForeign s =
  let xs = unpack s
  in if isPrefixOf "stg:" s
      then Just $ pack $ drop 4 xs
      else Nothing

data ForeignOp
  = ForeignExtName ExtName
  | ForeignPrimOp STG.Name

parsePrimOp : String -> Maybe STG.Name
parsePrimOp str = case unpack str of
  ('#' :: xs) => Just $ pack xs
  _           => Nothing

parseForeignStr : String -> Maybe ForeignOp
parseForeignStr str =
  (ForeignExtName <$> parseName str) <|>
  (ForeignPrimOp <$> parsePrimOp str)

argSgFromBinderSg : {r : RepType} -> SBinder r -> ArgSg
argSgFromBinderSg {r} b = (r ** (StgVarArg (binderId b)))

{-
Lookup if the give String is a primitive operation: no dots and ends in #
For primitives, unwrap the values, call the primitive, wrap the result
For non-primitives, every data like thing is considered as Lifted, just call the function
TODO: We need to handle the GHC calling convention right.
-}

toBinders
  :  UniqueMapRef
  => Ref Counter Int
  => Name.Name
  -> (cf : List (Nat,CFType))
  -> Core (BinderList (replicate (length cf) LiftedRep))
toBinders nm [] = pure []
toBinders nm ((k,x) :: xs) = do
  bdr <- mkSBinderLocal emptyFC nm (cast k)
  map (bdr ::) (toBinders nm xs)

toSBinderSgList : {rs : List PrimRep} -> BinderList rs -> List SBinderSg
toSBinderSgList [] = []
toSBinderSgList (x :: y) = mkSBinderSg x :: toSBinderSgList y

toArgSgList : {rs : List PrimRep} -> ArgList rs -> List ArgSg
toArgSgList [] = []
toArgSgList (x :: xs) = mkArgSg x :: toArgSgList xs

{-
System.IO.putStr : String -> IO ()
GHC.CString.unpackCString# : Addr# -> String
-}

getExtName
  :  Ref ExternalBinder ExtBindMap
  => UniqueMapRef
  => Ref Counter Int
  => ExtName -> Core (BinderId (SingleValue LiftedRep))
getExtName ename = do
  ((SingleValue LiftedRep) ** something) <- extName ename
    | _ => coreFail $ InternalError "....."
  pure something

{-
1. Create binders for all the parameters, there are special ones that needs transformation, for
   those we need to return a binder and an expression which bind the new value
2. For the return value we also need to do some kind of mapping.
   If the return value is non IO simple wrapping is enough, if we have IO we need to
   apply an extra void value to trigger the evaluation in GHCRuntime, the return
   value needs to be matched against an unboxed tuple.

Examples

1) Pure function
%foreign "stg: unit_Module.s.f"
haskellF : Int -> Int

This is a simple case, no need for wrapping values neither on the input, neither on the
output side. Its translation is like:

TopBinding haskellF [intBinder] = StgApp (mkExtName "unit" ["Module", "s"] "f") [intBinder]

2) IO () function
%foreign "stg: base_System.IO.putChar"
haskellF : Char -> IO ()

This is a simple case on the input side, but a complex on the output side as we need to use
an IO function, from the haskell library.

TopBinding haskellF [charBinder, worldBinder]
  = VoidBinder $ \voidBinder ->
    Seq  (StgApp (mkExtName "base" ["System", "IO"] "putChar") [charBinder, voidBinder]) $
    Bind (StgConApp mkUnitDataConId []) $ \unitBinder ->
    Done (StgConApp mkIOResDataConId [unitBinder, worldBinder])

3) IO with conversion
%foreign "stg: unit_Module.s.conversion"
haskellF : Double -> IO Int

This is similar to previous case, but it needs to return the right Integer coming from
the Haskell world.

TopBinding haskellF [doubleBinder, worldBinder]
  = VoidBinder $ \voidBinder ->
    Bind (StgApp (mkE "unit" ["Module", "s"] "conversion") [doubleBinder, voidBinder] $ \intBdrTpl ->
    Unwrap intBdrTpl $ \intBdr ->
    Done (StgConApp mkIOResDataConId [intBdr, worldBinder])

4) String function
%foreign "stg: unit_Module.s.func"
haskellF : String -> Int

Idris has different String representation than Haskell, the example below shows, first calling
the haskell function we need to convert the Idris String. When we get the Int that is
compatible with the Idris represented Int.

5) A function that returns a String
%foreign "stg: unit_Module.s.func"
haskellF : Int -> String

We need to write a function that traverses a Haskell list and calculates its length, and
creates an array, and copies the characters from the list.
Check one STG module where the list is used in some function, something from the base.

6) Handling [external] datatypes

-}

||| Convert the given String to STG, if it doesn't parse raise an InternalError
partial
exprFromString
  :  UniqueMapRef
  => Ref Counter Int
  => Ref ExternalBinder ExtBindMap
  => DataTypeMapRef
  => Name.Name -> (List CFType) -> CFType -> String
  -> Core TopBinding
exprFromString nm [CFString, CFWorld] (CFIORes CFUnit) str = do
  let Just en = parseForeignStr str
    | Nothing => coreFail $ InternalError $ "FFI name parsing has failed for " ++ str
  -- TODO: File location in the FFI file.
  -- TODO: Make this use of Vector
  [stringArg, worldArg] <- toBinders nm (numberFrom 0 [CFString, CFWorld])
    | _ => coreFail $ InternalError "..."
  addrBinder <- mkSBinderRepLocal (SingleValue AddrRep) emptyFC nm 3
  stringBinder <- mkSBinderLocal emptyFC nm 4
  mkUnitBinder <- mkSBinderLocal emptyFC nm 5
  voidBinder <- mkSBinderHardcoded hardcodedVoidHash emptyFC
  ((SingleValue LiftedRep) ** ghcCStringUnpackString)
    <- extName $ MkExtName "ghc-prim" ["GHC","CString"] "unpackCString#"
        | _ => coreFail $ InternalError "....."
  ((SingleValue LiftedRep) ** systemIOputStr)
    <- extName $ MkExtName "base" ["System", "IO"] "putStr"
        | _ => coreFail $ InternalError "..."
  ((AlgDataCon []) ** mkUnitDataConId) <- mkDataConIdStr "Builtin.MkUnit"
    | _ => coreFail $ InternalError "Missing Builtin.MkUnit data constructor."
  ((AlgDataCon [LiftedRep, LiftedRep]) ** mkIOResDataConId) <- mkDataConIdStr "PrimIO.MkIORes"
    | _ => coreFail $ InternalError "Missing PrimIO.MkIORes data constructor."
  pure
    $ StgTopLifted
    $ StgNonRec !(mkSBinderName emptyFC nm)
    $ StgRhsClosure ReEntrant (toSBinderSgList [stringArg, worldArg])
    $ StgCase
        (PrimAlt AddrRep)
        (StgApp
          !addrFromStringBinderId
          [mkArgSg (StgVarArg (binderId stringArg))]
          (SingleValue AddrRep))
        addrBinder
        [ MkAlt AltDefault ()
        $ StgCase
            PolyAlt -- because we only do default pattern matching
            (StgApp
              ghcCStringUnpackString
              [mkArgSg (StgVarArg (binderId addrBinder))]
              (SingleValue LiftedRep))
            stringBinder
            [ MkAlt AltDefault ()
            $ StgCase
                PolyAlt
                (StgApp
                  systemIOputStr
                  [ mkArgSg (StgVarArg (binderId stringBinder))
                  , mkArgSg (StgVarArg (binderId voidBinder))
                  ]
                  (SingleValue LiftedRep))
                !nonused
                [ MkAlt AltDefault ()
                $ StgCase
                    PolyAlt
                    (StgConApp mkUnitDataConId ())
                    mkUnitBinder
                    [ MkAlt AltDefault ()
                    $ StgConApp mkIOResDataConId
                        [ StgVarArg (binderId mkUnitBinder)
                        , StgVarArg (binderId worldArg)
                        ]
                    ]
                ]
                -- [ MkAlt AltDefailt () $ StgConApp MkIORes [StgVarArg MkUnit, StgVarArg worldArg] ]
            ]
        ]
exprFromString nm fargs ret str = do
  coreFail $ InternalError $ "exprFromString: " ++ show (nm, fargs, ret, str)

-- CString: Binary literal:
-- https://hackage.haskell.org/package/ghc-prim-0.6.1/docs/GHC-CString.html
-- IO in STG is not a concept. We need to apply a Void there. We need to use Void primitive.
-- It needs a special argument: Argument => BuiltIn Void

FOREIGN_DIR : String
FOREIGN_DIR = "./.foreign"

||| Search in the content of the file for 'name = stg' pattern
findForeign : String -> String -> Core String
findForeign name content = do
  let [stg] = mapMaybe
                (\ln => case break (=='=') ln of
                          ("", rest) => Nothing
                          (x, rest)  => if (trim x == trim name)
                                          then Just $ trim $ pack $ drop 1 $ unpack rest
                                          else Nothing)
            $ toList $ lines content
      | other => coreFail $ InternalError $ unwords
                  [ "Found none or more than one foreign for"
                  , name
                  , ":"
                  , show other
                  ]
  pure stg

||| Use the fully qualified name to create a path in the foreign, if the Foreign is not
||| found an InternalError is raised, if the foreign can not be parsed an InternalError is raised.
partial
findForeignInFile
  :  UniqueMapRef
  => Ref Counter Int
  => Ref Ctxt Defs
  => Ref ExternalBinder ExtBindMap
  => DataTypeMapRef
  => Name.Name -> List CFType -> CFType
  -> Core TopBinding
findForeignInFile nm fargs ret = do
  -- TODO: Make this more efficient with bulk loading of data.
  fn <- toFullNames nm
  -- logLine $ "Foreign name: " ++ show fn
  case fn of
    (NS ns (UN n)) => do
      let path = concat $ intersperse "/" $ (FOREIGN_DIR ::) $ toList $ split (=='.') $ show ns
      let filePath = path ++ ".stgffi"
      -- logLine $ "looking up file: " ++ filePath
      Right content <- coreLift $ readFile filePath
        | Left err => coreFail $ InternalError $ unwords
                        [ "Trying to resolve foreign definition"
                        , show fn
                        , "and got file error searching in foreign files:"
                        , show err
                        ]
      expr <- findForeign n content
      exprFromString fn fargs ret expr
    other => coreFail $ InternalError $ "Name not in namespace format: " ++ show other

||| Tries to find the definition in the given ccs parameter, if there is no Haskell definition
||| there, it tries to lookup in the .foreign/ files, the directory structure follows the
||| full qualified names path.
export
partial
foreign
  :  UniqueMapRef
  => Ref Counter Int
  => Ref Ctxt Defs
  => Ref ExternalBinder ExtBindMap
  => DataTypeMapRef
  => Name.Name -> (ccs : List String) -> (fargs : List CFType) -> (ret : CFType)
  -> Core TopBinding
foreign n css fargs ret = case mapMaybe stgForeign css of
  []    => findForeignInFile n fargs ret
  [str] => exprFromString n fargs ret str
  _     => coreFail $ InternalError $ "More than one foreign definition for: " ++ show n

max_stars_repo_name: andorp/IdrisExtSTGCodegen

max_issues_repo_name: andorp/IdrisExtSTGCodegen

max_forks_repo_name: andorp/IdrisExtSTGCodegen


text:
test1 : Int -> Int
test1 0x100 = 42
test1 0o100 = 43
test1 1234567890 = 44
test1 _         = 0


text:
module DataStore

import Data.Vect

infixr 5 .+.

public export
data Schema = SString | SInt | (.+.) Schema Schema

public export
SchemaType : Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

export
record DataStore (schema : Schema) where
    constructor MkData
    size : Nat
    items : Vect size (SchemaType schema)

export
empty : DataStore schema
empty = MkData 0 []

export
addToStore : (value : SchemaType schema) -> (store : DataStore schema) -> DataStore schema
addToStore value (MkData _ items) = MkData _ (value :: items)

public export
data StoreView : DataStore schema -> Type where
    SNil : StoreView empty
    SAdd : (rec : StoreView store) -> StoreView (addToStore value store)

storeViewHelp : (items : Vect size (SchemaType schema)) -> StoreView (MkData size items)
storeViewHelp [] = SNil
storeViewHelp (val :: xs) = SAdd (storeViewHelp xs)

export
storeView : (store : DataStore schema) -> StoreView store
storeView (MkData size items) = storeViewHelp items


text:
module Aliens

import Effect.SDL

record Alien : Type where
    MkAlien : (position : (Int, Int)) ->
              (xmovement : Int) ->
              (xstep : Int) ->
              (ystep : Int) -> Alien

startAliens : List Alien
startAliens = alienRow (-1) 100 ++
              alienRow 1 150 ++ alienRow (-1) 200
  where
    alienRow : Int -> Int -> List Alien
    alienRow mv y = map (\x => MkAlien (x*60, y) mv 30 15) [1..10]

move : List (Int, Int) -> -- bullet position
       List Alien -> List Alien
move bs as = map moveAlien as
  where moveAlien a = let xstep' = if (xstep a == 0) then 30 else xstep a - 1 in
                      let ystep' = if (ystep a == 0) then 15 else ystep a - 1 in
                      let (x, y) = position a in
                      let y' = if (ystep a == 0) then y+1 else y in
                      let xmovement' = if xstep a == 0 then -(xmovement a)
                                                       else xmovement a in
                      record { position = (x + xmovement a, y'),
                               xmovement = xmovement',
                               xstep = xstep',
                               ystep = ystep' } a

-- if any pair of bullet/alien collide, remove both
checkHit : List (Int, Int) -> List Alien -> (List (Int, Int), List Alien)
checkHit bs as = checkAll bs as [] []
  where testHit : (Int, Int) -> Alien -> Bool
        testHit (x, y) a
            = let (ax, ay) = position a in
                  (abs (x - ax) < 20 && abs (y - ay) < 15) -- hit!

        checkAll : List (Int, Int) -> List Alien -> List Alien -> List (Int, Int) ->
                   (List (Int, Int), List Alien)
        checkAll (b :: bs) (a :: as) asAcc bsAcc
            = if testHit b a
                 then checkAll bs as asAcc bsAcc
                 else checkAll (b :: bs) as (a :: asAcc) bsAcc
        checkAll (b :: bs) [] asAcc bsAcc
            = checkAll bs asAcc [] (b :: bsAcc)
        checkAll [] as asAcc bsAcc = (bsAcc, as ++ asAcc)

drawAliens : List Alien -> { [SDL_ON] } Eff IO ()
drawAliens [] = return ()
drawAliens (a :: as) = do let (x, y) = Alien.position a
                          drawAlien x y
                          drawAliens as
    where drawAlien : Int -> Int -> { [SDL_ON] } Eff IO ()
          drawAlien x y = do ellipse green x y 20 16
                             ellipse red (x-8) (y-6) 3 3
                             ellipse red (x-8) (y+6) 3 3
                             rectangle red (x-2) (y-3) 16 4
                             rectangle red (x-2) (y+3) 16 4

max_stars_repo_name: silky/idris-demos

max_issues_repo_name: silky/idris-demos

max_forks_repo_name: silky/idris-demos


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

import Effects
import Effect.State

import Edda
import Edda.Query

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

import Readability.Process.Effs
import public Readability.Process.Common

-- ----------------------------------------------------------------- [ Queries ]
||| Extract text from inlined elements.
extractText : Edda PRIME INLINE -> List String
extractText (Text t) = [t]
extractText _        = Nil

||| Extract paragraphs from documents.
extractPara : Edda PRIME BLOCK -> List (Edda PRIME BLOCK)
extractPara (Para txt) = [Para txt]
extractPara _          = Nil

||| Do extraction of paragraphs from a document.
getParas : Edda PRIME MODEL -> List (Edda PRIME BLOCK)
getParas = query extractPara

-- --------------------------------------------------------- [ Stat Collection ]

||| Extract Sentences from a paragraph.
getSentances : (Edda PRIME BLOCK) -> List (List (Edda PRIME INLINE))
getSentances (Para txt) = doSplit txt
  where
    isEOS : (Edda PRIME INLINE) -> Bool
    isEOS e = List.elem e [Period, Colon, Bang, QMark, SMark]

    doSplit : List (Edda PRIME INLINE) -> List (List (Edda PRIME INLINE))
    doSplit xs = filter (\x => x /= Nil) (List.split (isEOS) xs)

||| Process a paragraph, which is a list of sentences.
processPara : List (List (Edda PRIME INLINE)) -> Eff () ReadEffs
processPara Nil     = pure ()
processPara (s::ss) = do
  processSentence (query extractText s)
  updateReadState (\x => record {sentances = (sentances x) + 1} x)
  processPara ss

||| Process paragraphs.
processParas : List (Edda PRIME BLOCK) -> Eff () ReadEffs
processParas Nil      = pure ()
processParas (p::ps) = do
  processPara (getSentances p)
  processParas ps

export
calcReadabilityE : Edda PRIME MODEL
                -> Eff (Maybe ReadResult) ReadEffs
calcReadabilityE doc = do
    case getParas doc of
      Nil => pure Nothing
      ps  => do
        processParas ps
        res <- getReadState
        pure $ Just (calcScores res)

export
calcReadability : Edda PRIME MODEL -> Maybe ReadResult
calcReadability doc = runPure $ calcReadabilityE doc

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

max_stars_repo_name: jfdm/idris-read

max_issues_repo_name: jfdm/idris-read

max_forks_repo_name: jfdm/idris-read


text:
module Data.List.Predicates.Pairs

import public Data.List

import public Data.List.Predicates.Interleaving
import public Data.List.Predicates.Unique

%default total
%access public export

||| Proof that the contents of the given list of pairs originate from
||| a secondary list.
data PairsFromList : (pairs  : List (ty,ty))
                  -> (origin : List ty)
                  -> Type
  where
    NilPair : PairsFromList Nil as
    PairIn  : Elem a as
           -> Elem b as
           -> PairsFromList abs            as
           -> PairsFromList ((a,b) :: abs) as

||| Proof that the given list of paired elements originate from the
||| two given lists such that the following hold:
|||
|||    SubList (map fst pairs) as
|||
||| and
|||
|||    SubList (map snd pairs) bs
|||
data UnZipPairs : (pairs : List (ty,ty))
               -> (as    : List ty)
               -> (bs    : List ty)
               -> Type
  where
    UnZipOne  : UnZipPairs Nil as bs
    UnZipPair : (prf_a : Elem a as)
             -> (prf_b : Elem b bs)
             -> (rest  : UnZipPairs abs as bs)
             -> UnZipPairs ((a,b) :: abs) as bs

||| Proof that the given list of paired elements not only originate
||| from the given lists, but that all elements are unique.
data UZipPairsU : (pairs : List (ty,ty))
               -> (as    : List ty)
               -> (bs    : List ty)
               -> Type
  where
    ValidUSPU : (uniqueAs  : Unique as)
             -> (uniqueBs  : Unique bs)
             -> (uniqueABs : Unique (as ++ bs))
             -> (vswap     : UnZipPairs cs as bs)
             -> UZipPairsU cs as bs

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


text:
{-
$ cd collatzProof_DivSeq/program3
$ chcp 65001
$ idris
> :l ProofColDivSeqMain
-}
module ProofColDivSeqMain

import ProofColDivSeqBase as B
import ProofColDivSeqPostulate
import Sub02LTE72t45
import Sub03LTE216t81
import Sub04LTE216t153
import Sub05LTE216t225
import Sub06LTE108t27
import Sub07LTE108t63
import Sub08LTE108t99
import Sub09LTE18t15
import Sub11LTE36t21
import Sub12LTE108t39
import Sub13LTE108t75
import Sub14LTE108t111

%default total

-- 示すのに、整礎帰納法を使っている
makeLimitedDivSeq :
  ((z : Nat) -> ((FirstLimited . B.allDivSeq) z -> (AllLimited . B.allDivSeq) z))
    ->  (n : Nat) -> (FirstLimited . B.allDivSeq) n
makeLimitedDivSeq firstToAll n = wfInd {P=(\z=>(FirstLimited . B.allDivSeq) z)} {rel=LT'} (step firstToAll) n where
  step : ((z : Nat) -> ((FirstLimited . B.allDivSeq) z -> (AllLimited . B.allDivSeq) z))
    -> (x : Nat) -> ((y : Nat) -> LT' y x -> (FirstLimited . B.allDivSeq) y)
      -> (FirstLimited . B.allDivSeq) x
  step _          Z     _  = IsFirstLimited10                                                          -- 6*<0>+3 = 3
  step firstToAll (S x) rs with (mod3 x)
    -- 0 mod 9
    step firstToAll (S (j + j + j)) rs | ThreeZero with (parity j)
      step firstToAll (S ((Z+Z) + (Z+Z) + (Z+Z)))             rs | ThreeZero | Even = IsFirstLimited01 -- 6*<1>+3 = 9
      step firstToAll (S (((S k)+(S k)) + ((S k)+(S k)) + ((S k)+(S k))))             rs | ThreeZero | Even with (parity k)
        step firstToAll (S (((S (l+l))+(S (l+l))) + ((S (l+l))+(S (l+l))) + ((S (l+l))+(S (l+l)))))                         rs | ThreeZero | Even | Even
          = (IsFirstLimited02 l . firstToAll l) (rs l $ lteToLt' $ lte72t45 l)
        step firstToAll (S (((S (S (l+l)))+(S (S (l+l)))) + ((S (S (l+l)))+(S (S (l+l)))) + ((S (S (l+l)))+(S (S (l+l)))))) rs | ThreeZero | Even | Odd  with (mod3 l)
          step firstToAll (S (((S (S ((m+m+m)+(m+m+m))))+(S (S ((m+m+m)+(m+m+m))))) + ((S (S ((m+m+m)+(m+m+m))))+(S (S ((m+m+m)+(m+m+m))))) + ((S (S ((m+m+m)+(m+m+m))))+(S (S ((m+m+m)+(m+m+m)))))))                                                                                rs | ThreeZero | Even | Odd | ThreeZero
            = (IsFirstLimited03 m . firstToAll (m+m)) (rs (m+m) $ lteToLt' $ lte216t81 m)
          step firstToAll (S (((S (S ((S (m+m+m))+(S (m+m+m)))))+(S (S ((S (m+m+m))+(S (m+m+m)))))) + ((S (S ((S (m+m+m))+(S (m+m+m)))))+(S (S ((S (m+m+m))+(S (m+m+m)))))) + ((S (S ((S (m+m+m))+(S (m+m+m)))))+(S (S ((S (m+m+m))+(S (m+m+m))))))))                                                 rs | ThreeZero | Even | Odd | ThreeOne
            = (IsFirstLimited04 m . firstToAll (S ((m+m)+(m+m)))) (rs (S ((m+m)+(m+m))) $ lteToLt' $ lte216t153 m)
          step firstToAll (S (((S (S ((S (S (m+m+m)))+(S (S (m+m+m))))))+(S (S ((S (S (m+m+m)))+(S (S (m+m+m))))))) + ((S (S ((S (S (m+m+m)))+(S (S (m+m+m))))))+(S (S ((S (S (m+m+m)))+(S (S (m+m+m))))))) + ((S (S ((S (S (m+m+m)))+(S (S (m+m+m))))))+(S (S ((S (S (m+m+m)))+(S (S (m+m+m))))))))) rs | ThreeZero | Even | Odd | ThreeTwo
            = (IsFirstLimited05 m . firstToAll (S (S (S (S (S (S (S (m+m+m+m)+(m+m+m+m))))))))) (rs (S (S (S (S (S (S (S (m+m+m+m)+(m+m+m+m)))))))) $ lteToLt' $ lte216t225 m)
      step firstToAll (S ((S (k+k)) + (S (k+k)) + (S (k+k)))) rs | ThreeZero | Odd  with (mod3 k)
        step firstToAll (S ((S ((l+l+l)+(l+l+l))) + (S ((l+l+l)+(l+l+l))) + (S ((l+l+l)+(l+l+l)))))                                                 rs | ThreeZero | Odd | ThreeZero
          = (IsFirstLimited06 l . firstToAll (S (S (S (l+l+l+l)+(l+l+l+l)+(l+l+l+l)+(l+l+l+l))))) (rs (S (S (S (l+l+l+l)+(l+l+l+l)+(l+l+l+l)+(l+l+l+l)))) $ lteToLt' $ lte108t27 l)
        step firstToAll (S ((S ((S (l+l+l))+(S (l+l+l)))) + (S ((S (l+l+l))+(S (l+l+l)))) + (S ((S (l+l+l))+(S (l+l+l))))))                         rs | ThreeZero | Odd | ThreeOne
          = (IsFirstLimited07 l . firstToAll (S (S (S (S (l+l+l+l)+(l+l+l+l)))))) (rs (S (S (S (S (l+l+l+l)+(l+l+l+l))))) $ lteToLt' $ lte108t63 l)
        step firstToAll (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))))))) rs | ThreeZero | Odd | ThreeTwo
          = (IsFirstLimited08 l . firstToAll (S (S (S ((l+l)+(l+l)))))) (rs (S (S (S ((l+l)+(l+l))))) $ lteToLt' $ lte108t99 l)
    -- 6 mod 9
    step firstToAll (S (S (j + j + j)))     rs | ThreeOne
      = (IsFirstLimited09 j . firstToAll j) (rs j $ lteToLt' $ lte18t15 j)
    -- 3 mod 9
    step firstToAll (S (S (S (j + j + j)))) rs | ThreeTwo with (parity j)
      step firstToAll (S (S (S (   (k+k)  +    (k+k)  +    (k+k)))))  rs | ThreeTwo | Even
        = (IsFirstLimited11 k . firstToAll k) (rs k $ lteToLt' $ lte36t21 k)
      step firstToAll (S (S (S ((S (k+k)) + (S (k+k)) + (S (k+k)))))) rs | ThreeTwo | Odd  with (mod3 k)
        step firstToAll (S (S (S ((S ((l+l+l)+(l+l+l))) + (S ((l+l+l)+(l+l+l))) + (S ((l+l+l)+(l+l+l)))))))                                                 rs | ThreeTwo | Odd  | ThreeZero
          = (IsFirstLimited12 l . firstToAll (l+l)) (rs (l+l) $ lteToLt' $ lte108t39 l)
        step firstToAll (S (S (S ((S ((S (l+l+l))+(S (l+l+l)))) + (S ((S (l+l+l))+(S (l+l+l)))) + (S ((S (l+l+l))+(S (l+l+l))))))))                         rs | ThreeTwo | Odd  | ThreeOne
          = (IsFirstLimited13 l . firstToAll (S ((l+l)+(l+l)))) (rs (S ((l+l)+(l+l))) $ lteToLt' $ lte108t75 l)
        step firstToAll (S (S (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))))))))) rs | ThreeTwo | Odd  | ThreeTwo
          = (IsFirstLimited14 l . firstToAll (S (S (S (S (S (S (S (l+l+l+l)+(l+l+l+l))))))))) (rs (S (S (S (S (S (S (S (l+l+l+l)+(l+l+l+l)))))))) $ lteToLt' $ lte108t111 l)

-- 十分条件
firstToAll :
  (z : Nat) -> ((FirstLimited . B.allDivSeq) z -> (AllLimited . B.allDivSeq) z)
firstToAll z first =
  let
    suff2_1 = IsFirstLimitedSuff2_1 z first
    suff2_2 = IsFirstLimitedSuff2_2 z first
    suff2_3 = IsFirstLimitedSuff2_3 z first
    suff2_4 = IsFirstLimitedSuff2_4 z first
    suff2_5 = IsFirstLimitedSuff2_5 z first
    suff2_6 = IsFirstLimitedSuff2_6 z first
    all2    = IsAllLimited02 z suff2_1 suff2_2 suff2_3 suff2_4 suff2_5 suff2_6
    suff3_1 = IsFirstLimitedSuff3_1 z first
    suff3_2 = IsFirstLimitedSuff3_2 z first
    suff3_3 = IsFirstLimitedSuff3_3 z first
    suff3_4 = IsFirstLimitedSuff3_4 z first
    suff3_5 = IsFirstLimitedSuff3_5 z first
    suff3_6 = IsFirstLimitedSuff3_6 z first
    all3    = IsAllLimited03 z suff3_1 suff3_2 suff3_3 suff3_4 suff3_5 suff3_6
    suff4_1 = IsFirstLimitedSuff4_1 z first
    suff4_2 = IsFirstLimitedSuff4_2 z first
    suff4_3 = IsFirstLimitedSuff4_3 z first
    suff4_4 = IsFirstLimitedSuff4_4 z first
    suff4_5 = IsFirstLimitedSuff4_5 z first
    all4    = IsAllLimited04 z suff4_1 suff4_2 suff4_3 suff4_4 suff4_5
    suff5_1 = IsFirstLimitedSuff5_1 z first
    suff5_2 = IsFirstLimitedSuff5_2 z first
    suff5_3 = IsFirstLimitedSuff5_3 z first
    suff5_4 = IsFirstLimitedSuff5_4 z first
    suff5_5 = IsFirstLimitedSuff5_5 z first
    suff5_6 = IsFirstLimitedSuff5_6 z first
    all5    = IsAllLimited05 z suff5_1 suff5_2 suff5_3 suff5_4 suff5_5 suff5_6
    suff6_1 = IsFirstLimitedSuff6_1 z first
    suff6_2 = IsFirstLimitedSuff6_2 z first
    suff6_3 = IsFirstLimitedSuff6_3 z first
    suff6_4 = IsFirstLimitedSuff6_4 z first
    suff6_5 = IsFirstLimitedSuff6_5 z first
    suff6_6 = IsFirstLimitedSuff6_6 z first
    all6    = IsAllLimited06 z suff6_1 suff6_2 suff6_3 suff6_4 suff6_5 suff6_6
    suff7_1 = IsFirstLimitedSuff7_1 z first
    suff7_2 = IsFirstLimitedSuff7_2 z first
    suff7_3 = IsFirstLimitedSuff7_3 z first
    suff7_4 = IsFirstLimitedSuff7_4 z first
    suff7_5 = IsFirstLimitedSuff7_5 z first
    suff7_6 = IsFirstLimitedSuff7_6 z first
    suff7_7 = IsFirstLimitedSuff7_7 z first
    all7    = IsAllLimited07 z suff7_1 suff7_2 suff7_3 suff7_4 suff7_5 suff7_6 suff7_7
    suff8_1 = IsFirstLimitedSuff8_1 z first
    suff8_2 = IsFirstLimitedSuff8_2 z first
    suff8_3 = IsFirstLimitedSuff8_3 z first
    suff8_4 = IsFirstLimitedSuff8_4 z first
    suff8_5 = IsFirstLimitedSuff8_5 z first
    suff8_6 = IsFirstLimitedSuff8_6 z first
    all8    = IsAllLimited08 z suff8_1 suff8_2 suff8_3 suff8_4 suff8_5 suff8_6
  in IsAllLimited01 z IsAllLimited00 all2 all3 all4 all5 all6 all7 all8

-- 最終的な定理
limitedDivSeq : (n : Nat) -> (FirstLimited . B.allDivSeq) n
limitedDivSeq = makeLimitedDivSeq firstToAll


text:
module Data.GIS.Test

import Control.Algebra.NumericImplementations
import Data.GIS
import Data.Int.Algebra
import Data.Music

import Specdris.Spec

%access export

lewin2_1_1 : SpecTree
lewin2_1_1 = let int = int@{DiatonicPitchGIS} in
  describe "Diatonic pitch examples (Lewin, 2.1.1)" $ do
    it "int(C4, C4) = 0" $ do
      int (C, 4) (C, 4) === 0
    it "int(C4, D4) = 1" $ do
      int (C, 4) (D, 4) === 1
    it "int(C4, E4) = 2" $ do
      int (C, 4) (E, 4) === 2
    it "int(C4, C5) = 7" $ do
      int (C, 4) (C, 5) === 7
    it "int(C4, A3) = -2" $ do
      int (C, 4) (A, 3) === -2
    it "int(E4, G4) = 2" $ do
      int (E, 4) (G, 4) === 2
    it "int(C4, G4) = 4" $ do
      int (C, 4) (G, 4) === 4
    it "int(C4, E4) <+> int(E4, G4) = 4" $ do
      (<+>) (int (C, 4) (E, 4)) (int (E, 4) (G, 4)) === int (C, 4) (G, 4)

lewin2_1_2 : SpecTree
lewin2_1_2 = let int = int@{PSpaceGIS} in
  describe "p-space examples (Lewin, 2.1.2)" $ do
    it "int(C4, D4) = 2" $ do
      int (C, 4) (D, 4) === 2
    it "int(C4, G4) = 7" $ do
      int (C, 4) (G, 4) === 7
    it "int(C4, C5) = 12" $ do
      int (C, 4) (C, 5) === 12
    it "int(C4, F3) = -7" $ do
      int (C, 4) (F, 3) === -7
    it "int(C4, F2) = -19" $ do
      int (C, 4) (F, 2) === -19

lewin2_1_3 : SpecTree
lewin2_1_3 = let int = int@{PCSpaceGIS} in
  describe "pc-space examples (Lewin, 2.1.3)" $ do
    it "int(8, 1) = 5" $ do
      int (fromNat 8) (fromNat 1) === MkZn 5
    it "int(E, E) = 0" $ do
      int E E === MkZn 0
    it "int(E, F) = 1" $ do
      int E F === MkZn 1
    it "int(F, E) = 11" $ do
      int F E === MkZn 11

lewin2_1_4 : SpecTree
lewin2_1_4 = let int = int@{DiatonicPitchClassGIS} in
  describe "Diatonic pitch class examples (Lewin, 2.1.4)" $ do
    it "int(D, D) = 0" $ do
      int D D === MkZn 0
    it "int(D, E) = 1" $ do
      int D E === MkZn 1
    it "int(D, C) = 6" $ do
      int D C === MkZn 6

runTests : IO ()
runTests =
  flip for_ spec $
  [ lewin2_1_1
  , lewin2_1_2
  , lewin2_1_3
  , lewin2_1_4
  ]

max_stars_repo_name: yurrriq/gis

max_issues_repo_name: yurrriq/gis

max_forks_repo_name: yurrriq/gis


text:
module Network.Curl.Types.OptType

import Data.Buffer

import Network.Curl.Types.Code

import Derive.Enum
%language ElabReflection

public export
data OptType
  = UnusedOptType  -- -10, not part of curl, convenience
  | CURLOPTTYPE_LONG -- at east 32 bits -- 0
  | CURLOPTTYPE_OBJECTPOINT             -- 10000
  | CURLOPTTYPE_FUNCTIONPOINT -- void*  -- 20000
  | CURLOPTTYPE_OFF_T -- int64          -- 30000
  | CURLOPTTYPE_BLOB -- ???             -- 40000
  | CURLOPTTYPE_STRINGPOINT -- char*    -- 10000 -- aliases for OBJECTPOINT, useful for foreign decls
  -- | CURLOPTTYPE_SLISTPOINT              -- 10000 -- aliases for OBJECTPOINT

curlOptTypeEnumList : List Int
curlOptTypeEnumList = [-10,0,10000,20000,30000,40000,10000]

export
ToCode OptType where
  toCode = enumTo curlOptTypeEnumList

export
FromCode OptType where
  fromCode = enumFrom curlOptTypeEnumList

public export
optType : OptType -> Type
optType UnusedOptType = Void
optType CURLOPTTYPE_LONG = Int
optType CURLOPTTYPE_OBJECTPOINT = AnyPtr
optType CURLOPTTYPE_FUNCTIONPOINT = AnyPtr
optType CURLOPTTYPE_OFF_T = Bits64 -- maybe
optType CURLOPTTYPE_BLOB = Buffer -- I truly don't know what a blob is
optType CURLOPTTYPE_STRINGPOINT = String