Mysaa/mpri-2.4-project-2023-2024
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Infer.has_type: include a full example of a constraint that works for (lambda x. x)

Browse Source 
Suggested-by: Dai Weituo
This commit is contained in:
Gabriel Scherer 2024-02-08 15:47:35 +01:00
parent c0ad56a745
commit 44d184b6d4
1 changed files with 13 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
src/Infer.ml
View File

@ -64,6 +64,19 @@ module Make(T : Utils.Functor) = struct
For example, if [t] is the term [lambda x. x], then [has_type env t w] For example, if [t] is the term [lambda x. x], then [has_type env t w]
generates a constraint equivalent to [∃?v. ?w = (?v -> ?v)]. generates a constraint equivalent to [∃?v. ?w = (?v -> ?v)].
More precisely, one possible generated constraint would be:
{[
Exist(v, None,
Map(
Conj(
Exist (arr, Some (Arrow (v, v)), Eq (arr, w)),
MapErr(Decode v, fun e -> Cycle e)
),
fun ((), ty) -> Abs (x, ty, Var x)
))
]}
but the actually generated constraint may be more complex/verbose.
Precondition: when calling [has_type env t], [env] must map each Precondition: when calling [has_type env t], [env] must map each
term variable that is free in [t] to an inference variable. term variable that is free in [t] to an inference variable.
*) *)