From fa6eb49172bef3d61e91e8191f18f199fd11040c Mon Sep 17 00:00:00 2001
From: Ivan <8611739+IRBorisov@users.noreply.github.com>
Date: Wed, 28 Aug 2024 12:34:29 +0300
Subject: [PATCH] M: Add warning if term expressions are not equal

---
 .../dialogs/DlgEditOperation/TabSynthesis.tsx |  7 +-
 rsconcept/frontend/src/models/oss.ts          |  1 +
 rsconcept/frontend/src/models/ossAPI.ts       | 65 +++++++++++++++++--
 rsconcept/frontend/src/models/rsformAPI.ts    |  2 +-
 rsconcept/frontend/src/utils/constants.ts     |  3 +-
 rsconcept/frontend/src/utils/labels.ts        |  2 +
 6 files changed, 72 insertions(+), 8 deletions(-)

diff --git a/rsconcept/frontend/src/dialogs/DlgEditOperation/TabSynthesis.tsx b/rsconcept/frontend/src/dialogs/DlgEditOperation/TabSynthesis.tsx
index 5ee90712..be822e37 100644
--- a/rsconcept/frontend/src/dialogs/DlgEditOperation/TabSynthesis.tsx
+++ b/rsconcept/frontend/src/dialogs/DlgEditOperation/TabSynthesis.tsx
@@ -37,7 +37,12 @@ function TabSynthesis({
         substitutions={substitutions}
         setSubstitutions={setSubstitutions}
       />
-      <TextArea disabled value={validationText} style={{ borderColor: isCorrect ? undefined : colors.fgRed }} />
+      <TextArea
+        disabled
+        value={validationText}
+        rows={4}
+        style={{ borderColor: isCorrect ? undefined : colors.fgRed }}
+      />
     </DataLoader>
   );
 }
diff --git a/rsconcept/frontend/src/models/oss.ts b/rsconcept/frontend/src/models/oss.ts
index 5a6c08cc..e5b33c3b 100644
--- a/rsconcept/frontend/src/models/oss.ts
+++ b/rsconcept/frontend/src/models/oss.ts
@@ -213,6 +213,7 @@ export enum SubstitutionErrorType {
   typificationCycle,
   baseSubstitutionNotSet,
   unequalTypification,
+  unequalExpressions,
   unequalArgsCount,
   unequalArgs
 }
diff --git a/rsconcept/frontend/src/models/ossAPI.ts b/rsconcept/frontend/src/models/ossAPI.ts
index a01ba772..d5d6bbde 100644
--- a/rsconcept/frontend/src/models/ossAPI.ts
+++ b/rsconcept/frontend/src/models/ossAPI.ts
@@ -2,13 +2,15 @@
  * Module: API for OperationSystem.
  */
 
+import { limits } from '@/utils/constants';
 import { describeSubstitutionError, information } from '@/utils/labels';
 import { TextMatcher } from '@/utils/utils';
 
 import { Graph } from './Graph';
 import { ILibraryItem, LibraryItemID } from './library';
 import { ICstSubstitute, IOperation, IOperationSchema, SubstitutionErrorType } from './oss';
-import { ConstituentaID, CstType, IConstituenta, IRSForm } from './rsform';
+import { ConstituentaID, CstClass, CstType, IConstituenta, IRSForm } from './rsform';
+import { inferClass } from './rsformAPI';
 import { AliasMapping, ParsingStatus } from './rslang';
 import { applyAliasMapping, applyTypificationMapping, extractGlobals, isSetTypification } from './rslangAPI';
 
@@ -51,6 +53,7 @@ export function sortItemsForOSS(oss: IOperationSchema, items: ILibraryItem[]): I
 
 type CrossMapping = Map<LibraryItemID, AliasMapping>;
 
+// TODO: test validator
 /**
  * Validator for Substitution table.
  */
