text:
module Data.Strong.Array.Fusion

import Data.Strong.Array

import Language.Reflection

-- import public Language.Reflection.Pretty
-- import public Language.Reflection.Syntax
-- import public Language.Reflection.Types
--
-- import public Text.PrettyPrint.Prettyprinter
--
-- -- import Generics.Derive
%language ElabReflection

-- I can get elab to inline and fuse for me but not quite as
-- nicely/automatically as I prefer so far, work continues.

-- %hide Prelude.Basics.(.)

-- This is probably a lost cause currently, inlining occurs _after_ %transforms
-- so we can't use them to fuse things like blar. Perhaps elaborator reflection
-- can do something, but I'm not sure how far we can get with Check/Quote

data Step : Type -> Type -> Type where
  Yield : a -> s -> Step s a
  Skip : s -> Step s a
  Done : Step s a

data Stream : Nat -> Type -> Type where
  MkStream : (s -> Step s a) -> s -> (n : Nat) -> Stream n a

stream : Array n a -> Stream n a
-- stream arr = case arr of
    -- MkArray s _ _ => MkStream step 0 s
  -- where
    -- step : Int -> Step Int a
    -- step s = if s >= intSize arr
      -- then Done
      -- else Yield (unsafeReadArray arr (cast s)) (s+1)

unstream : Stream n a -> Array n a

-- %transform "what" Prelude.(.) = Fusion.gop

mapS : (a -> b) -> Stream n a -> Stream n b
mapS f (MkStream step s i) = MkStream (\s' => case step s' of
  (Yield x y) => Yield (f x) y
  (Skip x) => Skip x
  Done => Done) s i

-- braf : Elab ((b -> c) -> (a -> b) -> (a -> c))

-- I just want this to wrap in stream/unstream
-- export
-- streamWrap : (Stream a -> Stream b) -> Array s a -> Elab (Array s a -> Array s b)
-- streamWrap f arr = pure (newUnintializedArray 2)

-- %macro
-- streamWrap : {s,n,a,b:_} -> (Stream n a -> Stream n b) -> Elab (Array s a -> Array s b)
-- streamWrap f = do
--   r <- quote f
--   check `(unstream . ~r . stream)

-- %macro
-- map' : {s,a,b:_} -> (a -> b) -> Elab (Array s a -> Array s b)
-- map' f = do
--   r <- quote f
--   check `(unstream . mapS ~r . stream)

-- `(stream (unstream ~x))
spider : TTImp -> TTImp
spider `(stream (unstream ~x)) = spider x
spider (IPi x y z w argTy retTy) = IPi x y z w (spider argTy) (spider retTy)
spider (ILam x y z w argTy lamTy) = (ILam x y z w (spider argTy) (spider lamTy))
spider (ILet x lhsFC y z nTy nVal scope) = (ILet x lhsFC y z (spider  nTy) (spider nVal) (spider scope))
spider (ICase x y ty xs) = (ICase x y (spider ty) xs) -- do clauses?
spider (ILocal x xs y) = (ILocal x xs (spider y)) -- do decls?
spider (IUpdate x xs y) = (IUpdate x xs (spider y))
spider `(Data.Strong.Array.Fusion.stream {a = _} {n = _} (Data.Strong.Array.Fusion.unstream {a = _} {n = _} ~x)) = x
spider (INamedApp x y z w) = (INamedApp x (spider y) z (spider w))
spider (IApp x y z) = (IApp x (spider y) (spider z))
spider (IAutoApp x y z) = (IAutoApp x (spider y) (spider z))
spider (IWithApp x y z) = (IWithApp x (spider y) (spider z))
spider (IAlternative x y xs) = (IAlternative x y (map spider xs))
spider (IRewrite x y z) = (IRewrite x (spider y) (spider z))
spider (IBindHere x y z) = (IBindHere x y (spider z))
spider (IAs x nameFC y z w) = (IAs x nameFC y z (spider w))
spider (IMustUnify x y z) = (IMustUnify x y (spider z))
spider (IDelayed x y z) = (IDelayed x y (spider z))
spider (IDelay x y) = (IDelay x (spider y))
spider (IForce x y) = (IForce x (spider y))
spider (IQuote x y) = (IQuote x (spider y))
spider (IUnquote x y) = (IUnquote x (spider y))
spider (IWithUnambigNames x xs y) = (IWithUnambigNames x xs (spider y))
spider x = x

infixr 9 `dot`

-- fuse : x -> x
-- fuse x = %runElab do
--   r <- quote x
--   logTerm "" 1 "faf" r
--   check (spider r)

infixr 9 `dott`

%macro
dott : {c:_} -> (b -> c) -> (a -> b) -> Elab (a -> c)
dott f g  = lambda _ $ \x => do
  -- let r = g x
  -- let r' = f r
  -- d <- quote r
  -- `(Data.Strong.Array.Fusion.stream {a = _} {n = _} (Data.Strong.Array.Fusion.unstream {a = _} {n = _} ~y)) <- quote r
    -- | _ => pure r'
  -- _ <- check d
  pure (f (g x))
  -- ?dfdf

-- %transform "stream fusion1" Fusion.stream . Fusion.unstream = Prelude.id

-- %macro
-- dot : {c:_} -> (b -> c) -> (a -> b) -> a -> Elab c
-- dot f g x = do
--   r <- quote (f (g x))
--   check (spider r)

%macro
map' : (a -> b) -> Elab (Array s a -> Array s b)
map' f = lambda _ $ \x => pure $ unstream (mapS f (stream x))

-- %macro
-- streamWrap : {s,a,b:_} -> (Stream s a -> Stream s b) -> Elab (Array s a -> Array s b)
-- streamWrap f = lambda _ $ \x => pure $ unstream (f (stream x))

-- map' : (a -> b) -> Array s a -> Array s b
-- map' f = streamWrap (mapS f)

-- %inline
-- map' : (a -> b) -> Array s a -> Array s b
-- map' f = unstream `dot` mapS f `dot` stream

export
blar : Array s Double -> Array s Double
blar = map' {s} (Prelude.(+) 1.0) `dott` map' (Prelude.(+) 2.0) `dott` Prelude.id

-- export
-- blar : Array s Double -> Array s Double
-- blar arr =
--   let f = map' {s} (Prelude.(+) 1.0) `dott` map' (Prelude.(+) 2.0) `dott` id
--   in %runElab do
--     z <- quote (f arr)
--     let r = spider z
--     logTerm "" 1 "wah" r
--     check r
    -- pure z

-- farf : Int -> Int
-- farf = dot (+1) (+1)

-- I need map' to inline before our fusion rule fires so I get the below
-- which the rule should match:
-- ^ unstream . mapS (+1) . stream . unstream . mapS (+2) . stream
-- ^ unstream . (mapS (+1) . (stream . (unstream . (mapS (+2) . stream))))

-- So, how do we unroll map' via elab?

