(*  Title:      JinjaDCI/J/Annotate.thy

    Author:     Tobias Nipkow, Susannah Mansky
    Copyright   2003 Technische Universitaet Muenchen, 2019-20 UIUC

    Based on the Jinja theory J/Annotate.thy by Tobias Nipkow
*)

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 :: "[J_prog,env, expr , expr] → bool"
         (‹_,_ ⊨ _ ↝ _›   [51,0,0,51]50)
  and Annos :: "[J_prog,env, expr list, expr list] → bool"
         (‹_,_ ⊨ _ [↝] _› [51,0,0,51]50)
  for P :: J_prog
where
  
  AnnoNew: "P,E ⊨ new C ↝ new C"
| AnnoCast: "P,E ⊨ e ↝ e' ==> P,E ⊨ Cast C e ↝ Cast 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 sees V,NonStatic:T in D ]
               ==> P,E ⊨ Var V ↝ Var this∙V{D}"
| AnnoBinOp:
  "[ P,E ⊨ e1 ↝ e1'; P,E ⊨ e2 ↝ e2' ]
   ==> P,E ⊨ e1 «bop¬ e2 ↝ e1' «bop¬ e2'"
| AnnoLAssVar:
  "[ E V = ⌊T⌋; P,E ⊨ e ↝ e' ] ==> P,E ⊨ V:=e ↝ V:=e'"
| AnnoLAssField:
  "[ E V = None; E this = ⌊Class C⌋; P ⊨ C sees V,NonStatic:T in D; P,E ⊨ e ↝ e' ]
   ==> P,E ⊨ V:=e ↝ Var this∙V{D} := e'"
| AnnoFAcc:
  "[ P,E ⊨ e ↝ e'; P,E ⊨ e' :: Class C; P ⊨ C sees F,NonStatic:T in D ]
   ==> P,E ⊨ e∙F{[]} ↝ e'∙F{D}"
| AnnoSFAcc:
  "[ P ⊨ C sees F,Static:T in D ]
   ==> P,E ⊨ C∙_sF{[]} ↝ C∙_sF{D}"
| AnnoFAss: "[ P,E ⊨ e1 ↝ e1'; P,E ⊨ e2 ↝ e2';
             P,E ⊨ e1' :: Class C; P ⊨ C sees F,NonStatic:T in D ]
          ==> P,E ⊨ e1∙F{[]} := e2 ↝ e1'∙F{D} := e2'"
| AnnoSFAss: "[ P,E ⊨ e2 ↝ e2'; P ⊨ C sees F,Static:T in D ]
          ==> P,E ⊨ C∙_sF{[]} := e2 ↝ C∙_sF{D} := e2'"
| AnnoCall:
  "[ P,E ⊨ e ↝ e'; P,E ⊨ es [↝] es' ]
   ==> P,E ⊨ Call e M es ↝ Call e' M es'"
| AnnoSCall:
  "[ P,E ⊨ es [↝] es' ]
   ==> P,E ⊨ SCall C M es ↝ SCall C 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'"
| AnnoTry: "[ P,E ⊨ e1 ↝ e1'; P,E(V ↦ Class C) ⊨ e2 ↝ e2' ]
         ==> P,E ⊨ try e1 catch(C V) e2 ↝ try e1' catch(C V) e2'"

| AnnoNil: "P,E ⊨ [] [↝] []"
| AnnoCons: "[ P,E ⊨ e ↝ e'; P,E ⊨ es [↝] es' ]
           ==> P,E ⊨ e#es [↝] e'#es'"

end