interface update

Author: NeuralCoder3

package.json

@@ -3,6 +3,13 @@
   "version": "0.1.0",
   "private": true,
   "dependencies": {
+    "@emotion/react": "^11.10.6",
+    "@emotion/styled": "^11.10.6",
+    "@fortawesome/fontawesome-svg-core": "^6.4.0",
+    "@fortawesome/free-solid-svg-icons": "^6.4.0",
+    "@fortawesome/react-fontawesome": "^0.2.0",
+    "@mui/icons-material": "^5.11.16",
+    "@mui/material": "^5.12.0",
     "@testing-library/jest-dom": "^5.16.5",
     "@testing-library/react": "^13.4.0",
     "@testing-library/user-event": "^13.5.0",
@@ -16,6 +23,8 @@
     "react-draggable": "^4.4.5",
     "react-mathjax": "^1.0.1",
     "react-scripts": "5.0.1",
+    "react-select": "^5.7.2",
+    "react-zoom-pan-pinch": "^3.0.7",
     "typescript": "^4.9.5",
     "web-vitals": "^2.1.4"
   },

src/App.css

@@ -32,7 +32,36 @@
   from {
     transform: rotate(0deg);
   }
+
   to {
     transform: rotate(360deg);
   }
 }
+
+.InferenceArea {
+  text-align: center;
+  align-items: center;
+  justify-content: center;
+  display: flex;
+  width: 100%;
+  height: 100%;
+}
+
+
+.App,
+#root,
+body,
+html {
+  height: 100%;
+  width: 100%;
+}
+
+.main {
+  display: flex;
+  flex-direction: row;
+  position: absolute;
+  top: 30%;
+  left: 30%;
+  /* transform: translate(-50%, -50%); */
+  right: 50%;
+}

src/App.tsx

@@ -1,13 +1,10 @@
 import './App.css';
-import { TreeWrapper } from './components/TreeWrapper';
-import { calculus as color_calculus } from './logic/calculi/color';
-
-const calculus = color_calculus;
+import { InferenceInterface } from './components/InferenceInterface';
 
 function App() {
   return (
     <div className="App">
-      <TreeWrapper calculus={calculus} init={"Brown"} />
+      <InferenceInterface />
     </div>
   );
 }

src/components/InferenceInterface.tsx

@@ -0,0 +1,78 @@
+import { TreeWrapper } from '../components/TreeWrapper';
+// import { calculus as color_calculus } from './logic/calculi/color';
+import * as color from "../logic/calculi/color";
+import * as type_conversion from "../logic/calculi/type_conversion";
+import * as expr_ty from "../logic/calculi/static_semantics_expr";
+import * as stmt_ty from "../logic/calculi/static_semantics_stmt";
+import * as hoare from "../logic/calculi/hoare";
+import { StringDispatchRenderer } from '../logic/syntax/renderer';
+import React, { useContext } from 'react';
+import { TransformComponent, TransformWrapper } from 'react-zoom-pan-pinch';
+
+const calculus = color.calculus;
+const renderer = new StringDispatchRenderer();
+const goal = "Brown";
+
+// const calculus = expr_ty.calculus;
+// const type_renderer = new StringDispatchRenderer()
+//   .registerAppDispatcher(expr_ty.app_renderer).registerConstDispatcher(expr_ty.const_renderer);
+// const goal = "typed(Γ, BinOp(Minus, BinOp(Plus,Indir(x),y), 1), ?type)";
+
+export function InferenceInterface() {
+
+  let initial_scale = 1.0;
+
+  if (window.location.search) {
+    const urlParams = new URLSearchParams(window.location.search);
+    const scale = urlParams.get('scale');
+    if (scale) {
+      initial_scale = parseFloat(scale);
+    }
+  }
+
+  // const context = useContext(AppContext)
+  const [isMoveable, setIsMoveable] = React.useState<boolean>(false);
+
+  const onDrag = () => {
+    setIsMoveable(true)
+    //etc
+  }
+  const onStop = () => {
+    setIsMoveable(false)
+    //etc 
+  }
+
+  return (
+
+    <TransformWrapper
+      initialScale={initial_scale}
+      disabled={isMoveable}
+      minScale={.25}
+      maxScale={1.5}
+      limitToBounds={false}
+      // onPanning={updateXarrow}
+      // onZoom={updateXarrow}
+      pinch={{ step: 5 }}
+    >
+
+      <TransformComponent
+        contentClass='main'
+        wrapperStyle={{
+          height: '100vh', width: '100vw'
+        }}>
+        {/* <div> */}
+        <div className='InferenceArea'>
+          <TreeWrapper
+            init={goal}
+            calculus={calculus} renderer={renderer}
+            onDrag={onDrag} onStop={onStop}
+          // onClick={onInteracting} onEndClick={onInteractingEnd}
+          // onClick={onDrag} onEndClick={onStop}
+          />
+        </div>
+        {/* </div> */}
+
+      </TransformComponent>
+    </TransformWrapper >
+  );
+}

src/components/Tree.tsx

@@ -1,15 +1,19 @@
 import { calculus, ruleByName, applyRuleFull } from "../logic/inference/inference_rules";
+import { parse } from "../logic/syntax/parser";
 import { StringDispatchRenderer } from "../logic/syntax/renderer";
 import { Expr, getVars } from "../logic/syntax/syntactic_logic";
-import { Subst } from "../logic/unification/unification";
+import { Subst, applySubst } from "../logic/unification/unification";
 
-export interface Tree {
-  conclusion: string;
-  assumptions: Tree[];
+export interface GenericTree<T> {
+  conclusion: T;
+  assumptions: GenericTree<T>[];
   rule?: string;
 };
 
-export function goal_tree(conclusion: string): Tree {
+export type Tree = GenericTree<Expr>;
+export type StringTree = GenericTree<string>;
+
+export function goal_tree(conclusion: Expr): Tree {
   return {
     conclusion: conclusion,
     assumptions: [],
@@ -39,3 +43,40 @@ export function applyNamedRule(calc: calculus, name: string, goal: Expr): [Expr[
   }
   return [premises, goal_subst];
 }
+
+export function applyTreeSubst(tree: Tree, subst: Subst): Tree {
+  return {
+    conclusion: applySubst(subst, tree.conclusion),
+    assumptions: tree.assumptions.map(a => applyTreeSubst(a, subst)),
+    rule: tree.rule,
+  };
+}
+
+// deep copy of tree
+export function copyTree(tree: Tree): Tree {
+  return {
+    conclusion: tree.conclusion,
+    assumptions: tree.assumptions.map(a => copyTree(a)),
+    rule: tree.rule,
+  };
+}
+
+export function isClosed(tree: Tree): boolean {
+  return tree.rule !== undefined && tree.assumptions.every(a => isClosed(a));
+}
+
+export function stringTreeToTree(tree: StringTree): Tree {
+  return {
+    conclusion: parse(tree.conclusion),
+    assumptions: tree.assumptions.map(a => stringTreeToTree(a)),
+    rule: tree.rule,
+  };
+}
+
+export function treeToStringTree(tree: Tree): StringTree {
+  return {
+    conclusion: debugRenderer.render(tree.conclusion),
+    assumptions: tree.assumptions.map(a => treeToStringTree(a)),
+    rule: tree.rule,
+  };
+}