-- (IApp EmptyFC (INamedApp EmptyFC (INamedApp EmptyFC (IVar EmptyFC (NS (MkNS ["Fusion","Array","Strong","Data"]) (UN "stream"))) (UN "a") (IPrimVal EmptyFC DoubleType)) (UN "n") (IHole (MkFC (Virtual Interactive) (0,15) (0, 20)) "s")) (IApp EmptyFC (INamedApp EmptyFC (INamedApp EmptyFC (IVar EmptyFC (NS (MkNS ["Fusion","Array","Strong","Data"]) (UN "unstream"))) (UN "a") (IPrimVal EmptyFC DoubleType)) (UN "n") (IHole (MkFC (Virtual Interactive) (0,15) (0,20)) "s")) (UN "x")

-- (IApp EmptyFC
--   (INamedApp EmptyFC
--     (INamedApp EmptyFC
--       (IVar EmptyFC (NS (MkNS ["Fusion","Array","Strong","Data"]) (UN "stream")))
--       (UN "a")
--       (IPrimVal EmptyFC DoubleType))
--     (UN "n")
--     (IHole "s"))
--   (IApp EmptyFC
--     (INamedApp EmptyFC
--       (INamedApp EmptyFC
--         (IVar EmptyFC (NS (MkNS ["Fusion","Array","Strong","Data"]) (UN "unstream")))
--         (UN "a")
--         (IPrimVal EmptyFC DoubleType))
--       (UN "n")
--       (IHole "s"))

-- (IApp _ (INamedApp _ (INamedApp _ (IVar _ (NS (MkNS ["Fusion","Array","Strong","Data"]) (UN "stream"))) _ _) _ _) (IApp _ (INamedApp _ (INamedApp _ (IVar EmptyFC (NS (MkNS ["Fusion","Array","Strong","Data"]) (UN "unstream"))) _ _) _ _) w))

-- foo : TTImp
-- foo = `( stream . unstream)
--
-- spider : TTImp -> TTImp
-- spider `((~f . ~g) ~x) = `(~(spider f) (~(spider g) x))
-- spider r = r
--
-- fuse : TTImp -> TTImp
-- fuse `(stream (unstream ~x)) = x
-- fuse r = r

-- `(unstream . map1 . stream . unstream . map 2 . stream)
-- LOG declare.type:1: Processing Data.Strong.Array.Fusion.14044:1647:it
-- IApp (IApp (IVar (UN ".")) (IVar (UN "unstream"))) (IApp (IApp (IVar (UN ".")) (IVar (UN "map1"))) (IApp (IApp (IVar (UN ".")) (IVar (UN "stream"))) (IApp (IApp (MkFC (Virtual Interactive) (0, 29) (0,
-- 54)) (IVar (MkFC (Virtual Interactive) (0, 38) (0,
-- 39)) (UN ".")) (IVar (MkFC (Virtual Interactive) (0, 29) (0,
-- 37)) (UN "unstream"))) (IApp (MkFC (Virtual Interactive) (0, 40) (0,
-- 54)) (IApp (MkFC (Virtual Interactive) (0, 40) (0,
-- 54)) (IVar (MkFC (Virtual Interactive) (0, 46) (0,
-- 47)) (UN ".")) (IApp (MkFC (Virtual Interactive) (0, 40) (0,
-- 45)) (IVar (MkFC (Virtual Interactive) (0, 40) (0,
-- 43)) (UN "map")) (IApp (MkFC (Virtual Interactive) (0, 44) (0,
-- 45)) (IVar (MkFC (Virtual Interactive) (0, 44) (0,
-- 45)) (UN "fromInteger")) (IPrimVal (MkFC (Virtual Interactive) (0, 44) (0,
-- 45)) (BI 2))))) (IVar (MkFC (Virtual Interactive) (0, 48) (0,
-- 54)) (UN "stream"))))))
-- Data.Strong.Array.Fusion>

--
-- dot : (b -> c) -> (a -> b) -> (a -> c)
-- dot f g x = %runElab do
--   z <- quote $ blar {s=1}
--   q <- quote $ Fusion.map' (+1) {a=Int} {b=Int} {s=1}
--   logTerm "" 1 "blar" z
--   logTerm "" 1 "map'" q
--   logTerm "" 1 "spider" $ spider `(unstream . map1 . stream . unstream . map 2 . stream)
--   pure (f (g x))
--   --?sdffd
--
-- foo2 : Elab ()
-- foo2 = do
--   ?asSDfsfd

-- %transform "vectStreamFusion3" Fusion.map' f . Fusion.map' g = Fusion.map' (f . g)

main : IO ()
-- main = pure ()
main = do
  -- let xvar = nak $ MkStream {a=Int} (\_ => Done) 'a' 1
  printLn (blar $ fromList [1.0,2.0,3.0])

max_stars_repo_name: MarcelineVQ/sarray


text:
{-

1. Anything where the list is the same length as the input. We don't know
the types of elements contained in the list, however, so we can't look at them.
Some possibilities (there are many others!):

   - sorting the list
   - reversing the list
   - returning the input unchanged

2. Anything where the output list is twice as long as the input.
Some possibilities:

   - Duplicating each element
   - Returning the list appended to itself

3. Anything where the output list is one item shorter than the input, which
must itself be non-empty. Some possibilities:

    - Returning all but the first element
    - Returning all but the last element

4. The bounded number is likely to refer to a position in the list, so this
could be a function to return the element at that position.

-}

ext: idr

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
> module Fraction.EqProperties

> import Syntax.PreorderReasoning

> import Fraction.Fraction
> import Fraction.BasicOperations
> import Fraction.Predicates
> import Fraction.BasicProperties
> import PNat.PNat
> import PNat.Operations
> import PNat.Properties
> import Nat.LTProperties
> import Nat.OperationsProperties
> import Nat.Positive

> %default total
> %access export
> -- %access public export

> -- %logging 5

* |Eq| is an equivalence:

> ||| Eq is reflexive
> EqReflexive : {x : Fraction} -> x `Eq` x
> EqReflexive {x = (m, d')} = Refl

> ||| Eq is symmetric
> EqSymmetric : {x, y : Fraction} -> x `Eq` y -> y `Eq` x
> EqSymmetric {x = (m, d')} {y = (n, e')} = sym

> ||| Eq is transitive
> EqTransitive : {x, y, z : Fraction} -> x `Eq` y -> y `Eq` z  -> x `Eq` z
> EqTransitive {x = (m, d')} {y = (n, e')} {z = (o, f')} xy yz =
>   let d       =  toNat d' in
>   let e       =  toNat e' in
>   let f       =  toNat f' in
>   let neEQZ   :  (Not (e = Z))
>               =  gtZisnotZ (toNatLTLemma e') in
>   let s1      :  ((m * e) * f = (n * d) * f)
>               =  multPreservesEq (m * e) (n * d) f f xy Refl in
>   let s2      :  (m * (e * f) = (n * d) * f)
>               =  replace {P = \ ZUZU => ZUZU = (n * d) * f} (sym (multAssociative m e f)) s1 in
>   let s3      :  (m * (f * e) = (n * d) * f)
>               =  replace {P = \ ZUZU => m * ZUZU = (n * d) * f} (multCommutative e f) s2 in
>   let s4      :  ((m * f) * e = (n * d) * f)
>               =  replace {P = \ ZUZU => ZUZU = (n * d) * f} (multAssociative m f e) s3 in
>   let s5      :  ((m * f) * e = n * (d * f))
>               =  replace {P = \ ZUZU => (m * f) * e = ZUZU} (sym (multAssociative n d f)) s4 in
>   let s6      :  ((m * f) * e = n * (f * d))
>               =  replace {P = \ ZUZU => (m * f) * e = n * ZUZU} (multCommutative d f) s5 in
>   let s7      :  ((m * f) * e = (n * f) * d)
>               =  replace {P = \ ZUZU => (m * f) * e = ZUZU} (multAssociative n f d) s6 in
>   let s8      :  ((m * f) * e = (o * e) * d)
>               =  replace {P = \ ZUZU => (m * f) * e = ZUZU * d} yz s7 in
>   let s9      :  ((m * f) * e = o * (e * d))
>               =  replace {P = \ ZUZU => (m * f) * e = ZUZU} (sym (multAssociative o e d)) s8 in
>   let s10     :  ((m * f) * e = o * (d * e))
>               =  replace {P = \ ZUZU => (m * f) * e = o * ZUZU} (multCommutative e d) s9 in
>   let s11     :  ((m * f) * e = (o * d) * e)
>               =  replace {P = \ ZUZU => (m * f) * e = ZUZU} (multAssociative o d e) s10 in
>
>   multMultElimRight (m * f) (o * d) e e Refl neEQZ s11

* |Eq| decidable

> |||
> decEq : (x : Fraction) -> (y : Fraction) -> Dec (x `Eq` y)
> decEq (m, d') (n, e') = let d = toNat d' in
>                         let e = toNat e' in
>                         decEq (m * e) (n * d)

* Properties of |(=)| and |Eq|:

> ||| Equality implies `Eq`
> eqEq : {x, y : Fraction} -> x = y -> x `Eq` y
> eqEq {x = (m, d')} {y = (m, d')} Refl = Refl

Properties of |plus| and |Eq|:

> |||
> plusPreservesEq : (x, x', y, y' : Fraction) ->
>                   (x `Eq` x') -> (y `Eq` y') -> (x + y) `Eq` (x' + y')
> plusPreservesEq (n, Element d _) (n', Element d' _)
>                 (m, Element e _) (m', Element e' _)
>                 nd'EQn'd me'EQm'e = pf where
>   helper2 : (a, b, c, d, a', c' : Nat) -> (a * c = a' * c') ->
>             ((a * b) * (c * d)) = ((a' * d) * (c' * b))
>   helper2 a b c d a' c' acEQa'c' =
>     ((a * b) * (c * d))   ={ multFlipCentre a b c d }=
>     ((a * c) * (b * d))   ={ cong {f = \x => x * (b * d)} acEQa'c' }=
>     ((a' * c') * (b * d)) ={ cong {f = \x => (a' * c') * x} (multCommutative b d) }=
>     ((a' * c') * (d * b)) ={ multFlipCentre a' c' d b }=
>     ((a' * d) * (c' * b)) QED
>   pf : ((n * e) + (m * d)) * (d' * e') = ((n' * e') + (m' * d')) * (d * e)
>   pf =
>     (((n * e) + (m * d)) * (d' * e'))
>       ={ multDistributesOverPlusLeft (n * e) (m * d) (d' * e') }=
>     (((n * e) * (d' * e')) + ((m * d) * (d' * e')))
>       ={ cong {f = \x => x + ((m * d) * (d' * e'))} (helper2 n e d' e' n' d nd'EQn'd) }=
>     (((n' * e') * (d * e)) + ((m * d) * (d' * e')))
>       ={ cong {f = \x => ((n' * e') * (d * e)) + ((m * d) * x)} (multCommutative d' e') }=
>     (((n' * e') * (d * e)) + ((m * d) * (e' * d')))
>       ={ cong {f = \x => ((n' * e') * (d * e)) + x} (helper2 m d e' d' m' e me'EQm'e) }=
>     (((n' * e') * (d * e)) + ((m' * d') * (e * d)))
>       ={ cong {f = \x => ((n' * e') * (d * e)) + ((m' * d') * x)} (multCommutative e d) }=
>     (((n' * e') * (d * e)) + ((m' * d') * (d * e)))
>       ={ sym (multDistributesOverPlusLeft (n' * e') (m' * d') (d * e)) }=
>     (((n' * e') + (m' * d')) * (d * e))
>       QED

Properties of |mult|, |Eq|:

> |||
> multZeroRightEqZero : (x : Fraction) -> x * 0 `Eq` 0
> multZeroRightEqZero (m, d') =
>   let d = toNat d' in
>     ( (m * 0) * 1 )
>   ={ cong {f = \ ZUZU => ZUZU * 1} (multZeroRightZero m) }=
>     ( 0 * 1 )
>   ={ multZeroLeftZero 1 }=
>     ( 0 )
>   ={ sym (multZeroLeftZero (d * 1)) }=
>     ( 0 * (d * 1) )
>   QED

> |||
> multZeroLeftEqZero : (x : Fraction) -> 0 * x `Eq` 0
> multZeroLeftEqZero x =
>   let zxEqxz  : (0 * x `Eq` x * 0)
>               = eqEq (multCommutative 0 x) in
>   let xzEqz   : (x * 0 `Eq` 0)
>               = multZeroRightEqZero x in
>   EqTransitive zxEqxz xzEqz

> |||
> multPreservesEq : (x, x', y, y' : Fraction) ->
>                   (x `Eq` x') -> (y `Eq` y') -> (x * y) `Eq` (x' * y')
> multPreservesEq (n, Element d _) (n', Element d' _)
>                 (m, Element e _) (m', Element e' _)
>                 nd'EQn'd me'EQm'e = pf where
>   pf : (n * m) * (d' * e') = (n' * m') * (d * e)
>   pf =
>     ((n * m) * (d' * e')) ={ multFlipCentre n m d' e' }=
>     ((n * d') * (m * e')) ={ cong {f = \x => x * (m * e')} nd'EQn'd }=
>     ((n' * d) * (m * e')) ={ cong {f = \x => (n' * d) * x} me'EQm'e }=
>     ((n' * d) * (m' * e)) ={ multFlipCentre n' d m' e }=
>     ((n' * m') * (d * e)) QED

Properties of |plus|, |mult|, |Eq|:

> |||
> multDistributesOverPlusRightEq : {x, y, z : Fraction} -> x * (y + z) `Eq` (x * y) + (x * z)
> multDistributesOverPlusRightEq {x = (m, d')} {y = (n, e')} {z = (o, f')} =
>   let d       =  toNat d' in
>   let e       =  toNat e' in
>   let f       =  toNat f' in
>     ( (m * (n * f + o * e)) * (toNat ((d' * e') * (d' * f'))) )
>   ={ cong {f = \ ZUZU => (m * (n * f + o * e)) * ZUZU} toNatMultLemma }=
>     ( (m * (n * f + o * e)) * ((toNat (d' * e')) * (toNat (d' * f'))) )
>   ={ cong {f = \ ZUZU => (m * (n * f + o * e)) * (ZUZU * (toNat (d' * f')))} toNatMultLemma }=
>     ( (m * (n * f + o * e)) * ((d * e) * (toNat (d' * f'))) )
>   ={ cong {f = \ ZUZU => (m * (n * f + o * e)) * ((d * e) * ZUZU)} toNatMultLemma }=
>     ( (m * (n * f + o * e)) * ((d * e) * (d * f)) )
>   ={ cong {f = \ ZUZU => (m * (n * f + o * e)) * ZUZU} (multFlipCentre d e d f) }=
>     ( (m * (n * f + o * e)) * ((d * d) * (e * f)) )
>   ={ cong {f = \ ZUZU => (m * (n * f + o * e)) * ZUZU} (sym (multAssociative d d (e * f))) }=
>     ( (m * (n * f + o * e)) * (d * (d * (e * f))) )
>   ={ multAssociative (m * (n * f + o * e)) d (d * (e * f)) }=
>     ( ((m * (n * f + o * e)) * d) * (d * (e * f)) )
>   ={ cong {f = \ ZUZU => (ZUZU * d) * (d * (e * f))} (multDistributesOverPlusRight m (n * f) (o * e)) }=
>     ( ((m * (n * f) + m * (o * e)) * d) * (d * (e * f)) )
>   ={ cong {f = \ ZUZU => ((ZUZU + m * (o * e)) * d) * (d * (e * f))} (multAssociative m n f) }=
>     ( (((m * n) * f + m * (o * e)) * d) * (d * (e * f)) )
>   ={ cong {f = \ ZUZU => (((m * n) * f + ZUZU) * d) * (d * (e * f))} (multAssociative m o e) }=
>     ( (((m * n) * f + (m * o) * e) * d) * (d * (e * f)) )
>   ={ cong {f = \ ZUZU => ZUZU * (d * (e * f))} (multDistributesOverPlusLeft ((m * n) * f) ((m * o) * e) d)}=
>     ( (((m * n) * f) * d + ((m * o) * e) * d) * (d * (e * f)) )
>   ={ cong {f = \ ZUZU => (ZUZU + ((m * o) * e) * d) * (d * (e * f))} (sym (multAssociative (m * n) f d)) }=
>     ( ((m * n) * (f * d) + ((m * o) * e) * d) * (d * (e * f)) )
>   ={ cong {f = \ ZUZU => ((m * n) * (f * d) + ZUZU) * (d * (e * f))} (sym (multAssociative (m * o) e d)) }=
>     ( ((m * n) * (f * d) + (m * o) * (e * d)) * (d * (e * f)) )
>   ={ cong {f = \ ZUZU => ((m * n) * (f * d) + (m * o) * ZUZU) * (d * (e * f))} (multCommutative e d) }=
>     ( ((m * n) * (f * d) + (m * o) * (d * e)) * (d * (e * f)) )
>   ={ cong {f = \ ZUZU => ((m * n) * ZUZU + (m * o) * (d * e)) * (d * (e * f))} (multCommutative f d) }=
>     ( ((m * n) * (d * f) + (m * o) * (d * e)) * (d * (e * f)) )
>   ={ cong {f = \ ZUZU => ((m * n) * (d * f) + (m * o) * (d * e)) * (d * ZUZU)} (sym toNatMultLemma) }=
>     ( ((m * n) * (d * f) + (m * o) * (d * e)) * (d * (toNat (e' * f'))) )
>   ={ cong {f = \ ZUZU => ((m * n) * (d * f) + (m * o) * (d * e)) * ZUZU}  (sym toNatMultLemma) }=
>     ( ((m * n) * (d * f) + (m * o) * (d * e)) * (toNat (d' * (e' * f'))) )
>   ={ cong {f = \ ZUZU => ((m * n) * (d * f) + (m * o) * ZUZU) * (toNat (d' * (e' * f')))}
>           (sym toNatMultLemma) }=
>     ( ((m * n) * (d * f) + (m * o) * (toNat (d' * e'))) * (toNat (d' * (e' * f'))) )
>   ={ cong {f = \ ZUZU => ((m * n) * ZUZU + (m * o) * (toNat (d' * e'))) * (toNat (d' * (e' * f')))}
>           (sym toNatMultLemma) }=
>     ( ((m * n) * (toNat (d' * f')) + (m * o) * (toNat (d' * e'))) * (toNat (d' * (e' * f'))) )
>   QED

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Replica.App.Clock

import Control.App
import public System.Clock

%default total

public export
interface SystemClock e where
  threadClock : App e (Clock Thread)

export
PrimIO e => SystemClock e where
  threadClock = primIO $ clockTime Thread

export
showDuration : Clock Duration -> String
showDuration (MkClock seconds nanoseconds) = let
  ns = div nanoseconds 10000
  in "\{show seconds}.\{show ns}s"

export
durationOf : SystemClock e => App e a -> App e (Clock Duration, a)
durationOf x = do
  start <- threadClock
  res <- x
  end <- threadClock
  pure (timeDifference end start, res)

max_stars_repo_name: claymager/REPLica

max_issues_repo_name: claymager/REPLica

max_forks_repo_name: claymager/REPLica


text:
module Libraries.Data.Graph

import Libraries.Data.SortedMap
import Libraries.Data.SortedSet

import Data.List1

-- Mechanically transcribed from
-- https://en.wikipedia.org/wiki/Tarjan%27s_strongly_connected_components_algorithm#The_algorithm_in_pseudocode
private
record TarjanVertex where
  constructor TV
  index   : Int
  lowlink : Int
  inStack : Bool

private
record TarjanState cuid where
  constructor TS
  vertices           : SortedMap cuid TarjanVertex
  stack              : List cuid
  nextIndex          : Int
  components         : List (List1 cuid)
  impossibleHappened : Bool  -- we should get at least some indication of broken assumptions

initial : Ord cuid => TarjanState cuid
initial = TS empty [] 0 [] False

||| Find strongly connected components in the given graph.
|||
||| Input: map from vertex X to all vertices Y such that there is edge X->Y
||| Output: list of strongly connected components, ordered by output degree descending
export
tarjan : Ord cuid => SortedMap cuid (SortedSet cuid) -> List (List1 cuid)
tarjan {cuid} deps = loop initial (SortedMap.keys deps)
  where
    strongConnect : TarjanState cuid -> cuid -> TarjanState cuid
    strongConnect ts v =
        let ts'' = case SortedMap.lookup v deps of
              Nothing => ts'  -- no edges
              Just edgeSet => loop ts' (SortedSet.toList edgeSet)
          in case SortedMap.lookup v ts''.vertices of
              Nothing => { impossibleHappened := True } ts''
              Just vtv =>
                if vtv.index == vtv.lowlink
                  then createComponent ts'' v []
                  else ts''
      where
        createComponent : TarjanState cuid -> cuid -> List cuid -> TarjanState cuid
        createComponent ts v acc =
          case ts.stack of
            [] => { impossibleHappened := True } ts
            w :: ws =>
              let ts' : TarjanState cuid = {
                      vertices $= SortedMap.adjust w { inStack := False },
                      stack := ws
                    } ts
                in if w == v
                  then { components $= ((v ::: acc) ::) } ts'  -- that's it
                  else createComponent ts' v (w :: acc)

        loop : TarjanState cuid -> List cuid -> TarjanState cuid
        loop ts [] = ts
        loop ts (w :: ws) =
          loop (
            case SortedMap.lookup w ts.vertices of
              Nothing => let ts' = strongConnect ts w in
                case SortedMap.lookup w ts'.vertices of
                  Nothing => { impossibleHappened := True } ts'
                  Just wtv => { vertices $= SortedMap.adjust v { lowlink $= min wtv.lowlink } } ts'

              Just wtv => case wtv.inStack of
                False => ts  -- nothing to do
                True => { vertices $= SortedMap.adjust v { lowlink $= min wtv.index } } ts
          ) ws

        ts' : TarjanState cuid
        ts' = {
            vertices  $= SortedMap.insert v (TV ts.nextIndex ts.nextIndex True),
            stack     $= (v ::),
            nextIndex $= (1+)
          } ts

    loop : TarjanState cuid -> List cuid -> List (List1 cuid)
    loop ts [] =
      if ts.impossibleHappened
        then []
        else ts.components
    loop ts (v :: vs) =
      case SortedMap.lookup v ts.vertices of
        Just _ => loop ts vs  -- done, skip
        Nothing => loop (strongConnect ts v) vs


text:
module SubstLemmas

-- Lemmas about substitution (and the related
-- operations 'shiftTerm' and 'shift').

import Subst
import Term
import Typing

%default total
%access export

---------------------------------------
-- Begin: SUBSTITUTION PRESERVES TYPING

-- Lemmas about extending contexts (in the middle)
-- are required for the proof of the fact that
-- substitution preserves typing.
-- (In fact, the proof of preservation of typing under
-- substitution only requires a lemma about extending
-- the context at the front. However, to prove this
-- lemma about extending the context, one has to assume
-- that the context is extended in the middle in order
-- for induction to go through in the case of 'TAbs'.)

-- Extending a context 'ctx1++ctx2' in the middle preserves
-- the types that are in the context, but the index 'k' must
-- be shifted appropriately in order to retrieve the same
-- type from the extended context:
shiftTy : (k : Nat) ->
          index' k (ctx1++ctx2) = Just t ->
          (ctx : Context) ->
          index' (shift (length ctx1) (length ctx) k) (ctx1++ctx++ctx2) = Just t
shiftTy {ctx1 = []}       k     prf  []       = prf
shiftTy {ctx1 = []}       k     prf  (s::ctx) = shiftTy {ctx1=[]} k prf ctx
shiftTy {ctx1 = t1::ctx1} Z     Refl ctx      = Refl
shiftTy {ctx1 = t1::ctx1} (S k) prf  ctx      = shiftTy {ctx1=ctx1} k prf ctx

-- Typing is preserved if a context 'ctx1++ctx2' is extended
-- in the middle provided the term 'e' is shifted appropriately:
shiftTermTy : (e : Term) ->
              Typing (ctx1++ctx2) e t ->
              (ctx : Context) ->
              Typing (ctx1++ctx++ctx2) (shiftTerm (length ctx1) (length ctx) e) t
--
shiftTermTy (TVar i) (TyVar prf) ctx =
  TyVar $ shiftTy i prf ctx
--
shiftTermTy (TAbs e) (TyAbs s ty) ctx {ctx1} =
  TyAbs s $ shiftTermTy e ty ctx {ctx1=s::ctx1}
--
shiftTermTy (TApp e1 e2) (TyApp ty1 ty2) ctx =
  TyApp (shiftTermTy e1 ty1 ctx)
        (shiftTermTy e2 ty2 ctx)
--
shiftTermTy (TRec e1 e2 e3) (TyRec ty1 ty2 ty3) ctx =
  TyRec (shiftTermTy e1 ty1 ctx)
        (shiftTermTy e2 ty2 ctx)
        (shiftTermTy e3 ty3 ctx)
--
shiftTermTy TZero TyZero ctx = TyZero
--
shiftTermTy (TSucc e) (TySucc ty) ctx =
  TySucc $ shiftTermTy e ty ctx
--
shiftTermTy (TPred e) (TyPred ty) ctx =
  TyPred $ shiftTermTy e ty ctx
--
shiftTermTy (TIfz e1 e2 e3) (TyIfz ty1 ty2 ty3) ctx =
  TyIfz (shiftTermTy e1 ty1 ctx)
        (shiftTermTy e2 ty2 ctx)
        (shiftTermTy e3 ty3 ctx)

-- Finally, substitution preserves typing:
substPreservesTy : (e : Term) ->   -- Term in which substitution takes place.
                   Typing (ctx1++s::ctx2) e t ->
                   (es : Term) ->  -- Term that is substituted in.
                   Typing ctx2 es s ->
                   Typing (ctx1++ctx2) (subst es (length ctx1) e) t
--
substPreservesTy {ctx1 = []}       (TVar Z)     (TyVar Refl) es esTy = esTy
substPreservesTy {ctx1 = []}       (TVar (S i)) (TyVar prf)  es esTy = TyVar prf
substPreservesTy {ctx1 = t1::ctx1} (TVar Z)     (TyVar prf)  es esTy = TyVar prf
substPreservesTy {ctx1 = t1::ctx1} (TVar (S k)) (TyVar prf)  es esTy =
  let ih = substPreservesTy {ctx1=ctx1} (TVar k) (TyVar prf) es esTy
  in shiftTermTy _ ih [t1] {ctx1=[]}
--
substPreservesTy {ctx1} (TAbs e) (TyAbs s ty) es esTy =
  TyAbs s $ substPreservesTy e ty es esTy {ctx1=s::ctx1}
--
substPreservesTy (TApp e1 e2) (TyApp ty1 ty2) es esTy =
  TyApp (substPreservesTy e1 ty1 es esTy)
        (substPreservesTy e2 ty2 es esTy)
--
substPreservesTy (TRec e1 e2 e3) (TyRec ty1 ty2 ty3) es esTy =
  TyRec (substPreservesTy e1 ty1 es esTy)
        (substPreservesTy e2 ty2 es esTy)
        (substPreservesTy e3 ty3 es esTy)
--
substPreservesTy TZero TyZero es esTy = TyZero
--
substPreservesTy (TSucc e) (TySucc ty) es esTy =
  TySucc $ substPreservesTy e ty es esTy
--
substPreservesTy (TPred e) (TyPred ty) es esTy =
  TyPred $ substPreservesTy e ty es esTy
--
substPreservesTy (TIfz e1 e2 e3) (TyIfz ty1 ty2 ty3) es esTy =
  TyIfz (substPreservesTy e1 ty1 es esTy)
        (substPreservesTy e2 ty2 es esTy)
        (substPreservesTy e3 ty3 es esTy)

-- End: SUBSTITUTION PRESERVES TYPING
-------------------------------------

---------------------------------------
-- Begin: SEVERAL LEMMAS ABOUT SHIFTING

-- The following lemmas come in pairs:
-- The really useful lemma in each pair
-- is the one about 'shiftTerm'.
-- However, the lemma in each pair that
-- is non-trivial to prove is usually the
-- other one, i.e. the one about 'shift'.

shiftByZero : (c : Nat) ->
              (k : Nat) ->
              shift c Z k = k
shiftByZero Z     k     = Refl
shiftByZero (S c) Z     = Refl
shiftByZero (S c) (S k) = cong $ shiftByZero c k

shiftTermByZero : (c : Nat) ->
                  (e : Term) ->
                  shiftTerm c Z e = e
shiftTermByZero c (TVar i) = congVar $ shiftByZero c i
shiftTermByZero c (TAbs e) = congAbs $ shiftTermByZero (S c) e
shiftTermByZero c (TApp e1 e2) =
  congApp (shiftTermByZero c e1)
          (shiftTermByZero c e2)
shiftTermByZero c (TRec e1 e2 e3) =
  congRec (shiftTermByZero c e1)
          (shiftTermByZero c e2)
          (shiftTermByZero c e3)
shiftTermByZero c TZero = congZero
shiftTermByZero c (TSucc e) = congSucc $ shiftTermByZero c e
shiftTermByZero c (TPred e) = congPred $ shiftTermByZero c e
shiftTermByZero c (TIfz e1 e2 e3) =
  congIfz (shiftTermByZero c e1)
          (shiftTermByZero c e2)
          (shiftTermByZero c e3)

shiftTwice : (c : Nat) ->
             (d1 : Nat) -> (d2 : Nat) ->
             (k : Nat) ->
             shift c d2 (shift c d1 k) = shift c (d2+d1) k
shiftTwice Z     d1 d2 k     = plusAssociative d2 d1 k
shiftTwice (S c) d1 d2 Z     = Refl
shiftTwice (S c) d1 d2 (S k) = cong $ shiftTwice c d1 d2 k

shiftTermTwice : (c : Nat) ->
                 (d1 : Nat) -> (d2 : Nat) ->
                 (e : Term) ->
                 shiftTerm c d2 (shiftTerm c d1 e) = shiftTerm c (d2+d1) e
shiftTermTwice c d1 d2 (TVar i) = congVar $ shiftTwice c d1 d2 i
shiftTermTwice c d1 d2 (TAbs e) = congAbs $ shiftTermTwice (S c) d1 d2 e
shiftTermTwice c d1 d2 (TApp e1 e2) =
  congApp (shiftTermTwice c d1 d2 e1)
          (shiftTermTwice c d1 d2 e2)
shiftTermTwice c d1 d2 (TRec e1 e2 e3) =
  congRec (shiftTermTwice c d1 d2 e1)
          (shiftTermTwice c d1 d2 e2)
          (shiftTermTwice c d1 d2 e3)
shiftTermTwice c d1 d2 TZero = congZero
shiftTermTwice c d1 d2 (TSucc e) = congSucc $ shiftTermTwice c d1 d2 e
shiftTermTwice c d1 d2 (TPred e) = congPred $ shiftTermTwice c d1 d2 e
shiftTermTwice c d1 d2 (TIfz e1 e2 e3) =
  congIfz (shiftTermTwice c d1 d2 e1)
          (shiftTermTwice c d1 d2 e2)
          (shiftTermTwice c d1 d2 e3)

shiftTermTwice' : (c : Nat) ->
                  (d1 : Nat) -> (d2 : Nat) ->
                  (e : Term) ->
                  shiftTerm c d2 (shiftTerm c d1 e) = shiftTerm c d1 (shiftTerm c d2 e)
shiftTermTwice' c d1 d2 e =
  let eq1  = shiftTermTwice c d1 d2 e
      comm = cong {f = \q => shiftTerm c q e} $ plusCommutative d1 d2
      eq1' = trans eq1 (sym comm)
      eq2  = shiftTermTwice c d2 d1 e
  in trans eq1' (sym eq2)

shiftSwap :  (c1 : Nat) -> (d1 : Nat) ->
             (c2 : Nat) -> (d2 : Nat) ->
             (k : Nat) ->
             shift (c1+d1+c2) d2 (shift c1 d1 k) = shift c1 d1 (shift (c1+c2) d2 k)
shiftSwap Z      Z      c2 d2 k     = Refl
shiftSwap Z      (S d1) c2 d2 k     = cong $ shiftSwap Z d1 c2 d2 k
shiftSwap (S c1) d1     c2 d2 Z     = Refl
shiftSwap (S c1) d1     c2 d2 (S k) = cong $ shiftSwap c1 d1 c2 d2 k

shiftTermSwap : (c1 : Nat) -> (d1 : Nat) ->
                (c2 : Nat) -> (d2 : Nat) ->
                (e : Term) ->
                shiftTerm (c1+d1+c2) d2 (shiftTerm c1 d1 e) =
                  shiftTerm c1 d1 (shiftTerm (c1+c2) d2 e)
shiftTermSwap c1 d1 c2 d2 (TVar i) = congVar $ shiftSwap c1 d1 c2 d2 i
shiftTermSwap c1 d1 c2 d2 (TAbs e) = congAbs $ shiftTermSwap (S c1) d1 c2 d2 e
shiftTermSwap c1 d1 c2 d2 (TApp e1 e2) =
  congApp (shiftTermSwap c1 d1 c2 d2 e1)
          (shiftTermSwap c1 d1 c2 d2 e2)
shiftTermSwap c1 d1 c2 d2 (TRec e1 e2 e3) =
  congRec (shiftTermSwap c1 d1 c2 d2 e1)
          (shiftTermSwap c1 d1 c2 d2 e2)
          (shiftTermSwap c1 d1 c2 d2 e3)
shiftTermSwap c1 d1 c2 d2 TZero = congZero
shiftTermSwap c1 d1 c2 d2 (TSucc e) = congSucc $ shiftTermSwap c1 d1 c2 d2 e
shiftTermSwap c1 d1 c2 d2 (TPred e) = congPred $ shiftTermSwap c1 d1 c2 d2 e
shiftTermSwap c1 d1 c2 d2 (TIfz e1 e2 e3) =
  congIfz (shiftTermSwap c1 d1 c2 d2 e1)
          (shiftTermSwap c1 d1 c2 d2 e2)
          (shiftTermSwap c1 d1 c2 d2 e3)

-- Shifting acts as the identity if the
-- cutoff is set past the typing context:
shiftPastCtx : (k : Nat) ->
               (ctx : Context) ->
               index' k ctx = Just t ->
               (n : Nat) -> (d : Nat) ->
               shift (length ctx + n) d k = k
shiftPastCtx Z     []       Refl _ _ impossible
shiftPastCtx (S _) []       Refl _ _ impossible
shiftPastCtx Z     (s::ctx) prf  n d = Refl
shiftPastCtx (S k) (s::ctx) prf  n d =
  cong $ shiftPastCtx k ctx prf n d

shiftTermPastCtx : (e : Term) ->
                   (ctx : Context) ->
                   Typing ctx e t ->
                   (n : Nat) -> (d : Nat) ->
                   shiftTerm (length ctx + n) d e = e
shiftTermPastCtx (TVar i) ctx (TyVar prf) n d = congVar $ shiftPastCtx i ctx prf n d
shiftTermPastCtx (TAbs e) ctx (TyAbs s ty) n d = congAbs $ shiftTermPastCtx e (s::ctx) ty n d
shiftTermPastCtx (TApp e1 e2) ctx (TyApp ty1 ty2) n d =
  congApp (shiftTermPastCtx e1 ctx ty1 n d)
          (shiftTermPastCtx e2 ctx ty2 n d)
shiftTermPastCtx (TRec e1 e2 e3) ctx (TyRec ty1 ty2 ty3) n d =
  congRec (shiftTermPastCtx e1 ctx ty1 n d)
          (shiftTermPastCtx e2 ctx ty2 n d)
          (shiftTermPastCtx e3 ctx ty3 n d)
shiftTermPastCtx TZero ctx TyZero n d = congZero
shiftTermPastCtx (TSucc e) ctx (TySucc ty) n d = congSucc $ shiftTermPastCtx e ctx ty n d
shiftTermPastCtx (TPred e) ctx (TyPred ty) n d = congPred $ shiftTermPastCtx e ctx ty n d
shiftTermPastCtx (TIfz e1 e2 e3) ctx (TyIfz ty1 ty2 ty3) n d =
  congIfz (shiftTermPastCtx e1 ctx ty1 n d)
          (shiftTermPastCtx e2 ctx ty2 n d)
          (shiftTermPastCtx e3 ctx ty3 n d)

-- End: SEVERAL LEMMAS ABOUT SHIFTING
-------------------------------------

-------------------------------------------
-- Begin: SHIFTING AND SUBSTITUTION COMMUTE

-- The following lemma is a convoluted way of
-- expressing 'k < length ctx'; it is used to
-- address the 'TVar' case in the subsequent
-- lemma.
substVarPastCtx : (k : Nat) ->
                  (ctx : Context) ->
                  index' k ctx = Just t ->
                  subst_var x (length ctx + n) k = TVar k
substVarPastCtx Z     []       Refl impossible
substVarPastCtx (S _) []       Refl impossible
substVarPastCtx Z     (s::ctx) prf  = Refl
substVarPastCtx (S k) (s::ctx) prf  =
  let ih = substVarPastCtx k ctx prf
  in cong {f = \q => shiftTerm 0 1 q} ih

-- Subsituting at a de Bruijn index past the
-- context 'ctx' in which an expression 'e'
-- is typed yields 'e':
substPastCtx : (e : Term) ->
               (ctx : Context) ->
               Typing ctx e t ->
               subst x (length ctx + n) e = e
substPastCtx (TVar i) ctx (TyVar prf) = substVarPastCtx i ctx prf
substPastCtx (TAbs e) ctx (TyAbs s ty) = congAbs $ substPastCtx e (s::ctx) ty
substPastCtx (TApp e1 e2) ctx (TyApp ty1 ty2) =
  congApp (substPastCtx e1 ctx ty1)
          (substPastCtx e2 ctx ty2)
substPastCtx (TRec e1 e2 e3) ctx (TyRec ty1 ty2 ty3) =
  congRec (substPastCtx e1 ctx ty1)
          (substPastCtx e2 ctx ty2)
          (substPastCtx e3 ctx ty3)
substPastCtx TZero ctx TyZero = congZero
substPastCtx (TSucc e) ctx (TySucc ty) = congSucc $ substPastCtx e ctx ty
substPastCtx (TPred e) ctx (TyPred ty) = congPred $ substPastCtx e ctx ty
substPastCtx (TIfz e1 e2 e3) ctx (TyIfz ty1 ty2 ty3) =
  congIfz (substPastCtx e1 ctx ty1)
          (substPastCtx e2 ctx ty2)
          (substPastCtx e3 ctx ty3)

-- A less convoluted way of stating the lemma
-- that is used in the 'TVar' case above:
substVarPastCtx' : (k : Nat) ->
                   subst_var x (S k + n) k = TVar k
substVarPastCtx' Z     = Refl
substVarPastCtx' (S k) = let ih = substVarPastCtx' k
                         in cong {f = \q => shiftTerm 0 1 q} ih

-- Shifting and substituting for a variable commute:
shiftSubstVarComm : (c : Nat) -> (d : Nat) ->  (i : Nat) ->
                    (x : Term) ->
                    (k : Nat) ->
                    shiftTerm c d (subst_var x (c+i) k) = subst_var x (c+d+i) (shift c d k)
--
shiftSubstVarComm Z     Z     i x k = shiftTermByZero Z (subst_var x i k)
--
shiftSubstVarComm Z     (S d) i x k =
  let ih  = shiftSubstVarComm Z d i x k
      ih' = cong {f = \q => shiftTerm Z (S Z) q} ih
      eq  = shiftTermTwice Z d (S Z) (subst_var x i k)
  in trans (sym eq) ih'
--
shiftSubstVarComm (S c)  d    i x Z     = Refl
--
shiftSubstVarComm (S c)  d    i x (S k) =
  let ih  = shiftSubstVarComm c d i x k
      ih' = cong {f = \q => shiftTerm Z (S Z) q} ih
      eq  = shiftTermSwap Z (S Z) c d (subst_var x (c+i) k)
  in trans eq ih'

-- Shifting and substituting in a general term 'e' commute:
shiftTermSubstComm : (c : Nat) -> (d : Nat) -> (i : Nat) ->
                     (x : Term) ->
                     (e : Term) ->
                     shiftTerm c d (subst x (c+i) e) = subst x (c+d+i) (shiftTerm c d e)
--
shiftTermSubstComm c d i x (TVar k) = shiftSubstVarComm c d i x k
shiftTermSubstComm c d i x (TAbs e) = congAbs $ shiftTermSubstComm (S c) d i x e
shiftTermSubstComm c d i x (TApp e1 e2) =
  congApp (shiftTermSubstComm c d i x e1)
          (shiftTermSubstComm c d i x e2)
shiftTermSubstComm c d i x (TRec e1 e2 e3) =
  congRec (shiftTermSubstComm c d i x e1)
          (shiftTermSubstComm c d i x e2)
          (shiftTermSubstComm c d i x e3)
shiftTermSubstComm c d i x TZero = congZero
shiftTermSubstComm c d i x (TSucc e) = congSucc $ shiftTermSubstComm c d i x e
shiftTermSubstComm c d i x (TPred e) = congPred $ shiftTermSubstComm c d i x e
shiftTermSubstComm c d i x (TIfz e1 e2 e3) =
  congIfz (shiftTermSubstComm c d i x e1)
          (shiftTermSubstComm c d i x e2)
          (shiftTermSubstComm c d i x e3)

-- End: SHIFTING AND SUBSTITUTION COMMUTE
-----------------------------------------

-----------------------------------
-- Begin: SWAPPING OF SUBSTITUTIONS

-- Substitution in a shifted variable, below the
-- cutoff 'c' of the 'shift' operation, preserves
-- the variable (modulo shifting):
substVarBelowShift : (c : Nat) -> (n : Nat) ->
                     (k : Nat) ->
                     (x : Term) ->
                     subst_var x c (shift c (S n) k) = TVar (shift c n k)
substVarBelowShift Z     n k     x = Refl
substVarBelowShift (S c) n Z     x = Refl
substVarBelowShift (S c) n (S k) x =
  let ih  = substVarBelowShift c n k x
  in cong {f = shiftTerm Z (S Z)} ih

-- Substitution in a shifted term, below the
-- cutoff 'c' of the 'shift' operation, preserves
-- the term (modulo shifting):
substBelowShiftTerm : (c : Nat) -> (n : Nat) ->
                      (e : Term) ->
                      (x : Term) ->
                      subst x c (shiftTerm c (S n) e) = shiftTerm c n e
substBelowShiftTerm c n (TVar i) x = substVarBelowShift c n i x
substBelowShiftTerm c n (TAbs e) x = congAbs $ substBelowShiftTerm (S c) n e x
substBelowShiftTerm c n (TApp e1 e2) x =
  congApp (substBelowShiftTerm c n e1 x)
          (substBelowShiftTerm c n e2 x)
substBelowShiftTerm c n (TRec e1 e2 e3) x =
  congRec (substBelowShiftTerm c n e1 x)
          (substBelowShiftTerm c n e2 x)
          (substBelowShiftTerm c n e3 x)
substBelowShiftTerm c n TZero x = Refl
substBelowShiftTerm c n (TSucc e) x = cong $ substBelowShiftTerm c n e x
substBelowShiftTerm c n (TPred e) x = cong $ substBelowShiftTerm c n e x
substBelowShiftTerm c n (TIfz e1 e2 e3) x =
  congIfz (substBelowShiftTerm c n e1 x)
          (substBelowShiftTerm c n e2 x)
          (substBelowShiftTerm c n e3 x)

-- Swapping substitutions in the variable with
-- de Bruijn index 'k' does not affect the result:
-- (Note that the typing for 'x' in the empty context
-- ensures that there are no free variables in 'x',
-- which could otherwise be affected by the second
-- substitution of 'y' on the left-hand side of the
-- equation in the conclusion of the lemma.)
substVarSwap : (k : Nat) ->
               (i : Nat) ->
               (x : Term) -> (y : Term) ->
               (Typing [] x t) ->
               subst y i (subst_var x i k) = subst x i (subst_var y (S i) k)
--
substVarSwap Z     Z     x y tyx = substPastCtx x _ tyx {n=0}
--
substVarSwap Z     (S i) x y tyx = Refl
--
substVarSwap (S k) Z     x y tyx =
  case k of
    Z     => let eq1 = substBelowShiftTerm Z Z y x
                 eq2 = shiftTermByZero Z y
             in sym (trans eq1 eq2)
    (S _) => Refl
--
substVarSwap (S k) (S i) x y tyx =
  let ih  = substVarSwap k i x y tyx
      ih' = cong {f = shiftTerm Z (S Z)} ih
      eq1 = shiftTermSubstComm Z (S Z) i y (subst_var x i k)
      eq2 = trans (sym eq1) ih'
      eq3 = shiftTermSubstComm Z (S Z) i x (subst_var y (S i) k)
  in trans eq2 eq3

-- Swapping the order of two substitutions at adjacent
-- de Bruijn indices (indices 'i' and 'S i') preserves
-- the result:
-- (See the comment immediately before the previous
-- lemma for an explanation of why the typing of 'x'
-- in the empty context is needed.)
substSwap : (e : Term) ->
            (i : Nat) ->
            (x : Term) -> (y : Term) ->
            Typing [] x t ->
            subst y i (subst x i e) = subst x i (subst y (S i) e)
--
substSwap (TVar k) i x y tyx = substVarSwap k i x y tyx
substSwap (TAbs e) i x y tyx = congAbs $ substSwap e (S i) x y tyx
substSwap (TApp e1 e2) i x y tyx =
  congApp (substSwap e1 i x y tyx)
          (substSwap e2 i x y tyx)
substSwap (TRec e1 e2 e3) i x y tyx =
  congRec (substSwap e1 i x y tyx)
          (substSwap e2 i x y tyx)
          (substSwap e3 i x y tyx)
substSwap TZero i x y tyx = Refl
substSwap (TSucc e) i x y tyx = congSucc $ substSwap e i x y tyx
substSwap (TPred e) i x y tyx = congPred $ substSwap e i x y tyx
substSwap (TIfz e1 e2 e3) i x y tyx =
  congIfz (substSwap e1 i x y tyx)
          (substSwap e2 i x y tyx)
          (substSwap e3 i x y tyx)

-- End: SWAPPING OF SUBSTITUTIONS
---------------------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
import Resumption

data Bit : Type where
  Zero : Bit
  One  : Bit

xor : [static] Bit -> [static] Bit -> Bit
xor Zero Zero = Zero
xor One One   = Zero
xor _   _     = One

--Bit 8 type synonym
Bit8 : Type
Bit8 = Vect 8 Bit

zeros : Bit8
zeros = Zero :: Zero :: Zero :: Zero :: Zero :: Zero :: Zero :: Zero :: Nil

parity : (Vect (S(n)) Bit) ->  Bit
parity (x :: Nil) = x
parity (x :: xs)  = parity' x xs
  where
    parity' : Bit -> (Vect n Bit) -> Bit
    parity' b Nil = b
    parity' b (x :: xs) = parity' (b `xor` x) xs

device : [static] (a -> b) -> (a -> React a b ())
device f = \i => P (f i) (device f)

s : Bit8 -> React Bit8 Bit ()
s = device parity --zeros

pcrap : Bit
pcrap = parity zeros

max_stars_repo_name: igraves/draconis-resumptions

max_issues_repo_name: igraves/draconis-resumptions

max_forks_repo_name: igraves/draconis-resumptions


text:
-- SPDX-FileCopyrightText: 2021 The toml-idr developers
--
-- SPDX-License-Identifier: MPL-2.0

module Language.TOML.Lexer

import Text.Lexer
import Text.Token

import public Language.TOML.Tokens

%default total

-- TODO this is a valid JSON number, not a TOML float.
-- it's close enough but not correct.
private
floatLit : Lexer
floatLit
  = let sign  = is '-'
        whole = is '0' <|> range '1' '9' <+> many digit
        frac  = is '.' <+> digits
        exp   = like 'e' <+> opt (oneOf "+-") <+> digits in
        opt sign <+> whole <+> opt frac <+> opt exp

-- TODO doesn't handle prefix `+` yet or inline `_`
private
integerLit : Lexer
integerLit = intLit <|> hexLit

private
bareKey : Lexer
bareKey = some (alphaNum <|> is '_' <|> is '-')

-- TODO doesn't handle single quoted strings or escapes yet
private
stringLit : Lexer
stringLit = Text.Lexer.stringLit

private
tomlTokenMap : TokenMap TOMLToken
tomlTokenMap = toTokenMap $
    [
        (newline, TTPunct NewLine),
        (lineComment (is '#'), TTIgnored),
        (spaces, TTIgnored),
        (is ',', TTPunct Comma),
        (is '.', TTPunct Dot),
        (is '=', TTPunct Equal),
        (is '[', TTPunct $ Square Open),
        (is ']', TTPunct $ Square Close),
        (is '{', TTPunct $ Curly Open),
        (is '}', TTPunct $ Curly Close),
        (exact strTrue <|> exact strFalse, TTBoolean),
        (integerLit, TTInt),
        (floatLit, TTFloat),
        (Language.TOML.Lexer.stringLit, TTString), -- TODO doesn't handle all escapes
        (bareKey, TTBare)
    ]

export
lexTOMLTokData : String -> Maybe (List (TokenData TOMLToken))
lexTOMLTokData str =
    case lex tomlTokenMap str of
        (tokens, (_, _, "")) => Just tokens
        _ => Nothing

export
lexTOML : String -> Maybe (List (TOMLToken))
lexTOML str = do
    toks <- lexTOMLTokData str
    pure $ map (.tok) toks

max_stars_repo_name: tiatomee/toml-idr

max_issues_repo_name: tiatomee/toml-idr

max_forks_repo_name: tiatomee/toml-idr


text:
module DepSec

import public DepSec.DIO
import public DepSec.Poset
import public DepSec.Lattice
import public DepSec.Labeled

import public DepSec.File
import public DepSec.Ref

import public DepSec.Declassification

max_stars_repo_name: simongregersen/DepSec

max_issues_repo_name: simongregersen/DepSec

max_forks_repo_name: simongregersen/DepSec


text:
module Util

import Data.Vect
import ProcessLib
import System

%default total

export
(>>): Process iface a s0 s1 -> Process iface b s1 s2 -> Process iface b s0 s2
(>>) x y = do { x ; y }

export
sequence: Vect n (Process iface () s s) -> Process iface () s s
sequence xs = foldr (>>) (Pure ()) xs

export
sleeper: Nat -> Process iface () s s
sleeper Z     = Pure ()
sleeper (S k) = sleeper k >> (Action $ usleep 1000000)

export
dot_sleeper: Nat -> Process iface () s s
dot_sleeper Z = Pure ()
dot_sleeper (S k) = dot_sleeper k >> (do {Action (usleep 1000000); Action (putStrLn ".")})

max_stars_repo_name: jameshaydon/smproc

max_issues_repo_name: jameshaydon/smproc

max_forks_repo_name: jameshaydon/smproc


text:
module CaseAnalysis

import Booleans
import Bltnat

-- By using the commumative property of (+) it is easiest just to write (n + 1) as (1 + n) as beq_nat and (+) pattern match on the 1st argument, thus it can't be an unknown
plusft_com : (n : Nat) -> beq_nat (1 + n) 0 = False
plusft_com n = Refl

-- Or case split on the original
plusft : (n : Nat) -> beq_nat (n + 1) 0 = False
plusft Z = Refl
plusft (S k) = Refl

andb_commutative : (b, c : Bool) -> andb b c = andb c b
andb_commutative False False = Refl
andb_commutative False True = Refl
andb_commutative True False = Refl
andb_commutative True True = Refl

-- Alternative
andbcommutative'rhs_1 : (c : Bool) -> False = andb c False
andbcommutative'rhs_1 False = Refl
andbcommutative'rhs_1 True = Refl

andbcommutative'rhs_2 : (c : Bool) -> c = andb c True
andbcommutative'rhs_2 False = Refl
andbcommutative'rhs_2 True = Refl

andbCommutative : (b, c : Bool) -> andb b c = andb c b
andbCommutative False = andbcommutative'rhs_1
andbCommutative True = andbcommutative'rhs_2

-- Exercise 9.1
andbTelim2F : (c : Bool) -> (prf : andb False c = True) -> c = True
andbTelim2F False prf = prf
andbTelim2F True prf = Refl

andbTelim2T : (c : Bool) -> (prf : andb True c = True) -> c = True
andbTelim2T False prf = prf
andbTelim2T True prf = Refl

andbTelim2 : (b, c : Bool) -> (andb b c = True) -> c = True
andbTelim2 False c prf = andbTelim2F c prf
andbTelim2 True c prf = andbTelim2T c prf

-- Exercise 9.2
zeroNbeqPlusZ : False = False
zeroNbeqPlusZ = Refl

zeroNbeqPlus1S : (k : Nat) -> False = False
zeroNbeqPlus1S k = Refl

zeroNbeqPlus1 : (n : Nat) -> beq_nat 0 (n + 1) = False
zeroNbeqPlus1 Z = zeroNbeqPlusZ
zeroNbeqPlus1 (S k) = zeroNbeqPlus1S k


text:
module Modulo

import Data.Fin

%access export
%default total

add : Fin k -> Fin k -> Fin k
add {k=S k} n m = restrict k $ finToInteger n + finToInteger m

negate : Fin k -> Fin k
negate {k=S k} n = restrict k $ toIntegerNat (S k) - finToInteger n

subt : Fin k -> Fin k -> Fin k
subt {k=S k} n m = restrict k $ finToInteger n - finToInteger m + toIntegerNat (S k)

mult : Fin k -> Fin k -> Fin k
mult {k=S k} n m = restrict k $ finToInteger n * finToInteger m

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Libraries.Text.PrettyPrint.Prettyprinter.Render.String

import Data.String
import Libraries.Data.String.Extra
import Libraries.Text.PrettyPrint.Prettyprinter.Doc

%default total

export
renderString : SimpleDocStream ann -> String
renderString SEmpty = neutral
renderString (SChar c rest) = singleton c <+> renderString rest
renderString (SText l t rest) = t <+> renderString rest
renderString (SLine l rest) = singleton '\n' <+> textSpaces l <+> renderString rest
renderString (SAnnPush ann rest) = renderString rest
renderString (SAnnPop rest) = renderString rest

export
renderIO : SimpleDocStream ann -> IO ()
renderIO SEmpty = pure ()
renderIO (SChar c rest) = do putChar c; renderIO rest
renderIO (SText l t rest) = do putStr t; renderIO rest
renderIO (SLine l rest) = do putChar '\n'
                             putStr (textSpaces l)
                             renderIO rest
renderIO (SAnnPush ann rest) = renderIO rest
renderIO (SAnnPop rest) = renderIO rest

||| Prettyprints a document to standard output, using default options.
export
putDoc : Doc ann -> IO ()
putDoc = renderIO . layoutPretty defaultLayoutOptions


text:
module Echo

import Control.Monad.Trans
import Data.Buffer
import Data.Buffer.Ext
import Node
import Node.HTTP.Client
import Node.HTTP.Server
import TyTTP.Adapter.Node.HTTP as HTTP
import TyTTP.Core.Error
import TyTTP.HTTP
import TyTTP.HTTP.Combinators

hReflect : Context Method String StringHeaders Status StringHeaders (Publisher IO NodeError Buffer) ()
  -> IO $ Context Method String StringHeaders Status StringHeaders (Publisher IO NodeError Buffer) (Publisher IO NodeError Buffer)
hReflect ctx = do
  let m = ctx.request.method
      h = ctx.request.headers
      p : Publisher IO NodeError Buffer = MkPublisher $ \s => do
        s.onNext $ fromString "method -> \{show m}"
        s.onNext $ fromString "url -> \{ctx.request.url}"
        s.onNext "headers ->"
        for_ h $ \v => s.onNext $ fromString "\t\{fst v} : \{snd v}"
        s.onNext "body ->"
        ctx.request.body.subscribe s
  pure $ { response.body := p } ctx

main : IO ()
main = do
  http <- require
  server <- HTTP.listen' { e = NodeError } :> hReflect

  defer $ do
    ignore $ http.get "http://localhost:3000" $ \res => do
      putStrLn "GET"
      putStrLn res.statusCode
      onData res putStrLn

  defer $ do
    clientReq <- http.post "http://localhost:3000/the/resource" $ \res => do
      putStrLn "POST"
      putStrLn res.statusCode
      onData res putStrLn
      server.close

    clientReq.write "Hello World!"
    clientReq.write "With more chunks"
    clientReq.end

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
import Data.Vect

removeElem : (value : a) ->
             (xs : Vect (S n) a) ->
             (prf : Elem value xs) ->
             Vect n a
removeElem value (value :: ys) Here = ys
removeElem {n = Z} value (y :: []) (There later) = absurd later
removeElem {n = (S k)} value (y :: ys) (There later)
                                          = y :: removeElem value ys later


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

%name Vect xs, ys, zs

append : Vect n a -> Vect m a -> Vect (n + m) a
append {n} xs ys = ?foo

vadd : Num a => Vect n a -> Vect n a -> Vect n a
vadd [] ys = ?bar
vadd (x :: xs) ys = ?baz

suc : (x : Nat) -> (y : Nat) -> x = y -> S x = S y
suc x y prf = ?quux

suc' : x = y -> S x = S y
suc' {x} {y} prf = ?quuz


text:
module Vimscript.Builtins

import Vimscript.FFI
import Vimscript.List

%access public export
%default total

-- Note [Inline FStr]
--
-- For all functions operating on Vim mutable references, a %inline
-- annotation is a must:
--
-- This function *must* be given a %inline annotation, otherwise the
-- `name` is not reduced sufficiently during compilation and remains
-- an FCon instead of becoming an FStr.

%inline
echo : (x : t) -> VIM_IO ()
echo {t} v = foreign FFI_VIM VIM_Echo (Raw t -> VIM_IO ()) (MkRaw v)

||| Call a Vim builtin.
%inline
builtin : String -> (ty : Type) -> {auto fty : FTy FFI_VIM [] ty} -> ty
builtin name =
  foreign FFI_VIM (VIM_BuiltIn name)

||| Read the value of a Vim mutable reference.
%inline
readMutableRef : (ref : VIM_MutableRef) -> (name : String) -> VIM_IO String
readMutableRef ref name =
  foreign FFI_VIM (VIM_Get ref name) (VIM_IO String)

||| Write the value of a Vim mutable reference.
%inline
writeMutableRef : (ref : VIM_MutableRef) -> (name : String) -> (x : t) -> VIM_IO ()
writeMutableRef {t} ref name x =
  foreign FFI_VIM (VIM_Set ref name) (Raw t -> VIM_IO ()) (MkRaw x)

||| Read the value of a Vim option with unspecified scope (`&foo`).
%inline
readOption : (name : String) -> VIM_IO String
readOption name = readMutableRef VIM_Option name

||| Write the value of a Vim option with unspecified scope (`&foo`).
%inline
writeOption : (name : String) -> (x : t) -> VIM_IO ()
writeOption name x = writeMutableRef VIM_Option name x

||| Read the value of a Vim option with global scope (`&l:foo`).
%inline
readLocalOption : (name : String) -> VIM_IO String
readLocalOption name = readMutableRef VIM_LocalOption name

||| Write the value of a Vim option with global scope (`&l:foo`).
%inline
writeLocalOption : (name : String) -> (x : t) -> VIM_IO ()
writeLocalOption name x = writeMutableRef VIM_LocalOption name x

||| Read the value of a Vim option with global scope (`&g:foo`).
%inline
readGlobalOption : (name : String) -> VIM_IO String
readGlobalOption name = readMutableRef VIM_GlobalOption name

||| Write the value of a Vim option with global scope (`&g:foo`).
%inline
writeGlobalOption : (name : String) -> (x : t) -> VIM_IO ()
writeGlobalOption name x = writeMutableRef VIM_GlobalOption name x

||| Read the contents of a Vim register.
%inline
readRegister : (name : String) -> VIM_IO String
readRegister name = readMutableRef VIM_Register name

||| Set the contents of a Vim register.
%inline
writeRegister : (name : String) -> (x : t) -> VIM_IO ()
writeRegister name = writeMutableRef VIM_Register name

||| Execute a string as Vimscript.
%inline
execute : String -> VIM_IO ()
execute = builtin "execute" (String -> VIM_IO ())

-- [ Vim builtins ] ------------------------------------------------------------

%inline
line : String -> VIM_IO Int
line = builtin "line" (String -> VIM_IO Int)

%inline
col : String -> VIM_IO Int
col = builtin "col" (String -> VIM_IO Int)

%inline
getline : Int -> VIM_IO String
getline = builtin "getline" (Int -> VIM_IO String)

%inline
appendLines : Int -> VimList String -> VIM_IO ()
appendLines i l =
  builtin "append" (Int -> Raw (VimList String) -> VIM_IO ()) i (MkRaw l)

-- %inline
-- putStr : String -> VIM_IO ()
-- putStr str = execute ("echomsg" ++ " " ++ str)

-- %inline
-- putErr : String -> VIM_IO ()
-- putErr str = execute ("echoerr" ++ " " ++ str)

%inline
match : String -> String -> Int
match str regexp = unsafePerformIO
    (builtin "match" (String -> String -> VIM_IO Int) str regexp)

%inline
matchstr : String -> String -> String
matchstr str regexp = unsafePerformIO
    (builtin "matchstr" (String -> String -> VIM_IO String) str regexp)

%inline
shellescape : String -> String
shellescape str = unsafePerformIO
    (builtin "shellescape" (String -> VIM_IO String) str)

%inline
toupper : String -> String
toupper str = unsafePerformIO
    (builtin "toupper" (String -> VIM_IO String) str)

%inline
tolower : String -> String
tolower str = unsafePerformIO
    (builtin "tolower" (String -> VIM_IO String) str)

||| Compute the length of a string.
%inline
strlen : String -> Int
strlen str = unsafePerformIO
    (builtin "strlen" (String -> VIM_IO Int) str)

||| Extract a substring from a start index to an end index.
%inline
strpart : String -> (start : Int) -> (end : Int) -> String
strpart str start end = unsafePerformIO
    (builtin "strpart" (String -> Int -> Int -> VIM_IO String) str start end)

||| Extract a substring from a start index to the (implicit) end.
%inline
strpart' : String -> (start : Int) -> String
strpart' str start = unsafePerformIO
    (builtin "strpart" (String -> Int -> VIM_IO String) str start)

||| Access Vim's built-in globbing functionality.
|||
||| Current file name:
||| ```idris
||| expand '%'
||| ```
|||
||| Word under cursor:
||| ```idris
||| expand '<cword>'
||| ```
expand : String -> VIM_IO String
expand str = builtin "expand" (String -> VIM_IO String) str

cursor : (line : Int) -> (col : Int) -> VIM_IO ()
cursor line col = builtin "cursor" (Int -> Int -> VIM_IO ()) line col

getcwd : VIM_IO String
getcwd = builtin "getcwd" (VIM_IO String)

||| Execute a shell command and discard the output.
system_ : String -> VIM_IO ()
system_ = builtin "system" (String -> VIM_IO ())

-- [ Derived operations ] ------------------------------------------------------

||| Set a Vim option of the form `setting=value`. Type-unsafe.
%inline
unsafeSetUnary : String -> String -> VIM_IO ()
unsafeSetUnary o v = execute ("set " ++ o ++ "=" ++ v)

-- [Ex commands] ---------------------------------------------------------------

split : VIM_IO ()
split = execute "split"

vsplit : VIM_IO ()
vsplit = execute "vsplit"

-- %inline
-- getpos : (mark : String) -> VIM_IO ()
-- getpos = builtin "line" (String -> VIM_IO Int)

public export
Regex : Type
Regex = String

public export
Filename : Type
Filename = String

public export
FlagSet : Type
FlagSet = String

public export
Range : Type
Range = String

entireFile : Range
entireFile = "%"

currentLine : Range
currentLine = "."

lineNum : Int -> Range
lineNum = show

lastLine : Range
lastLine = "$"

noFlags : FlagSet
noFlags = ""

public export
data Line = Last

public export
data SubRepeatFlag = UseLastSearch | GlobalReplace

public export
data Ex
  = Delete
  | Write (Maybe Filename)
  | Sub Range Regex String FlagSet
  | SubRepeat (List SubRepeatFlag)
  | Global Regex Ex
  | VGlobal Regex Ex
  | Move (Maybe Range) Line
  | Undo

ppSubRepeatFlag : SubRepeatFlag -> String
ppSubRepeatFlag UseLastSearch = "r"
ppSubRepeatFlag GlobalReplace = "g"

ppLine : Line -> String
ppLine Last = "$"

ppRange : Maybe Range -> String
ppRange Nothing = ""
ppRange (Just r) = r

ppEx : Ex -> String
ppEx Delete = "d"
ppEx (SubRepeat fs) = "s" ++ (concat (map ppSubRepeatFlag fs))
ppEx (Sub r re s f) = r ++ "s/" ++ re ++ "/" ++ s ++ "/" ++ f
ppEx (Write f)
  = case f of
         Nothing => "w"
         Just x => "w " ++ x
ppEx (Global re a) = "g/" ++ re ++ "/" ++ ppEx a
ppEx (VGlobal re a) = "v/" ++ re ++ "/" ++ ppEx a
ppEx (Move r l) = ppRange r ++ "m" ++ ppLine l
ppEx Undo = "u"

exec : Ex -> VIM_IO ()
exec = execute . ppEx

sub : Range -> Regex -> String -> FlagSet -> VIM_IO ()
sub r re s fs = exec (Sub r re s fs)

sub' : Range -> Regex -> String -> VIM_IO ()
sub' r re s = sub r re s noFlags

-- TODO escaping
global : Regex -> Ex -> VIM_IO ()
global re a = exec (Global re a)

vglobal : Regex -> Ex -> VIM_IO ()
vglobal re a = exec (VGlobal re a)

v : Regex -> Ex -> VIM_IO ()
v = vglobal

g : Regex -> Ex -> VIM_IO ()
g = global

d : Ex
d = Delete

-- m$
moveEnd : Ex
moveEnd = Move Nothing Last

public export
data VimSwitch
  = No VimSwitch
  | Compatible
  | ExpandTab
  | Hidden
  | Wildmenu
  | RelativeNumber
  | UndoFile
  | VisualBell

ppSwitch : VimSwitch -> String
ppSwitch vs =
  case vs of
       Compatible     => "compatible"
       No o           => "no" ++ ppSwitch o
       ExpandTab      => "expandtab"
       Hidden         => "hidden"
       Wildmenu       => "wildmenu"
       RelativeNumber => "relativenumber"
       UndoFile       => "undofile"
       VisualBell     => "visualbell"

enable : VimSwitch -> VIM_IO ()
enable s = execute ("set" ++ " " ++ ppSwitch s)

disable : VimSwitch -> VIM_IO ()
disable s = enable (No s)

data Power = On | Off

private
ppPower : Power -> String
ppPower p = case p of
                 On => "on"
                 Off => "off"

data VimEncoding = UTF8

private
ppVimEncoding : VimEncoding -> String
ppVimEncoding e =
  case e of
       UTF8 => "utf8"

data VimBackground = Light | Dark

private
ppVimBackground : VimBackground -> String
ppVimBackground bg =
  case bg of
       Light => "light"
       Dark => "dark"

data VimOption
  = Syntax Power
  | TabStop Int
  | SoftTabStop Int
  | ShiftWidth Int
  | Encoding VimEncoding
  | Background VimBackground
  | StatusLine String

set : VimOption -> VIM_IO ()
set opt =
  case opt of
       Syntax p => unsafeSetUnary "syntax" (ppPower p)
       TabStop n => unsafeSetUnary "tabstop" (show n)
       SoftTabStop n => unsafeSetUnary "softtabstop" (show n)
       ShiftWidth n => unsafeSetUnary "shiftwidth" (show n)
       Encoding e => unsafeSetUnary "encoding" (ppVimEncoding e)
       Background bg => unsafeSetUnary "background" (ppVimBackground bg)
       StatusLine s => unsafeSetUnary "statusline" s

max_stars_repo_name: owickstrom/idris-vimscript

max_issues_repo_name: owickstrom/idris-vimscript

max_forks_repo_name: owickstrom/idris-vimscript


text:
module LetBinders

infix 1 :::
record List1 (a : Type) where
  constructor (:::)
  head : a
  tail : List a

swap : List1 a -> List1 a
swap aas =
  let (a ::: as) := aas in
  let (b :: bs) = as
        | [] => a ::: []
      rest = a :: bs
  in b ::: rest

identity : List (Nat, a) -> List (List a)
identity =
  let

    replicate : (n : Nat) -> a -> List a
    replicate Z a = []
    replicate (S n) a = a :: replicate n a

    closure := uncurry replicate

  in map closure


text:
module Network.HTTP.Scheduler

import Network.HTTP.Message
import Network.HTTP.Error
import Network.HTTP.Protocol
import Network.HTTP.Header
import Utils.Streaming
import System.Concurrency
import Data.List1
import Data.Compress.Interface
import Data.Compress.GZip
import Data.Compress.ZLib

public export
record ScheduleResponse (e : Type) (m : Type -> Type) where
  constructor MkScheduleResponse
  raw_http_response : HttpResponse
  content : Channel (Either (HttpError e) (Maybe (List Bits8)))

public export
record ScheduleRequest (e : Type) (m : Type -> Type) where
  constructor MkScheduleRequest
  raw_http_message : RawHttpMessage
  content : Stream (Of Bits8) m (Either e ())
  response : Channel (Either (HttpError e) (ScheduleResponse e m))

public export
interface Scheduler (e : Type) (m : Type -> Type) (0 a : Type) where
  ||| Schedule a HTTP request
  schedule_request : a -> Protocol -> ScheduleRequest e m -> m ()
  ||| Evict all HTTP connections, returning scheduler to a clean state (and closing all resources)
  evict_all : a -> m ()

channel_to_stream : (HasIO m, Decompressor c) => c -> Channel (Either (HttpError e) (Maybe (List Bits8))) ->
                    Stream (Of Bits8) m (Either (HttpError e) ())
channel_to_stream decomp channel = do
  Right (Just content) <- liftIO $ channelGet channel
  | Right Nothing =>
      case done decomp of
        Right [] => pure (Right ())
        Right xs => pure (Left $ DecompressionError "\{show $ length xs} leftover bytes in decompression buffer")
        Left err => pure (Left $ DecompressionError err)
  | Left err => pure (Left err)
  let Right (content, decomp) = feed decomp content
  | Left err => pure (Left $ DecompressionError err)
  fromList_ content *> channel_to_stream decomp channel

decompressor : List ContentEncodingScheme -> DPair Type Decompressor
decompressor [ GZip ] = MkDPair GZipState %search
decompressor [ Deflate ] = MkDPair ZLibState %search
decompressor _ = MkDPair IdentityState %search

to_list : Maybe (List1 a) -> List a
to_list Nothing = []
to_list (Just (x ::: xs)) = x :: xs

public export
start_request : {m, e : _} -> (HasIO m, Scheduler e m scheduler) =>
          scheduler ->
          Protocol ->
          RawHttpMessage ->
          Stream (Of Bits8) m (Either e ()) ->
          m (Either (HttpError e) (HttpResponse, Stream (Of Bits8) m (Either (HttpError e) ())))
start_request scheduler protocol msg content = do
  mvar <- makeChannel
  schedule_request scheduler protocol $ MkScheduleRequest msg content mvar
  Right response <- channelGet mvar
  | Left err => pure $ Left err
  let (encoding ** wit) = decompressor $ to_list $ lookup_header response.raw_http_response.headers ContentEncoding
  pure $ Right (response.raw_http_response, channel_to_stream (init @{wit}) response.content)


text:
module SQLite3.Direct.Streaming

import public SQLite3.Direct
import public Streaming
import public Control.Monad.Either
import Control.Monad.Trans

export
get_rows : HasIO m => Handle -> Stmt -> {xs : _} -> All Column xs -> Stream (Of (HList xs)) (EitherT Error m) ()
get_rows handle stmt columns = do
  True <- lift $ MkEitherT $ step handle stmt
  | False => pure ()
  row <- lift $ MkEitherT $ get_row handle stmt columns
  yield row
  get_rows handle stmt columns


text:
module NoCo

nats : Stream Nat
nats = Z :: map S nats

record Foo : Type where
  MkFoo : (bar : Bool) -> (baz : if bar then Nat else Bool) -> Foo

max_stars_repo_name: sualitu/thesis

max_issues_repo_name: sualitu/thesis

max_forks_repo_name: sualitu/thesis


text:
||| Dependently typed implementation of an Integer Map based on
||| _big-endian_ Patricia trees. Dependent types are used to encode
||| bit size of keys and to enforce some invariants for data structure.
|||
||| Algorithm is taken from Chris Okasaki and Andy Gill,
||| "Fast Mergeable Integer Maps", Workshop on ML, September 1998, pages 77-86.
||| Some implementation details are taken from
||| [Haskell implementation](http://hackage.haskell.org/package/containers-0.5.10.1/docs/Data-IntMap.html).
|||
||| Most functions have `O(min(n, W))` running time, where `n` is number of elements
||| and `W` is size of bits to store key.

module Patricia.IntMap

import Data.Bits
import Data.Fin

import Patricia.BitsUtils

%default total
%access export

||| The core patricia tree data structure used to represent integer key-value map.
|||
||| @bits  Number of bits in `key`.
||| @valTy The type associated with the value.
public export
data IntBitMap : (bits : Nat) -> (valTy : Type) -> Type where
    ||| An empty `IntBitMap` node.
    Empty : IntBitMap (S n) v

    ||| A Leaf node in the Tree.
    |||
    ||| @n     Number of bits in key.
    ||| @key   The key: integer of `n` bits.
    ||| @val   The value associated with the key.
    Leaf : (key : Bits (S n))
        -> (val : v)
        -> IntBitMap (S n) v

    ||| A binary node in the tree.
    |||
    ||| *Invariant:* `Empty` is never found as a child of `Bin`. TODO: encode this
    |||
    ||| @n        Number of bits in key.
--    ||| @leftPrf  Proof that left  subtree is not `Empty`
--    ||| @rightPrf Proof that right subtree is not `Empty`
    ||| @pref     The common high-order bits that all elements share to the left of
    |||           the `brBit` bit. Bit at `brBit` is set to `0` and all the lesser bits to `1`.
    ||| @brBit    The largest bit position in `pref` at which two elements of the set differ.
    ||| @left     The left child of the Binary Node.
    ||| @right    The right child of the Binary Node.
    Bin : -- {auto leftPrf  : NonEmptyPatricia left}
          -- {auto rightPrf : NonEmptyPatricia right}
          (pref  : Bits (S n))
       -> (brBit : Fin (S n))
       -> (left  : IntBitMap (S n) v)
       -> (right : IntBitMap (S n) v)
       -> IntBitMap (S n) v

--    ||| Invariant for `IntBitMap` that it's not empty.
--    |||
--    ||| @tree Tree for which invariant holds.
--    data NonEmptyPatricia : (tree : IntBitMap n v) -> Type where
--        ||| Invariant for `Leaf` constructor.
--        NonEmptyLeaf : NonEmptyPatricia (Leaf key val)
--
--        ||| Invariant for `Bin` constructor.
--        |||
--        ||| @left     Implicit param for left subtree.
--        ||| @right    Implicit param for right subtree.
--        ||| @leftPrf  Proof that @left subtree is not empty.
--        ||| @rightPrf Proof that @right subtree is not empty.
--        NonEmptyBin  : {left  : IntBitMap (S n) v}
--                    -> {right : IntBitMap (S n) v}
--                    -> (leftPrf  : NonEmptyPatricia left)
--                    -> (rightPrf : NonEmptyPatricia right)
--                    -> NonEmptyPatricia (Bin pref bit left right)

%name IntBitMap t, tree

-- TODO: not total?
-- Uninhabited (NonEmptyPatricia Empty) where
--     uninhabited NonEmptyLeaf impossible
--     uninhabited (NonEmptyBin _ _) impossible

Functor (IntBitMap (S n)) where
    map _ Empty                       = Empty
    map f (Leaf key val)              = Leaf key (f val)
    map f (Bin pref brBit left right) = Bin pref brBit (map f left) (map f right)

Foldable (IntBitMap (S n)) where
    foldr _ acc Empty                = acc
    foldr f acc (Leaf _ val)         = f val acc
    foldr f acc (Bin _ _ left right) = foldr f (foldr f acc right) left

||| Integer map with 32 bits integers as a key.
public export
Int32Map : (valTy : Type) -> Type
Int32Map v = IntBitMap 32 v

||| `O(n)`. Number of elements in `IntBitMap`.
public export
size : IntBitMap (S n) v -> Nat
size Empty = 0
size (Leaf _ _) = 1
size (Bin _ _ left right) = size left + size right

||| `O(min(n, W))`. Lookup the value at a key in the `IntBitMap`.
public export
lookup : Integer -> IntBitMap (S n) v -> Maybe v
lookup {n} key t with (intToBits {n=S n} key)
  lookup {n} key t | bitKey = go t where
    go : IntBitMap (S n) v -> Maybe v
    go Empty = Nothing
    go (Leaf treeKey val) = if treeKey == bitKey then Just val else Nothing
    go (Bin pref _ left right) = if bitKey <= pref  -- we can compare `key` with `pref` because of BE patricia trees
                                 then go left
                                 else go right

||| `O(W)`. Joins two nodes into one tree, creating `Bin` node.
||| Both nodes should be not `Empty`.
private
joinNodes : IntBitMap (S n) v -> IntBitMap (S n) v -> IntBitMap (S n) v
joinNodes Empty _ = Empty  -- TODO: ensure at compile time
joinNodes _ Empty = Empty  -- TODO: ensure at compile time
joinNodes {n} t1 t2 = let bBit     = branchingBit pref1 pref2
                          prefMask = maskInsignificant bBit pref1
                      in if isZeroBit bBit pref1
                         then Bin prefMask bBit t1 t2
                         else Bin prefMask bBit t2 t1
  where
    pref : IntBitMap (S n) v -> Bits (S n)
    pref Empty = cast 0  -- TODO: ensure this never happens
    pref (Leaf key _) = key
    pref (Bin p _ _ _) = p

    pref1 : Bits (S n)
    pref1 = pref t1

    pref2 : Bits (S n)
    pref2 = pref t2

||| `O(min(n,W))`. Insert a new `(key,value)` pair in the `IntBitMap`.
||| If the key is already present in the map, the associated value is
||| replaced with the supplied value.
public export
insert : Integer -> v -> IntBitMap (S n) v -> IntBitMap (S n) v
insert {n} key val t with (intToBits {n=S n} key)
  insert {n} key val t | bitKey = go t where
    go : IntBitMap (S n) v -> IntBitMap (S n) v
    go Empty = Leaf bitKey val

    go lf@(Leaf oldKey oldVal) =
        if oldKey == bitKey
        then Leaf bitKey val
        else joinNodes lf (Leaf bitKey val)

    go br@(Bin pref brBit left right) =
        if matchPrefix brBit pref bitKey
        then if isZeroBit brBit bitKey  -- bitKey <= pref
             then Bin pref brBit (go left) right
             else Bin pref brBit left (go right)
        else joinNodes br (Leaf bitKey val)

||| `O(min(n,W))`. Delete `key` with corresponding `value` from `IntBitMap`.
||| If the key is not present in the map, the tree isn't changed.
public export
delete : Integer -> IntBitMap (S n) v -> IntBitMap (S n) v
delete {n} key t with (intToBits {n=S n} key)
  delete {n} key t | bitKey = go t where
    go : IntBitMap (S n) v -> IntBitMap (S n) v
    go Empty = Empty
    go lf@(Leaf oldKey val) = if oldKey == bitKey then Empty else lf
    go (Bin pref _ left right) =
       if bitKey <= pref then case go left of
           Empty => right
           tree  => joinNodes tree right
       else case go right of
           Empty => left
           tree  => joinNodes left tree

||| Create `IntBitMap` from list of `(key, value)`.
public export
fromList : List (Integer, v) -> IntBitMap (S n) v
fromList = foldl insertKeyValPair Empty where
  insertKeyValPair : IntBitMap (S n) v -> (Integer, v) -> IntBitMap (S n) v
  insertKeyValPair tree (key, val) = insert key val tree

values : IntBitMap (S n) v -> List v
values = toList

max_stars_repo_name: ChShersh/idris-persistent-array

max_issues_repo_name: ChShersh/idris-patricia

max_forks_repo_name: ChShersh/idris-persistent-array


text:
||| The Core Computation Context.
|||
||| Borrowed from Idris2 `Rug` is the core computation context that
||| brings the computations together.
module Toolkit.TheRug

import System
import System.File
import System.Clock
import Data.Vect
import Data.String

import Decidable.Equality

import Text.Parser
import Text.Lexer

import Toolkit.System
import Toolkit.Text.Parser.Run
import Toolkit.Data.Location
import Toolkit.Text.Lexer.Run

import Toolkit.Data.DList
import Toolkit.Decidable.Informative

%default total

||| Because it ties everything together.
export
record TheRug e t where
  constructor MkTheRug
  rugRun : IO (Either e t)

export
run : (whenErr : e -> IO b)
   -> (whenOK  : a -> IO b)
   -> (prog    : TheRug e a)
                   -> IO b
run whenErr whenOK (MkTheRug rugRun)
  = either whenErr
           whenOK
           !rugRun

export
%inline
fail : (msg : e)
           -> TheRug e a
fail e
  = MkTheRug (pure (Left e))

export
%inline
throw : (msg : e) -> TheRug e a
throw = fail

export
%inline
map : (a -> b)
    -> TheRug e a
    -> TheRug e b
map f (MkTheRug a)
  = MkTheRug (map (map f) a)

export
%inline
ignore : TheRug e a -> TheRug e ()
ignore
  = map (\_ => ())

export
%inline
embed : (this : IO       a)
             -> TheRug e a
embed op
  = MkTheRug (do o <- op
                 pure (Right o))

export
%inline
embed_ : (this : IO        a)
              -> TheRug e ()
embed_ this = ignore (embed this)

export
%inline
(>>=) : TheRug       e a
     -> (a -> TheRug e b)
     -> TheRug e b
(>>=) (MkTheRug act) f
  = MkTheRug (act >>=
             (\res =>
                case res of
                  Left  err => pure (Left err)
                  Right val => rugRun (f val)))

export
%inline
(>>) : TheRug e ()
    -> TheRug e a
    -> TheRug e a
(>>) ma mb = ma >>= const mb

export
%inline
pure : a -> TheRug e a
pure x = MkTheRug (pure (pure x))

export
(<*>) : TheRug e (a -> b)
     -> TheRug e  a
     -> TheRug e       b
(<*>) (MkTheRug f)
      (MkTheRug a) = MkTheRug [| f <*> a |]

export
(*>) : TheRug e a
    -> TheRug e b
    -> TheRug e b
(*>) (MkTheRug a)
     (MkTheRug b) = MkTheRug [| a *> b |]

export
(<*) : TheRug e a
    -> TheRug e b
    -> TheRug e a
(<*) (MkTheRug a)
     (MkTheRug b) = MkTheRug [| a <* b |]

export
%inline
when : (test : Bool)
    -> Lazy (TheRug e ())
    -> TheRug e ()
when False _
  = pure ()

when True f
  = f

export
%inline
tryCatch : (onErr : ea -> eb)
        -> (prog  : TheRug ea a)
                 -> TheRug eb a
tryCatch onErr prog
  = MkTheRug (run (pure . Left . onErr)
                  (pure . Right)
                  prog)

namespace Decidable
  export
  %inline
  embed : (err : b)
       -> (result : Dec      r)
                 -> TheRug b r
  embed _ (Yes prfWhy)
    = pure prfWhy

  embed err (No prfWhyNot)
    = throw err

  export
  %inline
  when : (result : Dec      a)
      -> (this   : Lazy (TheRug e ()))
                   -> TheRug e ()
  when (Yes _) this
    = this
  when (No _) _
    = pure ()

  export
  %inline
  whenNot : (result : Dec      r)
         -> (this   : Lazy (TheRug e ()))
                   -> TheRug e ()
  whenNot (Yes _) _
    = pure ()
  whenNot (No _) this
    = this

  namespace Informative
    export
    %inline
    embed : (f : a -> b)
         -> (result : DecInfo a r)
                   -> TheRug  b r
    embed f (Yes prfWhy)
      = pure prfWhy

    embed f (No msgWhyNot prfWhyNot)
      = throw (f msgWhyNot)

namespace Traverse

  namespace List

    traverse' : (acc : List b)
             -> (f   : a -> TheRug e b)
             -> (xs  : List a)

                    -> TheRug e (List b)
    traverse' acc f []
      = pure (reverse acc)

    traverse' acc f (x :: xs)
      = traverse' (!(f x) :: acc) f xs

    export
    %inline
    traverse : (f  : a -> TheRug e b)
            -> (xs : List a)
                  -> TheRug e (List b)
    traverse = traverse' Nil

  namespace Vect
    export
    %inline
    traverse : (f  : a -> TheRug e b)
            -> (xs : Vect n a)
                  -> TheRug e (Vect n b)
    traverse f []
      = pure Nil

    traverse f (x :: xs)
      = [| f x :: traverse f xs |]

namespace IO
  export
  %inline
  putStr : (s : String)
             -> TheRug e ()
  putStr = (TheRug.embed . putStr)

  export
  %inline
  putStrLn : (s : String)
               -> TheRug e ()
  putStrLn = (TheRug.embed . putStrLn)

  export
  %inline
  print : Show a
       => (this : a)
               -> TheRug e ()
  print = (TheRug.embed . print)

  export
  %inline
  printLn : Show a
         => (this : a)
                 -> TheRug e ()
  printLn = (TheRug.embed . printLn)

  export
  covering -- not my fault
  readFile : (onErr : String -> FileError -> e)
          -> (fname : String)
                   -> TheRug e String
  readFile onErr fname
    = do Right content <- (TheRug.embed (readFile fname))
           | Left err => throw (onErr fname err)
         pure content

namespace Parsing
  export
  covering -- not my fault
  parseFile : {e     : _}
           -> (onErr : ParseError a -> err)
           -> (lexer : Lexer a)
           -> (rule  : Grammar () a e ty)
           -> (fname : String)
                    -> TheRug err ty
  parseFile onErr lexer rule fname
      = do Right res <- TheRug.embed (parseFile lexer rule fname)
                 | Left err => throw (onErr err)
           pure res

namespace Cheap
  export
  %inline
  log : (msg      : String)
                 -> TheRug e ()
  log = putStrLn

  namespace Timed
    export
    %inline
    log : (showTime : Bool)
       -> (time     : Lazy (Clock type))
       -> (msg      : String)
                   -> TheRug e ()
    log showTime t m
      = if showTime
        then do print t
                putStrLn m
        else putStrLn m

    export
    %inline
    try : Show e
       => (showTime : Bool)
       -> (msg      : String)
       -> (f        : a -> TheRug e b)
       -> (val      : a)
                   -> TheRug e b
    try showTime msg f val
      = do start <- (embed $ clockTime UTC)
           res   <- embed  (run (\err => do stop <- clockTime UTC
                                            putStrLn "Error Happened"
                                            let d = timeDifference stop start
                                            if showTime
                                              then do putStrLn (unwords [msg, show d])
                                                      printLn err
                                                      exitFailure
                                              else do putStrLn msg
                                                      printLn err
                                                      exitFailure)
                                (\res => do stop <- clockTime UTC
                                            let d = timeDifference stop start
                                            if showTime
                                              then do putStrLn (unwords [msg, show d])
                                                      pure res
                                              else do putStrLn msg
                                                      pure res)

                                (f val))
           pure res

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
module Graph

import Data.List
import Data.List.Quantifiers

-- Notes on a theory of graphs
-- Greg Meredith
-- https://stackedit.io/editor#!provider=couchdb&id=UdUSSGCZgNDxSIPYmMfoX5Kk

%default total

Disjoint : (xs, ys : List a) -> Type
Disjoint xs ys = All (\y => Not (Elem y xs)) ys

-- TODO: nicer syntax; maybe even dsl block
-- ISSUE: x, v have to be Dec

syntax GG "[" [x] "," [v] "]" ";" [gamma] "|-" [g]  = WellFormed x v gamma g;
syntax G  "[" [x] "," [v] "]"                       = GraphExpression x v;

data GraphExpression : (x: Type) -> (v: Type) -> Type where
  Empty : G[x, v]
  Adjoin : v -> G[x, v] -> G[x, v]
  AdjoinX : x -> G[x, v] -> G[x, v]
  Juxtapose : G[x, v] -> G[x, v] -> G[x, v]
  Let : x -> v -> G[x, v] -> G[x, v]
  Connect : x -> v -> G[x, v] -> x -> v -> G[x, v] -> G[x, v]

syntax [v] ":|" [g]                 = Adjoin v g;
syntax [x] ":/" [g]                 = AdjoinX x g; -- hmm..
syntax [g1] ":*:" [g2]             = Juxtapose g1 g2;
syntax "let" [x] "=" [v] "in" [g]  = Let x v g;
syntax "{" "let" [x1] "=" [v1] "in" [g1] "," "let" [x2] "=" [v2] "in" [g2] "}" = Connect x1 v1 g1 x2 v2 g2;

syntax GV "[" [x] "," [v] "]" ";" [gamma] "|-" [v'] = AdmissibleVertex x v gamma v';

data AdmissibleVertex : (x, v: Type) -> (List x) -> v -> Type where
  Verticity : {v': v} -> (GV[x, v] ; [] |- v')

syntax GX "[" [xx] "," [vv] "]" ";" [gamma] "|-" [x] = AdmissibleVariable xx vv gamma x;

data AdmissibleVariable : (x, v: Type) -> (List x) -> x -> Type where
  -- what is \emptyset doing in Variation? Why not ()?
  Variation : {x': x} -> (GX[x, v] ; [] |- x')

data WellFormed : (x, v: Type) -> (List x) -> G[x, v] -> Type where
  Foundation : GG[x, v] ; [] |- Empty
  Participation : (GG[x, v] ; gamma |- g) -> (GV[x, v] ; [] |- v')
    -> GG[x, v] ; gamma |- (v' :| g)
  Dependence :(GG[x, v] ; gamma |- g) -> (GX[x, v] ; [] |- x')
    -> GG[x, v] ; gamma |- (x' :/ g)
  Juxtaposition : {auto disjoint: Disjoint gamma1 gamma2 }
    -> (GG[x, v]; gamma1 |- g1) -> (GG[x, v]; gamma2 |- g2)
    -> GG[x, v]; (gamma1 ++ gamma2) |- (g1 :*: g2)
  Nomination :
       (GG[x, v]; (x' :: gamma) |- g) -> (GV[x, v]; [] |- v')
    -> GG[x, v]; gamma |- (let x' = v' in g)
  Connection : {auto disjoint: Disjoint gamma1 gamma2 }
    -> (GG[x, v]; gamma1 |- (let x1 = v1 in g1))
    -> (GG[x, v]; gamma2 |- (let x2 = v2 in g2))
    -> (GG[x, v]; (gamma1 ++ gamma2) |- ({let x1 = v1 in g1, let x2 = v2 in g2}))

syntax GE "[" [x] "," [v] "]" "|-" [v'] "in" [g] = Membership x v v' g;

data Membership: (x, v: Type) -> (v': v) -> G[x, v] -> Type where
  Ground: GE[x, v] |- v' in (v' :| g)
  Union: (GE[x, v] |- v' in g)
    -> GE[x, v] |- v' in (g :*: g')
  Transparency: (GE[x, v] |- v' in g)
    -> GE[x, v] |- v' in (let x' = v' in g)
  Link_L: (GE[x, v] |- v' in g_1)
    -> GE[x, v] |- v' in ({let x_1 = v_1 in g_1, let x_2 = v_2 in g_2})
  Link_R: (GE[x, v] |- v' in g_2)
    -> GE[x, v] |- v' in ({let x_1 = v_1 in g_1, let x_2 = v_2 in g_2})

-- hmm... can we absorb, rather than reify, some of these |-s?
syntax GI "[" [x] "," [v] "]" "|-" [g1] "=" [g2] = Equiv x v g1 g2

data Equiv: (x, v: Type) -> G[x, v] -> G[x, v] -> Type where
  Identity: GI[x, v] |- (Empty :*: g) = g
  Symmetry: GI[x, v] |- (g1 :*: g2) = (g2 :*: g1)
  Associativity: GI[x, v] |- (g1 :*: (g2 :*: g3)) = ((g1 :*: g2) :*: g3)
  Permutation:  GI[x, v] |- (v1 :| (vi :| (vj :| g))) = (v1 :| (vj :| (vi :| g)))
  Conservation: GI[x, v] |- (Let xx vv (Let x' vv g)) = (Let xx vv g)
{- Issue: variables / terms
  Extrusion: (Not (GE[x, v] |- xx in g2))
    -> GI[x, v] |- ((Let xx vv g1) :*: g2) = (Let xx vv (g1 :*: g2))
-}

discrete : Nat -> G[x, Nat]
discrete Z = Empty
discrete (S n_1) = (n :| Empty) :*: (discrete n_1)
  where n = S n_1

connect' : G[x, v] -> G[x, v] -> G[x, v]
connect' (let x1 = v1 in g1) (let x2 = v2 in g2) = {let x1 = v1 in g1, let x2 = v2 in g2}
connect' _ _ = Empty

chain : Nat -> G[Nat, Nat]
chain Z = Empty
chain (S Z) = Let 2 1 (1 :| Empty)
chain (S n_1) =
 Let (2 * n) n (connect' (let ((2 * (S n_1)) - 1) = n in (n :| Empty))
                         (chain n_1))
   where n = S n_1

cycle : Nat -> G[Nat, Nat]
cycle Z = Empty
cycle (S k) = connect' (chain n) (chain 1)
  where
    n = (S k)

vertices : Eq v => G[x, v] -> List v
vertices Empty = []
vertices (v :| g) = union [v] (vertices g)
vertices (x :/ g) = vertices g
vertices (g1 :*: g2) = union (vertices g1) (vertices g2)
vertices (let x = v in g) = vertices g  -- ISSUE: is this right?
vertices ({let x1 = v1 in g1, let x2 = v2 in g2}) = union (vertices g1) (vertices g2)

edges : Eq v => G[x, v] -> List (v, v)
edges Empty = []
edges (v :| g) = edges g
edges (x :/ g) = edges g
edges (g1 :*: g2) = union (edges g1) (edges g2)
edges (let x = v in g) = edges g  -- ISSUE: is this right?
edges ({let x1 = v1 in g1, let x2 = v2 in g2}) = union [(v1, v2)] (union (edges g1) (edges g2))

complete: Nat -> G[Nat, Nat]
complete Z = Empty
-- EDIT: paper says (discrete 1)
complete (S n_1) = combineAll (discrete n) (complete n_1)
  where
    n = S n_1
    combineAll : G[Nat, Nat] -> G[Nat, Nat] -> G[Nat, Nat]
    combineAll g1 g2 = foldr Juxtapose (g1 :*: g2) [
      {let x1 = x in g1, let x2 = y in g2}
        | x <- (vertices g1), y <- (vertices g2)]
      where
        -- ISSUE: where do x1, x2 come from?
        x1 = 1
        x2 = 2

-- Graph references

syntax GA "[" [x] "," [v] "]" ";" [gamma] ";" [bigG] "|-" [a]  = WFGraphRef x v gamma bigG a;

data WFGraphRef: (Either xv xg) -> v -> (List xv) -> (List xg) -> (a: xg) -> Type where
  Wire: GA[x, v] ; gamma ; [a] |- a

gmap : (x -> x') -> G[x, v] -> G[x', v]
gmap f Empty = Empty
gmap f (v :| g) = v :| (gmap f g)
gmap f (x :/ g) = (f x) :/ (gmap f g)
gmap f (g1 :*: g2) = (gmap f g1) :*: (gmap f g2)
gmap f (Let x v g) = Let (f x) v (gmap f g)
gmap f ({let x1 = v1 in g1, let x2 = v2 in g2}) =
    ({let (f x1) = v1 in (gmap f g1), let (f x2) = v2 in (gmap f g2)})

-- syntax GR "[" [xv] "+" [xg] "," [v] "]" ";" [gamma] ";" [bigG] "|-" [g]  = WFGraphRef xv xg v gamma bigG g;

{- I'm struggling with this bit...

data WF2: xv -> xg -> v -> (List xv) -> (List xg)
          -> (g: G[Either xv xg, v]) -> Type where
  Lift: {xv, xg, v': Type}
    -> (WellFormed xv v' gamma g)
    -> WF2 xv xg v' gamma [] (gmap {x=xv} {x'=Either xv xg} {v=v'} Left g)

  Bundle: {auto d1: Disjoint gamma1 gamma2}
    -> {auto d2: Disjoint bigG1 bigG2}
    ...
-}

max_stars_repo_name: jimscarver/togl

max_issues_repo_name: jimscarver/togl

max_forks_repo_name: jimscarver/togl


text:
module datastore_exercises

import DataStore

testStore : DataStore (SString .+. (SString .+. SInt))
testStore =
  addToStore ("Mercury", "Mariner 10", 1974) $
  addToStore ("Venus", "Venera", 1961) $
  addToStore ("Uranus", "Voyager 2", 1986) $
  addToStore ("Pluto", "New Horizons", 2015) $
  empty

getValues : DataStore (SString .+. val_schema) -> List (SchemaType val_schema)
getValues store with (storeView store)
  getValues empty | SNil = []
  getValues (addToStore (_, value) store) | SAdd store' = value :: getValues store | store'