jfdm

module FoobarE

import Effects
import Effect.State
import Effect.StdIO

namespace Lib
  MyLib : Type -> Type
  MyLib rTy = Eff rTy ['libstate ::: STATE (List Nat), STDIO]

jfdm

module Domains

allLTE : List Int -> Bool
allLTE Nil        = True
allLTE (x::Nil)   = True
allLTE (x::y::xs) = x < y && allLTE (y::xs)

data VRange : Int -> Int -> Bool -> Type where
  MkVRange  : VRange x y (x <= y)

jfdm

||| You need latest version of my containers package:
|||     https://github.com/jfdm/idris-containers/
module Interp

import Data.DList
import Data.DeBruijn


data Ty = TyInt | TyBool | TyFun Ty Ty

jfdm

class Expr(object):
    def __init__(self):
        raise NotImplementedError
    def eval(self):
        raise NotImplementedError

class Value(Expr):
    def __init__(self, value):
        self.value = value

jfdm

module Data.DList

using (aTy : Type, elemTy : (aTy -> Type), x : aTy)

  ||| A list construct for dependent types.
  |||
  ||| @aTy    The type of the value contained within the list element type.
  ||| @elemTy The type of the elements within the list
  ||| @as     The List used to contain the different values within the type.
  public export

jfdm

module Data.List.Constraints

import Data.Vect

data NotElem : a -> List a -> Type where
  NotHere  : NotElem x []
  NotThere : Eq ty => {x,y : ty}  -> {auto prf : x /= y = True} -> NotElem x xs -> NotElem x (y::xs)


data AllDiff : List a -> Type where

jfdm

module Pairing

||| Model different group types.
data GTy = G1 | G2 | GT

||| Group element, implementation is incomplete but shows how dependent types can be used to provide more infomation.
data Element : GTy -> Type where
  MkElement : value -> (ty : GT) -> Element ty

||| Pairing information, implementation is incomplete.

jfdm

-- ------------------------------------------------------------- [ Channel.idr ]
-- Module    : Channel.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
--
-- A effectful API for `System.Concurrency.Sessions`.
--
-- The code was partially adapted from existing code developed by
-- Edwin Brady (see `FILE_IO` effect) and Simon Fowler---see `Process`
-- effect in `IdrisNet2`.

jfdm

#!/usr/bin/env stack
-- stack --resolver lts-7.10 --install-ghc runghc
--  --package text
--  --package bytestring
--  --package containers
--  --package cassava
--  --package generics
--  --package vector
{-# LANGUAGE DeriveGeneric #-}
-- |

jfdm

protocol Show {
    func show() -> String
}

class Tree<T> : Show {
    func show() -> String { return "" }
}

class Leaf<T> : Tree<T> {
    override func show() -> String {