From 134ef566bee653d90b5126bf31152953a7b58214 Mon Sep 17 00:00:00 2001
From: Ivan <8611739+IRBorisov@users.noreply.github.com>
Date: Mon, 26 Aug 2024 17:25:07 +0300
Subject: [PATCH] F: Implement basic substitution checks

---
 .vscode/settings.json                         |   1 +
 .../DlgEditOperation/DlgEditOperation.tsx     |  35 +++-
 .../dialogs/DlgEditOperation/TabSynthesis.tsx |  18 +-
 .../frontend/src/hooks/useRSFormCache.ts      |   3 +
 rsconcept/frontend/src/models/Graph.test.ts   |  36 ++++
 rsconcept/frontend/src/models/Graph.ts        |  56 ++++++
 rsconcept/frontend/src/models/oss.ts          |  19 ++
 rsconcept/frontend/src/models/ossAPI.ts       | 170 +++++++++++++++++-
 rsconcept/frontend/src/models/rslang.ts       |   3 +
 rsconcept/frontend/src/utils/labels.ts        |  23 ++-
 10 files changed, 351 insertions(+), 13 deletions(-)

diff --git a/.vscode/settings.json b/.vscode/settings.json
index 05a9be93..49098169 100644
--- a/.vscode/settings.json
+++ b/.vscode/settings.json
@@ -155,6 +155,7 @@
     "toastify",
     "tooltipic",
     "tsdoc",
+    "Typifications",
     "unknwn",
     "Upvote",
     "Viewset",
diff --git a/rsconcept/frontend/src/dialogs/DlgEditOperation/DlgEditOperation.tsx b/rsconcept/frontend/src/dialogs/DlgEditOperation/DlgEditOperation.tsx
index 81967b3a..093e0f2b 100644
--- a/rsconcept/frontend/src/dialogs/DlgEditOperation/DlgEditOperation.tsx
+++ b/rsconcept/frontend/src/dialogs/DlgEditOperation/DlgEditOperation.tsx
@@ -1,7 +1,7 @@
 'use client';
 
 import clsx from 'clsx';
-import { useEffect, useMemo, useState } from 'react';
+import { useCallback, useEffect, useMemo, useState } from 'react';
 import { TabList, TabPanel, Tabs } from 'react-tabs';
 
 import BadgeHelp from '@/components/info/BadgeHelp';
@@ -18,6 +18,7 @@ import {
   OperationID,
   OperationType
 } from '@/models/oss';
+import { SubstitutionValidator } from '@/models/ossAPI';
 import { PARAMETER } from '@/utils/constants';
 
 import TabArguments from './TabArguments';
