loading machines visually now downs

web/root/src/automata.ts

@@ -0,0 +1,171 @@
+export type Machine = Fa | Pda | Tm;
+
+export function machine_from_json(json: string): Machine {
+  const machine: Machine = JSON.parse(json);
+  machine.states = new Map(Object.entries(machine.states));
+
+  if (machine.alphabet) {
+    machine.alphabet = new Map(Object.entries(machine.alphabet));
+  }
+  if (machine.final_states) {
+    machine.final_states = new Map(Object.entries(machine.final_states));
+  }
+
+  // deno-lint-ignore no-explicit-any
+  const transitions = machine.transitions as any as [any, any];
+  machine.transitions = new Map();
+  for (const [key, value] of transitions) {
+    machine.transitions.set(key, value);
+  }
+  machine.edges = new Map();
+
+  switch (machine.type) {
+    case "fa":
+      {
+        for (const [from, tos] of machine.transitions) {
+          for (const to of tos) {
+            const edge = from.state + "#" + to.state;
+            if (!machine.edges.has(edge)) machine.edges.set(edge, []);
+            machine.edges.get(edge)?.push({
+              repr: from.letter?from.letter:"ε",
+              function: to.function,
+              transition: to.transition,
+            });
+          }
+        }
+      }
+      break;
+    case "pda":
+      {
+        machine.symbols = new Map(Object.entries(machine.symbols));
+        for (const [from, tos] of machine.transitions) {
+          for (const to of tos) {
+            const edge = from.state + "#" + to.state;
+            if (!machine.edges.has(edge)) machine.edges.set(edge, []);
+            machine.edges.get(edge)?.push({
+              repr: (from.letter?from.letter:"ε")+","+from.symbol+"->["+to.stack+"]",
+              function: to.function,
+              transition: to.transition,
+            });
+          }
+        }
+      }
+      break;
+    case "tm":
+      {
+        machine.symbols = new Map(Object.entries(machine.symbols));
+        for (const [from, tos] of machine.transitions) {
+          for (const to of tos) {
+            const edge = from.state + "#" + to.state;
+            if (!machine.edges.has(edge)) machine.edges.set(edge, []);
+            machine.edges.get(edge)?.push({
+              repr: from.symbol+"->"+to.symbol+","+to.direction,
+              function: to.function,
+              transition: to.transition,
+            });
+          }
+        }
+      }
+      break;
+  }
+  return machine;
+}
+
+export type State = string;
+export type Symbol = string;
+export type Letter = string;
+
+export type Span = [number, number];
+
+export type StateInfo = { definition: Span };
+export type LetterInfo = { definition: Span };
+export type SymbolInfo = { definition: Span };
+
+export type FaTransFrom = {
+  state: State;
+  letter: Letter|null;
+};
+
+export type FaTransTo = {
+  state: State;
+
+  transition: Span;
+  function: Span;
+};
+
+export type Edge = {
+  repr: string;
+  function: Span;
+  transition: Span;
+};
+
+export type Fa = {
+  type: "fa";
+
+  initial_state: State;
+  states: Map<State, StateInfo>;
+  alphabet: Map<Letter, LetterInfo>;
+  final_states: Map<State, StateInfo>;
+
+  transitions: Map<FaTransFrom, FaTransTo[]>;
+
+  edges: Map<string, Edge[]>;
+};
+
+export type PdaTransFrom = {
+  state: State;
+  letter: Letter|null;
+  symbol: Symbol;
+};
+
+export type PdaTransTo = {
+  state: State;
+  stack: Symbol[];
+
+  transition: Span;
+  function: Span;
+};
+
+export type Pda = {
+  type: "pda";
+
+  initial_state: State;
+  initial_stack: Symbol;
+  states: Map<State, StateInfo>;
+  symbols: Map<Symbol, SymbolInfo>;
+  alphabet: Map<Letter, LetterInfo>;
+  final_states: Map<State, StateInfo> | null;
+
+  transitions: Map<PdaTransFrom, PdaTransTo[]>;
+
+  edges: Map<string, Edge[]>;
+};
+
+export type TmTransFrom = {
+  state: State;
+  symbol: Symbol;
+};
+
+export type TmTransTo = {
+  state: State;
+  symbol: Symbol;
+  direction: "L" | "R" | "N";
+
+  transition: Span;
+  function: Span;
+};
+
+export type Tm = {
+  type: "tm";
+
+  initial_state: State;
+  initial_tape: Symbol;
+  states: Map<State, StateInfo>;
+  symbols: Map<Symbol, SymbolInfo>;
+  alphabet: Map<Letter, LetterInfo>;
+  final_states: Map<State, StateInfo>;
+
+  transitions: Map<TmTransFrom, TmTransTo[]>;
+
+  edges: Map<string, Edge[]>;
+};

web/root/src/editor.ts

@@ -21,6 +21,7 @@ import wasm from "./wasm.ts"
 import { terminalPlugin } from "./terminal.ts";
 
 import { setAutomaton } from "./visualizer.ts";
