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