text:
module Data.Bytes.Util

moduleName : String
moduleName = "Data.Bytes.Util"

export
replicateM : Applicative f => Int -> f a -> f (List a)
replicateM n act = if 0 >= n then pure []
                             else [| act :: replicateM (n-1) act |]

-- Try not to use this, it'd be quite slow, better to use a casting prim of
-- some kind when one exists. This still has to +1 over and over after Nat is
-- optimized to Integer.
export
intToNat : Int -> Nat
intToNat i = if i >= 0 then go i else Z
  where
    go : Int -> Nat
    go 0 = Z
    go k = 1 + go (k-1)

-------------------------------------------------
-- Lies
-------------------------------------------------

-- Why lie about totality?

-- One may ask "If a thing can fail is it not partial?" but consider the total
-- expression x :: xs, if we fail to allocate space when applying :: does that
-- mean :: was partial all along? That's simply a failure of the system we're
-- running on not a failure of totality. The single intended use of this lie is
-- during allocation of bytes in memory. This is why we're lying here: There's
-- no reason to infect a whole codebase with partiality when it's outside
-- allocation that is failing.

-- TODO: bring this up with other devs for idris about it's merits and negatives
-- The less backdoors the better imo but this seems like a innocuous thing.
private
total
%foreign "scheme:lambda (x) (blodwen-error-quit x)"
lie_idris_crash : String -> a

export
total
lieErrorCall : String -> String -> String -> a
lieErrorCall mod fn_name msg = lie_idris_crash $ mod ++ ":" ++ fn_name ++ ": " ++ msg

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

export
partial
errorCall : String -> String -> String -> a
errorCall mod fn_name msg = idris_crash $ mod ++ ":" ++ fn_name ++ ": " ++ msg

-- It'd be nice to have have statically enforced size limits but it's a little
-- onerous at this stage and not something we should be forcing on users.
-- Integer would be safer but there's a (likely) size and performance hit that
-- would need investigating, tied with the fact that our Bytes can only be Int
-- large in the first place so that just moves the check not elimates it.
export
partial
checkedAdd : String -> String -> Int -> Int -> Int
checkedAdd mod fun x y
  = let v = x + y
    in if v >= 0 then v else errorCall mod fun $
         "numeric overflow: " ++ show x ++ " + " ++ show y ++ " = " ++ show v

public export
total -- minus where negative results are just 0
monus : Nat -> Nat -> Nat
monus n 0 = n
monus 0 n = 0
monus (S j) (S k) = monus j k

----------------------------------------------------------------------
-- Helpers
----------------------------------------------------------------------

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


text:
module Control.Cont.State

import Control.HigherOrder

import Control.Monad.Free

public export
data StateC1 : Type -> Type -> Type where
  Get : (s -> x) -> StateC1 s x
  Put : s -> x -> StateC1 s x

public export
Functor (StateC1 s) where
  map f (Get g) = Get (f . g)
  map f (Put s x) = Put s (f x)

public export
StateC : Type -> (Type -> Type) -> Type -> Type
StateC s = Lift (StateC1 s)

public export
runStateC : Syntax sig
         => s
         -> Free (StateC s :+: sig) a
         -> Free sig (s, a)
runStateC s (Return x) = Return (s, x)
runStateC s (Op (Inl (MkLift (Get k)))) =
  runStateC s (k s)
