Start experimenting with indirection

Author: ollef

Setup.hs

@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain

TODO

@@ -1,4 +1,46 @@
-Restriction and closure conversion
+Propagate sizes to all variables
+  Make a transform that makes all arguments constant size indirecting
+  non-constant sized types
+
+  map : (a -> b) -> List a -> List b
+  map f xs = case xs of
+    Nil -> Nil
+    Cons x xs' -> Cons (f x) (Ref (map f (deref xs')))
+
+  BuiltinPtr a = Ptr a
+  IndirectReturn a = Address -> Unit
+  write : StackPtr a -> Address -> Unit
+  alloc : Size -> Address
+
+  map : (BuiltinPtr a -> IndirectReturn b) -> BuiltinPtr (List a) -> IndirectReturn (List b)
+  map f xsp retAdr = case deref xsp of
+    Nil -> write Nil retAdr
+    Cons x xs' ->
+      write Cons retAdr;
+      f (Ref x) (retAdr + 1);
+      let nextAdr = alloc (sizeof (List b))
+      map f xs' nextAdr;
+      write nextAdr (retAdr + 1 + sizeof (List b))
+
+  map : (a -> b) -> Ptr (List a) -> Ptr (List b)
+  map f xs = case deref xs of
+    Nil -> Ref Nil
+    Cons x xs' -> Ref (Cons (f x) (map f xs'))
+
+  map : (BuiltinPtr a -> IndirectReturn b) -> Ptr (List a) -> Ptr (List b)
+  map f xsp = case deref xsp of
+    Nil ->
+      let res = alloc 1 in
+      write Nil res;
+      res
+    Cons x xs' -> 
+      let res = alloc (1 + sizeof a + 1) in
+      write Cons res;
+      f (xsp + 1) (res + 1);
+      write (map f xs') (res + sizeof a + 1);
+      res
+
+Closure conversion
 LLVM code generation
 Usage analysisis for better erasure
 Add new Int type

src/Indirect.hs

@@ -0,0 +1,19 @@
+module Indirect where
+
+import Syntax
+import qualified Syntax.Abstract as Abstract
+import qualified Syntax.Abstract as Constant
+
+import Meta
+type ConstantM = ConstantSize.Expr (MetaVar ConstantSize.Expr s)
+
+inferType :: AbstractM s -> TCM s (ConstantM s, ConstantM s)
+inferType expr = case expr of
+  Abstract.Var v -> return (Constant.Var v, metaType v)
+  Abstract.Global v -> undefined
+  Con qc -> undefined
+  Lit l -> undefined
+  Pi h a t s -> undefined
+  Lam h a t s -> undefined
+  App e1 a e2 -> undefined
+  Case e brs -> undefined

src/Infer.hs

@@ -42,8 +42,7 @@ checkType surrR surrP expr typ = do
     Concrete.Lam h1 a1 s1 -> do
       typ' <- whnf typ
       case typ' of
-        Abstract.Pi h2 a2 t2 ts2 | plicitness a1 == plicitness a2
-                                && relevance a1 >= min (relevance a2) surrR -> do
+        Abstract.Pi h2 a2 t2 ts2 | a1 == a2 -> do
           v <- forall_ (h2 <> h1) t2
           (body, ts2') <- checkType surrR surrP
                                     (instantiate1 (pure v) s1)
@@ -312,10 +311,10 @@ checkConstrDef (ConstrDef c (bindingsView Concrete.piView -> (args, ret))) = mdo
   return (ConstrDef c res, ret', size)
 
 checkDataType
-  :: MetaVar s
-  -> DataDef Concrete.Expr (MetaVar s)
+  :: MetaVar Abstract.Expr s
+  -> DataDef Concrete.Expr (MetaVar Abstract.Expr s)
   -> AbstractM s
-  -> TCM s ( DataDef Abstract.Expr (MetaVar s)
+  -> TCM s ( DataDef Abstract.Expr (MetaVar Abstract.Expr s)
            , AbstractM s
            )
 checkDataType name (DataDef cs) typ = mdo
@@ -353,20 +352,20 @@ checkDataType name (DataDef cs) typ = mdo
   return (DataDef cs', typ'')
 
 checkDefType
-  :: MetaVar s
-  -> Definition Concrete.Expr (MetaVar s)
+  :: MetaVar Abstract.Expr s
+  -> Definition Concrete.Expr (MetaVar Abstract.Expr s)
   -> AbstractM s
-  -> TCM s ( Definition Abstract.Expr (MetaVar s)
+  -> TCM s ( Definition Abstract.Expr (MetaVar Abstract.Expr s)
            , AbstractM s
            )
 checkDefType _ (Definition e) typ = first Definition <$> checkType Relevant Explicit e typ
 checkDefType v (DataDefinition d) typ = first DataDefinition <$> checkDataType v d typ
 
 generaliseDef
-  :: Vector (MetaVar s)
-  -> Definition Abstract.Expr (MetaVar s)
+  :: Vector (MetaVar Abstract.Expr s)
+  -> Definition Abstract.Expr (MetaVar Abstract.Expr s)
   -> AbstractM s
-  -> TCM s ( Definition Abstract.Expr (MetaVar s)
+  -> TCM s ( Definition Abstract.Expr (MetaVar Abstract.Expr s)
            , AbstractM s
            )
 generaliseDef vs (Definition e) t = do
@@ -390,11 +389,11 @@ generaliseDef vs (DataDefinition (DataDef cs)) typ = do
     g = pure . B . (+ Tele (length vs))
 
 generaliseDefs
-  :: Vector ( MetaVar s
-            , Definition Abstract.Expr (MetaVar s)
+  :: Vector ( MetaVar Abstract.Expr s
+            , Definition Abstract.Expr (MetaVar Abstract.Expr s)
             , AbstractM s
             )
-  -> TCM s (Vector ( Definition Abstract.Expr (Var Int (MetaVar s))
+  -> TCM s (Vector ( Definition Abstract.Expr (Var Int (MetaVar Abstract.Expr s))
                    , ScopeM Int Abstract.Expr s
                    )
            )
@@ -447,10 +446,10 @@ generaliseDefs xs = do
 
 checkRecursiveDefs
   :: Vector ( NameHint
-            , Definition Concrete.Expr (Var Int (MetaVar s))
+            , Definition Concrete.Expr (Var Int (MetaVar Abstract.Expr s))
             , ScopeM Int Concrete.Expr s
             )
-  -> TCM s (Vector ( Definition Abstract.Expr (Var Int (MetaVar s))
+  -> TCM s (Vector ( Definition Abstract.Expr (Var Int (MetaVar Abstract.Expr s))
                    , ScopeM Int Abstract.Expr s
                    )
            )

src/Main.hs

@@ -83,7 +83,7 @@ test inp = do
       ) mempty of
       (Left err, tr) -> do mapM_ putStrLn tr; putStrLn err
       (Right (res, restricted), _) -> do
-        mapM_ print $ (show . (\(x, (d, t)) -> runPrettyM $ prettyM x <+> prettyM "=" <+> prettyTypedDef (fe d) (fe t) (fst $ bindingsView Abstract.piView $ fe t))) <$> HM.toList res
+        mapM_ print $ ((\(x, (d, t)) -> runPrettyM $ prettyM x <+> prettyM "=" <+> prettyTypedDef (fe d) (fe t) (fst $ bindingsView Abstract.piView $ fe t))) <$> HM.toList res
         putStrLn "------------- erased ------------------"
         let erased = [(x, fe e') | (x, (e, _)) <- HM.toList res, Definition e' <- [eraseDef e]]
         mapM_ print $ pretty <$> erased

src/Meta.hs

@@ -14,6 +14,7 @@ import qualified Data.Set as S
 import Data.STRef
 import qualified Data.Traversable as T
 import qualified Data.Vector as V
+import Prelude.Extras
 
 import Syntax
 import qualified Syntax.Abstract as Abstract
@@ -22,39 +23,39 @@ import qualified Syntax.Lambda as Lambda
 import TCM
 import Util
 
-type Exists s = STRef s (Either Level (AbstractM s))
+type Exists e s = STRef s (Either Level (e (MetaVar e s)))
 
-data MetaVar s = MetaVar
-  { metaId    :: !Int
-  , metaType  :: AbstractM s
-  , metaHint  :: !NameHint
-  , metaRef   :: !(Maybe (Exists s))
+data MetaVar e s = MetaVar
+  { metaId   :: !Int
+  , metaType :: e (MetaVar e s)
+  , metaHint :: !NameHint
+  , metaRef  :: !(Maybe (Exists e s))
   }
 
-type ConcreteM s = Concrete.Expr (MetaVar s)
-type AbstractM s = Abstract.Expr (MetaVar s)
-type LambdaM s = Lambda.Expr (MetaVar s)
-type ScopeM b f s = Scope b f (MetaVar s)
-type BranchesM c f s = Branches c f (MetaVar s)
+type ConcreteM s = Concrete.Expr (MetaVar Abstract.Expr s)
+type AbstractM s = Abstract.Expr (MetaVar Abstract.Expr s)
+type LambdaM s = Lambda.Expr (MetaVar Abstract.Expr s)
+type ScopeM b f s = Scope b f (MetaVar Abstract.Expr s)
+type BranchesM c f s = Branches c f (MetaVar Abstract.Expr s)
 
-instance Eq (MetaVar s) where
+instance Eq (MetaVar e s) where
   (==) = (==) `on` metaId
 
-instance Ord (MetaVar s) where
+instance Ord (MetaVar e s) where
   compare = compare `on` metaId
 
-instance Hashable (MetaVar s) where
+instance Hashable (MetaVar e s) where
   hashWithSalt s = hashWithSalt s . metaId
 
-instance Show (MetaVar s) where
+instance Show1 e => Show (MetaVar e s) where
   showsPrec d (MetaVar i t h _) = showParen (d > 10) $
     showString "Meta" . showChar ' ' . showsPrec 11 i .
-    showChar ' ' . showsPrec 11 t . showChar ' ' . showsPrec 11 h .
+    showChar ' ' . showsPrec1 11 t . showChar ' ' . showsPrec 11 h .
     showChar ' ' . showString "<Ref>"
 
 showMeta
-  :: (Functor f, Foldable f, Pretty (f String))
-  => f (MetaVar s)
+  :: (Functor e, Foldable e, Functor f, Foldable f, Pretty (f String), Pretty (e String))
+  => f (MetaVar e s)
   -> TCM s Doc
 showMeta x = do
   vs <- foldMapM S.singleton x
@@ -68,9 +69,9 @@ showMeta x = do
   let solutions = [(sv v, pretty $ sv <$> metaType v, pretty $ fmap sv <$> msol) | (v, msol) <- zip vsl pvs]
   return $ pretty (sv <$> x) <> text ", vars: " <> pretty solutions
 
-tr :: (Functor f, Foldable f, Pretty (f String))
+tr :: (Functor e, Foldable e, Functor f, Foldable f, Pretty (f String), Pretty (e String))
    => String
-   -> f (MetaVar s)
+   -> f (MetaVar e s)
    -> TCM s ()
 tr s x = do
   i <- gets tcIndent
@@ -87,38 +88,38 @@ trs s x = do
   i <- gets tcIndent
   TCM.log $ mconcat (replicate i "| ") ++ "--" ++ s ++ ": " ++ show x
 
-existsAtLevel :: NameHint -> AbstractM s -> Level -> TCM s (MetaVar s)
+existsAtLevel :: NameHint -> e (MetaVar e s) -> Level -> TCM s (MetaVar e s)
 existsAtLevel hint typ l = do
   i   <- fresh
   ref <- liftST $ newSTRef $ Left l
   TCM.log $ "exists: " ++ show i
   return $ MetaVar i typ hint (Just ref)
 
-exists :: NameHint -> AbstractM s -> TCM s (MetaVar s)
+exists :: NameHint -> e (MetaVar e s) -> TCM s (MetaVar e s)
 exists hint typ = existsAtLevel hint typ =<< level
 
-existsVar :: Applicative g => NameHint -> AbstractM s -> TCM s (g (MetaVar s))
+existsVar :: Applicative g => NameHint -> e (MetaVar e s) -> TCM s (g (MetaVar e s))
 existsVar hint typ = pure <$> exists hint typ
 
-existsVarAtLevel :: Applicative g => NameHint -> AbstractM s -> Level -> TCM s (g (MetaVar s))
+existsVarAtLevel :: Applicative g => NameHint -> e (MetaVar e s) -> Level -> TCM s (g (MetaVar e s))
 existsVarAtLevel hint typ l = pure <$> existsAtLevel hint typ l
 
-forall_ :: NameHint -> AbstractM s -> TCM s (MetaVar s)
+forall_ :: NameHint -> e (MetaVar e s) -> TCM s (MetaVar e s)
 forall_ hint typ = do
   i <- fresh
   TCM.log $ "forall: " ++ show i
   return $ MetaVar i typ hint Nothing
 
-forallVar :: Applicative g => NameHint -> AbstractM s -> TCM s (g (MetaVar s))
+forallVar :: Applicative g => NameHint -> e (MetaVar e s) -> TCM s (g (MetaVar e s))
 forallVar hint typ = pure <$> forall_ hint typ
 
-solution :: Exists s -> TCM s (Either Level (AbstractM s))
+solution :: Exists e s -> TCM s (Either Level (e (MetaVar e s)))
 solution = liftST . readSTRef
 
-solve :: Exists s -> AbstractM s -> TCM s ()
+solve :: Exists e s -> e (MetaVar e s) -> TCM s ()
 solve r x = liftST $ writeSTRef r $ Right x
 
-refineIfSolved :: Exists s -> AbstractM s -> (AbstractM s -> TCM s (AbstractM s)) -> TCM s (AbstractM s)
+refineIfSolved :: Exists e s -> e (MetaVar e s) -> (e (MetaVar e s) -> TCM s (e (MetaVar e s))) -> TCM s (e (MetaVar e s))
 refineIfSolved r d f = do
   sol <- solution r
   case sol of
@@ -128,21 +129,21 @@ refineIfSolved r d f = do
       solve r e'
       return e'
 
-letMeta :: NameHint -> AbstractM s -> AbstractM s -> TCM s (MetaVar s)
+letMeta :: NameHint -> e (MetaVar e s) -> e (MetaVar e s) -> TCM s (MetaVar e s)
 letMeta hint expr typ = do
   i   <- fresh
   ref <- liftST $ newSTRef $ Right expr
   return $ MetaVar i typ hint (Just ref)
 
 letVar :: Applicative g
-       => NameHint -> AbstractM s -> AbstractM s -> TCM s (g (MetaVar s))
+       => NameHint -> e (MetaVar e s) -> e (MetaVar e s) -> TCM s (g (MetaVar e s))
 letVar hint expr typ = pure <$> letMeta hint expr typ
 
-foldMapM :: (Foldable f, Monoid m)
-         => (MetaVar s -> m) -> f (MetaVar s) -> TCM s m
+foldMapM :: (Foldable e, Foldable f, Monoid m)
+         => (MetaVar e s -> m) -> f (MetaVar e s) -> TCM s m
 foldMapM f = foldrM go mempty
   where
-    go v m = (<> m) . (<> f v) <$> do
+    go v m = (<> m) . (<> f v) <$>
       case metaRef v of
         Just r -> do
           sol <- solution r
@@ -151,9 +152,11 @@ foldMapM f = foldrM go mempty
             Right c -> foldMapM f c
         Nothing -> return mempty
 
-abstractM :: (MetaVar s -> Maybe b)
-          -> AbstractM s
-          -> TCM s (ScopeM b Abstract.Expr s)
+abstractM
+  :: (Monad e, Traversable e, Show1 e)
+  => (MetaVar e s -> Maybe b)
+  -> e (MetaVar e s)
+  -> TCM s (Scope b e (MetaVar e s))
 abstractM f e = do
   e' <- freeze e
   changed <- liftST $ newSTRef False
@@ -183,18 +186,18 @@ abstractM f e = do
     go _ v' = free v'
     free = pure . pure . pure . pure
 
-abstract1M :: MetaVar s
+abstract1M :: MetaVar Abstract.Expr s
            -> AbstractM s
            -> TCM s (ScopeM () Abstract.Expr s)
 abstract1M v e = do
   TCM.log $ "abstracting " ++ show (metaId v)
   abstractM (\v' -> if v == v' then Just () else Nothing) e
 
 abstractDefM
-  :: (MetaVar s -> Maybe b)
-  -> Definition Abstract.Expr (MetaVar s)
+  :: (MetaVar Abstract.Expr s -> Maybe b)
+  -> Definition Abstract.Expr (MetaVar Abstract.Expr s)
   -> AbstractM s
-  -> TCM s ( Definition Abstract.Expr (Var b (MetaVar s))
+  -> TCM s ( Definition Abstract.Expr (Var b (MetaVar Abstract.Expr s))
            , ScopeM b Abstract.Expr s
            )
 abstractDefM f (Definition e) t = do
@@ -207,10 +210,10 @@ abstractDefM f (DataDefinition e) t = do
   return (DataDefinition e', t')
 
 abstractDataDefM
-  :: (MetaVar s -> Maybe b)
-  -> DataDef Abstract.Expr (MetaVar s)
+  :: (MetaVar Abstract.Expr s -> Maybe b)
+  -> DataDef Abstract.Expr (MetaVar Abstract.Expr s)
   -> AbstractM s
-  -> TCM s (DataDef Abstract.Expr (Var b (MetaVar s)))
+  -> TCM s (DataDef Abstract.Expr (Var b (MetaVar Abstract.Expr s)))
 abstractDataDefM f (DataDef cs) typ = mdo
   let inst = instantiateTele $ pure <$> vs
       vs = (\(_, _, _, v) -> v) <$> ps'
@@ -229,23 +232,23 @@ abstractDataDefM f (DataDef cs) typ = mdo
 etaLamM
   :: NameHint
   -> Annotation
-  -> Abstract.Expr (MetaVar s)
-  -> Scope1 Abstract.Expr (MetaVar s)
-  -> TCM s (Abstract.Expr (MetaVar s))
+  -> Abstract.Expr (MetaVar Abstract.Expr s)
+  -> Scope1 Abstract.Expr (MetaVar Abstract.Expr s)
+  -> TCM s (Abstract.Expr (MetaVar Abstract.Expr s))
 etaLamM n p t s = do
   s' <- freezeBound s
   return $ Abstract.etaLam n p t s'
 
-freeze :: AbstractM s -> TCM s (AbstractM s)
+freeze :: (Monad e, Traversable e) => e (MetaVar e s) -> TCM s (e (MetaVar e s))
 freeze e = join <$> traverse go e
   where
     go v@(metaRef -> Just r) = either (const $ do mt <- freeze (metaType v); return $ pure v {metaType = mt})
                                           freeze =<< solution r
     go v                         = return $ pure v
 
-freezeBound :: (Traversable (t Abstract.Expr), Bound t)
-            => t Abstract.Expr (MetaVar s)
-            -> TCM s (t Abstract.Expr (MetaVar s))
+freezeBound :: (Monad e, Traversable e, Traversable (t e), Bound t)
+            => t e (MetaVar e s)
+            -> TCM s (t e (MetaVar e s))
 freezeBound e = (>>>= id) <$> traverse go e
   where
     go v@(metaRef -> Just r) = either (const $ do mt <- freeze (metaType v); return $ pure v {metaType = mt})