diff options
Diffstat (limited to 'testsuite/tests/gadt/nbe.hs')
| -rw-r--r-- | testsuite/tests/gadt/nbe.hs | 82 |
1 files changed, 41 insertions, 41 deletions
diff --git a/testsuite/tests/gadt/nbe.hs b/testsuite/tests/gadt/nbe.hs index 60141291fc..103319ad1d 100644 --- a/testsuite/tests/gadt/nbe.hs +++ b/testsuite/tests/gadt/nbe.hs @@ -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 |