From c414bf8564671ad5e81985d934f80b5c1068e462 Mon Sep 17 00:00:00 2001
From: Giovanni Bernardi <gio@irif.fr>
Date: Mon, 11 Mar 2024 09:31:56 +0100
Subject: [PATCH] project-inception

---
 README.md                     | 176 ++++++++++++++++++++++++++++++++++
 bin/dune                      |   4 +
 bin/main.ml                   |   1 +
 dune-project                  |  26 +++++
 lib/dune                      |   3 +
 lib/identifier.mli            |   4 +
 lib/inference.mli             |   7 ++
 lib/term.mli                  |  22 +++++
 lib/type.mli                  |   6 ++
 lib/typeSubstitution.mli      |   6 ++
 lib/unification.mli           |  10 ++
 test/dune                     |   3 +
 test/test_projet_pfa_23_24.ml |  19 ++++
 13 files changed, 287 insertions(+)
 create mode 100644 README.md
 create mode 100644 bin/dune
 create mode 100644 bin/main.ml
 create mode 100644 dune-project
 create mode 100644 lib/dune
 create mode 100644 lib/identifier.mli
 create mode 100644 lib/inference.mli
 create mode 100644 lib/term.mli
 create mode 100644 lib/type.mli
 create mode 100644 lib/typeSubstitution.mli
 create mode 100644 lib/unification.mli
 create mode 100644 test/dune
 create mode 100644 test/test_projet_pfa_23_24.ml

