Commit 9b35567d authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

Pdecl: do not require the invariant witness to be non-ghost

Certain types are not even intended for the executable code,
and we only need witnesses to ensure logical consistency.
In other words, even if we can only build a ghost witness,
we are still happy.

Thanks to Martin Clochard for this observation. Also, I relieve
him of any responsibility for the current syntax of the witnesses,
apart from the "by" keyword :)
parent 15fc3d65
......@@ -88,13 +88,11 @@ let create_plain_record_decl ~priv ~mut id args fdl invl witn =
[create_constructor ~constr:1 cid s fdl] in
if witn <> [] then begin
List.iter2 (fun fd ({e_loc = loc} as e) ->
Loc.try2 ?loc ity_equal_check e.e_ity fd.pv_ity;
if e.e_effect.eff_oneway then Loc.errorm ?loc
"This expression may not terminate, it cannot be a witness";
if not (eff_pure e.e_effect) then Loc.errorm ?loc
"This expression has side effects, it cannot be a witness";
if not fd.pv_ghost && mask_ghost e.e_mask then Loc.errorm ?loc
"Ghost witness for a non-ghost field %a" print_pv fd) fdl witn
Loc.try2 ?loc ity_equal_check e.e_ity fd.pv_ity) fdl witn
mk_itd s pjl csl invl witn
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