mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-09-11 08:45:32 +03:00
Show highlighted error line
This commit is contained in:
Victor Maia
parent
2817094f4e
commit
50fab9e81f
1
Cargo.lock
generated
1
Cargo.lock
generated
@ -143,6 +143,7 @@ name = "kind2"
|
||||
version = "0.1.0"
|
||||
dependencies = [
|
||||
"clap",
|
||||
"highlight_error",
|
||||
"hvm",
|
||||
]
|
||||
|
||||
|
||||
@ -7,4 +7,5 @@ edition = "2021"
|
||||
|
||||
[dependencies]
|
||||
hvm = "0.1.44"
|
||||
highlight_error = "0.1.1"
|
||||
clap = { version = "3.1.8", features = ["derive"] }
|
||||
|
||||
@ -51,7 +51,9 @@ Equal.apply t u a b f (Refl v k) = (Refl v (f k))
|
||||
Equal.rewrite (t: Type) (a: t) (b: t) (e: (Equal t a b)) (p: t -> Type) (x: (p a)) : (p b)
|
||||
Equal.rewrite t a b (Refl u k) p x = {x :: (p k)}
|
||||
|
||||
Main : Nat {
|
||||
let f = {(@x @y y) :: Nat -> Nat -> Nat}
|
||||
(f Zero (Nat.double (Succ (Succ (Succ Zero)))))
|
||||
}
|
||||
Foo (f: Bool -> Bool) (x: Bool) : Nat
|
||||
Foo f x = x
|
||||
|
||||
//Main : Nat {
|
||||
//(Succ True)
|
||||
//}
|
||||
|
||||
394
src/checker.hvm
394
src/checker.hvm
@ -16,9 +16,9 @@ Main = API.check_all
|
||||
// Name.length Name : U60
|
||||
(Name.length name) = (String.length (Show.name name))
|
||||
|
||||
// Bool.if -(r: Type) Bool r r : r
|
||||
(Bool.if False then else) = else
|
||||
(Bool.if True then else) = then
|
||||
// If -(r: Type) Bool r r : r
|
||||
(If False then else) = else
|
||||
(If True then else) = then
|
||||
|
||||
// Bool.and Bool Bool : Bool
|
||||
(Bool.and True b) = b
|
||||
@ -61,11 +61,15 @@ Main = API.check_all
|
||||
(String.length (String.cons x xs)) = (+ 1 (String.length xs))
|
||||
|
||||
// String.pad_right (str: String) (chr: U60) (len: U60) : String
|
||||
|
||||
(String.pad_right str chr 0) = String.nil
|
||||
(String.pad_right (String.cons x xs) chr len) = (String.cons x (String.pad_right xs chr (- len 1)))
|
||||
(String.pad_right String.nil chr len) = (String.cons chr (String.pad_right String.nil chr (- len 1)))
|
||||
|
||||
// String.equal (a: String) (b: String) : Bool
|
||||
//(String.equal (String.cons a as) (String.cons b bs)) = (If (U60.equal a b) (String.equal as bs) False)
|
||||
//(String.equal String.nil String.nil) = True
|
||||
//(String.equal as bs) = False
|
||||
|
||||
// Text (List String) : String
|
||||
(Text Nil) = String.nil
|
||||
(Text (Cons x xs)) = (String.concat x (Text xs))
|
||||
@ -116,7 +120,7 @@ Line = (String.cons 10 String.nil)
|
||||
|
||||
// type Result (a : Type) {
|
||||
// (Checked (ctx: Context) (dep: U60) (rhs: Bool) (ret: a))
|
||||
// (Errored Error)
|
||||
// (Errored (ctx: Context) Error)
|
||||
// }
|
||||
|
||||
// type Checker (a : Type) = (context: (List Term)) (depth: U60) (rhs: Bool) (Result a)
|
||||
@ -126,13 +130,13 @@ Line = (String.cons 10 String.nil)
|
||||
|
||||
// Checker.bind.result -(a: Type) -(b: Type) (Result a) : (a -> Checker b) (Result b)
|
||||
(Checker.bind.result (Checked ctx dep rhs val)) = λnext (next val ctx dep rhs)
|
||||
(Checker.bind.result (Errored err)) = λnext (Errored err)
|
||||
(Checker.bind.result (Errored ctx err)) = λnext (Errored ctx err)
|
||||
|
||||
// Checker.done -(a: Type) (x: a) : (Checker a)
|
||||
(Checker.done val) = λctx λdep λrhs (Checked ctx dep rhs val)
|
||||
|
||||
// Checker.fail -(a: Type) (err: (List Term) -> U60 -> Error) : (Checker a)
|
||||
(Checker.fail err) = λctx λdep λrhs (Errored (err ctx dep))
|
||||
(Checker.fail err) = λctx λdep λrhs (Errored ctx err)
|
||||
|
||||
// Checker.get_context -(a: Type) : (Checker Context)
|
||||
(Checker.get_context) = λctx λdep λrhs
|
||||
@ -177,68 +181,125 @@ Line = (String.cons 10 String.nil)
|
||||
// ----------
|
||||
|
||||
// Term.if_all -(r: Type) Term (Term -> (Term -> Term) -> r) r : r
|
||||
(Term.if_all (All name type body) then else) = (then type body)
|
||||
(Term.if_all other then else) = else
|
||||
(Term.if_all (All orig name type body) then else) = (then type body)
|
||||
(Term.if_all other then else) = else
|
||||
|
||||
// Term.orig
|
||||
(Term.get_origin (Typ orig)) = orig
|
||||
(Term.get_origin (Var orig name index)) = orig
|
||||
(Term.get_origin (All orig name type body)) = orig
|
||||
(Term.get_origin (Lam orig name body)) = orig
|
||||
(Term.get_origin (App orig func argm)) = orig
|
||||
(Term.get_origin (Let orig name expr body)) = orig
|
||||
(Term.get_origin (Ann orig expr type)) = orig
|
||||
(Term.get_origin (Ct0 name orig)) = orig
|
||||
(Term.get_origin (Ct1 name orig a)) = orig
|
||||
(Term.get_origin (Ct2 name orig a b)) = orig
|
||||
(Term.get_origin (Ct3 name orig a b c)) = orig
|
||||
(Term.get_origin (Ct4 name orig a b c d)) = orig
|
||||
(Term.get_origin (Ct5 name orig a b c d e)) = orig
|
||||
(Term.get_origin (Ct6 name orig a b c d e f)) = orig
|
||||
(Term.get_origin (Ct7 name orig a b c d e f g)) = orig
|
||||
(Term.get_origin (Ct8 name orig a b c d e f g h)) = orig
|
||||
(Term.get_origin (Fn0 name orig)) = orig
|
||||
(Term.get_origin (Fn1 name orig a)) = orig
|
||||
(Term.get_origin (Fn2 name orig a b)) = orig
|
||||
(Term.get_origin (Fn3 name orig a b c)) = orig
|
||||
(Term.get_origin (Fn4 name orig a b c d)) = orig
|
||||
(Term.get_origin (Fn5 name orig a b c d e)) = orig
|
||||
(Term.get_origin (Fn6 name orig a b c d e f)) = orig
|
||||
(Term.get_origin (Fn7 name orig a b c d e f g)) = orig
|
||||
(Term.get_origin (Fn8 name orig a b c d e f g h)) = orig
|
||||
|
||||
// Term.set_origin
|
||||
(Term.set_origin new_orig (Typ orig)) = (Typ new_orig)
|
||||
(Term.set_origin new_orig (Var orig name index)) = (Var new_orig name index)
|
||||
(Term.set_origin new_orig (All orig name type body)) = (All new_orig name type body)
|
||||
(Term.set_origin new_orig (Lam orig name body)) = (Lam new_orig name body)
|
||||
(Term.set_origin new_orig (App orig func argm)) = (App new_orig func argm)
|
||||
(Term.set_origin new_orig (Let orig name expr body)) = (Let new_orig name expr body)
|
||||
(Term.set_origin new_orig (Ann orig expr type)) = (Ann new_orig expr type)
|
||||
(Term.set_origin new_orig (Ct0 name orig)) = (Ct0 name new_orig)
|
||||
(Term.set_origin new_orig (Ct1 name orig a)) = (Ct1 name new_orig a)
|
||||
(Term.set_origin new_orig (Ct2 name orig a b)) = (Ct2 name new_orig a b)
|
||||
(Term.set_origin new_orig (Ct3 name orig a b c)) = (Ct3 name new_orig a b c)
|
||||
(Term.set_origin new_orig (Ct4 name orig a b c d)) = (Ct4 name new_orig a b c d)
|
||||
(Term.set_origin new_orig (Ct5 name orig a b c d e)) = (Ct5 name new_orig a b c d e)
|
||||
(Term.set_origin new_orig (Ct6 name orig a b c d e f)) = (Ct6 name new_orig a b c d e f)
|
||||
(Term.set_origin new_orig (Ct7 name orig a b c d e f g)) = (Ct7 name new_orig a b c d e f g)
|
||||
(Term.set_origin new_orig (Ct8 name orig a b c d e f g h)) = (Ct8 name new_orig a b c d e f g h)
|
||||
(Term.set_origin new_orig (Fn0 name orig)) = (Fn0 name new_orig)
|
||||
(Term.set_origin new_orig (Fn1 name orig a)) = (Fn1 name new_orig a)
|
||||
(Term.set_origin new_orig (Fn2 name orig a b)) = (Fn2 name new_orig a b)
|
||||
(Term.set_origin new_orig (Fn3 name orig a b c)) = (Fn3 name new_orig a b c)
|
||||
(Term.set_origin new_orig (Fn4 name orig a b c d)) = (Fn4 name new_orig a b c d)
|
||||
(Term.set_origin new_orig (Fn5 name orig a b c d e)) = (Fn5 name new_orig a b c d e)
|
||||
(Term.set_origin new_orig (Fn6 name orig a b c d e f)) = (Fn6 name new_orig a b c d e f)
|
||||
(Term.set_origin new_orig (Fn7 name orig a b c d e f g)) = (Fn7 name new_orig a b c d e f g)
|
||||
(Term.set_origin new_orig (Fn8 name orig a b c d e f g h)) = (Fn8 name new_orig a b c d e f g h)
|
||||
|
||||
// SO = Term.set_origin
|
||||
(SO new_orig term) = (Term.set_origin new_orig term)
|
||||
|
||||
// Equal Term Term : (Checker Bool)
|
||||
// --------------------------------
|
||||
|
||||
// Typ equality
|
||||
(Equal Typ Typ) =
|
||||
(Equal (Typ orig) (Typ orig)) =
|
||||
(Checker.done True)
|
||||
|
||||
// All equality
|
||||
(Equal (All a.name a.type a.body) (All b.name b.type b.body)) =
|
||||
(Equal (All a.orig a.name a.type a.body) (All b.orig b.name b.type b.body)) =
|
||||
ask dep = (Checker.bind Checker.get_depth)
|
||||
ask type = (Checker.bind (Equal a.type b.type))
|
||||
ask body = (Checker.bind (Checker.extended (Equal (a.body (Var a.name dep)) (b.body (Var b.name dep))) Null Null Null))
|
||||
ask body = (Checker.bind (Checker.extended (Equal (a.body (Var a.orig a.name dep)) (b.body (Var b.orig b.name dep))) Null Null Null))
|
||||
(Checker.done (Bool.and type body))
|
||||
|
||||
// Lam equality
|
||||
(Equal (Lam a.name a.body) (Lam b.name b.body)) =
|
||||
(Equal (Lam a.orig a.name a.body) (Lam b.orig b.name b.body)) =
|
||||
ask dep = (Checker.bind Checker.get_depth)
|
||||
ask body = (Checker.bind (Checker.extended (Equal (a.body (Var a.name dep)) (b.body (Var b.name dep))) Null Null Null))
|
||||
ask body = (Checker.bind (Checker.extended (Equal (a.body (Var a.orig a.name dep)) (b.body (Var b.orig b.name dep))) Null Null Null))
|
||||
body
|
||||
|
||||
// App equality
|
||||
(Equal (App a.func a.argm) (App b.func b.argm)) =
|
||||
(Equal (App a.orig a.func a.argm) (App b.orig b.func b.argm)) =
|
||||
ask func = (Checker.bind (Equal a.func b.func))
|
||||
ask argm = (Checker.bind (Equal a.argm b.argm))
|
||||
(Checker.done (Bool.and func argm))
|
||||
|
||||
// Let equality
|
||||
(Equal (Let a.name a.expr a.body) (Let b.name b.expr b.body)) =
|
||||
(Equal (Let a.orig a.name a.expr a.body) (Let b.orig b.name b.expr b.body)) =
|
||||
ask dep = (Checker.bind Checker.get_depth)
|
||||
ask expr = (Checker.bind (Equal a.expr b.expr))
|
||||
ask body = (Checker.bind (Checker.extended (Equal (a.body (Var a.name dep)) (b.body (Var b.name dep))) Null Null Null))
|
||||
ask body = (Checker.bind (Checker.extended (Equal (a.body (Var a.orig a.name dep)) (b.body (Var b.orig b.name dep))) Null Null Null))
|
||||
(Checker.done (Bool.and expr body))
|
||||
|
||||
// Ann equality
|
||||
(Equal (Ann a.expr a.type) (Ann b.expr b.type)) =
|
||||
(Equal (Ann a.orig a.expr a.type) (Ann b.orig b.expr b.type)) =
|
||||
ask expr = (Checker.bind (Equal a.expr b.expr))
|
||||
ask type = (Checker.bind (Equal a.type b.type))
|
||||
(Checker.done (Bool.and expr type))
|
||||
|
||||
// Ct0 equality
|
||||
(Equal (Ct0 a.ctid) (Ct0 b.ctid)) =
|
||||
(Equal (Ct0 a.ctid a.orig) (Ct0 b.ctid b.orig)) =
|
||||
let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid))
|
||||
(Checker.done ctid)
|
||||
|
||||
// Ct1 equality
|
||||
(Equal (Ct1 a.ctid a.x0) (Ct1 b.ctid b.x0)) =
|
||||
(Equal (Ct1 a.ctid a.orig a.x0) (Ct1 b.ctid b.orig b.x0)) =
|
||||
let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid))
|
||||
ask x0 = (Checker.bind (Equal a.x0 b.x0))
|
||||
(Checker.done (Bool.and ctid x0))
|
||||
|
||||
// Ct2 equality
|
||||
(Equal (Ct2 a.ctid a.x0 a.x1) (Ct2 b.ctid b.x0 b.x1)) =
|
||||
(Equal (Ct2 a.ctid a.orig a.x0 a.x1) (Ct2 b.ctid b.orig b.x0 b.x1)) =
|
||||
let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid))
|
||||
ask x0 = (Checker.bind (Equal a.x0 b.x0))
|
||||
ask x1 = (Checker.bind (Equal a.x1 b.x1))
|
||||
(Checker.done (Bool.and ctid (Bool.and x0 x1)))
|
||||
|
||||
// Ct3 equality
|
||||
(Equal (Ct3 a.ctid a.x0 a.x1 a.x2) (Ct3 b.ctid b.x0 b.x1 b.x2)) =
|
||||
(Equal (Ct3 a.ctid a.orig a.x0 a.x1 a.x2) (Ct3 b.ctid b.orig b.x0 b.x1 b.x2)) =
|
||||
let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid))
|
||||
ask x0 = (Checker.bind (Equal a.x0 b.x0))
|
||||
ask x1 = (Checker.bind (Equal a.x1 b.x1))
|
||||
@ -246,7 +307,7 @@ Line = (String.cons 10 String.nil)
|
||||
(Checker.done (Bool.and ctid (Bool.and x0 (Bool.and x1 x2))))
|
||||
|
||||
// Ct4 equality
|
||||
(Equal (Ct4 a.ctid a.x0 a.x1 a.x2 a.x3) (Ct4 b.ctid b.x0 b.x1 b.x2 b.x3)) =
|
||||
(Equal (Ct4 a.ctid a.orig a.x0 a.x1 a.x2 a.x3) (Ct4 b.ctid b.orig b.x0 b.x1 b.x2 b.x3)) =
|
||||
let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid))
|
||||
ask x0 = (Checker.bind (Equal a.x0 b.x0))
|
||||
ask x1 = (Checker.bind (Equal a.x1 b.x1))
|
||||
@ -255,7 +316,7 @@ Line = (String.cons 10 String.nil)
|
||||
(Checker.done (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 x3)))))
|
||||
|
||||
// Ct5 equality
|
||||
(Equal (Ct5 a.ctid a.x0 a.x1 a.x2 a.x3 a.x4) (Ct5 b.ctid b.x0 b.x1 b.x2 b.x3 b.x4)) =
|
||||
(Equal (Ct5 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4) (Ct5 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4)) =
|
||||
let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid))
|
||||
ask x0 = (Checker.bind (Equal a.x0 b.x0))
|
||||
ask x1 = (Checker.bind (Equal a.x1 b.x1))
|
||||
@ -265,7 +326,7 @@ Line = (String.cons 10 String.nil)
|
||||
(Checker.done (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 x4))))))
|
||||
|
||||
// Ct6 equality
|
||||
(Equal (Ct6 a.ctid a.x0 a.x1 a.x2 a.x3 a.x4 a.x5) (Ct6 b.ctid b.x0 b.x1 b.x2 b.x3 b.x4 b.x5)) =
|
||||
(Equal (Ct6 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5) (Ct6 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5)) =
|
||||
let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid))
|
||||
ask x0 = (Checker.bind (Equal a.x0 b.x0))
|
||||
ask x1 = (Checker.bind (Equal a.x1 b.x1))
|
||||
@ -276,7 +337,7 @@ Line = (String.cons 10 String.nil)
|
||||
(Checker.done (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 x5)))))))
|
||||
|
||||
// Ct7 equality
|
||||
(Equal (Ct7 a.ctid a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6) (Ct7 b.ctid b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6)) =
|
||||
(Equal (Ct7 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6) (Ct7 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6)) =
|
||||
let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid))
|
||||
ask x0 = (Checker.bind (Equal a.x0 b.x0))
|
||||
ask x1 = (Checker.bind (Equal a.x1 b.x1))
|
||||
@ -288,7 +349,7 @@ Line = (String.cons 10 String.nil)
|
||||
(Checker.done (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 x6))))))))
|
||||
|
||||
// Ct8 equality
|
||||
(Equal (Ct8 a.ctid a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7) (Ct8 b.ctid b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7)) =
|
||||
(Equal (Ct8 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7) (Ct8 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7)) =
|
||||
let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid))
|
||||
ask x0 = (Checker.bind (Equal a.x0 b.x0))
|
||||
ask x1 = (Checker.bind (Equal a.x1 b.x1))
|
||||
@ -301,14 +362,14 @@ Line = (String.cons 10 String.nil)
|
||||
(Checker.done (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 x7)))))))))
|
||||
|
||||
// Var equality #0
|
||||
(Equal (Var a.name a.index) b) =
|
||||
(Equal (Var a.orig a.name a.index) b) =
|
||||
ask rhs = (Checker.bind (Checker.get_right_hand_side))
|
||||
(Equal.var rhs a.name a.index b)
|
||||
(Equal.var rhs a.orig a.name a.index b)
|
||||
|
||||
// Var equality #1
|
||||
(Equal a (Var b.name b.index)) =
|
||||
(Equal a (Var b.orig b.name b.index)) =
|
||||
ask rhs = (Checker.bind (Checker.get_right_hand_side))
|
||||
(Equal.var rhs b.name b.index a)
|
||||
(Equal.var rhs b.orig b.name b.index a)
|
||||
|
||||
// Not equal
|
||||
(Equal a b) =
|
||||
@ -322,58 +383,57 @@ Line = (String.cons 10 String.nil)
|
||||
// If on RHS, check if a and b are equal
|
||||
|
||||
// Var-Var checker
|
||||
(Equal.var False a.name a.index b) =
|
||||
(Equal.var False a.orig a.name a.index b) =
|
||||
ask (Checker.bind (Checker.add_value a.index b))
|
||||
(Checker.done True)
|
||||
(Equal.var True a.name a.index (Var b.name b.index)) =
|
||||
(Bool.if (U60.equal a.index b.index)
|
||||
(Equal.var True a.orig a.name a.index (Var b.orig b.name b.index)) =
|
||||
(If (U60.equal a.index b.index)
|
||||
(Checker.done True)
|
||||
ask a.val = (Checker.bind (Checker.find a.index [] λnλtλv(v)))
|
||||
ask b.val = (Checker.bind (Checker.find b.index [] λnλtλv(v)))
|
||||
ask a.chk = (Checker.bind (Equal.var.try_values a.index a.val (Var b.name b.index)))
|
||||
ask b.chk = (Checker.bind (Equal.var.try_values b.index b.val (Var a.name a.index)))
|
||||
ask a.chk = (Checker.bind (Equal.var.try_values a.val (Var b.orig b.name b.index)))
|
||||
ask b.chk = (Checker.bind (Equal.var.try_values b.val (Var a.orig a.name a.index)))
|
||||
(Checker.done (Bool.or a.chk b.chk)))
|
||||
(Equal.var True a.name a.index b) =
|
||||
(Equal.var True a.orig a.name a.index b) =
|
||||
ask a.val = (Checker.bind (Checker.find a.index [] λnλtλv(v)))
|
||||
(Equal.var.try_values a.index a.val b)
|
||||
(Equal.var.try_values a.val b)
|
||||
|
||||
// Checks if any of a set of reductions is equal
|
||||
(Equal.var.try_values i (Cons a as) b) =
|
||||
(Equal.var.try_values (Cons a as) b) =
|
||||
ask head = (Checker.bind (Equal a b))
|
||||
(Bool.if head
|
||||
(If head
|
||||
(Checker.done True)
|
||||
(Equal.var.try_values i as b))
|
||||
(Equal.var.try_values i Nil b) =
|
||||
(Equal.var.try_values as b))
|
||||
(Equal.var.try_values Nil b) =
|
||||
(Checker.done False)
|
||||
|
||||
// Infer Term : (Checker Term)
|
||||
// ---------------------------
|
||||
|
||||
// Infers Var
|
||||
(Infer (Var name index)) =
|
||||
(Infer (Var orig name index)) =
|
||||
ask got_type = (Checker.bind (Checker.find index None λnλtλv(Some t)))
|
||||
(Maybe.case got_type
|
||||
(Checker.fail λctx λdep (UnboundVariable ctx dep))
|
||||
(Checker.fail (UnboundVariable (Var orig name index)))
|
||||
λvar_type (Checker.done var_type))
|
||||
|
||||
// Infers Typ
|
||||
(Infer Typ) =
|
||||
(Checker.done Typ)
|
||||
(Infer (Typ orig)) =
|
||||
(Checker.done (Typ orig))
|
||||
|
||||
// Infers All
|
||||
(Infer (All name type body)) =
|
||||
(Infer (All orig name type body)) =
|
||||
ask dep = (Checker.bind Checker.get_depth)
|
||||
ask type_chk = (Checker.bind (Check type Typ))
|
||||
ask body_chk = (Checker.bind (Checker.extended (Check (body (Var name dep)) Typ) name type []))
|
||||
(Checker.done Typ)
|
||||
ask type_chk = (Checker.bind (Check type (Typ orig)))
|
||||
ask body_chk = (Checker.bind (Checker.extended (Check (body (Var orig name dep)) (Typ orig)) name type []))
|
||||
(Checker.done (Typ orig))
|
||||
|
||||
// Infers Lam
|
||||
(Infer (Lam name body)) =
|
||||
(Checker.fail λctx λdep
|
||||
(CantInferLambda ctx dep))
|
||||
(Infer (Lam orig name body)) =
|
||||
(Checker.fail (CantInferLambda (Lam orig name body)))
|
||||
|
||||
// Infers App
|
||||
(Infer (App func argm)) =
|
||||
(Infer (App orig func argm)) =
|
||||
ask func_typ = (Checker.bind (Infer func))
|
||||
(Term.if_all func_typ
|
||||
// then
|
||||
@ -381,114 +441,113 @@ Line = (String.cons 10 String.nil)
|
||||
ask argm_ok = (Checker.bind (Check argm func_typ_type))
|
||||
(Checker.done (func_typ_body argm))
|
||||
// else
|
||||
(Checker.fail λctx λdep
|
||||
(NonFunctionApplication ctx dep)))
|
||||
(Checker.fail (InvalidCall (App orig func argm))))
|
||||
|
||||
// Infers Let
|
||||
(Infer (Let name expr body)) =
|
||||
(Infer (Let orig name expr body)) =
|
||||
ask dep = (Checker.bind Checker.get_depth)
|
||||
ask expr_typ = (Checker.bind (Infer expr))
|
||||
ask body_typ = (Checker.bind (Checker.extended (Infer (body (Var name dep))) name expr_typ []))
|
||||
ask body_typ = (Checker.bind (Checker.extended (Infer (body (Var orig name dep))) name expr_typ []))
|
||||
(Checker.done body_typ)
|
||||
|
||||
// Infers Ann
|
||||
(Infer (Ann expr type)) =
|
||||
(Infer (Ann orig expr type)) =
|
||||
ask expr_chk = (Checker.bind (Check expr type))
|
||||
(Checker.done type)
|
||||
|
||||
// Infers Ct0
|
||||
(Infer (Ct0 ctid)) =
|
||||
(Infer (Ct0 ctid orig)) =
|
||||
(Checker.done (TypeOf ctid))
|
||||
|
||||
// Infers Ct1
|
||||
(Infer (Ct1 ctid x0)) =
|
||||
(Infer (App (Ct0 ctid) x0))
|
||||
(Infer (Ct1 ctid orig x0)) =
|
||||
(Infer (App orig (Ct0 ctid orig) x0))
|
||||
|
||||
// Infers Ct2
|
||||
(Infer (Ct2 ctid x0 x1)) =
|
||||
(Infer (App (App (Ct0 ctid) x0) x1))
|
||||
(Infer (Ct2 ctid orig x0 x1)) =
|
||||
(Infer (App orig (App orig (Ct0 ctid orig) x0) x1))
|
||||
|
||||
// Infers Ct3
|
||||
(Infer (Ct3 ctid x0 x1 x2)) =
|
||||
(Infer (App (App (App (Ct0 ctid) x0) x1) x2))
|
||||
(Infer (Ct3 ctid orig x0 x1 x2)) =
|
||||
(Infer (App orig (App orig (App orig (Ct0 ctid orig) x0) x1) x2))
|
||||
|
||||
// Infers Ct4
|
||||
(Infer (Ct4 ctid x0 x1 x2 x3)) =
|
||||
(Infer (App (App (App (App (Ct0 ctid) x0) x1) x2) x3))
|
||||
(Infer (Ct4 ctid orig x0 x1 x2 x3)) =
|
||||
(Infer (App orig (App orig (App orig (App orig (Ct0 ctid orig) x0) x1) x2) x3))
|
||||
|
||||
// Infers Ct5
|
||||
(Infer (Ct5 ctid x0 x1 x2 x3 x4)) =
|
||||
(Infer (App (App (App (App (App (Ct0 ctid) x0) x1) x2) x3) x4))
|
||||
(Infer (Ct5 ctid orig x0 x1 x2 x3 x4)) =
|
||||
(Infer (App orig (App orig (App orig (App orig (App orig (Ct0 ctid orig) x0) x1) x2) x3) x4))
|
||||
|
||||
// Infers Ct6
|
||||
(Infer (Ct6 ctid x0 x1 x2 x3 x4 x5)) =
|
||||
(Infer (App (App (App (App (App (App (Ct0 ctid) x0) x1) x2) x3) x4) x5))
|
||||
(Infer (Ct6 ctid orig x0 x1 x2 x3 x4 x5)) =
|
||||
(Infer (App orig (App orig (App orig (App orig (App orig (App orig (Ct0 ctid orig) x0) x1) x2) x3) x4) x5))
|
||||
|
||||
// Infers Ct7
|
||||
(Infer (Ct7 ctid x0 x1 x2 x3 x4 x5 x6)) =
|
||||
(Infer (App (App (App (App (App (App (App (Ct0 ctid) x0) x1) x2) x3) x4) x5) x6))
|
||||
(Infer (Ct7 ctid orig x0 x1 x2 x3 x4 x5 x6)) =
|
||||
(Infer (App orig (App orig (App orig (App orig (App orig (App orig (App orig (Ct0 ctid orig) x0) x1) x2) x3) x4) x5) x6))
|
||||
|
||||
// Infers Ct8
|
||||
(Infer (Ct8 ctid x0 x1 x2 x3 x4 x5 x6 x7)) =
|
||||
(Infer (App (App (App (App (App (App (App (App (Ct0 ctid) x0) x1) x2) x3) x4) x5) x6) x7))
|
||||
(Infer (Ct8 ctid orig x0 x1 x2 x3 x4 x5 x6 x7)) =
|
||||
(Infer (App orig (App orig (App orig (App orig (App orig (App orig (App orig (App orig (Ct0 ctid orig) x0) x1) x2) x3) x4) x5) x6) x7))
|
||||
|
||||
// Infers Fn0
|
||||
(Infer (Fn0 ctid)) =
|
||||
(Infer (Fn0 ctid orig)) =
|
||||
(Checker.done (TypeOf ctid))
|
||||
|
||||
// Infers Fn1
|
||||
(Infer (Fn1 ctid x0)) =
|
||||
(Infer (App (Fn0 ctid) x0))
|
||||
(Infer (Fn1 ctid orig x0)) =
|
||||
(Infer (App orig (Fn0 ctid orig) x0))
|
||||
|
||||
// Infers Fn2
|
||||
(Infer (Fn2 ctid x0 x1)) =
|
||||
(Infer (App (App (Fn0 ctid) x0) x1))
|
||||
(Infer (Fn2 ctid orig x0 x1)) =
|
||||
(Infer (App orig (App orig (Fn0 ctid orig) x0) x1))
|
||||
|
||||
// Infers Fn3
|
||||
(Infer (Fn3 ctid x0 x1 x2)) =
|
||||
(Infer (App (App (App (Fn0 ctid) x0) x1) x2))
|
||||
(Infer (Fn3 ctid orig x0 x1 x2)) =
|
||||
(Infer (App orig (App orig (App orig (Fn0 ctid orig) x0) x1) x2))
|
||||
|
||||
// Infers Fn4
|
||||
(Infer (Fn4 ctid x0 x1 x2 x3)) =
|
||||
(Infer (App (App (App (App (Fn0 ctid) x0) x1) x2) x3))
|
||||
(Infer (Fn4 ctid orig x0 x1 x2 x3)) =
|
||||
(Infer (App orig (App orig (App orig (App orig (Fn0 ctid orig) x0) x1) x2) x3))
|
||||
|
||||
// Infers Fn5
|
||||
(Infer (Fn5 ctid x0 x1 x2 x3 x4)) =
|
||||
(Infer (App (App (App (App (App (Fn0 ctid) x0) x1) x2) x3) x4))
|
||||
(Infer (Fn5 ctid orig x0 x1 x2 x3 x4)) =
|
||||
(Infer (App orig (App orig (App orig (App orig (App orig (Fn0 ctid orig) x0) x1) x2) x3) x4))
|
||||
|
||||
// Infers Fn6
|
||||
(Infer (Fn6 ctid x0 x1 x2 x3 x4 x5)) =
|
||||
(Infer (App (App (App (App (App (App (Fn0 ctid) x0) x1) x2) x3) x4) x5))
|
||||
(Infer (Fn6 ctid orig x0 x1 x2 x3 x4 x5)) =
|
||||
(Infer (App orig (App orig (App orig (App orig (App orig (App orig (Fn0 ctid orig) x0) x1) x2) x3) x4) x5))
|
||||
|
||||
// Infers Fn7
|
||||
(Infer (Fn7 ctid x0 x1 x2 x3 x4 x5 x6)) =
|
||||
(Infer (App (App (App (App (App (App (App (Fn0 ctid) x0) x1) x2) x3) x4) x5) x6))
|
||||
(Infer (Fn7 ctid orig x0 x1 x2 x3 x4 x5 x6)) =
|
||||
(Infer (App orig (App orig (App orig (App orig (App orig (App orig (App orig (Fn0 ctid orig) x0) x1) x2) x3) x4) x5) x6))
|
||||
|
||||
// Infers Fn8
|
||||
(Infer (Fn8 ctid x0 x1 x2 x3 x4 x5 x6 x7)) =
|
||||
(Infer (App (App (App (App (App (App (App (App (Fn0 ctid) x0) x1) x2) x3) x4) x5) x6) x7))
|
||||
(Infer (Fn8 ctid orig x0 x1 x2 x3 x4 x5 x6 x7)) =
|
||||
(Infer (App orig (App orig (App orig (App orig (App orig (App orig (App orig (App orig (Fn0 ctid orig) x0) x1) x2) x3) x4) x5) x6) x7))
|
||||
|
||||
// Check Term Term : (Checker Unit)
|
||||
// --------------------------------
|
||||
|
||||
// Checks Lam
|
||||
(Check (Lam name body) (All t_name t_type t_body)) =
|
||||
(Check (Lam orig name body) (All t_orig t_name t_type t_body)) =
|
||||
ask dep = (Checker.bind Checker.get_depth)
|
||||
ask body_chk = (Checker.bind (Checker.extended (Check (body (Var name dep)) (t_body (Var t_name dep))) t_name t_type []))
|
||||
ask body_chk = (Checker.bind (Checker.extended (Check (body (Var orig name dep)) (t_body (Var orig t_name dep))) t_name t_type []))
|
||||
(Checker.done Unit)
|
||||
|
||||
// Checks Let
|
||||
(Check (Let name expr body) type) =
|
||||
(Check (Let orig name expr body) type) =
|
||||
ask dep = (Checker.bind Checker.get_depth)
|
||||
ask expr_typ = (Checker.bind (Infer expr))
|
||||
ask body_chk = (Checker.bind (Checker.extended (Check (body (Var name dep)) type) name expr_typ []))
|
||||
ask body_chk = (Checker.bind (Checker.extended (Check (body (Var orig name dep)) type) name expr_typ []))
|
||||
(Checker.done Unit)
|
||||
|
||||
// Checks Var
|
||||
(Check (Var name index) type) =
|
||||
(Check (Var orig name index) type) =
|
||||
ask rhs = (Checker.bind Checker.get_right_hand_side)
|
||||
(Bool.if rhs
|
||||
(Check.compare (Var name index) type)
|
||||
(If rhs
|
||||
(Check.compare (Var orig name index) type)
|
||||
(Checker.extend name type Nil))
|
||||
|
||||
// Checks others
|
||||
@ -499,19 +558,19 @@ Line = (String.cons 10 String.nil)
|
||||
(Check.compare term type) =
|
||||
ask term_typ = (Checker.bind (Infer term))
|
||||
ask is_equal = (Checker.bind (Equal term_typ type))
|
||||
(Bool.if is_equal
|
||||
(If is_equal
|
||||
(Checker.done Unit)
|
||||
(Checker.fail λctx λdep (TypeMismatch ctx dep type term_typ)))
|
||||
(Checker.fail (TypeMismatch term type term_typ)))
|
||||
|
||||
// Check.verify Verifier (List Term) : (Checker Unit)
|
||||
// --------------------------------------------------
|
||||
|
||||
(Check.verify (LHS arg args) (All name type body)) =
|
||||
(Check.verify (LHS arg args) (All orig name type body)) =
|
||||
ask arg_chk = (Checker.bind (Check arg type))
|
||||
ask args_chk = (Checker.bind (Check.verify args (body arg)))
|
||||
(Checker.done Unit)
|
||||
(Check.verify (LHS arg args) other) =
|
||||
(Checker.fail λctx λdep (InvalidEquationArity ctx dep))
|
||||
(Checker.fail (TooManyArguments arg))
|
||||
(Check.verify (RHS expr) type) =
|
||||
ask (Checker.bind (Checker.set_right_hand_side True))
|
||||
ask expr_chk = (Checker.bind (Check expr type))
|
||||
@ -520,70 +579,73 @@ Line = (String.cons 10 String.nil)
|
||||
// APP Term Term : Term
|
||||
// ----------------------
|
||||
|
||||
(APP (Lam name fbody) argm) = (fbody argm)
|
||||
(APP func argm) = (App func argm)
|
||||
(APP orig (Lam orig name fbody) argm) = (fbody argm)
|
||||
(APP orig func argm) = (App orig func argm)
|
||||
|
||||
// LET Name Term Term : Term
|
||||
// --------------------------
|
||||
|
||||
(LET name expr body) = (body expr)
|
||||
(LET orig name expr body) = (body expr)
|
||||
|
||||
// ANN Term Term : Term
|
||||
// --------------------------
|
||||
|
||||
(ANN expr type) = expr
|
||||
(ANN orig expr type) = expr
|
||||
|
||||
// Stringification
|
||||
// ---------------
|
||||
|
||||
(Show (Var name index)) = (Text [
|
||||
(Show (Var orig name index)) = (Text [
|
||||
(Show.name name)
|
||||
])
|
||||
|
||||
(Show Typ) = (Text [
|
||||
(Show (Typ orig)) = (Text [
|
||||
"Type"
|
||||
])
|
||||
|
||||
(Show (All name type body)) = (Text [
|
||||
"(" (Show.name name) ": " (Show type) ") "
|
||||
(Show (body (Var name 0)))
|
||||
])
|
||||
(Show (All orig name type body)) =
|
||||
(U60.if (== name 63) // underscore
|
||||
(Text [
|
||||
(Show type) " -> " (Show (body (Var orig name 0)))
|
||||
])
|
||||
(Text [
|
||||
"(" (Show.name name) ": " (Show type) ") "
|
||||
(Show (body (Var orig name 0)))
|
||||
]))
|
||||
|
||||
(Show (Lam name body)) = (Text [
|
||||
(Show (Lam orig name body)) = (Text [
|
||||
"@" (Show.name name) " "
|
||||
(Show (body (Var name 0)))
|
||||
(Show (body (Var orig name 0)))
|
||||
])
|
||||
|
||||
(Show (Let name expr body)) = (Text [
|
||||
"let " (Show.name name) " = " (Show (expr (Var name 0))) "; "
|
||||
(Show (body (Var name 0)))
|
||||
(Show (Let orig name expr body)) = (Text [
|
||||
"let " (Show.name name) " = " (Show (expr (Var orig name 0))) "; "
|
||||
(Show (body (Var orig name 0)))
|
||||
])
|
||||
|
||||
(Show (Ann expr type)) = (Text [
|
||||
(Show (Ann orig expr type)) = (Text [
|
||||
"{" (Show expr) " :: " (Show type) "}"
|
||||
])
|
||||
|
||||
(Show (App func argm)) = (Text [
|
||||
(Show (App orig func argm)) = (Text [
|
||||
"("
|
||||
(Show func) " "
|
||||
(Show argm)
|
||||
")"
|
||||
])
|
||||
|
||||
(Show (Ct0 ctid)) = (Text [
|
||||
"("
|
||||
(Show (Ct0 ctid orig)) = (Text [
|
||||
(NameOf ctid)
|
||||
")"
|
||||
])
|
||||
|
||||
(Show (Ct1 ctid x0)) = (Text [
|
||||
(Show (Ct1 ctid orig x0)) = (Text [
|
||||
"("
|
||||
(NameOf ctid) " "
|
||||
(Show x0)
|
||||
")"
|
||||
])
|
||||
|
||||
(Show (Ct2 ctid x0 x1)) = (Text [
|
||||
(Show (Ct2 ctid orig x0 x1)) = (Text [
|
||||
"("
|
||||
(NameOf ctid) " "
|
||||
(Show x0) " "
|
||||
@ -591,7 +653,7 @@ Line = (String.cons 10 String.nil)
|
||||
")"
|
||||
])
|
||||
|
||||
(Show (Ct3 ctid x0 x1 x2)) = (Text [
|
||||
(Show (Ct3 ctid orig x0 x1 x2)) = (Text [
|
||||
"("
|
||||
(NameOf ctid) " "
|
||||
(Show x0) " "
|
||||
@ -600,7 +662,7 @@ Line = (String.cons 10 String.nil)
|
||||
")"
|
||||
])
|
||||
|
||||
(Show (Ct4 ctid x0 x1 x2 x3)) = (Text [
|
||||
(Show (Ct4 ctid orig x0 x1 x2 x3)) = (Text [
|
||||
"("
|
||||
(NameOf ctid) " "
|
||||
(Show x0) " "
|
||||
@ -610,7 +672,7 @@ Line = (String.cons 10 String.nil)
|
||||
")"
|
||||
])
|
||||
|
||||
(Show (Ct5 ctid x0 x1 x2 x3 x4)) = (Text [
|
||||
(Show (Ct5 ctid orig x0 x1 x2 x3 x4)) = (Text [
|
||||
"("
|
||||
(NameOf ctid) " "
|
||||
(Show x0) " "
|
||||
@ -621,7 +683,7 @@ Line = (String.cons 10 String.nil)
|
||||
")"
|
||||
])
|
||||
|
||||
(Show (Ct6 ctid x0 x1 x2 x3 x4 x5)) = (Text [
|
||||
(Show (Ct6 ctid orig x0 x1 x2 x3 x4 x5)) = (Text [
|
||||
"("
|
||||
(NameOf ctid) " "
|
||||
(Show x0) " "
|
||||
@ -633,7 +695,7 @@ Line = (String.cons 10 String.nil)
|
||||
")"
|
||||
])
|
||||
|
||||
(Show (Ct7 ctid x0 x1 x2 x3 x4 x5 x6)) = (Text [
|
||||
(Show (Ct7 ctid orig x0 x1 x2 x3 x4 x5 x6)) = (Text [
|
||||
"("
|
||||
(NameOf ctid) " "
|
||||
(Show x0) " "
|
||||
@ -646,7 +708,7 @@ Line = (String.cons 10 String.nil)
|
||||
")"
|
||||
])
|
||||
|
||||
(Show (Ct8 ctid x0 x1 x2 x3 x4 x5 x6 x7)) = (Text [
|
||||
(Show (Ct8 ctid orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Text [
|
||||
"("
|
||||
(NameOf ctid) " "
|
||||
(Show x0) " "
|
||||
@ -660,20 +722,18 @@ Line = (String.cons 10 String.nil)
|
||||
")"
|
||||
])
|
||||
|
||||
(Show (Fn0 ctid)) = (Text [
|
||||
"("
|
||||
(Show (Fn0 ctid orig)) = (Text [
|
||||
(NameOf ctid)
|
||||
")"
|
||||
])
|
||||
|
||||
(Show (Fn1 ctid x0)) = (Text [
|
||||
(Show (Fn1 ctid orig x0)) = (Text [
|
||||
"("
|
||||
(NameOf ctid) " "
|
||||
(Show x0)
|
||||
")"
|
||||
])
|
||||
|
||||
(Show (Fn2 ctid x0 x1)) = (Text [
|
||||
(Show (Fn2 ctid orig x0 x1)) = (Text [
|
||||
"("
|
||||
(NameOf ctid) " "
|
||||
(Show x0) " "
|
||||
@ -681,7 +741,7 @@ Line = (String.cons 10 String.nil)
|
||||
")"
|
||||
])
|
||||
|
||||
(Show (Fn3 ctid x0 x1 x2)) = (Text [
|
||||
(Show (Fn3 ctid orig x0 x1 x2)) = (Text [
|
||||
"("
|
||||
(NameOf ctid) " "
|
||||
(Show x0) " "
|
||||
@ -690,7 +750,7 @@ Line = (String.cons 10 String.nil)
|
||||
")"
|
||||
])
|
||||
|
||||
(Show (Fn4 ctid x0 x1 x2 x3)) = (Text [
|
||||
(Show (Fn4 ctid orig x0 x1 x2 x3)) = (Text [
|
||||
"("
|
||||
(NameOf ctid) " "
|
||||
(Show x0) " "
|
||||
@ -700,7 +760,7 @@ Line = (String.cons 10 String.nil)
|
||||
")"
|
||||
])
|
||||
|
||||
(Show (Fn5 ctid x0 x1 x2 x3 x4)) = (Text [
|
||||
(Show (Fn5 ctid orig x0 x1 x2 x3 x4)) = (Text [
|
||||
"("
|
||||
(NameOf ctid) " "
|
||||
(Show x0) " "
|
||||
@ -711,7 +771,7 @@ Line = (String.cons 10 String.nil)
|
||||
")"
|
||||
])
|
||||
|
||||
(Show (Fn6 ctid x0 x1 x2 x3 x4 x5)) = (Text [
|
||||
(Show (Fn6 ctid orig x0 x1 x2 x3 x4 x5)) = (Text [
|
||||
"("
|
||||
(NameOf ctid) " "
|
||||
(Show x0) " "
|
||||
@ -723,7 +783,7 @@ Line = (String.cons 10 String.nil)
|
||||
")"
|
||||
])
|
||||
|
||||
(Show (Fn7 ctid x0 x1 x2 x3 x4 x5 x6)) = (Text [
|
||||
(Show (Fn7 ctid orig x0 x1 x2 x3 x4 x5 x6)) = (Text [
|
||||
"("
|
||||
(NameOf ctid) " "
|
||||
(Show x0) " "
|
||||
@ -736,7 +796,7 @@ Line = (String.cons 10 String.nil)
|
||||
")"
|
||||
])
|
||||
|
||||
(Show (Fn8 ctid x0 x1 x2 x3 x4 x5 x6 x7)) = (Text [
|
||||
(Show (Fn8 ctid orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Text [
|
||||
"("
|
||||
(NameOf ctid) " "
|
||||
(Show x0) " "
|
||||
@ -796,12 +856,12 @@ Line = (String.cons 10 String.nil)
|
||||
|
||||
API.check_all =
|
||||
let output = (API.output (List.reverse (API.check_functions Functions)))
|
||||
(Bool.if (String.is_empty output)
|
||||
(If (String.is_empty output)
|
||||
(Text [ "All terms check." Line Line ])
|
||||
output)
|
||||
|
||||
API.run_main = (Text [
|
||||
(Show (FN0 Main.))
|
||||
(Show (FN0 Main. 0))
|
||||
Line Line
|
||||
])
|
||||
|
||||
@ -834,40 +894,52 @@ API.run_main = (Text [
|
||||
String.nil
|
||||
(API.output.function fnid (Cons (Checked ctx dep rhs val) checks)) =
|
||||
(API.output.function fnid checks)
|
||||
(API.output.function fnid (Cons (Errored err) checks)) =
|
||||
(API.output.function fnid (Cons (Errored ctx err) checks)) =
|
||||
(Text [
|
||||
(Color "1") (Color "31") "Error on " (NameOf fnid) ":" (Color "0") Line
|
||||
Line
|
||||
(API.output.error err) Line
|
||||
(Color "1") "[" (NameOf fnid) "] " (Color "0") Line
|
||||
(API.output.error err ctx) Line
|
||||
(API.output.function fnid checks)
|
||||
])
|
||||
|
||||
(API.output.error (UnboundVariable ctx dep)) =
|
||||
(API.output.error (UnboundVariable term) ctx) =
|
||||
(Text [
|
||||
"Unbound Variable."
|
||||
(Color "4") "Unbound Variable." (Color "0") Line
|
||||
(API.output.error.details ctx term)
|
||||
])
|
||||
(API.output.error (CantInferLambda ctx dep)) =
|
||||
(API.output.error (CantInferLambda term) ctx) =
|
||||
(Text [
|
||||
"Can't infer lambda."
|
||||
(Color "4") "Can't infer lambda." (Color "0") Line
|
||||
(API.output.error.details ctx term)
|
||||
])
|
||||
(API.output.error (InvalidEquationArity ctx dep)) =
|
||||
(API.output.error (TooManyArguments term) ctx) =
|
||||
(Text [
|
||||
"Invalid equation arity."
|
||||
(Color "4") "Too many arguments." (Color "0") Line
|
||||
(API.output.error.details ctx term)
|
||||
])
|
||||
(API.output.error (NonFunctionApplication ctx dep)) =
|
||||
(API.output.error (InvalidCall term) ctx) =
|
||||
(Text [
|
||||
"Non-function application."
|
||||
(Color "4") "Invalid call." (Color "0") Line
|
||||
(API.output.error.details ctx term)
|
||||
])
|
||||
(API.output.error (TypeMismatch ctx dep expected detected)) =
|
||||
(API.output.error (TypeMismatch term expected detected) ctx) =
|
||||
(Text [
|
||||
"Type mismatch." Line
|
||||
(Color "4") "Type mismatch." (Color "0") Line
|
||||
"- Expected: " (Show expected) Line
|
||||
"- Detected: " (Show detected) Line
|
||||
(Bool.if (Context.is_empty ctx) "" (Text [
|
||||
"With context:" Line
|
||||
(API.output.error.details ctx term)
|
||||
])
|
||||
|
||||
(API.output.error.details ctx term) =
|
||||
let orig = (Term.get_origin term)
|
||||
(Text [
|
||||
(If (Context.is_empty ctx) "" (Text [
|
||||
(Color "4") "Context:" (Color "0") Line
|
||||
(Show.context ctx)
|
||||
]))
|
||||
(Color "4") "Source:" (Color "0") Line
|
||||
"{{#"(Show.u60 (& orig 16777215))":"(Show.u60 (>> orig 24))"#}}" Line
|
||||
])
|
||||
|
||||
|
||||
// User-Defined Functions
|
||||
// ----------------------
|
||||
|
||||
269
src/language.rs
269
src/language.rs
@ -31,15 +31,15 @@ pub struct Rule {
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub enum Term {
|
||||
Typ,
|
||||
Var { name: String },
|
||||
All { name: String, tipo: Box<Term>, body: Box<Term> },
|
||||
Lam { name: String, body: Box<Term> },
|
||||
App { func: Box<Term>, argm: Box<Term> },
|
||||
Let { name: String, expr: Box<Term>, body: Box<Term> },
|
||||
Ann { expr: Box<Term>, tipo: Box<Term> },
|
||||
Ctr { name: String, args: Vec<Box<Term>> },
|
||||
Fun { name: String, args: Vec<Box<Term>> },
|
||||
Typ { orig: u64 },
|
||||
Var { orig: u64, name: String },
|
||||
All { orig: u64, name: String, tipo: Box<Term>, body: Box<Term> },
|
||||
Lam { orig: u64, name: String, body: Box<Term> },
|
||||
App { orig: u64, func: Box<Term>, argm: Box<Term> },
|
||||
Let { orig: u64, name: String, expr: Box<Term>, body: Box<Term> },
|
||||
Ann { orig: u64, expr: Box<Term>, tipo: Box<Term> },
|
||||
Ctr { orig: u64, name: String, args: Vec<Box<Term>> },
|
||||
Fun { orig: u64, name: String, args: Vec<Box<Term>> },
|
||||
}
|
||||
|
||||
// Adjuster
|
||||
@ -91,52 +91,59 @@ pub fn adjust_rule(file: &File, rule: &Rule) -> Rule {
|
||||
// TODO: prevent defining the same name twice
|
||||
pub fn adjust_term(file: &File, term: &Term) -> Term {
|
||||
match *term {
|
||||
Term::Typ => {
|
||||
Term::Typ
|
||||
Term::Typ { orig } => {
|
||||
Term::Typ { orig }
|
||||
},
|
||||
Term::Var { ref name } => {
|
||||
Term::Var { name: name.clone() }
|
||||
Term::Var { ref orig, ref name } => {
|
||||
let orig = *orig;
|
||||
Term::Var { orig, name: name.clone() }
|
||||
},
|
||||
Term::Let { ref name, ref expr, ref body } => {
|
||||
Term::Let { ref orig, ref name, ref expr, ref body } => {
|
||||
let orig = *orig;
|
||||
let expr = Box::new(adjust_term(file, &*expr));
|
||||
let body = Box::new(adjust_term(file, &*body));
|
||||
Term::Let { name: name.clone(), expr, body }
|
||||
Term::Let { orig, name: name.clone(), expr, body }
|
||||
},
|
||||
Term::Ann { ref expr, ref tipo } => {
|
||||
Term::Ann { ref orig, ref expr, ref tipo } => {
|
||||
let orig = *orig;
|
||||
let expr = Box::new(adjust_term(file, &*expr));
|
||||
let tipo = Box::new(adjust_term(file, &*tipo));
|
||||
Term::Ann { expr, tipo }
|
||||
Term::Ann { orig, expr, tipo }
|
||||
},
|
||||
Term::All { ref name, ref tipo, ref body } => {
|
||||
Term::All { ref orig, ref name, ref tipo, ref body } => {
|
||||
let orig = *orig;
|
||||
let tipo = Box::new(adjust_term(file, &*tipo));
|
||||
let body = Box::new(adjust_term(file, &*body));
|
||||
Term::All { name: name.clone(), tipo, body }
|
||||
Term::All { orig, name: name.clone(), tipo, body }
|
||||
},
|
||||
Term::Lam { ref name, ref body } => {
|
||||
Term::Lam { ref orig, ref name, ref body } => {
|
||||
let orig = *orig;
|
||||
let body = Box::new(adjust_term(file, &*body));
|
||||
Term::Lam { name: name.clone(), body }
|
||||
Term::Lam { orig, name: name.clone(), body }
|
||||
},
|
||||
Term::App { ref func, ref argm } => {
|
||||
Term::App { ref orig, ref func, ref argm } => {
|
||||
let orig = *orig;
|
||||
let func = Box::new(adjust_term(file, &*func));
|
||||
let argm = Box::new(adjust_term(file, &*argm));
|
||||
Term::App { func, argm }
|
||||
Term::App { orig, func, argm }
|
||||
},
|
||||
Term::Ctr { ref name, ref args } => {
|
||||
Term::Ctr { ref orig, ref name, ref args } => {
|
||||
let orig = *orig;
|
||||
if let Some(entry) = file.entries.get(name) {
|
||||
let mut new_args = Vec::new();
|
||||
for arg in args {
|
||||
new_args.push(Box::new(adjust_term(file, &*arg)));
|
||||
}
|
||||
if entry.rules.len() > 0 {
|
||||
Term::Fun { name: name.clone(), args: new_args }
|
||||
Term::Fun { orig, name: name.clone(), args: new_args }
|
||||
} else {
|
||||
Term::Ctr { name: name.clone(), args: new_args }
|
||||
Term::Ctr { orig, name: name.clone(), args: new_args }
|
||||
}
|
||||
} else {
|
||||
panic!("Missing declaration for: '{}'.", name);
|
||||
}
|
||||
},
|
||||
Term::Fun { ref name, ref args } => {
|
||||
Term::Fun { ref orig, ref name, ref args } => {
|
||||
panic!("Internal error."); // shouldn't happen since we can't parse Fun{}
|
||||
},
|
||||
}
|
||||
@ -145,6 +152,19 @@ pub fn adjust_term(file: &File, term: &Term) -> Term {
|
||||
// Parser
|
||||
// ======
|
||||
|
||||
pub fn origin(init: usize, last: usize) -> u64 {
|
||||
((init as u64) & 0xFFFFFF) | (((last as u64) & 0xFFFFFF) << 24)
|
||||
}
|
||||
|
||||
pub fn get_init_index(state: parser::State) -> parser::Answer<usize> {
|
||||
let (state, _) = parser::skip(state)?;
|
||||
Ok((state, state.index))
|
||||
}
|
||||
|
||||
pub fn get_last_index(state: parser::State) -> parser::Answer<usize> {
|
||||
Ok((state, state.index))
|
||||
}
|
||||
|
||||
pub fn is_var_head(head: char) -> bool {
|
||||
('a'..='z').contains(&head) || head == '_' || head == '$'
|
||||
}
|
||||
@ -180,8 +200,11 @@ pub fn parse_var(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
|
||||
Ok((state, is_var_head(head)))
|
||||
}),
|
||||
Box::new(|state| {
|
||||
let (state, init) = get_init_index(state)?;
|
||||
let (state, name) = parse_var_name(state)?;
|
||||
Ok((state, Box::new(Term::Var { name })))
|
||||
let (state, last) = get_last_index(state)?;
|
||||
let orig = origin(init, last);
|
||||
Ok((state, Box::new(Term::Var { orig, name })))
|
||||
}),
|
||||
state,
|
||||
)
|
||||
@ -191,10 +214,13 @@ pub fn parse_lam(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
|
||||
parser::guard(
|
||||
parser::text_parser("@"),
|
||||
Box::new(move |state| {
|
||||
let (state, init) = get_init_index(state)?;
|
||||
let (state, _) = parser::consume("@", state)?;
|
||||
let (state, name) = parse_var_name(state)?;
|
||||
let (state, body) = parse_term(state)?;
|
||||
Ok((state, Box::new(Term::Lam { name, body })))
|
||||
let (state, last) = get_last_index(state)?;
|
||||
let orig = origin(init, last);
|
||||
Ok((state, Box::new(Term::Lam { orig, name, body })))
|
||||
}),
|
||||
state,
|
||||
)
|
||||
@ -209,13 +235,16 @@ pub fn parse_all(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
|
||||
Ok((state, all0 && all1 && name.len() > 0 && is_var_head(name.chars().nth(0).unwrap_or(' '))))
|
||||
}),
|
||||
Box::new(|state| {
|
||||
let (state, init) = get_init_index(state)?;
|
||||
let (state, _) = parser::consume("(", state)?;
|
||||
let (state, name) = parse_var_name(state)?;
|
||||
let (state, _) = parser::consume(":", state)?;
|
||||
let (state, tipo) = parse_term(state)?;
|
||||
let (state, _) = parser::consume(")", state)?;
|
||||
let (state, body) = parse_term(state)?;
|
||||
Ok((state, Box::new(Term::All { name, tipo, body })))
|
||||
let (state, last) = get_last_index(state)?;
|
||||
let orig = origin(init, last);
|
||||
Ok((state, Box::new(Term::All { orig, name, tipo, body })))
|
||||
}),
|
||||
state,
|
||||
)
|
||||
@ -225,16 +254,36 @@ pub fn parse_app(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
|
||||
return parser::guard(
|
||||
parser::text_parser("("),
|
||||
Box::new(|state| {
|
||||
parser::list(
|
||||
let (state, init_index) = get_init_index(state)?;
|
||||
parser::list::<(usize, usize, Box<Term>),Box<Term>> (
|
||||
parser::text_parser("("),
|
||||
parser::text_parser(""),
|
||||
parser::text_parser(")"),
|
||||
Box::new(parse_term),
|
||||
Box::new(|state| {
|
||||
let (state, init) = get_init_index(state)?;
|
||||
let (state, term) = parse_term(state)?;
|
||||
let (state, last) = get_last_index(state)?;
|
||||
return Ok((state, (init, last, term)));
|
||||
}),
|
||||
Box::new(|args| {
|
||||
if !args.is_empty() {
|
||||
args.into_iter().reduce(|a, b| Box::new(Term::App { func: a, argm: b })).unwrap()
|
||||
let (app_init_index, app_last_index, func) = &args[0];
|
||||
let mut term = func.clone();
|
||||
for i in 1 .. args.len() {
|
||||
let (argm_init_index, argm_last_index, argm) = &args[i];
|
||||
term = Box::new(Term::App {
|
||||
orig: origin(*app_init_index, *argm_last_index),
|
||||
func: term,
|
||||
argm: argm.clone(),
|
||||
});
|
||||
}
|
||||
return term;
|
||||
} else {
|
||||
Box::new(Term::Var { name: "?".to_string() })
|
||||
// TODO: "()" could make an Unit?
|
||||
return Box::new(Term::Var {
|
||||
orig: 0,
|
||||
name: "?".to_string(),
|
||||
});
|
||||
}
|
||||
}),
|
||||
state,
|
||||
@ -248,13 +297,16 @@ pub fn parse_let(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
|
||||
return parser::guard(
|
||||
parser::text_parser("let "),
|
||||
Box::new(|state| {
|
||||
let (state, init) = get_init_index(state)?;
|
||||
let (state, _) = parser::consume("let ", state)?;
|
||||
let (state, name) = parse_var_name(state)?;
|
||||
let (state, _) = parser::consume("=", state)?;
|
||||
let (state, expr) = parse_term(state)?;
|
||||
let (state, _) = parser::text(";", state)?;
|
||||
let (state, body) = parse_term(state)?;
|
||||
Ok((state, Box::new(Term::Let { name, expr, body })))
|
||||
let (state, last) = get_last_index(state)?;
|
||||
let orig = origin(init, last);
|
||||
Ok((state, Box::new(Term::Let { orig, name, expr, body })))
|
||||
}),
|
||||
state,
|
||||
);
|
||||
@ -264,12 +316,15 @@ pub fn parse_ann(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
|
||||
return parser::guard(
|
||||
parser::text_parser("{"),
|
||||
Box::new(|state| {
|
||||
let (state, init) = get_init_index(state)?;
|
||||
let (state, _) = parser::consume("{", state)?;
|
||||
let (state, expr) = parse_term(state)?;
|
||||
let (state, _) = parser::text("::", state)?;
|
||||
let (state, tipo) = parse_term(state)?;
|
||||
let (state, _) = parser::consume("}", state)?;
|
||||
Ok((state, Box::new(Term::Ann { expr, tipo })))
|
||||
let (state, last) = get_last_index(state)?;
|
||||
let orig = origin(init, last);
|
||||
Ok((state, Box::new(Term::Ann { orig, expr, tipo })))
|
||||
}),
|
||||
state,
|
||||
);
|
||||
@ -283,17 +338,22 @@ pub fn parse_ctr(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
|
||||
Ok((state, is_ctr_head(head)))
|
||||
}),
|
||||
Box::new(|state| {
|
||||
let (state, init) = get_init_index(state)?;
|
||||
let (state, open) = parser::text("(", state)?;
|
||||
let (state, name) = parse_ctr_name(state)?;
|
||||
if name == "Type" {
|
||||
Ok((state, Box::new(Term::Typ)))
|
||||
let (state, last) = get_last_index(state)?;
|
||||
let orig = origin(init, last);
|
||||
Ok((state, Box::new(Term::Typ { orig })))
|
||||
} else {
|
||||
let (state, args) = if open {
|
||||
parser::until(parser::text_parser(")"), Box::new(parse_term), state)?
|
||||
} else {
|
||||
(state, Vec::new())
|
||||
};
|
||||
Ok((state, Box::new(Term::Ctr { name, args })))
|
||||
let (state, last) = get_last_index(state)?;
|
||||
let orig = origin(init, last);
|
||||
Ok((state, Box::new(Term::Ctr { orig, name, args })))
|
||||
}
|
||||
}),
|
||||
state,
|
||||
@ -304,25 +364,30 @@ pub fn parse_hlp(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
|
||||
return parser::guard(
|
||||
parser::text_parser("?"),
|
||||
Box::new(|state| {
|
||||
let (state, init) = get_init_index(state)?;
|
||||
let (state, _) = parser::consume("?", state)?;
|
||||
let (state, name) = parser::name_here(state)?;
|
||||
Ok((state, Box::new(Term::Typ))) // TODO: Help constructor
|
||||
let (state, last) = get_last_index(state)?;
|
||||
let orig = origin(init, last);
|
||||
Ok((state, Box::new(Term::Typ { orig }))) // TODO: Help constructor
|
||||
}),
|
||||
state,
|
||||
);
|
||||
}
|
||||
|
||||
pub fn parse_arr(state: parser::State) -> parser::Answer<Option<Box<dyn Fn(Box<Term>) -> Box<Term>>>> {
|
||||
pub fn parse_arr(state: parser::State) -> parser::Answer<Option<Box<dyn Fn(usize, Box<Term>) -> Box<Term>>>> {
|
||||
return parser::guard(
|
||||
parser::text_parser("->"),
|
||||
Box::new(|state| {
|
||||
let (state, _) = parser::consume("->", state)?;
|
||||
let (state, body) = parse_term(state)?;
|
||||
Ok((state, Box::new(move |tipo| {
|
||||
let (state, last) = get_last_index(state)?;
|
||||
Ok((state, Box::new(move |init, tipo| {
|
||||
let orig = origin(init, last);
|
||||
let name = "_".to_string();
|
||||
let tipo = tipo.clone();
|
||||
let body = body.clone();
|
||||
Box::new(Term::All { name, tipo, body })
|
||||
Box::new(Term::All { orig, name, tipo, body })
|
||||
})))
|
||||
}),
|
||||
state,
|
||||
@ -343,17 +408,18 @@ pub fn parse_term_prefix(state: parser::State) -> parser::Answer<Box<Term>> {
|
||||
], state)
|
||||
}
|
||||
|
||||
pub fn parse_term_suffix(state: parser::State) -> parser::Answer<Box<dyn Fn(Box<Term>) -> Box<Term>>> {
|
||||
pub fn parse_term_suffix(state: parser::State) -> parser::Answer<Box<dyn Fn(usize,Box<Term>) -> Box<Term>>> {
|
||||
parser::grammar("Term", &[
|
||||
Box::new(parse_arr),
|
||||
Box::new(|state| Ok((state, Some(Box::new(|term| term))))),
|
||||
Box::new(|state| Ok((state, Some(Box::new(|init, term| term))))),
|
||||
], state)
|
||||
}
|
||||
|
||||
pub fn parse_term(state: parser::State) -> parser::Answer<Box<Term>> {
|
||||
let (state, init) = get_init_index(state)?;
|
||||
let (state, prefix) = parse_term_prefix(state)?;
|
||||
let (state, suffix) = parse_term_suffix(state)?;
|
||||
return Ok((state, suffix(prefix)));
|
||||
return Ok((state, suffix(init, prefix)));
|
||||
}
|
||||
|
||||
pub fn parse_entry(state: parser::State) -> parser::Answer<Box<Entry>> {
|
||||
@ -368,7 +434,7 @@ pub fn parse_entry(state: parser::State) -> parser::Answer<Box<Entry>> {
|
||||
let (state, anno) = parser::consume(":", state)?;
|
||||
parse_term(state)?
|
||||
} else {
|
||||
(state, Box::new(Term::Typ)) // TODO: return a hole
|
||||
(state, Box::new(Term::Typ { orig: 0 })) // TODO: return a hole, set orig
|
||||
};
|
||||
let (state, head) = parser::peek_char(state)?;
|
||||
if head == '{' {
|
||||
@ -377,7 +443,7 @@ pub fn parse_entry(state: parser::State) -> parser::Answer<Box<Entry>> {
|
||||
let (state, _) = parser::consume("}", state)?;
|
||||
let mut pats = vec![];
|
||||
for arg in &args {
|
||||
pats.push(Box::new(Term::Var { name: arg.name.clone() }));
|
||||
pats.push(Box::new(Term::Var { orig: 0, name: arg.name.clone() })); // TODO: set orig
|
||||
}
|
||||
let rules = vec![Box::new(Rule { name: name.clone(), pats, body })];
|
||||
return Ok((state, Box::new(Entry { name, args, tipo, rules })));
|
||||
@ -429,44 +495,44 @@ pub fn parse_file(state: parser::State) -> parser::Answer<Box<File>> {
|
||||
|
||||
pub fn show_term(term: &Term) -> String {
|
||||
match term {
|
||||
Term::Typ => {
|
||||
Term::Typ { .. } => {
|
||||
format!("Type")
|
||||
}
|
||||
Term::Var { name } => {
|
||||
Term::Var { orig: _, name } => {
|
||||
format!("{}", name)
|
||||
}
|
||||
Term::Lam { name, body } => {
|
||||
Term::Lam { orig: _, name, body } => {
|
||||
let body = show_term(body);
|
||||
format!("@{}({})", name, body)
|
||||
}
|
||||
Term::App { func, argm } => {
|
||||
Term::App { orig: _, func, argm } => {
|
||||
let mut args = vec![argm];
|
||||
let mut expr = func;
|
||||
while let Term::App { func, argm } = &**expr {
|
||||
while let Term::App { orig: _, func, argm } = &**expr {
|
||||
args.push(argm);
|
||||
expr = func;
|
||||
}
|
||||
args.reverse();
|
||||
format!("({} {})", show_term(expr), args.iter().map(|x| show_term(x)).collect::<Vec<String>>().join(" "))
|
||||
}
|
||||
Term::All { name, tipo, body } => {
|
||||
Term::All { orig: _, name, tipo, body } => {
|
||||
let body = show_term(body);
|
||||
format!("({}: {}) {}", name, show_term(tipo), body)
|
||||
}
|
||||
Term::Let { name, expr, body } => {
|
||||
Term::Let { orig: _, name, expr, body } => {
|
||||
let expr = show_term(expr);
|
||||
let body = show_term(body);
|
||||
format!("let {} = {}; {}", name, expr, body)
|
||||
}
|
||||
Term::Ann { expr, tipo } => {
|
||||
Term::Ann { orig: _, expr, tipo } => {
|
||||
let expr = show_term(expr);
|
||||
let tipo = show_term(tipo);
|
||||
format!("{{{} :: {}}}", expr, tipo)
|
||||
}
|
||||
Term::Ctr { name, args } => {
|
||||
Term::Ctr { orig: _, name, args } => {
|
||||
format!("({}{})", name, args.iter().map(|x| format!(" {}",show_term(x))).collect::<String>())
|
||||
}
|
||||
Term::Fun { name, args } => {
|
||||
Term::Fun { orig: _, name, args } => {
|
||||
format!("({}{})", name, args.iter().map(|x| format!(" {}",show_term(x))).collect::<String>())
|
||||
}
|
||||
}
|
||||
@ -528,42 +594,57 @@ pub fn read_file(code: &str) -> Result<Box<File>, String> {
|
||||
//Ctr { name: String, args: Vec<Box<Term>> },
|
||||
//Fun { name: String, args: Vec<Box<Term>> },
|
||||
//}
|
||||
pub fn compile_term(term: &Term, quote: bool) -> String {
|
||||
pub fn compile_term(term: &Term, quote: bool, lhs: bool) -> String {
|
||||
fn hide(orig: &u64, lhs: bool) -> String {
|
||||
if lhs {
|
||||
"orig".to_string()
|
||||
} else {
|
||||
format!("{}", orig)
|
||||
}
|
||||
}
|
||||
match term {
|
||||
Term::Typ => {
|
||||
format!("Typ")
|
||||
Term::Typ { orig } => {
|
||||
format!("(Typ {})", hide(orig,lhs))
|
||||
}
|
||||
Term::Var { name } => {
|
||||
name.clone()
|
||||
Term::Var { orig, name } => {
|
||||
if lhs {
|
||||
format!("{}", name)
|
||||
} else {
|
||||
if quote {
|
||||
format!("(SO {} {})", orig, name.clone())
|
||||
} else {
|
||||
format!("( {} {})", " ".repeat(format!("{}",orig).len()), name.clone()) // spaces to align with quoted version
|
||||
}
|
||||
}
|
||||
}
|
||||
Term::All { name, tipo, body } => {
|
||||
format!("(All {} {} λ{} {})", name_to_u64(name), compile_term(tipo, quote), name, compile_term(body, quote))
|
||||
Term::All { orig, name, tipo, body } => {
|
||||
format!("(All {} {} {} λ{} {})", hide(orig,lhs), name_to_u64(name), compile_term(tipo, quote, lhs), name, compile_term(body, quote, lhs))
|
||||
}
|
||||
Term::Lam { name, body } => {
|
||||
format!("(Lam {} λ{} {})", name_to_u64(name), name, compile_term(body, quote))
|
||||
Term::Lam { orig, name, body } => {
|
||||
format!("(Lam {} {} λ{} {})", hide(orig,lhs), name_to_u64(name), name, compile_term(body, quote, lhs))
|
||||
}
|
||||
Term::App { func, argm } => {
|
||||
format!("({} {} {})", if quote { "App" } else { "APP" }, compile_term(func, quote), compile_term(argm, quote))
|
||||
Term::App { orig, func, argm } => {
|
||||
format!("({} {} {} {})", if quote { "App" } else { "APP" }, hide(orig,lhs), compile_term(func, quote, lhs), compile_term(argm, quote, lhs))
|
||||
}
|
||||
Term::Let { name, expr, body } => {
|
||||
format!("({} {} {} λ{} {})", if quote { "Let" } else { "LET" }, name_to_u64(name), compile_term(expr, quote), name, compile_term(body, quote))
|
||||
Term::Let { orig, name, expr, body } => {
|
||||
format!("({} {} {} {} λ{} {})", if quote { "Let" } else { "LET" }, hide(orig,lhs), name_to_u64(name), compile_term(expr, quote, lhs), name, compile_term(body, quote, lhs))
|
||||
}
|
||||
Term::Ann { expr, tipo } => {
|
||||
format!("({} {} {})", if quote { "Ann" } else { "ANN" }, compile_term(expr, quote), compile_term(tipo, quote))
|
||||
Term::Ann { orig, expr, tipo } => {
|
||||
format!("({} {} {} {})", if quote { "Ann" } else { "ANN" }, hide(orig,lhs), compile_term(expr, quote, lhs), compile_term(tipo, quote, lhs))
|
||||
}
|
||||
Term::Ctr { name, args } => {
|
||||
Term::Ctr { orig, name, args } => {
|
||||
let mut args_strs : Vec<String> = Vec::new();
|
||||
for arg in args {
|
||||
args_strs.push(format!(" {}", compile_term(arg, quote)));
|
||||
args_strs.push(format!(" {}", compile_term(arg, quote, lhs)));
|
||||
}
|
||||
format!("(Ct{} {}.{})", args.len(), name, args_strs.join(""))
|
||||
format!("(Ct{} {}. {}{})", args.len(), name, hide(orig,lhs), args_strs.join(""))
|
||||
}
|
||||
Term::Fun { name, args } => {
|
||||
Term::Fun { orig, name, args } => {
|
||||
let mut args_strs : Vec<String> = Vec::new();
|
||||
for arg in args {
|
||||
args_strs.push(format!(" {}", compile_term(arg, quote)));
|
||||
args_strs.push(format!(" {}", compile_term(arg, quote, lhs)));
|
||||
}
|
||||
format!("({}{} {}.{})", if quote { "Fn" } else { "FN" }, args.len(), name, args_strs.join(""))
|
||||
format!("({}{} {}. {}{})", if quote { "Fn" } else { "FN" }, args.len(), name, hide(orig,lhs), args_strs.join(""))
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -572,22 +653,22 @@ pub fn compile_entry(entry: &Entry) -> String {
|
||||
fn compile_type(args: &Vec<Box<Argument>>, tipo: &Box<Term>, index: usize) -> String {
|
||||
if index < args.len() {
|
||||
let arg = &args[index];
|
||||
format!("(All {} {} λ{} {})", name_to_u64(&arg.name), compile_term(&arg.tipo, false), arg.name, compile_type(args, tipo, index + 1))
|
||||
format!("(All {} {} {} λ{} {})", 0, name_to_u64(&arg.name), compile_term(&arg.tipo, false, false), arg.name, compile_type(args, tipo, index + 1))
|
||||
} else {
|
||||
compile_term(tipo, false)
|
||||
compile_term(tipo, false, false)
|
||||
}
|
||||
}
|
||||
|
||||
fn compile_rule(rule: &Rule) -> String {
|
||||
let mut pats = vec![];
|
||||
for pat in &rule.pats {
|
||||
pats.push(format!(" {}", compile_term(pat, false)));
|
||||
pats.push(format!(" {}", compile_term(pat, false, true)));
|
||||
}
|
||||
let body_rhs = compile_term(&rule.body, true);
|
||||
let rule_rhs = compile_term(&rule.body, false);
|
||||
let body_rhs = compile_term(&rule.body, true, false);
|
||||
let rule_rhs = compile_term(&rule.body, false, false);
|
||||
let mut text = String::new();
|
||||
text.push_str(&format!("(QT{} {}.{}) = {}\n", rule.pats.len(), rule.name, pats.join(""), body_rhs));
|
||||
text.push_str(&format!("(FN{} {}.{}) = {}\n", rule.pats.len(), rule.name, pats.join(""), rule_rhs));
|
||||
text.push_str(&format!("(QT{} {}. orig{}) = {}\n", rule.pats.len(), rule.name, pats.join(""), body_rhs));
|
||||
text.push_str(&format!("(FN{} {}. orig{}) = {}\n", rule.pats.len(), rule.name, pats.join(""), rule_rhs));
|
||||
return text;
|
||||
}
|
||||
|
||||
@ -597,8 +678,8 @@ pub fn compile_entry(entry: &Entry) -> String {
|
||||
vars.push(format!(" x{}", idx));
|
||||
}
|
||||
let mut text = String::new();
|
||||
text.push_str(&format!("(QT{} {}.{}) = (Fn{} {}.{})\n", size, name, vars.join(""), size, name, vars.join("")));
|
||||
text.push_str(&format!("(FN{} {}.{}) = (Fn{} {}.{})\n", size, name, vars.join(""), size, name, vars.join("")));
|
||||
text.push_str(&format!("(QT{} {}. orig{}) = (Fn{} {}. orig{})\n", size, name, vars.join(""), size, name, vars.join("")));
|
||||
text.push_str(&format!("(FN{} {}. orig{}) = (Fn{} {}. orig{})\n", size, name, vars.join(""), size, name, vars.join("")));
|
||||
return text;
|
||||
}
|
||||
|
||||
@ -610,20 +691,20 @@ pub fn compile_entry(entry: &Entry) -> String {
|
||||
let tail = compile_rule_chk(rule, index + 1, vars, args);
|
||||
return format!("(LHS {} {})", head, tail);
|
||||
} else {
|
||||
return format!("(RHS (QT{} {}.{}))", index, rule.name, args.iter().map(|x| format!(" {}", x)).collect::<Vec<String>>().join(""));
|
||||
return format!("(RHS (QT{} {}. 0{}))", index, rule.name, args.iter().map(|x| format!(" {}", x)).collect::<Vec<String>>().join(""));
|
||||
}
|
||||
}
|
||||
|
||||
fn compile_patt_chk(patt: &Term, vars: &mut u64) -> (String, String) {
|
||||
// FIXME: remove redundancy
|
||||
match patt {
|
||||
Term::Var { name } => {
|
||||
let inp = format!("(Var {} {})", name_to_u64(name), vars);
|
||||
let var = format!("(Var {} {})", name_to_u64(name), vars);
|
||||
Term::Var { orig, name } => {
|
||||
let inp = format!("(Var {} {} {})", orig, name_to_u64(name), vars);
|
||||
let var = format!("(Var {} {} {})", orig, name_to_u64(name), vars);
|
||||
*vars += 1;
|
||||
return (inp, var);
|
||||
}
|
||||
Term::Ctr { name, args } => {
|
||||
Term::Ctr { orig, name, args } => {
|
||||
let mut inp_args_str = String::new();
|
||||
let mut var_args_str = String::new();
|
||||
for arg in args {
|
||||
@ -631,8 +712,8 @@ pub fn compile_entry(entry: &Entry) -> String {
|
||||
inp_args_str.push_str(&format!(" {}", inp_arg_str));
|
||||
var_args_str.push_str(&format!(" {}", var_arg_str));
|
||||
}
|
||||
let inp_str = format!("(Ct{} {}.{})", args.len(), name, inp_args_str);
|
||||
let var_str = format!("(Ct{} {}.{})", args.len(), name, var_args_str);
|
||||
let inp_str = format!("(Ct{} {}. {}{})", args.len(), name, orig, inp_args_str);
|
||||
let var_str = format!("(Ct{} {}. {}{})", args.len(), name, orig, var_args_str);
|
||||
return (inp_str, var_str);
|
||||
}
|
||||
_ => {
|
||||
|
||||
26
src/main.rs
26
src/main.rs
@ -11,6 +11,7 @@ use hvm::parser as parser;
|
||||
const CHECKER_HVM: &str = include_str!("checker.hvm");
|
||||
|
||||
fn main() {
|
||||
println!("{}", name_to_u64("_"));
|
||||
match run_cli() {
|
||||
Ok(..) => {}
|
||||
Err(err) => {
|
||||
@ -39,8 +40,8 @@ fn run_cli() -> Result<(), String> {
|
||||
|
||||
fn kind2(path: &str, main_function: &str) -> Result<(), String> {
|
||||
// Reads definitions from file
|
||||
let file = match std::fs::read_to_string(path) {
|
||||
Ok(code) => read_file(&code),
|
||||
let kind2_code = match std::fs::read_to_string(path) {
|
||||
Ok(code) => code,
|
||||
Err(msg) => {
|
||||
println!("File not found: {}", path);
|
||||
return Ok(());
|
||||
@ -48,7 +49,7 @@ fn kind2(path: &str, main_function: &str) -> Result<(), String> {
|
||||
};
|
||||
|
||||
// Prints errors if parsing failed
|
||||
let file = match file {
|
||||
let file = match read_file(&kind2_code) {
|
||||
Ok(file) => file,
|
||||
Err(msg) => {
|
||||
println!("{}", msg);
|
||||
@ -74,7 +75,8 @@ fn kind2(path: &str, main_function: &str) -> Result<(), String> {
|
||||
let mut rt = hvm::Runtime::from_code(&checker)?;
|
||||
let main = rt.alloc_code(main_function)?;
|
||||
rt.normalize(main);
|
||||
print!("{}", readback_string(&rt, main)); // TODO: optimize by deserializing term into text directly
|
||||
print!("{}", replace_ranges_by_code(&kind2_code, &readback_string(&rt, main)));
|
||||
|
||||
|
||||
// Display stats
|
||||
println!("Rewrites: {}", rt.get_rewrites());
|
||||
@ -82,6 +84,22 @@ fn kind2(path: &str, main_function: &str) -> Result<(), String> {
|
||||
Ok(())
|
||||
}
|
||||
|
||||
fn replace_ranges_by_code(file_code: &str, checker_output: &str) -> String {
|
||||
let mut code = String::new();
|
||||
let mut cout = checker_output;
|
||||
while let (Some(init_range_index), Some(last_range_index)) = (cout.find("{{#"), cout.find("#}}")) {
|
||||
let range_text = &cout[init_range_index + 3 .. last_range_index];
|
||||
let range_text = range_text.split(":").map(|x| x.parse::<u64>().unwrap()).collect::<Vec<u64>>();
|
||||
let range_init = range_text[0] as usize;
|
||||
let range_last = range_text[1] as usize;
|
||||
code.push_str(&cout[0 .. init_range_index]);
|
||||
code.push_str(&highlight_error::highlight_error(range_init, range_last, file_code));
|
||||
cout = &cout[last_range_index + 3 ..];
|
||||
}
|
||||
code.push_str(cout);
|
||||
return code;
|
||||
}
|
||||
|
||||
// ------------------------------------------------------------
|
||||
// ------------------------------------------------------------
|
||||
// ------------------------------------------------------------
|
||||
|
||||
Loading…
Reference in New Issue
Block a user