src/HOL/Hoare_Parallel/RG_Syntax.thy
changeset 32621 a073cb249a06
parent 31723 f5cafe803b55
child 34940 3e80eab831a1
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy	Mon Sep 21 10:58:25 2009 +0200
     1.3 @@ -0,0 +1,95 @@
     1.4 +header {* \section{Concrete Syntax} *}
     1.5 +
     1.6 +theory RG_Syntax
     1.7 +imports RG_Hoare Quote_Antiquote
     1.8 +begin
     1.9 +
    1.10 +syntax
    1.11 +  "_Assign"    :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com"                     ("(\<acute>_ :=/ _)" [70, 65] 61)
    1.12 +  "_skip"      :: "'a com"                                  ("SKIP")
    1.13 +  "_Seq"       :: "'a com \<Rightarrow> 'a com \<Rightarrow> 'a com"              ("(_;;/ _)" [60,61] 60)
    1.14 +  "_Cond"      :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com"   ("(0IF _/ THEN _/ ELSE _/FI)" [0, 0, 0] 61)
    1.15 +  "_Cond2"     :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com"             ("(0IF _ THEN _ FI)" [0,0] 56)
    1.16 +  "_While"     :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com"             ("(0WHILE _ /DO _ /OD)"  [0, 0] 61)
    1.17 +  "_Await"     :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com"             ("(0AWAIT _ /THEN /_ /END)"  [0,0] 61)
    1.18 +  "_Atom"      :: "'a com \<Rightarrow> 'a com"                        ("(\<langle>_\<rangle>)" 61)
    1.19 +  "_Wait"      :: "'a bexp \<Rightarrow> 'a com"                       ("(0WAIT _ END)" 61)
    1.20 +
    1.21 +translations
    1.22 +  "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (\<lambda>_. a))\<guillemotright>"
    1.23 +  "SKIP" \<rightleftharpoons> "Basic id"
    1.24 +  "c1;; c2" \<rightleftharpoons> "Seq c1 c2"
    1.25 +  "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "Cond .{b}. c1 c2"
    1.26 +  "IF b THEN c FI" \<rightleftharpoons> "IF b THEN c ELSE SKIP FI"
    1.27 +  "WHILE b DO c OD" \<rightharpoonup> "While .{b}. c"
    1.28 +  "AWAIT b THEN c END" \<rightleftharpoons> "Await .{b}. c"
    1.29 +  "\<langle>c\<rangle>" \<rightleftharpoons> "AWAIT True THEN c END"
    1.30 +  "WAIT b END" \<rightleftharpoons> "AWAIT b THEN SKIP END"
    1.31 +
    1.32 +nonterminals
    1.33 +  prgs
    1.34 +
    1.35 +syntax
    1.36 +  "_PAR"        :: "prgs \<Rightarrow> 'a"              ("COBEGIN//_//COEND" 60)
    1.37 +  "_prg"        :: "'a \<Rightarrow> prgs"              ("_" 57)
    1.38 +  "_prgs"       :: "['a, prgs] \<Rightarrow> prgs"      ("_//\<parallel>//_" [60,57] 57)
    1.39 +
    1.40 +translations
    1.41 +  "_prg a" \<rightharpoonup> "[a]"
    1.42 +  "_prgs a ps" \<rightharpoonup> "a # ps"
    1.43 +  "_PAR ps" \<rightharpoonup> "ps"
    1.44 +
    1.45 +syntax
    1.46 +  "_prg_scheme" :: "['a, 'a, 'a, 'a] \<Rightarrow> prgs"  ("SCHEME [_ \<le> _ < _] _" [0,0,0,60] 57)
    1.47 +
    1.48 +translations
    1.49 +  "_prg_scheme j i k c" \<rightleftharpoons> "(map (\<lambda>i. c) [j..<k])"
    1.50 +
    1.51 +text {* Translations for variables before and after a transition: *}
    1.52 +
    1.53 +syntax 
    1.54 +  "_before" :: "id \<Rightarrow> 'a" ("\<ordmasculine>_")
    1.55 +  "_after"  :: "id \<Rightarrow> 'a" ("\<ordfeminine>_")
    1.56 + 
    1.57 +translations
    1.58 +  "\<ordmasculine>x" \<rightleftharpoons> "x \<acute>fst"
    1.59 +  "\<ordfeminine>x" \<rightleftharpoons> "x \<acute>snd"
    1.60 +
    1.61 +print_translation {*
    1.62 +  let
    1.63 +    fun quote_tr' f (t :: ts) =
    1.64 +          Term.list_comb (f $ Syntax.quote_tr' "_antiquote" t, ts)
    1.65 +      | quote_tr' _ _ = raise Match;
    1.66 +
    1.67 +    val assert_tr' = quote_tr' (Syntax.const "_Assert");
    1.68 +
    1.69 +    fun bexp_tr' name ((Const ("Collect", _) $ t) :: ts) =
    1.70 +          quote_tr' (Syntax.const name) (t :: ts)
    1.71 +      | bexp_tr' _ _ = raise Match;
    1.72 +
    1.73 +    fun upd_tr' (x_upd, T) =
    1.74 +      (case try (unsuffix Record.updateN) x_upd of
    1.75 +        SOME x => (x, if T = dummyT then T else Term.domain_type T)
    1.76 +      | NONE => raise Match);
    1.77 +
    1.78 +    fun update_name_tr' (Free x) = Free (upd_tr' x)
    1.79 +      | update_name_tr' ((c as Const ("_free", _)) $ Free x) =
    1.80 +          c $ Free (upd_tr' x)
    1.81 +      | update_name_tr' (Const x) = Const (upd_tr' x)
    1.82 +      | update_name_tr' _ = raise Match;
    1.83 +
    1.84 +    fun K_tr' (Abs (_,_,t)) = if null (loose_bnos t) then t else raise Match
    1.85 +      | K_tr' (Abs (_,_,Abs (_,_,t)$Bound 0)) = if null (loose_bnos t) then t else raise Match
    1.86 +      | K_tr' _ = raise Match;
    1.87 +
    1.88 +    fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
    1.89 +          quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
    1.90 +            (Abs (x, dummyT, K_tr' k) :: ts)
    1.91 +      | assign_tr' _ = raise Match;
    1.92 +  in
    1.93 +    [("Collect", assert_tr'), ("Basic", assign_tr'),
    1.94 +      ("Cond", bexp_tr' "_Cond"), ("While", bexp_tr' "_While_inv")]
    1.95 +  end
    1.96 +*}
    1.97 +
    1.98 +end
    1.99 \ No newline at end of file