text:
import Data.Fin

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

append : Vect n e -> Vect m e -> Vect (n + m) e
append [] ys = ys
append (x :: xs) ys = x :: append xs ys

zip : Vect n a -> Vect n b -> Vect n (a, b)
zip [] ys = []
zip (x :: xs) (y :: ys) = (x, y) :: zip xs ys

index : Fin len -> Vect len e -> e
index FZ (x::_)  = x
index (FS k) (_::xs) = index k xs

tryIndex : {n : _} -> Integer -> Vect n a -> Maybe a
tryIndex i xs = case integerToFin i n of
                     Nothing => Nothing
                     (Just x) => Just (index x xs)

max_stars_repo_name: brunoflores/type-driven-with-idris

max_issues_repo_name: brunoflores/type-driven-with-idris

max_forks_repo_name: brunoflores/type-driven-with-idris


text:
import Data.Vect

infixr 5 .+.

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

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

data Command: Schema -> Type where
  -- SetSchema: (newSchema: Schema) -> Command schema
  Add: SchemaType schema -> Command schema
  Get: Integer -> Command schema
  Size: Command schema
  Quit: Command schema

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

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

display: SchemaType schema -> String
display {schema = SString} item = item
display {schema = SInt} item = show item
display {schema = (x .+. y)} (iteml, itemr) = display iteml ++ ", " ++ display itemr

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

parsePrefix: (schema: Schema) -> String -> Maybe (SchemaType schema, String)
parsePrefix SString item = getQuoted(unpack item)
  where
    getQuoted: List Char -> Maybe (String, String)
    getQuoted ('"' :: xs) = case span (/= '"') xs of
      (quoted, '"' :: rest) => Just(pack quoted, ltrim (pack rest))
      _ => Nothing
    getQuoted _ = Nothing

parsePrefix SInt item =
  case span isDigit item of
    ("", rest)  => Nothing
    (num, rest) => Just (cast num, ltrim rest)
parsePrefix (schemal .+. schemar) item =
  case parsePrefix schemal item of
    Nothing => Nothing
    Just(leftVal, input') =>
      case parsePrefix schemar input' of
        Nothing => Nothing
        Just (rightVal, input'') => Just ((leftVal, rightVal), input'')

parseBySchema : (schema : Schema) -> String -> Maybe(SchemaType schema)
parseBySchema schema input = case parsePrefix schema input of
  Just (res, "") => Just res
  Just _         => Nothing
  Nothing        => Nothing

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

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

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

main: IO()
main = replWith (MkData (SString .+. SString .+. SInt) _ [])
                "Command: " processInput

ext: idr

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
> module Lit

Test some string primitives while we're at it

> export st : String
> st = "abcdefg"

Literate main program

> export main : IO ()
> main = do { putStrLn (show (strHead st))
>             putStrLn (show (strIndex st 3))
>             putStrLn (strCons 'z' st)
>             putStrLn (reverse st)
>             let x = unpack st
>             putStrLn (show (reverse x))
>             putStrLn (pack x)
>           }

ext: lidr

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Text.WebIDL.Lexer

import Data.List
import Data.String
import Text.Lexer
import Text.WebIDL.Types

%default total

-- alias for `some`
plus : Lexer -> Lexer
plus = some

-- alias for `some`
star : Lexer -> Recognise False
star = many

-- /[1-9]/
nonZeroDigit : Lexer
nonZeroDigit = pred $ \c => '1' <= c && c <= '9'

--------------------------------------------------------------------------------
--          Numbers
--------------------------------------------------------------------------------

parseInt : String -> IdlToken
parseInt s = maybe (Invalid s) ILit $ readInt s

parseFloat : String -> IdlToken
parseFloat s = maybe (Invalid s) FLit $ readFloat s

-- /0[Xx][0-9A-Fa-f]+/
hex : Lexer
hex = (exact "0x" <|> exact "0X") <+> plus hexDigit

-- /0[0-7]*/
oct : Lexer
oct = is '0' <+> star octDigit

-- any integer literal
int : Lexer
int = hex <|> oct <|> (opt (is '-') <+> plus digit)

-- /[Ee][+-]?[0-9]+/
exp : Lexer
exp = oneOf "Ee" <+> opt (oneOf "+-") <+> plus digit

-- /([0-9]+\.[0-9]*|[0-9]*\.[0-9]+)([Ee][+-]?[0-9]+)?/
expOpt : Lexer
expOpt = let pre =   (plus digit <+> is '.' <+> star digit)
                 <|> (star digit <+> is '.' <+> plus digit)
          in pre <+> opt exp

-- [0-9]+[Ee][+-]?[0-9]+
expNonOpt : Lexer
expNonOpt = plus digit <+> exp

float : Lexer
float = (opt (is '-') <+> (expOpt <|> expNonOpt))

--------------------------------------------------------------------------------
--          Others
--------------------------------------------------------------------------------

-- [_-]?[A-Za-z][0-9A-Z_a-z-]*
identifier : Lexer
identifier =   opt (oneOf "_-")
           <+> alpha
           <+> star (pred $ \c => isAlphaNum c || c == '_' || c == '-')

-- Takes a valid identifier and converts it either
-- to a FloatLit, a Keyword, or an Identifier
ident : String -> IdlToken
ident "Infinity"        = FLit Infinity
ident "-Infinity"       = FLit NegativeInfinity
ident "NaN"             = FLit NaN
ident s                 = maybe (Ident $ MkIdent s) Key (refine s)

-- /\/\/.*/
comment : Lexer
comment =   lineComment (exact "//" )
        <|> surround (exact "/*" ) (exact "*/") any

-- /[^\t\n\r 0-9A-Za-z]/
other : Lexer
other = pred $
        \c => not (isAlpha c || isDigit c || isSpace c || isControl c)

symbol : String -> IdlToken
symbol "..." = Other Ellipsis
symbol s     = case fastUnpack s of
                    [c] => Other (Symb c)
                    _   => Invalid s

--------------------------------------------------------------------------------
--          Lexing
--------------------------------------------------------------------------------

tokenMap : TokenMap IdlToken
tokenMap = [ (spaces,                const Space)
           , (stringLit,             SLit . MkStrLit)
           , (comment,               Comment)
           , (identifier,            ident)
           , (float,                 parseFloat)
           , (int,                   parseInt)
           , (exact "..." <|> other, symbol)
           ]

isNoise : IdlToken -> Bool
isNoise Space       = True
isNoise (Comment _) = True
isNoise _           = False

||| Generates a list of IdlTokens (wrapped in TokenData, so
||| they come with line and position numbers) from an input
||| string.
export
lexIdl : String -> Either String $ List (WithBounds IdlToken)
lexIdl s = case lex tokenMap s of
                (ts, (_,_,"")) => Right ts
                (_,  t)        => Left $ "Lexer aborted at " ++ show t

||| Generates a list of IdlTokens
||| from an input string, removing unnecessary tokens by
||| means of `isNoise`.
export
lexIdlNoNoise : String -> Either String $ List (WithBounds IdlToken)
lexIdlNoNoise = map (filter (not . isNoise . val)) . lexIdl


text:
module xquant.Math.Set

import public Data.Vect

%default total

||| A vector of unique elements
data Set : Vect n a -> Type where
  Nil  : Set []
  (::) : Not (Elem x xs) -> Set xs -> Set (x :: xs)

||| Elements of a type
data HasElements : (t : Type) -> (v : Vect n t) -> Type where
  MkHas : {v : Vect n t} ->
          Set v ->
          ((x : t) -> Elem x v) ->
          HasElements t v

data Cardinality : (t : Type) -> Nat -> Type where
  Cardinal : {v : Vect n t} -> HasElements t v -> Cardinality t n

noElem : Elem x [] -> Void
noElem Here impossible

---- Example: Bool ----

notElemTF : Elem True [False] -> Void
notElemTF Here impossible
notElemTF (There x) = noElem x

setFalse : Set [False]
setFalse = noElem :: []

set1 : (x : a) -> Set [a]
set1 x = noElem :: []

setTrueFalse : Set [True, False]
setTrueFalse = notElemTF :: setFalse

boolHas : HasElements Bool [True,False]
boolHas = MkHas setTrueFalse (\b => case b of
                                         True  => Here
                                         False => There Here)

boolHasTwo : Cardinality Bool 2
boolHasTwo = Cardinal boolHas

max_stars_repo_name: fieldstrength/xquant

max_issues_repo_name: fieldstrength/xquant

max_forks_repo_name: fieldstrength/xquant


text:
module As

import Test as Toast

Toast.Needle Int where
  nardle x = x + x
  noo x = x * x


text:
import Data.Nat
import Data.Vect

{-
Exercise 1

Using plusZeroRightNeutral and plusSuccRightSucc, write your own version of plusCommutes:

myPlusCommutes : (n : Nat) -> (m : Nat) -> n + m = m + n

Hint: Write this by case splitting on n. In the case of S k,
you can rewrite with a recursive call to myPlusCommutes k m, and rewrites can be nested.
 -}
myPlusCommutative : (n : Nat) -> (m : Nat) -> n + m = m + n
myPlusCommutative 0 m = sym (plusZeroRightNeutral m)
{-
Need to prove: S (plus k m) = plus m (S k)

prf1 : plus k m = plus m k
prf2 : S (plus m k) = plus m (S k)

Using prf1,
Rewrite S (plus m k) = plus m (S k)
as      S (plus k m) = plus m (S k)

 -}
myPlusCommutative (S k) m = let prf1 = myPlusCommutative k m
                                prf2 = plusSuccRightSucc m k
                                in
                                rewrite prf1 in prf2

-- Exercise 2

reverseProof_nil : Vect k a -> Vect (plus k 0) a
reverseProof_nil xs = rewrite plusZeroRightNeutral k in xs

reverseProof_xs : Vect (S (plus k len)) a -> Vect (plus k (S len)) a
reverseProof_xs xs = rewrite sym (plusSuccRightSucc k len) in xs

myReverse2 : Vect n a -> Vect n a
myReverse2 xs = reverse' [] xs where
                reverse' : Vect k a -> Vect m a -> Vect (k + m) a
                reverse' acc [] = reverseProof_nil acc
                reverse' acc (x :: xs) = reverseProof_xs (reverse' (x :: acc) xs)


text:
module NatOrder

import NatUtils

%default total
%access public export

|||New type for <= on Nat
LEQ : (a : Nat) -> (b : Nat) -> Type
LEQ a b = (k : Nat ** ((a + k) = b))

|||New type for >= on Nat
GEQ : (a : Nat) -> (b : Nat) -> Type
GEQ a b = LEQ b a

|||New type for < on Nat
LNEQ : (a : Nat) -> (b : Nat) -> Type
LNEQ a b = (LEQ a b, Not (a = b))

|||New type for > on Nat
GNEQ : (a : Nat) -> (b : Nat) -> Type
GNEQ a b = LNEQ b a

