| Line No. | Rev | Author | Line |
|---|---|---|---|
| 1 | 1 | paulosilva | |
| 2 | {-# LANGUAGE FlexibleContexts #-} | ||
| 3 | {-# OPTIONS_GHC -Wall #-} | ||
| 4 | |||
| 5 | ------------------------------------------------------------------------------- | ||
| 6 | |||
| 7 | {- | | ||
| 8 | Module : Language.Law.TypeInference | ||
| 9 | Description : Type inference for the law representation. | ||
| 10 | Copyright : (c) Paulo Silva | ||
| 11 | License : LGPL | ||
| 12 | |||
| 13 | Maintainer : paufil@di.uminho.pt | ||
| 14 | Stability : experimental | ||
| 15 | Portability : portable | ||
| 16 | |||
| 17 | -} | ||
| 18 | |||
| 19 | ------------------------------------------------------------------------------- | ||
| 20 | |||
| 21 | module Language.Law.TypeInference ( | ||
| 22 | infer | ||
| 23 | ) where | ||
| 24 | |||
| 25 | import Control.GalcError | ||
| 26 | 3 | paulosilva | import Control.MonadOr |
| 27 | 1 | paulosilva | import Control.Monad.Error |
| 28 | import Control.Monad.Fresh | ||
| 29 | import Control.Monad.State | ||
| 30 | import Data.Existential | ||
| 31 | import Data.Env | ||
| 32 | import Language.Law.Syntax | ||
| 33 | import Language.Law.SyntaxADT | ||
| 34 | import Language.R.SafeCast | ||
| 35 | import qualified Language.R.TypeInference as R | ||
| 36 | import Language.Type.Constraint | ||
| 37 | import Language.Type.Unification | ||
| 38 | |||
| 39 | ------------------------------------------------------------------------------- | ||
| 40 | |||
| 41 | 3 | paulosilva | infer :: (MonadOr m, MonadError GalcError m, MonadFresh [String] String m) |
| 42 | 1 | paulosilva | => LawS -> m Law |
| 43 | infer s = evalStateT (infer' s) emptyEnv | ||
| 44 | |||
| 45 | ------------------------------------------------------------------------------- | ||
| 46 | 3 | paulosilva | infer' :: (MonadOr m, MonadError GalcError m, MonadState R.InfEnv m, MonadFresh [String] String m) |
| 47 | 1 | paulosilva | => LawS -> m Law |
| 48 | ------------------------------------------------------------------------------- | ||
| 49 | infer' a@(EquivS _ ident r1a r2a) = R.catchInfer a $ do | ||
| 50 | (Exists tr1 r1, Exists tr2 r2, unif, _) <- R.inferBin r1a r2a | ||
| 51 | constr <- unify $ [tr1 :=: tr2] ++ unif | ||
| 52 | Hide t1' <- typeRewrite constr tr1 | ||
| 53 | r1' <- rCast constr t1' r1 | ||
| 54 | r2' <- rCast constr t1' r2 | ||
| 55 | return $ EQUIV (Meta {name = ident, ruleType = Nothing}) t1' r1' r2' | ||
| 56 | ------------------------------------------------------------------------------- | ||
| 57 | infer' a@(ImplS _ ident r1a r2a) = R.catchInfer a $ do | ||
| 58 | (Exists tr1 r1, Exists tr2 r2, unif, _) <- R.inferBin r1a r2a | ||
| 59 | constr <- unify $ [tr1 :=: tr2] ++ unif | ||
| 60 | Hide t1' <- typeRewrite constr tr1 | ||
| 61 | r1' <- rCast constr t1' r1 | ||
| 62 | r2' <- rCast constr t1' r2 | ||
| 63 | return $ IMPL (Meta {name = ident, ruleType = Nothing}) t1' r1' r2' | ||
| 64 | ------------------------------------------------------------------------------- | ||
| 65 | |||
| 66 |