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
1914661d
Commit
1914661d
authored
Jun 18, 2011
by
Andrei Paskevich
Browse files
replace Theory.[MS]nm by Util.[MS]str everywhere
parent
d4ccd8f2
Changes
22
Hide whitespace changes
Inline
Side-by-side
src/bench/benchdb.ml
View file @
1914661d
...
...
@@ -151,7 +151,7 @@ let file whyconf env (dbf,wf) =
"Error : No sketch of proof for the theory %s of file %s.@."
thname
wf
in
Theory
.
Mnm
.
iter
iter
wths
Util
.
Mstr
.
iter
iter
wths
let
db
whyconf
env
=
...
...
src/bench/benchrc.ml
View file @
1914661d
...
...
@@ -134,7 +134,7 @@ let gen_from_file ~format ~prob_name ~file_path ~file_name env lth =
in
let
m
=
Env
.
read_channel
?
format
:
format
env
file_name
cin
in
close_in
cin
;
M
nm
.
bindings
m
in
M
str
.
bindings
m
in
let
file_id
=
if
Db
.
is_initialized
()
then
let
file_db
=
Sysutil
.
relativize_filename
(
Filename
.
dirname
(
Db
.
db_name
()
))
file_path
in
...
...
src/core/env.ml
View file @
1914661d
...
...
@@ -17,6 +17,7 @@
(* *)
(**************************************************************************)
open
Util
open
Ident
open
Theory
...
...
@@ -40,7 +41,7 @@ type find_channel = fformat -> pathname -> filename * in_channel
type
env
=
{
env_find
:
find_channel
;
env_memo
:
(
string
list
,
theory
M
nm
.
t
)
Hashtbl
.
t
;
env_memo
:
(
string
list
,
theory
M
str
.
t
)
Hashtbl
.
t
;
env_tag
:
Hashweak
.
tag
;
}
...
...
@@ -50,7 +51,7 @@ module Wenv = Hashweak.Make(struct type t = env let tag = env_tag end)
(** Input formats *)
type
read_channel
=
env
->
filename
->
in_channel
->
theory
M
nm
.
t
type
read_channel
=
env
->
filename
->
in_channel
->
theory
M
str
.
t
let
read_channel_table
=
Hashtbl
.
create
17
(* format name -> read_channel *)
let
extensions_table
=
Hashtbl
.
create
17
(* suffix -> format name *)
...
...
@@ -128,7 +129,7 @@ let find_channel env = env.env_find
let
find_library
env
sl
=
let
file
,
ic
=
env
.
env_find
"why"
sl
in
try
Hashtbl
.
replace
env
.
env_memo
sl
M
nm
.
empty
;
Hashtbl
.
replace
env
.
env_memo
sl
M
str
.
empty
;
let
mth
=
read_channel
~
format
:
"why"
env
file
ic
in
Hashtbl
.
replace
env
.
env_memo
sl
mth
;
close_in
ic
;
...
...
@@ -152,7 +153,7 @@ let get_builtin s =
let
find_theory
env
sl
s
=
if
sl
=
[]
then
get_builtin
s
else
let
mth
=
find_library
env
sl
in
try
M
nm
.
find
s
mth
with
Not_found
->
try
M
str
.
find
s
mth
with
Not_found
->
raise
(
TheoryNotFound
(
sl
,
s
))
(* Exception reporting *)
...
...
src/core/env.mli
View file @
1914661d
...
...
@@ -44,7 +44,7 @@ exception TheoryNotFound of pathname * string
open
Theory
type
read_channel
=
env
->
filename
->
in_channel
->
theory
Mnm
.
t
type
read_channel
=
env
->
filename
->
in_channel
->
theory
Util
.
Mstr
.
t
(** a function of type [read_channel] parses a channel using
its own syntax. The string argument indicates the origin of
the stream (e.g. file name) to be used in error messages. *)
...
...
@@ -69,7 +69,7 @@ val read_channel : ?format:fformat -> read_channel
@raise UnspecifiedFormat if format is not given and [file]
has no extension *)
val
read_file
:
?
format
:
fformat
->
env
->
filename
->
theory
Mnm
.
t
val
read_file
:
?
format
:
fformat
->
env
->
filename
->
theory
Util
.
Mstr
.
t
(** [read_file ?format env file] returns the theories in [file].
When given, [format] enforces the format, otherwise we choose
the format according to [file]'s extension. *)
...
...
src/core/pretty.ml
View file @
1914661d
...
...
@@ -434,10 +434,10 @@ module NsTree = struct
if
s
=
"real"
&&
ts_equal
ts
ts_real
then
acc
else
Leaf
(
"type "
^
s
)
::
acc
in
let
acc
=
M
nm
.
fold
add_ns
ns
.
ns_ns
[]
in
let
acc
=
M
nm
.
fold
add_pr
ns
.
ns_pr
acc
in
let
acc
=
M
nm
.
fold
add_ls
ns
.
ns_ls
acc
in
let
acc
=
M
nm
.
fold
add_ts
ns
.
ns_ts
acc
in
acc
let
acc
=
M
str
.
fold
add_ns
ns
.
ns_ns
[]
in
let
acc
=
M
str
.
fold
add_pr
ns
.
ns_pr
acc
in
let
acc
=
M
str
.
fold
add_ls
ns
.
ns_ls
acc
in
let
acc
=
M
str
.
fold
add_ts
ns
.
ns_ts
acc
in
acc
let
decomp
=
function
|
Namespace
(
s
,
ns
,
kn
)
->
s
,
contents
ns
kn
...
...
src/core/theory.ml
View file @
1914661d
...
...
@@ -26,21 +26,18 @@ open Decl
(** Namespace *)
module
Snm
=
Sstr
module
Mnm
=
Mstr
type
namespace
=
{
ns_ts
:
tysymbol
M
nm
.
t
;
(* type symbols *)
ns_ls
:
lsymbol
M
nm
.
t
;
(* logic symbols *)
ns_pr
:
prsymbol
M
nm
.
t
;
(* propositions *)
ns_ns
:
namespace
M
nm
.
t
;
(* inner namespaces *)
ns_ts
:
tysymbol
M
str
.
t
;
(* type symbols *)
ns_ls
:
lsymbol
M
str
.
t
;
(* logic symbols *)
ns_pr
:
prsymbol
M
str
.
t
;
(* propositions *)
ns_ns
:
namespace
M
str
.
t
;
(* inner namespaces *)
}
let
empty_ns
=
{
ns_ts
=
M
nm
.
empty
;
ns_ls
=
M
nm
.
empty
;
ns_pr
=
M
nm
.
empty
;
ns_ns
=
M
nm
.
empty
;
ns_ts
=
M
str
.
empty
;
ns_ls
=
M
str
.
empty
;
ns_pr
=
M
str
.
empty
;
ns_ns
=
M
str
.
empty
;
}
exception
ClashSymbol
of
string
...
...
@@ -51,20 +48,20 @@ let ns_replace eq chk x vo vn =
raise
(
ClashSymbol
x
)
let
ns_union
eq
chk
=
M
nm
.
union
(
fun
x
vn
vo
->
Some
(
ns_replace
eq
chk
x
vo
vn
))
M
str
.
union
(
fun
x
vn
vo
->
Some
(
ns_replace
eq
chk
x
vo
vn
))
let
rec
merge_ns
chk
ns1
ns2
=
let
fusion
_
ns1
ns2
=
Some
(
merge_ns
chk
ns1
ns2
)
in
{
ns_ts
=
ns_union
ts_equal
chk
ns1
.
ns_ts
ns2
.
ns_ts
;
ns_ls
=
ns_union
ls_equal
chk
ns1
.
ns_ls
ns2
.
ns_ls
;
ns_pr
=
ns_union
pr_equal
chk
ns1
.
ns_pr
ns2
.
ns_pr
;
ns_ns
=
M
nm
.
union
fusion
ns1
.
ns_ns
ns2
.
ns_ns
;
}
ns_ns
=
M
str
.
union
fusion
ns1
.
ns_ns
ns2
.
ns_ns
;
}
let
nm_add
chk
x
ns
m
=
M
nm
.
change
x
(
function
let
nm_add
chk
x
ns
m
=
M
str
.
change
x
(
function
|
None
->
Some
ns
|
Some
os
->
Some
(
merge_ns
chk
ns
os
))
m
let
ns_add
eq
chk
x
v
m
=
M
nm
.
change
x
(
function
let
ns_add
eq
chk
x
v
m
=
M
str
.
change
x
(
function
|
None
->
Some
v
|
Some
vo
->
Some
(
ns_replace
eq
chk
x
vo
v
))
m
...
...
@@ -79,8 +76,8 @@ let add_ns chk x nn ns = { ns with ns_ns = nm_add chk x nn ns.ns_ns }
let
rec
ns_find
get_map
ns
=
function
|
[]
->
assert
false
|
[
a
]
->
M
nm
.
find
a
(
get_map
ns
)
|
a
::
l
->
ns_find
get_map
(
M
nm
.
find
a
ns
.
ns_ns
)
l
|
[
a
]
->
M
str
.
find
a
(
get_map
ns
)
|
a
::
l
->
ns_find
get_map
(
M
str
.
find
a
ns
.
ns_ns
)
l
let
ns_find_ts
=
ns_find
(
fun
ns
->
ns
.
ns_ts
)
let
ns_find_ls
=
ns_find
(
fun
ns
->
ns
.
ns_ls
)
...
...
@@ -631,10 +628,10 @@ let clone_export uc th inst =
let
f_pr
pr
=
Mpr
.
find_default
pr
pr
cl
.
pr_table
in
let
rec
f_ns
ns
=
{
ns_ts
=
M
nm
.
map
f_ts
(
M
nm
.
filter
g_ts
ns
.
ns_ts
);
ns_ls
=
M
nm
.
map
f_ls
(
M
nm
.
filter
g_ls
ns
.
ns_ls
);
ns_pr
=
M
nm
.
map
f_pr
ns
.
ns_pr
;
ns_ns
=
M
nm
.
map
f_ns
ns
.
ns_ns
;
}
in
ns_ts
=
M
str
.
map
f_ts
(
M
str
.
filter
g_ts
ns
.
ns_ts
);
ns_ls
=
M
str
.
map
f_ls
(
M
str
.
filter
g_ls
ns
.
ns_ls
);
ns_pr
=
M
str
.
map
f_pr
ns
.
ns_pr
;
ns_ns
=
M
str
.
map
f_ns
ns
.
ns_ns
;
}
in
let
ns
=
f_ns
th
.
th_export
in
...
...
src/core/theory.mli
View file @
1914661d
...
...
@@ -18,6 +18,7 @@
(**************************************************************************)
open
Stdlib
open
Util
(** Theories and Namespaces *)
...
...
@@ -26,14 +27,11 @@ open Ty
open
Term
open
Decl
module
Mnm
:
Map
.
S
with
type
key
=
string
module
Snm
:
Mnm
.
Set
type
namespace
=
private
{
ns_ts
:
tysymbol
M
nm
.
t
;
(* type symbols *)
ns_ls
:
lsymbol
M
nm
.
t
;
(* logic symbols *)
ns_pr
:
prsymbol
M
nm
.
t
;
(* propositions *)
ns_ns
:
namespace
M
nm
.
t
;
(* inner namespaces *)
ns_ts
:
tysymbol
M
str
.
t
;
(* type symbols *)
ns_ls
:
lsymbol
M
str
.
t
;
(* logic symbols *)
ns_pr
:
prsymbol
M
str
.
t
;
(* propositions *)
ns_ns
:
namespace
M
str
.
t
;
(* inner namespaces *)
}
val
ns_find_ts
:
namespace
->
string
list
->
tysymbol
...
...
src/ide/session.ml
View file @
1914661d
...
...
@@ -742,7 +742,7 @@ let read_file fn =
in
let
theories
=
Env
.
read_file
env
fn
in
let
theories
=
Theory
.
Mnm
.
fold
Util
.
Mstr
.
fold
(
fun
name
th
acc
->
match
th
.
Theory
.
th_name
.
Ident
.
id_loc
with
|
Some
l
->
(
l
,
name
,
th
)
::
acc
...
...
src/main.ml
View file @
1914661d
...
...
@@ -461,14 +461,14 @@ let do_global_theory env drv (tname,p,t,glist) =
do_theory
env
drv
"lib"
tname
th
glist
let
do_local_theory
env
drv
fname
m
(
tname
,_,
t
,
glist
)
=
let
th
=
try
M
nm
.
find
t
m
with
Not_found
->
let
th
=
try
M
str
.
find
t
m
with
Not_found
->
eprintf
"Theory '%s' not found in file '%s'.@."
tname
fname
;
exit
1
in
do_theory
env
drv
fname
tname
th
glist
let
do_coq_realize_theory
env
_drv
oldf
fname
m
(
tname
,_,
t
,_
glist
)
=
let
th
=
try
M
nm
.
find
t
m
with
Not_found
->
let
th
=
try
M
str
.
find
t
m
with
Not_found
->
eprintf
"Theory '%s' not found in file '%s'.@."
tname
fname
;
exit
1
in
...
...
@@ -509,7 +509,7 @@ let do_input env drv = function
let
glist
=
Queue
.
create
()
in
let
add_th
t
th
mi
=
Ident
.
Mid
.
add
th
.
th_name
(
t
,
th
)
mi
in
let
do_th
_
(
t
,
th
)
=
do_theory
env
drv
fname
t
th
glist
in
Ident
.
Mid
.
iter
do_th
(
M
nm
.
fold
add_th
m
Ident
.
Mid
.
empty
)
Ident
.
Mid
.
iter
do_th
(
M
str
.
fold
add_th
m
Ident
.
Mid
.
empty
)
else
Queue
.
iter
(
do_local_theory
env
drv
fname
m
)
tlist
...
...
src/parser/lexer.mli
View file @
1914661d
...
...
@@ -19,7 +19,7 @@
(** parsing entry points *)
val
parse_logic_file
:
Env
.
env
->
Lexing
.
lexbuf
->
Theory
.
theory
Theory
.
Mnm
.
t
val
parse_logic_file
:
Env
.
env
->
Lexing
.
lexbuf
->
Theory
.
theory
Util
.
Mstr
.
t
val
parse_program_file
:
Lexing
.
lexbuf
->
Ptree
.
program_file
...
...
src/parser/parser.mly
View file @
1914661d
...
...
@@ -32,7 +32,7 @@ module Incremental = struct
let
ref_set
ref
v
=
ref
:=
v
::
ref_tail
ref
let
open_logic_file
env
=
ref_push
env_ref
env
;
ref_push
lenv_ref
Theory
.
Mnm
.
empty
ref_push
env_ref
env
;
ref_push
lenv_ref
Util
.
Mstr
.
empty
let
close_logic_file
()
=
ref_drop
env_ref
;
ref_pop
lenv_ref
...
...
@@ -243,7 +243,7 @@ end
%
type
<
Env
.
env
->
unit
>
pre_logic_file
%
start
pre_logic_file
%
type
<
Theory
.
theory
Theory
.
Mnm
.
t
>
logic_file
%
type
<
Theory
.
theory
Util
.
Mstr
.
t
>
logic_file
%
start
logic_file
%
type
<
Ptree
.
program_file
>
program_file
%
start
program_file
...
...
src/parser/typing.ml
View file @
1914661d
...
...
@@ -1057,7 +1057,7 @@ let prop_kind = function
let
find_theory
env
lenv
q
id
=
match
q
with
|
[]
->
(* local theory *)
begin
try
M
nm
.
find
id
lenv
begin
try
M
str
.
find
id
lenv
with
Not_found
->
find_theory
env
[]
id
end
|
_
::
_
->
(* theory in file f *)
...
...
@@ -1065,23 +1065,23 @@ let find_theory env lenv q id = match q with
let
rec
clone_ns
loc
sl
ns2
ns1
s
=
let
clash
id
=
error
~
loc
(
Clash
id
.
id_string
)
in
let
s
=
M
nm
.
fold
(
fun
nm
ns1
acc
->
if
not
(
M
nm
.
mem
nm
ns2
.
ns_ns
)
then
acc
else
let
ns2
=
M
nm
.
find
nm
ns2
.
ns_ns
in
let
s
=
M
str
.
fold
(
fun
nm
ns1
acc
->
if
not
(
M
str
.
mem
nm
ns2
.
ns_ns
)
then
acc
else
let
ns2
=
M
str
.
find
nm
ns2
.
ns_ns
in
clone_ns
loc
sl
ns2
ns1
acc
)
ns1
.
ns_ns
s
in
let
inst_ts
=
M
nm
.
fold
(
fun
nm
ts1
acc
->
if
not
(
M
nm
.
mem
nm
ns2
.
ns_ts
)
then
acc
else
let
inst_ts
=
M
str
.
fold
(
fun
nm
ts1
acc
->
if
not
(
M
str
.
mem
nm
ns2
.
ns_ts
)
then
acc
else
if
not
(
Sid
.
mem
ts1
.
ts_name
sl
)
then
acc
else
if
Mts
.
mem
ts1
acc
then
clash
ts1
.
ts_name
else
let
ts2
=
M
nm
.
find
nm
ns2
.
ns_ts
in
let
ts2
=
M
str
.
find
nm
ns2
.
ns_ts
in
Mts
.
add
ts1
ts2
acc
)
ns1
.
ns_ts
s
.
inst_ts
in
let
inst_ls
=
M
nm
.
fold
(
fun
nm
ls1
acc
->
if
not
(
M
nm
.
mem
nm
ns2
.
ns_ls
)
then
acc
else
let
inst_ls
=
M
str
.
fold
(
fun
nm
ls1
acc
->
if
not
(
M
str
.
mem
nm
ns2
.
ns_ls
)
then
acc
else
if
not
(
Sid
.
mem
ls1
.
ls_name
sl
)
then
acc
else
if
Mls
.
mem
ls1
acc
then
clash
ls1
.
ls_name
else
let
ls2
=
M
nm
.
find
nm
ns2
.
ns_ls
in
let
ls2
=
M
str
.
find
nm
ns2
.
ns_ls
in
Mls
.
add
ls1
ls2
acc
)
ns1
.
ns_ls
s
.
inst_ls
in
{
s
with
inst_ts
=
inst_ts
;
inst_ls
=
inst_ls
}
...
...
@@ -1180,8 +1180,8 @@ let close_theory loc lenv th =
if
Debug
.
test_flag
debug_parse_only
then
lenv
else
let
th
=
close_theory
th
in
let
id
=
th
.
th_name
.
id_string
in
if
M
nm
.
mem
id
lenv
then
error
~
loc
(
ClashTheory
id
);
M
nm
.
add
id
th
lenv
if
M
str
.
mem
id
lenv
then
error
~
loc
(
ClashTheory
id
);
M
str
.
add
id
th
lenv
let
close_namespace
loc
import
name
th
=
let
id
=
option_map
(
fun
id
->
id
.
id
)
name
in
...
...
src/parser/typing.mli
View file @
1914661d
...
...
@@ -29,12 +29,12 @@ val debug_type_only : Debug.flag
(** incremental parsing *)
val
add_decl
:
Env
.
env
->
theory
M
nm
.
t
->
theory_uc
->
Ptree
.
decl
->
theory_uc
val
add_decl
:
Env
.
env
->
theory
M
str
.
t
->
theory_uc
->
Ptree
.
decl
->
theory_uc
val
close_namespace
:
Loc
.
position
->
bool
->
Ptree
.
ident
option
->
theory_uc
->
theory_uc
val
close_theory
:
Loc
.
position
->
theory
M
nm
.
t
->
theory_uc
->
theory
M
nm
.
t
val
close_theory
:
Loc
.
position
->
theory
M
str
.
t
->
theory_uc
->
theory
M
str
.
t
(******************************************************************************)
(** The following is exported for program typing (src/programs/pgm_typing.ml) *)
...
...
src/programs/pgm_env.ml
View file @
1914661d
...
...
@@ -18,10 +18,11 @@
(**************************************************************************)
open
Why
open
Util
open
Theory
open
Pgm_module
type
module_file
=
Theory
.
theory
M
nm
.
t
*
Pgm_module
.
t
M
nm
.
t
type
module_file
=
Theory
.
theory
M
str
.
t
*
Pgm_module
.
t
M
str
.
t
type
t
=
{
env
:
Env
.
env
;
...
...
@@ -45,7 +46,7 @@ let find_library penv sl =
try
Hashtbl
.
find
penv
.
memo
sl
with
Not_found
->
Hashtbl
.
add
penv
.
memo
sl
(
M
nm
.
empty
,
M
nm
.
empty
);
Hashtbl
.
add
penv
.
memo
sl
(
M
str
.
empty
,
M
str
.
empty
);
let
file
,
c
=
Env
.
find_channel
penv
.
env
"whyml"
sl
in
let
r
=
penv
.
retrieve
penv
file
c
in
close_in
c
;
...
...
@@ -53,5 +54,5 @@ let find_library penv sl =
r
let
find_module
penv
sl
s
=
try
M
nm
.
find
s
(
snd
(
find_library
penv
sl
))
try
M
str
.
find
s
(
snd
(
find_library
penv
sl
))
with
Not_found
->
raise
(
ModuleNotFound
(
sl
,
s
))
src/programs/pgm_env.mli
View file @
1914661d
...
...
@@ -25,7 +25,7 @@ type t
val
get_env
:
t
->
Env
.
env
type
module_file
=
Theory
.
theory
Mnm
.
t
*
Pgm_module
.
t
Mnm
.
t
type
module_file
=
Theory
.
theory
Util
.
Mstr
.
t
*
Pgm_module
.
t
Util
.
Mstr
.
t
type
retrieve_module
=
t
->
string
->
in_channel
->
module_file
...
...
src/programs/pgm_main.ml
View file @
1914661d
...
...
@@ -36,7 +36,7 @@ let () = Exn_printer.register (fun fmt e -> match e with
let
add_module
?
(
type_only
=
false
)
env
penv
(
ltm
,
lmod
)
m
=
let
id
=
m
.
mod_name
in
let
loc
=
id
.
id_loc
in
if
M
nm
.
mem
id
.
id
lmod
then
raise
(
Loc
.
Located
(
loc
,
ClashModule
id
.
id
));
if
M
str
.
mem
id
.
id
lmod
then
raise
(
Loc
.
Located
(
loc
,
ClashModule
id
.
id
));
let
wp
=
not
type_only
in
let
uc
=
create_module
(
Ident
.
id_user
id
.
id
loc
)
in
let
prelude
=
Env
.
find_theory
env
[
"bool"
]
"Bool"
in
...
...
@@ -45,20 +45,20 @@ let add_module ?(type_only=false) env penv (ltm, lmod) m =
List
.
fold_left
(
Pgm_typing
.
decl
~
wp
env
penv
ltm
lmod
)
uc
m
.
mod_decl
in
let
m
=
close_module
uc
in
M
nm
.
add
id
.
id
m
.
m_pure
ltm
,
M
nm
.
add
id
.
id
m
lmod
M
str
.
add
id
.
id
m
.
m_pure
ltm
,
M
str
.
add
id
.
id
m
lmod
let
retrieve
penv
file
c
=
let
lb
=
Lexing
.
from_channel
c
in
Loc
.
set_file
file
lb
;
let
ml
=
Lexer
.
parse_program_file
lb
in
if
Debug
.
test_flag
Typing
.
debug_parse_only
then
M
nm
.
empty
,
M
nm
.
empty
M
str
.
empty
,
M
str
.
empty
else
let
type_only
=
Debug
.
test_flag
Typing
.
debug_type_only
in
let
env
=
Pgm_env
.
get_env
penv
in
List
.
fold_left
(
add_module
~
type_only
env
penv
)
(
M
nm
.
empty
,
M
nm
.
empty
)
ml
(
M
str
.
empty
,
M
str
.
empty
)
ml
let
pgm_env_of_env
=
let
h
=
Env
.
Wenv
.
create
17
in
...
...
src/programs/pgm_module.ml
View file @
1914661d
...
...
@@ -30,13 +30,13 @@ open Pgm_types.T
open
Pgm_ttree
type
namespace
=
{
ns_ex
:
esymbol
M
nm
.
t
;
(* exceptions*)
ns_ns
:
namespace
M
nm
.
t
;
(* inner namespaces *)
ns_ex
:
esymbol
M
str
.
t
;
(* exceptions*)
ns_ns
:
namespace
M
str
.
t
;
(* inner namespaces *)
}
let
empty_ns
=
{
ns_ex
=
M
nm
.
empty
;
ns_ns
=
M
nm
.
empty
;
ns_ex
=
M
str
.
empty
;
ns_ns
=
M
str
.
empty
;
}
exception
ClashSymbol
of
string
...
...
@@ -47,18 +47,18 @@ let ns_replace eq chk x vo vn =
raise
(
ClashSymbol
x
)
let
ns_union
eq
chk
=
M
nm
.
union
(
fun
x
vn
vo
->
Some
(
ns_replace
eq
chk
x
vo
vn
))
M
str
.
union
(
fun
x
vn
vo
->
Some
(
ns_replace
eq
chk
x
vo
vn
))
let
rec
merge_ns
chk
ns1
ns2
=
let
fusion
_
ns1
ns2
=
Some
(
merge_ns
chk
ns1
ns2
)
in
{
ns_ex
=
ns_union
ls_equal
chk
ns1
.
ns_ex
ns2
.
ns_ex
;
ns_ns
=
M
nm
.
union
fusion
ns1
.
ns_ns
ns2
.
ns_ns
;
}
ns_ns
=
M
str
.
union
fusion
ns1
.
ns_ns
ns2
.
ns_ns
;
}
let
nm_add
chk
x
ns
m
=
M
nm
.
change
x
(
function
let
nm_add
chk
x
ns
m
=
M
str
.
change
x
(
function
|
None
->
Some
ns
|
Some
os
->
Some
(
merge_ns
chk
ns
os
))
m
let
ns_add
eq
chk
x
v
m
=
M
nm
.
change
x
(
function
let
ns_add
eq
chk
x
v
m
=
M
str
.
change
x
(
function
|
None
->
Some
v
|
Some
vo
->
Some
(
ns_replace
eq
chk
x
vo
v
))
m
...
...
@@ -70,8 +70,8 @@ let add_ns chk x nn ns = { ns with ns_ns = nm_add chk x nn ns.ns_ns }
let
rec
ns_find
get_map
ns
=
function
|
[]
->
assert
false
|
[
a
]
->
M
nm
.
find
a
(
get_map
ns
)
|
a
::
l
->
ns_find
get_map
(
M
nm
.
find
a
ns
.
ns_ns
)
l
|
[
a
]
->
M
str
.
find
a
(
get_map
ns
)
|
a
::
l
->
ns_find
get_map
(
M
str
.
find
a
ns
.
ns_ns
)
l
let
ns_find_ex
=
ns_find
(
fun
ns
->
ns
.
ns_ex
)
let
ns_find_ns
=
ns_find
(
fun
ns
->
ns
.
ns_ns
)
...
...
@@ -259,8 +259,8 @@ let use_export_theory uc th =
(
create_mtsymbol
~
impure
:
ts
~
effect
:
ts
~
pure
:
ts
~
singleton
:
false
)
in
let
rec
add_ns
ns
uc
=
M
nm
.
iter
add_ts
ns
.
Theory
.
ns_ts
;
M
nm
.
fold
(
fun
_
->
add_ns
)
ns
.
Theory
.
ns_ns
uc
M
str
.
iter
add_ts
ns
.
Theory
.
ns_ts
;
M
str
.
fold
(
fun
_
->
add_ns
)
ns
.
Theory
.
ns_ns
uc
in
add_ns
th
.
th_export
uc
...
...
src/programs/pgm_module.mli
View file @
1914661d
...
...
@@ -26,8 +26,8 @@ open Pgm_types
open
Pgm_types
.
T
type
namespace
=
private
{
ns_ex
:
esymbol
Mnm
.
t
;
(* exception symbols *)
ns_ns
:
namespace
Mnm
.
t
;
(* inner namespaces *)
ns_ex
:
esymbol
Util
.
Mstr
.
t
;
(* exception symbols *)
ns_ns
:
namespace
Util
.
Mstr
.
t
;
(* inner namespaces *)
}
val
ns_find_ex
:
namespace
->
string
list
->
esymbol
...
...
@@ -74,14 +74,14 @@ val add_effect_decl : Decl.decl -> uc -> uc
val
add_pure_decl
:
Decl
.
decl
->
uc
->
uc
val
add_impure_pdecl
:
Env
.
env
->
Theory
.
theory
Theory
.
Mnm
.
t
->
Ptree
.
decl
->
uc
->
uc
Env
.
env
->
Theory
.
theory
Util
.
Mstr
.
t
->
Ptree
.
decl
->
uc
->
uc
val
add_effect_pdecl
:
Env
.
env
->
Theory
.
theory
Theory
.
Mnm
.
t
->
Ptree
.
decl
->
uc
->
uc
Env
.
env
->
Theory
.
theory
Util
.
Mstr
.
t
->
Ptree
.
decl
->
uc
->
uc
val
add_pure_pdecl
:
Env
.
env
->
Theory
.
theory
Theory
.
Mnm
.
t
->
Ptree
.
decl
->
uc
->
uc
Env
.
env
->
Theory
.
theory
Util
.
Mstr
.
t
->
Ptree
.
decl
->
uc
->
uc
val
add_pdecl
:
Env
.
env
->
Theory
.
theory
Theory
.
Mnm
.
t
->
Ptree
.
decl
->
uc
->
uc
Env
.
env
->
Theory
.
theory
Util
.
Mstr
.
t
->
Ptree
.
decl
->
uc
->
uc
(** add in impure, effect and pure *)
(** builtins *)
...
...
src/programs/pgm_typing.ml
View file @
1914661d
...
...
@@ -2176,7 +2176,7 @@ let add_logics env ltm uc d =
let
find_module
penv
lmod
q
id
=
match
q
with
|
[]
->
(* local module *)
M
nm
.
find
id
lmod
M
str
.
find
id
lmod
|
_
::
_
->
(* theory in file f *)
Pgm_env
.
find_module
penv
q
id
...
...
src/programs/pgm_typing.mli
View file @
1914661d
...
...
@@ -18,12 +18,11 @@
(**************************************************************************)
open
Why
open
Util
val
debug
:
Debug
.
flag
val
decl
:
wp
:
bool
->
Env
.
env
->
Pgm_env
.
t
->
Theory
.
theory
Theory
.
Mnm
.
t
->
Pgm_module
.
t
Theory
.
Mnm
.
t
->
Theory
.
theory
Util
.
Mstr
.
t
->
Pgm_module
.
t
Util
.
Mstr
.
t
->
Pgm_module
.
uc
->
Ptree
.
program_decl
->
Pgm_module
.
uc
Prev
1
2
Next
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