diff --git a/README.md b/README.md index a3b8d08..005c65c 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,7 @@ 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 +realise to get a partial note for the module "Programmation Fonctionelle Avancé". ## PART I: Scientific content the project @@ -11,7 +11,6 @@ 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 @@ -21,7 +20,6 @@ for functional programming. thanks to the constructors for application (`App`) and for function definition (`Fun`). - ## Aim of the project The [third lecture] @@ -35,35 +33,33 @@ 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 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) + +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`. + + - [ ] `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`. + - [ ] `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 +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 @@ -79,11 +75,10 @@ Do it asap. The final implementation must be in your fork by the -__ 30th of April 2024, 23h59 __ +** 30th of April 2024, 23h59 ** Any code pushed to your fork after that time will be ignored. - ## Requirements ### 1. Install OPAM @@ -93,9 +88,10 @@ is the recommended way to install the OCaml compiler and OCaml packages. The following should work for macOS and Linux: -````sh + +```sh bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)" -```` +``` ### Recommended: editor integration @@ -106,9 +102,10 @@ Emacs while [Merlin](https://github.com/ocaml/merlin) is an editor service that provides modern IDE features for OCaml. To install, run: -````sh + +```sh opam install tuareg merlin user-setup -```` +``` #### VSCode: Ocaml LSP @@ -121,9 +118,10 @@ This extension requires Protocol(LSP) implementation for OCaml To install, run: -````sh + +```sh opam install ocaml-lsp-server -```` +``` ## Development environment setup @@ -134,7 +132,6 @@ $ opam switch create . --deps-only --with-doc --with-test $ eval $(opam env) ``` - ## Build To build the project, type: @@ -153,12 +150,12 @@ instead. ## Running your main file -To run your code you will have to implement -`let () = ...` in the file `main.ml`, and +To run your code you will have to implement +`let () = ...` in the file `main.ml`, and then run it via ``` -$ dune exec +$ dune exec ``` ## Testing your code diff --git a/lib/dune b/lib/dune index 4ac3ff4..d907eb4 100644 --- a/lib/dune +++ b/lib/dune @@ -1,3 +1,4 @@ (library (name typeInference) - (preprocess (pps ppx_deriving.show ppx_deriving.ord ppx_deriving.eq))) + (preprocess + (pps ppx_deriving.show ppx_deriving.ord ppx_deriving.eq))) diff --git a/lib/inference.mli b/lib/inference.mli index 39c9348..781a4f1 100644 --- a/lib/inference.mli +++ b/lib/inference.mli @@ -1,7 +1,6 @@ -(* +(* 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/test/test_projet_pfa_23_24.ml b/test/test_projet_pfa_23_24.ml index 84b6d75..c324194 100644 --- a/test/test_projet_pfa_23_24.ml +++ b/test/test_projet_pfa_23_24.ml @@ -5,7 +5,7 @@ let tests_typeof = (* TODO: add more tests *) 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 =