module Persistence.Utils ( firstLibdir
                         , locIdOfDocument
                         , locIdOfOMSWithName
                         , locIdOfOMS
                         , locIdOfSentence
                         , locIdOfSymbol
                         , symbolDetails
                         , locIdOfMapping
                         , slugOfReasoner
                         , slugOfProver
                         , slugOfConsistencyChecker
                         , slugOfTranslation
                         , slugOfLanguageByName
                         , slugOfLogicMapping
                         , slugOfLogicMappingByName
                         , slugOfLogicInclusionByName
                         , slugOfLogicByName
                         , logicNameForDB
                         , logicNameForDBByName
                         , parameterize
                         , advisoryLocked
                         , coerceId
                         ) where

import Persistence.DBConfig

import qualified Persistence.Schema.Enums as Enums
import Persistence.Schema

import Common.Utils (replace, tryToStripPrefix)
import Driver.Options
import Persistence.Database
import Logic.Comorphism as Comorphism
import Logic.Logic as Logic
import Proofs.AbstractState
import Static.DevGraph (DGNodeLab (..))
import Static.DgUtils (showName)

import Control.Monad.IO.Class (MonadIO (..))
import Data.Char
import Data.Maybe
import qualified Data.Text as Text
import qualified Database.Esqueleto.Internal.Language as EIL
import qualified Database.Esqueleto.Internal.Sql as EIS
import Database.Persist hiding (replace)
import Database.Persist.Sql hiding (replace)

firstLibdir :: HetcatsOpts -> String
firstLibdir :: HetcatsOpts -> String
firstLibdir opts :: HetcatsOpts
opts =
  let libdir' :: String
libdir' = [String] -> String
forall a. [a] -> a
head ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> [String]
libdirs HetcatsOpts
opts
      libdir'' :: String
libdir'' = if String -> Char
forall a. [a] -> a
head String
libdir' Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '/' then "file://" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
libdir' else String
libdir'
  in  if String -> Char
forall a. [a] -> a
last String
libdir'' Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '/' then String
libdir'' else String
libdir'' String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/"

locIdOfDocument :: HetcatsOpts -> Maybe String -> String -> String
locIdOfDocument :: HetcatsOpts -> Maybe String -> String -> String
locIdOfDocument opts :: HetcatsOpts
opts locationM :: Maybe String
locationM displayName :: String
displayName =
  let fullLocation :: Maybe String
fullLocation =
        if (String -> Char) -> Maybe String -> Maybe Char
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Char
forall a. [a] -> a
head Maybe String
locationM Maybe Char -> Maybe Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char -> Maybe Char
forall a. a -> Maybe a
Just '/'
        then (String -> String) -> Maybe String -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ("file://" String -> String -> String
forall a. [a] -> [a] -> [a]
++) Maybe String
locationM
        else Maybe String
locationM
      base :: String
base = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
displayName Maybe String
fullLocation
  in  if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String] -> Bool) -> [String] -> Bool
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> [String]
libdirs HetcatsOpts
opts
      then String
base
      else String -> String -> String
tryToStripPrefix (HetcatsOpts -> String
firstLibdir HetcatsOpts
opts) String
base

locIdOfOMSWithName :: Entity LocIdBase -> String -> String
locIdOfOMSWithName :: Entity LocIdBase -> String -> String
locIdOfOMSWithName (Entity _ documentLocIdBaseValue :: LocIdBase
documentLocIdBaseValue) nodeName :: String
nodeName =
  case LocIdBase -> LocIdBaseKindType
locIdBaseKind LocIdBase
documentLocIdBaseValue of
    Enums.NativeDocument -> String
nodeName
    _ -> LocIdBase -> String
locIdBaseLocId LocIdBase
documentLocIdBaseValue
         String -> String -> String
forall a. [a] -> [a] -> [a]
++ "//oms/" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nodeName

locIdOfOMS :: Entity LocIdBase -> DGNodeLab -> String
locIdOfOMS :: Entity LocIdBase -> DGNodeLab -> String
locIdOfOMS documentEntity :: Entity LocIdBase
documentEntity nodeLabel :: DGNodeLab
nodeLabel =
  Entity LocIdBase -> String -> String
