HigherOrderCO/Kind
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind.git synced 2024-10-05 19:27:30 +03:00
Code Issues Packages Projects Releases Wiki Activity

i dont remember

Browse Source
This commit is contained in:
Victor Taelin 2024-02-20 01:11:21 -03:00
parent 2033189215
commit 8b16d0751f
3 changed files with 24 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
book/Kind.kind2
View File

@ -881,16 +881,19 @@ Kind.Term.parser.lam
(Kind.Term.parser.pure λscp
(Kind.lam nam λx(bod (Kind.Scope.extend nam x scp))))))))
// (f x)
// (f x y z ...)
Kind.Term.parser.app
: (Parser.Guard Kind.PreTerm)
= (Parser.Guard.text Kind.PreTerm "("
(Kind.Term.parser.bind Unit (Parser.text "(") λ_
(Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λfun
(Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λarg
(Kind.Term.parser.bind Unit (Parser.text ")") λ_
(Kind.Term.parser.pure λscp
(Kind.app (fun scp) (arg scp))))))))
(Kind.Term.parser.bind Unit (Parser.text "(") λ_
(Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λfun
(Kind.Term.parser.bind (List Kind.PreTerm) (Parser.until Kind.PreTerm (Parser.skip Bool (Parser.test ")")) Kind.Term.parser) λterms
(Kind.Term.parser.bind Unit (Parser.text ")") λ_
(Kind.Term.parser.pure λscp
(((List.fold Kind.PreTerm terms) ∀(fun:Kind.Term)Kind.Term
λargλrecλfun(rec (Kind.app fun (arg scp)))
λfun(fun))
(fun scp))))))))
// {x: T}
Kind.Term.parser.ann
@ -1071,7 +1074,7 @@ Kind.Book.parser
// Otherwise, parse a definition
let false =
(Parser.bind String Kind.Book Parser.name λnam
(Parser.bind Bool Kind.Book (Parser.test ":") λann
(Parser.bind Bool Kind.Book (Parser.skip Bool (Parser.test ":")) λann
let P = λx(Parser Kind.Book)
// If annotated, parses the annotation
let true =

32
book/Main.kind2
View File

@ -1,26 +1,16 @@
//Main = Kind.reduce.mat
//BOOK
//: String
//= "id = λx x
//Bool : * = $self ∀(P: ∀(x: Bool) *) ∀(t: (P Bool.true)) ∀(f: (P Bool.false)) (P self)
//Bool.true : Bool = ~λP λt λf t
//Bool.false : Bool = ~λP λt λf f
//"
BOOK
: String
= "id = λx x
//Main
//: String
//= (Kind.Book.show (Kind.Book.parse BOOK))
Bool
: *
= $self
∀(P: ∀(x: Bool) *)
∀(t: (P Bool.true))
∀(f: (P Bool.false))
(P self)
Bool.true : Bool = ~λP λt λf t
Bool.false : Bool = ~λP λt λf f
Foo = #12345
"
Main
: String
= (Kind.Book.show (Kind.Book.parse BOOK))
//Main = Kind.Term.parser.app
//Main
//: String

4
book/Parser.kind2
View File

@ -66,7 +66,7 @@ Parser.Guard.text
∀(then: (Parser A))
(Parser.Guard A)
= λA λtext λthen
(Parser.Guard.new A (Parser.test text) then)
(Parser.Guard.new A (Parser.skip Bool (Parser.test text)) then)
Parser.pure
: ∀(A: *)
@ -189,7 +189,7 @@ Parser.test
let nil = (Parser.Result.done Bool String.nil Bool.false)
(~code P cons nil)
let nil = λcode (Parser.Result.done Bool code Bool.true)
(~test P cons nil (String.skip code))
(~test P cons nil code)
// Parses an exact text.
// - If successful, consumes text.