|||Proof that 0 is the smallest natural number
LEQZero : {n : Nat} -> LEQ Z n
LEQZero {n} = (n ** Refl)

|||Proof that 0 is lesser than every successor
LNEQZeroSucc : {n : Nat} -> LNEQ Z (S n)
LNEQZeroSucc {n} = (((S n) ** Refl), ZIsNotS)

|||Proof that a <= b implies (S a) <= (S b)
LEQSucc : {a : Nat} -> {b : Nat} -> (LEQ a b) -> (LEQ (S a) (S b))
LEQSucc {a} {b} (k ** proofEq) = (k ** cong proofEq)

|||Proof that a < b implies (S a) < (S b)
LNEQSucc : {a : Nat} -> {b : Nat} -> (LNEQ a b) -> (LNEQ (S a) (S b))
LNEQSucc {a} {b} ((k ** proofEq), proofNotEq) = ((k ** cong proofEq), proofNotEqSucc proofNotEq) where
	proofNotEqSucc : (Not (a = b)) -> (Not (S a = S b))
	proofNotEqSucc proofNotEq proofEq = proofNotEq (predEqual proofEq)

|||Proof that (S a) <= (S b) implies a <= b
LEQPred : {a : Nat} -> {b : Nat} -> (LEQ (S a) (S b)) -> (LEQ a b)
LEQPred {a} {b} (k ** proofEq) = (k ** predEqual proofEq)

|||Proof that (S a) < (S b) implies a < b
LNEQPred : {a : Nat} -> {b : Nat} -> (LNEQ (S a) (S b)) -> (LNEQ a b)
LNEQPred {a} {b} ((k ** proofEq), proofNotEq) = ((k ** predEqual proofEq), proofNotEqPred proofNotEq) where
	proofNotEqPred : (Not (S a = S b)) -> (Not (a = b))
	proofNotEqPred proofNotEq proofEq = proofNotEq (cong proofEq)

|||Proof that !(a <= b) implies !((S a) <= (S b))
notLEQSucc : {a : Nat} -> {b : Nat} -> (Not (LEQ a b)) -> (Not (LEQ (S a) (S b)))
notLEQSucc {a} {b} proofNotLEQ proofLEQ = proofNotLEQ (LEQPred proofLEQ)

|||Proof that !((S a) <= (S b)) implies !(a <= b)
notLEQPred : {a : Nat} -> {b : Nat} ->  (Not (LEQ (S a) (S b))) -> (Not (LEQ a b))
notLEQPred {a} {b} proofNotLEQ proofLEQ = proofNotLEQ (LEQSucc proofLEQ)

|||Proof that !(a < b) implies !((S a) < (S b))
notLNEQSucc : {a : Nat} -> {b : Nat} -> (Not (LNEQ a b)) -> (Not (LNEQ (S a) (S b)))
notLNEQSucc {a} {b} proofNotLNEQ proofLNEQ = proofNotLNEQ (LNEQPred proofLNEQ)

|||Proof that !((S a) < (S b)) implies !(a < b)
notLNEQPred : {a : Nat} -> {b : Nat} ->  (Not (LNEQ (S a) (S b))) -> (Not (LNEQ a b))
notLNEQPred {a} {b} proofNotLNEQ proofLNEQ = proofNotLNEQ (LNEQSucc proofLNEQ)

|||Proof that !(a < = b) implies b < a
notLEQImpliesGNEQ : {a : Nat} -> {b : Nat} -> (Not (LEQ a b)) -> (GNEQ a b)
notLEQImpliesGNEQ {a = Z} {b} proofNotLEQ = void (proofNotLEQ (b ** Refl))
notLEQImpliesGNEQ {a = (S n)} {b = Z} _ = ((S n ** Refl), ZIsNotS)
notLEQImpliesGNEQ {a = (S n)} {b = (S m)} proofNotLEQ = (LEQSucc proofGEQ, notEqualSucc proofNotEq) where
	proofGEQ = fst (notLEQImpliesGNEQ {a = n} {b = m} (notLEQPred proofNotLEQ))
	proofNotEq = snd (notLEQImpliesGNEQ {a = n} {b = m} (notLEQPred proofNotLEQ))

|||Proof that !(a < b) implies b <= a
notLNEQImpliesGEQ : {a : Nat} -> {b : Nat} -> (Not (LNEQ a b)) -> (GEQ a b)
notLNEQImpliesGEQ {a} {b = Z} _ = (a ** Refl)
notLNEQImpliesGEQ {a = Z} {b = (S m)} proofNotLNEQ = void (proofNotLNEQ (((S m) ** Refl), ZIsNotS))
notLNEQImpliesGEQ {a = (S n)} {b = (S m)} proofNotLNEQ = (LEQSucc proofGEQ) where
	proofGEQ = notLNEQImpliesGEQ {a = n} {b = m} (notLNEQPred proofNotLNEQ)

|||decides if a <= b
isLEQ : (a : Nat) -> (b : Nat) -> Dec (LEQ a b)
isLEQ Z b = Yes (b ** Refl)
isLEQ (S a) Z = No (\(k ** proofEq) => (SIsNotZ proofEq))
isLEQ (S a) (S b) with (isLEQ a b)
	isLEQ (S a) (S b) | (Yes proofLEQ) = Yes (LEQSucc proofLEQ)
	isLEQ (S a) (S b) | (No contra) = No (\(k ** proofEq) => (contra (k ** (predEqual proofEq))))

|||Proof that a <= b implies a = b or a < b
leqImpliesEqOrLNEQ : {a : Nat} -> {b : Nat} -> (LEQ a b) -> Either (a = b) (LNEQ a b)
leqImpliesEqOrLNEQ {a} {b} (k ** proofEq) = case k of
	Z => Left (rewrite (plusCommutative Z a) in proofEq)
	(S n) => Right (((S n) ** proofEq), nonZeroSumNotEqual proofEq SIsNotZ)

|||Proof that all successors are larger than 0
succNotLEQzero : {n : Nat} -> (Not (LEQ (S n) Z))
succNotLEQzero {n} = \(k ** proofEq) => (SIsNotZ proofEq)

|||Proof that LEQ is reflexive
leqRefl : {n : Nat} -> LEQ n n
leqRefl {n} = (Z ** plusZeroRightNeutral n)

|||Proof that (a + k = b) and (b + l = a) implies (k = 0) and (l = 0)
leqAntiSymmetricIndirect : {a : Nat} -> {b : Nat} ->
						(proofLEQLeft : (LEQ a b)) -> (proofLEQRight : (LEQ b a)) ->
						((fst proofLEQLeft) = Z, (fst proofLEQRight) = Z)
leqAntiSymmetricIndirect {a} {b} (k ** proofEqLeft) (l ** proofEqRight) =
	sumZeroImpliesZero (plusLeftCancel a (k + l) Z inductionStep) where
	inductionStep = rewrite (plusAssociative a Z (k + l)) in
					rewrite (plusZeroRightNeutral a) in
					rewrite (plusAssociative a k l) in
					trans (cong {f = (\n => n + l)} proofEqLeft) proofEqRight

|||Proof that LEQ is antisymmetric
leqAntiSymmetric : {a : Nat} -> {b : Nat} -> (LEQ a b) -> (LEQ b a) -> (a = b)
leqAntiSymmetric {a} {b} (k ** proofEqLeft) (l ** proofEqRight) =
	rewrite (plusCommutative Z a) in
	rewrite (sym (fst (leqAntiSymmetricIndirect {a} {b} (k ** proofEqLeft) (l ** proofEqRight)))) in proofEqLeft

|||Proof that LEQ is transitive
leqTransitive : {a : Nat} -> {b : Nat} -> {c : Nat} -> (LEQ a b) -> (LEQ b c) -> (LEQ a c)
leqTransitive {a} {b} {c} (k ** proofEqLeft) (l ** proofEqRight) = ((k + l) ** proofEq) where
	proofEq = rewrite (plusAssociative a k l) in
			trans (cong {f = (\n => n + l)} proofEqLeft) (proofEqRight)

|||Proof that a <= b implies a <= b + c
leqPlusRight : {a : Nat} -> {b : Nat} -> (c : Nat) -> (LEQ a b) -> (LEQ a (b + c))
leqPlusRight {a} {b} c (k ** proofEq) = ((k + c) ** rewrite (plusAssociative a k c) in (cong {f = (\n => (n + c))} proofEq))

|||Proof that a + c <= b implies a <= b
ltePlusLeft : {a : Nat} -> {b : Nat} -> {c : Nat} -> (LEQ (a + c) b) -> (LEQ a b)
ltePlusLeft {a} {b} {c} (k ** proofEq) = ((c + k) ** rewrite (plusAssociative a c k) in proofEq)

|||Proof that a <= b implies (c + a) <= (c + b)
leqPlusConstantLeft : {a : Nat} -> {b : Nat} -> (c : Nat) -> (LEQ a b) -> (LEQ (c + a) (c + b))
leqPlusConstantLeft {a} {b} c (k ** proofEq) = (k ** proofFinalEq) where
	proofFinalEq = rewrite (sym (plusAssociative c a k)) in (cong {f = (\n => c + n)} proofEq)

|||Proof that a <= b implies (a + c) <= (b + c)
leqPlusConstantRight : {a : Nat} -> {b : Nat} -> (c : Nat) -> (LEQ a b) -> (LEQ (a + c) (b + c))
leqPlusConstantRight {a} {b} c proofLEQ = rewrite (plusCommutative a c) in
									rewrite (plusCommutative b c) in
									(leqPlusConstantLeft c proofLEQ)

|||Proof that (c + a) <= (c + b) implies a <= b
leqMinusConstantLeft : {a : Nat} -> {b : Nat} -> {c : Nat} -> (LEQ (c + a) (c + b)) -> (LEQ a b)
leqMinusConstantLeft {a} {b} {c} (k ** proofEq) = (k ** proofFinalEq) where
	proofFinalEq = (plusLeftCancel c (a + k) b (rewrite (plusAssociative c a k) in proofEq))

|||Proof that (a + c) <= (b + c) implies a <= b
leqMinusConstantRight : {a : Nat} -> {b : Nat} -> {c : Nat} -> (LEQ (a + c) (b + c)) -> (LEQ a b)
leqMinusConstantRight {a} {b} {c} proofLEQ = leqMinusConstantLeft {a} {b} {c} proofFinalEq where
	proofFinalEq = rewrite (plusCommutative c a) in
				rewrite (plusCommutative c b) in proofLEQ

|||Proof that if a <= b, and c <= d, then (a + c) <= (b + d)
leqPlusIsLEQ : {a : Nat} -> {b : Nat} -> {c : Nat} -> {d : Nat} ->
			(LEQ a b) -> (LEQ c d) -> (LEQ (a + c) (b + d))
