{-# LANGUAGE DeriveFunctor          #-}
{-# LANGUAGE DeriveTraversable      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE LambdaCase             #-}
{-# LANGUAGE MultiParamTypeClasses  #-}

module Language.While.Continuity where

import           Data.SBV

import           Data.Set              (Set)
import qualified Data.Set              as Set

import           Language.While.Hoare
import           Language.While.Syntax

import Language.Expression


  

-- data OpSpec =
--   OpSpec
--   { _osPrecondition :: Prop Int
--   , _osOpContinuity :: Set Int
--   }
--   deriving (Show)


-- exprOpSpecs :: ExprOp a -> [OpSpec]
-- exprOpSpecs = \case
--   OAdd _ _ -> [OpSpec (PLit True) (Set.fromList [0, 1])]
--   OMul _ _ -> [OpSpec (PLit True) (Set.fromList [0, 1])]
--   OSub _ _ -> [OpSpec (PLit True) (Set.fromList [0, 1])]


-- -- | @'exprContinuous' allVars prop inputs expr@ judges whether @expr@ is
-- -- continuous with respect to the given input variables, whenever the current
-- -- program state is one in which @prop@ is true. @allVars@ constrains the
-- -- variables in the program.
-- exprContinuous :: (Ord l) => Set l -> WhileProp l -> Set l -> Expr l -> Bool
-- exprContinuous = undefined


-- newtype SetVar = SetVar Int


-- data SetExpr l v
--   = SVar v
--   | SLit (Set l)
--   | SUnion (SetExpr l v) (SetExpr l v)
--   | SDiff


-- data SetProp l v
--   = Subset (SetExpr l v) (SetExpr l v)


-- class Monad m => MonadProveCont l m | m -> l where
--   -- Fresh variables
--   -- Adding proof obligations
--   -- Discharging some of the existing proof obligations
--   -- Querying state

-- -- | @'findContinuity' prop inputs command@ yields the largest set of output
-- -- variables such that the outputs vary continuously in the inputs when
-- -- @command@ from a state which satisfies @prop@.
-- findContinuity :: (MonadProveCont l m) => Prop l -> Set l -> Command l a -> m (Set l)
-- findContinuity prop inputs command = undefined

-- -- | @'continuityVcs' subspace inputs outputs command@ computes the verification
-- -- conditions for each of the variables in @outputs@ to vary continuously with
-- -- respect to each of the variables in @inputs@, after running @command@.
-- continuityVcs :: Prop l -> [l] -> [l] -> Command l a -> SBool
-- continuityVcs prop inputs outputs = undefined