+import { machine_from_json } from "./automata.ts";
 
 
 function tokenize(text: string) {
@@ -79,7 +80,7 @@ function buildAnalysis(text: string, doc: Text) {
 
   if (graph){
     try{
-      setAutomaton(JSON.parse(graph))
+      setAutomaton(machine_from_json(graph))
     }catch(e){
       console.log(e);
     }

web/root/src/visualizer.ts

@@ -3,11 +3,11 @@
 // deno-lint-ignore no-import-prefix
 import * as vis from "npm:vis-network/standalone";
 import { StateEffect } from "npm:@codemirror/state";
+import { Machine } from "./automata.ts";
 
 export const nodes = new vis.DataSet<vis.Node>();
 export const edges = new vis.DataSet<vis.Edge>();
 
-
 type Color = string;
 type GraphTheme = {
   bg_0: Color;
@@ -25,8 +25,8 @@ type GraphTheme = {
   edge_hover: Color;
   edge_active: Color;
 
-  edge_font_size: number,
-  node_font_size: number,
+  edge_font_size: number;
+  node_font_size: number;
 };
 
 let _graphTheme: GraphTheme | null = null;
@@ -55,11 +55,11 @@ function getGraphTheme(): GraphTheme {
     node_anchor: cssVar("--graph-node-anchor"),
     node_border: cssVar("--graph-node-border"),
     current_node_border: cssVar("--graph-current-node-border"),
-    
+
     edge: cssVar("--graph-edge"),
     edge_hover: cssVar("--graph-edge-hover"),
     edge_active: cssVar("--graph-edge-active"),
-    
+
     edge_font_size: Number(cssVar("--graph-edge-font-size")),
     node_font_size: Number(cssVar("--graph-node-font-size")),
   };
@@ -77,21 +77,21 @@ export function updateGraphTheme() {
         color: gt.fg_0,
         bold: {
           color: gt.fg_1,
-          mod: ''
+          mod: "",
         },
       },
     },
     edges: {
       labelHighlightBold: true,
-      font: { 
-        align: "top", 
+      font: {
+        align: "top",
         size: gt.edge_font_size,
         color: gt.fg_0,
         strokeColor: gt.bg_0,
         bold: {
           color: gt.fg_1,
           size: gt.edge_font_size,
-          mod: ''
+          mod: "",
         },
       },
       color: {
@@ -101,43 +101,39 @@ export function updateGraphTheme() {
       },
       shadow: {
         enabled: false,
-      }
+      },
     },
   });
 }
 
-
-type StateId = string;
-type GraphDef = {
-  initial: StateId;
-  final_states: Set<StateId>;
-  states: Set<StateId>;
-  transitions: Record<string, string>;
-};
-
-let automaton: GraphDef = {
-  initial: "",
-  final_states: new Set(),
-  states: new Set(),
-  transitions: {},
+let automaton: Machine = {
+  type: "fa",
+  alphabet: new Map(),
+  final_states: new Map(),
+  initial_state: "",
+  states: new Map(),
+  transitions: new Map(),
+  edges: new Map(),
 };
 
 export function clearAutomaton() {
-  setAutomaton({
-    initial: "",
-    final_states: new Set(),
-    states: new Set(),
-    transitions: {},
-  });
+  automaton = {
+    type: "fa",
+    alphabet: new Map(),
+    final_states: new Map(),
+    initial_state: "",
+    states: new Map(),
+    transitions: new Map(),
+    edges: new Map(),
+  };
 }
 
-export function setAutomaton(auto: GraphDef) {
+export function setAutomaton(auto: Machine) {
   console.log(auto);
   automaton = auto;
-  automaton.final_states = new Set(automaton.final_states)
-  automaton.states = new Set(automaton.states)
+
   // Populate nodes
-  for (const state of automaton.states) {
+  for (const state of automaton.states.keys()) {
     if (nodes.get(state)) {
       nodes.update({
         id: state,
@@ -151,40 +147,41 @@ export function setAutomaton(auto: GraphDef) {
     }
   }
 
-  // Populate edges
-  for (const [k, v] of Object.entries(automaton.transitions)) {
-    const to_from = k.split("#");
+  // // Populate edges
+  for (const [edge_id, transitions] of auto.edges) {
+    const to_from = edge_id.split("#");
     const font = {
-      vadjust: -getGraphTheme().edge_font_size*Math.floor(((v.match(/\n/g) || '').length + 1)/2)
-    };
-    if (edges.get(k)) {
+      vadjust: -getGraphTheme().edge_font_size *
+        Math.floor(transitions.length / 2),
+    };    
+    if (edges.get(edge_id)) {
       edges.update({
-        id: k,
+        id: edge_id,
         font,
         from: to_from[0],
         to: to_from[1],
-        label: v,
+        label: transitions.map(i => i.repr).join("\n"),
       });
     } else {
       edges.add({
-        id: k,
+        id: edge_id,
         font,
         from: to_from[0],
         to: to_from[1],
-        label: v,
+        label: transitions.map(i => i.repr).join("\n"),
       });
     }
   }
 
-  for (const edge_id of edges.getIds()){
-    if (auto.transitions[edge_id as string] === undefined){
-      edges.remove(edge_id)
+  for (const edge_id of edges.getIds()) {
+    if (!auto.edges.has(edge_id as string)) {
+      edges.remove(edge_id);
     }
   }
 
-  for (const node_id of nodes.getIds()){
-    if (!auto.states.has(node_id as string)){
-      nodes.remove(node_id)
+  for (const node_id of nodes.getIds()) {
+    if (!auto.states.has(node_id as string)) {
+      nodes.remove(node_id);
     }
   }
 }
@@ -278,12 +275,13 @@ function renderNode({
 }: any) {
   return {
     drawNode() {
-
       const t = getGraphTheme();
       const r = Math.max(14, style?.size ?? 18);
 
-      const isInitial = automaton.initial === id;
-      const isFinal = automaton.final_states.has(id);
+      const isInitial = automaton.initial_state === id;
+      const isFinal = automaton.final_states
+        ? automaton.final_states.has(id)
+        : false;
       const isActive = false;
 
       const fill = selected ? t.bg_2 : hover ? t.bg_1 : t.bg_0;