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-29 17:27:11 +00:00
|
|
|
{-# LANGUAGE BlockArguments #-}
|
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-30 10:27:26 +00:00
|
|
|
import Datalog.DatalogDB
|
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 17:27:11 +00:00
|
|
|
insertRelation :: NaiveDatabase -> Relation -> NaiveDatabase
|
|
|
|
|
insertRelation db relation =
|
|
|
|
|
db {
|
|
|
|
|
relations = Map.insert (_name relation) relation (relations db)
|
|
|
|
|
}
|
|
|
|
|
|
2026-01-30 10:47:27 +00:00
|
|
|
addRule :: (Literal, [Literal]) -> NaiveDatabase -> NaiveDatabase
|
|
|
|
|
addRule (ruleHead, body) db =
|
|
|
|
|
NaiveDatabase relationMap' constants' where
|
|
|
|
|
relationName = predName ruleHead
|
|
|
|
|
terms = arguments ruleHead
|
|
|
|
|
newArity = length terms
|
|
|
|
|
relation = lookupRelation0 relationName db newArity Set.empty
|
|
|
|
|
context = digestHead db relation ruleHead
|
|
|
|
|
context' = foldr digestBody context body
|
|
|
|
|
db' = _db context'
|
|
|
|
|
relationMap = relations db'
|
|
|
|
|
relation' = appendRule relation RelationRule {
|
|
|
|
|
headVariables = _variableNames context'
|
|
|
|
|
, bodyElements = toRuleBodyElement <$> _bodyConstraints context'
|
|
|
|
|
}
|
|
|
|
|
relationMap' = Map.insert relationName relation' relationMap
|
|
|
|
|
constants' = constants db'
|
|
|
|
|
|
2026-01-30 10:55:19 +00:00
|
|
|
addConstants :: NaiveDatabase -> Set Constant -> NaiveDatabase
|
|
|
|
|
addConstants db newConstants =
|
|
|
|
|
db {
|
|
|
|
|
constants = Set.union newConstants (constants db)
|
|
|
|
|
}
|
|
|
|
|
|
2026-01-30 10:47:27 +00:00
|
|
|
lookupRelation0 :: DatalogDB db => Text -> db -> Int -> Set [Constant] -> Relation
|
|
|
|
|
lookupRelation0 relationName db newArity tuples =
|
|
|
|
|
case lookupRelation db relationName of
|
|
|
|
|
Nothing -> Relation relationName newArity tuples []
|
|
|
|
|
Just relation ->
|
|
|
|
|
if _arity relation == newArity then
|
|
|
|
|
let newTuples = Set.union tuples $ _tuples relation
|
|
|
|
|
in relation { _tuples = newTuples }
|
|
|
|
|
else throw $ BadArityException relationName newArity
|
|
|
|
|
|
2026-01-29 17:27:11 +00:00
|
|
|
lookupRelation00 :: DatalogDB db =>
|
|
|
|
|
Text -> db -> Int -> (Relation -> Relation) -> db
|
|
|
|
|
lookupRelation00 relationName db newArity update =
|
|
|
|
|
insertRelation db (update newRelation)
|
|
|
|
|
where
|
|
|
|
|
newRelation = case lookupRelation db relationName of
|
|
|
|
|
Nothing -> Relation relationName newArity Set.empty []
|
|
|
|
|
Just relation ->
|
|
|
|
|
if _arity relation == newArity then
|
|
|
|
|
relation
|
|
|
|
|
else throw $ BadArityException relationName newArity
|
|
|
|
|
|
|
|
|
|
lookupRelation000:: DatalogDB db =>
|
|
|
|
|
Text -> db -> Int -> Set [Constant] -> (Relation -> Relation) -> db
|
|
|
|
|
lookupRelation000 relationName db newArity tuples update =
|
|
|
|
|
lookupRelation00 relationName db newArity \relation ->
|
|
|
|
|
update relation {
|
|
|
|
|
_tuples = Set.union tuples $ _tuples relation
|
|
|
|
|
}
|
2026-01-28 12:39:32 +00:00
|
|
|
|
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 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-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
|
|
|
|
|
|
|
|
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
|
2026-01-30 10:55:19 +00:00
|
|
|
-- db' = insertRelation db relation
|
2026-01-29 15:07:14 +00:00
|
|
|
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
|
|
|
|
|
|
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
|
|
|
|
|
|