Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in / Register
Toggle navigation
S
sturdy
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Locked Files
Issues
0
Issues
0
List
Boards
Labels
Service Desk
Milestones
Iterations
Merge Requests
0
Merge Requests
0
Requirements
Requirements
List
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Test Cases
Security & Compliance
Security & Compliance
Dependency List
License Compliance
Operations
Operations
Incidents
Environments
Packages & Registries
Packages & Registries
Package Registry
Container Registry
Analytics
Analytics
CI / CD
Code Review
Insights
Issue
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
PLMZ
sturdy
Commits
f145a89a
Unverified
Commit
f145a89a
authored
Feb 05, 2018
by
Sven Keidel
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
improve fixpoint algorithm
parent
0ab18859
Changes
15
Hide whitespace changes
Inline
Side-by-side
Showing
15 changed files
with
213 additions
and
187 deletions
+213
-187
lib/src/Control/Arrow/Class/Environment.hs
lib/src/Control/Arrow/Class/Environment.hs
+5
-1
lib/src/Control/Arrow/Class/Fix.hs
lib/src/Control/Arrow/Class/Fix.hs
+8
-0
lib/src/Control/Arrow/Class/FixpointCache.hs
lib/src/Control/Arrow/Class/FixpointCache.hs
+0
-49
lib/src/Control/Arrow/Environment.hs
lib/src/Control/Arrow/Environment.hs
+0
-2
lib/src/Control/Arrow/Fix.hs
lib/src/Control/Arrow/Fix.hs
+7
-7
lib/src/Control/Arrow/FixpointCache.hs
lib/src/Control/Arrow/FixpointCache.hs
+0
-7
lib/src/Control/Arrow/Transformer/BoundedEnvironment.hs
lib/src/Control/Arrow/Transformer/BoundedEnvironment.hs
+28
-18
lib/src/Control/Arrow/Transformer/Environment.hs
lib/src/Control/Arrow/Transformer/Environment.hs
+4
-1
lib/src/Control/Arrow/Transformer/FixpointCache.hs
lib/src/Control/Arrow/Transformer/FixpointCache.hs
+65
-68
lib/src/Control/Arrow/Utils.hs
lib/src/Control/Arrow/Utils.hs
+7
-0
lib/src/Data/Store.hs
lib/src/Data/Store.hs
+54
-0
lib/sturdy-lib.cabal
lib/sturdy-lib.cabal
+4
-2
pcf/src/Concrete.hs
pcf/src/Concrete.hs
+9
-5
pcf/src/IntervalAnalysis.hs
pcf/src/IntervalAnalysis.hs
+19
-22
pcf/src/Shared.hs
pcf/src/Shared.hs
+3
-5
No files found.
lib/src/Control/Arrow/Class/Environment.hs
View file @
f145a89a
...
...
@@ -3,7 +3,8 @@
{-# LANGUAGE Arrows #-}
module
Control.Arrow.Class.Environment
where
import
Control.Arrow
import
Control.Arrow
import
Control.Arrow.Utils
class
Arrow
c
=>
ArrowEnv
x
y
env
c
|
c
->
x
,
c
->
y
,
c
->
env
where
lookup
::
c
x
(
Maybe
y
)
...
...
@@ -16,3 +17,6 @@ extendEnv' f = proc (x,y,a) -> do
env
<-
getEnv
-<
()
env'
<-
extendEnv
-<
(
x
,
y
,
env
)
localEnv
f
-<
(
env'
,
a
)
bindings
::
(
ArrowChoice
c
,
ArrowEnv
x
y
env
c
)
=>
c
([(
x
,
y
)],
env
)
env
bindings
=
foldA
((
\
(
env
,(
x
,
y
))
->
(
x
,
y
,
env
))
^>>
extendEnv
)
lib/src/Control/Arrow/Class/
Alloc
.hs
→
lib/src/Control/Arrow/Class/
Fix
.hs
View file @
f145a89a
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
module
Control.Arrow.Class.
Alloc
where
module
Control.Arrow.Class.
Fix
(
ArrowFix
(
..
))
where
import
Control.Arrow
class
Arrow
c
=>
ArrowAlloc
x
addr
c
|
c
->
x
,
c
->
addr
where
alloc
::
c
x
addr
class
Arrow
c
=>
ArrowFix
x
y
c
|
c
->
y
,
c
->
x
where
fixA
::
(
c
x
y
->
c
x
y
)
->
c
x
y
lib/src/Control/Arrow/Class/FixpointCache.hs
deleted
100644 → 0
View file @
0ab18859
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE UndecidableInstances #-}
module
Control.Arrow.Class.FixpointCache
(
ArrowCache
(
..
),
fix
)
where
import
Prelude
hiding
(
id
,(
.
))
import
qualified
Data.Function
as
F
import
Control.Arrow
hiding
(
loop
)
import
Control.Category
class
Arrow
c
=>
ArrowCache
x
y
c
|
c
->
x
,
c
->
y
where
-- | Retrieves a value from the cache.
askCache
::
c
x
(
Maybe
y
)
-- | Initialize the cache with the value from the previous fixpoint iteration. If it does not exist, set it to bottom.
initializeCache
::
c
x
()
-- | Update the cache by taking the least upper bound of the old value with the new value.
updateCache
::
c
(
x
,
y
)
()
-- | Replaces the cache of the previous fixpoint iteration with a new cache.
retireCache
::
c
x
y
->
c
x
y
-- | The fixpoint is reached if the outcache after running the computation is equal to the incache.
reachedFixpoint
::
c
()
Bool
memoize
::
(
ArrowChoice
c
,
ArrowCache
x
y
c
)
=>
c
x
y
->
c
x
y
memoize
f
=
proc
x
->
do
m
<-
askCache
-<
x
case
m
of
Just
y
->
returnA
-<
y
Nothing
->
do
initializeCache
-<
x
y
<-
f
-<
x
updateCache
-<
(
x
,
y
)
returnA
-<
y
-- | Specialized fixpoint algorithm
fix
::
(
ArrowChoice
c
,
ArrowCache
x
y
c
)
=>
(
c
x
y
->
c
x
y
)
->
c
x
y
fix
f
=
proc
x
->
do
y
<-
retireCache
(
F
.
fix
(
f
.
memoize
))
-<
x
fp
<-
reachedFixpoint
-<
()
if
fp
then
returnA
-<
y
else
fix
f
-<
x
lib/src/Control/Arrow/Environment.hs
View file @
f145a89a
module
Control.Arrow.Environment
(
module
Control.Arrow.Class.Environment
,
module
Control.Arrow.Class.Alloc
,
module
Control.Arrow.Transformer.Environment
,
module
Control.Arrow.Transformer.BoundedEnvironment
,
)
where
import
Control.Arrow.Class.Environment
import
Control.Arrow.Class.Alloc
import
Control.Arrow.Transformer.Environment
import
Control.Arrow.Transformer.BoundedEnvironment
...
...
lib/src/Control/Arrow/Fix.hs
View file @
f145a89a
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
module
Control.Arrow.Fix
where
module
Control.Arrow.Fix
(
module
Control
.
Arrow
.
Class
.
Fix
,
module
Control
.
Arrow
.
Transformer
.
FixpointCache
)
where
import
Control.Arrow
class
Arrow
c
=>
ArrowFix
x
y
c
|
y
->
c
,
x
->
c
where
fixA
::
(
c
x
y
->
c
x
y
)
->
c
x
y
import
Control.Arrow.Class.Fix
import
Control.Arrow.Transformer.FixpointCache
lib/src/Control/Arrow/FixpointCache.hs
deleted
100644 → 0
View file @
0ab18859
module
Control.Arrow.FixpointCache
(
module
Control
.
Arrow
.
Class
.
FixpointCache
,
module
Control
.
Arrow
.
Transformer
.
FixpointCache
)
where
import
Control.Arrow.Class.FixpointCache
import
Control.Arrow.Transformer.FixpointCache
lib/src/Control/Arrow/Transformer/BoundedEnvironment.hs
View file @
f145a89a
...
...
@@ -5,47 +5,57 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
module
Control.Arrow.Transformer.BoundedEnvironment
(
ArrowAlloc
(
..
),
BoundedEnv
,
runBoundedEnv
,
liftBoundedEnv
)
where
module
Control.Arrow.Transformer.BoundedEnvironment
(
BoundedEnv
,
runBoundedEnv
,
liftBoundedEnv
,
Alloc
)
where
import
Control.Category
import
Control.Arrow
import
Control.Arrow.Class.Alloc
import
Control.Arrow.Class.Environment
import
Control.Arrow.Class.Reader
import
Control.Arrow.Class.State
import
Control.Arrow.Class.Fail
import
Control.Arrow.Transformer.Reader
import
Control.Arrow.Transformer.State
import
Control.Arrow.Utils
import
Data.HashMap.Lazy
(
HashMap
)
import
qualified
Data.HashMap.Lazy
as
H
import
Data.Hashable
import
Data.Order
import
Data.Store
(
Store
)
import
qualified
Data.Store
as
S
newtype
BoundedEnv
a
addr
b
c
x
y
=
BoundedEnv
(
ReaderArrow
(
HashMap
a
addr
)
(
StateArrow
(
HashMap
addr
b
)
c
)
x
y
)
type
Alloc
a
addr
b
c
=
BoundedEnv
a
addr
b
c
a
addr
newtype
BoundedEnv
a
addr
b
c
x
y
=
BoundedEnv
(
ReaderArrow
(
Alloc
a
addr
b
c
,
HashMap
a
addr
)
(
StateArrow
(
Store
addr
b
)
c
)
x
y
)
deriving
(
Category
,
Arrow
,
ArrowChoice
)
runBoundedEnv
::
Arrow
c
=>
BoundedEnv
a
addr
b
c
x
y
->
c
(
HashMap
a
addr
,
HashMap
addr
b
,
x
)
(
HashMap
addr
b
,
y
)
runBoundedEnv
(
BoundedEnv
(
ReaderArrow
(
StateArrow
f
)))
=
(
\
(
env
,
store
,
x
)
->
(
store
,(
env
,
x
)))
^>>
f
runBoundedEnv
::
(
Eq
a
,
Hashable
a
,
Eq
addr
,
Hashable
addr
,
Complete
b
,
ArrowChoice
c
,
ArrowApply
c
)
=>
BoundedEnv
a
addr
b
c
x
y
->
c
(
Alloc
a
addr
b
c
,
HashMap
a
b
,
x
)
y
runBoundedEnv
f
=
let
BoundedEnv
(
ReaderArrow
(
StateArrow
f'
))
=
proc
(
bs
,
x
)
->
do
env
<-
getEnv
-<
()
env'
<-
bindings
-<
(
bs
,
env
)
localEnv
f
-<
(
env'
,
x
)
in
(
\
(
alloc
,
env
,
x
)
->
(
S
.
empty
,((
alloc
,
H
.
empty
),(
H
.
toList
env
,
x
))))
^>>
f'
>>^
snd
liftBoundedEnv
::
Arrow
c
=>
c
x
y
->
BoundedEnv
a
addr
b
c
x
y
liftBoundedEnv
f
=
BoundedEnv
(
liftReader
(
liftState
f
))
instance
(
Eq
a
,
Hashable
a
,
Eq
addr
,
Hashable
addr
,
Complete
b
,
Arrow
c
,
ArrowAlloc
a
addr
(
BoundedEnv
a
addr
b
c
)
)
=>
instance
(
Eq
a
,
Hashable
a
,
Eq
addr
,
Hashable
addr
,
Complete
b
,
Arrow
Apply
c
)
=>
ArrowEnv
a
b
(
HashMap
a
addr
)
(
BoundedEnv
a
addr
b
c
)
where
lookup
=
proc
x
->
do
env
<-
getEnv
-<
()
store
<-
getStore
-<
()
returnA
-<
do
addr
<-
H
.
lookup
x
env
H
.
lookup
addr
store
getEnv
=
BoundedEnv
askA
S
.
lookup
addr
store
getEnv
=
BoundedEnv
(
pi2
<<<
askA
)
extendEnv
=
proc
(
x
,
y
,
env
)
->
do
addr
<-
localEnv
alloc
-<
(
env
,
x
)
alloc
<-
BoundedEnv
(
pi1
<<<
askA
)
-<
()
addr
<-
localEnv
alloc
-<<
(
env
,
x
)
store
<-
getStore
-<
()
putStore
-<
H
.
insertWith
(
⊔
)
addr
y
store
putStore
-<
S
.
insertWith
(
⊔
)
addr
y
store
returnA
-<
H
.
insert
x
addr
env
localEnv
(
BoundedEnv
f
)
=
BoundedEnv
(
localA
f
)
localEnv
(
BoundedEnv
(
ReaderArrow
f
))
=
BoundedEnv
(
ReaderArrow
((
\
((
alloc
,
_
),(
env
,
a
))
->
((
alloc
,
env
),
a
))
^>>
f
)
)
instance
ArrowReader
r
c
=>
ArrowReader
r
(
BoundedEnv
a
addr
b
c
)
where
askA
=
liftBoundedEnv
askA
...
...
@@ -62,16 +72,16 @@ instance ArrowFail e c => ArrowFail e (BoundedEnv a addr b c) where
instance
ArrowApply
c
=>
ArrowApply
(
BoundedEnv
a
addr
b
c
)
where
app
=
BoundedEnv
$
(
\
(
BoundedEnv
f
,
x
)
->
(
f
,
x
))
^>>
app
getStore
::
Arrow
c
=>
BoundedEnv
a
addr
b
c
()
(
HashMap
addr
b
)
getStore
::
Arrow
c
=>
BoundedEnv
a
addr
b
c
()
(
Store
addr
b
)
getStore
=
BoundedEnv
getA
{-# INLINE getStore #-}
putStore
::
Arrow
c
=>
BoundedEnv
a
addr
b
c
(
HashMap
addr
b
)
()
putStore
::
Arrow
c
=>
BoundedEnv
a
addr
b
c
(
Store
addr
b
)
()
putStore
=
BoundedEnv
putA
{-# INLINE putStore #-}
deriving
instance
PreOrd
(
c
(
HashMap
addr
b
,(
HashMap
a
addr
,
x
))
(
HashMap
addr
b
,
y
))
=>
PreOrd
(
BoundedEnv
a
addr
b
c
x
y
)
deriving
instance
Complete
(
c
(
HashMap
addr
b
,(
HashMap
a
addr
,
x
))
(
HashMap
addr
b
,
y
))
=>
Complete
(
BoundedEnv
a
addr
b
c
x
y
)
deriving
instance
CoComplete
(
c
(
HashMap
addr
b
,(
HashMap
a
addr
,
x
))
(
HashMap
addr
b
,
y
))
=>
CoComplete
(
BoundedEnv
a
addr
b
c
x
y
)
deriving
instance
LowerBounded
(
c
(
HashMap
addr
b
,(
HashMap
a
addr
,
x
))
(
HashMap
addr
b
,
y
))
=>
LowerBounded
(
BoundedEnv
a
addr
b
c
x
y
)
deriving
instance
UpperBounded
(
c
(
HashMap
addr
b
,(
HashMap
a
addr
,
x
))
(
HashMap
addr
b
,
y
))
=>
UpperBounded
(
BoundedEnv
a
addr
b
c
x
y
)
deriving
instance
PreOrd
(
c
(
Store
addr
b
,((
Alloc
a
addr
b
c
,
HashMap
a
addr
),
x
))
(
Store
addr
b
,
y
))
=>
PreOrd
(
BoundedEnv
a
addr
b
c
x
y
)
deriving
instance
Complete
(
c
(
Store
addr
b
,((
Alloc
a
addr
b
c
,
HashMap
a
addr
),
x
))
(
Store
addr
b
,
y
))
=>
Complete
(
BoundedEnv
a
addr
b
c
x
y
)
deriving
instance
CoComplete
(
c
(
Store
addr
b
,((
Alloc
a
addr
b
c
,
HashMap
a
addr
),
x
))
(
Store
addr
b
,
y
))
=>
CoComplete
(
BoundedEnv
a
addr
b
c
x
y
)
deriving
instance
LowerBounded
(
c
(
Store
addr
b
,((
Alloc
a
addr
b
c
,
HashMap
a
addr
),
x
))
(
Store
addr
b
,
y
))
=>
LowerBounded
(
BoundedEnv
a
addr
b
c
x
y
)
deriving
instance
UpperBounded
(
c
(
Store
addr
b
,((
Alloc
a
addr
b
c
,
HashMap
a
addr
),
x
))
(
Store
addr
b
,
y
))
=>
UpperBounded
(
BoundedEnv
a
addr
b
c
x
y
)
lib/src/Control/Arrow/Transformer/Environment.hs
View file @
f145a89a
...
...
@@ -20,9 +20,12 @@ import Control.Arrow.Class.State
import
Control.Arrow.Class.Fail
import
Control.Arrow.Class.Environment
newtype
Environment
a
b
c
x
y
=
Environment
{
runEnvironment
::
ReaderArrow
(
HashMap
a
b
)
c
x
y
}
newtype
Environment
a
b
c
x
y
=
Environment
(
ReaderArrow
(
HashMap
a
b
)
c
x
y
)
deriving
(
Category
,
Arrow
,
ArrowChoice
)
runEnvironment
::
Environment
a
b
c
x
y
->
c
(
HashMap
a
b
,
x
)
y
runEnvironment
(
Environment
(
ReaderArrow
f
))
=
f
liftEnv
::
Arrow
c
=>
c
x
y
->
Environment
a
b
c
x
y
liftEnv
f
=
Environment
(
liftReader
f
)
...
...
lib/src/Control/Arrow/Transformer/FixpointCache.hs
View file @
f145a89a
{-# LANGUAGE
FlexibleInstance
s #-}
{-# LANGUAGE
Arrow
s #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DeriveFunctor #-}
module
Control.Arrow.Transformer.FixpointCache
(
CacheArrow
,
runCacheArrow
,
liftCache
,
Cache
,
empty
,
insert
,
lookup
,
insertWith
,(
!
),
keys
,
toList
)
where
module
Control.Arrow.Transformer.FixpointCache
(
CacheArrow
,
runCacheArrow
,
liftCache
)
where
import
Prelude
hiding
(
id
,
lookup
)
import
Prelude
hiding
(
id
,(
.
),
lookup
)
import
Data.Function
(
fix
)
import
Control.Arrow
import
Control.Arrow.Class.Fail
(
ArrowFail
(
..
))
import
Control.Arrow.Class.Reader
import
Control.Arrow.Class.State
import
Control.Arrow.Class.FixpointCache
import
Control.Arrow.Class.Fix
import
Control.Arrow.Class.Environment
import
Control.Arrow.Utils
import
Control.Category
import
Data.Hashable
(
Hashable
)
import
Data.HashMap.Lazy
(
HashMap
)
import
qualified
Data.HashMap.Lazy
as
H
import
Data.HashSet
(
HashSet
)
import
qualified
Data.HashSet
as
S
import
Data.Maybe
import
Data.Order
import
Data.Store
(
Store
)
import
qualified
Data.Store
as
S
newtype
CacheArrow
a
b
c
x
y
=
CacheArrow
(
c
((
Store
a
b
,
Store
a
b
),
x
)
(
Store
a
b
,
y
))
runCacheArrow
::
Arrow
c
=>
CacheArrow
a
b
c
x
y
->
c
x
y
runCacheArrow
(
CacheArrow
f
)
=
(
\
x
->
((
S
.
empty
,
S
.
empty
),
x
))
^>>
f
>>^
snd
newtype
CacheArrow
a
b
c
x
y
=
CacheArrow
(
c
((
Cache
a
b
,
Cache
a
b
),
x
)
(
Cache
a
b
,
y
))
liftCache
::
Arrow
c
=>
c
x
y
->
CacheArrow
a
b
c
x
y
liftCache
f
=
CacheArrow
((
\
((
_
,
o
),
x
)
->
(
o
,
x
))
^>>
second
f
)
instance
Arrow
c
=>
Category
(
CacheArrow
i
o
c
)
where
id
=
liftCache
id
...
...
@@ -43,6 +48,9 @@ instance ArrowChoice c => ArrowChoice (CacheArrow i o c) where
left
(
CacheArrow
f
)
=
CacheArrow
$
(
\
((
i
,
o
),
e
)
->
injectRight
(
o
,
injectLeft
((
i
,
o
),
e
)))
^>>
left
f
>>^
eject
right
(
CacheArrow
f
)
=
CacheArrow
$
(
\
((
i
,
o
),
e
)
->
injectRight
((
i
,
o
),
injectLeft
(
o
,
e
)))
^>>
right
f
>>^
eject
instance
ArrowApply
c
=>
ArrowApply
(
CacheArrow
i
o
c
)
where
app
=
CacheArrow
$
(
\
(
io
,(
CacheArrow
f
,
x
))
->
(
f
,(
io
,
x
)))
^>>
app
instance
ArrowState
s
c
=>
ArrowState
s
(
CacheArrow
i
o
c
)
where
getA
=
liftCache
getA
putA
=
liftCache
putA
...
...
@@ -54,59 +62,48 @@ instance ArrowReader r c => ArrowReader r (CacheArrow i o c) where
instance
ArrowFail
e
c
=>
ArrowFail
e
(
CacheArrow
i
o
c
)
where
failA
=
liftCache
failA
instance
(
Eq
x
,
Hashable
x
,
LowerBounded
y
,
Complete
y
,
Arrow
c
)
=>
ArrowCache
x
y
(
CacheArrow
x
y
c
)
where
askCache
=
CacheArrow
$
arr
$
\
((
_
,
o
),
x
)
->
(
o
,
lookup
x
o
)
-- transfer cached value from old fixpoint iteration into the new cache
initializeCache
=
CacheArrow
$
arr
$
\
((
Cache
i
,
Cache
o
),
x
)
->
(
Cache
$
H
.
insert
x
(
fromMaybe
bottom
(
H
.
lookup
x
i
))
o
,
()
)
updateCache
=
CacheArrow
$
arr
$
\
((
_
,
o
),(
x
,
y
))
->
(
insertWith
(
⊔
)
x
y
o
,
()
)
retireCache
(
CacheArrow
f
)
=
CacheArrow
$
(
\
((
_
,
o
),
x
)
->
((
o
,
bottom
),
x
))
^>>
f
-- we reached or overshot the fixpoint if we landed in the reductive set, i.e. if f x ⊑ x
reachedFixpoint
=
CacheArrow
$
arr
$
\
((
i
,
o
),
()
)
->
(
o
,
o
⊑
i
)
newtype
Cache
a
b
=
Cache
(
HashMap
a
b
)
deriving
(
Functor
,
Foldable
,
Traversable
)
instance
(
Eq
a
,
Hashable
a
,
PreOrd
b
)
=>
PreOrd
(
Cache
a
b
)
where
Cache
m1
⊑
Cache
m2
=
subsetKeys
m1
m2
&&
all
(
\
(
k
,
v1
)
->
v1
⊑
(
m2
H
.!
k
))
(
H
.
toList
m1
)
Cache
m1
≈
Cache
m2
=
H
.
keys
m1
==
H
.
keys
m2
&&
all
(
\
(
k
,
v_o
)
->
v_o
⊑
(
m2
H
.!
k
))
(
H
.
toList
m1
)
instance
(
Eq
a
,
Hashable
a
,
Complete
b
)
=>
Complete
(
Cache
a
b
)
where
Cache
m1
⊔
Cache
m2
=
Cache
(
H
.
unionWith
(
⊔
)
m1
m2
)
instance
(
Eq
a
,
Hashable
a
,
CoComplete
b
)
=>
CoComplete
(
Cache
a
b
)
where
Cache
m1
⊓
Cache
m2
=
Cache
(
H
.
intersectionWith
(
⊓
)
m1
m2
)
instance
(
Eq
a
,
Hashable
a
,
PreOrd
b
)
=>
LowerBounded
(
Cache
a
b
)
where
bottom
=
empty
subsetKeys
::
(
Eq
a
,
Hashable
a
)
=>
HashMap
a
b
->
HashMap
a
b
->
Bool
subsetKeys
m1
m2
=
subset
(
S
.
fromMap
(
H
.
map
(
const
()
)
m1
))
(
S
.
fromMap
(
H
.
map
(
const
()
)
m2
))
subset
::
(
Eq
a
,
Hashable
a
)
=>
HashSet
a
->
HashSet
a
->
Bool
subset
s1
s2
=
S
.
size
(
S
.
intersection
s1
s2
)
==
S
.
size
s1
empty
::
Cache
a
b
empty
=
Cache
H
.
empty
runCacheArrow
::
Arrow
c
=>
CacheArrow
a
b
c
x
y
->
Cache
a
b
->
c
x
y
runCacheArrow
(
CacheArrow
f
)
i
=
(
\
x
->
((
i
,
empty
),
x
))
^>>
f
>>^
snd
liftCache
::
Arrow
c
=>
c
x
y
->
CacheArrow
i
o
c
x
y
liftCache
f
=
CacheArrow
$
(
\
((
_
,
o
),
x
)
->
(
o
,
x
))
^>>
second
f
lookup
::
(
Eq
a
,
Hashable
a
)
=>
a
->
Cache
a
b
->
Maybe
b
lookup
a
(
Cache
m
)
=
H
.
lookup
a
m
insert
::
(
Eq
a
,
Hashable
a
)
=>
a
->
b
->
Cache
a
b
->
Cache
a
b
insert
a
b
(
Cache
m
)
=
Cache
(
H
.
insert
a
b
m
)
insertWith
::
(
Eq
a
,
Hashable
a
)
=>
(
b
->
b
->
b
)
->
a
->
b
->
Cache
a
b
->
Cache
a
b
insertWith
f
a
b
(
Cache
m
)
=
Cache
(
H
.
insertWith
f
a
b
m
)
(
!
)
::
(
Eq
a
,
Hashable
a
)
=>
Cache
a
b
->
a
->
b
Cache
m
!
a
=
m
H
.!
a
keys
::
Cache
a
b
->
[
a
]
keys
(
Cache
m
)
=
H
.
keys
m
toList
::
Cache
a
b
->
[(
a
,
b
)]
toList
(
Cache
m
)
=
H
.
toList
m
instance
ArrowEnv
a
b
env
c
=>
ArrowEnv
a
b
env
(
CacheArrow
x
y
c
)
where
lookup
=
liftCache
lookup
getEnv
=
liftCache
getEnv
extendEnv
=
liftCache
extendEnv
localEnv
(
CacheArrow
f
)
=
CacheArrow
$
(
\
(
s
,(
env
,
a
))
->
(
env
,(
s
,
a
)))
^>>
localEnv
f
instance
(
Eq
a
,
Hashable
a
,
LowerBounded
b
,
Complete
b
,
ArrowChoice
c
)
=>
ArrowFix
a
b
(
CacheArrow
a
b
c
)
where
fixA
f
=
proc
x
->
do
y
<-
retireCache
(
fix
(
f
.
memoize
))
-<
x
fp
<-
reachedFixpoint
-<
()
if
fp
then
returnA
-<
y
else
fix
f
-<
x
memoize
::
(
Eq
a
,
Hashable
a
,
LowerBounded
b
,
Complete
b
,
ArrowChoice
c
)
=>
CacheArrow
a
b
c
a
b
->
CacheArrow
a
b
c
a
b
memoize
f
=
proc
x
->
do
m
<-
askCache
-<
x
case
m
of
Just
y
->
returnA
-<
y
Nothing
->
do
initializeCache
-<
x
y
<-
f
-<
x
updateCache
-<
(
x
,
y
)
returnA
-<
y
askCache
::
(
Eq
a
,
Hashable
a
,
Arrow
c
)
=>
CacheArrow
a
b
c
a
(
Maybe
b
)
askCache
=
CacheArrow
$
arr
$
\
((
_
,
o
),
x
)
->
(
o
,
S
.
lookup
x
o
)
retireCache
::
(
Eq
a
,
Hashable
a
,
LowerBounded
b
,
Arrow
c
)
=>
CacheArrow
a
b
c
x
y
->
CacheArrow
a
b
c
x
y
retireCache
(
CacheArrow
f
)
=
CacheArrow
$
(
\
((
_
,
o
),
x
)
->
((
o
,
bottom
),
x
))
^>>
f
initializeCache
::
(
Eq
a
,
Hashable
a
,
LowerBounded
b
,
Arrow
c
)
=>
CacheArrow
a
b
c
a
()
initializeCache
=
CacheArrow
$
arr
$
\
((
i
,
o
),
x
)
->
(
S
.
insert
x
(
fromMaybe
bottom
(
S
.
lookup
x
i
))
o
,
()
)
updateCache
::
(
Eq
a
,
Hashable
a
,
Complete
b
,
Arrow
c
)
=>
CacheArrow
a
b
c
(
a
,
b
)
()
updateCache
=
CacheArrow
$
arr
$
\
((
_
,
o
),(
x
,
y
))
->
(
S
.
insertWith
(
⊔
)
x
y
o
,
()
)
reachedFixpoint
::
(
Eq
a
,
Hashable
a
,
LowerBounded
b
,
Arrow
c
)
=>
CacheArrow
a
b
c
()
Bool
reachedFixpoint
=
CacheArrow
$
arr
$
\
((
i
,
o
),
()
)
->
(
o
,
o
⊑
i
)
deriving
instance
PreOrd
(
c
((
Store
a
b
,
Store
a
b
),
x
)
(
Store
a
b
,
y
))
=>
PreOrd
(
CacheArrow
a
b
c
x
y
)
deriving
instance
Complete
(
c
((
Store
a
b
,
Store
a
b
),
x
)
(
Store
a
b
,
y
))
=>
Complete
(
CacheArrow
a
b
c
x
y
)
deriving
instance
CoComplete
(
c
((
Store
a
b
,
Store
a
b
),
x
)
(
Store
a
b
,
y
))
=>
CoComplete
(
CacheArrow
a
b
c
x
y
)
deriving
instance
LowerBounded
(
c
((
Store
a
b
,
Store
a
b
),
x
)
(
Store
a
b
,
y
))
=>
LowerBounded
(
CacheArrow
a
b
c
x
y
)
deriving
instance
UpperBounded
(
c
((
Store
a
b
,
Store
a
b
),
x
)
(
Store
a
b
,
y
))
=>
UpperBounded
(
CacheArrow
a
b
c
x
y
)
lib/src/Control/Arrow/Utils.hs
View file @
f145a89a
...
...
@@ -35,6 +35,13 @@ zipWithA f = proc (l1,l2) -> case (l1,l2) of
cs
<-
zipWithA
f
-<
(
as
,
bs
)
returnA
-<
c
:
cs
foldA
::
ArrowChoice
c
=>
c
(
a
,
x
)
a
->
c
([
x
],
a
)
a
foldA
f
=
proc
(
l
,
a
)
->
case
l
of
(
x
:
xs
)
->
do
a'
<-
f
-<
(
a
,
x
)
foldA
f
-<
(
xs
,
a'
)
[]
->
returnA
-<
a
injectLeft
::
(
r
,
Either
a
b
)
->
Either
(
r
,
a
)
b
injectLeft
(
r
,
e
)
=
case
e
of
Left
a
->
Left
(
r
,
a
)
...
...
lib/src/Data/Store.hs
0 → 100644
View file @
f145a89a
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
module
Data.Store
(
Store
,
subsetKeys
,
empty
,
lookup
,
insert
,
insertWith
,(
!
),
keys
,
toList
)
where
import
Prelude
hiding
(
lookup
)
import
Data.Order
import
Data.Hashable
import
Data.HashMap.Lazy
(
HashMap
)
import
qualified
Data.HashMap.Lazy
as
H
import
Data.HashSet
(
HashSet
)
import
qualified
Data.HashSet
as
S
newtype
Store
a
b
=
Store
(
HashMap
a
b
)
deriving
(
Functor
,
Foldable
,
Traversable
)
instance
(
Eq
a
,
Hashable
a
,
PreOrd
b
)
=>
PreOrd
(
Store
a
b
)
where
Store
m1
⊑
Store
m2
=
subsetKeys
m1
m2
&&
all
(
\
(
k
,
v1
)
->
v1
⊑
(
m2
H
.!
k
))
(
H
.
toList
m1
)
Store
m1
≈
Store
m2
=
H
.
keys
m1
==
H
.
keys
m2
&&
all
(
\
(
k
,
v_o
)
->
v_o
⊑
(
m2
H
.!
k
))
(
H
.
toList
m1
)
instance
(
Eq
a
,
Hashable
a
,
Complete
b
)
=>
Complete
(
Store
a
b
)
where
Store
m1
⊔
Store
m2
=
Store
(
H
.
unionWith
(
⊔
)
m1
m2
)
instance
(
Eq
a
,
Hashable
a
,
CoComplete
b
)
=>
CoComplete
(
Store
a
b
)
where
Store
m1
⊓
Store
m2
=
Store
(
H
.
intersectionWith
(
⊓
)
m1
m2
)
instance
(
Eq
a
,
Hashable
a
,
PreOrd
b
)
=>
LowerBounded
(
Store
a
b
)
where
bottom
=
empty
subsetKeys
::
(
Eq
a
,
Hashable
a
)
=>
HashMap
a
b
->
HashMap
a
b
->
Bool
subsetKeys
m1
m2
=
subset
(
S
.
fromMap
(
H
.
map
(
const
()
)
m1
))
(
S
.
fromMap
(
H
.
map
(
const
()
)
m2
))
subset
::
(
Eq
a
,
Hashable
a
)
=>
HashSet
a
->
HashSet
a
->
Bool
subset
s1
s2
=
S
.
size
(
S
.
intersection
s1
s2
)
==
S
.
size
s1
empty
::
Store
a
b
empty
=
Store
H
.
empty
lookup
::
(
Eq
a
,
Hashable
a
)
=>
a
->
Store
a
b
->
Maybe
b
lookup
a
(
Store
m
)
=
H
.
lookup
a
m
insert
::
(
Eq
a
,
Hashable
a
)
=>
a
->
b
->
Store
a
b
->
Store
a
b
insert
a
b
(
Store
m
)
=
Store
(
H
.
insert
a
b
m
)
insertWith
::
(
Eq
a
,
Hashable
a
)
=>
(
b
->
b
->
b
)
->
a
->
b
->
Store
a
b
->
Store
a
b
insertWith
f
a
b
(
Store
m
)
=
Store
(
H
.
insertWith
f
a
b
m
)
(
!
)
::
(
Eq
a
,
Hashable
a
)
=>
Store
a
b
->
a
->
b
Store
m
!
a
=
m
H
.!
a
keys
::
Store
a
b
->
[
a
]
keys
(
Store
m
)
=
H
.
keys
m
toList
::
Store
a
b
->
[(
a
,
b
)]
toList
(
Store
m
)
=
H
.
toList
m
lib/sturdy-lib.cabal
View file @
f145a89a
...
...
@@ -28,6 +28,7 @@ library
Data.FreeCompletion,
Data.FreeCoCompletion,
Data.Widening,
Data.Store,
Data.Utils
Control.Arrow.Debug,
Control.Arrow.Deduplicate,
...
...
@@ -42,15 +43,16 @@ library
Control.Monad.Join,
Control.Monad.Try,
Control.Arrow.Utils
other-modules: Control.Arrow.Class.Alloc,
Control.Arrow.Class.Reader,
other-modules: Control.Arrow.Class.Reader,
Control.Arrow.Class.State,
Control.Arrow.Class.Fail,
Control.Arrow.Class.Fix,
Control.Arrow.Class.Environment,
Control.Arrow.Transformer.BoundedEnvironment,
Control.Arrow.Transformer.Environment,
Control.Arrow.Transformer.Reader,
Control.Arrow.Transformer.State,
Control.Arrow.Transformer.FixpointCache,
Control.Arrow.Transformer.Fail
build-depends: base,
...
...
pcf/src/Concrete.hs
View file @
f145a89a
...
...
@@ -7,9 +7,9 @@ module Concrete where
import
Prelude
import
Control.Arrow
import
Control.Arrow.Reader
import
Control.Arrow.Fail
import
Control.Arrow.Fix
import
Control.Arrow.Environment
import
Data.Error
import
qualified
Data.HashMap.Lazy
as
M
import
Data.Hashable
...
...
@@ -17,17 +17,17 @@ import Data.Text (Text)
import
GHC.Generics
import
PCF
(
Expr
)
import
Shared
hiding
(
Env
)
import
Shared
data
Closure
=
Closure
Text
Expr
Env
deriving
(
Eq
,
Show
,
Generic
)
type
Env
=
M
.
HashMap
Text
Val
data
Val
=
NumVal
Int
|
ClosureVal
Closure
deriving
(
Eq
,
Show
,
Generic
)
type
Interp
=
ReaderArrow
Env
(
ErrorArrow
String
(
->
))
type
Interp
=
Environment
Text
Val
(
ErrorArrow
String
(
->
))
evalConcrete
::
Env
->
Expr
->
Error
String
Val
evalConcrete
env
e
=
runErrorArrow
(
run
ReaderArrow
eval
)
(
env
,
e
)
evalConcrete
env
e
=
runErrorArrow
(
run
Environment
eval
)
(
env
,
e
)
instance
ArrowFix
Expr
Val
Interp
where
fixA
f
=
f
(
fixA
f
)
...
...
@@ -44,9 +44,13 @@ instance IsVal Val Interp where
NumVal
0
->
f
-<
x
NumVal
_
->
g
-<
y
_
->
failA
-<
"Expected a number as condition for 'ifZero'"
instance
IsClosure
Val
Env
Interp
where
closure
=
arr
$
\
(
x
,
e
,
env
)
->
ClosureVal
$
Closure
x
e
env
applyClosure
f
=
proc
(
fun
,
arg
)
->
case
fun
of
ClosureVal
(
Closure
x
body
env
)
->
localA
f
-<
(
M
.
insert
x
arg
env
,
body
)
ClosureVal
(
Closure
x
body
env
)
->
do
env'
<-
extendEnv
-<
(
x
,
arg
,
env
)
localEnv
f
-<
(
env'
,
body
)
_
->
failA
-<
"Expected a closure"
instance
Hashable
Closure
...
...
pcf/src/IntervalAnalysis.hs
View file @
f145a89a
...
...
@@ -5,14 +5,15 @@
{-# LANGUAGE DeriveGeneric #-}
module
IntervalAnalysis
where
import
Prelude
hiding
(
Bounded
)
import
Prelude
hiding
(
id
,
Bounded
)
import
Control.Category
import
Control.Arrow
import
Control.Arrow.Fail
import
Control.Arrow.Fix
import
Control.Arrow.Reader
import
Control.Arrow.Environment
import
Control.Arrow.Utils
import
Data.Error
import
Data.Foldable
(
toList
)
import
qualified
Data.HashMap.Lazy
as
M
...
...
@@ -23,31 +24,26 @@ import qualified Data.Interval as I
import
Data.Order
import
Data.Powerset
import
Data.Text
(
Text
)
import
Data.Widening
import
Data.Bounded
import
GHC.Generics