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-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-27 17:55:19 +00:00
|
|
|
import GHC.TypeError (ErrorMessage(Text))
|
2026-01-21 11:24:30 +00:00
|
|
|
|
2026-01-27 16:41:33 +00:00
|
|
|
data Value
|
|
|
|
|
= ValueInt Int
|
|
|
|
|
| ValueSymbol String
|
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-21 17:11:13 +00:00
|
|
|
|
2026-01-27 16:41:33 +00:00
|
|
|
data RuleElement -- entry occurring in a head or body relation - constant or variable
|
|
|
|
|
= RuleElementConstant Constant
|
|
|
|
|
| RuleElementVariable Text
|
2026-01-22 18:00:52 +00:00
|
|
|
deriving (Show, Eq)
|
|
|
|
|
|
2026-01-27 16:41:33 +00:00
|
|
|
data RuleBodyElement = RuleBodyElement
|
|
|
|
|
{ _subRelationId :: RelationId
|
|
|
|
|
, _ruleElements :: [RuleElement]
|
|
|
|
|
}
|
|
|
|
|
deriving (Show, Eq)
|
2026-01-27 12:41:23 +00:00
|
|
|
|
2026-01-27 16:41:33 +00:00
|
|
|
data RelationRule = RelationRule
|
|
|
|
|
{ headVariables :: [Text]
|
|
|
|
|
, bodyElements :: [RuleBodyElement]
|
|
|
|
|
}
|
|
|
|
|
deriving (Show, Eq)
|
2026-01-22 18:00:52 +00:00
|
|
|
|
2026-01-27 16:41:33 +00:00
|
|
|
data Relation = Relation
|
|
|
|
|
{ _name :: RelationId
|
|
|
|
|
, _arity :: Int
|
|
|
|
|
, _tuples :: Set [Constant]
|
|
|
|
|
, _rules :: [RelationRule]
|
|
|
|
|
}
|
|
|
|
|
deriving (Show, Eq)
|
2026-01-21 18:01:06 +00:00
|
|
|
|
2026-01-22 10:57:11 +00:00
|
|
|
-- Our constants will be the terms of the Datalog grammar - ints/variables/symbols
|
|
|
|
|
type Constant = Term
|
|
|
|
|
type RelationId = Text
|
|
|
|
|
|
2026-01-21 17:11:13 +00:00
|
|
|
emptyDB :: NaiveDatabase
|
2026-01-27 16:41:33 +00:00
|
|
|
emptyDB =
|
|
|
|
|
NaiveDatabase
|
|
|
|
|
{ relations = Map.empty
|
|
|
|
|
, constants = Set.empty -- the Herbrand universe
|
|
|
|
|
}
|
2026-01-21 17:11:13 +00:00
|
|
|
|
|
|
|
|
withFacts :: [Text] -> NaiveDatabase
|
|
|
|
|
withFacts facts =
|
2026-01-27 16:41:33 +00:00
|
|
|
foldl addFact emptyDB (extractFact <$> facts)
|
|
|
|
|
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
|
|
|
|
|
addFact :: NaiveDatabase -> Literal -> NaiveDatabase
|
|
|
|
|
addFact (NaiveDatabase relationMap constantSet) (Literal neg relationName terms) =
|
|
|
|
|
NaiveDatabase newRelationMap newConstantSet
|
|
|
|
|
where
|
|
|
|
|
newArity = length terms
|
|
|
|
|
newRelation = lookupRelation relationName relationMap newArity (Set.singleton terms)
|
|
|
|
|
newRelationMap = Map.insert relationName newRelation relationMap
|
|
|
|
|
newConstantSet = Set.union constantSet $ Set.fromList terms
|
2026-01-23 18:12:47 +00:00
|
|
|
|
2026-01-26 18:28:15 +00:00
|
|
|
lookupRelation :: RelationId -> Map RelationId Relation -> Int -> Set [Term] -> Relation
|
|
|
|
|
lookupRelation relationName relationMap newArity tuples =
|
2026-01-27 16:41:33 +00:00
|
|
|
case Map.lookup relationName relationMap of
|
|
|
|
|
Nothing -> Relation relationName newArity tuples []
|
|
|
|
|
Just relation ->
|
2026-01-27 17:33:44 +00:00
|
|
|
if _arity relation == newArity then
|
2026-01-27 16:41:33 +00:00
|
|
|
let newTuples = Set.union tuples $ _tuples relation
|
|
|
|
|
in Relation relationName newArity newTuples []
|
|
|
|
|
else throw $ BadArityException relationName newArity
|
|
|
|
|
|
|
|
|
|
data ConstraintElement -- entry occurring in a rule body constraint - constant or variable index
|
|
|
|
|
= ConstraintElementConstant Constant
|
|
|
|
|
| ConstraintElementIndex Int
|
2026-01-23 18:12:47 +00:00
|
|
|
deriving (Show, Eq)
|
|
|
|
|
|
2026-01-27 16:41:33 +00:00
|
|
|
data BodyConstraint = BodyConstraint
|
|
|
|
|
{ _relation :: Relation
|
|
|
|
|
, _elements :: [ConstraintElement]
|
|
|
|
|
}
|
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
|
|
|
|
|
|
|
|
maybeConstant :: RuleElement -> Maybe Constant
|
|
|
|
|
maybeConstant (RuleElementConstant constant) = Just constant
|
|
|
|
|
maybeConstant _ = Nothing
|
2026-01-21 17:11:13 +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
|
|
|
|
|
extractRule :: Text -> (Literal, [Literal])
|
|
|
|
|
extractRule ruleText =
|
2026-01-27 17:27:18 +00:00
|
|
|
case parseDatalog ruleText of
|
2026-01-27 16:41:33 +00:00
|
|
|
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
|
2026-01-27 17:55:19 +00:00
|
|
|
, _variableNames = extractVariableNames terms
|
2026-01-27 17:27:18 +00:00
|
|
|
, _headEntries = variables'
|
2026-01-27 16:41:33 +00:00
|
|
|
, _bodyConstraints = []
|
|
|
|
|
, _db = NaiveDatabase relationMap' constants'
|
|
|
|
|
}
|
|
|
|
|
where
|
|
|
|
|
relationMap :: Map RelationId Relation = relations db
|
|
|
|
|
relationMap' = Map.insert relationName relation relationMap
|
|
|
|
|
extraVariables = toElement <$> terms
|
|
|
|
|
variables' = nub extraVariables
|
2026-01-27 17:33:44 +00:00
|
|
|
extraConstants = mapMaybe maybeConstant variables'
|
2026-01-27 16:41:33 +00:00
|
|
|
constants' = Set.union (constants db) $ Set.fromList extraConstants
|
|
|
|
|
digestBody :: RuleContext -> Literal -> RuleContext
|
|
|
|
|
digestBody context (Literal neg subRelationName terms) =
|
|
|
|
|
RuleContext
|
|
|
|
|
{ __relation = relation
|
2026-01-27 17:55:19 +00:00
|
|
|
, _variableNames = _variableNames context
|
2026-01-27 17:27:18 +00:00
|
|
|
, _headEntries = variables'
|
2026-01-27 16:41:33 +00:00
|
|
|
, _bodyConstraints = constraints'
|
|
|
|
|
, _db = NaiveDatabase relationMap' constants'
|
|
|
|
|
}
|
|
|
|
|
where
|
|
|
|
|
relation = __relation context
|
|
|
|
|
newArity = length terms
|
|
|
|
|
subRelation = lookupRelation subRelationName relationMap newArity Set.empty
|
|
|
|
|
relationMap :: Map RelationId Relation = relations (_db context)
|
|
|
|
|
relationMap' = Map.insert subRelationName subRelation relationMap
|
|
|
|
|
extraVariables = toElement <$> terms
|
2026-01-27 17:27:18 +00:00
|
|
|
extraConstants = mapMaybe maybeConstant extraVariables
|
|
|
|
|
variables' = nub $ _headEntries context ++ extraVariables
|
2026-01-27 16:41:33 +00:00
|
|
|
constants' = Set.union (constants (_db context)) $ Set.fromList extraConstants
|
|
|
|
|
constraints = _bodyConstraints context
|
|
|
|
|
newConstraint = BodyConstraint subRelation (toConstraint <$> terms)
|
|
|
|
|
constraints' = constraints ++ [newConstraint]
|
|
|
|
|
varIndex :: Text -> Int
|
|
|
|
|
varIndex name =
|
|
|
|
|
case elemIndex (RuleElementVariable name) variables' of
|
|
|
|
|
Just index -> index
|
|
|
|
|
Nothing -> throw $ VariableLookupException name variables'
|
|
|
|
|
toConstraint :: Term -> ConstraintElement
|
|
|
|
|
toConstraint (Var name) = ConstraintElementIndex (varIndex name)
|
|
|
|
|
toConstraint constant = ConstraintElementConstant constant
|
|
|
|
|
addRule :: (Literal, [Literal]) -> NaiveDatabase ->NaiveDatabase
|
|
|
|
|
addRule (ruleHead, body) db =
|
|
|
|
|
NaiveDatabase newRelationMap constants'
|
|
|
|
|
where
|
|
|
|
|
relationName = predName ruleHead
|
|
|
|
|
terms = arguments ruleHead
|
|
|
|
|
newArity = length terms
|
|
|
|
|
relation = lookupRelation relationName (relations db) newArity Set.empty
|
2026-01-27 18:01:30 +00:00
|
|
|
context = digestHead db relation ruleHead
|
|
|
|
|
context' = foldl digestBody context body
|
|
|
|
|
db' = _db context'
|
2026-01-27 16:41:33 +00:00
|
|
|
relationMap = relations db'
|
2026-01-27 18:01:30 +00:00
|
|
|
variables' = _headEntries context'
|
2026-01-27 16:41:33 +00:00
|
|
|
extractVarName :: RuleElement -> Maybe Text
|
|
|
|
|
extractVarName (RuleElementVariable varName) = Just varName
|
|
|
|
|
extractVarName (RuleElementConstant constant) = Nothing
|
|
|
|
|
newRule =
|
|
|
|
|
RelationRule
|
2026-01-27 17:27:18 +00:00
|
|
|
{ headVariables = mapMaybe extractVarName variables'
|
2026-01-27 18:01:30 +00:00
|
|
|
, bodyElements = fromBodyConstraint <$> _bodyConstraints context'
|
2026-01-27 16:41:33 +00:00
|
|
|
}
|
|
|
|
|
where
|
|
|
|
|
fromBodyConstraint :: BodyConstraint -> RuleBodyElement
|
|
|
|
|
fromBodyConstraint (BodyConstraint subRelation elements) =
|
|
|
|
|
RuleBodyElement
|
|
|
|
|
{ _subRelationId = _name subRelation
|
|
|
|
|
, _ruleElements = toRuleElement <$> elements
|
|
|
|
|
}
|
|
|
|
|
toRuleElement :: ConstraintElement -> RuleElement
|
|
|
|
|
toRuleElement (ConstraintElementConstant constant) = RuleElementConstant constant
|
|
|
|
|
toRuleElement (ConstraintElementIndex index) = variables' !! index
|
|
|
|
|
relation' =
|
|
|
|
|
Relation
|
|
|
|
|
{ _name = _name relation
|
|
|
|
|
, _arity = newArity
|
|
|
|
|
, _tuples = _tuples relation
|
2026-01-27 17:27:18 +00:00
|
|
|
, _rules = newRule : _rules relation
|
2026-01-23 18:12:47 +00:00
|
|
|
}
|
2026-01-27 16:41:33 +00:00
|
|
|
newRelationMap = Map.insert relationName relation' relationMap
|
|
|
|
|
constants' = constants db'
|
|
|
|
|
toElement :: Term -> RuleElement
|
|
|
|
|
toElement (Var name) = RuleElementVariable name
|
|
|
|
|
toElement constant = RuleElementConstant constant
|
2026-01-27 17:55:19 +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
|
|
|
|
|
| VariableLookupException Text [RuleElement]
|
|
|
|
|
| UnexpectedConstantException Constant
|
2026-01-21 17:11:13 +00:00
|
|
|
deriving (Show)
|
|
|
|
|
|
|
|
|
|
instance Exception NaiveDatabaseException
|