Compare commits
No commits in common. "master" and "discord-haskell" have entirely different histories.
master
...
discord-ha
12 changed files with 21 additions and 664 deletions
|
|
@ -1,4 +1,3 @@
|
||||||
# propa-tools
|
# props
|
||||||
|
|
||||||
Various programming paradigm related bits and bobs. May not contain any actual
|
Propa tools
|
||||||
executables.
|
|
||||||
|
|
|
||||||
|
|
@ -1,4 +1,6 @@
|
||||||
module Main where
|
module Main where
|
||||||
|
|
||||||
|
import Props
|
||||||
|
|
||||||
main :: IO ()
|
main :: IO ()
|
||||||
main = putStrLn "Hello world!"
|
main = putStrLn helloWorld
|
||||||
|
|
|
||||||
11
package.yaml
11
package.yaml
|
|
@ -1,4 +1,4 @@
|
||||||
name: propa-tools
|
name: props
|
||||||
version: 0.1.0.0
|
version: 0.1.0.0
|
||||||
license: MIT
|
license: MIT
|
||||||
author: Garmelon <joscha@plugh.de>
|
author: Garmelon <joscha@plugh.de>
|
||||||
|
|
@ -13,17 +13,12 @@ extra-doc-files:
|
||||||
|
|
||||||
dependencies:
|
dependencies:
|
||||||
- base >= 4.7 && < 5
|
- base >= 4.7 && < 5
|
||||||
- containers
|
|
||||||
- megaparsec
|
|
||||||
- parser-combinators
|
|
||||||
- text
|
|
||||||
- transformers
|
|
||||||
|
|
||||||
library:
|
library:
|
||||||
source-dirs: src
|
source-dirs: src
|
||||||
|
|
||||||
executables:
|
executables:
|
||||||
propa-tools-exe:
|
props:
|
||||||
main: Main.hs
|
main: Main.hs
|
||||||
source-dirs: app
|
source-dirs: app
|
||||||
ghc-options:
|
ghc-options:
|
||||||
|
|
@ -31,4 +26,4 @@ executables:
|
||||||
- -rtsopts
|
- -rtsopts
|
||||||
- -with-rtsopts=-N
|
- -with-rtsopts=-N
|
||||||
dependencies:
|
dependencies:
|
||||||
- propa-tools
|
- props
|
||||||
|
|
|
||||||
|
|
@ -1,10 +1,12 @@
|
||||||
cabal-version: 1.18
|
cabal-version: 1.18
|
||||||
|
|
||||||
-- This file has been generated from package.yaml by hpack version 0.34.2.
|
-- This file has been generated from package.yaml by hpack version 0.33.0.
|
||||||
--
|
--
|
||||||
-- see: https://github.com/sol/hpack
|
-- see: https://github.com/sol/hpack
|
||||||
|
--
|
||||||
|
-- hash: 057a536ac3d0fd40b3122084eee53201158527bbcd0dbac7cec33d8fd06cf208
|
||||||
|
|
||||||
name: propa-tools
|
name: props
|
||||||
version: 0.1.0.0
|
version: 0.1.0.0
|
||||||
author: Garmelon <joscha@plugh.de>
|
author: Garmelon <joscha@plugh.de>
|
||||||
maintainer: Garmelon <joscha@plugh.de>
|
maintainer: Garmelon <joscha@plugh.de>
|
||||||
|
|
@ -20,39 +22,23 @@ extra-doc-files:
|
||||||
|
|
||||||
library
|
library
|
||||||
exposed-modules:
|
exposed-modules:
|
||||||
Propa.Lambda.Display
|
Props
|
||||||
Propa.Lambda.Term
|
|
||||||
Propa.Prolog.Debug
|
|
||||||
Propa.Prolog.Display
|
|
||||||
Propa.Prolog.Parse
|
|
||||||
Propa.Prolog.Types
|
|
||||||
Propa.Prolog.Unify
|
|
||||||
other-modules:
|
other-modules:
|
||||||
Paths_propa_tools
|
Paths_props
|
||||||
hs-source-dirs:
|
hs-source-dirs:
|
||||||
src
|
src
|
||||||
build-depends:
|
build-depends:
|
||||||
base >=4.7 && <5
|
base >=4.7 && <5
|
||||||
, containers
|
|
||||||
, megaparsec
|
|
||||||
, parser-combinators
|
|
||||||
, text
|
|
||||||
, transformers
|
|
||||||
default-language: Haskell2010
|
default-language: Haskell2010
|
||||||
|
|
||||||
executable propa-tools-exe
|
executable props
|
||||||
main-is: Main.hs
|
main-is: Main.hs
|
||||||
other-modules:
|
other-modules:
|
||||||
Paths_propa_tools
|
Paths_props
|
||||||
hs-source-dirs:
|
hs-source-dirs:
|
||||||
app
|
app
|
||||||
ghc-options: -threaded -rtsopts -with-rtsopts=-N
|
ghc-options: -threaded -rtsopts -with-rtsopts=-N
|
||||||
build-depends:
|
build-depends:
|
||||||
base >=4.7 && <5
|
base >=4.7 && <5
|
||||||
, containers
|
, props
|
||||||
, megaparsec
|
|
||||||
, parser-combinators
|
|
||||||
, propa-tools
|
|
||||||
, text
|
|
||||||
, transformers
|
|
||||||
default-language: Haskell2010
|
default-language: Haskell2010
|
||||||
|
|
@ -1,127 +0,0 @@
|
||||||
{-# 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
|
|
||||||
|
|
@ -1,56 +0,0 @@
|
||||||
-- | 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
|
|
||||||
|
|
@ -1,23 +0,0 @@
|
||||||
{-# LANGUAGE OverloadedStrings #-}
|
|
||||||
|
|
||||||
module Propa.Prolog.Debug
|
|
||||||
( parseAndRun
|
|
||||||
) where
|
|
||||||
|
|
||||||
import qualified Data.Text as T
|
|
||||||
import qualified Data.Text.IO as T
|
|
||||||
|
|
||||||
import Propa.Prolog.Display
|
|
||||||
import Propa.Prolog.Parse
|
|
||||||
import Propa.Prolog.Unify
|
|
||||||
|
|
||||||
parseAndRun :: String -> String -> IO ()
|
|
||||||
parseAndRun dbStr statsStr = T.putStrLn $ case results of
|
|
||||||
Left e -> e
|
|
||||||
Right [] -> "No."
|
|
||||||
Right rs -> T.intercalate "\n" rs
|
|
||||||
where
|
|
||||||
results = do
|
|
||||||
db <- parseDb "<db>" $ T.pack dbStr
|
|
||||||
stats <- parseStats "<query>" $ T.pack statsStr
|
|
||||||
pure $ map displayResult $ run db stats
|
|
||||||
|
|
@ -1,71 +0,0 @@
|
||||||
{-# LANGUAGE OverloadedStrings #-}
|
|
||||||
|
|
||||||
module Propa.Prolog.Display
|
|
||||||
( displayTerm
|
|
||||||
, displayTerms
|
|
||||||
, displayDef
|
|
||||||
, displayDefs
|
|
||||||
, displayResult
|
|
||||||
) where
|
|
||||||
|
|
||||||
import Data.Char
|
|
||||||
import Data.List
|
|
||||||
|
|
||||||
import qualified Data.Map as Map
|
|
||||||
import qualified Data.Text as T
|
|
||||||
|
|
||||||
import Propa.Prolog.Types
|
|
||||||
|
|
||||||
displayName :: T.Text -> T.Text
|
|
||||||
displayName name
|
|
||||||
| T.all isLower name = name
|
|
||||||
| otherwise = "\"" <> escaped <> "\""
|
|
||||||
where
|
|
||||||
escaped = foldl' (\s (a, b) -> T.replace a b s) name
|
|
||||||
[ ("\\", "\\\\")
|
|
||||||
, ("\n", "\\n")
|
|
||||||
, ("\r", "\\r")
|
|
||||||
, ("\t", "\\t")
|
|
||||||
]
|
|
||||||
|
|
||||||
displayStat :: Stat T.Text -> T.Text
|
|
||||||
displayStat (Stat "[]" []) = "[]"
|
|
||||||
displayStat (Stat "[|]" [a, b]) = "[" <> displayTerm a <> displayList b
|
|
||||||
displayStat (Stat name []) = displayName name
|
|
||||||
displayStat (Stat name args)
|
|
||||||
= displayName name
|
|
||||||
<> "("
|
|
||||||
<> T.intercalate ", " (map displayTerm args)
|
|
||||||
<> ")"
|
|
||||||
|
|
||||||
displayList :: Term T.Text -> T.Text
|
|
||||||
displayList (TStat (Stat "[|]" [a, b])) = "," <> displayTerm a <> displayList b
|
|
||||||
displayList (TStat (Stat "[]" [])) = "]"
|
|
||||||
displayList t = "|" <> displayTerm t <> "]"
|
|
||||||
|
|
||||||
displayTerm :: Term T.Text -> T.Text
|
|
||||||
displayTerm (TVar v) = v
|
|
||||||
displayTerm (TInt i) = T.pack $ show i
|
|
||||||
displayTerm (TStat s) = displayStat s
|
|
||||||
|
|
||||||
displayTerms :: [Term T.Text] -> T.Text
|
|
||||||
displayTerms terms = T.intercalate ",\n" (map displayTerm terms) <> "."
|
|
||||||
|
|
||||||
displayDef :: Def T.Text -> T.Text
|
|
||||||
displayDef (Def stat []) = displayStat stat <> "."
|
|
||||||
displayDef (Def stat stats)
|
|
||||||
= displayStat stat
|
|
||||||
<> " :-\n"
|
|
||||||
<> T.intercalate ",\n" (map (\t -> " " <> displayStat t) stats)
|
|
||||||
<> "."
|
|
||||||
|
|
||||||
displayDefs :: [Def T.Text] -> T.Text
|
|
||||||
displayDefs = T.intercalate "\n" . map displayDef
|
|
||||||
|
|
||||||
displayResult :: Map.Map T.Text (Term T.Text) -> T.Text
|
|
||||||
displayResult m
|
|
||||||
| null termsToDisplay = "Yes."
|
|
||||||
| otherwise = T.intercalate "\n" termsAsStrings
|
|
||||||
where
|
|
||||||
termsToDisplay = filter (\(k, v) -> v /= TVar k) $ Map.assocs m
|
|
||||||
termsAsStrings = map (\(k, v) -> k <> " = " <> displayTerm v) termsToDisplay
|
|
||||||
|
|
@ -1,128 +0,0 @@
|
||||||
{-# LANGUAGE OverloadedStrings #-}
|
|
||||||
|
|
||||||
module Propa.Prolog.Parse
|
|
||||||
( parseStats
|
|
||||||
, parseDb
|
|
||||||
) where
|
|
||||||
|
|
||||||
import Control.Monad
|
|
||||||
import Data.Bifunctor
|
|
||||||
import Data.Char
|
|
||||||
import Data.Void
|
|
||||||
|
|
||||||
import Control.Monad.Combinators.Expr
|
|
||||||
import qualified Data.Text as T
|
|
||||||
import Text.Megaparsec
|
|
||||||
import qualified Text.Megaparsec.Char as C
|
|
||||||
import qualified Text.Megaparsec.Char.Lexer as L
|
|
||||||
|
|
||||||
import Propa.Prolog.Types
|
|
||||||
|
|
||||||
type Parser = Parsec Void T.Text
|
|
||||||
|
|
||||||
-- Lexeme stuff
|
|
||||||
|
|
||||||
space :: Parser ()
|
|
||||||
space = L.space C.space1 (L.skipLineComment "%") (L.skipBlockComment "/*" "*/")
|
|
||||||
|
|
||||||
lexeme :: Parser a -> Parser a
|
|
||||||
lexeme = L.lexeme space
|
|
||||||
|
|
||||||
symbol :: T.Text -> Parser T.Text
|
|
||||||
symbol = L.symbol space
|
|
||||||
|
|
||||||
parens :: Parser a -> Parser a
|
|
||||||
parens = between (symbol "(") (symbol ")")
|
|
||||||
|
|
||||||
brackets :: Parser a -> Parser a
|
|
||||||
brackets = between (symbol "[") (symbol "]")
|
|
||||||
|
|
||||||
-- Names
|
|
||||||
|
|
||||||
pName :: Parser T.Text
|
|
||||||
pName = lexeme $ unquotedName <|> quotedName
|
|
||||||
where
|
|
||||||
unquotedName = takeWhile1P (Just "lowercase character") isLower
|
|
||||||
quotedName = fmap T.pack $ C.char '\'' *> manyTill L.charLiteral (C.char '\'')
|
|
||||||
|
|
||||||
pVarName :: Parser T.Text
|
|
||||||
pVarName = lexeme $ takeWhile1P (Just "uppercase character") isUpper
|
|
||||||
|
|
||||||
-- Statements
|
|
||||||
|
|
||||||
pTermToStat :: Parser (Term T.Text) -> Parser (Stat T.Text)
|
|
||||||
pTermToStat p = do
|
|
||||||
term <- p
|
|
||||||
case term of
|
|
||||||
(TVar _) -> fail "expected statement, not variable"
|
|
||||||
(TInt _) -> fail "expected statement, not integer"
|
|
||||||
(TStat s) -> pure s
|
|
||||||
|
|
||||||
-- | Parse a statement of the form @name(args)@.
|
|
||||||
pPlainStat :: Parser (Stat T.Text)
|
|
||||||
pPlainStat = do
|
|
||||||
name <- pName
|
|
||||||
terms <- parens (pTerm `sepBy1` symbol ",") <|> pure []
|
|
||||||
pure $ Stat name terms
|
|
||||||
|
|
||||||
pStat :: Parser (Stat T.Text)
|
|
||||||
pStat = pPlainStat <|> pTermToStat pTerm
|
|
||||||
|
|
||||||
pStats :: Parser [Stat T.Text]
|
|
||||||
pStats = (pStat `sepBy1` symbol ",") <* symbol "."
|
|
||||||
|
|
||||||
-- Terms
|
|
||||||
|
|
||||||
pCons :: Parser (Term T.Text)
|
|
||||||
pCons = brackets $ do
|
|
||||||
elems <- pTerm `sepBy1` symbol ","
|
|
||||||
void $ symbol "|"
|
|
||||||
rest <- pTerm
|
|
||||||
pure $ foldr (\a b -> TStat $ Stat "[|]" [a, b]) rest elems
|
|
||||||
|
|
||||||
pList :: Parser (Term T.Text)
|
|
||||||
pList = do
|
|
||||||
elems <- brackets $ pTerm `sepBy` symbol ","
|
|
||||||
pure $ foldr (\a b -> TStat $ Stat "[|]" [a, b]) (TStat $ Stat "[]" []) elems
|
|
||||||
|
|
||||||
-- | Parse a term that is not an expression.
|
|
||||||
pPlainTerm :: Parser (Term T.Text)
|
|
||||||
pPlainTerm
|
|
||||||
= (TVar <$> pVarName)
|
|
||||||
<|> (TInt <$> L.signed (pure ()) L.decimal)
|
|
||||||
<|> (TStat <$> pPlainStat)
|
|
||||||
<|> try pCons
|
|
||||||
<|> pList
|
|
||||||
<|> parens pTerm
|
|
||||||
|
|
||||||
pTerm :: Parser (Term T.Text)
|
|
||||||
pTerm = makeExprParser pPlainTerm
|
|
||||||
[ [ binary "=" ]
|
|
||||||
]
|
|
||||||
where
|
|
||||||
binary name = InfixL $ (\a b -> TStat $ Stat name [a, b]) <$ symbol name
|
|
||||||
|
|
||||||
-- Definitions
|
|
||||||
|
|
||||||
pDef :: Parser (Def T.Text)
|
|
||||||
pDef = do
|
|
||||||
stat <- pStat
|
|
||||||
stats <- (symbol ":-" *> (pStat `sepBy1` symbol ",")) <|> pure []
|
|
||||||
void $ symbol "."
|
|
||||||
pure $ Def stat stats
|
|
||||||
|
|
||||||
pDefs :: Parser [Def T.Text]
|
|
||||||
pDefs = many pDef
|
|
||||||
|
|
||||||
-- And finally, our nice parsers
|
|
||||||
|
|
||||||
parseHelper :: Parser a -> FilePath -> T.Text -> Either T.Text a
|
|
||||||
parseHelper p path input
|
|
||||||
= first (T.pack . errorBundlePretty)
|
|
||||||
$ parse (space *> p <* eof) path input
|
|
||||||
|
|
||||||
parseStats :: FilePath -> T.Text -> Either T.Text [Stat T.Text]
|
|
||||||
parseStats = parseHelper pStats
|
|
||||||
|
|
||||||
parseDb :: FilePath -> T.Text -> Either T.Text (Db T.Text)
|
|
||||||
parseDb = parseHelper pDefs
|
|
||||||
|
|
@ -1,60 +0,0 @@
|
||||||
module Propa.Prolog.Types
|
|
||||||
( Stat(..)
|
|
||||||
, Term(..)
|
|
||||||
, tVar
|
|
||||||
, Def(..)
|
|
||||||
, Db
|
|
||||||
) where
|
|
||||||
|
|
||||||
import qualified Data.Text as T
|
|
||||||
|
|
||||||
data Stat a = Stat T.Text [Term a]
|
|
||||||
deriving (Show, Eq)
|
|
||||||
|
|
||||||
instance Functor Stat where
|
|
||||||
fmap f (Stat name terms) = Stat name $ fmap (fmap f) terms
|
|
||||||
|
|
||||||
instance Foldable Stat where
|
|
||||||
foldMap f (Stat _ terms) = foldMap (foldMap f) terms
|
|
||||||
|
|
||||||
instance Traversable Stat where
|
|
||||||
traverse f (Stat name terms) = Stat name <$> traverse (traverse f) terms
|
|
||||||
|
|
||||||
data Term a
|
|
||||||
= TVar a
|
|
||||||
| TInt Integer
|
|
||||||
| TStat (Stat a)
|
|
||||||
deriving (Show, Eq)
|
|
||||||
|
|
||||||
instance Functor Term where
|
|
||||||
fmap f (TVar a) = TVar $ f a
|
|
||||||
fmap _ (TInt i) = TInt i
|
|
||||||
fmap f (TStat s) = TStat $ fmap f s
|
|
||||||
|
|
||||||
instance Foldable Term where
|
|
||||||
foldMap f (TVar a) = f a
|
|
||||||
foldMap _ (TInt _) = mempty
|
|
||||||
foldMap f (TStat s) = foldMap f s
|
|
||||||
|
|
||||||
instance Traversable Term where
|
|
||||||
traverse f (TVar a) = TVar <$> f a
|
|
||||||
traverse _ (TInt i) = pure $ TInt i
|
|
||||||
traverse f (TStat s) = TStat <$> traverse f s
|
|
||||||
|
|
||||||
tVar :: Term a -> Maybe a
|
|
||||||
tVar (TVar v) = Just v
|
|
||||||
tVar _ = Nothing
|
|
||||||
|
|
||||||
data Def a = Def (Stat a) [Stat a]
|
|
||||||
deriving (Show)
|
|
||||||
|
|
||||||
instance Functor Def where
|
|
||||||
fmap f (Def stat stats) = Def (fmap f stat) (fmap f <$> stats)
|
|
||||||
|
|
||||||
instance Foldable Def where
|
|
||||||
foldMap f (Def stat stats) = foldMap f stat <> foldMap (foldMap f) stats
|
|
||||||
|
|
||||||
instance Traversable Def where
|
|
||||||
traverse f (Def stat stats) = Def <$> traverse f stat <*> traverse (traverse f) stats
|
|
||||||
|
|
||||||
type Db a = [Def a]
|
|
||||||
|
|
@ -1,164 +0,0 @@
|
||||||
{-# LANGUAGE OverloadedStrings #-}
|
|
||||||
|
|
||||||
module Propa.Prolog.Unify
|
|
||||||
( run
|
|
||||||
) where
|
|
||||||
|
|
||||||
import Control.Applicative
|
|
||||||
import Control.Monad
|
|
||||||
import Data.Foldable
|
|
||||||
import Data.List
|
|
||||||
import Data.Tuple
|
|
||||||
|
|
||||||
import Control.Monad.Trans.Class
|
|
||||||
import Control.Monad.Trans.State
|
|
||||||
import qualified Data.Map as Map
|
|
||||||
import qualified Data.Set as Set
|
|
||||||
import qualified Data.Text as T
|
|
||||||
|
|
||||||
import Propa.Prolog.Types
|
|
||||||
|
|
||||||
-- General utility functions
|
|
||||||
|
|
||||||
-- | Start at a value and follow the map's entries until the end of the chain of
|
|
||||||
-- references.
|
|
||||||
follow :: (Ord a) => (b -> Maybe a) -> Map.Map a b -> b -> b
|
|
||||||
follow f m b = maybe b (follow f m) $ (m Map.!?) =<< f b
|
|
||||||
|
|
||||||
-- | Deduplicates the elements of a finite list. Doesn't preserve the order of
|
|
||||||
-- the elements. Doesn't work on infinite lists.
|
|
||||||
deduplicate :: (Ord a) => [a] -> [a]
|
|
||||||
deduplicate = Set.toList . Set.fromList
|
|
||||||
|
|
||||||
-- Now the fun begins...
|
|
||||||
|
|
||||||
data Context = Context
|
|
||||||
{ cDb :: Db T.Text
|
|
||||||
, cVarIdx :: Int
|
|
||||||
, cTerms :: Map.Map Int (Term Int)
|
|
||||||
} deriving (Show)
|
|
||||||
|
|
||||||
newContext :: [Def T.Text] -> Context
|
|
||||||
newContext db = Context db 0 Map.empty
|
|
||||||
|
|
||||||
bindTerm :: Int -> Term Int -> UniM ()
|
|
||||||
bindTerm k v = modify $ \c -> c{cTerms = Map.insert k v $ cTerms c}
|
|
||||||
|
|
||||||
-- | Look up a variable, first repeatedly in the var map and then the term map.
|
|
||||||
-- Returns statements unchanged.
|
|
||||||
--
|
|
||||||
-- If this returns a variable, then that variable is not bound.
|
|
||||||
lookupTerm :: Term Int -> UniM (Term Int)
|
|
||||||
lookupTerm t = do
|
|
||||||
c <- get
|
|
||||||
pure $ follow tVar (cTerms c) t
|
|
||||||
|
|
||||||
-- | A simple state monad transformer over the list monad for easy backtracking.
|
|
||||||
-- Needs to be changed when implementing cuts.
|
|
||||||
type UniM = StateT Context []
|
|
||||||
|
|
||||||
varMap :: (Foldable a) => a T.Text -> UniM (Map.Map T.Text Int)
|
|
||||||
varMap a = do
|
|
||||||
c <- get
|
|
||||||
let i = cVarIdx c
|
|
||||||
vars = deduplicate $ 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 T.Text -> UniM (a Int, Map.Map T.Text Int)
|
|
||||||
understand a = do
|
|
||||||
vmap <- varMap a
|
|
||||||
pure (fmap (vmap Map.!) a, vmap)
|
|
||||||
|
|
||||||
satisfyStat :: Stat Int -> UniM ()
|
|
||||||
satisfyStat stat = do
|
|
||||||
c <- get
|
|
||||||
(Def dStat dStats, _) <- understand =<< lift (cDb c)
|
|
||||||
unifyStat stat dStat
|
|
||||||
satisfyStats dStats
|
|
||||||
|
|
||||||
satisfyStats :: [Stat Int] -> UniM ()
|
|
||||||
satisfyStats = traverse_ satisfyStat
|
|
||||||
|
|
||||||
unifyStat :: Stat Int -> Stat Int -> UniM ()
|
|
||||||
unifyStat (Stat name1 args1) (Stat name2 args2) = do
|
|
||||||
guard $ name1 == name2
|
|
||||||
unifyTerms args1 args2
|
|
||||||
|
|
||||||
unifyTerm :: Term Int -> Term Int -> UniM ()
|
|
||||||
unifyTerm t1 t2 = do
|
|
||||||
t1' <- lookupTerm t1
|
|
||||||
t2' <- lookupTerm t2
|
|
||||||
case (t1', t2') of
|
|
||||||
(TStat s1, TStat s2) -> unifyStat s1 s2
|
|
||||||
(TInt i1, TInt i2) -> guard $ i1 == i2
|
|
||||||
(TVar v, TVar w) | v == w -> pure ()
|
|
||||||
(TVar v, t) -> bindTerm v t
|
|
||||||
(t, TVar v) -> bindTerm v t
|
|
||||||
(_, _) -> empty
|
|
||||||
|
|
||||||
unifyTerms :: [Term Int] -> [Term Int] -> UniM ()
|
|
||||||
unifyTerms t1 t2 = do
|
|
||||||
guard $ length t1 == length t2
|
|
||||||
sequenceA_ $ zipWith unifyTerm t1 t2
|
|
||||||
|
|
||||||
-- Figuring out how to display the result of the unification
|
|
||||||
|
|
||||||
-- | An infinite list of possible variable names: @A@, @B@, ..., @A1@, @B1@,
|
|
||||||
-- ..., @A2@, ...
|
|
||||||
varNames :: [T.Text]
|
|
||||||
varNames = do
|
|
||||||
num <- "" : map (T.pack . show) [(1::Integer)..]
|
|
||||||
char <- alphabet
|
|
||||||
pure $ char <> num
|
|
||||||
where
|
|
||||||
alphabet = map T.singleton ['A'..'Z']
|
|
||||||
|
|
||||||
-- | Find a naming (Map from integer to name) for all variables in a list of
|
|
||||||
-- terms based on the original variable names and the variable mapping. Attempts
|
|
||||||
-- to map variables to known variables instead of a common unknown variable.
|
|
||||||
findVarNaming :: Map.Map T.Text Int -> Map.Map Int (Term Int) -> [Term Int] -> Map.Map Int T.Text
|
|
||||||
findVarNaming known vars terms =
|
|
||||||
let knownLookedUp :: Map.Map T.Text Int
|
|
||||||
knownLookedUp = Map.mapMaybe (tVar . follow tVar vars . TVar) known
|
|
||||||
knownNaming = Map.fromList $ reverse $ map swap $ Map.toList knownLookedUp
|
|
||||||
knownNames = Map.keysSet known
|
|
||||||
knownVars = Map.keysSet knownNaming
|
|
||||||
termVars = Set.fromList $ concatMap toList terms
|
|
||||||
unknownVars = termVars Set.\\ knownVars
|
|
||||||
availVarNames = filter (not . (`Set.member` knownNames)) varNames
|
|
||||||
unknownNaming = Map.fromList $ zip (sort $ Set.toList unknownVars) availVarNames
|
|
||||||
in knownNaming <> unknownNaming
|
|
||||||
|
|
||||||
-- | Recursively set variables to their most resolved term.
|
|
||||||
resolveVars :: Term Int -> UniM (Term Int)
|
|
||||||
resolveVars t = do
|
|
||||||
t2 <- lookupTerm t
|
|
||||||
case t2 of
|
|
||||||
(TVar v) -> pure $ TVar v
|
|
||||||
(TInt i) -> pure $ TInt i
|
|
||||||
(TStat (Stat name args)) -> TStat . Stat name <$> traverse resolveVars args
|
|
||||||
|
|
||||||
-- | Helper type so I can resolve variables in multiple statements
|
|
||||||
-- simultaneously.
|
|
||||||
newtype Stats a = Stats { unStats :: [Stat a] }
|
|
||||||
|
|
||||||
instance Functor Stats where
|
|
||||||
fmap f (Stats ts) = Stats $ fmap (fmap f) ts
|
|
||||||
|
|
||||||
instance Foldable Stats where
|
|
||||||
foldMap f (Stats ts) = foldMap (foldMap f) ts
|
|
||||||
|
|
||||||
run :: Db T.Text -> [Stat T.Text] -> [Map.Map T.Text (Term T.Text)]
|
|
||||||
run db stats = map fst $ runStateT helper $ newContext db
|
|
||||||
where
|
|
||||||
helper = do
|
|
||||||
(stats2, vmap) <- understand $ Stats stats
|
|
||||||
satisfyStats $ unStats stats2
|
|
||||||
tmap <- traverse (resolveVars . TVar) vmap
|
|
||||||
c <- get
|
|
||||||
let naming = findVarNaming vmap (cTerms c) $ Map.elems tmap
|
|
||||||
pure $ fmap (naming Map.!) <$> tmap
|
|
||||||
4
src/Props.hs
Normal file
4
src/Props.hs
Normal file
|
|
@ -0,0 +1,4 @@
|
||||||
|
module Props where
|
||||||
|
|
||||||
|
helloWorld :: String
|
||||||
|
helloWorld = "Hello World!"
|
||||||
Loading…
Add table
Add a link
Reference in a new issue