Mix Fix Binders

Example syntax declarations:

 syntax Exists (\(_: A) -> B) = A  B
 syntax bind e1 (\x -> e2) = x ← e1 ; e2

Parsing effect:

A BExists (\(_:A) -> B)
(x : A) BExists (\(x:A) -> B)
{x : A} BRejected
x ← e1 ; e2bind e1 (\x -> e2)
(x:A) ← e1 ; e2bind e1 (\(x:A) -> e2)
{x:A} ← e1 ; e2Rejected

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 e2bind 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)