leqPlusIsLEQ {a = a0} {b = b0} {c = c0} {d = d0} proofLeftLEQ proofRightLEQ =
	leqTransitive (leqPlusConstantRight {a = a0} {b = b0} c0 proofLeftLEQ) (leqPlusConstantLeft {a = c0} {b = d0} b0 proofRightLEQ)

|||Proof that a <= b implies (c * a) <= (c * b)
leqMultConstantLeft : {a : Nat} -> {b : Nat} -> (c : Nat) -> (LEQ a b) -> (LEQ (c * a) (c * b))
leqMultConstantLeft {a} {b} c (k ** proofEq) = ((c * k) ** proofFinalEq) where
	proofFinalEq = rewrite (sym (multDistributesOverPlusRight c a k)) in
				cong {f = (\n => c * n)} proofEq

|||Proof that a <= b implies (a * c) <= (b * c)
leqMultConstantRight : {a : Nat} -> {b : Nat} -> (c : Nat) -> (LEQ a b) -> (LEQ (a * c) (b * c))
leqMultConstantRight {a} {b} c (k ** proofEq) = ((k * c) ** proofFinalEq) where
	proofFinalEq = rewrite (sym (multDistributesOverPlusLeft a k c)) in
				cong {f = (\n => n * c)} proofEq

|||Proof that if a <= b, and c <= d, then (a * c) <= (b * d)
leqMultIsLEQ : {a : Nat} -> {b : Nat} -> {c : Nat} -> {d : Nat} ->
			(LEQ a b) -> (LEQ c d) -> (LEQ (a * c) (b * d))
leqMultIsLEQ {a = a0} {b = b0} {c = c0} {d = d0} proofLeftLEQ proofRightLEQ =
	leqTransitive (leqMultConstantRight {a = a0} {b = b0} c0 proofLeftLEQ) (leqMultConstantLeft {a = c0} {b = d0} b0 proofRightLEQ)

|||Proof that (c * a) <= (c * b) and c != 0 implies a <= b
leqDivConstantLeft : {a : Nat} -> {b : Nat} -> {c : Nat} -> (Not (c = Z)) ->
					(LEQ (c * a) (c * b)) -> (LEQ a b)
--To be proved

|||Proof that (a * c) <= (b * c) and c != 0 implies a <= b
leqDivConstantRight : {a : Nat} -> {b : Nat} -> {c : Nat} -> (Not (c = Z)) ->
					(LEQ (a * c) (b * c)) -> (LEQ a b)
--To be proved

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

|||Convert from LEQ to LTE
leqToLTE : {a : Nat} -> {b : Nat} -> (LEQ a b) -> (LTE a b)
leqToLTE {a = Z} {b} _ = LTEZero
leqToLTE {a = S m} {b = Z} proofLEQ = void(succNotLEQzero proofLEQ)
leqToLTE {a = S m} {b = S n} (k ** proofEq) = LTESucc (leqToLTE {a = m} {b = n} (k ** predEqual proofEq))

|||Convert from LTE to LEQ
lteToLEQ : {a : Nat} -> {b : Nat} -> (LTE a b) -> (LEQ a b)
lteToLEQ {a = Z} {b} _ = LEQZero
lteToLEQ {a = S m} {b = Z} proofLTE = void(succNotLTEzero proofLTE)
lteToLEQ {a = S m} {b = S n} (LTESucc proofLTE) = LEQSucc (lteToLEQ {a = m} {b = n} proofLTE)

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


text:
import Data.Nat

data TakeN : List a -> Type where
     Fewer : TakeN xs
     Exact : (n_xs : List a) -> {rest : _ } -> TakeN (n_xs ++ rest)

takeN : (n : Nat) -> (xs : List a) -> TakeN xs
takeN _ [] = Fewer
takeN 0 _ = Exact [] -- there's some left, and n == Z so it must mean we have an exact amount
takeN (S k) (x :: xs) = case takeN k xs of
                             Fewer => Fewer
                             Exact n_xs => Exact (x :: n_xs)

groupByN : (n : Nat) -> (xs : List a) -> List (List a)
groupByN n xs with (takeN n xs)
  groupByN n xs | Fewer = [xs]
  groupByN n (n_xs ++ rest) | (Exact n_xs) = n_xs :: groupByN n rest

halves : List a -> (List a, List a)
halves xs with (takeN (div (length xs) 2) xs)
  halves xs | Fewer = ([], xs)
  halves (n_xs ++ rest) | (Exact n_xs) = (n_xs, rest)


text:
> module Isomorphism.Properties

> import Control.Isomorphism

> -- import Isomorphism.Operations
> import Fun.Properties
> import Basic.Operations

> %default total
> %access public export

> |||
> isoEq : {A, B : Type} -> A = B -> Iso A B
> isoEq Refl = isoRefl
> %freeze isoEq

> |||
> isoCong : {A : Type} -> {x : A} -> {y : A} -> {P : A -> Type} -> x = y -> Iso (P x) (P y)
> isoCong {x} {P} prf = replace {P = \ z => Iso (P x) (P z)} prf isoRefl
> %freeze isoCong

Injectivity of to and from

> injectiveFrom : {A, B : Type} -> (iso : Iso A B) -> Injective1 (from iso)
> injectiveFrom {A} {B} (MkIso to from toFrom fromTo) b1 b2 p = s3 where
>   s1 : from b1 = from b2
>   s1 = p
>   s2 : to (from b1) = to (from b2)
>   s2 = cong s1
>   s3 : b1 = b2
>   s3 = replace2 {a = B} {a1 = to (from b1)} {a2 = b1}
>                 {b = B} {b1 = to (from b2)} {b2 = b2}
>                 {P = \ a => \b => a = b}
>                 (toFrom b1) (toFrom b2) s2
> %freeze injectiveFrom

> {-

> ---}

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Data.Rel.Complement

import Data.Rel
import Data.Fun
import Data.Fun.Extra
import Data.HVect

%default total

||| The logical complement of a relation.
public export
complement : {ts : Vect n Type} -> (p : Rel ts) -> Rel ts
complement = chain Not

||| The negation of a relation for some elements
||| is equal to the complement of the relation.
public export
notToComplement :
  {0 ts : Vect n Type}
  -> (p : Rel ts)
  -> (elems : HVect ts)
  -> Not (uncurry p elems) = uncurry (complement {ts = ts} p) elems
notToComplement p  = chainUncurry p Not


text:
module Verified.Applicative.Either

import Verified.Applicative
import Verified.Functor
import Verified.Functor.Either

instance VerifiedApplicative (Either a) where
  applicativeMap (Left _) _ = Refl
  applicativeMap (Right _) _ = Refl
  applicativeIdentity (Left _) = Refl
  applicativeIdentity (Right _) = Refl
  applicativeComposition x g1 (Left _) = Refl
  applicativeComposition x (Left _) (Right _) = Refl
  applicativeComposition (Left x) (Right _) (Right _) = Refl
  applicativeComposition (Right _) (Right _) (Right _) = Refl
  applicativeHomomorphism x g = Refl
  applicativeInterchange x (Left _) = Refl
  applicativeInterchange x (Right _) = Refl

max_stars_repo_name: yurrriq/idris-verified

max_issues_repo_name: yurrriq/idris-verified

max_forks_repo_name: yurrriq/idris-verified


text:
> module Fraction.Fraction

> import PNat.PNat

> %default total
> %access public export

> ||| Fraction representation
> Fraction : Type
> Fraction = (Nat, PNat)


text:
module Foldable

data Tree elem = Empty
               | Node (Tree elem) elem (Tree elem)

totLen : List String -> Nat
totLen xs = foldr (\str, acc => acc + length str) 0 xs

Foldable Tree where
  foldr func acc Empty = acc
  foldr func acc (Node l e r)
        = let leftFold = foldr func acc l
              rightFold = foldr func leftFold r in
              func e rightFold


text:
{-
Copyright 2019, Mokshasoft AB (mokshasoft.com)

This software may be distributed and modified according to the terms of
the BSD 2-Clause license. Note that NO WARRANTY is provided.
See "LICENSE_BSD2.txt" for details.
-}

module BareMetal.BitHandler

%access public export
%default total

-- Writes a value to an address bitwise, and waits until the address reflects that value using the mask.
writeAddrWaitMask : Bits32 -> Bits32 -> Bits32 -> IO ()
writeAddrWaitMask addr value mask = do
    foreign FFI_C "write_addr_wait_mask" (Bits32 -> Bits32 -> Bits32 -> IO ()) addr value mask

-- Writes a value to an address bitwise, and waits until the address reflects that value.
writeAddrWait : Bits32 -> Bits32 -> IO ()
writeAddrWait addr value =
    foreign FFI_C "write_addr_wait" (Bits32 -> Bits32 -> IO ()) addr value

-- Waits until the address reflects the value using the mask.
addrWaitMask : Bits32 -> Bits32 -> Bits32 -> IO ()
addrWaitMask addr value mask =
    foreign FFI_C "addr_wait" (Bits32 -> Bits32 -> Bits32 -> IO ()) addr value mask

addrClearBits : Bits32 -> Bits32 -> IO ()
addrClearBits addr mask =
    foreign FFI_C "addr_clear_bits" (Bits32 -> Bits32 -> IO ()) addr mask

addrSetBits : Bits32 -> Bits32 -> IO ()
addrSetBits addr mask =
    foreign FFI_C "addr_set_bits" (Bits32 -> Bits32 -> IO ()) addr mask

max_stars_repo_name: mokshasoft/bare-metal-idris-drivers

max_issues_repo_name: mokshasoft/bare-metal-idris-drivers

max_forks_repo_name: mokshasoft/bare-metal-idris-drivers


text:
||| Show sum of the numbers from input
module NumbersSum

import Data.String

sumNums : List (Maybe Integer) -> Maybe Integer
sumNums [] = Just 0
sumNums (x :: xs) = case (x, sumNums xs) of
                      (Just num1, Just num2) => Just(num1 + num2)
                      (_, _) => Nothing
main : IO ()
main = do
  putStr "Enter numbers separated by a space: "
  x <- getLine
  case sumNums (map parseInteger (words x)) of
    Just sum => putStrLn ("Sum is " ++ show sum)
    Nothing => putStrLn "Invalid input"

max_stars_repo_name: DejanMilicic/IdrisPlayground

max_issues_repo_name: DejanMilicic/IdrisPlayground

max_forks_repo_name: DejanMilicic/IdrisPlayground


text:
module Data.Bool

%default total

export
notInvolutive : (x : Bool) -> not (not x) = x
notInvolutive True  = Refl
notInvolutive False = Refl

-- AND

export
andSameNeutral : (x : Bool) -> x && x = x
andSameNeutral False = Refl
andSameNeutral True = Refl

export
andFalseFalse : (x : Bool) -> x && False = False
andFalseFalse False = Refl
andFalseFalse True = Refl

