Library langs.L3.syntax

Require Export ZArith scopes.

L3 Syntax

Corresponds to paper Fig. 23 (with some extensions).
Types
Initializer expressions are references, referring to the declaration to be initialized with the value given by evaluating exp.
with initializer :=
| Initializer : R exp initializer

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.

Definition initRef (i : initializer) :=
  match i with
  | Initializer r _r
  end.
Definition initExp (i : initializer) :=
  match i with
  | Initializer _ ee
  end.

Class type fields are compactly represented as an optional Declaration, Type pair, and an initializer.
Fields that have some (D × T) pair represent field declarations, whereas fields that do not have such a pair represent an initializer for fields in a parent class.
Inductive fld_decl :=
| FldDecl : option (D × T) initializer fld_decl.

Definition fldDT (f: fld_decl) :=
  match f with
  | FldDecl optdt _optdt
  end.

Definition fldI (f: fld_decl) :=
  match f with
  | FldDecl _ ii
  end.

Class definitions: a Declaration that uniquely identifies the class, an optional Reference to a parent class, and a list of class type field declarations
A program consists of a list of class 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 and initializers
Definition split_b (b: binder) :=
  match b with
  | Binder d e(d, e)
  end.
Definition split_i (i: initializer) :=
  match i with
  | Initializer r e(r, e)
  end.
Definition split_f (f: fld_decl) :=
  match f with
  | FldDecl _ isplit_i i
  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.

Unzipping sequences of binders, initializers, and field declarations.
Definition unzipb := @unzip binder D exp split_b.
Definition unzipi := @unzip initializer R exp split_i.
Definition unzipf := @unzip fld_decl R exp split_f.