locIdOfOMSWithName Entity LocIdBase
documentEntity (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ NodeName -> String
showName (NodeName -> String) -> NodeName -> String
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> NodeName
dgn_name DGNodeLab
nodeLabel

locIdOfSentence :: Entity LocIdBase -> String -> String
locIdOfSentence :: Entity LocIdBase -> String -> String
locIdOfSentence (Entity _ omsLocIdBaseValue :: LocIdBase
omsLocIdBaseValue) name :: String
name =
  LocIdBase -> String
locIdBaseLocId LocIdBase
omsLocIdBaseValue String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/sentences/" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name

symbolDetails :: Logic.Logic lid sublogics
                   basic_spec sentence symb_items symb_map_items
                   sign morphism symbol raw_symbol proof_tree
              => Entity LocIdBase
              -> lid
              -> symbol
              -> (String, String, String, String)
symbolDetails :: Entity LocIdBase
-> lid -> symbol -> (String, String, String, String)
symbolDetails omsEntity :: Entity LocIdBase
omsEntity lid :: lid
lid symbol :: symbol
symbol =
  let name :: String
name = Id -> String
forall a. Show a => a -> String
show (Id -> String) -> Id -> String
forall a b. (a -> b) -> a -> b
$ lid -> symbol -> Id
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> Id
sym_name lid
lid symbol
symbol
      fullName :: String
fullName = lid -> symbol -> String
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> String
fullSymName lid
lid symbol
symbol
      symbolKind' :: String
symbolKind' = lid -> symbol -> String
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> String
symKind lid
lid symbol
symbol
      symbolKind :: String
symbolKind = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
symbolKind' then "symbol" else String
symbolKind'
  in  (Entity LocIdBase -> String -> String -> String
locIdOfSymbol Entity LocIdBase
omsEntity String
symbolKind String
name, String
name, String
fullName, String
symbolKind)

locIdOfSymbol :: Entity LocIdBase -> String -> String -> String
locIdOfSymbol :: Entity LocIdBase -> String -> String -> String
locIdOfSymbol (Entity _ omsLocIdBaseValue :: LocIdBase
omsLocIdBaseValue) symbolKind' :: String
symbolKind' name :: String
name =
  let symbolKind :: String
symbolKind = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
symbolKind' then "symbol" else String
symbolKind'
  in  LocIdBase -> String
locIdBaseLocId LocIdBase
omsLocIdBaseValue String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/symbols/" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
symbolKind String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name

locIdOfMapping :: Entity LocIdBase -> String -> String
locIdOfMapping :: Entity LocIdBase -> String -> String
locIdOfMapping (Entity _ documentLocIdBaseValue :: LocIdBase
documentLocIdBaseValue) displayName :: String
displayName =
  LocIdBase -> String
locIdBaseLocId LocIdBase
documentLocIdBaseValue String -> String -> String
forall a. [a] -> [a] -> [a]
++ "//mappings/" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
displayName

slugOfReasoner :: ProverOrConsChecker -> String
slugOfReasoner :: ProverOrConsChecker -> String
slugOfReasoner proverOrConsChecker :: ProverOrConsChecker
proverOrConsChecker =
  case ProverOrConsChecker
proverOrConsChecker of
    Prover gProver :: G_prover
gProver -> G_prover -> String
slugOfProver G_prover
gProver
    ConsChecker gConsChecker :: G_cons_checker
gConsChecker -> G_cons_checker -> String
slugOfConsistencyChecker G_cons_checker
gConsChecker

slugOfProver :: G_prover -> String
slugOfProver :: G_prover -> String
slugOfProver = String -> String
parameterize (String -> String) -> (G_prover -> String) -> G_prover -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. G_prover -> String
getProverName

slugOfConsistencyChecker :: G_cons_checker -> String
slugOfConsistencyChecker :: G_cons_checker -> String
slugOfConsistencyChecker = String -> String
parameterize (String -> String)
-> (G_cons_checker -> String) -> G_cons_checker -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. G_cons_checker -> String
getCcName

slugOfTranslation :: AnyComorphism -> String
slugOfTranslation :: AnyComorphism -> String
slugOfTranslation (Comorphism.Comorphism cid :: cid
cid) =
  String -> String
parameterize (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid

slugOfLanguageByName :: String -> String
slugOfLanguageByName :: String -> String
slugOfLanguageByName = String -> String
parameterize

slugOfLogicMapping :: AnyComorphism -> String
slugOfLogicMapping :: AnyComorphism -> String
slugOfLogicMapping (Comorphism.Comorphism cid :: cid
cid) =
  String -> String
slugOfLogicMappingByName (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid

slugOfLogicMappingByName :: String -> String
slugOfLogicMappingByName :: String -> String
slugOfLogicMappingByName = String -> String
parameterize

slugOfLogicInclusionByName :: String -> String
slugOfLogicInclusionByName :: String -> String
slugOfLogicInclusionByName =
  String -> String
parameterize (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  String -> String -> String -> String
forall a. Eq a => [a] -> [a] -> [a] -> [a]
replace "->" "-Arrow-" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  String -> String -> String -> String
forall a. Eq a => [a] -> [a] -> [a] -> [a]
replace "_" "-Sub-" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  String -> String -> String -> String
forall a. Eq a => [a] -> [a] -> [a] -> [a]
replace "." "-Dot-"

slugOfLogicByName :: String -> String
slugOfLogicByName :: String -> String
slugOfLogicByName = String -> String
parameterize

logicNameForDB :: Logic.Logic lid sublogics basic_spec sentence symb_items
                    symb_map_items sign morphism symbol raw_symbol proof_tree
               => lid -> sublogics -> String
logicNameForDB :: lid -> sublogics -> String
logicNameForDB lid :: lid
lid sublogic :: sublogics
sublogic =
  String -> String -> String
logicNameForDBByName (lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid) (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ sublogics -> String
forall l. SublogicName l => l -> String
sublogicName sublogics
sublogic

logicNameForDBByName :: String -> String -> String
logicNameForDBByName :: String -> String -> String
logicNameForDBByName languageName_ :: String
languageName_ logicName_ :: String
logicName_ =
  if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
logicName_ then String
languageName_ else String
logicName_


parameterize :: String -> String
parameterize :: String -> String
parameterize =
  String -> String
dropDashes (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Bool -> String -> String
mergeDashes Bool
False (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
replaceSpecialChars (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    String -> String -> String -> String
forall a. Eq a => [a] -> [a] -> [a] -> [a]
replace "=" "Eq" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower
  where
    replaceSpecialChars :: Char -> Char
    replaceSpecialChars :: Char -> Char
replaceSpecialChars c :: Char
c = if ('A' Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
c Bool -> Bool -> Bool
&& Char
c Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= 'Z') Bool -> Bool -> Bool
||
                               ('a' Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
c Bool -> Bool -> Bool
&& Char
c Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= 'z') Bool -> Bool -> Bool
||
                               ('0' Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
c Bool -> Bool -> Bool
&& Char
c Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= '9')
                            then Char
c
                            else '-'

    mergeDashes :: Bool -> [Char] -> [Char]
    mergeDashes :: Bool -> String -> String
mergeDashes _ [] = []
    mergeDashes previousWasDash :: Bool
previousWasDash (c :: Char
c:cs :: String
cs) =
      if Bool
previousWasDash
      then if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '-'
           then Bool -> String -> String
mergeDashes Bool
True String
cs
           else Char
c Char -> String -> String
forall a. a -> [a] -> [a]
: Bool -> String -> String
mergeDashes Bool
False String
cs
      else if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '-'
           then Char
c Char -> String -> String
forall a. a -> [a] -> [a]
: Bool -> String -> String
mergeDashes Bool
True String
cs
           else Char
c Char -> String -> String
forall a. a -> [a] -> [a]
: Bool -> String -> String
mergeDashes Bool
False String
cs

    dropDashes :: [Char] -> [Char]
    dropDashes :: String -> String
dropDashes = String -> String
forall a. [a] -> [a]
reverse (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '-') (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
forall a. [a] -> [a]
reverse (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '-')

advisoryLocked :: MonadIO m
               => HetcatsOpts -> String -> DBMonad m a -> DBMonad m a
advisoryLocked :: HetcatsOpts -> String -> DBMonad m a -> DBMonad m a
advisoryLocked opts :: HetcatsOpts
opts key :: String
key f :: DBMonad m a
f =
  case DBConfig -> Maybe String
adapter (DBConfig -> Maybe String) -> DBConfig -> Maybe String
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> DBConfig
databaseConfig HetcatsOpts
opts of
    Just "postgresql" -> do
      String -> DBMonad m [Single (Maybe Text)]
forall (m :: * -> *).
MonadIO m =>
String -> DBMonad m [Single (Maybe Text)]
advisoryLock String
key
      DBMonad m a
f
    _ -> DBMonad m a
f

advisoryLock :: MonadIO m => String -> DBMonad m [Single (Maybe Text.Text)]
advisoryLock :: String -> DBMonad m [Single (Maybe Text)]
advisoryLock key :: String
key = do
  let query :: Text
query = String -> Text
Text.pack (
        "SELECT pg_advisory_xact_lock("
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
advisoryLockKeyConvert
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ ");")
  Text -> [PersistValue] -> DBMonad m [Single (Maybe Text)]
forall a (m :: * -> *) backend.
(RawSql a, MonadIO m, BackendCompatible SqlBackend backend) =>
Text -> [PersistValue] -> ReaderT backend m [a]
rawSql Text
query [Text -> PersistValue
PersistText (Text -> PersistValue) -> Text -> PersistValue
forall a b. (a -> b) -> a -> b
$ String -> Text
Text.pack String
key]

advisoryLockKeyConvert :: String
advisoryLockKeyConvert :: String
advisoryLockKeyConvert =
  "(SELECT ('x' || lpad(md5(?),16,'0'))::bit(64)::bigint)"

-- This is used for Esqueleto JOIN statements with
-- "ON subclass.id = loc_id_bases.id"
-- Do NOT use this in other contexts.
-- Usage example:
--     selectedSymbols <- select $ from $
--       \(loc_id_bases `InnerJoin` symbols) -> do
--         on (coerceId (symbols ^. SymbolId) ==. loc_id_bases ^. LocIdBaseId)
--         return symbols
coerceId :: EIS.SqlExpr (EIL.Value a) -> EIS.SqlExpr (EIL.Value b)
coerceId :: SqlExpr (Value a) -> SqlExpr (Value b)
coerceId = SqlExpr (Value a) -> SqlExpr (Value b)
forall a b. SqlExpr (Value a) -> SqlExpr (Value b)
EIS.veryUnsafeCoerceSqlExprValue