F: Implement typification checks on substitutions

rsconcept/frontend/src/models/oss.ts

@@ -206,8 +206,13 @@ export interface ISubstitutionErrorDescription {
  */
 export enum SubstitutionErrorType {
   invalidIDs,
+  incorrectCst,
   invalidClasses,
   invalidBasic,
   invalidConstant,
-  typificationCycle
+  typificationCycle,
+  baseSubstitutionNotSet,
+  unequalTypification,
+  unequalArgsCount,
+  unequalArgs
 }

rsconcept/frontend/src/models/ossAPI.ts

@@ -9,7 +9,8 @@ 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';
+import { AliasMapping, ParsingStatus } from './rslang';
+import { applyAliasMapping, applyTypificationMapping, extractGlobals, isSetTypification } from './rslangAPI';
 
 /**
  * Checks if a given target {@link IOperation} matches the specified query using.
@@ -48,9 +49,10 @@ export function sortItemsForOSS(oss: IOperationSchema, items: ILibraryItem[]): I
   return result;
 }
 
+type CrossMapping = Map<LibraryItemID, AliasMapping>;
+
 /**
  * Validator for Substitution table.
- *
  */
 export class SubstitutionValidator {
   public msg: string = '';
@@ -83,6 +85,9 @@ export class SubstitutionValidator {
     if (!this.checkCycles()) {
       return false;
     }
+    if (!this.checkTypifications()) {
+      return false;
+    }
 
     return this.setValid();
   }
@@ -94,6 +99,9 @@ export class SubstitutionValidator {
       if (!original || !substitution) {
         return this.reportError(SubstitutionErrorType.invalidIDs, []);
       }
+      if (original.parse.status === ParsingStatus.INCORRECT || substitution.parse.status === ParsingStatus.INCORRECT) {
+        return this.reportError(SubstitutionErrorType.incorrectCst, [substitution.alias, original.alias]);
+      }
       switch (substitution.cst_type) {
         case CstType.BASE: {
           if (original.cst_type !== CstType.BASE && original.cst_type !== CstType.CONSTANT) {
@@ -196,6 +204,112 @@ export class SubstitutionValidator {
     return true;
   }
 
+  private checkTypifications(): boolean {
+    const baseMappings = this.prepareBaseMappings();
+    const typeMappings = this.calculateSubstituteMappings(baseMappings);
+    if (typeMappings === null) {
+      return false;
+    }
+    for (const item of this.substitutions) {
+      const original = this.cstByID.get(item.original)!;
+      if (original.cst_type === CstType.BASE || original.cst_type === CstType.CONSTANT) {
+        continue;
+      }
+      const substitution = this.cstByID.get(item.substitution)!;
+      const originalType = applyTypificationMapping(
+        applyAliasMapping(original.parse.typification, baseMappings.get(original.schema)!),
+        typeMappings
+      );
+      const substitutionType = applyTypificationMapping(
+        applyAliasMapping(substitution.parse.typification, baseMappings.get(substitution.schema)!),
+        typeMappings
+      );
+      if (originalType !== substitutionType) {
+        return this.reportError(SubstitutionErrorType.unequalTypification, [substitution.alias, original.alias]);
+      }
+      if (original.parse.args.length === 0) {
+        continue;
+      }
+      if (substitution.parse.args.length !== original.parse.args.length) {
+        return this.reportError(SubstitutionErrorType.unequalArgsCount, [substitution.alias, original.alias]);
+      }
+      for (let i = 0; i < original.parse.args.length; ++i) {
+        const originalArg = applyTypificationMapping(
+          applyAliasMapping(original.parse.args[i].typification, baseMappings.get(original.schema)!),
+          typeMappings
+        );
+        const substitutionArg = applyTypificationMapping(
+          applyAliasMapping(substitution.parse.args[i].typification, baseMappings.get(substitution.schema)!),
+          typeMappings
+        );
+        if (originalArg !== substitutionArg) {
+          return this.reportError(SubstitutionErrorType.unequalArgs, [substitution.alias, original.alias]);
+        }
+      }
+    }
+    return true;
+  }
+
+  private prepareBaseMappings(): CrossMapping {
+    const result: CrossMapping = new Map();
+    let baseCount = 0;
+    let constCount = 0;
+    for (const schema of this.schemas) {
+      const mapping: AliasMapping = {};
+      for (const cst of schema.items) {
+        if (cst.cst_type === CstType.BASE) {
+          baseCount++;
+          mapping[cst.alias] = `X${baseCount}`;
+        } else if (cst.cst_type === CstType.CONSTANT) {
+          constCount++;
+          mapping[cst.alias] = `C${constCount}`;
+        }
+        result.set(schema.id, mapping);
+      }
+    }
+    return result;
+  }
+
+  private calculateSubstituteMappings(baseMappings: CrossMapping): AliasMapping | null {
+    const result: AliasMapping = {};
+    const processed = new Set<string>();
+    for (const item of this.substitutions) {
+      const original = this.cstByID.get(item.original)!;
+      if (original.cst_type !== CstType.BASE && original.cst_type !== CstType.CONSTANT) {
+        continue;
+      }
+      const originalAlias = baseMappings.get(original.schema)![original.alias];
+
+      const substitution = this.cstByID.get(item.substitution)!;
+      let substitutionText = '';
+      if (substitution.cst_type === original.cst_type) {
+        substitutionText = baseMappings.get(substitution.schema)![substitution.alias];
+      } else {
+        substitutionText = applyAliasMapping(substitution.parse.typification, baseMappings.get(substitution.schema)!);
+        substitutionText = applyTypificationMapping(substitutionText, result);
+        console.log(substitutionText);
+        if (!isSetTypification(substitutionText)) {
+          this.reportError(SubstitutionErrorType.baseSubstitutionNotSet, [
+            substitution.alias,
+            substitution.parse.typification
+          ]);
+          return null;
+        }
+        if (substitutionText.includes('×') || substitutionText.startsWith('ℬℬ')) {
+          substitutionText = substitutionText.slice(1);
+        } else {
+          substitutionText = substitutionText.slice(2, -1);
+        }
+      }
+      for (const prevAlias of processed) {
+        result[prevAlias] = applyTypificationMapping(result[prevAlias], { [originalAlias]: substitutionText });
+      }
+      result[originalAlias] = substitutionText;
+      processed.add(originalAlias);
+    }
+    return result;
+  }
+
   private setValid(): boolean {
     this.msg = information.substitutionsCorrect;
     return true;

rsconcept/frontend/src/models/rslang.ts

@@ -2,6 +2,11 @@
  * Module: Models for RSLanguage.
  */
 
+/**
+ * Represents alias mapping.
+ */
+export type AliasMapping = Record<string, string>;
+
 /**
  * Represents formal expression.
  */

rsconcept/frontend/src/models/rslangAPI.ts

@@ -5,12 +5,13 @@
 import { applyPattern } from '@/utils/utils';
 
 import { CstType } from './rsform';
-import { IArgumentValue, IRSErrorDescription, RSErrorClass, RSErrorType } from './rslang';
+import { AliasMapping, IArgumentValue, IRSErrorDescription, RSErrorClass, RSErrorType } from './rslang';
 
 // cspell:disable
 const LOCALS_REGEXP = /[_a-zα-ω][a-zα-ω]*\d*/g;
 const GLOBALS_REGEXP = /[XCSADFPT]\d+/g;
 const COMPLEX_SYMBOLS_REGEXP = /[∀∃×ℬ;|:]/g;
+const TYPIFICATION_SET = /^ℬ+\([ℬ\(X\d+\)×]*\)$/g;
 // cspell:enable
 
 /**
@@ -27,6 +28,13 @@ export function isSimpleExpression(text: string): boolean {
   return !text.match(COMPLEX_SYMBOLS_REGEXP);
 }
 
+/**
+ * Check if expression is set typification.
+ */
+export function isSetTypification(text: string): boolean {
+  return !!text.match(TYPIFICATION_SET);
+}
+
 /**
  * Infers type of constituent for a given template and arguments.
  */
@@ -91,7 +99,7 @@ export function substituteTemplateArgs(expression: string, args: IArgumentValue[
     return expression;
   }
 
-  const mapping: Record<string, string> = {};
+  const mapping: AliasMapping = {};
   args
     .filter(arg => !!arg.value)
     .forEach(arg => {
@@ -144,3 +152,25 @@ export function getRSErrorPrefix(error: IRSErrorDescription): string {
     case RSErrorClass.UNKNOWN: return 'U' + id;
   }
 }
+
+/**
+ * Apply alias mapping.
+ */
+export function applyAliasMapping(target: string, mapping: AliasMapping): string {
+  return applyPattern(target, mapping, GLOBALS_REGEXP);
+}
+
+/**
+ * Apply alias typification mapping.
+ */
+export function applyTypificationMapping(target: string, mapping: AliasMapping): string {
+  const result = applyAliasMapping(target, mapping);
+  if (result === target) {
+    return target;
+  }
+
+  // remove double parentheses
+  // deal with ℬ(ℬ)
+
+  return result;
+}

rsconcept/frontend/src/utils/labels.ts

@@ -803,10 +803,11 @@ export function describeRSError(error: IRSErrorDescription): string {
  * Generates error description for {@link ISubstitutionErrorDescription}.
  */
 export function describeSubstitutionError(error: ISubstitutionErrorDescription): string {
-  // prettier-ignore
   switch (error.errorType) {
     case SubstitutionErrorType.invalidIDs:
-      return 'Ошибка в идентификаторах схем'
+      return 'Ошибка в идентификаторах схем';
+    case SubstitutionErrorType.incorrectCst:
+      return `Ошибка ${error.params[0]} -> ${error.params[1]}: некорректное выражение конституенты`;
     case SubstitutionErrorType.invalidBasic:
       return `Ошибка ${error.params[0]} -> ${error.params[1]}: замена структурного понятия базисным множеством`;
     case SubstitutionErrorType.invalidConstant:
@@ -815,6 +816,14 @@ export function describeSubstitutionError(error: ISubstitutionErrorDescription):
       return `Ошибка ${error.params[0]} -> ${error.params[1]}: классы конституент не совпадают`;
     case SubstitutionErrorType.typificationCycle:
       return `Ошибка: цикл подстановок в типизациях ${error.params[0]}`;
+    case SubstitutionErrorType.baseSubstitutionNotSet:
+      return `Ошибка: типизация не задает множество ${error.params[0]} ∈ ${error.params[1]}`;
+    case SubstitutionErrorType.unequalTypification:
+      return `Ошибка ${error.params[0]} -> ${error.params[1]}: типизация структурных операндов не совпадает`;
+    case SubstitutionErrorType.unequalArgsCount:
+      return `Ошибка ${error.params[0]} -> ${error.params[1]}: количество аргументов не совпадает`;
+    case SubstitutionErrorType.unequalArgs:
+      return `Ошибка ${error.params[0]} -> ${error.params[1]}: типизация аргументов не совпадает`;
   }
   return 'UNKNOWN ERROR';
 }

rsconcept/frontend/src/utils/utils.ts

@@ -4,6 +4,8 @@
 
 import axios, { AxiosError, AxiosHeaderValue, AxiosResponse } from 'axios';
 
+import { AliasMapping } from '@/models/rslang';
+
 import { prompts } from './labels';
 
 /**
@@ -46,7 +48,7 @@ export class TextMatcher {
 /**
  * Text substitution guided by mapping and regular expression.
  */
-export function applyPattern(text: string, mapping: Record<string, string>, pattern: RegExp): string {
+export function applyPattern(text: string, mapping: AliasMapping, pattern: RegExp): string {
   if (text === '' || pattern === null) {
     return text;
   }