Changeset 27 for sizechecking/branches/macs

Timestamp:

May 5, 2014, 3:10:33 PM (11 years ago)

Author:

gobi

Message:

new files

Location:

sizechecking/branches/macs

Files:

• Exp.hs (modified) (2 diffs)
• Lambda.hs (modified) (4 diffs)
• Ops.hs (modified) (2 diffs)
• Size.hs (modified) (3 diffs)
• SizedFun.hs (added)
• Tests/BindTest.hs (added)
• Tests/ExpTest.hs (modified) (1 diff)
• Tests/SizeTest.hs (modified) (1 diff)
• sizechecking.cabal (modified) (1 diff)

sizechecking/branches/macs/Exp.hs

@@ -4 +4 @@
 import Ops
 import Data.Supply as S
+import Data.Lens.Light
 
 class LOps l => Exp l where
@@ -21 +22 @@
     cond c tbranch fbranch = if unQ c then tbranch else fbranch
     undefined = Prelude.undefined 
-instance Exp S where
-    nil = S $ \_ _ -> showString "[]"
-    undefined = S $ \_ _ -> showString "undefined"
-    match list nbranch cbranch = S $ \s p ->
-        let (s1, s2, ss) = S.split3 s
+
+instance SContext s => Exp (S s) where
+    nil = S $ \_ -> showString "[]"
+    undefined = S $ \_ -> showString "undefined"
+    match list nbranch cbranch = S $ \ctx ->
+        let (s1, s2, ss) = S.split3 (getL supply ctx)
             (s3, s4, s5) = S.split3 ss
             v1           = S.supplyValue s4
-            showV1       = S $ \_ _ -> showVar v1
+            showV1       = S $ \_ -> showVar v1
             v2           = S.supplyValue s5
-            showV2       = S $ \_ _ -> showVar v2
+            showV2       = S $ \_ -> showVar v2
+            p = getL prec ctx
         in showParen (p>0) $ 
             showString "case ".
-            unS list s1 0 .
+            unS list (updateCtx s1 0 ctx) .
             showString " of [] => ".
-            unS nbranch s2 0 .
+            unS nbranch (updateCtx s2 0 ctx) .
             showString "; (" .  showVar v1 . showChar ':' . showVar v2 . showString ") => " .
-            unS (cbranch showV1 showV2) s3 0
-    cond c tbranch fbranch = S $ \s p ->
-        let (s1, s2, s3) = S.split3 s
+            unS (cbranch showV1 showV2) (updateCtx s3 0 ctx)
+    cond c tbranch fbranch = S $ \ctx ->
+        let (s1, s2, s3) = S.split3 (getL supply ctx)
+            p = getL prec ctx
         in showParen (p>0) $ 
             showString "if ".
-            unS c s1 0 .
+            unS c (updateCtx s1 0 ctx).
             showString " then " .
-            unS tbranch s2 0 .
+            unS tbranch (updateCtx s2 0 ctx).
             showString " else " .
-            unS fbranch s3 0
+            unS fbranch (updateCtx s3 0 ctx)

sizechecking/branches/macs/Lambda.hs

