programs: wp for match/with

parent a05a5f89
{
use import list.List
use import list.Length
}
let rec length_ (l : list 'a) variant { length l } =
{}
match l with
| Nil -> 0
| Cons _ r -> 1 + length_ r
end
{ result = length l }
let rec append (l1 : list 'a) (l2 : list 'a) variant { length l1 } =
{ }
match l1 with
| Nil -> l2
| Cons x r -> Cons x (append r l2)
end
{ length result = length l1 + length l2 }
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/list"
End:
*)
../programs/good/list.mlw
\ No newline at end of file
(* find a value in a sorted list *)
{
use import list.Mem
inductive sorted (l : list int) =
| Sorted_Nil :
sorted Nil
| Sorted_One :
forall x:int. sorted (Cons x Nil)
| Sorted_Two :
forall x y : int, l : list int.
x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l))
lemma Sorted_inversion :
forall y : int, l : list int. sorted (Cons y l) -> sorted l
lemma Sorted_not_mem:
forall x y : int, l : list int.
x < y -> sorted (Cons y l) -> not mem x (Cons y l)
}
let rec find x l =
{ sorted l }
match l with
| Nil -> False
| Cons y r -> x = y || x > y && find x r
end
{ result=True <-> mem x l }
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/sorted_list"
End:
*)
......@@ -146,7 +146,7 @@ and iexpr_desc =
| IEif of iexpr * iexpr * iexpr
| IEloop of loop_annotation * iexpr
| IElazy of lazy_op * iexpr * iexpr
| IEmatch of iexpr list * (Term.pattern list * iexpr) list
| IEmatch of Term.vsymbol list * (Term.pattern list * iexpr) list
| IEskip
| IEabsurd
| IEraise of Term.lsymbol * iexpr option
......@@ -183,7 +183,7 @@ and expr_desc =
| Esequence of expr * expr
| Eif of expr * expr * expr
| Eloop of loop_annotation * expr
| Ematch of expr list * (Term.pattern list * expr) list
| Ematch of Term.vsymbol list * (Term.pattern list * expr) list
| Eskip
| Eabsurd
| Eraise of Term.lsymbol * expr option
......
......@@ -682,7 +682,14 @@ and iexpr_desc gl env loc ty = function
(pl, iexpr gl env e)
in
let bl = List.map branch bl in
IEmatch (el, bl)
let rec mk_let vl = function
| [] ->
IEmatch (List.rev vl, bl)
| e :: el ->
let v = create_vsymbol (id_user "x" loc) e.iexpr_type in
IElet (v, e, mk_iexpr loc ty (mk_let (v :: vl) el))
in
mk_let [] el
| DEskip ->
IEskip
| DEabsurd ->
......@@ -975,19 +982,15 @@ and expr_desc gl env loc ty = function
Eif (e1, mk_true loc gl, e2)
in
d, Tpure ty, ef
| IEmatch (el, bl) ->
let add1 ef e =
let e = expr gl env e in E.union ef e.expr_effect, e
in
let ef, el = map_fold_left add1 E.empty el in
| IEmatch (vl, bl) ->
let branch ef (pl, e) =
let env = add_local_pats env pl in
let e = expr gl env e in
let ef = E.union ef e.expr_effect in
ef, (pl, e)
in
let ef, bl = map_fold_left branch ef bl in
Ematch (el, bl), Tpure ty, ef
let ef, bl = map_fold_left branch E.empty bl in
Ematch (vl, bl), Tpure ty, ef
| IEskip ->
Eskip, Tpure ty, E.empty
| IEabsurd ->
......
......@@ -297,8 +297,10 @@ and wp_desc env e q = match e.expr_desc with
(quantify env e.expr_effect (wp_implies i we)))
in
w
| Ematch _ ->
assert false (*TODO*)
| Ematch (xl, bl) ->
let branch (p, e) = p, wp_expr env e (filter_post e.expr_effect q) in
let tl = List.map t_var xl in
f_case tl (List.map branch bl)
| Eskip ->
let (_, q), _ = q in q
| Eabsurd ->
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment