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

whyml: error reporting improvements

parent 7fcc7954
module M
use import module stdlib.Ref
use import module ref.Ref
(* reference would escape its scope *)
......
module M
use import module stdlib.Ref
use import module ref.Ref
val r : ref 'a
......
module M
use import module stdlib.Ref
use import module ref.Ref
use import list.List
val r : ref (list 'a)
......
......@@ -96,7 +96,7 @@ syn keyword whyKeyword abstract absurd any assert assume
syn keyword whyKeyword check exception fun ghost
syn keyword whyKeyword invariant model mutable
syn keyword whyKeyword private raise raises reads rec
syn keyword whyKeyword variant while writes
syn keyword whyKeyword val variant while writes
syn keyword whyType bool int list map option real
syn keyword whyType array ref unit
......
......@@ -215,19 +215,6 @@ let clone_export_theory uc th i =
let add_meta uc m al =
{ uc with muc_theory = Theory.add_meta uc.muc_theory m al }
let th_unit =
let ts = create_tysymbol (id_fresh "unit") [] (Some ty_unit) in
let uc = create_theory (id_fresh "Unit") in
let uc = Theory.use_export uc (tuple_theory 0) in
let uc = Theory.add_ty_decl uc ts in
close_theory uc
let create_module ?(path=[]) n =
let m = empty_module n path in
let m = use_export_theory m bool_theory in
let m = use_export_theory m th_unit in
m
(** Program decls *)
let add_symbol add id v uc =
......@@ -291,6 +278,28 @@ let add_pdecl_with_tuples uc d =
let add n uc = use_export_theory uc (tuple_theory n) in
add_pdecl (Sint.fold add ixs uc) d
(* create module *)
let th_unit =
let ts = create_tysymbol (id_fresh "unit") [] (Some ty_unit) in
let uc = create_theory (id_fresh "Unit") in
let uc = Theory.use_export uc (tuple_theory 0) in
let uc = Theory.add_ty_decl uc ts in
close_theory uc
let mod_exit =
let xs = create_xsymbol (id_fresh "%Exit") ity_unit in
let uc = empty_module (id_fresh "Exit") [] in
let uc = add_pdecl uc (create_exn_decl xs) in
close_module uc
let create_module ?(path=[]) n =
let m = empty_module n path in
let m = use_export_theory m bool_theory in
let m = use_export_theory m th_unit in
let m = use_export m mod_exit in
m
(** Clone *)
let clone_export _uc _m _inst =
......
......@@ -106,7 +106,7 @@ let rec print_ity_node inn fmt ity = match ity.ity_node with
and print_regty fmt reg =
if Debug.test_flag debug_print_reg_types then print_reg fmt reg else
fprintf fmt "%a:@,%a" print_reg reg (print_ity_node false) reg.reg_ity
fprintf fmt "@[%a:@,%a@]" print_reg reg (print_ity_node false) reg.reg_ity
let print_ity = print_ity_node false
......@@ -134,14 +134,14 @@ let print_vtv fmt vtv =
fprintf fmt "%s%a" (if vtv.vtv_ghost then "?" else "") print_ity vtv.vtv_ity
let rec print_vta fmt vta =
fprintf fmt "%a@ ->@ %a%a" print_vtv vta.vta_arg
fprintf fmt "%a ->@ %a%a" print_vtv vta.vta_arg
print_effect vta.vta_effect print_vty vta.vta_result
and print_vty fmt = function
| VTarrow vta -> print_vta fmt vta
| VTvalue vtv -> print_vtv fmt vtv
let print_pvty fmt pv = fprintf fmt "%a%a:@,%a"
let print_pvty fmt pv = fprintf fmt "@[%a%a:@,%a@]"
print_pv pv print_reg_opt pv.pv_vtv.vtv_mut print_vtv pv.pv_vtv
let print_psty fmt ps =
......@@ -150,7 +150,7 @@ let print_psty fmt ps =
let print_regs fmt regs = if not (Sreg.is_empty regs) then
fprintf fmt "<%a>@ " (print_list comma print_regty) (Sreg.elements regs) in
let vars = ps.ps_vta.vta_vars in
fprintf fmt "%a :@ %a%a%a"
fprintf fmt "@[%a :@ %a%a%a@]"
print_ps ps
print_tvs (Stv.diff vars.vars_tv ps.ps_vars.vars_tv)
print_regs (Mreg.set_diff vars.vars_reg ps.ps_subst.ity_subst_reg)
......@@ -160,7 +160,7 @@ let print_psty fmt ps =
let print_post fmt post =
let vs,f = open_post post in
fprintf fmt "%a ->@ %a" print_vs vs print_term f;
fprintf fmt "@[%a ->@ %a@]" print_vs vs print_term f;
Pretty.forget_var vs
let print_lv fmt = function
......@@ -174,12 +174,12 @@ let forget_lv = function
let rec print_type_v fmt = function
| SpecV vtv -> print_vtv fmt vtv
| SpecA (pvl,tyc) ->
let print_arg fmt pv = fprintf fmt "(%a) ->@ " print_pvty pv in
let print_arg fmt pv = fprintf fmt "@[(%a)@] ->@ " print_pvty pv in
fprintf fmt "%a%a" (print_list nothing print_arg) pvl print_type_c tyc;
List.iter forget_pv pvl
and print_type_c fmt tyc =
fprintf fmt "{ %a }@ %a%a@ { %a }@]"
fprintf fmt "{ %a }@ %a%a@ { %a }"
print_term tyc.c_pre
print_effect tyc.c_effect
print_type_v tyc.c_result
......@@ -295,7 +295,7 @@ and print_enode pri fmt e = match e.e_node with
fprintf fmt "loop@ %a%a@\n@[<hov>%a@]@\nend"
print_invariant inv print_variant var print_expr e
| Efor (pv,(pvfrom,dir,pvto),inv,e) ->
fprintf fmt "@[<hov 2>for@ %a@ =@ %a@ %s@ %a@ %ado@\n%a@]@\ndone"
fprintf fmt "@[<hov 2>for@ %a =@ %a@ %s@ %a@ %ado@\n%a@]@\ndone"
print_pv pv print_pv pvfrom
(if dir = To then "to" else "downto") print_pv pvto
print_invariant inv print_expr e
......@@ -325,8 +325,8 @@ and print_xbranch fmt (xs, pv, e) =
forget_pv pv
and print_rec fst fmt { rec_ps = ps ; rec_lambda = lam } =
let print_arg fmt pv = fprintf fmt "(%a)" print_pvty pv in
fprintf fmt "@[<hov 2>%s (%a) %a =@\n{ %a }@\n%a%a@\n{ %a }@]"
let print_arg fmt pv = fprintf fmt "@[(%a)@]" print_pvty pv in
fprintf fmt "@[<hov 2>%s (%a)@ %a =@\n{ %a }@\n%a%a@\n{ %a }@]"
(if fst then "let rec" else "with")
print_psty ps
(print_list space print_arg) lam.l_args
......
......@@ -134,7 +134,12 @@ let dity_unit = ts_app ts_unit []
let dity_mark = ts_app ts_mark []
let expected_type ?(weak=false) e dity =
unify ~weak e.de_type dity
try unify ~weak e.de_type dity with
| TypeMismatch (ity1,ity2) ->
errorm ~loc:e.de_loc "This expression has type %a, \
but is expected to have type %a"
Mlw_pretty.print_ity ity1 Mlw_pretty.print_ity ity2
| exn -> error ~loc:e.de_loc exn
let rec extract_labels labs loc e = match e.Ptree.expr_desc with
| Ptree.Enamed (Ptree.Lstr s, e) -> extract_labels (Slab.add s labs) loc e
......@@ -321,7 +326,10 @@ and dpat_app denv ({ de_loc = loc } as de) ppl =
(* specifications *)
let dbinders denv bl =
let hv = Hashtbl.create 3 in
let dbinder (id,gh,pty) (denv,bl,tyl) =
if Hashtbl.mem hv id.id then errorm "duplicate argument %s" id.id;
Hashtbl.add hv id.id ();
let dity = match pty with
| Some pty -> dity_of_pty ~user:true denv pty
| None -> create_type_variable () in
......@@ -654,15 +662,20 @@ let rec get_eff_expr lenv { pp_desc = d; pp_loc = loc } = match d with
| PV pv -> e_value pv
| _ -> errorm ~loc:(qloc p) "%a is not a variable" print_qualid p
with Not_found -> errorm ~loc "unbound variable %a" print_qualid p end
| Ptree.PPapp (p, [e]) ->
let e = get_eff_expr lenv e in
| Ptree.PPapp (p, [le]) ->
let e = get_eff_expr lenv le in
let ity = (vtv_of_expr e).vtv_ity in
let x = Typing.string_list_of_qualid [] p in
let quit () =
errorm ~loc:(qloc p) "%a is not a projection symbol" print_qualid p in
begin try match ns_find_ps (get_namespace lenv.mod_uc) x with
| PL ({pl_args = [{vtv_ity = ta}]; pl_value = {vtv_ity = tr}} as pl) ->
let sbs = ity_match ity_subst_empty ta ity in
let sbs = try ity_match ity_subst_empty ta ity with
| TypeMismatch (ity1,ity2) ->
errorm ~loc:le.pp_loc "This expression has type %a, \
but is expected to have type %a"
Mlw_pretty.print_ity ity2 Mlw_pretty.print_ity ity1
| exn -> error ~loc:le.pp_loc exn in
let res = try ity_full_inst sbs tr with Not_found -> quit () in
e_plapp pl [e] res
| _ -> quit ()
......
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