Example syntax declarations:
syntax Exists (\(_: A) -> B) = A × B syntax bind e1 (\x -> e2) = x ← e1 ; e2
Parsing effect:
| A × B | Exists (\(_:A) -> B) |
| (x : A) × B | Exists (\(x:A) -> B) |
| {x : A} × B | Rejected |
| x ← e1 ; e2 | bind e1 (\x -> e2) |
| (x:A) ← e1 ; e2 | bind e1 (\(x:A) -> e2) |
| {x:A} ← e1 ; e2 | Rejected |
Pretty printing effect:
| Exists B | (x : _) × B x | |
| Exists (\(x:A) -> B) | (x : A) × B | |
| Exists (\(x:_) -> B) | Exists (\x -> B) | |
| Exists (\(x:A) -> B) | A × B | (x does not occur in B) |
| bind e1 (\x -> e2) | x ← e1 ; e2 | |
| bind e1 (\(x:A) -> e2) | (x:A) ← e1 ; e2 | |
| bind e1 e2 | bind e1 e2 |
TODO:
Name.hs:
- Add a representation for mixfix binders (DONE)
- Add a representation for mixfix declaration in the concrete syntax (DONE)
Parser.y:
- add a syntax declaration (DONE)
- parse "(x : T) |-> e" as an application.
- must add TypedBindings as an expression: this may cause ambiguity.
Operators.hs:
- fetch syntax decl. from the scope (DONE)
- change the parser builder (the generated tree must use fresh names!) (DONE)
Page last modified on September 12, 2010, at 10:49 am
Powered by
PmWiki