HigherOrderCO/Kind
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind.git synced 2024-09-11 17:56:48 +03:00
Code Issues Packages Projects Releases Wiki Activity
9a6ffc9a81
Kind/book/.check.hvm1
Victor Taelin 9a6ffc9a81 fix txt reducer
2024-02-25 21:17:09 -03:00

496 lines
26 KiB
Plaintext
Raw Blame History

// 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 typ bod)
//| (Ins val)
//| (Ref nam val)
//| (Let nam val bod)
//| (Set)
//| (U60)
//| (Num val)
//| (Op2 opr fst snd)
//| (Mat nam x z s p)
//| (Txt txt)
//| (Hol nam ctx val)
//| (Var nam idx)
//| (Src src val)
// Prelude
// -------
(Debug dep [] value) = value
(Debug dep msg value) = (HVM.print (String.join msg) value)
//(Debug dep [] value) = value
//(Debug dep msg value) = (If (> dep 10) 1 (HVM.print (String.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)
(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)))
(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))
(String.concat String.nil ys) = ys
(String.concat (String.cons x xs) ys) = (String.cons x (String.concat xs ys))
(String.join List.nil) = ""
(String.join (List.cons x xs)) = (String.concat x (String.join xs))
(Pair.fst (Pair fst snd)) = fst
(Pair.snd (Pair fst snd)) = snd
(Pair.get (Pair fst snd) fun) = (fun fst snd)
(Maybe.pure x) = (Some x)
(Maybe.bind a b) = (Maybe.bind.match a b)
(Maybe.bind.match None b) = None
(Maybe.bind.match (Some a) b) = (b a)
(String.color RESET) = (String.cons 27 "[0m")
(String.color BRIGHT) = (String.cons 27 "[1m")
(String.color DIM) = (String.cons 27 "[2m")
(String.color UNDERSCORE) = (String.cons 27 "[4m")
(String.color BLINK) = (String.cons 27 "[5m")
(String.color REVERSE) = (String.cons 27 "[7m")
(String.color HIDDEN) = (String.cons 27 "[8m")
(String.color BLACK) = (String.cons 27 "[30m")
(String.color RED) = (String.cons 27 "[31m")
(String.color GREEN) = (String.cons 27 "[32m")
(String.color YELLOW) = (String.cons 27 "[33m")
(String.color BLUE) = (String.cons 27 "[34m")
(String.color MAGENTA) = (String.cons 27 "[35m")
(String.color CYAN) = (String.cons 27 "[36m")
(String.color WHITE) = (String.cons 27 "[37m")
(String.color GRAY) = (String.cons 27 "[90m")
(String.color BG_BLACK) = (String.cons 27 "[40m")
(String.color BG_RED) = (String.cons 27 "[41m")
(String.color BG_GREEN) = (String.cons 27 "[42m")
(String.color BG_YELLOW) = (String.cons 27 "[43m")
(String.color BG_BLUE) = (String.cons 27 "[44m")
(String.color BG_MAGENTA) = (String.cons 27 "[45m")
(String.color BG_CYAN) = (String.cons 27 "[46m")
(String.color BG_WHITE) = (String.cons 27 "[47m")
(String.color BG_GRAY) = (String.cons 27 "[100m")
(String.color x) = "?"
// Evaluation
// ----------
(Reduce lv (App fun arg)) = (Reduce.app lv (Reduce lv fun) arg)
(Reduce lv (Ann val typ)) = (Reduce lv val)
(Reduce lv (Ins val)) = (Reduce lv val)
(Reduce lv (Ref nam val)) = (Reduce.ref lv nam (Reduce lv val))
(Reduce lv (Let nam val bod)) = (Reduce lv (bod val))
(Reduce lv (Op2 opr fst snd)) = (Reduce.op2 lv opr (Reduce lv fst) (Reduce lv snd))
(Reduce lv (Mat nam x z s p)) = (Reduce.mat lv nam (Reduce lv x) z s p)
(Reduce lv (Txt txt)) = (Reduce.txt lv txt)
(Reduce lv (Src src val)) = (Reduce lv val)
(Reduce lv val) = val
(Reduce.app lv (Lam nam bod) arg) = (Reduce lv (bod (Reduce 0 arg)))
(Reduce.app lv fun arg) = (App fun arg)
(Reduce.op2 lv ADD (Num fst) (Num snd)) = (Num (+ fst snd))
(Reduce.op2 lv SUB (Num fst) (Num snd)) = (Num (- fst snd))
(Reduce.op2 lv MUL (Num fst) (Num snd)) = (Num (* fst snd))
(Reduce.op2 lv DIV (Num fst) (Num snd)) = (Num (/ fst snd))
(Reduce.op2 lv MOD (Num fst) (Num snd)) = (Num (% fst snd))
(Reduce.op2 lv EQ (Num fst) (Num snd)) = (Num (== fst snd))
(Reduce.op2 lv NE (Num fst) (Num snd)) = (Num (!= fst snd))
(Reduce.op2 lv LT (Num fst) (Num snd)) = (Num (< fst snd))
(Reduce.op2 lv GT (Num fst) (Num snd)) = (Num (> fst snd))
(Reduce.op2 lv LTE (Num fst) (Num snd)) = (Num (<= fst snd))
(Reduce.op2 lv GTE (Num fst) (Num snd)) = (Num (>= fst snd))
(Reduce.op2 lv AND (Num fst) (Num snd)) = (Num (& fst snd))
(Reduce.op2 lv OR (Num fst) (Num snd)) = (Num (| fst snd))
(Reduce.op2 lv XOR (Num fst) (Num snd)) = (Num (^ fst snd))
(Reduce.op2 lv LSH (Num fst) (Num snd)) = (Num (<< fst snd))
(Reduce.op2 lv RSH (Num fst) (Num snd)) = (Num (>> fst snd))
(Reduce.op2 lv opr fst snd) = (Op2 opr fst snd)
(Reduce.mat lv nam (Num 0) z s p) = (Reduce lv z)
(Reduce.mat lv nam (Num n) z s p) = (Reduce lv (s (Num (- n 1))))
(Reduce.mat lv nam (Op2 ADD (Num 1) k) z s p) = (Reduce lv (s k))
(Reduce.mat lv nam val z s p) = (Mat nam val z s p)
(Reduce.ref 1 nam val) = (Reduce 1 val)
(Reduce.ref 2 nam val) = (Reduce 2 val)
(Reduce.ref lv nam val) = (Ref nam val)
(Reduce.txt lv (String.cons x xs)) = (Reduce lv (App (App Book.String.cons (Num x)) (Txt xs)))
(Reduce.txt lv String.nil) = (Reduce lv Book.String.nil)
(Reduce.txt lv val) = (Txt val)
(Normal lv term dep) = (Normal.term lv (Reduce lv term) dep)
(Normal.term lv (All nam inp bod) dep) = (All nam (Normal lv inp dep) λx(Normal lv (bod (Var nam dep)) (+ dep 1)))
(Normal.term lv (Lam nam bod) dep) = (Lam nam λx(Normal lv (bod (Var nam dep)) (+ 1 dep)))
(Normal.term lv (App fun arg) dep) = (App (Normal lv fun dep) (Normal lv arg dep))
(Normal.term lv (Ann val typ) dep) = (Ann (Normal lv val dep) (Normal lv typ dep))
(Normal.term lv (Slf nam typ bod) dep) = (Slf nam typ λx(Normal lv (bod (Var nam dep)) (+ 1 dep)))
(Normal.term lv (Ins val) dep) = (Ins (Normal lv val dep))
(Normal.term lv (Ref nam val) dep) = (Ref nam (Normal lv val dep))
(Normal.term lv (Let nam val bod) dep) = (Let nam (Normal lv val bod) λx(Normal lv (bod (Var nam dep)) (+ 1 dep)))
(Normal.term lv (Hol nam ctx) dep) = (Hol nam ctx)
(Normal.term lv Set dep) = Set
(Normal.term lv U60 dep) = U60
(Normal.term lv (Num val) dep) = (Num val)
(Normal.term lv (Op2 opr fst snd) dep) = (Op2 opr (Normal.term lv fst dep) (Normal.term lv snd dep))
(Normal.term lv (Mat nam x z s p) dep) = (Mat nam (Normal lv x dep) (Normal lv z dep) λk(Normal lv (s (Var (String.concat nam "-1") dep)) dep) λk(Normal lv (p (Var nam dep)) dep))
(Normal.term lv (Txt val) dep) = (Txt val)
(Normal.term lv (Var nam idx) dep) = (Var nam idx)
(Normal.term lv (Src src val) dep) = (Src src (Normal lv val dep))
// Equality
// --------
// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
// WARNING: this is a very delicate algorithm!
// Before changing it, READ `docs/equality.md`
// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
// Check if two terms are identical. If not...
(Equal a b dep) =
(If (Identical a b dep) 1
let a = (Reduce 2 a)
let b = (Reduce 2 b)
(If (Identical a b dep) 1
(Similar a b dep)))
(Similar (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)))
(Similar (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))
(Similar (App a.fun a.arg) (App b.fun b.arg) dep) = (& (Equal a.fun b.fun dep) (Equal a.arg b.arg dep))
(Similar (Slf a.nam a.typ a.bod) (Slf b.nam b.typ b.bod) dep) = (Similar (Reduce 0 a.typ) (Reduce 0 b.typ) dep) // <- must call Similar, NOT Equal
(Similar (Hol a.nam a.ctx) b dep) = (Debug dep ["Found: ?" a.nam " = " (Show (Normal 0 b dep) dep)] 1)
(Similar a (Hol b.nam b.ctx) dep) = (Debug dep ["Found: ?" b.nam " = " (Show (Normal 0 a dep) dep)] 1)
(Similar (Hol a.nam a.ctx) (Hol b.nam b.ctx) dep) = (Same a.nam b.nam)
(Similar (Op2 a.opr a.fst a.snd) (Op2 b.opr b.fst b.snd) dep) = (& (Equal a.fst b.fst dep) (Equal a.snd b.snd dep))
(Similar (Mat a.nam a.x a.z a.s a.p) (Mat b.nam b.x b.z b.s b.p) dep) = (& (Equal a.x b.x dep) (& (Equal a.z b.z dep) (& (Equal (a.s (Var (String.concat a.nam "-1") dep)) (b.s (Var (String.concat b.nam "-1") dep)) dep) (Equal (a.p (Var a.nam dep)) (b.p (Var b.nam dep)) dep))))
(Similar a b dep) = 0
(Identical (All a.nam a.inp a.bod) (All b.nam b.inp b.bod) dep) = (& (Identical a.inp b.inp dep) (Identical (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep)))
(Identical (Lam a.nam a.bod) (Lam b.nam b.bod) dep) = (Identical (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep))
(Identical (App a.fun a.arg) (App b.fun b.arg) dep) = (& (Identical a.fun b.fun dep) (Identical a.arg b.arg dep))
(Identical (Slf a.nam a.typ a.bod) (Slf b.nam b.typ b.bod) dep) = (Identical a.typ b.typ dep)
(Identical (Ins a.val) b dep) = (Identical a.val b dep)
(Identical a (Ins b.val) dep) = (Identical a b.val dep)
(Identical (Ref a.nam a.val) (Ref b.nam b.val) dep) = (Same a.nam b.nam)
(Identical (Let a.nam a.val a.bod) b dep) = (Identical (a.bod a.val) b dep)
(Identical a (Let b.nam b.val b.bod) dep) = (Identical a (b.bod b.val) dep)
(Identical Set Set dep) = 1
(Identical (Var a.nam a.idx) (Var b.nam b.idx) dep) = (== a.idx b.idx)
(Identical (Ann a.val a.typ) b dep) = (Identical a.val b dep)
(Identical a (Ann b.val b.typ) dep) = (Identical a b.val dep)
(Identical (Hol a.nam a.ctx) b dep) = (Debug dep ["Found: ?" a.nam " = " (Show (Normal 0 b dep) dep)] 1)
(Identical a (Hol b.nam b.ctx) dep) = (Debug dep ["Found: ?" b.nam " = " (Show (Normal 0 a dep) dep)] 1)
(Identical (Hol a.nam a.ctx) (Hol b.nam b.ctx) dep) = (Same a.nam b.nam)
(Identical U60 U60 dep) = 1
(Identical (Num a.val) (Num b.val) dep) = (== a.val b.val)
(Identical (Op2 a.opr a.fst a.snd) (Op2 b.opr b.fst b.snd) dep) = (& (Identical a.fst b.fst dep) (Identical a.snd b.snd dep))
(Identical (Mat a.nam a.x a.z a.s a.p) (Mat b.nam b.x b.z b.s b.p) dep) = (& (Identical a.x b.x dep) (& (Identical a.z b.z dep) (& (Identical (a.s (Var (String.concat a.nam "-1") dep)) (b.s (Var (String.concat b.nam "-1") dep)) dep) (Identical (a.p (Var a.nam dep)) (b.p (Var b.nam dep)) dep))))
(Identical (Txt a.txt) (Txt b.txt) dep) = (Same a.txt b.txt)
(Identical (Src a.src a.val) b dep) = (Identical a.val b dep)
(Identical a (Src b.src b.val) dep) = (Identical a b.val dep)
(Identical 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 typ bod) yep nop) = (yep nam typ 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) =
(Maybe.bind (Check 0 inp Set dep) λinp_typ
(Maybe.bind (Check 0 (bod (Ann (Var nam dep) inp)) Set (+ 1 dep)) λbod_typ
(Maybe.pure Set)))
(Infer.match (Lam nam bod) dep) =
(Debug dep ["NON_FUNCTION_LAMBDA" NewLine "- detected: " (Show (Lam nam bod) dep)] (None))
(Infer.match (App fun arg) dep) =
(Maybe.bind (Infer fun dep) λfun_typ
((IfAll (Reduce 2 fun_typ)
λfun_nam λfun_typ.inp λfun_typ.bod λfun λarg
(Maybe.bind (Check 0 arg fun_typ.inp dep) λval_typ
(Maybe.pure (fun_typ.bod arg)))
λfun λarg
(Debug dep ["Error: NonFunApp " (Show (App fun arg) dep)] None))
fun arg))
(Infer.match (Ann val typ) dep) =
(Maybe.pure typ)
(Infer.match (Slf nam typ bod) dep) =
(Maybe.bind (Check 0 (bod (Ann (Var nam dep) typ)) Set (+ dep 1)) λslf
(Maybe.pure Set))
(Infer.match (Ins val) dep) =
(Maybe.bind (Infer val dep) λval_typ
((IfSlf (Reduce 2 val_typ)
λval_typ.nam λval_typ.typ λval_typ.bod λval (Maybe.pure (val_typ.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) =
(Maybe.pure Set)
(Infer.match U60 dep) =
(Maybe.pure Set)
(Infer.match (Num num) dep) =
(Maybe.pure U60)
(Infer.match (Txt txt) dep) =
(Maybe.pure Book.String)
(Infer.match (Op2 opr fst snd) dep) =
(Maybe.bind (Check 0 fst U60 dep) λfst
(Maybe.bind (Check 0 snd U60 dep) λsnd
(Maybe.pure U60)))
(Infer.match (Mat nam x z s p) dep) =
(Maybe.bind (Check 0 x U60 dep) λx_typ
(Maybe.bind (Check 0 (p (Ann (Var nam dep) U60)) Set dep) λp_typ
(Maybe.bind (Check 0 z (p (Num 0)) dep) λz_typ
(Maybe.bind (Check 0 (s (Ann (Var (String.concat nam "-1") dep) U60)) (p (Op2 ADD (Num 1) (Var (String.concat nam "-1") dep))) (+ dep 1)) λs_typ
(Maybe.pure (p x))))))
(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)
(Infer.match (Src src val) dep) =
(Infer.match val dep)
//(Check src term type dep) = (Debug dep ["Check: " (Show term dep) " :: " (Show type dep) " ~> " (Show (Reduce 2 type) dep)] (Check.match src term type dep))
(Check src term type dep) = (Check.match src term type dep)
(Check.match src (Lam term.nam term.bod) type dep) =
((IfAll (Reduce 2 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 0 term type (+ dep 1))
λterm.bod
(Infer (Lam term.nam term.bod) dep))
term.bod)
(Check.match src (Ins term.val) type dep) =
((IfSlf (Reduce 2 type)
λtype.nam λtype.typ λtype.bod λterm.val (Check 0 term.val (type.bod (Ins term.val)) dep)
λterm.val (Infer (Ins term.val) dep))
term.val)
(Check.match src (Let term.nam term.val term.bod) type dep) =
(Check 0 (term.bod term.val) type (+ 1 dep))
(Check.match src (Hol term.nam term.ctx) type dep) =
(Debug dep [(String.color BRIGHT) "HOLE: ?" term.nam " :: " (Show (Normal 0 type dep) dep) (String.color RESET) (Context.show term.ctx dep)]
(Maybe.pure 0))
(Check.match src (Ref term.nam (Ann term.val term.typ)) type dep) = // better printing
(Check.report src (Equal type term.typ dep) term.typ type (Ref term.nam term.val) dep)
(Check.match src (Src term.src term.val) type dep) =
(Check term.src term.val type dep)
//(Check.match src (Ref term.nam term.val) type dep) =
//(Check term.val type dep)
(Check.match src term type dep) =
(Check.verify src term type dep)
(Check.verify src term type dep) =
(Maybe.bind (Infer term dep) λinfer
(Check.report src (Equal type infer dep) infer type term dep))
(Check.report src 0 detected expected value dep) =
let det = (Show (Normal 0 detected dep) dep)
let exp = (Show (Normal 0 expected dep) dep)
let val = (Show (Normal 0 value dep) dep)
(Debug dep [(String.color BRIGHT) "TYPE_MISMATCH" NewLine
"- expected: " (String.color RESET) (String.color GREEN) exp NewLine (String.color RESET) (String.color BRIGHT)
"- detected: " (String.color RESET) (String.color RED) det NewLine (String.color RESET) (String.color BRIGHT)
"- bad_term: " (String.color RESET) (String.color DIM) val NewLine (String.color RESET)
"##LOC{" (U60.show src) "}LOC##" NewLine
] None)
(Check.report src n inferred expected value dep) =
(Maybe.pure 0)
// Syntax
// ------
(Show (All nam inp bod) dep) = (String.join ["∀(" nam ": " (Show inp dep) ") " (Show (bod (Var nam dep)) (+ dep 1))])
(Show (Lam nam bod) dep) = (String.join ["λ" nam " " (Show (bod (Var nam dep)) (+ dep 1))])
(Show (App fun arg) dep) = (String.join ["(" (Show.unwrap (Show fun dep)) " " (Show arg dep) ")"])
(Show (Ann val typ) dep) = (String.join ["{" (Show val dep) ": " (Show typ dep) "}"])
(Show (Slf nam typ bod) dep) = (String.join ["$(" nam ": " (Show typ dep) ") " (Show (bod (Var nam dep)) (+ dep 1))])
(Show (Ins val) dep) = (String.join ["~" (Show val dep)])
(Show (Ref nam val) dep) = nam
(Show (Let nam val bod) dep) = (String.join ["let " nam " = " (Show val dep) "; " (Show (bod (Var nam dep)) (+ dep 1))])
(Show Set dep) = (String.join ["*"])
(Show U60 dep) = "#U60"
(Show (Num val) dep) = (String.join ["#" (U60.show val)])
(Show (Op2 opr fst snd) dep) = (String.join ["#(" (Op2.show opr) " " (Show fst dep) " " (Show snd dep) ")"])
(Show (Mat nam x z s p) dep) = (String.join ["#match " nam " = " (Show x dep) " { #0: " (Show z dep) " #+: " (Show (s (Var (String.concat nam "-1") dep)) (+ dep 1)) " }: " (Show (p (Var nam dep)) dep)])
(Show (Txt txt) dep) = (String.join [Quote txt Quote])
(Show (Hol nam ctx) dep) = (String.join ["?" nam])
(Show (Var nam idx) dep) = (String.join [nam])
(Show (Src src val) dep) = (Show val dep)
//(Show (Var nam idx) dep) = (String.join [nam "'" (U60.show idx)])
(Show.many List.nil dep) = ""
(Show.many (List.cons x xs) dep) = (String.join [" " (Show x dep) (Show.many xs dep)])
(Show.trim (String.cons ' ' xs)) = xs
(Show.trim str) = str
(Show.unwrap (String.cons '(' xs)) = (Show.begin xs)
(Show.unwrap 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) = (String.join [NewLine "- " (Context.show.ann x dep) (Context.show xs dep)])
(Context.show.ann (Ann val typ) dep) = (String.join ["{" (Show (Normal 0 val dep) dep) ": " (Show (Normal 0 typ dep) dep) "}"])
(Context.show.ann term dep) = (Show (Normal 0 term dep) dep)
//(Context.show.ann val dep) = (String.join ["{" (Show (Normal 0 val dep) dep) ": " (Show (Normal 0 (Infer val dep) dep) dep) "}"])
// Compilation
// -----------
(Str.view str) = (str 0 λheadλtail(String.cons head (Str.view tail)) String.nil)
(Str.make (String.cons x xs)) = λP λcons λnil (cons x (Str.make xs))
(Str.make String.nil) = λP λcons λnil nil
Compile.primitives = [
(Pair "HVM.log" λA λB λmsg λret (HVM.log msg ret))
(Pair "HVM.print" λA λmsg λret (HVM.print (Str.view msg) ret))
(Pair "HVM.save" λA λname λdata λret (HVM.save (Str.view name) (Str.view data) ret))
(Pair "HVM.load" λA λname λret (HVM.load (Str.view name) λdata (ret (Str.make data))))
]
(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 typ bod)) = 0
(Compile (Ins val)) = (Compile val)
(Compile (Ref nam val)) = (Compile.ref Compile.primitives nam 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))
(Compile (Mat nam x z s p)) = (Compile.mat (Compile x) (Compile z) λx(Compile (s (Var "" x))))
(Compile (Txt txt)) = (Str.make txt)
(Compile (Hol nam ctx)) = 0
(Compile (Var nam val)) = val
(Compile (Src src val)) = (Compile 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)
(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))
(Compile.ref (List.cons (Pair prim_name prim_func) prims) nam val) = (If (Same prim_name nam) prim_func (Compile.ref prims nam val))
(Compile.ref List.nil nam val) = (Compile val)
// API
// ---
(Normalizer (Ref nam val)) = (Normalizer val)
(Normalizer (Ann val typ)) = (Normalizer val)
(Normalizer (Src src val)) = (Normalizer val)
(Normalizer val) = (Compile val)
//(Normalizer val) = (Str.view (Compile val))
(Checker name (Ref nam val)) = (Checker name val)
(Checker name (Src src (Ann val typ))) = (Checker.report name (Check src val typ 0))
(Checker name (Src src val)) = (Checker name val)
(Checker name (Ann val typ)) = (Checker.report name (Check 0 val typ 0))
(Checker name val) = (Checker.report name (Infer val 0))
(Checker.report name (Some x)) = 1
(Checker.report name None) = 0
//(Checker.report name (Some x)) = (HVM.print (String.join [(String.color GREEN) "- " name ": ✔" (String.color RESET)]) 1)
//(Checker.report name None) = (HVM.print (String.join [(String.color RED) "- " name ": ✘" (String.color RESET)]) 0)
(Checker.many.go (List.cons (Pair name def) defs)) = (& (Checker name def) (Checker.many.go defs))
(Checker.many.go List.nil) = 1
(Checker.many list) = (If (Checker.many.go list) ALL_TERMS_CHECK ERRORS_FOUND)
Book.Main = (Ref "Main" (Ann (Src 1099526307859 (Txt "foo")) (Src 1099518967819 (U60))))
Book.List = (Ref "List" (Ann (Src 3298559000766 (Lam "T" λ_T (Src 3298565292222 (Slf "self" (Src 3298573680685 (App (Src 3298574729258 (Book.List)) (Src 3298579972140 _T))) λ_self (Src 3298586263742 (All "P" (Src 3298593603659 (All "xs" (Src 3298601992264 (App (Src 3298603040837 (Book.List)) (Src 3298608283719 _T))) λ_xs (Src 3298612478027 (Set)))) λ_P (Src 3298617721022 (All "cons" (Src 3298628206741 (All "head" (Src 3298638692452 _T) λ_head (Src 3298641838229 (All "tail" (Src 3298652323960 (App (Src 3298653372533 (Book.List)) (Src 3298658615415 _T))) λ_tail (Src 3298662809749 (App (Src 3298663858300 _P) (Src 3298665955476 (App (App (App (Src 3298667004039 (Book.List.cons)) (Src 3298677489801 _T)) (Src 3298679586958 _head)) (Src 3298684829843 _tail))))))))) λ_cons (Src 3298695315646 (All "nil" (Src 3298704752818 (App (Src 3298705801380 _P) (Src 3298707898545 (App (Src 3298708947118 (Book.List.nil)) (Src 3298718384304 _T))))) λ_nil (Src 3298725724350 (App (Src 3298726772920 _P) (Src 3298728870077 _self))))))))))))) (Src 3298542223380 (All "T" (Src 3298549563407 (Set)) λ_T (Src 3298554806292 (Set))))))
Book.String = (Ref "String" (Ann (Src 2199036887064 (App (Src 2199037935634 (Book.List)) (Src 2199043178519 (Book.Char)))) (Src 2199032692746 (Set))))
Book.List.nil = (Ref "List.nil" (Ann (Src 5497593790527 (Lam "T" λ_T (Src 5497600081983 (Ins (Src 5497601130559 (Lam "P" λ_P (Src 5497605324863 (Lam "cons" λ_cons (Src 5497612664895 (Lam "nil" λ_nil (Src 5497621053503 _nil))))))))))) (Src 5497569673247 (All "T" (Src 5497577013267 (Set)) λ_T (Src 5497582256159 (App (Src 5497583304732 (Book.List)) (Src 5497588547614 _T)))))))
Book.Char = (Ref "Char" (Ann (Src 6597081301007 (U60)) (Src 6597077106696 (Set))))
Book.String.cons = (Ref "String.cons" (Ann (Src 7696645357681 (Lam "head" λ_head (Src 7696652697713 (Lam "tail" λ_tail (Src 7696662134897 (Ins (Src 7696663183473 (Lam "P" λ_P (Src 7696667377777 (Lam "cons" λ_cons (Src 7696674717809 (Lam "nil" λ_nil (Src 7696683106417 (App (App (Src 7696684154982 _cons) (Src 7696689397867 _head)) (Src 7696694640752 _tail))))))))))))))) (Src 7696596074554 (All "head" (Src 7696606560284 (Book.Char)) λ_head (Src 7696614948922 (All "tail" (Src 7696625434672 (Book.String)) λ_tail (Src 7696635920442 (Book.String))))))))
Book.List.cons = (Ref "List.cons" (Ann (Src 4398122008704 (Lam "T" λ_T (Src 4398126203008 (Lam "head" λ_head (Src 4398133543040 (Lam "tail" λ_tail (Src 4398142980224 (Ins (Src 4398144028800 (Lam "P" λ_P (Src 4398148223104 (Lam "cons" λ_cons (Src 4398155563136 (Lam "nil" λ_nil (Src 4398163951744 (App (App (Src 4398165000309 _cons) (Src 4398170243194 _head)) (Src 4398175486079 _tail))))))))))))))))) (Src 4398059094085 (All "T" (Src 4398066434068 (Set)) λ_T (Src 4398071676997 (All "head" (Src 4398082162723 _T) λ_head (Src 4398087405637 (All "tail" (Src 4398097891385 (App (Src 4398098939958 (Book.List)) (Src 4398104182840 _T))) λ_tail (Src 4398110474309 (App (Src 4398111522882 (Book.List)) (Src 4398116765764 _T)))))))))))
Book.String.nil = (Ref "String.nil" (Ann (Src 8796116090925 (Ins (Src 8796117139501 (Lam "P" λ_P (Src 8796121333805 (Lam "cons" λ_cons (Src 8796128673837 (Lam "nil" λ_nil (Src 8796137062445 _nil))))))))) (Src 8796106653715 (Book.String))))
Main = (Checker.many [(Pair "Char" Book.Char) (Pair "List" Book.List) (Pair "List.cons" Book.List.cons) (Pair "List.nil" Book.List.nil) (Pair "Main" Book.Main) (Pair "String" Book.String) (Pair "String.cons" Book.String.cons) (Pair "String.nil" Book.String.nil)])
Reference in New Issue View Git Blame Copy Permalink