shithub: MicroHs

--- a/comb/mhs.comb

+++ b/comb/mhs.comb

@@ -1,3 +1,3 @@

 v4.0

-999

-((A :0 _883) ((A :1 ((B _929) _0)) ((A :2 (((S' _929) _0) I)) ((A :3 _853) ((A :4 (_3 "undefined")) ((A :5 I) ((A :6 (((C' B) _882) ((C _75) _5))) ((A :7 (((C' _6) (_900 _72)) ((_75 _898) _71))) ((A :8 ((B ((S _929) _898)) _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 _811)))) ((A :19 ((B (_74 _9)) (BK (P _811)))) ((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 _811)))) ((B (C' B)) (B _13))))) ((A :24 _3) ((A :25 (T (_14 _811))) ((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 _858) ((A :36 _859) ((A :37 (((S' _28) (_850 #97)) ((C _850) #122))) ((A :38 (((S' _28) (_850 #65)) ((C _850) #90))) ((A :39 (((S' _27) _37) _38)) ((A :40 (((S' _28) (_850 #48)) ((C _850) #57))) ((A :41 (((S' _28) (_850 #32)) ((C _850) #126))) ((A :42 _847) ((A :43 _848) ((A :44 _850) ((A :45 _849) ((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 (((_809 "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 (((_809 "lib/Data/Char.hs") #3) #8)))) ((B _35) (((C' _82) (((C' _83) _36) (_36 #97))) (_36 #65))))) ((A :49 _818) ((A :50 _819) ((A :51 _820) ((A :52 _821) ((A :53 (_50 %0.0)) ((A :54 _49) ((A :55 _50) ((A :56 _51) ((A :57 _52) ((A :58 _822) ((A :59 _823) ((A :60 _58) ((A :61 _59) ((A :62 _824) ((A :63 _825) ((A :64 _826) ((A :65 _827) ((A :66 _62) ((A :67 _63) ((A :68 _64) ((A :69 _65) ((A :70 _828) ((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 _854) ((A :80 ((C ((C S') _190)) _191)) ((A :81 (((C' (S' (C' B))) B) I)) ((A :82 _812) ((A :83 _813) ((A :84 _814) ((A :85 _815) ((A :86 _816) ((A :87 _817) ((A :88 (_83 #0)) ((A :89 _835) ((A :90 _836) ((A :91 _837) ((A :92 _838) ((A :93 _839) ((A :94 _840) ((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)))))))))) (((_809 "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

+1007

+((A :0 _891) ((A :1 ((B _937) _0)) ((A :2 (((S' _937) _0) I)) ((A :3 _861) ((A :4 (_3 "undefined")) ((A :5 I) ((A :6 (((C' B) _890) ((C _75) _5))) ((A :7 (((C' _6) (_908 _72)) ((_75 _906) _71))) ((A :8 ((B ((S _937) _906)) _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 _819)))) ((A :19 ((B (_74 _9)) (BK (P _819)))) ((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 _819)))) ((B (C' B)) (B _13))))) ((A :24 _3) ((A :25 (T (_14 _819))) ((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 _866) ((A :36 _867) ((A :37 (((S' _28) (_858 #97)) ((C _858) #122))) ((A :38 (((S' _28) (_858 #65)) ((C _858) #90))) ((A :39 (((S' _27) _37) _38)) ((A :40 (((S' _28) (_858 #48)) ((C _858) #57))) ((A :41 (((S' _28) (_858 #32)) ((C _858) #126))) ((A :42 _855) ((A :43 _856) ((A :44 _858) ((A :45 _857) ((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 (((_817 "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 (((_817 "lib/Data/Char.hs") #3) #8)))) ((B _35) (((C' _82) (((C' _83) _36) (_36 #97))) (_36 #65))))) ((A :49 _826) ((A :50 _827) ((A :51 _828) ((A :52 _829) ((A :53 (_50 %0.0)) ((A :54 _49) ((A :55 _50) ((A :56 _51) ((A :57 _52) ((A :58 _830) ((A :59 _831) ((A :60 _58) ((A :61 _59) ((A :62 _832) ((A :63 _833) ((A :64 _834) ((A :65 _835) ((A :66 _62) ((A :67 _63) ((A :68 _64) ((A :69 _65) ((A :70 _836) ((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 _862) ((A :80 ((C ((C S') _190)) _191)) ((A :81 (((C' (S' (C' B))) B) I)) ((A :82 _820) ((A :83 _821) ((A :84 _822) ((A :85 _823) ((A :86 _824) ((A :87 _825) ((A :88 (_83 #0)) ((A :89 _843) ((A :90 _844) ((A :91 _845) ((A :92 _846) ((A :93 _847) ((A :94 _848) ((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)))))))))) (((_817 "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

@@ -59,9 +59,11 @@

 type FixTable   = M.Map Fixity     -- precedence and associativity of operators

 type AssocTable = M.Map [Ident]    -- maps a type identifier to its associated construcors/selectors/methods

 type ClassTable = M.Map (Int, [Ident]) -- # super classes, instance names

-type Instances  = [([IdKind], [EConstraint], EConstraint)]

+type Instances  = [InstDict]

 type Constraints= [(Ident, EConstraint)]

+type InstDict   = (Ident, [IdKind], [EConstraint], EConstraint)

 type Sigma = EType

 --type Tau   = EType

 type Rho   = EType

@@ -301,6 +303,12 @@

 tcMode :: TCState -> TCMode

 tcMode (TC _ _ _ _ _ _ _ _ m _ _ _) = m

+instances :: TCState -> Instances

+instances (TC _ _ _ _ _ _ _ _ _ _ is _) = is

+constraints :: TCState -> Constraints

+constraints (TC _ _ _ _ _ _ _ _ _ _ _ e) = e

 putValueTable :: ValueTable -> T ()

 putValueTable venv = T.do

   TC mn n fx tenv senv _ ast sub m cs is es <- get

@@ -326,6 +334,11 @@

   TC mn n fx tenv senv venv ast sub _ cs is es <- get

   put (TC mn n fx tenv senv venv ast sub m cs is es)

+putInstances :: Instances -> T ()

+putInstances is = T.do

+  TC mn n fx tenv senv venv ast sub m cs _ es <- get

+  put (TC mn n fx tenv senv venv ast sub m cs is es)

 withTCMode :: forall a . TCMode -> T a -> T a

 withTCMode m ta = T.do

   om <- gets tcMode

@@ -354,11 +367,25 @@

   TC mn n fx tt st vt ast sub m cs is es <- get

   put $ TC mn n fx tt st vt ast sub m (M.insert i x cs) is es

-addInstance :: ([IdKind], [EConstraint], EConstraint) -> T ()

-addInstance inst = T.do

+addInstance :: InstDict -> T ()

+addInstance ic = T.do

+  is <- gets instances

+  putInstances (ic : is)

+addConstraint :: (Ident, EConstraint) -> T ()

+addConstraint e = T.do

+  traceM (show e)

   TC mn n fx tt st vt ast sub m cs is es <- get

-  put $ TC mn n fx tt st vt ast sub m cs (inst : is) es

+  put $ TC mn n fx tt st vt ast sub m cs is (e : es)

+withDict :: forall a . InstDict -> T a -> T a

+withDict ic ta = T.do

+  is <- gets instances

+  putInstances (ic : is)

+  a <- ta

+  putInstances is

+  T.return a

 -- XXX handle imports

 initTC :: IdentModule -> FixTable -> TypeTable -> SynTable -> ValueTable -> AssocTable -> TCState

 initTC mn fs ts ss vs as =

@@ -470,6 +497,11 @@

   if eqIdent n (mkIdent "->") || eqIdent n (mkIdent "Primitives.->") then Just (a, b) else Nothing

 getArrow _ = Nothing

+getImplies :: EType -> Maybe (EType, EType)

+getImplies (EApp (EApp (EVar n) a) b) =

+  if eqIdent n (mkIdent "=>") || eqIdent n (mkIdent "Primitives.=>") then Just (a, b) else Nothing

+getImplies _ = Nothing

{-

 getTuple :: Int -> EType -> Maybe [EType]

 getTuple n t = loop t []

@@ -535,7 +567,8 @@

     EForall iks t -> EForall iks <$> derefUVar t

     _ -> impossible

-tcErrorTK :: SLoc -> String -> T ()

+tcErrorTK :: --XHasCallStack =>

+             SLoc -> String -> T ()

 tcErrorTK loc msg = T.do

   tcm <- gets tcMode

   let s = case tcm of

@@ -622,7 +655,10 @@

   tLookup ("undefined " ++ s ++ " identifier") ("ambiguous " ++ s ++ " identifier") i

 tInst :: EType -> T EType

-tInst as =

+tInst t = tInst' t T.>>= tDict

+tInst' :: EType -> T EType

+tInst' as =

   case as of

     EForall vks t ->

       if null vks then T.return t

@@ -632,6 +668,14 @@

         T.return (subst (zip vs us) t)

     t -> T.return t

+tDict :: EType -> T EType

+tDict (EApp (EApp (EVar (Ident loc "Primitives.=>")) ctx) t) = T.do

+  u <- newUniq

+  let d = mkIdentSLoc loc ("dict$" ++ showInt u)

+  addConstraint (d, ctx)

+  tDict t

+tDict t = T.return t

 extValE :: --XHasCallStack =>

            Ident -> EType -> Expr -> T ()

 extValE i t e = T.do

@@ -974,7 +1018,7 @@

       sups = replicate nsup (EVar $ mkIdentSLoc loc "dict$")

       args = sups ++ meths

   let bind = Fcn iInst [Eqn [] $ EAlts [([], foldl EApp (EVar $ mkClassConstructor iCls) args)] bs']

-  addInstance (vks, ctx, cc)

+  addInstance (iInst, vks, ctx, cc)

   T.return [dinst, sign, bind]

 expandInst d = T.return [d]

@@ -1036,12 +1080,13 @@

 tcDefValue adef =

   case adef of

     Fcn i eqns -> T.do

---      traceM $ "tcDefValue: " ++ show i -- ++ " = " ++ showExpr rhs

       (_, tt) <- tLookup "no type signature" "many type signatures" i

       let (iks, tfn) = unForall tt

+      traceM $ "tcDefValue: " ++ show i ++ " :: " ++ showExpr tt

       mn <- gets moduleName

       teqns <- withExtTyps iks $ tcEqns tfn eqns

 --      traceM (showEDefs [Fcn i eqns, Fcn i teqns])

+      _ <- solveConstraints

       T.return $ Fcn (qualIdent mn i) teqns

     ForImp ie i t -> T.do

       mn <- gets moduleName

@@ -1095,7 +1140,12 @@

 tCheckExpr :: --XHasCallStack =>

               EType -> Expr -> T Expr

-tCheckExpr = tCheck tcExpr

+tCheckExpr t e | Just (ctx, t') <- getImplies t = T.do

+  u <- newUniq

+  let d = mkIdentSLoc (getSLocExpr e) ("adict$" ++ showInt u)

+  e' <- withDict (d, [], [], ctx) $ tCheckExpr t' e

+  T.return $ ELam [EVar d] e'

+tCheckExpr t e = tCheck tcExpr t e

 tGetRefType :: --XHasCallStack =>

                TRef -> T EType

@@ -1716,3 +1766,15 @@

 instSigma _   t1 (Infer r) = T.do

   t1' <- tInst t1

   tSetRefType r t1'

+-----

+solveConstraints :: T ()

+solveConstraints = T.do

+  cs <- gets constraints

+  if null cs then

+    T.return ()

+   else T.do

+    traceM "solveConstraints"

+    traceM (unlines $ map (\ (i, t) -> showIdent i ++ " :: " ++ showExpr t) cs)

+    T.return ()

--

⑨