    -- Copyright 2024 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.

    -- | Formally analyze Copilot Core specifications.
    module Copilot.Core.Analysis
        ( exprIsConstant )
      where

    -- External imports
    import qualified Copilot.Core          as Core
    import           Copilot.Theorem.What4 (SatResult (..), Solver (Z3), prove)
    import           Data.List             (lookup)

    -- | Determine if a boolean expression is always 'True' or always 'False'.
    --
    -- The first boolean in the result is 'True' if the expression can be proven
    -- always 'True'. The second boolean in the expression is 'True' is the
    -- expression can be proven always 'False'.
    --
    -- They values in the tuple cannot both 'True' at the same time.
    exprIsConstant :: Core.Spec
                   -> Core.Name
                   -> Core.Expr Bool
                   -> IO (Bool, Bool)
    exprIsConstant :: Spec -> Name -> Expr Bool -> IO (Bool, Bool)
    exprIsConstant Spec
    spec Name
    name Expr Bool
    expr = do
      r1 <- Spec -> Name -> Prop -> IO Bool
    propIsValid Spec
    spec Name
    name (Expr Bool -> Prop
    Core.Forall Expr Bool
    expr)
      r2 <- propIsValid spec name (Core.Forall (Core.Op1 Core.Not expr))
      pure (r1, r2)

    -- | 'True' if the Copilot 'Prop' with the given name and expression is
    -- constantly 'True', or valid, and 'False' otherwise (not always 'True' or
    -- unknown).
    propIsValid :: Core.Spec
                -> Core.Name
                -> Core.Prop
                -> IO Bool
    propIsValid :: Spec -> Name -> Prop -> IO Bool
    propIsValid Spec
    spec Name
    name Prop
    expr =
        Bool -> (SatResult -> Bool) -> Maybe SatResult -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    False SatResult -> Bool
    isValid (Maybe SatResult -> Bool)
    -> ([(Name, SatResult)] -> Maybe SatResult)
    -> [(Name, SatResult)]
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> [(Name, SatResult)] -> Maybe SatResult
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup Name
    name ([(Name, SatResult)] -> Bool) -> IO [(Name, SatResult)] -> IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Solver -> Spec -> IO [(Name, SatResult)]
    prove Solver
    Z3 Spec
    spec'
      where
        spec' :: Spec
    spec' = Spec
    spec { Core.specProperties = prop' : Core.specProperties spec }
        prop' :: Property
    prop' = Name -> Prop -> Property
    Core.Property Name
    name Prop
    expr

        isValid :: SatResult -> Bool
        isValid :: SatResult -> Bool
    isValid SatResult
    Valid = Bool
    True
        isValid SatResult
    _     = Bool
    False