{- |
Module      :  ./TIP/Utils.hs
Description :  utility functions for dealing with TIP objects
Copyright   :  (c) Tom Kranz 2022
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :
Stability   :  experimental
Portability :  non-portable (imports TIP.AbsTIP)

Extracting/wrapping names and attributes from/in TIP objects, with quoting.
-}
module TIP.Utils where

import TIP.AbsTIP
import TIP.PrintTIP (printTree)
import Data.Maybe
import Data.Char
import Data.Set hiding (filter,map)
import Data.Function

printTIP :: Start -> String
printTIP :: Start -> String
printTIP (Start ds :: [Decl]
ds) = [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Decl -> String) -> [Decl] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\d :: Decl
d -> "("String -> String -> String
forall a. [a] -> [a] -> [a]
++Decl -> String
forall a. Print a => a -> String
printTree Decl
dString -> String -> String
forall a. [a] -> [a] -> [a]
++")") [Decl]
ds

unquotedLaterSymbols :: Set Char
unquotedLaterSymbols :: Set Char
unquotedLaterSymbols = String -> Set Char
forall a. Ord a => [a] -> Set a
fromList "~!@$%^&*_-+=<>.?/"

isUnquotedLaterSymbol :: Char -> Bool
isUnquotedLaterSymbol :: Char -> Bool
isUnquotedLaterSymbol = ((Char -> Set Char -> Bool) -> Set Char -> Char -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Char -> Set Char -> Bool
forall a. Ord a => a -> Set a -> Bool
member) Set Char
unquotedLaterSymbols

unquotedInitialSymbols :: Set Char
unquotedInitialSymbols :: Set Char
unquotedInitialSymbols = String -> Set Char
forall a. Ord a => [a] -> Set a
fromList "~!@$%^&*_+=<>.?/"

isUnquotedInitialSymbol :: Char -> Bool
isUnquotedInitialSymbol :: Char -> Bool
isUnquotedInitialSymbol = ((Char -> Set Char -> Bool) -> Set Char -> Char -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Char -> Set Char -> Bool
forall a. Ord a => a -> Set a -> Bool
member) Set Char
unquotedInitialSymbols

