Skip to content
GitLab
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
a908f0e3
Commit
a908f0e3
authored
Nov 27, 2013
by
Stefan Berghofer
Browse files
fixed incorrect assumptions in realization code
parent
94b1bdd4
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/printer/isabelle.ml
View file @
a908f0e3
...
...
@@ -418,20 +418,20 @@ let print_task printer_args realize fmt task =
|
_
->
assert
false
)
Mid
.
empty
task
in
(* two cases: task is clone T with [] or task is a real goal *)
let
thname
,
realized_theories
=
match
task
with
|
None
->
assert
false
let
rec
upd_realized_theories
=
function
|
Some
{
Task
.
task_decl
=
{
Theory
.
td_node
=
Theory
.
Decl
{
Decl
.
d_node
=
Decl
.
Dprop
(
Decl
.
Pgoal
,
pr
,
_
)
}}}
->
id_unique
thprinter
pr
.
pr_name
,
realized_theories
|
Some
{
Task
.
task_decl
=
{
Theory
.
td_node
=
Theory
.
Clone
(
th
,_
)
}}
->
Sid
.
iter
(
fun
id
->
ignore
(
id_unique
iprinter
id
))
th
.
Theory
.
th_local
;
let
id
=
th
.
Theory
.
th_name
in
String
.
concat
"."
(
th
.
Theory
.
th_path
@
[
id_unique
thprinter
id
])
,
Mid
.
remove
id
realized_theories
|
Some
{
Task
.
task_decl
=
{
Theory
.
td_node
=
td
}
}
->
let
name
=
match
td
with
|
Theory
.
Decl
{
Decl
.
d_node
=
Dprop
(
_
,
pr
,
_
)
}
->
id_unique
thprinter
pr
.
pr_name
|
_
->
"goal"
in
name
,
realized_theories
in
|
Some
{
Task
.
task_decl
=
{
Theory
.
td_node
=
Theory
.
Meta
_
};
Task
.
task_prev
=
task
}
->
upd_realized_theories
task
|
_
->
assert
false
in
let
thname
,
realized_theories
=
upd_realized_theories
task
in
(* make names as stable as possible by first printing all identifiers *)
let
realized_theories'
=
Mid
.
map
fst
realized_theories
in
let
realized_symbols
=
Task
.
used_symbols
realized_theories'
in
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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