@@ -59,6 +62,10 @@ export class SubstitutionValidator {
 
   private schemas: IRSForm[];
   private substitutions: ICstSubstitute[];
+  private constituents = new Set<ConstituentaID>();
+  private originals = new Set<ConstituentaID>();
+  private mapping: CrossMapping = new Map();
+
   private cstByID = new Map<ConstituentaID, IConstituenta>();
   private schemaByID = new Map<LibraryItemID, IRSForm>();
   private schemaByCst = new Map<ConstituentaID, IRSForm>();
@@ -66,13 +73,32 @@ export class SubstitutionValidator {
   constructor(schemas: IRSForm[], substitutions: ICstSubstitute[]) {
     this.schemas = schemas;
     this.substitutions = substitutions;
+    if (this.substitutions.length === 0) {
+      return;
+    }
     schemas.forEach(schema => {
       this.schemaByID.set(schema.id, schema);
+      this.mapping.set(schema.id, {});
       schema.items.forEach(item => {
         this.cstByID.set(item.id, item);
         this.schemaByCst.set(item.id, schema);
       });
     });
+    let index = limits.max_semantic_index;
+    substitutions.forEach(item => {
+      this.constituents.add(item.original);
+      this.constituents.add(item.substitution);
+      this.originals.add(item.original);
+      const original = this.cstByID.get(item.original);
+      const substitution = this.cstByID.get(item.substitution);
+      if (!original || !substitution) {
+        return;
+      }
+      index++;
+      const newAlias = `${substitution.alias[0]}${index}`;
+      this.mapping.get(original.schema)![original.alias] = newAlias;
+      this.mapping.get(substitution.schema)![substitution.alias] = newAlias;
+    });
   }
 
   public validate(): boolean {
@@ -85,7 +111,7 @@ export class SubstitutionValidator {
     if (!this.checkCycles()) {
       return false;
     }
-    if (!this.checkTypifications()) {
+    if (!this.checkSubstitutions()) {
       return false;
     }
 
@@ -204,7 +230,7 @@ export class SubstitutionValidator {
     return true;
   }
 
-  private checkTypifications(): boolean {
+  private checkSubstitutions(): boolean {
     const baseMappings = this.prepareBaseMappings();
     const typeMappings = this.calculateSubstituteMappings(baseMappings);
     if (typeMappings === null) {
@@ -216,6 +242,13 @@ export class SubstitutionValidator {
         continue;
       }
       const substitution = this.cstByID.get(item.substitution)!;
+      if (original.cst_type === substitution.cst_type && inferClass(original.cst_type) === CstClass.DERIVED) {
+        if (!this.checkEqual(original, substitution)) {
+          this.reportError(SubstitutionErrorType.unequalExpressions, [substitution.alias, original.alias]);
+          // Note: do not interrupt the validation process. Only warn about the problem.
+        }
+      }
+
       const originalType = applyTypificationMapping(
         applyAliasMapping(original.parse.typification, baseMappings.get(original.schema)!),
         typeMappings
@@ -310,13 +343,35 @@ export class SubstitutionValidator {
     return result;
   }
 
+  private checkEqual(left: IConstituenta, right: IConstituenta): boolean {
+    const schema1 = this.schemaByID.get(left.schema)!;
+    const inputs1 = schema1.graph.at(left.id)!.inputs;
+    if (inputs1.some(id => !this.constituents.has(id))) {
+      return false;
+    }
+    const schema2 = this.schemaByID.get(right.schema)!;
+    const inputs2 = schema2.graph.at(right.id)!.inputs;
+    if (inputs2.some(id => !this.constituents.has(id))) {
+      return false;
+    }
+    const expression1 = applyAliasMapping(left.definition_formal, this.mapping.get(schema1.id)!);
+    const expression2 = applyAliasMapping(right.definition_formal, this.mapping.get(schema2.id)!);
+    return expression1.replace(' ', '') === expression2.replace(' ', '');
+  }
+
   private setValid(): boolean {
-    this.msg = information.substitutionsCorrect;
+    if (this.msg.length > 0) {
+      this.msg += '\n';
+    }
+    this.msg += information.substitutionsCorrect;
     return true;
   }
 
   private reportError(errorType: SubstitutionErrorType, params: string[]): boolean {
-    this.msg = describeSubstitutionError({
+    if (this.msg.length > 0) {
+      this.msg += '\n';
+    }
+    this.msg += describeSubstitutionError({
       errorType: errorType,
       params: params
     });
diff --git a/rsconcept/frontend/src/models/rsformAPI.ts b/rsconcept/frontend/src/models/rsformAPI.ts
index f209db0f..d3f2c058 100644
--- a/rsconcept/frontend/src/models/rsformAPI.ts
+++ b/rsconcept/frontend/src/models/rsformAPI.ts
@@ -93,7 +93,7 @@ export function inferTemplate(expression: string): boolean {
  * - `CstClass.DERIVED` if the CstType is TERM, FUNCTION, or PREDICATE.
  * - `CstClass.STATEMENT` if the CstType is AXIOM or THEOREM.
  */
-export function inferClass(type: CstType, isTemplate: boolean): CstClass {
+export function inferClass(type: CstType, isTemplate: boolean = false): CstClass {
   if (isTemplate) {
     return CstClass.TEMPLATE;
   }
diff --git a/rsconcept/frontend/src/utils/constants.ts b/rsconcept/frontend/src/utils/constants.ts
index b24e1200..08400d9c 100644
--- a/rsconcept/frontend/src/utils/constants.ts
+++ b/rsconcept/frontend/src/utils/constants.ts
@@ -42,7 +42,8 @@ export const PARAMETER = {
  * Numeric limitations.
  */
 export const limits = {
-  location_len: 500
+  location_len: 500,
+  max_semantic_index: 900
 };
 
 /**
diff --git a/rsconcept/frontend/src/utils/labels.ts b/rsconcept/frontend/src/utils/labels.ts
index 3eb769fe..3000c859 100644
--- a/rsconcept/frontend/src/utils/labels.ts
+++ b/rsconcept/frontend/src/utils/labels.ts
@@ -824,6 +824,8 @@ export function describeSubstitutionError(error: ISubstitutionErrorDescription):
       return `Ошибка ${error.params[0]} -> ${error.params[1]}: количество аргументов не совпадает`;
     case SubstitutionErrorType.unequalArgs:
       return `Ошибка ${error.params[0]} -> ${error.params[1]}: типизация аргументов не совпадает`;
+    case SubstitutionErrorType.unequalExpressions:
+      return `Предупреждение ${error.params[0]} -> ${error.params[1]}: определения понятий не совпадают`;
   }
   return 'UNKNOWN ERROR';
 }