| Line No. | Rev | Author | Line |
|---|---|---|---|
| 1 | 1 | paulosilva | |
| 2 | {-# OPTIONS_GHC -Wall #-} | ||
| 3 | |||
| 4 | ------------------------------------------------------------------------------- | ||
| 5 | |||
| 6 | {- | | ||
| 7 | Module : Galculator.Engine.LawToRule | ||
| 8 | Description : Engine that extracts rules from laws. | ||
| 9 | Copyright : (c) Paulo Silva | ||
| 10 | License : LGPL | ||
| 11 | |||
| 12 | Maintainer : paufil@di.uminho.pt | ||
| 13 | Stability : experimental | ||
| 14 | Portability : portable | ||
| 15 | |||
| 16 | -} | ||
| 17 | |||
| 18 | ------------------------------------------------------------------------------- | ||
| 19 | |||
| 20 | module Galculator.Engine.LawToRule ( | ||
| 21 | getRule, | ||
| 22 | getRuleInv | ||
| 23 | ) where | ||
| 24 | |||
| 25 | import Control.Monad | ||
| 26 | import Data.Existential | ||
| 27 | import Galculator.Rule | ||
| 28 | import Language.Law.Syntax | ||
| 29 | import Language.R.Constraint | ||
| 30 | import Language.R.Match | ||
| 31 | import Language.R.SafeCast | ||
| 32 | import Language.Type.Constraint | ||
| 33 | import Language.Type.Unification | ||
| 34 | |||
| 35 | ------------------------------------------------------------------------------- | ||
| 36 | |||
| 37 | getRule :: Law -> Rule | ||
| 38 | getRule (EQUIV m t1 r1 r2) t2 r = do | ||
| 39 | rcns <- rConstraint r1 r | ||
| 40 | cns <- unify $ [t1 :=: t2] ++ rcns | ||
| 41 | Hide t1' <- typeRewrite cns t1 | ||
| 42 | r1' <- rCast cns t1' r1 | ||
| 43 | r' <- rCast cns t1' r | ||
| 44 | r2' <- rCast cns t2 r2 | ||
| 45 | cnsu <- rMatch r1' r' | ||
| 46 | let r2u = rSubst cnsu t2 r2' | ||
| 47 | successEquiv m t2 r r2u | ||
| 48 | |||
| 49 | getRule (IMPL m t1 r1 r2) t2 r = do | ||
| 50 | rcns <- rConstraint r1 r | ||
| 51 | cns <- unify $ [t1 :=: t2] ++ rcns | ||
| 52 | Hide t1' <- typeRewrite cns t1 | ||
| 53 | r1' <- rCast cns t1' r1 | ||
| 54 | r' <- rCast cns t1' r | ||
| 55 | r2' <- rCast cns t2 r2 | ||
| 56 | cnsu <- rMatch r1' r' | ||
| 57 | let r2u = rSubst cnsu t2 r2' | ||
| 58 | successImpl m t2 r r2u | ||
| 59 | |||
| 60 | ------------------------------------------------------------------------------- | ||
| 61 | |||
| 62 | getRuleInv :: Law -> Rule | ||
| 63 | getRuleInv (EQUIV m t1 r1 r2) t2 r = do | ||
| 64 | rcns <- rConstraint r2 r | ||
| 65 | cns <- unify $ [t1 :=: t2] ++ rcns | ||
| 66 | Hide t1' <- typeRewrite cns t1 | ||
| 67 | r2' <- rCast cns t1' r2 | ||
| 68 | r' <- rCast cns t1' r | ||
| 69 | r1' <- rCast cns t2 r1 | ||
| 70 | cnsu <- rMatch r2' r' | ||
| 71 | let r1u = rSubst cnsu t2 r1' | ||
| 72 | successEquiv m t2 r r1u | ||
| 73 | getRuleInv (IMPL _ _ _ _) _ _ = mzero | ||
| 74 | |||
| 75 | ------------------------------------------------------------------------------- | ||
| 76 |