2026-01-21 11:24:30 +00:00
|
|
|
{-# HLINT ignore "Redundant flip" #-}
|
2026-01-21 17:11:13 +00:00
|
|
|
{-# LANGUAGE ImportQualifiedPost #-}
|
2026-01-27 16:41:33 +00:00
|
|
|
{-# LANGUAGE OverloadedStrings #-}
|
2026-01-23 18:12:47 +00:00
|
|
|
{-# LANGUAGE ScopedTypeVariables #-}
|
2026-01-27 16:41:33 +00:00
|
|
|
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
|
2026-01-29 16:42:53 +00:00
|
|
|
{-# LANGUAGE InstanceSigs #-}
|
2026-01-27 16:41:33 +00:00
|
|
|
|
2026-01-21 11:24:30 +00:00
|
|
|
module Datalog.NaiveDatabase where
|
|
|
|
|
|
2026-01-27 16:41:33 +00:00
|
|
|
import Control.Exception.Base
|
|
|
|
|
import Data.List
|
2026-01-21 11:24:30 +00:00
|
|
|
import Data.Map (Map)
|
2026-01-27 16:41:33 +00:00
|
|
|
import Data.Map qualified as Map
|
|
|
|
|
import Data.Maybe
|
2026-01-21 11:24:30 +00:00
|
|
|
import Data.Set (Set)
|
2026-01-21 17:11:13 +00:00
|
|
|
import Data.Set qualified as Set
|
|
|
|
|
import Data.Text (Text)
|
|
|
|
|
import Data.Void
|
2026-01-27 16:41:33 +00:00
|
|
|
import Datalog.DatalogParser (Head (HeadSingle), Literal (..), Statement (..), Term (..), parseDatalog)
|
|
|
|
|
import Text.Megaparsec (ParseErrorBundle)
|
2026-01-29 16:30:47 +00:00
|
|
|
import Datalog.Rules
|
2026-01-21 11:24:30 +00:00
|
|
|
|
2026-01-27 16:41:33 +00:00
|
|
|
data NaiveDatabase = NaiveDatabase
|
|
|
|
|
{ relations :: Map RelationId Relation
|
|
|
|
|
, constants :: Set Constant
|
2026-01-29 15:07:14 +00:00
|
|
|
} deriving (Show, Eq)
|
2026-01-21 17:11:13 +00:00
|
|
|
|
2026-01-22 10:57:11 +00:00
|
|
|
|
2026-01-29 16:42:53 +00:00
|
|
|
instance DatalogDB NaiveDatabase where
|
|
|
|
|
emptyDB :: NaiveDatabase
|
|
|
|
|
emptyDB = NaiveDatabase
|
2026-01-27 16:41:33 +00:00
|
|
|
{ relations = Map.empty
|
|
|
|
|
, constants = Set.empty -- the Herbrand universe
|
|
|
|
|
}
|
2026-01-21 17:11:13 +00:00
|
|
|
|
2026-01-29 17:02:27 +00:00
|
|
|
lookupRelation :: NaiveDatabase -> Text -> Maybe Relation
|
|
|
|
|
lookupRelation db relationName =
|
|
|
|
|
Map.lookup relationName $ relations db
|
|
|
|
|
|
2026-01-29 16:42:53 +00:00
|
|
|
-- insertRelation :: NaiveDatabase -> Text -> Relation -> NaiveDatabase
|
|
|
|
|
-- insertRelation = _
|
|
|
|
|
|
2026-01-29 17:02:27 +00:00
|
|
|
lookupRelation0 :: RelationId -> NaiveDatabase -> Int -> Set [Term] -> Relation
|
|
|
|
|
lookupRelation0 relationName db newArity tuples =
|
|
|
|
|
case lookupRelation db relationName of
|
2026-01-28 12:39:32 +00:00
|
|
|
Nothing -> Relation relationName newArity tuples []
|
|
|
|
|
Just relation ->
|
|
|
|
|
if _arity relation == newArity then
|
|
|
|
|
let newTuples = Set.union tuples $ _tuples relation
|
2026-01-29 15:07:14 +00:00
|
|
|
in relation { _tuples = newTuples }
|
2026-01-28 12:39:32 +00:00
|
|
|
else throw $ BadArityException relationName newArity
|
|
|
|
|
|
2026-01-21 17:11:13 +00:00
|
|
|
withFacts :: [Text] -> NaiveDatabase
|
2026-01-28 12:39:32 +00:00
|
|
|
withFacts =
|
|
|
|
|
foldr (addFact . extractFact) emptyDB
|
2026-01-27 16:41:33 +00:00
|
|
|
where
|
|
|
|
|
extractFact :: Text -> Literal
|
|
|
|
|
extractFact factText =
|
2026-01-27 17:33:44 +00:00
|
|
|
case parseDatalog factText of
|
2026-01-27 16:41:33 +00:00
|
|
|
Right (Fact fact) -> fact
|
|
|
|
|
Right otherStatement -> throw $ NonFactException factText otherStatement
|
|
|
|
|
Left ex -> throw $ CannotParseStatementException factText ex
|
2026-01-28 10:02:25 +00:00
|
|
|
addFact :: Literal -> NaiveDatabase -> NaiveDatabase
|
2026-01-29 17:02:27 +00:00
|
|
|
addFact (Literal neg relationName terms) db@(NaiveDatabase relationMap constantSet) =
|
2026-01-27 16:41:33 +00:00
|
|
|
NaiveDatabase newRelationMap newConstantSet
|
|
|
|
|
where
|
|
|
|
|
newArity = length terms
|
2026-01-29 17:02:27 +00:00
|
|
|
newRelation = lookupRelation0 relationName db newArity (Set.singleton terms)
|
2026-01-27 16:41:33 +00:00
|
|
|
newRelationMap = Map.insert relationName newRelation relationMap
|
|
|
|
|
newConstantSet = Set.union constantSet $ Set.fromList terms
|
2026-01-23 18:12:47 +00:00
|
|
|
|
2026-01-27 16:41:33 +00:00
|
|
|
data BodyConstraint = BodyConstraint
|
2026-01-28 10:02:25 +00:00
|
|
|
{ _subRelation :: Relation
|
2026-01-27 18:40:05 +00:00
|
|
|
, _elements :: [RuleElement]
|
2026-01-27 16:41:33 +00:00
|
|
|
}
|
2026-01-23 18:12:47 +00:00
|
|
|
|
2026-01-27 16:41:33 +00:00
|
|
|
data RuleContext = RuleContext
|
|
|
|
|
{ __relation :: Relation
|
2026-01-27 17:55:19 +00:00
|
|
|
, _variableNames :: [Text]
|
|
|
|
|
, _headEntries :: [RuleElement]
|
2026-01-27 16:41:33 +00:00
|
|
|
, _bodyConstraints :: [BodyConstraint]
|
|
|
|
|
, _db :: NaiveDatabase
|
|
|
|
|
}
|
2026-01-23 18:12:47 +00:00
|
|
|
|
2026-01-29 15:07:14 +00:00
|
|
|
appendRule :: Relation -> RelationRule -> Relation
|
|
|
|
|
appendRule relation rule =
|
|
|
|
|
relation {
|
|
|
|
|
_rules = rule : (_rules relation)
|
|
|
|
|
}
|
|
|
|
|
-- Relation { _name = _name relation
|
|
|
|
|
-- , _arity = _arity relation
|
|
|
|
|
-- , _tuples = _tuples relation
|
|
|
|
|
-- , _rules = rule : (_rules relation)
|
|
|
|
|
-- }
|
|
|
|
|
|
|
|
|
|
toRuleBodyElement :: BodyConstraint -> RuleBodyElement
|
|
|
|
|
toRuleBodyElement (BodyConstraint subRelation elements) =
|
|
|
|
|
RuleBodyElement {
|
|
|
|
|
_subRelationId = _name subRelation
|
|
|
|
|
, _ruleElements = elements
|
|
|
|
|
}
|
|
|
|
|
|
2026-01-22 17:33:49 +00:00
|
|
|
withFactsAndRules :: [Text] -> [Text] -> NaiveDatabase
|
2026-01-27 18:01:30 +00:00
|
|
|
withFactsAndRules facts = foldr (addRule . extractRule) (withFacts facts)
|
2026-01-27 16:41:33 +00:00
|
|
|
where
|
2026-01-29 15:07:14 +00:00
|
|
|
|
|
|
|
|
extractRule :: Text -> (Literal, [Literal])
|
|
|
|
|
extractRule ruleText =
|
|
|
|
|
case parseDatalog ruleText of
|
|
|
|
|
Right (Rule (HeadSingle lhs) rhs) -> (lhs, rhs)
|
|
|
|
|
Right otherStatement -> throw $ NonRuleException ruleText otherStatement
|
|
|
|
|
Left ex -> throw $ CannotParseStatementException ruleText ex
|
|
|
|
|
digestHead :: NaiveDatabase -> Relation -> Literal -> RuleContext
|
|
|
|
|
digestHead db relation (Literal neg relationName terms) =
|
|
|
|
|
RuleContext
|
|
|
|
|
{ __relation = relation
|
|
|
|
|
, _variableNames = variableNames
|
|
|
|
|
, _headEntries = entries'
|
|
|
|
|
, _bodyConstraints = []
|
|
|
|
|
, _db = NaiveDatabase relationMap' constants'
|
|
|
|
|
}
|
|
|
|
|
where
|
|
|
|
|
variableNames = nub $ extractVariableNames terms
|
|
|
|
|
headTermToElement :: Term -> RuleElement
|
|
|
|
|
headTermToElement (Var name) =
|
|
|
|
|
RuleElementVariable $ lookupVariable name variableNames
|
|
|
|
|
headTermToElement constant = RuleElementConstant constant
|
|
|
|
|
relationMap :: Map RelationId Relation = relations db
|
|
|
|
|
relationMap' = Map.insert relationName relation relationMap
|
|
|
|
|
extraVariables = headTermToElement <$> terms
|
|
|
|
|
entries' = nub extraVariables
|
|
|
|
|
extraConstants = mapMaybe extractConstant entries' where
|
|
|
|
|
extractConstant :: RuleElement -> Maybe Constant
|
|
|
|
|
extractConstant (RuleElementConstant constant) = Just constant
|
|
|
|
|
extractConstant _ = Nothing
|
|
|
|
|
constants' = Set.union (constants db) $ Set.fromList extraConstants
|
|
|
|
|
digestBody :: Literal -> RuleContext -> RuleContext
|
|
|
|
|
digestBody (Literal neg subRelationName subTerms) context =
|
|
|
|
|
context {
|
|
|
|
|
_variableNames = variableNames
|
|
|
|
|
, _bodyConstraints = newConstraint : constraints
|
|
|
|
|
, _db = NaiveDatabase relationMap' constants'
|
|
|
|
|
}
|
|
|
|
|
where
|
|
|
|
|
variableNames = nub $ _variableNames context ++ extractVariableNames subTerms
|
|
|
|
|
newArity = length subTerms
|
2026-01-29 17:02:27 +00:00
|
|
|
subRelation = lookupRelation0 subRelationName (_db context) newArity Set.empty
|
2026-01-29 15:07:14 +00:00
|
|
|
relationMap :: Map RelationId Relation = relations (_db context)
|
|
|
|
|
relationMap' = Map.insert subRelationName subRelation relationMap
|
|
|
|
|
extraConstants = mapMaybe constantFromTerm subTerms where
|
|
|
|
|
constantFromTerm :: Term -> Maybe Constant
|
|
|
|
|
constantFromTerm (Var _) = Nothing
|
|
|
|
|
constantFromTerm constant = Just constant
|
|
|
|
|
constants' = Set.union (constants (_db context)) $ Set.fromList extraConstants
|
|
|
|
|
constraints = _bodyConstraints context
|
|
|
|
|
newConstraint = BodyConstraint subRelation subRuleElements where
|
|
|
|
|
subRuleElements = toRuleElement <$> subTerms
|
|
|
|
|
toRuleElement :: Term -> RuleElement
|
|
|
|
|
toRuleElement (Var varName) = RuleElementVariable $ lookupVariable varName variableNames
|
|
|
|
|
toRuleElement constant = RuleElementConstant constant
|
|
|
|
|
lookupVariable :: Text -> [Text] -> Int
|
|
|
|
|
lookupVariable varName variableNames =
|
|
|
|
|
case elemIndex varName variableNames of
|
|
|
|
|
Just index -> index
|
|
|
|
|
Nothing -> throw $ VariableLookupException varName variableNames
|
|
|
|
|
|
|
|
|
|
addRule :: (Literal, [Literal]) -> NaiveDatabase -> NaiveDatabase
|
|
|
|
|
addRule (ruleHead, body) db =
|
|
|
|
|
NaiveDatabase relationMap' constants' where
|
2026-01-27 16:41:33 +00:00
|
|
|
relationName = predName ruleHead
|
|
|
|
|
terms = arguments ruleHead
|
|
|
|
|
newArity = length terms
|
2026-01-29 17:02:27 +00:00
|
|
|
relation = lookupRelation0 relationName db newArity Set.empty
|
2026-01-27 18:01:30 +00:00
|
|
|
context = digestHead db relation ruleHead
|
2026-01-28 10:02:25 +00:00
|
|
|
context' = foldr digestBody context body
|
2026-01-27 18:01:30 +00:00
|
|
|
db' = _db context'
|
2026-01-27 16:41:33 +00:00
|
|
|
relationMap = relations db'
|
2026-01-29 15:07:14 +00:00
|
|
|
relation' = appendRule relation RelationRule {
|
|
|
|
|
headVariables = _variableNames context'
|
|
|
|
|
, bodyElements = toRuleBodyElement <$> _bodyConstraints context'
|
|
|
|
|
}
|
2026-01-27 18:40:05 +00:00
|
|
|
relationMap' = Map.insert relationName relation' relationMap
|
2026-01-27 16:41:33 +00:00
|
|
|
constants' = constants db'
|
2026-01-29 16:30:47 +00:00
|
|
|
|
2026-01-29 15:07:14 +00:00
|
|
|
extractVariableNames :: [Term] -> [Text]
|
|
|
|
|
extractVariableNames = mapMaybe extractVariableName where
|
|
|
|
|
extractVariableName :: Term -> Maybe Text
|
|
|
|
|
extractVariableName (Var name) = Just name
|
|
|
|
|
extractVariableName _ = Nothing
|
2026-01-23 18:12:47 +00:00
|
|
|
|
2026-01-21 17:11:13 +00:00
|
|
|
query :: NaiveDatabase -> Text -> Text
|
|
|
|
|
query db qText =
|
2026-01-27 17:27:18 +00:00
|
|
|
case parseDatalog qText of
|
2026-01-21 17:11:13 +00:00
|
|
|
Right (Query texts literals) -> "#NYI"
|
|
|
|
|
Right otherStatement -> throw $ NonQueryException qText otherStatement
|
|
|
|
|
Left ex -> throw $ CannotParseStatementException qText ex
|
|
|
|
|
|
|
|
|
|
data NaiveDatabaseException
|
2026-01-27 16:41:33 +00:00
|
|
|
= CannotParseStatementException Text (ParseErrorBundle Text Void)
|
|
|
|
|
| NonFactException Text Statement
|
|
|
|
|
| NonRuleException Text Statement
|
|
|
|
|
| NonQueryException Text Statement
|
|
|
|
|
| BadArityException Text Int
|
2026-01-27 18:40:05 +00:00
|
|
|
| VariableLookupException Text [Text]
|
2026-01-27 16:41:33 +00:00
|
|
|
| UnexpectedConstantException Constant
|
2026-01-21 17:11:13 +00:00
|
|
|
deriving (Show)
|
|
|
|
|
|
|
|
|
|
instance Exception NaiveDatabaseException
|