nested application

lib/inference.ml

@@ -27,7 +27,10 @@ let typeof t =
          (match TypeSubstitution.find id env' with
           | Some ty -> Some ty, env'
           | None -> None, env')
-       | _ -> None, env)
+       (* Directly the type *)
+       | Some ty, _ -> Some ty, env
+       (* Bad typed *)
+       | None, _ -> None, env)
     | Term.Fun (id, body) ->
       let arg = TypeSubstitution.singleton id (Type.Var id) in
       (match infer (TypeSubstitution.compose arg env) body with
@@ -39,14 +42,21 @@ let typeof t =
     | Term.App (t1, t2) ->
       (* Infer the type of t1 and t2 *)
       (match infer env t1, infer env t2 with
-       | (Some (Type.Arrow (ty_param, _)), _), (Some ty_args, _) ->
+       | (Some (Type.Arrow (ty_param, ty_fn)), _), (Some ty_args, _) ->
          (* Check if the argument type matches the parameter type *)
          (match Unification.unify ty_param ty_args with
           | Some env' ->
-            (* Infer again now that we have some extra typing infos *)
+            let rec nested_infer oldenv currenv final =
-            (match infer env' t1 with
+              if TypeSubstitution.equal oldenv currenv
-             | Some (Type.Arrow (_, ty_fn)), env'' -> Some ty_fn, env''
+              then Some final, currenv
-             | _ -> None, env)
+              else (
+                match infer currenv t1 with
+                | Some (Type.Arrow (_, ty_fn)), newenv ->
+                  nested_infer currenv newenv ty_fn
+                | _ -> None, currenv)
+            in
+            (* 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 *)

lib/typeSubstitution.ml

@@ -24,7 +24,6 @@ let rec apply subst = function
 
 (** Compose two substitutions, last with priority *)
 let compose s2 s1 =
-  let merger =
   IdentifierMap.merge
     (* ID type_s1 type_s2 *)
       (fun _ ty1 ty2 ->
@@ -38,8 +37,6 @@ let compose s2 s1 =
       | None, None -> None)
     s1
     s2
-  in
-  merger
 ;;
 
 let to_string map =
@@ -57,3 +54,24 @@ let to_string map =
 ;;
 
 let find = IdentifierMap.find_opt
+
+let equal map1 map2 =
+  let l_map1 = List.length (IdentifierMap.bindings map1) in
+  let l_map2 = List.length (IdentifierMap.bindings map2) in
+  if l_map1 = l_map2 && l_map1 = 0
+  then (* Two empty maps *)
+    true
+  else (
+    (* Iterate over the largest map *)
+    let map_forall, map_find = if l_map1 > l_map2 then map1, map2 else map2, map1 in
+    IdentifierMap.for_all
+      (fun key value ->
+        match IdentifierMap.find_opt key map_find with
+        | Some value' ->
+          (* Equality between the two keys *)
+          value = value'
+        | _ ->
+          (* Key in map_find doesn't exists in map_forall *)
+          false)
+      map_forall)
+;;

lib/typeSubstitution.mli

@@ -8,3 +8,4 @@ val empty : t
 val singleton : Identifier.t -> Type.t -> t
 val find : Identifier.t -> t -> Type.t option
 val to_string : t -> string
+val equal : t -> t -> bool

test/test_projet_pfa_23_24.ml

@@ -51,6 +51,17 @@ let tests_typeof =
     , Term.(
         App (App (Fun (x, Fun (y, Binop (Var x, Plus, Var y))), IntConst 3), IntConst 4))
     , Some Type.Int )
+  ; (* Function with nested pair *)
+    ( "(fun x -> fst x) (1, 2)"
+    , Term.(App (Fun (x, Proj (First, Var x)), Pair (IntConst 1, IntConst 2)))
+    , Some Type.Int )
+  ; (* Function application with nested pair and projection *)
+    ( "(fun x -> fst (snd x)) ((1, 2), 3)"
+    , Term.(
+        App
+          ( Fun (x, Proj (First, Proj (Second, Var x)))
+          , Pair (Pair (IntConst 1, IntConst 2), IntConst 3) ))
+    , Some Type.Int )
   ]
 ;;