Skip to content

Instantly share code, notes, and snippets.

@caasi
Last active June 19, 2020 12:08
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save caasi/8ba477644fa0acf3a3729cfe8c80dfb8 to your computer and use it in GitHub Desktop.
Save caasi/8ba477644fa0acf3a3729cfe8c80dfb8 to your computer and use it in GitHub Desktop.
import {
Term,
tru,
fal,
cond,
succ,
pred,
isZero,
wrong,
} from '../syntax';
export function evaluate(term: Term): Term {
let curr = term;
do {
curr = evaluate1(curr);
} while (!curr.isValue);
return curr;
}
function evaluate1(term: Term): Term {
return term.matchWith({
If: ({ condition, success, failure }) => condition.isBadBool
// E-If-Wrong
? wrong
: condition.matchWith({
// E-IfTrue
True: () => success,
// E-IfFalse
False: () => failure,
// E-If
_: () => cond(evaluate1(condition), success, failure),
}),
Succ: ({ term }) => term.isBadNumeric
// E-Succ-Wrong
? wrong
// E-Succ
: succ(evaluate1(term)),
Pred: ({ term }) => term.isBadNumeric
// E-Pred-Wrong
? wrong
: term.matchWith({
// E-PredZero
Zero: (x) => x,
// E-PredSucc
Succ: ({ term }) => term,
// E-Pred
_: () => pred(evaluate1(term)),
}),
IsZero: ({ term }) => term.isBadNumeric
// E-IsZero-Wrong
? wrong
: term.matchWith({
// E-IsZeroZero
Zero: () => tru,
// E-IsZeroSucc
Succ: () => fal,
// E-IsZero
_: () => isZero(evaluate1(term)),
}),
_: (x) => x,
});
}
type TermPatternFull<T> = {
readonly True: (t: True) => T,
readonly False: (t: False) => T,
readonly If: (t: If) => T,
readonly Zero: (t: Zero) => T,
readonly Succ: (t: Succ) => T,
readonly Pred: (t: Pred) => T,
readonly IsZero: (t: IsZero) => T,
readonly Wrong: (t: Wrong) => T,
}
type TermPatternPartial<T> = {
readonly True?: (t: True) => T,
readonly False?: (t: False) => T,
readonly If?: (t: If) => T,
readonly Zero?: (t: Zero) => T,
readonly Succ?: (t: Succ) => T,
readonly Pred?: (t: Pred) => T,
readonly IsZero?: (t: IsZero) => T,
readonly Wrong?: (t: Wrong) => T,
readonly _: (t: Term) => T,
}
type TermPattern<T>
= TermPatternFull<T>
| TermPatternPartial<T>
function isPartialPattern<T>(pattern: TermPattern<T>): pattern is TermPatternPartial<T> {
return (
!pattern.True ||
!pattern.False ||
!pattern.If ||
!pattern.Zero ||
!pattern.Succ ||
!pattern.Pred ||
!pattern.IsZero ||
!pattern.Wrong
);
}
export interface Term {
isValue: boolean;
isNumericValue: boolean;
isBadNumeric: boolean;
isBadBool: boolean;
matchWith<T>(pattern: TermPattern<T>): T;
}
export class True implements Term {
isValue: boolean = true;
isNumericValue: boolean = false;
isBadNumeric: boolean = true;
isBadBool: boolean = false;
matchWith<T>(pattern: TermPattern<T>): T {
return isPartialPattern(pattern)
? (pattern.True || pattern._)(this)
: pattern.True(this);
}
}
export class False implements Term {
isValue: boolean = true;
isNumericValue: boolean = false;
isBadNumeric: boolean = true;
isBadBool: boolean = false;
matchWith<T>(pattern: TermPattern<T>): T {
return isPartialPattern(pattern)
? (pattern.False || pattern._)(this)
: pattern.False(this);
}
}
export class If implements Term {
isValue: boolean = false;
isNumericValue: boolean = false;
isBadNumeric: boolean = false;
isBadBool: boolean = false;
condition: Term;
success: Term;
failure: Term;
constructor(condition: Term, success: Term, failure: Term) {
this.condition = condition;
this.success = success;
this.failure = failure;
}
matchWith<T>(pattern: TermPattern<T>): T {
return isPartialPattern(pattern)
? (pattern.If || pattern._)(this)
: pattern.If(this);
}
}
export class Zero implements Term {
isValue: boolean = true;
isNumericValue: boolean = true;
isBadNumeric: boolean = false;
isBadBool: boolean = true;
matchWith<T>(pattern: TermPattern<T>): T {
return isPartialPattern(pattern)
? (pattern.Zero || pattern._)(this)
: pattern.Zero(this);
}
}
export class Succ implements Term {
get isValue(): boolean {
return this.isNumericValue;
};
get isNumericValue(): boolean {
return this.term.isNumericValue;
};
isBadNumeric: boolean = false;
isBadBool: boolean = true;
term: Term;
constructor(term: Term) {
this.term = term;
}
matchWith<T>(pattern: TermPattern<T>): T {
return isPartialPattern(pattern)
? (pattern.Succ || pattern._)(this)
: pattern.Succ(this);
}
}
export class Pred implements Term {
isValue: boolean = false;
isNumericValue: boolean = false;
isBadNumeric: boolean = false;
isBadBool: boolean = false;
term: Term;
constructor(term: Term) {
this.term = term;
}
matchWith<T>(pattern: TermPattern<T>): T {
return isPartialPattern(pattern)
? (pattern.Pred || pattern._)(this)
: pattern.Pred(this);
}
}
export class IsZero implements Term {
isValue: boolean = false;
isNumericValue: boolean = false;
isBadNumeric: boolean = false;
isBadBool: boolean = false;
term: Term;
constructor(term: Term) {
this.term = term;
}
matchWith<T>(pattern: TermPattern<T>): T {
return isPartialPattern(pattern)
? (pattern.IsZero || pattern._)(this)
: pattern.IsZero(this);
}
}
export class Wrong implements Term {
isValue: boolean = true;
isNumericValue: boolean = false;
isBadNumeric: boolean = true;
isBadBool: boolean = true;
matchWith<T>(pattern: TermPattern<T>): T {
return isPartialPattern(pattern)
? (pattern.Wrong || pattern._)(this)
: pattern.Wrong(this);
}
}
export const tru: True = new True();
export const fal: False = new False();
export function cond(c: Term, s: Term, f: Term): If { return new If(c, s, f) }
export const zero: Zero = new Zero();
export function succ(t: Term): Succ { return new Succ(t) }
export function pred(t: Term): Pred { return new Pred(t) }
export function isZero(t: Term): IsZero { return new IsZero(t) }
export const wrong: Wrong = new Wrong();
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment