| -- |
| -- Copyright 2018, Data61 |
| -- Commonwealth Scientific and Industrial Research Organisation (CSIRO) |
| -- ABN 41 687 119 230. |
| -- |
| -- This software may be distributed and modified according to the terms of |
| -- the GNU General Public License version 2. Note that NO WARRANTY is provided. |
| -- See "LICENSE_GPLv2.txt" for details. |
| -- |
| -- @TAG(DATA61_GPL) |
| -- |
| |
| {- LANGUAGE AllowAmbiguousTypes -} |
| {-# LANGUAGE DataKinds #-} |
| {- LANGUAGE DeriveDataTypeable -} |
| {-# LANGUAGE DeriveFunctor #-} |
| {-# LANGUAGE ExistentialQuantification #-} |
| {-# LANGUAGE FlexibleContexts #-} |
| {-# LANGUAGE FlexibleInstances #-} |
| {-# LANGUAGE GADTs #-} |
| {-# LANGUAGE GeneralizedNewtypeDeriving #-} |
| {- LANGUAGE InstanceSigs -} |
| {-# LANGUAGE KindSignatures #-} |
| {-# LANGUAGE LambdaCase #-} |
| {-# LANGUAGE MultiWayIf #-} |
| {-# LANGUAGE PatternGuards #-} |
| {-# LANGUAGE PolyKinds #-} |
| {-# LANGUAGE Rank2Types #-} |
| {-# LANGUAGE ScopedTypeVariables #-} |
| {- LANGUAGE StandaloneDeriving #-} |
| {-# LANGUAGE TupleSections #-} |
| {-# LANGUAGE TypeFamilies #-} |
| {-# LANGUAGE TypeOperators #-} |
| {-# LANGUAGE UndecidableInstances #-} |
| |
| module Cogent.Inference where |
| |
| import Cogent.Common.Syntax |
| import Cogent.Common.Types |
| import Cogent.Compiler |
| import Cogent.Core |
| import Cogent.Dargent.Allocation |
| import Cogent.Dargent.Util |
| import Cogent.Util |
| import Cogent.PrettyPrint (indent') |
| import Data.Ex |
| import Data.Fin |
| import Data.Nat |
| import qualified Data.OMap as OM |
| import Data.PropEq |
| import Data.Vec hiding (repeat, splitAt, length, zipWith, zip, unzip) |
| import qualified Data.Vec as Vec |
| |
| import Control.Applicative |
| import Control.Arrow |
| import Control.Monad.Except hiding (fmap, forM_) |
| import Control.Monad.Reader hiding (fmap, forM_) |
| import Control.Monad.State hiding (fmap, forM_) |
| import Control.Monad.Trans.Maybe |
| import Data.Foldable (forM_) |
| import Data.Function (on) |
| import qualified Data.IntMap as IM |
| import Data.Map (Map) |
| import Data.Maybe (isJust) |
| import qualified Data.Map as M |
| import Data.Monoid |
| #if __GLASGOW_HASKELL__ < 709 |
| import Data.Traversable(traverse) |
| #endif |
| import Lens.Micro (_2) |
| import Lens.Micro.Mtl (view) |
| import Text.PrettyPrint.ANSI.Leijen (Pretty, pretty) |
| import qualified Unsafe.Coerce as Unsafe (unsafeCoerce) -- NOTE: used safely to coerce phantom types only |
| |
| import Debug.Trace |
| |
| guardShow :: String -> Bool -> TC t v b () |
| guardShow x b = unless b $ TC (throwError $ "GUARD: " ++ x) |
| |
| guardShow' :: String -> [String] -> Bool -> TC t v b () |
| guardShow' mh mb b = unless b $ TC (throwError $ "GUARD: " ++ mh ++ "\n" ++ unlines mb) |
| |
| -- ---------------------------------------------------------------------------- |
| -- Type reconstruction |
| |
| -- Types that don't have the same representation / don't satisfy subtyping. |
| isUpcastable :: (Show b, Eq b) => Type t b -> Type t b -> TC t v b Bool |
| isUpcastable (TPrim p1) (TPrim p2) = return $ isSubtypePrim p1 p2 |
| isUpcastable (TSum s1) (TSum s2) = do |
| c1 <- flip allM s1 (\(c,(t,b)) -> case lookup c s2 of |
| Nothing -> return False |
| Just (t',b') -> (&&) <$> t `isSubtype` t' <*> pure (b == b')) |
| c2 <- flip allM s2 (\(c,(t,b)) -> return $ case lookup c s1 of Nothing -> b; Just _ -> True) -- other tags are all taken |
| return $ c1 && c2 |
| isUpcastable _ _ = return False |
| |
| isSubtype :: (Show b, Eq b) => Type t b -> Type t b -> TC t v b Bool |
| isSubtype t1 t2 = runMaybeT (t1 `lub` t2) >>= \case Just t -> return $ t == t2 |
| Nothing -> return False |
| |
| unroll :: RecParName -> RecContext (Type t b) -> Type t b |
| unroll v (Just ctxt) = erp (Just ctxt) (ctxt M.! v) |
| where |
| -- Embed rec pars |
| erp :: RecContext (Type t b) -> Type t b -> Type t b |
| erp c (TCon n ts s) = TCon n (map (erp c) ts) s |
| erp c (TFun t1 t2) = TFun (erp c t1) (erp c t2) |
| erp c (TSum r) = TSum $ map (\(a,(t,b)) -> (a, (erp c t, b))) r |
| erp c (TProduct t1 t2) = TProduct (erp c t1) (erp c t2) |
| erp (Just c) t@(TRecord rp fs s) = |
| let c' = case rp of Rec v -> M.insert v t c; _ -> c |
| in TRecord rp (map (\(a,(t,b)) -> (a, (erp (Just c') t, b))) fs) s |
| -- Context must be Nothing at this point |
| erp c (TRPar v Nothing) = TRPar v c |
| #ifdef BUILTIN_ARRAYS |
| erp c (TArray t l s h) = TArray (erp c t) l s h |
| #endif |
| erp _ t = t |
| |
| bound :: (Show b, Eq b) => Bound -> Type t b -> Type t b -> MaybeT (TC t v b) (Type t b) |
| bound _ t1 t2 | t1 == t2 = return t1 |
| bound b (TRecord rp1 fs1 s1) (TRecord rp2 fs2 s2) |
| | map fst fs1 == map fst fs2, s1 == s2, rp1 == rp2 = do |
| let op = case b of LUB -> (||); GLB -> (&&) |
| blob <- flip3 zipWithM fs2 fs1 $ \(f1,(t1,b1)) (_, (t2,b2)) -> do |
| t <- bound b t1 t2 |
| ok <- lift $ if b1 == b2 then return True |
| else kindcheck t >>= \k -> return (canDiscard k) |
| return ((f1, (t, b1 `op` b2)), ok) |
| let (fs, oks) = unzip blob |
| if and oks then return $ TRecord rp1 fs s1 |
| else MaybeT (return Nothing) |
| bound b (TSum s1) (TSum s2) | s1' <- M.fromList s1, s2' <- M.fromList s2, M.keys s1' == M.keys s2' = do |
| let op = case b of LUB -> (&&); GLB -> (||) |
| s <- flip3 unionWithKeyM s2' s1' $ \k (t1,b1) (t2,b2) -> (,) <$> bound b t1 t2 <*> pure (b1 `op` b2) |
| return $ TSum $ M.toList s |
| bound b (TProduct t11 t12) (TProduct t21 t22) = TProduct <$> bound b t11 t21 <*> bound b t12 t22 |
| bound b (TCon c1 t1 s1) (TCon c2 t2 s2) | c1 == c2, s1 == s2 = TCon c1 <$> zipWithM (bound b) t1 t2 <*> pure s1 |
| bound b (TFun t1 s1) (TFun t2 s2) = TFun <$> bound (theOtherB b) t1 t2 <*> bound b s1 s2 |
| -- At this point, we can assume recursive parameters and records agree |
| bound b t1@(TRecord rp fs s) t2@(TRPar v ctxt) = return t2 |
| bound b t1@(TRPar v ctxt) t2@(TRecord rp fs s) = return t2 |
| bound b t1@(TRPar v1 c1) t2@(TRPar v2 c2) = return t2 |
| #ifdef BUILTIN_ARRAYS |
| bound b (TArray t1 l1 s1 mhole1) (TArray t2 l2 s2 mhole2) |
| | l1 == l2, s1 == s2 = do |
| t <- bound b t1 t2 |
| ok <- lift $ case (mhole1, mhole2) of |
| (Nothing, Nothing) -> return True |
| (Just i1, Just i2) -> return $ i1 == i2 -- FIXME: change to propositional equality / zilinc |
| _ -> kindcheck t >>= \k -> return (canDiscard k) |
| let mhole = combineHoles b mhole1 mhole2 |
| if ok then return $ TArray t l1 s1 mhole |
| else MaybeT (return Nothing) |
| where |
| combineHoles b Nothing Nothing = Nothing |
| combineHoles b (Just i1) (Just _ ) = Just i1 |
| combineHoles b Nothing (Just i2) = case b of GLB -> Nothing; LUB -> Just i2 |
| combineHoles b (Just i1) Nothing = case b of GLB -> Nothing; LUB -> Just i1 |
| #endif |
| bound _ t1 t2 = __impossible ("bound: not comparable:\n" ++ show t1 ++ "\n" ++ |
| "----------------------------------------\n" ++ show t2 ++ "\n") |
| |
| lub :: (Show b, Eq b) => Type t b -> Type t b -> MaybeT (TC t v b) (Type t b) |
| lub = bound LUB |
| |
| glb :: (Show b, Eq b) => Type t b -> Type t b -> MaybeT (TC t v b) (Type t b) |
| glb = bound GLB |
| |
| -- checkUExpr_B :: UntypedExpr -> TC t v Bool |
| -- checkUExpr_B (E (Op op [e])) = return True |
| -- checkUExpr_B (E (Op op [e1,e2])) = return True |
| -- checkUExpr_B _ = return True |
| |
| |
| bang :: Type t b -> Type t b |
| bang (TVar v) = TVarBang v |
| bang (TVarBang v) = TVarBang v |
| bang (TVarUnboxed v) = TVarUnboxed v |
| bang (TCon n ts s) = TCon n (map bang ts) (bangSigil s) |
| bang (TFun ti to) = TFun ti to |
| bang (TPrim i) = TPrim i |
| bang (TString) = TString |
| bang (TSum ts) = TSum (map (second $ first bang) ts) |
| bang (TProduct t1 t2) = TProduct (bang t1) (bang t2) |
| bang (TRecord rp ts s) = TRecord rp (map (second $ first bang) ts) (bangSigil s) |
| bang (TRPar n ctxt) = TRPar n ctxt |
| bang (TUnit) = TUnit |
| #ifdef BUILTIN_ARRAYS |
| bang (TArray t l s tkns) = TArray (bang t) l (bangSigil s) tkns |
| #endif |
| |
| unbox :: Type t b -> Type t b |
| unbox (TVar v) = TVarUnboxed v |
| unbox (TVarBang v) = TVarUnboxed v |
| unbox (TVarUnboxed v) = TVarUnboxed v |
| unbox (TCon n ts s) = TCon n ts (unboxSigil s) |
| unbox (TRecord rp ts s)= TRecord rp ts (unboxSigil s) |
| unbox t = t -- NOTE that @#@ type operator behaves differently to @!@. |
| -- The application of @#@ should NOT be pushed inside of a |
| -- data type. / zilinc |
| |
| |
| substitute :: Vec t (Type u b) -> Type t b -> Type u b |
| substitute vs (TVar v) = vs `at` v |
| substitute vs (TVarBang v) = bang (vs `at` v) |
| substitute vs (TVarUnboxed v) = unbox (vs `at` v) |
| substitute vs (TCon n ts s) = TCon n (map (substitute vs) ts) s |
| substitute vs (TFun ti to) = TFun (substitute vs ti) (substitute vs to) |
| substitute _ (TPrim i) = TPrim i |
| substitute _ (TString) = TString |
| substitute vs (TProduct t1 t2) = TProduct (substitute vs t1) (substitute vs t2) |
| substitute vs (TRecord rp ts s) = TRecord rp (map (second (first $ substitute vs)) ts) s |
| substitute vs (TSum ts) = TSum (map (second (first $ substitute vs)) ts) |
| substitute _ (TUnit) = TUnit |
| substitute vs (TRPar v m) = TRPar v $ fmap (M.map (substitute vs)) m |
| #ifdef BUILTIN_ARRAYS |
| substitute vs (TArray t l s mhole) = TArray (substitute vs t) (substituteLE vs l) s (fmap (substituteLE vs) mhole) |
| #endif |
| |
| substituteL :: [DataLayout BitRange] -> Type t b -> Type t b |
| substituteL ls (TCon n ts s) = TCon n (map (substituteL ls) ts) s |
| substituteL ls (TFun ti to) = TFun (substituteL ls ti) (substituteL ls to) |
| substituteL ls (TProduct t1 t2) = TProduct (substituteL ls t1) (substituteL ls t2) |
| substituteL ls (TRecord rp ts s) = TRecord rp (map (second (first $ substituteL ls)) ts) (substituteS ls s) |
| substituteL ls (TSum ts) = TSum (map (second (first $ substituteL ls)) ts) |
| #ifdef BUILTIN_ARRAYS |
| substituteL ls (TArray t l s mhole) = TArray (substituteL ls t) l (substituteS ls s) mhole |
| #endif |
| substituteL _ t = t |
| |
| substituteS :: [DataLayout BitRange] -> Sigil (DataLayout BitRange) -> Sigil (DataLayout BitRange) |
| substituteS ls Unboxed = Unboxed |
| substituteS ls (Boxed b CLayout) = Boxed b CLayout |
| substituteS ls (Boxed b (Layout l)) = Boxed b . Layout $ substituteS' ls l |
| where |
| substituteS' :: [DataLayout BitRange] -> DataLayout' BitRange -> DataLayout' BitRange |
| substituteS' ls l = case l of |
| VarLayout n s -> case ls !! (natToInt n) of |
| CLayout -> __impossible "substituteS in Inference: CLayout shouldn't be here" |
| Layout l -> offset s l |
| SumLayout tag alts -> |
| let altl = M.toList alts |
| fns = fmap fst altl |
| fis = fmap fst $ fmap snd altl |
| fes = fmap snd $ fmap snd altl |
| in SumLayout tag $ M.fromList (zip fns $ zip fis (fmap (substituteS' ls) fes)) |
| RecordLayout fs -> |
| let fsl = M.toList fs |
| fns = fmap fst fsl |
| fes = fmap snd fsl |
| in RecordLayout $ M.fromList (zip fns (fmap (substituteS' ls) fes)) |
| #ifdef BUILTIN_ARRAYS |
| ArrayLayout e -> ArrayLayout $ substituteS' ls e |
| #endif |
| _ -> l |
| |
| substituteLE :: Vec t (Type u b) -> LExpr t b -> LExpr u b |
| substituteLE vs = \case |
| LVariable va -> LVariable va |
| LFun fn ts ls -> LFun fn (fmap (substitute vs) ts) ls |
| LOp op es -> LOp op $ fmap go es |
| LApp e1 e2 -> LApp (go e1) (go e2) |
| LCon tn e t -> LCon tn (go e) (substitute vs t) |
| LUnit -> LUnit |
| LILit n t -> LILit n t |
| LSLit s -> LSLit s |
| LLet a e e' -> LLet a (go e) (go e') |
| LLetBang bs a e e' -> LLetBang bs a (go e) (go e') |
| LTuple e1 e2 -> LTuple (go e1) (go e2) |
| LStruct fs -> LStruct $ fmap (second go) fs |
| LIf c th el -> LIf (go c) (go th) (go el) |
| LCase e tn (a1,e1) (a2,e2) |
| -> LCase (go e) tn (a1,go e1) (a2,go e2) |
| LEsac e -> LEsac $ go e |
| LSplit as e e' -> LSplit as (go e) (go e') |
| LMember e f -> LMember (go e) f |
| LTake as rec f e' -> LTake as (go rec) f (go e') |
| LPut rec f e -> LPut (go rec) f (go e) |
| LPromote t e -> LPromote (substitute vs t) (go e) |
| LCast t e -> LCast (substitute vs t) (go e) |
| where go = substituteLE vs |
| |
| remove :: (Eq a) => a -> [(a,b)] -> [(a,b)] |
| remove k = filter ((/= k) . fst) |
| |
| adjust :: (Eq a) => a -> (b -> b) -> [(a,b)] -> [(a,b)] |
| adjust k f = map (\(a,b) -> (a,) $ if a == k then f b else b) |
| |
| |
| newtype TC (t :: Nat) (v :: Nat) b x |
| = TC {unTC :: ExceptT String |
| (ReaderT (Vec t Kind, Map FunName (FunctionType b)) |
| (State (Vec v (Maybe (Type t b))))) |
| x} |
| deriving (Functor, Applicative, Alternative, Monad, MonadPlus, |
| MonadReader (Vec t Kind, Map FunName (FunctionType b))) |
| |
| #if MIN_VERSION_base(4,13,0) |
| instance MonadFail (TC t v b) where |
| fail = __impossible |
| #endif |
| |
| infixl 4 <||> |
| (<||>) :: TC t v b (x -> y) -> TC t v b x -> TC t v b y |
| (TC a) <||> (TC b) = TC $ do x <- get |
| f <- a |
| x1 <- get |
| put x |
| arg <- b |
| x2 <- get |
| -- XXX | unTC $ guardShow "<||>" $ x1 == x2 |
| -- \ ^^^ NOTE: This check is taken out to fix |
| -- #296. The issue here is that, if we define a |
| -- variable of permission D alone (w/o S), it will |
| -- be marked as used after it's been used, which |
| -- is correct. But when it is used in one branch |
| -- but not in the other one, which is allowed as |
| -- it's droppable, it will be marked as used in |
| -- the context of one branch but not the other and |
| -- render the two contexts different. The formal |
| -- specification requires that both contexts are |
| -- the same, but it is tantamount to merging two |
| -- differerent (correct) contexts correctly, which |
| -- can be established in the typing proof. |
| -- / v.jackson, zilinc |
| return (f arg) |
| |
| opType :: Op -> [Type t b] -> Maybe (Type t b) |
| opType opr [TPrim p1, TPrim p2] |
| | opr `elem` [Plus, Minus, Times, Divide, Mod, |
| BitAnd, BitOr, BitXor, LShift, RShift], |
| p1 == p2, p1 /= Boolean = Just $ TPrim p1 |
| opType opr [TPrim p1, TPrim p2] |
| | opr `elem` [Gt, Lt, Le, Ge, Eq, NEq], |
| p1 == p2, p1 /= Boolean = Just $ TPrim Boolean |
| opType opr [TPrim Boolean, TPrim Boolean] |
| | opr `elem` [And, Or, Eq, NEq] = Just $ TPrim Boolean |
| opType Not [TPrim Boolean] = Just $ TPrim Boolean |
| opType Complement [TPrim p] | p /= Boolean = Just $ TPrim p |
| opType opr ts = __impossible "opType" |
| |
| useVariable :: Fin v -> TC t v b (Maybe (Type t b)) |
| useVariable v = TC $ do ret <- (`at` v) <$> get |
| case ret of |
| Nothing -> return ret |
| Just t -> do |
| ok <- canShare <$> unTC (kindcheck t) |
| unless ok $ modify (\s -> update s v Nothing) |
| return ret |
| |
| funType :: CoreFunName -> TC t v b (Maybe (FunctionType b)) |
| funType v = TC $ (M.lookup (unCoreFunName v) . snd) <$> ask |
| |
| runTC :: TC t v b x |
| -> (Vec t Kind, Map FunName (FunctionType b)) |
| -> Vec v (Maybe (Type t b)) |
| -> Either String (Vec v (Maybe (Type t b)), x) |
| runTC (TC a) readers st = case runState (runReaderT (runExceptT a) readers) st of |
| (Left x, s) -> Left x |
| (Right x, s) -> Right (s,x) |
| |
| -- XXX | tc_debug :: [Definition UntypedExpr a] -> IO () |
| -- XXX | tc_debug = flip tc_debug' M.empty |
| -- XXX | where |
| -- XXX | tc_debug' :: [Definition UntypedExpr a] -> Map FunName FunctionType -> IO () |
| -- XXX | tc_debug' [] _ = putStrLn "tc2... OK!" |
| -- XXX | tc_debug' ((FunDef _ fn ts t rt e):ds) reader = |
| -- XXX | case runTC (infer e) (fmap snd ts, reader) (Cons (Just t) Nil) of |
| -- XXX | Left x -> putStrLn $ "tc2... failed! Due to: " ++ x |
| -- XXX | Right _ -> tc_debug' ds (M.insert fn (FT (fmap snd ts) t rt) reader) |
| -- XXX | tc_debug' ((AbsDecl _ fn ts t rt):ds) reader = tc_debug' ds (M.insert fn (FT (fmap snd ts) t rt) reader) |
| -- XXX | tc_debug' (_:ds) reader = tc_debug' ds reader |
| |
| retype :: (Show b, Eq b, Pretty b, a ~ b) |
| => [Definition TypedExpr a b] |
| -> Either String [Definition TypedExpr a b] |
| retype ds = fmap fst $ tc $ map untypeD ds |
| |
| tc :: (Show b, Eq b, Pretty b, a ~ b) |
| => [Definition UntypedExpr a b] |
| -> Either String ([Definition TypedExpr a b], Map FunName (FunctionType b)) |
| tc = flip tc' M.empty |
| where |
| tc' :: (Show b, Eq b, Pretty b, a ~ b) |
| => [Definition UntypedExpr a b] |
| -> Map FunName (FunctionType b) -- the reader |
| -> Either String ([Definition TypedExpr a b], Map FunName (FunctionType b)) |
| tc' [] reader = return ([], reader) |
| tc' ((FunDef attr fn ks ls t rt e):ds) reader = |
| -- Enable recursion by inserting this function's type into the function type dictionary |
| let ft = FT (snd <$> ks) (snd <$> ls) t rt in |
| case runTC (infer e >>= flip typecheck rt) (fmap snd ks, M.insert fn ft reader) (Cons (Just t) Nil) of |
| Left x -> Left x |
| Right (_, e') -> (first (FunDef attr fn ks ls t rt e':)) <$> tc' ds (M.insert fn (FT (fmap snd ks) (fmap snd ls) t rt) reader) |
| tc' (d@(AbsDecl _ fn ks ls t rt):ds) reader = (first (Unsafe.unsafeCoerce d:)) <$> tc' ds (M.insert fn (FT (fmap snd ks) (fmap snd ls) t rt) reader) |
| tc' (d:ds) reader = (first (Unsafe.unsafeCoerce d:)) <$> tc' ds reader |
| |
| tc_ :: (Show b, Eq b, Pretty b, a ~ b) |
| => [Definition UntypedExpr a b] |
| -> Either String [Definition TypedExpr a b] |
| tc_ = fmap fst . tc |
| |
| tcConsts :: [CoreConst UntypedExpr] |
| -> Map FunName (FunctionType VarName) |
| -> Either String ([CoreConst TypedExpr], Map FunName (FunctionType VarName)) |
| tcConsts [] reader = return ([], reader) |
| tcConsts ((v,e):ds) reader = |
| case runTC (infer e) (Nil, reader) Nil of |
| Left x -> Left x |
| Right (_,e') -> (first ((v,e'):)) <$> tcConsts ds reader |
| |
| withBinding :: Type t b -> TC t ('Suc v) b x -> TC t v b x |
| withBinding t x |
| = TC $ do readers <- ask |
| st <- get |
| case runTC x readers (Cons (Just t) st) of |
| Left e -> throwError e |
| Right (Cons Nothing s,r) -> do put s; return r |
| Right (Cons (Just t) s, r) -> do |
| ok <- canDiscard <$> unTC (kindcheck t) |
| if ok then put s >> return r |
| else throwError "Didn't use linear variable" |
| |
| withBindings :: Vec k (Type t b) -> TC t (v :+: k) b x -> TC t v b x |
| withBindings Nil tc = tc |
| withBindings (Cons x xs) tc = withBindings xs (withBinding x tc) |
| |
| withBang :: [Fin v] -> TC t v b x -> TC t v b x |
| withBang vs (TC x) = TC $ do st <- get |
| mapM_ (\v -> modify (modifyAt v (fmap bang))) vs |
| ret <- x |
| mapM_ (\v -> modify (modifyAt v (const $ st `at` v))) vs |
| return ret |
| |
| lookupKind :: Fin t -> TC t v b Kind |
| lookupKind f = TC ((`at` f) . fst <$> ask) |
| |
| kindcheck_ :: (Monad m) => (Fin t -> m Kind) -> Type t a -> m Kind |
| kindcheck_ f (TVar v) = f v |
| kindcheck_ f (TVarBang v) = bangKind <$> f v |
| kindcheck_ f (TVarUnboxed v) = return mempty |
| kindcheck_ f (TCon n vs s) = return $ sigilKind s |
| kindcheck_ f (TFun ti to) = return mempty |
| kindcheck_ f (TPrim i) = return mempty |
| kindcheck_ f (TString) = return mempty |
| kindcheck_ f (TProduct t1 t2) = mappend <$> kindcheck_ f t1 <*> kindcheck_ f t2 |
| kindcheck_ f (TRecord _ ts s) = mconcat <$> ((sigilKind s :) <$> mapM (kindcheck_ f . fst . snd) (filter (not . snd . snd) ts)) |
| kindcheck_ f (TSum ts) = mconcat <$> mapM (kindcheck_ f . fst . snd) (filter (not . snd . snd) ts) |
| kindcheck_ f (TUnit) = return mempty |
| kindcheck_ f (TRPar _ _) = return mempty |
| |
| #ifdef BUILTIN_ARRAYS |
| kindcheck_ f (TArray t l s _) = mappend <$> kindcheck_ f t <*> pure (sigilKind s) |
| #endif |
| |
| kindcheck = kindcheck_ lookupKind |
| |
| |
| typecheck :: (Pretty a, Show a, Eq a) => TypedExpr t v a a -> Type t a -> TC t v a (TypedExpr t v a a) |
| typecheck e t = do |
| let t' = exprType e |
| isSub <- isSubtype t' t |
| if | t == t' -> return e |
| | isSub -> return (promote t e) |
| | otherwise -> __impossible $ "Inferred type of\n" ++ |
| show (indent' $ pretty e) ++ |
| "\ndoesn't agree with the given type signature:\n" ++ |
| "Inferred type:\n" ++ |
| show (indent' $ pretty t') ++ |
| "\nGiven type:\n" ++ |
| show (indent' $ pretty t) ++ "\n" |
| |
| infer :: (Pretty a, Show a, Eq a) => UntypedExpr t v a a -> TC t v a (TypedExpr t v a a) |
| infer (E (Op o es)) |
| = do es' <- mapM infer es |
| let Just t = opType o (map exprType es') |
| return (TE t (Op o es')) |
| infer (E (ILit i t)) = return (TE (TPrim t) (ILit i t)) |
| infer (E (SLit s)) = return (TE TString (SLit s)) |
| #ifdef BUILTIN_ARRAYS |
| infer (E (ALit [])) = __impossible "We don't allow 0-size array literals" |
| infer (E (ALit es)) |
| = do es' <- mapM infer es |
| let ts = map exprType es' |
| n = LILit (fromIntegral $ length es) U32 |
| t <- lubAll ts |
| isSub <- allM (`isSubtype` t) ts |
| return (TE (TArray t n Unboxed Nothing) (ALit es')) |
| where |
| lubAll :: (Show b, Eq b) => [Type t b] -> TC t v b (Type t b) |
| lubAll [] = __impossible "lubAll: empty list" |
| lubAll [t] = return t |
| lubAll (t1:t2:ts) = do Just t <- runMaybeT $ lub t1 t2 |
| lubAll (t:ts) |
| infer (E (ArrayIndex arr idx)) |
| = do arr'@(TE ta _) <- infer arr |
| let TArray te l _ _ = ta |
| idx' <- infer idx |
| -- guardShow ("arr-idx out of bound") $ idx >= 0 && idx < l -- no way to check it. need ref types. / zilinc |
| guardShow ("arr-idx on non-linear") . canShare =<< kindcheck ta |
| return (TE te (ArrayIndex arr' idx')) |
| infer (E (ArrayMap2 (as,f) (e1,e2))) |
| = do e1'@(TE t1 _) <- infer e1 |
| e2'@(TE t2 _) <- infer e2 |
| let TArray te1 l1 _ _ = t1 |
| TArray te2 l2 _ _ = t2 |
| f' <- withBindings (Cons te2 (Cons te1 Nil)) $ infer f |
| let t = case __cogent_ftuples_as_sugar of |
| False -> TProduct t1 t2 |
| True -> TRecord NonRec (zipWith (\f t -> (f,(t,False))) tupleFieldNames [t1,t2]) Unboxed |
| return $ TE t $ ArrayMap2 (as,f') (e1',e2') |
| infer (E (Pop a e1 e2)) |
| = do e1'@(TE t1 _) <- infer e1 |
| let TArray te l s tkns = t1 |
| thd = te |
| ttl = TArray te (LOp Minus [l, LILit 1 U32]) s tkns |
| -- guardShow "arr-pop on a singleton array" $ l > 1 |
| e2'@(TE t2 _) <- withBindings (Cons thd (Cons ttl Nil)) $ infer e2 |
| return (TE t2 (Pop a e1' e2')) |
| infer (E (Singleton e)) |
| = do e'@(TE t _) <- infer e |
| let TArray te l _ _ = t |
| -- guardShow "singleton on a non-singleton array" $ l == 1 |
| return (TE te (Singleton e')) |
| infer (E (ArrayTake as arr i e)) |
| = do arr'@(TE tarr _) <- infer arr |
| i' <- infer i |
| let TArray telt len s Nothing = tarr |
| tarr' = TArray telt len s (Just $ texprToLExpr id i') |
| e'@(TE te _) <- withBindings (Cons telt (Cons tarr' Nil)) $ infer e |
| return (TE te $ ArrayTake as arr' i' e') |
| infer (E (ArrayPut arr i e)) |
| = do arr'@(TE tarr _) <- infer arr |
| i' <- infer i |
| e'@(TE te _) <- infer e |
| -- FIXME: all the checks are disabled here, for the lack of a proper |
| -- refinement type system. Also, we cannot know the exact index that |
| -- is being put, thus there's no way that we can infer the precise type |
| -- for the new array (tarr'). |
| let TArray telm len s tkns = tarr |
| -- XXX | mi <- evalExpr i' |
| -- XXX | guardShow "@put index not a integral constant" $ isJust mi |
| -- XXX | let Just i'' = mi |
| -- XXX | guardShow "@put index is out of range" $ i'' `IM.member` tkns |
| -- XXX | let Just itkn = IM.lookup i'' tkns |
| -- XXX | k <- kindcheck telm |
| -- XXX | unless itkn $ guardShow "@put a non-Discardable untaken element" $ canDiscard k |
| let tarr' = TArray telm len s Nothing |
| return (TE tarr' (ArrayPut arr' i' e')) |
| #endif |
| infer (E (Variable v)) |
| = do Just t <- useVariable (fst v) |
| return (TE t (Variable v)) |
| infer (E (Fun f ts ls note)) |
| | ExI (Flip ts') <- Vec.fromList ts |
| , ExI (Flip ls') <- Vec.fromList ls |
| = do myMap <- ask |
| x <- funType f |
| case x of |
| Just (FT ks lts ti to) -> |
| case (Vec.length ts' =? Vec.length ks, Vec.length ls' =? Vec.length lts) |
| of (Just Refl, Just Refl) -> let ti' = substitute ts' $ substituteL ls ti |
| to' = substitute ts' $ substituteL ls to |
| in do forM_ (Vec.zip ts' ks) $ \(t, k) -> do |
| k' <- kindcheck t |
| when ((k <> k') /= k) $ __impossible "kind not matched in type instantiation" |
| return $ TE (TFun ti' to') (Fun f ts ls note) |
| _ -> __impossible "lengths don't match" |
| _ -> error $ "Something went wrong in lookup of function type: '" ++ unCoreFunName f ++ "'" |
| infer (E (App e1 e2)) |
| = do e1'@(TE (TFun ti to) _) <- infer e1 |
| e2'@(TE ti' _) <- infer e2 |
| isSub <- ti' `isSubtype` ti |
| guardShow ("app (actual: " ++ show ti' ++ "; formal: " ++ show ti ++ ")") $ isSub |
| if ti' /= ti then return $ TE to (App e1' (promote ti e2')) |
| else return $ TE to (App e1' e2') |
| infer (E (Let a e1 e2)) |
| = do e1' <- infer e1 |
| e2' <- withBinding (exprType e1') (infer e2) |
| return $ TE (exprType e2') (Let a e1' e2') |
| infer (E (LetBang vs a e1 e2)) |
| = do e1' <- withBang (map fst vs) (infer e1) |
| k <- kindcheck (exprType e1') |
| guardShow "let!" $ canEscape k |
| e2' <- withBinding (exprType e1') (infer e2) |
| return $ TE (exprType e2') (LetBang vs a e1' e2') |
| infer (E Unit) = return $ TE TUnit Unit |
| infer (E (Tuple e1 e2)) |
| = do e1' <- infer e1 |
| e2' <- infer e2 |
| return $ TE (TProduct (exprType e1') (exprType e2')) (Tuple e1' e2') |
| infer (E (Con tag e tfull)) |
| = do e' <- infer e |
| -- Find type of payload for given tag |
| let TSum ts = tfull |
| Just (t, False) = lookup tag ts |
| -- Make sure to promote the payload to type t if necessary |
| e'' <- typecheck e' t |
| return $ TE tfull (Con tag e'' tfull) |
| infer (E (If ec et ee)) |
| = do ec' <- infer ec |
| guardShow "if-1" $ exprType ec' == TPrim Boolean |
| (et', ee') <- (,) <$> infer et <||> infer ee -- have to use applicative functor, as they share the same initial env |
| let tt = exprType et' |
| te = exprType ee' |
| Just tlub <- runMaybeT $ tt `lub` te |
| isSub <- (&&) <$> tt `isSubtype` tlub <*> te `isSubtype` tlub |
| guardShow' "if-2" ["Then type:", show (pretty tt) ++ ";", "else type:", show (pretty te)] isSub |
| let et'' = if tt /= tlub then promote tlub et' else et' |
| ee'' = if te /= tlub then promote tlub ee' else ee' |
| return $ TE tlub (If ec' et'' ee'') |
| infer (E (Case e tag (lt,at,et) (le,ae,ee))) |
| = do e' <- infer e |
| let TSum ts = exprType e' |
| Just (t, taken) = lookup tag ts |
| restt = TSum $ adjust tag (second $ const True) ts -- set the tag to taken |
| let e'' = case taken of |
| True -> promote (TSum $ OM.toList $ OM.adjust (\(t,True) -> (t,False)) tag $ OM.fromList ts) e' |
| False -> e' |
| (et',ee') <- (,) <$> withBinding t (infer et) |
| <||> withBinding restt (infer ee) |
| let tt = exprType et' |
| te = exprType ee' |
| Just tlub <- runMaybeT $ tt `lub` te |
| isSub <- (&&) <$> tt `isSubtype` tlub <*> te `isSubtype` tlub |
| guardShow' "case" ["Match type:", show (pretty tt) ++ ";", "rest type:", show (pretty te)] isSub |
| let et'' = if tt /= tlub then promote tlub et' else et' |
| ee'' = if te /= tlub then promote tlub ee' else ee' |
| return $ TE tlub (Case e'' tag (lt,at,et'') (le,ae,ee'')) |
| infer (E (Esac e)) |
| = do e'@(TE (TSum ts) _) <- infer e |
| let t1 = filter (not . snd . snd) ts |
| case t1 of |
| [(_, (t, False))] -> return $ TE t (Esac e') |
| _ -> __impossible $ "infer: esac (t1 = " ++ show t1 ++ ", ts = " ++ show ts ++ ")" |
| infer (E (Split a e1 e2)) |
| = do e1' <- infer e1 |
| let (TProduct t1 t2) = exprType e1' |
| e2' <- withBindings (Cons t1 (Cons t2 Nil)) (infer e2) |
| return $ TE (exprType e2') (Split a e1' e2') |
| infer (E (Member e f)) |
| = do e'@(TE t _) <- infer e -- canShare |
| let TRecord _ fs _ = t |
| guardShow "member-1" . canShare =<< kindcheck t |
| guardShow "member-2" $ f < length fs |
| let (_,(tau,c)) = fs !! f |
| guardShow "member-3" $ not c -- not taken |
| return $ TE tau (Member e' f) |
| infer (E (Struct fs)) |
| = do let (ns,es) = unzip fs |
| es' <- mapM infer es |
| let ts' = zipWith (\n e' -> (n, (exprType e', False))) ns es' |
| return $ TE (TRecord NonRec ts' Unboxed) $ Struct $ zip ns es' |
| infer (E (Take a e f e2)) |
| = do e'@(TE t _) <- infer e |
| -- trace ("@@@@t is " ++ show t) $ return () |
| let TRecord rp ts s = t |
| -- a common cause of this error is taking a field when you could have used member |
| guardShow ("take: sigil cannot be readonly: " ++ show (pretty e)) $ not (readonly s) |
| guardShow "take-1" $ f < length ts |
| let (init, (fn,(tau,False)):rest) = splitAt f ts |
| k <- kindcheck tau |
| e2' <- withBindings (Cons tau (Cons (TRecord rp (init ++ (fn,(tau,True)):rest) s) Nil)) (infer e2) -- take that field regardless of its shareability |
| return $ TE (exprType e2') (Take a e' f e2') |
| infer (E (Put e1 f e2)) |
| = do e1'@(TE t1 _) <- infer e1 |
| let TRecord rp ts s = t1 |
| guardShow "put: sigil not readonly" $ not (readonly s) |
| guardShow "put-1" $ f < length ts |
| let (init, (fn,(tau,taken)):rest) = splitAt f ts |
| k <- kindcheck tau |
| unless taken $ guardShow "put-2" $ canDiscard k -- if it's not taken, then it has to be discardable; if taken, then just put |
| e2'@(TE t2 _) <- infer e2 |
| isSub <- t2 `isSubtype` tau |
| guardShow "put-3" isSub |
| let e2'' = if t2 /= tau then promote tau e2' else e2' |
| return $ TE (TRecord rp (init ++ (fn,(tau,False)):rest) s) (Put e1' f e2'') -- put it regardless |
| infer (E (Cast ty e)) |
| = do (TE t e') <- infer e |
| guardShow ("cast: " ++ show t ++ " <<< " ++ show ty) =<< t `isUpcastable` ty |
| return $ TE ty (Cast ty $ TE t e') |
| infer (E (Promote ty e)) |
| = do (TE t e') <- infer e |
| guardShow ("promote: " ++ show t ++ " << " ++ show ty) =<< t `isSubtype` ty |
| return $ if t /= ty then promote ty $ TE t e' |
| else TE t e' -- see NOTE [How to handle type annotations?] in Desugar |
| |
| |
| -- | Promote an expression to a given type, pushing down the promote as far as possible. |
| -- This structure is useful when destructing runs of case expressions, for example in Cogent.Isabelle.Compound. |
| -- |
| -- Consider this example of a ternary case: |
| -- > Case scrutinee tag1 |
| -- > when_tag1 |
| -- > (Promote ty |
| -- > (Case (Var 0) tag2 |
| -- > when_tag2 |
| -- > (Promote ty |
| -- > (Let |
| -- > (Esac (Var 0)) |
| -- > when_tag3)))))) |
| -- |
| -- Here, the promote expressions obscure the nested pattern-matching structure of the program. |
| -- We would like instead to push down the promotes to the following: |
| -- > Case scrutinee tag1 |
| -- > when_tag1 |
| -- > (Case (Var 0) tag2 |
| -- > (Promote ty when_tag2) |
| -- > (Let |
| -- > (Esac (Var 0)) |
| -- > (Promote ty when_tag3))) |
| -- |
| -- In this pushed version, the promotion and the pattern matching are separate. |
| -- |
| -- A-normalisation results in a similar structure, but when squashing case expressions for the |
| -- shallow embedding, we want this to apply to desugared as well as normalised. |
| -- |
| promote :: Type t b -> TypedExpr t v a b -> TypedExpr t v a b |
| promote t (TE t' e) = case e of |
| -- For continuation forms, push the promote into the continuations |
| Let a e1 e2 -> TE t $ Let a e1 $ promote t e2 |
| LetBang vs a e1 e2 -> TE t $ LetBang vs a e1 $ promote t e2 |
| If ec et ee -> TE t $ If ec (promote t et) (promote t ee) |
| Case e tag (l1,a1,e1) (l2,a2,e2) |
| -> TE t $ Case e tag |
| (l1, a1, promote t e1) |
| (l2, a2, promote t e2) |
| -- Collapse consecutive promotes |
| Promote _ e' -> promote t e' |
| -- Otherwise, no simplification is necessary; construct a Promote expression as usual. |
| _ -> TE t $ Promote t (TE t' e) |
| |
| |
