{- |
Module      :  ./THF/Translate.hs
Description :  create legal THF mixfix identifier
Copyright   :  (c) A. Tsogias, DFKI Bremen 2011
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Alexis.Tsogias@dfki.de
Stability   :  provisional
Portability :  portable

translate 'Id' to THF Constant
-}

module THF.Translate where

import Common.Id
import Common.Result

import qualified Common.ProofUtils as CM (charMap)

import HasCASL.Builtin
import HasCASL.AsUtils

import THF.As as THFAs

import Data.Char
import qualified Data.Map as Map


mkTypesName :: THFAs.Constant -> THFAs.Name
mkTypesName :: Constant -> Name
mkTypesName c :: Constant
c = case Constant
c of
    A_Lower_Word w :: Token
w -> Constant -> Name
N_Atomic_Word (Constant -> Name) -> Constant -> Name
forall a b. (a -> b) -> a -> b
$ Token -> Constant
A_Lower_Word
                     (Token -> Constant) -> Token -> Constant
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId ("type_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
w)
    A_Single_Quoted s :: Token
s -> Constant -> Name
N_Atomic_Word (Constant -> Name) -> Constant -> Name
forall a b. (a -> b) -> a -> b
$ Token -> Constant
A_Single_Quoted
                        (Token -> Constant) -> Token -> Constant
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId ("type_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
s)

mkConstsName :: THFAs.Constant -> THFAs.Name
mkConstsName :: Constant -> Name
mkConstsName c :: Constant
c = case Constant
c of
    A_Lower_Word w :: Token
w -> Constant -> Name
N_Atomic_Word (Constant -> Name) -> Constant -> Name
forall a b. (a -> b) -> a -> b
$ Token -> Constant
A_Lower_Word
                     (Token -> Constant) -> Token -> Constant
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId ("const_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
w)
    A_Single_Quoted s :: Token
s -> Constant -> Name
N_Atomic_Word (Constant -> Name) -> Constant -> Name
forall a b. (a -> b) -> a -> b
$ Token -> Constant
A_Single_Quoted
                        (Token -> Constant) -> Token -> Constant
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId ("const_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
s)

mkDefName :: THFAs.Constant -> THFAs.Name
mkDefName :: Constant -> Name
mkDefName c :: Constant
c = case Constant
c of
    A_Lower_Word w :: Token
w -> Constant -> Name
N_Atomic_Word (Constant -> Name) -> Constant -> Name
forall a b. (a -> b) -> a -> b
$ Token -> Constant
A_Lower_Word
                     (Token -> Constant) -> Token -> Constant
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId ("def_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
w)
    A_Single_Quoted s :: Token
s -> Constant -> Name
N_Atomic_Word (Constant -> Name) -> Constant -> Name
forall a b. (a -> b) -> a -> b
$ Token -> Constant
A_Single_Quoted
                        (Token -> Constant) -> Token -> Constant
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId ("def_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
s)

transTypeId :: Id -> Result THFAs.Constant
transTypeId :: Id -> Result Constant
transTypeId id1 :: Id
id1 = case Id -> Map Id String -> Maybe String
forall a. Id -> Map Id a -> Maybe a
maybeElem Id
id1 Map Id String
preDefHCTypeIds of
    Just res :: String
res -> Constant -> Result Constant
forall (m :: * -> *) a. Monad m => a -> m a
return (Constant -> Result Constant) -> Constant -> Result Constant
forall a b. (a -> b) -> a -> b
$ String -> Constant
stringToConstant String
res
    Nothing -> case String -> Maybe String
