Quelle spark_vcs.ML Sprache: SML

(*  Title:      HOL/SPARK/Tools/spark_vcs.ML
    Author:     Stefan Berghofer
    Copyright:  secunet Security Networks AG

Store for verification conditions generated by SPARK/Ada.
*)

signature SPARK_VCS =
sig
  val set_vcs: Fdl_Parser.decls -> Fdl_Parser.rules ->
    (string * string) * Fdl_Parser.vcs -> Path.T -> string -> theory -> theory
  val add_proof_fun: (typ option -> 'a -> term) ->
    string * ((string list * string) option * 'a) ->
    theory -> theory
  val add_type: string * (typ * (string * string) list) -> theory -> theory
  val lookup_vc: theory -> bool -> string -> (Element.context_i list *
    (string * thm list option * Element.context_i * Element.statement_i)) option
  val get_vcs: theory -> bool ->
    Element.context_i list * (binding * thm) list * (string *
    (string * thm list option * Element.context_i * Element.statement_i)) list
  val mark_proved: string -> thm list -> theory -> theory
  val close: bool -> theory -> theory
  val is_closed: theory -> bool
end;

structure SPARK_VCs: SPARK_VCS =
struct

open Fdl_Parser;

(** theory data **)

fun err_unfinished () = error "An unfinished SPARK environment is still open."

val strip_number = apply2 implode o chop_suffix Fdl_Lexer.is_digit o raw_explode;

val name_ord = prod_ord string_ord (option_ord int_ord) o
  apply2 (strip_number ##> Int.fromString);

structure VCtab = Table(type key = string val ord = name_ord);

structure VCs = Theory_Data
(
  type T =
    {pfuns: ((string list * string) option * term) Symtab.table,
     type_map: (typ * (string * string) list) Symtab.table,
     env:
       {ctxt: Element.context_i list,
        defs: (binding * thm) list,
        types: fdl_type tab,
        funs: (string list * string) tab,
        pfuns: ((string list * string) option * term) Symtab.table,
        ids: (term * string) Symtab.table * Name.context,
        proving: bool,
        vcs: (string * thm list option *
          (string * expr) list * (string * expr) list) VCtab.table,
        path: Path.T,
        prefix: string} option}
  val empty : T = {pfuns = Symtab.empty, type_map = Symtab.empty, env = NONE}
  fun merge ({pfuns = pfuns1, type_map = type_map1, env = NONE},
        {pfuns = pfuns2, type_map = type_map2, env = NONE}) =
        {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2),
         type_map = Symtab.merge (op =) (type_map1, type_map2),
         env = NONE}
    | merge _ = err_unfinished ()
)

(** utilities **)

val to_lower = raw_explode #> map Symbol.to_ascii_lower #> implode;

val lcase_eq = (op =) o apply2 (to_lower o Long_Name.base_name);

fun lookup_prfx "" tab s = Symtab.lookup tab s
  | lookup_prfx prfx tab s = (case Symtab.lookup tab s of
        NONE => Symtab.lookup tab (prfx ^ "__" ^ s)
      | x => x);

fun strip_prfx s =
  let
    fun strip ys [] = ("", implode ys)
      | strip ys ("_" :: "_" :: xs) = (implode (rev xs), implode ys)
      | strip ys (x :: xs) = strip (x :: ys) xs
  in strip [] (rev (raw_explode s)) end;

fun unprefix_pfun "" s = s
  | unprefix_pfun prfx s =
      let val (prfx', s') = strip_prfx s
      in if prfx = prfx' then s' else s end;

fun mk_uminus t =
  let val T = fastype_of t
  in \<^Const>\<open>uminus T for t\<close> end;

fun mk_times (t, u) =
  let
    val setT = fastype_of t;
    val T = HOLogic.dest_setT setT;
    val U = HOLogic.dest_setT (fastype_of u)
  in \<^Const>\<open>Sigma T U for t \<open>Abs ("", T, u)\<close>\<close> end;

fun get_type thy prfx ty =
  let val {type_map, ...} = VCs.get thy
  in lookup_prfx prfx type_map ty end;

fun mk_type' _ _ "integer" = (HOLogic.intT, [])
  | mk_type' _ _ "boolean" = (HOLogic.boolT, [])
  | mk_type' thy prfx ty =
      (case get_type thy prfx ty of
         NONE =>
           (Syntax.check_typ (Proof_Context.init_global thy)
              (Type (Sign.full_name thy (Binding.name ty), [])),
            [])
       | SOME p => p);

fun mk_type thy prfx ty = fst (mk_type' thy prfx ty);

val booleanN = "boolean";
val integerN = "integer";

fun define_overloaded (def_name, eq) lthy =
  let
    val ((c, _), rhs) = eq |> Syntax.check_term lthy |>
      Logic.dest_equals |>> dest_Free;
    val ((_, (_, thm)), lthy') = Local_Theory.define
      ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs)) lthy
    val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
    val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm
  in (thm', lthy') end;

fun strip_underscores s =
  strip_underscores (unsuffix "_" s) handle Fail _ => s;

fun strip_tilde s =
  unsuffix "~" s ^ "_init" handle Fail _ => s;

val mangle_name = strip_underscores #> strip_tilde;

fun mk_variables thy prfx xs ty (tab, ctxt) =
  let
    val T = mk_type thy prfx ty;
    val (ys, ctxt') = fold_map Name.variant (map mangle_name xs) ctxt;
    val zs = map (Free o rpair T) ys;
  in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end;

fun get_record_info thy T = (case Record.dest_recTs T of
    [(tyname, [\<^typ>\<open>unit\<close>])] =>
      Record.get_info thy (Long_Name.qualifier tyname)
  | _ => NONE);

fun find_field [] fname fields =
      find_first (curry lcase_eq fname o fst) fields
  | find_field cmap fname fields =
      (case AList.lookup (op =) cmap fname of
         NONE => NONE
       | SOME fname' => SOME (fname', the (AList.lookup (op =) fields fname')));

fun find_field' fname = get_first (fn (flds, fldty) =>
  if member (op =) flds fname then SOME fldty else NONE);

fun assoc_ty_err thy T s msg =
  error ("Type " ^ Syntax.string_of_typ_global thy T ^
    " associated with SPARK type " ^ s ^ "\n" ^ msg);

(** generate properties of enumeration types **)

fun add_enum_type tyname tyname' thy =
  let
    val {case_name, ...} = the (BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] tyname');
    val cs = map Const (the (BNF_LFP_Compat.get_constrs thy tyname'));
    val k = length cs;
    val T = Type (tyname', []);
    val p = \<^Const>\<open>pos T\<close>;
    val v = \<^Const>\<open>val T\<close>;
    val card = \<^Const>\<open>card T for \<open>HOLogic.mk_UNIV T\<close>\<close>;

    fun mk_binrel_def rel f = Logic.mk_equals
      (rel T, Abs ("x", T, Abs ("y", T, rel \<^Type>\<open>int\<close> $ (f $ Bound 1) $ (f $ Bound 0))));

    val (((def1, def2), def3), lthy) = thy |>

      Class.instantiation ([tyname'], [], \<^sort>\spark_enum\) |>

      define_overloaded ("pos_" ^ tyname ^ "_def", Logic.mk_equals
        (p,
         list_comb (Const (case_name, replicate k HOLogic.intT @
             [T] ---> HOLogic.intT),
           map (HOLogic.mk_number HOLogic.intT) (0 upto k - 1)))) ||>>

      define_overloaded ("less_eq_" ^ tyname ^ "_def",
        mk_binrel_def (fn T => \<^Const>\<open>less_eq T\<close>) p) ||>>
      define_overloaded ("less_" ^ tyname ^ "_def",
        mk_binrel_def (fn T => \<^Const>\<open>less T\<close>) p);

    val UNIV_eq = Goal.prove lthy [] []
      (HOLogic.mk_Trueprop (HOLogic.mk_eq
         (HOLogic.mk_UNIV T, HOLogic.mk_set T cs)))
      (fn {context = ctxt, ...} =>
         resolve_tac ctxt @{thms subset_antisym} 1 THEN
         resolve_tac ctxt @{thms subsetI} 1 THEN
         Old_Datatype_Aux.exh_tac ctxt (K (#exhaust (BNF_LFP_Compat.the_info
           (Proof_Context.theory_of ctxt) [BNF_LFP_Compat.Keep_Nesting] tyname'))) 1 THEN
         ALLGOALS (asm_full_simp_tac ctxt));

    val finite_UNIV = Goal.prove lthy [] []
      (HOLogic.mk_Trueprop \<^Const>\<open>finite T for \<open>HOLogic.mk_UNIV T\<close>\<close>)
      (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [UNIV_eq]) 1);

    val card_UNIV = Goal.prove lthy [] []
      (HOLogic.mk_Trueprop (HOLogic.mk_eq
         (card, HOLogic.mk_number HOLogic.natT k)))
      (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [UNIV_eq]) 1);

    val range_pos = Goal.prove lthy [] []
      (HOLogic.mk_Trueprop (HOLogic.mk_eq
         (\<^Const>\<open>image T \<^Type>\<open>int\<close> for p \<open>HOLogic.mk_UNIV T\<close>\<close>,
          \<^Const>\<open>atLeastLessThan \<^Type>\<open>int\<close>
            for \<open>HOLogic.mk_number HOLogic.intT 0\<close> \<open>\<^term>\<open>int\<close> $ card\<close>\<close>)))
      (fn {context = ctxt, ...} =>
         simp_tac (ctxt addsimps [card_UNIV]) 1 THEN
         simp_tac (ctxt addsimps [UNIV_eq, def1]) 1 THEN
         resolve_tac ctxt @{thms subset_antisym} 1 THEN
         simp_tac ctxt 1 THEN
         resolve_tac ctxt @{thms subsetI} 1 THEN
         asm_full_simp_tac (ctxt addsimps @{thms interval_expand}
           delsimps @{thms atLeastLessThan_iff}) 1);

    val lthy' =
      Class.prove_instantiation_instance (fn ctxt =>
        Class.intro_classes_tac ctxt [] THEN
        resolve_tac ctxt [finite_UNIV] 1 THEN
        resolve_tac ctxt [range_pos] 1 THEN
        simp_tac (put_simpset HOL_basic_ss ctxt addsimps [def3]) 1 THEN
        simp_tac (put_simpset HOL_basic_ss ctxt addsimps [def2]) 1) lthy;

    val (pos_eqs, val_eqs) = split_list (map_index (fn (i, c) =>
      let
        val n = HOLogic.mk_number HOLogic.intT i;
        val th = Goal.prove lthy' [] []
          (HOLogic.mk_Trueprop (HOLogic.mk_eq (p $ c, n)))
          (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [def1]) 1);
        val th' = Goal.prove lthy' [] []
          (HOLogic.mk_Trueprop (HOLogic.mk_eq (v $ n, c)))
          (fn {context = ctxt, ...} =>
             resolve_tac ctxt [@{thm inj_pos} RS @{thm injD}] 1 THEN
             simp_tac (ctxt addsimps [@{thm pos_val}, range_pos, card_UNIV, th]) 1)
      in (th, th') end) cs);

    val first_el = Goal.prove lthy' [] []
      (HOLogic.mk_Trueprop (HOLogic.mk_eq (\<^Const>\<open>first_el T\<close>, hd cs)))
      (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [@{thm first_el_def}, hd val_eqs]) 1);

    val last_el = Goal.prove lthy' [] []
      (HOLogic.mk_Trueprop (HOLogic.mk_eq (\<^Const>\<open>last_el T\<close>, List.last cs)))
      (fn {context = ctxt, ...} =>
        simp_tac (ctxt addsimps [@{thm last_el_def}, List.last val_eqs, card_UNIV]) 1);
  in
    lthy' |>
    Local_Theory.note
      ((Binding.name (tyname ^ "_card"), @{attributes [simp]}), [card_UNIV]) ||>>
    Local_Theory.note
      ((Binding.name (tyname ^ "_pos"), @{attributes [simp]}), pos_eqs) ||>>
    Local_Theory.note
      ((Binding.name (tyname ^ "_val"), @{attributes [simp]}), val_eqs) ||>>
    Local_Theory.note
      ((Binding.name (tyname ^ "_first_el"), @{attributes [simp]}), [first_el]) ||>>
    Local_Theory.note
      ((Binding.name (tyname ^ "_last_el"), @{attributes [simp]}), [last_el]) |> snd |>
    Local_Theory.exit_global
  end;

fun check_no_assoc thy prfx s = case get_type thy prfx s of
    NONE => ()
  | SOME _ => error ("Cannot associate a type with " ^ s ^
      "\nsince it is no record or enumeration type");

fun check_enum [] [] = NONE
  | check_enum els [] = SOME ("has no element(s) " ^ commas els)
  | check_enum [] cs = SOME ("has extra element(s) " ^
      commas (map (Long_Name.base_name o fst) cs))
  | check_enum (el :: els) ((cname, _) :: cs) =
      if lcase_eq (el, cname) then check_enum els cs
      else SOME ("either has no element " ^ el ^
        " or it is at the wrong position");

fun invert_map [] = I
  | invert_map cmap =
      map (apfst (the o AList.lookup (op =) (map swap cmap)));

fun add_type_def prfx (s, Basic_Type ty) (ids, thy) =
      (check_no_assoc thy prfx s;
       (ids,
        Typedecl.abbrev_global (Binding.name s, [], NoSyn)
          (mk_type thy prfx ty) thy |> snd))

  | add_type_def prfx (s, Enum_Type els) ((tab, ctxt), thy) =
      let
        val (thy', tyname) = (case get_type thy prfx s of
            NONE =>
              let
                val tyb = Binding.name s;
                val tyname = Sign.full_name thy tyb
              in
                (thy |>
                 BNF_LFP_Compat.add_datatype [BNF_LFP_Compat.Keep_Nesting]
                   [((tyb, [], NoSyn),
                     map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |>
                 add_enum_type s tyname,
                 tyname)
              end
          | SOME (T as Type (tyname, []), cmap) =>
              (case BNF_LFP_Compat.get_constrs thy tyname of
                 NONE => assoc_ty_err thy T s "is not a datatype"
               | SOME cs =>
                   let val (prfx', _) = strip_prfx s
                   in
                     case check_enum (map (unprefix_pfun prfx') els)
                         (invert_map cmap cs) of
                       NONE => (thy, tyname)
                     | SOME msg => assoc_ty_err thy T s msg
                   end)
          | SOME (T, _) => assoc_ty_err thy T s "is not a datatype");
        val cs = map Const (the (BNF_LFP_Compat.get_constrs thy' tyname));
      in
        ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,
          fold Name.declare els ctxt),
         thy')
      end

  | add_type_def prfx (s, Array_Type (argtys, resty)) (ids, thy) =
      (check_no_assoc thy prfx s;
       (ids,
        Typedecl.abbrev_global (Binding.name s, [], NoSyn)
          (foldr1 HOLogic.mk_prodT (map (mk_type thy prfx) argtys) -->
             mk_type thy prfx resty) thy |> snd))

  | add_type_def prfx (s, Record_Type fldtys) (ids, thy) =
      (ids,
       let val fldTs = maps (fn (flds, ty) =>
         map (rpair (mk_type thy prfx ty)) flds) fldtys
       in case get_type thy prfx s of
           NONE =>
             Record.add_record {overloaded = false} ([], Binding.name s) NONE
               (map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy
         | SOME (rT, cmap) =>
             (case get_record_info thy rT of
                NONE => assoc_ty_err thy rT s "is not a record type"
              | SOME {fields, ...} =>
                  let val fields' = invert_map cmap fields
                  in
                    (case subtract (lcase_eq o apply2 fst) fldTs fields' of
                       [] => ()
                     | flds => assoc_ty_err thy rT s ("has extra field(s) " ^
                         commas (map (Long_Name.base_name o fst) flds));
                     map (fn (fld, T) =>
                       case AList.lookup lcase_eq fields' fld of
                         NONE => assoc_ty_err thy rT s ("has no field " ^ fld)
                       | SOME U => T = U orelse assoc_ty_err thy rT s
                           ("has field " ^
                            fld ^ " whose type\n" ^
                            Syntax.string_of_typ_global thy U ^
                            "\ndoes not match declared type\n" ^
                            Syntax.string_of_typ_global thy T)) fldTs;
                     thy)
                  end)
       end)

  | add_type_def prfx (s, Pending_Type) (ids, thy) =
      (ids,
       case get_type thy prfx s of
         SOME _ => thy
       | NONE => Typedecl.typedecl_global {final = true} (Binding.name s, [], NoSyn) thy |> snd);

fun term_of_expr thy prfx types pfuns =
  let
    fun tm_of vs (Funct ("->", [e, e'])) =
          (HOLogic.mk_imp (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

      | tm_of vs (Funct ("<->", [e, e'])) =
          (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

      | tm_of vs (Funct ("or", [e, e'])) =
          (HOLogic.mk_disj (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

      | tm_of vs (Funct ("and", [e, e'])) =
          (HOLogic.mk_conj (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

      | tm_of vs (Funct ("not", [e])) =
          (HOLogic.mk_not (fst (tm_of vs e)), booleanN)

      | tm_of vs (Funct ("=", [e, e'])) =
          (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

      | tm_of vs (Funct ("<>", [e, e'])) = (HOLogic.mk_not
          (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e'))), booleanN)

      | tm_of vs (Funct ("<", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\less\
          (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

      | tm_of vs (Funct (">", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\less\
          (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)

      | tm_of vs (Funct ("<=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\less_eq\
          (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

      | tm_of vs (Funct (">=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\less_eq\
          (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)

      | tm_of vs (Funct ("+", [e, e'])) = (HOLogic.mk_binop \<^const_name>\plus\
          (fst (tm_of vs e), fst (tm_of vs e')), integerN)

      | tm_of vs (Funct ("-", [e, e'])) = (HOLogic.mk_binop \<^const_name>\minus\
          (fst (tm_of vs e), fst (tm_of vs e')), integerN)

      | tm_of vs (Funct ("*", [e, e'])) = (HOLogic.mk_binop \<^const_name>\times\
          (fst (tm_of vs e), fst (tm_of vs e')), integerN)

      | tm_of vs (Funct ("/", [e, e'])) = (HOLogic.mk_binop \<^const_name>\divide\
          (fst (tm_of vs e), fst (tm_of vs e')), integerN)

      | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop \<^const_name>\sdiv\
          (fst (tm_of vs e), fst (tm_of vs e')), integerN)

      | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop \<^const_name>\modulo\
          (fst (tm_of vs e), fst (tm_of vs e')), integerN)

      | tm_of vs (Funct ("-", [e])) = (mk_uminus (fst (tm_of vs e)), integerN)

      | tm_of vs (Funct ("**", [e, e'])) =
          (\<^Const>\<open>power \<^Type>\<open>int\<close>\<close> $ fst (tm_of vs e) $ (\<^Const>\<open>nat\<close> $ fst (tm_of vs e')), integerN)

      | tm_of (tab, _) (Ident s) =
          (case Symtab.lookup tab s of
             SOME t_ty => t_ty
           | NONE => (case lookup_prfx prfx pfuns s of
               SOME (SOME ([], resty), t) => (t, resty)
             | _ => error ("Undeclared identifier " ^ s)))

      | tm_of _ (Number i) = (HOLogic.mk_number HOLogic.intT i, integerN)

      | tm_of vs (Quantifier (s, xs, ty, e)) =
          let
            val (ys, vs') = mk_variables thy prfx xs ty vs;
            val q = (case s of
                "for_all" => HOLogic.mk_all
              | "for_some" => HOLogic.mk_exists)
          in
            (fold_rev (fn Free (x, T) => fn t => q (x, T, t))
               ys (fst (tm_of vs' e)),
             booleanN)
          end

      | tm_of vs (Funct (s, es)) =

          (* record field selection *)
          (case try (unprefix "fld_") s of
             SOME fname => (case es of
               [e] =>
                 let
                   val (t, rcdty) = tm_of vs e;
                   val (rT, cmap) = mk_type' thy prfx rcdty
                 in case (get_record_info thy rT, lookup types rcdty) of
                     (SOME {fields, ...}, SOME (Record_Type fldtys)) =>
                       (case (find_field cmap fname fields,
                            find_field' fname fldtys) of
                          (SOME (fname', fT), SOME fldty) =>
                            (Const (fname', rT --> fT) $ t, fldty)
                        | _ => error ("Record " ^ rcdty ^
                            " has no field named " ^ fname))
                   | _ => error (rcdty ^ " is not a record type")
                 end
             | _ => error ("Function " ^ s ^ " expects one argument"))
           | NONE =>

          (* record field update *)
          (case try (unprefix "upf_") s of
             SOME fname => (case es of
               [e, e'] =>
                 let
                   val (t, rcdty) = tm_of vs e;
                   val (rT, cmap) = mk_type' thy prfx rcdty;
                   val (u, fldty) = tm_of vs e';
                   val fT = mk_type thy prfx fldty
                 in case get_record_info thy rT of
                     SOME {fields, ...} =>
                       (case find_field cmap fname fields of
                          SOME (fname', fU) =>
                            if fT = fU then
                              (Const (fname' ^ "_update",
                                 (fT --> fT) --> rT --> rT) $
                                   Abs ("x", fT, u) $ t,
                               rcdty)
                            else error ("Type\n" ^
                              Syntax.string_of_typ_global thy fT ^
                              "\ndoes not match type\n" ^
                              Syntax.string_of_typ_global thy fU ^
                              "\nof field " ^ fname)
                        | NONE => error ("Record " ^ rcdty ^
                            " has no field named " ^ fname))
                   | _ => error (rcdty ^ " is not a record type")
                 end
             | _ => error ("Function " ^ s ^ " expects two arguments"))
           | NONE =>

          (* enumeration type to integer *)
          (case try (unsuffix "__pos") s of
             SOME tyname => (case es of
               [e] => (\<^Const>\<open>pos \<open>mk_type thy prfx tyname\<close> for \<open>fst (tm_of vs e)\<close>\<close>, integerN)
             | _ => error ("Function " ^ s ^ " expects one argument"))
           | NONE =>

          (* integer to enumeration type *)
          (case try (unsuffix "__val") s of
             SOME tyname => (case es of
               [e] => (\<^Const>\<open>val \<open>mk_type thy prfx tyname\<close> for \<open>fst (tm_of vs e)\<close>\<close>, tyname)
             | _ => error ("Function " ^ s ^ " expects one argument"))
           | NONE =>

          (* successor / predecessor of enumeration type element *)
          if s = "succ" orelse s = "pred" then (case es of
              [e] =>
                let
                  val (t, tyname) = tm_of vs e;
                  val T = mk_type thy prfx tyname;
                  val const = if s = "succ" then \<^Const>\<open>succ T\<close> else \<^Const>\<open>pred T\<close>;
                in (const $ t, tyname) end
            | _ => error ("Function " ^ s ^ " expects one argument"))

          (* user-defined proof function *)
          else
            (case lookup_prfx prfx pfuns s of
               SOME (SOME (_, resty), t) =>
                 (list_comb (t, map (fst o tm_of vs) es), resty)
             | _ => error ("Undeclared proof function " ^ s))))))

      | tm_of vs (Element (e, es)) =
          let val (t, ty) = tm_of vs e
          in case lookup types ty of
              SOME (Array_Type (_, elty)) =>
                (t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es), elty)
            | _ => error (ty ^ " is not an array type")
          end

      | tm_of vs (Update (e, es, e')) =
          let val (t, ty) = tm_of vs e
          in case lookup types ty of
              SOME (Array_Type (idxtys, elty)) =>
                let
                  val T = foldr1 HOLogic.mk_prodT
                    (map (mk_type thy prfx) idxtys);
                  val U = mk_type thy prfx elty;
                in
                  (\<^Const>\<open>fun_upd T U\<close> $ t $
                    foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es) $ fst (tm_of vs e'),
                   ty)
                end
            | _ => error (ty ^ " is not an array type")
          end

      | tm_of vs (Record (s, flds)) =
          let
            val (T, cmap) = mk_type' thy prfx s;
            val {extension = (ext_name, _), fields, ...} =
              (case get_record_info thy T of
                 NONE => error (s ^ " is not a record type")
               | SOME info => info);
            val flds' = map (apsnd (tm_of vs)) flds;
            val fnames = fields |> invert_map cmap |>
              map (Long_Name.base_name o fst);
            val fnames' = map fst flds;
            val (fvals, ftys) = split_list (map (fn s' =>
              case AList.lookup lcase_eq flds' s' of
                SOME fval_ty => fval_ty
              | NONE => error ("Field " ^ s' ^ " missing in record " ^ s))
                  fnames);
            val _ = (case subtract lcase_eq fnames fnames' of
                [] => ()
              | xs => error ("Extra field(s) " ^ commas xs ^
                  " in record " ^ s));
            val _ = (case duplicates (op =) fnames' of
                [] => ()
              | xs => error ("Duplicate field(s) " ^ commas xs ^
                  " in record " ^ s))
          in
            (list_comb
               (Const (ext_name,
                  map (mk_type thy prfx) ftys @ [HOLogic.unitT] ---> T),
                fvals @ [HOLogic.unit]),
             s)
          end

      | tm_of vs (Array (s, default, assocs)) =
          (case lookup types s of
             SOME (Array_Type (idxtys, elty)) =>
               let
                 val Ts = map (mk_type thy prfx) idxtys;
                 val T = foldr1 HOLogic.mk_prodT Ts;
                 val U = mk_type thy prfx elty;
                 fun mk_idx' T (e, NONE) = HOLogic.mk_set T [fst (tm_of vs e)]
                   | mk_idx' T (e, SOME e') =
                      \<^Const>\<open>atLeastAtMost T for \<open>fst (tm_of vs e)\<close> \<open>fst (tm_of vs e')\\;
                 fun mk_idx idx =
                   if length Ts <> length idx then
                     error ("Arity mismatch in construction of array " ^ s)
                   else foldr1 mk_times (map2 mk_idx' Ts idx);
                 fun mk_upd (idxs, e) t =
                   if length idxs = 1 andalso forall (is_none o snd) (hd idxs)
                   then
                     \<^Const>\<open>fun_upd T U\<close> $ t $
                       foldl1 HOLogic.mk_prod
                         (map (fst o tm_of vs o fst) (hd idxs)) $
                       fst (tm_of vs e)
                   else
                     \<^Const>\<open>fun_upds T U\<close> $ t $
                       foldl1 (HOLogic.mk_binop \<^const_name>\<open>sup\<close>)
                         (map mk_idx idxs) $
                       fst (tm_of vs e)
               in
                 (fold mk_upd assocs
                    (case default of
                       SOME e => Abs ("x", T, fst (tm_of vs e))
                     | NONE => \<^Const>\<open>undefined \<open>T --> U\<close>\<close>),
                  s)
               end
           | _ => error (s ^ " is not an array type"))

  in tm_of end;

fun term_of_rule thy prfx types pfuns ids rule =
  let val tm_of = fst o term_of_expr thy prfx types pfuns ids
  in case rule of
      Inference_Rule (es, e) => Logic.list_implies
        (map (HOLogic.mk_Trueprop o tm_of) es, HOLogic.mk_Trueprop (tm_of e))
    | Substitution_Rule (es, e, e') => Logic.list_implies
        (map (HOLogic.mk_Trueprop o tm_of) es,
         HOLogic.mk_Trueprop (HOLogic.mk_eq (tm_of e, tm_of e')))
  end;

val builtin = Symtab.make (map (rpair ())
  ["->", "<->", "or", "and", "not", "=", "<>", "<", ">", "<=", ">=",
   "+", "-", "*", "/", "div", "mod", "**"]);

fun complex_expr (Number _) = false
  | complex_expr (Ident _) = false
  | complex_expr (Funct (s, es)) =
      not (Symtab.defined builtin s) orelse exists complex_expr es
  | complex_expr (Quantifier (_, _, _, e)) = complex_expr e
  | complex_expr _ = true;

fun complex_rule (Inference_Rule (es, e)) =
      complex_expr e orelse exists complex_expr es
  | complex_rule (Substitution_Rule (es, e, e')) =
      complex_expr e orelse complex_expr e' orelse
      exists complex_expr es;

val is_pfun =
  Symtab.defined builtin orf
  can (unprefix "fld_") orf can (unprefix "upf_") orf
  can (unsuffix "__pos") orf can (unsuffix "__val") orf
  equal "succ" orf equal "pred";

fun fold_opt f = the_default I o Option.map f;
fun fold_pair f g (x, y) = f x #> g y;

fun fold_expr f g (Funct (s, es)) = f s #> fold (fold_expr f g) es
  | fold_expr f g (Ident s) = g s
  | fold_expr f g (Number _) = I
  | fold_expr f g (Quantifier (_, _, _, e)) = fold_expr f g e
  | fold_expr f g (Element (e, es)) =
      fold_expr f g e #> fold (fold_expr f g) es
  | fold_expr f g (Update (e, es, e')) =
      fold_expr f g e #> fold (fold_expr f g) es #> fold_expr f g e'
  | fold_expr f g (Record (_, flds)) = fold (fold_expr f g o snd) flds
  | fold_expr f g (Array (_, default, assocs)) =
      fold_opt (fold_expr f g) default #>
      fold (fold_pair
        (fold (fold (fold_pair
          (fold_expr f g) (fold_opt (fold_expr f g)))))
        (fold_expr f g)) assocs;

fun add_expr_pfuns funs = fold_expr
  (fn s => if is_pfun s then I else insert (op =) s)
  (fn s => if is_none (lookup funs s) then I else insert (op =) s);

val add_expr_idents = fold_expr (K I) (insert (op =));

fun pfun_type thy prfx (argtys, resty) =
  map (mk_type thy prfx) argtys ---> mk_type thy prfx resty;

fun check_pfun_type thy prfx s t optty1 optty2 =
  let
    val T = fastype_of t;
    fun check ty =
      let val U = pfun_type thy prfx ty
      in
        T = U orelse
        error ("Type\n" ^
          Syntax.string_of_typ_global thy T ^
          "\nof function " ^
          Syntax.string_of_term_global thy t ^
          " associated with proof function " ^ s ^
          "\ndoes not match declared type\n" ^
          Syntax.string_of_typ_global thy U)
      end
  in (Option.map check optty1; Option.map check optty2; ()) end;

fun upd_option x y = if is_some x then x else y;

fun check_pfuns_types thy prfx funs =
  Symtab.map (fn s => fn (optty, t) =>
   let val optty' = lookup funs (unprefix_pfun prfx s)
   in
     (check_pfun_type thy prfx s t optty optty';
      (NONE |> upd_option optty |> upd_option optty', t))
   end);

(** the VC store **)

fun pp_vcs msg vcs = Pretty.big_list msg (map (Pretty.str o fst) vcs);

fun pp_open_vcs [] = Pretty.str "All verification conditions have been proved."
  | pp_open_vcs vcs = pp_vcs
      "The following verification conditions remain to be proved:" vcs;

fun partition_vcs vcs = VCtab.fold_rev
  (fn (name, (trace, SOME thms, ps, cs)) =>
        apfst (cons (name, (trace, thms, ps, cs)))
    | (name, (trace, NONE, ps, cs)) =>
        apsnd (cons (name, (trace, ps, cs))))
  vcs ([], []);

fun insert_break prt = Pretty.block0 [Pretty.fbrk, prt];

fun print_open_vcs f vcs =
  (Pretty.writeln (f (pp_open_vcs (snd (partition_vcs vcs)))); vcs);

fun set_env ctxt defs types funs ids vcs path prefix thy = VCs.map (fn
    {pfuns, type_map, env = NONE} =>
      {pfuns = pfuns,
       type_map = type_map,
       env = SOME
         {ctxt = ctxt, defs = defs, types = types, funs = funs,
          pfuns = check_pfuns_types thy prefix funs pfuns,
          ids = ids, proving = false, vcs = print_open_vcs I vcs, path = path,
          prefix = prefix}}
  | _ => err_unfinished ()) thy;

fun mk_pat s = (case Int.fromString s of
    SOME i => [HOLogic.mk_Trueprop (Var (("C", i), HOLogic.boolT))]
  | NONE => error ("Bad conclusion identifier: C" ^ s));

fun mk_vc thy prfx types pfuns ids name_concl (tr, proved, ps, cs) =
  let val prop_of =
    HOLogic.mk_Trueprop o fst o term_of_expr thy prfx types pfuns ids
  in
    (tr, proved,
     Element.Assumes (map (fn (s', e) =>
       ((Binding.name ("H" ^ s'), []), [(prop_of e, [])])) ps),
     Element.Shows (map (fn (s', e) =>
       (if name_concl then (Binding.name ("C" ^ s'), [])
        else Binding.empty_atts,
        [(prop_of e, mk_pat s')])) cs))
  end;

fun fold_vcs f vcs =
  VCtab.fold (fn (_, (_, _, ps, cs)) => fold f ps #> fold f cs) vcs;

fun pfuns_of_vcs prfx funs pfuns vcs =
  fold_vcs (add_expr_pfuns funs o snd) vcs [] |>
  filter (is_none o lookup_prfx prfx pfuns);

fun declare_missing_pfuns thy prfx funs pfuns vcs (tab, ctxt) =
  let
    val (fs, (tys, Ts)) =
      pfuns_of_vcs prfx funs pfuns vcs |>
      map_filter (fn s => lookup funs s |>
        Option.map (fn ty => (s, (SOME ty, pfun_type thy prfx ty)))) |>
      split_list ||> split_list;
    val (fs', ctxt') = fold_map Name.variant fs ctxt
  in
    (fold Symtab.update_new (fs ~~ (tys ~~ map Free (fs' ~~ Ts))) pfuns,
     Element.Fixes (map2 (fn s => fn T =>
       (Binding.name s, SOME T, NoSyn)) fs' Ts),
     (tab, ctxt'))
  end;

fun map_pfuns f {pfuns, type_map, env} =
  {pfuns = f pfuns, type_map = type_map, env = env}

fun map_pfuns_env f {pfuns, type_map,
      env = SOME {ctxt, defs, types, funs, pfuns = pfuns_env,
        ids, proving, vcs, path, prefix}} =
  if proving then err_unfinished ()
  else
    {pfuns = pfuns, type_map = type_map,
     env = SOME {ctxt = ctxt, defs = defs, types = types, funs = funs,
       pfuns = f pfuns_env, ids = ids, proving = false, vcs = vcs,
       path = path, prefix = prefix}};

fun add_proof_fun prep (s, (optty, raw_t)) thy =
  VCs.map (fn data as {env, ...} =>
    let
      val (optty', prfx, map_pf) = (case env of
          SOME {funs, prefix, ...} =>
            (lookup funs (unprefix_pfun prefix s),
             prefix, map_pfuns_env)
        | NONE => (NONE, "", map_pfuns));
      val optty'' = NONE |> upd_option optty |> upd_option optty';
      val t = prep (Option.map (pfun_type thy prfx) optty'') raw_t;
      val _ = (case fold_aterms (fn u =>
          if is_Var u orelse is_Free u then insert (op =) u else I) t [] of
          [] => ()
        | ts => error ("Term\n" ^ Syntax.string_of_term_global thy t ^
            "\nto be associated with proof function " ^ s ^
            " contains free variable(s) " ^
            commas (map (Syntax.string_of_term_global thy) ts)));
    in
      (check_pfun_type thy prfx s t optty optty';
       if is_some optty'' orelse is_none env then
         map_pf (Symtab.update_new (s, (optty'', t))) data
           handle Symtab.DUP _ => error ("Proof function " ^ s ^
             " already associated with function")
       else error ("Undeclared proof function " ^ s))
    end) thy;

fun check_mapping _ _ [] _ = ()
  | check_mapping err s cmap cs =
      (case duplicates (op = o apply2 fst) cmap of
         [] => (case duplicates (op = o apply2 snd) cmap of
             [] => (case subtract (op = o apsnd snd) cs cmap of
                 [] => (case subtract (op = o apfst snd) cmap cs of
                     [] => ()
                   | zs => err ("has extra " ^ s ^ "(s) " ^ commas zs))
               | zs => err ("does not have " ^ s ^ "(s) " ^
                   commas (map snd zs)))
           | zs => error ("Several SPARK names are mapped to " ^
               commas (map snd zs)))
       | zs => error ("The SPARK names " ^ commas (map fst zs) ^
           " are mapped to more than one name"));

fun add_type (s, (T as Type (tyname, Ts), cmap)) thy =
      let val cmap' = map (apsnd (Sign.intern_const thy)) cmap
      in
        thy |>
        VCs.map (fn
            {env = SOME _, ...} => err_unfinished ()
          | {pfuns, type_map, env} =>
              {pfuns = pfuns,
               type_map = Symtab.update_new (s, (T, cmap')) type_map,
               env = env}
                handle Symtab.DUP _ => error ("SPARK type " ^ s ^
                  " already associated with type")) |>
        (fn thy' =>
           case BNF_LFP_Compat.get_constrs thy' tyname of
             NONE => (case get_record_info thy' T of
               NONE => thy'
             | SOME {fields, ...} =>
                 (check_mapping (assoc_ty_err thy' T s) "field"
                    cmap' (map fst fields);
                  thy'))
           | SOME cs =>
               if null Ts then
                 (map
                    (fn (_, Type (_, [])) => ()
                      | (cname, _) => assoc_ty_err thy' T s
                          ("has illegal constructor " ^
                           Long_Name.base_name cname)) cs;
                  check_mapping (assoc_ty_err thy' T s) "constructor"
                    cmap' (map fst cs);
                  add_enum_type s tyname thy')
               else assoc_ty_err thy' T s "is illegal")
      end
  | add_type (s, (T, _)) thy = assoc_ty_err thy T s "is illegal";

val is_closed = is_none o #env o VCs.get;

fun lookup_vc thy name_concl name =
  (case VCs.get thy of
    {env = SOME {vcs, types, funs, pfuns, ids, ctxt, prefix, ...}, ...} =>
      (case VCtab.lookup vcs name of
         SOME vc =>
           let val (pfuns', ctxt', ids') =
             declare_missing_pfuns thy prefix funs pfuns vcs ids
           in
             SOME (ctxt @ [ctxt'],
               mk_vc thy prefix types pfuns' ids' name_concl vc)
           end
       | NONE => NONE)
  | _ => NONE);

fun get_vcs thy name_concl = (case VCs.get thy of
    {env = SOME {vcs, types, funs, pfuns, ids, ctxt, defs, prefix, ...}, ...} =>
      let val (pfuns', ctxt', ids') =
        declare_missing_pfuns thy prefix funs pfuns vcs ids
      in
        (ctxt @ [ctxt'], defs,
         VCtab.dest vcs |>
         map (apsnd (mk_vc thy prefix types pfuns' ids' name_concl)))
      end
  | _ => ([], [], []));

fun mark_proved name thms = VCs.map (fn
    {pfuns, type_map,
     env = SOME {ctxt, defs, types, funs, pfuns = pfuns_env,
        ids, vcs, path, prefix, ...}} =>
      {pfuns = pfuns,
       type_map = type_map,
       env = SOME {ctxt = ctxt, defs = defs,
         types = types, funs = funs, pfuns = pfuns_env,
         ids = ids,
         proving = true,
         vcs = print_open_vcs insert_break (VCtab.map_entry name
           (fn (trace, _, ps, cs) => (trace, SOME thms, ps, cs)) vcs),
         path = path,
         prefix = prefix}}
  | x => x);

fun close incomplete thy =
  thy |> VCs.map (fn {pfuns, type_map, env} =>
    (case env of
      NONE => error "No SPARK environment is currently open"
    | SOME {vcs, path, ...} =>
        let
          val (proved, unproved) = partition_vcs vcs;
          val _ = Thm.consolidate (maps (#2 o snd) proved);
          val (proved', proved'') =
            List.partition (fn (_, (_, thms, _, _)) => Thm_Deps.has_skip_proof thms) proved;
          val _ =
            if null unproved then ()
            else (if incomplete then warning else error) (Pretty.string_of (pp_open_vcs unproved));
          val _ =
            if null proved' then ()
            else warning (Pretty.string_of (pp_vcs
             "The following VCs are not marked as proved \
             \because their proofs contain oracles:" proved'));
          val prv_path = Path.ext "prv" path;
          val _ =
            Export.export thy (Path.binding (prv_path, Position.none))
              (proved'' |> map (fn (s, _) =>
                XML.Text (snd (strip_number s) ^
                  " -- proved by " ^ Isabelle_System.identification () ^ "\n")));
        in {pfuns = pfuns, type_map = type_map, env = NONE} end))
  |> Sign.parent_path;

(** set up verification conditions **)

fun partition_opt f =
  let
    fun part ys zs [] = (rev ys, rev zs)
      | part ys zs (x :: xs) = (case f x of
            SOME y => part (y :: ys) zs xs
          | NONE => part ys (x :: zs) xs)
  in part [] [] end;

fun dest_def (id, (Substitution_Rule ([], Ident s, rhs))) = SOME (id, (s, rhs))
  | dest_def _ = NONE;

fun mk_rulename (s, i) = Binding.name (s ^ string_of_int i);

fun add_const prfx (s, ty) ((tab, ctxt), thy) =
  let
    val T = mk_type thy prfx ty;
    val b = Binding.name s;
    val c = Const (Sign.full_name thy b, T)
  in
    (c,
     ((Symtab.update (s, (c, ty)) tab, Name.declare s ctxt),
      Sign.add_consts [(b, T, NoSyn)] thy))
  end;

fun add_def prfx types pfuns consts (id, (s, e)) (ids as (tab, ctxt), thy) =
  (case lookup consts s of
    SOME ty =>
      let
        val (t, ty') = term_of_expr thy prfx types pfuns ids e;
        val T = mk_type thy prfx ty;
        val T' = mk_type thy prfx ty';
        val _ = T = T' orelse
          error ("Declared type " ^ ty ^ " of " ^ s ^
            "\ndoes not match type " ^ ty' ^ " in definition");
        val id' = mk_rulename id;
        val ((t', (_, th)), lthy') = Named_Target.theory_init thy
          |> Specification.definition NONE [] []
            ((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq (Free (s, T), t)));
        val phi =
          Proof_Context.export_morphism lthy'
            (Proof_Context.init_global (Proof_Context.theory_of lthy'));
      in
        ((id', Morphism.thm phi th),
          ((Symtab.update (s, (Morphism.term phi t', ty)) tab, Name.declare s ctxt),
            Local_Theory.exit_global lthy'))
       end
  | NONE => error ("Undeclared constant " ^ s));

fun add_var prfx (s, ty) (ids, thy) =
  let val ([Free p], ids') = mk_variables thy prfx [s] ty ids
  in (p, (ids', thy)) end;

fun add_init_vars prfx vcs (ids_thy as ((tab, _), _)) =
  fold_map (add_var prfx)
    (map_filter
       (fn s => case try (unsuffix "~") s of
          SOME s' => (case Symtab.lookup tab s' of
            SOME (_, ty) => SOME (s, ty)
          | NONE => error ("Undeclared identifier " ^ s'))
        | NONE => NONE)
       (fold_vcs (add_expr_idents o snd) vcs []))
    ids_thy;

fun is_trivial_vc ([], [(_, Ident "true")]) = true
  | is_trivial_vc _ = false;

fun rulenames rules = commas
  (map (fn ((s, i), _) => s ^ "(" ^ string_of_int i ^ ")") rules);

(* sort definitions according to their dependency *)
fun sort_defs _ _ _ _ [] sdefs = rev sdefs
  | sort_defs prfx funs pfuns consts defs sdefs =
      (case find_first (fn (_, (_, e)) =>
         forall (is_some o lookup_prfx prfx pfuns)
           (add_expr_pfuns funs e []) andalso
         forall (fn id =>
           member (fn (s, (_, (s', _))) => s = s') sdefs id orelse
           consts id)
             (add_expr_idents e [])) defs of
         SOME d => sort_defs prfx funs pfuns consts
           (remove (op =) d defs) (d :: sdefs)
       | NONE => error ("Bad definitions: " ^ rulenames defs));

fun set_vcs ({types, vars, consts, funs} : decls)
      (rules, _) ((_, ident), vcs) path opt_prfx thy =
  let
    val prfx' =
      if opt_prfx = "" then
        space_implode "__" (Long_Name.explode (Long_Name.qualifier ident))
      else opt_prfx;
    val prfx = to_lower prfx';
    val {pfuns, ...} = VCs.get thy;
    val (defs, rules') = partition_opt dest_def rules;
    val consts' =
      subtract (fn ((_, (s, _)), (s', _)) => s = s') defs (items consts);
    (* ignore all complex rules in rls files *)
    val (rules'', other_rules) =
      List.partition (complex_rule o snd) rules';
    val _ = if null rules'' then ()
      else warning ("Ignoring rules: " ^ rulenames rules'');

    val vcs' = VCtab.make (maps (fn (tr, vcs) =>
      map (fn (s, (ps, cs)) => (s, (tr, NONE, ps, cs)))
        (filter_out (is_trivial_vc o snd) vcs)) vcs);

    val _ = (case filter_out (is_some o lookup funs)
        (pfuns_of_vcs prfx funs pfuns vcs') of
        [] => ()
      | fs => error ("Undeclared proof function(s) " ^ commas fs));

    val (((defs', vars''), ivars), (ids, thy')) =
      ((Symtab.empty |>
        Symtab.update ("false", (\<^term>\<open>False\<close>, booleanN)) |>
        Symtab.update ("true", (\<^term>\<open>True\<close>, booleanN)),
        Name.context),
       thy |> Sign.add_path
         ((if prfx' = "" then "" else prfx' ^ "__") ^ Long_Name.base_name ident)) |>
      fold (add_type_def prfx) (items types) |>
      fold (snd oo add_const prfx) consts' |> (fn ids_thy as ((tab, _), _) =>
        ids_thy |>
        fold_map (add_def prfx types pfuns consts)
          (sort_defs prfx funs pfuns (Symtab.defined tab) defs []) ||>>
        fold_map (add_var prfx) (items vars) ||>>
        add_init_vars prfx vcs');

    val ctxt =
      [Element.Fixes (map (fn (s, T) =>
         (Binding.name s, SOME T, NoSyn)) (vars'' @ ivars)),
       Element.Assumes (map (fn (id, rl) =>
         ((mk_rulename id, []),
          [(term_of_rule thy' prfx types pfuns ids rl, [])]))
           other_rules),
       Element.Notes ("", [((Binding.name "defns", []), map (rpair [] o single o snd) defs')])]

  in
    set_env ctxt defs' types funs ids vcs' path prfx thy'
  end;

end;

quality100%

¤ 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.0.11Bemerkung: Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Bot Zugriff

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.