programs: recursive functions

parent c1a3c3f9
(** Recursive functions *)
(** 1. Pure function *)
let rec f1 (x:int) : int variant { x } =
{ x >= 0 } (if x > 0 then (f1 (x-1)) else x) { result = 0 }
(** 2. With effects but no argument *)
parameter x : int ref
let rec f2 (u:unit) : unit variant { !x } =
{ !x >= 0 } (if !x > 0 then begin x := !x - 1; f2 () end) { !x = 0 }
(** 3. With effects and a pure argument *)
let rec f3 (a:int) : unit variant { a } =
{ a >= 0 }
if a > 0 then begin x := !x + 1; (f3 (a-1)) end
{ !x = old !x + a }
(** 4. With effects and a reference as argument *)
let rec f4 (a:int ref) : unit variant { !a } =
{ !a >= 0 }
if !a > 0 then begin x := !x + 1; a := !a - 1; f4 a end
{ !x = old !x + old !a }
(** 5. The acid test:
partial application of a recursive function with effects *)
let rec f5 (a:int ref) (b:int ref) variant { !a } =
{ !a >= 0 }
if !a = 0 then !b else begin a := !a - 1; b := !b + 1; f5 a b end
{ result = old !a + old !b }
let test_f5 () =
{ !x >= 0 } let f = f5 x in let b = ref 0 in f b { result = old !x }
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/recfun"
End:
*)
../programs/good/recfun.mlw
\ No newline at end of file
......@@ -181,7 +181,6 @@ and expr_desc =
| Esequence of expr * expr
| Eif of expr * expr * expr
| Eloop of loop_annotation * expr
| Elazy of lazy_op * expr * expr
| Ematch of expr list * (Term.pattern list * expr) list
| Eskip
| Eabsurd
......
......@@ -447,12 +447,13 @@ and dletrec env dl =
let add_one env (id, bl, var, t) =
let ty = create_type_var id.id_loc in
let env = add_local env id.id (DTpure ty) in
env, ((id, ty), bl, option_map (dvariant env) var, t)
env, ((id, ty), bl, var, t)
in
let env, dl = map_fold_left add_one env dl in
(* then type-check all of them and unify *)
let type_one ((id, tyres), bl, v, t) =
let env, bl = map_fold_left dbinder env bl in
let v = option_map (dvariant env) v in
let (_,e,_) as t = dtriple env t in
let tyl = List.map (fun (x,_) -> Typing.find_var x.id env.denv) bl in
let ty = dcurrying env.env tyl e.dexpr_type in
......@@ -831,7 +832,7 @@ let rec is_pure_expr e =
| Elabel (_, e1) -> is_pure_expr e1
| Eany c -> E.no_side_effect c.c_effect
| Eghost _ | Eassert _ | Etry _ | Eraise _ | Ematch _
| Elazy _ | Eloop _ | Esequence _ | Eletrec _ | Efun _
| Eloop _ | Esequence _ | Eletrec _ | Efun _
| Eglobal _ | Eabsurd -> false (* TODO: improve *)
let mk_expr loc ty ef d =
......@@ -1116,6 +1117,4 @@ TODO:
- polymorphic let?
- ghost
- move effect inference here (from pgm_wp), as phase 3
*)
......@@ -261,8 +261,10 @@ and wp_desc env e q = match e.expr_desc with
let q1 = result, f_subst (subst1 x (t_var result)) w2 in
let q1 = saturate_post e1.expr_effect q1 q in
wp_expr env e1 q1
| Eletrec _ ->
assert false (*TODO*)
| Eletrec (dl, e1) ->
let w1 = wp_expr env e1 q in
let wl = List.map (wp_recfun env) dl in
wp_ands ~sym:true (w1 :: wl)
| Esequence (e1, e2) ->
let w2 = wp_expr env e2 (filter_post e2.expr_effect q) in
......@@ -295,8 +297,6 @@ and wp_desc env e q = match e.expr_desc with
(quantify env e.expr_effect (wp_implies i we)))
in
w
| Elazy _ ->
assert false (*TODO*)
| Ematch _ ->
assert false (*TODO*)
| Eskip ->
......@@ -351,7 +351,7 @@ and wp_desc env e q = match e.expr_desc with
let w = opaque_wp env c.c_effect c.c_post q in
wp_and c.c_pre w
| _ ->
| Eghost _ ->
assert false (*TODO*)
and wp_triple env (p, e, q) =
......@@ -359,11 +359,13 @@ and wp_triple env (p, e, q) =
let f = wp_implies p f in
quantify ~all:true env e.expr_effect f
and wp_recfun env (_, bl, _var, t) =
let f = wp_triple env t in
wp_binders bl f
let wp env e =
wp_expr env e (default_post e.expr_type e.expr_effect)
let wp_recfun _env _l _def = f_true (* TODO *)
let add_wp_decl l f env =
let pr = create_prsymbol (id_fresh ("WP_" ^ l.ls_name.id_string)) in
let d = create_prop_decl Pgoal pr f in
......@@ -381,10 +383,11 @@ let decl env = function
env
| Pgm_ttree.Dletrec dl ->
let add_one env (ls, def) =
let f = wp_recfun env ls def in
let env = add_wp_decl ls f env in
let _v = assert false (*TODO*) in
env
let f = wp_recfun env def in
if !debug then
eprintf "wp %a = %a@\n----------------@."
print_ls ls Pretty.print_fmla f;
add_wp_decl ls f env
in
List.fold_left add_one env dl
| Pgm_ttree.Dparam _ ->
......
let foo (x:int ref) =
{ }
if !x = 0 && !x = 1 then 2 else 3
{ result = 3 }
let rec foo (x:int) =
{ x >= 0 }
if x = 0 then 0 else foo (x-1)+1-1
{ result = 0 }
let test () = {} foo 4 {result=0}
(*
Local Variables:
......
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