[new type system for core, with a much more interesting kind hierarchy
John Meacham <john@repetae.net>**20061118035222] hunk ./DataConstructors.hs 524
-    | sortStarLike kind, (e,ts) <- fromPi kind = drop (length ts) (conSlots mc)
+    | sortKindLike kind, (e,ts) <- fromPi kind = drop (length ts) (conSlots mc)
hunk ./E/E.hs 57
-    EStar     -- ^ the sort of types
-    | EHash   -- ^ the sort of unboxed types
-    | EBox    -- ^ the sort of types of types
+    EStar         -- ^ the sort of boxed lazy types
+    | EBang       -- ^ the sort of boxed strict types
+    | EHash       -- ^ the sort of unboxed types
+    | ETuple      -- ^ the sort of unboxed tuples
+    | EHashHash   -- ^ the supersort of unboxed types
+    | EStarStar   -- ^ the supersort of boxed types
+    | ESortNamed Name -- ^ user defined sorts
hunk ./E/E.hs 70
-    showsPrec _ EBox = showString "BOX"
+    showsPrec _ EStarStar = showString "**"
+    showsPrec _ EHashHash = showString "##"
+    showsPrec _ ETuple = showString "(#)"
+    showsPrec _ EBang = showString "!"
+
hunk ./E/E.hs 257
-eBox :: E
-eBox = ESort EBox
-
hunk ./E/FromHs.hs 173
-argTypes e = span ((== eBox) . getType) (map tvrType xs) where
+argTypes e = span (sortSortLike . getType) (map tvrType xs) where
hunk ./E/FromHs.hs 203
-            maine = foldl EAp (EVar tvm) [ tAbsurd k |  TVr { tvrType = k } <- xs, sortStarLike k ]
+            maine = foldl EAp (EVar tvm) [ tAbsurd k |  TVr { tvrType = k } <- xs, sortKindLike k ]
hunk ./E/FromHs.hs 224
-        (args,_rargs) = span (sortStarLike . getType)  args'
+        (args,_rargs) = span (sortKindLike . getType)  args'
hunk ./E/FromHs.hs 280
-            ts <- flip mapM (filter (sortStarLike . getType) $ freeVars e1) $ \tvr -> do
+            ts <- flip mapM (filter (sortKindLike . getType) $ freeVars e1) $ \tvr -> do
hunk ./E/FromHs.hs 361
-        es <- newVars [ t |  t <- ts, not (sortStarLike t) ]
+        es <- newVars [ t |  t <- ts, not (sortKindLike t) ]
hunk ./E/FromHs.hs 380
-        es <- newVars [ t |  t <- ts, not (sortStarLike t) ]
+        es <- newVars [ t |  t <- ts, not (sortKindLike t) ]
hunk ./E/FromHs.hs 555
-                    (args,rargs) = span (sortStarLike . getType) as
+                    (args,rargs) = span (sortKindLike . getType) as
hunk ./E/LambdaLift.hs 148
-        g ec@ECase { eCaseScrutinee = (EVar v), eCaseAlts = as, eCaseDefault = d} | sortStarLike (tvrType v) = do
+        g ec@ECase { eCaseScrutinee = (EVar v), eCaseAlts = as, eCaseDefault = d} | sortKindLike (tvrType v) = do
hunk ./E/LambdaLift.hs 165
-                ss = filter (sortStarLike . tvrType) fvs'
+                ss = filter (sortKindLike . tvrType) fvs'
hunk ./E/LetFloat.hs 101
-canFloatPast t | sortStarLike . getType $ t = True
+canFloatPast t | sortKindLike . getType $ t = True
hunk ./E/Show.hs 169
-        f (ESort EStar) = return $ symbol (text "*")
-        f (ESort EBox) = return $ symbol UC.box
-        f (ESort EHash) = return $ symbol (text "#")
+        f (ESort s) = return $ symbol (tshow s)
hunk ./E/TypeAnalysis.hs 47
-    f (ELam tvr e) rs | sortStarLike (getType tvr) = f e (runIdentity (Info.lookup $ tvrInfo tvr):rs)
+    f (ELam tvr e) rs | sortKindLike (getType tvr) = f e (runIdentity (Info.lookup $ tvrInfo tvr):rs)
hunk ./E/TypeAnalysis.hs 98
-        tls = takeWhile (sortStarLike . getType) ls
+        tls = takeWhile (sortKindLike . getType) ls
hunk ./E/TypeAnalysis.hs 133
-    d (t,e) | not (sortStarLike (getType t)) = return ()
+    d (t,e) | not (sortKindLike (getType t)) = return ()
hunk ./E/TypeAnalysis.hs 166
---calcE env ec@ECase {} | sortStarLike (getType $ eCaseScrutinee ec) = do
+--calcE env ec@ECase {} | sortKindLike (getType $ eCaseScrutinee ec) = do
hunk ./E/TypeAnalysis.hs 184
-        when (sortStarLike (getType a)) $ do
+        when (sortKindLike (getType a)) $ do
hunk ./E/TypeAnalysis.hs 226
-    prune ec@ECase { eCaseScrutinee = EVar v } | sortStarLike (getType v), Just vm <- Info.lookup (tvrInfo v) = do
+    prune ec@ECase { eCaseScrutinee = EVar v } | sortKindLike (getType v), Just vm <- Info.lookup (tvrInfo v) = do
hunk ./E/TypeAnalysis.hs 280
-    spec t | Just nt <- Info.lookup (tvrInfo t) >>= getTyp (getType t) dataTable, sortStarLike (getType t) = (t,Just (repi nt))
+    spec t | Just nt <- Info.lookup (tvrInfo t) >>= getTyp (getType t) dataTable, sortKindLike (getType t) = (t,Just (repi nt))
hunk ./E/TypeCheck.hs 6
-    sortStarLike,
+    sortSortLike,
+    sortKindLike,
hunk ./E/TypeCheck.hs 41
--- S = (*,#,Box)
--- A = (*::Box,#::Box)
--- R = (*,*,*) (*,#,*) (#,#,*) (#,*,*) (Box,*,*) (Box,#,*) (Box,Box,Box)
+-- S = (*,!,**,#,(#),##)
+-- A = (*::**,#::##,(#)::##,!::**)
+--
hunk ./E/TypeCheck.hs 46
+-- ! is the sort of boxed strict values
+-- ** is the supersort of all boxed value
hunk ./E/TypeCheck.hs 49
--- notice that functions are always boxed
+-- (#) is the sort of unboxed tuples
+-- ## is the supersort of all unboxed values
+-- we also have user defined kinds, which are always of supersort ##
+--
+-- notice that functions are always boxed, but may be strict if they take an unboxed tuple as an argument
+
+--  -- these rules apply to lambda abstractions, data constructors can be _defined_ to have types that would be invalid otherwise
+-- as a shortcut we will use *# to mean either * or # and so forth
+--
+-- so (*#,*#,*) means (*,*,*) (#,*,*) (*,#,*) (#,#,*)
+--
+-- R =
+--    (*#!,*#!,*)
+--    (*#!,(#),*)
+--    ((#),*#!,!)
+--    ((#),(#),!)
+--    (**,*,*)  -- may have a function from an unboxed type to a value
+--    (**,#,*)
+--    (**,!,*)
+--    (**,**,**)  -- we have functions from types to types
+--    (**,##,##)  -- Array__ a :: #
+--
+-- _|_ :: t iff t::*
hunk ./E/TypeCheck.hs 76
-ptsAxioms = [
-    (EStar,EBox),
-    (EHash,EBox)
-    ]
hunk ./E/TypeCheck.hs 77
-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
+ptsAxioms :: Map.Map ESort ESort
+ptsAxioms = Map.fromList [
+    (EStar,EStarStar),
+    (EBang,EStarStar),
+    (EHash,EHashHash),
+    (ETuple,EHashHash)
hunk ./E/TypeCheck.hs 85
-ptsRulesMap = Map.fromList [ ((a,b),c) | (a,b,c) <- ptsRules ]
+ptsRulesMap :: Map.Map (ESort,ESort) ESort
+ptsRulesMap = Map.fromList [ ((a,b),c) | (as,bs,c) <- ptsRules, a <- as, b <- bs  ] where
+    starHashBang = [EStar,EHash,EBang]
+    ptsRules = [
+        (starHashBang,ETuple:starHashBang,EStar),
+        ([ETuple],ETuple:starHashBang,EBang),
+        ([EStarStar],starHashBang,EStar),
+        ([EStarStar],[EStarStar],EStarStar),
+        ([EStarStar],[EHashHash],EHashHash)
+        ]
hunk ./E/TypeCheck.hs 97
-canBeBox EPi {} = True
hunk ./E/TypeCheck.hs 102
-typ (ESort s) = case lookup s ptsAxioms of
+typ (ESort s) = case Map.lookup s ptsAxioms of
hunk ./E/TypeCheck.hs 104
-    Nothing -> error "Box inhabits nowhere"
+    Nothing -> error ("TypeOf: " ++ show s)
hunk ./E/TypeCheck.hs 107
-typ (EPi _ b) = typ b
+typ e@(EPi TVr { tvrType = a } b)
+    | typa == Unknown || typb == Unknown = Unknown
+    | otherwise = maybe (error $ "getType: " ++ show e) ESort $ do
+        ESort s1 <- return $ typ a
+        ESort s2 <- return $ typ b
+        Map.lookup (s1,s2) ptsRulesMap
+    where typa = typ a; typb = typ b
hunk ./E/TypeCheck.hs 115
--- typ e@(EAp (ELit LitCons { litType = ty }) b) | ty == eStar = eStar -- XXX functions might have unboxed return types in the future
--- XXX the following should never occur
hunk ./E/TypeCheck.hs 118
-typ (EAp a b) = eAp (typ a) b
+typ (EAp a b) = if typa == Unknown then Unknown else eAp typa b where typa = typ a
hunk ./E/TypeCheck.hs 127
--- * -> 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
-
-
+instance CanType ESort ESort where
+    getType s = case Map.lookup s ptsAxioms of
+        Just s -> s
+        Nothing -> error $ "getType: " ++ show s
hunk ./E/TypeCheck.hs 141
-sortStarLike e = e /= eBox && getType e == eBox
-sortTypeLike e = e /= eBox && not (sortStarLike e) && sortStarLike (getType e)
-sortTermLike e = e /= eBox && not (sortStarLike e) && not (sortTypeLike e) && sortTypeLike (getType e)
+sortSortLike e = e == ESort EHashHash || e == ESort EStarStar
+sortKindLike e = not (sortSortLike e) && sortSortLike (getType e)
+sortTypeLike e = not (sortSortLike e) && not (sortKindLike e) && sortKindLike (getType e)
+sortTermLike e = not (sortSortLike e) && not (sortKindLike e) && not (sortTypeLike e) && sortTypeLike (getType e)
hunk ./E/TypeCheck.hs 184
-    fc (EPi (TVr { tvrIdent = n, tvrType =  at}) b) = valid at >> rfc' [ d | d@(v,_) <- ds, tvrIdent v /= n ] b
+    fc (EPi (TVr { tvrIdent = n, tvrType =  at}) b) = do
+        ESort a <- rfc at
+        ESort b <- rfc' [ d | d@(v,_) <- ds, tvrIdent v /= n ] b
+        liftM ESort $ Map.lookup (a,b) ptsRulesMap
+        --valid at >> rfc' [ d | d@(v,_) <- ds, tvrIdent v /= n ] b
hunk ./E/TypeCheck.hs 199
-            --b <- strong' b
hunk ./E/TypeCheck.hs 200
-        {-
-        case followAliases dataTable a' of
-            (EPi tvr@(TVr { tvrType =  t}) v) -> do
-                valid t
-                withContextDoc (hsep [text "Application: ", parens $ prettyE a <> text "::" <> prettyE a', parens $ prettyE b]) $ fceq ds b t
-                b' <- if sortStarLike t then strong' b else return b
-                nt <- return (subst tvr b' v)
-                valid nt
-                return nt
-            x -> fail $ "App: " ++ render (tupled [ePretty x,ePretty a, ePretty a', ePretty b])
-            -}
hunk ./E/TypeCheck.hs 258
+    valid' nds ESort {} = return ()
hunk ./E/TypeCheck.hs 260
-        | s == eBox = return ()
hunk ./E/TypeCheck.hs 285
-    typecheck _ tvr = return $ getType tvr
+    typecheck dt tvr = do
+        typecheck dt (getType tvr)
+        return $ getType tvr
hunk ./E/TypeCheck.hs 290
-    typecheck _ l = return $ getType l
+    typecheck  dt LitCons { litType = t } = typecheck dt t >> return t
+    typecheck  dt LitInt  { litType = t } = typecheck dt t >> return t
hunk ./E/TypeCheck.hs 295
-    typecheck dt (Alt _ e) = typecheck dt e
+    typecheck dt (Alt l e) = typecheck dt l >> typecheck dt e
hunk ./E/TypeCheck.hs 333
-    prettyE = ePrettyEx
-    rfc e =  withContextDoc (text "fullCheck':" </> prettyE e) (fc e >>=  strong')
-    rfc' nds e =  withContextDoc (text "fullCheck':" </> prettyE e) (inferType' nds  e >>=  strong')
-    strong' e = withContextDoc (text "Strong':" </> prettyE e) $ strong ds e
+    rfc e =  withContextDoc (text "fullCheck':" </> ePrettyEx e) (fc e >>=  strong')
+    rfc' nds e =  withContextDoc (text "fullCheck':" </> ePrettyEx e) (inferType' nds  e >>=  strong')
+    strong' e = withContextDoc (text "Strong':" </> ePrettyEx e) $ strong ds e
hunk ./E/TypeCheck.hs 341
-    fc (EPi TVr { tvrIdent = n, tvrType = at} b) =  rfc' [ d | d@(v,_) <- ds, tvrIdent v /= n ] b
+    fc (EPi TVr { tvrIdent = n, tvrType = at} b) =  do
+        ESort a <- rfc at
+        ESort b <- rfc' [ d | d@(v,_) <- ds, tvrIdent v /= n ] b
+        liftM ESort $ Map.lookup (a,b) ptsRulesMap
hunk ./E/TypeCheck.hs 365
-    fc e = failDoc $ text "what's this? " </> (prettyE e)
+    fc e = failDoc $ text "what's this? " </> (ePrettyEx e)
hunk ./E/Values.hs 119
-    | sortStarLike ty && isAtomic e = subst t e e'
-    | sortStarLike ty = ELetRec [(t,e)] (typeSubst mempty (msingleton (tvrIdent t) e) e')
+    | sortKindLike ty && isAtomic e = subst t e e'
+    | sortKindLike ty = ELetRec [(t,e)] (typeSubst mempty (msingleton (tvrIdent t) e) e')
hunk ./E/Values.hs 126
-eStrictLet t@(TVr { tvrType =  ty }) v e | sortStarLike ty  = eLet t v e
+eStrictLet t@(TVr { tvrType =  ty }) v e | sortKindLike ty  = eLet t v e
hunk ./E/Values.hs 132
-    tas = filter (sortStarLike . tvrType . fst) nas
+    tas = filter (sortKindLike . tvrType . fst) nas
hunk ./E/Values.hs 140
-    tas = filter (sortStarLike . tvrType . fst) nas
+    tas = filter (sortKindLike . tvrType . fst) nas
hunk ./Grin/FromE.hs 224
-        n | sortStarLike (conType c) = convertName (conName c)
+        n | sortKindLike (conType c) = convertName (conName c)
hunk ./Grin/MangleE.hs 28
-import E.TypeCheck(sortStarLike)
+import E.TypeCheck(sortKindLike)
hunk ./Grin/MangleE.hs 92
-good tvr = sortStarLike (tvrType tvr)
+good tvr = sortKindLike (tvrType tvr)
hunk ./Main.hs 628
-            ts' = takeWhile (sortStarLike . getType) ts
+            ts' = takeWhile (sortKindLike . getType) ts