src/HOL/Hoare/hoare_syntax.ML
author wenzelm
Wed Nov 26 20:05:34 2014 +0100 (2014-11-26)
changeset 59058 a78612c67ec0
parent 55659 4089f6e98ab9
child 61125 4c68426800de
permissions -rw-r--r--
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm@42153
     1
(*  Title:      HOL/Hoare/hoare_syntax.ML
wenzelm@42153
     2
    Author:     Leonor Prensa Nieto & Tobias Nipkow
wenzelm@42153
     3
wenzelm@42153
     4
Syntax translations for Hoare logic.
wenzelm@42153
     5
*)
wenzelm@42153
     6
wenzelm@42153
     7
signature HOARE_SYNTAX =
wenzelm@42153
     8
sig
wenzelm@42153
     9
  val hoare_vars_tr: term list -> term
wenzelm@42153
    10
  val spec_tr': string -> term list -> term
wenzelm@42153
    11
end;
wenzelm@42153
    12
wenzelm@42153
    13
structure Hoare_Syntax: HOARE_SYNTAX =
wenzelm@42153
    14
struct
wenzelm@42153
    15
wenzelm@42153
    16
(** parse translation **)
wenzelm@42153
    17
wenzelm@42153
    18
local
wenzelm@42153
    19
wenzelm@42153
    20
fun idt_name (Free (x, _)) = SOME x
wenzelm@51693
    21
  | idt_name (Const (@{syntax_const "_constrain"}, _) $ t $ _) = idt_name t
wenzelm@42153
    22
  | idt_name _ = NONE;
wenzelm@42153
    23
wenzelm@42153
    24
fun eq_idt tu =
wenzelm@59058
    25
  (case apply2 idt_name tu of
wenzelm@42153
    26
    (SOME x, SOME y) => x = y
wenzelm@42153
    27
  | _ => false);
wenzelm@42153
    28
wenzelm@42284
    29
fun mk_abstuple [x] body = Syntax_Trans.abs_tr [x, body]
wenzelm@42153
    30
  | mk_abstuple (x :: xs) body =
blanchet@55414
    31
      Syntax.const @{const_syntax case_prod} $ Syntax_Trans.abs_tr [x, mk_abstuple xs body];
wenzelm@42153
    32
wenzelm@42153
    33
fun mk_fbody x e [y] = if eq_idt (x, y) then e else y
wenzelm@42153
    34
  | mk_fbody x e (y :: xs) =
wenzelm@42153
    35
      Syntax.const @{const_syntax Pair} $
wenzelm@42153
    36
        (if eq_idt (x, y) then e else y) $ mk_fbody x e xs;
wenzelm@42153
    37
wenzelm@42153
    38
fun mk_fexp x e xs = mk_abstuple xs (mk_fbody x e xs);
wenzelm@42153
    39
wenzelm@42153
    40
wenzelm@42153
    41
(* bexp_tr & assn_tr *)
wenzelm@42153
    42
(*all meta-variables for bexp except for TRUE are translated as if they
wenzelm@42153
    43
  were boolean expressions*)
wenzelm@42153
    44
wenzelm@55659
    45
fun bexp_tr (Const ("TRUE", _)) _ = Syntax.const "TRUE"   (* FIXME !? *)
wenzelm@42153
    46
  | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;
wenzelm@42153
    47
wenzelm@42153
    48
fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
wenzelm@42153
    49
wenzelm@42153
    50
wenzelm@42153
    51
(* com_tr *)
wenzelm@42153
    52
wenzelm@42153
    53
fun com_tr (Const (@{syntax_const "_assign"}, _) $ x $ e) xs =
wenzelm@42153
    54
      Syntax.const @{const_syntax Basic} $ mk_fexp x e xs
wenzelm@55659
    55
  | com_tr (Const (@{const_syntax Basic},_) $ f) _ = Syntax.const @{const_syntax Basic} $ f
wenzelm@42153
    56
  | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
wenzelm@42153
    57
      Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
wenzelm@42153
    58
  | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
wenzelm@42153
    59
      Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
wenzelm@42153
    60
  | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs =
wenzelm@42153
    61
      Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
wenzelm@42153
    62
  | com_tr t _ = t;
wenzelm@42153
    63
wenzelm@42153
    64
fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = idt :: vars_tr vars
wenzelm@42153
    65
  | vars_tr t = [t];
wenzelm@42153
    66
wenzelm@42153
    67
in
wenzelm@42153
    68
wenzelm@42153
    69
fun hoare_vars_tr [vars, pre, prg, post] =
wenzelm@42153
    70
      let val xs = vars_tr vars
wenzelm@42153
    71
      in Syntax.const @{const_syntax Valid} $
wenzelm@42153
    72
         assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
wenzelm@42153
    73
      end
wenzelm@42153
    74
  | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
wenzelm@42153
    75
wenzelm@42153
    76
end;
wenzelm@42153
    77
wenzelm@42153
    78
wenzelm@42153
    79
wenzelm@42153
    80
(** print translation **)
wenzelm@42153
    81
wenzelm@42153
    82
local
wenzelm@42153
    83
