Commit 0ef05cfc authored by Andrei Paskevich's avatar Andrei Paskevich

pretty-print arrow types + warnings in Mlw_dexpr

parent 07d793f0
......@@ -73,37 +73,40 @@ let rec dty_unify dty1 dty2 = match dty1,dty2 with
List.iter2 dty_unify dl1 dl2
| _ -> raise Exit
let dty_int = Duty ty_int
let dty_int = Duty ty_int
let dty_real = Duty ty_real
let dty_bool = Duty ty_bool
let rec print_dty ht inn fmt = function
let protect_on x s = if x then "(" ^^ s ^^ ")" else s
let rec print_dty ht pri fmt = function
| Dvar { contents = Dval dty } ->
print_dty ht inn fmt dty
print_dty ht pri fmt dty
| Dvar { contents = Dind i } ->
let tv = try Hint.find ht i with Not_found ->
let tv = create_tvsymbol (id_fresh "xi") in
Hint.replace ht i tv; tv in
Pretty.print_tv fmt tv
| Dapp (ts,[d1;d2]) when ts_equal ts Ty.ts_func ->
Format.fprintf fmt (protect_on (pri > 0) "%a@ ->@ %a")
(print_dty ht 1) d1 (print_dty ht 0) d2
| Dapp (ts,dl) when is_ts_tuple ts ->
Format.fprintf fmt "(%a)"
(Pp.print_list Pp.comma (print_dty ht false)) dl
(Pp.print_list Pp.comma (print_dty ht 0)) dl
| Dapp (ts,[]) ->
Pretty.print_ts fmt ts
| Dapp (ts,dl) when inn ->
Format.fprintf fmt "(%a@ %a)"
Pretty.print_ts ts (Pp.print_list Pp.space (print_dty ht true)) dl
| Dapp (ts,dl) ->
Format.fprintf fmt "%a@ %a"
Pretty.print_ts ts (Pp.print_list Pp.space (print_dty ht true)) dl
Format.fprintf fmt (protect_on (pri > 1) "%a@ %a")
Pretty.print_ts ts (Pp.print_list Pp.space (print_dty ht 2)) dl
| Duty ({ty_node = Tyapp (ts,(_::_))} as ty)
when inn && not (is_ts_tuple ts) ->
when (pri > 1 && not (is_ts_tuple ts))
|| (pri = 1 && ts_equal ts Ty.ts_func) ->
Format.fprintf fmt "(%a)" Pretty.print_ty ty
| Duty ty ->
Pretty.print_ty fmt ty
let print_dty = let ht = Hint.create 3 in fun fmt dty ->
print_dty ht false fmt dty
print_dty ht 0 fmt dty
(** Symbols *)
......@@ -285,11 +288,19 @@ let dterm ?loc node =
let dtyl, dty = specialize_ls ls in
dty_unify_app ls dterm_expected_type dtl dtyl;
dty
| DTfapp (dt1,dt2) ->
| DTfapp ({dt_dty = Some res} as dt1,dt2) ->
let rec not_arrow = function
| Dvar {contents = Dval dty} -> not_arrow dty
| Duty {ty_node = Tyapp (ts,_)}
| Dapp (ts,_) -> not (ts_equal ts Ty.ts_func)
| Dvar _ -> false | _ -> true in
if not_arrow res then Loc.errorm ?loc:dt1.dt_loc
"This term has type %a,@ it cannot be applied" print_dty res;
let dtyl, dty = specialize_ls fs_func_app in
(* TODO: better error messages based on dt1 *)
dty_unify_app fs_func_app dterm_expected_type [dt1;dt2] dtyl;
dty
| DTfapp ({dt_dty = None; dt_loc = loc},_) ->
Loc.errorm ?loc "This term has type bool,@ it cannot be applied"
| DTif (df,dt1,dt2) ->
dfmla_expected_type df;
dexpr_expected_type dt2 dt1.dt_dty;
......
......@@ -119,15 +119,18 @@ let print_pr fmt pr =
let protect_on x s = if x then "(" ^^ s ^^ ")" else s
let rec print_ty_node inn fmt ty = match ty.ty_node with
let rec print_ty_node pri fmt ty = match ty.ty_node with
| Tyvar v -> print_tv fmt v
| Tyapp (ts, tl) when is_ts_tuple ts -> fprintf fmt "(%a)"
(print_list comma (print_ty_node false)) tl
| Tyapp (ts, [t1;t2]) when ts_equal ts Ty.ts_func ->
fprintf fmt (protect_on (pri > 0) "%a@ ->@ %a")
(print_ty_node 1) t1 (print_ty_node 0) t2
| Tyapp (ts, tl) when is_ts_tuple ts ->
fprintf fmt "(%a)" (print_list comma (print_ty_node 0)) tl
| Tyapp (ts, []) -> print_ts fmt ts
| Tyapp (ts, tl) -> fprintf fmt (protect_on inn "%a@ %a")
print_ts ts (print_list space (print_ty_node true)) tl
| Tyapp (ts, tl) -> fprintf fmt (protect_on (pri > 1) "%a@ %a")
print_ts ts (print_list space (print_ty_node 2)) tl
let print_ty = print_ty_node false
let print_ty fmt ty = print_ty_node 0 fmt ty
let print_const fmt = function
| ConstInt (IConstDec s) -> fprintf fmt "%s" s
......@@ -292,7 +295,7 @@ and print_tl fmt tl =
(** Declarations *)
let print_tv_arg fmt tv = fprintf fmt "@ %a" print_tv tv
let print_ty_arg fmt ty = fprintf fmt "@ %a" (print_ty_node true) ty
let print_ty_arg fmt ty = fprintf fmt "@ %a" (print_ty_node 2) ty
let print_vs_arg fmt vs = fprintf fmt "@ (%a)" print_vsty vs
let print_constr fmt (cs,pjl) =
......@@ -500,9 +503,10 @@ let () = Exn_printer.register
| Ty.TypeMismatch (t1,t2) ->
fprintf fmt "Type mismatch between %a and %a"
print_ty t1 print_ty t2
| Ty.BadTypeArity ({ts_args = []} as ts, _) ->
fprintf fmt "Type symbol %a expects no arguments" print_ts ts
| Ty.BadTypeArity (ts, app_arg) ->
fprintf fmt "Bad type arity: type symbol %a must be applied \
to %i arguments, but is applied to %i"
fprintf fmt "Type symbol %a expects %i arguments but is applied to %i"
print_ts ts (List.length ts.ts_args) app_arg
| Ty.DuplicateTypeVar tv ->
fprintf fmt "Type variable %a is used twice" print_tv tv
......@@ -510,9 +514,12 @@ let () = Exn_printer.register
fprintf fmt "Unbound type variable: %a" print_tv tv
| Ty.UnexpectedProp ->
fprintf fmt "Unexpected propositional type"
| Term.BadArity ({ls_args = []} as ls, _) ->
fprintf fmt "%s %a expects no arguments"
(if ls.ls_value = None then "Predicate" else "Function") print_ls ls
| Term.BadArity (ls, app_arg) ->
fprintf fmt "Bad arity: symbol %a must be applied \
to %i arguments, but is applied to %i"
fprintf fmt "%s %a expects %i arguments but is applied to %i"
(if ls.ls_value = None then "Predicate" else "Function")
print_ls ls (List.length ls.ls_args) app_arg
| Term.EmptyCase ->
fprintf fmt "Empty match expression"
......@@ -525,20 +532,21 @@ let () = Exn_printer.register
| Term.PredicateSymbolExpected ls ->
fprintf fmt "Not a predicate symbol: %a" print_ls ls
| Term.ConstructorExpected ls ->
fprintf fmt "Symbol %a is not a constructor"
print_ls ls
fprintf fmt "%s %a is not a constructor"
(if ls.ls_value = None then "Predicate" else "Function") print_ls ls
| Term.TermExpected t ->
fprintf fmt "Not a term: %a" print_term t
| Term.FmlaExpected t ->
fprintf fmt "Not a formula: %a" print_term t
| Pattern.ConstructorExpected (ls,ty) ->
fprintf fmt "Symbol %a is not a constructor of type %a"
print_ls ls print_ty ty
fprintf fmt "%s %a is not a constructor of type %a"
(if ls.ls_value = None then "Predicate" else "Function") print_ls ls
print_ty ty
| Pattern.NonExhaustive pl ->
fprintf fmt "Pattern not covered by a match:@\n @[%a@]"
print_pat (List.hd pl)
| Decl.BadConstructor ls ->
fprintf fmt "Bad constructor symbol: %a" print_ls ls
fprintf fmt "Bad constructor: %a" print_ls ls
| Decl.BadRecordField ls ->
fprintf fmt "Not a record field: %a" print_ls ls
| Decl.RecordFieldMissing (_cs,ls) ->
......
......@@ -210,20 +210,23 @@ let print_dity fmt dity =
let protect_on x s = if x then "(" ^^ s ^^ ")" else s in
let print_rtvs fmt tv = Mlw_pretty.print_reg fmt
(create_region (id_clone tv.tv_name) Mlw_ty.ity_unit) in
let rec print_dity inn fmt = function
let rec print_dity pri fmt = function
| Dvar { contents = Dtvs tv }
| Dutv tv -> Pretty.print_tv fmt tv
| Dvar { contents = Dval dty } -> print_dity inn fmt dty
| Dvar { contents = Dval dty } -> print_dity pri fmt dty
| Dpur (s,[t1;t2]) when ts_equal s Ty.ts_func ->
Format.fprintf fmt (protect_on (pri > 0) "%a@ ->@ %a")
(print_dity 1) t1 (print_dity 0) t2
| Dpur (s,tl) when is_ts_tuple s -> Format.fprintf fmt "(%a)"
(Pp.print_list Pp.comma (print_dity false)) tl
(Pp.print_list Pp.comma (print_dity 0)) tl
| Dpur (s,[]) -> Pretty.print_ts fmt s
| Dpur (s,tl) -> Format.fprintf fmt (protect_on inn "%a@ %a")
Pretty.print_ts s (Pp.print_list Pp.space (print_dity true)) tl
| Dapp (s,[],rl) -> Format.fprintf fmt (protect_on inn "%a@ <%a>")
| Dpur (s,tl) -> Format.fprintf fmt (protect_on (pri > 1) "%a@ %a")
Pretty.print_ts s (Pp.print_list Pp.space (print_dity 2)) tl
| Dapp (s,[],rl) -> Format.fprintf fmt (protect_on (pri > 1) "%a@ <%a>")
Mlw_pretty.print_its s (Pp.print_list Pp.comma print_dreg) rl
| Dapp (s,tl,rl) -> Format.fprintf fmt (protect_on inn "%a@ <%a>@ %a")
| Dapp (s,tl,rl) -> Format.fprintf fmt (protect_on (pri > 1) "%a@ <%a>@ %a")
Mlw_pretty.print_its s (Pp.print_list Pp.comma print_dreg) rl
(Pp.print_list Pp.space (print_dity true)) tl
(Pp.print_list Pp.space (print_dity 2)) tl
and print_dreg fmt = function
| Rreg (r,_) when Debug.test_flag debug_print_reg_types ->
Format.fprintf fmt "@[%a:@,%a@]" Mlw_pretty.print_reg r
......@@ -231,11 +234,11 @@ let print_dity fmt dity =
| Rreg (r,_) -> Mlw_pretty.print_reg fmt r
| Rvar { contents = Rtvs (tv,dity) }
when Debug.test_flag debug_print_reg_types ->
Format.fprintf fmt "@[%a:@,%a@]" print_rtvs tv (print_dity false) dity
Format.fprintf fmt "@[%a:@,%a@]" print_rtvs tv (print_dity 0) dity
| Rvar { contents = Rtvs (tv,_) } -> print_rtvs fmt tv
| Rvar { contents = Rval dreg } -> print_dreg fmt dreg
in
print_dity false fmt dity
print_dity 0 fmt dity
(* Specialization of symbols *)
......@@ -652,7 +655,13 @@ let dexpr ?loc node =
| DEapply ({de_dvty = (dity::argl, res)}, de2) ->
dexpr_expected_type de2 dity;
argl, res
| DEapply (de1, de2) -> (* TODO: better error messages *)
| DEapply ({de_dvty = ([],res)} as de1, de2) ->
let rec not_arrow = function
| Dvar {contents = Dval dity} -> not_arrow dity
| Dpur (ts,_) -> not (ts_equal ts Ty.ts_func)
| Dvar _ -> false | _ -> true in
if not_arrow res then Loc.errorm ?loc:de1.de_loc
"This expression has type %a,@ it cannot be applied" print_dity res;
let argl, res = specialize_ls fs_func_app in
dity_unify_app fs_func_app dexpr_expected_type [de1;de2] argl;
[], res
......@@ -1051,6 +1060,16 @@ let spec_invariant env pvs vty spec =
(** Abstract values *)
let warn_unused s loc =
if not (String.length s > 0 && s.[0] = '_') then
Warning.emit ?loc "unused variable %s" s
let check_used_pv e pv = if not (Spv.mem pv e.e_syms.syms_pv) then
warn_unused pv.pv_vs.vs_name.id_string pv.pv_vs.vs_name.id_loc
let check_used_ps e ps = if not (Sps.mem ps e.e_syms.syms_ps) then
warn_unused ps.ps_name.id_string ps.ps_name.id_loc
let rec type_c env pvs vars otv (dtyv, dsp) =
let vty = type_v env pvs vars otv dtyv in
let res = ty_of_vty vty in
......@@ -1161,6 +1180,10 @@ and try_expr keep_loc uloc env ({de_dvty = argl,res} as de0) =
let e2_unit = match e2.e_vty with
| VTvalue ity -> ity_equal ity ity_unit
| _ -> false in
let id_in_e2 = match ld1.let_sym with
| LetV pv -> Spv.mem pv e2.e_syms.syms_pv
| LetA ps -> Sps.mem ps e2.e_syms.syms_ps in
if not id_in_e2 then warn_unused id.pre_name id.pre_loc;
let e1_no_eff =
Sreg.is_empty e1.e_effect.eff_writes &&
Sexn.is_empty e1.e_effect.eff_raises &&
......@@ -1168,9 +1191,7 @@ and try_expr keep_loc uloc env ({de_dvty = argl,res} as de0) =
(* if e1 is a recursive call, we may not know yet its effects,
so we have to rely on an heuristic: if the result of e1 is
not used in e2, then it was probably called for the effect. *)
match ld1.let_sym with
| LetV pv -> Spv.mem pv e2.e_syms.syms_pv
| LetA ps -> Sps.mem ps e2.e_syms.syms_ps
id_in_e2
in
let e2 =
if e2_unit (* e2 is unit *)
......@@ -1202,7 +1223,9 @@ and try_expr keep_loc uloc env ({de_dvty = argl,res} as de0) =
let ghost = e1.e_ghost in
let branch (dp,de) =
let vm, pat = make_ppattern dp.dp_pat ~ghost ity in
pat, get (add_pv_map env vm) de in
let e = get (add_pv_map env vm) de in
Mstr.iter (fun _ pv -> check_used_pv e pv) vm;
pat, e in
e_case e1 (List.map branch bl)
| DEassign (pl,de1,de2) ->
e_assign pl (get env de1) (get env de2)
......@@ -1223,6 +1246,7 @@ and try_expr keep_loc uloc env ({de_dvty = argl,res} as de0) =
let add_branch (m,l) (xs,dp,de) =
let vm, pat = make_ppattern dp.dp_pat xs.xs_ity in
let e = get (add_pv_map env vm) de in
Mstr.iter (fun _ pv -> check_used_pv e pv) vm;
try Mexn.add xs ((pat,e) :: Mexn.find xs m) m, l
with Not_found -> Mexn.add xs [pat,e] m, (xs::l) in
let xsm, xsl = List.fold_left add_branch (Mexn.empty,[]) bl in
......@@ -1293,6 +1317,7 @@ and try_expr keep_loc uloc env ({de_dvty = argl,res} as de0) =
| DEfun (fd,de) ->
let fd = expr_fun ~keep_loc ~strict:true uloc env fd in
let e = get (add_fundef env fd) de in
check_used_ps e fd.fun_ps;
e_rec [fd] e
| DElam (bl,de,sp) ->
let fd = id_fresh "fn", false, bl, de, sp in
......
......@@ -79,30 +79,33 @@ let print_its fmt ts = print_ts fmt ts.its_ts
let protect_on x s = if x then "(" ^^ s ^^ ")" else s
let rec print_ity_node s inn fmt ity = match ity.ity_node with
let rec print_ity_node s pri fmt ity = match ity.ity_node with
| Ityvar v ->
begin match Mtv.find_opt v s.ity_subst_tv with
| Some ity -> print_ity_node ity_subst_empty inn fmt ity
| Some ity -> print_ity_node ity_subst_empty pri fmt ity
| None -> print_tv fmt v
end
| Itypur (ts,[t1;t2]) when ts_equal ts Ty.ts_func ->
fprintf fmt (protect_on (pri > 0) "%a@ ->@ %a")
(print_ity_node s 1) t1 (print_ity_node s 0) t2
| Itypur (ts,tl) when is_ts_tuple ts -> fprintf fmt "(%a)"
(print_list comma (print_ity_node s false)) tl
(print_list comma (print_ity_node s 0)) tl
| Itypur (ts,[]) -> print_ts fmt ts
| Itypur (ts,tl) -> fprintf fmt (protect_on inn "%a@ %a")
print_ts ts (print_list space (print_ity_node s true)) tl
| Ityapp (ts,[],rl) -> fprintf fmt (protect_on inn "%a@ <%a>")
| Itypur (ts,tl) -> fprintf fmt (protect_on (pri > 1) "%a@ %a")
print_ts ts (print_list space (print_ity_node s 2)) tl
| Ityapp (ts,[],rl) -> fprintf fmt (protect_on (pri > 1) "%a@ <%a>")
print_its ts (print_list comma print_regty)
(List.map (fun r -> Mreg.find_def r r s.ity_subst_reg) rl)
| Ityapp (ts,tl,rl) -> fprintf fmt (protect_on inn "%a@ <%a>@ %a")
| Ityapp (ts,tl,rl) -> fprintf fmt (protect_on (pri > 1) "%a@ <%a>@ %a")
print_its ts (print_list comma print_regty)
(List.map (fun r -> Mreg.find_def r r s.ity_subst_reg) rl)
(print_list space (print_ity_node s true)) tl
(print_list space (print_ity_node s 2)) tl
and print_regty fmt reg =
if Debug.test_noflag debug_print_reg_types then print_reg fmt reg
else fprintf fmt "@[%a:@,%a@]" print_reg reg print_ity reg.reg_ity
and print_ity fmt ity = print_ity_node ity_subst_empty false fmt ity
and print_ity fmt ity = print_ity_node ity_subst_empty 2 fmt ity
let print_reg_opt fmt = function
| Some r -> fprintf fmt "<%a>" print_regty r
......@@ -342,7 +345,7 @@ and print_tl fmt tl =
let print_tv_arg fmt tv = fprintf fmt "@ %a" print_tv tv
let print_ty_arg fmt ty =
fprintf fmt "@ %a" (print_ity_node ity_subst_empty true) ty
fprintf fmt "@ %a" (print_ity_node ity_subst_empty 2) ty
let print_constr fmt (cs,pjl) =
let print_pj fmt (fd,pj) = match pj with
......@@ -426,13 +429,14 @@ let print_pdecl fmt d = match d.pd_node with
let () = Exn_printer.register
begin fun fmt exn -> match exn with
| Mlw_ty.BadItyArity ({its_ts = {ts_args = []}} as ts, _) ->
fprintf fmt "Type symbol %a expects no arguments" print_its ts
| Mlw_ty.BadItyArity (ts, app_arg) ->
fprintf fmt "Bad type arity: type symbol %a must be applied \
to %i arguments, but is applied to %i"
fprintf fmt "Type symbol %a expects %i arguments but is applied to %i"
print_its ts (List.length ts.its_ts.ts_args) app_arg
| Mlw_ty.BadRegArity (ts, app_arg) ->
fprintf fmt "Bad region arity: type symbol %a must be applied \
to %i regions, but is applied to %i"
fprintf fmt "Type symbol %a expects \
%i region arguments but is applied to %i"
print_its ts (List.length ts.its_regs) app_arg
| Mlw_ty.DuplicateRegion r ->
fprintf fmt "Region %a is used twice" print_reg r
......@@ -447,7 +451,7 @@ let () = Exn_printer.register
print_regty r1 print_regty r2
| Mlw_ty.TypeMismatch (t1,t2,s) ->
fprintf fmt "Type mismatch between %a and %a"
(print_ity_node s false) t1 print_ity t2
(print_ity_node s 0) t1 print_ity t2
| Mlw_ty.PolymorphicException (id,_ity) ->
fprintf fmt "Exception %s has a polymorphic type" id.id_string
| Mlw_ty.MutableException (id,_ity) ->
......
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