Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
119
Issues
119
List
Boards
Labels
Service Desk
Milestones
Merge Requests
16
Merge Requests
16
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
94b2b33b
Commit
94b2b33b
authored
Nov 08, 2013
by
Andrei Paskevich
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Libencoding: reuse monomorphised lsymbols to increase sharing
parent
a8ab6cc1
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
30 additions
and
6 deletions
+30
-6
src/transform/discriminate.ml
src/transform/discriminate.ml
+8
-5
src/transform/libencoding.ml
src/transform/libencoding.ml
+22
-1
No files found.
src/transform/discriminate.ml
View file @
94b2b33b
...
...
@@ -73,16 +73,19 @@ module Lsmap = struct
instantié. Un tag sur un logique polymorphe doit être un tag sur toute
la famille de fonctions *)
let
ls_inst
=
Wls
.
memoize
3
(
fun
ls
->
let
m
=
ref
Mtyl
.
empty
in
fun
tyl
tyv
->
let
ls_inst
=
(* FIXME? Skolem type constants are short-living but
will stay in lsmap as long as the lsymbol is alive *)
let
lsmap
=
Wls
.
memoize
63
(
fun
_
->
ref
Mtyl
.
empty
)
in
fun
ls
tyl
tyv
->
let
m
=
lsmap
ls
in
let
l
=
oty_cons
tyl
tyv
in
match
Mtyl
.
find_opt
l
!
m
with
|
Some
ls
->
ls
|
None
->
|
None
->
let
nls
=
create_lsymbol
(
id_clone
ls
.
ls_name
)
tyl
tyv
in
m
:=
Mtyl
.
add
l
nls
!
m
;
nls
)
nls
type
t
=
lsymbol
Mtyl
.
t
Mls
.
t
...
...
src/transform/libencoding.ml
View file @
94b2b33b
...
...
@@ -191,6 +191,27 @@ let d_monomorph ty_base kept lsmap d =
let
add
ls
acc
=
create_param_decl
ls
::
acc
in
Sls
.
fold
add
!
consts
dl
module
OHTyl
=
Stdlib
.
OrderedHashedList
(
struct
type
t
=
ty
let
tag
=
ty_hash
end
)
module
Mtyl
=
Extmap
.
Make
(
OHTyl
)
let
ls_inst
=
(* FIXME? Skolem type constants are short-living but
will stay in lsmap as long as the lsymbol is alive *)
let
lsmap
=
Wls
.
memoize
63
(
fun
_
->
ref
Mtyl
.
empty
)
in
fun
ls
tyl
tyv
->
let
m
=
lsmap
ls
in
let
l
=
oty_cons
tyl
tyv
in
match
Mtyl
.
find_opt
l
!
m
with
|
Some
ls
->
ls
|
None
->
let
nls
=
create_lsymbol
(
id_clone
ls
.
ls_name
)
tyl
tyv
in
m
:=
Mtyl
.
add
l
nls
!
m
;
nls
let
lsmap
ty_base
kept
=
Hls
.
memo
63
(
fun
ls
->
let
prot_arg
=
is_protecting_id
ls
.
ls_name
in
let
prot_val
=
is_protected_id
ls
.
ls_name
in
...
...
@@ -200,7 +221,7 @@ let lsmap ty_base kept = Hls.memo 63 (fun ls ->
let
ty_res
=
Opt
.
map
pos
ls
.
ls_value
in
if
Opt
.
equal
ty_equal
ty_res
ls
.
ls_value
&&
List
.
for_all2
ty_equal
ty_arg
ls
.
ls_args
then
ls
else
create_lsymbol
(
id_clone
ls
.
ls_name
)
ty_arg
ty_res
)
else
ls_inst
ls
ty_arg
ty_res
)
(* replace all non-kept types with ty_base *)
let
monomorphise_task
=
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment