text:
= ImpCEvalFun : Evaluation Function for Imp

> module ImpCEvalFun

We saw in the `Imp` chapter how a naive approach to defining a function
representing evaluation for Imp runs into difficulties. There, we adopted the
solution of changing from a functional to a relational definition of evaluation.
In this optional chapter, we consider strategies for getting the functional
approach to work.

> import Logic
> import Maps
> import Imp

> %access public export
> %default total

== A Broken Evaluator

Here was our first try at an evaluation function for commands, omitting
\idr{WHILE}.

> ceval_step1 : (st : State) -> (c : Com) -> State
> ceval_step1 st CSkip = st
> ceval_step1 st (CAss l a1) = t_update l (aeval st a1) st
> ceval_step1 st (CSeq c1 c2) =
>   let st' = ceval_step1 st c1
>   in ceval_step1 st' c2
> ceval_step1 st (CIf b c1 c2) =
>   if beval st b
>     then ceval_step1 st c1
>     else ceval_step1 st c2
> ceval_step1 st (CWhile b c) = st   -- bogus

As we remarked in chapter `Imp`, in a traditional functional programming
language like ML or Haskell we could write the WHILE case as follows:

```idris
...
ceval_step1 st (CWhile b c) =
  if (beval st b)
    then ceval_step1 st (CSeq c $ CWhile b c)
    else st
```

Idris doesn't accept such a definition (\idr{ImpCEvalFun.ceval_step1 is possibly
not total due to recursive path ImpCEvalFun.ceval_step1 -->
ImpCEvalFun.ceval_step1 --> ImpCEvalFun.ceval_step1}) because the function we
want to define is not guaranteed to terminate. Indeed, the changed
\idr{ceval_step1} function applied to the \idr{loop} program from `Imp.lidr`
would never terminate. Since Idris is not just a functional programming
language, but also a consistent logic, any potentially non-terminating function
needs to be rejected. Here is an invalid(!) Idris program showing what would go
wrong if Idris allowed non-terminating recursive functions:

```idris
loop_false : (n : Nat) -> Void
loop_false n = loop_false n
```

That is, propositions like \idr{Void} would become provable (e.g.,
\idr{loop_false 0} would be a proof of \idr{Void}), which would be a disaster
for Idris's logical consistency.

Thus, because it doesn't terminate on all inputs, the full version of
\idr{ceval_step1} cannot be written in Idris -- at least not without one
additional trick...

== A Step-Indexed Evaluator

The trick we need is to pass an _additional_ parameter to the evaluation
function that tells it how long to run. Informally, we start the evaluator with
a certain amount of "gas" in its tank, and we allow it to run until either it
terminates in the usual way _or_ it runs out of gas, at which point we simply
stop evaluating and say that the final result is the empty memory. (We could
also say that the result is the current state at the point where the evaluator
runs out fo gas -- it doesn't really matter because the result is going to be
wrong in either case!)

