{- |
Module      :  ./CSL/Tools.hs
Description :  Abstract syntax for reduce
Copyright   :  (c) Dominik Dietrich, DFKI Bremen 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  dominik.dietrich@dfki.de
Stability   :  experimental
Portability :  portable

-}

module CSL.Tools where

import CSL.AS_BASIC_CSL
import CSL.ASUtils
import Common.Id
import Common.AS_Annotation as AS_Anno

negateFormula :: CMD -> CMD
negateFormula :: CMD -> CMD
negateFormula (Cmd s :: String
s exps :: [EXPRESSION]
exps) = String -> [EXPRESSION] -> CMD
Cmd "Not" [String -> [EXPRESSION] -> EXPRESSION
mkOp String
s [EXPRESSION]
exps]
negateFormula _ = String -> CMD
forall a. HasCallStack => String -> a
error "negateFormula: not implemented" -- TODO: implement this

getAtoms :: EXPRESSION -> [String]
getAtoms :: EXPRESSION -> [String]
getAtoms e :: EXPRESSION
e =
    case EXPRESSION
e of
      Var tk :: Token
tk -> ["var:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Token -> String
tokStr Token
tk]
      Op s :: OPID
s _ el :: [EXPRESSION]
el _ -> ("op:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ OPID -> String
forall a. Show a => a -> String
show OPID
s) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (EXPRESSION -> [String]) -> [EXPRESSION] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap EXPRESSION -> [String]
getAtoms [EXPRESSION]
el
      List el :: [EXPRESSION]
el _ -> "list" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (EXPRESSION -> [String]) -> [EXPRESSION] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap EXPRESSION -> [String]
getAtoms [EXPRESSION]
el
      Int _ _ -> ["int"]
      Rat _ _ -> ["dbl"]
      Interval {} -> ["intv"]

getCmdAtoms :: CMD -> [String]
getCmdAtoms :: CMD -> [String]
getCmdAtoms c :: CMD
c =
    case CMD
c of
      Cmd s :: String
s el :: [EXPRESSION]
el -> ("cmd:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (EXPRESSION -> [String]) -> [EXPRESSION] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap EXPRESSION -> [String]
getAtoms [EXPRESSION]
el
      Repeat e :: EXPRESSION
e cl :: [CMD]
cl -> "repeat" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (EXPRESSION -> [String]
getAtoms EXPRESSION
e [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (CMD -> [String]) -> [CMD] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CMD -> [String]
getCmdAtoms [CMD]
cl)
      _ -> [] -- TODO: implement this


getBSAtoms :: BASIC_SPEC -> [String]
getBSAtoms :: BASIC_SPEC -> [String]
getBSAtoms (Basic_spec l :: [Annoted BASIC_ITEM]
l) = (Annoted BASIC_ITEM -> [String])
-> [Annoted BASIC_ITEM] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (BASIC_ITEM -> [String]
f (BASIC_ITEM -> [String])
-> (Annoted BASIC_ITEM -> BASIC_ITEM)
-> Annoted BASIC_ITEM
-> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted BASIC_ITEM -> BASIC_ITEM
forall a. Annoted a -> a
AS_Anno.item) [Annoted BASIC_ITEM]
l
    where f :: BASIC_ITEM -> [String]
f (Op_decl _) = []
          f (Axiom_item ac :: Annoted CMD
ac) = CMD -> [String]
getCmdAtoms (CMD -> [String]) -> CMD -> [String]
forall a b. (a -> b) -> a -> b
$ Annoted CMD -> CMD
forall a. Annoted a -> a
AS_Anno.item Annoted CMD
ac
          f _ = [] -- TODO: implement this