binder 0.1 → 0.2

raw patch · 6 files changed

+604/−105 lines, 6 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +7/−0
• binder.cabal +4/−3
• src/Data/Binder.hs +200/−50
• test/Binder1Spec.hs +19/−17
• test/Binder2Spec.hs +40/−35
• test/Binder3Spec.hs +334/−0

@@ -2,6 +2,13 @@  ## version 0 +### 0.2 -- 2023-10-06++* Add operations for list.+* Integrate mkFree function into Var and Binder.+* Now MkFree requires monadic instance.+* Binder requires Monad typeclass.+ ### 0.1 -- 2023-10-04  Initial release.

@@ -1,6 +1,6 @@ cabal-version:      3.0 name:               binder-version:            0.1+version:            0.2 synopsis:           Variable binding for abstract syntax tree description:     binder is purely functional implementation of Ocaml's@@ -29,11 +29,12 @@ source-repository this     type:     git     location: https://github.com/ijaketak/binder-    tag:      0.1+    tag:      0.2  common depends     build-depends:           containers < 0.8+        , lens < 5.3         , text < 2.2         , transformers < 0.7 @@ -48,7 +49,6 @@     -- other-extensions:     build-depends:           base < 4.19-        , lens < 5.3     hs-source-dirs:   src     default-language: Haskell2010 @@ -58,6 +58,7 @@     other-modules:           Binder1Spec         , Binder2Spec+        , Binder3Spec     -- other-extensions:     type:             exitcode-stdio-1.0     hs-source-dirs:   test

