mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-24 04:09:10 +03:00
[ perf ] Use delay
and force
to memoize lazy toplevel definitions
This commit is contained in:
parent
d4f84ab78a
commit
24fcc0b551
@ -535,10 +535,11 @@ parameters (constants : SortedSet Name,
|
|||||||
= do val' <- schExp i val
|
= do val' <- schExp i val
|
||||||
sc' <- schExp i sc
|
sc' <- schExp i sc
|
||||||
pure $ "(let ((" ++ schName x ++ " " ++ val' ++ ")) " ++ sc' ++ ")"
|
pure $ "(let ((" ++ schName x ++ " " ++ val' ++ ")) " ++ sc' ++ ")"
|
||||||
schExp i (NmApp fc x@(NmRef _ n) []) =
|
schExp i (NmApp fc x@(NmRef exp n) []) =
|
||||||
if contains n constants
|
if contains n constants
|
||||||
then schExp i x
|
then schExp i x
|
||||||
else pure $ "(" ++ !(schExp i x) ++ ")"
|
else pure $ "(" ++ !(schExp i x) ++ ")"
|
||||||
|
|
||||||
schExp i (NmApp fc x args)
|
schExp i (NmApp fc x args)
|
||||||
= pure $ "(" ++ !(schExp i x) ++ " " ++ sepBy " " !(traverse (schExp i) args) ++ ")"
|
= pure $ "(" ++ !(schExp i x) ++ " " ++ sepBy " " !(traverse (schExp i) args) ++ ")"
|
||||||
schExp i (NmCon fc _ NIL tag []) = pure $ "'()"
|
schExp i (NmCon fc _ NIL tag []) = pure $ "'()"
|
||||||
@ -562,6 +563,8 @@ parameters (constants : SortedSet Name,
|
|||||||
= schOp op !(schArgs i args)
|
= schOp op !(schArgs i args)
|
||||||
schExp i (NmExtPrim fc p args)
|
schExp i (NmExtPrim fc p args)
|
||||||
= schExtPrim i (toPrim p) args
|
= schExtPrim i (toPrim p) args
|
||||||
|
schExp i (NmForce _ _ (NmApp fc x@(NmRef _ _) []))
|
||||||
|
= pure $ "(force " ++ !(schExp i x) ++ ")" -- Special version for memoized toplevel lazy definitions
|
||||||
schExp i (NmForce fc lr t) = pure $ "(" ++ !(schExp i t) ++ ")"
|
schExp i (NmForce fc lr t) = pure $ "(" ++ !(schExp i t) ++ ")"
|
||||||
schExp i (NmDelay fc lr t) = pure $ "(lambda () " ++ !(schExp i t) ++ ")"
|
schExp i (NmDelay fc lr t) = pure $ "(lambda () " ++ !(schExp i t) ++ ")"
|
||||||
schExp i (NmConCase fc sc alts def)
|
schExp i (NmConCase fc sc alts def)
|
||||||
@ -652,11 +655,17 @@ parameters (constants : SortedSet Name,
|
|||||||
|
|
||||||
schDef : {auto c : Ref Ctxt Defs} ->
|
schDef : {auto c : Ref Ctxt Defs} ->
|
||||||
Name -> NamedDef -> Core Builder
|
Name -> NamedDef -> Core Builder
|
||||||
|
|
||||||
|
schDef n (MkNmFun [] (NmDelay _ _ exp))
|
||||||
|
= pure $ "(define " ++ schName !(getFullName n) ++ "(delay "
|
||||||
|
++ !(schExp 0 exp) ++ "))\n" -- Special version for memoized toplevel lazy definitions
|
||||||
|
|
||||||
schDef n (MkNmFun [] exp)
|
schDef n (MkNmFun [] exp)
|
||||||
= if contains n constants
|
= if contains n constants
|
||||||
then pure $ "(define " ++ schName !(getFullName n) ++ " " ++ !(schExp 0 exp) ++ ")\n"
|
then pure $ "(define " ++ schName !(getFullName n) ++ " " ++ !(schExp 0 exp) ++ ")\n"
|
||||||
else pure $ "(define " ++ schName !(getFullName n) ++ " (lambda () " ++ !(schExp 0 exp) ++ "))\n"
|
else pure $ "(define " ++ schName !(getFullName n) ++ " (lambda () " ++ !(schExp 0 exp) ++ "))\n"
|
||||||
|
|
||||||
|
|
||||||
schDef n (MkNmFun args exp)
|
schDef n (MkNmFun args exp)
|
||||||
= pure $ "(define " ++ schName !(getFullName n) ++ " (lambda (" ++ schArglist args ++ ") "
|
= pure $ "(define " ++ schName !(getFullName n) ++ " (lambda (" ++ schArglist args ++ ") "
|
||||||
++ !(schExp 0 exp) ++ "))\n"
|
++ !(schExp 0 exp) ++ "))\n"
|
||||||
|
@ -48,6 +48,7 @@ schHeader prof libs = fromString """
|
|||||||
(require racket/async-channel) ; for asynchronous channels
|
(require racket/async-channel) ; for asynchronous channels
|
||||||
(require racket/future) ; for parallelism/concurrency
|
(require racket/future) ; for parallelism/concurrency
|
||||||
(require racket/math) ; for math ops
|
(require racket/math) ; for math ops
|
||||||
|
(require racket/promise) ; for delay/force in toplevel defs
|
||||||
(require racket/system) ; for system
|
(require racket/system) ; for system
|
||||||
(require racket/unsafe/ops) ; for fast fixnum ops
|
(require racket/unsafe/ops) ; for fast fixnum ops
|
||||||
(require rnrs/bytevectors-6) ; for buffers
|
(require rnrs/bytevectors-6) ; for buffers
|
||||||
|
Loading…
Reference in New Issue
Block a user