Spaces:

dx2102
/

lean-expr-tree

Sleeping

App Files Files Community

dx2102 commited on Aug 19

Commit

3e53e47

•

1 Parent(s): d468aa0

Upload 4 files

Browse files

Files changed (5) hide show

.gitattributes +1 -0
Dockerfile +6 -0
exported.txt +3 -0
server.py +52 -0
website.html +105 -0

.gitattributes CHANGED Viewed

@@ -33,3 +33,4 @@ saved_model/**/* filter=lfs diff=lfs merge=lfs -text
 *.zip filter=lfs diff=lfs merge=lfs -text
 *.zst filter=lfs diff=lfs merge=lfs -text
 *tfevents* filter=lfs diff=lfs merge=lfs -text

 *.zip filter=lfs diff=lfs merge=lfs -text
 *.zst filter=lfs diff=lfs merge=lfs -text
 *tfevents* filter=lfs diff=lfs merge=lfs -text
+exported.txt filter=lfs diff=lfs merge=lfs -text

Dockerfile ADDED Viewed

	@@ -0,0 +1,6 @@

+FROM python:3.9
+WORKDIR /app
+COPY --chown=user . /app
+RUN pip install fastapi uvicorn
+CMD ["uvicorn", "server:app", "--host", "0.0.0.0", "--port", "7860"]

exported.txt ADDED Viewed

	@@ -0,0 +1,3 @@

+version https://git-lfs.github.com/spec/v1
+oid sha256:d9799396336c9763476c49cae9a3b02feceae9b76941e0baac3930bb52477036
+size 3571992971

server.py ADDED Viewed

	@@ -0,0 +1,52 @@

+from fastapi import FastAPI, Query
+from fastapi.responses import HTMLResponse, JSONResponse
+from fastapi.staticfiles import StaticFiles
+import json
+from dataclasses import dataclass, asdict
+'''
+cd python/lean-expr-tree
+uvicorn server:app --reload
+'''
+app = FastAPI()
+# return website.html when accessing root
+@app.get("/")
+async def get_root():
+    return HTMLResponse(content=open('website.html', 'r').read())
+@dataclass
+class Decl:
+    file: str
+    name: str
+    typ: str
+    docs: str
+    ast: str
+def parse_exported_file():
+    decls = []
+    print('Reading exported.txt')
+    lines = open('exported.txt', 'r').read() # 1000000)
+    print('Splitting exported.txt')
+    lines = lines.split('----ast----\n')[1:]
+    print('Parsing exported.txt')
+    for block in lines:
+        parts = block.split('--ast--\n')[:-1]
+        if len(parts) != 5:
+            continue
+        file, name, typ, docs, ast = parts
+        decls.append(Decl(file, name, typ, docs, ast))
+    print('Finished parsing exported.txt')
+    return decls
+decls = parse_exported_file()
+@app.get("/search")
+async def search(query: str = Query(...)):
+    matched = [decl for decl in decls if query in decl.name]
+    matched = sorted(matched, key=lambda decl: decl.name)
+    matched_results = [asdict(decl) for decl in matched]
+    return JSONResponse(content=matched_results)

website.html ADDED Viewed

	@@ -0,0 +1,105 @@

+<!DOCTYPE html>
+<html lang="en">
+<head>
+    <meta charset="UTF-8">
+    <meta name="viewport" content="width=device-width, initial-scale=1.0">
+    <title>Syntax Tree Visualization</title>
+    <script src="https://cdn.tailwindcss.com"></script>
+</head>
+<body class="bg-gray-50 text-gray-900">
+    <div class="container mx-auto mt-10">
+        <h1 class="text-4xl font-bold mb-5">Syntax Tree Visualization</h1>
+        <form class="mb-5" onsubmit="event.preventDefault(); search();">
+            <input id="search-input" type="text" value="Lean" class="w-full p-2 border border-gray-300 rounded-md">
+            <button class="mt-2 bg-blue-500 text-white px-4 py-2 rounded-md">Search</button>
+        </form>
+        <div id="results" class="mb-5"></div>
+        <canvas id="tree-canvas" class="mx-auto border border-gray-300 rounded-md"></canvas>
+    </div>
+    <script>
+        async function search() {
+            console.log('search');
+            const query = document.getElementById('search-input').value;
+            const response = await fetch(`/search?query=${query}`);
+            const data = await response.json();
+            console.log(data);
+            const resultsDiv = document.getElementById('results');
+            resultsDiv.innerHTML = '';
+            data.forEach((result, index) => {
+                const button = document.createElement('button');
+                button.innerText = result.name;
+                button.className = 'block w-full text-left p-2 bg-gray-200 my-2 rounded-md';
+                if (data[index].ast !== 'expression tree does not exist\n') {
+                    data[index].ast = JSON.parse(data[index].ast);
+                    console.log(data[index].ast);
+                }
+                button.onclick = () => visualizeTree(data[index].ast);
+                resultsDiv.appendChild(button);
+            });
+            visualizeTree(data[0].ast);
+        }
+        const canvas = document.getElementById('tree-canvas');
+        const ctx = canvas.getContext('2d');
+        ctx.font = '100px Arial';
+        canvas.width = Math.floor(window.innerWidth * 0.8) * 2;
+        canvas.height = Math.floor(window.innerHeight * 0.8) * 2;
+        canvas.style.width = Math.floor(window.innerWidth * 0.8) + 'px';
+        canvas.style.height = Math.floor(window.innerHeight * 0.8) + 'px';
+        function visualizeTree(tree) {
+            ctx.fillStyle = 'white';
+            ctx.clearRect(0, 0, canvas.width, canvas.height);
+            const width = drawNode(tree, 10, 10);
+            if (width > canvas.width) {
+                canvas.width = width;
+                canvas.style.width = width / 2 + 'px';
+            }
+            // draw again
+            drawNode(tree, 10, 10);
+        }
+        const sizeX = 60;
+        const sizeY = 30;
+        function drawNode(node, x, y) {
+            // This is recursive. Returns the width of the node.
+            // if node is still an object, it is a non-leaf node
+            const isLeaf = typeof node !== 'object';
+            if (isLeaf) {
+                // draw leaf node simply as text
+                ctx.fillStyle = 'rgba(256, 0, 0, 0.1)';
+                ctx.fillRect(x, y, sizeX, sizeY);
+                ctx.fillStyle = 'black';
+                ctx.font = '20px Arial';
+                ctx.fillText(node, x, y + sizeY);
+                return sizeX;
+            }
+            // draw non-leaf node as a black square
+            ctx.fillStyle = 'rgba(0, 0, 0, 0.1)';
+            ctx.fillRect(x, y, sizeX, sizeY);
+            ctx.fillStyle = 'black';
+            ctx.font = '20px Arial';
+            ctx.fillText(node.kind, x, y + sizeY);
+            // draw children
+            const childY = y + sizeY;
+            let childX = x;
+            let totalWidth = 0;
+            node.children.forEach((child, index) => {
+                let width = drawNode(child, childX, childY);
+                childX += width;
+                totalWidth += width;
+            });
+            return totalWidth;
+        }
+    </script>
+</body>
+</html>