text:
module Protocol.IDE.Highlight

import Protocol.SExp

import Protocol.IDE.FileContext
import Protocol.IDE.Decoration

%default total

public export
record Highlight where
  constructor MkHighlight
  location : FileContext
  name : String
  isImplicit : Bool
  key : String
  decor : Decoration
  docOverview : String
  typ : String
  ns : String

public export
record LwHighlight where
  constructor MkLwHighlight
  location : FileContext
  decor : Decoration

export
SExpable Highlight where
  toSExp (MkHighlight fc nam impl k dec doc t ns)
    = SExpList [ toSExp fc
               , SExpList [ SExpList [ SymbolAtom "name", StringAtom nam ]
                          , SExpList [ SymbolAtom "namespace", StringAtom ns ]
                          , toSExp dec
                          , SExpList [ SymbolAtom "implicit", toSExp impl ]
                          , SExpList [ SymbolAtom "key", StringAtom k ]
                          , SExpList [ SymbolAtom "doc-overview", StringAtom doc ]
                          , SExpList [ SymbolAtom "type", StringAtom t ]
                          ]
               ]

export
FromSExpable Highlight where
  fromSExp (SExpList [ fc
               , SExpList [ SExpList [ SymbolAtom "name", StringAtom nam ]
                          , SExpList [ SymbolAtom "namespace", StringAtom ns ]
                          , dec
                          , SExpList [ SymbolAtom "implicit", impl ]
                          , SExpList [ SymbolAtom "key", StringAtom key ]
                          , SExpList [ SymbolAtom "doc-overview", StringAtom doc ]
                          , SExpList [ SymbolAtom "type", StringAtom typ ]
                          ]
               ]) = do
                 pure $ MkHighlight
                   { location = !(fromSExp fc)
                   , name = nam
                   , ns
                   , isImplicit = !(fromSExp impl)
                   , decor = !(fromSExp dec)
                   , docOverview = doc
                   , key, typ}
  fromSExp _ = Nothing

export
SExpable LwHighlight where
  toSExp lwhl = SExpList
                 [ toSExp lwhl.location
                 , SExpList [ toSExp lwhl.decor]
                 ]

export
FromSExpable LwHighlight where
  fromSExp (SExpList
            [ location
            , SExpList [ decor ]
            ]) = do pure $ MkLwHighlight
                      { location = !(fromSExp location)
                      , decor    = !(fromSExp decor)}
  fromSExp _ = Nothing

public export
data SourceHighlight =
    Full Highlight
  | Lw LwHighlight

export
SExpable SourceHighlight where
  toSExp (Full hl) = toSExp hl
  toSExp (Lw   hl) = toSExp hl

export
FromSExpable SourceHighlight where
  fromSExp shl = do
    let Nothing = fromSExp shl
      | Just hl => Just (Full hl)
    hl <- fromSExp shl
    pure $ Lw hl

ext: idr


text:
module Data.Bytes.Lazy.Internal

import Data.Bytes.Strict

private
moduleName : String
moduleName = "Data.Bytes.Lazy.Internal"

---------------------------------------------------------------------
-- This module is experimental as idris2 doesn't check productivity/totality
-- very well, if at all
---------------------------------------------------------------------

-- Because we don't have good namespace management yet this is being given a
-- different name for the type. We might want the same name as strict Bytes so
-- people can swap it in types easier as they iterate their software's design.
-- That being said ByteString of Haskell calling lazy and nonlazy ByteString's
-- the same has certainly caused confusion so I'm inclined to keep LBytes.

-- Lazy or Inf for this type?
public export
data LBytes : Type where
  Empty : LBytes
  Chunk : (b : Bytes) -> (bs : Inf LBytes) -> LBytes

public export
data NonEmpty : LBytes -> Type where
  IsNonEmpty : NonEmpty (Chunk _ _)

---------------------------------------------------------------------
-- Sizing
---------------------------------------------------------------------

-- The idea/distant-hope is to fit what we're working on into L1/L2 cache, this
-- means it's very much backend dependent and possibly not even a realistic
-- goal. Do you know the memory layout of a chez scheme bytevector? A gambit
-- bytevector? JS vector?

-- We can micromanage it ourselves via C (given an appropriate GC to clean up
-- our immutable bytes) but that cuts out a swath of possible backends, e.g.
-- javascript.

-- These should be tested with various backends. In fact they should have a
-- mechanism to allow them to depend on the backend. Perhaps backends should
-- provide sizeOf operator for values.
defaultChunkSize : Int
defaultChunkSize = 32*1024

smallChunkSize : Int
smallChunkSize = 4*1024
-- Also the goal size for chunks from things like
-- unpackBytes/unpackAppendBytesLazy

chunkOverhead : Int
chunkOverhead = 3*64 -- Complete guess!
-- Chunk Bytes LBytes
--  Int   Ptr   Ptr

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

-- Should we simply require NonEmpty for Chunk in the first place instead of
-- enforcing/checking invariants?

-- Having Lazy in the type is neat and all but do I also need Lazy in functions
-- or is it enough that I'm constructing an LBytes? Without
-- totality/productivity checking I'm not quite sure.

export
chunk : (b : Bytes) -> NonEmpty b => LBytes -> LBytes
chunk b bs = Chunk b bs

export
chunk' : (b : Bytes) -> LBytes -> LBytes
chunk' b bs = if null b then bs else Chunk b bs

export
foldrChunk : (Bytes -> b -> b) -> b -> LBytes -> b
foldrChunk f z Empty = z
foldrChunk f z (Chunk b bs) = f b (foldrChunk f z bs)

export
foldlChunk : (b -> Bytes -> b) -> b -> LBytes -> b
foldlChunk f z Empty = z
foldlChunk f z (Chunk b bs) = foldlChunk f (f z b) bs


text:
module Circuits.Idealised.Check

import Decidable.Equality

import Data.Nat
import Data.String
import Data.List.Elem
import Data.List.Quantifiers

import Toolkit.Decidable.Informative
import Toolkit.Decidable.Equality.Views

import Toolkit.Data.Graph.EdgeBounded
import Toolkit.Data.Whole
import Toolkit.Data.Location
import Toolkit.Data.List.DeBruijn

import Ref

import Circuits.Split
import Circuits.Idealised.Types
import Circuits.Idealised.Terms
import Circuits.Idealised.AST

%default total

data Entry : (String, (Ty, Usage)) -> Type where
  MkEntry : (name : String)
         -> (type : Ty)
         -> (u    : Usage)
                 -> Entry (name, (type,u))

Env : List (String, (Ty, Usage)) -> Type
Env = Env (String, (Ty, Usage)) Entry

showEnv : Env es -> String
showEnv [] = ""
showEnv ((MkEntry name type FREE) :: rest)
  = name <+> " : " <+> show type <+> "\n" <+> (showEnv rest)
showEnv ((MkEntry name type USED) :: rest) = showEnv rest

isEmpty : (s : String) -> DPair Ty (\t => Elem (s, (t, FREE)) []) -> Void
isEmpty _ (MkDPair _ _) impossible

lookupLaterFail : (DPair Ty (\t => Elem (s, (t, FREE)) xs) -> Void)
               -> (s = name -> Void)
               -> DPair Ty (\t => Elem (s, (t, FREE)) ((name, (type, u)) :: xs))
               -> Void
lookupLaterFail f g (MkDPair type Here) = g Refl
lookupLaterFail f g (MkDPair fst (There x)) = f (MkDPair fst x)

lookupLaterFailAlt : (DPair Ty (\t => Elem (s, (t, FREE)) xs) -> Void)
                   -> DPair Ty (\t => Elem (s, (t, FREE)) ((s, (type, USED)) :: xs)) -> Void
lookupLaterFailAlt f (MkDPair fst (There z)) = f (MkDPair fst z)

data LookupFail = NotFound String | IsUsed String

lookup : (s : String)
      -> Env ctxt
      -> DecInfo LookupFail (t ** Elem (s,(t,FREE)) ctxt)
lookup s [] = No (NotFound s) (isEmpty s)
lookup s ((MkEntry name type u) :: rest) with (decEq s name)
  lookup s ((MkEntry s type u) :: rest) | (Yes Refl) with (u)
    lookup s ((MkEntry s type u) :: rest) | (Yes Refl) | USED with (lookup s rest)
      lookup s ((MkEntry s type u) :: rest) | (Yes Refl) | USED | (Yes (MkDPair fst snd))
        = Yes (MkDPair fst (There snd))
      lookup s ((MkEntry s type u) :: rest) | (Yes Refl) | USED | (No reason contra)
        = No (IsUsed s) (lookupLaterFailAlt contra)
    lookup s ((MkEntry s type u) :: rest) | (Yes Refl) | FREE
      = Yes (MkDPair type Here)

  lookup s ((MkEntry name type u) :: rest) | (No contra) with (lookup s rest)
    lookup s ((MkEntry name type u) :: rest) | (No contra) | (Yes (MkDPair fst snd))
      = Yes (MkDPair fst (There snd))
    lookup s ((MkEntry name type u) :: rest) | (No contra) | (No reason f)
      = No reason (lookupLaterFail f contra)

strip : {ctxt : List (String, (Ty, Usage))}
     -> Elem (s,(type,usage)) ctxt -> Elem (type,usage) (map Builtin.snd ctxt)
strip Here = Here
strip (There x) = There (strip x)

data Use : (curr : List (String, (Ty, Usage)))
        -> (prf  : Elem (s,(type,FREE)) curr)
        -> (next : List (String, (Ty, Usage)))
        -> Type
  where
    H : Use ((s,(type,FREE)) :: rest)
            Here
            ((s,(type,USED)) :: rest)
    T :  Use rest later restAlt
      -> Use ((s,(t,u)) :: rest)
             (There later)
             ((s,(t,u)) :: restAlt)

use : {curr : List (String, (Ty,Usage))}
   -> (prf : Elem (s,(t,FREE)) curr)
   -> (env : Env curr)
          -> DPair (List (String, (Ty,Usage)))
                   (Use curr prf)
use _ [] impossible

use {curr = ((s, (t, FREE)) :: xs)} Here (elem :: rest) = MkDPair ((s, (t, USED)) :: xs) H
use {curr = ((x, (z, w)) :: xs)} (There y) (elem :: rest) with (use y rest)
  use {curr = ((x, (z, w)) :: xs)} (There y) (elem :: rest) | (MkDPair fst snd) = MkDPair ((x, (z, w)) :: fst) (T snd)

strip' : {curr,next : List (String, (Ty,Usage))}
      -> {prf       : Elem (s,(t,FREE)) curr}
      -> Use curr prf next
      -> Use (map Builtin.snd curr)
             (strip prf)
             (map Builtin.snd next)
strip' H = H
strip' (T x) = T (strip' x)

newEnv : (env : Env curr)
      -> (use : Use curr prf next)
             -> Env next
newEnv (MkEntry s type FREE :: rest) H = MkEntry s type USED :: rest
newEnv (elem :: rest) (T x) = elem :: newEnv rest x

laterUsed : (All Used (map Builtin.snd xs) -> Void) -> All Used ((type, USED) :: map Builtin.snd xs) -> Void
laterUsed f (x :: y) = f y

isUsed : DList (String, (Ty, Usage)) Entry xs -> All Used ((type, FREE) :: map Builtin.snd xs) -> Void
isUsed [] (Types.IsUsed :: _) impossible
isUsed (_ :: _) (Types.IsUsed :: _) impossible

used : Env ctxt
    -> Dec (All Used (map Builtin.snd ctxt))
used [] = Yes []
used ((MkEntry name type USED) :: rest) with (used rest)
  used ((MkEntry name type USED) :: rest) | (Yes prf) = Yes (IsUsed :: prf)

  used ((MkEntry name type USED) :: rest) | (No contra) = No (laterUsed contra)

used ((MkEntry name type FREE) :: rest) = No (isUsed rest)

export
data FailingEdgeCase = InvalidSplit Nat Nat Nat Nat
                     | InvalidEdge  Nat Nat Nat

export
Show FailingEdgeCase where
  show (InvalidSplit p s l r) = "Pivot (" <+> show p <+> ") is wrong do not add up: " <+> unwords [show s, "!= 1 + ", show l, "+", show r]
  show (InvalidEdge  s l r) = "Indices do not add up: " <+> unwords [show s, "= 1 + ", show l, "+", show r]

export
data Error = Mismatch Ty Ty | ElemFail LookupFail | PortExpected Direction
           | VectorExpected
           | VectorTooShort
           | VectorSizeMismatch Whole Whole Whole
           | LinearityError (Env es)
           | Err FileContext Check.Error
           | NotEdgeCase FailingEdgeCase
           | MismatchGate DType DType
export
Show Check.Error where
  show (Mismatch x y) = "Type Mismatch:\n\n" <+> unlines [unwords ["\tExpected:",show x], unwords ["\tGiven:", show y]]
  show (MismatchGate x y) = "Type Mismatch:\n\n" <+> unlines [unwords ["\tExpected:",show x], unwords ["\tGiven:", show y]]
  show (ElemFail (IsUsed x))   = unwords ["Port is used:", x]
  show (ElemFail (NotFound x)) = unwords ["Undeclared variable::", x]
  show (NotEdgeCase r)  = "Not an edge case:\n\n" <+> show r
  show (PortExpected INPUT) = "Expected an Input Port"
  show (PortExpected OUTPUT) = "Expected an Output Port"
  show (LinearityError env) = "Dangling Ports:\n\n" <+> showEnv env
  show (VectorExpected) = "Vector Expected"
  show (VectorTooShort) = "Output Vector must be a length greater or equal to two."
  show (VectorSizeMismatch o a b)
    = unlines [ "Output Vector and input are wrong sizes:"
              , unwords ["\t" <+> show o, "!=", show a, "+", show b]]
  show (Err x y) = unwords [show x, show y]

