From dc1efb51e29bc6fd86fff8ccc1ccea289ec0fcb7 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 30 Apr 2024 13:36:12 +0200
Subject: [PATCH] nested application

---
 lib/inference.ml              | 22 ++++++++++-----
 lib/typeSubstitution.ml       | 50 ++++++++++++++++++++++++-----------
 lib/typeSubstitution.mli      |  1 +
 test/test_projet_pfa_23_24.ml | 11 ++++++++
 4 files changed, 62 insertions(+), 22 deletions(-)

diff --git a/lib/inference.ml b/lib/inference.ml
index 6f38001..27125a6 100644
--- a/lib/inference.ml
+++ b/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 *)
-            (match infer env' t1 with
-             | Some (Type.Arrow (_, ty_fn)), env'' -> Some ty_fn, env''
-             | _ -> None, env)
+            let rec nested_infer oldenv currenv final =
+              if TypeSubstitution.equal oldenv currenv
+              then Some final, currenv
+              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 *)
diff --git a/lib/typeSubstitution.ml b/lib/typeSubstitution.ml
index cce888c..c6a5e41 100644
--- a/lib/typeSubstitution.ml
+++ b/lib/typeSubstitution.ml
@@ -24,22 +24,19 @@ 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 ->
-        match ty1, ty2 with
-        (* Give priority to s1 *)
-        | Some ty1', Some _ -> Some ty1'
-        (* Use of the substitution we already have *)
-        | Some ty1', None -> Some ty1'
-        | None, Some ty2' -> Some ty2'
-        (* Variable untyped *)
-        | None, None -> None)
-      s1
-      s2
-  in
-  merger
+  IdentifierMap.merge
+    (* ID type_s1 type_s2 *)
+      (fun _ ty1 ty2 ->
+      match ty1, ty2 with
+      (* Give priority to s1 *)
+      | Some ty1', Some _ -> Some ty1'
+      (* Use of the substitution we already have *)
+      | Some ty1', None -> Some ty1'
+      | None, Some ty2' -> Some ty2'
+      (* Variable untyped *)
+      | None, None -> None)
+    s1
+    s2
 ;;
 
 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)
+;;
diff --git a/lib/typeSubstitution.mli b/lib/typeSubstitution.mli
index f7d437e..0fe98ee 100644
--- a/lib/typeSubstitution.mli
+++ b/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
diff --git a/test/test_projet_pfa_23_24.ml b/test/test_projet_pfa_23_24.ml
index aa41a34..eff0620 100644
--- a/test/test_projet_pfa_23_24.ml
+++ b/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 )
   ]
 ;;