Rename from props to propa-tools

src/Propa/Lambda/Display.hs

@@ -0,0 +1,127 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+-- | This module contains functions useful for displaying 'Term's.
+
+module Propa.Lambda.Display
+  ( Name
+  , findConstNames
+  , makeVarNamesUnique
+  , findVarNames
+  , displayTerm
+  , displayTerm'
+  ) where
+
+import           Data.Maybe
+import           Numeric.Natural
+
+import           Control.Monad.Trans.State
+import qualified Data.Set                  as Set
+import qualified Data.Text                 as T
+
+import           Propa.Lambda.Term
+
+-- | The name of a variable or a constant.
+type Name = T.Text
+
+varNames :: [Name]
+varNames = chars ++ (mappend <$> constNames <*> chars)
+  where
+    chars = map T.singleton ['a'..'z']
+
+constNames :: [Name]
+constNames = chars ++ (mappend <$> constNames <*> chars)
+  where
+    chars = map T.singleton ['A'..'Z']
+
+chooseUnique :: (Ord a) => Set.Set a -> [a] -> a
+chooseUnique taken = head . dropWhile (`Set.member` taken)
+
+makeNameUnique :: Set.Set Name -> Name -> Name
+makeNameUnique taken name
+  = chooseUnique taken
+  $ zipWith (<>) (repeat name)
+  $ "" : map (T.pack . show) [(2::Integer) ..]
+
+-- | Find names for constants that don't overlap with existing constants. Every
+-- unnamed constant is assumed to be a different constant. This means that every
+-- unnamed constant will be assigned a unique name.
+--
+-- Names for constants follow the schema @A@, @B@, ... @AA@, @AB@, ...
+findConstNames :: Term e (Maybe Name) v -> Term e Name v
+findConstNames term = evalState (helper term) (Set.fromList $ catMaybes $ consts term)
+  where
+    helper (Var i) = pure $ Var i
+    helper (Const c) = do
+      taken <- get
+      let name = fromMaybe (chooseUnique taken constNames) c
+      put $ Set.insert name taken
+      pure $ Const name
+    helper (Lambda v t) = Lambda v <$> helper t
+    helper (App l r) = App <$> helper l <*> helper r
+    helper (Ext e) = pure $ Ext e
+
+-- | Make names of existing variables unique. If the name is not already unique
+-- in the current scope, tries to make it unique by appending a number from
+-- @[2..]@.
+makeVarNamesUnique :: Term e Name (Maybe Name) -> Term e Name (Maybe Name)
+makeVarNamesUnique term = helper (Set.fromList $ consts term) term
+  where
+    helper _     (Var i) = Var i
+    helper _     (Const c) = Const c
+    helper taken (Lambda v t) = case v of
+      Nothing -> Lambda Nothing $ helper taken t
+      Just name ->
+        let newName = makeNameUnique taken name
+        in  Lambda (Just newName) $ helper (Set.insert name taken) t
+    helper taken (App l r) = App (helper taken l) (helper taken r)
+    helper _     (Ext e) = Ext e
+
+-- | Find names for unnamed variables that are unique in the current scope.
+--
+-- Names for variables follow the schema @a@, @b@, ..., @aa@, @ab@, ...
+findVarNames :: Term e Name (Maybe Name) -> Term e Name Name
+findVarNames term = helper (Set.fromList $ consts term) term
+  where
+    helper _     (Var i) = Var i
+    helper _     (Const c) = Const c
+    helper taken (Lambda v t) =
+      let name = fromMaybe (chooseUnique taken varNames) v
+      in  Lambda name $ helper (Set.insert name taken) t
+    helper taken (App l r) = App (helper taken l) (helper taken r)
+    helper _     (Ext e) = Ext e
+
+-- | Display a term using the variable and constant names provided. Does not
+-- attempt to resolve name collisions.
+displayTerm :: (e -> T.Text) -> Term e Name Name -> T.Text
+displayTerm f = dTerm f []
+
+-- | Display a term. Tries to use the provided variable names where possible.
+-- Resolves name collisions.
+displayTerm' :: (e -> T.Text) -> Term e (Maybe Name) (Maybe Name) -> T.Text
+displayTerm' f = displayTerm f . findVarNames . makeVarNamesUnique . findConstNames
+
+nth :: [a] -> Natural -> Maybe a
+nth []     _ = Nothing
+nth (x:_)  0 = Just x
+nth (_:xs) n = nth xs $ n - 1
+
+varName :: [Name] -> Natural -> Name
+varName vs i = fromMaybe e $ nth vs i
+  where
+    e = "[" <> T.pack (show i) <> "]"
+
+dTerm :: (e -> T.Text) -> [Name] -> Term e Name Name -> T.Text
+dTerm _ vs (Var i) = varName vs i
+dTerm _ _  (Const c) = c
+dTerm f vs (Lambda v t) = "λ" <> v <> dLambda (v:vs) t
+  where
+    dLambda ws (Lambda w u) = " " <> w <> dLambda (w:ws) u
+    dLambda ws u            = ". " <> dTerm f ws u
+dTerm f vs (App l r) = dLeft l <> " " <> dRight r
+  where
+    dLeft t@(Lambda _ _) = "(" <> dTerm f vs t <> ")"
+    dLeft t              = dTerm f vs t
+    dRight t@(Lambda _ _) = "(" <> dTerm f vs t <> ")"
+    dRight t@(App _ _)    = "(" <> dTerm f vs t <> ")"
+    dRight t              = dTerm f vs t
+dTerm f _  (Ext e) = f e