> ceval_step2 : (st : State) -> (c : Com) -> (i : Nat) -> State
> ceval_step2 _ _ Z = empty_state
> ceval_step2 st CSkip (S i') = st
> ceval_step2 st (CAss l a1) (S i') = t_update l (aeval st a1) st
> ceval_step2 st (CSeq c1 c2) (S i') =
>   let st' = ceval_step2 st c1 i'
>   in ceval_step2 st' c2 i'
> ceval_step2 st (CIf b c1 c2) (S i') =
>   if beval st b
>     then ceval_step2 st c1 i'
>     else ceval_step2 st c2 i'
> ceval_step2 st c@(CWhile b1 c1) (S i') =
>   if (beval st b1)
>     then let st' = ceval_step2 st c1 i' in
>          ceval_step2 st' c i'
>     else st

_Note_: It is tempting to think that the index \idr{i} here is counting the
"number of steps of evaluation." But if you look closely you'll see that this
is not the case: for example, in the rule for sequencing, the same \idr{i} is
passed to both recursive calls. Understanding the exact way that \idr{i} is
treated will be important in the proof of \idr{ceval__ceval_step}, which is
given as an exercise below.

One thing that is not so nice about this evaluator is that we can't tell, from
its result, whether it stopped because the program terminated normally or
because it ran out of gas.  Our next version returns an \idr{Maybe State}
instead of just a \idr{State}, so that we can distinguish between normal and
abnormal termination.

> ceval_step3 : (st : State) -> (c : Com) -> (i : Nat) -> Maybe State
> ceval_step3 _ _ Z = Nothing
> ceval_step3 st CSkip (S i') = Just st
> ceval_step3 st (CAss l a1) (S i') = Just $ t_update l (aeval st a1) st
> ceval_step3 st (CSeq c1 c2) (S i') =
>   case ceval_step3 st c1 i' of
>     Just st' => ceval_step3 st' c2 i'
>     Nothing => Nothing
> ceval_step3 st (CIf b c1 c2) (S i') =
>   if beval st b
>     then ceval_step3 st c1 i'
>     else ceval_step3 st c2 i'
> ceval_step3 st c@(CWhile b1 c1) (S i') =
>   if (beval st b1)
>     then case ceval_step3 st c1 i' of
>            Just st' => ceval_step3 st' c i'
>            Nothing => Nothing
>     else Just st

We can improve the readability of this version by using the fact that /idr{Maybe} forms a monad to hide the plumbing involved in repeatedly matching against optional
states.

```idris
Monad Maybe where
    Nothing  >>= k = Nothing
    (Just x) >>= k = k x
```

> ceval_step : (st : State) -> (c : Com) -> (i : Nat) -> Maybe State
> ceval_step _ _ Z = Nothing
> ceval_step st CSkip (S i') = Just st
> ceval_step st (CAss l a1) (S i') = Just $ t_update l (aeval st a1) st
> ceval_step st (CSeq c1 c2) (S i') =
>   do st' <- ceval_step st c1 i'
>      ceval_step st' c2 i'
> ceval_step st (CIf b c1 c2) (S i') =
>   if beval st b
>     then ceval_step st c1 i'
>     else ceval_step st c2 i'
> ceval_step st c@(CWhile b1 c1) (S i') =
>   if (beval st b1)
>     then do st' <- ceval_step st c1 i'
>             ceval_step st' c i'
>     else Just st

> test_ceval : (st : State) -> (c : Com) -> Maybe (Nat, Nat, Nat)
> test_ceval st c  = case ceval_step st c 500 of
>   Nothing => Nothing
>   Just st => Just (st X, st Y, st Z)

\todo[inline]{Syntax sugar for IF breaks down here}

```idris
λΠ> test_ceval Imp.empty_state (CSeq (X ::= ANum 2) (CIf (BLe (AId X) (ANum 1)) (Y ::= ANum 3) (Z ::= ANum 4)))
Just (2, 0, 4) : Maybe (Nat, Nat, Nat)
```

==== Exercise: 2 stars, recommended (pup_to_n)

Write an Imp program that sums the numbers from \idr{1} to \idr{X} (inclusive:
\idr{1 + 2 + ... + X}) in the variable \idr{Y}. Make sure your solution
satisfies the test that follows.

> pup_to_n : Com
> pup_to_n = ?pup_to_n_rhs

> pup_to_n_1 : test_ceval (t_update X 5 $ Imp.empty_state) ImpCEvalFun.pup_to_n = Just (0, 15, 0)
> pup_to_n_1 = ?pup_to_n_1 -- replace with Refl when done

$\square$

==== Exercise: 2 stars, optional (peven)

Write a \idr{While} program that sets \idr{Z} to \idr{0} if \idr{X} is even and
sets \idr{Z} to \idr{1} otherwise. Use \idr{test_ceval} to test your program.

> -- FILL IN HERE

$\square$

== Relational vs. Step-Indexed Evaluation

As for arithmetic and boolean expressions, we'd hope that the two alternative
definitions of evaluation would actually amount to the same thing in the end.
This section shows that this is the case.

> ceval_step__ceval : (c : Com) -> (st, st' : State) -> (i ** ceval_step st c i = Just st') -> c / st \\ st'
> ceval_step__ceval c st st' (Z ** prf) = absurd prf
> ceval_step__ceval CSkip st st (S i ** Refl) = E_Skip
> ceval_step__ceval (CAss l a) st st' (S i ** prf) =
>  rewrite sym $ justInjective prf in
>  E_Ass {n=aeval st a} Refl
> ceval_step__ceval (CSeq c1 c2) st st' (S i ** prf) with (ceval_step st c1 i) proof c1prf
>   ceval_step__ceval (CSeq c1 c2) st st' (S i ** prf) | Just st1 =
>     E_Seq (ceval_step__ceval c1 st st1 (i**sym c1prf))
>           (ceval_step__ceval c2 st1 st' (i**prf))
>   ceval_step__ceval (CSeq c1 c2) st st' (S i ** prf) | Nothing = absurd prf
> ceval_step__ceval (CIf b c1 c2) st st' (S i ** prf) with (beval st b) proof bprf
>   ceval_step__ceval (CIf b c1 c2) st st' (S i ** prf) | True  =
>     E_IfTrue (sym bprf) (ceval_step__ceval c1 st st' (i**prf))
>   ceval_step__ceval (CIf b c1 c2) st st' (S i ** prf) | False =
>     E_IfFalse (sym bprf) (ceval_step__ceval c2 st st' (i**prf))
> ceval_step__ceval (CWhile b c) st st' (S i ** prf) with (beval st b) proof bprf
>   ceval_step__ceval (CWhile b c) st st' (S i ** prf) | True with (ceval_step st c i) proof cprf
>     ceval_step__ceval (CWhile b c) st st' (S i ** prf) | True | Just st1 =
>       E_WhileLoop (sym bprf) (ceval_step__ceval c st st1 (i**sym cprf))

\todo[inline]{Idris can't see sigma is decreasing, use WellFounded here?}

>                              (assert_total $ ceval_step__ceval (CWhile b c) st1 st' (i**prf))
>     ceval_step__ceval (CWhile b c) st st' (S i ** prf) | True | Nothing = absurd prf
>   ceval_step__ceval (CWhile b c) st st (S i ** Refl) | False = E_WhileEnd (sym bprf)

==== Exercise: 4 stars (ceval_step__ceval_inf)

Write an informal proof of \idr{ceval_step__ceval}, following the usual
template. (The template for case analysis on an inductively defined value should
look the same as for induction, except that there is no induction hypothesis.)
Make your proof communicate the main ideas to a human reader; do not simply
transcribe the steps of the formal proof.

> -- FILL IN HERE

$\square$

> ceval_step_more : (i1, i2 : Nat) -> (st, st' : State) -> (c : Com) -> LTE i1 i2 -> ceval_step st c i1 = Just st'
>                -> ceval_step st c i2 = Just st'
> ceval_step_more Z i2 st st' c lte prf = absurd prf
> ceval_step_more (S i1) Z st st' c lte prf = absurd lte
> ceval_step_more (S i1) (S i2) st st' CSkip lte prf = prf
> ceval_step_more (S i1) (S i2) st st' (CAss l a) lte prf = prf
> ceval_step_more (S i1) (S i2) st st' (CSeq c1 c2) lte prf with (ceval_step st c1 i1) proof cprf
>   ceval_step_more (S i1) (S i2) st st' (CSeq c1 c2) lte prf | Just st1 =
>     rewrite ceval_step_more i1 i2 st st1 c1 (fromLteSucc lte) (sym cprf) in
>     ceval_step_more i1 i2 st1 st' c2 (fromLteSucc lte) prf
>   ceval_step_more (S i1) (S i2) st st' (CSeq c1 c2) lte prf | Nothing = absurd prf
> ceval_step_more (S i1) (S i2) st st' (CIf b c1 c2) lte prf with (beval st b) proof bprf
>   ceval_step_more (S i1) (S i2) st st' (CIf b c1 c2) lte prf | True =
>     ceval_step_more i1 i2 st st' c1 (fromLteSucc lte) prf
>   ceval_step_more (S i1) (S i2) st st' (CIf b c1 c2) lte prf | False =
>     ceval_step_more i1 i2 st st' c2 (fromLteSucc lte) prf
> ceval_step_more (S i1) (S i2) st st' (CWhile b c) lte prf with (beval st b)
>   ceval_step_more (S i1) (S i2) st st' (CWhile b c) lte prf | True with (ceval_step st c i1) proof cprf
>     ceval_step_more (S i1) (S i2) st st' (CWhile b c) lte prf | True | Just st1 =
>       rewrite ceval_step_more i1 i2 st st1 c (fromLteSucc lte) (sym cprf) in
>       ceval_step_more i1 i2 st1 st' (CWhile b c) (fromLteSucc lte) prf
>     ceval_step_more (S i1) (S i2) st st' (CWhile b c) lte prf | True | Nothing = absurd prf
>   ceval_step_more (S i1) (S i2) st st' (CWhile b c) lte prf | False = prf

==== Exercise: 3 stars, recommended (ceval__ceval_step)

Finish the following proof. You'll need \idr{ceval_step_more} in a few places,
as well as some basic facts about \idr{LTE} and \idr{S}.

> ceval__ceval_step : (c : Com) -> (st, st' : State) -> (c / st \\ st') -> (i ** ceval_step st c i = Just st')
> ceval__ceval_step c st st' prf = ?ceval__ceval_step_rhs

$\square$

> ceval_and_ceval_step_coincide : (c : Com) -> (st, st' : State) -> (c / st \\ st') <-> (i ** ceval_step st c i = Just st')
> ceval_and_ceval_step_coincide c st st' = (ceval__ceval_step c st st', ceval_step__ceval c st st')

== Determinism of Evaluation Again

Using the fact that the relational and step-indexed definition of evaluation are
the same, we can give a slicker proof that the evaluation _relation_ is
deterministic.

> ceval_deterministic' : (c : Com) -> (st, st1, st2 : State) -> (c / st \\ st1) -> (c / st \\ st2) -> st1 = st2
> ceval_deterministic' c st st1 st2 prf1 prf2 =
>   let
>     (i1**e1) = ceval__ceval_step c st st1 prf1
>     (i2**e2) = ceval__ceval_step c st st2 prf2
>     plus1 = ceval_step_more i1 (i1+i2) st st1 c (lteAddRight i1) e1
>     plus2 = ceval_step_more i2 (i1+i2) st st2 c (rewrite plusCommutative i1 i2 in lteAddRight i2) e2
>     in
>   justInjective $ trans (sym plus1) plus2

ext: lidr

max_stars_repo_name: diseraluca/software-foundations

max_issues_repo_name: diseraluca/software-foundations

max_forks_repo_name: diseraluca/software-foundations


text:
||| Safe pointer
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module Foreign.Memory.Ptr

import Decidable.Equality

%default total

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

export isNullPtr : {a:Type} -> Ptr a -> Bool
isNullPtr p = prim__nullAnyPtr (prim__forgetPtr p) /= 0

export nullPtr : {a:Type} -> Ptr a
nullPtr = prim__castPtr (prim__getNullAnyPtr)

%foreign "C:idris2_isNull, libidris2_support"
         "javascript:lambda:x=>x===undefined||x===null?1n:0n"
export prim__nullGCAnyPtr : GCAnyPtr -> Int

export isNullGCPtr : {a:Type} -> GCPtr a -> Bool
isNullGCPtr p = prim__nullGCAnyPtr (believe_me p) /= 0

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

public export
isNotNullPtr : {ty:Type} -> Ptr ty -> Type
isNotNullPtr ptr = isNullPtr ptr = False

public export
isNotNullGCPtr : {ty:Type} -> GCPtr ty -> Type
isNotNullGCPtr ptr = isNullGCPtr ptr = False

-- --------------------------------------------------------------------------
-- vim: tw=80 sw=2 expandtab :

ext: idr


text:
module Control.Optics.Prism

import public Control.Optics.Types

export
prism : (b -> t) -> (s -> Either t a) -> Prism s t a b
prism inj prj = dimap prj (either pure (map inj)) . right'


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

import public Minecraft.Core.Entity
import public Minecraft.Base.PreClassic.Cobblestone.Block
import public Minecraft.Base.PreClassic.Cobblestone.Item
import public Minecraft.Base.PreClassic.Cobblestone.ItemEntity

%default total

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

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

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

[cobblestoneBlock']
Block Cobblestone.Block where
  id = Item.id {self = Cobblestone.Item}

[breakCobblestone']
Break Cobblestone.Block where
  breakBlk self = [new Cobblestone.ItemEntity Cobblestone.MkItemEntity]

[cobblestoneVtbl']
Vtbl Cobblestone.Block where
  vtable (Block    Cobblestone.Block) = Just cobblestoneBlock
  vtable (Break    Cobblestone.Block) = Just breakCobblestone
  vtable (Tangible Cobblestone.Block) = Just %search
  vtable _ = Nothing

cobblestoneBlock = cobblestoneBlock'
breakCobblestone = breakCobblestone'
cobblestoneVtbl  = cobblestoneVtbl'

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module GuardedRecursion

%default total

data Later : Type -> Type where
  next  : a -> Later a

compose : Later (a -> b) -> Later a -> Later b
compose (next t) (next u) = next (t u)

instance Functor Later where
  map f (next t) = next (f t)

instance Applicative Later where
  pure = next
  (next t) <$> (next u) = compose (next t) (next u)
{-
data Box : Type where
  Boxed   : Box
  Unboxed : Box

data GT : Box -> Type -> Type where
  Guard : (b : Box) -> a -> GT b a

instance Functor (GT b) where
  map f g = case g of
              Guard b a => Guard b (f a)
-}

partial
fix : (Later a -> a) -> a
fix f = f (next (fix f))

nextid : (u : Later a) -> ((next id) <$> u) = u
nextid (next x) = Refl

nextcompose : (s : Later (b -> c)) -> (t : Later (c -> b)) -> (u : Later c) -> ((next (.) <$> s) <$> t) <$> u = s <$> (t <$> u)
nextcompose (next s') (next t') (next u') = Refl

nextcompose' : (t : (a -> b)) -> (u : a) -> next t <$> next u = next (t u)
nextcompose' t' u' = Refl

nextright : (u : Later (a -> b)) -> (t : a) -> u <$> next t =  next(\g => g t) <$> u
nextright (next u') t = Refl

laterDist : Later (Later (a -> b)) -> Later (Later a -> Later b)
laterDist (next t) = next (t <$>)

nLater : Nat -> Type -> Type
nLater Z a = a
nLater (S n) a = Later (nLater n a)

nCompose : (n : Nat) -> nLater (S n) (a -> b) -> nLater (S n) a -> nLater (S n) b
nCompose Z t u = compose t u
nCompose (S n') (next t) (next u) = next (nCompose n' t u)

doubleCompose : Later (Later (a -> b)) -> Later (Later a) -> Later (Later b)
doubleCompose = nCompose 1

oneComposeIsCompose : (nCompose 0 t u) = compose t u
oneComposeIsCompose = Refl

twoComposeIsDoubleCompose : (nCompose 1 t u) = doubleCompose t u
twoComposeIsDoubleCompose = Refl

unsafeForce : Later a -> a
unsafeForce (next t) = t

app1 : Later (a -> b) -> a -> Later b
app1 f a = f <$> (next a)

app1' : nLater (S n) (a -> b) -> nLater n a -> nLater (S n) b
app1' {n} f a = nCompose n f (next a)

app1n : (n : Nat) -> nLater n (a -> b) -> a -> nLater n b
app1n (S Z) f a = f <$> (next a)
app1n (S n') (next f) a = next $ (app1n n' f a)

app1Eq : app1 f a = app1n 1 f a
app1Eq = Refl

app1Eq' : app1n 1 (next f) a = app1' {n = Z} (next f) a
app1Eq' = Refl

app2 : (a -> b) -> Later a -> Later b
app2 f (next a) = next (f a)

app2' : nLater n (a -> b) -> nLater (S n) a -> nLater (S n) b
app2' {n} f a = nCompose n (next f) a

app2n : (n : Nat) -> (a -> b) -> nLater n a -> nLater n b
app2n Z f a = f a
app2n (S Z) f (next a) = next (f a)
app2n (S n') f (next a) = next (app2n n' f a)

app2Eq : (eq : (next b) = a) -> app2 f a = app2n 1 f a
app2Eq = ?app2EqMeta

app2Eq' : (eq : (next b) = a) -> app2n 1 f a = app2' {n = Z} f a
app2Eq' = ?app2Eq'Meta

app3 : (a -> b) -> a -> Later b
app3 f a = next (f a)

app3' : nLater n (a -> b) -> nLater n a -> nLater (S n) b
app3' {n} f a = nCompose n (next f) (next a)

app3n : (n : Nat) -> (a -> b) -> a -> nLater n b
app3n Z f a = f a
app3n (S n') f a = next (app3n n' f a)

app4 : Later (a -> b) -> Later a -> Later b
app4 = nCompose 0

app4' : nLater (S n) (a -> b) -> nLater (S n) a -> nLater (S n) b
app4' {n} = nCompose n

app4n : (n : Nat) -> nLater (S n) (a -> b) -> nLater (S n) a -> nLater (S n) b
app4n n = app4' {n}

corecord Stream' : Type -> Type where
   hd : Stream' a -> a
   tl : Stream' a -> Later (Stream' a)
   constructor StreamCons

take' : (n : Nat) -> Stream' a -> Vect n a
take' Z _ = []
take' (S n) s = (hd s) :: (take' n (unsafeForce (tl s)))

partial
take'' : (n : Nat) -> Stream' a -> List a
take'' = fix(\t,n,s => case n of
                         Z    => []
                         S n' => (hd s) :: (unsafeForce ( ( t <$> (next n') ) <$> (tl s))))

partial
zeros : Stream' Nat
zeros = fix (\f => StreamCons 0 f)

partial
moreZeros : Stream' Nat
moreZeros = fix (\f => StreamCons 0 (app1 (app3 StreamCons 0) f))

partial
prepend : List a -> Stream' a -> Stream' a
prepend = fix (\p => \l => \s => case l of
                                   [] => s
                                   (x :: xs) => StreamCons x ((p <$> (next xs)) <$> (next s)))

{-
partial
prepend'Z : Vect Z a -> Stream' a -> Stream' a
prepend'Z = fix (\p, [], s => s)

prepend'S : Vect (S n) a -> Stream' a -> Stream' a
prepend'S = fix (\p, (x :: xs), s => StreamCons x (p <$> (next xs) <$> (next s)))
-}
partial
hMerge : Stream' a -> Stream' a -> Stream' a
hMerge = fix (\m => \xs => \ys => StreamCons (hd xs) (next (StreamCons (hd ys) (m <$> (tl xs) <$> (tl ys)))))

partial
hMerge' : Stream' a -> Stream' a -> Stream' a
hMerge' = fix (\m => \xs => \ys => StreamCons (hd xs) ((next StreamCons <$> next (hd ys)) <$> next ((m <$> (tl xs)) <$> (tl ys))))

partial
mergef : (a -> a -> Later (Stream' a) -> Stream' a) -> Stream' a -> Stream' a -> Stream' a
mergef f = fix (\m => \xs => \ys => f (hd xs) (hd ys) ((m <$> (tl xs)) <$> (tl ys)))

partial
mergef' : (a -> a -> Later (Stream' a) -> Stream' a) -> Stream' a -> Stream' a -> Stream' a
mergef' = fix (\m => \f => \xs => \ys => f (hd xs) (hd ys) (((m <$> (next f)) <$> (tl xs)) <$> (tl ys)))
{-
unguard : (GT Boxed a) -> a
unguard (Guard _ a) = a

partial
gMap : (a -> b) -> (GT x (Stream' a)) -> (GT x (Stream' b))
gMap = fix (\m, f, s => Guard x (StreamCons (map (f . hd) s)  ))

partial
gEven : (GT Boxed (Stream' a)) -> (GT Boxed (Stream' a))
-}
partial
sMap : (a -> b) -> Stream' a -> Stream' b
sMap = fix (\m => \f => \s => StreamCons (f (hd s)) ((m <$> (next f)) <$> (tl s)))

partial
sMap' : (a -> b) -> Stream' a -> Stream' b
sMap' = fix (\m => \f => \s => StreamCons (f (hd s)) (app4 (app1 m f) (tl s)))

partial
sMerge : Ord a => Stream' a -> Stream' a -> Stream' a
sMerge = fix (\m => \s => \t => StreamCons
                                 (if (hd s) <= (hd t) then hd s else hd t)
                                 (if (hd s) <= (hd t) then
                                     (if (hd t <= hd s) then
                                        app4 (app4 m (tl s)) (tl t)
                                     else
                                        app1 (app4 m (tl s)) t)
                                 else
                                    app4 (app1 m s) (tl t)))

partial
hamming : Stream' Nat
hamming = fix (\h => StreamCons 1
		            (((next sMerge) <$> ((next (sMap (\x => 2 * x)) <$> h))) <$>
                                               (((next sMerge) <$> (next (sMap (\x => 3 * x)) <$> h)) <$>
                                                                   (next (sMap (\x => 5 * x)) <$> h))))

partial
zipWith' : (a -> b -> c) -> Stream' a -> Stream' b -> Stream' c
zipWith' f = fix(\g => \s => \t => StreamCons (f (hd s) (hd t)) (g <$> (tl s) <$> (tl t)))

partial
zipWithNat : (Nat -> Nat -> Nat) -> Stream' Nat -> Stream' Nat -> Stream' Nat
zipWithNat = zipWith' {a=Nat} {b=Nat} {c=Nat}

partial
fib : Stream' Nat
fib = fix (\f => StreamCons 0 (app4 (app3 StreamCons 1) (app4' (app1' {n=1} (app3n 2 zipWithNat (+)) f) (app2 tl f))))

partial
nats : Stream' Nat
nats = fix (\n => StreamCons 0 ((next sMap <$> next S) <$> n))

partial tailtail : Stream' a -> Later (Later (Stream' a))
tailtail = fix(\t, s => (next tl) <$> (tl s))

hat : nLater (S n) (a -> b) -> (Later (nLater n a -> nLater n b))
hat = ?h

partial nats2 : Stream' Nat
nats2 = fix(\n => StreamCons 0 (app4 (app3 StreamCons 1) (app4 (hat {n=1} (app3n 2 sMap S)) (app2 tl n))))

partial bad : (Stream' Nat)
bad = fix(\b => b)

corecord Foo : Type where
  bar : Foo -> Bool
  baz : (f : Foo) -> (if bar f then (Later Foo) else Nat)

partial
alpha : Foo
alpha = fix (\a => MkFoo True (next alpha))

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

GuardedRecursion.app2EqMeta = proof
  intros
  rewrite eq
  compute
  refine Refl

GuardedRecursion.app2Eq'Meta = proof
  intros
  rewrite eq
  compute
  refine Refl

max_stars_repo_name: sualitu/thesis

max_issues_repo_name: sualitu/thesis

max_forks_repo_name: sualitu/thesis


text:
import System.Random

main : IO ()
main = do
  value <- randomRIO (the Double 10, the Double 30.5)
  printLn $ value > 10


text:
data SplitList : List a -> Type where
  SplitNil : SplitList []
  SplitOne : SplitList [x]
  SplitPair : (lefts : List a) -> (rights : List a) -> SplitList (lefts ++ rights)

splitList : (xs : List a) -> SplitList xs
splitList xs = splitList' xs xs
  where
    splitList' : (counter : List a) -> (input : List a) -> SplitList input
    splitList' _ [] = SplitNil
    splitList' _ [x] = SplitOne
    splitList' (_ :: _ :: counter) (item :: items)
      = case splitList' counter items of
             SplitNil => SplitOne
             SplitOne {x} => SplitPair [item] [x]
             (SplitPair lefts rights) => SplitPair (item :: lefts) rights
    splitList' _ items = SplitPair [] items

merge_sort : Ord a => List a -> List a
merge_sort xs with (splitList xs)
  merge_sort [] | SplitNil = []
  merge_sort [x] | SplitOne = [x]
  merge_sort (lefts ++ rights) | (SplitPair lefts rights)
    = merge (merge_sort lefts) (merge_sort rights)

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module GRIN.Pipeline

import Data.SortedSet as Set
import Data.SortedMap as Map
import Data.String.Builder

import System.Clock
import System.File

import GRIN.AST
import GRIN.Error
import GRIN.GrinM

import GRIN.Analysis.CallGraph
import GRIN.Analysis.Inline

import GRIN.Opts.CaseSimplify
import GRIN.Opts.CopyPropogation
import GRIN.Opts.Inline
import GRIN.Opts.NormaliseBind
import GRIN.Opts.UnusedConstructorElim
import GRIN.Opts.UnusedFunctionElim
import GRIN.Opts.UnusedParameterElim

public export
data Optimise name
    = CaseSimplify
    | CopyPropogation
    | InlineSimpleDef
    | InlineUsedOnce
    | InlineFunc name
    | NormaliseBind
    | UnusedConstructorElim
    | UnusedFunctionElim
    | UnusedParamElim
    | Fix (List (Optimise name))

Show name => Show (Optimise name) where
    show CopyPropogation = "copy propogation"
    show CaseSimplify = "case simplification"
    show InlineSimpleDef = "inline simple definitions"
    show InlineUsedOnce = "inline functions used once"
    show (InlineFunc fn) = "inline " ++ show fn
    show NormaliseBind = "bind normalisation"
    show UnusedConstructorElim = "unused constructor elimintation"
    show UnusedFunctionElim = "unused function elimination"
    show UnusedParamElim = "unused parameter elimination"
    show (Fix os) = "fix " ++ show os

export
runOpts : Monad m => Ord name => List (Optimise name) -> GrinT name m ()

export
runOpt : Monad m => Ord name => Optimise name -> GrinT name m ()
runOpt CaseSimplify = caseSimplify
runOpt CopyPropogation = copyProp
runOpt InlineSimpleDef = do
    inlineSimpleDefs
    inlineAll
runOpt InlineUsedOnce = do
    inlineUsedOnce
    inlineAll
runOpt (InlineFunc fn) = do
    ds <- gets $ defs . prog
    case lookup fn ds of
        Nothing => pure ()
        Just def => modify $ record { toInline = singleton fn def }
    inlineAll
runOpt NormaliseBind = normaliseBind
runOpt UnusedConstructorElim = unusedConsElim
runOpt UnusedFunctionElim = unusedFuncElim
runOpt UnusedParamElim = unusedParamElim
runOpt s@(Fix ss) = do
    p0 <- gets prog
    runOpts ss
    p1 <- gets prog
    if p1 == p0
        then pure ()
        else runOpt s

runOpts [] = pure ()
runOpts (s :: ss) = runOpt s *> runOpts ss

public export
data Transform name
    = O (Optimise name)
    | SaveGrin Bool String
    | SaveCalls Bool String
    | SaveCalledBy Bool String
    | SaveInlineSimple Bool String

Show name => Show (Transform name) where
    show (O o) = show o
    show (SaveGrin _ _) = "save GRIN"
    show (SaveCalls _ _) = "save calls graph"
    show (SaveCalledBy _ _) = "save called by graph"
    show (SaveInlineSimple _ _) = "save simple functions to inline"

export
runTransform : Show name => ShowB (Prog name) => Ord name => Transform name -> GrinT name IO ()
runTransform (O opt) = runOpt opt
runTransform (SaveGrin True f) = do
    p <- gets prog
    let pretty = runBuilder $ showB p
    Right () <- lift $ writeFile f pretty
        | Left err => newError $ FileErr f err
    pure ()
runTransform (SaveCalls True f) = do
    cg <- getCalls
    let pretty = showCallGraph cg
    Right () <- lift $ writeFile f pretty
        | Left err => newError $ FileErr f err
    pure ()
runTransform (SaveCalledBy True f) = do
    cg <- getCalledBy
    let pretty = showCallGraph cg
    Right () <- lift $ writeFile f pretty
        | Left err => newError $ FileErr f err
    pure ()
runTransform (SaveInlineSimple True f) = do
    inlineSimpleDefs
    ti <- gets toInline
    Right () <- lift $ writeFile f $ show $ keys ti
        | Left err => newError $ FileErr f err
    pure ()
runTransform _ = pure ()

export
runTransforms : Show name => ShowB (Prog name) => Ord name => List (Transform name) -> GrinT name IO ()
runTransforms [] = pure ()
runTransforms (t :: ts) = runTransform t *> runTransforms ts

nano : Integer
nano = 1000000000

micro : Integer
micro = 1000000

export
runWithTiming : Show name => ShowB (Prog name) => Ord name => List (Transform name) -> GrinT name IO ()
runWithTiming [] = pure ()
runWithTiming (t :: ts) = do
    putStrLn $ "Start " ++ show t
    clock <- liftIO $ clockTime Process
    let start = seconds clock * nano + nanoseconds clock
    runTransform t
    let end = seconds clock * nano + nanoseconds clock
    let time = end - start
    putStrLn $
        "Finished, took: "
        ++ show (time `div` nano) ++ "."
        ++ addZeros (unpack (show ((time `mod` nano) `div` micro)))
        ++ "s"
    runWithTiming ts
  where
    addZeros : List Char -> String
    addZeros [] = "000"
    addZeros [x] = "00" ++ cast x
    addZeros [x, y] = "0" ++ cast x ++ cast y
    addZeros str = pack str


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

import System

import Sif.Types
import Sif.AbsSyntax
import Sif.Pattern
import Sif.Builder.AbsInterp
import Sif.Builder.DirectRep
import Sif.Effs

import Sif.Error
import Sif.Library
import Sif.DSL.State
import Sif.DSL.Parser.Problem
import Sif.DSL.Parser.Solution
import Sif.DSL.Parser
import Sif.DSL

import Sif.Options
import Sif.API
import Sif.REPL
import Sif.Perf

%default partial

runMode : Maybe SifMode -> Sif ()
runMode Nothing     = putStrLn helpStr
runMode (Just VERS) = printLn FeatureNotImpl
runMode (Just HELP) = putStrLn helpStr

runMode (Just REPL) = do
    loadPrelude
    sifREPL

runMode (Just Eval) = do
    os <- getOptions
    putStrLn $ "Evaluating Pattern"
    evalPatternFromFile (pSpec os) (sSpec os)

runMode (Just Check) = do
    os <- getOptions
    putStrLn $ "Checking Providing Files"
    doSyntaxCheck (pSpec os) (sSpec os)

runMode (Just Conv) = do
    os <- getOptions
    putStrLn "Converting Pattern"
    convPatternFromFile (pSpec os) (sSpec os) (out os) (to os)

sifMain : Sif ()
sifMain = do
    opts <- parseOptions
    putOptions opts
    setLogLvl (loglvl opts)
    perfSetup
    setSifBackend (backend opts)
    runMode (mode opts)
    displayPerfMetrics

main : IO ()
main = do
  run $ sifMain
  exit 0

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
module SkewBinaryRandomAccessList

import RandomAccessList

%default total
%access private

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

export
data SkewList a = SL (List (Int, Tree a))

ncCons : a -> List (Int, Tree a) -> SkewList a
ncCons x ts = SL ((1, Leaf x) :: ts)

export
RandomAccessList SkewList where
  empty = SL []
  isEmpty (SL ts) = isNil ts

  cons x (SL ts@((w1, t1) :: (w2, t2) :: tts)) =
    if w1 == w2 then SL ((1 + w1 + w2, Node x t1 t2) :: tts) else ncCons x ts
  cons x (SL ts) = ncCons x ts

  head (SL []) = idris_crash "empty list"
  head (SL ((_, Leaf x) :: ts)) = x
  head (SL ((w, Node x t1 t2) :: ts)) = x

  tail (SL []) = ?RandomAccessList_rhs_1
  tail (SL ((_, Leaf x) :: ts)) = SL ts
  tail (SL ((w, Node x t1 t2) :: ts)) = let hw = assert_total $ w `div` 2 in
    SL ((hw, t1) :: (hw, t2) :: ts)

  lookup i (SL ts) = look i ts
   where
    lookTree : Int -> Int -> Tree a -> a
    lookTree _ 0 (Leaf x) = x
    lookTree _ i (Leaf x) = idris_crash "bad subscript"
    lookTree w 0 (Node x t1 t2) = x
    lookTree w i (Node x t1 t2) = let w' = assert_total $ w `div` 2 in
      if i <= w' then lookTree w' (i - 1) t1 else lookTree w' (i - 1 - w') t2

    look i []             = idris_crash "bad subscript"
    look i ((w, t) :: ts) =
      if i < w then lookTree w i t else look (i - w) ts

  update i y (SL ts) = SL (upd i ts)
   where
    updTree : Int -> Int -> Tree a -> Tree a
    updTree _ 0 (Leaf x) = Leaf y
    updTree _ i (Leaf x) = idris_crash "bad subscript"
    updTree w 0 (Node x t1 t2) = Node y t1 t2
    updTree w i (Node x t1 t2) = let w' = assert_total $ w `div` 2 in
      if i <= w' then Node x (updTree w' (i - 1) t1) t2
      else Node x t1 (updTree w' (i - 1 - w') t2)

    upd i [] = idris_crash "bad subscript"
    upd i ((w, t) :: ts) =
      if i < w then (w, updTree w i t) :: ts else (w, t) :: upd (i - w) ts


text:
module Data.Trimorphisms

%default total
%access public export

data Trimorphism : Type -> Type -> Type -> Type where
  Trimo : (a -> b -> c) -> Trimorphism a b c

applyTimo : Trimorphism a b c -> a -> b -> c
applyTimo (Trimo t) a b = (t a) b

max_stars_repo_name: lemastero/Idris-Trifunctors

max_issues_repo_name: lemastero/Idris-Trifunctors

max_forks_repo_name: lemastero/Idris-Trifunctors


text:
module Python.Lib.Requests

import Python

%access public export
%default total

Response : Signature
Response f = case f of
  "text" => Attr String
  _ => Object f

Session : Signature
Session f = case f of
  "get" => [String] ~~> Obj Response
  _ => Object f

Requests : Signature
Requests f = case f of
  "Session" => [] ~~> Obj Session
  _ => Module f

import_ : PIO $ Obj Requests
import_ = importModule "requests"

max_stars_repo_name: ziman/idris-py

max_issues_repo_name: ziman/idris-py

max_forks_repo_name: ziman/idris-py


text:
module Test.LazyTest

import Data.Bytes.Lazy
import Data.Bytes
import Data.Bytes.Util

import Data.Word.Word8

import System.File

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

cas : Char -> Word8
cas c = cast (cast {to=Int} c)

-- read some number of file chacters, crash with msg on problem or eof, this is
-- to check if we're reading lazily.
-- If we eof crash then we read the whole file at once.
partial
readN : File -> Int -> IO (List Word8)
readN f n = if 0 >= n then pure []
                      else
                        do Right c <- fGetChar f
                             | Left err => idris_crash "readN Left"
                           False <- fEOF f
                             | True => idris_crash "readN eof"
                             -- If we're at fEOF then c was \NUL !
                           [| pure (cas c) :: readN f (n-1) |]

take : Nat -> LBytes -> LBytes
take Z lb = Empty
take (S k) Empty = Empty
take (S k) (Chunk b bs) = Chunk b (take k bs)

partial
fileTest : IO LBytes
fileTest = do Right f <- openFile "foo.txt" Read
                | Left err => idris_crash (show err)
              r <- make f []
              pure $ buildup f r
  where
    partial
    make : File -> List Word8 -> IO (Bytes, List Word8)
    make f rem
      = do rs@(_::_) <- readN f 32
             | [] => pure (empty,[])
           pure (packUpToNBytes 32 (rem ++ rs))
    partial
    buildup : File -> (Bytes, List Word8) -> LBytes
    buildup f (b,rem)
      = if null b then Empty
                  else Chunk b (buildup f (unsafePerformIO $ make f rem))
    -- ^ unsafePerformIO is so that we're not in IO, so we can do this creation
    -- lazily, don't do this yourself! Make or use a streaming IO lib. In the
    -- real world we desire predictable errors, thus our use of IO should be
    -- predictable, who knows where in our program our errrors are going to
    -- explode up now that we've lied and said `make` is pure.

printo : LBytes -> IO ()
printo lb = go 0 lb
  where
    go : Int -> LBytes -> IO ()
    go n Empty = putStrLn $ "End of lazy bytes. If you didn't get an eof"
      ++ "error\nthen we succeeded in reading only part of the file."
    go n (Chunk _ lbs) = do
      putStrLn $ "Chunk " ++ show n
      go (n + 1) lbs

export
partial
lazyIOTest : IO ()
lazyIOTest = do f <- fileTest
                putStrLn "Lazy Bytes test:"
                printo (take 2 f)
                putStrLn "Eat to eof test:"
                printo f -- This should eof crash.


text:
%flag C "-I/nix/store/rcq128vq55nv4d4gqr4clyasg6zld9sy-mesa-19.1.5-dev/include -I/nix/store/rkkd7znrivqm37sbs5mj9954lmldrink-glew-2.1.0-dev/include -I/nix/store/xpzfnwicijd2l21azlrgkwdr42clc190-glu-9.0.1-dev/include -I/nix/store/031c5pk5lzabgmpqpyd46hzi625as6bp-libpng-apng-1.6.37-dev/include/libpng16 -I/nix/store/24rw4c3nm4nlsvq5hxbc2bc8gbzw1jib-zlib-1.2.11-dev/include"
%flag C "-L/nix/store/s2nz5pzn6m31jwndq8p48cfqpdfrx7g4-libglvnd-1.0.0/lib -L/nix/store/9kc72g8apidhdjb6mfqfv2dp3hywzh0k-glew-2.1.0/lib -L/nix/store/bdgnd4v8lzgvylybc13dlcm97afk7af5-glu-9.0.1/lib -L/nix/store/bcw1cimbj66vlck3lv3hh770cqhxp1zb-libpng-apng-1.6.37/lib -L/nix/store/3bfzi6w3067hbdyl15vmypjn4q6az9j6-zlib-1.2.11/lib -lGLEW -lGLU -lGL -lpng16 -lz"
%flag C "-lGL"

max_stars_repo_name: xiphiness/gl-idris

max_issues_repo_name: xiphiness/gl-idris

max_forks_repo_name: xiphiness/gl-idris


text:
import Data.Vect
import Data.Strings

data ATMState = Ready | CardInserted | Session

data PINCheck = CorrectPIN | IncorrectPIN

PIN : Type
PIN = Vect 4 Char

data HasCard : ATMState -> Type where
  HasCI : HasCard CardInserted
  HasSession : HasCard Session

data ATMCmd : (ty : Type) -> ATMState -> (ty -> ATMState) -> Type where
  InsertCard : ATMCmd ()  Ready        (const CardInserted)
  EjectCard :  {auto prf : HasCard state} ->
               ATMCmd ()  state        (const Ready)
  GetPIN :     ATMCmd PIN CardInserted (const CardInserted)

  CheckPIN : PIN -> ATMCmd PINCheck CardInserted (\check => case check of
                                                                 CorrectPIN => Session
                                                                 IncorrectPIN => CardInserted)

  GetAmount :                   ATMCmd Nat state   (const state)
  Dispense :  (amount : Nat) -> ATMCmd ()  Session (const Session)

  Message :  String -> ATMCmd () state          (const state)
  Pure : (res : ty) -> ATMCmd ty (state_fn res) state_fn
  (>>=) : ATMCmd a state1 state2_fn ->
          ((res : a) -> ATMCmd b (state2_fn res) state3_fn) ->
          ATMCmd b state1 state3_fn

readVect : (n : Nat) -> IO (Vect n Char)
readVect Z = do discard <- getLine  -- rest of input up to enter
                pure []
readVect (S k) = do ch <- getChar
                    chs <- readVect k
                    pure (ch :: chs)

testPIN : Vect 4 Char
testPIN = ['1', '2', '3', '4']

insertEject : ATMCmd () Ready (const Ready)
insertEject = do InsertCard
                 EjectCard  -- ?insertEject_rhs

-- badATM : ATMCmd () Ready (const Ready)
-- badATM = EjectCard

runATM : ATMCmd res inState outState_fn -> IO res
runATM InsertCard = do putStrLn "Please insert your card (press enter)"
                       x <- getLine
                       pure ()
runATM EjectCard = putStrLn "Card ejected"
runATM GetPIN = do putStr "Enter PIN: "
                   readVect 4
runATM (CheckPIN pin) = if pin == testPIN
                           then pure CorrectPIN
                           else pure IncorrectPIN
runATM GetAmount = do putStr "How much would you like? "
                      x <- getLine
                      pure (stringToNatOrZ x)
runATM (Dispense amount) = putStrLn ("Here is " ++ show amount)
runATM (Message msg) = putStrLn msg
runATM (Pure res) = pure res
runATM (x >>= f) = do x' <- runATM x
                      runATM (f x')

atm : ATMCmd () Ready (const Ready)
atm = do InsertCard
         pin <- GetPIN
         pinOK <- CheckPIN pin
         case pinOK of
              CorrectPIN => do cash <- GetAmount
                               Dispense cash
                               EjectCard
              IncorrectPIN => EjectCard

atm_alt : ATMCmd () Ready (const Ready)
atm_alt = do InsertCard
             pin <- GetPIN
             cash <- GetAmount
             pinOK <- CheckPIN pin
             Message "Checking Card"
             case pinOK of
                  CorrectPIN => do Dispense cash
                                   EjectCard
                                   Message "Please remove your card and cash"
                  IncorrectPIN => do Message "Incorrect PIN"
                                     EjectCard


text:
module Rationals

import ZZ
import ZZUtils
import GCDZZ
import Divisors

-- The functions below are completely based on the code from GCDZZ; they were written to improve
-- readability.

Quotient: (a: ZZ) -> (b: ZZ) -> (IsNonNegative a) -> (IsPositive b) -> (ZZ)
Quotient a b x y = Prelude.Pairs.DPair.fst (QuotRemZ a b x y)

Remainder: (a: ZZ) -> (b: ZZ) -> (IsNonNegative a) -> (IsPositive b) -> (ZZ)
Remainder a b x y = Prelude.Pairs.DPair.fst(Prelude.Pairs.DPair.snd (QuotRemZ a b x y))

%access public export

Pair : Type
Pair = (Integer, Integer)

ZZPair : Type
ZZPair = (ZZ, ZZ)

ZZtoDb : ZZ -> Double
ZZtoDb x = cast{from=Integer}{to=Double} (cast{from=ZZ}{to=Integer} x)

DbtoZZ : Double -> ZZ
DbtoZZ x = cast{from=Integer}{to=ZZ} (cast{from=Double}{to=Integer} x)

isNotZero :  Nat -> Bool
isNotZero Z = False
isNotZero (S k) = True

isFactorInt : Integer -> Integer -> Type  --Needed for defining Integer division
isFactorInt m n = (k : Integer ** (m * k = n))

divides : (m: Integer) -> (n: Integer) -> (k: Integer ** (m * k = n)) -> Integer
divides m n k = (fst k)

--Integer implemetation of gcd
CalcGCD : (Integer, Integer) -> Integer
CalcGCD (a, b) = if (isNotZero (toNat b)) then next else a where
    next = CalcGCD (b, toIntegerNat (modNat (toNat a) (toNat b)))

OnlyPositive : (x: Pair) -> Pair
OnlyPositive x = (if (fst x)>0 then fst x else (-1)*(fst x), if(snd x)>0 then (snd x) else (-1)*(snd x))

--Integer implemetation of gcd
gccd : (Integer, Integer) -> Integer
gccd x = CalcGCD (OnlyPositive x)

data ZZNotZero : ZZ -> Type where
  ZZOneNotZero : ZZNotZero 1
  ZZNegativeNotZero : ( n: ZZ ) -> ZZNotZero n -> ZZNotZero (-n)
  ZZPositiveNotZero : ( m: ZZ ) -> LTE 1 (fromIntegerNat (cast(m)))  -> ZZNotZero m

--Type for equality of two Rationals
data EqRat : (x: ZZPair) -> (y: ZZPair) -> ((fst x)*(snd y) = (fst y)*(snd x)) -> Type where
  IdEq : (m : ZZPair) -> EqRat m m Refl
  MulEq : (x: ZZPair) -> (y: ZZPair) -> (prf : (fst x)*(snd y) = (fst y)*(snd x)) -> EqRat x y prf

make_rational : (p: Nat) -> (q: ZZ) -> ZZNotZero q -> ZZPair
make_rational p q x = (fromInt(toIntegerNat(p)), q)

InclusionMap : (n : Nat) -> ZZPair --Includes the naturals in Q
InclusionMap n = make_rational n 1 ZZOneNotZero

AddRationals : (x: ZZPair) -> ZZNotZero (snd x) -> (y: ZZPair) -> ZZNotZero (snd y) -> ZZPair
AddRationals x a y b = ((fst x)*(snd y) + (snd x)*(fst y), (snd x)*(snd y))

MultiplyRationals : (x: ZZPair) -> ZZNotZero (snd x) -> (y: ZZPair) -> ZZNotZero (snd y) -> ZZPair
MultiplyRationals x a y b =((fst x)*(fst y), (snd x)*(snd y))

MultInverse : (x: ZZPair) -> ZZNotZero (fst x) -> ZZNotZero (snd x) -> ZZPair
MultInverse x y z = ((snd x), (fst x))

AddInverse : (x: ZZPair) -> ZZNotZero (snd x) -> ZZPair
AddInverse x a = (-(fst x), (snd x))

Subtraction : (x: ZZPair) -> ZZNotZero (snd x) -> (y: ZZPair) -> ZZNotZero (snd y) -> ZZPair
Subtraction x a y b = AddRationals x a (AddInverse y b) b

Division : (x: ZZPair) -> ZZNotZero (snd x) -> (y: ZZPair) -> ZZNotZero (fst y) -> ZZNotZero (snd y) -> ZZPair
Division x a y b c = MultiplyRationals x a (MultInverse y b c) b

Scaling: (a: ZZ) -> (x: ZZPair) -> ZZPair
Scaling a x = (a*(fst x), (snd x))

remZeroDivisible: (a: ZZ) -> (b: ZZ) -> (quot: ZZ) -> (rem: ZZ) -> (a = rem + quot*b) -> (rem = 0) -> (a=quot*b)
remZeroDivisible a b quot rem prf prf1 = rewrite sym (plusZeroLeftNeutralZ (quot*b)) in
                                         rewrite sym prf1 in
                                         prf

IsRationalZ: (x: ZZPair) -> (prf1 :IsNonNegative (fst x)) -> (prf2: IsPositive (snd x)) -> Either (quot: ZZ ** ((fst x)=quot*(snd x))) (NotZero (fst (snd (QuotRemZ (fst x) (snd x) prf1 prf2) )) )
IsRationalZ x prf1 prf2 = case (decEq (fst (snd (QuotRemZ (fst x) (snd x) prf1 prf2))) (Pos Z)) of
                          (Yes prf) => Left ( (Quotient (fst x) (snd x) prf1 prf2) **
                          (remZeroDivisible (fst x) (snd x) (Quotient (fst x) (snd x) prf1 prf2) (Remainder (fst x) (snd x) prf1 prf2) (Prelude.Basics.fst (Prelude.Pairs.DPair.snd (Prelude.Pairs.DPair.snd (QuotRemZ (fst x) (snd x) prf1 prf2)) )) prf ) )
                          (No contra) => Right (nonZeroNotZero (fst (snd (QuotRemZ (fst x) (snd x) prf1 prf2))) contra)

--To prove that the SimplifyRational works, we can just check if the output is equal to the input
-- To be done
simplifyRational : (x : ZZPair) -> ZZPair
simplifyRational (a, b) = (sa, sb) where
  sa = DbtoZZ (da / g) where
    da = ZZtoDb a
    g = cast {from=Integer} {to=Double}
      (gccd (cast {from=ZZ} {to=Integer}a,cast {from=ZZ} {to=Integer}b))
  sb = DbtoZZ (db / g) where
    db = ZZtoDb b
    g = cast {from=Integer} {to=Double}
      (gccd (cast {from=ZZ} {to=Integer}a,cast {from=ZZ} {to=Integer}b))

--Above, I will need to supply a proof that the GCD divides the two numbers. Then, the function defined above will produce the rational in simplified form.

xAndInverseNotZero : (x: ZZPair) -> (k: ZZNotZero (snd x)) -> ZZNotZero (snd (AddInverse x k))
xAndInverseNotZero x (ZZPositiveNotZero (snd x) y) = (ZZPositiveNotZero (snd x) y)

FirstIsInverted : (x: ZZPair) -> (k: ZZNotZero (snd x)) -> (a: ZZ) -> (a = (fst x)) -> ((-a) = fst (AddInverse x k))
FirstIsInverted x k a prf = (apZZ (\x => -x) a (fst x) prf)

SecondStaysSame : (x: ZZPair) -> (k: ZZNotZero (snd x)) -> (b: ZZ) -> (b = (snd x)) -> (b = (snd (AddInverse x k)))
SecondStaysSame x k b prf = (apZZ (\x => x) b (snd x) prf)

xplusinverse: (x: ZZPair) -> (k: ZZNotZero (snd x)) -> ZZPair
xplusinverse x k = AddRationals x k (AddInverse x k) (xAndInverseNotZero x k)

addinverselemma: (a: ZZ) -> (b: ZZ) -> ((-a)=b) -> (a + b = ((-a) + a)) -> ((-a)+a =0 ) -> (a + b = 0)
addinverselemma a b prf prf1 prf2 = trans prf1 prf2

addinverseFST: (x: ZZPair) -> (k: ZZNotZero (snd x)) -> (a: ZZ) -> (a = (fst x)) -> (fst (AddInverse x k) = b) -> ((-a) = b)
addinverseFST x k a prf prf1 = trans (FirstIsInverted x k a prf) (prf1)

addinverseSND: (x: ZZPair) -> (k: ZZNotZero (snd x)) -> (c: ZZ) -> (c = (snd x)) -> (snd (AddInverse x k) = b) -> (c = b)
addinverseSND x k c prf prf1 = trans (SecondStaysSame x k c prf) (prf1)


text:
module Control.Monad.Trans

%default total

public export
interface MonadTrans t where
    lift : Monad m => m a -> t m a


text:
module Main

import Chez

display : String -> SIO ()
display s = foreign FFI_S "display" (String -> SIO ()) s

displayBool : Bool -> SIO ()
displayBool b = foreign FFI_S "display" (Bool -> SIO ()) b

schemeEqual : Int -> Int -> SIO Bool
schemeEqual x y = foreign FFI_S "=" (Int -> Int -> SIO Bool) x y

main : SIO ()
main = do
    display "O RLY?"
    displayBool True
    a <-  schemeEqual 1 2
    displayBool a

max_stars_repo_name: melted/idris-chez

max_issues_repo_name: melted/idris-chez

max_forks_repo_name: melted/idris-chez


text:
-- Module      : Itea.Utils
-- Description :
-- Copyright   : (c) Simon Nielsen Knights 2018
-- License     : MIT
-- Maintainer  : simonank@mail.ru
-- Stability   : unstable
-- Portability : portable

module Itea.Utils
import Language.Reflection.Utils

%language ElabReflection
%default total
%access public export

jsbool : Bool -> Int
jsbool True = 1
jsbool False = 0

||| Call a native javascript procedure
|||
||| @native Javascript procedure/expression to call
||| @type type of given procedure/expression
||| @ok proof that the given type satisfies the FFI_JS interface
jscall : (native : String)
      -> (type : Type)
      -> { auto ok : FTy FFI_JS [] type }
      -> type
jscall name type = foreign FFI_JS name type

||| Log a string to the console
consoleLog : String -> JS_IO ()
consoleLog = jscall "console.log(%0)" (String -> JS_IO ())

||| Display the alert dialog with given text
alert : String -> JS_IO ()
alert = jscall "alert(%0)" (String -> JS_IO ())

||| Print a message for debugging with source location as a side effect
|||
||| @loc call site location
||| @message message to display
||| @result the result returned
trace : {default (%runElab sourceLocation) loc : SourceLocation}
     -> (message : String)
     -> (result : a)
     -> a
trace {loc} text res = unsafePerformIO {ffi=FFI_JS}
  (consoleLog ("[T] " ++ show loc ++ "::" ++ text) *> pure res)
-- %deprecated trace "Debug function `trace' used in source file"

||| Index a list given a constructor/function and a stream of values
indexdWith : (f : (a -> b -> c)) -> Stream a -> List b -> List c
indexdWith _ _ [] = []
indexdWith f (x :: xs) (y :: ys) = f x y :: indexdWith f xs ys

||| Index a list elements with their position
indexed : (Enum b, Num b) => List a -> List (b, a)
indexed = indexdWith MkPair [0..]

max_stars_repo_name: simonank/idris-tea

max_issues_repo_name: simonank/idris-tea

max_forks_repo_name: simonank/idris-tea


text:
main : IO ()
main = do putStrLn "RVM code:"
          putStrLn ");'u?>vD?>vRD?>vRA?>vRA?>vR:?>vR=!(:lkm!':lkv6y" -- RVM code that prints HELLO!

max_stars_repo_name: zwizwa/ribbit

max_issues_repo_name: zwizwa/ribbit

max_forks_repo_name: zwizwa/ribbit


text:
module Utils.Bytes

import Syntax.WithProof
import Data.Bits
import Data.DPair
import Data.Fin
import Data.Fin.Extra
import Data.Nat
import Data.List
import Data.Vect
import Data.Nat.Factor
import Data.Nat.Order.Properties
import Utils.Misc

weakenN' : {m : Nat} -> (0 n : Nat) -> Fin m -> Fin (n + m)
weakenN' n m' = rewrite plusCommutative n m in weakenN n m'

fix_fin : (m : Nat) -> (n : Nat) -> (S m) = n -> S (S (S (S (S (S (S (S (mult m 8)))))))) = mult n 8
fix_fin m n prf = rewrite sym prf in Refl

export
to_le : (FiniteBits a, Cast a Bits8) => {n : _} -> {auto 0 no0 : NonZero n} -> {auto 0 prf : n * 8 = (bitSize {a})} -> a -> Vect n Bits8
to_le x = let (S m) = n; nmeq = Refl in map (go nmeq x) Fin.range
  where
    go : {m : Nat} -> ((S m) = n) -> a -> Fin (S m) -> Bits8
    go nmeq b i = cast $ shiftR b (bitsToIndex $ coerce prf $ coerce (fix_fin m n nmeq) $ weakenN' 7 $ i * 8)

export
to_be : (FiniteBits a, Cast a Bits8) => {n : _} -> {auto 0 no0 : NonZero n} -> {auto 0 prf : n * 8 = (bitSize {a})} -> a -> Vect n Bits8
to_be = reverse . to_le

export
from_le : (FiniteBits a, Cast Bits8 a) => {n : _} -> {auto 0 no0 : NonZero n} -> {auto 0 prf : n * 8 = (bitSize {a})} -> Vect n Bits8 -> a
from_le p = let (S m) = n; nmeq = Refl in foldl (.|.) zeroBits $ zipWith (go nmeq) p Fin.range
  where
    go : {m : Nat} -> ((S m) = n) -> Bits8 -> Fin (S m) -> a
    go nmeq b i = shiftL (cast b) (bitsToIndex $ coerce prf $ coerce (fix_fin m n nmeq) $ weakenN' 7 $ i * 8)

export
from_be : (FiniteBits a, Cast Bits8 a) => {n : _} -> {auto 0 no0 : NonZero n} -> {auto 0 prf :  n * 8 = (bitSize {a})} -> Vect n Bits8 -> a
from_be = from_le . reverse

export
set_bit_to : Bits a => Bool -> Index {a} -> a -> a
set_bit_to False _ x = x
set_bit_to True pos x = setBit x pos

export
to_bools_be' : FiniteBits a => (n : Fin (S (bitSize {a}))) -> a -> Vect (finToNat n) Bool
to_bools_be' FZ x = []
to_bools_be' (FS wit) x = testBit x (bitsToIndex wit) :: (replace_vect finToNatWeakenNeutral $ to_bools_be' (weaken wit) x)

export
to_bools_be : FiniteBits a => a -> Vect (bitSize {a}) Bool
to_bools_be x = replace_vect finToNatLastIsBound $ to_bools_be' {a = a} Fin.last x

export
le_to_integer : Foldable t => t Bits8 -> Integer
le_to_integer = go . toList
  where
  go : List Bits8 -> Integer
  go v = foldr (.|.) 0 $ zipWith shiftL (cast {to=Integer} <$> v) ((*8) <$> [0..(length v)])

export
be_to_integer : Foldable t => t Bits8 -> Integer
be_to_integer = le_to_integer . reverse . toList

export
integer_to_le : (n : Nat) -> Integer -> Vect n Bits8
integer_to_le n v = (cast . shiftR v) <$> (((*8) . finToNat) <$> Fin.range)

export
integer_to_be : (n : Nat) -> Integer -> Vect n Bits8
integer_to_be n = reverse . integer_to_le n

export
to_digit : Bool -> Char
to_digit False = '0'
to_digit True = '1'

export
show_bin : FiniteBits a => a -> String
show_bin = pack . toList . map to_digit . to_bools_be

||| if 0-15, then return the corresponding hex char
||| otherwise returns a '?'
export
hex_lower : Bits8 -> Char
hex_lower 0 = '0'
hex_lower 1 = '1'
hex_lower 2 = '2'
hex_lower 3 = '3'
hex_lower 4 = '4'
hex_lower 5 = '5'
hex_lower 6 = '6'
hex_lower 7 = '7'
hex_lower 8 = '8'
hex_lower 9 = '9'
hex_lower 10 = 'a'
hex_lower 11 = 'b'
hex_lower 12 = 'c'
hex_lower 13 = 'd'
hex_lower 14 = 'e'
hex_lower 15 = 'f'
hex_lower _ = '?'

export
show_hex : Bits8 -> String
show_hex x = strCons (hex_lower (div x 16)) $ strCons (hex_lower (mod x 16)) $ ""

||| takes a list of bytes and show them using `show_hex` interspersed by a whitespace
export
xxd : Foldable t => t Bits8 -> String
xxd = concat . intersperse " " . map show_hex . toList

export
string_to_ascii : (x : String) -> List Bits8
string_to_ascii = map (cast . ord) . unpack

export
ascii_to_string : List Bits8 -> String
ascii_to_string = pack . map cast

maybe_a_a : Lazy a -> Maybe a -> a
maybe_a_a a Nothing  = Force a
maybe_a_a _ (Just a) = a

export
shiftL' : FiniteBits a => a -> Nat -> a
shiftL' x i = maybe_a_a zeroBits $ do
  i' <- natToFin i _
  Just $ shiftL x (bitsToIndex i')

export
shiftR' : FiniteBits a => a -> Nat -> a
shiftR' x i = maybe_a_a zeroBits $ do
  i' <- natToFin i _
  Just $ shiftR x (bitsToIndex i')

export
rotl : FiniteBits a => {n : Nat} -> {auto prf : ((S n) = bitSize {a})} -> Fin (S n) -> a -> a
rotl FZ x = x
rotl (FS i) x = (shiftL x $ bitsToIndex (coerce prf $ FS i)) .|. (shiftR x $ bitsToIndex $ invFin $ coerce prf $ weaken i)

export
rotr : FiniteBits a => {n : Nat} -> {auto prf : ((S n) = bitSize {a})} -> Fin (S n) -> a -> a
rotr FZ x = x
rotr (FS i) x = (shiftR x $ bitsToIndex (coerce prf $ FS i)) .|. (shiftL x $ bitsToIndex $ invFin $ coerce prf $ weaken i)


text:
{-

1. (String, String, String)
   List String
   ((Char, String), Char)

-}

{- 2 -}

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

{- 3 -}

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

{- 4 -}

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

{- 5 -}

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

{- 6 -}

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

{- 7 -}

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

{- 8 -}

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

max_stars_repo_name: PiotrJander/TypeDD-Samples

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
module lib.Library1

import lib.Library2

export
salute1 : String
salute1 = "Hello, I'm library 1, and there is someone who wants to say something\n" ++ salute2


text:
module Control.Monad.Trans

public export
interface MonadTrans (t : (Type -> Type) -> Type -> Type) where
    lift : Monad m => m a -> t m a


text:
module Y

import X

h : f 0 = A
h = Refl

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
%default partial

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

zip : Vect n a -> Vect n b -> Vect n (a, b)
zip [] [] impossible
zip (x :: xs) (y :: ys) = (x, y) :: zip xs ys


text:
> module Data.List.TypeEnumeration
> import Data.List
> import Data.List.DecIn
> import Functions
> %access public export

This module contains utilities for "enumerating a type" by placing all elements
of that type into a list. It contains two basic quantifiers on a type `t` and a
list `xs : List t`:

- `All {t} xs`, proofs that `xs` contains every element of `t`
- `NoDupes {t} xs`, proofs that `xs` contains no duplicate elements of `t`

First we start with `All {t} xs`: how can we determine if `xs` contains every
element of `t`? If this were the case, we would be able to construct a
function $f_{xs} : (x:t) \rightarrow \texttt{Elem} x xs$.

> ||| Proofs that a given list contains all possible elements of a given type.
> All : {t : Type} -> List t -> Type
> All xs {t} = (x:t) -> Elem x xs

There are some boilerplate and uninhabited trivialities to get out of the way.

> ||| Given a type t and a proof of t, it is a contradiction to have a proof that
> ||| the empty list contains all elements of t.
> allNotEmpty : All {t} [] -> t -> Void
> allNotEmpty f x = absurd (f x)

> ||| If a type `t` is uninhabited, then the empty list contains all elements
> ||| of that type.
> voidEmptyAll : Uninhabited t => All {t} []
> voidEmptyAll = \c => absurd c

Proofs that a list contains some elements of $t$ with no duplicates are defined by

> ||| Proofs that a list contains  no duplicates.
> NoDupes : {t:Type} -> List t -> Type
> NoDupes {t} xs = (x:t) -> Prop (Elem x xs)

With this we can start working on proving if a given list uniquely contains all
elements of a given type. We start with some trivial helper lemmas:

> ||| If we know $x$ belongs to a list $xs$ then $x :: xs$ obviously contains
> ||| duplicate values (namely, $x$).
> noDupesInHeadLemma : Elem x xs -> NoDupes (x :: xs) -> Void
> noDupesInHeadLemma {x = x} {xs = []} _ _ impossible
> noDupesInHeadLemma {x} a b = hereIsNotThere (b x Here (There a))

If a type has decidable equality, then All and NoDupes are decidable.
We need a (somewhat metamathematical) lemma to start stating that any two
void values of the same type are equal (there are in fact zero of them - this
is just a wrapper for "void can prove anything")

> ||| Any two contradictions of the same type are identical.
> voidsAreEquivalent : {t: Type} -> (t -> Void) -> (a:t) -> (b:t) -> (a=b)
> voidsAreEquivalent f a b = void (f a)

> ||| Equivalent to `There` being an injective function.
> thereLemma2 : {a: Elem x xs} -> {b : Elem x xs} -> (There a = There b) -> a = b
> thereLemma2 {a = Here} {b = Here} pf = Refl
> thereLemma2 {a = Here} {b = (There _)} Refl impossible
> thereLemma2 {a = (There _)} {b = Here} Refl impossible
> thereLemma2 {a = (There x)} {b = (There x)} Refl = Refl

> ||| For fixed $y$, `There` is an injective function from `Elem x xs` to
> ||| `Elem x (y :: xs)`.
> thereInjective : Injective There
> thereInjective x y = thereLemma2 {a=x} {b=y}

> ||| Given a list `xs` without duplicates, and an element `x` known not to be
> ||| contained in `xs`, then `x :: xs` also contains no duplicates.
> consNoDupes : DecEq t => {x : t} -> NoDupes {t} xs -> (Not (Elem x xs)) -> NoDupes (x :: xs)
> consNoDupes {x = x} noDupesSublist notIn y pf1 pf2 with (decEq x y)
>   consNoDupes {x = y} noDupesSublist notIn y Here Here | Yes pf = Refl
>   consNoDupes {x = y} noDupesSublist notIn y Here (There later) | Yes pf =
>               absurd (notIn later)
>   consNoDupes {x = y} noDupesSublist notIn y (There later) Here | Yes pf =
>               absurd (notIn later)
>   consNoDupes {x = x} noDupesSublist notIn y (There later) (There z) | Yes pf =
>               absurd (notIn (rewrite pf in later))
>   consNoDupes {x = y} noDupesSublist notIn y Here Here | No contra = Refl
>   consNoDupes {x = y} noDupesSublist notIn y Here (There later) | No contra =
>               absurd (notIn later)
>   consNoDupes {x = y} noDupesSublist notIn y (There later) Here | No contra =
>               absurd (notIn later)
>   consNoDupes {x = x} noDupesSublist notIn y (There later) (There z) | No contra =
>               let ndupes = (noDupesSublist y later z) in cong ndupes

> ||| If a nonempty list contains no duplicates, then its tail has no duplicates.
> dupeCons : NoDupes (x :: xs) -> NoDupes xs
> dupeCons dupeBiglist item pf1 pf2 = thereLemma2 (dupeBiglist item (There pf1) (There pf2))

> ||| If a type `t` has decidable equality, then `List t` has a decision
> ||| procedure for determining if it contains any duplicates.
> deqEqToDupe : DecEq t => (xs:List t) -> Dec (NoDupes xs)
> deqEqToDupe [] = Yes (\a => (\b => (\c => (voidsAreEquivalent uninhabited b c))))
> deqEqToDupe (x :: xs) with (isElem x xs)
>   deqEqToDupe (x :: xs) | Yes pf = No (noDupesInHeadLemma pf)
>   deqEqToDupe (x :: xs) | No contra = case deqEqToDupe xs of
>       Yes noDupes => Yes (consNoDupes noDupes contra)
>       No areDupes => No (\c => areDupes (dupeCons c))

Decidable list membership allows us to remove duplicates from a list:

> ||| Given an input list `xs`, return a list `ys` satisfying the following:
> ||| - `Elem y ys` has at most one element up to equality (`NoDupes ys`)
> ||| - Given a proof `Elem x xs` (resp `Elem x ys`) we have a proof `Elem x ys`
> ||| (resp `Elem x xs`) (`ElementPreservingCorrespondence xs ys`)
> remDup : DecIn t => (xs : List t) -> (ys ** (NoDupes ys, ElementPreservingCorrespondence xs ys))

max_stars_repo_name: nicklecompte/idris-finite-sets

max_issues_repo_name: nicklecompte/idris-finite-sets

max_forks_repo_name: nicklecompte/idris-finite-sets


text:
module InfIO

data InfIO : Type where
     Do : IO a
          -> (a -> Inf InfIO)
          -> InfIO

data Fuel = Dry | More (Lazy Fuel)

(>>=) : IO a -> (a -> Inf InfIO) -> InfIO
(>>=) = Do

forever : Fuel
forever = More forever

tank : Nat -> Fuel
tank Z = Dry
tank (S k) = More $ tank k

run : Fuel -> InfIO -> IO ()
run Dry (Do action cont) = putStrLn "Out of fuel."
run (More x) (Do action cont) = action >>= \res => run x $ cont res

loopPrint : String -> InfIO
loopPrint m = Do (putStrLn m) (\_ => loopPrint m)

lp : String -> InfIO
lp m = do putStrLn m
          lp m

max_stars_repo_path: Chapter 11/InfIO.idr

max_issues_repo_path: Chapter 11/InfIO.idr

max_forks_repo_path: Chapter 11/InfIO.idr


text:
module Language.Reflection.TTImp

import public Language.Reflection.TT

%default total

-- Unchecked terms and declarations in the intermediate language
mutual
  public export
  data BindMode = PI Count | PATTERN | NONE

  -- For as patterns matching linear arguments, select which side is
  -- consumed
  public export
  data UseSide = UseLeft | UseRight

  public export
  data DotReason = NonLinearVar
                 | VarApplied
                 | NotConstructor
                 | ErasedArg
                 | UserDotted
                 | UnknownDot
                 | UnderAppliedCon

  public export
  data TTImp : Type where
       IVar : FC -> Name -> TTImp
       IPi : FC -> Count -> PiInfo TTImp -> Maybe Name ->
             (argTy : TTImp) -> (retTy : TTImp) -> TTImp
       ILam : FC -> Count -> PiInfo TTImp -> Maybe Name ->
              (argTy : TTImp) -> (lamTy : TTImp) -> TTImp
       ILet : FC -> (lhsFC : FC) -> Count -> Name ->
              (nTy : TTImp) -> (nVal : TTImp) ->
              (scope : TTImp) -> TTImp
       ICase : FC -> TTImp -> (ty : TTImp) ->
               List Clause -> TTImp
       ILocal : FC -> List Decl -> TTImp -> TTImp
       IUpdate : FC -> List IFieldUpdate -> TTImp -> TTImp

       IApp : FC -> TTImp -> TTImp -> TTImp
       INamedApp : FC -> TTImp -> Name -> TTImp -> TTImp
       IAutoApp : FC -> TTImp -> TTImp -> TTImp
       IWithApp : FC -> TTImp -> TTImp -> TTImp

       ISearch : FC -> (depth : Nat) -> TTImp
       IAlternative : FC -> AltType -> List TTImp -> TTImp
       IRewrite : FC -> TTImp -> TTImp -> TTImp

       -- Any implicit bindings in the scope should be bound here, using
       -- the given binder
       IBindHere : FC -> BindMode -> TTImp -> TTImp
       -- A name which should be implicitly bound
       IBindVar : FC -> String -> TTImp
       -- An 'as' pattern, valid on the LHS of a clause only
       IAs : FC -> (nameFC : FC) -> UseSide -> Name -> TTImp -> TTImp
       -- A 'dot' pattern, i.e. one which must also have the given value
       -- by unification
       IMustUnify : FC -> DotReason -> TTImp -> TTImp

       -- Laziness annotations
       IDelayed : FC -> LazyReason -> TTImp -> TTImp -- the type
       IDelay : FC -> TTImp -> TTImp -- delay constructor
       IForce : FC -> TTImp -> TTImp

       -- Quasiquotation
       IQuote : FC -> TTImp -> TTImp
       IQuoteName : FC -> Name -> TTImp
       IQuoteDecl : FC -> List Decl -> TTImp
       IUnquote : FC -> TTImp -> TTImp

       IPrimVal : FC -> (c : Constant) -> TTImp
       IType : FC -> TTImp
       IHole : FC -> String -> TTImp

       -- An implicit value, solved by unification, but which will also be
       -- bound (either as a pattern variable or a type variable) if unsolved
       -- at the end of elaborator
       Implicit : FC -> (bindIfUnsolved : Bool) -> TTImp
       IWithUnambigNames : FC -> List Name -> TTImp -> TTImp

  public export
  data IFieldUpdate : Type where
       ISetField : (path : List String) -> TTImp -> IFieldUpdate
       ISetFieldApp : (path : List String) -> TTImp -> IFieldUpdate

  public export
  data AltType : Type where
       FirstSuccess : AltType
       Unique : AltType
       UniqueDefault : TTImp -> AltType

  public export
  data FnOpt : Type where
       Inline : FnOpt
       TCInline : FnOpt
       -- Flag means the hint is a direct hint, not a function which might
       -- find the result (e.g. chasing parent interface dictionaries)
       Hint : Bool -> FnOpt
       -- Flag means to use as a default if all else fails
       GlobalHint : Bool -> FnOpt
       ExternFn : FnOpt
       -- Defined externally, list calling conventions
       ForeignFn : List TTImp -> FnOpt
       -- assume safe to cancel arguments in unification
       Invertible : FnOpt
       Totality : TotalReq -> FnOpt
       Macro : FnOpt
       SpecArgs : List Name -> FnOpt

  public export
  data ITy : Type where
       MkTy : FC -> (nameFC : FC) -> (n : Name) -> (ty : TTImp) -> ITy

  public export
  data DataOpt : Type where
       SearchBy : List Name -> DataOpt -- determining arguments
       NoHints : DataOpt -- Don't generate search hints for constructors
       UniqueSearch : DataOpt -- auto implicit search must check result is unique
       External : DataOpt -- implemented externally
       NoNewtype : DataOpt -- don't apply newtype optimisation

  public export
  data Data : Type where
       MkData : FC -> (n : Name) -> (tycon : TTImp) ->
                (opts : List DataOpt) ->
                (datacons : List ITy) -> Data
       MkLater : FC -> (n : Name) -> (tycon : TTImp) -> Data

  public export
  data IField : Type where
       MkIField : FC -> Count -> PiInfo TTImp -> Name -> TTImp ->
                  IField

  public export
  data Record : Type where
       MkRecord : FC -> (n : Name) ->
                  (params : List (Name, Count, PiInfo TTImp, TTImp)) ->
                  (conName : Name) ->
                  (fields : List IField) ->
                  Record

  public export
  data WithFlag = Syntactic

  public export
  data Clause : Type where
       PatClause : FC -> (lhs : TTImp) -> (rhs : TTImp) -> Clause
       WithClause : FC -> (lhs : TTImp) -> (wval : TTImp) ->
                    (prf : Maybe Name) -> (flags : List WithFlag) ->
                    List Clause -> Clause
       ImpossibleClause : FC -> (lhs : TTImp) -> Clause

  public export
  data Decl : Type where
       IClaim : FC -> Count -> Visibility -> List FnOpt ->
                ITy -> Decl
       IData : FC -> Visibility -> Data -> Decl
       IDef : FC -> Name -> List Clause -> Decl
       IParameters : FC -> List (Name, Count, PiInfo TTImp, TTImp) ->
                     List Decl -> Decl
       IRecord : FC ->
                 Maybe String -> -- nested namespace
                 Visibility -> Record -> Decl
       INamespace : FC -> Namespace -> List Decl -> Decl
       ITransform : FC -> Name -> TTImp -> TTImp -> Decl
       IRunElabDecl : FC -> TTImp -> Decl
       ILog : Maybe (List String, Nat) -> Decl
       IBuiltin : FC -> BuiltinType -> Name -> Decl

public export
getFC : TTImp -> FC
getFC (IVar fc y)                = fc
getFC (IPi fc _ _ _ _ _)         = fc
getFC (ILam fc _ _ _ _ _)        = fc
getFC (ILet fc _ _ _ _ _ _)      = fc
getFC (ICase fc _ _ _)           = fc
getFC (ILocal fc _ _)            = fc
getFC (IUpdate fc _ _)           = fc
getFC (IApp fc _ _)              = fc
getFC (INamedApp fc _ _ _)       = fc
getFC (IAutoApp fc _ _)          = fc
getFC (IWithApp fc _ _)          = fc
getFC (ISearch fc _)             = fc
getFC (IAlternative fc _ _)      = fc
getFC (IRewrite fc _ _)          = fc
getFC (IBindHere fc _ _)         = fc
getFC (IBindVar fc _)            = fc
getFC (IAs fc _ _ _ _)           = fc
getFC (IMustUnify fc _ _)        = fc
getFC (IDelayed fc _ _)          = fc
getFC (IDelay fc _)              = fc
getFC (IForce fc _)              = fc
getFC (IQuote fc _)              = fc
getFC (IQuoteName fc _)          = fc
getFC (IQuoteDecl fc _)          = fc
getFC (IUnquote fc _)            = fc
getFC (IPrimVal fc _)            = fc
getFC (IType fc)                 = fc
getFC (IHole fc _)               = fc
getFC (Implicit fc _)            = fc
getFC (IWithUnambigNames fc _ _) = fc


text:
module Dart.FFI.Types

import public Dart.FFI.Constructors

||| Represents a Dart generic type.
public export
data GenericType : String -> List Type -> Type where [external]

||| Represents a Dart nullable type (T?).
export
data Nullable : a -> Type where [external]

infixl 9 @.

||| Object-oriented method invocation syntax.
%inline
public export
(@.) : a -> (a -> b) -> b
(@.) x f = f x

export
Cast a (Nullable a) where
  cast a = believe_me a


text:
import Data.Buffer

export
data ForeignPtr : Type -> Type where
  MkFP : Buffer -> ForeignPtr a

public export
interface Storable a where
  size : Int

  peekByteOff : HasIO io => ForeignPtr a -> Int -> io a

  peekElemOff : HasIO io => ForeignPtr a -> Int -> io a
  peekElemOff fp off = peekByteOff fp (off * size {a})

Storable Bits8 where
  size = 8
  peekByteOff (MkFP b) off = getBits8 b off


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

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

%default total

namespace Export
  public export %hint cobblestoneBlock : Block Cobblestone.Block
  public export %hint breakCobblestone : Break Cobblestone.Block
  public export %hint cobblestoneVtbl  : Vtbl  Cobblestone.Block


text:
module Examples.AOC3

import Data.String
import Data.List
import Data.Nat

import Stream
import System
import System.File

accum : List Int32 -> String -> List Int32
accum xs s = case trim s of
  "" => xs
  s2 => zipWith (+) xs (map dec $ unpack s2)
  where dec : Char -> Int32
        dec '0' = -1
        dec _   = 1

encode : List Int32 -> Bits32
encode = foldl (\acc,x => 2 * acc + (if x > 0 then 1 else 0)) 0

export
part1 : IO ()
part1 = ignore $ withLines "resources/aoc3a" $ \ls => do
  cs <- run $ fold_ accum (replicate 200 0) id ls
  let g = encode cs
      e = encode (map negate cs)
  putStrLn "Day3, Result A: \{show $ g * e} (g: \{show g}, e: \{show e}, acc: \{show cs})"

export
part2 : IO ()
part2 = pure ()


text:
module FVect

import Data.Vect
import Data.Fin
import Data.Nat
import Decidable.Equality

%hide Data.Vect.elem
%hide Prelude.Types.elem

%default total

||| A Fin-based Vect. Can be thought of as a Vect with both a length and
||| a maximum capacity. Operations like filtering can reduce the length
||| without affecting maximum capacity which provides proof that a Vect's
||| length has not increased over the course of a series of operations.
public export
data FVect : (capacity : Nat) -> (len : Fin (S capacity)) -> (elem : Type) -> Type where
  Nil : FVect capacity FZ elem

  ||| Cons an element to the FVect, increasing its capacity.
  ||| See (:::) for an operator that conses an element without
  ||| increasing capacity.
  (::) : (x : elem)
      -> (xs : FVect capacity len elem)
      -> FVect (S capacity) (FS len) elem

%name FVect xs, ys, zs

Uninhabited (FVect 0 (FS l) e) where
  uninhabited [] impossible
  uninhabited (x :: xs) impossible

||| Cons an element without increasing the capacity of the FVect.
||| You must make sure the capacity and length of the FVect being
||| consed onto are accessible in the context where you call this.
|||
||| The function signature is a bit tricky because it needs to
||| ensure you are going from length of type Fin n to length of
||| type Fin n but calling Fin's FS constructor increments n.
||| To increment the value stored without weakening the bounds of
||| the Fin, we go from (weaken (Fin (S n))) to (FS (Fin (S n))).
|||
||| In other words, we go from a weaker input Fin to the succesor of a
||| stronger bounded Fin.
public export
(:::) : {n : Nat}
     -> {len' : Fin (S n)}
     -> (v : elem)
     -> FVect (S n) (weaken len') elem
     -> FVect (S n) (FS len') elem
(:::) {n = n}     {len' = FZ}      v _ = [v]
(:::) {n = 0}     {len' = (FS l')} _ _ = absurd l'
(:::) {n = (S k)} {len' = (FS l')} v (x :: xs) = v :: (x ::: xs)

||| Create an empty FVect with the given capacity.
export
empty : (capacity : Nat) -> FVect capacity FZ elem
empty _ = []

||| Create an FVect by replicating the given element
||| enough to fill the needed length.
export
replicate : {capacity : Nat} -> (l : Fin (S capacity)) -> elem -> FVect capacity l elem
replicate {capacity} FZ x = []
replicate {capacity = (S k)} (FS y) x = x :: replicate y x

||| Allow FVect to hold one more element.
||| Do not change the elements currently in the FVect.
public export
addCapacity : FVect c l a -> (FVect (S c) (weaken l) a)
addCapacity [] = []
addCapacity (x :: xs) = x :: (addCapacity xs)

||| Allow FVect to hold n more elements.
||| Do not change the elements currently in the FVect.
public export
addCapacityN : (n : Nat)
            -> FVect capacity l a
            -> (FVect (capacity + n) (weakenN n l) a)
addCapacityN n [] = Nil
addCapacityN n (x :: xs) = x :: (addCapacityN n xs)

||| Reduce the FVect's capacity to hold elements.
public export
removeCapacity : {n : Nat}
              -> {len' : Fin (S n)}
              -> FVect (S n) (weaken len') a
              -> FVect n len' a
removeCapacity {n = n}     {len' = FZ}      [] = []
removeCapacity {n = 0}     {len' = (FS l')} (x :: xs) = absurd l'
removeCapacity {n = (S k)} {len' = (FS l')} (x :: xs) = x :: (removeCapacity xs)

||| Calculate the length of the FVect.
export
length : FVect capacity l a
      -> Nat
length [] = 0
length (x :: xs) = S (length xs)

--
-- to/from List and Vect
--

||| Get the smallest FVect that can contain the given Vect.
export
fromVect : Vect l a -> FVect l (last {n=l}) a
fromVect [] = []
fromVect (x :: xs) = x :: fromVect xs

export
toVect : FVect c l elem -> Vect (finToNat l) elem
toVect [] = []
toVect (x :: xs) = x :: (toVect xs)

-- toList provided by Foldable/Data.List

--
-- Accessors
--

||| All but the first element of the FVect.
||| This operation does not change capacity. This means you can
||| carry out this operation and retain proof that the new FVect
||| length is less than or equal to the original FVect (although
||| in this case the length is exactly one less than before the
||| call to tail).
public export
tail : FVect c (FS l) elem -> FVect c (weaken l) elem
tail (x :: xs) = addCapacity xs

||| Like tail but reduces the capacity by 1 in addition
||| to dropping the first element.
public export
dropFirst : FVect (S c) (FS l) elem -> FVect c l elem
dropFirst (x :: xs) = xs

public export
head : FVect c (FS l) elem -> elem
head (x :: _) = x

public export
last : FVect c (FS l) elem -> elem
last [x] = x
last (x :: (y :: xs)) = last $ y :: xs

||| All but the last element of the FVect.
||| This operation does not change capacity. This means you can
||| carry out this operation and retain proof that the new FVect
||| length is less than or equal to the original FVect (although
||| in this case the length is exactly one less than before the
||| call to tail).
public export
init : FVect c (FS l) elem -> FVect c (weaken l) elem
init [_] = []
init (x :: (y :: xs)) = x :: (init $ y :: xs)

||| Like init but reduces the capacity by 1 in addition
||| to removing the last element.
public export
dropLast : FVect (S c) (FS l) elem -> FVect c l elem
dropLast [_] = []
dropLast (x :: (y :: xs)) = x :: (dropLast $ y :: xs)

--
-- Properties
--

||| If two FVects are equal, their heads and tails are equal.
export
fVectInjective : {0 xs : FVect c l elem}
              -> {0 ys : FVect c l elem}
              -> x :: xs = y :: ys
              -> (x = y, xs = ys)
fVectInjective Refl = (Refl, Refl)

--
-- Functor
--

export
Functor (FVect c l) where
  map f [] = []
  map f (x :: xs) = f x :: map f xs

--
-- Applicative
--

export
{capacity : Nat} -> {l : Fin (S capacity)} -> Applicative (FVect capacity l) where
  pure = replicate _

  [] <*> [] = []
  (f :: fs) <*> (x :: xs) = f x :: (fs <*> xs)

--
-- Foldable
--

export
Foldable (FVect c l) where
  foldr _ acc [] = acc
  foldr f acc (x :: xs) = f x $ foldr f acc xs

--
-- Eq/DecEq
--

export
Eq elem => Eq (FVect c l elem) where
  [] == [] = True
  (x :: xs) == (y :: ys) = if x == y
                              then xs == ys
                              else False

export
DecEq elem => DecEq (FVect c l elem) where
  decEq [] [] = Yes Refl
  decEq (x :: xs) (y :: ys) with (decEq x y, decEq xs ys)
    decEq (y :: ys) (y :: ys) | (Yes Refl, Yes Refl)  = Yes Refl
    decEq (x :: xs) (y :: ys) | (_,        No contra) = No $ contra . snd . fVectInjective
    decEq (x :: xs) (y :: ys) | (No contra, _)        = No $ contra . fst . fVectInjective

--
-- Utility
--

||| Remove all Nothings from the FVect.
||| This operation does not change capacity. That means you can
||| carry out this operation and retain proof that the new FVect
||| length is less than or equal to that of the original FVect.
export
catMaybes : {len : Fin (S capacity)}
         -> FVect capacity len (Maybe elem)
         -> (len' : Fin (S capacity) ** FVect capacity len' elem)
catMaybes {len = FZ} [] = (FZ ** [])
catMaybes {len = (FS k)} (Nothing  :: xs) = let (l' ** rest) = catMaybes xs in
                                              (weaken l' ** addCapacity rest)
catMaybes {len = (FS k)} ((Just x) :: xs) = let (l' ** rest) = catMaybes xs in
                                              (FS l' ** x :: rest)

||| Map all elements, removing any Nothings along the way.
||| This operation does not change capacity. That means you can
||| carry out this operation and retain proof that the new FVect
||| length is less than or equal to that of the original FVect.
export
mapMaybes : {len : Fin (S capacity)}
         -> (f : elem -> Maybe elem')
         -> FVect capacity len elem
         -> (len' : Fin (S capacity) ** FVect capacity len' elem')
mapMaybes {len = FZ} f [] = (FZ ** [])
mapMaybes {len = (FS k)} f (x :: xs) = case (f x) of
                                            Nothing => let (l' ** rest) = mapMaybes f xs in
                                                           (weaken l' ** addCapacity rest)
                                            (Just y) => let (l' ** rest) = mapMaybes f xs in
                                                            (FS l' ** y :: rest)

||| Filter down to only elements matching the predicate.
||| This operation does not change capacity. That means you can
||| carry out this operation and retain proof that the new FVect
||| length is less than or equal to that of the original FVect.
export
filter : (elem -> Bool)
      -> FVect capacity len elem
      -> (len' : Fin (S capacity) ** FVect capacity len' elem)
filter p [] = (FZ ** [])
filter p (x :: xs) = let (l' ** rest) = filter p xs in
                         if p x
                            then (FS l' ** x :: rest)
                            else (weaken l' ** addCapacity rest)

max_stars_repo_name: mattpolzin/idris-fvect

max_issues_repo_name: mattpolzin/idris-fvect

max_forks_repo_name: mattpolzin/idris-fvect


text:
module LightClick.IR.Channel.MicroSV.InterpTy

import LightClick.IR.ModuleCentric
import LightClick.Types.Direction

import Language.SystemVerilog.MetaTypes
import Language.SystemVerilog.Direction

%default total

total
export
interpDir : Types.Direction.Direction -> SystemVerilog.Direction.Direction
interpDir IN = IN
interpDir OUT = OUT
interpDir INOUT = INOUT

public export
data InterpTy : TyIR -> Ty -> Type where
  PP : (x : String) -> InterpTy PORT   (PORT x)
  UU : InterpTy UNIT   UNIT
  MM : (xs : List String) -> InterpTy MODULE (MODULE xs)
  CM : (xs : List String) -> InterpTy CONN   (MINST xs)
  DD : InterpTy DATA   DATA
  CC : InterpTy CHAN   CHAN
  GG : InterpTy GATE   GINST

public export
getTy : {ty : Ty} -> InterpTy type ty -> Ty
getTy {ty} _ = ty

-- Ports

portMod : InterpTy PORT (MODULE xs) -> Void
portMod (PP _) impossible
portMod UU impossible
portMod (MM _) impossible
portMod (CM _) impossible
portMod DD impossible
portMod CC impossible
portMod GG impossible

portDat : InterpTy PORT DATA -> Void
portDat (PP _) impossible
portDat UU impossible
portDat (MM _) impossible
portDat (CM _) impossible
portDat DD impossible
portDat CC impossible
portDat GG impossible

portCha : InterpTy PORT CHAN -> Void
portCha (PP _) impossible
portCha UU impossible
portCha (MM _) impossible
portCha (CM _) impossible
portCha DD impossible
portCha CC impossible
portCha GG impossible

portMIn : InterpTy PORT (MINST xs) -> Void
portMIn (PP _) impossible
portMIn UU impossible
portMIn (MM _) impossible
portMIn (CM _) impossible
portMIn DD impossible
portMIn CC impossible
portMIn GG impossible

portUni : InterpTy PORT UNIT -> Void
portUni (PP _) impossible
portUni UU impossible
portUni (MM _) impossible
portUni (CM _) impossible
portUni DD impossible
portUni CC impossible
portUni GG impossible

portTyp : InterpTy PORT TYPE -> Void
portTyp (PP _) impossible
portTyp UU impossible
portTyp (MM _) impossible
portTyp (CM _) impossible
portTyp DD impossible
portTyp CC impossible
portTyp GG impossible

portGat : InterpTy PORT GATE -> Void
portGat (PP _) impossible
portGat UU impossible
portGat (MM _) impossible
portGat (CM _) impossible
portGat DD impossible
portGat CC impossible
portGat GG impossible

portGinst : InterpTy PORT GINST -> Void
portGinst (PP _) impossible
portGinst UU impossible
portGinst (MM _) impossible
portGinst (CM _) impossible
portGinst DD impossible
portGinst CC impossible
portGinst GG impossible

-- Unit

unitMod : InterpTy UNIT (MODULE xs) -> Void
unitMod (PP _) impossible
unitMod UU impossible
unitMod (MM _) impossible
unitMod (CM _) impossible
unitMod DD impossible
unitMod CC impossible
unitMod GG impossible

unitDat : InterpTy UNIT DATA -> Void
unitDat (PP _) impossible
unitDat UU impossible
unitDat (MM _) impossible
unitDat (CM _) impossible
unitDat DD impossible
unitDat CC impossible
unitDat GG impossible

unitCh : InterpTy UNIT CHAN -> Void
unitCh (PP _) impossible
unitCh UU impossible
unitCh (MM _) impossible
unitCh (CM _) impossible
unitCh DD impossible
unitCh CC impossible
unitCh GG impossible

unitPor : InterpTy UNIT (PORT x) -> Void
unitPor (PP _) impossible
unitPor UU impossible
unitPor (MM _) impossible
unitPor (CM _) impossible
unitPor DD impossible
unitPor CC impossible
unitPor GG impossible

unitMIn : InterpTy UNIT (MINST xs) -> Void
unitMIn (PP _) impossible
unitMIn UU impossible
unitMIn (MM _) impossible
unitMIn (CM _) impossible
unitMIn DD impossible
unitMIn CC impossible
unitMIn GG impossible

unitTyp : InterpTy UNIT TYPE -> Void
unitTyp (PP _) impossible
unitTyp UU impossible
unitTyp (MM _) impossible
unitTyp (CM _) impossible
unitTyp DD impossible
unitTyp CC impossible
unitTyp GG impossible

unitGat : InterpTy UNIT GATE -> Void
unitGat (PP _) impossible
unitGat UU impossible
unitGat (MM _) impossible
unitGat (CM _) impossible
unitGat DD impossible
unitGat CC impossible
unitGat GG impossible

unitGinst : InterpTy UNIT GINST -> Void
unitGinst (PP _) impossible
unitGinst UU impossible
unitGinst (MM _) impossible
unitGinst (CM _) impossible
unitGinst DD impossible
unitGinst CC impossible
unitGinst GG impossible

-- Module

moduleUni : InterpTy MODULE UNIT -> Void
moduleUni (PP _) impossible
moduleUni UU impossible
moduleUni (MM _) impossible
moduleUni (CM _) impossible
moduleUni DD impossible
moduleUni CC impossible
moduleUni GG impossible

moduleDat : InterpTy MODULE DATA -> Void
moduleDat (PP _) impossible
moduleDat UU impossible
moduleDat (MM _) impossible
moduleDat (CM _) impossible
moduleDat DD impossible
moduleDat CC impossible
moduleDat GG impossible

moduleCh : InterpTy MODULE CHAN -> Void
moduleCh (PP _) impossible
moduleCh UU impossible
moduleCh (MM _) impossible
moduleCh (CM _) impossible
moduleCh DD impossible
moduleCh CC impossible
moduleCh GG impossible

modulePor : InterpTy MODULE (PORT x) -> Void
modulePor (PP _) impossible
modulePor UU impossible
modulePor (MM _) impossible
modulePor (CM _) impossible
modulePor DD impossible
modulePor CC impossible
modulePor GG impossible

moduleMIn : InterpTy MODULE (MINST xs) -> Void
moduleMIn (PP _) impossible
moduleMIn UU impossible
moduleMIn (MM _) impossible
moduleMIn (CM _) impossible
moduleMIn DD impossible
moduleMIn CC impossible
moduleMIn GG impossible

moduleTyp : InterpTy MODULE TYPE -> Void
moduleTyp (PP _) impossible
moduleTyp UU impossible
moduleTyp (MM _) impossible
moduleTyp (CM _) impossible
moduleTyp DD impossible
moduleTyp CC impossible
moduleTyp GG impossible

moduleGat : InterpTy MODULE GATE -> Void
moduleGat (PP _) impossible
moduleGat UU impossible
moduleGat (MM _) impossible
moduleGat (CM _) impossible
moduleGat DD impossible
moduleGat CC impossible
moduleGat GG impossible

moduleGinst : InterpTy MODULE GINST -> Void
moduleGinst (PP _) impossible
moduleGinst UU impossible
moduleGinst (MM _) impossible
moduleGinst (CM _) impossible
moduleGinst DD impossible
moduleGinst CC impossible
moduleGinst GG impossible

-- Data

dataMod : InterpTy DATA (MODULE xs) -> Void
dataMod (PP _) impossible
dataMod UU impossible
dataMod (MM _) impossible
dataMod (CM _) impossible
dataMod DD impossible
dataMod CC impossible
dataMod GG impossible

dataUni : InterpTy DATA UNIT -> Void
dataUni (PP _) impossible
dataUni UU impossible
dataUni (MM _) impossible
dataUni (CM _) impossible
dataUni DD impossible
dataUni CC impossible
dataUni GG impossible

dataCh : InterpTy DATA CHAN -> Void
dataCh (PP _) impossible
dataCh UU impossible
dataCh (MM _) impossible
dataCh (CM _) impossible
dataCh DD impossible
dataCh CC impossible
dataCh GG impossible

dataPor : InterpTy DATA (PORT x) -> Void
dataPor (PP _) impossible
dataPor UU impossible
dataPor (MM _) impossible
dataPor (CM _) impossible
dataPor DD impossible
dataPor CC impossible
dataPor GG impossible

dataMIn : InterpTy DATA (MINST xs) -> Void
dataMIn (PP _) impossible
dataMIn UU impossible
dataMIn (MM _) impossible
dataMIn (CM _) impossible
dataMIn DD impossible
dataMIn CC impossible
dataMIn GG impossible

dataTyp : InterpTy DATA TYPE -> Void
dataTyp (PP _) impossible
dataTyp UU impossible
dataTyp (MM _) impossible
dataTyp (CM _) impossible
dataTyp DD impossible
dataTyp CC impossible
dataTyp GG impossible

dataGat : InterpTy DATA GATE -> Void
dataGat (PP _) impossible
dataGat UU impossible
dataGat (MM _) impossible
dataGat (CM _) impossible
dataGat DD impossible
dataGat CC impossible
dataGat GG impossible

dataGinst : InterpTy DATA GINST -> Void
dataGinst (PP _) impossible
dataGinst UU impossible
dataGinst (MM _) impossible
dataGinst (CM _) impossible
dataGinst DD impossible
dataGinst CC impossible
dataGinst GG impossible

-- Conns

connMod : InterpTy CONN (MODULE xs) -> Void
connMod (PP _) impossible
connMod UU impossible
connMod (MM _) impossible
connMod (CM _) impossible
connMod DD impossible
connMod CC impossible
connMod GG impossible

connUni : InterpTy CONN UNIT -> Void
connUni (PP _) impossible
connUni UU impossible
connUni (MM _) impossible
connUni (CM _) impossible
connUni DD impossible
connUni CC impossible
connUni GG impossible

connCh : InterpTy CONN CHAN -> Void
connCh (PP _) impossible
connCh UU impossible
connCh (MM _) impossible
connCh (CM _) impossible
connCh DD impossible
connCh CC impossible
connCh GG impossible

connPor : InterpTy CONN (PORT x) -> Void
connPor (PP _) impossible
connPor UU impossible
connPor (MM _) impossible
connPor (CM _) impossible
connPor DD impossible
connPor CC impossible
connPor GG impossible

connTyp : InterpTy CONN TYPE -> Void
connTyp (PP _) impossible
connTyp UU impossible
connTyp (MM _) impossible
connTyp (CM _) impossible
connTyp DD impossible
connTyp CC impossible
connTyp GG impossible

connDat : InterpTy CONN DATA -> Void
connDat (PP _) impossible
connDat UU impossible
connDat (MM _) impossible
connDat (CM _) impossible
connDat DD impossible
connDat CC impossible
connDat GG impossible

connGat : InterpTy CONN GATE -> Void
connGat (PP _) impossible
connGat UU impossible
connGat (MM _) impossible
connGat (CM _) impossible
connGat DD impossible
connGat CC impossible
connGat GG impossible

connGinst : InterpTy CONN GINST -> Void
connGinst (PP _) impossible
connGinst UU impossible
connGinst (MM _) impossible
connGinst (CM _) impossible
connGinst DD impossible
connGinst CC impossible
connGinst GG impossible

-- Channel

chanMod : InterpTy CHAN (MODULE xs) -> Void
chanMod (PP _) impossible
chanMod UU impossible
chanMod (MM _) impossible
chanMod (CM _) impossible
chanMod DD impossible
chanMod CC impossible
chanMod GG impossible

chanUni : InterpTy CHAN UNIT -> Void
chanUni (PP _) impossible
chanUni UU impossible
chanUni (MM _) impossible
chanUni (CM _) impossible
chanUni DD impossible
chanUni CC impossible
chanUni GG impossible

chanPor : InterpTy CHAN (PORT x) -> Void
chanPor (PP _) impossible
chanPor UU impossible
chanPor (MM _) impossible
chanPor (CM _) impossible
chanPor DD impossible
chanPor CC impossible
chanPor GG impossible

chanTyp : InterpTy CHAN TYPE -> Void
chanTyp (PP _) impossible
chanTyp UU impossible
chanTyp (MM _) impossible
chanTyp (CM _) impossible
chanTyp DD impossible
chanTyp CC impossible
chanTyp GG impossible

chanDat : InterpTy CHAN DATA -> Void
chanDat (PP _) impossible
chanDat UU impossible
chanDat (MM _) impossible
chanDat (CM _) impossible
chanDat DD impossible
chanDat CC impossible
chanDat GG impossible

chanMIn : InterpTy CHAN (MINST xs) -> Void
chanMIn (PP _) impossible
chanMIn UU impossible
chanMIn (MM _) impossible
chanMIn (CM _) impossible
chanMIn DD impossible
chanMIn CC impossible
chanMIn GG impossible

chanGat : InterpTy CHAN GATE -> Void
chanGat (PP _) impossible
chanGat UU impossible
chanGat (MM _) impossible
chanGat (CM _) impossible
chanGat DD impossible
chanGat CC impossible
chanGat GG impossible

chanGinst : InterpTy CHAN GINST -> Void
chanGinst (PP _) impossible
chanGinst UU impossible
chanGinst (MM _) impossible
chanGinst (CM _) impossible
chanGinst DD impossible
chanGinst CC impossible
chanGinst GG impossible

-- Channel

gateMod : InterpTy GATE (MODULE xs) -> Void
gateMod (PP _) impossible
gateMod UU impossible
gateMod (MM _) impossible
gateMod (CM _) impossible
gateMod DD impossible
gateMod CC impossible
gateMod GG impossible

gateUni : InterpTy GATE UNIT -> Void
gateUni (PP _) impossible
gateUni UU impossible
gateUni (MM _) impossible
gateUni (CM _) impossible
gateUni DD impossible
gateUni CC impossible
gateUni GG impossible

gatePor : InterpTy GATE (PORT x) -> Void
gatePor (PP _) impossible
gatePor UU impossible
gatePor (MM _) impossible
gatePor (CM _) impossible
gatePor DD impossible
gatePor CC impossible
gatePor GG impossible

gateTyp : InterpTy GATE TYPE -> Void
gateTyp (PP _) impossible
gateTyp UU impossible
gateTyp (MM _) impossible
gateTyp (CM _) impossible
gateTyp DD impossible
gateTyp CC impossible
gateTyp GG impossible

gateDat : InterpTy GATE DATA -> Void
gateDat (PP _) impossible
gateDat UU impossible
gateDat (MM _) impossible
gateDat (CM _) impossible
gateDat DD impossible
gateDat CC impossible
gateDat GG impossible

gateMIn : InterpTy GATE (MINST xs) -> Void
gateMIn (PP _) impossible
gateMIn UU impossible
gateMIn (MM _) impossible
gateMIn (CM _) impossible
gateMIn DD impossible
gateMIn CC impossible
gateMIn GG impossible

gateGat : InterpTy GATE GATE -> Void
gateGat (PP _) impossible
gateGat UU impossible
gateGat (MM _) impossible
gateGat (CM _) impossible
gateGat DD impossible
gateGat CC impossible
gateGat GG impossible

gateChan : InterpTy GATE CHAN -> Void
gateChan (PP _) impossible
gateChan UU impossible
gateChan (MM _) impossible
gateChan (CM _) impossible
gateChan DD impossible
gateChan CC impossible
gateChan GG impossible

export
interpTy : (ty : TyIR)
        -> (type : Ty)
        -> Dec (InterpTy ty type)
interpTy PORT (MODULE xs) = No portMod
interpTy PORT DATA = No portDat
interpTy PORT CHAN = No portCha
interpTy PORT (PORT x) = Yes (PP x)
interpTy PORT (MINST xs) = No portMIn
interpTy PORT UNIT = No portUni
interpTy PORT TYPE = No portTyp
interpTy PORT GATE = No portGat
interpTy PORT GINST = No portGinst

interpTy UNIT (MODULE xs) = No unitMod
interpTy UNIT DATA = No unitDat
interpTy UNIT CHAN = No unitCh
interpTy UNIT (PORT x) = No unitPor
interpTy UNIT (MINST xs) = No unitMIn
interpTy UNIT UNIT = Yes UU
interpTy UNIT TYPE = No unitTyp
interpTy UNIT GATE = No unitGat
interpTy UNIT GINST = No unitGinst

interpTy MODULE (MODULE xs) = Yes (MM xs)
interpTy MODULE DATA = No moduleDat
interpTy MODULE CHAN = No moduleCh
interpTy MODULE (PORT x) = No modulePor
interpTy MODULE (MINST xs) = No moduleMIn
interpTy MODULE UNIT = No moduleUni
interpTy MODULE TYPE = No moduleTyp
interpTy MODULE GATE = No moduleGat
interpTy MODULE GINST = No moduleGinst

interpTy CONN (MODULE xs) = No connMod
interpTy CONN DATA = No connDat
interpTy CONN CHAN = No connCh
interpTy CONN (PORT x) = No connPor
interpTy CONN (MINST xs) = Yes (CM xs)
interpTy CONN UNIT = No connUni
interpTy CONN TYPE = No connTyp
interpTy CONN GATE = No connGat
interpTy CONN GINST = No connGinst

interpTy DATA (MODULE xs) = No dataMod
interpTy DATA DATA = Yes DD
interpTy DATA CHAN = No dataCh
interpTy DATA (PORT x) = No dataPor
interpTy DATA (MINST xs) = No dataMIn
interpTy DATA UNIT = No dataUni
interpTy DATA TYPE = No dataTyp
interpTy DATA GATE = No dataGat
interpTy DATA GINST = No dataGinst

interpTy CHAN (MODULE xs) = No chanMod
interpTy CHAN DATA = No chanDat
interpTy CHAN CHAN = Yes CC
interpTy CHAN (PORT x) = No chanPor
interpTy CHAN (MINST xs) = No chanMIn
interpTy CHAN UNIT = No chanUni
interpTy CHAN TYPE = No chanTyp
interpTy CHAN GATE = No chanGat
interpTy CHAN GINST = No chanGinst

interpTy GATE (MODULE xs) = No gateMod
interpTy GATE DATA        = No gateDat
interpTy GATE CHAN        = No gateChan
interpTy GATE (PORT x)    = No gatePor
interpTy GATE (MINST xs)  = No gateMIn
interpTy GATE UNIT        = No gateUni
interpTy GATE TYPE        = No gateTyp
interpTy GATE GATE        = No gateGat
interpTy GATE GINST       = Yes GG

namespace TyIR
  public export
  data IsGlobal : TyIR -> Type where
    IsDeclM : IsGlobal MODULE
    IsDeclD : IsGlobal DATA

  public export
  data IsLocal : TyIR -> Type where
    IsInstM : IsLocal CONN
    IsInstC : IsLocal CHAN
    IsInstG : IsLocal GATE

  public export
  data Bindable : TyIR -> Type where
    IsDecl : IsGlobal type -> Bindable type
    IsLet  : IsLocal type  -> Bindable type
    Unbindable : TyIR.Bindable type

  export
  isBindable : (type : TyIR) -> Bindable type
  isBindable PORT = Unbindable
  isBindable UNIT = Unbindable
  isBindable MODULE = IsDecl IsDeclM
  isBindable CONN = IsLet IsInstM
  isBindable DATA = IsDecl IsDeclD
  isBindable CHAN = IsLet IsInstC
  isBindable GATE = IsLet IsInstG

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

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Test.Basics

import Control.Monad.Identity
import Data.List
import Data.MSF
import Data.SOP
import Hedgehog

%default total

--------------------------------------------------------------------------------
--          Generators
--------------------------------------------------------------------------------

smallInt : Gen Integer
smallInt = integer (linear 0 1000)

smallInts : Gen (List Integer)
smallInts = list (linear 0 30) smallInt

--------------------------------------------------------------------------------
--          Properties
--------------------------------------------------------------------------------

prop_const : Property
prop_const = property $ do
  [n,ns] <- forAll $ np [smallInt, smallInts]
  embedI ns (const n) === map (const n) ns

prop_arrId : Property
prop_arrId = property $ do
  ns <- forAll smallInts
  embedI ns (arr id) === ns

prop_arr : Property
prop_arr = property $ do
  [n,ns] <- forAll $ np [smallInt, smallInts]
  embedI ns (arr (*n)) === map (*n) ns

prop_elementwise : Property
prop_elementwise = property $ do
  [n1,n2,ns] <- forAll $ np [smallInt,smallInt,smallInts]
  embedI ns (map (*n1) (arr (+n2))) ===
    map (\n => n1 * (n + n2)) ns

prop_elementwise2 : Property
prop_elementwise2 = property $ do
  [n1,n2,ns] <- forAll $ np [smallInt,smallInt,smallInts]
  embedI ns [| arr (+n1) * arr (+n2) |] ===
  zipWith (*) (map (+n1) ns) (map (+n2) ns)

prop_once : Property
prop_once = property $ do
  [n1,n2,ns] <- forAll $ np [smallInt,smallInt,smallInts]
  embedI (n2 :: ns) (once n1) === Ev n1 :: (ns $> NoEv)

prop_onceOrId : Property
prop_onceOrId = property $ do
  [n1,n2,ns] <- forAll $ np [smallInt,smallInt,smallInts]
  embedI (map Ev $ n2 :: ns) (once n1 <|> id) === Ev n1 :: map Ev ns

prop_idOrOnce : Property
prop_idOrOnce = property $ do
  [n1,n2,ns] <- forAll $ np [smallInt,smallInt,smallInts]
  embedI (map Ev $ n2 :: ns) (id <|> once n1) === Ev n2 :: map Ev ns
  embedI (NoEv :: map Ev ns) (id <|> once n1) === Ev n1 :: map Ev ns

--------------------------------------------------------------------------------
--          props
--------------------------------------------------------------------------------

export
props : Group
props = MkGroup "basic properties"
          [ ("prop_const", prop_const)
          , ("prop_arrId", prop_arrId)
          , ("prop_arr", prop_arr)
          , ("prop_elementwise", prop_elementwise)
          , ("prop_elementwise2", prop_elementwise2)
          , ("prop_once", prop_once)
          , ("idOrOnce", prop_idOrOnce)
          ]


text:
--module Data.Iso
module Iso

import Data.DPair
import Data.Nat
import Data.Fin
import Data.Fin.Extra

import Syntax.WithProof

%default total

-- TODO to think of weaker form of isomorphism:
--  0 to_from_to_is_from : (x : a) -> to (from (to x)) = to x
--  0 from_to_from_is_to : (y : b) -> from (to (from y)) = from y

infix 0 =~=

public export
interface (=~=) a b where
  constructor MkIso

  to   : a -> b
  from : b -> a

  0 from_to_id : (x : a) -> from (to x) = x
  0 to_from_id : (y : b) -> to (from y) = y

public export
(=~=) (Fin n) (Subset Nat (`LT` n)) where
  to {n=S k} FZ = Element Z (LTESucc LTEZero)
  to (FS x)     = bimap S LTESucc $ to x

  from = uncurry natToFinLTE

  from_to_id FZ = Refl
  from_to_id {n=S k} (FS x) with (from_to_id {b=Subset Nat (`LT` k)} x)
    from_to_id (FS x) | fti with (to {b=Subset Nat (`LT` k)} x)
      from_to_id (FS x) | fti | Element fst snd = rewrite fti in Refl

  to_from_id (Element Z (LTESucc LTEZero)) = Refl
  to_from_id {n=S n} (Element (S k) (LTESucc x)) = rewrite to_from_id {a=Fin n} {b=Subset Nat (`LT` n)} (Element k x) in Refl
  to_from_id (Element (S k) LTEZero) impossible