text:
module IdrisScript.Objects

import IdrisScript

%access public export

infixl 6 !!

Object : JS_IO (JSValue JSFunction)
Object = do
  obj <- jscall "Object" (JS_IO Ptr)
  pure $ MkJSFunction obj

||| Creates an empty JavaScript object.
empty : JS_IO (JSValue (JSObject "Object"))
empty = do
  obj <- jscall "new Object()" (JS_IO Ptr)
  pure $ MkJSObject obj

||| Sets the property `prop` to the value `val` for an object `obj`. Modifies
||| the original value.
setProperty : (prop : String)
           -> (val : JSValue a)
           -> (obj : JSValue (JSObject c))
           -> JS_IO (JSValue (JSObject c))
setProperty prop val obj = do
  jscall "%0[%1] = %2" (Ptr -> String -> Ptr -> JS_IO Ptr)
         (unpack obj) prop (unpack val)
  pure obj

||| Gets the property `prop` from an object `obj`.
getProperty : (prop : String)
           -> (obj : JSValue (JSObject c))
           -> JS_IO (Maybe (t ** JSValue t))
getProperty prop obj = do
  elm <- jscall "%0[%1]" (Ptr -> String -> JS_IO Ptr) (unpack obj) prop
  case !(typeOf elm) of
       JSUndefined => pure Nothing
       _           => pure $ Just !(pack elm)

||| Gets the property `prop` from an object `obj`.
(!!) : (obj : JSValue (JSObject c))
    -> (prop : String)
    -> JS_IO (Maybe (t : JSType ** JSValue t))
obj !! prop = getProperty prop obj

||| Checks if an object `obj` has the property `prop`.
hasOwnProperty : (prop : String)
              -> (obj : JSValue (JSObject c))
              -> JS_IO Bool
hasOwnProperty prop obj = do
  res <- jscall "%0.hasOwnProperty(%1)" (Ptr -> String -> JS_IO Int)
                (unpack obj) prop
  pure $ res == 1

||| Returns the keys of an object.
keys : JSValue (JSObject c) -> JS_IO (JSValue JSArray)
keys obj = do
  keys <- jscall "Object.keys(%0)" (Ptr -> JS_IO Ptr) (unpack obj)
  pure $ MkJSObject keys

||| Returns the constructor of an object.
constr : JSValue (JSObject c) -> JS_IO (JSValue JSFunction)
constr obj = do
  con <- jscall "%0.constructor" (Ptr -> JS_IO Ptr) (unpack obj)
  pure $ MkJSFunction con

||| Transforms a `Traversable` to an object.
toJSObject : (Traversable f, ToJS from to)
          => f (String, from)
          -> JS_IO (JSValue (JSObject "Object"))
toJSObject {from} {to} xs = do
  obj <- empty
  traverse_ (\x =>
      setProperty (fst x) (toJS {from} {to} (snd x)) obj
    ) xs
  pure obj

max_stars_repo_name: jimmyhmiller/IdrisScript

max_issues_repo_name: jimmyhmiller/IdrisScript

max_forks_repo_name: jimmyhmiller/IdrisScript


text:
-- --------------------------------------------------------------- [ Utils.idr ]
-- Module    : Utils.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Text.Markup.Edda.Reader.Utils

import Data.AVL.Dict

import Lightyear
import Lightyear.Char
import Lightyear.Strings

import Text.Markup.Edda.Model.Common
import Text.Markup.Edda.Model.Raw
import Text.Markup.Edda.Model.Processed

import Text.Markup.Edda.Process.Utils

%access export

-- ------------------------------------------------------------- [ Combinators ]

lexemeL : Monad m => ParserT String m a -> ParserT String m a
lexemeL p = space *> p

lexL : Monad m => ParserT String m a -> ParserT String m a
lexL p = lexemeL p

lex : Monad m => ParserT String m a -> ParserT String m a
lex p = lexeme p

-- ---------------------------------------------------------- [ String Parsers ]

char' : Char -> Parser ()
char' c = char c *> pure ()

private
pathChar : Parser Char
pathChar = urlChar <|> satisfy (isAlphaNum) <?> "Path Char"
  where
    urlChar : Parser Char
    urlChar = do
      c <- satisfy (const True)
      case c of
        '\\' => pure '\\'
        '/'  => pure '/'
        '.'  => pure '.'
        ':'  => pure ':'
        '#'  => pure '#'
        '='  => pure '='
        '?'  => pure '?'
        '-'  => pure '-'
        _    => satisfy (const False)

url : Parser String
url = map pack (some pathChar) <?> "URL"

word : Parser String
word = map pack (some alphaNum) <?> "Word"

punctuation : Parser Char
punctuation = satisfy (\x => not $ isAlphaNum x) <?> "Punctuation"

-- -------------------------------------------------------------- [ Misc Stuff ]

dealWithSrcAttrs : Maybe String
                -> (Dict String String)
                -> (Dict String String)
dealWithSrcAttrs Nothing         as = as
dealWithSrcAttrs (Just srcattrs) as = insert ("src_lang") (trim $ fst foo) $
                                      insert ("src_opts") (trim $ snd foo ) as
  where
    foo : (String, String)
    foo = break (== ' ') srcattrs

convertOpts : Maybe (List Char) -> Maybe String
convertOpts b = case b of
                  Just x => Just (pack x)
                  Nothing => Nothing

convertAttrs : Maybe (String, String) -> Dict String String
convertAttrs Nothing  = empty
convertAttrs (Just (k,v)) = insert k v empty

-- ----------------------------------------------------------------- [ Parsers ]

punc : Parser (EddaRaw INLINE)
punc = map Punc punctuation <?> "Raw Punctuation"

text : Parser (EddaRaw INLINE)
text = map (Font SerifTy) word <?> "Raw Word"

rsvp : List Char
rsvp = ['+', '=', '*', '/', '~', '_']

borderPunc : Parser (Char)
borderPunc = do
    c <- punctuation
    case c of
      ','  => satisfy (const False)
      '\'' => satisfy (const False)
      '\"' => satisfy (const False)
      x    => if x `elem` rsvp
                then satisfy (const False)
                else pure x

mText : Parser (EddaRaw INLINE)
mText = text <|> map Punc borderPunc <?> "Texted used in markup"

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

ext: idr

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
module Depling.TypeCheck

import Depling
import Depling.Incr
import Depling.Elevate
import Depling.Reduce
import Depling.Replace
import Depling.Decr
import Depling.Unification
import Utils
import Data.Vect

total
export
dType : Vect n (DAST n) -> DAST n -> DAST n
dType c (ʌ v) = index v c
dType c (λ at b) = λT at $ dType (map (incr 0) $ at :: c) b
dType c (λT at rt) = 𝕋
dType c (f =!= a) = (dType c f) =!= a
dType c 𝕋 = 𝕋
dType c (𝔽 at rt b) = λT at rt
dType c (𝕌 n t) = t
dType c (ℂ {a} (DConV n ats rt) as) = dAppN (elevate $ dLamN ats $ replace (sym $ plusZeroRightNeutral a) $ rt) (toList as)
dType c (ℙ v cn t f) = dType c f
dType c (𝔹 t) = t

public export
data DTypeError : Type where
	DTypeErrorV : DAST n -> List (DAST n) -> DTypeError

total
check : DAST n -> UnificationGroup n n -> Maybe DTypeError
check a (UnificationGroupV es {ne}) with (nubBy is_similar $ map fromEither es)
	check a (UnificationGroupV _ {ne}) | [e] = Nothing
	check a (UnificationGroupV _ {ne}) | es' = Just $ DTypeErrorV a es'

total
ensureType : Vect n (DAST n) -> DAST n -> DAST n -> List DTypeError
ensureType {n} c a t = catMaybes $ map (check a) $ unify (dType c a) t []

reverse : DRCtx n m -> Vect m (DAST m) -> Vect (n + m) (DAST (n + m))
reverse [] c = c
reverse {n=S n} {m} (h :: t) c = rewrite plusSuccRightSucc n m in reverse t $ map (incr 0) $ h :: c

total
export
typeCheck : Vect n (DAST n) -> DAST n -> List DTypeError
typeCheck c (ʌ v) = []
typeCheck c (λ at b) = typeCheck c at ++ ensureType c at 𝕋 ++ typeCheck (map (incr 0) $ at :: c) b
typeCheck c (λT at r) = typeCheck c at ++ ensureType c at 𝕋 ++ typeCheck (map (incr 0) $ at :: c) r ++ ensureType (map (incr 0) $ at :: c) r 𝕋
typeCheck {n} c ast@(f =!= a) =
	typeCheck c f ++
	typeCheck c a ++
	case lfreduce ft of
		λT fat b => ensureType c a fat
		_ => [DTypeErrorV ast [ft, λT at $ 𝕌 "result" 𝕋]]
	where
		ft : DAST n
		ft = dType c f
		at : DAST n
		at = dType c a
typeCheck c 𝕋 = []
typeCheck c (𝔽 at rt b) =
	typeCheck c at ++ ensureType c at 𝕋 ++
	typeCheck (map (incr 0) $ at :: c) rt ++ ensureType (map (incr 0) $ at :: c) rt 𝕋 ++
	typeCheck (map (incr 0 . incr 0) $ at :: (λT at rt) :: c) b ++ ensureType (map (incr 0 . incr 0) $ at :: (λT at rt) :: c) b (incr 1 rt)
typeCheck c (𝕌 n t) = typeCheck c t ++ ensureType c t 𝕋
typeCheck {n} c (ℂ (DConV {a} _ ats rt) as) = assert_total $ typeCheck c tca ++ ensureType c tca 𝕋
	where
		tca : DAST n
		tca = dAppN (elevate $ dLamN ats $ replace (sym $ plusZeroRightNeutral a) $ rt) (toList as)
