diff --git a/book/Bool.not.kind2 b/book/Bool.not.kind2
index dfd2ef73..775f3167 100644
--- a/book/Bool.not.kind2
+++ b/book/Bool.not.kind2
@@ -1,3 +1,4 @@
Bool.not
-: ∀(b: Bool) Bool
-= λb b
+: ∀(x: Bool) Bool
+= λx ~ λP λt λf
+ ?foo
diff --git a/kind2.hvm1 b/kind2.hvm1
index 7b9862ef..9c3a5247 100644
--- a/kind2.hvm1
+++ b/kind2.hvm1
@@ -13,22 +13,25 @@
//= (Pair fst snd)
//data Term
- //= (All inp bod)
- //| (Lam bod)
+ //= (All nam inp bod)
+ //| (Lam nam bod)
//| (App fun arg)
//| (Ann val typ)
- //| (Slf bod)
+ //| (Slf nam bod)
//| (Ins val)
//| (Ref nam val)
//| (Set)
- //| (Hol
- //| (Var idx)
+ //| (Hol nam ctx)
+ //| (Var nam idx)
// Prelude
// -------
-(Debug [] value) = value
-(Debug msg value) = (HVM.print (Join msg) value)
+(Debug msg value) = value
+//(Debug [] value) = value
+//(Debug msg value) = (HVM.print (Join msg) value)
+
+(NewLine) = (String.cons 10 String.nil)
(And True b) = b
(And False b) = False
@@ -71,11 +74,11 @@
// Term
// ----
-(IfAll (All inp bod) yep nop) = (yep inp bod)
-(IfAll other yep nop) = nop
+(IfAll (All nam inp bod) yep nop) = (yep nam inp bod)
+(IfAll other yep nop) = nop
-(IfSlf (Slf bod) yep nop) = (yep bod)
-(IfSlf other yep nop) = nop
+(IfSlf (Slf nam bod) yep nop) = (yep nam bod)
+(IfSlf other yep nop) = nop
// Evaluation
// ----------
@@ -86,47 +89,44 @@
(Reduce 1 (Ref nam val)) = (Reduce 1 val)
(Reduce r val) = val
-(Reduce.app r (Lam bod) arg) = (Reduce r (bod (Reduce r arg)))
-(Reduce.app r fun arg) = (App fun arg)
+(Reduce.app r (Lam nam bod) arg) = (Reduce r (bod (Reduce r arg)))
+(Reduce.app r fun arg) = (App fun arg)
(Normal r term dep) = (Normal.term r (Reduce r term) dep)
-(Normal.term r (All inp bod) dep) = (All (Normal r inp dep) λx (Normal r (bod (Var dep)) (+ dep 1)))
-(Normal.term r (Lam bod) dep) = (Lam λx (Normal r (bod (Var dep)) (+ 1 dep)))
-(Normal.term r (App fun arg) dep) = (App (Normal r fun dep) (Normal r arg dep))
-(Normal.term r (Ann val typ) dep) = (Ann (Normal r val dep) (Normal r typ dep))
-(Normal.term r (Slf bod) dep) = (Slf λx (Normal r (bod (Var dep)) (+ 1 dep)))
-(Normal.term r (Ins val) dep) = (Ins (Normal r val dep))
-(Normal.term r (Ref nam val) dep) = (Ref nam (Normal r val dep))
-(Normal.term r Set dep) = Set
-(Normal.term r (Var idx) dep) = (Var idx)
+(Normal.term r (All nam inp bod) dep) = (All nam (Normal r inp dep) λx (Normal r (bod (Var nam dep)) (+ dep 1)))
+(Normal.term r (Lam nam bod) dep) = (Lam nam λx(Normal r (bod (Var nam dep)) (+ 1 dep)))
+(Normal.term r (App fun arg) dep) = (App (Normal r fun dep) (Normal r arg dep))
+(Normal.term r (Ann val typ) dep) = (Ann (Normal r val dep) (Normal r typ dep))
+(Normal.term r (Slf nam bod) dep) = (Slf nam λx (Normal r (bod (Var nam dep)) (+ 1 dep)))
+(Normal.term r (Ins val) dep) = (Ins (Normal r val dep))
+(Normal.term r (Ref nam val) dep) = (Ref nam (Normal r val dep))
+(Normal.term r (Hol nam ctx) dep) = (Hol nam ctx)
+(Normal.term r Set dep) = Set
+(Normal.term r (Var nam idx) dep) = (Var nam idx)
// Equality
// --------
(Equal a b dep) = (Compare a b dep)
-// Note: this is a simpler equality function than the original one.
-(Compare (All a.inp a.bod) (All b.inp b.bod) dep) = (& (Equal a.inp b.inp dep) (Equal (a.bod (Var dep)) (b.bod (Var dep)) (+ 1 dep)))
-(Compare (Lam a.bod) (Lam b.bod) dep) = (Equal (a.bod (Var dep)) (b.bod (Var dep)) (+ 1 dep))
-(Compare (App a.fun a.arg) (App b.fun b.arg) dep) = (& (Equal a.fun b.fun dep) (Equal a.arg b.arg dep))
-(Compare (Ann a.val a.typ) (Ann b.val b.typ) dep) = (& (Equal a.val b.val dep) (Equal a.typ b.typ dep))
-(Compare (Slf a.bod) (Slf b.bod) dep) = (Equal (a.bod (Var dep)) (b.bod (Var dep)) (+ 1 dep))
-(Compare (Ins a.val) b dep) = (Equal a.val b dep)
-(Compare a (Ins b.val) dep) = (Equal a b.val dep)
-(Compare (Ref a.nam a.val) (Ref b.nam b.val) dep) = (Same a.nam b.nam)
-(Compare Set Set dep) = 1
-(Compare (Var a.idx) (Var b.idx) dep) = (== a.idx b.idx)
-(Compare (Ref a.nam a.val) b dep) = (Equal a.val b dep)
-(Compare a (Ref b.nam b.val) dep) = (Equal a b.val dep)
-(Compare (Ann a.val a.typ) b dep) = (Equal a.val b dep)
-(Compare a (Ann b.val b.typ) dep) = (Equal a b.val dep)
-(Compare a b dep) = 0
-
-C0 = (Lam λf(Lam λx(x)))
-C1 = (Lam λf(Lam λx(App f x)))
-C2 = (Lam λf(Lam λx(App f (App f x))))
-C3 = (Lam λf(Lam λx(App f (App f (App f x)))))
+(Compare (All a.nam a.inp a.bod) (All b.nam b.inp b.bod) dep) = (& (Equal a.inp b.inp dep) (Equal (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep)))
+(Compare (Lam a.nam a.bod) (Lam b.nam b.bod) dep) = (Equal (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep))
+(Compare (App a.fun a.arg) (App b.fun b.arg) dep) = (& (Equal a.fun b.fun dep) (Equal a.arg b.arg dep))
+(Compare (Ann a.val a.typ) (Ann b.val b.typ) dep) = (& (Equal a.val b.val dep) (Equal a.typ b.typ dep))
+(Compare (Slf a.nam a.bod) (Slf b.nam b.bod) dep) = (Equal (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep))
+(Compare (Ins a.val) b dep) = (Equal a.val b dep)
+(Compare a (Ins b.val) dep) = (Equal a b.val dep)
+(Compare (Ref a.nam a.val) (Ref b.nam b.val) dep) = (Same a.nam b.nam)
+(Compare Set Set dep) = 1
+(Compare (Var a.nam a.idx) (Var b.nam b.idx) dep) = (== a.idx b.idx)
+(Compare (Ref a.nam a.val) b dep) = (Equal a.val b dep)
+(Compare a (Ref b.nam b.val) dep) = (Equal a b.val dep)
+(Compare (Ann a.val a.typ) b dep) = (Equal a.val b dep)
+(Compare a (Ann b.val b.typ) dep) = (Equal a b.val dep)
+(Compare (Hol a.nam a.ctx) b dep) = 1
+(Compare a (Hol b.nam b.ctx) dep) = 1
+(Compare a b dep) = 0
// Logger
// -------
@@ -143,49 +143,52 @@ C3 = (Lam λf(Lam λx(App f (App f (App f x)))))
(Infer term dep) = (Debug ["Infer: " (Show term dep)] (Infer.match term dep))
-(Infer.match (All term.inp term.bod) dep) =
- (Bind (Check term.inp Set dep) λinp_ty
- (Bind (Check (term.bod (Ann (Var dep) term.inp)) Set (+ 1 dep)) λbod_ty
+(Infer.match (All nam inp bod) dep) =
+ (Bind (Check inp Set dep) λinp_ty
+ (Bind (Check (bod (Ann (Var nam dep) inp)) Set (+ 1 dep)) λbod_ty
(Pure Set)))
-(Infer.match (Lam term.bod) dep) =
- (Debug ["Error: NonFunLam " (Show (Lam term.bod) dep)] (None))
-(Infer.match (App term.fun term.arg) dep) =
- (Bind (Infer term.fun dep) λfun_ty
+(Infer.match (Lam nam bod) dep) =
+ (Debug ["Error: NonFunLam " (Show (Lam nam bod) dep)] (None))
+(Infer.match (App fun arg) dep) =
+ (Bind (Infer fun dep) λfun_ty
(IfAll (Reduce 1 fun_ty)
- λfun_ty.inp λfun_ty.bod
- (Bind (Check term.arg fun_ty.inp dep) λval_ty
- (Pure (fun_ty.bod term.arg)))
- (Debug ["Error: NonFunApp " (Show (App term.fun term.arg) dep)] None)))
-(Infer.match (Ann term.val term.typ) dep) =
- (Pure term.typ)
-(Infer.match (Slf term.bod) dep) =
- (Bind (Check (term.bod (Ann (Var dep) (Slf term.bod))) Set (+ dep 1)) λslf
+ λfun_nam λfun_ty.inp λfun_ty.bod
+ (Bind (Check arg fun_ty.inp dep) λval_ty
+ (Pure (fun_ty.bod arg)))
+ (Debug ["Error: NonFunApp " (Show (App fun arg) dep)] None)))
+(Infer.match (Ann val typ) dep) =
+ (Pure typ)
+(Infer.match (Slf nam bod) dep) =
+ (Bind (Check (bod (Ann (Var nam dep) (Slf nam bod))) Set (+ dep 1)) λslf
(Pure Set))
-(Infer.match (Ins term.val) dep) =
- (Bind (Infer term.val dep) λval_ty
+(Infer.match (Ins val) dep) =
+ (Bind (Infer val dep) λval_ty
(IfSlf (Reduce 1 val_ty)
- λval_ty.bod (Pure (val_ty.bod (Ins term.val)))
- (Debug ["Error: NonSlfIns " (Show (Ins term.val) dep)] None)))
-(Infer.match (Ref term.nam term.val) dep) =
- (Infer term.val dep)
+ λval_nam λval_ty.bod (Pure (val_ty.bod (Ins val)))
+ (Debug ["Error: NonSlfIns " (Show (Ins val) dep)] None)))
+(Infer.match (Ref nam val) dep) =
+ (Infer val dep)
(Infer.match Set dep) =
(Pure Set)
-(Infer.match (Var term.idx) dep) =
- (Debug ["Error: NonAnnVar " (Show (Var term.idx) dep)] None)
+(Infer.match (Var nam idx) dep) =
+ (Debug ["Error: NonAnnVar " (Show (Var nam idx) dep)] None)
(Check term type dep) = (Debug
["Check: " (Show term dep) " :: " (Show (Reduce 1 type) dep)]
(Check.match term (Reduce 1 type) dep))
-(Check.match (Lam term.bod) (All type.inp type.bod) dep) =
- let ann = (Ann (Var dep) type.inp)
+(Check.match (Lam term.nam term.bod) (All type.nam type.inp type.bod) dep) =
+ let ann = (Ann (Var term.nam dep) type.inp)
let term = (term.bod ann)
let type = (type.bod ann)
(Check term type (+ dep 1))
-(Check.match (Ins term.val) (Slf type.bod) dep) =
+(Check.match (Ins term.val) (Slf type.nam type.bod) dep) =
(Check term.val (type.bod (Ins term.val)) dep)
(Check.match (Ref term.nam term.val) type dep) =
(Check term.val type dep)
+(Check.match (Hol term.nam term.ctx) type dep) =
+ (HVM.print (Join ["HOLE!: ?" term.nam " :: " (Show type dep) (Context.show term.ctx dep)])
+ (Pure 0))
(Check.match val term.type dep) =
(Bind (Infer val dep) λinfer
(If (Equal term.type infer dep)
@@ -197,32 +200,26 @@ C3 = (Lam λf(Lam λx(App f (App f (App f x)))))
(Show term dep) = (Show.match term dep)
-(Show.match (All term.inp term.bod) dep) = (Join ["∀(x" (U60.show dep) ":" (Show term.inp dep) ") " (Show (term.bod (Var dep)) (+ dep 1))])
-(Show.match (Lam term.bod) dep) = (Join ["λx" (U60.show dep) " " (Show (term.bod (Var dep)) (+ dep 1))])
-(Show.match (App term.fun term.arg) dep) = (Join ["(" (Show term.fun dep) " " (Show term.arg dep) ")"])
-(Show.match (Ann term.val term.typ) dep) = (Join ["{" (Show term.val dep) ":" (Show term.typ dep) "}"])
-(Show.match (Slf term.bod) dep) = (Join ["$x" (U60.show dep) " " (Show (term.bod (Var dep)) (+ dep 1))])
-(Show.match (Ins term.val) dep) = (Join ["~" (Show term.val dep)])
-(Show.match (Ref term.nam term.val) dep) = term.nam
-(Show.match Set dep) = (Join ["*"])
-(Show.match (Var term.idx) dep) = (Join ["x" (U60.show term.idx)])
+(Show.match (All nam inp bod) dep) = (Join ["∀(" nam ": " (Show inp dep) ") " (Show (bod (Var nam dep)) (+ dep 1))])
+(Show.match (Lam nam bod) dep) = (Join ["λ" nam " " (Show (bod (Var nam dep)) (+ dep 1))])
+(Show.match (App fun arg) dep) = (Join ["(" (Show fun dep) " " (Show arg dep) ")"])
+(Show.match (Ann val typ) dep) = (Join ["{" (Show val dep) " : " (Show typ dep) "}"])
+(Show.match (Slf nam bod) dep) = (Join ["$" nam " " (Show (bod (Var nam dep)) (+ dep 1))])
+(Show.match (Ins val) dep) = (Join ["~" (Show val dep)])
+(Show.match (Ref nam val) dep) = nam
+(Show.match Set dep) = (Join ["*"])
+(Show.match (Hol nam ctx) dep) = (Join ["?" nam])
+(Show.match (Var nam idx) dep) = nam
+
+(Context.show List.nil dep) = ""
+(Context.show (List.cons x xs) dep) = (Join [NewLine "- " (Show x dep) (Context.show xs dep)])
// API
// ---
(Checker (Ref nam val)) = (Checker val)
-(Checker (Ann val typ)) = (Check val typ 0)
-(Checker val) = "untyped"
+(Checker (Ann val typ)) = (Checker.report (Check val typ 0))
+(Checker val) = (HVM.print "Untyped." 1)
-// Tests
-// -----
-
-//T_Bool = (Ref "Bool" (Ann (Slf λa (All (All T_Bool λb (Set)) λb (All (App b T_true) λc (All (App b T_false) λd (App b a))))) (Set)))
-//T_false = (Ref "false" (Ann (Lam λa (Lam λb (Lam λc c))) T_Bool))
-//T_true = (Ref "true" (Ann (Lam λa (Lam λb (Lam λc b))) T_Bool))
-//T_BoolB = (All (All T_Bool λb (Set)) λb (All (App b T_true) λc (All (App b T_false) λd (App b (Var 0)))))
-
-//Main = (Checker T_Bool)
-//Main = ((Check (Slf λa (All (All T_Bool λb (Set)) λb (All (App b T_true) λc (All (App b T_false) λd (App b a))))) Set 0) List.nil)
-
-//([(Ref "OK" (Var 0)), 1] [logs])
+(Checker.report (Some x)) = (HVM.print "Check!" 1)
+(Checker.report None) = (HVM.print "Error." 0)
diff --git a/main.ts b/main.ts
index 255a953a..0276381e 100755
--- a/main.ts
+++ b/main.ts
@@ -1,5 +1,9 @@
#!/usr/bin/env ts-node
+// NOTE FOR GPT: the file below has been refactored in order to add a "nam"
+// field to the All, Lam, Slf and Var constructors. not all functions were
+// updated. your task is to update these functions when asked.
+
// ICC: Parser, Stringifier and CLI
// ================================
@@ -19,26 +23,28 @@ const Nil = (): List => ({ tag: "Nil" });
// NEW TERM TYPE
type Term =
- | { $: "All"; inp: Term; bod: (x:Term)=> Term } // ∀(x: inp) bod
- | { $: "Lam"; bod: (x:Term)=> Term } // λx bod
+ | { $: "All"; nam: string; inp: Term; bod: (x:Term)=> Term } // ∀(x: inp) bod
+ | { $: "Lam"; nam: string; bod: (x:Term)=> Term } // λx bod
| { $: "App"; fun: Term; arg: Term } // (fun arg)
| { $: "Ann"; val: Term; typ: Term } // {val:typ}
- | { $: "Slf"; bod: (x:Term)=> Term } // $x bod
+ | { $: "Slf"; nam: string; bod: (x:Term)=> Term } // $x bod
| { $: "Ins"; val: Term } // ~val
| { $: "Set" } // *
| { $: "Ref"; nam: string; val?: Term }
- | { $: "Var"; idx: number };
+ | { $: "Hol"; nam: string }
+ | { $: "Var"; nam: string; idx: number };
// Constructors
-export const All = (inp: Term, bod: (x:Term)=> Term): Term => ({ $: "All", inp, bod });
-export const Lam = (bod: (x:Term)=> Term): Term => ({ $: "Lam", bod });
+export const All = (nam: string, inp: Term, bod: (x:Term)=> Term): Term => ({ $: "All", nam, inp, bod });
+export const Lam = (nam: string, bod: (x:Term)=> Term): Term => ({ $: "Lam", nam, bod });
export const App = (fun: Term, arg: Term): Term => ({ $: "App", fun, arg });
export const Ann = (val: Term, typ: Term): Term => ({ $: "Ann", val, typ });
-export const Slf = (bod: (x:Term)=> Term): Term => ({ $: "Slf", bod });
+export const Slf = (nam: string, bod: (x:Term)=> Term): Term => ({ $: "Slf", nam, bod });
export const Ins = (val: Term): Term => ({ $: "Ins", val });
export const Set = (): Term => ({ $: "Set" });
export const Ref = (nam: string, val?: Term): Term => ({ $: "Ref", nam, val });
-export const Var = (idx: number): Term => ({ $: "Var", idx });
+export const Hol = (nam: string): Term => ({ $: "Hol", nam });
+export const Var = (nam: string, idx: number): Term => ({ $: "Var", nam, idx });
// Book
// ----
@@ -67,29 +73,24 @@ export const name = (numb: number): string => {
return name;
}
-export const show = (term: Term, dep: number = 0): string => {
- switch (term.$) {
- case "All": return `∀(${name(dep)}: ${show(term.inp, dep)}) ${show(term.bod(Var(dep)), dep + 1)}`;
- case "Lam": return `λ${name(dep)} ${show(term.bod(Var(dep)), dep + 1)}`;
- case "App": return `(${show(term.fun, dep)} ${show(term.arg, dep)})`;
- case "Ann": return `{${show(term.val, dep)} : ${show(term.typ, dep)}}`;
- case "Slf": return `${name(dep)} ${show(term.bod(Var(dep)), dep + 1)}`;
- case "Ins": return `~${show(term.val, dep)}`;
- case "Set": return `*`;
- case "Var": return term.idx === -1 ? "*" : name(term.idx);
- case "Ref": return term.nam;
+export const context = (numb: number): string => {
+ var names = [];
+ for (var i = 0; i < numb; ++i) {
+ names.push(name(i));
}
-};
+ return "["+names.join(",")+"]";
+}
export const compile = (term: Term, used_refs: any, dep: number = 0): string => {
switch (term.$) {
- case "All": return `(All ${compile(term.inp, used_refs, dep)} λ${name(dep)} ${compile(term.bod(Var(dep)), used_refs, dep + 1)})`;
- case "Lam": return `(Lam λ${name(dep)} ${compile(term.bod(Var(dep)), used_refs, dep + 1)})`;
+ case "All": return `(All "${term.nam}" ${compile(term.inp, used_refs, dep)} λ${name(dep)} ${compile(term.bod(Var(term.nam,dep)), used_refs, dep + 1)})`;
+ case "Lam": return `(Lam "${term.nam}" λ${name(dep)} ${compile(term.bod(Var(term.nam,dep)), used_refs, dep + 1)})`;
case "App": return `(App ${compile(term.fun, used_refs, dep)} ${compile(term.arg, used_refs, dep)})`;
case "Ann": return `(Ann ${compile(term.val, used_refs, dep)} ${compile(term.typ, used_refs, dep)})`;
- case "Slf": return `(Slf λ${name(dep)} ${compile(term.bod(Var(dep)), used_refs, dep + 1)})`;
+ case "Slf": return `(Slf "${term.nam}" λ${name(dep)} ${compile(term.bod(Var(term.nam,dep)), used_refs, dep + 1)})`;
case "Ins": return `(Ins ${compile(term.val, used_refs, dep)})`;
case "Set": return `(Set)`;
+ case "Hol": return `(Hol "${term.nam}" ${context(dep)})`;
case "Var": return name(term.idx);
case "Ref": return (used_refs[term.nam] = 1), ("Book." + term.nam);
}
@@ -166,13 +167,13 @@ export function parse_term(code: string): [string, (ctx: Scope) => Term] {
var [code, inp] = parse_term(code);
var [code, __ ] = parse_text(code, ")");
var [code, bod] = parse_term(code);
- return [code, ctx => All(inp(ctx), x => bod(Cons([nam, x], ctx)))];
+ return [code, ctx => All(nam, inp(ctx), x => bod(Cons([nam, x], ctx)))];
}
// LAM: `λx f`
if (code[0] === "λ") {
var [code, nam] = parse_name(code.slice(1));
var [code, bod] = parse_term(code);
- return [code, ctx => Lam(x => bod(Cons([nam, x], ctx)))];
+ return [code, ctx => Lam(nam, x => bod(Cons([nam, x], ctx)))];
}
// APP: `(f x y z ...)`
if (code[0] === "(") {
@@ -198,7 +199,7 @@ export function parse_term(code: string): [string, (ctx: Scope) => Term] {
if (code[0] === "$") {
var [code, nam] = parse_name(code.slice(1));
var [code, bod] = parse_term(code);
- return [code, ctx => Slf(x => bod(Cons([nam, x], ctx)))];
+ return [code, ctx => Slf(nam, x => bod(Cons([nam, x], ctx)))];
}
// INS: `~x`
if (code[0] === "~") {
@@ -209,6 +210,11 @@ export function parse_term(code: string): [string, (ctx: Scope) => Term] {
if (code[0] === "*") {
return [code.slice(1), ctx => Set()];
}
+ // HOL: `?name`
+ if (code[0] === "?") {
+ var [code, nam] = parse_name(code.slice(1));
+ return [code, ctx => Hol(nam)];
+ }
// VAR: `name`
var [code, nam] = parse_name(code);
if (nam.length > 0) {
@@ -269,7 +275,6 @@ export function main() {
// Parses into book.
const book = do_parse_book(code);
-
// Compiles book to hvm1.
//var book_hvm1 = "Names = [" + Object.keys(book).map(x => '"'+x+'"').join(",") + "]\n";
//var ref_count = 0;