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 ->

    11     (string * string) * Fdl_Parser.vcs -> Path.T -> string -> theory -> theory

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

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

    14     theory -> theory

    15   val add_type: string * typ -> theory -> theory

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

    17     (string * thm list option * Element.context_i * Element.statement_i)) option

    18   val get_vcs: theory ->

    19     Element.context_i list * (binding * thm) list * (string *

    20     (string * thm list option * Element.context_i * Element.statement_i)) list

    21   val mark_proved: string -> thm list -> theory -> theory

    22   val close: theory -> theory

    23   val is_closed: theory -> bool

    24 end;

    26 structure SPARK_VCs: SPARK_VCS =

    27 struct

    29 open Fdl_Parser;

    32 (** theory data **)

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

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

    38 val name_ord = prod_ord string_ord (option_ord int_ord) o

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

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

    43 structure VCs = Theory_Data

    44 (

    45   type T =

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

    47      type_map: typ Symtab.table,

    48      env:

    49        {ctxt: Element.context_i list,

    50         defs: (binding * thm) list,

    51         types: fdl_type tab,

    52         funs: (string list * string) tab,

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

    54         proving: bool,

    55         vcs: (string * thm list option *

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

    57         path: Path.T,

    58         prefix: string} option}

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

    60   val extend = I

    61   fun merge ({pfuns = pfuns1, type_map = type_map1, env = NONE},

    62         {pfuns = pfuns2, type_map = type_map2, env = NONE}) =

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

    64          type_map = Symtab.merge (op =) (type_map1, type_map2),

    65          env = NONE}

    66     | merge _ = err_unfinished ()

    67 )

    70 (** utilities **)

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

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

    76 fun lookup_prfx "" tab s = Symtab.lookup tab s

    77   | lookup_prfx prfx tab s = (case Symtab.lookup tab s of

    78         NONE => Symtab.lookup tab (prfx ^ "__" ^ s)

    79       | x => x);

    81 fun strip_prfx s =

    82   let

    83     fun strip ys [] = ("", implode ys)

    84       | strip ys ("_" :: "_" :: xs) = (implode (rev xs), implode ys)

    85       | strip ys (x :: xs) = strip (x :: ys) xs

    86   in strip [] (rev (raw_explode s)) end;

    88 fun mk_unop s t =

    89   let val T = fastype_of t

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

    92 fun mk_times (t, u) =

    93   let

    94     val setT = fastype_of t;

    95     val T = HOLogic.dest_setT setT;

    96     val U = HOLogic.dest_setT (fastype_of u)

    97   in

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

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

   100   end;

   102 fun get_type thy prfx ty =

   103   let val {type_map, ...} = VCs.get thy

   104   in lookup_prfx prfx type_map ty end;

   106 fun mk_type _ _ "integer" = HOLogic.intT

   107   | mk_type _ _ "boolean" = HOLogic.boolT

   108   | mk_type thy prfx ty =

   109       (case get_type thy prfx ty of

   110          NONE =>

   111            Syntax.check_typ (Proof_Context.init_global thy)

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

   113        | SOME T => T);

   115 val booleanN = "boolean";

   116 val integerN = "integer";

   118 fun define_overloaded (def_name, eq) lthy =

   119   let

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

   121       Logic.dest_equals |>> dest_Free;

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

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

   124     val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');

   125     val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm

   126   in (thm', lthy') end;

   128 fun strip_underscores s =

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

   131 fun strip_tilde s =

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

   134 val mangle_name = strip_underscores #> strip_tilde;

   136 fun mk_variables thy prfx xs ty (tab, ctxt) =

   137   let

   138     val T = mk_type thy prfx ty;

   139     val (ys, ctxt') = fold_map Name.variant (map mangle_name xs) ctxt;

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

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

   143 fun get_record_info thy T = (case Record.dest_recTs T of

   144     [(tyname, [@{typ unit}])] =>

   145       Record.get_info thy (Long_Name.qualifier tyname)

   146   | _ => NONE);

   148 fun find_field fname = find_first (curry lcase_eq fname o fst);

   150 fun find_field' fname = get_first (fn (flds, fldty) =>

   151   if member (op =) flds fname then SOME fldty else NONE);

   153 fun assoc_ty_err thy T s msg =

   154   error ("Type " ^ Syntax.string_of_typ_global thy T ^

   155     " associated with SPARK type " ^ s ^ "\n" ^ msg);

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

   160 fun add_enum_type tyname tyname' thy =

   161   let

   162     val {case_name, ...} = the (Datatype_Data.get_info thy tyname');

   163     val cs = map Const (the (Datatype_Data.get_constrs thy tyname'));

   164     val k = length cs;

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

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

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

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

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

   171     fun mk_binrel_def s f = Logic.mk_equals

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

   173        Abs ("x", T, Abs ("y", T,

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

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

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

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

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

   182         (p,

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

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

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

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

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

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

   190         mk_binrel_def @{const_name less} p);

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

   193       (HOLogic.mk_Trueprop (HOLogic.mk_eq

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

   195       (fn _ =>

   196          rtac @{thm subset_antisym} 1 THEN

   197          rtac @{thm subsetI} 1 THEN

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

   199            (Proof_Context.theory_of lthy) tyname'))) 1 THEN

   200          ALLGOALS (asm_full_simp_tac (simpset_of lthy)));

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

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

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

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

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

   208       (HOLogic.mk_Trueprop (HOLogic.mk_eq

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

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

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

   213       (HOLogic.mk_Trueprop (HOLogic.mk_eq

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

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

   216               p $ HOLogic.mk_UNIV T,

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

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

   219               HOLogic.mk_number HOLogic.intT 0 $

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

   221       (fn _ =>

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

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

   224          rtac @{thm subset_antisym} 1 THEN

   225          simp_tac (simpset_of lthy) 1 THEN

   226          rtac @{thm subsetI} 1 THEN

   227          asm_full_simp_tac (simpset_of lthy addsimps @{thms interval_expand}

   228            delsimps @{thms atLeastLessThan_iff}) 1);

   230     val lthy' =

   231       Class.prove_instantiation_instance (fn _ =>

   232         Class.intro_classes_tac [] THEN

   233         rtac finite_UNIV 1 THEN

   234         rtac range_pos 1 THEN

   235         simp_tac (HOL_basic_ss addsimps [def3]) 1 THEN

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

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

   239       let

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

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

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

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

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

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

   246           (fn _ =>

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

   248              simp_tac (simpset_of lthy' addsimps

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

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

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

   253       (HOLogic.mk_Trueprop (HOLogic.mk_eq

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

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

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

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

   259       (HOLogic.mk_Trueprop (HOLogic.mk_eq

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

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

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

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

   266   in

   267     lthy' |>

   268     Local_Theory.note

   269       ((Binding.name (tyname ^ "_card"), simp_att), [card_UNIV]) ||>>

   270     Local_Theory.note

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

   272     Local_Theory.note

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

   274     Local_Theory.note

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

   276     Local_Theory.note

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

   278     Local_Theory.exit_global

   279   end;

   282 fun check_no_assoc thy prfx s = case get_type thy prfx s of

   283     NONE => ()

   284   | SOME _ => error ("Cannot associate a type with " ^ s ^

   285       "\nsince it is no record or enumeration type");

   287 fun check_enum [] [] = NONE

   288   | check_enum els [] = SOME ("has no element(s) " ^ commas els)

   289   | check_enum [] cs = SOME ("has extra element(s) " ^

   290       commas (map (Long_Name.base_name o fst) cs))

   291   | check_enum (el :: els) ((cname, _) :: cs) =

   292       if lcase_eq (el, cname) then check_enum els cs

   293       else SOME ("either has no element " ^ el ^

   294         " or it is at the wrong position");

   296 fun add_type_def prfx (s, Basic_Type ty) (ids, thy) =

   297       (check_no_assoc thy prfx s;

   298        (ids,

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

   300           (mk_type thy prfx ty) thy |> snd))

   302   | add_type_def prfx (s, Enum_Type els) ((tab, ctxt), thy) =

   303       let

   304         val (thy', tyname) = (case get_type thy prfx s of

   305             NONE =>

   306               let

   307                 val tyb = Binding.name s;

   308                 val tyname = Sign.full_name thy tyb

   309               in

   310                 (thy |>

   311                  Datatype.add_datatype {strict = true, quiet = true} [s]

   312                    [([], tyb, NoSyn,

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

   314                  add_enum_type s tyname,

   315                  tyname)

   316               end

   317           | SOME (T as Type (tyname, [])) =>

   318               (case Datatype_Data.get_constrs thy tyname of

   319                  NONE => assoc_ty_err thy T s "is not a datatype"

   320                | SOME cs =>

   321                    let

   322                      val (prfx', _) = strip_prfx s;

   323                      val els' =

   324                        if prfx' = "" then els

   325                        else map (unprefix (prfx' ^ "__")) els

   326                          handle Fail _ => error ("Bad enumeration type " ^ s)

   327                    in

   328                      case check_enum els' cs of

   329                        NONE => (thy, tyname)

   330                      | SOME msg => assoc_ty_err thy T s msg

   331                    end));

   332         val cs = map Const (the (Datatype_Data.get_constrs thy' tyname))

   333       in

   334         ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,

   335           fold Name.declare els ctxt),

   336          thy')

   337       end

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

   340       (check_no_assoc thy prfx s;

   341        (ids,

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

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

   344              mk_type thy prfx resty) thy |> snd))

   346   | add_type_def prfx (s, Record_Type fldtys) (ids, thy) =

   347       (ids,

   348        let val fldTs = maps (fn (flds, ty) =>

   349          map (rpair (mk_type thy prfx ty)) flds) fldtys

   350        in case get_type thy prfx s of

   351            NONE =>

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

   353                (map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy

   354          | SOME rT =>

   355              (case get_record_info thy rT of

   356                 NONE => assoc_ty_err thy rT s "is not a record type"

   357               | SOME {fields, ...} =>

   358                   (case subtract (lcase_eq o pairself fst) fldTs fields of

   359                      [] => ()

   360                    | flds => assoc_ty_err thy rT s ("has extra field(s) " ^

   361                        commas (map (Long_Name.base_name o fst) flds));

   362                    map (fn (fld, T) =>

   363                      case AList.lookup lcase_eq fields fld of

   364                        NONE => assoc_ty_err thy rT s ("has no field " ^ fld)

   365                      | SOME U => T = U orelse assoc_ty_err thy rT s

   366                          ("has field " ^

   367                           fld ^ " whose type\n" ^

   368                           Syntax.string_of_typ_global thy U ^

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

   370                           Syntax.string_of_typ_global thy T)) fldTs;

   371                    thy))

   372        end)

   374   | add_type_def prfx (s, Pending_Type) (ids, thy) =

   375       (ids,

   376        case get_type thy prfx s of

   377          SOME _ => thy

   378        | NONE => Typedecl.typedecl_global

   379            (Binding.name s, [], NoSyn) thy |> snd);

   382 fun term_of_expr thy prfx types pfuns =

   383   let

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   444           (case Symtab.lookup tab s of

   445              SOME t_ty => t_ty

   446            | NONE => (case lookup_prfx prfx pfuns s of

   447                SOME (SOME ([], resty), t) => (t, resty)

   448              | _ => error ("Undeclared identifier " ^ s)))

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

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

   453           let

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

   455             val q = (case s of

   456                 "for_all" => HOLogic.mk_all

   457               | "for_some" => HOLogic.mk_exists)

   458           in

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

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

   461              booleanN)

   462           end

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

   466           (* record field selection *)

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

   468              SOME fname => (case es of

   469                [e] =>

   470                  let

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

   472                    val rT = mk_type thy prfx rcdty

   473                  in case (get_record_info thy rT, lookup types rcdty) of

   474                      (SOME {fields, ...}, SOME (Record_Type fldtys)) =>

   475                        (case (find_field fname fields,

   476                             find_field' fname fldtys) of

   477                           (SOME (fname', fT), SOME fldty) =>

   478                             (Const (fname', rT --> fT) $ t, fldty)

   479                         | _ => error ("Record " ^ rcdty ^

   480                             " has no field named " ^ fname))

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

   482                  end

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

   484            | NONE =>

   486           (* record field update *)

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

   488              SOME fname => (case es of

   489                [e, e'] =>

   490                  let

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

   492                    val rT = mk_type thy prfx rcdty;

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

   494                    val fT = mk_type thy prfx fldty

   495                  in case get_record_info thy rT of

   496                      SOME {fields, ...} =>

   497                        (case find_field fname fields of

   498                           SOME (fname', fU) =>

   499                             if fT = fU then

   500                               (Const (fname' ^ "_update",

   501                                  (fT --> fT) --> rT --> rT) $

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

   503                                rcdty)

   504                             else error ("Type\n" ^

   505                               Syntax.string_of_typ_global thy fT ^

   506                               "\ndoes not match type\n" ^

   507                               Syntax.string_of_typ_global thy fU ^

   508                               "\nof field " ^ fname)

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

   510                             " has no field named " ^ fname))

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

   512                  end

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

   514            | NONE =>

   516           (* enumeration type to integer *)

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

   518              SOME tyname => (case es of

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

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

   521                  integerN)

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

   523            | NONE =>

   525           (* integer to enumeration type *)

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

   527              SOME tyname => (case es of

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

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

   530                  tyname)

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

   532            | NONE =>

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

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

   536               [e] =>

   537                 let

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

   539                   val T = mk_type thy prfx tyname

   540                 in (Const

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

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

   543                 end

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

   546           (* user-defined proof function *)

   547           else

   548             (case lookup_prfx prfx pfuns s of

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

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

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

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

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

   555           in case lookup types ty of

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

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

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

   559           end

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

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

   563           in case lookup types ty of

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

   565                 let

   566                   val T = foldr1 HOLogic.mk_prodT

   567                     (map (mk_type thy prfx) idxtys);

   568                   val U = mk_type thy prfx elty;

   569                   val fT = T --> U

   570                 in

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

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

   573                        fst (tm_of vs e'),

   574                    ty)

   575                 end

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

   577           end

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

   580           let

   581             val T = mk_type thy prfx s;

   582             val {extension = (ext_name, _), fields, ...} =

   583               (case get_record_info thy T of

   584                  NONE => error (s ^ " is not a record type")

   585                | SOME info => info);

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

   587             val fnames = map (Long_Name.base_name o fst) fields;

   588             val fnames' = map fst flds;

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

   590               case AList.lookup lcase_eq flds' s' of

   591                 SOME fval_ty => fval_ty

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

   593                   fnames);

   594             val _ = (case subtract lcase_eq fnames fnames' of

   595                 [] => ()

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

   597                   " in record " ^ s));

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

   599                 [] => ()

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

   601                   " in record " ^ s))

   602           in

   603             (list_comb

   604                (Const (ext_name,

   605                   map (mk_type thy prfx) ftys @ [HOLogic.unitT] ---> T),

   606                 fvals @ [HOLogic.unit]),

   607              s)

   608           end

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

   611           (case lookup types s of

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

   613                let

   614                  val Ts = map (mk_type thy prfx) idxtys;

   615                  val T = foldr1 HOLogic.mk_prodT Ts;

   616                  val U = mk_type thy prfx elty;

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

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

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

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

   621                  fun mk_idx idx =

   622                    if length Ts <> length idx then

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

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

   625                  fun mk_upd (idxs, e) t =

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

   627                    then

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

   629                          T --> U --> T --> U) $ t $

   630                        foldl1 HOLogic.mk_prod

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

   632                        fst (tm_of vs e)

   633                    else

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

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

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

   637                          (map mk_idx idxs) $

   638                        fst (tm_of vs e)

   639                in

   640                  (fold mk_upd assocs

   641                     (case default of

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

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

   644                   s)

   645                end

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

   648   in tm_of end;

   651 fun term_of_rule thy prfx types pfuns ids rule =

   652   let val tm_of = fst o term_of_expr thy prfx types pfuns ids

   653   in case rule of

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

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

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

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

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

   659   end;

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

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

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

   666 fun complex_expr (Number _) = false

   667   | complex_expr (Ident _) = false

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

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

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

   671   | complex_expr _ = true;

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

   674       complex_expr e orelse exists complex_expr es

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

   676       complex_expr e orelse complex_expr e' orelse

   677       exists complex_expr es;

   679 val is_pfun =

   680   Symtab.defined builtin orf

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

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

   683   equal "succ" orf equal "pred";

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

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

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

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

   690   | fold_expr f g (Number _) = I

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

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

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

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

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

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

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

   698       fold_opt (fold_expr f g) default #>

   699       fold (fold_pair

   700         (fold (fold (fold_pair

   701           (fold_expr f g) (fold_opt (fold_expr f g)))))

   702         (fold_expr f g)) assocs;

   704 fun add_expr_pfuns funs = fold_expr

   705   (fn s => if is_pfun s then I else insert (op =) s)

   706   (fn s => if is_none (lookup funs s) then I else insert (op =) s);

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

   710 fun pfun_type thy prfx (argtys, resty) =

   711   map (mk_type thy prfx) argtys ---> mk_type thy prfx resty;

   713 fun check_pfun_type thy prfx s t optty1 optty2 =

   714   let

   715     val T = fastype_of t;

   716     fun check ty =

   717       let val U = pfun_type thy prfx ty

   718       in

   719         T = U orelse

   720         error ("Type\n" ^

   721           Syntax.string_of_typ_global thy T ^

   722           "\nof function " ^

   723           Syntax.string_of_term_global thy t ^

   724           " associated with proof function " ^ s ^

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

   726           Syntax.string_of_typ_global thy U)

   727       end

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

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

   732 fun check_pfuns_types thy prfx funs =

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

   734    let val optty' = lookup funs

   735      (if prfx = "" then s

   736       else unprefix (prfx ^ "__") s handle Fail _ => s)

   737    in

   738      (check_pfun_type thy prfx s t optty optty';

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

   740    end);

   743 (** the VC store **)

   745 fun err_vcs names = error (Pretty.string_of

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

   747     (map Pretty.str names)))

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

   750     {pfuns, type_map, env = NONE} =>

   751       {pfuns = check_pfuns_types thy prefix funs pfuns,

   752        type_map = type_map,

   753        env = SOME env}

   754   | _ => err_unfinished ()) thy;

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

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

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

   760 fun mk_vc thy prfx types pfuns ids (tr, proved, ps, cs) =

   761   let val prop_of =

   762     HOLogic.mk_Trueprop o fst o term_of_expr thy prfx types pfuns ids

   763   in

   764     (tr, proved,

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

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

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

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

   769   end;

   771 fun fold_vcs f vcs =

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

   774 fun pfuns_of_vcs prfx funs pfuns vcs =

   775   fold_vcs (add_expr_pfuns funs o snd) vcs [] |>

   776   filter (is_none o lookup_prfx prfx pfuns);

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

   779   let

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

   781       pfuns_of_vcs prfx funs pfuns vcs |>

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

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

   784       split_list ||> split_list;

   785     val (fs', ctxt') = fold_map Name.variant fs ctxt

   786   in

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

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

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

   790      (tab, ctxt'))

   791   end;

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

   794   VCs.map (fn

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

   796     | {pfuns, type_map, env} =>

   797         let

   798           val (optty', prfx) = (case env of

   799               SOME {funs, prefix, ...} => (lookup funs s, prefix)

   800             | NONE => (NONE, ""));

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

   802           val t = prep (Option.map (pfun_type thy prfx) optty'') raw_t;

   803           val _ = (case fold_aterms (fn u =>

   804               if is_Var u orelse is_Free u then insert (op =) u else I) t [] of

   805               [] => ()

   806             | ts => error ("Term\n" ^ Syntax.string_of_term_global thy t ^

   807                 "\nto be associated with proof function " ^ s ^

   808                 " contains free variable(s) " ^

   809                 commas (map (Syntax.string_of_term_global thy) ts)));

   810         in

   811           (check_pfun_type thy prfx s t optty optty';

   812            if is_some optty'' orelse is_none env then

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

   814               type_map = type_map,

   815               env = env}

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

   817                  " already associated with function")

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

   819         end) thy;

   821 fun add_type (s, T as Type (tyname, Ts)) thy =

   822       thy |>

   823       VCs.map (fn

   824           {env = SOME _, ...} => err_unfinished ()

   825         | {pfuns, type_map, env} =>

   826             {pfuns = pfuns,

   827              type_map = Symtab.update_new (s, T) type_map,

   828              env = env}

   829               handle Symtab.DUP _ => error ("SPARK type " ^ s ^

   830                 " already associated with type")) |>

   831       (fn thy' =>

   832          case Datatype_Data.get_constrs thy' tyname of

   833            NONE => thy'

   834          | SOME cs =>

   835              if null Ts then

   836                (map

   837                   (fn (_, Type (_, [])) => ()

   838                     | (cname, _) => assoc_ty_err thy T s

   839                         ("has illegal constructor " ^

   840                          Long_Name.base_name cname)) cs;

   841                 add_enum_type s tyname thy')

   842              else assoc_ty_err thy T s "is illegal")

   843   | add_type (s, T) thy = assoc_ty_err thy T s "is illegal";

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

   847 fun lookup_vc thy name =

   848   (case VCs.get thy of

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

   850       (case VCtab.lookup vcs name of

   851          SOME vc =>

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

   853              declare_missing_pfuns thy prefix funs pfuns vcs ids

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

   855        | NONE => NONE)

   856   | _ => NONE);

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

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

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

   861         declare_missing_pfuns thy prefix funs pfuns vcs ids

   862       in

   863         (ctxt @ [ctxt'], defs,

   864          VCtab.dest vcs |>

   865          map (apsnd (mk_vc thy prefix types pfuns' ids')))

   866       end

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

   869 fun mark_proved name thms = VCs.map (fn

   870     {pfuns, type_map,

   871      env = SOME {ctxt, defs, types, funs, ids, vcs, path, prefix, ...}} =>

   872       {pfuns = pfuns,

   873        type_map = type_map,

   874        env = SOME {ctxt = ctxt, defs = defs,

   875          types = types, funs = funs, ids = ids,

   876          proving = true,

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

   878            (trace, SOME thms, ps, cs)) vcs,

   879          path = path,

   880          prefix = prefix}}

   881   | x => x);

   883 fun write_prv path s =

   884   let val path_prv = Path.ext "prv" path;

   885   in if try File.read path_prv = SOME s then () else File.write path_prv s end;

   887 fun close thy =

   888   thy |>

   889   VCs.map (fn

   890       {pfuns, type_map, env = SOME {vcs, path, ...}} =>

   891         (case VCtab.fold_rev (fn vc as (_, (_, p, _, _)) =>

   892              (if is_some p then apfst else apsnd) (cons vc)) vcs ([], []) of

   893            (proved, []) =>

   894              (Thm.join_proofs (maps (the o #2 o snd) proved);

   895               write_prv path

   896                 (implode (map (fn (s, _) => snd (strip_number s) ^

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

   898               {pfuns = pfuns, type_map = type_map, env = NONE})

   899          | (_, unproved) => err_vcs (map fst unproved))

   900     | _ => error "No SPARK environment is currently open") |>

   901   Sign.parent_path;

   904 (** set up verification conditions **)

   906 fun partition_opt f =

   907   let

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

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

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

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

   912   in part [] [] end;

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

   915   | dest_def _ = NONE;

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

   919 fun add_const prfx (s, ty) ((tab, ctxt), thy) =

   920   let

   921     val T = mk_type thy prfx ty;

   922     val b = Binding.name s;

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

   924   in

   925     (c,

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

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

   928   end;

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

   931   (case lookup consts s of

   932      SOME ty =>

   933        let

   934          val (t, ty') = term_of_expr thy prfx types pfuns ids e;

   935          val T = mk_type thy prfx ty;

   936          val T' = mk_type thy prfx ty';

   937          val _ = T = T' orelse

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

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

   940          val id' = mk_rulename id;

   941          val lthy = Named_Target.theory_init thy;

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

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

   944              (Free (s, T), t)))) lthy;

   945          val phi = Proof_Context.export_morphism lthy' lthy

   946        in

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

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

   949             Name.declare s ctxt),

   950            Local_Theory.exit_global lthy'))

   951        end

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

   954 fun add_var prfx (s, ty) (ids, thy) =

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

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

   958 fun add_init_vars prfx vcs (ids_thy as ((tab, _), _)) =

   959   fold_map (add_var prfx)

   960     (map_filter

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

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

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

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

   965         | NONE => NONE)

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

   967     ids_thy;

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

   970   | is_trivial_vc _ = false;

   972 fun rulenames rules = commas

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

   975 (* sort definitions according to their dependency *)

   976 fun sort_defs _ _ _ _ [] sdefs = rev sdefs

   977   | sort_defs prfx funs pfuns consts defs sdefs =

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

   979          forall (is_some o lookup_prfx prfx pfuns)

   980            (add_expr_pfuns funs e []) andalso

   981          forall (fn id =>

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

   983            consts id)

   984              (add_expr_idents e [])) defs of

   985          SOME d => sort_defs prfx funs pfuns consts

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

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

   989 fun set_vcs ({types, vars, consts, funs} : decls)

   990       (rules, _) ((_, ident), vcs) path prfx thy =

   991   let

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

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

   994     val consts' =

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

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

   997     val (rules'', other_rules) =

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

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

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

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

  1003       map (fn (s, (ps, cs)) => (s, (tr, NONE, ps, cs)))

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

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

  1007         (pfuns_of_vcs prfx funs pfuns vcs') of

  1008         [] => ()

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

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

  1012       ((Symtab.empty |>

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

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

  1015         Name.context),

  1016        thy |> Sign.add_path (Long_Name.base_name ident)) |>

  1017       fold (add_type_def prfx) (items types) |>

  1018       fold (snd oo add_const prfx) consts' |> (fn ids_thy as ((tab, _), _) =>

  1019         ids_thy |>

  1020         fold_map (add_def prfx types pfuns consts)

  1021           (sort_defs prfx funs pfuns (Symtab.defined tab) defs []) ||>>

  1022         fold_map (add_var prfx) (items vars) ||>>

  1023         add_init_vars prfx vcs');

  1025     val ctxt =

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

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

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

  1029          ((mk_rulename id, []),

  1030           [(term_of_rule thy' prfx types pfuns ids rl, [])]))

  1031            other_rules),

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

  1034   in

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

  1036       ids = ids, proving = false, vcs = vcs', path = path, prefix = prfx} thy'

  1037   end;

  1039 end;

author	wenzelm
	Sun, 06 Nov 2011 16:41:53 +0100
changeset 46239	157e74588c49
parent 45524	6d8d09b90398
child 46457	a6d9464a230b
permissions	-rw-r--r--