transToTHFString (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Id -> String
forall a. Show a => a -> String
show Id
id1 of
        Just s :: String
s -> Constant -> Result Constant
forall (m :: * -> *) a. Monad m => a -> m a
return (Constant -> Result Constant)
-> (String -> Constant) -> String -> Result Constant
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> Constant
A_Lower_Word (Token -> Constant) -> (String -> Token) -> String -> Constant
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Token
mkSimpleId (String -> Result Constant) -> String -> Result Constant
forall a b. (a -> b) -> a -> b
$ "x_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
        Nothing -> String -> Range -> Result Constant
forall a. String -> Range -> Result a
fatal_error ("Unable to translate " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
id1 String -> String -> String
forall a. [a] -> [a] -> [a]
++
            " into a THF valide Constant.") Range
nullRange

transAssumpId :: Id -> Result THFAs.Constant
transAssumpId :: Id -> Result Constant
transAssumpId id1 :: Id
id1 = case Id -> Map Id String -> Maybe String
forall a. Id -> Map Id a -> Maybe a
maybeElem Id
id1 Map Id String
preDefHCAssumpIds of
    Just res :: String
res -> Constant -> Result Constant
forall (m :: * -> *) a. Monad m => a -> m a
return (Constant -> Result Constant) -> Constant -> Result Constant
forall a b. (a -> b) -> a -> b
$ String -> Constant
stringToConstant String
res
    Nothing -> case String -> Maybe String
transToTHFString (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Id -> String
forall a. Show a => a -> String
show Id
id1 of
        Just s :: String
s -> Constant -> Result Constant
forall (m :: * -> *) a. Monad m => a -> m a
return (Constant -> Result Constant) -> Constant -> Result Constant
forall a b. (a -> b) -> a -> b
$ String -> Constant
stringToConstant String
s
        Nothing -> String -> Range -> Result Constant
forall a. String -> Range -> Result a
fatal_error ("Unable to translate " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
id1 String -> String -> String
forall a. [a] -> [a] -> [a]
++
            " into a THF valide Constant.") Range
nullRange

transAssumpsId :: Id -> Int -> Result THFAs.Constant
transAssumpsId :: Id -> Int -> Result Constant
transAssumpsId id1 :: Id
id1 int :: Int
int = if Int
int Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 then Id -> Result Constant
transAssumpId Id
id1 else
    case String -> Maybe String
transToTHFString (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Id -> String
forall a. Show a => a -> String
show Id
id1 of
        Just s :: String
s -> Constant -> Result Constant
forall (m :: * -> *) a. Monad m => a -> m a
return (Constant -> Result Constant) -> Constant -> Result Constant
forall a b. (a -> b) -> a -> b
$ String -> Constant
stringToConstant (String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
int)
        Nothing -> String -> Range -> Result Constant
forall a. String -> Range -> Result a
fatal_error ("Unable to translate " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
id1 String -> String -> String
forall a. [a] -> [a] -> [a]
++
            " into a THF valide Constant.") Range
nullRange

stringToConstant :: String -> THFAs.Constant
stringToConstant :: String -> Constant
stringToConstant = Token -> Constant
A_Lower_Word (Token -> Constant) -> (String -> Token) -> String -> Constant
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Token
stringToLowerWord

stringToLowerWord :: String -> Token
stringToLowerWord :: String -> Token
stringToLowerWord = String -> Token
mkSimpleId (String -> Token) -> (String -> String) -> String -> Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \ s :: String
s -> case String
s of
   c :: Char
c : r :: String
r -> if Char -> Bool
isLower Char
c then String
s else 'x' Char -> String -> String
forall a. a -> [a] -> [a]
: Char
c Char -> String -> String
forall a. a -> [a] -> [a]
: String
r
   "" -> ""

stringToVariable :: String -> String
stringToVariable :: String -> String
stringToVariable s :: String
s = case String
s of
   c :: Char
c : r :: String
r -> if Char -> Bool
isUpper Char
c then String
s else let d :: Char
d = Char -> Char
toUpper Char
c in Char
d Char -> String -> String
forall a. a -> [a] -> [a]
: 'x' Char -> String -> String
forall a. a -> [a] -> [a]
: Char
d Char -> String -> String
forall a. a -> [a] -> [a]
: String
r
   "" -> ""

transVarId :: Id -> Result Token
transVarId :: Id -> Result Token
transVarId id1 :: Id
id1 = case String -> Maybe String
transToTHFString (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Id -> String
forall a. Show a => a -> String
show Id
id1 of
        Just s :: String
s -> Token -> Result Token
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> Result Token) -> Token -> Result Token
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId (String -> Token) -> String -> Token
forall a b. (a -> b) -> a -> b
$ String -> String
stringToVariable String
s
        Nothing -> String -> Range -> Result Token
forall a. String -> Range -> Result a
fatal_error ("Unable to translate " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
id1 String -> String -> String
forall a. [a] -> [a] -> [a]
++
            " into a THF valide Variable.") Range
nullRange

transToTHFString :: String -> Maybe String
transToTHFString :: String -> Maybe String
transToTHFString = Bool -> String -> Maybe String
transToTHFStringAux Bool
True

transToTHFStringAux :: Bool -> String -> Maybe String
transToTHFStringAux :: Bool -> String -> Maybe String
transToTHFStringAux first :: Bool
first s :: String
s = case String
s of
    "" -> String -> Maybe String
forall a. a -> Maybe a
Just ""
    c :: Char
c : rc :: String
rc -> let
      x :: Char
x = 'x' -- escape character
      rest :: Maybe String
rest = Bool -> String -> Maybe String
transToTHFStringAux Bool
False String
rc
      in
        if Char -> Bool
isTHFChar Char
c
        then if Bool
first Bool -> Bool -> Bool
&& Char -> Bool
isDigit Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
x then (String -> String) -> Maybe String -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char
x, Char
c] String -> String -> String
forall a. [a] -> [a] -> [a]
++) Maybe String
rest else
             (String -> String) -> Maybe String -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Char
c Char -> String -> String
forall a. a -> [a] -> [a]
:) Maybe String
rest
        else case Char -> Map Char String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Char
c Map Char String
charMap of
            Just res :: String
res -> (String -> String) -> Maybe String -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String
res String -> String -> String
forall a. [a] -> [a] -> [a]
++) Maybe String
rest
            Nothing -> Maybe String
