wneuper/isa: src/HOL/SPARK/Tools/spark

     1 (*  Title:      HOL/SPARK/Tools/spark_vcs.ML

     2     Author:     Stefan Berghofer

     3     Copyright:  secunet Security Networks AG

     5 Store for verification conditions generated by SPARK/Ada.

     6 *)

     8 signature SPARK_VCS =

     9 sig

    10   val set_vcs: Fdl_Parser.decls -> Fdl_Parser.rules -> Fdl_Parser.vcs ->

    11     Path.T -> theory -> theory

    12   val add_proof_fun: (typ option -> 'a -> term) ->

    13     string * ((string list * string) option * 'a) ->

    14     theory -> theory

    15   val lookup_vc: theory -> string -> (Element.context_i list *

    16     (string * bool * Element.context_i * Element.statement_i)) option

    17   val get_vcs: theory ->

    18     Element.context_i list * (binding * thm) list *

    19     (string * (string * bool * Element.context_i * Element.statement_i)) list

    20   val mark_proved: string -> theory -> theory

    21   val close: theory -> theory

    22   val is_closed: theory -> bool

    23 end;

    25 structure SPARK_VCs: SPARK_VCS =

    26 struct

    28 open Fdl_Parser;

    31 (** utilities **)

    33 fun mk_unop s t =

    34   let val T = fastype_of t

    35   in Const (s, T --> T) $ t end;

    37 fun mk_times (t, u) =

    38   let

    39     val setT = fastype_of t;

    40     val T = HOLogic.dest_setT setT;

    41     val U = HOLogic.dest_setT (fastype_of u)

    42   in

    43     Const (@{const_name Sigma}, setT --> (T --> HOLogic.mk_setT U) -->

    44       HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u)

    45   end;

    47 fun mk_type _ "integer" = HOLogic.intT

    48   | mk_type _ "boolean" = HOLogic.boolT

    49   | mk_type thy ty = Syntax.check_typ (ProofContext.init_global thy)

    50       (Type (Sign.full_name thy (Binding.name ty), []));

    52 val booleanN = "boolean";

    53 val integerN = "integer";

    55 fun mk_qual_name thy s s' =

    56   Sign.full_name thy (Binding.qualify true s (Binding.name s'));

    58 fun define_overloaded (def_name, eq) lthy =

    59   let

    60     val ((c, _), rhs) = eq |> Syntax.check_term lthy |>

    61       Logic.dest_equals |>> dest_Free;

    62     val ((_, (_, thm)), lthy') = Local_Theory.define

    63       ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs)) lthy

    64     val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy');

    65     val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm

    66   in (thm', lthy') end;

    68 fun strip_underscores s =

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

    71 fun strip_tilde s =

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

    74 val mangle_name = strip_underscores #> strip_tilde;

    76 fun mk_variables thy xs ty (tab, ctxt) =

    77   let

    78     val T = mk_type thy ty;

    79     val (ys, ctxt') = Name.variants (map mangle_name xs) ctxt;

    80     val zs = map (Free o rpair T) ys;

    81   in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end;

    84 (** generate properties of enumeration types **)

    86 fun add_enum_type tyname els (tab, ctxt) thy =

    87   let

    88     val tyb = Binding.name tyname;

    89     val tyname' = Sign.full_name thy tyb;

    90     val T = Type (tyname', []);

    91     val case_name = mk_qual_name thy tyname (tyname ^ "_case");

    92     val cs = map (fn s => Const (mk_qual_name thy tyname s, T)) els;

    93     val k = length els;

    94     val p = Const (@{const_name pos}, T --> HOLogic.intT);

    95     val v = Const (@{const_name val}, HOLogic.intT --> T);

    96     val card = Const (@{const_name card},

    97       HOLogic.mk_setT T --> HOLogic.natT) $ HOLogic.mk_UNIV T;

    99     fun mk_binrel_def s f = Logic.mk_equals

   100       (Const (s, T --> T --> HOLogic.boolT),

   101        Abs ("x", T, Abs ("y", T,

   102          Const (s, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $

   103            (f $ Bound 1) $ (f $ Bound 0))));

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

   106       Datatype.add_datatype {strict = true, quiet = true} [tyname]

   107         [([], tyb, NoSyn,

   108           map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |>

   110       Class.instantiation ([tyname'], [], @{sort enum}) |>

   112       define_overloaded ("pos_" ^ tyname ^ "_def", Logic.mk_equals

   113         (p,

   114          list_comb (Const (case_name, replicate k HOLogic.intT @

   115              [T] ---> HOLogic.intT),

   116            map (HOLogic.mk_number HOLogic.intT) (0 upto k - 1)))) ||>>

   118       define_overloaded ("less_eq_" ^ tyname ^ "_def",

   119         mk_binrel_def @{const_name less_eq} p) ||>>

   120       define_overloaded ("less_" ^ tyname ^ "_def",

   121         mk_binrel_def @{const_name less} p);

   123     val UNIV_eq = Goal.prove lthy [] []

   124       (HOLogic.mk_Trueprop (HOLogic.mk_eq

   125          (HOLogic.mk_UNIV T, HOLogic.mk_set T cs)))

   126       (fn _ =>

   127          rtac @{thm subset_antisym} 1 THEN

   128          rtac @{thm subsetI} 1 THEN

   129          Datatype_Aux.exh_tac (K (#exhaust (Datatype_Data.the_info

   130            (ProofContext.theory_of lthy) tyname'))) 1 THEN

   131          ALLGOALS (asm_full_simp_tac (simpset_of lthy)));

   133     val finite_UNIV = Goal.prove lthy [] []

   134       (HOLogic.mk_Trueprop (Const (@{const_name finite},

   135          HOLogic.mk_setT T --> HOLogic.boolT) $ HOLogic.mk_UNIV T))

   136       (fn _ => simp_tac (simpset_of lthy addsimps [UNIV_eq]) 1);

   138     val card_UNIV = Goal.prove lthy [] []

   139       (HOLogic.mk_Trueprop (HOLogic.mk_eq

   140          (card, HOLogic.mk_number HOLogic.natT k)))

   141       (fn _ => simp_tac (simpset_of lthy addsimps [UNIV_eq]) 1);

   143     val range_pos = Goal.prove lthy [] []

   144       (HOLogic.mk_Trueprop (HOLogic.mk_eq

   145          (Const (@{const_name image}, (T --> HOLogic.intT) -->

   146             HOLogic.mk_setT T --> HOLogic.mk_setT HOLogic.intT) $

   147               p $ HOLogic.mk_UNIV T,

   148           Const (@{const_name atLeastLessThan}, HOLogic.intT -->

   149             HOLogic.intT --> HOLogic.mk_setT HOLogic.intT) $

   150               HOLogic.mk_number HOLogic.intT 0 $

   151               (@{term int} $ card))))

   152       (fn _ =>

   153          simp_tac (simpset_of lthy addsimps [card_UNIV]) 1 THEN

   154          simp_tac (simpset_of lthy addsimps [UNIV_eq, def1]) 1 THEN

   155          rtac @{thm subset_antisym} 1 THEN

   156          simp_tac (simpset_of lthy) 1 THEN

   157          rtac @{thm subsetI} 1 THEN

   158          asm_full_simp_tac (simpset_of lthy addsimps @{thms interval_expand}

   159            delsimps @{thms atLeastLessThan_iff}) 1);

   161     val lthy' =

   162       Class.prove_instantiation_instance (fn _ =>

   163         Class.intro_classes_tac [] THEN

   164         rtac finite_UNIV 1 THEN

   165         rtac range_pos 1 THEN

   166         simp_tac (HOL_basic_ss addsimps [def3]) 1 THEN

   167         simp_tac (HOL_basic_ss addsimps [def2]) 1) lthy;

   169     val (pos_eqs, val_eqs) = split_list (map_index (fn (i, c) =>

   170       let

   171         val n = HOLogic.mk_number HOLogic.intT i;

   172         val th = Goal.prove lthy' [] []

   173           (HOLogic.mk_Trueprop (HOLogic.mk_eq (p $ c, n)))

   174           (fn _ => simp_tac (simpset_of lthy' addsimps [def1]) 1);

   175         val th' = Goal.prove lthy' [] []

   176           (HOLogic.mk_Trueprop (HOLogic.mk_eq (v $ n, c)))

   177           (fn _ =>

   178              rtac (@{thm inj_pos} RS @{thm injD}) 1 THEN

   179              simp_tac (simpset_of lthy' addsimps

   180                [@{thm pos_val}, range_pos, card_UNIV, th]) 1)

   181       in (th, th') end) cs);

   183     val first_el = Goal.prove lthy' [] []

   184       (HOLogic.mk_Trueprop (HOLogic.mk_eq

   185          (Const (@{const_name first_el}, T), hd cs)))

   186       (fn _ => simp_tac (simpset_of lthy' addsimps

   187          [@{thm first_el_def}, hd val_eqs]) 1);

   189     val last_el = Goal.prove lthy' [] []

   190       (HOLogic.mk_Trueprop (HOLogic.mk_eq

   191          (Const (@{const_name last_el}, T), List.last cs)))

   192       (fn _ => simp_tac (simpset_of lthy' addsimps

   193          [@{thm last_el_def}, List.last val_eqs, card_UNIV]) 1);

   195     val simp_att = [Attrib.internal (K Simplifier.simp_add)]

   197   in

   198     ((fold (Symtab.update_new o apsnd (rpair tyname)) (els ~~ cs) tab,

   199       fold Name.declare els ctxt),

   200      lthy' |>

   201      Local_Theory.note

   202        ((Binding.name (tyname ^ "_card_UNIV"), simp_att), [card_UNIV]) ||>>

   203      Local_Theory.note

   204        ((Binding.name (tyname ^ "_pos"), simp_att), pos_eqs) ||>>

   205      Local_Theory.note

   206        ((Binding.name (tyname ^ "_val"), simp_att), val_eqs) ||>>

   207      Local_Theory.note

   208        ((Binding.name (tyname ^ "_first_el"), simp_att), [first_el]) ||>>

   209      Local_Theory.note

   210        ((Binding.name (tyname ^ "_last_el"), simp_att), [last_el]) |> snd |>

   211      Local_Theory.exit_global)

   212   end;

   215 fun add_type_def (s, Basic_Type ty) (ids, thy) =

   216       (ids,

   217        Typedecl.abbrev_global (Binding.name s, [], NoSyn)

   218          (mk_type thy ty) thy |> snd)

   220   | add_type_def (s, Enum_Type els) (ids, thy) = add_enum_type s els ids thy

   222   | add_type_def (s, Array_Type (argtys, resty)) (ids, thy) =

   223       (ids,

   224        Typedecl.abbrev_global (Binding.name s, [], NoSyn)

   225          (foldr1 HOLogic.mk_prodT (map (mk_type thy) argtys) -->

   226             mk_type thy resty) thy |> snd)

   228   | add_type_def (s, Record_Type fldtys) (ids, thy) =

   229       (ids,

   230        Record.add_record true ([], Binding.name s) NONE

   231          (maps (fn (flds, ty) =>

   232             let val T = mk_type thy ty

   233             in map (fn fld => (Binding.name fld, T, NoSyn)) flds

   234             end) fldtys) thy)

   236   | add_type_def (s, Pending_Type) (ids, thy) =

   237       (ids, Typedecl.typedecl_global (Binding.name s, [], NoSyn) thy |> snd);

   240 fun term_of_expr thy types funs pfuns =

   241   let

   242     fun tm_of vs (Funct ("->", [e, e'])) =

   243           (HOLogic.mk_imp (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

   245       | tm_of vs (Funct ("<->", [e, e'])) =

   246           (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

   248       | tm_of vs (Funct ("or", [e, e'])) =

   249           (HOLogic.mk_disj (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

   251       | tm_of vs (Funct ("and", [e, e'])) =

   252           (HOLogic.mk_conj (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

   254       | tm_of vs (Funct ("not", [e])) =

   255           (HOLogic.mk_not (fst (tm_of vs e)), booleanN)

   257       | tm_of vs (Funct ("=", [e, e'])) =

   258           (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

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

   261           (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e'))), booleanN)

   263       | tm_of vs (Funct ("<", [e, e'])) = (HOLogic.mk_binrel @{const_name less}

   264           (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

   266       | tm_of vs (Funct (">", [e, e'])) = (HOLogic.mk_binrel @{const_name less}

   267           (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)

   269       | tm_of vs (Funct ("<=", [e, e'])) = (HOLogic.mk_binrel @{const_name less_eq}

   270           (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

   272       | tm_of vs (Funct (">=", [e, e'])) = (HOLogic.mk_binrel @{const_name less_eq}

   273           (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)

   275       | tm_of vs (Funct ("+", [e, e'])) = (HOLogic.mk_binop @{const_name plus}

   276           (fst (tm_of vs e), fst (tm_of vs e')), integerN)

   278       | tm_of vs (Funct ("-", [e, e'])) = (HOLogic.mk_binop @{const_name minus}

   279           (fst (tm_of vs e), fst (tm_of vs e')), integerN)

   281       | tm_of vs (Funct ("*", [e, e'])) = (HOLogic.mk_binop @{const_name times}

   282           (fst (tm_of vs e), fst (tm_of vs e')), integerN)

   284       | tm_of vs (Funct ("/", [e, e'])) = (HOLogic.mk_binop @{const_name divide}

   285           (fst (tm_of vs e), fst (tm_of vs e')), integerN)

   287       | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop @{const_name sdiv}

   288           (fst (tm_of vs e), fst (tm_of vs e')), integerN)

   290       | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop @{const_name smod}

   291           (fst (tm_of vs e), fst (tm_of vs e')), integerN)

   293       | tm_of vs (Funct ("-", [e])) =

   294           (mk_unop @{const_name uminus} (fst (tm_of vs e)), integerN)

   296       | tm_of vs (Funct ("**", [e, e'])) =

   297           (Const (@{const_name power}, HOLogic.intT --> HOLogic.natT -->

   298              HOLogic.intT) $ fst (tm_of vs e) $

   299                (@{const nat} $ fst (tm_of vs e')), integerN)

   301       | tm_of (tab, _) (Ident s) =

   302           (case Symtab.lookup tab s of

   303              SOME t_ty => t_ty

   304            | NONE => error ("Undeclared identifier " ^ s))

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

   308       | tm_of vs (Quantifier (s, xs, ty, e)) =

   309           let

   310             val (ys, vs') = mk_variables thy xs ty vs;

   311             val q = (case s of

   312                 "for_all" => HOLogic.mk_all

   313               | "for_some" => HOLogic.mk_exists)

   314           in

   315             (fold_rev (fn Free (x, T) => fn t => q (x, T, t))

   316                ys (fst (tm_of vs' e)),

   317              booleanN)

   318           end

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

   322           (* record field selection *)

   323           (case try (unprefix "fld_") s of

   324              SOME fname => (case es of

   325                [e] =>

   326                  let val (t, rcdty) = tm_of vs e

   327                  in case lookup types rcdty of

   328                      SOME (Record_Type fldtys) =>

   329                        (case get_first (fn (flds, fldty) =>

   330                             if member (op =) flds fname then SOME fldty

   331                             else NONE) fldtys of

   332                           SOME fldty =>

   333                             (Const (mk_qual_name thy rcdty fname,

   334                                mk_type thy rcdty --> mk_type thy fldty) $ t,

   335                              fldty)

   336                         | NONE => error ("Record " ^ rcdty ^

   337                             " has no field named " ^ fname))

   338                    | _ => error (rcdty ^ " is not a record type")

   339                  end

   340              | _ => error ("Function " ^ s ^ " expects one argument"))

   341            | NONE =>

   343           (* record field update *)

   344           (case try (unprefix "upf_") s of

   345              SOME fname => (case es of

   346                [e, e'] =>

   347                  let

   348                    val (t, rcdty) = tm_of vs e;

   349                    val rT = mk_type thy rcdty;

   350                    val (u, fldty) = tm_of vs e';

   351                    val fT = mk_type thy fldty

   352                  in case lookup types rcdty of

   353                      SOME (Record_Type fldtys) =>

   354                        (case get_first (fn (flds, fldty) =>

   355                             if member (op =) flds fname then SOME fldty

   356                             else NONE) fldtys of

   357                           SOME fldty' =>

   358                             if fldty = fldty' then

   359                               (Const (mk_qual_name thy rcdty (fname ^ "_update"),

   360                                  (fT --> fT) --> rT --> rT) $

   361                                    Abs ("x", fT, u) $ t,

   362                                rcdty)

   363                             else error ("Type " ^ fldty ^

   364                               " does not match type " ^ fldty' ^ " of field " ^

   365                               fname)

   366                         | NONE => error ("Record " ^ rcdty ^

   367                             " has no field named " ^ fname))

   368                    | _ => error (rcdty ^ " is not a record type")

   369                  end

   370              | _ => error ("Function " ^ s ^ " expects two arguments"))

   371            | NONE =>

   373           (* enumeration type to integer *)

   374           (case try (unsuffix "__pos") s of

   375              SOME tyname => (case es of

   376                [e] => (Const (@{const_name pos},

   377                  mk_type thy tyname --> HOLogic.intT) $ fst (tm_of vs e), integerN)

   378              | _ => error ("Function " ^ s ^ " expects one argument"))

   379            | NONE =>

   381           (* integer to enumeration type *)

   382           (case try (unsuffix "__val") s of

   383              SOME tyname => (case es of

   384                [e] => (Const (@{const_name val},

   385                  HOLogic.intT --> mk_type thy tyname) $ fst (tm_of vs e), tyname)

   386              | _ => error ("Function " ^ s ^ " expects one argument"))

   387            | NONE =>

   389           (* successor / predecessor of enumeration type element *)

   390           if s = "succ" orelse s = "pred" then (case es of

   391               [e] =>

   392                 let

   393                   val (t, tyname) = tm_of vs e;

   394                   val T = mk_type thy tyname

   395                 in (Const

   396                   (if s = "succ" then @{const_name succ}

   397                    else @{const_name pred}, T --> T) $ t, tyname)

   398                 end

   399             | _ => error ("Function " ^ s ^ " expects one argument"))

   401           (* user-defined proof function *)

   402           else

   403             (case Symtab.lookup pfuns s of

   404                SOME (SOME (_, resty), t) =>

   405                  (list_comb (t, map (fst o tm_of vs) es), resty)

   406              | _ => error ("Undeclared proof function " ^ s))))))

   408       | tm_of vs (Element (e, es)) =

   409           let val (t, ty) = tm_of vs e

   410           in case lookup types ty of

   411               SOME (Array_Type (_, elty)) =>

   412                 (t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es), elty)

   413             | _ => error (ty ^ " is not an array type")

   414           end

   416       | tm_of vs (Update (e, es, e')) =

   417           let val (t, ty) = tm_of vs e

   418           in case lookup types ty of

   419               SOME (Array_Type (idxtys, elty)) =>

   420                 let

   421                   val T = foldr1 HOLogic.mk_prodT (map (mk_type thy) idxtys);

   422                   val U = mk_type thy elty;

   423                   val fT = T --> U

   424                 in

   425                   (Const (@{const_name fun_upd}, fT --> T --> U --> fT) $

   426                      t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es) $

   427                        fst (tm_of vs e'),

   428                    ty)

   429                 end

   430             | _ => error (ty ^ " is not an array type")

   431           end

   433       | tm_of vs (Record (s, flds)) =

   434           (case lookup types s of

   435              SOME (Record_Type fldtys) =>

   436                let

   437                  val flds' = map (apsnd (tm_of vs)) flds;

   438                  val fnames = maps fst fldtys;

   439                  val fnames' = map fst flds;

   440                  val (fvals, ftys) = split_list (map (fn s' =>

   441                    case AList.lookup (op =) flds' s' of

   442                      SOME fval_ty => fval_ty

   443                    | NONE => error ("Field " ^ s' ^ " missing in record " ^ s))

   444                        fnames);

   445                  val _ = (case subtract (op =) fnames fnames' of

   446                      [] => ()

   447                    | xs => error ("Extra field(s) " ^ commas xs ^

   448                        " in record " ^ s));

   449                  val _ = (case duplicates (op =) fnames' of

   450                      [] => ()

   451                    | xs => error ("Duplicate field(s) " ^ commas xs ^

   452                        " in record " ^ s))

   453                in

   454                  (list_comb

   455                     (Const (mk_qual_name thy s (s ^ "_ext"),

   456                        map (mk_type thy) ftys @ [HOLogic.unitT] --->

   457                          mk_type thy s),

   458                      fvals @ [HOLogic.unit]),

   459                   s)

   460                end

   461            | _ => error (s ^ " is not a record type"))

   463       | tm_of vs (Array (s, default, assocs)) =

   464           (case lookup types s of

   465              SOME (Array_Type (idxtys, elty)) =>

   466                let

   467                  val Ts = map (mk_type thy) idxtys;

   468                  val T = foldr1 HOLogic.mk_prodT Ts;

   469                  val U = mk_type thy elty;

   470                  fun mk_idx' T (e, NONE) = HOLogic.mk_set T [fst (tm_of vs e)]

   471                    | mk_idx' T (e, SOME e') = Const (@{const_name atLeastAtMost},

   472                        T --> T --> HOLogic.mk_setT T) $

   473                          fst (tm_of vs e) $ fst (tm_of vs e');

   474                  fun mk_idx idx =

   475                    if length Ts <> length idx then

   476                      error ("Arity mismatch in construction of array " ^ s)

   477                    else foldr1 mk_times (map2 mk_idx' Ts idx);

   478                  fun mk_upd (idxs, e) t =

   479                    if length idxs = 1 andalso forall (is_none o snd) (hd idxs)

   480                    then

   481                      Const (@{const_name fun_upd}, (T --> U) -->

   482                          T --> U --> T --> U) $ t $

   483                        foldl1 HOLogic.mk_prod

   484                          (map (fst o tm_of vs o fst) (hd idxs)) $

   485                        fst (tm_of vs e)

   486                    else

   487                      Const (@{const_name fun_upds}, (T --> U) -->

   488                          HOLogic.mk_setT T --> U --> T --> U) $ t $

   489                        foldl1 (HOLogic.mk_binop @{const_name sup})

   490                          (map mk_idx idxs) $

   491                        fst (tm_of vs e)

   492                in

   493                  (fold mk_upd assocs

   494                     (case default of

   495                        SOME e => Abs ("x", T, fst (tm_of vs e))

   496                      | NONE => Const (@{const_name undefined}, T --> U)),

   497                   s)

   498                end

   499            | _ => error (s ^ " is not an array type"))

   501   in tm_of end;

   504 fun term_of_rule thy types funs pfuns ids rule =

   505   let val tm_of = fst o term_of_expr thy types funs pfuns ids

   506   in case rule of

   507       Inference_Rule (es, e) => Logic.list_implies

   508         (map (HOLogic.mk_Trueprop o tm_of) es, HOLogic.mk_Trueprop (tm_of e))

   509     | Substitution_Rule (es, e, e') => Logic.list_implies

   510         (map (HOLogic.mk_Trueprop o tm_of) es,

   511          HOLogic.mk_Trueprop (HOLogic.mk_eq (tm_of e, tm_of e')))

   512   end;

   515 val builtin = Symtab.make (map (rpair ())

   516   ["->", "<->", "or", "and", "not", "=", "<>", "<", ">", "<=", ">=",

   517    "+", "-", "*", "/", "div", "mod", "**"]);

   519 fun complex_expr (Number _) = false

   520   | complex_expr (Ident _) = false

   521   | complex_expr (Funct (s, es)) =

   522       not (Symtab.defined builtin s) orelse exists complex_expr es

   523   | complex_expr (Quantifier (_, _, _, e)) = complex_expr e

   524   | complex_expr _ = true;

   526 fun complex_rule (Inference_Rule (es, e)) =

   527       complex_expr e orelse exists complex_expr es

   528   | complex_rule (Substitution_Rule (es, e, e')) =

   529       complex_expr e orelse complex_expr e' orelse

   530       exists complex_expr es;

   532 val is_pfun =

   533   Symtab.defined builtin orf

   534   can (unprefix "fld_") orf can (unprefix "upf_") orf

   535   can (unsuffix "__pos") orf can (unsuffix "__val") orf

   536   equal "succ" orf equal "pred";

   538 fun fold_opt f = the_default I o Option.map f;

   539 fun fold_pair f g (x, y) = f x #> g y;

   541 fun fold_expr f g (Funct (s, es)) = f s #> fold (fold_expr f g) es

   542   | fold_expr f g (Ident s) = g s

   543   | fold_expr f g (Number _) = I

   544   | fold_expr f g (Quantifier (_, _, _, e)) = fold_expr f g e

   545   | fold_expr f g (Element (e, es)) =

   546       fold_expr f g e #> fold (fold_expr f g) es

   547   | fold_expr f g (Update (e, es, e')) =

   548       fold_expr f g e #> fold (fold_expr f g) es #> fold_expr f g e'

   549   | fold_expr f g (Record (_, flds)) = fold (fold_expr f g o snd) flds

   550   | fold_expr f g (Array (_, default, assocs)) =

   551       fold_opt (fold_expr f g) default #>

   552       fold (fold_pair

   553         (fold (fold (fold_pair

   554           (fold_expr f g) (fold_opt (fold_expr f g)))))

   555         (fold_expr f g)) assocs;

   557 val add_expr_pfuns = fold_expr

   558   (fn s => if is_pfun s then I else insert (op =) s) (K I);

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

   562 fun pfun_type thy (argtys, resty) =

   563   map (mk_type thy) argtys ---> mk_type thy resty;

   565 fun check_pfun_type thy s t optty1 optty2 =

   566   let

   567     val T = fastype_of t;

   568     fun check ty =

   569       let val U = pfun_type thy ty

   570       in

   571         T = U orelse

   572         error ("Type\n" ^

   573           Syntax.string_of_typ_global thy T ^

   574           "\nof function " ^

   575           Syntax.string_of_term_global thy t ^

   576           " associated with proof function " ^ s ^

   577           "\ndoes not match declared type\n" ^

   578           Syntax.string_of_typ_global thy U)

   579       end

   580   in (Option.map check optty1; Option.map check optty2; ()) end;

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

   584 fun check_pfuns_types thy funs =

   585   Symtab.map (fn s => fn (optty, t) =>

   586    let val optty' = lookup funs s

   587    in

   588      (check_pfun_type thy s t optty optty';

   589       (NONE |> upd_option optty |> upd_option optty', t))

   590    end);

   593 (** the VC store **)

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

   597 fun err_vcs names = error (Pretty.string_of

   598   (Pretty.big_list "The following verification conditions have not been proved:"

   599     (map Pretty.str names)))

   601 val strip_number = pairself implode o take_suffix Fdl_Lexer.is_digit o raw_explode;

   603 val name_ord = prod_ord string_ord (option_ord int_ord) o

   604   pairself (strip_number ##> Int.fromString);

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

   608 structure VCs = Theory_Data

   609 (

   610   type T =

   611     {pfuns: ((string list * string) option * term) Symtab.table,

   612      env:

   613        {ctxt: Element.context_i list,

   614         defs: (binding * thm) list,

   615         types: fdl_type tab,

   616         funs: (string list * string) tab,

   617         ids: (term * string) Symtab.table * Name.context,

   618         proving: bool,

   619         vcs: (string * bool *

   620           (string * expr) list * (string * expr) list) VCtab.table,

   621         path: Path.T} option}

   622   val empty : T = {pfuns = Symtab.empty, env = NONE}

   623   val extend = I

   624   fun merge ({pfuns = pfuns1, env = NONE}, {pfuns = pfuns2, env = NONE}) =

   625         {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2),

   626          env = NONE}

   627     | merge _ = err_unfinished ()

   628 )

   630 fun set_env (env as {funs, ...}) thy = VCs.map (fn

   631     {pfuns, env = NONE} =>

   632       {pfuns = check_pfuns_types thy funs pfuns, env = SOME env}

   633   | _ => err_unfinished ()) thy;

   635 fun mk_pat s = (case Int.fromString s of

   636     SOME i => [HOLogic.mk_Trueprop (Var (("C", i), HOLogic.boolT))]

   637   | NONE => error ("Bad conclusion identifier: C" ^ s));

   639 fun mk_vc thy types funs pfuns ids (tr, proved, ps, cs) =

   640   let val prop_of =

   641     HOLogic.mk_Trueprop o fst o term_of_expr thy types funs pfuns ids

   642   in

   643     (tr, proved,

   644      Element.Assumes (map (fn (s', e) =>

   645        ((Binding.name ("H" ^ s'), []), [(prop_of e, [])])) ps),

   646      Element.Shows (map (fn (s', e) =>

   647        (Attrib.empty_binding, [(prop_of e, mk_pat s')])) cs))

   648   end;

   650 fun fold_vcs f vcs =

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

   653 fun pfuns_of_vcs pfuns vcs =

   654   fold_vcs (add_expr_pfuns o snd) vcs [] |>

   655   filter_out (Symtab.defined pfuns);

   657 fun declare_missing_pfuns thy funs pfuns vcs (tab, ctxt) =

   658   let

   659     val (fs, (tys, Ts)) =

   660       pfuns_of_vcs pfuns vcs |>

   661       map_filter (fn s => lookup funs s |>

   662         Option.map (fn ty => (s, (SOME ty, pfun_type thy ty)))) |>

   663       split_list ||> split_list;

   664     val (fs', ctxt') = Name.variants fs ctxt

   665   in

   666     (fold Symtab.update_new (fs ~~ (tys ~~ map Free (fs' ~~ Ts))) pfuns,

   667      Element.Fixes (map2 (fn s => fn T =>

   668        (Binding.name s, SOME T, NoSyn)) fs' Ts),

   669      (tab, ctxt'))

   670   end;

   672 fun add_proof_fun prep (s, (optty, raw_t)) thy =

   673   VCs.map (fn

   674       {env = SOME {proving = true, ...}, ...} => err_unfinished ()

   675     | {pfuns, env} =>

   676         let

   677           val optty' = (case env of

   678               SOME {funs, ...} => lookup funs s

   679             | NONE => NONE);

   680           val optty'' = NONE |> upd_option optty |> upd_option optty';

   681           val t = prep (Option.map (pfun_type thy) optty'') raw_t

   682         in

   683           (check_pfun_type thy s t optty optty';

   684            if is_some optty'' orelse is_none env then

   685              {pfuns = Symtab.update_new (s, (optty'', t)) pfuns,

   686               env = env}

   687                handle Symtab.DUP _ => error ("Proof function " ^ s ^

   688                  " already associated with function")

   689            else error ("Undeclared proof function " ^ s))

   690         end) thy;

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

   694 fun lookup_vc thy name =

   695   (case VCs.get thy of

   696     {env = SOME {vcs, types, funs, ids, ctxt, ...}, pfuns} =>

   697       (case VCtab.lookup vcs name of

   698          SOME vc =>

   699            let val (pfuns', ctxt', ids') =

   700              declare_missing_pfuns thy funs pfuns vcs ids

   701            in SOME (ctxt @ [ctxt'], mk_vc thy types funs pfuns' ids' vc) end

   702        | NONE => NONE)

   703   | _ => NONE);

   705 fun get_vcs thy = (case VCs.get thy of

   706     {env = SOME {vcs, types, funs, ids, ctxt, defs, ...}, pfuns} =>

   707       let val (pfuns', ctxt', ids') =

   708         declare_missing_pfuns thy funs pfuns vcs ids

   709       in

   710         (ctxt @ [ctxt'], defs,

   711          VCtab.dest vcs |>

   712          map (apsnd (mk_vc thy types funs pfuns' ids')))

   713       end

   714   | _ => ([], [], []));

   716 fun mark_proved name = VCs.map (fn

   717     {pfuns, env = SOME {ctxt, defs, types, funs, ids, vcs, path, ...}} =>

   718       {pfuns = pfuns,

   719        env = SOME {ctxt = ctxt, defs = defs,

   720          types = types, funs = funs, ids = ids,

   721          proving = true,

   722          vcs = VCtab.map_entry name (fn (trace, _, ps, cs) =>

   723            (trace, true, ps, cs)) vcs,

   724          path = path}}

   725   | x => x);

   727 fun close thy = VCs.map (fn

   728     {pfuns, env = SOME {vcs, path, ...}} =>

   729       (case VCtab.fold_rev (fn (s, (_, p, _, _)) =>

   730            (if p then apfst else apsnd) (cons s)) vcs ([], []) of

   731          (proved, []) =>

   732            (File.write (Path.ext "prv" path)

   733               (concat (map (fn s => snd (strip_number s) ^

   734                  " -- proved by " ^ Distribution.version ^ "\n") proved));

   735             {pfuns = pfuns, env = NONE})

   736        | (_, unproved) => err_vcs unproved)

   737   | x => x) thy;

   740 (** set up verification conditions **)

   742 fun partition_opt f =

   743   let

   744     fun part ys zs [] = (rev ys, rev zs)

   745       | part ys zs (x :: xs) = (case f x of

   746             SOME y => part (y :: ys) zs xs

   747           | NONE => part ys (x :: zs) xs)

   748   in part [] [] end;

   750 fun dest_def (id, (Substitution_Rule ([], Ident s, rhs))) = SOME (id, (s, rhs))

   751   | dest_def _ = NONE;

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

   755 fun add_const (s, ty) ((tab, ctxt), thy) =

   756   let

   757     val T = mk_type thy ty;

   758     val b = Binding.name s;

   759     val c = Const (Sign.full_name thy b, T)

   760   in

   761     (c,

   762      ((Symtab.update (s, (c, ty)) tab, Name.declare s ctxt),

   763       Sign.add_consts_i [(b, T, NoSyn)] thy))

   764   end;

   766 fun add_def types funs pfuns consts (id, (s, e)) (ids as (tab, ctxt), thy) =

   767   (case lookup consts s of

   768      SOME ty =>

   769        let

   770          val (t, ty') = term_of_expr thy types funs pfuns ids e;

   771          val _ = ty = ty' orelse

   772            error ("Declared type " ^ ty ^ " of " ^ s ^

   773              "\ndoes not match type " ^ ty' ^ " in definition");

   774          val id' = mk_rulename id;

   775          val lthy = Named_Target.theory_init thy;

   776          val ((t', (_, th)), lthy') = Specification.definition

   777            (NONE, ((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq

   778              (Free (s, mk_type thy ty), t)))) lthy;

   779          val phi = ProofContext.export_morphism lthy' lthy

   780        in

   781          ((id', Morphism.thm phi th),

   782           ((Symtab.update (s, (Morphism.term phi t', ty)) tab,

   783             Name.declare s ctxt),

   784            Local_Theory.exit_global lthy'))

   785        end

   786    | NONE => error ("Undeclared constant " ^ s));

   788 fun add_var (s, ty) (ids, thy) =

   789   let val ([Free p], ids') = mk_variables thy [s] ty ids

   790   in (p, (ids', thy)) end;

   792 fun add_init_vars vcs (ids_thy as ((tab, _), _)) =

   793   fold_map add_var

   794     (map_filter

   795        (fn s => case try (unsuffix "~") s of

   796           SOME s' => (case Symtab.lookup tab s' of

   797             SOME (_, ty) => SOME (s, ty)

   798           | NONE => error ("Undeclared identifier " ^ s'))

   799         | NONE => NONE)

   800        (fold_vcs (add_expr_idents o snd) vcs []))

   801     ids_thy;

   803 fun is_trivial_vc ([], [(_, Ident "true")]) = true

   804   | is_trivial_vc _ = false;

   806 fun rulenames rules = commas

   807   (map (fn ((s, i), _) => s ^ "(" ^ string_of_int i ^ ")") rules);

   809 (* sort definitions according to their dependency *)

   810 fun sort_defs _ _ [] sdefs = rev sdefs

   811   | sort_defs pfuns consts defs sdefs =

   812       (case find_first (fn (_, (_, e)) =>

   813          forall (Symtab.defined pfuns) (add_expr_pfuns e []) andalso

   814          forall (fn id =>

   815            member (fn (s, (_, (s', _))) => s = s') sdefs id orelse

   816            member (fn (s, (s', _)) => s = s') consts id)

   817              (add_expr_idents e [])) defs of

   818          SOME d => sort_defs pfuns consts

   819            (remove (op =) d defs) (d :: sdefs)

   820        | NONE => error ("Bad definitions: " ^ rulenames defs));

   822 fun set_vcs ({types, vars, consts, funs} : decls) (rules, _) vcs path thy =

   823   let

   824     val {pfuns, ...} = VCs.get thy;

   825     val (defs', rules') = partition_opt dest_def rules;

   826     val consts' =

   827       subtract (fn ((_, (s, _)), (s', _)) => s = s') defs' (items consts);

   828     val defs = sort_defs pfuns consts' defs' [];

   829     (* ignore all complex rules in rls files *)

   830     val (rules'', other_rules) =

   831       List.partition (complex_rule o snd) rules';

   832     val _ = if null rules'' then ()

   833       else warning ("Ignoring rules: " ^ rulenames rules'');

   835     val vcs' = VCtab.make (maps (fn (tr, vcs) =>

   836       map (fn (s, (ps, cs)) => (s, (tr, false, ps, cs)))

   837         (filter_out (is_trivial_vc o snd) vcs)) vcs);

   839     val _ = (case filter_out (is_some o lookup funs)

   840         (pfuns_of_vcs pfuns vcs') of

   841         [] => ()

   842       | fs => error ("Undeclared proof function(s) " ^ commas fs));

   844     val (((defs', vars''), ivars), (ids, thy')) =

   845       ((Symtab.empty |>

   846         Symtab.update ("false", (HOLogic.false_const, booleanN)) |>

   847         Symtab.update ("true", (HOLogic.true_const, booleanN)),

   848         Name.context), thy) |>

   849       fold add_type_def (items types) |>

   850       fold (snd oo add_const) consts' |>

   851       fold_map (add_def types funs pfuns consts) defs ||>>

   852       fold_map add_var (items vars) ||>>

   853       add_init_vars vcs';

   855     val ctxt =

   856       [Element.Fixes (map (fn (s, T) =>

   857          (Binding.name s, SOME T, NoSyn)) (vars'' @ ivars)),

   858        Element.Assumes (map (fn (id, rl) =>

   859          ((mk_rulename id, []),

   860           [(term_of_rule thy' types funs pfuns ids rl, [])]))

   861            other_rules),

   862        Element.Notes (Thm.definitionK,

   863          [((Binding.name "defns", []), map (rpair [] o single o snd) defs')])]

   865   in

   866     set_env {ctxt = ctxt, defs = defs', types = types, funs = funs,

   867       ids = ids, proving = false, vcs = vcs', path = path} thy'

   868   end;

   870 end;

author	berghofe
	Sat, 15 Jan 2011 12:35:29 +0100
changeset 41809	d1318f3c86ba
child 41883	f938a6022d2e
permissions	-rw-r--r--