text:
module Grover

import Data.Nat
import Data.Vect
import Decidable.Equality
import Unitary
import Injection
import LinearTypes
import Lemmas
import Control.Linear.LIO
import QStateT
import AlterningBitsOracle
import QuantumOp

%default total

|||GROVER'S ALGORITHM
|||1. Start with |0> ¤ n
|||2. Apply H ¤ n
|||3. Grover iteration
|||   3.1 : Apply oracle
|||   3.2 : Apply H ¤ n
|||   3.3 : Amplification
|||   3.4 : Apply H ¤ n

------------- AMPLIFICATION-------------

public export total
amplification : (n : Nat) -> Unitary n
amplification 0 = IdGate
amplification 1 = IdGate
amplification (S k) =
  let x = tensorn (S k) (X 0 IdGate)
      h1 = H k {prf = lemmaLTSucc k} x
      c = multipleQubitControlledNOT (S k) . h1
      h2 = H k {prf = lemmaLTSucc k} c
  in x . h2

---------------GROVER ITERATION--------------

public export total
groverIteration : (n : Nat) -> {p : Nat} -> (oracle : Unitary (n + p)) -> Unitary (n + p)
groverIteration n oracle =
  let h = tensorn n (H 0 IdGate)
  in (h # IdGate) . (amplification n # IdGate) . (h # IdGate) . oracle

public export total
repeatGroverIteration : (k : Nat) -> (n : Nat) -> {p : Nat} -> (oracle : Unitary (n + p)) -> Unitary (n + p)
repeatGroverIteration 0 n _ = IdGate
repeatGroverIteration (S k) n oracle = (groverIteration n oracle) . (repeatGroverIteration k n oracle)

----------------GROVER'S ALGORITHM------------------

xhAncilla : (p : Nat) -> Unitary p
xhAncilla 0 = IdGate
xhAncilla (S p) = let xh = (H 0 IdGate) . (X 0 IdGate) in rewrite sym $ lemmaplusOneRight p in IdGate # xh

hxAncilla : (p : Nat) -> Unitary p
hxAncilla 0 = IdGate
hxAncilla (S p) = let xh = (X 0 IdGate) . (H 0 IdGate) in rewrite sym $ lemmaplusOneRight p in IdGate # xh

public export total
grover' : (n : Nat) -> {p : Nat} -> (oracle : Unitary (n + p)) -> (nbIter : Nat) -> Unitary (n + p)
grover' n oracle nbIter =
  let h = (tensorn n (H 0 IdGate)) # xhAncilla p
  in (IdGate # hxAncilla p) . (repeatGroverIteration nbIter n oracle) . h

public export total
grover : QuantumOp t =>
         (n : Nat) -> {p : Nat} -> (oracle : Unitary (n + p)) -> (nbIter : Nat) -> IO (Vect n Bool)
grover n oracle nbIter = do
    let circuit = grover' n oracle nbIter
    w <- run (do
                 q <- newQubits {t=t} (n + p)
                 q <- applyUnitary q circuit
                 v <- measureAll q
                 pure v
                 )
    pure (take n w)

--------------------------SMALL TEST---------------------------

--Example with the alternating bits oracle

public export
testGrover : IO (Vect 4 Bool)
testGrover =
  grover {t = SimulatedOp} 4 {p = 1} (solve 2) 1

public export
testG : (nbIter : Nat) -> IO (Vect 3 Nat)
testG 0 = pure [0,0,0]
testG (S k) = do
  [a,b,c] <- testG k
  v <- testGrover
  case v of
       [True,False,True,False] => pure [S a,b,c]
       [False,True,False,True] => pure [a,S b,c]
       _ => pure [a,b,S c]

max_stars_repo_name: zamdzhiev/Qimaera

max_issues_repo_name: zamdzhiev/Qimaera

max_forks_repo_name: zamdzhiev/Qimaera


text:
import Decidable.Equality

data Vect : Nat -> Type -> Type where
     Nil  : Vect Z a
     (::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a
%name Vect xs, ys, zs

-- the equalities below (i.e (x = y) -> Void ) get constrained
-- to be the same value (i.e (x = x) -> Void )

headUnequal : DecEq a => {xs : Vect n a} -> {ys : Vect n a} ->
       (contra : (x = y) -> Void) -> ((x :: xs) = (y :: ys)) -> Void
headUnequal contra Refl = contra Refl

tailUnequal : DecEq a => {xs : Vect n a} -> {ys : Vect n a} ->
       (contra : (xs = ys) -> Void) -> ((x :: xs) = (y :: ys)) -> Void
tailUnequal contra Refl = contra Refl

DecEq a => DecEq (Vect n a) where
       decEq [] [] = Yes Refl
       decEq (x :: xs) (y :: ys) =
              case decEq x y of
                   Yes Refl => case decEq xs ys of
                                    Yes Refl => Yes Refl
                                    No contra => No (tailUnequal contra)
                   No contra => No (headUnequal contra)

ext: idr


text:
module Examples.AOC1

import Data.String
import Data.Vect

import Stream
import System
import System.File

export
part1 : IO ()
part1 = ignore $ withLines "resources/aoc1a" $ \ls => do
  res <- run
       . count_ (\[x,y] => x > y)
       . slidingWindow 2
       $ mapVals (cast {to = Nat} . trim) ls
  putStrLn "Day1, Result A: \{show res}"

export
part2 : IO ()
part2 = ignore $ withLines "resources/aoc1a" $ \ls => do
  res <- run
       . count_ (\[x,y] => sum x > sum y)
       . slidingWindow 2
       . slidingWindow 3
       $ mapVals (cast {to = Nat} . trim) ls
  putStrLn "Day1, Result B: \{show res}"


text:
module Data.Vect

import Data.DPair
import Data.List
import Data.Nat
import public Data.Fin
import public Data.Zippable

import Decidable.Equality

%default total

public export
data Vect : (len : Nat) -> (elem : Type) -> Type where
  ||| Empty vector
  Nil  : Vect Z elem
  ||| A non-empty vector of length `S len`, consisting of a head element and
  ||| the rest of the list, of length `len`.
  (::) : (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem

-- Hints for interactive editing
%name Vect xs, ys, zs, ws

public export
length : (xs : Vect len elem) -> Nat
length [] = 0
length (_::xs) = 1 + length xs

||| Show that the length function on vectors in fact calculates the length
export
lengthCorrect : (xs : Vect len elem) -> length xs = len
lengthCorrect []        = Refl
lengthCorrect (_ :: xs) = rewrite lengthCorrect xs in Refl

||| If two vectors are equal, their heads and tails are equal
export
vectInjective : {0 xs : Vect n a} -> {0 ys : Vect m b} -> x::xs = y::ys -> (x = y, xs = ys)
vectInjective Refl = (Refl, Refl)

--------------------------------------------------------------------------------
-- Indexing into vectors
--------------------------------------------------------------------------------

||| All but the first element of the vector
|||
||| ```idris example
||| tail [1,2,3,4]
||| ```
public export
tail : Vect (S len) elem -> Vect len elem
tail (_::xs) = xs

||| Only the first element of the vector
|||
||| ```idris example
||| head [1,2,3,4]
||| ```
public export
head : Vect (S len) elem -> elem
head (x::_) = x

||| The last element of the vector
|||
||| ```idris example
||| last [1,2,3,4]
||| ```
public export
last : Vect (S len) elem -> elem
last [x]        = x
last (_::y::ys) = last $ y::ys

||| All but the last element of the vector
|||
||| ```idris example
||| init [1,2,3,4]
||| ```
public export
init : Vect (S len) elem -> Vect len elem
init [_]        = []
init (x::y::ys) = x :: init (y::ys)

||| Extract the first `n` elements of a Vect.
public export
take : (n  : Nat)
    -> (  xs : Vect (n + m) type)
    -> Vect n type
take 0 xs = Nil
take (S k) (x :: xs) = x :: take k xs

namespace Stream
  ||| Take precisely n elements from the stream.
  ||| @ n how many elements to take
  ||| @ xs the stream
  public export
  take : (n : Nat) -> (xs : Stream a) -> Vect n a
  take Z xs = []
  take (S k) (x :: xs) = x :: take k xs

||| Drop the first `n` elements of a Vect.
public export
drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem
drop 0 xs = xs
drop (S k) (x :: xs) = drop k xs

||| Drop up to the first `n` elements of a Vect.
public export
drop' : (n : Nat) -> Vect l elem -> Vect (l `minus` n) elem
drop' 0 xs = rewrite minusZeroRight l in xs
drop' (S k) [] = rewrite minusZeroLeft (S k) in []
drop' (S k) (x :: xs) = drop' k xs

||| Extract a particular element from a vector
|||
||| ```idris example
||| index 1 [1,2,3,4]
||| ```
public export
index : Fin len -> Vect len elem -> elem
index FZ     (x::_)  = x
index (FS k) (_::xs) = index k xs

||| Insert an element at a particular index
|||
||| ```idris example
||| insertAt 1 8 [1,2,3,4]
||| ```
public export
insertAt : (idx : Fin (S len)) -> (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem
insertAt FZ     y xs      = y :: xs
insertAt (FS k) y (x::xs) = x :: insertAt k y xs

||| Construct a new vector consisting of all but the indicated element
|||
||| ```idris example
||| deleteAt 1 [1,2,3,4]
||| ```
public export
deleteAt : Fin (S len) -> Vect (S len) elem -> Vect len elem
deleteAt FZ     (_::xs)        = xs
deleteAt (FS k) [x]            = absurd k
deleteAt (FS k) (x::xs@(_::_)) = x :: deleteAt k xs

||| Replace an element at a particlar index with another
|||
||| ```idris example
||| replaceAt 1 8 [1,2,3,4]
||| ```
public export
replaceAt : Fin len -> elem -> Vect len elem -> Vect len elem
replaceAt FZ     y (_::xs) = y :: xs
replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs

||| Replace the element at a particular index with the result of applying a function to it
||| @ i the index to replace at
||| @ f the update function
||| @ xs the vector to replace in
|||
||| ```idris example
||| updateAt 1 (+10) [1,2,3,4]
||| ```
public export
updateAt : (i : Fin len) -> (f : elem -> elem) -> (xs : Vect len elem) -> Vect len elem
updateAt FZ     f (x::xs) = f x :: xs
updateAt (FS k) f (x::xs) = x :: updateAt k f xs

||| Append two vectors
|||
||| ```idris example
||| [1,2,3,4] ++ [5,6]
||| ```
public export
(++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem
(++) []      ys = ys
(++) (x::xs) ys = x :: xs ++ ys

||| Add an element at the end of the vector.
||| The main use case for it is to get the expected type signature
||| `Vect n a -> a -> Vect (S n) a` instead of
||| `Vect n a -> a -> Vect (n + 1) a` which you get by using `++ [x]`
|||
||| Snoc gets its name by reversing `cons`, indicating we are
||| tacking on the element at the end rather than the begining.
||| `append` would also be a suitable name.
|||
||| @ xs The vector to be appended
||| @ v The value to append
public export
snoc : (xs : Vect n a) -> (v : a) -> Vect (S n) a
snoc [] v = [v]
snoc (x :: xs) v = x :: snoc xs v

||| Repeate some value some number of times.
|||
||| @ len the number of times to repeat it
||| @ x the value to repeat
|||
||| ```idris example
||| replicate 4 1
||| ```
public export
replicate : (len : Nat) -> (x : elem) -> Vect len elem
replicate Z     _ = []
replicate (S k) x = x :: replicate k x

||| Merge two ordered vectors
|||
||| ```idris example
||| mergeBy compare (fromList [1,3,5]) (fromList [2,3,4,5,6])
||| ```
export
mergeBy : (elem -> elem -> Ordering) -> (xs : Vect n elem) -> (ys : Vect m elem) -> Vect (n + m) elem
mergeBy _ [] ys = ys
mergeBy _ xs [] = rewrite plusZeroRightNeutral n in xs
mergeBy {n = S k} {m = S k'} order (x :: xs) (y :: ys)
     = case order x y of
            LT => x :: mergeBy order xs (y :: ys)
            _  => rewrite sym (plusSuccRightSucc k k') in
                             y :: mergeBy order (x :: xs) ys

export
merge : Ord elem => Vect n elem -> Vect m elem -> Vect (n + m) elem
merge = mergeBy compare

-- Properties for functions in this section --

export
replaceAtSameIndex : (xs : Vect n a) -> (i : Fin n) -> (0 y : a) -> index i (replaceAt i y xs) = y
replaceAtSameIndex (_::_) FZ     _ = Refl
replaceAtSameIndex (_::_) (FS _) _ = replaceAtSameIndex _ _ _

export
replaceAtDiffIndexPreserves : (xs : Vect n a) -> (i, j : Fin n) -> Not (i = j) -> (0 y : a) -> index i (replaceAt j y xs) = index i xs
replaceAtDiffIndexPreserves (_::_) FZ     FZ     co _ = absurd $ co Refl
replaceAtDiffIndexPreserves (_::_) FZ     (FS _) _  _ = Refl
replaceAtDiffIndexPreserves (_::_) (FS _) FZ     _  _ = Refl
replaceAtDiffIndexPreserves (_::_) (FS z) (FS w) co y = replaceAtDiffIndexPreserves _ z w (co . cong FS) y

--------------------------------------------------------------------------------
-- Transformations
--------------------------------------------------------------------------------

||| Reverse the order of the elements of a vector
|||
||| ```idris example
||| reverse [1,2,3,4]
||| ```
public export
reverse : (xs : Vect len elem) -> Vect len elem
reverse xs = go [] xs
  where go : Vect n elem -> Vect m elem -> Vect (n+m) elem
        go {n}         acc []        = rewrite plusZeroRightNeutral n in acc
        go {n} {m=S m} acc (x :: xs) = rewrite sym $ plusSuccRightSucc n m
                                       in go (x::acc) xs

||| Alternate an element between the other elements of a vector
||| @ sep the element to intersperse
||| @ xs the vector to separate with `sep`
|||
||| ```idris example
||| intersperse 0 [1,2,3,4]
||| ```
export
intersperse : (sep : elem) -> (xs : Vect len elem) -> Vect (len + pred len) elem
intersperse sep []      = []
intersperse sep (x::xs) = x :: intersperse' sep xs
  where
    intersperse' : elem -> Vect n elem -> Vect (n + n) elem
    intersperse'         sep []      = []
    intersperse' {n=S n} sep (x::xs) = rewrite sym $ plusSuccRightSucc n n
                                       in sep :: x :: intersperse' sep xs

--------------------------------------------------------------------------------
-- Conversion from list (toList is provided by Foldable)
--------------------------------------------------------------------------------

public export
toVect : (n : Nat) -> List a -> Maybe (Vect n a)
toVect Z [] = Just []
toVect (S k) (x :: xs)
    = do xs' <- toVect k xs
         pure (x :: xs')
toVect _ _ = Nothing

public export
fromList' : (xs : Vect len elem) -> (l : List elem) -> Vect (length l + len) elem
fromList' ys [] = ys
fromList' ys (x::xs) =
  rewrite (plusSuccRightSucc (length xs) len) in
  fromList' (x::ys) xs

||| Convert a list to a vector.
|||
||| The length of the list should be statically known.
|||
||| ```idris example
||| fromList [1,2,3,4]
||| ```
public export
fromList : (xs : List elem) -> Vect (length xs) elem
fromList l =
  rewrite (sym $ plusZeroRightNeutral (length l)) in
  reverse $ fromList' [] l

--------------------------------------------------------------------------------
-- Equality
--------------------------------------------------------------------------------

public export
Eq a => Eq (Vect n a) where
  (==) []      []      = True
  (==) (x::xs) (y::ys) = x == y && xs == ys

public export
DecEq a => DecEq (Vect n a) where
  decEq []      []      = Yes Refl
  decEq (x::xs) (y::ys) with (decEq x y, decEq xs ys)
    decEq (x::xs) (x::xs) | (Yes Refl, Yes Refl) = Yes Refl
    decEq (x::xs) (y::ys) | (No nhd, _) = No $ nhd . fst . vectInjective
    decEq (x::xs) (y::ys) | (_, No ntl) = No $ ntl . snd . vectInjective

--------------------------------------------------------------------------------
-- Order
--------------------------------------------------------------------------------

public export
implementation Ord elem => Ord (Vect len elem) where
  compare []      []      = EQ
  compare (x::xs) (y::ys)
      = case compare x y of
             EQ => compare xs ys
             x => x

--------------------------------------------------------------------------------
-- Maps
--------------------------------------------------------------------------------

public export
implementation Functor (Vect n) where
  map f []        = []
  map f (x::xs) = f x :: map f xs

||| Map a partial function across a vector, returning those elements for which
||| the function had a value.
|||
||| The first projection of the resulting pair (ie the length) will always be
||| at most the length of the input vector. This is not, however, guaranteed
||| by the type.
|||
||| @ f the partial function (expressed by returning `Maybe`)
||| @ xs the vector to check for results
|||
||| ```idris example
||| mapMaybe ((find (=='a')) . unpack) (fromList ["abc","ade","bgh","xyz"])
||| ```
export
mapMaybe : (f : a -> Maybe b) -> (xs : Vect len a) -> (m : Nat ** Vect m b)
mapMaybe f []      = (_ ** [])
mapMaybe f (x::xs) =
  let (len ** ys) = mapMaybe f xs
  in case f x of
       Just y  => (S len ** y :: ys)
       Nothing => (  len **      ys)

--------------------------------------------------------------------------------
-- Folds
--------------------------------------------------------------------------------

public export
foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> Vect n t -> acc
foldrImpl f e go [] = go e
foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs

public export
implementation Foldable (Vect n) where
  foldr f e xs = foldrImpl f e id xs
  foldl f z [] = z
  foldl f z (x :: xs) = foldl f (f z x) xs

  null [] = True
  null _ = False

  foldMap f = foldl (\acc, elem => acc <+> f elem) neutral

--------------------------------------------------------------------------------
-- Special folds
--------------------------------------------------------------------------------

||| Flatten a vector of equal-length vectors
|||
||| ```idris example
||| concat [[1,2,3], [4,5,6]]
||| ```
public export
concat : (xss : Vect m (Vect n elem)) -> Vect (m * n) elem
concat []      = []
concat (v::vs) = v ++ Vect.concat vs

||| Foldr without seeding the accumulator
|||
||| ```idris example
||| foldr1 (-) (fromList [1,2,3])
||| ```
public export
foldr1 : (t -> t -> t) -> Vect (S n) t -> t
foldr1 f [x]        = x
foldr1 f (x::y::xs) = f x (foldr1 f (y::xs))

||| Foldl without seeding the accumulator
|||
||| ```idris example
||| foldl1 (-) (fromList [1,2,3])
||| ```
public export
foldl1 : (t -> t -> t) -> Vect (S n) t -> t
foldl1 f (x::xs) = foldl f x xs
--------------------------------------------------------------------------------
-- Scans
--------------------------------------------------------------------------------

||| The scanl function is similar to foldl, but returns all the intermediate
||| accumulator states in the form of a vector.
|||
||| ```idris example
||| scanl (-) 0 (fromList [1,2,3])
||| ```
public export
scanl : (res -> elem -> res) -> res -> Vect len elem -> Vect (S len) res
scanl f q []      = [q]
scanl f q (x::xs) = q :: scanl f (f q x) xs

||| The scanl1 function is a variant of scanl that doesn't require an explicit
||| starting value.
||| It assumes the first element of the vector to be the starting value and then
||| starts the fold with the element following it.
|||
||| ```idris example
||| scanl1 (-) (fromList [1,2,3])
||| ```
public export
scanl1 : (elem -> elem -> elem) -> Vect len elem -> Vect len elem
scanl1 f [] = []
scanl1 f (x::xs) = scanl f x xs

--------------------------------------------------------------------------------
-- Membership tests
--------------------------------------------------------------------------------

||| Search for an item using a user-provided test
||| @ p the equality test
||| @ e the item to search for
||| @ xs the vector to search in
|||
||| ```idris example
||| elemBy (==) 2 [1,2,3,4]
||| ```
public export
elemBy : (p : elem -> elem -> Bool) -> (e : elem) -> (xs : Vect len elem) -> Bool
elemBy p e []      = False
elemBy p e (x::xs) = p e x || elemBy p e xs

||| Use the default Boolean equality on elements to search for an item
||| @ x what to search for
||| @ xs where to search
|||
||| ```idris example
||| elem 3 [1,2,3,4]
||| ```
public export
elem : Eq elem => (x : elem) -> (xs : Vect len elem) -> Bool
elem = elemBy (==)

||| Find the association of some key with a user-provided comparison
||| @ p the comparison operator for keys (True if they match)
||| @ e the key to look for
|||
||| ```idris example
||| lookupBy (==) 2 [(1, 'a'), (2, 'b'), (3, 'c')]
||| ```
public export
lookupBy : (p : key -> key -> Bool) -> (e : key) -> (xs : Vect n (key, val)) -> Maybe val
lookupBy p e []           = Nothing
lookupBy p e ((l, r)::xs) = if p e l then Just r else lookupBy p e xs

||| Find the assocation of some key using the default Boolean equality test
|||
||| ```idris example
||| lookup 3 [(1, 'a'), (2, 'b'), (3, 'c')]
||| ```
public export
lookup : Eq key => key -> Vect n (key, val) -> Maybe val
lookup = lookupBy (==)

||| Check if any element of xs is found in elems by a user-provided comparison
||| @ p the comparison operator
||| @ elems the vector to search
||| @ xs what to search for
|||
||| ```idris example
||| hasAnyBy (==) [2,5] [1,2,3,4]
||| ```
public export
hasAnyBy : (p : elem -> elem -> Bool) -> (elems : Vect m elem) -> (xs : Vect len elem) -> Bool
hasAnyBy p elems []      = False
hasAnyBy p elems (x::xs) = elemBy p x elems || hasAnyBy p elems xs

||| Check if any element of xs is found in elems using the default Boolean equality test
|||
||| ```idris example
||| hasAny [2,5] [1,2,3,4]
||| ```
public export
hasAny : Eq elem => Vect m elem -> Vect len elem -> Bool
hasAny = hasAnyBy (==)

--------------------------------------------------------------------------------
-- Searching with a predicate
--------------------------------------------------------------------------------

||| Find the first element of the vector that satisfies some test
||| @ p the test to satisfy
|||
||| ```idris example
||| find (== 3) [1,2,3,4]
||| ```
public export
find : (p : elem -> Bool) -> (xs : Vect len elem) -> Maybe elem
find p []      = Nothing
find p (x::xs) = if p x then Just x else find p xs

||| Find the index of the first element of the vector that satisfies some test
|||
||| ```idris example
||| findIndex (== 3) [1,2,3,4]
||| ```
public export
findIndex : (elem -> Bool) -> Vect len elem -> Maybe (Fin len)
findIndex p []        = Nothing
findIndex p (x :: xs) = if p x then Just FZ else FS <$> findIndex p xs

||| Find the indices of all elements that satisfy some test
|||
||| ```idris example
||| findIndices (< 3) [1,2,3,4]
||| ```
public export
findIndices : (elem -> Bool) -> Vect m elem -> List (Fin m)
findIndices p []        = []
findIndices p (x :: xs)
     = let is = FS <$> findIndices p xs in
           if p x then FZ :: is else is

||| Find the index of the first element of the vector that satisfies some test
|||
||| ```idris example
||| elemIndexBy (==) 3 [1,2,3,4]
||| ```
public export
elemIndexBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> Maybe (Fin m)
elemIndexBy p e = findIndex $ p e

||| Find the index of the first element of the vector equal to the given one.
|||
||| ```idris example
||| elemIndex 3 [1,2,3,4]
||| ```
public export
elemIndex : Eq elem => elem -> Vect m elem -> Maybe (Fin m)
elemIndex = elemIndexBy (==)

||| Find the indices of all elements that satisfy some test
|||
||| ```idris example
||| elemIndicesBy (<=) 3 [1,2,3,4]
||| ```
public export
elemIndicesBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> List (Fin m)
elemIndicesBy p e = findIndices $ p e

||| Find the indices of all elements uquals to the given one
|||
||| ```idris example
||| elemIndices 3 [1,2,3,4,3]
||| ```
public export
elemIndices : Eq elem => elem -> Vect m elem -> List (Fin m)
elemIndices = elemIndicesBy (==)

--------------------------------------------------------------------------------
-- Filters
--------------------------------------------------------------------------------

||| Find all elements of a vector that satisfy some test
|||
||| ```idris example
||| filter (< 3) (fromList [1,2,3,4])
||| ```
public export
filter : (elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
filter p []      = ( _ ** [] )
filter p (x::xs) =
  let (_ ** tail) = filter p xs
   in if p x then
        (_ ** x::tail)
      else
        (_ ** tail)

||| Make the elements of some vector unique by some test
|||
||| ```idris example
||| nubBy (==) (fromList [1,2,2,3,4,4])
||| ```
public export
nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
nubBy = nubBy' []
  where
    nubBy' : forall len . Vect m elem -> (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
    nubBy' acc p []      = (_ ** [])
    nubBy' acc p (x::xs) with (elemBy p x acc)
      nubBy' acc p (x :: xs) | True  = nubBy' acc p xs
      nubBy' acc p (x :: xs) | False with (nubBy' (x::acc) p xs)
        nubBy' acc p (x :: xs) | False | (_ ** tail) = (_ ** x::tail)

||| Make the elements of some vector unique by the default Boolean equality
|||
||| ```idris example
||| nub (fromList [1,2,2,3,4,4])
||| ```
public export
nub : Eq elem => Vect len elem -> (p ** Vect p elem)
nub = nubBy (==)

||| Delete first element from list according to some test
|||
||| ```idris example
||| deleteBy (<) 3 (fromList [1,2,2,3,4,4])
||| ```
public export
deleteBy : {len : _} -> -- needed for the dependent pair
           (elem -> elem -> Bool) -> elem -> Vect len elem -> (p ** Vect p elem)
deleteBy _  _ []      = (_ ** [])
deleteBy eq x (y::ys) =
  let (len ** zs) = deleteBy eq x ys
  in if x `eq` y then (_ ** ys) else (S len ** y ::zs)

||| Delete first element from list equal to the given one
|||
||| ```idris example
||| delete 2 (fromList [1,2,2,3,4,4])
||| ```
public export
delete : {len : _} ->
         Eq elem => elem -> Vect len elem -> (p ** Vect p elem)
delete = deleteBy (==)

--------------------------------------------------------------------------------
-- Splitting and breaking lists
--------------------------------------------------------------------------------

||| A tuple where the first element is a `Vect` of the `n` first elements and
||| the second element is a `Vect` of the remaining elements of the original.
||| It is equivalent to `(take n xs, drop n xs)` (`splitAtTakeDrop`),
||| but is more efficient.
|||
||| @ n   the index to split at
||| @ xs  the `Vect` to split in two
|||
||| ```idris example
||| splitAt 2 (fromList [1,2,3,4])
||| ```
public export
splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem)
splitAt Z xs = ([], xs)
splitAt (S k) (x :: xs) with (splitAt k {m} xs)
  splitAt (S k) (x :: xs) | (tk, dr) = (x :: tk, dr)

||| A tuple where the first element is a `Vect` of the `n` elements passing given test
||| and the second element is a `Vect` of the remaining elements of the original.
|||
||| ```idris example
||| partition (== 2) (fromList [1,2,3,2,4])
||| ```
public export
partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem))
partition p []      = ((_ ** []), (_ ** []))
partition p (x::xs) =
  let ((leftLen ** lefts), (rightLen ** rights)) = partition p xs in
    if p x then
      ((S leftLen ** x::lefts), (rightLen ** rights))
    else
      ((leftLen ** lefts), (S rightLen ** x::rights))

--------------------------------------------------------------------------------
-- Predicates
--------------------------------------------------------------------------------

||| Verify vector prefix
|||
||| ```idris example
||| isPrefixOfBy (==) (fromList [1,2]) (fromList [1,2,3,4])
||| ```
public export
isPrefixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
isPrefixOfBy p [] right        = True
isPrefixOfBy p left []         = False
isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys

||| Verify vector prefix
|||
||| ```idris example
||| isPrefixOf (fromList [1,2]) (fromList [1,2,3,4])
||| ```
public export
isPrefixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
isPrefixOf = isPrefixOfBy (==)

||| Verify vector suffix
|||
||| ```idris example
||| isSuffixOfBy (==) (fromList [3,4]) (fromList [1,2,3,4])
||| ```
public export
isSuffixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)

||| Verify vector suffix
|||
||| ```idris example
||| isSuffixOf (fromList [3,4]) (fromList [1,2,3,4])
||| ```
public export
isSuffixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
isSuffixOf = isSuffixOfBy (==)

--------------------------------------------------------------------------------
-- Conversions
--------------------------------------------------------------------------------

||| Convert Maybe type into Vect
|||
||| ```idris example
||| maybeToVect (Just 2)
||| ```
public export
maybeToVect : Maybe elem -> (p ** Vect p elem)
maybeToVect Nothing  = (_ ** [])
maybeToVect (Just j) = (_ ** [j])

||| Convert first element of Vect (if exists) into Maybe.
|||
||| ```idris example
||| vectToMaybe [2]
||| ```
public export
vectToMaybe : Vect len elem -> Maybe elem
vectToMaybe []      = Nothing
vectToMaybe (x::xs) = Just x

--------------------------------------------------------------------------------
-- Misc
--------------------------------------------------------------------------------

||| Filter out Nothings from Vect and unwrap the Justs
|||
||| ```idris example
||| catMaybes [Just 1, Just 2, Nothing, Nothing, Just 5]
||| ```
public export
catMaybes : (xs : Vect n (Maybe elem)) -> (p ** Vect p elem)
catMaybes []             = (_ ** [])
catMaybes (Nothing::xs)  = catMaybes xs
catMaybes ((Just j)::xs) =
  let (_ ** tail) = catMaybes xs
   in (_ ** j::tail)

||| Get diagonal elements
|||
||| ```idris example
||| diag [[1,2,3], [4,5,6], [7,8,9]]
||| ```
public export
diag : Vect len (Vect len elem) -> Vect len elem
diag []             = []
diag ((x::xs)::xss) = x :: diag (map tail xss)

namespace Fin

  public export
  tabulate : {len : Nat} -> (Fin len -> a) -> Vect len a
  tabulate {len = Z} f = []
  tabulate {len = S _} f = f FZ :: tabulate (f . FS)

  public export
  range : {len : Nat} -> Vect len (Fin len)
  range = tabulate id

namespace Subset

  public export
  tabulate : {len : Nat} -> (Subset Nat (`LT` len) -> a) -> Vect len a
  tabulate {len = Z} f = []
  tabulate {len = S _} f
    = f (Element Z ltZero)
    :: Subset.tabulate (\ (Element n prf) => f (Element (S n) (LTESucc prf)))

  public export
  range : {len : Nat} -> Vect len (Subset Nat (`LT` len))
  range = tabulate id

--------------------------------------------------------------------------------
-- Zippable
--------------------------------------------------------------------------------

public export
Zippable (Vect k) where
  zipWith _ [] [] = []
  zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys

  zipWith3 _ [] [] [] = []
  zipWith3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: zipWith3 f xs ys zs

  unzipWith f [] = ([], [])
  unzipWith f (x :: xs) = let (b, c) = f x
                              (bs, cs) = unzipWith f xs in
                              (b :: bs, c :: cs)

  unzipWith3 f [] = ([], [], [])
  unzipWith3 f (x :: xs) = let (b, c, d) = f x
                               (bs, cs, ds) = unzipWith3 f xs in
                               (b :: bs, c :: cs, d :: ds)

export
zipWithIndexLinear : (0 f : _) -> (xs, ys : Vect n a) -> (i : Fin n) -> index i (zipWith f xs ys) = f (index i xs) (index i ys)
zipWithIndexLinear _ (_::xs) (_::ys) FZ     = Refl
zipWithIndexLinear f (_::xs) (_::ys) (FS i) = zipWithIndexLinear f xs ys i

export
zipWith3IndexLinear : (0 f : _) -> (xs, ys, zs : Vect n a) -> (i : Fin n) -> index i (zipWith3 f xs ys zs) = f (index i xs) (index i ys) (index i zs)
zipWith3IndexLinear _ (_::xs) (_::ys) (_::zs) FZ     = Refl
zipWith3IndexLinear f (_::xs) (_::ys) (_::zs) (FS i) = zipWith3IndexLinear f xs ys zs i

--------------------------------------------------------------------------------
-- Matrix transposition
--------------------------------------------------------------------------------
||| Transpose a `Vect` of `Vect`s, turning rows into columns and vice versa.
|||
||| This is like zipping all the inner `Vect`s together and is equivalent to `traverse id` (`transposeTraverse`).
|||
||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
|||
||| ```idris example
||| transpose [[1,2], [3,4], [5,6], [7,8]]
||| ```
public export
transpose : {n : _} -> (array : Vect m (Vect n elem)) -> Vect n (Vect m elem)
transpose []        = replicate _ []                 -- = [| [] |]
transpose (x :: xs) = zipWith (::) x (transpose xs) -- = [| x :: xs |]

--------------------------------------------------------------------------------
-- Applicative/Monad/Traversable
--------------------------------------------------------------------------------
-- These only work if the length is known at run time!

public export
implementation {k : Nat} -> Applicative (Vect k) where
    pure = replicate _
    fs <*> vs = zipWith apply fs vs

-- ||| This monad is different from the List monad, (>>=)
-- ||| uses the diagonal.
public export
implementation {k : Nat} -> Monad (Vect k) where
    m >>= f = diag (map f m)

public export
implementation Traversable (Vect k) where
    traverse f []        = pure []
    traverse f (x :: xs) = [| f x :: traverse f xs |]

--------------------------------------------------------------------------------
-- Semigroup/Monoid
--------------------------------------------------------------------------------

public export
Semigroup a => Semigroup (Vect k a) where
  (<+>) = zipWith (<+>)

public export
{k : Nat} -> Monoid a => Monoid (Vect k a) where
  neutral = replicate k neutral

--------------------------------------------------------------------------------
-- Show
--------------------------------------------------------------------------------

export
implementation Show elem => Show (Vect len elem) where
    show = show . toList

-- Some convenience functions for testing lengths

-- Needs to be Maybe rather than Dec, because if 'n' is unequal to m, we
-- only know we don't know how to make a Vect n a, not that one can't exist.
export
exactLength : {m : Nat} -> -- expected at run-time
              (len : Nat) -> (xs : Vect m a) -> Maybe (Vect len a)
exactLength {m} len xs with (decEq m len)
  exactLength {m = m} m xs | (Yes Refl) = Just xs
  exactLength {m = m} len xs | (No contra) = Nothing

||| If the given Vect is at least the required length, return a Vect with
||| at least that length in its type, otherwise return Nothing
||| @len the required length
||| @xs the vector with the desired length
export
overLength : {m : Nat} -> -- expected at run-time
             (len : Nat) -> (xs : Vect m a) -> Maybe (p ** Vect (plus p len) a)
overLength n xs with (cmp m n)
  overLength {m}   (plus m (S y)) xs | (CmpLT y) = Nothing
  overLength {m}                m xs | CmpEQ     = Just (0 ** xs)
  overLength {m = plus n (S x)} n xs | (CmpGT x)
         = Just (S x ** rewrite plusCommutative (S x) n in xs)


text:
module Replica.Core

import public Replica.Core.Types
import public Replica.Core.Parse

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica


text:
||| Here we present the syntax for our global types.
||| Global Types present a top-level view of the protocol.
|||
||| We are inspired from the Tech Report 'A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming' (DTRS12-2).
||| The author's note that sending and receiving are special cases of choice.
|||
|||
module Sessions.Global

import Decidable.Equality
import Data.List
import Data.List.Elem

import Data.List1

import Sessions.Meta

%default total

public export
data Global : (role, label, msg : Type)
           -> (rvars : List Ty)
           -> (type  : Ty)
                   -> Type
  where
    End : Global typeR typeL typeM rs G

    Call : Elem R rs -> Global typeR typeL typeM rs R

    Rec : Global typeR typeL typeM (R::rs) R
       -> Global typeR typeL typeM     rs  R

    Choice : (sender, receiver : typeR)
          -> (prf              : Not (sender = receiver))
          -> (choices          : List1 (typeL, typeM, Global typeR typeL typeM rs g))
                              -> Global typeR typeL typeM rs g

public export
Branch : (role, label, msg : Type)
      -> (rvars : List Ty)
      -> (type  : Ty)
               -> Type
Branch role label msg rvars type
  = (label, msg, Global role label msg rvars type)

public export
Branches : (role, label, msg : Type)
        -> (rvars : List Ty)
        -> (type  : Ty)
                 -> Type
Branches role label msg rvars type
  = List1 (Branch role label msg rvars type)

public export
Branches' : (role, label, msg : Type)
         -> (rvars : List Ty)
         -> (type  : Ty)
                  -> Type
Branches' role label msg rvars type
  = List (Branch role label msg rvars type)

-- [ EOF ]

max_stars_repo_name: DSbD-AppControl/sessions-playground

max_issues_repo_name: DSbD-AppControl/sessions-playground

max_forks_repo_name: DSbD-AppControl/sessions-playground


text:
foo : String
foo = """"""


text:
module Sub08Apply108x63

import ProofColDivSeqBase
import ProofColDivSeqPostulate
import ProofColDivSeqPostuProof

%default total
-- %language ElabReflection

-- 3(36x+21) --F[5,-2]->B[1,-2]--> 3(16x+9)
export
apply108x63 : (Not . P) (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                                    (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                              (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))))))
  -> (m : Nat **
        (LTE (S m)
             (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                        (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                  (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))))))),
         (Not . P) m))
