Commit 15515d3e authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: type for and loop constructions

parent 5d63c35e
......@@ -157,7 +157,11 @@ let xpost_vars = Mexn.fold (fun xs -> post_vars xs.xs_ity)
let variant_vars varl vsset =
let add_variant s { v_term = t; v_rel = ps } =
ignore (Util.option_map (fun ps -> ps_app ps [t;t]) ps);
begin match ps with
| Some ps -> ignore (ps_app ps [t;t])
| None -> t_ty_check t (Some ty_int)
(* TODO: allow algebraic types in variants *)
end;
Mvs.set_union s t.t_vars in
List.fold_left add_variant vsset varl
......@@ -412,7 +416,7 @@ type for_direction = To | DownTo
type for_bounds = pvsymbol * for_direction * pvsymbol
type invariant = term option
type invariant = term
type expr = {
e_node : expr_node;
......@@ -814,7 +818,7 @@ let e_lazy_or e1 e2 =
let e_loop inv variant e =
let vtv = vtv_of_expr e in
ity_equal_check vtv.vtv_ity ity_unit;
let vsset = Util.option_fold (fun s f -> fmla_vars f s) Mvs.empty inv in
let vsset = fmla_vars inv Mvs.empty in
let vsset = variant_vars variant vsset in
let vars = Mvs.fold (fun vs _ m -> add_vs_vars vs m) vsset e.e_vars in
check_postexpr e e.e_effect vars;
......@@ -828,10 +832,12 @@ let e_for_real pv bounds inv e =
ity_equal_check pv.pv_vtv.vtv_ity ity_int;
ity_equal_check pvfrom.pv_vtv.vtv_ity ity_int;
ity_equal_check pvto.pv_vtv.vtv_ity ity_int;
if pv.pv_vtv.vtv_mut <> None then
Loc.errorm "mutable index in a for loop";
let ghost = pv.pv_vtv.vtv_ghost || pvfrom.pv_vtv.vtv_ghost ||
pvto.pv_vtv.vtv_ghost || vtv.vtv_ghost in
let eff = if ghost then eff_ghostify e.e_effect else e.e_effect in
let vars = Util.option_fold (fun m f -> add_t_vars f m) e.e_vars inv in
let vars = add_t_vars inv e.e_vars in
(* FIXME? We check that no variable in the loop body, _including_
the index variable, is not invalidated because of a region reset.
We ignore the loop bounds, since they are computed just once. *)
......
......@@ -149,7 +149,7 @@ type for_direction = To | DownTo
type for_bounds = pvsymbol * for_direction * pvsymbol
type invariant = term option
type invariant = term
type expr = private {
e_node : expr_node;
......
......@@ -174,7 +174,8 @@ let rec print_type_v fmt = function
| SpecV vtv -> print_vtv fmt vtv
| SpecA (pvl,tyc) ->
let print_arg fmt pv = fprintf fmt "(%a) ->@ " print_pvty pv in
fprintf fmt "%a%a" (print_list nothing print_arg) pvl print_type_c tyc
fprintf fmt "%a%a" (print_list nothing print_arg) pvl print_type_c tyc;
List.iter forget_pv pvl
and print_type_c fmt tyc =
fprintf fmt "{ %a }@ %a%a@ { %a }@]"
......@@ -184,9 +185,8 @@ and print_type_c fmt tyc =
print_post tyc.c_post
(* TODO: print_xpost *)
let print_invariant fmt = function
| Some f -> fprintf fmt "invariant@ { %a }@ " Pretty.print_term f
| None -> ()
let print_invariant fmt f =
fprintf fmt "invariant@ { %a }@ " Pretty.print_term f
let print_variant fmt varl =
let print_rel fmt = function
......@@ -196,6 +196,10 @@ let print_variant fmt varl =
fprintf fmt " %a%a" Pretty.print_term t print_rel ps in
fprintf fmt "variant@ {%a }@ " (print_list comma print_var) varl
let print_invariant fmt f = match f.t_node with
| Ttrue -> ()
| _ -> print_invariant fmt f
let print_variant fmt = function
| [] -> ()
| varl -> print_variant fmt varl
......@@ -263,12 +267,17 @@ and print_enode pri fmt e = match e.e_node with
print_ps fmt a
| Eapp (e,v) ->
fprintf fmt "(%a@ %a)" (print_lexpr pri) e print_pv v
| Elet ({ let_var = LetV pv ; let_expr = e1 }, e2)
when pv.pv_vs.vs_name.id_string = "_" &&
ity_equal pv.pv_vtv.vtv_ity ity_unit ->
fprintf fmt (protect_on (pri > 0) "%a;@\n%a")
print_expr e1 print_expr e2;
| Elet ({ let_var = lv ; let_expr = e1 }, e2) ->
fprintf fmt (protect_on (pri > 0) "let %a = @[%a@] in@ %a")
fprintf fmt (protect_on (pri > 0) "@[<hov 2>let %a =@ %a@ in@]@\n%a")
print_lv lv (print_lexpr 4) e1 print_expr e2;
forget_lv lv
| Erec (rdl,e) ->
fprintf fmt (protect_on (pri > 0) "%a@ in@ %a")
fprintf fmt (protect_on (pri > 0) "%a@ in@\n%a")
(print_list_next newline print_rec) rdl print_expr e;
let forget_rd rd = forget_ps rd.rec_ps in
List.iter forget_rd rdl
......@@ -285,7 +294,7 @@ and print_enode pri fmt e = match e.e_node with
fprintf fmt "loop@ %a%a@\n@[<hov>%a@]@\nend"
print_invariant inv print_variant var print_expr e
| Efor (pv,(pvfrom,dir,pvto),inv,e) ->
fprintf fmt "for@ %a@ =@ %a@ %s@ %a@ %ado\n@[<hov>%a@]@\ndone"
fprintf fmt "@[<hov 2>for@ %a@ =@ %a@ %s@ %a@ %ado@\n%a@]@\ndone"
print_pv pv print_pv pvfrom
(if dir = To then "to" else "downto") print_pv pvto
print_invariant inv print_expr e
......@@ -313,7 +322,7 @@ and print_xbranch fmt (xs, pv, e) =
and print_rec fst fmt { rec_ps = ps ; rec_lambda = lam } =
let print_arg fmt pv = fprintf fmt "(%a)" print_pvty pv in
fprintf fmt "@[<hov 2>%s (%a) %a =@ { %a }@ %a%a@ { %a }@]"
fprintf fmt "@[<hov 2>%s (%a) %a =@\n{ %a }@\n%a%a@\n{ %a }@]"
(if fst then "let rec" else "with")
print_psty ps
(print_list space print_arg) lam.l_args
......
......@@ -347,6 +347,14 @@ and dtype_v denv = function
let tyc,dity = dtype_c denv tyc in
DSpecA (bl,tyc), make_arrow_type tyl dity
let dvariant uc = function
| Some (le, Some q) -> [le, Some (find_variant_ls uc q)]
| Some (le, None) -> [le, None]
| None -> []
(* TODO: accept a list of variants in the surface language
List.map (fun (le,q) -> le, Util.option_map (find_variant_ls uc) q) var
*)
(* expressions *)
let de_unit ~loc = hidden_ls ~loc (fs_tuple 0)
......@@ -522,10 +530,20 @@ and de_desc denv loc = function
| Ptree.Eany tyc ->
let tyc, dity = dtype_c denv tyc in
DEany tyc, dity
| Ptree.Eloop (_ann, _e1) ->
assert false (*TODO*)
| Ptree.Efor (_id, _e1, _dir, _e2, _lexpr_opt, _e3) ->
assert false (*TODO*)
| Ptree.Eloop ({ loop_invariant = inv; loop_variant = var }, e1) ->
let e1 = dexpr denv e1 in
let var = dvariant denv.uc var in
expected_type e1 dity_unit;
DEloop (var,inv,e1), e1.de_type
| Ptree.Efor (id, efrom, dir, eto, inv, e1) ->
let efrom = dexpr denv efrom in
let eto = dexpr denv eto in
let denv = add_var id dity_int denv in
let e1 = dexpr denv e1 in
expected_type efrom dity_int;
expected_type eto dity_int;
expected_type e1 dity_unit;
DEfor (id,efrom,dir,eto,inv,e1), e1.de_type
| Ptree.Eabstract (_e1, _post) ->
assert false (*TODO*)
......@@ -545,15 +563,9 @@ and dletrec denv rdl =
and dlambda denv bl var (p, e, (q, xq)) =
let denv,bl,tyl = dbinders denv bl in
let e = dexpr denv e in
let var = match var with
| Some (le, Some q) -> [le, Some (find_variant_ls denv.uc q)]
| Some (le, None) -> [le, None]
| None -> [] in
(* TODO: accept a list of variants in the surface language
let var = List.map (fun (le,q) ->
le, Util.option_map (find_variant_ls denv.uc) q) var in
*)
(bl, var, p, e, q, dxpost denv.uc xq), make_arrow_type tyl e.de_type
let var = dvariant denv.uc var in
let xq = dxpost denv.uc xq in
(bl, var, p, e, q, xq), make_arrow_type tyl e.de_type
(** stage 2 *)
......@@ -587,8 +599,10 @@ let create_post lenv x ty f =
let create_pre lenv f =
Typing.type_fmla (get_theory lenv.mod_uc) lenv.log_denv lenv.log_vars f
let create_variant lenv t =
Typing.type_term (get_theory lenv.mod_uc) lenv.log_denv lenv.log_vars t
let create_variant lenv (t,r) =
let t =
Typing.type_term (get_theory lenv.mod_uc) lenv.log_denv lenv.log_vars t in
{ v_term = t; v_rel = r }
let add_local x lv lenv = match lv with
| LetA _ ->
......@@ -728,8 +742,25 @@ let rec expr lenv de = match de.de_desc with
e_any (type_c lenv dtyc)
| DEghost de1 ->
e_ghost (expr lenv de1)
| _ ->
assert false (*TODO*)
| DEloop (var,inv,de1) ->
let inv = match inv with
| Some inv -> create_pre lenv inv
| None -> t_true in
let var = List.map (create_variant lenv) var in
e_loop inv var (expr lenv de1)
| DEfor (x,defrom,dir,deto,inv,de1) ->
let efrom = expr lenv defrom in
let eto = expr lenv deto in
let pv = create_pvsymbol (Denv.create_user_id x) (vty_value ity_int) in
let lenv = add_local x.id (LetV pv) lenv in
let dir = match dir with
| Ptree.To -> To
| Ptree.Downto -> DownTo in
let inv = match inv with
| Some inv -> create_pre lenv inv
| None -> t_true in
let e1 = expr lenv de1 in
e_for pv efrom dir eto inv e1
and expr_rec lenv rdl =
let step1 lenv (id, dity, lam) =
......@@ -751,10 +782,10 @@ and expr_lam lenv (bl, var, p, e, q, xq) =
let e = expr lenv e in
let ty = match e.e_vty with
| VTarrow _ -> ty_unit
| VTvalue vtv -> ty_of_ity vtv.vtv_ity in
let mk_variant (t,r) = { v_term = create_variant lenv t; v_rel = r } in
| VTvalue vtv -> ty_of_ity vtv.vtv_ity
in
{ l_args = pvl;
l_variant = List.map mk_variant var;
l_variant = List.map (create_variant lenv) var;
l_pre = create_pre lenv p;
l_expr = e;
l_post = create_post lenv "result" ty q;
......
......@@ -44,7 +44,7 @@ module N
| Node {| contents = v |} f -> v + on_forest f
| Leaf -> raise (Exit Leaf)
end { at r 'L = t }
with on_forest f variant { f } = match f with
with on_forest f = match f with
| Cons t f -> let ee = Leaf in on_tree t + on_forest f + on_tree ee
| Nil -> 1
end
......@@ -52,6 +52,7 @@ module N
let dr = create_dref 0 in
let or = dr.dcontents in
let nr = {| contents = 1 |} in
for i = 3 to 10 do let j = i + 5 in () done;
dr.dcontents <- nr;
assert { r = r };
try on_tree r with Exit -> 0 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