Library langs.L2.syntax

Require Export ZArith scopes.

L2 Syntax

Corresponds to paper Fig. 16 (with some extensions).
Types
Inductive T :=
| Tint : T
| Tbool: T
n-ary function type, where n is given by the length of list T
For dereferencing a variable (lhs)
n-ary functions
n-ary application
parallel let (bodies of binders can't refer to each other)
sequential let (bodies of binders can refer to previous bindings)
recursive let (bodies of binders can refer to all other bindings, including the one being currently bound)
Assign a value to a variable (lhs)
For creating a record value whose structure is described by the declaration that R refers to
| New : R pre_exp

with lhs :=
| Var : R lhs
| Field : exp R lhs

with binder :=
| Binder : D exp binder

with exp :=
| E : ScopeId T pre_exp exp.

Definition expScope (e : exp) : ScopeId :=
  match e with
  | E s _ _s
  end.

Definition expType (e : exp) : T :=
  match e with
  | E _ t _t
  end.

Record type field declarations consist of a Declaration, Type pair
Inductive fld_decl :=
| Flddecl : D T fld_decl.

Definition fldDecl (f: fld_decl) :=
  match f with
  | Flddecl d _d
  end.

Definition fldType (f: fld_decl) :=
  match f with
  | Flddecl _ tt
  end.

Record definitions: a Declaration that uniquely identifies the record, and a list of record type field declarations
Inductive decl :=
| Rdef : D list fld_decl decl.

A program consists of a list of record type declarations and an expression to be evaluated
Inductive prog :=
| Prog : list decl exp prog.

Auxiliary definitions

Distinguishing value expressions. Used for type-checking LetRecs, to avoid black hole semantics of self-referential let-bindings.
Definition is_val e :=
  match e with
  | E _ _ e'
    match e' with
    | CNum _True
    | CTrueTrue
    | CFalseTrue
    | Fn _ _True
    | _False
    end
  end.

Some helpers for working with binders.
Definition split_b (b: binder) :=
  match b with
  | Binder d e(d, e)
  end.

Fixpoint unzip {C T1 T2} {split: C (T1 × T2)} (l: list C) : (list T1 × list T2) :=
  match l with
  | c :: cs
    let (t1,t2) := split c in
    let t1t2s := @unzip C T1 T2 split cs in
    (t1 :: (fst t1t2s), t2 :: (snd t1t2s))
  | []([], [])
  end.

Unzips a sequence of binders into a list of declarations and a list of expressions
Definition unzipb := @unzip binder D exp split_b.