Fix typing

This commit is contained in:
Louis Gesbert 2022-09-26 18:19:39 +02:00
parent 6701b0760d
commit 3b4b070aaa
3 changed files with 9 additions and 9 deletions

View File

@ -89,7 +89,8 @@ let type_rule decl_ctx env = function
let expr' = Typing.expr decl_ctx ~env ~typ expr in
Definition (loc, typ, io, Bindlib.unbox expr')
| Assertion expr ->
let expr' = Typing.expr decl_ctx ~env expr in
let typ = Marked.mark (Expr.pos expr) (TLit TBool) in
let expr' = Typing.expr decl_ctx ~env ~typ expr in
Assertion (Bindlib.unbox expr')
| Call (sc_name, ssc_name) -> Call (sc_name, ssc_name)

View File

@ -222,7 +222,7 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Ast.expr) :
in
if EnumConstructorMap.cardinal remaining_e_cases > 0 then
Errors.raise_spanned_error (Expr.pos e)
"Patter matching is incomplete for enum %a: missing cases %a"
"Pattern matching is incomplete for enum %a: missing cases %a"
EnumName.format_t enum_name
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ", ")

View File

@ -386,10 +386,8 @@ let rec typecheck_expr_bottom_up :
let c_ty =
ast_to_typ (List.assoc c_name (A.EnumMap.find e_name ctx.A.ctx_enums))
in
let+ e_enum' =
typecheck_expr_top_down ctx env (unionfind_make (TEnum e_name)) e_enum
in
mark (A.EEnumInj (e_enum', c_name, e_name)) c_ty
let+ e_enum' = typecheck_expr_top_down ctx env c_ty e_enum in
mark (A.EEnumInj (e_enum', c_name, e_name)) (unionfind_make (TEnum e_name))
| A.EMatchS (e1, e_name, cases) ->
let cases_ty = A.EnumMap.find e_name ctx.A.ctx_enums in
let t_ret = unionfind_make ~pos:e1 (TAny (Any.fresh ())) in
@ -612,11 +610,12 @@ and typecheck_expr_top_down :
in
A.EStructAccess (e_struct', f_name, s_name)
| A.EEnumInj (e_enum, c_name, e_name) ->
unify_and_mark
(ast_to_typ (List.assoc c_name (A.EnumMap.find e_name ctx.A.ctx_enums)))
unify_and_mark (unionfind_make (TEnum e_name))
@@ fun () ->
let+ e_enum' =
typecheck_expr_top_down ctx env (unionfind_make (TEnum e_name)) e_enum
typecheck_expr_top_down ctx env
(ast_to_typ (List.assoc c_name (A.EnumMap.find e_name ctx.A.ctx_enums)))
e_enum
in
A.EEnumInj (e_enum', c_name, e_name)
| A.EMatchS (e1, e_name, cases) ->