text:
module Toolkit.Data.Rig

import public Decidable.Equality
import public Data.Vect

%default total

public export
data TyRig = None | One | Tonne

public export
noneNotOne : (None = One) -> Void
noneNotOne Refl impossible

public export
noneNotTonne : (None = Tonne) -> Void
noneNotTonne Refl impossible

public export
oneNotTonne : (One = Tonne) -> Void
oneNotTonne Refl impossible

public export
DecEq TyRig where
  decEq None None = Yes Refl
  decEq None One = No noneNotOne
  decEq None Tonne = No noneNotTonne
  decEq One None = No (negEqSym noneNotOne)
  decEq One One = Yes Refl
  decEq One Tonne = No oneNotTonne
  decEq Tonne None = No (negEqSym noneNotTonne)
  decEq Tonne One = No (negEqSym oneNotTonne)
  decEq Tonne Tonne = Yes Refl

public export
plus : TyRig -> TyRig -> TyRig
plus None None = None
plus None One = One
plus None Tonne = Tonne
plus One None = One
plus One One = Tonne
plus One Tonne = Tonne
plus Tonne None = Tonne
plus Tonne One = Tonne
plus Tonne Tonne = Tonne

public export
multiply : TyRig -> TyRig -> TyRig
multiply None None = None
multiply None One = None
multiply None Tonne = None
multiply One None = None
multiply One One = One
multiply One Tonne = Tonne
multiply Tonne None = None
multiply Tonne One = Tonne
multiply Tonne Tonne = Tonne

public export
product : Vect n TyRig -> Vect n TyRig -> Vect n TyRig
product [] [] = []
product (x :: xs) (y :: ys) = multiply x y :: product xs ys

public export
sum : Vect n TyRig -> Vect n TyRig -> Vect n TyRig
sum [] [] = []
sum (x :: xs) (y :: ys) = plus x y :: sum xs ys

ext: idr

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
-- ----------------------------------------------------------------- [ Org.idr ]
-- Module    : Org.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Text.Markup.Edda.Writer.Org

import Data.AVL.Dict

import Effects
import Effect.File
import Effect.Exception

import Text.Markup.Edda.Model

import Text.Markup.Edda.Writer.Common

-- -------------------------------------------------------------- [ Directives ]
%default total
%access private

-- ------------------------------------------------------------ [ Misc Writing ]
rawtag : String -> String -> String
rawtag k v = unwords ["#+" ++ k ++ ":", v]

ntimes : Char -> Nat -> String
ntimes c n = concat $ ntimes' (S n)
  where
    ntimes' : Nat -> List String
    ntimes' Z     = Nil
    ntimes' (S k) = (cast c) :: ntimes' k