export
andTrueNeutral : (x : Bool) -> x && True = x
andTrueNeutral False = Refl
andTrueNeutral True = Refl

export
andAssociative : (x, y, z : Bool) -> x && (y && z) = (x && y) && z
andAssociative True  _ _ = Refl
andAssociative False _ _ = Refl

export
andCommutative : (x, y : Bool) -> x && y = y && x
andCommutative x True  = andTrueNeutral x
andCommutative x False = andFalseFalse x

export
andNotFalse : (x : Bool) -> x && not x = False
andNotFalse False = Refl
andNotFalse True = Refl

-- OR

export
orSameNeutral : (x : Bool) -> x || x = x
orSameNeutral False = Refl
orSameNeutral True = Refl

export
orFalseNeutral : (x : Bool) -> x || False = x
orFalseNeutral False = Refl
orFalseNeutral True = Refl

export
orTrueTrue : (x : Bool) -> x || True = True
orTrueTrue False = Refl
orTrueTrue True = Refl

export
orAssociative : (x, y, z : Bool) -> x || (y || z) = (x || y) || z
orAssociative True  _ _ = Refl
orAssociative False _ _ = Refl

export
orCommutative : (x, y : Bool) -> x || y = y || x
orCommutative x True  = orTrueTrue x
orCommutative x False = orFalseNeutral x

export
orNotTrue : (x : Bool) -> x || not x = True
orNotTrue False = Refl
orNotTrue True = Refl

-- interaction & De Morgan's laws

export
orSameAndRightNeutral : (x, y : Bool) -> x || (x && y) = x
orSameAndRightNeutral False _ = Refl
orSameAndRightNeutral True  _ = Refl

export
andDistribOrR : (x, y, z : Bool) -> x && (y || z) = (x && y) || (x && z)
andDistribOrR False _ _ = Refl
andDistribOrR True  _ _ = Refl

export
orDistribAndR : (x, y, z : Bool) -> x || (y && z) = (x || y) && (x || z)
orDistribAndR False _ _ = Refl
orDistribAndR True  _ _ = Refl

export
notAndIsOr : (x, y : Bool) -> not (x && y) = not x || not y
notAndIsOr False _ = Refl
notAndIsOr True  _ = Refl

export
notOrIsAnd : (x, y : Bool) -> not (x || y) = not x && not y
notOrIsAnd False _ = Refl
notOrIsAnd True  _ = Refl

-- Interaction with typelevel `Not`

export
notTrueIsFalse : {1 x : Bool} -> Not (x = True) -> x = False
notTrueIsFalse {x=False} _ = Refl
notTrueIsFalse {x=True}  f = absurd $ f Refl

export
notFalseIsTrue : {1 x : Bool} -> Not (x = False) -> x = True
notFalseIsTrue {x=True} _  = Refl
notFalseIsTrue {x=False} f = absurd $ f Refl


text:
module Three3

%default total
%access public export

data Qry : (Type -> Type) -> Type -> Type where
  ||| Pure for monad/applicative: lift a plain value into the tree
  Pure : a -> Qry q a
  ||| Lift a query into the tree
  Lift : q i -> (i -> a) -> Qry q a
  ||| Gives us a monoid operation
  Join : Qry q (Qry q a) -> Qry q a

liftQ : q a -> Qry q a
liftQ qry = Lift qry id

--infixr 5 ^+^
--||| Generalized semigroup operation, not requiring anything from the underlying
--||| data types
--(^+^) : Qry q a -> Qry q b -> Qry q (a, b)
--(Pure x) ^+^ r = ?bat_2
--(Lift q h) ^+^ r = ?bat_3
--(Join qry) ^+^ r = ?bat_4

-- Back to the same old problem. Must surface the size in the type to
-- demonstrate well-foundedness. Will then loose monad and applicative
-- instances...
Functor (Qry q) where
  map f (Pure x) = Pure $ f x
  map f (Lift q h) = ?functor_huh_2
  map f (Join q) = Join $ map (map f) q


text:
module Daten

-- Liste
zahlen : List Nat
zahlen = [1,2,3,4,5]

zahlen' : List Nat
zahlen' = [1..5]

namen : List String
namen = "Marie" :: "Carsten" :: []

-- Tuple
person : (String, Nat)
person = ("Max", 40)

-- union Type
data Farbe
  = Rot
  | Blau

data Ergebnis
  = Fehler String
  | Erfolg Int

-- GADT
data Ergebnis' : Type where
  Fehler' : String -> Ergebnis'
  Erfolg' : Int -> Ergebnis'

data Expression : Type -> Type where
  Falsch : Expression Bool
  Wahr : Expression Bool
  Zahl : Nat -> Expression Nat
  Plus : Expression Nat -> Expression Nat -> Expression Nat
  Gleich : Expression Nat -> Expression Nat -> Expression Bool
  Falls : Expression Bool -> Expression a -> Expression a -> Expression a


text:
import Data.Vect

-- Exercise 2
data PowerSource = Petrol | Pedal | Electric

-- Exercise 1
data Vehicle : PowerSource -> Type where
    Unicycle : Vehicle Pedal
    Bicycle : Vehicle Pedal
    Motorcycle : (fuel : Nat) -> Vehicle Petrol
    Car : (fuel : Nat) -> Vehicle Petrol
    Bus : (fuel : Nat) -> Vehicle Petrol

wheels : Vehicle power -> Nat
wheels Unicycle = 1
wheels Bicycle = 2
wheels (Motorcycle _) = 2
wheels (Car _) = 4
wheels (Bus _) = 4

refuel : Vehicle Petrol -> Vehicle Petrol
refuel (Motorcycle _) = Motorcycle 100
refuel (Car _) = Car 100
refuel (Bus _) = Bus 100
refuel Unicycle impossible
refuel Bicycle impossible

-- Exercise 3 and Exercise 4
vectTake : (n: Nat) -> Vect (n + m) a -> Vect n a
vectTake Z xs = []
vectTake (S k) (x :: xs) = x :: vectTake k xs

-- Exercise 5
sumEntries : Num a => (pos : Integer) -> Vect n a -> Vect n a -> Maybe a
sumEntries {n} pos xs ys
  = case integerToFin pos n of
      Nothing => Nothing
      (Just idx) => Just $ (Vect.index idx xs) + (Vect.index idx ys)


text:
module Algebra.Solver.CommutativeMonoid

import public Algebra.Monoid
import public Algebra.Solver.Prod
import Syntax.PreorderReasoning

%default total

public export
times : CommutativeMonoid a => Nat -> a -> a
times 0     x = neutral
times (S k) x = x <+> times k x

public export
data Expr : (a : Type) -> (as : List a) -> Type where
  Lit     : (x : a) -> Expr a as
  Var     : (x : a) -> Elem x as -> Expr a as
  Neutral : Expr a as
  Append  : Expr a as -> Expr a as -> Expr a as

public export
FromString a => FromString (Expr a as) where
  fromString = Lit . fromString

public export
Semigroup (Expr a as) where
  (<+>) = Append

public export
Monoid (Expr a as) where
  neutral = Neutral

--------------------------------------------------------------------------------
--          Normalization
--------------------------------------------------------------------------------

public export
record Term (a : Type) (as : List a) where
  constructor T
  factor : a
  prod   : Prod a as

public export
append : CommutativeMonoid a => Term a as -> Term a as -> Term a as
append (T f1 p1) (T f2 p2) = T (f1 <+> f2) (mult p1 p2)

public export
normalize : CommutativeMonoid a => {as : List a} -> Expr a as -> Term a as
normalize (Lit x)      = T x one
normalize (Var x y)    = T neutral (fromVar y)
normalize Neutral      = T neutral one
normalize (Append x y) = append (normalize x) (normalize y)

--------------------------------------------------------------------------------
--          Evaluation
--------------------------------------------------------------------------------

public export
eval : CommutativeMonoid a => Expr a as -> a
eval (Lit x)      = x
eval (Var x y)    = x
eval Neutral      = neutral
eval (Append x y) = eval x <+> eval y

public export
eprod : CommutativeMonoid a => {as : List a} -> Prod a as -> a
eprod []                        = neutral
eprod {as = v :: vs} (exp :: x) = times exp v <+> eprod x

public export
eterm : CommutativeMonoid a => {as : List a} -> Term a as -> a
eterm (T f p) = f <+> eprod p

--------------------------------------------------------------------------------
--          Proofs
--------------------------------------------------------------------------------

0 p1324 :  CommutativeMonoid a
        => {k,l,m,n : a}
        -> (k <+> l) <+> (m <+> n) === (k <+> m) <+> (l <+> n)
p1324 = Calc $
  |~ (k <+> l) <+> (m <+> n)
  ~~ ((k <+> l) <+> m) <+> n ... appendAssociative
  ~~ (k <+> (l <+> m)) <+> n ..< cong (<+>n) appendAssociative
  ~~ (k <+> (m <+> l)) <+> n ... cong (\x => (k <+> x) <+> n) appendCommutative
  ~~ ((k <+> m) <+> l) <+> n ... cong (<+>n) appendAssociative
  ~~ (k <+> m) <+> (l <+> n) ..< appendAssociative

0 pone :  CommutativeMonoid a
       => (as : List a)
       -> eprod {as} Prod.one === Prelude.neutral
pone []        = Refl
pone (v :: vs) = Calc $
  |~ neutral <+> eprod {as = vs} one
  ~~ neutral <+> neutral             ... cong (neutral <+>) (pone vs)
  ~~ neutral                         ... appendLeftNeutral

export
0 pvar :  CommutativeMonoid a
       => (as : List a)
       -> (e  : Elem x as)
       -> eprod (fromVar {as} e) === x
pvar (x :: vs) Here      = Calc $
  |~ (x <+> neutral) <+> eprod {as = vs} one
  ~~ (x <+> neutral) <+> neutral ... cong ((x <+> neutral) <+>) (pone vs)
  ~~ x <+> neutral               ... appendRightNeutral
  ~~ x                           ... appendRightNeutral

pvar (v :: vs) (There y) = Calc $
  |~ neutral <+> eprod (fromVar y)
  ~~ eprod (fromVar y)             ... appendLeftNeutral
  ~~ x                             ... pvar vs y

pvar [] Here impossible
pvar [] (There y) impossible

0 ptimes :  CommutativeMonoid a
         => (m,n : Nat)
         -> (x : a)
         -> times m x <+> times n x === times (m + n) x
ptimes 0     n x = appendLeftNeutral
ptimes (S k) n x = Calc $
  |~ (x <+> times k x) <+> times n x
  ~~ x <+> (times k x <+> times n x) ..< appendAssociative
  ~~ x <+> times (k + n) x           ... cong (x <+>) (ptimes k n x)

0 ppm :  CommutativeMonoid a
      => (e1,e2 : Prod a as)
      -> eprod e1 <+> eprod e2 === eprod (mult e1 e2)
