Theory Annotate

(*  Title:       CoreC++
    Author:      Tobias Nipkow, Daniel Wasserrab
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>
*)

section ‹Program annotation›

theory Annotate imports WellType begin


abbreviation (output)
  unanFAcc :: "expr ⇒ vname ⇒ expr" (‹(_∙_)› [10,10] 90) where
  "unanFAcc e F == FAcc e F []"

abbreviation (output)
  unanFAss :: "expr ⇒ vname ⇒ expr ⇒ expr" (‹(_∙_ := _)› [10,0,90] 90) where
  "unanFAss e F e' == FAss e F [] e'"


inductive
  Anno :: "[prog,env, expr     , expr] ⇒ bool"
         (‹_,_ ⊢ _ ↝ _›   [51,0,0,51]50)
  and Annos :: "[prog,env, expr list, expr list] ⇒ bool"
         (‹_,_ ⊢ _ [↝] _› [51,0,0,51]50)
  for P :: prog
where
  
  AnnoNew: "is_class P C  ⟹  P,E ⊢ new C ↝ new C"
| AnnoCast: "P,E ⊢ e ↝ e' ⟹ P,E ⊢ Cast C e ↝ Cast C e'"
| AnnoStatCast: "P,E ⊢ e ↝ e' ⟹ P,E ⊢ StatCast C e ↝ StatCast C e'"
| AnnoVal: "P,E ⊢ Val v ↝ Val v"
| AnnoVarVar: "E V = ⌊T⌋ ⟹ P,E ⊢ Var V ↝ Var V"
| AnnoVarField: "⟦ E V = None; E this = ⌊Class C⌋; P ⊢ C has least V:T via Cs ⟧
               ⟹ P,E ⊢ Var V ↝ Var this∙V{Cs}"
| AnnoBinOp:
  "⟦ P,E ⊢ e1 ↝ e1';  P,E ⊢ e2 ↝ e2' ⟧
   ⟹ P,E ⊢ e1 «bop» e2 ↝ e1' «bop» e2'"
| AnnoLAss:
  "P,E ⊢ e ↝ e' ⟹ P,E ⊢ V:=e ↝ V:=e'"
| AnnoFAcc:
  "⟦ P,E ⊢ e ↝ e';  P,E ⊢ e' :: Class C;  P ⊢ C has least F:T via Cs ⟧
   ⟹ P,E ⊢ e∙F{[]} ↝ e'∙F{Cs}"
| AnnoFAss: "⟦ P,E ⊢ e1 ↝ e1';  P,E ⊢ e2 ↝ e2';
             P,E ⊢ e1' :: Class C; P ⊢ C has least F:T via Cs ⟧
          ⟹ P,E ⊢ e1∙F{[]} := e2 ↝ e1'∙F{Cs} := e2'"
| AnnoCall:
  "⟦ P,E ⊢ e ↝ e';  P,E ⊢ es [↝] es' ⟧
   ⟹ P,E ⊢ Call e Copt M es ↝ Call e' Copt M es'"
| AnnoBlock:
  "P,E(V ↦ T) ⊢ e ↝ e'  ⟹  P,E ⊢ {V:T; e} ↝ {V:T; e'}"
| AnnoComp: "⟦ P,E ⊢ e1 ↝ e1';  P,E ⊢ e2 ↝ e2' ⟧
           ⟹  P,E ⊢ e1;;e2 ↝ e1';;e2'"
| AnnoCond: "⟦ P,E ⊢ e ↝ e'; P,E ⊢ e1 ↝ e1';  P,E ⊢ e2 ↝ e2' ⟧
          ⟹ P,E ⊢ if (e) e1 else e2 ↝ if (e') e1' else e2'"
| AnnoLoop: "⟦ P,E ⊢ e ↝ e';  P,E ⊢ c ↝ c' ⟧
          ⟹ P,E ⊢ while (e) c ↝ while (e') c'"
| AnnoThrow: "P,E ⊢ e ↝ e'  ⟹  P,E ⊢ throw e ↝ throw e'"

| AnnoNil: "P,E ⊢ [] [↝] []"
| AnnoCons: "⟦ P,E ⊢ e ↝ e';  P,E ⊢ es [↝] es' ⟧
           ⟹  P,E ⊢ e#es [↝] e'#es'"

end