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
121
Issues
121
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
fa077ec4
Commit
fa077ec4
authored
Mar 21, 2013
by
Andrei Paskevich
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
fix why3session.dtd
parent
3aa8f430
Changes
3
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
293 additions
and
357 deletions
+293
-357
examples/logic/triangle_inequality/why3session.xml
examples/logic/triangle_inequality/why3session.xml
+281
-341
share/why3session.dtd
share/why3session.dtd
+4
-5
src/session/session.ml
src/session/session.ml
+8
-11
No files found.
examples/logic/triangle_inequality/why3session.xml
View file @
fa077ec4
This diff is collapsed.
Click to expand it.
share/why3session.dtd
View file @
fa077ec4
...
...
@@ -55,23 +55,22 @@
<!ELEMENT label EMPTY>
<!ATTLIST label name CDATA #REQUIRED>
<!ELEMENT metas (ts_pos*,
ls_pos*, pr_pos*,
meta_args*,goal)>
<!ELEMENT metas (ts_pos*,
ls_pos*,pr_pos*,
meta_args*,goal)>
<!ATTLIST metas proved CDATA #REQUIRED>
<!ATTLIST metas expanded CDATA #IMPLIED>
<!ELEMENT ts_pos (ip_library
+
,ip_qualid+)>
<!ELEMENT ts_pos (ip_library
*
,ip_qualid+)>
<!ATTLIST ts_pos name CDATA #REQUIRED>
<!ATTLIST ts_pos arity CDATA #REQUIRED>
<!ATTLIST ts_pos id CDATA #REQUIRED>
<!ATTLIST ts_pos ip_theory CDATA #REQUIRED>
<!ELEMENT ls_pos (ip_library+,ip_qualid+)>
<!ELEMENT ls_pos (ip_library*,ip_qualid+)>
<!ATTLIST ls_pos name CDATA #REQUIRED>
<!ATTLIST ls_pos id CDATA #REQUIRED>
<!ATTLIST ls_pos ip_theory CDATA #REQUIRED>
<!ELEMENT pr_pos (ip_library
+
,ip_qualid+)>
<!ELEMENT pr_pos (ip_library
*
,ip_qualid+)>
<!ATTLIST pr_pos name CDATA #REQUIRED>
<!ATTLIST pr_pos id CDATA #REQUIRED>
<!ATTLIST pr_pos ip_theory CDATA #REQUIRED>
...
...
src/session/session.ml
View file @
fa077ec4
...
...
@@ -558,26 +558,25 @@ and save_metas provers fmt _ m =
fprintf
fmt
"@
\n
@[<v 1><metas@ proved=
\"
%b
\"
@ expanded=
\"
%b
\"
>"
m
.
metas_verified
m
.
metas_expanded
;
let
save_pos
fmt
pos
=
fprintf
fmt
"
@
\n
@[<v 1>
ip_theory=
\"
%a
\"
>"
save_string
pos
.
ip_theory
;
fprintf
fmt
"ip_theory=
\"
%a
\"
>"
save_string
pos
.
ip_theory
;
List
.
iter
(
fprintf
fmt
"@
\n
@[<v 1><ip_library@ name=
\"
%a
\"
/>@]"
save_string
)
pos
.
ip_library
;
List
.
iter
(
fprintf
fmt
"@
\n
@[<v 1><ip_qualid@ name=
\"
%a
\"
/>@]"
save_string
)
pos
.
ip_qualid
;
fprintf
fmt
"@]"
;
in
let
save_ts_pos
fmt
ts
pos
=
fprintf
fmt
"@
\n
@[<v 1><ts_pos@ name=
\"
%a
\"
@ arity=
\"
%i
\"
@ \
id=
\"
%i
\"
@ %a
</ts_pos>@]
"
id=
\"
%i
\"
@ %a
@]@
\n
</ts_pos>
"
save_string
ts
.
ts_name
.
id_string
(
List
.
length
ts
.
ts_args
)
(
ts_hash
ts
)
save_pos
pos
in
let
save_ls_pos
fmt
ls
pos
=
(** TODO: add the signature? *)
fprintf
fmt
"@
\n
@[<v 1><ls_pos@ name=
\"
%a
\"
@ id=
\"
%i
\"
@ %a
</ls_pos>@]
"
fprintf
fmt
"@
\n
@[<v 1><ls_pos@ name=
\"
%a
\"
@ id=
\"
%i
\"
@ %a
@]@
\n
</ls_pos>
"
save_string
ls
.
ls_name
.
id_string
(
ls_hash
ls
)
save_pos
pos
in
let
save_pr_pos
fmt
pr
pos
=
fprintf
fmt
"@
\n
@[<v 1><pr_pos@ name=
\"
%a
\"
@ id=
\"
%i
\"
@ %a
</pr_pos>@]
"
fprintf
fmt
"@
\n
@[<v 1><pr_pos@ name=
\"
%a
\"
@ id=
\"
%i
\"
@ %a
@]@
\n
</pr_pos>
"
save_string
pr
.
pr_name
.
id_string
(
pr_hash
pr
)
save_pos
pos
in
...
...
@@ -1888,7 +1887,7 @@ and merge_trans ~keygen ~theories env to_goal _ from_transf =
with
Exit
->
()
(** convert the ident from the ol
f
task to the ident at the same
(** convert the ident from the ol
d
task to the ident at the same
position in the new task *)
and
merge_metas_aux
~
keygen
~
theories
env
to_goal
_
from_metas
=
(** Find in the new task the new symbol (ts,ls,pr) *)
...
...
@@ -1907,11 +1906,9 @@ and merge_metas_aux ~keygen ~theories env to_goal _ from_metas =
let
rec
read_theory
ip
=
function
|
[]
->
raise
(
Env
.
LibFileNotFound
ip
.
ip_library
)
|
format
::
formats
->
try
Env
.
read_theory
~
format
env
.
env
ip
.
ip_library
ip
.
ip_theory
with
Env
.
LibFileNotFound
_
|
Env
.
TheoryNotFound
_
->
read_theory
ip
formats
try
Env
.
read_theory
~
format
env
.
env
ip
.
ip_library
ip
.
ip_theory
with
Env
.
LibFileNotFound
_
|
Env
.
TheoryNotFound
_
->
read_theory
ip
formats
in
let
read_theory
ip
=
if
ip
.
ip_library
=
[]
then
Mstr
.
find
ip
.
ip_theory
theories
...
...
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