forall a. Maybe a
Nothing

isTHFChar :: Char -> Bool
isTHFChar :: Char -> Bool
isTHFChar c :: Char
c = Char -> Bool
isAlphaNum Char
c Bool -> Bool -> Bool
&& Char -> Bool
isAscii Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '_'

isLowerTHFChar :: Char -> Bool
isLowerTHFChar :: Char -> Bool
isLowerTHFChar c :: Char
c = Char -> Bool
isLower Char
c Bool -> Bool -> Bool
&& Char -> Bool
isAscii Char
c

preDefHCTypeIds :: Map.Map Id String
preDefHCTypeIds :: Map Id String
preDefHCTypeIds = [(Id, String)] -> Map Id String
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
    [ (Id
logId, "hct" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
logId)
    , (Id
predTypeId, "hct" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
predTypeId)
    , (Id
unitTypeId, "hct" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
unitTypeId)
    , (Id
lazyTypeId, "hctLazy")
    , (Arrow -> Id
arrowId Arrow
FunArr, "hct__FunArr__")
    , (Arrow -> Id
arrowId Arrow
PFunArr, "hct__PFunArr__")
    , (Arrow -> Id
arrowId Arrow
ContFunArr, "hct__ContFunArr__")
    , (Arrow -> Id
arrowId Arrow
PContFunArr, "hct__PContFunArr__")
    , (Int -> Range -> Id
productId 2 Range
nullRange, "hct__X__")
    , (Int -> Range -> Id
productId 3 Range
nullRange, "hct__X__X__")
    , (Int -> Range -> Id
productId 4 Range
nullRange, "hct__X__X__X__")
    , (Int -> Range -> Id
productId 5 Range
nullRange, "hct__X__X__X__X__") ]

preDefHCAssumpIds :: Map.Map Id String
preDefHCAssumpIds :: Map Id String
preDefHCAssumpIds = [(Id, String)] -> Map Id String
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
    [ (Id
botId, "hcc" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
botId)
    , (Id
defId, "hcc" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
defId)
    , (Id
notId, "hcc" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
notId)
    , (Id
negId, "hccNeg__")
    , (Id
whenElse, "hcc" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
whenElse)
    , (Id
trueId, "hcc" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
trueId)
    , (Id
falseId, "hcc" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
falseId)
    , (Id
eqId, "hcc__Eq__")
    , (Id
exEq, "hcc__ExEq__")
    , (Id
resId, "hcc" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
resId)
    , (Id
andId, "hcc__And__")
    , (Id
orId, "hcc__Or__")
    , (Id
eqvId, "hcc__Eqv__")
    , (Id
implId, "hcc__Impl__")
    , (Id
infixIf, "hcc" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
infixIf) ]

maybeElem :: Id -> Map.Map Id a -> Maybe a
maybeElem :: Id -> Map Id a -> Maybe a
maybeElem id1 :: Id
id1 m :: Map Id a
m = Id -> [(Id, a)] -> Maybe a
forall a. Id -> [(Id, a)] -> Maybe a
helper Id
id1 (Map Id a -> [(Id, a)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Id a
m)
    where
        helper :: Id -> [(Id, a)] -> Maybe a
        helper :: Id -> [(Id, a)] -> Maybe a
helper _ [] = Maybe a
forall a. Maybe a
Nothing
        helper id2 :: Id
id2 ((eid :: Id
eid, ea :: a
ea) : r :: [(Id, a)]
r) =
            if Id -> Id -> Bool
myEqId Id
id2 Id
eid then a -> Maybe a
forall a. a -> Maybe a
Just a
ea else Id -> [(Id, a)] -> Maybe a
forall a. Id -> [(Id, a)] -> Maybe a
helper Id
id2 [(Id, a)]
r

myEqId :: Id -> Id -> Bool
myEqId :: Id -> Id -> Bool
myEqId (Id t1 :: [Token]
t1 c1 :: [Id]
c1 _) (Id t2 :: [Token]
t2 c2 :: [Id]
c2 _) = ([Token]
t1, [Id]
c1) ([Token], [Id]) -> ([Token], [Id]) -> Bool
forall a. Eq a => a -> a -> Bool
== ([Token]
t2, [Id]
c2)

-- | a separate Map speeds up lookup
charMap :: Map.Map Char String
charMap :: Map Char String
charMap = Char -> String -> Map Char String -> Map Char String
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert '\'' "Apostrophe"
  (Map Char String -> Map Char String)
-> (Map Char String -> Map Char String)
-> Map Char String
-> Map Char String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> String -> Map Char String -> Map Char String
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert '.' "Dot"
  (Map Char String -> Map Char String)
-> Map Char String -> Map Char String
forall a b. (a -> b) -> a -> b
$ (String -> String) -> Map Char String -> Map Char String
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map String -> String
stringToVariable Map Char String
CM.charMap
  -- this map is no longer injective