packages feed

typecheck-plugin-nat-simple (empty) → 0.1.0.0

raw patch · 27 files changed

+1439/−0 lines, 27 filesdep +basedep +containersdep +ghcsetup-changed

Dependencies added: base, containers, ghc, typecheck-plugin-nat-simple

Files

+ ChangeLog.md view
@@ -0,0 +1,3 @@+# Changelog for typecheck-plugin-nat-simple++## Unreleased changes
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Yoshikuni Jujo (c) 2020++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Yoshikuni Jujo nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,167 @@+# typecheck-plugin-nat-simple++## what's this++This package provide plugin which extend type checking of Nat.+The type checker can calculate only addition, subtraction and less or equal of+constants and variables.++(View sample code on directory sample/.)++## motivation++Suppose you need lengthed list. You define like following.+(View `sample/lengthed_tail.hs`)++```haskell+import GHC.TypeNats++infixr 6 :.++data List :: Nat -> * -> * where+        Nil :: List 0 a+	(:.) :: a -> List ln a -> List (ln + 1) a+```++And you want to define function `tail`.++```haskell+tail_ :: List (n + 1) a -> List n a+tail_ Nil = error "tail_: Nil"+tail_ (_ :. xs) = xs+```++But it cause type check error.++```+error:+  ・Could not deduce: ln ~ n+    from the context: (n + 1) ~ (ln + 1)+    ...+```++Type checker say "I cannot derive (ln == n) from (n + 1 == ln + 1)".+But it seems to be obvious.+You can use this plugin like following.++```haskell+{-# OPTIONS_GHC -fplugin=Plugin.TypeCheck.Nat.Simple #-}+```++Add it to top of the code, then type check succeed.++## more example++To show more example, I will use Data.Proxy.Proxy.+First examle is following (View `sample/mplus1_nplus1.hs`).++```haskell+foo :: (m + 1) ~ (n + 1) => Proxy m -> Proxy n+foo = id+```++If you don't use this plugin, then following error occur.++```+  ・Could not deduce: m ~ n+    from the context: (m + 1) ~ (n + 1)+    ...+```++Use this plugin, you can compile it.++Second example is following (View `sample/two_equations.hs`).++```haskell+foo :: ((x + y) ~ z, (w - y) ~ v) => Proxy (x + w) -> Proxy (z + v)+foo = id+```++Without this plugin, following error occur.++```+  ・Could not deduce: (x + w) ~ (z + v)+    from the context: ((x + y) ~ z, (w - y) ~ v)+    ...+```++Use this plugin, you can compile it.++## error and recovery++### type check error++See following code.++```haskell+foo :: Proxy (n - 1 + 1) -> Proxy n+foo = id+```++This cause type check error even if you use this plugin.++```+  ・Couldn't match type `n' with `(n - 1) + 1'+  ...+```++### research++What's wrong?+You can see type check log of this plugin like following.++```+% stack ghc sample/minus1plus1.hs -- -ddump-tc-trace 2>&1 | grep -A 20 'Plugin.TypeCheck.Nat.Simple'+...+givens ([Exp v 'Boolean]): given (Givens v): (Givens [])+exBool: not boolean: (n_a1s2[sk:1] - 1) + 1+wanted (Exp v 'Boolean): ((((Var n_a1s2[sk:1]) :- (Const 1)) :+ (Const 1)) :== (Var n_a1s2[sk:1]))+wanted (Wanted v): (Wanted [(0 == 0), (1 * n_a1s2[sk:1] >= 0), (-1 + 1 * n_a1s2[sk:1] >= 0), (1 * n_a1s2[sk:1] >= 0)])+canDerive1: (0 == 0) is self-contained+canDerive1: (1 * n_a1s2[sk:1] >= 0) is self-contained+canDerive1: (-1 + 1 * n_a1s2[sk:1] >= 0) cannot be derived from+canDerive1: (1 * n_a1s2[sk:1] >= 0) is self-contained+result: type checker: return False+...+```++See the line of `canDerive1: (- 1 + 1 * n_a1s2[sk:1] >= 0) cannot be derived from`.+It mean "`-1 + n_a1s2[sk:1]` should be greater or equal than 0. But no such context".++### try calculation more portably++You can try to caluculate more simply.++```+% stack ghci+> :set -XTypeApplications+> :module Data.Derivation.Parse Data.Derivation.CanDerive Control.Monad.Try Data.Maybe+> parseConstraint "n - 1 + 1 == n"+Just ((:==) ((:+) ((:=) (Var "n") (Const 1)) (Const 1)) (Var "n"))+> Just w = wanted @String <$> it+> gs = givens @String []+> fst . runTry $ uncurry canDerive =<< (,) <$> gs <*> w+Right False+```++The wanted constraint cannot be derived from empty given constraint.+Let's add `1 <= n` constraint.++```+> gs = given @String . maybeToList $ parseConstraint "1 <= n"+> fst . runTry $ uncurry canDerive =<< (,) <$> gs <*> w+Right True+```++OK! It succeed if you add `1 <= n` to given constraint.++### recovery++Let's add `1 <= n` context like following.++```haskell+foo :: 1 <= n => Proxy (n - 1 + 1) -> Proxy n+foo = id+```++Then it succeed to type check.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ sample/complex.hs view
@@ -0,0 +1,21 @@+{-# LANGUAGE ScopedTypeVariables, RankNTypes #-}+{-# LANGUAGE DataKinds, KindSignatures, TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}++import GHC.TypeNats+import Data.Proxy++main :: forall (a :: Nat) . IO ()+main = do+	print (foo (Proxy :: Proxy (a + 3)) :: Proxy (a + 3))+--	print (bar (Proxy :: Proxy (a + 3)) :: Proxy (a + 3))+--	print (bar (Proxy :: Proxy a) :: Proxy a)+	print (bar (Proxy :: Proxy 123) :: Proxy 123)+-- main = print (foo (Proxy :: Proxy a) :: Proxy a)++foo :: ((m + n) ~ (j + k), (n - j) ~ 3) => Proxy (m + 3) -> Proxy k+foo = id++bar :: ((m + n) ~ (j + k), (n - j) ~ 3) => Proxy k -> Proxy (m + 3)+bar = id
+ sample/lengthed_tail.hs view
@@ -0,0 +1,22 @@+{-# LANGUAGE DataKinds, KindSignatures, TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE StandaloneDeriving #-}+-- {-# OPTIONS_GHC -Wall -fno-warn-tabs #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}++import GHC.TypeNats++main :: IO ()+main = print . tail_ $ 1 :. 2 :. 3 :. Nil++infixr 6 :.++data List :: Nat -> * -> * where+	Nil :: List 0 a+	(:.) :: a -> List ln a -> List (ln + 1) a++deriving instance Show a => Show (List n a)++tail_ :: List (n + 1) a -> List n a+tail_ Nil = error "tail_: Nil"+tail_ (_ :. xs) = xs
+ sample/minus1plus1.hs view
@@ -0,0 +1,15 @@+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE DataKinds, TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}+-- {-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++import GHC.TypeNats+import Data.Proxy++main :: IO ()+main = print $ foo @1 Proxy++-- foo :: Proxy (n - 1 + 1) -> Proxy n+foo :: 1 <= n => Proxy (n - 1 + 1) -> Proxy n+foo = id
+ sample/mplus1_nplus1.hs view
@@ -0,0 +1,13 @@+{-# LANGUAGE DataKinds, TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}+-- {-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++import GHC.TypeNats+import Data.Proxy++main :: IO ()+main = print $ foo Proxy++foo :: (m + 1) ~ (n + 1) => Proxy m -> Proxy n+foo = id
+ sample/plus1minus1.hs view
@@ -0,0 +1,12 @@+{-# LANGUAGE DataKinds, TypeOperators #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}+-- {-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++import GHC.TypeNats+import Data.Proxy++main :: IO ()+main = print $ foo Proxy++foo :: Proxy (n + 1 - 1) -> Proxy n+foo = id
+ sample/two_equations.hs view
@@ -0,0 +1,14 @@+{-# LANGUAGE DataKinds, TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}+-- {-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++import GHC.TypeNats+import Data.Proxy++main :: IO ()+main = print $ foo Proxy++foo :: ((x + y) ~ z, (w - y) ~ v) => Proxy (x + w) -> Proxy (z + v)+foo = id
+ src/Control/Monad/StateT.hs view
@@ -0,0 +1,51 @@+{-# LANGUAGE BlockArguments, TupleSections #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Control.Monad.StateT (StateT(..), lift) where++import Control.Applicative (Alternative(..))+import Control.Arrow (first)+import Control.Monad (MonadPlus, (>=>))++---------------------------------------------------------------------------++-- * NEWTYPE STATE T+-- * INSTANCE+--	+ FUNCTOR+--	+ APPLICATIVE AND ALTERNATIVE+--	+ MONAD AND MONAD PLUS++---------------------------------------------------------------------------+-- NEWTYPE STATE T+---------------------------------------------------------------------------++newtype StateT s m a = StateT { runStateT :: s -> m (a, s) }++lift :: Functor m => m a -> StateT s m a+lift m = StateT \s -> (, s) <$> m++---------------------------------------------------------------------------+-- INSTANCE+---------------------------------------------------------------------------++-- FUNCTOR++instance Functor m => Functor (StateT s m) where+	f `fmap` StateT k = StateT $ ((f `first`) <$>) . k++-- APPLICATIVE AND ALTERNATIVE++instance Monad m => Applicative (StateT s m) where+	pure = StateT . (pure .) . (,)+	StateT kf <*> mx = StateT $ kf >=> \(f, s') -> (f <$> mx) `runStateT` s'++instance MonadPlus m => Alternative (StateT s m) where+	empty = StateT $ const empty+	StateT k <|> StateT l = StateT $ (<|>) <$> k <*> l++-- MONAD AND MONAD PLUS++instance Monad m => Monad (StateT s m) where+	StateT k >>= f = StateT $ k >=> \(x, s') -> f x `runStateT` s'++instance MonadPlus m => MonadPlus (StateT s m)
+ src/Control/Monad/Try.hs view
@@ -0,0 +1,114 @@+{-# LANGUAGE BlockArguments, LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Control.Monad.Try (+	-- * DATA TRY+	Try, maybeToTry,+	-- * RUN TRY+	runTry, gatherSuccess,+	-- * THROW AND CATCH ERROR+	throw, catch, rights,+	-- * WRITE AND GET LOG+	Set, tell, partial,+	-- * TOOL+	cons ) where++import Control.Applicative (Alternative(..))+import Control.Arrow (first)+import Control.Monad (MonadPlus)+import Data.Maybe (catMaybes)++---------------------------------------------------------------------------++-- * DATA TRY+--	+ DATA+--	+ INSTANCE+-- * RUN TRY+-- * THROW AND CATCH ERROR+-- * WRITE AND GET LOG+-- * TOOL++---------------------------------------------------------------------------+-- DATA TRY+---------------------------------------------------------------------------++-- DATA++data Try e w a = Try (Either e a) w deriving Show++try :: (Either e a -> w -> b) -> Try e w a -> b+try f (Try ex w) = f ex w++maybeToTry :: Monoid w => e -> Maybe a -> Try e w a+maybeToTry e = maybe (throw e) pure++-- INSTANCE++instance Functor (Try e w) where+	fmap f = try $ either (Try . Left) (Try . Right . f)++instance Monoid w => Applicative (Try e w) where+	pure = (`Try` mempty) . Right+	Try (Left e) w <*> _ = Try (Left e) w+	Try (Right f) w <*> mx = (\ex -> Try ex . (w <>)) `try` (f <$> mx)++instance Monoid w => Alternative (Try w w) where+	empty = Try (Left mempty) mempty+	Try (Left e) w <|> t = tell w >> tell e >> t+	t@(Try (Right _) _) <|> _ = t++instance Monoid w => Monad (Try e w) where+	Try (Left e) w >>= _ = Try (Left e) w+	Try (Right x) w >>= f = (\ex -> Try ex . (w <>)) `try` f x++instance Monoid w => MonadPlus (Try w w)++---------------------------------------------------------------------------+-- RUN TRY+---------------------------------------------------------------------------++runTry :: Try e w a -> (Either e a, w)+runTry (Try ex w) = (ex, w)++gatherSuccess :: (Monoid w, Set w w) => [Try w w a] -> ([a], w)+gatherSuccess = (either (const []) id `first`) . runTry . rights++---------------------------------------------------------------------------+-- THROW AND CATCH ERROR+---------------------------------------------------------------------------++throw :: Monoid w => e -> Try e w a+throw = (`Try` mempty) . Left++catch :: Semigroup w => Try e w a -> (e -> Try e w a) -> Try e w a+Try (Left e) w `catch` h = (\ex -> Try ex . (w <>)) `try` h e+t@(Try (Right _) _) `catch` _ = t++rights :: (Monoid w, Set w w) => [Try w w a] -> Try w w [a]+rights = (catMaybes <$>) . mapM ((`catch` (Nothing <$) . tell) . (Just <$>))++---------------------------------------------------------------------------+-- WRITE AND GET LOG+---------------------------------------------------------------------------++class Set x xs where set :: x -> xs++instance Set x x where set = id+instance Monoid xs => Set x (x, xs) where set x = (x, mempty)++instance {-# OVERLAPPABLE #-} (Monoid y, Set x xs) => Set x (y, xs) where+	set x = (mempty, set x)++tell :: Set w ws => w -> Try e ws ()+tell = Try (Right ()) . set++partial :: Try e (w, ws) a -> Try e ws (Either e a, w)+partial (Try ex (w, ws)) = Try (Right (ex, w)) ws++---------------------------------------------------------------------------+-- TOOL+---------------------------------------------------------------------------++cons :: (Monoid w, Set w w) => Either w a -> [a] -> Try w w [a]+cons = either (flip (<$) . tell) ((pure .) . (:))
+ src/Data/Derivation/CanDerive.hs view
@@ -0,0 +1,122 @@+{-# LANGUAGE BlockArguments, OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables, TypeApplications #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Data.Derivation.CanDerive (+	-- * CAN DERIVE+	canDerive,+	-- * GIVENS+	Givens, givens,+	-- * WANTED+	Wanted, wanted ) where++import Prelude hiding (unwords, log)++import Control.Arrow (second)+import Control.Monad ((<=<))+import Control.Monad.Try (Try, throw, tell, cons)+import Data.Map.Strict (empty)+import Data.Either (partitionEithers)+import Data.List (unfoldr, (\\), nub, partition, sort)+import Data.Bool (bool)+import Data.String (IsString)+import Data.Log (Log, (.+.), intersperse, unwords, log, Loggable(..))+import Data.Derivation.Constraint (+	Constraint,+	vars, has, isDerivFrom, positives, selfContained, eliminate )+import Data.Derivation.Expression.Internal (+	Exp, ExpType(..), constraint, varBool )++---------------------------------------------------------------------------++-- * CAN DERIVE+-- * GIVENS+--	+ NEWTYPE GIVENS AND CONSTRUCTOR+--	+ GIVENS VARIABLES+--	+ REMOVE VARIABLE+-- * WANTED++---------------------------------------------------------------------------+-- CAN DERIVE+---------------------------------------------------------------------------++canDerive :: (IsString s, Ord v) => Givens v -> Wanted v -> Try e (Log s v) Bool+canDerive g = (canDerive1 g `allM`) . unWanted++allM :: Monad m => (a -> m Bool) -> [a] -> m Bool+p `allM` xs = and <$> p `mapM` xs++canDerive1 :: forall s v e .+	(IsString s, Ord v) => Givens v -> Wanted1 v -> Try e (Log s v) Bool+canDerive1 g w = (s || d) <$ if s+	then t $ ttl .+. lw .+. " is self-contained"+	else t $ ttl .+. lw .+. " can" .+. nt .+. " be derived from"+	where+	s = selfContained w+	d = any (w `isDerivFrom`) . unGivens . foldr rmVar g $ gVars g \\ vars w+	t = tell @(Log s v)+	ttl = "canDerive1: "; lw = log w; nt = bool "not" "" d++---------------------------------------------------------------------------+-- GIVENS+---------------------------------------------------------------------------++-- NEWTYPE GIVENS AND CONSTRUCTOR++newtype Givens v = Givens { unGivens :: [Constraint v] } deriving Show++instance IsString s => Loggable s v (Givens v) where+	log (Givens cs) = "(Givens [" .+. intersperse ", " (log <$> cs) .+. "])"++givens :: forall s v . (IsString s, Ord v) =>+	[Exp v 'Boolean] -> Try (Log s v) (Log s v) (Givens v)+givens gs = do+	t $ "givens ([Exp v 'Boolean]): " .+. unwords (log <$> gs)+	gs' <- Givens . nub . sort . ((++) <$> id <*> (positives <$>)) . concat+		<$> (uncurry cons <=< constraint (varBool gs)) `mapM` gs+	gs' <$ t ("givens (Givens v): " .+. log gs')+	where t = tell @(Log s v)++-- GIVENS VARIABLES++gVars :: Ord v => Givens v -> [Maybe v]+gVars = nub . sort . concat . (vars <$>) . unGivens++-- REMOVE VARIABLE++rmVar :: Ord v => Maybe v -> Givens v -> Givens v+rmVar v (Givens gs) = Givens . sort . concat . uncurry (:)+	. second (unfoldUntil null (rvStep v)) $ partition (not . (`has` v)) gs++rvStep :: Ord v => Maybe v -> [Constraint v] -> ([Constraint v], [Constraint v])+rvStep _ [] = ([], [])+rvStep v (c : cs) = partitionEithers $ rmVar1 v c <$> cs++rmVar1 :: Ord v => Maybe v -> Constraint v ->+	Constraint v -> Either (Constraint v) (Constraint v)+rmVar1 v c0 c = maybe (Right c) Left $ eliminate v c0 c++unfoldUntil :: (s -> Bool) -> (s -> (r, s)) -> s -> [r]+unfoldUntil p f = unfoldr $ flip bool Nothing <$> Just . f <*> p++---------------------------------------------------------------------------+-- WANTED+---------------------------------------------------------------------------++newtype Wanted v = Wanted { unWanted :: [Wanted1 v] } deriving Show++type Wanted1 v = Constraint v++instance IsString s => Loggable s v (Wanted v) where+	log (Wanted cs) = "(Wanted [" .+. intersperse ", " (log <$> cs) .+. "])"++wanted :: forall s v . (IsString s, Ord v) =>+	Exp v 'Boolean -> Try (Log s v) (Log s v) (Wanted v)+wanted w = do+	t $ "wanted (Exp v 'Boolean): " .+. log w+	(e, s) <- constraint empty w+	w' <- either throw (pure . Wanted . (: s)) e+	w' <$ t ("wanted (Wanted v): " .+. log w')+	where t = tell @(Log s v)
+ src/Data/Derivation/Constraint.hs view
@@ -0,0 +1,144 @@+{-# LANGUAGE BlockArguments, LambdaCase, OverloadedStrings #-}+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Data.Derivation.Constraint (+	Constraint, equal, greatEqualThan, greatThan, vars, has,+	isDerivFrom, positives, selfContained, eliminate,+	Poly, (.+), (.-) ) where++import Prelude hiding (null, filter)++import Control.Monad (guard)+import Data.Map.Strict (Map, null, singleton, (!?), filter, toList, lookupMin)+import Data.Map.Merge.Strict (+	merge, preserveMissing, mapMissing,+	zipWithMatched, zipWithMaybeMatched )+import Data.Maybe (isJust)+import Data.String (IsString, fromString)+import Data.Log (Log, logVar, (.+.), intersperse, Loggable(..))++---------------------------------------------------------------------------++-- * CONSTRAINT+--	+ DATA CONSTRAINT+--	+ CONSTRUCT+--	+ READ+-- 	+ CONVERT+-- * POLYNOMIAL+-- 	+ TYPE POLY+-- 	+ CONSTRUCT+-- 	+ READ+-- 	+ CONVERT++---------------------------------------------------------------------------+-- CONSTRAINT+---------------------------------------------------------------------------++-- DATA CONSTRAINT++data Constraint v = Eq (Poly v) | Geq (Poly v) deriving (Show, Eq, Ord)++constraint :: (Poly v -> a) -> (Poly v -> a) -> Constraint v -> a+constraint f g = \case Eq p -> f p; Geq p -> g p++instance IsString s => Loggable s v (Constraint v) where+	log = constraint+		(\p -> "(" .+. polyToLog (toList p) .+. " == 0)")+		(\p -> "(" .+. polyToLog (toList p) .+. " >= 0)")++-- CONSTRUCT++equal :: Ord v => Poly v -> Poly v -> Constraint v+l `equal` r = Eq . posit . reduce $ l .- r++greatEqualThan :: Ord v => Poly v -> Poly v -> Constraint v+l `greatEqualThan` r = Geq . reduce $ l .- r++greatThan :: Ord v => Poly v -> Poly v -> Constraint v+l `greatThan` r = Geq $ reduce (l .- r) .- singleton Nothing 1++-- READ++vars :: Ord v => Constraint v -> [Maybe v]+vars = (fst <$>) . constraint toList toList++has :: Ord v => Constraint v -> Maybe v -> Bool+has = constraint (\p -> isJust . (p !?)) (\p -> isJust . (p !?))++selfContained :: Constraint v -> Bool+selfContained = constraint null $ all (>= 0)++isDerivFrom :: Ord v => Constraint v -> Constraint v -> Bool+Eq w `isDerivFrom` Eq g = w == g+Geq w `isDerivFrom` Eq g = w `isGeqThan` g+Geq w `isDerivFrom` Geq g = w `isGeqThan` g+_ `isDerivFrom` _ = False++-- CONVERT++positives :: Constraint v -> Constraint v+positives = constraint Eq $ Geq . filter (>= 0)++eliminate ::+	Ord v => Maybe v -> Constraint v -> Constraint v -> Maybe (Constraint v)+eliminate v (Eq l) (Eq r) = Eq . posit . reduce . uncurry (.+) <$> alignEE v l r+eliminate v (Eq l) (Geq r) = Geq . reduce . uncurry (.+) <$> alignEG v l r+eliminate v (Geq l) (Geq r) = Geq . reduce . uncurry (.+) <$> alignGG v l r+eliminate v l r = eliminate v r l++type Aligned v = Maybe (Poly v, Poly v)++alignEE :: Ord v => Maybe v -> Poly v -> Poly v -> Aligned v+alignEE v l r =+	(<$> ((,) <$> l !? v <*> r !? v)) \(m, s) -> (l `mul` s, r `mul` (- m))++alignEG :: Ord v => Maybe v -> Poly v -> Poly v -> Aligned v+alignEG v l r = (<$> ((,) <$> l !? v <*> r !? v)) \(m, s) ->+	(l `mul` (- signum m * s), r `mul` abs m)++alignGG :: Ord v => Maybe v -> Poly v -> Poly v -> Aligned v+alignGG v l r = (,) <$> l !? v <*> r !? v >>= \(m, s) ->+	(l `mul` abs s, r `mul` abs m) <$ guard (m * s < 0)++---------------------------------------------------------------------------+-- POLYNOMIAL+---------------------------------------------------------------------------++-- TYPE POLY++type Poly v = Map (Maybe v) Integer++polyToLog :: IsString s => [(Maybe v, Integer)] -> Log s v+polyToLog [] = "0"+polyToLog ps = intersperse " + " $ polyToLog1 <$> ps++polyToLog1 :: IsString s => (Maybe v, Integer) -> Log s v+polyToLog1 (Nothing, n) = fromString $ show n+polyToLog1 (Just v, n) = fromString (show n ++ " * ") .+. logVar v++-- CONSTRUCT++(.+), (.-) :: Ord v => Poly v -> Poly v -> Poly v+(.+) = merge preserveMissing preserveMissing+	(zipWithMaybeMatched \_ a b -> (<$) <$> id <*> guard . (/= 0) $ a + b)+(.-) = merge preserveMissing (mapMissing $ const negate)+	(zipWithMaybeMatched \_ a b -> (<$) <$> id <*> guard . (/= 0) $ a - b)++-- READ++isGeqThan :: Ord v => Poly v -> Poly v -> Bool+isGeqThan = (and .) . merge+	(mapMissing \_ nl -> nl >= 0)+	(mapMissing \_ nr -> nr <= 0) (zipWithMatched $ const (>=))++-- CONVERT++posit :: Poly v -> Poly v+posit p = p `maybe` ((p `mul`) . signum . snd) $ lookupMin p++reduce :: Poly v -> Poly v+reduce = divide <$> id <*> foldr gcd 0++mul, divide :: Poly v -> Integer -> Poly v+mul p = (<$> p) . (*); divide p = (<$> p) . flip div
+ src/Data/Derivation/Expression.hs view
@@ -0,0 +1,7 @@+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Data.Derivation.Expression (+	-- * DATA EXP+	Exp(..), ExpType(..) ) where++import Data.Derivation.Expression.Internal (Exp(..), ExpType(..))
+ src/Data/Derivation/Expression/Internal.hs view
@@ -0,0 +1,158 @@+{-# LANGUAGE BlockArguments, LambdaCase, OverloadedStrings #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Data.Derivation.Expression.Internal (+	Exp(..), ExpType(..), constraint, varBool ) where++import Prelude hiding ((<>), log)++import Outputable (Outputable(..), SDoc, (<>), (<+>), text)+import Control.Arrow (first, second)+import Control.Monad.Try (Try, throw, tell, partial)+import Data.Map.Strict (Map, (!?), empty, singleton, insert)+import Data.Maybe (fromJust)+import Data.List (find)+import Data.String (IsString, fromString)+import Data.Log (Log, (.+.), logVar, Loggable(..))+import Data.Derivation.Constraint (+	Constraint, equal, greatEqualThan, greatThan, Poly, (.+), (.-) )++---------------------------------------------------------------------------++-- * DATA EXP+--	+ DATA+--	+ INSTANCE+-- * CONSTRAINT+--	+ CONSTRAINT+--	+ PROCESS EQUATION+-- * POLYNOMIAL+-- * MAP FROM VARIABLE TO BOOL++---------------------------------------------------------------------------+-- DATA EXP+---------------------------------------------------------------------------++-- DATA++data Exp v t where+	Bool :: Bool -> Exp v 'Boolean; Var :: v -> Exp v t+	Const :: Integer -> Exp v 'Number+	(:==) :: Exp v t -> Exp v t -> Exp v 'Boolean+	(:<=) :: Exp v 'Number -> Exp v 'Number -> Exp v 'Boolean+	(:+) :: Exp v 'Number -> Exp v 'Number -> Exp v 'Number+	(:-) :: Exp v 'Number -> Exp v 'Number -> Exp v 'Number++data ExpType = Boolean | Number deriving Show++-- INSTANCE++deriving instance Show v => Show (Exp v t)++instance Outputable v => Outputable (Exp v t) where+	ppr = \case+		Bool b -> text "(Bool" <+> ppr b <> text ")"+		Var v -> text "(Var" <+> ppr v <> text ")"+		Const n -> text "(Const" <+> ppr n <> text ")"+		l :== r -> pprOp ":==" l r; l :<= r -> pprOp ":<=" l r+		l :+ r -> pprOp ":+" l r; l :- r -> pprOp ":-" l r++pprOp :: Outputable v => String -> Exp v t -> Exp v t -> SDoc+pprOp op l r = text "(" <> ppr l <+> text op <+> ppr r <> text ")"++instance IsString s => Loggable s v (Exp v t) where+	log = \case+		Bool b -> fromString $ "(Bool " ++ show b ++ ")"+		Var v -> fromString "(Var " .+. logVar v .+. fromString ")"+		Const n -> fromString $ "(Const " ++ show n ++ ")"+		l :== r -> logOp ":==" l r; l :<= r -> logOp ":<=" l r+		l :+ r -> logOp ":+" l r; l :- r -> logOp ":-" l r++logOp :: IsString s => String -> Exp v t -> Exp v t -> Log s v+logOp op l r = fromString "(" .+.+	log l .+. fromString (" " ++ op ++ " ") .+. log r .+. fromString ")"++---------------------------------------------------------------------------+-- CONSTRAINT+---------------------------------------------------------------------------++-- CONSTRAINT++constraint :: (Monoid w, IsString s, Ord v) => VarBool v -> Exp v 'Boolean ->+	Try (Log s v) w (Either (Log s v) (Constraint v), [Constraint v])+constraint vb ex = partial $ procEq vb ex True++-- PROCCESS EQUATION++procEq :: (Monoid w, IsString s, Ord v) => VarBool v -> Exp v 'Boolean ->+	Bool -> Try (Log s v) ([Constraint v], w) (Constraint v)+procEq _ b@(Bool _) _ = throw $ "procEq: only Boolean value: " .+. log b+procEq _ v@(Var _) _ = throw $ "procEq: only Variable: " .+. log v+procEq _ (l :<= r) False = greatThan <$> poly l <*> poly r+procEq _ (l :<= r) True = greatEqualThan <$> poly r <*> poly l+procEq vb (l :== Bool r) b = procEq vb l (r == b)+procEq vb (Bool l :== r) b = procEq vb r (l == b)+procEq vb e@(l :== Var r) b | Just br <- vb !? r = case l of+	_ :== _ -> procEq vb l (br == b); _ :<= _ -> procEq vb l (br == b)+	_ -> throw $ "procEq: can't interpret: " .+. log e+procEq vb e@(Var l :== r) b | Just bl <- vb !? l = case r of+	_ :== _ -> procEq vb r (bl == b); _ :<= _ -> procEq vb r (bl == b)+	_ -> throw $ "procEq: can't interpret: " .+. log e+procEq _ e@(l :== r) True = case (l, r) of+	(Const _, _) -> equal <$> poly l <*> poly r+	(_ :+ _, _) -> equal <$> poly l <*> poly r+	(_ :- _, _) -> equal <$> poly l <*> poly r+	(_, Const _) -> equal <$> poly l <*> poly r+	(_, _ :+ _) -> equal <$> poly l <*> poly r+	(_, _ :- _) -> equal <$> poly l <*> poly r+	(Var v, Var w) -> equal <$> poly (Var v) <*> poly (Var w)+	_ -> throw $ "procEq: can't interpret: " .+. log e .+. " == True"+procEq _ e@(_ :== _) False =+	throw $ "procEq: can't interpret: " .+. log e .+. " == False"++---------------------------------------------------------------------------+-- POLYNOMIAL+---------------------------------------------------------------------------++poly :: (Monoid s, IsString e, Ord v) =>+	Exp v 'Number -> Try e ([Constraint v], s) (Poly v)+poly = \case+	Const n	| n < 0 -> throw+			. fromString $ "poly: Negative constant " ++ show n+		| 0 <- n -> pure empty+		| otherwise -> pure $ singleton Nothing n+	Var v -> let p = singleton (Just v) 1 in+		p <$ tell [p `greatEqualThan` empty]+	l :+ r -> (.+) <$> poly l <*> poly r+	l :- r -> (,) <$> poly l <*> poly r >>= \(pl, pr) ->+		pl .- pr <$ tell [pl `greatEqualThan` pr]++---------------------------------------------------------------------------+-- MAP FROM VARIABLES TO BOOL+---------------------------------------------------------------------------++type VarBool v = Map v Bool++varBool :: Ord v => [Exp v 'Boolean] -> VarBool v+varBool = snd . untilFixed (uncurry vbStep) . vbInit++vbInit :: Ord v => [Exp v 'Boolean] -> ([(v, v)], VarBool v)+vbInit [] = ([], empty)+vbInit (Var l :== Var r : es) = ((l, r) :) `first` vbInit es+vbInit (Var l :== Bool r : es) = insert l r `second` vbInit es+vbInit (Bool l :== Var r : es) = insert r l `second` vbInit es+vbInit (_ : es) = vbInit es++vbStep :: Ord v => [(v, v)] -> VarBool v -> ([(v, v)], VarBool v)+vbStep [] vb = ([], vb)+vbStep ((l, r) : vs) vb = case (vb !? l, vb !? r) of+	(Just bl, _) -> vbStep vs $ insert r bl vb+	(Nothing, Just br) -> vbStep vs $ insert l br vb+	(Nothing, Nothing) -> ((l, r) :) `first` vbStep vs vb++untilFixed :: Eq a => (a -> a) -> a -> a+untilFixed f x = fst . fromJust . find (uncurry (==)) $ zip xs (tail xs)+	where xs = iterate f x
+ src/Data/Derivation/Parse.hs view
@@ -0,0 +1,109 @@+{-# LANGUAGE DataKinds #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Data.Derivation.Parse (+	-- * PARSE CONSTRAINT+	parseConstraint, Var ) where++import Control.Applicative (empty, (<|>), many)+import Control.Arrow (second)+import Data.Function ((&))+import Data.Maybe (listToMaybe)+import Data.List (uncons, unfoldr)+import Data.Char (isDigit, isLower)+import Data.Parse (Parse, parse, unparse, (>>!))+import Data.Derivation.Expression (Exp(..), ExpType(..))++import qualified Data.Bool as B (bool)++---------------------------------------------------------------------------++-- * PARSE CONSTRAINT+-- * MEMO+-- * GRAMMAR+-- * PICK AND CHECK++---------------------------------------------------------------------------+-- PARSE CONSTRAINT+---------------------------------------------------------------------------++parseConstraint :: String -> Maybe (Exp Var 'Boolean)+parseConstraint = (fst <$>) . constraint . memo . unfoldr (listToMaybe . lex)++---------------------------------------------------------------------------+-- MEMO+---------------------------------------------------------------------------++data Memo = Memo {+	constraint, equal, bool, lessEqual :: M (Exp Var 'Boolean),+	polynomial, number :: M (Exp Var 'Number), token :: M String }++type M a = Maybe (a, Memo); type Var = String++memo :: [String] -> Memo+memo ts = m where+	m = Memo ct eq bl le pl nm tk+	ct = pConstraint `unparse` m+	eq = pEqual `unparse` m+	bl = pBool `unparse` m+	le = pLessEqual `unparse` m+	pl = pPolynomial `unparse` m+	nm = pNumber `unparse` m+	tk = (memo `second`) <$> uncons ts++---------------------------------------------------------------------------+-- GRAMMAR+---------------------------------------------------------------------------++-- Constraint <- Equal / LessEqual+-- Equal <-+--	var "==" var !("+" / "-" / "<=") /+--	var "==" Polynomial !"<=" /+--	var "==" Bool /+--	Polynomial "==" Polynomial /+--	Bool "==" Bool+-- Bool <- LessEqual / "F" / "T" / var+-- LessEqual <- Polynomial "<=" Polynomial+-- Polynomial <- Number ("+" Number / "-" Number)*+-- Number <- <digit string> / var / "(" Polynomial ")"++pConstraint :: Parse Memo (Exp Var 'Boolean)+pConstraint = parse equal <|> parse lessEqual++pEqual :: Parse Memo (Exp Var 'Boolean)+pEqual =+	(:==) <$> var <* pick "==" <*> var+		>>! (pick "+" <|> pick "-" <|> pick "<=") <|>+	(:==) <$> var <* pick "==" <*> parse polynomial >>! pick "<=" <|>+	(:==) <$> var <* pick "==" <*> parse bool <|>+	(:==) <$> parse polynomial <* pick "==" <*> parse polynomial <|>+	(:==) <$> parse bool <* pick "==" <*> parse bool++pBool :: Parse Memo (Exp Var 'Boolean)+pBool =	parse lessEqual <|>+	Bool False <$ pick "F" <|> Bool True <$ pick "T" <|> var++pLessEqual :: Parse Memo (Exp Var 'Boolean)+pLessEqual = (:<=) <$> parse polynomial <* pick "<=" <*> parse polynomial++pPolynomial :: Parse Memo (Exp Var 'Number)+pPolynomial = foldl (&) <$> parse number <*> many (+	flip (:+) <$> (pick "+" *> parse number) <|>+	flip (:-) <$> (pick "-" *> parse number) )++pNumber :: Parse Memo (Exp Var 'Number)+pNumber = Const . read <$> check (all isDigit) <|> var <|>+	pick "(" *> parse polynomial <* pick ")"++var :: Parse Memo (Exp Var t)+var = Var <$> check (all isLower)++---------------------------------------------------------------------------+-- PICK AND CHECK+---------------------------------------------------------------------------++pick :: String -> Parse Memo String+pick = check . (==)++check :: (String -> Bool) -> Parse Memo String+check p = parse token >>= B.bool empty <$> pure <*> p
+ src/Data/Log.hs view
@@ -0,0 +1,111 @@+{-# LANGUAGE BlockArguments, LambdaCase, OverloadedStrings #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Data.Log (+	-- * LOG+	-- ** DATA LOG+	Log, logVar, (.+.), intersperse, unwords,+	-- ** CLASS+	Loggable(..), Message(..),+	-- * SDOC+	IsSDoc(..), SDocStr ) where++import Prelude hiding (unwords, log)++import Outputable (Outputable, SDoc, empty, ppr, text, ($$))+import Data.String (IsString(..))++import qualified Outputable as O ((<>))++---------------------------------------------------------------------------++-- * LOG+--	+ NEWTYPE LOG+--	+ INSTANCE+--	+ FUNCTION+--	+ CLASS+-- * SDOC++---------------------------------------------------------------------------+-- LOG+---------------------------------------------------------------------------++-- NEWTYPE LOG++newtype Log s v = Log ([[Either s v]] -> [[Either s v]])++-- INSTANCE++instance Semigroup (Log s v) where Log l <> Log r = Log $ l . r+instance Monoid (Log s v) where mempty = Log id++instance (Show s, Show v) => Show (Log s v) where+	show (Log k) = "(Log (" ++ show (k []) ++ " ++))"++instance (Outputable s, Outputable v) => Outputable (Log s v) where+	ppr (Log k) = foldr ($$) empty $ pprLog1 <$> k []++pprLog1 :: (Outputable s, Outputable v) => [Either s v] -> SDoc+pprLog1 = foldr (O.<>) empty . (either ppr ppr <$>)++instance (Message s, Show v) => Message (Log s v) where+	message (Log k) = unlines $ messageLog1 <$> k []++messageLog1 :: (Message s, Show v) => [Either s v] -> String+messageLog1 = concatMap $ either message show++instance IsString s => IsString (Log s v) where+	fromString = Log . (++) . ((: []) . Left . fromString <$>) . lines++instance IsSDoc s => IsSDoc (Log s v) where+	fromSDoc = Log . (:) . (: []) . Left . fromSDoc++-- FUNCTION++logVar :: v -> Log s v+logVar v = Log ([Right v] :)++infixr 7 .+.++(.+.) :: Log s v -> Log s v -> Log s v+Log l .+. Log r = Log $ (l [] %) . r where+	[] % yss = yss+	[xs] % (ys : yss) = (xs ++ ys) : yss+	(xs : xss) % yss = xs : (xss % yss)++intersperse :: Log s v -> [Log s v] -> Log s v+intersperse s = \case [] -> mempty; ls -> foldr1 (\l -> (l .+.) . (s .+.)) ls++unwords :: IsString s => [Log s v] -> Log s v+unwords = intersperse " "++-- CLASS++class Loggable s v a where log :: a -> Log s v++class Message s where+	message :: s -> String+	messageList :: [s] -> String+	messageList = unlines . (message <$>)++instance Message s => Message [s] where message = messageList+instance Message Char where message = (: []); messageList = id++---------------------------------------------------------------------------+-- SDOC STRING+---------------------------------------------------------------------------++class IsSDoc s where fromSDoc :: SDoc -> s++data SDocStr = SDocStrEmpty | SDocStr SDoc++instance Semigroup SDocStr where+	SDocStrEmpty <> r = r; l <> SDocStrEmpty = l+	SDocStr l <> SDocStr r = SDocStr $ l $$ r++instance Monoid SDocStr where mempty = SDocStrEmpty+instance Outputable SDocStr where ppr SDocStrEmpty = empty; ppr (SDocStr s) = s+instance IsString SDocStr where fromString = SDocStr . text+instance IsSDoc SDocStr where fromSDoc = SDocStr
+ src/Data/Parse.hs view
@@ -0,0 +1,20 @@+{-# LANGUAGE BlockArguments #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Data.Parse (Parse, parse, unparse, (>>!)) where++import Control.Applicative (empty)+import Control.Monad ((>=>))+import Control.Monad.StateT (StateT(..))++type Parse s = StateT s Maybe++parse :: (s -> Maybe (a, s)) -> Parse s a+parse = StateT++unparse :: Parse s a -> s -> Maybe (a, s)+unparse = runStateT++(>>!) :: Parse s a -> Parse s b -> Parse s a+p >>! nla = parse $ unparse p >=> \r@(_, s) ->+	maybe (pure r) (const empty) $ nla `unparse` s
+ src/Plugin/TypeCheck/Nat/Simple.hs view
@@ -0,0 +1,34 @@+{-# LANGUAGE BlockArguments, OverloadedStrings #-}+{-# LANGUAGE TypeApplications #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Plugin.TypeCheck.Nat.Simple (+	-- * PLUGIN+	plugin ) where++import Prelude hiding (log)++import GhcPlugins (Plugin, Var, ppr)+import Control.Monad.Try (tell)+import Data.Log (Log, (.+.), fromSDoc, SDocStr)+import Data.Derivation.CanDerive (canDerive, givens, wanted)+import Plugin.TypeCheck.Nat.Simple.TypeCheckWith (typeCheckWith)+import Plugin.TypeCheck.Nat.Simple.Decode (decode, decodeAll)++type L = Log SDocStr Var++-- | > type L = Log SDocStr Var+--   >+--   > plugin :: Plugin+--   > plugin = typeCheckWith @L "Plugin.TypeCheck.Nat.Simple" \gs _ w ->+--   >	tell @L $ "givens: " .+. fromSDoc (ppr gs)+--   >	tell @L $ "wanted: " .+. fromSDoc (ppr w)+--   >	uncurry canDerive+--   >		=<< (,) <$> (givens =<< decodeAll gs) <*> (wanted =<< decode w)++plugin :: Plugin+plugin = typeCheckWith @L "Plugin.TypeCheck.Nat.Simple" \gs _ w -> do+	tell @L $ "givens: " .+. fromSDoc (ppr gs)+	tell @L $ "wanted: " .+. fromSDoc (ppr w)+	uncurry canDerive+		=<< (,) <$> (givens =<< decodeAll gs) <*> (wanted =<< decode w)
+ src/Plugin/TypeCheck/Nat/Simple/Decode.hs view
@@ -0,0 +1,60 @@+{-# LANGUAGE BlockArguments, OverloadedStrings #-}+{-# LANGUAGE DataKinds #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Plugin.TypeCheck.Nat.Simple.Decode (+	-- * DECODE CT+	decodeAll, decode ) where++import TcRnTypes (Ct)+import TcTypeNats (typeNatAddTyCon, typeNatSubTyCon, typeNatLeqTyCon)+import TysWiredIn (promotedFalseDataCon, promotedTrueDataCon)+import TyCoRep (Type(..), TyLit(..))+import Var (Var)+import Outputable (ppr, text, (<+>))+import Control.Applicative ((<|>))+import Control.Monad ((<=<))+import Control.Monad.Try (Try, throw, rights, Set)+import Data.Log (IsSDoc, fromSDoc)+import Data.Derivation.Expression (Exp(..), ExpType(..))+import Plugin.TypeCheck.Nat.Simple.UnNomEq (unNomEq)++---------------------------------------------------------------------------++-- * DECODE+-- * BOOLEAN AND NUMBER++---------------------------------------------------------------------------+-- DECODE+---------------------------------------------------------------------------++decodeAll :: (Monoid w, IsSDoc w, Set w w) => [Ct] -> Try w w [Exp Var 'Boolean]+decodeAll = rights . (decode <$>)++decode :: (Monoid w, IsSDoc w) => Ct -> Try w w (Exp Var 'Boolean)+decode = uncurry decodeTs <=< 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++---------------------------------------------------------------------------+-- BOOLEAN AND NUMBER+---------------------------------------------------------------------------++exBool :: (Monoid s, IsSDoc e) => 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++exNum :: (Monoid s, IsSDoc e) => Type -> Try e s (Exp Var 'Number)+exNum (TyVarTy v) = pure $ Var v+exNum (LitTy (NumTyLit n)) = pure $ Const n+exNum (TyConApp tc [l, r])+	| tc == typeNatAddTyCon = (:+) <$> exNum l <*> exNum r+	| tc == typeNatSubTyCon = (:-) <$> exNum l <*> exNum r+exNum t = throw . fromSDoc $ text "exNum: not number:" <+> ppr t
+ src/Plugin/TypeCheck/Nat/Simple/TypeCheckWith.hs view
@@ -0,0 +1,41 @@+{-# LANGUAGE OverloadedStrings #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Plugin.TypeCheck.Nat.Simple.TypeCheckWith (+	-- * TYPE CHECK WITH+	typeCheckWith ) where++import GhcPlugins (+	Plugin(..), defaultPlugin, Expr(..), mkUnivCo, Role(..),+	Outputable, ppr, text )+import TcPluginM (TcPluginM, tcPluginTrace)+import TcRnTypes (TcPlugin(..), Ct, TcPluginResult(..))+import TcEvidence (EvTerm(..))+import TyCoRep (UnivCoProvenance(..))+import Control.Monad.Try (Try, gatherSuccess, throw, Set)+import Data.Bool (bool)+import Data.Log (IsSDoc, fromSDoc)+import Plugin.TypeCheck.Nat.Simple.UnNomEq (unNomEq)++---------------------------------------------------------------------------++typeCheckWith :: (Monoid w, Outputable w, IsSDoc w, Set w w) =>+	String -> ([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) ->+	[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++result :: (Monoid s, IsSDoc e) =>+	String -> ([Ct] -> [Ct] -> Ct -> Try e s Bool) ->+	[Ct] -> [Ct] -> Ct -> Try e s (EvTerm, Ct)+result hd ck gs ds w = unNomEq w >>= \(l, r) ->+	bool (throw em) (pure (et l r, w)) =<< ck gs ds w+	where+	em = fromSDoc $ text "result: type checker: return False"+	et = ((EvExpr . Coercion) .) . mkUnivCo (PluginProv hd) Nominal
+ src/Plugin/TypeCheck/Nat/Simple/UnNomEq.hs view
@@ -0,0 +1,16 @@+{-# LANGUAGE OverloadedStrings #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Plugin.TypeCheck.Nat.Simple.UnNomEq (unNomEq) where++import TcRnTypes (Ct, ctEvidence, ctEvPred)+import Type (Type, PredTree(..), EqRel(..), classifyPredType)+import Outputable (ppr, text, (<+>))+import Control.Monad.Try (Try, throw)+import Data.Log (IsSDoc, fromSDoc)++unNomEq :: (Monoid w, IsSDoc e) => Ct -> Try e w (Type, Type)+unNomEq ct = case classifyPredType . ctEvPred $ ctEvidence ct of+	EqPred NomEq l r -> pure (l, r)+	_ -> throw . fromSDoc+		$ text "unNomEq: no match to EqPred NomEq l r:" <+> ppr ct
+ test/log.hs view
@@ -0,0 +1,12 @@+{-# LANGUAGE DataKinds, TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}++import GHC.TypeNats+import Data.Proxy++foo :: 1 <= n => Proxy (n - 1 + 1) -> Proxy (n + 1 - 1)+foo = id++main :: IO ()+main = putStrLn "test log"
+ test/spec.hs view
@@ -0,0 +1,12 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeApplications #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++import Data.Derivation.CanDerive+import Data.Derivation.Parse++import Control.Monad.Try++main :: IO ()+main = do+	print $ wanted @String @String =<< maybeToTry "parse error" (parseConstraint "0 == n - n")
+ test/tryLog.hs view
@@ -0,0 +1,23 @@+{-# LANGUAGE BlockArguments, OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++import Outputable+import Control.Monad.Try hiding (Message)+import Data.String+import Data.Log++main :: IO ()+main = do+	let	(r, l) = runTry do+			n <- 8 `devide` 3 :: Try (Log String Int) (Log String Int) Int+			(15 `devide` 0) `catch` \e -> tell e >> pure (n + 0)+	putStr $ message l+	putStrLn . showSDocUnsafe $ ppr l+	print r++devide :: forall s . (IsString s, Message s) => Int -> Int -> Try (Log s Int) (Log s Int) Int+m `devide` 0 = throw $ logVar m .+. " is devided by " .+. logVar 0+m `devide` n = do+	tell (logVar m .+. " is devided by " .+. logVar n :: Log s Int)+	pure $ m `div` n
+ typecheck-plugin-nat-simple.cabal view
@@ -0,0 +1,106 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.33.0.+--+-- see: https://github.com/sol/hpack+--+-- hash: 37e93024d7892b53d4f73b5eaf1a2fd50b85d7b7ccf19998c52119e2bfdee1b8++name:           typecheck-plugin-nat-simple+version:        0.1.0.0+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+homepage:       https://github.com/YoshikuniJujo/typecheck-plugin-nat-simple#readme+bug-reports:    https://github.com/YoshikuniJujo/typecheck-plugin-nat-simple/issues+author:         Yoshikuni Jujo+maintainer:     yoshikuni.jujo.pc@gmail.com+copyright:      Yoshikuni Jujo+license:        BSD3+license-file:   LICENSE+build-type:     Simple+extra-source-files:+    README.md+    ChangeLog.md+data-files:+    lengthed_tail.hs+    plus1minus1.hs+    two_equations.hs+    minus1plus1.hs+    complex.hs+    mplus1_nplus1.hs+data-dir:       sample++source-repository head+  type: git+  location: https://github.com/YoshikuniJujo/typecheck-plugin-nat-simple++library+  exposed-modules:+      Plugin.TypeCheck.Nat.Simple+      Plugin.TypeCheck.Nat.Simple.TypeCheckWith+      Plugin.TypeCheck.Nat.Simple.Decode+      Data.Derivation.CanDerive+      Data.Derivation.Expression+      Data.Derivation.Parse+      Control.Monad.Try+      Data.Log+  other-modules:+      Control.Monad.StateT+      Data.Derivation.Constraint+      Data.Derivation.Expression.Internal+      Data.Parse+      Plugin.TypeCheck.Nat.Simple.UnNomEq+      Paths_typecheck_plugin_nat_simple+  hs-source-dirs:+      src+  build-depends:+      base >=4.7 && <5+    , containers+    , ghc+  default-language: Haskell2010++test-suite typecheck-plugin-nat-simple-test-log+  type: exitcode-stdio-1.0+  main-is: log.hs+  other-modules:+      Paths_typecheck_plugin_nat_simple+  hs-source-dirs:+      test+  ghc-options: -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      base >=4.7 && <5+    , containers+    , ghc+    , typecheck-plugin-nat-simple+  default-language: Haskell2010++test-suite typecheck-plugin-nat-simple-test-spec+  type: exitcode-stdio-1.0+  main-is: spec.hs+  other-modules:+      Paths_typecheck_plugin_nat_simple+  hs-source-dirs:+      test+  ghc-options: -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      base >=4.7 && <5+    , containers+    , ghc+    , typecheck-plugin-nat-simple+  default-language: Haskell2010++test-suite typecheck-plugin-nat-simple-test-tryLog+  type: exitcode-stdio-1.0+  main-is: tryLog.hs+  other-modules:+      Paths_typecheck_plugin_nat_simple+  hs-source-dirs:+      test+  ghc-options: -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      base >=4.7 && <5+    , containers+    , ghc+    , typecheck-plugin-nat-simple+  default-language: Haskell2010