Quelle hoare_syntax.ML Sprache: SML

(*  Title:      HOL/Hoare/hoare_syntax.ML
    Author:     Leonor Prensa Nieto & Tobias Nipkow
    Author:     Walter Guttmann (initial extension to total-correctness proofs)
    Author:     Tobias Nipkow (complete version of total correctness with separate anno type)

Syntax translations for Hoare logic.
*)

signature HOARE_SYNTAX =
sig
  val hoare_vars_tr: Proof.context -> term list -> term
  val hoare_tc_vars_tr: Proof.context -> term list -> term
  val spec_tr': string -> Proof.context -> term list -> term
  val setup:
    {Basic: string, Skip: string, Seq: string, Cond: string, While: string,
      Valid: string, ValidTC: string} -> theory -> theory
end;

structure Hoare_Syntax: HOARE_SYNTAX =
struct

(** theory data **)

structure Data = Theory_Data
(
  type T =
    {Basic: string, Skip: string, Seq: string, Cond: string, While: string,
      Valid: string, ValidTC: string} option;
  val empty: T = NONE;
  fun merge (data1, data2) =
    if is_some data1 andalso is_some data2 andalso data1 <> data2 then
      error "Cannot merge syntax from different Hoare Logics"
    else merge_options (data1, data2);
);

fun const_syntax ctxt which =
  (case Data.get (Proof_Context.theory_of ctxt) of
    SOME consts => which consts
  | NONE => error "Undefined Hoare syntax consts");

val syntax_const = Syntax.const oo const_syntax;

(** parse translation **)

local

fun idt_name (Free (x, _)) = SOME x
  | idt_name (Const (\<^syntax_const>\<open>_constrain\<close>, _) $ t $ _) = idt_name t
  | idt_name _ = NONE;

fun eq_idt tu =
  (case apply2 idt_name tu of
    (SOME x, SOME y) => x = y
  | _ => false);

fun mk_abstuple [x] body = Syntax_Trans.abs_tr [x, body]
  | mk_abstuple (x :: xs) body =
      Syntax.const \<^const_syntax>\<open>case_prod\<close> $ Syntax_Trans.abs_tr [x, mk_abstuple xs body];

fun mk_fbody x e [y] = if eq_idt (x, y) then e else y
  | mk_fbody x e (y :: xs) =
      Syntax.const \<^const_syntax>\<open>Pair\<close> $
        (if eq_idt (x, y) then e else y) $ mk_fbody x e xs;

fun mk_fexp x e xs = mk_abstuple xs (mk_fbody x e xs);

(* bexp_tr & assn_tr *)
(*all meta-variables for bexp except for TRUE are translated as if they
  were boolean expressions*)

fun bexp_tr (Const ("TRUE", _)) _ = Syntax.const "TRUE"   (* FIXME !? *)
  | bexp_tr b xs = Syntax.const \<^const_syntax>\<open>Collect\<close> $ mk_abstuple xs b;

fun assn_tr r xs = Syntax.const \<^const_syntax>\<open>Collect\<close> $ mk_abstuple xs r;

fun var_tr v xs = mk_abstuple xs v;

(* com_tr *)

