text:
module Data.SortedMap.Dependent

import Data.DPair

import Decidable.Equality

-- TODO: write split

-------------------------------
--- Internal representation ---
-------------------------------

private
data Tree : Nat -> (k : Type) -> (v : k -> Type) -> Ord k -> Type where
  Leaf : (x : k) -> v x -> Tree Z k v o
  Branch2 : Tree n k v o -> k -> Tree n k v o -> Tree (S n) k v o
  Branch3 : Tree n k v o -> k -> Tree n k v o -> k -> Tree n k v o -> Tree (S n) k v o

branch4 :
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o ->
  Tree (S (S n)) k v o
branch4 a b c d e f g =
  Branch2 (Branch2 a b c) d (Branch2 e f g)

branch5 :
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o ->
  Tree (S (S n)) k v o
branch5 a b c d e f g h i =
  Branch2 (Branch2 a b c) d (Branch3 e f g h i)

branch6 :
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o ->
  Tree (S (S n)) k v o
branch6 a b c d e f g h i j k =
  Branch3 (Branch2 a b c) d (Branch2 e f g) h (Branch2 i j k)

branch7 :
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o ->
  Tree (S (S n)) k v o
branch7 a b c d e f g h i j k l m =
  Branch3 (Branch3 a b c d e) f (Branch2 g h i) j (Branch2 k l m)

merge1 : Tree n k v o -> k -> Tree (S n) k v o -> k -> Tree (S n) k v o -> Tree (S (S n)) k v o
merge1 a b (Branch2 c d e) f (Branch2 g h i) = branch5 a b c d e f g h i
merge1 a b (Branch2 c d e) f (Branch3 g h i j k) = branch6 a b c d e f g h i j k
merge1 a b (Branch3 c d e f g) h (Branch2 i j k) = branch6 a b c d e f g h i j k
merge1 a b (Branch3 c d e f g) h (Branch3 i j k l m) = branch7 a b c d e f g h i j k l m

merge2 : Tree (S n) k v o -> k -> Tree n k v o -> k -> Tree (S n) k v o -> Tree (S (S n)) k v o
merge2 (Branch2 a b c) d e f (Branch2 g h i) = branch5 a b c d e f g h i
merge2 (Branch2 a b c) d e f (Branch3 g h i j k) = branch6 a b c d e f g h i j k
merge2 (Branch3 a b c d e) f g h (Branch2 i j k) = branch6 a b c d e f g h i j k
merge2 (Branch3 a b c d e) f g h (Branch3 i j k l m) = branch7 a b c d e f g h i j k l m

merge3 : Tree (S n) k v o -> k -> Tree (S n) k v o -> k -> Tree n k v o -> Tree (S (S n)) k v o
merge3 (Branch2 a b c) d (Branch2 e f g) h i = branch5 a b c d e f g h i
merge3 (Branch2 a b c) d (Branch3 e f g h i) j k = branch6 a b c d e f g h i j k
merge3 (Branch3 a b c d e) f (Branch2 g h i) j k = branch6 a b c d e f g h i j k
merge3 (Branch3 a b c d e) f (Branch3 g h i j k) l m = branch7 a b c d e f g h i j k l m

treeLookup : Ord k => (x : k) -> Tree n k v o -> Maybe (y : k ** v y) -- may also return an erased `So (x == y)`
treeLookup k (Leaf k' v) =
  if k == k' then
    Just (k' ** v)
  else
    Nothing
treeLookup k (Branch2 t1 k' t2) =
  if k <= k' then
    treeLookup k t1
  else
    treeLookup k t2
treeLookup k (Branch3 t1 k1 t2 k2 t3) =
  if k <= k1 then
    treeLookup k t1
  else if k <= k2 then
    treeLookup k t2
  else
    treeLookup k t3

treeInsert' : Ord k => (x : k) -> v x -> Tree n k v o -> Either (Tree n k v o) (Tree n k v o, k, Tree n k v o)
treeInsert' k v (Leaf k' v') =
  case compare k k' of
    LT => Right (Leaf k v, k, Leaf k' v')
    EQ => Left (Leaf k v)
    GT => Right (Leaf k' v', k', Leaf k v)
treeInsert' k v (Branch2 t1 k' t2) =
  if k <= k' then
    case treeInsert' k v t1 of
      Left t1' => Left (Branch2 t1' k' t2)
      Right (a, b, c) => Left (Branch3 a b c k' t2)
  else
    case treeInsert' k v t2 of
      Left t2' => Left (Branch2 t1 k' t2')
      Right (a, b, c) => Left (Branch3 t1 k' a b c)
treeInsert' k v (Branch3 t1 k1 t2 k2 t3) =
  if k <= k1 then
    case treeInsert' k v t1 of
      Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
      Right (a, b, c) => Right (Branch2 a b c, k1, Branch2 t2 k2 t3)
  else
    if k <= k2 then
      case treeInsert' k v t2 of
        Left t2' => Left (Branch3 t1 k1 t2' k2 t3)
        Right (a, b, c) => Right (Branch2 t1 k1 a, b, Branch2 c k2 t3)
    else
      case treeInsert' k v t3 of
        Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
        Right (a, b, c) => Right (Branch2 t1 k1 t2, k2, Branch2 a b c)

treeInsert : Ord k => (x : k) -> v x -> Tree n k v o -> Either (Tree n k v o) (Tree (S n) k v o)
treeInsert k v t =
  case treeInsert' k v t of
    Left t' => Left t'
    Right (a, b, c) => Right (Branch2 a b c)

delType : Nat -> (k : Type) -> (v : k -> Type) -> Ord k -> Type
delType Z k v o = ()
delType (S n) k v o = Tree n k v o

treeDelete : Ord k => (n : Nat) -> k -> Tree n k v o -> Either (Tree n k v o) (delType n k v o)
treeDelete _ k (Leaf k' v) =
  if k == k' then
    Right ()
  else
    Left (Leaf k' v)
treeDelete (S Z) k (Branch2 t1 k' t2) =
  if k <= k' then
    case treeDelete Z k t1 of
      Left t1' => Left (Branch2 t1' k' t2)
      Right () => Right t2
  else
    case treeDelete Z k t2 of
      Left t2' => Left (Branch2 t1 k' t2')
      Right () => Right t1
treeDelete (S Z) k (Branch3 t1 k1 t2 k2 t3) =
  if k <= k1 then
    case treeDelete Z k t1 of
      Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
      Right () => Left (Branch2 t2 k2 t3)
  else if k <= k2 then
    case treeDelete Z k t2 of
      Left t2' => Left (Branch3 t1 k1 t2' k2 t3)
      Right () => Left (Branch2 t1 k1 t3)
  else
    case treeDelete Z k t3 of
      Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
      Right () => Left (Branch2 t1 k1 t2)
treeDelete (S (S n)) k (Branch2 t1 k' t2) =
  if k <= k' then
    case treeDelete (S n) k t1 of
      Left t1' => Left (Branch2 t1' k' t2)
      Right t1' =>
        case t2 of
          Branch2 a b c => Right (Branch3 t1' k' a b c)
          Branch3 a b c d e => Left (branch4 t1' k' a b c d e)
  else
    case treeDelete (S n) k t2 of
      Left t2' => Left (Branch2 t1 k' t2')
      Right t2' =>
        case t1 of
          Branch2 a b c => Right (Branch3 a b c k' t2')
          Branch3 a b c d e => Left (branch4 a b c d e k' t2')
treeDelete (S (S n)) k (Branch3 t1 k1 t2 k2 t3) =
  if k <= k1 then
    case treeDelete (S n) k t1 of
      Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
      Right t1' => Left (merge1 t1' k1 t2 k2 t3)
  else if k <= k2 then
    case treeDelete (S n) k t2 of
      Left t2' => Left (Branch3 t1 k1 t2' k2 t3)
      Right t2' => Left (merge2 t1 k1 t2' k2 t3)
  else
    case treeDelete (S n) k t3 of
      Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
      Right t3' => Left (merge3 t1 k1 t2 k2 t3')

treeToList : Tree n k v o -> List (x : k ** v x)
treeToList = treeToList' (:: [])
  where
    -- explicit quantification to avoid conflation with {n} from treeToList
    treeToList' : {0 n : Nat} -> ((x : k ** v x) -> List (x : k ** v x)) -> Tree n k v o -> List (x : k ** v x)
    treeToList' cont (Leaf k v) = cont (k ** v)
    treeToList' cont (Branch2 t1 _ t2) = treeToList' (:: treeToList' cont t2) t1
    treeToList' cont (Branch3 t1 _ t2 _ t3) = treeToList' (:: treeToList' (:: treeToList' cont t3) t2) t1

----------------------
--- User interface ---
----------------------

export
data SortedDMap : (k : Type) -> (v : k -> Type) -> Type where
  Empty : Ord k => SortedDMap k v
  M : (o : Ord k) => (n : Nat) -> Tree n k v o -> SortedDMap k v

export
empty : Ord k => SortedDMap k v
empty = Empty

export
lookup : (x : k) -> SortedDMap k v -> Maybe (y : k ** v y) -- could return also `So (x == y)`
lookup _ Empty = Nothing
lookup k (M _ t) = treeLookup k t

export
lookupPrecise : DecEq k => (x : k) -> SortedDMap k v -> Maybe (v x)
lookupPrecise x = lookup x >=> \(y ** v) =>
  case decEq x y of
    Yes Refl => Just v
    No _     => Nothing

export
insert : (x : k) -> v x -> SortedDMap k v -> SortedDMap k v
insert k v Empty = M Z (Leaf k v)
insert k v (M _ t) =
  case treeInsert k v t of
    Left t' => (M _ t')
    Right t' => (M _ t')

export
singleton : Ord k => (x : k) -> v x -> SortedDMap k v
singleton k v = insert k v empty

export
insertFrom : Foldable f => f (x : k ** v x) -> SortedDMap k v -> SortedDMap k v
insertFrom = flip $ foldl $ flip $ uncurry insert

export
delete : k -> SortedDMap k v -> SortedDMap k v
delete _ Empty = Empty
delete k (M Z t) =
  case treeDelete Z k t of
    Left t' => (M _ t')
    Right () => Empty
delete k (M (S n) t) =
  case treeDelete (S n) k t of
    Left t' => (M _ t')
    Right t' => (M _ t')

export
fromList : Ord k => List (x : k ** v x) -> SortedDMap k v
fromList = foldl (flip (uncurry insert)) empty

export
toList : SortedDMap k v -> List (x : k ** v x)
toList Empty = []
toList (M _ t) = treeToList t

||| Gets the keys of the map.
export
keys : SortedDMap k v -> List k
keys = map fst . toList

export
values : SortedDMap k v -> List (x : k ** v x)
values = toList

treeMap : ({x : k} -> a x -> b x) -> Tree n k a o -> Tree n k b o
treeMap f (Leaf k v) = Leaf k (f v)
treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)
treeMap f (Branch3 t1 k1 t2 k2 t3)
    = Branch3 (treeMap f t1) k1 (treeMap f t2) k2 (treeMap f t3)

treeTraverse : Applicative f => ({x : k} -> a x -> f (b x)) -> Tree n k a o -> f (Tree n k b o)
treeTraverse f (Leaf k v) = Leaf k <$> f v
treeTraverse f (Branch2 t1 k t2) =
  Branch2
    <$> treeTraverse f t1
    <*> pure k
    <*> treeTraverse f t2
treeTraverse f (Branch3 t1 k1 t2 k2 t3) =
  Branch3
    <$> treeTraverse f t1
    <*> pure k1
    <*> treeTraverse f t2
    <*> pure k2
    <*> treeTraverse f t3

export
map : ({x : k} -> v x -> w x) -> SortedDMap k v -> SortedDMap k w
map _ Empty = Empty
map f (M _ t) = M _ $ treeMap f t

export
foldl : (acc -> (x : k ** v x) -> acc) -> acc -> SortedDMap k v -> acc
foldl f i = foldl f i . values

export
foldr : ((x : k ** v x) -> acc -> acc) -> acc -> SortedDMap k v -> acc
foldr f i = foldr f i . values

export
foldlM : Monad m => (acc -> (x : k ** v x) -> m acc) -> acc -> SortedDMap k v -> m acc
foldlM f i = foldl (\ma, b => ma >>= flip f b) (pure i)

