mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-09-11 07:15:45 +03:00
ignore spaces before words
This commit is contained in:
parent
a3c73894fd
commit
32b13b2b8f
@ -642,47 +642,21 @@ Lit.Core.World.run.terms(
|
||||
Lit.Core: _
|
||||
let world = {}
|
||||
let code =
|
||||
Lit.Lang.Type
|
||||
| Lit.Lang.Cmp
|
||||
| Lit.Lang.Nat
|
||||
| Lit.Lang.Bits
|
||||
| Lit.Lang.BitsMap
|
||||
|
|
||||
`
|
||||
type BoolList {
|
||||
nil
|
||||
cons{
|
||||
head: Bool
|
||||
tail: NatList
|
||||
}
|
||||
}
|
||||
`
|
||||
type Unit {
|
||||
new
|
||||
}
|
||||
|
||||
type NatList {
|
||||
nil
|
||||
cons{
|
||||
head: Nat
|
||||
tail: BoolList
|
||||
}
|
||||
}
|
||||
|
||||
Count.inc, MrDog @ Count(): Bits
|
||||
Bits/o{pred: Bits/e}
|
||||
|
||||
Count.inc(): Unit
|
||||
call c = Count();
|
||||
call d = Bits.inc(c);
|
||||
bind Count = d;
|
||||
Unit/new
|
||||
|
||||
do {
|
||||
call ret = Bits.add(Bits/i{pred:Bits/i{pred: Bits/e}}, Bits/i{pred: Bits/e})
|
||||
call dupped = Bits.dup(ret)
|
||||
Unit/new
|
||||
}: Unit
|
||||
|
||||
`
|
||||
FirstTest(): Unit
|
||||
Unit/new
|
||||
|
||||
SecondTest(): U64
|
||||
2
|
||||
`
|
||||
let page = Parser.run!(Lit.Lang.parser.page(world), code) abort IO.print("parse error")
|
||||
log("parsed:")
|
||||
log(Lit.Lang.show.page(page, world))
|
||||
|
||||
case Lit.Core.World.run.page(page, world) as result {
|
||||
none:
|
||||
IO.print("failure")
|
||||
|
@ -315,14 +315,15 @@ Lit.Lang.parser.term(world: Lit.Core.World): Parser<Lit.Core.Term>
|
||||
Lit.Lang.parser.term.match(world)
|
||||
Lit.Lang.parser.term.bind(world)
|
||||
Lit.Lang.parser.term.call(world)
|
||||
Lit.Lang.parser.term.word
|
||||
Lit.Lang.parser.term.var(world)
|
||||
Lit.Lang.parser.term.compare(world)
|
||||
Lit.Lang.parser.term.word
|
||||
Lit.Lang.parser.term.operate(world)
|
||||
])
|
||||
|
||||
Lit.Lang.parser.term.word: Parser<Lit.Core.Term>
|
||||
Parser {
|
||||
Lit.Lang.parser.ignore
|
||||
get num = Parser.nat
|
||||
if num >? 18446744073709551615 then
|
||||
Parser.fail!("Number out of bound")
|
||||
@ -537,6 +538,10 @@ Lit.Lang.parser.ignore: Parser(List<Unit>)
|
||||
}
|
||||
]))
|
||||
|
||||
// TODO solve ambiguity with numbers by putting
|
||||
// the word parser before the nat parser.
|
||||
// right now this seems to be looping the parser
|
||||
// I don't know why
|
||||
Lit.Lang.parser.name: Parser<String>
|
||||
Parser {
|
||||
Lit.Lang.parser.ignore
|
||||
|
Loading…
Reference in New Issue
Block a user