    {-# 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."