ppm []        []        = appendRightNeutral
ppm {as = v :: vs} (m :: xs) (n :: ys) = Calc $
  |~ (times m v <+> eprod xs) <+> (times n v <+> eprod ys)
  ~~ (times m v <+> times n v) <+> (eprod xs <+> eprod ys)
     ... p1324
  ~~ (times m v <+> times n v) <+> eprod (mult xs ys)
     ... cong ((times m v <+> times n v) <+>) (ppm xs ys)
  ~~ times (m + n) v <+> eprod (mult xs ys)
     ... cong (<+> eprod (mult xs ys)) (ptimes m n v)

0 pappend :  CommutativeMonoid a
          => (e1,e2 : Term a as)
          -> eterm e1 <+> eterm e2 === eterm (append e1 e2)
pappend (T f p) (T g q) = Calc $
  |~ (f <+> eprod p) <+> (g <+> eprod q)
  ~~ (f <+> g) <+> (eprod p <+> eprod q) ... p1324
  ~~ (f <+> g) <+> eprod (mult p q)      ... cong ((f <+> g) <+>) (ppm p q)

0 pnorm :  CommutativeMonoid a
        => (e : Expr a as)
        -> eval e === eterm (normalize e)
pnorm (Lit x) = Calc $
  |~ x
  ~~ x <+> neutral        ..< appendRightNeutral
  ~~ x <+> eprod {as} one ..< cong (x <+>) (pone as)

pnorm (Var x y) = Calc $
 |~ x
 ~~ eprod (fromVar y)             ..< pvar as y
 ~~ neutral <+> eprod (fromVar y) ..< appendLeftNeutral

pnorm Neutral = Calc $
  |~ neutral
  ~~ neutral <+> neutral        ..< appendRightNeutral
  ~~ neutral <+> eprod {as} one ..< cong (neutral <+>) (pone as)

pnorm (Append x y) = Calc $
  |~ eval x <+> eval y
  ~~ eterm (normalize x) <+> eval y
     ... cong (<+> eval y) (pnorm x)
  ~~ eterm (normalize x) <+> eterm (normalize y)
     ... cong (eterm (normalize x) <+>) (pnorm y)
  ~~ eterm (append (normalize x) (normalize y))
     ... pappend (normalize x) (normalize y)

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

export
0 solve :  CommutativeMonoid a
        => (as : List a)
        -> (e1,e2 : Expr a as)
        -> (prf : normalize e1 === normalize e2)
        => eval e1 === eval e2
solve _ e1 e2 = Calc $
  |~ eval e1
  ~~ eterm (normalize e1) ... pnorm e1
  ~~ eterm (normalize e2) ... cong eterm prf
  ~~ eval e2              ..< pnorm e2


text:
-- ----------------------------------------------------------- [ Interface.idr ]
-- Module    : Interface.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Description of an interface as used by an IP Core.
module Cordial.Model.Interface

import Data.Vect
import Data.DList
import Data.Ranged

import Text.Markup.Edda

import public Cordial.Model.Common
import        Cordial.Model.Specification
import public Cordial.Model.Projection

import public Cordial.Model.Interface.Kinds
import public Cordial.Model.Interface.Ports
import public Cordial.Model.Interface.PortGroup

%default total
%access public export

