Translate.hs

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

{-# 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 (..))

#if !MIN_VERSION_base(4,13,0)
-- Control.Monad.Fail import is redundant since GHC 8.8.1
import           Control.Monad.Fail
#endif

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 = \case
  PFExpr e -> do
    e' <- translateBoolExpression e
    return $ expr $ e'

  PFLogical x -> foldPrimLogic <$> traverse translateFormula 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 e = do
  SomePair d1 e' <- translateExpression e

  case matchPrimD d1 of
    Just (MatchPrimD (MatchPrim _ SBTLogical) prim1) -> return $
      case prim1 of
        PBool8  -> liftFortranExpr e'
        PBool16 -> liftFortranExpr e'
        PBool32 -> liftFortranExpr e'
        PBool64 -> liftFortranExpr e'
    _ -> throwError $ ErrUnexpectedType "formula" (Some (DPrim PBool8)) (Some d1)


foldPrimLogic :: PrimLogic (MetaFormula Bool) -> MetaFormula Bool
foldPrimLogic = \case
  PLAnd x y -> x *&& y
  PLOr x y -> x *|| y
  PLImpl x y -> x *-> y
  PLEquiv x y -> x *<-> y
  PLNot x -> pnot x
  PLLit x -> plit 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' . hduomapFirst' (review chooseOp)

liftFortranExpr :: (LiftD a b) => FortranExpr a -> MetaExpr FortranVar b
liftFortranExpr e =
  let e' = HWrap (HopLift (LiftDOp (HPure e)))
  in squashExpression e'