typeCheck {n} c a@(ℙ v (DConV {a} _ ats rt) t f) =
	typeCheck c v ++
	typeCheck c f ++
	typeCheck (reverse (elevateRC {gte=LTEZero} ats) c) t ++
	(catMaybes $ map (check $ incr' a) groups) ++
	ensureType (map replace' $ reverse (elevateRC {gte=LTEZero} ats) c) (replace' t) (replace' $ incr' $ dType c f)
	where
		total
		groups : List (UnificationGroup (a + n) (a + n))
		groups =
			map (map $ either (Left . incr') (Right . elevate {gte = ltePlus'})) $
			unify (dType c v) rt []

		total
		replacements : List (DAST (a + n), DAST (a + n))
		replacements = do
			g <- groups
			let pr = primary g
			let UnificationGroupV es = g
			e <- es
			if e == pr
			then []
			else pure (fromEither pr, fromEither e)

		replace' : DAST (a + n) -> DAST (a + n)
		replace' a = foldl (\a, (p, r) => dReplace p r a) a replacements
typeCheck c (𝔹 t) = typeCheck c t ++ ensureType c t 𝕋

max_stars_repo_name: CoderPuppy/idris-depling

max_issues_repo_name: CoderPuppy/idris-depling

max_forks_repo_name: CoderPuppy/idris-depling


text:
module Record.List

import Data.List

-- All functions must be total
%default total

-- All definitions and functions are exported
%access public export

-- *** Properties of equality ***

symNot : Not (x = y) -> Not (y = x)
symNot notEqual Refl = notEqual Refl

-- *** Properties of List ***

consNotEqNil : {xs : List t} -> Not (x :: xs = [])
consNotEqNil Refl impossible

-- *** Properties of Elem ***

noEmptyElem : Not (Elem x [])
noEmptyElem Here impossible

noElemInCons : Not (Elem x (y :: ys)) -> Not (Elem x ys)
noElemInCons notElemCons elemTail = notElemCons $ There elemTail

ifNotElemThenNotEqual : Not (Elem x (y :: ys)) -> Not (x = y)
ifNotElemThenNotEqual notElemCons equal = notElemCons $ rewrite equal in Here

ifNotEqualNotElemThenNotInCons : Not (Elem x ys) -> Not (x = y) -> Not (Elem x (y :: ys))
ifNotEqualNotElemThenNotInCons nIsE nEq Here = nEq Refl
ifNotEqualNotElemThenNotInCons nIsE nEq (There th) = nIsE th

-- *** Predicates over lists ***

-- Represents that every element of the first list fulfills a predicate over the entire second list
data AllOverList : (t -> List u -> Type) -> List t -> List u -> Type where
  AllOverListNil : AllOverList p [] us
  AllOverListCons : (v : t) -> p v us -> AllOverList p ts us -> AllOverList p (v :: ts) us

-- All elements from the first list belong in the second list
AllInList : List t -> List t -> Type
AllInList ts us = AllOverList Elem ts us

-- No element from the first list belong in the second list
AllNotInList : List t -> List t -> Type
AllNotInList ts us = AllOverList (\x => \xs => Not (Elem x xs)) ts us

nothingIsInEmpty : (xs : List t) -> AllNotInList xs []
nothingIsInEmpty [] = AllOverListNil
nothingIsInEmpty (x :: xs) = AllOverListCons x noEmptyElem (nothingIsInEmpty xs)

ifAllNotInConsThenAllNotInRest : AllNotInList ls (x :: xs) -> AllNotInList ls xs
ifAllNotInConsThenAllNotInRest  AllOverListNil = AllOverListNil
ifAllNotInConsThenAllNotInRest {ls = l :: _} (AllOverListCons l nIsE notAllInList) =
  let allNotInRest = ifAllNotInConsThenAllNotInRest notAllInList
  in AllOverListCons l (noElemInCons nIsE) allNotInRest

ifAllNotInListAndValueNotInFirstOneThenNotInCons : Not (Elem y xs) -> AllNotInList xs ys -> AllNotInList xs (y :: ys)
ifAllNotInListAndValueNotInFirstOneThenNotInCons nIsE AllOverListNil = AllOverListNil
ifAllNotInListAndValueNotInFirstOneThenNotInCons nIsEY (AllOverListCons x nIsEX allNot) =
  let allNotInRest = ifAllNotInListAndValueNotInFirstOneThenNotInCons (noElemInCons nIsEY) allNot
      nEq = ifNotElemThenNotEqual nIsEY
      nIsEXCons = ifNotEqualNotElemThenNotInCons nIsEX (symNot nEq)
  in AllOverListCons x nIsEXCons allNotInRest

ifAllNotInListThenOthersAreNotInFirstOne : AllNotInList xs ys -> AllNotInList ys xs
ifAllNotInListThenOthersAreNotInFirstOne {ys} AllOverListNil = nothingIsInEmpty ys
ifAllNotInListThenOthersAreNotInFirstOne (AllOverListCons _ nIsE allNot) =
  let allNotInXs = ifAllNotInListThenOthersAreNotInFirstOne allNot
  in ifAllNotInListAndValueNotInFirstOneThenNotInCons nIsE allNotInXs

-- *** IsSet ***

data IsSet : List t -> Type where
  IsSetNil : IsSet []
  IsSetCons : Not (Elem x xs) -> IsSet xs -> IsSet (x :: xs)

ifSetThenNotElemFirst : IsSet (x :: xs) -> Not (Elem x xs)
ifSetThenNotElemFirst (IsSetCons notXIsInXs  _) = notXIsInXs

ifSetThenRestIsSet : IsSet (x :: xs) -> IsSet xs
ifSetThenRestIsSet (IsSetCons _ xsIsSet) = xsIsSet

ifNotSetHereThenNeitherThere : Not (IsSet xs) -> Not (IsSet (x :: xs))
ifNotSetHereThenNeitherThere notXsIsSet (IsSetCons xIsInXs xsIsSet) = notXsIsSet xsIsSet

ifIsElemThenConsIsNotSet : Elem x xs -> Not (IsSet (x :: xs))
ifIsElemThenConsIsNotSet xIsInXs (IsSetCons notXIsInXs xsIsSet) = notXIsInXs xIsInXs

-- Decidability function for IsSet
isSet : DecEq t => (xs : List t) -> Dec (IsSet xs)
isSet [] = Yes IsSetNil
isSet (x :: xs) with (isSet xs)
  isSet (x :: xs) | No notXsIsSet = No $ ifNotSetHereThenNeitherThere notXsIsSet
  isSet (x :: xs) | Yes xsIsSet with (isElem x xs)
    isSet (x :: xs) | Yes xsIsSet | No notXInXs = Yes $ IsSetCons notXInXs xsIsSet
    isSet (x :: xs) | Yes xsIsSet | Yes xInXs = No $ ifIsElemThenConsIsNotSet xInXs

-- *** Functions on List (lty, Type) ***

labelsOf: List (lty, Type) -> List lty
labelsOf = map fst

infixr 3 ://:

-- Deletes a single element from the list
(://:) : DecEq lty => lty -> List (lty, Type) -> List (lty, Type)
(://:) l [] = []
(://:) l ((l', ty) :: ts) with (decEq l l')
  (://:) l ((l', ty) :: ts) | Yes _ = ts
  (://:) l ((l', ty) :: ts) | No _  = (l', ty) :: (l ://: ts)

infixr 4 :///:

-- Deletes a list of elements from the list
(:///:) : DecEq lty => List lty -> List (lty, Type) -> List (lty, Type)
(:///:) [] ts = ts
(:///:) (l :: ls) ts = l ://: (ls :///: ts)

infixr 4 :||:

-- Returns the left union of two lists
(:||:) : DecEq lty => List (lty, Type) -> List (lty, Type) -> List (lty, Type)
(:||:) ts us = ts ++ ((labelsOf ts) :///: us)

infixr 4 :<:

-- Returns left projection of a list
(:<:) : DecEq lty => List lty -> List (lty, Type) -> List (lty, Type)
(:<:) _ [] = []
(:<:) ls ((l, ty) :: ts) with (isElem l ls)
  (:<:) ls ((l, ty) :: ts) | Yes _ = (l, ty) :: (ls :<: ts)
  (:<:) ls ((l, _) :: ts)  | No _  = ls :<: ts

infixr 4 :>:

-- Returns right projection of a lsit
(:>:) : DecEq lty => List lty -> List (lty, Type) -> List (lty, Type)
(:>:) _ [] = []
(:>:) ls ((l, ty) :: ts) with (isElem l ls)
  (:>:) ls ((l, _) :: ts)  | Yes _ = ls :>: ts
  (:>:) ls ((l, ty) :: ts) | No _  = (l, ty) :: (ls :>: ts)

-- *** Theorems on append ***

ifIsInOneThenIsInAppend : DecEq lty => {ts, us : List (lty, Type)} -> {l : lty} ->
                          Either (Elem l (labelsOf ts)) (Elem l (labelsOf us)) ->
                          Elem l (labelsOf (ts ++ us))
ifIsInOneThenIsInAppend (Left isE) = ifIsElemThenIsInAppendLeft isE
  where
    ifIsElemThenIsInAppendLeft : DecEq lty => {ts, us : List (lty, Type)} -> {l : lty} ->
                                 Elem l (labelsOf ts) -> Elem l (labelsOf (ts ++ us))
    ifIsElemThenIsInAppendLeft {ts=((_, _) :: _)} Here = Here
    ifIsElemThenIsInAppendLeft {ts=((_, _) :: _)} (There th) =
      let isEApp = ifIsElemThenIsInAppendLeft th
      in There isEApp
ifIsInOneThenIsInAppend (Right isE) = ifIsElemThenIsInAppendRight isE
  where
    ifIsElemThenIsInAppendRight : DecEq lty => {ts, us : List (lty, Type)} -> {l : lty} ->
                                  Elem l (labelsOf us) -> Elem l (labelsOf (ts ++ us))
    ifIsElemThenIsInAppendRight {ts=[]} isE' = isE'
    ifIsElemThenIsInAppendRight {ts=((_, _) :: _)} {us=[]} isE' = absurd $ noEmptyElem isE'
    ifIsElemThenIsInAppendRight {ts=((_, _) :: _)} {us=((_, _) :: _)} isE' =
      let isEApp = ifIsElemThenIsInAppendRight isE'
      in There isEApp

ifIsInAppendThenIsInOne : DecEq lty => {ts, us : List (lty, Type)} -> {l : lty} ->
                          Elem l (labelsOf (ts ++ us)) ->
                          Either (Elem l (labelsOf ts)) (Elem l (labelsOf us))
ifIsInAppendThenIsInOne {ts=[]} isE = Right isE
ifIsInAppendThenIsInOne {ts=((_, _) :: _)} Here = Left Here
ifIsInAppendThenIsInOne {ts=((_, _) :: _)} (There th) =
  case (ifIsInAppendThenIsInOne th) of
    Left isE => Left $ There isE
    Right isE => Right isE

ifNotInAppendThenNotInNeither : DecEq lty => {ts, us : List (lty, Type)} -> {l : lty} ->
                                Not (Elem l (labelsOf (ts ++ us))) ->
                                (Not (Elem l (labelsOf ts)), Not (Elem l (labelsOf us)))
ifNotInAppendThenNotInNeither {ts=[]} {us} {l} notInAppend = (nIsE1, nIsE2)
  where
    nIsE1 : Not (Elem l [])
    nIsE1 isE = noEmptyElem isE

    nIsE2 : Not (Elem l (labelsOf us))
    nIsE2 isE = notInAppend isE
ifNotInAppendThenNotInNeither {ts=((lt, tyt) :: ts)} {us} {l} nIsEApp = (nIsE1, nIsE2)
  where
    nIsE1 : Not (Elem l (labelsOf ((lt, tyt) :: ts)))
    nIsE1 a with (decEq l lt)
      nIsE1 a | Yes ok
        = case a of
            Here     => nIsEApp Here
            There th => nIsEApp (rewrite ok in Here)
      nIsE1 a | No contra
        = case a of
            Here     => contra Refl
            There th => let isEApp = ifIsInOneThenIsInAppend (Left th)
                        in  nIsEApp (There isEApp)

    nIsE2 : Not (Elem l (labelsOf us))
    nIsE2 isE =
      let isEApp = ifIsInOneThenIsInAppend (Right isE)
      in nIsEApp (There isEApp)

ifNotInNeitherThenNotInAppend : DecEq lty => {ts, us : List (lty, Type)} -> {l : lty} ->
                               (Not (Elem l (labelsOf ts)), Not (Elem l (labelsOf us))) ->
                               Not (Elem l (labelsOf (ts ++ us)))
ifNotInNeitherThenNotInAppend {ts=[]} (_, nIsE2) isEApp = nIsE2 isEApp
ifNotInNeitherThenNotInAppend {ts=((_, _) :: _)} (nIsE1, _) Here = nIsE1 Here
ifNotInNeitherThenNotInAppend {ts=((_, _) :: _)} (nIsE1, nIsE2) (There th) =
  let nIsEApp = ifNotInNeitherThenNotInAppend ((noElemInCons nIsE1), nIsE2)
  in nIsEApp th

ifAppendIsSetThenEachIsSet : DecEq lty => {ts, us : List (lty, Type)} ->
                             IsSet (labelsOf (ts ++ us)) ->
                             (IsSet (labelsOf ts), IsSet (labelsOf us))
ifAppendIsSetThenEachIsSet {ts=[]} isS = (IsSetNil, isS)
ifAppendIsSetThenEachIsSet {ts=((_, _) :: _)} (IsSetCons nIsE isS) =
  let (isSLeft, isSRight) = ifAppendIsSetThenEachIsSet isS
      nIsELeft = fst $ ifNotInAppendThenNotInNeither nIsE
  in (IsSetCons nIsELeft isSLeft, isSRight)

ifEachIsSetThenAppendIsSet : DecEq lty => {ts, us : List (lty, Type)} ->
                             (IsSet (labelsOf ts), IsSet (labelsOf us)) -> AllNotInList (labelsOf ts) (labelsOf us) ->
                             IsSet (labelsOf (ts ++ us))
ifEachIsSetThenAppendIsSet {ts=[]} (_, isSU) AllOverListNil = isSU
ifEachIsSetThenAppendIsSet {ts=(l, _) :: ts} {us} ((IsSetCons nIsET isST), isSU) (AllOverListCons l nIsEU overList) =
  let isSApp = ifEachIsSetThenAppendIsSet {ts} {us} (isST, isSU) overList
      nIsEApp = ifNotInNeitherThenNotInAppend (nIsET, nIsEU)
  in IsSetCons nIsEApp isSApp

-- *** Theorems on delete ***

ifDeleteThenIsNotElem : DecEq lty => {ts : List (lty, Type)} -> (l : lty) -> {l' : lty} ->
                             Not (Elem l' (labelsOf ts)) -> Not (Elem l' (labelsOf (l ://: ts)))
ifDeleteThenIsNotElem {ts=[]} l {l'} nIsE isEDel = absurd $ noEmptyElem isEDel
ifDeleteThenIsNotElem {ts=(l'', ty)::ts} l {l'} nIsE isEDel with (decEq l l'')
  ifDeleteThenIsNotElem {ts=(l, ty)::ts} l {l'} nIsE isEDel      | Yes Refl = (noElemInCons nIsE) isEDel
  ifDeleteThenIsNotElem {ts=(l', ty)::ts} l {l'} nIsE Here       | No contra = nIsE Here
  ifDeleteThenIsNotElem {ts=(l'', ty)::ts} l {l'} nIsE (There th)| No _ =
                             ifDeleteThenIsNotElem l {l'} {ts} (noElemInCons nIsE) th

ifDeleteThenIsSet : DecEq lty => {ts : List (lty, Type)} -> (l : lty) -> IsSet (labelsOf ts) -> IsSet (labelsOf (l ://: ts))
ifDeleteThenIsSet {ts=[]} l isS = IsSetNil
ifDeleteThenIsSet {ts=(l', ty)::ts} l (IsSetCons nIsE isS) with (decEq l l')
  ifDeleteThenIsSet {ts=(l, ty)::ts} l (IsSetCons nIsE isS)  | Yes Refl = isS
  ifDeleteThenIsSet {ts=(l', ty)::ts} l (IsSetCons nIsE isS) | No _  =
    let nIsEDel = ifDeleteThenIsNotElem l {l'} nIsE
        isSDel = ifDeleteThenIsSet l isS
    in IsSetCons nIsEDel isSDel

-- *** Theorems on delete labels ***

ifDeleteLabelsThenIsNotElem : DecEq lty => {ts : List (lty, Type)} -> {l : lty} -> (ls : List lty) ->
                             Not (Elem l (labelsOf ts)) -> Not (Elem l (labelsOf (ls :///: ts)))
ifDeleteLabelsThenIsNotElem [] nIsE isEDel = absurd $ nIsE isEDel
ifDeleteLabelsThenIsNotElem {ts} {l} (l' :: ls) nIsE isEDel =
  let nIsEDelLabels = ifDeleteLabelsThenIsNotElem ls {ts} nIsE
  in ifDeleteThenIsNotElem {l'=l} {ts=ls :///: ts} l' nIsEDelLabels isEDel

ifDeleteLabelsThenIsSet : DecEq lty => {ts : List (lty, Type)} -> (ls : List lty) -> IsSet (labelsOf ts) -> IsSet (labelsOf (ls :///: ts))
ifDeleteLabelsThenIsSet [] isS = isS
ifDeleteLabelsThenIsSet (l :: ls) isS =
  let isSSub = ifDeleteLabelsThenIsSet ls isS
  in ifDeleteThenIsSet l isSSub

ifDeleteThenResultsAreNotInList : DecEq lty => {ts : List (lty, Type)} -> {ls : List lty} -> (l : lty) ->
  AllNotInList ls (labelsOf ts) -> IsSet (labelsOf ts) ->
  AllNotInList (l :: ls) (labelsOf (l ://: ts))
ifDeleteThenResultsAreNotInList {ts=[]} l overList _ = AllOverListCons l noEmptyElem overList
ifDeleteThenResultsAreNotInList {ts=(l', _) :: ts} l overList isS with (decEq l l')
  ifDeleteThenResultsAreNotInList {ts=(l, _) :: ts} l overList (IsSetCons nIsE _) | Yes Refl =
    let allNotInTs = ifAllNotInConsThenAllNotInRest overList
    in AllOverListCons l nIsE allNotInTs
  ifDeleteThenResultsAreNotInList {ts=(l', _) :: ts} l overList (IsSetCons _ isS) | No nEq =
    let overRest = ifAllNotInConsThenAllNotInRest overList
        delAreNotInRest = ifDeleteThenResultsAreNotInList {ts} l overRest isS
        (AllOverListCons _ nIsELSupInLs _) = ifAllNotInListThenOthersAreNotInFirstOne overList
        nIsELSupInCons = ifNotEqualNotElemThenNotInCons nIsELSupInLs (symNot nEq)
    in ifAllNotInListAndValueNotInFirstOneThenNotInCons nIsELSupInCons delAreNotInRest

ifDeleteLabelsThenNoneAreInList : DecEq lty => (ls : List lty) -> (ts : List (lty, Type)) ->
                                  IsSet (labelsOf ts) ->
                                  AllNotInList ls (labelsOf (ls :///: ts))
ifDeleteLabelsThenNoneAreInList [] _ _ = AllOverListNil
ifDeleteLabelsThenNoneAreInList (l :: ls) ts isS =
  let nInListTs = ifDeleteLabelsThenNoneAreInList ls ts isS
      isSDel = ifDeleteLabelsThenIsSet ls isS
  in ifDeleteThenResultsAreNotInList {ts = ls :///: ts} l nInListTs isSDel

-- *** Theorems on left union ***

ifLeftUnionThenIsNotElem : DecEq lty => {ts, us : List (lty, Type)} -> (l : lty) ->
                           Not (Elem l (labelsOf ts)) -> Not (Elem l (labelsOf us)) ->
                           Not (Elem l (labelsOf (ts :||: us)))
ifLeftUnionThenIsNotElem {ts} {us} l nIsET nIsEU =
  let nIsEDelLabels = ifDeleteLabelsThenIsNotElem {ts=us} (labelsOf ts) nIsEU
      nIsEApp = ifNotInNeitherThenNotInAppend (nIsET, nIsEDelLabels)
  in nIsEApp

ifLeftUnionThenisSet : DecEq lty => {ts, us : List (lty, Type)} ->
                       IsSet (labelsOf ts) -> IsSet (labelsOf us) ->
                       IsSet (labelsOf (ts :||: us))
ifLeftUnionThenisSet {ts} {us} isS1 isS2 =
  let isSDel = ifDeleteLabelsThenIsSet {ts=us} (labelsOf ts) isS2
      delLabelsNotInList = ifDeleteLabelsThenNoneAreInList (labelsOf ts) us isS2
      isSApp = ifEachIsSetThenAppendIsSet {ts} {us=(labelsOf ts) :///: us} (isS1, isSDel) delLabelsNotInList
  in isSApp

-- *** Theorems on left projection ***

ifProjectLeftThenIsNotElem : DecEq lty => {ts : List (lty, Type)} -> (ls : List lty) ->
                             Not (Elem l (labelsOf ts)) -> Not (Elem l (labelsOf (ls :<: ts)))
ifProjectLeftThenIsNotElem {ts=[]} ls nIsE isEProj = noEmptyElem isEProj
ifProjectLeftThenIsNotElem {ts=(l', _) :: ts} {l} ls nIsE isEProj with (isElem l' ls)
  ifProjectLeftThenIsNotElem {ts=(l, _) :: ts} {l} _ nIsE Here         | Yes _ = nIsE Here
  ifProjectLeftThenIsNotElem {ts=(l', _) :: ts} {l} ls nIsE (There th) | Yes _ =
    ifProjectLeftThenIsNotElem {ts} ls (noElemInCons nIsE) th
  ifProjectLeftThenIsNotElem {ts=(l', _) :: ts} {l} ls nIsE isEProj    | No _  =
    ifProjectLeftThenIsNotElem {ts} ls (noElemInCons nIsE) isEProj

ifProjectLeftThenIsSet : DecEq lty => {ts : List (lty, Type)} -> (ls : List lty) ->
                         IsSet (labelsOf ts) -> IsSet (labelsOf (ls :<: ts))
ifProjectLeftThenIsSet {ts=[]} _ _ = IsSetNil
ifProjectLeftThenIsSet {ts=(l, _) :: ts} ls isS with (isElem l ls)
  ifProjectLeftThenIsSet {ts=(l, _) :: ts} ls (IsSetCons nIsE isS) | Yes _ =
    let nIsEInProj = ifProjectLeftThenIsNotElem {ts} ls nIsE
        isSProj = ifProjectLeftThenIsSet {ts} ls isS
    in IsSetCons nIsEInProj isSProj
  ifProjectLeftThenIsSet {ts=(l, _) :: ts} ls (IsSetCons _ isS)    | No _  =
                         ifProjectLeftThenIsSet ls isS

-- *** Theorems on right projection ***

ifProjectRightThenIsNotElem : DecEq lty => {ts : List (lty, Type)} -> (ls : List lty) ->
                             Not (Elem l (labelsOf ts)) -> Not (Elem l (labelsOf (ls :>: ts)))
ifProjectRightThenIsNotElem {ts=[]} ls nIsE isEProj = noEmptyElem isEProj
ifProjectRightThenIsNotElem {ts=(l', _) :: ts} {l} ls nIsE isEProj with (isElem l' ls)
  ifProjectRightThenIsNotElem {ts=(l', _) :: ts} {l} ls nIsE isEProj    | Yes _  =
    ifProjectRightThenIsNotElem {ts} ls (noElemInCons nIsE) isEProj
  ifProjectRightThenIsNotElem {ts=(l, _) :: ts} {l} _ nIsE Here         | No _ = nIsE Here
  ifProjectRightThenIsNotElem {ts=(l', _) :: ts} {l} ls nIsE (There th) | No _ =
    ifProjectRightThenIsNotElem {ts} ls (noElemInCons nIsE) th

ifProjectRightThenIsSet : DecEq lty => {ts : List (lty, Type)} -> (ls : List lty) ->
                         IsSet (labelsOf ts) -> IsSet (labelsOf (ls :>: ts))
ifProjectRightThenIsSet {ts=[]} _ _ = IsSetNil
ifProjectRightThenIsSet {ts=(l, _) :: ts} ls isS with (isElem l ls)
  ifProjectRightThenIsSet {ts=(l, _) :: ts} ls (IsSetCons _ isS)    | Yes _ =
                         ifProjectRightThenIsSet ls isS
  ifProjectRightThenIsSet {ts=(l, _) :: ts} ls (IsSetCons nIsE isS) | No _ =
    let nIsEInProj = ifProjectRightThenIsNotElem {ts} ls nIsE
        isSProj = ifProjectRightThenIsSet {ts} ls isS
    in IsSetCons nIsEInProj isSProj

max_stars_repo_name: gonzaw/extensible-records

max_issues_repo_name: gonzaw/extensible-records

max_forks_repo_name: gonzaw/extensible-records


text:
import Decidable.Equality

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

%name Vect xs, ys, zs

data Elem : a -> Vect k a -> Type where
     Here : Elem x (x :: xs)
     There : (later : Elem x xs) -> Elem x (y :: xs)

not_in_nil : Elem value [] -> Void
not_in_nil Here impossible
not_in_nil (There _) impossible

not_in_tail : (notThere : Elem value xs -> Void) -> (notHere : (value = x) -> Void) -> Elem value (x :: xs) -> Void
not_in_tail notThere notHere Here = notHere Refl
not_in_tail notThere notHere (There later) = notThere later

isElem : DecEq a => (value : a) -> (xs : Vect n a) -> Dec (Elem value xs)
isElem value [] = No not_in_nil
isElem value (x :: xs) = case decEq value x of
                              Yes Refl => Yes Here
                              No notHere => case isElem value xs of
                                                 Yes prf => Yes (There prf)
                                                 No notThere => No (not_in_tail notThere notHere)


text:
-- ----------------------------------------------------------- [ Clippings.idr ]
-- Module  : Text.Kindle.Clippings
--
-- License : This code is distributed under the MIT license. See the
--           file LICENSE in the root directory for its full text.
-- --------------------------------------------------------------------- [ EOH ]
module Text.Kindle.Clippings

import public Text.Kindle.Clippings.Types
import public Text.Kindle.Clippings.Reader

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

max_stars_repo_name: yurrriq/my-clippings

max_issues_repo_name: yurrriq/my-clippings

max_forks_repo_name: yurrriq/my-clippings


text:
module Capabilities

-- Inspired by http://okmij.org/ftp/Computation/lightweight-static-guarantees.html

interface Sortable (f : Type -> Type) where
  Sorted : (a : Type) -> (a -> a -> Ordering) -> Type

  sortBy : (cmp : a -> a -> Ordering) -> f a -> Sorted a cmp
  mergeBy : (cmp : a -> a -> Ordering) -> Sorted a cmp  -> Sorted a cmp -> Sorted a cmp
  get : Sorted a cmp -> f a

Sortable List where
  Sorted a cmp = List a

  sortBy cmp xs = List.sortBy cmp xs
  mergeBy cmp xs ys = List.mergeBy cmp xs ys
  get xs = xs

example : Sortable f => (cmp : a -> a -> Ordering) -> f a -> f a -> f a
example @{sortable} cmp xs ys =
  let sxs = sortBy cmp xs in
  let sys = sortBy cmp ys in
  let sms = mergeBy @{sortable} cmp sxs sys in
  get sms

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Tk

import public Data.So

%default total
%access public export

infix 6 ==., /=.

interface Equ a where
  (==.) : a -> a -> Bool

  eqRefl  : (x : a) -> So (x ==. x)
  eqSymm  : (x, y : a) -> x ==. y = y ==. x
  eqTrans : (x, y, z : a) -> So (x ==. y) -> So (y ==. z) -> So (x ==. z)

  (/=.) : a -> a -> Bool
  x /=. y = not $ x ==. y

  neqIsNotEq : (x, y : a) -> x ==. y = not (x /=. y)

infix 6 <., <=., >., >=.

interface Equ a => Ordu a where
  (<.) : a -> a -> Bool

  ltArefl : (x : a) -> So (not $ x <. x)
  ltAsymm : (x, y : a) -> So (x <. y) -> So (not $ y <. x)
  ltTrans : (x, y, z : a) -> So (x <. y) -> So (y <. z) -> So (x <. z)

  (<=.) : a -> a -> Bool
  x <=. y = x <. y || x ==. y

  lteIsLtOrE : (x, y : a) -> x <=. y = (x <. y || x ==. y)

  (>.) : a -> a -> Bool
  x >. y = y <. x

  gtInverseOfLt : (x, y : a) -> x <. y = y >. x

  (>=.) : a -> a -> Bool
  x >=. y = y <=. x

  gteIsGtOrE : (x, y : a) -> x >=. y = (x >. y || x ==. y)

max_stars_repo_name: buzden/code-in-lectures

max_issues_repo_name: buzden/code-in-lectures

max_forks_repo_name: buzden/code-in-lectures


text:
{-
205
[]
True
True
36
[(1, 5), (1, 6), (2, 5), (2, 6), (11, 5), (11, 6), (11, 7), (12, 4), (12, 8), (13, 3), (13, 9), (14, 3), (14, 9), (15, 6), (16, 4), (16, 8), (17, 5), (17, 6), (17, 7), (18, 6), (21, 3), (21, 4), (21, 5), (22, 3), (22, 4), (22, 5), (23, 2), (23, 6), (25, 1), (25, 2), (25, 6), (25, 7), (35, 3), (35, 4), (36, 3), (36, 4)]
-}

import Data.HashSet

%default total

data CollidingInt = MkCollidingInt Int

Eq CollidingInt where
  (==) (MkCollidingInt i) (MkCollidingInt j) = i == j

Hash CollidingInt where
  hash (MkCollidingInt i) = assert_total (prim__zextInt_B32 (mod i 39))

Show CollidingInt where
  show (MkCollidingInt i) = show i

Cell : Type
Cell = (Int, Int)

Cells : Type
Cells = HashSet Cell

gosperGun : Cells
gosperGun = fromList
  [(1,5),  (1,6),  (2,5),  (2,6),
   (11,5), (11,6), (11,7), (12,4), (12,8),
   (13,3), (13,9), (14,3), (14,9), (15,6),
   (16,4), (16,8), (17,5), (17,6), (17,7), (18,6),
   (21,3), (21,4), (21,5), (22,3), (22,4), (22,5),
   (23,2), (23,6), (25,1), (25,2), (25,6), (25,7),
   (35,3), (36,3), (35,4), (36,4)]

for : Monad m => HashSet a -> (a -> m b) -> m (List b)
for xs f = foldM (\acc, e => (:: acc) <$> f e) [] xs

main : IO ()
main = do
  let keys = MkCollidingInt <$> [0, 5..1024]
  let set = foldl (flip insert) (the (HashSet CollidingInt) empty) keys
  printLn (length set)
  printLn (filter (not . flip member set) keys)
  printLn (all (flip member set) keys)
  printLn (all (not . flip member set) (MkCollidingInt <$> [1024, 1033..2048]))

  let cells = gosperGun
  printLn (length cells)
  ls <- for cells pure
  printLn (sort ls)

-- Local Variables:
-- idris-load-packages: ("cil")
-- End:

max_stars_repo_name: timjs/iris-clean

max_issues_repo_name: timjs/iris-clean

max_forks_repo_name: timjs/iris-clean


text:
-- vim: set ft=idris sw=2 ts=2:
--
-- fibonacci.idr
-- Calculate Fibonacci numbers in the Idris programming language
--

module Fibonacci

-- Naive implementation
export
fib_naive : Int -> Int
fib_naive 0 = 0
fib_naive 1 = 1
fib_naive n = fib_naive (n - 1) + fib_naive (n - 2)

-- Tail-call friendly version
export
fib : Nat -> Nat
fib n = fib_aux Z (S Z) n where
  fib_aux : Nat -> Nat -> Nat -> Nat
  fib_aux a b Z = a
  fib_aux a b (S n) = fib_aux b (plus a b) n

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
module Data.Nat.Algebra

import Control.Algebra
import Data.Nat

%default total

public export
SemigroupV Nat where
  semigroupOpIsAssociative = plusAssociative

public export
MonoidV Nat where
  monoidNeutralIsNeutralL = plusZeroRightNeutral
  monoidNeutralIsNeutralR = plusZeroLeftNeutral


text:
{- 1 -}

printLonger : IO ()
printLonger = do putStr "First string: "
                 str1 <- getLine
                 putStr "Second string: "
                 str2 <- getLine
                 if length str1 > length str2
                    then putStrLn (show (length str1))
                    else putStrLn (show (length str2))

{- 2 -}

printLonger' : IO ()
printLonger' = putStr "First string: " >>= \_ =>
               getLine >>= \str1 =>
               putStr "Second string: " >>= \_ =>
               getLine >>= \str2 =>
                  if length str1 > length str2
                     then putStrLn (show (length str1))
                     else putStrLn (show (length str2))

max_stars_repo_name: PiotrJander/TypeDD-Samples

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
module Group_property

import Monoid
import Group
import congruence

%access public export

||| Property 1 - Identity is unique for groups
total
Group_property_1 : (grp : Type) -> ((*) : grp -> grp -> grp) ->
                   (IsGroup grp (*)) -> (e1 : grp) -> (e2 :grp) ->
                   (IsIdentity grp (*) e1) -> (IsIdentity grp (*) e2) ->
                   (e1 = e2)

Group_property_1 grp (*) pf_grp e1 e2 pf1 pf2 = trans (sym(snd (pf2 e1))) (fst (pf1 e2))

||| Property 2 - Inverse of an element is unique
total
Group_property_2 : (grp : Type) -> ((*) : grp -> grp -> grp) -> (pfgrp : IsGroup grp (*)) ->
                   (a : grp) -> (b : grp) -> (c : grp) ->
                   (IsInverse grp (*) (fst(snd pfgrp)) a b) ->
                   (IsInverse grp (*) (fst(snd pfgrp)) a c) -> (b = c)

Group_property_2 grp (*) pfgrp a b c pfb pfc = let
                                               pfAss = fst pfgrp
                                               pfid = (fst (snd pfgrp))
                                               in
                                               rewrite (sym (fst ((snd pfid) b))) in
                                              (rewrite (sym (fst pfc)) in
                                              (rewrite (sym (pfAss b a c)) in
                                              (rewrite (snd pfb) in
                                              (rewrite (snd ((snd pfid) c)) in Refl))))

||| Property 3 - b = c implies a*b = a*c
total
Group_property_3 : (grp : Type) -> ((*) : grp -> grp -> grp) -> (pfgrp : IsGroup grp (*)) ->
                   (a : grp) -> (b : grp) -> (c : grp) -> (b = c) -> (a*b = a*c)
Group_property_3 grp (*) pfgrp a b c pfEq = cong pfEq

||| Property 4 - a*b = a*c implies b = c
total
Group_property_4 : (grp : Type) -> ((*) : grp -> grp -> grp) -> (pfgrp : IsGroup grp (*)) ->
                   (a : grp) -> (b : grp) -> (c : grp) -> (a*b = a*c) -> (b = c)
Group_property_4 grp (*) pfgrp a b c pfEq = let pfid = (fst (snd (snd pfgrp)))
                                                a_inv = fst(Inv_with_pf grp (*) pfgrp a)
                                                pf_inv = snd(Inv_with_pf grp (*) pfgrp a)
                                                pfAss = fst pfgrp
                                                in
                                                (rewrite (sym (snd ((snd pfid) b))) in
                                                (rewrite (sym (snd ((snd pfid) c))) in
                                                (rewrite (sym (snd pf_inv)) in
                                                (rewrite (pfAss a_inv a b) in
                                                (rewrite (pfAss a_inv a c) in
                                                (Group_property_3 grp (*) pfgrp a_inv (a*b) (a*c) pfEq))))))

||| Property 5 - b = c implies b*a = c*a
total
Group_property_5 : (grp : Type) -> ((*) : grp -> grp -> grp) -> (pfgrp : IsGroup grp (*)) ->
                   (a : grp) -> (b : grp) -> (c : grp) -> (b = c) -> ( (b*a) = (c*a) )
Group_property_5 grp (*) pfgrp a b c pfEq = (congruence grp grp b c (\x : grp => x*a) pfEq)

||| Property 6 - b*a = c*a implies b = c
total
Group_property_6 : (grp : Type) -> ((*) : grp -> grp -> grp) -> (pfgrp : IsGroup grp (*)) ->
                   (a : grp) -> (b : grp) -> (c : grp) -> (b*a = c*a) -> (b = c)
Group_property_6 grp (*) pfgrp a b c pfEq = let pfid = (fst (snd (snd pfgrp)))
                                                a_inv = fst(Inv_with_pf grp (*) pfgrp a)
                                                pf_inv = snd(Inv_with_pf grp (*) pfgrp a)
                                                pfAss = fst pfgrp
                                                in
                                                (rewrite (sym (fst ((snd pfid) b))) in
                                                (rewrite (sym (fst ((snd pfid) c))) in
                                                (rewrite (sym (fst pf_inv)) in
                                                (rewrite (sym (pfAss b a a_inv)) in
                                                (rewrite (sym (pfAss c a a_inv)) in
                                                (Group_property_5 grp (*) pfgrp a_inv (b*a) (c*a) pfEq))))))

||| Auxilliary proof 1 - Two idenitities mentioned in the definition of the group
||| (one in (fst (snd pfgrp)) another in (fst (snd (snd pfgrp))) are equal.
total
Group_aux_pf_1 : (grp : Type) -> ((*) : grp -> grp -> grp) -> (pfgrp : (IsGroup grp (*))) ->
                 ( (fst (Group_id grp (*) pfgrp)) = (fst (fst (snd (snd pfgrp)))) )

Group_aux_pf_1 grp (*) pfgrp = let
                               pfid1 = (Group_id grp (*) pfgrp)
                               e1 = (fst pfid1)
                               pf1 = (snd pfid1)
                               pfid2 = (fst (snd (snd pfgrp)))
                               e2 = (fst pfid2)
                               pf2 = (snd pfid2)
                               in
                               (Group_property_1 grp (*) pfgrp e1 e2 pf1 pf2)

||| Property 7 - One sided inverse is two sided inverse
total
Group_property_7 : (grp : Type) -> ((*) : grp -> grp -> grp) -> (pfgrp : (IsGroup grp (*))) -> (a : grp)
                   -> (b : grp) -> ( (a*b) = (fst (Group_id grp (*) pfgrp)) )
                   -> (IsInverse grp (*) (Group_id grp (*) pfgrp) a b)

Group_property_7 grp (*) pfgrp a b pfEq = let
                                          pfid1 = Group_id grp (*) pfgrp -- Identity in IdentityExists
                                          pfid2 = fst (snd (snd pfgrp)) -- Identity in InverseExists
                                          e1 = (fst pfid1)
                                          e2 = (fst pfid2)
                                          a_inv = Inv grp (*) pfgrp a
                                          a_inv_pf = snd (Inv_with_pf grp (*) pfgrp a)
                                          a_inv_pf1 = (fst a_inv_pf) -- Proof that a*a_inv = e2
                                          a_inv_pf2 = (snd a_inv_pf) -- Proof that a_inv*a = e2
                                          pfId_eq = Group_aux_pf_1 grp (*) pfgrp -- proof that e1 = e2
                                          pf1 = trans a_inv_pf1 (sym pfId_eq) -- proof that a*a_inv = e1
                                          pf2 = trans pf1 (sym pfEq) -- proof that a*a_inv = a*b
                                          pf3 = Group_property_4 grp (*) pfgrp a a_inv b pf2 -- proof that a_inv b
                                          pf4 = trans a_inv_pf2 (sym pfId_eq) -- proof that a_inv*a = e1
                                          pf5 = Group_property_5 grp (*) pfgrp a a_inv b pf3 -- proof that a_inv*a = b*a
                                          pf6 = trans (sym pf5) pf4
                                          in
                                          (pfEq, pf6)

||| Property 8 - If f : g -> h is group homomorphism then f(inv(a)) = inv(f(a))
total
Group_property_8 : (dom : Type) -> ((*) : dom -> dom -> dom) -> (pfdom : IsGroup dom (*)) ->
                    (cod : Type) -> ((+) : cod -> cod -> cod) -> (pfcod : IsGroup cod (+)) ->
                    (f : dom -> cod) -> (pfhom : (Hom dom (*) pfdom cod (+) pfcod f)) ->
                    (a : dom) -> ( (f (Inv dom (*) pfdom a)) = (Inv cod (+) pfcod (f a)) )

Group_property_8 dom (*) pfdom cod (+) pfcod f pfhom a = let
                                                         pfid1_dom = (fst (snd pfdom))
                                                         e_dom1 = (fst pfid1_dom) -- identity in the IdentityExists
                                                         e_dom1_pf = (snd pfid1_dom) -- proof that e_dom1 is the identity

                                                         pfid2_dom = (fst (snd (snd pfdom)))
                                                         e_dom2 = (fst pfid2_dom) -- identity in the InverseExists
                                                         e_dom2_pf = (snd pfid2_dom) -- prood that it is the identity

                                                         pf_eq_dom_id12 = (Group_property_1 dom (*) pfdom e_dom1 e_dom2
                                                                            e_dom1_pf e_dom2_pf) -- proof that e_dom1 and e_dom2 are equal

                                                         pfid1_cod = (fst (snd pfcod))
                                                         e_cod1 = (fst pfid1_cod) -- identity in the IdentityExists
                                                         e_cod1_pf = (snd pfid1_cod) -- proof that e_cod1 is the identity

                                                         pfid2_cod = (fst (snd (snd pfcod)))
                                                         e_cod2 = (fst pfid2_cod) -- identity in the InverseExists
                                                         e_cod2_pf = (snd pfid2_cod) -- prood that it is the identity

                                                         pf_eq_cod_id12 = (Group_property_1 cod (+) pfcod e_cod1 e_cod2
                                                                            e_cod1_pf e_cod2_pf) -- proof that e_cod1 and e_cod2 are equal

                                                         a_inv_with_pf = snd (snd (snd pfdom)) a -- (Inv_with_pf dom (*) pfdom a)
                                                         a_inv = fst a_inv_with_pf
                                                         b = (f a_inv)
                                                         c = (Inv cod (+) pfcod (f a))

                                                         pf_id_to_id = (fst pfhom)
                                                         pf_res = (snd pfhom)

                                                         --aux_pf1 : ( ( Group_id dom (*) pfdom ) = (fst (snd pfdom)) )
                                                         --aux_pf1 = Refl -- proof that fst (Group_id dom (*) pfdom) = fst (fst (snd pfdom))

                                                         pf1 = (pf_res a a_inv) -- proof that f(a * a_inv) = f a + f a_inv
                                                         pf2 = (fst (snd a_inv_with_pf)) -- proof that a * a_inv = e_dom2
                                                         pf3 = congruence dom cod (a * a_inv) e_dom2 f pf2 -- proof that a * a_inv = e_dom2
                                                         pf4 = trans (sym pf1) pf3 -- proof that f(a * a_inv) = f e_dom2
                                                         pf5 = (Group_property_1 cod (+) pfcod
                                                               (f e_dom1) e_cod1 pf_id_to_id e_cod1_pf) -- proof that f e_dom1 = e_cod1
                                                         pf6 = congruence dom cod e_dom1 e_dom2 f pf_eq_dom_id12-- proof that f e_dom1 = f e_dom2
                                                         pf7 = trans (trans pf4 (sym pf6)) pf5

                                                         in
                                                         (Group_property_2 cod (+) pfcod (f a) b c (pf7,?rhs1) ?rhs2)


text:
module pigeonhole

-- a try to prove pegionhole principle

import Data.Fin
import Data.Vect

%access public export
%default total

same_hole : (n : Nat) -> (m : Nat) -> (Vect n (Fin m)) -> Type
same_hole n m v = (p : (Fin n) ** (q : (Fin n) **
                  ( prf : ((p = q) -> Void) ** ( (index p v) = (index q v)))))

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

||| proof that Fin Z is empty
aux_prf_1 : (Fin Z) -> Void
aux_prf_1 q impossible

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

||| the type of proofs that a particular element is in the vector or not
data There_is : (n : Nat) -> (m : Nat) -> (v : Vect n (Fin m)) -> (a : Fin m) -> Type where
    Yes : (k : (Fin n) ** ( (index k v) = a)) -> (There_is n m v a)
    No : ( (k : (Fin n) ** ( (index k v) = a)) -> Void ) -> (There_is n m v a)

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

||| finds the first index with the given entry, or returns that there is no such index

is_there : (n : Nat) -> (m : Nat) -> (a : Fin m) -> (v : Vect n (Fin m)) ->
           (There_is n m v a)

-- for vectors of length zero this is false clearly.
is_there Z m a v = No contra where
    contra : ( (k : (Fin Z) ** ( (index k v) = a)) -> Void )
    contra = aux_prf_1 . fst

-- for vectors of non zero length it  checks if the first element is a.
is_there (S n) m a (x :: v) = case (decEq x a) of

    -- If yes gives it as the proof
    Yes prf => Yes (FZ ** prf)

    -- if not then recursively checks the remaining part.
    No contra => (case (is_there n m a v) of

                      -- If the element is in the remaining part then gives the proof
                      Yes prf1 => (let
                          k = fst prf1
                          prf2 = snd prf1
                          in
                          ( Yes ( (FS k) ** prf2) ) )

                      -- if the element is not in the remaining part recursively
                      -- constructs the contradiction

                      No not_in_v => (No (\k => case  k of
                                                (FZ ** prf3) => (contra prf3) --
                                                ((FS l) ** prf4) => (not_in_v (l ** prf4 ) ))))

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

swapHelper : (m : Nat) -> (a , b, x : (Fin m)) -> (Dec (x = a)) -> (Dec (x = b)) -> (Fin m)
swapHelper m a b x (Yes pf) _ = b
swapHelper m a b x (No con) (Yes pf) = a
swapHelper m a b x (No con1) (No con2) = x

----------------------------------------------------------------------------------------------------------------
||| swaps two element in a vector
swap : (n : Nat) -> (m : Nat) -> (a, b : Fin m) -> (v : Vect n (Fin m)) -> (Vect n (Fin m))
swap Z _ _ _ _ = []
swap (S n) m a b (x :: v) = (swapHelper m a b x (decEq x a) (decEq x b)) :: (swap n m a b v)
{-
    case (decEq x a) of
        Yes prf => b :: (swap n m a b v)
        No prf => case (decEq x b) of
            Yes prf => a :: (swap n m a b v)
            No prf => x :: (swap n m a b v)
-}

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

simple_case : (n : Nat) -> (v : Vect (S n) (Fin n) ) -> (same_hole (S n) n v)
simple_case Z v = void (aux_prf_1 (Vect.index FZ v ))
simple_case (S n) v = ?rhs


text:
module TTImp.Impossible

import Core.Context
import Core.Env
import Core.Normalise
import Core.TT
import Core.Value

import TTImp.TTImp

import Data.List

%default covering

-- This file contains support for building a guess at the term on the LHS of an
-- 'impossible' case, in order to help build a tree of covered cases for
-- coverage checking. Since the LHS by definition won't be well typed, we are
-- only guessing! But we can still do some type-directed disambiguation of
-- names.
-- Constants (fromInteger/fromString etc) won't be supported, because in general
-- they involve resoling interfaces - they'll just become unmatchable patterns.

match : {auto c : Ref Ctxt Defs} ->
        NF [] -> (Name, Int, ClosedTerm) -> Core Bool
match nty (n, i, rty)
    = do defs <- get Ctxt
         rtynf <- nf defs [] rty
         sameRet nty rtynf
  where
    sameRet : NF [] -> NF [] -> Core Bool
    sameRet _ (NApp _ _ _) = pure True
    sameRet _ (NErased _ _) = pure True
    sameRet (NApp _ _ _) _ = pure True
    sameRet (NErased _ _) _ = pure True
    sameRet (NTCon _ n _ _ _) (NTCon _ n' _ _ _) = pure (n == n')
    sameRet (NPrimVal _ c) (NPrimVal _ c') = pure (c == c')
    sameRet (NType _) (NType _) = pure True
    sameRet nf (NBind fc _ (Pi _ _ _ _) sc)
        = do defs <- get Ctxt
             sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))
             sameRet nf sc'
    sameRet _ _ = pure False

dropNoMatch : {auto c : Ref Ctxt Defs} ->
              Maybe (NF []) -> List (Name, Int, ClosedTerm) ->
              Core (List (Name, Int, ClosedTerm))
dropNoMatch _ [t] = pure [t]
dropNoMatch Nothing ts = pure ts
dropNoMatch (Just nty) ts
    = -- if the return type of a thing in ts doesn't match nty, drop it
      filterM (match nty) ts

nextVar : {auto q : Ref QVar Int} ->
          FC -> Core (Term [])
nextVar fc
    = do i <- get QVar
         put QVar (i + 1)
         pure (Ref fc Bound (MN "imp" i))

mutual
  processArgs : {auto c : Ref Ctxt Defs} ->
                {auto q : Ref QVar Int} ->
                Term [] -> NF [] ->
                (expargs : List RawImp) -> (impargs : List (Maybe Name, RawImp)) ->
                Core ClosedTerm
  processArgs fn (NBind fc x (Pi _ _ Explicit ty) sc) (e :: exp) imp
     = do e' <- mkTerm e (Just ty) [] []
          defs <- get Ctxt
          processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))
                      exp imp
  processArgs fn (NBind fc x (Pi _ _ Implicit ty) sc) exp imp
     = do defs <- get Ctxt
          case useImp [] imp of
            Nothing => do e' <- nextVar fc
                          processArgs (App fc fn e')
                                      !(sc defs (toClosure defaultOpts [] e'))
                                      exp imp
            Just (e, impargs') =>
               do e' <- mkTerm e (Just ty) [] []
                  processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))
                              exp impargs'
    where
      useImp : List (Maybe Name, RawImp) -> List (Maybe Name, RawImp) ->
               Maybe (RawImp, List (Maybe Name, RawImp))
      useImp acc [] = Nothing
      useImp acc ((Just x', xtm) :: rest)
          = if x == x'
               then Just (xtm, reverse acc ++ rest)
               else useImp ((Just x', xtm) :: acc) rest
      useImp acc (ximp :: rest)
          = useImp (ximp :: acc) rest
  processArgs fn (NBind fc x (Pi _ _ AutoImplicit ty) sc) exp imp
     = do defs <- get Ctxt
          case useAutoImp [] imp of
            Nothing => do e' <- nextVar fc
                          processArgs (App fc fn e')
                                      !(sc defs (toClosure defaultOpts [] e'))
                                      exp imp
            Just (e, impargs') =>
               do e' <- mkTerm e (Just ty) [] []
                  processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))
                              exp impargs'
    where
      useAutoImp : List (Maybe Name, RawImp) -> List (Maybe Name, RawImp) ->
                   Maybe (RawImp, List (Maybe Name, RawImp))
      useAutoImp acc [] = Nothing
      useAutoImp acc ((Nothing, xtm) :: rest)
          = Just (xtm, reverse acc ++ rest)
      useAutoImp acc ((Just x', xtm) :: rest)
          = if x == x'
               then Just (xtm, reverse acc ++ rest)
               else useAutoImp ((Just x', xtm) :: acc) rest
      useAutoImp acc (ximp :: rest)
          = useAutoImp (ximp :: acc) rest
  processArgs fn ty [] [] = pure fn
  processArgs fn ty exp imp
     = throw (GenericMsg (getLoc fn)
                ("Badly formed impossible clause "
                     ++ show (fn, exp, imp)))

  buildApp : {auto c : Ref Ctxt Defs} ->
             {auto q : Ref QVar Int} ->
             FC -> Name -> Maybe (NF []) ->
             (expargs : List RawImp) -> (impargs : List (Maybe Name, RawImp)) ->
             Core ClosedTerm
  buildApp fc n mty exp imp
      = do defs <- get Ctxt
           fi <- fromIntegerName
           si <- fromStringName
           ci <- fromCharName
           when (Just n `elem` [fi, si,ci]) $
               throw (InternalError "Can't deal with constants here yet")

           tys <- lookupTyName n (gamma defs)
           [(n', _, ty)] <- dropNoMatch mty tys
              | [] => throw (UndefinedName fc n)
              | ts => throw (AmbiguousName fc (map fst ts))
           tynf <- nf defs [] ty
           processArgs (Ref fc Func n') tynf exp imp

  mkTerm : {auto c : Ref Ctxt Defs} ->
           {auto q : Ref QVar Int} ->
           RawImp -> Maybe (NF []) ->
           (expargs : List RawImp) -> (impargs : List (Maybe Name, RawImp)) ->
           Core ClosedTerm
  mkTerm (IVar fc n) mty exp imp
     = buildApp fc n mty exp imp
  mkTerm (IApp fc fn arg) mty exp imp
     = mkTerm fn mty (arg :: exp) imp
  mkTerm (IImplicitApp fc fn nm arg) mty exp imp
     = mkTerm fn mty exp ((nm, arg) :: imp)
  mkTerm (IPrimVal fc c) _ _ _ = pure (PrimVal fc c)
  mkTerm tm _ _ _ = nextVar (getFC tm)

-- Given an LHS that is declared 'impossible', build a term to match from,
-- so that when we build the case tree for checking coverage, we take into
-- account the impossible clauses
export
getImpossibleTerm : {vars : _} ->
                    {auto c : Ref Ctxt Defs} ->
                    Env Term vars -> NestedNames vars -> RawImp -> Core ClosedTerm
getImpossibleTerm env nest tm
    = do q <- newRef QVar (the Int 0)
         mkTerm (applyEnv tm) Nothing [] []
  where
    addEnv : {vars : _} ->
             FC -> Env Term vars -> List RawImp
    addEnv fc [] = []
    addEnv fc (b :: env) =
       if isLet b
          then addEnv fc env
          else Implicit fc False :: addEnv fc env

    expandNest : RawImp -> RawImp
    expandNest (IVar fc n)
        = case lookup n (names nest) of
               Just (Just n', _, _) => IVar fc n'
               _ => IVar fc n
    expandNest tm = tm

    -- Need to apply the function to the surrounding environment, and update
    -- the name to the proper one from the nested names map
    applyEnv : RawImp -> RawImp
    applyEnv (IApp fc fn arg) = IApp fc (applyEnv fn) arg
    applyEnv (IImplicitApp fc fn n arg)
        = IImplicitApp fc (applyEnv fn) n arg
    applyEnv tm = apply (expandNest tm) (addEnv (getFC tm) env)


text:
data Foo : Type where
  FooBase : Foo
  (@) : Foo -> Foo -> Foo


text:
module R

-- Definition of the logical relation 'R'
-- that is central to proving normalization
-- for the simply-typed lambda calculus
-- (with primitive recursion).

import Determinism
import PnP
import Step
import Term
import Typing

%default total
%access export

---------------------------
-- Begin: PREDICATE 'HALTS'

-- The predicate 'Halts' defines what it
-- means that the evaluation of a term 'e'
-- under 'Step' terminates - namely that
-- the term 'e' must evaluate to a value:
public export
data Halts : Term -> Type where
  H : (e : Term) ->
      (e' : Term ** (Value e', TransStep e e'))
      -> Halts e

-- For terms 'e1' and 'e2', if one of them steps
-- to the other, then either both satisfy 'Halts'
-- or neither term does; in formulae:
--
--   Step e1 e2 => (Halts e1 <=> Halts e2)
--
-- The following two lemmas establish this equivalence,
-- given 'Step e1 e2'.
-- The next two lemmas then extend this equivalence to
-- the 'TransStep' relation.

stepPreservesHalts_1 : (e : Term) -> (e' : Term) ->
                       Step e e' -> Halts e -> Halts e'
stepPreservesHalts_1 e e' step (H e ev) = case ev of
  (x ** (vx, tstx)) => case tstx of
                            (TStRefl e) => absurd $ valueIrreducible e vx step
                            (TStTrans st tst) => case stepDeterministic step st of
                                                      Refl => H e' (x ** (vx, tst))

stepPreservesHalts_2 : (e : Term) -> (e' : Term) ->
                       Step e e' -> Halts e' -> Halts e
stepPreservesHalts_2 e e' step (H e' ev) = case ev of
  (x ** (vx, tstx)) => H e (x ** (vx, TStTrans step tstx))

transStepPreservesHalts_1 : (e : Term) -> (e' : Term) ->
                          TransStep e e' -> Halts e -> Halts e'
transStepPreservesHalts_1 e e  (TStRefl e)       h = h
transStepPreservesHalts_1 e e' (TStTrans st tst) h =
  let h' = stepPreservesHalts_1 _ _ st h
  in transStepPreservesHalts_1 _ _ tst h'

transStepPreservesHalts_2 : (e : Term) -> (e' : Term) ->
                          TransStep e e' -> Halts e' -> Halts e
transStepPreservesHalts_2 e e (TStRefl e)        h = h
transStepPreservesHalts_2 e e' (TStTrans st tst) h =
  let h' = transStepPreservesHalts_2 _ _ tst h
  in stepPreservesHalts_2 _ _ st h'

haltsAbs : (e : Term) -> Halts (TAbs e)
haltsAbs e = H (TAbs e) (TAbs e ** (VAbs, TStRefl (TAbs e)))

haltsZero : Halts TZero
haltsZero = H TZero (TZero ** (VZero, TStRefl TZero))

-- End: PREDICATE 'HALTS'
-------------------------

--------------------------------------
-- Begin: (UNARY) LOGICAL RELATION 'R'

mutual
  public export
  r : (t : Ty) -> (e : Term) -> Type
  r TyNat       e = (Typing [] e TyNat,    Halts e)
  r (TyFun s t) e = (Typing [] e (s:->:t), Halts e, rFun s t e)

  public export
  rFun : (s : Ty) -> (t : Ty) -> (e : Term) -> Type
  rFun s t e = (y : Term) -> r s y -> r t (TApp e y)

rTyping : (e : Term) -> r t e -> Typing [] e t
rTyping {t = TyNat}         _ r = fst r
rTyping {t = (TyFun t1 t2)} _ r = fst r

rHalts : r t e -> Halts e
rHalts {t = TyNat}         r = snd r
rHalts {t = (TyFun t1 t2)} r = fst $ snd r

rHalts' : r t e -> (e' : Term ** (Value e', TransStep e e'))
rHalts' r = case rHalts r of
                 (H _ ev) => ev

rImplication : r (s :->: t) e -> rFun s t e
rImplication r =  snd $ snd r

-- Forward stepping preserves the predicate 'R':
mutual
  stepPreservesR_1 : (t : Ty) ->
                     (e  : Term) -> (e' : Term) ->
                     Step e e' -> r t e -> r t e'
  stepPreservesR_1 TyNat       e e' st (ty, h) =
    let ty' = preservation e ty st
        h'  = stepPreservesHalts_1 e e' st h
    in (ty', h')
  stepPreservesR_1 (TyFun s t) e e' st (ty, h, imp) =
    let ty'  = preservation e ty st
        h'   = stepPreservesHalts_1 e e' st h
        imp' = stepPreservesR_1_Fun s t e e' st imp
    in (ty', h', imp')

  stepPreservesR_1_Fun : (s : Ty) -> (t : Ty) ->
                         (e  : Term) -> (e' : Term) ->
                         Step e e' -> rFun s t e -> rFun s t e'
  stepPreservesR_1_Fun s t e e' st imp y ry =
    let r'  = imp y ry
        st' = StApp1 st
    in stepPreservesR_1 t _ _ st' r'

-- Backward stepping preserves the predicate 'R',
-- but an explicit typing of the expression 'e'
-- (i.e. the expression that steps) must be provided:
-- (For the forward direction, an explicit typing
-- argument is not required thanks to 'preservation'.)
mutual
  stepPreservesR_2 : (t : Ty) ->
                     (e  : Term) -> (Typing [] e t) ->
                     (e' : Term) ->
                     Step e e' -> r t e' -> r t e
  stepPreservesR_2 TyNat       e ty e' st (_, h') =
    let h = stepPreservesHalts_2 e e' st h'
    in (ty, h)
  stepPreservesR_2 (TyFun s t) e ty e' st (_, h', imp') =
    let h   = stepPreservesHalts_2 e e' st h'
        imp = stepPreservesR_2_Fun s t e ty e' st imp'
    in (ty, h, imp)

  stepPreservesR_2_Fun : (s : Ty) -> (t : Ty) ->
                         (e  : Term) -> (Typing [] e (s :->: t)) ->
                         (e' : Term) ->
                         Step e e' -> rFun s t e' -> rFun s t e
  stepPreservesR_2_Fun s t e ty e' st imp' y ry =
    let r   = imp' y ry
        st' = StApp1 st
        tyy = rTyping y ry
        tya = TyApp ty tyy
    in stepPreservesR_2 t _ tya _ st' r

transStepPreservesR_1 : (t : Ty) ->
                        (e  : Term) -> (e' : Term) ->
                        TransStep e e' -> r t e -> r t e'
transStepPreservesR_1 t e _  (TStRefl _)       re = re
transStepPreservesR_1 t e e' (TStTrans st tst) re = let r' = stepPreservesR_1 t _ _ st re
                                                    in transStepPreservesR_1 t _ _ tst r'

transStepPreservesR_2 : (t : Ty) ->
                        (e  : Term) -> (Typing [] e t) ->
                        (e' : Term) ->
                        TransStep e e' -> r t e' -> r t e
transStepPreservesR_2 t e ty _  (TStRefl _)       re' = re'
transStepPreservesR_2 t e ty e' (TStTrans st tst) re' =
  let ty1 = preservation e ty st
      r'  = transStepPreservesR_2 t _ ty1 _ tst re'
  in stepPreservesR_2 t _ ty _ st r'

rZero : r TyNat TZero
rZero = (TyZero, haltsZero)

-- End: (UNARY) LOGICAL RELATION 'R'
------------------------------------

-----------------------------------------
-- Begin: INVERT PREDICATE 'R' OF 'TSucc'

transStepSuccInjective : TransStep (TSucc e1) (TSucc e2) -> TransStep e1 e2
transStepSuccInjective (TStRefl (TSucc e1)) = TStRefl _
transStepSuccInjective (TStTrans (StSucc st) tst) =
  let ih = transStepSuccInjective tst
  in TStTrans st ih

transStepSuccSucc : TransStep (TSucc e1) e2 -> (e2' : Term ** e2 = TSucc e2')
transStepSuccSucc (TStRefl (TSucc e1)) = (e1 ** Refl)
transStepSuccSucc (TStTrans (StSucc st) tst) = transStepSuccSucc tst

succHaltsHalts : Typing ctx (TSucc e) TyNat -> Halts (TSucc e) -> Halts e
succHaltsHalts (TySucc ty) (H (TSucc e) (_ ** (v, tst))) =
  let ty' = transPreservation (TSucc e) (TySucc ty) tst
  in case canonicalNat _ ty' v of
          (Left Refl) => let (_ ** eq) = transStepSuccSucc tst
                         in case eq of Refl impossible
          (Right (_ ** (v', Refl))) => let tst' = transStepSuccInjective tst
                                       in H _ (_ ** (v', tst'))

succRR : r TyNat (TSucc e) -> r TyNat e
succRR re = let ty = rTyping _ re
                h  = rHalts re
            in case ty of
                    (TySucc ty') => (ty', succHaltsHalts ty h)

-- End: INVERT PREDICATE 'R' OF 'TSucc'
---------------------------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
module Main

import Effects
import Effect.File
import Effect.State
import Effect.StdIO
import Control.IOExcept

FileIO : Type -> Type -> Type
FileIO st t
  = Eff t [FILE_IO st, STDIO, STATE Int]

readFile : FileIO (OpenFile Read) (List String)
readFile = readAcc [] where
    readAcc : List String -> FileIO (OpenFile Read) (List String)
    readAcc acc = do e <- eof
                     if (not e)
                        then do str <- readLine
                                put (!get + 1)
                                readAcc (str :: acc)
                        else return (reverse acc)

dumpFile : String -> FileIO () ()
dumpFile fname = do ok <- open fname Read
                    staticEff $ -- toEff [FILE_IO _, _, _] $
                     case ok of
                       True => do num <- get
                                  putStrLn (show !get ++ "\n" ++
                                            show !readFile)
                                  close
                       False => putStrLn ("Error!")
                    putStrLn "DONE!"
                    return ()

main : IO ()
main = run $ dumpFile "testfile"

max_stars_repo_name: idris-hackers/idris-demos

max_issues_repo_name: idris-hackers/idris-demos

max_forks_repo_name: idris-hackers/idris-demos


text:
module BioFasta.Common

import Data.List
import Data.Maybe
import Data.Strings
import BioCore.Sequence

||| Splits a character list into a list of newline separated character lists.
|||
||| ```idris example
||| lines' (unpack "\rA BC\nD\r\nE\n")
||| ```
public export
lines' : List Char -> List (List Char)
lines' [] = []
lines' s  = case break isNL s of
              (l, s') => l :: case s' of
                                []       => []
                                _ :: s'' => lines' (assert_smaller s s'')

||| The groupBy function returns a list of lists such that the concatenation
||| of the list is equal to the argument, and each sublist contains only
||| elements that are equal according to the user-supplied predicate.
|||
||| ```idris example
||| groupBy (==) [1, 1, 2, 3, 3]
||| ```
|||
public export
groupBy : (a -> a -> Bool) -> List a -> List (List a)
groupBy _ [] = []
groupBy p' (x'::xs') =
    let (ys',zs') = go p' x' xs'
    in (x' :: ys') :: zs'
    where
        go : (a -> a -> Bool) -> a -> List a -> (List a, List (List a))
        go p z (x::xs) =
            let (ys,zs) = go p x xs
            in case p z x of
                True => (x :: ys, zs)
                False => ([], (x :: ys) :: zs)
        go _ _ [] = ([], [])


text:
module Erlang.Conversion

import Erlang.Types

%default total

-- UNSAFE CONVERSIONS

-- IsErlType a -> IsErlType b

||| Cast a value from one type to another. (Caution: Wrong usage of this
||| function may result in run-time errors.)
|||
||| Both the target type and the type of the given value must be a member of `IsErlType`.
|||
||| `erlUnsafeCast` should only be used when you are sure the casting is safe.
||| In the common case, you should probably use the functions from `Erlang.Decode`.
export %inline
erlUnsafeCast : IsErlType from => (0 to : Type) -> IsErlType to => from -> to
erlUnsafeCast _ = believe_me

-- CONVERSION TO `ErlTerm`

||| Convert a value to an untyped Erlang value (`ErlTerm`).
public export
interface ToErlTerm a where
  toErlTerm : a -> ErlTerm

-- Values that conform to `IsErlType` are already proper Erlang values.
export %inline
IsErlType a => ToErlTerm a where
  toErlTerm = believe_me

export
ToErlTerm Bool where
  toErlTerm True = toErlTerm (MkAtom "true")
  toErlTerm False = toErlTerm (MkAtom "false")

-- CASTS

-- Bool -> ErlAtom

export
Cast Bool ErlAtom where
  cast True = MkAtom "true"
  cast False = MkAtom "false"

-- ErlNil/ErlCons -> List

export
Cast ErlNil (List a) where
  cast [] = []

export
Cast b (List a) => Cast (ErlCons a b) (List a) where
  cast (x :: y) = x :: cast y

-- ErlNil/ErlCons -> ErlList

export
Cast ErlNil (ErlList []) where
  cast [] = []

export
Cast b (ErlList bs) => Cast (ErlCons a b) (ErlList (a :: bs)) where
  cast (x :: y) = x :: cast y

-- ErlList -> List

export
Cast (ErlList []) (List a) where
  cast [] = []

export
Cast (ErlList as) (List a) => Cast (ErlList (a :: as)) (List a) where
  cast (x :: xs) = x :: cast xs

-- ErlList -> ErlNil/ErlCons

export
Cast (ErlList []) ErlNil where
  cast [] = []

export
Cast (ErlList [a]) (ErlCons a ErlNil) where
  cast (x :: xs) = x :: cast xs

export
Cast (ErlList as) (ErlCons b c) => Cast (ErlList (a :: as)) (ErlCons a (ErlCons b c)) where
  cast (x :: xs) = x :: cast xs

-- List -> ErlNil/ErlCons

||| Helper functions for `listToErlCons`.
export
0 ListToErlCons : List a -> Type
ListToErlCons [] = ErlNil
ListToErlCons (_ :: xs) = ErlCons a (ListToErlCons xs)

||| Convert `List` to `ErlNil` and `ErlCons`.
export
listToErlCons : (xs : List a) -> ListToErlCons xs
listToErlCons [] = []
listToErlCons (x :: xs) = x :: listToErlCons xs

-- List -> ErlList

||| Helper function for `listToErlList`.
export
0 ListToTypes : List a -> List Type
ListToTypes [] = []
ListToTypes (_ :: xs) = a :: ListToTypes xs

||| Convert `List` to `ErlList`.
export
listToErlList : (xs : List a) -> ErlList (ListToTypes xs)
listToErlList [] = []
listToErlList (x :: xs) = x :: listToErlList xs


text:
record Is3 (n : Nat) where
  constructor MkThree
  {auto prf : n === 3}

three : Is3 3
three = MkThree


text:
import Data.Vect
import Control.Monad.State
import Control.Monad.Identity

VThing : Type
VThing = {n : Nat} -> Vect n Int -> Int

foo : Int -> Vect m Int -> ({n : Nat} -> Vect n Int -> Int) -> Int
foo x xs f = x + f xs

foo' : Int -> Vect m Int -> VThing -> Int
foo' x xs f = x + f xs

bar : Int -> VThing
bar y [] = 0
bar y (x :: xs) = y + x + bar y xs

vsum : Vect n Int -> Int
vsum [] = 0
vsum (x :: xs) = x + vsum xs

testfoo : Vect n Int -> Int
testfoo xs = foo 42 xs (\ xs => vsum xs)

testfoo2 : Vect n Int -> Int
testfoo2 xs = foo' 42 xs vsum

testfoo3 : Vect n Int -> Int
testfoo3 xs = foo 42 xs (bar 10)

AnyST : Type -> Type -> Type
AnyST s a = {m : _} -> Monad m => StateT s m a

-- foost : AnyST Int ()
foost : StateT Int Maybe ()
foost = do x <- get
           put x

wibble : StateT Int Maybe ()
wibble = foost

appShow : Show a => ({b : _} -> Show b => b -> String) -> a -> String
appShow s x = s x

myshow : Show a => a -> String
myshow = show

baz : Int -> String
baz x = appShow myshow x ++ appShow show x

tupleId : ({a : _} -> a -> a) -> (a, b) -> (a, b)
tupleId f (a, b) = (f a, f b)

AppendType : Type
AppendType = {a, n, m : _} -> Vect n a -> Vect m a -> Vect (n + m) a

append : AppendType
append [] ys = ys
append (x :: xs) ys = x :: append xs ys

main : IO ()
main = do putStrLn (baz 42)
          printLn (append [1,2,3] [4,5,6])

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
{-
before thread
in thread
after thread
True
False
>> True
>> False
-}
module Main

import CIL.FFI

Thread : Type
Thread = corlib "System.Threading.Thread"

%inline
invokeThread : String -> Thread -> CIL_IO ()
invokeThread fn = invoke (CILInstance fn)
                         (Thread -> CIL_IO ())

Start : Thread -> CIL_IO ()
Start = invokeThread "Start"

Join : Thread -> CIL_IO ()
Join = invokeThread "Join"

ThreadStartTy : CILTy
ThreadStartTy = corlibTy "System.Threading.ThreadStart"

ThreadStart : Type
ThreadStart = CilFn ThreadStartTy (CIL_IO ())

%inline
BoolToStringTy : CILTy
BoolToStringTy = CILTyGen (corlibTy "System.Func") [CILTyBool, CILTyStr]

BoolToString : Type
BoolToString = CilFn BoolToStringTy (Bool -> String)

%inline
Invoke : BoolToString -> Bool -> CIL_IO String
Invoke = invoke (CILInstanceCustom "Invoke" [CILTyGenParam "0"] (CILTyGenParam "1"))
                (BoolToString -> Bool -> CIL_IO String)

boolToString : Bool -> String
boolToString = show

testBoolToString : BoolToString -> CIL_IO ()
testBoolToString bts =
  for_ [True, False] $ \b =>
    Invoke bts b >>= putStrLn

threadMain : CIL_IO ()
threadMain = putStrLn "in thread"

main : CIL_IO ()
main = do
  -- And now for something completely different... Threads!
  ts <- delegate ThreadStartTy (CIL_IO ()) threadMain
  t <- new (ThreadStart -> CIL_IO Thread) ts
  putStrLn "before thread"
  Start t; Join t
  putStrLn "after thread"

  bts <- delegate BoolToStringTy (Bool -> String) boolToString
  testBoolToString bts

  --        new String ('>', 2)
  prefix <- new (Char -> Int -> CIL_IO String) '>' 2 -- using FFI to avoid inlining into the lambda below
  let lambda = \b => prefix ++ " " ++ show b
  bts <- delegate BoolToStringTy (Bool -> String) lambda
  testBoolToString bts

max_stars_repo_name: Despair/idris-cil

max_issues_repo_name: Despair/idris-cil

max_forks_repo_name: Despair/idris-cil


text:
module Salo.Language.Lexer

import Text.Lexer
import Data.List
import Data.String

||| All possible tokens.
public export
data Token
  = Arrow
  | Colon
  | Equals
  | Bar

  | Space
  | Comment

  | DocComment String

  | Keyword String
  | Ident String
  | StringLit String

public export
Show Token where
  show Arrow          = "->"
  show Colon          = ":"
  show Equals         = "="
  show Bar            = "|"

  show Space          = "(space)"
  show Comment        = "(comment)"

  show (DocComment s) = "doc comment: " ++ show s

  show (Keyword s)    = "keyword "      ++ show s
  show (Ident s)      = "identifier "   ++ show s
  show (StringLit s)  = show s

public export
Eq Token where
  (==) x y = case (x, y) of
    (Arrow, Arrow)     => True
    (Colon, Colon)     => True
    (Equals, Equals)   => True
    (Bar, Bar)         => True

    (Space,   Space)   => True
    (Comment, Comment) => True

    (DocComment s, DocComment s') => s == s'

    (Keyword s,   Keyword s')   => s == s'
    (Ident s,     Ident s')     => s == s'
    (StringLit s, StringLit s') => s == s'

    _                  => False

||| All possible errors that the parser can encounter.
public export
data ParseError : Type where
  --            Line,  Col,   Rest
  LexError    : Int -> Int -> String -> ParseError
  --            Line,  Col,   Message,  Rest
  SyntaxError : Int -> Int -> String -> List (TokenData Token) -> ParseError

public export
Show ParseError where
  show (LexError l c msg)       = "Lex error at " ++ show (l, c) ++ ": " ++ msg
  show (SyntaxError l c msg ts) = "Parse error at " ++ show (l, c) ++ ": " ++ msg ++ "; next up: " ++ show [tok t | t <- take 8 ts]

||| Lexes a given string.
|||
|||  @ src String to parse.
export
lex : String -> Either ParseError (List (TokenData Token))
lex src = case lex tokens src of
            (ts, (_, _, "")) => Right $ filter notSpace ts
            (_, (l, c, rest)) => Left $ LexError l c rest
            _ => Left $ LexError 1 1 ""
          where
            notSpace : TokenData Token -> Bool
            notSpace td = case tok td of
              Space   => False
              Comment => False
              _       => True

            ident : Lexer
            ident = some $ pred (\x => isAlpha x || isDigit x || x == '_' || x == '\'')

            parseString : String -> Token
            parseString s = StringLit $ assert_total (strTail (reverse (strTail (reverse s))))

            ||| Given a string, check if it's a keyword from the list of
            ||| keywords, or an identifier.
            kwdOrIdent : String -> Token
            kwdOrIdent s =
              if s `elem` keywords
                then Keyword s
                else Ident   s
              where
                keywords : List String
                keywords =
                  [ "Type"
                  , "data"
                  ]

            mkDocComment : String -> Token
            mkDocComment s = DocComment s

            tokens : TokenMap Token
            tokens =
              [ (exact "->",             const Arrow)
              , (is ':',                 const Colon)
              , (is '=',                 const Equals)
              , (is '|',                 const Bar)

              , (space,                                    const Space)
              , (lineComment (exact "--"),                 const Comment)
              , (blockComment (exact "{--") (exact "--}"), const Comment)

              , (lineComment (exact "||"),                 mkDocComment)
              , (blockComment (exact "{||") (exact "||}"), mkDocComment)

              , (ident,                     kwdOrIdent)
              , (stringLit,                 parseString)
            ]

-- TODO: There are no assertions in these tests :)
namespace Test
  namespace Examples
    export
    exampleProg : String
    exampleProg = #"""
      -- This is a comment.

      || This is a doc comment
      myvalue : String
      myvalue = "This is an immutable value, myvalue, with the type of String."

      myfunction : String -> String
      myfunction "" = "This is a function that pattern matches on its first argument."
      myfunction _  = "If the first argument is a blank String, it evaluates to ^"
      -- Else, `myfunction` evaluates to ^.

      -- This is a type declaration. Here, we declare that the type `MyType` as EITHER
      -- `True` or `False`.
      type MyType = True | False

      -- This is a dependent type declaration. Here, we declare `MyDependentType` to
      -- be a type that depends on two Nats.
      type MyDependentType = Nat -> Nat

      {--
        Here's a block comment.

        We can have quite long block comments!
      --}

      {||
        Here's a block doc comment.

        We can have quite long block doc comments, too!
      ||}

      -- Functions can also be polymorphic
      f : a -> a
      f x = x

      -- `f` can now be called on anything.

      -- In this sample file, we didn't cover imports.
    """#

    export
    docComments : String
    docComments = #"""
      {||
        AAA!
      ||}
    """#

  LexerType : Type
  LexerType = Either ParseError (List (TokenData Token))

  lexExampleProg : LexerType
  lexExampleProg = Salo.Language.Lexer.lex exampleProg

  lexDocComments : LexerType
  lexDocComments = Salo.Language.Lexer.lex docComments

  testHarness : LexerType -> IO ()
  testHarness t = case t of
            Left err   => putStrLn $ "  -> Error: " ++ (show err)
            Right toks => putStrLn $ "  -> Success"

  export
  test : IO ()
  test = do putStrLn "Lexer:"
            testHarness lexExampleProg
            testHarness lexDocComments

max_stars_repo_name: semissioncontrol/semcos

max_issues_repo_name: semissioncontrol/semcos

max_forks_repo_name: semissioncontrol/semcos


text:
-- 3.3.3 examples

import Data.Vect

createEmpties : {n: _} -> Vect n (Vect 0 a)
createEmpties = replicate _ []

transposeHelper : (x : Vect n a)
               -> (xsTrans : Vect n (Vect k a))
               -> Vect n (Vect (S k) a)
transposeHelper [] [] = []
transposeHelper (x :: xs) (y :: ys) = (x :: y) :: transposeHelper xs ys

transposeMat : {n: _} -> Vect m (Vect n a) -> Vect n (Vect m a)
transposeMat [] = createEmpties
transposeMat (x :: xs) = let xsTrans = transposeMat xs in transposeHelper x xsTrans

transposeMat2 : {n: _} -> Vect m (Vect n a) -> Vect n (Vect m a)
transposeMat2 [] = createEmpties
transposeMat2 (x :: xs) = let xsTrans = transposeMat2 xs in zipWith (::) x xsTrans

{-
Addition recursion

input: addMatrix [[1,2], [3,4]] [[5,6], [7,8]]
expected: [[6, 8], [10, 12]]

addMatrix (x :: xs) (y :: ys) = ([1,2] :: [[3,4]])  ([5,6] :: [[7,8]])
    addMatrix xs ys = [[3,4]] [[7,8]]
        addMatrix (x :: xs) (y :: ys) = ([3,4] :: [])  ([7,8] :: [])
            addMatrix [] ys = []
        sumMatrix: zipWith (+) [3,4] [7,8] :: [] ==> [[10,12]]
    sumMatrix: zipWith (+) [1,2] [3,4] :: [[10,12]] ==> [[6,8], [10,12]]
 -}
addMatrix : Num a => Vect n (Vect m a)
                  -> Vect n (Vect m a)
                  -> Vect n (Vect m a)
addMatrix [] ys = ys
addMatrix (x :: xs) (y :: ys) = let sumMatrix = addMatrix xs ys in zipWith (+) x y :: sumMatrix

multVect : {p: _} -> Num a
        => Vect m a
        -> Vect p (Vect m a)
        -> Vect p a
multVect _ [] = []
multVect xs ys = map (\y => sum (zipWith (*) xs y)) ys

dotProduct : Num a => {n: _} -> {p: _} -> Vect n (Vect m a)
         -> Vect p (Vect m a)
         -> Vect n (Vect p a)
dotProduct [] _ = []
dotProduct _ [] = createEmpties
dotProduct (x :: xs) ys = let productMat =
                             dotProduct xs ys
                             in multVect x ys :: productMat

{-
Transposes right matrix:
input: multMatrix [[1,2], [3,4], [5,6]] [[7,8,9,10], [11,12,13,14]]

transposeMat2 [[7,8,9,10], [11,12,13,14]] ==> [[7, 11], [8, 12], [9, 13], [10, 14]]

then performs matrix dot product
 -}
multMatrix : Num a => {n: _} -> {p: _} -> Vect n (Vect m a)
                             -> Vect m (Vect p a)
                             -> Vect n (Vect p a)
multMatrix xs ys = dotProduct xs (transposeMat2 ys)


text:
data Shape = ||| A triangle with a base and a height
             Triangle Double Double
           | ||| A square with base and a height
             Rectangle Double Double
           | ||| A circle with it's radius
             Circle Double
%name Shape shape, shape1, shape2

area : Shape -> Double
area (Triangle base height) = 0.5 * base * height
area (Rectangle base height) = base * height
area (Circle radius) = pi * radius * radius

data Picture = Primitive Shape
             | Combine Picture Picture
             | Rotate Double Picture
             | Translate Double Double Picture
%name Picture pic, pic1, pic2

testPicture : Picture
testPicture = Combine (Translate 5  5  (Primitive (Rectangle 20 10)))
            $ Combine (Translate 35 5  (Primitive (Circle    5    )))
                      (Translate 15 25 (Primitive (Triangle  10 10)))

pictureArea: Picture -> Double
pictureArea (Primitive shape) = area shape
pictureArea (Combine pic pic1) = pictureArea pic + (pictureArea pic1)
pictureArea (Rotate _ pic) = pictureArea pic
pictureArea (Translate _ _ pic) = pictureArea pic

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

insert : Ord a => a -> Tree a -> Tree a
insert a Empty = Node Empty a Empty
insert a node@(Node left val right) =
  case compare a val of
      LT => Node (insert a left) val right
      EQ => node
      GT => Node left val (insert a right)

listToTree : Ord a => List a -> Tree a
listToTree = foldr insert Empty

treeToList : Tree a -> List a
treeToList Empty = []
treeToList (Node left val right) = treeToList left ++ [val] ++ (treeToList right)

data Expr = Val Int
          | Sum Expr Expr
          | Sub Expr Expr
          | Mul Expr Expr

eval : Expr -> Int
eval (Val x) = x
eval (Sum x y) = eval x + (eval y)
eval (Sub x y) = eval x - (eval y)
eval (Mul x y) = eval x * (eval y)

liftA2' : Applicative f => (a -> b -> c) -> f a -> f b -> f c
liftA2' f x y = map f x <*> y

maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe Nothing Nothing = Nothing
maxMaybe Nothing (Just x) = Just x
maxMaybe (Just x) Nothing = Just x
maxMaybe (Just x) (Just y) = Just $ max x y

testPic1 : Picture
testPic1 = Combine (Primitive (Triangle 2 3))
                   (Primitive (Triangle 2 4))

testPic2 : Picture
testPic2 = Combine (Primitive (Rectangle 1 3))
                   (Primitive (Circle 4))

biggestTriangle : Picture -> Maybe Double
biggestTriangle (Primitive triangle@(Triangle x y)) = Just $ area triangle
biggestTriangle (Primitive _) = Nothing
biggestTriangle (Combine pic pic1) = maxMaybe (biggestTriangle pic) (biggestTriangle pic1)
biggestTriangle (Rotate _ pic) = biggestTriangle pic
biggestTriangle (Translate _ _ pic) = biggestTriangle pic


text:
module Data.Scientific

import Data.Precision

import Data.Fin
import Data.List
import Data.Vect

public export
data Sign = Positive
          | Negative

export
Eq Sign where
  Positive == Positive = True
  Negative == Negative = True
  _ == _ = False

export
Ord Sign where
  compare Positive Positive = EQ
  compare Positive Negative = GT
  compare Negative Positive = LT
  compare Negative Negative = EQ

public export
data Scientific : Type where
  SciZ : Scientific
  Sci : Sign -> Precision 10 n -> Scientific

export
Eq Scientific where
  SciZ == SciZ = True
  Sci sign prec == Sci sign' prec' = sign == sign' && eqPrecs prec prec'
  _ == _ = False

export
Ord Scientific where
  compare SciZ SciZ = EQ
  compare SciZ (Sci sign prec) =
    case sign of
         Positive => LT
         Negative => GT
  compare (Sci sign prec) SciZ =
    case sign of
         Positive => GT
         Negative => LT
  compare (Sci sign prec) (Sci sign' prec') =
    case compare sign sign' of
         LT => LT
         EQ => case sign of
                    Positive => comparePrecs prec prec'
                    Negative => comparePrecs prec' prec
         GT => GT

-- TODO: don't use Show?
export
Show Scientific where
  show SciZ = "0"
  show (Sci sign prec) = (++ show prec) $ case sign of
                                               Positive => ""
                                               Negative => "-"


text:
namespace MyDo
  export
  (>>=) : a -> (a -> IO b) -> IO b
  (>>=) val k = k val

foo : IO ()
foo = MyDo.do
         x <- "Silly"
         putStrLn x

namespace A
  namespace B
    export
    (>>=) : Nat -> (() -> Nat) -> Nat
    (>>=) x fy = x + (fy ())

test : Nat
test = B.A.do
         5
         6
         7

test2 : Nat
test2 = A.B.do
         5
         6
         7


text:
data Fin : Nat -> Type where
     FZ : Fin (S k)
     FS : Fin k -> Fin (S k)

interface Finite t where
  0 card   : Nat
  to     : t -> Fin card

implementation Finite (Fin k) where
  card = k
  to = id

interface BadFinite t where
  badcard   : Nat
  badto     : t -> Fin card

implementation BadFinite (Fin k) where
  badcard = k
  badto = id


text:
module Its

import Control.Monad.State

import Data.Maybe

%default total

--- Staty iterator ---

cr : Alternative m => MonadState (List a) m => m a
cr = do
  (x::xs) <- get
    | [] => empty
  put xs $> x

--- `MonadState` for `StateT` on pairs ---

export
Monad m => MonadState l (StateT (l, r) m) where
  get = Builtin.fst <$> get
  put = modify . mapFst . const

export
Monad m => MonadState r (StateT (l, r) m) where
  get = Builtin.snd <$> get
  put = modify . mapSnd . const

--- Data structure ---

data Y a b c = MkY a b c

data X a b c = MkX a a (Y a b ()) (Y a b c) c

Show a => Show b => Show c => Show (Y a b c) where
  show (MkY a b c) = "MkY \{show a} \{show b} \{show c}"

Show a => Show b => Show c => Show (X a b c) where
  show (MkX a1 a2 b1 b2 c) = "MkX \{show a1} \{show a2} (\{show b1}) (\{show b2}) \{show c}"

-- Iterator with external subiterators ---

itY : Applicative m => m a -> m b -> m c -> m (Y a b c)
itY ma mb mc = [| MkY ma mb mc |]

itX : Applicative m => m a -> m b -> m c -> m (X a b c)
itX ma mb mc = [| MkX ma ma (itY ma mb [| () |]) (itY ma mb mc) mc |]

--- Special data for special needs (tracking) ---

data TrackFull a = MkTrackFull (Maybe (a, Bool))

Functor TrackFull where
  map f (MkTrackFull m) = MkTrackFull $ mapFst f <$> m

Applicative TrackFull where
  pure = MkTrackFull . pure . (,True)
  MkTrackFull f <*> MkTrackFull x = MkTrackFull $ (\(f, bl) => bimap f (bl &&)) <$> f <*> x

Alternative TrackFull where
  empty = MkTrackFull empty
  x@(MkTrackFull (Just _)) <|> _             = x
  MkTrackFull Nothing      <|> MkTrackFull y = MkTrackFull $ y <&> mapSnd (const False)

Monad TrackFull where
  MkTrackFull m >>= f = MkTrackFull $ m >>= \(a, bl) => let MkTrackFull n = f a in mapSnd (bl &&) <$> n

-- like `fromMaybe` but for `TrackFull`
fromTrackEnd : Lazy a -> TrackFull a -> (a, Bool)
fromTrackEnd x (MkTrackFull cont) = fromMaybe (x, False) cont

--- Running harness ---

-- Like specialised `sequence` but produces the longest possible non-failing sequence
-- using recovering with `Alternative`
runPartialCartesian : Monad m => Alternative m => List (StateT s m a) -> StateT s m (List a)
runPartialCartesian []           = pure []
runPartialCartesian (curr::rest) = ST $ \s => do
  (s, l) <- map pure <$> runStateT s curr          <|> pure (s, [])
  (s, r) <- runStateT s (runPartialCartesian rest) <|> pure (s, [])
  pure (s, l ++ r)

xsc : (spending1 : List a) -> (cartesian : List b) -> (spending2 : List c) -> (List $ X a b c, Bool)
xsc as bs cs = fromTrackEnd [] $ evalStateT (as, cs) $ runPartialCartesian $
              itX (pure cr) (pure <$> bs) (pure cr) @{Applicative.Compose}

--- Example run ---

aLotOfNats : List Nat
aLotOfNats = [100 .. 999]

aFewNats : List Nat
aFewNats = [100 .. 130]

theStrs : List String
theStrs = ["a", "b", "c"]

theChrs : List Char
theChrs = chr <$> let k = ord 'a' in [k .. k + 25]

main : IO ()
main = for_ [aFewNats, aLotOfNats] $ \nats => do
  let (xs, full) = xsc nats theStrs theChrs
  for_ xs $ putStrLn . ("\n" ++) . show
  putStrLn "\n^^^^^^^^^ cartesian iteration was\{the String $ if full then "" else "n't"} full"

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Web.Internal.UIEventsTypes

import JS

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

export data CompositionEvent : Type where [external]

export
ToFFI CompositionEvent CompositionEvent where toFFI = id

export
FromFFI CompositionEvent CompositionEvent where fromFFI = Just

export
SafeCast CompositionEvent where
  safeCast = unsafeCastOnPrototypeName "CompositionEvent"

export data FocusEvent : Type where [external]

export
ToFFI FocusEvent FocusEvent where toFFI = id

export
FromFFI FocusEvent FocusEvent where fromFFI = Just

export
SafeCast FocusEvent where
  safeCast = unsafeCastOnPrototypeName "FocusEvent"

export data InputEvent : Type where [external]

export
ToFFI InputEvent InputEvent where toFFI = id

export
FromFFI InputEvent InputEvent where fromFFI = Just

export
SafeCast InputEvent where
  safeCast = unsafeCastOnPrototypeName "InputEvent"

export data KeyboardEvent : Type where [external]

export
ToFFI KeyboardEvent KeyboardEvent where toFFI = id

export
FromFFI KeyboardEvent KeyboardEvent where fromFFI = Just

export
SafeCast KeyboardEvent where
  safeCast = unsafeCastOnPrototypeName "KeyboardEvent"

export data MouseEvent : Type where [external]

export
ToFFI MouseEvent MouseEvent where toFFI = id

export
FromFFI MouseEvent MouseEvent where fromFFI = Just

export
SafeCast MouseEvent where
  safeCast = unsafeCastOnPrototypeName "MouseEvent"

export data UIEvent : Type where [external]

export
ToFFI UIEvent UIEvent where toFFI = id

export
FromFFI UIEvent UIEvent where fromFFI = Just

export
SafeCast UIEvent where
  safeCast = unsafeCastOnPrototypeName "UIEvent"

export data WheelEvent : Type where [external]

export
ToFFI WheelEvent WheelEvent where toFFI = id

export
FromFFI WheelEvent WheelEvent where fromFFI = Just

export
SafeCast WheelEvent where
  safeCast = unsafeCastOnPrototypeName "WheelEvent"

--------------------------------------------------------------------------------
--          Dictionaries
--------------------------------------------------------------------------------

export data CompositionEventInit : Type where [external]

export
ToFFI CompositionEventInit CompositionEventInit where toFFI = id

export
FromFFI CompositionEventInit CompositionEventInit where fromFFI = Just

export data EventModifierInit : Type where [external]

export
ToFFI EventModifierInit EventModifierInit where toFFI = id

export
FromFFI EventModifierInit EventModifierInit where fromFFI = Just

export data FocusEventInit : Type where [external]

export
ToFFI FocusEventInit FocusEventInit where toFFI = id

export
FromFFI FocusEventInit FocusEventInit where fromFFI = Just

export data InputEventInit : Type where [external]

export
ToFFI InputEventInit InputEventInit where toFFI = id

export
FromFFI InputEventInit InputEventInit where fromFFI = Just

export data KeyboardEventInit : Type where [external]

export
ToFFI KeyboardEventInit KeyboardEventInit where toFFI = id

export
FromFFI KeyboardEventInit KeyboardEventInit where fromFFI = Just

export data MouseEventInit : Type where [external]

export
ToFFI MouseEventInit MouseEventInit where toFFI = id

export
FromFFI MouseEventInit MouseEventInit where fromFFI = Just

export data UIEventInit : Type where [external]

export
ToFFI UIEventInit UIEventInit where toFFI = id

export
FromFFI UIEventInit UIEventInit where fromFFI = Just

export data WheelEventInit : Type where [external]

export
ToFFI WheelEventInit WheelEventInit where toFFI = id

export
FromFFI WheelEventInit WheelEventInit where fromFFI = Just


text:
nats : List Nat -> List Nat
nats = the (List Nat)

singletonRange : nats [1..1] = nats [1]
singletonRange = Refl

basicIncreasingRange : nats [1..3] = nats [1, 2 , 3]
basicIncreasingRange = Refl

basicDecreasingRange : nats [3..1] = nats [3, 2, 1]
basicDecreasingRange = Refl

increasingRangeWithStep : nats [3, 5..11] = nats [3, 5, 7, 9, 11]
increasingRangeWithStep = Refl

increaingRangeWithStepEmpty : nats [3, 5..1] = nats []
increaingRangeWithStepEmpty = Refl

singletonRangeWithStep : nats [3, 4..3] = nats [3]
singletonRangeWithStep = Refl

zeroStepEmptyList : nats [3, 3..5] = nats []
zeroStepEmptyList = Refl

zeroStepWhenBoundEqual : nats [1, 1..1] = nats [1]
zeroStepWhenBoundEqual = Refl

decreasingRangeWithStep : nats [11, 8..1] = nats [11, 8, 5, 2]
decreasingRangeWithStep = Refl

decreasingRangeWithStepEmpty : nats [9, 8..10] = nats []
decreasingRangeWithStepEmpty = Refl

decreasingSingletonRangeWithStep : nats [9, 8..9] = nats [9]
decreasingSingletonRangeWithStep = Refl