?prevdifflink? - Blame
|
{-# OPTIONS_GHC -Wall #-} ------------------------------------------------------------------------------- {- | Module : Galculator.Engine.LawToRule Description : Engine that extracts rules from laws. Copyright : (c) Paulo Silva License : LGPL Maintainer : paufil@di.uminho.pt Stability : experimental Portability : portable -} ------------------------------------------------------------------------------- module Galculator.Engine.LawToRule ( getRule, getRuleInv ) where import Control.Monad import Data.Existential import Galculator.Rule import Language.Law.Syntax import Language.R.Constraint import Language.R.Match import Language.R.SafeCast import Language.Type.Constraint import Language.Type.Unification ------------------------------------------------------------------------------- getRule :: Law -> Rule getRule (EQUIV m t1 r1 r2) t2 r = do rcns <- rConstraint r1 r cns <- unify $ [t1 :=: t2] ++ rcns Hide t1' <- typeRewrite cns t1 r1' <- rCast cns t1' r1 r' <- rCast cns t1' r r2' <- rCast cns t2 r2 cnsu <- rMatch r1' r' let r2u = rSubst cnsu t2 r2' successEquiv m t2 r r2u getRule (IMPL m t1 r1 r2) t2 r = do rcns <- rConstraint r1 r cns <- unify $ [t1 :=: t2] ++ rcns Hide t1' <- typeRewrite cns t1 r1' <- rCast cns t1' r1 r' <- rCast cns t1' r r2' <- rCast cns t2 r2 cnsu <- rMatch r1' r' let r2u = rSubst cnsu t2 r2' successImpl m t2 r r2u ------------------------------------------------------------------------------- getRuleInv :: Law -> Rule getRuleInv (EQUIV m t1 r1 r2) t2 r = do rcns <- rConstraint r2 r cns <- unify $ [t1 :=: t2] ++ rcns Hide t1' <- typeRewrite cns t1 r2' <- rCast cns t1' r2 r' <- rCast cns t1' r r1' <- rCast cns t2 r1 cnsu <- rMatch r2' r' let r1u = rSubst cnsu t2 r1' successEquiv m t2 r r1u getRuleInv (IMPL _ _ _ _) _ _ = mzero ------------------------------------------------------------------------------- |