[start switching from lambda cube to a PTS
John Meacham <john@repetae.net>**20061010044605] hunk ./E/E.hs 29
+-- We are now based on a PTS, which is
+-- a generalization of the lambda cube
+-- see E.TypeCheck for a description
+-- of the type system.
hunk ./E/TypeCheck.hs 16
+import qualified Data.Map as Map
hunk ./E/TypeCheck.hs 34
+-- PTS type checker
+-- core is the following PTS
+-- S = (*,#,Box)
+-- A = (*::Box,#::Box)
+-- R = (*,*,*) (*,#,*) (#,#,*) (#,*,*) (Box,*,*) (Box,#,*) (Box,Box,Box)
+--
+-- * is the sort of boxed values
+-- # is the sort of unboxed values
+-- notice that functions are always boxed
+--
+-- this PTS is functional but not injective
+
+
+ptsAxioms = [
+    (EStar,EBox),
+    (EHash,EBox)
+    ]
+
+ptsRules = [
+    (EStar,EStar,EStar),  -- Int -> Int :: *
+    (EStar,EHash,EStar),  -- Int -> Int# :: *
+    (EHash,EStar,EStar),  -- Int# -> Int :: *
+    (EHash,EHash,EStar),  -- Int# -> Int# :: *
+    (EBox,EStar,EStar),   -- forall x . Foo x :: *
+    (EBox,EHash,EStar),   -- forall x . Int# :: *
+    (EBox,EBox,EBox)      -- * -> * :: Box
+    ]
+
+ptsRulesMap = Map.fromList [ ((a,b),c) | (a,b,c) <- ptsRules ]
+
+
hunk ./E/TypeCheck.hs 71
-typ (ESort EStar) =  eBox
-typ (ESort EHash) =  eBox
-typ (ESort EBox) = error "Box inhabits nowhere."
+typ (ESort s) = case lookup s ptsAxioms of
+    Just r -> ESort r
+    Nothing -> error "Box inhabits nowhere"
hunk ./E/TypeCheck.hs 89
+
+-- * -> Int#
+
+-- * -> *
+
+sortOf e = f e where
+    f (ESort s) = lookup s ptsAxioms
+    f (EVar TVr { tvrType = ESort t }) = return t
+    f (EPi TVr { tvrType = a } b) = do
+        a' <- f a
+        b' <- f b
+        Map.lookup (a',b') ptsRulesMap
+--    f (EAp x y) = Map.lookup
+--        EPi _ b = getType x
+