Changeset 17

Timestamp:

Oct 27, 2013, 9:55:17 PM (12 years ago)

Author:

gobi

Message:

copyu

Location:

sizechecking

Files:

• Constraints.hs (modified) (1 diff)
• Examples.hs (modified) (1 diff)
• Lambda.hs (modified) (1 diff)
• Setup.hs (modified) (1 diff)
• SizedExp.hs (modified) (6 diffs)
• Test.hs (modified) (1 diff)

sizechecking/Constraints.hs

@@ +1 @@
+--
+-- Copyright (C) 2012 Attila Gobi - http://kp.elte.hu/sizechecking
+--
+
 {-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances,
              IncoherentInstances, RankNTypes, ScopedTypeVariables,

sizechecking/Examples.hs

@@ +1 @@
+--
+-- Copyright (C) 2012 Attila Gobi - http://kp.elte.hu/sizechecking
+--
+
 {-# LANGUAGE ScopedTypeVariables, ExistentialQuantification, Rank2Types #-}
 module Examples where

sizechecking/Lambda.hs

@@ +1 @@
+--
+-- Copyright (C) 2012 Attila Gobi - http://kp.elte.hu/sizechecking
+--
+
 module Lambda where
 

sizechecking/Setup.hs

@@ +1 @@
+--
+-- Copyright (C) 2012 Attila Gobi - http://kp.elte.hu/sizechecking
+--
+
 import Distribution.Simple
 main = defaultMain

sizechecking/SizedExp.hs

@@ -2 +2 @@
              IncoherentInstances, RankNTypes, ScopedTypeVariables,
              FlexibleContexts,UndecidableInstances #-}
+--
+-- Copyright (C) 2012 Attila Gobi - http://kp.elte.hu/sizechecking
+--
 
 module SizedExp  where
---    (
---        SizedExp(..), ($), unQ, prove
---    ) where
 
-import Lambda as L 
-import Constraints 
+import Lambda as L
+import Constraints
 import Data.Supply
 import Control.Arrow
@@ -15 +15 @@
 
 class TS b => (Unify se a b)  where
-    unify :: (forall a b c. (TS c, Unify se a b) => c -> (Size se c -> a) -> (Size se (c -> b), d)) -> 
-        (b -> Size se b -> (Size se b, d)) -> 
+    unify :: (forall a b c. (TS c, Unify se a b) => c -> (Size se c -> a) -> (Size se (c -> b), d)) ->
+        (b -> Size se b -> (Size se b, d)) ->
         a -> (Size se b, d)
 
@@ -56 +56 @@
 fresh :: TypeKind -> Supply Int -> L
 fresh sig var = fresh' sig [] var
-    where 
+    where
     fresh' U _ _ = Unsized
     fresh' V l var = appall (supplyValue var) l
@@ -74 +74 @@
 
 freshvars :: (TS c, Unify Q a b) => Supply Int -> c -> (Size Q c -> a) -> (Size Q (c -> b), L -> L)
-freshvars supply q = freshvars' (unify (freshvars s1) (freshvars2 s2)) 
-    where 
+freshvars supply q = freshvars' (unify (freshvars s1) (freshvars2 s2))
+    where
     (s1, s2, s3) = split3 supply
     freshvars' :: (Unify Q a b) => (a -> (Size Q b, L -> L)) -> (Size Q c -> a) -> (Size Q (c -> b), L -> L)
     freshvars' u exp = (QSynt $ sizeof x, \l -> f $ App l fv)
         where
-        (x, f) = u $ exp $ QSynt $ do 
---            putStrLn $ "[Bind] var="++ show fv ++" of type "++ show (tk q)
+        (x, f) = u $ exp $ QSynt $ do
             return [([], fv)]
         fv = fresh (tk q) s3
@@ -100 +99 @@
             match1 (cond, ltype) = do
                     x <- sizeof l
---                    putStrLn $ "ORIGINAL is " ++ show x
---                    putStrLn $ "[MATCH] ==> " ++ show ltype
                     let lt = rall$  App (AAbs 18 5 $ Var 18) ltype
---                    putStrLn $ " --- NIL  ---" ++ show lt
                     nils <- sizeof nil
---                    print nils
                     let nilc = foldr addConstraint nils $ Zero lt:cond
                     let tx = rall $ App (AAbs 18 5 $ App (Var 5) (Op (Var 18) '-' (Num 1))) ltype
                     let txs = rall $App (AAbs 18 5 $ List (Op (Var 18) '-' (Num 1)) (Var 5)) ltype
---                    putStrLn $ " --- CONS --- "++ show tx ++" <-> "++ show txs
                     conss <- sizeof $ cons (QSynt$return [([], tx)]) (QSynt$return [([], txs)])
---                    print conss
                     let consc = foldr addConstraint conss $ lt `GEC` Num 1:cond
---                    print "END MATCH"
---                    print  $ nilc ++ consc
                     return $ nilc ++ consc
-        in QSynt $ sizeof l >>= concatMapM match1 
+        in QSynt $ sizeof l >>= concatMapM match1
 
-    iff _ l1 l2 = QSynt $ do 
+    iff _ l1 l2 = QSynt $ do
         ll1 <- sizeof l1
         ll2 <- sizeof l2
@@ -137 +128 @@
                 rr (GEC a b) = rall a `GEC` rall b
                 rr (LTC a b) = rall a `LTC` rall b
-            in do 
-                l3 <- sizeof sexp 
---                print l
---                print ll
+            in do
+                l3 <- sizeof sexp
                 return $ map (\(c,l2) -> Condition (map rr c) ll (rall l2)) l3
 

sizechecking/Test.hs

@@ +1 @@
+--
+-- Copyright (C) 2012 Attila Gobi - http://kp.elte.hu/sizechecking
+--
+
 module Main where
 import Examples (runTests)