programs: checking variant for mutally recursive functions

parent 147694e9
......@@ -237,6 +237,11 @@ clean::
rm -f bin/whyml.byte bin/whyml.opt
rm -f .depend.programs
# test target
%: %.mlw bin/whyml.byte
bin/whyml.byte -I theories $*.mlw
###############
# proof manager
###############
......@@ -511,12 +516,6 @@ test: bin/why.byte $(TOOLS)
testl: bin/whyml.byte
ocamlrun -bt bin/whyml.byte -I theories/ tests/test-pgm-jcf.mlw
bench/programs/good/%: bin/whyml.byte
bin/whyml.byte -I theories bench/programs/good/$*.mlw
examples/programs/%: bin/whyml.byte
bin/whyml.byte -I theories examples/programs/$*.mlw
###############
# installation
###############
......
(* missing variant *)
let rec even (x:int) variant {x} =
odd (x-1) : int
and odd (x:int) =
even (x-1) : int
(* different relations *)
{
logic rel(int, int)
}
let rec even (x:int) variant {x} for rel =
odd (x-1) : int
and odd (x:int) variant {x} =
even (x-1) : int
......@@ -566,7 +566,27 @@ and letrec uc env dl =
let t = triple uc env t in
(v, bl, var, t)
in
env, List.map step2 dl
let dl = List.map step2 dl in
(* finally, check variants are all absent or all present and consistent *)
let error e =
errorm ~loc:e.expr_loc "variants must be all present or all absent"
in
begin match dl with
| [] ->
assert false
| (_, _, None, _) :: r ->
let check_no_variant (_,_,var,(_,e,_)) = if var <> None then error e in
List.iter check_no_variant r
| (_, _, Some (_, ps), _) :: r ->
let check_variant (_,_,var,(_,e,_)) = match var with
| None -> error e
| Some (_, ps') -> if not (ls_equal ps ps') then
errorm ~loc:e.expr_loc
"variants must share the same order relation"
in
List.iter check_variant r
end;
env, dl
and triple uc env ((denvp, p), e, q) =
let p = Typing.type_fmla denvp env p in
......@@ -652,7 +672,8 @@ TODO:
- tuples
- mutually recursive functions: check variants are all present or all absent
- variant: check type int or relation order specified
- program symbol table outside of the theory
- ghost / effects
*)
......@@ -29,7 +29,7 @@ let rec is_even (x:int) variant {x} for rel =
if x = 0 then True else not (is_odd (x-1))
{true}
and is_odd (x:int) variant {x} for rel2 =
and is_odd (x:int) variant {x} for rel =
if x = 0 then False else not (is_even (x-1))
let b = is_even 2
......@@ -82,7 +82,7 @@ let rec size_tree (t: 'a tree) variant {tree_height(t)} = match t with
| Empty -> 0
| Node (_, f) -> 1 + size_forest f
end
and size_forest (f: 'a forest) = match f with
and size_forest (f: 'a forest) variant {forest_height(f)} = match f with
| Fnil -> 0
| Fcons (t, f) -> size_tree t + size_forest f
end
......
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