attrs : Dict String String -> String
attrs as = rawtag "ATTR" (unwords as')
  where
    as' : List String
    as' = map (\(k,v) => k ++ ":" ++ v) (Dict.toList as)

-- ----------------------------------------------------------- [ Write Inlines ]

mutual

  |||  Convert the list of inlines to their org mode representation.
  export
  inlines : List (Edda INLINE) -> String
  inlines xs = assert_total $ concatMap inline xs

  parens : Char -> Char -> Either String (List (Edda INLINE)) -> String
  parens l r (Left str) = concat [cast l, str,        cast r]
  parens l r (Right ts) = concat [cast l, inlines ts, cast r]

  markup : Char -> Either String (List (Edda INLINE)) -> String
  markup t txt = parens t t txt

  link : String -> List (Edda INLINE) -> String
  link uri Nil  = concat ["[[", uri, "]]"]
  link uri desc = concat ["[[", uri, "][", inlines desc, "]]"]

  inline : Edda INLINE -> String
  inline (Text t) = t
  inline (Sans t) = t
  inline (Scap t) = t
  inline (Mono t) = t
  inline (Verb v)     = markup '=' (Left v)
  inline (Code v)     = markup '~' (Left v)
  inline (Math v)     = markup '$' (Left v)
  inline (Emph t)     = markup '/' (Right t)
  inline (Bold t)     = markup '*' (Right t)
  inline (Strike t)   = markup '+' (Right t)
  inline (Uline t)    = markup '_' (Right t)
  inline (Quote ty t) =
    case ty of
      SQuote => markup '\'' (Right t)
      DQuote => markup '\"' (Right t)
  inline (Parens ty t) =
    case ty of
      Parents  => parens '(' ')' (Right t)
      Brackets => parens '[' ']' (Right t)
      Braces   => parens '{' '}' (Right t)
  inline (Ref url)        = link url Nil
  inline (Hyper uri desc) = link uri desc
  inline (FNote l d) =
    case d of
      Nil => parens '[' ']' (Left (concat ["fn", ":", l, ":"]))
      x   => parens '[' ']' (Right ([Text ("fn:" ++ l ++ ":")] ++ x))
  inline (Cite ty uri) =
    case ty of
      ParenSty => ("[[citep:" ++ uri ++ "]]")
      TextSty  => ("[[citet:" ++ uri ++ "]]")
  inline (MiscPunc c) = (cast c)
  inline Space      = " "
  inline Newline    = "\n"
  inline Tab        = "\t"
  inline LBrace     = "{"
  inline RBrace     = "}"
  inline LParen     = "("
  inline RParen     = ")"
  inline LBrack     = "["
  inline RBrack     = "]"
  inline LAngle     = "<"
  inline RAngle     = ">"
  inline Dollar     = "$"
  inline Colon      = ":"
  inline Semi       = ";"
  inline EnDash     = "--"
  inline EmDash     = "---"
  inline FSlash     = "/"
  inline BSlash     = "\\"
  inline Apostrophe = "'"
  inline SMark      = "\""
  inline Comma      = ","
  inline Plus       = "+"
  inline Ellipsis   = "..."
  inline Hyphen     = "-"
  inline Bang       = "!"
  inline Period     = "."
  inline QMark      = "?"
  inline Hash       = "#"
  inline Equals     = "="
  inline Pipe       = "|"

tag : String -> List (Edda INLINE) -> String
tag k vs = unlines [rawtag k (inlines vs)]

-- ----------------------------------------------------- [ Write Generic Block ]

genblock : (a -> String)
        -> String
        -> Maybe String
        -> List (Edda INLINE)
        -> a
        -> String
genblock f t l c b = unlines
  [ tag "CAPTION" c
  , strFromMaybe (\x => rawtag "NAME" x) l
  , "#+BEGIN_" ++ t
  , f b
  , "#+END_" ++ t
  ]

textblock : String
         -> Maybe String
         -> List (Edda INLINE)
         -> List (Edda INLINE)
         -> String
textblock = genblock (inlines)

verbblock : String
         -> Maybe String
         -> List (Edda INLINE)
         -> String
         -> String
verbblock = genblock (\x => x)

-- ------------------------------------------------------------- [ Write Block ]

itemDef : (List (Edda INLINE), List (Edda INLINE)) -> String
itemDef (k,vs) = unwords ["-", inlines k, "::", inlines vs]

item : String -> List (Edda INLINE) -> String
item m b = unwords [m, inlines b]

||| Convert a block to their org mode representation
export
block : Edda BLOCK -> String
block (HRule) = "-----"
block (Empty) = ""
block (Section lvl label title as body) = assert_total $
    unlines $ unwords [ ntimes '*' lvl
                      , inlines title
                      , fromMaybe "" label
                      , "\n"]
              :: map block body
block (Figure l c as fig) =
    unlines [ tag "CAPTION" c
            , rawtag "NAME" (fromMaybe "EMPTY" l)
            , attrs as
            , inline fig
            , "\n"]
block (DList kvs) = (unlines $ map itemDef kvs)
block (OList bs)  = (unlines $ map (item "1.") bs)
block (BList bs)  = (unlines $ map (item "+")  bs)
block (Para txt) = inlines txt ++ "\n"
block (Listing l c lang langopts as src) =
    unlines [ tag "CAPTION" c
            , rawtag "NAME" $ fromMaybe "MISSING" l
            , attrs as
            , unwords ["#+BEGIN_SRC", fromMaybe "" lang, fromMaybe "" langopts]
            , src
            , "#+END_SRC"
            ]
block (Comment ss)          = verbblock "COMMENT" Nothing Nil ss
block (Equation l eq)       = verbblock "EQUATION" l Nil eq
block (Literal l c src)     = verbblock "EXAMPLE" l c src
block (Quotation l txt)     = textblock "QUOTE" l Nil txt
block (Theorem l c txt)     = textblock "Theorem" l c txt
block (Corollary l c txt)   = textblock "COROLLARY" l c txt
block (Lemma l c txt)       = textblock "LEMMA" l c txt
block (Proposition l c txt) = textblock "PROPOSITION" l c txt
block (Proof l c txt)       = textblock "PROOF" l c txt
block (Definition l c txt)  = textblock "DEFINITION" l c txt
block (Exercise l c txt)    = textblock "EXERCISE" l c txt
block (Note l c txt)        = textblock "NOTE" l c txt
block (Remark l c txt)      = textblock "REMARK" l c txt
block (Problem l c txt)     = textblock "PROBLEM" l c txt
block (Question l c txt)    = textblock "QUESTION" l c txt
block (Solution l c txt)    = textblock "SOLUTION" l c txt
block (Example l c txt)     = textblock "EXAMPLE" l c txt

||| Convert a list of blocks to their org mode representation.
export
blocks : List (Edda BLOCK) -> String
blocks bs = unlines $ map block bs

-- -------------------------------------------------------- [ Write List (String, String) ]

properties : List (Edda INLINE) -> Dict String String -> String
properties title ps = unlines ts
  where
    ps' : List (String, String)
    ps' = toList ps

    ts : List String
    ts = [ rawtag "TITLE"  $ inlines title ]
         ++
         map (\(k,v) => rawtag k v) ps'
         ++
         ["\n"]

-- --------------------------------------------------------------- [ Write Org ]

namespace Doc
  ||| Return a string containing the org mode representation of the document.
  export
  toOrg : Edda DOC -> String
  toOrg (Doc title ps body) = unlines $ (properties title ps :: map block body)

namespace File
  ||| Write the org mode representation of the given document to file.
  export
  toOrgE : String
          -> Edda DOC
          -> Eff (FileOpSuccess) [FILE ()]
  toOrgE fn doc = writeEddaFileE toOrg fn doc

  export
  toOrg : String
          -> Edda DOC
          -> IO (Either FileError ())
  toOrg fn doc = writeEddaFile toOrg fn doc

namespace Snippet
  export
  toOrg : Edda SNIPPET -> String
  toOrg (Snippet snippet prf) with (prf)
    toOrg (Snippet snippet prf) | IsInLine = inlines snippet
    toOrg (Snippet snippet prf) | IsBlock = blocks snippet

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

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
module TyTTP.Core.Stream

import Data.Contravariant

public export
record Subscriber (m : Type -> Type) (e : Type) (a : Type) where
  constructor MkSubscriber
  onNext: a -> m ()
  onSucceded: () -> m ()
  onFailed: e -> m ()

export
Contravariant (Subscriber m e) where
  contramap f subscriber = { onNext := subscriber.onNext . f } subscriber

public export
record Publisher (m : Type -> Type) (e : Type) (a : Type) where
  constructor MkPublisher
  subscribe : Subscriber m e a -> m ()

export
Functor (Publisher m e) where
  map f publisher = MkPublisher $ \s => publisher.subscribe $ contramap f s

export
empty : Publisher m e a
empty = MkPublisher $ \s => s.onSucceded ()

export
fail : e -> Publisher m e a
fail e = MkPublisher $ \s => s.onFailed e

export
singleton : Monad m => a -> Publisher m e a
singleton a = MkPublisher $ \s => s.onNext a >>= s.onSucceded

export
fromList : Monad m => List a -> Publisher m e a
fromList list = MkPublisher $ \s => do
  traverse_ s.onNext list
  s.onSucceded ()

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
module CIL.FFI.Array

import public CIL.FFI
import Data.Vect

%default total

%access public export

IsA Object (TypedArray cilTy elem) where {}

IsA Array (TypedArray cilTy elem) where {}

total
interpCILTy : CILTy -> Type
interpCILTy (CILTyVal "" "int") = Int
interpCILTy (CILTyVal "" "char") = Char
interpCILTy (CILTyVal "" "bool") = Bool
interpCILTy (CILTyRef "" "string") = String
interpCILTy ty = CIL ty

%inline
TypedArrayOf : (elTy : CILTy) -> Type
TypedArrayOf elTy = TypedArray (CILTyArr elTy) (interpCILTy elTy)

%inline
Int32Array : Type
Int32Array = TypedArrayOf CILTyInt32

%inline
ObjectArray : Type
ObjectArray = TypedArrayOf CILTyObj

%inline
StringArray : Type
StringArray = TypedArrayOf CILTyStr

%inline
CharArray : Type
CharArray = TypedArrayOf CILTyChar

%inline
length : TypedArray cilTy elem
      -> {auto fty : FTy FFI_CIL [] (TypedArray cilTy elem -> CIL_IO Int)}
      -> CIL_IO Nat
length {cilTy} {elem} a =
  cast <$> invokeInstance "get_Length" (TypedArray cilTy elem -> CIL_IO Int) a

%inline
get : TypedArray cilTy elem
   -> (index : Int)
   -> {auto fty : FTy FFI_CIL [] (TypedArray cilTy elem -> Int -> CIL_IO elem)}
   -> CIL_IO elem
get {cilTy} {elem} a i =
  invokeInstance "get_Item" (TypedArray cilTy elem -> Int -> CIL_IO elem) a i

%inline
set : TypedArray cilTy elem
   -> (index : Int)
   -> (element : elem)
   -> {auto fty : FTy FFI_CIL [] (TypedArray cilTy elem -> Int -> elem -> CIL_IO ())}
   -> CIL_IO ()
set {cilTy} {elem} a i e =
  invokeInstance "set_Item" (TypedArray cilTy elem -> Int -> elem -> CIL_IO ()) a i e

%inline
newArrayOf : (elTy : CILTy) -> Int -> CIL_IO (TypedArrayOf elTy)
newArrayOf elTy n = new (Int -> CIL_IO (TypedArrayOf elTy)) n

%inline
copyInto : TypedArray cilTy elem
        -> Int
        -> Vect n elem
        -> {auto fty : FTy FFI_CIL [] (TypedArray cilTy elem -> Int -> elem -> CIL_IO ())}
        -> CIL_IO ()
copyInto array i (x :: xs) = set array i x *> copyInto array (i + 1) xs
copyInto _     _ []        = pure ()

%inline
arrayOf : (elTy : CILTy)
       -> Vect n (interpCILTy elTy)
       -> {auto fty : FTy FFI_CIL [] (TypedArrayOf elTy -> Int -> (interpCILTy elTy) -> CIL_IO ())}
       -> CIL_IO (TypedArrayOf elTy)
arrayOf {n} elTy xs = do
  array <- newArrayOf elTy (cast n)
  copyInto array 0 xs
  pure array

namespace Array

  %inline
  foldl : (acc -> elem -> CIL_IO acc)
       -> acc
       -> TypedArray cilTy elem
       -> {auto fty : FTy FFI_CIL [] (TypedArray cilTy elem -> Int -> CIL_IO elem)}
       -> CIL_IO acc
  foldl f init array = loop 0 !(length array) (\acc, i => get array i >>= f acc) init
  where
    loop : Int -> Nat -> (acc -> Int -> CIL_IO acc) -> acc -> CIL_IO acc
    loop i (S n) f acc = f acc i >>= loop (i + 1) n f
    loop _ Z     _ acc = pure acc

  %inline
  foldr : (elem -> acc -> CIL_IO acc)
       -> acc
       -> TypedArray cilTy elem
       -> {auto fty : FTy FFI_CIL [] (TypedArray cilTy elem -> Int -> CIL_IO elem)}
       -> CIL_IO acc
  foldr f init array = loop !(length array) (\acc, i => do e <- get array i; f e acc) init
  where
    loop : Nat -> (acc -> Int -> CIL_IO acc) -> acc -> CIL_IO acc
    loop (S n) f acc = f acc (cast n) >>= loop n f
    loop Z     _ acc = pure acc

  %inline
  toList : TypedArray cilTy elem
       -> {auto fty : FTy FFI_CIL [] (TypedArray cilTy elem -> Int -> CIL_IO elem)}
       -> CIL_IO (List elem)
  toList xs = foldr (\e, acc => pure (e :: acc)) [] xs

  %inline
  forEach_ : TypedArray cilTy elem
          -> (elem -> CIL_IO ())
          -> {auto fty : FTy FFI_CIL [] (TypedArray cilTy elem -> Int -> CIL_IO elem)}
          -> CIL_IO ()
  forEach_ array f = Array.foldl (\_, e => f e) () array

max_stars_repo_name: alaendle/idris-cil

max_issues_repo_name: alaendle/idris-cil

max_forks_repo_name: alaendle/idris-cil


text:
> data Elem : a -> List a -> Type where
>      Here : Elem x (x :: xs)
>      There : Elem x xs -> Elem x (y :: xs)

> interface DecEq a where
>   decEq : (x : a) -> (y : a) -> Dec (x = y)

> zeroNotSucc : Z = (S k) -> Void
> zeroNotSucc Refl impossible

> recNotEq : (k = j -> Void) -> (S k) = (S j) -> Void

> DecEq Nat where
>   decEq Z Z = Yes Refl
>   decEq Z (S k) = No zeroNotSucc
>   decEq (S k) Z = No ?succNotZero
>   decEq (S k) (S j) with (decEq k j)
>     decEq (S j) (S j) | (Yes Refl) = Yes Refl
>     decEq (S k) (S j) | (No contra) = No ?recNotEqLift

> isElem : DecEq a => (x : a) -> (xs : List a) -> Maybe (Elem x xs)
> isElem x [] = Nothing
> isElem x (y :: xs) with (decEq x y)
>   isElem y (y :: xs) | (Yes Refl) = Just Here
>   isElem x (y :: xs) | (No contra) with (isElem x xs)
>     isElem x (y :: xs) | (No contra) | Nothing = Nothing
>     isElem x (y :: xs) | (No contra) | (Just z) = Just (There z)

ext: lidr


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

||| More Quantifiers for Lists, but keeping them out of the prelude so
||| need a new module name.
module Data.List.Predicates

import public Data.List

%default total
%access public export

||| Proof that an element is not in a list.
data NotElem : (elem : ty)
            -> (list : List ty)
            -> Type
  where
    NotHere  : NotElem x []
    NotThere : Eq ty
            => {x,y : ty}
            -> (prf : x /= y = True)
            -> NotElem x xs
            -> NotElem x (y::xs)

||| Proof that the given list is made of unique elements.
data AllDiff : (unique : List ty)
            -> Type
  where
    EmptyCase : AllDiff Nil
    OneCase   : AllDiff [x]
    ManyCase  : NotElem x xs -> AllDiff xs -> AllDiff (x::xs)

||| Proof that `sub_list` is an actual sub list of `list`
data SubList : (sub_list : List ty)
            -> (list     : List ty )
            -> Type
  where
    SubNil : SubList [] xs
    InList : (prf  : Elem x ys)
          -> (rest : SubList xs ys)
          -> SubList (x :: xs) ys

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

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

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

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

max_stars_repo_name: elba/idris-containers

max_issues_repo_name: elba/idris-containers

max_forks_repo_name: elba/idris-containers


text:
-- Idris2

import System.Concurrency

||| Test basic lock/acquire and unlock/release functionality from child thread
main : IO ()
main =
  do m <- makeMutex
     t <- fork $ do mutexAcquire m
                    putStrLn "Child acquired mutex"
                    mutexRelease m
                    putStrLn "Child released mutex"
     threadWait t


text:
module Data.Sign

%access public export

||| A representation of signs for signed datatypes such as `ZZ`
data Sign = Plus | Zero | Minus

opposite : Sign -> Sign
opposite Plus  = Minus
opposite Zero  = Zero
opposite Minus = Plus

multiply : Sign -> Sign -> Sign
multiply Zero  _    = Zero
multiply _     Zero = Zero
multiply Plus  x    = x
multiply Minus x    = opposite x

||| Discover the sign of some type
interface Signed t where
  total sign : t -> Sign

Signed Int where
  sign x with (compare x 0)
    | LT = Minus
    | EQ = Zero
    | GT = Plus

Signed Integer where
  sign x with (compare x 0)
    | LT = Minus
    | EQ = Zero
    | GT = Plus

Signed Double where
  sign x with (compare x 0.0)
    | LT = Minus
    | EQ = Zero
    | GT = Plus


text:
module Baum

-- ein Baum ist entweder ein leeres Blatt
-- oder ein Ast mit einem Wert und zwei Unterbäumen
-- überlege wie der entsprechende Datentyp aussehen könnte

data Baum : (a : Type) -> Type where
  Blatt : Baum a
  Ast : (wert : a) -> (links : Baum a) -> (rechts : Baum a) -> Baum a

-- ähnlich `Elem` für den Vektor wollen wir eine Datenstruktur
-- die "beweist", dass ein Wert in einem Baum ist, indem der Weg
-- dorthin aufgezeigt wird
-- Wie kann das ausehen?

data PfadZu : (wert : a) -> (baum : Baum a) -> Type where
  Hier : PfadZu wert (Ast wert l r)
  IstLinks : PfadZu wert links -> PfadZu wert (Ast y links r)
  IstRechts : PfadZu wert rechts -> PfadZu wert (Ast y l rechts)

-- jetzt müssen wir noch entscheiden, ob wir einen Weg finden können

nichtImBlatt : PfadZu zu Blatt -> Void
nichtImBlatt Hier impossible
nichtImBlatt (IstLinks _) impossible

nowhere : (notRechts : PfadZu zu rechts -> Void) ->
          (notLinks : PfadZu zu links -> Void) ->
          (notHere : (zu = wert) -> Void) ->
          PfadZu zu (Ast wert links rechts) -> Void
nowhere notRechts notLinks notHere Hier = notHere Refl
nowhere notRechts notLinks notHere (IstLinks l) = notLinks l
nowhere notRechts notLinks notHere (IstRechts r) = notRechts r

gibtEsPfad : DecEq a => (zu : a) -> (baum : Baum a) -> Dec (PfadZu zu baum)
gibtEsPfad zu Blatt = No nichtImBlatt
gibtEsPfad zu (Ast wert links rechts) =
  case decEq zu wert of
    Yes Refl => Yes Hier
    No notHere =>
      case gibtEsPfad zu links of
        Yes links => Yes (IstLinks links)
        No notLinks =>
          case gibtEsPfad zu rechts of
            Yes rechts => Yes (IstRechts rechts)
            No notRechts => No (nowhere notRechts notLinks notHere)

----------------------------------------------------------------------
-- Wenn alles passt sollte `zu0 = Yes (IstLinks (IstRechts Hier))` sein!

beispiel : Baum Int
beispiel = Ast 2 (Ast 1 Blatt (Ast 0 Blatt Blatt)) (Ast 3 Blatt Blatt)

zu0 : Dec (PfadZu 0 Baum.beispiel)
zu0 = gibtEsPfad _ _


text:
> module Nat.Operations

> import Nat.Predicates

> %default total
> %access public export
> %hide (-)

Predecessor:

> pred : (n : Nat) -> Z `LT` n -> Nat
> pred  Z    prf = absurd prf
> pred (S m) _   = m

Infix minus:

> (-) : Nat -> Nat -> Nat
> (-) = minus

Division:

> -- quotient : (m : Nat) -> (d : Nat) -> d `Divisor` m -> Nat
> -- quotient _ _ (Evidence q _) = q

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Text.WebIDL.Codegen.Definitions

import Data.List
import Data.List.Elem
import Data.SOP
import Data.String
import Text.WebIDL.Codegen.Args
import Text.WebIDL.Codegen.Enum
import Text.WebIDL.Codegen.Members
import Text.WebIDL.Codegen.Rules
import Text.WebIDL.Codegen.Types
import public Text.WebIDL.Codegen.Util

--------------------------------------------------------------------------------
--          Imports
--------------------------------------------------------------------------------

defImports : CGDomain -> String
defImports d = #"""
               import JS
               import Web.Internal.\#{d.name}Prim
               import Web.Internal.Types
               """#

typeImports : String
typeImports = "import JS"

--------------------------------------------------------------------------------
--          Data Declarations
--------------------------------------------------------------------------------

extern : CGDomain -> String
extern d = fastUnlines [ section "Interfaces" $ exts ext name d.ifaces
                       , section "Dictionaries" $ exts extNoCast name d.dicts
                       , section "Mixins" $ exts extNoCast name d.mixins
                       , section "Callbacks" $ exts extNoCast name d.callbacks
                       ]
  where extNoCast : String -> String
        extNoCast s = #"""
                      export data \#{s} : Type where [external]

                      export
                      ToFFI \#{s} \#{s} where toFFI = id

                      export
                      FromFFI \#{s} \#{s} where fromFFI = Just
                      """#

        ext : String -> String
        ext s = extNoCast s ++ "\n\n" ++
                #"""
                export
                SafeCast \#{s} where
                  safeCast = unsafeCastOnPrototypeName "\#{s}"
                """#

        exts :  (f : String -> String)
             -> (a -> Identifier)
             -> List a
             -> List String
        exts f g = map (("\n" ++) . f) . sort . map (value . g)

--------------------------------------------------------------------------------
--          CallbackInterfaces
--------------------------------------------------------------------------------

cbacks : (CGCallback -> List String) -> CGDomain -> String
cbacks f = section "Callbacks" . map ns . sortBy (comparing name) . callbacks
  where ns : CGCallback -> String
        ns i = namespaced i.name (f i)

callbacks : CGDomain -> String
callbacks = cbacks go
  where go : CGCallback -> List String
        go cb = callback cb :: constants cb.constants

primCallbacks : CGDomain -> String
primCallbacks = cbacks (pure . primCallback)

--------------------------------------------------------------------------------
--          JSType
--------------------------------------------------------------------------------

jsTypes : List CGDomain -> String
jsTypes ds =
  let ifs  = sortBy (comparing name) (ds >>= ifaces)
      dics = sortBy (comparing name) (ds >>= dicts)
   in section "Inheritance" $
        map (\i => jsType i.name i.super) ifs ++
        map (\d => jsType d.name d.super) dics

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

ifaces' : (CGIface -> List String) -> CGDomain -> String
ifaces' f = section "Interfaces" . map ns . sortBy (comparing name) . ifaces
  where ns : CGIface -> String
        ns i = namespaced i.name (f i)

ifaces : CGDomain -> String
ifaces = ifaces' $ \(MkIface n s cs fs) => constants cs ++ functions fs

primIfaces : CGDomain -> String
primIfaces = ifaces' (primFunctions . functions)

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

dicts' : (CGDict -> List String) -> CGDomain -> String
dicts' f = section "Dictionaries" . map ns . sortBy (comparing name) . dicts
  where ns : CGDict -> String
        ns d = namespaced d.name (f d)

dicts : CGDomain -> String
dicts = dicts' $ \(MkDict n s fs) => functions fs

primDicts : CGDomain -> String
primDicts = dicts' (primFunctions . functions)

--------------------------------------------------------------------------------
--          Mixins
--------------------------------------------------------------------------------

mixins' : (CGMixin -> List String) -> CGDomain -> String
mixins' f = section "Mixins" . map ns . sortBy (comparing name) . mixins
  where ns : CGMixin -> String
        ns m = namespaced m.name (f m)

mixins : CGDomain -> String
mixins = mixins' $ \(MkMixin n cs fs) => constants cs ++ functions fs

primMixins : CGDomain -> String
primMixins = mixins' (primFunctions . functions)

--------------------------------------------------------------------------------
--          Typedefs
--------------------------------------------------------------------------------

export
typedefs : List CGDomain -> String
typedefs ds =
      #"""
      module Web.Internal.Types

      import JS
      import public Web.Internal.AnimationTypes as Types
      import public Web.Internal.ClipboardTypes as Types
      import public Web.Internal.CssTypes as Types
      import public Web.Internal.DomTypes as Types
      import public Web.Internal.FetchTypes as Types
      import public Web.Internal.FileTypes as Types
      import public Web.Internal.GeometryTypes as Types
      import public Web.Internal.HtmlTypes as Types
      import public Web.Internal.MediasourceTypes as Types
      import public Web.Internal.MediastreamTypes as Types
      import public Web.Internal.PermissionsTypes as Types
      import public Web.Internal.ServiceworkerTypes as Types
      import public Web.Internal.StreamsTypes as Types
      import public Web.Internal.SvgTypes as Types
      import public Web.Internal.UIEventsTypes as Types
      import public Web.Internal.UrlTypes as Types
      import public Web.Internal.VisibilityTypes as Types
      import public Web.Internal.WebglTypes as Types
      import public Web.Internal.WebidlTypes as Types
      import public Web.Internal.XhrTypes as Types

      %default total
      """# ++ "\n\n" ++ jsTypes ds

--------------------------------------------------------------------------------
--          Codegen
--------------------------------------------------------------------------------
--
export
types : CGDomain -> String
types d =
  #"""
  module Web.Internal.\#{d.name}Types

  \#{typeImports}

  %default total

  \#{enums d.enums}
  \#{extern d}
  """#

export
primitives : CGDomain -> String
primitives d =
  #"""
  module Web.Internal.\#{d.name}Prim

  import JS
  import Web.Internal.Types

  %default total

  \#{primIfaces d}
  \#{primMixins d}
  \#{primDicts d}
  \#{primCallbacks d}
  """#

export
definitions : CGDomain -> String
definitions d =
  #"""
  module Web.Raw.\#{d.name}

  \#{defImports d}

  %default total

  \#{Definitions.ifaces d}
  \#{Definitions.mixins d}
  \#{Definitions.dicts d}
  \#{Definitions.callbacks d}
  """#


text:
-- --------------------------------------------------------------- [ Clock.idr ]
-- Module  : Data.Time.Clock
--
-- License : This code is distributed under the MIT license. See the
--           file LICENSE in the root directory for its full text.
-- --------------------------------------------------------------------- [ EOH ]
module Data.Time.Clock

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

max_stars_repo_name: yurrriq/idris-time

max_issues_repo_name: yurrriq/idris-time

max_forks_repo_name: yurrriq/idris-time


text:
module Dec2

import Data.Vect
import Data.String
import Utils

dec2a : (Ord a, Neg a) => List (List a) -> a
dec2a xs = foldl f 0 xs where
  g : List a -> a
  g [] = 0
  g (x :: []) = 0
  g (x :: (y :: ys)) = let xs = fromList (y :: ys) in
                           max' (x :: xs) - min' (x :: xs)

  f : a -> List a -> a
  f x xs = x + g xs

divEvenly : (Integral a, Eq a) => (dividend : a) -> (divisor : a) -> Maybe a
divEvenly dividend divisor = do divisor' <- case divisor of
                                              0 => Nothing
                                              _ => Just divisor
                                if mod dividend divisor' == 0
                                then Just (div dividend divisor')
                                else Nothing

reduceAllPairs : Monoid a => (a -> a -> Maybe a) -> Vect (S n) a -> Maybe a
reduceAllPairs f xs = let ys = map (uncurry f) $ concat $ allPairs xs in
                          foldl (<+>) neutral ys

dec2b : (Integral a, Eq a, Monoid a) => List (List a) -> a
dec2b xs = foldl f 0 xs where
  g : List a -> a
  g [] = 0
  g (x :: xs) = fromMaybe 0 $ reduceAllPairs divEvenly (x :: fromList xs)

  f : a -> List a -> a
  f x xs = x + g xs

Semigroup Int where
  (<+>) = (+)

Monoid Int where
  neutral = 0

input : String
input = """278	1689	250	1512	1792	1974	175	1639	235	1635	1690	1947	810	224	928	859
160	50	55	81	68	130	145	21	211	136	119	78	174	155	149	72
4284	185	4499	273	4750	4620	4779	4669	2333	231	416	1603	197	922	5149	2993
120	124	104	1015	1467	110	299	320	1516	137	1473	132	1229	1329	1430	392
257	234	3409	2914	2993	3291	368	284	259	3445	245	1400	3276	339	2207	233
1259	78	811	99	2295	1628	3264	2616	116	3069	2622	1696	1457	1532	268	82
868	619	139	522	168	872	176	160	1010	200	974	1008	1139	552	510	1083
1982	224	3003	234	212	1293	1453	3359	326	3627	3276	3347	1438	2910	248	2512
4964	527	5108	4742	4282	4561	4070	3540	196	228	3639	4848	152	1174	5005	202
1381	1480	116	435	980	1022	155	1452	1372	121	128	869	1043	826	1398	137
2067	2153	622	1479	2405	1134	2160	1057	819	99	106	1628	1538	108	112	1732
4535	2729	4960	241	4372	3960	248	267	230	5083	827	1843	3488	4762	2294	3932
3245	190	2249	2812	2620	2743	2209	465	139	2757	203	2832	2454	177	2799	2278
1308	797	498	791	1312	99	1402	1332	521	1354	1339	101	367	1333	111	92
149	4140	112	3748	148	815	4261	138	1422	2670	32	334	2029	4750	4472	2010
114	605	94	136	96	167	553	395	164	159	284	104	530	551	544	18"""

dec2 : String -> Maybe (Int, Int)
dec2 str = map (\xs => (dec2a xs, dec2b xs)) $ f str where
  g  : (Neg a) => String -> Maybe (List a)
  g str = traverse parseInteger $ words str

  f : (Neg a) => String -> Maybe (List (List a))
  f str = traverse g $ lines str


text:
-- ---------------------------------------------------------------- [ YAML.idr ]
-- Module    : YAML.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Config.Test.YAML

import Config.YAML

import Lightyear.Testing

%access export
-- ------------------------------------------------------------------- [ Begin ]

yamlTest1 : TestReport
yamlTest1 = parseTest "YAML Test 1"
                      parseYAMLDoc
                      """%YAML 1.2
---
receipt: Oz Ware Purchase Invoice
date: "2012 08 06"
customer: {given: Dorothy, family: Gale}
items: {partno:   A4786, descrip:   Water Bucket Filled}
items: { partno:   E1628,
      descrip:   High Heeled Ruby Slippers,
      size:      8,
      price:     100.27,
      quantity:  1}
billto: { city: East Centerville, state: KS}
...
    """

yamlTest2 : TestReport
yamlTest2 = parseTestNot "YAML Test 2"
                         parseYAMLDoc
                         """# sequencer protocols for Laser eye surgery
---
- step:  &id001                  # defines anchor label &id001
    instrument:      Lasik 2000
    pulseEnergy:     5.4
    pulseDuration:   12
    repetition:      1000
    spotSize:        1mm

- step: &id002
    instrument:      Lasik 2000
    pulseEnergy:     5.0
    pulseDuration:   10
    repetition:      500
    spotSize:        2mm

- step: *id001                   # refers to the first step (with anchor &id001)
- step: *id002                   # refers to the second step
- step: *id001
- step: *id002
"""

yamlTest3 : TestReport
yamlTest3 = parseTest "YAML Test 3"
                      parseYAMLDoc
                      """%YAML 1.2
---
pattern: {problem: file.p, solution: file.p}
pattern: {problem: file.p, solution: file.p}
...
    """

runTests : IO ()
runTests = Testing.runTests [yamlTest1, yamlTest2, yamlTest3]
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-config

max_issues_repo_name: jfdm/idris-config

max_forks_repo_name: jfdm/idris-config


text:
module TyTTP.HTTP.Consumer

import Control.Monad.Trans
import Control.Monad.Either
import Data.Buffer
import Data.List
import Data.List.Quantifiers
import TyTTP
import TyTTP.HTTP
import TyTTP.HTTP.Combinators

public export
interface Accept t where
  contentType : (ty : Type) -> { auto p : ty = t } -> List String

public export
data IsAccept : (t : Type) -> Type where
  ItIsAccept : Accept t => IsAccept t

public export
ConsumerError : Type
ConsumerError = String

public export
interface Accept t => Consumer a t where
  consumeRaw : (ty : Type) -> { auto p : ty = t } -> (ct : String) -> (raw : Buffer) -> Either ConsumerError a

public export
data IsConsumer : (a : Type) -> (t : Type) -> Type where
  ItIsConsumer : Consumer a t => IsConsumer a t

consumePayload :
  (t : Type)
  -> (isConsumer : IsConsumer a t)
  -> (ct : String)
  -> (raw : Buffer)
  -> Either ConsumerError a
consumePayload t ItIsConsumer ct raw =
  consumeRaw t ct raw

safeConsume :
  Error e
  => MonadTrans m
  => Alternative (m (Promise e IO))
  => HasContentType h1
  => (list: List Type)
  -> (areAccepts : All IsAccept list)
  -> (areConsumers : All (IsConsumer a) list)
  -> (ct : String)
  -> (
    Step Method u h1 s h2 (Either ConsumerError a) b
    -> Promise e IO $ Step Method u' h1' s' h2' a' b'
  )
  -> Step Method u h1 s h2 (Publisher IO e Buffer) b
  -> m (Promise e IO) $
     Step Method u' h1' s' h2' (Publisher IO e Buffer) b'
safeConsume [] _ _ _ _ _ = empty
safeConsume (t::ts) (ItIsAccept::as) (c::cs) ct handler step =
  if elem ct (contentType t)
  then lift $ flip unsafeConsumeBody step $ \s => MkPromise $ \cb => do
          let raw = s.request.body
              result = handler $ { request.body := consumePayload t c ct raw } s
          result.continuation $ MkCallbacks
            { onSucceded = \r => cb.onSucceded $ { request.body := singleton raw } r
            , onFailed = \err => cb.onFailed err }
  else safeConsume ts as cs ct handler step

export
consumes :
  Error e
  => MonadTrans m
  => Alternative (m (Promise e IO))
  => HasContentType h1
  => (list: List Type)
  -> {auto isNonEmpty : NonEmpty list}
  -> {auto areAccepts : All IsAccept list}
  -> {auto areConsumers : All (IsConsumer a) list}
  -> (
    Step Method u h1 s h2 (Either ConsumerError a) b
    -> Promise e IO $ Step Method u' h1' s' h2' a' b'
  )
  -> Step Method u h1 s h2 (Publisher IO e Buffer) b
  -> m (Promise e IO) $
     Step Method u' h1' s' h2' (Publisher IO e Buffer) b'
consumes list {isNonEmpty} {areAccepts} {areConsumers} handler step = do
  let Just ct = getContentType step.request.headers
    | _ => empty

  safeConsume list areAccepts areConsumers ct handler step

export
consumes' :
  Error e
  => MonadTrans m
  => Alternative (m (Promise e IO))
  => HasContentType h1
  => (list: List Type)
  -> {auto isNonEmpty : NonEmpty list}
  -> {auto areAccepts : All IsAccept list}
  -> {auto areConsumers : All (IsConsumer a) list}
  -> (
    Step Method u h1 s h2 ConsumerError b
    -> Promise e IO $ Step Method u' h1' s' h2' a' b'
  )
  -> (
    Step Method u h1 s h2 a b
    -> Promise e IO $ Step Method u' h1' s' h2' a'' b'
  )
  -> Step Method u h1 s h2 (Publisher IO e Buffer) b
  -> m (Promise e IO) $
     Step Method u' h1' s' h2' (Publisher IO e Buffer) b'
consumes' list {isNonEmpty} {areAccepts} {areConsumers} errHandler handler step =
  let handler' :
        Step Method u h1 s h2 (Either ConsumerError a) b
        -> Promise e IO $ Step Method u' h1' s' h2' () b'
      handler' s =
        case s.request.body of
          Right r => do
            result <- handler $ { request.body := r } s
            pure $ { request.body := () } result
          Left  l => do
            result <- errHandler $ { request.body := l } s
            pure $ { request.body := () } result
  in consumes list handler' step


text:
||| A telescope is the variable context in a dependently typed program.
||| Dependent types with free varialbes  are really only well-defined in a telescope.
|||
||| A segment of a telescope is a tuple of types in that
||| telescope. These are usually implicit in formal developments, but
||| seem to be crucial to get a compositional account. Here we use
||| them to get 'n-ary dependent function' (compare with `Data.Fun`
||| and `Data.Rel`).
|||
||| I've learned this from Conor McBride on an SPLV'19 bus ride.
||| A literary reference would be welcome. This paper is a start:
||| Unifiers as Equivalences: Proof-Relevant Unification of Dependently Typed Data.
||| Jesper Cockx, Dominique Devriese, Frank Piessens, ICFP'16.
||| but they don't seem to have segments and their left action on contexts.
module Data.Telescope

import public Data.Telescope.Telescope
import public Data.Telescope.Segment
import public Data.Telescope.SimpleFun
import public Data.Telescope.Fun
import public Data.Telescope.Congruence


text:
module Replica.Command

import Data.List
import Data.List1
import Data.List.AtIndex
import Data.OpenUnion

import Replica.Option.Types
import Replica.Other.Decorated
import Replica.Other.Validation

import public Replica.Command.Info
import public Replica.Command.Run
import public Replica.Command.Help

public export
Commands : Type
Commands = Union Prelude.id [RunCommand, InfoCommand, Help]

export
parseArgs : List1 String -> ParseResult Commands
parseArgs xs = foldl1 go $ toList1 $ map (flip apply xs)
  [ map inj . parseRun
  , map inj . parseInfo
  , map inj . parseHelp
  ]
  where
    go : ParseResult Commands -> ParseResult Commands -> ParseResult Commands
    go (Done x) _ = Done x
    go _ (Done x) = Done x
    go (InvalidMix x) y = InvalidMix x
    go (InvalidOption ys) y = y

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica


text:
||| A way to capture optional restrictions on values in both the Schema and the Values themselves.
module Data.Schema.Restricted

%default total

namespace Schema

  public export
  data Restriction : (type : Type) -> Type where
    RestrictedNot : Restriction type
    Restricted : (predicate : type -> Type) -> Restriction type

namespace Data

  public export
  data Restriction : (type : Type)
                  -> (mres  : Schema.Restriction type)
                  -> (value : type)
                           -> Type
    where
      RestrictedNot : Restriction type RestrictedNot value

      Restricted : (prf : predicate value)
                       -> Restriction type (Restricted predicate) value

-- [ EOF ]

max_stars_repo_name: jfdm/idris-shaped

max_issues_repo_name: jfdm/idris-shaped

max_forks_repo_name: jfdm/idris-shaped


text:
data Expr num = Val num
              | Add (Expr num) (Expr num)
              | Sub (Expr num) (Expr num)
              | Mul (Expr num) (Expr num)
              | Div (Expr num) (Expr num)
              | Absolute (Expr num)

eval : (Neg num, Abs num, Integral num) => Expr num -> num
eval (Val x) = x
eval (Add x y) = eval x + eval y
eval (Sub x y) = eval x - eval y
eval (Mul x y) = eval x * eval y
eval (Div x y) = eval x `div` eval y
eval (Absolute x) = abs (eval x)

Num ty => Num (Expr ty) where
    (+) = Add
    (*) = Mul
    fromInteger = Val . fromInteger

Neg ty => Neg (Expr ty) where
    negate x = 0 - x
    (-) = Sub

Show ty => Show (Expr ty) where
    show (Val x) = show x
    show (Add x y) = "(" ++ show x ++ " + " ++ show y ++ ")"
    show (Sub x y) = "(" ++ show x ++ " - " ++ show y ++ ")"
    show (Mul x y) = "(" ++ show x ++ " * " ++ show y ++ ")"
    show (Div x y) = "(" ++ show x ++ " / " ++ show y ++ ")"
    show (Absolute x) = "|" ++ show x ++ "|"

(Neg ty, Integral ty, Abs ty, Eq ty) => Eq (Expr ty) where
    (==) x y = eval x == eval y

(Neg ty, Integral ty, Abs ty) => Cast (Expr ty) ty where
     cast expr = eval expr

Functor Expr where
    map f (Val x) = Val $ f x
    map f (Add x y) = Add (map f x) (map f y)
    map f (Sub x y) = Sub (map f x) (map f y)
    map f (Mul x y) = Mul (map f x) (map f y)
    map f (Div x y) = Div (map f x) (map f y)
    map f (Absolute x) = Absolute (map f x)


text:
module Minecraft.Base.PreClassic.Air.Block

import public Minecraft.Base.PreClassic.Air
import public Minecraft.Core.Block.Export
import public Minecraft.Data.Type.Vtbl

%default total

namespace Export
  public export %hint airBlock : Block Air.Block
  public export %hint airVtbl  : Vtbl  Air.Block

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
-- -------------------------------------------------------------- [ Parser.idr ]
-- Description : A simple parser for command options.
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Commons.Options.ArgParse.Parser

import Text.Lexer
import Text.Parser

import Commons.Text.Lexer.Run
import public Commons.Text.Parser.Run

import Commons.Options.ArgParse.Lexer
import Commons.Options.ArgParse.Parser.API
import Commons.Options.ArgParse.Model

%access private

-- ----------------------------------------------------------------- [ Parsers ]

flagLong : Rule Token Arg
flagLong = do
  l <- longFlag
  pure $ Flag l

flagShort : Rule Token Arg
flagShort = do
   s <- shortFlag
   pure $ Flag s

kvLong : Rule Token Arg
kvLong = do
    key <- longFlag
    equals
    value <- (arg <|> quoted)
    pure $ KeyValue key value

kvShort : Rule Token Arg
kvShort = do
    k <- shortFlag
    v <- (arg <|> quoted)
    pure $ KeyValue k v

options : Rule Token Arg
options = kvShort <|> kvLong <|> flagShort <|> flagLong <|> (do fs <- arg; pure $ File fs)

args : RuleEmpty Token $ List Arg
args = do
    os <- many options
    pure $ os

export
parseArgsStr : (str  : String)
            -> Either (Run.ParseError Token) (List Arg)
parseArgsStr str = parseString ArgParseLexer args str

export
parseArgsFile :(fname : String)
            -> IO (Either (Run.ParseError Token) (List Arg))
parseArgsFile fn = parseFile ArgParseLexer args fn

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

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module TyTTP.Core.Request

public export
record Request m u h a where
  constructor MkRequest
  method : m
  url : u
  headers : h
  body : a

export
Functor (Request m u h) where
  map f req = { body $= f } req


text:
module Network.Curl.Prim

import Network.Curl.Types

import public Network.Curl.Prim.Easy
import public Network.Curl.Prim.Global
import public Network.Curl.Prim.Mime
import public Network.Curl.Prim.Multi
import public Network.Curl.Prim.Other


text:
module BigStep

-- Relation 'BigStep' for fully reducing terms
-- in the simply-typed lambda calculus to values.

import Term
import Subst

%default total
%access public export

-----------------------------------------------------------------------
-- Begin: BIG-STEP EVALUATION RELATION FOR TERMS IN THE LAMBDA CALCULUS

-- The relation 'BigStep' defines evaluation of terms in the lambda
-- calculus following big-step semantics.
--
-- Big-step semantics fully evaluates terms to values.
-- (A proof of this statement appears below.)
data BigStep : Term [] t -> (y: Term [] t) -> Type where
  BStValue    : (v : Value e) -> BigStep e e
  --
  BStApp      : BigStep e1 (TAbs e1') ->
                BigStep e2 e2' ->
                BigStep (subst e2' FZ e1') e ->
                BigStep (TApp e1 e2) e
  --
  BStFix      : BigStep e (TAbs e') ->
                BigStep (subst (TFix (TAbs e')) FZ e') e'' ->
                BigStep (TFix e) e''
  --
  BStSucc     : BigStep e e' ->
                BigStep (TSucc e) (TSucc e')
  --
  BStPredZero : BigStep e TZero ->
                BigStep (TPred e) TZero
  --
  BStPredSucc : BigStep e (TSucc e') ->
                BigStep (TPred e) e'
  --
  BStIfzZero  : BigStep e1 TZero ->
                BigStep e2 e ->
                BigStep (TIfz e1 e2 _) e
  --
  BStIfzSucc  : BigStep e1 (TSucc _) ->
                BigStep e3 e ->
                BigStep (TIfz e1 _ e3) e

bigStepFst : {e : Term [] t} -> BigStep e _ -> Term [] t
bigStepFst {e = e} _ = e

bigStepSnd : {e : Term [] t} -> BigStep _ e -> Term [] t
bigStepSnd {e = e} _ = e

bigStepValue : BigStep _ e -> Value e
bigStepValue (BStValue v)     = v
bigStepValue (BStApp _ _ z)   = bigStepValue z
bigStepValue (BStFix _ z)     = bigStepValue z
bigStepValue (BStSucc z)      = VSucc (bigStepValue z)
bigStepValue (BStPredZero _)  = VZero
bigStepValue (BStPredSucc z)  = case bigStepValue z of
                                    VZero impossible
                                    VSucc v => v
bigStepValue (BStIfzZero _ z) = bigStepValue z
bigStepValue (BStIfzSucc _ z) = bigStepValue z

-- End: BIG-STEP EVALUATION RELATION FOR TERMS IN THE LAMBDA CALCULUS
---------------------------------------------------------------------

---------------------------------------------------------
-- Begin: DIVERGENCE OF TERM 'Subst.omega' UNDER BIG-STEP

-- The following straightforward approach to proving
-- that 'omega' diverges does not pass Idris' totality
-- checker because of the rewriting of 'bst' in the
-- induction step:
--
-- divergenceOmega : BigStep Subst.omega e -> Void
-- divergenceOmega {e = _} (BStValue v) = case v of
--                                             VZero     impossible
--                                             (VSucc _) impossible
--                                             VAbs      impossible
-- divergenceOmega {e = e} (BStFix (BStValue v) bst) =
--   let bst' = replace {P = \x => BigStep x e} substOmega bst
--   in divergenceOmega bst'

-- To prove that 'omega' diverges under big-step semantics,
-- an indexed version of the 'BigStep' relation is introduced:
data BigStepN : Nat -> Term [] t -> (y: Term [] t) -> Type where
  BStValueN    : (v : Value e) -> BigStepN Z e e
  --
  BStAppN      : BigStepN k e1 (TAbs e1') ->
                 BigStepN m e2 e2' ->
                 BigStepN n (subst e2' FZ e1') e ->
                 BigStepN (S $ k+m+n) (TApp e1 e2) e
  --
  BStFixN      : BigStepN m e (TAbs e') ->
                 BigStepN n (subst (TFix (TAbs e')) FZ e') e'' ->
                 BigStepN (S $ m+n) (TFix e) e''
  --
  BStSuccN     : BigStepN n e e' ->
                 BigStepN (S n) (TSucc e) (TSucc e')
  --
  BStPredZeroN : BigStepN n e TZero ->
                 BigStepN (S n) (TPred e) TZero
  --
  BStPredSuccN : BigStepN n e (TSucc e') ->
                 BigStepN (S n) (TPred e) e'
  --
  BStIfzZeroN  : BigStepN m e1 TZero ->
                 BigStepN n e2 e ->
                 BigStepN (S $ m+n) (TIfz e1 e2 _) e
  --
  BStIfzSuccN  : BigStepN m e1 (TSucc _) ->
                 BigStepN n e3 e ->
                 BigStepN (S $ m+n) (TIfz e1 _ e3) e

bigStepToN : BigStep e1 e2 -> (n : Nat ** BigStepN n e1 e2)
bigStepToN (BStValue v) = (Z ** BStValueN v)
--
bigStepToN (BStApp bst1 bst2 bst3) = let (n1 ** bstn1) = bigStepToN bst1
                                         (n2 ** bstn2) = bigStepToN bst2
                                         (n3 ** bstn3) = bigStepToN bst3
                                     in ((S $ n1+n2+n3) ** BStAppN bstn1 bstn2 bstn3)
--
bigStepToN (BStFix bst1 bst2) = let (n1 ** bstn1) = bigStepToN bst1
                                    (n2 ** bstn2) = bigStepToN bst2
                                in ((S $ n1+n2) ** BStFixN bstn1 bstn2)
--
bigStepToN (BStSucc bst) = let (n ** bstn) = bigStepToN bst
                           in ((S n) ** BStSuccN bstn)
--
bigStepToN (BStPredZero bst) = let (n ** bstn) = bigStepToN bst
                               in ((S n) ** BStPredZeroN bstn)
--
bigStepToN (BStPredSucc bst) = let (n ** bstn) = bigStepToN bst
                               in ((S n) ** BStPredSuccN bstn)
--
bigStepToN (BStIfzZero bst1 bst2) = let (n1 ** bstn1) = bigStepToN bst1
                                        (n2 ** bstn2) = bigStepToN bst2
                                    in ((S $ n1+n2) ** BStIfzZeroN bstn1 bstn2)
--
bigStepToN (BStIfzSucc bst1 bst2) = let (n1 ** bstn1) = bigStepToN bst1
                                        (n2 ** bstn2) = bigStepToN bst2
                                    in ((S $ n1+n2) ** BStIfzSuccN bstn1 bstn2)

bigStepFromN : BigStepN n e1 e2 -> BigStep e1 e2
bigStepFromN (BStValueN v) = BStValue v
--
bigStepFromN (BStAppN bstn1 bstn2 bstn3) = let bst1 = bigStepFromN bstn1
                                               bst2 = bigStepFromN bstn2
                                               bst3 = bigStepFromN bstn3
                                           in BStApp bst1 bst2 bst3
--
bigStepFromN (BStFixN bstn1 bstn2) = let bst1 = bigStepFromN bstn1
                                         bst2 = bigStepFromN bstn2
                                     in BStFix bst1 bst2
--
bigStepFromN (BStSuccN bstn) = let bst = bigStepFromN bstn
                               in BStSucc bst
--
bigStepFromN (BStPredZeroN bstn) = let bst = bigStepFromN bstn
                                   in BStPredZero bst
--
bigStepFromN (BStPredSuccN bstn) = let bst = bigStepFromN bstn
                                   in BStPredSucc bst
--
bigStepFromN (BStIfzZeroN bstn1 bstn2) = let bst1 = bigStepFromN bstn1
                                             bst2 = bigStepFromN bstn2
                                         in BStIfzZero bst1 bst2
--
bigStepFromN (BStIfzSuccN bstn1 bstn2) = let bst1 = bigStepFromN bstn1
                                             bst2 = bigStepFromN bstn2
                                         in BStIfzSucc bst1 bst2

-- Divergence of 'omega' under the indexed version of big-step semantics:
divergenceOmega' : {e : Term [] TyNat} -> (n : Nat) -> BigStepN n Subst.omega e -> Void
divergenceOmega' Z (BStValueN v) = case v of
                                        VZero     impossible
                                        (VSucc _) impossible
                                        VAbs      impossible
divergenceOmega' {e} (S n) bstn = case bstn of
  (BStFixN (BStValueN v) bstn2) => let bstn2' = replace {P = \x => BigStepN n x e} substOmega bstn2
                                   in divergenceOmega' n bstn2'

divergenceOmega : BigStep Subst.omega e -> Void
divergenceOmega bst = let (n ** bstn) = bigStepToN bst
                      in divergenceOmega' n bstn

-- End: DIVERGENCE OF TERM 'Subst.omega' UNDER BIG-STEP
-------------------------------------------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
module Rationals

data NotZero : Integer -> Type where --Proof that a number is not zero, needed to construct Q
  OneNotZero : NotZero 1
  NegativeNotZero : ( n: Integer ) -> NotZero n -> NotZero (-n)
  PositiveNotZero : ( m: Integer ) -> LTE 1 (fromIntegerNat m)  -> NotZero m

rational : (p: Nat) -> (q: Integer) -> NotZero q -> (Integer, Integer)
rational Z q x = (toIntegerNat(0), q)
rational (S k) q x = (toIntegerNat(S k), q)

SecondPart : (Integer, Integer) -> Integer
SecondPart x = (snd x)

InclusionMap : (n : Nat) -> (Integer, Integer) --Includes the naturals in Q
InclusionMap n = rational n 1 OneNotZero

AddRationals : (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer) --Need to implement proof checking for nonzero denominators
AddRationals x y = ((fst x)*(snd y) + (snd x)*(fst y), (snd x)*(snd y))

MultiplyRationals : (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer) --Need to implement proof checking for nonzero denominators
MultiplyRationals  x y = ((fst x)*(fst y), (snd x)*(snd y))

--Need to create multiplicative inverses of rationals as well

--A GCD function with proof that it is the GCD would be useful to reduce rationals into simplified form

test : Nat
test = fct 3


text:
import Data.Vect

-- Exercise 1
createEmpties : Vect n (Vect 0 elem)
createEmpties = replicate _ []

{-
transposeHelper : (x : Vect n elem)
               -> (xTrans : Vect n (Vect k elem))
               -> Vect n (Vect (S k) elem)
transposeHelper [] [] = []
transposeHelper (x :: xs) (y :: ys) = (x :: y) :: transposeHelper xs ys
-}

transposeMat : Vect m (Vect n elem) -> Vect n (Vect m elem)
transposeMat [] = createEmpties
transposeMat (x :: xs) = let xTrans = transposeMat xs in
                             zipWith (::) x xTrans

-- Exercise 2
addMatrix : Num a => Vect n (Vect m a) -> Vect n (Vect m a) -> Vect n (Vect m a)
addMatrix [] [] = []
addMatrix (x :: xs) (y :: ys) = zipWith (+) x y :: addMatrix xs ys

addMatrix' : Num a => Vect n (Vect m a) -> Vect n (Vect m a) -> Vect n (Vect m a)
addMatrix' mat1 mat2 = zipWith (zipWith (+)) mat1 mat2

(+) : Num a => Vect n (Vect m a) -> Vect n (Vect m a) -> Vect n (Vect m a)
(+) = addMatrix

-- Exercise 3
multVecs : Num a => (xs : Vect n a) -> (ys : Vect n a) -> a
multVecs xs ys = sum (zipWith (*) xs ys)

makeRow : Num a => (x : Vect n a)
                -> (ysTrans : Vect p (Vect n a))
                -> Vect p a
makeRow x [] = []
makeRow x (y :: xs) = multVecs x y :: makeRow x xs

multMatrixHelper : Num a => (xs : Vect m (Vect n a))
                         -> (ysTrans : Vect p (Vect n a))
                         -> Vect m (Vect p a)
multMatrixHelper [] ysTrans = []
multMatrixHelper (x :: xs) ysTrans
     = makeRow x ysTrans :: multMatrixHelper xs ysTrans

multMatrix : Num a => Vect m (Vect n a)
                   -> Vect n (Vect p a)
                   -> Vect m (Vect p a)
multMatrix xs ys = let ysTrans = transposeMat ys
                   in  multMatrixHelper xs ysTrans


text:
module Main

word_lengths : List String -> List Nat
word_lengths [] = []
word_lengths (word :: words) = length word :: word_lengths words

xor : Bool -> Bool -> Bool
xor False y = y
xor True y = not y

mutual
  even : Nat -> Bool
  even Z = True
  even (S k) = odd k

  odd : Nat -> Bool
  odd Z = False
  odd (S k) = even k

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
import Data.Vect

readToBlank : IO (List String)
readToBlank = do x <- getLine
                 if (x == "")
                    then pure ([])
                    else do xs <- readToBlank
                            pure (x :: xs)

readAndSave : IO ()
readAndSave = do cnt <- readToBlank
                 putStr "File name: "
                 fn <- getLine
                 Right r <- writeFile fn (unlines cnt) | Left err => putStrLn (show err)
                 pure r

readVectStr : (f : File) -> IO (len ** Vect len String)
readVectStr f = do Right x <- fGetLine f | Left err => pure (_ ** [])
                   isEof <- fEOF f
                   putStrLn (show x)
                   if (isEof == True || x == "")
                   then pure (_ ** [])
                   else do (_ ** xs) <- readVectStr f
                           pure (_ ** x :: xs)

readVectFile : (filename : String) -> IO (n ** Vect n String)
readVectFile fn = do Right f <- openFile fn Read | Left err => pure (_ ** [])
                     res <- readVectStr f
                     closeFile f
                     pure res


text:
module Data.Compress.Inflate

import Data.Compress.Utils.Parser
import Data.Compress.Utils.Bytes
import Data.Compress.Utils.Misc
import Data.Compress.Huffman
import Data.Compress.Interface
import Data.Compress.Utils.FiniteBuffer
import Data.Vect
import Data.Bits
import Data.List
import Data.SnocList
import Data.Stream
import Control.Monad.Error.Either

public export
data InflateParserState'
  = InflateInit
  | InflateHuffman
  | InflateUncompressed
  | InflateEnd

public export
data InflateParserState : InflateParserState' -> Type where
  AtHeader : InflateParserState InflateInit
  AtHuffman : Bool -> HuffmanTree -> InflateParserState InflateHuffman
  AtUncompressed : Bool -> Nat -> InflateParserState InflateUncompressed
  AtEnd : SnocList Bits8 -> InflateParserState InflateEnd

public export
data InflateState
  = MkState Bitstream (FiniteBuffer Bits8) (DPair InflateParserState' InflateParserState)

match_off : List Nat
match_off = [ 3,4,5,6,7,8,9,10,11,13,15,17,19,23,27,31,35,43,51,59,67,83,99,115,131,163,195,227,258 ]

match_extra : List (Fin 32)
match_extra = [ 0,0,0,0,0,0,0,0,1,1,1,1,2,2,2,2,3,3,3,3,4,4,4,4,5,5,5,5,0 ]

dist_off : List Nat
dist_off = [ 1,2,3,4,5,7,9,13,17,25,33,49,65,97,129,193,257,385,513,769,1025,1537,2049,3073,4097,6145,8193,12289,16385,24577 ]

dist_extra : List (Fin 32)
dist_extra = [ 0,0,0,0,1,1,2,2,3,3,4,4,5,5,6,6,7,7,8,8,9,9,10,10,11,11,12,12,13,13 ]

clen_alphabets : List (Fin 19)
clen_alphabets = [ 16,17,18,0,8,7,9,6,10,5,11,4,12,3,13,2,14,1,15 ]

length_lookup : Nat -> Maybe (Nat, Fin 32)
length_lookup n = Just (!(index_may n match_off), !(index_may n match_extra))

distance_lookup : Nat -> Maybe (Nat, Fin 32)
distance_lookup n = Just (!(index_may n dist_off), !(index_may n dist_extra))

parse_inflate_uncompressed_len : Parser Bitstream (SimpleError String) Nat
parse_inflate_uncompressed_len = do
  len <- le_nat 2
  nlen <- cast <$> le_nat 2
  let True = (cast {to=Bits16} len) == (complement nlen)
  | False => fail $ msg "invalid length header"
  pure len

-- List (literal, code length)
parse_inflate_code_lengths : Bits32 -> Maybe Bits32 -> Parser Bitstream (SimpleError String) (Fin 19) -> ?
parse_inflate_code_lengths n_lit_code supplied_prev_length parser = loop [] 0 where
  loop : List (Bits32, Bits32) -> Bits32 -> Parser Bitstream (SimpleError String) (List (Bits32, Bits32))
  loop acc current = if current >= n_lit_code then pure acc else parser >>= \case
    16 => do
      let Just prev_length = map snd (head' acc) <|> supplied_prev_length
      | Nothing => fail $ msg "asked for previous code length, but buffer is empty"
      n <- (3 +) <$> get_bits 2
      let literals = zip [current..(current + n - 1)] (take (cast n) $ repeat prev_length)
      loop (literals <+> acc) (current + n)
    17 => do
      n <- (3 +) <$> get_bits 3
      loop acc (current + n)
    18 => do
      n <- (11 +) <$> get_bits 7
      loop acc (current + n)
    n => do
      let len = cast $ finToNat n
      loop ((current, len) :: acc) (current + 1)

parse_inflate_dynamic : Parser Bitstream (SimpleError String) HuffmanTree
parse_inflate_dynamic = do
  n_lit_code <- (257 +) <$> get_bits 5
  n_dist_code <- (1 +) <$> get_bits 5
  n_len_code <- (cast . (4 +)) <$> get_bits 4
  let True = n_len_code <= 19
  | False => fail $ msg "n_len_code exceeds 19"
  alphabets <- for (take (cast n_len_code) clen_alphabets) (\k => (k,) <$> get_bits 3)
  let Just code_length_parser = make_tree alphabets 19
  | Nothing => fail $ msg "failed to generate code length tree"

  literals <- parse_inflate_code_lengths n_lit_code Nothing code_length_parser
  let Just prev_length = map snd $ head' literals
  | Nothing => fail $ msg "literals tree parser did nothing"
  let Just literals_parser = make_tree literals (cast n_lit_code)
  | Nothing => fail $ msg "failed to generate code literals tree"

  distances <- parse_inflate_code_lengths n_dist_code (Just prev_length) code_length_parser
  let Just distances_parser = make_tree distances (cast n_dist_code)
  | Nothing => fail $ msg "failed to generate code distances tree"

  pure (MkTree literals_parser distances_parser)

data HuffmanOutput = End | Literal Bits8 | Copy Nat Nat

parse_inflate_huffman : HuffmanTree -> Parser Bitstream (SimpleError String) HuffmanOutput
parse_inflate_huffman tree = do
  x <- tree.parse_literals
  if x < 256 then pure $ Literal (cast x)
    else if x == 256 then pure End
    else if x < 286 then do
      let Just (off, extra) = length_lookup (cast (x - 257))
      | Nothing => fail $ msg "length symbol out of bound"
      length <- map (\b => off + cast b) (get_bits extra)
      dcode <- tree.parse_distance

      let Just (off, extra) = distance_lookup (cast dcode)
      | Nothing => fail $ msg "distance symbol out of bound"
      distance <- map (\b => off + cast b) (get_bits extra)
      pure $ Copy (cast length) (cast distance)
    else fail $ msg "invalid code \{show x} encountered"

parse_inflate_header : Parser Bitstream (SimpleError String) (DPair InflateParserState' InflateParserState)
parse_inflate_header = do
  final <- token
  case !(count 2 token) of
    -- Uncompressed
    [False, False] => do
      len <- parse_inflate_uncompressed_len
      pure (_ ** AtUncompressed final len)
    -- Fixed Huffman
    [True , False] => do
      pure (_ ** AtHuffman final default_tree)
    -- Dynamic Huffman
    [False, True ] => do
      tree <- parse_inflate_dynamic
      pure (_ ** AtHuffman final tree)
    -- Invalid
    [True , True ] => do
      fail $ msg "invalid compression method"

next_state : (is_final : Bool) -> DPair InflateParserState' InflateParserState
next_state True  = (_ ** AtEnd [<])
next_state False = (_ ** AtHeader)

feed_inflate' : SnocList Bits8 -> FiniteBuffer Bits8 -> DPair InflateParserState' InflateParserState ->
                Bitstream -> Either String (SnocList Bits8, InflateState)

feed_inflate' acc ob (_ ** AtEnd leftover) content =
  Right (acc, MkState neutral (empty 0) (_ ** AtEnd (leftover <>< toBits8 content))) -- terminates

feed_inflate' acc ob (InflateInit ** state) content =
  case feed content parse_inflate_header of
    Pure leftover state =>
      feed_inflate' acc ob state leftover
    Fail err =>
      Left (show err)
    _ => -- underfed, need more input
      Right (acc, MkState content ob (_ ** AtHeader))

feed_inflate' acc ob (_ ** (AtUncompressed final remaining)) content =
  let (output, leftover) = fromBits8 <$> splitAt remaining (toBits8 content)
      ob = ob +<>< output
      acc = acc <>< output
  in case minus remaining (length output) of
       S n => Right (acc, MkState leftover ob (_ ** AtUncompressed final (S n))) -- underfed
       Z   => feed_inflate' acc ob (next_state final) leftover

feed_inflate' acc' ob (_ ** (AtHuffman final tree)) content = go acc' ob tree content where
  go : SnocList Bits8 -> FiniteBuffer Bits8 -> HuffmanTree -> Bitstream -> Either String (SnocList Bits8, InflateState)
  go acc ob tree input =
    case feed input (parse_inflate_huffman tree) of
      Fail err =>
        Left (show err)
      Pure leftover End =>
        feed_inflate' acc ob (next_state final) leftover
      Pure leftover (Literal literal) =>
        go (acc :< literal) (ob +< literal) tree leftover
      Pure leftover (Copy len distance) =>
        case take_last distance ob of
          Just copied_chunk =>
            let appended = take len $ stream_concat $ repeat copied_chunk
            in go (acc <>< appended) (ob +<>< appended) tree leftover
          Nothing => Left "asked for distance \{show distance} but only \{show (length ob)} in buffer"
      _ => -- underfed, need more input
        Right (acc, MkState input ob (_ ** (AtHuffman final tree)))

export
Decompressor InflateState where
  feed (MkState ib ob state) content = mapFst toList <$> feed_inflate' Lin ob state (ib <+> fromBits8 content)
  done (MkState _ _ (_ ** AtEnd leftover)) = Right (toList leftover)
  done _ = Left "inflate: underfed"
  init = MkState neutral (empty 32768) (_ ** AtHeader)


text:
module LightClick.Main

import Data.String

import System
import System.File
import System.Clock

import Toolkit.System

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

import LightClick.Values

import LightClick.IR.ModuleCentric
import LightClick.IR.ChannelCentric
import LightClick.IR.Channel.Normalise
import LightClick.IR.Channel.MicroSV.Error
import LightClick.IR.Channel.MicroSV.Intermediate
import LightClick.IR.Channel.MicroSV

import LightClick.DSL.AST
import LightClick.DSL.Lexer
import LightClick.DSL.Parser
import LightClick.DSL.Convert

import Language.SystemVerilog.Micro
import Language.SystemVerilog.Micro.Pretty

export
Show a => Show (ParseFailure a) where
  show err
    = trim $ unlines [show (location err), (error err)]

export
Show a => Show (Run.ParseError a) where
  show (FError err)
    = trim $ unlines ["File Error: "
                     , show err]
  show (PError err)
    = trim $ unlines (forget (map show err))

  show (LError (MkLexFail l i))
    = trim $ unlines [show l, show i]

processArgs : List String -> IO $ Maybe (Bool, String)
processArgs (x::"--timing"::z::xs) = pure $ Just (True, z)
processArgs (x::y::xs) = pure $ Just (False, y)
processArgs _          = pure $ Nothing

printLog : Bool -> Clock type -> String -> IO ()
printLog True  t m = do putStr m
                        printLn t
printLog False t m = putStrLn m

timeToTryOrDie : Show err
              => Bool
              -> String
              -> (a -> Either err type)
              -> a
              -> IO type
timeToTryOrDie timing msg f a
    = do start <- clockTime UTC
         case f a of
           Left err => do stop <- clockTime UTC
                          putStrLn "Error Happened"
                          printLn err
                          let diff = timeDifference stop start
                          printLog timing diff msg
                          exitFailure
           Right res => do stop <- clockTime UTC
                           let diff =  timeDifference stop start
                           printLog timing diff msg
                           pure res

main : IO ()
main = do
  args <- getArgs
  Just (timing, fname) <- processArgs args | Nothing => do {putStrLn "Invalid args."; exitFailure}
  (res) <- fromFile fname
  case res of
    Left err => do { printLn err; exitFailure}
    Right ast => do

      putStrLn "LOG: Parsing Complete "

      term <- timeToTryOrDie timing
                             "LOG: MetaTyping Complete "
                             runConvert
                             ast

      v <- timeToTryOrDie timing
                          "LOG: Typing Complete "
                          runCheck
                          term

--      putStrLn "LOG : Showing Values"
--      printLn v
      putStrLn "LOG : Showing ModuleIR"
      cir <- tryOrDie (ChannelCentric.runConvert (ModuleCentric.runConvert v))

--      putStrLn "LOG : Showing ChannelIR"
--      printLn cir

      putStrLn "LOG : Normalising ChannelIR"
      cirn <- tryOrDie (normalise cir)

--      putStrLn "LOG : Showing Normalised ChannelIR"
--      printLn cirn

      putStrLn "LOG : Convert to MicroSV IR"
      msvir <- tryOrDie (Intermediate.runConvert cirn)
--
      putStrLn "LOG : Convert to MicroSV"
      msv <- tryOrDie (convertSpec msvir)
--
      putStrLn "LOG : Pretty Printing"
      let prettyMSV = prettySpec msv
      printLn prettyMSV

      putStrLn "LOG : Bye"
      exitSuccess

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Solutions.Functor

import Data.IORef
import Data.List
import Data.List1
import Data.String
import Data.Vect

%default total

--------------------------------------------------------------------------------
--          Code Required from the Turoial
--------------------------------------------------------------------------------

interface Functor' (0 f : Type -> Type) where
  map' : (a -> b) -> f a -> f b

interface Functor' f => Applicative' f where
  app   : f (a -> b) -> f a -> f b
  pure' : a -> f a

record Comp (f,g : Type -> Type) (a : Type) where
  constructor MkComp
  unComp  : f (g a)

implementation Functor f => Functor g => Functor (Comp f g) where
  map f (MkComp v) = MkComp $ map f <$> v

record Product (f,g : Type -> Type) (a : Type) where
  constructor MkProduct
  fst  : f a
  snd  : g a

implementation Functor f => Functor g => Functor (Product f g) where
  map f (MkProduct l r) = MkProduct (map f l) (map f r)

data Gender = Male | Female | Other

record Name where
  constructor MkName
  value : String

record Email where
  constructor MkEmail
  value : String

record Password where
  constructor MkPassword
  value : String

record User where
  constructor MkUser
  firstName : Name
  lastName  : Name
  age       : Maybe Nat
  email     : Email
  gender    : Gender
  password  : Password

interface CSVField a where
  read : String -> Maybe a

CSVField Gender where
  read "m" = Just Male
  read "f" = Just Female
  read "o" = Just Other
  read _   = Nothing

CSVField Bool where
  read "t" = Just True
  read "f" = Just False
  read _   = Nothing

CSVField Nat where
  read = parsePositive

CSVField Integer where
  read = parseInteger

CSVField Double where
  read = parseDouble

CSVField a => CSVField (Maybe a) where
  read "" = Just Nothing
  read s  = Just <$> read s

readIf : (String -> Bool) -> (String -> a) -> String -> Maybe a
readIf p mk s = if p s then Just (mk s) else Nothing

isValidName : String -> Bool
isValidName s =
  let len = length s
   in 0 < len && len <= 100 && all isAlpha (unpack s)

CSVField Name where
  read = readIf isValidName MkName

isEmailChar : Char -> Bool
isEmailChar '.' = True
isEmailChar '@' = True
isEmailChar c   = isAlphaNum c

isValidEmail : String -> Bool
isValidEmail s =
  let len = length s
   in 0 < len && len <= 100 && all isEmailChar (unpack s)

CSVField Email where
  read = readIf isValidEmail MkEmail

isPasswordChar : Char -> Bool
isPasswordChar ' ' = True
isPasswordChar c   = not (isControl c) && not (isSpace c)

isValidPassword : String -> Bool
isValidPassword s =
  let len = length s
   in 8 < len && len <= 100 && all isPasswordChar (unpack s)

CSVField Password where
  read = readIf isValidPassword MkPassword

data HList : (ts : List Type) -> Type where
  Nil  : HList Nil
  (::) : (v : t) -> (vs : HList ts) -> HList (t :: ts)

--------------------------------------------------------------------------------
--          Functor
--------------------------------------------------------------------------------

-- 1

Functor' Maybe where
  map' _ Nothing  = Nothing
  map' f (Just v) = Just $ f v

Functor' List where
  map' _ []        = []
  map' f (x :: xs) = f x :: map f xs

Functor' List1 where
  map' f (h ::: t) = f h ::: map' f t

Functor' (Vect n) where
  map' _ []        = []
  map' f (x :: xs) = f x :: map f xs

Functor' (Either e) where
  map' _ (Left ve)  = Left ve
  map' f (Right va) = Right $ f va

Functor' (Pair e) where
  map' f (ve,va) = (ve, f va)

-- 2

[Prod] Functor f => Functor g => Functor (\a => (f a, g a)) where
  map fun (fa, ga) = (map fun fa, map fun ga)

-- 3

record Identity a where
  constructor Id
  value : a

Functor Identity where
  map f (Id va) = Id $ f va

-- 4

record Const (e,a : Type) where
  constructor MkConst
  value : e

Functor (Const e) where
  map _ (MkConst v) = MkConst v

-- 5

data Crud : (i : Type) -> (a : Type) -> Type where
  Create : (value : a) -> Crud i a
  Update : (id : i) -> (value : a) -> Crud i a
  Read   : (id : i) -> Crud i a
  Delete : (id : i) -> Crud i a

Functor (Crud i) where
  map f (Create value)    = Create $ f value
  map f (Update id value) = Update id $ f value
  map _ (Read id)         = Read id
  map _ (Delete id)       = Delete id

-- 6

data Response : (e, i, a : Type) -> Type where
  Created : (id : i) -> (value : a) -> Response e i a
  Updated : (id : i) -> (value : a) -> Response e i a
  Found   : (values : List a) -> Response e i a
  Deleted : (id : i) -> Response e i a
  Error   : (err : e) -> Response e i a

Functor (Response e i) where
  map f (Created id value) = Created id $ f value
  map f (Updated id value) = Updated id $ f value
  map f (Found values)     = Found $ map f values
  map _ (Deleted id)       = Deleted id
  map _ (Error err)        = Error err

-- 7

data Validated : (e,a : Type) -> Type where
  Invalid : (err : e) -> Validated e a
  Valid   : (val : a) -> Validated e a

Functor (Validated e) where
  map _ (Invalid err) = Invalid err
  map f (Valid val)   = Valid $ f val

--------------------------------------------------------------------------------
--          Applicative
--------------------------------------------------------------------------------

-- 1

Applicative' (Either e) where
  pure' = Right
  app (Right f) (Right v) = Right $ f v
  app (Left ve) _         = Left ve
  app _         (Left ve) = Left ve

Applicative Identity where
  pure = Id
  Id f <*> Id v = Id $ f v

-- 2

{n : _} -> Applicative' (Vect n) where
  pure' = replicate n
  app []        []        = []
  app (f :: fs) (v :: vs) = f v :: app fs vs

-- 3

Monoid e => Applicative' (Pair e) where
  pure' v = (neutral, v)
  app (e1,f) (e2,v) = (e1 <+> e2, f v)

-- 4

Monoid e => Applicative (Const e) where
  pure _ = MkConst neutral
  MkConst e1 <*> MkConst e2 = MkConst $ e1 <+> e2

-- 5

Semigroup e => Applicative (Validated e) where
  pure = Valid
  Valid   f  <*> Valid v    = Valid $ f v
  Valid   _  <*> Invalid ve = Invalid ve
  Invalid e1 <*> Invalid e2 = Invalid $ e1 <+> e2
  Invalid ve <*> Valid _    = Invalid ve

-- 6

data CSVError : Type where
  FieldError           : (line, column : Nat) -> (str : String) -> CSVError
  UnexpectedEndOfInput : (line, column : Nat) -> CSVError
  ExpectedEndOfInput   : (line, column : Nat) -> CSVError
  App                  : (fst, snd : CSVError) -> CSVError

Semigroup CSVError where
  (<+>) = App

-- 7

readField : CSVField a => (line, column : Nat) -> String -> Validated CSVError a
readField line col str =
  maybe (Invalid $ FieldError line col str) Valid (read str)

toVect : (n : Nat) -> (line, col : Nat) -> List a -> Validated CSVError (Vect n a)
toVect 0     line _   []        = Valid []
toVect 0     line col _         = Invalid (ExpectedEndOfInput line col)
toVect (S k) line col []        = Invalid (UnexpectedEndOfInput line col)
toVect (S k) line col (x :: xs) = (x ::) <$> toVect k line (S col) xs

-- We can't use do notation here as we don't have an implementation
-- of Monad for `Validated`
readUser' : (line : Nat) -> List String -> Validated CSVError User
readUser' line ss = case toVect 6 line 0 ss of
  Valid [fn,ln,a,em,g,pw] =>
    [| MkUser (readField line 1 fn)
              (readField line 2 ln)
              (readField line 3 a)
              (readField line 4 em)
              (readField line 5 g)
              (readField line 6 pw) |]
  Invalid err => Invalid err

readUser : (line : Nat) -> String -> Validated CSVError User
readUser line = readUser' line . forget . split (',' ==)

interface CSVLine a where
  decodeAt : (line, col : Nat) -> List String -> Validated CSVError a

CSVLine (HList []) where
  decodeAt _ _ [] = Valid Nil
  decodeAt l c _  = Invalid (ExpectedEndOfInput l c)

CSVField t => CSVLine (HList ts) => CSVLine (HList (t :: ts)) where
  decodeAt l c []        = Invalid (UnexpectedEndOfInput l c)
  decodeAt l c (s :: ss) = [| readField l c s :: decodeAt l (S c) ss |]

decode : CSVLine a => (line : Nat) -> String -> Validated CSVError a
decode line = decodeAt line 1 . forget . split (',' ==)

hdecode :  (0 ts : List Type)
        -> CSVLine (HList ts)
        => (line : Nat)
        -> String
        -> Validated CSVError (HList ts)
hdecode _ = decode

-- 8

-- 8.1
head : HList (t :: ts) -> t
head (v :: _) = v

-- 8.2
tail : HList (t :: ts) -> HList ts
tail (_ :: t) = t

-- 8.3
(++) : HList xs -> HList ys -> HList (xs ++ ys)
[]        ++ ws = ws
(v :: vs) ++ ws = v :: (vs ++ ws)

-- 8.4
indexList : (as : List a) -> Fin (length as) -> a
indexList (x :: _)   FZ    = x
indexList (_ :: xs) (FS y) = indexList xs y
indexList []        x impossible

index : (ix : Fin (length ts)) -> HList ts -> indexList ts ix
index FZ     (v :: _)  = v
index (FS x) (_ :: vs) = index x vs
index ix [] impossible

-- 8.5
namespace HVect
  public export
  data HVect : (ts : Vect n Type) -> Type where
    Nil  : HVect Nil
    (::) : (v : t) -> (vs : HVect ts) -> HVect (t :: ts)

  public export
  head : HVect (t :: ts) -> t
  head (v :: _) = v

  public export
  tail : HVect (t :: ts) -> HVect ts
  tail (_ :: t) = t

  public export
  (++) : HVect xs -> HVect ys -> HVect (xs ++ ys)
  []        ++ ws = ws
  (v :: vs) ++ ws = v :: (vs ++ ws)

  public export
  index :  {0 n : Nat}
        -> {0 ts : Vect n Type}
        -> (ix : Fin n)
        -> HVect ts -> index ix ts
  index FZ     (v :: _)  = v
  index (FS x) (_ :: vs) = index x vs
  index ix [] impossible

-- 8.6

-- Note: We are usually not allowed to pattern match
-- on an erased argument. However, in this case, the
-- shape of `ts` follows from `n`, so we can pattern
-- match on `ts` to help Idris inferring the types.
--
-- Note also, that we create a `HVect` holding only empty
-- `Vect`s. We therefore only need to know about the length
-- of the type-level vector to implement this.
empties :  {n : Nat} -> {0 ts : Vect n Type} -> HVect (Vect 0 <$> ts)
empties {n = 0}   {ts = []}     = []
empties {n = S _} {ts = _ :: _} = [] :: empties

hcons :  {0 ts : Vect n Type}
      -> HVect ts
      -> HVect (Vect m <$> ts)
      -> HVect (Vect (S m) <$> ts)
hcons []        []        = []
hcons (v :: vs) (w :: ws) = (v :: w) :: hcons vs ws

htranspose :  {n : Nat}
           -> {0 ts : Vect n Type}
           -> Vect m (HVect ts)
           -> HVect (Vect m <$> ts)
htranspose []        = empties
htranspose (x :: xs) = hcons x (htranspose xs)

vects : Vect 3 (HVect [Bool, Nat, String])
vects = [[True, 100, "Hello"], [False, 0, "Idris"], [False, 2, "!"]]

vects' : HVect [Vect 3 Bool, Vect 3 Nat, Vect 3 String]
vects' = htranspose vects

-- 9
Applicative f => Applicative g => Applicative (Comp f g) where
  pure = MkComp . pure . pure
  MkComp ff <*> MkComp fa = MkComp [| ff <*> fa |]

-- 10
Applicative f => Applicative g => Applicative (Product f g) where
  pure v = MkProduct (pure v) (pure v)
  MkProduct ffl ffr  <*> MkProduct fal far =
    MkProduct (ffl <*> fal) (ffr <*> far)

--------------------------------------------------------------------------------
--          Monad
--------------------------------------------------------------------------------

-- 1
mapWithApp : Applicative f => (a -> b) -> f a -> f b
mapWithApp fun fa = pure fun <*> fa

-- 2
appWithBind : Monad f => f (a -> b) -> f a -> f b
appWithBind ff fa = ff >>= (\fun => fa >>= (\va => pure $ fun va))

-- or, more readable, the same thing with do notation
appWithBindDo : Monad f => f (a -> b) -> f a -> f b
appWithBindDo ff fa = do
  fun <- ff
  va  <- fa
  pure $ fun va

-- 3
bindFromJoin : Monad m => m a -> (a -> m b) -> m b
bindFromJoin ma f = join $ map f ma

-- 4
joinFromBind : Monad m => m (m a) -> m a
joinFromBind = (>>= id)

-- 5
-- The third law
-- `mf <*> ma = mf >>= (\fun => map (fun $) ma)`
-- does not hold, as implementation of *apply* on the
-- right hand side does not perform error accumulation.
--
-- `Validated e` therefore comes without implementation of
-- `Monad`. In order to use it in do blocks, it's best to
-- convert it to Either and back.

-- 6

DB : Type
DB = IORef (List (Nat,User))

data DBError : Type where
  UserExists        : Email -> Nat -> DBError
  UserNotFound      : Nat -> DBError
  SizeLimitExceeded : DBError

record Prog a where
  constructor MkProg
  runProg : DB -> IO (Either DBError a)

-- 6.1

-- make sure you are able to read and understand the
-- point-free style in the implementation of `map`!
Functor Prog where
  map f (MkProg run) = MkProg $ map (map f) . run

Applicative Prog where
  pure v = MkProg $ \_ => pure (Right v)
  MkProg rf <*> MkProg ra = MkProg $ \db => do
    Right fun <- rf db | Left err => pure (Left err)
    Right va  <- ra db | Left err => pure (Left err)
    pure (Right $ fun va)

Monad Prog where
  MkProg ra >>= f = MkProg $ \db => do
    Right va <- ra db | Left err => pure (Left err)
    runProg (f va) db

-- 6.2

HasIO Prog where
  liftIO act = MkProg $ \_ => map Right act

-- 6.3
throw : DBError -> Prog a
throw err = MkProg $ \_ => pure (Left err)

getUsers : Prog (List (Nat,User))
getUsers = MkProg (map Right . readIORef)

putUsers : List (Nat,User) -> Prog ()
putUsers us =
  if length us > 1000 then throw SizeLimitExceeded
  else MkProg $ \db => Right <$> writeIORef db us

modifyDB : (List (Nat,User) -> List (Nat,User)) -> Prog ()
modifyDB f = getUsers >>= putUsers . f

-- 6.4
lookupUser : (id : Nat) -> Prog User
lookupUser id = do
  db <- getUsers
  case lookup id db of
    Just u  => pure u
    Nothing => throw (UserNotFound id)

-- 6.5
deleteUser : (id : Nat) -> Prog ()
deleteUser id =
  -- In the first step, we are only interested in the potential
  -- of failure, not the actual user value.
  -- We can therefore use `(>>)` to chain the operations.
  -- In order to do so, we must wrap `lookupUser` in a call
  -- to `ignore`.
  ignore (lookupUser id) >> modifyDB (filter $ (id /=) . fst)

-- 6.6
Eq Email where (==) = (==) `on` value

newId : List (Nat,User) -> Nat
newId = S . foldl (\n1,(n2,_) => max n1 n2) 0

addUser : (u : User) -> Prog Nat
addUser u = do
  us <- getUsers
  case find ((u.email ==) . email . snd) us of
    Just (id,_) => throw $ UserExists u.email id
    Nothing     => let id = newId us in putUsers ((id, u) :: us) $> id

-- 6.7

update : Eq a => a -> b -> List (a,b) -> List (a,b)
update va vb = map (\p@(va',vb') => if va == va' then (va,vb) else p)

updateUser : (id : Nat) -> (mod : User -> User) -> Prog User
updateUser id mod = do
  u  <- mod <$> lookupUser id
  us <- getUsers
  case find ((u.email ==) . email . snd) us of
    Just (id',_) => if id /= id'
                      then throw $ UserExists u.email id'
                      else putUsers (update id u us) $> u
    Nothing      => putUsers (update id u us) $> u

-- 6.8

record Prog' env err a where
  constructor MkProg'
  runProg' : env -> IO (Either err a)

Functor (Prog' env err) where
  map f (MkProg' run) = MkProg' $ map (map f) . run

Applicative (Prog' env err) where
  pure v = MkProg' $ \_ => pure (Right v)
  MkProg' rf <*> MkProg' ra = MkProg' $ \db => do
    Right fun <- rf db | Left err => pure (Left err)
    Right va  <- ra db | Left err => pure (Left err)
    pure (Right $ fun va)

Monad (Prog' env err) where
  MkProg' ra >>= f = MkProg' $ \db => do
    Right va <- ra db | Left err => pure (Left err)
    runProg' (f va) db

HasIO (Prog' env err) where
  liftIO act = MkProg' $ \_ => map Right act

throw' : err -> Prog' env err a
throw' ve = MkProg' $ \_ => pure (Left ve)


text:
module EqualityIn

interface Preorder t (po : t -> t -> Type) where
  transitive : (0 a, b, c : t) -> po a b -> po b c -> po a c
  reflexive : (0 a : t) -> po a a

interface Preorder t eq => Equivalence t (eq : t -> t -> Type) where
  symmetric : (0 a, b : t) -> eq a b -> eq b a

interface Equivalence t eq => Congruence t (f : t -> t) (eq : t -> t -> Type) where
  congruent : (0 a, b : t) -> eq a b -> eq (f a) (f b)

Preorder t Equal where
  transitive _ _ _ ab bc = trans ab bc
  reflexive _ = Refl

Equivalence t Equal where
  symmetric _ _ ab = sym ab

Congruence t f Equal where
  congruent _ _ ab = cong f ab

abba : a = b -> b = a
abba = symmetric a b

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
fun1 : a -> a
fun1 x = x

{-

allow unclosed comment block at the end of file

{-

fun2 : a -> a
fun2 x = x

fun3 : a -> a
fun3 x = x


text:
-- ---------------------------------------------------------------- [ Core.idr ]
-- Module    : Core.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Core Data Types used in Cordial
module Cordial.Model.Common

import Data.Ranged
import Data.Vect
import Text.Markup.Edda

import public Cordial.Model.Common.Essential
import public Cordial.Model.Common.VLNV
import public Cordial.Model.Common.Widths
import public Cordial.Model.Common.Hacks
import public Cordial.Model.Common.Whole
import public Cordial.Model.Common.WireTy
import public Cordial.Model.Common.Direction
import public Cordial.Model.Common.Necessary
import public Cordial.Model.Common.Label
import public Cordial.Model.Common.Name

%default total
%access public export

namespace ClockInfo

  data ClockInfo : (wty : WireTy) -> (dir : Direction ty endpoint flow prf) -> Type where
    MkCOut : (mce   : Maybe ClockEdge)
          -> (md    : Maybe Delay)
          -> (mtc   : Maybe (RangedNat 0 100))
          -> (phase : RangedNat 0 360)
          -> (freq  : Nat)
          -> ClockInfo (Clock mce md mtc) OUT
    MkCIn : (mce   : Maybe ClockEdge)
         -> (md    : Maybe Delay)
         -> (mtc   : Maybe (RangedNat 0 100))
         -> (phase : Maybe (RangedNat 0 360))
         -> (freq  : Maybe Nat)
         -> ClockInfo (Clock mce md mtc) IN

namespace DataEndian

  data DataEndian : Maybe Endian -> Type where
    Dictated : (endian : Endian) -> DataEndian (Just endian)
    Free     : (endian : Endian) -> DataEndian Nothing

namespace Extension
  data ExtensionTy = DESCRIPTION
                   | PORTDESC WireTy
                   | PORT WireTy
                   | COMPONENT
                   | INTERFACE
                   | DESIGN
                   | CONNECTION ConnectionTy

  ExtensionKind : Type
  ExtensionKind = (ExtensionTy -> Type)

  data VendorExt : (ty : ExtensionTy) -> Type where
    Ext : {kind : ExtensionTy -> Type} -> (value : kind ty) -> VendorExt ty
    Empty : VendorExt ty

namespace DocString

  data IsRight : Either a b -> Type where
    ItIsRight : IsRight (Right value)

  Uninhabited (IsRight (Left l)) where
    uninhabited ItIsRight impossible

  data DocString : Type where
    Empty : DocString
    Doc   : (src : Edda SNIPPET)
         -> DocString

  newDocString : (src : String)
              -> (p   : String -> Either String (Edda SNIPPET))
              -> DocString
  newDocString src p with (p src)
    newDocString src p | (Left l) = Empty
    newDocString src p | (Right r) = Doc r

  toString : (Edda SNIPPET -> String) -> DocString -> String
  toString _ Empty = ""
  toString p (Doc src) = p src

namespace Driver
  data Driver = Any | Clock | SingleShot

namespace Value
  data ValueOrigin : PortWidthDesc shape -> Type where
    DefaultValue   : Vect (toNat w) Value -> ValueOrigin w
    Zeroed         : ValueOrigin w
    RequiresDriver : Driver -> ValueOrigin w
    NoValue        : ValueOrigin w

-- ----------------------------------------- [ High-Level Protocol Information ]

namespace Protocol

  record ProtocolInfo where
    constructor MkPInfo
    protocolType : Maybe String
    payloadName  : String
    payloadType  : String

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

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
module Util

import Network.Socket
import Data.Primitives.Views
import System

%access public export

randHelper : (seed' : Int) -> Int
randHelper seed' with (divides seed' 9999)
  randHelper ((9999 * div) + rem) | (DivBy prf) = rem

randPort : (seed : Nat) -> Port
randPort seed = let seed' = toIntNat (1664525 * seed + 1013904223) in
                randHelper (seed' `shiftR` 2)

max_stars_repo_name: AsmusAB/Idris-peer-to-peer-network

max_issues_repo_name: AsmusAB/Idris-peer-to-peer-network

max_forks_repo_name: AsmusAB/Idris-peer-to-peer-network


text:
module Imperative.Lexer

import DataStructures
import Lightyear.Strings

%access export

rIf : Parser ()
rIf = token "if"

rThen : Parser ()
rThen = token "then"

rElse : Parser ()
rElse = token "else"

rWhile : Parser ()
rWhile = token "while"

rDo : Parser ()
rDo = token "do"

rSkip : Parser ()
rSkip = token "skip"

rTrue : Parser ()
rTrue = token "true"

rFalse : Parser ()
rFalse = token "false"

rPlus : Parser ()
rPlus = token "+"

rMinus : Parser ()
rMinus = token "-"

rTimes : Parser ()
rTimes = token "*"

rDivide : Parser ()
rDivide = token "/"

rAssign : Parser ()
rAssign = token ":="

rLT : Parser ()
rLT = token "<"

rGT : Parser ()
rGT = token ">"

rAnd : Parser ()
rAnd = token "and"

rOr : Parser ()
rOr = token "or"

rNot : Parser ()
rNot = token "not"

reservedNames : List String
reservedNames = [ "if"
                , "then"
                , "else"
                , "while"
                , "do"
                , "skip"
                , "true"
                , "false"
                , "not"
                , "and"
                , "or"
                ]

max_stars_repo_name: alexhumphreys/pl-playground

max_issues_repo_name: alexhumphreys/pl-playground

max_forks_repo_name: alexhumphreys/pl-playground


text:
module Program

import CommonTestingStuff

import Data.List

export
beforeString : String
beforeString = "before coop"

s55 : PrintString m => CanSleep m => (offset : Time) => m String
s55 = do
  printTime offset "                         s55 proc, first"
  for 5 $ do
    printTime offset "                         s55 proc, before 350"
    sleepFor 350.millis
    printTime offset "                         s55 proc, before 750"
    sleepFor 750.millis
  "short" <$ printTime offset "                         s55 proc, last"

export
program : PrintString m => CanSleep m => Zippable m => Alternative m => m Unit
program = do
  offset <- currentTime
  printTime offset "start"

  res <- zipWith (++) empty s55
  printTime offset "top: \{res}"

  printTime offset "end"


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

import Sif.Types
import Sif.Pattern
import Readability
import Readability.Process.XML

public export
data PEvalResult : Type where
  ResSif  : EvalResult -> PEvalResult
  ResRead : ReadResult -> PEvalResult
  ResWTA  : Float      -> PEvalResult

Show PEvalResult where
  show (ResSif  res) = show res
  show (ResRead res) = show res
  show (ResWTA  res) = show res

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

max_stars_repo_name: jfdm/frigg-tool

max_issues_repo_name: jfdm/frigg-tool

max_forks_repo_name: jfdm/frigg-tool


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.Utils

%access public export
%default total
%include C "stdio.h"
%include C "busywait.h"

uartWrite : String -> IO ()
uartWrite str =
    foreign FFI_C "printf" (String -> IO ()) str

busyWait : Int -> IO ()
busyWait loops =
    foreign FFI_C "busywait" (Int -> IO ()) loops

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:
module Linear.Equality

import Linear.Types

public export
replace1 : (0 p : a -> Type) -> (1 _ : x = y) -> p x -<> p y
replace1 p Refl r = r

public export
promoteEq : (0 _ : x = y) -> x = y
promoteEq Refl = Refl

public export
lcong : (f : (1 _ : t) -> u) ->
        (1 _ : a = b) -> f a = f b
lcong f Refl = Refl

public export
lcong2 : (f : (1 _ : t) -> (1 _ : s) -> u) ->
        a = b -> a' = b' -> f a a' = f b b'
lcong2 f Refl Refl = Refl

public export
lcongApp : {f, g : (1 _ : t) -> u} -> f = g -> (x : t) -> f x = g x
lcongApp Refl _ = Refl

public export
congApp : {f, g : t -> u} -> f = g -> (x : t) -> f x = g x
congApp Refl _ = Refl

public export
uip : {x, y : a} -> (p , q : x = y) -> p = q
uip Refl Refl = Refl

max_stars_repo_name: g-nakov/quantitative-poly

max_issues_repo_name: g-nakov/quantitative-poly

max_forks_repo_name: g-nakov/quantitative-poly


text:
module Assn

import Expr
import Logic
import Maps

%access public export

%default total

Assertion : Type
Assertion = State -> Type

namespace ExAssertions
  as1 : Assertion
  as1 = \st => st X = 3

  as2 : Assertion
  as2 = \st => LTE (st X) (st Y)

  as3 : Assertion
  as3 = \st => Either (st X = 3) (LTE (st X) (st Y))

  as4 : Assertion
  as4 = \st => (LTE (st Z * st Z) (st X), Not (LTE (S (st Z) * S (st Z)) (st X)))

  as5 : Assertion
  as5 = \st => ()

  as6 : Assertion
  as6 = \st => Void

AssertImplies : (p, q : Assertion) -> Type
AssertImplies p q = (st : State) -> p st -> q st

infixr 8 ->>

(->>) : (p, q : Assertion) -> Type
(->>) = AssertImplies

assertImpliesRefl : p ->> p
assertImpliesRefl _ p_st = p_st

assertImpliesTrans : p ->> q -> q ->> r -> p ->> r
assertImpliesTrans p_imp_q q_imp_r = \st, p_st =>
  q_imp_r st (p_imp_q st p_st)

infix 8 <<->>

(<<->>) : (p, q : Assertion) -> Type
(<<->>) p q = (AssertImplies p q, AssertImplies q p)

assertEquivRefl : p <<->> p
assertEquivRefl = (assertImpliesRefl, assertImpliesRefl)

assertEquivTrans : p <<->> q -> q <<->> r -> p <<->> r
assertEquivTrans (p_imp_q, q_imp_p) (q_imp_r, r_imp_q) =
  (assertImpliesTrans p_imp_q q_imp_r, assertImpliesTrans r_imp_q q_imp_p)

AssignSub : (x : Id) -> (a : AExp) -> (p : Assertion) -> Assertion
AssignSub x a p = \st => p (t_update x (aeval st a) st)

BAssn : (b : BExp) -> Assertion
BAssn b = \st => beval st b = True

bexp_eval_true : beval st b = True -> BAssn b st
bexp_eval_true prf = prf

bexp_eval_false : beval st b = False -> Not (BAssn b st)
bexp_eval_false bfalse btrue = absurd $ trans (sym bfalse) btrue

bassn_eval_false : Not (BAssn b st) -> beval st b = False
bassn_eval_false contra = fst not_true_iff_false contra


text:
module Part2.Sec8_3_deceq
import Data.Vect

{-
data Dec : (prop : Type) -> Type where
     Yes : (prf : prop) -> Dec prop
     No  : (contra : prop -> Void) -> Dec prop

interface DecEq ty where
            decEq : (val1 : ty) -> (val2 : ty) -> Dec (val1 = val2)
-}

{- Redone example from 8.1 -}
exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength {m} len input = case decEq m len of
         Yes Refl => Just input
         No contra => Nothing

{- Just for Fun, This code shows code for instance of DecEq -}
data MyPair a b = MkMyPair a b

secondUnequal :  {a1 : a, a2 : a, b1 : b, b2 : b} -> (a1 = a2) -> (contra : (b1 = b2) -> Void) ->  (MkMyPair a1 b1 = MkMyPair a2 b2) -> Void
secondUnequal Refl contra Refl = contra Refl

{- Seems to know that it does not even need to check the second param! -}
firstUnequal : (contra : (a1 = a2) -> Void) -> (MkMyPair a1 b1 = MkMyPair a2 b2) -> Void
firstUnequal contra Refl = contra Refl

(DecEq a, DecEq b) => DecEq (MyPair a b) where
   decEq (MkMyPair a1 b1) (MkMyPair a2 b2) = case decEq a1 a2 of
        Yes Refl => case decEq b1 b2 of
            Yes Refl => Yes Refl
            No contra => No (secondUnequal Refl contra)
        No contra => No (firstUnequal contra)

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes


text:
{-
System.Int32[]
17
25
42
-}
import CIL.FFI.Array
import Data.Vect

infixl 5 >=>

(>=>) : Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
(>=>) f g x = f x >>= g

main : CIL_IO ()
main = do
  array <- arrayOf CILTyInt32 [17, 25]
  putStrLn !(ToString array)
  let a = \i => get array i
  for_ [0..1] $
    a >=> printLn
  printLn (!(a 0) + !(a 1))

-- Local Variables:
-- idris-load-packages: ("cil")
-- End:

max_stars_repo_name: timjs/iris-clean

max_issues_repo_name: timjs/iris-clean

max_forks_repo_name: timjs/iris-clean