Commit e43c3352 authored by Andrei Paskevich's avatar Andrei Paskevich

Dterm: handle anonymous binders correctly

parent fc3a0752
......@@ -163,6 +163,8 @@ type dbinop =
type dquant =
| DTforall | DTexists | DTlambda
type dbinder = preid option * dty * Loc.position option
type dterm = {
dt_node : dterm_node;
dt_dty : dty option;
......@@ -179,7 +181,7 @@ and dterm_node =
| DTlet of dterm * preid * dterm
| DTcase of dterm * (dpattern * dterm) list
| DTeps of preid * dty * dterm
| DTquant of dquant * (preid * dty) list * dterm list list * dterm
| DTquant of dquant * dbinder list * dterm list list * dterm
| DTbinop of dbinop * dterm * dterm
| DTnot of dterm
| DTtrue
......@@ -214,8 +216,13 @@ let denv_add_let denv dt {pre_name = n} =
Mstr.add n (DTvar (n, dty_of_dterm dt)) denv
let denv_add_quant denv vl =
let add acc ({pre_name = n}, dty) =
Mstr.add_new (DuplicateVar n) n (DTvar (n, dty)) acc in
let add acc (id,dty,_) = match id with
| Some ({pre_name = n} as id) ->
let exn = match id.pre_loc with
| Some loc -> Loc.Located (loc, DuplicateVar n)
| None -> DuplicateVar n in
Mstr.add_new exn n (DTvar (n,dty)) acc
| None -> acc in
let s = List.fold_left add Mstr.empty vl in
Mstr.set_union s denv
......@@ -329,7 +336,7 @@ let dterm ?loc node =
Some dty
| DTquant (DTlambda,vl,_,df) ->
let res = Opt.get_def dty_bool df.dt_dty in
let app (_,l) r = Dapp (ts_func, [l;r]) in
let app (_,l,_) r = Dapp (ts_func,[l;r]) in
Some (List.fold_right app vl res)
| DTquant ((DTforall|DTexists),_,_,df) ->
dfmla_expected_type df;
......@@ -401,13 +408,17 @@ let pattern ~strict env dp =
Mstr.set_union !acc env, pat
let quant_vars ~strict env vl =
let add acc ({pre_name = n} as id, dty) =
let ty = var_ty_of_dty id ~strict dty in
let vs = create_vsymbol id ty in
let exn = match id.pre_loc with
| Some loc -> Loc.Located (loc, DuplicateVar n)
| None -> DuplicateVar n in
Mstr.add_new exn n vs acc, vs in
let add acc (id,dty,loc) = match id with
| Some ({pre_name = n} as id) ->
let ty = var_ty_of_dty id ~strict dty in
let vs = create_vsymbol id ty in
let exn = match id.pre_loc with
| Some loc -> Loc.Located (loc, DuplicateVar n)
| None -> DuplicateVar n in
Mstr.add_new exn n vs acc, vs
| None ->
let ty = Loc.try1 ?loc (pat_ty_of_dty ~strict) dty in
acc, create_vsymbol (id_fresh "_") ty in
let acc, vl = Lists.map_fold_left add Mstr.empty vl in
Mstr.set_union acc env, vl
......
......@@ -44,6 +44,8 @@ type dbinop =
type dquant =
| DTforall | DTexists | DTlambda
type dbinder = preid option * dty * Loc.position option
type dterm = private {
dt_node : dterm_node;
dt_dty : dty option;
......@@ -60,7 +62,7 @@ and dterm_node =
| DTlet of dterm * preid * dterm
| DTcase of dterm * (dpattern * dterm) list
| DTeps of preid * dty * dterm
| DTquant of dquant * (preid * dty) list * dterm list list * dterm
| DTquant of dquant * dbinder list * dterm list list * dterm
| DTbinop of dbinop * dterm * dterm
| DTnot of dterm
| DTtrue
......@@ -84,7 +86,7 @@ val denv_add_var : denv -> preid -> dty -> denv
val denv_add_let : denv -> dterm -> preid -> denv
val denv_add_quant : denv -> (preid * dty) list -> denv
val denv_add_quant : denv -> dbinder list -> denv
val denv_add_pat : denv -> dpattern -> denv
......
......@@ -174,13 +174,10 @@ let rec dpattern uc { pat_desc = desc; pat_loc = loc } =
let quant_var uc (loc, id, gh, ty) =
assert (not gh);
let id = match id with
| Some x -> create_user_id x
| None -> id_user "_" loc in
let ty = match ty with
| Some ty -> dty_of_ty (ty_of_pty uc ty)
| None -> dty_fresh () in
id, ty
Opt.map create_user_id id, ty, Some loc
let is_reusable dt = match dt.dt_node with
| DTvar _ | DTgvar _ | DTconst _ | DTtrue | DTfalse -> true
......@@ -211,8 +208,8 @@ type global_vs = Ptree.qualid -> vsymbol option
let mk_closure loc ls =
let mk dt = Dterm.dterm ~loc dt in
let mk_v i _ =
id_user ("y" ^ string_of_int i) loc, dty_fresh () in
let mk_t (id, dty) = mk (DTvar (id.pre_name, dty)) in
Some (id_user ("y" ^ string_of_int i) loc), dty_fresh (), None in
let mk_t (id, dty, _) = mk (DTvar ((Opt.get id).pre_name, dty)) in
let vl = Lists.mapi mk_v ls.ls_args in
DTquant (DTlambda, vl, [], mk (DTapp (ls, List.map mk_t vl)))
......
......@@ -941,11 +941,11 @@ let check_user_effect ?ps e spec args dsp =
if full_xpost then Sexn.iter check_raise eeff.eff_raises;
if full_xpost then Sexn.iter check_raise eeff.eff_ghostx;
if eeff.eff_diverg && not ueff.eff_diverg then match ps with
| Some {ps_name = {id_label = l}}
when not (Slab.mem lab_w_diverges_no l) ->
Warning.emit ?loc:(e_find_loc (fun e -> e.e_effect.eff_diverg) e)
"this@ expression@ may@ diverge,@ \
which@ is@ not@ stated@ in@ the@ specification"
| Some {ps_name = {id_label = l}}
when not (Slab.mem lab_w_diverges_no l) ->
Warning.emit ?loc:(e_find_loc (fun e -> e.e_effect.eff_diverg) e)
"this@ expression@ may@ diverge,@ \
which@ is@ not@ stated@ in@ the@ specification"
| _ -> ()
let check_lambda_effect ({fun_lambda = lam} as fd) bl dsp =
......
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