From cc8e1095719ae6205ecbe726702d1ab6e6ecd450 Mon Sep 17 00:00:00 2001 From: Victor Taelin Date: Mon, 19 Feb 2024 12:37:51 -0300 Subject: [PATCH] skip comments --- book/Char.is_whitespace.kind2 | 7 ---- book/Kind.kind2 | 76 ++++++++++++++++++++++++++++++++++- book/Main.kind2 | 14 +++++-- book/Parser.kind2 | 3 +- book/String.skip.kind2 | 46 +++++++++++++++++---- 5 files changed, 127 insertions(+), 19 deletions(-) delete mode 100644 book/Char.is_whitespace.kind2 diff --git a/book/Char.is_whitespace.kind2 b/book/Char.is_whitespace.kind2 deleted file mode 100644 index f9b3bfa3..00000000 --- a/book/Char.is_whitespace.kind2 +++ /dev/null @@ -1,7 +0,0 @@ -Char.is_whitespace -: ∀(a: Char) - Bool -= λa (Bool.or - (Char.equal a #10) // newline - (Char.equal a #32)) // space - diff --git a/book/Kind.kind2 b/book/Kind.kind2 index 61528dd4..997b4c1f 100644 --- a/book/Kind.kind2 +++ b/book/Kind.kind2 @@ -732,7 +732,8 @@ Kind.show : ∀(term: Kind.Term) ∀(dep: Nat) String -= λterm λdep (String.Concatenator.build (Kind.show.go term dep)) += λterm λdep + (String.Concatenator.build (Kind.show.go term dep)) Kind.Oper.show.go : ∀(oper: Kind.Oper) @@ -1378,6 +1379,79 @@ Kind.report let false = λinferred λexpected λvalue λdep none // TODO: HVM.log error (~e P true false inferred expected value dep) +// Compilers +// --------- + +Kind.compile.hvm.go +: ∀(term: Kind.Term) + ∀(dep: Nat) + String.Concatenator += λterm λdep + let P = λx String.Concatenator + let all = λnam λinp λbod + (Kind.Text.show.go "0") + let lam = λnam λbod λnil + ((Kind.Text.show.go "λ") + ((Kind.Text.show.go (U60.name (U60.from_nat dep))) + ((Kind.Text.show.go " " + ((Kind.compile.hvm.go (bod (Kind.var nam dep)) (Nat.succ dep)) + nil))))) + let app = λfun λarg λnil + ((Kind.Text.show.go "(") + ((Kind.compile.hvm.go fun dep) + ((Kind.Text.show.go " ") + ((Kind.compile.hvm.go arg dep) + ((Kind.Text.show.go ")") + nil))))) + let ann = λval λtyp + (Kind.compile.hvm.go val dep) + let slf = λnam λbod + (Kind.Text.show.go "0") + let ins = λval + (Kind.compile.hvm.go val dep) + let ref = λnam λval + (Kind.Text.show.go nam) + let def = λnam λval λbod λnil + ((Kind.Text.show.go "let ") + ((Kind.Text.show.go nam) + ((Kind.Text.show.go " = ") + ((Kind.compile.hvm.go val dep) + ((Kind.Text.show.go "; ") + ((Kind.compile.hvm.go (bod (Kind.var nam dep)) (Nat.succ dep)) + nil)))))) + let set = + (Kind.Text.show.go "*") + let u60 = + (Kind.Text.show.go "*") + let num = λval + (U60.show.go val) + let op2 = λopr λfst λsnd λnil + ((Kind.Text.show.go "(") + ((Kind.Oper.show.go opr) + ((Kind.Text.show.go " ") + ((Kind.compile.hvm.go fst dep) + ((Kind.Text.show.go " ") + ((Kind.compile.hvm.go snd dep) + ((Kind.Text.show.go ")") + nil))))))) + let txt = λtxt λnil + ((Kind.Text.show.go String.quote) + ((Kind.Text.show.go txt) + ((Kind.Text.show.go String.quote) + nil))) + let hol = λnam λctx + (Kind.Text.show.go "0") + let var = λnam λidx + (Kind.Text.show.go (U60.name (U60.from_nat idx))) + (~term P all lam app ann slf ins ref def set u60 num op2 txt hol var) + +Kind.compile.hvm +: ∀(term: Kind.Term) + ∀(dep: Nat) + String += λterm λdep + (String.Concatenator.build (Kind.compile.hvm.go term dep)) + // Tests // ----- diff --git a/book/Main.kind2 b/book/Main.kind2 index af3e3915..c1dc6445 100644 --- a/book/Main.kind2 +++ b/book/Main.kind2 @@ -2,10 +2,18 @@ //Main = Parser.skip +Main = (String.skip "//oimeugrandeamigo... tudo bem? +eu to, e vc? +foo +") + //Main = Parser.text -Main -: String -= (Kind.show (Kind.Term.parser.run "λx λy (y x)") Nat.zero) +//Main +//: String +//= let term = (Kind.Term.parser.run " + //λf λx (f (f x)) + //") + //(Kind.compile.hvm term Nat.zero) diff --git a/book/Parser.kind2 b/book/Parser.kind2 index ae6a4691..290ff900 100644 --- a/book/Parser.kind2 +++ b/book/Parser.kind2 @@ -111,7 +111,8 @@ Parser.skip : ∀(A: *) ∀(parser: (Parser A)) (Parser A) -= λA λparser λcode (parser (String.skip code)) += λA λparser λcode + (parser (String.skip code)) // Takes characters while a condition is true. Parser.pick_while diff --git a/book/String.skip.kind2 b/book/String.skip.kind2 index d633d77b..7d364fab 100644 --- a/book/String.skip.kind2 +++ b/book/String.skip.kind2 @@ -1,14 +1,46 @@ -// TODO: implement comment skipper +// Skips space characters and comments String.skip : ∀(str: String) String = λstr + // Pattern-matches str let P = λx(String) - let cons = λhead λtail - let skip = (Char.is_whitespace head) - let P = λx ∀(head: Char) ∀(tail: String) (String) - let true = λhead λtail (String.skip tail) - let false = λhead λtail (String.cons head tail) - (~skip P true false head tail) + let cons = λc0 λcs + // If first char is space, skip it + let P = λx ∀(c0: Char) ∀(cs: String) (String) + let true = λc0 λcs (String.skip cs) + let false = λc0 λcs + // If first char is slash, check next char + let P = λx ∀(c0: Char) ∀(cs: String) (String) + let true = λc0 λcs + // Pattern-matches str's tail + let P = λx ∀(c0: Char) (String) + let cons = λc1 λcs λc0 + // If second char is slash, skip comment + let P = λx ∀(c0: Char) ∀(c1: Char) ∀(cs: String) (String) + let true = λc0 λc1 λcs (String.skip.comment cs) + let false = λc0 λc1 λcs (String.cons c0 (String.cons c1 cs)) + (~(Char.is_slash c1) P true false c0 c1 cs) + let nil = λc0 (String.cons c0 String.nil) + (~cs P cons nil c0) + let false = λc0 λcs (String.cons c0 cs) + (~(Char.is_slash c0) P true false c0 cs) + (~(Char.is_blank c0) P true false c0 cs) + let nil = String.nil + (~str P cons nil) + +// Skips all characters until Char.is_newline is true +String.skip.comment +: ∀(str: String) + String += λstr + // Pattern-matches str + let P = λx(String) + let cons = λc0 λcs + // If first char is not a newline, skip and recurse + let P = λx ∀(c0: Char) ∀(cs: String) (String) + let true = λc0 λcs cs + let false = λc0 λcs (String.skip.comment cs) + (~(Char.is_newline c0) P true false c0 cs) let nil = String.nil (~str P cons nil)