{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImplicitParams, RankNTypes #-}
{-|
    Module      :  Numeric.AERN.Basics.Laws.Relation
    Description :  common properties of arithmetic operations arbitrarily-little rounded  
    Copyright   :  (c) Michal Konecny
    License     :  BSD3

    Maintainer  :  mikkonecny@gmail.com
    Stability   :  experimental
    Portability :  portable
    
    Common properties of arithmetic operations when these operations
    are rounded but the rounding can be diminished arbitrarily 
    by increasing an effort indicator.
-}

module Numeric.AERN.RealArithmetic.Laws where

import Numeric.AERN.RealArithmetic.Measures

import Numeric.AERN.Basics.Effort
import Numeric.AERN.Basics.Consistency
import Numeric.AERN.Basics.Laws.Utilities
import Numeric.AERN.Basics.Mutable

import Numeric.AERN.Misc.Bool
import Numeric.AERN.Misc.Debug
import Numeric.AERN.Misc.List
import Numeric.AERN.Misc.Maybe
import Data.Maybe

import Numeric.AERN.RealArithmetic.ExactOps
import Numeric.AERN.RealArithmetic.NumericOrderRounding.Conversion
import qualified Numeric.AERN.Basics.NumericOrder as NumOrd
import Numeric.AERN.Basics.NumericOrder.OpsImplicitEffort

import qualified Numeric.AERN.Basics.RefinementOrder as RefOrd

import Numeric.AERN.Basics.Exception
import Control.Exception

roundedRefinementMonotone1 ::
    (RefOrd.PartialComparison t, 
     RefOrd.ArbitraryOrderedTuple t, 
     Show t, HasLegalValues t) =>
    String ->
    (Expr1Eff ei t) ->
    (Expr1Eff ei t) ->
    ei -> (RefOrd.LEPair t) -> 
    (RefOrd.PartialCompareEffortIndicator t) ->
    Bool
roundedRefinementMonotone1 contextDescription exprUp exprDn effort (RefOrd.LEPair (e1L, e1H)) effortComp =
    case RefOrd.pLeqEff effortComp resDn resUp of
        Just b -> b
        _ -> True
    where
    resUp = check $ exprUp effort e1H
    resDn = check $ exprDn effort e1L
    check = detectIllegalValues $ contextDescription ++ " monotone"

roundedRefinementMonotone2 ::
    (RefOrd.PartialComparison t, 
     RefOrd.ArbitraryOrderedTuple t, 
     Show t, HasLegalValues t) =>
    String ->
    (Expr2Eff ei t) ->
    (Expr2Eff ei t) ->
    ei -> (RefOrd.LEPair t) -> (RefOrd.LEPair t) -> 
    (RefOrd.PartialCompareEffortIndicator t) ->
    Bool
roundedRefinementMonotone2 
        contextDescription exprUp exprDn effort 
        (RefOrd.LEPair (e1L, e1H)) (RefOrd.LEPair (e2L, e2H)) effortComp =
--    unsafePrint ("\nroundedRefinementMonotone2: " 
--      ++ "\n Up: op(" ++ show e1H ++ ", " ++ show e2H ++ ") = " ++ show resUp 
--      ++ "\n Dn: op(" ++ show e1L ++ ", " ++ show e2L ++ ") = " ++ show resDn
--      ++ "\n" 
--    ) $
    case RefOrd.pLeqEff effortComp resDn resUp of
        Just b -> b
        _ -> True
    where
    resUp = check $ exprUp effort e1H e2H
    resDn = check $ exprDn effort e1L e2L
    check = detectIllegalValues $ contextDescription ++ " monotone"

roundedUnit ::
    (EffortIndicator eiRel, Show eiRel, 
     EffortIndicator eiOp, Show eiOp, 
     Show t, HasLegalValues t) =>
    t -> 
    (PRelEff eiRel t) -> 
    (OpEff eiOp t) -> (OpEff eiOp t) -> 
    (eiRel, eiOp) -> 
    t -> Bool
roundedUnit unit =
    equalRoundingUpDnBin1Var1 "roundedUnit" (\_ _ e -> e) expr2
    where
    expr2 opEff effort e = 
        unit * e
        where
        (*) = opEff effort

roundedReflexiveCollapse ::
    (EffortIndicator eiRel, Show eiRel, 
     EffortIndicator eiOp, Show eiOp, 
     Show t, HasLegalValues t) =>
    t -> 
    (PRelEff eiRel t) -> 
    (OpEff eiOp t) -> (OpEff eiOp t) -> 
    (eiRel, eiOp) -> 
    t -> Bool
roundedReflexiveCollapse unit =
    equalRoundingUpDnBin1Var1 "roundedReflexiveCollapse" (\_ _ e -> unit) expr2
    where
    expr2 opEff effort e = 
        e * e
        where
        (*) = opEff effort

roundedCommutative ::
    (EffortIndicator eiRel, Show eiRel, 
     EffortIndicator eiOp, Show eiOp, 
     Show t, HasLegalValues t) =>
    (PRelEff eiRel t) -> 
    (OpEff eiOp t) -> (OpEff eiOp t) -> 
    (eiRel, eiOp) -> 
    t -> t -> Bool
roundedCommutative =
    equalRoundingUpDnBin1Var2 "roundedCommutative" expr1 expr2
    where
    expr1 opEff effort e1 e2 = 
        e1 * e2
        where
        (*) = opEff effort
    expr2 opEff effort e1 e2 = 
        e2 * e1
        where
        (*) = opEff effort

roundedAssociative ::
    (EffortIndicator eiRel, Show eiRel, 
     EffortIndicator eiOp, Show eiOp, 
     Show t, HasLegalValues t) =>
    (PRelEff eiRel t) -> 
    (OpEff eiOp t) -> (OpEff eiOp t) -> 
    (eiRel, eiOp) -> 
    t -> t -> t -> Bool
roundedAssociative =
    equalRoundingUpDnBin1Var3 "roundedAssociative" expr1 expr2
    where
    expr1 opEff effort e1 e2 e3 = 
        (e1 * e2) * e3
        where
        (*) = opEff effort
    expr2 opEff effort e1 e2 e3 = 
        e1 * (e2 * e3)
        where
        (*) = opEff effort

roundedDistributive ::
    (EffortIndicator eiRel, Show eiRel, 
     EffortIndicator eiOp1, Show eiOp1, 
     EffortIndicator eiOp2, Show eiOp2,
     HasAntiConsistency t, Show t, HasLegalValues t) =>
    (PRelEff eiRel t) -> 
    (OpEff eiOp1 t) -> (OpEff eiOp2 t) -> 
    (OpEff eiOp1 t) -> (OpEff eiOp2 t) -> 
    (ConsistencyEffortIndicator t) ->
    (eiRel, (eiOp1, eiOp2)) -> 
    t -> t -> t -> Bool
roundedDistributive 
        pCompareEff
        op1UpEff op2UpEff 
        op1DnEff op2DnEff 
        effortConsistency
        initEffort 
        e1 e2 e3 =
--    unsafePrint
--    (
--        "property roundedDistributive: "
--        ++ "\n e1 = " ++ show e1
--        ++ "\n e2 = " ++ show e2
--        ++ "\n e3 = " ++ show e3
--    ) $        
    thinEqualConsLeqRoundingUpDnImprovement "roundedDistributive"
        -- cannot get equality when e1 is not thin 
        -- because e1 appears twice in expr1 (dependency error)
        [e1] expr1Up expr1Dn expr2Up expr2Dn 
        pCompareEff
        effortConsistency 
        initEffort
    where
    expr1Up eff = expr1 op1UpEff op2UpEff eff e1 e2 e3
    expr1Dn eff = expr1 op1DnEff op2DnEff eff e1 e2 e3
    expr2Up eff = expr2 op1UpEff op2UpEff eff e1 e2 e3
    expr2Dn eff = expr2 op1DnEff op2DnEff eff e1 e2 e3
    expr1 op1Eff op2Eff (effort1, effort2) e1 e2 e3 = 
        (e1 * e2) + (e1 * e3)
        where
        (*) = op1Eff effort1
        (+) = op2Eff effort2
    expr2 op1Eff op2Eff (effort1, effort2) e1 e2 e3 = 
        e1 * (e2 + e3)
        where
        (*) = op1Eff effort1
        (+) = op2Eff effort2


roundedNegSymmetric ::
    (Neg t,
     EffortIndicator eiRel, Show eiRel, 
     EffortIndicator eiOp, Show eiOp, 
     Show t, HasLegalValues t) =>
    (PRelEff eiRel t) -> 
    (UnaryOpEff eiOp t) -> (UnaryOpEff eiOp t) -> 
    (eiRel, eiOp) -> 
    t -> Bool
roundedNegSymmetric =
    equalRoundingUpDnUnary1Var1 "roundedNegSymmetric" expr1 expr2
    where
    expr1 opEff effort e = 
         opEff effort e
    expr2 opEff effort e = 
         opEff effort (neg e) 

roundedIdempotent ::
    (EffortIndicator eiRel, Show eiRel, 
     EffortIndicator eiOp, Show eiOp, 
     Show t, HasLegalValues t) =>
    (PRelEff eiRel t) -> 
    (UnaryOpEff eiOp t) -> (UnaryOpEff eiOp t) -> 
    (eiRel, eiOp) -> 
    t -> Bool
roundedIdempotent =
    equalRoundingUpDnUnary1Var1 "roundedIdempotent" expr1 expr2
    where
    expr1 opEff effort e = 
         opEff effort e
    expr2 opEff effort e = 
         opEff effort (opEff effort e)


equalRoundingUpDnUnary1Var1 :: 
    (EffortIndicator eiRel, Show eiRel, 
     EffortIndicator eiOp, Show eiOp, 
     Show t, HasLegalValues t) =>
    String ->
    (Expr1UnaryOp1Eff eiOp t) -> 
    (Expr1UnaryOp1Eff eiOp t) -> 
    (PRelEff eiRel t) -> 
    (UnaryOpEff eiOp t) -> (UnaryOpEff eiOp t) -> 
    (eiRel, eiOp) -> 
    t -> Bool
equalRoundingUpDnUnary1Var1 contextDescription expr1 expr2 pCompareEff opUpEff opDnEff 
        initEffort e =
    equalRoundingUpDn contextDescription expr1Up expr1Dn expr2Up expr2Dn pCompareEff initEffort
    where
    expr1Up eff = expr1 opUpEff eff e
    expr1Dn eff = expr1 opDnEff eff e
    expr2Up eff = expr2 opUpEff eff e
    expr2Dn eff = expr2 opDnEff eff e

equalRoundingUpDnBin1Var1 :: 
    (EffortIndicator eiRel, Show eiRel, 
     EffortIndicator eiOp, Show eiOp, 
     Show t, HasLegalValues t) =>
    String ->
    (Expr1Op1Eff eiOp t) -> 
    (Expr1Op1Eff eiOp t) -> 
    (PRelEff eiRel t) -> 
    (OpEff eiOp t) -> (OpEff eiOp t) -> 
    (eiRel, eiOp) -> 
    t -> Bool
equalRoundingUpDnBin1Var1 
        contextDescription expr1 expr2 pCompareEff 
        opUpEff opDnEff initEffort e =
    equalRoundingUpDn 
        contextDescription expr1Up expr1Dn expr2Up expr2Dn pCompareEff initEffort
    where
    expr1Up eff = expr1 opUpEff eff e
    expr1Dn eff = expr1 opDnEff eff e
    expr2Up eff = expr2 opUpEff eff e
    expr2Dn eff = expr2 opDnEff eff e

equalRoundingUpDnBin1Var2 :: 
    (EffortIndicator eiRel, Show eiRel, 
     EffortIndicator eiOp, Show eiOp, 
     Show t, HasLegalValues t) =>
    String ->
    (Expr1Op2Eff eiOp t) -> 
    (Expr1Op2Eff eiOp t) -> 
    (PRelEff eiRel t) -> 
    (OpEff eiOp t) -> (OpEff eiOp t) -> 
    (eiRel, eiOp) -> 
    t -> t -> Bool
equalRoundingUpDnBin1Var2 contextDescription expr1 expr2 pCompareEff opUpEff opDnEff 
        initEffort e1 e2 =
    equalRoundingUpDn contextDescription expr1Up expr1Dn expr2Up expr2Dn pCompareEff initEffort
    where
    expr1Up eff = expr1 opUpEff eff e1 e2
    expr1Dn eff = expr1 opDnEff eff e1 e2
    expr2Up eff = expr2 opUpEff eff e1 e2
    expr2Dn eff = expr2 opDnEff eff e1 e2

equalRoundingUpDnBin1Var3 :: 
    (EffortIndicator eiRel, Show eiRel, 
     EffortIndicator eiOp, Show eiOp, 
     Show t, HasLegalValues t) =>
    String ->
    (Expr1Op3Eff eiOp t) -> 
    (Expr1Op3Eff eiOp t) -> 
    (PRelEff eiRel t) -> 
    (OpEff eiOp t) -> (OpEff eiOp t) -> 
    (eiRel, eiOp) -> 
    t -> t -> t -> Bool
equalRoundingUpDnBin1Var3 contextDescription expr1 expr2 pCompareEff opUpEff opDnEff 
        initEffort e1 e2 e3 =
    equalRoundingUpDn contextDescription expr1Up expr1Dn expr2Up expr2Dn pCompareEff initEffort
    where
    expr1Up eff = expr1 opUpEff eff e1 e2 e3
    expr1Dn eff = expr1 opDnEff eff e1 e2 e3
    expr2Up eff = expr2 opUpEff eff e1 e2 e3
    expr2Dn eff = expr2 opDnEff eff e1 e2 e3

equalRoundingUpDnBin2Var3 :: 
    (EffortIndicator eiRel, Show eiRel, 
     EffortIndicator eiOp1, Show eiOp1, 
     EffortIndicator eiOp2, Show eiOp2,
     Show t, HasLegalValues t) =>
    String ->
    (Expr2Op3Eff eiOp1 eiOp2 t) -> 
    (Expr2Op3Eff eiOp1 eiOp2 t) -> 
    (PRelEff eiRel t) -> 
    (OpEff eiOp1 t) -> (OpEff eiOp2 t) -> 
    (OpEff eiOp1 t) -> (OpEff eiOp2 t) -> 
    (eiRel, (eiOp1, eiOp2)) -> 
    t -> t -> t -> Bool
equalRoundingUpDnBin2Var3 contextDescription expr1 expr2 pCompareEff 
        op1UpEff op2UpEff 
        op1DnEff op2DnEff 
        initEffort e1 e2 e3 =
    equalRoundingUpDn contextDescription expr1Up expr1Dn expr2Up expr2Dn pCompareEff initEffort
    where
    expr1Up eff = expr1 op1UpEff op2UpEff eff e1 e2 e3
    expr1Dn eff = expr1 op1DnEff op2DnEff eff e1 e2 e3
    expr2Up eff = expr2 op1UpEff op2UpEff eff e1 e2 e3
    expr2Dn eff = expr2 op1DnEff op2DnEff eff e1 e2 e3

thinEqualConsLeqRoundingUpDnImprovementBin2Var3 :: 
    (EffortIndicator eiRel, Show eiRel, 
     EffortIndicator eiOp1, Show eiOp1, 
     EffortIndicator eiOp2, Show eiOp2,
     HasAntiConsistency t, Show t, HasLegalValues t) =>
    String ->
    (Expr2Op3Eff eiOp1 eiOp2 t) -> 
    (Expr2Op3Eff eiOp1 eiOp2 t) -> 
    (PRelEff eiRel t) -> 
    (OpEff eiOp1 t) -> (OpEff eiOp2 t) -> 
    (OpEff eiOp1 t) -> (OpEff eiOp2 t) ->
    (ConsistencyEffortIndicator t) -> 
    (eiRel, (eiOp1, eiOp2)) -> 
    t -> t -> t -> Bool
thinEqualConsLeqRoundingUpDnImprovementBin2Var3
        contextDescription
        expr1 expr2 pCompareEff 
        op1UpEff op2UpEff 
        op1DnEff op2DnEff 
        effortConsistency
        initEffort 
        e1 e2 e3 =
    thinEqualConsLeqRoundingUpDnImprovement
        contextDescription
        [e1,e2,e3] expr1Up expr1Dn expr2Up expr2Dn 
        pCompareEff
        effortConsistency 
        initEffort
    where
    expr1Up eff = expr1 op1UpEff op2UpEff eff e1 e2 e3
    expr1Dn eff = expr1 op1DnEff op2DnEff eff e1 e2 e3
    expr2Up eff = expr2 op1UpEff op2UpEff eff e1 e2 e3
    expr2Dn eff = expr2 op1DnEff op2DnEff eff e1 e2 e3



equalRoundingUpDnBin2Var2 :: 
    (EffortIndicator eiRel, Show eiRel, 
     EffortIndicator eiOp1, Show eiOp1, 
     EffortIndicator eiOp2, Show eiOp2,
     Show t, HasLegalValues t) =>
    String ->
    (Expr2Op2Eff eiOp1 eiOp2 t) -> 
    (Expr2Op2Eff eiOp1 eiOp2 t) -> 
    (PRelEff eiRel t) -> 
    (OpEff eiOp1 t) -> (OpEff eiOp2 t) -> 
    (OpEff eiOp1 t) -> (OpEff eiOp2 t) -> 
    (eiRel, (eiOp1, eiOp2)) -> 
    t -> t -> Bool
equalRoundingUpDnBin2Var2 contextDescription expr1 expr2 pCompareEff 
        op1UpEff op2UpEff 
        op1DnEff op2DnEff 
        initEffort e1 e2 =
    equalRoundingUpDn contextDescription expr1Up expr1Dn expr2Up expr2Dn pCompareEff initEffort
    where
    expr1Up eff = expr1 op1UpEff op2UpEff eff e1 e2
    expr1Dn eff = expr1 op1DnEff op2DnEff eff e1 e2
    expr2Up eff = expr2 op1UpEff op2UpEff eff e1 e2
    expr2Dn eff = expr2 op1DnEff op2DnEff eff e1 e2

thinEqualConsLeqRoundingUpDnImprovement :: 
    (EffortIndicator eiRel, EffortIndicator eiOp,
     Show eiOp, Show eiRel,
     HasAntiConsistency t, Show t, HasLegalValues t) =>
    String ->
    [t] -> 
    (eiOp -> t) {-^ left hand side expression UP -} -> 
    (eiOp -> t) {-^ left hand side expression DN -} -> 
    (eiOp -> t) {-^ right hand side expression UP -} -> 
    (eiOp -> t) {-^ right hand side expression DN -} ->
    (PRelEff eiRel t) -> 
    (ConsistencyEffortIndicator t) -> 
    (eiRel, eiOp) -> Bool
thinEqualConsLeqRoundingUpDnImprovement
        contextDescription
        parameters
        expr1Up expr1Dn expr2Up expr2Dn
        pCompareEff
        consistencyEffort 
        initEffort@(effComp, effOp)
    | allConsistent && allAntiConsistent =
        okIfThin
    | allConsistent =
        okIfConsistent
    | allAntiConsistent =
        okIfAntiConsistent
    where
    allConsistent =
        and $ map isConsistent parameters
    allAntiConsistent =
        and $ map isAntiConsistent parameters
    okIfThin =
            (equalRoundingUpDn contextDescription
                expr1Up expr1Dn expr2Up expr2Dn 
                pCompareEff initEffort)
    okIfConsistent =
            leqRoundingUpDn expr1Dn expr2Up
    okIfAntiConsistent = 
            leqRoundingUpDn expr2Dn expr1Up
    isConsistent a = 
        justButNot False $ isConsistentEff consistencyEffort a
    isAntiConsistent a = 
        justButNot False $ isAntiConsistentEff consistencyEffort a
    leqRoundingUpDn expr1Dn expr2Up =
        case pCompareEff effComp (expr1Dn effOp) (expr2Up effOp) of
            Just res -> res
            Nothing -> True


equalRoundingUpDn :: 
    (EffortIndicator eiRel, EffortIndicator eiOp,
     Show eiOp, Show eiRel,
     Show t, HasLegalValues t) =>
    String ->
    (eiOp -> t) {-^ left hand side expression UP -} -> 
    (eiOp -> t) {-^ left hand side expression DN -} -> 
    (eiOp -> t) {-^ right hand side expression UP -} -> 
    (eiOp -> t) {-^ right hand side expression DN -} -> 
    (PRelEff eiRel t) -> 
    (eiRel, eiOp) -> Bool
equalRoundingUpDn 
        contextDescription
        expr1Up expr1Dn expr2Up expr2Dn 
        pCompareEff initEffort =
--    unsafePrint 
--    (
--        "equalRoundingUpDn:"
--        ++ "\n  efforts executed = \n" ++ unlines (map show $ take (comparisonCount + 1) efforts)
--        ++ "\n  5 successes = \n" ++ unlines (map show relevantSuccesses)
--    ) 
--    $
    case evalCatchDomViolationExceptions "checking a property" result of
            Left e -> True
                -- ignore tests during which a domain violation exception arises 
            Right res -> res
                -- throw an exception if the result is an illegal values (eg NaN) 
    where
    result = 
        (andUnsafeReportFirstFalse relevantSuccesses)  
    relevantSuccesses = take 5 successes
    successes = map check efforts
    efforts =
        (initEffort : ) $ take 15 $ effortIncrementSequence initEffort
    check (effortRel, effortOp) =
        successWithMsg 
        where
        successWithMsg =
            (success,
              "failure for effortRel = " ++ show effortRel 
                ++ " effortOp = " ++ show effortOp
              ++ "\n val1Dn <=? val2Up is " 
                ++ show val1Dn ++ " <=? " ++ show val2Up ++ " = "
                ++ show (val1Dn <=? val2Up)
              ++ "\n val2Dn <=? val1Up is " 
                ++ show val2Dn ++ " <=? " ++ show val1Up ++ " = "
                ++ show (val2Dn <=? val1Up)
            )
        success =
            (defined (val1Dn <=? val2Up) ===> (val1Dn <= val2Up))
            &&
            (defined (val2Dn <=? val1Up) ===> (val2Dn <= val1Up))
        val1Dn = check $ expr1Dn effortOp
        val1Up = check $ expr1Up effortOp
        val2Dn = check $ expr2Dn effortOp
        val2Up = check $ expr2Up effortOp
        check = detectIllegalValues contextDescription
        (<=) = assumeTotal2 (<=?)
        (<=?) = pCompareEff effortRel

roundedInPlace1ConsistentWithPure ::
    (EffortIndicator eiRel, EffortIndicator eiOp,
     Show eiOp, Show eiRel,
     CanBeMutable t, Show t, HasLegalValues t) =>
    String ->
    (forall s. eiOp -> OpMutable1 t s) {-^ left hand side expression UP -} -> 
    (forall s. eiOp -> OpMutable1 t s) {-^ left hand side expression DN -} -> 
    (eiOp -> UnaryOp t) {-^ right hand side expression UP -} -> 
    (eiOp -> UnaryOp t) {-^ right hand side expression DN -} -> 
    (PRelEff eiRel t) -> 
    (eiRel, eiOp) -> 
    t ->
    Bool
roundedInPlace1ConsistentWithPure
        contextDescription
        opUpInPlaceEff opDnInPlaceEff opUpEff opDnEff 
        pLeqEff initEffort
        e
        =
    equalRoundingUpDn
        ("in-place" ++ contextDescription ++ " consistent with pure")
        expr1Up expr1Dn expr2Up expr2Dn 
        pLeqEff initEffort
    where
    opUpEffViaInPlace = mutable1EffToPure (opUpInPlaceEff)
    opDnEffViaInPlace = mutable1EffToPure (opDnInPlaceEff)
    expr1Up eff = opUpEff eff e
    expr1Dn eff = opDnEff eff e
    expr2Up eff = opUpEffViaInPlace eff e
    expr2Dn eff = opDnEffViaInPlace eff e

roundedInPlace2ConsistentWithPure ::
    (EffortIndicator eiRel, EffortIndicator eiOp,
     Show eiOp, Show eiRel,
     CanBeMutable t, Show t, HasLegalValues t) =>
    String ->
    (forall s. eiOp -> OpMutable2 t s) {-^ left hand side expression UP -} -> 
    (forall s. eiOp -> OpMutable2 t s) {-^ left hand side expression DN -} -> 
    (eiOp -> Op t) {-^ right hand side expression UP -} -> 
    (eiOp -> Op t) {-^ right hand side expression DN -} -> 
    (PRelEff eiRel t) -> 
    (eiRel, eiOp) -> 
    t -> t ->
    Bool
roundedInPlace2ConsistentWithPure
        contextDescription
        opUpInPlaceEff opDnInPlaceEff opUpEff opDnEff 
        pLeqEff initEffort
        e1 e2
        =
    equalRoundingUpDn
        ("in-place" ++ contextDescription ++ " consistent with pure")
        expr1Up expr1Dn expr2Up expr2Dn 
        pLeqEff initEffort
    where
    opUpEffViaInPlace = mutable2EffToPure (opUpInPlaceEff)
    opDnEffViaInPlace = mutable2EffToPure (opDnInPlaceEff)
    expr1Up eff =
        let (*^) = opUpEff eff in e1 *^ e2
    expr1Dn eff =
        let (*.) = opDnEff eff in e1 *. e2
    expr2Up eff =
        let (*^) = opUpEffViaInPlace eff in e1 *^ e2
    expr2Dn eff =
        let (*.) = opDnEffViaInPlace eff in e1 *. e2