public export
TyCheck : Type -> Type
TyCheck = Either Check.Error

lift : Dec a -> Check.Error -> TyCheck a
lift (Yes prf) _ = Right prf
lift (No contra) e = Left e

namespace Info
  public export
  lift : DecInfo e a -> Check.Error -> TyCheck a
  lift (Yes prf)     _ = Right prf
  lift (No m contra) e = Left e

  public export
  allEqual : FileContext
          -> (a,b,c : DType)
          -> TyCheck (AllEqual a b c)
  allEqual fc a b c with (Views.allEqual a b c)
    allEqual fc c c c | (Yes AE)
      = pure AE
    allEqual fc a b c | (No AB prfWhyNot)
      = Left (Err fc (MismatchGate a b))
    allEqual fc a b c | (No AC prfWhyNot)
      = Left (Err fc (MismatchGate a c))

typeCheck : {ctxt : List (String, (Ty,Usage))}
         -> (curr : Env ctxt)
         -> (ast  : AST)
                  -> TyCheck (type ** cout ** Pair (Env cout) (Term (map Builtin.snd ctxt)
                                                                    type
                                                                    (map Builtin.snd cout)))
typeCheck curr (Var x) with (lookup (get x) curr)
  typeCheck curr (Var x) | (Yes (MkDPair ty prf)) with (use prf curr)
    typeCheck curr (Var x) | (Yes (MkDPair ty prf)) | (MkDPair next u)
       = Right (ty ** next ** MkPair (newEnv curr u) (Var (strip prf) (strip' u)))

  typeCheck curr (Var x) | (No reason contra) = Left (Err (span x) (ElemFail reason))

typeCheck curr (Input fc x y s z)
  = do (TyUnit ** cz ** (ex,term)) <- typeCheck (MkEntry (get s) (TyPort (MkPair x y)) FREE :: curr) z
         | (ty ** _  ** _) => Left (Mismatch TyUnit ty)

       case ex of
         Nil => pure (TyUnit ** cz ** (Nil, (NewSignal x y term)))
         _   => Left (Err fc (LinearityError ex))

typeCheck curr (Wire fc x a b y)
  = do (TyUnit ** cz ** (ex,term)) <- typeCheck (MkEntry (get a) (TyPort (MkPair OUTPUT x)) FREE ::
                                               MkEntry (get b) (TyPort (MkPair INPUT  x)) FREE :: curr) y
         | (ty ** _  ** _) => Left (Mismatch TyUnit ty)

       case ex of
         Nil => pure (TyUnit ** cz ** (Nil, (Wire x term)))
         _   => Left (Err fc (LinearityError ex))

typeCheck curr (Dup fc x y z)
  = do (TyPort (OUTPUT,dtypeA) ** cx ** (ex,termX)) <- typeCheck curr x
                  | ty => Left (Err fc (PortExpected OUTPUT))

       (TyPort (OUTPUT,dtypeB) ** cy ** (ey,termY)) <- typeCheck ex y
                  | ty => Left (Err fc (PortExpected OUTPUT))

       (TyPort (INPUT,dtypeC) ** cz ** (ez,termZ)) <- typeCheck ey z
                  | ty => Left (Err fc (PortExpected INPUT))

       Refl <- lift (decEq dtypeA dtypeB)
                    (Err fc (MismatchGate dtypeA dtypeB))

       Refl <- lift (decEq dtypeB dtypeC)
                    (Err fc (MismatchGate dtypeA dtypeC))

       pure (TyGate ** cz ** (ez, Dup termX termY termZ))

typeCheck curr (Seq x y)
  = do (TyGate ** cx ** (ex,termX)) <- typeCheck curr x
            | (ty ** _ ** _) => Left (Mismatch TyGate ty)

       (TyUnit ** cy ** (ey, termY)) <- typeCheck ex y
             | (ty ** _ ** _) => Left (Mismatch TyUnit ty)

       case ey of
         Nil => pure (TyUnit ** cy ** (Nil, Seq termX termY))
         _   => Left ((LinearityError ey))

typeCheck curr (Not fc x y)
  = do (TyPort (OUTPUT,LOGIC) ** cx ** (ex,termX)) <- typeCheck curr x
         | (ty ** cx ** (ex,termX))
             => Left (Err fc (Mismatch (TyPort (OUTPUT,LOGIC)) ty))

       (TyPort (INPUT,LOGIC) ** cy ** (ey,termY)) <- typeCheck ex y
         | (ty ** cy ** (ey,termY))
             => Left (Err fc (Mismatch (TyPort (INPUT,LOGIC)) ty))

       pure (TyGate ** cy ** (ey,Not termX termY))

typeCheck curr (Gate fc k x y z)
  = do (TyPort (OUTPUT,LOGIC) ** cx ** (ex,termX)) <- typeCheck curr x
         | (ty ** cx ** (ex,termX)) => Left (Err fc (Mismatch (TyPort (OUTPUT, LOGIC)) ty))

       (TyPort (INPUT,LOGIC) ** cy ** (ey,termY)) <- typeCheck ex y
         | (ty ** cy ** (ey,termY))
             => Left (Err fc (Mismatch (TyPort (INPUT,LOGIC)) ty))

       (TyPort (INPUT,LOGIC) ** cz ** (ez,termZ)) <- typeCheck ey z
         | (ty ** cz ** (ez,termZ))
             => Left (Err fc (Mismatch (TyPort (INPUT,LOGIC)) ty))

       pure (TyGate ** cz ** (ez,Gate k termX termY termZ))

typeCheck curr (Mux fc v x y z)
  = do (TyPort (OUTPUT,dtypeA) ** cv ** (ev,termV)) <- typeCheck curr v
                  | ty => Left (Err fc (PortExpected OUTPUT))

       (TyPort (INPUT,LOGIC) ** cx ** (ex,termX)) <- typeCheck ev x
                  | (ty ** cx ** (ex,termX))
                       => Left (Err fc (Mismatch (TyPort (INPUT,LOGIC)) ty))

       (TyPort (INPUT,dtypeB) ** cy ** (ey,termY)) <- typeCheck ex y
                  | ty => Left (Err fc (PortExpected INPUT))

       (TyPort (INPUT,dtypeC) ** cz ** (ez,termZ)) <- typeCheck ey z
                  | ty => Left (Err fc (PortExpected INPUT))

       Refl <- lift (decEq dtypeA dtypeB)
                    (Err fc (MismatchGate dtypeA dtypeB))

       Refl <- lift (decEq dtypeB dtypeC)
                    (Err fc (MismatchGate dtypeA dtypeC))

       pure (TyGate ** cz ** (ez,Mux termV termX termY termZ))

typeCheck curr (IndexS fc o i)
  = do (TyPort (OUTPUT,dtypeO) ** co ** (eo,termO)) <- typeCheck curr o
                  | ty => Left (Err fc (PortExpected OUTPUT))

       (TyPort (INPUT,BVECT (W (S Z) ItIsSucc) dtypeI) ** ci ** (ei,termI)) <- typeCheck eo i
                  | (TyPort (INPUT, BVECT s type) ** cx ** (ex,termX))
                       => Left (Err fc (Mismatch (TyPort (INPUT,BVECT (W (S Z) ItIsSucc) type)) (TyPort (INPUT, BVECT s type))))
                  | ty => Left (Err fc (PortExpected INPUT))

       Refl <- lift (decEq dtypeO dtypeI)
                    (Err fc (MismatchGate dtypeO  dtypeI))

       pure (TyGate ** ci ** (ei,IndexSingleton termO termI))

typeCheck curr (IndexE fc k a b i)
  = do (TyPort (OUTPUT,dtypeA) ** cA ** (eA,termA)) <- typeCheck curr a
                  | ty => Left (Err fc (PortExpected OUTPUT))

       (TyPort (OUTPUT,BVECT free dtypeB) ** cB ** (eB,termB)) <- typeCheck eA b
                  | ty => Left (Err fc (PortExpected OUTPUT))

       (TyPort (INPUT,BVECT size dtypeC) ** cC ** (eC,termC)) <- typeCheck eB i
                  | ty => Left (Err fc (PortExpected INPUT))

       Refl <- lift (decEq dtypeA dtypeB)
                    (Err fc (MismatchGate dtypeA dtypeB))

       Refl <- lift (decEq dtypeB dtypeC)
                    (Err fc (MismatchGate dtypeB dtypeC))

       let p = case k of { F => minus (toNat size) 1; L => 0}

       (s ** prf) <- Info.lift (EdgeCase.index size p)
                               (Err fc (NotEdgeCase (InvalidEdge (toNat size) (S Z) (toNat free))))

       Refl <- lift (decEq free s)
                    (Err fc (NotEdgeCase (InvalidEdge (toNat size) (S Z) (toNat free))))

       pure (TyGate ** cC ** (eC,IndexEdge p prf termA termB termC))

typeCheck curr (IndexP fc p a b c i)
  = do (TyPort (OUTPUT,dtypeA) ** cA ** (eA,termA)) <- typeCheck curr a
                  | ty => Left (Err fc (PortExpected OUTPUT))

       (TyPort (OUTPUT,BVECT freeB dtypeB) ** cB ** (eB,termB)) <- typeCheck eA b
                  | ty => Left (Err fc (PortExpected OUTPUT))

       (TyPort (OUTPUT,BVECT freeC dtypeC) ** cC ** (eC,termC)) <- typeCheck eB c
                  | ty => Left (Err fc (PortExpected OUTPUT))

       (TyPort (INPUT,BVECT size dtypeD) ** cI ** (eI,termI)) <- typeCheck eC i
                  | ty => Left (Err fc (PortExpected INPUT))

       Refl <- lift (decEq dtypeA dtypeB)
                    (Err fc (MismatchGate dtypeA (BVECT freeB dtypeB)))

       Refl <- lift (decEq dtypeB dtypeC)
                    (Err fc (MismatchGate (BVECT freeB dtypeB) (BVECT freeC dtypeC)))

       Refl <- lift (decEq dtypeC dtypeD)
                    (Err fc (MismatchGate (BVECT freeC dtypeC) (BVECT size dtypeD)))

       (a ** b ** prf) <- Info.lift (Pivot.index p size)
                                    (Err fc (NotEdgeCase (InvalidSplit p (toNat size) (toNat freeB) (toNat freeC))))

       Refl <- lift (decEq freeB a)
                    (Err fc (MismatchGate (BVECT a     dtypeB)
                                          (BVECT freeB dtypeB)))

       Refl <- lift (decEq freeC b)
                    (Err fc (MismatchGate (BVECT b     dtypeB)
                                          (BVECT freeC dtypeB)))

       pure (TyGate ** cI ** (eI,IndexSplit p prf termA termB termC termI))

typeCheck curr (MergeS fc o i)
  = do (TyPort (OUTPUT,BVECT (W (S Z) ItIsSucc) dtypeO) ** cO ** (eO,termO)) <- typeCheck curr o
           | (TyPort (INPUT, BVECT s type) ** cx ** (ex,termX))
                => Left (Err fc (Mismatch (TyPort (OUTPUT, BVECT (W (S Z) ItIsSucc) type))
                                          (TyPort (INPUT,  BVECT s                  type))))
           | ty => Left (Err fc (PortExpected OUTPUT))

       (TyPort (INPUT, dtypeI) ** cI ** (eI, termI)) <- typeCheck eO i
           | ty => Left (Err fc (PortExpected INPUT))

       Refl <- lift (decEq dtypeO dtypeI)
                    (Err fc (MismatchGate dtypeO dtypeI))

       pure (TyGate ** cI ** (eI, MergeSingleton termO termI))

typeCheck curr (MergeV fc o a b)
  = do (TyPort (OUTPUT, dtypeO) ** cO ** (eO, termO)) <- typeCheck curr o
           | ty => Left (Err fc (PortExpected OUTPUT))

       (TyPort (INPUT, dtypeA) ** cA ** (eA, termA)) <- typeCheck eO a
           | ty => Left (Err fc (PortExpected INPUT))

       (TyPort (INPUT, dtypeB) ** cB ** (eB, termB)) <- typeCheck eA b
           | ty => Left (Err fc (PortExpected INPUT))

       case Views.allEqual LOGIC dtypeA dtypeB of
            -- Case when merging two logic wires into a vector of size two
            (Yes AE) =>
              do Refl <- lift (decEq dtypeO (BVECT (W (S (S Z)) ItIsSucc) LOGIC))
                              (Err fc (MismatchGate (BVECT (W (S (S Z)) ItIsSucc) LOGIC)
                                                    dtypeO))

                 pure (TyGate ** cB ** (eB, Merge2L2V termO termA termB))

            -- Case when merging two vectors. coudl be cleaner.
            (No msgWhyNot prfWhyNot) =>
                case dtypeO of
                  LOGIC => Left (Err fc VectorExpected)
                  BVECT sizeO typeO =>
                    case dtypeA of
                      LOGIC => Left (Err fc VectorExpected)
                      BVECT sizeA typeA =>
                        case dtypeB of
                          LOGIC => Left (Err fc VectorExpected)
                          BVECT sizeB typeB =>
                            do prfSize <- lift (isPlus sizeA sizeB sizeO)
                                               (Err fc (VectorSizeMismatch sizeO sizeA sizeB))
                               AE <- allEqual fc typeO typeA typeB

                               pure (TyGate ** cB ** (eB, Merge2V2V prfSize termO termA termB))

typeCheck curr (Stop fc) with (used curr)
  typeCheck curr (Stop fc) | (Yes prf) = Right (TyUnit ** _ ** (Nil, Stop prf))
  typeCheck curr (Stop fc) | (No contra) = Left (Err fc (LinearityError curr))

namespace Design
  export
  typeCheck : (ast : AST) -> TyCheck (Term Nil TyUnit Nil)
  typeCheck ast with (typeCheck Nil ast)
    typeCheck ast | (Left x) = Left x
    typeCheck ast | (Right (MkDPair TyUnit (MkDPair Nil (env,term)))) = Right term
    typeCheck ast | (Right (MkDPair ty snd)) = Left (Mismatch TyUnit ty)

  export
  typeCheckIO : (ast : AST) -> IO (TyCheck (Term Nil TyUnit Nil))
  typeCheckIO ast = pure (typeCheck ast)

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Graphics.Util.Color

%access public export

data Color : Type where
  RGBA : (red: Double) -> (green: Double) -> (blue: Double) -> (alpha: Double) -> Color

max_stars_repo_name: spearman/gl-idris

max_issues_repo_name: spearman/gl-idris

max_forks_repo_name: spearman/gl-idris


text:
module Tree

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

Functor Tree where
  map func Empty = Empty
  map func (Node l el r) = Node (map func l) (func el) (map func r)


text:
module Text.Markup.Edda.Model.Raw

import Data.AVL.Dict

import Text.Markup.Edda.Model.Common

%default total
%access public export

data EddaRaw : EddaTy -> Type where
-- ------------------------------------------------------------------ [ Inline ]
-- --------------------------------------------------------------------- [ Raw ]
  Font : (ty : FontTy)
      -> (word : String)
      -> EddaRaw INLINE
  Punc : (c : Char)
      -> EddaRaw INLINE

  Link : (ty : LinkTy)
      -> (url  : String )
      -> (desc : List (EddaRaw INLINE))
      -> EddaRaw INLINE

  Mark : (ty   : MarkupTy)
      -> (text : List (EddaRaw INLINE))
      -> EddaRaw INLINE

  Raw  : (ty   : RawTy)
      -> (verb : String)
      -> EddaRaw INLINE

-- ------------------------------------------------------------------ [ Blocks ]

  HRule : EddaRaw BLOCK
  Empty : EddaRaw BLOCK

  Figure : (label   : Maybe String)
        -> (caption : List (EddaRaw INLINE))
        -> (attrs   : Dict String String)
        -> (link    : EddaRaw INLINE)

        -> EddaRaw BLOCK

  DList : (kvpairs : List (List (EddaRaw INLINE), List (EddaRaw INLINE)))
       -> EddaRaw BLOCK

  Heading : (depth : Nat)
         -> (label : Maybe String)
         -> (title : List (EddaRaw INLINE))
         -> (attrs : Dict String String)
         -> EddaRaw BLOCK

  TextBlock : (ty : TextBlockTy)
           -> (label : Maybe String)
           -> (title : List (EddaRaw INLINE))
           -> (attrs : Dict String String)
           -> (text  : List (EddaRaw INLINE))
           -> EddaRaw BLOCK

  VerbBlock : (ty      : VerbBlockTy)
           -> (label   : Maybe String)
           -> (caption : List (EddaRaw INLINE))
           -> (attrs   : Dict String String)
           -> (content : String)
           -> EddaRaw BLOCK

  ListBlock : (ty : ListTy)
           -> (items : List (List (EddaRaw INLINE)))
           -> EddaRaw BLOCK

  Snippet : (content : List $ EddaRaw a)
         -> (prf : ValidSnippet a)
         -> EddaRaw SNIPPET

  Doc : (title : List (EddaRaw INLINE)) -- @TODO resolve author and dates
     -> (attrs : Dict String String)
     -> (body  : List (EddaRaw BLOCK))
     -> EddaRaw DOC

implementation Show QuoteTy where
  show SQuote = "SQuote"
  show DQuote = "DQuote"

implementation Show CiteSty where
  show ParenSty = "ParenCite"
  show TextSty  = "TextCite"

implementation Show ParenTy where
  show Parents = "Parens"
  show Brackets = "Brackets"
  show Braces = "Braces"

implementation Show FontTy where
  show SerifTy = "Serif"
  show SansTy  = "Sans"
  show ScapTy  = "SmallCaps"
  show MonoTy  = "Monospaced"

implementation Show LinkTy where
  show HyperTy   = "HyperLink"
  show ExposedTy = "Exposed"
  show FnoteTy   = "Footnote"
  show RefTy     = "Internal"
  show CiteTy    = "Citation"

implementation Show MarkupTy where
  show BoldTy   = "Strong"
  show EmphTy   = "Emph"
  show StrikeTy = "Strike"
  show UlineTy  = "Uline"

implementation Show RawTy where
  show VerbTy = "Verb"
  show CodeTy = "Code"
  show MathTy = "Math"

implementation Show TextBlockTy where
  show ParaTy        = "PARAGRAPH"
  show TheoremTy     = "THEOREM"
  show CorollaryTy   = "COROLLARY"
  show LemmaTy       = "LEMMA"
  show PropositionTy = "PROPOSITION"
  show ProofTy       = "PROOF"
  show DefinitionTy  = "DEFINITION"
  show ExampleTy     = "EXAMPLE"
  show ExerciseTy    = "EXERCISE"
  show NoteTy        = "NOTE"
  show ProblemTy     = "PROBLEM"
  show QuestionTy    = "QUESTION"
  show RemarkTy      = "REMARK"
  show SolutionTy    = "SOLUTION"
  show QuotationTy   = "QUOTATION"

implementation Show VerbBlockTy where
  show CommentTy  = "COMMENT"
  show ListingTy  = "LISTING"
  show LiteralTy  = "LITERTAL"
  show EquationTy = "EQUATION"

implementation Show ListTy where
  show BulletTy = "Bullet"
  show NumberTy = "Number"

private
partial
showInline : EddaRaw INLINE -> String
showInline (Punc c)    = unwords ["{Punc", show c,  "}"]
showInline (Font ty t) = unwords ["{Font", show ty, show t, "}"]
showInline (Raw ty t)  = unwords ["{Raw",  show ty, show t, "}"]

showInline (Mark ty ts) = unwords ["{Mark"
                                      , show ty
                                      , concatMap showInline ts
                                      , "}"]

showInline (Link ty u ts) = unwords ["{Link"
                                        , show ty
                                        , "<" ++ u ++ ">"
                                        , show $ concatMap showInline ts
                                        , "}"]

private
partial
showBlock : EddaRaw BLOCK -> String
showBlock (HRule) = "[HRule]"
showBlock (Empty) = "[Empty]"
showBlock (TextBlock ty lab cap as txt) = unwords
    ["[TextBlock"
    , show ty
    , show lab
    , concatMap showInline cap
    , show as
    , concatMap showInline txt
    , "]"]
showBlock (VerbBlock ty lab cap as txt) = unwords
    ["[VerbBlock"
    , show ty
    , show lab
    , concatMap showInline cap
    , show as
    , show txt
    , "]"]
showBlock (ListBlock ty iis) = unwords
    [ "[BList"
    , show ty
    , concatMap (\is => unwords ["[Item", concatMap showInline is, "]"]) iis
    , "]"]
showBlock (Heading d l t a) = unwords
    [ "[Heading"
    , show d
    , show l
    , concatMap showInline t
    , show a
    , "]"]
showBlock (Figure l c as img) = unwords
    [ "[Figure"
    , show l
    , concatMap showInline c
    , show as
    , showInline img
    , "]"]
showBlock (DList ds) = unwords
    [ "[DList"
    , concatMap (\(k,vs) => concatMap showInline k ++ " " ++ concatMap showInline vs) ds
    , "]"]

Show (EddaRaw ty) where
  show x {ty = INLINE} = assert_total $ showInline x
  show x {ty = BLOCK} = assert_total $ showBlock x
  show (Snippet content prf) {ty = SNIPPET} with (prf)
    show (Snippet content prf) {ty = SNIPPET} | IsInLine =
      assert_total $ unwords $ ["[Snippet "] ++ [show content] ++ [" IsInLine]"]
    show (Snippet content prf) {ty = SNIPPET} | IsBlock =
      assert_total $ unwords $ ["[Snippet "] ++ [show content] ++ [" IsBlock]"]

  show (Doc title attrs body) {ty = DOC} =
     assert_total $ unwords $ ["[Doc "] ++ [show title, show attrs, show body] ++ ["]"]

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
module TyTTP.Core.Routing

import Control.Monad.Maybe
import TyTTP.Core.Step

export
routes : Alternative m
  => List (
    Step me u h1 s h2 a b
    -> m $ Step me' p' h1' s' h2' a' b'
  )
  -> Step me u h1 s h2 a b
  -> m $ Step me' p' h1' s' h2' a' b'
routes handlers step = choiceMap ($ step) handlers

export
routes' : Monad m
  => (
    Step me u h1 s h2 a b
    -> m $ Step me' p' h1' s' h2' a' b'
  )
  -> List (
    Step me u h1 s h2 a b
    -> MaybeT m $ Step me' p' h1' s' h2' a' b'
  )
  -> Step me u h1 s h2 a b
  -> m $ Step me' p' h1' s' h2' a' b'
routes' def handlers step = do
  Just result <- runMaybeT $ routes handlers step
    | Nothing => def step
  pure result

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
import Control.Monad.State

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

testTree : Tree String
testTree = Node (Node (Node Empty "Jim" Empty) "Fred"
                      (Node Empty "Sheila" Empty)) "Alice"
                (Node Empty "Bob" (Node Empty "Eve" Empty))

-- Exercise 1

update : (stateType -> stateType) -> State stateType ()
update f = do st <- get
              put (f st)

increment : Nat -> State Nat ()
increment x = update (+x)

-- Exercise 2

countEmpty : Tree a -> State Nat ()
countEmpty Empty = update (+1)
countEmpty (Node left val right) = do countEmpty left
                                      countEmpty right

-- Exercise 3

countEmptyNode : Tree a -> State (Nat, Nat) ()
countEmptyNode Empty = do (empty, nodes) <- get
                          put (empty + 1, nodes)
countEmptyNode (Node left val right) = do countEmptyNode left
                                          (empty, nodes) <- get
                                          put (empty, nodes + 1)
                                          countEmptyNode right


text:
-- Exercise 1
{-
   (String, String, String)
   List String
   ((Char, String), Char)

-}

-- Exercise 2

palindrome : String -> Bool
palindrome str = str == reverse str

-- Exercise 3

palindrome_q3 : String -> Bool
palindrome_q3 str = let strL = toLower str in
                        strL == reverse strL

-- Exercise 4

palindrome_q4 : String -> Bool
palindrome_q4 str = if length str > 10
                       then palindrome_q3 str
                       else False

-- Exercise 5

palindrome_q5 : Nat -> String -> Bool
palindrome_q5 min str = if length str > min
                           then palindrome_q3 str
                           else False

-- Exercise 6

counts : String -> (Nat, Nat)
counts str = (length (words str), length str)

-- Exercise 7

top_ten : Ord a => List a -> List a
top_ten xs = take 10 (reverse (sort xs))

-- Exercise 8

over_length : Nat -> List String -> Nat
over_length num xs = let lengths = map length xs in
                         length (filter (> num) lengths)


text:
> module SequentialDecisionProblems.FastStochasticDefaults

> import SequentialDecisionProblems.CoreTheory
> import SequentialDecisionProblems.Utils

> import FastSimpleProb.SimpleProb
> import FastSimpleProb.MonadicOperations
> import FastSimpleProb.MonadicProperties

> %default total
> %auto_implicits off

In stochastic SDPs, |M = SimpleProb|:

> SequentialDecisionProblems.CoreTheory.M =
>   SimpleProb

Thus, |M| is a functor:

> SequentialDecisionProblems.CoreTheory.fmap =
>   FastSimpleProb.MonadicOperations.fmap

, |M| is a monad:

> SequentialDecisionProblems.Utils.ret =
>   FastSimpleProb.MonadicOperations.ret

> SequentialDecisionProblems.Utils.bind =
>   FastSimpleProb.MonadicOperations.bind

Moreover, |M| is a container monad

> SequentialDecisionProblems.CoreTheory.Elem =
>   FastSimpleProb.MonadicOperations.Elem

> SequentialDecisionProblems.CoreTheory.NotEmpty =
>   FastSimpleProb.MonadicOperations.NonEmpty

> SequentialDecisionProblems.CoreTheory.All =
>   FastSimpleProb.MonadicOperations.All

> SequentialDecisionProblems.CoreTheory.elemNotEmptySpec0 =
>   FastSimpleProb.MonadicProperties.elemNonEmptySpec0

> SequentialDecisionProblems.CoreTheory.elemNotEmptySpec1 =
>   FastSimpleProb.MonadicProperties.elemNonEmptySpec1

> SequentialDecisionProblems.CoreTheory.tagElem =
>   FastSimpleProb.MonadicOperations.tagElem

> SequentialDecisionProblems.CoreTheory.allElemSpec0 =
>   FastSimpleProb.MonadicProperties.containerMonadSpec3

and |All| and |NotEmpty| are finite and decidable:

> SequentialDecisionProblems.Utils.finiteAll =
>   FastSimpleProb.MonadicProperties.finiteAll

> SequentialDecisionProblems.Utils.finiteNotEmpty =
>   FastSimpleProb.MonadicProperties.finiteNonEmpty

> SequentialDecisionProblems.Utils.decidableAll =
>   FastSimpleProb.MonadicProperties.decidableAll

> SequentialDecisionProblems.Utils.decidableNotEmpty =
>   FastSimpleProb.MonadicProperties.decidableNonEmpty

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Compo

import Halfer
import Incrementer

||| Composition of incrementer . halfer . ?hole, where the registry
||| will be in charge of filling the hole.
|||
||| TODO: ultimately Idris could fill such hole, thus maybe we want
||| the registry to heavely rely on such a capability of Idris.
export
compo : Integer -> Integer
compo = incrementer . (halfer . ?hole)

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
module IdrisJvm.IR.Types

%access public export

%hide Language.Reflection.ArithTy
%hide Language.Reflection.IntTy
%hide Language.Reflection.NativeTy
%hide Language.Reflection.Const

data LVar = Loc Int | Glob String

Show LVar where
  show (Loc loc) = "Loc " ++ show loc
  show (Glob s) = "Glob " ++ s

data CaseType = Updatable | Shared

Show CaseType where
  show Updatable = "Updatable"
  show Shared = "Shared"

data FDesc = FCon String
           | FStr String
           | FUnknown
           | FIO FDesc
           | FApp String (List FDesc)

Show FDesc where
  show (FCon s) = "FCon(" ++ s ++ ")"
  show (FStr s) = "FStr(" ++ s ++ ")"
  show FUnknown = "FUnknown"
  show (FIO fdesc) = "FIO(" ++ show fdesc ++ ")"
  show (FApp f descs) = concat $ the (List String) ["FApp(", f, ", ", show descs, ")"]

mutual
  data SExp = SV LVar
            | SApp Bool String (List LVar)
            | SLet LVar SExp SExp
            | SUpdate LVar SExp
            | SCon (Maybe LVar) -- location to reallocate, if available
                   Int String (List LVar)
            | SCase CaseType LVar (List SAlt)
            | SChkCase LVar (List SAlt)
            | SProj LVar Int
            | SConst Const
            -- Keep DExps for describing foreign things, because they get
            -- translated differently
            | SForeign FDesc FDesc (List (FDesc, LVar))
            | SOp PrimFn (List LVar)
            | SNothing -- erased value, will never be inspected
            | SError String

  data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy
              | LUDiv IntTy | LSDiv ArithTy | LURem IntTy | LSRem ArithTy
              | LAnd IntTy | LOr IntTy | LXOr IntTy | LCompl IntTy
              | LSHL IntTy | LLSHR IntTy | LASHR IntTy
              | LEq ArithTy | LLt IntTy | LLe IntTy | LGt IntTy | LGe IntTy
              | LSLt ArithTy | LSLe ArithTy | LSGt ArithTy | LSGe ArithTy
              | LSExt IntTy IntTy | LZExt IntTy IntTy | LTrunc IntTy IntTy
              | LStrConcat | LStrLt | LStrEq | LStrLen
              | LIntFloat IntTy | LFloatInt IntTy | LIntStr IntTy | LStrInt IntTy
              | LFloatStr | LStrFloat | LChInt IntTy | LIntCh IntTy
              | LBitCast ArithTy ArithTy -- Only for values of equal width

              | LFExp | LFLog | LFSin | LFCos | LFTan | LFASin | LFACos | LFATan
              | LFSqrt | LFFloor | LFCeil | LFNegate

              | LStrHead | LStrTail | LStrCons | LStrIndex | LStrRev | LStrSubstr
              | LReadStr | LWriteStr

              -- system info
              | LSystemInfo

              | LFork
              | LPar -- evaluate argument anywhere, possibly on another
                     -- core or another machine. 'id' is a valid implementation
              | LExternal String
              | LCrash

              | LNoOp

  data SDecl = SFun String (List String) Int SExp

  data SAlt = SConCase Int Int String (List String) SExp
            | SConstCase Const SExp
            | SDefaultCase SExp

  data NativeTy = IT8 | IT16 | IT32 | IT64

  data IntTy = ITFixed NativeTy | ITNative | ITBig | ITChar

  data ArithTy = ATInt IntTy | ATFloat

  data Const = I Int | BI String | Fl Double | Ch Char | Str String
             | B8 Bits8 | B16 Bits16 | B32 Int | B64 Bits64
             | AType ArithTy | StrType
             | WorldType | TheWorld
             | VoidType | Forgot

itBitsName : NativeTy -> String
itBitsName IT8 = "Bits8"
itBitsName IT16 = "Bits16"
itBitsName IT32 = "Bits32"
itBitsName IT64 = "Bits64"

Show NativeTy where
  show IT8 = "IT8"
  show IT16 = "IT16"
  show IT32 = "IT32"
  show IT64 = "IT64"

Show IntTy where
  show (ITFixed nativeTy) = "ITFixed " ++ show nativeTy
  show ITNative = "ITNative"
  show ITBig = "ITBig"
  show ITChar = "ITChar"

Show ArithTy where
  show (ATInt intTy) = "ATInt " ++ show intTy
  show ATFloat = "ATFloat"

Show Const where
  show (I i) = show i
  show (BI i) = show i
  show (Fl f) = show f
  show (Ch c) = show c
  show (Str s) = show s
  show (B8 x) = show x
  show (B16 x) = show x
  show (B32 x) = show x
  show (B64 x) = show x
  show (AType ATFloat) = "Double"
  show (AType (ATInt ITBig)) = "Integer"
  show (AType (ATInt ITNative)) = "Int"
  show (AType (ATInt ITChar)) = "Char"
  show (AType (ATInt (ITFixed it))) = itBitsName it
  show TheWorld = "prim__TheWorld"
  show WorldType = "prim__WorldType"
  show StrType = "String"
  show VoidType = "Void"
  show Forgot = "Forgot"

data Export = ExportData FDesc -- Exported data descriptor (usually string)
            | ExportFun String -- Idris name
                        FDesc -- Exported function descriptor
                        FDesc -- Return type descriptor
                        (List FDesc) -- Argument types

data ExportIFace = MkExportIFace String -- FFI descriptor
                                 String -- interface file
                                 (List Export)

Show PrimFn where
  show (LPlus a) = "LPlus " ++ show a
  show (LMinus a) = "LPlus " ++ show a
  show (LTimes a) = "LPlus " ++ show a
  show (LUDiv a) = "LUDiv " ++ show a
  show (LSDiv a) = "LSDiv " ++ show a
  show (LURem a) = "LURem " ++ show a
  show (LSRem a) = "LSRem " ++ show a
  show (LAnd a) = "LAnd " ++ show a
  show (LOr a) = "LOr " ++ show a
  show (LXOr a) = "LXOr " ++ show a
  show (LCompl a) = "LCompl " ++ show a
  show (LSHL a) = "LSHL " ++ show a
  show (LLSHR a) = "LLSHR " ++ show a
  show (LASHR a) = "LASHR " ++ show a
  show (LEq a) = "LEq " ++ show a
  show (LLt a) = "LLt " ++ show a
  show (LLe a) = "LLe " ++ show a
  show (LGt a) = "LGt " ++ show a
  show (LGe a) = "LGe " ++ show a
  show (LSLt a) = "LSLt " ++ show a
  show (LSLe a) = "LSLe " ++ show a
  show (LSGt a) = "LSGt " ++ show a
  show (LSGe a) = "LSGe " ++ show a
  show (LSExt a b) = "LSExt (" ++ show a ++ ", " ++ show b ++ ")"
  show (LZExt a b) = "LZExt (" ++ show a ++ ", " ++ show b ++ ")"
  show (LTrunc a b) = "LTrunc (" ++ show a ++ ", " ++ show b ++ ")"
  show LStrConcat = "LStrConcat"
  show LStrLt = "LStrLt"
  show LStrEq = "LStrEq"
  show LStrLen = "LStrLen"
  show (LIntFloat a) = "LIntFloat " ++ show a
  show (LFloatInt a) = "LFloatInt " ++ show a
  show (LIntStr a) = "LIntStr " ++ show a
  show (LStrInt a) = "LStrInt " ++ show a
  show LFloatStr = "LFloatStr"
  show LStrFloat = "LStrFloat"
  show (LChInt a) = "LChInt " ++ show a
  show (LIntCh a) = "LIntCh " ++ show a
  show (LBitCast a b) = "LBitCast (" ++ show a ++ ", " ++ show b ++ ")"
  show LFExp = "LFExp"
  show LFLog = "LFLog"
  show LFSin = "LFSin"
  show LFCos = "LFCos"
  show LFTan = "LFTan"
  show LFASin = "LFASin"
  show LFACos = "LFACos"
  show LFATan = "LFATan"
  show LFSqrt = "LFSqrt"
  show LFFloor = "LFFloor"
  show LFCeil = "LFCeil"
  show LFNegate = "LFNegate"
  show LStrHead = "LStrHead"
  show LStrTail = "LStrTail"
  show LStrCons = "LStrCons"
  show LStrIndex = "LStrIndex"
  show LStrRev = "LStrRev"
  show LStrSubstr = "LStrSubstr"
  show LReadStr = "LReadStr"
  show LWriteStr = "LWriteStr"
  show LSystemInfo = "LSystemInfo"
  show LFork = "LFork"
  show LPar = "LPar"
  show (LExternal s) = "LExternal " ++ s
  show LCrash = "LCrash"
  show LNoOp = "LNoOp"

Show Export where
  show (ExportData fdesc) = "ExportData(" ++ show fdesc ++ ")"
  show (ExportFun f desc retDesc argDescs)
    = "ExportFun(" ++ f ++ ", " ++ show desc ++ ", " ++ show retDesc ++ ", " ++ show argDescs ++ ")"

Show ExportIFace where
  show (MkExportIFace desc f exports) = "MKExportIFace(" ++ desc ++ ", " ++ f ++ ", " ++ show exports ++ ")"

isTypeConst : Const -> Bool
isTypeConst (AType _) = True
isTypeConst StrType = True
isTypeConst WorldType = True
isTypeConst VoidType = True
isTypeConst _ = False


text:
module Test.Main

-- contrib
import Decidable.Order
import Test.Unit

-- Fast really_believe_me implementation of Ordered for Int
import Decidable.IntOrder

-- data structures
import Data.Vect
import Data.LeftistHeap
import Data.OrderedVect
import Data.MergeList
import Data.LazyPairingHeap
import Data.VectRankedElem
import Data.Queue
import Data.BinarySearchTree
import Data.RandomAccessList

%default total

-- taken from the Type-Driven Development book
randoms : Int -> Stream Int
randoms seed = let seed' = 1664525 * seed + 1013904223 in
               (seed' `shiftR` 2) :: randoms seed'

namespace CountedOrderedVect
  toVect : {constraint : Ordered Int LTE} -> (cnt : Nat ** Lazy $ MergeList 1 cnt constraint) -> (cnt ** OrderedVect cnt constraint)
  toVect (cnt ** xs) = (cnt ** mergeListToOrderedVect 1 cnt xs)
  head : {constraint : Ordered Int LTE} -> (cnt ** OrderedVect cnt constraint) -> Maybe Int
  head (Z ** Nil) = Nothing
  head (_ ** x::xs) = Just x
  tail : {constraint : Ordered Int LTE} -> (cnt ** OrderedVect cnt constraint) -> (cnt ** OrderedVect cnt constraint)
  tail (Z ** Nil) = (Z ** [])
  tail (S cnt ** x::xs) = (cnt ** xs)

||| Showcase basic operations on the various data structures in this module
||| and verify that proofs are erased as expected:
|||
|||     idris --warnreach --testpkg data.ipkg
export
mainTests : IO ()
mainTests
  = do putStrLn "Start"
       let l = take 10000 $ randoms 42
       let leftistHeap = foldl (flip insert) emptyHeap l
       let mergeList = foldl CountedMergeList.insert emptyMergeList l
       let pairingHeap = foldl CountedPairingHeap.insert emptyPairingHeap l
       let binaryTree = foldl BinarySearchTree.insert emptyBinaryTree l
       let countedRandomAccessList = foldl (flip CountedRandomAccessList.cons) CountedRandomAccessList.empty l
       putStrLn "Results: "
       putStrLn $ show $ findMin $ deleteMin leftistHeap
       putStrLn $ show $ count $ leftistHeap

       -- putStrLn $ show $ CountedOrderedVect.head $ tail $ toVect mergeList
       -- ^ broken on Idris 1.3.1, works on 1.3.0
       -- A more modest alternative:
       let mergeList' = foldl CountedMergeList.insert emptyMergeList $ take 1000 l
       putStrLn $ show $ CountedOrderedVect.head $ tail $ toVect mergeList'

       putStrLn $ show $ CountedPairingHeap.findMin $ deleteMin pairingHeap
       putStrLn $ show $ head $ VectRankedElem.cons 0 $ rev $ [1, 2, 3] `concat` [4, 5]
       putStrLn $ show $ Queue.head $ tail queue

       -- putStrLn $ show $ 1 `elem` binaryTree
       -- ^ broken on Idris 1.3.0, works on 1.3.1
       -- See https://github.com/idris-lang/Idris-dev/issues/4090
       -- Nat.LTE alternative:
       let emptyNatTree = emptyBinaryTree {ty = Nat} {rel = Nat.LTE}
       let natTree = foldl BinarySearchTree.insert emptyNatTree (the (List Nat) [0, 1, 2])
       putStrLn $ show $ 1 `elem` natTree

       putStrLn $ show $ the (Maybe Int) $ CountedRandomAccessList.index 2 $ CountedRandomAccessList.tail $ CountedRandomAccessList.update 2 countedRandomAccessList (const (the Int 42))
       putStrLn "End"
       pure ()
  where
    emptyHeap : {auto constraint : Ordered Int LTE} -> CountedHeap constraint
    emptyHeap = empty
    emptyMergeList : {auto constraint : Ordered Int LTE} -> CountedMergeList 1 constraint
    emptyMergeList = empty
    emptyPairingHeap : {auto constraint : Ordered Int LTE} -> CountedPairingHeap constraint
    emptyPairingHeap = CountedPairingHeap.empty
    queue : Queue 4 Int
    queue = snoc (snoc (snoc (snoc empty 1) 2) 3) 4
    emptyBinaryTree : {default Int ty : Type} -> {default LTE rel : ty -> ty -> Type} ->
                      {auto constraint : Ordered ty rel} -> (len : Nat ** BinarySearchTree constraint len)
    emptyBinaryTree = (Z ** Empty)

export
randomAccessListTests : IO ()
randomAccessListTests
  = do runTests $
         [ assertEquals (at (n + 1)) Nothing ] ++
         (flip map) range (\i => assertEquals (at i) $ Just (n `minus` i))
  where n : Nat
        n = 6
        range : List Nat
        range = [0..n]
        ral : CountedRandomAccessList Nat
        ral = foldl (flip cons) CountedRandomAccessList.empty range
        at : Nat -> Maybe Nat
        at = (`index` ral)

max_stars_repo_name: jdevuyst/idris-data

max_issues_repo_name: jdevuyst/idris-data

max_forks_repo_name: jdevuyst/idris-data


text:
> module Nat.Divisor

> import Pairs.Operations

> %default total

> %access public export

> Divisor : (m : Nat) -> (n : Nat) -> Type
> Divisor m n = Subset Nat (\ q => m * q = n)


text:
module Data.Bytes.Prim

import Data.Bytes.Util

import Data.Buffer

import Data.Word.Word8

moduleName : String
moduleName = "Data.Bytes.Prim"

---------------------------------------------------------------------
-- Operations on blocks of memory
---------------------------------------------------------------------

-- Should probably be a newtype
export
Block : Type
Block = Buffer

-- This is only useable so long as idris2 prefers scheme as the backend. It'd
-- be better to add this equivalent to Data.Buffer in base so that backend
-- makers are incentivised to support it broadly.
%foreign "scheme:eq?"
prim_exactEqBuff : Buffer -> Buffer -> PrimIO Bool
-- TODO: Check if I can use AnyPtr equality here.

-- Compare if two Blocks are the same object, in the sense of ptr equality.
export
exactEqBlock : Block -> Block -> IO Bool
exactEqBlock x y = primIO $ prim_exactEqBuff x y

export
getByte : Block -> (loc : Int) -> IO Word8
getByte b loc = cast <$> Data.Buffer.getByte b loc

export
blockData : Block -> IO (List Word8)
blockData b = map cast <$> bufferData b

---------------------------------------------------------------------
-- Mutation
---------------------------------------------------------------------

-- Bytes are immutable `Block`s of memory. Here, combined with the allocation
-- functions in the next section, we enforce that the only place we're allowed
-- to mutate a Block is during its creation.

export
data MutBlock = MkMB Block

export
setByte : MutBlock -> Int -> Word8 -> IO ()
setByte (MkMB mb) pos v = Data.Buffer.setByte mb pos (cast v)

export
copyBlock : (src : Block) -> (start, len : Int) ->
            (dest : MutBlock) -> (loc : Int) -> IO ()
copyBlock src start len (MkMB dest) loc
  = Data.Buffer.copyData src start len dest loc

-- Overloading isn't quite up to snuff for this to share the name of getByte,
-- even with namespaces. Still, we might desire to read from a MutBlock so this
-- is provided.
export
getMByte : MutBlock -> (loc : Int) -> IO Word8
getMByte (MkMB mb) loc = cast <$> Data.Buffer.getByte mb loc

---------------------------------------------------------------------
-- Block Allocation
---------------------------------------------------------------------

-- Kind of a weird one, Data.Buffer.newBuffer can't actually return a Nothing
-- currently. 18/5/2020
private
allocateBlock : Int -> IO Block
allocateBlock len
  = do Just block <- newBuffer len
         | Nothing => lieErrorCall moduleName "allocateBlock" "allocation failed"
       pure block

-- NB: The `f`'s below are the only place in Bytes that we can work with a
-- `MutBlock`. The only ways to set bytes that we provide work on
-- `MutBlock`s. This means that only here, where a new Block is being made,
-- can we mutate and ensures the immutability of Bytes.

-- Allocate and then use a function to populate the block.
export
allocateAndFill : Int -> (MutBlock -> IO ()) -> IO Block
allocateAndFill len f = do
  b <- allocateBlock len
  f (MkMB b)
  pure b

-- Allocate and then use a function to populate the block, return some extra
-- value.
export
allocateAndFill' : Int -> (MutBlock -> IO a) -> IO (Block, a)
allocateAndFill' len f = do
  b <- allocateBlock len
  r <- f (MkMB b)
  pure (b,r)

-- Allocate and then use a function to populate the block, return the length of
-- what was filled.
export
allocateAndFillToN : Int -> (MutBlock -> IO Int) -> IO (Block, Int)
allocateAndFillToN len f = do
  b <- allocateBlock len
  i <- f (MkMB b)
  pure (b,i)

-- Allocate and then use a function to populate the block, return the length of
-- what was filled and some extra value.
export
allocateAndFillToN' : Int -> (MutBlock -> IO (Int, a)) -> IO (Block, Int, a)
allocateAndFillToN' len f = do
  b <- allocateBlock len
  (i,a) <- f (MkMB b)
  pure (b,i,a)

-- Allocate and then use a function to populate the block, trim the resulting
-- Block based on the length we actually filled, and return that length.
export
allocateAndTrim : Int -> (MutBlock -> IO Int) -> IO (Block, Int)
allocateAndTrim len f = do
    (xb,len') <- allocateAndFill' len f
    yb <- allocateAndFill len' $ \zb => copyBlock xb 0 len' zb 0
    pure (yb,len')

-- Allocate and then use a function to populate the block, trim the resulting
-- Block based on the slice we actually filled and return that slice and some
-- extra value.
export
allocateAndTrim' : Int -> (MutBlock -> IO (Int,Int,a)) -> IO (Block, (Int,Int), a)
allocateAndTrim' len0 f = do
    (xb, (pos, len, a)) <- allocateAndFill' len0 f
    yb <- allocateAndFill len $ \zb => copyBlock xb pos len zb 0
    pure (yb, (pos,len), a)


text:
module Node.URI

public export
data URIError = MkURIError String

export
%foreign """
  node:lambda:
  s => {
    try {
      const result = decodeURI(s);
      return {
        h: 1, // Right
        a1: result
      };
    } catch(e) {
      return {
        h: 0, // Left
        a1: e.message
      };
    }
  }
  """
decodeURI : String -> Either URIError String

export
%foreign """
  node:lambda:
  s => {
    try {
      const result = decodeURIComponent(s);
      return {
        h: 1, // Right
        a1: result
      };
    } catch(e) {
      return {
        h: 0, // Left
        a1: e.message
      };
    }
  }
  """
decodeURIComponent : String -> Either URIError String

export
%foreign """
  node:lambda:
  s => {
    try {
      const result = encodeURI(s);
      return {
        h: 1, // Right
        a1: result
      };
    } catch(e) {
      return {
        h: 0, // Left
        a1: e.message
      };
    }
  }
  """
encodeURI : String -> Either URIError String

export
%foreign """
  node:lambda:
  s => {
    try {
      const result = encodeURIComponent(s);
      return {
        h: 1, // Right
        a1: result
      };
    } catch(e) {
      return {
        h: 0, // Left
        a1: e.message
      };
    }
  }
  """
encodeURIComponent : String -> Either URIError String


text:
add : Int -> Int -> Int
add x y = x + y


text:
module binary

-- Binary literals

data BinChar : Char -> Type Where
  O : BinChar '0'
  I : BinChar '1'

  data Every : (a -> Type) -> List a -> Type where
    Nil : {P : a -> Type} -> Every P []
    (::) : {P : a -> Type} -> P x -> Every P xs -> Every P (x :: xs)

-- For every BinChar in some list get a natural number
-- How many bits do we have?
fromBinChars : Every Binchar xs -> Nat -> Nat
fromBinChars [] _ = 0
fromBinChars (O :: ys) k = fromBinChats ys (k - 1)
fromBinChats (I :: ys) k = pow 2 k + fromBinChats ys (k - 1)

-- Proof?
b: (s : String) -> {auto p: Every BinChar (unpack s)} -> Nat
-- Use the proof
b {p} s = fromBinChats p (length s - 1)

example1 : b"101" = 5
example1 = refl

max_stars_repo_name: ExpandingShapes/idris-experiments

max_issues_repo_name: ExpandingShapes/idris-experiments

max_forks_repo_name: ExpandingShapes/idris-experiments


text:
module Main

-- add inports
-- convenient for Idris build script
-- forces compiling of all modules

main : IO ()
main = putStrLn "hello idris"

max_stars_repo_name: epicallan/learn-idris

max_issues_repo_name: epicallan/learn-idris

max_forks_repo_name: epicallan/learn-idris


text:
-- PalindromeMain.idr
-- App for checking palindromes

module Main

import Exercises

main : IO ()
main = repl "Enter a string: " (\s => format $ countWithSpace s)
  where
    format : (Nat, Nat) -> String
    format c = "Number of words: " ++ (show (fst c)) ++ ", " ++
               "number of Chars: " ++ (show (snd c)) ++ "\n"

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
module Graphics.Util.Time

%include C "gl_idris.h"
%link C "gl_idris.o"

record Time where
  constructor MicroTime
  seconds : Int
  microseconds : Int

implementation Show Time where
  show (MicroTime seconds useconds) = (show seconds) ++ "." ++ (show useconds)

||| get the current time as a pair of seconds and microseconds since epoch
currentTimeMicros : IO Time
currentTimeMicros
    = do me <- getMyVM
         MkRaw e <-
               foreign FFI_C "idr_currentTimeMicros" (Ptr -> IO (Raw Time)) me
         pure e

implementation Eq Time where
  (MicroTime s1 us1) == (MicroTime s2 us2) = s1 == s2 && us1 == us2

implementation Ord Time where
  compare (MicroTime s1 us1) (MicroTime s2 us2) = if (s1 < s2) then LT
                                                  else if (s1 > s2) then GT
                                                       else compare us1 us2
toMicros : Time -> Integer
toMicros (MicroTime s ms) = (cast s) * 1000000 + (cast ms)

fromMicros : Integer -> Time
fromMicros t = MicroTime (fromInteger $ t `div` 1000000) (fromInteger $ t `mod` 1000000)

difference : Time -> Time -> Time
difference t1 t2 = fromMicros $ (toMicros t1) - (toMicros t2)


text:
module Data.Maybe.Extra

%default total

public export
catMaybes : List (Maybe a) -> List a
catMaybes [] = []
catMaybes (Nothing :: rest) = catMaybes rest
catMaybes (Just x :: rest) = x :: catMaybes rest

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
module Data.Tainted

import Classes.Verified
import Control.Algebra.Lattice

%default total

data Tainted a = Clean a | Dirty a

instance (Show a) => Show (Tainted a) where
  show (Clean a) = "Clean " ++ (show a)
  show (Dirty a) = "Dirty " ++ (show a)

--- Semigroup Definitions
instance Semigroup a => Semigroup (Tainted a) where
  (Clean a) <+> (Clean b) = Clean (a <+> b)
  (Dirty a) <+> (Dirty b) = Dirty (a <+> b)
  (Clean a) <+> (Dirty b) = Dirty (a <+> b)
  (Dirty a) <+> (Clean b) = Dirty (a <+> b)

--- Verify that Tainted satisfies the Semigroup laws
instance VerifiedSemigroup a => VerifiedSemigroup (Tainted a) where
 semigroupOpIsAssociative (Clean x) (Clean y) (Clean z) = rewrite (semigroupOpIsAssociative x y z) in Refl
 semigroupOpIsAssociative (Clean x) (Clean y) (Dirty z) = rewrite (semigroupOpIsAssociative x y z) in Refl
 semigroupOpIsAssociative (Clean x) (Dirty y) (Clean z) = rewrite (semigroupOpIsAssociative x y z) in Refl
 semigroupOpIsAssociative (Clean x) (Dirty y) (Dirty z) = rewrite (semigroupOpIsAssociative x y z) in Refl
 semigroupOpIsAssociative (Dirty x) (Clean y) (Clean z) = rewrite (semigroupOpIsAssociative x y z) in Refl
 semigroupOpIsAssociative (Dirty x) (Clean y) (Dirty z) = rewrite (semigroupOpIsAssociative x y z) in Refl
 semigroupOpIsAssociative (Dirty x) (Dirty y) (Clean z) = rewrite (semigroupOpIsAssociative x y z) in Refl
 semigroupOpIsAssociative (Dirty x) (Dirty y) (Dirty z) = rewrite (semigroupOpIsAssociative x y z) in Refl

-- Monoid Definitions
instance Monoid a => Monoid (Tainted a) where
  neutral = Clean neutral

-- Verify that Tainted satisfied the Monoid laws
instance VerifiedMonoid a => VerifiedMonoid (Tainted a) where
  monoidNeutralIsNeutralL (Clean x) = rewrite (monoidNeutralIsNeutralL x) in Refl
  monoidNeutralIsNeutralL (Dirty x) = rewrite (monoidNeutralIsNeutralL x) in Refl
  monoidNeutralIsNeutralR (Clean x) = rewrite (monoidNeutralIsNeutralR x) in Refl
  monoidNeutralIsNeutralR (Dirty x) = rewrite (monoidNeutralIsNeutralR x) in Refl

--Meet-Semilattice Definitions
instance MeetSemilattice a => MeetSemilattice (Tainted a) where
  meet (Clean x) (Clean y) = Clean (meet x y)
  meet (Dirty x) (Dirty y) = Dirty (meet x y)
  meet (Clean x) (Dirty y) = Dirty (meet x y)
  meet (Dirty x) (Clean y) = Dirty (meet x y)

instance VerifiedMeetSemilattice a => VerifiedMeetSemilattice (Tainted a) where
  meetSemilatticeMeetIsAssociative (Clean x) (Clean y) (Clean z) =
    rewrite (meetSemilatticeMeetIsAssociative x y z) in Refl
  meetSemilatticeMeetIsAssociative (Clean x) (Clean y) (Dirty z) =
    rewrite (meetSemilatticeMeetIsAssociative x y z) in Refl
  meetSemilatticeMeetIsAssociative (Clean x) (Dirty y) (Clean z) =
    rewrite (meetSemilatticeMeetIsAssociative x y z) in Refl
  meetSemilatticeMeetIsAssociative (Clean x) (Dirty y) (Dirty z) =
    rewrite (meetSemilatticeMeetIsAssociative x y z) in Refl
  meetSemilatticeMeetIsAssociative (Dirty x) (Clean y) (Clean z) =
    rewrite (meetSemilatticeMeetIsAssociative x y z) in Refl
  meetSemilatticeMeetIsAssociative (Dirty x) (Clean y) (Dirty z) =
    rewrite (meetSemilatticeMeetIsAssociative x y z) in Refl
  meetSemilatticeMeetIsAssociative (Dirty x) (Dirty y) (Clean z) =
    rewrite (meetSemilatticeMeetIsAssociative x y z) in Refl
  meetSemilatticeMeetIsAssociative (Dirty x) (Dirty y) (Dirty z) =
    rewrite (meetSemilatticeMeetIsAssociative x y z) in Refl

  meetSemilatticeMeetIsCommutative (Clean x) (Clean y) =
    rewrite (meetSemilatticeMeetIsCommutative x y) in Refl
  meetSemilatticeMeetIsCommutative (Clean x) (Dirty y) =
    rewrite (meetSemilatticeMeetIsCommutative x y) in Refl
  meetSemilatticeMeetIsCommutative (Dirty x) (Clean y) =
    rewrite (meetSemilatticeMeetIsCommutative x y) in Refl
  meetSemilatticeMeetIsCommutative (Dirty x) (Dirty y) =
    rewrite (meetSemilatticeMeetIsCommutative x y) in Refl

  meetSemilatticeMeetIsIdempotent (Clean x) = rewrite (meetSemilatticeMeetIsIdempotent x) in Refl
  meetSemilatticeMeetIsIdempotent (Dirty x) = rewrite (meetSemilatticeMeetIsIdempotent x) in Refl

-- BoundedMeetSemilattice Definitions
instance BoundedMeetSemilattice a => BoundedMeetSemilattice (Tainted a) where
  top = (Clean top)

--instance (VerifiedBoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice (Tainted a) where
--  boundedMeetSemilatticeTopIsTop (Clean x) = rewrite believe_me in Refl --(boundedMeetSemilatticeTopIsTop x) in Refl
--  boundedMeetSemilatticeTopIsTop (Dirty x) = rewrite believe_me in Refl(boundedMeetSemilatticeTopIsTop x) in Refl

-- JoinSemilattice Definitions
instance JoinSemilattice a => JoinSemilattice (Tainted a) where
  join (Clean x) (Clean y) = Clean (join x y)
  join (Clean x) (Dirty y) = Clean (join x y)
  join (Dirty x) (Clean y) = Clean (join x y)
  join (Dirty x) (Dirty y) = Dirty (join x y)

-- Verify that Tainted satisfies the JoinSemilattice laws
instance VerifiedJoinSemilattice a => VerifiedJoinSemilattice (Tainted a) where
  joinSemilatticeJoinIsAssociative (Clean x) (Clean y) (Clean z) =
    rewrite (joinSemilatticeJoinIsAssociative x y z) in Refl
  joinSemilatticeJoinIsAssociative (Clean x) (Clean y) (Dirty z) =
    rewrite (joinSemilatticeJoinIsAssociative x y z) in Refl
  joinSemilatticeJoinIsAssociative (Clean x) (Dirty y) (Clean z) =
    rewrite (joinSemilatticeJoinIsAssociative x y z) in Refl
  joinSemilatticeJoinIsAssociative (Clean x) (Dirty y) (Dirty z) =
    rewrite (joinSemilatticeJoinIsAssociative x y z) in Refl
  joinSemilatticeJoinIsAssociative (Dirty x) (Clean y) (Clean z) =
    rewrite (joinSemilatticeJoinIsAssociative x y z) in Refl
  joinSemilatticeJoinIsAssociative (Dirty x) (Clean y) (Dirty z) =
    rewrite (joinSemilatticeJoinIsAssociative x y z) in Refl
  joinSemilatticeJoinIsAssociative (Dirty x) (Dirty y) (Clean z) =
    rewrite (joinSemilatticeJoinIsAssociative x y z) in Refl
  joinSemilatticeJoinIsAssociative (Dirty x) (Dirty y) (Dirty z) =
    rewrite (joinSemilatticeJoinIsAssociative x y z) in Refl

  joinSemilatticeJoinIsCommutative (Clean x) (Clean y) =
    rewrite (joinSemilatticeJoinIsCommutative x y) in Refl
  joinSemilatticeJoinIsCommutative (Clean x) (Dirty y) =
    rewrite (joinSemilatticeJoinIsCommutative x y) in Refl
  joinSemilatticeJoinIsCommutative (Dirty x) (Clean y) =
    rewrite (joinSemilatticeJoinIsCommutative x y) in Refl
  joinSemilatticeJoinIsCommutative (Dirty x) (Dirty y) =
    rewrite (joinSemilatticeJoinIsCommutative x y) in Refl

  joinSemilatticeJoinIsIdempotent (Clean x) = rewrite (joinSemilatticeJoinIsIdempotent x) in Refl
  joinSemilatticeJoinIsIdempotent (Dirty x) = rewrite (joinSemilatticeJoinIsIdempotent x) in Refl

-- BoundedJoinSemilattice Definitions
--instance BoundedJoinSemilattice a => BoundedJoinSemilattice (Tainted a) where
--  bottom = (Dirty bottom)

-- Verify that Tainted satisfies the BoundedJoinSemilattice laws
--instance VerifiedBoundedJoinSemilattice a => VerifiedBoundedJoinSemilattice (Tainted a) where
--  boundedJoinSemilatticeBottomIsBottom (Clean x) =
--    rewrite (boundedJoinSemilatticeBottomIsBottom x) in Refl
--  boundedJoinSemilatticeBottomIsBottom (Dirty x) =
--    rewrite (boundedJoinSemilatticeBottomIsBottom x) in Refl

-- Lattice Definitions, no extra operations over BoundedJoinSemilattice + BoundedMeetSemilattice
--instance Lattice a => Lattice (Tainted a)

-- Verify that Tainted satisfies the Lattice laws, need to show Join and Meet absorb one
-- another
{-
instance VerifiedLattice a => VerifiedLattice (Tainted a) where
  latticeMeetAbsorbsJoin (Clean x) (Clean y) = rewrite (latticeMeetAbsorbsJoin x y) in Refl
  latticeMeetAbsorbsJoin (Clean x) (Dirty y) = rewrite (latticeMeetAbsorbsJoin x y) in Refl
  latticeMeetAbsorbsJoin (Dirty x) (Clean y) = rewrite (latticeMeetAbsorbsJoin x y) in Refl
  latticeMeetAbsorbsJoin (Dirty x) (Dirty y) = rewrite (latticeMeetAbsorbsJoin x y) in Refl

  latticeJoinAbsorbsMeet (Clean x) (Clean y) = rewrite (latticeJoinAbsorbsMeet x y) in Refl
  latticeJoinAbsorbsMeet (Clean x) (Dirty y) = rewrite (latticeJoinAbsorbsMeet x y) in Refl
  latticeJoinAbsorbsMeet (Dirty x) (Clean y) = rewrite (latticeJoinAbsorbsMeet x y) in Refl
  latticeJoinAbsorbsMeet (Dirty x) (Dirty y) = rewrite (latticeJoinAbsorbsMeet x y) in Refl

-- Since Tainted has been verified to be an instance of BoundedJoinSemilattice +
-- BoundedMeetSemilattice + Lattice it follows that Tainted is also an instance of BoundedLattice
instance BoundedLattice a => BoundedLattice (Tainted a)
--instance VerifiedBoundedLattice a => VerifiedBoundedLattice (Tainted a)
-}

--- Functor Definitions ---
instance Functor Tainted where
  map f (Dirty a) = Dirty (f a)
  map f (Clean a) = Clean (f a)

-- | Verify that Tainted satisfies the Functor laws
instance VerifiedFunctor Tainted where
  functorIdentity (Clean _) = Refl
  functorIdentity (Dirty _) = Refl

  functorComposition (Clean _) g1 g2 = Refl
  functorComposition (Dirty _) g1 g2 = Refl

--- Applicative Definitions ---

instance Applicative Tainted where
  pure = Clean
  (Clean f) <*> (Clean c) = Clean (f c)
  (Clean f) <*> (Dirty d) = Dirty (f d)
  (Dirty f) <*> (Clean c) = Dirty (f c)
  (Dirty f) <*> (Dirty d) = Dirty (f d)

-- | Verify that Tainted satisfies the Applicative laws
instance VerifiedApplicative Tainted where
   applicativeMap (Clean _) _ = Refl
   applicativeMap (Dirty _) _ = Refl

   applicativeIdentity (Clean _) = Refl
   applicativeIdentity (Dirty _) = Refl

   applicativeComposition (Clean x) (Clean g1) (Clean g2) = Refl
   applicativeComposition (Clean x) (Clean g1) (Dirty g2) = Refl
   applicativeComposition (Clean x) (Dirty g1) (Dirty g2) = Refl
   applicativeComposition (Clean x) (Dirty g1) (Clean g2) = Refl
   applicativeComposition (Dirty x) (Dirty g1) (Dirty g2) = Refl
   applicativeComposition (Dirty x) (Dirty g1) (Clean g2) = Refl
   applicativeComposition (Dirty x) (Clean g1) (Dirty g2) = Refl
   applicativeComposition (Dirty x) (Clean g1) (Clean g2) = Refl

   applicativeHomomorphism x g = Refl

   applicativeInterchange x (Clean _) = Refl
   applicativeInterchange x (Dirty _) = Refl

--- Monad Definitions ---

instance Monad Tainted where
  (Dirty x) >>= f = case f x of
                  (Clean y) => Dirty y
                  (Dirty y) => Dirty y
  (Clean x) >>= f = f x

-- | Verify that Tainted satisfies the Monad laws
instance VerifiedMonad Tainted where
  monadApplicative (Dirty _) (Dirty _) = Refl
  monadApplicative (Dirty _) (Clean _) = Refl
  monadApplicative (Clean _) (Dirty _) = Refl
  monadApplicative (Clean _) (Clean _) = Refl

  monadLeftIdentity _ _  = Refl

  monadRightIdentity (Dirty _) = Refl
  monadRightIdentity (Clean _) = Refl

  monadAssociativity (Clean _) f g = Refl

  monadAssociativity (Dirty x) f g with (f x)
    monadAssociativity (Dirty x) f g | Clean y with (g y)
      monadAssociativity (Dirty x) f g | Clean y | Clean z = Refl
      monadAssociativity (Dirty x) f g | Clean y | Dirty z = Refl
    monadAssociativity (Dirty x) f g | Dirty y with (g y)
      monadAssociativity (Dirty x) f g | Dirty y | Clean z = Refl
      monadAssociativity (Dirty x) f g | Dirty y | Dirty z = Refl

--- Tainted Functions ---

-- | Returns 'True' iff its argument is of the form 'Clean _.
isClean : Tainted a -> Bool
isClean (Clean _) = True
isClean _ = False

-- | Returns 'True' iff its argument is of the form Dirty _.
isDirty : Tainted a -> Bool
isDirty = not . isClean

-- | Extract the value contained in a 'Tainted' type
extractTaint : Tainted a -> a
extractTaint (Clean a) = a
extractTaint (Dirty a) = a

-- | Extracts from a list of 'Tainted' all the 'Clean' elements.
--   All the 'Clean' elements are extracted in order.
cleans : List (Tainted a) -> List a
cleans = map extractTaint . filter isClean

-- | Extracts from a list of 'Tainted' all the 'Dirty' elements.
--   All the 'Dirty' elements are extracted in order.
dirtys : List (Tainted a) -> List a
dirtys = map extractTaint . filter isDirty

-- | Partitions a list of 'Tainted' into two lists.
--   All the 'Dirty' elements are extracted, in order, to the first component of the output.
--   Similarly the 'Clean' elements are extracted to the second component of the output.
partitionTaints : List (Tainted a) -> (List a, List a)
partitionTaints ts = (c, d)
    where c = cleans  ts
          d = dirtys  ts

max_stars_repo_name: RossMeikleham/Idris-Tainted

max_issues_repo_name: RossMeikleham/Idris-Tainted

max_forks_repo_name: RossMeikleham/Idris-Tainted


text:
module Main

import Motivation.Exfer

main : IO ()
main = putStrLn "Hello"


text:
> module GenericSimpleProb.SimpleProb

> import List.Operations

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

> |||
> data SimpleProb : Type -> Type -> Type where
>   MkSimpleProb : {A, B : Type} ->
>                  Num B =>
>                  (aps : List (A, B)) ->
>                  sumMapSnd aps = 1 ->
>                  SimpleProb A B

> {-

> ---}


text:
module Circuits.NetList.Linear.Usage.TermType

import Decidable.Equality

import Data.Nat
import Data.List.Elem
import Data.List.Quantifiers

import Data.Vect
import Data.Vect.AtIndex
import Data.Vect.Quantifiers

import Data.String

import Toolkit.Data.Whole
import Toolkit.Data.DList
import Toolkit.Data.DList.Elem

import Toolkit.Data.Vect.Extra
import Toolkit.Data.DVect

import Circuits.Common

import Circuits.NetList.Types

import Circuits.NetList.Linear.Usage.DataType
import Circuits.NetList.Linear.Usage.DataType.Use.Full
import Circuits.NetList.Linear.Usage.DataType.Use.Partial

%default total

public export
data Usage : Ty -> Type where
  TyPort : (u : Usage                type)
             -> Usage (TyPort (flow, type))

  TyChan : (ein  : Usage         type)
        -> (eout : Usage         type)
                -> Usage (TyChan type)

  TyGate : Usage TyGate
  TyUnit : Usage TyUnit

namespace Free

  public export
  data IsFree : (type : Ty) -> (u : Usage type) -> Type
    where
      FreeP : (prf : IsFree type u)
                  -> IsFree (TyPort (flow,type)) (TyPort u)

      FreeCB : (pin  : IsFree type a)
            -> (pout : IsFree type b)
                    -> IsFree (TyChan type) (TyChan a b)

      FreeG : IsFree TyGate TyGate
      FreeU : IsFree TyUnit TyUnit

  export
  isFree : {type : Ty} -> (u : Usage type) -> Dec (IsFree type u)
  isFree (TyPort x) with (isFree x)
    isFree (TyPort x) | (Yes prf)
      = Yes (FreeP prf)
    isFree (TyPort x) | (No contra)
      = No (\(FreeP prf) => contra prf)

  isFree (TyChan x y) with (isFree x)
    isFree (TyChan x y) | (Yes prfX) with (isFree y)
      isFree (TyChan x y) | (Yes prfX) | (Yes prfY)
        = Yes (FreeCB prfX prfY)
      isFree (TyChan x y) | (Yes prfX) | (No contra)
        = No (\(FreeCB a b) => contra b)
    isFree (TyChan x y) | (No contra)
      = No (\(FreeCB a b) => contra a)

  isFree TyGate
    = Yes FreeG

  isFree TyUnit
    = Yes FreeU

namespace Used

  public export
  data IsUsed : (type : Ty) -> (u : Usage type) -> Type where
    UsedP : IsUsed type u -> IsUsed (TyPort (flow,type)) (TyPort u)

    UsedC : (uin : IsUsed ty a)
         -> (uou : IsUsed ty b )
                -> IsUsed (TyChan ty) (TyChan a b)

  Uninhabited (IsUsed TyGate u) where
    uninhabited (UsedP x) impossible

  Uninhabited (IsUsed TyUnit u) where
    uninhabited (UsedP x) impossible

  export
  isUsed : {type : Ty} -> (u : Usage type) -> Dec (IsUsed type u)
  isUsed (TyPort x) with (isUsed x)
    isUsed (TyPort x) | (Yes prf)
      = Yes (UsedP prf)
    isUsed (TyPort x) | (No contra)
      = No (\(UsedP prf) => contra prf)

  isUsed (TyChan x y) with (isUsed x)
    isUsed (TyChan x y) | (Yes prfX) with (isUsed y)
      isUsed (TyChan x y) | (Yes prfX) | (Yes prfY)
        = Yes (UsedC prfX prfY)
      isUsed (TyChan x y) | (Yes prfX) | (No contra)
        = No (\(UsedC a b) => contra b)
    isUsed (TyChan x y) | (No contra)
      = No (\(UsedC a b) => contra a)

  isUsed TyGate = No absurd
  isUsed TyUnit = No absurd

namespace Part

  public export
  data IsPart : (type : Ty) -> (u : Usage type) -> Type where
    PartP : IsPart type u
         -> IsPart (TyPort (flow,type)) (TyPort u)

    PartCI : (uin : IsPart ty a)
                 -> IsPart (TyChan ty) (TyChan a b)

    PartCO : (uin : IsPart ty b)
                 -> IsPart (TyChan ty) (TyChan a b)

  Uninhabited (IsPart TyGate u) where
    uninhabited (PartP x) impossible

  Uninhabited (IsPart TyUnit u) where
    uninhabited (PartP x) impossible

  portNotPart : (IsPart type u -> Void) -> IsPart (TyPort (flow, type)) (TyPort u) -> Void
  portNotPart f (PartP x) = f x

  chanNotPart : (IsPart type eout -> Void) -> (IsPart type ein -> Void) -> IsPart (TyChan type) (TyChan ein eout) -> Void
  chanNotPart f g (PartCI uin) = g uin
  chanNotPart f g (PartCO uin) = f uin

  export
  isPart : {type : Ty} -> (u : Usage type) -> Dec (IsPart type u)
  isPart (TyPort u) with (isPart u)
    isPart (TyPort u) | (Yes prf)
      = Yes (PartP prf)

    isPart (TyPort u) | (No contra)
      = No (portNotPart contra)

  isPart (TyChan ein eout) with (isPart ein)
    isPart (TyChan ein eout) | (Yes prf)
      = Yes (PartCI prf)

    isPart (TyChan ein eout) | (No cin) with (isPart eout)
      isPart (TyChan ein eout) | (No cin) | (Yes prf)
        = Yes (PartCO prf)

      isPart (TyChan ein eout) | (No cin) | (No cou)
        = No (chanNotPart cou cin)

  isPart TyGate = No absurd
  isPart TyUnit = No absurd

public export
data IsFreeAt : (idx : Fin n) -> (type : Ty) -> (u : Usage type) -> Type
  where
    FreeAt : (prf : IsFreeAt idx              (BVECT (W (S n) ItIsSucc) type)          us)
                 -> IsFreeAt idx (TyPort (flow,BVECT (W (S n) ItIsSucc) type)) (TyPort us)

Uninhabited (IsFreeAt idx TyGate u) where
  uninhabited (FreeAt prf) impossible

Uninhabited (IsFreeAt idx TyUnit u) where
  uninhabited (FreeAt prf) impossible

Uninhabited (IsFreeAt idx (TyChan type) u) where
  uninhabited (FreeAt prf) impossible

isNotFreeAt : (IsFreeAt idx type u -> Void) -> IsFreeAt idx (TyPort (flow, type)) (TyPort u) -> Void
isNotFreeAt f (FreeAt prf) = f prf

export
isFreeAt : {n    : Nat}
        -> {type : Ty}
        -> (idx  : Fin n)
        -> (u    : Usage type)
                -> Dec (IsFreeAt idx type u)

isFreeAt idx (TyPort u) with (isFreeAt idx u)
  isFreeAt idx (TyPort (Array us)) | (Yes (FreeAt prf))
    = Yes (FreeAt (FreeAt prf))

  isFreeAt idx (TyPort u) | (No contra)
    = No (isNotFreeAt contra)

isFreeAt idx (TyChan ein eout) = No absurd
isFreeAt idx TyGate = No absurd
isFreeAt idx TyUnit = No absurd

public export
data IsUsedAt : (idx : Fin n) -> (type : Ty) -> (u : Usage type) -> Type
  where
    UsedAt : (prf : IsUsedAt idx              (BVECT (W (S n) ItIsSucc) type)          us)
                 -> IsUsedAt idx (TyPort (flow,BVECT (W (S n) ItIsSucc) type)) (TyPort us)

Uninhabited (IsUsedAt idx TyGate u) where
  uninhabited (UsedAt prf) impossible

Uninhabited (IsUsedAt idx TyUnit u) where
  uninhabited (UsedAt prf) impossible

Uninhabited (IsUsedAt idx (TyChan type) u) where
  uninhabited (UsedAt prf) impossible

isNotUsedAt : (IsUsedAt idx type u -> Void) -> IsUsedAt idx (TyPort (flow, type)) (TyPort u) -> Void
isNotUsedAt f (UsedAt prf) = f prf

export
isUsedAt : {n    : Nat}
        -> {type : Ty}
        -> (idx  : Fin n)
        -> (u    : Usage type)
                -> Dec (IsUsedAt idx type u)

isUsedAt idx (TyPort u) with (isUsedAt idx u)
  isUsedAt idx (TyPort (Array us)) | (Yes (UsedAt prf))
    = Yes (UsedAt (UsedAt prf))

  isUsedAt idx (TyPort u) | (No contra)
    = No (isNotUsedAt contra)

isUsedAt idx (TyChan ein eout) = No absurd
isUsedAt idx TyGate = No absurd
isUsedAt idx TyUnit = No absurd

-- [ EOF ]


text:
module Data.Contravariant

%default total

infixl 4 >$, >$<, >&<, $<

||| Contravariant functors
public export
interface Contravariant (0 f : Type -> Type) where
  contramap : (a -> b) -> f b -> f a

  (>$) : b -> f b -> f a
  v >$ fb = contramap (const v) fb

||| If `f` is both `Functor` and `Contravariant` then by the time you factor in the
||| laws of each of those classes, it can't actually use its argument in any
||| meaningful capacity.
public export %inline
phantom : Contravariant f => Functor f => f a -> f b
phantom fa = () >$ (fa $> ())

||| This is an infix alias for `contramap`.
public export %inline
(>$<) : Contravariant f => (a -> b) -> f b -> f a
(>$<) = contramap

||| This is an infix version of `contramap` with the arguments flipped.
public export %inline
(>&<) : Contravariant f => f b -> (a -> b) -> f a
(>&<) = flip contramap

||| This is `>$` with its arguments flipped.
public export %inline
($<) : Contravariant f => f b -> b -> f a
($<) = flip (>$)

||| Composition of `Contravariant` is a `Functor`.
public export
[Compose] (Contravariant f, Contravariant g) => Functor (f . g) where
  map = contramap . contramap

||| Composition of a `Functor` and a `Contravariant` is a `Contravariant`.
public export
[ComposeFC] (Functor f, Contravariant g) => Contravariant (f . g) where
  contramap = map . contramap

||| Composition of a `Contravariant` and a `Functor` is a `Contravariant`.
public export
[ComposeCF] (Contravariant f, Functor g) => Contravariant (f . g) where
  contramap = contramap . map


text:
module Minecraft.Base.PreClassic.GrassBlock.Block.Export

import public Minecraft.Core.Entity
import public Minecraft.Base.PreClassic.Dirt.ItemEntity
import public Minecraft.Base.PreClassic.GrassBlock.Block
import public Minecraft.Base.PreClassic.GrassBlock.Item

%default total

public export
Eq GrassBlock.Block where
  x == y = True

public export
Serialize GrassBlock.Block where
  identifier = "GrassBlock.Block"
  serialize x = JObject [
    ("waterLogged", JBoolean x.base.waterLogged)
  ]

public export
Deserialize GrassBlock.Block where
  deserialize (JObject [
    ("waterLogged", JBoolean waterLogged)
  ]) = Just $ GrassBlock.MkBlock {base = (GenericData.MkBlock {waterLogged = waterLogged})}
  deserialize _ = Nothing

[grassBlockBlock']
Block GrassBlock.Block where
  id = Item.id {self = GrassBlock.Item}

[breakGrassBlock']
Break GrassBlock.Block where
  breakBlk self = [new Dirt.ItemEntity Dirt.MkItemEntity]

[grassBlockVtbl']
Vtbl GrassBlock.Block where
  vtable (Block    GrassBlock.Block) = Just grassBlockBlock
  vtable (Break    GrassBlock.Block) = Just breakGrassBlock
  vtable (Tangible GrassBlock.Block) = Just %search
  vtable _ = Nothing

grassBlockBlock = grassBlockBlock'
breakGrassBlock = breakGrassBlock'
grassBlockVtbl  = grassBlockVtbl'

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module Circuits.NetList

import public Circuits.NetList.Core
import public Circuits.NetList.Types
import public Circuits.NetList.Terms
import public Circuits.NetList.AST
import public Circuits.NetList.Lexer
import public Circuits.NetList.Parser
import public Circuits.NetList.Check
import public Circuits.NetList.Interp

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
module TestParser

import India.Interpreter.AST
import India.Language.Core

import India
import India.Wrapper
import India.Union
import Text.Lexer
import Text.Parser

myTest : IO ()
myTest = do
  Right res <- parseFileWith myParser "Content.in"
    | Left err => putStrLn "Test failure: \{err}"
  putStrLn res.content
  where
    myParser : String -> Either String (AST Paragraph)
    myParser = simpleParser

max_stars_repo_name: berewt/india

max_issues_repo_name: berewt/india

max_forks_repo_name: berewt/india


text:
module Syntax.Term
import public Loc
import Data.String
import Data.List1

formatText : String -> Nat -> String
formatText text ident =
  let identation = replicate ident ' ' in
  unlines $ map (++ identation) $ (lines text)

mutual

  public export
  record Program where
    constructor MkProgram
    fileName  : String
    dataDefs  : List DataDef
    defs      : List Def
    recordDef : List RecordDef

  public export
  record Name where
    constructor MkName
    range: Range
    name: String

  public export
  record DataDef where
    constructor DefData
    name : Name
    type : Maybe Types
    fields : List (Name, List Types)

  public export
  record Def where
    constructor Define
    name : Name
    type : Maybe Types
    value : Expr

  public export
  record RecordDef where
    constructor DefRecord
    name : Name
    type : Maybe Types
    fields : List (Name, Types)

  public export
  data Path
    = PDot      Range Name Path
    | PName     Range String

  public export
  data Expr
    = ELit      Range Literal
    | ELambda   Range Name Expr
    | ECall     Range Expr Expr
    | EDo       Range (List Expr)
    | ECase     Range Expr (List (Pat, Expr))
    | ELet      Range Name Expr Expr
    | EId       Path

  public export
  data Pat
    = PaId       Name
    | PaLit      Range Literal
    | PaData     Range Path (List Pat)
    | PaList     Range (List Pat)
    | PaHdTl     Range Pat Pat

  public export
  data Literal
    = LStr      Range String
    | LInt      Range Int

  public export
  data Types
    = TSimple   Range String
    | TArrow    Range Types Types
    | TPoly     Range Path Types
    | TVar      Range String

  Show Name where
    show (MkName range n) = n

  public export
  Show Path where
    show (PDot r name path) = (show name) ++ "." ++ (show path)
    show (PName r str) = str

  Show Literal where
    show (LStr r str) = "\"" ++ str ++ "\""
    show (LInt r int) = show int

  Show Expr where
    show (ELit r lit) = show lit
    show (ELambda r arg expr) = "(λ [" ++ (show arg) ++ "] " ++ (show expr) ++ ")"
    show (EDo r exprs) = "(Do\n" ++ formatText (unlines $ map show exprs) 2 ++ ")"
    show (ECase r cond exprs) = "(case " ++ (show cond) ++ "\n" ++ formatText (unlines $ map show exprs) 2 ++ ")"
    show (ECall r a b) = concat ["(", show a, " ", show b,")"]
    show (EId n) = show n
    show (ELet r name val expr) = concat ["(let ", show name, "=", show val, "\n  ", show expr]

  Show Pat where
    show (PaId n) = show n
    show (PaLit r l) = show l
    show (PaData r path pats) = "(" ++ show path ++ ", " ++ (concatMap ((\a => a ++ ",") . show) pats)  ++ ")"
    show (PaList r list) = "[" ++ (concatMap ((\a => a ++ ", ") . show) list) ++ "]"
    show (PaHdTl r a b) = concat ["(", show a, "::", show b, ")"]

  Show Types where
    show (TSimple r s) = s
    show (TArrow r a b) = "(" ++ show a ++ " -> " ++ show b ++ ")"
    show (TPoly r path n) = "(" ++ (show path) ++ " " ++ show n ++ ")"
    show (TVar a s) = s

  Show DataDef where
    show (DefData name type fields) =
      "Data: \n  " ++ (formatText (concat [
        "Name: \n    ", show name, "\n",
        "Type: \n    ", show type, "\n",
        "Fields: \n", (formatText (
          unlines $ map (\(name, type) => concat ["(", show name,":",show type, ")"]) fields
        ) 2)
      ]
      ) 2)

  Show RecordDef where
    show (DefRecord name type fields) =
      "Record: \n" ++ (formatText (concat [
        "Name:\n    ", show name, "\n",
        "Type: \n    ", show type, "\n",
        "Fields: \n", (formatText (
          unlines $ map (\(name, type) => concat ["(", show name," : ",show type, ")"]) fields
        ) 2)
      ]
      ) 2)

  Show Def where
    show (Define name type expr) =
      "Def: \n" ++ (formatText (concat [
        "Name: \n    ", show name, "\n",
        "Type: \n    ", show type, "\n",
        "Value: \n", (formatText (show expr) 2)]
      ) 2)

  public export
  Show Program where
    show (MkProgram name datad defs recs) =
      "Program: \n" ++ (formatText (concat [
        "Datas: \n", (formatText (show datad) 2), "\n",
        "Defs: \n", (formatText (show defs) 2), "\n",
        "Records: \n", (formatText (show recs) 2)]
      ) 2)

max_stars_repo_name: felipegchi/Yurei

max_issues_repo_name: felipegchi/Yurei

max_forks_repo_name: felipegchi/Yurei


text:
module Path

%default total
%access public export

validNameChar : Char -> Maybe Char
validNameChar c =
  if c < ' ' || c == '\DEL' || c == '/' || c == '\\' || c == ':'
  then Nothing
  else Just c

||| There are characters that we want to block from a file path, whether because
||| they are not supported in the underlying filesystem, or just because it is
||| ridiculous or inconvenient to have them in file paths, even if they were in
||| the underlying filesystem. Now we could do this by constructing elaborate
||| proofs that our characters were only in a certain subset of what they could
||| be; but this sounds like an incredibly heavyweight, unweildy thing to do
||| when we are dealing at the level of an individual character within a much
||| larger string-like object! Instead, then, we exploit the idea of
||| isomorphisms between normal forms: that is, we want to construct our
||| parser-printer such that there is a one-to-one match between the normal form
||| of a path in the syntax, and its normal form in our conceptual model. The
||| ability to speak of normal forms is what frees us to not have to construct
||| such proofs: instead, we simply allow the conceptual model to have multiple
||| characters normalize to only one character that we want in our target subset
||| of path characters. This gives us a way to sane, consistent way to handle
||| illegal characters, without having to actually use the type system to blot
||| them out of existence.
|||
||| An advantage of this approach is that it is portable to languages that do
||| not have dependent types, without the need to introduce opaque types (types
||| with private constructors). A potential disadvantage in the abstract is the
||| imposition of the need for normalization; however, this imposition is not
||| such a great disadvantage in this case, since due to `.` and `..` the
||| standard syntax for filepaths is already subject to this complexity.
|||
||| We choose to normalize a character in a path name by mapping illegal
||| characters and `.` to `_`. `.` is not considered an illegal character since
||| it is allowed in the syntax; but in the conceptual model it is not encoded
||| as a character directly, and therefore for our purposes here must be
||| remapped.
normalizeNameChar : Char -> Char
normalizeNameChar '.' = '_'
normalizeNameChar c = fromMaybe '_' $ validNameChar c

normalize_name_char_never_returns_dot : Not (normalizeNameChar c = '.')
normalize_name_char_never_returns_dot Refl impossible

||| Valid names for files or directories. This does not include . or .., and we
||| encode the dots separately from the other characters in order to ensure that
||| does not happen: actually, we block any number of dots, unless there is a
||| non-dot character to go along with it, since these filepaths are of
||| questionable use and can cause odd behaviors on some platforms.
|||
||| Specifically, we encode the dots as a list of offsets where there are dots,
||| and we encode the other characters as a head and tail (to ensure
||| nonemptiness) of characters, subject to normalization at printing.
record PathName where
  constructor PName
  dots : List Nat
  hdcr : Char
  chrs : List Char

||| Convert the path name to the syntax in a list of characters.
chars : PathName -> List Char
chars (PName dots c cs) = chars' dots $ c :: cs where
  chars' : List Nat -> List Char -> List Char
  chars' [] ys = map normalizeNameChar ys
  chars' (Z :: xs) ys = chars' xs ys
  chars' xs@(_ :: _) [] = map (\_ => '.') xs
  chars' ((S x) :: xs) (y :: ys) = y :: chars' (x :: xs) ys

path_name_doesnt_include_dot_or_dotdot_etc : Not (chars n = replicate x '.')
path_name_doesnt_include_dot_or_dotdot_etc Refl impossible

Show PathName where
  show = pack . chars

data PathSeg = Name PathName | Parent

isName : PathSeg -> Bool
isName (Name _) = True
isName _ = False

Show PathSeg where
  show (Name n) = show n
  show Parent = ".."

||| A path on the local filesystem, possibly rooted
record LPath (rooted : Bool) where
  constructor LocalPath
  ||| The segments of the path, in reverse order form how they are displayed in
  ||| the syntax
  segs : List PathSeg

HasName : LPath r -> Type
HasName (LocalPath segs) =
  length (filter isName segs) = 0

record NetworkPath where
  constructor NetworkP
  ||| The remote host's name
  host : PathSeg
  ||| The path on the remote host
  remotePath : List PathSeg

data Path
  = Local (LPath rooted)
  | Remote NetworkPath

||| Path segment separator: `\` or `/`
data PathSegSep = Backslash | Slash

pathSegSep : PathSegSep -> Char
pathSegSep Backslash = '\\'
pathSegSep Slash = '/'

max_stars_repo_name: Kazark/filepath

max_issues_repo_name: Kazark/filepath

max_forks_repo_name: Kazark/filepath


text:
y : Integer
y = 42 -- the number 42 is popular

k : Integer
k = -7

{-
I called the first number y just because I
did so in the second video
-}

willnotcomebackto : Integer

n : Integer
n = 150

aholefromepisode4 : Integer
aholefromepisode4 = ?will_come_back_to_later

n' : Integer
n' = 53

n_ : Integer
n_ = 54

_n : Integer
_n = 55

u : Integer
u = 2+3

v : Integer
v = n + 10

a : Integer
a = 10000

b
:
Integer
b
=
 33

msg : String
msg = "Hello!"

youtube : String
youtube = "http://youtube.com"

faulty : Integer

youtube_prefix : String
youtube_prefix = youtube ++ "/watch?v="

episode2 : String
episode2 = youtube_prefix ++ "OGmwGSpwT1U"

editor : String
editor = "Atom"

blank : String
blank = " "

greeting : String
greeting = "Servus" ++ blank ++ editor

cry : String
cry = "Check\nthis\nout!"

f : Integer -> Integer
f x = x + 2000

z : Integer
z = f 10

max_stars_repo_name: Nikolaj-K/idris

max_issues_repo_name: Nikolaj-K/idris

max_forks_repo_name: Nikolaj-K/idris


text:
module CoproductProps

import Basic
import Unit
import Void
import Coproduct

import Path
import General
import Dec

public export
UnitNotVoid : Unit /= Void
UnitNotVoid p = IdFun p ()

public export
-- p : 1 == 0
OneNotTwo : Inr () /= Inl ()
OneNotTwo p = UnitNotVoid q
 where
  f : Two -> Type
  f (Inl ()) = Void
  f (Inr ()) = Unit

  q : Unit == Void
  q = ap f p

public export
TwoDecEq : DecEq Two
-- 0 == 0 + Neg (0 == 0)
TwoDecEq (Inl ()) (Inl ()) = Inl (Refl (Inl ()))
-- (0 == 1) + Neg (0 == 1)
TwoDecEq (Inl ()) (Inr ()) = Inr (negSym OneNotTwo)
-- (1 == 0) + Neg (1 == 0)
TwoDecEq (Inr ()) (Inl ()) = Inr OneNotTwo
-- 1 == 1 + Neg (1 == 1)
TwoDecEq (Inr ()) (Inr ()) = Inl (Refl (Inr ()))

public export
NotZeroIsOne : (n : Two) -> n /= Inl () -> n == Inr ()
-- 0 /= 0
NotZeroIsOne (Inl ()) f = VoidInduction
  (const $ Inl () == Inr ()) (f (Refl _))
-- 1 /= 0 -> 1 == 1
NotZeroIsOne (Inr ()) f = Refl _

public export
SumDisjointImages : {x : a} -> {y : b} -> Inl x /= Inr y
SumDisjointImages p = UnitNotVoid q
-- p : 0 == 1
 where
  f : a + b -> Type
  f (Inl x) = Unit
  f (Inr y) = Void

  q : Unit == Void
  q = ap f p

public export
LeftIfNotRight : a + b -> Neg b -> a
LeftIfNotRight (Inl p) _ = p
LeftIfNotRight (Inr p) f = VoidRecursion a (f p)