From b2be96a0f5920e583027a70d41ce29b49f81d02d Mon Sep 17 00:00:00 2001 From: Mylloon Date: Sun, 14 Apr 2024 03:49:59 +0200 Subject: [PATCH] a try --- lib/inference.ml | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/lib/inference.ml b/lib/inference.ml index 89b5e96..2ddb9b6 100644 --- a/lib/inference.ml +++ b/lib/inference.ml @@ -35,14 +35,21 @@ let typeof t = | None, _ -> Some (Type.Arrow (Type.Var id, ty_body)), env') | _ -> None, env) | Term.App (t1, t2) -> - (* TODO: When a variable is a function *) + (* Infer the type of t1 and t2 *) (match infer env t1, infer env t2 with | (Some (Type.Arrow (ty_param, ty_fn)), _), (Some ty_args, _) -> - (* Check if the function type matches the arguments *) + (* Check if the argument type matches the parameter type *) (match Unification.unify ty_param ty_args with | Some _ -> Some ty_fn, env | None -> None, env) - | _, _ -> None, env) + | (Some _ (* (Type.Var _ as ty1) *), _), _ -> + (* On this case we may have a function represented as the variable *) + (* let ty2 = Type.Arrow (ty1, ty1) in + (match Unification.unify ty1 ty2 with + | Some env' -> Some ty2, env' + | _ -> None, env) *) + None, env + | _ -> None, env) in fst (infer TypeSubstitution.empty t) ;;