export
foldMap : Monoid m => (f : (x : k) -> v x -> m) -> SortedDMap k v -> m
foldMap f = foldr ((<+>) . uncurry f) neutral

export
null : SortedDMap k v -> Bool
null Empty   = True
null (M _ _) = False

export
traverse : Applicative f => ({x : k} -> v x -> f (w x)) -> SortedDMap k v -> f (SortedDMap k w)
traverse _ Empty = pure Empty
traverse f (M _ t) = M _ <$> treeTraverse f t

||| Merge two maps. When encountering duplicate keys, using a function to combine the values.
||| Uses the ordering of the first map given.
export
mergeWith : DecEq k => ({x : k} -> v x -> v x -> v x) -> SortedDMap k v -> SortedDMap k v -> SortedDMap k v
mergeWith f x y = insertFrom inserted x where
  inserted : List (x : k ** v x)
  inserted = do
    (k ** v) <- toList y
    let v' = (maybe id f $ lookupPrecise k x) v
    pure (k ** v')

||| Merge two maps using the Semigroup (and by extension, Monoid) operation.
||| Uses mergeWith internally, so the ordering of the left map is kept.
export
merge : DecEq k => ({x : k} -> Semigroup (v x)) => SortedDMap k v -> SortedDMap k v -> SortedDMap k v
merge = mergeWith (<+>)

||| Left-biased merge, also keeps the ordering specified  by the left map.
export
mergeLeft : DecEq k => SortedDMap k v -> SortedDMap k v -> SortedDMap k v
mergeLeft = mergeWith const

treeLeftMost : Tree n k v o -> (x : k ** v x)
treeLeftMost (Leaf x y) = (x ** y)
treeLeftMost (Branch2 x _ _) = treeLeftMost x
treeLeftMost (Branch3 x _ _ _ _) = treeLeftMost x

treeRightMost : Tree n k v o -> (x : k ** v x)
treeRightMost (Leaf x y) = (x ** y)
treeRightMost (Branch2 _ _ x) = treeRightMost x
treeRightMost (Branch3 _ _ _ _ x) = treeRightMost x

treeLookupBetween : Ord k => k -> Tree n k v o -> (Maybe (x : k ** v x), Maybe (x : k ** v x))
treeLookupBetween k (Leaf k' v) with (k < k')
  treeLookupBetween k (Leaf k' v) | True = (Nothing, Just (k' ** v))
  treeLookupBetween k (Leaf k' v) | False = (Just (k' ** v), Nothing)
treeLookupBetween k (Branch2 t1 k' t2) with (k < k')
  treeLookupBetween k (Branch2 t1 k' t2) | True = -- k < k'
    let (lower, upper) = treeLookupBetween k t1 in
    (lower, upper <|> pure (treeLeftMost t2))
  treeLookupBetween k (Branch2 t1 k' t2) | False = -- k >= k'
    let (lower, upper) = treeLookupBetween k t2 in
    (lower <|> pure (treeRightMost t1), upper)
treeLookupBetween k (Branch3 t1 k1 t2 k2 t3) with (k < k1)
  treeLookupBetween k (Branch3 t1 k1 t2 k2 t3) | True = treeLookupBetween k (Branch2 t1 k1 t2)
  treeLookupBetween k (Branch3 t1 k1 t2 k2 t3) | False with (k < k2)
    treeLookupBetween k (Branch3 t1 k1 t2 k2 t3) | False | False = treeLookupBetween k (Branch2 t2 k2 t3)
    treeLookupBetween k (Branch3 t1 k1 t2 k2 t3) | False | True = --k1 <= k < k2
      let (lower, upper) = treeLookupBetween k (Branch2 t1 k1 t2) in
      (lower, upper <|> pure (treeLeftMost t3))

||| looks up a key in map, returning the left and right closest values, so that
|||  k1 <= k < k2. If at the end of the beginning and/or end of the sorted map, returns
||| nothing appropriately
export
lookupBetween : k -> SortedDMap k v -> (Maybe (x : k ** v x), Maybe (x : k ** v x))
lookupBetween k Empty = (Nothing, Nothing)
lookupBetween k (M _ t) = treeLookupBetween k t

||| Returns the leftmost (least) key and value
export
leftMost : SortedDMap k v -> Maybe (x : k ** v x)
leftMost Empty = Nothing
leftMost (M _ t) = Just $ treeLeftMost t

||| Returns the rightmost (greatest) key and value
export
rightMost : SortedDMap k v -> Maybe (x : k ** v x)
rightMost Empty = Nothing
rightMost (M _ t) = Just $ treeRightMost t

export
(Show k, {x : k} -> Show (v x)) => Show (SortedDMap k v) where
   show m = "fromList " ++ (show $ toList m)

export
(DecEq k, {x : k} -> Eq (v x)) => Eq (SortedDMap k v) where
  (==) = (==) `on` toList

export
strictSubmap : DecEq k => ({x : k} -> Eq (v x)) => (sub : SortedDMap k v) -> (sup : SortedDMap k v) -> Bool
strictSubmap sub sup = all (\(k ** v) => Just v == lookupPrecise k sup) $ toList sub

-- TODO: is this the right variant of merge to use for this? I think it is, but
-- I could also see the advantages of using `mergeLeft`. The current approach is
-- strictly more powerful I believe, because `mergeLeft` can be emulated with
-- the `First` monoid. However, this does require more code to do the same
-- thing.
export
DecEq k => ({x : k} -> Semigroup (v x)) => Semigroup (SortedDMap k v) where
  (<+>) = merge

||| For `neutral <+> y`, y is rebuilt in `Ord k`, so this is not a "strict" Monoid.
||| However, semantically, it should be equal.
export
DecEq k => Ord k => ({x : k} -> Semigroup (v x)) => Monoid (SortedDMap k v) where
  neutral = empty


text:
module Circuits.NetList.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.List.DeBruijn
import Toolkit.Data.Whole

import Circuits.NetList.Types
import Circuits.NetList.Terms

%default total

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

InterpTy (TyPort x)
  = Vertex String

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

InterpTy TyGate
  = Graph String

namespace Environments

  public export
  Env : List Ty -> Type
  Env = Env Ty InterpTy

namespace Result

  public export
  data Result : (type : Ty)
                     -> Type
    where
      R : (counter : Nat)
       -> (graph   : Graph String)
       -> (result  : InterpTy type)
                  -> Result type
  public export
  getResult : Result type -> InterpTy type
  getResult (R _ _ res) = res

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

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

interp : (env     : Env ctxt)
      -> (counter : Nat)
      -> (graph   : Graph String)
      -> (term    : Term ctxt type)
                 -> Result type
interp env c g (Var x)
  = R c g (read x env)

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

      in let R c2 g1 MkUnit = interp (extend env v)
                                     c1
                                     (insertNode v g)
                                     body
      in R 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 )

-- [ NOTE ]
--
-- Wires are internal connected nodes in the graph
interp env c g (Wire dtype 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 c3 g2 MkUnit = interp (extend env (chanIN, chanOUT))
                                     c2
                                     (updateWith g [chanIN, chanOUT]
                                                   [MkPair (ident chanIN) (ident chanOUT)])
                                     body
      in R c3 g2 MkUnit

-- [ NOTES ]
--
--
interp env c g (GateDecl gate body)
  = let    R c1 g1 g2     = interp env c g gate
    in let R c2 g3 MkUnit = interp (extend env g2) c1 (merge g1 g2) body
    in     R c2 g3 MkUnit

-- [ NOTE ]
--
--
interp env c g Stop
  = R c g MkUnit

-- [ NOTE ]
--
-- 'Just' an edge
interp env c g (Assign {type} i o rest)
  = let    R c1 g1 vi = interp env c  g  i
    in let R c2 g2 vo = interp env c1 g1 o

    in let es = replicate (size type) (MkPair (ident vi) (ident vo))

    in interp env c2 (updateWith g2 Nil es)
                     rest

-- [ NOTE ]
--
-- Multiplexers are internal nodes connected to other nodes.
interp env c g (Mux o x l r)
    = let c1 = S c

      in let mux = node "MUX" c1 3 1

      in let R c2 g1 vo = interp env c1 g  o
      in let R c3 g2 vl = interp env c2 g1 l
      in let R c4 g3 vr = interp env c3 g2 r
      in let R c5 g4 vc = interp env c4 g3 x

      in R c5 g4
              (fromLists [mux] [ MkPair (ident vl)  (ident mux)
                               , MkPair (ident vr)  (ident mux)
                               , MkPair (ident vc)  (ident mux)
                               , MkPair (ident mux) (ident vo)
                               ])

-- [ NOTE ]
--
-- internal nodes connected to other nodes.
interp env c g (GateB x o l r)
    = let c1 = S c

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

      in let R c2 g1 vo = interp env c1 g  o
      in let R c3 g2 vl = interp env c2 g1 l
      in let R c4 g3 vr = interp env c3 g2 r

      in R c4 g3
              (fromLists [bgate] [ MkPair (ident vl)    (ident bgate)
                                 , MkPair (ident vr)    (ident bgate)
                                 , MkPair (ident bgate) (ident vo)
                                 ])

-- [ NOTE ]
--
-- Multiplexers are internal nodes connected to other nodes.
interp env c g (GateU x o i)
    = let c1 = S c

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

      in let R c2 g1 vo = interp env c1 g  o
      in let R c3 g2 vi = interp env c2 g1 i

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

-- [ NOTE ]
--
-- Indexing ports creates a new edge in the graph to a node representing the index.
--
interp env c g (Index dir what idx)
    = let c1 = S c

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

      in let R c2 gsub whatVertex = interp env c1 g what

      in R c2 (updateWith gsub [idxVertex]
                               (buildEdge dir whatVertex 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)]

-- [ NOTE ]
--
-- Projection of channels returns the channel's appropriate endpoint.
interp env c g (Project how chan)

    = let R c1 g2 (i,o) = interp env c g chan

      in R c1 g2
              (selectNode how i o)

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

-- [ NOTE]
--
-- Splitting inserts a node.
interp env 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 g1 av = interp env c1 g  a
    in let R c3 g2 bv = interp env c2 g1 b
    in let R c4 g3 iv = interp env 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 g3
            (fromLists [av,bv,iv,sVertex]
                       (esIS ++ esSA ++ esSB))

interp env 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 g1 ov = interp env c1 g  o
    in let R c3 g2 av = interp env c2 g1 a
    in let R c4 g3 bv = interp env 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 g3
            (fromLists [ov,av,bv,sVertex]
                       (esAC ++ esBC ++ esSO))

-- [ NOTE ]
--
-- Casting inserts a new edge
interp env c g (Cast {type} how what)
    = let c1 = S c

      in let s = size type

      in let cVertex = both "CAST" c1 s

      in let R c2 g1 what = interp env c1 g what

      in let es = replicate s (buildEdge how cVertex what)

      in R c2 (updateWith g1 [cVertex] es)
              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)

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 TyUnit)
                  -> Type
  where
    D : {res : Result TyUnit}
     -> (g   : Graph String)
            -> GetGraph res g
            -> ValidGraph g
            -> Valid res

isValid : (r : Result TyUnit)
            -> DecInfo (Graph String, HasExactDegree.Error String)
                       (Valid r)