||| Data type representing the physical port.
data Interface : (annot          : Type)
              -> (labelTy        : Type)
              -> (endpoint       : Endpoint)
              -> (kind           : InterfaceKind isMonitor endpoint)
              -> (endian         : Maybe Endian)
              -> (interfaceTy    : InterfaceTy annot labelTy)
              -> (pinterfaceTy   : ProjectedInterfaceTy labelTy endpoint interfaceTy)
              -> Type
  where
    MkInterface : (name            : VLNV)
               -> (endian          : Maybe Endian)
               -> (mustBeConnected : Bool)
               -> (doc             : DocString)
               -> (ports           : PortGroup annot labelTy endpoint endian (portTys ++ flatten chans) pportTys)
               -> Interface annot labelTy endpoint kind endian (MkInterfaceTy  vlnv  i cStyle mp mc portTys chans doc')
                                                               (MkPInterfaceTy vlnv    cStyle pportTys)

portGroup : Interface annot labelTy endpoint kind endian iType iPType
     -> PortGroup annot labelTy endpoint endian (fullPortGroupTy iType) (projectedPortGroup iPType)
portGroup (MkInterface name endian mustBeConnected doc ports) = ports

{- [ NOTE ]

  We source the projected port types from the projected interface.

-}

||| Project an interface based on a given interface kind.
projectByKind : {endpoint : Endpoint}
             -> (kind : InterfaceKind isMonitor endpoint)
             -> (interfaceTy : InterfaceTy annot labelTy)
             -> ProjectedInterfaceTy labelTy endpoint interfaceTy
projectByKind kind interfaceTy {endpoint} = projectInterface endpoint interfaceTy

||| A collection of interfaces.
data Interfaces : (annot : Type)
               -> (kinds         : InterfaceKinds ks)
               -> (interfaceTys  : InterfaceTys annot labelTys)
               -> Type where
  Nil  : Interfaces annot Nil Nil
  (::) : Interface annot labelTy endpoint kind endian interfaceTy (projectByKind kind interfaceTy)
      -> Interfaces annot kinds interfaceTys
      -> Interfaces annot (kind::kinds) (interfaceTy::interfaceTys)

namespace Typed

  ||| Interface definition that calculates the projected interface
  ||| using a given interface type definition, and the projection
  ||| kind.
  Interface : (annot       : Type)
           -> (labelTy       : Type)
           -> (endpoint    : Endpoint)
           -> (kind        : InterfaceKind isMonitor endpoint)
           -> (endian      : Maybe Endian)
           -> (interfaceTy : InterfaceTy annot labelTy)
           -> Type
  Interface annot labelTy endpoint kind endian interfaceTy =
    Interface.Interface annot labelTy endpoint kind endian interfaceTy (projectByKind kind interfaceTy)

  namespace Dictated

    ||| Interface definition that calculates the projected interface
    ||| using a given interface type definition, and the projection
    ||| kind.
    Interface : (annot : Type)
             -> (labelTy : Type)
             -> (kind        : InterfaceKind isMonitor endpoint)
             -> (endian      : Endian)
             -> (interfaceTy : InterfaceTy annot labelTy)
             -> Type
    Interface annot labelTy {endpoint} kind endian interfaceTy =
      Interface.Interface annot labelTy endpoint kind (Just endian) interfaceTy (projectByKind kind interfaceTy)

    PortGroup : (annot  : Type)
             -> (labelTy  : Type)
             -> (type   : InterfaceTy annot labelTy)
             -> (kind   : InterfaceKind isMonitor endpoint)
             -> (endian : Endian)
             -> Type
    PortGroup annot labelTy {endpoint} type kind endian =
      PortGroup.PortGroup annot
                          labelTy
                          endpoint
                          (Just endian)
                          (portGroupTy type ++ flatten (channels type))
                          (projectedPortGroup (projectInterface endpoint type))

  namespace Free
    ||| Interface definition that calculates the projected interface
    ||| using a given interface type definition, and the projection
    ||| kind.
    Interface : (annot       : Type)
             -> (labelTy       : Type)
             -> (kind        : InterfaceKind isMonitor endpoint)
             -> (interfaceTy : InterfaceTy annot labelTy)
             -> Type
    Interface annot labelTy {endpoint} kind interfaceTy =
      Interface.Interface annot labelTy endpoint kind Nothing interfaceTy (projectByKind kind interfaceTy)

    PortGroup : (annot   : Type)
             -> (labelTy   : Type)
             -> (type    : InterfaceTy annot labelTy)
             -> (kind    : InterfaceKind isMonitor endpoint)
             -> Type
    PortGroup annot labelTy {endpoint} type kind =
      PortGroup.PortGroup annot
                          labelTy
                          endpoint
                          Nothing
                          (portGroupTy type ++ flatten (channels type))
                          (projectedPortGroup (projectInterface endpoint type))

  newInterface : (interfaceTy     : InterfaceTy annot labelTy)
              -> (kind            : InterfaceKind isMonitor endpoint)
              -> (name            : VLNV)
              -> (endian          : Maybe Endian)
              -> (mustBeConnected : Bool)
              -> (doc             : DocString)
              -> (ports           : PortGroup annot labelTy endpoint endian
                                       (portGroupTy interfaceTy ++ flatten (channels interfaceTy))
                                       (projectedPortGroup (projectInterface endpoint interfaceTy)))
              -> Interface annot labelTy endpoint kind endian interfaceTy (projectInterface endpoint interfaceTy)
  newInterface type k n e mustConn doc ps with (type)
    newInterface type k n e mustConn doc ps | (MkInterfaceTy name info cstyle maxProducers maxConsumers portGroupTy channels x) =
      MkInterface n e mustConn doc ps

  namespace NoDoc
    newInterface : (interfaceTy     : InterfaceTy annot labelTy)
                -> (kind            : InterfaceKind isMonitor endpoint)
                -> (name            : VLNV)
                -> (endian          : Maybe Endian)
                -> (mustBeConnected : Bool)
                -> (ports           : PortGroup annot labelTy endpoint endian
                                          (portGroupTy interfaceTy ++ flatten (channels interfaceTy))
                                          (projectedPortGroup (projectInterface endpoint interfaceTy)))
                -> Interface annot labelTy endpoint kind endian interfaceTy (projectInterface endpoint interfaceTy)
    newInterface type kind name endian mustConn ps with (type)
      newInterface type kind name endian mustConn ps | (MkInterfaceTy x info cstyle maxProducers maxConsumers portGroupTy channels doc) =
        MkInterface name endian mustConn Empty ps

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

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
module Dynamical

import Data.Vect

%access public export

--- Code by David I. Spivak and David Jaz Myers
--- © 2020

------ The category of arenas ------

--Also called Cont, the category of containers.
--Equivalent to Poly, the category of polynomial functors in one variable.

--- Objects ---
record Arena where
       constructor MkArena
       pos : Type
       dis : pos -> Type

--- Morphisms---

record Lens (dom : Arena) (cod : Arena) where
       constructor MkLens
       observe   : pos dom -> pos cod
       interpret : (p : pos dom) -> dis cod (observe p) -> dis dom p

--- Identity ---

idLens : (a : Arena) -> Lens a a
idLens a = MkLens id (\_ => id)

--- Composition ---

infixr 4 <.>
(<.>) : Lens a2 a3 -> Lens a1 a2 -> Lens a1 a3
(<.>) lens23 lens12 = MkLens obs int
      where
        obs : pos a1 -> pos a3
        obs = (observe lens23) . (observe lens12)

        int : (p : pos a1) -> (dis a3 (obs p)) -> dis a1 p
        int p = (interpret lens12 p) . (interpret lens23 (observe lens12 p))

--- Manipulations on Arenas ---

Display : Arena -> Type
Display a = (p : pos a ** dis a p)

AsFunctor : Arena -> Type -> Type
AsFunctor a y = (p : pos a ** dis a p -> y)

--- Special Arenas ---

ArenaIO : (i : Type) -> (o : Type) -> Arena --positions as output and
ArenaIO i o = MkArena o (\_ => i)           --distinctions as input

Self : Type -> Arena
Self s = ArenaIO s s

Closed : Arena
Closed = ArenaIO () ()

--- Factorization of lenses ---

Factor : {a, c : Arena} -> Lens a c -> (b : Arena ** (Lens b c, Lens a b))
Factor {a} {c} f = (b ** (cartf, vertf)) where
       b     : Arena
       vertf : Lens a b
       cartf : Lens b c
       b     = MkArena (pos a) $ dis c . observe f
       vertf = MkLens id (interpret f)
       cartf = MkLens (observe f) (\_ => id)

--- Reflections to Type ---

Exception : Type -> Arena
Exception t = ArenaIO Void t

Emitter : Type -> Arena
Emitter t = ArenaIO () t

Sensor : Type -> Arena
Sensor t = ArenaIO t ()

ev0 : Arena -> Arena
ev0 a = Exception $ AsFunctor a Void

fromEv0 : (a : Arena) -> Lens (ev0 a) a
fromEv0 a = MkLens o i
          where
            o : (p : pos a ** dis a p -> Void) -> pos a
            o = fst
--          i : (x : pos (ev0 a)) -> dis a (o x) -> dis (ev0 a) x
--          i : (x : AsFunctor a Void) -> dis a (o x) -> dis (ev0 a) x
            i : (x : (p : pos a ** dis a p -> Void)) -> dis a (fst x) -> dis (ev0 a) x
            i (p ** f) = f

ev1 : Arena -> Arena
ev1 a = Exception $ pos a -- = Exception $ AsFunctor a ()

toEv1 : (a : Arena) -> Lens a (ev1 a)
toEv1 a = MkLens id (\_ => absurd)

ev1y : Arena -> Arena
ev1y a = Emitter $ pos a

fromEv1y : (a : Arena) -> Lens (ev1y a) a
fromEv1y a = MkLens id (\_, _ => ())

constantFunction : {t, u : Type} -> (t -> u) -> Lens (Exception t) (Exception u)
constantFunction {t} {u} f = MkLens f (\_ => id)

EmitterFunction : {t, u : Type} -> (t -> u) -> Lens (Emitter t) (Emitter u)
EmitterFunction {t} {u} f = MkLens f (\_ => id)

SensorFunction : {t, u: Type} -> (t -> u) -> Lens (Sensor u) (Sensor t)
SensorFunction {t} {u} f = MkLens id (\_ => f)

enclose : Arena -> Type
enclose a = Lens a Closed

encloseFunction : {t, u : Type} -> (t -> u) -> Lens (ArenaIO u t) Closed
encloseFunction {t} {u} f = MkLens (\_ => ()) (\d => \_ => f d)

auto : {m : Type} -> enclose (Emitter m)
auto {m} = encloseFunction $ \_ => ()

--- functors and monads ---

lift : (f : Type -> Type) -> Functor f => Arena -> Arena
lift f ar = MkArena (pos ar) fdis
          where
            fdis : (p : pos ar) -> Type
            fdis p = f $ dis ar p

LiftLens : {a, b : Arena} -> (f : Type -> Type) -> Functor f =>
           Lens a b -> Lens (lift f a) (lift f b)
LiftLens {a} {b} f lens = MkLens (observe lens) int
          where
            int : (p : pos a) -> f $ dis b (observe lens p) -> f $ dis a p
            int p = map $ interpret lens p

extract : {a : Arena} -> (f : Type -> Type) -> Monad f =>
            Lens (lift f a) a
extract {a} f = MkLens id pur
          where
            pur : (p : pos a) -> dis a p -> dis (lift f a) p
            pur p = pure

extend : {a : Arena} -> (f : Type -> Type) -> Monad f =>
            Lens (lift f a) (lift f (lift f a))
extend {a} f = MkLens id joi
          where
            joi : (p : pos a) -> dis (lift f (lift f a)) p -> dis (lift f a) p
            joi p = join

--- sum ---

zero : Arena
zero = ArenaIO Void Void

infixr 4 <++>

(<++>) : Arena -> Arena -> Arena
(<++>) a b = MkArena posSum disSum
          where
            posSum : Type
            posSum = Either (pos a) (pos b)
            disSum : posSum -> Type
            disSum (Left p)  = dis a p
            disSum (Right p) = dis b p

sum : (ind : Type ** ind -> Arena) -> Arena
sum (ind ** arena) = MkArena psum dsum
          where
            psum : Type
            psum = (i : ind ** pos (arena i))
            dsum : psum -> Type
            dsum (i ** p) = dis (arena i) p

sumLens : Lens a1 b1 -> Lens a2 b2 -> Lens (a1 <++> a2) (b1 <++> b2)
sumLens {a1} {b1} {a2} {b2} l1 l2 = MkLens o i
          where
            o : pos (a1 <++> a2) -> pos (b1 <++> b2)
            o (Left p1)   = Left (observe l1 p1)
            o (Right p2) = Right (observe l2 p2)
            i : (p : pos (a1 <++> a2)) -> dis (b1 <++> b2) (o p) -> dis (a1 <++> a2) p
            i (Left p1) d1  = interpret l1 p1 d1
            i (Right p2) d2 = interpret l2 p2 d2

copair : {a1 : Arena} -> {a2 : Arena} -> {b : Arena} ->
          Lens a1 b -> Lens a2 b -> Lens (a1 <++> a2) b
copair {a1} {a2} {b} l1 l2 = MkLens obs int
          where
            obs : pos (a1 <++> a2) -> pos b
            int : (p : pos (a1 <++> a2)) -> dis b (obs p) -> dis (a1 <++> a2) p
            obs (Left  p1) = observe l1 p1
            obs (Right p2) = observe l2 p2
            int (Left  p1) d1 = interpret l1 p1 d1
            int (Right p2) d2 = interpret l2 p2 d2

--- product ---

one : Arena
one = ArenaIO Void ()

infixr 4 <**>

(<**>) : Arena -> Arena -> Arena
(<**>) a b = MkArena posProd disProd
          where
            posProd : Type
            posProd = (pos a, pos b)
            disProd : posProd -> Type
            disProd (pa, pb) = Either (dis a pa) (dis b pb)

prodList : List Arena -> Arena
prodList [] = one
prodList [a] = a
prodList (a :: as) = a <**> (prodList as)

-- functoriality of prod
prodLens : Lens a1 b1 -> Lens a2 b2 -> Lens (a1 <**> a2) (b1 <**> b2)
prodLens {a1} {b1} {a2} {b2} l1 l2 = MkLens o i
          where
            o : pos (a1 <**> a2) -> pos (b1 <**> b2)
            o (p1, p2) = (observe l1 p1, observe l2 p2)
            i : (p : pos (a1 <**> a2)) -> dis (b1 <**> b2) (o p) -> dis (a1 <**> a2) p
            i (p1, p2) (Left d1)  = Left (interpret l1 p1 d1)
            i (p1, p2) (Right d2) = Right (interpret l2 p2 d2)

-- prod is the dependent product of polynomials; used in both inner homs
prod : (ind : Type ** ind -> Arena) -> Arena
prod (ind ** arena) = MkArena pprod dprod
          where
            pprod : Type
            pprod = (i : ind) -> pos (arena i)
            dprod : pprod -> Type
            dprod p = (i : ind ** dis (arena i) (p i))

pair : {a : Arena} -> {b1 : Arena} -> {b2 : Arena} ->
        Lens a b1 -> Lens a b2 -> Lens a (b1 <**> b2)
pair {a} {b1} {b2} l1 l2 = MkLens obs int
          where
            obs : pos a -> (pos b1, pos b2)
            obs p = (observe l1 p, observe l2 p)
            int : (p : pos a) -> dis (b1 <**> b2) (obs p) -> dis a p
            int p (Left d1)  = interpret l1 p d1
            int p (Right d2) = interpret l2 p d2

--- Juxtaposition ---

infixr 4 &

(&) : Arena -> Arena -> Arena
(&) a b = MkArena posJuxt disJuxt
          where
            posJuxt : Type
            posJuxt = (pos a, pos b)
            disJuxt : posJuxt -> Type
            disJuxt (pa, pb) = (dis a pa, dis b pb)

juxtList : List Arena -> Arena
juxtList [] = Closed
juxtList [a] = a
juxtList (a :: as) = a & (juxtList as)

juxtLens : Lens a1 b1 -> Lens a2 b2 -> Lens (a1 & a2) (b1 & b2)
juxtLens {a1} {b1} {a2} {b2} l1 l2 = MkLens o i
          where
            o : pos (a1 & a2) -> pos (b1 & b2)
            o (p1, p2) = (observe l1 p1, observe l2 p2)
            i : (p : pos (a1 & a2)) -> dis (b1 & b2) (o p) -> dis (a1 & a2) p
            i (p1, p2) (d1, d2) = (interpret l1 p1 d1, interpret l2 p2 d2)

--- Composition product ---

infixr 4 @@
(@@) : Arena -> Arena -> Arena
(@@) a b = MkArena posCirc disCirc
          where
            posCirc : Type
            posCirc = (p : pos a ** dis a p -> pos b)
            disCirc : posCirc -> Type
            disCirc (p ** f) = (d : dis a p ** dis b (f d))

circLens : {a1 : Arena} -> {b1 : Arena} -> {a2 : Arena} -> {b2 : Arena} ->
           Lens a1 b1 -> Lens a2 b2 -> Lens (a1 @@ a2) (b1 @@ b2)
circLens {a1} {b1} {a2} {b2} l1 l2 = MkLens o i
          where
            o : pos (a1 @@ a2) -> pos (b1 @@ b2)
            o (p ** f) = (observe l1 p ** (observe l2) . f . (interpret l1 p))
            i : (p : pos (a1 @@ a2)) -> dis (b1 @@ b2) (o p) -> dis (a1 @@ a2) p
            i (p ** f) (d1 ** d2) = (e1 ** interpret l2 (f e1) d2)
            where
              e1 : dis a1 p
              e1 = interpret l1 p d1

CircPow : Arena -> Nat -> Arena
CircPow _  Z     = Closed
CircPow a (S n) = a @@ CircPow a n

CircPowLens : {a : Arena} -> {b : Arena} ->
              Lens a b -> (n : Nat) -> Lens (CircPow a n) (CircPow b n)
CircPowLens {a} {b} _     Z    = idLens Closed
CircPowLens {a} {b} lens (S n) = circLens lens (CircPowLens lens n)

EmitterPow : (t : Type) -> (n : Nat) -> Lens (CircPow (Emitter t) n) (Emitter (Vect n t))
EmitterPow t Z = MkLens (\_ => Nil) (\_, _ => ())

--- Comonoids ---

record Comonoid where
       constructor MkComonoid
       domains    : Arena
       identities : Lens domains Closed
       codsComps  : Lens domains (domains @@ domains)

codata Behavior : (ar : Arena) -> Type where
          (::) : (p : pos ar) -> (dis ar p -> Behavior ar) -> Behavior ar

head : {ar : Arena} -> Behavior ar -> pos ar
head {ar} (h :: _) = h

tail : {ar : Arena} -> (b : Behavior ar) -> dis ar (head b) -> Behavior ar
tail {ar} (_ :: t) = t

MonSensor : (t : Type) -> t -> (t -> t -> t) -> Comonoid
MonSensor t neut plus = MkComonoid sens idy cc
      where
        sens : Arena
        idy  : Lens sens Closed
        cc   : Lens sens (sens @@ sens)
        sens = (Sensor t)
        idy  = SensorFunction $ \_ => neut
        cc   = MkLens obs int
          where
            obs : pos sens -> (p : pos sens ** dis sens p -> pos sens)
            obs _ = (() ** \_ => ())
            int : (p : pos sens) -> dis (sens @@ sens) (obs p) -> dis sens p
            int _ (d ** e) = d `plus` e

TrajComon : Comonoid
TrajComon = MonSensor Nat Z (+)

--- Selves are comonoids ---

counit : (s : Type) -> Lens (Self s) Closed
counit s = MkLens o i
          where
            o : s -> ()
            o _ = ()
            i : s -> () -> s
            i s _ = s

comult : (s : Type) -> Lens (Self s) ((Self s) @@ (Self s))
comult s = MkLens o i
          where
            o : s -> pos ((Self s) @@ (Self s))
            o x = (x ** id)
            i : (x : s) -> (dis ((Self s) @@ (Self s)) (o x)) -> s
            i x (d1 ** d2) = d2

ContrGrpd : Type -> Comonoid
ContrGrpd t = MkComonoid (Self t) (counit t) (comult t)

comultPow : (s : Type) -> (n : Nat) -> Lens (Self s) (CircPow (Self s) n)
comultPow s  Z    = counit s
comultPow s (S n) = (circLens (idLens (Self s)) (comultPow s n)) <.> (comult s)

--- Duoidal ---

duoidal : {a1, a2, b1, b2 : Arena} -> Lens ((a1 @@ a2) & (b1 @@ b2))
                                           ((a1 & b1) @@ (a2 & b2))
duoidal {a1} {a2} {b1} {b2} = MkLens o i
          where
            x : Arena
            x = (a1 @@ a2) & (b1 @@ b2)
            y : Arena
            y = (a1 & b1) @@ (a2 & b2)
            o : pos x -> pos y
            o ((p1 ** p2), (q1 ** q2)) = pp
              where
                pp : (p : (pos a1, pos b1) ** dis (a1 & b1) p -> pos (a2 & b2))
                pp = ((p1, q1) ** (\d : dis (a1 & b1) (p1, q1) => (p2 (fst d), q2 (snd d))))
            i : (p : pos x) -> dis y (o p) -> dis x p
            i ((p1 ** p2), (q1 ** q2)) = ii
              where
--              ii : dis y ((p1, q1) ** (\d : dis (a1 & b1) (p1, q1) => (p2 (fst d), q2 (snd d))))
--                      -> dis x ((p1 ** p2), (q1 ** q2))
                ii : (de1 : dis (a1 & b1) (p1, q1) ** dis (a2 & b2) (p2 (fst de1), q2 (snd de1)))
                        -> dis x ((p1 ** p2), (q1 ** q2))
                ii (de1 ** de2) = ((fst de1 ** fst de2), (snd de1 ** snd de2))

--- Exponentiation ---

infixr 4 ^

--prod : (ind : Type ** ind -> Arena) -> Arena
(^) : Arena -> Arena -> Arena
(^) a b = prod (pos a ** arena)
          where
            arena : pos a -> Arena
            arena p = b @@ ((Exception $ dis a p) <++> Closed)

--- Internal Hom ---

infixr 4 ^^
(^^) : Arena -> Arena -> Arena
(^^) a b = prod (pos a ** arena)
          where
            arena : pos a -> Arena
            arena p = b @@ (Emitter $ dis a p)

{-
eval : {a : Arena} -> {b : Arena} -> Lens (a & (b ^^ a)) b
eval {a} {b} = MkLens obs int
          where
            obs : (pos a, pos (b ^^ a)) -> pos b
            int : (p : (pos a, pos (b ^^ a))) -> dis b (obs p) -> dis (a & (b ^^ a)) p
            obs (pa, pab) = ?evalo
            int p d = ?evali
-}

--- Dynamical systems ---

record DynSystem where
       constructor MkDynSystem
       state : Type
       body  : Arena
       pheno : Lens (Self state) body

static : DynSystem
static = MkDynSystem () Closed (EmitterFunction id)

infixr 4 &&&
(&&&) : DynSystem -> DynSystem -> DynSystem
(&&&) dyn1 dyn2 = MkDynSystem state12 body12 pheno12
          where
            state12 : Type
            body12  : Arena
            pheno12 : Lens (Self state12) body12
            state12 = (state dyn1, state dyn2)
            body12  = (body dyn1) & (body dyn2)
            pheno12 = MkLens o i
            where
              o : (state dyn1, state dyn2) -> (pos (body dyn1), pos (body dyn2))
              i : (s12 : (state dyn1, state dyn2)) -> dis body12 (o s12) -> state12
              o (s1, s2) = (observe (pheno dyn1) s1, observe (pheno dyn2) s2)
              i (s1, s2) (d1, d2) =
                (interpret (pheno dyn1) s1 d1, interpret (pheno dyn2) s2 d2)

juxtapose : List DynSystem -> DynSystem
juxtapose []        = static
juxtapose [d]       = d
juxtapose (d :: ds) = d &&& (juxtapose ds)

install : (d : DynSystem) -> (a : Arena) -> Lens (body d) a -> DynSystem
install d a l = MkDynSystem (state d) a (l <.> (pheno d))

speedUp : DynSystem -> Nat -> DynSystem
speedUp dyn n = MkDynSystem (state dyn) fastBody fastWork
            where
              fastBody   : Arena
              fastWork   : Lens (Self $ state dyn) fastBody
              fastBody   = CircPow (body dyn) n
              fastWork   = CircPowLens (pheno dyn) n <.> comultPow (state dyn) n

run : (d : DynSystem) -> enclose (body d) -> (state d) -> Stream (pos $ body d)
run d e s = outp :: (run d e next)
            where
              outp : pos $ body d
              next : state d
              outp = observe (pheno d) s
              next = interpret (pheno d) s $ interpret e outp ()

toStreamBehavior : {a : Arena} -> (b : Behavior a) -> (phys : enclose a) -> Stream (pos a)
toStreamBehavior {a} b phys = currpos :: toStreamBehavior rest phys
  where
    currpos : pos a
    currpos = head b

    rest : Behavior a
    rest = tail b $ interpret phys currpos ()

dynBehavior : (d : DynSystem) -> (state d) -> Behavior (body d)
dynBehavior dyn st = current :: choice
            where
              current : pos $ body dyn
              choice  : dis (body dyn) current -> Behavior (body dyn)
              current  = observe (pheno dyn) st
              choice d = dynBehavior dyn (interpret (pheno dyn) st d)

runBehav : (d : DynSystem) -> enclose (body d) -> (state d) -> Stream (pos $ body d)
runBehav dyn phys st = toStreamBehavior (dynBehavior dyn st) phys

--- IO ---

-- EmitterM : (m : Type -> Type) -> Monad m => (a : Type) -> DynSystem
-- EmitterM m a = MkDynSystem (m a) (Emitter (m a)) passInput
--           where
--             passInput : Lens (Self (m a)) (Emitter (m a))
--             passInput = MkLens id

IOEmitter : (a : Type) -> (String -> a) -> DynSystem
IOEmitter a Cast = MkDynSystem (IO a) (Emitter $ IO a) passUserInput
          where
            passUserInput : Lens (Self $ IO a) (Emitter $ IO a)
            passUserInput = MkLens id listen
            where
              listen : (old : IO a) -> () -> IO a
              listen _ _ = map Cast getLine

--- Debugging ---

-- current : (d : DynSystem) -> state d -> pos (body d)
-- current d s = observe (pheno d) s

-- feed : (dyn : DynSystem) -> (s : state dyn) -> dis (body dyn) (observe (pheno dyn) s) -> state dyn
-- feed dyn s d = interpret play s d
--           where
--             play : Lens (Self (state dyn)) (body dyn)
--             play = pheno dyn

--- Examples ---

funcToDynSystem : {s : Type} -> {t : Type} -> (s -> t) -> DynSystem
funcToDynSystem {s} {t} f = MkDynSystem t bodyf phenof
            where
              bodyf : Arena
              phenof : Lens (Self t) bodyf
              bodyf = ArenaIO s t
              phenof = MkLens id (\_ => f)

delay : (s : Type) -> DynSystem
delay s = funcToDynSystem (the (s -> s) id)

plus : DynSystem
plus = funcToDynSystem (uncurry (+))

Prefib : DynSystem
Prefib = plus &&& (delay Integer)

fibwd : Lens (body Prefib) (Emitter Integer)
fibwd = MkLens observe interpret
          where
            observe : (Integer, Integer) -> Integer
            interpret : (p : (Integer, Integer)) -> () -> dis (body Prefib) p
            observe (pl, de) = de
            interpret (pl, de) = \_ => ((de, pl), pl)

Fibonacci : DynSystem
Fibonacci = install Prefib (Emitter Integer) fibwd

FibSeq : Stream Integer
FibSeq = run Fibonacci auto (1, 1)

--------  Fibonacci in REPL --------

-- Run this in the REPL:
-- take 10 FibSeq

-- ==========================

--- Distributivity ---

prodSum : {a, b, c : Arena} -> Lens (a <**> (b <++> c)) ((a <**> b) <++> (a <**> c))
prodSum {a} {b} {c} = MkLens o i
            where
              a1 : Arena
              a1 = a <**> (b <++> c)
              a2 : Arena
              a2 = (a <**> b) <++> (a <**> c)
              o : pos a1 -> pos a2
              o (p, Left q)  = Left (p, q)
              o (p, Right r) = Right (p, r)
              i : (p : pos a1) -> dis a2 (o p) -> dis a1 p
              i (pa, Left pb) (Left da) = Left da
              i (pa, Left pb) (Right db) = Right db
              i (pa, Right pc) (Left da) = Left da
              i (pa, Right pc) (Right dc) = Right dc

sumProd : {a, b, c : Arena} -> Lens ((a <**> b) <++> (a <**> c)) (a <**> (b <++> c))
sumProd {a} {b} {c} = MkLens o i
            where
              a1 : Arena
              a1 = (a <**> b) <++> (a <**> c)
              a2 : Arena
              a2 = a <**> (b <++> c)
              o : pos a1 -> pos a2
              o (Left (pa, pb)) = (pa, Left pb)
              o (Right (pa, pc)) = (pa, Right pc)
              i : (p : pos a1) -> dis a2 (o p) -> dis a1 p
              i (Left (pa, pb)) (Left da) = Left da
              i (Left (pa, pb)) (Right db) = Right db
              i (Right (pa, pc)) (Left da) = Left da
              i (Right (pa, pc)) (Right dc) = Right dc

juxtSum : {a, b, c : Arena} -> Lens (a & (b <++> c)) ((a & b) <++> (a & c))
juxtSum {a} {b} {c} = MkLens o i
            where
              a1 : Arena
              a1 = a & (b <++> c)
              a2 : Arena
              a2 = (a & b) <++> (a & c)
              o : pos a1 -> pos a2
              o (pa, Left pb) = Left (pa, pb)
              o (pa, Right pc) = Right (pa, pc)
              i : (p : pos a1) -> dis a2 (o p) -> dis a1 p
              i (pa, Left pb) (da, db) = (da, db)
              i (pa, Right pc) (da, dc) = (da, dc)

sumJuxt : {a, b, c : Arena} -> Lens ((a & b) <++> (a & c)) (a & (b <++> c))
sumJuxt {a} {b} {c} = MkLens o i
            where
              a1 : Arena
              a1 = (a & b) <++> (a & c)
              a2 : Arena
              a2 = a & (b <++> c)
              o : pos a1 -> pos a2
              o (Left (pa, pb)) = (pa, Left pb)
              o (Right (pa, pc)) = (pa, Right pc)
              i : (p : pos a1) -> dis a2 (o p) -> dis a1 p
              i (Left (pa, pb)) (da, db) = (da, db)
              i (Right (pa, pc)) (da, dc) = (da, dc)

max_stars_repo_name: mstone/poly

max_issues_repo_name: dspivak/poly

max_forks_repo_name: dspivak/poly


text:
module VectFilter

import Data.Vect

filter' : (a -> Bool) -> Vect n a -> (m ** Vect m a)
filter' pred [] = (0 ** [])
filter' pred (x :: xs) =
  let (_ ** rek) = filter' pred xs
  in if pred x then (_ ** x::rek) else (_ ** rek)

beispiel : (m ** Vect m Integer)
beispiel = filter' (\x => (x `mod` 2) == 0) [1,2,3,4,5,6,7,8,9,10]


text:
import Data.Vect

Position : Type
Position = (Double, Double)

Polygon : Nat -> Type
Polygon n = Vect n Position

StringOrInt : Bool -> Type
StringOrInt False = String
StringOrInt True = Int

getStringOrInt : (isInt : Bool) -> StringOrInt isInt
getStringOrInt False = "false"
getStringOrInt True = 1

valToString : (isInt : Bool) -> StringOrInt isInt -> String
valToString False y = ?valToString_rhs_2
valToString True y = ?valToString_rhs_3

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
import System
import System.File
import System.Info
import Data.List1
import Data.String

windowsPath : String -> String
windowsPath path =
    let replaceSlashes : List Char -> List Char
        replaceSlashes [] = []
        replaceSlashes ('/' :: cs) = '\\' :: replaceSlashes cs
        replaceSlashes (c :: cs) = c :: replaceSlashes cs
    in
        pack $ replaceSlashes (unpack path)

main : IO ()
main = do
    Just cmd <- getEnv "POPEN_CMD"
        | Nothing => putStrLn "POPEN_CMD env var not set"
    let cmd = if isWindows then windowsPath cmd else cmd
    Right fh <- popen cmd Read
        | Left err => printLn err
    putStrLn "opened"
    Right output <- fGetLine fh
        | Left err => printLn err
    pclose fh
    putStrLn "closed"
    let (idris2 ::: _) = split ((==) ',') output
        | _ => printLn "Unexpected result"
    putStrLn idris2


text:
module Main
import System

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

readNumbers : IO (Maybe (Nat, Nat))
readNumbers =
  do Just num1_ok <- readNumber
     Just num2_ok <- readNumber
     pure (Just (num1_ok, num2_ok))

guess : (target : Nat) -> (guesses : Nat) -> IO ()
guess target guesses = do putStr ("Guess the number (" ++ show guesses ++ " guesses so far): ")
                          Just startNum <- readNumber | Nothing => do putStrLn "Invalid input"
                                                                      guess target guesses
                          case compare startNum target of
                             LT => do putStrLn "Too low"
                                      guess target (S guesses)
                             EQ => do putStrLn ("You finally got it: " ++ show target ++ " (after " ++ show guesses ++ " tries)")
                                      pure ()
                             GT => do putStrLn "Too high"
                                      guess target (S guesses)

main : IO ()
main = do rand <- time
          let randy = cast (mod rand 100)
          guess randy 0


text:
module Sub05Apply9x6

import ProofColDivSeqBase
import ProofColDivSeqPostulate
import ProofColDivSeqPostuProof

%default total
-- %language ElabReflection

-- 3(3x+2) --C[4,-4]--> 3x
export
apply9x6 : (Not . P) (S (S (plus (plus j j) j)))
  -> (m : Nat ** (LTE (S m) (S (S (plus (plus j j) j))), (Not . P) m))
apply9x6 {j} col = (j ** (lte9x6 j, c9x6To3x j col)) where
  lte9x6 : (j:Nat) -> LTE (S j) (S (S (plus (plus j j) j)))
  lte9x6 Z = (lteSuccRight . LTESucc) LTEZero
  lte9x6 (S j) = let lemma = lte9x6 j in
    rewrite (sym (plusSuccRightSucc j j)) in
    rewrite (sym (plusSuccRightSucc (plus j j) j)) in
      (lteSuccRight . lteSuccRight . LTESucc) lemma


text:
module DecEqTest

import Language.Elab.Deriving.DecEq
import Decidable.Equality

%language ElabReflection

data Flippy = Dolphin | Shark

%runElab deriveDecEq Export  `{{Flippy}}

export
data Foo1 : Type -> Type where
  Bor1 : Foo1 a

export
data Foo2 : Type -> Type where
  Bor2 : a -> Foo2 a

data Foo4 : Type -> Type -> Type where
  Bor4 : b -> Foo4 a b

data Foo5 : Type -> Type -> Type -> Type where
  Bor5 : a -> b -> c -> Foo5 a b c

-- NB c is never used, so Eq shouldn't be required for it
data Foo7 : Type -> Type -> Type -> Type where
  Zor7 : a -> Foo7 a b c
  Gor7 : b -> Foo7 a b c
  Nor7A : a -> b -> Foo7 a b c
  Nor7B : a -> b -> c -> Foo7 a b c
  Bor7 : Foo7 a b c

-- NB a is never used, so Eq shouldn't be required for it
data Foo7' : Type -> Type -> Type -> Type where
  Zor7' : c -> Foo7' a b c
  Gor7' : b -> Foo7' a b c
  Nor7' : b -> c -> Foo7' a b c
  Bor7' : Foo7' a b c

  -- we'll use our own nat for index experimentation
export
data MyNat : Type where
  MZ : MyNat
  MS : MyNat -> MyNat

data Foo6 : Type -> Type -> Type -> Nat -> Type where
  Zor6 : a -> b -> Foo6 a b c Z
  Gor6 : b -> Foo6 a b c (S k)
  Nor6A : a -> b -> c -> Foo6 a b c n
  -- Nor6B : a -> (0 _ : b) -> c -> Foo6 a b c n -- NB: 0 Use arg
  Bor6A : Foo6 a b c n
  Bor6B : Foo6 a b c n -> Foo6 a b c n
  Wah6 : a -> (n : Nat) -> Foo6 a b c n

export
data Foo6' : Type -> Type -> Type -> MyNat -> Type where
  Zor6'  : a -> b -> Foo6' a b c MZ
  Gor6A'  : b -> Foo6' a b c (MS k)
  Gor6B'  : (k : MyNat) -> b -> Foo6' a b c (MS k)
  Nor6A' : a -> b -> c -> Foo6' a b c n
  -- Nor6B' : a -> (0 _ : b) -> c -> Foo6' a b c n
  Bor6'  : Foo6' a b c n
  Wah6'  : a -> (n : MyNat) -> Foo6' a b c n
  -- Kah6'  : a -> (n : MyNat) -> (0 _ : c) -> Foo6' a b c n
  -- Pah6'  : a -> (n : MyNat) -> MyNat -> (0 _ : c) -> Foo6' a b c n
  -- Rah6'  : a -> (n : MyNat) -> Foo6' a b c n -> MyNat -> (0 _ : c) -> Foo6' a b c n -> Foo6' a b c n
  -- Gah6'  : {1 _ : a} -> (n : MyNat) -> MyNat -> (0 _ : c) -> Foo6' a b c n
  -- ^ another case to consider, what if I'm implicit but M1?
  -- Seems like an error would be appropriate there rather than showing
  -- implicits. Though showing implicits could be a flag in instance generation
  -- I guess.

-- eqImplFoo6'Fun (Wah6' 'c' MZ) (Wah6' 'c' MZ)
-- eqImplFoo6'Fun (Nor6A' {n=MZ} 'c' 'd' 'e')

-- eqImplFoo6Fun (Wah6 {b=Int} {c=String} 'c' (S Z)) (Wah6 'c' (S Z))

data FooN : MyNat -> Type -> Type where
  BorZ : b -> FooN MZ b
  BorS : b -> FooN (MS MZ) b
  BorNA : (k : MyNat) -> b -> FooN n b
  BorNB : (n : MyNat) -> b -> FooN n b

data XXX : Type where
  MkXXX : {a : Int} -> (b : Int) -> XXX

%runElab deriveDecEq Export  `{{MyNat}}
%runElab deriveDecEq Export `{{Foo1}}
%runElab deriveDecEq Export  `{{Foo2}}
%runElab deriveDecEq Private `{{Foo4}}
%runElab deriveDecEq Private `{{Foo5}}
%runElab deriveDecEq Private `{{Foo7}}
%runElab deriveDecEq Private `{{Foo7'}}
-- %runElab deriveDecEq Private `{{FooN}}
-- %runElab deriveDecEq Private `{{Foo6}}
-- %runElab deriveDecEq Export  `{{Foo6'}}
%runElab deriveDecEq Export  `{{XXX}}

-- can check what's generated via
-- :printdef eqImplFoo7'Fun


text:
namespace X
  export
  OneX : Bool -> Bool

namespace Y
  export
  data Foo = OneX

foo : Bool
foo = OneX (id False)