Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
5c8c603b
Commit
5c8c603b
authored
Jun 29, 2015
by
Andrei Paskevich
Browse files
Mlw: put exception symbols into a separate namespace
we are not going to use exceptions as first-class values any time soon
parent
f53b752f
Changes
3
Hide whitespace changes
Inline
Side-by-side
src/mlw/pmodule.ml
View file @
5c8c603b
...
...
@@ -23,17 +23,18 @@ open Pdecl
type
prog_symbol
=
|
PV
of
pvsymbol
|
RS
of
rsymbol
|
XS
of
xsymbol
type
namespace
=
{
ns_ts
:
itysymbol
Mstr
.
t
;
(* type symbols *)
ns_ps
:
prog_symbol
Mstr
.
t
;
(* program symbols *)
ns_xs
:
xsymbol
Mstr
.
t
;
(* exception symbols *)
ns_ns
:
namespace
Mstr
.
t
;
(* inner namespaces *)
}
let
empty_ns
=
{
ns_ts
=
Mstr
.
empty
;
ns_ps
=
Mstr
.
empty
;
ns_xs
=
Mstr
.
empty
;
ns_ns
=
Mstr
.
empty
;
}
...
...
@@ -45,7 +46,6 @@ let ns_replace eq chk x vo vn =
let
psym_equal
p1
p2
=
match
p1
,
p2
with
|
PV
p1
,
PV
p2
->
pv_equal
p1
p2
|
RS
p1
,
RS
p2
->
rs_equal
p1
p2
|
XS
p1
,
XS
p2
->
xs_equal
p1
p2
|
_
,
_
->
false
let
rec
merge_ns
chk
ns1
ns2
=
...
...
@@ -56,6 +56,7 @@ let rec merge_ns chk ns1 ns2 =
let
fusion
_
ns1
ns2
=
Some
(
merge_ns
chk
ns1
ns2
)
in
{
ns_ts
=
ns_union
its_equal
ns1
.
ns_ts
ns2
.
ns_ts
;
ns_ps
=
ns_union
psym_equal
ns1
.
ns_ps
ns2
.
ns_ps
;
ns_xs
=
ns_union
xs_equal
ns1
.
ns_xs
ns2
.
ns_xs
;
ns_ns
=
Mstr
.
union
fusion
ns1
.
ns_ns
ns2
.
ns_ns
;
}
let
add_ns
chk
x
ns
m
=
Mstr
.
change
(
function
...
...
@@ -66,8 +67,9 @@ let ns_add eq chk x vn m = Mstr.change (function
|
Some
vo
->
Some
(
ns_replace
eq
chk
x
vo
vn
)
|
None
->
Some
vn
)
x
m
let
add_xs
chk
x
xs
ns
=
{
ns
with
ns_xs
=
ns_add
xs_equal
chk
x
xs
ns
.
ns_xs
}
let
add_ts
chk
x
ts
ns
=
{
ns
with
ns_ts
=
ns_add
its_equal
chk
x
ts
ns
.
ns_ts
}
let
add_ps
chk
x
p
f
ns
=
{
ns
with
ns_ps
=
ns_add
psym_equal
chk
x
p
f
ns
.
ns_ps
}
let
add_ps
chk
x
p
s
ns
=
{
ns
with
ns_ps
=
ns_add
psym_equal
chk
x
p
s
ns
.
ns_ps
}
let
add_ns
chk
x
nn
ns
=
{
ns
with
ns_ns
=
add_ns
chk
x
nn
ns
.
ns_ns
}
let
rec
ns_find
get_map
ns
=
function
...
...
@@ -77,6 +79,7 @@ let rec ns_find get_map ns = function
let
ns_find_prog_symbol
=
ns_find
(
fun
ns
->
ns
.
ns_ps
)
let
ns_find_ns
=
ns_find
(
fun
ns
->
ns
.
ns_ns
)
let
ns_find_xs
=
ns_find
(
fun
ns
->
ns
.
ns_xs
)
let
ns_find_its
=
ns_find
(
fun
ns
->
ns
.
ns_ts
)
let
ns_find_pv
ns
s
=
match
ns_find_prog_symbol
ns
s
with
...
...
@@ -85,9 +88,6 @@ let ns_find_pv ns s = match ns_find_prog_symbol ns s with
let
ns_find_rs
ns
s
=
match
ns_find_prog_symbol
ns
s
with
|
RS
rs
->
rs
|
_
->
raise
Not_found
let
ns_find_xs
ns
s
=
match
ns_find_prog_symbol
ns
s
with
|
XS
xs
->
xs
|
_
->
raise
Not_found
(** {2 Module} *)
type
pmodule
=
{
...
...
@@ -236,7 +236,7 @@ let add_pdecl uc d =
|
PDlet
(
LDvar
(
v
,_
))
->
add_symbol
add_ps
v
.
pv_vs
.
vs_name
(
PV
v
)
uc
|
PDlet
(
LDsym
(
s
,_
))
->
add_rs
uc
s
|
PDlet
(
LDrec
l
)
->
List
.
fold_left
(
fun
uc
d
->
add_rs
uc
d
.
rec_sym
)
uc
l
|
PDexn
xs
->
add_symbol
add_
p
s
xs
.
xs_name
(
XS
xs
)
uc
|
PDexn
xs
->
add_symbol
add_
x
s
xs
.
xs_name
xs
uc
|
PDpure
->
uc
(** {2 Builtin symbols} *)
...
...
src/mlw/pmodule.mli
View file @
5c8c603b
...
...
@@ -21,11 +21,11 @@ open Pdecl
type
prog_symbol
=
|
PV
of
pvsymbol
|
RS
of
rsymbol
|
XS
of
xsymbol
type
namespace
=
{
ns_ts
:
itysymbol
Mstr
.
t
;
(* type symbols *)
ns_ps
:
prog_symbol
Mstr
.
t
;
(* program symbols *)
ns_xs
:
xsymbol
Mstr
.
t
;
(* exception symbols *)
ns_ns
:
namespace
Mstr
.
t
;
(* inner namespaces *)
}
...
...
src/parser/typing.ml
View file @
5c8c603b
...
...
@@ -81,24 +81,24 @@ let find_psymbol tuc q = find_psymbol_ns (Theory.get_namespace tuc) q
let
find_itysymbol_ns
ns
q
=
find_qualid
(
fun
s
->
s
.
its_ts
.
ts_name
)
Pmodule
.
ns_find_its
ns
q
let
find_xsymbol_ns
ns
q
=
find_qualid
(
fun
s
->
s
.
xs_name
)
Pmodule
.
ns_find_xs
ns
q
let
find_prog_symbol_ns
ns
p
=
let
get_id_ps
=
function
|
PV
pv
->
pv
.
pv_vs
.
vs_name
|
RS
rs
->
rs
.
rs_name
|
XS
xs
->
xs
.
xs_name
in
|
RS
rs
->
rs
.
rs_name
in
find_qualid
get_id_ps
ns_find_prog_symbol
ns
p
let
get_namespace
muc
=
List
.
hd
muc
.
Pmodule
.
muc_import
let
find_xsymbol
muc
q
=
find_xsymbol_ns
(
get_namespace
muc
)
q
let
find_itysymbol
muc
q
=
find_itysymbol_ns
(
get_namespace
muc
)
q
let
find_prog_symbol
muc
q
=
find_prog_symbol_ns
(
get_namespace
muc
)
q
let
find_rsymbol
muc
q
=
match
find_prog_symbol
muc
q
with
RS
rs
->
rs
|
_
->
Loc
.
errorm
~
loc
:
(
qloc
q
)
"program symbol expected"
let
find_xsymbol
muc
q
=
match
find_prog_symbol
muc
q
with
XS
xs
->
xs
|
_
->
Loc
.
errorm
~
loc
:
(
qloc
q
)
"exception symbol expected"
(** Parsing types *)
let
ty_of_pty
tuc
pty
=
...
...
@@ -564,8 +564,6 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
let
qualid_app
loc
q
el
=
match
find_prog_symbol
muc
q
with
|
PV
pv
->
expr_app
loc
(
DEpv
pv
)
el
|
RS
rs
->
expr_app
loc
(
DErs
rs
)
el
|
XS
xs
->
Loc
.
errorm
~
loc
:
(
qloc
q
)
"unexpected exception symbol %a"
print_xs
xs
in
let
qualid_app
loc
q
el
=
match
q
with
|
Qident
{
id_str
=
n
}
->
...
...
Write
Preview
Supports
Markdown
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