diff --git a/lib/inference.ml b/lib/inference.ml index 27125a6..6c66973 100644 --- a/lib/inference.ml +++ b/lib/inference.ml @@ -58,12 +58,13 @@ let typeof t = (* Nested *) nested_infer env env' ty_fn | None -> None, env) - (* | (Some (Type.Var _ as ty1), _), _ -> - (* On this case we may have a function represented as a variable *) - let ty2 = Type.Arrow (ty1, ty1) in - (match Unification.unify ty1 ty2 with + | (Some (Type.Var _ as ty1), _), _ -> + (* On this case we may have a function represented as a variable *) + (* TODO: Nested application *) + 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) diff --git a/test/test_projet_pfa_23_24.ml b/test/test_projet_pfa_23_24.ml index eff0620..e8c6aa8 100644 --- a/test/test_projet_pfa_23_24.ml +++ b/test/test_projet_pfa_23_24.ml @@ -62,6 +62,13 @@ let tests_typeof = ( Fun (x, Proj (First, Proj (Second, Var x))) , Pair (Pair (IntConst 1, IntConst 2), IntConst 3) )) , Some Type.Int ) + (* ; (* x -> y -> (x -> y -> z) -> z *) + ( "fun x -> fun y -> fun z -> z x y" + , Term.(Fun (x, Fun (y, Fun (z, App (Var z, App (Var x, Var y)))))) + , Some + Type.( + Arrow (Var x, Arrow (Var y, Arrow (Arrow (Var x, Arrow (Var y, Var z)), Var z)))) + ) *) ] ;;