diff --git a/src/TypeInference/Def.ml b/src/TypeInference/Def.ml new file mode 100644 index 00000000..ba46d055 --- /dev/null +++ b/src/TypeInference/Def.ml @@ -0,0 +1,467 @@ +(* This file is part of DBL, released under MIT license. + * See LICENSE for details. + *) + +(** Type-inference for definitions *) + +open Common +open TypeCheckFix + +(** Information about the label used by a handler *) +type label_info = + { l_expr : T.expr; + (** Expression that evaluates to the label *) + + l_ctx : T.expr -> T.expr; + (** Context that generates fresh label when necessary *) + + l_eff : T.effect; + (** Effect provided by this label *) + + l_sub : T.tvar -> T.subst; + (** Substitution generating function, used to instantiate capability *) + + l_delim_tp : T.typ; + (** Type of the delimiter *) + + l_delim_eff : T.effrow + (** Effect of the delimiter *) + } + +(** Check if given expression is a monomorphic variable *) +let is_monomorphic_var env (e : S.expr) = + match e.data with + | EPoly(p, _, _) -> + let sch_opt = + match p.data with + | EVar x -> + begin match Env.lookup_var env x with + | None | Some (VI_Ctor _) | Some (VI_MethodFn _) -> None + | Some (VI_Var(_, sch)) -> Some sch + end + | EImplicit name -> + Option.map (fun (_, sch, _) -> sch) (Env.lookup_implicit env name) + | EMethod _ -> None + in + begin match sch_opt with + | Some { sch_targs = []; sch_named = []; sch_body = _ } -> true + | _ -> false + end + | _ -> false + +(* ------------------------------------------------------------------------- *) +(** Shrink scope of type response. On error, raise escaping scope error + for given position *) +let type_resp_in_scope (type dir) ~env ~pos ~scope + (resp : (T.typ, dir) response) : (T.typ, dir) response = + match resp with + | Infered tp -> + (* TODO: tp can be raised to some supertype in the scope *) + begin match T.Type.try_shrink_scope ~scope tp with + | Ok () -> Infered tp + | Error x -> + Error.fatal (Error.type_escapes_its_scope ~pos ~env x) + end + | Checked -> Checked + +(* ------------------------------------------------------------------------- *) +(** Check let-definition *) +let check_let ~tcfix ~pos env ienv body eff = + let open (val tcfix : TCFix) in + let (body_env, ims) = ImplicitEnv.begin_generalize env ienv in + let (body, tp, r_eff) = infer_expr_type body_env body eff in + (* Purity restriction: check if r_eff is pure. If so, then generalize type + of an expression *) + match r_eff with + | Pure -> + let (targs, ims) = ImplicitEnv.end_generalize_pure ims (T.Type.uvars tp) in + (* TODO: make sure that names do not overlap *) + let (body, sch) = ExprUtils.generalize ~pos targs ims body tp in + (sch, body, Pure) + | Impure -> + ImplicitEnv.end_generalize_impure ~env:body_env ~pos:body.pos ims tp; + let sch = T.Scheme.of_type tp in + (sch, body, Impure) + +(* ------------------------------------------------------------------------- *) +(** First pass of checking recursive function: guessing its scheme *) +let prepare_rec_fun (env, ienv) (fd : S.rec_fun) = + let (RecFun(name, targs, nargs, body)) = fd.data in + let (body_env, tvars) = Type.tr_named_type_args env targs in + let (body_env, named, r_eff1) = + Pattern.infer_named_arg_schemes body_env nargs in + (* TODO: use type annotation to obtain this type *) + let body_tp = Env.fresh_uvar body_env T.Kind.k_type in + let sch = + { T.sch_targs = tvars; + T.sch_named = List.map (fun (name, _, sch) -> (name, sch)) named; + T.sch_body = body_tp + } in + let (env, ienv, x) = ImplicitEnv.add_poly_id ~pos:fd.pos env ienv name sch in + let fd = (fd.pos, name, x, sch, targs, nargs, body) in + ((env, ienv), fd) + +(** Second pass of checking recursive function: type-checking *) +let check_rec_fun ~tcfix env (pos, name, x, sch, targs, nargs, body) = + let open (val tcfix : TCFix) in + let (body_env, tvars) = Type.tr_named_type_args env targs in + let (body_env, named, r_eff1) = + Pattern.infer_named_arg_schemes body_env nargs in + let body_tp = Env.fresh_uvar body_env T.Kind.k_type in + let sch' = + { T.sch_targs = tvars; + T.sch_named = List.map (fun (name, _, sch) -> (name, sch)) named; + T.sch_body = body_tp + } in + if Unification.subscheme env sch' sch <> Unify_Success then + (* Both schemes come from the same definition. They should be unifiable *) + assert false; + let (body, r_eff2) = check_expr_type body_env body body_tp T.Effect.pure in + begin match ret_effect_join r_eff1 r_eff2 with + | Pure -> () + | Impure -> Error.report (Error.func_not_pure ~pos) + end; + let (named, body) = + ExprUtils.inst_args_match named body body_tp T.Effect.pure in + let body = ExprUtils.make_nfun named body in + (pos, name, x, sch, tvars, body) + +(** Third pass of checking recursive function: collecting unification + variables *) +let collect_rec_fun_uvars uvs (_, _, _, sch, _, _) = + T.Scheme.collect_uvars sch uvs + +(** Fourth pass of checking recursive function: building final environment *) +let add_rec_fun tvs1 ims (env, ienv) (pos, name, x, sch, tvs2, body) = + let make data = { T.pos = pos; T.data = data } in + let make_app ims f = + List.fold_left + (fun f (_, x, _) -> make (T.EApp(f, make (T.EVar x)))) + f ims in + let make_tapp tvs f = + List.fold_left + (fun f (_, x) -> make (T.ETApp(f, T.Type.t_var x))) + f tvs in + let y_sch = + { T.sch_targs = tvs1 @ sch.T.sch_targs; + T.sch_named = + List.map (fun (name, _, sch) -> (name, sch)) ims @ sch.T.sch_named; + T.sch_body = sch.T.sch_body + } in + let (env, ienv, y) = ImplicitEnv.add_poly_id ~pos env ienv name y_sch in + (* Less-generalized form of this function *) + let x_body = + ExprUtils.make_tfun tvs2 + (make (T.EVar y) |> make_tapp tvs1 |> make_tapp tvs2 |> make_app ims) in + let fd = (pos, y, y_sch, x, sch, x_body, tvs1 @ tvs2, ims, body) in + ((env, ienv), fd) + +(** Fifth and final pass of checking recursive function: build an expression + with local definitions of less-generalized functions *) +let finalize_rec_fun fds (pos, y, y_sch, _, _, _, tvs, ims, body) = + let make data = { T.pos = pos; T.data = data } in + let build_local_inst (_, _, _, x, x_sch, x_body, _, _, _) body = + make (T.ELet(x, x_sch, x_body, body)) in + let build_local_ctx body = + List.fold_right build_local_inst fds body in + let rec update_body (body : T.expr) = + let make data = { body with data = data } in + match body.T.data with + | EUnitPrf | ENum _ | EStr _ | EExtern _ -> body + | EVar x -> + if List.exists (fun (_, _, _, x', _, _, _, _, _) -> Var.equal x x') fds + then + Error.fatal (Error.non_productive_rec_def ~pos:body.pos); + body + | EFn(arg, arg_sch, body) -> + make (T.EFn(arg, arg_sch, build_local_ctx body)) + | EPureFn(arg, arg_sch, body) -> + make (T.EPureFn(arg, arg_sch, update_body body)) + | ETFun(x, body) -> + make (T.ETFun(x, update_body body)) + | ECtor(prf, n, tps, args) -> + make (T.ECtor(prf, n, tps, List.map update_body args)) + | EApp _ | ETApp _ | ELet _ | ELetRec _ | EData _ | EMatchEmpty _ + | EMatch _ | ELabel _ | EHandle _ | EHandler _ | EEffect _ | ERepl _ + | EReplExpr _ -> + Error.fatal (Error.non_productive_rec_def ~pos:body.pos) + in + let body = update_body body in + (y, y_sch, ExprUtils.make_tfun tvs (ExprUtils.make_nfun ims body)) + +(* ------------------------------------------------------------------------- *) +(** Check expression put into REPL *) +let check_repl_expr ~tcfix env ienv e eff = + let open (val tcfix : TCFix) in + let (env1, ims) = ImplicitEnv.begin_generalize env ienv in + let (e, tp, r_eff) = infer_expr_type env e eff in + ImplicitEnv.end_generalize_impure ~pos:e.pos ~env:env1 ims tp; + let pp_ctx = Pretty.empty_context () in + (e, Pretty.type_to_string pp_ctx env tp, r_eff) + +(* ------------------------------------------------------------------------- *) +let check_def : type dir. tcfix:tcfix -> + Env.t -> ImplicitEnv.t -> S.def -> + (T.typ, dir) request -> T.effrow -> def_cont -> + T.expr * (T.typ, dir) response * ret_effect = + fun ~tcfix env ienv def req eff cont -> + let open (val tcfix : TCFix) in + let make (e : T.expr) data = + { T.pos = Position.join def.pos e.pos; + T.data = data + } in + let pos = def.pos in + match def.data with + | DLetId(id, e1) -> + let (sch, e1, r_eff1) = check_let ~tcfix ~pos env ienv e1 eff in + let (env, ienv, x) = + ImplicitEnv.add_poly_id ~pos env ienv id sch in + let (e2, resp, r_eff2) = cont.run env ienv req eff in + (make e2 (T.ELet(x, sch, e1, e2)), resp, ret_effect_join r_eff1 r_eff2) + + | DLetFun(id, targs, nargs, body) -> + let (body_env, tvars2) = Type.tr_named_type_args env targs in + let (body_env, ims1) = ImplicitEnv.begin_generalize body_env ienv in + let (body_env, ims2, r_eff1) = + Pattern.infer_named_arg_schemes body_env nargs in + let (body, tp, r_eff2) = infer_expr_type body_env body T.Effect.pure in + begin match ret_effect_join r_eff1 r_eff2 with + | Pure -> () + | Impure -> Error.report (Error.func_not_pure ~pos:def.pos) + end; + (* TODO: check if [tp] is in proper scope (ims2 may bind some types) *) + let (ims2, body) = ExprUtils.inst_args_match ims2 body tp T.Effect.pure in + let (tvars1, ims1) = + ImplicitEnv.end_generalize_pure ims1 (T.Type.uvars tp) in + let (body, sch) = + ExprUtils.generalize ~pos (tvars1 @ tvars2) (ims1 @ ims2) body tp in + let (env, ienv, x) = + ImplicitEnv.add_poly_id ~pos env ienv id sch in + let (e2, resp, r_eff) = cont.run env ienv req eff in + (make e2 (T.ELet(x, sch, body, e2)), resp, r_eff) + + | DLetPat(pat, e1) -> + let scope = Env.scope env in + let (env1, ims) = ImplicitEnv.begin_generalize env ienv in + let (e1, tp, r_eff1) = infer_expr_type env1 e1 eff in + ImplicitEnv.end_generalize_impure ~env:env1 ~pos:e1.pos ims tp; + let (env, pat, names, r_eff2) = + Pattern.check_type ~env ~scope pat tp in + let ienv = ImplicitEnv.shadow_names ienv names in + let (e2, resp, r_eff3) = cont.run env ienv req eff in + let resp = type_resp_in_scope ~env ~pos:def.pos ~scope resp in + let res_tp = bidir_result req resp in + (make e2 (T.EMatch(e1, [(pat, e2)], res_tp, eff)), resp, + ret_effect_joins [ r_eff1; r_eff2; r_eff3 ]) + + | DMethodFn(public, x, method_name) -> + let env = Env.add_method_fn ~public env x method_name in + cont.run env ienv req eff + + | DFunRec fds -> + let (rec_env, ims) = ImplicitEnv.begin_generalize env ienv in + let ((rec_env, _), fds) = + List.fold_left_map prepare_rec_fun (rec_env, ienv) fds in + let fds = List.map (check_rec_fun ~tcfix rec_env) fds in + let uvars = List.fold_left collect_rec_fun_uvars T.UVar.Set.empty fds in + let (tvars, ims) = ImplicitEnv.end_generalize_pure ims uvars in + let ((env, ienv), fds) = + List.fold_left_map (add_rec_fun tvars ims) (env, ienv) fds in + let fds = List.map (finalize_rec_fun fds) fds in + let (e2, resp, r_eff) = cont.run env ienv req eff in + (make e2 (T.ELetRec(fds, e2)), resp, r_eff) + + | DLabel(eff_opt, pat) -> + let scope = Env.scope env in + let (env, l_eff) = Env.add_the_effect ~pos:def.pos env in + let env = + Type.check_type_alias_binder_opt env eff_opt (T.Type.t_var l_eff) in + let tp0 = Env.fresh_uvar env T.Kind.k_type in + let eff0 = Env.fresh_uvar env T.Kind.k_effrow in + let l_tp = T.Type.t_label (T.Type.t_var l_eff) tp0 eff0 in + let scope1 = Env.scope env in + let (env, pat, names, _) = + Pattern.check_type ~env ~scope:scope1 pat l_tp in + let ienv = ImplicitEnv.shadow_names ienv names in + let (e2, resp, _) = cont.run env ienv req eff in + let resp = type_resp_in_scope ~env ~pos:def.pos ~scope resp in + let res_tp = bidir_result req resp in + let x = Var.fresh ~name:"lbl" () in + (make e2 (T.ELabel(l_eff, x, tp0, eff0, + (make e2 (T.EMatch({ def with data = T.EVar x}, + [(pat, e2)], res_tp, eff))))), + resp, Impure) + + | DHandlePat + { label; effect = eff_opt; cap_pat = pat; capability = eh; + ret_clauses = rcs; fin_clauses = fcs } -> + let env0 = env in + let (lbl, env) = + match label with + | None -> + let (env, l_eff) = Env.add_the_effect env in + let env = + Type.check_type_alias_binder_opt env eff_opt (T.Type.t_var l_eff) in + let tp0 = Env.fresh_uvar env T.Kind.k_type in + let eff0 = Env.fresh_uvar env T.Kind.k_effrow in + let (env, x) = Env.add_the_label env (T.Type.t_var l_eff) tp0 eff0 in + let ctx e = + { T.pos = Position.join def.pos e.T.pos; + T.data = T.ELabel(l_eff, x, tp0, eff0, e) + } + in + { l_expr = { T.pos = def.pos; T.data = T.EVar x }; + l_ctx = ctx; + l_eff = T.Type.t_var l_eff; + l_sub = + (* It might be tempting to use [T.Subst.rename_to_fresh] here, but + we cannot ensure that this freshly generated type variable do + not appear in component of the handler type (and it is easy to + find counter-example). However, for monomorphic handlers it + could be done better. *) + (fun a -> + if is_monomorphic_var env eh then + T.Subst.rename_to_fresh T.Subst.empty a l_eff + else + T.Subst.add_type T.Subst.empty a (T.Type.t_var l_eff)); + l_delim_tp = tp0; + l_delim_eff = eff0 + }, env + | Some le -> + let (env', ims) = ImplicitEnv.begin_generalize env ienv in + let (le, le_tp, _) = infer_expr_type env' le eff in + ImplicitEnv.end_generalize_impure ~env:env' ~pos:le.pos ims le_tp; + begin match Unification.as_label env le_tp with + | L_Label(l_eff, tp0, eff0) -> + let env = Type.check_type_alias_binder_opt env eff_opt l_eff in + let env = Env.add_the_effect_alias env l_eff in + let (env, l_var) = Env.add_the_label env l_eff tp0 eff0 in + let ctx e = + { T.pos = Position.join def.pos e.T.pos; + T.data = T.ELet(l_var, T.Scheme.of_type le_tp, le, e) + } in + { l_expr = { le with data = T.EVar l_var }; + l_ctx = ctx; + l_eff = l_eff; + l_sub = (fun a -> T.Subst.add_type T.Subst.empty a l_eff); + l_delim_tp = tp0; + l_delim_eff = eff0 + }, env + + | L_NoEffect -> + Error.fatal (Error.unbound_the_effect ~pos:le.pos) + + | L_No -> + Error.fatal (Error.expr_not_label ~pos:le.pos ~env le_tp) + end + in + let env_f = env in + let (env_h, ims) = ImplicitEnv.begin_generalize env ienv in + let (eh, eh_tp, _) = infer_expr_type env_h eh eff in + (* TODO: effect capability may have a scheme instead of type *) + ImplicitEnv.end_generalize_impure ~env:env_h ~pos:eh.pos ims eh_tp; + begin match Unification.to_handler env eh_tp with + | H_Handler(a, cap_tp, res_tp, res_eff) -> + let sub = lbl.l_sub a in + let cap_tp = T.Type.subst sub cap_tp in + let res_tp = T.Type.subst sub res_tp in + let res_eff = T.Type.subst sub res_eff in + Error.check_unify_result ~pos:def.pos + (Unification.unify_type env lbl.l_delim_tp res_tp) + ~on_error:(Error.delim_type_mismatch ~env lbl.l_delim_tp res_tp); + Error.check_unify_result ~pos:def.pos + (Unification.unify_type env lbl.l_delim_eff res_eff) + ~on_error:(Error.delim_effect_mismatch ~env lbl.l_delim_eff res_eff); + let (env, pat, names, _) = + Pattern.check_type ~env ~scope:(Env.scope env) pat cap_tp in + let ienv = ImplicitEnv.shadow_names ienv names in + let (ret_x, body_tp, ret_body) = + MatchClause.check_return_clauses ~tcfix env rcs res_tp res_eff in + let body_eff = T.Effect.cons_eff lbl.l_eff res_eff in + let (body, Checked, _) = cont.run env ienv (Check body_tp) body_eff in + let (x, body) = ExprUtils.arg_match pat body body_tp body_eff in + let pos = Position.join def.pos body.pos in + Error.check_unify_result ~pos + (Unification.subeffect env0 res_eff eff) + ~on_error:(Error.expr_effect_mismatch ~env:env0 res_eff eff); + let e = + make body (T.EHandle + { label = lbl.l_expr; + effect = lbl.l_eff; + cap_var = x; + body = body; + capability = eh; + ret_var = ret_x; + ret_body = ret_body; + result_tp = res_tp; + result_eff = res_eff + }) in + let (e, tp, r_eff) = + MatchClause.check_finally_clauses ~tcfix env_f fcs e res_tp req eff in + (lbl.l_ctx e, tp, r_eff) + + | H_No -> + Error.fatal (Error.expr_not_handler ~pos:eh.pos ~env eh_tp) + end + + | DImplicit(n, args, sch) -> + let (env1, ims) = ImplicitEnv.begin_generalize env ienv in + let (env1, args1) = Type.tr_named_type_args env1 args in + let sch = Type.tr_scheme env1 sch in + let (args2, ims) = + ImplicitEnv.end_generalize_pure ims (T.Scheme.uvars sch) in + assert (List.is_empty ims); + let args = args1 @ args2 in + let ienv = ImplicitEnv.declare_implicit ienv n args sch in + cont.run env ienv req eff + + | DData dd -> + let scope = Env.scope env in + let (env, dd) = DataType.check_data_def env dd in + let (e, resp, r_eff) = cont.run env ienv req eff in + let resp = type_resp_in_scope ~env ~pos:def.pos ~scope resp in + (make e (T.EData([dd], e)), resp, r_eff) + + | DDataRec dds -> + let scope = Env.scope env in + let (env, dds) = DataType.check_rec_data_defs env dds in + let (e, resp, r_eff) = cont.run env ienv req eff in + let resp = type_resp_in_scope ~env ~pos:def.pos ~scope resp in + (make e (T.EData(dds, e)), resp, r_eff) + + | DModule(public, name, defs) -> + let env = Env.enter_module env in + check_defs env ImplicitEnv.empty defs req eff + { run = fun env _ req eff -> + let env = Env.leave_module env ~public name in + cont.run env ienv req eff } + + | DOpen(public, path) -> + begin match Env.lookup_module env path with + | Some m -> + let env = Env.open_module env ~public m in + cont.run env ienv req eff + | None -> + Error.report (Error.unbound_module ~pos path); + cont.run env ienv req eff + end + + | DReplExpr e1 -> + let scope = Env.scope env in + let (e1, tp1, r_eff1) = check_repl_expr ~tcfix env ienv e1 eff in + let (e, resp, r_eff2) = cont.run env ienv req eff in + let resp = type_resp_in_scope ~env ~pos:def.pos ~scope resp in + (make e (T.EReplExpr(e1, tp1, e)), resp, ret_effect_join r_eff1 r_eff2) + +(* ------------------------------------------------------------------------- *) +let check_defs : type dir. tcfix:tcfix -> + Env.t -> ImplicitEnv.t -> S.def list -> + (T.typ, dir) request -> T.effrow -> def_cont -> + T.expr * (T.typ, dir) response * ret_effect = + fun ~tcfix env ienv defs req eff cont -> + let open (val tcfix : TCFix) in + match defs with + | [] -> cont.run env ienv req eff + | def :: defs -> + check_def env ienv def req eff + { run = fun env ienv req eff -> check_defs env ienv defs req eff cont } diff --git a/src/TypeInference/Def.mli b/src/TypeInference/Def.mli new file mode 100644 index 00000000..388b5e77 --- /dev/null +++ b/src/TypeInference/Def.mli @@ -0,0 +1,24 @@ +(* This file is part of DBL, released under MIT license. + * See LICENSE for details. + *) + +(** Type-inference for definitions *) + +open Common +open TypeCheckFix + +(** Check type and effect of a single definition. It uses bidirectional + type checking, and pass the extended environment to the body-generating + continuation. *) +val check_def : tcfix:tcfix -> + Env.t -> ImplicitEnv.t -> S.def -> + (T.typ, 'dir) request -> T.effrow -> def_cont -> + T.expr * (T.typ, 'dir) response * ret_effect + +(** Check type and effect of a block of definitions. It uses bidirectional + type checking, and pass the extended environment to the body-generating + continuation. *) +val check_defs : tcfix:tcfix -> + Env.t -> ImplicitEnv.t -> S.def list -> + (T.typ, 'dir) request -> T.effrow -> def_cont -> + T.expr * (T.typ, 'dir) response * ret_effect diff --git a/src/TypeInference/Expr.ml b/src/TypeInference/Expr.ml index f21417fc..b2bd069d 100644 --- a/src/TypeInference/Expr.ml +++ b/src/TypeInference/Expr.ml @@ -5,176 +5,46 @@ (** Type-inference for expressions and related syntactic categories *) open Common - -(** Type of continuation used to type-checking of definitions. It is defined - as record, in order to allow it to be polymorphic in a direction of type - checking. *) -type def_cont = - { run : 'dir. - Env.t -> ImplicitEnv.t -> (T.typ, 'dir) request -> T.effrow -> - T.expr * (T.typ, 'dir) response * ret_effect - } - -(** Information about the label used by a handler *) -type label_info = - { l_expr : T.expr; - (** Expression that evaluates to the label *) - - l_ctx : T.expr -> T.expr; - (** Context that generates fresh label when necessary *) - - l_eff : T.effect; - (** Effect provided by this label *) - - l_sub : T.tvar -> T.subst; - (** Substitution generating function, used to instantiate capability *) - - l_delim_tp : T.typ; - (** Type of the delimiter *) - - l_delim_eff : T.effrow - (** Effect of the delimiter *) - } - -(** Shrink scope of type response. On error, raise escaping scope error - for given position *) -let type_resp_in_scope (type dir) ~env ~pos ~scope - (resp : (T.typ, dir) response) : (T.typ, dir) response = - match resp with - | Infered tp -> - (* TODO: tp can be raised to some supertype in the scope *) - begin match T.Type.try_shrink_scope ~scope tp with - | Ok () -> Infered tp - | Error x -> - Error.fatal (Error.type_escapes_its_scope ~pos ~env x) - end - | Checked -> Checked - -(** Check if given expression is a monomorphic variable *) -let is_monomorphic_var env (e : S.expr) = - match e.data with - | EPoly(p, _, _) -> - let sch_opt = - match p.data with - | EVar x -> - begin match Env.lookup_var env x with - | None | Some (VI_Ctor _) | Some (VI_MethodFn _) -> None - | Some (VI_Var(_, sch)) -> Some sch - end - | EImplicit name -> - Option.map (fun (_, sch, _) -> sch) (Env.lookup_implicit env name) - | EMethod _ -> None - in - begin match sch_opt with - | Some { sch_targs = []; sch_named = []; sch_body = _ } -> true - | _ -> false - end - | _ -> false +open TypeCheckFix (* ------------------------------------------------------------------------- *) -(** Infer scheme of type variable *) -let infer_var_scheme ~pos env x = - match Env.lookup_var env x with - | Some (VI_Var(x, sch)) -> - ({ T.pos = pos; T.data = T.EVar x }, sch) - | Some (VI_Ctor(idx, info)) -> - let ctor = List.nth info.adt_ctors idx in - let targs = info.adt_args @ ctor.ctor_targs in - let sch = { - T.sch_targs = targs; - T.sch_named = ctor.ctor_named; - T.sch_body = T.Type.t_pure_arrows ctor.ctor_arg_schemes info.adt_type - } in - (ExprUtils.ctor_func ~pos idx info, sch) - | Some (VI_MethodFn name) -> - Error.fatal (Error.method_fn_without_arg ~pos x name) - | None -> - Error.fatal (Error.unbound_var ~pos x) - -(* ------------------------------------------------------------------------- *) -(** Infer scheme of a named implicit *) -let infer_implicit_scheme ~pos env name = - match Env.lookup_implicit env name with - | Some (x, sch, on_use) -> - on_use pos; - ({ T.pos = pos; T.data = T.EVar x }, sch) - | None -> - Error.fatal (Error.unbound_implicit ~pos name) +(** Default behaviour of type-inferece for application *) +let infer_app_type ~tcfix ~pos env e1 e2 eff = + let open (val tcfix : TCFix) in + let make data = T.{ data; pos } in + let (e1, ftp, r_eff1) = infer_expr_type env e1 eff in + match Unification.to_arrow env ftp with + | Arr_UVar -> assert false + | Arr_Pure(sch, vtp) -> + let (e2, r_eff2) = PolyExpr.check_actual_arg ~tcfix env e2 sch eff in + (make (T.EApp(e1, e2)), vtp, ret_effect_join r_eff1 r_eff2) + | Arr_Impure(sch, vtp, f_eff) -> + let (e2, r_eff2) = PolyExpr.check_actual_arg ~tcfix env e2 sch eff in + Error.check_unify_result ~pos:e1.pos + (Unification.subeffect env f_eff eff) + ~on_error:(Error.func_effect_mismatch ~env f_eff eff); + (make (T.EApp(e1, e2)), vtp, Impure) + | Arr_No -> + Error.fatal (Error.expr_not_function ~pos:e1.pos ~env ftp) (* ------------------------------------------------------------------------- *) -(** Infer scheme of a polymorphic expression. The effect of en expression is - always in the check-mode. It returns a tuple, that contains the context of - the polymorphic expression (computing polymorphic expression may have some - effects, that should be performed before explicit instantiation), the - translated polymorphic expression, its scheme, and the hints for the scheme - instantiation. The context is a function that takes instantiation, its type - and effect, and returns translated expression, its type and the effect. *) -let rec infer_poly_scheme env (e : S.poly_expr) eff = - let pos = e.pos in - let default_ctx e tp r_eff = (e, tp, r_eff) in - match e.data with - | EVar x -> - let (e, sch) = infer_var_scheme ~pos env x in - (default_ctx, e, sch, T.TVar.Map.empty) - | EImplicit n -> - let (e, sch) = infer_implicit_scheme ~pos env n in - (default_ctx, e, sch, T.TVar.Map.empty) - | EMethod(self, name) -> - let (self, self_tp, self_r_eff) = infer_expr_type env self eff in - begin match T.Type.whnf self_tp with - | Whnf_Neutral(NH_Var a, _) -> - begin match Env.lookup_method env a name with - | Some(x, sch) -> - (method_call_ctx ~pos ~env ~self ~self_tp ~self_r_eff ~eff, - { T.pos = pos; T.data = T.EVar x }, - sch, - TypeUtils.method_inst_hints sch self_tp) - | None -> - Error.fatal (Error.unbound_method ~pos ~env a name) - end - | Whnf_Neutral(NH_UVar _, _) -> - Error.fatal (Error.method_call_on_unknown_type ~pos:e.pos) - - | Whnf_PureArrow _ | Whnf_Arrow _ | Whnf_Handler _ - | Whnf_Label _ -> - Error.fatal (Error.method_call_on_invalid_type ~pos:e.pos ~env self_tp) - - | Whnf_Effect _ | Whnf_Effrow _ -> - failwith "Internal kind error" - end - -(** Context of a method call, returned by [infer_poly_scheme] *) -and method_call_ctx ~pos ~env ~self ~self_tp ~self_r_eff ~eff = - fun e method_tp r_eff -> - let result_expr = { T.pos = pos; T.data = T.EApp(e, self) } in - match T.Type.view method_tp with - | TArrow( - { sch_targs = []; sch_named = []; sch_body = self_tp' }, - res_tp, res_eff) -> - Error.check_unify_result ~pos:self.pos - (Unification.subtype env self_tp self_tp') - ~on_error:(Error.expr_type_mismatch ~env self_tp self_tp'); - Error.check_unify_result ~pos - (Unification.subeffect env res_eff eff) - ~on_error:(Error.method_effect_mismatch ~env res_eff eff); - (* The method is impure, so the result is impure too. *) - (result_expr, res_tp, Impure) - | TPureArrow( - { sch_targs = []; sch_named = []; sch_body = self_tp' }, - res_tp) -> - Error.check_unify_result ~pos:self.pos - (Unification.subtype env self_tp self_tp') - ~on_error:(Error.expr_type_mismatch ~env self_tp self_tp'); - (result_expr, res_tp, ret_effect_join self_r_eff r_eff) - | _ -> - (* Method must be an arrow with monomorphic argument *) - InterpLib.InternalError.report ~reason:"invalid method type" () +(** Bidirectional type-checker of expressions *) +let tr_expr : type dir. tcfix:tcfix -> + Env.t -> S.expr -> (T.typ, dir) request -> T.effrow -> + (T.expr * (T.typ, dir) response * ret_effect) = + fun ~tcfix env e tp_req eff -> + let open (val tcfix : TCFix) in + match tp_req with + | Infer -> + let (e, tp, r_eff) = infer_expr_type env e eff in + (e, Infered tp, r_eff) + | Check tp -> + let (e, r_eff) = check_expr_type env e tp eff in + (e, Checked, r_eff) (* ------------------------------------------------------------------------- *) -(** Infer type of an expression. The effect of an expression is always in - the check mode. However, pure expressions may returns an information that - they are pure (see [ret_effect] type). *) -and infer_expr_type env (e : S.expr) eff = +let infer_expr_type ~tcfix env (e : S.expr) eff = + let open (val tcfix : TCFix) in let make data = { e with data = data } in let pos = e.pos in match e.data with @@ -193,19 +63,19 @@ and infer_expr_type env (e : S.expr) eff = (make (T.EStr s), T.Type.t_var T.BuiltinType.tv_string, Pure) | EPoly(e, tinst, inst) -> - let (p_ctx, e, sch, hints1) = infer_poly_scheme env e eff in + let (p_ctx, e, sch, hints1) = PolyExpr.infer_scheme ~tcfix env e eff in Uniqueness.check_type_inst_uniqueness tinst; Uniqueness.check_inst_uniqueness inst; let tinst = Type.check_type_insts env tinst sch.sch_targs in let (hints2, cached_inst) = - extract_implicit_type_hints ~pos env sch inst eff in - let hints = TypeUtils.merge_hints hints1 hints2 in + TypeHints.extract_implicit_type_hints ~tcfix ~pos env sch inst eff in + let hints = TypeHints.merge_hints hints1 hints2 in let (sub, tps) = ExprUtils.guess_types ~pos ~tinst ~hints env sch.sch_targs in let e = ExprUtils.make_tapp e tps in let named = List.map (T.NamedScheme.subst sub) sch.sch_named in let (i_ctx, inst, r_eff) = - check_explicit_insts env named inst cached_inst eff in + PolyExpr.check_explicit_insts ~tcfix env named inst cached_inst eff in let e = ExprUtils.instantiate_named_params env e named inst in let tp = T.Type.subst sub sch.sch_body in (p_ctx (i_ctx e) tp r_eff) @@ -233,15 +103,15 @@ and infer_expr_type env (e : S.expr) eff = let new_m = { e with data = S.EMethod(e2, name) } in let new_e = { e1 with data = S.EPoly(new_m, tinst, insts) } in infer_expr_type env new_e eff - | _ -> infer_app_type ~pos env e1 e2 eff + | _ -> infer_app_type ~tcfix ~pos env e1 e2 eff end - | _ -> infer_app_type ~pos env e1 e2 eff + | _ -> infer_app_type ~tcfix ~pos env e1 e2 eff end | EDefs(defs, e) -> let (e, Infered tp, r_eff) = check_defs env ImplicitEnv.empty defs Infer eff - { run = fun env _ req eff -> tr_expr env e req eff } + { run = fun env _ req eff -> tr_expr ~tcfix env e req eff } in (e, tp, r_eff) @@ -264,38 +134,60 @@ and infer_expr_type env (e : S.expr) eff = let (e, r_eff) = check_expr_type env e tp eff in (e, tp, r_eff) -(** Default behaviour of type-inferece for application *) -and infer_app_type ~pos env e1 e2 eff = - let make data = T.{ data; pos } in - let (e1, ftp, r_eff1) = infer_expr_type env e1 eff in - match Unification.to_arrow env ftp with - | Arr_UVar -> assert false - | Arr_Pure(sch, vtp) -> - let (e2, r_eff2) = check_actual_arg ~pos env e2 sch eff in - (make (T.EApp(e1, e2)), vtp, ret_effect_join r_eff1 r_eff2) - | Arr_Impure(sch, vtp, f_eff) -> - let (e2, r_eff2) = check_actual_arg ~pos env e2 sch eff in - Error.check_unify_result ~pos:e1.pos - (Unification.subeffect env f_eff eff) - ~on_error:(Error.func_effect_mismatch ~env f_eff eff); - (make (T.EApp(e1, e2)), vtp, Impure) - | Arr_No -> - Error.fatal (Error.expr_not_function ~pos:e1.pos ~env ftp) +(* ------------------------------------------------------------------------- *) +(** Check the sequence of REPL definitions, provided by a user. Always + in type-check mode. *) +let rec check_repl_def_seq ~tcfix env ienv def_seq tp eff = + let open (val tcfix : TCFix) in + let func () = + match def_seq () with + | Seq.Nil -> assert false + | Seq.Cons(def, def_seq) -> + let cont (type dir) env ienv (tp_req : (_, dir) request) eff : + _ * (_, dir) response * _ = + match tp_req with + | Check tp -> + let e = check_repl_def_seq ~tcfix env ienv def_seq tp eff in + (e, Checked, Impure) + | Infer -> + let tp = Env.fresh_uvar env T.Kind.k_type in + let e = check_repl_def_seq ~tcfix env ienv def_seq tp eff in + (e, Infered tp, Impure) + in + let (e, Checked, _) = + check_def env ienv def (Check tp) eff { run = cont } in + e + in + let e = + { T.pos = Position.nowhere; + T.data = T.ERepl(func, tp, eff) + } in + e + +(* ------------------------------------------------------------------------- *) +(** Default action in type-check mode: switching to infer mode *) +let check_expr_type_default ~tcfix env (e : S.expr) tp eff = + let open (val tcfix : TCFix) in + let pos = e.pos in + let (e, tp', r_eff) = infer_expr_type env e eff in + Error.check_unify_result ~pos + (Unification.subtype env tp' tp) + ~on_error:(Error.expr_type_mismatch ~env tp' tp); + (e, r_eff) (* ------------------------------------------------------------------------- *) -(** Check type and effect of an expression. Returns also information about - the purity of an expression. *) -and check_expr_type env (e : S.expr) tp eff = +let check_expr_type ~tcfix env (e : S.expr) tp eff = + let open (val tcfix : TCFix) in let make data = { e with data = data } in let pos = e.pos in match e.data with | EUnit | ENum _ | EStr _ | EPoly _ | EApp _ -> - check_expr_type_default env e tp eff + check_expr_type_default ~tcfix env e tp eff | EFn(arg, body) -> begin match Unification.from_arrow env tp with | Arr_UVar -> - check_expr_type_default env e tp eff + check_expr_type_default ~tcfix env e tp eff | Arr_Pure(sch, tp2) -> let (env, pat, r_eff1) = Pattern.check_arg_scheme env arg sch in @@ -320,7 +212,7 @@ and check_expr_type env (e : S.expr) tp eff = | EDefs(defs, e) -> let (e, Checked, r_eff) = check_defs env ImplicitEnv.empty defs (Check tp) eff - { run = fun env _ req eff -> tr_expr env e req eff } + { run = fun env _ req eff -> tr_expr ~tcfix env e req eff } in (e, r_eff) @@ -350,7 +242,8 @@ and check_expr_type env (e : S.expr) tp eff = | EMatch(e, cls) -> let (e, e_tp, _) = infer_expr_type env e eff in - let (cls, r_eff) = check_match_clauses env e_tp cls tp eff in + let (cls, r_eff) = + MatchClause.check_match_clauses ~tcfix env e_tp cls tp eff in (make (T.EMatch(e, cls, tp, eff)), r_eff) | EHandler h -> @@ -404,663 +297,4 @@ and check_expr_type env (e : S.expr) tp eff = check_expr_type env e' tp' eff | ERepl def_seq -> - (check_repl_def_seq env ImplicitEnv.empty def_seq tp eff, Impure) - -(** Default action in type-check mode: switching to infer mode *) -and check_expr_type_default env (e : S.expr) tp eff = - let pos = e.pos in - let (e, tp', r_eff) = infer_expr_type env e eff in - Error.check_unify_result ~pos - (Unification.subtype env tp' tp) - ~on_error:(Error.expr_type_mismatch ~env tp' tp); - (e, r_eff) - -(** Bidirectional type-checker of expressions *) -and tr_expr : - type dir. Env.t -> S.expr -> (T.typ, dir) request -> T.effrow -> - (T.expr * (T.typ, dir) response * ret_effect) = - fun env e tp_req eff -> - match tp_req with - | Infer -> - let (e, tp, r_eff) = infer_expr_type env e eff in - (e, Infered tp, r_eff) - | Check tp -> - let (e, r_eff) = check_expr_type env e tp eff in - (e, Checked, r_eff) - -(* ------------------------------------------------------------------------- *) -(** Check the scheme of an actual parameter of a function *) -and check_actual_arg ~pos env (arg : S.expr) sch eff = - let (env, tvars, named, body_tp) = TypeUtils.open_scheme ~pos env sch in - let (body, res_eff) = - match tvars, named with - | [], [] -> check_expr_type env arg body_tp eff - | _ -> - let (body, res_eff) = check_expr_type env arg body_tp T.Effect.pure in - begin match res_eff with - | Pure -> () - | Impure -> Error.report (Error.func_not_pure ~pos:arg.pos) - end; - (body, Pure) - in - (ExprUtils.make_tfun tvars (ExprUtils.make_nfun named body), res_eff) - -(* ------------------------------------------------------------------------- *) -(** Extracts type hints for a type scheme from environment and explicit - instantiation. Returns hints and cached translated explicit - instantiations. *) -and extract_implicit_type_hints ~pos env (sch : T.scheme) inst eff = - let targs = sch.sch_targs in - let inst = - List.map (fun { T.data = (n, e); _ } -> (Name.tr_name env n, e)) inst in - let rec loop hints cache named = - match named with - | [] -> (hints, cache) - | (name, arg_sch) :: named - when T.Scheme.is_monomorphic arg_sch - && TypeUtils.is_tvar_neutral arg_sch.sch_body -> - let expr_opt = - match T.Name.assoc name inst with - | None -> - let make data = { S.pos = pos; S.data = data } in - begin match name with - | NLabel | NVar _ | NMethod _ -> None - | NImplicit n -> - (* type hints can be extracted only from monomorphic implicits - (and explicit instantiation, of course), in order to avoid - infinite loops: implicit parameters can depend on itself. *) - begin match Env.lookup_implicit env (NPName n) with - | Some(_, isch, _) when T.Scheme.is_monomorphic isch -> - Some (make (S.EPoly(make (S.EImplicit (S.NPName n)), [], []))) - | _ -> None - end - end - | Some e -> Some e - in - begin match expr_opt with - | None -> loop hints cache named - | Some e -> - let (e, tp, r_eff) = infer_expr_type env e eff in - let hints2 = TypeUtils.type_inst_hints targs arg_sch.sch_body tp in - loop - (TypeUtils.merge_hints hints hints2) - ((name, (e, tp, r_eff)) :: cache) - named - end - | _ :: named -> - loop hints cache named - in - loop T.TVar.Map.empty [] sch.sch_named - -(* ------------------------------------------------------------------------- *) -(** Check explicit instantiations against given list of named parameters (from - type scheme). It returns context (represented as meta-function) that - preserves the order of computations, list of checked instantiations, and - the effect. *) -and check_explicit_insts env named insts cache eff = - match insts with - | [] -> (Fun.id, [], Pure) - | { data = (n, e); pos } :: insts -> - let make data = { T.data; T.pos } in - let n = Name.tr_name env n in - let (e, sch, r_eff1) = - match T.Name.assoc n named with - | Some sch -> - begin match T.Name.assoc n cache with - | None -> - let (e, r_eff1) = check_actual_arg ~pos:e.pos env e sch eff in - (e, sch, r_eff1) - | Some (e, tp, r_eff1) -> - assert (T.Scheme.is_monomorphic sch); - Error.check_unify_result ~pos:e.pos - (Unification.subtype env tp sch.sch_body) - ~on_error:(Error.named_param_type_mismatch ~env n tp sch.sch_body); - (e, sch, r_eff1) - end - | None -> - Error.warn (Error.redundant_named_parameter ~pos n); - let (e, tp, r_eff1) = infer_expr_type env e eff in - (e, T.Scheme.of_type tp, r_eff1) - in - let (ctx, insts, r_eff2) = - check_explicit_insts env named insts cache eff in - let x = Var.fresh () in - let ctx e0 = make (T.ELet(x, sch, e, ctx e0)) in - let insts = (n, make (T.EVar x)) :: insts in - (ctx, insts, ret_effect_join r_eff1 r_eff2) - -(* ------------------------------------------------------------------------- *) -(** Check type and effect of a block of definitions. It uses bidirectional - type checking, and pass the extended environment to the body-generating - continuation. *) -and check_defs : type dir. - Env.t -> ImplicitEnv.t -> S.def list -> - (T.typ, dir) request -> T.effrow -> def_cont -> - T.expr * (T.typ, dir) response * ret_effect = - fun env ienv defs req eff cont -> - match defs with - | [] -> cont.run env ienv req eff - | def :: defs -> - check_def env ienv def req eff - { run = fun env ienv req eff -> check_defs env ienv defs req eff cont } - -and check_def : type dir. - Env.t -> ImplicitEnv.t -> S.def -> - (T.typ, dir) request -> T.effrow -> def_cont -> - T.expr * (T.typ, dir) response * ret_effect = - fun env ienv def req eff cont -> - let make (e : T.expr) data = - { T.pos = Position.join def.pos e.pos; - T.data = data - } in - let pos = def.pos in - match def.data with - | DLetId(id, e1) -> - let (sch, e1, r_eff1) = check_let ~pos env ienv e1 eff in - let (env, ienv, x) = - ImplicitEnv.add_poly_id ~pos env ienv id sch in - let (e2, resp, r_eff2) = cont.run env ienv req eff in - (make e2 (T.ELet(x, sch, e1, e2)), resp, ret_effect_join r_eff1 r_eff2) - - | DLetFun(id, targs, nargs, body) -> - let (body_env, tvars2) = Type.tr_named_type_args env targs in - let (body_env, ims1) = ImplicitEnv.begin_generalize body_env ienv in - let (body_env, ims2, r_eff1) = - Pattern.infer_named_arg_schemes body_env nargs in - let (body, tp, r_eff2) = infer_expr_type body_env body T.Effect.pure in - begin match ret_effect_join r_eff1 r_eff2 with - | Pure -> () - | Impure -> Error.report (Error.func_not_pure ~pos:def.pos) - end; - (* TODO: check if [tp] is in proper scope (ims2 may bind some types) *) - let (ims2, body) = ExprUtils.inst_args_match ims2 body tp T.Effect.pure in - let (tvars1, ims1) = - ImplicitEnv.end_generalize_pure ims1 (T.Type.uvars tp) in - let (body, sch) = - ExprUtils.generalize ~pos (tvars1 @ tvars2) (ims1 @ ims2) body tp in - let (env, ienv, x) = - ImplicitEnv.add_poly_id ~pos env ienv id sch in - let (e2, resp, r_eff) = cont.run env ienv req eff in - (make e2 (T.ELet(x, sch, body, e2)), resp, r_eff) - - | DLetPat(pat, e1) -> - let scope = Env.scope env in - let (env1, ims) = ImplicitEnv.begin_generalize env ienv in - let (e1, tp, r_eff1) = infer_expr_type env1 e1 eff in - ImplicitEnv.end_generalize_impure ~env:env1 ~pos:e1.pos ims tp; - let (env, pat, names, r_eff2) = - Pattern.check_type ~env ~scope pat tp in - let ienv = ImplicitEnv.shadow_names ienv names in - let (e2, resp, r_eff3) = cont.run env ienv req eff in - let resp = type_resp_in_scope ~env ~pos:def.pos ~scope resp in - let res_tp = bidir_result req resp in - (make e2 (T.EMatch(e1, [(pat, e2)], res_tp, eff)), resp, - ret_effect_joins [ r_eff1; r_eff2; r_eff3 ]) - - | DMethodFn(public, x, method_name) -> - let env = Env.add_method_fn ~public env x method_name in - cont.run env ienv req eff - - | DFunRec fds -> - let (rec_env, ims) = ImplicitEnv.begin_generalize env ienv in - let ((rec_env, _), fds) = - List.fold_left_map prepare_rec_fun (rec_env, ienv) fds in - let fds = List.map (check_rec_fun rec_env) fds in - let uvars = List.fold_left collect_rec_fun_uvars T.UVar.Set.empty fds in - let (tvars, ims) = ImplicitEnv.end_generalize_pure ims uvars in - let ((env, ienv), fds) = - List.fold_left_map (add_rec_fun tvars ims) (env, ienv) fds in - let fds = List.map (finalize_rec_fun fds) fds in - let (e2, resp, r_eff) = cont.run env ienv req eff in - (make e2 (T.ELetRec(fds, e2)), resp, r_eff) - - | DLabel(eff_opt, pat) -> - let scope = Env.scope env in - let (env, l_eff) = Env.add_the_effect ~pos:def.pos env in - let env = - Type.check_type_alias_binder_opt env eff_opt (T.Type.t_var l_eff) in - let tp0 = Env.fresh_uvar env T.Kind.k_type in - let eff0 = Env.fresh_uvar env T.Kind.k_effrow in - let l_tp = T.Type.t_label (T.Type.t_var l_eff) tp0 eff0 in - let scope1 = Env.scope env in - let (env, pat, names, _) = - Pattern.check_type ~env ~scope:scope1 pat l_tp in - let ienv = ImplicitEnv.shadow_names ienv names in - let (e2, resp, _) = cont.run env ienv req eff in - let resp = type_resp_in_scope ~env ~pos:def.pos ~scope resp in - let res_tp = bidir_result req resp in - let x = Var.fresh ~name:"lbl" () in - (make e2 (T.ELabel(l_eff, x, tp0, eff0, - (make e2 (T.EMatch({ def with data = T.EVar x}, - [(pat, e2)], res_tp, eff))))), - resp, Impure) - - | DHandlePat - { label; effect = eff_opt; cap_pat = pat; capability = eh; - ret_clauses = rcs; fin_clauses = fcs } -> - let env0 = env in - let (lbl, env) = - match label with - | None -> - let (env, l_eff) = Env.add_the_effect env in - let env = - Type.check_type_alias_binder_opt env eff_opt (T.Type.t_var l_eff) in - let tp0 = Env.fresh_uvar env T.Kind.k_type in - let eff0 = Env.fresh_uvar env T.Kind.k_effrow in - let (env, x) = Env.add_the_label env (T.Type.t_var l_eff) tp0 eff0 in - let ctx e = - { T.pos = Position.join def.pos e.T.pos; - T.data = T.ELabel(l_eff, x, tp0, eff0, e) - } - in - { l_expr = { T.pos = def.pos; T.data = T.EVar x }; - l_ctx = ctx; - l_eff = T.Type.t_var l_eff; - l_sub = - (* It might be tempting to use [T.Subst.rename_to_fresh] here, but - we cannot ensure that this freshly generated type variable do - not appear in component of the handler type (and it is easy to - find counter-example). However, for monomorphic handlers it - could be done better. *) - (fun a -> - if is_monomorphic_var env eh then - T.Subst.rename_to_fresh T.Subst.empty a l_eff - else - T.Subst.add_type T.Subst.empty a (T.Type.t_var l_eff)); - l_delim_tp = tp0; - l_delim_eff = eff0 - }, env - | Some le -> - let (env', ims) = ImplicitEnv.begin_generalize env ienv in - let (le, le_tp, _) = infer_expr_type env' le eff in - ImplicitEnv.end_generalize_impure ~env:env' ~pos:le.pos ims le_tp; - begin match Unification.as_label env le_tp with - | L_Label(l_eff, tp0, eff0) -> - let env = Type.check_type_alias_binder_opt env eff_opt l_eff in - let env = Env.add_the_effect_alias env l_eff in - let (env, l_var) = Env.add_the_label env l_eff tp0 eff0 in - let ctx e = - { T.pos = Position.join def.pos e.T.pos; - T.data = T.ELet(l_var, T.Scheme.of_type le_tp, le, e) - } in - { l_expr = { le with data = T.EVar l_var }; - l_ctx = ctx; - l_eff = l_eff; - l_sub = (fun a -> T.Subst.add_type T.Subst.empty a l_eff); - l_delim_tp = tp0; - l_delim_eff = eff0 - }, env - - | L_NoEffect -> - Error.fatal (Error.unbound_the_effect ~pos:le.pos) - - | L_No -> - Error.fatal (Error.expr_not_label ~pos:le.pos ~env le_tp) - end - in - let env_f = env in - let (env_h, ims) = ImplicitEnv.begin_generalize env ienv in - let (eh, eh_tp, _) = infer_expr_type env_h eh eff in - (* TODO: effect capability may have a scheme instead of type *) - ImplicitEnv.end_generalize_impure ~env:env_h ~pos:eh.pos ims eh_tp; - begin match Unification.to_handler env eh_tp with - | H_Handler(a, cap_tp, res_tp, res_eff) -> - let sub = lbl.l_sub a in - let cap_tp = T.Type.subst sub cap_tp in - let res_tp = T.Type.subst sub res_tp in - let res_eff = T.Type.subst sub res_eff in - Error.check_unify_result ~pos:def.pos - (Unification.unify_type env lbl.l_delim_tp res_tp) - ~on_error:(Error.delim_type_mismatch ~env lbl.l_delim_tp res_tp); - Error.check_unify_result ~pos:def.pos - (Unification.unify_type env lbl.l_delim_eff res_eff) - ~on_error:(Error.delim_effect_mismatch ~env lbl.l_delim_eff res_eff); - let (env, pat, names, _) = - Pattern.check_type ~env ~scope:(Env.scope env) pat cap_tp in - let ienv = ImplicitEnv.shadow_names ienv names in - let (ret_x, body_tp, ret_body) = - check_return_clauses env rcs res_tp res_eff in - let body_eff = T.Effect.cons_eff lbl.l_eff res_eff in - let (body, Checked, _) = cont.run env ienv (Check body_tp) body_eff in - let (x, body) = ExprUtils.arg_match pat body body_tp body_eff in - let pos = Position.join def.pos body.pos in - Error.check_unify_result ~pos - (Unification.subeffect env0 res_eff eff) - ~on_error:(Error.expr_effect_mismatch ~env:env0 res_eff eff); - let e = - make body (T.EHandle - { label = lbl.l_expr; - effect = lbl.l_eff; - cap_var = x; - body = body; - capability = eh; - ret_var = ret_x; - ret_body = ret_body; - result_tp = res_tp; - result_eff = res_eff - }) in - let (e, tp, r_eff) = check_finally_clauses env_f fcs e res_tp req eff in - (lbl.l_ctx e, tp, r_eff) - - | H_No -> - Error.fatal (Error.expr_not_handler ~pos:eh.pos ~env eh_tp) - end - - | DImplicit(n, args, sch) -> - let (env1, ims) = ImplicitEnv.begin_generalize env ienv in - let (env1, args1) = Type.tr_named_type_args env1 args in - let sch = Type.tr_scheme env1 sch in - let (args2, ims) = - ImplicitEnv.end_generalize_pure ims (T.Scheme.uvars sch) in - assert (List.is_empty ims); - let args = args1 @ args2 in - let ienv = ImplicitEnv.declare_implicit ienv n args sch in - cont.run env ienv req eff - - | DData dd -> - let scope = Env.scope env in - let (env, dd) = DataType.check_data_def env dd in - let (e, resp, r_eff) = cont.run env ienv req eff in - let resp = type_resp_in_scope ~env ~pos:def.pos ~scope resp in - (make e (T.EData([dd], e)), resp, r_eff) - - | DDataRec dds -> - let scope = Env.scope env in - let (env, dds) = DataType.check_rec_data_defs env dds in - let (e, resp, r_eff) = cont.run env ienv req eff in - let resp = type_resp_in_scope ~env ~pos:def.pos ~scope resp in - (make e (T.EData(dds, e)), resp, r_eff) - - | DModule(public, name, defs) -> - let env = Env.enter_module env in - check_defs env ImplicitEnv.empty defs req eff - { run = fun env _ req eff -> - let env = Env.leave_module env ~public name in - cont.run env ienv req eff } - - | DOpen(public, path) -> - begin match Env.lookup_module env path with - | Some m -> - let env = Env.open_module env ~public m in - cont.run env ienv req eff - | None -> - Error.report (Error.unbound_module ~pos path); - cont.run env ienv req eff - end - - | DReplExpr e1 -> - let scope = Env.scope env in - let (e1, tp1, r_eff1) = check_repl_expr env ienv e1 eff in - let (e, resp, r_eff2) = cont.run env ienv req eff in - let resp = type_resp_in_scope ~env ~pos:def.pos ~scope resp in - (make e (T.EReplExpr(e1, tp1, e)), resp, ret_effect_join r_eff1 r_eff2) - -(* ------------------------------------------------------------------------- *) -(** Check let-definition *) -and check_let ~pos env ienv body eff = - let (body_env, ims) = ImplicitEnv.begin_generalize env ienv in - let (body, tp, r_eff) = infer_expr_type body_env body eff in - (* Purity restriction: check if r_eff is pure. If so, then generalize type - of an expression *) - match r_eff with - | Pure -> - let (targs, ims) = ImplicitEnv.end_generalize_pure ims (T.Type.uvars tp) in - (* TODO: make sure that names do not overlap *) - let (body, sch) = ExprUtils.generalize ~pos targs ims body tp in - (sch, body, Pure) - | Impure -> - ImplicitEnv.end_generalize_impure ~env:body_env ~pos:body.pos ims tp; - let sch = T.Scheme.of_type tp in - (sch, body, Impure) - -(* ------------------------------------------------------------------------- *) -(** First pass of checking recursive function: guessing its scheme *) -and prepare_rec_fun (env, ienv) fd = - let (RecFun(name, targs, nargs, body)) = fd.data in - let (body_env, tvars) = Type.tr_named_type_args env targs in - let (body_env, named, r_eff1) = - Pattern.infer_named_arg_schemes body_env nargs in - (* TODO: use type annotation to obtain this type *) - let body_tp = Env.fresh_uvar body_env T.Kind.k_type in - let sch = - { T.sch_targs = tvars; - T.sch_named = List.map (fun (name, _, sch) -> (name, sch)) named; - T.sch_body = body_tp - } in - let (env, ienv, x) = ImplicitEnv.add_poly_id ~pos:fd.pos env ienv name sch in - let fd = (fd.pos, name, x, sch, targs, nargs, body) in - ((env, ienv), fd) - -(** Second pass of checking recursive function: type-checking *) -and check_rec_fun env (pos, name, x, sch, targs, nargs, body) = - let (body_env, tvars) = Type.tr_named_type_args env targs in - let (body_env, named, r_eff1) = - Pattern.infer_named_arg_schemes body_env nargs in - let body_tp = Env.fresh_uvar body_env T.Kind.k_type in - let sch' = - { T.sch_targs = tvars; - T.sch_named = List.map (fun (name, _, sch) -> (name, sch)) named; - T.sch_body = body_tp - } in - if Unification.subscheme env sch' sch <> Unify_Success then - (* Both schemes come from the same definition. They should be unifiable *) - assert false; - let (body, r_eff2) = check_expr_type body_env body body_tp T.Effect.pure in - begin match ret_effect_join r_eff1 r_eff2 with - | Pure -> () - | Impure -> Error.report (Error.func_not_pure ~pos) - end; - let (named, body) = - ExprUtils.inst_args_match named body body_tp T.Effect.pure in - let body = ExprUtils.make_nfun named body in - (pos, name, x, sch, tvars, body) - -(** Third pass of checking recursive function: collecting unification - variables *) -and collect_rec_fun_uvars uvs (_, _, _, sch, _, _) = - T.Scheme.collect_uvars sch uvs - -(** Fourth pass of checking recursive function: building final environment *) -and add_rec_fun tvs1 ims (env, ienv) (pos, name, x, sch, tvs2, body) = - let make data = { T.pos = pos; T.data = data } in - let make_app ims f = - List.fold_left - (fun f (_, x, _) -> make (T.EApp(f, make (T.EVar x)))) - f ims in - let make_tapp tvs f = - List.fold_left - (fun f (_, x) -> make (T.ETApp(f, T.Type.t_var x))) - f tvs in - let y_sch = - { T.sch_targs = tvs1 @ sch.T.sch_targs; - T.sch_named = - List.map (fun (name, _, sch) -> (name, sch)) ims @ sch.T.sch_named; - T.sch_body = sch.T.sch_body - } in - let (env, ienv, y) = ImplicitEnv.add_poly_id ~pos env ienv name y_sch in - (* Less-generalized form of this function *) - let x_body = - ExprUtils.make_tfun tvs2 - (make (T.EVar y) |> make_tapp tvs1 |> make_tapp tvs2 |> make_app ims) in - let fd = (pos, y, y_sch, x, sch, x_body, tvs1 @ tvs2, ims, body) in - ((env, ienv), fd) - -(** Fifth and final pass of checking recursive function: build an expression - with local definitions of less-generalized functions *) -and finalize_rec_fun fds (pos, y, y_sch, _, _, _, tvs, ims, body) = - let make data = { T.pos = pos; T.data = data } in - let build_local_inst (_, _, _, x, x_sch, x_body, _, _, _) body = - make (T.ELet(x, x_sch, x_body, body)) in - let build_local_ctx body = - List.fold_right build_local_inst fds body in - let rec update_body (body : T.expr) = - let make data = { body with data = data } in - match body.T.data with - | EUnitPrf | ENum _ | EStr _ | EExtern _ -> body - | EVar x -> - if List.exists (fun (_, _, _, x', _, _, _, _, _) -> Var.equal x x') fds - then - Error.fatal (Error.non_productive_rec_def ~pos:body.pos); - body - | EFn(arg, arg_sch, body) -> - make (T.EFn(arg, arg_sch, build_local_ctx body)) - | EPureFn(arg, arg_sch, body) -> - make (T.EPureFn(arg, arg_sch, update_body body)) - | ETFun(x, body) -> - make (T.ETFun(x, update_body body)) - | ECtor(prf, n, tps, args) -> - make (T.ECtor(prf, n, tps, List.map update_body args)) - | EApp _ | ETApp _ | ELet _ | ELetRec _ | EData _ | EMatchEmpty _ - | EMatch _ | ELabel _ | EHandle _ | EHandler _ | EEffect _ | ERepl _ - | EReplExpr _ -> - Error.fatal (Error.non_productive_rec_def ~pos:body.pos) - in - let body = update_body body in - (y, y_sch, ExprUtils.make_tfun tvs (ExprUtils.make_nfun ims body)) - -(* ------------------------------------------------------------------------- *) -(** Check a pattern-matching clause - In [check_match_clause env tp cl res_tp res_eff] the parameters have the - following meaning: - - [env] -- an environment - - [tp] -- type of the matched expression - - [cl] -- clause - - [res_tp] -- returned type - - [res_eff] -- returned effect *) -and check_match_clause env tp (cl : S.match_clause) res_tp res_eff = - match cl.data with - | Clause(pat, body) -> - let scope = Env.scope env in - let (env, pat, _, r_eff1) = Pattern.check_type ~env ~scope pat tp in - let (body, r_eff2) = check_expr_type env body res_tp res_eff in - (pat, body, ret_effect_join r_eff1 r_eff2) - -and check_match_clauses env tp cls res_tp res_eff = - let (r_eff, cls) = List.fold_left_map - (fun r_eff1 cl -> - let (pat, body, r_eff2) = check_match_clause env tp cl res_tp res_eff in - (ret_effect_join r_eff1 r_eff2, (pat, body))) - Pure - cls - in - (cls, r_eff) - -and make_nonempty_match env tp cls res_tp res_eff = - let pos = - match cls with - | [] -> assert false - | cl :: cls -> - let p1 = cl.S.pos in - let p2 = List.fold_left (fun _ cl -> cl.S.pos) p1 cls in - Position.join p1 p2 - in - let (cls, _) = check_match_clauses env tp cls res_tp res_eff in - let x = Var.fresh () in - let body = - { T.pos; - T.data = T.EMatch({ pos; data = T.EVar x }, cls, res_tp, res_eff) } - in (x, body) - -(* ------------------------------------------------------------------------- *) -(** Check return clauses of handler. - In [check_return_clauses env rcs res_tp res_eff] the meaning of the - parameters is the following. - - [env] -- the environment. - - [rcs] -- list of clauses. If this list is empty, then the default - identity clause is created. - - [res_tp] -- the expected of the return clause - - [ref_eff] -- the expected effect of the return clause - - This function returns triple: a variable bound by the return clause, - its type, and the body of the clause (including pattern-matching). *) -and check_return_clauses env rcs res_tp res_eff = - match rcs with - | [] -> - let x = Var.fresh () in - (x, res_tp, { T.pos = Position.nowhere; T.data = T.EVar x }) - | _ -> - let tp = Env.fresh_uvar env T.Kind.k_type in - let (x, body) = make_nonempty_match env tp rcs res_tp res_eff in - (x, tp, body) - -(* ------------------------------------------------------------------------- *) -(** Check finally clauses of handler. - In [check_finally_clauses env fcs hexpr htp req eff] the meaning of the - parameters is the following. - - [env] -- the environment. - - [fcs] -- list of clauses. If this list is empty, then the equivalent of - the default identity clause is created. - - [hexpr] -- the handler expression, to be wrapped around the finally - clauses. - - [htp] -- the type of the handler expression - - [req] -- type request of the bidirectional type-checking. - - [eff] -- the expected effect of the clauses. - - This function returns a triple with the same meaning as the triple returned - by [tr_expr] function. Handlers are always impure. *) -and check_finally_clauses : type dir. - Env.t -> S.match_clause list -> T.expr -> T.typ -> - (T.typ, dir) request -> T.effrow -> - T.expr * (T.typ, dir) response * ret_effect = - fun env fcs hexpr htp req eff -> - match fcs with - | [] -> - begin match req with - | Infer -> (hexpr, Infered htp, Impure) - | Check tp -> - Error.check_unify_result ~pos:hexpr.pos - (Unification.subtype env htp tp) - ~on_error:(Error.expr_type_mismatch ~env htp tp); - (hexpr, Checked, Impure) - end - | _ -> - let (tp, (resp : (T.typ, dir) response)) = - match req with - | Infer -> - let tp = Env.fresh_uvar env T.Kind.k_type in - (tp, Infered tp) - | Check tp -> (tp, Checked) - in - let (x, body) = make_nonempty_match env htp fcs tp eff in - let expr = - { T.pos = Position.join body.pos hexpr.pos; - T.data = T.ELet(x, T.Scheme.of_type htp, hexpr, body) } - in (expr, resp, Impure) - -(* ------------------------------------------------------------------------- *) -(** Check the sequence of REPL definitions, provided by a user. Always - in type-check mode. *) -and check_repl_def_seq env ienv def_seq tp eff = - let func () = - match def_seq () with - | Seq.Nil -> assert false - | Seq.Cons(def, def_seq) -> - let cont (type dir) env ienv (tp_req : (_, dir) request) eff : - _ * (_, dir) response * _ = - match tp_req with - | Check tp -> - let e = check_repl_def_seq env ienv def_seq tp eff in - (e, Checked, Impure) - | Infer -> - let tp = Env.fresh_uvar env T.Kind.k_type in - let e = check_repl_def_seq env ienv def_seq tp eff in - (e, Infered tp, Impure) - in - let (e, Checked, _) = - check_def env ienv def (Check tp) eff { run = cont } in - e - in - let e = - { T.pos = Position.nowhere; - T.data = T.ERepl(func, tp, eff) - } in - e - -(* ------------------------------------------------------------------------- *) -(** Check expression put into REPL *) -and check_repl_expr env ienv e eff = - let (env1, ims) = ImplicitEnv.begin_generalize env ienv in - let (e, tp, r_eff) = infer_expr_type env e eff in - ImplicitEnv.end_generalize_impure ~pos:e.pos ~env:env1 ims tp; - let pp_ctx = Pretty.empty_context () in - (e, Pretty.type_to_string pp_ctx env tp, r_eff) + (check_repl_def_seq ~tcfix env ImplicitEnv.empty def_seq tp eff, Impure) diff --git a/src/TypeInference/Expr.mli b/src/TypeInference/Expr.mli new file mode 100644 index 00000000..4b4c9f41 --- /dev/null +++ b/src/TypeInference/Expr.mli @@ -0,0 +1,19 @@ +(* This file is part of DBL, released under MIT license. + * See LICENSE for details. + *) + +(** Type-inference for expressions and related syntactic categories *) + +open Common +open TypeCheckFix + +(** Infer type of an expression. The effect of an expression is always in + the check mode. However, pure expressions may returns an information that + they are pure (see [ret_effect] type). *) +val infer_expr_type : tcfix:tcfix -> + Env.t -> S.expr -> T.effrow -> T.expr * T.typ * ret_effect + +(** Check type and effect of an expression. Returns also information about + the purity of an expression. *) +val check_expr_type : tcfix:tcfix -> + Env.t -> S.expr -> T.typ -> T.effrow -> T.expr * ret_effect diff --git a/src/TypeInference/Main.ml b/src/TypeInference/Main.ml index 57e6f8f9..d2a045df 100644 --- a/src/TypeInference/Main.ml +++ b/src/TypeInference/Main.ml @@ -5,9 +5,26 @@ (** Main module of a type inference *) open Common +open TypeCheckFix + +(** Module of mutually recursive functions of the type-checker. + See [TypeCheckFix] for more details. *) +module rec TCFix : TCFix = struct + let infer_expr_type env e eff = + Expr.infer_expr_type ~tcfix:(module TCFix) env e eff + + let check_expr_type env e tp eff = + Expr.check_expr_type ~tcfix:(module TCFix) env e tp eff + + let check_def env ienv def tp_req eff cont = + Def.check_def ~tcfix:(module TCFix) env ienv def tp_req eff cont + + let check_defs env ienv defs tp_req eff cont = + Def.check_defs ~tcfix:(module TCFix) env ienv defs tp_req eff cont +end let tr_program p = let (p, _) = - Expr.check_expr_type Env.empty p T.Type.t_unit T.Effect.io in + TCFix.check_expr_type Env.empty p T.Type.t_unit T.Effect.io in InterpLib.Error.assert_no_error (); p diff --git a/src/TypeInference/MatchClause.ml b/src/TypeInference/MatchClause.ml new file mode 100644 index 00000000..5955c2d2 --- /dev/null +++ b/src/TypeInference/MatchClause.ml @@ -0,0 +1,88 @@ +(* This file is part of DBL, released under MIT license. + * See LICENSE for details. + *) + +(** Type-inference for match clauses and related constructs *) + +open Common +open TypeCheckFix + +let check_match_clause ~tcfix env tp (cl : S.match_clause) res_tp res_eff = + let open (val tcfix : TCFix) in + match cl.data with + | Clause(pat, body) -> + let scope = Env.scope env in + let (env, pat, _, r_eff1) = Pattern.check_type ~env ~scope pat tp in + let (body, r_eff2) = check_expr_type env body res_tp res_eff in + (pat, body, ret_effect_join r_eff1 r_eff2) + +let check_match_clauses ~tcfix env tp cls res_tp res_eff = + let (r_eff, cls) = List.fold_left_map + (fun r_eff1 cl -> + let (pat, body, r_eff2) = + check_match_clause ~tcfix env tp cl res_tp res_eff in + (ret_effect_join r_eff1 r_eff2, (pat, body))) + Pure + cls + in + (cls, r_eff) + +(* ------------------------------------------------------------------------- *) +(** Make pattern-matching expression for given non-empty clause list (the + meaning of parameters is the same as for [check_match_clauses]). It returns + fresh variable [x], and match-expression that matches [x] against given list + of clauses. *) +let make_nonempty_match ~tcfix env tp cls res_tp res_eff = + let pos = + match cls with + | [] -> assert false + | cl :: cls -> + let p1 = cl.S.pos in + let p2 = List.fold_left (fun _ cl -> cl.S.pos) p1 cls in + Position.join p1 p2 + in + let (cls, _) = check_match_clauses ~tcfix env tp cls res_tp res_eff in + let x = Var.fresh () in + let body = + { T.pos; + T.data = T.EMatch({ pos; data = T.EVar x }, cls, res_tp, res_eff) } + in (x, body) + +(* ------------------------------------------------------------------------- *) +let check_return_clauses ~tcfix env rcs res_tp res_eff = + match rcs with + | [] -> + let x = Var.fresh () in + (x, res_tp, { T.pos = Position.nowhere; T.data = T.EVar x }) + | _ -> + let tp = Env.fresh_uvar env T.Kind.k_type in + let (x, body) = make_nonempty_match ~tcfix env tp rcs res_tp res_eff in + (x, tp, body) + +(* ------------------------------------------------------------------------- *) +let check_finally_clauses (type dir) + ~tcfix env fcs hexpr htp (req : (T.typ, dir) request) eff : + T.expr * (T.typ, dir) response * ret_effect = + match fcs with + | [] -> + begin match req with + | Infer -> (hexpr, Infered htp, Impure) + | Check tp -> + Error.check_unify_result ~pos:hexpr.pos + (Unification.subtype env htp tp) + ~on_error:(Error.expr_type_mismatch ~env htp tp); + (hexpr, Checked, Impure) + end + | _ -> + let (tp, (resp : (T.typ, dir) response)) = + match req with + | Infer -> + let tp = Env.fresh_uvar env T.Kind.k_type in + (tp, Infered tp) + | Check tp -> (tp, Checked) + in + let (x, body) = make_nonempty_match ~tcfix env htp fcs tp eff in + let expr = + { T.pos = Position.join body.pos hexpr.pos; + T.data = T.ELet(x, T.Scheme.of_type htp, hexpr, body) } + in (expr, resp, Impure) diff --git a/src/TypeInference/MatchClause.mli b/src/TypeInference/MatchClause.mli new file mode 100644 index 00000000..a40783a2 --- /dev/null +++ b/src/TypeInference/MatchClause.mli @@ -0,0 +1,55 @@ +(* This file is part of DBL, released under MIT license. + * See LICENSE for details. + *) + +(** Type-inference for match clauses and related constructs *) + +open Common +open TypeCheckFix + +(** Check pattern-matching clauses + In [check_match_clauses env tp cls res_tp res_eff] the parameters have the + following meaning: + - [env] -- an environment + - [tp] -- type of the matched expression + - [cls] -- list of clauses + - [res_tp] -- returned type + - [res_eff] -- returned effect *) +val check_match_clauses : tcfix:tcfix -> + Env.t -> T.typ -> S.match_clause list -> T.typ -> T.effrow -> + T.match_clause list * ret_effect + +(* ------------------------------------------------------------------------- *) +(** Check return clauses of handler. + In [check_return_clauses env rcs res_tp res_eff] the meaning of the + parameters is the following. + - [env] -- the environment. + - [rcs] -- list of clauses. If this list is empty, then the default + identity clause is created. + - [res_tp] -- the expected of the return clause + - [ref_eff] -- the expected effect of the return clause + + This function returns triple: a variable bound by the return clause, + its type, and the body of the clause (including pattern-matching). *) +val check_return_clauses : tcfix:tcfix -> + Env.t -> S.match_clause list -> T.typ -> T.effrow -> + T.var * T.typ * T.expr + +(** Check finally clauses of handler. + In [check_finally_clauses env fcs hexpr htp req eff] the meaning of the + parameters is the following. + - [env] -- the environment. + - [fcs] -- list of clauses. If this list is empty, then the equivalent of + the default identity clause is created. + - [hexpr] -- the handler expression, to be wrapped around the finally + clauses. + - [htp] -- the type of the handler expression + - [req] -- type request of the bidirectional type-checking. + - [eff] -- the expected effect of the clauses. + + This function returns a triple with the same meaning as the triple returned + by [tr_expr] function. Handlers are always impure. *) +val check_finally_clauses : tcfix:tcfix -> + Env.t -> S.match_clause list -> T.expr -> T.typ -> + (T.typ, 'dir) request -> T.effrow -> + T.expr * (T.typ, 'dir) response * ret_effect diff --git a/src/TypeInference/PolyExpr.ml b/src/TypeInference/PolyExpr.ml new file mode 100644 index 00000000..4fff0605 --- /dev/null +++ b/src/TypeInference/PolyExpr.ml @@ -0,0 +1,165 @@ +(* This file is part of DBL, released under MIT license. + * See LICENSE for details. + *) + +(** Scheme-inference for polymorphic expressions and related constructs: + actual parameters, and explicit instantiations. *) + +open Common +open TypeCheckFix + +type inst_context = + T.expr -> T.typ -> ret_effect -> T.expr * T.typ * ret_effect + +type simple_context = T.expr -> T.expr + +(* ------------------------------------------------------------------------- *) +(** Context of a method call, returned by [infer_poly_scheme] *) +let method_call_ctx ~pos ~env ~self ~self_tp ~self_r_eff ~eff = + fun e method_tp r_eff -> + let result_expr = { T.pos = pos; T.data = T.EApp(e, self) } in + match T.Type.view method_tp with + | TArrow( + { sch_targs = []; sch_named = []; sch_body = self_tp' }, + res_tp, res_eff) -> + Error.check_unify_result ~pos:self.pos + (Unification.subtype env self_tp self_tp') + ~on_error:(Error.expr_type_mismatch ~env self_tp self_tp'); + Error.check_unify_result ~pos + (Unification.subeffect env res_eff eff) + ~on_error:(Error.method_effect_mismatch ~env res_eff eff); + (* The method is impure, so the result is impure too. *) + (result_expr, res_tp, Impure) + | TPureArrow( + { sch_targs = []; sch_named = []; sch_body = self_tp' }, + res_tp) -> + Error.check_unify_result ~pos:self.pos + (Unification.subtype env self_tp self_tp') + ~on_error:(Error.expr_type_mismatch ~env self_tp self_tp'); + (result_expr, res_tp, ret_effect_join self_r_eff r_eff) + | _ -> + (* Method must be an arrow with monomorphic argument *) + InterpLib.InternalError.report ~reason:"invalid method type" () + +(* ------------------------------------------------------------------------- *) +(** Default instantiation context. *) +let default_ctx e tp r_eff = (e, tp, r_eff) + +(* ------------------------------------------------------------------------- *) +(** Infer scheme of regular variable *) +let infer_var_scheme ~pos env x = + match Env.lookup_var env x with + | Some (VI_Var(x, sch)) -> + ({ T.pos = pos; T.data = T.EVar x }, sch) + | Some (VI_Ctor(idx, info)) -> + let ctor = List.nth info.adt_ctors idx in + let targs = info.adt_args @ ctor.ctor_targs in + let sch = { + T.sch_targs = targs; + T.sch_named = ctor.ctor_named; + T.sch_body = T.Type.t_pure_arrows ctor.ctor_arg_schemes info.adt_type + } in + (ExprUtils.ctor_func ~pos idx info, sch) + | Some (VI_MethodFn name) -> + Error.fatal (Error.method_fn_without_arg ~pos x name) + | None -> + Error.fatal (Error.unbound_var ~pos x) + +(* ------------------------------------------------------------------------- *) +(** Infer scheme of a named implicit *) +let infer_implicit_scheme ~pos env name = + match Env.lookup_implicit env name with + | Some (x, sch, on_use) -> + on_use pos; + ({ T.pos = pos; T.data = T.EVar x }, sch) + | None -> + Error.fatal (Error.unbound_implicit ~pos name) + +(* ------------------------------------------------------------------------- *) +let infer_scheme ~tcfix env (e : S.poly_expr) eff = + let open (val tcfix : TCFix) in + let pos = e.pos in + match e.data with + | EVar x -> + let (e, sch) = infer_var_scheme ~pos env x in + (default_ctx, e, sch, T.TVar.Map.empty) + | EImplicit n -> + let (e, sch) = infer_implicit_scheme ~pos env n in + (default_ctx, e, sch, T.TVar.Map.empty) + | EMethod(self, name) -> + let (self, self_tp, self_r_eff) = infer_expr_type env self eff in + begin match T.Type.whnf self_tp with + | Whnf_Neutral(NH_Var a, _) -> + begin match Env.lookup_method env a name with + | Some(x, sch) -> + (method_call_ctx ~pos ~env ~self ~self_tp ~self_r_eff ~eff, + { T.pos = pos; T.data = T.EVar x }, + sch, + TypeHints.method_inst_hints sch self_tp) + | None -> + Error.fatal (Error.unbound_method ~pos ~env a name) + end + | Whnf_Neutral(NH_UVar _, _) -> + Error.fatal (Error.method_call_on_unknown_type ~pos:e.pos) + + | Whnf_PureArrow _ | Whnf_Arrow _ | Whnf_Handler _ + | Whnf_Label _ -> + Error.fatal (Error.method_call_on_invalid_type ~pos:e.pos ~env self_tp) + + | Whnf_Effect _ | Whnf_Effrow _ -> + failwith "Internal kind error" + end + +(* ------------------------------------------------------------------------- *) +let check_actual_arg ~tcfix env (arg : S.expr) sch eff = + let open (val tcfix : TCFix) in + let (env, tvars, named, body_tp) = + TypeUtils.open_scheme ~pos:arg.pos env sch in + let (body, res_eff) = + match tvars, named with + | [], [] -> check_expr_type env arg body_tp eff + | _ -> + let (body, res_eff) = check_expr_type env arg body_tp T.Effect.pure in + begin match res_eff with + | Pure -> () + | Impure -> Error.report (Error.func_not_pure ~pos:arg.pos) + end; + (body, Pure) + in + (ExprUtils.make_tfun tvars (ExprUtils.make_nfun named body), res_eff) + +(* ------------------------------------------------------------------------- *) +let rec check_explicit_insts ~tcfix + env named (insts : S.inst list) (cache : TypeHints.inst_cache) eff = + let open (val tcfix : TCFix) in + match insts with + | [] -> (Fun.id, [], Pure) + | { data = (n, e); pos } :: insts -> + let make data = { T.data; T.pos } in + let n = Name.tr_name env n in + let (e, sch, r_eff1) = + match T.Name.assoc n named with + | Some sch -> + begin match T.Name.assoc n cache with + | None -> + let (e, r_eff1) = + check_actual_arg ~tcfix env e sch eff in + (e, sch, r_eff1) + | Some (e, tp, r_eff1) -> + assert (T.Scheme.is_monomorphic sch); + Error.check_unify_result ~pos:e.pos + (Unification.subtype env tp sch.sch_body) + ~on_error:(Error.named_param_type_mismatch ~env n tp sch.sch_body); + (e, sch, r_eff1) + end + | None -> + Error.warn (Error.redundant_named_parameter ~pos n); + let (e, tp, r_eff1) = infer_expr_type env e eff in + (e, T.Scheme.of_type tp, r_eff1) + in + let (ctx, insts, r_eff2) = + check_explicit_insts ~tcfix env named insts cache eff in + let x = Var.fresh () in + let ctx e0 = make (T.ELet(x, sch, e, ctx e0)) in + let insts = (n, make (T.EVar x)) :: insts in + (ctx, insts, ret_effect_join r_eff1 r_eff2) diff --git a/src/TypeInference/PolyExpr.mli b/src/TypeInference/PolyExpr.mli new file mode 100644 index 00000000..1210c083 --- /dev/null +++ b/src/TypeInference/PolyExpr.mli @@ -0,0 +1,44 @@ +(* This file is part of DBL, released under MIT license. + * See LICENSE for details. + *) + +(** Scheme-inference for polymorphic expressions and related constructs: + actual parameters, and explicit instantiations. *) + +open Common +open TypeCheckFix + +(** Instantiation context of polymorphic expression. The context is a function + that takes instantiated expression, its type and effect, and returns + translated expression, its type and the effect. Instantiation contexts are + important in case of method calls, because the self parameter should be + computed before instantiation and supplied as a additional parameter, after + instantiation. *) +type inst_context = + T.expr -> T.typ -> ret_effect -> T.expr * T.typ * ret_effect + +(** Simple instantiation context, that do not interact with types *) +type simple_context = T.expr -> T.expr + +(** Infer scheme of a polymorphic expression. The effect of en expression is + always in the check-mode. It returns a tuple, that contains the context of + the polymorphic expression (computing polymorphic expression may have some + effects, that should be performed before explicit instantiation), the + translated polymorphic expression, its scheme, and the hints for the scheme + instantiation. *) +val infer_scheme : tcfix:tcfix -> + Env.t -> S.poly_expr -> T.effrow -> + inst_context * T.expr * T.scheme * TypeHints.t + +(** Check the scheme of an actual parameter of a function *) +val check_actual_arg : tcfix:tcfix -> + Env.t -> S.expr -> T.scheme -> T.effrow -> T.expr * ret_effect + +(** Check explicit instantiations against given list of named parameters (from + type scheme). It returns context (represented as meta-function) that + preserves the order of computations, list of checked instantiations, and + the effect. *) +val check_explicit_insts : tcfix:tcfix -> + Env.t -> + T.named_scheme list -> S.inst list -> TypeHints.inst_cache -> T.effrow -> + simple_context * (T.name * T.expr) list * ret_effect diff --git a/src/TypeInference/TypeCheckFix.ml b/src/TypeInference/TypeCheckFix.ml new file mode 100644 index 00000000..832db82b --- /dev/null +++ b/src/TypeInference/TypeCheckFix.ml @@ -0,0 +1,55 @@ +(* This file is part of DBL, released under MIT license. + * See LICENSE for details. + *) + +(** Signatures of mutually recursive functions defined across several + modules. *) + +open Common + +(** Type of continuation used to type-checking of definitions. It is defined + as record, in order to allow it to be polymorphic in a direction of type + checking. *) +type def_cont = + { run : 'dir. + Env.t -> ImplicitEnv.t -> (T.typ, 'dir) request -> T.effrow -> + T.expr * (T.typ, 'dir) response * ret_effect + } + +(** Unfortunately, OCaml does not support mutually recursive modules defined + in several files. For this reason, some functions of the type-checker takes + as a parameter a module with mutually recursive functions. The variant of + these functions with this additional module parameter can be defined in + separate modules, but at some point, they should be packed into single + recursive module, passed as the first parameter for them. See + [TypeInference.Main] for this recursive definition. *) +module type TCFix = sig + (** Infer type of an expression. The effect of an expression is always in + the check mode. However, pure expressions may returns an information that + they are pure (see [ret_effect] type). *) + val infer_expr_type : + Env.t -> S.expr -> T.effrow -> T.expr * T.typ * ret_effect + + (** Check type and effect of an expression. Returns also information about + the purity of an expression. *) + val check_expr_type : + Env.t -> S.expr -> T.typ -> T.effrow -> T.expr * ret_effect + + (** Check type and effect of a single definition. It uses bidirectional + type checking, and pass the extended environment to the body-generating + continuation. *) + val check_def : + Env.t -> ImplicitEnv.t -> S.def -> + (T.typ, 'dir) request -> T.effrow -> def_cont -> + T.expr * (T.typ, 'dir) response * ret_effect + + (** Check type and effect of a block of definitions. It uses bidirectional + type checking, and pass the extended environment to the body-generating + continuation. *) + val check_defs : + Env.t -> ImplicitEnv.t -> S.def list -> + (T.typ, 'dir) request -> T.effrow -> def_cont -> + T.expr * (T.typ, 'dir) response * ret_effect +end + +type tcfix = (module TCFix) diff --git a/src/TypeInference/TypeHints.ml b/src/TypeInference/TypeHints.ml new file mode 100644 index 00000000..19b32b4c --- /dev/null +++ b/src/TypeInference/TypeHints.ml @@ -0,0 +1,111 @@ +(* This file is part of DBL, released under MIT license. + * See LICENSE for details. + *) + +(** Extraction of type hints *) + +open Common +open TypeCheckFix + +type t = T.typ T.TVar.Map.t +type inst_cache = (T.name * (T.expr * T.typ * ret_effect)) list + +let merge_hints hints1 hints2 = + T.TVar.Map.merge + (fun _ h1 h2 -> + match h1 with + | Some tp -> Some tp + | None -> h2) + hints1 + hints2 + +let update_hints hints s_tp tp = + match T.Type.view s_tp with + | TVar x when T.TVar.Map.mem x hints -> + T.TVar.Map.add x (Some tp) hints + | _ -> hints + +let method_inst_hints (sch : T.scheme) self_tp = + (* initial map, with all type variables bound by the scheme *) + let hints = + sch.sch_targs + |> List.map (fun (_, x) -> (x, None)) + |> List.to_seq |> T.TVar.Map.of_seq + in + let self_sch_s = + match T.Type.view sch.sch_body with + | TArrow(sch, _, _) | TPureArrow(sch, _) -> sch + + | _ -> failwith "Internal error: invalid method scheme" + in + assert (List.is_empty self_sch_s.sch_targs); + assert (List.is_empty self_sch_s.sch_named); + match T.Type.whnf self_sch_s.sch_body, T.Type.whnf self_tp with + | Whnf_Neutral(NH_Var a1, s_targs), Whnf_Neutral(NH_Var a2, args) -> + assert (T.TVar.equal a1 a2); + assert (List.length s_targs = List.length args); + List.fold_left2 update_hints hints s_targs args + |> T.TVar.Map.filter_map (fun _ x -> x) + + | _ -> failwith "Internal error: invalid method scheme" + +let type_inst_hints sch_targs req_tp act_tp = + match T.Type.whnf req_tp, T.Type.whnf act_tp with + | Whnf_Neutral(NH_Var a1, args1), Whnf_Neutral(NH_Var a2, args2) + when T.TVar.equal a1 a2 -> + assert (List.length args1 = List.length args2); + (* initial map, with all type variables bound by the scheme *) + let hints = + sch_targs + |> List.map (fun (_, x) -> (x, None)) + |> List.to_seq |> T.TVar.Map.of_seq + in + List.fold_left2 update_hints hints args1 args2 + |> T.TVar.Map.filter_map (fun _ x -> x) + + | _ -> T.TVar.Map.empty + +(* ------------------------------------------------------------------------- *) +let extract_implicit_type_hints ~tcfix ~pos env (sch : T.scheme) inst eff = + let open (val tcfix : TCFix) in + let targs = sch.sch_targs in + let inst = + List.map (fun { T.data = (n, e); _ } -> (Name.tr_name env n, e)) inst in + let rec loop hints cache named = + match named with + | [] -> (hints, cache) + | (name, arg_sch) :: named + when T.Scheme.is_monomorphic arg_sch + && TypeUtils.is_tvar_neutral arg_sch.sch_body -> + let expr_opt = + match T.Name.assoc name inst with + | None -> + let make data = { S.pos = pos; S.data = data } in + begin match name with + | NLabel | NVar _ | NMethod _ -> None + | NImplicit n -> + (* type hints can be extracted only from monomorphic implicits + (and explicit instantiation, of course), in order to avoid + infinite loops: implicit parameters can depend on itself. *) + begin match Env.lookup_implicit env (NPName n) with + | Some(_, isch, _) when T.Scheme.is_monomorphic isch -> + Some (make (S.EPoly(make (S.EImplicit (S.NPName n)), [], []))) + | _ -> None + end + end + | Some e -> Some e + in + begin match expr_opt with + | None -> loop hints cache named + | Some e -> + let (e, tp, r_eff) = infer_expr_type env e eff in + let hints2 = type_inst_hints targs arg_sch.sch_body tp in + loop + (merge_hints hints hints2) + ((name, (e, tp, r_eff)) :: cache) + named + end + | _ :: named -> + loop hints cache named + in + loop T.TVar.Map.empty [] sch.sch_named diff --git a/src/TypeInference/TypeHints.mli b/src/TypeInference/TypeHints.mli new file mode 100644 index 00000000..7edfa70a --- /dev/null +++ b/src/TypeInference/TypeHints.mli @@ -0,0 +1,47 @@ +(* This file is part of DBL, released under MIT license. + * See LICENSE for details. + *) + +(** Extraction of type hints + + In order to avoid some ambiguities during type inference, unification + variables of an effect kind are forbidden. This makes instantiation of + polymorphic scheme much more complicated. Normally, type parameters that + were not explicitly provided are guessed by instantiating them with fresh + unification variables. However, for effect parameters we need another + solution: some of type parameters are inferred based on types of actual + parameters. *) + +open Common +open TypeCheckFix + +(** Type hints *) +type t = T.typ T.TVar.Map.t + +(** Cached translated explicit instantiations. During extraction of type hints + type of some of named parameters is inferred. This parameters are stored in + the cache in order to not infer their types again. *) +type inst_cache = (T.name * (T.expr * T.typ * ret_effect)) list + +(** Merge type hints *) +val merge_hints : t -> t -> t + +(** Get type instantiation hints, by matching the method scheme with the + actual type of the "self" value. Returned hints are a partial map from + type variables bound by the scheme to types. It assumes that the scheme + is valid for given self type, i.e., is a function scheme, where the + argument is monomorphic neutral type with the same head as the self type. *) +val method_inst_hints : T.scheme -> T.typ -> t + +(** Get type instantiation hints, by matching requested argument type + (the second parameter) with its actual type (the third parameter). + The first parameter is a list of types generalized by a scheme to be + instantiated. *) +val type_inst_hints : T.named_tvar list -> T.typ -> T.typ -> t + +(** Extracts type hints for a type scheme from environment and explicit + instantiation. Returns hints and cached translated explicit + instantiations. *) +val extract_implicit_type_hints : tcfix:tcfix -> + pos:Position.t -> Env.t -> T.scheme -> S.inst list -> T.effrow -> + t * inst_cache diff --git a/src/TypeInference/TypeUtils.ml b/src/TypeInference/TypeUtils.ml index c1b393ab..f235d906 100644 --- a/src/TypeInference/TypeUtils.ml +++ b/src/TypeInference/TypeUtils.ml @@ -58,58 +58,3 @@ let open_scheme ~pos (env : Env.t) (sch : T.scheme) = env sch.sch_named in (env, sch.sch_targs, ims, sch.sch_body) - -let merge_hints hints1 hints2 = - T.TVar.Map.merge - (fun _ h1 h2 -> - match h1 with - | Some tp -> Some tp - | None -> h2) - hints1 - hints2 - -let update_hints hints s_tp tp = - match T.Type.view s_tp with - | TVar x when T.TVar.Map.mem x hints -> - T.TVar.Map.add x (Some tp) hints - | _ -> hints - -let method_inst_hints (sch : T.scheme) self_tp = - (* initial map, with all type variables bound by the scheme *) - let hints = - sch.sch_targs - |> List.map (fun (_, x) -> (x, None)) - |> List.to_seq |> T.TVar.Map.of_seq - in - let self_sch_s = - match T.Type.view sch.sch_body with - | TArrow(sch, _, _) | TPureArrow(sch, _) -> sch - - | _ -> failwith "Internal error: invalid method scheme" - in - assert (List.is_empty self_sch_s.sch_targs); - assert (List.is_empty self_sch_s.sch_named); - match T.Type.whnf self_sch_s.sch_body, T.Type.whnf self_tp with - | Whnf_Neutral(NH_Var a1, s_targs), Whnf_Neutral(NH_Var a2, args) -> - assert (T.TVar.equal a1 a2); - assert (List.length s_targs = List.length args); - List.fold_left2 update_hints hints s_targs args - |> T.TVar.Map.filter_map (fun _ x -> x) - - | _ -> failwith "Internal error: invalid method scheme" - -let type_inst_hints sch_targs req_tp act_tp = - match T.Type.whnf req_tp, T.Type.whnf act_tp with - | Whnf_Neutral(NH_Var a1, args1), Whnf_Neutral(NH_Var a2, args2) - when T.TVar.equal a1 a2 -> - assert (List.length args1 = List.length args2); - (* initial map, with all type variables bound by the scheme *) - let hints = - sch_targs - |> List.map (fun (_, x) -> (x, None)) - |> List.to_seq |> T.TVar.Map.of_seq - in - List.fold_left2 update_hints hints args1 args2 - |> T.TVar.Map.filter_map (fun _ x -> x) - - | _ -> T.TVar.Map.empty diff --git a/src/TypeInference/TypeUtils.mli b/src/TypeInference/TypeUtils.mli index 6ee7bbbf..947c69f4 100644 --- a/src/TypeInference/TypeUtils.mli +++ b/src/TypeInference/TypeUtils.mli @@ -6,8 +6,6 @@ open Common -type hints = T.typ T.TVar.Map.t - (** Check if type is a neutral type starting with type variable *) val is_tvar_neutral : T.typ -> bool @@ -19,19 +17,3 @@ val method_owner_of_scheme : pos:Position.t -> env:Env.t -> T.scheme -> T.tvar introduced named parameters, and the type of the scheme body. *) val open_scheme : pos:Position.t -> Env.t -> T.scheme -> Env.t * T.named_tvar list * (T.name * T.var * T.scheme) list * T.typ - -(** Merge type hints *) -val merge_hints : hints -> hints -> hints - -(** Get type instantiation hints, by matching the method scheme with the - actual type of the "self" value. Returned hints are a partial map from - type variables bound by the scheme to types. It assumes that the scheme - is valid for given self type, i.e., is a function scheme, where the - argument is monomorphic neutral type with the same head as the self type. *) -val method_inst_hints : T.scheme -> T.typ -> hints - -(** Get type instantiation hints, by matching requested argument type - (the second parameter) with its actual type (the third parameter). - The first parameter is a list of types generalized by a scheme to be - instantiated. *) -val type_inst_hints : T.named_tvar list -> T.typ -> T.typ -> hints