@@ -24,10 +24,10 @@ -- * Variable and Box   , Var   , Box-  , MkFree(..) -- ** Variable   , var'Key   , var'Name+  , var'mkFree   , var'Box   , nameOf   , boxVar@@ -45,9 +45,12 @@   , boxPair   , boxTriple   , boxT+  , boxList+  , boxJoin -- * Variable binding   , Binder   , binder'Name+  , binder'mkFree   , binder'Body   , subst   , buildBinder@@ -55,9 +58,32 @@   , unbind   , eqBinder   , boxBinder+  , bindApply+-- * List+-- * Variable list+  , VarList+  , varList'Keys+  , varList'Names+  , varList'Boxes+  , namesOf+  , boxVarList+  , newVarList+-- * Binder for list+  , BinderList+  , binderList'Names+  , binderList'Body+  , binderList'mkFree+  , binderList'Arity+  , substList+  , eqBinderList+  , bindList+  , unbindList+  , boxBinderList+  , bindListApply   ) where  import Control.Lens+import Control.Monad (join) import Data.Kind (Type) import qualified Data.Map.Lazy as M import Data.Maybe (fromJust)@@ -78,6 +104,7 @@   } data VarBody m a = VarBody   { _varBody'Name :: Text+  , _varBody'mkFree :: Var m a -> m a   , _varBody'Box :: Box m a   } -- | Representation of under-construction things@@ -86,23 +113,22 @@   = Box'Closed a   | Box'Env (EnvVar m) (Closure m a) --- | Typeclass for free variable constructor.-class MkFree m a where-  mkFree :: Var m a -> a--data AnyVar m = forall a. MkFree m a => AnyVar (Var m a)+data AnyVar m = forall a. AnyVar (Var m a) type EnvVar m = M.Map (Numbering m) (AnyVar m)-data AnyMkFree m = forall a. MkFree m a => AnyMkFree a-type EnvMkFree m = M.Map (Numbering m) (AnyMkFree m)-newtype Closure m a = Closure { unClosure :: (EnvMkFree m) -> a }+data AnyOne = forall a. AnyOne a+type EnvOne m = M.Map (Numbering m) AnyOne+newtype Closure m a = Closure { unClosure :: (EnvOne m) -> m a } -instance Functor (Closure m) where-  fmap f cla = Closure $ f . unClosure cla+instance Functor m => Functor (Closure m) where+  fmap f cla = Closure $ fmap f . unClosure cla -instance Applicative (Closure m) where-  pure a = Closure $ const a-  clf <*> cla = Closure $ \env -> unClosure clf env $ unClosure cla env+instance Applicative m => Applicative (Closure m) where+  pure a = Closure $ const $ pure a+  clf <*> cla = Closure $ \env -> unClosure clf env <*> unClosure cla env +closureJoin :: Monad m => Closure m (m a) -> Closure m a+closureJoin cl = Closure $ \env -> join $ unClosure cl env+ instance MonadNumbering m => Eq (Var m a) where   Var x _ == Var y _ = x == y @@ -115,6 +141,8 @@  var'Name :: Lens' (Var m a) Text var'Name = var'Body . varBody'Name+var'mkFree :: Lens' (Var m a) (Var m a -> m a)+var'mkFree = var'Body . varBody'mkFree var'Box :: Lens' (Var m a) (Box m a) var'Box = var'Body . varBody'Box @@ -134,15 +162,15 @@ boxVar x = x ^. var'Box  -- | Create a new variable with given name.-newVar :: forall m a. (MkFree m a, MonadNumbering m) => Text -> m (Var m a)-newVar name = do+newVar :: forall m a. MonadNumbering m => Text -> (Var m a -> m a) -> m (Var m a)+newVar name mkFree = do   i <- numbering   let x = let b = Box'Env                 (M.singleton i $ AnyVar x)                 (Closure $ \env ->-                  let f (AnyMkFree y) = unsafeCoerce y+                  let f (AnyOne y) = pure $ unsafeCoerce y                    in f $ fromJust $ M.lookup i env)-           in Var i $ VarBody name b+           in Var i $ VarBody name mkFree b   return x  @@ -157,31 +185,31 @@ occur v (Box'Env vs _) = M.member (v ^. var'Key) vs  -instance Functor (Box m) where+instance Functor m => Functor (Box m) where   fmap f (Box'Closed a) = Box'Closed (f a)   fmap f (Box'Env vs ta) = Box'Env vs (f <$> ta) -instance (MonadNumbering m) => Applicative (Box m) where+instance MonadNumbering m => Applicative (Box m) where   pure = Box'Closed   Box'Closed f <*> Box'Closed a = Box'Closed (f a)   Box'Closed f <*> Box'Env va ta = Box'Env va (f <$> ta)   Box'Env vf tf <*> Box'Closed a = Box'Env vf (appClosure tf a)    where-    appClosure clf x = Closure $ \env -> unClosure clf env x+    appClosure clf x = Closure $ \env -> unClosure clf env <*> pure x   Box'Env vf tf <*> Box'Env va ta = Box'Env (M.union vf va) (tf <*> ta)  -- | Pick out and complete the construction of @a@.-unbox :: forall m a. Box m a -> a-unbox (Box'Closed t) = t-unbox (Box'Env env cl) = unClosure cl $ f <$> env+unbox :: forall m a. Monad m => Box m a -> m a+unbox (Box'Closed t) = pure t+unbox (Box'Env env cl) = unClosure cl =<< traverse f env  where-  f (AnyVar x) = AnyMkFree @m $ mkFree x+  f (AnyVar x) = fmap AnyOne $ x ^. var'mkFree $ x  box :: MonadNumbering m => a -> Box m a box = pure apBox :: MonadNumbering m => Box m (a -> b) -> Box m a -> Box m b apBox = (<*>)-boxApply :: (a -> b) -> Box m a -> Box m b+boxApply :: Functor m => (a -> b) -> Box m a -> Box m b boxApply = fmap boxApply2 :: MonadNumbering m => (a -> b -> c) -> Box m a -> Box m b -> Box m c boxApply2 f ta tb = f <$> ta <*> tb@@ -195,61 +223,183 @@ boxTriple = boxApply3 (,,) boxT :: (MonadNumbering m, Traversable t) => t (Box m a) -> Box m (t a) boxT = sequenceA+boxList :: MonadNumbering m => [Box m a] -> Box m [a]+boxList = sequenceA+boxJoin :: MonadNumbering m => Box m (m a) -> m (Box m a)+boxJoin (Box'Closed ma) = return . Box'Closed =<< ma+boxJoin (Box'Env env cl) = return $ Box'Env env $ closureJoin cl   -- | Variable binding.---   Essentially, @Binder a b@ means @a -> b@.-data Binder a b = Binder+--   Essentially, @Binder a m b@ means @a -> m b@.+data Binder a m b = Binder   { _binder'Name :: Text-  , _binder'Body :: a -> b+  , _binder'mkFree :: Var m a -> m a+  , _binder'Body :: a -> m b   }  $(makeLenses ''Binder)  -- | Variable substitution.-subst :: Binder a b -> a -> b+subst :: Binder a m b -> a -> m b subst b = b ^. binder'Body  -- | unbinding-unbind :: (MkFree m a, MonadNumbering m) => Binder a b -> m (Var m a, b)+unbind :: MonadNumbering m => Binder a m b -> m (Var m a, b) unbind b = do-  x <- newVar $ b ^. binder'Name-  return (x, subst b $ mkFree x)+  let mkFree = b ^. binder'mkFree+  x <- newVar (b ^. binder'Name) mkFree+  y <- subst b =<< mkFree x+  return (x, y) -unbind2 :: (MkFree m a, MonadNumbering m)-        => Binder a b1 -> Binder a b2 -> m (Var m a, b1, b2)+unbind2 :: MonadNumbering m+        => Binder a m b1 -> Binder a m b2 -> m (Var m a, b1, b2) unbind2 b1 b2 = do-  x <- newVar $ b1 ^. binder'Name-  let v = mkFree x-  return (x, subst b1 v, subst b2 v)+  let mkFree = b1 ^. binder'mkFree+  x <- newVar (b1 ^. binder'Name) mkFree+  v <- mkFree x+  y1 <- subst b1 v+  y2 <- subst b2 v+  return (x, y1, y2)  -- | Check if two bindings are equal.-eqBinder :: (MkFree m a, MonadNumbering m)-         => (b -> b -> m Bool) -> Binder a b -> Binder a b -> m Bool+eqBinder :: MonadNumbering m+         => (b -> b -> m Bool) -> Binder a m b -> Binder a m b -> m Bool eqBinder eq f g = do   (_, t, u) <- unbind2 f g   eq t u   -- | Smart constructor for 'Binder'.-buildBinder :: Var m a -> (a -> b) -> Binder a b-buildBinder x body = Binder (x ^. var'Name) body+buildBinder :: Var m a -> (a -> m b) -> Binder a m b+buildBinder x body = Binder (x ^. var'Name) (x ^. var'mkFree) body  -- | binding-bind :: (MkFree m a, MonadNumbering m)-        => Var m a -> Box m b -> Box m (Binder a b)-bind x (Box'Closed t) = Box'Closed $ buildBinder x $ const t+bind :: MonadNumbering m => Var m a -> Box m b -> Box m (Binder a m b)+bind x (Box'Closed t) = Box'Closed $ buildBinder x $ const $ return t bind x (Box'Env vs t) =   let vs' = M.delete (x ^. var'Key) vs in if length vs' == 0     then Box'Closed $ buildBinder x $-      \arg -> unClosure t $ M.singleton (x ^. var'Key) (AnyMkFree arg)+      \arg -> unClosure t $ M.singleton (x ^. var'Key) (AnyOne arg)     else Box'Env vs' $ Closure $-      \ms -> buildBinder x $-      \arg -> unClosure t $ M.insert (x ^. var'Key) (AnyMkFree arg) ms+      \ms -> return $ buildBinder x $+      \arg -> unClosure t $ M.insert (x ^. var'Key) (AnyOne arg) ms -boxBinder :: (MkFree m a, MonadNumbering m)-          => (b -> m (Box m b)) -> Binder a b -> m (Box m (Binder a b))+boxBinder :: MonadNumbering m+          => (b -> m (Box m b)) -> Binder a m b -> m (Box m (Binder a m b)) boxBinder f b = do   (x, t) <- unbind b   ft <- f t   return $ bind x ft++bindApply :: MonadNumbering m => Box m (Binder a m b) -> Box m a -> m (Box m b)+bindApply b arg = boxJoin $ subst <$> b <*> arg+++type VarList m a = [Var m a]++varList'Keys :: Getter (VarList m a) [Numbering m]+varList'Keys = to $ fmap $ view var'Key+varList'Names :: Getter (VarList m a) [Text]+varList'Names = to $ fmap $ view var'Name+varList'Boxes :: Getter (VarList m a) [Box m a]+varList'Boxes = to $ fmap $ view var'Box++-- | The names of variables.+namesOf :: VarList m a -> [Text]+namesOf = fmap $ view var'Name++-- | Smart constructor for a list of 'Box'.+boxVarList :: VarList m a -> [Box m a]+boxVarList = fmap $ view var'Box++-- | Create new variables with given names.+newVarList :: MonadNumbering m => [Text] -> (Var m a -> m a) -> m (VarList m a)+newVarList names mkFree = sequence $ flip fmap names $ \name -> newVar name mkFree+++-- | Essentially, @BinderList a m b@ means @[a] -> m b@.+data BinderList a m b = BinderList+  { _binderList'Names :: [Text]+  , _binderList'mkFree :: Var m a -> m a+  , _binderList'Body :: [a] -> m b+  }++$(makeLenses ''BinderList)++binderList'Arity :: Getter (BinderList a m b) Int+binderList'Arity = binderList'Names . to length++-- | Variable substitution.+substList :: BinderList a m b -> [a] -> m b+substList ba = ba ^. binderList'Body++-- | unbinding+unbindList :: MonadNumbering m => BinderList a m b -> m (VarList m a, b)+unbindList ba = do+  let mkFree = ba ^. binderList'mkFree+  xs <- newVarList (ba ^. binderList'Names) mkFree+  y <- substList ba =<< traverse mkFree xs+  return (xs, y)++unbind2List :: MonadNumbering m+             => BinderList a m b1 -> BinderList a m b2+             -> m (VarList m a, b1, b2)+unbind2List ba1 ba2 = do+  let mkFree = ba1 ^. binderList'mkFree+  xs <- newVarList (ba1 ^. binderList'Names) mkFree+  vs <- traverse mkFree xs+  y1 <- substList ba1 vs+  y2 <- substList ba2 vs+  return (xs, y1, y2)++-- | Check if two bindings are equal.+eqBinderList :: MonadNumbering m+              => (b -> b -> m Bool)+              -> BinderList a m b -> BinderList a m b -> m Bool+eqBinderList eq f g =+  if f ^. binderList'Arity /= g ^. binderList'Arity+    then return False+    else do+      (_, t, u) <- unbind2List f g+      eq t u++-- | Smart constructor for 'BinderList.+buildBinderList :: VarList m a -> ([a] -> m b) -> BinderList a m b+buildBinderList xs body =+  BinderList (xs ^. varList'Names) (head xs ^. var'mkFree) body++deleteList :: Ord k => [k] -> M.Map k a -> M.Map k a+deleteList = flip $ foldl $ \m k -> M.delete k m+insertList :: Ord k => [k] -> [a] -> M.Map k a -> M.Map k a+insertList ks xs m = foldl f m $ zip ks xs+ where+  f n (k, x) = M.insert k x n+zipList :: Ord k => [k] -> [a] -> M.Map k a+zipList ks xs = insertList ks xs M.empty++-- | binding+bindList :: MonadNumbering m+          => VarList m a -> Box m b -> Box m (BinderList a m b)+bindList xs (Box'Closed t) = Box'Closed $ buildBinderList xs $ const $ return t+bindList xs (Box'Env vs t) =+  let vs' = deleteList (xs ^. varList'Keys) vs in if length vs' == 0+    then Box'Closed $ buildBinderList xs $+      \args -> unClosure t $+      zipList (xs ^. varList'Keys) (AnyOne <$> args)+    else Box'Env vs' $ Closure $+      \ms -> return $ buildBinderList xs $+      \args -> unClosure t $+      insertList (xs ^. varList'Keys) (AnyOne <$> args) ms++boxBinderList :: MonadNumbering m+               => (b -> m (Box m b)) -> BinderList a m b+               -> m (Box m (BinderList a m b))+boxBinderList f b = do+  (xs, t) <- unbindList b+  ft <- f t+  return $ bindList xs ft++bindListApply :: MonadNumbering m+              => Box m (BinderList a m b) -> Box m [a] -> m (Box m b)+bindListApply b args = boxJoin $ substList <$> b <*> args

@@ -37,15 +37,15 @@  data Term   = Term'Var (Var S Term)-  | Term'Abs (Binder Term Term)+  | Term'Abs (Binder Term S Term)   | Term'App Term Term -instance MkFree S Term where-  mkFree = Term'Var+term'mkFree :: Var S Term -> S Term+term'mkFree = return . Term'Var  var :: Var S Term -> Box S Term var = boxVar-absRaw :: Box S (Binder Term Term) -> Box S Term+absRaw :: Box S (Binder Term S Term) -> Box S Term absRaw = fmap Term'Abs abs :: Var S Term -> Box S Term -> Box S Term abs x t = absRaw $ bind x t@@ -56,11 +56,13 @@ boxTerm (Term'Abs b) = absRaw <$> boxBinder boxTerm b boxTerm (Term'App t u) = app <$> boxTerm t <*> boxTerm u -eval :: Term -> Term-eval t@(Term'App f a) = case eval f of-  Term'Abs b -> eval (subst b a)-  _ -> t-eval t = t+eval :: Term -> S Term+eval t@(Term'App f a) = do+  ef <- eval f+  case ef of+    Term'Abs b -> eval =<< subst b a+    _ -> return t+eval t = return t  size :: Term -> S Int size (Term'Var _) = return 0@@ -86,18 +88,18 @@  termIdentity, termFst, termDelta, termOmega :: S Term termIdentity = do-  x <- newVar "x"-  return $ unbox $ abs x $ var x+  x <- newVar "x" term'mkFree+  unbox $ abs x $ var x termFst = do-  x <- newVar "x"-  y <- newVar "y"-  return $ unbox $ abs x $ abs y $ var x+  x <- newVar "x" term'mkFree+  y <- newVar "y" term'mkFree+  unbox $ abs x $ abs y $ var x termDelta = do-  x <- newVar "x"-  return $ unbox $ abs x $ app (var x) (var x)+  x <- newVar "x" term'mkFree+  unbox $ abs x $ app (var x) (var x) termOmega = do   delta <- box <$> termDelta-  return $ unbox $ app delta delta+  unbox $ app delta delta  spec :: Spec spec = do

@@ -39,38 +39,38 @@ data Ty   = Ty'Var (Var S Ty)   | Ty'Arr Ty Ty-  | Ty'All (Binder Ty Ty)+  | Ty'All (Binder Ty S Ty)  data Te   = Te'Var (Var S Te)-  | Te'Abs Ty (Binder Te Te)+  | Te'Abs Ty (Binder Te S Te)   | Te'App Te Te-  | Te'Lam (Binder Ty Te)+  | Te'Lam (Binder Ty S Te)   | Te'Spe Te Ty -instance MkFree S Ty where-  mkFree = Ty'Var-instance MkFree S Te where-  mkFree = Te'Var+ty'mkFree :: Var S Ty -> S Ty+ty'mkFree = return . Ty'Var+te'mkFree :: Var S Te -> S Te+te'mkFree = return . Te'Var  ty'Var :: Var S Ty -> Box S Ty ty'Var = boxVar ty'Arr :: Box S Ty -> Box S Ty -> Box S Ty ty'Arr a b = Ty'Arr <$> a <*> b-ty'AllRaw :: Box S (Binder Ty Ty) -> Box S Ty+ty'AllRaw :: Box S (Binder Ty S Ty) -> Box S Ty ty'AllRaw = fmap Ty'All ty'All :: Var S Ty -> Box S Ty -> Box S Ty ty'All x t = ty'AllRaw $ bind x t  te'Var :: Var S Te -> Box S Te te'Var = boxVar-te'AbsRaw :: Box S Ty -> Box S (Binder Te Te) -> Box S Te+te'AbsRaw :: Box S Ty -> Box S (Binder Te S Te) -> Box S Te te'AbsRaw a f = Te'Abs <$> a <*> f te'Abs :: Box S Ty -> Var S Te -> Box S Te -> Box S Te te'Abs a x t = te'AbsRaw a $ bind x t te'App :: Box S Te -> Box S Te -> Box S Te te'App t u = Te'App <$> t <*> u-te'LamRaw :: Box S (Binder Ty Te) -> Box S Te+te'LamRaw :: Box S (Binder Ty S Te) -> Box S Te te'LamRaw = fmap Te'Lam te'Lam :: Var S Ty -> Box S Te -> Box S Te te'Lam x t = te'LamRaw $ bind x t@@ -88,36 +88,41 @@ boxTe (Te'Lam f) = te'LamRaw <$> boxBinder boxTe f boxTe (Te'Spe t a) = te'Spe <$> boxTe t <*> boxTy a -hnf :: Te -> Te-hnf (Te'App t u) = let v = hnf u in case hnf t of-  Te'Abs _ b -> hnf $ subst b v-  h -> Te'App h v-hnf (Te'Spe t a) = case hnf t of-  Te'Lam b -> hnf $ subst b a-  h -> Te'Spe h a-hnf t = t+hnf :: Te -> S Te+hnf (Te'App t u) = do+  hu <- hnf u+  ht <- hnf t+  case ht of+    Te'Abs _ b -> hnf =<< subst b hu+    _ -> return $ Te'App ht hu+hnf (Te'Spe t a) = do+  ht <- hnf t+  case ht of+    Te'Lam b -> hnf =<< subst b a+    _ -> return $ Te'Spe ht a+hnf t = return t  nf :: Te -> S Te nf (Te'Abs a f) = do   (x, t) <- unbind f   nt <- nf t   bt <- boxTe nt-  return $ Te'Abs a $ unbox $ bind x bt+  fmap (Te'Abs a) $ unbox $ bind x bt nf (Te'App t u) = do   nt <- nf t   nu <- nf u   case nt of-    Te'Abs _ f -> nf $ subst f u+    Te'Abs _ f -> nf =<< subst f u     _ -> return $ Te'App nt nu nf (Te'Lam f) = do   (x, t) <- unbind f   nt <- nf t   bt <- boxTe nt-  return $ Te'Lam $ unbox $ bind x bt+  fmap Te'Lam $ unbox $ bind x bt nf (Te'Spe t a) = do   nt <- nf t   case nt of-    Te'Lam f -> nf $ subst f a+    Te'Lam f -> nf =<< subst f a     _ -> return $ Te'Spe nt a nf t = return t @@ -155,12 +160,12 @@   case mtyt of     Just tyt -> do       bt <- boxTy tyt-      return $ Just $ Ty'All $ unbox $ bind x bt+      fmap (Just . Ty'All) $ unbox $ bind x bt     Nothing -> return Nothing infer ctxt (Te'Spe t a) = do   mtyt <- infer ctxt t   case mtyt of-    Just (Ty'All f) -> return $ Just $ subst f a+    Just (Ty'All f) -> Just <$> subst f a     _ -> return Nothing  check :: Ctxt -> Te -> Ty -> S Bool@@ -204,21 +209,21 @@ type1, type2 :: S Ty term1 :: S Te type1 = do-  x <- newVar "X"-  y <- newVar "Y"-  return $ unbox $ ty'Arr (ty'Var x) (ty'Var y)+  x <- newVar "X" ty'mkFree+  y <- newVar "Y" ty'mkFree+  unbox $ ty'Arr (ty'Var x) (ty'Var y) type2 = do-  x <- newVar "X"-  y <- newVar "Y"+  x <- newVar "X" ty'mkFree+  y <- newVar "Y" ty'mkFree   let arr = ty'Arr (ty'Var x) (ty'Var y)-  return $ unbox $ ty'All x $ ty'All y $ ty'Arr arr arr+  unbox $ ty'All x $ ty'All y $ ty'Arr arr arr term1 = do-  x <- newVar "X"-  y <- newVar "Y"-  f <- newVar "f"-  a <- newVar "a"+  x <- newVar "X" ty'mkFree+  y <- newVar "Y" ty'mkFree+  f <- newVar "f" te'mkFree+  a <- newVar "a" te'mkFree   let arr = ty'Arr (ty'Var x) (ty'Var y)-  return $ unbox $ te'Lam x $ te'Lam y $ te'Abs arr f $ te'Abs (ty'Var x) a $+  unbox $ te'Lam x $ te'Lam y $ te'Abs arr f $ te'Abs (ty'Var x) a $     te'App (te'Var f) (te'Var a)  spec :: Spec

@@ -0,0 +1,334 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}++module Binder3Spec where++import Control.Lens+import Control.Monad ((<=<))+import Control.Monad.IO.Class (MonadIO)+import Control.Monad.Trans.State.Strict (evalStateT, get, modify, StateT)+import Data.List (intersperse)+-- import qualified Data.Map.Lazy as M+import Data.Text (Text)+import qualified Data.Text as T (pack)+import GHC.Generics hiding (S, to)+import Test.Hspec++import Data.Binder++newtype S a = S { runS :: StateT Int IO a }+  deriving+  ( Generic+  , Generic1+  , Functor+  , Applicative+  , Monad+  , MonadIO+  )++instance MonadNumbering S where+  type Numbering S = Int+  numbering = do+    i <- S $ get+    S $ modify succ+    return i++-- This example is stolen from one example of bindlib.+-- https://github.com/rlepigre/ocaml-bindlib/blob/master/examples/pred2.ml++data Symbol = Symbol Text Int+  deriving (Eq, Show)++data Term+  = Term'Var (Var S Term)+  | Term'Fun Symbol [Term]++data Form+  = Form'Imply Form Form+  | Form'Univ1 (Binder Term S Form)+  | Form'Univ2 Int (Binder Pred S Form)+  | Form'FVari (Var S Pred) [Term]++newtype Pred = Pred { unPred :: BinderList Term S Form }++data Proof+  = Proof'ImplyI Form (Binder Proof S Proof)+  | Proof'ImplyE Proof Proof+  | Proof'Univ1I (Binder Term S Proof)+  | Proof'Univ1E Proof Term+  | Proof'Univ2I Int (Binder Pred S Proof)+  | Proof'Univ2E Proof Pred+  | Proof'Axiom Form (Var S Proof)++pred'Arity :: Getter Pred Int+pred'Arity = to unPred . binderList'Arity+pred'makeRaw :: Box S (BinderList Term S Form) -> Box S Pred+pred'makeRaw = fmap Pred+pred'make :: VarList S Term -> Box S Form -> Box S Pred+pred'make xs t = pred'makeRaw $ bindList xs t++term'mkFree :: Var S Term -> S Term+term'mkFree = return . Term'Var+pred'mkFree :: Int -> Var S Pred -> S Pred+pred'mkFree n vp = do+  let names = if n == 1 then ["x"]+                        else flip map [1..n] $ \i -> "x" <> T.pack (show i)+  xs <- newVarList names term'mkFree+  let ts = boxList $ map term'Var xs+      p = Form'FVari vp <$> ts+  fmap Pred $ unbox $ bindList xs p+proof'mkFree :: Form -> Var S Proof -> S Proof+proof'mkFree f = return . Proof'Axiom f++term'Var :: Var S Term -> Box S Term+term'Var = boxVar+term'Fun :: Symbol -> [Box S Term] -> Box S Term+term'Fun s ts = Term'Fun s <$> boxList ts+form'Imply :: Box S Form -> Box S Form -> Box S Form+form'Imply f g = Form'Imply <$> f <*> g+form'Univ1Raw :: Box S (Binder Term S Form) -> Box S Form+form'Univ1Raw = fmap Form'Univ1+form'Univ1 :: Var S Term -> Box S Form -> Box S Form+form'Univ1 x t = form'Univ1Raw $ bind x t+form'Univ2Raw :: Int -> Box S (Binder Pred S Form) -> Box S Form+form'Univ2Raw arity = fmap $ Form'Univ2 arity+form'Univ2 :: Int -> Var S Pred -> Box S Form -> Box S Form+form'Univ2 arity x t = form'Univ2Raw arity $ bind x t+form'FVari :: Var S Pred -> [Box S Term] -> Box S Form+form'FVari x ts = Form'FVari x <$> boxList ts+proof'ImplyIRaw :: Box S Form -> Box S (Binder Proof S Proof) -> Box S Proof+proof'ImplyIRaw p b = Proof'ImplyI <$> p <*> b+proof'ImplyI :: Box S Form -> Var S Proof -> Box S Proof -> Box S Proof+proof'ImplyI p x t = proof'ImplyIRaw p $ bind x t+proof'ImplyE :: Box S Proof -> Box S Proof -> Box S Proof+proof'ImplyE p q = Proof'ImplyE <$> p <*> q+proof'Univ1IRaw :: Box S (Binder Term S Proof) -> Box S Proof+proof'Univ1IRaw = fmap Proof'Univ1I+proof'Univ1I :: Var S Term -> Box S Proof -> Box S Proof+proof'Univ1I x t = proof'Univ1IRaw $ bind x t+proof'Univ1E :: Box S Proof -> Box S Term -> Box S Proof+proof'Univ1E p q = Proof'Univ1E <$> p <*> q+proof'Univ2IRaw :: Int -> Box S (Binder Pred S Proof) -> Box S Proof+proof'Univ2IRaw arity = fmap $ Proof'Univ2I arity+proof'Univ2I :: Int -> Var S Pred -> Box S Proof -> Box S Proof+proof'Univ2I arity x t = proof'Univ2IRaw arity $ bind x t+proof'Univ2E :: Box S Proof -> Box S Pred -> Box S Proof+proof'Univ2E p q = Proof'Univ2E <$> p <*> q+proof'Axiom :: Box S Form -> Var S Proof -> Box S Proof+proof'Axiom f v = (\g -> Proof'Axiom g v) <$> f++boxTerm :: Term -> S (Box S Term)+boxTerm (Term'Var x) = return $ term'Var x+boxTerm (Term'Fun s ts) = fmap (term'Fun s) $ sequenceA $ boxTerm <$> ts+boxForm :: Form -> S (Box S Form)+boxForm (Form'Imply a b) = form'Imply <$> boxForm a <*> boxForm b+boxForm (Form'Univ1 b) = form'Univ1Raw <$> boxBinder boxForm b+boxForm (Form'Univ2 a b) = form'Univ2Raw a <$> boxBinder boxForm b+boxForm (Form'FVari x ts) = do+  let arg1 = unPred <$> boxVar x+  arg2 <- fmap boxList $ sequenceA $ boxTerm <$> ts+  boxJoin $ substList <$> arg1 <*> arg2++showTerm :: Term -> Text+showTerm (Term'Var x) = nameOf x+showTerm (Term'Fun (Symbol s _) ts) =+  s <> "(" <> mconcat (intersperse ", " $ map showTerm ts) <> ")"+showForm :: Form -> S Text+showForm (Form'Imply a b) = do+  sha <- showForm a+  shb <- showForm b+  return $ "(" <> sha <> ") => (" <> shb <> ")"+showForm (Form'Univ1 b) = do+  (x, t) <- unbind b+  sht <- showForm t+  return $ "forall_1 " <> nameOf x <> ".(" <> sht <> ")"+showForm (Form'Univ2 _ b) = do+  (x, t) <- unbind b+  sht <- showForm t+  return $ "forall_2 " <> nameOf x <> ".(" <> sht <> ")"+showForm (Form'FVari x ts) = do+  return $ nameOf x <> "(" <> mconcat (intersperse ", " $ map showTerm ts) <> ")"++eqTerm :: Term -> Term -> Bool+eqTerm (Term'Var x) (Term'Var y) = x == y+eqTerm (Term'Fun s1 ts1) (Term'Fun s2 ts2) =+  s1 == s2 && and (map (uncurry eqTerm) $ zip ts1 ts2)+eqTerm _ _ = False+eqForm :: Form -> Form -> S Bool+eqForm (Form'Imply a1 b1) (Form'Imply a2 b2) = do+  ca <- eqForm a1 a2+  cb <- eqForm b1 b2+  return $ ca && cb+eqForm (Form'Univ1 b1) (Form'Univ1 b2) = eqBinder eqForm b1 b2+eqForm (Form'Univ2 a1 b1) (Form'Univ2 a2 b2) = do+  c <- eqBinder eqForm b1 b2+  return $ a1 == a2 && c+eqForm (Form'FVari x1 ts1) (Form'FVari x2 ts2) =+  return $ x1 == x2 && and (map (uncurry eqTerm) $ zip ts1 ts2)+eqForm _ _ = return False++data BadProof+  = BadProof'Imply+  | BadProof'ImplyDifferForm Form Form+  | BadProof'Univ1+  | BadProof'Univ2++showBadProof :: BadProof -> S Text+showBadProof BadProof'Imply = return "BadProof'Imply"+showBadProof (BadProof'ImplyDifferForm a b) = do+  sha <- showForm a+  shb <- showForm b+  return $ "BadProof'ImplyDifferForm (" <> sha <> ") (" <> shb <> ")"+showBadProof BadProof'Univ1 = return "BadProof'Univ1"+showBadProof BadProof'Univ2 = return "BadProof'Univ2"++typeInfer :: Proof -> S (Either BadProof Form)+typeInfer = unbox <=< fn+ where+  fn :: Proof -> S (Box S (Either BadProof Form))+  fn (Proof'ImplyI f p) = do+    ax <- newVar (p ^. binder'Name) $ proof'mkFree f+    tax <- proof'mkFree f ax+    pr <- subst p tax+    ber <- fn pr+    er <- unbox ber+    case er of+      Right r -> do+        bf <- boxForm f+        br <- boxForm r+        return $ Right <$> form'Imply bf br+      Left err -> return $ pure $ Left err+  fn (Proof'ImplyE p1 p2) = do+    mf1' <- unbox =<< fn p2+    mf2' <- unbox =<< fn p1+    case (mf1', mf2') of+      (Right f1', Right (Form'Imply f1 f2)) -> do+        b <- eqForm f1 f1'+        if b then fmap Right <$> boxForm f2+             else return $ pure $ Left $ BadProof'ImplyDifferForm f1 f1'+      _ -> return $ pure $ Left BadProof'Imply+  fn (Proof'Univ1I p) = do+    t <- newVar (p ^. binder'Name) term'mkFree+    te <- term'mkFree t+    pr <- subst p te+    ef <- unbox =<< fn pr+    case ef of+      Right f -> do+        bf <- boxForm f+        return $ Right <$> form'Univ1 t bf+      Left err -> return $ pure $ Left err+  fn (Proof'Univ1E p t) = do+    mf <- unbox =<< fn p+    case mf of+      Right (Form'Univ1 b) -> do+        f <- subst b t+        fmap Right <$> boxForm f+      Right _ -> return $ pure $ Left BadProof'Univ1+      Left err -> return $ pure $ Left err+  fn (Proof'Univ2I arity f) = do+    t <- newVar (f ^. binder'Name) $ pred'mkFree arity+    pr <- pred'mkFree arity t+    eg <- unbox =<< fn =<< subst f pr+    case eg of+      Right g -> do+        bg <- boxForm g+        return $ fmap Right $ form'Univ2 arity t bg+      Left err -> return $ pure $ Left err+  fn (Proof'Univ2E p p0) = do+    mf <- unbox =<< fn p+    case mf of+      Right (Form'Univ2 arity b) -> if arity == p0 ^. pred'Arity+        then do+          f <- subst b p0+          fmap Right <$> boxForm f+        else return $ pure $ Left BadProof'Univ2+      Right _ -> return $ pure $ Left BadProof'Univ2+      Left err -> return $ pure $ Left err+  fn (Proof'Axiom f _) = fmap Right <$> boxForm f++typeCheck :: Proof -> Form -> S Bool+typeCheck p f0 = do+  ef <- typeInfer p+  case ef of+    Right f -> eqForm f0 f+    _ -> return False+++leq :: S (Box S Pred)+leq = do+  u <- newVar "u" term'mkFree+  v <- newVar "v" term'mkFree+  let bu = term'Var u+      bv = term'Var v+  x <- newVar "X" $ pred'mkFree 1+  let bl = unPred <$> boxVar x+  p1 <- bindListApply bl $ boxList [bu]+  p2 <- bindListApply bl $ boxList [bv]+  return $ fmap Pred $ bindList [u, v] $ form'Univ2 1 x $ form'Imply p1 p2++equalTransitive :: S Form+equalTransitive = do+  q <- leq+  x <- newVar "x" term'mkFree+  y <- newVar "y" term'mkFree+  z <- newVar "z" term'mkFree+  let bx = term'Var x+      by = term'Var y+      bz = term'Var z+      bl = fmap unPred q+  p1 <- bindListApply bl $ boxList [bx, by]+  p2 <- bindListApply bl $ boxList [by, bz]+  p3 <- bindListApply bl $ boxList [bx, bz]+  unbox $ form'Univ1 x $ form'Univ1 y $ form'Univ1 z $+    form'Imply p1 $ form'Imply p2 p3++equalTransitiveProof :: S Proof+equalTransitiveProof = do+  q <- leq+  x <- newVar "x" term'mkFree+  y <- newVar "y" term'mkFree+  z <- newVar "z" term'mkFree+  let bx = term'Var x+      by = term'Var y+      bz = term'Var z+      bl = fmap unPred q+  f <- bindListApply bl $ boxList [bx, by]+  uf <- unbox f+  h1 <- newVar "h1" $ proof'mkFree uf+  g <- bindListApply bl $ boxList [by, bz]+  ug <- unbox g+  h2 <- newVar "h2" $ proof'mkFree ug+  px <- newVar "X" $ pred'mkFree 1+  p <- bindListApply (unPred <$> boxVar px) $ boxList [bx]+  up <- unbox p+  h3 <- newVar "h3" $ proof'mkFree up+  unbox $ proof'Univ1I x $ proof'Univ1I y $ proof'Univ1I z $+    proof'ImplyI f h1 $ proof'ImplyI g h2 $+    proof'Univ2I 1 px $ proof'ImplyI p h3 $+    proof'ImplyE (proof'Univ2E (boxVar h2) (boxVar px)) $+    proof'ImplyE (proof'Univ2E (boxVar h1) (boxVar px)) (boxVar h3)++spec :: Spec+spec = describe "leq" $ do+  it "forms correctly" $ do+    let r = "forall_1 x.(forall_1 y.(forall_1 z.((forall_2 X.((X(x)) => (X(y)))) => ((forall_2 X.((X(y)) => (X(z)))) => (forall_2 X.((X(x)) => (X(z))))))))"+    flip shouldReturn r $ flip evalStateT 0 $ runS $ do+      f <- equalTransitive+      showForm f+  it "infers type soundly" $ do+    let r = "forall_1 x.(forall_1 y.(forall_1 z.((forall_2 X.((X(x)) => (X(y)))) => ((forall_2 X.((X(y)) => (X(z)))) => (forall_2 X.((X(x)) => (X(z))))))))"+    flip shouldReturn r $ flip evalStateT 0 $ runS $ do+      ef <- typeInfer =<< equalTransitiveProof+      case ef of+        Right f -> showForm f+        Left bp -> showBadProof bp+  it "checks correctly" $ do+    let r = True+    flip shouldReturn r $ flip evalStateT 0 $ runS $ do+      p <- equalTransitiveProof+      f <- equalTransitive+      typeCheck p f