tnelson / Forge

Forge: A Tool and Language for Teaching Formal Methods
https://forge-fm.org/
MIT License
67 stars 8 forks source link

parser: change ~literal to ~datum #201

Closed bennn closed 1 year ago

bennn commented 1 year ago

the brag parser puts symbols in head position, not identifiers, so ~literal (which compares free-identifier=?) isn't right and ~datum is better, so students can define a sig Name {} or whatever without breaking the expander

after the fix, Tim's program from the other day compiles and runs:

#lang forge

sig Name {}

pred foo {}
// before: error in PredDecl macro, expected QualName or Name identifier
// after: no error