wenzelm@42153
    84
fun dest_abstuple
blanchet@55414
    85
      (Const (@{const_syntax case_prod}, _) $ Abs (v, _, body)) =
wenzelm@42153
    86
        subst_bound (Syntax.free v, dest_abstuple body)
wenzelm@42153
    87
  | dest_abstuple (Abs (v,_, body)) = subst_bound (Syntax.free v, body)
wenzelm@42153
    88
  | dest_abstuple tm = tm;
wenzelm@42153
    89
blanchet@55414
    90
fun abs2list (Const (@{const_syntax case_prod}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
wenzelm@55659
    91
  | abs2list (Abs (x, T, _)) = [Free (x, T)]
wenzelm@42153
    92
  | abs2list _ = [];
wenzelm@42153
    93
wenzelm@55659
    94
fun mk_ts (Const (@{const_syntax case_prod}, _) $ Abs (_, _, t)) = mk_ts t
wenzelm@55659
    95
  | mk_ts (Abs (_, _, t)) = mk_ts t
wenzelm@42153
    96
  | mk_ts (Const (@{const_syntax Pair}, _) $ a $ b) = a :: mk_ts b
wenzelm@42153
    97
  | mk_ts t = [t];
wenzelm@42153
    98
blanchet@55414
    99
fun mk_vts (Const (@{const_syntax case_prod},_) $ Abs (x, _, t)) =
wenzelm@42153
   100
      (Syntax.free x :: abs2list t, mk_ts t)
wenzelm@42153
   101
  | mk_vts (Abs (x, _, t)) = ([Syntax.free x], [t])
wenzelm@55659
   102
  | mk_vts _ = raise Match;
wenzelm@42153
   103
wenzelm@55659
   104
fun find_ch [] _ _ = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))  (* FIXME no_ch!? *)
wenzelm@42153
   105
  | find_ch ((v, t) :: vts) i xs =
wenzelm@42153
   106
      if t = Bound i then find_ch vts (i - 1) xs
wenzelm@42153
   107
      else (true, (v, subst_bounds (xs, t)));
wenzelm@42153
   108
wenzelm@55659
   109
fun is_f (Const (@{const_syntax case_prod}, _) $ Abs _) = true
wenzelm@55659
   110
  | is_f (Abs _) = true
wenzelm@55659
   111
  | is_f _ = false;
wenzelm@42153
   112
wenzelm@42153
   113
wenzelm@42153
   114
(* assn_tr' & bexp_tr'*)
wenzelm@42153
   115
wenzelm@42153
   116
fun assn_tr' (Const (@{const_syntax Collect}, _) $ T) = dest_abstuple T
wenzelm@42153
   117
  | assn_tr' (Const (@{const_syntax inter}, _) $
wenzelm@42153
   118
        (Const (@{const_syntax Collect}, _) $ T1) $ (Const (@{const_syntax Collect}, _) $ T2)) =
wenzelm@42153
   119
      Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2
wenzelm@42153
   120
  | assn_tr' t = t;
wenzelm@42153
   121
wenzelm@42153
   122
fun bexp_tr' (Const (@{const_syntax Collect}, _) $ T) = dest_abstuple T
wenzelm@42153
   123
  | bexp_tr' t = t;
wenzelm@42153
   124
wenzelm@42153
   125
wenzelm@42153
   126
(* com_tr' *)
wenzelm@42153
   127
wenzelm@42153
   128
fun mk_assign f =
wenzelm@42153
   129
  let
wenzelm@42153
   130
    val (vs, ts) = mk_vts f;
wenzelm@42153
   131
    val (ch, which) = find_ch (vs ~~ ts) (length vs - 1) (rev vs);
wenzelm@42153
   132
  in
wenzelm@42153
   133
    if ch
wenzelm@42153
   134
    then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which
wenzelm@42153
   135
    else Syntax.const @{const_syntax annskip}
wenzelm@42153
   136
  end;
wenzelm@42153
   137
wenzelm@42153
   138
fun com_tr' (Const (@{const_syntax Basic}, _) $ f) =
wenzelm@42153
   139
      if is_f f then mk_assign f
wenzelm@42153
   140
      else Syntax.const @{const_syntax Basic} $ f
wenzelm@42153
   141
  | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) =
wenzelm@42153
   142
      Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2
wenzelm@42153
   143
  | com_tr' (Const (@{const_syntax Cond}, _) $ b $ c1 $ c2) =
wenzelm@42153
   144
      Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
wenzelm@42153
   145
  | com_tr' (Const (@{const_syntax While}, _) $ b $ I $ c) =
wenzelm@42153
   146
      Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c
wenzelm@42153
   147
  | com_tr' t = t;
wenzelm@42153
   148
wenzelm@42153
   149
in
wenzelm@42153
   150
wenzelm@55659
   151
fun spec_tr' syn [p, c, q] = Syntax.const syn $ assn_tr' p $ com_tr' c $ assn_tr' q;
wenzelm@42153
   152
wenzelm@42153
   153
end;
wenzelm@42153
   154
wenzelm@42153
   155
end;
wenzelm@42153
   156