src/HOL/Hoare/hoare_syntax.ML
changeset 42153 fa108629d132
child 42284 326f57825e1a
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Hoare/hoare_syntax.ML	Tue Mar 29 21:48:01 2011 +0200
     1.3 @@ -0,0 +1,156 @@
     1.4 +(*  Title:      HOL/Hoare/hoare_syntax.ML
     1.5 +    Author:     Leonor Prensa Nieto & Tobias Nipkow
     1.6 +
     1.7 +Syntax translations for Hoare logic.
     1.8 +*)
     1.9 +
    1.10 +signature HOARE_SYNTAX =
    1.11 +sig
    1.12 +  val hoare_vars_tr: term list -> term
    1.13 +  val spec_tr': string -> term list -> term
    1.14 +end;
    1.15 +
    1.16 +structure Hoare_Syntax: HOARE_SYNTAX =
    1.17 +struct
    1.18 +
    1.19 +(** parse translation **)
    1.20 +
    1.21 +local
    1.22 +
    1.23 +fun idt_name (Free (x, _)) = SOME x
    1.24 +  | idt_name (Const ("_constrain", _) $ t $ _) = idt_name t
    1.25 +  | idt_name _ = NONE;
    1.26 +
    1.27 +fun eq_idt tu =
    1.28 +  (case pairself idt_name tu of
    1.29 +    (SOME x, SOME y) => x = y
    1.30 +  | _ => false);
    1.31 +
    1.32 +fun mk_abstuple [x] body = Syntax.abs_tr [x, body]
    1.33 +  | mk_abstuple (x :: xs) body =
    1.34 +      Syntax.const @{const_syntax prod_case} $ Syntax.abs_tr [x, mk_abstuple xs body];
    1.35 +
    1.36 +fun mk_fbody x e [y] = if eq_idt (x, y) then e else y
    1.37 +  | mk_fbody x e (y :: xs) =
    1.38 +      Syntax.const @{const_syntax Pair} $
    1.39 +        (if eq_idt (x, y) then e else y) $ mk_fbody x e xs;
    1.40 +
    1.41 +fun mk_fexp x e xs = mk_abstuple xs (mk_fbody x e xs);
    1.42 +
    1.43 +
    1.44 +(* bexp_tr & assn_tr *)
    1.45 +(*all meta-variables for bexp except for TRUE are translated as if they
    1.46 +  were boolean expressions*)
    1.47 +
    1.48 +fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE"   (* FIXME !? *)
    1.49 +  | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;
    1.50 +
    1.51 +fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
    1.52 +
    1.53 +
    1.54 +(* com_tr *)
    1.55 +
    1.56 +fun com_tr (Const (@{syntax_const "_assign"}, _) $ x $ e) xs =
    1.57 +      Syntax.const @{const_syntax Basic} $ mk_fexp x e xs
    1.58 +  | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
    1.59 +  | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
    1.60 +      Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
    1.61 +  | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
    1.62 +      Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
    1.63 +  | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs =
    1.64 +      Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
    1.65 +  | com_tr t _ = t;
    1.66 +
    1.67 +fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = idt :: vars_tr vars
    1.68 +  | vars_tr t = [t];
    1.69 +
    1.70 +in
    1.71 +
    1.72 +fun hoare_vars_tr [vars, pre, prg, post] =
    1.73 +      let val xs = vars_tr vars
    1.74 +      in Syntax.const @{const_syntax Valid} $
    1.75 +         assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
    1.76 +      end
    1.77 +  | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
    1.78 +
    1.79 +end;
    1.80 +
    1.81 +
    1.82 +
    1.83 +(** print translation **)
    1.84 +
    1.85 +local
    1.86 +
    1.87 +fun dest_abstuple
    1.88 +      (Const (@{const_syntax prod_case}, _) $ Abs (v, _, body)) =
    1.89 +        subst_bound (Syntax.free v, dest_abstuple body)
    1.90 +  | dest_abstuple (Abs (v,_, body)) = subst_bound (Syntax.free v, body)
    1.91 +  | dest_abstuple tm = tm;
    1.92 +
    1.93 +fun abs2list (Const (@{const_syntax prod_case}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
    1.94 +  | abs2list (Abs (x, T, t)) = [Free (x, T)]
    1.95 +  | abs2list _ = [];
    1.96 +
    1.97 +fun mk_ts (Const (@{const_syntax prod_case}, _) $ Abs (x, _, t)) = mk_ts t
    1.98 +  | mk_ts (Abs (x, _, t)) = mk_ts t
    1.99 +  | mk_ts (Const (@{const_syntax Pair}, _) $ a $ b) = a :: mk_ts b
   1.100 +  | mk_ts t = [t];
   1.101 +
   1.102 +fun mk_vts (Const (@{const_syntax prod_case},_) $ Abs (x, _, t)) =
   1.103 +      (Syntax.free x :: abs2list t, mk_ts t)
   1.104 +  | mk_vts (Abs (x, _, t)) = ([Syntax.free x], [t])
   1.105 +  | mk_vts t = raise Match;
   1.106 +
   1.107 +fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))  (* FIXME no_ch!? *)
   1.108 +  | find_ch ((v, t) :: vts) i xs =
   1.109 +      if t = Bound i then find_ch vts (i - 1) xs
   1.110 +      else (true, (v, subst_bounds (xs, t)));
   1.111 +
   1.112 +fun is_f (Const (@{const_syntax prod_case}, _) $ Abs (x, _, t)) = true
   1.113 +  | is_f (Abs (x, _, t)) = true
   1.114 +  | is_f t = false;
   1.115 +
   1.116 +
   1.117 +(* assn_tr' & bexp_tr'*)
   1.118 +
   1.119 +fun assn_tr' (Const (@{const_syntax Collect}, _) $ T) = dest_abstuple T
   1.120 +  | assn_tr' (Const (@{const_syntax inter}, _) $
   1.121 +        (Const (@{const_syntax Collect}, _) $ T1) $ (Const (@{const_syntax Collect}, _) $ T2)) =
   1.122 +      Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2
   1.123 +  | assn_tr' t = t;
   1.124 +
   1.125 +fun bexp_tr' (Const (@{const_syntax Collect}, _) $ T) = dest_abstuple T
   1.126 +  | bexp_tr' t = t;
   1.127 +
   1.128 +
   1.129 +(* com_tr' *)
   1.130 +
   1.131 +fun mk_assign f =
   1.132 +  let
   1.133 +    val (vs, ts) = mk_vts f;
   1.134 +    val (ch, which) = find_ch (vs ~~ ts) (length vs - 1) (rev vs);
   1.135 +  in
   1.136 +    if ch
   1.137 +    then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which
   1.138 +    else Syntax.const @{const_syntax annskip}
   1.139 +  end;
   1.140 +
   1.141 +fun com_tr' (Const (@{const_syntax Basic}, _) $ f) =
   1.142 +      if is_f f then mk_assign f
   1.143 +      else Syntax.const @{const_syntax Basic} $ f
   1.144 +  | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) =
   1.145 +      Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2
   1.146 +  | com_tr' (Const (@{const_syntax Cond}, _) $ b $ c1 $ c2) =
   1.147 +      Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
   1.148 +  | com_tr' (Const (@{const_syntax While}, _) $ b $ I $ c) =
   1.149 +      Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c
   1.150 +  | com_tr' t = t;
   1.151 +
   1.152 +in
   1.153 +
   1.154 +fun spec_tr' syn [p, c, q] = Syntax.const syn $ assn_tr' p $ com_tr' c $ assn_tr' q
   1.155 +
   1.156 +end;
   1.157 +
   1.158 +end;
   1.159 +