https://github.com/EasyCrypt/easycrypt
Tip revision: 846710a2a656834065e745d19416ebdc83158f55 authored by Benjamin Gregoire on 14 July 2019, 06:50:07 UTC
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Tip revision: 846710a
ecTypeClass.ml
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcUtils
open EcPath
(* -------------------------------------------------------------------- *)
type graph = {
tcg_nodes : Sp.t Mp.t;
tcg_closure : Sp.t Mp.t;
}
type nodes = {
tcn_graph : graph;
tcn_nodes : Sp.t;
}
type node = EcPath.path
exception CycleDetected
(* -------------------------------------------------------------------- *)
module Graph = struct
let empty : graph = {
tcg_nodes = Mp.empty;
tcg_closure = Mp.empty;
}
let dump gr =
Printf.sprintf "%s\n"
(String.concat "\n"
(List.map
(fun (p, ps) -> Printf.sprintf "%s -> %s"
(EcPath.tostring p)
(String.concat ", " (List.map EcPath.tostring (Sp.elements ps))))
(Mp.bindings gr.tcg_nodes)))
let has_path ~src ~dst g =
if EcPath.p_equal src dst then
true
else
match Mp.find_opt src g.tcg_closure with
| None -> false
| Some m -> Mp.mem dst m
let add ~src ~dst g =
if has_path dst src g then
raise CycleDetected;
match Mp.find_opt src g.tcg_nodes with
| Some m when Mp.mem dst m -> g
| _ ->
let up_node m = Sp.add dst (odfl Sp.empty m)
and up_clos m =
Sp.union
(odfl Sp.empty (Mp.find_opt dst g.tcg_closure))
(Sp.add dst (odfl Sp.empty m))
in
{ g with
tcg_nodes = Mp.change (some -| up_node) src g.tcg_nodes;
tcg_closure = Mp.change (some -| up_clos) src g.tcg_closure; }
end
(* -------------------------------------------------------------------- *)
module Nodes = struct
let empty g = {
tcn_graph = g;
tcn_nodes = Sp.empty;
}
let add n nodes =
let module E = struct exception Discard end in
try
let aout =
Sp.filter
(fun p ->
if Graph.has_path p n nodes.tcn_graph then raise E.Discard;
not (Graph.has_path n p nodes.tcn_graph))
nodes.tcn_nodes
in
{ nodes with tcn_nodes = Sp.add n aout }
with E.Discard -> nodes
let toset nodes = nodes.tcn_nodes
let reduce set g =
toset (Sp.fold add set (empty g))
end