diff --git a/README.md b/README.md
new file mode 100644
index 0000000..a3b8d08
--- /dev/null
+++ b/README.md
@@ -0,0 +1,176 @@
+# Project of "Programmation Fonctionelle Avancé"
+
+This file is divided in two parts.
+The first part describes the project that you have to
+realise to get a partial note for the module 
+"Programmation Fonctionelle Avancé".
+
+## PART I: Scientific content the project
+
+To realise this project you will implement a type inference
+algorithm that works over terms of a programming language
+for functional programming.
+
+
+## Terms = Expressions = Programs
+
+- [Term](./lib/term.mli) This module contains the syntax of
+  the minimal programming language to we use in this project.
+  Terms (i.e. programs) are values of type `Term.t`.
+  This language is "applicative", i.e. fit for functional programming,
+  thanks to the constructors for application (`App`) and
+  for function definition (`Fun`).
+
+
+## Aim of the project
+
+The [third lecture]
+(https://gaufre.informatique.univ-paris-diderot.fr/Bernardi/pfa-2324/tree/master/week03)
+describes two algorithms:
+the first one transforms any given program into a system of
+equations, and the second one is a unification algorithm that solves
+such systems.
+
+To realise this project you will have to implement the following modules:
+
+1. [typeSubstitution](./lib/typeSubstituion.ml)
+   You must implement at least:
+   - [ ] `type t`, i.e. how to represent syntactic substitutions in memory,
+   - [ ] `val apply`,  which applies a syntactic substitution to a type
+   - [ ] `val compose`, which computes the substitution obtained composing two given substitutions.
+    
+   
+1. [unifcation](./lib/unification.ml) 
+   You must implement at least:
+   - [ ] `val unify` which given two type `t1` and `t2`, 
+	 must compute the substitution `s` such that if
+	 `unify t1 t2 = Some s` then `apply s t1 = apply s t2`.
+
+   You can of course use the Herbrand / Robinson algorithm
+   to start designing your implementation.
+
+
+1. [inference](./lib/inference.ml)
+   You must implement at least:
+   - [ ] `val typeof`, which given a term  `t` must compute either
+   `None`, if there is no type for `t`, or `Some ty`, if ty is the type of term `t`.
+
+You may add more definitions to each of these modules, and extend their signatures accordingly.
+You may also create new compilation units (i.e. new `.ml` files).
+
+1. You may, and *should*, extend the [testing module](./test/test_projet_pfa_23_24.ml) with additional
+tests, or replace it with a testing framework of your choice (using e.g. QCheck).
+   
+   
+## PART II: Logistics of the project
+
+
+## Fork
+
+To realise your project and have it evaluated,
+you have to
+
+1. fork the git repository that contains this file, and
+1. add G. BERNARDI and G. GEOFFROY with the role `Maintainer` to your fork.
+
+Do it asap.
+
+## Deadline
+
+The final implementation must be in your fork by the
+
+__ 30th of April 2024, 23h59 __
+
+Any code pushed to your fork after that time will be ignored.
+
+
+## Requirements
+
+### 1. Install OPAM
+
+[OPAM](https://opam.ocaml.org/) is the package manager for OCaml. It
+is the recommended way to install the OCaml compiler and OCaml
+packages.
+
+The following should work for macOS and Linux:
+````sh
+bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)"
+````
+
+### Recommended: editor integration
+
+#### Emacs: Tuareg & Merlin
+
+[Tuareg](https://github.com/ocaml/tuareg) is an OCaml major mode for
+Emacs while [Merlin](https://github.com/ocaml/merlin) is an editor
+service that provides modern IDE features for OCaml.
+
+To install, run:
+````sh
+opam install tuareg merlin user-setup
+````
+
+#### VSCode: Ocaml LSP
+
+Install the extension called **OCaml Platform** available in the
+[Visual Studio
+Marketplace](https://marketplace.visualstudio.com/items?itemName=ocamllabs.ocaml-platform)
+
+This extension requires
+[OCaml-LSP](https://github.com/ocaml/ocaml-lsp), an Language Server
+Protocol(LSP) implementation for OCaml
+
+To install, run:
+````sh
+opam install ocaml-lsp-server
+````
+
+## Development environment setup
+
+If the required opam packages conflict with your default switch, you may setup a [local](https://opam.ocaml.org/blog/opam-local-switches/) Opam switch using the following commands:
+
+```
+$ opam switch create . --deps-only --with-doc --with-test
+$ eval $(opam env)
+```
+
+
+## Build
+
+To build the project, type:
+
+```
+$ dune build
+```
+
+For continuous build, use
+
+```
+$ dune build --watch
+```
+
+instead.
+
+## Running your main file
+
+To run your code you will have to implement 
+`let () = ...` in the file  `main.ml`, and
+then run it via
+
+```
+$ dune exec 
+```
+
+## Testing your code
+
+To test the project, type:
+
+```
+$ dune runtest
+```
+
+This can be combined with continuous build & test, using
+
+```
+$ dune runtest --watch
+```
diff --git a/bin/dune b/bin/dune
new file mode 100644
index 0000000..73e1707
--- /dev/null
+++ b/bin/dune
@@ -0,0 +1,4 @@
+(executable
+ (public_name projet_pfa_23_24)
+ (name main)
+ (libraries typeInference))
diff --git a/bin/main.ml b/bin/main.ml
new file mode 100644
index 0000000..7bf6048
--- /dev/null
+++ b/bin/main.ml
@@ -0,0 +1 @@
+let () = print_endline "Hello, World!"
diff --git a/dune-project b/dune-project
new file mode 100644
index 0000000..c9d1fe6
--- /dev/null
+++ b/dune-project
@@ -0,0 +1,26 @@
+(lang dune 3.13)
+
+(name projet_pfa_23_24)
+
+(generate_opam_files true)
+
+(source
+ (github username/reponame))
+
+(authors "Author Name")
+
+(maintainers "Maintainer Name")
+
+(license LICENSE)
+
+(documentation https://url/to/documentation)
+
+(package
+ (name projet_pfa_23_24)
+ (synopsis "A short synopsis")
+ (description "A longer description")
+ (depends ocaml dune alcotest ppx_deriving)
+ (tags
+  (topics "to describe" your project)))
+
+; See the complete stanza docs at https://dune.readthedocs.io/en/stable/dune-files.html#dune-project
diff --git a/lib/dune b/lib/dune
new file mode 100644
index 0000000..4ac3ff4
--- /dev/null
+++ b/lib/dune
@@ -0,0 +1,3 @@
+(library
+ (name typeInference)
+ (preprocess (pps ppx_deriving.show ppx_deriving.ord ppx_deriving.eq)))
diff --git a/lib/identifier.mli b/lib/identifier.mli
new file mode 100644
index 0000000..511512f
--- /dev/null
+++ b/lib/identifier.mli
@@ -0,0 +1,4 @@
+type t (* = ... -> Students, this is your job ! *)
+[@@deriving eq, ord, show]
+
+val fresh : unit -> t
diff --git a/lib/inference.mli b/lib/inference.mli
new file mode 100644
index 0000000..39c9348
--- /dev/null
+++ b/lib/inference.mli
@@ -0,0 +1,7 @@
+(* 
+   If `t` is a term, then `typeof t` must compute
+   - `None`, if there is no type for `t`
+   - `Some ty`, if ty is the type of term `t`
+*)
+val typeof : Term.t -> Type.t option
+    
diff --git a/lib/term.mli b/lib/term.mli
new file mode 100644
index 0000000..cc8da2a
--- /dev/null
+++ b/lib/term.mli
@@ -0,0 +1,22 @@
+(*
+   This module contains the syntax of terms of a minimal programming language.
+*)
+type binop =
+  | Plus | Minus | Times | Div
+  [@@deriving eq, ord, show]
+
+type projection = First | Second
+  [@@deriving eq, ord, show]
+
+(*
+   Every value of type Term.t is the abstract syntax tree of a program.
+*)
+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.mli b/lib/type.mli
new file mode 100644
index 0000000..16eef74
--- /dev/null
+++ b/lib/type.mli
@@ -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.mli b/lib/typeSubstitution.mli
new file mode 100644
index 0000000..92362c7
--- /dev/null
+++ b/lib/typeSubstitution.mli
@@ -0,0 +1,6 @@
+type t = Type.t Map.Make(Identifier).t
+
+val apply : t -> Type.t -> Type.t
+
+(* compose s2 s1 : first s1, then s2 *)
+val compose : t -> t -> t
diff --git a/lib/unification.mli b/lib/unification.mli
new file mode 100644
index 0000000..cc5bf9d
--- /dev/null
+++ b/lib/unification.mli
@@ -0,0 +1,10 @@
+(*
+   The function `unify` must compute the substitution
+   `s` such that if  `unify t1 t2 = Some s` then
+   `apply s t1 = apply s t2`.
+
+   You can use the slides on the Herbrand / Robinson algorithm
+   to start designing your implementation.
+
+*)
+val unify : Type.t -> Type.t -> TypeSubstitution.t option
diff --git a/test/dune b/test/dune
new file mode 100644
index 0000000..1f3f1a9
--- /dev/null
+++ b/test/dune
@@ -0,0 +1,3 @@
+(test
+ (name test_projet_pfa_23_24)
+ (libraries typeInference alcotest))
diff --git a/test/test_projet_pfa_23_24.ml b/test/test_projet_pfa_23_24.ml
new file mode 100644
index 0000000..84b6d75
--- /dev/null
+++ b/test/test_projet_pfa_23_24.ml
@@ -0,0 +1,19 @@
+open TypeInference
+
+let tests_typeof = (* TODO: add more tests *)
+  let x = Identifier.fresh () in
+  let y = Identifier.fresh () in
+  [ ("0", Term.IntConst 0, Some Type.Int);
+    ("fun x -> fun y -> x+y", Term.(Fun (x, Fun (y, Binop (Var x, Plus, Var y)))), Some Type.(Arrow (Int, Arrow (Int, Int)))); ]
+  
+let typeModule = (module Type : Alcotest.TESTABLE with type t = Type.t)
+
+let check_typeof term_text term expected_type =
+  let open Alcotest in
+  test_case term_text `Quick (fun () -> check (option typeModule) "Same type" expected_type (Inference.typeof term))
+
+let () =
+  let open Alcotest in
+  run "Inference" [
+      "typeof", List.map (fun (term_text, term, expected_type) -> check_typeof term_text term expected_type) tests_typeof ;
+    ]