runStateC s (Op (Inl (MkLift (Put s' k)))) =
  runStateC s' k
runStateC s (Op (Inr op)) =
  Op (weave {m1 = ?t} {s = Pair _} (s, ()) (uncurry runStateC) op)

public export
get : (Inj (StateC s) sig) => Free sig s
get = inject {sub = StateC s} (MkLift (Get Return))

public export
put : (Inj (StateC s) sig) => s -> Free sig ()
put val = inject {sub = StateC s} (MkLift (Put val (Return ())))

public export
modify : Syntax sig => Inj (StateC s) sig => (s -> s) -> Free sig ()
modify f = do
  v <- get
  put (f v)

public export
withSt : Syntax sig => Inj (StateC st) sig => a -> Free sig (st, a)
withSt x = map (, x) get

ext: idr


text:
import Data.IORef

count : HasReference ffi =>  Nat -> IORef Integer -> IO' ffi ()
count Z ref
    = do x <- readIORef' ref
         printLn' x
count (S k) ref
    = do modifyIORef' ref (+1)
         count k ref

main : IO ()
main = do r <- newIORef' 0
          count 1000 r

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:
import Data.Vect

word_lengths : Vect len String -> Vect len Nat
word_lengths [] = []
word_lengths (x :: xs) = length x :: word_lengths xs

insert : (Ord elem) => (x : elem) -> (xs_sorted : Vect k elem) -> Vect (S k) elem
insert x [] = [x]
insert x (y :: xs) = case x < y of
                          False => y :: insert x xs
                          True => x :: y :: xs

ins_sort : (Ord elem) => Vect n elem -> Vect n elem
ins_sort [] = []
ins_sort (x :: xs) = let xs_sorted = ins_sort xs in
                         insert x xs_sorted

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
{-
Copyright 2018, Mokshasoft AB (mokshasoft.com)

This software may be distributed and modified according to the terms of
the BSD 2-Clause license. Note that NO WARRANTY is provided.
See "LICENSE_BSD2.txt" for details.
-}

module seL4.Bootinfo

import seL4.BootinfoTypes
import seL4.seL4Debug
import seL4.SharedTypes
import seL4.Types

%include C "ffi-bootinfo.h"
%access public export
%default total

get_bootinfo_ptr : IO Ptr
get_bootinfo_ptr = foreign FFI_C "get_bootinfo" (IO Ptr)

peek8 : Ptr -> Int -> IO Int
peek8 ptr offset = do
    _val <- prim_peek8 ptr offset
    pure $ prim__zextB8_Int _val

ifdef(`CONFIG_ARCH_X86_64', `

wordSize : Int
wordSize = 8

b64ToInt : Bits64 -> Int
b64ToInt b = sum $
    List.zipWith (*)
                 (map (\p => pow 256 (the Nat p)) [7..0])
                 (map prim__zextB8_Int (b64ToBytes b))

peekWord : Ptr -> Int -> IO Int
peekWord ptr offset = do
    _val <- prim_peek64 ptr offset
    pure $ b64ToInt _val

')

ifdef(`CONFIG_ARCH_IA32', `

wordSize : Int
wordSize = 4

b32ToInt : Bits32 -> Int
b32ToInt b = sum $
    List.zipWith (*)
                 (map (\p => pow 256 (the Nat p)) [3..0])
                 (map prim__zextB8_Int (b32ToBytes b))

peekWord : Ptr -> Int -> IO Int
peekWord ptr offset = do
    _val <- prim_peek32 ptr offset
    pure $ b32ToInt _val

')

peekSlotRegion : Ptr -> Int -> IO SeL4_SlotRegion
peekSlotRegion ptr offset = do
    _start <- peekWord ptr (offset + 0)
    _end   <- peekWord ptr (offset + wordSize)
    pure $ MKSeL4_SlotRegion _start _end

ifdef(`CONFIG_ARCH_X86_64', `

seL4_GetBootinfo : IO SeL4_BootInfo
seL4_GetBootinfo = do
    ptr <- get_bootinfo_ptr
    _extraLen         <- peekWord ptr 0
    _nodeID           <- peekWord ptr 8
    _numNodes         <- peekWord ptr 16
    _numIOPTLevels    <- peekWord ptr 24
    _ipcBuffer        <- peekWord ptr 32
    _empty            <- peekSlotRegion ptr 40
    _sharedFrames     <- peekSlotRegion ptr 56
    _userImageFrames  <- peekSlotRegion ptr 72
    _userImagePaging  <- peekSlotRegion ptr 88
    _ioSpaceCaps      <- peekSlotRegion ptr 104
    _extraBIPages     <- peekSlotRegion ptr 120
    _initThreadCNodeSizeBits <- peek8 ptr 136
    _initThreadDomain <- peekWord ptr 137
    _archInfo         <- peekWord ptr 145
    _untyped          <- peekSlotRegion ptr 153
    pure $
        MKSeL4_BootInfo
            _extraLen
            _nodeID
            _numNodes
            _numIOPTLevels
            _ipcBuffer
            _empty
            _sharedFrames
            _userImageFrames
            _userImagePaging
            _ioSpaceCaps
            _extraBIPages
            _initThreadCNodeSizeBits
            _initThreadDomain
            _archInfo
            _untyped

')

ifdef(`CONFIG_ARCH_IA32', `

seL4_GetBootinfo : IO SeL4_BootInfo
seL4_GetBootinfo = do
    ptr <- get_bootinfo_ptr
    _extraLen         <- peekWord ptr 0
    _nodeID           <- peekWord ptr 4
    _numNodes         <- peekWord ptr 8
    _numIOPTLevels    <- peekWord ptr 12
    _ipcBuffer        <- peekWord ptr 16
    _empty            <- peekSlotRegion ptr 20
    _sharedFrames     <- peekSlotRegion ptr 28
    _userImageFrames  <- peekSlotRegion ptr 36
    _userImagePaging  <- peekSlotRegion ptr 44
    _ioSpaceCaps      <- peekSlotRegion ptr 52
    _extraBIPages     <- peekSlotRegion ptr 60
    _initThreadCNodeSizeBits <- peek8 ptr 68
    _initThreadDomain <- peekWord ptr 69
    _archInfo         <- peekWord ptr 73
    _untyped          <- peekSlotRegion ptr 77
    pure $
        MKSeL4_BootInfo
            _extraLen
            _nodeID
            _numNodes
            _numIOPTLevels
            _ipcBuffer
            _empty
            _sharedFrames
            _userImageFrames
            _userImagePaging
            _ioSpaceCaps
            _extraBIPages
            _initThreadCNodeSizeBits
            _initThreadDomain
            _archInfo
            _untyped

')


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

module Commons.Options.ArgParse.Error

import Commons.Data.Location

import Commons.Options.ArgParse.Model
import Commons.Options.ArgParse.Lexer
import Commons.Options.ArgParse.Parser

%default total
%access public export

data ArgParseError : Type where
  InvalidOption   : Arg -> ArgParseError
  MalformedOption : ParseError Token -> ArgParseError

(Show Arg) => Show ArgParseError where
  show (InvalidOption o) = "Invalid Option " ++ show o
  show (MalformedOption (PError (MkParseFail error location rest))) =
    unlines [show location, error]
  show (MalformedOption (LError (MkLexFail l i)))  = unwords [show l, ":\n" <+> i]
  show (MalformedOption (FError x))  = unlines ["File Error:", show x]

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

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


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

module Language.TOML.Lexer

import Text.Lexer
import Text.Token

import public Language.TOML.Tokens

%default total

private
nonZeroDigit : Lexer
nonZeroDigit = range '1' '9'

private
floatLit : Lexer
floatLit
  = let sign     = oneOf "+-"
        whole    = is '0' <|> nonZeroDigit <+> many (opt (is '_') <+> digit)
        frac     = the Lexer $ is '.' <+> digit <+> many (opt (is '_') <+> digit)
        exp      = the Lexer $ like 'e' <+> opt (oneOf "+-") <+> digits
        constant = exact "nan" <|> exact "inf" in
        opt sign <+> (
            whole <+> ((frac <+> opt exp) <|> exp)
            <|> constant)

private
sepIntLit : Lexer
sepIntLit = opt (oneOf "+-") <+> nonZeroDigit <+> many (is '_' <|> digit)

private
sepBaseLit : (pre : String) -> (digit : Lexer) -> Lexer
sepBaseLit pre digit =
    exact pre
    <+> digit
    <+> many (opt (is '_') <+> digit)

private
integerLit : Lexer
integerLit =
    (sepBaseLit "0x" hexDigit
    <|> sepBaseLit "0o" octDigit
    <|> sepBaseLit "0b" binDigit
    <|> sepIntLit) <+> reject (oneOf ".eE")

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

-- TODO doesn't handle single quoted strings or escapes yet
private
basicStringLit : Lexer
basicStringLit = quote (is '"') (escape (is '\\') any <|> isNot '\\')

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

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

max_stars_repo_name: sepiina/toml-idr

max_issues_repo_name: sepiina/toml-idr

max_forks_repo_name: sepiina/toml-idr


text:
module BottomUpMergeSort

import Sortable

%default total
%access private

export
data MergeSort a = MS Int (Lazy (List (List a)))

mrg : Ord a => List a -> List a -> List a
mrg    []         ys            = ys
mrg xs               []         = xs
mrg xs@(x :: xs') ys@(y :: ys') =
  if x <= y then x :: mrg xs' ys else y :: mrg xs ys'

addSeg : Ord a => List a -> List (List a) -> Int -> List (List a)
addSeg seg segs size = let size' = assert_total $ size `div` 2
                           r     = assert_total $ size `mod` 2 in
  if 0 == r then seg :: segs
            else addSeg (mrg seg (head segs {ok = segsNonEmpty}))
                        (tail segs {ok = segsNonEmpty})
                        (assert_smaller size size')
 where
  segsNonEmpty = believe_me "length segs = ceil lg size"

export
Sortable MergeSort where
  empty = MS 0 []
  add x (MS size segs) = MS (size + 1) (addSeg [x] segs size)
  sort (MS size segs) = foldl mrg [] segs


text:
data TakeN : List a -> Type where
    Fewer : TakeN xs
    Exact : (n_xs : List a) -> TakeN (n_xs ++ rest)

total
takeN : (n : Nat) -> (xs : List a) -> TakeN xs
takeN Z xs = Exact []
takeN (S k) [] = Fewer
takeN (S k) (x :: xs) =
    case takeN k xs of
        Fewer => Fewer
        Exact taken => Exact (x :: taken)

groupByN : (n : Nat) -> (xs : List a) -> List (List a)
groupByN n xs with (takeN n xs)
  groupByN n xs | Fewer = [xs]
  groupByN n (n_xs ++ rest) | (Exact n_xs) = n_xs :: groupByN n rest

halves : List a -> (List a, List a)
halves xs with (takeN (div (length xs) 2) xs)
  halves xs | Fewer = ([], xs)
  halves (n_xs ++ rest) | (Exact n_xs) = (n_xs, rest)


text:
main: IO ()
main = putStrLn "Hello, world!"

max_stars_repo_name: nixdog/helloworld

max_issues_repo_name: nixdog/helloworld

max_forks_repo_name: nixdog/helloworld


text:
module TypeCheck

import Syntax

public export
TypeError : Type
TypeError = String

typeError : TypeError -> Either TypeError Ty
typeError msg = Left msg

||| Type context.
public export
Ctx : Type
Ctx = List (Name, Ty)

mutual
  check : Ctx -> Ty -> Expr -> Either TypeError Ty
  check ctx ty e = do
    ty' <- typeOf ctx e
    if ty' /= ty
    then typeError ((show e) ++ " has type " ++ (show ty') ++ " but is used as if it has type " ++ (show ty))
    else pure ty

  ||| `typeOf ctx e` computes the type of expression `e` in
  ||| type context `ctx`. If `e` does not have a type it
  ||| returns a `TypeError`.
  export
  typeOf : Ctx -> Expr -> Either TypeError Ty
  typeOf ctx e = case e of
    Var name => case lookup name ctx of
                  Nothing => typeError ("unknown variable " ++ name)
                  Just ty => Right ty
    EInt _  => Right TInt
    EBool _ => Right TBool
    Times e1 e2 => do check ctx TInt e1
                      check ctx TInt e2
                      pure TInt
    Plus e1 e2  => do check ctx TInt e1
                      check ctx TInt e2
                      pure TInt
    Minus e1 e2 => do check ctx TInt e1
                      check ctx TInt e2
                      pure TInt
    Equal e1 e2 => do check ctx TInt e1
                      check ctx TInt e2
                      pure TBool
    Less e1 e2  => do check ctx TInt e1
                      check ctx TInt e2
                      pure TBool

    If e1 e2 e3 => do check ctx TBool e1
                      ty <- typeOf ctx e2
                      check ctx ty e3
                      pure ty

    Fun f x pty rty e => let ectx = (f, TArrow pty rty) :: (x, pty) :: ctx in
                         do check ectx rty e
                            pure (TArrow pty rty)

    Apply e1 e2 =>  do ty1 <- typeOf ctx e1
                       case ty1 of
                         TArrow pty rty => do check ctx pty e2
                                              pure rty
                         ty => typeError $ (show e1) ++ " is used as a function but its type is " ++ (show ty)

max_stars_repo_name: steshaw/idris-miniml

max_issues_repo_name: steshaw/idris-miniml

max_forks_repo_name: steshaw/idris-miniml


text:
module Idris.Parser.Let

import Idris.Syntax
import Libraries.Text.Bounded

import Data.Either
import Data.List1

import Libraries.Utils.String

%default total

------------------------------------------------------------------------
-- Types

-- `let ... in ...` is used for two different notions:
-- * pattern-matching let binders to locally take an expression apart
-- * Local definitions that can be recursive

public export
record LetBinder where
  constructor MkLetBinder
  letUsage     : RigCount
  letPattern   : PTerm
  letBoundType : PTerm
  letBoundTerm : PTerm
  letUnhappy   : List PClause

public export
LetDecl : Type
LetDecl = List PDecl

------------------------------------------------------------------------
-- Let-binding functions

letFactory : (List (WithBounds LetBinder) -> a -> a) ->
             (WithBounds LetDecl -> a -> a) ->
             List1 (WithBounds (Either LetBinder LetDecl)) ->
             a -> a
letFactory letBind letDeclare blocks scope = foldr mkLet scope groups where

  LetBlock : Type
  LetBlock = Either (List1 (WithBounds LetBinder)) (List1 (WithBounds LetDecl))

  groups : List LetBlock
  groups = compress (forget $ map (\ b => bimap (<$ b) (<$ b) b.val) blocks)

  mkLet : LetBlock -> a -> a
  mkLet (Left  letBinds) = letBind (forget letBinds)
  mkLet (Right letDecls) =
    let bounds = mergeBounds (head letDecls) (last letDecls)
    in letDeclare (concatMap val letDecls <$ bounds)

export
mkLets : OriginDesc ->
         List1 (WithBounds (Either LetBinder LetDecl)) ->
         PTerm -> PTerm
mkLets origin = letFactory buildLets
  (\ decls, scope => PLocal (virtualiseFC $ boundToFC origin decls) decls.val scope)

  where

    buildLets : List (WithBounds LetBinder) -> PTerm -> PTerm
    buildLets [] sc = sc
    buildLets (b :: rest) sc
      = let (MkLetBinder rig pat ty val alts) = b.val
            fc = virtualiseFC $ boundToFC origin b
        in PLet fc rig pat ty val (buildLets rest sc) alts

export
mkDoLets : OriginDesc ->
           List1 (WithBounds (Either LetBinder LetDecl)) ->
           List PDo
mkDoLets origin lets = letFactory
    (\ binds, rest => buildDoLets binds ++ rest)
    (\ decls, rest => DoLetLocal (boundToFC origin decls) decls.val :: rest)
    lets
    []

  where

    buildDoLets : List (WithBounds LetBinder) -> List PDo
    buildDoLets [] = []
    buildDoLets (b :: rest) = let fc = boundToFC origin b in case b.val of
      (MkLetBinder rig (PRef fc' (UN un)) ty val []) =>
         (if isPatternVariable un
            then DoLet fc fc' (UN un) rig ty val
            else DoLetPat fc (PRef fc' (UN un)) ty val []
         ) :: buildDoLets rest
      (MkLetBinder rig (PImplicit fc') ty val []) =>
        DoLet fc fc' (UN Underscore) rig ty val :: buildDoLets rest
      (MkLetBinder rig pat ty val alts) =>
        DoLetPat fc pat ty val alts :: buildDoLets rest


text:
module Reverse

reverse' : List a -> List a
reverse' xs = revAcc [] xs where
  revAcc : List a -> List a -> List a
  revAcc acc [] = acc
  revAcc acc (x :: xs) = revAcc (x :: acc) xs

max_stars_repo_name: aztecrex/try-idris

max_issues_repo_name: aztecrex/try-idris

max_forks_repo_name: aztecrex/try-idris


text:
module PackageFormat

import Effects
import Effect.File

import Lightyear
import Lightyear.Char
import Lightyear.Strings
import Lightyear.Combinators
import Lightyear.StringFile

import Package
import ConfigProvider

%language TypeProviders
-- Disabled to stop compiler from hanging on this file
--%provide (defaultDir : String) with getPkgPath

defaultDir : String
defaultDir = "./example/"

record PackageMeta where
  constructor Meta
  name, description, license, homepage, issues, maintainer : String
  contributors : List String
  installCandidates : List Pkg

Show PackageMeta where
  show pkg = "\n " ++ unwords
             [ "Name: " ++ name pkg ++ "\n"
             , "Description: " ++ description pkg ++ "\n"
             , "License: " ++ license pkg ++ "\n"
             , "Homepage: " ++ homepage pkg ++ "\n"
             , "Issues: " ++ issues pkg ++ "\n"
             , "Maintainer: " ++ maintainer pkg ++ "\n"
             , "Contributors: " ++ (show $ contributors pkg) ++ "\n"
             , "Install Candidates: " ++ (show' $ installCandidates pkg) ++ "\n"
             ]
  where show' : List Pkg -> String
        show' pkgs = show $ map (show @{pkgverbose}) pkgs

data Sexpr = Ident   String
           | Literal String
           | ExpList (List Sexpr)

spacedOut : Parser a -> Parser a
spacedOut x = spaces *> x <* spaces

ident : Parser Sexpr
ident = Ident <$> liftA2 strCons first (the (List Char -> String) pack <$> rest)
  where sym : Parser Char -- Why is this one needed, but not the others?
        sym   = oneOf "!@#$%^&*-_=+[{]};:'\\|,<.>/?`~"
        first = letter <|> sym
        rest  = many $ alphaNum <|> sym

literal : Parser Sexpr
literal = Literal <$> quoted '"'

mutual
  explist : Parser Sexpr
  explist = ExpList <$> (char '(') >! many sexpr <* (char ')')

  sexpr : Parser Sexpr
  sexpr = spacedOut ident <|> spacedOut literal <|> spacedOut explist

Show Sexpr where
  show (Ident s)    = s
  show (Literal s)  = "\"" ++ s ++ "\""
  show (ExpList xs) = show xs

parseVersion : Parser Version
parseVersion = (\[x, y, z] => V (cast x) (cast y) (cast z)) <$> sepByN 3 integer (char '.')

Alternative (Either String) where     -- Needed for us to use choice
  empty   = Left "Error in package definition/empty"
  a <|> b = case (a, b) of
              (Right a,      _) => Right a
              (Left _, Right a) => Right a
              (Left e, Left  _) => Left e

join : Either a (Either a b) -> Either a b
join (Left a)          = Left a
join (Right (Left a))  = Left a
join (Right (Right b)) = Right b

find : String -> Sexpr -> Either String Sexpr
find q (ExpList $ (Ident x)::xs) = if x == q then
                                     return $ ExpList $ (Ident x)::xs
                                   else choice $ map (find q) xs
find q s                         = Left $ "Error in package definition/find " ++ q ++ " for " ++ show s

extract : Sexpr -> Either String String
extract (ExpList $ _::(Literal s)::_) = return s
extract (ExpList $ _::(Ident s)::_)   = return s
extract (ExpList _)                   = Left "Error in package definition/extract"

extractl : Sexpr -> Either String (List String)
extractl (ExpList [])      = return []
extractl (ExpList $ (Literal x)::xs) = do return $ x :: !(extractl $ ExpList xs)
extractl (ExpList $ (Ident x)::xs)   = do extractl $ ExpList xs
extractl _                           = Left "Error in package definition/extractl"

getDependency : Sexpr -> Dep
getDependency sexpr = case sexpr of
                        ExpList [Ident "*", name]                => Dependency (read name) Any []
                        ExpList [Ident "=", version, name]       => Dependency (read name) (Exactly $ readv version) []
                        ExpList [Ident ">", lower, name]         => Dependency (read name) (Up $ readv lower) []
                        ExpList [Ident "<", upper, name]         => Dependency (read name) (Down $ readv upper) []
                        ExpList [Ident "><", lower, upper, name] => Dependency (read name) (Between (readv lower) (readv upper)) []
                        _                                        => Dependency "Error" Any []
  where read : Sexpr -> String
        read (Ident i)        = i
        read (Literal s)      = s
        read (ExpList (x::_)) = read x

        readv : Sexpr -> Version
        readv vstr = case parse parseVersion $ read vstr of
                       Left _  => V 1 0 0
                       Right v => v

getCandidates : String -> List Sexpr -> Either String (List Pkg)
getCandidates name []      = return []
getCandidates name (x::xs) = do case parseCandidate x of
                                  Left e  => Left e
                                  Right p => return $ p :: !(getCandidates name xs)
  where parseCandidate : Sexpr -> Either String Pkg
        parseCandidate sexpr = do root <- find "v" sexpr
                                  version <- parse parseVersion !(extract root)
                                  ExpList (_::depsroot) <- find "depends" root
                                    | sexpr => Left ("Error while reading dependencies of a package file: " ++ show sexpr)
                                  deps <- return $ map getDependency depsroot -- Finish building this tree...
                                  src <- extract !(find "src" root)
                                  hash <- extractHash !(find "hash" root <|> find "hash-sha1" root <|> find "hash-md5" root <|> (Right $ ExpList []))
                                  compile <- extract !(find "compile" root <|> (Right $ ExpList [])) <|> return "./configure && make"
                                  install <- extract !(find "install" root <|> (Right $ ExpList [])) <|> return "sudo make install"
                                  uninstall <- extract !(find "uninstall" root <|> (Right $ ExpList [])) <|> return "sudo make uninstall"
                                  return $ Package name version compile install uninstall src hash deps
    where extractHash : Sexpr -> Either String Hash
          extractHash (ExpList [Ident "hash",      Literal h]) = return $ Blake2 h
          extractHash (ExpList [Ident "hash-md5",  Literal h]) = return $ Md5 h
          extractHash (ExpList [Ident "hash-sha1", Literal h]) = return $ Sha1 h
          extractHash _                                        = return None

getData : Sexpr -> Either String PackageMeta
getData sexpr = do root <- find "pkg" sexpr
                   name <- extract !(find "name" root)
                   desc <- extract !(find "description" root)
                   license <- extract !(find "license" root)
                   homepage <- extract !(find "homepage" root)
                   issues <- extract !(find "issues" root)
                   maintainer <- extract !(find "maintainer" root)
                   contributors <- extractl !(find "contributors" root)
                   candidates <- getCandidates name $ case !(find "candidates" root) of
                                                        ExpList (_::xs) => xs
                                                        _               => []
                   return (Meta name desc license homepage issues maintainer contributors candidates)

parseMeta : Parser (Either String PackageMeta)
parseMeta = do tree <- sexpr
               return $ getData tree

readPackage : String -> Eff (Either String PackageMeta) [FILE_IO ()]
readPackage name = do meta <- readFile (\err => "Couldn't find package: " ++ name) (defaultDir ++ "db/" ++ name ++ ".forge")
                      return $ join $ meta >>= parse parseMeta

readSexpr : String -> Eff (Either String Sexpr) [FILE_IO ()]
readSexpr name = do sexp <- readFile (\err => "Couldn't find package: " ++ name) (defaultDir ++ "db/" ++ name ++ ".forge")
                    return $ sexp >>= parse sexpr

max_stars_repo_name: nv-vn/Anvil

max_issues_repo_name: nv-vn/Anvil

max_forks_repo_name: nv-vn/Anvil


text:
module FishInElab

import Language.Reflection

%default total

%language ElabReflection

x : List String
x = ["a", "b"]

infixl 1 >==>

-- From prelude:
--(>=>) : Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
--(>=>) f g = \x => f x >>= g

(>==>) : Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
(>==>) f g = \x => f x >>= \r => g r

%runElab traverse_ (pure >==> logMsg "debug" 0) x -- works
%runElab traverse_ (pure >=> \s => logMsg "debug" 0 s) x -- works
%runElab traverse_ (pure >=> logMsg "debug" 0) x -- should work, but does not

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Main

main : IO ()
main = putStrLn "Cum vă numiți?"
-- todo

max_stars_repo_name: ioanluca/real-world-idris

max_issues_repo_name: ioanluca/real-world-idris

max_forks_repo_name: ioanluca/real-world-idris


text:
module Language.SystemVerilog.MetaTypes

import        Data.String

import public Toolkit.Data.DList.DeBruijn
import public Toolkit.Decidable.Equality.Indexed

%default total

public export
data Ty = MODULE (List String)
        | DATA
        | CHAN
        | PORT String
        | MINST (List String)
        | UNIT
        | TYPE
        | GATE
        | GINST

export
Show Ty where
  show (MODULE xs) = unwords ["(MODULE", show xs, ")"]
  show DATA = "(DATA)"
  show CHAN = "(CHAN)"
  show (PORT x) = unwords ["(PORT", show x, ")"]
  show (MINST xs) = unwords ["(MINST", show xs, ")"]
  show UNIT = "(UNIT)"
  show TYPE = "(TYPE)"
  show GATE = "(GATE)"
  show GINST = "(GINST)"

public export
Context : Type
Context = List (Pair String Ty)

public export
Index : Context -> Pair String Ty -> Type
Index = DeBruijn.Index (Pair String Ty)

export
Eq Ty where
  (==) (MODULE xs)   (MODULE ys)     = xs == ys
  (==) DATA          DATA            = True
  (==) CHAN          CHAN            = True
  (==) (PORT x)      (PORT y)        = x == y
  (==) (MINST xs)    (MINST ys)      = xs == ys
  (==) UNIT          UNIT            = True
  (==) TYPE          TYPE            = True
  (==) GATE          GATE            = True
  (==) GINST         GINST           = True
  (==) _             _               = False

namespace DecEq

  -- Modules

  modulesDifferentNames : (xs : List String)
                       -> (ys : List String)
                       -> (contra : (xs = ys) -> Void)
                       -> (MODULE xs = MODULE ys)
                       -> Void
  modulesDifferentNames ys ys contra Refl = contra Refl

  moduleDataNotEq : (MODULE xs = DATA) -> Void
  moduleDataNotEq Refl impossible

  moduleChanNotEq : (MODULE xs = CHAN) -> Void
  moduleChanNotEq Refl impossible

  modulePortNotEq : (MODULE xs = PORT x) -> Void
  modulePortNotEq Refl impossible

  moduleDeclmoduleInstNotEq : (MODULE xs = MINST ys) -> Void
  moduleDeclmoduleInstNotEq Refl impossible

  moduleUnitNotEq : (MODULE xs = UNIT) -> Void
  moduleUnitNotEq Refl impossible

  moduleTypeNotEq : (MODULE xs = TYPE) -> Void
  moduleTypeNotEq Refl impossible

  moduleGateNotEq : (MODULE xs = GATE) -> Void
  moduleGateNotEq Refl impossible

  moduleGinstNotEq : (MODULE xs = GINST) -> Void
  moduleGinstNotEq Refl impossible

  -- Data.

  dataChanNotEq : (DATA = CHAN) -> Void
  dataChanNotEq Refl impossible

  dataPortNotEq : (DATA = PORT x) -> Void
  dataPortNotEq Refl impossible

  dataModuleInstNotEq : (DATA = MINST xs) -> Void
  dataModuleInstNotEq Refl impossible

  dataUnitNotEq : (DATA = UNIT) -> Void
  dataUnitNotEq Refl impossible

  dataTypeNotEq : (DATA = TYPE) -> Void
  dataTypeNotEq Refl impossible

  dataGateNotEq : (DATA = GATE) -> Void
  dataGateNotEq Refl impossible

  dataGinstNotEq : (DATA = GINST) -> Void
  dataGinstNotEq Refl impossible

  -- Channels

  chanPortNotEq : (CHAN = PORT x) -> Void
  chanPortNotEq Refl impossible

  chanModuleInstNotEq : (CHAN = MINST xs) -> Void
  chanModuleInstNotEq Refl impossible

  chanUnitNotEq : (CHAN = UNIT) -> Void
  chanUnitNotEq Refl impossible

  chanTypeNotEq : (CHAN = TYPE) -> Void
  chanTypeNotEq Refl impossible

  chanGateNotEq : (CHAN = GATE) -> Void
  chanGateNotEq Refl impossible

  chanGinstNotEq : (CHAN = GINST) -> Void
  chanGinstNotEq Refl impossible

  -- Port

  portLabelMismatch : (contra : (x = y) -> Void) -> (PORT x = PORT y) -> Void
  portLabelMismatch contra Refl = contra Refl

  portModuleInstNotEq : (PORT x = MINST xs) -> Void
  portModuleInstNotEq Refl impossible

  portUnitNotEq : (PORT x = UNIT) -> Void
  portUnitNotEq Refl impossible

  portTypeNotEq : (PORT x = TYPE) -> Void
  portTypeNotEq Refl impossible

  portGateNotEq : (PORT x = GATE) -> Void
  portGateNotEq Refl impossible

  portGinstNotEq : (PORT x = GINST) -> Void
  portGinstNotEq Refl impossible

  -- MInst
  moduleInstParamsDiffer : (xs : List String)
                        -> (ys : List String)
                        -> (contra : (xs = ys) -> Void) -> (MINST xs = MINST ys) -> Void
  moduleInstParamsDiffer ys ys contra Refl = contra Refl

  moduleInstUnitNotEq : (MINST xs = UNIT) -> Void
  moduleInstUnitNotEq Refl impossible

  moduleInstTypeNotEq : (MINST xs = TYPE) -> Void
  moduleInstTypeNotEq Refl impossible

  moduleInstGateNotEq : (MINST xs = GATE) -> Void
  moduleInstGateNotEq Refl impossible

  moduleInstGinstNotEq : (MINST xs = GINST) -> Void
  moduleInstGinstNotEq Refl impossible

  -- Unit

  unitTypeNotEq : (UNIT = TYPE) -> Void
  unitTypeNotEq Refl impossible

  unitGateNotEq : (UNIT = GATE) -> Void
  unitGateNotEq Refl impossible

  unitGinstNotEq : (UNIT = GINST) -> Void
  unitGinstNotEq Refl impossible

  -- Type

  typeGateNotEq : (TYPE = GATE) -> Void
  typeGateNotEq Refl impossible

  typeGinstNotEq : (TYPE = GINST) -> Void
  typeGinstNotEq Refl impossible

  -- Gate
  gateGinstNotEq : (GATE = GINST) -> Void
  gateGinstNotEq Refl impossible

  -- Definition

  decEqTy : (x,y : Ty) -> Dec (x = y)
  decEqTy (MODULE xs) ty with (ty)
    decEqTy (MODULE xs) ty | (MODULE ys) with (decEq xs ys)
      decEqTy (MODULE ys) ty | (MODULE ys) | (Yes Refl) = Yes Refl
      decEqTy (MODULE xs) ty | (MODULE ys) | (No contra) = No (modulesDifferentNames xs ys contra)

    decEqTy (MODULE xs) ty | DATA = No (moduleDataNotEq)
    decEqTy (MODULE xs) ty | CHAN = No (moduleChanNotEq)
    decEqTy (MODULE xs) ty | (PORT x) = No (modulePortNotEq)
    decEqTy (MODULE xs) ty | (MINST ys) = No (moduleDeclmoduleInstNotEq)
    decEqTy (MODULE xs) ty | UNIT = No (moduleUnitNotEq)
    decEqTy (MODULE xs) ty | TYPE = No (moduleTypeNotEq)
    decEqTy (MODULE xs) ty | GATE = No (moduleGateNotEq)
    decEqTy (MODULE xs) ty | (GINST) = No (moduleGinstNotEq)

  decEqTy DATA ty with (ty)
    decEqTy DATA ty | (MODULE xs) = No (negEqSym moduleDataNotEq)
    decEqTy DATA ty | DATA = Yes Refl
    decEqTy DATA ty | CHAN = No (dataChanNotEq)
    decEqTy DATA ty | (PORT x) = No (dataPortNotEq)
    decEqTy DATA ty | (MINST xs) = No (dataModuleInstNotEq)
    decEqTy DATA ty | UNIT = No (dataUnitNotEq)
    decEqTy DATA ty | TYPE = No (dataTypeNotEq)
    decEqTy DATA ty | GATE = No (dataGateNotEq)
    decEqTy DATA ty | (GINST) = No (dataGinstNotEq)

  decEqTy CHAN ty with (ty)
    decEqTy CHAN ty | (MODULE xs) = No (negEqSym moduleChanNotEq)
    decEqTy CHAN ty | DATA = No (negEqSym dataChanNotEq)
    decEqTy CHAN ty | CHAN = Yes Refl
    decEqTy CHAN ty | (PORT x) = No (chanPortNotEq)
    decEqTy CHAN ty | (MINST xs) = No (chanModuleInstNotEq)
    decEqTy CHAN ty | UNIT = No (chanUnitNotEq)
    decEqTy CHAN ty | TYPE = No (chanTypeNotEq)
    decEqTy CHAN ty | GATE = No (chanGateNotEq)
    decEqTy CHAN ty | (GINST) = No (chanGinstNotEq)

  decEqTy (PORT x) ty with (ty)
    decEqTy (PORT x) ty | (MODULE xs) = No (negEqSym modulePortNotEq)
    decEqTy (PORT x) ty | DATA = No (negEqSym dataPortNotEq)
    decEqTy (PORT x) ty | CHAN = No (negEqSym chanPortNotEq)
    decEqTy (PORT x) ty | (PORT y) with (decEq x y)
      decEqTy (PORT y) ty | (PORT y) | (Yes Refl) = Yes Refl
      decEqTy (PORT x) ty | (PORT y) | (No contra) = No (portLabelMismatch contra)

    decEqTy (PORT x) ty | (MINST xs) = No (portModuleInstNotEq)
    decEqTy (PORT x) ty | UNIT = No (portUnitNotEq)
    decEqTy (PORT x) ty | TYPE = No (portTypeNotEq)
    decEqTy (PORT x) ty | GATE = No (portGateNotEq)
    decEqTy (PORT x) ty | (GINST) = No (portGinstNotEq)

  decEqTy (MINST xs) ty with (ty)
    decEqTy (MINST xs) ty | (MODULE ys) = No (negEqSym moduleDeclmoduleInstNotEq)
    decEqTy (MINST xs) ty | DATA = No (negEqSym dataModuleInstNotEq)
    decEqTy (MINST xs) ty | CHAN = No (negEqSym chanModuleInstNotEq)
    decEqTy (MINST xs) ty | (PORT x) = No (negEqSym portModuleInstNotEq)
    decEqTy (MINST xs) ty | (MINST ys) with (decEq xs ys)
      decEqTy (MINST ys) ty | (MINST ys) | (Yes Refl) = Yes Refl
      decEqTy (MINST xs) ty | (MINST ys) | (No contra) = No (moduleInstParamsDiffer xs ys contra)

    decEqTy (MINST xs) ty | UNIT = No moduleInstUnitNotEq
    decEqTy (MINST xs) ty | TYPE = No moduleInstTypeNotEq
    decEqTy (MINST xs) ty | GATE = No moduleInstGateNotEq
    decEqTy (MINST xs) ty | (GINST) = No moduleInstGinstNotEq

  decEqTy UNIT ty with (ty)
    decEqTy UNIT ty | (MODULE xs) = No (negEqSym moduleUnitNotEq)
    decEqTy UNIT ty | DATA = No (negEqSym dataUnitNotEq)
    decEqTy UNIT ty | CHAN = No (negEqSym chanUnitNotEq)
    decEqTy UNIT ty | (PORT x) = No (negEqSym portUnitNotEq)
    decEqTy UNIT ty | (MINST xs) = No (negEqSym moduleInstUnitNotEq)
    decEqTy UNIT ty | UNIT = Yes Refl
    decEqTy UNIT ty | TYPE = No unitTypeNotEq
    decEqTy UNIT ty | GATE = No unitGateNotEq
    decEqTy UNIT ty | (GINST) = No unitGinstNotEq

  decEqTy TYPE ty with (ty)
    decEqTy TYPE ty | (MODULE xs) = No (negEqSym moduleTypeNotEq)
    decEqTy TYPE ty | DATA = No (negEqSym dataTypeNotEq)
    decEqTy TYPE ty | CHAN = No (negEqSym chanTypeNotEq)
    decEqTy TYPE ty | (PORT x) = No (negEqSym portTypeNotEq)
    decEqTy TYPE ty | (MINST xs) = No (negEqSym moduleInstTypeNotEq)
    decEqTy TYPE ty | UNIT = No (negEqSym unitTypeNotEq)
    decEqTy TYPE ty | TYPE = Yes Refl
    decEqTy TYPE ty | GATE = No typeGateNotEq
    decEqTy TYPE ty | (GINST) = No typeGinstNotEq

  decEqTy GATE ty with (ty)
    decEqTy GATE ty | (MODULE xs) = No (negEqSym moduleGateNotEq)
    decEqTy GATE ty | DATA = No (negEqSym dataGateNotEq)
    decEqTy GATE ty | CHAN = No (negEqSym chanGateNotEq)
    decEqTy GATE ty | (PORT x) = No (negEqSym portGateNotEq)
    decEqTy GATE ty | (MINST xs) = No (negEqSym moduleInstGateNotEq)
    decEqTy GATE ty | UNIT = No (negEqSym unitGateNotEq)
    decEqTy GATE ty | TYPE = No (negEqSym typeGateNotEq)
    decEqTy GATE ty | GATE = Yes Refl
    decEqTy GATE ty | (GINST) = No gateGinstNotEq

  decEqTy (GINST) ty with (ty)
    decEqTy (GINST) ty | (MODULE xs) = No (negEqSym moduleGinstNotEq)
    decEqTy (GINST) ty | DATA = No (negEqSym dataGinstNotEq)
    decEqTy (GINST) ty | CHAN = No (negEqSym chanGinstNotEq)
    decEqTy (GINST) ty | (PORT x) = No (negEqSym portGinstNotEq)
    decEqTy (GINST) ty | (MINST xs) = No (negEqSym moduleInstGinstNotEq)
    decEqTy (GINST) ty | UNIT = No (negEqSym unitGinstNotEq)
    decEqTy (GINST) ty | TYPE = No (negEqSym typeGinstNotEq)
    decEqTy (GINST) ty | GATE = No (negEqSym gateGinstNotEq)
    decEqTy (GINST) ty | (GINST) = Yes Refl

  export
  DecEq Ty where
   decEq = decEqTy

namespace Validity

  namespace Decl
    public export
    data ValidDecl : (expr : Ty) -> (type : Ty) -> Type where
       IsDeclM : ValidDecl (MODULE names) TYPE
       IsDeclD : ValidDecl DATA           TYPE

    -- Modules

    moduleCannotHaveTypeModule : ValidDecl (MODULE xs) (MODULE ys) -> Void
    moduleCannotHaveTypeModule IsDeclM impossible
    moduleCannotHaveTypeModule IsDeclD impossible

    moduleCannotHaveTypeData : ValidDecl (MODULE xs) DATA -> Void
    moduleCannotHaveTypeData IsDeclM impossible
    moduleCannotHaveTypeData IsDeclD impossible

    moduleCannotHaveTypeChan : ValidDecl (MODULE xs) CHAN -> Void
    moduleCannotHaveTypeChan IsDeclM impossible
    moduleCannotHaveTypeChan IsDeclD impossible

    moduleCannotHaveTypePort : ValidDecl (MODULE xs) (PORT x) -> Void
    moduleCannotHaveTypePort IsDeclM impossible
    moduleCannotHaveTypePort IsDeclD impossible

    moduleCannotHaveTypeMInst : ValidDecl (MODULE xs) (MINST ys) -> Void
    moduleCannotHaveTypeMInst IsDeclM impossible
    moduleCannotHaveTypeMInst IsDeclD impossible

    moduleCannotHaveTypeUnit : ValidDecl (MODULE xs) UNIT -> Void
    moduleCannotHaveTypeUnit IsDeclM impossible
    moduleCannotHaveTypeUnit IsDeclD impossible

    moduleCannotHaveTypeGate : ValidDecl (MODULE xs) GATE -> Void
    moduleCannotHaveTypeGate IsDeclM impossible
    moduleCannotHaveTypeGate IsDeclD impossible

    moduleCannotHaveTypeGinst : ValidDecl (MODULE xs) (GINST) -> Void
    moduleCannotHaveTypeGinst IsDeclM impossible
    moduleCannotHaveTypeGinst IsDeclD impossible

    -- Data

    dataCannotHaveTypeModule : ValidDecl DATA (MODULE xs) -> Void
    dataCannotHaveTypeModule IsDeclM impossible
    dataCannotHaveTypeModule IsDeclD impossible

    dataCannotHaveTypeData : ValidDecl DATA DATA -> Void
    dataCannotHaveTypeData IsDeclM impossible
    dataCannotHaveTypeData IsDeclD impossible

    dataCannotHaveTypeChan : ValidDecl DATA CHAN -> Void
    dataCannotHaveTypeChan IsDeclM impossible
    dataCannotHaveTypeChan IsDeclD impossible

    dataCannotHaveTypePort : ValidDecl DATA (PORT x) -> Void
    dataCannotHaveTypePort IsDeclM impossible
    dataCannotHaveTypePort IsDeclD impossible

    dataCannotHaveTypeMInst : ValidDecl DATA (MINST xs) -> Void
    dataCannotHaveTypeMInst IsDeclM impossible
    dataCannotHaveTypeMInst IsDeclD impossible

    dataCannotHaveTypeUnit : ValidDecl DATA UNIT -> Void
    dataCannotHaveTypeUnit IsDeclM impossible
    dataCannotHaveTypeUnit IsDeclD impossible

    dataCannotHaveTypeGate : ValidDecl DATA GATE -> Void
    dataCannotHaveTypeGate IsDeclM impossible
    dataCannotHaveTypeGate IsDeclD impossible

    dataCannotHaveTypeGinst : ValidDecl DATA (GINST) -> Void
    dataCannotHaveTypeGinst IsDeclM impossible
    dataCannotHaveTypeGinst IsDeclD impossible

    -- CHAN

    chanCannotBeDecl : ValidDecl CHAN type -> Void
    chanCannotBeDecl IsDeclM impossible
    chanCannotBeDecl IsDeclD impossible

    portCannotBeDecl : ValidDecl (PORT x) type -> Void
    portCannotBeDecl IsDeclM impossible
    portCannotBeDecl IsDeclD impossible

    minstsCannotBeDecl : ValidDecl (MINST xs) type -> Void
    minstsCannotBeDecl IsDeclM impossible
    minstsCannotBeDecl IsDeclD impossible

    unitCannotBeDecl : ValidDecl UNIT type -> Void
    unitCannotBeDecl IsDeclM impossible
    unitCannotBeDecl IsDeclD impossible

    typeCannotBeDecl : ValidDecl TYPE type -> Void
    typeCannotBeDecl IsDeclM impossible
    typeCannotBeDecl IsDeclD impossible

    gateCannotBeDecl : ValidDecl GATE type -> Void
    gateCannotBeDecl IsDeclM impossible
    gateCannotBeDecl IsDeclD impossible

    ginstCannotBeDecl : ValidDecl (GINST) type -> Void
    ginstCannotBeDecl IsDeclM impossible
    ginstCannotBeDecl IsDeclD impossible

    export
    validDecl : (expr : Ty)
             -> (type : Ty)
             -> Dec (ValidDecl expr type)
    validDecl (MODULE xs) (MODULE ys) = No moduleCannotHaveTypeModule
    validDecl (MODULE xs) DATA = No moduleCannotHaveTypeData
    validDecl (MODULE xs) CHAN = No moduleCannotHaveTypeChan
    validDecl (MODULE xs) (PORT x) = No moduleCannotHaveTypePort
    validDecl (MODULE xs) (MINST ys) = No moduleCannotHaveTypeMInst
    validDecl (MODULE xs) UNIT = No moduleCannotHaveTypeUnit
    validDecl (MODULE xs) TYPE = Yes IsDeclM
    validDecl (MODULE xs) GATE = No moduleCannotHaveTypeGate
    validDecl (MODULE xs) (GINST) = No moduleCannotHaveTypeGinst

    validDecl DATA (MODULE xs) = No dataCannotHaveTypeModule
    validDecl DATA DATA = No dataCannotHaveTypeData
    validDecl DATA CHAN = No dataCannotHaveTypeChan
    validDecl DATA (PORT x) = No dataCannotHaveTypePort
    validDecl DATA (MINST xs) = No dataCannotHaveTypeMInst
    validDecl DATA UNIT = No dataCannotHaveTypeUnit
    validDecl DATA TYPE = Yes IsDeclD
    validDecl DATA GATE = No dataCannotHaveTypeGate
    validDecl DATA (GINST) = No dataCannotHaveTypeGinst

    validDecl CHAN _ = No chanCannotBeDecl
    validDecl (PORT x) _ = No portCannotBeDecl
    validDecl (MINST xs) _ = No minstsCannotBeDecl
    validDecl UNIT _ = No unitCannotBeDecl
    validDecl TYPE _ = No typeCannotBeDecl
    validDecl GATE _ = No gateCannotBeDecl
    validDecl (GINST) _ = No ginstCannotBeDecl

  namespace LetBinding
    public export
    data ValidLet : (expr : Ty) -> (type : Ty) -> Type where
       IsLetMM : (prf :                 xs  =         ys)
                     -> ValidLet (MINST xs)   (MODULE ys)

       IsLetCD : ValidLet CHAN DATA

       IsLetGG : ValidLet (GINST) GATE

       IsLetDecl : ValidDecl expr ty
                -> ValidLet  expr ty

    -- Modules

    moduleCannotHaveTypeModuleLocal : ValidLet (MODULE xs) (MODULE ys) -> Void
    moduleCannotHaveTypeModuleLocal (IsLetDecl IsDeclM) impossible
    moduleCannotHaveTypeModuleLocal (IsLetDecl IsDeclD) impossible

    moduleCannotHaveTypeDataLocal : ValidLet (MODULE xs) DATA -> Void
    moduleCannotHaveTypeDataLocal (IsLetDecl IsDeclM) impossible
    moduleCannotHaveTypeDataLocal (IsLetDecl IsDeclD) impossible

    moduleCannotHaveTypeChanLocal :  ValidLet (MODULE xs) CHAN -> Void
    moduleCannotHaveTypeChanLocal (IsLetDecl IsDeclM) impossible
    moduleCannotHaveTypeChanLocal (IsLetDecl IsDeclD) impossible

    moduleCannotHaveTypePortLocal : ValidLet (MODULE xs) (PORT y) -> Void
    moduleCannotHaveTypePortLocal (IsLetDecl IsDeclM) impossible
    moduleCannotHaveTypePortLocal (IsLetDecl IsDeclD) impossible

    moduleCannotHaveTypeMInstLocal : ValidLet (MODULE xs) (MINST ys) -> Void
    moduleCannotHaveTypeMInstLocal (IsLetDecl IsDeclM) impossible
    moduleCannotHaveTypeMInstLocal (IsLetDecl IsDeclD) impossible

    moduleCannotHaveTypeUnitLocal : ValidLet (MODULE xs) UNIT -> Void
    moduleCannotHaveTypeUnitLocal (IsLetDecl IsDeclM) impossible
    moduleCannotHaveTypeUnitLocal (IsLetDecl IsDeclD) impossible

    moduleCannotHaveTypeGateLocal : ValidLet (MODULE xs) GATE -> Void
    moduleCannotHaveTypeGateLocal (IsLetDecl IsDeclM) impossible
    moduleCannotHaveTypeGateLocal (IsLetDecl IsDeclD) impossible

    moduleCannotHaveTypeGInstLocal : ValidLet (MODULE xs) (GINST) -> Void
    moduleCannotHaveTypeGInstLocal (IsLetDecl IsDeclM) impossible
    moduleCannotHaveTypeGInstLocal (IsLetDecl IsDeclD) impossible

    -- Data

    dataCannotHaveTypeModuleLocal : ValidLet DATA (MODULE xs) -> Void
    dataCannotHaveTypeModuleLocal (IsLetDecl IsDeclM) impossible
    dataCannotHaveTypeModuleLocal (IsLetDecl IsDeclD) impossible

    dataCannotHaveTypeDataLocal : ValidLet DATA DATA -> Void
    dataCannotHaveTypeDataLocal (IsLetDecl IsDeclM) impossible
    dataCannotHaveTypeDataLocal (IsLetDecl IsDeclD) impossible

    dataCannotHaveTypeChanLocal : ValidLet DATA CHAN -> Void
    dataCannotHaveTypeChanLocal (IsLetDecl IsDeclM) impossible
    dataCannotHaveTypeChanLocal (IsLetDecl IsDeclD) impossible

    dataCannotHaveTypePortLocal : ValidLet DATA (PORT y) -> Void
    dataCannotHaveTypePortLocal (IsLetDecl IsDeclM) impossible
    dataCannotHaveTypePortLocal (IsLetDecl IsDeclD) impossible

    dataCannotHaveTypeMInstLocal : ValidLet DATA (MINST xs) -> Void
    dataCannotHaveTypeMInstLocal (IsLetDecl IsDeclM) impossible
    dataCannotHaveTypeMInstLocal (IsLetDecl IsDeclD) impossible

    dataCannotHaveTypeUnitLocal : ValidLet DATA UNIT -> Void
    dataCannotHaveTypeUnitLocal (IsLetDecl IsDeclM) impossible
    dataCannotHaveTypeUnitLocal (IsLetDecl IsDeclD) impossible

    dataCannotHaveTypeGateLocal : ValidLet DATA GATE -> Void
    dataCannotHaveTypeGateLocal (IsLetDecl IsDeclM) impossible
    dataCannotHaveTypeGateLocal (IsLetDecl IsDeclD) impossible

    dataCannotHaveTypeGInstLocal : ValidLet DATA (GINST) -> Void
    dataCannotHaveTypeGInstLocal (IsLetDecl IsDeclM) impossible
    dataCannotHaveTypeGInstLocal (IsLetDecl IsDeclD) impossible

    -- Chan

    chanCannotHaveTypeType : ValidLet CHAN TYPE -> Void
    chanCannotHaveTypeType (IsLetDecl IsDeclM) impossible
    chanCannotHaveTypeType (IsLetDecl IsDeclD) impossible

    chanCannotHaveTypeModule : ValidLet CHAN (MODULE xs) -> Void
    chanCannotHaveTypeModule (IsLetDecl IsDeclM) impossible
    chanCannotHaveTypeModule (IsLetDecl IsDeclD) impossible

    chanCannotHaveTypeChan : ValidLet CHAN CHAN -> Void
    chanCannotHaveTypeChan (IsLetDecl IsDeclM) impossible
    chanCannotHaveTypeChan (IsLetDecl IsDeclD) impossible

    chanCannotHaveTypePort : ValidLet CHAN (PORT y) -> Void
    chanCannotHaveTypePort (IsLetDecl IsDeclM) impossible
    chanCannotHaveTypePort (IsLetDecl IsDeclD) impossible

    chanCannotHaveTypeMInst : ValidLet CHAN (MINST xs) -> Void
    chanCannotHaveTypeMInst (IsLetDecl IsDeclM) impossible
    chanCannotHaveTypeMInst (IsLetDecl IsDeclD) impossible

    chanCannotHaveTypeUnit : ValidLet CHAN UNIT -> Void
    chanCannotHaveTypeUnit (IsLetDecl IsDeclM) impossible
    chanCannotHaveTypeUnit (IsLetDecl IsDeclD) impossible

    chanCannotHaveTypeGateLocal : ValidLet CHAN GATE -> Void
    chanCannotHaveTypeGateLocal (IsLetDecl IsDeclM) impossible
    chanCannotHaveTypeGateLocal (IsLetDecl IsDeclD) impossible

    chanCannotHaveTypeGInstLocal : ValidLet CHAN (GINST) -> Void
    chanCannotHaveTypeGInstLocal (IsLetDecl IsDeclM) impossible
    chanCannotHaveTypeGInstLocal (IsLetDecl IsDeclD) impossible

    -- Ports

    portCannotHaveTypeModule : ValidLet (PORT y) (MODULE xs) -> Void
    portCannotHaveTypeModule (IsLetDecl IsDeclM) impossible
    portCannotHaveTypeModule (IsLetDecl IsDeclD) impossible

    portCannotHaveTypeData : ValidLet (PORT y) DATA -> Void
    portCannotHaveTypeData (IsLetDecl IsDeclM) impossible
    portCannotHaveTypeData (IsLetDecl IsDeclD) impossible

    portCannotHaveTypeChan : ValidLet (PORT y) CHAN -> Void
    portCannotHaveTypeChan (IsLetDecl IsDeclM) impossible
    portCannotHaveTypeChan (IsLetDecl IsDeclD) impossible

    portCannotHaveTypePort : ValidLet (PORT y) (PORT x) -> Void
    portCannotHaveTypePort (IsLetDecl IsDeclM) impossible
    portCannotHaveTypePort (IsLetDecl IsDeclD) impossible

    portCannotHaveTypeMInst : ValidLet (PORT y) (MINST xs) -> Void
    portCannotHaveTypeMInst (IsLetDecl IsDeclM) impossible
    portCannotHaveTypeMInst (IsLetDecl IsDeclD) impossible

    portCannotHaveTypeUnit : ValidLet (PORT y) UNIT -> Void
    portCannotHaveTypeUnit (IsLetDecl IsDeclM) impossible
    portCannotHaveTypeUnit(IsLetDecl IsDeclD) impossible

    portCannotHaveTypeType : ValidLet (PORT y) TYPE -> Void
    portCannotHaveTypeType (IsLetDecl IsDeclM) impossible
    portCannotHaveTypeType (IsLetDecl IsDeclD) impossible

    portCannotHaveTypeGateLocal : ValidLet (PORT p) GATE -> Void
    portCannotHaveTypeGateLocal (IsLetDecl IsDeclM) impossible
    portCannotHaveTypeGateLocal (IsLetDecl IsDeclD) impossible

    portCannotHaveTypeGInstLocal : ValidLet (PORT p) (GINST) -> Void
    portCannotHaveTypeGInstLocal (IsLetDecl IsDeclM) impossible
    portCannotHaveTypeGInstLocal (IsLetDecl IsDeclD) impossible

    -- MINST

    minstCannotHaveTypeData : ValidLet (MINST xs) DATA -> Void
    minstCannotHaveTypeData (IsLetDecl IsDeclM) impossible
    minstCannotHaveTypeData (IsLetDecl IsDeclD) impossible

    minstCannotHaveTypeChan : ValidLet (MINST xs) CHAN -> Void
    minstCannotHaveTypeChan (IsLetDecl IsDeclM) impossible
    minstCannotHaveTypeChan (IsLetDecl IsDeclD) impossible

    minstCannotHaveTypePort : ValidLet (MINST xs) (PORT x) -> Void
    minstCannotHaveTypePort (IsLetDecl IsDeclM) impossible
    minstCannotHaveTypePort (IsLetDecl IsDeclD) impossible

    minstCannotHaveTypeMInst : ValidLet (MINST xs) (MINST ys) -> Void
    minstCannotHaveTypeMInst (IsLetDecl IsDeclM) impossible
    minstCannotHaveTypeMInst (IsLetDecl IsDeclD) impossible

    minstCannotHaveTypeUnit : ValidLet (MINST xs) UNIT -> Void
    minstCannotHaveTypeUnit (IsLetDecl IsDeclM) impossible
    minstCannotHaveTypeUnit(IsLetDecl IsDeclD) impossible

    minstCannotHaveTypeType : ValidLet (MINST xs) TYPE -> Void
    minstCannotHaveTypeType (IsLetDecl IsDeclM) impossible
    minstCannotHaveTypeType (IsLetDecl IsDeclD) impossible

    minstCannotHaveTypeGateLocal : ValidLet (MINST xs) GATE -> Void
    minstCannotHaveTypeGateLocal (IsLetDecl IsDeclM) impossible
    minstCannotHaveTypeGateLocal (IsLetDecl IsDeclD) impossible

    minstCannotHaveTypeGInstLocal : ValidLet (MINST xs) (GINST) -> Void
    minstCannotHaveTypeGInstLocal (IsLetDecl IsDeclM) impossible
    minstCannotHaveTypeGInstLocal (IsLetDecl IsDeclD) impossible

    -- Unit
    unitCannotHaveTypeModule : ValidLet UNIT (MODULE xs) -> Void
    unitCannotHaveTypeModule (IsLetDecl IsDeclM) impossible
    unitCannotHaveTypeModule (IsLetDecl IsDeclD) impossible

    unitCannotHaveTypeData : ValidLet UNIT DATA -> Void
    unitCannotHaveTypeData (IsLetDecl IsDeclM) impossible
    unitCannotHaveTypeData (IsLetDecl IsDeclD) impossible

    unitCannotHaveTypeChan : ValidLet UNIT CHAN -> Void
    unitCannotHaveTypeChan (IsLetDecl IsDeclM) impossible
    unitCannotHaveTypeChan (IsLetDecl IsDeclD) impossible

    unitCannotHaveTypePort : ValidLet UNIT (PORT x) -> Void
    unitCannotHaveTypePort (IsLetDecl IsDeclM) impossible
    unitCannotHaveTypePort (IsLetDecl IsDeclD) impossible

    unitCannotHaveTypeMInst : ValidLet UNIT (MINST xs) -> Void
    unitCannotHaveTypeMInst (IsLetDecl IsDeclM) impossible
    unitCannotHaveTypeMInst (IsLetDecl IsDeclD) impossible

    unitCannotHaveTypeUnit : ValidLet UNIT UNIT -> Void
    unitCannotHaveTypeUnit (IsLetDecl IsDeclM) impossible
    unitCannotHaveTypeUnit(IsLetDecl IsDeclD) impossible

    unitCannotHaveTypeType : ValidLet UNIT TYPE -> Void
    unitCannotHaveTypeType (IsLetDecl IsDeclM) impossible
    unitCannotHaveTypeType (IsLetDecl IsDeclD) impossible

    unitCannotHaveTypeGateLocal : ValidLet UNIT GATE -> Void
    unitCannotHaveTypeGateLocal (IsLetDecl IsDeclM) impossible
    unitCannotHaveTypeGateLocal (IsLetDecl IsDeclD) impossible

    unitCannotHaveTypeGInstLocal : ValidLet UNIT (GINST) -> Void
    unitCannotHaveTypeGInstLocal (IsLetDecl IsDeclM) impossible
    unitCannotHaveTypeGInstLocal (IsLetDecl IsDeclD) impossible

    -- TYPE

    typeCannotHaveTypeModule : ValidLet TYPE (MODULE xs) -> Void
    typeCannotHaveTypeModule (IsLetDecl IsDeclM) impossible
    typeCannotHaveTypeModule (IsLetDecl IsDeclD) impossible

    typeCannotHaveTypeData : ValidLet TYPE DATA -> Void
    typeCannotHaveTypeData (IsLetDecl IsDeclM) impossible
    typeCannotHaveTypeData (IsLetDecl IsDeclD) impossible

    typeCannotHaveTypeChan : ValidLet TYPE CHAN -> Void
    typeCannotHaveTypeChan (IsLetDecl IsDeclM) impossible
    typeCannotHaveTypeChan (IsLetDecl IsDeclD) impossible

    typeCannotHaveTypePort : ValidLet TYPE (PORT x) -> Void
    typeCannotHaveTypePort (IsLetDecl IsDeclM) impossible
    typeCannotHaveTypePort (IsLetDecl IsDeclD) impossible

    typeCannotHaveTypeMInst : ValidLet TYPE (MINST xs) -> Void
    typeCannotHaveTypeMInst (IsLetDecl IsDeclM) impossible
    typeCannotHaveTypeMInst (IsLetDecl IsDeclD) impossible

    typeCannotHaveTypeUnit : ValidLet TYPE UNIT -> Void
    typeCannotHaveTypeUnit (IsLetDecl IsDeclM) impossible
    typeCannotHaveTypeUnit(IsLetDecl IsDeclD) impossible

    typeCannotHaveTypeType : ValidLet TYPE TYPE -> Void
    typeCannotHaveTypeType (IsLetDecl IsDeclM) impossible
    typeCannotHaveTypeType (IsLetDecl IsDeclD) impossible

    typeCannotHaveTypeGateLocal : ValidLet TYPE GATE -> Void
    typeCannotHaveTypeGateLocal (IsLetDecl IsDeclM) impossible
    typeCannotHaveTypeGateLocal (IsLetDecl IsDeclD) impossible

    typeCannotHaveTypeGInstLocal : ValidLet TYPE (GINST) -> Void
    typeCannotHaveTypeGInstLocal (IsLetDecl IsDeclM) impossible
    typeCannotHaveTypeGInstLocal (IsLetDecl IsDeclD) impossible

    -- Gates

    gateCannotHaveTypeModuleLocal : ValidLet GATE (MODULE xs) -> Void
    gateCannotHaveTypeModuleLocal (IsLetDecl IsDeclM) impossible
    gateCannotHaveTypeModuleLocal (IsLetDecl IsDeclD) impossible

    gateCannotHaveTypeDataLocal : ValidLet GATE DATA -> Void
    gateCannotHaveTypeDataLocal (IsLetDecl IsDeclM) impossible
    gateCannotHaveTypeDataLocal (IsLetDecl IsDeclD) impossible

    gateCannotHaveTypeChanLocal : ValidLet GATE CHAN -> Void
    gateCannotHaveTypeChanLocal (IsLetDecl IsDeclM) impossible
    gateCannotHaveTypeChanLocal (IsLetDecl IsDeclD) impossible

    gateCannotHaveTypePortLocal : ValidLet GATE (PORT y) -> Void
    gateCannotHaveTypePortLocal (IsLetDecl IsDeclM) impossible
    gateCannotHaveTypePortLocal (IsLetDecl IsDeclD) impossible

    gateCannotHaveTypeMInstLocal : ValidLet GATE (MINST xs) -> Void
    gateCannotHaveTypeMInstLocal (IsLetDecl IsDeclM) impossible
    gateCannotHaveTypeMInstLocal (IsLetDecl IsDeclD) impossible

    gateCannotHaveTypeUnitLocal : ValidLet GATE UNIT -> Void
    gateCannotHaveTypeUnitLocal (IsLetDecl IsDeclM) impossible
    gateCannotHaveTypeUnitLocal (IsLetDecl IsDeclD) impossible

    gateCannotHaveTypeGateLocal : ValidLet GATE GATE -> Void
    gateCannotHaveTypeGateLocal (IsLetDecl IsDeclM) impossible
    gateCannotHaveTypeGateLocal (IsLetDecl IsDeclD) impossible

    gateCannotHaveTypeGInstLocal : ValidLet GATE (GINST) -> Void
    gateCannotHaveTypeGInstLocal (IsLetDecl IsDeclM) impossible
    gateCannotHaveTypeGInstLocal (IsLetDecl IsDeclD) impossible

    gateCannotHaveTypeTypeLocal : ValidLet GATE TYPE -> Void
    gateCannotHaveTypeTypeLocal (IsLetDecl IsDeclM) impossible
    gateCannotHaveTypeTypeLocal (IsLetDecl IsDeclD) impossible

    -- GInst

    ginstCannotHaveTypeModuleLocal : ValidLet (GINST) (MODULE xs) -> Void
    ginstCannotHaveTypeModuleLocal (IsLetDecl IsDeclM) impossible
    ginstCannotHaveTypeModuleLocal (IsLetDecl IsDeclD) impossible

    ginstCannotHaveTypeDataLocal : ValidLet (GINST) DATA -> Void
    ginstCannotHaveTypeDataLocal (IsLetDecl IsDeclM) impossible
    ginstCannotHaveTypeDataLocal (IsLetDecl IsDeclD) impossible

    ginstCannotHaveTypeChanLocal : ValidLet (GINST) CHAN -> Void
    ginstCannotHaveTypeChanLocal (IsLetDecl IsDeclM) impossible
    ginstCannotHaveTypeChanLocal (IsLetDecl IsDeclD) impossible

    ginstCannotHaveTypePortLocal : ValidLet (GINST) (PORT y) -> Void
    ginstCannotHaveTypePortLocal (IsLetDecl IsDeclM) impossible
    ginstCannotHaveTypePortLocal (IsLetDecl IsDeclD) impossible

    ginstCannotHaveTypeMInstLocal : ValidLet (GINST) (MINST xs) -> Void
    ginstCannotHaveTypeMInstLocal (IsLetDecl IsDeclM) impossible
    ginstCannotHaveTypeMInstLocal (IsLetDecl IsDeclD) impossible

    ginstCannotHaveTypeUnitLocal : ValidLet (GINST) UNIT -> Void
    ginstCannotHaveTypeUnitLocal (IsLetDecl IsDeclM) impossible
    ginstCannotHaveTypeUnitLocal (IsLetDecl IsDeclD) impossible

    ginstCannotHaveTypeTypeLocal : ValidLet (GINST) TYPE -> Void
    ginstCannotHaveTypeTypeLocal (IsLetDecl IsDeclM) impossible
    ginstCannotHaveTypeTypeLocal (IsLetDecl IsDeclD) impossible

    ginstCannotHaveTypeGInstLocal : ValidLet (GINST) (GINST) -> Void
    ginstCannotHaveTypeGInstLocal (IsLetDecl IsDeclM) impossible
    ginstCannotHaveTypeGInstLocal (IsLetDecl IsDeclD) impossible

    -- Misc
    minstAndModulesHaveDiffNames : (f : (xs = ys) -> Void)
                                -> ValidLet (MINST xs) (MODULE ys)
                                -> Void
    minstAndModulesHaveDiffNames f (IsLetMM Refl) = f Refl
    minstAndModulesHaveDiffNames _ (IsLetDecl IsDeclM) impossible
    minstAndModulesHaveDiffNames _ (IsLetDecl IsDeclD) impossible

    export
    validLet : (expr : Ty)
            -> (type : Ty)
            -> Dec (ValidLet expr type)
    validLet (MODULE xs) (MODULE ys) = No moduleCannotHaveTypeModuleLocal
    validLet (MODULE xs) DATA        = No moduleCannotHaveTypeDataLocal
    validLet (MODULE xs) CHAN        = No moduleCannotHaveTypeChanLocal
    validLet (MODULE xs) (PORT x)    = No moduleCannotHaveTypePortLocal
    validLet (MODULE xs) (MINST ys)  = No moduleCannotHaveTypeMInstLocal
    validLet (MODULE xs) UNIT        = No moduleCannotHaveTypeUnitLocal
    validLet (MODULE xs) TYPE        = Yes (IsLetDecl IsDeclM)
    validLet (MODULE xs) GATE        = No moduleCannotHaveTypeGateLocal
    validLet (MODULE xs) (GINST) = No moduleCannotHaveTypeGInstLocal

    validLet DATA (MODULE xs) = No (dataCannotHaveTypeModuleLocal)
    validLet DATA DATA        = No (dataCannotHaveTypeDataLocal)
    validLet DATA CHAN        = No (dataCannotHaveTypeChanLocal)
    validLet DATA (PORT x)    = No (dataCannotHaveTypePortLocal)
    validLet DATA (MINST xs)  = No (dataCannotHaveTypeMInstLocal)
    validLet DATA UNIT        = No (dataCannotHaveTypeUnitLocal)
    validLet DATA TYPE        = Yes (IsLetDecl IsDeclD)
    validLet DATA GATE         = No dataCannotHaveTypeGateLocal
    validLet DATA (GINST) = No dataCannotHaveTypeGInstLocal

    validLet CHAN (MODULE xs) = No (chanCannotHaveTypeModule)
    validLet CHAN DATA        = Yes IsLetCD
    validLet CHAN CHAN        = No (chanCannotHaveTypeChan)
    validLet CHAN (PORT x)    = No (chanCannotHaveTypePort)
    validLet CHAN (MINST xs)  = No (chanCannotHaveTypeMInst)
    validLet CHAN UNIT        = No (chanCannotHaveTypeUnit)
    validLet CHAN TYPE        = No (chanCannotHaveTypeType)
    validLet CHAN GATE         = No chanCannotHaveTypeGateLocal
    validLet CHAN (GINST) = No chanCannotHaveTypeGInstLocal

    validLet (PORT x) (MODULE xs) =  No portCannotHaveTypeModule
    validLet (PORT x) DATA        =  No portCannotHaveTypeData
    validLet (PORT x) CHAN        =  No (portCannotHaveTypeChan)
    validLet (PORT x) (PORT y)    =  No portCannotHaveTypePort
    validLet (PORT x) (MINST xs)  =  No portCannotHaveTypeMInst
    validLet (PORT x) UNIT        =  No portCannotHaveTypeUnit
    validLet (PORT x) TYPE        =  No portCannotHaveTypeType
    validLet (PORT x) GATE         = No portCannotHaveTypeGateLocal
    validLet (PORT x) (GINST) = No portCannotHaveTypeGInstLocal

    validLet (MINST xs) (MODULE ys) with (decEq xs ys)
      validLet (MINST ys) (MODULE ys) | (Yes Refl) = Yes (IsLetMM Refl)
      validLet (MINST xs) (MODULE ys) | (No contra) = No (minstAndModulesHaveDiffNames contra)

    validLet (MINST xs) DATA       =  No minstCannotHaveTypeData
    validLet (MINST xs) CHAN       =  No minstCannotHaveTypeChan
    validLet (MINST xs) (PORT x)   =  No minstCannotHaveTypePort
    validLet (MINST xs) (MINST ys) =  No minstCannotHaveTypeMInst
    validLet (MINST xs) UNIT       =  No minstCannotHaveTypeUnit
    validLet (MINST xs) TYPE       =  No minstCannotHaveTypeType
    validLet (MINST xs) GATE         = No minstCannotHaveTypeGateLocal
    validLet (MINST xs) (GINST) = No minstCannotHaveTypeGInstLocal

    validLet UNIT (MODULE xs) = No unitCannotHaveTypeModule
    validLet UNIT DATA        = No unitCannotHaveTypeData
    validLet UNIT CHAN        = No unitCannotHaveTypeChan
    validLet UNIT (PORT x)    = No unitCannotHaveTypePort
    validLet UNIT (MINST xs)  = No unitCannotHaveTypeMInst
    validLet UNIT UNIT        = No unitCannotHaveTypeUnit
    validLet UNIT TYPE        = No unitCannotHaveTypeType
    validLet UNIT GATE         = No unitCannotHaveTypeGateLocal
    validLet UNIT (GINST) = No unitCannotHaveTypeGInstLocal

    validLet TYPE (MODULE xs) = No typeCannotHaveTypeModule
    validLet TYPE DATA        = No typeCannotHaveTypeData
    validLet TYPE CHAN        = No typeCannotHaveTypeChan
    validLet TYPE (PORT y)    = No typeCannotHaveTypePort
    validLet TYPE (MINST xs)  = No typeCannotHaveTypeMInst
    validLet TYPE UNIT        = No typeCannotHaveTypeUnit
    validLet TYPE TYPE        = No typeCannotHaveTypeType
    validLet TYPE GATE         = No typeCannotHaveTypeGateLocal
    validLet TYPE (GINST) = No typeCannotHaveTypeGInstLocal

    validLet GATE (MODULE xs)   = No gateCannotHaveTypeModuleLocal
    validLet GATE DATA          = No gateCannotHaveTypeDataLocal
    validLet GATE CHAN          = No gateCannotHaveTypeChanLocal
    validLet GATE (PORT y)      = No gateCannotHaveTypePortLocal
    validLet GATE (MINST xs)    = No gateCannotHaveTypeMInstLocal
    validLet GATE UNIT          = No gateCannotHaveTypeUnitLocal
    validLet GATE TYPE          = No gateCannotHaveTypeTypeLocal
    validLet GATE GATE          = No gateCannotHaveTypeGateLocal
    validLet GATE (GINST) = No gateCannotHaveTypeGInstLocal

    validLet (GINST) (MODULE xs)     = No ginstCannotHaveTypeModuleLocal
    validLet (GINST) DATA            = No ginstCannotHaveTypeDataLocal
    validLet (GINST) CHAN            = No ginstCannotHaveTypeChanLocal
    validLet (GINST) (PORT y)        = No ginstCannotHaveTypePortLocal
    validLet (GINST) (MINST xs)      = No ginstCannotHaveTypeMInstLocal
    validLet (GINST) UNIT            = No ginstCannotHaveTypeUnitLocal
    validLet (GINST) TYPE            = No ginstCannotHaveTypeTypeLocal
    validLet (GINST) GATE            = Yes IsLetGG
    validLet (GINST) GINST           = No ginstCannotHaveTypeGInstLocal

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

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Control.Monad.Logic.Logic

import public Control.Monad.Logic.Interface
import Control.Monad.Identity
import Control.Monad.Trans

-- import Data.Colist
import Data.List.Lazy -- this has more functions than `Data/Colist.idr`

public export
record LogicT (m : Type -> Type) (a : Type) where
  constructor MkLogicT
  runLogicT : forall r. (cons : a -> m r -> m r) -> (nil : m r) -> m r

public export
Logic : (a : Type) -> Type
Logic = LogicT Identity

public export
runLogic : Logic a -> (a -> r -> r) -> r -> r
runLogic xz cons nil = runIdentity $ runLogic xz (map . cons) (Id nil)

||| possibly useless due to cases of infinite branching in underlying monads' unfavorable control flow
public export
observeT : Applicative m => LogicT m a -> m (LazyList a)
observeT xz = runLogicT xz (\x, xs => map (\xs_ => x :: xs_) xs) (pure [])

public export
observe : Logic a -> LazyList a
observe = runIdentity . observeT

public export
Functor (LogicT m) where
  map f xz = MkLogicT $ \cons, nil => runLogicT xz (\x, xs => cons (f x) xs) nil

public export
Applicative (LogicT m) where
  pure x = MkLogicT $ \cons, nil => cons x nil
  fz <*> xz = MkLogicT $ \cons, nil => runLogicT fz (\f, fs => runLogicT xz (\x, xs => cons (f x) xs) fs) nil

public export
Monad (LogicT m) where
  act >>= react = MkLogicT $ \cons, nil => runLogicT act (\r, rs => runLogicT (react r) cons rs) nil

public export
Alternative (LogicT m) where
  empty = MkLogicT $ \cons, nil => nil
  xz <|> yz = MkLogicT $ \cons, nil => runLogicT xz cons (runLogicT yz cons nil)

public export
MonadTrans LogicT where
  lift xz = MkLogicT $ \cons, nil => xz >>= \x => cons x nil

export
HasIO m => HasIO (LogicT m) where
  liftIO = lift . liftIO

public export
Monad m => MonadLogic (LogicT m) where
  split xz = lift $ runLogicT xz (\cons, nil => pure $ Just (cons, lift nil >>= reflect)) (pure Nothing)


text:
{-#  OPTIONS --type-in-type #-}
module Bias

import IdrisPrelude

myFun : (a : Type) -> a -> a -> a -> Nat
myFun a x y z = Zero

myApp1 : Nat
myApp1 = myFun _ Zero Zero (IdrisPrelude.Nil Nat)

myApp2 : Nat
myApp2 = myFun _ (Nil Nat) Zero Zero

max_stars_repo_name: JoeyEremondi/lambda-pi-constraint

max_issues_repo_name: JoeyEremondi/lambda-pi-constraint

max_forks_repo_name: JoeyEremondi/lambda-pi-constraint


text:
module ArithTotal

import Data.Primitives.Views
import System

%default total

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

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

data Fuel = Dry | More (Lazy Fuel)

run : Fuel -> InfIO -> IO ()
run Dry y = putStrLn "Out of fuel."
run (More x) (Do y f) = do res <- y
                           run x (f res)

quiz : Stream Int -> (score : Nat) -> InfIO
quiz (v1 :: v2 :: vs) score =
  do putStrLn $ "Score so far: " ++ show score
     putStr $ show v1 ++ " * " ++ show v2 ++ "? "
     answer <- getLine
     case cast answer == v1 * v2 of
          False => do putStrLn $ "Incorrect. Answer is: " ++ show (v1 * v2)
                      quiz vs score
          True => do putStrLn $ "Correct!"
                     quiz vs (score + 1)

randoms : Int -> Stream Int
randoms seed = let seed' = 163525 * seed + 1013904223 in
                   (seed' `shiftR` 2) :: randoms seed'

arithInputs : Int -> Stream Int
arithInputs seed = map bound (randoms seed)
  where
    bound : Int -> Int
    bound x with (divides x 12)
      bound ((12 * div) + rem) | (DivBy prf) = abs rem + 1

partial
forever : Fuel
forever = More forever

partial
main : IO ()
main = do seed <- time
          run forever $ quiz (arithInputs $ fromInteger seed) 0

-- 11.2 Exercise
totalREPL : (prompt : String) -> (action : String -> String) -> InfIO
totalREPL prompt action = do putStrLn prompt
                             res <- getLine
                             putStrLn $ action res
                             totalREPL prompt action

max_stars_repo_path: Chapter 11/ArithTotal.idr

max_issues_repo_path: Chapter 11/ArithTotal.idr

max_forks_repo_path: Chapter 11/ArithTotal.idr


text:
nil_app : (l : List Nat) -> ([] ++ l) = l
nil_app l = Refl

tl : List Nat -> List Nat
tl [] = []
tl (x :: xs) = xs

tl_length_pred : (l : List Nat) -> pred (length l) = length (tl l)
tl_length_pred [] = Refl
tl_length_pred (x :: xs) = Refl

app_assoc : (l1, l2, l3 : List Nat) -> ((l1 ++ l2) ++ l3) = (l1 ++ (l2 ++ l3))
app_assoc [] l2 l3 = Refl
app_assoc (x :: xs) l2 l3 = rewrite app_assoc xs l2 l3 in Refl

rev : (l : List Nat) -> List Nat
rev [] = []
rev (x :: xs) = (rev xs) ++ [x]

test_rev1 : rev [1, 2, 3] = [3, 2, 1]
test_rev1 = Refl

test_rev2 : rev [] = []
test_rev2 = Refl

app_length : (l1, l2 : List Nat) -> length (l1 ++ l2) = (length l1) + (length l2)
app_length [] l2 = Refl
app_length (x :: xs) l2 = rewrite app_length xs l2 in Refl

rev_length_firsttry : (l : List Nat) -> length (rev l) = length l
rev_length_firsttry [] = Refl
rev_length_firsttry (x :: xs) =
    rewrite app_length (rev xs) [x]
        in rewrite plusCommutative (length (rev xs)) 1
            in rewrite rev_length_firsttry xs
                in Refl

app_nil_r : (l : List Nat) -> (l ++ []) = l
app_nil_r [] = Refl
app_nil_r (x :: xs) = rewrite app_nil_r xs in Refl

rev_app_distr : (l1, l2 : List Nat) -> rev (l1 ++ l2) = (rev l2) ++ (rev l1)
rev_app_distr [] l2 =
    rewrite sym (app_nil_r l2)
        in rewrite app_nil_r (rev (l2 ++ []))
            in Refl
rev_app_distr (x :: xs) l2 =
    rewrite rev_app_distr xs l2
        in rewrite app_assoc (rev l2) (rev xs) [x]
            in Refl

rev_involutive : (l : List Nat) -> rev (rev l) = l
rev_involutive [] = Refl
rev_involutive (x :: xs) =
    rewrite rev_app_distr (rev xs) [x]
        in rewrite rev_involutive xs
            in Refl

app_assoc4 : (l1, l2, l3, l4 : List Nat) -> (l1 ++ (l2 ++ (l3 ++ l4))) = ((l1 ++ l2) ++ l3) ++ l4
app_assoc4 [] l2 l3 l4 = rewrite app_assoc l2 l3 l4 in Refl
app_assoc4 (x :: xs) l2 l3 l4 = rewrite app_assoc4 xs l2 l3 l4 in Refl

nonzeros : List Nat -> List Nat
nonzeros [] = []
nonzeros (Z :: xs) = nonzeros xs
nonzeros (k :: xs) = k :: nonzeros xs

nonzeros_app : (l1, l2 : List Nat) -> nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2)
nonzeros_app [] l2 = Refl
nonzeros_app (Z :: xs) l2 = rewrite nonzeros_app xs l2 in Refl
nonzeros_app ((S k) :: xs) l2 = rewrite nonzeros_app xs l2 in Refl

beq_list_nat : (l1, l2 : List Nat) -> Bool
beq_list_nat [] [] = True
beq_list_nat (x :: xs) (y :: ys) = x == y && beq_list_nat xs ys
beq_list_nat xs ys = False

test_beq_list_nat1 : beq_list_nat [] [] = True
test_beq_list_nat1 = Refl

test_beq_list_nat2 : beq_list_nat [1, 2, 3] [1, 2, 3] = True
test_beq_list_nat2 = Refl

test_beq_list_nat3 : beq_list_nat [1, 2, 3] [1, 2, 4] = False
test_beq_list_nat3 = Refl

beq_list_nat_refl : (l : List Nat) -> True = beq_list_nat l l
beq_list_nat_refl [] = Refl
beq_list_nat_refl (Z :: xs) = rewrite beq_list_nat_refl xs in Refl
beq_list_nat_refl ((S k) :: xs) =
    rewrite beq_list_nat_refl (k :: xs) in
        Refl

total
rev_injective : (l1, l2 : List Nat) -> rev l1 = rev l2 -> l1 = l2
rev_injective [] [] prf = Refl
rev_injective xs ys prf =
    rewrite sym $ rev_involutive xs in
        rewrite sym $ rev_involutive ys in
            rewrite prf in
                Refl


text:
module Mmhelloworld.IdrisSpringBoot.Web.Bind.Annotation

import IdrisJvm.IO

%access public export

term syntax "<@RequestMapping>" [attrs] = <@> "org/springframework/web/bind/annotation/RequestMapping" attrs
term syntax "<@RestController>" [attrs] = <@> "org/springframework/web/bind/annotation/RestController" attrs
term syntax "<@RequestBody>" [attrs] = <@> "org/springframework/web/bind/annotation/RequestBody" attrs
term syntax "<@Param>" [attrs] = <@> "org/springframework/web/bind/annotation/Param" attrs
term syntax "<@RequestMethod>" [method] = <@enum> "org/springframework/web/bind/annotation/RequestMethod" method

max_stars_repo_name: mmhelloworld/idris-spring-boot

max_issues_repo_name: mmhelloworld/idris-spring-boot

max_forks_repo_name: mmhelloworld/idris-spring-boot


text:
module Main

main : IO ()
main = do
    let x = "aaa"
    putStrLn $ show x
    putStrLn $ show "dsa"


text:
module Examples.CSS.Colors

import Data.Maybe
import Text.CSS

export
lightest_grey : Color
lightest_grey = hsl 0 0 90

export
lighter_grey : Color
lighter_grey = hsl 0 0 70

export
light_grey : Color
light_grey = hsl 0 0 50

export
dark_grey : Color
dark_grey = hsl 0 0 30

export
darker_grey : Color
darker_grey = hsl 0 0 10

export
base100 : Color
base100 = rgb 230 115 0

export
base80 : Color
base80 = rgb 230 138 46

export
base60 : Color
base60 = rgb 230 161 92

export
base40 : Color
base40 = rgb 230 184 138

export
base20 : Color
base20 = rgb 230 207 184

export
comp100 : Color
comp100 = rgb 0 115 230

export
comp80 : Color
comp80 = rgb 46 138 230

export
comp60 : Color
comp60 = rgb 92 161 230

export
comp40 : Color
comp40 = rgb 138 184 230

export
comp20 : Color
comp20 = rgb 184 207 230


text:
module Finite.idr

import Data.Fin

--- This is the module for the Finite sets

||| The Data type finite. It is the same as Fin except the size has been made explicit
data Finite : Nat -> Type where
    FinZ : (k : Nat) -> (Finite (S k))
    FinS : (k : Nat) -> (Finite k) -> (Finite (S k))

total
Finite_to_Fin : (k : Nat) -> (Finite k) -> (Fin k)
Finite_to_Fin Z a impossible
Finite_to_Fin (S k) (FinZ k) = FZ
Finite_to_Fin (S k) (FinS k nm) = FS (Finite_to_Fin k nm)

total
Fin_to_Finite : (k : Nat) -> (Fin k) -> (Finite k)
Fin_to_Finite Z a impossible
Fin_to_Finite (S k) FZ = FinZ k
Fin_to_Finite (S k) (FS l) = FinS k (Fin_to_Finite k l)

||| Predecessor function for finite
total
predFinite : (k : Nat) -> (Finite k) -> (Finite k)
predFinite Z a impossible
predFinite (S k) (FinZ k) = FinZ k
predFinite (S (S k)) (FinS (S k) (FinZ k)) = FinZ (S k)
predFinite (S (S k)) (FinS (S k) l) = FinS (S k) (predFinite (S k) l)

||| Predecessor function for fin
total
predFin : (n : Nat) -> (Fin n) -> (Fin n)
predFin n a = Finite_to_Fin n ( predFinite n (Fin_to_Finite n a))


text:
||| Wyvern! A simple little web server written in Idris.
|||
||| Author:  Eric Weinstein <eric.q.weinstein@gmail.com>
||| License: MIT (see LICENSE)
module Wyvern

import public Wyvern.Core

max_stars_repo_name: ericqweinstein/wyvern

max_issues_repo_name: ericqweinstein/wyvern

max_forks_repo_name: ericqweinstein/wyvern


text:
module ZipWithN

import Data.List
import Data.Vect

%default total

public export
interface ZipWithable f where
  zipWith : (a -> b -> c) -> f a -> f b -> f c

public export
ZipWithable List where
  zipWith = List.zipWith

public export
ZipWithable (Vect n) where
  zipWith = Vect.zipWith

namespace FunctionBased

  public export
  FunN : Vect n Type -> Type -> Type
  FunN []      ty = ty
  FunN (x::xs) ty = x -> FunN xs ty

  apFunN : {n : Nat} -> {0 args : Vect n Type} -> ZipWithable f => f $ FunN args res -> FunN (f <$> args) (f res)
  apFunN {n=Z}   {args=[]}    = id
  apFunN {n=S k} {args=a::as} = \fs, fa => apFunN $ zipWith apply fs fa

  public export
  zipWithN : {n : Nat} -> {0 args : Vect n Type} -> (ZipWithable m, Applicative m) => FunN args res -> FunN (m <$> args) (m res)
  zipWithN {n=Z}   {args=[]}    = pure
  zipWithN {n=S k} {args=a::as} = \f, xs => apFunN $ f <$> xs

namespace PseudoTypeclassBased_SearchBoth

  public export
  data FunN : (m : Type -> Type) -> ty -> mty -> Type where
    Constant : FunN m ty (m ty)
    Function : FunN m ty mty -> FunN m (a -> ty) (m a -> mty)

  apFunN : FunN m ty mty => ZipWithable m => m ty -> mty
  apFunN @{Constant}   = id
  apFunN @{Function s} = \fs, fa => apFunN $ zipWith apply fs fa

  public export
  zipWithN : FunN m ty mty => ZipWithable m => Applicative m => ty -> mty
  zipWithN @{Constant}   = pure
  zipWithN @{Function s} = \f, xs => apFunN $ f <$> xs