152 lines
4.0 KiB
TypeScript
152 lines
4.0 KiB
TypeScript
export type PropVar = "p" | "q" | "r" | "s";
|
||
|
||
export const propVars: PropVar[] = ["p", "q", "r", "s"];
|
||
|
||
export type Formula =
|
||
| { type: "top" | "bot" }
|
||
| { type: "propvar"; name: PropVar }
|
||
| { type: "not" | "box" | "diamond"; fml: Formula }
|
||
| {
|
||
type: "to" | "or" | "and" | "eq";
|
||
left: Formula;
|
||
right: Formula;
|
||
};
|
||
|
||
export function vars(fml: Formula): Set<PropVar> {
|
||
switch (fml.type) {
|
||
case "top":
|
||
case "bot":
|
||
return new Set();
|
||
case "box":
|
||
case "diamond":
|
||
case "not":
|
||
return vars(fml.fml);
|
||
case "to":
|
||
case "or":
|
||
case "and":
|
||
case "eq":
|
||
return new Set([...vars(fml.left), ...vars(fml.right)]);
|
||
case "propvar":
|
||
return new Set([fml.name]);
|
||
}
|
||
}
|
||
|
||
export const propvar = (name: PropVar) => ({ type: "propvar", name }) as const;
|
||
|
||
export const top = { type: "top" } as const satisfies Formula;
|
||
export const bot = { type: "bot" } as const satisfies Formula;
|
||
|
||
export const box = (fml: Formula) =>
|
||
({ type: "box", fml }) as const satisfies Formula;
|
||
export const diamond = (fml: Formula) =>
|
||
({ type: "diamond", fml }) as const satisfies Formula;
|
||
export const not = (fml: Formula) =>
|
||
({ type: "not", fml }) as const satisfies Formula;
|
||
|
||
export const to = (left: Formula, right: Formula) =>
|
||
({ type: "to", left, right }) as const satisfies Formula;
|
||
export const and = (left: Formula, right: Formula) =>
|
||
({ type: "and", left, right }) as const satisfies Formula;
|
||
export const or = (left: Formula, right: Formula) =>
|
||
({ type: "or", left, right }) as const satisfies Formula;
|
||
export const eq = (left: Formula, right: Formula) =>
|
||
({ type: "eq", left, right }) as const satisfies Formula;
|
||
|
||
export type Symbols = Record<Exclude<Formula["type"], "propvar">, string>;
|
||
|
||
export const asciiSymbols: Symbols = {
|
||
top: "T",
|
||
bot: "F",
|
||
box: "[]",
|
||
diamond: "<>",
|
||
not: "~",
|
||
and: "^",
|
||
or: "v",
|
||
to: "->",
|
||
eq: "<->",
|
||
};
|
||
|
||
export const unicodeSymbols: Symbols = {
|
||
top: "⊤",
|
||
bot: "⊥",
|
||
box: "□",
|
||
diamond: "◇",
|
||
not: "¬",
|
||
and: "∧",
|
||
or: "∨",
|
||
to: "→",
|
||
eq: "↔",
|
||
};
|
||
|
||
export const latexSymbols: Symbols = {
|
||
top: "\\top ",
|
||
bot: "\\bot ",
|
||
box: "\\Box ",
|
||
diamond: "\\Diamond ",
|
||
not: "\\neg ",
|
||
and: "\\land",
|
||
or: "\\lor",
|
||
to: "\\to",
|
||
eq: "\\leftrightarrow",
|
||
};
|
||
|
||
export function prettyPrint(
|
||
fml: Formula,
|
||
config?: { paren?: boolean | ((fml: Formula) => boolean); symbols?: Symbols },
|
||
): string {
|
||
const { paren = false, symbols = unicodeSymbols } = config ?? {};
|
||
const withParen = (s: string) =>
|
||
(typeof paren === "boolean" ? paren : paren(fml)) ? `(${s})` : s;
|
||
|
||
switch (fml.type) {
|
||
case "top":
|
||
return symbols.top;
|
||
case "bot":
|
||
return symbols.bot;
|
||
case "propvar":
|
||
return fml.name;
|
||
case "not":
|
||
return `${symbols.not}${prettyPrint(fml.fml, { paren: true, symbols })}`;
|
||
case "box":
|
||
return `${symbols.box}${prettyPrint(fml.fml, { paren: true, symbols })}`;
|
||
case "diamond":
|
||
return `${symbols.diamond}${prettyPrint(fml.fml, { paren: true, symbols })}`;
|
||
case "and": {
|
||
const newConfig: typeof config = {
|
||
symbols,
|
||
paren: (f) => f.type !== "and",
|
||
};
|
||
return withParen(
|
||
`${prettyPrint(fml.left, newConfig)} ${symbols.and} ${prettyPrint(fml.right, newConfig)}`,
|
||
);
|
||
}
|
||
case "or": {
|
||
const newConfig: typeof config = {
|
||
symbols,
|
||
paren: (f) => f.type !== "or",
|
||
};
|
||
return withParen(
|
||
`${prettyPrint(fml.left, newConfig)} ${symbols.or} ${prettyPrint(fml.right, newConfig)}`,
|
||
);
|
||
}
|
||
case "to": {
|
||
const newConfig: typeof config = {
|
||
symbols,
|
||
paren: (f) => f.type !== "to",
|
||
};
|
||
return withParen(
|
||
`${prettyPrint(fml.left, { symbols, paren: true })} ${symbols.to} ${prettyPrint(fml.right, newConfig)}`,
|
||
);
|
||
}
|
||
case "eq": {
|
||
const newConfig: typeof config = {
|
||
symbols,
|
||
paren: (f) => f.type !== "eq",
|
||
};
|
||
return withParen(
|
||
`${prettyPrint(fml.left, newConfig)} ${symbols.eq} ${prettyPrint(fml.right, newConfig)}`,
|
||
);
|
||
}
|
||
}
|
||
}
|