Paris7/unification-pfa
Archived
1
0
Fork 0
Code Issues Activity

all done

Browse source
This commit is contained in:
Mylloon 2024-04-30 13:56:02 +02:00
parent fe03ff0351
commit 1f203b5138
Signed by: Anri
GPG key ID: A82D63DFF8D1317F
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
README.md
View file

@ -33,14 +33,14 @@ To realise this project you will have to implement the following modules:
1. [typeSubstitution](./lib/typeSubstituion.ml) 1. [typeSubstitution](./lib/typeSubstituion.ml)
You must implement at least: You must implement at least:
- [ ] `type t`, i.e. how to represent syntactic substitutions in memory, - [x] `type t`, i.e. how to represent syntactic substitutions in memory,
- [ ] `val apply`, which applies a syntactic substitution to a type - [x] `val apply`, which applies a syntactic substitution to a type
- [ ] `val compose`, which computes the substitution obtained composing two given substitutions. - [x] `val compose`, which computes the substitution obtained composing two given substitutions.
1. [unification](./lib/unification.ml) 1. [unification](./lib/unification.ml)
You must implement at least: You must implement at least:
- [ ] `val unify` which given two type `t1` and `t2`, - [x] `val unify` which given two type `t1` and `t2`,
must compute the substitution `s` such that if must compute the substitution `s` such that if
`unify t1 t2 = Some s` then `apply s t1 = apply s t2`. `unify t1 t2 = Some s` then `apply s t1 = apply s t2`.
@ -49,7 +49,7 @@ To realise this project you will have to implement the following modules:
1. [inference](./lib/inference.ml) 1. [inference](./lib/inference.ml)
You must implement at least: You must implement at least:
- [ ] `val typeof`, which given a term `t` must compute either - [x] `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`. `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 add more definitions to each of these modules, and extend their signatures accordingly.