Commit 915e07c3 authored by thomie's avatar thomie
Browse files

Testsuite: tabs -> spaces [skip ci]

parent 46ff80f2
{-# LANGUAGE GADTs, ScopedTypeVariables #-}
-- Supplied by Henrik Nilsson, showed up a bug in GADTs
-- Supplied by Henrik Nilsson, showed up a bug in GADTs
module Nilsson where
......@@ -12,7 +12,7 @@ fromEvent = undefined
usrErr :: String -> String -> String -> a
usrErr = undefined
type DTime = Double -- [s]
type DTime = Double -- [s]
data SF a b = SF {sfTF :: a -> Transition a b}
......@@ -53,13 +53,13 @@ sfArr (FDG f) = sfArrG f
sfId :: SF' a a
sfId = sf
where
sf = SFArr (\_ a -> (sf, a)) FDI
sf = SFArr (\_ a -> (sf, a)) FDI
sfConst :: b -> SF' a b
sfConst b = sf
where
sf = SFArr (\_ _ -> (sf, b)) (FDC b)
sf = SFArr (\_ _ -> (sf, b)) (FDC b)
sfNever :: SF' a (Event b)
......@@ -76,7 +76,7 @@ sfArrE f fne = sf
sfArrG :: (a -> b) -> SF' a b
sfArrG f = sf
where
sf = SFArr (\_ a -> (sf, f a)) (FDG f)
sf = SFArr (\_ a -> (sf, f a)) (FDG f)
sfAcc :: (c -> a -> (c, b)) -> c -> b -> SF' (Event a) b
......@@ -107,10 +107,10 @@ sfAcc f c bne = sf
-- * We still want to be able to get hold of the original function.
data FunDesc a b where
FDI :: FunDesc a a -- Identity function
FDC :: b -> FunDesc a b -- Constant function
FDE :: (Event a -> b) -> b -> FunDesc (Event a) b -- Event-processing fun
FDG :: (a -> b) -> FunDesc a b -- General function
FDI :: FunDesc a a -- Identity function
FDC :: b -> FunDesc a b -- Constant function
FDE :: (Event a -> b) -> b -> FunDesc (Event a) b -- Event-processing fun
FDG :: (a -> b) -> FunDesc a b -- General function
fdFun :: FunDesc a b -> (a -> b)
fdFun FDI = id
......@@ -142,17 +142,17 @@ vfyNoEv :: Event a -> b -> b
vfyNoEv NoEvent b = b
vfyNoEv _ _ = usrErr "AFRP" "vfyNoEv"
"Assertion failed: Functions on events must not \
\map NoEvent to Event."
\map NoEvent to Event."
compPrim :: SF a b -> SF b c -> SF a c
compPrim (SF {sfTF = tf10}) (SF {sfTF = tf20}) = SF {sfTF = tf0}
where
tf0 a0 = (cpXX sf1 sf2, c0)
where
(sf1, b0) = tf10 a0
(sf2, c0) = tf20 b0
tf0 a0 = (cpXX sf1 sf2, c0)
where
(sf1, b0) = tf10 a0
(sf2, c0) = tf20 b0
-- Naming convention: cp<X><Y> where <X> and <Y> is one of:
-- Naming convention: cp<X><Y> where <X> and <Y> is one of:
-- X - arbitrary signal function
-- A - arbitrary pure arrow
-- C - constant arrow
......@@ -165,35 +165,35 @@ compPrim (SF {sfTF = tf10}) (SF {sfTF = tf20}) = SF {sfTF = tf0}
cpXX sf1 (SFArr _ fd2) = cpXA sf1 fd2
cpXX (SFAcc _ f1 s1 bne) (SFAcc _ f2 s2 cne) =
sfAcc f (s1, s2) (vfyNoEv bne cne)
where
f (s1, s2) a =
case f1 s1 a of
(s1', NoEvent) -> ((s1', s2), cne)
(s1', Event b) ->
let (s2', c) = f2 s2 b in ((s1', s2'), c)
where
f (s1, s2) a =
case f1 s1 a of
(s1', NoEvent) -> ((s1', s2), cne)
(s1', Event b) ->
let (s2', c) = f2 s2 b in ((s1', s2'), c)
cpXX (SFCpAXA _ fd11 sf12 fd13) (SFCpAXA _ fd21 sf22 fd23) =
cpAXA fd11 (cpXX (cpXA sf12 (fdComp fd13 fd21)) sf22) fd23
cpXX sf1 sf2 = SF' tf
where
tf dt a = (cpXX sf1' sf2', c)
where
(sf1', b) = (sfTF' sf1) dt a
(sf2', c) = (sfTF' sf2) dt b
cpXX sf1 sf2 = SF' tf
where
tf dt a = (cpXX sf1' sf2', c)
where
(sf1', b) = (sfTF' sf1) dt a
(sf2', c) = (sfTF' sf2) dt b
cpAXA :: FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
cpAXA FDI sf2 fd3 = cpXA sf2 fd3
cpAXA fd1 sf2 FDI = cpAX fd1 sf2
cpAXA (FDC b) sf2 fd3 = cpCXA b sf2 fd3
cpAXA fd1 sf2 (FDC d) = sfConst d
cpAXA fd1 sf2 (FDC d) = sfConst d
cpAXA fd1 (SFArr _ fd2) fd3 = sfArr (fdComp (fdComp fd1 fd2) fd3)
cpAX :: FunDesc a b -> SF' b c -> SF' a c
cpAX :: FunDesc a b -> SF' b c -> SF' a c
cpAX FDI sf2 = sf2
cpAX (FDC b) sf2 = cpCX b sf2
cpAX (FDE f1 f1ne) sf2 = cpEX f1 f1ne sf2
cpAX (FDG f1) sf2 = cpGX f1 sf2
cpXA :: SF' a b -> FunDesc b c -> SF' a c
cpXA :: SF' a b -> FunDesc b c -> SF' a c
cpXA sf1 FDI = sf1
cpXA sf1 (FDC c) = sfConst c
cpXA sf1 (FDE f2 f2ne) = cpXE sf1 f2 f2ne
......@@ -204,13 +204,13 @@ compPrim (SF {sfTF = tf10}) (SF {sfTF = tf20}) = SF {sfTF = tf0}
cpCX b (SFAcc _ _ _ cne) = sfConst (vfyNoEv b cne)
cpCX b (SFCpAXA _ fd21 sf22 fd23) =
cpCXA ((fdFun fd21) b) sf22 fd23
cpCX b sf2 = SFCpAXA tf (FDC b) sf2 FDI
where
tf dt _ = (cpCX b sf2', c)
where
(sf2', c) = (sfTF' sf2) dt b
cpCX b sf2 = SFCpAXA tf (FDC b) sf2 FDI
where
tf dt _ = (cpCX b sf2', c)
where
(sf2', c) = (sfTF' sf2) dt b
-- For SPJ: The following version did not work.
-- For SPJ: The following version did not work.
-- The commented out one below did work, by lambda-lifting cpCXAux
cpCXA :: b -> SF' b c -> FunDesc c d -> SF' a d
cpCXA b sf2 FDI = cpCX b sf2
......@@ -219,7 +219,7 @@ compPrim (SF {sfTF = tf10}) (SF {sfTF = tf20}) = SF {sfTF = tf0}
where
f3 = fdFun fd3
cpCXAAux :: SF' b c -> SF' a d
cpCXAAux :: SF' b c -> SF' a d
cpCXAAux (SFArr _ fd2) = sfConst (f3 ((fdFun fd2) b))
cpCXAAux (SFAcc _ _ _ cne) = sfConst (vfyNoEv b (f3 cne))
cpCXAAux (SFCpAXA _ fd21 sf22 fd23) = cpCXA ((fdFun fd21) b) sf22 (fdComp fd23 fd3)
......@@ -231,7 +231,7 @@ compPrim (SF {sfTF = tf10}) (SF {sfTF = tf20}) = SF {sfTF = tf0}
cpCXA b sf2 fd3 = cpCXAAux b fd3 (fdFun fd3) sf2
where
-- f3 = fdFun fd3
-- Really something like: cpCXAAux :: SF' b c -> SF' a d
-- Really something like: cpCXAAux :: SF' b c -> SF' a d
cpCXAAux :: b -> FunDesc c d -> (c -> d) -> SF' b c -> SF' a d
cpCXAAux b fd3 f3 (SFArr _ fd2) = sfConst (f3 ((fdFun fd2) b))
cpCXAAux b fd3 f3 (SFAcc _ _ _ cne) = sfConst (vfyNoEv b (f3 cne))
......@@ -239,44 +239,44 @@ compPrim (SF {sfTF = tf10}) (SF {sfTF = tf20}) = SF {sfTF = tf0}
-}
cpGX :: (a -> b) -> SF' b c -> SF' a c
cpGX f1 (SFArr _ fd2) = sfArr (fdComp (FDG f1) fd2)
cpGX f1 (SFArr _ fd2) = sfArr (fdComp (FDG f1) fd2)
cpGX f1 (SFCpAXA _ fd21 sf22 fd23) =
cpAXA (fdComp (FDG f1) fd21) sf22 fd23
cpGX f1 sf2 = SFCpAXA tf (FDG f1) sf2 FDI
where
tf dt a = (cpGX f1 sf2', c)
where
(sf2', c) = (sfTF' sf2) dt (f1 a)
cpGX f1 sf2 = SFCpAXA tf (FDG f1) sf2 FDI
where
tf dt a = (cpGX f1 sf2', c)
where
(sf2', c) = (sfTF' sf2) dt (f1 a)
cpXG :: SF' a b -> (b -> c) -> SF' a c
cpXG (SFArr _ fd1) f2 = sfArr (fdComp fd1 (FDG f2))
cpXG (SFArr _ fd1) f2 = sfArr (fdComp fd1 (FDG f2))
cpXG (SFAcc _ f1 s bne) f2 = sfAcc f s (f2 bne)
where
f s a = let (s', b) = f1 s a in (s', f2 b)
cpXG (SFCpAXA _ fd11 sf12 fd22) f2 =
cpXG (SFCpAXA _ fd11 sf12 fd22) f2 =
cpAXA fd11 sf12 (fdComp fd22 (FDG f2))
cpXG sf1 f2 = SFCpAXA tf FDI sf1 (FDG f2)
where
tf dt a = (cpXG sf1' f2, f2 b)
where
(sf1', b) = (sfTF' sf1) dt a
cpXG sf1 f2 = SFCpAXA tf FDI sf1 (FDG f2)
where
tf dt a = (cpXG sf1' f2, f2 b)
where
(sf1', b) = (sfTF' sf1) dt a
cpEX :: (Event a -> b) -> b -> SF' b c -> SF' (Event a) c
cpEX f1 f1ne (SFArr _ fd2) = sfArr (fdComp (FDE f1 f1ne) fd2)
cpEX f1 f1ne (SFAcc _ f2 s cne) = sfAcc f s (vfyNoEv f1ne cne)
cpEX f1 f1ne (SFArr _ fd2) = sfArr (fdComp (FDE f1 f1ne) fd2)
cpEX f1 f1ne (SFAcc _ f2 s cne) = sfAcc f s (vfyNoEv f1ne cne)
where
f s a = f2 s (fromEvent (f1 (Event a)))
cpEX f1 f1ne (SFCpAXA _ fd21 sf22 fd23) =
cpEX f1 f1ne (SFCpAXA _ fd21 sf22 fd23) =
cpAXA (fdComp (FDE f1 f1ne) fd21) sf22 fd23
cpEX f1 f1ne sf2 = SFCpAXA tf (FDE f1 f1ne) sf2 FDI
where
tf dt ea = (cpEX f1 f1ne sf2', c)
where
cpEX f1 f1ne sf2 = SFCpAXA tf (FDE f1 f1ne) sf2 FDI
where
tf dt ea = (cpEX f1 f1ne sf2', c)
where
(sf2', c) = case ea of
NoEvent -> (sfTF' sf2) dt f1ne
_ -> (sfTF' sf2) dt (f1 ea)
NoEvent -> (sfTF' sf2) dt f1ne
_ -> (sfTF' sf2) dt (f1 ea)
cpXE :: SF' a (Event b) -> (Event b -> c) -> c -> SF' a c
cpXE :: SF' a (Event b) -> (Event b -> c) -> c -> SF' a c
cpXE (SFArr _ fd1) f2 f2ne = sfArr (fdComp fd1 (FDE f2 f2ne))
cpXE (SFAcc _ f1 s bne) f2 f2ne = sfAcc f s (vfyNoEv bne f2ne)
where
......@@ -285,9 +285,9 @@ compPrim (SF {sfTF = tf10}) (SF {sfTF = tf20}) = SF {sfTF = tf0}
case eb of NoEvent -> (s', f2ne); _ -> (s', f2 eb)
cpXE (SFCpAXA _ fd11 sf12 fd13) f2 f2ne =
cpAXA fd11 sf12 (fdComp fd13 (FDE f2 f2ne))
cpXE sf1 f2 f2ne = SFCpAXA tf FDI sf1 (FDE f2 f2ne)
where
tf dt a = (cpXE sf1' f2 f2ne,
cpXE sf1 f2 f2ne = SFCpAXA tf FDI sf1 (FDE f2 f2ne)
where
tf dt a = (cpXE sf1' f2 f2ne,
case eb of NoEvent -> f2ne; _ -> f2 eb)
where
where
(sf1', eb) = (sfTF' sf1) dt a
......@@ -9,8 +9,8 @@ class Key k where
instance (Key a, Key b) => Key (a,b) where
type Map (a,b) = MP a b
lookup (a,b) (m :: Map (a,b) elt)
lookup (a,b) (m :: Map (a,b) elt)
= case lookup a m :: Maybe (Map b elt) of
Just (m2 :: Map b elt) -> lookup b m2 :: Maybe elt
Just (m2 :: Map b elt) -> lookup b m2 :: Maybe elt
data MP a b elt = MP (Map a (Map b elt))
......@@ -7,9 +7,9 @@ data Abs env g v where
class Eval g env h v where
eval :: env -> g env h v -> v
evalAbs :: Eval g2 (a2, env) h2 v2
=> env
-> Abs env (g2 (a2, env) h2 v2) (a2->v2)
-> (a2->v2)
evalAbs env (Abs e) x
evalAbs :: Eval g2 (a2, env) h2 v2
=> env
-> Abs env (g2 (a2, env) h2 v2) (a2->v2)
-> (a2->v2)
evalAbs env (Abs e) x
= eval (x, env) e -- e :: g (a,env) h v
......@@ -15,4 +15,4 @@ g (T n) | n >= 3 = if n>3 then GT else EQ
g (T n) = LT
main = do print [f (T 0), f (T 1)]
print [g (T 2), g (T 3), g (T 4)]
print [g (T 2), g (T 3), g (T 4)]
......@@ -5,7 +5,7 @@
module Foo where
data TValue t where
TList :: [a] -> TValue [a]
TList :: [a] -> TValue [a]
instance (Eq b) => Eq (TValue b) where
(==) (TList p) (TList q) = (==) p q
......@@ -15,19 +15,19 @@ instance (Eq b) => Eq (TValue b) where
Here's the reasoning (I have done a bit of renaming).
* The TList constructor really has type
TList :: forall a. forall x. (a~[x]) => [x] -> TValue a
TList :: forall a. forall x. (a~[x]) => [x] -> TValue a
* So in the pattern match we have
(Eq b) available from the instance header
TList p :: TValue b
x is a skolem, existentially bound by the pattern
p :: [x]
b ~ [x] available from the pattern match
(Eq b) available from the instance header
TList p :: TValue b
x is a skolem, existentially bound by the pattern
p :: [x]
b ~ [x] available from the pattern match
* On the RHS we find we need (Eq [x]).
* So the constraint problem we have is
(Eq b, b~[x]) => Eq [x]
(Eq b, b~[x]) => Eq [x]
["Given" => "Wanted"]
Can we prove this? From the two given constraints we can see
that we also have Eq [x], and that certainly proves Eq [x].
......@@ -38,4 +38,4 @@ consequences of the "given" constraints, we might use the top-level Eq
a => Eq [a] instance to solve the wanted Eq [x]. And now we need Eq
x, which *isn't* a consequence of (Eq b, b~[x]).
-}
\ No newline at end of file
-}
......@@ -3,21 +3,21 @@
module Main where
data Term a where
Lit :: Int -> Term Int
Lit :: Int -> Term Int
IsZero :: Term Int -> Term Bool
If :: Term Bool -> Term a -> Term a -> Term a
Pr :: Term a -> Term b -> Term (a, b)
Fst :: Term (a, b) -> Term a
Snd :: Term (a, b) -> Term b
Pr :: Term a -> Term b -> Term (a, b)
Fst :: Term (a, b) -> Term a
Snd :: Term (a, b) -> Term b
eval :: Term v -> v
eval (Lit n) = n
eval (Lit n) = n
eval (IsZero t) = eval t == 0
eval (If t1 t2 t3) = if eval t1 then eval t2 else eval t3
eval (Pr t1 t2) = (eval t1, eval t2)
eval (Fst t) = case (eval t) of { (a,b) -> a }
eval (Snd t) = case (eval t) of { (a,b) -> b }
eval (Fst t) = case (eval t) of { (a,b) -> a }
eval (Snd t) = case (eval t) of { (a,b) -> b }
term = If (IsZero (Lit 1)) (Pr (Lit 2) (Lit 3)) (Pr (Lit 3) (Lit 4))
main = print (eval term)
\ No newline at end of file
main = print (eval term)
{-# LANGUAGE GADTs, KindSignatures #-}
-- Test a couple of trivial things:
-- explicit layout
-- trailing semicolons
-- kind signatures
-- explicit layout
-- trailing semicolons
-- kind signatures
module ShouldCompile where
data Expr :: * -> * where {
EInt :: Int -> Expr Int ;
EBool :: Bool -> Expr Bool ;
EIf :: (Expr Bool) -> (Expr a) -> (Expr a) -> Expr a ;
-- Note trailing semicolon, should be ok
-- Note trailing semicolon, should be ok
}
{-# LANGUAGE GADTs, KindSignatures,
MultiParamTypeClasses, FunctionalDependencies #-}
-- Program from Josef Svenningsson
-- Program from Josef Svenningsson
-- Just a short explanation of the program. It contains
-- some class declarations capturing some definitions from
......@@ -10,7 +10,7 @@
-- function defining the semantics for lambda terms called
-- 'interp'.
-- Made GHC 6.4 bleat
-- Made GHC 6.4 bleat
-- Quantified type variable `t' is unified with
-- another quantified type variable `terminal'
-- When trying to generalise the type inferred for `interp'
......@@ -38,14 +38,14 @@ class Category arr =>
inRight :: arr b (coprod a b)
ccase :: arr a c -> arr b c -> arr (coprod a b) c
class ProductCategory prod arr =>
class ProductCategory prod arr =>
Exponential exp prod arr | arr -> exp where
eval :: arr (prod (exp a b) a) b
curryA :: arr (prod c a) b -> arr c (exp a b)
class (Exponential exp prod arr, Terminal terminal arr) =>
CartesianClosed terminal exp prod arr | arr -> terminal exp prod
class (Exponential exp prod arr, Terminal terminal arr) =>
CartesianClosed terminal exp prod arr | arr -> terminal exp prod
data V prod env t where
Z :: V prod (prod env t) t
......@@ -55,13 +55,13 @@ data Lambda terminal (exp :: * -> * -> *) prod env t where
Unit :: Lambda foo exp prod env foo
Var :: V prod env t -> Lambda terminal exp prod env t
{- Lam :: Lambda terminal exp prod (prod env a) t
-> Lambda terminal exp prod env (exp a t)
App :: Lambda terminal exp prod env (exp t t')
-> Lambda terminal exp prod env t -> Lambda terminal exp prod env t'
-> Lambda terminal exp prod env (exp a t)
App :: Lambda terminal exp prod env (exp t t')
-> Lambda terminal exp prod env t -> Lambda terminal exp prod env t'
-}
interp :: CartesianClosed terminal exp prod arr =>
Lambda terminal exp prod s t -> arr s t
interp :: CartesianClosed terminal exp prod arr =>
Lambda terminal exp prod s t -> arr s t
interp (Unit) = terminal -- Terminal terminal arr => arr a terminal
-- interp (Var Z) = second
-- interp (Var (S v)) = first `comp` interp (Var v)
......
......@@ -11,10 +11,10 @@ data Ty t where
Arr :: Ty a -> Ty b -> Ty (a -> b)
data Exp g t where
Var :: Var g t -> Exp g t
Lam :: Ty a -> Exp (g,a) b -> Exp g (a->b)
App :: Exp g (s -> t) -> Exp g s -> Exp g t
If :: Exp g Bool -> Exp g t -> Exp g t -> Exp g t
Var :: Var g t -> Exp g t
Lam :: Ty a -> Exp (g,a) b -> Exp g (a->b)
App :: Exp g (s -> t) -> Exp g s -> Exp g t
If :: Exp g Bool -> Exp g t -> Exp g t -> Exp g t
ETrue :: Exp g Bool
EFalse :: Exp g Bool
......@@ -72,12 +72,12 @@ data TyEnv g where
Cons :: Ty t -> TyEnv h -> TyEnv (h,t)
infer :: TyEnv g -> Exp g t -> Ty t
infer g (Var x) = inferVar g x
infer g (Lam t e) = Arr t (infer (Cons t g) e)
infer g (App e e') = case infer g e of Arr _ t -> t
infer g (ETrue) = Bool
infer g (EFalse) = Bool
infer g (If _ e _) = infer g e
infer g (Var x) = inferVar g x
infer g (Lam t e) = Arr t (infer (Cons t g) e)
infer g (App e e') = case infer g e of Arr _ t -> t
infer g (ETrue) = Bool
infer g (EFalse) = Bool
infer g (If _ e _) = infer g e
inferVar :: TyEnv g -> Var g t -> Ty t
inferVar (Cons t h) (SVar x) = inferVar h x
......@@ -87,8 +87,8 @@ inferVar (Cons t h) (ZVar) = t
data Tree a = Val a | Choice (Tree a) (Tree a)
-- doesn't yet force trees to be fully balanced:
-- Val :: a -> Tree a Z
-- Choice :: Tree a n -> Tree a n -> Tree a (S n)
-- Val :: a -> Tree a Z
-- Choice :: Tree a n -> Tree a n -> Tree a (S n)
instance Functor Tree where
fmap = liftM
......@@ -114,8 +114,8 @@ flatten t = flatten_ t []
-- quote & friends -------------------------------------------------------------
-- for values --------------------------
enumV :: Ty t -> Tree t
questionsV :: Ty t -> [t -> Bool]
enumV :: Ty t -> Tree t
questionsV :: Ty t -> [t -> Bool]
enumV Bool = Choice (Val True) (Val False)
......@@ -123,46 +123,46 @@ enumV (Arr s t) = mkEnum (questionsV s) (enumV t)
where
mkEnum [] t = tmap const t
mkEnum (q:qs) es = do
f1 <- mkEnum qs es
f2 <- mkEnum qs es
return (\d -> if q d then f1 d else f2 d)
f1 <- mkEnum qs es
f2 <- mkEnum qs es
return (\d -> if q d then f1 d else f2 d)
questionsV Bool = return (\x -> x)
questionsV (Arr s t) = do
d <- flatten (enumV s)
q <- questionsV t
return (\f -> q (f d))
questionsV Bool = return (\x -> x)
questionsV (Arr s t) = do
d <- flatten (enumV s)
q <- questionsV t
return (\f -> q (f d))
-- for expressions ---------------------
enumE :: Ty t -> Tree (Exp g t)
questionsE :: Ty t -> [Exp g t -> Exp g Bool]
enumE :: Ty t -> Tree (Exp g t)
questionsE :: Ty t -> [Exp g t -> Exp g Bool]
enumE Bool = Choice (Val ETrue) (Val EFalse)
enumE (Arr s t) = tmap (lamE s) (mkEnumE (questionsE s) (enumE t))
where
mkEnumE [] t = tmap const t
mkEnumE (q:qs) es = do
f1 <- mkEnumE qs es
f2 <- mkEnumE qs es
return (\d -> ifE (q d) (f1 d) (f2 d))
questionsE Bool = return (\x -> x)
questionsE (Arr s t) = do
d <- flatten (enumE s)
q <- questionsE t
return (\f -> q (App f d))
-- should be
-- find (List (Exp g Bool) n) -> Tree (Exp g a) n -> Exp g a
f1 <- mkEnumE qs es
f2 <- mkEnumE qs es
return (\d -> ifE (q d) (f1 d) (f2 d))
questionsE Bool = return (\x -> x)
questionsE (Arr s t) = do
d <- flatten (enumE s)
q <- questionsE t
return (\f -> q (App f d))
-- should be
-- find (List (Exp g Bool) n) -> Tree (Exp g a) n -> Exp g a
find :: [Exp g Bool] -> Tree (Exp g a) -> Exp g a
find [] (Val a) = a
find (b:bs) (Choice l r) = ifE b (find bs l) (find bs r)
find _ _ = error "bad arguments to find"
find [] (Val a) = a
find (b:bs) (Choice l r) = ifE b (find bs l) (find bs r)
find _ _ = error "bad arguments to find"
quote :: Ty t -> t -> Exp g t
quote Bool t = case t of True -> ETrue; False -> EFalse
quote (Arr s t) f = lamE s (\e -> find (do q <- questionsE s; return (q e))
(tmap (quote t . f) (enumV s)))
(tmap (quote t . f) (enumV s)))
-- normalization (by evaluation) -----------------------------------------------
data BoxExp t = Box (forall g. Exp g t)
......@@ -183,4 +183,4 @@ test = [ eqB (nf b22b thrice) (nf b22b once)
, eqB (nf b22b twice) (nf b22b once)]
where nf = normalize
main = print test
\ No newline at end of file
main = print test
......@@ -18,8 +18,7 @@ g (T1 {x=xv, y=yv}) = T2 { x = xv }
h v = x v + 1
main = do { let t1 = T1 { y = "foo", x = 4 }
t2 = g t1
; print (h (f 8 undefined))
; print (h t2)
}
\ No newline at end of file
t2 = g t1
; print (h (f 8 undefined))
; print (h t2)
}
......@@ -5,7 +5,7 @@ module ShouldCompile where
-- data RBTree = forall n. Root (SubTree Black n)
-- Kind Colour
data Red
data Red