module HERMIT.Dictionary.Reasoning
(
externals
, verifyEqualityLeftToRightT
, verifyEqualityCommonTargetT
, verifyIsomorphismT
, verifyRetractionT
, retractionBR
)
where
import Control.Applicative
import Control.Arrow
import HERMIT.Core
import HERMIT.External
import HERMIT.GHC
import HERMIT.Kure
import HERMIT.Monad
import HERMIT.ParserCore
import HERMIT.Utilities
import HERMIT.Dictionary.Common
externals :: [External]
externals =
[ external "retraction" ((\ f g r -> promoteExprBiR $ retraction (Just r) f g) :: CoreString -> CoreString -> RewriteH Core -> BiRewriteH Core)
[ "Given f :: X -> Y and g :: Y -> X, and a proof that f (g y) ==> y, then"
, "f (g y) <==> y."
] .+ Shallow
, external "retraction-unsafe" ((\ f g -> promoteExprBiR $ retraction Nothing f g) :: CoreString -> CoreString -> BiRewriteH Core)
[ "Given f :: X -> Y and g :: Y -> X, then"
, "f (g y) <==> y."
, "Note that the precondition (f (g y) == y) is expected to hold."
] .+ Shallow .+ PreCondition
]
verifyEqualityLeftToRightT :: MonadCatch m => CoreExpr -> CoreExpr -> Rewrite c m CoreExpr -> Translate c m a ()
verifyEqualityLeftToRightT sourceExpr targetExpr r =
prefixFailMsg "equality verification failed: " $
do resultExpr <- r <<< return sourceExpr
guardMsg (exprAlphaEq targetExpr resultExpr) "result of running proof on lhs of equality does not match rhs of equality."
verifyEqualityCommonTargetT :: MonadCatch m => CoreExpr -> CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Translate c m a ()
verifyEqualityCommonTargetT lhs rhs lhsR rhsR =
prefixFailMsg "equality verification failed: " $
do lhsResult <- lhsR <<< return lhs
rhsResult <- rhsR <<< return rhs
guardMsg (exprAlphaEq lhsResult rhsResult) "results of running proofs on both sides of equality do not match."
verifyIsomorphismT :: CoreExpr -> CoreExpr -> Rewrite c HermitM CoreExpr -> Rewrite c HermitM CoreExpr -> Translate c HermitM a ()
verifyIsomorphismT f g fgR gfR = prefixFailMsg "Isomorphism verification failed: " $
do (tyX, tyY) <- funsWithInverseTypes f g
x <- constT (newGlobalIdH "x" tyX)
y <- constT (newGlobalIdH "y" tyY)
verifyEqualityLeftToRightT (App f (App g (Var y))) (Var y) fgR
verifyEqualityLeftToRightT (App g (App f (Var x))) (Var x) gfR
verifyRetractionT :: CoreExpr -> CoreExpr -> Rewrite c HermitM CoreExpr -> Translate c HermitM a ()
verifyRetractionT f g r = prefixFailMsg "Retraction verification failed: " $
do (_tyX, tyY) <- funsWithInverseTypes f g
y <- constT (newGlobalIdH "y" tyY)
let lhs = App f (App g (Var y))
rhs = Var y
verifyEqualityLeftToRightT lhs rhs r
retractionBR :: forall c. Maybe (Rewrite c HermitM CoreExpr) -> CoreExpr -> CoreExpr -> BiRewrite c HermitM CoreExpr
retractionBR mr f g = beforeBiR
(prefixFailMsg "Retraction failed: " $
do whenJust (verifyRetractionT f g) mr
y <- idR
(_, tyY) <- funsWithInverseTypes f g
guardMsg (exprKindOrType y `typeAlphaEq` tyY) "type of expression does not match given retraction components."
return y
)
(\ y -> bidirectional
retractionL
(return $ App f (App g y))
)
where
retractionL :: Rewrite c HermitM CoreExpr
retractionL = prefixFailMsg "Retraction failed: " $
withPatFailMsg (wrongExprForm "App f (App g y)") $
do App f' (App g' y) <- idR
guardMsg (exprAlphaEq f f' && exprAlphaEq g g') "given retraction components do not match current expression."
return y
retraction :: Maybe (RewriteH Core) -> CoreString -> CoreString -> BiRewriteH CoreExpr
retraction mr = parse2beforeBiR (retractionBR (extractR <$> mr))