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)