src/Propa/Lambda/Term.hs

@@ -0,0 +1,56 @@
+-- | This module contains 'Term', the base type for lambda expressions. It also
+-- contains a few utility functions for operating on it.
+
+module Propa.Lambda.Term
+  ( Term(..)
+  , vars
+  , mapVars
+  , consts
+  , mapConsts
+  ) where
+
+import           Numeric.Natural
+
+-- | Lambda calculus term using De Bruijn indexing and expanded to deal with
+-- naming complexity and extensions.
+data Term e c v
+  = Var Natural
+  -- ^ Variable using a De Bruijn index
+  | Const c
+  -- ^ Constant living outside the variable namespace
+  | Lambda v (Term e c v)
+  -- ^ Lambda definition
+  | App (Term e c v) (Term e c v)
+  -- ^ Lambda application
+  | Ext e
+  -- ^ Term extension (set @e@ to 'Data.Void' if you don't need this)
+  deriving (Show)
+
+-- | All of a term's variable names in order from left to right.
+vars :: Term e c v -> [v]
+vars (Lambda v t) = v : vars t
+vars (App l r)    = vars l <> vars r
+vars _            = []
+
+-- | Map over the variable names.
+mapVars :: (a -> b) -> Term e c a -> Term e c b
+mapVars _ (Var i)      = Var i
+mapVars _ (Const c)    = Const c
+mapVars f (Lambda a t) = Lambda (f a) (mapVars f t)
+mapVars f (App l r)    = App (mapVars f l) (mapVars f r)
+mapVars _ (Ext e)      = Ext e
+
+-- | All of a term's constant names in order from left to right.
+consts :: Term e c v -> [c]
+consts (Const c)    = [c]
+consts (Lambda _ t) = consts t
+consts (App l r)    = consts l <> consts r
+consts _            = []
+
+-- | Map over the constant names.
+mapConsts :: (a -> b) -> Term e a v -> Term e b v
+mapConsts _ (Var i)      = Var i
+mapConsts f (Const c)    = Const (f c)
+mapConsts f (Lambda v t) = Lambda v (mapConsts f t)
+mapConsts f (App l r)    = App (mapConsts f l) (mapConsts f r)
+mapConsts _ (Ext e)      = Ext e

src/Propa/Prolog.hs

@@ -0,0 +1,143 @@
+module Propa.Prolog where
+
+import           Control.Monad
+import           Data.Foldable
+
+import           Control.Monad.Trans.Class
+import           Control.Monad.Trans.State
+import qualified Data.Map                  as Map
+import qualified Data.Set                  as Set
+
+data Term a
+  = Var a
+  | Stat String [Term a]
+  deriving (Show)
+
+instance Functor Term where
+  fmap f (Var a)          = Var $ f a
+  fmap f (Stat name args) = Stat name $ fmap (fmap f) args
+
+instance Foldable Term where
+  foldMap f (Var a)       = f a
+  foldMap f (Stat _ args) = foldMap (foldMap f) args
+
+instance Traversable Term where
+  traverse f (Var a)          = Var <$> f a
+  traverse f (Stat name args) = Stat name <$> traverse (traverse f) args
+
+data Def a = Def String [Term a] [Term a]
+  deriving (Show)
+
+instance Functor Def where
+  fmap f (Def dName dArgs dTerms) = Def dName (fmap f <$> dArgs) (fmap f <$> dTerms)
+
+instance Foldable Def where
+  foldMap f (Def _ dArgs dTerms) = foldMap (foldMap f) dArgs <> foldMap (foldMap f) dTerms
+
+instance Traversable Def where
+  traverse f (Def dName dArgs dTerms)
+    =   Def dName
+    <$> traverse (traverse f) dArgs
+    <*> traverse (traverse f) dTerms
+
+data Context = Context
+  { cDb     :: [Def String]
+  , cVarIdx :: Int
+  , cVars   :: Map.Map Int Int
+  , cTerms  :: Map.Map Int (String, [Term Int])
+  } deriving (Show)
+
+newContext :: [Def String] -> Context
+newContext db = Context db 0 Map.empty Map.empty
+
+learnVar :: Int -> Int -> UniM ()
+learnVar k v = modify $ \c -> c{cVars = Map.insert k v $ cVars c}
+
+learnTerm :: Int -> String -> [Term Int] -> UniM ()
+learnTerm k name args = modify $ \c -> c{cTerms = Map.insert k (name, args) $ cTerms c}
+
+-- | Look up a variable, first in the var map and then the term map. Returns
+-- statements unchanged.
+--
+-- If this returns a variable, then that variable is unbound.
+lookupVar :: Term Int -> UniM (Term Int)
+lookupVar t@(Stat _ _) = pure t
+lookupVar t@(Var v) = do
+  c <- get
+  case cVars c Map.!? v of
+    Just v' -> lookupVar (Var v')
+    Nothing -> pure $ case cTerms c Map.!? v of
+      Nothing           -> t
+      Just (name, args) -> Stat name args
+
+-- | A simple state monad transformer over the list monad for easy backtracking.
+-- Needs to be changed when implementing cuts.
+type UniM = StateT Context []
+
+-- | A faster version of 'nub'.
+fastNub :: (Ord a) => [a] -> [a]
+fastNub = Set.toList . Set.fromList
+
+varMap :: (Foldable a) => a String -> UniM (Map.Map String Int)
+varMap a = do
+  c <- get
+  let i = cVarIdx c
+      vars = fastNub $ toList a
+      vmap = Map.fromList $ zip vars [i..]
+  put c{cVarIdx = i + Map.size vmap}
+  pure vmap
+
+-- | Convert a definition's variables to unique integers that are not already in
+-- use in the current context.
+understand :: (Functor a, Foldable a) => a String -> UniM (a Int, Map.Map String Int)
+understand a = do
+  vmap <- varMap a
+  pure (fmap (vmap Map.!) a, vmap)
+
+satisfy :: Term Int -> UniM ()
+satisfy (Var _)          = undefined
+satisfy (Stat name args) = do
+  c <- get
+  (Def dName dArgs dTerms, _) <- understand =<< lift (cDb c)
+  lift $ guard $ name == dName -- Not sure if 'lift' is really necessary
+  unifyTerms args dArgs
+  satisfyTerms dTerms
+
+satisfyTerms :: [Term Int] -> UniM ()
+satisfyTerms = traverse_ satisfy
+
+unify :: Term Int -> Term Int -> UniM ()
+unify t1 t2 = do
+  t1' <- lookupVar t1
+  t2' <- lookupVar t2
+  case (t1', t2') of
+    (Stat name1 args1, Stat name2 args2) -> do
+      lift $ guard $ name1 == name2
+      unifyTerms args1 args2
+    (Var v1, Stat name2 args2) -> learnTerm v1 name2 args2
+    (Stat name1 args1, Var v2) -> learnTerm v2 name1 args1
+    (Var v1, Var v2) -> learnVar v1 v2 -- The order shouldn't really matter
+
+unifyTerms :: [Term Int] -> [Term Int] -> UniM ()
+unifyTerms t1 t2 = do
+  lift $ guard $ length t1 == length t2
+  sequenceA_ $ zipWith unify t1 t2
+
+run :: Term String -> UniM (Map.Map String (Term Int))
+run t = do
+  (t2, vmap) <- understand t
+  satisfy t2
+  traverse (lookupVar . Var) vmap
+
+exampleDb :: [Def String]
+exampleDb =
+  [ Def "food" [Stat "burger" []] []
+  , Def "food" [Stat "sandwich" []] []
+  , Def "meal" [Var "X"] [Stat "food" [Var "X"]]
+  ]
+
+burgerIsMeal :: Term String
+burgerIsMeal = Stat "meal" [Stat "burger" []]
+
+whatIsMeal :: Term String
+whatIsMeal = Stat "meal" [Var "X"]