summaryrefslogtreecommitdiff
path: root/testsuite/tests/gadt/while.hs
diff options
context:
space:
mode:
authorDavid Terei <davidterei@gmail.com>2011-07-20 11:09:03 -0700
committerDavid Terei <davidterei@gmail.com>2011-07-20 11:26:35 -0700
commit16514f272fb42af6e9c7674a9bd6c9dce369231f (patch)
treee4f332b45fe65e2a7a2451be5674f887b42bf199 /testsuite/tests/gadt/while.hs
parentebd422aed41048476aa61dd4c520d43becd78682 (diff)
downloadhaskell-16514f272fb42af6e9c7674a9bd6c9dce369231f.tar.gz
Move tests from tests/ghc-regress/* to just tests/*
Diffstat (limited to 'testsuite/tests/gadt/while.hs')
-rw-r--r--testsuite/tests/gadt/while.hs216
1 files changed, 216 insertions, 0 deletions
diff --git a/testsuite/tests/gadt/while.hs b/testsuite/tests/gadt/while.hs
new file mode 100644
index 0000000000..2040511c0f
--- /dev/null
+++ b/testsuite/tests/gadt/while.hs
@@ -0,0 +1,216 @@
+{-# LANGUAGE GADTs, ExistentialQuantification #-}
+
+module Main where
+
+succeed :: a -> Maybe a
+succeed = return
+
+data V s t where
+ Z :: V (t,m) t
+ S :: V m t -> V (x,m) t
+
+data Exp s t where
+ IntC :: Int -> Exp s Int -- 5
+ BoolC :: Bool -> Exp s Bool -- True
+ Plus :: Exp s Int -> Exp s Int -> Exp s Int -- x + 3
+ Lteq :: Exp s Int -> Exp s Int -> Exp s Bool -- x <= 3
+ Var :: V s t -> Exp s t -- x
+
+data Com s where
+ Set :: V s t -> Exp s t -> Com s -- x := e
+ Seq :: Com s -> Com s -> Com s -- { s1; s2; }
+ If :: Exp s Bool -> Com s -> Com s -> Com s -- if e then x else y
+ While :: Exp s Bool -> Com s -> Com s -- while e do s
+ Declare :: Exp s t -> Com (t,s) -> Com s -- { int x = 5; s }
+
+update :: (V s t) -> t -> s -> s
+update Z n (x,y) = (n,y)
+update (S v) n (x,y) = (x,update v n y)
+
+eval :: Exp s t -> s -> t
+eval (IntC n) s = n
+eval (BoolC b) s = b
+eval (Plus x y) s = (eval x s) + (eval y s)
+eval (Lteq x y) s = (eval x s) <= (eval y s)
+eval (Var Z) (x,y) = x
+eval (Var (S v)) (x,y) = eval (Var v) y
+
+
+exec :: (Com st) -> st -> st
+exec (Set v e) s = update v (eval e s) s
+exec (Seq x y) s = exec y (exec x s)
+exec (If test x1 x2) s =
+ if (eval test s) then exec x1 s else exec x2 s
+exec (While test body) s = loop s
+ where loop s = if (eval test s)
+ then loop (exec body s)
+ else s
+exec (Declare e body) s = store
+ where (_,store) = (exec body (eval e s,s))
+
+v0 = Z
+v1 = S Z
+v2 = S (S Z)
+v3 = S (S (S Z))
+
+e2 = Lteq (Plus (Var v0)(Var v1)) (Plus (Var v0) (IntC 1))
+
+sum_var = Z
+x = S Z
+
+prog :: Com (Int,(Int,a))
+prog =
+ Seq (Set sum_var (IntC 0))
+ (Seq (Set x (IntC 1))
+ (While (Lteq (Var x) (IntC 5))
+ (Seq (Set sum_var (Plus (Var sum_var)(Var x)))
+ (Set x (Plus (Var x) (IntC 1))))))
+
+ans = exec prog (34,(12,1))
+main = print ans
+{-
+{ sum = 0 ;
+ x = 1;
+ while (x <= 5)
+ { sum = sum + x;
+ x = x + 1;
+ }
+}
+-}
+
+
+---------------------------------------------------
+-- Untyped Annotated AST
+
+data TyAst = I | B | P TyAst TyAst
+
+data TypeR t where
+ IntR :: TypeR Int
+ BoolR :: TypeR Bool
+ PairR :: TypeR a -> TypeR b -> TypeR (a,b)
+
+-- Judgments for Types
+data TJudgment = forall t . TJ (TypeR t)
+
+checkT :: TyAst -> TJudgment
+checkT I = TJ IntR
+checkT B = TJ BoolR
+checkT (P x y) =
+ case (checkT x,checkT y) of
+ (TJ a, TJ b) -> TJ(PairR a b)
+
+----------------------------------------------------
+-- Equality Proofs and Type representations
+data Equal a b where
+ EqProof :: Equal a a
+
+match :: TypeR a -> TypeR b -> Maybe (Equal a b)
+match IntR IntR = succeed EqProof
+match BoolR BoolR = succeed EqProof
+match (PairR a b) (PairR c d) =
+ do { EqProof <- match a c
+ ; EqProof <- match b d
+ ; succeed EqProof }
+match _ _ = fail "match fails"
+
+
+----------------------------------------------
+-- checking Variables are consistent
+
+checkV :: Int -> TypeR t -> TypeR s -> Maybe(V s t)
+checkV 0 t1 (PairR t2 p) =
+ do { EqProof <- match t1 t2
+ ; return Z }
+checkV n t1 (PairR ty p) =
+ do { v <- checkV (n-1) t1 p; return(S v)}
+checkV n t1 sr = Nothing
+
+
+-----------------------------------------------------
+data ExpAst
+ = IntCA Int
+ | BoolCA Bool
+ | PlusA ExpAst ExpAst
+ | LteqA ExpAst ExpAst
+ | VarA Int TyAst
+
+-- Judgments for Expressions
+data EJudgment s = forall t . EJ (TypeR t) (Exp s t)
+
+checkE :: ExpAst -> TypeR s -> Maybe (EJudgment s)
+checkE (IntCA n) sr = succeed(EJ IntR (IntC n))
+checkE (BoolCA b) sr = succeed(EJ BoolR (BoolC b))
+checkE (PlusA x y) sr =
+ do { EJ t1 e1 <- checkE x sr
+ ; EqProof <- match t1 IntR
+ ; EJ t2 e2 <- checkE y sr
+ ; EqProof <- match t2 IntR
+ ; succeed(EJ IntR (Plus e1 e2))}
+checkE (VarA n ty) sr =
+ do { TJ t <- succeed(checkT ty)
+ ; v <- checkV n t sr
+ ; return(EJ t (Var v)) }
+
+-----------------------------------------------------
+data ComAst
+ = SetA Int TyAst ExpAst
+ | SeqA ComAst ComAst
+ | IfA ExpAst ComAst ComAst
+ | WhileA ExpAst ComAst
+ | DeclareA TyAst ExpAst ComAst
+
+data CJudgment s = EC (Com s)
+
+checkC :: ComAst -> TypeR s -> Maybe(CJudgment s)
+checkC (SetA n ty e) sr =
+ do { TJ t1 <- succeed(checkT ty)
+ ; v <- checkV n t1 sr
+ ; EJ t2 e1 <- checkE e sr
+ ; EqProof <- match t1 t2
+ ; return(EC (Set v e1))}
+checkC (SeqA x y) sr =
+ do { EC c1 <- checkC x sr
+ ; EC c2 <- checkC y sr
+ ; return(EC (Seq c1 c2)) }
+checkC (IfA e x y) sr =
+ do { EJ t1 e1 <- checkE e sr
+ ; EqProof <- match t1 BoolR
+ ; EC c1 <- checkC x sr
+ ; EC c2 <- checkC y sr
+ ; return(EC(If e1 c1 c2)) }
+checkC (WhileA e x) sr =
+ do { EJ t1 e1 <- checkE e sr
+ ; EqProof <- match t1 BoolR
+ ; EC c1 <- checkC x sr
+ ; return(EC(While e1 c1)) }
+checkC (DeclareA ty e c) sr =
+ do { TJ t1 <- succeed(checkT ty)
+ ; EJ t2 e2 <- checkE e sr
+ ; EqProof <- match t1 t2
+ ; EC c2 <- checkC c (PairR t1 sr)
+ ; return(EC(Declare e2 c2)) }
+
+--------------------------------------------------------------
+
+e1 = Lteq (Plus (Var sum_var)(Var x)) (Plus (Var x) (IntC 1))
+
+{-
+data Store s
+ = M (Code s)
+ | forall a b . N (Code a) (Store b) where s = (a,b)
+
+eval2 :: Exp s t -> Store s -> Code t
+eval2 (IntC n) s = lift n
+eval2 (BoolC b) s = lift b
+eval2 (Plus x y) s = [| $(eval2 x s) + $(eval2 y s) |]
+eval2 (Lteq x y) s = [| $(eval2 x s) <= $(eval2 y s) |]
+eval2 (Var Z) (N a b) = a
+eval2 (Var (S v)) (N a b) = eval2 (Var v) b
+eval2 (Var Z) (M x) = [| fst $x |]
+eval2 (Var (S v)) (M x) = eval2 (Var v) (M [| snd $x |])
+
+
+test e = [| \ (x,(y,z)) -> $(eval2 e (N [|x|] (N [|y|] (M [|z|])))) |]
+
+-- test e1 ---> [| \ (x,(y,z)) -> x + y <= y + 1 |]
+-} \ No newline at end of file