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
125
Issues
125
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
4766128c
Commit
4766128c
authored
Apr 28, 2010
by
Andrei Paskevich
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
shyly hide the physical equality from the eyes of the users (in core/)
parent
7f8fecf3
Changes
13
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
13 changed files
with
218 additions
and
173 deletions
+218
-173
src/core/decl.ml
src/core/decl.ml
+18
-12
src/core/decl.mli
src/core/decl.mli
+2
-0
src/core/ident.ml
src/core/ident.ml
+3
-2
src/core/ident.mli
src/core/ident.mli
+3
-1
src/core/pretty.ml
src/core/pretty.ml
+1
-1
src/core/task.ml
src/core/task.ml
+11
-13
src/core/task.mli
src/core/task.mli
+1
-0
src/core/term.ml
src/core/term.ml
+142
-129
src/core/term.mli
src/core/term.mli
+17
-7
src/core/theory.ml
src/core/theory.ml
+1
-1
src/core/ty.ml
src/core/ty.ml
+13
-6
src/core/ty.mli
src/core/ty.mli
+5
-0
src/transform/eliminate_algebraic.ml
src/transform/eliminate_algebraic.ml
+1
-1
No files found.
src/core/decl.ml
View file @
4766128c
...
...
@@ -85,6 +85,8 @@ module Spr = Prop.S
module
Mpr
=
Prop
.
M
module
Hpr
=
Prop
.
H
let
pr_equal
=
(
==
)
let
create_prsymbol
n
=
{
pr_name
=
id_register
n
}
type
prop
=
prsymbol
*
fmla
...
...
@@ -119,26 +121,28 @@ module Hsdecl = Hashcons.Make (struct
type
t
=
decl
let
eq_td
(
ts1
,
td1
)
(
ts2
,
td2
)
=
ts
1
==
ts2
&&
match
td1
,
td2
with
let
eq_td
(
ts1
,
td1
)
(
ts2
,
td2
)
=
ts
_equal
ts1
ts2
&&
match
td1
,
td2
with
|
Tabstract
,
Tabstract
->
true
|
Talgebraic
l1
,
Talgebraic
l2
->
list_all2
(
==
)
l1
l2
|
Talgebraic
l1
,
Talgebraic
l2
->
list_all2
ls_equal
l1
l2
|
_
->
false
let
eq_ld
(
ls1
,
ld1
)
(
ls2
,
ld2
)
=
ls
1
==
ls2
&&
match
ld1
,
ld2
with
|
Some
(
_
,
f1
)
,
Some
(
_
,
f2
)
->
f
1
==
f2
let
eq_ld
(
ls1
,
ld1
)
(
ls2
,
ld2
)
=
ls
_equal
ls1
ls2
&&
match
ld1
,
ld2
with
|
Some
(
_
,
f1
)
,
Some
(
_
,
f2
)
->
f
_equal
f1
f2
|
None
,
None
->
true
|
_
->
false
let
eq_iax
(
pr1
,
fr1
)
(
pr2
,
fr2
)
=
pr1
==
pr2
&&
fr1
==
fr2
let
eq_iax
(
pr1
,
fr1
)
(
pr2
,
fr2
)
=
pr_equal
pr1
pr2
&&
f_equal
fr1
fr2
let
eq_ind
(
ps1
,
al1
)
(
ps2
,
al2
)
=
ps1
==
ps2
&&
list_all2
eq_iax
al1
al2
let
eq_ind
(
ps1
,
al1
)
(
ps2
,
al2
)
=
ls_equal
ps1
ps2
&&
list_all2
eq_iax
al1
al2
let
equal
d1
d2
=
match
d1
.
d_node
,
d2
.
d_node
with
|
Dtype
l1
,
Dtype
l2
->
list_all2
eq_td
l1
l2
|
Dlogic
l1
,
Dlogic
l2
->
list_all2
eq_ld
l1
l2
|
Dind
l1
,
Dind
l2
->
list_all2
eq_ind
l1
l2
|
Dprop
(
k1
,
pr1
,
f1
)
,
Dprop
(
k2
,
pr2
,
f2
)
->
k1
=
=
k2
&&
pr1
==
pr2
&&
f1
==
f2
k1
=
k2
&&
pr_equal
pr1
pr2
&&
f_equal
f1
f2
|
_
,_
->
false
let
hs_td
(
ts
,
td
)
=
match
td
with
...
...
@@ -178,6 +182,8 @@ module Sdecl = Decl.S
module
Mdecl
=
Decl
.
M
module
Hdecl
=
Decl
.
H
let
d_equal
=
(
==
)
(** Declaration constructors *)
let
mk_decl
n
=
{
d_node
=
n
;
d_tag
=
-
1
}
...
...
@@ -217,7 +223,7 @@ let create_ty_decl tdl =
let
check_decl
acc
(
ts
,
td
)
=
match
td
with
|
Tabstract
->
add_id
acc
ts
.
ts_name
|
Talgebraic
cl
->
if
ts
.
ts_def
!=
None
then
raise
(
IllegalTypeAlias
ts
);
if
ts
.
ts_def
<>
None
then
raise
(
IllegalTypeAlias
ts
);
let
ty
=
ty_app
ts
(
List
.
map
ty_var
ts
.
ts_args
)
in
List
.
fold_left
(
check_constr
ty
)
(
add_id
acc
ts
.
ts_name
)
cl
in
...
...
@@ -227,7 +233,7 @@ let create_ty_decl tdl =
let
create_logic_decl
ldl
=
if
ldl
=
[]
then
raise
EmptyDecl
;
let
check_decl
acc
(
ls
,
ld
)
=
match
ld
with
|
Some
(
s
,_
)
when
s
!=
ls
->
raise
(
BadLogicDecl
ls
.
ls_name
)
|
Some
(
s
,_
)
when
not
(
ls_equal
s
ls
)
->
raise
(
BadLogicDecl
ls
.
ls_name
)
|
_
->
add_id
acc
ls
.
ls_name
in
ignore
(
List
.
fold_left
check_decl
Sid
.
empty
ldl
);
...
...
@@ -267,7 +273,7 @@ let create_ind_decl idl =
in
let
cls
,
f
=
clause
[]
(
check_fvs
f
)
in
match
f
.
f_node
with
|
Fapp
(
s
,
tl
)
when
s
==
ps
->
|
Fapp
(
s
,
tl
)
when
ls_equal
s
ps
->
let
mtch
sb
t
ty
=
try
ty_match
sb
(
t
.
t_ty
)
ty
with
TypeMismatch
->
raise
(
TooSpecificIndDecl
(
ps
,
pr
,
t
))
...
...
@@ -420,7 +426,7 @@ let known_fmla kn f = f_s_fold (known_ts kn) (known_ls kn) () f
let
merge_known
kn1
kn2
=
let
add_known
id
decl
kn
=
try
if
Mid
.
find
id
kn2
!=
decl
then
raise
(
RedeclaredIdent
id
);
if
not
(
d_equal
(
Mid
.
find
id
kn2
)
decl
)
then
raise
(
RedeclaredIdent
id
);
kn
with
Not_found
->
Mid
.
add
id
decl
kn
in
...
...
@@ -428,7 +434,7 @@ let merge_known kn1 kn2 =
let
add_known
id
decl
kn
=
try
if
Mid
.
find
id
kn
!=
decl
then
raise
(
RedeclaredIdent
id
);
if
not
(
d_equal
(
Mid
.
find
id
kn
)
decl
)
then
raise
(
RedeclaredIdent
id
);
raise
(
KnownIdent
id
)
with
Not_found
->
Mid
.
add
id
decl
kn
...
...
src/core/decl.mli
View file @
4766128c
...
...
@@ -87,6 +87,8 @@ module Sdecl : Set.S with type elt = decl
module
Mdecl
:
Map
.
S
with
type
key
=
decl
module
Hdecl
:
Hashtbl
.
S
with
type
key
=
decl
val
d_equal
:
decl
->
decl
->
bool
(** Declaration constructors *)
val
create_ty_decl
:
ty_decl
list
->
decl
...
...
src/core/ident.ml
View file @
4766128c
...
...
@@ -33,7 +33,6 @@ and origin =
|
Derived
of
ident
|
Fresh
module
Id
=
StructMake
(
struct
type
t
=
ident
let
tag
id
=
id
.
id_tag
...
...
@@ -45,6 +44,8 @@ module Hid = Id.H
type
preid
=
ident
let
id_equal
=
(
==
)
(* constructors *)
let
gentag
=
let
r
=
ref
0
in
fun
()
->
incr
r
;
!
r
...
...
@@ -70,7 +71,7 @@ let id_derive_long sh ln id = create_ident sh ln (Derived id)
let
id_clone
id
=
create_ident
id
.
id_short
id
.
id_long
(
Derived
id
)
let
id_dup
id
=
{
id
with
id_tag
=
-
1
}
let
rec
id_derived_from
i1
i2
=
i
1
==
i2
||
let
rec
id_derived_from
i1
i2
=
i
d_equal
i1
i2
||
(
match
i1
.
id_origin
with
|
Derived
i3
->
id_derived_from
i3
i2
|
_
->
false
)
...
...
src/core/ident.mli
View file @
4766128c
...
...
@@ -35,6 +35,8 @@ module Sid : Set.S with type elt = ident
module
Mid
:
Map
.
S
with
type
key
=
ident
module
Hid
:
Hashtbl
.
S
with
type
key
=
ident
val
id_equal
:
ident
->
ident
->
bool
(* a user-created type of unregistered identifiers *)
type
preid
...
...
@@ -75,7 +77,7 @@ val create_ident_printer :
val
id_unique
:
ident_printer
->
?
sanitizer
:
(
string
->
string
)
->
ident
->
string
(** use ident_printer to generate a unique name for ident
(** use ident_printer to generate a unique name for ident
an optional sanitizer is applied over the printer's sanitizer *)
val
string_unique
:
ident_printer
->
string
->
string
...
...
src/core/pretty.ml
View file @
4766128c
...
...
@@ -117,7 +117,7 @@ let print_const fmt = function
(* can the type of a value be derived from the type of the arguments? *)
let
unambig_fs
fs
=
let
rec
lookup
v
ty
=
match
ty
.
ty_node
with
|
Tyvar
u
when
u
==
v
->
true
|
Tyvar
u
when
tv_equal
u
v
->
true
|
_
->
ty_any
(
lookup
v
)
ty
in
let
lookup
v
=
List
.
exists
(
lookup
v
)
fs
.
ls_args
in
...
...
src/core/task.ml
View file @
4766128c
...
...
@@ -46,30 +46,28 @@ let task_known = option_apply Mid.empty (fun t -> t.task_known)
let
task_clone
=
option_apply
Mid
.
empty
(
fun
t
->
t
.
task_clone
)
let
task_used
=
option_apply
Mid
.
empty
(
fun
t
->
t
.
task_used
)
let
task_hd_equal
=
(
==
)
let
task_equal
t1
t2
=
match
t1
,
t2
with
|
Some
t1
,
Some
t2
->
t1
==
t2
|
Some
_
,
None
->
false
|
None
,
Some
_
->
false
|
Some
t1
,
Some
t2
->
task_hd_equal
t1
t2
|
None
,
None
->
true
|
_
->
false
module
Task
=
struct
type
t
=
task_hd
let
equal_pair
(
il1
,
ir1
)
(
il2
,
ir2
)
=
il1
==
il2
&&
ir1
==
ir2
let
equal_pair
(
il1
,
ir1
)
(
il2
,
ir2
)
=
id_equal
il1
il2
&&
id_equal
ir1
ir2
let
equal_tdecl
td1
td2
=
match
td1
,
td2
with
|
Decl
d1
,
Decl
d2
->
d
1
==
d2
|
Use
th1
,
Use
th2
->
th1
.
th_name
==
th2
.
th_name
|
Decl
d1
,
Decl
d2
->
d
_equal
d1
d2
|
Use
th1
,
Use
th2
->
id_equal
th1
.
th_name
th2
.
th_name
|
Clone
(
th1
,
sl1
)
,
Clone
(
th2
,
sl2
)
->
th1
.
th_name
==
th2
.
th_name
&&
list_all2
equal_pair
sl1
sl2
id_equal
th1
.
th_name
th2
.
th_name
&&
list_all2
equal_pair
sl1
sl2
|
_
,_
->
false
let
equal
a
b
=
equal_tdecl
a
.
task_decl
b
.
task_decl
&&
match
a
.
task_prev
,
b
.
task_prev
with
|
Some
na
,
Some
nb
->
na
==
nb
|
None
,
None
->
true
|
_
->
false
let
equal
a
b
=
equal_tdecl
a
.
task_decl
b
.
task_decl
&&
task_equal
a
.
task_prev
b
.
task_prev
let
hash_pair
(
il
,
ir
)
=
Hashcons
.
combine
il
.
id_tag
ir
.
id_tag
...
...
src/core/task.mli
View file @
4766128c
...
...
@@ -42,6 +42,7 @@ and tdecl = private
|
Clone
of
theory
*
(
ident
*
ident
)
list
val
task_equal
:
task
->
task
->
bool
val
task_hd_equal
:
task_hd
->
task_hd
->
bool
val
task_known
:
task
->
known_map
val
task_clone
:
task
->
clone_map
...
...
src/core/term.ml
View file @
4766128c
This diff is collapsed.
Click to expand it.
src/core/term.mli
View file @
4766128c
...
...
@@ -31,6 +31,8 @@ module Svs : Set.S with type elt = vsymbol
module
Mvs
:
Map
.
S
with
type
key
=
vsymbol
module
Hvs
:
Hashtbl
.
S
with
type
key
=
vsymbol
val
vs_equal
:
vsymbol
->
vsymbol
->
bool
val
create_vsymbol
:
preid
->
ty
->
vsymbol
(** Function and predicate symbols *)
...
...
@@ -41,14 +43,16 @@ type lsymbol = private {
ls_value
:
ty
option
;
}
val
create_lsymbol
:
preid
->
ty
list
->
ty
option
->
lsymbol
val
create_fsymbol
:
preid
->
ty
list
->
ty
->
lsymbol
val
create_psymbol
:
preid
->
ty
list
->
lsymbol
module
Sls
:
Set
.
S
with
type
elt
=
lsymbol
module
Mls
:
Map
.
S
with
type
key
=
lsymbol
module
Hls
:
Hashtbl
.
S
with
type
key
=
lsymbol
val
ls_equal
:
lsymbol
->
lsymbol
->
bool
val
create_lsymbol
:
preid
->
ty
list
->
ty
option
->
lsymbol
val
create_fsymbol
:
preid
->
ty
list
->
ty
->
lsymbol
val
create_psymbol
:
preid
->
ty
list
->
lsymbol
(** Exceptions *)
exception
BadArity
of
int
*
int
...
...
@@ -70,6 +74,8 @@ and pattern_node = private
|
Papp
of
lsymbol
*
pattern
list
|
Pas
of
pattern
*
vsymbol
val
pat_equal
:
pattern
->
pattern
->
bool
(* smart constructors for patterns *)
val
pat_wild
:
ty
->
pattern
...
...
@@ -163,6 +169,13 @@ module Sterm : Set.S with type elt = term
module
Mfmla
:
Map
.
S
with
type
key
=
fmla
module
Sfmla
:
Set
.
S
with
type
elt
=
fmla
val
t_equal
:
term
->
term
->
bool
val
f_equal
:
fmla
->
fmla
->
bool
val
e_equal
:
expr
->
expr
->
bool
val
tr_equal
:
trigger
->
trigger
->
bool
val
trl_equal
:
trigger
list
->
trigger
list
->
bool
(* smart constructors for term *)
val
t_var
:
vsymbol
->
term
...
...
@@ -238,7 +251,6 @@ val f_open_exists : fmla -> vsymbol list * fmla
val
e_map
:
(
term
->
term
)
->
(
fmla
->
fmla
)
->
expr
->
expr
val
e_fold
:
(
'
a
->
term
->
'
a
)
->
(
'
a
->
fmla
->
'
a
)
->
'
a
->
expr
->
'
a
val
e_apply
:
(
term
->
'
a
)
->
(
fmla
->
'
a
)
->
expr
->
'
a
val
e_equal
:
expr
->
expr
->
bool
val
tr_map
:
(
term
->
term
)
->
(
fmla
->
fmla
)
->
trigger
list
->
trigger
list
...
...
@@ -246,8 +258,6 @@ val tr_map : (term -> term) ->
val
tr_fold
:
(
'
a
->
term
->
'
a
)
->
(
'
a
->
fmla
->
'
a
)
->
'
a
->
trigger
list
->
'
a
val
tr_equal
:
trigger
list
->
trigger
list
->
bool
(* map/fold over symbols *)
val
t_s_map
:
(
tysymbol
->
tysymbol
)
->
(
lsymbol
->
lsymbol
)
->
term
->
term
...
...
src/core/theory.ml
View file @
4766128c
...
...
@@ -420,7 +420,7 @@ let cl_add_type cl inst_ts acc (ts, def) =
let
extract_ls_defn
f
=
let
vl
,
ef
=
f_open_forall
f
in
match
ef
.
f_node
with
|
Fapp
(
s
,
[
t1
;
t2
])
when
s
==
ps_equ
->
|
Fapp
(
s
,
[
t1
;
t2
])
when
ls_equal
s
ps_equ
->
begin
match
t1
.
t_node
with
|
Tapp
(
fs
,
_
)
->
make_fs_defn
fs
vl
t2
|
_
->
assert
false
...
...
src/core/ty.ml
View file @
4766128c
...
...
@@ -35,6 +35,8 @@ module Stv = Tvar.S
module
Mtv
=
Tvar
.
M
module
Htv
=
Tvar
.
H
let
tv_equal
=
(
==
)
let
create_tvsymbol
n
=
{
tv_name
=
id_register
n
}
(* type symbols and types *)
...
...
@@ -64,6 +66,9 @@ module Mts = Tsym.M
module
Hts
=
Tsym
.
H
module
Wts
=
Tsym
.
W
let
ts_equal
=
(
==
)
let
ty_equal
=
(
==
)
let
mk_ts
name
args
def
=
{
ts_name
=
name
;
ts_args
=
args
;
...
...
@@ -76,8 +81,9 @@ module Hsty = Hashcons.Make (struct
type
t
=
ty
let
equal
ty1
ty2
=
match
ty1
.
ty_node
,
ty2
.
ty_node
with
|
Tyvar
n1
,
Tyvar
n2
->
n1
==
n2
|
Tyapp
(
s1
,
l1
)
,
Tyapp
(
s2
,
l2
)
->
s1
==
s2
&&
List
.
for_all2
(
==
)
l1
l2
|
Tyvar
n1
,
Tyvar
n2
->
tv_equal
n1
n2
|
Tyapp
(
s1
,
l1
)
,
Tyapp
(
s2
,
l2
)
->
ts_equal
s1
s2
&&
List
.
for_all2
ty_equal
l1
l2
|
_
->
false
let
hash_ty
ty
=
ty
.
ty_tag
...
...
@@ -150,7 +156,7 @@ let rec tv_inst m ty = match ty.ty_node with
let
ty_app
s
tl
=
let
tll
=
List
.
length
tl
in
let
stl
=
List
.
length
s
.
ts_args
in
if
tll
!=
stl
then
raise
(
BadTypeArity
(
stl
,
tll
));
if
tll
<>
stl
then
raise
(
BadTypeArity
(
stl
,
tll
));
match
s
.
ts_def
with
|
Some
ty
->
let
add
m
v
t
=
Mtv
.
add
v
t
m
in
...
...
@@ -179,12 +185,13 @@ let ty_s_any pr ty =
exception
TypeMismatch
let
rec
ty_match
s
ty1
ty2
=
if
ty
1
==
ty2
then
s
if
ty
_equal
ty1
ty2
then
s
else
match
ty1
.
ty_node
,
ty2
.
ty_node
with
|
Tyvar
n1
,
_
->
(
try
if
Mtv
.
find
n1
s
==
ty2
then
s
else
raise
TypeMismatch
(
try
if
ty_equal
(
Mtv
.
find
n1
s
)
ty2
then
s
else
raise
TypeMismatch
with
Not_found
->
Mtv
.
add
n1
ty2
s
)
|
Tyapp
(
f1
,
l1
)
,
Tyapp
(
f2
,
l2
)
when
f1
==
f2
->
|
Tyapp
(
f1
,
l1
)
,
Tyapp
(
f2
,
l2
)
when
ts_equal
f1
f2
->
List
.
fold_left2
ty_match
s
l1
l2
|
_
->
raise
TypeMismatch
...
...
src/core/ty.mli
View file @
4766128c
...
...
@@ -29,6 +29,8 @@ module Stv : Set.S with type elt = tvsymbol
module
Mtv
:
Map
.
S
with
type
key
=
tvsymbol
module
Htv
:
Hashtbl
.
S
with
type
key
=
tvsymbol
val
tv_equal
:
tvsymbol
->
tvsymbol
->
bool
val
create_tvsymbol
:
preid
->
tvsymbol
(* type symbols and types *)
...
...
@@ -58,6 +60,9 @@ module Mty : Map.S with type key = ty
module
Hty
:
Hashtbl
.
S
with
type
key
=
ty
module
Wty
:
Hashweak
.
S
with
type
key
=
ty
val
ts_equal
:
tysymbol
->
tysymbol
->
bool
val
ty_equal
:
ty
->
ty
->
bool
exception
BadTypeArity
of
int
*
int
exception
DuplicateTypeVar
of
tvsymbol
exception
UnboundTypeVars
of
Stv
.
t
...
...
src/transform/eliminate_algebraic.ml
View file @
4766128c
...
...
@@ -144,7 +144,7 @@ and rewriteF kn state av sign f = match f.f_node with
(
rewriteF
kn
state
Svs
.
empty
sign
)
tr
in
let
av
=
List
.
fold_left
(
fun
s
v
->
Svs
.
add
v
s
)
av
vl
in
let
f1'
=
rewriteF
kn
state
av
sign
f1
in
if
f1'
==
f1
&&
tr_equal
tr'
tr
then
f
else
f_quant
q
vl
tr'
f1'
if
f1'
==
f1
&&
tr
l
_equal
tr'
tr
then
f
else
f_quant
q
vl
tr'
f1'
|
Fbinop
(
o
,
_
,
_
)
when
(
o
=
Fand
&&
sign
)
||
(
o
=
For
&&
not
sign
)
->
f_map_sign
(
rewriteT
kn
state
)
(
rewriteF
kn
state
av
)
sign
f
|
Flet
(
t1
,
_
)
->
...
...
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