@@ -44,6 +45,9 @@ function DlgEditOperation({ hideWindow, oss, target, onSubmit }: DlgEditOperatio
   const [title, setTitle] = useState(target.title);
   const [comment, setComment] = useState(target.comment);
 
+  const [isCorrect, setIsCorrect] = useState(true);
+  const [validationText, setValidationText] = useState('');
+
   const [inputs, setInputs] = useState<OperationID[]>(oss.graph.expandInputs([target.id]));
   const inputOperations = useMemo(() => inputs.map(id => oss.operationByID.get(id)!), [inputs, oss.operationByID]);
   const schemasIDs = useMemo(
@@ -54,10 +58,10 @@ function DlgEditOperation({ hideWindow, oss, target, onSubmit }: DlgEditOperatio
   const cache = useRSFormCache();
   const schemas = useMemo(
     () => schemasIDs.map(id => cache.getSchema(id)).filter(item => item !== undefined),
-    [schemasIDs, cache]
+    [schemasIDs, cache.getSchema]
   );
 
-  const isValid = useMemo(() => alias !== '', [alias]);
+  const canSubmit = useMemo(() => alias !== '', [alias]);
 
   useEffect(() => {
     cache.preload(schemasIDs);
@@ -82,7 +86,16 @@ function DlgEditOperation({ hideWindow, oss, target, onSubmit }: DlgEditOperatio
     );
   }, [schemasIDs, schemas, cache.loading]);
 
-  const handleSubmit = () => {
+  useEffect(() => {
+    if (cache.loading || schemas.length !== schemasIDs.length) {
+      return;
+    }
+    const validator = new SubstitutionValidator(schemas, substitutions);
+    setIsCorrect(validator.validate());
+    setValidationText(validator.msg);
+  }, [substitutions, cache.loading, schemas, schemasIDs.length]);
+
+  const handleSubmit = useCallback(() => {
     const data: IOperationUpdateData = {
       target: target.id,
       item_data: {
@@ -95,7 +108,7 @@ function DlgEditOperation({ hideWindow, oss, target, onSubmit }: DlgEditOperatio
       substitutions: target.operation_type !== OperationType.SYNTHESIS ? undefined : substitutions
     };
     onSubmit(data);
-  };
+  }, [alias, comment, title, inputs, substitutions, target, onSubmit]);
 
   const cardPanel = useMemo(
     () => (
@@ -134,12 +147,14 @@ function DlgEditOperation({ hideWindow, oss, target, onSubmit }: DlgEditOperatio
           schemas={schemas}
           loading={cache.loading}
           error={cache.error}
+          validationText={validationText}
+          isCorrect={isCorrect}
           substitutions={substitutions}
           setSubstitutions={setSubstitutions}
         />
       </TabPanel>
     ),
-    [cache.loading, cache.error, substitutions, schemas]
+    [cache.loading, cache.error, substitutions, schemas, validationText, isCorrect]
   );
 
   return (
@@ -147,7 +162,7 @@ function DlgEditOperation({ hideWindow, oss, target, onSubmit }: DlgEditOperatio
       header='Редактирование операции'
       submitText='Сохранить'
       hideWindow={hideWindow}
-      canSubmit={isValid}
+      canSubmit={canSubmit}
       onSubmit={handleSubmit}
       className='w-[40rem] px-6 min-h-[35rem]'
     >
@@ -167,7 +182,11 @@ function DlgEditOperation({ hideWindow, oss, target, onSubmit }: DlgEditOperatio
             <TabLabel title='Выбор аргументов операции' label='Аргументы' className='w-[8rem]' />
           ) : null}
           {target.operation_type === OperationType.SYNTHESIS ? (
-            <TabLabel title='Таблица отождествлений' label='Отождествления' className='w-[8rem]' />
+            <TabLabel
+              titleHtml={'Таблица отождествлений' + (isCorrect ? '' : '<br/>(не прошла проверку)')}
+              label={isCorrect ? 'Отождествления' : 'Отождествления*'}
+              className='w-[8rem]'
+            />
           ) : null}
         </TabList>
 
diff --git a/rsconcept/frontend/src/dialogs/DlgEditOperation/TabSynthesis.tsx b/rsconcept/frontend/src/dialogs/DlgEditOperation/TabSynthesis.tsx
index 3e1d08f0..5ee90712 100644
--- a/rsconcept/frontend/src/dialogs/DlgEditOperation/TabSynthesis.tsx
+++ b/rsconcept/frontend/src/dialogs/DlgEditOperation/TabSynthesis.tsx
@@ -1,6 +1,8 @@
 import { ErrorData } from '@/components/info/InfoError';
 import PickSubstitutions from '@/components/select/PickSubstitutions';
+import TextArea from '@/components/ui/TextArea';
 import DataLoader from '@/components/wrap/DataLoader';
+import { useConceptOptions } from '@/context/ConceptOptionsContext';
 import { ICstSubstitute } from '@/models/oss';
 import { IRSForm } from '@/models/rsform';
 import { prefixes } from '@/utils/constants';
@@ -8,22 +10,34 @@ import { prefixes } from '@/utils/constants';
 interface TabSynthesisProps {
   loading: boolean;
   error: ErrorData;
+  validationText: string;
+  isCorrect: boolean;
 
   schemas: IRSForm[];
   substitutions: ICstSubstitute[];
   setSubstitutions: React.Dispatch<React.SetStateAction<ICstSubstitute[]>>;
 }
 
-function TabSynthesis({ schemas, loading, error, substitutions, setSubstitutions }: TabSynthesisProps) {
+function TabSynthesis({
+  schemas,
+  loading,
+  error,
+  validationText,
+  isCorrect,
+  substitutions,
+  setSubstitutions
+}: TabSynthesisProps) {
+  const { colors } = useConceptOptions();
   return (
     <DataLoader id='dlg-synthesis-tab' className='cc-column mt-3' isLoading={loading} error={error}>
       <PickSubstitutions
         schemas={schemas}
         prefixID={prefixes.dlg_cst_substitutes_list}
-        rows={8}
+        rows={10}
         substitutions={substitutions}
         setSubstitutions={setSubstitutions}
       />
+      <TextArea disabled value={validationText} style={{ borderColor: isCorrect ? undefined : colors.fgRed }} />
     </DataLoader>
   );
 }
diff --git a/rsconcept/frontend/src/hooks/useRSFormCache.ts b/rsconcept/frontend/src/hooks/useRSFormCache.ts
index a62f7890..737c9cf9 100644
--- a/rsconcept/frontend/src/hooks/useRSFormCache.ts
+++ b/rsconcept/frontend/src/hooks/useRSFormCache.ts
@@ -54,6 +54,9 @@ function useRSFormCache() {
   );
 
   useEffect(() => {
+    if (pending.length === 0) {
+      return;
+    }
     const ids = pending.filter(id => !processing.includes(id) && !cache.find(schema => schema.id === id));
     setPending([]);
     if (ids.length === 0) {
diff --git a/rsconcept/frontend/src/models/Graph.test.ts b/rsconcept/frontend/src/models/Graph.test.ts
index 1a72834d..be7cd9eb 100644
--- a/rsconcept/frontend/src/models/Graph.test.ts
+++ b/rsconcept/frontend/src/models/Graph.test.ts
@@ -159,4 +159,40 @@ describe('Testing Graph queries', () => {
     expect(graph.maximizePart([3, 2])).toStrictEqual([3, 2, 6, 4]);
     expect(graph.maximizePart([3, 1])).toStrictEqual([3, 1, 7, 5, 6]);
   });
+
+  test('find elementary cycle', () => {
+    const graph = new Graph([
+      [1, 1] //
+    ]);
+    expect(graph.findCycle()).toStrictEqual([1, 1]);
+  });
+
+  test('find cycle acyclic', () => {
+    const graph = new Graph([
+      [1, 2], //
+      [2]
+    ]);
+    expect(graph.findCycle()).toStrictEqual(null);
+  });
+
+  test('find cycle typical', () => {
+    const graph = new Graph([
+      [1, 2], //
+      [1, 4],
+      [2, 3],
+      [3, 1],
+      [3, 4],
+      [4]
+    ]);
+    expect(graph.findCycle()).toStrictEqual([1, 2, 3, 1]);
+  });
+
+  test('find cycle acyclic 2 components', () => {
+    const graph = new Graph([
+      [0, 1], //
+      [2, 3],
+      [3, 0]
+    ]);
+    expect(graph.findCycle()).toStrictEqual(null);
+  });
 });
diff --git a/rsconcept/frontend/src/models/Graph.ts b/rsconcept/frontend/src/models/Graph.ts
index 029cca3b..8d44d090 100644
--- a/rsconcept/frontend/src/models/Graph.ts
+++ b/rsconcept/frontend/src/models/Graph.ts
@@ -293,4 +293,60 @@ export class Graph {
       }
     });
   }
+
+  /**
+   * Finds a cycle in the graph.
+   *
+   * @returns {number[] | null} The cycle if found, otherwise `null`.
+   * Uses non-recursive DFS.
+   */
+  findCycle(): number[] | null {
+    const visited = new Set<number>();
+    const nodeStack = new Set<number>();
+    const parents = new Map<number, number>();
+
+    for (const nodeId of this.nodes.keys()) {
+      if (visited.has(nodeId)) {
+        continue;
+      }
+
+      const callStack: { nodeId: number; parentId: number | null }[] = [];
+      callStack.push({ nodeId: nodeId, parentId: null });
+      while (callStack.length > 0) {
+        const { nodeId, parentId } = callStack[callStack.length - 1];
+        if (visited.has(nodeId)) {
+          nodeStack.delete(nodeId);
+          callStack.pop();
+          continue;
+        }
+        visited.add(nodeId);
+        nodeStack.add(nodeId);
+        if (parentId !== null) {
+          parents.set(nodeId, parentId);
+        }
+
+        const currentNode = this.nodes.get(nodeId)!;
+        for (const child of currentNode.outputs) {
+          if (!visited.has(child)) {
+            callStack.push({ nodeId: child, parentId: nodeId });
+            continue;
+          }
+          if (!nodeStack.has(child)) {
+            continue;
+          }
+          const cycle: number[] = [];
+          let current = nodeId;
+          cycle.push(child);
+          while (current !== child) {
+            cycle.push(current);
+            current = parents.get(current)!;
+          }
+          cycle.push(child);
+          cycle.reverse();
+          return cycle;
+        }
+      }
+    }
+    return null;
+  }
 }
diff --git a/rsconcept/frontend/src/models/oss.ts b/rsconcept/frontend/src/models/oss.ts
index 6410d2f5..0b20368c 100644
--- a/rsconcept/frontend/src/models/oss.ts
+++ b/rsconcept/frontend/src/models/oss.ts
@@ -192,3 +192,22 @@ export interface IInputCreatedResponse {
   new_schema: ILibraryItem;
   oss: IOperationSchemaData;
 }
+
+/**
+ * Represents substitution error description.
+ */
+export interface ISubstitutionErrorDescription {
+  errorType: SubstitutionErrorType;
+  params: string[];
+}
+
+/**
+ * Represents Substitution table error types.
+ */
+export enum SubstitutionErrorType {
+  invalidIDs,
+  invalidClasses,
+  invalidBasic,
+  invalidConstant,
+  typificationCycle
+}
diff --git a/rsconcept/frontend/src/models/ossAPI.ts b/rsconcept/frontend/src/models/ossAPI.ts
index 48bc24ba..8a875813 100644
--- a/rsconcept/frontend/src/models/ossAPI.ts
+++ b/rsconcept/frontend/src/models/ossAPI.ts
@@ -2,10 +2,14 @@
  * Module: API for OperationSystem.
  */
 
+import { describeSubstitutionError, information } from '@/utils/labels';
 import { TextMatcher } from '@/utils/utils';
 
-import { ILibraryItem } from './library';
-import { IOperation, IOperationSchema } from './oss';
+import { Graph } from './Graph';
+import { ILibraryItem, LibraryItemID } from './library';
+import { ICstSubstitute, IOperation, IOperationSchema, SubstitutionErrorType } from './oss';
+import { ConstituentaID, CstType, IConstituenta, IRSForm } from './rsform';
+import { extractGlobals } from './rslangAPI';
 
 /**
  * Checks if a given target {@link IOperation} matches the specified query using.
@@ -43,3 +47,165 @@ export function sortItemsForOSS(oss: IOperationSchema, items: ILibraryItem[]): I
   }
   return result;
 }
+
+/**
+ * Validator for Substitution table.
+ *
+ */
+export class SubstitutionValidator {
+  public msg: string = '';
+
+  private schemas: IRSForm[];
+  private substitutions: ICstSubstitute[];
+  private cstByID = new Map<ConstituentaID, IConstituenta>();
+  private schemaByID = new Map<LibraryItemID, IRSForm>();
+  private schemaByCst = new Map<ConstituentaID, IRSForm>();
+
+  constructor(schemas: IRSForm[], substitutions: ICstSubstitute[]) {
+    this.schemas = schemas;
+    this.substitutions = substitutions;
+    schemas.forEach(schema => {
+      this.schemaByID.set(schema.id, schema);
+      schema.items.forEach(item => {
+        this.cstByID.set(item.id, item);
+        this.schemaByCst.set(item.id, schema);
+      });
+    });
+  }
+
+  public validate(): boolean {
+    if (this.substitutions.length === 0) {
+      return this.setValid();
+    }
+    if (!this.checkTypes()) {
+      return false;
+    }
+    if (!this.checkCycles()) {
+      return false;
+    }
+
+    return this.setValid();
+  }
+
+  private checkTypes(): boolean {
+    for (const item of this.substitutions) {
+      const original = this.cstByID.get(item.original);
+      const substitution = this.cstByID.get(item.substitution);
+      if (!original || !substitution) {
+        return this.reportError(SubstitutionErrorType.invalidIDs, []);
+      }
+      switch (substitution.cst_type) {
+        case CstType.BASE: {
+          if (original.cst_type !== CstType.BASE && original.cst_type !== CstType.CONSTANT) {
+            return this.reportError(SubstitutionErrorType.invalidBasic, [substitution.alias, original.alias]);
+          }
+          break;
+        }
+
+        case CstType.CONSTANT: {
+          if (original.cst_type !== CstType.CONSTANT) {
+            return this.reportError(SubstitutionErrorType.invalidConstant, [substitution.alias, original.alias]);
+          }
+          break;
+        }
+
+        case CstType.AXIOM:
+        case CstType.THEOREM: {
+          if (original.cst_type !== CstType.AXIOM && original.cst_type !== CstType.THEOREM) {
+            return this.reportError(SubstitutionErrorType.invalidClasses, [substitution.alias, original.alias]);
+          }
+          break;
+        }
+
+        case CstType.FUNCTION: {
+          if (original.cst_type !== CstType.FUNCTION) {
+            return this.reportError(SubstitutionErrorType.invalidClasses, [substitution.alias, original.alias]);
+          }
+          break;
+        }
+        case CstType.PREDICATE: {
+          if (original.cst_type !== CstType.PREDICATE) {
+            return this.reportError(SubstitutionErrorType.invalidClasses, [substitution.alias, original.alias]);
+          }
+          break;
+        }
+
+        case CstType.TERM:
+        case CstType.STRUCTURED: {
+          if (
+            original.cst_type !== CstType.TERM &&
+            original.cst_type !== CstType.STRUCTURED &&
+            original.cst_type !== CstType.BASE
+          ) {
+            return this.reportError(SubstitutionErrorType.invalidClasses, [substitution.alias, original.alias]);
+          }
+          break;
+        }
+      }
+    }
+    return true;
+  }
+
+  private checkCycles(): boolean {
+    const graph = new Graph();
+    for (const schema of this.schemas) {
+      for (const cst of schema.items) {
+        if (cst.cst_type === CstType.BASE || cst.cst_type === CstType.CONSTANT) {
+          graph.addNode(cst.id);
+        }
+      }
+    }
+    for (const item of this.substitutions) {
+      const original = this.cstByID.get(item.original)!;
+      const substitution = this.cstByID.get(item.substitution)!;
+      for (const cst of [original, substitution]) {
+        if (cst.cst_type === CstType.BASE || cst.cst_type === CstType.CONSTANT) {
+          continue;
+        }
+        graph.addNode(cst.id);
+        const parents = extractGlobals(cst.parse.typification);
+        for (const arg of cst.parse.args) {
+          for (const alias of extractGlobals(arg.typification)) {
+            parents.add(alias);
+          }
+        }
+        if (parents.size === 0) {
+          continue;
+        }
+        const schema = this.schemaByID.get(cst.schema)!;
+        for (const alias of parents) {
+          const parent = schema.cstByAlias.get(alias);
+          if (parent) {
+            graph.addEdge(parent.id, cst.id);
+          }
+        }
+      }
+      graph.addEdge(substitution.id, original.id);
+    }
+    const cycle = graph.findCycle();
+    if (cycle !== null) {
+      const cycleMsg = cycle
+        .map(id => {
+          const cst = this.cstByID.get(id)!;
+          const schema = this.schemaByID.get(cst.schema)!;
+          return `[${schema.alias}]-${cst.alias}`;
+        })
+        .join(', ');
+      return this.reportError(SubstitutionErrorType.typificationCycle, [cycleMsg]);
+    }
+    return true;
+  }
+
+  private setValid(): boolean {
+    this.msg = information.substitutionsCorrect;
+    return true;
+  }
+
+  private reportError(errorType: SubstitutionErrorType, params: string[]): boolean {
+    this.msg = describeSubstitutionError({
+      errorType: errorType,
+      params: params
+    });
+    return false;
+  }
+}
diff --git a/rsconcept/frontend/src/models/rslang.ts b/rsconcept/frontend/src/models/rslang.ts
index c83250c4..d1e6086c 100644
--- a/rsconcept/frontend/src/models/rslang.ts
+++ b/rsconcept/frontend/src/models/rslang.ts
@@ -199,6 +199,9 @@ export enum TokenID {
   END
 }
 
+/**
+ * Represents RSLang expression error types.
+ */
 export enum RSErrorType {
   unknownSymbol = 33283,
   syntax = 33792,
diff --git a/rsconcept/frontend/src/utils/labels.ts b/rsconcept/frontend/src/utils/labels.ts
index c342a495..ff4299a0 100644
--- a/rsconcept/frontend/src/utils/labels.ts
+++ b/rsconcept/frontend/src/utils/labels.ts
@@ -10,7 +10,7 @@ import { GramData, Grammeme, ReferenceType } from '@/models/language';
 import { AccessPolicy, LibraryItemType, LocationHead } from '@/models/library';
 import { validateLocation } from '@/models/libraryAPI';
 import { CstMatchMode, DependencyMode, GraphColoring, GraphSizing, HelpTopic } from '@/models/miscellaneous';
-import { OperationType } from '@/models/oss';
+import { ISubstitutionErrorDescription, OperationType, SubstitutionErrorType } from '@/models/oss';
 import { CstClass, CstType, ExpressionStatus, IConstituenta, IRSForm } from '@/models/rsform';
 import {
   IArgumentInfo,
@@ -799,6 +799,26 @@ export function describeRSError(error: IRSErrorDescription): string {
   return 'UNKNOWN ERROR';
 }
 
+/**
+ * Generates error description for {@link ISubstitutionErrorDescription}.
+ */
+export function describeSubstitutionError(error: ISubstitutionErrorDescription): string {
+  // prettier-ignore
+  switch (error.errorType) {
+    case SubstitutionErrorType.invalidIDs:
+      return 'Ошибка в идентификаторах схем'
+    case SubstitutionErrorType.invalidBasic:
+      return `Ошибка ${error.params[0]} -> ${error.params[1]}: замена структурного понятия базисным множеством`;
+    case SubstitutionErrorType.invalidConstant:
+      return `Ошибка ${error.params[0]} -> ${error.params[1]}: подстановка константного множества возможна только вместо другого константного`;
+    case SubstitutionErrorType.invalidClasses:
+      return `Ошибка ${error.params[0]} -> ${error.params[1]}: классы конституент не совпадают`;
+    case SubstitutionErrorType.typificationCycle:
+      return `Ошибка: цикл подстановок в типизациях ${error.params[0]}`;
+  }
+  return 'UNKNOWN ERROR';
+}
+
 /**
  * Retrieves label for {@link UserLevel}.
  */
@@ -934,6 +954,7 @@ export const information = {
   locationRenamed: 'Ваши схемы перемещены',
   cloneComplete: (alias: string) => `Копия создана: ${alias}`,
   noDataToExport: 'Нет данных для экспорта',
+  substitutionsCorrect: 'Таблица отождествлений прошла проверку',
 
   addedConstituents: (count: number) => `Добавлены конституенты: ${count}`,
   newLibraryItem: 'Схема успешно создана',