src/HOL/SPARK/Tools/spark_commands.ML
author wenzelm
Sat, 14 May 2016 13:52:01 +0200
changeset 63093 3081f7719df7
parent 63092 a949b2a5f51d
child 63094 056ea294c256
permissions -rw-r--r--
reverted accidental commit;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     1
(*  Title:      HOL/SPARK/Tools/spark_commands.ML
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     2
    Author:     Stefan Berghofer
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     3
    Copyright:  secunet Security Networks AG
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     4
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     5
Isar commands for handling SPARK/Ada verification conditions.
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     6
*)
56798
939e88e79724 Discontinued old spark_open; spark_open_siv is now spark_open
berghofe
parents: 56334
diff changeset
     7
55789
8d4d339177dc modernized theory setup;
wenzelm
parents: 55788
diff changeset
     8
structure SPARK_Commands: sig end =
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     9
struct
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    10
56798
939e88e79724 Discontinued old spark_open; spark_open_siv is now spark_open
berghofe
parents: 56334
diff changeset
    11
fun spark_open header (files, prfx) thy =
48908
713f24d7a40f added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
wenzelm
parents: 48167
diff changeset
    12
  let
55788
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 51658
diff changeset
    13
    val ([{src_path, lines = vc_lines, pos = vc_pos, ...}: Token.file,
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 51658
diff changeset
    14
      {lines = fdl_lines, pos = fdl_pos, ...},
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 51658
diff changeset
    15
      {lines = rls_lines, pos = rls_pos, ...}], thy') = files thy;
56208
06cc31dff138 clarifed module name;
wenzelm
parents: 55789
diff changeset
    16
    val base = fst (Path.split_ext (File.full_path (Resources.master_directory thy') src_path));
48908
713f24d7a40f added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
wenzelm
parents: 48167
diff changeset
    17
  in
713f24d7a40f added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
wenzelm
parents: 48167
diff changeset
    18
    SPARK_VCs.set_vcs
55788
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 51658
diff changeset
    19
      (snd (Fdl_Parser.parse_declarations fdl_pos (cat_lines fdl_lines)))
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 51658
diff changeset
    20
      (Fdl_Parser.parse_rules rls_pos (cat_lines rls_lines))
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 51658
diff changeset
    21
      (snd (Fdl_Parser.parse_vcs header vc_pos (cat_lines vc_lines)))
48908
713f24d7a40f added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
wenzelm
parents: 48167
diff changeset
    22
      base prfx thy'
713f24d7a40f added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
wenzelm
parents: 48167
diff changeset
    23
  end;
713f24d7a40f added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
wenzelm
parents: 48167
diff changeset
    24
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    25
fun add_proof_fun_cmd pf thy =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42356
diff changeset
    26
  let val ctxt = Proof_Context.init_global thy
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    27
  in SPARK_VCs.add_proof_fun
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    28
    (fn optT => Syntax.parse_term ctxt #>
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    29
       the_default I (Option.map Type.constraint optT) #>
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    30
       Syntax.check_term ctxt) pf thy
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    31
  end;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    32
46725
d34ec0512dfb Added infrastructure for mapping SPARK field / constructor names
berghofe
parents: 43702
diff changeset
    33
fun add_spark_type_cmd (s, (raw_typ, cmap)) thy =
d34ec0512dfb Added infrastructure for mapping SPARK field / constructor names
berghofe
parents: 43702
diff changeset
    34
  SPARK_VCs.add_type (s, (Syntax.read_typ_global thy raw_typ, cmap)) thy;
42356
e8777e3ea6ef Added command for associating user-defined types with SPARK types.
berghofe
parents: 42003
diff changeset
    35
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    36
fun get_vc thy vc_name =
48167
da1a1eae93fa Various improvements
berghofe
parents: 47067
diff changeset
    37
  (case SPARK_VCs.lookup_vc thy false vc_name of
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    38
    SOME (ctxt, (_, proved, ctxt', stmt)) =>
41896
582cccdda0ed spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents: 41887
diff changeset
    39
      if is_some proved then
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    40
        error ("The verification condition " ^
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    41
          quote vc_name ^ " has already been proved.")
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    42
      else (ctxt @ [ctxt'], stmt)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    43
  | NONE => error ("There is no verification condition " ^
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    44
      quote vc_name ^ "."));
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    45
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    46
fun prove_vc vc_name lthy =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    47
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42356
diff changeset
    48
    val thy = Proof_Context.theory_of lthy;
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    49
    val (ctxt, stmt) = get_vc thy vc_name
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    50
  in
63093
3081f7719df7 reverted accidental commit;
wenzelm
parents: 63092
diff changeset
    51
    Specification.theorem Thm.theoremK NONE
41896
582cccdda0ed spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents: 41887
diff changeset
    52
      (fn thmss => (Local_Theory.background_theory
582cccdda0ed spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents: 41887
diff changeset
    53
         (SPARK_VCs.mark_proved vc_name (flat thmss))))
50787
065c684130ad disable interactive mode of Specification.theorem with its slow printing of results;
wenzelm
parents: 49444
diff changeset
    54
      (Binding.name vc_name, []) [] ctxt stmt false lthy
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    55
  end;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    56
41896
582cccdda0ed spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents: 41887
diff changeset
    57
fun string_of_status NONE = "(unproved)"
582cccdda0ed spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents: 41887
diff changeset
    58
  | string_of_status (SOME _) = "(proved)";
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    59
51658
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 50787
diff changeset
    60
fun show_status thy (p, f) =
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    61
  let
48167
da1a1eae93fa Various improvements
berghofe
parents: 47067
diff changeset
    62
    val (context, defs, vcs) = SPARK_VCs.get_vcs thy true;
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    63
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    64
    val vcs' = AList.coalesce (op =) (map_filter
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    65
      (fn (name, (trace, status, ctxt, stmt)) =>
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    66
         if p status then
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    67
           SOME (trace, (name, status, ctxt, stmt))
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    68
         else NONE) vcs);
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    69
51658
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 50787
diff changeset
    70
    val ctxt = thy |>
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42356
diff changeset
    71
      Proof_Context.init_global |>
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    72
      Context.proof_map (fold Element.init context)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    73
  in
41592
74c0629a11e9 Tuned show_status
berghofe
parents: 41586
diff changeset
    74
    [Pretty.str "Context:",
74c0629a11e9 Tuned show_status
berghofe
parents: 41586
diff changeset
    75
     Pretty.chunks (maps (Element.pretty_ctxt ctxt) context),
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    76
41592
74c0629a11e9 Tuned show_status
berghofe
parents: 41586
diff changeset
    77
     Pretty.str "Definitions:",
43547
f3a8476285c6 clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
wenzelm
parents: 42396
diff changeset
    78
     Pretty.chunks (map (fn (b, th) => Pretty.block
f3a8476285c6 clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
wenzelm
parents: 42396
diff changeset
    79
       [Binding.pretty b, Pretty.str ":",
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    80
        Pretty.brk 1,
61268
abe08fb15a12 moved remaining display.ML to more_thm.ML;
wenzelm
parents: 59936
diff changeset
    81
        Thm.pretty_thm ctxt th])
41592
74c0629a11e9 Tuned show_status
berghofe
parents: 41586
diff changeset
    82
          defs),
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    83
41592
74c0629a11e9 Tuned show_status
berghofe
parents: 41586
diff changeset
    84
     Pretty.str "Verification conditions:",
74c0629a11e9 Tuned show_status
berghofe
parents: 41586
diff changeset
    85
     Pretty.chunks2 (maps (fn (trace, vcs'') =>
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    86
       Pretty.str trace ::
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    87
       map (fn (name, status, context', stmt) =>
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    88
         Pretty.big_list (name ^ " " ^ f status)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    89
           (Element.pretty_ctxt ctxt context' @
41592
74c0629a11e9 Tuned show_status
berghofe
parents: 41586
diff changeset
    90
            Element.pretty_stmt ctxt stmt)) vcs'') vcs')] |>
56334
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 56208
diff changeset
    91
    Pretty.writeln_chunks2
51658
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 50787
diff changeset
    92
  end;
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    93
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    94
val _ =
59936
b8ffc3dc9e24 @{command_spec} is superseded by @{command_keyword};
wenzelm
parents: 59927
diff changeset
    95
  Outer_Syntax.command @{command_keyword spark_open_vcg}
48908
713f24d7a40f added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
wenzelm
parents: 48167
diff changeset
    96
    "open a new SPARK environment and load a SPARK-generated .vcg file"
56798
939e88e79724 Discontinued old spark_open; spark_open_siv is now spark_open
berghofe
parents: 56334
diff changeset
    97
    (Resources.provide_parse_files "spark_open_vcg" -- Parse.parname
48908
713f24d7a40f added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
wenzelm
parents: 48167
diff changeset
    98
      >> (Toplevel.theory o spark_open Fdl_Lexer.vcg_header));
713f24d7a40f added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
wenzelm
parents: 48167
diff changeset
    99
713f24d7a40f added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
wenzelm
parents: 48167
diff changeset
   100
val _ =
59936
b8ffc3dc9e24 @{command_spec} is superseded by @{command_keyword};
wenzelm
parents: 59927
diff changeset
   101
  Outer_Syntax.command @{command_keyword spark_open}
48908
713f24d7a40f added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
wenzelm
parents: 48167
diff changeset
   102
    "open a new SPARK environment and load a SPARK-generated .siv file"
56798
939e88e79724 Discontinued old spark_open; spark_open_siv is now spark_open
berghofe
parents: 56334
diff changeset
   103
    (Resources.provide_parse_files "spark_open" -- Parse.parname
48908
713f24d7a40f added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
wenzelm
parents: 48167
diff changeset
   104
      >> (Toplevel.theory o spark_open Fdl_Lexer.siv_header));
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   105
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   106
val pfun_type = Scan.option
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   107
  (Args.parens (Parse.list1 Parse.name) --| Args.colon -- Parse.name);
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   108
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   109
val _ =
59936
b8ffc3dc9e24 @{command_spec} is superseded by @{command_keyword};
wenzelm
parents: 59927
diff changeset
   110
  Outer_Syntax.command @{command_keyword spark_proof_functions}
41586
1f930561a560 more standard command descriptions;
wenzelm
parents: 41561
diff changeset
   111
    "associate SPARK proof functions with terms"
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   112
    (Scan.repeat1 (Parse.name -- (pfun_type --| Args.$$$ "=" -- Parse.term)) >>
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46725
diff changeset
   113
      (Toplevel.theory o fold add_proof_fun_cmd));
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   114
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   115
val _ =
59936
b8ffc3dc9e24 @{command_spec} is superseded by @{command_keyword};
wenzelm
parents: 59927
diff changeset
   116
  Outer_Syntax.command @{command_keyword spark_types}
42356
e8777e3ea6ef Added command for associating user-defined types with SPARK types.
berghofe
parents: 42003
diff changeset
   117
    "associate SPARK types with types"
46725
d34ec0512dfb Added infrastructure for mapping SPARK field / constructor names
berghofe
parents: 43702
diff changeset
   118
    (Scan.repeat1 (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.typ --
d34ec0512dfb Added infrastructure for mapping SPARK field / constructor names
berghofe
parents: 43702
diff changeset
   119
       Scan.optional (Args.parens (Parse.list1
62969
9f394a16c557 eliminated "xname" and variants;
wenzelm
parents: 61268
diff changeset
   120
         (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.name)))) [])) >>
42356
e8777e3ea6ef Added command for associating user-defined types with SPARK types.
berghofe
parents: 42003
diff changeset
   121
       (Toplevel.theory o fold add_spark_type_cmd));
e8777e3ea6ef Added command for associating user-defined types with SPARK types.
berghofe
parents: 42003
diff changeset
   122
e8777e3ea6ef Added command for associating user-defined types with SPARK types.
berghofe
parents: 42003
diff changeset
   123
val _ =
59936
b8ffc3dc9e24 @{command_spec} is superseded by @{command_keyword};
wenzelm
parents: 59927
diff changeset
   124
  Outer_Syntax.local_theory_to_proof @{command_keyword spark_vc}
41586
1f930561a560 more standard command descriptions;
wenzelm
parents: 41561
diff changeset
   125
    "enter into proof mode for a specific verification condition"
59927
251fa1530de1 more standard local_theory command setup;
wenzelm
parents: 59923
diff changeset
   126
    (Parse.name >> prove_vc);
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   127
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   128
val _ =
59936
b8ffc3dc9e24 @{command_spec} is superseded by @{command_keyword};
wenzelm
parents: 59927
diff changeset
   129
  Outer_Syntax.command @{command_keyword spark_status}
41586
1f930561a560 more standard command descriptions;
wenzelm
parents: 41561
diff changeset
   130
    "show the name and state of all loaded verification conditions"
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   131
    (Scan.optional
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   132
       (Args.parens
41896
582cccdda0ed spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents: 41887
diff changeset
   133
          (   Args.$$$ "proved" >> K (is_some, K "")
582cccdda0ed spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents: 41887
diff changeset
   134
           || Args.$$$ "unproved" >> K (is_none, K "")))
51658
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 50787
diff changeset
   135
       (K true, string_of_status) >> (fn args =>
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 50787
diff changeset
   136
        Toplevel.keep (fn state => show_status (Toplevel.theory_of state) args)))
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   137
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   138
val _ =
59936
b8ffc3dc9e24 @{command_spec} is superseded by @{command_keyword};
wenzelm
parents: 59927
diff changeset
   139
  Outer_Syntax.command @{command_keyword spark_end}
41586
1f930561a560 more standard command descriptions;
wenzelm
parents: 41561
diff changeset
   140
    "close the current SPARK environment"
48167
da1a1eae93fa Various improvements
berghofe
parents: 47067
diff changeset
   141
    (Scan.optional (@{keyword "("} |-- Parse.!!!
da1a1eae93fa Various improvements
berghofe
parents: 47067
diff changeset
   142
         (Parse.reserved "incomplete" --| @{keyword ")"}) >> K true) false >>
da1a1eae93fa Various improvements
berghofe
parents: 47067
diff changeset
   143
       (Toplevel.theory o SPARK_VCs.close));
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   144
55789
8d4d339177dc modernized theory setup;
wenzelm
parents: 55788
diff changeset
   145
val _ = Theory.setup (Theory.at_end (fn thy =>
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   146
  let
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   147
    val _ = SPARK_VCs.is_closed thy
56798
939e88e79724 Discontinued old spark_open; spark_open_siv is now spark_open
berghofe
parents: 56334
diff changeset
   148
      orelse error ("Found the end of the theory, " ^
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   149
        "but the last SPARK environment is still open.")
55789
8d4d339177dc modernized theory setup;
wenzelm
parents: 55788
diff changeset
   150
  in NONE end));
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   151
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   152
end;