text:
{- These files given an introductory look at programming in the (currently
 - pre-alpha) release of Idris2, a dependently typed programming language.
 - They can be run by installing Idris2 (not trivial at the moment), and
 - the interactive type-driven development features described are available
 - through the Idris Atom plugin. Not all features of dependently typed
 - programmming are touched on, most significantly equality proofs are not
 - discussed.
 -
 - While Haskell makes the claim "all values have types" Idris and other
 - dependently typed languages add the claim that "values are types and
 - types are values." -}

x : Int -- x has type Int (note the symbols : and :: are reversed from Haskell)
x = 4

y : Type -- y has type Type
y = Int  -- y's value is a type

z : Type -- the value Type has type Type as well.
z = Type

{- For proofs in our system to be sound, we should not have Type : Type
 - as this leads to paradoxes. We should instead have universes or levels
 - of types, i.e. Type : Type1, Type1 : Type2. This already exists in other
 - dependently typed languages and will eventually exist in Idris2. Don't
 - worry about this for now, as it will not be important to the examples.

 - To understand dependent types, we will first revisit polymorphism. What
 - are polymorphic values? They are functions on types. -}

-- Consider the polymorphic identity function
id : a -> a
id x = x

{- id2 below makes explicit in the type signature what is implicit above, that
 - it takes an initial {implicit} type argument and returns a monomorphic
 - identity function on that type. Since the value is implicit, Idris can
 - infer it from the other arguments. -}

id2 : {a : Type} -> a -> a -- takes a value `a` of type `Type`
id2 x = x                  -- and a value `x` of type `a`.

id3 : Int -> Int
id3 = id2 { a = Int } -- you can pass implicit arguments explicitly

{- We could also write an identity function with an explicit type parameter -}

id4 : (a : Type) -> a -> a
id4 a x = x

{- These are already examples of a "dependent type", where part of the type
 - (the type `a` of the second argument in this instance) depends on the
 - *value* `a` passed (possibly implicitly) as the first argument. -}


text:
module Constants

%default total

export
RamSize : Int
RamSize = 0x1000

export
StartingAddress : Int
StartingAddress = 0x200

-- we store default sprites in the interpreter space. this address is
-- arbitrarily chosen, but must fit in the range 0x000 to 0x1fff.
export
DefaultSpriteDataAddress : Int
DefaultSpriteDataAddress = 0x100

export
DefaultSpriteDataLength : Int
DefaultSpriteDataLength = 5

export
RandomSeed : Integer
RandomSeed = 1234567890

export
Scale : Int
Scale = 5

export
Width : Int
Width = 64

export
Height : Int
Height = 32

ext: idr


text:
module Main

import ErlPrelude

testFiles : EIO ()
testFiles = do putStrLn "testFiles"
               h <- openFile "test_file" Read
               putStrLn $ "read char from file: " ++ singleton !(fgetc h)
               putStrLn $ "read from file: " ++ !(fread h)
               if !(feof h) then putStrLn "EOF" else putStrLn "Not EOF"
               closeFile h
               h' <- openFile "other_file" Write
               fwrite h' "test"
               closeFile h'

-- testProcesses : IO ()
-- testProcesses = do putStrLn "testProcesses"
--                    h <- popen "echo 'foo'" Read
--                    putStrLn $ "read from echo: " ++ !(fread h)
--                    pclose h

testStrings : EIO ()
testStrings = do putStrLn "testStrings"
                 s <- return ""
                 if !(nullStr s) then putStrLn "null" else putStrLn "not null"

main : EIO ()
main = do testFiles
          -- testProcesses
          testStrings

max_stars_repo_name: lenary/idris-erlang

max_issues_repo_name: yurrriq/idris-erlang

max_forks_repo_name: yurrriq/idris-erlang


text:
||| A channel with a dedicated read and write end, built on top of
||| System.Concurrency.Queue. It is MTSafe thanks to Queues being MTSafe.
module System.Concurrency.Pipe

import System.Concurrency

import public System.Concurrency.Queue

||| A channel whose read end has type `rdT` and whose write end has type `wrT`.
export
data Pipe : (rdT : Type) -> (wrT : Type) -> Type where
  MkPipe : {0 a : Type} -> {0 b : Type}
         -> (inbox  : IORef (Queue a))
         -> (iCondLock : Mutex)
         -> (iCondVar : Condition)
         -> (outbox : IORef (Queue b))
         -> (oCondLock : Mutex)
         -> (oCondVar : Condition)
         -> Pipe a b

---------------------------
-- CONSTRUCTOR FUNCTIONS --
---------------------------

||| Create a new Pipe.
export
makePipe : IO (IORef (Pipe rdT wrT))
makePipe = do iQueue <- makeQueue
              iCondLock <- makeMutex
              iCondVar <- makeCondition
              -- ^ inbox/read things
              -- v outbox/write things
              oQueue <- makeQueue
              oCondLock <- makeMutex
              oCondVar <- makeCondition
              -- create the pipe in an IORef
              newIORef (MkPipe iQueue iCondLock iCondVar
                               oQueue oCondLock oCondVar)

||| Given an IORef to a Pipe, obtained through the `makePipe` function, create a
||| version which is primarily used for sending messages.
export
makeSender : (pRef : IORef (Pipe rdT wrT)) -> IO (Pipe rdT wrT)
makeSender pRef
  = do (MkPipe inbox iCL iCV outbox oCL oCV) <- readIORef pRef
       pure (MkPipe inbox iCL iCV outbox oCL oCV)

||| Given an IORef to a Pipe, obtained through the `makePipe` function, create a
||| version which is primarily used for receiving messages, possibly responding
||| on what appears as the `rd` end to the other process.
export
makeReceiver : (pRef : IORef (Pipe rdT wrT)) -> IO (Pipe wrT rdT)
makeReceiver pRef
  = do (MkPipe inbox iCL iCV outbox oCL oCV) <- readIORef pRef
       pure (MkPipe outbox oCL oCV inbox iCL iCV)

------------------------
-- INBOX MANIPULATION --
------------------------

getInbox : Pipe a b -> IORef (Queue a)
getInbox (MkPipe inbox _ _ _ _ _) = inbox

-------------------------
-- OUTBOX MANIPULATION --
-------------------------

getOutbox : Pipe a b -> IORef (Queue b)
getOutbox (MkPipe _ _ _ outbox _ _) = outbox

||| Unlock at least one of the threads currently waiting on the outbox's
||| condition variable.
signalOutbox : Pipe a b -> IO ()
signalOutbox (MkPipe _ _ _ _ _  oCondVar)
  = conditionSignal oCondVar

||| Unlock all of the threads currently waiting on the outbox's condition
||| variable.
broadcastOutbox : Pipe a b -> IO ()
broadcastOutbox (MkPipe _ _ _ _ _ oCondVar)
  = conditionBroadcast oCondVar

-------------
-- SENDING --
-------------

||| Send a thing through the Pipe and *signal* on the condition variable for the
||| Pipe's outbox to indicate to at least one blocking thread blocking on it,
||| that a thing can be received.
|||
||| @chan: The Pipe to send the thing through.
||| @thing: The thing to send.
|||
||| MTSafe: YES
export
sendAndSignal : (chan : Pipe rdT wrT) -> (thing : wrT) -> IO ()
sendAndSignal chan thing =
  do enqueue (getOutbox chan) thing
     signalOutbox chan

||| Send a thing through the Pipe and *broadcast* on the condition variable for
||| the Pipe's outbox to indicate to all threads currently blocking on it, that
||| a thing can be received.
|||
||| @chan: The Pipe to send the thing through.
||| @thing: The thing to send.
|||
||| MT-Safe: YES
export
sendAndBroadcast : (chan : Pipe rdT wrT) -> (thing : wrT) -> IO ()
sendAndBroadcast chan thing =
  do enqueue (getOutbox chan) thing
     broadcastOutbox chan

---------------
-- RECEIVING --
---------------

||| Crash Idris with a message signalling that something went wrong in terms of
||| the fundamental guarantees of condition variables.
|||
||| Essentially, the point of waiting on a CV is to wait until something is
||| available for consumption. So as soon as the CV lets us past, there will be
||| something to retrieve. However, Idris doesn't know this.
await_crash : IO a
await_crash =
  assert_total $ idris_crash "Await somehow got Nothing despite waiting on a CV"

||| Receive a thing through the Pipe, if there is one, removing it from the
||| inbox in the process. Does not block but immediately returns `Nothing` if
||| there was nothing available.
|||
||| @chan: The Pipe to receive the thing through.
|||
||| MT-Safe: YES
export
receive : (chan : Pipe rdT wrT) -> IO (Maybe rdT)
receive chan = dequeue (getInbox chan)

||| Similar to `receive`, but blocks on the condition variable of the inbox
||| until a thing is available, at which point it receives the thing, removing
||| it from the inbox in the process.
|||
||| @chan: The Pipe to receive the thing through.
|||
||| MT-Safe: YES
export
await : (chan : Pipe rdT wrT) -> IO rdT
await (MkPipe inbox iCondLock iCondVar _ _ _) =
  do (Just thing) <- dequeue inbox
          -- if at first you don't succeed...
        | Nothing => do mutexAcquire iCondLock
                        conditionWait iCondVar iCondLock
                        (Just thing') <- dequeue inbox
                            | Nothing => await_crash
                        mutexRelease iCondLock
                        -- ^  FIXME: necessary? Yes. Right place for it?
                        pure thing'

     pure thing

--------------
-- PEEK+SPY --
--------------

||| Receive a thing through the Pipe, if there is one, *without* removing
||| from the inbox in the process. Does not block but immediately returns
||| `Nothing` if there was nothing available.
|||
||| @chan: The Pipe to receive the thing through.
|||
||| MT-Safe: YES
export
peek : (chan : Pipe rdT wrT) -> IO (Maybe rdT)
peek (MkPipe inbox _ _ _ _ _) = peek inbox

||| Watches the Pipe until a thing appears, at which point it "reports back"
||| with the thing that arrived. Hence, `spy`.
|||
||| Similar to `peek`, but blocks on the condition variable of the inbox until a
||| thing is available, at which point it receives the thing, *without* removing
||| it from the Pipe's inbox in the process.
|||
||| @chan: The Pipe to receive the thing through.
|||
||| MT-Safe: YES
export
spy : (chan : Pipe rdT wrT) -> IO rdT
spy (MkPipe inbox iCondLock iCondVar _ _ _) =
  do (Just thing) <- peek inbox
        | Nothing => do mutexAcquire iCondLock
                        conditionWait iCondVar iCondLock
                        (Just thing') <- peek inbox
                            | Nothing => await_crash
                        mutexRelease iCondLock
                        -- ^  FIXME: necessary? Yes. Right place for it?
                        pure thing'
     pure thing


text:
module TaintExample

import Data.Tainted

data Expr =
  Number (Tainted Int)
  | Add Expr Expr

instance Show Expr where
  show (Number x) = "Number (" ++ show x ++ ")"
  show (Add e1 e2) = "Add " ++ show e1 ++ " " ++ show e2

pure1 : Expr
pure1 = Number (Clean 3)

pure2 : Expr
pure2 = Number (Clean 7)

impure1 : Expr
impure1 = Number (Dirty 5)

expr1 : Expr
expr1 = Add pure1 pure2

expr2 : Expr
expr2 = Add impure1 pure1

expr3 : Expr
expr3 = Add pure1 (Add impure1 pure2)

--Evaluate expression as much as Possible
evalExpr : Expr -> Expr
evalExpr (Number n) = Number n
evalExpr (Add e1 e2) =
    case (evalExpr e1, evalExpr e2) of
            (Number i, Number j) => Number $ liftA2 (+) i j
            (x, y) => Add x y

reducedExpr1 : Expr
reducedExpr1 = evalExpr expr1

reducedExpr2 : Expr
reducedExpr2 = evalExpr expr2

reducedExpr3 : Expr
reducedExpr3 = evalExpr expr3

max_stars_repo_name: RossMeikleham/Idris-Tainted

max_issues_repo_name: RossMeikleham/Idris-Tainted

max_forks_repo_name: RossMeikleham/Idris-Tainted


text:
import Data.Vect
%default total
data Info = String

data Term = TmVar Info Nat Nat
          | TmAbs Info String Term
          | TmApp Info Term Term
%name Term t, t1, t2, t3

data Binding = NameBind

Context : Nat -> Type
Context k = Vect k (String, Binding)
%name Context context, context1, context2, context3

data Command = Eval Info Term
             | Bind Info String Binding

Show Binding where
  show NameBind = ""

emptyContext : Context 0
emptyContext = []

contextLength : Context n -> Nat
contextLength x {n} = n

addBinding : Context n -> String -> Binding -> Context (S n)
addBinding context name binding = (name, binding) :: context

addName : Context n -> String -> Context (S n)
addName context name = addBinding context name NameBind

isNameBound : Context n -> String -> Bool
isNameBound context name = case context of
                                [] => False
                                ((bound_name, _) :: xs) =>
                                                   if bound_name == name
                                                      then True
                                                      else isNameBound xs name

pickFreshName : (context : Context n) ->
                (name : String) ->
                {auto prf : Elem (name, _) context} ->
                Context (S n)
pickFreshName context name = (name ++ "'", NameBind) :: context

contextIndex : (a : Nat) -> {auto prf : LT 0 a} -> Nat
contextIndex (S a) {prf = (LTESucc x)} = a

indexToName : (context : Context n) -> Fin n -> String
indexToName ((name, _) :: xs) FZ = name
indexToName (x :: xs) (FS k) = indexToName xs k

nameToIndex : (context : Context n) ->
              (name : String) ->
              {auto prf : Elem (name, _) context} ->
              Nat
nameToIndex ((name, b) :: _) name {prf = Here} = 0
nameToIndex (_ :: xs) name {prf = (There later)} = 1 + nameToIndex xs name

getBinding  : (context : Context n) -> Fin n -> Binding
getBinding ((_, b) :: _) FZ = b
getBinding (_ :: xs) (FS k) = getBinding xs k

termMap : (f : (modifier : Nat) -> (cutoff : Nat) -> (t : Term) -> Term) ->
          (modifier : Nat) ->
          (cutoff : Nat) ->
          (t : Term) -> Term
termMap f modifier cutoff term = f modifier cutoff term
termMap f modifier cutoff (TmAbs fileInfo nameHint term)
  = TmAbs fileInfo nameHint (termMap f modifier (cutoff + 1) term)
termMap f modifier cutoff (TmApp fileInfo term1 term2)
  = TmApp fileInfo
          (termMap f modifier cutoff term1)
          (termMap f modifier cutoff term2)

shiftAbove : (modifier : Nat) -> (cutoff : Nat) -> Term -> Term
shiftAbove modifier cutoff t = termMap shiftAboveHelper modifier cutoff t where
  shiftAboveHelper : (modifier : Nat) -> (cutoff : Nat) -> (t : Term) -> Term
  shiftAboveHelper modifier cutoff (TmVar fileInfo index check)
    = if index >= cutoff
        then TmVar fileInfo
                    (index + modifier)
                    (check + modifier)
        else TmVar fileInfo index (check + modifier)
  shiftAboveHelper _ _ t = t

shift : (modifier : Nat) -> Term -> Term
shift modifier t = shiftAbove modifier 1 t

termSubstitution : (sub_index : Nat) -> (s : Term) -> (t: Term) -> Term
termSubstitution sub_index s t = substitutionHelper sub_index 0 t where
  substitutionHelper : (sub_index : Nat) ->
                       (cutoff : Nat) ->
                       (t : Term) ->
                       Term
  substitutionHelper sub_index cutoff (TmVar fileInfo index check)
    = if index == sub_index + cutoff
         then shift cutoff (TmVar fileInfo index check)
         else TmVar fileInfo index check
  substitutionHelper _ _ t= t

substitute : (s : Term) -> (t : Term) -> Term
substitute s t = shift 0 (termSubstitution 0 (shift 1 s) t)

checkContextLength : (t : Term) -> (context : Context n) -> Bool
checkContextLength (TmVar _ _ check) _ {n} = check == n
checkContextLength  _ _ = False

getNameFromIndex : Context n -> Nat -> Either String String
getNameFromIndex context Z {n} = Left ("Error: bad index 0/" ++ (show n) ++
                                      " in " ++ (show context))
getNameFromIndex context (S k) {n}
  = let fin = (natToFin (contextIndex (S k)) n) in
        (case fin of
              Nothing => Left ("Error: " ++ (show (S k)) ++ "/" ++ (show n) ++
                        " in " ++ (show context))
              (Just idx) => Right (show (indexToName context idx)))

termInfo : Term -> Info
termInfo (TmVar fileInfo _ _) = fileInfo
termInfo (TmAbs fileInfo _ _) = fileInfo
termInfo (TmApp fileInfo _ _) = fileInfo

printTerm : Term -> Context n -> String
printTerm (TmVar _ index check) context {n}
  = case (compare check n) of
         GT => ("Error: bad check " ++ (show check) ++ "/" ++ (show n) ++
              " in " ++ (show context))
         _ =>  (case getNameFromIndex context index of
                     (Left err) => err
                     (Right res) => res)
printTerm (TmAbs _ nameHint t) context = "lambda" ++ nameHint ++ ".(\n\t" ++
                                         (printTerm t context) ++ ")"
printTerm (TmApp _ t1 t2) context = (printTerm t1 context) ++ " " ++
                                    (printTerm t2 context)

max_stars_repo_name: Ryxai/Ulambda

max_issues_repo_name: Ryxai/Ulambda

max_forks_repo_name: Ryxai/Ulambda


text:
||| A simplified Wadler style pretty printing library without the pretty part.
module Printer

import Data.String.Extra
import System.File

export
data Doc
  = Nil
  | LineBreak
  | Text String
  | Nest Int Doc
  | Seq Doc Doc

public export
Semigroup Doc where
  Nil <+> y = y
  x <+> Nil = x
  x <+> y = Seq x y

public export
Monoid Doc where
  neutral = Nil

public export
Show Doc where
  show doc = case doc of
    Nil => "Nil"
    LineBreak => "LineBreak"
    Text s => show s
    Seq x y => "(" ++ show x ++ " <+> " ++ show y ++ ")"
    Nest i d => "(Nest " ++ show i ++ " " ++ show d ++ ")"

export
empty : Doc
empty = Nil

export
line : Doc
line = LineBreak

export
emptyLine : Doc
emptyLine = line <+> line

export
text : String -> Doc
text "" = Nil
text "\n" = LineBreak
text s = Text s

public export %inline
shown : Show a => a -> Doc
shown a = text (show a)

export
FromString Doc where
  fromString = text

export
nest : Int -> Doc -> Doc
nest = Nest

export
indented : Doc -> Doc
indented d = nest 2 (line <+> d) <+> line

export
sepBy : Doc -> List Doc -> Doc
sepBy sep [] = empty
sepBy sep (d::ds) = foldl (\acc, e => acc <+> sep <+> e) d ds

export
vcat : List Doc -> Doc
vcat = sepBy line

export
hcat : List Doc -> Doc
hcat = sepBy empty

export
commaSep : List Doc -> Doc
commaSep = sepBy ", "

export
paren : Doc -> Doc
paren d = "(" <+> d <+> ")"

export
tupled : List Doc -> Doc
tupled = paren . commaSep

export
block : Doc -> Doc
block b = " {" <+> indented b <+> "}"

export
semi : Doc
semi = text ";"

export
dot : Doc
dot = text "."

ok : Either FileError ()
ok = Right ()

writeDocTo : HasIO io => File -> Doc -> (indent : String) -> io (Either FileError ())
writeDocTo f doc i = case doc of
  Text s => fPutStr f s
  LineBreak => do
    Right () <- fPutStr f "\n" | e => pure e
    if length i > 0
      then fPutStr f i
      else pure ok
  Seq x y => do
    Right () <- writeDocTo f x i | e => pure e
    writeDocTo f y i
  Nest w d => writeDocTo f d (nSpaces (fromInteger (cast w) + length i))
  Nil => pure ok
  where
    nSpaces : Nat -> String
    nSpaces i = replicate i ' '

||| Writes a [Doc] to a file
export
writeDocToFile : HasIO io => (filepath: String) -> (doc : Doc) -> io (Either FileError ())
writeDocToFile fn doc = do
  Right h  <- openFile fn WriteTruncate
    | Left err => pure (Left err)
  Right () <- writeDocTo h doc ""
    | Left err => do
      closeFile h
      pure (Left err)
  closeFile h
  pure ok


text:
module Solver

import Decidable.Equality
import Control.Monad.State
import Data.Vect
import Data.Vect.Quantifiers
import System

-- %default total

-- Solver ----------------------------------------------------------------------

Cell : Nat -> Type
Cell n = Maybe (Fin n)

data Board : Nat -> Type where
  MkBoard : {n : Nat} -> Vect n (Vect n (Cell n)) -> Board n

emptyBoard : Board n
emptyBoard {n=n} = MkBoard (replicate n (replicate n Nothing))

showElt : Cell n -> String
showElt Nothing = "."
showElt (Just x) = show (1 + (the Int (fromInteger (cast x))))

-- FIXME: Inline type decl should not be necessary here
showRow : Vect n (Cell n) -> String
showRow {n=n} xs = unwords (toList (the (Vect n String) (map showElt xs)))

unlines : Vect n String -> String
unlines Nil = ""
unlines (l::Nil) = l
unlines (l::ls) = pack (foldl addLine (unpack l) (map unpack ls))
  where
    addLine : List Char -> List Char -> List Char
    addLine w s = w ++ ('\n' :: s)

Show (Board n) where
  show (MkBoard rs) = unlines (map showRow rs)

updateAt : Fin n -> Vect n a -> (a -> a) -> Vect n a
updateAt FZ (x::xs) f = f x :: xs
updateAt (FS i) (x::xs) f = x :: updateAt i xs f

setCell : Board n -> (Fin n, Fin n) -> Fin n -> Board n
setCell (MkBoard b) (x, y) value = MkBoard (updateAt y b (\row => updateAt x row (const (Just value))))

getCell : Board n -> (Fin n, Fin n) -> Cell n
getCell (MkBoard b) (x, y) = index x (index y b)

anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
anyElim _ f (Here p) = f p
anyElim f _ (There p) = f p

getRow : Fin n -> Board n -> Vect n (Cell n)
getRow i (MkBoard b) = index i b

getCol : Fin n -> Board n -> Vect n (Cell n)
getCol i (MkBoard b) = helper i b
  where
    helper : Fin n -> Vect m (Vect n a) -> Vect m a
    helper _ Nil = Nil
    helper i (xs::xss) = index i xs :: helper i xss

LegalNeighbors : Cell n -> Cell n -> Type
LegalNeighbors (Just x) (Just y) = Not (x = y)
LegalNeighbors _ _ = ()

legalNeighbors : (x : Cell n) -> (y : Cell n) -> Dec (LegalNeighbors x y)
legalNeighbors (Just x) (Just y) with (decEq x y)
  | Yes prf = No (\pf => pf prf)
  | No prf = Yes prf
legalNeighbors Nothing (Just _) = Yes ()
legalNeighbors (Just _) Nothing = Yes ()
legalNeighbors Nothing Nothing = Yes ()

rowSafe : (b : Board n) -> (r : Fin n) -> (val : Fin n) -> Dec (All (LegalNeighbors (Just val)) (getRow r b))
rowSafe b r v = all (legalNeighbors (Just v)) (getRow r b)

colSafe : (b : Board n) -> (r : Fin n) -> (val : Fin n) -> Dec (All (LegalNeighbors (Just val)) (getCol r b))
colSafe b r v = all (legalNeighbors (Just v)) (getCol r b)

Empty : Cell n -> Type
Empty {n=n} x = (the (Cell n) Nothing) = x

empty : (cell : Cell n) -> Dec (Empty cell)
empty Nothing = Yes Refl
empty (Just _) = No nothingNotJust

-- Predicate for legal cell assignments
LegalVal : Board n -> (Fin n, Fin n) -> Fin n -> Type
LegalVal b (x, y) val = (Empty (getCell b (x, y)), All (LegalNeighbors (Just val)) (getCol x b), All (LegalNeighbors (Just val)) (getRow y b))

legalVal : (b : Board n) -> (coord : (Fin n, Fin n)) -> (val : Fin n) -> Dec (LegalVal b coord val)
legalVal b (x, y) v =
  case rowSafe b y v of
    No prf => No (\(_, _, rf) => prf rf)
    Yes prf =>
      case colSafe b x v of
        No prf' => No (\(_, cf, _) => prf' cf)
        Yes prf' =>
          case Solver.empty (getCell b (x, y)) of
            No prf'' => No (\(ef, _, _) => prf'' ef)
            Yes prf'' => Yes (prf'', prf', prf)

Filled : Cell n -> Type
--Filled {n=n} x = Not (Empty x) -- TODO: Find out why this doesn't work
Filled {n=n} = (\x => Not (Empty x))
--Filled {n=n} x = the (Maybe (Fin n)) Nothing = x -> Void
--Filled {n=n} = \x => the (Maybe (Fin n)) Nothing = x -> Void

filled : (cell : Cell n) -> Dec (Filled cell)
filled Nothing = No (\f => f Refl)
filled (Just _) = Yes nothingNotJust

FullBoard : Board n -> Type
FullBoard (MkBoard b) = All (All Filled) b

fullBoard : (b : Board n) -> Dec (FullBoard b)
fullBoard (MkBoard b) = all (all filled) b

fins : Vect n (Fin n)
fins {n=Z} = Nil
fins {n=(S m)} = last :: map weaken fins

data LegalBoard : Board n -> Type where
  Base : LegalBoard (emptyBoard {n})
  Step : {b : Board n} -> {coords : (Fin n, Fin n)} -> {v : Fin n} -> LegalVal b coords v -> LegalBoard b -> LegalBoard (setCell b coords v)

CompleteBoard : Board n -> Type
CompleteBoard b = (LegalBoard b, FullBoard b)

indexStep : {i : Fin n} -> {xs : Vect n a} -> {x : a} -> index i xs = index (FS i) (x::xs)
indexStep = Refl

find : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a)
       -> Either (All (\x => Not (P x)) xs) (y : a ** (P y, (i : Fin n ** y = index i xs)))
find _ Nil = Left Nil
find d (x::xs) with (d x)
  | Yes prf = Right (x ** (prf, (FZ ** Refl)))
  | No prf =
    case find d xs of
      Right (y ** (prf', (i ** prf''))) =>
        Right (y ** (prf', (FS i ** replace {P=(\x => y = x)} (indexStep {x=x}) prf'')))
      Left prf' => Left (prf::prf')

findEmptyInRow : (xs : Vect n (Cell n)) -> Either (All Filled xs) (i : Fin n ** Empty (index i xs))
findEmptyInRow xs =
  case find {P=Empty} empty xs of
    Right (_ ** (pempty, (i ** pidx))) => Right (i ** trans pempty pidx)
    Left p => Left p

emptyCell : (b : Board n) -> Either (FullBoard b) (c : (Fin n, Fin n) ** Empty (getCell b c))
emptyCell (MkBoard rs) =
  case helper rs of
    Left p => Left p
    Right (ri ** (ci ** pf)) => Right ((ci, ri) ** pf)
  where
    helper : (rs : Vect m (Vect n (Cell n)))
             -> Either (All (All Filled) rs) (r : Fin m ** (c : Fin n ** Empty (index c (index r rs))))
    helper Nil = Left Nil
    helper (r::rs) =
      case findEmptyInRow r of
        Right (ci ** pf) => Right (FZ ** (ci ** pf))
        Left prf =>
          case helper rs of
            Left prf' => Left (prf::prf')
            Right (ri ** (ci ** pf)) => Right (FS ri ** (ci ** pf))

tryValue : {b : Board (S n)} -> LegalBoard b -> (c : (Fin (S n), Fin (S n))) -> Empty (getCell b c) -> (v : Fin (S n))
           -> Either (Not (LegalVal b c v)) (b' : Board (S n) ** LegalBoard b')
tryValue {b=b} l c _ v =
  case legalVal b c v of
    No prf => Left prf
    Yes prf => Right (_ ** Step prf l)

nullBoardFull : (b : Board Z) -> FullBoard b
nullBoardFull (MkBoard Nil) = Nil

-- TODO: Prove complete by induction on illegal values wrt. some base state, e.g. every value is illegal for 123\21_\3_2
fillBoard : (b : Board n) -> LegalBoard b -> Maybe (b' : Board n ** CompleteBoard b')
fillBoard {n=Z} b l = Just (b ** (l, nullBoardFull b))
fillBoard {n=(S n)} b l with (emptyCell b)
  | Left full = Just (b ** (l, full))
  | Right (coords ** p) = recurse last
  where
    %assert_total
    tryAll : (v : Fin (S n)) -> (Fin (S n), Maybe (b' : Board (S n) ** LegalBoard b'))
    tryAll v = --trace ("Trying " ++ show (the Int (cast v))) $
      case tryValue l coords p v of
        Right success => (v, Just success)
        Left _ => -- TODO: Prove unsolvable
          case v of
            FS k => tryAll (weaken k)
            FZ => (v, Nothing)

    %assert_total
    recurse : Fin (S n) -> Maybe (b' : Board (S n) ** CompleteBoard b')
    recurse start =
      case tryAll start of
        (_, Nothing) => Nothing
        (FZ, Just (b' ** l')) => fillBoard b' l'
        (FS next, Just (b' ** l')) =>
          case fillBoard b' l' of
            Just solution => Just solution
            Nothing => recurse (weaken next)

-- Parser ----------------------------------------------------------------------

ParseErr : Type
ParseErr = String

Parser : Nat -> Type
Parser n = Either ParseErr (b : Board n ** LegalBoard b)

mapM : Monad m => (a -> m b) -> Vect n a -> m (Vect n b)
mapM _ Nil = pure Vect.Nil
mapM f (x::xs) = do
  x' <- f x
  xs' <- mapM f xs
  pure (Vect.(::) x' xs')

parseToken : String -> Either String (Cell n)
parseToken "." = pure Nothing
parseToken "0" = Left "Got cell 0, expected 1-based numbering"
parseToken x = map Just (tryParseFin ((cast x) - 1))
  where
    tryParseFin : Int -> Either String (Fin n)
    tryParseFin {n=Z} _ = Left ("Given cell " ++ x ++ " out of range")
    tryParseFin {n=S k} 0 = pure FZ
    tryParseFin {n=S k} x =
      case tryParseFin {n=k} (x-1) of
        Left err => Left err
        Right fin => pure (FS fin)

length : Vect n a -> Nat
length {n=n} _ = n

parseCols : {b : Board n} -> Fin n -> LegalBoard b -> Vect n String -> Parser n
parseCols {n=Z} _ l _ = Right (_ ** l)
parseCols {n=S k} row l cs = helper last l
  where
    step : {b : Board (S k)} -> LegalBoard b -> Fin (S k) -> Parser (S k)
    step {b=b} l x = do
      let here = (x, row) -- TODO: Determine why naming this makes idris smarter
      tok <- parseToken {n=S k} (index x cs)
      case tok of
        Nothing => pure (_ ** l)
        Just t =>
           case legalVal b here t of
             Yes prf => Right (_ ** Step prf l)
             No _ => Left ("Illegal cell " ++ index x cs)

    helper : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)
    helper FZ l = step l FZ
    helper (FS k) l = do
      (_ ** next) <- step l (FS k)
      helper (weaken k) next

parseRows : (b : Board n) -> LegalBoard b -> Vect n String -> Parser n
parseRows {n=Z}   _ l _  = Right (_ ** l)
parseRows {n=S k} _ l rs = helper last l
  where
    step : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)
    step i l =
      let cs = fromList (words (index i rs)) in
      case decEq (Parser.length cs) (S k) of
        No _  => Left "Row length not equal to column height"
        Yes prf => parseCols i l (replace {P=\n => Vect n String} prf cs)

    helper : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)
    helper FZ l = step FZ l
    helper (FS k) l = do
      (_ ** next) <- step (FS k) l
      helper (weaken k) next

parse : String -> Either String (n : Nat ** (b : Board n ** LegalBoard b))
parse str =
  let rows = fromList (lines str) in
  case parseRows {n=length rows} emptyBoard Base rows of
    Left msg => Left msg
    Right board => pure (_ ** board)

-- Main ------------------------------------------------------------------------

main : IO ()
main = do
  args <- getArgs
  case args of
    [_, path] => do
      f <- readFile path
      case f of
        Left _err => putStrLn $ "Error reading file: " ++ path
        Right f' =>
          case parse f' of
            Left err => putStrLn err
            Right (_ ** (board ** legal)) => do
              putStrLn "Got board:"
              printLn board
              putStrLn "Solving..."
              case fillBoard board legal of
                Nothing => putStrLn "No solution found"
                Just (solved ** _) => do
                  putStrLn "Solution found:"
                  printLn solved
    [self] => putStrLn ("Usage: " ++ self ++ " <board file>")

max_stars_repo_name: timjs/iris-clean

max_issues_repo_name: timjs/iris-clean

max_forks_repo_name: timjs/iris-clean


text:
||| A queue implementation based on the description in "Purely Functional Data
||| Structures" by Chris Okasaki
module System.Concurrency.Queue

import Data.List
import System.Concurrency

import public Data.IORef

-----------
-- Stack --
-----------

||| A convenient alias to make it easier to reason about operations
Stack : Type -> Type
Stack = List

emptyStack : Stack a
emptyStack = []

||| Create a new, empty stack.
||| For internal use.
makeSharedStack : IO (IORef (Stack a))
makeSharedStack = newIORef emptyStack

||| Put something on the top of the stack.
||| For internal use.
|||
||| MTSafe: NO
push : (sRef : IORef (Stack a)) -> (thing : a) -> IO ()
push sRef thing = modifyIORef sRef ((::) thing)

||| Get the first item on the stack if there is one, removing it in the process.
||| For internal use.
|||
||| MTSafe: NO
pop : (sRef : IORef (Stack a)) -> IO (Maybe a)
pop sRef = do stack <- readIORef sRef
              case stack of
                   [] => pure Nothing
                   (x :: xs) => do writeIORef sRef xs
                                   pure (Just x)

||| Get the first item on the stack if there is one, without removing it.
||| For internal use.
|||
||| MTSafe: NO
stackPeek : (sRef : IORef (Stack a)) -> IO (Maybe a)
stackPeek sRef = do stack <- readIORef sRef
                    case stack of
                         [] => pure Nothing
                         (x :: xs) => pure (Just x)

-----------
-- Queue --
-----------

||| A FIFO data structure.
export
data Queue : Type -> Type where
  MkQueue : (front : IORef (Stack a))
          -> (rear : IORef (Stack a))
          -> (lock : Mutex)
          -> Queue a

-- Accessors and constructor function --

||| Accessor for `front`.
||| For internal use.
getFront : Queue a -> IORef (Stack a)
getFront (MkQueue front _ _) = front

||| Accessor for `rear`.
||| For internal use.
getRear : Queue a -> IORef (Stack a)
getRear (MkQueue _ rear _) = rear

||| Create a new, empty queue.
export
makeQueue : IO (IORef (Queue a))
makeQueue =
  do front <- makeSharedStack
     rear <- makeSharedStack
     lock <- makeMutex
     newIORef (MkQueue front rear lock)

-- Lock manipulation --

||| Lock the queue by acquiring its mutex.
||| For internal use.
lockQueue : Queue _ -> IO ()
lockQueue (MkQueue _ _ lock) = mutexAcquire lock

||| Unlock the queue by releasing its mutex.
||| For internal use.
unlockQueue : Queue _ -> IO ()
unlockQueue (MkQueue _ _ lock) = mutexRelease lock

-- Queue manipulation --

||| Move the `rear` to the `front`. Used when the queue appears to have run out
||| of items but there may be items in the rear.
||| For internal use.
|||
||| MTSafe: NO
reorder : (frontRef : IORef (Stack a))
        -> (rearRef : IORef (Stack a))
        -> IO ()
reorder frontRef rearRef =
  do rear <- readIORef rearRef
     case rear of
          [] => pure ()   -- Nothing to do
          xs => do writeIORef frontRef (reverse xs)
                   writeIORef rearRef emptyStack

||| Put a thing at the end of the queue.
|||
||| MTSafe: YES
export
enqueue : (sharedQueue : IORef (Queue a))
        -> (thing : a)
        -> IO ()
enqueue sharedQueue thing =
  do queue <- readIORef sharedQueue
     lockQueue queue
     push (getRear queue) thing
     unlockQueue queue

||| Get a thing from the front of the queue if there is one, removing it in the
||| process.
|||
||| MTSafe: YES
export
dequeue : (sharedQueue : IORef (Queue a))
        -> IO (Maybe a)
dequeue sharedQueue =
  do queue <- readIORef sharedQueue
     lockQueue queue
     let frontRef = getFront queue
     let rearRef  = getRear  queue
     maybeFront <- pop frontRef
     case maybeFront of
          (Just thing) => do unlockQueue queue
                             pure (Just thing)

          Nothing => do -- reorder and try again
                        reorder frontRef rearRef
                        maybeFront' <- pop frontRef
                        -- no need to inspect maybeFront' since theres nothing
                        -- to do if we got another Nothing; then the queue is
                        -- empty
                        unlockQueue queue
                        pure maybeFront'

||| Get a thing from the front of the queue if there is one, without removing
||| it.
|||
||| MTSafe: YES
export
peek : (sharedQueue : IORef (Queue a))
        -> IO (Maybe a)
peek sharedQueue =
  do queue <- readIORef sharedQueue
     lockQueue queue
     let frontRef = getFront queue
     let rearRef  = getRear  queue
     maybeFront <- stackPeek frontRef
     case maybeFront of
          (Just thing) => do unlockQueue queue
                             pure (Just thing)

          Nothing => do -- reorder and try again
                        reorder frontRef rearRef
                        maybeFront' <- stackPeek frontRef
                        -- no need to inspect maybeFront' since theres nothing
                        -- to do if we got another Nothing; then the queue is
                        -- empty
                        unlockQueue queue
                        pure maybeFront'


text:
module Hedgehog.Internal.Options

import Data.String
import Decidable.Equality
import Hedgehog.Internal.Property
import System.Console.GetOpt

public export
data NumTest = Relaxed TestLimit | Forced TestLimit

public export
record Config where
  constructor MkConfig
  printHelp  : Bool
  numTests   : Maybe NumTest
  numShrinks : Maybe ShrinkLimit
  confidence : Maybe Confidence

export
init : Config
init = MkConfig False Nothing Nothing Nothing

parseNat : String -> Either (List String) Nat
parseNat s =
  maybe (Left [#"Not a natural number: \#{s}"#]) Right $ parsePositive s

toConfidence : Nat -> Either (List String) Confidence
toConfidence n =
  let c = cast {to = Bits64} n
   in case decEq (c >= 2) True of
        (Yes prf)   => Right $ MkConfidence c prf
        (No contra) => Left [ #"Not a valid confidence value: \#{show n}"# ]

setTests : String -> Config -> Either (List String) Config
setTests s c =
  map (\n => { numTests := Just $ Relaxed $ MkTagged n} c)
      (parseNat s)

setShrinks : String -> Config -> Either (List String) Config
setShrinks s c =
  map (\n => { numShrinks := Just $ MkTagged n} c)
      (parseNat s)

setConfidence : String -> Config -> Either (List String) Config
setConfidence s c =
  map (\n => { confidence := Just n} c)
      (parseNat s >>= toConfidence)

setTestsForced : String -> Config -> Either (List String) Config
setTestsForced s c =
  map (\n => { numTests := Just $ Forced $ MkTagged n} c)
      (parseNat s)

setHelp : Config -> Either (List String) Config
setHelp = Right . { printHelp := True }

descs : List $ OptDescr (Config -> Either (List String) Config)
descs = [ MkOpt ['n'] ["testlimit"] (ReqArg setTests "<tests>")
            "number of tests to be passed by each property"
        , MkOpt ['N'] ["testlimit!"] (ReqArg setTestsForced "<tests>")
            "like -n but includes tests that are only run once"
        , MkOpt ['s'] ["shrinklimit"] (ReqArg setShrinks "<shrinks>")
            "maximal number of shrinks in case of a failed test"
        , MkOpt ['c'] ["confidence"] (ReqArg setConfidence "<confidence>")
            "acceptable occurence of false positives"
        , MkOpt [] ["--help"] (NoArg setHelp)
            "print this help text"
        ]

export
info : String
info = usageInfo "Hedgehog command line args:\n" descs

export
applyArgs : List String -> Either (List String) Config
applyArgs args =
  case getOpt Permute descs args of
       MkResult opts _ _ [] => foldl (>>=) (Right init) opts
       MkResult _    _ _ e  => Left e

export
applyConfig : Config -> Group -> Group
applyConfig (MkConfig _ nt ns c) =
  maybe id adjTests nt . maybe id withShrinks ns . maybe id withConfidence c

  where
    adjPropTests : NumTest -> Property -> Property
    adjPropTests (Forced x)  = withTests x
    adjPropTests (Relaxed x) = mapTests $ \n => if n > 1 then x else n

    adjTests : NumTest -> Group -> Group
    adjTests = mapProperty . adjPropTests


text:
module basic024

namespace Main
  main : IO ()
  main = do
    printLn $ div (the Integer 5) 2
    printLn $ div (the Int 5) 2
    printLn $ div (the Bits8 5) 2
    printLn $ div (the Bits16 5) 2
    printLn $ div (the Bits32 5) 2
    printLn $ div (the Bits64 5) 2
    printLn $ div (the Nat 5) 2

    printLn $ mod (the Integer 5) 2
    printLn $ mod (the Int 5) 2
    printLn $ mod (the Bits8 5) 2
    printLn $ mod (the Bits16 5) 2
    printLn $ mod (the Bits32 5) 2
    printLn $ mod (the Bits64 5) 2
    printLn $ mod (the Nat 5) 2

    printLn $ div (the Integer 3) 5
    printLn $ div (the Int 3) 5
    printLn $ div (the Bits8 3) 5
    printLn $ div (the Bits16 3) 5
    printLn $ div (the Bits32 3) 5
    printLn $ div (the Bits64 3) 5
    printLn $ div (the Nat 3) 5

    printLn $ mod (the Integer 3) 5
    printLn $ mod (the Int 3) 5
    printLn $ mod (the Bits8 3) 5
    printLn $ mod (the Bits16 3) 5
    printLn $ mod (the Bits32 3) 5
    printLn $ mod (the Bits64 3) 5
    printLn $ mod (the Nat 3) 5

    printLn $ div (the Integer (-5)) 2
    printLn $ div (the Int (-5)) 2

    printLn $ mod (the Integer (-5)) 2
    printLn $ mod (the Int (-5)) 2

    printLn $ div (the Integer (-3)) 5
    printLn $ div (the Int (-3)) 5

    printLn $ mod (the Integer (-3)) 5
    printLn $ mod (the Int (-3)) 5

    printLn $ div (-432642342742368327462378462387) 36473264372
    printLn $ mod (-432642342742368327462378462387) 36473264372

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Web.Raw.Geometry

import JS
import Web.Internal.GeometryPrim
import Web.Internal.Types

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

namespace DOMMatrix

  export
  fromFloat32Array : (array32 : Float32Array) -> JSIO DOMMatrix
  fromFloat32Array a = primJS $ DOMMatrix.prim__fromFloat32Array a

  export
  fromFloat64Array : (array64 : Float64Array) -> JSIO DOMMatrix
  fromFloat64Array a = primJS $ DOMMatrix.prim__fromFloat64Array a

  export
  fromMatrix :  (0 _ : JSType t1)
             => {auto 0 _ : Elem DOMMatrixInit (Types t1)}
             -> (other : Optional t1)
             -> JSIO DOMMatrix
  fromMatrix a = primJS $ DOMMatrix.prim__fromMatrix (optUp a)

  export
  fromMatrix' : JSIO DOMMatrix
  fromMatrix' = primJS $ DOMMatrix.prim__fromMatrix undef

  export
  invertSelf : (obj : DOMMatrix) -> JSIO DOMMatrix
  invertSelf a = primJS $ DOMMatrix.prim__invertSelf a

  export
  multiplySelf :  (0 _ : JSType t1)
               => {auto 0 _ : Elem DOMMatrixInit (Types t1)}
               -> (obj : DOMMatrix)
               -> (other : Optional t1)
               -> JSIO DOMMatrix
  multiplySelf a b = primJS $ DOMMatrix.prim__multiplySelf a (optUp b)

  export
  multiplySelf' : (obj : DOMMatrix) -> JSIO DOMMatrix
  multiplySelf' a = primJS $ DOMMatrix.prim__multiplySelf a undef

  export
  preMultiplySelf :  (0 _ : JSType t1)
                  => {auto 0 _ : Elem DOMMatrixInit (Types t1)}
                  -> (obj : DOMMatrix)
                  -> (other : Optional t1)
                  -> JSIO DOMMatrix
  preMultiplySelf a b = primJS $ DOMMatrix.prim__preMultiplySelf a (optUp b)

  export
  preMultiplySelf' : (obj : DOMMatrix) -> JSIO DOMMatrix
  preMultiplySelf' a = primJS $ DOMMatrix.prim__preMultiplySelf a undef

  export
  rotateAxisAngleSelf :  (obj : DOMMatrix)
                      -> (x : Optional Double)
                      -> (y : Optional Double)
                      -> (z : Optional Double)
                      -> (angle : Optional Double)
                      -> JSIO DOMMatrix
  rotateAxisAngleSelf a b c d e = primJS
                                $ DOMMatrix.prim__rotateAxisAngleSelf a
                                                                      (toFFI b)
                                                                      (toFFI c)
                                                                      (toFFI d)
                                                                      (toFFI e)

  export
  rotateAxisAngleSelf' : (obj : DOMMatrix) -> JSIO DOMMatrix
  rotateAxisAngleSelf' a = primJS
                         $ DOMMatrix.prim__rotateAxisAngleSelf a
                                                               undef
                                                               undef
                                                               undef
                                                               undef

  export
  rotateFromVectorSelf :  (obj : DOMMatrix)
                       -> (x : Optional Double)
                       -> (y : Optional Double)
                       -> JSIO DOMMatrix
  rotateFromVectorSelf a b c = primJS
                             $ DOMMatrix.prim__rotateFromVectorSelf a
                                                                    (toFFI b)
                                                                    (toFFI c)

  export
  rotateFromVectorSelf' : (obj : DOMMatrix) -> JSIO DOMMatrix
  rotateFromVectorSelf' a = primJS
                          $ DOMMatrix.prim__rotateFromVectorSelf a undef undef

  export
  rotateSelf :  (obj : DOMMatrix)
             -> (rotX : Optional Double)
             -> (rotY : Optional Double)
             -> (rotZ : Optional Double)
             -> JSIO DOMMatrix
  rotateSelf a b c d = primJS
                     $ DOMMatrix.prim__rotateSelf a
                                                  (toFFI b)
                                                  (toFFI c)
                                                  (toFFI d)

  export
  rotateSelf' : (obj : DOMMatrix) -> JSIO DOMMatrix
  rotateSelf' a = primJS $ DOMMatrix.prim__rotateSelf a undef undef undef

  export
  scale3dSelf :  (obj : DOMMatrix)
              -> (scale : Optional Double)
              -> (originX : Optional Double)
              -> (originY : Optional Double)
              -> (originZ : Optional Double)
              -> JSIO DOMMatrix
  scale3dSelf a b c d e = primJS
                        $ DOMMatrix.prim__scale3dSelf a
                                                      (toFFI b)
                                                      (toFFI c)
                                                      (toFFI d)
                                                      (toFFI e)

  export
  scale3dSelf' : (obj : DOMMatrix) -> JSIO DOMMatrix
  scale3dSelf' a = primJS
                 $ DOMMatrix.prim__scale3dSelf a undef undef undef undef

  export
  scaleSelf :  (obj : DOMMatrix)
            -> (scaleX : Optional Double)
            -> (scaleY : Optional Double)
            -> (scaleZ : Optional Double)
            -> (originX : Optional Double)
            -> (originY : Optional Double)
            -> (originZ : Optional Double)
            -> JSIO DOMMatrix
  scaleSelf a b c d e f g = primJS
                          $ DOMMatrix.prim__scaleSelf a
                                                      (toFFI b)
                                                      (toFFI c)
                                                      (toFFI d)
                                                      (toFFI e)
                                                      (toFFI f)
                                                      (toFFI g)

  export
  scaleSelf' : (obj : DOMMatrix) -> JSIO DOMMatrix
  scaleSelf' a = primJS
               $ DOMMatrix.prim__scaleSelf a undef undef undef undef undef undef

  export
  setMatrixValue :  (obj : DOMMatrix)
                 -> (transformList : String)
                 -> JSIO DOMMatrix
  setMatrixValue a b = primJS $ DOMMatrix.prim__setMatrixValue a b

  export
  skewXSelf : (obj : DOMMatrix) -> (sx : Optional Double) -> JSIO DOMMatrix
  skewXSelf a b = primJS $ DOMMatrix.prim__skewXSelf a (toFFI b)

  export
  skewXSelf' : (obj : DOMMatrix) -> JSIO DOMMatrix
  skewXSelf' a = primJS $ DOMMatrix.prim__skewXSelf a undef

  export
  skewYSelf : (obj : DOMMatrix) -> (sy : Optional Double) -> JSIO DOMMatrix
  skewYSelf a b = primJS $ DOMMatrix.prim__skewYSelf a (toFFI b)

  export
  skewYSelf' : (obj : DOMMatrix) -> JSIO DOMMatrix
  skewYSelf' a = primJS $ DOMMatrix.prim__skewYSelf a undef

  export
  translateSelf :  (obj : DOMMatrix)
                -> (tx : Optional Double)
                -> (ty : Optional Double)
                -> (tz : Optional Double)
                -> JSIO DOMMatrix
  translateSelf a b c d = primJS
                        $ DOMMatrix.prim__translateSelf a
                                                        (toFFI b)
                                                        (toFFI c)
                                                        (toFFI d)

  export
  translateSelf' : (obj : DOMMatrix) -> JSIO DOMMatrix
  translateSelf' a = primJS $ DOMMatrix.prim__translateSelf a undef undef undef

namespace DOMMatrixReadOnly

  export
  fromFloat32Array : (array32 : Float32Array) -> JSIO DOMMatrixReadOnly
  fromFloat32Array a = primJS $ DOMMatrixReadOnly.prim__fromFloat32Array a

  export
  fromFloat64Array : (array64 : Float64Array) -> JSIO DOMMatrixReadOnly
  fromFloat64Array a = primJS $ DOMMatrixReadOnly.prim__fromFloat64Array a

  export
  fromMatrix :  (0 _ : JSType t1)
             => {auto 0 _ : Elem DOMMatrixInit (Types t1)}
             -> (other : Optional t1)
             -> JSIO DOMMatrixReadOnly
  fromMatrix a = primJS $ DOMMatrixReadOnly.prim__fromMatrix (optUp a)

  export
  fromMatrix' : JSIO DOMMatrixReadOnly
  fromMatrix' = primJS $ DOMMatrixReadOnly.prim__fromMatrix undef

  export
  a :  (0 _ : JSType t1)
    => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
    -> (obj : t1)
    -> JSIO Double
  a b = primJS $ DOMMatrixReadOnly.prim__a (up b)

  export
  b :  (0 _ : JSType t1)
    => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
    -> (obj : t1)
    -> JSIO Double
  b a = primJS $ DOMMatrixReadOnly.prim__b (up a)

  export
  c :  (0 _ : JSType t1)
    => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
    -> (obj : t1)
    -> JSIO Double
  c a = primJS $ DOMMatrixReadOnly.prim__c (up a)

  export
  d :  (0 _ : JSType t1)
    => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
    -> (obj : t1)
    -> JSIO Double
  d a = primJS $ DOMMatrixReadOnly.prim__d (up a)

  export
  e :  (0 _ : JSType t1)
    => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
    -> (obj : t1)
    -> JSIO Double
  e a = primJS $ DOMMatrixReadOnly.prim__e (up a)

  export
  f :  (0 _ : JSType t1)
    => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
    -> (obj : t1)
    -> JSIO Double
  f a = primJS $ DOMMatrixReadOnly.prim__f (up a)

  export
  is2D :  (0 _ : JSType t1)
       => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
       -> (obj : t1)
       -> JSIO Bool
  is2D a = tryJS "DOMMatrixReadOnly.is2D" $ DOMMatrixReadOnly.prim__is2D (up a)

  export
  isIdentity :  (0 _ : JSType t1)
             => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
             -> (obj : t1)
             -> JSIO Bool
  isIdentity a = tryJS "DOMMatrixReadOnly.isIdentity"
               $ DOMMatrixReadOnly.prim__isIdentity (up a)

  export
  m11 :  (0 _ : JSType t1)
      => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
      -> (obj : t1)
      -> JSIO Double
  m11 a = primJS $ DOMMatrixReadOnly.prim__m11 (up a)

  export
  m12 :  (0 _ : JSType t1)
      => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
      -> (obj : t1)
      -> JSIO Double
  m12 a = primJS $ DOMMatrixReadOnly.prim__m12 (up a)

  export
  m13 :  (0 _ : JSType t1)
      => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
      -> (obj : t1)
      -> JSIO Double
  m13 a = primJS $ DOMMatrixReadOnly.prim__m13 (up a)

  export
  m14 :  (0 _ : JSType t1)
      => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
      -> (obj : t1)
      -> JSIO Double
  m14 a = primJS $ DOMMatrixReadOnly.prim__m14 (up a)

  export
  m21 :  (0 _ : JSType t1)
      => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
      -> (obj : t1)
      -> JSIO Double
  m21 a = primJS $ DOMMatrixReadOnly.prim__m21 (up a)

  export
  m22 :  (0 _ : JSType t1)
      => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
      -> (obj : t1)
      -> JSIO Double
  m22 a = primJS $ DOMMatrixReadOnly.prim__m22 (up a)

  export
  m23 :  (0 _ : JSType t1)
      => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
      -> (obj : t1)
      -> JSIO Double
  m23 a = primJS $ DOMMatrixReadOnly.prim__m23 (up a)

  export
  m24 :  (0 _ : JSType t1)
      => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
      -> (obj : t1)
      -> JSIO Double
  m24 a = primJS $ DOMMatrixReadOnly.prim__m24 (up a)

  export
  m31 :  (0 _ : JSType t1)
      => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
      -> (obj : t1)
      -> JSIO Double
  m31 a = primJS $ DOMMatrixReadOnly.prim__m31 (up a)

  export
  m32 :  (0 _ : JSType t1)
      => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
      -> (obj : t1)
      -> JSIO Double
  m32 a = primJS $ DOMMatrixReadOnly.prim__m32 (up a)

  export
  m33 :  (0 _ : JSType t1)
      => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
      -> (obj : t1)
      -> JSIO Double
  m33 a = primJS $ DOMMatrixReadOnly.prim__m33 (up a)

  export
  m34 :  (0 _ : JSType t1)
      => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
      -> (obj : t1)
      -> JSIO Double
  m34 a = primJS $ DOMMatrixReadOnly.prim__m34 (up a)

  export
  m41 :  (0 _ : JSType t1)
      => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
      -> (obj : t1)
      -> JSIO Double
  m41 a = primJS $ DOMMatrixReadOnly.prim__m41 (up a)

  export
  m42 :  (0 _ : JSType t1)
      => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
      -> (obj : t1)
      -> JSIO Double
  m42 a = primJS $ DOMMatrixReadOnly.prim__m42 (up a)

  export
  m43 :  (0 _ : JSType t1)
      => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
      -> (obj : t1)
      -> JSIO Double
  m43 a = primJS $ DOMMatrixReadOnly.prim__m43 (up a)

  export
  m44 :  (0 _ : JSType t1)
      => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
      -> (obj : t1)
      -> JSIO Double
  m44 a = primJS $ DOMMatrixReadOnly.prim__m44 (up a)

  export
  flipX :  (0 _ : JSType t1)
        => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
        -> (obj : t1)
        -> JSIO DOMMatrix
  flipX a = primJS $ DOMMatrixReadOnly.prim__flipX (up a)

  export
  flipY :  (0 _ : JSType t1)
        => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
        -> (obj : t1)
        -> JSIO DOMMatrix
  flipY a = primJS $ DOMMatrixReadOnly.prim__flipY (up a)

  export
  inverse :  (0 _ : JSType t1)
          => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
          -> (obj : t1)
          -> JSIO DOMMatrix
  inverse a = primJS $ DOMMatrixReadOnly.prim__inverse (up a)

  export
  multiply :  (0 _ : JSType t1)
           => (0 _ : JSType t2)
           => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
           -> {auto 0 _ : Elem DOMMatrixInit (Types t2)}
           -> (obj : t1)
           -> (other : Optional t2)
           -> JSIO DOMMatrix
  multiply a b = primJS $ DOMMatrixReadOnly.prim__multiply (up a) (optUp b)

  export
  multiply' :  (0 _ : JSType t1)
            => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
            -> (obj : t1)
            -> JSIO DOMMatrix
  multiply' a = primJS $ DOMMatrixReadOnly.prim__multiply (up a) undef

  export
  rotateAxisAngle :  (0 _ : JSType t1)
                  => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
                  -> (obj : t1)
                  -> (x : Optional Double)
                  -> (y : Optional Double)
                  -> (z : Optional Double)
                  -> (angle : Optional Double)
                  -> JSIO DOMMatrix
  rotateAxisAngle a b c d e = primJS
                            $ DOMMatrixReadOnly.prim__rotateAxisAngle (up a)
                                                                      (toFFI b)
                                                                      (toFFI c)
                                                                      (toFFI d)
                                                                      (toFFI e)

  export
  rotateAxisAngle' :  (0 _ : JSType t1)
                   => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
                   -> (obj : t1)
                   -> JSIO DOMMatrix
  rotateAxisAngle' a = primJS
                     $ DOMMatrixReadOnly.prim__rotateAxisAngle (up a)
                                                               undef
                                                               undef
                                                               undef
                                                               undef

  export
  rotate :  (0 _ : JSType t1)
         => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
         -> (obj : t1)
         -> (rotX : Optional Double)
         -> (rotY : Optional Double)
         -> (rotZ : Optional Double)
         -> JSIO DOMMatrix
  rotate a b c d = primJS
                 $ DOMMatrixReadOnly.prim__rotate (up a)
                                                  (toFFI b)
                                                  (toFFI c)
                                                  (toFFI d)

  export
  rotate' :  (0 _ : JSType t1)
          => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
          -> (obj : t1)
          -> JSIO DOMMatrix
  rotate' a = primJS $ DOMMatrixReadOnly.prim__rotate (up a) undef undef undef

  export
  rotateFromVector :  (0 _ : JSType t1)
                   => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
                   -> (obj : t1)
                   -> (x : Optional Double)
                   -> (y : Optional Double)
                   -> JSIO DOMMatrix
  rotateFromVector a b c = primJS
                         $ DOMMatrixReadOnly.prim__rotateFromVector (up a)
                                                                    (toFFI b)
                                                                    (toFFI c)

  export
  rotateFromVector' :  (0 _ : JSType t1)
                    => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
                    -> (obj : t1)
                    -> JSIO DOMMatrix
  rotateFromVector' a = primJS
                      $ DOMMatrixReadOnly.prim__rotateFromVector (up a)
                                                                 undef
                                                                 undef

  export
  scale3d :  (0 _ : JSType t1)
          => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
          -> (obj : t1)
          -> (scale : Optional Double)
          -> (originX : Optional Double)
          -> (originY : Optional Double)
          -> (originZ : Optional Double)
          -> JSIO DOMMatrix
  scale3d a b c d e = primJS
                    $ DOMMatrixReadOnly.prim__scale3d (up a)
                                                      (toFFI b)
                                                      (toFFI c)
                                                      (toFFI d)
                                                      (toFFI e)

  export
  scale3d' :  (0 _ : JSType t1)
           => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
           -> (obj : t1)
           -> JSIO DOMMatrix
  scale3d' a = primJS
             $ DOMMatrixReadOnly.prim__scale3d (up a) undef undef undef undef

  export
  scale :  (0 _ : JSType t1)
        => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
        -> (obj : t1)
        -> (scaleX : Optional Double)
        -> (scaleY : Optional Double)
        -> (scaleZ : Optional Double)
        -> (originX : Optional Double)
        -> (originY : Optional Double)
        -> (originZ : Optional Double)
        -> JSIO DOMMatrix
  scale a b c d e f g = primJS
                      $ DOMMatrixReadOnly.prim__scale (up a)
                                                      (toFFI b)
                                                      (toFFI c)
                                                      (toFFI d)
                                                      (toFFI e)
                                                      (toFFI f)
                                                      (toFFI g)

  export
  scale' :  (0 _ : JSType t1)
         => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
         -> (obj : t1)
         -> JSIO DOMMatrix
  scale' a = primJS
           $ DOMMatrixReadOnly.prim__scale (up a)
                                           undef
                                           undef
                                           undef
                                           undef
                                           undef
                                           undef

  export
  scaleNonUniform :  (0 _ : JSType t1)
                  => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
                  -> (obj : t1)
                  -> (scaleX : Optional Double)
                  -> (scaleY : Optional Double)
                  -> JSIO DOMMatrix
  scaleNonUniform a b c = primJS
                        $ DOMMatrixReadOnly.prim__scaleNonUniform (up a)
                                                                  (toFFI b)
                                                                  (toFFI c)

  export
  scaleNonUniform' :  (0 _ : JSType t1)
                   => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
                   -> (obj : t1)
                   -> JSIO DOMMatrix
  scaleNonUniform' a = primJS
                     $ DOMMatrixReadOnly.prim__scaleNonUniform (up a)
                                                               undef
                                                               undef

  export
  skewX :  (0 _ : JSType t1)
        => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
        -> (obj : t1)
        -> (sx : Optional Double)
        -> JSIO DOMMatrix
  skewX a b = primJS $ DOMMatrixReadOnly.prim__skewX (up a) (toFFI b)

  export
  skewX' :  (0 _ : JSType t1)
         => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
         -> (obj : t1)
         -> JSIO DOMMatrix
  skewX' a = primJS $ DOMMatrixReadOnly.prim__skewX (up a) undef

  export
  skewY :  (0 _ : JSType t1)
        => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
        -> (obj : t1)
        -> (sy : Optional Double)
        -> JSIO DOMMatrix
  skewY a b = primJS $ DOMMatrixReadOnly.prim__skewY (up a) (toFFI b)

  export
  skewY' :  (0 _ : JSType t1)
         => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
         -> (obj : t1)
         -> JSIO DOMMatrix
  skewY' a = primJS $ DOMMatrixReadOnly.prim__skewY (up a) undef

  export
  toFloat32Array :  (0 _ : JSType t1)
                 => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
                 -> (obj : t1)
                 -> JSIO Float32Array
  toFloat32Array a = primJS $ DOMMatrixReadOnly.prim__toFloat32Array (up a)

  export
  toFloat64Array :  (0 _ : JSType t1)
                 => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
                 -> (obj : t1)
                 -> JSIO Float64Array
  toFloat64Array a = primJS $ DOMMatrixReadOnly.prim__toFloat64Array (up a)

  export
  toJSON :  (0 _ : JSType t1)
         => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
         -> (obj : t1)
         -> JSIO Object
  toJSON a = primJS $ DOMMatrixReadOnly.prim__toJSON (up a)

  export
  toString :  (0 _ : JSType t1)
           => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
           -> (obj : t1)
           -> JSIO String
  toString a = primJS $ DOMMatrixReadOnly.prim__toString (up a)

  export
  transformPoint :  (0 _ : JSType t1)
                 => (0 _ : JSType t2)
                 => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
                 -> {auto 0 _ : Elem DOMPointInit (Types t2)}
                 -> (obj : t1)
                 -> (point : Optional t2)
                 -> JSIO DOMPoint
  transformPoint a b = primJS
                     $ DOMMatrixReadOnly.prim__transformPoint (up a) (optUp b)

  export
  transformPoint' :  (0 _ : JSType t1)
                  => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
                  -> (obj : t1)
                  -> JSIO DOMPoint
  transformPoint' a = primJS
                    $ DOMMatrixReadOnly.prim__transformPoint (up a) undef

  export
  translate :  (0 _ : JSType t1)
            => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
            -> (obj : t1)
            -> (tx : Optional Double)
            -> (ty : Optional Double)
            -> (tz : Optional Double)
            -> JSIO DOMMatrix
  translate a b c d = primJS
                    $ DOMMatrixReadOnly.prim__translate (up a)
                                                        (toFFI b)
                                                        (toFFI c)
                                                        (toFFI d)

  export
  translate' :  (0 _ : JSType t1)
             => {auto 0 _ : Elem DOMMatrixReadOnly (Types t1)}
             -> (obj : t1)
             -> JSIO DOMMatrix
  translate' a = primJS
               $ DOMMatrixReadOnly.prim__translate (up a) undef undef undef

namespace DOMPoint

  export
  fromPoint :  (0 _ : JSType t1)
            => {auto 0 _ : Elem DOMPointInit (Types t1)}
            -> (other : Optional t1)
            -> JSIO DOMPoint
  fromPoint a = primJS $ DOMPoint.prim__fromPoint (optUp a)

  export
  fromPoint' : JSIO DOMPoint
  fromPoint' = primJS $ DOMPoint.prim__fromPoint undef

namespace DOMPointReadOnly

  export
  fromPoint :  (0 _ : JSType t1)
            => {auto 0 _ : Elem DOMPointInit (Types t1)}
            -> (other : Optional t1)
            -> JSIO DOMPointReadOnly
  fromPoint a = primJS $ DOMPointReadOnly.prim__fromPoint (optUp a)

  export
  fromPoint' : JSIO DOMPointReadOnly
  fromPoint' = primJS $ DOMPointReadOnly.prim__fromPoint undef

  export
  w :  (0 _ : JSType t1)
    => {auto 0 _ : Elem DOMPointReadOnly (Types t1)}
    -> (obj : t1)
    -> JSIO Double
  w a = primJS $ DOMPointReadOnly.prim__w (up a)

  export
  x :  (0 _ : JSType t1)
    => {auto 0 _ : Elem DOMPointReadOnly (Types t1)}
    -> (obj : t1)
    -> JSIO Double
  x a = primJS $ DOMPointReadOnly.prim__x (up a)

  export
  y :  (0 _ : JSType t1)
    => {auto 0 _ : Elem DOMPointReadOnly (Types t1)}
    -> (obj : t1)
    -> JSIO Double
  y a = primJS $ DOMPointReadOnly.prim__y (up a)

  export
  z :  (0 _ : JSType t1)
    => {auto 0 _ : Elem DOMPointReadOnly (Types t1)}
    -> (obj : t1)
    -> JSIO Double
  z a = primJS $ DOMPointReadOnly.prim__z (up a)

  export
  matrixTransform :  (0 _ : JSType t1)
                  => (0 _ : JSType t2)
                  => {auto 0 _ : Elem DOMPointReadOnly (Types t1)}
                  -> {auto 0 _ : Elem DOMMatrixInit (Types t2)}
                  -> (obj : t1)
                  -> (matrix : Optional t2)
                  -> JSIO DOMPoint
  matrixTransform a b = primJS
                      $ DOMPointReadOnly.prim__matrixTransform (up a) (optUp b)

  export
  matrixTransform' :  (0 _ : JSType t1)
                   => {auto 0 _ : Elem DOMPointReadOnly (Types t1)}
                   -> (obj : t1)
                   -> JSIO DOMPoint
  matrixTransform' a = primJS
                     $ DOMPointReadOnly.prim__matrixTransform (up a) undef

  export
  toJSON :  (0 _ : JSType t1)
         => {auto 0 _ : Elem DOMPointReadOnly (Types t1)}
         -> (obj : t1)
         -> JSIO Object
  toJSON a = primJS $ DOMPointReadOnly.prim__toJSON (up a)

namespace DOMQuad

  export
  fromQuad :  (0 _ : JSType t1)
           => {auto 0 _ : Elem DOMQuadInit (Types t1)}
           -> (other : Optional t1)
           -> JSIO DOMQuad
  fromQuad a = primJS $ DOMQuad.prim__fromQuad (optUp a)

  export
  fromQuad' : JSIO DOMQuad
  fromQuad' = primJS $ DOMQuad.prim__fromQuad undef

  export
  fromRect :  (0 _ : JSType t1)
           => {auto 0 _ : Elem DOMRectInit (Types t1)}
           -> (other : Optional t1)
           -> JSIO DOMQuad
  fromRect a = primJS $ DOMQuad.prim__fromRect (optUp a)

  export
  fromRect' : JSIO DOMQuad
  fromRect' = primJS $ DOMQuad.prim__fromRect undef

  export
  p1 : (obj : DOMQuad) -> JSIO DOMPoint
  p1 a = primJS $ DOMQuad.prim__p1 a

  export
  p2 : (obj : DOMQuad) -> JSIO DOMPoint
  p2 a = primJS $ DOMQuad.prim__p2 a

  export
  p3 : (obj : DOMQuad) -> JSIO DOMPoint
  p3 a = primJS $ DOMQuad.prim__p3 a

  export
  p4 : (obj : DOMQuad) -> JSIO DOMPoint
  p4 a = primJS $ DOMQuad.prim__p4 a

  export
  getBounds : (obj : DOMQuad) -> JSIO DOMRect
  getBounds a = primJS $ DOMQuad.prim__getBounds a

  export
  toJSON : (obj : DOMQuad) -> JSIO Object
  toJSON a = primJS $ DOMQuad.prim__toJSON a

namespace DOMRect

  export
  fromRect :  (0 _ : JSType t1)
           => {auto 0 _ : Elem DOMRectInit (Types t1)}
           -> (other : Optional t1)
           -> JSIO DOMRect
  fromRect a = primJS $ DOMRect.prim__fromRect (optUp a)

  export
  fromRect' : JSIO DOMRect
  fromRect' = primJS $ DOMRect.prim__fromRect undef

namespace DOMRectList

  export
  length : (obj : DOMRectList) -> JSIO Bits32
  length a = primJS $ DOMRectList.prim__length a

  export
  item : (obj : DOMRectList) -> (index : Bits32) -> JSIO (Maybe DOMRect)
  item a b = tryJS "DOMRectList.item" $ DOMRectList.prim__item a b

namespace DOMRectReadOnly

  export
  fromRect :  (0 _ : JSType t1)
           => {auto 0 _ : Elem DOMRectInit (Types t1)}
           -> (other : Optional t1)
           -> JSIO DOMRectReadOnly
  fromRect a = primJS $ DOMRectReadOnly.prim__fromRect (optUp a)

  export
  fromRect' : JSIO DOMRectReadOnly
  fromRect' = primJS $ DOMRectReadOnly.prim__fromRect undef

  export
  bottom :  (0 _ : JSType t1)
         => {auto 0 _ : Elem DOMRectReadOnly (Types t1)}
         -> (obj : t1)
         -> JSIO Double
  bottom a = primJS $ DOMRectReadOnly.prim__bottom (up a)

  export
  height :  (0 _ : JSType t1)
         => {auto 0 _ : Elem DOMRectReadOnly (Types t1)}
         -> (obj : t1)
         -> JSIO Double
  height a = primJS $ DOMRectReadOnly.prim__height (up a)

  export
  left :  (0 _ : JSType t1)
       => {auto 0 _ : Elem DOMRectReadOnly (Types t1)}
       -> (obj : t1)
       -> JSIO Double
  left a = primJS $ DOMRectReadOnly.prim__left (up a)

  export
  right :  (0 _ : JSType t1)
        => {auto 0 _ : Elem DOMRectReadOnly (Types t1)}
        -> (obj : t1)
        -> JSIO Double
  right a = primJS $ DOMRectReadOnly.prim__right (up a)

  export
  top :  (0 _ : JSType t1)
      => {auto 0 _ : Elem DOMRectReadOnly (Types t1)}
      -> (obj : t1)
      -> JSIO Double
  top a = primJS $ DOMRectReadOnly.prim__top (up a)

  export
  width :  (0 _ : JSType t1)
        => {auto 0 _ : Elem DOMRectReadOnly (Types t1)}
        -> (obj : t1)
        -> JSIO Double
  width a = primJS $ DOMRectReadOnly.prim__width (up a)

  export
  x :  (0 _ : JSType t1)
    => {auto 0 _ : Elem DOMRectReadOnly (Types t1)}
    -> (obj : t1)
    -> JSIO Double
  x a = primJS $ DOMRectReadOnly.prim__x (up a)

  export
  y :  (0 _ : JSType t1)
    => {auto 0 _ : Elem DOMRectReadOnly (Types t1)}
    -> (obj : t1)
    -> JSIO Double
  y a = primJS $ DOMRectReadOnly.prim__y (up a)

  export
  toJSON :  (0 _ : JSType t1)
         => {auto 0 _ : Elem DOMRectReadOnly (Types t1)}
         -> (obj : t1)
         -> JSIO Object
  toJSON a = primJS $ DOMRectReadOnly.prim__toJSON (up a)

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

namespace DOMMatrix2DInit

  export
  new :  (a : Optional Double)
      -> (b : Optional Double)
      -> (c : Optional Double)
      -> (d : Optional Double)
      -> (e : Optional Double)
      -> (f : Optional Double)
      -> (m11 : Optional Double)
      -> (m12 : Optional Double)
      -> (m21 : Optional Double)
      -> (m22 : Optional Double)
      -> (m41 : Optional Double)
      -> (m42 : Optional Double)
      -> JSIO DOMMatrix2DInit
  new a b c d e f g h i j k l = primJS
                              $ DOMMatrix2DInit.prim__new (toFFI a)
                                                          (toFFI b)
                                                          (toFFI c)
                                                          (toFFI d)
                                                          (toFFI e)
                                                          (toFFI f)
                                                          (toFFI g)
                                                          (toFFI h)
                                                          (toFFI i)
                                                          (toFFI j)
                                                          (toFFI k)
                                                          (toFFI l)

  export
  new' : JSIO DOMMatrix2DInit
  new' = primJS
       $ DOMMatrix2DInit.prim__new undef
                                   undef
                                   undef
                                   undef
                                   undef
                                   undef
                                   undef
                                   undef
                                   undef
                                   undef
                                   undef
                                   undef

  export
  a :  (0 _ : JSType t)
    => {auto 0 _ : Elem DOMMatrix2DInit (Types t)}
    -> t
    -> Attribute False Optional Double
  a v = fromUndefOrPrimNoDefault "DOMMatrix2DInit.geta"
                                 prim__a
                                 prim__setA
                                 (v :> DOMMatrix2DInit)

  export
  b :  (0 _ : JSType t)
    => {auto 0 _ : Elem DOMMatrix2DInit (Types t)}
    -> t
    -> Attribute False Optional Double
  b v = fromUndefOrPrimNoDefault "DOMMatrix2DInit.getb"
                                 prim__b
                                 prim__setB
                                 (v :> DOMMatrix2DInit)

  export
  c :  (0 _ : JSType t)
    => {auto 0 _ : Elem DOMMatrix2DInit (Types t)}
    -> t
    -> Attribute False Optional Double
  c v = fromUndefOrPrimNoDefault "DOMMatrix2DInit.getc"
                                 prim__c
                                 prim__setC
                                 (v :> DOMMatrix2DInit)

  export
  d :  (0 _ : JSType t)
    => {auto 0 _ : Elem DOMMatrix2DInit (Types t)}
    -> t
    -> Attribute False Optional Double
  d v = fromUndefOrPrimNoDefault "DOMMatrix2DInit.getd"
                                 prim__d
                                 prim__setD
                                 (v :> DOMMatrix2DInit)

  export
  e :  (0 _ : JSType t)
    => {auto 0 _ : Elem DOMMatrix2DInit (Types t)}
    -> t
    -> Attribute False Optional Double
  e v = fromUndefOrPrimNoDefault "DOMMatrix2DInit.gete"
                                 prim__e
                                 prim__setE
                                 (v :> DOMMatrix2DInit)

  export
  f :  (0 _ : JSType t)
    => {auto 0 _ : Elem DOMMatrix2DInit (Types t)}
    -> t
    -> Attribute False Optional Double
  f v = fromUndefOrPrimNoDefault "DOMMatrix2DInit.getf"
                                 prim__f
                                 prim__setF
                                 (v :> DOMMatrix2DInit)

  export
  m11 :  (0 _ : JSType t)
      => {auto 0 _ : Elem DOMMatrix2DInit (Types t)}
      -> t
      -> Attribute False Optional Double
  m11 v = fromUndefOrPrimNoDefault "DOMMatrix2DInit.getm11"
                                   prim__m11
                                   prim__setM11
                                   (v :> DOMMatrix2DInit)

  export
  m12 :  (0 _ : JSType t)
      => {auto 0 _ : Elem DOMMatrix2DInit (Types t)}
      -> t
      -> Attribute False Optional Double
  m12 v = fromUndefOrPrimNoDefault "DOMMatrix2DInit.getm12"
                                   prim__m12
                                   prim__setM12
                                   (v :> DOMMatrix2DInit)

  export
  m21 :  (0 _ : JSType t)
      => {auto 0 _ : Elem DOMMatrix2DInit (Types t)}
      -> t
      -> Attribute False Optional Double
  m21 v = fromUndefOrPrimNoDefault "DOMMatrix2DInit.getm21"
                                   prim__m21
                                   prim__setM21
                                   (v :> DOMMatrix2DInit)

  export
  m22 :  (0 _ : JSType t)
      => {auto 0 _ : Elem DOMMatrix2DInit (Types t)}
      -> t
      -> Attribute False Optional Double
  m22 v = fromUndefOrPrimNoDefault "DOMMatrix2DInit.getm22"
                                   prim__m22
                                   prim__setM22
                                   (v :> DOMMatrix2DInit)

  export
  m41 :  (0 _ : JSType t)
      => {auto 0 _ : Elem DOMMatrix2DInit (Types t)}
      -> t
      -> Attribute False Optional Double
  m41 v = fromUndefOrPrimNoDefault "DOMMatrix2DInit.getm41"
                                   prim__m41
                                   prim__setM41
                                   (v :> DOMMatrix2DInit)

  export
  m42 :  (0 _ : JSType t)
      => {auto 0 _ : Elem DOMMatrix2DInit (Types t)}
      -> t
      -> Attribute False Optional Double
  m42 v = fromUndefOrPrimNoDefault "DOMMatrix2DInit.getm42"
                                   prim__m42
                                   prim__setM42
                                   (v :> DOMMatrix2DInit)

namespace DOMMatrixInit

  export
  new :  (m13 : Optional Double)
      -> (m14 : Optional Double)
      -> (m23 : Optional Double)
      -> (m24 : Optional Double)
      -> (m31 : Optional Double)
      -> (m32 : Optional Double)
      -> (m33 : Optional Double)
      -> (m34 : Optional Double)
      -> (m43 : Optional Double)
      -> (m44 : Optional Double)
      -> (is2D : Optional Bool)
      -> JSIO DOMMatrixInit
  new a b c d e f g h i j k = primJS
                            $ DOMMatrixInit.prim__new (toFFI a)
                                                      (toFFI b)
                                                      (toFFI c)
                                                      (toFFI d)
                                                      (toFFI e)
                                                      (toFFI f)
                                                      (toFFI g)
                                                      (toFFI h)
                                                      (toFFI i)
                                                      (toFFI j)
                                                      (toFFI k)

  export
  new' : JSIO DOMMatrixInit
  new' = primJS
       $ DOMMatrixInit.prim__new undef
                                 undef
                                 undef
                                 undef
                                 undef
                                 undef
                                 undef
                                 undef
                                 undef
                                 undef
                                 undef

  export
  is2D :  (0 _ : JSType t)
       => {auto 0 _ : Elem DOMMatrixInit (Types t)}
       -> t
       -> Attribute False Optional Bool
  is2D v = fromUndefOrPrimNoDefault "DOMMatrixInit.getis2D"
                                    prim__is2D
                                    prim__setIs2D
                                    (v :> DOMMatrixInit)

  export
  m13 :  (0 _ : JSType t)
      => {auto 0 _ : Elem DOMMatrixInit (Types t)}
      -> t
      -> Attribute True Optional Double
  m13 v = fromUndefOrPrim "DOMMatrixInit.getm13"
                          prim__m13
                          prim__setM13
                          0
                          (v :> DOMMatrixInit)

  export
  m14 :  (0 _ : JSType t)
      => {auto 0 _ : Elem DOMMatrixInit (Types t)}
      -> t
      -> Attribute True Optional Double
  m14 v = fromUndefOrPrim "DOMMatrixInit.getm14"
                          prim__m14
                          prim__setM14
                          0
                          (v :> DOMMatrixInit)

  export
  m23 :  (0 _ : JSType t)
      => {auto 0 _ : Elem DOMMatrixInit (Types t)}
      -> t
      -> Attribute True Optional Double
  m23 v = fromUndefOrPrim "DOMMatrixInit.getm23"
                          prim__m23
                          prim__setM23
                          0
                          (v :> DOMMatrixInit)

  export
  m24 :  (0 _ : JSType t)
      => {auto 0 _ : Elem DOMMatrixInit (Types t)}
      -> t
      -> Attribute True Optional Double
  m24 v = fromUndefOrPrim "DOMMatrixInit.getm24"
                          prim__m24
                          prim__setM24
                          0
                          (v :> DOMMatrixInit)

  export
  m31 :  (0 _ : JSType t)
      => {auto 0 _ : Elem DOMMatrixInit (Types t)}
      -> t
      -> Attribute True Optional Double
  m31 v = fromUndefOrPrim "DOMMatrixInit.getm31"
                          prim__m31
                          prim__setM31
                          0
                          (v :> DOMMatrixInit)

  export
  m32 :  (0 _ : JSType t)
      => {auto 0 _ : Elem DOMMatrixInit (Types t)}
      -> t
      -> Attribute True Optional Double
  m32 v = fromUndefOrPrim "DOMMatrixInit.getm32"
                          prim__m32
                          prim__setM32
                          0
                          (v :> DOMMatrixInit)

  export
  m33 :  (0 _ : JSType t)
      => {auto 0 _ : Elem DOMMatrixInit (Types t)}
      -> t
      -> Attribute True Optional Double
  m33 v = fromUndefOrPrim "DOMMatrixInit.getm33"
                          prim__m33
                          prim__setM33
                          1
                          (v :> DOMMatrixInit)

  export
  m34 :  (0 _ : JSType t)
      => {auto 0 _ : Elem DOMMatrixInit (Types t)}
      -> t
      -> Attribute True Optional Double
  m34 v = fromUndefOrPrim "DOMMatrixInit.getm34"
                          prim__m34
                          prim__setM34
                          0
                          (v :> DOMMatrixInit)

  export
  m43 :  (0 _ : JSType t)
      => {auto 0 _ : Elem DOMMatrixInit (Types t)}
      -> t
      -> Attribute True Optional Double
  m43 v = fromUndefOrPrim "DOMMatrixInit.getm43"
                          prim__m43
                          prim__setM43
                          0
                          (v :> DOMMatrixInit)

  export
  m44 :  (0 _ : JSType t)
      => {auto 0 _ : Elem DOMMatrixInit (Types t)}
      -> t
      -> Attribute True Optional Double
  m44 v = fromUndefOrPrim "DOMMatrixInit.getm44"
                          prim__m44
                          prim__setM44
                          1
                          (v :> DOMMatrixInit)

namespace DOMPointInit

  export
  new :  (x : Optional Double)
      -> (y : Optional Double)
      -> (z : Optional Double)
      -> (w : Optional Double)
      -> JSIO DOMPointInit
  new a b c d = primJS
              $ DOMPointInit.prim__new (toFFI a) (toFFI b) (toFFI c) (toFFI d)

  export
  new' : JSIO DOMPointInit
  new' = primJS $ DOMPointInit.prim__new undef undef undef undef

  export
  w :  (0 _ : JSType t)
    => {auto 0 _ : Elem DOMPointInit (Types t)}
    -> t
    -> Attribute True Optional Double
  w v = fromUndefOrPrim "DOMPointInit.getw"
                        prim__w
                        prim__setW
                        1
                        (v :> DOMPointInit)

  export
  x :  (0 _ : JSType t)
    => {auto 0 _ : Elem DOMPointInit (Types t)}
    -> t
    -> Attribute True Optional Double
  x v = fromUndefOrPrim "DOMPointInit.getx"
                        prim__x
                        prim__setX
                        0
                        (v :> DOMPointInit)

  export
  y :  (0 _ : JSType t)
    => {auto 0 _ : Elem DOMPointInit (Types t)}
    -> t
    -> Attribute True Optional Double
  y v = fromUndefOrPrim "DOMPointInit.gety"
                        prim__y
                        prim__setY
                        0
                        (v :> DOMPointInit)

  export
  z :  (0 _ : JSType t)
    => {auto 0 _ : Elem DOMPointInit (Types t)}
    -> t
    -> Attribute True Optional Double
  z v = fromUndefOrPrim "DOMPointInit.getz"
                        prim__z
                        prim__setZ
                        0
                        (v :> DOMPointInit)

namespace DOMQuadInit

  export
  new :  (0 _ : JSType t1)
      => (0 _ : JSType t2)
      => (0 _ : JSType t3)
      => (0 _ : JSType t4)
      => {auto 0 _ : Elem DOMPointInit (Types t1)}
      -> {auto 0 _ : Elem DOMPointInit (Types t2)}
      -> {auto 0 _ : Elem DOMPointInit (Types t3)}
      -> {auto 0 _ : Elem DOMPointInit (Types t4)}
      -> (p1 : Optional t1)
      -> (p2 : Optional t2)
      -> (p3 : Optional t3)
      -> (p4 : Optional t4)
      -> JSIO DOMQuadInit
  new a b c d = primJS
              $ DOMQuadInit.prim__new (optUp a) (optUp b) (optUp c) (optUp d)

  export
  new' : JSIO DOMQuadInit
  new' = primJS $ DOMQuadInit.prim__new undef undef undef undef

  export
  p1 :  (0 _ : JSType t)
     => {auto 0 _ : Elem DOMQuadInit (Types t)}
     -> t
     -> Attribute False Optional DOMPointInit
  p1 v = fromUndefOrPrimNoDefault "DOMQuadInit.getp1"
                                  prim__p1
                                  prim__setP1
                                  (v :> DOMQuadInit)

  export
  p2 :  (0 _ : JSType t)
     => {auto 0 _ : Elem DOMQuadInit (Types t)}
     -> t
     -> Attribute False Optional DOMPointInit
  p2 v = fromUndefOrPrimNoDefault "DOMQuadInit.getp2"
                                  prim__p2
                                  prim__setP2
                                  (v :> DOMQuadInit)

  export
  p3 :  (0 _ : JSType t)
     => {auto 0 _ : Elem DOMQuadInit (Types t)}
     -> t
     -> Attribute False Optional DOMPointInit
  p3 v = fromUndefOrPrimNoDefault "DOMQuadInit.getp3"
                                  prim__p3
                                  prim__setP3
                                  (v :> DOMQuadInit)

  export
  p4 :  (0 _ : JSType t)
     => {auto 0 _ : Elem DOMQuadInit (Types t)}
     -> t
     -> Attribute False Optional DOMPointInit
  p4 v = fromUndefOrPrimNoDefault "DOMQuadInit.getp4"
                                  prim__p4
                                  prim__setP4
                                  (v :> DOMQuadInit)

namespace DOMRectInit

  export
  new :  (x : Optional Double)
      -> (y : Optional Double)
      -> (width : Optional Double)
      -> (height : Optional Double)
      -> JSIO DOMRectInit
  new a b c d = primJS
              $ DOMRectInit.prim__new (toFFI a) (toFFI b) (toFFI c) (toFFI d)

  export
  new' : JSIO DOMRectInit
  new' = primJS $ DOMRectInit.prim__new undef undef undef undef

  export
  height :  (0 _ : JSType t)
         => {auto 0 _ : Elem DOMRectInit (Types t)}
         -> t
         -> Attribute True Optional Double
  height v = fromUndefOrPrim "DOMRectInit.getheight"
                             prim__height
                             prim__setHeight
                             0
                             (v :> DOMRectInit)

  export
  width :  (0 _ : JSType t)
        => {auto 0 _ : Elem DOMRectInit (Types t)}
        -> t
        -> Attribute True Optional Double
  width v = fromUndefOrPrim "DOMRectInit.getwidth"
                            prim__width
                            prim__setWidth
                            0
                            (v :> DOMRectInit)

  export
  x :  (0 _ : JSType t)
    => {auto 0 _ : Elem DOMRectInit (Types t)}
    -> t
    -> Attribute True Optional Double
  x v = fromUndefOrPrim "DOMRectInit.getx"
                        prim__x
                        prim__setX
                        0
                        (v :> DOMRectInit)

  export
  y :  (0 _ : JSType t)
    => {auto 0 _ : Elem DOMRectInit (Types t)}
    -> t
    -> Attribute True Optional Double
  y v = fromUndefOrPrim "DOMRectInit.gety"
                        prim__y
                        prim__setY
                        0
                        (v :> DOMRectInit)


text:
module Main

import Data.Vect

data DataStore : Type where
     MkData : (size : Nat) ->
              (items : Vect size String) ->
              DataStore

data Command = Add String
               | Get Integer
               | Size
               | Quit

size : DataStore -> Nat
size (MkData size' items') = size'

items : (store : DataStore) -> Vect (size store) String
items (MkData _ items') = items'

addToStore : DataStore -> String -> DataStore
addToStore (MkData _ items) item = MkData _ (add item items)
           where
            add : String -> Vect old String -> Vect (S old) String
            add item [] = [item]
            add item (x :: xs) = x :: add item xs

parseCommand : (cmd : String) -> (args : String) -> Maybe Command
parseCommand "add" str = Just (Add str)
parseCommand "get" val = case all isDigit (unpack val) of
                              False => Nothing
                              True => Just (Get (cast val))
parseCommand "size" _ = Just Size
parseCommand "quit" "" = Just Quit
parseCommand _ _ = Nothing

parse : (input : String) -> Maybe Command
parse input = case Strings.span (/= ' ') input of
              (cmd, args) => parseCommand cmd (Strings.ltrim args)

getEntry : (pos : Integer) -> (store : DataStore) -> Maybe (String, DataStore)
getEntry pos store = let store_items = items store in
                         case integerToFin pos (size store) of
                              Nothing => Nothing
                              Just f => Just (index f store_items ++ "\n", store)

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store inp = case parse inp of
                              Nothing => Just ("Invalid command\n", store)
                              Just (Add item) => Just ("ID " ++ show (size store) ++ "\n ", addToStore store item)
                              Just (Get pos) => getEntry pos store
                              Just Size => let (MkData size _) = store in Just (("Size = " ++ show size ++ "\n"), store)
                              Just Quit => Nothing

main : IO ()
main = replWith (MkData _ ["Moscow", "Kurgan", "Ekaterinburg"]) "Command: " processInput

Enter the sequantally strings and press Enter when input will be compleated.


text:
module Main

import Data.Vect

infixr 5 .+.

data Schema = SString
            | SInt
            | SChar
            | (.+.) Schema Schema

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

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

-- search : (store : DataStore) -> String -> List String
-- search (MkData _ items) q = filter (isInfixOf q) (toList items)

-- search' : (store : DataStore) -> String -> List (Nat, String)
-- search' (MkData size items) q
--   = filter ((isInfixOf q) . snd)
--            (zip (enumFromTo 0 size) (toList items))

addToStore : (store : DataStore) -> SchemaType (schema store) -> DataStore
addToStore (MkData schema size items) item = MkData schema _ (addToData items)
  where
    addToData : Vect old (SchemaType schema) -> Vect (S old) (SchemaType schema)
    addToData [] = [item]
    addToData (x :: xs) = x :: addToData xs

-- sumInputs : Integer -> String -> Maybe (String, Integer)
-- sumInputs sum input
--   = let val = cast input in
--         if val < 0
--         then Nothing
--         else let newVal = sum + val in
--                  Just ("Subtotal: " ++ show newVal ++ "\n", newVal)

data Command : Schema -> Type where
  SetSchema : (new : Schema) -> Command schema
  Add : SchemaType schema -> Command schema
  Get : Integer -> Command schema
  GetAll : Command schema
  Search : String -> Command schema
  Size : Command schema
  Quit : Command schema

mutual
  parseSchema : List String -> Maybe Schema
  parseSchema ("String" :: xs) = doParseSchema xs SString
  parseSchema ("Int" :: xs) = doParseSchema xs SInt
  parseSchema ("Char" :: xs) = doParseSchema xs SChar
  parseSchema _ = Nothing

  doParseSchema : List String -> Schema -> Maybe Schema
  doParseSchema [] type = Just type
  doParseSchema xs type = do
    xs' <- parseSchema xs
    pure (type .+. xs')

setSchema : (store : DataStore) -> Schema -> Maybe DataStore
setSchema store schema =
  case size store of
       Z => Just (MkData schema _ [])
       (S k) => Nothing

parsePrefix : (schema : Schema) -> String -> Maybe (SchemaType schema, String)
parsePrefix SString input = getQuoted (unpack input)
  where
    getQuoted : List Char -> Maybe (String, String)
    getQuoted ('"' :: xs) =
      case span (/= '"') xs of
        (quoted, '"' :: rest) => Just (pack quoted, ltrim (pack rest))
        _ => Nothing
    getQuoted _ = Nothing
parsePrefix SInt input = case span isDigit input of
                             ("", rest) => Nothing
                             (num, rest) => Just (cast num, ltrim rest)
parsePrefix SChar input = getQuoted (unpack input)
  where
    getQuoted : List Char -> Maybe (Char, String)
    getQuoted ('\'' :: c :: '\'' :: rest) = Just (c, ltrim (pack rest))
    getQuoted ('\'' :: '\\' :: '\'' :: '\'' :: rest) = Just ('\'', ltrim (pack rest))
    getQuoted _ = Nothing
parsePrefix (lft .+. rgt) input = do
  (l, input') <- parsePrefix lft input
  (r, input'') <- parsePrefix rgt input'
  pure ((l, r), input'')

parseBySchema : (schema : Schema) -> String -> Maybe (SchemaType schema)
parseBySchema schema input = do
  (res, "") <- parsePrefix schema input | _ => Nothing
  pure res

parseCommand : (schema : Schema) -> (cmd : String) -> (args : String) -> Maybe (Command schema)
parseCommand schema "add" str = Add <$> parseBySchema schema str
parseCommand schema "get" "" = Just GetAll
parseCommand schema "get" val =
  case all isDigit (unpack val) of
       False => Nothing
       True => Just (Get (cast val))
parseCommand schema "search" query = Just (Search query)
parseCommand schema "size" "" = Just Size
parseCommand schema "quit" "" = Just Quit
parseCommand schema "schema" str = SetSchema <$> parseSchema (words str)
parseCommand _ _ _ = Nothing

parse : (schema : Schema) -> (input : String) -> Maybe (Command schema)
parse schema input =
  case span (/= ' ') input of
       (cmd, args) => parseCommand schema cmd (ltrim args)

display : (SchemaType schema) -> String
display {schema = SString} item = show item
display {schema = SInt} item = show item
display {schema = SChar} item = show item
display {schema = (_ .+. _)} (l, r) = (display l) ++ ", " ++ (display r)

showStore : DataStore -> String
showStore store = showItems (items store)
  where
    showItems : Vect size (SchemaType schema) -> String
    showItems = concat . map (\x => display x ++ "\n")

getEntry : (store : DataStore) -> (id : Integer) -> Maybe String
getEntry store id = do
  id' <- integerToFin id (size store)
  pure (display (index id' (items store)))

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input
  = case parse (schema store) input of
         Nothing => Just ("Invalid command\n", store)
         Just cmd => processCommand cmd
  where
    processCommand : (cmd : Command (schema store)) -> Maybe (String, DataStore)
    processCommand (Add item)
      = Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
    processCommand (Get id) = case getEntry store id of
                                         Just item => Just (item ++ "\n", store)
                                         Nothing => Just ("Out of range\n", store)
    processCommand GetAll = Just (showStore store, store)
    -- processCommand (Search query)
    --   = let results = search' store query
    --         results' = map (\(k, v) => show k ++ ": " ++ v) results in
    --         Just (unlines results' ++ "\n", store)
    processCommand Size = Just ("Size: " ++ show (size store) ++ "\n", store)
    processCommand (SetSchema schema') =
      case setSchema store schema' of
           Nothing => Just ("Can't update schema\n", store)
           Just store' => Just ("OK\n", store')
    processCommand Quit = Nothing

main : IO ()
main = replWith (MkData SString Z [])  "Command: " processInput

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module DataStore2

import Data.Vect

infixr 5 .+.

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

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

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

addToStore : (store : DataStore) -> SchemaType (schema store) ->
             DataStore
addToStore (MkData schema _ items) newitem = MkData schema _ (addToData items)
  where addToData : Vect oldsize (SchemaType schema) -> Vect (S oldsize)
                    (SchemaType schema)
        addToData [] = [newitem]
        addToData (x :: xs) = newitem :: x :: xs

display : (schema : Schema) -> SchemaType schema -> String
display SString x = x
display SInt x = show x
display (s1 .+. s2) (t1, t2) = "(" ++ display s1 t1 ++ ", " ++ display s2 t2 ++
                               ")"

getAction : (pos : Integer) -> (store : DataStore) -> Maybe (String, DataStore)
getAction pos store = case integerToFin pos (size store) of
                           Nothing => Just ("Out of range", store)
                           Just id => Just (display (schema store) (index id (items store)) ++
                                            "\n", store)

data Command: Schema -> Type where
  Add : SchemaType schema -> Command schema
  Get : Integer -> Command schema
  Size : Command schema
  Search : String -> Command schema
  Quit : Command schema

parseBySchema : (schema : Schema) -> (str : String) -> Maybe (SchemaType schema)
parseBySchema SString str = Just str
parseBySchema SInt str = Just (cast str)
parseBySchema (x .+. y) str = ?parseBySchema_rhs_3

parseCommand : (schema : Schema) -> (cmd : String) -> (args : String)
               -> Maybe (Command schema)
parseCommand schema "add" str = case parseBySchema schema str of
                                     Nothing => Nothing
                                     Just item => Just (Add item)
parseCommand schema "get" val = case all isDigit (unpack val) of
                                     False => Nothing
                                     True => Just (Get (cast val))
parseCommand schema "quit" "" = Just Quit
parseCommand schema "size" "" = Just Size
parseCommand schema "search" str = Just (Search str)
parseCommand _ _ _ = Nothing

parse : (schema : Schema) -> (input : String) -> Maybe (Command schema)
parse schema input = case span (/= ' ') input of
                          (cmd, args) => parseCommand schema cmd (ltrim args)

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input =
    case parse (schema store) input of
         Nothing => Just ("Invalid command\n", store)
         Just Quit => Nothing
         Just (Add item) => Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
         Just (Get pos) => case integerToFin pos (size store) of
                                Nothing => Just ("Out of range \n", store)
                                Just id => Just (?show (index id (items store)) ++ "\n", store)
         Just Size => Just ("Number of items: " ++ show (size store) ++ "\n", store)
         Just (Search x) => case findIndices (isInfixOf x) (map ?show (items store)) of
                                 [] => Just ("Item not found\n", store)
                                 idx => Just (concat (map showSearchIdx idx), store)
    where showSearchIdx : Fin (size store) -> String
          showSearchIdx id = show (finToNat id) ++ ": " ++ ?show (index id (items store)) ++ "\n"

max_stars_repo_name: neduard/type-driven-development

max_issues_repo_name: neduard/type-driven-development

max_forks_repo_name: neduard/type-driven-development


text:
module SemVar

import SemVar.Lexer
import SemVar.Parser
import public SemVar.Data

import Text.Bounded

||| Parse a Version
export
parseVersion : String -> Maybe Version
parseVersion x = parseVersionToks !(lexSemVar x)

||| Parse a Requirement
export
parseRequirement : String -> Maybe Requirement
parseRequirement x = parseRequirementToks !(lexSemVar x)

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo