mirror of
https://github.com/IRBorisov/ConceptPortal.git
synced 2025-06-26 04:50:36 +03:00
Add datastructure for Term graph
This commit is contained in:
parent
11b7914d37
commit
d7138e8b37
18
rsconcept/frontend/src/pages/RSFormPage/EditorTermGraph.tsx
Normal file
18
rsconcept/frontend/src/pages/RSFormPage/EditorTermGraph.tsx
Normal file
|
@ -0,0 +1,18 @@
|
||||||
|
import PrettyJson from '../../components/Common/PrettyJSON';
|
||||||
|
import { useRSForm } from '../../context/RSFormContext';
|
||||||
|
import { GraphNode } from '../../utils/Graph';
|
||||||
|
|
||||||
|
function EditorTermGraph() {
|
||||||
|
const { schema } = useRSForm();
|
||||||
|
|
||||||
|
const data: GraphNode[] = [];
|
||||||
|
schema?.graph.visitDFS(node => data.push(node));
|
||||||
|
|
||||||
|
return (
|
||||||
|
<div>
|
||||||
|
<PrettyJson data={data} />
|
||||||
|
</div>
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
export default EditorTermGraph;
|
|
@ -17,13 +17,15 @@ import DlgUploadRSForm from './DlgUploadRSForm';
|
||||||
import EditorConstituenta from './EditorConstituenta';
|
import EditorConstituenta from './EditorConstituenta';
|
||||||
import EditorItems from './EditorItems';
|
import EditorItems from './EditorItems';
|
||||||
import EditorRSForm from './EditorRSForm';
|
import EditorRSForm from './EditorRSForm';
|
||||||
|
import EditorTermGraph from './EditorTermGraph';
|
||||||
import RSFormStats from './elements/RSFormStats';
|
import RSFormStats from './elements/RSFormStats';
|
||||||
import RSTabsMenu from './RSTabsMenu';
|
import RSTabsMenu from './RSTabsMenu';
|
||||||
|
|
||||||
export enum RSTabsList {
|
export enum RSTabsList {
|
||||||
CARD = 0,
|
CARD = 0,
|
||||||
CST_LIST = 1,
|
CST_LIST = 1,
|
||||||
CST_EDIT = 2
|
CST_EDIT = 2,
|
||||||
|
TERM_GRAPH = 3
|
||||||
}
|
}
|
||||||
|
|
||||||
function RSTabs() {
|
function RSTabs() {
|
||||||
|
@ -169,6 +171,7 @@ function RSTabs() {
|
||||||
<span>{`${schema.stats?.count_errors ?? 0} | ${schema.stats?.count_all ?? 0}`}</span>
|
<span>{`${schema.stats?.count_errors ?? 0} | ${schema.stats?.count_all ?? 0}`}</span>
|
||||||
</ConceptTab>
|
</ConceptTab>
|
||||||
<ConceptTab>Редактор</ConceptTab>
|
<ConceptTab>Редактор</ConceptTab>
|
||||||
|
<ConceptTab>Граф термов</ConceptTab>
|
||||||
</TabList>
|
</TabList>
|
||||||
|
|
||||||
<TabPanel className='flex items-start w-full gap-2'>
|
<TabPanel className='flex items-start w-full gap-2'>
|
||||||
|
@ -183,6 +186,10 @@ function RSTabs() {
|
||||||
<TabPanel>
|
<TabPanel>
|
||||||
<EditorConstituenta onShowAST={onShowAST} onShowCreateCst={onShowCreateCst} />
|
<EditorConstituenta onShowAST={onShowAST} onShowCreateCst={onShowCreateCst} />
|
||||||
</TabPanel>
|
</TabPanel>
|
||||||
|
|
||||||
|
<TabPanel>
|
||||||
|
<EditorTermGraph />
|
||||||
|
</TabPanel>
|
||||||
</Tabs>
|
</Tabs>
|
||||||
</>
|
</>
|
||||||
}
|
}
|
||||||
|
|
|
@ -4,8 +4,8 @@ import Checkbox from '../../../components/Common/Checkbox';
|
||||||
import DataTableThemed from '../../../components/Common/DataTableThemed';
|
import DataTableThemed from '../../../components/Common/DataTableThemed';
|
||||||
import { useRSForm } from '../../../context/RSFormContext';
|
import { useRSForm } from '../../../context/RSFormContext';
|
||||||
import useLocalStorage from '../../../hooks/useLocalStorage';
|
import useLocalStorage from '../../../hooks/useLocalStorage';
|
||||||
import { CstType, type IConstituenta, matchConstituenta } from '../../../utils/models';
|
import { CstType, extractGlobals,type IConstituenta, matchConstituenta } from '../../../utils/models';
|
||||||
import { extractGlobals, getMockConstituenta } from '../../../utils/staticUI';
|
import { getMockConstituenta } from '../../../utils/staticUI';
|
||||||
|
|
||||||
interface ViewSideConstituentsProps {
|
interface ViewSideConstituentsProps {
|
||||||
expression: string
|
expression: string
|
||||||
|
|
88
rsconcept/frontend/src/utils/Graph.ts
Normal file
88
rsconcept/frontend/src/utils/Graph.ts
Normal file
|
@ -0,0 +1,88 @@
|
||||||
|
// Graph class with basic comparison. Does not work for objects
|
||||||
|
export class GraphNode {
|
||||||
|
id: number;
|
||||||
|
adjacent: number[];
|
||||||
|
|
||||||
|
constructor(id: number) {
|
||||||
|
this.id = id;
|
||||||
|
this.adjacent = [];
|
||||||
|
}
|
||||||
|
|
||||||
|
addAdjacent(node: number): void {
|
||||||
|
this.adjacent.push(node);
|
||||||
|
}
|
||||||
|
|
||||||
|
removeAdjacent(target: number): number | null {
|
||||||
|
const index = this.adjacent.findIndex(node => node === target);
|
||||||
|
if (index > -1) {
|
||||||
|
return this.adjacent.splice(index, 1)[0];
|
||||||
|
}
|
||||||
|
return null;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
export class Graph {
|
||||||
|
nodes: Map<number, GraphNode> = new Map();
|
||||||
|
|
||||||
|
constructor() {}
|
||||||
|
|
||||||
|
addNode(target: number): GraphNode {
|
||||||
|
let node = this.nodes.get(target);
|
||||||
|
if (!node) {
|
||||||
|
node = new GraphNode(target);
|
||||||
|
this.nodes.set(target, node);
|
||||||
|
}
|
||||||
|
return node;
|
||||||
|
}
|
||||||
|
|
||||||
|
removeNode(target: number): GraphNode | null {
|
||||||
|
const nodeToRemove = this.nodes.get(target);
|
||||||
|
if (!nodeToRemove) {
|
||||||
|
return null;
|
||||||
|
}
|
||||||
|
this.nodes.forEach((node) => {
|
||||||
|
node.removeAdjacent(nodeToRemove.id);
|
||||||
|
});
|
||||||
|
this.nodes.delete(target);
|
||||||
|
return nodeToRemove;
|
||||||
|
}
|
||||||
|
|
||||||
|
addEdge(source: number, destination: number): void {
|
||||||
|
const sourceNode = this.addNode(source);
|
||||||
|
const destinationNode = this.addNode(destination);
|
||||||
|
sourceNode.addAdjacent(destinationNode.id);
|
||||||
|
}
|
||||||
|
|
||||||
|
removeEdge(source: number, destination: number): void {
|
||||||
|
const sourceNode = this.nodes.get(source);
|
||||||
|
const destinationNode = this.nodes.get(destination);
|
||||||
|
if (sourceNode && destinationNode) {
|
||||||
|
sourceNode.removeAdjacent(destination);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
visitDFS(visitor: (node: GraphNode) => void) {
|
||||||
|
const visited: Map<number, boolean> = new Map();
|
||||||
|
this.nodes.forEach(node => {
|
||||||
|
if (!visited.has(node.id)) {
|
||||||
|
this.depthFirstSearchAux(node, visited, visitor);
|
||||||
|
}
|
||||||
|
});
|
||||||
|
}
|
||||||
|
|
||||||
|
private depthFirstSearchAux(node: GraphNode, visited: Map<number, boolean>, visitor: (node: GraphNode) => void): void {
|
||||||
|
if (!node) {
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
visited.set(node.id, true);
|
||||||
|
|
||||||
|
visitor(node);
|
||||||
|
|
||||||
|
node.adjacent.forEach((item) => {
|
||||||
|
if (!visited.has(item)) {
|
||||||
|
const childNode = this.nodes.get(item);
|
||||||
|
if (childNode) this.depthFirstSearchAux(childNode, visited, visitor);
|
||||||
|
}
|
||||||
|
});
|
||||||
|
}
|
||||||
|
}
|
|
@ -1,4 +1,5 @@
|
||||||
import { RSErrorType, TokenID } from './enums'
|
import { RSErrorType, TokenID } from './enums'
|
||||||
|
import { Graph } from './Graph'
|
||||||
|
|
||||||
// ========= Users ===========
|
// ========= Users ===========
|
||||||
export interface IUser {
|
export interface IUser {
|
||||||
|
@ -175,6 +176,7 @@ export interface IRSForm {
|
||||||
owner: number | null
|
owner: number | null
|
||||||
items: IConstituenta[]
|
items: IConstituenta[]
|
||||||
stats: IRSFormStats
|
stats: IRSFormStats
|
||||||
|
graph: Graph
|
||||||
}
|
}
|
||||||
|
|
||||||
export interface IRSFormData extends Omit<IRSForm, 'stats' > {}
|
export interface IRSFormData extends Omit<IRSForm, 'stats' > {}
|
||||||
|
@ -212,6 +214,11 @@ export enum ExpressionStatus {
|
||||||
VERIFIED
|
VERIFIED
|
||||||
}
|
}
|
||||||
|
|
||||||
|
// ========== Model functions =================
|
||||||
|
export function extractGlobals(expression: string): Set<string> {
|
||||||
|
return new Set(expression.match(/[XCSADFPT]\d+/g) ?? []);
|
||||||
|
}
|
||||||
|
|
||||||
export function inferStatus(parse?: ParsingStatus, value?: ValueClass): ExpressionStatus {
|
export function inferStatus(parse?: ParsingStatus, value?: ValueClass): ExpressionStatus {
|
||||||
if (!parse || !value) {
|
if (!parse || !value) {
|
||||||
return ExpressionStatus.UNDEFINED;
|
return ExpressionStatus.UNDEFINED;
|
||||||
|
@ -233,6 +240,7 @@ export function inferStatus(parse?: ParsingStatus, value?: ValueClass): Expressi
|
||||||
|
|
||||||
export function LoadRSFormData(schema: IRSFormData): IRSForm {
|
export function LoadRSFormData(schema: IRSFormData): IRSForm {
|
||||||
const result = schema as IRSForm
|
const result = schema as IRSForm
|
||||||
|
result.graph = new Graph;
|
||||||
if (!result.items) {
|
if (!result.items) {
|
||||||
result.stats = {
|
result.stats = {
|
||||||
count_all: 0,
|
count_all: 0,
|
||||||
|
@ -254,35 +262,45 @@ export function LoadRSFormData(schema: IRSFormData): IRSForm {
|
||||||
return result;
|
return result;
|
||||||
}
|
}
|
||||||
result.stats = {
|
result.stats = {
|
||||||
count_all: schema.items.length || 0,
|
count_all: result.items.length || 0,
|
||||||
count_errors: schema.items.reduce(
|
count_errors: result.items.reduce(
|
||||||
(sum, cst) => sum + (cst.parse?.status === ParsingStatus.INCORRECT ? 1 : 0) || 0, 0),
|
(sum, cst) => sum + (cst.parse?.status === ParsingStatus.INCORRECT ? 1 : 0) || 0, 0),
|
||||||
count_property: schema.items.reduce(
|
count_property: result.items.reduce(
|
||||||
(sum, cst) => sum + (cst.parse?.valueClass === ValueClass.PROPERTY ? 1 : 0) || 0, 0),
|
(sum, cst) => sum + (cst.parse?.valueClass === ValueClass.PROPERTY ? 1 : 0) || 0, 0),
|
||||||
count_incalc: schema.items.reduce(
|
count_incalc: result.items.reduce(
|
||||||
(sum, cst) => sum +
|
(sum, cst) => sum +
|
||||||
((cst.parse?.status === ParsingStatus.VERIFIED && cst.parse?.valueClass === ValueClass.INVALID) ? 1 : 0) || 0, 0),
|
((cst.parse?.status === ParsingStatus.VERIFIED && cst.parse?.valueClass === ValueClass.INVALID) ? 1 : 0) || 0, 0),
|
||||||
|
|
||||||
count_termin: schema.items.reduce(
|
count_termin: result.items.reduce(
|
||||||
(sum, cst) => (sum + (cst.term?.raw ? 1 : 0) || 0), 0),
|
(sum, cst) => (sum + (cst.term?.raw ? 1 : 0) || 0), 0),
|
||||||
|
|
||||||
count_base: schema.items.reduce(
|
count_base: result.items.reduce(
|
||||||
(sum, cst) => sum + (cst.cstType === CstType.BASE ? 1 : 0), 0),
|
(sum, cst) => sum + (cst.cstType === CstType.BASE ? 1 : 0), 0),
|
||||||
count_constant: schema.items?.reduce(
|
count_constant: result.items?.reduce(
|
||||||
(sum, cst) => sum + (cst.cstType === CstType.CONSTANT ? 1 : 0), 0),
|
(sum, cst) => sum + (cst.cstType === CstType.CONSTANT ? 1 : 0), 0),
|
||||||
count_structured: schema.items?.reduce(
|
count_structured: result.items?.reduce(
|
||||||
(sum, cst) => sum + (cst.cstType === CstType.STRUCTURED ? 1 : 0), 0),
|
(sum, cst) => sum + (cst.cstType === CstType.STRUCTURED ? 1 : 0), 0),
|
||||||
count_axiom: schema.items?.reduce(
|
count_axiom: result.items?.reduce(
|
||||||
(sum, cst) => sum + (cst.cstType === CstType.AXIOM ? 1 : 0), 0),
|
(sum, cst) => sum + (cst.cstType === CstType.AXIOM ? 1 : 0), 0),
|
||||||
count_term: schema.items.reduce(
|
count_term: result.items.reduce(
|
||||||
(sum, cst) => sum + (cst.cstType === CstType.TERM ? 1 : 0), 0),
|
(sum, cst) => sum + (cst.cstType === CstType.TERM ? 1 : 0), 0),
|
||||||
count_function: schema.items.reduce(
|
count_function: result.items.reduce(
|
||||||
(sum, cst) => sum + (cst.cstType === CstType.FUNCTION ? 1 : 0), 0),
|
(sum, cst) => sum + (cst.cstType === CstType.FUNCTION ? 1 : 0), 0),
|
||||||
count_predicate: schema.items.reduce(
|
count_predicate: result.items.reduce(
|
||||||
(sum, cst) => sum + (cst.cstType === CstType.PREDICATE ? 1 : 0), 0),
|
(sum, cst) => sum + (cst.cstType === CstType.PREDICATE ? 1 : 0), 0),
|
||||||
count_theorem: schema.items.reduce(
|
count_theorem: result.items.reduce(
|
||||||
(sum, cst) => sum + (cst.cstType === CstType.THEOREM ? 1 : 0), 0)
|
(sum, cst) => sum + (cst.cstType === CstType.THEOREM ? 1 : 0), 0)
|
||||||
}
|
}
|
||||||
|
result.items.forEach(cst => {
|
||||||
|
result.graph.addNode(cst.id);
|
||||||
|
const dependencies = extractGlobals(cst.definition.formal);
|
||||||
|
dependencies.forEach(value => {
|
||||||
|
const destination = schema.items.find(cst => cst.alias === value)
|
||||||
|
if (destination) {
|
||||||
|
result.graph.addEdge(cst.id, destination.id);
|
||||||
|
}
|
||||||
|
});
|
||||||
|
});
|
||||||
return result;
|
return result;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -269,10 +269,6 @@ export function getStatusInfo(status?: ExpressionStatus): IStatusInfo {
|
||||||
};
|
};
|
||||||
}
|
}
|
||||||
|
|
||||||
export function extractGlobals(expression: string): Set<string> {
|
|
||||||
return new Set(expression.match(/[XCSADFPT]\d+/g) ?? []);
|
|
||||||
}
|
|
||||||
|
|
||||||
export function createAliasFor(type: CstType, schema: IRSForm): string {
|
export function createAliasFor(type: CstType, schema: IRSForm): string {
|
||||||
const prefix = getCstTypePrefix(type);
|
const prefix = getCstTypePrefix(type);
|
||||||
if (!schema.items || schema.items.length <= 0) {
|
if (!schema.items || schema.items.length <= 0) {
|
||||||
|
|
Loading…
Reference in New Issue
Block a user