proper thy_load command 'boogie_file' -- avoid direct access to file-system;
authorwenzelm
Sat Nov 16 16:57:09 2013 +0100 (2013-11-16)
changeset 54447019394de2b41
parent 54446 31884c67d73a
child 54448 7110476960f7
proper thy_load command 'boogie_file' -- avoid direct access to file-system;
etc/isar-keywords.el
src/HOL/ROOT
src/HOL/SMT_Examples/Boogie.thy
src/HOL/SMT_Examples/boogie.ML
     1.1 --- a/etc/isar-keywords.el	Sat Nov 16 13:12:02 2013 +0100
     1.2 +++ b/etc/isar-keywords.el	Sat Nov 16 16:57:09 2013 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4  ;;
     1.5  ;; Keyword classification tables for Isabelle/Isar.
     1.6 -;; Generated from HOL + HOL-Auth + HOL-BNF + HOL-BNF-LFP + HOL-Bali + HOL-Decision_Procs + HOL-IMP + HOL-Imperative_HOL + HOL-Import + HOL-Library + HOL-Mutabelle + HOL-Nominal + HOL-Proofs + HOL-Proofs-Extraction + HOL-SPARK + HOL-Statespace + HOL-TPTP + HOL-ex + HOLCF + Pure.
     1.7 +;; Generated from HOL + HOL-Auth + HOL-BNF + HOL-BNF-LFP + HOL-Bali + HOL-Decision_Procs + HOL-IMP + HOL-Imperative_HOL + HOL-Import + HOL-Library + HOL-Mutabelle + HOL-Nominal + HOL-Proofs + HOL-Proofs-Extraction + HOL-SPARK + HOL-Statespace + HOL-TPTP + HOL-Word-SMT_Examples + HOL-ex + HOLCF + Pure.
     1.8  ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
     1.9  ;;
    1.10  
    1.11 @@ -33,6 +33,7 @@
    1.12      "axiomatization"
    1.13      "back"
    1.14      "bnf"
    1.15 +    "boogie_file"
    1.16      "bundle"
    1.17      "by"
    1.18      "cannot_undo"
    1.19 @@ -487,6 +488,7 @@
    1.20      "atom_decl"
    1.21      "attribute_setup"
    1.22      "axiomatization"
    1.23 +    "boogie_file"
    1.24      "bundle"
    1.25      "case_of_simps"
    1.26      "class"
     2.1 --- a/src/HOL/ROOT	Sat Nov 16 13:12:02 2013 +0100
     2.2 +++ b/src/HOL/ROOT	Sat Nov 16 16:57:09 2013 +0100
     2.3 @@ -779,13 +779,10 @@
     2.4    theories [condition = ISABELLE_FULL_TEST]
     2.5      SMT_Tests
     2.6    files
     2.7 -    "Boogie_Dijkstra.b2i"
     2.8      "Boogie_Dijkstra.certs"
     2.9 -    "Boogie_Max.b2i"
    2.10      "Boogie_Max.certs"
    2.11      "SMT_Examples.certs"
    2.12      "SMT_Word_Examples.certs"
    2.13 -    "VCC_Max.b2i"
    2.14      "VCC_Max.certs"
    2.15  
    2.16  session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
     3.1 --- a/src/HOL/SMT_Examples/Boogie.thy	Sat Nov 16 13:12:02 2013 +0100
     3.2 +++ b/src/HOL/SMT_Examples/Boogie.thy	Sat Nov 16 16:57:09 2013 +0100
     3.3 @@ -6,6 +6,7 @@
     3.4  
     3.5  theory Boogie
     3.6  imports Main
     3.7 +keywords "boogie_file" :: thy_load ("b2i")
     3.8  begin
     3.9  
    3.10  text {*
    3.11 @@ -56,17 +57,17 @@
    3.12  
    3.13  declare [[smt_certificates = "Boogie_Max.certs"]]
    3.14  
    3.15 -setup {* Boogie.boogie_prove "Boogie_Max.b2i" *}
    3.16 +boogie_file Boogie_Max
    3.17  
    3.18  
    3.19  declare [[smt_certificates = "Boogie_Dijkstra.certs"]]
    3.20  
    3.21 -setup {* Boogie.boogie_prove "Boogie_Dijkstra.b2i" *}
    3.22 +boogie_file Boogie_Dijkstra
    3.23  
    3.24  
    3.25  declare [[z3_with_extensions = true]]
    3.26  declare [[smt_certificates = "VCC_Max.certs"]]
    3.27  
    3.28 -setup {* Boogie.boogie_prove "VCC_Max.b2i" *}
    3.29 +boogie_file VCC_Max
    3.30  
    3.31  end
     4.1 --- a/src/HOL/SMT_Examples/boogie.ML	Sat Nov 16 13:12:02 2013 +0100
     4.2 +++ b/src/HOL/SMT_Examples/boogie.ML	Sat Nov 16 16:57:09 2013 +0100
     4.3 @@ -6,7 +6,7 @@
     4.4  
     4.5  signature BOOGIE =
     4.6  sig
     4.7 -  val boogie_prove: string -> theory -> theory
     4.8 +  val boogie_prove: theory -> string -> unit
     4.9  end
    4.10  
    4.11  structure Boogie: BOOGIE =
    4.12 @@ -299,21 +299,33 @@
    4.13    ALLGOALS (SMT_Solver.smt_tac ctxt (boogie_rules @ axioms))
    4.14  
    4.15  
    4.16 -fun boogie_prove file_name thy =
    4.17 +fun boogie_prove thy text =
    4.18    let
    4.19 -    val (text, thy') = Thy_Load.use_file (Path.explode file_name) thy
    4.20      val lines = explode_lines text
    4.21  
    4.22      val ((axioms, vc), ctxt) =
    4.23        empty_context
    4.24        |> parse_lines lines
    4.25        |> add_unique_axioms
    4.26 -      |> build_proof_context thy'
    4.27 +      |> build_proof_context thy
    4.28  
    4.29      val _ = Goal.prove ctxt [] axioms vc (fn {prems, context} =>
    4.30        boogie_tac context prems)
    4.31      val _ = writeln "Verification condition proved successfully"
    4.32  
    4.33 -  in thy' end
    4.34 +  in () end
    4.35 +
    4.36 +
    4.37 +(* Isar command *)
    4.38 +
    4.39 +val _ =
    4.40 +  Outer_Syntax.command @{command_spec "boogie_file"}
    4.41 +    "prove verification condition from .b2i file"
    4.42 +    (Thy_Load.provide_parse_files "boogie_file" >> (fn files =>
    4.43 +      Toplevel.theory (fn thy =>
    4.44 +        let
    4.45 +          val ([{text, ...}], thy') = files thy;
    4.46 +          val _ = boogie_prove thy' text;
    4.47 +        in thy' end)))
    4.48  
    4.49  end