From 77fbfce58c12ad5587b9cf522875c8b9cc4c1fe5 Mon Sep 17 00:00:00 2001 From: Fadi Shawki Date: Wed, 10 Jan 2024 14:19:59 +0100 Subject: [PATCH] 2024/02/10 - More naive translations --- src/@orbitmines/external/chyp/Chyp.ts | 184 +++++++++++++++++++++++++- 1 file changed, 179 insertions(+), 5 deletions(-) diff --git a/src/@orbitmines/external/chyp/Chyp.ts b/src/@orbitmines/external/chyp/Chyp.ts index a516426..fc85408 100644 --- a/src/@orbitmines/external/chyp/Chyp.ts +++ b/src/@orbitmines/external/chyp/Chyp.ts @@ -754,6 +754,46 @@ export class Graph extends Ray { this.vdata.highlight = false; this.edata.highlight = false; } + + /** + * Return matches of domain into codomain. + */ + match = (other: Graph, convex: boolean = true): Matches => new Matches(this, other, convex); + + /** + * Return an isomorphism between graphs g and h if found, otherwise `None`. + * + * If found, the isomorphism is returned as a :py:class:`Matches` instance, whose vertex and edge maps are bijections. + */ + find_iso = (other: Graph): Match => { // TODO | NONE + + // TODO: Again, more equivalence checks + // First, check the domains and codomains are equal between the two graphs. + if (this.domain !== other.domain || this.codomain !== other.codomain) + return None; //TODO + + // Try to find an initial match mapping one of the boundary vertices of the domain graph to the corresponding boundary vertex (the vertex in the same input/output location) of the codomain graph. If no initial match is found, return `None`. + const initial_match = new Match(this, other); + + const ___temp = (func: (ray: Graph) => Ray) => { + ([func(this), func(other)] as Ray).zip(([initial, terminal]) => { + if (!initial_match.try_add_vertex(initial, terminal)) + return None; //TODO, DOESNT ACTUALLY RETURN THE FUNCTION HERE. Wait till matcher is abstracted to fix this + }); + } + + ___temp(ray => ray.inputs); + ___temp(ray => ray.outputs); // TODO: See again, the same pattern over and over again, same on both sides. + + // If an initial match is found, try to find a total and surjective match of the domain graph into the codomain graph. + + return new Matches(this, other, initial_match, false) + .filter(match => match.is_surjective()); // TODO; With this filter it should allow you to keep looking + + // TODO::: Automatic?? + // If a total surjective match is not found, return `None`. + return None; + } } export class Chyp extends Ray { @@ -937,6 +977,13 @@ export class Chyp extends Ray { */ } + + /** + * Some more delegations here + */ + match_graph = (domain: Graph, codomain: Graph, convex: boolean = true): Matches => domain.match(codomain, convex); + match_rule = (rule: Rule, codomain: Graph, convex: boolean = true): Matches => rule.match(codomain, convex); + find_iso = (domain: Graph, codomain: Graph): Match => domain.find_iso(codomain); } export class CodeView extends Ray { @@ -1160,14 +1207,134 @@ export class Match extends Ray { return bool(True); } - try_add_edge = (domain_edge = int, codomain_edge = int): Ray => { throw new NotImplementedError(); } + /** + * Try to map `domain_edge` to `codomain_edge`. + * + * This must satisfy certain conditions, such as being injective and having consistency with the vertex map. + * + * @param domain_edge + * @param codomain_edge + * + * `True` if a consistent match is found mapping `domain_edge` to `codomain_edge`, otherwise `False`. + */ + try_add_edge = (initial: EData, terminal: EData): Ray => { + log(`Trying to add edge ${initial} -> ${terminal} to match:`); + log(this.toString()); + + // TODO: Again an equivalence + // Check the values of the domain and codomain edges match. + if (initial.value !== terminal.value) { + log(`Edge failed: values ${initial.value} != ${terminal.value}`) + return false; + } + + // The edge map must be injective. + if (this.edge_image.includes(terminal)) { + console.log('Edge failed: the map would become non-injective.'); + return false; + } + + // If the values match and the codomain edge has not already been mapped to, map domain edge to codomain edge. + this.edge_map[initial] = terminal; + this.edge_image.add(terminal); + + // Domain sources must match codomain sources and domain targets must match codomain targets. + + // TODO: Again more equivalences, just to log - debug mode + { + // initial = preimg + // terminal = image + + // Domain sources must match codomain sources and domain targets must match codomain targets. + if (initial.domain !== terminal.domain) { + log(`Edge domain ${initial.domain} does not match image domain ${terminal.domain}.`); + } + + // TODO, again both sides + if (initial.codomain !== terminal.codomain) { + log(`Edge codomain ${initial.codomain} does not match image codomain ${terminal.codomain}.`); + } + } + + // TODO: This too probably general pattern to extract + // Check a vertex map consistent with this edge pairing exists. + // TODO: + here is just concat, so that zip can easily match it + ([initial.source + initial.target, terminal.source + terminal.target] as Ray).zip(([initial_vertex, terminal_vertex]) => { + // Each vertex that is already mapped needs to be consistent. + // TODO: More equivlaency, could be on the vertecies themselves + if (this.vertex_map.includes(initial_vertex) && this.vertex_image[initial_vertex] !== terminal_vertex) { + log('Edge failed: inconsistent with previously mapped vertex.'); + return false; // TODO: NOT RETURNING AGAIN + } + + // Otherwise, a consistent match must be found vertex for unmapped source and target vertices. + + if (!this.try_add_vertex(initial_vertex, terminal_vertex)) { + log('Edge failed: couldn\'t add a source or target vertex.'); + return false; + } + }); + + log('Edge success.'); + return true; + } + + domain_neighbourhood_mapped = (vertex = int): Ray => { throw new NotImplementedError(); } map_scalars = (): Ray => { throw new NotImplementedError(); } more = (): Ray => { throw new NotImplementedError(); } - is_total = (): Ray => { throw new NotImplementedError(); } - is_surjective = (): Ray => { throw new NotImplementedError(); } - is_injective = (): Ray => { throw new NotImplementedError(); } - is_convex = (): Ray => { throw new NotImplementedError(); } + + + // TODO: Total=surjective on another level of description ??? + ___defuq = (string: 'image' | 'map', domain) => + this[`vertex_${string}`].count === domain.vertices.count + && this[`edge_${string}`].count === domain.edges.count; // TODO: Again vertex/edge pattern, just collapse to one check + + /** + * Return whether all domain vertices and edges have been mapped. + */ + is_total = (): Ray => this.___defuq('map', this.domain); + /** + * Return whether the vertex and edge maps are surjective. + */ + is_surjective = (): Ray => this.___defuq('image', this.codomain); + + /** + * Return whether the vertex and edge maps are injective. + */ + is_injective = (): Ray => { + // Since the edge map is always injective, we only need to check the vertex map is injective. TODO (GENERALIZE) + return this.vertex_map.count === this.vertex_image.count; + } + + /** + * Return whether this match is convex. + * + * A match is convex if: + * - It is injective. + * - Its image in the codomain hypergraph is a convex sub-hypergraph. This means that for any two nodes in the sub-hypergraph and any path between these two nodes, every hyperedge along the path is also in the sub-hypergraph. + * + * TODO: Just no overlap?? + */ + is_convex = (): Ray => { + if (!this.is_injective()) { //TODO: WHY? + return false; + } + + + // Check that the image sub-hypergraph is convex. Get all successors of vertices in the image of the output of the domain graph. + const output_image_successors = this.codomain.successors( + this.domain.outputs + .filter(vertex => this.vertex_map[vertex]) // TODO INCLUDES + ); // TODO, Why search in codomain fromi these, ?? this must be easier + + // Check there is no path from any vertices in the image of the domain outputs to a vertex in the image of the domain inputs. + this.domain.inputs + .filter(vertex => this.vertex_map.includes(vertex) && output_image_successors.includes(this.vertex_map[vertex])) + .any(() => { return false }) // TODO DOESNT ACTUALLY RETURNM + + return true; + } /** * TODO Not implemented;; @@ -1346,6 +1513,13 @@ export class Rule extends Ray { const result: Match = this.dpo(match).first().cast(); return result.codomain; } + + // TODO: Can probably just match Rule=Graph, and use only one of these methods?? + /** + * Return matches of the left side of `rule` into `graph`. + */ + match = (other: Graph, convex: boolean = true): Matches => new Matches(this.lhs, other, convex); + } export class RewriteState extends Ray {