make_suitable_for_environment: Expand unavailable variables occurring only once#492
Conversation
chambart
left a comment
There was a problem hiding this comment.
This is OK. There are some tedious parts. I don't know how much it could be improved
| | One -> | ||
| ( unavailable_vars_renamed, | ||
| var :: unavailable_vars_expanded, | ||
| unavailable_vars_removed ) |
There was a problem hiding this comment.
Maybe declare a record and use { unavailable_var with ... }
Maybe only
| match to_erase with | ||
| | Everything_not_in suitable_for -> | ||
| not (TE.mem suitable_for (Name.var var)) | ||
| | All_variables_except to_keep -> not (Variable.Set.mem var to_keep) |
There was a problem hiding this comment.
That's a lot of negations. I'm not sure that it can be a lot better though
| else unavailable_vars) | ||
| let ( unavailable_vars_renamed, | ||
| unavailable_vars_expanded, | ||
| unavailable_vars_removed ) = |
There was a problem hiding this comment.
Maybe 'to_be_renamed' 'to_be_removed'...
| 'head t -> | ||
| Name_occurrences.t | ||
|
|
||
| val free_names_no_cache : |
There was a problem hiding this comment.
Maybe a name that tells the use case would be better.
There was a problem hiding this comment.
What would you suggest ? free_names_restricted would work too, but I feel like it's less precise.
| ~var:(fun var ~coercion -> | ||
| if Variable.Set.mem var to_expand | ||
| then TG.apply_coercion (expand var) coercion | ||
| else ty) |
There was a problem hiding this comment.
This seems very similar to Descr.project_variables_out would it be sensible to share it in some way ?
|
|
||
| let rec project_variables_out ~to_project ~expand t = | ||
| match t with | ||
| | Value ty -> |
There was a problem hiding this comment.
There must be something nicer that we could do. But sadly I couldn't find some simple refactoring for that...
| then TG.apply_coercion (expand var) coercion | ||
| else ty) | ||
| in | ||
| TG.project_variables_out ~to_project ~expand ty |
There was a problem hiding this comment.
This looks like tying the knot of the recursion from outside TG.project_variables_out. Would it be nicer to do the recursion in TG.project_variables_out instead ?
There was a problem hiding this comment.
The key pain point is that it's not possible to refer to a typing environment inside Type_grammar.ml. It might be possible to only pass a find_type function instead of the expand function though.
| | String _ -> head | ||
| | Array { element_kind; length } -> | ||
| let length' = project_variables_out ~to_project ~expand length in | ||
| if length == length' then head else Array { element_kind; length = length' } |
There was a problem hiding this comment.
All those sharings would be quite easy to break. Some test would be nice for that (but reaaaally tedious...)
| t -> used_closure_vars:Var_within_closure.Set.t -> t | ||
|
|
||
| val project_variables_out : | ||
| to_project:Variable.Set.t -> expand:(Variable.t -> t) -> t -> t |
There was a problem hiding this comment.
Wouldn't project_variable be ok as a name ? why _out ?
There was a problem hiding this comment.
The out underlines the idea that the variables have to disappear afterwards.
| then other_tags | ||
| else Ok { index; env_extension = env_extension'; maps_to = maps_to' } | ||
| in | ||
| if known_tags == known_tags' && other_tags == other_tags' |
There was a problem hiding this comment.
I realise that this kind of code is quite fragile and hard to properly review. It would be easy to forget to check a case.
It might be possible to define a nice 'did not modify' monad with some let operator to make this kind of code more automatic. Maybe
There was a problem hiding this comment.
It could look like this maybe
module Share : sig
type 'a map = ('a -> 'a) * 'a
type 'a ret
val bind : 'a map -> ('a -> 'b ret) -> 'b ret
val (let*) : 'a map -> ('a -> 'b ret) -> 'b ret
val return : 'a -> 'a ret
val select : 'a -> 'a ret -> 'a
end = struct
type 'a map = ('a -> 'a) * 'a
type 'a ret = 'a * bool
let bind (type t) ((f : t -> t), (v : t)) r =
let v' = f v in
let b, eq = r v' in
b, eq && v' == v
let (let*) = bind
let return v = v, true
let select a (a', c) =
if c then a else a'
end
let fa x = x+1
let fb x = not x
let f ((a, b, c) as orig) =
let open Share in
select orig @@
let* a = fa, a in
let* b = fb, b in
return (a, b, c)9338f34 to
1a0cc14
Compare
|
The above conversations are to remain for later. |
This PR is aimed at reducing the number of variables that get quantified existentially when making a type suitable for another environment.
This works by finding the variables that only occur once (transitively) in the input types, and replacing them by a valid expansion (if they're canonical, their head expansion, otherwise either a valid alias or the expansion of it).
Since this has to explore types in depth, it requires a new set of functions, that I've called
project_*because they correspond to the concept projection on a lower-dimensional plane in the context of multi-dimensional environments.