Represent polarizers as function application

src/semantics/compact.ts

@@ -171,8 +171,6 @@ export function compact(expr: CompactExpr): CompactExpr {
 				fn: compact(expr.fn) as Expr,
 				argument: compact(expr.argument) as Expr,
 			};
-		case 'polarizer':
-			return { ...expr, body: compact(expr.body) as Expr };
 		case 'presuppose':
 			return {
 				...expr,

src/semantics/format/base.ts

@@ -1,4 +1,4 @@
-import { Expr, KnownConstant, KnownInfix } from '../model';
+import { Expr, KnownConstant, KnownInfix, KnownPolarizer } from '../model';
 
 export type NameType = 'e' | 'v' | 'i' | 's' | 'fn';
 
@@ -40,7 +40,7 @@ export interface Names {
 
 export type Quantifier = (Expr & { head: 'quantifier' })['name'] | 'lambda';
 export type Infix = KnownInfix['name'];
-export type Polarizer = (Expr & { head: 'polarizer' })['name'];
+export type Polarizer = KnownPolarizer['name'];
 export type Constant = KnownConstant['name'];
 
 /**
@@ -69,7 +69,6 @@ export interface Format<T> {
 	let: (name: T, value: T, body: T) => T;
 	symbolForInfix: (symbol: Infix) => T;
 	infix: (symbol: T, left: T, right: T) => T;
-	symbolForPolarizer: (symbol: Polarizer) => T;
 	polarizer: (symbol: T, body: T) => T;
 	symbolForConstant: (symbol: Constant) => T;
 	quote: (text: string) => T;

src/semantics/format/json.ts

@@ -101,7 +101,6 @@ export const json: Format<JsonExprIntermediate> = {
 		left: left as JsonExpr,
 		right: right as JsonExpr,
 	}),
-	symbolForPolarizer: polarizer => polarizer,
 	polarizer: (polarizer, body) =>
 		({ [polarizer as Polarizer]: body as JsonExpr }) as JsonPolarizerExpr,
 	symbolForConstant: constant => ({ constant }),

src/semantics/format/latex.ts

@@ -56,12 +56,10 @@ export const latex: Format<string> = {
 		roi: '&',
 	}),
 	infix: (symbol, left, right) => `${left} ${symbol} ${right}`,
-	symbolForPolarizer: fnFromMap({
-		not: '\\neg',
-		indeed: '\\dagger',
-	}),
 	polarizer: (symbol, body) => `${symbol} ${body}`,
 	symbolForConstant: fnFromMap({
+		not: '\\neg',
+		indeed: '\\dagger',
 		ji: '\\text{jí}',
 		suq: '\\text{súq}',
 		nhao: '\\text{nháo}',

src/semantics/format/mathml.ts

@@ -66,12 +66,10 @@ export const mathml: Format<string> = {
 		roi: '<mo>&</mo>',
 	}),
 	infix: (symbol, left, right) => `${left} ${symbol} ${right}`,
-	symbolForPolarizer: fnFromMap({
-		not: '<mo>¬</mo>',
-		indeed: '<mo>†</mo>',
-	}),
 	polarizer: (symbol, body) => `${symbol} ${body}`,
 	symbolForConstant: fnFromMap({
+		not: '<mo>¬</mo>',
+		indeed: '<mo>†</mo>',
 		ji: '<mi>jí</mi>',
 		suq: '<mi>súq</mi>',
 		nhao: '<mi>nháo</mi>',

src/semantics/format/plaintext.ts

@@ -69,12 +69,10 @@ export const plainText: Format<string> = {
 		roi: '&',
 	}),
 	infix: (symbol, left, right) => `${left} ${symbol} ${right}`,
-	symbolForPolarizer: fnFromMap({
-		not: '¬',
-		indeed: '†',
-	}),
 	polarizer: (symbol, body) => `${symbol}${body}`,
 	symbolForConstant: fnFromMap({
+		not: '¬',
+		indeed: '†',
 		ji: 'jí',
 		suq: 'súq',
 		nhao: 'nháo',

src/semantics/model.ts

@@ -63,14 +63,6 @@ interface Presuppose {
 	defines?: number;
 }
 
-type Polarizer<Name extends string> = {
-	head: 'polarizer';
-	type: 't';
-	context: ExprType[];
-	name: Name;
-	body: Expr;
-};
-
 interface Quantifier<Name extends string> {
 	head: 'quantifier';
 	type: 't';
@@ -122,7 +114,12 @@ export type KnownInfix =
 	| Constant<'roi', ['e', ['e', 'e']]>
 	| Constant<'coevent', ['v', ['v', 't']]>;
 
+export type KnownPolarizer =
+	| Constant<'not', ['t', 't']>
+	| Constant<'indeed', ['t', 't']>;
+
 export type KnownConstant =
+	| KnownPolarizer
 	| Pronoun<'ji'>
 	| Pronoun<'suq'>
 	| Pronoun<'nhao'>
@@ -169,8 +166,6 @@ export type Expr =
 	| Presuppose
 	| KnownInfix
 	| KnownConstant
-	| Polarizer<'not'>
-	| Polarizer<'indeed'>
 	| Quantifier<'some'>
 	| Quantifier<'every'>
 	| Quantifier<'every_sing'>
@@ -476,13 +471,16 @@ export function implies(left: Expr, right: Expr): Expr {
 	return conjunction('implies', left, right);
 }
 
-export function polarizer(
-	name: (Expr & { head: 'polarizer' })['name'],
-	body: Expr,
-): Expr {
+export function polarizer(name: KnownPolarizer['name'], body: Expr): Expr {
 	assertSubtype(body.type, 't');
 
-	return { head: 'polarizer', type: 't', context: body.context, name, body };
+	const operator: Expr = {
+		head: 'constant',
+		type: ['t', 't'],
+		context: body.context,
+		name,
+	};
+	return app(operator, body);
 }
 
 export function not(body: Expr): Expr {

src/semantics/operations.ts

@@ -68,9 +68,6 @@ function mapVariables(
 				e.defines === undefined ? undefined : mapDefines(e.defines),
 			);
 		}
-		case 'polarizer': {
-			return polarizer(e.name, sub(e.body));
-		}
 		case 'quantifier': {
 			return quantifier(
 				e.name,
@@ -321,10 +318,6 @@ export function reduce_(e: Expr, premises: Set<string>): Expr {
 			body = withPremise(presupposition, () => reduceAndIsolate(e.body));
 			break;
 		}
-		case 'polarizer': {
-			body = polarizer(e.name, reduceAndIsolate(e.body));
-			break;
-		}
 		case 'quantifier': {
 			const restriction =
 				e.restriction === undefined
@@ -741,9 +734,6 @@ function* subexprsShallow(e: Expr): Generator<Expr, void, unknown> {
 			yield* subexprsShallow(e.body);
 			yield* subexprsShallow(e.presupposition);
 			break;
-		case 'polarizer':
-			yield* subexprsShallow(e.body);
-			break;
 		default:
 			e satisfies never; // This switch statement should be exhaustive
 	}

src/semantics/render.ts

@@ -1,6 +1,12 @@
 import { Impossible } from '../core/error';
 import { CompactExpr } from './compact';
-import { Expr, ExprType, KnownConstant, KnownInfix } from './model';
+import {
+	Expr,
+	ExprType,
+	KnownConstant,
+	KnownInfix,
+	KnownPolarizer,
+} from './model';
 import {
 	Format,
 	NameType,
@@ -39,6 +45,11 @@ const infixAssociativity: Record<KnownInfix['name'], boolean> = {
 	coevent: false,
 };
 
+const polarizerPrecedence: Record<KnownPolarizer['name'], number> = {
+	not: 14,
+	indeed: 14,
+};
+
 const noNames: Names = {
 	context: [],
 	nextVariableIds: {
@@ -179,6 +190,15 @@ function render<T>(
 				const right = render(e.argument, names, fmt, p, rp);
 				const content = fmt.infix(symbol, left, right);
 				return bracket ? fmt.bracket(content) : content;
+			} else if (e.fn.head === 'constant' && e.fn.name in polarizerPrecedence) {
+				const name = e.fn.name as KnownPolarizer['name'];
+				const symbol = fmt.symbolForConstant(name);
+				const p = polarizerPrecedence[name];
+				const bracket = rightPrecedence > p;
+				const rp = bracket ? 0 : rightPrecedence;
+				const body = render(e.argument, names, fmt, p, rp);
+				const content = fmt.polarizer(symbol, body);
+				return bracket ? fmt.bracket(content) : content;
 			} else {
 				const p = 14;
 				const bracket = leftPrecedence > p;
@@ -202,14 +222,6 @@ function render<T>(
 			const content = fmt.presuppose(body, presupposition);
 			return bracket ? fmt.bracket(content) : content;
 		}
-		case 'polarizer': {
-			const symbol = fmt.symbolForPolarizer(e.name);
-			const p = 14;
-			const bracket = rightPrecedence > p;
-			const body = render(e.body, names, fmt, p, bracket ? 0 : rightPrecedence);
-			const content = fmt.polarizer(symbol, body);
-			return bracket ? fmt.bracket(content) : content;
-		}
 		case 'quantifier': {
 			const symbol = fmt.symbolForQuantifier(e.name);
 			const p = 2;