anyOf :: a -> [a -> Bool] -> Bool
anyOf :: a -> [a -> Bool] -> Bool
anyOf c :: a
c = ((a -> Bool) -> Bool) -> [a -> Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (a
c a -> (a -> Bool) -> Bool
forall a b. a -> (a -> b) -> b
&)

getFormulaName :: Decl -> Maybe String
getFormulaName :: Decl -> Maybe String
getFormulaName (Formula _ attrs :: [Attr]
attrs _) = [String] -> Maybe String
forall a. [a] -> Maybe a
listToMaybe ([String] -> Maybe String) -> [String] -> Maybe String
forall a b. (a -> b) -> a -> b
$ String -> [Attr] -> [String]
getAttrValues ":axiom" [Attr]
attrs
getFormulaName (FormulaPar _ attrs :: [Attr]
attrs _ _) = [String] -> Maybe String
forall a. [a] -> Maybe a
listToMaybe ([String] -> Maybe String) -> [String] -> Maybe String
forall a b. (a -> b) -> a -> b
$ String -> [Attr] -> [String]
getAttrValues ":axiom" [Attr]
attrs
getFormulaName _ = Maybe String
forall a. Maybe a
Nothing

getAttrValues :: String -> [Attr] -> [String]
getAttrValues :: String -> [Attr] -> [String]
getAttrValues skey :: String
skey = (Attr -> Maybe String) -> [Attr] -> [String]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((Attr -> Maybe String) -> [Attr] -> [String])
-> (Attr -> Maybe String) -> [Attr] -> [String]
forall a b. (a -> b) -> a -> b
$ String -> Attr -> Maybe String
getAttrValue String
skey

getAttrValue :: String -> Attr -> Maybe String
getAttrValue :: String -> Attr -> Maybe String
getAttrValue skey :: String
skey attr :: Attr
attr
  | (Value (Keyword akey :: String
akey) sym :: Symbol
sym) <- Attr
attr
  , (String
akey String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
skey)
  = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Symbol -> String
fromSymbol Symbol
sym
  | Bool
otherwise = Maybe String
forall a. Maybe a
Nothing

addAttr :: Decl -> (String, Maybe String) -> Decl
addAttr :: Decl -> (String, Maybe String) -> Decl
addAttr (Formula assertion :: Assertion
assertion attrs :: [Attr]
attrs expr :: Expr
expr) kv :: (String, Maybe String)
kv = Assertion -> [Attr] -> Expr -> Decl
Formula Assertion
assertion ((String, Maybe String) -> Attr
toAttr (String, Maybe String)
kv Attr -> [Attr] -> [Attr]
forall a. a -> [a] -> [a]
: [Attr]
attrs) Expr
expr
addAttr (FormulaPar assertion :: Assertion
assertion attrs :: [Attr]
attrs par :: Par
par expr :: Expr
expr) kv :: (String, Maybe String)
kv = Assertion -> [Attr] -> Par -> Expr -> Decl
FormulaPar Assertion
assertion ((String, Maybe String) -> Attr
toAttr (String, Maybe String)
kv Attr -> [Attr] -> [Attr]
forall a. a -> [a] -> [a]
: [Attr]
attrs) Par
par Expr
expr
addAttr other :: Decl
other _ = Decl
other

stripAttrs :: Decl -> Decl
stripAttrs :: Decl -> Decl
stripAttrs (Formula assertion :: Assertion
assertion _ expr :: Expr
expr) = Assertion -> [Attr] -> Expr -> Decl
Formula Assertion
assertion [] Expr
expr
stripAttrs (FormulaPar assertion :: Assertion
assertion _ par :: Par
par expr :: Expr
expr) = Assertion -> [Attr] -> Par -> Expr -> Decl
FormulaPar Assertion
assertion [] Par
par Expr
expr
stripAttrs other :: Decl
other = Decl
other

declareData :: [(DatatypeName, Datatype)] -> [Decl]
declareData :: [(DatatypeName, Datatype)] -> [Decl]
declareData [] = []
declareData ((DatatypeName n :: AttrSymbol
n _,t :: Datatype
t):[]) = [AttrSymbol -> Datatype -> Decl
DeclareDatatype AttrSymbol
n Datatype
t]
declareData plural :: [(DatatypeName, Datatype)]
plural = [[DatatypeName] -> [Datatype] -> Decl
DeclareDatatypes (((DatatypeName, Datatype) -> DatatypeName)
-> [(DatatypeName, Datatype)] -> [DatatypeName]
forall a b. (a -> b) -> [a] -> [b]
map (DatatypeName, Datatype) -> DatatypeName
forall a b. (a, b) -> a
fst [(DatatypeName, Datatype)]
plural) (((DatatypeName, Datatype) -> Datatype)
-> [(DatatypeName, Datatype)] -> [Datatype]
forall a b. (a -> b) -> [a] -> [b]
map (DatatypeName, Datatype) -> Datatype
forall a b. (a, b) -> b
snd [(DatatypeName, Datatype)]
plural)]

singularizeDatas :: Decl -> [Decl]
singularizeDatas :: Decl -> [Decl]
singularizeDatas (DeclareDatatypes dns :: [DatatypeName]
dns dts :: [Datatype]
dts) = ((DatatypeName, Datatype) -> [Decl])
-> [(DatatypeName, Datatype)] -> [Decl]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([(DatatypeName, Datatype)] -> [Decl]
declareData([(DatatypeName, Datatype)] -> [Decl])
-> ((DatatypeName, Datatype) -> [(DatatypeName, Datatype)])
-> (DatatypeName, Datatype)
-> [Decl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.((DatatypeName, Datatype)
-> [(DatatypeName, Datatype)] -> [(DatatypeName, Datatype)]
forall a. a -> [a] -> [a]
:[])) ([(DatatypeName, Datatype)] -> [Decl])
-> [(DatatypeName, Datatype)] -> [Decl]
forall a b. (a -> b) -> a -> b
$ [DatatypeName] -> [Datatype] -> [(DatatypeName, Datatype)]
forall a b. [a] -> [b] -> [(a, b)]
zip [DatatypeName]
dns [Datatype]
dts
singularizeDatas d :: Decl
d = Decl
dDecl -> [Decl] -> [Decl]
forall a. a -> [a] -> [a]
:[]

fromSymbol :: Symbol -> String
fromSymbol :: Symbol -> String
fromSymbol (Unquoted (UnquotedSymbol (_, sym :: String
sym))) = String
sym
fromSymbol (Quoted (QuotedSymbol (_, sym :: String
sym))) = String -> String
unquoteSymbolChars (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. [a] -> [a]
init (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. [a] -> [a]
tail String
sym

toAttr :: (String, Maybe String) -> Attr
toAttr :: (String, Maybe String) -> Attr
toAttr (key :: String
key, mValue :: Maybe String
mValue)
  | Just value :: String
value <- Maybe String
mValue = Keyword -> Symbol -> Attr
Value Keyword
kw (Symbol -> Attr) -> Symbol -> Attr
forall a b. (a -> b) -> a -> b
$ String -> Symbol
toSymbol String
value
  | Bool
otherwise = Keyword -> Attr
NoValue Keyword
kw
    where kw :: Keyword
kw = (String -> Keyword
Keyword (String -> Keyword) -> String -> Keyword
forall a b. (a -> b) -> a -> b
$ ':' Char -> String -> String
forall a. a -> [a] -> [a]
: (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
filter (((Char -> [Char -> Bool] -> Bool) -> [Char -> Bool] -> Char -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Char -> [Char -> Bool] -> Bool
forall a. a -> [a -> Bool] -> Bool
anyOf) [Char -> Bool
isLetter,Char -> Bool
isDigit,(Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
=='-')]) String
key)

quoteSymbolChar :: Char -> String
quoteSymbolChar :: Char -> String
quoteSymbolChar '\\' = "\\\\"
quoteSymbolChar '|' = "\\|"
quoteSymbolChar c :: Char
c = [Char
c]

unquoteSymbolChars :: String -> String
unquoteSymbolChars :: String -> String
unquoteSymbolChars ('\\' : c :: Char
c : cs :: String
cs) = Char
c Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
unquoteSymbolChars String
cs
unquoteSymbolChars (c :: Char
c : cs :: String
cs) = Char
c Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
unquoteSymbolChars String
cs
unquoteSymbolChars [] = []

toSymbol :: String -> Symbol
toSymbol :: String -> Symbol
toSymbol s :: String
s
  | (h :: Char
h : t :: String
t) <- String
s
  , Char -> [Char -> Bool] -> Bool
forall a. a -> [a -> Bool] -> Bool
anyOf Char
h [Char -> Bool
isUnquotedInitialSymbol, Char -> Bool
isLetter]
  , (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (((Char -> [Char -> Bool] -> Bool) -> [Char -> Bool] -> Char -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Char -> [Char -> Bool] -> Bool
forall a. a -> [a -> Bool] -> Bool
anyOf) [Char -> Bool
isUnquotedLaterSymbol, Char -> Bool
isDigit, Char -> Bool
isLetter]) String
t
  = UnquotedSymbol -> Symbol
Unquoted (UnquotedSymbol -> Symbol) -> UnquotedSymbol -> Symbol
forall a b. (a -> b) -> a -> b
$ ((Int, Int), String) -> UnquotedSymbol
UnquotedSymbol ((0,0),String
s)
  | Bool
otherwise
  = QuotedSymbol -> Symbol
Quoted (QuotedSymbol -> Symbol) -> QuotedSymbol -> Symbol
forall a b. (a -> b) -> a -> b
$ ((Int, Int), String) -> QuotedSymbol
QuotedSymbol ((0,0),"|" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Char -> String) -> String -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
quoteSymbolChar String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "|")