Problemas de nomenclatura em bigStepSemantics, smallStepSemantics e testBigStep

[GabrielPiresF]

Definição de não-terminais

Não é possível definir não-terminais com as letras Z, O, F porque a gramática BigStep contém a produção [re Z O F]

(judgment-holds (eval (F (/ ε ε) (H (• F 1) (V (• ε 3) ∅))) ((• 1 ε) (4)) s) s)
. . eval: judgment input values do not match its contract;
(unknown output values indicated by _)
contract: (eval G E s)
values: (eval (F (/ ε ε) (H (• F 1) (V (• ε 3) ∅))) ((• 1 ε) (4)) _)
(judgment-holds (eval (A (/ ε ε) (H (• A 1) (V (• ε 3) ∅))) ((• 1 ε) (4)) s) s)
'(⊥)

---

Ambiguidade da metafunção ⊕

Ambas bigStepSemantics e smallStepSemantics, importadas em testBigStep, contém uma metafunção ⊕

Em bigStepSemantics:

(define-metafunction PegRelation
⊕ : t t -> t
[(⊕ (boolean_1 hs_1) (boolean_2 hs_2))
(,(or (term boolean_1) (term boolean_2))
(∪ hs_1 hs_2))])

Em smallStepSemantics:

(define-metafunction Reduct
[(⊕ natural_1 natural_2) ,(+ (term natural_1) (term natural_2))]
)

O que resulta no erro:

testBigStep.rkt:9:9: module: identifier already required
at: ⊕
in: "../smallStepSemantics.rkt"
also provided by: "../bigStepSemantics.rkt"
#(156 27)