Tried to implement Var and Abs has_type method ...

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)
+        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) ->