mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-07-14 21:00:27 +03:00
tmp
This commit is contained in:
Victor Taelin
parent
b9683c424d
commit
6b764e9522
@ -1,4 +1,4 @@
|
||||
Bool.lemma.bft
|
||||
Bool.lemma.notnot
|
||||
: ∀(b: Bool)
|
||||
(Equal Bool (Bool.not (Bool.not b)) b)
|
||||
= λb (~b λx(Equal Bool (Bool.not (Bool.not x)) x)
|
||||
|
||||
@ -2,6 +2,6 @@ Nat
|
||||
: *
|
||||
= $self
|
||||
∀(P: ∀(n: Nat) *)
|
||||
∀(s: ∀(n: Nat) (P (Nat.succ n)))
|
||||
∀(z: (P Nat.zero))
|
||||
∀(succ: ∀(n: Nat) (P (Nat.succ n)))
|
||||
∀(zero: (P Nat.zero))
|
||||
(P self)
|
||||
|
||||
@ -1,5 +1,5 @@
|
||||
Nat.succ
|
||||
: ∀(n: Nat) Nat
|
||||
= λn
|
||||
~λP λs λz
|
||||
(s n)
|
||||
~λP λsucc λzero
|
||||
(succ n)
|
||||
|
||||
@ -1,5 +1,5 @@
|
||||
Nat.zero
|
||||
: Nat
|
||||
= ~λP λs λz
|
||||
z
|
||||
= ~λP λsucc λzero
|
||||
zero
|
||||
|
||||
|
||||
97
kind2.hvm1
97
kind2.hvm1
@ -27,9 +27,9 @@
|
||||
// Prelude
|
||||
// -------
|
||||
|
||||
//(Debug msg value) = value
|
||||
(Debug [] value) = value
|
||||
(Debug msg value) = (HVM.print (Join msg) value)
|
||||
(Debug dep msg value) = value
|
||||
//(Debug dep [] value) = value
|
||||
//(Debug dep msg value) = (HVM.print (Join msg) value)
|
||||
|
||||
(NewLine) = (String.cons 10 String.nil)
|
||||
|
||||
@ -71,27 +71,32 @@
|
||||
|
||||
(Get (Pair fst snd) fun) = (fun fst snd)
|
||||
|
||||
// Term
|
||||
// ----
|
||||
(Pure x) = (Some x)
|
||||
|
||||
(IfAll (All nam inp bod) yep nop) = (yep nam inp bod)
|
||||
(IfAll other yep nop) = nop
|
||||
(Bind a b) = (Bind.match a b)
|
||||
|
||||
(IfSlf (Slf nam bod) yep nop) = (yep nam bod)
|
||||
(IfSlf other yep nop) = nop
|
||||
(Bind.match None b) = None
|
||||
(Bind.match (Some a) b) = (b a)
|
||||
|
||||
// Evaluation
|
||||
// ----------
|
||||
|
||||
(Reduce r (App fun arg)) = (Reduce.app r (Reduce r fun) arg)
|
||||
(Reduce r (Ann val typ)) = (Reduce r val)
|
||||
(Reduce r (Ins val)) = (Reduce r val)
|
||||
(Reduce 1 (Ref nam val)) = (Reduce 1 val)
|
||||
(Reduce r val) = val
|
||||
(Reduce r (App fun arg)) = (Reduce.app r (Reduce r fun) arg)
|
||||
(Reduce r (Ann val typ)) = (Reduce r val)
|
||||
(Reduce r (Ins val)) = (Reduce r val)
|
||||
(Reduce 1 (Ref nam val)) = (Reduce 1 val)
|
||||
(Reduce r (Op2 op2 fst snd)) = (Reduce.op2 op2 fst snd)
|
||||
(Reduce r val) = val
|
||||
|
||||
(Reduce.app r (Lam nam bod) arg) = (Reduce r (bod (Reduce r arg)))
|
||||
(Reduce.app r fun arg) = (App fun arg)
|
||||
|
||||
(Reduce.op2 ADD (Num fst) (Num snd)) = (Num (+ fst snd))
|
||||
(Reduce.op2 SUB (Num fst) (Num snd)) = (Num (- fst snd))
|
||||
(Reduce.op2 MUL (Num fst) (Num snd)) = (Num (* fst snd))
|
||||
(Reduce.op2 DIV (Num fst) (Num snd)) = (Num (/ fst snd))
|
||||
(Reduce.op2 op2 fst snd) = (Op2 op2 fst snd)
|
||||
|
||||
(Normal r term dep) = (Normal.term r (Reduce r term) dep)
|
||||
|
||||
(Normal.term r (All nam inp bod) dep) = (All nam (Normal r inp dep) λx (Normal r (bod (Var nam dep)) (+ dep 1)))
|
||||
@ -103,13 +108,16 @@
|
||||
(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 U60 dep) = U60
|
||||
(Normal.term r (Num val) dep) = (Num val)
|
||||
(Normal.term r (Op2 op2 fst snd) dep) = (Op2 op2 (Normal.term r fst dep) (Normal.term r snd dep))
|
||||
(Normal.term r (Var nam idx) dep) = (Var nam idx)
|
||||
|
||||
// Equality
|
||||
// --------
|
||||
|
||||
(Equal a b dep) = (If (Compare a b dep) 1 (Compare (Reduce 1 a) (Reduce 1 b) dep))
|
||||
//(Equal a b dep) = (Debug ["Equal: " (Show a dep) NewLine " == " (Show b dep)] (If (Compare a b dep) 1 (Compare (Reduce 1 a) (Reduce 1 b) dep)))
|
||||
//(Equal a b dep) = (Debug dep ["Equal: " (Show a dep) NewLine " == " (Show b dep)] (If (Compare a b dep) 1 (Compare (Reduce 1 a) (Reduce 1 b) dep)))
|
||||
|
||||
(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))
|
||||
@ -121,28 +129,27 @@
|
||||
(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 (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) = (Debug ["Found: ?" a.nam " = " (Show b dep)] 1)
|
||||
(Compare a (Hol b.nam b.ctx) dep) = (Debug ["Found: ?" b.nam " = " (Show a dep)] 1)
|
||||
(Compare (Hol a.nam a.ctx) b dep) = (Debug dep ["Found: ?" a.nam " = " (Show b dep)] 1)
|
||||
(Compare a (Hol b.nam b.ctx) dep) = (Debug dep ["Found: ?" b.nam " = " (Show a dep)] 1)
|
||||
(Compare U60 U60 dep) = 1
|
||||
(Compare (Num a.val) (Num b.val) dep) = (== a.val b.val)
|
||||
(Compare (Op2 a.op2 a.fst a.snd) (Op2 b.op2 b.fst b.snd) dep) = (& (Equal a.fst a.snd dep) (Equal b.fst b.snd dep))
|
||||
(Compare a b dep) = 0
|
||||
|
||||
// Logger
|
||||
// -------
|
||||
|
||||
(Pure x) = (Some x)
|
||||
|
||||
(Bind a b) = (Bind.match a b)
|
||||
|
||||
(Bind.match None b) = None
|
||||
(Bind.match (Some a) b) = (b a)
|
||||
|
||||
// Type-Checking
|
||||
// -------------
|
||||
|
||||
//(Infer term dep) = (Debug ["Infer: " (Show term dep)] (Infer.match term dep))
|
||||
(IfAll (All nam inp bod) yep nop) = (yep nam inp bod)
|
||||
(IfAll other yep nop) = nop
|
||||
|
||||
(IfSlf (Slf nam bod) yep nop) = (yep nam bod)
|
||||
(IfSlf other yep nop) = nop
|
||||
|
||||
//(Infer term dep) = (Debug dep ["Infer: " (Show term dep)] (Infer.match term dep))
|
||||
(Infer term dep) = (Infer.match term dep)
|
||||
|
||||
(Infer.match (All nam inp bod) dep) =
|
||||
@ -150,14 +157,14 @@
|
||||
(Bind (Check (bod (Ann (Var nam dep) inp)) Set (+ 1 dep)) λbod_ty
|
||||
(Pure Set)))
|
||||
(Infer.match (Lam nam bod) dep) =
|
||||
(Debug ["Error: NonFunLam " (Show (Lam nam bod) dep)] (None))
|
||||
(Debug dep ["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_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)))
|
||||
(Debug dep ["Error: NonFunApp " (Show (App fun arg) dep)] None)))
|
||||
(Infer.match (Ann val typ) dep) =
|
||||
(Pure typ)
|
||||
(Infer.match (Slf nam bod) dep) =
|
||||
@ -167,15 +174,23 @@
|
||||
(Bind (Infer val dep) λval_ty
|
||||
(IfSlf (Reduce 1 val_ty)
|
||||
λval_nam λval_ty.bod (Pure (val_ty.bod (Ins val)))
|
||||
(Debug ["Error: NonSlfIns " (Show (Ins val) dep)] None)))
|
||||
(Debug dep ["Error: NonSlfIns " (Show (Ins val) dep)] None)))
|
||||
(Infer.match (Ref nam val) dep) =
|
||||
(Infer val dep)
|
||||
(Infer.match Set dep) =
|
||||
(Pure Set)
|
||||
(Infer.match U60 dep) =
|
||||
(Pure Set)
|
||||
(Infer.match (Num num) dep) =
|
||||
(Pure U60)
|
||||
(Infer.match (Op2 op2 fst snd) dep) =
|
||||
(Bind (Check fst U60 dep) λfst
|
||||
(Bind (Check snd U60 dep) λsnd
|
||||
(Pure U60)))
|
||||
(Infer.match (Hol nam ctx) dep) =
|
||||
(Debug ["Error: NonAnnHol " (Show (Hol nam ctx) dep)] None)
|
||||
(Debug dep ["Error: NonAnnHol " (Show (Hol nam ctx) dep)] None)
|
||||
(Infer.match (Var nam idx) dep) =
|
||||
(Debug ["Error: NonAnnVar " (Show (Var nam idx) dep)] None)
|
||||
(Debug dep ["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 term type dep) = (Check.match term type dep)
|
||||
@ -194,13 +209,13 @@
|
||||
(Check.match (Ref term.nam term.val) type dep) =
|
||||
(Check term.val type dep)
|
||||
(Check.match (Hol term.nam term.ctx) type dep) =
|
||||
(Debug ["HOLE!: ?" term.nam " :: " (Show (Normal 0 type dep) dep) (Context.show term.ctx dep)]
|
||||
(Debug dep ["HOLE!: ?" term.nam " :: " (Show (Normal 0 type dep) 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)
|
||||
(Pure 0)
|
||||
(Debug ["Error: " (Show (Normal 0 infer dep) dep) NewLine " != " (Show (Normal 0 term.type dep) dep)] None)))
|
||||
(Debug dep ["Error: " (Show (Normal 0 infer dep) dep) NewLine " != " (Show (Normal 0 term.type dep) dep)] None)))
|
||||
|
||||
// Syntax
|
||||
// ------
|
||||
@ -215,6 +230,9 @@
|
||||
(Show.match (Ins val) dep) = (Join ["~" (Show val dep)])
|
||||
(Show.match (Ref nam val) dep) = nam
|
||||
(Show.match Set dep) = (Join ["*"])
|
||||
(Show.match U60 dep) = "#U60"
|
||||
(Show.match (Num val) dep) = (Join ["#" (U60.show val)])
|
||||
(Show.match (Op2 op2 fst snd) dep) = (Join ["#(" (Op2.show op2) " " (Show fst dep) " " (Show snd dep) ")"])
|
||||
(Show.match (Hol nam ctx) dep) = (Join ["?" nam])
|
||||
(Show.match (Var nam idx) dep) = nam
|
||||
|
||||
@ -225,6 +243,11 @@
|
||||
(Show.begin (String.cons x xs)) = (String.cons x (Show.begin xs))
|
||||
(Show.begin String.nil) = String.nil
|
||||
|
||||
(Op2.show ADD) = "+"
|
||||
(Op2.show SUB) = "-"
|
||||
(Op2.show MUL) = "*"
|
||||
(Op2.show DIV) = "/"
|
||||
|
||||
(Context.show List.nil dep) = ""
|
||||
(Context.show (List.cons x xs) dep) = (Join [NewLine "- " (Context.show.ann x dep) (Context.show xs dep)])
|
||||
|
||||
|
||||
59
main.ts
59
main.ts
@ -28,6 +28,9 @@ type Term =
|
||||
| { $: "Slf"; nam: string; bod: (x:Term)=> Term } // $x bod
|
||||
| { $: "Ins"; val: Term } // ~val
|
||||
| { $: "Set" } // *
|
||||
| { $: "U60" } // #U60
|
||||
| { $: "Num"; val: BigInt } // #num
|
||||
| { $: "Op2"; op2: string; fst: Term; snd: Term } // #(<op2> fst snd)
|
||||
| { $: "Ref"; nam: string; val?: Term }
|
||||
| { $: "Hol"; nam: string }
|
||||
| { $: "Var"; nam: string; idx: number };
|
||||
@ -40,6 +43,9 @@ export const Ann = (val: Term, typ: Term): Term => ({ $: "Ann", val, typ });
|
||||
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 U60 = (): Term => ({ $: "U60" });
|
||||
export const Num = (val: BigInt): Term => ({ $: "Num", val });
|
||||
export const Op2 = (op2: string, fst: Term, snd: Term): Term => ({ $: "Op2", op2, fst, snd });
|
||||
export const Ref = (nam: string, val?: Term): Term => ({ $: "Ref", nam, val });
|
||||
export const Hol = (nam: string): Term => ({ $: "Hol", nam });
|
||||
export const Var = (nam: string, idx: number): Term => ({ $: "Var", nam, idx });
|
||||
@ -79,6 +85,23 @@ export const context = (numb: number): string => {
|
||||
return "["+names.join(",")+"]";
|
||||
}
|
||||
|
||||
const compile_oper = (op2: string): string => {
|
||||
switch (op2) {
|
||||
case "+" : return "ADD";
|
||||
case "-" : return "SUB";
|
||||
case "*" : return "MUL";
|
||||
case "/" : return "DIV";
|
||||
case "%" : return "MOD";
|
||||
case "==": return "EQ";
|
||||
case "!=": return "NEQ";
|
||||
case "<" : return "LT";
|
||||
case "<=": return "LTE";
|
||||
case ">" : return "GT";
|
||||
case ">=": return "GTE";
|
||||
default: throw new Error("Unknown operator: " + op2);
|
||||
}
|
||||
};
|
||||
|
||||
export const compile = (term: Term, used_refs: any, dep: number = 0): string => {
|
||||
switch (term.$) {
|
||||
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)})`;
|
||||
@ -88,6 +111,9 @@ export const compile = (term: Term, used_refs: any, dep: number = 0): string =>
|
||||
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 "U60": return `(U60)`;
|
||||
case "Num": return `(Num ${term.val.toString()})`;
|
||||
case "Op2": return `(Op2 ${compile_oper(term.op2)} ${compile(term.fst, used_refs, dep)} ${compile(term.snd, used_refs, dep)})`;
|
||||
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);
|
||||
@ -135,16 +161,28 @@ export function is_name_char(c: string): boolean {
|
||||
return /[a-zA-Z0-9_.]/.test(c);
|
||||
}
|
||||
|
||||
export function parse_name(code: string): [string, string] {
|
||||
export function is_oper_char(c: string): boolean {
|
||||
return /[+\-*/%<>=&|^!~]/.test(c);
|
||||
}
|
||||
|
||||
export function parse_word(is_letter: (c: string) => boolean, code: string): [string, string] {
|
||||
code = skip(code);
|
||||
var name = "";
|
||||
while (is_name_char(code[0]||"")) {
|
||||
while (is_letter(code[0]||"")) {
|
||||
name = name + code[0];
|
||||
code = code.slice(1);
|
||||
}
|
||||
return [code, name];
|
||||
}
|
||||
|
||||
export function parse_name(code: string): [string, string] {
|
||||
return parse_word(is_name_char, code);
|
||||
}
|
||||
|
||||
export function parse_oper(code: string): [string, string] {
|
||||
return parse_word(is_oper_char, code);
|
||||
}
|
||||
|
||||
export function parse_text(code: string, text: string): [string, null] {
|
||||
code = skip(code);
|
||||
if (text === "") {
|
||||
@ -208,6 +246,23 @@ export function parse_term(code: string): [string, (ctx: Scope) => Term] {
|
||||
if (code[0] === "*") {
|
||||
return [code.slice(1), ctx => Set()];
|
||||
}
|
||||
// U60: `#U60`
|
||||
if (code.slice(0,4) === "#U60") {
|
||||
return [code.slice(4), ctx => U60()];
|
||||
}
|
||||
// OP2: `#(<op2> fst snd)`
|
||||
if (code.slice(0,2) === "#(") {
|
||||
var [code, op2] = parse_oper(code.slice(2));
|
||||
var [code, fst] = parse_term(code);
|
||||
var [code, snd] = parse_term(code);
|
||||
var [code, _] = parse_text(code, ")");
|
||||
return [code, ctx => Op2(op2, fst(ctx), snd(ctx))];
|
||||
}
|
||||
// NUM: `#num`
|
||||
if (code[0] === "#") {
|
||||
var [code, num] = parse_name(code.slice(1));
|
||||
return [code, ctx => Num(BigInt(num))];
|
||||
}
|
||||
// HOL: `?name`
|
||||
if (code[0] === "?") {
|
||||
var [code, nam] = parse_name(code.slice(1));
|
||||
|
||||
Loading…
Reference in New Issue
Block a user