Implement template argument substitutions

rsconcept/frontend/src/models/rslangAPI.test.ts

@@ -0,0 +1,32 @@
+import { extractGlobals, splitTemplateDefinition } from './rslangAPI';
+
+const globalsData = [
+  ['', ''],
+  ['X1', 'X1'],
+  ['X11 X1 X11', 'X11 X1'],
+  ['∀α∈S1 ∀β∈F1[α] Pr1,1(β)∩β=∅', 'S1 F1'],
+]
+describe('Testing extract globals', () => {
+  it.each(globalsData)('Extract globals %p', 
+  (input: string, expected: string) => {
+    const result = extractGlobals(input);
+    expect([...result].join(' ')).toBe(expected);
+  });
+});
+
+
+const splitData = [
+  ['', '||'],
+  ['[α∈ℬ(R1)] α⊆red(σ)', 'α∈ℬ(R1)||α⊆red(σ)'],
+  ['[α∈ℬ(R1)] α⊆red(σ) ', 'α∈ℬ(R1)||α⊆red(σ)'],
+  [' [α∈ℬ(R1)] α⊆red(σ)', 'α∈ℬ(R1)||α⊆red(σ)'],
+  ['[α∈ℬ(R1)]α⊆red(σ)', 'α∈ℬ(R1)||α⊆red(σ)'],
+  ['[α∈ℬ(R1), σ∈ℬℬ(R1)] α⊆red(σ)', 'α∈ℬ(R1), σ∈ℬℬ(R1)||α⊆red(σ)'],
+]
+describe('Testing split template', () => {
+  it.each(splitData)('Split %p', 
+  (input: string, expected: string) => {
+    const result = splitTemplateDefinition(input);
+    expect(`${result.head}||${result.body}`).toBe(expected);
+  });
+});

rsconcept/frontend/src/models/rslangAPI.ts

@@ -1,8 +1,11 @@
 // Module: RSLang model API
 
+import { applyPattern } from '../utils/utils';
 import { CstType } from './rsform';
 import { IArgumentValue } from './rslang'
 
+const LOCALS_REGEXP = /[_a-zα-ω][a-zα-ω]*\d*/g;
+
 export function extractGlobals(expression: string): Set<string> {
   return new Set(expression.match(/[XCSADFPT]\d+/g) ?? []);
 }
@@ -17,20 +20,6 @@ export function inferTemplatedType(templateType: CstType, args: IArgumentValue[]
   }
 }
 
-export function substituteTemplateArgs(expression: string, args: IArgumentValue[]): string {
-  if (args.every(arg => !arg.value)) {
-    return expression;
-  }
-
-  const mapping: { [key: string]: string } = {};
-  args.filter(arg => !!arg.value).forEach(arg => { mapping[arg.alias] = arg.value!; })
-
-
-
-  // TODO: figure out actual substitution
-  return expression
-}
-
 export function splitTemplateDefinition(target: string) {
   let start = 0;
   for (; start < target.length && target[start] !== '['; ++start) ;
@@ -42,7 +31,10 @@ export function splitTemplateDefinition(target: string) {
         if (counter !== 0) {
           --counter;
         } else {
-          
+          return {
+            head: target.substring(start + 1, end).trim(),
+            body: target.substring(end + 1).trim()
+          }
         }
       }
     }
@@ -53,39 +45,31 @@ export function splitTemplateDefinition(target: string) {
   }
 }
 
-// function applyPattern(text: string, mapping: { [key: string]: string }, pattern: RegExp): string {
-//   /** Apply mapping to matching in regular expression patter subgroup 1. */
-//   if (text === '' || pattern === null) {
-//       return text;
-//   }
-//   let posInput: number = 0;
-//   let output: string = '';
-//   const patternMatches = text.matchAll(pattern);
-//   for (const segment of patternMatches) {
-//       const entity = segment[1];
-//       if (entity in mapping) {
-//           output += text.substring(posInput, segment.index);
-//           output += mapping[entity];
-//           output += text.substring(segment.index, segment.index + segment[0].length);
-//           posInput = segment.index + segment[0].length;
-//       }
-//   }
-//   output += text.substring(posInput);
-//   return output;
-// }
+export function substituteTemplateArgs(expression: string, args: IArgumentValue[]): string {
+  if (args.every(arg => !arg.value)) {
+    return expression;
+  }
 
-// def apply_pattern(text: str, mapping: dict[str, str], pattern: re.Pattern[str]) -> str:
-//     ''' Apply mapping to matching in regular expression patter subgroup 1. '''
-//     if text == '' or pattern == '':
-//         return text
-//     pos_input: int = 0
-//     output: str = ''
-//     for segment in re.finditer(pattern, text):
-//         entity = segment.group(1)
-//         if entity in mapping:
-//             output += text[pos_input : segment.start(1)]
-//             output += mapping[entity]
-//             output += text[segment.end(1) : segment.end(0)]
-//             pos_input = segment.end(0)
-//     output += text[pos_input : len(text)]
-//     return output
+  const mapping: { [key: string]: string } = {};
+  args.filter(arg => !!arg.value).forEach(arg => { mapping[arg.alias] = arg.value!; })
+
+  let { head, body } = splitTemplateDefinition(expression);
+  body = applyPattern(body, mapping, LOCALS_REGEXP);
+  const argTexts = head.split(',').map(text => text.trim());
+  head = argTexts
+  .filter(
+    arg => [...arg.matchAll(LOCALS_REGEXP)]
+      .every(local => local.every(match => !(match in mapping)))
+  ).join(', ');
+
+  console.log(body);
+  console.log(head);
+  console.log(args);
+  console.log(mapping);
+
+  if (!head) {
+    return body;
+  } else {
+    return `[${head}] ${body}`
+  }
+}

rsconcept/frontend/src/utils/utils.tsx

@@ -31,3 +31,26 @@ export class TextMatcher {
     }
   }
 }
+
+/**
+ * Text substitution guided by mapping and regular explression.
+*/
+export function applyPattern(text: string, mapping: { [key: string]: string }, pattern: RegExp): string {
+  if (text === '' || pattern === null) {
+    return text;
+  }
+  let posInput = 0;
+  let output = '';
+  const patternMatches = text.matchAll(pattern);
+  for (const segment of patternMatches) {
+    const entity = segment[0];
+    const start = segment.index!;
+    if (entity in mapping) {
+      output += text.substring(posInput, start);
+      output += mapping[entity];
+      posInput = start + segment[0].length;
+    }
+  }
+  output += text.substring(posInput);
+  return output;
+}