{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications  #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

{-# HLINT ignore "Redundant flip" #-}
{-# LANGUAGE ImportQualifiedPost #-}
module Datalog.NaiveDatabase where

import Data.Map (Map)
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Text (Text)
import qualified Data.Text as T
import Datalog.DatalogParser(parseDatalog, Literal(Literal), Statement(..), Term, Head (HeadSingle))
import qualified Data.Map as Map
import Text.Megaparsec (ParseErrorBundle)
import Data.Void
import Control.Exception (Exception)
import Control.Exception.Base

data Value =
  ValueInt Int |
  ValueSymbol String

data NaiveDatabase = NaiveDatabase {
  relations :: Map RelationId Relation,
  constants :: Set Constant
}

data BodyEntry = -- entry occurring in a head or body relation - constant or variable
  BodyEntryConstant Constant |
  BodyEntryVariable Text
  deriving (Show, Eq)

data RelationRule = RelationRule {
  headVariables :: [BodyEntry],
  body :: [(Relation, [BodyEntry])]
} deriving (Show, Eq)

data Relation = Relation {
  arity :: Int,
  tuples :: Set [Constant],
  rules :: [RelationRule]
} deriving (Show, Eq)

-- newtype RelationId = RelationId Text
--   deriving (Eq, Ord, Show)

-- Our constants will be the terms of the Datalog grammar - ints/variables/symbols
type Constant = Term
type RelationId = Text

-- newtype Constant = Constant Text
--   deriving (Eq, Ord, Show)

emptyDB :: NaiveDatabase
emptyDB = NaiveDatabase {
  relations = Map.empty,
  constants = Set.empty   -- the Herbrand universe
}

withFacts :: [Text] -> NaiveDatabase
withFacts facts =
  foldl addFact emptyDB (extractFact <$> facts) where
    extractFact:: Text -> Literal
    extractFact factText =
      case (parseDatalog factText) of
        Right (Fact fact) -> fact
        Right otherStatement -> throw $ NonFactException factText otherStatement
        Left ex -> throw $ CannotParseStatementException factText ex
    addFact :: NaiveDatabase -> Literal -> NaiveDatabase
    addFact (NaiveDatabase relations constants) (Literal neg relationName terms) =
      NaiveDatabase newRelations newConstants where
        newArity = length terms
        newRelation =
          case Map.lookup relationName relations of
            Nothing -> Relation (length terms) (Set.singleton terms) []
            Just relation ->
              if (arity relation == newArity)
                then Relation (length terms) (Set.singleton terms) []
                else throw $ BadArityException relationName newArity
        newRelations = Map.insert relationName newRelation relations 
        newConstants = Set.union constants $ Set.fromList terms

withFactsAndRules :: [Text] -> [Text] -> NaiveDatabase
withFactsAndRules facts rules =
  foldl addRule (withFacts facts) (extractRule <$> rules) where
    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
    addRule :: NaiveDatabase -> (Literal, [Literal]) -> NaiveDatabase
    addRule (NaiveDatabase relations constants) ((Literal neg relationName terms), body) =
      NaiveDatabase newRelations newConstants where
        newRelations = relations 
        newConstants = constants
 
query :: NaiveDatabase -> Text -> Text
query db qText =
  case (parseDatalog qText) of
    Right (Query texts literals) -> "#NYI"
    Right otherStatement -> throw $ NonQueryException qText otherStatement
    Left ex -> throw $ CannotParseStatementException qText ex

data NaiveDatabaseException
  = CannotParseStatementException Text (ParseErrorBundle Text Void) |
    NonFactException Text Statement |
    NonRuleException Text Statement |
    NonQueryException Text Statement |
    BadArityException Text Int
  deriving (Show)

instance Exception NaiveDatabaseException