server.py

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()
    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)[:10]
    matched_results = [asdict(decl) for decl in matched]
    return JSONResponse(content=matched_results)