Kind: change forall syntax, now self must be together with parenthesis

This commit is contained in:
rheidner 2021-08-19 22:14:29 -03:00
parent 54235dd465
commit 23fce8d7dd
5 changed files with 13150 additions and 13137 deletions

View File

@ -29,10 +29,10 @@ Kind.Parser.ADT.adt: Parser(Kind.Parser.ADT.Datatype)
Parser {
Kind.Parser.text("type ")
get name = Kind.Parser.name1
get pars = Parser.maybe!(Kind.Parser.binder(":"))
get pars = Parser.maybe!(Kind.Parser.binder(":", false))
get inds = Parser.maybe!(Parser {
Kind.Parser.text("~")
Kind.Parser.binder(":")
Kind.Parser.binder(":", false)
})
let pars = Maybe.default!(pars, [])
let inds = Maybe.default!(inds, [])
@ -51,10 +51,10 @@ Kind.Parser.ADT.adt: Parser(Kind.Parser.ADT.Datatype)
Kind.Parser.ADT.ctor(namespace: Kind.Name): Parser(Kind.Parser.ADT.Constructor)
Parser {
get name = Kind.Parser.name1
get args = Parser.maybe!(Kind.Parser.binder(":"))
get args = Parser.maybe!(Kind.Parser.binder(":", false))
get inds = Parser.maybe!(Parser {
Kind.Parser.text("~")
Kind.Parser.binder("=")
Kind.Parser.binder("=", false)
})
let args = Maybe.default!(args, [])
let inds = Maybe.default!(inds, [])

View File

@ -1,17 +1,22 @@
Kind.Parser.binder(sep: String): Parser(List<Kind.Binder>)
Kind.Parser.binder(sep: String, mandatory_spaces: Bool): Parser(List<Kind.Binder>)
Parser {
get lists = Parser.many1!(Parser.choice!([
Kind.Parser.binder.homo(sep, true)
Kind.Parser.binder.homo(sep, false)
Kind.Parser.binder.homo(sep, true, mandatory_spaces)
Kind.Parser.binder.homo(sep, false, mandatory_spaces)
]))
return List.flatten!(lists)
}
Kind.Parser.binder.homo(sep: String, eras: Bool): Parser(List<Kind.Binder>)
Kind.Parser.binder.homo(sep: String, eras: Bool, mandatory_spaces: Bool): Parser(List<Kind.Binder>)
Parser {
let open = if eras then "<" else "("
let clos = if eras then ">" else ")"
get bind = Kind.Parser.items1!(open, Kind.Parser.name_term(sep), clos)
let items_parser =
if mandatory_spaces then
Kind.Parser.items_now
else
Kind.Parser.items
get bind = items_parser!(open, Kind.Parser.name_term(sep), clos)
return List.mapped!(bind)!((pair) case pair {
new: Kind.Binder.new(eras, pair.fst, pair.snd)
})

View File

@ -68,7 +68,7 @@ Kind.Parser.file.def(file: String, code: String, defs: Kind.Defs): Parser(Kind.D
Kind.Parser.spaces
get from = Parser.get_idx
get name = Kind.Parser.name1
get args = Parser.many!(Kind.Parser.binder(":"))
get args = Parser.many!(Kind.Parser.binder(":", false))
let args = List.flatten!(args)
Kind.Parser.text(":")
get type = Kind.Parser.term

View File

@ -1,7 +1,7 @@
Kind.Parser.forall: Parser(Kind.Term)
Kind.Parser.block("forall", Parser {
get self = Kind.Parser.name
get bind = Kind.Parser.binder(":")
get bind = Kind.Parser.binder(":", true)
Kind.Parser.text("->")
get body = Kind.Parser.term
let term = List.fold!(bind)!(body, (x,t) case x {

File diff suppressed because it is too large Load Diff