ref: 1887ae044bf79d2f7f9855647d5c81aeb5eaa736
parent: 4d1231db9de52ca40c77d165ec30d1cc234165a2
author: Lennart Augustsson <lennart.augustsson@epicgames.com>
date: Thu Oct 19 17:11:17 EDT 2023
Handle tupled constraints.
--- a/comb/mhs.comb
+++ b/comb/mhs.comb
@@ -1,3 +1,3 @@
v4.0
-1084
-((A :0 _907) ((A :1 ((B _953) _0)) ((A :2 (((S' _953) _0) I)) ((A :3 _877) ((A :4 (_3 "undefined")) ((A :5 I) ((A :6 (((C' B) _906) ((C _76) _5))) ((A :7 (((C' _6) (_924 _72)) ((_76 _922) _71))) ((A :8 ((B ((S _953) _922)) _3)) ((A :9 T) ((A :10 (T I)) ((A :11 ((B (_76 _191)) _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 _835)))) ((A :19 ((B (_74 _9)) (BK (P _835)))) ((A :20 ((_74 _9) ((S P) I))) ((A :21 ((B (_74 _9)) ((C (S' P)) I))) ((A :22 ((B Y) ((B (B (P (_14 _116)))) (((C' B) ((B (C' B)) (B _12))) (((C' (C' B)) (B _12)) ((B (B _14)) _117)))))) ((A :23 ((B Y) ((B (B (P (_14 _835)))) ((B (C' B)) (B _13))))) ((A :24 _3) ((A :25 (T (_14 _835))) ((A :26 (_22 _77)) ((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 _882) ((A :36 _883) ((A :37 (((S' _28) (_874 #97)) ((C _874) #122))) ((A :38 (((S' _28) (_874 #65)) ((C _874) #90))) ((A :39 (((S' _27) _37) _38)) ((A :40 (((S' _28) (_874 #48)) ((C _874) #57))) ((A :41 (((S' _28) (_874 #32)) ((C _874) #126))) ((A :42 _871) ((A :43 _872) ((A :44 _874) ((A :45 _873) ((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 (((_833 "lib/Data/Char.hs") #3) #8)))) ((B _35) (((C' _83) (((C' _84) _36) (_36 #65))) (_36 #97))))) ((A :48 ((S ((S (((S' _28) (_44 #97)) ((C _44) #97))) (_34 (((_833 "lib/Data/Char.hs") #3) #8)))) ((B _35) (((C' _83) (((C' _84) _36) (_36 #97))) (_36 #65))))) ((A :49 _842) ((A :50 _843) ((A :51 _844) ((A :52 _845) ((A :53 (_50 %0.0)) ((A :54 _49) ((A :55 _50) ((A :56 _51) ((A :57 _52) ((A :58 _846) ((A :59 _847) ((A :60 _58) ((A :61 _59) ((A :62 _848) ((A :63 _849) ((A :64 _850) ((A :65 _851) ((A :66 _62) ((A :67 _63) ((A :68 _64) ((A :69 _65) ((A :70 _852) ((A :71 ((B BK) T)) ((A :72 (BK T)) ((A :73 P) ((A :74 I) ((A :75 (S _879)) ((A :76 B) ((A :77 I) ((A :78 K) ((A :79 C) ((A :80 _878) ((A :81 ((C ((C S') _191)) _192)) ((A :82 (((C' (S' (C' B))) B) I)) ((A :83 _836) ((A :84 _837) ((A :85 _838) ((A :86 _839) ((A :87 _840) ((A :88 _841) ((A :89 (_84 #0)) ((A :90 _859) ((A :91 _860) ((A :92 _861) ((A :93 _862) ((A :94 _863) ((A :95 _864) ((A :96 _90) ((A :97 (BK K)) ((A :98 ((B BK) ((B (B BK)) P))) ((A :99 ((B (B (B BK))) ((B (B (B BK))) ((B (B (B C))) ((B (B C)) P))))) ((A :100 (((S' S) (((S' (S' C)) (((C' (C' S)) (((C' B) ((B (S' S')) (((C' B) ((B _27) (_93 #0))) (_90 #0)))) ((B (B ((C' P) (_88 #1)))) _83))) (C P))) _86)) _87)) ((A :101 _97) ((A :102 (((S' C) ((B (P _179)) (((C' (C' B)) (((C' C) _90) _179)) _180))) ((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') (_90 #0))))) ((B ((C' (C' C)) ((B (B ((S' S') (_90 #1)))) ((B ((C' C) ((B ((C' S') (_90 #2))) (C _102)))) (C _102))))) (C _102))))) (C _102)))) (T K))) (T A)))) ((C _100) #4)))) ((A :103 (_109 _78)) ((A :104 ((_124 (_81 _103)) _101)) ((A :105 ((C (((C' B) ((P _116) (((C' (C' O)) P) K))) (((S' (C' (C' (C' B)))) ((B (B (B (B _106)))) (((S' (C' (C' B))) ((B (B (B _106))) (((S' (C' B)) ((B (B _106)) (((C' B) ((B _122) (T #0))) _105))) (((C' B) ((B _122) (T #1))) _105)))) (((C' B) ((B _122) (T #2))) _105)))) (((C' B) ((B _122) (T #3))) _105)))) ((B T) ((B (B P)) ((C' _83) (_85 #4)))))) ((A :106 ((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) _92)))) ((B ((C' B) _117)) _106)))))) ((B ((C' B) _117)) (C _106)))))))))) (((_833 "lib/Data/IntMap.hs") #3) #8))))))))) ((A :107 ((_76 (_122 _191)) _105)) ((A :108 (((C' C) (((C' C) (C _102)) (_3 "Data.IntMap.!"))) I)) ((A :109 ((B (C' Y)) (((C' (C' (S' (S' C)))
\ No newline at end of file
+1085
+((A :0 _908) ((A :1 ((B _954) _0)) ((A :2 (((S' _954) _0) I)) ((A :3 _878) ((A :4 (_3 "undefined")) ((A :5 I) ((A :6 (((C' B) _907) ((C _76) _5))) ((A :7 (((C' _6) (_925 _72)) ((_76 _923) _71))) ((A :8 ((B ((S _954) _923)) _3)) ((A :9 T) ((A :10 (T I)) ((A :11 ((B (_76 _191)) _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 _836)))) ((A :19 ((B (_74 _9)) (BK (P _836)))) ((A :20 ((_74 _9) ((S P) I))) ((A :21 ((B (_74 _9)) ((C (S' P)) I))) ((A :22 ((B Y) ((B (B (P (_14 _116)))) (((C' B) ((B (C' B)) (B _12))) (((C' (C' B)) (B _12)) ((B (B _14)) _117)))))) ((A :23 ((B Y) ((B (B (P (_14 _836)))) ((B (C' B)) (B _13))))) ((A :24 _3) ((A :25 (T (_14 _836))) ((A :26 (_22 _77)) ((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 _883) ((A :36 _884) ((A :37 (((S' _28) (_875 #97)) ((C _875) #122))) ((A :38 (((S' _28) (_875 #65)) ((C _875) #90))) ((A :39 (((S' _27) _37) _38)) ((A :40 (((S' _28) (_875 #48)) ((C _875) #57))) ((A :41 (((S' _28) (_875 #32)) ((C _875) #126))) ((A :42 _872) ((A :43 _873) ((A :44 _875) ((A :45 _874) ((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 (((_834 "lib/Data/Char.hs") #3) #8)))) ((B _35) (((C' _83) (((C' _84) _36) (_36 #65))) (_36 #97))))) ((A :48 ((S ((S (((S' _28) (_44 #97)) ((C _44) #97))) (_34 (((_834 "lib/Data/Char.hs") #3) #8)))) ((B _35) (((C' _83) (((C' _84) _36) (_36 #97))) (_36 #65))))) ((A :49 _843) ((A :50 _844) ((A :51 _845) ((A :52 _846) ((A :53 (_50 %0.0)) ((A :54 _49) ((A :55 _50) ((A :56 _51) ((A :57 _52) ((A :58 _847) ((A :59 _848) ((A :60 _58) ((A :61 _59) ((A :62 _849) ((A :63 _850) ((A :64 _851) ((A :65 _852) ((A :66 _62) ((A :67 _63) ((A :68 _64) ((A :69 _65) ((A :70 _853) ((A :71 ((B BK) T)) ((A :72 (BK T)) ((A :73 P) ((A :74 I) ((A :75 (S _880)) ((A :76 B) ((A :77 I) ((A :78 K) ((A :79 C) ((A :80 _879) ((A :81 ((C ((C S') _191)) _192)) ((A :82 (((C' (S' (C' B))) B) I)) ((A :83 _837) ((A :84 _838) ((A :85 _839) ((A :86 _840) ((A :87 _841) ((A :88 _842) ((A :89 (_84 #0)) ((A :90 _860) ((A :91 _861) ((A :92 _862) ((A :93 _863) ((A :94 _864) ((A :95 _865) ((A :96 _90) ((A :97 (BK K)) ((A :98 ((B BK) ((B (B BK)) P))) ((A :99 ((B (B (B BK))) ((B (B (B BK))) ((B (B (B C))) ((B (B C)) P))))) ((A :100 (((S' S) (((S' (S' C)) (((C' (C' S)) (((C' B) ((B (S' S')) (((C' B) ((B _27) (_93 #0))) (_90 #0)))) ((B (B ((C' P) (_88 #1)))) _83))) (C P))) _86)) _87)) ((A :101 _97) ((A :102 (((S' C) ((B (P _179)) (((C' (C' B)) (((C' C) _90) _179)) _180))) ((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') (_90 #0))))) ((B ((C' (C' C)) ((B (B ((S' S') (_90 #1)))) ((B ((C' C) ((B ((C' S') (_90 #2))) (C _102)))) (C _102))))) (C _102))))) (C _102)))) (T K))) (T A)))) ((C _100) #4)))) ((A :103 (_109 _78)) ((A :104 ((_124 (_81 _103)) _101)) ((A :105 ((C (((C' B) ((P _116) (((C' (C' O)) P) K))) (((S' (C' (C' (C' B)))) ((B (B (B (B _106)))) (((S' (C' (C' B))) ((B (B (B _106))) (((S' (C' B)) ((B (B _106)) (((C' B) ((B _122) (T #0))) _105))) (((C' B) ((B _122) (T #1))) _105)))) (((C' B) ((B _122) (T #2))) _105)))) (((C' B) ((B _122) (T #3))) _105)))) ((B T) ((B (B P)) ((C' _83) (_85 #4)))))) ((A :106 ((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) _92)))) ((B ((C' B) _117)) _106)))))) ((B ((C' B) _117)) (C _106)))))))))) (((_834 "lib/Data/IntMap.hs") #3) #8))))))))) ((A :107 ((_76 (_122 _191)) _105)) ((A :108 (((C' C) (((C' C) (C _102)) (_3 "Data.IntMap.!"))) I)) ((A :109 ((B (C' Y)) (((C' (C' (S' (S' C)))
\ No newline at end of file
--- a/src/MicroHs/Expr.hs
+++ b/src/MicroHs/Expr.hs
@@ -412,8 +412,10 @@
ppIdKind (IdKind i k) = parens $ ppIdent i <> text "::" <> ppEKind k
ppEDefs :: [EDef] -> Doc
-ppEDefs ds = vcat (map (nl . ppEDef) ds)
- where nl d = d $+$ text ""
+ppEDefs ds = vcat (map pp ds)
+ where pp d@(Sign _ _) = ppEDef d
+ pp d@(Import _) = ppEDef d
+ pp d = ppEDef d $+$ text ""
ppAlts :: Doc -> EAlts -> Doc
ppAlts asep (EAlts alts bs) = ppWhere (ppAltsL asep alts) bs
--- a/src/MicroHs/TypeCheck.hs
+++ b/src/MicroHs/TypeCheck.hs
@@ -450,11 +450,14 @@
primTypes =
let
entry i = Entry (EVar (mkIdentB i))
+ k = mkIdent "k"
+ kv = EVar k
+ kk = IdKind k kTypeS
tuple n =
let
i = tupleConstr builtinLoc n
- in (i, [entry (unIdent i) $ foldr kArrow kType (replicate n kType)])
- in
+ in (i, [entry (unIdent i) $ EForall [kk] $ foldr kArrow kv (replicate n kv)])
+ in
[
-- The function arrow et al are bothersome to define in Primitives, so keep them here.
-- But the fixity is defined in Primitives.
@@ -931,10 +934,25 @@
-- Ord$super1 :: forall a . Ord a -> Eq a
-- <= :: forall a . Ord a -> (a -> a -> Bool)
-- <=$dflt = _noDefault "Ord.<="
+--
+-- instance Eq Int where (==) = primEqInt
+-- expands to
+-- inst$999 = Eq$ meth$1 meth$2
+-- where meth$1 = primEqInt
+-- meth$2 = /=$dflt dict$999
+--
+-- instance Ord Int where (<=) = primLEInt
+-- expands to
+-- inst$888 = Ord$ dict$ meth$1
+-- where meth$1 = primLEInt
+-- where dict$ is a special magic identifier that the type checker expands
+-- to whatever dictionary is forced by the type.
+-- In this case (dict$ :: Eq Int), so it with be inst$999
+--
-- The actual definitions for the constructor and methods are added
-- in the desugaring pass.
-- Default methods are added as actual definitions.
--- The constructor and mathods are added to the symbol table in addValueType.
+-- The constructor and methods are added to the symbol table in addValueType.
expandClass :: EDef -> T [EDef]
expandClass dcls@(Class ctx (iCls, vks) ms) = T.do
mn <- gets moduleName
@@ -954,46 +972,7 @@
addClassTable (qualIdent mn iCls) (vks, ctx, methIds)
T.return $ dcls : dDflts
expandClass d = T.return [d]
-{-- mn <- gets moduleName
- supTys <- T.return sups -- T.mapM clsToDict sups
- let iDict = 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
- nSups = length sups
- nArgs = nSups + nMeths
- iCon = iDict -- dictionary constructor name
- dData = Data (iDict, vs) [Constr iCon $ Left $ 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 mid $ tForall $ tDict `tArrow` t, selFcn mid k ]
- where mid = i
- mkSel _ _ = impossible
- 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 = mkIdent (unIdent iCls ++ "$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 = mkDefaultMethodId 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
- dDflts = concatMap mkDflt meths
-
- -- XXX add iDict to symbol table
- T.return $ [dData] ++ dSupers ++ dSels ++ dDflts
--}
-- Turn (unqualified) class and method names into a default method name
mkDefaultMethodId :: Ident -> Ident
mkDefaultMethodId meth = addIdentSuffix meth "$dflt"
@@ -1008,12 +987,6 @@
usup []
-}
--- Implement:
--- * Look up class to get number of super-classes and methods
--- Generate Cls$C dict$ dict$ ... method1 ... methodN
--- Where methodK is either from bs of the default method.
--- There's one magic dict$ for each superclass.
--- * Add instance to instance table
expandInst :: EDef -> T [EDef]
expandInst dinst@(Instance vks ctx cc bs) = T.do
let loc = getSLocExpr cc
@@ -1865,19 +1838,30 @@
if null cs then
T.return []
else T.do
- traceM "solveConstraints"
+-- traceM "solveConstraints"
cs' <- T.mapM (\ (i,t) -> T.do { t' <- derefUVar t; T.return (i,t') }) cs- traceM ("constraints:\n" ++ unlines (map (\ (i, t) -> showIdent i ++ " :: " ++ showExpr t) cs'))+-- traceM ("constraints:\n" ++ unlines (map (\ (i, t) -> showIdent i ++ " :: " ++ showExpr t) cs'))is <- gets instances
- traceM ("instances:\n" ++ unlines (map (\ (i, _, _, t) -> showExpr i ++ " :: " ++ showExpr t) is))- let xs = map solve cs'
- solve c@(d, t) =
- case [ e | (e, [], [], t') <- is, eqEType t t' ] of
- [e] -> Right (d, e)
- _ -> Left c
- putConstraints [ c | Left c <- xs ]
- traceM ("solved:\n" ++ unlines [ showIdent i ++ " = " ++ showExpr e | Right (i, e) <- xs ])- T.return [ ie | Right ie <- xs ]
+-- traceM ("instances:\n" ++ unlines (map (\ (i, _, _, t) -> showExpr i ++ " :: " ++ showExpr t) is))+ let solve :: [(Ident, EType)] -> [(Ident, EType)] -> [(Ident, Expr)] -> T ([(Ident, EType)], [(Ident, Expr)])
+ solve [] uns sol = T.return (uns, sol)
+ solve (cns@(di, ct) : cnss) uns sol = T.do
+ let loc = getSLocIdent di
+ (iCls, cts) = getApp ct
+ case getTupleConstr iCls of
+ Just _ -> T.do
+ goals <- T.mapM (\ c -> T.do { d <- newIdent loc "dict"; T.return (d, c) }) cts+ solve (goals ++ cnss) uns ((di, ETuple (map (EVar . fst) goals)) : sol)
+ Nothing ->
+ case [ de | (de, [], [], t) <- is, eqEType ct t ] of
+ [] -> solve cnss (cns : uns) sol
+ [de] -> solve cnss uns ((di, de) : sol)
+ _ -> tcError loc $ "Multiple constraint solutions for: " ++ showEType ct
+ (unsolved, solved) <- solve cs' [] []
+ putConstraints unsolved
+-- traceM ("solved:\n" ++ unlines [ showIdent i ++ " = " ++ showExpr e | (i, e) <- solved ])+-- traceM ("unsolved:\n" ++ unlines [ showIdent i ++ " :: " ++ showEType t | (i, t) <- unsolved ])+ T.return solved
checkConstraints :: T ()
checkConstraints = T.do
--
⑨