copumpkin

// Something like this, anyway ;)
// by pumpkin

struct class_info_t {
  struct class_info_t *metaclass; // maybe not exactly a class_info_t, maybe an info_table_t
  struct class_info_t *superclass; // as above
  void *cache;
  void *vtable;
  struct info_table_t *info;
}

copumpkin

/*
kernelcache.idc, by pumpkin with contributions from roxfan
Copyright (C) 2008 pumpkin

This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,

copumpkin

{-# LANGUAGE EmptyDataDecls, FlexibleContexts, FlexibleInstances, FunctionalDependencies, TypeFamilies, MultiParamTypeClasses, ScopedTypeVariables, TypeOperators, ImplicitParams, RankNTypes, GADTs, GeneralizedNewtypeDeriving, NoImplicitPrelude, TypeSynonymInstances, TypeOperators #-}
module Main where

-- ZOMG failgebra by copumpkin (not intended to be useful, but just as a straggly experiment to see what's possible)

-- TODO: using2 could take a function mapping from common types to wrapper types and maybe reduce ugliness

import Prelude hiding (id, (+), (-), (*), (/), Integral, fromInteger, Real)
import qualified Prelude as P
import Data.Number.CReal 

copumpkin

{-# LANGUAGE ScopedTypeVariables #-}
module Data.Enumerable where

import Data.Int
import Data.Word
import Data.Ratio

import Unsafe.Coerce

import Data.List

copumpkin

module Search where

open import Coinduction
open import Function
open import Data.Empty
open import Data.Nat
open import Data.Product
open import Relation.Nullary

-- Thanks to Ed Kmett for helping me clarify what I was getting at here,

copumpkin

module Split where

open import Data.Bool
open import Data.Nat
open import Data.Nat.Properties
open import Data.List hiding ([_])
open import Data.Product

open import Relation.Binary
open import Relation.Binary.PropositionalEquality

copumpkin

module Routing where

open import Function hiding (type-signature)

open import Data.Bool hiding (_≟_)
open import Data.Maybe
open import Data.Char hiding (_≟_)
open import Data.String as String
open import Data.List as List hiding ([_])
open import Data.Product hiding (curry; uncurry)

copumpkin

module Nicomachus where

open import Function
open import Relation.Binary.PropositionalEquality
import Relation.Binary.EqReasoning as EqReasoning

open import Data.Nat
open import Data.Nat.Properties

-- http://en.wikipedia.org/wiki/Nicomachus%27s_theorem

copumpkin

{-# OPTIONS --type-in-type --without-K #-}
module Russell where

open import Data.Empty
open import Data.Product
open import Relation.Nullary hiding (yes; no)
open import Relation.Binary.PropositionalEquality

-- Based on Robert Dockins's Coq reorganization of Chad E Brown's proof of Russell's paradox

copumpkin

module Categories.Agda.State where

open import Categories.Category
open import Categories.Agda
open import Categories.Agda.Product
open import Categories.Functor hiding (_≡_)
open import Categories.Functor.Product
open import Categories.Functor.Hom
open import Categories.Monad
open import Categories.Adjunction