Commit 38491aaa authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: some typechecking fixes

parent ceabae7e
......@@ -205,7 +205,15 @@ let make_arrow_type tyl ty =
List.fold_right arrow tyl ty
let rec unify_list d1 el res =
let unify_loc loc d1 d2 = try unify d1 d2 with
let rec check_val loc = function
| Dts (ts, _) when ts_equal ts ts_arrow ->
Loc.errorm ~loc "This expression is not a first-order value"
| Dvar { contents = Dval d } -> check_val loc d
| _ -> ()
in
let unify_loc loc d1 d2 =
check_val loc d2;
try unify d1 d2 with
| TypeMismatch (ity1, ity2) ->
Loc.errorm ~loc "This expression has type %a, \
but is expected to have type %a"
......
......@@ -307,7 +307,7 @@ and print_enode pri fmt e = match e.e_node with
| Eabsurd ->
fprintf fmt "absurd"
| Eassert (ak,f) ->
fprintf fmt "%a@ { %a }" print_ak ak print_term f
fprintf fmt "%a { %a }" print_ak ak print_term f
| Eabstr (e,q,_xq) ->
(* TODO: print_xpost *)
fprintf fmt "abstract %a@ { %a }" print_expr e print_post q
......@@ -388,17 +388,17 @@ let print_ty_decl fmt ts =
print_ty_decl fmt ts; forget_tvs_regs ()
let print_data_decl fst fmt (ts,csl) =
fprintf fmt "@[<hov 2>%a =@\n@[<hov>%a@]@]"
fprintf fmt "@[<hov 2>%a =@ %a@]"
(print_head fst) ts (print_list newline print_constr) csl;
forget_tvs_regs ()
let print_val_decl fmt { val_name = lv ; val_spec = tyv } =
fprintf fmt "@[<hov 2>val (%a) : @[%a@]@]" print_lv lv print_type_v tyv;
fprintf fmt "@[<hov 2>val (%a) :@ %a@]" print_lv lv print_type_v tyv;
(* FIXME: don't forget global regions *)
forget_tvs_regs ()
let print_let_decl fmt { let_var = lv ; let_expr = e } =
fprintf fmt "@[<hov 2>let %a = @[%a@]@]" print_lv lv print_expr e;
fprintf fmt "@[<hov 2>let %a =@ %a@]" print_lv lv print_expr e;
(* FIXME: don't forget global regions *)
forget_tvs_regs ()
......
......@@ -537,7 +537,9 @@ and de_desc denv loc = function
let id, denv = match id with
| Some id -> id, add_var id dity denv
| None -> mk_id "void" loc, denv in
xs, id, dexpr denv e
let e = dexpr denv e in
expected_type e e1.de_type;
xs, id, e
in
let cl = List.map branch cl in
DEtry (e1, cl), e1.de_type
......@@ -610,10 +612,8 @@ let create_lenv uc = {
}
let rec dty_of_ty ty = match ty.ty_node with
| Ty.Tyvar v ->
Typing.create_user_type_var v.tv_name.id_string
| Ty.Tyapp (ts, tyl) ->
Denv.tyapp ts (List.map dty_of_ty tyl)
| Ty.Tyapp (ts, tyl) -> Denv.tyapp ts (List.map dty_of_ty tyl)
| Ty.Tyvar v -> Denv.tyuvar v
let create_post lenv x ty f =
let res = create_vsymbol (id_fresh x) ty in
......@@ -820,10 +820,8 @@ and expr_desc lenv loc de = match de.de_desc with
| DEglobal_ps ps ->
e_cast ps (vty_of_dity de.de_type)
| DEglobal_pl pl ->
assert (pl.pl_ls.ls_args = []);
e_plapp pl [] (ity_of_dity de.de_type)
| DEglobal_ls ls ->
assert (ls.ls_args = []);
e_lapp ls [] (ity_of_dity de.de_type)
| DEif (de1, de2, de3) ->
e_if (expr lenv de1) (expr lenv de2) (expr lenv de3)
......
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