ast

AUTHOR 
Zhi Zhang
Department of Computer and Information Sciences
Kansas State University
zhangzhi@ksu.edu

Require Export ast_basics.

This file can be auto-generated from language_template.v by running languagegen in terminal

SPARK Subset Language

We use the Ada terminology to define the terms of this subset language, which makes it easy for Ada(SPARK) users to read it; Besides, we also indicate the reference chapter (for example, ,3.5.3) in Ada 2012 RM, and formalize the language in the same (not exactly) order as they are defined in Ada 2012 RM;


Expression


Inductive exp: Type :=
    | Literal: astnum -> literal -> exp
    | Name: astnum -> name -> exp
    | BinOp: astnum -> binary_operator -> exp -> exp -> exp
    | UnOp: astnum -> unary_operator -> exp -> exp

in IndexedComponent, the first astnum is the ast number for the indexed component, and the second astnum is the ast number for array represented by name; in E_SelectedComponent, the first astnum is the ast number for the record field, and second astnum is the ast number for record represented by name;
with name: Type :=
    | Identifier: astnum -> idnum -> name
    | IndexedComponent: astnum -> name -> exp -> name
    | SelectedComponent: astnum -> name -> idnum -> name .

Induction scheme for exp and name
Scheme exp_ind := Induction for exp Sort Prop with name_ind := Induction for name Sort Prop.

Statement

Inductive stmt: Type :=
    | Null: stmt
    | Assign: astnum -> name -> exp -> stmt
    | If: astnum -> exp -> stmt -> stmt -> stmt
    | While: astnum -> exp -> stmt -> stmt
    | Call: astnum -> astnum -> procnum -> list exp -> stmt
    | Seq: astnum -> stmt -> stmt -> stmt .

it's used for subtype declarations:
  • subtype declaration, e.g. subtype MyInt is Integer range 0 .. 5;
  • derived type declaration, e.g. type MyInt is new Integer range 1 .. 100;
  • integer type declaration, e.g. type MyInt is range 1 .. 10;
Inductive range: Type := Range (l: Z) (u: Z).

Type Declaration

Inductive typeDecl: Type :=
    | SubtypeDecl:
        astnum -> typenum -> type -> range -> typeDecl
    | DerivedTypeDecl:
        astnum -> typenum -> type -> range -> typeDecl
    | IntegerTypeDecl:
        astnum -> typenum -> range -> typeDecl
    | ArrayTypeDecl:
        astnum -> typenum -> type -> type -> typeDecl
    | RecordTypeDecl:
        astnum -> typenum -> list (idnum * type ) -> typeDecl .

Record objDecl: Type := mkobjDecl{
    declaration_astnum: astnum;
    object_name: idnum;
    object_nominal_subtype: type;
    initialization_exp: option (exp)
}.

Record paramSpec: Type := mkparamSpec{
    parameter_astnum: astnum;
    parameter_name: idnum;
    parameter_subtype_mark: type;
    parameter_mode: mode

}.

Declaration

Inductive decl: Type :=
    | NullDecl: decl
    | TypeDecl: astnum -> typeDecl -> decl
    | ObjDecl: astnum -> objDecl -> decl
    | ProcBodyDecl: astnum -> procBodyDecl -> decl
    | SeqDecl: astnum -> decl -> decl -> decl

Procedure

with procBodyDecl: Type :=
  mkprocBodyDecl
    (procedure_astnum: astnum)
    (procedure_name: procnum)
    (procedure_parameter_profile: list paramSpec)
    (procedure_declarative_part: decl)
    (procedure_statements: stmt).

Program

A program is composed of a sequence of (1) type declarations, (2) variable declarations (3) procedure declarations, where 'main' is the main procedure (with empty parameters) working as the entry point of the whole program

Record program : Type := mkprogram{
    decls: decl;
    main: procnum
}.

Auxiliary Functions


Section AuxiliaryFunctions.

  Definition procedure_statements pb :=
    match pb with
      | mkprocBodyDecl _ _ _ _ x => x
    end.

  Definition procedure_declarative_part pb :=
    match pb with
      | mkprocBodyDecl _ _ _ x _ => x
    end.

  Definition procedure_parameter_profile pb :=
    match pb with
      | mkprocBodyDecl _ _ x _ _ => x
    end.

  Definition procedure_name pb :=
    match pb with
      | mkprocBodyDecl _ x _ _ _ => x
    end.

  Definition type_name td :=
    match td with
    | SubtypeDecl _ tn _ _ => tn
    | DerivedTypeDecl _ tn _ _ => tn
    | IntegerTypeDecl _ tn _ => tn
    | ArrayTypeDecl _ tn _ _ => tn
    | RecordTypeDecl _ tn _ => tn
    end.

  Definition subtype_range (t: typeDecl): option range :=
    match t with
    | SubtypeDecl ast_num tn t r => Some r
    | DerivedTypeDecl ast_num tn t r => Some r
    | IntegerTypeDecl ast_num tn r => Some r
    | _ => None
    end.

  Definition expression_astnum e :=
    match e with
    | Literal ast_num l => ast_num
    | Name ast_num n => ast_num
    | BinOp ast_num bop e1 e2 => ast_num
    | UnOp ast_num uop e => ast_num
    end.

  Definition name_astnum n :=
    match n with
    | Identifier ast_num x => ast_num
    | IndexedComponent ast_num x e => ast_num
    | SelectedComponent ast_num x f => ast_num
    end.

End AuxiliaryFunctions.