module Spec where import Prelude hiding (return, (>>=), (>>)) -- Part of the exam question: data P s a symbol :: P s s pfail :: P s a (+++) :: P s a -> P s a -> P s a return :: a -> P s a (>>=) :: P s a -> (a -> P s b) -> P s b type Bag = [] (\/) = (++) type Sem s a = [s] -> Bag (a, [s]) sem :: P s a -> Sem s a symbol = error "TBD" pfail = error "TBD" (+++) = error "TBD" return = error "TBD" (>>=) = error "TBD" sem = error "TBD" a >> b = a >>= const b -- Start of answers: -- a) the value is [('h', ")")] type ProofSteps = [] -- Poor man's proofs (only type checked) proofSteps :: ProofSteps (Bag (Char, String)) proofSteps = [ sem (symbol >> symbol) "(h)" , -- def. of |>>| sem (symbol >>= const symbol) "(h)" , -- Lemma1 + beta reduction sem symbol "h)" , -- sem.sym.1 [('h', ")")] ] ---------------------------------------------------------------- {- Lemma1: sem (symbol >>= f) (s:ss) = sem (f s) ss Lemma2: sem (symbol >>= f) [] = [] -} stepsEmpty :: (s -> P s a) -> (s -> P s a) -> ProofSteps [(a, [s])] stepsEmpty f g = [ sem ((symbol >>= f) +++ (symbol >>= g)) [] , -- Spec. of sem (p +++ q) sem (symbol >>= f) [] \/ sem (symbol >>= g) [] , -- Lemma2 twice [] \/ [] , -- bag laws [] , -- Lemma2 "backwards" sem (symbol >>= \s -> f s +++ g s) [] ] stepsCons :: (s -> P s a) -> (s -> P s a) -> s -> [s] -> ProofSteps [(a, [s])] stepsCons f g s ss = [ sem ((symbol >>= f) +++ (symbol >>= g)) (s:ss) , -- sem.+++ sem (symbol >>= f) (s:ss) \/ sem (symbol >>= g) (s:ss) , -- Lemma1 twice sem (f s) ss \/ sem (g s) ss , -- Spec. of sem (p +++ q) "backwards" } sem (f s +++ g s) ss , -- Eta expansion sem ((\s -> f s +++ g s) s) ss , -- Lemma 1 "backwards" sem (symbol >>= (\s -> f s +++ g s)) (s:ss) ]