text:
||| Primitive Javascript arrays. This offers an alternative
||| to the functionality provided by `Data.IOArray.Prims` from base.
|||
||| In addition to mutable arrays, we also provide linear arrays
||| for imperatively filling arrays in a pure envirionment,
||| as well as immutable arrays, the latter being guaranteed to always
||| return a value if an index is within bounds.
|||
||| We use `Bits32` for indexing, as this is the type reflecting
||| most exactly the kinds of indices use to access array elements.
||| However, right now, `Bits32` is represented by `BigInt` at the Javascript
||| backend. This might negatively affect performance, as we always have
||| to convert to `Number` first (that's `Double` in Idris2).
||| Hopefully, the backend representation will change in the future, and
||| this will be no longer an issue.
|||
||| In addition, `Bits32` does not offer a lot of functionality when
||| it comes to available proofs for it being in bounds. This
||| module provides a minimal amount of utilities for this, but again,
||| these might hopefully go elswhere, where the whole topic is treated
||| more thoroughly.
module JS.Array

import Control.Monad.Either
import Decidable.Equality
import Data.DPair
import Data.List

import JS.Any
import JS.Boolean
import JS.Marshall
import JS.Undefined
import JS.Util

--------------------------------------------------------------------------------
--          Utilities
--------------------------------------------------------------------------------

||| Type for indexing into an array of known size.
public export
Ix : Bits32 -> Type
Ix n = Subset Bits32 $ \ix => ix < n = True

||| Calculates the length of a list as an array index.
public export
len32 : List a -> Bits32
len32 = fromInteger . natToInteger . length

||| Zips a list of elements with the corresponding
||| array indices.
public export
zipWithIndex : (as : List a) -> List (Ix $ len32 as, a)
zipWithIndex as = run 0 as
  -- being pragmatic here and going via `believe_me`
  where run : Bits32 -> List a -> List (Ix $ len32 as, a)
        run _ []        = []
        run n (x :: xs) =  (Element n $ believe_me (Refl {x}), x)
                        :: run (n+1) xs

||| Tries to convert a number into an index for
||| an array of the given size.
public export
toIx : (size : Bits32) -> Bits32 -> Maybe (Ix size)
toIx size x = case decEq (x < size) True of
                   Yes prf => Just $ Element x prf
                   No  _   => Nothing

--------------------------------------------------------------------------------
--          FFI
--------------------------------------------------------------------------------

export
data Array : Type -> Type where [external]

-- Note: in the backend, type parameters are passed
-- as additional erased arguments of type `undefined`
-- to the lambdas. The lambdas therefore need to take
-- additional arguments, based on the number of type parameters.

-- determines the size of a (potentially) mutable Array-like object.
%foreign "javascript:lambda:(u,x) => x.length"
prim__sizeIO : forall arr . arr -> PrimIO Bits32

-- reads a value at the given index from a (potentially) mutable Array-like object.
%foreign "javascript:lambda:(u,v,arr,n) => arr[n]"
prim__readIO : forall a,arr . arr -> Bits32 -> PrimIO (UndefOr a)

-- determines the size of an immutable Array-like object.
%foreign "javascript:lambda:(u,x) => x.length"
prim__size : forall arr . arr -> Bits32

-- reads a value at the given index from an immutable Array-like object.
%foreign "javascript:lambda:(u,v,arr,n) => arr[n]"
prim__read : forall a,arr . arr -> Bits32 -> a

-- writes a value to a mutable array
%foreign "javascript:lambda:(u,arr,n,v) => { arr[n] = v }"
prim__writeIO : forall a . Array a -> Bits32 -> a -> PrimIO ()

-- creates a new mutable array of the given size
%foreign "javascript:lambda:(u,n) => { return new Array(n) }"
prim__newArrayIO : forall a . Bits32 -> PrimIO (Array a)

-- determines, whether the given pointer is an array.
%foreign "javascript:lambda:x => Array.isArray(x)"
prim__isArray : AnyPtr -> Boolean

-- clones an Array-like object, thus creating a new array.
%foreign "javascript:lambda:(u,x) => Array.from(x)"
prim__fromArrayLikeIO : forall arr . arr -> PrimIO (Array a)

--------------------------------------------------------------------------------
--          ArrayLike
--------------------------------------------------------------------------------

||| Witness, that a given value represents an Array-like object.
||| Array-like objects must provide the following functionality in
||| the Javascript backend:
|||
|||  * a `length` property, returning the value's length as an unsigned 32bit
|||    integer
|||  * the ability to access values of the given `elem` type`
|||    at a given index by means of the following syntax: `arr[12]`.
|||
||| Javascript Arrays are, of course, Array-like, as are Strings.
||| Some other Array-likes include `NodeList` in the DOM.
|||
||| Note, that this is just a witnessing interface. All functionality
||| is already implemented through functions `sizeIO` and `readIO`.
||| It is possible to clone an `ArrayLike` to an actual Javascript
||| Array by invoking `Array.from(v)` at the backend. This functionality
||| is available through `arrayDataFrom` for mutable arrays and
||| `arrayFrom` for immutable arrays.
public export
interface ArrayLike (0 arr : Type) (0 el : Type) | arr where

export
sizeIO : (HasIO io, ArrayLike arr el) => arr -> io Bits32
sizeIO v = fromInteger . cast <$> primIO (prim__sizeIO v)

export
readIO : (HasIO io, ArrayLike arr e) => arr -> Bits32 -> io (Maybe e)
readIO v ix = undeforToMaybe <$> (primIO . prim__readIO v $ toFFI ix)

export
ArrayLike String Char where

export
ArrayLike (Array a) a where

||| Witness, that a given value represents an immutable
||| Array-like object. The same rules as for `ArrayLike`
||| hold, with the addition, that values of types implementing
||| this interface must be immutable.
||| It is then safe to provide pure versions of `readIO` and `sizeIO`.
public export
interface ArrayLike arr el => IArrayLike arr el | arr where

export
size : IArrayLike arr el => arr -> Bits32
size arr = fromInteger . cast $ prim__size arr

export
read : IArrayLike arr el
     => (elems : arr) -> (ix : Ix $ size elems) -> el
read elems (Element ix _) = prim__read elems $ toFFI ix

export
readMaybe : IArrayLike arr el
          => (elems : arr) -> Bits32 -> Maybe el
readMaybe elems = map (read elems) . toIx (size elems)

||| Returns true if the given immutable arrays contain
||| the same elements in the same order.
export
sameElements : (IArrayLike arr el, Eq el) => arr -> arr -> Bool
sameElements a1 a2 =
  case decEq (size a2) (size a1) of
       Yes prf => run prf 0
       No _    => False
  where run : (0 _ : size a2 = size a1) -> Bits32 -> Bool
        run refl ix =
          case decEq (ix < size a1) True of
               No  _   => True
               Yes prf =>
                 read a1 (Element ix prf) ==
                   read a2 (Element ix (rewrite refl in prf)) &&
                 run refl (ix+1)

export
foldlArray :  IArrayLike arr el
           => (acc -> el -> acc) -> acc -> arr -> acc
foldlArray f ini arr = run 0 ini
  where run : Bits32 -> acc -> acc
        run n res = case readMaybe arr n of
                         Just el => run (n+1) (f res el)
                         Nothing => res

export
foldrArray :  IArrayLike arr el
           => (el -> acc -> acc) -> acc -> arr -> acc
foldrArray f ini arr = run 0
  where run : Bits32 -> acc
        run n = case readMaybe arr n of
                     Just el => f el $ run (n+1)
                     Nothing => ini

export
arrayToList : IArrayLike arr el => arr -> List el
arrayToList = foldrArray (::) Nil

export
IArrayLike String Char where

--------------------------------------------------------------------------------
--          IO Arrays
--------------------------------------------------------------------------------

export
ToFFI (Array a) (Array a) where toFFI = id

export
FromFFI (Array a) (Array a) where fromFFI = Just

export %inline
isArray : anyVal -> Bool
isArray v = eqv true $ prim__isArray (toFFI $ MkAny v)

export
writeIO : HasIO io => Array a -> Bits32 -> a -> io ()
writeIO arr ix v = primIO $  prim__writeIO arr (toFFI ix) v

export
newArrayIO : HasIO io => Bits32 -> io (Array a)
newArrayIO n = primIO $  prim__newArrayIO (toFFI n)

export
arrayDataFrom : (HasIO io, ArrayLike arr e) => arr -> io (Array e)
arrayDataFrom arr = primIO $ prim__fromArrayLikeIO arr

--------------------------------------------------------------------------------
--          Arrays and Lists
--------------------------------------------------------------------------------

export
fromListIO : HasIO io => List a -> io (Array a)
fromListIO as = let len = the Bits32 (fromInteger . natToInteger $ length as)
                 in newArrayIO len >>= fill 0 as
  where fill : Bits32 -> List a -> Array a -> io (Array a)
        fill _ []        arr = pure arr
        fill n (x :: xs) arr = do writeIO arr n x
                                  fill (n+1) xs arr

export
fromFoldableIO : (HasIO io, Foldable t) => t a -> io (Array a)
fromFoldableIO = fromListIO . toList

export
ToFFI a b => ToFFI (List a) (IO $ Array b)
  where toFFI = fromListIO . map toFFI

--------------------------------------------------------------------------------
--          Linear Arrays
--------------------------------------------------------------------------------

%foreign "javascript:lambda:(u,arr,n,v) => { arr[n] = v; return arr }"
prim__write : forall a . Array a -> Bits32 -> a -> Array a

%foreign "javascript:lambda:(u,n,a) => { var res = new Array(n); return res.fill(a) }"
prim__newArray : forall a . Bits32 -> a -> Array a

%foreign "javascript:lambda:(u,n) => { return new Array(n) }"
prim__undefArray : forall a . Bits32 -> Array a

%foreign "javascript:lambda:u => { return = new Array(0) }"
prim__emptyArray : forall a . Array a

%foreign "javascript:lambda:(u,x,v) => Array.from(v)"
prim__fromArray : forall arr . arr -> Array a

||| A linear wrapper around a primitive array.
export
record LinArray (sze : Bits32) (a : Type) where
  constructor MkLinArray
  array : Array a

export
thaw : (1 _ : LinArray sze a) -> IO (Array a)
thaw (MkLinArray arr) = pure arr

-- This must not leak out, as we allocate a new array of
-- `undefined` values. It is used to create an array by
-- iteratively filling it up.
private
undefArray : (sze : Bits32) -> (1 _ : (1 _ : LinArray sze a) -> b) -> b
undefArray sze f = f (MkLinArray $ prim__undefArray (toFFI sze))

private
unsafeWrite : (1 _ : LinArray sze a) -> (n : Bits32) -> a -> LinArray sze a
unsafeWrite (MkLinArray arr) n v = MkLinArray $ prim__write arr (toFFI n) v

export
emptyArray : (1 _ : (1 _ : LinArray 0 a) -> b) -> b
emptyArray f = f (MkLinArray $ prim__emptyArray)

export
newArray :  (val : a)
         -> (sze : Bits32)
         -> (1 _ : (1 _ : LinArray sze a) -> b)
         -> b
newArray v sze f = f (MkLinArray $ prim__newArray (toFFI sze) v)

export
withArray :  IArrayLike arr el
          => (v : arr)
          -> (1 _ : (1 _ : LinArray (size v) el) -> a)
          -> a
withArray array f = f (MkLinArray $ prim__fromArray array)

export
write : (1 _ : LinArray sze a) -> (ix : Ix sze) -> a -> LinArray sze a
write arr (Element n _) = unsafeWrite arr n

export
lread :  (1 _ : LinArray sze a)
      -> (ix : Ix sze)
      -> Res a (const $ LinArray sze a)
lread (MkLinArray arr) (Element ix _) =
  prim__read arr (toFFI ix) # MkLinArray arr

export
lsize : (1 _ : LinArray sze a) -> Res Bits32 (\s => LinArray s a)
lsize (MkLinArray arr) = fromInteger (cast $ prim__size arr) # MkLinArray arr

export
iterate' :  (sze : Bits32)
         -> (Ix sze -> a)
         -> ((1 _ : LinArray sze a) -> b)
         -> b
iterate' sze f g = undefArray sze (run 0)
  where run : Bits32 -> (1 _ : LinArray sze a) -> b
        run n arr = case toIx sze n of
                         Nothing => g arr
                         Just ix => run (n+1) (write arr ix (f ix))

export
fromList' : (as : List a) -> ((1 _ : LinArray (len32 as) a) -> b) -> b
fromList' as f = undefArray (len32 as) (run $ zipWithIndex as)
  where run :  List (Ix $ len32 as, a) -> (1 _ : LinArray (len32 as) a) -> b
        run []            linA = f linA
        run ((ix,a) :: t) linA = run t (write linA ix a)

export
map' : IArrayLike arr a =>
       (vs : arr) -> ((1 _ : LinArray (size vs) b) -> c) -> (a -> b) -> c
map' vs fromArr f = iterate' (size vs) (\ix => f (read vs ix)) fromArr

export
totalSize : (IArrayLike arr1 arr2, IArrayLike arr2 el)
          => arr1 -> Bits32
totalSize = foldlArray (\n,vs => n + size vs) 0

||| Concatenates to nested layers of immutable
||| array-like objects.
export
join' :  (IArrayLike arr1 arr2, IArrayLike arr2 el)
      => (vss : arr1)
      -> ((1 _ : LinArray (totalSize {arr2} vss) el) -> a)
      -> a
join' vss f = undefArray (totalSize {arr2} vss) (outer 0 0)
   where inner :  (n : Bits32)
               -> (pos : Bits32)
               -> arr2
               -> (1 _ : LinArray (totalSize {arr2} vss) el)
               -> LinArray (totalSize {arr2} vss) el
         inner n pos as la =
           case readMaybe as n of
                Just v  => inner (n+1) pos as (unsafeWrite la (pos + n) v)
                Nothing => la

         outer :  (n : Bits32)
               -> (pos : Bits32)
               -> (1 _ : LinArray (totalSize {arr2} vss) el)
               -> a
         outer n pos la =
           case readMaybe vss n of
                Just v  => outer (n+1) (pos + size v) (inner 0 pos v la)
                Nothing => f la

--------------------------------------------------------------------------------
--          Immutable Arrays
--------------------------------------------------------------------------------

||| An immutable array from a resource that guarantees, that
||| this will not be modified any more.
|||
||| Typically, these are generated by freezing a `LinArray`
||| or by cloning an `ArrayLike` value.
export
record IArray (a : Type) where
  constructor MkIArray
  array : Array a

export
freeze : forall sze,a . (1 _ : LinArray sze a) -> IArray a
freeze (MkLinArray arr) = MkIArray arr

export
fromList : List a -> IArray a
fromList as = fromList' as freeze

export
singleton : a -> IArray a
singleton = fromList . pure

export
ArrayLike (IArray a) a where

export
IArrayLike (IArray a) a where

export
concat : IArray (IArray a) -> IArray a
concat as = join' {arr2 = IArray a} as freeze

export
Eq el => Eq (IArray el) where
  (==) = sameElements {el}

export
Show a => Show (IArray a) where
  showPrec p v = showCon p "fromList " (show $ arrayToList v)

export
Semigroup (IArray a) where
  a1 <+> a2 = concat $ fromList [a1,a2]

export
Monoid (IArray a) where
  neutral = fromList []

export
Functor IArray where
  map f as = map' as freeze f

export
Applicative IArray where
  pure = singleton
  fs <*> as = concat $ map (\f => map (apply f) as) fs

export
Monad IArray where
  join = concat

export
Foldable IArray where
  foldr    = foldrArray
  foldl    = foldlArray
  null arr = size arr == 0

-- No idea if this can be done more efficiently without
-- going via List. Any idea to do this via direct iteration
-- over the indices is highly welcome.
export
Traversable IArray where
  traverse f arr = fromList <$> traverse f (toList arr)

export
Alternative IArray where
  empty     = fromList []
  as <|> bs = if null as then bs else as

export
FromString (IArray Char) where
  fromString s = withArray s freeze


text:
record Book where
       constructor MkBook
       title : String
       author : String

record Album where
       constructor MkAlbum
       title : String
       tracks : List String

ext: idr


text:
module Circuits.NetList.Linear.Interp

import Decidable.Equality

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

import Toolkit.Decidable.Informative

import Toolkit.Data.Graph.EdgeBounded
import Toolkit.Data.Graph.EdgeBounded.HasExactDegree.All

import Toolkit.Data.Whole
import Toolkit.Data.List.DeBruijn

import Circuits.NetList.Types

import Circuits.NetList.Linear.Usage
import Circuits.NetList.Linear.Terms

%default total

public export
InterpTy : Ty -> Type
InterpTy TyUnit
  = Unit

InterpTy (TyPort x)
  = Vertex String

InterpTy (TyChan x)
  = Pair (Vertex String) (Vertex String)

InterpTy TyGate
  = Graph String

select : Project dir -> Vertex a -> Vertex a -> Vertex a
select WRITE y z = y
select READ y z = z

namespace Environments

  public export
  data Env : List Item -> Type where
    Empty  : Env Nil
    Extend : (term : InterpTy type)
          -> (env  : Env rest)
                  -> Env (I type usage :: rest)

  namespace Port

    export
    lookup : (env : Env this)
          -> (prf : IsFreePort (I (TyPort (flow,type)) u) this)
          -> (use : UsePort this prf that)
                 -> (Env that, InterpTy (TyPort (flow,type)))
    lookup (Extend term rest) (FreePortHere pf) (UsePortHere use)
      = (Extend term rest, term)

    lookup (Extend not_term env) (FreePortThere rest) (UsePortThere later) with (lookup env rest later)
      lookup (Extend not_term env) (FreePortThere rest) (UsePortThere later) | (new, term)
        = (Extend not_term new, term)

  namespace Project

    export
    lookup : (env : Env this)
          -> (prf : IsFreeChannel how (I (TyChan type) (TyChan ein eout)) this)
          -> (use : ProjectChannel how this prf that)
                 -> (Env that, InterpTy (TyChan type))
    lookup (Extend term env) (FreeChannelHere prf) (ProjectHere use)
      = (Extend term env, term)

    lookup (Extend not_term env) (FreeChannelThere rest) (ProjectThere later) with (lookup env rest later)
      lookup (Extend not_term env) (FreeChannelThere rest) (ProjectThere later) | (new, term)
        = (Extend not_term new, term)

  namespace Index

   export
   lookup : (env : Env this)
         -> (prf : CanIndexPort idx (I (TyPort (flow, BVECT (W (S n) ItIsSucc) type)) u) this)
         -> (use : IndexPort idx this prf that)
                -> (Env that, InterpTy (TyPort (flow, type)))
   lookup (Extend term env) (CanIndexHere prf) (IndexHere use)
     = (Extend term env, term)

   lookup (Extend not_term env) (CanIndexThere rest) (IndexThere later) with (lookup env rest later)
     lookup (Extend not_term env) (CanIndexThere rest) (IndexThere later) | (new, term)
       = (Extend not_term new, term)

namespace Result

  public export
  data Result : (context : List Item)
             -> (type    : Ty)
                        -> Type
   where
     R : (counter : Nat)
      -> (env     : Env      new)
      -> (graph   : Graph String)
      -> (result  : InterpTy     type)
                 -> Result   new type

  public export
  getResult : Result ctxt type -> InterpTy type
  getResult (R counter env g result) = result

  public export
  data GetGraph : (res : Result.Result ctxt type) -> Graph String -> Type
    where
      G : (g : Graph String) -> GetGraph (R c e g r) g

  public export
  getGraph : (r : Result.Result ctxt type) -> DPair (Graph String) (GetGraph r)
  getGraph (R counter env graph result) = MkDPair graph (G graph)

interp : (env     : Env this)
      -> (counter : Nat)
      -> (graph   : Graph String)
      -> (term    : Term this type that)
                 -> Result that type

-- [ NOTE ]
--
-- As normal
interp e c g (VarPort prf use)

  = let (new, ret) = lookup e prf use
    in R c new g ret

-- [ NOTE ]
--
-- Ports are leaf nodes in the graph.
interp e c g (Port flow dtype (FP u prf) body)
    = let    c1 = S c
      in let v  = vertexFromFlow flow c1 (size dtype)

      in let R e1 c2 g1 MkUnit = interp (Extend v e)
                                        c1
                                        (insertNode v g)
                                        body
      in R e1 c2 g1 MkUnit

  where
    vertexFromFlow : Direction -> Nat -> Nat -> Vertex String
    vertexFromFlow INPUT  = driver  ("INPUT : "  <+> show dtype )
    vertexFromFlow OUTPUT = catcher ("OUTPUT : " <+> show dtype )
    vertexFromFlow INOUT  = gateway ("INOUT : "  <+> show dtype )

interp e c g (Wire dtype (FC u prf) body)
  = let    c1 = S c
    in let c2 = S c1

    in let s = size dtype

    in let chanIN  = node ("CHAN_IN : "  <+> show dtype) c1 s 1
    in let chanOUT = node ("CHAN_OUT : " <+> show dtype) c2 1 s

    in let R e1 c3 g2 MkUnit = interp (Extend (chanIN, chanOUT) e)
                                      c2
                                      (updateWith g [chanIN, chanOUT]
                                                    [MkPair (ident chanIN) (ident chanOUT)])
                                       body
    in R e1 c3 g2 MkUnit

interp e c g (Gate gate body)
  = let R c1 e1 g1 res = interp e c g gate
    in interp (Extend res e1) c1 (merge g res) body

interp e c g (Stop prf)
  = R c Empty g MkUnit

interp e c g (Mux o s l r)

  = let c1 = S c

    in let mux = node "MUX" c1 3 1

    in let R c2 e1 g1 vo = interp e  c1 g  o
    in let R c3 e2 g2 vc = interp e1 c2 g1 s
    in let R c4 e3 g3 vl = interp e2 c2 g2 l
    in let R c5 e4 g4 vr = interp e3 c3 g3 r

    in let mg = fromLists [mux]
                          [ (ident vl,  ident mux)
                          , (ident vr,  ident mux)
                          , (ident vc,  ident mux)
                          , (ident mux, ident vo)
                          ]
    in R c5 e4 g4 mg

interp e c g (GateU kind o i)
    = let c1 = S c

      in let ugate = node (show kind) c1 1 1

      in let R c2 e1 g1 vo = interp e  c1 g  o
      in let R c3 e2 g2 vi = interp e1 c2 g1 i

      in R c3 e2 g2
              (fromLists [ugate] [ MkPair (ident vi)    (ident ugate)
                                 , MkPair (ident ugate) (ident vo)
                                 ])

interp e c g (GateB kind o l r)

   = let c1 = S c

    in let bgate = node (show kind) c1 2 1

    in let R c2 e1 g1 vo = interp e  c1 g  o
    in let R c3 e2 g2 vl = interp e1 c2 g1 l
    in let R c4 e3 g3 vr = interp e2 c3 g2 r

    in let bg = fromLists [bgate]
                          [ MkPair (ident bgate) (ident vo)
                          , MkPair (ident vl) (ident bgate)
                          , MkPair (ident vr) (ident bgate)
                          ]

    in R c4 e3 g3 bg

interp e c g (Split a b i)

  = let c1 = S c
    in let s = size LOGIC

    in let sVertex = both "SPLIT" c1 s

    in let R c2 e1 g1 av = interp e  c1 g  a
    in let R c3 e2 g2 bv = interp e1 c2 g1 b
    in let R c4 e3 g3 iv = interp e2 c3 g2 i

    in let esIS = replicate s (MkPair (ident iv)      (ident sVertex))
    in let esSA = replicate s (MkPair (ident sVertex) (ident av))
    in let esSB = replicate s (MkPair (ident sVertex) (ident bv))

    in R c4 e3
            g3
            (fromLists [av,bv,iv,sVertex]
                       (esIS ++ esSA ++ esSB))

interp e c g (Collect {type} o a b)

  = let c1 = S c
    in let s = size type

    in let sVertex = both "COLLECT" c1 s

    in let R c2 e1 g1 ov = interp e  c1 g  o
    in let R c3 e2 g2 av = interp e1 c2 g1 a
    in let R c4 e3 g3 bv = interp e2 c3 g2 b

    in let esAC = replicate s (MkPair (ident av) (ident sVertex))
    in let esBC = replicate s (MkPair (ident bv) (ident sVertex))
    in let esSO = replicate s (MkPair (ident sVertex) (ident ov))

    in R c4 e3
            g3
            (fromLists [ov,av,bv,sVertex]
                       (esAC ++ esBC ++ esSO))

interp e c g (Cast cast port)
    = let c1 = S c

      in let cVertex = both "CAST" c1 1

      in let R c2 e1 g1 what = interp e c1 g port

      in R c2 e1
              (updateWith g1 [cVertex] [buildEdge cast cVertex what])
              cVertex

  where buildEdge : Cast INOUT r -> (a,b : Vertex String) -> Edge
        buildEdge BI a b = MkPair (ident b) (ident a)
        buildEdge BO a b = MkPair (ident a) (ident b)

interp e c g (Project how prf use)

    = let (new, (i,o)) = lookup e prf use

      in R c new g (selectNode how i o)

  where selectNode : Project dir -> Vertex String -> Vertex String -> Vertex String
        selectNode WRITE i _ = i
        selectNode READ  _ o = o

interp e c g (Index dir idx prf use)
    = let c1 = S c

      in let idxVertex = both ("IDX [" <+> show (finToNat idx) <+> "](" <+>  show dir <+>")" ) c1 1

      in let (new,p) = lookup e prf use

      in R c1 new (updateWith g [idxVertex]
                               (buildEdge dir p idxVertex))
              idxVertex
  where buildEdge : Index direc -> (a,b : Vertex String) -> Edges
        buildEdge (UP x)   a b = [MkPair (ident b) (ident a)]
        buildEdge (DOWN x) a b = [MkPair (ident a) (ident b)]

public export
data ValidGraph : Graph type -> Type where
  IsValid : HasExactDegrees vs es
         -> ValidGraph (MkGraph vs es)

export
validGraph : {type : Type}
          -> (g    : Graph type)
                  -> DecInfo (HasExactDegree.Error type)
                             (ValidGraph g)
validGraph (MkGraph nodes edges) with (hasExactDegrees nodes edges)
  validGraph (MkGraph nodes edges) | (Yes prf)
    = Yes (IsValid prf)
  validGraph (MkGraph nodes edges) | (No msg contra)
    = No msg (\(IsValid prf) => contra prf)

public export
data Valid : (res  : Result ctxt TyUnit)
                  -> Type
  where
    D : {res : Result ctxt TyUnit}
     -> (g   : Graph String)
            -> GetGraph res g
            -> ValidGraph g
            -> Valid res

isValid : (r : Result ctxt TyUnit)
            -> DecInfo (Graph String, HasExactDegree.Error String)
                       (Valid r)
isValid r with (getGraph r)
  isValid (R c e g r) | (MkDPair g (G g)) with (validGraph g)
    isValid (R c e g r) | (MkDPair g (G g)) | (Yes prf)
      = Yes (D g (G g) prf)
    isValid (R c e g r) | (MkDPair g (G g)) | (No msg contra)
      = No (g,msg) (\(D graph (G graph) prf) => contra prf)

public export
data Run : (term : Term Nil TyUnit Nil) -> Type where
  R : (prf  : Valid (interp Empty Z (MkGraph Nil Nil) term))
           -> Run term

public export
getGraph : Run term -> DPair (Graph String) ValidGraph
getGraph (R (D g x y)) = MkDPair g y

export
run : (term : Term Nil TyUnit Nil)
           -> DecInfo (Graph String, HasExactDegree.Error String) (Run term)
run term with (isValid (interp Empty Z empty term))
  run term | (Yes prf) = Yes (R prf)
  run term | (No msg contra) = No msg (\(R prf) => contra prf)

export
runIO : (term : Term Nil TyUnit Nil)
             -> IO (Either (Graph String, HasExactDegree.Error String)
                           (Run term))
runIO term = pure $ (asEither (run term))

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


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

import System

import XML.DOM
import XML.Reader

import Freyja
import Freyja.Extract

import Readability

import Frigg.Effs
import Frigg.Options
import Frigg.Error
import Frigg.Eval
import Frigg.API
import Frigg.REPL

execMode : Maybe FriggMode -> Frigg ()
execMode Nothing       = printLn NoModeSpecified
execMode (Just VERS)   = printLn FeatureNotImpl
execMode (Just HELP)   = putStrLn friggHelpStr

execMode (Just REPL)  = friggREPL
execMode (Just Conv)  = convertShowDoc
execMode (Just Read)  = evalReadAndReport
execMode (Just Sif)   = evalSifAndReport
execMode (Just Templ) = evalTemplateAndReport

friggMain : Eff () FriggEffs
friggMain = do
  o <- processOptions
  putOptions o
  loadPatternDoc (patt o)
  execMode (mode o)

export
main : IO ()
main = do
  run $ friggMain
  exit 0

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

max_stars_repo_name: jfdm/frigg-tool

max_issues_repo_name: jfdm/frigg-tool

max_forks_repo_name: jfdm/frigg-tool


text:
ones : Stream Integer
ones = num :: ones
  where
    num : Integer -- gratuitous where for a regression test!
    num = 1

readNat : IO Nat
readNat = pure $ -- sprinkle some IO to prevent inlining
  case !getLine of
    "42" => Z
    _ => S (S (S (S Z)))

main : IO ()
main = do
  n <- readNat
  print (take n ones)


text:
module Utils.Parser

import Data.List
import Data.List.Elem
import Data.List1
import Data.Vect
import Data.Void
import Decidable.Equality
import Syntax.WithProof

public export
interface Cons a s | s where
  singleton : a -> s
  uncons : s -> Maybe (a, s)

public export
Cons Char String where
  singleton = cast
  uncons = strUncons

public export
Cons a (List a) where
  singleton = pure
  uncons [] = Nothing
  uncons (x :: xs) = Just (x, xs)

||| a simple incremental parser
public export
data Parser : (input : Type) -> (error : Type) -> (a : Type) -> Type where
  Fail : e -> Parser i e a
  Pure : (leftover : i) -> a -> Parser i e a
  More : (on_feed : (i -> Parser i e a)) -> Parser i e a
  Alt : Parser i e a -> Lazy (Parser i e a) -> Parser i e a

public export
Functor (Parser i e) where
  map f (Fail e) = Fail e
  map f (Pure leftover x) = Pure leftover (f x)
  map f (More on_feed) = More (map f . on_feed)
  map f (Alt p1 p2) = Alt (map f p1) (map f p2)

||| maps over the errors of the parser
public export
map_error : (e -> e') -> Parser i e a -> Parser i e' a
map_error f (Fail e) = Fail (f e)
map_error f (Pure leftover x) = Pure leftover x
map_error f (More on_feed) = More (map_error f . on_feed)
map_error f (Alt p1 p2) = Alt (map_error f p1) (map_error f p2)

public export
(<|>) : Semigroup e => Parser i e a -> Lazy (Parser i e a) -> Parser i e a
Fail e <|> p = map_error (e <+>) p
Pure leftover x <|> p = Pure leftover x
p <|> q = Alt p q

||| fail with an error
public export
fail : e -> Parser i e a
fail = Fail

||| feed input into the parser incrementally
public export
feed : (Semigroup e, Semigroup i) => i -> Parser i e a -> Parser i e a
feed input (Fail e) = Fail e
feed input (Pure leftover x) = Pure (leftover <+> input) x
feed input (More on_feed) = on_feed input
feed input (Alt p1 p2) = feed input p1 <|> feed input p2

apply : (Semigroup e, Semigroup i) => (Parser i e a -> Parser i e b) -> Parser i e a -> Parser i e b
apply f (Fail msg) = Fail msg
apply f (Alt p1 p2) = Alt (f p1) (f p2)
apply f (More on_feed) = More (f . on_feed)
apply f parser = More (\input => f $ feed input parser)

public export
pure : Monoid i => a -> Parser i e a
pure x = Pure neutral x

public export
(<*>) : (Semigroup e, Monoid i) => Parser i e (a -> b) -> Lazy (Parser i e a) -> Parser i e b
Pure leftover f <*> p = map f $ feed leftover p
p1 <*> p2 = apply (<*> p2) p1

public export
(<*) : (Semigroup e, Monoid i) => Parser i e a -> Parser i e b -> Parser i e a
x <* y = map const x <*> y

public export
(*>) : (Semigroup e, Monoid i) => Parser i e a -> Parser i e b -> Parser i e b
x *> y = map (const id) x <*> y

public export
(>>=) : (Semigroup e, Monoid i) => Parser i e a -> (a -> Parser i e b) -> Parser i e b
(>>=) (Pure leftover x) f = feed leftover $ f x
(>>=) p f = apply (>>= f) p

public export
more : (i -> Parser i e a) -> Parser i e a
more = More

||| peek into the next token without consuming it
public export
peek : Cons c i => Parser i e c
peek = more $ \input =>
  case uncons input of
    Just (x, _) => Pure input x
    Nothing => peek

||| reads the next token
public export
token : Cons c i => Parser i e c
token = more $ \input =>
  case uncons input of
    Just (x, xs) => Pure xs x
    Nothing => token

||| run `p` `k` times and collect the results
public export
count : (Semigroup e, Monoid i, Cons c i) => (k : Nat) -> (p : Parser i e a) -> Parser i e (Vect k a)
count Z parser = pure []
count (S k) parser = pure $ !parser :: !(count k parser)

||| return the result of `p` if it succeeds, otherwise return `x`
public export
option : (Semigroup e, Monoid i) => (x : a) -> (p : Parser i e a) -> Parser i e a
option x p = p <|> pure x

mutual
  public export
  some : (Semigroup e, Monoid i) => Parser i e a -> Parser i e (List1 a)
  some p = pure $ !p ::: !(many p)

  public export
  many : (Semigroup e, Monoid i) => Parser i e a -> Parser i e (List a)
  many p = option [] (forget <$> some p)

namespace Error
  ||| example: `SimpleError String`
  public export
  data SimpleError : Type -> Type where
    Msg : a -> SimpleError a
    Alt : SimpleError a -> SimpleError a -> SimpleError a
    Under : a -> SimpleError a -> SimpleError a

  public export
  Semigroup (SimpleError a) where
    (<+>) = Alt

  public export
  Show a => Show (SimpleError a) where
    show (Msg x) = show x
    show (Alt a b) = "(" <+> show a <+> " <|> " <+> show b <+> ")"
    show (Under x a) = "(" <+> show x <+> ": " <+> show a <+> ")"

  public export
  msg : e -> SimpleError e
  msg = Msg

  public export
  under : e -> Parser i (SimpleError e) a -> Parser i (SimpleError e) a
  under = map_error . Under


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 14, section 3, Hangman part

import Data.Vect

-- check that all functions are total
%default total

||| Remove an element in a vector
removeElem : (value : a) -> (xs : Vect (S n) a) ->
              {auto prf : Elem value xs} ->
              Vect n a
removeElem value (value :: ys) {prf = Here} = ys
removeElem {n = Z} value (y :: []) {prf = There later} = absurd later
removeElem {n = (S k)} value (y :: ys) {prf = There later}
  = y :: removeElem value ys

||| (Abstract) State of the game
data GameState : Type where
  NotRunning : GameState
  Running : (guesses : Nat) -> (letters : Nat) -> GameState

||| Result of a guess
data GuessResult = Correct | Incorrect

||| Letters in a word
letters : String -> List Char
letters str = nub $ map toUpper $ unpack str

||| Game commands
data GameCmd : (ty : Type) -> GameState -> (ty -> GameState) -> Type where
  ||| new game
  NewGame : (word : String) ->
            GameCmd () NotRunning $
                       const (Running 6 (length (letters word)))
  ||| won game
  Won : GameCmd () (Running (S guesses) 0) $
                   const NotRunning
  ||| lost game
  Lost : GameCmd () (Running 0 (S guesses)) $
                    const NotRunning
  ||| guess a letter
  Guess : (c : Char) ->
          GameCmd  GuessResult
                   (Running (S guesses) (S letters))
                   (\res => case res of
                              Correct => Running (S guesses) letters
                              Incorrect => Running guesses (S letters))
  ||| display the game state
  ShowState : GameCmd () state $ const state
  ||| display a message
  Message : String -> GameCmd () state $ const state
  ||| read a guess
  ReadGuess : GameCmd Char state $ const state
  ||| pure
  Pure : (res : ty) -> GameCmd ty (state res) state
  ||| sequence
  (>>=) : GameCmd a state1 state2 ->
          ((res : a) -> GameCmd b (state2 res) state3) ->
          GameCmd b state1 state3

namespace Loop
  ||| Game loop (type)
  data GameLoop : (ty : Type) -> GameState -> (ty -> GameState) -> Type where
    ||| sequence
    (>>=) : GameCmd a state1 state2 ->
            ((res : a) -> Inf (GameLoop b (state2 res) state3)) ->
            GameLoop b state1 state3
    ||| exit game
    Exit : GameLoop () NotRunning $ const NotRunning

||| Game loop (implementation)
gameLoop : GameLoop () (Running (S guesses) (S letters)) $ const NotRunning
gameLoop {guesses} {letters}
  = do ShowState
       g <- ReadGuess
       ok <- Guess g
       (case ok of
             Correct => case letters of
                          Z => do Won
                                  ShowState
                                  Exit
                          S k => do Message "Correct"
                                    gameLoop
             Incorrect => case guesses of
                          Z => do Lost
                                  ShowState
                                  Exit
                          S k => do Message "Incorrect"
                                    gameLoop)

||| Game set up
hangman : GameLoop () NotRunning $ const NotRunning
hangman = do NewGame "testing"
             gameLoop

||| (Concrete) Game state
data Game : GameState -> Type where
  GameStart : Game NotRunning
  GameWon : (word : String) -> Game NotRunning
  GameLost : (word : String) -> Game NotRunning
  InProgress : (word : String) -> (guesses : Nat) ->
               (missing : Vect letters Char) ->
               Game (Running guesses letters)

||| Game representation
Show (Game gs) where
  show GameStart = "Starting"
  show (GameWon word) = "Game won: word was " ++ word
  show (GameLost word) = "Game lost: word was " ++ word
  show (InProgress word guesses missing)
    = "\n" ++ pack (map hideMissing (unpack word))
           ++ "\n" ++ show guesses ++ " guesses left"
    where hideMissing : Char -> Char
          hideMissing c = if c `elem` missing then '-' else c

||| Fuel machinery
data Fuel = Dry | More (Lazy Fuel)

||| Result of a game
data GameResult : (ty : Type) -> (ty -> GameState) -> Type where
  OK : (res : ty) -> Game (outstate res) ->
       GameResult ty outstate
  OutOfFuel : GameResult ty outstate

||| Helper for returns of runs
ok : (res : ty) -> Game (outstate res) -> IO (GameResult ty outstate)
ok res st = pure (OK res st)

||| Running a game command over fuel
runCmd : Fuel ->
         Game instate ->
         GameCmd ty instate outstate ->
         IO (GameResult ty outstate)
runCmd fuel state (NewGame word)
  = ok () (InProgress (toUpper word) _ (fromList (letters word)))
runCmd fuel (InProgress word _ missing) Won = ok () (GameWon word)
runCmd fuel (InProgress word _ missing) Lost = ok () (GameLost word)
runCmd fuel (InProgress word _ missing) (Guess c)
  = case isElem c missing of
      Yes prf => ok Correct (InProgress word _ (removeElem c missing))
      No contra => ok Incorrect (InProgress word _ missing)
runCmd fuel state ShowState = do printLn state
                                 ok () state
runCmd fuel state (Message x) = do putStrLn x
                                   ok () state
runCmd (More fuel) state ReadGuess
  = do putStr "Guess: "
       input <- getLine
       case unpack input of
         [x] => if isAlpha x
                  then ok (toUpper x) state
                  else do putStrLn "Invalid input"
                          runCmd fuel state ReadGuess
         _ => do putStrLn "Invalid input"
                 runCmd fuel state ReadGuess
runCmd Dry _ _ = pure OutOfFuel
runCmd fuel state (Pure res) = ok res state
runCmd fuel st (cmd >>= next)
  = do OK cmdRes newSt <- runCmd fuel st cmd
        | OutOfFuel => pure OutOfFuel
       runCmd fuel newSt (next cmdRes)

||| Running a game loop over fuel
run : Fuel ->
      Game instate ->
      GameLoop ty instate outstate ->
      IO (GameResult ty outstate)
run Dry _ _ = pure OutOfFuel
run (More fuel) st (cmd >>= next)
  = do OK cmdRes newSt <- runCmd fuel st cmd
       | OutOfFuel => pure OutOfFuel
       run fuel newSt (next cmdRes)
run (More fuel) st Exit = ok () st

-- all remaining functions are partial
%default partial

forever : Fuel
forever = More forever

main : IO ()
main = do run forever GameStart hangman
          pure ()

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
import Control.Monad.Error.Either
import Control.Monad.Identity

-- Errorful monadic functions --

f1 : Monad m => Int -> m (Either String Int)
f1 5 = pure $ Right 0
f1 _ = pure $ Left "fail 1"

f2 : Monad m => Int -> m (Either String Int)
f2 6 = pure $ Right 0
f2 _ = pure $ Left "fail 2"

-- Compositions --

c1 : Monad m => m (Either String Int)
c1 = f1 1 *> f2 1

c2 : Monad m => m (Either String Int)
c2 = (f1 1 *> f2 1) @{Applicative.Compose}

c3 : Monad m => m (Either String Int)
c3 = runEitherT $ MkEitherT {m} (f1 1) *> MkEitherT {m} (f2 1)

-- These checks are meant to be true --

r1 : Bool
r1 = runIdentity c1 == Left "fail 2"

r2 : Bool
r2 = runIdentity c2 == Left "fail 1"

r3 : Bool
r3 = runIdentity c3 == Left "fail 1"

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Network.Curl.Types

import public Network.Curl.Types.Code
import public Network.Curl.Types.OptType
import public Network.Curl.Types.CurlEOption
import public Network.Curl.Types.CurlMOption
import public Network.Curl.Types.CurlECode
import public Network.Curl.Types.CurlMCode
import public Network.Curl.Types.SSL
import public Network.Curl.Types.Handle


text:
module Main

import Dart.Core
import Dart.FFI
import Dart.FFI.Elab
import Data.String

%foreign """
Dart:defineGenericBox,

// A Dart generic type.
class Box<T> {
  final T value;
  Box({this.value});
  // A Dart generic member function.
  Box<U> map<U>(U Function(T) f) => Box<U>(value: f(value));
}

defineGenericBox() {}
"""
defineGenericBox : PrimIO ()

%language ElabReflection

%runElab importDart [
  package "" [
    generic ["a"] $
      class' "Box" [
        final "a" "value",
        new "" ["value" :? "a"],
        generic ["b"] $
          fun ("Box" :<> "b") "map" ["f" :: "a" :-> "b"]
      ]
  ]
]

main : IO ()
main = do
  box <- Box.new [Box.New.value @= "foo"]
  Core.print box
  Core.print (box @. map String.toUpper @. value)
  primIO defineGenericBox


text:
||| Additional data types related to ordering notions
module Data.Order

%default total

||| Trichotomous formalises the fact that three relations are mutually exclusive.
||| It is meant to be used with relations that complement each other so that the
||| `Trichotomous lt eq gt` relation is the total relation.
public export
data Trichotomous : (lt, eq, gt : a -> a -> Type) -> (a -> a -> Type) where
  MkLT : {0 lt, eq, gt : a -> a -> Type} ->
         lt v w       -> Not (eq v w) -> Not (gt v w) -> Trichotomous lt eq gt v w
  MkEQ : {0 lt, eq, gt : a -> a -> Type} ->
         Not (lt v w) -> eq v w       -> Not (gt v w) -> Trichotomous lt eq gt v w
  MkGT : {0 lt, eq, gt : a -> a -> Type} ->
         Not (lt v w) -> Not (eq v w) -> gt v w       -> Trichotomous lt eq gt v w


text:
module Flutter.Widgets.Painter

import Dart.FFI.Elab
import Flutter.FFI

%language ElabReflection

%inline
public export
Painter : Type
Painter = Struct """
_Painter,

import 'package:flutter/material.dart' as material;

class _Painter extends material.CustomPainter {

  final void Function(material.Canvas, material.Size) onPaint;

  const _Painter({@material.required this.onPaint});

  @$.override
  void paint(material.Canvas canvas, material.Size size) {
    onPaint(canvas, size);
  }

  @$.override
  $.bool shouldRepaint(covariant material.CustomPainter oldDelegate) {
    return oldDelegate != this;
  }
}
""" []

%runElab importDart [
  package "" [
    partial' $
      class' "Painter" [
        extends "CustomPainter",
        const $ new "" [
          "onPaint" :? "Canvas" :-> "Size" :-> "IO" :<> "()"
        ]
      ]
  ]
]


text:
module Demo.Main

import Demo            -- this will import modules Demo.Utils and Demo.Other
-- import Demo.Other   -- import of just module Demo.Other

-- these imports allow you to access test functions from repl
import Test.Utils
import Test.Other

main : IO ()
main = do
    putStrLn hello
    putStrLn Demo.Other.hello  -- fully qualified

max_stars_repo_name: roycrippen/scratch

max_issues_repo_name: roycrippen/scratch

max_forks_repo_name: roycrippen/scratch


text:
> module NonNegRational.open_issues.Main

> import NonNegRational.NonNegRational
> import NonNegRational.BasicOperations
> import NonNegRational.BasicProperties
> import Fraction.Fraction
> import PNat.PNat
> import Nat.Positive

> %default total
> %auto_implicits off

> n : Nat
> n = 1

> x : NonNegRational
> x = fromFraction (1, Element (S n) MkPositive)

> y : NonNegRational
> y = fromFraction (n, Element (S n) MkPositive)

> q : x + y = 1
> q = Refl

> main : IO ()
> main = do putStrLn ("x           = " ++ show x)
>           putStrLn ("y           = " ++ show y)
>           putStrLn ("x + y       = " ++ show (x + y))

For small |n|, type checking time is roughly constant in |n| and
execution time is roughly linear in |n| as one would expect. But:

1) For |n > 399| the computation segfaults

2) Uncommenting lines 22-23 (the computation of |q|) yields unacceptable
   type checking times even for very small |n|:

     n = 1  ->   16 sec.
     n = 2  ->   18 sec.
     n = 3  ->   20 sec.
     n = 4  ->   28 sec.
     n = 5  ->   47 sec.
     n = 6  ->   88 sec.
     n = 7  ->  188 sec.
     n = 8  ->  647 sec.
     n = 9  ->  killed

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
import Data.Vect

%default total

infix 3 .<=.
(.<=.) : Int -> Int -> Bool
(.<=.) p q = case (p, q) of
  (0, _) => True
  _ => False

countGreater : (thr : Int) -> (ctx : Vect n Int) -> Nat
countGreater thr [] = Z
countGreater thr (x :: xs) with (x .<=. thr)
  countGreater thr (x :: xs) | True = countGreater thr xs
  countGreater thr (x :: xs) | False = S $ countGreater thr xs

-- map a variable from the old context to the erased context
-- where we erase all bindings less than or equal to the threshold
eraseVar : (thr : Int) -> (ctx : Vect n Int) -> Fin n -> Maybe (Fin (countGreater thr ctx))
eraseVar thr (x :: xs) j with (x .<=. thr)
  eraseVar thr (x :: xs) FZ | True = Nothing
  eraseVar thr (x :: xs) FZ | False = Just FZ
  eraseVar thr (x :: xs) (FS i) | True = FS <$> eraseVar thr xs i
  eraseVar thr (x :: xs) (FS i) | False = FS <$> eraseVar thr xs i

boom : Maybe (Fin 1)
boom = eraseVar 0 [0, 1] (FS FZ)


text:
module Package.IkanAssets

%access public export

flGitignore : String
flGitignore = """
*.ibc
*.o

# -*- mode: gitignore; -*-
*~
\#*\#
/.emacs.desktop
/.emacs.desktop.lock
*.elc
auto-save-list
tramp
.\#*

ikan
"""

flMain  : String
flMain = """
module Main\n
"""

flPkg  : String->String
flPkg nm = """
package $nm

modules = Main

main = Main

sourcedir = src

executable = main

"""

max_stars_repo_name: renpillay/ikan

max_issues_repo_name: renpillay/ikan

max_forks_repo_name: renpillay/ikan


text:
import Control.Monad.Identity
import Control.Monad.Writer

diga : a -> Writer (List a) ()
diga a = tell [a]

f : String -> Writer (List String) Int
f s = do
       diga s
       pure 1

-- o segundo item do writer é o log
-- snd $ runIdentity $ runWriterT f
-- o primeiro item do writer é o retorno
-- fst $ runIdentity $ runWriterT f

--transicoes : Pi -> Writer (List String) Pi
--transicoes p = do
--                    diga (show p)
--                    if (controlStackIsEmpty p) then
--                       pure p
                   -- ELSE
                   --    TRANSICOES (TRANSICAO P)

max_stars_repo_name: RonaldCamp/ImpCompiler

max_issues_repo_name: RonaldCamp/ImpCompiler

max_forks_repo_name: RonaldCamp/ImpCompiler


text:
foo : Int -> Int
foo x = case isLT of
            Yes => x*2
            No => x*4
    where
       data MyLT = Yes | No

       isLT : MyLT
       isLT = if x < 20 then Yes else No

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

test : List Nat
test = [c (S 1), c Z, d (S Z)]
  where c : Nat -> Nat
        c x = 42 + x

        d : Nat -> Nat
        d y = c (y + 1 + z y)
              where z : Nat -> Nat
                    z w = y + w


text:
module Test.Suite

import IdrTest.Test

import Test.Extra.ListTest
import Test.Extra.StringTest

suite : IO ()
suite = do
  runSuites
    [ Test.Extra.ListTest.suite
    , Test.Extra.StringTest.suite
    ]

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module TyTTP.HTTP.Routing

import Data.Mime.Apache
import Data.String

import TyTTP
import TyTTP.HTTP

namespace Method

  methodRouter : Alternative m
    => Method
    -> (
      Step Method u h1 s h2 a b
      -> m $ Step me' p' h1' s' h2' a' b'
    )
    -> Step Method u h1 s h2 a b
    -> m $ Step me' p' h1' s' h2' a' b'
  methodRouter m handler step =
    if step.request.method == m
    then handler step
    else empty

  export
  options : Alternative m
    => (
      Step Method u h1 s h2 a b
      -> m $ Step me' p' h1' s' h2' a' b'
    )
    -> Step Method u h1 s h2 a b
    -> m $ Step me' p' h1' s' h2' a' b'
  options = methodRouter OPTIONS

  export
  get : Alternative m
    => (
      Step Method u h1 s h2 a b
      -> m $ Step me' p' h1' s' h2' a' b'
    )
    -> Step Method u h1 s h2 a b
    -> m $ Step me' p' h1' s' h2' a' b'
  get = methodRouter GET

  export
  head : Alternative m
    => (
      Step Method u h1 s h2 a b
      -> m $ Step me' p' h1' s' h2' a' b'
    )
    -> Step Method u h1 s h2 a b
    -> m $ Step me' p' h1' s' h2' a' b'
  head = methodRouter HEAD

  export
  post : Alternative m
    => (
      Step Method u h1 s h2 a b
      -> m $ Step me' p' h1' s' h2' a' b'
    )
    -> Step Method u h1 s h2 a b
    -> m $ Step me' p' h1' s' h2' a' b'
  post = methodRouter POST

  export
  put : Alternative m
    => (
      Step Method u h1 s h2 a b
      -> m $ Step me' p' h1' s' h2' a' b'
    )
    -> Step Method u h1 s h2 a b
    -> m $ Step me' p' h1' s' h2' a' b'
  put = methodRouter PUT

  export
  delete : Alternative m
    => (
      Step Method u h1 s h2 a b
      -> m $ Step me' p' h1' s' h2' a' b'
    )
    -> Step Method u h1 s h2 a b
    -> m $ Step me' p' h1' s' h2' a' b'
  delete = methodRouter DELETE

  export
  trace : Alternative m
    => (
      Step Method u h1 s h2 a b
      -> m $ Step me' p' h1' s' h2' a' b'
    )
    -> Step Method u h1 s h2 a b
    -> m $ Step me' p' h1' s' h2' a' b'
  trace = methodRouter TRACE

  export
  connect : Alternative m
    => (
      Step Method u h1 s h2 a b
      -> m $ Step me' p' h1' s' h2' a' b'
    )
    -> Step Method u h1 s h2 a b
    -> m $ Step me' p' h1' s' h2' a' b'
  connect = methodRouter CONNECT

  export
  other : Alternative m
    => String
    -> (
      Step Method u h1 s h2 a b
      -> m $ Step me' p' h1' s' h2' a' b'
    )
    -> Step Method u h1 s h2 a b
    -> m $ Step me' p' h1' s' h2' a' b'
  other str = methodRouter (OtherMethod str)

namespace ContentType

  stringMatchesMime : Mime -> String -> Bool
  stringMatchesMime mime candidate =
    let mimeString = show mime
    in isPrefixOf mimeString $ toLower candidate

  export
  contentType : Alternative m
    => HasContentType h1
    => Mime
    -> (
      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'
  contentType mime handler step =
    case stringMatchesMime mime <$> getContentType step.request.headers of
      Just True => handler step
      _ => empty

  export
  json : Alternative m
    => HasContentType h1
    => (
      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'
  json = contentType APPLICATION_JSON

  export
  text : Alternative m
    => HasContentType h1
    => (
      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'
  text = contentType TEXT_PLAIN

  export
  binary : Alternative m
    => HasContentType h1
    => (
      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'
  binary = contentType APPLICATION_OCTET_STREAM

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
module TaggedProb

import Semiring
import Data.Morphisms
import HetVect
import Marginalization

-- %default total
%access public export

mutual
  data Prob : (unit : Type) -> (current : Type) -> Type where
    Dist : ((a -> s) -> s) -> Prob s a
    Fmap : (Vect xs -> b) -> ListProb s xs -> Prob s b
    Join : Prob s (Prob s a) -> Prob s a

  data ListProb : (unit : Type) -> (xs : List Type) -> Type where
    Nil : ListProb s []
    (::) : Prob s x -> ListProb s xs -> ListProb s (x::xs)

getProb : Prob s a -> (a -> s) -> s
getProb (Dist g) f = g f
getProb (Join x) f = getProb x (\a => getProb a f)
getProb (Fmap g ps) f = go g ps f where
  go : (Vect xs -> b) -> ListProb s xs -> (b -> s) -> s
  go f [] g = g (f [])
  go f (p :: ps) g = getProb p (\x => go (f . (x::)) ps g)

map : (a -> b) -> Prob s a -> Prob s b
map f (Dist g) = Dist (\h => g (h . f))
map f (Fmap g x) = Fmap (f . g) x
map f (Join x) = Join (map (\p => map f p) x)

(<$>) : (a -> b) -> Prob s a -> Prob s b
(<$>) = map

pure : a -> Prob s a
pure x = Fmap (\([]) => x) Nil

return : a -> Prob s a
return = pure

(<*>) : Prob s (a -> b) -> Prob s a -> Prob s b
(<*>) (Dist f) xs = Dist (\k => f (\c => getProb xs (k . c)))
(<*>) (Fmap f ps) p = Fmap (\(v::vs) => f vs v) (p::ps)
(<*>) (Join x) xs = Join (map (<*> xs) x)

join : Prob s (Prob s a) -> Prob s a
join = Join

(>>=) : Prob s a -> (a -> Prob s b) -> Prob s b
(>>=) p f = Join (map f p)

dice : Prob Double Int
dice = Dist (\f => Semiring.sum ( map (\n => f n / 6.0) [1 .. 6]) )

probOf : (Eq a, Semiring s) => a -> Prob s a -> s
probOf x p = getProb p (\y => if x == y then one else zer)

dices : Prob Double Int
dices = do
  x <- dice
  y <- dice
  return (x+y)

max_stars_repo_name: oisdk/belief-propagation-idris

max_issues_repo_name: oisdk/belief-propagation-idris

max_forks_repo_name: oisdk/belief-propagation-idris


text:
module Erlang

import public Erlang.Conversion as Erlang
import public Erlang.Decode as Erlang
import public Erlang.IO as Erlang
import public Erlang.Show as Erlang
import public Erlang.System.Concurrency as Erlang
import public Erlang.Types as Erlang
import public Erlang.Types.Map as Erlang


text:
a : Monad m => (Unit -> Unit) -> m $ Maybe ()

f : Monad m => m ()
f = do
  Just _ <- a id
    | Nothing => pure ()

  Just _ <- a id
  | Nothing => pure ()

  Just _ <- a $ \() => ()
  | Nothing => pure ()

  Just _ <- a $ \() => ()
    | Nothing => pure ()

  pure ()


text:
||| Internal functions used by HashMap and HashSet
module Data.HashMap.Internal

import Data.Array16
import public Data.Hashable

infix 6 `eq`

infixr 5 .&.
infixr 4 >>

||| Binary and.
%inline
(.&.) : Bits64 -> Bits64 -> Bits64
(.&.) = prim__and_Bits64

||| Right shift.
%inline
(>>) : Bits64 -> Bits64 -> Bits64
(>>) = prim__shr_Bits64

||| Mask for 4 bits.
export
data BitMask
    = BM0
    | BM1
    | BM2
    | BM3
    | BM4
    | BM5
    | BM6
    | BM7
    | BM8
    | BM9
    | BMa
    | BMb
    | BMc
    | BMd
    | BMe
    | BMf

||| Initial bit mask.
export
bitMask0 : BitMask
bitMask0 = BM0

public export
Hash : Type
Hash = Bits64

||| Mask 4 bits.
bitMask : BitMask -> Hash -> Bits64
bitMask mask h = case mask of
    BM0 => 0x000000000000000f .&. h >> 0x00
    BM1 => 0x00000000000000f0 .&. h >> 0x04
    BM2 => 0x0000000000000f00 .&. h >> 0x08
    BM3 => 0x000000000000f000 .&. h >> 0x0c
    BM4 => 0x00000000000f0000 .&. h >> 0x10
    BM5 => 0x0000000000f00000 .&. h >> 0x14
    BM6 => 0x000000000f000000 .&. h >> 0x18
    BM7 => 0x00000000f0000000 .&. h >> 0x1c
    BM8 => 0x0000000f00000000 .&. h >> 0x20
    BM9 => 0x000000f000000000 .&. h >> 0x24
    BMa => 0x00000f0000000000 .&. h >> 0x28
    BMb => 0x0000f00000000000 .&. h >> 0x2c
    BMc => 0x000f000000000000 .&. h >> 0x30
    BMd => 0x00f0000000000000 .&. h >> 0x34
    BMe => 0x0f00000000000000 .&. h >> 0x38
    BMf => 0xf000000000000000 .&. h >> 0x3c

||| Get the `BitMask` for the next 4 bits.
nextBitMask : BitMask -> BitMask
nextBitMask = \case
    BM0 => BM1
    BM1 => BM2
    BM2 => BM3
    BM3 => BM4
    BM4 => BM5
    BM5 => BM6
    BM6 => BM7
    BM7 => BM8
    BM8 => BM9
    BM9 => BMa
    BMa => BMb
    BMb => BMc
    BMc => BMd
    BMd => BMe
    BMe => BMf
    BMf => BM0

||| Is this the last 4 bits?
isLastBM : BitMask -> Bool
isLastBM = \case
    BMf => True
    _ => False

public export
Salt : Type
Salt = Bits64

||| Get the next salt.
-- TODO: get better algorithm
nextSalt : Salt -> Salt
nextSalt = (2 +)

||| Return just if a predicate is satisfied.
justWhen : Bool -> Lazy a -> Maybe a
justWhen True x = Just x
justWhen False _ = Nothing

||| Return `Nothing` is predicate is false, else return other value.
joinWhen : Bool -> Lazy (Maybe a) -> Maybe a
joinWhen True x = x
joinWhen False _ = Nothing

||| Internal Hash-array map trie (HAMT) that assumes the same hash and Eq is used.
export
data HashArrayMapTrie k v
    = Empty
    | Leaf Hash k v -- full hash
    | Collision Hash Salt (HashArrayMapTrie k v) -- full hash
    | Node (Array16 (HashArrayMapTrie k v))

export
Functor (HashArrayMapTrie k) where
    map _ Empty = Empty
    map f (Leaf h k v) = Leaf h k (f v)
    map f (Collision h s m) = Collision h s (map f m)
    map f (Node arr) = Node (map (map f) arr)

||| An empty HAMT.
export
empty : HashArrayMapTrie k v
empty = Empty

||| A HAMT containing one key and value.
export
singleton : Hash -> k -> v -> HashArrayMapTrie k v
singleton = Leaf

||| Create a HAMT from 2 keys and values, which have different hashes.
node2 : BitMask -> Hash -> k -> v -> Hash -> k -> v -> HashArrayMapTrie k v
node2 bm h0 k0 v0 h1 k1 v1 = Node $
    write (bitMask bm h0) (Leaf h0 k0 v0) $
    write (bitMask bm h1) (Leaf h1 k1 v1) $
    new Empty

mutual
    ||| Create a HAMT from 2 keys and values, where the hashes collide.
    collision2 :
        (eq : k -> k -> Bool) ->
        (hashWithSalt : Salt -> k -> Hash) ->
        Salt -> Hash ->
        k -> v -> k -> v ->
        HashArrayMapTrie k v
    collision2 eq hws s0 h k0 v0 k1 v1 =
        let s1 = nextSalt s0
            h0 = hws s1 k0
            h1 = hws s1 k1
            m0 = insert eq hws s1 BM0 h0 k0 v0
                $ insert eq hws s1 BM0 h1 k1 v1
                Empty
        in Collision h s1 m0

    export
    ||| Insert a key and value into a HAMT, replacing any existing values.
    insert :
        (eq : k -> k -> Bool) ->
        (hashWithSalt : Salt -> k -> Hash) ->
        Salt ->
        BitMask ->
        Hash ->
        k ->
        v ->
        HashArrayMapTrie k v ->
        HashArrayMapTrie k v
    insert eq hws s0 bm0 h0 k0 v0 m0 = case m0 of
        Empty => Leaf h0 k0 v0
        Leaf h1 k1 v1 => if h0 /= h1
            then node2 bm0 h0 k0 v0 h1 k1 v1
            else if k0 `eq` k1
                then Leaf h0 k0 v0
                else collision2 eq hws s0 h0 k0 v0 k1 v1
        Collision h1 s1 m1 => if h0 == h1
            then Collision h1 s1
                $ insert eq hws s1 BM0 (hws s1 k0) k0 v0 m1
            else -- hashes are different so it can't be the last bit mask
                Node $
                update (bitMask bm0 h0) (insert eq hws s0 (nextBitMask bm0) h0 k0 v0) $
                write (bitMask bm0 h1) m0 $
                new Empty
        Node ar =>
            Node $ update (bitMask bm0 h0)
            (insert eq hws s0 (nextBitMask bm0) h0 k0 v0) ar

||| Delete a key and value from a HAMT.
export
delete :
    (eq : k -> k -> Bool) ->
    (hashWithSalt : Salt -> k -> Hash) ->
    BitMask ->
    Hash -> k ->
    HashArrayMapTrie k v ->
    HashArrayMapTrie k v
delete eq hws bm0 h0 k0 m0 = case m0 of
    Empty => Empty
    Leaf h1 k1 v1 => if h0 == h1 && k0 `eq` k1
        then Empty
        else Leaf h1 k1 v1
    Collision h1 s1 m1 => if h0 == h1
        then Collision h1 s1
            $ delete eq hws BM0 (hws s1 k0) k0 m1
        else m0
    Node ar => Node $ update (bitMask bm0 h0) (delete eq hws (nextBitMask bm0) h0 k0) ar

||| Lookup a value at a key in a HAMT.
export
lookup :
    (eq : k -> k -> Bool) ->
    (hashWithSalt : Salt -> k -> Hash) ->
    BitMask ->
    Hash -> k ->
    HashArrayMapTrie k v ->
    Maybe v
lookup eq hws bm0 h0 k0 m0 = case m0 of
    Empty => Nothing
    Leaf h1 k1 v => justWhen (h0 == h1 && k0 `eq` k1) v
    Collision h1 s m1 => joinWhen (h0 == h1)
        $ lookup eq hws BM0 (hws s k0) k0 m1
    Node ar => lookup eq hws (nextBitMask bm0) h0 k0 $ index (bitMask bm0 h0) ar

||| Fold a HAMT with the key and value.
||| Note: this is based on the order of the hash not the key.
export
foldWithKey : (k -> v -> acc -> acc) -> acc -> HashArrayMapTrie k v -> acc
foldWithKey _ z Empty = z
foldWithKey f z (Leaf _ k v) = f k v z
foldWithKey f z (Collision _ _ m) = foldWithKey f z m
foldWithKey f z (Node ar) = foldr (flip $ foldWithKey f) z ar


text:
module NewEden.NaturalAxioms

import Prelude.Either

import NewEden.Algebra

{- NaturalProperties -

   An incomplete (http://www.dicosmo.org/Articles/zeroisnfa.pdf), non-recursive,
   axiomatic description of the natural numbers defined in terms of functions on a
   given type t.

   Despite the fact that this is *not* a full description of the behavior of the
   Peano naturals, it is probably good enough to do anything of practical interest
   to most people (even mathematicians, in most cases).
-}

data NaturalProperties : (t:Type) -> Type where
  ProofNaturalProperties :
      (Zero:t)
   -> (One:t)
   -> (lemmaDistinction: (Zero = One -> Void))
   -> (plus: (t -> t -> t))
   -> (lemmaPlusCommut: CommutativeFunction t plus)
   -> (lemmaPlusMonoid: Monoid t plus Zero)
   -> (lemmaPlusNoInverses: StrictMonoid lemmaPlusMonoid)
   -> (lemmaPlusMonomorphic: ((a:t) -> MonomorphicFunction $ plus a))
   -> (multiply: (t -> t -> t))
   -> (lemmaMultCommut: CommutativeFunction t multiply)
   -> (lemmaMultMonoid: Monoid t multiply One)
   -> (lemmaMultNoInverses: StrictMonoid lemmaMultMonoid)
   -> (lemmaMultiplyMonomorphic: ((a:t) -> MonomorphicFunction $ multiply a))
   -> (lemmaMultByZeroIsZero: ((a:t) -> multiply a Zero = Zero))
   -> (lemmaDistributive: ((a:t) -> (b:t) -> (c:t) -> multiply a (plus b c) = plus (multiply a b) (multiply a c)))
   -> (lemmaSequence: ((a:t) -> (b:t) -> (p1: (a = Zero -> Void)) -> (p2: plus a b = One) -> a = One))
   -> (compare:((a:t) -> (b:t) -> Either (a = b) (Either ((c ** ((plus a c = b, (c = Zero -> Void))))) (c ** ((plus b c = a, (c = Zero -> Void)))))))
   -> NaturalProperties t

max_stars_repo_name: identicalsnowflake/neweden

max_issues_repo_name: identicalsnowflake/neweden

max_forks_repo_name: identicalsnowflake/neweden


text:
import Erlang.Data.Ref

stsum : Num a => List a -> a
stsum xs
    = runST $
        do acc <- newRef 0
           add xs acc
           readRef acc
  where
    add : List a -> STRef s a -> ST s ()
    add [] ref = pure ()
    add (x :: xs) ref
        = do acc <- readRef ref
             writeRef ref (acc + x)
             add xs ref


text:
|||
||| A type-checkable division algorithm.
|||
||| CC-BY 2020 James B. Wilson
||| Department of Mathematics
||| Colorado State University
|||

data LT = {m:Nat} ->  (n:Nat) ->  Type
mkLessThan : {m:Nat} -> (n:Nat) -> (k:Nat) -> (e:n+k+1=m) -> LessThan m

data GTE = {m:Nat} ->  (n:Nat) ->  Type
mkGreaterThanEqual : {m:Nat} -> (n:Nat) -> (k:Nat) -> (e:n=m+k) -> GTE m

||| Proposition: For all positive natural numbers m and all natural numbers n,
||| there exists a natural number q, and natural number r < m, such that n=qm+r.
div :  (m:Nat) -> (n:Fin m) -> (q:Nat ** (r:Nat ** (n=(q*m+r+q)))
div m n = (Z ** (n ** Refl))
div m n = lift (div m n-m) where lift (q**(r**e)) = ((q+1)**(r**cong {f} e)))

---div S(m) n:Fin m = (q,n, refl:n=n)
---div S(m) n       = (1+q,r, cong(e):n=q*S(m)+r) where (q,r,e) = div(S(m),n-m)

max_stars_repo_name: algeboy/FormalAlgebra

max_issues_repo_name: algeboy/FormalAlgebra

max_forks_repo_name: algeboy/FormalAlgebra


text:
||| Views to show how a role interacts, or not, with a Term from a Global Type.
module Sessions.Global.Involved

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

import Data.List1

import Sessions.Meta
import Sessions.Global

%default total

public export
data Involved : (p, s, r : role)
                        -> Type
  where
    Sends : (prfS : role = s)
                 -> Involved role s r

    Recvs : (prfR : role = r)
                 -> Involved role s r

    Skips : (prfSNot : Not (role = s))
         -> (prfRNot : Not (role = r))
                    -> Involved role s r

public export
involved : DecEq role
        => (p, s, r : role)
        -> (contra  : Not (s = r))
                   -> Involved p s r
involved p s r contra with (decEq p s)
  involved p p r contra | (Yes Refl) = (Sends Refl)
  involved p s r contra | (No f) with (decEq p r)
    involved p s p contra | (No f) | (Yes Refl) = (Recvs Refl)
    involved p s r contra | (No f) | (No g) = (Skips f g)

-- [ EOF ]

max_stars_repo_name: DSbD-AppControl/sessions-playground

max_issues_repo_name: DSbD-AppControl/sessions-playground

max_forks_repo_name: DSbD-AppControl/sessions-playground


text:
module xquant.Spinor.Gamma

import xquant.Core.Types
import public Data.Matrix.Algebraic
import public Control.Algebra.NumericInstances
import public Data.Complex

%default total

-- Begin with two primative Gamma matrices, Γ0 and Γ1, generating Spin(2)

|||  Γ0 = iσy
g0 : Matrix 2 2 (Complex Integer)
g0 = [[c0, c1], [m1, c0]]

|||  Γ1 = σx
g1 : Matrix 2 2 (Complex Integer)
g1 = [[c0, c1], [c1, c0]]

{- Construct gammas for even-dimensional spinor representations (D = 2k + 2)
   First tensor as follows:

      G^μ    = Γ^mu <&> diag(-1,1),  (where mu <- [0..D-2])  or equivalently,
      G^μ    = Γ^mu <&> (g1 <> g0)

   Then adding two new gammas:

      G^{D-1} = Id <&> Γ1    = Id ⊗ σx
      G^D     = Id <&> -iΓ0  = Id ⊗ σy  -}

|||  Gamma matrices for even dimensions D = 2k + 2, with size 2^(k+1)
gammaEven : (k : Nat) -> Vect (k*2 + 2) $ Matrix (power 2 (S k)) (power 2 (S k)) (Complex Integer)
gammaEven Z      = [g0, g1]
gammaEven (S k) ?= {Lemma_1} map (\g => g <&> (g1 <> g0)) (gammaEven k) ++ [Id <&> g1, mi <#> Id <&> g0]

{- Matrices defined in this way satisy the gamma matrix algebra:

     {Γμ,Γν} = 2 η{μν} Id   (upstairs indices)

   They also furnish Poincaré generators   Σ^{μν} = −i[Γ^μ,Γ^ν]
   satisfying, by definition:   i[Σμν,Σσρ] = ηνσΣμρ + ημρΣνσ − ηνρΣμσ − ημσΣνρ

   This holds in any dimensionality and in both Minkowski and Euclidean signatures.

   Now define the "fifth Gamma Matrix", denoted Γ  -}

||| The "fifth gamma matrix" given by
|||
||| Γ = i^{–k} (Γ^0 ... Γ^{D-1})
|||
||| forms an odd-dimensional (irriducible) spinor representation by adding to the appropriate (gammaEven k)
gamma : Vect (k*2+2) $ Matrix (power 2 $ S k) (power 2 $ S k) (Complex Integer) ->
        Matrix (power 2 $ S k) (power 2 $ S k) (Complex Integer)
gamma {k} gs = (pow' mi k) <#> (product' gs)

{- Γ has eigenvalues of ±1 and satisfies:

     Γ^2 = 1
     {Γ,Γ^μ} = 0
     [Γ,Σ^{μν}] = 0  -}

g3 : Matrix 2 2 (Complex Integer)
g3 = product' $ with List [g0,g1]

{-
||| Anticommutation relation, {Γμ,Γν} = 2 η{μν} Id, for D = 2
D2_anticommRelation_00 : (g0 >><< g0) = ((-2 :+ 0) <#> Id)
D2_anticommRelation_00 = Refl

||| Anticommutation relation, {Γμ,Γν} = 2 η{μν} Id, for D = 2
D2_anticommRelation_01 : g0 >><< g1 = [neutral, neutral]
D2_anticommRelation_01 = Refl

||| Anticommutation relation, {Γμ,Γν} = 2 η{μν} Id, for D = 2
D2_anticommRelation_10 : g1 >><< g0 = [neutral, neutral]
D2_anticommRelation_10 = Refl

||| Anticommutation relation, {Γμ,Γν} = 2 η{μν} Id, for D = 2
D2_anticommRelation_11 : g1 >><< g1 = (2 :+ 0) <#> Id
D2_anticommRelation_11 = Refl
-}

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

multTwoRightPlusTimesOne : (n : Nat) -> mult n 2 = n + (mult n 1)
multTwoRightPlusTimesOne = proof
  intros
  rewrite (multRightSuccPlus n (S Z))
  trivial

multTwoRightPlus : (n : Nat) -> n * 2 = plus n n
multTwoRightPlus = proof
  intros
  rewrite (sym $ multTwoRightPlusTimesOne n)
  rewrite (sym $ multOneRightNeutral n)
  trivial

plusPlusZero : (x,y : Nat) -> x + y = x + (y + 0)
plusPlusZero = proof
  intros
  rewrite (sym $ plusZeroRightNeutral y)
  trivial

Lemma_1 = proof
  intros
  rewrite (plusZeroRightNeutral (plus (mult k 2) 2))
  rewrite (sym $ plusSuccRightSucc (plus (mult k 2) 2) 0)
  rewrite (sym $ plusSuccRightSucc (plus (mult k 2) 2) 1)
  rewrite (sym $ plusZeroRightNeutral (power 2 k))
  rewrite (sym $ plusZeroRightNeutral (power 2 k + (power 2 k)))
  rewrite (multTwoRightPlus (plus (power 2 k) (power 2 k)))
  rewrite (sym $ plusPlusZero (power 2 k) (power 2 k))
  trivial

max_stars_repo_name: fieldstrength/xquant

max_issues_repo_name: fieldstrength/xquant

max_forks_repo_name: fieldstrength/xquant


text:
-- Picture.idr
--
-- Demonstraters recursive data types

import Shape

||| Represents a picture with multiple shapes
public export
data Picture = Primitive Shape
             | Combine Picture Picture
             | Rotate Double Picture
             | Translate Double Double Picture

-- %name Shape shape, shape1, shape2
%name Picture pic, pic1, pic2

-- a test picture
rectangle : Picture
rectangle = Primitive (Rectangle 20 10)

circle : Picture
circle = Primitive (Circle 5)

triangle : Picture
triangle = Primitive (Triangle 10 10)

testPicture : Picture
testPicture = Combine (Translate 5 5 rectangle)
              (Combine (Translate 35 5 circle)
              (Translate 15 25 triangle))

||| Calculates the sum area of all shapes in a picture
export
pictureArea : Picture -> Double
pictureArea (Primitive shape) = area shape
pictureArea (Combine pic pic1) = pictureArea pic + pictureArea pic1
pictureArea (Rotate x pic) = pictureArea pic
pictureArea (Translate x y pic) = pictureArea pic

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
module Main

import Debug.Trace
import System
import System.Concurrency

-- Signal from child

main : IO ()
main = do
    mutex <- makeMutex
    cond <- makeCondition

    threadID <- fork $ do
        putStrLn "Hello"
        sleep 1
        conditionSignal cond

    mutexAcquire mutex
    conditionWait cond mutex
    putStrLn "Goodbye"
    mutexRelease mutex

    threadWait threadID