Skip to content
GitLab
Menu
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
5f6e63a2
Commit
5f6e63a2
authored
May 17, 2011
by
Jean-Christophe Filliâtre
Browse files
programs: record construction {| x1=e1; ... xn=en |}
parent
92ead131
Changes
9
Hide whitespace changes
Inline
Side-by-side
examples/programs/vacid_0_sparse_array.mlw
View file @
5f6e63a2
...
...
@@ -82,95 +82,72 @@ back +-+-+-+-------------------+
forall
i
:
int
.
0
<=
i
<
a
.
card
->
a
.
idx
[
i
]
=
dirichlet
a
.
card
a
.
back
i
&&
is_elt
a
i
parameter
create
:
sz
:
int
->
{
0
<=
sz
<=
maxlen
}
sparse_array
{
invariant_
result
and
result
.
card
=
0
and
length
result
=
sz
and
forall
i
:
int
.
model
result
i
=
default
}
parameter
create
:
sz
:
int
->
{
0
<=
sz
<=
maxlen
}
sparse_array
{
invariant_
result
and
result
.
card
=
0
and
length
result
=
sz
and
forall
i
:
int
.
model
result
i
=
default
}
(*
parameter
malloc
:
n
:
int
->
{}
array
'a { A.length result = n }
(*
parameter
malloc
:
n
:
int
->
{}
array
'a { A.length result = n }
let create sz =
{ 0 <= sz <= maxlen }
Mk_sparse_array (malloc sz) (malloc sz) (malloc sz) 0
{ invariant_ result and
let create sz =
{ 0 <= sz <= maxlen }
Mk_sparse_array (malloc sz) (malloc sz) (malloc sz) 0
{ invariant_ result and
sa_sz result = sz and forall i:int. model result i = default }
*)
let test (a: sparse_array) i =
{ 0 <= i < length a and invariant_ a }
let idx = idx a in
let back = back a in
let n = card a in
0 <= idx[i] && idx[i] < n && back[idx[i]] = i
{ result=True <-> is_elt a i }
(***
(*
parameter get :
a:ref sparse_array -> i:int ->
{ 0 <= i < sa_sz !a }
elt reads a
{ result = model !a i }
*)
let get (a: sparse_array) i =
{ 0 <= i < length a and invariant_ a }
if test a i then
array_get (val a) i
else
default
{ result = model a i }
*)
(*
parameter set :
a:ref sparse_array -> i:int -> v:elt ->
{ 0 <= i < sa_sz !a and invariant !a }
unit writes a
{ invariant !a and
sa_sz !a = sa_sz (old !a) and
model !a i = v and
forall j:int. j <> i -> model !a j = model (old !a) j }
*)
let set (a : ref sparse_array) i v =
{ 0 <= i < sa_sz a and invariant_ a }
(* let SA val idx back sz n = !a in *)
let val = sa_val !a in
let idx = sa_idx !a in
let back = sa_back !a in
let sz= sa_sz !a in
let n = sa_n !a in
let val = array_set val i v in
if test a i then
a := SA val idx back sz n
else begin
assert { n < sz };
let idx = array_set idx i n in
let back = array_set back n i in
a := SA val idx back sz (n+1)
end
{ invariant_ a and
sa_sz a = sa_sz (old a) and
model a i = v and
forall j:int. j <> i -> model a j = model (old a) j }
let harness () =
let a = create 10 in
let b = create 20 in
let get_a_5 = get a 5 in assert { get_a_5 = default };
let get_b_7 = get b 7 in assert { get_b_7 = default };
set a 5 c1;
set b 7 c2;
let get_a_5 = get a 5 in assert { get_a_5 = c1 };
let get_b_7 = get b 7 in assert { get_b_7 = c2 };
let get_a_7 = get a 7 in assert { get_a_7 = default };
let get_b_5 = get b 5 in assert { get_b_5 = default };
let get_a_0 = get a 0 in assert { get_a_0 = default };
let get_b_0 = get b 0 in assert { get_b_0 = default };
()
***)
let test (a: sparse_array) i =
{ 0 <= i < length a and invariant_ a }
let idx = idx a in
let back = back a in
let n = card a in
0 <= idx[i] && idx[i] < n && back[idx[i]] = i
{ result=True <-> is_elt a i }
let get (a: sparse_array) i =
{ 0 <= i < length a and invariant_ a }
if test a i then
(val a)[i]
else
default
{ result = model a i }
let set (a: sparse_array) i v =
{ 0 <= i < length a and invariant_ a }
(* let SA val idx back sz n = !a in *)
let val = val a in
let idx = idx a in
let back = back a in
let n = card a in
set val i v;
if not (test a i) then begin
assert { n < length a };
set idx i n;
set back n i;
() (*TODO a.card <- n+1 *)
end
{ invariant_ a and
model a i = v and
forall j:int. j <> i -> model a j = model (old a) j }
let harness () =
let a = create 10 in
let b = create 20 in
let get_a_5 = get a 5 in assert { get_a_5 = default };
let get_b_7 = get b 7 in assert { get_b_7 = default };
set a 5 c1;
set b 7 c2;
let get_a_5 = get a 5 in assert { get_a_5 = c1 };
let get_b_7 = get b 7 in assert { get_b_7 = c2 };
let get_a_7 = get a 7 in assert { get_a_7 = default };
let get_b_5 = get b 5 in assert { get_b_5 = default };
let get_a_0 = get a 0 in assert { get_a_0 = default };
let get_b_0 = get b 0 in assert { get_b_0 = default };
()
end
...
...
examples/programs/vacid_0_union_find.mlw
View file @
5f6e63a2
...
...
@@ -4,16 +4,19 @@ module M
use import module ref.Ref
use import module array.Array as A
type uf = UF (link : array int)
(dist : array int) (* distance to representative *)
(size : int) (* elements are 0..size-1 *)
(num : int) (* number of classes *)
type uf = {| link : array int;
dist : array int; (* distance to representative *)
num : int; (* number of classes *) |}
logic size (u: uf) : int = A.length u.link
logic inv (u : uf) =
let UF l d s n = u in
(forall i:int. 0 <= i < s -> 0 <= l[i] < s) and
let s = A.length u.link in
A.length u.dist = s and
(forall i:int. 0 <= i < s -> 0 <= u.link[i] < s) and
(forall i:int. 0 <= i < s ->
((d[i] = 0 and l[i] = i) or (d[i] > 0 and d[l[i]] < d[i])))
( (u.dist[i] = 0 and u.link[i] = i)
or (u.dist[i] > 0 and u.dist[u.link[i]] < u.dist[i])))
inductive repr (u:uf) (x:int) (r:int) =
| Repr_root: forall u:uf. inv u ->
...
...
@@ -26,7 +29,7 @@ module M
lemma Repr_bounds_2:
forall u:uf, x y:int. repr u x y -> 0 <= y < size u
lemma Repr_dist_1:
forall u:uf, x y:int. repr u x y -> dist
u # y
= 0
forall u:uf, x y:int. repr u x y ->
u.
dist
[y]
= 0
logic same (u:uf) (x y:int) =
forall r:int. repr u x r <-> repr u y r
...
...
@@ -38,90 +41,86 @@ module M
forall u:uf. num u = 1 ->
forall x y:int. 0 <= x < size u -> 0 <= y < size u -> same u x y
let get_num_classes (u:ref uf) =
{} num !u { result = num u }
let create (n:int) =
{ 0 <= n }
let l = ref (A.create_const_length 0 n) in
let i = ref 0 in
while !i < n do
invariant { 0 <= i <= n and
forall j:int. 0 <= j < i -> l#j = j }
variant { n - i }
l := A.set !l !i !i;
i := !i + 1
done;
ref (UF !l (A.create_const_length 0 n) n n)
{ inv result and
num result = n and size result = n and
forall x:int. 0 <= x < n -> repr result x x }
let path_compression (u : ref uf) x r =
{ inv u and 0 <= x < size u and dist u # x > 0 and repr u x r }
let UF l d s n = !u in
let l = A.set l x r in
let d = A.set d x 1 in
u := UF l d s n
{ inv u and size u = size (old u) and
num u = num (old u) and same_reprs (old u) u }
let rec find (u:ref uf) (x:int) variant { dist u # x } =
{ inv u and 0 <= x < size u }
let y = A.get (link !u) x in
if y <> x then begin
let r = find u y in
path_compression u x r;
r
end else
x
{ inv u and
repr u x result and
size u = size (old u) and num u = num (old u) and
same_reprs u (old u) }
(***
parameter ghost_find : u:ref uf -> x:int ->
{ inv !u and 0 <= x < size !u }
int reads u
{ repr !u x result }
let increment u r =
{ inv !u and 0 <= r < size !u }
let i = ref 0 in
let d = ref (dist !u) in
while !i < size !u do
invariant { 0 <= !i <= size !u and
forall j:int. 0 <= j < size !u ->
!d#j = dist(!u)#j +
if repr !u j r and j < !i then 1 else 0 }
variant { size !u - !i }
if ghost_find u !i = r then
d := A.set !d !i (A.get !d !i + 1)
done;
!d
{ forall i:int. 0 <= i < size !u ->
result#i = (dist !u)#i + if repr !u i r then 1 else 0 }
let union u a b =
{ inv !u and
0 <= a < size !u and 0 <= b < size !u and not same !u a b }
let ra = find u a in
let rb = find u b in
let l = link !u in
let d = increment u ra in
u := UF (A.set l ra rb) d (size !u) (num !u - 1)
{ inv !u and
same !u a b and
size !u = size (old !u) and num !u = num (old !u) - 1 and
forall x y:int. 0 <= x < size !u -> 0 <= y < size !u ->
same !u x y <->
same (old !u) x y or
same (old !u) x a and same (old !u) b y or
same (old !u) x b and same (old !u) a y }
***)
let get_num_classes (u: uf) =
{} num u { result = num u }
let create (n:int) =
{ 0 <= n }
let l = A.make n 0 in
for i = 0 to n-1 do
invariant { forall j:int. 0 <= j < i -> u.link[j] = j }
A.set l i i
done;
mk_uf l (A.make n 0) n
{ inv result and
num result = n and size result = n and
forall x:int. 0 <= x < n -> repr result x x }
let path_compression (u : ref uf) x r =
{ inv u and 0 <= x < size u and dist u # x > 0 and repr u x r }
let UF l d s n = !u in
let l = A.set l x r in
let d = A.set d x 1 in
u := UF l d s n
{ inv u and size u = size (old u) and
num u = num (old u) and same_reprs (old u) u }
let rec find (u:ref uf) (x:int) variant { dist u # x } =
{ inv u and 0 <= x < size u }
let y = A.get (link !u) x in
if y <> x then begin
let r = find u y in
path_compression u x r;
r
end else
x
{ inv u and
repr u x result and
size u = size (old u) and num u = num (old u) and
same_reprs u (old u) }
(***
parameter ghost_find : u:ref uf -> x:int ->
{ inv !u and 0 <= x < size !u }
int reads u
{ repr !u x result }
let increment u r =
{ inv !u and 0 <= r < size !u }
let i = ref 0 in
let d = ref (dist !u) in
while !i < size !u do
invariant { 0 <= !i <= size !u and
forall j:int. 0 <= j < size !u ->
!d#j = dist(!u)#j +
if repr !u j r and j < !i then 1 else 0 }
variant { size !u - !i }
if ghost_find u !i = r then
d := A.set !d !i (A.get !d !i + 1)
done;
!d
{ forall i:int. 0 <= i < size !u ->
result#i = (dist !u)#i + if repr !u i r then 1 else 0 }
let union u a b =
{ inv !u and
0 <= a < size !u and 0 <= b < size !u and not same !u a b }
let ra = find u a in
let rb = find u b in
let l = link !u in
let d = increment u ra in
u := UF (A.set l ra rb) d (size !u) (num !u - 1)
{ inv !u and
same !u a b and
size !u = size (old !u) and num !u = num (old !u) - 1 and
forall x y:int. 0 <= x < size !u -> 0 <= y < size !u ->
same !u x y <->
same (old !u) x y or
same (old !u) x a and same (old !u) b y or
same (old !u) x b and same (old !u) a y }
***)
end
...
...
src/parser/parser.pre.mly
View file @
5f6e63a2
...
...
@@ -1119,6 +1119,8 @@ simple_expr:
{
$
2
}
|
LEFTPAR
RIGHTPAR
{
mk_expr
Eskip
}
|
LEFTREC
list1_field_expr
opt_semicolon
RIGHTREC
{
mk_expr
(
Erecord
(
List
.
rev
$
2
))
}
|
BEGIN
END
{
mk_expr
Eskip
}
|
OPPREF
simple_expr
...
...
@@ -1129,6 +1131,15 @@ simple_expr:
{
mk_mixfix3
"[<-]"
$
1
$
3
$
5
}
;
list1_field_expr
:
|
field_expr
{
[
$
1
]
}
|
list1_field_expr
SEMICOLON
field_expr
{
$
3
::
$
1
}
;
field_expr
:
|
lqualid
EQUAL
expr
{
$
1
,
$
3
}
;
list1_simple_expr
:
|
simple_expr
%
prec
prec_simple
{
[
$
1
]
}
|
simple_expr
list1_simple_expr
{
$
1
::
$
2
}
...
...
src/parser/ptree.ml
View file @
5f6e63a2
...
...
@@ -210,6 +210,7 @@ and expr_desc =
|
Elet
of
ident
*
expr
*
expr
|
Eletrec
of
(
ident
*
binder
list
*
variant
option
*
triple
)
list
*
expr
|
Etuple
of
expr
list
|
Erecord
of
(
qualid
*
expr
)
list
(* control *)
|
Esequence
of
expr
*
expr
|
Eif
of
expr
*
expr
*
expr
...
...
src/parser/typing.ml
View file @
5f6e63a2
...
...
@@ -671,7 +671,7 @@ and dfmla_node ~localize loc uc env = function
|
PPbinop
(
a
,
(
PPand
|
PPor
|
PPimplies
|
PPiff
as
op
)
,
b
)
->
Fbinop
(
binop
op
,
dfmla
~
localize
uc
env
a
,
dfmla
~
localize
uc
env
b
)
|
PPif
(
a
,
b
,
c
)
->
Fif
(
dfmla
~
localize
uc
env
a
,
Fif
(
dfmla
~
localize
uc
env
a
,
dfmla
~
localize
uc
env
b
,
dfmla
~
localize
uc
env
c
)
|
PPquant
(
q
,
uqu
,
trl
,
a
)
->
check_quant_linearity
uqu
;
...
...
@@ -710,7 +710,7 @@ and dfmla_node ~localize loc uc env = function
begin
match
e12
.
pp_desc
with
|
PPinfix
(
_
,
op1
,
e2
)
when
is_psymbol
(
Qident
op1
)
uc
->
let
e23
=
{
pp_desc
=
PPinfix
(
e2
,
op2
,
e3
);
pp_loc
=
loc
}
in
Fbinop
(
Tand
,
dfmla
~
localize
uc
env
e12
,
Fbinop
(
Tand
,
dfmla
~
localize
uc
env
e12
,
dfmla
~
localize
uc
env
e23
)
|
_
->
let
s
,
tyl
=
specialize_psymbol
(
Qident
op2
)
uc
in
...
...
@@ -921,8 +921,8 @@ let add_types dl th =
in
List
.
fold_left
add_projections
th
dl
let
prepare_typedef
td
=
if
td
.
td_model
then
let
prepare_typedef
td
=
if
td
.
td_model
then
errorm
~
loc
:
td
.
td_loc
"model types are not allowed in the logic"
;
match
td
.
td_def
with
|
TDabstract
|
TDalgebraic
_
|
TDalias
_
->
...
...
@@ -972,7 +972,7 @@ let add_logics dl th =
let
id
=
d
.
ld_ident
.
id
in
let
dadd_var
denv
(
x
,
ty
)
=
match
x
with
|
None
->
denv
|
Some
id
->
|
Some
id
->
{
denv
with
dvars
=
Mstr
.
add
id
.
id
(
dty
th'
denv
ty
)
denv
.
dvars
}
in
let
denv
=
Hashtbl
.
find
denvs
id
in
...
...
src/parser/typing.mli
View file @
5f6e63a2
...
...
@@ -91,3 +91,9 @@ val is_projection : theory_uc -> lsymbol -> (tysymbol * lsymbol * int) option
- [Some (ts, lsc, i)] if [ls] is the i-th projection of an
algebraic datatype [ts] with only one constructor [lcs]
- [None] otherwise *)
val
list_fields
:
theory_uc
->
(
Ptree
.
qualid
*
'
a
)
list
->
tysymbol
*
lsymbol
*
(
Ptree
.
loc
*
'
a
)
option
list
(** check that the given fields all belong to the same record type
and do not appear several times *)
src/programs/pgm_typing.ml
View file @
5f6e63a2
...
...
@@ -25,6 +25,7 @@ open Ident
open
Ty
open
Term
open
Theory
open
Pretty
open
Denv
open
Ptree
open
Pgm_ttree
...
...
@@ -103,8 +104,15 @@ let rec create_regions ~user n =
let
tv
=
create_tvsymbol
(
id_fresh
"rho"
)
in
tyvar
(
create_ty_decl_var
~
user
tv
)
::
create_regions
~
user
(
n
-
1
)
(* region variables are collected in the following list of lists
so that we can check after typing that two region variables in the same
list (i.e. for the same symbol) are not mapped to the same region *)
let
region_vars
=
ref
[]
let
new_regions_vars
()
=
region_vars
:=
Htv
.
create
17
::
!
region_vars
let
push_region_var
tv
vloc
=
match
!
region_vars
with
|
[]
->
assert
false
|
h
::
_
->
Htv
.
replace
h
tv
vloc
...
...
@@ -156,6 +164,10 @@ let rec specialize_type_v ?(policy=Region_var) ~loc htv = function
(
List
.
map
(
fun
pv
->
specialize_type_v
~
loc
htv
pv
.
pv_tv
)
bl
)
(
specialize_type_v
~
policy
:
Region_ret
~
loc
htv
c
.
c_result_type
)
let
specialize_lsymbol
?
(
policy
=
Region_var
)
~
loc
htv
s
=
List
.
map
(
specialize_ty
~
policy
~
loc
htv
)
s
.
ls_args
,
option_map
(
specialize_ty
~
policy
:
Region_ret
~
loc
htv
)
s
.
ls_value
let
parameter
x
=
"parameter "
^
x
let
rec
parameter_q
=
function
|
[]
->
assert
false
...
...
@@ -364,7 +376,7 @@ and dexpr_desc ~ghost env loc = function
DElocal
(
x
,
tyv
)
,
tyv
|
Ptree
.
Eident
p
->
(* global variable *)
region_vars
:=
Htv
.
create
17
::
!
region_vars
;
new_
region
s
_vars
()
;
let
x
=
Typing
.
string_list_of_qualid
[]
p
in
let
ls
=
try
...
...
@@ -428,21 +440,39 @@ and dexpr_desc ~ghost env loc = function
let
s
=
Typing
.
fs_tuple
n
in
let
tyl
=
List
.
map
(
fun
_
->
create_type_var
loc
)
el
in
let
ty
=
dty_app
(
Typing
.
ts_tuple
n
,
tyl
)
in
let
create
d
ty
=
{
dexpr_desc
=
d
;
dexpr_type
=
ty
;
dexpr_loc
=
loc
}
in
let
create
d
ty
=
{
dexpr_desc
=
d
;
dexpr_type
=
ty
;
dexpr_loc
=
loc
}
in
let
apply
e1
e2
ty2
=
let
e2
=
dexpr
~
ghost
env
e2
in
assert
(
Denv
.
unify
e2
.
dexpr_type
ty2
);
let
ty
=
create_type_var
loc
in
assert
(
Denv
.
unify
e1
.
dexpr_type
(
dty_app
(
ts_arrow
,
[
ty2
;
ty
])));
assert
(
Denv
.
unify
e1
.
dexpr_type
(
dty_app
(
ts_arrow
,
[
ty2
;
ty
])));
create
(
DEapply
(
e1
,
e2
))
ty
in
let
e
=
create
(
DElogic
s
)
(
dcurrying
tyl
ty
)
in
let
e
=
List
.
fold_left2
apply
e
el
tyl
in
e
.
dexpr_desc
,
ty
|
Ptree
.
Erecord
fl
->
let
_
,
cs
,
fl
=
Typing
.
list_fields
(
impure_uc
env
.
uc
)
fl
in
new_regions_vars
()
;
let
tyl
,
ty
=
specialize_lsymbol
~
loc
(
Htv
.
create
17
)
cs
in
let
ty
=
of_option
ty
in
let
create
d
ty
=
{
dexpr_desc
=
d
;
dexpr_type
=
ty
;
dexpr_loc
=
loc
}
in
let
constructor
d
f
tyf
=
match
f
with
|
Some
(
_
,
f
)
->
let
f
=
dexpr
~
ghost
env
f
in
assert
(
Denv
.
unify
f
.
dexpr_type
tyf
);
let
ty
=
create_type_var
loc
in
assert
(
Denv
.
unify
d
.
dexpr_type
(
dty_app
(
ts_arrow
,
[
tyf
;
ty
])));
create
(
DEapply
(
d
,
f
))
ty
|
None
->
errorm
~
loc
"some record fields are missing"
in
let
d
=
let
ps
=
get_psymbol
cs
in
create
(
DElogic
ps
.
ps_pure
)
(
dcurrying
tyl
ty
)
in
let
d
=
List
.
fold_left2
constructor
d
fl
tyl
in
d
.
dexpr_desc
,
ty
|
Ptree
.
Esequence
(
e1
,
e2
)
->
let
e1
=
dexpr
~
ghost
env
e1
in
...
...
@@ -1995,8 +2025,7 @@ let add_logics env ltm uc d =
in
let
addi
uc
d
=
add
uc
{
ld_loc
=
d
.
in_loc
;
ld_ident
=
d
.
in_ident
;
ld_params
=
List
.
map
add_param
d
.
in_params
;
ld_type
=
None
;
ld_def
=
None
;
}
ld_params
=
d
.
in_params
;
ld_type
=
None
;
ld_def
=
None
;
}
in
match
d
with
|
LogicDecl
dl
->
List
.
fold_left
add
uc
dl
...
...
src/util/util.ml
View file @
5f6e63a2
...
...
@@ -163,7 +163,7 @@ let list_fold_lefti f acc l =
let
rec
prefix
n
l
=
if
n
=
0
then
[]
else
if
n
<
0
||
l
=
[]
then
invalid_arg
"Util.chop"
else
List
.
hd
l
::
prefix
(
n
-
1
)
l
else
List
.
hd
l
::
prefix
(
n
-
1
)
(
List
.
tl
l
)
let
rec
chop
n
l
=
if
n
=
0
then
l
...
...
tests/test-pgm-jcf.mlw
View file @
5f6e63a2
...
...
@@ -2,14 +2,10 @@
module M
use import int.Int
type t = {| mutable a: int; mutable b: int |}
let test (x: t) =
a x = b x
type t = {| mutable a: int; mutable b: int |}
let foo (x: t) =
test x
let foo () = {} let x = {| a = 1; b = 2 |} in a x { result=1 }
end
...
...
@@ -41,9 +37,9 @@ module TestRef
let bar () = { a=0 } a := 1 { a=1 }
(* TODO:
le programme "let f n = n := 1"
provoque "undefined type variable" (la rgion)
(* TODO:
le programme "let f n = n := 1"
provoque "undefined type variable" (la rgion)
problme : comment faire l'infrence du type de n
*)
...
...
@@ -60,9 +56,9 @@ module TestArray
use import module stdlib.Array
(* TODO: update *)
let f (x: array int) =
{ x.length = 2 }
set x 0 1;
let f (x: array int) =
{ x.length = 2 }
set x 0 1;
set x 1 2
{ x[1] = 2 and x.length = 2 }
...
...
@@ -70,7 +66,7 @@ end
**)
(*
Local Variables:
Local Variables:
compile-command: "unset LANG; make -C .. testl-ide"
End:
End:
*)
Write
Preview
Supports
Markdown
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