[add SEQ2 rule to boxy matching. new specialization routine for E conversion
John Meacham <john@repetae.net>**20060214120954] hunk ./E/FromHs.hs 13
+import Char
hunk ./E/FromHs.hs 28
-import Support.CanType
-import Char
hunk ./E/FromHs.hs 34
-import E.LetFloat(atomizeApps)
hunk ./E/FromHs.hs 35
+import E.LetFloat(atomizeApps)
hunk ./E/FromHs.hs 41
-import Support.FreeVars
+import FrontEnd.Rename(unRename)
+import FrontEnd.SrcLoc
+import FrontEnd.Tc.Type(prettyPrintType)
+import FrontEnd.Utils
hunk ./E/FromHs.hs 50
-import Util.NameMonad
-import FrontEnd.SrcLoc
-import FrontEnd.Rename(unRename)
-import FrontEnd.Tc.Type(prettyPrintType)
+import Name.VConsts
hunk ./E/FromHs.hs 53
-import qualified Util.Seq as Seq
hunk ./E/FromHs.hs 54
+import qualified Util.Seq as Seq
hunk ./E/FromHs.hs 56
-import FrontEnd.Utils
-import Name.VConsts
+import Support.CanType
+import Support.FreeVars
+import Type(schemeToType)
+import Util.NameMonad
hunk ./E/FromHs.hs 128
+{-
hunk ./E/FromHs.hs 137
+-}
+
+
+fromTyvar (Tyvar _ n k _) = tVr (toId n) (kind k)
+
+fromSigma (TForAll vs (_ :=> t)) = (map fromTyvar vs, tipe t)
+fromSigma t = ([], tipe t)
+
+convertVal assumps n = (foldr ePi t vs, flip (foldr eLam) vs) where
+    (vs,t) = case Map.lookup n assumps of
+        Just z -> fromSigma $ schemeToType z
+        Nothing -> error $ "convertVal.Lookup failed: " ++ (show n)
hunk ./E/FromHs.hs 384
-    cExpr (HsAsPat n' (HsVar n)) = spec t t' $ EVar (tv n) where
-        (Forall _ (_ :=> t)) = getAssump n
-        Forall [] ((_ :=> t')) = getAssump n'
+    cExpr (HsAsPat n' (HsVar n)) = foldl eAp (EVar (tv n)) (map ty $ specialize t t') where
+        t = getAssump n
+        t' = getAssump n'
+    --cExpr (HsAsPat n' (HsVar n)) = spec t t' $ EVar (tv n) where
+        --(Forall _ (_ :=> t)) = getAssump n
+        --Forall [] ((_ :=> t')) = getAssump n'
hunk ./E/FromHs.hs 391
-        Forall [] ((_ :=> t')) = getAssump n'
+        --Forall [] ((_ :=> t')) = getAssump n'
+        t' = getAssump n'
hunk ./E/FromHs.hs 441
-        Just z -> z
+        Just z -> schemeToType z
hunk ./E/FromHs.hs 444
-        Just z -> z
+        Just z -> schemeToType z
hunk ./E/FromHs.hs 466
-        gg' a b = error $ "specialization: " <> parens  (prettyPrintType a) <+> parens (prettyPrintType b) <+> "in spec" <+> hsep (map parens [prettyPrintType g, prettyPrintType s, show e])
+        gg' a b = error $ "specialization: " <> parens  (prettyPrintType a) <+> parens (prettyPrintType b) <+> "\nin spec\n" <+> vcat (map parens [prettyPrintType g, prettyPrintType s, show e])
hunk ./E/FromHs.hs 483
+-- | determine what arguments must be passed to something of the first type, to transform it into something of the second type.
+specialize :: Type -> Type -> [Type]
+specialize TForAll {} TForAll {} = []  -- we assume program is typesafe
+specialize g@(TForAll vs (_ :=> t)) s = snds (gg t s)  where
+    ps = zip vs [0 :: Int ..]
+    gg a b = snubFst $ gg' a b
+    gg' (TAp t1 t2) (TAp ta tb) = gg' t1 ta ++ gg' t2 tb
+    gg' (TArrow t1 t2) (TArrow ta tb) = gg' t1 ta ++ gg' t2 tb
+    gg' (TCon a) (TCon b) = if a /= b then error "constructors don't match." else []
+    gg' (TVar a) t | Just n <- lookup a ps = [(n,t)]
+    gg' (TVar a) (TVar b) | a == b = []
+    gg' (TMetaVar a) (TMetaVar b) | a == b = []
+    gg' a b = error $ "specialization: " <> parens  (prettyPrintType a) <+> parens (prettyPrintType b) <+> "\nin spec\n" <+> vcat (map parens [prettyPrintType g, prettyPrintType s])
+specialize _g _s = []
hunk ./FrontEnd/Tc/Class.hs 11
+    assertEquivalant,
hunk ./FrontEnd/Tc/Class.hs 187
+
+assertEquivalant :: Preds -> Preds -> Tc ()
+assertEquivalant qs ps = do
+    assertEntailment qs ps
+    assertEntailment ps qs
hunk ./FrontEnd/Tc/Unify.hs 5
+import qualified Data.Map as Map
hunk ./FrontEnd/Tc/Unify.hs 7
-import Doc.PPrint
hunk ./FrontEnd/Tc/Unify.hs 8
-import FrontEnd.Tc.Type
-import Support.CanType
+import Doc.PPrint
+import FrontEnd.Tc.Class
hunk ./FrontEnd/Tc/Unify.hs 11
+import FrontEnd.Tc.Type
+import GenUtil
hunk ./FrontEnd/Tc/Unify.hs 15
-import GenUtil
+import Support.CanType
hunk ./FrontEnd/Tc/Unify.hs 162
-    bm (TForAll vs (ps :=> t)) (TForAll vs' (ps' :=> t')) = fail "SEQ2"
-    --bm a (TMetaVar mv)  = do
-     --   varBind mv a
-     --   return False
+    bm t1@TForAll {} (TForAll as2 qt2) = do
+        TForAll as1 (ps1 :=> r1) <- freshSigma t1
+        let (ps2 :=> r2) = inst mempty (Map.fromList [ (tyvarAtom a2,TVar a1) | a1 <- as1 | a2 <- as2 ]) qt2
+        printRule "SEQ2"
+        boxyMatch r1 r2
+        assertEquivalant ps1 ps2
+        return False
+
hunk ./test/Forall.hs 74
+xs :: [forall a . a -> a]
+xs = [id,const undefined,error "three"]
+
+myhead ::  [forall a . a -> a] -> (forall a . a -> a)
+myhead = head
+
hunk ./test/Forall.hs 84
+    putChar $ myhead xs 'z'