isValid r with (getGraph r)
  isValid (R c g r) | (MkDPair g (G g)) with (validGraph g)
    isValid (R c g r) | (MkDPair g (G g)) | (Yes prf)
      = Yes (D g (G g) prf)
    isValid (R c 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) -> Type where
  R : (prf  : Valid (interp Nil 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)
           -> DecInfo (Graph String, HasExactDegree.Error String) (Run term)
run term with (isValid (interp Nil 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)
             -> IO (Either (Graph String, HasExactDegree.Error String)
                           (Run term))
runIO term = pure $ (asEither (run term))

-- [ EOF ]

ext: idr

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
-- Parses even at https://github.com/gallais/Idris2/tree/issue710 at 9c7705f7c8db

interface Lalala where
  constructor cons
  x : Int -> Int

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Commons.Control.File

import Control.ST

import Commons.Control.ST

import Commons.Data.Action

%access public export
%default total

-- -------------------------------------------------------------- [ Predicates ]

||| A record of the file modes that can read from a file.
data ValidModeRead : Mode -> Type where
  VMRRead   : ValidModeRead Read
  VMRReadW  : ValidModeRead ReadWrite
  VMRReadWT : ValidModeRead ReadWriteTruncate
  VMRReadA  : ValidModeRead ReadAppend

||| A record of the file modes that can write from a file.
data ValidModeWrite : Mode -> Type where
  VMWWrite  : ValidModeWrite WriteTruncate
  VMWAppend : ValidModeWrite Append
  VMWReadW  : ValidModeWrite ReadWrite
  VMWReadWT : ValidModeWrite ReadWriteTruncate

data State = Closed | Open

-- -------------------------------------------------- [ Custom Error Reporting ]

||| Alias for File actions.
FileAction : ActionTy -> Type -> Type
FileAction action = Action action FileError

interface FileIO (m : Type -> Type) where
  data File : Mode -> State -> Type

  open : (fname : String)
      -> (fmode : Mode)
      -> ST m (FileAction RESULT Var) [addIfResult $ File fmode Open]

  openX : (fname : String)
       -> (fmode : Mode)
       -> ST m (FileAction RESULT Var) [addIfResult $ File fmode Open]

  close : (fh : Var)
        -> ST m () [Remove fh (File fm st)]

  readChar : (fh : Var)
          -> {auto prf : ValidModeRead fm}
          -> ST m (FileAction RESULT Char)
                  [fh ::: File fm Open :-> onAction (File fm Open) (File fm Closed)]

  readLine : (fh : Var)
          -> {auto prf : ValidModeRead fm}
          -> ST m (FileAction RESULT String)
                  [fh ::: File fm Open :-> onAction (File fm Open) (File fm Closed)]

  readFile : (fname : String)
          -> STrans m (FileAction RESULT String) xs (const xs)

  writeStr : (fh : Var)
          -> (str : String)
          -> {auto prf : ValidModeWrite fm}
          -> ST m (FileAction SUCCESS ())
                  [fh ::: File fm Open :-> onAction (File fm Open) (File fm Closed)]

  writeLine : (fh : Var)
           -> (str : String)
           -> {auto prf : ValidModeWrite fm}
           -> ST m (FileAction SUCCESS ())
                   [fh ::: File fm Open :-> onAction (File fm Open) (File fm Closed)]

  writeFile : (fname : String)
           -> (str : String)
           -> STrans m (FileAction SUCCESS ()) xs (const xs)

  -- misc
  flush : (fh : Var)
       -> ST m () [fh ::: File fm Open]

  eof : (fh : Var)
     -> ST m Bool [fh ::: File fm Open]

FileIO IO where
  File x y = State File

  open fname fmode = do
    res <- lift $ openFile fname fmode
    case res of
      Left err => pure $ Error err
      Right fh => do
        v <- new fh
        pure $ Result v

  openX fname fmode = do
    res <- lift $ openFileX fname fmode
    case res of
      Left err => pure $ Error err
      Right fh => do
        v <- new fh
        pure $ Result v

  close v = do
     fh  <- read v
     lift $ closeFile fh
     delete v
     pure ()

  readChar var = do
      fh <- read var
      case !(lift $ fgetc fh) of
        Left err => pure $ Error err
        Right ln => pure $ Result ln

  readLine var = do
    fh <- read var
    case !(lift $ fGetLine fh) of
      Left err => pure $ Error err
      Right ln => pure $ Result ln

  readFile fname = do
    case !(lift $ readFile fname) of
      Left err  => pure $ Error err
      Right str => pure $ Result str

  writeStr var str = do
    fh <- read var
    case !(lift $ fPutStr fh str) of
      Left err => pure $ Error err
      Right _  => pure $ Success

  writeLine var str = do
    fh <- read var
    case !(lift $ fPutStrLn fh str) of
      Left err => pure $ Error err
      Right _  => pure $ Success

  writeFile fname str = do
    case !(lift $ writeFile fname str) of
      Left err => pure $ Error err
      Right  _ => pure $ Success

  flush var = do
    fh <- read var
    res <- lift $ fflush fh
    pure res

  eof var = do
    fh <- read var
    res <- lift $ fEOF fh
    pure res

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

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module Data.Strings

import public Data.String as Data.Strings

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
module Inigo.Async.FS

import Inigo.Async.Promise
import Inigo.Async.Util
import Data.Buffer
import Extra.Buffer
import System.Path

%foreign (promisifyPrim "(path)=>require('fs').promises.readFile(path,'utf8')")
fs_readFile__prim : String -> promise String

%foreign (promisifyPrim "(path)=>require('fs').promises.readFile(path)")
fs_readFileBuf__prim : String -> promise Buffer

%foreign (promisifyPrim "(path,contents)=>require('fs').promises.writeFile(path,contents)")
fs_writeFile__prim : String -> String -> promise ()

%foreign (promisifyPrim "(path,contents)=>require('fs').promises.writeFile(path,contents)")
fs_writeFileBuf__prim : String -> Buffer -> promise ()

%foreign (promisifyPrim "(path,r)=>require('fs').promises.mkdir(path,{recursive: r === 1})")
fs_mkdir__prim : String -> Int -> promise ()

%foreign (promisifyPrim "(path,r)=>require('fs').promises.rmdir(path,{recursive: r === 1})")
fs_rmdir__prim : String -> Int -> promise ()

%foreign (promisifyPrim "(path)=>require('fs').promises.readdir(path).then(__prim_js2idris_array)")
fs_getFiles__prim : String -> promise (List String)

%foreign (promisifyPrim "(path)=>require('fs').promises.stat(path).then((s)=>s.isDirectory() ? 1 : 0)")
fs_isDir__prim : String -> promise Int

%foreign (promisifyPrim "(path)=>require('fs').promises.access(path).then(()=>1).catch(()=>0)")
fs_exists__prim : String -> promise Int

export
fs_readFile : String -> Promise String
fs_readFile path =
  promisify (fs_readFile__prim path)

export
fs_writeFile : String -> String -> Promise ()
fs_writeFile path contents =
  promisify (fs_writeFile__prim path contents)

export
fs_readFileBuf : String -> Promise Buffer
fs_readFileBuf path =
  promisify (fs_readFileBuf__prim path)

export
fs_writeFileBuf : String -> Buffer -> Promise ()
fs_writeFileBuf path contents =
  promisify (fs_writeFileBuf__prim path contents)

export
fs_mkdir : Bool -> String -> Promise ()
fs_mkdir recursive path =
  promisify (fs_mkdir__prim path (boolToInt recursive))

export
fs_rmdir : Bool -> String -> Promise ()
fs_rmdir recursive path =
  promisify (fs_rmdir__prim path (boolToInt recursive))

export
fs_getFiles : String -> Promise (List String)
fs_getFiles path =
  promisify (fs_getFiles__prim path)

export
fs_isDir : String -> Promise Bool
fs_isDir path =
  intToBool <$> promisify (fs_isDir__prim path)

export
fs_exists : String -> Promise Bool
fs_exists path =
  intToBool <$> promisify (fs_exists__prim path)

export
fs_getFilesR : String -> Promise (List String)
fs_getFilesR path =
  doGetFilesR path
  where
  doGetFilesR : String -> Promise (List String)
  doGetFilesR path =
    do
      isDir <- fs_isDir path
      if isDir
        then do
          entries <- fs_getFiles path
          let fullEntries = map (path </>) entries
          allFiles <- all (map doGetFilesR fullEntries)
          pure (concat allFiles)
        else
          pure [path]

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
||| Spec: https://webassembly.github.io/spec/core/syntax/modules.html#tables
module WebAssembly.Structure.Modules.Tables

import WebAssembly.Structure.Types

import Decidable.Equality

-- Definition

public export
record Table where
  constructor MkTable
  type : TableType

-- Equality

total public export
lemma_table__type_injective : ((t1 = t2) -> Void) -> (MkTable t1 = MkTable t2) -> Void
lemma_table__type_injective t1_not_t2 Refl = t1_not_t2 Refl

-- Decidable Equality

public export
implementation DecEq Table where
  decEq (MkTable t1) (MkTable t2) = case decEq t1 t2 of
    No t1_not_t2 => No $ lemma_table__type_injective t1_not_t2
    Yes Refl     => Yes Refl

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
> module Main

> import Data.List

> import EscardoOliva.SelectionFunction
> import EscardoOliva.Operations

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

> xs : List Int
> xs = [7,-3, 0]

> partial
> e : J Int Int
> e = argsup xs

> f : Int -> J Int (List Int)
> f i = \ p => [p [i, i, i]]

> partial
> es : J Int (List Int)
> es = otimes e f

> partial
> ys : List Int
> ys = es sum

> partial
> main : IO ()
> main = do putStr ("ys = " ++ show ys ++ "\n")

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module GRIN.Analysis.CallGraph

import Data.Maybe
import Data.SortedMap as Map
import Data.SortedSet as Set

import GRIN.AST
import GRIN.GrinState

callsSExp : SExp name -> SortedSet name -> SortedSet name
callsExp : Exp name -> SortedSet name -> SortedSet name

callsSExp (Do e) = callsExp e
callsSExp (App fn _) = insert fn
callsSExp _ = id

callsExp (SimpleExp e) m = callsSExp e m
callsExp (Bind _ rhs rest) m = callsExp rest $ callsSExp rhs m
callsExp (Case _ alts) m = foldr (callsExp . altExp) m alts

||| Get the call graph for all functions called by `def`.
callGraphDef :
    Ord name =>
    SortedMap name (Extern name) ->
    SortedMap name (Def name) ->
    (fn : name) ->
    CallGraph name ->
    CallGraph name
callGraphDef exts defs fn cg = case lookup fn cg of
    Nothing => case lookup fn defs of
        Just (MkDef _ _ exp _) =>
            let calls = callsExp exp empty
            in foldr (callGraphDef exts defs) (insert fn calls cg) calls
        Nothing => case lookup fn exts of
            Just _ => insert fn empty cg
            Nothing => cg
    Just _ => cg

||| Get the call graph for all functions (transitively) called by main
export
callsGraph : Ord name => Prog name -> CallGraph name
callsGraph (MkProg exts defs main) = case lookup main defs of
    Nothing => empty
    Just (MkDef fn _ _ _) => callGraphDef exts defs fn empty

export
calledByGraph : Ord name => CallGraph name -> CallGraph name
calledByGraph calls = foldl go empty (Map.toList calls)
  where
    go : CallGraph name -> (name, SortedSet name) -> CallGraph name
    go cg0 (caller, callees) = foldl (\cg, callee => case lookup callee cg of
        Nothing => insert callee (singleton caller) cg
        Just callers => insert callee (insert caller callers) cg) cg0 callees

export
showCallGraph : Show name => CallGraph name -> String
showCallGraph cg = fastConcat $ showCalls <$> toList cg
  where
    showCalls : (name, SortedSet name) -> String
    showCalls (fn, fns) = fastConcat [show fn, ": ", show $ Set.toList fns, "\n"]


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

import XML.DOM

import Edda
import Edda.Writer.Org
import Edda.Writer.LaTeX
import Edda.Writer.CommonMark

import Freyja
import Freyja.Convert.XML
import Freyja.Convert.Edda

%access public export

data FreyjaOutFormat = ORG | LATEX | CMARK | XML | EDDA

implementation Eq FreyjaOutFormat where
  (==) LATEX   LATEX   = True
  (==) CMARK   CMARK   = True
  (==) ORG     ORG     = True
  (==) XML     XML     = True
  (==) EDDA    EDDA    = True
  (==) _       _       = False

implementation Show FreyjaOutFormat where
  show LATEX = "LaTeX"
  show CMARK = "CommonMark"
  show ORG   = "Org"
  show XML   = "XML"
  show EDDA  = "EDDA"

export
readOutFMT : String -> Maybe FreyjaOutFormat
readOutFMT s =
  case toLower s of
    "latex"    => Just LATEX
    "markdown" => Just CMARK
    "org"      => Just ORG
    "xml"      => Just XML
    otherwise  => Nothing

export
convTy : FreyjaOutFormat -> Type
convTy LATEX   = String
convTy CMARK   = String
convTy ORG     = String
convTy XML     = XMLDoc
convTy EDDA    = EddaDoc

export
convTo : (fmt : FreyjaOutFormat) -> PatternDoc-> (convTy fmt)
convTo XML   p = toXML p
convTo EDDA  p = toEdda p
convTo ORG   p = org $ toEdda p
convTo LATEX p = latex $ toEdda p
convTo CMARK p = markdown $ toEdda p

covering
export
convShow : FreyjaOutFormat -> PatternDoc -> Maybe String
convShow XML   p = Just (show @{xml} (convTo XML p))
convShow ORG   p = Just ((convTo ORG p))
convShow CMARK p = Just ((convTo CMARK p))
convShow LATEX p = Just ((convTo LATEX p))
convShow _     _ = Nothing

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

max_stars_repo_name: jfdm/freyja-schema

max_issues_repo_name: jfdm/freyja-schema

max_forks_repo_name: jfdm/freyja-schema


text:
module System.File.Meta

import System.File.Handle
import System.File.Support
import public System.File.Types
import System.FFI

%default total

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

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

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

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

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

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

%foreign support "idris2_fileIsTTY"
         "node:lambda:fp=>Number(require('tty').isatty(fp.fd))"
prim__fileIsTTY : FilePtr -> PrimIO Int

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

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

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

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

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

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

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

||| Check whether the given File is a terminal device.
export
isTTY : HasIO io => (h : File) -> io Bool
isTTY (FHandle f) = (/= 0) <$> primIO (prim__fileIsTTY f)


text:
module Web.Dom

import JS
import public Web.Internal.Types
import public Web.Raw.Dom as Dom

%default total

--------------------------------------------------------------------------------
--          Main entry points
--------------------------------------------------------------------------------

%foreign "browser:lambda:()=>window"
prim__window : PrimIO Window

%foreign "browser:lambda:()=>document"
prim__document : PrimIO Document

export
window : JSIO Window
window = primJS prim__window

export
document : JSIO Document
document = primJS prim__document

export
body : JSIO HTMLElement
body = unMaybe "Web.Dom.body" $ document >>= to body

--------------------------------------------------------------------------------
--          Aliases
--------------------------------------------------------------------------------

namespace Alias
  public export
  Anchor : Type
  Anchor = HTMLAnchorElement

  public export
  Area : Type
  Area = HTMLAreaElement

  public export
  Audio : Type
  Audio = HTMLAudioElement

  public export
  BR : Type
  BR = HTMLBRElement

  public export
  Base : Type
  Base = HTMLBaseElement

  public export
  Body : Type
  Body = HTMLBodyElement

  public export
  Button : Type
  Button = HTMLButtonElement

  public export
  Canvas : Type
  Canvas = HTMLCanvasElement

  public export
  DList : Type
  DList = HTMLDListElement

  public export
  Data : Type
  Data = HTMLDataElement

  public export
  DataList : Type
  DataList = HTMLDataListElement

  public export
  Details : Type
  Details = HTMLDetailsElement

  public export
  Dialog : Type
  Dialog = HTMLDialogElement

  public export
  Div : Type
  Div = HTMLDivElement

  public export
  Embed : Type
  Embed = HTMLEmbedElement

  public export
  FieldSet : Type
  FieldSet = HTMLFieldSetElement

  public export
  Form : Type
  Form = HTMLFormElement

  public export
  HR : Type
  HR = HTMLHRElement

  public export
  Heading : Type
  Heading = HTMLHeadingElement

  public export
  Html : Type
  Html = HTMLHtmlElement

  public export
  IFrame : Type
  IFrame = HTMLIFrameElement

  public export
  Image : Type
  Image = HTMLImageElement

  public export
  Input : Type
  Input = HTMLInputElement

  public export
  LI : Type
  LI = HTMLLIElement

  public export
  Label : Type
  Label = HTMLLabelElement

  public export
  Legend : Type
  Legend = HTMLLegendElement

  public export
  Link : Type
  Link = HTMLLinkElement

  public export
  Map : Type
  Map = HTMLMapElement

  public export
  Menu : Type
  Menu = HTMLMenuElement

  public export
  Meta : Type
  Meta = HTMLMetaElement

  public export
  Meter : Type
  Meter = HTMLMeterElement

  public export
  Mod : Type
  Mod = HTMLModElement

  public export
  OList : Type
  OList = HTMLOListElement

  public export
  Object : Type
  Object = HTMLObjectElement

  public export
  OptGroup : Type
  OptGroup = HTMLOptGroupElement

  public export
  Option : Type
  Option = HTMLOptionElement

  public export
  Output : Type
  Output = HTMLOutputElement

  public export
  Paragraph : Type
  Paragraph = HTMLParagraphElement

  public export
  Param : Type
  Param = HTMLParamElement

  public export
  Picture : Type
  Picture = HTMLPictureElement

  public export
  Pre : Type
  Pre = HTMLPreElement

  public export
  Progress : Type
  Progress = HTMLProgressElement

  public export
  Quote : Type
  Quote = HTMLQuoteElement

  public export
  Script : Type
  Script = HTMLScriptElement

  public export
  Select : Type
  Select = HTMLSelectElement

  public export
  Slot : Type
  Slot = HTMLSlotElement

  public export
  Source : Type
  Source = HTMLSourceElement

  public export
  Span : Type
  Span = HTMLSpanElement

  public export
  Style : Type
  Style = HTMLStyleElement

  public export
  TableCaption : Type
  TableCaption = HTMLTableCaptionElement

  public export
  TableCell : Type
  TableCell = HTMLTableCellElement

  public export
  TableCol : Type
  TableCol = HTMLTableColElement

  public export
  Table : Type
  Table = HTMLTableElement

  public export
  TableRow : Type
  TableRow = HTMLTableRowElement

  public export
  TableSection : Type
  TableSection = HTMLTableSectionElement

  public export
  Template : Type
  Template = HTMLTemplateElement

  public export
  TextArea : Type
  TextArea = HTMLTextAreaElement

  public export
  Time : Type
  Time = HTMLTimeElement

  public export
  Title : Type
  Title = HTMLTitleElement

  public export
  Track : Type
  Track = HTMLTrackElement

  public export
  UList : Type
  UList = HTMLUListElement

  public export
  Video : Type
  Video = HTMLVideoElement

--------------------------------------------------------------------------------
--          Elements
--------------------------------------------------------------------------------

||| HTML Element Tags.
|||
||| This is mainly to be used with `Web.Dom.createElement` and `newElement`.
||| Some deprecated tags have been left out, some others might
||| still be missing.
public export
data ElementType : (tag : String) -> (htmlElement : Type) -> Type where
  A          : ElementType "a" Anchor
  Area       : ElementType "area" Area
  Audio      : ElementType "audio" Audio
  Base       : ElementType "base" Base
  Blockquote : ElementType "blockquote" Quote
  Body       : ElementType "body" Alias.Body
  Br         : ElementType "br" BR
  Button     : ElementType "button" Button
  Canvas     : ElementType "canvas" Canvas
  Caption    : ElementType "caption" TableCaption
  Col        : ElementType "col" TableCol
  Colgroup   : ElementType "colgroup" TableCol
  Data       : ElementType "data" Data
  Datalist   : ElementType "datalist" DataList
  Del        : ElementType "del" Mod
  Details    : ElementType "details" Details
  Dialog     : ElementType "dialog" Dialog
  Div        : ElementType "div" Div
  Dl         : ElementType "dl" DList
  Embed      : ElementType "embed" Embed
  FieldSet   : ElementType "fieldset" FieldSet
  Form       : ElementType "form" Form
  H1         : ElementType "h1" Heading
  H2         : ElementType "h2" Heading
  H3         : ElementType "h3" Heading
  H4         : ElementType "h4" Heading
  H5         : ElementType "h5" Heading
  H6         : ElementType "h6" Heading
  HR         : ElementType "hr" HR
  Html       : ElementType "html" Html
  IFrame     : ElementType "iframe" IFrame
  Img        : ElementType "img" Image
  Input      : ElementType "input" Input
  Ins        : ElementType "ins" Mod
  Label      : ElementType "label" Label
  Legend     : ElementType "legend" Legend
  Li         : ElementType "li" LI
  Link       : ElementType "link" Link
  Map        : ElementType "map" Map
  Menu       : ElementType "menu" Menu
  Meta       : ElementType "meta" Meta
  Meter      : ElementType "meter" Meter
  Object     : ElementType "object" Alias.Object
  Ol         : ElementType "ol" OList
  OptGroup   : ElementType "optgroup" OptGroup
  Option     : ElementType "option" Option
  Output     : ElementType "output" Output
  P          : ElementType "p" Paragraph
  Param      : ElementType "param" Param
  Picture    : ElementType "picture" Picture
  Pre        : ElementType "pre" Pre
  Progress   : ElementType "progress" Progress
  Q          : ElementType "q" Quote
  Script     : ElementType "script" Script
  Select     : ElementType "Select" Select
  Slot       : ElementType "slot" Slot
  Source     : ElementType "source" Source
  Span       : ElementType "span" Span
  Style      : ElementType "style" Style
  Table      : ElementType "table" Table
  Tbody      : ElementType "tbody" TableSection
  Td         : ElementType "td" TableCell
  Template   : ElementType "template" Template
  TextArea   : ElementType "textarea" TextArea
  Tfoot      : ElementType "tfoot" TableSection
  Th         : ElementType "th" TableCell
  Thead      : ElementType "thead" TableSection
  Time       : ElementType "time" Time
  Title      : ElementType "title" Title
  Tr         : ElementType "tr" TableRow
  Track      : ElementType "track" Track
  Ul         : ElementType "ul" UList
  Video      : ElementType "video" Video

||| Extracts the `tag` String from a known `ElementType`.
public export
elementTag : {tag : _} -> (0 _ : ElementType tag t) -> String
elementTag _ = tag

||| Proof, that each element type has an instance of `SafeCast`.
export
elemCast :  (0 f : Type -> Type)
         -> ({0 a : Type} -> SafeCast a => f a)
         -> (e : ElementType s t)
         -> f t
elemCast _ fun A          = fun
elemCast _ fun Area       = fun
elemCast _ fun Audio      = fun
elemCast _ fun Base       = fun
elemCast _ fun Blockquote = fun
elemCast _ fun Body       = fun
elemCast _ fun Br         = fun
elemCast _ fun Button     = fun
elemCast _ fun Canvas     = fun
elemCast _ fun Caption    = fun
elemCast _ fun Col        = fun
elemCast _ fun Colgroup   = fun
elemCast _ fun Data       = fun
elemCast _ fun Datalist   = fun
elemCast _ fun Del        = fun
elemCast _ fun Details    = fun
elemCast _ fun Dialog     = fun
elemCast _ fun Div        = fun
elemCast _ fun Dl         = fun
elemCast _ fun Embed      = fun
elemCast _ fun FieldSet   = fun
elemCast _ fun Form       = fun
elemCast _ fun H1         = fun
elemCast _ fun H2         = fun
elemCast _ fun H3         = fun
elemCast _ fun H4         = fun
elemCast _ fun H5         = fun
elemCast _ fun H6         = fun
elemCast _ fun HR         = fun
elemCast _ fun Html       = fun
elemCast _ fun IFrame     = fun
elemCast _ fun Img        = fun
elemCast _ fun Input      = fun
elemCast _ fun Ins        = fun
elemCast _ fun Label      = fun
elemCast _ fun Legend     = fun
elemCast _ fun Li         = fun
elemCast _ fun Link       = fun
elemCast _ fun Map        = fun
elemCast _ fun Menu       = fun
elemCast _ fun Meta       = fun
elemCast _ fun Meter      = fun
elemCast _ fun Object     = fun
elemCast _ fun Ol         = fun
elemCast _ fun OptGroup   = fun
elemCast _ fun Option     = fun
elemCast _ fun Output     = fun
elemCast _ fun P          = fun
elemCast _ fun Param      = fun
elemCast _ fun Picture    = fun
elemCast _ fun Pre        = fun
elemCast _ fun Progress   = fun
elemCast _ fun Q          = fun
elemCast _ fun Script     = fun
elemCast _ fun Select     = fun
elemCast _ fun Slot       = fun
elemCast _ fun Source     = fun
elemCast _ fun Span       = fun
elemCast _ fun Style      = fun
elemCast _ fun Table      = fun
elemCast _ fun Tbody      = fun
elemCast _ fun Td         = fun
elemCast _ fun Template   = fun
elemCast _ fun TextArea   = fun
elemCast _ fun Tfoot      = fun
elemCast _ fun Th         = fun
elemCast _ fun Thead      = fun
elemCast _ fun Time       = fun
elemCast _ fun Title      = fun
elemCast _ fun Tr         = fun
elemCast _ fun Track      = fun
elemCast _ fun Ul         = fun
elemCast _ fun Video      = fun

||| Creates a new element using the given `ElementType`'s `tag`
||| and casting the result to the corresponding HTML element type.
||| See also `newElement`.
export
createElement : {tag : _} -> (e : ElementType tag t) -> JSIO t
createElement e =
   elemCast JSIO ( castingTo #"JS.Dom.createElement [\#{tag}]"# $
                   document >>= (`createElement'` tag)) e

||| Like `createElement` but applies the given set of
||| modifiers. This is especially useful for setting an element's
||| attributes.
export
newElement :  {tag : _}
           -> (e : ElementType tag t)
           -> (mods : List (t -> JSIO ()))
           -> JSIO t
newElement e mods = do res <- createElement e
                       for_ mods $ \m => m res
                       pure res

--------------------------------------------------------------------------------
--          Finding Elements
--------------------------------------------------------------------------------

export
getElementById : String -> JSIO (Maybe Element)
getElementById s = getElementById !document s

export
castElementById_ : SafeCast a => String -> JSIO (Maybe a)
castElementById_ = map (>>= safeCast) . getElementById

export
castElementById : (0 a : Type) -> SafeCast a => String -> JSIO (Maybe a)
castElementById _ = castElementById_

export
htmlElementById : ElementType tag a -> String -> JSIO (Maybe a)
htmlElementById e s = elemCast (JSIO . Maybe) (castElementById_ s) e

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

export
ArrayLike NodeList Node where

export
ArrayLike DOMTokenList String where

export
Callback EventListener (Event -> JSIO ()) where
  callback f = toEventListener (runJS . f)

export
Callback MutationCallback (  Array MutationRecord
                          -> MutationObserver
                          -> JSIO () ) where
  callback f = toMutationCallback $ \a,m => runJS (f a m)

||| In case of an error, the error is logged to the console and
||| the node is rejected
export
Callback NodeFilter (Node -> JSIO Bits16) where
  callback f = toNodeFilter (runJSWithDefault FILTER_REJECT . f)

export
Callback XPathNSResolver (Maybe String -> JSIO (Maybe String) ) where
  callback f = toXPathNSResolver $ map maybeToNullable
                                 . runJSWithDefault Nothing
                                 . f
                                 . nullableToMaybe


text:
> module Main

> import Data.List

> import EscardoOliva.SelectionFunction
> import EscardoOliva.Quantifier
> import EscardoOliva.Operations

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

> data Player =  X | O

> Outcome : Type
> Outcome = Int

> Move : Type
> Move = Int

> Board : Type
> Board = (List Move, List Move)

> contained : {X : Type} -> Ord X => List X -> List X -> Bool
> contained       []        ys  = True
> contained       xs        []  = False
> contained (x :: xs) (y :: ys) = if x == y
>                                 then contained xs ys
>                                 else if x >= y
>                                      then contained (x :: xs) ys
>                                      else False

> someContained : {X : Type} -> Ord X =>
>                 List (List X) -> List X -> Bool
> someContained         []  ys  = False
> someContained        xss  []  = False
> someContained (xs :: xss) ys = contained xs ys || someContained xss ys

> wins : List Move -> Bool
> wins = someContained [[0,1,2],[3,4,5],[6,7,8],
>                       [0,3,6],[1,4,7],[2,5,8],
>                       [0,4,8],[2,4,6]]

> value : Board -> Outcome
> value (xs, os) = if wins xs
>                  then 1
>                  else if wins os
>                       then -1
>                       else 0

> insert : {X : Type} -> Ord X => X -> List X -> List X
> insert x [] = [x]
> insert x (y :: ys) = if x == y
>                      then (y :: ys)
>                      else if x < y
>                           then x :: (y :: ys)
>                           else y :: (insert x ys)

> outcome : Player -> List Move -> Board -> Board
> outcome _      Nil     board = board
> outcome X (m :: ms) (xs, os) = if wins os
>                                then (xs, os)
>                                else outcome O ms (insert m xs, os)
> outcome O (m :: ms) (xs, os) = if wins xs
>                                then (xs, os)
>                                else outcome X ms (xs, insert m os)

> delete : {X : Type} -> Ord X => X -> List X -> List X
> delete x [] = []
> delete x (y :: ys) = if x == y
>                      then ys
>                      else if x < y
>                           then y :: ys
>                           else y :: Main.delete x ys

> setMinus : {X : Type} -> Ord X =>
>            List X -> List X -> List X
> setMinus xs       []  = xs
> setMinus xs (y :: ys) = setMinus (Main.delete y xs) ys

> partial
> epsilons : List (List Move -> J Outcome Move)
> epsilons = take 3 all where
>   partial
>   eX  :  List Move -> J Outcome Move
>   eX  =  \ h => argsup (setMinus [0..8] h)
>   partial
>   eO  :  List Move -> J Outcome Move
>   eO  =  \ h => arginf (setMinus [0..8] h)
>   partial
>   all :  List (List Move -> J Outcome Move)
>   all =  [eX, eO, eX, eO, eX, eO, eX, eO, eX, eO]

> p : List Move -> Outcome
> p ms = value (outcome X ms (Nil, Nil))

> partial
> optimalPlay : List Move
> optimalPlay = bigotimes epsilons p

> partial
> optimalOutcome : Outcome
> optimalOutcome = p optimalPlay

> partial
> main : IO ()
> main =
>   do putStr ("An optimal play for Tic-Tac-Toe is "
>              ++
>              show optimalPlay ++ "\n"
>              ++
>              "and the optimal outcome is "
>              ++
>              show optimalOutcome ++ "\n"
>              )

> {-

> ---}


text:
module Toolkit.Data.DVect.Elem

import Data.Vect

import Toolkit.Data.DVect

import public Toolkit.Decidable.Equality.Indexed

%default total

public export
data Elem : (iTy : Type)
         -> (elemTy : iTy -> Type)
         -> forall i, is
          . (e : elemTy i)
         -> (es : DVect iTy elemTy l is)
         -> Type
  where
    H : Elem iTy eTy x (y::xs)
    T : (later : Elem iTy eTy x      xs)
             ->  Elem iTy eTy x (x'::xs)

-- [ EOF ]


text:
module Main

import Json

test : String -> IO ()
test s = case parse jsonToplevelValue s of
  Left err => putStrLn $ "error: " ++ err
  Right v  => printLn v

main : IO ()
main = do
  test "[1,2,4,[5,6],null,{\"some\":[\"object\"]},false]"
  test "{\n  \"hallo\":42,\"nichts\":null}"
  test "{{\n  \"hallo\":42,\"nichts\":null}"
  test "{\"hello\": [{\"world\": false}, 3, \"string\", true, null]}"

max_stars_repo_name: david-christiansen/lightyear

max_issues_repo_name: david-christiansen/lightyear

max_forks_repo_name: david-christiansen/lightyear


text:
||| This module can be used to run an SF for a long time
||| as quickly as possible to check for memory leaks.
module Test.Leak

import Control.ANSI.CSI
import Control.Monad.Identity
import Control.Monad.Reader
import Control.MonadRec
import Data.Fuel
import Data.Iterable
import Data.MSF
import Data.MSF.Running
import Data.MSF.Switch
import Data.MSF.Trans
import Data.String

%default total

--------------------------------------------------------------------------------
--          Some FRP primitives
--------------------------------------------------------------------------------

DTime : Type
DTime = Double

SF : Type -> Type -> Type
SF = MSF (ReaderT DTime Identity)

Velocity : Type
Velocity = Double

Acceleration : Type
Acceleration = Double

integralFrom : (v0 : Double) -> SF Double Double
integralFrom v0 = fan [id, iPre v0, ask] >>> accumulateWith next 0
  where next : NP I [Double,Double,DTime] -> Double -> Double
        next [new,old,dt] acc = acc + (dt / 2 * (new + old))

acc : Acceleration
acc = -9.81

velocity : (v0 : Velocity) -> (a0 : Acceleration) -> SF Acceleration Velocity
velocity v0 a0 = integralFrom a0 >>^ (+ v0)

position : (p0 : Double) -> (v0 : Velocity) -> SF Velocity Double
position p0 v0 = integralFrom v0 >>^ (+ p0)

--------------------------------------------------------------------------------
--          Bouncing Ball
--------------------------------------------------------------------------------

record Ball where
  constructor MkBall
  pos : Double
  vel : Velocity

dispBall : NP I [Ball,Nat] -> String
dispBall [b,n] =
  let char = if b.vel <= 0 then '<' else '>'
   in    cursorUp1
      ++ eraseLine End
      ++ padLeft 9 ' ' (show n)
      ++ "  "
      ++ replicate (cast b.pos) char

ballFrom : Ball -> SF i Ball
ballFrom (MkBall p0 v0) =
      const acc
  >>> velocity v0 acc
  >>> fan [position p0 v0, id]
  >>^ \[p,v] => MkBall p v

bounce : Ball -> Event (SF i Ball)
bounce (MkBall y vy) =
  if y <= 0 then Ev . ballFrom $ MkBall y (-vy) else NoEv

ballGame : Ball -> SF i Ball
ballGame b0 = feedback NoEv $ rSwitch (ballFrom b0) >>> fan [arr bounce, id]

game : MSF Identity () Ball
game = const 0.0001 >>> fromReader_ (ballGame $ MkBall 80 0)

controller : MSF IO () ()
controller = morph (pure . runIdentity) (fan [game,count]) >>! putStrLn . dispBall

run : Fuel -> IO ()
run f = iterM (\_,sf => snd <$> step sf ()) (const ()) controller f

||| This uses monad morphisms and recursive switches under the hood,
||| which were problematic in earlier implementations. Hence this test
||| that they behave correctly over a prolonged period of time.
partial
main : IO ()
main = run (limit 10000000)


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

max_stars_repo_name: jeremy-miller/type-driven-development

max_issues_repo_name: jeremy-miller/type-driven-development

max_forks_repo_name: jeremy-miller/type-driven-development


text:
module Main

import IR
import IR.Event
import IR.Layout
import IR.Lens
import IR.StackSet

%flag C "-framework Cocoa"
%include C "cbits/quartz.h"
%link C "src/quartz.o"
%include C "cbits/ir.h"
%link C "src/ir.o"

%default total

partial
putErrLn : String -> IO ()
putErrLn s = fwrite stderr (s ++ "\n")

quartzInit : IO Bool
quartzInit = map (/= 0) (mkForeign (FFun "quartzInit" [] FInt))

quartzSpacesCount : IO Int
quartzSpacesCount = mkForeign (FFun "quartzSpacesCount" [] FInt)

QuartzWindow : Type
QuartzWindow = Int

QuartzSpace : Type
QuartzSpace = Int

QuartzState : Type
QuartzState = IRState QuartzWindow QuartzSpace

QUARTZ : EFFECT
QUARTZ = IR QuartzWindow QuartzSpace

quartzGetWindows : IO (List QuartzWindow, QuartzWindow)
quartzGetWindows = do
  p <- mkForeign (FFun "quartzWindows" [] FPtr)
  l <- mkForeign (FFun "quartzWindowsLength" [FPtr] FInt) p
  wids <- traverse (\a => mkForeign (FFun "quartzWindowId" [FPtr, FInt] FInt) p a) [0..l-1]
  focused <- mkForeign (FFun "quartzWindowsFocusedId" [FPtr] FInt) p
  mkForeign (FFun "quartzWindowsFree" [FPtr] FUnit) p
  return (wids, focused)

quartzTileWindow : QuartzWindow -> Rectangle -> IO ()
quartzTileWindow wid r =
  mkForeign (FFun "quartzWindowSetRect" [FInt, FFloat, FFloat, FFloat, FFloat] FUnit) wid (rectX r) (rectY r) (rectW r) (rectH r)

quartzFocusWindow : QuartzWindow -> IO ()
quartzFocusWindow wid =
  mkForeign (FFun "quartzWindowSetFocus" [FInt] FUnit) wid

quartzRefresh : QuartzState -> IO QuartzState
quartzRefresh s = do
  (wids, focused) <- quartzGetWindows
  let stack = workspaceStack' . screenWorkspace' . stackSetCurrent' . irStateStackSet' ^$ s
  let wids' = fromMaybe [] (map (\s => toList (integrate s)) stack)
  let deleted = wids' \\ wids
  let inserted = wids \\ wids'
  return (irStateStackSet' ^%= (\ss => focusWindow focused (foldr insertUp (foldr delete ss deleted) inserted)) $ s)

quartzGetFrame : Ptr -> Int -> IO Rectangle
quartzGetFrame p i = do
  r <- mkForeign (FFun "quartzScreensFrame" [FPtr, FInt] FPtr) p i
  x <- mkForeign (FFun "irFrameX" [FPtr] FFloat) r
  y <- mkForeign (FFun "irFrameY" [FPtr] FFloat) r
  w <- mkForeign (FFun "irFrameW" [FPtr] FFloat) r
  h <- mkForeign (FFun "irFrameH" [FPtr] FFloat) r
  return (MkRectangle x y w h)

quartzGetFrames : IO (n ** Vect (S n) Rectangle)
quartzGetFrames = do
  p <- mkForeign (FFun "quartzScreens" [] FPtr)
  l <- mkForeign (FFun "quartzScreensLength" [FPtr] FInt) p
  mainFrame <- quartzGetFrame p 0
  frames <- traverse (quartzGetFrame p) [1..l-1]
  mkForeign (FFun "quartzScreensFree" [FPtr] FUnit) p
  return (length frames ** mainFrame :: fromList frames)

quartzGrabKeys : List Key -> IO ()
quartzGrabKeys keys =
  let grabKey = \key => do
        let c = keyCode' ^$ key
        let f = \b => if b then 1 else 0
        let alt = f $ keyHasAlt' ^$ key
        let cmd = f $ keyHasCmd' ^$ key
        let ctrl = f $ keyHasCtrl' ^$ key
        let shift = f $ keyHasShift' ^$ key
        mkForeign (FFun "quartzGrabKey" [FInt, FInt, FInt, FInt, FInt] FUnit) c alt cmd ctrl shift
  in traverse_ grabKey keys

instance Handler (IREffect QuartzWindow QuartzSpace) IO where
  handle () GetEvent k = do
    p <- mkForeign (FFun "quartzEvent" [] FPtr)
    e <- eventFromPtr p
    k e ()
  handle () (GrabKeys keys) k = do
    quartzGrabKeys keys
    k () ()
  handle () (RefreshState s) k = do
    s' <- quartzRefresh s
    k s' ()
  handle () (TileWindow wid r) k = do
    quartzTileWindow wid r
    k () ()
  handle () (SetFocus wid) k = do
    quartzFocusWindow wid
    k () ()
  handle () GetWindows k = do
    (wids, _) <- quartzGetWindows
    k wids ()
  handle () GetFrames k = do
    f <- quartzGetFrames
    k f ()

initialQuartzState : IO (IRState QuartzWindow QuartzSpace)
initialQuartzState = do
  (_ ** frame :: _) <- quartzGetFrames
  (wids, _) <- quartzGetWindows
  let workspace : Workspace QuartzWindow = foldr manage (MkWorkspace (choose [columnLayout, mirrorLayout columnLayout, fullLayout]) Nothing) wids
  return (MkIRState (MkStackSet (MkScreen workspace 0 frame) [] []))

quartzConf : IRConf QuartzWindow QuartzSpace
quartzConf =
  MkIRConf (fromList [
    (MkKey 49 True True False False, update nextLayout >>= \_ => refresh)
  , (MkKey 38 True True False False, windows focusDown)
  , (MkKey 40 True True False False, windows focusUp)
  , (MkKey 38 True True False True, windows swapDown)
  , (MkKey 40 True True False True, windows swapUp)
  ])

partial
main : IO ()
main = do
  putStrLn "iridium started"
  a <- quartzInit
  if not a
  then do
    putErrLn "iridium doesn't have Accessibility permission."
    putErrLn "You can enable this under Privacy in Security & Privacy in System Preferences."
  else runInit [(), !initialQuartzState, quartzConf] runIR

max_stars_repo_name: victoredwardocallaghan/iridium

max_issues_repo_name: victoredwardocallaghan/iridium

max_forks_repo_name: victoredwardocallaghan/iridium


text:
-- This ought to go into base at some future point
module Libraries.Data.Span

public export
record Span (a : Type) where
  constructor MkSpan
  start    : Nat
  length   : Nat
  property : a

export
Functor Span where
  map f = { property $= f }

export
Foldable Span where
  foldr c n span = c span.property n

export
Traversable Span where
  traverse f (MkSpan start width prop)
    = MkSpan start width <$> f prop

export
Show a => Show (Span a) where
  show (MkSpan start width prop)
    = concat {t = List} [ "[", show start, "-", show width, "]"
                        , show prop
                        ]


text:
module Hamming

import Data.Vect

public export
data Nucleotide = A | C | G | T

public export
implementation Eq Nucleotide where
  A == A = True
  C == C = True
  G == G = True
  T == T = True
  _ == _ = False

export
hamming_distance : Eq a => Vect n a -> Vect n a -> Nat
hamming_distance s1 s2 =
  fst $ filter ((/=) 0) $ map (\(n1,n2) => if n1 == n2 then 0 else 1) $ zip s1 s2

export
version : String
version = "1.0.0"


text:
module Flexidisc.Record

import Control.Monad.Identity

import        Flexidisc.RecordContent

import public Flexidisc.Dec.IsYes
import public Flexidisc.Header
import public Flexidisc.Record.Type
import public Flexidisc.Record.Read
import public Flexidisc.Record.Update
import public Flexidisc.TaggedValue
import public Flexidisc.THList

%default total
%access export

||| Append two records, it fails if some fields are duplicated
|||
||| Complexity is _O(n)_ where _n_ is the length of the longest record.
|||
merge : (xs : RecordM m k header) -> (ys : RecordM m k header') ->
        {auto prf : Disjoint header header'} ->
        RecordM m k (merge header header')
merge (Rec xs nubX) (Rec ys nubY) {prf = D prf} =
  Rec (merge xs ys) (disjointNub prf nubX nubY)

||| Alias for `merge`
(++) : (xs : RecordM m k header) -> (ys : RecordM m k header') ->
       {auto prf : Disjoint header header'} ->
       RecordM m k (merge header header')
(++) = merge

||| Patch the right-hand side record with the values on the left-hand side
(|>) : DecEq k =>
       (xs : RecordM m k header) -> (ys : RecordM m k header') ->
       {default (S Same) prf : SameOrd header header'} ->
        RecordM m k (patch header header')
(|>) (Rec xs nubX) (Rec ys nubY) {prf = S prf} = let
  nubProof = disjointNub diffIsDisjoint (isNubFromSub diffIsSub nubY) nubX
  in Rec (xs |> ys) nubProof

-- DELETE

||| Remove a row from a Record.
|||
||| Complexity is _O(n)_
|||
||| @ xs the record
||| @ loc  the proof that the row is in it
dropByLabel : (xs : RecordM m k header) -> (loc : Label query header) ->
              RecordM m k (dropLabel header loc)
dropByLabel (Rec xs nub) (L prf) =
  Rec (drop xs prf) (dropPreservesNub nub prf)

||| Remove a row from a Record.
|||
||| Complexity is _O(n)_
|||
||| @ query  the row name
||| @ xs     the record
||| @ loc    the proof that the row is in it
drop : (query : k) -> (xs : RecordM m k header) ->
       {auto loc : Label query header} ->
       RecordM m k (dropLabel header loc)
drop _ xs {loc} = dropByLabel xs loc

-- TRANSFORM

||| Project a record (keep only a subset of its field and reorder them.
|||
||| Complexity is _O(n)_
|||
project : RecordM m k header -> {auto prf : Sub sub header} -> RecordM m k sub
project (Rec xs nub) {prf = S prf} = Rec (project xs prf) (isNubFromSub prf nub)

||| Build a projection with the given keys
|||
||| @keys The rows to keep
||| @xs The record to project
||| @prf Proof that the rows are parts of the record
keep : (keys : List k) -> (xs : RecordM m k pre) ->
       {auto prf : SubWithKeys keys post pre} ->
       RecordM m k post
keep keys (Rec xs nub) {prf = S prf} =
  Rec (keep xs prf) (isNubFromSub (toSub prf) nub)

||| Build a projection that excludes the given keys
|||
||| @keys The rows to skip
||| @xs The record to project
||| @prf Proof that the rows are parts of the record
discard : (keys : List k) -> (xs : RecordM m k pre) ->
          {auto prf : CompWithKeys keys post pre} ->
          RecordM m k post
discard keys (Rec xs nub) {prf = S prf} =
  Rec (discard xs prf) (isNubFromSub (toSub prf) nub)

decLabel : DecEq k => (l : k) -> (xs : RecordM m k header) -> Dec (Label l header)
decLabel l _ {header} = decLabel l header

toTHList : RecordM m k header -> THList m k (toList header)
toTHList (Rec xs _) = toTHList xs

-- COMPARE

implementation
Eq (THList m k (toList header)) => Eq (RecordM m k header) where
  (==) xs ys = toTHList xs == toTHList ys
  (/=) xs ys = toTHList xs /= toTHList ys

-- SHOW

implementation
Show (THList m k (toList header)) => Show (RecordM m k header) where
  show xs = show (toTHList xs)

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module Algebra.Solver.Ring.Expr

import public Data.List.Elem
import public Algebra.Ring
import Syntax.PreorderReasoning

%default total

--------------------------------------------------------------------------------
--          Natural Numbers
--------------------------------------------------------------------------------

||| Multiplies a value `n` times with itself. In case of `n`
||| being zero, this returns `1`.
public export
pow : Ring a => a -> Nat -> a
pow x 0     = 1
pow x (S k) = x * pow x k

--------------------------------------------------------------------------------
--          Expression
--------------------------------------------------------------------------------

||| Data type representing expressions in a commutative ring.
|||
||| This is used to at compile time compare different forms of
||| the same expression and proof that they evaluate to
||| the same result.
|||
||| An example:
|||
||| ```idris example
||| 0 binom1 : {x,y : Bits8} -> (x + y) * (x + y) === x * x + 2 * x * y + y * y
||| binom1 = solve [x,y]
|||                ((x .+. y) * (x .+. y))
|||                (x .*. x + 2 *. x *. y + y .*. y)
||| ```
|||
||| @ a  the type used in the arithmetic expression
||| @ as list of variables which don't reduce at compile time
|||
||| In the example above, `x` and `y` are variables, while `2`
||| is a literal known at compile time. To make working with
||| variables more convenient (the have to be wrapped in data
||| constructor `Var`, by using function `var` for instance),
||| additional operators for addition, multiplication, and
||| subtraction are provided.
|||
||| In order to proof that two expressions evaluate to the
||| same results, the following steps are taken at compile
||| time:
|||
||| 1. Both expressions are converted to a normal form via
|||    `Algebra.Solver.Ring.Sum.normalize`.
||| 2. The normal forms are compared for being identical.
||| 3. Since in `Algebra.Solver.Ring.Sum` there is a proof that
|||    converting an expression to its normal form does not
|||    affect the result when evaluating it, if the normal
|||    forms are identical, the two expressions must evaluate
|||    to the same result.
|||
||| You can find several examples of making use of this
||| in `Data.Prim.Integer.Extra`.
public export
data Expr : (a : Type) -> (as : List a) -> Type where
  ||| A literal. This should be a value known at compile time
  ||| so that it reduces during normalization.
  Lit   : (v : a) -> Expr a as

  ||| A variabl. This is is for values not known at compile
  ||| time. In order to compare and merge variables, we need an
  ||| `Elem x as` proof.
  Var   : (x : a) -> Elem x as -> Expr a as

  ||| Negates and expression.
  Neg   : Expr a as -> Expr a as

  ||| Addition of two expressions.
  Plus  : (x,y : Expr a as) -> Expr a as

  ||| Multiplication of two expressions.
  Mult  : (x,y : Expr a as) -> Expr a as

  ||| Subtraction of two expressions.
  Minus : (x,y : Expr a as) -> Expr a as

||| While this allows you to use the usual operators
||| for addition and multiplication, it is often convenient
||| to use related operators `.*.`, `.+.`, and similar when
||| working with variables.
public export
Num a => Num (Expr a as) where
  (+) = Plus
  (*) = Mult
  fromInteger = Lit . fromInteger

public export
Neg a => Neg (Expr a as) where
  negate = Neg
  (-)    = Minus

||| Like `Var` but takes the `Elem x as` as an auto implicit
||| argument.
public export
var : {0 as : List a} -> (x : a) -> Elem x as => Expr a as
var x = Var x %search

--------------------------------------------------------------------------------
--          Syntax
--------------------------------------------------------------------------------

infixl 8 .+., .+, +.

infixl 8 .-., .-, -.

infixl 9 .*., .*, *.

||| Addition of variables. This is an alias for
||| `var x + var y`.
public export
(.+.) :  {0 as : List a}
      -> (x,y : a)
      -> Elem x as
      => Elem y as
      => Expr a as
(.+.) x y = Plus (var x) (var y)

||| Addition of variables. This is an alias for
||| `x + var y`.
public export
(+.) :  {0 as : List a}
     -> (x : Expr a as)
     -> (y : a)
     -> Elem y as
     => Expr a as
(+.) x y = Plus x (var y)

||| Addition of variables. This is an alias for
||| `var x + y`.
public export
(.+) :  {0 as : List a}
     -> (x : a)
     -> (y : Expr a as)
     -> Elem x as
     => Expr a as
(.+) x y = Plus (var x) y

||| Subtraction of variables. This is an alias for
||| `var x - var y`.
public export
(.-.) :  {0 as : List a}
      -> (x,y : a)
      -> Elem x as
      => Elem y as
      => Expr a as
(.-.) x y = Minus (var x) (var y)

||| Subtraction of variables. This is an alias for
||| `x - var y`.
public export
(-.) :  {0 as : List a}
     -> (x : Expr a as)
     -> (y : a)
     -> Elem y as
     => Expr a as
(-.) x y = Minus x (var y)

||| Subtraction of variables. This is an alias for
||| `var x - y`.
public export
(.-) :  {0 as : List a}
     -> (x : a)
     -> (y : Expr a as)
     -> Elem x as
     => Expr a as
(.-) x y = Minus (var x) y

||| Multiplication of variables. This is an alias for
||| `var x * var y`.
public export
(.*.) :  {0 as : List a}
      -> (x,y : a)
      -> Elem x as
      => Elem y as
      => Expr a as
(.*.) x y = Mult (var x) (var y)

||| Multiplication of variables. This is an alias for
||| `var x * y`.
public export
(*.) :  {0 as : List a}
     -> (x : Expr a as)
     -> (y : a)
     -> Elem y as
     => Expr a as
(*.) x y = Mult x (var y)

||| Multiplication of variables. This is an alias for
||| `x * var y`.
public export
(.*) :  {0 as : List a}
     -> (x : a)
     -> (y : Expr a as)
     -> Elem x as
     => Expr a as
(.*) x y = Mult (var x) y

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

||| Evaluation of expressions. This keeps the exact
||| structure of the expression tree. For instance
||| `eval $ x .*. (y .+. z)` evaluates to `x * (y + z)`.
public export
eval : Ring a => Expr a as -> a
eval (Lit v)     = v
eval (Var x y)   = x
eval (Neg v)     = neg $ eval v
eval (Plus x y)  = eval x + eval y
eval (Mult x y)  = eval x * eval y
eval (Minus x y) = eval x - eval y

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

||| Proof that addition of exponents is equivalent to multiplcation
||| of the two terms.
export
0 ppow :  Ring a
       => (m,n : Nat)
       -> (x   : a)
       -> pow x (m + n) === pow x m * pow x n
ppow 0     n x = sym multOneLeftNeutral
ppow (S k) n x = Calc $
  |~ x * pow x (plus k n)
  ~~ x * (pow x k * pow x n) ... cong (x*) (ppow k n x)
  ~~ (x * pow x k) * pow x n ... multAssociative


text:
module Main
import Data.Vect

data DataStore : Type where
     MkData : (size : Nat) -> (items : Vect size String) -> DataStore

size : DataStore -> Nat
size (MkData size' items') = size'

items : (store : DataStore) -> Vect (size store) String
items (MkData size' items') = items'

addToStore : DataStore -> String -> DataStore
addToStore (MkData size store) newitem = MkData _ (addToData store)
  where
    addToData : Vect oldsize String -> Vect (S oldsize) String
    addToData [] = [newitem]
    addToData (x :: xs) = x :: addToData xs

data Command = Add String
             | Get Integer
             | Size {- question 1 -}
             | Search String {- question 2 -}
             | Quit

parseCommand : List String -> Maybe Command
parseCommand ("add" :: rest) = Just (Add (unwords rest))
parseCommand ["get", val] = case all isDigit (unpack val) of
                                 False => Nothing
                                 True => Just (Get (cast val))
parseCommand ["quit"] = Just Quit
parseCommand ["size"] = Just Size {- question 1 -}
parseCommand ("search" :: rest) = Just (Search (unwords rest)) {- question 2 -}
parseCommand _ = Nothing

parse : (input : String) -> Maybe Command
parse input = parseCommand (words input)

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

{- question 2/3 -}
searchString : Nat -> (items : Vect n String) -> (str : String) -> String
searchString idx [] str = ""
searchString idx (x :: xs) str
    = let rest = searchString (idx + 1) xs str in
      if isInfixOf str x
         then show idx ++ ": " ++ x ++ "\n" ++ rest
         else rest

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input
    = case parse input of
           Nothing => Just ("Invalid command\n", store)
           Just (Add item) =>
              Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
           Just (Get pos) => getEntry pos store
           Just Size => Just (show (size store) ++ "\n", store) {- question 1 -}
           Just (Search str) => Just (searchString 0 (items store) str, store) {- question 2 -}
           Just Quit => Nothing

main : IO ()
main = replWith (MkData _ []) "Command: " processInput

max_stars_repo_name: PiotrJander/TypeDD-Samples

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
module Vector

%default total

data Vector = V Float Float Float

dot : Vector -> Vector -> Float
dot (V x y z) (V x' y' z') = x * x' + y * y' + z * z'

magnitude : Vector -> Float
magnitude v = v `dot` v

cross : Vector -> Vector -> Vector
cross (V x y z) (V x' y' z') = V (y * z' + z * y')
                                 (-(x * z' + z * x'))
                                 (x * y' + y * x')

zero : Vector
zero = V 0.0 0.0 0.0

unit : Fin 3 -> Vector
unit fZ           = V 1 0 0
unit (fS fZ)      = V 0 1 0
unit (fS (fS fZ)) = V 0 0 1
unit (fS (fS (fS i))) = FalseElim (fin0empty i)
  where fin0empty : Fin 0 -> _|_
        fin0empty fZ impossible
        fin0empty (fS _) impossible

(+) : Vector -> Vector -> Vector
(V x y z) + (V x' y' z') = V (x + x') (y + y') (z + z')

(*) : Vector -> Float -> Vector
(V x y z) * i = V (i*x) (i*y) (i*z)

neg : Vector -> Vector
neg v = v * -1.0

max_stars_repo_name: david-christiansen/idris-raytracer

max_issues_repo_name: david-christiansen/idris-raytracer

max_forks_repo_name: david-christiansen/idris-raytracer


text:
namespace Q1

  data DoorState = DoorOpen | DoorClosed

  data DoorCmd : Type -> DoorState -> DoorState -> Type where
       Open : DoorCmd () DoorClosed DoorOpen
       Close : DoorCmd () DoorOpen DoorClosed
       RingBell : DoorCmd () state state

       Pure : ty -> DoorCmd ty state state
       (>>=) : DoorCmd a state1 state2 ->
               (a -> DoorCmd b state2 state3) ->
               DoorCmd b state1 state3

  doorProg : DoorCmd () DoorClosed DoorClosed
  doorProg = do RingBell
                Open
                RingBell
                Close

namespace Q2

  data GuessCmd : Type -> Nat -> Nat -> Type where
       Try : Integer -> GuessCmd Ordering (S guesses) guesses

       Pure : ty -> GuessCmd ty state state
       (>>=) : GuessCmd a state1 state2 ->
               (a -> GuessCmd b state2 state3) ->
               GuessCmd b state1 state3

  threeGuesses : GuessCmd () 3 0
  threeGuesses = do Try 10
                    Try 20
                    Try 15
                    Pure ()

  {-
  no_guesses : GuessCmd () 0 0
  no_guesses = do Try 10
                  Pure ()
  -}

namespace Q3

  data Matter = Solid | Liquid | Gas

  data MatterCmd : Type -> Matter -> Matter -> Type where
       Melt : MatterCmd () Solid Liquid
       Boil : MatterCmd () Liquid Gas

       Condense : MatterCmd () Gas Liquid
       Freeze : MatterCmd () Liquid Solid

       Pure : ty -> MatterCmd ty state state
       (>>=) : MatterCmd a state1 state2 ->
               (a -> MatterCmd b state2 state3) ->
               MatterCmd b state1 state3

  iceSteam : MatterCmd () Solid Gas
  iceSteam = do Melt
                Boil

  steamIce : MatterCmd () Gas Solid
  steamIce = do Condense
                Freeze

{-
overMelt : MatterCmd () Solid Gas
overMelt = do Melt
              Melt
               -}


text:
data Vect : Nat -> Type -> Type where
     Nil : Vect Z a
     (::) : a -> Vect k a -> Vect (S k) a

wrong : a -> Vect (S n) a -> Vect (S n) a
wrong x xs = x :: x


text:
module Main
import TypeTrans.AST

main : IO ()
main = print "todo"

max_stars_repo_name: RossMeikleham/MSci-Project

max_issues_repo_name: RossMeikleham/MSci-Project

max_forks_repo_name: RossMeikleham/MSci-Project


text:
||| This module provides the reference implementation of
||| `Control.Monad.Dom.Interface.MonadDom`.
module Control.Monad.Dom.DomIO

import Control.MonadRec
import Control.Monad.Dom.Event
import Control.Monad.Dom.Interface
import Control.WellFounded
import Data.Contravariant
import Data.MSF
import Data.IORef
import Data.Iterable
import JS
import Text.Html
import Web.Dom
import Web.Html

%default total

--------------------------------------------------------------------------------
--          Implementation Utilities
--------------------------------------------------------------------------------

||| The environment needed to perform the necessary `MonadDom event`
||| operations: A mutable counter of natural number plus a string prefix
||| to generate unique IDs for reactive components, plus
||| an event handler to be registered at interactive elements.
public export
record DomEnv (event : Type) where
  constructor MkDomEnv
  pre      : String
  unique   : IORef Nat
  handler  : event -> JSIO ()

export
Contravariant DomEnv where
  contramap f  = {handler $= (. f) }

||| Low level method for registering `DOMEvents` at
||| HTML elements.
|||
||| Use this, for instance, to register `DOMEvents` at
||| a HTMLElement of a static document.
export
registerDOMEvent :  (el : EventTarget)
                 -> DOMEvent e
                 -> (handler : e -> JSIO ())
                 -> JSIO ()
registerDOMEvent el de h = case de of
  Input f      => handle "input" inputInfo f
  Change f     => handle "change" changeInfo f
  Click f      => handle "click" mouseInfo f
  DblClick f   => handle "dblclick" mouseInfo f
  KeyDown f    => handle "keydown" keyInfo f
  KeyUp f      => handle "keyup" keyInfo f
  Blur v       => handle "blur" {a = Event} (const $ pure v) Just
  Focus v      => handle "focus" {a = Event} (const $ pure v) Just
  MouseDown f  => handle "mousedown" mouseInfo f
  MouseUp f    => handle "mouseup" mouseInfo f
  MouseEnter f => handle "mouseenter" mouseInfo f
  MouseLeave f => handle "mouseleave" mouseInfo f
  MouseOver f  => handle "mouseover" mouseInfo f
  MouseOut f   => handle "mouseout" mouseInfo f
  MouseMove f  => handle "mousemove" mouseInfo f
  HashChange v => handle "hashchange" {a = Event} (const $ pure v) Just

  where handle :  {0 a,b : _}
               -> SafeCast a
               => String
               -> (a -> JSIO b)
               -> (b -> Maybe e)
               -> JSIO ()
        handle s conv f = do
          c <- callback {cb = EventListener} $ \e => do
            va <- tryCast_ a "Control.Monad.Dom.DomIO.handle" e
            conv va >>= maybe (pure ()) h . f

          addEventListener' el s (Just c)

-- how to listen to a DOMEvent
registerImpl : (ref : ElemRef t) -> DOMEvent e -> DomEnv e -> JSIO ()
registerImpl ref de (MkDomEnv _ _ h) = do
  el  <- castElementByRef ref
  registerDOMEvent el de h

createId : DomEnv e -> JSIO String
createId (MkDomEnv pre u _) = do
  n <- readIORef u
  writeIORef u (S n)
  pure $ pre ++ show n

--------------------------------------------------------------------------------
--          Implementation
--------------------------------------------------------------------------------

||| Reference implementation of `MonadDom event`. This is just
||| a reader monad under the hood.
public export
record DomIO (event : Type) (io : Type -> Type) (a : Type) where
  constructor MkDom
  runDom : DomEnv event -> io a

export
mapEvent : {0 a : _} -> (ev1 -> ev2) -> DomIO ev1 io a -> DomIO ev2 io a
mapEvent f (MkDom runDom) = MkDom $ runDom . contramap f

export
env : Monad m => DomIO ev m (DomEnv ev)
env = MkDom pure

export
fireEvent : LiftJSIO m => ev -> DomIO ev m ()
fireEvent e =  MkDom $ \env => liftJSIO $ env.handler e

export
Functor io => Functor (DomIO ev io) where
  map f dom = MkDom (map f . dom.runDom)

export
Applicative io => Applicative (DomIO ev io) where
  pure v = MkDom $ \_ => pure v
  f <*> v = MkDom $ \ref => f.runDom ref <*> v.runDom ref

export
Monad io => Monad (DomIO ev io) where
  v >>= f = MkDom $ \ref => v.runDom ref >>= (`runDom` ref) . f

convR :  {0 a,e,b,st : Type}
      -> {0 rel : a -> a -> Type}
      -> (f : (v : a) -> st -> DomIO e m (Step rel v st b))
      -> (env : DomEnv e)
      -> (v : a)
      -> (ini : st)
      -> m (Step rel v st b)
convR f env v s1 = runDom (f v s1) env

export
MonadRec io => MonadRec (DomIO e io) where
  tailRecM x ini acc f =
    MkDom $ \env => tailRecM x ini acc (convR f env)

export
HasIO io => HasIO (DomIO ev io) where
  liftIO act = MkDom $ \_ => liftIO act

export
LiftJSIO io => LiftJSIO (DomIO ev io) where
  liftJSIO act = MkDom $ \_ => liftJSIO act

export %inline
LiftJSIO io => MonadDom ev (DomIO ev io) where
  registerEvent ref e = MkDom $ liftJSIO . registerImpl ref e
  uniqueId = MkDom $ liftJSIO . createId

export
handleEvent : LiftJSIO m => ElemRef t -> DOMEvent ev -> DomIO ev m ()
handleEvent el ev = do
  e <- env
  liftJSIO $ registerImpl el ev e

export
setAttribute : LiftJSIO m => ElemRef t -> Attribute ev -> DomIO ev m ()
setAttribute ref a = do
  el <- castElementByRef {t2 = HTMLElement} ref
  case a of
    Id v         => liftJSIO $ setAttribute el "id" v
    Str n v      => liftJSIO $ setAttribute el n v
    Bool n True  => liftJSIO $ setAttribute el n ""
    Bool n False => liftJSIO $ removeAttribute el n
    Event ev     => map handler env >>= liftJSIO . registerDOMEvent (up el) ev

export
setAttributes :  MonadRec m
              => LiftJSIO m
              => ElemRef t
              -> List (Attribute ev)
              -> DomIO ev m ()
setAttributes el = forM_ (setAttribute el)

--------------------------------------------------------------------------------
--          Reactimate
--------------------------------------------------------------------------------

record Refs (ev : Type) where
  constructor MkRefs
  sfRef  : IORef (MSF (DomIO ev JSIO) ev ())
  hRef   : IORef (ev -> JSIO ())
  env    : DomEnv ev

mkRefs : (idPrefix : String) -> (idRef : IORef Nat) -> JSIO (Refs ev)
mkRefs pre idRef = do
  -- the current application state consists of the current
  -- monadic stream function, which will be stored in a
  -- mutable ref
  sfRef  <- newIORef {a = MSF (DomIO ev JSIO) ev ()} (const ())

  -- here we will put the properevent handler, once everyting
  -- is ready. This is not Haskell, so we can't define
  -- the handler lazily and satisfy the totality checker at
  -- the same time
  hRef  <- newIORef {a = ev -> JSIO ()} (const $ pure ())

  -- the `DomEnv` needed to run `mkMSF`
  let env = MkDomEnv pre idRef $ \ev =>
              readIORef hRef >>= (`apply` ev)

  -- we can now implement the *real* event handler:
  -- when an event is being fired, we evaluate the current
  -- MSF and put the resulting continuation in the mutable ref
  -- to be used when the next event occurs.
  let handle : ev -> JSIO ()
      handle = \e => do
        sf1      <- readIORef sfRef
        (_, sf2) <- runDom (step sf1 e) env
        writeIORef sfRef sf2

  -- we need to register the correct event handler, otherwise
  -- nothing will run
  writeIORef hRef handle

  pure (MkRefs sfRef hRef env)

-- initialEvent: If `Just e`, evaluate the given `MSF` once with `e` to
-- properly initialize all components.
-- idPrefix: prefix for uniqe ids
reactimateDom_ :  (initialEvent : Maybe ev)
               -> (idPrefix     : String)
               -> DomIO ev JSIO (MSF (DomIO ev JSIO) ev (), JSIO ())
               -> (idRef        : IORef Nat)
               -> JSIO (JSIO ())
reactimateDom_ ie pre mkMSF idRef = do
  MkRefs sfRef _ env <- mkRefs pre idRef

  -- effectfully create the monadic stream function
  -- this will typically set up (a part of) the visible
  -- user interface, hence the need for `env` with its
  -- event handler and ability to generate unique IDs
  (sf,cl) <- mkMSF.runDom env

  -- register the initial stream function
  writeIORef sfRef sf

  -- finally, we run the initial event (if any)
  traverse_ env.handler ie

  pure cl

||| Sets up an event handler to invoke the given `MSF`
||| whenever the handler is called with a new event
||| value.
|||
||| Uses `idPrefix` as a prefix when generating unique IDs.
||| If you need to properly setup all components by running
||| the MSF with an initial event, use `reactimateDomIni`.
export %inline
reactimateDom : (idPrefix : String)
              -> DomIO ev JSIO (MSF (DomIO ev JSIO) ev (), JSIO ())
              -> JSIO (JSIO ())
reactimateDom pre sf = newIORef 0 >>= reactimateDom_ Nothing pre sf

||| Sets up an event handler to invoke the given `MSF`
||| whenever the handler is called with a new event
||| value.
|||
||| Uses the ID prefix and unique counter generator from
||| the calling `DomIO` environment.
export %inline
reactimateInDom :  DomIO ev JSIO (MSF (DomIO ev JSIO) ev (), JSIO ())
                -> DomIO ev2 JSIO (JSIO ())
reactimateInDom sf =
  MkDom $ \env => reactimateDom_ Nothing env.pre sf env.unique

||| Sets up an event handler to invoke the given `MSF`
||| whenever the handler is called with a new event
||| value.
|||
||| Uses `idPrefix` as a prefix when generating unique IDs.
|||
||| A first evaluation step is run with the given event value
||| to properly setup all components.
export %inline
reactimateDomIni :  ev
                 -> (idPrefix : String)
                 -> DomIO ev JSIO (MSF (DomIO ev JSIO) ev (), JSIO ())
                 -> JSIO (JSIO ())
reactimateDomIni e pre sf =
  newIORef 0 >>= reactimateDom_ (Just e) pre sf

||| Sets up an event handler to invoke the given `MSF`
||| whenever the handler is called with a new event
||| value.
|||
||| Uses the ID prefix and unique counter generator from
||| the calling `DomIO` environment.
|||
||| A first evaluation step is run with the given event value
||| to properly setup all components.
export %inline
reactimateInDomIni :  ev
                   -> DomIO ev JSIO (MSF (DomIO ev JSIO) ev (), JSIO())
                   -> DomIO ev2 JSIO (JSIO ())
reactimateInDomIni v sf =
  MkDom $ \env => reactimateDom_ (Just v) env.pre sf env.unique


text:
module Minecraft.Base.PreClassic.Cobblestone.ItemEntity

import public Minecraft.Base.PreClassic.Cobblestone
import public Minecraft.Core.Entity.Pickup.Export
import public Minecraft.Data.Type.Vtbl

%default total

namespace Export
  public export %hint cobblestoneItemEntity : Pickup Cobblestone.ItemEntity
  public export %hint cobblestoneVtbl       : Vtbl   Cobblestone.ItemEntity

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
||| Copyright 2016 Google Inc.
|||
||| Licensed under the Apache License, Version 2.0 (the "License");
||| you may not use this file except in compliance with the License.
||| You may obtain a copy of the License at
|||
|||     http://www.apache.org/licenses/LICENSE-2.0
|||
||| Unless required by applicable law or agreed to in writing, software
||| distributed under the License is distributed on an "AS IS" BASIS,
||| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
||| See the License for the specific language governing permissions and
||| limitations under the License.

module Protobuf.ParseUtils

import Protobuf.Core

%default total

public export singularTypeForField : FieldDescriptor -> Type
singularTypeForField (MkFieldDescriptor _ ty _ _) = interpFieldValue ty

-- Because fields can come in any order, parsing a message is done in two
-- phases.  First, we parse all the fields into a list of pairs
-- (i : Fin k ** interpField (index fields i))
-- Second, for each field we scan through this list and fill in that field's
-- value based on the list (or create an error).
public export FieldList : Vect k FieldDescriptor -> Type
FieldList {k=k} fields = List (i : Fin k ** singularTypeForField (index i fields))

||| Takes a `FieldList`, and selects the elements which represent the 0th field
||| and puts these into a list, and also creates a list of the remaining
||| elements, which are mapped to be part of of a new `FieldList` for the
||| remaining fields.
reduceFieldList : FieldList (f :: fs) -> (List (singularTypeForField f), FieldList fs)
reduceFieldList Nil = (Nil, Nil)
reduceFieldList ((FZ ** x) :: xs) = let (ys, zs) = reduceFieldList xs in
  (x :: ys, zs)
reduceFieldList (((FS k) ** x) :: xs) = let (ys, zs) = reduceFieldList xs in
  (ys, (k ** x) :: zs)

optionalFieldFromList : List (interpFieldValue f) -> Maybe (interpFieldValue f)
optionalFieldFromList Nil      = Nothing
optionalFieldFromList (x::Nil) = Just x
optionalFieldFromList (x::xs)  = optionalFieldFromList xs

fieldFromFieldList : List (singularTypeForField d) -> Either String (interpField d)
fieldFromFieldList {d=MkFieldDescriptor Optional _ _ _} xs = Right (last' xs)
fieldFromFieldList {d=MkFieldDescriptor Required _ name _} xs = case (last' xs) of
    Nothing  => Left ("The required field " ++ (show name) ++ " was not set.")
    (Just x) => Right x
fieldFromFieldList {d=MkFieldDescriptor Repeated _ _ _} xs = Right xs

export messageFromFieldList : FieldList fields -> Either String (InterpFields fields)
messageFromFieldList {fields=Nil} _ = return Nil
messageFromFieldList {fields=f::fs} xs = let (ys, zs) = reduceFieldList xs in
  case fieldFromFieldList ys of
    Left err => Left err
    Right first => case messageFromFieldList zs of
      Left err => Left err
      Right rest => Right (first :: rest)

max_stars_repo_name: google/idris-protobuf

max_issues_repo_name: google/idris-protobuf

max_forks_repo_name: google/idris-protobuf