Commit e372532f authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

whyml: forbid lsymbols defined on impure types in programs

parent cee844be
......@@ -292,6 +292,12 @@ let specialize_plsymbol pls =
List.map conv pls.pl_args, conv pls.pl_value
let dity_of_ty htv hreg vars ty =
let rec pure ty = match ty.ty_node with
| Tyapp (ts,tl) ->
begin try ignore (restore_its ts); false
with Not_found -> List.for_all pure tl end
| Tyvar _ -> true in
if not (pure ty) then raise Exit;
dity_of_ity htv hreg vars (ity_of_ty ty)
let specialize_lsymbol ls =
......@@ -300,6 +306,11 @@ let specialize_lsymbol ls =
let ty = Opt.get_def ty_bool ls.ls_value in
List.map conv ls.ls_args, conv ty
let specialize_lsymbol ls =
try specialize_lsymbol ls with Exit ->
Loc.errorm "Function symbol `%a' can only be used in specification"
Pretty.print_ls ls
(* Pretty-printing *)
let debug_print_reg_types = Debug.register_info_flag "print_reg_types"
......
......@@ -89,6 +89,9 @@ val create_itysymbol :
preid -> ?abst:bool -> ?priv:bool -> ?inv:bool ->
tvsymbol list -> region list -> ity option -> itysymbol
val restore_its : tysymbol -> itysymbol
(* raises Not_found if the argument is not a its_ts *)
val ity_var : tvsymbol -> ity
val ity_pur : tysymbol -> ity list -> ity
......
......@@ -248,7 +248,7 @@ let hidden_pl ~loc pl =
let hidden_ls ~loc ls =
{ de_desc = DEglobal_ls ls;
de_type = specialize_lsymbol ls;
de_type = Loc.try1 loc specialize_lsymbol ls;
de_loc = loc; de_lab = Slab.empty }
(* helper functions for let-expansion *)
......@@ -286,7 +286,7 @@ let specialize_qualid uc p = match uc_find_ps uc p with
| PV pv -> DEglobal_pv pv, ([],specialize_pvsymbol pv)
| PS ps -> DEglobal_ps ps, specialize_psymbol ps
| PL pl -> DEglobal_pl pl, specialize_plsymbol pl
| LS ls -> DEglobal_ls ls, specialize_lsymbol ls
| LS ls -> DEglobal_ls ls, Loc.try1 (qloc p) specialize_lsymbol ls
| XS xs -> errorm ~loc:(qloc p) "unexpected exception symbol %a" print_xs xs
let find_xsymbol uc p = match uc_find_ps uc p with
......
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