Commit ceabae7e authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: check for runaway typevars in toplevel declarations

parent 6f6a574e
......@@ -125,11 +125,16 @@ let create_data_decl tdl =
let tdl = List.map build_type tdl in
mk_decl (PDdata tdl) !syms !news
let check_vars vars =
if not (Stv.is_empty vars.vars_tv) then
raise (UnboundTypeVar (Stv.choose vars.vars_tv))
let letvar_news = function
| LetV pv -> check_vars pv.pv_vtv.vtv_vars; Sid.singleton pv.pv_vs.vs_name
| LetA ps -> check_vars ps.ps_vars; Sid.singleton ps.ps_name
let create_let_decl ld =
let id = match ld.let_var with
| LetV pv -> pv.pv_vs.vs_name
| LetA ps -> ps.ps_name in
let news = Sid.singleton id in
let news = letvar_news ld.let_var in
(* FIXME!!! This is not a correct way of counting symbols,
since it ignores type symbols and exception symbols, and
lsymbols inside specifications. We should either extend
......@@ -141,7 +146,7 @@ let create_let_decl ld =
let create_rec_decl rdl =
if rdl = [] then raise Decl.EmptyDecl;
let add_rd s rd = news_id s rd.rec_ps.ps_name in
let add_rd s { rec_ps = p } = check_vars p.ps_vars; news_id s p.ps_name in
let news = List.fold_left add_rd Sid.empty rdl in
let add_rd s rd = Sid.union s (Mid.map (fun _ -> ()) rd.rec_vars) in
(* FIXME!!! See the comment in create_let_decl *)
......@@ -149,10 +154,7 @@ let create_rec_decl rdl =
mk_decl (PDrec rdl) syms news
let create_val_decl vd =
let id = match vd.val_name with
| LetV pv -> pv.pv_vs.vs_name
| LetA ps -> ps.ps_name in
let news = Sid.singleton id in
let news = letvar_news vd.val_name in
(* FIXME!!! See the comment in create_let_decl *)
let syms = Mid.map (fun _ -> ()) vd.val_vars in
mk_decl (PDval vd) syms news
......
......@@ -1398,32 +1398,32 @@ let add_module lib path mm mt m =
let pd = match e.de_desc with
| DEfun lam ->
let def = expr_fun (create_lenv uc) id gh lam in
create_rec_decl [def]
Loc.try1 loc create_rec_decl [def]
| _ ->
let e = e_ghostify gh (expr (create_lenv uc) e) in
if not gh && vty_ghost e.e_vty then
errorm ~loc "%s must be a ghost variable" id.id;
let def = create_let_defn (Denv.create_user_id id) e in
create_let_decl def
Loc.try1 loc create_let_decl def
in
Loc.try2 loc add_pdecl_with_tuples uc pd
| Dletrec rdl ->
let rdl = dletrec (create_denv uc) rdl in
let rdl = expr_rec (create_lenv uc) rdl in
let pd = create_rec_decl rdl in
let pd = Loc.try1 loc create_rec_decl rdl in
Loc.try2 loc add_pdecl_with_tuples uc pd
| Dexn (id, pty) ->
let ity = match pty with
| Some pty ->
ity_of_dity (dity_of_pty ~user:false (create_denv uc) pty)
| None -> ity_unit in
let xs = create_xsymbol (Denv.create_user_id id) ity in
let pd = create_exn_decl xs in
let xs = Loc.try2 loc create_xsymbol (Denv.create_user_id id) ity in
let pd = Loc.try1 loc create_exn_decl xs in
Loc.try2 loc add_pdecl_with_tuples uc pd
| Dparam (id, gh, tyv) ->
let tyv, _ = dtype_v (create_denv uc) tyv in
let tyv = type_v (create_lenv uc) gh vars_empty tyv in
let vd = create_val (Denv.create_user_id id) tyv in
let vd = Loc.try2 loc create_val (Denv.create_user_id id) tyv in
begin match vd.val_name with
| LetA { ps_vta = { vta_ghost = true }} when not gh ->
errorm ~loc "%s must be a ghost function" id.id
......@@ -1431,7 +1431,7 @@ let add_module lib path mm mt m =
errorm ~loc "%s must be a ghost variable" id.id
| _ -> ()
end;
let pd = create_val_decl vd in
let pd = Loc.try1 loc create_val_decl vd in
Loc.try2 loc add_pdecl_with_tuples uc pd
(* TODO: this is made obsolete by Duseclone, remove later *)
| Duse (qid, use_imp_exp, use_as) ->
......
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