mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-08-16 21:30:32 +03:00
249 lines
9.6 KiB
Plaintext
249 lines
9.6 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)
|
|
//| (Set)
|
|
//| (Hol nam ctx)
|
|
//| (Var nam idx)
|
|
|
|
// Prelude
|
|
// -------
|
|
|
|
//(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
|
|
|
|
(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)
|
|
|
|
// Term
|
|
// ----
|
|
|
|
(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
|
|
|
|
// 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.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 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) = (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)))
|
|
|
|
(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) = (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 (App a.fun a.arg) b dep) = (Compare.app.l (Reduce 1 (App a.fun a.arg)) b dep)
|
|
//(Compare a (App b.fun b.arg) dep) = (Compare.app.r a (Reduce 1 (App b.fun b.arg)) dep)
|
|
//(Compare (Lam a.nam a.bod) b dep) = (Compare (Lam a.nam a.bod) (Lam a.nam λx(App b x)) dep)
|
|
//(Compare a (Lam b.nam b.bod) dep) = (Compare (Lam b.nam λx(App a x)) (Lam b.nam b.bod) 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))
|
|
(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 ["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)))
|
|
(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 (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 (Hol nam ctx) dep) =
|
|
(Debug ["Error: NonAnnHol " (Show (Hol nam ctx) 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 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
|
|
let ann = (Ann (Var term.nam dep) type.inp)
|
|
let term = (term.bod ann)
|
|
let type = (type.bod ann)
|
|
(Check term type (+ dep 1))
|
|
(Infer (Lam term.nam term.bod) dep))
|
|
(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 (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)]
|
|
(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)))
|
|
|
|
// Syntax
|
|
// ------
|
|
|
|
(Show term dep) = (Show.match term dep)
|
|
|
|
(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.prune (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
|
|
|
|
(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
|
|
|
|
(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 term) = (HVM.print (Show (Normal 1 term 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)
|