Language syntax — Programming Language Theories

Imports

import PlTheories.FunZero.Syntax.Parsing
import PlTheories.FunZero.Syntax.Helpers

Literal defines the literals we support in our language:

inductive Literal where
| number_lit (s: Nat)
| bool_lit (b: Bool)
| string_lit (s: String)

Expr defines the basic expressions of our language:

variable

literal

tuple

lambda abstraction

function application

let binding

inductive Expr where
| var (s: String)
| literal (l: Literal)
| tuple (fst: Expr) (snd: Expr)
| abs (x: String) (body: Expr)
| app (f: Expr) (arg: Expr)
| let_ (v: String) (binding: Expr) (inExpr: Expr)

Basically Expr is a tree and for each constructor above we have a parser specification. The ones for var and literal are the following:

def var_parser : Parser Expr := .var <$> identifier

def literal_parser: Parser Expr := .literal <$> literal

The following are a little more complicated, but basically they all follow the pattern of declaring the intermediate rest values in the existential quantifier, and use each one as input to the next.

Now expression includes them all:

              mutualdef tuple_parser : Parser Expr
  | input, .tuple e1 e2, rest =>
    ∃ left_rest e1_rest comma_rest e2_rest,
      lparen input lparen_token left_rest
      ∧ expression left_rest e1 e1_rest
      ∧ comma e1_rest comma_token comma_rest
      ∧ expression comma_rest e2 e2_rest
      ∧ rparen e2_rest rparen_token rest
  | _, _, _ => False

def lambda_parser : Parser Expr
  | input, .abs x body, rest =>
    ∃ lambda_rest ident_rest arrow_rest,
      lambda_tok input lambda_token lambda_rest
      ∧ identifier lambda_rest x ident_rest
      ∧ arrow ident_rest arrow_token arrow_rest
      ∧ expression arrow_rest body rest
  | _, _, _ => False

def app_parser : Parser Expr
  | input, .app f arg, rest =>
    ∃ f_rest,
      expression input f f_rest
      ∧ expression f_rest arg rest
  | _, _, _ => False

def let_parser : Parser Expr
  | input, .let_ v binding inExpr, rest =>
    ∃ let_rest id_rest eq_rest ex_rest in_rest,
      let_tok input let_token let_rest
      ∧ identifier let_rest v id_rest
      ∧ equals id_rest equals_token eq_rest
      ∧ expression eq_rest binding ex_rest
      ∧ in_tok ex_rest in_token in_rest
      ∧ expression in_rest inExpr rest
  | _, _, _ => Falsedef expression : Parser Expr
  | input, .var s, rest => var_parser input (.var s) rest
  | input, .literal l, rest => literal_parser input (.literal l) rest
  | input, .tuple e1 e2, rest => tuple_parser input (.tuple e1 e2) rest
  | input, .abs x body, rest => lambda_parser input (.abs x body) rest
  | input, .app f arg, rest => app_parser input (.app f arg) rest
  | input, .let_ v binding inExpr, rest =>
      let_parser input (.let_ v binding inExpr) rest

end