Changeset 10

Timestamp:

Nov 14, 2012, 8:45:28 PM (13 years ago)

Author:

gobi

Message:

adding a new implementation of Lambda

Files:

• sizechecking/Examples.hs (modified) (1 diff)
• sizechecking_branches (added)
• sizechecking_branches/L.hs (moved) (moved from sizechecking/L.hs) (3 diffs)
• sizechecking_branches/LL.hs (added)

sizechecking/Examples.hs

@@ -210 +210 @@
 comp :: (SizedExp se)  => Size se ( (b->c) -> (a->b) -> a->c )
 comp = bind comps $ \f g x -> f `app` (g `app` x)
+
+test1s = Abs 2 $ AAbs 19 6 $ (Var 2) `App` (List (Var 19) (Var 6))
+test1 :: (SizedExp se)  => Size se (([a] -> [b]) -> [a] -> [b])
+test1 = bind test1s $ \f l -> match (f `app` l) nil (\x xs -> f `app` l)
+
+
+test2s = Abs 2 $ AAbs 18 5  $ appends `App` (Var 2 `App` (List (Var 18) (Var 5))) `App` (List (Var 18) (Var 5))
+test2 :: (SizedExp se)  => Size se (([a] -> [a]) -> [a] -> [a])
+test2 = bind test2s $ \f l -> append `app` (f `app` l) `app` l
 
 data TestCase = forall a . TestCase P.String (forall se. SizedExp se => Size se a)

sizechecking_branches/L.hs

@@ -1 @@
-{-# Language GADTs, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, FunctionalDependencies, ScopedTypeVariables, TypeFamilies, NoMonomorphismRestriction #-}
+{-# Language GADTs, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, FunctionalDependencies, ScopedTypeVariables, TypeFamilies, NoMonomorphismRestriction, OverlappingInstances #-}
+module L where
 
 import Data.Char(ord, chr)
@@ -11 +12 @@
 {- Lambda calculus without free variables -}
 type Arr repr a b = repr a -> repr b
---type family Arr (repr :: * -> *) (a :: *) (b :: *) :: *
 
 class Lambda l where
@@ -26 +26 @@
     undef   :: l Bottom
     unsized :: l ()
+
+instance Lambda l => Show (l a) where
+    showsPrec _ e = error "Error: no show"
+
+instance Lambda l => Eq (l a) where
+    (==) _ _ = error "Error: no eq"
 
 instance Lambda l => Num (l Int) where