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
123
Issues
123
List
Boards
Labels
Service Desk
Milestones
Merge Requests
15
Merge Requests
15
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
122f0b4c
Commit
122f0b4c
authored
Feb 04, 2013
by
Andrei Paskevich
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
whyml: introduce specialized ns_find_(its|ts|pv|ps|pl|xs) functions
parent
285d1ff3
Changes
6
Hide whitespace changes
Inline
Side-by-side
Showing
6 changed files
with
47 additions
and
49 deletions
+47
-49
examples/use_api/use_api.ml
examples/use_api/use_api.ml
+3
-17
src/jessie/ACSLtoWhy3.ml
src/jessie/ACSLtoWhy3.ml
+4
-20
src/whyml/mlw_driver.ml
src/whyml/mlw_driver.ml
+2
-4
src/whyml/mlw_module.ml
src/whyml/mlw_module.ml
+24
-3
src/whyml/mlw_module.mli
src/whyml/mlw_module.mli
+12
-3
src/whyml/mlw_typing.ml
src/whyml/mlw_typing.ml
+2
-2
No files found.
examples/use_api/use_api.ml
View file @
122f0b4c
...
...
@@ -310,29 +310,15 @@ let ref_modules, ref_theories =
let
ref_module
:
Mlw_module
.
modul
=
Stdlib
.
Mstr
.
find
"Ref"
ref_modules
let
ref_type
:
Mlw_ty
.
T
.
itysymbol
=
match
Mlw_module
.
ns_find_ts
ref_module
.
Mlw_module
.
mod_export
[
"ref"
]
with
|
Mlw_module
.
PT
itys
->
itys
|
Mlw_module
.
TS
_
->
assert
false
Mlw_module
.
ns_find_its
ref_module
.
Mlw_module
.
mod_export
[
"ref"
]
(* the "ref" function *)
let
ref_fun
:
Mlw_expr
.
psymbol
=
match
Mlw_module
.
ns_find_ps
ref_module
.
Mlw_module
.
mod_export
[
"ref"
]
with
|
Mlw_module
.
PS
p
->
p
|
_
->
assert
false
Mlw_module
.
ns_find_ps
ref_module
.
Mlw_module
.
mod_export
[
"ref"
]
(* the "!" function *)
let
get_fun
:
Mlw_expr
.
psymbol
=
match
Mlw_module
.
ns_find_ps
ref_module
.
Mlw_module
.
mod_export
[
"prefix !"
]
with
|
Mlw_module
.
PS
p
->
p
|
_
->
assert
false
Mlw_module
.
ns_find_ps
ref_module
.
Mlw_module
.
mod_export
[
"prefix !"
]
let
d2
=
let
args
=
...
...
src/jessie/ACSLtoWhy3.ml
View file @
122f0b4c
...
...
@@ -92,35 +92,19 @@ let ref_modules, ref_theories =
let
ref_module
:
Mlw_module
.
modul
=
Stdlib
.
Mstr
.
find
"Ref"
ref_modules
let
ref_type
:
Mlw_ty
.
T
.
itysymbol
=
match
Mlw_module
.
ns_find_ts
ref_module
.
Mlw_module
.
mod_export
[
"ref"
]
with
|
Mlw_module
.
PT
itys
->
itys
|
Mlw_module
.
TS
_
->
assert
false
Mlw_module
.
ns_find_its
ref_module
.
Mlw_module
.
mod_export
[
"ref"
]
let
ref_fun
:
Mlw_expr
.
psymbol
=
match
Mlw_module
.
ns_find_ps
ref_module
.
Mlw_module
.
mod_export
[
"ref"
]
with
|
Mlw_module
.
PS
p
->
p
|
_
->
assert
false
Mlw_module
.
ns_find_ps
ref_module
.
Mlw_module
.
mod_export
[
"ref"
]
let
get_logic_fun
:
Term
.
lsymbol
=
find
ref_module
.
Mlw_module
.
mod_theory
"prefix !"
let
get_fun
:
Mlw_expr
.
psymbol
=
match
Mlw_module
.
ns_find_ps
ref_module
.
Mlw_module
.
mod_export
[
"prefix !"
]
with
|
Mlw_module
.
PS
p
->
p
|
_
->
assert
false
Mlw_module
.
ns_find_ps
ref_module
.
Mlw_module
.
mod_export
[
"prefix !"
]
let
set_fun
:
Mlw_expr
.
psymbol
=
match
Mlw_module
.
ns_find_ps
ref_module
.
Mlw_module
.
mod_export
[
"infix :="
]
with
|
Mlw_module
.
PS
p
->
p
|
_
->
assert
false
Mlw_module
.
ns_find_ps
ref_module
.
Mlw_module
.
mod_export
[
"infix :="
]
(*********)
...
...
src/whyml/mlw_driver.ml
View file @
122f0b4c
...
...
@@ -141,16 +141,14 @@ let load_driver lib file extra_files =
try
add_local
th
rule
with
e
->
raise
(
Loc
.
Located
(
loc
,
e
))
in
let
find_val
m
(
loc
,
q
)
=
try
match
ns_find_p
s
m
.
mod_export
q
with
try
match
ns_find_p
rog_symbol
m
.
mod_export
q
with
|
PV
pv
->
pv
.
pv_vs
.
vs_name
|
PS
ps
->
ps
.
ps_name
|
PL
_
|
XS
_
|
LS
_
->
raise
Not_found
with
Not_found
->
raise
(
Loc
.
Located
(
loc
,
UnknownVal
(
!
qualid
,
q
)))
in
let
find_xs
m
(
loc
,
q
)
=
try
match
ns_find_ps
m
.
mod_export
q
with
|
XS
xs
->
xs
|
PV
_
|
PS
_
|
PL
_
|
LS
_
->
raise
Not_found
try
ns_find_xs
m
.
mod_export
q
with
Not_found
->
raise
(
Loc
.
Located
(
loc
,
UnknownExn
(
!
qualid
,
q
)))
in
let
add_local_module
loc
m
=
function
...
...
src/whyml/mlw_module.ml
View file @
122f0b4c
...
...
@@ -105,9 +105,30 @@ let rec ns_find get_map ns = function
|
[
a
]
->
Mstr
.
find
a
(
get_map
ns
)
|
a
::
l
->
ns_find
get_map
(
Mstr
.
find
a
ns
.
ns_ns
)
l
let
ns_find_ts
=
ns_find
(
fun
ns
->
ns
.
ns_ts
)
let
ns_find_ps
=
ns_find
(
fun
ns
->
ns
.
ns_ps
)
let
ns_find_ns
=
ns_find
(
fun
ns
->
ns
.
ns_ns
)
let
ns_find_type_symbol
=
ns_find
(
fun
ns
->
ns
.
ns_ts
)
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_its
ns
s
=
match
ns_find_type_symbol
ns
s
with
|
PT
its
->
its
|
_
->
raise
Not_found
let
ns_find_ts
ns
s
=
match
ns_find_type_symbol
ns
s
with
|
TS
ts
->
ts
|
_
->
raise
Not_found
let
ns_find_pv
ns
s
=
match
ns_find_prog_symbol
ns
s
with
|
PV
pv
->
pv
|
_
->
raise
Not_found
let
ns_find_ps
ns
s
=
match
ns_find_prog_symbol
ns
s
with
|
PS
ps
->
ps
|
_
->
raise
Not_found
let
ns_find_pl
ns
s
=
match
ns_find_prog_symbol
ns
s
with
|
PL
pl
->
pl
|
_
->
raise
Not_found
let
ns_find_xs
ns
s
=
match
ns_find_prog_symbol
ns
s
with
|
XS
xs
->
xs
|
_
->
raise
Not_found
let
ns_find_ls
ns
s
=
match
ns_find_prog_symbol
ns
s
with
|
LS
ls
->
ls
|
_
->
raise
Not_found
(** Module *)
...
...
src/whyml/mlw_module.mli
View file @
122f0b4c
...
...
@@ -37,9 +37,18 @@ type namespace = {
ns_ns
:
namespace
Mstr
.
t
;
(* inner namespaces *)
}
val
ns_find_ts
:
namespace
->
string
list
->
type_symbol
val
ns_find_ps
:
namespace
->
string
list
->
prog_symbol
val
ns_find_ns
:
namespace
->
string
list
->
namespace
val
ns_find_type_symbol
:
namespace
->
string
list
->
type_symbol
val
ns_find_prog_symbol
:
namespace
->
string
list
->
prog_symbol
val
ns_find_its
:
namespace
->
string
list
->
itysymbol
val
ns_find_ts
:
namespace
->
string
list
->
tysymbol
val
ns_find_pv
:
namespace
->
string
list
->
pvsymbol
val
ns_find_ps
:
namespace
->
string
list
->
psymbol
val
ns_find_pl
:
namespace
->
string
list
->
plsymbol
val
ns_find_xs
:
namespace
->
string
list
->
xsymbol
val
ns_find_ls
:
namespace
->
string
list
->
lsymbol
val
ns_find_ns
:
namespace
->
string
list
->
namespace
(** Module *)
...
...
src/whyml/mlw_typing.ml
View file @
122f0b4c
...
...
@@ -150,7 +150,7 @@ let get_id_ts = function
|
TS
ts
->
ts
.
ts_name
let
uc_find_ts
uc
p
=
Typing
.
find_ns
get_id_ts
ns_find_t
s
p
(
get_namespace
uc
)
Typing
.
find_ns
get_id_ts
ns_find_t
ype_symbol
p
(
get_namespace
uc
)
let
get_id_ps
=
function
|
PV
pv
->
pv
.
pv_vs
.
vs_name
...
...
@@ -160,7 +160,7 @@ let get_id_ps = function
|
LS
ls
->
ls
.
ls_name
let
uc_find_ps
uc
p
=
Typing
.
find_ns
get_id_ps
ns_find_p
s
p
(
get_namespace
uc
)
Typing
.
find_ns
get_id_ps
ns_find_p
rog_symbol
p
(
get_namespace
uc
)
(** Typing type expressions *)
...
...
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