Skip to content

Commit c486736

Browse files
GulinSSGulinSS
committed
ScopedSnocList: WIP
1 parent 2482ebb commit c486736

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

56 files changed

+1432
-935
lines changed

‎src/Compiler/ANF.idr

Lines changed: 13 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ import Core.CompileExpr
66
import Core.Context
77
import Core.Core
88
import Core.TT
9+
import Core.Name.ScopedList
910

1011
import Data.List
1112
import Data.Vect
@@ -136,9 +137,9 @@ Show ANFDef where
136137
show args ++ " -> " ++ show ret
137138
show (MkAError exp) = "Error: " ++ show exp
138139

139-
data AVars : List Name -> Type where
140-
Nil : AVars []
141-
(::) : Int -> AVars xs -> AVars (x :: xs)
140+
data AVars : ScopedList Name -> Type where
141+
Nil : AVars SLNil
142+
(::) : Int -> AVars xs -> AVars (x :%: xs)
142143

143144
data Next : Type where
144145

@@ -194,7 +195,7 @@ mutual
194195
List (Lifted vars) -> (List AVar -> ANF) -> Core ANF
195196
anfArgs fc vs args f
196197
= do args' <- traverse (anf vs) args
197-
letBind fc args' f
198+
letBind fc (toList args') f
198199

199200
anf : {vars : _} ->
200201
{auto v : Ref Next Int} ->
@@ -244,10 +245,10 @@ mutual
244245
= do (is, vs') <- bindArgs args vs
245246
pure $ MkAConAlt n ci t is !(anf vs' sc)
246247
where
247-
bindArgs : (args : List Name) -> AVars vars' ->
248-
Core (List Int, AVars (args ++ vars'))
249-
bindArgs [] vs = pure ([], vs)
250-
bindArgs (n :: ns) vs
248+
bindArgs : (args : ScopedList Name) -> AVars vars' ->
249+
Core (List Int, AVars (args +%+ vars'))
250+
bindArgs SLNil vs = pure ([], vs)
251+
bindArgs (n :%: ns) vs
251252
= do i <- nextVar
252253
(is, vs') <- bindArgs ns vs
253254
pure (i :: is, i :: vs')
@@ -269,10 +270,10 @@ toANF (MkLFun args scope sc)
269270
pure $ MkAFun (iargs ++ reverse iargs') !(anf vs sc)
270271
where
271272
bindArgs : {auto v : Ref Next Int} ->
272-
(args : List Name) -> AVars vars' ->
273-
Core (List Int, AVars (args ++ vars'))
274-
bindArgs [] vs = pure ([], vs)
275-
bindArgs (n :: ns) vs
273+
(args : ScopedList Name) -> AVars vars' ->
274+
Core (List Int, AVars (args +%+ vars'))
275+
bindArgs SLNil vs = pure ([], vs)
276+
bindArgs (n :%: ns) vs
276277
= do i <- nextVar
277278
(is, vs') <- bindArgs ns vs
278279
pure (i :: is, i :: vs')

‎src/Compiler/CaseOpts.idr

Lines changed: 26 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -32,14 +32,14 @@ case t of
3232

3333
shiftUnder : {args : _} ->
3434
{idx : _} ->
35-
(0 p : IsVar n idx (x :: args ++ vars)) ->
36-
NVar n (args ++ x :: vars)
35+
(0 p : IsVar n idx (x :%: args +%+ vars)) ->
36+
NVar n (args +%+ x :%: vars)
3737
shiftUnder First = weakenNVar (mkSizeOf args) (MkNVar First)
3838
shiftUnder (Later p) = insertNVar (mkSizeOf args) (MkNVar p)
3939

4040
shiftVar : {outer, args : Scope} ->
41-
NVar n (outer ++ (x :: args ++ vars)) ->
42-
NVar n (outer ++ (args ++ x :: vars))
41+
NVar n (outer +%+ (x :%: args +%+ vars)) ->
42+
NVar n (outer +%+ (args +%+ x :%: vars))
4343
shiftVar nvar
4444
= let out = mkSizeOf outer in
4545
case locateNVar out nvar of
@@ -49,21 +49,21 @@ shiftVar nvar
4949
mutual
5050
shiftBinder : {outer, args : _} ->
5151
(new : Name) ->
52-
CExp (outer ++ old :: (args ++ vars)) ->
53-
CExp (outer ++ (args ++ new :: vars))
52+
CExp (outer +%+ old :%: (args +%+ vars)) ->
53+
CExp (outer +%+ (args +%+ new :%: vars))
5454
shiftBinder new (CLocal fc p)
5555
= case shiftVar (MkNVar p) of
5656
MkNVar p' => CLocal fc (renameVar p')
5757
where
58-
renameVar : IsVar x i (outer ++ (args ++ (old :: rest))) ->
59-
IsVar x i (outer ++ (args ++ (new :: rest)))
58+
renameVar : IsVar x i (outer +%+ (args +%+ (old :%: rest))) ->
59+
IsVar x i (outer +%+ (args +%+ (new :%: rest)))
6060
renameVar = believe_me -- it's the same index, so just the identity at run time
6161
shiftBinder new (CRef fc n) = CRef fc n
6262
shiftBinder {outer} new (CLam fc n sc)
63-
= CLam fc n $ shiftBinder {outer = n :: outer} new sc
63+
= CLam fc n $ shiftBinder {outer = n :%: outer} new sc
6464
shiftBinder new (CLet fc n inlineOK val sc)
6565
= CLet fc n inlineOK (shiftBinder new val)
66-
$ shiftBinder {outer = n :: outer} new sc
66+
$ shiftBinder {outer = n :%: outer} new sc
6767
shiftBinder new (CApp fc f args)
6868
= CApp fc (shiftBinder new f) $ map (shiftBinder new) args
6969
shiftBinder new (CCon fc ci c tag args)
@@ -87,34 +87,34 @@ mutual
8787

8888
shiftBinderConAlt : {outer, args : _} ->
8989
(new : Name) ->
90-
CConAlt (outer ++ (x :: args ++ vars)) ->
91-
CConAlt (outer ++ (args ++ new :: vars))
90+
CConAlt (outer +%+ (x :%: args +%+ vars)) ->
91+
CConAlt (outer +%+ (args +%+ new :%: vars))
9292
shiftBinderConAlt new (MkConAlt n ci t args' sc)
93-
= let sc' : CExp ((args' ++ outer) ++ (x :: args ++ vars))
94-
= rewrite sym (appendAssociative args' outer (x :: args ++ vars)) in sc in
93+
= let sc' : CExp ((args' +%+ outer) +%+ (x :%: args +%+ vars))
94+
= rewrite sym (appendAssociative args' outer (x :%: args +%+ vars)) in sc in
9595
MkConAlt n ci t args' $
96-
rewrite (appendAssociative args' outer (args ++ new :: vars))
97-
in shiftBinder new {outer = args' ++ outer} sc'
96+
rewrite (appendAssociative args' outer (args +%+ new :%: vars))
97+
in shiftBinder new {outer = args' +%+ outer} sc'
9898

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

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

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

125125
tryLiftOutConst : (new : Name) ->
126126
List (CConstAlt vars) ->
127-
Maybe (List (CConstAlt (new :: vars)))
127+
Maybe (List (CConstAlt (new :%: vars)))
128128
tryLiftOutConst new [] = Just []
129129
tryLiftOutConst new (MkConstAlt c (CLam fc x sc) :: as)
130130
= do as' <- tryLiftOutConst new as
131-
let sc' = liftOutLambda {args = []} new sc
131+
let sc' = liftOutLambda {args = SLNil} new sc
132132
pure (MkConstAlt c sc' :: as')
133133
tryLiftOutConst _ _ = Nothing
134134

135135
tryLiftDef : (new : Name) ->
136136
Maybe (CExp vars) ->
137-
Maybe (Maybe (CExp (new :: vars)))
137+
Maybe (Maybe (CExp (new :%: vars)))
138138
tryLiftDef new Nothing = Just Nothing
139139
tryLiftDef new (Just (CLam fc x sc))
140-
= let sc' = liftOutLambda {args = []} new sc in
140+
= let sc' = liftOutLambda {args = SLNil} new sc in
141141
pure (Just sc')
142142
tryLiftDef _ _ = Nothing
143143

‎src/Compiler/Common.idr

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -80,7 +80,7 @@ Ord UsePhase where
8080
public export
8181
record CompileData where
8282
constructor MkCompileData
83-
mainExpr : CExp [] -- main expression to execute. This also appears in
83+
mainExpr : CExp SLNil -- main expression to execute. This also appears in
8484
-- the definitions below as MN "__mainExpression" 0
8585
-- For incremental compilation and for compiling exported
8686
-- names only, this can be set to 'erased'.
@@ -351,8 +351,8 @@ getCompileDataWith exports doLazyAnnots phase_in tm_in
351351
traverse (lambdaLift doLazyAnnots) cseDefs
352352
else pure []
353353

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

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

409409
export
410410
compileTerm : {auto c : Ref Ctxt Defs} ->
411-
ClosedTerm -> Core (CExp [])
411+
ClosedTerm -> Core (CExp SLNil)
412412
compileTerm tm_in
413413
= do tm <- toFullNames tm_in
414414
fixArityExp !(compileExp tm)

0 commit comments

Comments
 (0)