Skip to content

Commit

Permalink
refactor: fold shared logic back in to core package
Browse files Browse the repository at this point in the history
  • Loading branch information
jamesdabbs committed Jun 4, 2024
1 parent 594be10 commit ba49e7f
Show file tree
Hide file tree
Showing 23 changed files with 182 additions and 166 deletions.
2 changes: 1 addition & 1 deletion packages/compile/package.json
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@
"glob": "^8.1.0",
"js-yaml": "^4.1.0",
"yaml-front-matter": "^4.1.1",
"zod": "^3.22.4"
"zod": "^3.23.8"
},
"devDependencies": {
"@types/cors": "^2.8.17",
Expand Down
12 changes: 12 additions & 0 deletions packages/core/bin/build
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
#!/bin/bash
set -exo pipefail

# VSCode extensions can only use CommonJS modules (for now), but we want to
# continue using our standard Vite/ESM build process elsewhere. This builds
# both versions, corresponding to `package.json`'s `exports` field.

tsc --module es2022 --outDir dist/esm/
echo '{"type": "module"}' > dist/esm/package.json

tsc --module commonjs --outDir dist/cjs/
echo '{"type": "commonjs"}' > dist/cjs/package.json
10 changes: 7 additions & 3 deletions packages/core/package.json
Original file line number Diff line number Diff line change
Expand Up @@ -14,15 +14,19 @@
},
"license": "MIT",
"author": "James Dabbs <james.dabbs@gmail.com> (https://jdabbs.com)",
"main": "./dist/esm/index.js",
"types": "./dist/types/index.d.ts",
"exports": {
"types": "./dist/types/index.d.ts",
"require": "./dist/cjs/index.js",
"import": "./dist/esm/index.js"
},
"repository": {
"type": "git",
"url": "git+https://github.com/pi-base/web.git"
},
"scripts": {
"build:peg": "peggy --plugin ./node_modules/ts-pegjs/dist/tspegjs -o src/Formula/Grammar.ts --cache src/Formula/Grammar.pegjs",
"build": "pnpm build:peg && tsc",
"build": "pnpm build:peg && ./bin/build",
"dev": "pnpm build:peg && tsc --watch",
"test": "vitest run",
"test:cov": "vitest run --coverage",
Expand All @@ -40,7 +44,7 @@
"unified": "^10.1.2",
"unist-util-is": "^5.2.1",
"unist-util-visit": "^4.1.2",
"zod": "^3.22.4"
"zod": "^3.23.8"
},
"devDependencies": {
"@types/debug": "^4.1.12",
Expand Down
6 changes: 1 addition & 5 deletions packages/core/src/Bundle.ts
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,7 @@ import { Space, spaceSchema } from './Space.js'
import { Theorem, theoremSchema } from './Theorem.js'
import { Trait, traitSchema } from './Trait.js'

export const defaultHost = import.meta.env?.VITE_PUBLIC_DATA_URL
? import.meta.env.VITE_PUBLIC_DATA_URL
: import.meta.env?.DEV
? 'http://localhost:3141'
: 'https://pi-base-bundles.s3.us-east-2.amazonaws.com'
export const defaultHost = 'https://pi-base-bundles.s3.us-east-2.amazonaws.com'

export type Version = {
ref: string
Expand Down
36 changes: 36 additions & 0 deletions packages/core/src/Id.ts
Original file line number Diff line number Diff line change
Expand Up @@ -54,3 +54,39 @@ export function toInt(id: string): number {

return tagged.id
}

// TODO: these were extracted from other parallel-but-divergent implementations
// and should be unified.

type Pad = '' | '0' | '00' | '000' | '0000' | '00000' | '00000'
type XId<Prefix extends string> = `${Prefix}${Pad}${number}`

export type SId = XId<'S'>
export type PId = XId<'P'>
export type TId = XId<'T'>
export type SPId = [SId, PId]
export type EntityId = SId | PId | TId | SPId

export function isSpaceId(token: string): token is SId {
return token.match(/^S\d{1,6}$/) !== null
}

export function isPropertyId(token: string): token is PId {
return token.match(/^P\d{1,6}$/) !== null
}

export function isTheoremId(token: string): token is SId {
return token.match(/^T\d{1,6}$/) !== null
}

export function isTraitId(pair: [string, string]): pair is SPId {
return isSpaceId(pair[0]) && isPropertyId(pair[1])
}

export const idExp = /[PST]\d{1,6}/g

export function normalizeId(id: SId): SId
export function normalizeId(id: PId): PId
export function normalizeId(id: string) {
return `${id[0]}${id.slice(1).padStart(6, '0')}`
}
11 changes: 11 additions & 0 deletions packages/core/src/Property.ts
Original file line number Diff line number Diff line change
@@ -1,5 +1,15 @@
import { z } from 'zod'
import { recordSchema } from './Record.js'
import { refSchema } from './Ref.js'

export const propertyPageSchema = z.object({
uid: z.string(),
name: z.string(),
aliases: z.array(z.string()).optional(),
counterexamples_id: z.number().nullable().optional(),
refs: z.array(refSchema).optional(),
description: z.string(),
})

export const propertySchema = z.intersection(
z.object({
Expand All @@ -10,3 +20,4 @@ export const propertySchema = z.intersection(
)

export type Property = z.infer<typeof propertySchema>
export type PropertyPage = z.infer<typeof propertyPageSchema>
11 changes: 11 additions & 0 deletions packages/core/src/Space.ts
Original file line number Diff line number Diff line change
@@ -1,5 +1,15 @@
import { z } from 'zod'
import { recordSchema } from './Record.js'
import { refSchema } from './Ref.js'

export const spacePageSchema = z.object({
uid: z.string(),
name: z.string(),
aliases: z.array(z.string()).optional(),
counterexamples_id: z.number().nullable().optional(),
refs: z.array(refSchema).optional(),
description: z.string(),
})

export const spaceSchema = z.intersection(
z.object({
Expand All @@ -11,3 +21,4 @@ export const spaceSchema = z.intersection(
)

export type Space = z.infer<typeof spaceSchema>
export type SpacePage = z.infer<typeof spacePageSchema>
10 changes: 6 additions & 4 deletions packages/core/src/index.ts
Original file line number Diff line number Diff line change
@@ -1,20 +1,20 @@
import { formulaSchema } from './Formula.js'
import { propertySchema } from './Property.js'
import { spaceSchema } from './Space.js'
import { propertySchema, propertyPageSchema } from './Property.js'
import { spaceSchema, spacePageSchema } from './Space.js'
import { theoremSchema } from './Theorem.js'
import { traitSchema } from './Trait.js'

export { type Bundle } from './Bundle.js'
export { type Formula, type And, type Atom, type Or } from './Formula.js'
export { parser } from './Parser.js'
export { type Property } from './Property.js'
export { type Property, PropertyPage } from './Property.js'
export {
ImplicationIndex,
deduceTraits,
disproveFormula,
proveTheorem,
} from './Logic/index.js'
export { type Space } from './Space.js'
export { type Space, SpacePage } from './Space.js'
export { type Theorem } from './Theorem.js'
export { type Trait } from './Trait.js'
export { type Version } from './Bundle.js'
Expand All @@ -29,7 +29,9 @@ export * as TestUtils from './testUtils.js'
export const schemas = {
formula: formulaSchema,
property: propertySchema,
propertyPage: propertyPageSchema,
space: spaceSchema,
spacePage: spacePageSchema,
theorem: theoremSchema,
trait: traitSchema,
}
1 change: 1 addition & 0 deletions packages/vscode/package.json
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,7 @@
"npm-run-all": "^4.1.5"
},
"dependencies": {
"@pi-base/core": "workspace:*",
"debug": "^4.3.4",
"js-yaml": "^4.1.0",
"zod": "^3.23.8"
Expand Down
38 changes: 27 additions & 11 deletions packages/vscode/src/extension.ts
Original file line number Diff line number Diff line change
Expand Up @@ -6,23 +6,29 @@ import { EntityIdLinkProvider } from './providers/EntityIdLinkProvider'
import { ExternalLinkProvider } from './providers/ExternalLinkProvider'
import { setupDecorationProvider } from './providers/decorationProvider'

export function activate(context: vscode.ExtensionContext) {
findRootFolder().then(uri => {
if (uri) {
setup(context, uri)
} else {
console.log(
'No data folder found in workspace. Skipping π-base initialization.',
)
}
})
}

export function deactivate() {}

// TODO: can we target these more narrowly? Notebook type?
// Note that we need to match file:// and also vscode-vfs:// schemes to work on github.dev
const selector: vscode.DocumentSelector = {
// scheme: "file"
language: 'markdown',
}

export function activate(context: vscode.ExtensionContext) {
// TODO: handle multiple workspace folders (detect the one(s) that contains
// the relevant files?)
const folders = vscode.workspace.workspaceFolders
const basePath = folders && folders[0]
if (!basePath) {
return
}

const entities = new EntityStore(basePath.uri.fsPath, vscode.workspace.fs)
function setup(context: vscode.ExtensionContext, baseUri: vscode.Uri) {
const entities = new EntityStore(baseUri, vscode.workspace.fs)

context.subscriptions.push(
vscode.languages.registerHoverProvider(
Expand All @@ -46,4 +52,14 @@ export function activate(context: vscode.ExtensionContext) {
setupDecorationProvider(context, entities)
}

export function deactivate() {}
async function findRootFolder() {
const expected = ['spaces', 'properties', 'theorems']

for (const folder of vscode.workspace.workspaceFolders || []) {
const files = await vscode.workspace.fs.readDirectory(folder.uri)
const names = files.map(([name, _]) => name)
if (expected.every(name => names.includes(name))) {
return folder.uri
}
}
}
File renamed without changes.
67 changes: 28 additions & 39 deletions packages/vscode/src/models/EntityStore.ts
Original file line number Diff line number Diff line change
@@ -1,24 +1,16 @@
import * as vscode from 'vscode'
import * as yaml from 'js-yaml'
import { z } from 'zod'
import { propertySchema, spaceSchema } from './schemas'
import {
Property,
PropertyId,
Space,
SpaceId,
isPropertyId,
isSpaceId,
normalizeId,
} from './types'
import { SpacePage, PropertyPage, Id, schemas } from '@pi-base/core'

type Location = { path: string; uri: vscode.Uri }

// Repository for filesystem-backed entities (spaces, properties, etc.)
export class EntityStore {
#pageCache: Record<string, string> = {}

constructor(
private readonly root: string,
private readonly root: vscode.Uri,
private readonly fs: vscode.FileSystem,
) {}

Expand All @@ -28,9 +20,9 @@ export class EntityStore {

lookup(token: string) {
try {
if (isSpaceId(token)) {
if (Id.isSpaceId(token)) {
return this.fetch(token)
} else if (isPropertyId(token)) {
} else if (Id.isPropertyId(token)) {
return this.fetch(token)
}
} catch (error) {
Expand All @@ -39,57 +31,54 @@ export class EntityStore {
}
}

private async fetch(id: SpaceId): Promise<(Space & Location) | null>
private async fetch(id: PropertyId): Promise<(Property & Location) | null>
private async fetch(id: Id.SId): Promise<(SpacePage & Location) | null>
private async fetch(id: Id.PId): Promise<(PropertyPage & Location) | null>
private async fetch(id: string) {
switch (id[0]) {
case 'S':
return this.load(
`spaces/${normalizeId(id as SpaceId)}/README.md`,
spaceSchema,
return this.load<SpacePage>(
`spaces/${Id.normalizeId(id as Id.SId)}/README.md`,
schemas.spacePage,
)
case 'P':
return this.load(
`properties/${normalizeId(id as PropertyId)}.md`,
propertySchema,
return this.load<PropertyPage>(
`properties/${Id.normalizeId(id as Id.PId)}.md`,
schemas.propertyPage,
)
default:
return null
}
}

private async load<T>(path: string, schema: z.ZodSchema<T>) {
path = `${this.root}/${path}`
const uri = expandPath(path)
path = `${this.root.path}/${path}`
const uri = this.expandPath(path)

if (!this.#pageCache[path]) {
const bytes = await this.fs.readFile(uri)
this.#pageCache[path] = new TextDecoder().decode(bytes)
}

const parsed = parseDocument(schema, this.#pageCache[path])
if (!parsed) {
return null
}
if (parsed.error) {
if (!parsed || parsed.error) {
console.error('Failed to parse', {
path,
contents: this.#pageCache[path],
error: parsed?.error.errors,
})
// TODO: handle
return null
}

return { ...parsed.data, path, uri }
}
}

function expandPath(path: string) {
// In github.dev, file URIs look like vscode-vfs://github%2B.../pi-base/data/...
// See also notes in https://code.visualstudio.com/api/extension-guides/web-extensions#migrate-extension-with-code
// TODO: clean this up / make it less implicit
const uri = vscode.Uri.file(path)
const folders = vscode.workspace.workspaceFolders
if (folders) {
const root = folders[0].uri
return uri.with({ authority: root.authority, scheme: root.scheme })
} else {
return uri
private expandPath(path: string) {
// In github.dev, file URIs look like vscode-vfs://github%2B.../pi-base/data/...
// See also notes in https://code.visualstudio.com/api/extension-guides/web-extensions#migrate-extension-with-code
// TODO: clean this up / make it less implicit
const { authority, scheme } = this.root
return vscode.Uri.file(path).with({ scheme, authority })
}
}

Expand Down
21 changes: 0 additions & 21 deletions packages/vscode/src/models/schemas.ts

This file was deleted.

Loading

0 comments on commit ba49e7f

Please sign in to comment.