Commit 87c6bc75 authored by Jean-Christophe's avatar Jean-Christophe

fixed typing error with variants when int.Int is not imported

parent 04d4cf72
......@@ -81,7 +81,7 @@ and print_pv fmt v =
and print_triple fmt (p, e, q) =
fprintf fmt "@[<hv 0>%a@ %a@ %a@]" print_pre p print_expr e print_post q
and print_recfun fmt (v, bl, _, t, _) =
and print_recfun fmt (v, bl, t, _) =
fprintf fmt "@[<hov 2>rec %a@ %a =@ %a@]"
print_pv v (print_list space print_pv) bl print_triple t
......
......@@ -134,7 +134,11 @@ and dtriple = dpre * dexpr * dpost
(*****************************************************************************)
(* phase 2: removal of destructive types *)
type variant = Term.term * Term.lsymbol option
type variant_rel =
| Vuser of Term.lsymbol
| Vint of Term.lsymbol (* <= *) * Term.lsymbol (* < *)
type variant = Term.term * variant_rel
type loop_annotation = {
loop_invariant : Term.term option;
......@@ -175,7 +179,7 @@ and ibinder = ivsymbol * itype_v
type label = Term.vsymbol
type irec_variant = ivsymbol * Term.term * Term.lsymbol option
type irec_variant = ivsymbol * Term.term * variant_rel
(* FIXME: get rid of ipattern *)
type ipattern = {
......@@ -236,8 +240,6 @@ type pre = T.pre
type post = T.post
type rec_variant = pvsymbol * Term.term * Term.lsymbol option
type pattern = {
ppat_pat : Term.pattern; (* logic variables *)
ppat_node : ppat_node;
......@@ -279,7 +281,7 @@ and expr_desc =
| Elabel of label * expr
| Eany of type_c
and recfun = pvsymbol * pvsymbol list * rec_variant option * triple * E.t
and recfun = pvsymbol * pvsymbol list * triple * E.t
and triple = pre * expr * post
......
......@@ -879,6 +879,13 @@ let iterm env l =
let t = dterm (pure_uc env.i_uc) env.i_denv l in
Denv.term env.i_pures t
let variant_rel_int env loc =
let find s =
try find_ls ~pure:true env s
with Not_found -> errorm ~loc "cannot find symbol %s" s
in
Vint (find "infix <=", find "infix <")
(* TODO: should we admit an instance of a polymorphic order relation? *)
let ivariant env (t, ps) =
let loc = t.pp_loc in
......@@ -887,9 +894,9 @@ let ivariant env (t, ps) =
| None ->
if not (Ty.ty_equal ty_int (t_type t)) then
errorm ~loc "variant should have type int";
t, ps
| Some { ls_args = [t1; _] } when Ty.ty_equal t1 (t_type t) ->
t, ps
t, variant_rel_int env.i_uc loc
| Some ({ ls_args = [t1; _] } as ps) when Ty.ty_equal t1 (t_type t) ->
t, Vuser ps
| Some { ls_args = [t1; _] } ->
errorm ~loc "@[variant has type %a, but is expected to have type %a@]"
Pretty.print_ty (t_type t) Pretty.print_ty t1
......@@ -1297,8 +1304,8 @@ and iletrec gl env dl =
List.iter check_no_variant r
| (_, _, Some (_, _, ps), _) :: r ->
let r_equal r1 r2 = match r1, r2 with
| None, None -> true
| Some ls1, Some ls2 -> ls_equal ls1 ls2
| Vint _, Vint _ -> true
| Vuser ls1, Vuser ls2 -> ls_equal ls1 ls2
| _ -> false
in
let check_variant (_,_,var,(_,e,_)) = match var with
......@@ -1570,7 +1577,7 @@ and expr_desc gl env loc ty = function
| IEletrec (dl, e1) ->
let env, dl = letrec gl env dl in
let e1 = expr gl env e1 in
let add_effect ef (_,_,_,_,ef') = E.union ef ef' in
let add_effect ef (_,_,_,ef') = E.union ef ef' in
let ef = List.fold_left add_effect e1.expr_effect dl in
Eletrec (dl, e1), e1.expr_type_v, ef
......@@ -1588,8 +1595,10 @@ and expr_desc gl env loc ty = function
let ef = e1.expr_effect in
let ef, inv = option_map_fold term_effect ef a.loop_invariant in
let ef, var = match a.loop_variant with
| Some (t, ls) -> let ef, t = term_effect ef t in ef, Some (t, ls)
| None -> ef, None
| Some (t, ls) ->
let ef, t = term_effect ef t in ef, Some (t, ls)
| None ->
ef, None
in
let a = { loop_invariant = inv; loop_variant = var } in
Eloop (a, e1), type_v_unit gl, ef
......@@ -1709,13 +1718,8 @@ and letrec gl env dl = (* : env * recfun list *)
| Some phi0, Some (_, phi, r) ->
let _, phi = term_effect E.empty phi in
let decphi = match r with
| None -> (* 0 <= phi0 and phi < phi0 *)
t_and (ps_app (find_ls ~pure:true gl "infix <=")
[t_int_const "0"; t_var phi0])
(ps_app (find_ls ~pure:true gl "infix <")
[phi;t_var phi0])
| Some r ->
ps_app r [phi; t_var phi0]
| Vint (le, lt) -> Pgm_wp.default_variant le lt phi (t_var phi0)
| Vuser r -> ps_app r [phi; t_var phi0]
in
{ c with c_pre = t_and decphi c.c_pre }
| _ ->
......@@ -1761,8 +1765,8 @@ and letrec gl env dl = (* : env * recfun list *)
in
let m0 = List.fold_left add_empty_effect Mvs.empty dl in
let m, dl = fixpoint m0 in
let add_effect (pv, bl, var, (_,e,_ as t)) =
pv, bl, var, t, remove_bl_effects bl e.expr_effect
let add_effect (pv, bl, _, (_,e,_ as t)) =
pv, bl, t, remove_bl_effects bl e.expr_effect
in
make_env env m, List.map add_effect dl
......@@ -1784,7 +1788,7 @@ let rec fresh_expr gl ~term locals e = match e.expr_desc with
fresh_expr gl ~term:false locals e1;
fresh_expr gl ~term (Spv.add vs locals) e2
| Eletrec (fl, e1) ->
List.iter (fun (_, _, _, t, _) -> fresh_triple gl t) fl;
List.iter (fun (_, _, t, _) -> fresh_triple gl t) fl;
fresh_expr gl ~term locals e1
| Eif (e1, e2, e3) ->
......@@ -2195,7 +2199,7 @@ let rec decl ~wp env penv ltm lmod uc = function
let _, dl = dletrec ~ghost:false denv dl in
let _, dl = iletrec uc (create_ienv denv) dl in
let _, dl = letrec uc Mvs.empty dl in
let one uc (v, _, _, _, _ as d) =
let one uc (v, _, _, _ as d) =
let tyv = v.pv_tv in
let loc = loc_of_id v.pv_name in
let id = v.pv_name.id_string in
......
......@@ -376,24 +376,27 @@ let default_exns_post ef =
let xs = Sexn.elements ef.E.raises in
List.map default_exn_post xs
let term_at env lab t =
t_app (find_ls ~pure:true env "at") [t; t_var lab] t.t_ty
let term_at lab t =
t_app fs_at [t; t_var lab] t.t_ty
let wp_expl l f =
t_label ?loc:f.t_loc (("expl:"^l)::Split_goal.stop_split::f.t_label) f
let while_post_block env inv var lab e =
(* 0 <= phi0 and phi < phi0 *)
let default_variant le lt phi phi0 =
t_and
(ps_app le [t_int_const "0"; phi0])
(ps_app lt [phi; phi0])
let while_post_block inv var lab e =
let decphi = match var with
| None ->
t_true
| Some (phi, None) ->
let old_phi = term_at env lab phi in
(* 0 <= old_phi and phi < old_phi *)
wp_and (ps_app (find_ls ~pure:true env "infix <=")
[t_int_const "0"; old_phi])
(ps_app (find_ls ~pure:true env "infix <") [phi; old_phi])
| Some (phi, Some r) ->
ps_app r [phi; term_at env lab phi]
| Some (phi, Vint (le, lt)) ->
let old_phi = term_at lab phi in
default_variant le lt phi old_phi
| Some (phi, Vuser r) ->
ps_app r [phi; term_at lab phi]
in
let decphi = wp_expl "loop variant decreases" decphi in
let ql = default_exns_post e.expr_effect in
......@@ -406,7 +409,7 @@ let while_post_block env inv var lab e =
let well_founded_rel = function
| None -> t_true
| Some (_,_r) -> t_true (* TODO: Papp (well_founded, [Tvar r], []) *)
| Some _ -> t_true (* TODO: Papp (well_founded, [Tvar r], []) *)
(* Recursive computation of the weakest precondition *)
......@@ -487,7 +490,7 @@ and wp_desc env rm e q = match e.expr_desc with
| Eloop ({ loop_invariant = inv; loop_variant = var }, e1) ->
let wfr = well_founded_rel var in
let lab = fresh_label () in
let q1 = while_post_block env inv var lab e1 in
let q1 = while_post_block inv var lab e1 in
let q1 = sup q1 q in (* exc. posts taken from [q] *)
let we = wp_expr env rm e1 q1 in
let we = erase_label lab we in
......@@ -620,7 +623,7 @@ and wp_triple env rm bl (p, e, q) =
let f = wp_close_state env rm e.expr_effect f in
wp_binders bl f
and wp_recfun env rm (_, bl, _var, t, _) =
and wp_recfun env rm (_, bl, t, _) =
wp_triple env rm bl t
let global_regions = ref Mreg.empty
......@@ -634,7 +637,7 @@ let wp env e =
let f = wp_expr env rm e (default_post e.expr_type e.expr_effect) in
wp_close rm e.expr_effect f
let wp_rec env (_,_,_,_,ef as def) =
let wp_rec env (_,_,_,ef as def) =
let rm = !global_regions in
let f = wp_recfun env rm def in
wp_close rm ef f
......
......@@ -18,6 +18,7 @@
(**************************************************************************)
open Why
open Term
val debug : Debug.flag
......@@ -31,3 +32,7 @@ val declare_global_regions : Pgm_types.T.pvsymbol -> unit
val declare_mutable_field : Ty.tysymbol -> int -> int -> unit
(* [declare_mutable_field ts i j] indicates that region [i] in
[ts] args correspond to the mutable field [j] of [ts] *)
val default_variant : lsymbol -> lsymbol -> term -> term -> term
(* [default_variant le lt phi phi0] = 0 <= phi0 and phi < phi0 *)
......@@ -3,13 +3,9 @@ module M
use import int.Int
use import module ref.Ref
type t 'a = {| a: 'a; b: bool; c: 'a |}
let test1 (x: t (ref int)) =
{}
let y = {| x with a = 0; c = 0 |} in
x = y
{ result = True }
let test1 () =
let x = ref 0 in
while !x = 0 do variant { !x } () done
(***
use import option.Option
......
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