Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
1312788c
Commit
1312788c
authored
Aug 06, 2015
by
Andrei Paskevich
Browse files
API: rename [open|close]_namespace to [open|close]_scope
parent
d1453b19
Changes
15
Hide whitespace changes
Inline
Side-by-side
doc/api.tex
View file @
1312788c
...
...
@@ -398,9 +398,9 @@ provide a helper function for that:
theory th1 under construction *)
let use th1 th2 =
let name = th2.Theory.th
_
name in
Theory.close
_
namespace
Theory.close
_
scope
(Theory.use
_
export
(Theory.open
_
namespac
e th1 name.Ident.id
_
string) th2) true
(Theory.open
_
scop
e th1 name.Ident.id
_
string) th2) true
\end{ocamlcode}
Addition of formula 3 is then
\begin{ocamlcode}
...
...
examples/use_api/logic.ml
View file @
1312788c
...
...
@@ -201,9 +201,9 @@ let my_theory : Theory.theory_uc = Theory.add_decl my_theory decl_goal2
in theory th1 under construction *)
let
use
th1
th2
=
let
name
=
th2
.
Theory
.
th_name
in
Theory
.
close_
namespac
e
(
Theory
.
use_export
(
Theory
.
open_
namespac
e
th1
name
.
Ident
.
id_string
)
th2
)
true
Theory
.
close_
scop
e
(
Theory
.
use_export
(
Theory
.
open_
scop
e
th1
name
.
Ident
.
id_string
)
th2
)
~
import
:
true
let
()
=
printf
"@[adding goal 3@]@."
(* use import int.Int *)
...
...
examples/use_api/mlw_tree.ml
View file @
1312788c
...
...
@@ -46,22 +46,6 @@ let t : Ptree.incremental = Mlw_typing.open_file env pathname
open
Ptree
(*
type incremental = {
open_theory : ident -> unit;
close_theory : unit -> unit;
open_module : ident -> unit;
close_module : unit -> unit;
open_namespace : string -> unit;
close_namespace : loc -> bool (*import:*) -> unit;
new_decl : loc -> decl -> unit;
new_pdecl : loc -> pdecl -> unit;
use_clone : loc -> use_clone -> unit;
}
*)
(* start a module *)
let
mk_ident
?
(
label
=
[]
)
?
(
loc
=
Loc
.
dummy_position
)
s
=
{
...
...
plugins/tptp/tptp_typing.ml
View file @
1312788c
...
...
@@ -574,9 +574,9 @@ let typedecl denv env impl loc s (tvl,(el,e)) =
let
flush_impl
~
strict
env
uc
impl
=
let
update_th
_
e
uc
=
match
e
with
|
Suse
th
->
let
uc
=
open_
namespac
e
uc
th
.
th_name
.
id_string
in
let
uc
=
open_
scop
e
uc
th
.
th_name
.
id_string
in
let
uc
=
use_export
uc
th
in
close_
namespace
uc
false
close_
scope
uc
~
import
:
false
|
_
->
uc
in
let
update
s
e
(
env
,
uc
)
=
match
e
with
...
...
src/core/theory.ml
View file @
1312788c
...
...
@@ -288,14 +288,14 @@ let close_theory uc = match uc.uc_export with
let
get_namespace
uc
=
List
.
hd
uc
.
uc_import
let
open_
namespac
e
uc
s
=
match
uc
.
uc_import
with
let
open_
scop
e
uc
s
=
match
uc
.
uc_import
with
|
ns
::
_
->
{
uc
with
uc_prefix
=
s
::
uc
.
uc_prefix
;
uc_import
=
ns
::
uc
.
uc_import
;
uc_export
=
empty_ns
::
uc
.
uc_export
;
}
|
[]
->
assert
false
let
close_
namespac
e
uc
import
=
let
close_
scop
e
uc
~
import
=
match
uc
.
uc_prefix
,
uc
.
uc_import
,
uc
.
uc_export
with
|
s
::
prf
,
_
::
i1
::
sti
,
e0
::
e1
::
ste
->
let
i1
=
if
import
then
merge_ns
false
e0
i1
else
i1
in
...
...
src/core/theory.mli
View file @
1312788c
...
...
@@ -131,8 +131,8 @@ type theory_uc = private {
val
create_theory
:
?
path
:
string
list
->
preid
->
theory_uc
val
close_theory
:
theory_uc
->
theory
val
open_
namespac
e
:
theory_uc
->
string
->
theory_uc
val
close_
namespac
e
:
theory_uc
->
bool
(*
import
*)
->
theory_uc
val
open_
scop
e
:
theory_uc
->
string
->
theory_uc
val
close_
scop
e
:
theory_uc
->
import
:
bool
->
theory_uc
val
get_namespace
:
theory_uc
->
namespace
...
...
src/jessie/ACSLtoWhy3.ml
View file @
1312788c
...
...
@@ -748,8 +748,8 @@ and predicate_named ~label p = predicate ~label p.content
let
use
th1
th2
=
let
name
=
th2
.
Theory
.
th_name
in
Theory
.
close_
namespac
e
(
Theory
.
use_export
(
Theory
.
open_
namespac
e
th1
name
.
Ident
.
id_string
)
th2
)
Theory
.
close_
scop
e
(
Theory
.
use_export
(
Theory
.
open_
scop
e
th1
name
.
Ident
.
id_string
)
th2
)
true
let
add_decl
th
d
=
...
...
@@ -1330,17 +1330,17 @@ let add_pdecl m d =
let
use
m
th
=
let
name
=
th
.
Theory
.
th_name
in
Mlw_module
.
close_
namespac
e
Mlw_module
.
close_
scop
e
(
Mlw_module
.
use_export_theory
(
Mlw_module
.
open_
namespac
e
m
name
.
Ident
.
id_string
)
(
Mlw_module
.
open_
scop
e
m
name
.
Ident
.
id_string
)
th
)
true
let
use_module
m
modul
=
let
name
=
modul
.
Mlw_module
.
mod_theory
.
Theory
.
th_name
in
Mlw_module
.
close_
namespac
e
Mlw_module
.
close_
scop
e
(
Mlw_module
.
use_export
(
Mlw_module
.
open_
namespac
e
m
name
.
Ident
.
id_string
)
(
Mlw_module
.
open_
scop
e
m
name
.
Ident
.
id_string
)
modul
)
true
...
...
src/mlw/pmodule.ml
View file @
1312788c
...
...
@@ -155,16 +155,16 @@ let close_module, restore_module =
m
)
,
(
fun
th
->
Hid
.
find
h
th
.
th_name
)
let
open_
namespac
e
uc
s
=
match
uc
.
muc_import
with
let
open_
scop
e
uc
s
=
match
uc
.
muc_import
with
|
ns
::
_
->
{
uc
with
muc_theory
=
Theory
.
open_
namespac
e
uc
.
muc_theory
s
;
muc_theory
=
Theory
.
open_
scop
e
uc
.
muc_theory
s
;
muc_units
=
[
Uscope
(
s
,
false
,
uc
.
muc_units
)];
muc_import
=
ns
::
uc
.
muc_import
;
muc_export
=
empty_ns
::
uc
.
muc_export
;
}
|
[]
->
assert
false
let
close_
namespac
e
uc
~
import
=
let
th
=
Theory
.
close_
namespac
e
uc
.
muc_theory
import
in
let
close_
scop
e
uc
~
import
=
let
th
=
Theory
.
close_
scop
e
uc
.
muc_theory
~
import
in
match
List
.
rev
uc
.
muc_units
,
uc
.
muc_import
,
uc
.
muc_export
with
|
Uscope
(
s
,_,
ul1
)
::
ul0
,
_
::
i1
::
sti
,
e0
::
e1
::
ste
->
let
i1
=
if
import
then
merge_ns
false
e0
i1
else
i1
in
...
...
src/mlw/pmodule.mli
View file @
1312788c
...
...
@@ -86,8 +86,8 @@ type pmodule_uc = private {
val
create_module
:
Env
.
env
->
?
path
:
string
list
->
preid
->
pmodule_uc
val
close_module
:
pmodule_uc
->
pmodule
val
open_
namespac
e
:
pmodule_uc
->
string
->
pmodule_uc
val
close_
namespac
e
:
pmodule_uc
->
import
:
bool
->
pmodule_uc
val
open_
scop
e
:
pmodule_uc
->
string
->
pmodule_uc
val
close_
scop
e
:
pmodule_uc
->
import
:
bool
->
pmodule_uc
val
restore_path
:
ident
->
string
list
*
string
*
string
list
(** [restore_path id] returns the triple (library path, module,
...
...
src/parser/parser.mly
View file @
1312788c
...
...
@@ -183,11 +183,11 @@ module_head:
scope_head
:
|
SCOPE
boption
(
IMPORT
)
uident
{
Typing
.
open_
namespac
e
(
floc
$
startpos
$
endpos
)
$
3
;
$
2
}
{
Typing
.
open_
scop
e
(
floc
$
startpos
$
endpos
)
$
3
;
$
2
}
module_decl
:
|
scope_head
module_decl
*
END
{
Typing
.
close_
namespac
e
(
floc
$
startpos
(
$
1
)
$
endpos
(
$
1
))
~
import
:$
1
}
{
Typing
.
close_
scop
e
(
floc
$
startpos
(
$
1
)
$
endpos
(
$
1
))
~
import
:$
1
}
|
d
=
pure_decl
|
d
=
prog_decl
|
d
=
meta_decl
{
Typing
.
add_decl
(
floc
$
startpos
$
endpos
)
d
}
|
use_clone
{
()
}
...
...
@@ -201,14 +201,14 @@ use_clone:
{
Typing
.
add_decl
(
floc
$
startpos
$
endpos
)
(
Dclone
(
$
3
,
$
4
))
}
|
USE
boption
(
IMPORT
)
tqualid
option
(
preceded
(
AS
,
uident
))
{
let
loc
=
floc
$
startpos
$
endpos
in
Typing
.
open_
namespac
e
loc
(
use_as
$
3
$
4
);
Typing
.
open_
scop
e
loc
(
use_as
$
3
$
4
);
Typing
.
add_decl
loc
(
Duse
$
3
);
Typing
.
close_
namespac
e
loc
~
import
:$
2
}
Typing
.
close_
scop
e
loc
~
import
:$
2
}
|
CLONE
boption
(
IMPORT
)
tqualid
option
(
preceded
(
AS
,
uident
))
clone_subst
{
let
loc
=
floc
$
startpos
$
endpos
in
Typing
.
open_
namespac
e
loc
(
use_as
$
3
$
4
);
Typing
.
open_
scop
e
loc
(
use_as
$
3
$
4
);
Typing
.
add_decl
loc
(
Dclone
(
$
3
,
$
5
));
Typing
.
close_
namespac
e
loc
~
import
:$
2
}
Typing
.
close_
scop
e
loc
~
import
:$
2
}
clone_subst
:
|
(* epsilon *)
{
[]
}
...
...
src/parser/typing.ml
View file @
1312788c
...
...
@@ -1111,18 +1111,18 @@ let top_muc_on_demand loc slice = match slice.muc with
slice
.
muc
<-
Some
muc
;
muc
let
open_
namespac
e
loc
nm
=
let
open_
scop
e
loc
nm
=
assert
(
not
(
Stack
.
is_empty
state
));
let
slice
=
Stack
.
top
state
in
let
muc
=
top_muc_on_demand
loc
slice
in
if
Debug
.
test_noflag
debug_parse_only
then
slice
.
muc
<-
Some
(
open_
namespac
e
muc
nm
.
id_str
)
slice
.
muc
<-
Some
(
open_
scop
e
muc
nm
.
id_str
)
let
close_
namespac
e
loc
~
import
=
let
close_
scop
e
loc
~
import
=
assert
(
not
(
Stack
.
is_empty
state
)
&&
(
Stack
.
top
state
)
.
muc
<>
None
);
if
Debug
.
test_noflag
debug_parse_only
then
let
slice
=
Stack
.
top
state
in
let
muc
=
Loc
.
try1
~
loc
(
close_
namespac
e
~
import
)
(
Opt
.
get
slice
.
muc
)
in
let
muc
=
Loc
.
try1
~
loc
(
close_
scop
e
~
import
)
(
Opt
.
get
slice
.
muc
)
in
slice
.
muc
<-
Some
muc
let
add_decl
loc
d
=
...
...
src/parser/typing.mli
View file @
1312788c
...
...
@@ -21,8 +21,8 @@ val open_module : Ptree.ident -> unit
val
close_module
:
Loc
.
position
->
unit
val
open_
namespac
e
:
Loc
.
position
->
Ptree
.
ident
->
unit
val
open_
scop
e
:
Loc
.
position
->
Ptree
.
ident
->
unit
val
close_
namespac
e
:
Loc
.
position
->
import
:
bool
->
unit
val
close_
scop
e
:
Loc
.
position
->
import
:
bool
->
unit
val
add_decl
:
Loc
.
position
->
Ptree
.
decl
->
unit
src/whyml/mlw_module.ml
View file @
1312788c
...
...
@@ -193,16 +193,16 @@ let get_theory uc = uc.muc_theory
let
get_namespace
uc
=
List
.
hd
uc
.
muc_import
let
get_known
uc
=
uc
.
muc_known
let
open_
namespac
e
uc
s
=
match
uc
.
muc_import
with
let
open_
scop
e
uc
s
=
match
uc
.
muc_import
with
|
ns
::
_
->
{
uc
with
muc_theory
=
Theory
.
open_
namespac
e
uc
.
muc_theory
s
;
muc_theory
=
Theory
.
open_
scop
e
uc
.
muc_theory
s
;
muc_prefix
=
s
::
uc
.
muc_prefix
;
muc_import
=
ns
::
uc
.
muc_import
;
muc_export
=
empty_ns
::
uc
.
muc_export
;
}
|
[]
->
assert
false
let
close_
namespac
e
uc
import
=
let
th
=
Theory
.
close_
namespac
e
uc
.
muc_theory
import
in
(* catches errors *)
let
close_
scop
e
uc
import
=
let
th
=
Theory
.
close_
scop
e
uc
.
muc_theory
import
in
(* catches errors *)
match
uc
.
muc_prefix
,
uc
.
muc_import
,
uc
.
muc_export
with
|
s
::
prf
,
_
::
i1
::
sti
,
e0
::
e1
::
ste
->
let
i1
=
if
import
then
merge_ns
false
e0
i1
else
i1
in
...
...
src/whyml/mlw_module.mli
View file @
1312788c
...
...
@@ -70,8 +70,8 @@ type module_uc (* a module under construction *)
val
create_module
:
Env
.
env
->
?
path
:
string
list
->
preid
->
module_uc
val
close_module
:
module_uc
->
modul
val
open_
namespac
e
:
module_uc
->
string
->
module_uc
val
close_
namespac
e
:
module_uc
->
bool
->
module_uc
val
open_
scop
e
:
module_uc
->
string
->
module_uc
val
close_
scop
e
:
module_uc
->
bool
->
module_uc
val
get_theory
:
module_uc
->
theory_uc
val
get_namespace
:
module_uc
->
namespace
...
...
src/whyml/mlw_typing.ml
View file @
1312788c
...
...
@@ -1172,7 +1172,7 @@ let use_clone_pure env mth uc loc (use,inst) =
if
Debug
.
test_flag
Glob
.
flag
then
Glob
.
use
s
.
id_loc
th
.
th_name
;
(* open namespace, if any *)
let
uc
=
match
use
.
use_import
with
|
Some
(
_
,
use_as
)
->
Theory
.
open_
namespac
e
uc
use_as
|
Some
(
_
,
use_as
)
->
Theory
.
open_
scop
e
uc
use_as
|
None
->
uc
in
(* use or clone *)
let
uc
=
match
inst
with
...
...
@@ -1182,7 +1182,7 @@ let use_clone_pure env mth uc loc (use,inst) =
Theory
.
clone_export
uc
th
(
Typing
.
type_inst
uc
th
inst
)
in
(* close namespace, if any *)
match
use
.
use_import
with
|
Some
(
import
,
_
)
->
Theory
.
close_
namespac
e
uc
import
|
Some
(
import
,
_
)
->
Theory
.
close_
scop
e
uc
import
|
None
->
uc
let
use_clone_pure
env
mth
uc
loc
use
=
...
...
@@ -1198,7 +1198,7 @@ let use_clone env mmd mth uc loc (use,inst) =
(
match
mth
with
Module
m
->
m
.
mod_theory
.
th_name
|
Theory
th
->
th
.
th_name
);
(* open namespace, if any *)
let
uc
=
match
use
.
use_import
with
|
Some
(
_
,
use_as
)
->
open_
namespac
e
uc
use_as
|
Some
(
_
,
use_as
)
->
open_
scop
e
uc
use_as
|
None
->
uc
in
(* use or clone *)
let
uc
=
match
mth
,
inst
with
...
...
@@ -1235,7 +1235,7 @@ let use_clone env mmd mth uc loc (use,inst) =
clone_export_theory
uc
th
(
Typing
.
type_inst
(
get_theory
uc
)
th
inst
)
in
(* close namespace, if any *)
match
use
.
use_import
with
|
Some
(
import
,
_
)
->
close_
namespac
e
uc
import
|
Some
(
import
,
_
)
->
close_
scop
e
uc
import
|
None
->
uc
let
use_clone
env
mmd
mth
uc
loc
use
=
...
...
@@ -1277,12 +1277,12 @@ let open_file, close_file =
Stack
.
push
(
close_theory
(
Stack
.
pop
lenv
)
(
Stack
.
pop
tuc
))
lenv
in
let
close_module
()
=
ignore
(
Stack
.
pop
inm
);
Stack
.
push
(
close_module
(
Stack
.
pop
lenv
)
(
Stack
.
pop
muc
))
lenv
in
let
open_
namespac
e
name
=
if
Stack
.
top
inm
then
Stack
.
push
(
Mlw_module
.
open_
namespac
e
(
Stack
.
pop
muc
)
name
)
muc
else
Stack
.
push
(
Theory
.
open_
namespac
e
(
Stack
.
pop
tuc
)
name
)
tuc
in
let
close_
namespac
e
imp
=
if
Stack
.
top
inm
then
Stack
.
push
(
Mlw_module
.
close_
namespac
e
(
Stack
.
pop
muc
)
imp
)
muc
else
Stack
.
push
(
Theory
.
close_
namespac
e
(
Stack
.
pop
tuc
)
imp
)
tuc
in
let
open_
scop
e
name
=
if
Stack
.
top
inm
then
Stack
.
push
(
Mlw_module
.
open_
scop
e
(
Stack
.
pop
muc
)
name
)
muc
else
Stack
.
push
(
Theory
.
open_
scop
e
(
Stack
.
pop
tuc
)
name
)
tuc
in
let
close_
scop
e
imp
=
if
Stack
.
top
inm
then
Stack
.
push
(
Mlw_module
.
close_
scop
e
(
Stack
.
pop
muc
)
imp
)
muc
else
Stack
.
push
(
Theory
.
close_
scop
e
(
Stack
.
pop
tuc
)
imp
)
tuc
in
let
new_decl
loc
d
=
if
Stack
.
top
inm
then
Stack
.
push
(
add_decl
~
wp
loc
(
Stack
.
pop
muc
)
d
)
muc
else
Stack
.
push
(
Typing
.
add_decl
loc
(
Stack
.
pop
tuc
)
d
)
tuc
in
...
...
@@ -1295,8 +1295,8 @@ let open_file, close_file =
close_theory
=
close_theory
;
open_module
=
open_module
;
close_module
=
close_module
;
open_
namespac
e
=
open_
namespac
e
;
close_
namespac
e
=
(
fun
loc
imp
->
Loc
.
try1
~
loc
close_
namespac
e
imp
);
open_
scop
e
=
open_
scop
e
;
close_
scop
e
=
(
fun
loc
imp
->
Loc
.
try1
~
loc
close_
scop
e
imp
);
new_decl
=
new_decl
;
new_pdecl
=
new_pdecl
;
use_clone
=
use_clone
;
}
...
...
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