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
126
Issues
126
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
937c08a1
Commit
937c08a1
authored
Apr 26, 2010
by
Andrei Paskevich
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
a bit of renaming (Declaration -> Decl, Expression -> Expr, etc)
parent
e12dddfd
Changes
7
Hide whitespace changes
Inline
Side-by-side
Showing
7 changed files
with
85 additions
and
79 deletions
+85
-79
src/driver/register.ml
src/driver/register.ml
+24
-22
src/driver/register.mli
src/driver/register.mli
+32
-28
src/printer/alt_ergo.ml
src/printer/alt_ergo.ml
+8
-8
src/printer/smt.ml
src/printer/smt.ml
+6
-6
src/transform/eliminate_algebraic.ml
src/transform/eliminate_algebraic.ml
+8
-8
src/transform/eliminate_if.ml
src/transform/eliminate_if.ml
+2
-2
src/transform/encoding_decorate.ml
src/transform/encoding_decorate.ml
+5
-5
No files found.
src/driver/register.ml
View file @
937c08a1
...
...
@@ -164,41 +164,39 @@ let list_printers () = Hashtbl.fold (fun k _ acc -> k::acc) printers []
let
list_transforms
()
=
Hashtbl
.
fold
(
fun
k
_
acc
->
k
::
acc
)
transforms
[]
let
list_transforms_l
()
=
Hashtbl
.
fold
(
fun
k
_
acc
->
k
::
acc
)
transforms_l
[]
(** exception to use in a printer and transformation *)
open
Ty
open
Term
open
Decl
open
Ty
type
error
=
|
UnsupportedType
of
ty
*
string
|
UnsupportedExpr
ession
of
expr
*
string
|
UnsupportedDecl
aration
of
decl
*
string
|
NotImplemented
of
string
|
UnsupportedType
of
ty
*
string
|
UnsupportedExpr
of
expr
*
string
|
UnsupportedDecl
of
decl
*
string
|
NotImplemented
of
string
exception
Error
of
error
let
error
e
=
raise
(
Error
e
)
let
unsupportedType
e
s
=
error
(
UnsupportedType
(
e
,
s
))
let
unsupportedExpression
e
s
=
error
(
UnsupportedExpression
(
e
,
s
))
let
unsupportedDeclaration
e
s
=
error
(
UnsupportedDeclaration
(
e
,
s
))
let
notImplemented
s
=
error
(
NotImplemented
s
)
let
unsupportedTerm
e
s
=
error
(
UnsupportedExpr
(
Term
e
,
s
))
let
unsupportedFmla
e
s
=
error
(
UnsupportedExpr
(
Fmla
e
,
s
))
let
unsupportedExpr
e
s
=
error
(
UnsupportedExpr
(
e
,
s
))
let
unsupportedDecl
e
s
=
error
(
UnsupportedDecl
(
e
,
s
))
let
notImplemented
s
=
error
(
NotImplemented
s
)
let
report
fmt
=
function
|
UnsupportedType
(
e
,
s
)
->
let
msg
=
"This type isn't supported"
in
Format
.
fprintf
fmt
"@[<hov 3> %s:@
\n
%a@
\n
%s@]@
\n
"
msg
Pretty
.
print_ty
e
s
|
UnsupportedExpr
ession
(
e
,
s
)
->
|
UnsupportedExpr
(
e
,
s
)
->
let
msg
=
"This expression isn't supported"
in
Format
.
fprintf
fmt
"@[<hov 3> %s:@
\n
%a@
\n
%s@]@
\n
"
msg
Pretty
.
print_expr
e
s
|
UnsupportedDecl
aration
(
d
,
s
)
->
|
UnsupportedDecl
(
d
,
s
)
->
let
msg
=
"This declaration isn't supproted"
in
Format
.
fprintf
fmt
"@[<hov 3> %s:@
\n
%a@
\n
%s@]@
\n
"
msg
Pretty
.
print_decl
d
s
...
...
@@ -210,14 +208,18 @@ exception Unsupported of string
let
unsupported
s
=
raise
(
Unsupported
s
)
let
catch_unsupportedtype
f
ty
=
try
f
ty
with
Unsupported
s
->
unsupportedType
ty
s
let
catch_unsupportedType
f
e
=
try
f
e
with
Unsupported
s
->
unsupportedType
e
s
let
catch_unsupportedTerm
f
e
=
try
f
e
with
Unsupported
s
->
unsupportedTerm
e
s
let
catch_unsupportedFmla
f
e
=
try
f
e
with
Unsupported
s
->
unsupportedFmla
e
s
let
catch_unsupported
term
f
t
=
try
f
t
with
Unsupported
s
->
unsupportedExpression
(
Term
t
)
s
let
catch_unsupported
Expr
f
e
=
try
f
e
with
Unsupported
s
->
unsupportedExpr
e
s
let
catch_unsupported
fmla
f
t
=
try
f
t
with
Unsupported
s
->
unsupportedExpression
(
Fmla
t
)
s
let
catch_unsupported
Decl
f
e
=
try
f
e
with
Unsupported
s
->
unsupportedDecl
e
s
let
catch_unsupportedDeclaration
f
d
=
try
f
d
with
Unsupported
s
->
unsupportedDeclaration
d
s
src/driver/register.mli
View file @
937c08a1
...
...
@@ -82,25 +82,25 @@ val list_transforms_l : unit -> string list
(** {2 exceptions to use in transformations and printers } *)
type
error
=
|
UnsupportedType
of
Ty
.
ty
*
string
|
UnsupportedExpr
ession
of
Term
.
expr
*
string
|
UnsupportedDecl
aration
of
Decl
.
decl
*
string
|
NotImplemented
of
string
|
UnsupportedType
of
Ty
.
ty
*
string
|
UnsupportedExpr
of
Term
.
expr
*
string
|
UnsupportedDecl
of
Decl
.
decl
*
string
|
NotImplemented
of
string
exception
Error
of
error
val
unsupportedType
:
Ty
.
ty
->
string
->
'
a
(** [unsupportedType ty s]
- [ty] is the problematic
formula
val
unsupportedType
:
Ty
.
ty
->
string
->
'
a
(** [unsupportedType ty s]
- [ty] is the problematic
type
- [s] explain the problem and
possibly a way to solve it (such as applying another
transforamtion) *)
val
unsupported
Expression
:
Term
.
expr
->
string
->
'
a
val
unsupported
Declaration
:
Decl
.
decl
->
string
->
'
a
val
notImplemented
:
string
->
'
a
val
unsupported
Term
:
Term
.
term
->
string
->
'
a
val
unsupportedFmla
:
Term
.
fmla
->
string
->
'
a
val
unsupported
Expr
:
Term
.
expr
->
string
->
'
a
val
unsupportedDecl
:
Decl
.
decl
->
string
->
'
a
val
notImplemented
:
string
->
'
a
(** [notImplemented s]. [s] explains what is not implemented *)
val
report
:
Format
.
formatter
->
error
->
unit
...
...
@@ -109,27 +109,31 @@ val report : Format.formatter -> error -> unit
(** {3 functions which catch inner error} *)
exception
Unsupported
of
string
(** This exception must be raised only in
a inside call of one of the above
catch_* function
*)
(** This exception must be raised only in
side a call
of one of the catch_* functions below
*)
val
unsupported
:
string
->
'
a
(** convenient function to raise the {! Unsupported} exception *)
val
catch_unsupportedtype
:
(
Ty
.
ty
->
'
a
)
->
(
Ty
.
ty
->
'
a
)
(** [catch_unsupportedtype f] return a function which applied on [arg] :
- return [f arg] if [f arg] doesn't raise the {!
Unsupported} exception.
- raise [Error (unsupportedType (arg,s))] if [f arg]
val
catch_unsupportedType
:
(
Ty
.
ty
->
'
a
)
->
(
Ty
.
ty
->
'
a
)
(** [catch_unsupportedType f] return a function which applied on [arg]:
- return [f arg] if [f arg] does not raise {!Unsupported} exception
- raise [Error (unsupportedType (arg,s))] if [f arg]
raises [Unsupported s]*)
val
catch_unsupportedterm
:
(
Term
.
term
->
'
a
)
->
(
Term
.
term
->
'
a
)
(** same as {! catch_unsupportedtype} but use [UnsupportedExpression]
instead of [UnsupportedType]*)
val
catch_unsupportedTerm
:
(
Term
.
term
->
'
a
)
->
(
Term
.
term
->
'
a
)
(** same as {! catch_unsupportedType} but use [UnsupportedExpr]
instead of [UnsupportedType]*)
val
catch_unsupportedFmla
:
(
Term
.
fmla
->
'
a
)
->
(
Term
.
fmla
->
'
a
)
(** same as {! catch_unsupportedType} but use [UnsupportedExpr]
instead of [UnsupportedType]*)
val
catch_unsupportedExpr
:
(
Term
.
expr
->
'
a
)
->
(
Term
.
expr
->
'
a
)
(** same as {! catch_unsupportedType} but use [UnsupportedExpr]
instead of [UnsupportedType]*)
val
catch_unsupported
fmla
:
(
Term
.
fmla
->
'
a
)
->
(
Term
.
fmla
->
'
a
)
(** same as {! catch_unsupportedtype} but use [UnsupportedExpression]
instead of [UnsupportedType]
*)
val
catch_unsupported
Decl
:
(
Decl
.
decl
->
'
a
)
->
(
Decl
.
decl
->
'
a
)
(** same as {! catch_unsupportedType} but use [UnsupportedDecl]
instead of [UnsupportedType]
*)
val
catch_unsupportedDeclaration
:
(
Decl
.
decl
->
'
a
)
->
(
Decl
.
decl
->
'
a
)
(** same as {! catch_unsupportedtype} but use
[UnsupportedDeclaration] instead of [UnsupportedType] *)
src/printer/alt_ergo.ml
View file @
937c08a1
...
...
@@ -70,13 +70,13 @@ let rec print_term drv fmt t = match t.t_node with
|
Some
s
->
Driver
.
syntax_arguments
s
(
print_term
drv
)
fmt
tl
|
None
->
fprintf
fmt
"%a%a"
print_ident
ls
.
ls_name
(
print_tapp
drv
)
tl
end
|
Tlet
_
->
unsupported
Expression
(
Term
t
)
|
Tlet
_
->
unsupported
Term
t
"alt-ergo : you must eliminate let in term"
|
Tif
_
->
unsupported
Expression
(
Term
t
)
|
Tif
_
->
unsupported
Term
t
"alt-ergo : you must eliminate if_then_else"
|
Tcase
_
->
unsupported
Expression
(
Term
t
)
|
Tcase
_
->
unsupported
Term
t
"alt-ergo : you must eliminate match"
|
Teps
_
->
unsupported
Expression
(
Term
t
)
|
Teps
_
->
unsupported
Term
t
"alt-ergo : you must eliminate epsilon"
and
print_tapp
drv
fmt
=
function
...
...
@@ -118,9 +118,9 @@ let rec print_fmla drv fmt f = match f.f_node with
fprintf
fmt
"((%a and %a) or (not %a and %a))"
(
print_fmla
drv
)
f1
(
print_fmla
drv
)
f2
(
print_fmla
drv
)
f1
(
print_fmla
drv
)
f3
|
Flet
_
->
unsupported
Expression
(
Fmla
f
)
|
Flet
_
->
unsupported
Fmla
f
"alt-ergo : you must eliminate let in formula"
|
Fcase
_
->
unsupported
Expression
(
Fmla
f
)
|
Fcase
_
->
unsupported
Fmla
f
"alt-ergo : you must eliminate match"
...
...
@@ -186,7 +186,7 @@ let print_decl drv fmt d = match d.d_node with
print_list_opt
newline
(
print_type_decl
drv
)
fmt
dl
|
Dlogic
dl
->
print_list_opt
newline
(
print_logic_decl
drv
)
fmt
dl
|
Dind
_
->
unsupportedDecl
aration
d
|
Dind
_
->
unsupportedDecl
d
"alt-ergo : inductive definition are not supported"
|
Dprop
(
Paxiom
,
pr
,
_
)
when
Driver
.
query_remove
drv
pr
.
pr_name
->
false
|
Dprop
(
Paxiom
,
pr
,
f
)
->
...
...
@@ -198,7 +198,7 @@ let print_decl drv fmt d = match d.d_node with
|
Dprop
(
Plemma
,
_
,
_
)
->
assert
false
let
print_decl
drv
fmt
=
catch_unsupportedDecl
aration
(
print_decl
drv
fmt
)
let
print_decl
drv
fmt
=
catch_unsupportedDecl
(
print_decl
drv
fmt
)
let
print_task
drv
fmt
task
=
Driver
.
print_full_prelude
drv
task
fmt
;
...
...
src/printer/smt.ml
View file @
937c08a1
...
...
@@ -59,7 +59,7 @@ and print_tyapp drv fmt = function
|
[
ty
]
->
fprintf
fmt
"%a "
(
print_type
drv
)
ty
|
tl
->
fprintf
fmt
"(%a) "
(
print_list
comma
(
print_type
drv
))
tl
let
print_type
drv
fmt
=
catch_unsupported
t
ype
(
print_type
drv
fmt
)
let
print_type
drv
fmt
=
catch_unsupported
T
ype
(
print_type
drv
fmt
)
let
rec
print_term
drv
fmt
t
=
match
t
.
t_node
with
|
Tbvar
_
->
assert
false
...
...
@@ -81,9 +81,9 @@ let rec print_term drv fmt t = match t.t_node with
|
Tif
(
f1
,
t1
,
t2
)
->
fprintf
fmt
"@[(ite %a@ %a@ %a)@]"
(
print_fmla
drv
)
f1
(
print_term
drv
)
t1
(
print_term
drv
)
t2
|
Tcase
_
->
unsupported
Expression
(
Term
t
)
|
Tcase
_
->
unsupported
Term
t
"smtv1 : you must eliminate match"
|
Teps
_
->
unsupported
Expression
(
Term
t
)
|
Teps
_
->
unsupported
Term
t
"smtv1 : you must eliminate epsilon"
and
print_fmla
drv
fmt
f
=
match
f
.
f_node
with
...
...
@@ -131,7 +131,7 @@ and print_fmla drv fmt f = match f.f_node with
fprintf
fmt
"@[(let (%a %a)@ %a)@]"
print_var
v
(
print_term
drv
)
t1
(
print_fmla
drv
)
f2
;
forget_var
v
|
Fcase
_
->
unsupported
Expression
(
Fmla
f
)
|
Fcase
_
->
unsupported
Fmla
f
"smtv1 : you must eliminate match"
and
print_expr
drv
fmt
=
e_apply
(
print_term
drv
fmt
)
(
print_fmla
drv
fmt
)
...
...
@@ -173,7 +173,7 @@ let print_decl drv fmt d = match d.d_node with
print_list_opt
newline
(
print_type_decl
drv
)
fmt
dl
|
Dlogic
dl
->
print_list_opt
newline
(
print_logic_decl
drv
)
fmt
dl
|
Dind
_
->
unsupportedDecl
aration
d
|
Dind
_
->
unsupportedDecl
d
"smt : inductive definition are not supported"
|
Dprop
(
Paxiom
,
pr
,
_
)
when
Driver
.
query_remove
drv
pr
.
pr_name
->
false
|
Dprop
(
Paxiom
,
_pr
,
f
)
->
...
...
@@ -189,7 +189,7 @@ let print_decl drv fmt d = match d.d_node with
fprintf
fmt
" @[(not@ %a)@]"
(
print_fmla
drv
)
f
;
true
|
Dprop
(
Plemma
,
_
,
_
)
->
assert
false
let
print_decl
drv
fmt
=
catch_unsupportedDecl
aration
(
print_decl
drv
fmt
)
let
print_decl
drv
fmt
=
catch_unsupportedDecl
(
print_decl
drv
fmt
)
let
print_task
drv
fmt
task
=
fprintf
fmt
"(benchmark toto@
\n
"
...
...
src/transform/eliminate_algebraic.ml
View file @
937c08a1
...
...
@@ -46,24 +46,24 @@ let rec rewriteT kn state t = match t.t_node with
|
[{
pat_node
=
Papp
(
cs
,
pl
)
}]
->
let
add_var
e
p
pj
=
match
p
.
pat_node
with
|
Pvar
v
->
t_let
v
(
t_app
pj
[
t1
]
v
.
vs_ty
)
e
|
_
->
Register
.
unsupported
Expression
(
Term
t
)
uncompiled
|
_
->
Register
.
unsupported
Term
t
uncompiled
in
let
pjl
=
Mls
.
find
cs
state
.
pj_map
in
let
e
=
List
.
fold_left2
add_var
e
pl
pjl
in
w
,
Mls
.
add
cs
e
m
|
[{
pat_node
=
Pwild
}]
->
Some
e
,
m
|
_
->
Register
.
unsupported
Expression
(
Term
t
)
uncompiled
|
_
->
Register
.
unsupported
Term
t
uncompiled
in
let
w
,
m
=
List
.
fold_left
mk_br
(
None
,
Mls
.
empty
)
bl
in
let
find
cs
=
try
Mls
.
find
cs
m
with
Not_found
->
of_option
w
in
let
ts
=
match
t1
.
t_ty
.
ty_node
with
|
Tyapp
(
ts
,_
)
->
ts
|
_
->
Register
.
unsupported
Expression
(
Term
t
)
uncompiled
|
_
->
Register
.
unsupported
Term
t
uncompiled
in
let
tl
=
List
.
map
find
(
find_constructors
kn
ts
)
in
t_app
(
Mts
.
find
ts
state
.
mt_map
)
(
t1
::
tl
)
t
.
t_ty
|
Tcase
_
->
Register
.
unsupported
Expression
(
Term
t
)
uncompiled
|
Tcase
_
->
Register
.
unsupported
Term
t
uncompiled
|
_
->
t_map
(
rewriteT
kn
state
)
(
rewriteF
kn
state
Svs
.
empty
true
)
t
and
rewriteF
kn
state
av
sign
f
=
match
f
.
f_node
with
...
...
@@ -77,12 +77,12 @@ and rewriteF kn state av sign f = match f.f_node with
|
[{
pat_node
=
Papp
(
cs
,
pl
)
}]
->
let
get_var
p
=
match
p
.
pat_node
with
|
Pvar
v
->
v
|
_
->
Register
.
unsupported
Expression
(
Fmla
f
)
uncompiled
|
_
->
Register
.
unsupported
Fmla
f
uncompiled
in
w
,
Mls
.
add
cs
(
List
.
map
get_var
pl
,
e
)
m
|
[{
pat_node
=
Pwild
}]
->
Some
e
,
m
|
_
->
Register
.
unsupported
Expression
(
Fmla
f
)
uncompiled
|
_
->
Register
.
unsupported
Fmla
f
uncompiled
in
let
w
,
m
=
List
.
fold_left
mk_br
(
None
,
Mls
.
empty
)
bl
in
let
find
cs
=
...
...
@@ -105,11 +105,11 @@ and rewriteF kn state av sign f = match f.f_node with
in
let
ts
=
match
t1
.
t_ty
.
ty_node
with
|
Tyapp
(
ts
,_
)
->
ts
|
_
->
Register
.
unsupported
Expression
(
Fmla
f
)
uncompiled
|
_
->
Register
.
unsupported
Fmla
f
uncompiled
in
let
op
=
if
sign
then
f_and_simp
else
f_or_simp
in
map_join_left
find
op
(
find_constructors
kn
ts
)
|
Fcase
_
->
Register
.
unsupported
Expression
(
Fmla
f
)
uncompiled
|
Fcase
_
->
Register
.
unsupported
Fmla
f
uncompiled
|
Fquant
(
q
,
bf
)
when
(
q
=
Fforall
&&
sign
)
||
(
q
=
Fexists
&&
not
sign
)
->
let
vl
,
tr
,
f1
=
f_open_quant
bf
in
let
tr'
=
tr_map
(
rewriteT
kn
state
)
...
...
src/transform/eliminate_if.ml
View file @
937c08a1
...
...
@@ -38,7 +38,7 @@ let rec elim_t letl contT t = match t.t_node with
let
f
=
List
.
fold_left
(
fun
f
(
v
,
t
)
->
f_let
v
t
f
)
f
letl
in
f_if
f
(
elim_t
letl
contT
t1
)
(
elim_t
letl
contT
t2
)
|
Tcase
_
->
Register
.
unsupported
Expression
(
Term
t
)
Register
.
unsupported
Term
t
"cannot eliminate 'if-then-else' under 'match' in terms"
|
_
->
t_map_cont
(
elim_t
letl
)
elim_f
contT
t
...
...
@@ -51,7 +51,7 @@ and elim_f contF f = match f.f_node with
(* the only terms we can still meet are the terms in triggers *)
and
elim_tr
contT
t
=
match
t
.
t_node
with
|
Tif
_
->
Register
.
unsupported
Expression
(
Term
t
)
Register
.
unsupported
Term
t
"cannot eliminate 'if-then-else' in trigger terms"
|
_
->
t_map_cont
elim_tr
elim_f
contT
t
...
...
src/transform/encoding_decorate.ml
View file @
937c08a1
...
...
@@ -241,8 +241,8 @@ let rec rewrite_term tenv tvar vsvar t =
let
t1'
=
fnT
vsvar
t1
in
let
t2'
=
fnT
vsvar
t2
in
if
t1'
==
t1
&&
t2'
==
t2
then
t
else
t_let
u
t1'
t2'
|
Tcase
_
|
Teps
_
|
Tbvar
_
->
Register
.
unsupported
Expression
(
Term
t
)
"Encoding decorate : I can't encode this term"
Register
.
unsupported
Term
t
"Encoding decorate : I can't encode this term"
and
rewrite_fmla
tenv
tvar
vsvar
f
=
let
fnT
=
rewrite_term
tenv
tvar
vsvar
in
...
...
@@ -296,13 +296,13 @@ let decl (tenv:tenv) d =
Hts
.
add
tenv
.
trans_tsymbol
ts
tty
;
tty
in
[
create_decl
(
create_logic_decl
[(
tty
,
None
)])]
|
Dtype
_
->
Register
.
unsupportedDecl
aration
|
Dtype
_
->
Register
.
unsupportedDecl
d
"encoding_decorate : I can work only on abstract\
type which are not in recursive bloc."
|
Dlogic
l
->
let
fn
=
function
|
_ls
,
Some
_
->
Register
.
unsupportedDecl
aration
Register
.
unsupportedDecl
d
"encoding_decorate : I can't encode definition. \
Perhaps you could use eliminate_definition"
|
ls
,
None
->
...
...
@@ -314,7 +314,7 @@ Perhaps you could use eliminate_definition"
Hls
.
add
tenv
.
trans_lsymbol
ls
ls_conv
;
ls_conv
,
None
in
[
create_decl
(
create_logic_decl
(
List
.
map
fn
l
))]
|
Dind
_
->
Register
.
unsupportedDecl
aration
|
Dind
_
->
Register
.
unsupportedDecl
d
"encoding_decorate : I can't work on inductive"
(* let fn (pr,f) = pr, fnF f in *)
(* let fn (ps,l) = ps, List.map fn l in *)
...
...
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