2024-02-08 19:51:51 +03:00
// Types
// -----
//data Maybe
//= (Some value)
//| None
//data Bool
//= False
//| True
//data Pair
//= (Pair fst snd)
//data Term
2024-02-08 23:47:51 +03:00
//= (All nam inp bod)
//| (Lam nam bod)
2024-02-08 19:51:51 +03:00
//| (App fun arg)
//| (Ann val typ)
2024-02-08 23:47:51 +03:00
//| (Slf nam bod)
2024-02-08 19:51:51 +03:00
//| (Ins val)
//| (Ref nam val)
2024-02-10 18:25:48 +03:00
//| (Let nam val bod)
2024-02-08 19:51:51 +03:00
//| (Set)
2024-02-10 18:25:48 +03:00
//| (U60)
//| (Num val)
2024-02-11 05:15:08 +03:00
//| (Op2 opr fst snd)
2024-02-13 02:15:50 +03:00
//| (Mat nam x z s p)
2024-02-10 18:25:48 +03:00
//| (Txt txt)
2024-02-19 00:55:09 +03:00
//| (Hol nam ctx val)
2024-02-08 23:47:51 +03:00
//| (Var nam idx)
2024-02-08 19:51:51 +03:00
// Prelude
// -------
2024-02-10 18:25:48 +03:00
(Debug dep [] value) = value
(Debug dep msg value) = (HVM.print (Join msg) value)
2024-02-11 00:34:04 +03:00
//(Debug dep [] value) = value
//(Debug dep msg value) = (If (> dep 10) 1 (HVM.print (Join msg) value))
2024-02-08 23:47:51 +03:00
(NewLine) = (String.cons 10 String.nil)
2024-02-10 18:25:48 +03:00
(Quote) = (String.cons 34 String.nil)
2024-02-08 19:51:51 +03:00
(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)
2024-02-13 02:15:50 +03:00
(U60.show n) = (U60.show.go n String.nil)
(U60.show.go n res) = (U60.show.go.match (< n 10) n res)
2024-02-08 19:51:51 +03:00
(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)
2024-02-13 02:15:50 +03:00
(U60.name n) = (U60.name.go (+ n 1))
(U60.name.go 0) = ""
(U60.name.go n) = (String.cons (+ 97 (% (- n 1) 26)) (U60.name.go (/ (- n 1) 26)))
2024-02-08 19:51:51 +03:00
(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)
2024-02-10 15:20:22 +03:00
(Pure x) = (Some x)
2024-02-08 19:51:51 +03:00
2024-02-10 15:20:22 +03:00
(Bind a b) = (Bind.match a b)
2024-02-08 19:51:51 +03:00
2024-02-10 15:20:22 +03:00
(Bind.match None b) = None
(Bind.match (Some a) b) = (b a)
2024-02-08 19:51:51 +03:00
// Evaluation
// ----------
2024-02-10 15:20:22 +03:00
(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)
2024-02-10 18:25:48 +03:00
(Reduce r (Let nam val bod)) = (Reduce r (bod val))
2024-02-13 02:15:50 +03:00
(Reduce r (Op2 opr fst snd)) = (Reduce.op2 r opr fst snd)
(Reduce r (Mat nam x z s p)) = (Reduce.mat r nam x z s p)
(Reduce 1 (Txt txt)) = (Reduce.txt 1 txt)
2024-02-10 15:20:22 +03:00
(Reduce r val) = val
2024-02-08 19:51:51 +03:00
2024-02-19 00:55:09 +03:00
(Reduce.app r (Lam nam bod) arg) = (Reduce r (bod (Reduce r arg)))
//(Reduce.app r (Hol nam ctx ars) arg) = (Hol nam ctx (List.cons arg ars))
(Reduce.app r fun arg) = (App fun arg)
2024-02-08 19:51:51 +03:00
2024-02-13 02:15:50 +03:00
(Reduce.op2 r ADD (Num fst) (Num snd)) = (Num (+ fst snd))
(Reduce.op2 r SUB (Num fst) (Num snd)) = (Num (- fst snd))
(Reduce.op2 r MUL (Num fst) (Num snd)) = (Num (* fst snd))
(Reduce.op2 r DIV (Num fst) (Num snd)) = (Num (/ fst snd))
(Reduce.op2 r MOD (Num fst) (Num snd)) = (Num (% fst snd))
(Reduce.op2 r EQ (Num fst) (Num snd)) = (Num (== fst snd))
(Reduce.op2 r NE (Num fst) (Num snd)) = (Num (!= fst snd))
(Reduce.op2 r LT (Num fst) (Num snd)) = (Num (< fst snd))
(Reduce.op2 r GT (Num fst) (Num snd)) = (Num (> fst snd))
(Reduce.op2 r LTE (Num fst) (Num snd)) = (Num (<= fst snd))
(Reduce.op2 r GTE (Num fst) (Num snd)) = (Num (>= fst snd))
(Reduce.op2 r AND (Num fst) (Num snd)) = (Num (& fst snd))
(Reduce.op2 r OR (Num fst) (Num snd)) = (Num (| fst snd))
(Reduce.op2 r XOR (Num fst) (Num snd)) = (Num (^ fst snd))
(Reduce.op2 r LSH (Num fst) (Num snd)) = (Num (<< fst snd))
(Reduce.op2 r RSH (Num fst) (Num snd)) = (Num (>> fst snd))
(Reduce.op2 r opr fst snd) = (Op2 opr fst snd)
(Reduce.mat r nam (Num 0) z s p) = (Reduce r z)
(Reduce.mat r nam (Num n) z s p) = (Reduce r (s (Num (- n 1))))
(Reduce.mat r nam val z s p) = (Mat nam val z s p)
(Reduce.txt r (String.cons x xs)) = (Reduce 1 (App (App Book.String.cons (Num x)) (Txt xs)))
(Reduce.txt r String.nil) = (Reduce 1 Book.String.nil)
(Reduce.txt r val) = val
2024-02-10 18:25:48 +03:00
2024-02-08 21:47:43 +03:00
(Normal r term dep) = (Normal.term r (Reduce r term) dep)
2024-02-08 19:51:51 +03:00
2024-02-13 02:15:50 +03:00
(Normal.term r (All nam inp bod) dep) = (All nam (Normal r inp dep) λx(Normal r (bod (Var nam dep)) (+ dep 1)))
2024-02-08 23:47:51 +03:00
(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))
2024-02-13 02:15:50 +03:00
(Normal.term r (Slf nam bod) dep) = (Slf nam λx(Normal r (bod (Var nam dep)) (+ 1 dep)))
2024-02-08 23:47:51 +03:00
(Normal.term r (Ins val) dep) = (Ins (Normal r val dep))
(Normal.term r (Ref nam val) dep) = (Ref nam (Normal r val dep))
2024-02-10 18:25:48 +03:00
(Normal.term r (Let nam val bod) dep) = (Let nam (Normal r val bod) λx(Normal r (bod (Var nam dep)) (+ 1 dep)))
2024-02-08 23:47:51 +03:00
(Normal.term r (Hol nam ctx) dep) = (Hol nam ctx)
(Normal.term r Set dep) = Set
2024-02-10 15:20:22 +03:00
(Normal.term r U60 dep) = U60
(Normal.term r (Num val) dep) = (Num val)
2024-02-10 18:25:48 +03:00
(Normal.term r (Txt val) dep) = (Txt val)
2024-02-11 05:15:08 +03:00
(Normal.term r (Op2 opr fst snd) dep) = (Op2 opr (Normal.term r fst dep) (Normal.term r snd dep))
2024-02-13 02:15:50 +03:00
(Normal.term r (Mat nam x z s p) dep) = (Mat nam (Normal r x dep) (Normal r z dep) λk(Normal r (s (Var (Concat nam "-1") dep)) dep) λk(Normal r (p (Var nam dep)) dep))
2024-02-08 23:47:51 +03:00
(Normal.term r (Var nam idx) dep) = (Var nam idx)
2024-02-08 19:51:51 +03:00
// Equality
// --------
2024-02-11 00:34:04 +03:00
// Check if two terms are identical. If not...
2024-02-19 00:55:09 +03:00
(Equal a b dep) = (Equal.unify.a a λx(x) b dep)
//(Equal a b dep) = (Equal.minor (Identical a b dep) a b dep)
// ...
(Equal.unify.a (App a.fun a.arg) as b dep) = (Equal.unify.a a.fun λk(as (App k a.arg)) b dep)
(Equal.unify.a (Hol a.nam a.ctx) as b dep) = (Debug dep ["Found: ?" a.nam " = " (Show b dep)] 1)
(Equal.unify.a a as b dep) = (Equal.unify.b (as a) b λx(x) dep)
// ...
(Equal.unify.b a (App b.fun b.arg) bs dep) = (Equal.unify.b a b.fun λk(bs (App k b.arg)) dep)
(Equal.unify.b a (Hol b.nam b.ctx) bs dep) = (Debug dep ["Found: ?" b.nam " = " (Show a dep)] 1)
(Equal.unify.b a b bs dep) = let b = (bs b); (Equal.minor (Identical a b dep) a b dep)
2024-02-11 00:34:04 +03:00
// 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.
2024-02-11 05:15:08 +03:00
(Equal.enter 0 a b dep) = (Comparer λaλbλdep(Equal a b dep) a b dep)
(Equal.enter 1 a b dep) = 1
2024-02-11 00:34:04 +03:00
// Checks if two terms are identical, without reductions.
2024-02-11 05:15:08 +03:00
(Identical a b dep) = (Comparer λaλbλdep(Identical a b dep) a b dep)
// Generic comparer.
2024-02-13 02:15:50 +03:00
(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)
2024-02-19 00:55:09 +03:00
(Comparer rec (Hol a.nam a.ctx) (Hol b.nam b.ctx) dep) = (Same a.nam b.nam)
2024-02-13 02:15:50 +03:00
(Comparer rec U60 U60 dep) = 1
(Comparer rec (Num a.val) (Num b.val) dep) = (== a.val b.val)
(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 (Mat a.nam a.x a.z a.s a.p) (Mat b.nam b.x b.z b.s b.p) dep) = (& (rec a.x b.x dep) (& (rec a.z b.z dep) (& (rec (a.s (Var (Concat a.nam "-1") dep)) (b.s (Var (Concat b.nam "-1") dep)) dep) (rec (a.p (Var a.nam dep)) (b.p (Var b.nam dep)) dep))))
(Comparer rec (Txt a.txt) (Txt b.txt) dep) = (Same a.txt b.txt)
(Comparer rec a b dep) = 0
2024-02-08 19:51:51 +03:00
// Type-Checking
// -------------
2024-02-10 15:20:22 +03:00
(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
2024-02-11 00:34:04 +03:00
//(Infer term dep) = (Debug dep ["Infer: " (Show term dep)] (Infer.match term dep))
(Infer term dep) = (Infer.match term dep)
2024-02-08 19:51:51 +03:00
2024-02-08 23:47:51 +03:00
(Infer.match (All nam inp bod) dep) =
2024-02-13 02:15:50 +03:00
(Bind (Check inp Set dep) λinp_typ
(Bind (Check (bod (Ann (Var nam dep) inp)) Set (+ 1 dep)) λbod_typ
2024-02-08 19:51:51 +03:00
(Pure Set)))
2024-02-08 23:47:51 +03:00
(Infer.match (Lam nam bod) dep) =
2024-02-10 15:20:22 +03:00
(Debug dep ["Error: NonFunLam " (Show (Lam nam bod) dep)] (None))
2024-02-08 23:47:51 +03:00
(Infer.match (App fun arg) dep) =
2024-02-13 02:15:50 +03:00
(Bind (Infer fun dep) λfun_typ
((IfAll (Reduce 1 fun_typ)
λfun_nam λfun_typ.inp λfun_typ.bod λfun λarg
(Bind (Check arg fun_typ.inp dep) λval_typ
(Pure (fun_typ.bod arg)))
2024-02-11 00:34:04 +03:00
λfun λarg
(Debug dep ["Error: NonFunApp " (Show (App fun arg) dep)] None))
fun arg))
2024-02-08 23:47:51 +03:00
(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
2024-02-08 19:51:51 +03:00
(Pure Set))
2024-02-08 23:47:51 +03:00
(Infer.match (Ins val) dep) =
2024-02-13 02:15:50 +03:00
(Bind (Infer val dep) λval_typ
((IfSlf (Reduce 1 val_typ)
λval_nam λval_typ.bod λval (Pure (val_typ.bod (Ins val)))
2024-02-11 00:34:04 +03:00
λval (Debug dep ["Error: NonSlfIns " (Show (Ins val) dep)] None))
val))
2024-02-08 23:47:51 +03:00
(Infer.match (Ref nam val) dep) =
(Infer val dep)
2024-02-10 18:25:48 +03:00
(Infer.match (Let nam val bod) dep) =
(Debug dep ["Error: NonAnnLet " (Show (Let nam val bod) dep)] (None))
2024-02-08 19:51:51 +03:00
(Infer.match Set dep) =
(Pure Set)
2024-02-10 15:20:22 +03:00
(Infer.match U60 dep) =
(Pure Set)
(Infer.match (Num num) dep) =
(Pure U60)
2024-02-10 18:25:48 +03:00
(Infer.match (Txt txt) dep) =
(Pure Book.String)
2024-02-11 05:15:08 +03:00
(Infer.match (Op2 opr fst snd) dep) =
2024-02-10 15:20:22 +03:00
(Bind (Check fst U60 dep) λfst
(Bind (Check snd U60 dep) λsnd
(Pure U60)))
2024-02-13 02:15:50 +03:00
// x : U60
// p : ∀(x: U60) *
// z : (p 0)
// s : ∀(x-1 : U60) (p (+ 1 x-1))
// ------------------------------
// (Mat nam x z s p) : (p x)
(Infer.match (Mat nam x z s p) dep) =
(Bind (Check x U60 dep) λx_typ
(Bind (Check (p (Ann (Var nam dep) U60)) Set dep) λp_typ
(Bind (Check z (p (Num 0)) dep) λz_typ
(Bind (Check (s (Ann (Var (Concat nam "-1") dep) U60)) (p (Op2 ADD (Num 1) (Var (Concat nam "-1") dep))) (+ dep 1)) λs_typ
(Pure (p x))))))
2024-02-09 01:01:46 +03:00
(Infer.match (Hol nam ctx) dep) =
2024-02-10 15:20:22 +03:00
(Debug dep ["Error: NonAnnHol " (Show (Hol nam ctx) dep)] None)
2024-02-08 23:47:51 +03:00
(Infer.match (Var nam idx) dep) =
2024-02-10 15:20:22 +03:00
(Debug dep ["Error: NonAnnVar " (Show (Var nam idx) dep)] None)
2024-02-08 19:51:51 +03:00
2024-02-12 02:14:37 +03:00
//(Check term type dep) = (Debug dep ["Check: " (Show term dep) " :: " (Show type dep)] (Check.match term type dep))
2024-02-11 00:34:04 +03:00
(Check term type dep) = (Check.match term type dep)
2024-02-09 02:01:37 +03:00
(Check.match (Lam term.nam term.bod) type dep) =
2024-02-12 02:14:37 +03:00
((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)
2024-02-09 02:01:37 +03:00
(Check.match (Ins term.val) type dep) =
2024-02-12 02:14:37 +03:00
((IfSlf (Reduce 1 type)
λtype.nam λtype.bod λterm.val (Check term.val (type.bod (Ins term.val)) dep)
λterm.val (Infer (Ins term.val) dep))
term.val)
2024-02-10 18:25:48 +03:00
(Check.match (Let term.nam term.val term.bod) type dep) =
(Check (term.bod term.val) type (+ 1 dep))
2024-02-08 23:47:51 +03:00
(Check.match (Hol term.nam term.ctx) type dep) =
2024-02-10 15:20:22 +03:00
(Debug dep ["HOLE!: ?" term.nam " :: " (Show (Normal 0 type dep) dep) (Context.show term.ctx dep)]
2024-02-08 23:47:51 +03:00
(Pure 0))
2024-02-12 02:14:37 +03:00
(Check.match (Ref term.nam (Ann term.val term.typ)) type dep) = // better printing
(Check.report (Equal type term.typ dep) term.typ type (Ref term.nam term.val) dep)
//(Check.match (Ref term.nam term.val) type dep) =
//(Check term.val type dep)
2024-02-11 00:34:04 +03:00
(Check.match term type dep) =
2024-02-12 02:14:37 +03:00
(Check.verify term type dep)
(Check.verify term type dep) =
2024-02-11 00:34:04 +03:00
(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)
2024-02-08 19:51:51 +03:00
// Syntax
// ------
2024-02-11 00:34:04 +03:00
(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)])
2024-02-11 05:15:08 +03:00
(Show (Op2 opr fst snd) dep) = (Join ["#(" (Op2.show opr) " " (Show fst dep) " " (Show snd dep) ")"])
2024-02-13 02:15:50 +03:00
(Show (Mat nam x z s p) dep) = (Join ["match " nam " = " (Show x dep) " { #0 => " (Show z dep) "; #+ => " (Show (s (Var (Concat nam "-1") dep)) (+ dep 1)) " }: " (Show (p (Var nam dep)) dep)])
2024-02-11 00:34:04 +03:00
(Show (Txt txt) dep) = (Join [Quote txt Quote])
(Show (Hol nam ctx) dep) = (Join ["?" nam])
2024-02-12 02:14:37 +03:00
(Show (Var nam idx) dep) = (Join [nam])
//(Show (Var nam idx) dep) = (Join [nam "'" (U60.show idx)])
2024-02-08 23:47:51 +03:00
2024-02-19 00:55:09 +03:00
(Show.many List.nil dep) = ""
(Show.many (List.cons x xs) dep) = (Join [" " (Show x dep) (Show.many xs dep)])
(Show.trim (String.cons ' ' xs)) = xs
(Show.trim str) = str
2024-02-09 01:01:46 +03:00
(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
2024-02-10 15:20:22 +03:00
(Op2.show ADD) = "+"
(Op2.show SUB) = "-"
(Op2.show MUL) = "*"
(Op2.show DIV) = "/"
2024-02-08 23:47:51 +03:00
(Context.show List.nil dep) = ""
2024-02-09 01:01:46 +03:00
(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)
2024-02-08 19:51:51 +03:00
2024-02-12 23:18:29 +03:00
// Compilation
// -----------
(Compile (All nam inp bod)) = 0
(Compile (Lam nam bod)) = λx(Compile (bod (Var "" x)))
(Compile (App fun arg)) = ((Compile fun) (Compile arg))
(Compile (Ann val typ)) = (Compile val)
(Compile (Slf nam bod)) = 0
(Compile (Ins val)) = (Compile val)
(Compile (Ref nam val)) = (Compile val)
(Compile (Let nam val bod)) = (Compile (bod val))
(Compile Set) = 0
(Compile U60) = 0
(Compile (Num val)) = val
(Compile (Op2 opr fst snd)) = (Compile.op2 opr (Compile fst) (Compile snd))
2024-02-13 02:15:50 +03:00
(Compile (Mat nam x z s p)) = (Compile.mat (Compile x) (Compile z) λx(Compile (s (Var "" x))))
2024-02-12 23:18:29 +03:00
(Compile (Txt txt)) = (Compile (Compile.txt txt))
(Compile (Hol nam ctx)) = 0
(Compile (Var nam val)) = val
(Compile.txt (String.cons x xs)) = (App (App Book.String.cons (Num x)) (Compile.txt xs))
(Compile.txt String.nil) = Book.String.nil
(Compile.op2 ADD fst snd) = (+ fst snd)
(Compile.op2 SUB fst snd) = (- fst snd)
(Compile.op2 MUL fst snd) = (* fst snd)
(Compile.op2 DIV fst snd) = (/ fst snd)
2024-02-13 02:15:50 +03:00
(Compile.op2 MOD fst snd) = (% fst snd)
(Compile.op2 EQ fst snd) = (== fst snd)
(Compile.op2 NE fst snd) = (!= fst snd)
(Compile.op2 LT fst snd) = (< fst snd)
(Compile.op2 GT fst snd) = (> fst snd)
(Compile.op2 LTE fst snd) = (<= fst snd)
(Compile.op2 GTE fst snd) = (>= fst snd)
(Compile.op2 AND fst snd) = (& fst snd)
(Compile.op2 OR fst snd) = (| fst snd)
(Compile.op2 XOR fst snd) = (^ fst snd)
(Compile.op2 LSH fst snd) = (<< fst snd)
(Compile.op2 RSH fst snd) = (>> fst snd)
(Compile.mat 0 z s) = z
(Compile.mat n z s) = (s (- n 1))
2024-02-12 23:18:29 +03:00
2024-02-08 19:51:51 +03:00
// API
// ---
2024-02-12 23:18:29 +03:00
(Read str) = (str 0 λheadλtail(String.cons head (Read tail)) String.nil)
2024-02-10 18:25:48 +03:00
(Normalizer (Ref nam val)) = (Normalizer val)
(Normalizer (Ann val typ)) = (Normalizer val)
2024-02-19 21:27:32 +03:00
(Normalizer val) = (Read (Compile val)) // compiles to native and reads as string
//(Normalizer val) = ((Compile val)) // compiles to native and show it
2024-02-19 21:16:21 +03:00
//(Normalizer val) = (Normal 1 val 1) // uses the normalizer function
2024-02-09 02:01:37 +03:00
2024-02-08 19:51:51 +03:00
(Checker (Ref nam val)) = (Checker val)
2024-02-08 23:47:51 +03:00
(Checker (Ann val typ)) = (Checker.report (Check val typ 0))
2024-02-19 00:55:09 +03:00
(Checker val) = (Checker.report (Infer val 0))
2024-02-08 19:51:51 +03:00
2024-02-09 02:01:37 +03:00
(Checker.report (Some x)) = (HVM.print "Check!" OK)
(Checker.report None) = (HVM.print "Error." ERR)
2024-02-13 02:15:50 +03:00