@@ -1 @@
-{-# LANGUAGE TypeFamilies, GADTs #-}
+{-# LANGUAGE TypeFamilies, GADTs, Rank2Types, TemplateHaskell #-}
 
 module Lambda where
@@ -5 +5 @@
 import qualified Data.Supply as S
 import qualified Data.Char as C
-import Control.Monad.IO.Class (MonadIO, liftIO)
-import Data.IORef (newIORef, readIORef, writeIORef)
+import Data.Lens.Light 
 
 {-
@@ -29 +28 @@
 
 {-
- - show interpreter
- -}
+- show interpreter
+-}
 showVar :: Int -> String -> String
 showVar x = if x>28 
@@ -36 +35 @@
     else showChar $ C.chr $ C.ord 'a' + x
 
-newtype S a = S { unS :: S.Supply Int -> Int -> ShowS }
+class SContext a where
+  supply :: Lens a (S.Supply Int)
+  prec :: Lens a Int
 
-instance Lambda S where
-    lit a = S (\_ p -> showsPrec p a)
-    app (S fun) (S arg) = S (\s p -> 
-        let (s1, s2) = S.split2 s 
-        in showParen (p>6) $ fun s1 6 . showChar ' ' . arg s2 7)
-    lam fun = S (\s p -> 
-        let (s1, s2) = S.split2 s
+newtype S ctx a = S { unS :: ctx -> ShowS }
+
+instance SContext ctx => Lambda (S ctx) where
+    lit a = S (\ctx -> showsPrec (getL prec ctx) a)
+    app (S fun) (S arg) = S (\ctx ->
+        let (s1, s2) = S.split2 (getL supply ctx)
+            p = getL prec ctx
+        in showParen (p>6) $ fun (updateCtx s1 6 ctx) . showChar ' ' . arg (updateCtx s2 7 ctx))
+    lam fun = S (\ctx -> 
+        let (s1, s2) = S.split2 (getL supply ctx)
             v        = S.supplyValue s1
-            showV = S $ \_ _ -> showVar v
-        in showParen (p>0) $ showChar 'λ' . showVar v . showChar '.' . unS (fun showV) s2 0)
+            p        = getL prec ctx
+            showV = S $ \ctx -> showVar v
+        in showParen (p>0) $ showChar 'λ' . showVar v . showChar '.' . unS (fun showV) (updateCtx s2 0 ctx))
 
-ast :: S a -> IO ShowS
+updateCtx :: SContext ctx => S.Supply Int -> Int -> ctx -> ctx
+updateCtx s p = setL supply s . setL prec p
+
+data SData = SData { _getSDataSupply :: S.Supply Int, _getSDataPrec :: Int }
+$(makeLens ''SData)
+
+instance SContext SData where
+  supply = getSDataSupply
+  prec = getSDataPrec
+
+ast :: S SData a -> IO ShowS
 ast a = do
     s <- S.newSupply 0 (+1)
-    return $ unS a s 0
+    return $ unS a $ SData s 0
 
-printAst :: S a -> IO ()
+printAst :: S SData a -> IO ()
 printAst l = ast l >>= (\s -> putStrLn $ s "")
 
-
-{-
- - reduction
- -}
-data IR h t where
-    Lit :: Int -> IR h Int
-    App :: IR h (a -> b) -> IR h a -> IR h b
-    Lam :: (IR h a -> IR h b) -> IR h (a -> b)
-
-instance Lambda (IR h) where
-    lam = Lam
-    app = App
-    lit = Lit
-
-toFinal :: (Lambda l) => IR h t

sizechecking/branches/macs/Ops.hs

@@ -7 +7 @@
 import qualified Prelude
 import Lambda
+import Data.Lens.Light
 
 -- infix operatorok, ezek beagyazasa picit necces, lasd a type family kesobb
@@ -32 +33 @@
     fun _ = Q
 
-instance LOps S where
-    fun name _ = S (\_ p -> Prelude.showsPrec p name)
+instance (SContext s) => LOps (S s) where
+    fun name _ = S (\ctx -> Prelude.showsPrec (getL prec ctx) name)
 
-    infixopl name prec _ lhs rhs = S(\s p ->
-        let (s1, s2) = S.split2 s
-        in Prelude.showParen (p Prelude.> prec) $
-            unS lhs s1 prec .
+    infixopl name p _ lhs rhs = S(\ctx ->
+        let (s1, s2) = S.split2 (getL supply ctx)
+        in Prelude.showParen ((getL prec ctx) Prelude.> p) $
+            unS lhs (setL supply s1 $ setL prec p ctx) .
             Prelude.showString name .
-            unS rhs s2 (Prelude.succ prec)
+            unS rhs (setL supply s2 $ setL prec (Prelude.succ p) ctx)
         )
-    infixop name prec _ lhs rhs = S(\s p ->
-        let (s1, s2) = S.split2 s
-        in Prelude.showParen (p Prelude.> prec) $
-            unS lhs s1 (Prelude.succ prec) .
+
+    infixop  name p _ lhs rhs = S(\ctx ->
+        let (s1, s2) = S.split2 (getL supply ctx)
+        in Prelude.showParen ((getL prec ctx) Prelude.> p) $
+            unS lhs (setL supply s1 $ setL prec (Prelude.succ p) ctx) .
             Prelude.showString name .
-            unS rhs s2 (Prelude.succ prec)
+            unS rhs (setL supply s2 $ setL prec (Prelude.succ p) ctx)
         )
-    infixopr name prec _ lhs rhs = S(\s p ->
-        let (s1, s2) = S.split2 s
-        in Prelude.showParen (p Prelude.> prec) $
-            unS lhs s1 (Prelude.succ prec) .
+
+    infixopr name p _ lhs rhs = S(\ctx ->
+        let (s1, s2) = S.split2 (getL supply ctx)
+        in Prelude.showParen ((getL prec ctx) Prelude.> p) $
+            unS lhs (setL supply s1 $ setL prec (Prelude.succ p) ctx) .
             Prelude.showString name .
-            unS rhs s2 prec
+            unS rhs (setL supply s2 $ setL prec p ctx)
         )

sizechecking/branches/macs/Size.hs

@@ -8 +8 @@
 import Ops
 import Data.Supply as S
+import Data.Lens.Light
 
 data Unsized
@@ -19 +20 @@
 
 
-instance Size S where
-    unsized = S $ \_ _ -> showChar 'U'
-    bottom = S $ \_ _ -> showChar '┮'
-    list size sexp = S $ \s p ->
-        let (s1, s2) = S.split2 s
+instance SContext s => Size (S s) where
+    unsized = S $ \_ -> showChar 'U'
+    bottom = S $ \_ -> showChar '┮'
+    list size sexp = S $ \ctx ->
+        let (s1, s2) = S.split2 (getL supply ctx)
+            p = getL prec ctx
         in showParen (p>0) $
             showString "List " .
-            unS size s1 9 .
+            unS size (updateCtx s1 9 ctx) .
             showChar ' ' .
-            unS sexp s2 9
-    slam f = S $ \s p ->
-        let (s1, s2, s3) = S.split3 s
+            unS sexp (updateCtx s2 9 ctx)
+    slam f = S $ \ctx ->
+        let (s1, s2, s3) = S.split3 (getL supply ctx)
             v1           = S.supplyValue s1
-            showV1       = S $ \_ _ -> showVar v1
+            showV1       = S $ \_ -> showVar v1
             v2           = S.supplyValue s2
-            showV2       = S $ \_ _ -> showVar v2
+            showV2       = S $ \_ -> showVar v2
+            p = getL prec ctx
         in showParen (p>0) $
             showChar 'Λ' .
@@ -41 +44 @@
             showVar v2 .
             showChar '.' .
-            unS (f showV1 showV2) s3 0
-    shift e1 ss e2 = S $ \s p ->
-        let (s1, s2, s3) = S.split3 s
+            unS (f showV1 showV2) (updateCtx s3 0 ctx)
+    shift e1 ss e2 = S $ \ctx ->
+        let (s1, s2, s3) = S.split3 (getL supply ctx)
+            p = getL prec ctx
         in showParen (p>0)
         $ showString "Shift "
-        . unS e1 s1 2
+        . unS e1 (updateCtx s1 2 ctx)
         . showChar ' '
-        . unS ss s2 2
+        . unS ss (updateCtx s2 2 ctx)
         . showChar ' '
-        . unS e2 s3 2
+        . unS e2 (updateCtx s3 2 ctx)
 

sizechecking/branches/macs/Tests/ExpTest.hs

@@ -30 +30 @@
 testD2Cons = cons (cons (lit 1) nil) nil
 
-checkAST :: S a -> String -> IO Bool
+checkAST :: S SData a -> String -> IO Bool
 checkAST exp repr = ast exp >>= (\t -> return $ t "" == repr )
 

sizechecking/branches/macs/Tests/SizeTest.hs

@@ -21 +21 @@
 testTail = slam $ \s f -> list (s - lit 1) f
 
+testAddOne :: (Size l) => l ([Unsized] -> [Unsized])
+testAddOne = slam $ \s f -> list (s + lit 1) (lam $ const unsized)
+
 testCons :: Size l => l (a -> [a] -> [a])
 testCons = lam $ \x -> slam $ \s f ->
     list (s + lit 1) $ shift f s (lam $ const x)
 
-checkAst :: S a -> String -> IO Bool
+testConcat :: Size l => l ([a] -> [a] -> [a])
+testConcat = slam $ \s1 f1 -> slam $ \s2 f2 ->
+    list (s1 + s2) $ shift f1 s1 f2
+
+
+checkAst :: S SData a -> String -> IO Bool
 checkAst exp repr = ast exp >>= (\t -> return $ t "" == repr)
 

sizechecking/branches/macs/sizechecking.cabal

@@ -55 +55 @@
   -- Other library packages from which modules are imported.
   build-depends:       base ==4.*, containers ==0.5.*, sbv, value-supply,
-                       transformers
+                       transformers, data-lens-light