62 end; |
62 end; |
63 |
63 |
64 fun string_of_status false = "(unproved)" |
64 fun string_of_status false = "(unproved)" |
65 | string_of_status true = "(proved)"; |
65 | string_of_status true = "(proved)"; |
66 |
66 |
67 fun chunks ps = Pretty.blk (0, |
|
68 flat (separate [Pretty.fbrk, Pretty.fbrk] (map single ps))); |
|
69 |
|
70 fun show_status (p, f) = Toplevel.no_timing o Toplevel.keep (fn state => |
67 fun show_status (p, f) = Toplevel.no_timing o Toplevel.keep (fn state => |
71 let |
68 let |
72 val thy = Toplevel.theory_of state; |
69 val thy = Toplevel.theory_of state; |
73 |
70 |
74 val (context, defs, vcs) = SPARK_VCs.get_vcs thy; |
71 val (context, defs, vcs) = SPARK_VCs.get_vcs thy; |
82 val ctxt = state |> |
79 val ctxt = state |> |
83 Toplevel.theory_of |> |
80 Toplevel.theory_of |> |
84 ProofContext.init_global |> |
81 ProofContext.init_global |> |
85 Context.proof_map (fold Element.init context) |
82 Context.proof_map (fold Element.init context) |
86 in |
83 in |
87 (* FIXME print as single message, e.g. via Pretty.big_list, Pretty.chunks etc. *) |
84 [Pretty.str "Context:", |
88 (writeln "Context:\n"; |
85 Pretty.chunks (maps (Element.pretty_ctxt ctxt) context), |
89 Pretty.chunks (maps (Element.pretty_ctxt ctxt) context) |> |
|
90 Pretty.writeln; |
|
91 |
86 |
92 writeln "\nDefinitions:\n"; |
87 Pretty.str "Definitions:", |
93 Pretty.chunks (map (fn (bdg, th) => Pretty.block |
88 Pretty.chunks (map (fn (bdg, th) => Pretty.block |
94 [Pretty.str (Binding.str_of bdg ^ ":"), |
89 [Pretty.str (Binding.str_of bdg ^ ":"), |
95 Pretty.brk 1, |
90 Pretty.brk 1, |
96 Display.pretty_thm ctxt th]) |
91 Display.pretty_thm ctxt th]) |
97 defs) |> |
92 defs), |
98 Pretty.writeln; |
|
99 |
93 |
100 writeln "\nVerification conditions:\n"; |
94 Pretty.str "Verification conditions:", |
101 chunks (maps (fn (trace, vcs'') => |
95 Pretty.chunks2 (maps (fn (trace, vcs'') => |
102 Pretty.str trace :: |
96 Pretty.str trace :: |
103 map (fn (name, status, context', stmt) => |
97 map (fn (name, status, context', stmt) => |
104 Pretty.big_list (name ^ " " ^ f status) |
98 Pretty.big_list (name ^ " " ^ f status) |
105 (Element.pretty_ctxt ctxt context' @ |
99 (Element.pretty_ctxt ctxt context' @ |
106 Element.pretty_stmt ctxt stmt)) vcs'') vcs') |> |
100 Element.pretty_stmt ctxt stmt)) vcs'') vcs')] |> |
107 Pretty.writeln) |
101 Pretty.chunks2 |> Pretty.writeln |
108 end); |
102 end); |
109 |
103 |
110 val _ = |
104 val _ = |
111 Outer_Syntax.command "spark_open" |
105 Outer_Syntax.command "spark_open" |
112 "open a new SPARK environment and load a SPARK-generated .vcg or .siv file" |
106 "open a new SPARK environment and load a SPARK-generated .vcg or .siv file" |