andrevidela

||| A well-typed entity component system
||| The goal of an entity component system is to be able to deal with a heterogenous
||| collection of objects some of which share a set of features or interfaces.
module ECS

import Data.List
import Data.Maybe
import Data.Product
import Data.List.Quantifiers

andrevidela

module Univ

import Decidable.Equality

-- Weapon, which can have "attack power" to evaluate its damage potential
interface IsWeapon a where
  getAttack : a -> Int

-- Kitchen tool, which can have "quality" to evaluate its usefulness and durability
interface IsKitchen a where

andrevidela

.markdown-rendered .block-language-tikz svg {
    zoom:2
}

andrevidela

module Equality

import Data.Nat
import Control.Relation
import Control.Order

%default total

infix 4 ~~

andrevidela

module IndexedGames

import Data.List
import Data.Vect
import Data.Nat

infixr 6 >>>>
infixr 6 >>>
infixr 5 &&&&
infixr 5 &&&

andrevidela

{-# LANGUAGE FlexibleInstances,
             DerivingVia,
             DeriveGeneric,
             DeriveFoldable,
             DeriveFunctor,
             GeneralizedNewtypeDeriving#-}
module Main where

import Control.Monad.Zip

andrevidela

import Effects
import Effect.State
import Effect.Exception

runTest : Effects.SimpleEff.Eff a [EXCEPTION String, 'S1 ::: STATE Int, 'S2 ::: STATE Bool] -> Either String a
runTest m = runInit ['S1 := 2, 'S2 := False] m

andrevidela

import TParsec

except : (Alternative mn, Monad mn, Inspect (Toks p) (Tok p), Eq (Tok p)) =>
         Tok p -> All (Parser mn p (Tok p))
except t = guard (\t' => (t /= t')) anyTok

notChar : (Alternative mn, Monad mn, Subset Char (Tok p), Eq (Tok p), Inspect (Toks p) (Tok p)) =>
          Char -> All (Parser mn p (Tok p))
notChar = except . into

andrevidela

data Set : a -> Type where
  Empty : Set a
  Singleton : a -> Set a
  Union : Set a -> Set a -> Set a
  Inter : Set a -> Set a -> Set a

andrevidela

package com.ovoenergy

import java.util.{Calendar, Date}

object Aggregator {

  case class DailySnapshot(date: Date, amount: Double)
  case class MonthlyConsumption(date: Date, amount: Double)

  def parseData(data: Seq[(String, Double)]): Seq[DailySnapshot] = {