Overview  Index  Help 

CoreAst


The First-Order LoopW Type Inference core abstract syntax. The core abstract syntax is used to represent input LoopW programs.

Opened structures

Error

         
Type summary

type block = sequence * (ident list * typedIdent list)
          blocks.

type expType = ProofAst.formula
          formulas as in proof abstract syntax.

type ident = ProofAst.ident
          identifiers as in proof abstract syntax.

type program = sequence
          programs.

type term = ProofAst.term
          terms as in proof abstract syntax.

type typedIdent = ident * expType
          typed identifiers.

 
Datatype summary

datatype command =
         Block of block
       | For of ident * expression * block
       | Affect of ident * expression
       | Inc of ident
       | Dec of ident
       | ProcCall of expression * expression list * ident list
       | Label of ident * block
       | Jump of expression * expression list * typedIdent list
       | CommRegion of command * region

          commands.

datatype expression =
         Id of ident
       | Val of value
       | Cast of expression * expType
       | ExpRegion of expression * region

          expressions.

datatype sequence =
         Empty
       | Comm of command * sequence
       | Cst of ident * expression * sequence
       | Var of ident * expression * sequence
       | SeqRegion of sequence * region

          sequences.

datatype value =
         Star
       | Int of int
       | Proc of
         ident list * typedIdent list * ident list * typedIdent list * block
       | ValRegion of value * region

          values.

 
DataConstructor summary

constructor Affect : ident * expression -> command
          assignment: x := e.

constructor Block : block -> command
          block: { s }{i}x:tau

constructor Cast : expression * expType -> expression
          cast to a given type: e :> tau.

constructor Comm : command * sequence -> sequence
          composed command: c; s.

constructor CommRegion : command * region -> command
          region used for error display.

constructor Cst : ident * expression * sequence -> sequence
          constant declaration: cst x = e; s.

constructor Dec : ident -> command
          decrementation: dec(x).

constructor Empty : sequence
          empty sequence.

constructor ExpRegion : expression * region -> expression
          region used for error display.

constructor For : ident * expression * block -> command
          for-loop: for I := e { s }{j}x:tau.

constructor Id : ident -> expression
          identifier.

constructor Inc : ident -> command
          incrementation: inc(x).

constructor Int : int -> value
          natural number: n.

constructor Jump : expression * expression list * typedIdent list -> command
          jump to a label: jump(k,el)x:tau.

constructor Label : ident * block -> command
          label definition: k:{ s }{j}x:tau.

constructor Proc
            : ident list *
              typedIdent list *
              ident list *
              typedIdent list *
              block ->
                value

          anonymous procedure declaration: proc({il} in xfl; {jl} out yfl){ s }{jl}yfl.

constructor ProcCall : expression * expression list * ident list -> command
          procedure call: p(el, il).

constructor SeqRegion : sequence * region -> sequence
          region used for error display.

constructor Star : value
          null value: *.

constructor Val : value -> expression
          value.

constructor ValRegion : value * region -> value
          region used for error display.

constructor Var : ident * expression * sequence -> sequence
          variable declaration: var x := e; s.

   

 
Type detail

ident

type ident = ProofAst.ident

identifiers as in proof abstract syntax.


term

type term = ProofAst.term

terms as in proof abstract syntax.


expType

type expType = ProofAst.formula

formulas as in proof abstract syntax.


typedIdent

type typedIdent = ident * expType

typed identifiers.


block

type block = sequence * (ident list * typedIdent list)

blocks.


program

type program = sequence

programs.

 
Datatype detail

command

datatype command =
         Block of block
       | For of ident * expression * block
       | Affect of ident * expression
       | Inc of ident
       | Dec of ident
       | ProcCall of expression * expression list * ident list
       | Label of ident * block
       | Jump of expression * expression list * typedIdent list
       | CommRegion of command * region

commands.


sequence

datatype sequence =
         Empty
       | Comm of command * sequence
       | Cst of ident * expression * sequence
       | Var of ident * expression * sequence
       | SeqRegion of sequence * region

sequences.


expression

datatype expression =
         Id of ident
       | Val of value
       | Cast of expression * expType
       | ExpRegion of expression * region

expressions.


value

datatype value =
         Star
       | Int of int
       | Proc of
         ident list * typedIdent list * ident list * typedIdent list * block
       | ValRegion of value * region

values.

 
DataConstructor detail

Block

constructor Block : block -> command

block: { s }{i}x:tau


For

constructor For : ident * expression * block -> command

for-loop: for I := e { s }{j}x:tau.


Affect

constructor Affect : ident * expression -> command

assignment: x := e.


Inc

constructor Inc : ident -> command

incrementation: inc(x).


Dec

constructor Dec : ident -> command

decrementation: dec(x).


ProcCall

constructor ProcCall : expression * expression list * ident list -> command

procedure call: p(el, il).


Label

constructor Label : ident * block -> command

label definition: k:{ s }{j}x:tau.


Jump

constructor Jump : expression * expression list * typedIdent list -> command

jump to a label: jump(k,el)x:tau.


CommRegion

constructor CommRegion : command * region -> command

region used for error display.


Empty

constructor Empty : sequence

empty sequence.


Comm

constructor Comm : command * sequence -> sequence

composed command: c; s.


Cst

constructor Cst : ident * expression * sequence -> sequence

constant declaration: cst x = e; s.


Var

constructor Var : ident * expression * sequence -> sequence

variable declaration: var x := e; s.


SeqRegion

constructor SeqRegion : sequence * region -> sequence

region used for error display.


Id

constructor Id : ident -> expression

identifier.


Val

constructor Val : value -> expression

value.


Cast

constructor Cast : expression * expType -> expression

cast to a given type: e :> tau.


ExpRegion

constructor ExpRegion : expression * region -> expression

region used for error display.


Star

constructor Star : value

null value: *.


Int

constructor Int : int -> value

natural number: n.


Proc

constructor Proc
            : ident list *
              typedIdent list *
              ident list *
              typedIdent list *
              block ->
                value

anonymous procedure declaration: proc({il} in xfl; {jl} out yfl){ s }{jl}yfl.


ValRegion

constructor ValRegion : value * region -> value

region used for error display.

   


Overview  Index  Help