From 1fc5a46904e375aeb433c28413e123716a08a743 Mon Sep 17 00:00:00 2001
From: MysaaJava <samyavrillon@netcourrier.com>
Date: Thu, 15 Feb 2024 05:46:29 +0100
Subject: [PATCH] Tried to implement Var and Abs has_type method ...

---
 src/Infer.ml | 22 +++++++++++++++++++---
 1 file changed, 19 insertions(+), 3 deletions(-)

diff --git a/src/Infer.ml b/src/Infer.ml
index 4c72967..8a0ef2a 100644
--- a/src/Infer.ml
+++ b/src/Infer.ml
@@ -83,11 +83,27 @@ module Make(T : Utils.Functor) = struct
   let rec has_type (env : env) (t : Untyped.term) (w : variable) : (STLC.term, err) t =
     match t with
     | Untyped.Var x ->
-      Utils.not_yet "Infer.has_type: Var case" (env, t, w, x)
+      (Option.fold 
+          ~none:(
+            let a = Var.fresh "x" in
+            Exist(a, None, Ret (fun _ -> STLC.Var(x)))
+          ) 
+          ~some:(
+            fun envt -> Map(eq envt w, fun _ -> STLC.Var(x))
+          ) 
+          (Env.find_opt x env)
+      )
     | Untyped.App (t, u) ->
       Utils.not_yet "Infer.has_type: App case" (env, t, u, fun () -> has_type)
-    | Untyped.Abs (x, t) ->
-      Utils.not_yet "Infer.has_type: Abs case" (env, x, t, fun () -> has_type)
+    | Untyped.Abs (x, t) -> 
+        let tau,a,b = Var.fresh "τ",Var.fresh "α", Var.fresh "β" in
+        let newenv = Env.add x a env in
+        Exist(tau, Some (Arrow(a, b)),
+          Map(Conj(
+            has_type newenv t b,
+            eq tau w
+          ), fun t -> let (x,_) = p in x) (* term * unit -> term isomorphism *)
+        )
     | Untyped.Let (x, t, u) ->
       Utils.not_yet "Infer.has_type: Let case" (env, x, t, u, fun () -> has_type)
     | Untyped.Annot (t, ty) ->