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
119
Issues
119
List
Boards
Labels
Service Desk
Milestones
Merge Requests
16
Merge Requests
16
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
bfd52e95
Commit
bfd52e95
authored
Mar 08, 2010
by
Francois Bobot
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
patch propose par andrei, pour gerer cloned
parent
039db14d
Changes
6
Hide whitespace changes
Inline
Side-by-side
Showing
6 changed files
with
29 additions
and
23 deletions
+29
-23
Makefile.in
Makefile.in
+4
-2
configure.in
configure.in
+6
-0
src/core/context_utils.ml
src/core/context_utils.ml
+2
-8
src/core/theory.ml
src/core/theory.ml
+14
-10
src/core/theory.mli
src/core/theory.mli
+1
-1
src/transform/inlining.ml
src/transform/inlining.ml
+2
-2
No files found.
Makefile.in
View file @
bfd52e95
...
...
@@ -50,6 +50,8 @@ OCAMLLIB = @OCAMLLIB@
OCAMLBEST
=
@OCAMLBEST@
OCAMLVERSION
=
@OCAMLVERSION@
CAMLP4
=
@CAMLP4O@
PSVIEWER
=
@PSVIEWER@
PDFVIEWER
=
@PDFVIEWER@
INCLUDES
=
-I
src/core
-I
src/util
-I
src/parser
-I
src/output
\
-I
src/transform
-I
src
...
...
@@ -409,8 +411,8 @@ wc:
dep
:
$(MAKE)
depend
cat
.depend | ocamldot | dot
-Tp
s
>
dep.ps
gv dep.ps
cat
.depend | ocamldot | dot
-Tp
df
>
dep.pdf
$(PDFVIEWER)
dep.pdf
# distrib
#########
...
...
configure.in
View file @
bfd52e95
...
...
@@ -422,6 +422,10 @@ else
fi
fi
#Viewer for ps and pdf
AC_CHECK_PROGS(PSVIEWER,gv evince)
AC_CHECK_PROGS(PDFVIEWER,xpdf acroread evince)
# substitutions to perform
AC_SUBST(VERBOSEMAKE)
AC_SUBST(EXE)
...
...
@@ -473,6 +477,8 @@ AC_SUBST(MIZARLIB)
AC_SUBST(FORPACK)
AC_SUBST(PSVIEWER)
AC_SUBST(PDFVIEWER)
# Finally create the Makefile from Makefile.in
dnl AC_OUTPUT(Makefile)
AC_OUTPUT(Makefile bench/bench)
...
...
src/core/context_utils.ml
View file @
bfd52e95
...
...
@@ -6,11 +6,5 @@ let cloned_from ctxt i1 i2 =
(* Format.printf "@[<hov 2>cloned (%a = %a)?: %a@]@\n"
print_ident i2 print_ident i1
print_ctxt ctxt;*)
let
rec
aux
i
=
i
==
i1
||
try
let
i3
=
Mid
.
find
i
ctxt
.
ctxt_cloned
in
List
.
exists
aux
i3
with
Not_found
->
false
in
aux
i2
try
i1
==
i2
||
Sid
.
mem
i2
(
Mid
.
find
i1
ctxt
.
ctxt_cloned
)
with
Not_found
->
false
src/core/theory.ml
View file @
bfd52e95
...
...
@@ -145,7 +145,7 @@ and namespace = {
and
context
=
{
ctxt_decls
:
(
decl
*
context
)
option
;
ctxt_known
:
decl
Mid
.
t
;
ctxt_cloned
:
ident
lis
t
Mid
.
t
;
ctxt_cloned
:
Sid
.
t
Mid
.
t
;
ctxt_tag
:
int
;
}
...
...
@@ -340,19 +340,23 @@ let empty_inst = {
module
Context
=
struct
let
empty_context
=
Hctxt
.
hashcons
{
ctxt_decls
=
None
;
ctxt_known
=
builtin_known
;
ctxt_decls
=
None
;
ctxt_known
=
builtin_known
;
ctxt_cloned
=
Mid
.
empty
;
ctxt_tag
=
-
1
;
ctxt_tag
=
-
1
;
}
let
push_decl
ctxt
kn
d
=
(* get the set of prototype symbols represented by [id] *)
let
get_cl
m
id
=
try
Mid
.
find
id
m
with
Not_found
->
Sid
.
empty
in
(* add a new association: [id'] represents [id] *)
let
add_cl
m
(
id
,
id'
)
=
(* from now on [id'] represents [id] and everything
* that [id] represented at the moment of cloning *)
Mid
.
add
id'
(
Sid
.
add
id
(
Sid
.
union
(
get_cl
m
id
)
(
get_cl
m
id'
)))
m
in
let
cloned
=
match
d
.
d_node
with
|
Dclone
l
->
List
.
fold_left
(
fun
m
(
i1
,
i2
)
->
let
l
=
try
Mid
.
find
i1
m
with
Not_found
->
[]
in
Mid
.
add
i1
(
i2
::
l
)
m
)
ctxt
.
ctxt_cloned
l
|
Dclone
l
->
List
.
fold_left
add_cl
ctxt
.
ctxt_cloned
l
|
_
->
ctxt
.
ctxt_cloned
in
Hctxt
.
hashcons
{
ctxt
with
...
...
@@ -878,7 +882,7 @@ let print_uc fmt uc = print_namespace fmt (Theory.get_namespace uc)
let
print_ctxt
fmt
ctxt
=
fprintf
fmt
"@[<hov 2>ctxt : cloned : %a@]"
(
Pp
.
print_iter2
Mid
.
iter
Pp
.
semi
(
Pp
.
constant_string
"->"
)
print_ident
(
Pp
.
print_
list
Pp
.
simple_comma
print_ident
))
print_ident
(
Pp
.
print_
iter1
Sid
.
iter
Pp
.
simple_comma
print_ident
))
ctxt
.
ctxt_cloned
let
print_th
fmt
th
=
fprintf
fmt
"<theory (TODO>"
...
...
src/core/theory.mli
View file @
bfd52e95
...
...
@@ -97,7 +97,7 @@ and namespace = private {
and
context
=
private
{
ctxt_decls
:
(
decl
*
context
)
option
;
ctxt_known
:
decl
Mid
.
t
;
ctxt_cloned
:
ident
lis
t
Mid
.
t
;
ctxt_cloned
:
Sid
.
t
Mid
.
t
;
ctxt_tag
:
int
;
}
...
...
src/transform/inlining.ml
View file @
bfd52e95
...
...
@@ -12,14 +12,14 @@ type env = { fs : (vsymbol list * term) Mls.t;
let
empty_env
=
{
fs
=
Mls
.
empty
;
ps
=
Mls
.
empty
}
open
Format
(*
let print_env fmt env =
let print_map iter pterm pfs = Pp.print_iter2 iter Pp.newline Pp.comma pfs
(Pp.print_pair (Pp.print_list Pp.comma Pretty.print_vsymbol) pterm) in
fprintf fmt "fs:@[<hov>%a@]@\nps:@[<hov>%a@]@\n"
(print_map Mls.iter Pretty.print_term Pretty.print_lsymbol) env.fs
(print_map Mls.iter Pretty.print_fmla Pretty.print_lsymbol) env.ps
*)
let
rec
replacet
env
t
=
let
t
=
substt
env
t
in
match
t
.
t_node
with
...
...
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