text:
> module Vect.Properties

> import Data.Vect
> import Data.Vect.Quantifiers
> import Data.Fin

> import Vect.Operations
> import Sigma.Sigma
> import Sigma.Operations
> import Pairs.Operations
> import Exists.Operations
> import Decidable.Predicates
> import Rel.TotalPreorder
> import Rel.TotalPreorderOperations
> import Nat.LTProperties
> import Fin.Properties
> import Fun.Operations

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

> {-
> implementation Uninhabited (Elem {a} x Nil) where
>   uninhabited Here impossible
>   uninhabited (There p) impossible
> -}

Injectivity (of |flip index|):

> ||| Injectivity (one direction)
> Injective1 : Vect n t -> Type
> Injective1 {n} xs = (i : Fin n) -> (j : Fin n) -> index i xs = index j xs -> i = j

> ||| Injectivity (the other direction)
> Injective2 : Vect n t -> Type
> Injective2 {n} xs = (i : Fin n) -> (j : Fin n) -> Not (i = j) -> Not (index i xs = index j xs)

> ||| Injective1 implies Injective2
> injectiveLemma : (xs : Vect n t) -> Injective1 xs -> Injective2 xs
> injectiveLemma xs i1xs i j contra = contra . (i1xs i j)
> %freeze injectiveLemma