apply108x63 {o} col = ((S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))))))))))
                                                           ** (lte108x63 o, fb108x63To48x27 o col)) where
  lte108x63 : (o:Nat) -> LTE (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))
                                              (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))))))))))))
          (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                           (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                     (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                               (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))))))
  lte108x63 Z = (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc) LTEZero
  lte108x63 (S o) = let lemma = lte108x63 o in
    rewrite (sym (plusSuccRightSucc o o)) in
    rewrite (sym (plusSuccRightSucc (plus o o)  (S (plus o o)))) in
    rewrite (sym (plusSuccRightSucc (plus o o)  (plus o o))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) (plus o o))  (S (S (S (plus (plus o o) (plus o o))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) (plus o o))  (S (S (plus (plus o o) (plus o o)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) (plus o o))  (S (plus (plus o o) (plus o o))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) (plus o o))  (plus (plus o o) (plus o o)))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (S (S (S (S (S (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (S (S (S (S (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (S (S (S (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (S (S (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (S (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o)))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o))))) in

    rewrite (sym (plusSuccRightSucc (plus o o)  o)) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) o)  (S (S (S (plus (plus o o) o)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) o)  (S (S (plus (plus o o) o))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) o)  (S (plus (plus o o) o)))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (S (plus (plus o o) o)))  (S (S (S (S (S (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (S (plus (plus o o) o)))  (S (S (S (S (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (S (plus (plus o o) o)))  (S (S (S (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (S (plus (plus o o) o)))  (S (S (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (S (plus (plus o o) o)))  (S (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (S (plus (plus o o) o)))  (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o))))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                    (S (S (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                    (S (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                    (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                    (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                      (S (plus (plus o o) o)))
                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                          (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                      (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                                                                o))))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                      (S (plus (plus o o) o)))
                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                          (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                      (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                                                                o)))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                      (S (plus (plus o o) o)))
                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                          (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                      (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                                                                o))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                      (S (plus (plus o o) o)))
                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                          (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                      (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                    (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                                                                o)))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                      (S (plus (plus o o) o)))
                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                          (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                      (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                    (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                                                                o))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                      (S (plus (plus o o) o)))
                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                          (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                      (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                    (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                                                                o)))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                      (S (plus (plus o o) o)))
                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                          (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                      (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                    (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                                                                o))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                      (S (plus (plus o o) o)))
                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                          (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                      (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                    (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                                                                o)))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                      (S (plus (plus o o) o)))
                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                          (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                      (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                    (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                                                                o))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                      (S (plus (plus o o) o)))
                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                          (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                      (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                    (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                                                                o)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                      (S (plus (plus o o) o)))
                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                          (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                      (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                    (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                                                                o))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                      (S (plus (plus o o) o)))
                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                          (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                      (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                    (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                                                                o)))))))))) in
      (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc) lemma


text:
-- Like SimpleRealizedFunction but uses data instead of record

module SimpleDataRealizedFunction
%default total

public export
data SimpleDataRealizedFunction : (t : Type) -> (cost : Integer) -> (quality : Double)
                                  -> Type where
  MkSimpleDataRealizedFunction : (f : t) -> (cost : Integer) -> (quality : Double)
                                 -> SimpleDataRealizedFunction t cost quality

-- Perform the composition between 2 simple realized functions.  The
-- resulting realized function is formed as follows:
--
-- 1. Composed lifted functions
-- 2. Costs are added
-- 3. Composed quality is the min of the component qualities
public export
compose : {a : Type} -> {b : Type} -> {c : Type} ->
          (SimpleDataRealizedFunction (b -> c) g_cost g_q) ->
          (SimpleDataRealizedFunction (a -> b) f_cost f_q) ->
          (SimpleDataRealizedFunction (a -> c) (f_cost + g_cost) (min f_q g_q))
compose (MkSimpleDataRealizedFunction f f_cost f_q) (MkSimpleDataRealizedFunction g g_cost g_q) =
         MkSimpleDataRealizedFunction (f . g) (g_cost + f_cost) (min g_q f_q)

-- Perform function application over realized functions.  Maybe we'd
-- want to used some funded data, as defined in FndType.
public export
apply : (SimpleDataRealizedFunction (a -> b) cost quality) -> a -> b
apply (MkSimpleDataRealizedFunction f cost quality) = f

max_stars_repo_name: sroberti/ai-dsl

max_issues_repo_name: sroberti/ai-dsl

max_forks_repo_name: sroberti/ai-dsl


text:
{-
[1, 42, 51]
True
False
-}
module Main

data T a = L | B a (T a) (T a)

toList : T a -> List a
toList L = []
toList (B a l r) = Main.toList l ++ [a] ++ Main.toList r

contains : Ord a => T a -> a -> Bool
contains L _ = False
contains (B a l r) x =
  case (compare x a) of
    EQ => True
    LT => contains l x
    GT => contains r x

main : IO ()
main = do printLn $ Main.toList tree
          printLn $ contains tree 1
          printLn $ contains tree 52
  where tree : T Nat
        tree = (B 42 (B 1 L L) (B 51 L L))

max_stars_repo_name: timjs/iris-clean

max_issues_repo_name: timjs/iris-clean

max_forks_repo_name: timjs/iris-clean


text:
module Control.Comonad.Store.Store

import Control.Comonad
import Control.Comonad.Trans
import Control.Monad.Identity

%default total

public export
record StoreT (s : Type) (w : Type -> Type) (a : Type) where
  constructor MkStoreT
  run : w (s -> a)
  val : s

public export
Store : (s : Type) -> (a : Type) -> Type
Store s = StoreT s Identity

||| Create a Store using an accessor function and a stored value
public export
store : (s -> a) -> s -> Store s a
store f s = MkStoreT (Id f) s

public export
runStore : Store s a -> (s -> a, s)
runStore (MkStoreT (Id f) s) = (f, s)

public export
runStoreT : StoreT s w a -> (w (s -> a), s)
runStoreT (MkStoreT wf s) = (wf, s)

--------------------------------------------------------------------------------
--          Interface Implementations
--------------------------------------------------------------------------------

public export
Functor w => Functor (StoreT s w) where
  map f = record { run $= map (f .) }

appEnv : (s -> a -> b) -> (s -> a) -> s -> b
appEnv ff fa s = ff s (fa s)

public export
(Monoid s, Applicative w) => Applicative (StoreT s w) where
  pure a = MkStoreT (pure $ const a) neutral
  MkStoreT f m <*> MkStoreT a n = MkStoreT [| appEnv f a |]  (m <+> n)

public export
Comonad w => Comonad (StoreT s w) where
  extract (MkStoreT wf s)   = extract wf s
  duplicate (MkStoreT wf s) = MkStoreT (extend MkStoreT wf) s
  extend f (MkStoreT wf s)  =
    MkStoreT (extend (\wf',s' => f (MkStoreT wf' s')) wf) s

public export
ComonadTrans (StoreT s) where
  lower (MkStoreT f s) = map ($ s) f

public export
(ComonadApply w, Semigroup s) => ComonadApply (StoreT s w) where
  MkStoreT f m <@> MkStoreT a n = MkStoreT (map appEnv f <@> a) (m <+> n)


text:
module Lib
import Prelude.Doubles as db

export
stopwords : List String
stopwords = ["the", "a", "and", "is", "be", "will", "is"]

export
nums : String
nums = "0123456789!@#$%^&*()_+=-:;"

export
removeStopWords : String -> List String
removeStopWords line = do
              let tmp = words line
              foldr (\x, acc => if elem x stopwords then acc else x::acc ) [] tmp

export
makeWordPairs : List String -> List (String, String)
makeWordPairs [] = []
makeWordPairs (x::y::z::h::xs) = (x,y)::(x,z)::(y,z)::(y,h)::(z,x)::(z,y)::(z,h)::(h,x)::(h,y)::(h,z)::makeWordPairs xs
makeWordPairs (x::y::z::xs) = (x,y)::(x,z)::(y,z)::(z,x)::(z,y)::makeWordPairs xs
makeWordPairs (x::y::xs) = (x,y)::makeWordPairs xs

export
createDictionary : List String ->  List (String, Nat)
createDictionary xss = func 0 tmp
              where
                tmp = sort . nub $ xss
                func : Nat -> List String -> List (String, Nat)
                func _ [] = []
                func Z (x::xs) = (x, S Z) :: func (S (S Z)) xs
                func (S k) (x::xs) = (x, S k) :: func (S (S k) ) xs

export
insertAt : List Double -> Double -> Nat -> List Double
insertAt [] elem pos = []
insertAt (x::xs) elem  Z = elem::x::xs
insertAt (x::xs) elem (S Z) = x::elem::xs
insertAt (x::xs) elem (S k) = x::insertAt xs elem k

export
oneHotEncoder : List Nat -> List Double -> List (List Double)
oneHotEncoder ws zs = foldr(\x, acc => (insertAt zs 1.0 x)::acc) [] ws

export
matrix_gen : Num j =>  List j -> List j -> List (List j )
matrix_gen ws zs = foldr (\x, acc => zs::acc) [] ws

b : Double
b = 0.3

export
softmax_activation : List Double -> List Double
softmax_activation xs = let softmax_denom = sum $ map exp $ xs
in foldr (\x,acc => (exp x)/softmax_denom::acc) [] xs

export
nn_Layer : List Double -> List Double -> List Double
nn_Layer [] _ = []
nn_Layer _ [] = []
nn_Layer [] [] = []
nn_Layer (x::xs) (y::ys) = (x * y + b)::nn_Layer xs ys

export
grad_CrossEntropy : List Double -> List Double -> List Double
grad_CrossEntropy [] _ = []
grad_CrossEntropy _ [] = []
grad_CrossEntropy [] [] = []
grad_CrossEntropy (x::xs) (y::ys) = -(y/x) + (1-y)/(1-x)::grad_CrossEntropy xs ys

export
adam_Optimizer : List Double -> List Double -> Double -> Double -> Double -> Double -> Double -> Double -> List Double
adam_Optimizer [] _ _ _ _ _ _ _ =  []
adam_Optimizer _ [] _ _ _ _ _ _ =  []
adam_Optimizer (t::thetas) (gt::gts) alpha m_prev v_prev beta1 beta2 epsilon = do
              let m_current = (beta1 * m_prev + (1-beta1) * gt)/ (1-beta1)
              let v_current = (beta2 * v_prev + (1-beta2) *  (db.pow gt 2))/(1-(db.pow beta2 2))
              let mhat_current = m_current /(1-beta1)
              let vhat_current = v_current/(1-beta2)
              (t - alpha * mhat_current / ((sqrt  vhat_current) + epsilon)):: adam_Optimizer thetas gts alpha m_current v_current beta1 beta2 epsilon

export
wordpairs : List String -> List (String,String)
wordpairs wrds = makeWordPairs wrds

export
xss : List (String, String) -> List String
xss wordpairs = map (\(a,b) => a ) wordpairs

export
yss : List (String,String) -> List String
yss wordpairs = map (\(a,b) => b ) wordpairs

export
wordify : List String -> List String
wordify [] = []
wordify (fst::xss) =
            let bn = words fst
            in bn ++ wordify xss

export
rawToDict : List String -> List (String,Nat)
rawToDict [] = []
rawToDict dataset = let some_var = wordify dataset
                    in createDictionary some_var

export
rawToCleaned : List String -> List String
rawToCleaned [] = []
rawToCleaned (x::xs) = let some_var = removeStopWords x
                       in some_var ++ rawToCleaned xs
export
fullNNLayer : List (List Double) -> List (List Double) -> List (List Double)
fullNNLayer [] [] = []
fullNNLayer (x::inputs) (y::weights) = (softmax_activation $ nn_Layer x y)::fullNNLayer inputs weights

export
loss_func : (List Double -> List Double -> List Double ) -> List (List Double) -> List (List Double) -> List (List Double)
loss_func f [] _ = []
loss_func f _ [] = []
loss_func f [] [] = []
loss_func f (p::preds) (t::targets) = f p t :: loss_func f preds targets

export
optimizer : ( List Double -> List Double -> Double -> Double -> Double -> Double -> Double -> Double -> List Double) -> List (List Double) -> List (List Double) -> Double -> Double -> Double -> Double -> Double -> Double -> List (List Double)
optimizer f [] _ _ _ _ _ _ _ = []
optimizer f _ [] _ _ _ _ _ _ = []
optimizer f [] [] _ _ _ _ _ _= []
optimizer f (ws::wss) (cs::costs) alpha  m v beta1 beta2 epsilon =  (f ws cs alpha m v beta1 beta2 epsilon) :: optimizer f wss costs alpha m  v beta1 beta2 epsilon

export
model : List (List Double) -> List (List Double) -> List (List Double) -> Double -> Double -> Double -> Double -> Int -> List (List Double )
model [] _ _ _ _ _ _ _ = []
model _ [] _ _ _ _ _ _ = []
model _ _ [] _ _ _ _ _ = []
model [] [] [] _ _ _ _ _= []
model weights inputs targets alpha beta1 beta2 epsilon iterations = case iterations == 0 of
                                              True => weights
                                              False => do
                                                  let predicted = fullNNLayer inputs weights
                                                  let full_cost = loss_func grad_CrossEntropy predicted targets
                                                  let new_weights = optimizer adam_Optimizer weights full_cost alpha 0.0 0.0 beta1 beta2 epsilon
                                                  model new_weights inputs targets alpha beta1 beta2 epsilon (iterations - 1)


text:
module System.File

import public Data.Fuel

import Data.List
import Data.Strings
import System.Info
import System.FFI

%default total

public export
data Mode = Read | WriteTruncate | Append | ReadWrite | ReadWriteTruncate | ReadAppend

public export
FilePtr : Type
FilePtr = AnyPtr

support : String -> String
support fn = "C:" ++ fn ++ ", libidris2_support, idris_file.h"

fileClass : String
fileClass = "io/github/mmhelloworld/idrisjvm/runtime/ChannelIo"

%foreign support "idris2_openFile"
         "node:support:openFile,support_system_file"
         jvm' fileClass "open" "String String" fileClass
prim__open : String -> String -> PrimIO FilePtr

%foreign support "idris2_closeFile"
         "node:lambda:(fp) => require('fs').closeSync(fp.fd)"
         jvm' fileClass "close" fileClass "void"
prim__close : FilePtr -> PrimIO ()

%foreign support "idris2_fileError"
         "node:lambda:x=>(x===1n?BigInt(1):BigInt(0))"
         jvm' fileClass "getErrorNumber" fileClass "int"
prim__error : FilePtr -> PrimIO Int

%foreign support "idris2_fileErrno"
         "node:support:fileErrno,support_system_file"
         jvm' runtimeClass "getErrorNumber" "java/lang/Object" "int"
prim__fileErrno : PrimIO Int

%foreign support "idris2_seekLine"
         "node:support:seekLine,support_system_file"
         jvm' fileClass ".seekLine" fileClass "int"
prim__seekLine : FilePtr -> PrimIO Int

%foreign support "idris2_readLine"
         "node:support:readLine,support_system_file"
         jvm' fileClass "readLine" fileClass "String"
prim__readLine : FilePtr -> PrimIO (Ptr String)

%foreign support "idris2_readChars"
         jvm' fileClass "readChars" ("int " ++ fileClass) "String"
prim__readChars : Int -> FilePtr -> PrimIO (Ptr String)
%foreign "C:fgetc,libc 6"
         jvm' fileClass "readChar" fileClass "char"
prim__readChar : FilePtr -> PrimIO Int

%foreign support "idris2_writeLine"
         "node:lambda:(filePtr, line) => require('fs').writeSync(filePtr.fd, line, undefined, 'utf-8')"
         jvm' fileClass "writeLine" (fileClass ++ " String") "int"
prim__writeLine : FilePtr -> String -> PrimIO Int

%foreign support "idris2_eof"
         "node:lambda:x=>(x.eof?1n:0n)"
         jvm' fileClass "isEof" fileClass "int"
prim__eof : FilePtr -> PrimIO Int

%foreign "C:fflush,libc 6"
         jvm' fileClass "flush" fileClass "int"
prim__flush : FilePtr -> PrimIO Int
%foreign support "idris2_popen"
         jvm' fileClass "popen" "String String" fileClass
prim__popen : String -> String -> PrimIO FilePtr
%foreign support "idris2_pclose"
         jvm' fileClass "close" fileClass "void"
prim__pclose : FilePtr -> PrimIO ()

%foreign support "idris2_removeFile"
         jvm' fileClass "delete" "String" "int"
prim__removeFile : String -> PrimIO Int

%foreign support "idris2_fileSize"
         "node:lambda:fp=>require('fs').fstatSync(fp.fd, {bigint: true}).size"
         jvm' fileClass "size" fileClass "int"
prim__fileSize : FilePtr -> PrimIO Int

%foreign support "idris2_fileSize"
         jvm' fileClass "size" fileClass "int"
prim__fPoll : FilePtr -> PrimIO Int

%foreign support "idris2_fileAccessTime"
         jvm' fileClass "getAccessTime" fileClass "int"
prim__fileAccessTime : FilePtr -> PrimIO Int

%foreign support "idris2_fileModifiedTime"
         "node:lambda:fp=>require('fs').fstatSync(fp.fd, {bigint: true}).mtimeMs / 1000n"
         jvm' fileClass "getModifiedTime" fileClass "int"
prim__fileModifiedTime : FilePtr -> PrimIO Int

%foreign support "idris2_fileStatusTime"
         jvm' fileClass "getStatusTime" fileClass "int"
prim__fileStatusTime : FilePtr -> PrimIO Int

%foreign support "idris2_stdin"
         "node:lambda:x=>({fd:0, buffer: Buffer.alloc(0), name:'<stdin>', eof: false})"
         jvm runtimeClass "getStdin"
prim__stdin : FilePtr

%foreign support "idris2_stdout"
         "node:lambda:x=>({fd:1, buffer: Buffer.alloc(0), name:'<stdout>', eof: false})"
         jvm runtimeClass "getStdout"
prim__stdout : FilePtr

%foreign support "idris2_stderr"
         "node:lambda:x=>({fd:2, buffer: Buffer.alloc(0), name:'<stderr>', eof: false})"
         jvm runtimeClass "getStderr"
prim__stderr : FilePtr

%foreign "C:chmod, libc 6, sys/stat.h"
         "node:support:chmod,support_system_file"
         jvm' fileClass "chmod" "String int" "int"
prim__chmod : String -> Int -> PrimIO Int

modeStr : Mode -> String
modeStr Read              = if isWindows then "rb" else "r"
modeStr WriteTruncate     = if isWindows then "wb" else "w"
modeStr Append            = if isWindows then "ab" else "a"
modeStr ReadWrite         = if isWindows then "rb+" else "r+"
modeStr ReadWriteTruncate = if isWindows then "wb+" else "w+"
modeStr ReadAppend        = if isWindows then "ab+" else "a+"

public export
data FileError = GenericFileError Int -- errno
               | FileReadError
               | FileWriteError
               | FileNotFound
               | PermissionDenied
               | FileExists

returnError : HasIO io => io (Either FileError a)
returnError
    = do err <- primIO prim__fileErrno
         pure $ Left $
           case err of
              0 => FileReadError
              1 => FileWriteError
              2 => FileNotFound
              3 => PermissionDenied
              4 => FileExists
              _ => GenericFileError (err-5)

export
Show FileError where
  show (GenericFileError errno) = "File error: " ++ show errno
  show FileReadError = "File Read Error"
  show FileWriteError = "File Write Error"
  show FileNotFound = "File Not Found"
  show PermissionDenied = "Permission Denied"
  show FileExists = "File Exists"

ok : HasIO io => a -> io (Either FileError a)
ok x = pure (Right x)

public export
data File : Type where
     FHandle : FilePtr -> File

export
stdin : File
stdin = FHandle prim__stdin

export
stdout : File
stdout = FHandle prim__stdout

export
stderr : File
stderr = FHandle prim__stderr

export
openFile : HasIO io => String -> Mode -> io (Either FileError File)
openFile f m
    = do res <- primIO (prim__open f (modeStr m))
         if prim__nullAnyPtr res /= 0
            then returnError
            else ok (FHandle res)

export
closeFile : HasIO io => File -> io ()
closeFile (FHandle f) = primIO (prim__close f)

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

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

export
fileError : HasIO io => File -> io Bool
fileError (FHandle f)
    = do x <- primIO $ prim__error f
         pure (x /= 0)

||| Seek through the next newline.
||| This is @fGetLine@ without the overhead of copying
||| any characters.
export
fSeekLine : HasIO io => (h : File) -> io (Either FileError ())
fSeekLine (FHandle f)
    = do res <- primIO (prim__seekLine f)
         if res /= 0
            then returnError
            else ok ()

export
fGetLine : HasIO io => (h : File) -> io (Either FileError String)
fGetLine (FHandle f)
    = do res <- primIO (prim__readLine f)
         if prim__nullPtr res /= 0
            then returnError
            else ok (prim__getString res)

export
fGetChars : HasIO io => (h : File) -> Int -> io (Either FileError String)
fGetChars (FHandle f) max
    = do res <- primIO (prim__readChars max f)
         if prim__nullPtr res /= 0
            then returnError
            else ok (prim__getString res)

export
fGetChar : HasIO io => (h : File) -> io (Either FileError Char)
fGetChar (FHandle h)
    = do c <- primIO (prim__readChar h)
         ferr <- primIO (prim__error h)
         if (ferr /= 0)
            then returnError
            else ok (cast c)

export
fPutStr : HasIO io => (h : File) -> String -> io (Either FileError ())
fPutStr (FHandle f) str
    = do res <- primIO (prim__writeLine f str)
         if res == 0
            then returnError
            else ok ()

export
fPutStrLn : HasIO io => (h : File) -> String -> io (Either FileError ())
fPutStrLn f str = fPutStr f (str ++ "\n")

export
fEOF : HasIO io => (h : File) -> io Bool
fEOF (FHandle f)
    = do res <- primIO (prim__eof f)
         pure (res /= 0)

export
fflush : HasIO io => (h : File) -> io ()
fflush (FHandle f)
    = ignore $ primIO (prim__flush f)

export
popen : HasIO io => String -> Mode -> io (Either FileError File)
popen f m = do
    ptr <- primIO (prim__popen f (modeStr m))
    if prim__nullAnyPtr ptr /= 0
        then returnError
        else pure (Right (FHandle ptr))

export
pclose : HasIO io => File -> io ()
pclose (FHandle h) = primIO (prim__pclose h)

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

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

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

export
removeFile : HasIO io => String -> io (Either FileError ())
removeFile fname
    = do res <- primIO (prim__removeFile fname)
         if res == 0
            then ok ()
            else returnError

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

export
fPoll : HasIO io => File -> io Bool
fPoll (FHandle f)
    = do p <- primIO (prim__fPoll f)
         pure (p > 0)

||| Perform a given operation on successful file open
||| and ensure the file is closed afterwards or perform
||| a different operation if the file fails to open.
export
withFile : HasIO io => (filename : String) ->
                       Mode ->
                       (onError : FileError -> io a) ->
                       (onOpen  : File -> io (Either a b)) ->
                       io (Either a b)
withFile filename mode onError onOpen =
  do Right h <- openFile filename mode
       | Left err => Left <$> onError err
     res <- onOpen h
     closeFile h
     pure res

readLinesOnto : HasIO io => (acc : List String) ->
                            (offset : Nat) ->
                            (fuel : Fuel) ->
                            File ->
                            io (Either FileError (Bool, List String))
readLinesOnto acc _ Dry h = pure (Right (False, reverse acc))
readLinesOnto acc offset (More fuel) h
  = do False <- fEOF h
         | True => pure $ Right (True, reverse acc)
       case offset of
            (S offset') => (fSeekLine h *> readLinesOnto acc offset' (More fuel) h) @{Applicative.Compose}
            0           => (fGetLine h >>= \str => readLinesOnto (str :: acc) 0 fuel h) @{Monad.Compose}

||| Read a chunk of a file in a line-delimited fashion.
||| You can use this function to read an entire file
||| as with @readFile@ by reading until @forever@ or by
||| iterating through pages until hitting the end of
||| the file.
|||
||| The @limit@ function can provide you with enough
||| fuel to read exactly a given number of lines.
|||
||| On success, returns a tuple of whether the end of
||| the file was reached or not and the lines read in
||| from the file.
|||
||| Note that each line will still have a newline
||| character at the end.
|||
||| Important: because we are chunking by lines, this
||| function's totality depends on the assumption that
||| no single line in the input file is infinite.
export
readFilePage : HasIO io => (offset : Nat) -> (until : Fuel) -> String -> io (Either FileError (Bool, List String))
readFilePage offset fuel file
  = withFile file Read pure $
      readLinesOnto [] offset fuel

export
partial
readFile : HasIO io => String -> io (Either FileError String)
readFile = (map $ map (fastConcat . snd)) . readFilePage 0 forever

||| Write a string to a file
export
writeFile : HasIO io =>
            (filepath : String) -> (contents : String) ->
            io (Either FileError ())
writeFile file contents
  = withFile file WriteTruncate pure $
      (flip fPutStr contents)

namespace FileMode
  public export
  data FileMode = Read | Write | Execute

public export
record Permissions where
  constructor MkPermissions
  user   : List FileMode
  group  : List FileMode
  others : List FileMode

mkMode : Permissions -> Int
mkMode p
    = getMs (user p) * 64 + getMs (group p) * 8 + getMs (others p)
  where
    getM : FileMode -> Int
    getM Read = 4
    getM Write = 2
    getM Execute = 1

    getMs : List FileMode -> Int
    getMs = sum . map getM

export
chmodRaw : HasIO io => String -> Int -> io (Either FileError ())
chmodRaw fname p
    = do ok <- primIO $ prim__chmod fname p
         if ok == 0
            then pure (Right ())
            else returnError

export
chmod : HasIO io => String -> Permissions -> io (Either FileError ())
chmod fname p = chmodRaw fname (mkMode p)

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
module Eternity2SMT

import Data.String
import Data.Vect
import src.SMTLib
import src.Tensor
import src.GridOps

Dim : Nat
Dim = 4

E : Nat
E = 4

BitSize : Nat
BitSize = 8

ColorBitSize : Nat
ColorBitSize = 5

record Piece where
 constructor MkPiece
 up : Char
 right : Char
 down : Char
 left : Char

record PieceColors (size : Nat) where
 constructor MkPieceColors
 upVar : Expr (BitVecT size)
 rightVar : Expr (BitVecT size)
 downVar : Expr (BitVecT size)
 leftVar : Expr (BitVecT size)

puzzle : Vect (Dim * Dim) (Vect E Char)
puzzle = [ ['Y', 'X', 'X', 'B'], ['Y', 'B', 'X', 'X'], ['X', 'B', 'B', 'X'], ['X', 'Y', 'Y', 'X'],
           ['U', 'U', 'U', 'P'], ['P', 'U', 'P', 'P'], ['U', 'U', 'P', 'P'], ['U', 'U', 'P', 'P'],
           ['Y', 'X', 'Y', 'P'], ['B', 'X', 'B', 'P'], ['Y', 'X', 'B', 'P'], ['B', 'X', 'Y', 'P'],
           ['Y', 'X', 'Y', 'U'], ['B', 'X', 'B', 'U'], ['B', 'X', 'Y', 'U'], ['Y', 'X', 'B', 'U'] ]

data Lookup : (a : Type) -> Fin n -> Fin m -> Vect n (Vect m a) -> Type where
 FF : a -> a -> Lookup a n m xs
 LL : a -> a -> Lookup a n m xs
 FL : a -> a -> Lookup a n m xs
 LF : a -> a -> Lookup a n m xs
 FM : a -> a -> a -> Lookup a n m xs
 LM : a -> a -> a -> Lookup a n m xs
 MF : a -> a -> a -> Lookup a n m xs
 ML : a -> a -> a -> Lookup a n m xs
 M : a -> a -> a -> a -> Lookup a n m xs

toLookup : (fn : Fin n) -> (fm : Fin m) -> a -> (xs : Vect n (Vect m a)) -> Lookup a fn fm xs
toLookup i j x xs with (toPos i, toPos j)
 toLookup i j x xs | (First, First) = FF (lookup i j [Left] x xs) (lookup i j [Up] x xs)
 toLookup i j x xs | (Last, Last) = LL (lookup i j [Down] x xs) (lookup i j [Right] x xs)
 toLookup i j x xs | (First, Last) = FL (lookup i j [Up] x xs) (lookup i j [Right] x xs)
 toLookup i j x xs | (Last, First) = LF (lookup i j [Down] x xs) (lookup i j [Left] x xs)
 toLookup i j x xs | (First, _) = FM (lookup i j [Left] x xs) (lookup i j [Up] x xs) (lookup i j [Right] x xs)
 toLookup i j x xs | (Last, _) = LM (lookup i j [Down] x xs) (lookup i j [Left] x xs) (lookup i j [Right] x xs)
 toLookup i j x xs | (_, First) = MF (lookup i j [Down] x xs) (lookup i j [Left] x xs) (lookup i j [Up] x xs)
 toLookup i j x xs | (_, Last) = ML (lookup i j [Down] x xs) (lookup i j [Up] x xs) (lookup i j [Right] x xs)
 toLookup i j x xs | (_, _) = M (lookup i j [Down] x xs) (lookup i j [Left] x xs) (lookup i j [Up] x xs) (lookup i j [Right] x xs)

colorInt : Char -> Int
colorInt c = cast c - cast 'A'

intColor : Int -> Char
intColor i = cast $ cast 'A' + i

rotate : Vect n a -> Vect n a
rotate {n = Z} [] = []
rotate {n = (S n)} (x :: xs) = let rs = xs ++ [x] in
                               replace {P = (\x => Vect x a)} (plusCommutative n 1) rs

rotations : Vect E Char -> Vect E Piece
rotations p = let p' = rotate p in
              let p'' = rotate p' in
              let p''' = rotate p'' in
              let f = \p => MkPiece (index 0 p) (index 1 p) (index 2 p) (index 3 p) in
              [ f p, f p', f p'', f p''' ]

pieces : Vect (Dim * Dim) (Int, Vect E Piece)
pieces = tabulate (\i => (finToInt i, rotations $ index i puzzle))

varPieces : Tensor [Dim, Dim] String
varPieces = toTensor $ tabulate (\i => tabulate (\j => "x_" ++ show (finToNat i) ++ "_" ++ show (finToNat j)))

varColorPieces : Tensor [Dim, Dim, E] String
varColorPieces = toTensor $ tabulate (\i => tabulate (\j => ["cx_" ++ show (finToNat i) ++ "_" ++ show (finToNat j) ++ "_Up",
                                                             "cx_" ++ show (finToNat i) ++ "_" ++ show (finToNat j) ++ "_Right",
                                                             "cx_" ++ show (finToNat i) ++ "_" ++ show (finToNat j) ++ "_Down",
                                                             "cx_" ++ show (finToNat i) ++ "_" ++ show (finToNat j) ++ "_Left"]))

mapColorPieces : Vect Dim (Vect Dim (Vect E (Expr (BitVecT ColorBitSize)))) -> Vect Dim (Vect Dim (PieceColors ColorBitSize))
mapColorPieces vs = tabulate (\i => tabulate (\j => MkPieceColors (index 0 $ index j $ index i vs) (index 1 $ index j $ index i vs)
                                                                  (index 2 $ index j $ index i vs) (index 3 $ index j $ index i vs)))

equalColors : Piece -> PieceColors ColorBitSize -> Expr BoolT
equalColors p pc = and [bv (colorInt $ up p) ColorBitSize == upVar pc,
                        bv (colorInt $ right p) ColorBitSize == rightVar pc,
                        bv (colorInt $ down p) ColorBitSize == downVar pc,
                        bv (colorInt $ left p) ColorBitSize == leftVar pc]

validPieces : Vect Dim (Vect Dim (Expr (BitVecT BitSize))) -> Expr BoolT
validPieces varPieces = and $ concat $ tabulate (\i => tabulate (\j => bvuge (index i j varPieces) (bv 0 BitSize) && bvult (index i j varPieces) (bv (toIntNat $ Dim * Dim) BitSize)))

dummy : PieceColors ColorBitSize
dummy = MkPieceColors (bv 0 ColorBitSize) (bv 0 ColorBitSize) (bv 0 ColorBitSize) (bv 0 ColorBitSize)

colorConstraint : Fin Dim -> Fin Dim -> Vect Dim (Vect Dim (PieceColors ColorBitSize)) -> Expr BoolT
colorConstraint i j pcs with (index i j pcs, toLookup i j dummy pcs)
  colorConstraint i j pcs | (pc, (FF r d)) = and [upVar pc == bv (colorInt 'X') ColorBitSize,
                                                  leftVar pc == bv (colorInt 'X') ColorBitSize,
                                                  rightVar pc == leftVar r, downVar pc == upVar d]
  colorConstraint i j pcs | (pc, (LL u l)) = and [downVar pc == bv (colorInt 'X') ColorBitSize,
                                                  rightVar pc == bv (colorInt 'X') ColorBitSize,
                                                  upVar pc == downVar u, leftVar pc == rightVar l]
  colorConstraint i j pcs | (pc, (FL d l)) = and [upVar pc == bv (colorInt 'X') ColorBitSize,
                                                  rightVar pc == bv (colorInt 'X') ColorBitSize,
                                                  downVar pc == upVar d, leftVar pc == rightVar l]
  colorConstraint i j pcs | (pc, (LF u r)) = and [downVar pc == bv (colorInt 'X') ColorBitSize,
                                                  leftVar pc == bv (colorInt 'X') ColorBitSize,
                                                  upVar pc == downVar u, rightVar pc == leftVar r]
  colorConstraint i j pcs | (pc, (FM r d l)) = and [upVar pc == bv (colorInt 'X') ColorBitSize,
                                                    downVar pc == upVar d, leftVar pc == rightVar l, rightVar pc == leftVar r]
  colorConstraint i j pcs | (pc, (LM u r l)) = and [downVar pc == bv (colorInt 'X') ColorBitSize,
                                                    upVar pc == downVar u, leftVar pc == rightVar l, rightVar pc == leftVar r]
  colorConstraint i j pcs | (pc, (MF u r d)) = and [leftVar pc == bv (colorInt 'X') ColorBitSize,
                                                    upVar pc == downVar u, downVar pc == upVar d, rightVar pc == leftVar r]
  colorConstraint i j pcs | (pc, (ML u d l)) = and [rightVar pc == bv (colorInt 'X') ColorBitSize,
                                                    upVar pc == downVar u, downVar pc == upVar d, leftVar pc == rightVar l]
  colorConstraint i j pcs | (pc, (M u r d l)) = and [upVar pc == downVar u, downVar pc == upVar d,
                                                     leftVar pc == rightVar l, rightVar pc == leftVar r]

colorConstraints : Vect Dim (Vect Dim (PieceColors ColorBitSize)) -> Expr BoolT
colorConstraints pcs = and $ concat $ tabulate (\i => tabulate (\j => colorConstraint i j pcs))

pieceConstraint : Vect (Dim * Dim) (Int, Vect E Piece) -> Expr (BitVecT BitSize) -> PieceColors ColorBitSize -> Expr BoolT
pieceConstraint ps vp pc = or $ map (\(i, ps) => let ors = or $ map (\p => equalColors p pc) ps in
                                                 bv i BitSize == vp && ors) ps

pieceConstraints : Vect (Dim * Dim) (Int, Vect E Piece) -> Vect Dim (Vect Dim (Expr (BitVecT BitSize))) -> Vect Dim (Vect Dim (PieceColors ColorBitSize)) -> Expr BoolT
pieceConstraints ps vps pcs = and $ concat $ tabulate (\i => tabulate (\j => pieceConstraint ps (index i j vps) (index i j pcs)))

solver : Smt ()
solver = do setLogic "QF_BV"
            setOption ":pp.bv-literals false"
            setOption ":model_validate true"
            varPieces <- declareVars varPieces (BitVecT BitSize)
            varColorPieces <- declareVars varColorPieces (BitVecT ColorBitSize)
            let varPieces = toVect varPieces
            let varColorPieces = toVect varColorPieces
            let colorPieces = mapColorPieces varColorPieces
            assert $ validPieces varPieces
            assert $ distinct $ concat varPieces
            assert $ colorConstraints colorPieces
            assert $ pieceConstraints pieces varPieces colorPieces
            checkSat
            getModel
            end

pieceColorSolution : Vect Dim (Vect Dim (Vect E String)) -> Model -> Vect Dim (Vect Dim String)
pieceColorSolution vcps model = tabulate (\i => tabulate (\j => let f = the (Fin E -> String)
                                                                        (\k => case lookup (index k $ index j $ index i vcps) model of
                                                                                Nothing => ""
                                                                                Just v => case parseInteger {a = Int} v of
                                                                                Nothing => ""
                                                                                Just x => cast $ intColor x) in
                                                                f 0 ++ f 1 ++ f 2 ++ f 3))

pieceSolution : Vect Dim (Vect Dim String) -> Model -> Vect Dim (Vect Dim String)
pieceSolution vps model =  tabulate (\i => tabulate (\j => case lookup (index i j vps) model of
                                                                Nothing => ""
                                                                Just v => v))

runSolver : IO ()
runSolver = do r <- sat solver
               case r of
                 Nothing => do putStrLn "Error parsing result"
                 Just (Sat, model) =>
                        do putStrLn $ unlines $ toList $ map (unwords . toList) $ pieceSolution (toVect varPieces) model
                           putStrLn $ unlines $ toList $ map (unwords . toList) $ pieceColorSolution (toVect varColorPieces) model
                 Just (UnSat, _) => putStrLn "unsat"
                 Just (Unknown, _) => putStrLn "unknown"

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets