project-inception
This commit is contained in:
commit
c414bf8564
13 changed files with 287 additions and 0 deletions
176
README.md
Normal file
176
README.md
Normal file
|
@ -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
|
||||||
|
```
|
4
bin/dune
Normal file
4
bin/dune
Normal file
|
@ -0,0 +1,4 @@
|
||||||
|
(executable
|
||||||
|
(public_name projet_pfa_23_24)
|
||||||
|
(name main)
|
||||||
|
(libraries typeInference))
|
1
bin/main.ml
Normal file
1
bin/main.ml
Normal file
|
@ -0,0 +1 @@
|
||||||
|
let () = print_endline "Hello, World!"
|
26
dune-project
Normal file
26
dune-project
Normal file
|
@ -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
|
3
lib/dune
Normal file
3
lib/dune
Normal file
|
@ -0,0 +1,3 @@
|
||||||
|
(library
|
||||||
|
(name typeInference)
|
||||||
|
(preprocess (pps ppx_deriving.show ppx_deriving.ord ppx_deriving.eq)))
|
4
lib/identifier.mli
Normal file
4
lib/identifier.mli
Normal file
|
@ -0,0 +1,4 @@
|
||||||
|
type t (* = ... -> Students, this is your job ! *)
|
||||||
|
[@@deriving eq, ord, show]
|
||||||
|
|
||||||
|
val fresh : unit -> t
|
7
lib/inference.mli
Normal file
7
lib/inference.mli
Normal file
|
@ -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
|
||||||
|
|
22
lib/term.mli
Normal file
22
lib/term.mli
Normal file
|
@ -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]
|
6
lib/type.mli
Normal file
6
lib/type.mli
Normal file
|
@ -0,0 +1,6 @@
|
||||||
|
type t =
|
||||||
|
| Var of Identifier.t
|
||||||
|
| Int
|
||||||
|
| Product of t * t
|
||||||
|
| Arrow of t * t
|
||||||
|
[@@deriving eq, ord, show]
|
6
lib/typeSubstitution.mli
Normal file
6
lib/typeSubstitution.mli
Normal file
|
@ -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
|
10
lib/unification.mli
Normal file
10
lib/unification.mli
Normal file
|
@ -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
|
3
test/dune
Normal file
3
test/dune
Normal file
|
@ -0,0 +1,3 @@
|
||||||
|
(test
|
||||||
|
(name test_projet_pfa_23_24)
|
||||||
|
(libraries typeInference alcotest))
|
19
test/test_projet_pfa_23_24.ml
Normal file
19
test/test_projet_pfa_23_24.ml
Normal file
|
@ -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 ;
|
||||||
|
]
|
Reference in a new issue