> ||| Tail preserves injectivity (one direction)
> injectiveTailLemma1 : (xs : Vect (S n) t) -> Injective1 xs -> Injective1 (tail xs)
> injectiveTailLemma1  Nil      p _ _ _ impossible
> injectiveTailLemma1 (x :: xs) p i j q = FSInjective i j (p (FS i) (FS j) q') where
>   q' : index (FS i) (x :: xs) = index (FS j) (x :: xs)
>   q' = q
> %freeze injectiveTailLemma1

> ||| Tail preserves injectivity (the other direction)
> injectiveTailLemma2 : (xs : Vect (S n) t) -> Injective2 xs -> Injective2 (tail xs)
> injectiveTailLemma2  Nil      p _ _ _ impossible
> injectiveTailLemma2 (x :: xs) p i j q = p (FS i) (FS j) (fsInjective2 i j q)
> %freeze injectiveTailLemma2

Indexing and lookup

> |||
> indexLemma : (k : Fin n) -> (xs : Vect n t) -> Elem (index k xs) xs
> indexLemma {n = Z}       k   Nil      = absurd k
> indexLemma {n = S m}  FZ    (x :: xs) = Here
> indexLemma {n = S m} (FS k) (x :: xs) = There (indexLemma k xs)
> %freeze indexLemma

> |||
> indexLookupLemma : (x : alpha) ->
>                    (xs : Vect n alpha) ->
>                    (prf : Elem x xs) ->
>                    index (lookup x xs prf) xs = x
> indexLookupLemma x  Nil        prf        = absurd prf
> indexLookupLemma x (x :: xs)   Here       = Refl
> indexLookupLemma x (x' :: xs) (There prf) =
>   let ih = indexLookupLemma x xs prf in rewrite ih in Refl
> {-
> indexLookupLemma x (x' :: xs) (There prf) = trans s1 (trans s2 s3) where
>   s1 : index (lookup x (x' :: xs) (There prf)) (x' :: xs)
>        =
>        index (FS (lookup x xs prf)) (x' :: xs)
>   s1 = Refl
>   s2 : index (FS (lookup x xs prf)) (x' :: xs)
>        =
>        index (lookup x xs prf) xs
>   s2 = Refl
>   s3 : index (lookup x xs prf) xs
>        =
>        x
>   s3 = indexLookupLemma x xs prf
> -}
> %freeze indexLookupLemma

> |||
> lookupIndexLemma : (k : Fin n) ->
>                    (xs : Vect n t) ->
>                    (p : Injective2 xs) ->
>                    (q : Elem (index k xs) xs) ->
>                    lookup (index k xs) xs q = k
> lookupIndexLemma  FZ     Nil      _  _        impossible
> lookupIndexLemma  FZ    (x :: xs) p  Here     = Refl
> lookupIndexLemma  FZ    (x :: xs) p (There q) = s5 where
>   s1 : Not (FZ = lookup x (x :: xs) (There q))
>   s1 Refl impossible
>   s2 : index FZ (x :: xs) = x
>   s2 = Refl
>   s3 : index (lookup x (x :: xs) (There q)) (x :: xs) = x
>   s3 = indexLookupLemma x (x :: xs) (There q)
>   s4 : index FZ (x :: xs) = index (lookup x (x :: xs) (There q)) (x :: xs)
>   s4 = trans s2 (sym s3)
>   s5 : lookup (index FZ (x :: xs)) (x :: xs) (There q) = FZ
>   s5 = void ((p FZ (lookup x (x :: xs) (There q)) s1) s4)
> lookupIndexLemma (FS k)  Nil      _  _        impossible
> lookupIndexLemma (FS k) (_ :: xs) p  Here     = s5 where
>   s1 : Not (FZ = FS k)
>   s1 Refl impossible
>   s2 : index FZ ((index k xs) :: xs) = index (FS k) ((index k xs) :: xs)
>   s2 = Refl
>   s5 : lookup (index (FS k) ((index k xs) :: xs)) ((index k xs) :: xs) Here = (FS k)
>   s5 = void ((p FZ (FS k) s1) s2)
> lookupIndexLemma (FS k) (x :: xs) p (There q) =
>   let p' = injectiveTailLemma2 (x :: xs) p in
>   let ih = lookupIndexLemma k xs p' q in
>   rewrite ih in Refl
> %freeze lookupIndexLemma

> |||
> -- indexToVectLemma : {A : Type} -> (f : Fin n -> A) -> (k : Fin n) -> f k = index k (toVect f)

Membership, quantifiers:

> ||| Membership => non emptyness
> elemLemma : {A : Type} -> {n : Nat} ->
>             (a : A) -> (as : Vect n A) ->
>             Elem a as -> LT Z n
> elemLemma {n = Z}   a Nil p = absurd p
> elemLemma {n = S m} a as  p = ltZS m
> %freeze elemLemma

> |||
> AnySigmaLemma : {A : Type} -> {P : A -> Type} -> {as : Vect n A} ->
>                 Any P as -> Sigma A P
> AnySigmaLemma (Here px) = MkSigma _ px
> AnySigmaLemma (There prf) = AnySigmaLemma prf

> |||
> AnyExistsLemma : {A : Type} -> {P : A -> Type} -> {as : Vect n A} ->
>                  Any P as -> Exists P
> AnyExistsLemma (Here px) = Evidence _ px
> AnyExistsLemma (There prf) = AnyExistsLemma prf

> ElemAnyLemma : {A : Type} -> {P : A -> Type} -> P a -> Elem a as -> Any P as
> ElemAnyLemma p Here = Here p
> ElemAnyLemma p (There e) = There (ElemAnyLemma p e)
> %freeze ElemAnyLemma

> |||
> decAny : {A : Type} -> {P : A -> Type} -> Dec1 P -> Dec1 (Any P)
> decAny d1P = any d1P
> %freeze decAny

> elemNotHeadTail : Elem a (a' :: as) -> Not (a = a') -> Elem a as
> elemNotHeadTail  Here     q = void (q Refl)
> elemNotHeadTail (There p) _ = p

> decElemTailDecElemHeadTail : {A : Type} -> {n : Nat} -> (DecEq A) =>
>                              (a : A) -> (a' : A) -> (as : Vect n A)->
>                              Dec (Elem a as) -> Dec (Elem a (a' :: as))
> decElemTailDecElemHeadTail a a' as (Yes p) = Yes (There p)
> decElemTailDecElemHeadTail a a' as (No  p) with (decEq a a')
>   | Yes q = Yes (replace {P = \ X => Elem a (X :: as)} q Here)
>   |  No q =  No (\ prf => p (elemNotHeadTail prf q))

> |||
> decElem : {A : Type} -> {n : Nat} -> (DecEq A) =>
>           (a : A) -> (as : Vect n A)-> Dec (Elem a as)
> decElem a Nil = No absurd
> decElem a (a' :: as) with (decEq a a')
>   | Yes p  = Yes (replace {P = \ X => Elem a (X :: as)} p Here)
>   | No  p  = decElemTailDecElemHeadTail a a' as (decElem a as)

Container monad properties

> |||
> mapLemma : {A, B : Type} -> (as : Vect n A) -> (f : A -> B) ->
>            (a : A) -> Elem a as -> Elem (f a) (map f as)
> mapLemma  Nil      f a aeas = absurd aeas
> mapLemma (a :: as) f a   Here       = Here
> mapLemma (a :: as) f a' (There prf) = There (mapLemma as f a' prf)
> %freeze mapLemma

> |||
> mapIdfLemma : {A, B : Type} -> (as : Vect n A) -> (f : A -> B) ->
>               (ab : (A,B)) -> Elem ab (map (pair (Prelude.Basics.id,f)) as) ->
>               f (fst ab) = snd ab
> mapIdfLemma  Nil      f  ab     p        = absurd p
> mapIdfLemma (a :: as) f (a, _)  Here     = Refl
> mapIdfLemma (a :: as) f  ab    (There p) = mapIdfLemma as f ab p
> %freeze mapIdfLemma

Filtering

> ||| |filter| preserves membership
> filterLemma : {A : Type} ->
>               {P : A -> Type} ->
>               (d1P : Dec1 P) ->
>               (a : A) ->
>               (as : Vect n A) ->
>               Elem a as ->
>               (p : P a) ->
>               Elem a (getProof (filter d1P as))
> filterLemma d1P a   Nil       prf  p = absurd prf
> filterLemma d1P a1 (a1 :: as) Here p with (filter d1P as)
>   | (MkSigma n as') with (d1P a1)
>     | (Yes _) = Here {x = a1} {xs = as'}
>     | (No  contra) = void (contra p)
> filterLemma {A} {P} d1P a1 (a2 :: as) (There prf) p with (filter d1P as) proof itsEqual
>   | (MkSigma n as') with (d1P a2)
>     | (Yes _) = -- There {x = a1} {xs = as'} {y = a2} (filterLemma d1P a1 as prf p)
>                 There {x = a1} {xs = as'} {y = a2} $
>                   replace {P = \rec => Elem a1 (getProof rec)} (sym itsEqual) $
>                     filterLemma {A} {P} d1P a1 as prf p
>     | (No  _) = -- filterLemma {A} {P} d1P a1 as prf p
>                 replace {P = \rec => Elem a1 (getProof rec)} (sym itsEqual) $
>                   filterLemma {P = P} d1P a1 as prf p
> %freeze filterLemma

> ||| |filterTagSigma| preserves membership
> filterTagSigmaLemma : {A : Type} ->
>                       {P : A -> Type} ->
>                       {n : Nat} ->
>                       (d1P : Dec1 P) ->
>                       (a : A) ->
>                       (as : Vect n A) ->
>                       Elem a as ->
>                       (p : P a) ->
>                       Elem a (map Sigma.Operations.outl (Sigma.Operations.outr (filterTagSigma d1P as)))
> filterTagSigmaLemma d1P a   Nil       prf  p = absurd prf
> filterTagSigmaLemma d1P a1 (a1 :: as) Here p with (filterTagSigma d1P as)
>   | (MkSigma n aps') with (d1P a1)
>     | (Yes _) = Here {x = a1} {xs = map Sigma.Operations.outl aps'}
>     | (No  contra) = void (contra p)
> filterTagSigmaLemma d1P a1 (a2 :: as) (There prf) p with (filterTagSigma d1P as) proof itsEqual
>   | (MkSigma n aps') with (d1P a2)
>     | (Yes _) = -- There {x = a1} {xs = map Sigma.Operations.outl aps'} {y = a2} (filterTagSigmaLemma d1P a1 as prf p)
>                 There {x = a1} {xs = map Sigma.Operations.outl aps'} {y = a2} $
>                   replace {P = \rec => Elem a1 (map Sigma.Operations.outl (getProof rec))} (sym itsEqual) $
>                     filterTagSigmaLemma d1P a1 as prf p
>     | (No  _) = -- filterTagSigmaLemma d1P a1 as prf p
>                 replace {P = \rec => Elem a1 (map Sigma.Operations.outl (getProof rec))} (sym itsEqual) $
>                   filterTagSigmaLemma d1P a1 as prf p
> %freeze filterTagSigmaLemma

> ||| |filterTagExists| preserves membership
> filterTagExistsLemma : {A : Type} ->
>                        {P : A -> Type} ->
>                        {n : Nat} ->
>                        (d1P : Dec1 P) ->
>                        (a : A) ->
>                        (as : Vect n A) ->
>                        Elem a as ->
>                        (p : P a) ->
>                        Elem a (map Exists.getWitness (Sigma.getProof (filterTagExists d1P as)))
> filterTagExistsLemma d1P a   Nil       prf  p = absurd prf
> filterTagExistsLemma d1P a1 (a1 :: as) Here p with (filterTagExists d1P as)
>   | (MkSigma n aps') with (d1P a1)
>     | (Yes _) = Here {x = a1} {xs = map getWitness aps'}
>     | (No  contra) = void (contra p)
> filterTagExistsLemma d1P a1 (a2 :: as) (There prf) p with (filterTagExists d1P as) proof itsEqual
>   | (MkSigma n aps') with (d1P a2)
>     | (Yes _) = -- There {x = a1} {xs = map getWitness aps'} {y = a2} (filterTagExistsLemma d1P a1 as prf p)
>                 There {x = a1} {xs = map getWitness aps'} {y = a2} $
>                   replace {P = \rec => Elem a1 (map Exists.getWitness (getProof rec))} (sym itsEqual) $
>                     filterTagExistsLemma d1P a1 as prf p
>     | (No  _) = -- filterTagExistsLemma d1P a1 as prf p
>                 replace {P = \rec => Elem a1 (map Exists.getWitness (getProof rec))} (sym itsEqual) $
>                   filterTagExistsLemma d1P a1 as prf p
> %freeze filterTagExistsLemma

> ||| |filterTagSubset| preserves membership
> filterTagSubsetLemma : {A : Type} ->
>                        {P : A -> Type} ->
>                        {n : Nat} ->
>                        (d1P : Dec1 P) ->
>                        (a : A) ->
>                        (as : Vect n A) ->
>                        Elem a as ->
>                        (p : P a) ->
>                        Elem a (map Subset.getWitness (Sigma.getProof (filterTagSubset d1P as)))
> filterTagSubsetLemma d1P a   Nil       prf  p = absurd prf
> filterTagSubsetLemma d1P a1 (a1 :: as) Here p with (filterTagSubset d1P as)
>   | (MkSigma n aps') with (d1P a1)
>     | (Yes _) = Here {x = a1} {xs = map getWitness aps'}
>     | (No  contra) = void (contra p)
> filterTagSubsetLemma d1P a1 (a2 :: as) (There prf) p with (filterTagSubset d1P as) proof itsEqual
>   | (MkSigma n aps') with (d1P a2)
>     | (Yes _) = -- There {x = a1} {xs = map getWitness aps'} {y = a2} (filterTagLemma d1P a1 as prf p)
>                 There {x = a1} {xs = map getWitness aps'} {y = a2} $
>                   replace {P = \rec => Elem a1 (map Subset.getWitness (getProof rec))} (sym itsEqual) $
>                     filterTagSubsetLemma d1P a1 as prf p
>     | (No  _) = -- filterTagLemma d1P a1 as prf p
>                 replace {P = \rec => Elem a1 (map Subset.getWitness (getProof rec))} (sym itsEqual) $
>                   filterTagSubsetLemma d1P a1 as prf p
> %freeze filterTagSubsetLemma

> {- Just commented out for testing
> ||| |filter| preserves injectivity
> injectiveFilterLemma : {A : Type} ->
>                        {P : A -> Type} ->
>                        {n : Nat} ->
>                        (dP : Dec1 P) ->
>                        (as : Vect n A) ->
>                        Injective1 as ->
>                        Injective1 (getProof (filter dP as))
> -}
> {-
>     = s0 where
>   n'  : Nat
>   n'  = getWitness (filter dP (a :: as))
>   as' : Vect n' A
>   as' = getProof (filter dP (a :: as))
>   s0 : Injective1 (getProof (filter dP (a :: as)))
>   s0 i j q with (filter dP as)
>     | (n' ** as') with (dP a)
>       | (Yes _) = ?liko
>       | (No  _) = s5 where
>         s5 : i = j
>         s5 = ?lala -- injectiveFilterLemma dP as (injectiveTailLemma1 (a :: as) iaas) i j q
> -}

> {-
> ||| |filterTagSigma| preserves injectivity
> injectiveFilterTagSigmaLemma : {A : Type} ->
>                                {P : A -> Type} ->
>                                (dP : Dec1 P) ->
>                                (as : Vect n A) ->
>                                Injective1 as ->
>                                Injective1 (getProof (filterTagSigma d1P as))
> injectiveFilterTagSigmaLemma {n = Z}   dP Nil i1as i j p = absurd i

> ||| |filterTagSubset| preserves injectivity
> injectiveFilterTagSubsetLemma : {A : Type} ->
>                                 {P : A -> Type} ->
>                                 (dP : Dec1 P) ->
>                                 (as : Vect n A) ->
>                                 Injective1 as ->
>                                 Injective1 (getProof (filterTagSubset d1P as))
> injectiveFilterTagSubsetLemma {n = Z}   dP Nil i1as i j p = absurd i
> -}

Max and argmax

> |||
> maxLemma : {A : Type} -> {R : A -> A -> Type} ->
>            (tp : TotalPreorder R) ->
>            (a : A) -> (as : Vect n A) -> (p : LT Z n) -> a `Elem` as ->
>            R a (max tp as p)
> maxLemma {R} {n = Z}       tp a        Nil          p  _          = absurd p
> maxLemma {R} {n = S Z}     tp a (a  :: Nil)         _  Here       = reflexive tp a
> maxLemma {R} {n = S Z}     tp a (a' :: Nil)         _ (There prf) = absurd prf
> maxLemma {R} {n = S (S m)} tp a (a :: (a'' :: as))  _  Here with (argmaxMax tp (a'' :: as) (ltZS m))
>   | (k, max) with (totalPre tp a max)
>     | (Left  p) = p
>     | (Right _) = reflexive tp a
> maxLemma {R} {n = S (S m)} tp a (a' :: (a'' :: as)) _ (There prf) with (argmaxMax tp (a'' :: as) (ltZS m)) proof itsEqual
>   | (k, max) with (totalPre tp a' max)
>     | (Left  _) = replace {P = \rec => R a (snd rec)}
>                           (sym itsEqual)
>                           (maxLemma {n = S m} tp a (a'' :: as) (ltZS m) prf)
>     | (Right p) = s3 where
>       s1 : R a (snd (Vect.Operations.argmaxMax tp (a'' :: as) (ltZS m)))
>       s1 = maxLemma {n = S m} tp a (a'' :: as) (ltZS m) prf
>       s2 : R (snd (Vect.Operations.argmaxMax tp (a'' :: as) (ltZS m))) a'
>       s2 = replace {P = \rec => R (snd rec) a'} itsEqual p
>       s3 : R a a'
>       s3 = transitive tp a (snd (Vect.Operations.argmaxMax tp (a'' :: as) (ltZS m))) a' s1 s2
> %freeze maxLemma

> |||
> argmaxLemma : {A : Type} -> {R : A -> A -> Type} ->
>               (tp : TotalPreorder R) ->
>               (as : Vect n A) -> (p : LT Z n) ->
>               index (argmax tp as p) as = max tp as p
> argmaxLemma {n = Z}       tp  Nil              p = absurd p
> argmaxLemma {n = S Z}     tp (a :: Nil)        p = Refl
> argmaxLemma {n = S (S m)} tp (a' :: (a'' :: as)) p with (argmaxMax tp (a'' :: as) (ltZS m)) proof itsEqual
>   | (k, max') with (totalPre tp a' max')
>     | (Left   _) = assert_total (replace {P = \rec => Data.Vect.index (fst rec) (a'' :: as) = snd rec}
>                                          (sym itsEqual)
>                                          (argmaxLemma tp (a'' :: as) (ltZS m)))
>     | (Right  _) = Refl
> %freeze argmaxLemma

> |||
> maxElemLemma : {A : Type} -> {R : A -> A -> Type} ->
>                (tp : TotalPreorder R) ->
>                (as : Vect n A) -> (p : LT Z n) ->
>                Elem (max tp as p) as
> maxElemLemma {n = Z}       tp  Nil                p = absurd p
> maxElemLemma {n = S Z}     tp (a :: Nil)          p = Here
> maxElemLemma {n = S (S m)} tp (a' :: (a'' :: as)) p with (argmaxMax tp (a'' :: as) (ltZS m)) proof itsEqual
>   | (k, max) with (totalPre tp a' max)
>     | (Left   _) = assert_total (replace {P = \ ZUZU => Elem ZUZU (a' :: (a'' :: as))}
>                                          (cong {f = Prelude.Basics.snd} (sym itsEqual))
>                                          (There {y = a'} (maxElemLemma tp (a'' :: as) (ltZS m))))
>     | (Right  _) = Here
> %freeze maxElemLemma

> {-

> |||
> maxLemma : {A : Type} ->
>            (tp : TotalPreorder A) ->
>            (a : A) -> (as : Vect n A) -> (p : LT Z n) -> a `Elem` as ->
>            R tp a (max tp as p)
> maxLemma {n = Z}       tp a        Nil          p  _          = absurd p
> maxLemma {n = S Z}     tp a (a  :: Nil)         _  Here       = reflexive tp a
> maxLemma {n = S Z}     tp a (a' :: Nil)         _ (There prf) = absurd prf
> maxLemma {n = S (S m)} tp a (a :: (a'' :: as))  _  Here with (argmaxMax tp (a'' :: as) (ltZS m))
>   | (k, max) with (totalPre tp a max)
>     | (Left  p) = p
>     | (Right _) = reflexive tp a
> maxLemma {n = S (S m)} tp a (a' :: (a'' :: as)) _ (There prf) with (argmaxMax tp (a'' :: as) (ltZS m)) proof itsEqual
>   | (k, max) with (totalPre tp a' max)
>     | (Left  _) = replace {P = \rec => R tp a (snd rec)}
>                           (sym itsEqual)
>                           (maxLemma {n = S m} tp a (a'' :: as) (ltZS m) prf)
>     | (Right p) = s3 where
>       s1 : R tp a (snd (Vect.Operations.argmaxMax tp (a'' :: as) (ltZS m)))
>       s1 = maxLemma {n = S m} tp a (a'' :: as) (ltZS m) prf
>       s2 : R tp (snd (Vect.Operations.argmaxMax tp (a'' :: as) (ltZS m))) a'
>       s2 = replace {P = \rec => R tp (snd rec) a'} itsEqual p
>       s3 : R tp a a'
>       s3 = transitive tp a (snd (Vect.Operations.argmaxMax tp (a'' :: as) (ltZS m))) a' s1 s2
> %freeze maxLemma

> |||
> argmaxLemma : {A : Type} ->
>               (tp : TotalPreorder A) ->
>               (as : Vect n A) -> (p : LT Z n) ->
>               index (argmax tp as p) as = max tp as p
> argmaxLemma {n = Z}       tp  Nil              p = absurd p
> argmaxLemma {n = S Z}     tp (a :: Nil)        p = Refl
> argmaxLemma {n = S (S m)} tp (a' :: (a'' :: as)) p with (argmaxMax tp (a'' :: as) (ltZS m)) proof itsEqual
>   | (k, max') with (totalPre tp a' max')
>     | (Left   _) = assert_total (replace {P = \rec => Data.Vect.index (fst rec) (a'' :: as) = snd rec}
>                                          (sym itsEqual)
>                                          (argmaxLemma tp (a'' :: as) (ltZS m)))
>     | (Right  _) = Refl
> %freeze argmaxLemma

> |||
> maxElemLemma : {A : Type} ->
>                (tp : TotalPreorder A) ->
>                (as : Vect n A) -> (p : LT Z n) ->
>                Elem (max tp as p) as
> maxElemLemma {n = Z}       tp  Nil                p = absurd p
> maxElemLemma {n = S Z}     tp (a :: Nil)          p = Here
> maxElemLemma {n = S (S m)} tp (a' :: (a'' :: as)) p with (argmaxMax tp (a'' :: as) (ltZS m)) proof itsEqual
>   | (k, max) with (totalPre tp a' max)
>     | (Left   _) = assert_total (replace {P = \ ZUZU => Elem ZUZU (a' :: (a'' :: as))}
>                                          (cong {f = Prelude.Basics.snd} (sym itsEqual))
>                                          (There {y = a'} (maxElemLemma tp (a'' :: as) (ltZS m))))
> {-
>     | (Left   _) = s4 where
>       s1 : Elem (snd (argmaxMax tp (a'' :: as) (ltZS m))) (a' :: (a'' :: as))
>       s1 = There {y = a'} (maxElemLemma tp (a'' :: as) (ltZS m))
>       s2 : argmaxMax tp (a'' :: as) (ltZS m) = (k, max)
>       s2 = sym itsEqual
>       s3 : snd (argmaxMax tp (a'' :: as) (ltZS m)) = max
>       s3 = cong {f = Prelude.Basics.snd} s2
>       s4 : Elem max (a' :: (a'' :: as))
>       s4 = replace {P = \ ZUZU => Elem ZUZU (a' :: (a'' :: as))} s3 s1
> -}
>     | (Right  _) = Here
> %freeze maxElemLemma

> -}

> {-

> |||
> maxLemma : {A : Type} -> {TO : A -> A -> Type} -> Preordered A TO =>
>            (a : A) -> (as : Vect (S n) A) -> a `Elem` as ->
>            TO a (max as)
> maxLemma {TO} {n = Z}   a (a :: Nil)          Here       = reflexive a
> maxLemma {TO} {n = Z}   a (a' :: Nil)        (There prf) = absurd prf
> maxLemma {TO} {n = S m} a (a :: (a'' :: as))  Here with (preorder a (max (a'' :: as)))
>   | (Left  p) = p
>   | (Right _) = reflexive a
> maxLemma {TO} {n = S m} a (a' :: (a'' :: as)) (There prf) with (preorder a' (max (a'' :: as)))
>   | (Left  _) = maxLemma a (a'' :: as) prf
>   | (Right p) = s3 where
>     s1 : TO a (max (a'' :: as))
>     s1 = maxLemma a (a'' :: as) prf
>     s2 : TO (max (a'' :: as)) a'
>     s2 = p
>     s3 : TO a a'
>     s3 = transitive a (max (a'' :: as)) a' s1 s2

> |||
> argmaxLemma : {A : Type} -> {TO : A -> A -> Type} -> Preordered A TO =>
>               (as : Vect (S n) A) ->
>               index (argmax as) as = max as
> argmaxLemma {TO} {n = Z}   (a :: Nil) = Refl
> argmaxLemma {TO} {n = S m} (a :: (a' :: as)) with (preorder a (max (a' :: as)))
>   | (Left   _) = argmaxLemma (a' :: as)
>   | (Right  _) = Refl

> -}

> {-

> |||
> maxLemma : {A, F : Type} -> {TO : F -> F -> Type} -> Ordered F TO =>
>            (af : (A,F)) -> (afs : Vect (S n) (A,F)) -> af `Elem` afs ->
>            TO (snd af) (max afs)
> maxLemma {A} {F} {TO} {n = Z}   af (af :: Nil)   Here       = reflexive (snd af)
> maxLemma {A} {F} {TO} {n = Z}   af (af' :: Nil) (There prf) = absurd prf
> maxLemma {A} {F} {TO} {n = S m} af (af :: (af'' :: afs)) Here with (order (snd af) (snd (argmaxMax (af'' :: afs))))
>   | (Left  p) = p
>   | (Right _) = reflexive (snd af)
> maxLemma {A} {F} {TO} {n = S m} af (af' :: (af'' :: afs)) (There prf) with (order (snd af') (snd (argmaxMax (af'' :: afs))))
>   | (Left  _) = maxLemma {A} {F} {TO} {n = m} af (af'' :: afs) prf
>   | (Right p) = s3 where
>     s1 : TO (snd af) (max (af'' :: afs))
>     s1 = maxLemma {A} {F} {TO} {n = m} af (af'' :: afs) prf
>     s2 : TO (max (af'' :: afs)) (snd af')
>     s2 = p
>     s3 : TO (snd af) (snd af')
>     s3 = transitive (snd af) (VectOperations.max (af'' :: afs)) (snd af') s1 s2

> -}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Test.Spec

import Refined

import Props.Util
import Props.Char
import Props.String
import Props.Nat

%access public export

zeroIsDigit : Refined Char Digit
zeroIsDigit = '0'

upperAIsLetter : Refined Char Letter
upperAIsLetter = 'A'

lowerAIsAlpha : Refined Char AlphaNumeric
lowerAIsAlpha = 'a'

upperAIsAlpha : Refined Char AlphaNumeric
upperAIsAlpha = 'A'

zeroIsAlpha : Refined Char AlphaNumeric
zeroIsAlpha = '0'

-- TODO: Proof these using Void
--dollarIsNotAlpha : Refined Char AlphaNumeric -> Void
--dollarIsNotAlpha = '$'

blankIsWhitespace : Refined Char Whitespace
blankIsWhitespace = ' '

textIsNonEmpty : Refined String NonEmpty
textIsNonEmpty = "text"

-- FIXME: Somehow implicit conversion doesnt work here
oneIsGreaterThanZero : Refined Nat (Greater Z)
oneIsGreaterThanZero = toRefined $ S Z

--zeroIsGreaterThanZero : Refined Nat (Greater Z)
--zeroIsGreaterThanZero = toRefined $ Z

oneIsGreaterEqualOne : Refined Nat $ GreaterEqual $ S Z
oneIsGreaterEqualOne = toRefined $ S Z

zeroIsLessThanOne : Refined Nat (Less (S Z))
zeroIsLessThanOne = toRefined Z

--zeroIsLessThanZero : Refined Nat (Less Z)
--zeroIsLessThanZero = toRefined Z

testMe : IO()
testMe = putStrLn("Passed")

ext: idr

max_stars_repo_name: janschultecom/idris-refined

max_issues_repo_name: janschultecom/idris-refined

max_forks_repo_name: janschultecom/idris-refined


text:
module Quantities.Screen

import Quantities.Core
import Quantities.SIBaseQuantities
import Quantities.ImperialUnits
import Quantities.SIBaseUnits

%default total
%access public export

ScreenLength : Dimension
ScreenLength = MkDimension "ScreenLength"

Pixel : ElemUnit ScreenLength
Pixel = MkElemUnit "px" 1
Px : ElemUnit ScreenLength
Px = Pixel

ScreenArea : Quantity
ScreenArea = ScreenLength ^ 2
ScreenEstate : Quantity
ScreenEstate = ScreenArea

ScreenResolution : Quantity
ScreenResolution = ScreenLength </> Length

PixelPerCentimetre : ElemUnit ScreenResolution
PixelPerCentimetre = < one "ppcm" equals 1 (Pixel <//> Centimetre) >
PixelPerCentimeter : ElemUnit ScreenResolution
PixelPerCentimeter = PixelPerCentimetre
Ppcm : ElemUnit ScreenResolution
Ppcm = PixelPerCentimetre

PixelPerInch : ElemUnit ScreenResolution
PixelPerInch = < one "ppi" equals 1 (Pixel <//> Inch) >
Ppi : ElemUnit ScreenResolution
Ppi = PixelPerInch

max_stars_repo_name: timjb/quantities

max_issues_repo_name: timjb/quantities

max_forks_repo_name: timjb/quantities


text:
-- Idris2

module Sinter.ANF

import Data.List
import Data.Vect
import Data.String.Extra

import Core.Context
import Core.CompileExpr

import Compiler.ANF
import Compiler.Common
import Idris.Driver

------------
-- SINTER --
------------

sqBrack : String -> String
sqBrack s = "[ " ++ s ++ " ]"

-- only literals in sinter are ints
data SinterLit
  = SinInt Int Nat    -- TODO: Int is value then width
  | SinStr String

-- IDs are basically strings (not really, TODO)
data SinterID = MkSinterID String

genSinterID : SinterID -> String
genSinterID (MkSinterID id_) = id_

Show SinterID where
  show = genSinterID

-- declared here, defined later
data SinterGlobal : Type where

-- an expression is a list of expressions, an ID, or a literal
data Sexpr : Type where
  SexprList : (es : List Sexpr) -> Sexpr
  SexprID : (id_ : SinterID) -> Sexpr
  SexprLit : SinterLit -> Sexpr
  SexprLet : (next : Sexpr) -> (defFun : SinterGlobal) -> Sexpr  -- let-in for sinter

genSexpr : Sexpr -> String
genSexpr (SexprList []) = "[]"

genSexpr (SexprList es) =
  let
    exprs = map genSexpr es
  in sqBrack $ join " " exprs
--  in "[ " ++ (concat exprs) ++ " ]"

genSexpr (SexprID id_) = show id_

genSexpr (SexprLit (SinInt v w)) =
  "( " ++ show w ++ "; " ++ show v ++ " )"

genSexpr (SexprLit (SinStr s)) =
  show s

-- TODO
genSexpr (SexprLet next defFun) =
  genSexpr next

Show Sexpr where
  show = genSexpr

-------------------------------
-- Things that can be global --
-------------------------------

-- declared earlier, defined here
data SinterGlobal = SinDef SinterID (List SinterID) Sexpr
                  | SinDecl SinterID (List SinterID)
                  | SinType SinterID (List SinterID)

genSinter : SinterGlobal -> String
genSinter (SinDef fName args body) =
  let
    args' = map show args
    argsStr = sqBrack $ join " " args'
  in sqBrack $ "def " ++ show fName ++ " " ++ argsStr ++ "\n\t"
                ++ genSexpr body

genSinter (SinDecl fName args) =
  let
    args' = map show args
    argsStr = sqBrack $ join " " args'
  in sqBrack $ "dec " ++ show fName ++ " " ++ argsStr

genSinter (SinType tName membs) =
  let
    membs' = map show membs
    membsStr = sqBrack $ join " " membs'
  in sqBrack $ "type " ++ show tName ++ membsStr

Show SinterGlobal where
  show = genSinter

testCase : SinterGlobal
testCase = SinDef (MkSinterID "test") [(MkSinterID "arg1"), (MkSinterID "arg2")]
                  (SexprList [SexprLit (SinInt 1 2)])

-----------------------
-- Sinter primitives --
-----------------------

||| Primitive implemented in sinter
sinterPrim : String -> Sexpr
sinterPrim name = SexprID $ MkSinterID name

||| Primitive supplied by stdlib
sinterStdlib : String -> Sexpr
sinterStdlib name = SexprID $ MkSinterID ("stdlib_" ++ name)

||| Call the special sinter function for creating closures
sinterClosureCon : Sexpr
sinterClosureCon = sinterPrim ">makeClosure"

||| Call the special sinter function for running or adding args to closures
sinterClosureAdd : Sexpr
sinterClosureAdd = sinterPrim ">closureAddElem"

||| Crash sinter very inelegantly
sinterCrash : Sexpr
sinterCrash = SexprList [ sinterPrim "CRASH" ]

------------------
-- GORY DETAILS --
------------------

||| Symbol for indicating membership of namespace: "--|"
specialSep : String
specialSep = "--|"

||| Symbol for indicating record access: "."
recordAcc : String
recordAcc = "."

||| Separate two ids by "specialSep"
stitch : SinterID -> SinterID -> SinterID
stitch (MkSinterID x) (MkSinterID y) = MkSinterID $ x ++ specialSep ++ y

||| Turn a NS into a string separated by "specialSep"
mangleNS : Namespace -> SinterID
mangleNS ns = MkSinterID $ showNSWithSep specialSep ns

||| Sinter doesn't have a concept of NameSpaces, so define unique, but
||| identifiable names/strings instead.
mangle : Name -> SinterID
mangle (NS nameSpace name) =
  let
    nameSpace' = mangleNS nameSpace
    name' = mangle name
  in
    stitch nameSpace' name'

mangle (UN x) = MkSinterID x

mangle (MN x i) = MkSinterID $ x ++ "-" ++ show i

mangle (PV n i) = MkSinterID $ (show $ mangle n) ++ "-" ++ show i

--mangle (DN x y) = MkSinterID x      -- FIXME: correct? (assumes x repr.s y)
mangle (DN _ y) = mangle y            -- ^ incorrect! the Name itself still
                                      -- needs to be mangled; the way to display
                                      -- it doesn't necessarily match our way of
                                      -- representing names.

mangle (RF x) = MkSinterID $ recordAcc ++ x

mangle (Nested (i, j) n) =
  MkSinterID $ "nested_" ++ (show i) ++ "_" ++ (show j) ++ (show $ mangle n)

-- string repr.n of case followed by unique Int (?)
mangle (CaseBlock x i) = MkSinterID $ "case_" ++ x ++ "-" ++ (show i)

mangle (WithBlock x i) = MkSinterID $ "with_" ++ x ++ "-" ++ (show i)

mangle (Resolved i) = MkSinterID $ "resolved_" ++ (show i)

idrisWorld : Sexpr
idrisWorld = SexprID $ MkSinterID "**IDRIS_WORLD**"

||| Assume < 2^31 number of args to any function (seriously, what would you do
||| with 2^31 args?...)
nArgsWidth : Nat
nArgsWidth = 32

||| Turn all the arguments (including the scope) into SinterIDs
superArgsToSinter : List Name -> List SinterID
superArgsToSinter ns = map mangle ns

-- Constants

constantToSexpr : Constant -> Sexpr
constantToSexpr (I x) = ?sexprConstI
constantToSexpr (BI x) = ?sexprConstBI
constantToSexpr (B8 x) = SexprLit $ SinInt (cast x) 8
constantToSexpr (B16 x) = SexprLit $ SinInt (cast x) 16
constantToSexpr (B32 x) = SexprLit $ SinInt (cast x) 32
constantToSexpr (B64 x) = SexprLit $ SinInt (cast x) 64
constantToSexpr (Str x) = SexprLit $ SinStr x
constantToSexpr (Ch x) = ?constantToSexpr_rhs_8
constantToSexpr (Db x) = ?constantToSexpr_rhs_9
constantToSexpr WorldVal = idrisWorld
constantToSexpr IntType = ?constantToSexpr_rhs_11
constantToSexpr IntegerType = ?constantToSexpr_rhs_12
constantToSexpr Bits8Type = ?constantToSexpr_rhs_13
constantToSexpr Bits16Type = ?constantToSexpr_rhs_14
constantToSexpr Bits32Type = ?constantToSexpr_rhs_15
constantToSexpr Bits64Type = ?constantToSexpr_rhs_16
constantToSexpr StringType = ?constantToSexpr_rhs_17
constantToSexpr CharType = ?constantToSexpr_rhs_18
constantToSexpr DoubleType = ?constantToSexpr_rhs_19
constantToSexpr WorldType = ?constantToSexpr_rhs_20

intNameToSinterID : Int -> SinterID
intNameToSinterID i = MkSinterID $ "a" ++ show i

aVarToSexpr : AVar -> Sexpr
aVarToSexpr (ALocal i) = SexprID $ intNameToSinterID i
aVarToSexpr ANull = SexprLit $ SinInt 0 1

mutual
  -- Primitive Functions

  primFnToSexpr : PrimFn arity -> Vect arity AVar -> Sexpr
  primFnToSexpr (Add ty) [x, y] =
    SexprList [ sinterStdlib "add", aVarToSexpr x, aVarToSexpr y ]

  primFnToSexpr (Sub ty) [x, y] =
    SexprList [ sinterStdlib "sub", aVarToSexpr x, aVarToSexpr y ]

  primFnToSexpr (Mul ty) [x, y] =
    SexprList [ sinterStdlib "mul", aVarToSexpr x, aVarToSexpr y ]

  primFnToSexpr (Div ty) [x, y] =
    SexprList [ sinterStdlib "div", aVarToSexpr x, aVarToSexpr y ]

  primFnToSexpr (Mod ty) [x, y] =
    SexprList [ sinterStdlib "mod", aVarToSexpr x, aVarToSexpr y ]

  primFnToSexpr (Neg ty) [x] =
    SexprList [ sinterStdlib "neg", aVarToSexpr x ]

  primFnToSexpr (ShiftL ty) [x, y] =
    SexprList [ sinterStdlib "shiftl", aVarToSexpr x, aVarToSexpr y ]

  primFnToSexpr (ShiftR ty) [x, y] =
    SexprList [ sinterStdlib "shiftr", aVarToSexpr x, aVarToSexpr y ]

  primFnToSexpr (BAnd ty) [x, y] =
    SexprList [ sinterStdlib "bitwAnd", aVarToSexpr x, aVarToSexpr y ]

  primFnToSexpr (BOr ty) [x, y] =
    SexprList [ sinterStdlib "bitwOr", aVarToSexpr x, aVarToSexpr y ]

  primFnToSexpr (BXOr ty) [x, y] =
    SexprList [ sinterStdlib "bitwXor", aVarToSexpr x, aVarToSexpr y ]

  primFnToSexpr (LT ty) [x, y] =
    SexprList [ sinterStdlib "lt", aVarToSexpr x, aVarToSexpr y ]

  primFnToSexpr (LTE ty) [x, y] =
    SexprList [ sinterStdlib "lte", aVarToSexpr x, aVarToSexpr y ]

  primFnToSexpr (EQ ty) [x, y] =
    SexprList [ sinterStdlib "eq", aVarToSexpr x, aVarToSexpr y ]

  primFnToSexpr (GTE ty) [x, y] =
    SexprList [ sinterStdlib "gte", aVarToSexpr x, aVarToSexpr y ]

  primFnToSexpr (GT ty) [x, y] =
    SexprList [ sinterStdlib "gt", aVarToSexpr x, aVarToSexpr y ]

  -- TODO
  primFnToSexpr StrLength [s] = ?sinterStrLen
  primFnToSexpr StrHead [s] = ?sinterStrHead
  primFnToSexpr StrTail [s] = ?sinterStrTail
  primFnToSexpr StrIndex [s, i] = ?sinterStrIndex
  primFnToSexpr StrCons [s1, s2] = ?sinterStrCons
  primFnToSexpr StrAppend [s1, s2] =
    SexprList [ sinterStdlib "strAppend", aVarToSexpr s1, aVarToSexpr s2 ]
  primFnToSexpr StrReverse [s] = ?sinterStrReverse
  primFnToSexpr StrSubstr [i, j, s] = ?sinterSubstr

  -- TODO
  primFnToSexpr DoubleExp [d] = ?primFnToSexpr_rhs_25
  primFnToSexpr DoubleLog [d] = ?primFnToSexpr_rhs_26
  primFnToSexpr DoubleSin [d] = ?primFnToSexpr_rhs_27
  primFnToSexpr DoubleCos [d] = ?primFnToSexpr_rhs_28
  primFnToSexpr DoubleTan [d] = ?primFnToSexpr_rhs_29
  primFnToSexpr DoubleASin [d] = ?primFnToSexpr_rhs_30
  primFnToSexpr DoubleACos [d] = ?primFnToSexpr_rhs_31
  primFnToSexpr DoubleATan [d] = ?primFnToSexpr_rhs_32
  primFnToSexpr DoubleSqrt [d] = ?primFnToSexpr_rhs_33
  primFnToSexpr DoubleFloor [d] = ?primFnToSexpr_rhs_34
  primFnToSexpr DoubleCeiling [d] = ?primFnToSexpr_rhs_35

  -- TODO
  primFnToSexpr (Cast x y) [z] = ?primFnToSexpr_rhs_36
  primFnToSexpr BelieveMe [_, _, thing] = aVarToSexpr thing
                                        -- ^ I believe this is correct?

  primFnToSexpr Crash [fc, reason] =
    sinterCrash

  ||| Create a call to a function which evaluates `in` over `let`
  |||   let f x = y in z
  ||| is equivalent to
  |||   (\f . z) (\x . y)
  aLetToSexpr : FC -> (var : Int) -> (val : ANF) -> (in_expr : ANF) -> Sexpr
  aLetToSexpr fc var val in_expr =
    let
      varName = intNameToSinterID var
      cFunName = MkSinterID $ ">>let_" ++ ("a" ++ show var) ++ "_<<in_" ++ show fc
      val_sexpr = anfToSexpr val
      in_sexpr = anfToSexpr in_expr
      --cFunDef = SinDef $ cFunName val_sexpr
    in
      ?aLetToSexpr_rhs

  anfToSexpr : ANF -> Sexpr
  anfToSexpr (AV fc x) =
    aVarToSexpr x

  anfToSexpr (AAppName fc _ n fArgs) =
      let
        funName = SexprID $ mangle n
        funArgs = map aVarToSexpr fArgs
      in
        SexprList $ funName :: funArgs

  anfToSexpr (AUnderApp fc n missing partArgs) =
      let
        sinName  = SexprID $ mangle n
        sinMiss  = SexprLit $ SinInt (cast missing) nArgsWidth
        nArgs    = length partArgs
        sinNArgs = SexprLit $ SinInt (cast nArgs) nArgsWidth
        -- number of args function expects
        sinArity = SexprLit $ SinInt (cast (missing + nArgs)) nArgsWidth
        -- list of arguments
        sinArgs  = SexprList $ map aVarToSexpr partArgs
      in
        -- make a closure containing the above info (sinter-specific closure)
        SexprList [sinterClosureCon , sinName , sinArity , sinNArgs , sinArgs]

  -- application of a closure to another argument; potentially to the last arg
  anfToSexpr (AApp fc _ closure arg) =
    let
      sinClosure = aVarToSexpr closure
      sinArg = aVarToSexpr arg
    in
      SexprList [sinterClosureAdd, sinClosure, sinArg]

  anfToSexpr (ALet fc var let_expr in_expr) =
    aLetToSexpr fc var let_expr in_expr

  anfToSexpr (ACon fc n tag xs) =
    let
      (MkSinterID mn) = mangle n
      name = MkSinterID $ mn ++ show tag
      fArgs = map aVarToSexpr xs
    in
      SexprList $ (SexprID name) :: fArgs

  anfToSexpr (AOp fc _ fn args) = primFnToSexpr fn args

  anfToSexpr (AExtPrim fc _ n args) = ?anfToSexpr_rhs_8

  anfToSexpr (AConCase fc avar alts m_default) = ?anfToSexpr_rhs_9

  anfToSexpr (AConstCase fc x xs y) = ?anfToSexpr_rhs_10

  anfToSexpr (APrimVal fc c) = constantToSexpr c

  anfToSexpr (AErased fc) =
    SexprLit $ SinInt 0 0

  anfToSexpr (ACrash fc x) =
    sinterCrash

compileANF : (Name, ANFDef) -> Core SinterGlobal
compileANF (n, (MkAFun args body)) =
  let
    sinName = mangle n
    sinArgs = map intNameToSinterID args
    sinBody = anfToSexpr body
  in
    pure $ SinDef sinName sinArgs sinBody
compileANF (n, (MkACon tag arity def)) = ?compileANF_rhs_3
compileANF (n, (MkAForeign ccs fargs x)) = ?compileANF_rhs_4
compileANF (n, (MkAError e)) = ?compileANF_rhs_5

----------------
-- TOP OF API --
----------------

compile : Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
        ClosedTerm -> (outfile : String) -> Core (Maybe String)
compile context tmpDir outputDir term outfile =
  do compData <- getCompileData False ANF term
     let defs = anf compData
     sinterGlobs <- traverse compileANF defs
     -- readyForCG <- traverse bubbleLets sinterGlobs
     ?compile_rhs

execute : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
execute context tmpDir term =
  throw $ InternalError "Sinter backend can only compile, sorry."

sinterCodegen : Codegen
sinterCodegen = MkCG compile execute

main : IO ()
main = mainWithCodegens [("sinter", sinterCodegen)]


text:
module Main

import Test.Golden

url : TestPool
url = MkTestPool "URL tests" [] Nothing [ "url" ]

node : TestPool
node = MkTestPool "Node tests" [] (Just Node) [ "node/uri" ]

server : TestPool
server = MkTestPool "Server" [] (Just Node) [ "server/echo", "server/files" ]

ext : TestPool
ext = MkTestPool "Extensions" [] Nothing [ "ext/buffer" ]

main : IO ()
main = runner [ url, node, server, ext ]

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
module Specifiers

{- This tests both the given specifiers and the error reporting of them.
   To this end it tests via:
   --exec main      -- testing cli

   > :exec main     -- testing repl

   > :set eval exec -- repl with eval set to execute
   > main
-}

-- Generic match good for any scheme backend
%foreign "scheme:+"
plusGeneric : Int -> Int -> Int

-- We're testing with --cg chez so this specifier should be chosen.
%foreign "scheme,chez:+"
plusChez : Int -> Int -> Int

-- We're testing with --cg chez so this should match C because chez accepts C
-- specifiers but the next test should fail.
%foreign "scheme,racket:+"
         "C:notreal,notalib"
plusRacketOK : Int -> Int -> Int

-- We're testing with --cg chez so this shouldn't find a valid specifier to use.
%foreign "scheme,racket:+"
plusRacketFail : Int -> Int -> Int

-- We don't actually do any printing this is just to use the specifiers so the
-- failures are exposed.
main : IO ()
main = do
  printLn $ plusGeneric 2 3
  printLn $ plusChez 2 3
  printLn $ plusRacketOK 2 3
  printLn $ plusRacketFail 2 3
  pure ()


text:
module InteractiveEditing

import Data.Vect

%default total

%name Vect xs, ys, zs

{-
  <LocalLeader> a -> add initial clause
  <LocalLeader> c -> case split
  <LocalLeader> m -> add missing clause(s)
  <LocalLeader> s -> proof search
  <LocalLeader> w -> add with clause

-}

vzipwith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
vzipwith f [] [] = []
vzipwith f (x :: xs) (y :: ys) = f x y :: vzipwith f xs ys

max_stars_repo_name: timmyjose-study/idris-from-the-docs

max_issues_repo_name: timmyjose-study/idris-from-the-docs

max_forks_repo_name: timmyjose-study/idris-from-the-docs


text:
||| This was first introduced in chapter *Functor and Friends*
||| and is used in later chapters as well.
module Text.CSV

import Data.Fin
import Data.HList
import Data.List1
import Data.Maybe
import Data.String
import Data.Validated

%default total

--------------------------------------------------------------------------------
--          CSVField
--------------------------------------------------------------------------------

public export
interface CSVField a where
  read : String -> Maybe a

--------------------------------------------------------------------------------
--          Implementations
--------------------------------------------------------------------------------

public export
CSVField Bool where
  read "t" = Just True
  read "f" = Just False
  read _   = Nothing

public export
CSVField Nat where
  read = parsePositive

public export
CSVField Integer where
  read = parseInteger

public export
CSVField Double where
  read = parseDouble

public export
CSVField String where
  read = Just

boundedPos : Cast Nat a => (max : Nat) -> String -> Maybe a
boundedPos max str =
  parsePositive str >>= \v => toMaybe (v <= max) (cast v)

public export
CSVField Bits8 where
  read = boundedPos 0xff

public export
CSVField Bits16 where
  read = boundedPos 0xffff

public export
CSVField Bits32 where
  read = boundedPos 0xffffffff

public export
CSVField Bits64 where
  read = boundedPos 0xffffffffffffffff

boundedInt : Cast Integer a => (min,max : Integer) -> String -> Maybe a
boundedInt min max str =
  parseInteger str >>= \v => toMaybe (min <= v && v <= max) (cast v)

public export
CSVField Int8 where
  read = boundedInt (-0x80) 0x7f

public export
CSVField Int16 where
  read = boundedInt (-0x8000) 0x7fff

public export
CSVField Int32 where
  read = boundedInt (-0x80000000) 0x7fffffff

public export
CSVField Int64 where
  read = boundedInt (-0x8000000000000000) 0x7fffffffffffffff

public export
CSVField a => CSVField (Maybe a) where
  read "" = Just Nothing
  read s  = Just <$> read s

public export
{n : Nat} -> CSVField (Fin n) where
  read s = read s >>= (`natToFin` n)

--------------------------------------------------------------------------------
--          CSVError
--------------------------------------------------------------------------------

public export
data CSVError : Type where
  FieldError           : (line, column : Nat) -> (str : String) -> CSVError
  UnexpectedEndOfInput : (line, column : Nat) -> CSVError
  ExpectedEndOfInput   : (line, column : Nat) -> CSVError
  Append               : CSVError -> CSVError -> CSVError

public export
Show CSVError where
  showPrec p (FieldError l c s) =
    showCon p "FieldError" $ showArg l ++ showArg c ++ showArg s
  showPrec p (UnexpectedEndOfInput l c) =
    showCon p "UnexpectedEndOfInput" $ showArg l ++ showArg c
  showPrec p (ExpectedEndOfInput l c) =
    showCon p "ExpectedEndOfInput" $ showArg l ++ showArg c
  showPrec p (Append l r) =
    showCon p "Append" $ " " ++ showPrec App l ++ " " ++ showPrec App r

public export
Semigroup CSVError where
  (<+>) = Append

public export
readField : CSVField a => (line, col : Nat) -> String -> Validated CSVError a
readField line col str =
  maybe (Invalid $ FieldError line col str) Valid (read str)

--------------------------------------------------------------------------------
--          CSVLine
--------------------------------------------------------------------------------

public export
interface CSVLine a where
  decodeAt : (line, col : Nat) -> List String -> Validated CSVError a

public export
CSVLine (HList []) where
  decodeAt _ _ [] = Valid Nil
  decodeAt l c _  = Invalid (ExpectedEndOfInput l c)

public export
CSVField t => CSVLine (HList ts) => CSVLine (HList (t :: ts)) where
  decodeAt l c []        = Invalid (UnexpectedEndOfInput l c)
  decodeAt l c (s :: ss) = [| readField l c s :: decodeAt l (S c) ss |]

public export
decode : CSVLine a => (line : Nat) -> String -> Validated CSVError a
decode line = decodeAt line 1 . forget . split (',' ==)

public export
hdecode :  (0 ts : List Type)
        -> CSVLine (HList ts)
        => (line : Nat)
        -> String
        -> Validated CSVError (HList ts)
hdecode _ = decode


text:
||| Interpolation implementations
module Interp

import System.File.Error
import Data.Version
import Data.String.Extra

export
Interpolation Version where
  interpolate = show

export
Interpolation a => Interpolation (List a) where
  interpolate = join ", " . map interpolate

export
Interpolation FileError where
  interpolate (GenericFileError x) = show x
  interpolate FileReadError = "failed to read file"
  interpolate FileWriteError = "failed to write file"
  interpolate FileNotFound = "file was not found"
  interpolate PermissionDenied = "file has the wrong permissions"
  interpolate FileExists = "file already exists"

max_stars_repo_name: memoryruins/idv

max_issues_repo_name: memoryruins/idv

max_forks_repo_name: memoryruins/idv


text:
module Temp

import Data.List

foo : (l : List Int) -> String -> String
foo l "length" with (length l)
  foo l "length" | 0 = "Zero"
  foo l "length" | n = "Not Zero"
foo l s = "Other"


text:
||| Messages exchanged during the IDE protocol
module Protocol.IDE

import Protocol.SExp
import Data.List
import Data.Maybe

import public Libraries.Data.Span

import public Protocol.IDE.Command     as Protocol.IDE
import public Protocol.IDE.Decoration  as Protocol.IDE
import public Protocol.IDE.Formatting  as Protocol.IDE
import public Protocol.IDE.FileContext as Protocol.IDE
import public Protocol.IDE.Holes       as Protocol.IDE
import public Protocol.IDE.Result      as Protocol.IDE
import public Protocol.IDE.Highlight   as Protocol.IDE

%default total
------------------------------------------------------------------------

public export
Highlighting : Type
Highlighting = List (Span Properties)

export
SExpable a => SExpable (Span a) where
  toSExp (MkSpan start width ann)
    = SExpList [ IntegerAtom (cast start)
               , IntegerAtom (cast width)
               , toSExp ann
               ]

export
FromSExpable a => FromSExpable (Span a) where
  fromSExp (SExpList [ start
                     , width
                     , ann
                     ]) = do pure $ MkSpan { start = !(fromSExp start)
                                           , length = !(fromSExp width)
                                           , property  = !(fromSExp ann)}
  fromSExp _ = Nothing

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

public export
data ReplyPayload =
    OK    Result Highlighting
  | HighlightSource (List SourceHighlight)
  | Error String Highlighting

export
SExpable ReplyPayload where
  toSExp (OK    result hl) = SExpList (SymbolAtom "ok" :: toSExp result ::
    case hl of
      [] => []
      _ => [SExpList (map toSExp hl)])
  toSExp (HighlightSource hls) = SExpList
    [ SymbolAtom "ok"
    , SExpList
      [ SymbolAtom "highlight-source"
      , toSExp hls]
    ]
  toSExp (Error msg    hl) = SExpList (SymbolAtom "error" :: toSExp msg ::
    case hl of
      [] => []
      _  => [SExpList (map toSExp hl)])

-- Again, not the most efficient. Probably better to index by the
-- expected return type in the future
export
FromSExpable ReplyPayload where
  fromSExp (SExpList [SymbolAtom "ok", result])
    = do pure $ OK !(fromSExp result) []
  fromSExp (SExpList [SymbolAtom "ok", result, hl])
    = do pure $ OK !(fromSExp result) !(fromSExp hl)
  fromSExp (SExpList
    [ SymbolAtom "ok"
    , SExpList
      [ SymbolAtom "highlight-source"
      , hls]
    ]) = do pure $ HighlightSource !(fromSExp hls)
  fromSExp (SExpList [SymbolAtom "error", msg])
    = do pure $ Error !(fromSExp msg) []
  fromSExp (SExpList [SymbolAtom "error", msg, hl])
    = do pure $ Error !(fromSExp msg) !(fromSExp hl)
  fromSExp _ = Nothing

public export
data Reply =
    ProtocolVersion Int Int
  | Immediate    ReplyPayload Integer
  | Intermediate ReplyPayload Integer
  | WriteString String Integer
  | SetPrompt   String Integer
  | Warning FileContext String Highlighting Integer

export
SExpable Reply where
  toSExp (ProtocolVersion maj min) =  toSExp (SymbolAtom "protocol-version", maj, min)
  toSExp (   Immediate payload id) = SExpList [SymbolAtom "return",
                                                      toSExp payload, toSExp id]
  toSExp (Intermediate payload id) = SExpList [SymbolAtom "output",
                                                      toSExp payload, toSExp id]
  toSExp (WriteString str id) = SExpList [SymbolAtom "write-string", toSExp str, toSExp id]
  toSExp (SetPrompt str   id) = SExpList [SymbolAtom "set-prompt"  , toSExp str, toSExp id]
  toSExp (Warning fc str spans id) = SExpList [SymbolAtom "warning",
    SExpList $ toSExp fc.file :: toSExp (fc.range.startLine, fc.range.startCol)
                              :: toSExp (fc.range.endLine  , fc.range.endCol  )
                              :: toSExp str :: case spans of
      [] => []
      _  => [SExpList (map toSExp spans)]
      , toSExp id]

export
FromSExpable Reply where
  fromSExp (SExpList [SymbolAtom "protocol-version", major, minor]) =
     do Just $ ProtocolVersion !(fromSExp major) !(fromSExp minor)
  fromSExp (SExpList [SymbolAtom "return", payload, iden]) =
     do Just $ Immediate !(fromSExp payload) !(fromSExp iden)
  fromSExp (SExpList [SymbolAtom "output", payload, iden]) =
     do Just $ Intermediate !(fromSExp payload) !(fromSExp iden)
  fromSExp (SExpList [SymbolAtom "write-string", str, iden]) =
     do Just $ WriteString !(fromSExp str) !(fromSExp iden)
  fromSExp (SExpList [SymbolAtom "set-prompt", str, iden]) =
     do Just $ SetPrompt !(fromSExp str) !(fromSExp iden)
  fromSExp (SExpList [SymbolAtom "warning"
    , SExpList [filename, SExpList [startLine, startCol]
                      , SExpList [endLine  , endCol  ]
                      , str]
    , iden]) = do
      pure $ Warning (MkFileContext
           { file = !(fromSExp filename)
           , range = MkBounds { startLine = !(fromSExp startLine)
                              , startCol  = !(fromSExp startCol)
                              , endLine   = !(fromSExp endLine)
                              , endCol    = !(fromSExp endCol)}
           })
           !(fromSExp str)
           []
           !(fromSExp iden)
  fromSExp (SExpList [SymbolAtom "warning"
    , SExpList [filename, SExpList [startLine, startCol]
                      , SExpList [endLine  , endCol  ]
                      , str, hl]
    , iden]) = do
      pure $ Warning (MkFileContext
           { file = !(fromSExp filename)
           , range = MkBounds { startLine = !(fromSExp startLine)
                              , startCol  = !(fromSExp startCol)
                              , endLine   = !(fromSExp endLine)
                              , endCol    = !(fromSExp endCol)}
           })
           !(fromSExp str)
           !(fromSExp hl)
           !(fromSExp iden)
  fromSExp _ = Nothing

public export
data Request =
    Cmd IDECommand

export
SExpable Request where
  toSExp (Cmd cmd) = toSExp cmd

export
FromSExpable Request where
  fromSExp cmd = do pure $ Cmd !(fromSExp cmd)


text:
data State : (stateType : Type) -> Type -> Type where
  Get : State stateType stateType
  Put : stateType -> State stateType ()

  Pure : ty -> State stateType ty
  Bind : State stateType a -> (a -> State stateType b) -> State stateType b

get : State stateType stateType
get = Get

put : stateType -> State stateType ()
put = Put

pure : ty -> State stateType ty
pure = Pure

(>>=) : State stateType a -> (a -> State stateType b) -> State stateType b
(>>=) = Bind

{- Functor (State stateType) where
  map func x = Bind x (\val => Pure (func val))

Applicative (State stateType) where
  pure = Pure
  (<*>) f a = Bind f (\f' =>
              Bind a (\a' =>
              Pure (f' a')))

Monad (State stateType) where
  (>>=) = Bind-}

mutual
  Functor (State stateType) where
    map func x = do val <- x
                    pure (func val)

  Applicative (State stateType) where
    pure = Pure
    (<*>) f a = do f' <- f
                   a' <- a
                   pure (f' a')

  Monad (State stateType) where
    (>>=) = Bind

addIfPositive : Integer -> State Integer Bool
addIfPositive val = do when (val > 0) $
                             do current <- get
                                put (current + val)
                       pure (val > 0)

addPositives : List Integer -> State Integer Nat
addPositives vals = do added <- traverse addIfPositive vals
                       pure (length (filter id added))

runState : State stateType a -> (st : stateType) -> (a, stateType)
runState Get st = (st, st)
runState (Put newState) st = ((), newState)
runState (Pure x) st = (x, st)
runState (Bind cmd prog) st = let (val, nextState) = runState cmd st in
                                  runState (prog val) nextState


text:
-- ------------------------------------------------------------- [ Tibetan.idr ]
-- Module      : Text.Show.Tibetan
-- Description : Parsers for Tibetan numerals.
-- --------------------------------------------------------------------- [ EOH ]
||| Module with functions to display Tibetan numerals from Integers.
module Text.Show.Tibetan

%default total

replace : (Eq a) => a -> a -> List a -> List a
replace c1 c2 l = map (\c => if c == c1 then c2 else c) l

||| Given an integer, display it using Tibetan numerals, e.g.
|||
||| ```idris example
||| showBo 13
||| ```
export
showBo : (Integral a, Show a) => a -> String
showBo i = pack . foldr (.) id fs $ iString
  where iString = unpack . show $ i
        fs : List (List Char -> List Char)
        fs = zipWith replace ['0'..'9'] ['༠','༡','༢','༣','༤','༥','༦','༧','༨','༩']

export
showTest : (Integral a, Show a) => a -> String
showTest i = pack . foldr (.) id fs $ iString
  where iString = unpack . show $ i
        fs : List (List Char -> List Char)
        fs = zipWith replace ['0'..'9'] ['0'..'9']


text:
module SMTLibFinal

import Data.Vect

data NumTyp = IntT | RealT

data TypeT : Type where
  BoolT : TypeT
  NumT : NumTyp -> TypeT
  BitVecT : Nat -> TypeT

Show TypeT where
  show BoolT = "Bool"
  show (NumT IntT) = "Int"
  show (NumT RealT) = "Real"
  show (BitVecT n) = "BitVec " ++ show n

interface Smt where
  Expr : TypeT -> Type
  Cmd : Type -> Type

  (>>=) : Cmd a -> (a -> Cmd b) -> Cmd b
  pure : a -> Cmd a
  declareVar : String -> (t : TypeT) -> Cmd (Expr t)
  declareVars : Vect n String -> (t : TypeT) -> Cmd (Vect n (Expr t))
  assert : Expr BoolT -> Cmd ()
  checkSat : Cmd ()
  getModel : Cmd ()

  bool : Bool -> Expr BoolT
  bv : Int -> (n : Nat) -> Expr (BitVecT n)
  int : Int -> Expr (NumT IntT)
  real : Double -> Expr (NumT RealT)
  bvadd : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
  bvmul : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
  bvand : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
  bvor : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
  bvnot : Expr (BitVecT n) -> Expr (BitVecT n)
  (+) : Expr (NumT a) -> Expr (NumT a) -> Expr (NumT a)
  (*) : Expr (NumT a) -> Expr (NumT a) -> Expr (NumT a)
  (==) : Expr a -> Expr a -> Expr BoolT
  (&&) : Expr BoolT -> Expr BoolT -> Expr BoolT
  (||) : Expr BoolT -> Expr BoolT -> Expr BoolT
  not : Expr BoolT -> Expr BoolT
  ite : Expr BoolT -> Expr a -> Expr a -> Expr a

[smt] Smt where
  Expr _ = String
  Cmd a = (a, String)

  (>>=) (a, s) f = let (b, s') = f a in (b, s ++ "\n" ++ s')
  pure x = (x, "")
  declareVar x t = (x, "(declare-const " ++ x ++ " " ++ show t ++ ")")
  declareVars [] t = pure []
  declareVars (x :: xs) t = do x' <- declareVar x t
                               xs' <- declareVars xs t
                               pure $ x' :: xs'
  assert e = ((), "(assert " ++ e ++ ")")
  checkSat = ((), "(check-sat)")
  getModel = ((), "(get-model)")

  bool x = if x then "true" else "false"
  bv v n = "(_ bv" ++ show v ++ " " ++ show n ++ ")"
  int x = show x
  real x = show x
  bvadd l r = "(bvadd " ++ l ++ " " ++ r ++ ")"
  bvmul l r = "(bvmul " ++ l ++ " " ++ r ++ ")"
  bvand l r = "(bvand " ++ l ++ " " ++ r ++ ")"
  bvor l r = "(bvor " ++ l ++ " " ++ r ++ ")"
  bvnot x = "(bvnot " ++ x ++ ")"
  (+) l r = "(+ " ++ l ++ " " ++ r ++ ")"
  (*) l r = "(* " ++ l ++ " " ++ r ++ ")"
  (==) l r = "(= " ++ l ++ " " ++ r ++ ")"
  (&&) l r = "(and " ++ l ++ " " ++ r ++ ")"
  (||) l r = "(or " ++ l ++ " " ++ r ++ ")"
  not x = "(not " ++ x ++ ")"
  ite p l r = "(if " ++ p ++ " " ++ l ++ " " ++ r ++ ")"

example0 : Smt => Expr BoolT
example0 = (bool True) == (bool True)

example1 : Smt => Expr BoolT
example1 = (bv 1 8) == (bv 1 8)

example2 : Smt => Cmd ()
example2 = checkSat

example3 : Smt => Cmd ()
example3 = do x <- declareVar "x" BoolT
              y <- declareVar "y" BoolT
              assert $ not (x && y) == (not x || not y)
              checkSat
              getModel

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
import Postgres
import TestLib

setupQuery1 : String
setupQuery1 = "create table public.expected_types (i integer, d float8, b bool, t text, c char, j json, ai integer[], dm float8)"

setupQuery2 : String
setupQuery2 = "insert into public.expected_types (i, d, b, t, c, j, ai, dm) values (1, 2.5, true, 'hello', 'c', '{\"hello\": \"world\"}', '{1,2,3}', null)"

testQuery : String
testQuery = "select * from public.expected_types"

main : IO ()
main =
  ignore . withTestDB $ do
    res1 <- exec $ perform setupQuery1
    liftIO' . putStrLn $ show res1
    res2 <- exec $ perform setupQuery2
    liftIO' . putStrLn $ show res2
    Right (rows ** res3) <- exec $ expectedQuery [Integer, Double, Bool, String, Char, JSON, List Integer, Maybe Double] testQuery
      | Left err => liftIO' $ putStrLn err
    liftIO' . for_ res3 $ putStrLn . show

max_stars_repo_name: mattpolzin/pg-idris

max_issues_repo_name: mattpolzin/pg-idris

max_forks_repo_name: mattpolzin/pg-idris


text:
module Issue1191

main : IO ()
main = printLn (the Nat (1 + 2))


text:
module Crypto.Random.JS

import Crypto.Random
import System.FFI
import Data.Vect
import Utils.Misc
import Data.Buffer
import System.Info

%foreign "node:lambda:n => require('crypto').randomBytes(n)"
prim_io__randomBytes : Int -> PrimIO Buffer

-- Test this
%foreign "javascript:lambda:n => crypto.getRandomValues(new Uint8Array(n))"
prim_io__getRandomValues : Int -> PrimIO Buffer

buffer_content : HasIO io => (Int -> PrimIO Buffer) -> (n : Nat) -> io (Vect n Bits8)
buffer_content f n = do
  buffer <- primIO $ f (cast n)
  traverse (getBits8 buffer) $ map (cast . finToNat) range

public export
HasIO io => MonadRandom io where
  random_bytes Z = pure []
  random_bytes n =
  case codegen of
    "node" => buffer_content prim_io__randomBytes n
    "javascript" => buffer_content prim_io__getRandomValues n
    _ => assert_total $ idris_crash "no random backend availible"


text:
module Util

import Language.Reflection.TT
import Language.Reflection.TTImp

-- %language PostfixProjections

infixl 1 <&>
export
(<&>) : Functor f => f a -> (a -> b) -> f b
x <&> f = f <$> x

infixl 4 <$,$>

-- For when Lazy is causing type problems
infixr 4 &&|
export
(&&|) : Bool -> Bool -> Bool
(&&|) x y = x && y

export
zipWithSL : (a -> b -> c) -> Stream a -> List b -> List c
zipWithSL _ _ [] = []
zipWithSL f (x :: xs) (y :: ys) = f x y :: zipWithSL f xs ys

export
zipWithLS : (a -> b -> c) -> List a -> Stream b -> List c
zipWithLS _ [] _ = []
zipWithLS f (x :: xs) (y :: ys) = f x y :: zipWithLS f xs ys

export
%inline
zipSL : Stream a -> List b -> List (a,b)
zipSL = zipWithSL MkPair

export
%inline
zipLS : List a -> Stream b -> List (a,b)
zipLS = zipWithLS MkPair

-- provided by Data.List now
-- export
-- catMaybes : List (Maybe a) -> List a
-- catMaybes z = foldr (\m,f => maybe f (\x => (x ::) . f) m) id z []

export
unzip : List (a,b) -> (List a, List b)
unzip = foldr (\(x,y),(xs,ys) => (x :: xs, y :: ys)) ([],[])

export
isJust : Maybe a -> Bool
isJust (Just _ ) = True
isJust _ = False

export
unless : Applicative f => Bool -> Lazy (f ()) -> f ()
unless b act = if b then pure () else act

infixr 4 &&.
export
(&&) : (a -> Bool) -> Lazy (a -> Bool) -> a -> Bool
(&&) x y = \a => Prelude.(&&) (x a) (y a)

-- useful for working with TypeInfo cons without having a type just for that
-- Really we should just give cons its own type.
export
one : (a,b,c) -> a
one (x, (y, z)) = x

export
two : (a,b,c) -> b
two (x, (y, z)) = y

export
three : (a,b,c) -> c
three (x, (y, z)) = z

export
Range Char where
  rangeFromTo x y = map cast [cast x .. cast y] {a=Int}
  rangeFromThenTo x y z = map cast [cast x, cast y .. cast z] {a=Int}
  rangeFrom x = map cast [cast x ..] {a=Int}
  rangeFromThen x y = map cast [cast x, cast y..] {a=Int}


text:
> module SimpleProb.Functor

> import SimpleProb.SimpleProb
> import SimpleProb.MonadicOperations

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

> ||| |SimpleProb| is a functor:
> implementation Functor SimpleProb where
>   map = fmap

> {-

> ---}


text:
||| Spec: https://webassembly.github.io/spec/core/syntax/values.html#names
module WebAssembly.Structure.Values.Names

-- Definition

public export
Name : Type
Name = String

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
import Data.List.Views
import Data.Vect
import Data.Vect.Views
import Data.Nat.Views

equalSuffix : Eq a => List a -> List a -> List a
equalSuffix input1 input2 with (snocList input1)
  equalSuffix [] input2 | Empty = []
  equalSuffix (xs ++ [x]) input2 | (Snoc xsrec) with (snocList input2)
    equalSuffix (xs ++ [x]) [] | (Snoc xsrec) | Empty = []
    equalSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc xsrec) | (Snoc ysrec) =
        if x == y then (equalSuffix xs ys | xsrec | ysrec) ++ [x]
            else []

mergeSort : Ord a => Vect n a -> Vect n a
mergeSort input with (splitRec input)
  mergeSort [] | SplitRecNil = []
  mergeSort [x] | SplitRecOne = [x]
  mergeSort (xs ++ ys) | (SplitRecPair lrec rrec) =
    merge (mergeSort xs | lrec) (mergeSort ys | rrec)

toBinary : Nat -> String
toBinary k with (halfRec k)
  toBinary Z | HalfRecZ = ""
  toBinary (n + n) | (HalfRecEven rec) = toBinary n | rec ++ "0"
  toBinary (S (n + n)) | (HalfRecOdd rec) = toBinary n | rec ++ "1"

palindrome : Eq a => List a -> Bool
palindrome input with (vList input)
  palindrome [] | VNil = True
  palindrome [x] | VOne = True
  palindrome (x :: (xs ++ [y])) | (VCons rec) =
    if x == y then palindrome xs | rec
        else False


text:
module ggg

export
yyy : Int
yyy = 0


text:
module tipos

import Data.SortedMap

%access public export

mutual
  data Id = ValID String

  data AExp = Sum AExp AExp | Sub AExp AExp | Div AExp AExp | Mul AExp AExp | N Int | IdA Id

  data BExp = Equal AExp AExp | Not BExp | LT AExp AExp | GT AExp AExp | LE AExp AExp | GE AExp AExp | And BExp BExp | OR BExp BExp | Boo Bool | IdB Id

  data Exp = AExpR AExp | BExpR BExp | Ref Exp | DeRef Id | ValRef Id | Cns Exp

  data Formals = Form (List Id)

  data Actuals = Act (List Exp)

  data Cmd = Assign Id Exp | Loop BExp Cmd | Cond BExp Cmd Cmd | CSeq Cmd Cmd | Blk Dec Cmd | Call Id Actuals | NOP

  data Abst = Abstr Formals Cmd

  data Dec = Bind Id Exp | DSeq Dec Dec | BindF Id Abst | Rbnd Id Abst

  data CmdOp = CtrlAssign | CtrlLoop | CtrlCond | CtrlCSeq | CtrlBlkDec | CtrlBlkCmd | CtrlCall Id Nat

  data ExpOp = CtrlSum | CtrlSub | CtrlDiv | CtrlMul | CtrlNot | CtrlLT | CtrlGT | CtrlLE | CtrlGE | CtrlAnd | CtrlOR | CtrlEq | CtrlRef | CtrlCns

  data DecOp = CtrlBind | CtrlDSeq | CtrlBindF

  data Ctrl = CtExp Exp | CtExpOp ExpOp | CtCmd Cmd | CtDec Dec | CtCmdOp CmdOp | CtDecOp DecOp | CtAbs Abst

  data Loc = L Int

  data Bindable = BindLoc Loc | BindInt Int | BindClos Closure | BindRec Reclose

  data Val = ValInt Int | ValBool Bool | ValId String | ValCmd Cmd | ValLoc Loc | ValListLoc (List Loc) | ValEnv (SortedMap Id Bindable) | ValBindable Bindable | ValClos Closure | ValNop

  data Closure = Clos (Formals, Cmd, (SortedMap Id Bindable))

  data Reclose = Rec (Formals, Cmd, (SortedMap Id Bindable), (SortedMap Id Bindable))

  implementation Eq Loc where
    (L a) == (L b) = a == b
    (L a) /= (L b) = a /= b

  implementation Ord Loc where
    compare (L a) (L b) = compare a b

  implementation Eq Id where
    (ValID a) == (ValID b) = a == b
    (ValID a) /= (ValID b) = a /= b

  implementation Ord Id where
    compare (ValID a) (ValID b) = compare a b

  implementation Show Id where
    show (ValID x) = "ValID " ++ show x

  implementation Show AExp where
    show (Sum a b) = "Sum (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
    show (Sub a b) = "Sub (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
    show (Mul a b) = "Mul (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
    show (Div a b) = "Div (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
    show (N a) = "N " ++ show a
    show (IdA a) = "IdA (" ++ show a ++ ")"

  implementation Show BExp where
    show (Equal a b) = "Equal (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
    show (GT a b) = "GT (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
    show (LT a b) = "LT (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
    show (LE a b) = "LE (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
    show (GE a b) = "GE (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
    show (And a b) = "And (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
    show (OR a b) = "OR (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
    show (Boo a) = "Boo " ++ show a
    show (Not a) = "Not (" ++ show a ++ ")"
    show (IdB a) = "IdB (" ++ show a ++ ")"

  implementation Show Exp where
    show (AExpR a) = "AExpR (" ++ show a ++ ")"
    show (BExpR a) = "BExpR (" ++ show a ++ ")"
    show (Ref a) = "Ref (" ++ show a ++ ")"
    show (DeRef id) = "DeRef (" ++ show id ++ ")"
    show (ValRef id) = "ValRef (" ++ show id ++ ")"

  implementation Show Actuals where
    show (Act x) = "Act " ++ show x

  implementation Show Formals where
    show (Form x) = "Form " ++ show x

  implementation Show Abst where
    show (Abstr b c) = "Abstr (" ++ show b ++ ") " ++ "(" ++ show c ++ ")"

  implementation Show Dec where
    show (Bind a b) = "Bind (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
    show (DSeq a b) = "DSeq (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
    show (BindF a b) = "BindF (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
    show (Rbnd a b) = "Rbnd (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"

  implementation Show Cmd where
    show (Assign id exp) = "Assign (" ++ show id ++ ") " ++ "("++ show exp ++ ")"
    show (Loop b c) = "Loop (" ++ show b ++ ") " ++ "("++ show c ++ ")"
    show (Cond b c1 c2) = "Cond (" ++ show b ++ ") " ++ "("++ show c1 ++ ")" ++ " (" ++ show c2 ++ ")"
    show (CSeq c1 c2) = "CSeq (" ++ show c1 ++ ") " ++ "("++ show c2 ++ ")"
    show (Blk d c) = "Blk (" ++ show d ++ ") " ++ "("++ show c ++ ")"
    show (Call d c) = "Call (" ++ show d ++ ") " ++ "("++ show c ++ ")"
    show (NOP) = "NOP"

  implementation Show Closure where
    show (Clos (f, c, e)) = "Clos (" ++ show f ++ ", " ++ show c ++ ", " ++ show (toList e) ++ ")"

  implementation Show Reclose where
    show (Rec (f, c, e, e')) = "Clos (" ++ show f ++ ", " ++ show c ++ ", " ++ show (toList e) ++ show (toList e') ++ ")"

  implementation Show CmdOp where
    show CtrlAssign = "CtrlAssign"
    show CtrlLoop = "CtrlLoop"
    show CtrlCond = "CtrlCond"
    show CtrlCSeq = "CtrlCSeq"
    show CtrlBlkDec = "CtrlBlkDec"
    show CtrlBlkCmd = "CtrlBlkCmd"
    show (CtrlCall id tam) = "CtrlCall (" ++ show id ++ ") " ++ "(" ++ show tam ++ ")"

  implementation Show ExpOp where
    show CtrlSum = "CtrlSum"
    show CtrlSub = "CtrlSub"
    show CtrlDiv = "CtrlDiv"
    show CtrlMul = "CtrlMul"
    show CtrlNot = "CtrlNot"
    show CtrlLT = "CtrlLT"
    show CtrlGT = "CtrlGT"
    show CtrlLE = "CtrlLE"
    show CtrlGE = "CtrlGE"
    show CtrlAnd = "CtrlAnd"
    show CtrlOR = "CtrlOR"
    show CtrlEq = "CtrlEq"
    show CtrlRef = "CtrlRef"
    show CtrlCns = "CtrlCns"

  implementation Show DecOp where
    show CtrlBind = "CtrlBind"
    show CtrlDSeq = "CtrlDSeq"
    show CtrlBindF = "CtrlBindF"

  implementation Show Ctrl where
    show (CtExp a) = "CtExp (" ++ show a ++ ")"
    show (CtExpOp a) = "CtExpOp (" ++ show a ++ ")"
    show (CtCmd a) = "CtCmd (" ++ show a ++ ")"
    show (CtDec a) = "CtDec " ++ show a
    show (CtAbs a) = "CtAbs " ++ show a
    show (CtCmdOp a) = "CtCmdOp (" ++ show a ++ ")"
    show (CtDecOp a) = "CtDecOp (" ++ show a ++ ")"

  implementation Show Loc where
    show (L a) = "L " ++ show a

  implementation Show Bindable where
    show (BindLoc x) = "BindLoc (" ++ show x ++ ")"
    show (BindInt x) = "BindInt (" ++ show x ++ ")"
    show (BindClos x) = "BindClos (" ++ show x ++ ")"
    show (BindRec x) = "BindRec (" ++ show x ++ ")"

  implementation Show Val where
    show (ValInt a) = "ValInt (" ++ show a ++ ")"
    show (ValBool b) = "ValBool (" ++ show b ++ ")"
    show (ValId a) = "ValId (" ++ show a ++ ")"
    show (ValCmd a) = "ValCmd (" ++ show a ++ ")"
    show (ValLoc a) = "ValLoc (" ++ show a ++ ")"
    show (ValListLoc a) = "ValListLoc (" ++ show a ++ ")"
    show (ValEnv map) = "ValEnv (" ++ show (toList map) ++ ")"
    show (ValClos cls) = "ValClos (" ++ show cls ++ ")"
    show ValNop = "ValNop"

max_stars_repo_name: RonaldCamp/ImpCompiler

max_issues_repo_name: RonaldCamp/ImpCompiler

max_forks_repo_name: RonaldCamp/ImpCompiler


text:
module Compiler.ES.ES

import Compiler.Common
import Compiler.ES.Imperative
import Libraries.Utils.Hex
import Data.List1
import Data.Strings
import Libraries.Data.SortedMap
import Libraries.Data.String.Extra

import Core.Directory

%default covering

%hide Data.Strings.lines
%hide Data.Strings.lines'
%hide Data.Strings.unlines
%hide Data.Strings.unlines'

data ESs : Type where

record ESSt where
  constructor MkESSt
  preamble : SortedMap String String
  ccTypes : List String

jsString : String -> String
jsString s = "'" ++ (concatMap okchar (unpack s)) ++ "'"
  where
    okchar : Char -> String
    okchar c = if (c >= ' ') && (c /= '\\')
                  && (c /= '"') && (c /= '\'') && (c <= '~')
                  then cast c
                  else case c of
                            '\0' => "\\0"
                            '\'' => "\\'"
                            '"' => "\\\""
                            '\r' => "\\r"
                            '\n' => "\\n"
                            other => "\\u{" ++ asHex (cast {to=Int} c) ++ "}"

esName : String -> String
esName x = "__esPrim_" ++ x

addToPreamble : {auto c : Ref ESs ESSt} ->
                String -> String -> String -> Core String
addToPreamble name newName def =
  do
    s <- get ESs
    case lookup name (preamble s) of
      Nothing =>
        do
          put ESs (record { preamble = insert name def (preamble s) } s)
          pure newName
      Just x =>
        if x /= def
         then throw $ InternalError $ "two incompatible definitions for "
                         ++ name ++ "<|" ++ x ++"|> <|"++ def ++ "|>"
         else pure newName

addConstToPreamble : {auto c : Ref ESs ESSt} -> String -> String -> Core String
addConstToPreamble name def =
  do
    let newName = esName name
    let v = "const " ++ newName ++ " = (" ++ def ++ ");"
    addToPreamble name newName v

addSupportToPreamble : {auto c : Ref ESs ESSt} -> String -> String -> Core String
addSupportToPreamble name code =
  addToPreamble name name code

addStringIteratorToPreamble : {auto c : Ref ESs ESSt} -> Core String
addStringIteratorToPreamble =
  do
    let defs = unlines $
      [ "function __prim_stringIteratorNew(str) {"
      , "  return 0;"
      , "}"
      , "function __prim_stringIteratorToString(_, str, it, f) {"
      , "  return f(str.slice(it));"
      , "}"
      , "function __prim_stringIteratorNext(str, it) {"
      , "  if (it >= str.length)"
      , "    return {h: 0};"
      , "  else"
      , "    return {h: 1, a1: str.charAt(it), a2: it + 1};"
      , "}"
      ]
    let name = "stringIterator"
    let newName = esName name
    addToPreamble name newName defs

jsIdent : String -> String
jsIdent s = concatMap okchar (unpack s)
  where
    okchar : Char -> String
    okchar '_' = "_"
    okchar c = if isAlphaNum c
                  then cast c
                  else "$" ++ the (String) (asHex (cast {to=Int} c))

keywordSafe : String -> String
keywordSafe "var" = "var_"
keywordSafe s = s

jsName : Name -> String
jsName (NS ns n) = jsIdent (showNSWithSep "_" ns) ++ "_" ++ jsName n
jsName (UN n) = keywordSafe $ jsIdent n
jsName (MN n i) = jsIdent n ++ "_" ++ show i
jsName (PV n d) = "pat__" ++ jsName n
jsName (DN _ n) = jsName n
jsName (RF n) = "rf__" ++ jsIdent n
jsName (Nested (i, x) n) = "n__" ++ show i ++ "_" ++ show x ++ "_" ++ jsName n
jsName (CaseBlock x y) = "case__" ++ jsIdent x ++ "_" ++ show y
jsName (WithBlock x y) = "with__" ++ jsIdent x ++ "_" ++ show y
jsName (Resolved i) = "fn__" ++ show i

jsCrashExp : {auto c : Ref ESs ESSt} -> String -> Core String
jsCrashExp message  =
  do
    n <- addConstToPreamble "crashExp" "x=>{throw new IdrisError(x)}"
    pure $ n ++ "("++ message ++ ")"

toBigInt : String -> String
toBigInt e = "BigInt(" ++ e ++ ")"

fromBigInt : String -> String
fromBigInt e = "Number(" ++ e ++ ")"

useBigInt' : Int -> Bool
useBigInt' = (> 32)

useBigInt : IntKind -> Bool
useBigInt (Signed $ P x)     = useBigInt' x
useBigInt (Signed Unlimited) = True
useBigInt (Unsigned x)       = useBigInt' x

jsBigIntOfString : {auto c : Ref ESs ESSt} -> String -> Core String
jsBigIntOfString x =
  do
    n <- addConstToPreamble "bigIntOfString" "s=>{const idx = s.indexOf('.'); return idx === -1 ? BigInt(s) : BigInt(s.slice(0, idx));}"
    pure $ n ++ "(" ++ x ++ ")"

jsNumberOfString : {auto c : Ref ESs ESSt} -> String -> Core String
jsNumberOfString x = pure $ "parseFloat(" ++ x ++ ")"

jsIntOfString : {auto c : Ref ESs ESSt} -> IntKind -> String -> Core String
jsIntOfString k = if useBigInt k then jsBigIntOfString else jsNumberOfString

nSpaces : Nat -> String
nSpaces n = pack $ List.replicate n ' '

binOp : String -> String -> String -> String
binOp o lhs rhs = "(" ++ lhs ++ " " ++ o ++ " " ++ rhs ++ ")"

adjInt : Int -> String -> String
adjInt bits = if useBigInt' bits then toBigInt else id

toInt : IntKind -> String -> String
toInt k = if useBigInt k then toBigInt else id

fromInt : IntKind -> String -> String
fromInt k = if useBigInt k then fromBigInt else id

jsIntOfChar : IntKind -> String -> String
jsIntOfChar k s = toInt k $ s ++ ".codePointAt(0)"

jsIntOfDouble : IntKind -> String -> String
jsIntOfDouble k s = toInt k $ "Math.trunc(" ++ s ++ ")"

jsAnyToString : String -> String
jsAnyToString s = "(''+" ++ s ++ ")"

-- Valid unicode code poing range is [0,1114111], therefore,
-- we calculate the remainder modulo 1114112 (= 17 * 2^16).
jsCharOfInt : {auto c : Ref ESs ESSt} -> IntKind -> String -> Core String
jsCharOfInt k e =
  do fn <- addConstToPreamble
             ("truncToChar")
             ("x=>(x >= 0 && x <= 55295) || (x >= 57344 && x <= 1114111) ? x : 0")
     pure $ "String.fromCodePoint(" ++ fn ++ "(" ++ fromInt k e ++ "))"

makeIntBound : {auto c : Ref ESs ESSt} ->
               (isBigInt : Bool) -> Int -> Core String
makeIntBound isBigInt bits =
  let f    = if isBigInt then toBigInt else id
      name = if isBigInt then "bigint_bound_" else "int_bound_"
   in addConstToPreamble (name ++ show bits) (f "2" ++ " ** "++ f (show bits))

boundedInt :  {auto c : Ref ESs ESSt}
           -> (isBigInt : Bool)
           -> Int
           -> String
           -> Core String
boundedInt useBigInt bits e =
  let bs   = show bits
      f    = if useBigInt then toBigInt else id
      name = if useBigInt then "truncToBigInt" else "truncToInt"
   in do max  <- makeIntBound useBigInt bits
         half <- makeIntBound useBigInt (bits - 1)
         fn   <- addConstToPreamble
                  (name ++ show bits)
                  ( concat {t = List}
                      [ "x=>{ const v = x<",f "0","?x%",max,"+",max,":x%",max,";"
                      , "return v>=",half,"?","v-",max,":v}"
                      ])
         pure $ fn ++ "(" ++ e ++ ")"

boundedUInt : {auto c : Ref ESs ESSt} ->
              (isBigInt : Bool) -> Int -> String -> Core String
boundedUInt isBigInt bits e =
   let name = if isBigInt then "truncToUBigInt" else "truncToUInt"
    in do n  <- makeIntBound isBigInt bits
          fn <- addConstToPreamble
                  (name ++ show bits)
                  ("x=>{const m = x%" ++ n ++ ";return m>=0?m:m+" ++ n ++ "}")
          pure $ fn ++ "(" ++ e ++ ")"

boundedIntOp : {auto c : Ref ESs ESSt} ->
               Int -> String -> String -> String -> Core String
boundedIntOp bits o lhs rhs =
  boundedInt (useBigInt' bits) bits (binOp o lhs rhs)

boundedUIntOp : {auto c : Ref ESs ESSt} ->
                Int -> String -> String -> String -> Core String
boundedUIntOp bits o lhs rhs =
  boundedUInt (useBigInt' bits) bits (binOp o lhs rhs)

boolOp : String -> String -> String -> String
boolOp o lhs rhs = "(" ++ binOp o lhs rhs ++ " ? BigInt(1) : BigInt(0))"

jsConstant : {auto c : Ref ESs ESSt} -> Constant -> Core String
jsConstant (I i) = pure $ show i ++ "n"
jsConstant (I8 i) = pure $ show i
jsConstant (I16 i) = pure $ show i
jsConstant (I32 i) = pure $ show i
jsConstant (I64 i) = pure $ show i ++ "n"
jsConstant (BI i) = pure $ show i ++ "n"
jsConstant (Str s) = pure $ jsString s
jsConstant (Ch c) = pure $ jsString $ Data.Strings.singleton c
jsConstant (Db f) = pure $ show f
jsConstant WorldVal = addConstToPreamble "idrisworld" "Symbol('idrisworld')";
jsConstant (B8 i) = pure $ show i
jsConstant (B16 i) = pure $ show i
jsConstant (B32 i) = pure $ show i
jsConstant (B64 i) = pure $ show i ++ "n"
jsConstant ty = throw (InternalError $ "Unsuported constant " ++ show ty)

-- For multiplication of 32bit integers (signed or unsigned),
-- we go via BigInt and back, otherwise the calculation is
-- susceptible to rounding error, since we might exceed `MAX_SAFE_INTEGER`.
mult :  {auto c : Ref ESs ESSt}
        -> Maybe IntKind
        -> (x : String)
        -> (y : String)
        -> Core String
mult (Just $ Signed $ P 32) x y =
  fromBigInt <$> boundedInt True 32 (binOp "*" (toBigInt x) (toBigInt y))

mult (Just $ Unsigned 32)   x y =
  fromBigInt <$> boundedUInt True 32 (binOp "*" (toBigInt x) (toBigInt y))

mult (Just $ Signed $ P n) x y = boundedIntOp n "*" x y
mult (Just $ Unsigned n)   x y = boundedUIntOp n "*" x y
mult _                     x y = pure $ binOp "*" x y

div :  {auto c : Ref ESs ESSt}
       -> Maybe IntKind
       -> (x : String)
       -> (y : String)
       -> Core String
div (Just $ Signed $ Unlimited) x y = pure $ binOp "/" x y
div (Just $ k@(Signed $ P n)) x y =
  if useBigInt k then boundedIntOp n "/" x y
                 else boundedInt False n (jsIntOfDouble k (x ++ " / " ++ y))
div (Just $ k@(Unsigned n)) x y =
  if useBigInt k then pure $ binOp "/" x y
                 else pure $ jsIntOfDouble k (x ++ " / " ++ y)
div Nothing x y = pure $ binOp "/" x y

-- Creates the definition of a binary arithmetic operation.
-- Rounding / truncation behavior is determined from the
-- `IntKind`.
arithOp :  {auto c : Ref ESs ESSt}
        -> Maybe IntKind
        -> (op : String)
        -> (x : String)
        -> (y : String)
        -> Core String
arithOp (Just $ Signed $ P n) op x y = boundedIntOp n op x y
arithOp (Just $ Unsigned n)   op x y = boundedUIntOp n op x y
arithOp _                     op x y = pure $ binOp op x y

-- Same as `arithOp` but for bitwise operations that might
-- go out of the valid range.
-- Note: Bitwise operations on `Number` work correctly for
-- 32bit *signed* integers. For `Bits32` we therefore go via `BigInt`
-- in order not having to deal with all kinds of negativity nastiness.
bitOp :  {auto c : Ref ESs ESSt}
      -> Maybe IntKind
      -> (op : String)
      -> (x : String)
      -> (y : String)
      -> Core String
bitOp (Just $ Signed $ P n) op x y = boundedIntOp n op x y
bitOp (Just $ Unsigned 32)  op x y =
  fromBigInt <$> boundedUInt True 32 (binOp op (toBigInt x) (toBigInt y))
bitOp (Just $ Unsigned n)   op x y = boundedUIntOp n op x y
bitOp _                     op x y = pure $ binOp op x y

constPrimitives : {auto c : Ref ESs ESSt} -> ConstantPrimitives
constPrimitives = MkConstantPrimitives {
    charToInt    = \k => truncInt (useBigInt k) k . jsIntOfChar k
  , intToChar    = jsCharOfInt
  , stringToInt  = \k,s => jsIntOfString k s >>= truncInt (useBigInt k) k
  , intToString  = \_   => pure . jsAnyToString
  , doubleToInt  = \k => truncInt (useBigInt k) k . jsIntOfDouble k
  , intToDouble  = \k => pure . fromInt k
  , intToInt     = intImpl
  }
  where truncInt : (isBigInt : Bool) -> IntKind -> String -> Core String
        truncInt b (Signed Unlimited) = pure
        truncInt b (Signed $ P n)     = boundedInt b n
        truncInt b (Unsigned n)       = boundedUInt b n

        shrink : IntKind -> IntKind -> String -> String
        shrink k1 k2 = case (useBigInt k1, useBigInt k2) of
                            (True, False) => fromBigInt
                            _             => id

        expand : IntKind -> IntKind -> String -> String
        expand k1 k2 = case (useBigInt k1, useBigInt k2) of
                            (False,True) => toBigInt
                            _            => id

        -- when going from BigInt to Number, we must make
        -- sure to first truncate the BigInt, otherwise we
        -- might get rounding issues
        intImpl : IntKind -> IntKind -> String -> Core String
        intImpl k1 k2 s =
          let expanded = expand k1 k2 s
              shrunk   = shrink k1 k2 <$> truncInt (useBigInt k1) k2 s
           in case (k1,k2) of
                (_, Signed Unlimited)    => pure $ expanded
                (Signed m, Signed n)     =>
                  if n >= m then pure expanded else shrunk

                (Signed _, Unsigned n)   =>
                  case (useBigInt k1, useBigInt k2) of
                       (False,True)  => truncInt True k2 (toBigInt s)
                       _             => shrunk

                (Unsigned m, Unsigned n) =>
                  if n >= m then pure expanded else shrunk

                -- Only if the precision of the target is greater
                -- than the one of the source, there is no need to cast.
                (Unsigned m, Signed n)   =>
                  if n > P m then pure expanded else shrunk

jsOp : {0 arity : Nat} -> {auto c : Ref ESs ESSt} ->
       PrimFn arity -> Vect arity String -> Core String
jsOp (Add ty) [x, y] = arithOp (intKind ty) "+" x y
jsOp (Sub ty) [x, y] = arithOp (intKind ty) "-" x y
jsOp (Mul ty) [x, y] = mult (intKind ty) x y
jsOp (Div ty) [x, y] = div (intKind ty) x y
jsOp (Mod ty) [x, y] = arithOp (intKind ty) "%" x y
jsOp (Neg ty) [x] = pure $ "(-(" ++ x ++ "))"
jsOp (ShiftL Int32Type) [x, y] = pure $ binOp "<<" x y
jsOp (ShiftL ty) [x, y] = bitOp (intKind ty) "<<" x y
jsOp (ShiftR Int32Type) [x, y] = pure $ binOp ">>" x y
jsOp (ShiftR ty) [x, y] = bitOp (intKind ty) ">>" x y
jsOp (BAnd Bits32Type) [x, y] = pure . fromBigInt $ binOp "&" (toBigInt x) (toBigInt y)
jsOp (BOr Bits32Type) [x, y] = pure . fromBigInt $ binOp "|" (toBigInt x) (toBigInt y)
jsOp (BXOr Bits32Type) [x, y] = pure . fromBigInt $ binOp "^" (toBigInt x) (toBigInt y)
jsOp (BAnd ty) [x, y] = pure $ binOp "&" x y
jsOp (BOr ty) [x, y] = pure $ binOp "|" x y
jsOp (BXOr ty) [x, y] = pure $ binOp "^" x y
jsOp (LT ty) [x, y] = pure $ boolOp "<" x y
jsOp (LTE ty) [x, y] = pure $ boolOp "<=" x y
jsOp (EQ ty) [x, y] = pure $ boolOp "===" x y
jsOp (GTE ty) [x, y] = pure $ boolOp ">=" x y
jsOp (GT ty) [x, y] = pure $ boolOp ">" x y
jsOp StrLength [x] = pure $ toBigInt $ x ++ ".length"
jsOp StrHead [x] = pure $ "(" ++ x ++ ".charAt(0))"
jsOp StrTail [x] = pure $ "(" ++ x ++ ".slice(1))"
jsOp StrIndex [x, y] = pure $ "(" ++ x ++ ".charAt(" ++ fromBigInt y ++ "))"
jsOp StrCons [x, y] = pure $ binOp "+" x y
jsOp StrAppend [x, y] = pure $ binOp "+" x y
jsOp StrReverse [x] =
  do
    n <- addConstToPreamble "strReverse" "x => x.split('').reverse().join('')"
    pure $ n ++ "(" ++ x ++ ")"
jsOp StrSubstr [offset, length, str] =
  pure $ str ++ ".slice(" ++ fromBigInt offset ++ ", " ++ fromBigInt offset ++ " + " ++ fromBigInt length ++ ")"
jsOp DoubleExp [x] = pure $ "Math.exp(" ++ x ++ ")"
jsOp DoubleLog [x] = pure $ "Math.log(" ++ x ++ ")"
jsOp DoubleSin [x] = pure $ "Math.sin(" ++ x ++ ")"
jsOp DoubleCos [x] = pure $ "Math.cos(" ++ x ++ ")"
jsOp DoubleTan [x] = pure $ "Math.tan(" ++ x ++ ")"
jsOp DoubleASin [x] = pure $ "Math.asin(" ++ x ++ ")"
jsOp DoubleACos [x] = pure $ "Math.acos(" ++ x ++ ")"
jsOp DoubleATan [x] = pure $ "Math.atan(" ++ x ++ ")"
jsOp DoubleSqrt [x] = pure $ "Math.sqrt(" ++ x ++ ")"
jsOp DoubleFloor [x] = pure $ "Math.floor(" ++ x ++ ")"
jsOp DoubleCeiling [x] = pure $ "Math.ceil(" ++ x ++ ")"

jsOp (Cast StringType DoubleType) [x] = jsNumberOfString x
jsOp (Cast ty StringType) [x] = pure $ jsAnyToString x
jsOp (Cast ty ty2) [x]        = castInt constPrimitives ty ty2 x
jsOp BelieveMe [_,_,x] = pure x
jsOp (Crash) [_, msg] = jsCrashExp msg

readCCPart : String -> (String, String)
readCCPart x =
  let (cc, def) = break (== ':') x
  in (cc, drop 1 def)

searchForeign : List String -> List String -> Maybe String
searchForeign prefixes [] = Nothing
searchForeign prefixes (x::xs) =
  let (cc, def) = readCCPart x
  in if cc `elem` prefixes then Just def
                           else searchForeign prefixes xs

makeForeign : {auto d : Ref Ctxt Defs} -> {auto c : Ref ESs ESSt} -> Name -> String -> Core String
makeForeign n x =
  do
    let (ty, def) = readCCPart x
    case ty of
      "lambda" => pure $ "const " ++ jsName n ++ " = (" ++ def ++ ")\n"
      "support" =>
        do
          let (name, lib_) = break (== ',') def
          let lib = drop 1 lib_
          lib_code <- readDataFile ("js/" ++ lib ++ ".js")
          ignore $ addSupportToPreamble lib lib_code
          pure $ "const " ++ jsName n ++ " = " ++ lib ++ "_" ++ name ++ "\n"
      "stringIterator" =>
        do
          ignore addStringIteratorToPreamble
          case def of
            "new" => pure $ "const " ++ jsName n ++ " = __prim_stringIteratorNew;\n"
            "next" => pure $ "const " ++ jsName n ++ " = __prim_stringIteratorNext;\n"
            "toString" => pure $ "const " ++ jsName n ++ " = __prim_stringIteratorToString;\n"
            _ => throw (InternalError $ "invalid string iterator function: " ++ def ++ ", supported functions are \"new\", \"next\", \"toString\"")

      _ => throw (InternalError $ "invalid foreign type : " ++ ty ++ ", supported types are \"lambda\", \"support\"")

foreignDecl : {auto d : Ref Ctxt Defs} -> {auto c : Ref ESs ESSt} -> Name -> List String -> Core String
foreignDecl n ccs =
  do
    s <- get ESs
    case searchForeign (ccTypes s) ccs of
      Just x => makeForeign n x
      Nothing => throw (InternalError $ "No node or javascript definition found for " ++ show n ++ " in " ++ show ccs)

jsPrim : {auto c : Ref ESs ESSt} -> Name -> List String -> Core String
jsPrim (NS _ (UN "prim__newIORef")) [_,v,_] = pure $ "({value: "++ v ++"})"
jsPrim (NS _ (UN "prim__readIORef")) [_,r,_] = pure $ "(" ++ r ++ ".value)"
jsPrim (NS _ (UN "prim__writeIORef")) [_,r,v,_] = pure $ "(" ++ r ++ ".value=" ++ v ++ ")"
jsPrim (NS _ (UN "prim__newArray")) [_,s,v,_] = pure $ "(Array(Number(" ++ s ++ ")).fill(" ++ v ++ "))"
jsPrim (NS _ (UN "prim__arrayGet")) [_,x,p,_] = pure $ "(" ++ x ++ "[" ++ p ++ "])"
jsPrim (NS _ (UN "prim__arraySet")) [_,x,p,v,_] = pure $ "(" ++ x ++ "[" ++ p ++ "] = " ++ v ++ ")"
jsPrim (NS _ (UN "prim__os")) [] =
  do
    let oscalc = "(o => o === 'linux'?'unix':o==='win32'?'windows':o)"
    sysos <- addConstToPreamble "sysos" (oscalc ++ "(require('os').platform())")
    pure sysos
jsPrim (NS _ (UN "void")) [_, _] = jsCrashExp $ jsString $ "Error: Executed 'void'"  -- DEPRECATED. TODO: remove when bootstrap has been updated
jsPrim (NS _ (UN "prim__void")) [_, _] = jsCrashExp $ jsString $ "Error: Executed 'void'"
jsPrim (NS _ (UN "prim__codegen")) [] = do
    (cg :: _) <- ccTypes <$> get ESs
        | _ => pure "\"javascript\""
    pure $ jsString cg
jsPrim x args = throw $ InternalError $ "prim not implemented: " ++ (show x)

tag2es : Either Int String -> String
tag2es (Left x) = show x
tag2es (Right x) = jsString x

mutual
  impExp2es : {auto d : Ref Ctxt Defs} -> {auto c : Ref ESs ESSt} -> ImperativeExp -> Core String
  impExp2es (IEVar n) =
    pure $ jsName n
  impExp2es (IELambda args body) =
    pure $ "(" ++ showSep ", " (map jsName args) ++ ") => {" ++ !(imperative2es 0 body) ++ "}"
  impExp2es (IEApp f args) =
    pure $ !(impExp2es f) ++ "(" ++ showSep ", " !(traverse impExp2es args) ++ ")"
  impExp2es (IEConstant c) =
    jsConstant c
  impExp2es (IEPrimFn f args) =
    jsOp f !(traverseVect impExp2es args)
  impExp2es (IEPrimFnExt n args) =
    jsPrim n !(traverse impExp2es args)
  impExp2es (IEConstructorHead e) =
    pure $ !(impExp2es e) ++ ".h"
  impExp2es (IEConstructorTag x) =
    pure $ tag2es x
  impExp2es (IEConstructorArg i e) =
    pure $ !(impExp2es e) ++ ".a" ++ show i
  impExp2es (IEConstructor h args) =
    let argPairs = zipWith (\i,a => "a" ++ show i ++ ": " ++ a ) [1..length args] !(traverse impExp2es args)
    in pure $ "({" ++ showSep ", " (("h:" ++ tag2es h)::argPairs) ++ "})"
  impExp2es (IEDelay e) =
    pure $ "(()=>" ++ !(impExp2es e) ++ ")"
  impExp2es (IEForce e) =
    pure $ !(impExp2es e) ++ "()"
  impExp2es IENull =
    pure "undefined"

  imperative2es : {auto d : Ref Ctxt Defs} -> {auto c : Ref ESs ESSt} -> Nat -> ImperativeStatement -> Core String
  imperative2es indent DoNothing =
    pure ""
  imperative2es indent (SeqStatement x y) =
    pure $ !(imperative2es indent x) ++ "\n" ++ !(imperative2es indent y)
  imperative2es indent (FunDecl fc n args body) =
    pure $ nSpaces indent ++ "function " ++ jsName n ++ "(" ++ showSep ", " (map jsName args) ++ "){//"++ show fc ++"\n" ++
           !(imperative2es (indent+1) body) ++ "\n" ++ nSpaces indent ++ "}\n"
  imperative2es indent (ForeignDecl fc n path args ret) =
    pure $ !(foreignDecl n path) ++ "\n"
  imperative2es indent (ReturnStatement x) =
    pure $ nSpaces indent ++ "return " ++ !(impExp2es x) ++ ";"
  imperative2es indent (SwitchStatement e alts def) =
    do
      def <- case def of
                Nothing => pure ""
                Just x => pure $ nSpaces (indent+1) ++ "default:\n" ++ !(imperative2es (indent+2) x)
      let sw = nSpaces indent ++ "switch(" ++ !(impExp2es e) ++ "){\n"
      let alts = concat !(traverse (alt2es (indent+1)) alts)
      pure $ sw ++ alts ++ def ++ "\n" ++ nSpaces indent ++ "}"
  imperative2es indent (LetDecl x v) =
    case v of
      Nothing => pure $ nSpaces indent ++ "let " ++ jsName x ++ ";"
      Just v_ => pure $ nSpaces indent ++ "let " ++ jsName x ++ " = " ++ !(impExp2es v_) ++ ";"
  imperative2es indent (ConstDecl x v) =
    pure $ nSpaces indent ++ "const " ++ jsName x ++ " = " ++ !(impExp2es v) ++ ";"
  imperative2es indent (MutateStatement x v) =
    pure $ nSpaces indent ++ jsName x ++ " = " ++ !(impExp2es v) ++ ";"
  imperative2es indent (ErrorStatement msg) =
    pure $ nSpaces indent ++ "throw new Error("++ jsString msg ++");"
  imperative2es indent (EvalExpStatement e) =
    pure $ nSpaces indent ++ !(impExp2es e) ++ ";"
  imperative2es indent (CommentStatement x) =
    pure $ "\n/*" ++ x ++ "*/\n"
  imperative2es indent (ForEverLoop x) =
    pure $ nSpaces indent ++ "while(true){\n" ++ !(imperative2es (indent+1) x) ++ "\n" ++ nSpaces indent ++ "}"

  alt2es : {auto d : Ref Ctxt Defs} -> {auto c : Ref ESs ESSt} -> Nat -> (ImperativeExp, ImperativeStatement) -> Core String
  alt2es indent (e, b) = pure $ nSpaces indent ++ "case " ++ !(impExp2es e) ++ ": {\n" ++
                                !(imperative2es (indent+1) b) ++ "\n" ++ nSpaces (indent+1) ++ "break; }\n"

static_preamble : List String
static_preamble =
  [ "class IdrisError extends Error { }"
  , "function __prim_js2idris_array(x){if(x.length ===0){return {h:0}}else{return {h:1,a1:x[0],a2: __prim_js2idris_array(x.slice(1))}}}"
  , "function __prim_idris2js_array(x){const result = Array();while (x.h != 0) {result.push(x.a1); x = x.a2;}return result;}"
  ]

export
compileToES : Ref Ctxt Defs -> ClosedTerm -> List String -> Core String
compileToES c tm ccTypes =
  do
    (impDefs, impMain) <- compileToImperative c tm
    s <- newRef ESs (MkESSt empty ccTypes)
    defs <- imperative2es 0 impDefs
    main_ <- imperative2es 0 impMain
    let main = "try{" ++ main_ ++ "}catch(e){if(e instanceof IdrisError){console.log('ERROR: ' + e.message)}else{throw e} }"
    st <- get ESs
    let pre = showSep "\n" $ static_preamble ++ (SortedMap.values $ preamble st)
    pure $ pre ++ "\n\n" ++ defs ++ main

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
-- --------------------------------------------------------------- [ Stack.idr ]
-- Module    : Stack.idr
-- Copyright : (c) 2015,2016 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Helper functions to treat lists like a stack.
|||
||| A collection of aliases so that working on `List` which is used
||| like a stack, actually feels like working on a stack.
|||
||| This module is here as a convince than anything else.
module Data.Stack

-- TODO Make popS and peekS 'safe' using the magic of proofs

%access export
%default total

||| A Stack containing items of type `ty`.
|||
||| @ty The type of elements in the stack.
public export
Stack : (ty : Type) -> Type
Stack ty = List ty

||| Create an empty stack.
mkStack : Stack ty
mkStack = Nil

||| Push an element on the stack.
pushS : ty -> Stack ty -> Stack ty
pushS e Nil = [e]
pushS e xs  = e::xs

||| Initialise the stack with the given element.
initS : ty -> Stack ty
initS e = pushS e $ mkStack

||| Mass push the list of elements onto the stack.
pushSThings : List ty -> Stack ty -> Stack ty
pushSThings xs s = xs ++ s

||| Remove an element from the stack, returning the pair (head, tail).
popS : (s : Stack ty) -> {auto ok : isCons s = True} -> (ty, Stack ty)
popS Nil     {ok=Refl} impossible
popS (x::xs) {ok=p}    = (x,xs)

||| Remove an element from the stack, returning the pair (head, tail).
popS' : (s : Stack ty) -> Maybe (ty, Stack ty)
popS' Nil     = Nothing
popS' (x::xs) = Just (x,xs)

||| See what is at the top of the stack.
peekS' : (s : Stack ty) -> Maybe ty
peekS' Nil     = Nothing
peekS' (x::xs) = Just x

||| See what is at the top of the stack.
peekS : (s : Stack ty) -> {auto ok : isCons s = True} ->  ty
peekS Nil     {ok=Refl} impossible
peekS (x::xs) {ok=p}    = x

clear : Stack ty -> Stack ty
clear _ = mkStack

isSEmpty : Stack ty -> Bool
isSEmpty xs = isNil xs

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

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers