{-# LANGUAGE ExistentialQuantification #-}
-- Copyright 2022 United States Government as represented by the Administrator
-- of the National Aeronautics and Space Administration. All Rights Reserved.
--
-- Disclaimers
--
-- Licensed under the Apache License, Version 2.0 (the "License"); you may
-- not use this file except in compliance with the License. You may obtain a
-- copy of the License at
--
--      https://www.apache.org/licenses/LICENSE-2.0
--
-- Unless required by applicable law or agreed to in writing, software
-- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
-- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
-- License for the specific language governing permissions and limitations
-- under the License.
--
-- | Abstraction for expressions used in specifications.
module Data.ExprPair
    ( ExprPair(..)
    , ExprPairT(..)
    , exprPair
    , exprPairShow
    )
  where

-- External imports
import qualified Language.Lustre.AbsLustre     as Lustre
import qualified Language.Lustre.ParLustre     as Lustre (myLexer, pBoolSpec)
import qualified Language.SMV.AbsSMV           as SMV
import qualified Language.SMV.ParSMV           as SMV (myLexer, pBoolSpec)
import           Language.SMV.Substitution     (substituteBoolExpr)
import qualified Language.Trans.Lustre2Copilot as Lustre (boolSpec2Copilot,
                                                          boolSpecNames)
import           Language.Trans.SMV2Copilot    as SMV (boolSpec2Copilot,
                                                       boolSpecNames)

-- | Existential wrapper over abstraction to handle expressions used in
-- specifications.
--
-- The abstraction provides mechanisms to parse expressions, replace variables
-- in them, render them in a known format or notation, and find identifiers in
-- them, and it provides a default value to use when an expression is needed.
data ExprPair = forall a . ExprPair
  { ()
exprTPair :: ExprPairT a
  }

-- | Abstraction to handle expressions used in specifications.
--
-- The abstraction provides mechanisms to parse expressions, replace variables
-- in them, render them in a known format or notation, and find identifiers in
-- them, and it provides a default value to use when an expression is needed.
data ExprPairT a = ExprPairT
  { forall a. ExprPairT a -> String -> Either String a
exprTParse   :: String -> Either String a
  , forall a. ExprPairT a -> [(String, String)] -> a -> a
exprTReplace :: [(String, String)] -> a -> a
  , forall a. ExprPairT a -> a -> String
exprTPrint   :: a -> String
  , forall a. ExprPairT a -> a -> [String]
exprTIdents  :: a -> [String]
  , forall a. ExprPairT a -> a
exprTUnknown :: a
  }

-- | Return 'ExprPair' for a given language (e.g., Lustre, SMV).
--
-- The language name must be lowercase.
--
-- We default to SMV if no format is given.
--
-- The format literal returns an ExprPair that uses Strings as the base type
-- and keeps them unchanged.
exprPair :: String -> ExprPair
exprPair :: String -> ExprPair
exprPair String
"lustre" = ExprPairT BoolSpec -> ExprPair
forall a. ExprPairT a -> ExprPair
ExprPair (ExprPairT BoolSpec -> ExprPair) -> ExprPairT BoolSpec -> ExprPair
forall a b. (a -> b) -> a -> b
$
  (String -> Either String BoolSpec)
-> ([(String, String)] -> BoolSpec -> BoolSpec)
-> (BoolSpec -> String)
-> (BoolSpec -> [String])
-> BoolSpec
-> ExprPairT BoolSpec
forall a.
(String -> Either String a)
-> ([(String, String)] -> a -> a)
-> (a -> String)
-> (a -> [String])
-> a
-> ExprPairT a
ExprPairT
    ([Token] -> Either String BoolSpec
Lustre.pBoolSpec ([Token] -> Either String BoolSpec)
-> (String -> [Token]) -> String -> Either String BoolSpec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [Token]
Lustre.myLexer)
    (\[(String, String)]
_ -> BoolSpec -> BoolSpec
forall a. a -> a
id)
    (BoolSpec -> String
Lustre.boolSpec2Copilot)
    (BoolSpec -> [String]
Lustre.boolSpecNames)
    (Ident -> BoolSpec
Lustre.BoolSpecSignal (String -> Ident
Lustre.Ident String
"undefined"))
exprPair String
"literal" = ExprPairT String -> ExprPair
forall a. ExprPairT a -> ExprPair
ExprPair (ExprPairT String -> ExprPair) -> ExprPairT String -> ExprPair
forall a b. (a -> b) -> a -> b
$
  (String -> Either String String)
-> ([(String, String)] -> String -> String)
-> (String -> String)
-> (String -> [String])
-> String
-> ExprPairT String
forall a.
(String -> Either String a)
-> ([(String, String)] -> a -> a)
-> (a -> String)
-> (a -> [String])
-> a
-> ExprPairT a
ExprPairT
    String -> Either String String
forall a b. b -> Either a b
Right
    (\[(String, String)]
_ -> String -> String
forall a. a -> a
id)
    String -> String
forall a. a -> a
id
    ([String] -> String -> [String]
forall a b. a -> b -> a
const [])
    String
"undefined"
exprPair String
"cocospec" = String -> ExprPair
exprPair String
"lustre"
exprPair String
_ = ExprPairT BoolSpec -> ExprPair
forall a. ExprPairT a -> ExprPair
ExprPair (ExprPairT BoolSpec -> ExprPair) -> ExprPairT BoolSpec -> ExprPair
forall a b. (a -> b) -> a -> b
$
  (String -> Either String BoolSpec)
-> ([(String, String)] -> BoolSpec -> BoolSpec)
-> (BoolSpec -> String)
-> (BoolSpec -> [String])
-> BoolSpec
-> ExprPairT BoolSpec
forall a.
(String -> Either String a)
-> ([(String, String)] -> a -> a)
-> (a -> String)
-> (a -> [String])
-> a
-> ExprPairT a
ExprPairT
    ([Token] -> Either String BoolSpec
SMV.pBoolSpec ([Token] -> Either String BoolSpec)
-> (String -> [Token]) -> String -> Either String BoolSpec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [Token]
SMV.myLexer)
    ([(String, String)] -> BoolSpec -> BoolSpec
forall {t :: * -> *}.
Foldable t =>
t (String, String) -> BoolSpec -> BoolSpec
substituteBoolExpr)
    (BoolSpec -> String
SMV.boolSpec2Copilot)
    (BoolSpec -> [String]
SMV.boolSpecNames)
    (Ident -> BoolSpec
SMV.BoolSpecSignal (String -> Ident
SMV.Ident String
"undefined"))

-- | Parse and print a value using an auxiliary Expression Pair.
--
-- Fails if the value has no valid parse.
exprPairShow :: ExprPair -> String -> String
exprPairShow :: ExprPair -> String -> String
exprPairShow (ExprPair ExprPairT a
exprP) =
    a -> String
printProp (a -> String) -> (String -> a) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either String a -> a
forall a b. Either a b -> b
fromRight' (Either String a -> a)
-> (String -> Either String a) -> String -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Either String a
parseProp
  where
    ExprPairT String -> Either String a
parseProp [(String, String)] -> a -> a
_replace a -> String
printProp a -> [String]
_ids a
_unknown = ExprPairT a
exprP

    -- | Unsafe fromRight. Fails if the value is a 'Left'.
    fromRight' :: Either a b -> b
    fromRight' :: forall a b. Either a b -> b
fromRight' (Right b
v) = b
v
    fromRight' Either a b
_         = String -> b
forall a. HasCallStack => String -> a
error String
"fromRight' applied to Left value."