josh-hs-ko

-- programming

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

_+_ : Nat → Nat → Nat
zero  + n = n
suc m + n = suc (m + n)

josh-hs-ko

open import Data.Sum

module BinomialHeap (V : Set)
                    (_≤_ : V → V → Set) (≤-refl : {x : V} → x ≤ x) (≤-trans : {x y z : V} → x ≤ y → y ≤ z → x ≤ z)
                    (_≤?_ : (x y : V) → x ≤ y ⊎ y ≤ x) where

open import Level using (Level; _⊔_)
open import Function
open import Data.Empty
open import Data.Unit

josh-hs-ko

"Embedded Domain-Specific Languages"
Jeremy Gibbons, University of Oxford <jeremy.gibbons@cs.ox.ac.uk>
Formosan Summer School on Logic, Languages and Computation, Taipei, July 2014

Complete solutions for exercises.

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

> {-# LANGUAGE StandaloneDeriving #-}
>

josh-hs-ko

"Embedded Domain-Specific Languages"
Jeremy Gibbons, University of Oxford <jeremy.gibbons@cs.ox.ac.uk>
Formosan Summer School on Logic, Languages and Computation, Taipei, July 2014

Skeleton code for exercises.

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

> {-# LANGUAGE StandaloneDeriving #-}
>

josh-hs-ko

{-# LINE 30 "parser.ltx" #-}
{-#  LANGUAGE KindSignatures, GADTs  #-}
import Data.List (inits, tails)
import Data.Char (ord)
import Control.Monad (mplus)
{-# LINE 56 "parser.ltx" #-}
data Grammar :: *   where
  Empty   :: Grammar
  Unit    :: Grammar
  Single  :: Char -> Grammar