ref: 30be00d866cac749277b60b67013771c3d737d84
parent: fb418b077823bb00a7ad98af674dae5a83951e66
author: Lennart Augustsson <lennart.augustsson@epicgames.com>
date: Fri Oct 20 14:17:14 EDT 2023
Handle instances with a context.
--- a/comb/mhs.comb
+++ b/comb/mhs.comb
@@ -1,3 +1,3 @@
v4.0
-1089
-((A :0 _912) ((A :1 ((B _958) _0)) ((A :2 (((S' _958) _0) I)) ((A :3 _882) ((A :4 (_3 "undefined")) ((A :5 I) ((A :6 (((C' B) _911) ((C _76) _5))) ((A :7 (((C' _6) (_929 _72)) ((_76 _927) _71))) ((A :8 ((B ((S _958) _927)) _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 _840)))) ((A :19 ((B (_74 _9)) (BK (P _840)))) ((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 _840)))) ((B (C' B)) (B _13))))) ((A :24 _3) ((A :25 (T (_14 _840))) ((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 _887) ((A :36 _888) ((A :37 (((S' _28) (_879 #97)) ((C _879) #122))) ((A :38 (((S' _28) (_879 #65)) ((C _879) #90))) ((A :39 (((S' _27) _37) _38)) ((A :40 (((S' _28) (_879 #48)) ((C _879) #57))) ((A :41 (((S' _28) (_879 #32)) ((C _879) #126))) ((A :42 _876) ((A :43 _877) ((A :44 _879) ((A :45 _878) ((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 (((_838 "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 (((_838 "lib/Data/Char.hs") #3) #8)))) ((B _35) (((C' _83) (((C' _84) _36) (_36 #97))) (_36 #65))))) ((A :49 _847) ((A :50 _848) ((A :51 _849) ((A :52 _850) ((A :53 (_50 %0.0)) ((A :54 _49) ((A :55 _50) ((A :56 _51) ((A :57 _52) ((A :58 _851) ((A :59 _852) ((A :60 _58) ((A :61 _59) ((A :62 _853) ((A :63 _854) ((A :64 _855) ((A :65 _856) ((A :66 _62) ((A :67 _63) ((A :68 _64) ((A :69 _65) ((A :70 _857) ((A :71 ((B BK) T)) ((A :72 (BK T)) ((A :73 P) ((A :74 I) ((A :75 (S _884)) ((A :76 B) ((A :77 I) ((A :78 K) ((A :79 C) ((A :80 _883) ((A :81 ((C ((C S') _191)) _192)) ((A :82 (((C' (S' (C' B))) B) I)) ((A :83 _841) ((A :84 _842) ((A :85 _843) ((A :86 _844) ((A :87 _845) ((A :88 _846) ((A :89 (_84 #0)) ((A :90 _864) ((A :91 _865) ((A :92 _866) ((A :93 _867) ((A :94 _868) ((A :95 _869) ((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)))))))))) (((_838 "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
+1092
+((A :0 _915) ((A :1 ((B _961) _0)) ((A :2 (((S' _961) _0) I)) ((A :3 _885) ((A :4 (_3 "undefined")) ((A :5 I) ((A :6 (((C' B) _914) ((C _76) _5))) ((A :7 (((C' _6) (_932 _72)) ((_76 _930) _71))) ((A :8 ((B ((S _961) _930)) _3)) ((A :9 T) ((A :10 (T I)) ((A :11 ((B (_76 _192)) _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 _843)))) ((A :19 ((B (_74 _9)) (BK (P _843)))) ((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 _843)))) ((B (C' B)) (B _13))))) ((A :24 _3) ((A :25 (T (_14 _843))) ((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 _890) ((A :36 _891) ((A :37 (((S' _28) (_882 #97)) ((C _882) #122))) ((A :38 (((S' _28) (_882 #65)) ((C _882) #90))) ((A :39 (((S' _27) _37) _38)) ((A :40 (((S' _28) (_882 #48)) ((C _882) #57))) ((A :41 (((S' _28) (_882 #32)) ((C _882) #126))) ((A :42 _879) ((A :43 _880) ((A :44 _882) ((A :45 _881) ((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 (((_841 "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 (((_841 "lib/Data/Char.hs") #3) #8)))) ((B _35) (((C' _83) (((C' _84) _36) (_36 #97))) (_36 #65))))) ((A :49 _850) ((A :50 _851) ((A :51 _852) ((A :52 _853) ((A :53 (_50 %0.0)) ((A :54 _49) ((A :55 _50) ((A :56 _51) ((A :57 _52) ((A :58 _854) ((A :59 _855) ((A :60 _58) ((A :61 _59) ((A :62 _856) ((A :63 _857) ((A :64 _858) ((A :65 _859) ((A :66 _62) ((A :67 _63) ((A :68 _64) ((A :69 _65) ((A :70 _860) ((A :71 ((B BK) T)) ((A :72 (BK T)) ((A :73 P) ((A :74 I) ((A :75 (S _887)) ((A :76 B) ((A :77 I) ((A :78 K) ((A :79 C) ((A :80 _886) ((A :81 ((C ((C S') _192)) _193)) ((A :82 (((C' (S' (C' B))) B) I)) ((A :83 _844) ((A :84 _845) ((A :85 _846) ((A :86 _847) ((A :87 _848) ((A :88 _849) ((A :89 (_84 #0)) ((A :90 _867) ((A :91 _868) ((A :92 _869) ((A :93 _870) ((A :94 _871) ((A :95 _872) ((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 _180)) (((C' (C' B)) (((C' C) _90) _180)) _181))) ((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)))))))))) (((_841 "lib/Data/IntMap.hs") #3) #8))))))))) ((A :107 ((_76 (_122 _192)) _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/lib/Data/List.hs
+++ b/lib/Data/List.hs
@@ -64,6 +64,10 @@
foldl1 _ [] = error "foldl1"
foldl1 f (x : xs) = foldl f x xs
+minimum :: [P.Int] -> P.Int
+minimum [] = error "minimum"
+minimum (x:ys) = foldr (\ y m -> if y < m then y else m) x ys
+
sum :: [P.Int] -> P.Int
sum = foldr (+) 0
@@ -262,6 +266,7 @@
deleteFirstsBy :: forall a . (a -> a -> Bool) -> [a] -> [a] -> [a]
deleteFirstsBy eq = foldl (flip (deleteBy eq))
+-- Delete all from the second argument from the first argument
deleteAllsBy :: forall a . (a -> a -> Bool) -> [a] -> [a] -> [a]
deleteAllsBy eq = foldl (flip (deleteAllBy eq))
--- a/src/MicroHs/Expr.hs
+++ b/src/MicroHs/Expr.hs
@@ -246,6 +246,7 @@
-- Enough to handle subsitution in types
subst :: [(Ident, Expr)] -> Expr -> Expr
+subst [] = id
subst s =
let
sub ae =
@@ -254,6 +255,8 @@
EApp f a -> EApp (sub f) (sub a)
ESign e t -> ESign (sub e) t
EUVar _ -> ae
+ EForall iks t -> EForall iks $ subst [ x | x@(i, _) <- s, not (elemBy eqIdent i is) ] t
+ where is = map idKindIdent iks
_ -> error "subst unimplemented"
in sub
--- a/src/MicroHs/TypeCheck.hs
+++ b/src/MicroHs/TypeCheck.hs
@@ -1010,11 +1010,12 @@
addConstraints :: [EConstraint] -> EType -> EType
addConstraints [] t = t
-addConstraints [c] t = c `tImplies` t
addConstraints cs t = tupleConstraints cs `tImplies` t
tupleConstraints :: [EConstraint] -> EConstraint
-tupleConstraints cs = tApps (tupleConstr noSLoc (length cs)) cs
+tupleConstraints [] = error "tupleConstraints"
+tupleConstraints [c] = c
+tupleConstraints cs = tApps (tupleConstr noSLoc (length cs)) cs
expandInst :: EDef -> T [EDef]
expandInst dinst@(Instance vks ctx cc bs) = T.do
@@ -1868,6 +1869,17 @@
mkSuperSel :: IdentModule -> Ident -> Int -> Ident
mkSuperSel mn c i = qualIdent mn $ mkIdent $ unIdent c ++ "$super" ++ showInt i
+{-+showInstDict :: InstDict -> String
+showInstDict (e, iks, ctx, ct) = showExpr e ++ " :: " ++ showEType (eForall iks $ addConstraints ctx ct)
+
+showConstraint :: (Ident, EConstraint) -> String
+showConstraint (i, t) = showIdent i ++ " :: " ++ showEType t
+
+showMatch :: (Expr, [EConstraint]) -> String
+showMatch (e, ts) = showExpr e ++ " " ++ showList showEType ts
+-}
+
-- Solve as many constraints as possible.
-- Return bindings for the dictionary witnesses.
-- Unimplemented:
@@ -1878,15 +1890,16 @@
if null cs then
T.return []
else T.do
--- traceM "solveConstraints"
+-- traceM "------------------------------------------\nsolveConstraints"
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 showConstraint cs'))it <- gets instTable
let instsOf c = fromMaybe [] $ M.lookup c it
--- traceM ("instances:\n" ++ unlines (map (\ (i, _, _, t) -> showExpr i ++ " :: " ++ showExpr t) (concat $ M.elems it)))+-- traceM ("instances:\n" ++ unlines (map showInstDict (concat $ M.elems it)))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
+-- traceM ("trying " ++ showEType ct)let loc = getSLocIdent di
(iCls, cts) = getApp ct
case getTupleConstr iCls of
@@ -1893,16 +1906,73 @@
Just _ -> T.do
goals <- T.mapM (\ c -> T.do { d <- newIdent loc "dict"; T.return (d, c) }) ctssolve (goals ++ cnss) uns ((di, ETuple (map (EVar . fst) goals)) : sol)
- Nothing ->
- case [ de | (de, [], [], t) <- instsOf iCls, eqEType ct t ] of
- [] -> solve cnss (cns : uns) sol
- [de] -> solve cnss uns ((di, de) : sol)
- _ -> tcError loc $ "Multiple constraint solutions for: " ++ showEType ct
+ Nothing -> T.do
+ let matches = getBestMatches $ findMatches (instsOf iCls) ct
+-- traceM ("matches " ++ showList showMatch matches)+ case matches of
+ [] -> solve cnss (cns : uns) sol
+ [(de, ctx)] ->
+ if null ctx then
+ solve cnss uns ((di, de) : sol)
+ else T.do
+ d <- newIdent (getSLocIdent iCls) "dict"
+-- traceM ("constraint " ++ showIdent di ++ " :: " ++ showEType ct ++ "\n" +++-- " turns into " ++ showIdent d ++ " :: " ++ showEType (tupleConstraints ctx) ++ ", " ++
+-- showIdent di ++ " = " ++ showExpr (EApp de (EVar d)))
+ solve ((d, tupleConstraints ctx) : cnss) uns ((di, EApp de (EVar d)) : 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
+
+-- Given some instances and a constraint, find the matching instances.
+-- For each matching instance return: (subst-size, (dict-expression, new-constraints))
+-- The subst-size is the size of the substitution that made the input instance match.
+-- It is a measure of how exact the match is.
+findMatches :: [InstDict] -> EConstraint -> [(Int, (Expr, [EConstraint]))]
+findMatches ds ct =
+ let rrr =
+ [ (length s, (de, map (substEUVar s . subst r) ctx))
+ | (de, iks, ctx, t) <- ds, let { r = freshSubst iks }, Just s <- [matchType [] (subst r t) ct] ]+ in --trace ("findMatches: " ++ showList showInstDict ds ++ "; " ++ showEType ct ++ "; " ++ show rrr)+ rrr
+ where
+ -- Change type variable to unique unification variables.
+ -- These unification variables will never leak out of findMatches.
+ freshSubst iks = zipWith (\ ik j -> (idKindIdent ik, EUVar j)) iks [1000000000 ..] -- make sure the variables are unique
+
+ -- Match two types, instantiate variables in the first type.
+ matchType r (EVar i) (EVar i') | eqIdent i i' = Just r
+ matchType r (EApp f a) (EApp f' a') = -- XXX should use Maybe monad
+ case matchType r f f' of
+ Nothing -> Nothing
+ Just r' -> matchType r' a a'
+ matchType r (EUVar i) t =
+ -- For a variable, check that any previous match is the same.
+ case lookupBy eqInt i r of
+ Just t' -> if eqEType t t' then Just r else Nothing
+ Nothing -> Just ((i, t) : r)
+ matchType _ _ _ = Nothing
+
+ -- Do substitution for EUVar.
+ -- XXX similat to derefUVar
+ substEUVar [] t = t
+ substEUVar _ t@(EVar _) = t
+ substEUVar s (EApp f a) = EApp (substEUVar s f) (substEUVar s a)
+ substEUVar s t@(EUVar i) = fromMaybe t $ lookupBy (eqInt) i s
+ substEUVar s (EForall iks t) = EForall iks (substEUVar s t)
+ substEUVar _ _ = impossible
+
+
+-- Get the best matches. These are the matches with the smallest substitution.
+getBestMatches :: [(Int, (Expr, [EConstraint]))] -> [(Expr, [EConstraint])]
+getBestMatches [] = []
+getBestMatches ms =
+ let b = minimum (map fst ms) -- minimum substitution size
+ in [ ec | (s, ec) <- ms, s == b ] -- pick out the smallest
-- Check that there are no unsolved constraints.
checkConstraints :: T ()
--
⑨