Equations environment using a Hashtbl

This commit is contained in:
Olivier 2023-02-10 17:14:17 +01:00
parent 3e3fb4cc05
commit fa34543f1d
1 changed files with 271 additions and 0 deletions

View File

@ -312,6 +312,277 @@ end (* Env *)
(* -------------------------------------------------------------------------- *)
module StructTable = Hashtbl
module EqEnv : sig
type scope =
int
type vertex =
structure
and structure =
S of vertex ABS.structure
val add: vertex -> unit
exception InconsistentContext
val add_equality: scope -> vertex -> vertex -> unit
val eq: vertex -> vertex -> scope option
end = struct
(* TODO : remove useless assert statements ? *)
type scope =
int
let base_scope =
0
(* We store an undirected graph representing equalities between structures.
A vertex is either :
- disconnected from other vertices and points to None
- connected to at least one other vertex (and cannot point to None)
An edge between two vertices means that they are equal. *)
type vertex =
structure
and structure =
S of vertex ABS.structure
(* For each equality, we store a scope, that corresponds to the scope
where the equality is well-defined. We represent our graph with a
hash-table mapping vertices to pairs of vertex and scope.
For every mapping (v1 -> (v2,scope)) we store a mapping
(v2 -> (v1,scope)) as well, so as to provide an undirected graph. *)
let table : (vertex, (vertex * scope) option) StructTable.t =
StructTable.create 64
(* ------------------------------------------------------------------------ *)
(* Searching through the graph. *)
let get_neighbours v =
assert (StructTable.mem table v);
let vs = StructTable.find_all table v in
match vs with
(* [v] is either disconnected, and its only neighbour is None ... *)
| [None] ->
[]
(* ... or it is connected with a list of (Some _) neighbours *)
| _ ->
List.map Option.get vs
(* TODO : use a mark to keep trace of already visited vertices like in
[Generalization.ml] ? *)
let rec search
(v:vertex) (visited:vertex list) (stop:vertex -> bool)
: vertex option =
if stop v then
Some v
else
let neighbours = List.map fst (get_neighbours v) in
let unvisited_neighbours =
List.filter (fun v -> not (List.mem v visited)) neighbours
in
List.fold_left (fun res v ->
match res with
| None ->
search v (v::visited) stop
| Some _ ->
res
) None unvisited_neighbours
let search v stop =
search v [] stop
let get_structure v : vertex option =
assert (StructTable.mem table v);
let stop v =
match v with
| S (ABS.User _) ->
true
| S (ABS.Abstract _) ->
false
in
search v stop
let path_exists v1 v2 =
assert (StructTable.mem table v1);
assert (StructTable.mem table v2);
let stop =
( = ) v2
in
match search v1 stop with
| None ->
false
| Some _ ->
true
(* ------------------------------------------------------------------------ *)
(* Add vertices and edges. *)
let add v =
if not (StructTable.mem table v) then
StructTable.add table v None
(* [add_directed_edge v1 v2 scope] adds an edge between [v1] and [v2] with
[scope]. If [v1] pointed to None, then remove this binding beforehand. *)
let add_directed_edge scope v1 v2 =
if StructTable.find table v1 = None then
StructTable.remove table v1;
StructTable.add table v1 (Some (v2,scope))
(* Add a binding in both ways. *)
let add_edge scope v1 v2 =
assert (StructTable.mem table v1);
assert (StructTable.mem table v2);
add_directed_edge scope v1 v2;
add_directed_edge scope v2 v1
(* ------------------------------------------------------------------------ *)
(* Unification. *)
(* There can be more than one way to prove an equality, depending on the
equations in the context. Consider for example the introduction of the
following equations (in this specific order) :
(1) a = b
(2) a = int
(3) b = int
We can prove the equality (a = int) by using equation (2) or by using both
(1) and (3). It is always a good choice to pick the lowest scope, that is
use the most early introduced equations. So there is no need to add
redundant equations in the context. In the above example, equation (3)
will not be added because it can be deduced from (1) and (2). In order to
detect redundant equations, we search through the graph of already added
equations before adding new ones. *)
(* TODO : Comment ! Copy the comments in [FTypechecker.ml] ? *)
type mode = Input | Check
exception Clash
(* Unify two vertices, with at least one that is an abstract. *)
let unify_abstract mode scope v1 v2 =
match mode with
| Input ->
add_edge scope v1 v2
| Check ->
raise Clash
exception InconsistentContext
(* The context can become inconsistent if we try to unify two different
structures, otherwise we just add a new edge between the two vertices
we try to unify (and between their leaves if necessary). *)
let rec unify mode scope (v1:vertex) (v2:vertex) =
if not (path_exists v1 v2) then
match v1, v2 with
(* Two rigid variables. *)
| S ABS.Abstract _, S ABS.Abstract _ ->
(* Simply add an edge between them *)
unify_abstract mode scope v1 v2
(* One rigid and one structure.*)
| (S ABS.Abstract _ as r), v
| v, (S ABS.Abstract _ as r) ->
(* Try to find a structure equal to the rigid *)
begin match get_structure r with
(* If the rigid [r] is not bound to a structure, then [v] is the new
structure for [r] (we add an edge between them) *)
| None ->
unify_abstract mode scope v1 v2
(* Otherwise, try to unify the two structures *)
| Some v' ->
unify mode scope v v'
end
(* Two structures. *)
| S (ABS.User s1), S (ABS.User s2) ->
(* Try to unify the leaves ...*)
try
ignore (ABS.S.conjunction (unify mode scope) s1 s2)
(* ... if it fails, we have an inconsistent context. *)
with S.InconsistentConjunction ->
match mode with
| Input ->
raise InconsistentContext
| Check ->
raise Clash
(* Adding an equality amounts to unify two vertices of the graph. *)
let add_equality scope v1 v2 : unit =
unify Input scope v1 v2
(* ------------------------------------------------------------------------ *)
(* Equality test. *)
(* We added edges to represent equalities only when necessary. So we have the
property that there is at most one path between two vertices. Hence
we know that the biggest scope encountered along the path between two
vertices is the lowest scope where the equality is well-defined. *)
let dummy_scope =
base_scope
(* [eq_aux vs current_max v2] make a depth-first search through the graph
to see if there exists a vertex in [vs] connected to [v2]. We maintain
a worklist [vs] of vertices to left to visit associated with the maximum
scope encountered along the way. If a path exists we return this scope
value, otherwise we return None. *)
let rec eq_aux (vs : (vertex * scope) list) (v2 : vertex) : scope option =
match vs with
(* We exhausted all paths. *)
| [] ->
None
(* Take the head of our work list ... *)
| (v1,scope)::vs ->
(* ... and try to unify it with the "destination" vertex. *)
try
unify Check dummy_scope v1 v2;
Some scope
(* If it failed to unify, ... *)
with Clash ->
(* ... compute all the neighbours, ... *)
let neighbours =
get_neighbours v1
in
(* ... associate the new maximum scope to them ... *)
let neighbours_scope_max =
List.map (fun (v,scope') -> (v,max scope scope')) neighbours
in
(* ... and call ourselves recursively with the unvisited vertices *)
eq_aux (neighbours_scope_max @ vs) v2
let eq v1 v2 : scope option =
assert (StructTable.mem table v1);
assert (StructTable.mem table v2);
eq_aux [(v1,base_scope)] v2
end (* EqEnv *)
let _ =
ignore (EqEnv.(add, add_equality, eq))
(* -------------------------------------------------------------------------- *)
(* The solver maintains a mutable mapping of immutable type variables to
unifier variables. *)