ref: 7ff283ebf5c2d4ce75e27bbc41b4d38d9983c7f4
parent: 75145b53a7b58235f199f526df415e1be0416a99
author: Lennart Augustsson <lennart.augustsson@epicgames.com>
date: Sun Oct 15 12:20:02 EDT 2023
Update for new Class and Instance
--- a/comb/mhs.comb
+++ b/comb/mhs.comb
@@ -1,3 +1,3 @@
v4.0
-983
-((A :0 _867) ((A :1 ((B _913) _0)) ((A :2 (((S' _913) _0) I)) ((A :3 _837) ((A :4 (_3 "undefined")) ((A :5 I) ((A :6 (((C' B) _866) ((C _75) _5))) ((A :7 (((C' _6) (_884 _72)) ((_75 _882) _71))) ((A :8 ((B ((S _913) _882)) _3)) ((A :9 T) ((A :10 (T I)) ((A :11 ((B (_75 _190)) _10)) ((A :12 ((B (B (_74 _9))) (((C' B) ((B C) _10)) (B _10)))) ((A :13 ((B (B (_74 _9))) (((C' B) ((B C) _10)) (BK _10)))) ((A :14 ((B (_74 _9)) P)) ((A :15 ((B (B (_74 _9))) ((B ((C' C) _10)) (B P)))) ((A :16 _15) ((A :17 (((C' B) _12) (((C' B) _12) (B _14)))) ((A :18 ((B (_74 _9)) (B (P _795)))) ((A :19 ((B (_74 _9)) (BK (P _795)))) ((A :20 ((_74 _9) ((S P) I))) ((A :21 ((B (_74 _9)) ((C (S' P)) I))) ((A :22 ((B Y) ((B (B (P (_14 _115)))) (((C' B) ((B (C' B)) (B _12))) (((C' (C' B)) (B _12)) ((B (B _14)) _116)))))) ((A :23 ((B Y) ((B (B (P (_14 _795)))) ((B (C' B)) (B _13))))) ((A :24 _3) ((A :25 (T (_14 _795))) ((A :26 (_22 _76)) ((A :27 (R _34)) ((A :28 (T _33)) ((A :29 ((P _34) _33)) ((A :30 _34) ((A :31 ((C ((C S') _29)) I)) ((A :32 ((C S) _29)) ((A :33 K) ((A :34 A) ((A :35 _842) ((A :36 _843) ((A :37 (((S' _28) (_834 #97)) ((C _834) #122))) ((A :38 (((S' _28) (_834 #65)) ((C _834) #90))) ((A :39 (((S' _27) _37) _38)) ((A :40 (((S' _28) (_834 #48)) ((C _834) #57))) ((A :41 (((S' _28) (_834 #32)) ((C _834) #126))) ((A :42 _831) ((A :43 _832) ((A :44 _834) ((A :45 _833) ((A :46 (((S' _27) ((C _42) #32)) (((S' _27) ((C _42) #9)) ((C _42) #10)))) ((A :47 ((S ((S (((S' _28) (_44 #65)) ((C _44) #90))) (_34 (((_794 "lib/Data/Char.hs") #3) #8)))) ((B _35) (((C' _82) (((C' _83) _36) (_36 #65))) (_36 #97))))) ((A :48 ((S ((S (((S' _28) (_44 #97)) ((C _44) #97))) (_34 (((_794 "lib/Data/Char.hs") #3) #8)))) ((B _35) (((C' _82) (((C' _83) _36) (_36 #97))) (_36 #65))))) ((A :49 _802) ((A :50 _803) ((A :51 _804) ((A :52 _805) ((A :53 (_50 %0.0)) ((A :54 _49) ((A :55 _50) ((A :56 _51) ((A :57 _52) ((A :58 _806) ((A :59 _807) ((A :60 _58) ((A :61 _59) ((A :62 _808) ((A :63 _809) ((A :64 _810) ((A :65 _811) ((A :66 _62) ((A :67 _63) ((A :68 _64) ((A :69 _65) ((A :70 _812) ((A :71 ((B BK) T)) ((A :72 (BK T)) ((A :73 P) ((A :74 I) ((A :75 B) ((A :76 I) ((A :77 K) ((A :78 C) ((A :79 _838) ((A :80 ((C ((C S') _190)) _191)) ((A :81 (((C' (S' (C' B))) B) I)) ((A :82 _796) ((A :83 _797) ((A :84 _798) ((A :85 _799) ((A :86 _800) ((A :87 _801) ((A :88 (_83 #0)) ((A :89 _819) ((A :90 _820) ((A :91 _821) ((A :92 _822) ((A :93 _823) ((A :94 _824) ((A :95 _89) ((A :96 (BK K)) ((A :97 ((B BK) ((B (B BK)) P))) ((A :98 ((B (B (B BK))) ((B (B (B BK))) ((B (B (B C))) ((B (B C)) P))))) ((A :99 (((S' S) (((S' (S' C)) (((C' (C' S)) (((C' B) ((B (S' S')) (((C' B) ((B _27) (_92 #0))) (_89 #0)))) ((B (B ((C' P) (_87 #1)))) _82))) (C P))) _85)) _86)) ((A :100 _96) ((A :101 (((S' C) ((B (P _178)) (((C' (C' B)) (((C' C) _89) _178)) _179))) ((B ((C' (C' (C' C))) (((C' (C' (C' C))) (((C' (C' (C' (C' S')))) ((B (B (B (B C)))) ((B ((C' (C' (C' C))) ((B (B (B ((S' S') (_89 #0))))) ((B ((C' (C' C)) ((B (B ((S' S') (_89 #1)))) ((B ((C' C) ((B ((C' S') (_89 #2))) (C _101)))) (C _101))))) (C _101))))) (C _101)))) (T K))) (T A)))) ((C _99) #4)))) ((A :102 (_108 _77)) ((A :103 ((_123 (_80 _102)) _100)) ((A :104 ((C (((C' B) ((P _115) (((C' (C' O)) P) K))) (((S' (C' (C' (C' B)))) ((B (B (B (B _105)))) (((S' (C' (C' B))) ((B (B (B _105))) (((S' (C' B)) ((B (B _105)) (((C' B) ((B _121) (T #0))) _104))) (((C' B) ((B _121) (T #1))) _104)))) (((C' B) ((B _121) (T #2))) _104)))) (((C' B) ((B _121) (T #3))) _104)))) ((B T) ((B (B P)) ((C' _82) (_84 #4)))))) ((A :105 ((S S) ((B BK) ((B BK) (((S' S) T) ((B BK) ((B BK) ((C (((S' C') S) ((B (B (B (S B)))) ((B (B (B (B (B BK))))) ((B ((S' (C' B)) ((B B') B'))) ((B (B (B (B (B (S B)))))) ((B (B (B (B (B (B (B BK))))))) (((C' B) (B' (B' ((B (C' (C' (C' C)))) ((B ((C' B) (B' ((B C) _91)))) ((B ((C' B) _116)) _105)))))) ((B ((C' B) _116)) (C _105)))))))))) (((_794 "lib/Data/IntMap.hs") #3) #8))))))))) ((A :106 ((_75 (_121 _190)) _104)) ((A :107 (((C' C) (((C' C) (C _101)) (_3 "Data.IntMap.!"))) I)) ((A :108 ((B ((C' B) T)) ((B (B Y)) (((C' (C' (S' (S' C)))) ((B
\ No newline at end of file
+995
+((A :0 _879) ((A :1 ((B _925) _0)) ((A :2 (((S' _925) _0) I)) ((A :3 _849) ((A :4 (_3 "undefined")) ((A :5 I) ((A :6 (((C' B) _878) ((C _75) _5))) ((A :7 (((C' _6) (_896 _72)) ((_75 _894) _71))) ((A :8 ((B ((S _925) _894)) _3)) ((A :9 T) ((A :10 (T I)) ((A :11 ((B (_75 _190)) _10)) ((A :12 ((B (B (_74 _9))) (((C' B) ((B C) _10)) (B _10)))) ((A :13 ((B (B (_74 _9))) (((C' B) ((B C) _10)) (BK _10)))) ((A :14 ((B (_74 _9)) P)) ((A :15 ((B (B (_74 _9))) ((B ((C' C) _10)) (B P)))) ((A :16 _15) ((A :17 (((C' B) _12) (((C' B) _12) (B _14)))) ((A :18 ((B (_74 _9)) (B (P _807)))) ((A :19 ((B (_74 _9)) (BK (P _807)))) ((A :20 ((_74 _9) ((S P) I))) ((A :21 ((B (_74 _9)) ((C (S' P)) I))) ((A :22 ((B Y) ((B (B (P (_14 _115)))) (((C' B) ((B (C' B)) (B _12))) (((C' (C' B)) (B _12)) ((B (B _14)) _116)))))) ((A :23 ((B Y) ((B (B (P (_14 _807)))) ((B (C' B)) (B _13))))) ((A :24 _3) ((A :25 (T (_14 _807))) ((A :26 (_22 _76)) ((A :27 (R _34)) ((A :28 (T _33)) ((A :29 ((P _34) _33)) ((A :30 _34) ((A :31 ((C ((C S') _29)) I)) ((A :32 ((C S) _29)) ((A :33 K) ((A :34 A) ((A :35 _854) ((A :36 _855) ((A :37 (((S' _28) (_846 #97)) ((C _846) #122))) ((A :38 (((S' _28) (_846 #65)) ((C _846) #90))) ((A :39 (((S' _27) _37) _38)) ((A :40 (((S' _28) (_846 #48)) ((C _846) #57))) ((A :41 (((S' _28) (_846 #32)) ((C _846) #126))) ((A :42 _843) ((A :43 _844) ((A :44 _846) ((A :45 _845) ((A :46 (((S' _27) ((C _42) #32)) (((S' _27) ((C _42) #9)) ((C _42) #10)))) ((A :47 ((S ((S (((S' _28) (_44 #65)) ((C _44) #90))) (_34 (((_805 "lib/Data/Char.hs") #3) #8)))) ((B _35) (((C' _82) (((C' _83) _36) (_36 #65))) (_36 #97))))) ((A :48 ((S ((S (((S' _28) (_44 #97)) ((C _44) #97))) (_34 (((_805 "lib/Data/Char.hs") #3) #8)))) ((B _35) (((C' _82) (((C' _83) _36) (_36 #97))) (_36 #65))))) ((A :49 _814) ((A :50 _815) ((A :51 _816) ((A :52 _817) ((A :53 (_50 %0.0)) ((A :54 _49) ((A :55 _50) ((A :56 _51) ((A :57 _52) ((A :58 _818) ((A :59 _819) ((A :60 _58) ((A :61 _59) ((A :62 _820) ((A :63 _821) ((A :64 _822) ((A :65 _823) ((A :66 _62) ((A :67 _63) ((A :68 _64) ((A :69 _65) ((A :70 _824) ((A :71 ((B BK) T)) ((A :72 (BK T)) ((A :73 P) ((A :74 I) ((A :75 B) ((A :76 I) ((A :77 K) ((A :78 C) ((A :79 _850) ((A :80 ((C ((C S') _190)) _191)) ((A :81 (((C' (S' (C' B))) B) I)) ((A :82 _808) ((A :83 _809) ((A :84 _810) ((A :85 _811) ((A :86 _812) ((A :87 _813) ((A :88 (_83 #0)) ((A :89 _831) ((A :90 _832) ((A :91 _833) ((A :92 _834) ((A :93 _835) ((A :94 _836) ((A :95 _89) ((A :96 (BK K)) ((A :97 ((B BK) ((B (B BK)) P))) ((A :98 ((B (B (B BK))) ((B (B (B BK))) ((B (B (B C))) ((B (B C)) P))))) ((A :99 (((S' S) (((S' (S' C)) (((C' (C' S)) (((C' B) ((B (S' S')) (((C' B) ((B _27) (_92 #0))) (_89 #0)))) ((B (B ((C' P) (_87 #1)))) _82))) (C P))) _85)) _86)) ((A :100 _96) ((A :101 (((S' C) ((B (P _178)) (((C' (C' B)) (((C' C) _89) _178)) _179))) ((B ((C' (C' (C' C))) (((C' (C' (C' C))) (((C' (C' (C' (C' S')))) ((B (B (B (B C)))) ((B ((C' (C' (C' C))) ((B (B (B ((S' S') (_89 #0))))) ((B ((C' (C' C)) ((B (B ((S' S') (_89 #1)))) ((B ((C' C) ((B ((C' S') (_89 #2))) (C _101)))) (C _101))))) (C _101))))) (C _101)))) (T K))) (T A)))) ((C _99) #4)))) ((A :102 (_108 _77)) ((A :103 ((_123 (_80 _102)) _100)) ((A :104 ((C (((C' B) ((P _115) (((C' (C' O)) P) K))) (((S' (C' (C' (C' B)))) ((B (B (B (B _105)))) (((S' (C' (C' B))) ((B (B (B _105))) (((S' (C' B)) ((B (B _105)) (((C' B) ((B _121) (T #0))) _104))) (((C' B) ((B _121) (T #1))) _104)))) (((C' B) ((B _121) (T #2))) _104)))) (((C' B) ((B _121) (T #3))) _104)))) ((B T) ((B (B P)) ((C' _82) (_84 #4)))))) ((A :105 ((S S) ((B BK) ((B BK) (((S' S) T) ((B BK) ((B BK) ((C (((S' C') S) ((B (B (B (S B)))) ((B (B (B (B (B BK))))) ((B ((S' (C' B)) ((B B') B'))) ((B (B (B (B (B (S B)))))) ((B (B (B (B (B (B (B BK))))))) (((C' B) (B' (B' ((B (C' (C' (C' C)))) ((B ((C' B) (B' ((B C) _91)))) ((B ((C' B) _116)) _105)))))) ((B ((C' B) _116)) (C _105)))))))))) (((_805 "lib/Data/IntMap.hs") #3) #8))))))))) ((A :106 ((_75 (_121 _190)) _104)) ((A :107 (((C' C) (((C' C) (C _101)) (_3 "Data.IntMap.!"))) I)) ((A :108 ((B ((C' B) T)) ((B (B Y)) (((C' (C' (S' (S' C)))) ((B
\ No newline at end of file
--- a/src/MicroHs/TypeCheck.hs
+++ b/src/MicroHs/TypeCheck.hs
@@ -652,7 +652,7 @@
tcDefs ds = T.do
T.mapM_ tcAddInfix ds
dst <- tcDefsType ds
- traceM (showEDefs dst)
+ --traceM (showEDefs dst)
T.mapM_ addTypeSyn dst
tcDefsValue dst
@@ -692,10 +692,10 @@
withTypeTable $ T.do
let
loop r [] = T.do
- kkr <- tcInferTypeT kr
+ kkr <- tInferTypeT kr
T.return (reverse r, kkr)
loop r (IdKind i k : iks) = T.do
- kk <- tcInferTypeT k
+ kk <- tInferTypeT k
withExtVal i kk $ loop (IdKind i kk : r) iks
loop [] vks
fun nvks nkr
@@ -738,17 +738,16 @@
tcDefType d = T.do
tcReset
case d of
- Data lhs cs -> Data lhs <$> withVars (snd lhs) (T.mapM tcConstr cs)
- Newtype lhs c t -> Newtype lhs c <$> withVars (snd lhs) (tcTypeT (Check kType) t)
- Type lhs t -> Type lhs <$> withVars (snd lhs) (tcInferTypeT t)
- Sign i t -> (Sign i ) <$> tcTypeT (Check kType) t
- ForImp ie i t -> (ForImp ie i) <$> tcTypeT (Check kType) t
- Class mc lhs m -> withVars (snd lhs) $ Class <$> tcCtx mc T.<*> T.return lhs T.<*> T.mapM tcMethod m
- Instance vs mc t m -> withVars vs $ Instance vs <$> tcCtx mc T.<*> tcTypeT (Check kConstraint) t T.<*> T.return m
- _ -> T.return d
+ Data lhs@(_, iks) cs -> withVars iks $ Data lhs <$> T.mapM tcConstr cs
+ Newtype lhs@(_, iks) c t -> withVars iks $ Newtype lhs c <$> tCheckTypeT kType t
+ Type lhs@(_, iks) t -> withVars iks $ Type lhs <$> tInferTypeT t
+ Sign i t -> Sign i <$> tCheckTypeT kType t
+ ForImp ie i t -> ForImp ie i <$> tCheckTypeT kType t
+ Class ctx lhs@(_, iks) ms -> withVars iks $ Class <$> tcCtx ctx T.<*> T.return lhs T.<*> T.mapM tcMethod ms
+ Instance iks ctx c m -> withVars iks $ Instance iks <$> tcCtx ctx T.<*> tCheckTypeT kConstraint c T.<*> T.return m
+ _ -> T.return d
where
- tcCtx Nothing = T.return Nothing
- tcCtx (Just c) = Just <$> tcTypeT (Check kConstraint) c
+ tcCtx = T.mapM (tCheckTypeT kConstraint)
tcMethod (BSign i t) = BSign i <$> tcTypeT (Check kType) t
tcMethod m = T.return m
@@ -763,12 +762,13 @@
tcConstr (Constr i ts) = Constr i <$> T.mapM (\ t -> tcTypeT (Check kType) t) ts
expandClassInst :: EDef -> T [EDef]
-expandClassInst d@(Class _ lhs m) = (d:) <$> expandClass lhs m
-expandClassInst d@(Instance vs mc _ m) = (d:) <$> expandInst vs mc m
+expandClassInst d@(Class ctx lhs m) = (d:) <$> expandClass ctx lhs m
+expandClassInst d@(Instance iks mc c m) = (d:) <$> expandInst iks mc c m
expandClassInst d = T.return [d]
-- Expand a class defintion to
-- * a type for the dictionary
+-- * superclass selectors
-- * method selectors
-- * default methods
-- E.g.
@@ -778,38 +778,48 @@
-- x /= y = not (x == y)
-- expands to
-- data Eq$Dict a = Eq (a -> a -> Bool) (a -> a -> Bool)
--- (==) :: forall a . Eq$Dict a -> (a -> a -> Bool)
--- (==) (Eq x _) = x
--- (/=) :: forall a . Eq$Dict a -> (a -> a -> Bool)
--- (/=) (Eq _ x) = x
--- (==$dflt) :: forall a . (Eq a) => (a -> a -> Bool)
--- (==$dflt) = _noDefault "Eq.=="
--- (/=$dflt) :: forall a . (Eq a) => (a -> a -> Bool)
--- (/=$dflt) x y = not (x == y)
+-- Eq$== :: forall a . Eq$Dict a -> (a -> a -> Bool)
+-- Eq$== (Eq x _) = x
+-- Eq$/= :: forall a . Eq$Dict a -> (a -> a -> Bool)
+-- Eq$/= (Eq _ x) = x
+-- Eq$==$dflt :: forall a . (Eq a) => (a -> a -> Bool)
+-- Eq$==$dflt = _noDefault "Eq.=="
+-- Eq$/=$dflt :: forall a . (Eq a) => (a -> a -> Bool)
+-- Eq$/=$dflt x y = not (x == y)
--
-expandClass :: LHS -> [EBind] -> T [EDef]
-expandClass (iCls, vs) ms = T.do
+expandClass :: [EConstraint] -> LHS -> [EBind] -> T [EDef]
+expandClass sups (iCls, vs) ms = T.do
mn <- gets moduleName
- let iDict = addIdentSuffix iCls "Dict" {-"$Dict"-}+ supTys <- T.mapM clsToDict sups
+ let iDict = mkDictId iCls -- dictionary type name
meths = [ b | b@(BSign _ _) <- ms ]
mdflts = [ (i, eqns) | BFcn i eqns <- ms ]
+ methTys = map (\ (BSign _ t) -> t) meths
nMeths = length meths
- iCon = iCls
- dData = Data (iDict, vs) [Constr iCon $ map (\ (BSign _ t) -> t) meths]
+ nSups = length sups
+ nArgs = nSups + nMeths
+ iCon = iDict -- dictionary constructor name
+ dData = Data (iDict, vs) [Constr iCon $ supTys ++ methTys]
ex = EVar (mkIdent "x")
tForall = EForall vs
tDict = tApps (qualIdent mn iDict) (map (EVar . idKindIdent) vs)
pat k n = foldl EApp (EVar iCon) [ if k == i then ex else EVar dummyIdent | i <- [1..n] ]
- mkSel (BSign i t) k = [ Sign i $ tForall $ tArrow tDict t, Fcn i [Eqn [pat k nMeths] $ EAlts [([], ex)] []] ]
+ mkSel (BSign i t) k = [ Sign mid $ tForall $ tDict `tArrow` t, selFcn mid k ]
+ where mid = mkMethodId iCls i
mkSel _ _ = impossible
- dSels = concat $ zipWith mkSel meths [1..]
+ dSels = concat $ zipWith mkSel meths [nSups+1 ..]
+ selFcn i k = Fcn i [Eqn [pat k nArgs] $ EAlts [([], ex)] []]
+ mkSupSel tsup k = [Sign sid $ tForall $ tDict `tArrow` tsup, selFcn sid k]
+ where sid = mkMethodId iCls (mkIdent ("Super" ++ showInt k))+ dSupers = concat $ zipWith mkSupSel supTys [1 ..]
+
tCtx = tApps (qualIdent mn iCls) (map (EVar . idKindIdent) vs)
mkDflt (BSign i t) = [ Sign iDflt $ tForall $ tCtx `tImplies` t, def $ lookupBy eqIdent i mdflts ]
where def Nothing = Fcn iDflt [Eqn [] $ EAlts [([], noDflt)] []]
def (Just eqns) = Fcn iDflt eqns
- iDflt = addIdentSuffix i "dflt" {-"$dflt"-}+ iDflt = mkDefaultMethodId iCls i
-- XXX This isn't right, "Prelude._nodefault" might not be in scope
noDflt = EApp (EVar (mkIdent "Prelude._noDefault")) (ELit noSLoc (LStr (unIdent iCls ++ "." ++ unIdent i)))
mkDflt _ = impossible
@@ -816,11 +826,42 @@
dDflts = concatMap mkDflt meths
-- XXX add iDict to symbol table
- T.return $ [dData] ++ dSels ++ dDflts
+ T.return $ [dData] ++ dSupers ++ dSels ++ dDflts
-expandInst :: [IdKind] -> Maybe EConstraint -> [EBind] -> T [EDef]
-expandInst _ _ _ = T.return [] -- XXX
+-- Turn a (unqualified) class name into the dictionary type name.
+mkDictId :: Ident -> Ident
+mkDictId cls = addIdentSuffix cls "$Dict"
+-- Turn (unqualified) class and method names into a selector name.
+mkMethodId :: Ident -> Ident -> Ident
+mkMethodId cls meth = addIdentSuffix cls ("$" ++ unIdent meth)+
+-- Turn (unqualified) class and method names into a default method name
+mkDefaultMethodId :: Ident -> Ident -> Ident
+mkDefaultMethodId cls meth = addIdentSuffix cls ("$" ++ unIdent meth ++ "$dflt")+
+clsToDict :: EType -> T EType
+clsToDict = T.do
+ -- XXX for now, only allow contexts of the form (C t1 ... tn)
+ let usup as (EVar c) | isConIdent c = T.return (tApps (mkDictId c) as)
+ usup as (EApp f a) = usup (a:as) f
+ usup _ t = tcError (getSLocExpr t) ("bad context " ++ showEType t)+ usup []
+
+expandInst :: [IdKind] -> [EConstraint] -> EType -> [EBind] -> T [EDef]
+expandInst vks _ctx cc bs = T.do
+ ct <- clsToDict cc
+ let iCon = getAppCon ct
+ iInst = mkIdent "inst$"
+ sign = Sign iInst (eForall vks ct)
+ bind = Fcn iInst [Eqn [] $ EAlts [([], foldl EApp (EVar iCon) meths)] bs]
+ meths = []
+ T.return [sign, bind]
+
+eForall :: [IdKind] -> EType -> EType
+eForall [] t = t
+eForall vs t = EForall vs t
+
---------------------
tcDefsValue :: [EDef] -> T [EDef]
@@ -872,8 +913,11 @@
T.return (ForImp ie (qualIdent mn i) t)
_ -> T.return adef
-tcInferTypeT :: EType -> T EType
-tcInferTypeT t = fst <$> tInfer tcTypeT t
+tCheckTypeT :: EType -> EType -> T EType
+tCheckTypeT = tCheck tcTypeT
+
+tInferTypeT :: EType -> T EType
+tInferTypeT t = fst <$> tInfer tcTypeT t
-- Kind check a type while already in type checking mode
tcTypeT :: --XHasCallStack =>
--
⑨