fun com_tr ctxt =
  let
    fun tr (Const (\<^syntax_const>\<open>_assign\<close>, _) $ x $ e) xs =
          (syntax_const ctxt #Basic $ mk_fexp x e xs, Syntax.const \<^const_syntax>\<open>Abasic\<close>)
      | tr (Const (\<^syntax_const>\<open>_Seq\<close>,_) $ c1 $ c2) xs =
          let val (c1',a1) = tr c1 xs;
              val (c2',a2) = tr c2 xs
          in (syntax_const ctxt #Seq $ c1' $ c2', Syntax.const \<^const_syntax>\<open>Aseq\<close> $ a1 $ a2) end
      | tr (Const (\<^syntax_const>\<open>_Cond\<close>,_) $ b $ c1 $ c2) xs =
          let val (c1',a1) = tr c1 xs;
              val (c2',a2) = tr c2 xs
          in (syntax_const ctxt #Cond $ bexp_tr b xs $ c1' $ c2',
              Syntax.const \<^const_syntax>\<open>Acond\<close> $ a1 $ a2)
          end
      | tr (Const (\<^syntax_const>\<open>_While\<close>,_) $ b $ i $ v $ c) xs =
          let val (c',a) = tr c xs
              val (v',A) = case Term_Position.strip_positions v of
                Const (\<^const_syntax>\<open>HOL.eq\<close>, _) $ z $ t => (t, Syntax_Trans.abs_tr [z, a]) |
                t => (t, Abs ("n", dummyT, a))
          in (syntax_const ctxt #While $ bexp_tr b xs $ c',
              Syntax.const \<^const_syntax>\<open>Awhile\<close>
                $ assn_tr i xs $ var_tr v' xs $ A)
          end
      | tr (Const (\<^syntax_const>\<open>_While0\<close>,_) $ b $ I $ c) xs =
          let val (c',a) = tr c xs
          in (syntax_const ctxt #While $ bexp_tr b xs $ c',
              Syntax.const \<^const_syntax>\<open>Awhile\<close>
                $ assn_tr I xs $ var_tr (Syntax.const \<^const_syntax>\<open>zero_class.zero\<close>) xs
                $ absdummy dummyT a)
          end
      | tr t _ = (t, Syntax.const \<^const_syntax>\<open>Abasic\<close>)
  in tr end;

fun vars_tr (Const (\<^syntax_const>\<open>_idts\<close>, _) $ idt $ vars) = idt :: vars_tr vars
  | vars_tr t = [t];

in

fun hoare_vars_tr ctxt [vars, pre, prg, post] =
      let val xs = vars_tr vars
          val (c',a) = com_tr ctxt prg xs
      in syntax_const ctxt #Valid $ assn_tr pre xs $ c' $ a $ assn_tr post xs end
  | hoare_vars_tr _ ts = raise TERM ("hoare_vars_tr", ts);

fun hoare_tc_vars_tr ctxt [vars, pre, prg, post] =
      let val xs = vars_tr vars
          val (c',a) = com_tr ctxt prg xs
      in syntax_const ctxt #ValidTC $ assn_tr pre xs $ c' $ a $ assn_tr post xs end
  | hoare_tc_vars_tr _ ts = raise TERM ("hoare_tc_vars_tr", ts);

end;

(** print translation **)

local

fun dest_abstuple
      (Const (\<^const_syntax>\<open>case_prod\<close>, _) $ Abs (v, _, body)) =
        subst_bound (Syntax.free v, dest_abstuple body)
  | dest_abstuple (Abs (v,_, body)) = subst_bound (Syntax.free v, body)
  | dest_abstuple tm = tm;

fun abs2list (Const (\<^const_syntax>\<open>case_prod\<close>, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
  | abs2list (Abs (x, T, _)) = [Free (x, T)]
  | abs2list _ = [];

fun mk_ts (Const (\<^const_syntax>\<open>case_prod\<close>, _) $ Abs (_, _, t)) = mk_ts t
  | mk_ts (Abs (_, _, t)) = mk_ts t
  | mk_ts (Const (\<^const_syntax>\<open>Pair\<close>, _) $ a $ b) = a :: mk_ts b
  | mk_ts t = [t];

fun mk_vts (Const (\<^const_syntax>\<open>case_prod\<close>,_) $ Abs (x, _, t)) =
      (Syntax.free x :: abs2list t, mk_ts t)
  | mk_vts (Abs (x, _, t)) = ([Syntax.free x], [t])
  | mk_vts _ = raise Match;

fun find_ch [] _ _ = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))  (* FIXME no_ch!? *)
  | find_ch ((v, t) :: vts) i xs =
      if t = Bound i then find_ch vts (i - 1) xs
      else (true, (v, subst_bounds (xs, t)));

fun is_f (Const (\<^const_syntax>\<open>case_prod\<close>, _) $ Abs _) = true
  | is_f (Abs _) = true
  | is_f _ = false;

(* assn_tr' & bexp_tr'*)

fun assn_tr' (Const (\<^const_syntax>\Collect\, _) $ T) = dest_abstuple T
  | assn_tr' (Const (\<^const_syntax>\inter\, _) $
        (Const (\<^const_syntax>\<open>Collect\<close>, _) $ T1) $ (Const (\<^const_syntax>\<open>Collect\<close>, _) $ T2)) =
      Syntax.const \<^const_syntax>\<open>inter\<close> $ dest_abstuple T1 $ dest_abstuple T2
  | assn_tr' t = t;

fun bexp_tr' (Const (\<^const_syntax>\Collect\, _) $ T) = dest_abstuple T
  | bexp_tr' t = t;

fun var_tr' xo T =
  let val n = dest_abstuple T
  in case xo of NONE => n | SOME x => Syntax.const \<^const_syntax>\<open>HOL.eq\<close> $ Syntax.free x $ n end

(* com_tr' *)

fun mk_assign ctxt f =
  let
    val (vs, ts) = mk_vts f;
    val (ch, (a, b)) = find_ch (vs ~~ ts) (length vs - 1) (rev vs);
  in
    if ch
    then Syntax.const \<^syntax_const>\<open>_assign\<close> $ a $ b
    else syntax_const ctxt #Skip
  end;

fun com_tr' ctxt (t,a) =
  let
    val (head, args) = apfst (try Term.dest_Const_name) (Term.strip_comb t);
    fun arg k = nth args (k - 1);
    val n = length args;
    val (_, args_a) = apfst (try Term.dest_Const_name) (Term.strip_comb a);
    fun arg_a k = nth args_a (k - 1)
  in
    case head of
      NONE => t
    | SOME c =>
        if c = const_syntax ctxt #Basic andalso n = 1 andalso is_f (arg 1) then
          mk_assign ctxt (arg 1)
        else if c = const_syntax ctxt #Seq andalso n = 2 then
          Syntax.const \<^syntax_const>\<open>_Seq\<close>
            $ com_tr' ctxt (arg 1, arg_a 1) $ com_tr' ctxt (arg 2, arg_a 2)
        else if c = const_syntax ctxt #Cond andalso n = 3 then
          Syntax.const \<^syntax_const>\<open>_Cond\<close> $
            bexp_tr' (arg 1) $ com_tr' ctxt (arg 2, arg_a 1) $ com_tr' ctxt (arg 3, arg_a 2)
        else if c = const_syntax ctxt #While andalso n = 2 then
               let val (xo,a') = case arg_a 3 of
                     Abs(x,_,a) => (if loose_bvar1(a,0) then SOME x else NONE,
                                    subst_bound (Syntax.free x, a)) |
                     t => (NONE,t)
               in Syntax.const \<^syntax_const>\<open>_While\<close>
                 $ bexp_tr' (arg 1) $ assn_tr' (arg_a 1) $ var_tr' xo (arg_a 2) $ com_tr' ctxt (arg 2, a')
               end
        else t
  end;

in

fun spec_tr' syn ctxt [p, c, a, q] =
  Syntax.const syn $ assn_tr' p $ com_tr' ctxt (c,a) $ assn_tr' q;

end;

(** setup **)

val _ =
  Theory.setup
   (Sign.parse_translation
    [(\<^syntax_const>\<open>_hoare_vars\<close>, hoare_vars_tr),
     (\<^syntax_const>\<open>_hoare_vars_tc\<close>, hoare_tc_vars_tr)]);

fun setup consts =
  Data.put (SOME consts) #>
  Sign.print_translation
   [(#Valid consts, spec_tr' \<^syntax_const>\_hoare\),
    (#ValidTC consts, spec_tr' \<^syntax_const>\_hoare_tc\)];

end;

quality95%

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.