jozefg

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
module Lift where
import Control.Monad.Gen
import Data.Functor.Foldable (Fix(..))

jozefg

{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module PatCompile where
import Bound
import Bound.Var
import Bound.Scope
import Control.Monad (ap)

jozefg

{-# LANGUAGE FlexibleContexts #-}
module PickRandom where
import Data.List (group, sort)
import Control.Monad
import Control.Monad.Random (MonadRandom, getRandomR)
import qualified Control.Foldl as F

-- Pick a value uniformly from a fold
pickRandom :: MonadRandom m => a -> F.FoldM m a a
pickRandom a = F.FoldM choose (return (a, 0 :: Int)) (return . fst)

jozefg

module Main where
import Control.Concurrent
import Control.Concurrent.STM
import Control.Exception
import Control.Monad

-- To start with, an intermezzo of the book's definition of Async and some key
-- operations on it.
data Async a = Async { pid :: ! ThreadId
                     , getAsync :: STM (Either SomeException a)

jozefg

#lang racket

;; This compiles some nontrivial subset of scheme with let, letrec, let*
;; quote, set!, and if to some subset of Scheme which is CPSed, has no
;; nested lambdas and is explicitly closure converted. Mostly done to stretch
;; my legs a bit with Racket.

(define *primops*
  '(+ - * / equal? < = and or not display cons car list box unbox set-box!))

jozefg

module ind-rec where
open import Data.Empty
open import Data.Product
open import Function
open import Level

record ⊤ {ℓ : Level} : Set ℓ where
  constructor tt

mutual

jozefg

module realize where
open import Relation.Nullary
import      Data.Empty       as E
open import Data.Product
open import Data.Sum
open import Data.Nat

data Term : Set where
  var    : ℕ → Term
  lam    : Term → Term

jozefg

module realize where
open import Relation.Nullary
import Data.Unit as U
import Data.Empty as E
open import Data.Product
open import Data.Sum
open import Data.Nat

data Lam : Set where
  var : ℕ → Lam

jozefg

signature TAG =
sig
  type tagged
  type 'a tag

  val new    : unit -> 'a tag
  val tag    : 'a tag -> 'a -> tagged
  val untag  : 'a tag -> tagged -> 'a option
end

jozefg

signature COROUTINE =
sig
  type ('a, 'b, 'r) t

  val await : ('a, 'b, 'a) t
  val yield : 'b -> ('a, 'b, unit) t

  (* Monadic interface and stuffs *)
  val map    : ('c -> 'd) -> ('a, 'b, 'c) t -> ('a, 'b, 'd) t
  val return : 'c -> ('a, 'b, 'c) t