{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE TypeFamilies          #-}

{-# OPTIONS_GHC -Wall #-}

{-|

Translation from annotation syntax defined in
"Camfort.Specification.Hoare.Syntax" to strongly-typed meta-expressions defined
in "Language.Fortran.Model.Op.Meta".

-}
module Camfort.Specification.Hoare.Translate
  (
    -- * Meta Expression Types
    MetaExpr
  , MetaFormula
  , AllOps

    -- * Translation
  , translateBoolExpression
  , translateFormula

    -- * Combinators
  , intoMetaExpr
  ) where

import           Prelude                            hiding (span)

import           Control.Lens
import           Control.Monad.Except               (MonadError (..))
import           Control.Monad.Fail

import qualified Language.Fortran.Analysis          as F
import qualified Language.Fortran.AST               as F

import           Language.Expression
import           Language.Expression.Choice
import           Language.Expression.Prop

import           Camfort.Helpers.TypeLevel
import           Language.Fortran.Model
import           Language.Fortran.Model.Singletons
import           Language.Fortran.Model.Translate
import           Language.Fortran.Model.Types.Match
import           Language.Fortran.Model.Vars

import           Camfort.Specification.Hoare.Syntax

--------------------------------------------------------------------------------
--  Lifting Logical Values
--------------------------------------------------------------------------------

type AllOps = '[HighOp, MetaOp, CoreOp]
type MetaExpr = HFree' AllOps
type MetaFormula = Prop (MetaExpr FortranVar)

--------------------------------------------------------------------------------
--  Translate
--------------------------------------------------------------------------------

-- | Translate an untyped logical formula into a strongly typed 'MetaFormula'.
translateFormula :: (Monad m, MonadFail m) => PrimFormula (F.Analysis ann) -> TranslateT m (MetaFormula Bool)
translateFormula :: PrimFormula (Analysis ann) -> TranslateT m (MetaFormula Bool)
translateFormula = \case
  PFExpr Expression (Analysis ann)
e -> do
    MetaExpr FortranVar Bool
e' <- Expression (Analysis ann)
-> TranslateT m (MetaExpr FortranVar Bool)
forall (m :: * -> *) ann.
(Monad m, MonadFail m) =>
Expression (Analysis ann)
-> TranslateT m (MetaExpr FortranVar Bool)
translateBoolExpression Expression (Analysis ann)
e
    MetaFormula Bool -> TranslateT m (MetaFormula Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaFormula Bool -> TranslateT m (MetaFormula Bool))
-> MetaFormula Bool -> TranslateT m (MetaFormula Bool)
forall a b. (a -> b) -> a -> b
$ MetaExpr FortranVar Bool -> MetaFormula Bool
forall (expr :: * -> *) a. expr a -> Prop expr a
expr (MetaExpr FortranVar Bool -> MetaFormula Bool)
-> MetaExpr FortranVar Bool -> MetaFormula Bool
forall a b. (a -> b) -> a -> b
$ MetaExpr FortranVar Bool
e'

  PFLogical PrimLogic (PrimFormula (Analysis ann))
x -> PrimLogic (MetaFormula Bool) -> MetaFormula Bool
foldPrimLogic (PrimLogic (MetaFormula Bool) -> MetaFormula Bool)
-> TranslateT m (PrimLogic (MetaFormula Bool))
-> TranslateT m (MetaFormula Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PrimFormula (Analysis ann) -> TranslateT m (MetaFormula Bool))
-> PrimLogic (PrimFormula (Analysis ann))
-> TranslateT m (PrimLogic (MetaFormula Bool))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse PrimFormula (Analysis ann) -> TranslateT m (MetaFormula Bool)
forall (m :: * -> *) ann.
(Monad m, MonadFail m) =>
PrimFormula (Analysis ann) -> TranslateT m (MetaFormula Bool)
translateFormula PrimLogic (PrimFormula (Analysis ann))
x


-- | Translate a boolean-valued untyped Fortran expression into a strongly typed 'MetaExpr'.
translateBoolExpression
  :: (Monad m, MonadFail m)
  => F.Expression (F.Analysis ann)
  -> TranslateT m (MetaExpr FortranVar Bool)
translateBoolExpression :: Expression (Analysis ann)
-> TranslateT m (MetaExpr FortranVar Bool)
translateBoolExpression Expression (Analysis ann)
e = do
  SomePair D a
d1 FortranExpr a
e' <- Expression (Analysis ann)
-> TranslateT m (Some (PairOf D FortranExpr))
forall (m :: * -> *) ann.
(Monad m, MonadFail m) =>
Expression (Analysis ann)
-> TranslateT m (Some (PairOf D FortranExpr))
translateExpression Expression (Analysis ann)
e

  case D a -> Maybe (MatchPrimD a)
forall a. D a -> Maybe (MatchPrimD a)
matchPrimD D a
d1 of
    Just (MatchPrimD (MatchPrim Sing p
_ Sing k
SBTLogical) Prim p k a
prim1) -> MetaExpr FortranVar Bool -> TranslateT m (MetaExpr FortranVar Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaExpr FortranVar Bool
 -> TranslateT m (MetaExpr FortranVar Bool))
-> MetaExpr FortranVar Bool
-> TranslateT m (MetaExpr FortranVar Bool)
forall a b. (a -> b) -> a -> b
$
      case Prim p k a
prim1 of
        Prim p k a
PBool8  -> FortranExpr a -> MetaExpr FortranVar Bool
forall a b. LiftD a b => FortranExpr a -> MetaExpr FortranVar b
liftFortranExpr FortranExpr a
e'
        Prim p k a
PBool16 -> FortranExpr a -> MetaExpr FortranVar Bool
forall a b. LiftD a b => FortranExpr a -> MetaExpr FortranVar b
liftFortranExpr FortranExpr a
e'
        Prim p k a
PBool32 -> FortranExpr a -> MetaExpr FortranVar Bool
forall a b. LiftD a b => FortranExpr a -> MetaExpr FortranVar b
liftFortranExpr FortranExpr a
e'
        Prim p k a
PBool64 -> FortranExpr a -> MetaExpr FortranVar Bool
forall a b. LiftD a b => FortranExpr a -> MetaExpr FortranVar b
liftFortranExpr FortranExpr a
e'
    Maybe (MatchPrimD a)
_ -> TranslateError -> TranslateT m (MetaExpr FortranVar Bool)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TranslateError -> TranslateT m (MetaExpr FortranVar Bool))
-> TranslateError -> TranslateT m (MetaExpr FortranVar Bool)
forall a b. (a -> b) -> a -> b
$ Text -> SomeType -> SomeType -> TranslateError
ErrUnexpectedType Text
"formula" (D (PrimS Bool8) -> SomeType
forall k (f :: k -> *) (a :: k). f a -> Some f
Some (Prim 'P8 'BTLogical Bool8 -> D (PrimS Bool8)
forall (p :: Precision) (k :: BasicType) a.
Prim p k a -> D (PrimS a)
DPrim Prim 'P8 'BTLogical Bool8
PBool8)) (D a -> SomeType
forall k (f :: k -> *) (a :: k). f a -> Some f
Some D a
d1)


foldPrimLogic :: PrimLogic (MetaFormula Bool) -> MetaFormula Bool
foldPrimLogic :: PrimLogic (MetaFormula Bool) -> MetaFormula Bool
foldPrimLogic = \case
  PLAnd MetaFormula Bool
x MetaFormula Bool
y -> MetaFormula Bool
x MetaFormula Bool -> MetaFormula Bool -> MetaFormula Bool
forall (expr :: * -> *).
Prop expr Bool -> Prop expr Bool -> Prop expr Bool
*&& MetaFormula Bool
y
  PLOr MetaFormula Bool
x MetaFormula Bool
y -> MetaFormula Bool
x MetaFormula Bool -> MetaFormula Bool -> MetaFormula Bool
forall (expr :: * -> *).
Prop expr Bool -> Prop expr Bool -> Prop expr Bool
*|| MetaFormula Bool
y
  PLImpl MetaFormula Bool
x MetaFormula Bool
y -> MetaFormula Bool
x MetaFormula Bool -> MetaFormula Bool -> MetaFormula Bool
forall (expr :: * -> *).
Prop expr Bool -> Prop expr Bool -> Prop expr Bool
*-> MetaFormula Bool
y
  PLEquiv MetaFormula Bool
x MetaFormula Bool
y -> MetaFormula Bool
x MetaFormula Bool -> MetaFormula Bool -> MetaFormula Bool
forall (expr :: * -> *).
Prop expr Bool -> Prop expr Bool -> Prop expr Bool
*<-> MetaFormula Bool
y
  PLNot MetaFormula Bool
x -> MetaFormula Bool -> MetaFormula Bool
forall (expr :: * -> *). Prop expr Bool -> Prop expr Bool
pnot MetaFormula Bool
x
  PLLit Bool
x -> Bool -> MetaFormula Bool
forall (expr :: * -> *). Bool -> Prop expr Bool
plit Bool
x


--------------------------------------------------------------------------------
--  Util
--------------------------------------------------------------------------------

-- | Convert an expression over 'HighOp', 'MetaOp' or 'CoreOp' into a 'MetaExpr'.
intoMetaExpr :: (ChooseOp op AllOps, HTraversable op) => HFree op v a -> MetaExpr v a
intoMetaExpr :: HFree op v a -> MetaExpr v a
intoMetaExpr = HFree (OpChoice AllOps) v a -> MetaExpr v a
forall (ops :: [(* -> *) -> * -> *]) (v :: * -> *) a.
HFree (OpChoice ops) v a -> HFree' ops v a
HFree' (HFree (OpChoice AllOps) v a -> MetaExpr v a)
-> (HFree op v a -> HFree (OpChoice AllOps) v a)
-> HFree op v a
-> MetaExpr v a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (g :: * -> *) b. op g b -> OpChoice AllOps g b)
-> HFree op v a -> HFree (OpChoice AllOps) v a
forall u (h :: ((u -> *) -> u -> *) -> (u -> *) -> u -> *)
       (s :: (u -> *) -> u -> *) (s' :: (u -> *) -> u -> *) (t :: u -> *)
       (a :: u).
(HDuofunctor h, HFunctor s) =>
(forall (g :: u -> *) (b :: u). s g b -> s' g b)
-> h s t a -> h s' t a
hduomapFirst' (AReview (OpChoice AllOps g b) (op g b)
-> op g b -> OpChoice AllOps g b
forall b (m :: * -> *) t. MonadReader b m => AReview t b -> m t
review AReview (OpChoice AllOps g b) (op g b)
forall (op :: (* -> *) -> * -> *) (ops :: [(* -> *) -> * -> *])
       (t :: * -> *) a.
ChooseOp op ops =>
Prism' (OpChoice ops t a) (op t a)
chooseOp)

liftFortranExpr :: (LiftD a b) => FortranExpr a -> MetaExpr FortranVar b
liftFortranExpr :: FortranExpr a -> MetaExpr FortranVar b
liftFortranExpr FortranExpr a
e =
  let e' :: HFree HighOp FortranExpr b
e' = HighOp (HFree HighOp FortranExpr) b -> HFree HighOp FortranExpr b
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
h (HFree h t) a -> HFree h t a
HWrap (LiftDOp (HFree HighOp FortranExpr) b
-> HighOp (HFree HighOp FortranExpr) b
forall (t :: * -> *) a. LiftDOp t a -> HighOp t a
HopLift (HFree HighOp FortranExpr a -> LiftDOp (HFree HighOp FortranExpr) b
forall b a (t :: * -> *). LiftD b a => t b -> LiftDOp t a
LiftDOp (FortranExpr a -> HFree HighOp FortranExpr a
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
t a -> HFree h t a
HPure FortranExpr a
e)))
  in HFree HighOp FortranExpr b -> MetaExpr FortranVar b
forall (op1 :: (* -> *) -> * -> *) (op2 :: (* -> *) -> * -> *)
       (ops :: [(* -> *) -> * -> *]) (v :: * -> *) a.
(HFunctor op1, HFunctor op2, HFunctor (OpChoice ops),
 ChooseOp op1 ops, ChooseOp op2 ops) =>
HFree op1 (HFree op2 v) a -> HFree' ops v a
squashExpression HFree HighOp FortranExpr b
e'