mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-08-17 08:30:27 +03:00
this is temporarily becoming a behemoth, but that is fine - the goal is to first complete the bootstrap, and then add more features, which can then be used to decrease the size of the implementation.
318 lines
12 KiB
Plaintext
318 lines
12 KiB
Plaintext
// Types
|
|
// -----
|
|
|
|
//data Maybe
|
|
//= (Some value)
|
|
//| None
|
|
|
|
//data Bool
|
|
//= False
|
|
//| True
|
|
|
|
//data Pair
|
|
//= (Pair fst snd)
|
|
|
|
//data Term
|
|
//= (All nam inp bod)
|
|
//| (Lam nam bod)
|
|
//| (App fun arg)
|
|
//| (Ann val typ)
|
|
//| (Slf nam bod)
|
|
//| (Ins val)
|
|
//| (Ref nam val)
|
|
//| (Let nam val bod)
|
|
//| (Set)
|
|
//| (U60)
|
|
//| (Num val)
|
|
//| (Op2 opr fst snd)
|
|
//| (Txt txt)
|
|
//| (Hol nam ctx)
|
|
//| (Var nam idx)
|
|
|
|
// Prelude
|
|
// -------
|
|
|
|
(Debug dep [] value) = value
|
|
(Debug dep msg value) = (HVM.print (Join msg) value)
|
|
//(Debug dep [] value) = value
|
|
//(Debug dep msg value) = (If (> dep 10) 1 (HVM.print (Join msg) value))
|
|
|
|
(NewLine) = (String.cons 10 String.nil)
|
|
(Quote) = (String.cons 34 String.nil)
|
|
|
|
(And True b) = b
|
|
(And False b) = False
|
|
|
|
(Or True b) = True
|
|
(Or False b) = b
|
|
|
|
(If 0 t f) = f
|
|
(If 1 t f) = t
|
|
|
|
(When None some none) = none
|
|
(When (Some val) some none) = (some val)
|
|
|
|
(U60.show n) = (U60.show.go n String.nil)
|
|
|
|
(U60.show.go n res) = (U60.show.go.match (< n 10) n res)
|
|
|
|
(U60.show.go.match 0 n res) = (U60.show.go (/ n 10) (String.cons (+ '0' (% n 10)) res))
|
|
(U60.show.go.match i n res) = (String.cons (+ '0' n) res)
|
|
|
|
(Same String.nil String.nil) = 1
|
|
(Same String.nil (String.cons y ys)) = 0
|
|
(Same (String.cons x xs) String.nil) = 0
|
|
(Same (String.cons x xs) (String.cons y ys)) = (& (== x y) (Same xs ys))
|
|
|
|
(Find name List.nil) = None
|
|
(Find name (List.cons (Pair nam val) tail)) = (If (Same nam name) (Some val) (Find name tail))
|
|
|
|
(Concat String.nil ys) = ys
|
|
(Concat (String.cons x xs) ys) = (String.cons x (Concat xs ys))
|
|
|
|
(Join List.nil) = ""
|
|
(Join (List.cons x xs)) = (Concat x (Join xs))
|
|
|
|
(Fst (Pair fst snd)) = fst
|
|
(Snd (Pair fst snd)) = snd
|
|
|
|
(Get (Pair fst snd) fun) = (fun fst snd)
|
|
|
|
(Pure x) = (Some x)
|
|
|
|
(Bind a b) = (Bind.match a b)
|
|
|
|
(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 (Let nam val bod)) = (Reduce r (bod val))
|
|
(Reduce r (Op2 opr fst snd)) = (Reduce.op2 opr fst snd)
|
|
(Reduce 1 (Txt txt)) = (Reduce.txt txt)
|
|
(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 opr fst snd) = (Op2 opr fst snd)
|
|
|
|
(Reduce.txt (String.cons x xs)) = (Reduce 1 (App (App Book.String.cons (Num x)) (Txt xs)))
|
|
(Reduce.txt String.nil) = (Reduce 1 Book.String.nil)
|
|
(Reduce.txt val) = val
|
|
|
|
(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)))
|
|
(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 (Let nam val bod) dep) = (Let nam (Normal r val bod) λx(Normal r (bod (Var nam dep)) (+ 1 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 (Txt val) dep) = (Txt val)
|
|
(Normal.term r (Op2 opr fst snd) dep) = (Op2 opr (Normal.term r fst dep) (Normal.term r snd dep))
|
|
(Normal.term r (Var nam idx) dep) = (Var nam idx)
|
|
|
|
// Equality
|
|
// --------
|
|
|
|
// Check if two terms are identical. If not...
|
|
(Equal a b dep) = (Equal.minor (Identical a b dep) a b dep)
|
|
|
|
// Check if they're identical after a minor weak reduction. If not...
|
|
(Equal.minor 0 a b dep) = (Equal.major (Identical (Reduce 0 a) (Reduce 0 b) dep) a b dep)
|
|
(Equal.minor 1 a b dep) = 1
|
|
|
|
// Check if they're identical after a major weak reduction. If not...
|
|
(Equal.major 0 a b dep) = (Equal.enter (Identical (Reduce 1 a) (Reduce 1 b) dep) a b dep)
|
|
(Equal.major 1 a b dep) = 1
|
|
|
|
// Check if they become identical after reducing fields.
|
|
(Equal.enter 0 a b dep) = (Comparer λaλbλdep(Equal a b dep) a b dep)
|
|
(Equal.enter 1 a b dep) = 1
|
|
|
|
// Checks if two terms are identical, without reductions.
|
|
(Identical a b dep) = (Comparer λaλbλdep(Identical a b dep) a b dep)
|
|
|
|
// Generic comparer.
|
|
(Comparer rec (All a.nam a.inp a.bod) (All b.nam b.inp b.bod) dep) = (& (rec a.inp b.inp dep) (rec (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep)))
|
|
(Comparer rec (Lam a.nam a.bod) (Lam b.nam b.bod) dep) = (rec (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep))
|
|
(Comparer rec (App a.fun a.arg) (App b.fun b.arg) dep) = (& (rec a.fun b.fun dep) (rec a.arg b.arg dep))
|
|
(Comparer rec (Slf a.nam a.bod) (Slf b.nam b.bod) dep) = (rec (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep))
|
|
(Comparer rec (Ins a.val) b dep) = (rec a.val b dep)
|
|
(Comparer rec a (Ins b.val) dep) = (rec a b.val dep)
|
|
(Comparer rec (Ref a.nam a.val) (Ref b.nam b.val) dep) = (Same a.nam b.nam)
|
|
(Comparer rec (Let a.nam a.val a.bod) b dep) = (rec (a.bod a.val) b dep)
|
|
(Comparer rec a (Let b.nam b.val b.bod) dep) = (rec a (b.bod b.val) dep)
|
|
(Comparer rec Set Set dep) = 1
|
|
(Comparer rec (Var a.nam a.idx) (Var b.nam b.idx) dep) = (== a.idx b.idx)
|
|
(Comparer rec (Ann a.val a.typ) b dep) = (rec a.val b dep)
|
|
(Comparer rec a (Ann b.val b.typ) dep) = (rec a b.val dep)
|
|
(Comparer rec (Hol a.nam a.ctx) b dep) = (Debug dep ["Found: ?" a.nam " = " (Show b dep)] 1)
|
|
(Comparer rec a (Hol b.nam b.ctx) dep) = (Debug dep ["Found: ?" b.nam " = " (Show a dep)] 1)
|
|
(Comparer rec U60 U60 dep) = 1
|
|
(Comparer rec (Num a.val) (Num b.val) dep) = (== a.val b.val)
|
|
(Comparer rec (Txt a.txt) (Txt b.txt) dep) = (Same a.txt b.txt)
|
|
(Comparer rec (Op2 a.opr a.fst a.snd) (Op2 b.opr b.fst b.snd) dep) = (& (rec a.fst a.snd dep) (rec b.fst b.snd dep))
|
|
(Comparer rec a b dep) = 0
|
|
|
|
// Type-Checking
|
|
// -------------
|
|
|
|
(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) =
|
|
(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 nam bod) dep) =
|
|
(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 λfun λarg
|
|
(Bind (Check arg fun_ty.inp dep) λval_ty
|
|
(Pure (fun_ty.bod arg)))
|
|
λfun λarg
|
|
(Debug dep ["Error: NonFunApp " (Show (App fun arg) dep)] None))
|
|
fun arg))
|
|
(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 val) dep) =
|
|
(Bind (Infer val dep) λval_ty
|
|
((IfSlf (Reduce 1 val_ty)
|
|
λval_nam λval_ty.bod λval (Pure (val_ty.bod (Ins val)))
|
|
λval (Debug dep ["Error: NonSlfIns " (Show (Ins val) dep)] None))
|
|
val))
|
|
(Infer.match (Ref nam val) dep) =
|
|
(Infer val dep)
|
|
(Infer.match (Let nam val bod) dep) =
|
|
(Debug dep ["Error: NonAnnLet " (Show (Let nam val bod) dep)] (None))
|
|
(Infer.match Set dep) =
|
|
(Pure Set)
|
|
(Infer.match U60 dep) =
|
|
(Pure Set)
|
|
(Infer.match (Num num) dep) =
|
|
(Pure U60)
|
|
(Infer.match (Txt txt) dep) =
|
|
(Pure Book.String)
|
|
(Infer.match (Op2 opr fst snd) dep) =
|
|
(Bind (Check fst U60 dep) λfst
|
|
(Bind (Check snd U60 dep) λsnd
|
|
(Pure U60)))
|
|
(Infer.match (Hol nam ctx) dep) =
|
|
(Debug dep ["Error: NonAnnHol " (Show (Hol nam ctx) dep)] None)
|
|
(Infer.match (Var nam idx) dep) =
|
|
(Debug dep ["Error: NonAnnVar " (Show (Var nam idx) dep)] None)
|
|
|
|
//(Check term type dep) = (Debug dep ["Check: " (Show term dep) " :: " (Show (Reduce 0 type) dep)] (Check.match term type dep))
|
|
(Check term type dep) = (Check.match term type dep)
|
|
|
|
(Check.match (Lam term.nam term.bod) type dep) =
|
|
((IfAll (Reduce 1 type) λtype.nam λtype.inp λtype.bod λterm.bod
|
|
let ann = (Ann (Var term.nam dep) type.inp)
|
|
let term = (term.bod ann)
|
|
let type = (type.bod ann)
|
|
(Check term type (+ dep 1))
|
|
λterm.bod
|
|
(Infer (Lam term.nam term.bod) dep))
|
|
term.bod)
|
|
(Check.match (Ins term.val) type dep) =
|
|
(IfSlf (Reduce 1 type) λtype.nam λtype.bod
|
|
(Check term.val (type.bod (Ins term.val)) dep)
|
|
(Infer (Ins term.val) dep))
|
|
(Check.match (Let term.nam term.val term.bod) type dep) =
|
|
(Check (term.bod term.val) type (+ 1 dep))
|
|
(Check.match (Ref term.nam term.val) type dep) =
|
|
(Check term.val type dep)
|
|
(Check.match (Hol term.nam term.ctx) type dep) =
|
|
(Debug dep ["HOLE!: ?" term.nam " :: " (Show (Normal 0 type dep) dep) (Context.show term.ctx dep)]
|
|
(Pure 0))
|
|
(Check.match term type dep) =
|
|
(Bind (Infer term dep) λinfer
|
|
(Check.report (Equal type infer dep) infer type term dep))
|
|
|
|
(Check.report 0 inferred expected value dep) =
|
|
let inf = (Show (Normal 0 inferred dep) dep)
|
|
let exp = (Show (Normal 0 expected dep) dep)
|
|
let val = (Show (Normal 0 value dep) dep)
|
|
(Debug dep ["Error: " inf NewLine " != " exp NewLine " in " val] None)
|
|
(Check.report n inferred expected value dep) =
|
|
(Pure 0)
|
|
|
|
// Syntax
|
|
// ------
|
|
|
|
(Show (All nam inp bod) dep) = (Join ["∀(" nam ": " (Show inp dep) ") " (Show (bod (Var nam dep)) (+ dep 1))])
|
|
(Show (Lam nam bod) dep) = (Join ["λ" nam " " (Show (bod (Var nam dep)) (+ dep 1))])
|
|
(Show (App fun arg) dep) = (Join ["(" (Show.prune (Show fun dep)) " " (Show arg dep) ")"])
|
|
(Show (Ann val typ) dep) = (Join ["{" (Show val dep) ": " (Show typ dep) "}"])
|
|
(Show (Slf nam bod) dep) = (Join ["$" nam " " (Show (bod (Var nam dep)) (+ dep 1))])
|
|
(Show (Ins val) dep) = (Join ["~" (Show val dep)])
|
|
(Show (Ref nam val) dep) = nam
|
|
(Show (Let nam val bod) dep) = (Join ["let " nam " = " (Show val dep) "; " (Show (bod (Var nam dep)) (+ dep 1))])
|
|
(Show Set dep) = (Join ["*"])
|
|
(Show U60 dep) = "#U60"
|
|
(Show (Num val) dep) = (Join ["#" (U60.show val)])
|
|
(Show (Op2 opr fst snd) dep) = (Join ["#(" (Op2.show opr) " " (Show fst dep) " " (Show snd dep) ")"])
|
|
(Show (Txt txt) dep) = (Join [Quote txt Quote])
|
|
(Show (Hol nam ctx) dep) = (Join ["?" nam])
|
|
(Show (Var nam idx) dep) = (Join [nam "'" (U60.show idx)])
|
|
|
|
(Show.prune (String.cons '(' xs)) = (Show.begin xs)
|
|
(Show.prune str) = str
|
|
|
|
(Show.begin (String.cons x (String.cons y String.nil))) = (String.cons x String.nil)
|
|
(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)])
|
|
|
|
(Context.show.ann (Ann val typ) dep) = (Join ["{" (Show (Normal 0 val dep) dep) ": " (Show (Normal 0 typ dep) dep) "}"])
|
|
(Context.show.ann term dep) = (Show (Normal 0 term dep) dep)
|
|
|
|
// API
|
|
// ---
|
|
|
|
(Normalizer (Ref nam val)) = (Normalizer val)
|
|
(Normalizer (Ann val typ)) = (Normalizer val)
|
|
(Normalizer val) = (HVM.print (Show (Normal 1 val 0) 0) OK)
|
|
|
|
(Checker (Ref nam val)) = (Checker val)
|
|
(Checker (Ann val typ)) = (Checker.report (Check val typ 0))
|
|
(Checker val) = (HVM.print "Untyped." OK)
|
|
|
|
(Checker.report (Some x)) = (HVM.print "Check!" OK)
|
|
(Checker.report None) = (HVM.print "Error." ERR)
|