packages feed

typecheck-plugin-nat-simple 0.1.0.4 → 0.1.0.5

raw patch · 4 files changed

+60/−24 lines, 4 filesdep +ghc-tcplugins-extradep ~ghc

Dependencies added: ghc-tcplugins-extra

Dependency ranges changed: ghc

Files

src/Plugin/TypeCheck/Nat/Simple.hs view
@@ -27,8 +27,8 @@ --   >		=<< (,) <$> (givens =<< decodeAll gs) <*> (wanted =<< decode w)  plugin :: Plugin-plugin = typeCheckWith @L "Plugin.TypeCheck.Nat.Simple" \gs _ w -> do+plugin = typeCheckWith @L "Plugin.TypeCheck.Nat.Simple" \occ gs _ w -> do 	tell @L $ "givens: " .+. fromSDoc (ppr gs) 	tell @L $ "wanted: " .+. fromSDoc (ppr w) 	uncurry canDerive-		=<< (,) <$> (givens =<< decodeAll gs) <*> (wanted =<< decode w)+		=<< (,) <$> (givens =<< decodeAll occ gs) <*> (wanted =<< decode occ w)
src/Plugin/TypeCheck/Nat/Simple/Decode.hs view
@@ -4,11 +4,11 @@  module Plugin.TypeCheck.Nat.Simple.Decode ( 	-- * DECODE CT-	decodeAll, decode ) where+	decodeAll, decode, lookupOrdCondCompare ) where  import GHC.Tc.Types.Constraint (Ct) import GHC.Builtin.Types.Literals (-	typeNatAddTyCon, typeNatSubTyCon, typeNatLeqTyCon )+	typeNatAddTyCon, typeNatSubTyCon) -- , typeNatLeqTyCon ) import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon) import GHC.Core.TyCo.Rep (Type(..), TyLit(..)) import GHC.Types.Var (Var)@@ -20,6 +20,13 @@ import Data.Derivation.Expression (Exp(..), ExpType(..)) import Plugin.TypeCheck.Nat.Simple.UnNomEq (unNomEq) +import GHC.Tc.Plugin+import GHC.TcPluginM.Extra+import GHC.Data.FastString+import GHC.Unit.Module+import GHC.Types.Name.Occurrence+import GHC.Core.TyCon+ ---------------------------------------------------------------------------  -- * DECODE@@ -29,28 +36,34 @@ -- DECODE --------------------------------------------------------------------------- -decodeAll :: (Monoid w, IsSDoc w, Set w w) => [Ct] -> Try w w [Exp Var 'Boolean]-decodeAll = rights . (decode <$>)+decodeAll :: (Monoid w, IsSDoc w, Set w w) => (TyCon, TyCon) -> [Ct] -> Try w w [Exp Var 'Boolean]+decodeAll occ = rights . (decode occ <$>) -decode :: (Monoid w, IsSDoc w) => Ct -> Try w w (Exp Var 'Boolean)-decode = uncurry decodeTs <=< unNomEq+decode :: (Monoid w, IsSDoc w) => (TyCon, TyCon) -> Ct -> Try w w (Exp Var 'Boolean)+decode occ = uncurry (decodeTs occ) <=< unNomEq -decodeTs :: (Monoid w, IsSDoc w) => Type -> Type -> Try w w (Exp Var 'Boolean)-decodeTs (TyVarTy l) (TyVarTy r) = pure $ Var l :== Var r-decodeTs l r = (:==) <$> exBool l <*> exBool r <|> (:==) <$> exNum l <*> exNum r+decodeTs :: (Monoid w, IsSDoc w) => (TyCon, TyCon) -> Type -> Type -> Try w w (Exp Var 'Boolean)+decodeTs _ (TyVarTy l) (TyVarTy r) = pure $ Var l :== Var r+decodeTs occ l r = (:==) <$> exBool occ l <*> exBool occ r <|> (:==) <$> exNum l <*> exNum r  --------------------------------------------------------------------------- -- BOOLEAN AND NUMBER --------------------------------------------------------------------------- -exBool :: (Monoid s, IsSDoc e) => Type -> Try e s (Exp Var 'Boolean)-exBool (TyVarTy v) = pure $ Var v-exBool (TyConApp tc [])+exBool :: (Monoid s, IsSDoc e) => (TyCon, TyCon) -> Type -> Try e s (Exp Var 'Boolean)+exBool _ (TyVarTy v) = pure $ Var v+exBool _ (TyConApp tc []) 	| tc == promotedFalseDataCon = pure $ Bool False 	| tc == promotedTrueDataCon = pure $ Bool True-exBool (TyConApp tc [l, r])-	| tc == typeNatLeqTyCon = (:<=) <$> exNum l <*> exNum r-exBool t = throw . fromSDoc $ text "exBool: not boolean:" <+> ppr t+-- exBool (TyConApp tc [l, r])+--	| tc == typeNatLeqTyCon = (:<=) <$> exNum l <*> exNum r+exBool (oc, cmp) (TyConApp tc [_,+		TyConApp cmpNatTc [_, l, r],+		TyConApp t1 [], TyConApp t2 [], TyConApp f1 []])+	| tc == oc, cmpNatTc == cmp+	, t1 == promotedTrueDataCon, t2 == promotedTrueDataCon+	, f1 == promotedFalseDataCon = (:<=) <$> exNum l <*> exNum r+exBool _ t = throw . fromSDoc $ text "exBool: not boolean:" <+> ppr t  exNum :: (Monoid s, IsSDoc e) => Type -> Try e s (Exp Var 'Number) exNum (TyVarTy v) = pure $ Var v@@ -59,3 +72,17 @@ 	| tc == typeNatAddTyCon = (:+) <$> exNum l <*> exNum r 	| tc == typeNatSubTyCon = (:-) <$> exNum l <*> exNum r exNum t = throw . fromSDoc $ text "exNum: not number:" <+> ppr t++lookupOrdCondCompare :: TcPluginM (TyCon, TyCon)+lookupOrdCondCompare = do+	md2 <- lookupModule ordModule basePackage+	(,) <$> look md2 "OrdCond" <*> look md2 "Compare"++ordModule :: ModuleName+ordModule = mkModuleName "Data.Type.Ord"++basePackage :: FastString+basePackage = fsLit "base"++look :: Module -> String -> TcPluginM TyCon+look md s = tcLookupTyCon =<< lookupName md (mkTcOcc s)
src/Plugin/TypeCheck/Nat/Simple/TypeCheckWith.hs view
@@ -6,7 +6,7 @@ 	typeCheckWith ) where  import GHC.Plugins (-	Plugin(..), defaultPlugin, Expr(..), mkUnivCo, Role(..),+	Plugin(..), defaultPlugin, Expr(..), mkUnivCo, 	Outputable, ppr, text ) import GHC.Tc.Plugin (TcPluginM, tcPluginTrace) import GHC.Tc.Types (TcPlugin(..), TcPluginResult(..))@@ -18,19 +18,24 @@ import Data.Log (IsSDoc, fromSDoc) import Plugin.TypeCheck.Nat.Simple.UnNomEq (unNomEq) +import Plugin.TypeCheck.Nat.Simple.Decode (lookupOrdCondCompare)+import GHC.Core.TyCon+ ---------------------------------------------------------------------------  typeCheckWith :: (Monoid w, Outputable w, IsSDoc w, Set w w) =>-	String -> ([Ct] -> [Ct] -> Ct -> Try w w Bool) -> Plugin+	String -> ((TyCon, TyCon) -> [Ct] -> [Ct] -> Ct -> Try w w Bool) -> Plugin typeCheckWith hd ck = defaultPlugin { tcPlugin = const $ Just TcPlugin { 	tcPluginInit = pure (), tcPluginSolve = const $ solve hd ck, 	tcPluginStop = const $ pure () } }  solve :: (Monoid w, Outputable w, IsSDoc w, Set w w) =>-	String -> ([Ct] -> [Ct] -> Ct -> Try w w Bool) ->+	String -> ((TyCon, TyCon) -> [Ct] -> [Ct] -> Ct -> Try w w Bool) -> 	[Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult-solve hd ck gs ds ws = TcPluginOk rs [] <$ tcPluginTrace hd (ppr lgs)-	where (rs, lgs) = gatherSuccess $ result hd ck gs ds <$> ws+solve hd ck gs ds ws = do+	occ <- lookupOrdCondCompare+	let	(rs, lgs) = gatherSuccess $ result hd (ck occ) gs ds <$> ws+	TcPluginOk rs [] <$ tcPluginTrace hd (ppr lgs)  result :: (Monoid s, IsSDoc e) => 	String -> ([Ct] -> [Ct] -> Ct -> Try e s Bool) ->
typecheck-plugin-nat-simple.cabal view
@@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack ----- hash: a9ba3f2374494be0d74d84c38ca16841d48bfc5e88e9446906fc520669707902+-- hash: e2e0789fc40e15f06d431a711fa5db62d9d427d20e869202ae7f8e3cac3e5fb9  name:           typecheck-plugin-nat-simple-version:        0.1.0.4+version:        0.1.0.5 synopsis:       Simple type check plugin which calculate addition, subtraction and less-or-equal-than description:    Please see the README on GitHub at <https://github.com/YoshikuniJujo/typecheck-plugin-nat-simple#readme> category:       Compiler Plugin@@ -58,6 +58,7 @@       base >=4.7 && <5     , containers     , ghc >=9.0.2+    , ghc-tcplugins-extra   default-language: Haskell2010  test-suite typecheck-plugin-nat-simple-test-log@@ -72,6 +73,7 @@       base >=4.7 && <5     , containers     , ghc >=9.0.2+    , ghc-tcplugins-extra     , typecheck-plugin-nat-simple   default-language: Haskell2010 @@ -87,6 +89,7 @@       base >=4.7 && <5     , containers     , ghc >=9.0.2+    , ghc-tcplugins-extra     , typecheck-plugin-nat-simple   default-language: Haskell2010 @@ -102,5 +105,6 @@       base >=4.7 && <5     , containers     , ghc >=9.0.2+    , ghc-tcplugins-extra     , typecheck-plugin-nat-simple   default-language: Haskell2010