| Line No. | Rev | Author | Line |
|---|---|---|---|
| 1 | 1 | paulosilva | |
| 2 | {-# LANGUAGE GADTs, FlexibleContexts #-} | ||
| 3 | {-# OPTIONS_GHC -Wall #-} | ||
| 4 | |||
| 5 | ------------------------------------------------------------------------------- | ||
| 6 | |||
| 7 | {- | | ||
| 8 | Module : Language.R.TypeInference | ||
| 9 | Description : Type inference for the expression 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.R.TypeInference ( | ||
| 22 | infer, | ||
| 23 | inferBin, | ||
| 24 | catchInfer, | ||
| 25 | InfEnv | ||
| 26 | ) where | ||
| 27 | |||
| 28 | import Control.GalcError | ||
| 29 | import Control.Monad.Error | ||
| 30 | import Control.Monad.Fresh | ||
| 31 | import Control.Monad.State | ||
| 32 | import Data.Env | ||
| 33 | import Data.Existential | ||
| 34 | import Data.List | ||
| 35 | import qualified Data.Map as Map | ||
| 36 | import Language.R.SafeCast | ||
| 37 | import Language.R.Syntax | ||
| 38 | import Language.R.SyntaxADT | ||
| 39 | import Language.Type.Constraint | ||
| 40 | import Language.Type.Syntax | ||
| 41 | import Language.Type.Unification | ||
| 42 | |||
| 43 | ------------------------------------------------------------------------------- | ||
| 44 | |||
| 45 | 7 | paulosilva | infer :: (MonadError GalcError m, MonadFresh [String] String m) --, MonadOr m) |
| 46 | 1 | paulosilva | => S -> m RType |
| 47 | infer s = evalStateT (infer' s) emptyEnv | ||
| 48 | |||
| 49 | ------------------------------------------------------------------------------- | ||
| 50 | |||
| 51 | type InfEnv = Env TypeBox | ||
| 52 | |||
| 53 | ------------------------------------------------------------------------------- | ||
| 54 | |||
| 55 | catchInfer :: (Show s, MonadError GalcError m) => s -> m a -> m a | ||
| 56 | catchInfer a f = f `catchError` (\e -> throwError $ InferenceError e (show a)) | ||
| 57 | |||
| 58 | ------------------------------------------------------------------------------- | ||
| 59 | |||
| 60 | addVariableEnv :: MonadState InfEnv m => String -> TypeBox -> m () | ||
| 61 | addVariableEnv s t = modify (addEnv s t) | ||
| 62 | |||
| 63 | ------------------------------------------------------------------------------- | ||
| 64 | |||
| 65 | updateEnvM :: (MonadError GalcError m, MonadState InfEnv m) | ||
| 66 | => [Constraint] -> InfEnv -> m () | ||
| 67 | updateEnvM constr = | ||
| 68 | put . fmap ( \(Hide t) -> maybe (Hide t) id (typeRewrite constr t) ) | ||
| 69 | |||
| 70 | ------------------------------------------------------------------------------- | ||
| 71 | |||
| 72 | getUnifications :: [InfEnv] -> [Constraint] | ||
| 73 | getUnifications = aux . concatMap toList | ||
| 74 | where | ||
| 75 | aux :: [(String,TypeBox)] -> [Constraint] | ||
| 76 | aux [] = [] | ||
| 77 | aux ((n, Hide t):xs) = | ||
| 78 | (map (\(_, Hide t') -> t :=: t') . filter ((==) n . fst) $ xs) ++ aux xs | ||
| 79 | |||
| 80 | ------------------------------------------------------------------------------- | ||
| 81 | |||
| 82 | getFreshT :: MonadFresh [String] String m => m (Type Var) | ||
| 83 | getFreshT = getFreshLift (TVar . ('t':)) | ||
| 84 | |||
| 85 | ------------------------------------------------------------------------------- | ||
| 86 | infer' :: ( | ||
| 87 | MonadFresh [String] String m, | ||
| 88 | MonadError GalcError m, | ||
| 89 | MonadState InfEnv m | ||
| 90 | ) | ||
| 91 | => S -> m RType | ||
| 92 | ------------------------------------------------------------------------------- | ||
| 93 | infer' (RefS _ _) = throwError $ ImpossibleError | ||
| 94 | ------------------------------------------------------------------------------- | ||
| 95 | infer' (RefExtS _ d) = return d | ||
| 96 | ------------------------------------------------------------------------------- | ||
| 97 | infer' (BotS _) = do | ||
| 98 | t1 <- getFreshT | ||
| 99 | t2 <- getFreshT | ||
| 100 | return $ Exists (Rel t1 t2) BOT | ||
| 101 | ------------------------------------------------------------------------------- | ||
| 102 | infer' (TopS _) = do | ||
| 103 | t1 <- getFreshT | ||
| 104 | t2 <- getFreshT | ||
| 105 | return $ Exists (Rel t1 t2) TOP | ||
| 106 | ------------------------------------------------------------------------------- | ||
| 107 | infer' a@(NegS _ ra) = catchInfer a $ do | ||
| 108 | (Exists tr r, envR) <- inferUni ra | ||
| 109 | t1 <- getFreshT; t2 <- getFreshT | ||
| 110 | constr <- unify [tr :=: Rel t1 t2] | ||
| 111 | 7 | paulosilva | Hide t1'' <- typeRewriteE constr t1 |
| 112 | Hide t2'' <- typeRewriteE constr t2 | ||
| 113 | 1 | paulosilva | r' <- rCast constr (Rel t1'' t2'') r |
| 114 | updateEnvM constr envR | ||
| 115 | return $ Exists (Rel t1'' t2'') (NEG r') | ||
| 116 | ------------------------------------------------------------------------------- | ||
| 117 | infer' a@(MeetS _ r1a r2a) = catchInfer a $ do | ||
| 118 | (Exists tr1 r1, Exists tr2 r2, unif, envR) <- inferBin r1a r2a | ||
| 119 | t1 <- getFreshT; t2 <- getFreshT; t1' <- getFreshT; t2' <- getFreshT | ||
| 120 | constr <- unify $ | ||
| 121 | [tr1 :=: Rel t1 t2, tr2 :=: Rel t1' t2', t1 :=: t1', t2 :=: t2'] ++ unif | ||
| 122 | 7 | paulosilva | Hide t1'' <- typeRewriteE constr t1 |
| 123 | Hide t2'' <- typeRewriteE constr t2 | ||
| 124 | 1 | paulosilva | r1' <- rCast constr (Rel t1'' t2'') r1 |
| 125 | r2' <- rCast constr (Rel t1'' t2'') r2 | ||
| 126 | updateEnvM constr envR | ||
| 127 | return $ Exists (Rel t1'' t2'') (MEET r1' r2') | ||
| 128 | ------------------------------------------------------------------------------- | ||
| 129 | infer' a@(JoinS _ r1a r2a) = catchInfer a $ do | ||
| 130 | (Exists tr1 r1, Exists tr2 r2, unif, envR) <- inferBin r1a r2a | ||
| 131 | t1 <- getFreshT; t2 <- getFreshT; t1' <- getFreshT; t2' <- getFreshT | ||
| 132 | constr <- unify $ | ||
| 133 | [tr1 :=: Rel t1 t2, tr2 :=: Rel t1' t2', t1 :=: t1', t2 :=: t2'] ++ unif | ||
| 134 | 7 | paulosilva | Hide t1'' <- typeRewriteE constr t1 |
| 135 | Hide t2'' <- typeRewriteE constr t2 | ||
| 136 | 1 | paulosilva | r1' <- rCast constr (Rel t1'' t2'') r1 |
| 137 | r2' <- rCast constr (Rel t1'' t2'') r2 | ||
| 138 | updateEnvM constr envR | ||
| 139 | return $ Exists (Rel t1'' t2'') (JOIN r1' r2') | ||
| 140 | ------------------------------------------------------------------------------- | ||
| 141 | infer' (IdS _) = do | ||
| 142 | t <- getFreshT | ||
| 143 | return $ Exists (Rel t t) ID | ||
| 144 | ------------------------------------------------------------------------------- | ||
| 145 | infer' a@(ConvS _ ra) = catchInfer a $ do | ||
| 146 | (Exists tr r, envR) <- inferUni ra | ||
| 147 | t1 <- getFreshT; t2 <- getFreshT | ||
| 148 | constr <- unify [tr :=: Rel t1 t2] | ||
| 149 | 7 | paulosilva | Hide t1' <- typeRewriteE constr t1 |
| 150 | Hide t2' <- typeRewriteE constr t2 | ||
| 151 | 1 | paulosilva | r' <- rCast constr (Rel t1' t2') r |
| 152 | updateEnvM constr envR | ||
| 153 | return $ Exists (Rel t2' t1') (CONV r') | ||
| 154 | ------------------------------------------------------------------------------- | ||
| 155 | infer' a@(CompS _ r1a r2a) = catchInfer a $ do | ||
| 156 | (Exists tr1 r1, Exists tr2 r2, unif, envR) <- inferBin r1a r2a | ||
| 157 | t1 <- getFreshT; t2 <- getFreshT; t2' <- getFreshT; t3 <- getFreshT | ||
| 158 | 7 | paulosilva | constr <- unify $ |
| 159 | 1 | paulosilva | [tr1 :=: Rel t3 t2, tr2 :=: Rel t2' t1, t2 :=: t2'] ++ unif |
| 160 | 7 | paulosilva | Hide t1'' <- typeRewriteE constr t1 |
| 161 | Hide t2'' <- typeRewriteE constr t2 | ||
| 162 | Hide t3'' <- typeRewriteE constr t3 | ||
| 163 | 1 | paulosilva | r1' <- rCast constr (Rel t3'' t2'') r1 |
| 164 | r2' <- rCast constr (Rel t2'' t1'') r2 | ||
| 165 | updateEnvM constr envR | ||
| 166 | return $ Exists (Rel t3'' t1'') (COMP t2'' r1' r2') | ||
| 167 | ------------------------------------------------------------------------------- | ||
| 168 | infer' a@(SplitS _ r1a r2a) = catchInfer a $ do | ||
| 169 | (Exists tr1 r1, Exists tr2 r2, unif, envR) <- inferBin r1a r2a | ||
| 170 | t1 <- getFreshT; t2 <- getFreshT; t3 <- getFreshT; t1' <- getFreshT | ||
| 171 | constr <- unify $ | ||
| 172 | [tr1 :=: Rel t2 t1, tr2 :=: Rel t3 t1', t1 :=: t1'] ++ unif | ||
| 173 | 7 | paulosilva | Hide t1'' <- typeRewriteE constr t1 |
| 174 | Hide t2'' <- typeRewriteE constr t2 | ||
| 175 | Hide t3'' <- typeRewriteE constr t3 | ||
| 176 | 1 | paulosilva | r1' <- rCast constr (Rel t2'' t1'') r1 |
| 177 | r2' <- rCast constr (Rel t3'' t1'') r2 | ||
| 178 | updateEnvM constr envR | ||
| 179 | return $ Exists (Rel (Prod t2'' t3'') t1'') (SPLIT r1' r2') | ||
| 180 | ------------------------------------------------------------------------------- | ||
| 181 | infer' a@(OrdS _ ra) = catchInfer a $ do | ||
| 182 | (Exists tr r, envR) <- inferUni ra | ||
| 183 | t <- getFreshT | ||
| 184 | constr <- unify [tr :=: Ord t] | ||
| 185 | 7 | paulosilva | Hide t'' <- typeRewriteE constr t |
| 186 | 1 | paulosilva | r' <- rCast constr (Ord t'') r |
| 187 | updateEnvM constr envR | ||
| 188 | return $ Exists (Rel t'' t'') (ORD r') | ||
| 189 | ------------------------------------------------------------------------------- | ||
| 190 | infer' a@(FunS _ ra) = catchInfer a $ do | ||
| 191 | (Exists tr r, envR) <- inferUni ra | ||
| 192 | t1 <- getFreshT; t2 <- getFreshT | ||
| 193 | constr <- unify [tr :=: Fun t2 t1] | ||
| 194 | 7 | paulosilva | Hide t1'' <- typeRewriteE constr t1 |
| 195 | Hide t2'' <- typeRewriteE constr t2 | ||
| 196 | 1 | paulosilva | r' <- rCast constr (Fun t2'' t1'') r |
| 197 | updateEnvM constr envR | ||
| 198 | return $ Exists (Rel t2'' t1'') (FUN r') | ||
| 199 | ------------------------------------------------------------------------------- | ||
| 200 | infer' a@(LeftsecS _ r1a r2a) = catchInfer a $ do | ||
| 201 | (Exists tr1 r1, Exists tr2 r2, unif, envR) <- inferBin r1a r2a | ||
| 202 | t1 <- getFreshT; t2 <- getFreshT; t3 <- getFreshT | ||
| 203 | constr <- unify $ [tr1 :=: Fun t1 (Prod t2 t3), t2 :=: tr2] ++ unif | ||
| 204 | 7 | paulosilva | Hide t1'' <- typeRewriteE constr t1 |
| 205 | Hide t2'' <- typeRewriteE constr t2 | ||
| 206 | Hide t3'' <- typeRewriteE constr t3 | ||
| 207 | 1 | paulosilva | r2' <- rCast constr t2'' r2 |
| 208 | r1' <- rCast constr (Fun t1'' (Prod t2'' t3'')) r1 | ||
| 209 | updateEnvM constr envR | ||
| 210 | return $ Exists (Fun t1'' t3'') (LEFTSEC t2'' r1' r2') | ||
| 211 | ------------------------------------------------------------------------------- | ||
| 212 | infer' a@(RightsecS _ r1a r2a) = catchInfer a $ do | ||
| 213 | (Exists tr1 r1, Exists tr2 r2, unif, envR) <- inferBin r1a r2a | ||
| 214 | t1 <- getFreshT; t2 <- getFreshT; t3 <- getFreshT | ||
| 215 | constr <- unify $ [tr1 :=: Fun t1 (Prod t2 t3), t3 :=: tr2] ++ unif | ||
| 216 | 7 | paulosilva | Hide t1'' <- typeRewriteE constr t1 |
| 217 | Hide t2'' <- typeRewriteE constr t2 | ||
| 218 | Hide t3'' <- typeRewriteE constr t3 | ||
| 219 | 1 | paulosilva | r2' <- rCast constr t3'' r2 |
| 220 | r1' <- rCast constr (Fun t1'' (Prod t2'' t3'')) r1 | ||
| 221 | updateEnvM constr envR | ||
| 222 | return $ Exists (Fun t1'' t2'') (RIGHTSEC t3'' r1' r2') | ||
| 223 | ------------------------------------------------------------------------------- | ||
| 224 | infer' a@(ApplyS _ r1a r2a) = catchInfer a $ do | ||
| 225 | (Exists tr1 r1, Exists tr2 r2, unif, envR) <- inferBin r1a r2a | ||
| 226 | t1 <- getFreshT; t2 <- getFreshT | ||
| 227 | constr <- unify $ [tr1 :=: Fun t1 t2, t2 :=: tr2] ++ unif | ||
| 228 | 7 | paulosilva | Hide t2'' <- typeRewriteE constr t2 |
| 229 | Hide t1'' <- typeRewriteE constr t1 | ||
| 230 | 1 | paulosilva | r1' <- rCast constr (Fun t1'' t2'') r1 |
| 231 | r2' <- rCast constr t2'' r2 | ||
| 232 | updateEnvM constr envR | ||
| 233 | return $ Exists t1'' (APPLY t2'' r1' r2') | ||
| 234 | ------------------------------------------------------------------------------- | ||
| 235 | infer' (DefS _ n (Hide t)) = return $ Exists t (DEF n t) | ||
| 236 | ------------------------------------------------------------------------------- | ||
| 237 | infer' (VarS _ n) = do | ||
| 238 | t <- getFreshT | ||
| 239 | addVariableEnv n (Hide t) | ||
| 240 | return $ Exists t (Var n) | ||
| 241 | ------------------------------------------------------------------------------- | ||
| 242 | infer' a@(ProdS _ r1a r2a) = catchInfer a $ do | ||
| 243 | (Exists tr1 r1, Exists tr2 r2, unif, envR) <- inferBin r1a r2a | ||
| 244 | t1 <- getFreshT; t2 <- getFreshT; t3 <- getFreshT; t4 <- getFreshT | ||
| 245 | constr <- unify $ [tr1 :=: Rel t3 t1, tr2 :=: Rel t4 t2] ++ unif | ||
| 246 | 7 | paulosilva | Hide t1'' <- typeRewriteE constr t1 |
| 247 | Hide t2'' <- typeRewriteE constr t2 | ||
| 248 | Hide t3'' <- typeRewriteE constr t3 | ||
| 249 | Hide t4'' <- typeRewriteE constr t4 | ||
| 250 | 1 | paulosilva | r1' <- rCast constr (Rel t3'' t1'') r1 |
| 251 | r2' <- rCast constr (Rel t4'' t2'') r2 | ||
| 252 | updateEnvM constr envR | ||
| 253 | return $ Exists (Rel (Prod t3'' t4'') (Prod t1'' t2'')) (PROD r1' r2') | ||
| 254 | ------------------------------------------------------------------------------- | ||
| 255 | infer' a@(EitherS _ r1a r2a) = catchInfer a $ do | ||
| 256 | (Exists tr1 r1, Exists tr2 r2, unif, envR) <- inferBin r1a r2a | ||
| 257 | t1 <- getFreshT; t2 <- getFreshT; t3 <- getFreshT; t4 <- getFreshT | ||
| 258 | constr <- unify $ [tr1 :=: Rel t3 t1, tr2 :=: Rel t4 t2] ++ unif | ||
| 259 | 7 | paulosilva | Hide t1'' <- typeRewriteE constr t1 |
| 260 | Hide t2'' <- typeRewriteE constr t2 | ||
| 261 | Hide t3'' <- typeRewriteE constr t3 | ||
| 262 | Hide t4'' <- typeRewriteE constr t4 | ||
| 263 | 1 | paulosilva | r1' <- rCast constr (Rel t3'' t1'') r1 |
| 264 | r2' <- rCast constr (Rel t4'' t2'') r2 | ||
| 265 | updateEnvM constr envR | ||
| 266 | return $ Exists (Rel (Either t3'' t4'') (Either t1'' t2'')) (EITHER r1' r2') | ||
| 267 | ------------------------------------------------------------------------------- | ||
| 268 | infer' a@(MaybeS _ ra) = catchInfer a $ do | ||
| 269 | (Exists tr r, envR) <- inferUni ra | ||
| 270 | t1 <- getFreshT; t2 <- getFreshT | ||
| 271 | constr <- unify [tr :=: Rel t2 t1] | ||
| 272 | 7 | paulosilva | Hide t1'' <- typeRewriteE constr t1 |
| 273 | Hide t2'' <- typeRewriteE constr t2 | ||
| 274 | 1 | paulosilva | r1' <- rCast constr (Rel t2'' t1'') r |
| 275 | updateEnvM constr envR | ||
| 276 | return $ Exists (Rel (Maybe t2'') (Maybe t1'')) (MAYBE r1') | ||
| 277 | ------------------------------------------------------------------------------- | ||
| 278 | infer' a@(ListS _ ra) = catchInfer a $ do | ||
| 279 | (Exists tr r, envR) <- inferUni ra | ||
| 280 | t1 <- getFreshT; t2 <- getFreshT | ||
| 281 | constr <- unify [tr :=: Rel t2 t1] | ||
| 282 | 7 | paulosilva | Hide t1'' <- typeRewriteE constr t1 |
| 283 | Hide t2'' <- typeRewriteE constr t2 | ||
| 284 | 1 | paulosilva | r1' <- rCast constr (Rel t2'' t1'') r |
| 285 | updateEnvM constr envR | ||
| 286 | return $ Exists (Rel (List t2'') (List t1'')) (LIST r1') | ||
| 287 | ------------------------------------------------------------------------------- | ||
| 288 | infer' a@(SetS _ ra) = catchInfer a $ do | ||
| 289 | (Exists tr r, envR) <- inferUni ra | ||
| 290 | t1 <- getFreshT; t2 <- getFreshT | ||
| 291 | constr <- unify [tr :=: Rel t2 t1] | ||
| 292 | 7 | paulosilva | Hide t1'' <- typeRewriteE constr t1 |
| 293 | Hide t2'' <- typeRewriteE constr t2 | ||
| 294 | 1 | paulosilva | r1' <- rCast constr (Rel t2'' t1'') r |
| 295 | updateEnvM constr envR | ||
| 296 | return $ Exists (Rel (Set t2'') (Set t1'')) (SET r1') | ||
| 297 | ------------------------------------------------------------------------------- | ||
| 298 | infer' a@(MapS _ ra) = catchInfer a $ do | ||
| 299 | (Exists tr r, envR) <- inferUni ra | ||
| 300 | t1 <- getFreshT; t2 <- getFreshT; t3 <- getFreshT | ||
| 301 | constr <- unify [tr :=: Rel t2 t1] | ||
| 302 | 7 | paulosilva | Hide t1'' <- typeRewriteE constr t1 |
| 303 | Hide t2'' <- typeRewriteE constr t2 | ||
| 304 | 1 | paulosilva | r1' <- rCast constr (Rel t2'' t1'') r |
| 305 | updateEnvM constr envR | ||
| 306 | return $ Exists (Rel (Map t3 t2'') (Map t3 t1'')) (MAP r1') | ||
| 307 | ------------------------------------------------------------------------------- | ||
| 308 | 5 | paulosilva | infer' a@(ReynoldsS _ r1a r2a) = catchInfer a $ do |
| 309 | (Exists tr1 r1, Exists tr2 r2, unif, envR) <- inferBin r1a r2a | ||
| 310 | t1 <- getFreshT; t2 <- getFreshT; t3 <- getFreshT; t4 <- getFreshT | ||
| 311 | constr <- unify $ [tr1 :=: Rel t2 t1, tr2 :=: Rel t4 t3] ++ unif | ||
| 312 | 7 | paulosilva | Hide t1' <- typeRewriteE constr t1 |
| 313 | Hide t2' <- typeRewriteE constr t2 | ||
| 314 | Hide t3' <- typeRewriteE constr t3 | ||
| 315 | Hide t4' <- typeRewriteE constr t4 | ||
| 316 | 5 | paulosilva | r1' <- rCast constr (Rel t2' t1') r1 |
| 317 | r2' <- rCast constr (Rel t4' t3') r2 | ||
| 318 | updateEnvM constr envR | ||
| 319 | return $ Exists (Rel (Fun t2' t4') (Fun t1' t3')) (REYNOLDS r1' r2') | ||
| 320 | ------------------------------------------------------------------------------- | ||
| 321 | 1 | paulosilva | infer' (FIdS _) = do |
| 322 | t <- getFreshT | ||
| 323 | return $ Exists (Fun t t) FId | ||
| 324 | ------------------------------------------------------------------------------- | ||
| 325 | infer' a@(FCompS _ r1a r2a) = catchInfer a $ do | ||
| 326 | (Exists tr1 r1, Exists tr2 r2, unif, envR) <- inferBin r1a r2a | ||
| 327 | t1 <- getFreshT; t2 <- getFreshT; t3 <- getFreshT; t2' <- getFreshT | ||
| 328 | constr <- unify $ | ||
| 329 | [tr1 :=: Fun t1 t2, tr2 :=: Fun t2' t3, t2 :=: t2'] ++ unif | ||
| 330 | 7 | paulosilva | Hide t1'' <- typeRewriteE constr t1 |
| 331 | Hide t2'' <- typeRewriteE constr t2 | ||
| 332 | Hide t3'' <- typeRewriteE constr t3 | ||
| 333 | 1 | paulosilva | r1' <- rCast constr (Fun t1'' t2'') r1 |
| 334 | r2' <- rCast constr (Fun t2'' t3'') r2 | ||
| 335 | updateEnvM constr envR | ||
| 336 | return $ Exists (Fun t1'' t3'') (FComp t2'' r1' r2') | ||
| 337 | ------------------------------------------------------------------------------- | ||
| 338 | infer' (OIdS _) = do | ||
| 339 | t <- getFreshT | ||
| 340 | return $ Exists (Ord t) OId | ||
| 341 | ------------------------------------------------------------------------------- | ||
| 342 | infer' a@(OCompS _ r1a r2a) = catchInfer a $ do | ||
| 343 | (Exists tr1 r1, Exists tr2 r2, unif, envR) <- inferBin r1a r2a | ||
| 344 | t <- getFreshT; t' <- getFreshT | ||
| 345 | constr <- unify $ [tr1 :=: Ord t, tr2 :=: Ord t', t :=: t'] ++ unif | ||
| 346 | 7 | paulosilva | Hide t'' <- typeRewriteE constr t |
| 347 | 1 | paulosilva | r1' <- rCast constr (Ord t'') r1 |
| 348 | r2' <- rCast constr (Ord t'') r2 | ||
| 349 | updateEnvM constr envR | ||
| 350 | return $ Exists (Ord t'') (OComp r1' r2') | ||
| 351 | ------------------------------------------------------------------------------- | ||
| 352 | infer' a@(OConvS _ ra) = catchInfer a $ do | ||
| 353 | (Exists tr r, envR) <- inferUni ra | ||
| 354 | t <- getFreshT | ||
| 355 | constr <- unify [tr :=: Ord t] | ||
| 356 | 7 | paulosilva | Hide t'' <- typeRewriteE constr t |
| 357 | 1 | paulosilva | r' <- rCast constr (Ord t'') r |
| 358 | updateEnvM constr envR | ||
| 359 | return $ Exists (Ord t'') (OConv r') | ||
| 360 | ------------------------------------------------------------------------------- | ||
| 361 | infer' a@(OProdS _ ra) = catchInfer a $ do | ||
| 362 | (Exists tr r, envR) <- inferUni ra | ||
| 363 | t <- getFreshT | ||
| 364 | constr <- unify [tr :=: Ord t] | ||
| 365 | 7 | paulosilva | Hide t'' <- typeRewriteE constr t |
| 366 | 1 | paulosilva | r' <- rCast constr (Ord t'') r |
| 367 | updateEnvM constr envR | ||
| 368 | return $ Exists (Ord (Prod t'' t'')) (OProd r') | ||
| 369 | ------------------------------------------------------------------------------- | ||
| 370 | infer' a@(OJoinS _ ra) = catchInfer a $ do | ||
| 371 | (Exists tr r, envR) <- inferUni ra | ||
| 372 | t <- getFreshT | ||
| 373 | constr <- unify [tr :=: Ord t] | ||
| 374 | 7 | paulosilva | Hide t'' <- typeRewriteE constr t |
| 375 | 1 | paulosilva | r' <- rCast constr (Ord t'') r |
| 376 | updateEnvM constr envR | ||
| 377 | return $ Exists (Fun t'' (Prod t'' t'')) (OJoin r') | ||
| 378 | ------------------------------------------------------------------------------- | ||
| 379 | infer' a@(OMeetS _ ra) = catchInfer a $ do | ||
| 380 | (Exists tr r, envR) <- inferUni ra | ||
| 381 | t <- getFreshT | ||
| 382 | constr <- unify [tr :=: Ord t] | ||
| 383 | 7 | paulosilva | Hide t'' <- typeRewriteE constr t |
| 384 | 1 | paulosilva | r' <- rCast constr (Ord t'') r |
| 385 | updateEnvM constr envR | ||
| 386 | return $ Exists (Fun t'' (Prod t'' t'')) (OMeet r') | ||
| 387 | ------------------------------------------------------------------------------- | ||
| 388 | infer' a@(OMaxS _ ra) = catchInfer a $ do | ||
| 389 | (Exists tr r, envR) <- inferUni ra | ||
| 390 | t <- getFreshT | ||
| 391 | constr <- unify [tr :=: Ord t] | ||
| 392 | 7 | paulosilva | Hide t'' <- typeRewriteE constr t |
| 393 | 1 | paulosilva | r' <- rCast constr (Ord t'') r |
| 394 | updateEnvM constr envR | ||
| 395 | return $ Exists t'' (OMax r') | ||
| 396 | ------------------------------------------------------------------------------- | ||
| 397 | infer' a@(OMinS _ ra) = catchInfer a $ do | ||
| 398 | (Exists tr r, envR) <- inferUni ra | ||
| 399 | t <- getFreshT | ||
| 400 | constr <- unify [tr :=: Ord t] | ||
| 401 | 7 | paulosilva | Hide t'' <- typeRewriteE constr t |
| 402 | 1 | paulosilva | r' <- rCast constr (Ord t'') r |
| 403 | updateEnvM constr envR | ||
| 404 | return $ Exists t'' (OMin r') | ||
| 405 | ------------------------------------------------------------------------------- | ||
| 406 | infer' a@(GDefS _ n f1a f2a o1a o2a) = catchInfer a $ do | ||
| 407 | (Exists tf1 f1, envF1) <- inferUni f1a | ||
| 408 | (Exists tf2 f2, envF2) <- inferUni f2a | ||
| 409 | (Exists to1 o1, envO1) <- inferUni o1a | ||
| 410 | (Exists to2 o2, envO2) <- inferUni o2a | ||
| 411 | t1 <- getFreshT; t2 <- getFreshT | ||
| 412 | t1' <- getFreshT; t2' <- getFreshT | ||
| 413 | t1'' <- getFreshT; t2'' <- getFreshT | ||
| 414 | let envR = envF1 `Map.union` envF2 `Map.union` envO1 `Map.union` envO2 | ||
| 415 | unif = getUnifications [envF1,envF2,envO1,envO2] | ||
| 416 | constr <- unify $ | ||
| 417 | [tf1 :=: Fun t1 t2, tf2 :=: Fun t2' t1', to1 :=: Ord t1'', to2 :=: Ord t2'', | ||
| 418 | t1 :=: t1', t1' :=: t1'', t2 :=: t2', t2' :=: t2''] ++ unif | ||
| 419 | 7 | paulosilva | Hide t1''' <- typeRewriteE constr t1 |
| 420 | Hide t2''' <- typeRewriteE constr t2 | ||
| 421 | 1 | paulosilva | f1' <- rCast constr (Fun t1''' t2''') f1 |
| 422 | f2' <- rCast constr (Fun t2''' t1''') f2 | ||
| 423 | o1' <- rCast constr (Ord t1''') o1 | ||
| 424 | o2' <- rCast constr (Ord t2''') o2 | ||
| 425 | updateEnvM constr envR | ||
| 426 | return $ Exists (GC t1''' t2''') (GDef n f1' f2' o1' o2') | ||
| 427 | ------------------------------------------------------------------------------- | ||
| 428 | infer' (GIdS _) = do | ||
| 429 | t <- getFreshT | ||
| 430 | return $ Exists (GC t t) GId | ||
| 431 | ------------------------------------------------------------------------------- | ||
| 432 | infer' a@(GCompS _ r1a r2a) = catchInfer a $ do | ||
| 433 | (Exists tr1 r1, Exists tr2 r2, unif, envR) <- inferBin r1a r2a | ||
| 434 | t1 <- getFreshT; t2 <- getFreshT; t3 <- getFreshT; t2' <- getFreshT | ||
| 435 | constr <- unify $ | ||
| 436 | [tr1 :=: GC t1 t2, tr2 :=: GC t2' t3, t2 :=: t2'] ++ unif | ||
| 437 | 7 | paulosilva | Hide t1'' <- typeRewriteE constr t1 |
| 438 | Hide t2'' <- typeRewriteE constr t2 | ||
| 439 | Hide t3'' <- typeRewriteE constr t3 | ||
| 440 | 1 | paulosilva | r1' <- rCast constr (GC t1'' t2'') r1 |
| 441 | r2' <- rCast constr (GC t2'' t3'') r2 | ||
| 442 | updateEnvM constr envR | ||
| 443 | return $ Exists (GC t1'' t3'') (GComp t2'' r1' r2') | ||
| 444 | ------------------------------------------------------------------------------- | ||
| 445 | infer' a@(GConvS _ ra) = catchInfer a $ do | ||
| 446 | (Exists tr r, envR) <- inferUni ra | ||
| 447 | t1 <- getFreshT; t2 <- getFreshT | ||
| 448 | constr <- unify [tr :=: GC t1 t2] | ||
| 449 | 7 | paulosilva | Hide t1'' <- typeRewriteE constr t1 |
| 450 | Hide t2'' <- typeRewriteE constr t2 | ||
| 451 | 1 | paulosilva | r' <- rCast constr (GC t1'' t2'') r |
| 452 | updateEnvM constr envR | ||
| 453 | return $ Exists (GC t2'' t1'') (GConv r') | ||
| 454 | ------------------------------------------------------------------------------- | ||
| 455 | infer' a@(GLAdjS _ ra) = catchInfer a $ do | ||
| 456 | (Exists tr r, envR) <- inferUni ra | ||
| 457 | t1 <- getFreshT; t2 <- getFreshT | ||
| 458 | constr <- unify [tr :=: GC t1 t2] | ||
| 459 | 7 | paulosilva | Hide t1'' <- typeRewriteE constr t1 |
| 460 | Hide t2'' <- typeRewriteE constr t2 | ||
| 461 | 1 | paulosilva | r' <- rCast constr (GC t1'' t2'') r |
| 462 | updateEnvM constr envR | ||
| 463 | return $ Exists (Fun t1'' t2'') (GLAdj r') | ||
| 464 | ------------------------------------------------------------------------------- | ||
| 465 | infer' a@(GUAdjS _ ra) = catchInfer a $ do | ||
| 466 | (Exists tr r, envR) <- inferUni ra | ||
| 467 | t1 <- getFreshT; t2 <- getFreshT | ||
| 468 | constr <- unify [tr :=: GC t1 t2] | ||
| 469 | 7 | paulosilva | Hide t1'' <- typeRewriteE constr t1 |
| 470 | Hide t2'' <- typeRewriteE constr t2 | ||
| 471 | 1 | paulosilva | r' <- rCast constr (GC t1'' t2'') r |
| 472 | updateEnvM constr envR | ||
| 473 | return $ Exists (Fun t2'' t1'') (GUAdj r') | ||
| 474 | ------------------------------------------------------------------------------- | ||
| 475 | infer' a@(GLOrdS _ ra) = catchInfer a $ do | ||
| 476 | (Exists tr r, envR) <- inferUni ra | ||
| 477 | t1 <- getFreshT; t2 <- getFreshT | ||
| 478 | constr <- unify [tr :=: GC t1 t2] | ||
| 479 | 7 | paulosilva | Hide t1'' <- typeRewriteE constr t1 |
| 480 | Hide t2'' <- typeRewriteE constr t2 | ||
| 481 | 1 | paulosilva | r' <- rCast constr (GC t1'' t2'') r |
| 482 | updateEnvM constr envR | ||
| 483 | return $ Exists (Ord t1'') (GLOrd t2'' r') | ||
| 484 | ------------------------------------------------------------------------------- | ||
| 485 | infer' a@(GUOrdS _ ra) = catchInfer a $ do | ||
| 486 | (Exists tr r, envR) <- inferUni ra | ||
| 487 | t1 <- getFreshT; t2 <- getFreshT | ||
| 488 | constr <- unify [tr :=: GC t1 t2] | ||
| 489 | 7 | paulosilva | Hide t1'' <- typeRewriteE constr t1 |
| 490 | Hide t2'' <- typeRewriteE constr t2 | ||
| 491 | 1 | paulosilva | r' <- rCast constr (GC t1'' t2'') r |
| 492 | updateEnvM constr envR | ||
| 493 | return $ Exists (Ord t2'') (GUOrd t1'' r') | ||
| 494 | ------------------------------------------------------------------------------- | ||
| 495 | |||
| 496 | 7 | paulosilva | inferUni :: (MonadError GalcError m, |
| 497 | 1 | paulosilva | MonadState InfEnv m, |
| 498 | MonadFresh [String] String m) | ||
| 499 | => S -> m (RType, InfEnv) | ||
| 500 | inferUni r = do | ||
| 501 | x <- infer' r | ||
| 502 | envR <- get | ||
| 503 | put emptyEnv | ||
| 504 | return (x, envR) | ||
| 505 | |||
| 506 | ------------------------------------------------------------------------------- | ||
| 507 | |||
| 508 | 7 | paulosilva | inferBin :: (MonadError GalcError m, |
| 509 | 1 | paulosilva | MonadState InfEnv m, |
| 510 | MonadFresh [String] String m) | ||
| 511 | => S -> S -> m (RType, RType, [Constraint], InfEnv) | ||
| 512 | inferBin r1 r2 = do | ||
| 513 | (x, envR1) <- inferUni r1 | ||
| 514 | (y, envR2) <- inferUni r2 | ||
| 515 | let envR = envR1 `Map.union` envR2 | ||
| 516 | unif = getUnifications [envR1,envR2] | ||
| 517 | return (x,y,unif,envR) | ||
| 518 | |||
| 519 | ------------------------------------------------------------------------------- | ||
| 520 |