Skip to content

Commit

Permalink
ScopedSnocList: WIP
Browse files Browse the repository at this point in the history
  • Loading branch information
@GulinSS
GulinSS committed Aug 13, 2024
1 parent 2482ebb commit 9b9e8d5
Show file tree
Hide file tree
Showing 94 changed files with 2,172 additions and 1,605 deletions.
25 changes: 13 additions & 12 deletions src/Compiler/ANF.idr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ import Core.CompileExpr
import Core.Context
import Core.Core
import Core.TT
import Core.Name.ScopedList

import Data.List
import Data.Vect
Expand Down Expand Up @@ -136,9 +137,9 @@ Show ANFDef where
show args ++ " -> " ++ show ret
show (MkAError exp) = "Error: " ++ show exp

data AVars : List Name -> Type where
Nil : AVars []
(::) : Int -> AVars xs -> AVars (x :: xs)
data AVars : ScopedList Name -> Type where
Nil : AVars SLNil
(::) : Int -> AVars xs -> AVars (x :%: xs)

data Next : Type where

Expand Down Expand Up @@ -194,7 +195,7 @@ mutual
List (Lifted vars) -> (List AVar -> ANF) -> Core ANF
anfArgs fc vs args f
= do args' <- traverse (anf vs) args
letBind fc args' f
letBind fc (toList args') f

anf : {vars : _} ->
{auto v : Ref Next Int} ->
Expand Down Expand Up @@ -244,10 +245,10 @@ mutual
= do (is, vs') <- bindArgs args vs
pure $ MkAConAlt n ci t is !(anf vs' sc)
where
bindArgs : (args : List Name) -> AVars vars' ->
Core (List Int, AVars (args ++ vars'))
bindArgs [] vs = pure ([], vs)
bindArgs (n :: ns) vs
bindArgs : (args : ScopedList Name) -> AVars vars' ->
Core (List Int, AVars (args +%+ vars'))
bindArgs SLNil vs = pure ([], vs)
bindArgs (n :%: ns) vs
= do i <- nextVar
(is, vs') <- bindArgs ns vs
pure (i :: is, i :: vs')
Expand All @@ -269,10 +270,10 @@ toANF (MkLFun args scope sc)
pure $ MkAFun (iargs ++ reverse iargs') !(anf vs sc)
where
bindArgs : {auto v : Ref Next Int} ->
(args : List Name) -> AVars vars' ->
Core (List Int, AVars (args ++ vars'))
bindArgs [] vs = pure ([], vs)
bindArgs (n :: ns) vs
(args : ScopedList Name) -> AVars vars' ->
Core (List Int, AVars (args +%+ vars'))
bindArgs SLNil vs = pure ([], vs)
bindArgs (n :%: ns) vs
= do i <- nextVar
(is, vs') <- bindArgs ns vs
pure (i :: is, i :: vs')
Expand Down
52 changes: 26 additions & 26 deletions src/Compiler/CaseOpts.idr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,14 +32,14 @@ case t of

shiftUnder : {args : _} ->
{idx : _} ->
(0 p : IsVar n idx (x :: args ++ vars)) ->
NVar n (args ++ x :: vars)
(0 p : IsVar n idx (x :%: args +%+ vars)) ->
NVar n (args +%+ x :%: vars)
shiftUnder First = weakenNVar (mkSizeOf args) (MkNVar First)
shiftUnder (Later p) = insertNVar (mkSizeOf args) (MkNVar p)

shiftVar : {outer, args : Scope} ->
NVar n (outer ++ (x :: args ++ vars)) ->
NVar n (outer ++ (args ++ x :: vars))
NVar n (outer +%+ (x :%: args +%+ vars)) ->
NVar n (outer +%+ (args +%+ x :%: vars))
shiftVar nvar
= let out = mkSizeOf outer in
case locateNVar out nvar of
Expand All @@ -49,21 +49,21 @@ shiftVar nvar
mutual
shiftBinder : {outer, args : _} ->
(new : Name) ->
CExp (outer ++ old :: (args ++ vars)) ->
CExp (outer ++ (args ++ new :: vars))
CExp (outer +%+ old :%: (args +%+ vars)) ->
CExp (outer +%+ (args +%+ new :%: vars))
shiftBinder new (CLocal fc p)
= case shiftVar (MkNVar p) of
MkNVar p' => CLocal fc (renameVar p')
where
renameVar : IsVar x i (outer ++ (args ++ (old :: rest))) ->
IsVar x i (outer ++ (args ++ (new :: rest)))
renameVar : IsVar x i (outer +%+ (args +%+ (old :%: rest))) ->
IsVar x i (outer +%+ (args +%+ (new :%: rest)))
renameVar = believe_me -- it's the same index, so just the identity at run time
shiftBinder new (CRef fc n) = CRef fc n
shiftBinder {outer} new (CLam fc n sc)
= CLam fc n $ shiftBinder {outer = n :: outer} new sc
= CLam fc n $ shiftBinder {outer = n :%: outer} new sc
shiftBinder new (CLet fc n inlineOK val sc)
= CLet fc n inlineOK (shiftBinder new val)
$ shiftBinder {outer = n :: outer} new sc
$ shiftBinder {outer = n :%: outer} new sc
shiftBinder new (CApp fc f args)
= CApp fc (shiftBinder new f) $ map (shiftBinder new) args
shiftBinder new (CCon fc ci c tag args)
Expand All @@ -87,34 +87,34 @@ mutual

shiftBinderConAlt : {outer, args : _} ->
(new : Name) ->
CConAlt (outer ++ (x :: args ++ vars)) ->
CConAlt (outer ++ (args ++ new :: vars))
CConAlt (outer +%+ (x :%: args +%+ vars)) ->
CConAlt (outer +%+ (args +%+ new :%: vars))
shiftBinderConAlt new (MkConAlt n ci t args' sc)
= let sc' : CExp ((args' ++ outer) ++ (x :: args ++ vars))
= rewrite sym (appendAssociative args' outer (x :: args ++ vars)) in sc in
= let sc' : CExp ((args' +%+ outer) +%+ (x :%: args +%+ vars))
= rewrite sym (appendAssociative args' outer (x :%: args +%+ vars)) in sc in
MkConAlt n ci t args' $
rewrite (appendAssociative args' outer (args ++ new :: vars))
in shiftBinder new {outer = args' ++ outer} sc'
rewrite (appendAssociative args' outer (args +%+ new :%: vars))
in shiftBinder new {outer = args' +%+ outer} sc'

shiftBinderConstAlt : {outer, args : _} ->
(new : Name) ->
CConstAlt (outer ++ (x :: args ++ vars)) ->
CConstAlt (outer ++ (args ++ new :: vars))
CConstAlt (outer +%+ (x :%: args +%+ vars)) ->
CConstAlt (outer +%+ (args +%+ new :%: vars))
shiftBinderConstAlt new (MkConstAlt c sc) = MkConstAlt c $ shiftBinder new sc

-- If there's a lambda inside a case, move the variable so that it's bound
-- outside the case block so that we can bind it just once outside the block
liftOutLambda : {args : _} ->
(new : Name) ->
CExp (old :: args ++ vars) ->
CExp (args ++ new :: vars)
liftOutLambda = shiftBinder {outer = []}
CExp (old :%: args +%+ vars) ->
CExp (args +%+ new :%: vars)
liftOutLambda = shiftBinder {outer = SLNil}

-- If all the alternatives start with a lambda, we can have a single lambda
-- binding outside
tryLiftOut : (new : Name) ->
List (CConAlt vars) ->
Maybe (List (CConAlt (new :: vars)))
Maybe (List (CConAlt (new :%: vars)))
tryLiftOut new [] = Just []
tryLiftOut new (MkConAlt n ci t args (CLam fc x sc) :: as)
= do as' <- tryLiftOut new as
Expand All @@ -124,20 +124,20 @@ tryLiftOut _ _ = Nothing

tryLiftOutConst : (new : Name) ->
List (CConstAlt vars) ->
Maybe (List (CConstAlt (new :: vars)))
Maybe (List (CConstAlt (new :%: vars)))
tryLiftOutConst new [] = Just []
tryLiftOutConst new (MkConstAlt c (CLam fc x sc) :: as)
= do as' <- tryLiftOutConst new as
let sc' = liftOutLambda {args = []} new sc
let sc' = liftOutLambda {args = SLNil} new sc
pure (MkConstAlt c sc' :: as')
tryLiftOutConst _ _ = Nothing

tryLiftDef : (new : Name) ->
Maybe (CExp vars) ->
Maybe (Maybe (CExp (new :: vars)))
Maybe (Maybe (CExp (new :%: vars)))
tryLiftDef new Nothing = Just Nothing
tryLiftDef new (Just (CLam fc x sc))
= let sc' = liftOutLambda {args = []} new sc in
= let sc' = liftOutLambda {args = SLNil} new sc in
pure (Just sc')
tryLiftDef _ _ = Nothing

Expand Down
10 changes: 5 additions & 5 deletions src/Compiler/Common.idr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ Ord UsePhase where
public export
record CompileData where
constructor MkCompileData
mainExpr : CExp [] -- main expression to execute. This also appears in
mainExpr : CExp SLNil -- main expression to execute. This also appears in
-- the definitions below as MN "__mainExpression" 0
-- For incremental compilation and for compiling exported
-- names only, this can be set to 'erased'.
Expand Down Expand Up @@ -152,7 +152,7 @@ getMinimalDef (Coded ns bin)
name <- fromBuf b
let def
= MkGlobalDef fc name (Erased fc Placeholder) [] [] [] [] mul
[] (specified Public) (MkTotality Unchecked IsCovering) False
SLNil (specified Public) (MkTotality Unchecked IsCovering) False
[] Nothing refsR False False True
None cdef Nothing [] Nothing
pure (def, Just (ns, bin))
Expand Down Expand Up @@ -351,8 +351,8 @@ getCompileDataWith exports doLazyAnnots phase_in tm_in
traverse (lambdaLift doLazyAnnots) cseDefs
else pure []

let lifted = (mainname, MkLFun [] [] liftedtm) ::
ldefs ++ concat lifted_in
let lifted = (mainname, MkLFun SLNil SLNil liftedtm) ::
(ldefs ++ concat lifted_in)

anf <- if phase >= ANF
then logTime 2 "Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted
Expand Down Expand Up @@ -408,7 +408,7 @@ getCompileData = getCompileDataWith []

export
compileTerm : {auto c : Ref Ctxt Defs} ->
ClosedTerm -> Core (CExp [])
ClosedTerm -> Core (CExp SLNil)
compileTerm tm_in
= do tm <- toFullNames tm_in
fixArityExp !(compileExp tm)
Expand Down
Loading

0 comments on commit 9b9e8d5

Please sign in to comment.