mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-09-11 12:25:47 +03:00
Working Rust CLI! Pretty errors. Many improvements
This commit is contained in:
parent
ee3c1550d9
commit
6dbe738b4c
5
Cargo.lock
generated
5
Cargo.lock
generated
@ -4,9 +4,9 @@ version = 3
|
|||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "TSPL"
|
name = "TSPL"
|
||||||
version = "0.0.1"
|
version = "0.0.4"
|
||||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
checksum = "d7f7bc3c167472f0599b71590ead5067418477b7d512ec251b25b4aa78fa808f"
|
checksum = "5b8ec3e7412fb948ebd3410595e15e7f80c12bf7958ffb83a7f6ff34942505f9"
|
||||||
dependencies = [
|
dependencies = [
|
||||||
"highlight_error",
|
"highlight_error",
|
||||||
]
|
]
|
||||||
@ -45,6 +45,7 @@ name = "kind2"
|
|||||||
version = "0.1.0"
|
version = "0.1.0"
|
||||||
dependencies = [
|
dependencies = [
|
||||||
"TSPL",
|
"TSPL",
|
||||||
|
"highlight_error",
|
||||||
"im",
|
"im",
|
||||||
]
|
]
|
||||||
|
|
||||||
|
@ -3,8 +3,11 @@ name = "kind2"
|
|||||||
version = "0.1.0"
|
version = "0.1.0"
|
||||||
edition = "2021"
|
edition = "2021"
|
||||||
|
|
||||||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
|
[[bin]]
|
||||||
|
name = "kind2"
|
||||||
|
path = "src/main.rs"
|
||||||
|
|
||||||
[dependencies]
|
[dependencies]
|
||||||
TSPL = "0.0.1"
|
TSPL = "0.0.4"
|
||||||
|
highlight_error = "0.1.1"
|
||||||
im = "15.1.0"
|
im = "15.1.0"
|
||||||
|
486
book/.check.hvm1
Normal file
486
book/.check.hvm1
Normal file
@ -0,0 +1,486 @@
|
|||||||
|
// 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)
|
||||||
|
//| (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 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 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)
|
||||||
|
(Reduce r (Src src val)) = (Reduce r val)
|
||||||
|
(Reduce r val) = val
|
||||||
|
|
||||||
|
(Reduce.app r (Lam nam bod) arg) = (Reduce r (bod (Reduce 0 arg)))
|
||||||
|
//(Reduce.app r (Hol nam ctx ars) arg) = (Hol nam ctx (List.cons arg ars))
|
||||||
|
(Reduce.app r fun arg) = (App fun arg)
|
||||||
|
|
||||||
|
(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 (Op2 ADD (Num 1) k) z s p) = (Reduce r (s k))
|
||||||
|
(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
|
||||||
|
|
||||||
|
(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 (Op2 opr fst snd) dep) = (Op2 opr (Normal.term r fst dep) (Normal.term r snd dep))
|
||||||
|
(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 (String.concat nam "-1") dep)) dep) λk(Normal r (p (Var nam dep)) dep))
|
||||||
|
(Normal.term r (Txt val) dep) = (Txt val)
|
||||||
|
(Normal.term r (Var nam idx) dep) = (Var nam idx)
|
||||||
|
(Normal.term r (Src src val) dep) = (Src src (Normal r val dep))
|
||||||
|
|
||||||
|
// 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) (Reduce 0 a) (Reduce 0 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 (Normal 0 b dep) dep)] 1)
|
||||||
|
(Comparer rec a (Hol b.nam b.ctx) dep) = (Debug dep ["Found: ?" b.nam " = " (Show (Normal 0 a dep) dep)] 1)
|
||||||
|
(Comparer rec (Hol a.nam a.ctx) (Hol b.nam b.ctx) dep) = (Same a.nam b.nam)
|
||||||
|
(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 b.fst dep) (rec a.snd 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 (String.concat a.nam "-1") dep)) (b.s (Var (String.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 (Src a.src a.val) b dep) = (Comparer rec a.val b dep)
|
||||||
|
(Comparer rec a (Src b.src b.val) dep) = (Comparer rec a b.val dep)
|
||||||
|
(Comparer rec a b dep) = 0
|
||||||
|
//(Comparer rec a b dep) = (HVM.log (NOP (Show a dep) (Show 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) =
|
||||||
|
(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 ["Error: NonFunLam " (Show (Lam nam bod) dep)] (None))
|
||||||
|
(Infer.match (App fun arg) dep) =
|
||||||
|
(Maybe.bind (Infer fun dep) λfun_typ
|
||||||
|
((IfAll (Reduce 1 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 bod) dep) =
|
||||||
|
(Maybe.bind (Check 0 (bod (Ann (Var nam dep) (Slf nam bod))) Set (+ dep 1)) λslf
|
||||||
|
(Maybe.pure Set))
|
||||||
|
(Infer.match (Ins val) dep) =
|
||||||
|
(Maybe.bind (Infer val dep) λval_typ
|
||||||
|
((IfSlf (Reduce 1 val_typ)
|
||||||
|
λval_nam λ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 term type dep) = (Debug dep ["Check: " (Show term dep) " :: " (Show type dep)] (Check.match 0 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 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 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 1 type)
|
||||||
|
λtype.nam λ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 bod) dep) = (String.join ["$" nam " " (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 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.List.cons = (Ref "List.cons" (Ann (Src 5497633636480 (Lam "T" λ_T (Src 5497637830784 (Lam "head" λ_head (Src 5497645170816 (Lam "tail" λ_tail (Src 5497654608000 (Ins (Src 5497655656576 (Lam "P" λ_P (Src 5497659850880 (Lam "cons" λ_cons (Src 5497667190912 (Lam "nil" λ_nil (Src 5497675579520 (App (App (Src 5497676628085 _cons) (Src 5497681870970 _head)) (Src 5497687113855 _tail))))))))))))))))) (Src 5497570721861 (All "T" (Src 5497578061844 (Set)) λ_T (Src 5497583304773 (All "head" (Src 5497593790499 _T) λ_head (Src 5497599033413 (All "tail" (Src 5497609519161 (App (Src 5497610567734 (Book.List)) (Src 5497615810616 _T))) λ_tail (Src 5497622102085 (App (Src 5497623150658 (Book.List)) (Src 5497628393540 _T)))))))))))
|
||||||
|
Book.List.nil = (Ref "List.nil" (Ann (Src 6597105418303 (Lam "T" λ_T (Src 6597111709759 (Ins (Src 6597112758335 (Lam "P" λ_P (Src 6597116952639 (Lam "cons" λ_cons (Src 6597124292671 (Lam "nil" λ_nil (Src 6597132681279 _nil))))))))))) (Src 6597081301023 (All "T" (Src 6597088641043 (Set)) λ_T (Src 6597093883935 (App (Src 6597094932508 (Book.List)) (Src 6597100175390 _T)))))))
|
||||||
|
Book.Main = (Ref "Main" (Ann (Src 1099526307866 (Op2 ADD (Src 1099530502165 (Num 12)) (Src 1099534696473 (Num 30)))) (Src 1099518967819 (U60))))
|
||||||
|
Book.List = (Ref "List" (Ann (Src 4398070628530 (Lam "T" λ_T (Src 4398076919986 (Slf "self" λ_self (Src 4398085308594 (All "P" (Src 4398092648511 (All "xs" (Src 4398101037116 (App (Src 4398102085689 (Book.List)) (Src 4398107328571 _T))) λ_xs (Src 4398111522879 (Set)))) λ_P (Src 4398116765874 (All "cons" (Src 4398127251593 (All "head" (Src 4398137737304 _T) λ_head (Src 4398140883081 (All "tail" (Src 4398151368812 (App (Src 4398152417385 (Book.List)) (Src 4398157660267 _T))) λ_tail (Src 4398161854601 (App (Src 4398162903152 _P) (Src 4398165000328 (App (App (App (Src 4398166048891 (Book.List.cons)) (Src 4398176534653 _T)) (Src 4398178631810 _head)) (Src 4398183874695 _tail))))))))) λ_cons (Src 4398194360498 (All "nil" (Src 4398203797670 (App (Src 4398204846232 _P) (Src 4398206943397 (App (Src 4398207991970 (Book.List.nil)) (Src 4398217429156 _T))))) λ_nil (Src 4398224769202 (App (Src 4398225817772 _P) (Src 4398227914929 _self))))))))))))) (Src 4398053851156 (All "T" (Src 4398061191183 (Set)) λ_T (Src 4398066434068 (Set))))))
|
||||||
|
Book.Char = (Ref "Char" (Ann (Src 3298546417679 (U60)) (Src 3298542223368 (Set))))
|
||||||
|
Book.String = (Ref "String" (Ann (Src 2199036887064 (App (Src 2199037935634 (Book.List)) (Src 2199043178519 (Book.Char)))) (Src 2199032692746 (Set))))
|
||||||
|
|
||||||
|
Main = (Normalizer Book.Main)
|
14
book/IO.bind.kind2
Normal file
14
book/IO.bind.kind2
Normal file
@ -0,0 +1,14 @@
|
|||||||
|
IO.bind
|
||||||
|
: ∀(A: *)
|
||||||
|
∀(B: *)
|
||||||
|
∀(a: (IO A))
|
||||||
|
∀(b: ∀(x: A) (IO B))
|
||||||
|
(IO B)
|
||||||
|
= λA λB λa λb
|
||||||
|
let P = λx ∀(b: ∀(x: A) (IO B)) (IO B)
|
||||||
|
let print = λtext λthen λb (IO.print B text λx(IO.bind A B (then x) b))
|
||||||
|
let load = λfile λthen λb (IO.load B file λs(IO.bind A B (then s) b))
|
||||||
|
let save = λfile λdata λthen λb (IO.save B file data λx(IO.bind A B (then Unit.one) b))
|
||||||
|
let done = λterm λb (b term)
|
||||||
|
((~a P print load save done) b)
|
||||||
|
|
8
book/IO.done.kind2
Normal file
8
book/IO.done.kind2
Normal file
@ -0,0 +1,8 @@
|
|||||||
|
IO.done
|
||||||
|
: ∀(A: *)
|
||||||
|
∀(term: A)
|
||||||
|
(IO A)
|
||||||
|
= λA λterm
|
||||||
|
~λP λprint λload λsave λdone
|
||||||
|
(done term)
|
||||||
|
|
@ -8,88 +8,3 @@ IO
|
|||||||
∀(save: ∀(file: String) ∀(data: String) ∀(then: ∀(x: Unit) (IO A)) (P (IO.save A file data then)))
|
∀(save: ∀(file: String) ∀(data: String) ∀(then: ∀(x: Unit) (IO A)) (P (IO.save A file data then)))
|
||||||
∀(done: ∀(term: A) (P (IO.done A term)))
|
∀(done: ∀(term: A) (P (IO.done A term)))
|
||||||
(P self)
|
(P self)
|
||||||
|
|
||||||
IO.print
|
|
||||||
: ∀(A: *)
|
|
||||||
∀(text: String)
|
|
||||||
∀(then: ∀(x: Unit) (IO A))
|
|
||||||
(IO A)
|
|
||||||
= λA λtext λthen
|
|
||||||
~λP λprint λload λsave λdone
|
|
||||||
(print text then)
|
|
||||||
|
|
||||||
IO.load
|
|
||||||
: ∀(A: *)
|
|
||||||
∀(file: String)
|
|
||||||
∀(then: ∀(x: String) (IO A))
|
|
||||||
(IO A)
|
|
||||||
= λA λfile λthen
|
|
||||||
~λP λprint λload λsave λdone
|
|
||||||
(load file then)
|
|
||||||
|
|
||||||
IO.save
|
|
||||||
: ∀(A: *)
|
|
||||||
∀(file: String)
|
|
||||||
∀(data: String)
|
|
||||||
∀(then: ∀(x: Unit) (IO A))
|
|
||||||
(IO A)
|
|
||||||
= λA λfile λdata λthen
|
|
||||||
~λP λprint λload λsave λdone
|
|
||||||
(save file data then)
|
|
||||||
|
|
||||||
IO.done
|
|
||||||
: ∀(A: *)
|
|
||||||
∀(term: A)
|
|
||||||
(IO A)
|
|
||||||
= λA λterm
|
|
||||||
~λP λprint λload λsave λdone
|
|
||||||
(done term)
|
|
||||||
|
|
||||||
IO.run
|
|
||||||
: ∀(A: *)
|
|
||||||
∀(x: (IO A))
|
|
||||||
(IO A)
|
|
||||||
= λA λx
|
|
||||||
let P = λx(A)
|
|
||||||
let print = λtext λthen (HVM.print A text (IO.run A (then Unit.one)))
|
|
||||||
let load = λfile λthen (HVM.load A file λs(IO.run A (then s)))
|
|
||||||
let save = λfile λdata λthen (HVM.save A file data (IO.run A (then Unit.one)))
|
|
||||||
let done = λterm (IO.done A term)
|
|
||||||
(~x P print load save done)
|
|
||||||
|
|
||||||
IO.print.do
|
|
||||||
: ∀(text: String)
|
|
||||||
(IO Unit)
|
|
||||||
= λtext
|
|
||||||
(IO.print Unit text λx
|
|
||||||
(IO.done Unit x))
|
|
||||||
|
|
||||||
IO.load.do
|
|
||||||
: ∀(file: String)
|
|
||||||
(IO String)
|
|
||||||
= λfile
|
|
||||||
(IO.load String file λx
|
|
||||||
(IO.done String x))
|
|
||||||
|
|
||||||
IO.save.do
|
|
||||||
: ∀(file: String)
|
|
||||||
∀(data: String)
|
|
||||||
(IO Unit)
|
|
||||||
= λfile λdata
|
|
||||||
(IO.save Unit file data λx
|
|
||||||
(IO.done Unit x))
|
|
||||||
|
|
||||||
IO.bind
|
|
||||||
: ∀(A: *)
|
|
||||||
∀(B: *)
|
|
||||||
∀(a: (IO A))
|
|
||||||
∀(b: ∀(x: A) (IO B))
|
|
||||||
(IO B)
|
|
||||||
= λA λB λa λb
|
|
||||||
let P = λx ∀(b: ∀(x: A) (IO B)) (IO B)
|
|
||||||
let print = λtext λthen λb (IO.print B text λx(IO.bind A B (then x) b))
|
|
||||||
let load = λfile λthen λb (IO.load B file λs(IO.bind A B (then s) b))
|
|
||||||
let save = λfile λdata λthen λb (IO.save B file data λx(IO.bind A B (then Unit.one) b))
|
|
||||||
let done = λterm λb (b term)
|
|
||||||
((~a P print load save done) b)
|
|
||||||
|
|
||||||
|
7
book/IO.load.do.kind2
Normal file
7
book/IO.load.do.kind2
Normal file
@ -0,0 +1,7 @@
|
|||||||
|
IO.load.do
|
||||||
|
: ∀(file: String)
|
||||||
|
(IO String)
|
||||||
|
= λfile
|
||||||
|
(IO.load String file λx
|
||||||
|
(IO.done String x))
|
||||||
|
|
9
book/IO.load.kind2
Normal file
9
book/IO.load.kind2
Normal file
@ -0,0 +1,9 @@
|
|||||||
|
IO.load
|
||||||
|
: ∀(A: *)
|
||||||
|
∀(file: String)
|
||||||
|
∀(then: ∀(x: String) (IO A))
|
||||||
|
(IO A)
|
||||||
|
= λA λfile λthen
|
||||||
|
~λP λprint λload λsave λdone
|
||||||
|
(load file then)
|
||||||
|
|
7
book/IO.print.do.kind2
Normal file
7
book/IO.print.do.kind2
Normal file
@ -0,0 +1,7 @@
|
|||||||
|
IO.print.do
|
||||||
|
: ∀(text: String)
|
||||||
|
(IO Unit)
|
||||||
|
= λtext
|
||||||
|
(IO.print Unit text λx
|
||||||
|
(IO.done Unit x))
|
||||||
|
|
9
book/IO.print.kind2
Normal file
9
book/IO.print.kind2
Normal file
@ -0,0 +1,9 @@
|
|||||||
|
IO.print
|
||||||
|
: ∀(A: *)
|
||||||
|
∀(text: String)
|
||||||
|
∀(then: ∀(x: Unit) (IO A))
|
||||||
|
(IO A)
|
||||||
|
= λA λtext λthen
|
||||||
|
~λP λprint λload λsave λdone
|
||||||
|
(print text then)
|
||||||
|
|
12
book/IO.run.kind2
Normal file
12
book/IO.run.kind2
Normal file
@ -0,0 +1,12 @@
|
|||||||
|
IO.run
|
||||||
|
: ∀(A: *)
|
||||||
|
∀(x: (IO A))
|
||||||
|
(IO A)
|
||||||
|
= λA λx
|
||||||
|
let P = λx(IO A)
|
||||||
|
let print = λtext λthen (HVM.print (IO A) text (IO.run A (then Unit.one)))
|
||||||
|
let load = λfile λthen (HVM.load (IO A) file λs(IO.run A (then s)))
|
||||||
|
let save = λfile λdata λthen (HVM.save (IO A) file data (IO.run A (then Unit.one)))
|
||||||
|
let done = λterm (IO.done A term)
|
||||||
|
(~x P print load save done)
|
||||||
|
|
8
book/IO.save.do.kind2
Normal file
8
book/IO.save.do.kind2
Normal file
@ -0,0 +1,8 @@
|
|||||||
|
IO.save.do
|
||||||
|
: ∀(file: String)
|
||||||
|
∀(data: String)
|
||||||
|
(IO Unit)
|
||||||
|
= λfile λdata
|
||||||
|
(IO.save Unit file data λx
|
||||||
|
(IO.done Unit x))
|
||||||
|
|
10
book/IO.save.kind2
Normal file
10
book/IO.save.kind2
Normal file
@ -0,0 +1,10 @@
|
|||||||
|
IO.save
|
||||||
|
: ∀(A: *)
|
||||||
|
∀(file: String)
|
||||||
|
∀(data: String)
|
||||||
|
∀(then: ∀(x: Unit) (IO A))
|
||||||
|
(IO A)
|
||||||
|
= λA λfile λdata λthen
|
||||||
|
~λP λprint λload λsave λdone
|
||||||
|
(save file data then)
|
||||||
|
|
@ -7,6 +7,6 @@ Kind.Term.parser.app
|
|||||||
(Kind.Term.parser.bind Unit (Parser.text ")") λ_
|
(Kind.Term.parser.bind Unit (Parser.text ")") λ_
|
||||||
(Kind.Term.parser.pure λscp
|
(Kind.Term.parser.pure λscp
|
||||||
(((List.fold Kind.PreTerm terms) ∀(fun:Kind.Term)Kind.Term
|
(((List.fold Kind.PreTerm terms) ∀(fun:Kind.Term)Kind.Term
|
||||||
λargλrecλfun(rec (Kind.app fun (arg scp)))
|
λarg λrec λfun (rec (Kind.app fun (arg scp)))
|
||||||
λfun(fun))
|
λfun(fun))
|
||||||
(fun scp))))))))
|
(fun scp))))))))
|
@ -3,4 +3,4 @@ Kind.Term.to_hvm
|
|||||||
∀(dep: Nat)
|
∀(dep: Nat)
|
||||||
String
|
String
|
||||||
= λterm λdep
|
= λterm λdep
|
||||||
(String.Concatenator.build (Kind.Term.to_hvm.go term dep))
|
(String.Concatenator.build (Kind.Term.to_hvm.go term dep Bool.true Nat.zero))
|
||||||
|
8
book/Kind.load.code.kind2
Normal file
8
book/Kind.load.code.kind2
Normal file
@ -0,0 +1,8 @@
|
|||||||
|
// Loads a file into a book
|
||||||
|
Kind.load.code
|
||||||
|
: ∀(name: String)
|
||||||
|
(IO Kind.Book)
|
||||||
|
= λname
|
||||||
|
(IO.load Kind.Book (String.concat name ".kind2") λdata
|
||||||
|
(IO.done Kind.Book (Kind.Book.parse data)))
|
||||||
|
|
13
book/Kind.load.dependencies.kind2
Normal file
13
book/Kind.load.dependencies.kind2
Normal file
@ -0,0 +1,13 @@
|
|||||||
|
// Loads a list of dependencies
|
||||||
|
Kind.load.dependencies
|
||||||
|
: ∀(deps: (List String))
|
||||||
|
∀(book: Kind.Book)
|
||||||
|
(IO Kind.Book)
|
||||||
|
= λdeps λbook
|
||||||
|
let P = λx ∀(book: Kind.Book) (IO Kind.Book)
|
||||||
|
let cons = λdeps.head λdeps.tail λbook
|
||||||
|
(IO.bind Kind.Book Kind.Book (Kind.load.dependency deps.head book) λbook
|
||||||
|
(Kind.load.dependencies deps.tail book))
|
||||||
|
let nil = λbook (IO.done Kind.Book book)
|
||||||
|
((~deps P cons nil) book)
|
||||||
|
|
13
book/Kind.load.dependency.kind2
Normal file
13
book/Kind.load.dependency.kind2
Normal file
@ -0,0 +1,13 @@
|
|||||||
|
// Loads a single dependency, if not present
|
||||||
|
// FIXME: String.map.has.linear is removing the entry
|
||||||
|
Kind.load.dependency
|
||||||
|
: ∀(name: String)
|
||||||
|
∀(book: Kind.Book)
|
||||||
|
(IO Kind.Book)
|
||||||
|
= λname λbook
|
||||||
|
let has = (String.Map.has Kind.Term name book)
|
||||||
|
let P = λx ∀(book: Kind.Book) (IO Kind.Book)
|
||||||
|
let true = λbook (IO.done Kind.Book book)
|
||||||
|
let false = λbook (Kind.load.name name book)
|
||||||
|
((~has P true false) book)
|
||||||
|
|
@ -4,65 +4,3 @@ Kind.load
|
|||||||
= λname
|
= λname
|
||||||
let book = (String.Map.new Kind.Term)
|
let book = (String.Map.new Kind.Term)
|
||||||
(Kind.load.name name book)
|
(Kind.load.name name book)
|
||||||
|
|
||||||
// Loads a file into a book
|
|
||||||
Kind.load.code
|
|
||||||
: ∀(name: String)
|
|
||||||
(IO Kind.Book)
|
|
||||||
= λname
|
|
||||||
(IO.load Kind.Book (String.concat name ".kind2") λdata
|
|
||||||
(IO.done Kind.Book (Kind.Book.parse data)))
|
|
||||||
|
|
||||||
// Loads a name into a book; then, load its dependencies
|
|
||||||
Kind.load.name
|
|
||||||
: ∀(name: String)
|
|
||||||
∀(book: Kind.Book)
|
|
||||||
(IO Kind.Book)
|
|
||||||
= λname λbook
|
|
||||||
(IO.bind Kind.Book Kind.Book (Kind.load.code name) λfile
|
|
||||||
let defs = (String.Map.to_list Kind.Term file)
|
|
||||||
let fold = (List.fold (Pair String Kind.Term) defs)
|
|
||||||
let set2 = λnam λval (String.Map.set Kind.Term nam val book)
|
|
||||||
let setP = λdef λbook (~def λx(Kind.Book) set2)
|
|
||||||
let book = (fold Kind.Book setP book)
|
|
||||||
let deps = (Kind.Book.get_refs file)
|
|
||||||
(Kind.load.dependencies deps book))
|
|
||||||
|
|
||||||
// Loads a list of dependencies
|
|
||||||
Kind.load.dependencies
|
|
||||||
: ∀(deps: (List String))
|
|
||||||
∀(book: Kind.Book)
|
|
||||||
(IO Kind.Book)
|
|
||||||
= λdeps λbook
|
|
||||||
let P = λx ∀(book: Kind.Book) (IO Kind.Book)
|
|
||||||
let cons = λdeps.head λdeps.tail λbook
|
|
||||||
(IO.bind Kind.Book Kind.Book (Kind.load.dependency deps.head book) λbook
|
|
||||||
(Kind.load.dependencies deps.tail book))
|
|
||||||
let nil = λbook (IO.done Kind.Book book)
|
|
||||||
((~deps P cons nil) book)
|
|
||||||
|
|
||||||
// Loads a single dependency, if not present
|
|
||||||
// FIXME: String.map.has.linear is removing the entry
|
|
||||||
Kind.load.dependency
|
|
||||||
: ∀(name: String)
|
|
||||||
∀(book: Kind.Book)
|
|
||||||
(IO Kind.Book)
|
|
||||||
= λname λbook
|
|
||||||
let has = (String.Map.has Kind.Term name book)
|
|
||||||
let P = λx ∀(book: Kind.Book) (IO Kind.Book)
|
|
||||||
let true = λbook (IO.done Kind.Book book)
|
|
||||||
let false = λbook (Kind.load.name name book)
|
|
||||||
((~has P true false) book)
|
|
||||||
|
|
||||||
//Kind.load.dependency
|
|
||||||
//: ∀(name: String)
|
|
||||||
//∀(book: Kind.Book)
|
|
||||||
//(IO Kind.Book)
|
|
||||||
//= λname λbook
|
|
||||||
//let P = λx (IO Kind.Book)
|
|
||||||
//let new = λhas λbook
|
|
||||||
//let P = λx ∀(book: Kind.Book) (IO Kind.Book)
|
|
||||||
//let true = λbook (IO.done Kind.Book book)
|
|
||||||
//let false = λbook (Kind.load.name name book)
|
|
||||||
//((~has P true false) book)
|
|
||||||
//(~(String.Map.has.linear Kind.Term name book) P new)
|
|
||||||
|
15
book/Kind.load.name.kind2
Normal file
15
book/Kind.load.name.kind2
Normal file
@ -0,0 +1,15 @@
|
|||||||
|
// Loads a name into a book; then, load its dependencies
|
||||||
|
Kind.load.name
|
||||||
|
: ∀(name: String)
|
||||||
|
∀(book: Kind.Book)
|
||||||
|
(IO Kind.Book)
|
||||||
|
= λname λbook
|
||||||
|
(IO.bind Kind.Book Kind.Book (Kind.load.code name) λfile
|
||||||
|
let defs = (String.Map.to_list Kind.Term file)
|
||||||
|
let fold = (List.fold (Pair String Kind.Term) defs)
|
||||||
|
let set2 = λnam λval (String.Map.set Kind.Term nam val book)
|
||||||
|
let setP = λdef λbook (~def λx(Kind.Book) set2)
|
||||||
|
let book = (fold Kind.Book setP book)
|
||||||
|
let deps = (Kind.Book.get_refs file)
|
||||||
|
(Kind.load.dependencies deps book))
|
||||||
|
|
@ -13,6 +13,7 @@ Kind.reduce.op2
|
|||||||
let mul = λfst_val λsnd_val (Kind.num #(* fst_val snd_val))
|
let mul = λfst_val λsnd_val (Kind.num #(* fst_val snd_val))
|
||||||
let sub = λfst_val λsnd_val (Kind.num #(- fst_val snd_val))
|
let sub = λfst_val λsnd_val (Kind.num #(- fst_val snd_val))
|
||||||
let div = λfst_val λsnd_val (Kind.num #(/ fst_val snd_val))
|
let div = λfst_val λsnd_val (Kind.num #(/ fst_val snd_val))
|
||||||
|
let mod = λfst_val λsnd_val (Kind.num #(% fst_val snd_val))
|
||||||
let eq = λfst_val λsnd_val (Kind.num #(== fst_val snd_val))
|
let eq = λfst_val λsnd_val (Kind.num #(== fst_val snd_val))
|
||||||
let ne = λfst_val λsnd_val (Kind.num #(!= fst_val snd_val))
|
let ne = λfst_val λsnd_val (Kind.num #(!= fst_val snd_val))
|
||||||
let lt = λfst_val λsnd_val (Kind.num #(< fst_val snd_val))
|
let lt = λfst_val λsnd_val (Kind.num #(< fst_val snd_val))
|
||||||
@ -24,7 +25,7 @@ Kind.reduce.op2
|
|||||||
let xor = λfst_val λsnd_val (Kind.num #(^ fst_val snd_val))
|
let xor = λfst_val λsnd_val (Kind.num #(^ fst_val snd_val))
|
||||||
let lsh = λfst_val λsnd_val (Kind.num #(<< fst_val snd_val))
|
let lsh = λfst_val λsnd_val (Kind.num #(<< fst_val snd_val))
|
||||||
let rsh = λfst_val λsnd_val (Kind.num #(>> fst_val snd_val))
|
let rsh = λfst_val λsnd_val (Kind.num #(>> fst_val snd_val))
|
||||||
(~opr P add mul sub div eq ne lt gt lte gte and or xor lsh rsh fst_val snd_val)
|
((~opr P add mul sub div mod eq ne lt gt lte gte and or xor lsh rsh) fst_val snd_val)
|
||||||
let N = λsnd λfst_val (Kind.op2 opr (Kind.num fst_val) snd)
|
let N = λsnd λfst_val (Kind.op2 opr (Kind.num fst_val) snd)
|
||||||
(Kind.if.num snd P Y N fst_val)
|
(Kind.if.num snd P Y N fst_val)
|
||||||
let N = λfst λsnd (Kind.op2 opr fst snd)
|
let N = λfst λsnd (Kind.op2 opr fst snd)
|
||||||
|
@ -1,5 +1,16 @@
|
|||||||
Main
|
Main
|
||||||
= (Kind.API.to_hvm "Bool")
|
: #U60
|
||||||
|
= #(+ #12 #30)
|
||||||
|
|
||||||
|
//TYPE_MISMATCH
|
||||||
|
//- expected: (Pair (Maybe V) (String.Map V))
|
||||||
|
//- detected: (Pair (Maybe V) (BBT String V))
|
||||||
|
//- bad_term: (BBT.got String V String.cmp key map)
|
||||||
|
//./String.Map.kind2
|
||||||
|
//20 | (BBT.got String V String.cmp key map)
|
||||||
|
|
||||||
|
//(List.cons (Pair Char Char) (Pair.new Char Char Char #8) // '\b'
|
||||||
|
//(List.nil (Pair Char Char)))
|
||||||
|
|
||||||
|
|
||||||
//Main
|
//Main
|
||||||
|
8
book/String.Map.get.kind2
Normal file
8
book/String.Map.get.kind2
Normal file
@ -0,0 +1,8 @@
|
|||||||
|
String.Map.get
|
||||||
|
: ∀(V: *)
|
||||||
|
∀(key: String)
|
||||||
|
∀(map: (String.Map V))
|
||||||
|
(Maybe V)
|
||||||
|
= λV λkey λmap
|
||||||
|
(BBT.get String V String.cmp key map)
|
||||||
|
|
8
book/String.Map.got.kind2
Normal file
8
book/String.Map.got.kind2
Normal file
@ -0,0 +1,8 @@
|
|||||||
|
String.Map.got
|
||||||
|
: ∀(V: *)
|
||||||
|
∀(key: String)
|
||||||
|
∀(map: (String.Map V))
|
||||||
|
(Pair (Maybe V) (String.Map V))
|
||||||
|
= λV λkey λmap
|
||||||
|
(BBT.got String V String.cmp key map)
|
||||||
|
|
@ -2,34 +2,3 @@ String.Map
|
|||||||
: ∀(V: *)
|
: ∀(V: *)
|
||||||
*
|
*
|
||||||
= λV (BBT String V)
|
= λV (BBT String V)
|
||||||
|
|
||||||
String.Map.get
|
|
||||||
: ∀(V: *)
|
|
||||||
∀(key: String)
|
|
||||||
∀(map: (String.Map V))
|
|
||||||
(Maybe V)
|
|
||||||
= λV λkey λmap
|
|
||||||
(BBT.get String V String.cmp key map)
|
|
||||||
|
|
||||||
String.Map.got
|
|
||||||
: ∀(V: *)
|
|
||||||
∀(key: String)
|
|
||||||
∀(map: (String.Map V))
|
|
||||||
(Pair (Maybe V) (String.Map V))
|
|
||||||
= λV λkey λmap
|
|
||||||
(BBT.got String V String.cmp key map)
|
|
||||||
|
|
||||||
String.Map.set
|
|
||||||
: ∀(V: *)
|
|
||||||
∀(key: String)
|
|
||||||
∀(val: V)
|
|
||||||
∀(map: (String.Map V))
|
|
||||||
(String.Map V)
|
|
||||||
= λV λkey λval λmap
|
|
||||||
(BBT.set String V String.cmp key val map)
|
|
||||||
|
|
||||||
String.Map.new
|
|
||||||
: ∀(V: *)
|
|
||||||
(String.Map V)
|
|
||||||
= λV (BBT.tip String V)
|
|
||||||
|
|
||||||
|
5
book/String.Map.new.kind2
Normal file
5
book/String.Map.new.kind2
Normal file
@ -0,0 +1,5 @@
|
|||||||
|
String.Map.new
|
||||||
|
: ∀(V: *)
|
||||||
|
(String.Map V)
|
||||||
|
= λV (BBT.tip String V)
|
||||||
|
|
9
book/String.Map.set.kind2
Normal file
9
book/String.Map.set.kind2
Normal file
@ -0,0 +1,9 @@
|
|||||||
|
String.Map.set
|
||||||
|
: ∀(V: *)
|
||||||
|
∀(key: String)
|
||||||
|
∀(val: V)
|
||||||
|
∀(map: (String.Map V))
|
||||||
|
(String.Map V)
|
||||||
|
= λV λkey λval λmap
|
||||||
|
(BBT.set String V String.cmp key val map)
|
||||||
|
|
4
book/_check_all.sh
Executable file
4
book/_check_all.sh
Executable file
@ -0,0 +1,4 @@
|
|||||||
|
for file in *.kind2; do
|
||||||
|
echo "checking ${file}"
|
||||||
|
kind2 check "${file%.*}"
|
||||||
|
done
|
@ -1,99 +0,0 @@
|
|||||||
Kind.all
|
|
||||||
: ∀(nam: String)
|
|
||||||
∀(inp: Kind.Term)
|
|
||||||
∀(bod: ∀(x: Kind.Term) Kind.Term)
|
|
||||||
Kind.Term
|
|
||||||
= λnam λinp λbod
|
|
||||||
~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
|
|
||||||
(all nam inp bod)Kind.ann
|
|
||||||
: ∀(val: Kind.Term)
|
|
||||||
∀(typ: Kind.Term)
|
|
||||||
Kind.Term
|
|
||||||
= λval λtyp
|
|
||||||
~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
|
|
||||||
(ann val typ)
|
|
||||||
Kind.app
|
|
||||||
: ∀(fun: Kind.Term)
|
|
||||||
∀(arg: Kind.Term)
|
|
||||||
Kind.Term
|
|
||||||
= λfun λarg
|
|
||||||
~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
|
|
||||||
(app fun arg)
|
|
||||||
Kind.def
|
|
||||||
: ∀(nam: String)
|
|
||||||
∀(val: Kind.Term)
|
|
||||||
∀(bod: ∀(x: Kind.Term) Kind.Term)
|
|
||||||
Kind.Term
|
|
||||||
= λnam λval λbod
|
|
||||||
~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
|
|
||||||
(def nam val bod)Kind.hol
|
|
||||||
: ∀(nam: String)
|
|
||||||
∀(ctx: (List Kind.Term))
|
|
||||||
Kind.Term
|
|
||||||
= λnam λctx
|
|
||||||
~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
|
|
||||||
(hol nam ctx)Kind.ins
|
|
||||||
: ∀(val: Kind.Term)
|
|
||||||
Kind.Term
|
|
||||||
= λval
|
|
||||||
~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
|
|
||||||
(ins val)Kind.lam
|
|
||||||
: ∀(nam: String)
|
|
||||||
∀(bod: ∀(x: Kind.Term) Kind.Term)
|
|
||||||
Kind.Term
|
|
||||||
= λnam λbod
|
|
||||||
~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
|
|
||||||
(lam nam bod)
|
|
||||||
Kind.mat
|
|
||||||
: ∀(nam: String)
|
|
||||||
∀(x: Kind.Term)
|
|
||||||
∀(z: Kind.Term)
|
|
||||||
∀(s: ∀(x: Kind.Term) Kind.Term)
|
|
||||||
∀(p: ∀(x: Kind.Term) Kind.Term)
|
|
||||||
Kind.Term
|
|
||||||
= λnam λx λz λs λp
|
|
||||||
~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
|
|
||||||
(mat nam x z s p)Kind.num
|
|
||||||
: ∀(val: #U60)
|
|
||||||
Kind.Term
|
|
||||||
= λval
|
|
||||||
~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
|
|
||||||
(num val)Kind.op2
|
|
||||||
: ∀(opr: Kind.Oper)
|
|
||||||
∀(fst: Kind.Term)
|
|
||||||
∀(snd: Kind.Term)
|
|
||||||
Kind.Term
|
|
||||||
= λopr λfst λsnd
|
|
||||||
~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
|
|
||||||
(op2 opr fst snd)Kind.ref
|
|
||||||
: ∀(nam: String)
|
|
||||||
∀(val: Kind.Term)
|
|
||||||
Kind.Term
|
|
||||||
= λnam λval
|
|
||||||
~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
|
|
||||||
(ref nam val)Kind.set
|
|
||||||
: Kind.Term
|
|
||||||
= ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
|
|
||||||
(set)
|
|
||||||
Kind.slf
|
|
||||||
: ∀(nam: String)
|
|
||||||
∀(bod: ∀(x: Kind.Term) Kind.Term)
|
|
||||||
Kind.Term
|
|
||||||
= λnam λbod
|
|
||||||
~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
|
|
||||||
(slf nam bod)Kind.txt
|
|
||||||
: ∀(lit: Kind.Text)
|
|
||||||
Kind.Term
|
|
||||||
= λlit
|
|
||||||
~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
|
|
||||||
(txt lit)Kind.u60
|
|
||||||
: Kind.Term
|
|
||||||
= ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
|
|
||||||
u60
|
|
||||||
Kind.var
|
|
||||||
: ∀(nam: String)
|
|
||||||
∀(idx: Nat)
|
|
||||||
Kind.Term
|
|
||||||
= λnam λidx
|
|
||||||
~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
|
|
||||||
(var nam idx)
|
|
@ -1,6 +1,6 @@
|
|||||||
test7.book
|
test7.book
|
||||||
: String
|
: String
|
||||||
= `
|
= "
|
||||||
Kind.Term
|
Kind.Term
|
||||||
: *
|
: *
|
||||||
= $self
|
= $self
|
||||||
@ -22,7 +22,7 @@ Kind.Term
|
|||||||
∀(hol: ∀(nam: String) ∀(ctx: (List Kind.Term)) (P (Kind.hol nam ctx)))
|
∀(hol: ∀(nam: String) ∀(ctx: (List Kind.Term)) (P (Kind.hol nam ctx)))
|
||||||
∀(var: ∀(nam: String) ∀(idx: Nat) (P (Kind.var nam idx)))
|
∀(var: ∀(nam: String) ∀(idx: Nat) (P (Kind.var nam idx)))
|
||||||
(P self)
|
(P self)
|
||||||
`
|
"
|
||||||
|
|
||||||
test7
|
test7
|
||||||
: (IO Unit)
|
: (IO Unit)
|
||||||
|
2
kind2.ts
2
kind2.ts
@ -409,8 +409,6 @@ export function main() {
|
|||||||
|
|
||||||
//const output = execSync("hvm1 run .kind2.hvm1 -s -L -1").toString();
|
//const output = execSync("hvm1 run .kind2.hvm1 -s -L -1").toString();
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
//for (let name in book) {
|
//for (let name in book) {
|
||||||
//console.log("Checking: " + name);
|
//console.log("Checking: " + name);
|
||||||
|
|
||||||
|
@ -29,14 +29,15 @@
|
|||||||
//| (Txt txt)
|
//| (Txt txt)
|
||||||
//| (Hol nam ctx val)
|
//| (Hol nam ctx val)
|
||||||
//| (Var nam idx)
|
//| (Var nam idx)
|
||||||
|
//| (Src src val)
|
||||||
|
|
||||||
// Prelude
|
// Prelude
|
||||||
// -------
|
// -------
|
||||||
|
|
||||||
(Debug dep [] value) = value
|
(Debug dep [] value) = value
|
||||||
(Debug dep msg value) = (HVM.print (Join msg) value)
|
(Debug dep msg value) = (HVM.print (String.join msg) value)
|
||||||
//(Debug dep [] value) = value
|
//(Debug dep [] value) = value
|
||||||
//(Debug dep msg value) = (If (> dep 10) 1 (HVM.print (Join msg) value))
|
//(Debug dep msg value) = (If (> dep 10) 1 (HVM.print (String.join msg) value))
|
||||||
|
|
||||||
(NewLine) = (String.cons 10 String.nil)
|
(NewLine) = (String.cons 10 String.nil)
|
||||||
(Quote) = (String.cons 34 String.nil)
|
(Quote) = (String.cons 34 String.nil)
|
||||||
@ -70,23 +71,50 @@
|
|||||||
(Find name List.nil) = None
|
(Find name List.nil) = None
|
||||||
(Find name (List.cons (Pair nam val) tail)) = (If (Same nam name) (Some val) (Find name tail))
|
(Find name (List.cons (Pair nam val) tail)) = (If (Same nam name) (Some val) (Find name tail))
|
||||||
|
|
||||||
(Concat String.nil ys) = ys
|
(String.concat String.nil ys) = ys
|
||||||
(Concat (String.cons x xs) ys) = (String.cons x (Concat xs ys))
|
(String.concat (String.cons x xs) ys) = (String.cons x (String.concat xs ys))
|
||||||
|
|
||||||
(Join List.nil) = ""
|
(String.join List.nil) = ""
|
||||||
(Join (List.cons x xs)) = (Concat x (Join xs))
|
(String.join (List.cons x xs)) = (String.concat x (String.join xs))
|
||||||
|
|
||||||
(Fst (Pair fst snd)) = fst
|
(Pair.fst (Pair fst snd)) = fst
|
||||||
(Snd (Pair fst snd)) = snd
|
(Pair.snd (Pair fst snd)) = snd
|
||||||
|
|
||||||
(Get (Pair fst snd) fun) = (fun fst snd)
|
(Pair.get (Pair fst snd) fun) = (fun fst snd)
|
||||||
|
|
||||||
(Pure x) = (Some x)
|
(Maybe.pure x) = (Some x)
|
||||||
|
|
||||||
(Bind a b) = (Bind.match a b)
|
(Maybe.bind a b) = (Maybe.bind.match a b)
|
||||||
|
|
||||||
(Bind.match None b) = None
|
(Maybe.bind.match None b) = None
|
||||||
(Bind.match (Some a) b) = (b a)
|
(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
|
// Evaluation
|
||||||
// ----------
|
// ----------
|
||||||
@ -99,6 +127,7 @@
|
|||||||
(Reduce r (Op2 opr fst snd)) = (Reduce.op2 r opr fst snd)
|
(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 r (Mat nam x z s p)) = (Reduce.mat r nam x z s p)
|
||||||
(Reduce 1 (Txt txt)) = (Reduce.txt 1 txt)
|
(Reduce 1 (Txt txt)) = (Reduce.txt 1 txt)
|
||||||
|
(Reduce r (Src src val)) = (Reduce r val)
|
||||||
(Reduce r val) = val
|
(Reduce r val) = val
|
||||||
|
|
||||||
(Reduce.app r (Lam nam bod) arg) = (Reduce r (bod (Reduce 0 arg)))
|
(Reduce.app r (Lam nam bod) arg) = (Reduce r (bod (Reduce 0 arg)))
|
||||||
@ -147,27 +176,27 @@
|
|||||||
(Normal.term r U60 dep) = U60
|
(Normal.term r U60 dep) = U60
|
||||||
(Normal.term r (Num val) dep) = (Num val)
|
(Normal.term r (Num val) dep) = (Num val)
|
||||||
(Normal.term r (Op2 opr fst snd) dep) = (Op2 opr (Normal.term r fst dep) (Normal.term r snd dep))
|
(Normal.term r (Op2 opr fst snd) dep) = (Op2 opr (Normal.term r fst dep) (Normal.term r snd dep))
|
||||||
(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))
|
(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 (String.concat nam "-1") dep)) dep) λk(Normal r (p (Var nam dep)) dep))
|
||||||
(Normal.term r (Txt val) dep) = (Txt val)
|
(Normal.term r (Txt val) dep) = (Txt val)
|
||||||
(Normal.term r (Var nam idx) dep) = (Var nam idx)
|
(Normal.term r (Var nam idx) dep) = (Var nam idx)
|
||||||
|
(Normal.term r (Src src val) dep) = (Src src (Normal r val dep))
|
||||||
|
|
||||||
// Equality
|
// Equality
|
||||||
// --------
|
// --------
|
||||||
|
|
||||||
// Check if two terms are identical. If not...
|
// Check if two terms are identical. If not...
|
||||||
//(Equal a b 8) = 0 // limits depth FIXME: won't be necessary with better ref-ids equality
|
|
||||||
(Equal a b dep) = (Equal.minor (Identical a b dep) a b dep)
|
(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...
|
// Check if they're identical after a minor weak reduction. If not...
|
||||||
(Equal.minor 0 a b dep) = let a = (Reduce 0 a); let b = (Reduce 0 b); (Equal.major (Identical a b dep) a b dep)
|
(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
|
(Equal.minor 1 a b dep) = 1
|
||||||
|
|
||||||
// Check if they're identical after a major weak reduction. If not...
|
// Check if they're identical after a major weak reduction. If not...
|
||||||
(Equal.major 0 a b dep) = let a = (Reduce 1 a); let b = (Reduce 1 b); (Equal.enter (Identical a b dep) a b dep)
|
(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
|
(Equal.major 1 a b dep) = 1
|
||||||
|
|
||||||
// Check if they become identical after reducing fields.
|
// 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 0 a b dep) = (Comparer λaλbλdep(Equal a b dep) (Reduce 0 a) (Reduce 0 b) dep)
|
||||||
(Equal.enter 1 a b dep) = 1
|
(Equal.enter 1 a b dep) = 1
|
||||||
|
|
||||||
// Checks if two terms are identical, without reductions.
|
// Checks if two terms are identical, without reductions.
|
||||||
@ -193,8 +222,10 @@
|
|||||||
(Comparer rec U60 U60 dep) = 1
|
(Comparer rec U60 U60 dep) = 1
|
||||||
(Comparer rec (Num a.val) (Num b.val) dep) = (== a.val b.val)
|
(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 b.fst dep) (rec a.snd b.snd dep))
|
(Comparer rec (Op2 a.opr a.fst a.snd) (Op2 b.opr b.fst b.snd) dep) = (& (rec a.fst b.fst dep) (rec a.snd 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 (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 (String.concat a.nam "-1") dep)) (b.s (Var (String.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 (Txt a.txt) (Txt b.txt) dep) = (Same a.txt b.txt)
|
||||||
|
(Comparer rec (Src a.src a.val) b dep) = (Comparer rec a.val b dep)
|
||||||
|
(Comparer rec a (Src b.src b.val) dep) = (Comparer rec a b.val dep)
|
||||||
(Comparer rec a b dep) = 0
|
(Comparer rec a b dep) = 0
|
||||||
//(Comparer rec a b dep) = (HVM.log (NOP (Show a dep) (Show b dep)) 0)
|
//(Comparer rec a b dep) = (HVM.log (NOP (Show a dep) (Show b dep)) 0)
|
||||||
|
|
||||||
@ -211,29 +242,29 @@
|
|||||||
(Infer term dep) = (Infer.match term dep)
|
(Infer term dep) = (Infer.match term dep)
|
||||||
|
|
||||||
(Infer.match (All nam inp bod) dep) =
|
(Infer.match (All nam inp bod) dep) =
|
||||||
(Bind (Check inp Set dep) λinp_typ
|
(Maybe.bind (Check 0 inp Set dep) λinp_typ
|
||||||
(Bind (Check (bod (Ann (Var nam dep) inp)) Set (+ 1 dep)) λbod_typ
|
(Maybe.bind (Check 0 (bod (Ann (Var nam dep) inp)) Set (+ 1 dep)) λbod_typ
|
||||||
(Pure Set)))
|
(Maybe.pure Set)))
|
||||||
(Infer.match (Lam nam bod) dep) =
|
(Infer.match (Lam nam bod) dep) =
|
||||||
(Debug dep ["Error: NonFunLam " (Show (Lam nam bod) dep)] (None))
|
(Debug dep ["Error: NonFunLam " (Show (Lam nam bod) dep)] (None))
|
||||||
(Infer.match (App fun arg) dep) =
|
(Infer.match (App fun arg) dep) =
|
||||||
(Bind (Infer fun dep) λfun_typ
|
(Maybe.bind (Infer fun dep) λfun_typ
|
||||||
((IfAll (Reduce 1 fun_typ)
|
((IfAll (Reduce 1 fun_typ)
|
||||||
λfun_nam λfun_typ.inp λfun_typ.bod λfun λarg
|
λfun_nam λfun_typ.inp λfun_typ.bod λfun λarg
|
||||||
(Bind (Check arg fun_typ.inp dep) λval_typ
|
(Maybe.bind (Check 0 arg fun_typ.inp dep) λval_typ
|
||||||
(Pure (fun_typ.bod arg)))
|
(Maybe.pure (fun_typ.bod arg)))
|
||||||
λfun λarg
|
λfun λarg
|
||||||
(Debug dep ["Error: NonFunApp " (Show (App fun arg) dep)] None))
|
(Debug dep ["Error: NonFunApp " (Show (App fun arg) dep)] None))
|
||||||
fun arg))
|
fun arg))
|
||||||
(Infer.match (Ann val typ) dep) =
|
(Infer.match (Ann val typ) dep) =
|
||||||
(Pure typ)
|
(Maybe.pure typ)
|
||||||
(Infer.match (Slf nam bod) dep) =
|
(Infer.match (Slf nam bod) dep) =
|
||||||
(Bind (Check (bod (Ann (Var nam dep) (Slf nam bod))) Set (+ dep 1)) λslf
|
(Maybe.bind (Check 0 (bod (Ann (Var nam dep) (Slf nam bod))) Set (+ dep 1)) λslf
|
||||||
(Pure Set))
|
(Maybe.pure Set))
|
||||||
(Infer.match (Ins val) dep) =
|
(Infer.match (Ins val) dep) =
|
||||||
(Bind (Infer val dep) λval_typ
|
(Maybe.bind (Infer val dep) λval_typ
|
||||||
((IfSlf (Reduce 1 val_typ)
|
((IfSlf (Reduce 1 val_typ)
|
||||||
λval_nam λval_typ.bod λval (Pure (val_typ.bod (Ins val)))
|
λval_nam λval_typ.bod λval (Maybe.pure (val_typ.bod (Ins val)))
|
||||||
λval (Debug dep ["Error: NonSlfIns " (Show (Ins val) dep)] None))
|
λval (Debug dep ["Error: NonSlfIns " (Show (Ins val) dep)] None))
|
||||||
val))
|
val))
|
||||||
(Infer.match (Ref nam val) dep) =
|
(Infer.match (Ref nam val) dep) =
|
||||||
@ -241,99 +272,103 @@
|
|||||||
(Infer.match (Let nam val bod) dep) =
|
(Infer.match (Let nam val bod) dep) =
|
||||||
(Debug dep ["Error: NonAnnLet " (Show (Let nam val bod) dep)] (None))
|
(Debug dep ["Error: NonAnnLet " (Show (Let nam val bod) dep)] (None))
|
||||||
(Infer.match Set dep) =
|
(Infer.match Set dep) =
|
||||||
(Pure Set)
|
(Maybe.pure Set)
|
||||||
(Infer.match U60 dep) =
|
(Infer.match U60 dep) =
|
||||||
(Pure Set)
|
(Maybe.pure Set)
|
||||||
(Infer.match (Num num) dep) =
|
(Infer.match (Num num) dep) =
|
||||||
(Pure U60)
|
(Maybe.pure U60)
|
||||||
(Infer.match (Txt txt) dep) =
|
(Infer.match (Txt txt) dep) =
|
||||||
(Pure Book.String)
|
(Maybe.pure Book.String)
|
||||||
(Infer.match (Op2 opr fst snd) dep) =
|
(Infer.match (Op2 opr fst snd) dep) =
|
||||||
(Bind (Check fst U60 dep) λfst
|
(Maybe.bind (Check 0 fst U60 dep) λfst
|
||||||
(Bind (Check snd U60 dep) λsnd
|
(Maybe.bind (Check 0 snd U60 dep) λsnd
|
||||||
(Pure U60)))
|
(Maybe.pure U60)))
|
||||||
// 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) =
|
(Infer.match (Mat nam x z s p) dep) =
|
||||||
(Bind (Check x U60 dep) λx_typ
|
(Maybe.bind (Check 0 x U60 dep) λx_typ
|
||||||
(Bind (Check (p (Ann (Var nam dep) U60)) Set dep) λp_typ
|
(Maybe.bind (Check 0 (p (Ann (Var nam dep) U60)) Set dep) λp_typ
|
||||||
(Bind (Check z (p (Num 0)) dep) λz_typ
|
(Maybe.bind (Check 0 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
|
(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
|
||||||
(Pure (p x))))))
|
(Maybe.pure (p x))))))
|
||||||
(Infer.match (Hol nam ctx) dep) =
|
(Infer.match (Hol nam ctx) dep) =
|
||||||
(Debug dep ["Error: NonAnnHol " (Show (Hol nam ctx) dep)] None)
|
(Debug dep ["Error: NonAnnHol " (Show (Hol nam ctx) dep)] None)
|
||||||
(Infer.match (Var nam idx) dep) =
|
(Infer.match (Var nam idx) dep) =
|
||||||
(Debug dep ["Error: NonAnnVar " (Show (Var nam idx) dep)] None)
|
(Debug dep ["Error: NonAnnVar " (Show (Var nam idx) dep)] None)
|
||||||
|
(Infer.match (Src src val) dep) =
|
||||||
|
(Infer.match val dep)
|
||||||
|
|
||||||
//(Check term type dep) = (Debug dep ["Check: " (Show term dep) " :: " (Show type dep)] (Check.match term type dep))
|
//(Check term type dep) = (Debug dep ["Check: " (Show term dep) " :: " (Show type dep)] (Check.match 0 term type dep))
|
||||||
(Check term type dep) = (Check.match term type dep)
|
(Check src term type dep) = (Check.match src term type dep)
|
||||||
|
|
||||||
(Check.match (Lam term.nam term.bod) type dep) =
|
(Check.match src (Lam term.nam term.bod) type dep) =
|
||||||
((IfAll (Reduce 1 type)
|
((IfAll (Reduce 1 type)
|
||||||
λtype.nam λtype.inp λtype.bod λterm.bod
|
λtype.nam λtype.inp λtype.bod λterm.bod
|
||||||
let ann = (Ann (Var term.nam dep) type.inp)
|
let ann = (Ann (Var term.nam dep) type.inp)
|
||||||
let term = (term.bod ann)
|
let term = (term.bod ann)
|
||||||
let type = (type.bod ann)
|
let type = (type.bod ann)
|
||||||
(Check term type (+ dep 1))
|
(Check 0 term type (+ dep 1))
|
||||||
λterm.bod
|
λterm.bod
|
||||||
(Infer (Lam term.nam term.bod) dep))
|
(Infer (Lam term.nam term.bod) dep))
|
||||||
term.bod)
|
term.bod)
|
||||||
(Check.match (Ins term.val) type dep) =
|
(Check.match src (Ins term.val) type dep) =
|
||||||
((IfSlf (Reduce 1 type)
|
((IfSlf (Reduce 1 type)
|
||||||
λtype.nam λtype.bod λterm.val (Check term.val (type.bod (Ins term.val)) dep)
|
λtype.nam λtype.bod λterm.val (Check 0 term.val (type.bod (Ins term.val)) dep)
|
||||||
λterm.val (Infer (Ins term.val) dep))
|
λterm.val (Infer (Ins term.val) dep))
|
||||||
term.val)
|
term.val)
|
||||||
(Check.match (Let term.nam term.val term.bod) type dep) =
|
(Check.match src (Let term.nam term.val term.bod) type dep) =
|
||||||
(Check (term.bod term.val) type (+ 1 dep))
|
(Check 0 (term.bod term.val) type (+ 1 dep))
|
||||||
(Check.match (Hol term.nam term.ctx) type dep) =
|
(Check.match src (Hol term.nam term.ctx) type dep) =
|
||||||
(Debug dep ["HOLE!: ?" term.nam " :: " (Show (Normal 0 type dep) dep) (Context.show term.ctx dep)]
|
(Debug dep [(String.color BRIGHT) "HOLE: ?" term.nam " :: " (Show (Normal 0 type dep) dep) (String.color RESET) (Context.show term.ctx dep)]
|
||||||
(Pure 0))
|
(Maybe.pure 0))
|
||||||
(Check.match (Ref term.nam (Ann term.val term.typ)) type dep) = // better printing
|
(Check.match src (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.report src (Equal type term.typ dep) term.typ type (Ref term.nam term.val) dep)
|
||||||
//(Check.match (Ref term.nam term.val) type 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 term.val type dep)
|
||||||
(Check.match term type dep) =
|
(Check.match src term type dep) =
|
||||||
(Check.verify term type dep)
|
(Check.verify src term type dep)
|
||||||
|
|
||||||
(Check.verify term type dep) =
|
(Check.verify src term type dep) =
|
||||||
(Bind (Infer term dep) λinfer
|
(Maybe.bind (Infer term dep) λinfer
|
||||||
(Check.report (Equal type infer dep) infer type term dep))
|
(Check.report src (Equal type infer dep) infer type term dep))
|
||||||
|
|
||||||
(Check.report 0 inferred expected value dep) =
|
(Check.report src 0 detected expected value dep) =
|
||||||
let inf = (Show (Normal 0 inferred dep) dep)
|
let det = (Show (Normal 0 detected dep) dep)
|
||||||
let exp = (Show (Normal 0 expected dep) dep)
|
let exp = (Show (Normal 0 expected dep) dep)
|
||||||
let val = (Show (Normal 0 value dep) dep)
|
let val = (Show (Normal 0 value dep) dep)
|
||||||
(Debug dep ["Error: " inf NewLine " != " exp NewLine " in " val] None)
|
(Debug dep [(String.color BRIGHT) "TYPE_MISMATCH" NewLine
|
||||||
(Check.report n inferred expected value dep) =
|
"- expected: " (String.color RESET) (String.color GREEN) exp NewLine (String.color RESET) (String.color BRIGHT)
|
||||||
(Pure 0)
|
"- 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
|
// Syntax
|
||||||
// ------
|
// ------
|
||||||
|
|
||||||
(Show (All nam inp bod) dep) = (Join ["∀(" nam ": " (Show inp dep) ") " (Show (bod (Var nam dep)) (+ dep 1))])
|
(Show (All nam inp bod) dep) = (String.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 (Lam nam bod) dep) = (String.join ["λ" nam " " (Show (bod (Var nam dep)) (+ dep 1))])
|
||||||
(Show (App fun arg) dep) = (Join ["(" (Show.unwrap (Show fun dep)) " " (Show arg dep) ")"])
|
(Show (App fun arg) dep) = (String.join ["(" (Show.unwrap (Show fun dep)) " " (Show arg dep) ")"])
|
||||||
(Show (Ann val typ) dep) = (Join ["{" (Show val dep) ": " (Show typ dep) "}"])
|
(Show (Ann val typ) dep) = (String.join ["{" (Show val dep) ": " (Show typ dep) "}"])
|
||||||
(Show (Slf nam bod) dep) = (Join ["$" nam " " (Show (bod (Var nam dep)) (+ dep 1))])
|
(Show (Slf nam bod) dep) = (String.join ["$" nam " " (Show (bod (Var nam dep)) (+ dep 1))])
|
||||||
(Show (Ins val) dep) = (Join ["~" (Show val dep)])
|
(Show (Ins val) dep) = (String.join ["~" (Show val dep)])
|
||||||
(Show (Ref nam val) dep) = nam
|
(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 (Let nam val bod) dep) = (String.join ["let " nam " = " (Show val dep) "; " (Show (bod (Var nam dep)) (+ dep 1))])
|
||||||
(Show Set dep) = (Join ["*"])
|
(Show Set dep) = (String.join ["*"])
|
||||||
(Show U60 dep) = "#U60"
|
(Show U60 dep) = "#U60"
|
||||||
(Show (Num val) dep) = (Join ["#" (U60.show val)])
|
(Show (Num val) dep) = (String.join ["#" (U60.show val)])
|
||||||
(Show (Op2 opr fst snd) dep) = (Join ["#(" (Op2.show opr) " " (Show fst dep) " " (Show snd dep) ")"])
|
(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) = (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)])
|
(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) = (Join [Quote txt Quote])
|
(Show (Txt txt) dep) = (String.join [Quote txt Quote])
|
||||||
(Show (Hol nam ctx) dep) = (Join ["?" nam])
|
(Show (Hol nam ctx) dep) = (String.join ["?" nam])
|
||||||
(Show (Var nam idx) dep) = (Join [nam])
|
(Show (Var nam idx) dep) = (String.join [nam])
|
||||||
//(Show (Var nam idx) dep) = (Join [nam "'" (U60.show idx)])
|
(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.nil dep) = ""
|
||||||
(Show.many (List.cons x xs) dep) = (Join [" " (Show x dep) (Show.many xs 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 (String.cons ' ' xs)) = xs
|
||||||
(Show.trim str) = str
|
(Show.trim str) = str
|
||||||
@ -351,11 +386,11 @@
|
|||||||
(Op2.show DIV) = "/"
|
(Op2.show DIV) = "/"
|
||||||
|
|
||||||
(Context.show List.nil dep) = ""
|
(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 (List.cons x xs) dep) = (String.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 (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 term dep) = (Show (Normal 0 term dep) dep)
|
||||||
//(Context.show.ann val dep) = (Join ["{" (Show (Normal 0 val dep) dep) ": " (Show (Normal 0 (Infer val dep) dep) dep) "}"])
|
//(Context.show.ann val dep) = (String.join ["{" (Show (Normal 0 val dep) dep) ": " (Show (Normal 0 (Infer val dep) dep) dep) "}"])
|
||||||
|
|
||||||
// Compilation
|
// Compilation
|
||||||
// -----------
|
// -----------
|
||||||
@ -388,6 +423,7 @@ Compile.primitives = [
|
|||||||
(Compile (Txt txt)) = (Str.make txt)
|
(Compile (Txt txt)) = (Str.make txt)
|
||||||
(Compile (Hol nam ctx)) = 0
|
(Compile (Hol nam ctx)) = 0
|
||||||
(Compile (Var nam val)) = val
|
(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.cons x xs)) = (App (App Book.String.cons (Num x)) (Compile.txt xs))
|
||||||
//(Compile.txt String.nil) = Book.String.nil
|
//(Compile.txt String.nil) = Book.String.nil
|
||||||
@ -420,12 +456,22 @@ Compile.primitives = [
|
|||||||
|
|
||||||
(Normalizer (Ref nam val)) = (Normalizer val)
|
(Normalizer (Ref nam val)) = (Normalizer val)
|
||||||
(Normalizer (Ann val typ)) = (Normalizer val)
|
(Normalizer (Ann val typ)) = (Normalizer val)
|
||||||
|
(Normalizer (Src src val)) = (Normalizer val)
|
||||||
(Normalizer val) = (Compile val)
|
(Normalizer val) = (Compile val)
|
||||||
//(Normalizer val) = (Str.view (Compile val))
|
//(Normalizer val) = (Str.view (Compile val))
|
||||||
|
|
||||||
(Checker (Ref nam val)) = (Checker val)
|
(Checker name (Ref nam val)) = (Checker name val)
|
||||||
(Checker (Ann val typ)) = (Checker.report (Check val typ 0))
|
(Checker name (Src src (Ann val typ))) = (Checker.report name (Check src val typ 0))
|
||||||
(Checker val) = (Checker.report (Infer val 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 (Some x)) = (HVM.print "Check!" OK)
|
(Checker.report name (Some x)) = 1
|
||||||
(Checker.report None) = (HVM.print "Error." ERR)
|
(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)
|
335
src/main.rs
335
src/main.rs
@ -3,6 +3,11 @@
|
|||||||
use TSPL::Parser;
|
use TSPL::Parser;
|
||||||
use std::collections::HashMap;
|
use std::collections::HashMap;
|
||||||
use std::collections::HashSet;
|
use std::collections::HashSet;
|
||||||
|
use std::env;
|
||||||
|
use std::fs::File;
|
||||||
|
use std::io::Write;
|
||||||
|
use std::process::Command;
|
||||||
|
use highlight_error::highlight_error;
|
||||||
//use std::fmt;
|
//use std::fmt;
|
||||||
|
|
||||||
#[derive(Clone, Copy)]
|
#[derive(Clone, Copy)]
|
||||||
@ -31,10 +36,12 @@ enum Term {
|
|||||||
Let { nam: String, val: Box<Term>, bod: Box<Term> },
|
Let { nam: String, val: Box<Term>, bod: Box<Term> },
|
||||||
Hol { nam: String },
|
Hol { nam: String },
|
||||||
Var { nam: String },
|
Var { nam: String },
|
||||||
|
Src { src: u64, val: Box<Term> },
|
||||||
}
|
}
|
||||||
|
|
||||||
struct Book {
|
struct Book {
|
||||||
defs: HashMap<String, Term>,
|
defs: HashMap<String, Term>,
|
||||||
|
fids: HashMap<String, u64>,
|
||||||
}
|
}
|
||||||
|
|
||||||
// NOT USED ANYMORE
|
// NOT USED ANYMORE
|
||||||
@ -49,6 +56,22 @@ struct Book {
|
|||||||
//name
|
//name
|
||||||
//}
|
//}
|
||||||
|
|
||||||
|
pub fn new_src(fid: u64, ini: u64, end: u64) -> u64 {
|
||||||
|
(fid << 40) | (ini << 20) | end
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn src_fid(src: u64) -> u64 {
|
||||||
|
src >> 40
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn src_ini(src: u64) -> u64 {
|
||||||
|
(src >> 20) & 0xFFFFF
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn src_end(src: u64) -> u64 {
|
||||||
|
src & 0xFFFFF
|
||||||
|
}
|
||||||
|
|
||||||
pub fn cons<A>(vector: &im::Vector<A>, value: A) -> im::Vector<A> where A: Clone {
|
pub fn cons<A>(vector: &im::Vector<A>, value: A) -> im::Vector<A> where A: Clone {
|
||||||
let mut new_vector = vector.clone();
|
let mut new_vector = vector.clone();
|
||||||
new_vector.push_back(value);
|
new_vector.push_back(value);
|
||||||
@ -117,26 +140,31 @@ impl Term {
|
|||||||
Term::Let { nam, val, bod } => format!("let {} = {} in {}", nam, val.show(), bod.show()),
|
Term::Let { nam, val, bod } => format!("let {} = {} in {}", nam, val.show(), bod.show()),
|
||||||
Term::Hol { nam } => format!("?{}", nam),
|
Term::Hol { nam } => format!("?{}", nam),
|
||||||
Term::Var { nam } => nam.clone(),
|
Term::Var { nam } => nam.clone(),
|
||||||
|
Term::Src { src: _, val } => val.show(),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn to_hvm1(&self, env: im::Vector<String>) -> String {
|
fn to_hvm1(&self, env: im::Vector<String>) -> String {
|
||||||
|
fn binder(name: &str) -> String {
|
||||||
|
format!("_{}", name.replace("-", "._."))
|
||||||
|
}
|
||||||
match self {
|
match self {
|
||||||
Term::All { nam, inp, bod } => format!("(All \"{}\" {} λ{} {})", nam, inp.to_hvm1(env.clone()), nam, bod.to_hvm1(cons(&env, nam.clone()))),
|
Term::All { nam, inp, bod } => format!("(All \"{}\" {} λ{} {})", nam, inp.to_hvm1(env.clone()), binder(nam), bod.to_hvm1(cons(&env, nam.clone()))),
|
||||||
Term::Lam { nam, bod } => format!("(Lam \"{}\" λ{} {})", nam, nam, bod.to_hvm1(cons(&env, nam.clone()))),
|
Term::Lam { nam, bod } => format!("(Lam \"{}\" λ{} {})", nam, binder(nam), bod.to_hvm1(cons(&env, nam.clone()))),
|
||||||
Term::App { fun, arg } => format!("(App {} {})", fun.to_hvm1(env.clone()), arg.to_hvm1(env.clone())),
|
Term::App { fun, arg } => format!("(App {} {})", fun.to_hvm1(env.clone()), arg.to_hvm1(env.clone())),
|
||||||
Term::Ann { val, typ } => format!("(Ann {} {})", val.to_hvm1(env.clone()), typ.to_hvm1(env.clone())),
|
Term::Ann { val, typ } => format!("(Ann {} {})", val.to_hvm1(env.clone()), typ.to_hvm1(env.clone())),
|
||||||
Term::Slf { nam, bod } => format!("(Slf \"{}\" λ{} {})", nam, nam, bod.to_hvm1(cons(&env, nam.clone()))),
|
Term::Slf { nam, bod } => format!("(Slf \"{}\" λ{} {})", nam, binder(nam), bod.to_hvm1(cons(&env, nam.clone()))),
|
||||||
Term::Ins { val } => format!("(Ins {})", val.to_hvm1(env.clone())),
|
Term::Ins { val } => format!("(Ins {})", val.to_hvm1(env.clone())),
|
||||||
Term::Set => "(Set)".to_string(),
|
Term::Set => "(Set)".to_string(),
|
||||||
Term::U60 => "(U60)".to_string(),
|
Term::U60 => "(U60)".to_string(),
|
||||||
Term::Num { val } => format!("(Num {})", val),
|
Term::Num { val } => format!("(Num {})", val),
|
||||||
Term::Op2 { opr, fst, snd } => format!("(Op2 {} {} {})", opr.to_hvm1(), fst.to_hvm1(env.clone()), snd.to_hvm1(env.clone())),
|
Term::Op2 { opr, fst, snd } => format!("(Op2 {} {} {})", opr.to_hvm1(), fst.to_hvm1(env.clone()), snd.to_hvm1(env.clone())),
|
||||||
Term::Mat { nam, x, z, s, p } => format!("(Mat \"{}\" {} {} λ{} {} λ{} {})", nam, x.to_hvm1(env.clone()), z.to_hvm1(env.clone()), nam, s.to_hvm1(cons(&env, nam.clone())), nam, p.to_hvm1(cons(&env, nam.clone()))),
|
Term::Mat { nam, x, z, s, p } => format!("(Mat \"{}\" {} {} λ{} {} λ{} {})", nam, x.to_hvm1(env.clone()), z.to_hvm1(env.clone()), binder(&format!("{}-1",nam)), s.to_hvm1(cons(&env, format!("{}-1",nam))), binder(nam), p.to_hvm1(cons(&env, nam.clone()))),
|
||||||
Term::Txt { txt } => format!("(Txt \"{}\")", txt),
|
Term::Txt { txt } => format!("(Txt \"{}\")", txt),
|
||||||
Term::Let { nam, val, bod } => format!("(Let \"{}\" {} λ{} {})", nam, val.to_hvm1(env.clone()), nam, bod.to_hvm1(cons(&env, nam.clone()))),
|
Term::Let { nam, val, bod } => format!("(Let \"{}\" {} λ{} {})", nam, val.to_hvm1(env.clone()), binder(nam), bod.to_hvm1(cons(&env, nam.clone()))),
|
||||||
Term::Hol { nam } => format!("(Hol \"{}\" [{}])", nam, env.iter().map(|n| format!("\"{}\"", n)).collect::<Vec<_>>().join(",")),
|
Term::Hol { nam } => format!("(Hol \"{}\" [{}])", nam, env.iter().map(|n| binder(n)).collect::<Vec<_>>().join(",")),
|
||||||
Term::Var { nam } => if env.contains(nam) { nam.clone() } else { format!("(Book.{})", nam) },
|
Term::Var { nam } => if env.contains(nam) { format!("{}", binder(nam)) } else { format!("(Book.{})", nam) },
|
||||||
|
Term::Src { src, val } => format!("(Src {} {})", src, val.to_hvm1(env)),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -173,7 +201,7 @@ impl Term {
|
|||||||
Term::Mat { nam, x, z, s, p } => {
|
Term::Mat { nam, x, z, s, p } => {
|
||||||
x.get_free_vars(env.clone(), free);
|
x.get_free_vars(env.clone(), free);
|
||||||
z.get_free_vars(env.clone(), free);
|
z.get_free_vars(env.clone(), free);
|
||||||
s.get_free_vars(cons(&env, nam.clone()), free);
|
s.get_free_vars(cons(&env, format!("{}-1",nam)), free);
|
||||||
p.get_free_vars(cons(&env, nam.clone()), free);
|
p.get_free_vars(cons(&env, nam.clone()), free);
|
||||||
},
|
},
|
||||||
Term::Txt { txt: _ } => {},
|
Term::Txt { txt: _ } => {},
|
||||||
@ -182,6 +210,9 @@ impl Term {
|
|||||||
bod.get_free_vars(cons(&env, nam.clone()), free);
|
bod.get_free_vars(cons(&env, nam.clone()), free);
|
||||||
},
|
},
|
||||||
Term::Hol { nam: _ } => {},
|
Term::Hol { nam: _ } => {},
|
||||||
|
Term::Src { src: _, val } => {
|
||||||
|
val.get_free_vars(env, free);
|
||||||
|
},
|
||||||
Term::Var { nam } => {
|
Term::Var { nam } => {
|
||||||
if !env.contains(nam) {
|
if !env.contains(nam) {
|
||||||
free.insert(nam.clone());
|
free.insert(nam.clone());
|
||||||
@ -202,120 +233,151 @@ impl<'i> KindParser<'i> {
|
|||||||
Some('*') => { self.advance_one(); Ok(Oper::Mul) }
|
Some('*') => { self.advance_one(); Ok(Oper::Mul) }
|
||||||
Some('/') => { self.advance_one(); Ok(Oper::Div) }
|
Some('/') => { self.advance_one(); Ok(Oper::Div) }
|
||||||
Some('%') => { self.advance_one(); Ok(Oper::Mod) }
|
Some('%') => { self.advance_one(); Ok(Oper::Mod) }
|
||||||
Some('=') => { self.consume("=")?; Ok(Oper::Eq) }
|
Some('=') => { self.consume("==")?; Ok(Oper::Eq) }
|
||||||
Some('!') => { self.consume("!=")?; Ok(Oper::Ne) }
|
Some('!') => { self.consume("!=")?; Ok(Oper::Ne) }
|
||||||
Some('<') => {
|
Some('<') => {
|
||||||
match self.peek_many(2) {
|
match self.peek_many(2) {
|
||||||
Some("<=") => { self.advance_many(2); Ok(Oper::Lte) }
|
Some("<=") => { self.advance_many(2); Ok(Oper::Lte) }
|
||||||
|
Some("<<") => { self.advance_many(2); Ok(Oper::Lsh) }
|
||||||
_ => { self.advance_one(); Ok(Oper::Lt) }
|
_ => { self.advance_one(); Ok(Oper::Lt) }
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
Some('>') => {
|
Some('>') => {
|
||||||
match self.peek_many(2) {
|
match self.peek_many(2) {
|
||||||
Some(">=") => { self.advance_many(2); Ok(Oper::Gte) }
|
Some(">=") => { self.advance_many(2); Ok(Oper::Gte) }
|
||||||
|
Some(">>") => { self.advance_many(2); Ok(Oper::Rsh) }
|
||||||
_ => { self.advance_one(); Ok(Oper::Gt) }
|
_ => { self.advance_one(); Ok(Oper::Gt) }
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
Some('&') => { self.advance_one(); Ok(Oper::And) }
|
Some('&') => { self.advance_one(); Ok(Oper::And) }
|
||||||
Some('|') => { self.advance_one(); Ok(Oper::Or) }
|
Some('|') => { self.advance_one(); Ok(Oper::Or) }
|
||||||
Some('^') => { self.advance_one(); Ok(Oper::Xor) }
|
Some('^') => { self.advance_one(); Ok(Oper::Xor) }
|
||||||
Some('l') => { self.consume("<<")?; Ok(Oper::Lsh) }
|
|
||||||
Some('r') => { self.consume(">>")?; Ok(Oper::Rsh) }
|
|
||||||
_ => self.expected("operator"),
|
_ => self.expected("operator"),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn parse_term(&mut self) -> Result<Term, String> {
|
fn parse_term(&mut self, fid: u64) -> Result<Term, String> {
|
||||||
self.skip_trivia();
|
self.skip_trivia();
|
||||||
match self.peek_one() {
|
match self.peek_one() {
|
||||||
Some('∀') => {
|
Some('∀') => {
|
||||||
|
let ini = *self.index() as u64;
|
||||||
self.consume("∀")?;
|
self.consume("∀")?;
|
||||||
self.consume("(")?;
|
self.consume("(")?;
|
||||||
let nam = self.parse_name()?;
|
let nam = self.parse_name()?;
|
||||||
self.consume(":")?;
|
self.consume(":")?;
|
||||||
let inp = Box::new(self.parse_term()?);
|
let inp = Box::new(self.parse_term(fid)?);
|
||||||
self.consume(")")?;
|
self.consume(")")?;
|
||||||
let bod = Box::new(self.parse_term()?);
|
let bod = Box::new(self.parse_term(fid)?);
|
||||||
Ok(Term::All { nam, inp, bod })
|
let end = *self.index() as u64;
|
||||||
|
let src = new_src(fid, ini, end);
|
||||||
|
Ok(Term::Src { src, val: Box::new(Term::All { nam, inp, bod }) })
|
||||||
}
|
}
|
||||||
Some('λ') => {
|
Some('λ') => {
|
||||||
|
let ini = *self.index() as u64;
|
||||||
self.consume("λ")?;
|
self.consume("λ")?;
|
||||||
let nam = self.parse_name()?;
|
let nam = self.parse_name()?;
|
||||||
let bod = Box::new(self.parse_term()?);
|
let bod = Box::new(self.parse_term(fid)?);
|
||||||
Ok(Term::Lam { nam, bod })
|
let end = *self.index() as u64;
|
||||||
|
let src = new_src(fid, ini, end);
|
||||||
|
Ok(Term::Src { src, val: Box::new(Term::Lam { nam, bod }) })
|
||||||
}
|
}
|
||||||
Some('(') => {
|
Some('(') => {
|
||||||
|
let ini = *self.index() as u64;
|
||||||
self.consume("(")?;
|
self.consume("(")?;
|
||||||
let fun = Box::new(self.parse_term()?);
|
let fun = Box::new(self.parse_term(fid)?);
|
||||||
let mut args = Vec::new();
|
let mut args = Vec::new();
|
||||||
while self.peek_one() != Some(')') {
|
while self.peek_one() != Some(')') {
|
||||||
args.push(Box::new(self.parse_term()?));
|
args.push(Box::new(self.parse_term(fid)?));
|
||||||
|
self.skip_trivia();
|
||||||
}
|
}
|
||||||
self.consume(")")?;
|
self.consume(")")?;
|
||||||
|
let end = *self.index() as u64;
|
||||||
|
let src = new_src(fid, ini, end);
|
||||||
let mut app = fun;
|
let mut app = fun;
|
||||||
for arg in args {
|
for arg in args {
|
||||||
app = Box::new(Term::App { fun: app, arg });
|
app = Box::new(Term::App { fun: app, arg });
|
||||||
}
|
}
|
||||||
Ok(*app)
|
Ok(Term::Src { src, val: app })
|
||||||
}
|
}
|
||||||
Some('{') => {
|
Some('{') => {
|
||||||
|
let ini = *self.index() as u64;
|
||||||
self.consume("{")?;
|
self.consume("{")?;
|
||||||
let val = Box::new(self.parse_term()?);
|
let val = Box::new(self.parse_term(fid)?);
|
||||||
self.consume(":")?;
|
self.consume(":")?;
|
||||||
let typ = Box::new(self.parse_term()?);
|
let typ = Box::new(self.parse_term(fid)?);
|
||||||
self.consume("}")?;
|
self.consume("}")?;
|
||||||
Ok(Term::Ann { val, typ })
|
let end = *self.index() as u64;
|
||||||
|
let src = new_src(fid, ini, end);
|
||||||
|
Ok(Term::Src { src, val: Box::new(Term::Ann { val, typ }) })
|
||||||
}
|
}
|
||||||
Some('$') => {
|
Some('$') => {
|
||||||
|
let ini = *self.index() as u64;
|
||||||
self.consume("$")?;
|
self.consume("$")?;
|
||||||
let nam = self.parse_name()?;
|
let nam = self.parse_name()?;
|
||||||
let bod = Box::new(self.parse_term()?);
|
let bod = Box::new(self.parse_term(fid)?);
|
||||||
Ok(Term::Slf { nam, bod })
|
let end = *self.index() as u64;
|
||||||
|
let src = new_src(fid, ini, end);
|
||||||
|
Ok(Term::Src { src, val: Box::new(Term::Slf { nam, bod }) })
|
||||||
}
|
}
|
||||||
Some('~') => {
|
Some('~') => {
|
||||||
|
let ini = *self.index() as u64;
|
||||||
self.consume("~")?;
|
self.consume("~")?;
|
||||||
let val = Box::new(self.parse_term()?);
|
let val = Box::new(self.parse_term(fid)?);
|
||||||
Ok(Term::Ins { val })
|
let end = *self.index() as u64;
|
||||||
|
let src = new_src(fid, ini, end);
|
||||||
|
Ok(Term::Src { src, val: Box::new(Term::Ins { val }) })
|
||||||
}
|
}
|
||||||
Some('*') => {
|
Some('*') => {
|
||||||
|
let ini = *self.index() as u64;
|
||||||
self.consume("*")?;
|
self.consume("*")?;
|
||||||
Ok(Term::Set)
|
let end = *self.index() as u64;
|
||||||
|
let src = new_src(fid, ini, end);
|
||||||
|
Ok(Term::Src { src, val: Box::new(Term::Set) })
|
||||||
}
|
}
|
||||||
Some('#') => {
|
Some('#') => {
|
||||||
|
let ini = *self.index() as u64;
|
||||||
self.consume("#")?;
|
self.consume("#")?;
|
||||||
match self.peek_one() {
|
match self.peek_one() {
|
||||||
Some('U') => {
|
Some('U') => {
|
||||||
self.consume("U60")?;
|
self.consume("U60")?;
|
||||||
Ok(Term::U60)
|
let end = *self.index() as u64;
|
||||||
|
let src = new_src(fid, ini, end);
|
||||||
|
Ok(Term::Src { src, val: Box::new(Term::U60) })
|
||||||
}
|
}
|
||||||
Some('(') => {
|
Some('(') => {
|
||||||
self.consume("(")?;
|
self.consume("(")?;
|
||||||
let opr = self.parse_oper()?;
|
let opr = self.parse_oper()?;
|
||||||
let fst = Box::new(self.parse_term()?);
|
let fst = Box::new(self.parse_term(fid)?);
|
||||||
let snd = Box::new(self.parse_term()?);
|
let snd = Box::new(self.parse_term(fid)?);
|
||||||
self.consume(")")?;
|
self.consume(")")?;
|
||||||
Ok(Term::Op2 { opr, fst, snd })
|
let end = *self.index() as u64;
|
||||||
|
let src = new_src(fid, ini, end);
|
||||||
|
Ok(Term::Src { src, val: Box::new(Term::Op2 { opr, fst, snd }) })
|
||||||
}
|
}
|
||||||
Some('m') => {
|
Some('m') => {
|
||||||
self.consume("match")?;
|
self.consume("match")?;
|
||||||
let nam = self.parse_name()?;
|
let nam = self.parse_name()?;
|
||||||
self.consume("=")?;
|
self.consume("=")?;
|
||||||
let x = Box::new(self.parse_term()?);
|
let x = Box::new(self.parse_term(fid)?);
|
||||||
self.consume("{")?;
|
self.consume("{")?;
|
||||||
self.consume("#0")?;
|
self.consume("#0")?;
|
||||||
self.consume(":")?;
|
self.consume(":")?;
|
||||||
let z = Box::new(self.parse_term()?);
|
let z = Box::new(self.parse_term(fid)?);
|
||||||
self.consume("#+")?;
|
self.consume("#+")?;
|
||||||
self.consume(":")?;
|
self.consume(":")?;
|
||||||
let s = Box::new(self.parse_term()?);
|
let s = Box::new(self.parse_term(fid)?);
|
||||||
self.consume("}")?;
|
self.consume("}")?;
|
||||||
self.consume(":")?;
|
self.consume(":")?;
|
||||||
let p = Box::new(self.parse_term()?);
|
let p = Box::new(self.parse_term(fid)?);
|
||||||
Ok(Term::Mat { nam, x, z, s, p })
|
let end = *self.index() as u64;
|
||||||
|
let src = new_src(fid, ini, end);
|
||||||
|
Ok(Term::Src { src, val: Box::new(Term::Mat { nam, x, z, s, p }) })
|
||||||
}
|
}
|
||||||
Some(_) => {
|
Some(_) => {
|
||||||
let val = self.parse_u64()?;
|
let val = self.parse_u64()?;
|
||||||
Ok(Term::Num { val })
|
let end = *self.index() as u64;
|
||||||
|
let src = new_src(fid, ini, end);
|
||||||
|
Ok(Term::Src { src, val: Box::new(Term::Num { val }) })
|
||||||
}
|
}
|
||||||
_ => {
|
_ => {
|
||||||
self.expected("numeric-expression")
|
self.expected("numeric-expression")
|
||||||
@ -323,54 +385,69 @@ impl<'i> KindParser<'i> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
Some('?') => {
|
Some('?') => {
|
||||||
|
let ini = *self.index() as u64;
|
||||||
self.consume("?")?;
|
self.consume("?")?;
|
||||||
let nam = self.parse_name()?;
|
let nam = self.parse_name()?;
|
||||||
Ok(Term::Hol { nam })
|
let end = *self.index() as u64;
|
||||||
|
let src = new_src(fid, ini, end);
|
||||||
|
Ok(Term::Src { src, val: Box::new(Term::Hol { nam }) })
|
||||||
}
|
}
|
||||||
Some('\'') => {
|
Some('\'') => {
|
||||||
|
let ini = *self.index() as u64;
|
||||||
let chr = self.parse_quoted_char()?;
|
let chr = self.parse_quoted_char()?;
|
||||||
Ok(Term::Num { val: chr as u64 })
|
let end = *self.index() as u64;
|
||||||
|
let src = new_src(fid, ini, end);
|
||||||
|
Ok(Term::Src { src, val: Box::new(Term::Num { val: chr as u64 }) })
|
||||||
}
|
}
|
||||||
Some('"') => {
|
Some('"') => {
|
||||||
|
let ini = *self.index() as u64;
|
||||||
let txt = self.parse_quoted_string()?;
|
let txt = self.parse_quoted_string()?;
|
||||||
Ok(Term::Txt { txt })
|
let end = *self.index() as u64;
|
||||||
|
let src = new_src(fid, ini, end);
|
||||||
|
Ok(Term::Src { src, val: Box::new(Term::Txt { txt }) })
|
||||||
}
|
}
|
||||||
_ => {
|
_ => {
|
||||||
if self.peek_many(4) == Some("let ") {
|
if self.peek_many(4) == Some("let ") {
|
||||||
|
let ini = *self.index() as u64;
|
||||||
self.advance_many(4);
|
self.advance_many(4);
|
||||||
let nam = self.parse_name()?;
|
let nam = self.parse_name()?;
|
||||||
self.consume("=")?;
|
self.consume("=")?;
|
||||||
let val = Box::new(self.parse_term()?);
|
let val = Box::new(self.parse_term(fid)?);
|
||||||
let bod = Box::new(self.parse_term()?);
|
let bod = Box::new(self.parse_term(fid)?);
|
||||||
Ok(Term::Let { nam, val, bod })
|
let end = *self.index() as u64;
|
||||||
|
let src = new_src(fid, ini, end);
|
||||||
|
Ok(Term::Src { src, val: Box::new(Term::Let { nam, val, bod }) })
|
||||||
} else {
|
} else {
|
||||||
|
let ini = *self.index() as u64;
|
||||||
let nam = self.parse_name()?;
|
let nam = self.parse_name()?;
|
||||||
Ok(Term::Var { nam })
|
let end = *self.index() as u64;
|
||||||
|
let src = new_src(fid, ini, end);
|
||||||
|
Ok(Term::Src { src, val: Box::new(Term::Var { nam }) })
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn parse_def(&mut self) -> Result<(String, Term), String> {
|
fn parse_def(&mut self, fid: u64) -> Result<(String, Term), String> {
|
||||||
let nam = self.parse_name()?;
|
let nam = self.parse_name()?;
|
||||||
self.skip_trivia();
|
self.skip_trivia();
|
||||||
if self.peek_one() == Some(':') {
|
if self.peek_one() == Some(':') {
|
||||||
self.consume(":")?;
|
self.consume(":")?;
|
||||||
let typ = self.parse_term()?;
|
let typ = self.parse_term(fid)?;
|
||||||
self.consume("=")?;
|
self.consume("=")?;
|
||||||
let val = self.parse_term()?;
|
let val = self.parse_term(fid)?;
|
||||||
Ok((nam, Term::Ann { val: Box::new(val), typ: Box::new(typ) }))
|
Ok((nam, Term::Ann { val: Box::new(val), typ: Box::new(typ) }))
|
||||||
} else {
|
} else {
|
||||||
self.consume("=")?;
|
self.consume("=")?;
|
||||||
let val = self.parse_term()?;
|
let val = self.parse_term(fid)?;
|
||||||
Ok((nam, val))
|
Ok((nam, val))
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn parse_book(&mut self) -> Result<Book, String> {
|
fn parse_book(&mut self, fid: u64) -> Result<Book, String> {
|
||||||
let mut book = Book::new();
|
let mut book = Book::new();
|
||||||
while *self.index() < self.input().len() {
|
while *self.index() < self.input().len() {
|
||||||
let (name, term) = self.parse_def()?;
|
let (name, term) = self.parse_def(fid)?;
|
||||||
book.defs.insert(name, term);
|
book.defs.insert(name, term);
|
||||||
self.skip_trivia();
|
self.skip_trivia();
|
||||||
}
|
}
|
||||||
@ -383,6 +460,7 @@ impl Book {
|
|||||||
fn new() -> Self {
|
fn new() -> Self {
|
||||||
Book {
|
Book {
|
||||||
defs: HashMap::new(),
|
defs: HashMap::new(),
|
||||||
|
fids: HashMap::new(),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -404,48 +482,165 @@ impl Book {
|
|||||||
book_str
|
book_str
|
||||||
}
|
}
|
||||||
|
|
||||||
fn load_file(filename: &str) -> Result<Self, String> {
|
|
||||||
std::fs::read_to_string(filename)
|
|
||||||
.map_err(|_| format!("Could not read file: {}", filename))
|
|
||||||
.and_then(|contents| KindParser::new(&contents).parse_book())
|
|
||||||
}
|
|
||||||
|
|
||||||
fn load(name: &str) -> Result<Self, String> {
|
fn load(name: &str) -> Result<Self, String> {
|
||||||
fn load_term(name: &str, book: &mut Book) -> Result<(), String> {
|
fn load_go(name: &str, book: &mut Book) -> Result<(), String> {
|
||||||
|
//println!("... {}", name);
|
||||||
if !book.defs.contains_key(name) {
|
if !book.defs.contains_key(name) {
|
||||||
let file = format!("./book/{}.kind2", name);
|
let file = format!("./{}.kind2", name);
|
||||||
let text = std::fs::read_to_string(&file).map_err(|_| format!("Could not read file: {}", file))?;
|
let text = std::fs::read_to_string(&file).map_err(|_| format!("Could not read file: {}", file))?;
|
||||||
let defs = KindParser::new(&text).parse_book()?;
|
let fid = book.get_file_id(&file);
|
||||||
|
//println!("... parsing: {}", name);
|
||||||
|
let defs = KindParser::new(&text).parse_book(fid)?;
|
||||||
|
//println!("... parsed: {}", name);
|
||||||
for (def_name, def_term) in &defs.defs {
|
for (def_name, def_term) in &defs.defs {
|
||||||
book.defs.insert(def_name.clone(), def_term.clone());
|
book.defs.insert(def_name.clone(), def_term.clone());
|
||||||
}
|
}
|
||||||
|
//println!("laoding deps for: {}", name);
|
||||||
for (_, def_term) in defs.defs.into_iter() {
|
for (_, def_term) in defs.defs.into_iter() {
|
||||||
let mut dependencies = HashSet::new();
|
let mut dependencies = HashSet::new();
|
||||||
def_term.get_free_vars(im::Vector::new(), &mut dependencies);
|
def_term.get_free_vars(im::Vector::new(), &mut dependencies);
|
||||||
|
//println!("{} deps: {:?}", name, dependencies);
|
||||||
for ref_name in dependencies {
|
for ref_name in dependencies {
|
||||||
load_term(&ref_name, book)?;
|
load_go(&ref_name, book)?;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
return Ok(());
|
return Ok(());
|
||||||
}
|
}
|
||||||
let mut book = Book::new();
|
let mut book = Book::new();
|
||||||
load_term(name, &mut book)?;
|
load_go(name, &mut book)?;
|
||||||
|
load_go("String", &mut book)?;
|
||||||
|
//println!("DONE!");
|
||||||
Ok(book)
|
Ok(book)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
fn get_file_id(&mut self, name: &str) -> u64 {
|
||||||
|
if let Some(id) = self.fids.get(name) {
|
||||||
|
*id
|
||||||
|
} else {
|
||||||
|
let id = self.fids.len() as u64 + 1;
|
||||||
|
self.fids.insert(name.to_string(), id);
|
||||||
|
id
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
// FIXME: asymptotics
|
||||||
|
fn get_file_name(&self, id: u64) -> Option<String> {
|
||||||
|
for (name, &fid) in &self.fids {
|
||||||
|
if fid == id {
|
||||||
|
return Some(name.clone());
|
||||||
|
}
|
||||||
|
}
|
||||||
|
None
|
||||||
|
}
|
||||||
|
|
||||||
|
fn inject_sources(&self, input: &str) -> Result<String, String> {
|
||||||
|
let mut result = input.to_string();
|
||||||
|
let ini_sym = "##LOC{";
|
||||||
|
let end_sym = "}LOC##";
|
||||||
|
while let (Some(ini), Some(end)) = (result.find(ini_sym), result.find(end_sym)) {
|
||||||
|
let got = &result[ini + ini_sym.len()..end];
|
||||||
|
let loc = got.parse::<u64>().map_err(|_| "Failed to parse location")?;
|
||||||
|
let fid = src_fid(loc);
|
||||||
|
let ini = src_ini(loc) as usize;
|
||||||
|
let end = src_end(loc) as usize;
|
||||||
|
if loc == 0 {
|
||||||
|
result = result.replace(&format!("{}{}{}", ini_sym, got, end_sym), "");
|
||||||
|
} else if let Some(file_name) = self.get_file_name(fid) {
|
||||||
|
let source_file = std::fs::read_to_string(&file_name).map_err(|_| "Failed to read source file")?;
|
||||||
|
let context_str = highlight_error(ini, end, &source_file);
|
||||||
|
let context_str = format!("\x1b[4m{}\x1b[0m\n{}", file_name, context_str);
|
||||||
|
result = result.replace(&format!("{}{}{}", ini_sym, got, end_sym), &context_str);
|
||||||
|
} else {
|
||||||
|
return Err("File ID not found".to_string());
|
||||||
|
}
|
||||||
|
}
|
||||||
|
Ok(result)
|
||||||
|
}
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
fn run() -> Result<(), String> {
|
//fn run() -> Result<(), String> {
|
||||||
let book = Book::load("Bool")?;
|
//let book = Book::load("Nat")?;
|
||||||
//let book = KindParser::new("f : * = ∀(a: *) λf λx (ID (f (f a b c)))").parse_book()?;
|
//println!("{}", book.show());
|
||||||
println!("{}", book.show());
|
//println!("{}", book.to_hvm1());
|
||||||
println!("{}", book.to_hvm1());
|
//return Ok(());
|
||||||
return Ok(());
|
//}
|
||||||
|
|
||||||
|
//fn main() {
|
||||||
|
//if let Err(e) = run() {
|
||||||
|
//eprintln!("{}", e);
|
||||||
|
//}
|
||||||
|
//}
|
||||||
|
|
||||||
|
|
||||||
|
fn generate_check_hvm1(book: &Book, command: &str, arg: &str) -> String {
|
||||||
|
// Gets used def names, sorted alphabetically.
|
||||||
|
let mut used_defs: Vec<_> = book.defs.keys().collect();
|
||||||
|
used_defs.sort();
|
||||||
|
let used_defs = used_defs.iter().map(|name| format!("(Pair \"{}\" Book.{})", name, name)).collect::<Vec<_>>().join(" ");
|
||||||
|
// Generates '.check.hvm1' contents.
|
||||||
|
let kind2_hvm1 = include_str!("./kind2.hvm1");
|
||||||
|
let book_hvm1 = book.to_hvm1();
|
||||||
|
let main_hvm1 = match command {
|
||||||
|
"check" => format!("Main = (Checker.many [{}])\n", used_defs),
|
||||||
|
"run" => format!("Main = (Normalizer Book.{})\n", arg),
|
||||||
|
_ => panic!("invalid command"),
|
||||||
|
};
|
||||||
|
let hvm1_code = format!("{}\n{}\n{}", kind2_hvm1, book_hvm1, main_hvm1);
|
||||||
|
return hvm1_code;
|
||||||
}
|
}
|
||||||
|
|
||||||
fn main() {
|
fn main() {
|
||||||
if let Err(e) = run() {
|
let args: Vec<String> = env::args().collect();
|
||||||
eprintln!("{}", e);
|
|
||||||
|
if args.len() < 3 {
|
||||||
|
show_help();
|
||||||
|
}
|
||||||
|
|
||||||
|
let cmd = &args[1];
|
||||||
|
let arg = &args[2];
|
||||||
|
|
||||||
|
//println!("loading");
|
||||||
|
match cmd.as_str() {
|
||||||
|
"check" | "run" => {
|
||||||
|
match Book::load(arg) {
|
||||||
|
Ok(book) => {
|
||||||
|
//println!("loaded!");
|
||||||
|
let check_hvm1 = generate_check_hvm1(&book, cmd, arg);
|
||||||
|
|
||||||
|
// Saves it to a file.
|
||||||
|
let mut file = File::create(".check.hvm1").expect("Failed to create '.check.hvm1'.");
|
||||||
|
file.write_all(check_hvm1.as_bytes()).expect("Failed to write '.check.hvm1'.");
|
||||||
|
|
||||||
|
let output = Command::new("hvm1").arg("run").arg("-t").arg("1").arg("-c").arg("-f").arg(".check.hvm1").arg("(Main)").output().expect("Failed to execute command");
|
||||||
|
//let stdout : Result<String,String> = Ok(format!("{}", String::from_utf8_lossy(&output.stdout)));
|
||||||
|
let stdout = book.inject_sources(&format!("{}", String::from_utf8_lossy(&output.stdout)));
|
||||||
|
let stderr = String::from_utf8_lossy(&output.stderr);
|
||||||
|
|
||||||
|
match stdout {
|
||||||
|
//Ok(output) => println!("{}", output.replace("(ERRORS_FOUND)","")),
|
||||||
|
Ok(output) => println!("{}", output),
|
||||||
|
Err(error) => eprintln!("{}", error),
|
||||||
|
}
|
||||||
|
|
||||||
|
if !output.stderr.is_empty() {
|
||||||
|
eprintln!("{}", stderr);
|
||||||
|
}
|
||||||
|
},
|
||||||
|
Err(e) => {
|
||||||
|
eprintln!("{}", e);
|
||||||
|
std::process::exit(1);
|
||||||
|
},
|
||||||
|
}
|
||||||
|
},
|
||||||
|
_ => {
|
||||||
|
show_help();
|
||||||
|
},
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
fn show_help() {
|
||||||
|
eprintln!("Usage: kind2 [check|run] <name>");
|
||||||
|
std::process::exit(1);
|
||||||
|
}
|
||||||
|
Loading…
Reference in New Issue
Block a user