小编Yar*_*nov的帖子

我有一个编写简单解析器生成器的任务,所以我编写了类似ANTLR的语法并试图解析像"foo:bar;"这样的简单文件,但得到了以下输出:

[@0,0:2='foo',<1>,1:0]
[@1,3:3=':',<16>,1:3]
[@2,4:6='bar',<1>,1:4]
[@3,7:7=';',<18>,1:7]
[@4,8:7='<EOF>',<-1>,1:8]
line 1:0 no viable alternative at input 'foo'
(rule foo : bar ;)

我的语法看起来像

grammar parsGen;

gram : rule SEMICOLON (NEWLINE+ rule SEMICOLON)* ;

rule : lRule | pRule ;

lRule : LRULEID COLON lRule1 ;
lRule1 : (((LRULEID | STRING | SET) | LBRACE lRule1 PIPE lRule1 RBRACE) modificator? SPACE+)+ ;

pRule : PRULEID COLON pRule1 ;
pRule1 : (((LRULEID | PRULEID) | LBRACE lRule1 PIPE lRule1 RBRACE) modificator? SPACE+)+ ;

modificator : …

我正在通过教程学习Agda,现在我正在阅读依赖对.

所以,这是代码片段:

data ? (A : Set) (B : A ? Set) : Set where
  _,_ : (a : A) ? (b : B a) ? ? A B

infixr 4 _,_

?proj? : {A : Set}{B : A ? Set} ? ? A B ? A
?proj? (a , b) = a

data _?_ {A : Set}(x : A) : List A ? Set where
  first : {xs : List A} ? x ? x …