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

clarify(?) the documentation of ['a on_sol]

Browse Source
This commit is contained in:
Gabriel Scherer 2024-01-07 22:37:37 +01:00
parent 3cf46e36c2
commit 97e3c01eaa
1 changed files with 10 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
src/Constraint.ml
View File

@ -57,11 +57,16 @@ module Make (T : Utils.Functor) = struct
| Do : ('a, 'e) t T.t -> ('a, 'e) t | Do : ('a, 'e) t T.t -> ('a, 'e) t
and 'a on_sol = (variable -> STLC.ty) -> 'a and 'a on_sol = (variable -> STLC.ty) -> 'a
(** A value of type [('a, 'e) t] represents a part of an (** ['a on_sol] represents an elaborated witness of type ['a] that
inference constraint, but the value of type ['a] that depends on the solution to the whole constraint -- represented
it produces on success may depend on the solution to by a mapping from inference variables to elaborated types,
the whole constraint, not just for this part of the [variable -> STLC.ty].
constraint.
This is used in the success constraint above
[Ret : 'a on_sol -> ('a, 'e) t];
using just [Ret : 'a -> ('a, 'e) t] would not work, as the
witness we want to produce may depend on the solution to the
whole constraint.
For example, consider the untyped term For example, consider the untyped term
[(lambda y. 42) 0] [(lambda y. 42) 0]
@ -75,10 +80,6 @@ module Make (T : Utils.Functor) = struct
handle the application of [0]. We have to solve the handle the application of [0]. We have to solve the
whole constraint, and then come back to elaborate an whole constraint, and then come back to elaborate an
explictly-typed term [lambda (y : int). 42]. explictly-typed term [lambda (y : int). 42].
The solution to the whole constraint is represented by
a mapping from inference variables to elaborated
types.
*) *)
let (let+) c f = Map(c, f) let (let+) c f = Map(c, f)