From 83b2039262459219751ad3f5913151490c47f8ce Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Thu, 14 Mar 2024 22:24:38 +0100
Subject: [PATCH] * Add dummy implementation * Add Identifier.t * WIP: typeof?
 (idk what Im doing)

---
 lib/identifier.ml       |  9 +++++++++
 lib/identifier.mli      |  3 +--
 lib/inference.ml        | 19 +++++++++++++++++++
 lib/term.ml             | 21 +++++++++++++++++++++
 lib/type.ml             |  6 ++++++
 lib/typeSubstitution.ml |  4 ++++
 lib/unification.ml      |  1 +
 7 files changed, 61 insertions(+), 2 deletions(-)
 create mode 100644 lib/identifier.ml
 create mode 100644 lib/inference.ml
 create mode 100644 lib/term.ml
 create mode 100644 lib/type.ml
 create mode 100644 lib/typeSubstitution.ml
 create mode 100644 lib/unification.ml

diff --git a/lib/identifier.ml b/lib/identifier.ml
new file mode 100644
index 0000000..50e5bfc
--- /dev/null
+++ b/lib/identifier.ml
@@ -0,0 +1,9 @@
+type t = string [@@deriving eq, ord, show]
+
+let fresh =
+  let r = ref 0 in
+  fun () ->
+    let id = "id_" ^ string_of_int !r in
+    incr r;
+    id
+;;
diff --git a/lib/identifier.mli b/lib/identifier.mli
index 511512f..21bb0d4 100644
--- a/lib/identifier.mli
+++ b/lib/identifier.mli
@@ -1,4 +1,3 @@
-type t (* = ... -> Students, this is your job ! *)
-[@@deriving eq, ord, show]
+type t = string [@@deriving eq, ord, show]
 
 val fresh : unit -> t
diff --git a/lib/inference.ml b/lib/inference.ml
new file mode 100644
index 0000000..e7f78d5
--- /dev/null
+++ b/lib/inference.ml
@@ -0,0 +1,19 @@
+let rec typeof = function
+  | Term.Var _ ->
+    (* Une variable n'a pas de type *)
+    None
+  | Term.IntConst _ -> Some Type.Int
+  | Term.Binop (t1, _, t2) ->
+    (* Les 2 types de l'opération sont égaux *)
+    (match typeof t1, typeof t2 with
+     | Some (_ as ty1), Some (_ as ty2) -> if ty1 = ty2 then Some ty1 else None
+     | _ -> None)
+  | Term.Pair (t1, t2) ->
+    (* On forme le produit *)
+    (match typeof t1, typeof t2 with
+     | Some ty1, Some ty2 -> Some (Type.Product (ty1, ty2))
+     | _ -> None)
+  | Term.Proj (_proj, _t) -> failwith "TODO"
+  | Term.Fun (_, _) -> failwith "TODO"
+  | Term.App (_t1, _t2) -> failwith "TODO"
+;;
diff --git a/lib/term.ml b/lib/term.ml
new file mode 100644
index 0000000..cf9f357
--- /dev/null
+++ b/lib/term.ml
@@ -0,0 +1,21 @@
+type binop =
+  | Plus
+  | Minus
+  | Times
+  | Div
+[@@deriving eq, ord, show]
+
+type projection =
+  | First
+  | Second
+[@@deriving eq, ord, show]
+
+type t =
+  | Var of Identifier.t
+  | IntConst of int
+  | Binop of t * binop * t
+  | Pair of t * t
+  | Proj of projection * t
+  | Fun of Identifier.t * t
+  | App of t * t
+[@@deriving eq, ord, show]
diff --git a/lib/type.ml b/lib/type.ml
new file mode 100644
index 0000000..c3adb3d
--- /dev/null
+++ b/lib/type.ml
@@ -0,0 +1,6 @@
+type t =
+  | Var of Identifier.t
+  | Int
+  | Product of t * t
+  | Arrow of t * t
+[@@deriving eq, ord, show]
diff --git a/lib/typeSubstitution.ml b/lib/typeSubstitution.ml
new file mode 100644
index 0000000..9137223
--- /dev/null
+++ b/lib/typeSubstitution.ml
@@ -0,0 +1,4 @@
+type t = Type.t Map.Make(Identifier).t
+
+let apply _t _tt = failwith "TODO"
+let compose _s2 _s1 = failwith "TODO"
diff --git a/lib/unification.ml b/lib/unification.ml
new file mode 100644
index 0000000..d89600c
--- /dev/null
+++ b/lib/unification.ml
@@ -0,0 +1 @@
+let unify _ty1 _ty2 = failwith "TODO"