| blob | 4d81997fea8fe73f1349e8c9e84409d020255fa3 |
1 signature WHY3 =
2 sig
3 val add_why3_const: string * string -> theory -> theory
4 val add_why3_type: string * string -> theory -> theory
5 val add_why3_thm: string * thm list -> theory -> theory
6 val add_why3_def: string * thm list -> theory -> theory
7 val setup: theory -> theory
8 end
10 structure Why3: WHY3 =
11 struct
13 (**** XML utilities ****)
15 fun get_opt_att s atts = AList.lookup (op =) atts s;
17 fun get_att s atts = (case get_opt_att s atts of
18 SOME x => x
19 | NONE => error ("Missing attribute " ^ s));
21 fun get_att_default x s atts = (case get_opt_att s atts of
22 SOME y => y
23 | NONE => x);
25 fun get_name atts = get_att "name" atts;
27 fun get_name'' atts =
28 case (get_opt_att "path" atts, get_opt_att "altname" atts) of
29 (SOME s, SOME s') => SOME (s, s')
30 | _ => NONE;
32 fun get_name' atts = (get_name atts, get_name'' atts);
34 fun get_opt_name atts =
35 case get_opt_att "name" atts of
36 NONE => NONE
37 | SOME name => SOME (name, get_name'' atts);
39 fun variant fs (XML.Elem ((s, atts), ts)) =
40 (case AList.lookup (op =) fs s of
41 SOME f => (f atts ts handle General.Match =>
42 error ("Failed to parse element " ^ s))
43 | NONE => error ("Bad element: " ^ s))
44 | variant _ _ = error "Element expected";
46 fun elem s f (XML.Elem ((s', atts), ts)) =
47 if s = s' then f atts ts
48 else error ("Element " ^ s ^ " expected")
49 | elem _ _ _ = error "Element expected";
51 fun optional _ x [] = x
52 | optional f _ [x] = f x;
54 fun option _ [] = NONE
55 | option f [x] = SOME (f x);
57 fun get_bool s atts = (case get_att_default "false" s atts of
58 "false" => false
59 | "true" => true
60 | _ => error "Bad value for boolean attribute");
62 fun strip_whspc (XML.Elem (p, ts)) =
63 SOME (XML.Elem (p, map_filter strip_whspc ts))
64 | strip_whspc (txt as XML.Text s) =
65 if forall Symbol.is_blank (raw_explode s)
66 then NONE else SOME txt;
68 fun parse_xml s =
69 (case strip_whspc (XML.parse s) of
70 SOME x => x
71 | NONE => error "Bad input");
74 (**** terms and types ****)
76 (* replace occurrences of dummy_pattern by distinct variables *)
77 fun replace_dummies (Const (@{const_name Pure.dummy_pattern}, T)) used =
78 let val (x, used') = Name.variant "x" used
79 in (Free (x, T), used') end
80 | replace_dummies (t $ u) used =
81 let
82 val (t', used') = replace_dummies t used;
83 val (u', used'') = replace_dummies u used';
84 in (t' $ u', used'') end
85 | replace_dummies t used = (t, used);
87 fun make_case t ps =
88 Syntax.const @{const_name case_guard} $ @{term True} $ t $
89 fold_rev (fn (l, r) => fn u =>
90 let val (l', _) = replace_dummies l
91 (Name.context |>
92 Term.declare_term_frees l |>
93 Term.declare_term_frees r)
94 in
95 Syntax.const @{const_name case_cons} $
96 fold (fn p => fn b =>
97 Syntax.const @{const_name case_abs} $
98 Term.absfree p b)
99 (Term.add_frees l' [])
100 (Syntax.const @{const_name case_elem} $ l' $ r) $ u
101 end)
102 ps (Syntax.const @{const_name case_nil});
104 val get_tvar = prefix "'" o get_name;
106 fun typ f = variant
107 [("type", fn atts => fn Ts => Type (f atts, map (typ f) Ts)),
108 ("tvar", fn atts => fn [] => TFree (get_tvar atts, dummyS)),
109 ("fun", fn _ => fn Ts as _ :: _ => op ---> (split_last (map (typ f) Ts))),
110 ("pred", fn _ => fn Ts => map (typ f) Ts ---> @{typ bool}),
111 ("prodt", K
112 (fn [] => HOLogic.unitT
113 | Ts => foldr1 HOLogic.mk_prodT (map (typ f) Ts)))];
115 fun term f g = variant
116 [("const", fn atts => fn Ts =>
117 Const (f atts, optional (typ g) dummyT Ts)),
118 ("var", fn atts => fn Ts =>
119 Free (get_name atts, optional (typ g) dummyT Ts)),
120 ("abs", fn atts => fn [T, t] =>
121 Term.absfree (get_name atts, typ g T) (term f g t)),
122 ("app", fn _ => fn t :: ts => list_comb (term f g t, map (term f g) ts)),
123 ("num", fn atts => fn Ts => HOLogic.mk_number
124 (optional (typ g) dummyT Ts)
125 (case Int.fromString (get_att "val" atts) of SOME i => i)),
126 ("case", fn _ => fn t :: ps => make_case (term f g t)
127 (map (elem "pat" (K (fn [l, r] => (term f g l, term f g r)))) ps)),
128 ("prod", K
129 (fn [] => HOLogic.unit
130 | ts => foldr1 (fn (t, u) => Syntax.const @{const_name Pair} $ t $ u)
131 (map (term f g) ts)))];
134 (**** declarations ****)
136 type name' = (string * string) option
137 type name = string * name'
139 datatype decl =
140 Lemma of name * term list * term list
141 | Axiom of name * term list
142 | Typedecl of name * string list * typ option
143 | Param of name * typ
144 | Definition of name' * term
145 | Datatype of (name * string list * (name * (name option * typ) list) list) list
146 | Inductive of bool * (name * typ * (name * term) list) list
147 | Function of (name' * term list) list
149 fun err_unfinished () = error "An unfinished Why3 environment is still open.";
150 fun err_no_env () = error "No Why3 environment is currently open.";
152 type tables =
153 {consts: string Symtab.table,
154 types: string Symtab.table,
155 thms: thm list Symtab.table,
156 defs: thm list Symtab.table}
158 val empty_tables =
159 {consts = Symtab.empty,
160 types = Symtab.empty,
161 thms = Symtab.empty,
162 defs = Symtab.empty};
164 fun map_consts f {consts, types, thms, defs} =
165 {consts = f consts, types = types, thms = thms, defs = defs};
167 fun map_types f {consts, types, thms, defs} =
168 {consts = consts, types = f types, thms = thms, defs = defs};
170 fun map_thms f {consts, types, thms, defs} =
171 {consts = consts, types = types, thms = f thms, defs = defs};
173 fun map_defs f {consts, types, thms, defs} =
174 {consts = consts, types = types, thms = thms, defs = f defs};
176 fun merge_tables
177 ({consts = consts1, types = types1, thms = thms1, defs = defs1},
178 {consts = consts2, types = types2, thms = thms2, defs = defs2}) =
179 {consts = Symtab.merge (op =) (consts1, consts2),
180 types = Symtab.merge (op =) (types1, types2),
181 thms = Symtab.merge (eq_list Thm.eq_thm_strict) (thms1, thms2),
182 defs = Symtab.merge (eq_list Thm.eq_thm_strict) (defs1, defs2)};
184 structure Why3_Data = Theory_Data
185 (
186 type T =
187 {theories: tables Symtab.table,
188 env:
189 {thyname: string,
190 decls: (decl * Timing.timing) list,
191 vcs: (thm list option * term list * term list) Symtab.table} option}
192 val empty : T = {theories = Symtab.empty, env = NONE}
193 val extend = I
194 fun merge ({theories = theories1, env = NONE},
195 {theories = theories2, env = NONE}) =
196 {theories = Symtab.join (K merge_tables) (theories1, theories2),
197 env = NONE}
198 | merge _ = err_unfinished ()
199 )
201 fun lookup_vc thy name =
202 (case Why3_Data.get thy of
203 {env = SOME {vcs, ...}, ...} => Symtab.lookup vcs name
204 | _ => NONE);
206 val is_closed = is_none o #env o Why3_Data.get;
208 fun mk_vc name_concl prems concls =
209 (Element.Assumes (map_index (fn (i, t) =>
210 ((Binding.name ("H" ^ string_of_int (i + 1)), []), [(t, [])])) prems),
211 Element.Shows (map_index (fn (i, t) =>
212 (if name_concl then (Binding.name ("C" ^ string_of_int (i + 1)), [])
213 else Binding.empty_atts,
214 [(t, [HOLogic.mk_Trueprop
215 (Var (("C", i + 1), HOLogic.boolT))])])) concls));
217 fun get_vc thy vc_name =
218 (case lookup_vc thy vc_name of
219 SOME (proved, prems, concls) =>
220 if is_some proved then
221 error ("The verification condition " ^
222 quote vc_name ^ " has already been proved.")
223 else mk_vc false prems concls
224 | NONE => error ("There is no verification condition " ^
225 quote vc_name ^ "."));
227 fun pp_vcs msg vcs = Pretty.big_list msg (map (Pretty.str o fst) vcs);
229 fun pp_open_vcs [] = Pretty.str "All verification conditions have been proved."
230 | pp_open_vcs vcs = pp_vcs
231 "The following verification conditions remain to be proved:" vcs;
233 fun partition_vcs vcs = Symtab.fold_rev
234 (fn (name, (SOME thms, ps, cs)) =>
235 apfst (cons (name, (thms, ps, cs)))
236 | (name, (NONE, ps, cs)) =>
237 apsnd (cons (name, (ps, cs))))
238 vcs ([], []);
240 fun insert_break prt = Pretty.blk (0, [Pretty.fbrk, prt]);
242 fun print_open_vcs f vcs =
243 (Pretty.writeln (f (pp_open_vcs (snd (partition_vcs vcs)))); vcs);
245 fun mark_proved name thms = Why3_Data.map (fn
246 {theories,
247 env = SOME {thyname, decls, vcs}} =>
248 {theories = theories,
249 env = SOME {thyname = thyname, decls = decls,
250 vcs = print_open_vcs insert_break (Symtab.map_entry name
251 (fn (_, ps, cs) => (SOME thms, ps, cs)) vcs)}}
252 | x => x);
254 fun add_name kind sel th (p as (x, _)) tab =
255 Symtab.map_default (th, empty_tables) (sel (Symtab.update_new p)) tab
256 handle Symtab.DUP _ =>
257 error ("The " ^ kind ^ " " ^ x ^ " is already defined.");
259 fun add_item add opt_thyname p = Why3_Data.map
260 (fn {theories, env} =>
261 {theories = add
262 (case (env, opt_thyname) of
263 (SOME {thyname, ...}, NONE) => thyname
264 | (NONE, SOME thyname) => thyname
265 | (NONE, NONE) => err_no_env ()
266 | (SOME _, SOME _) => err_unfinished ())
267 p theories,
268 env = env});
270 fun add_item_intern add intrn s thy = add_item add NONE (s, intrn thy s) thy;
272 val add_const = add_item_intern (add_name "constant" map_consts) Sign.intern_const;
273 val add_type = add_item_intern (add_name "type" map_types) Sign.intern_type;
275 val add_const_raw = add_item (add_name "constant" map_consts);
276 val add_type_raw = add_item (add_name "type" map_types);
277 val add_thm_raw = add_item (add_name "theorem" map_thms);
278 val add_def_raw = add_item (add_name "definition" map_defs);
280 fun add_qualified add prep (s, x) thy =
281 (Long_Name.is_qualified s orelse
282 error ("Qualified name expected, but " ^ s ^ " was found");
283 add (SOME (Long_Name.qualifier s))
284 (Long_Name.base_name s, prep (Proof_Context.init_global thy) x) thy);
286 val add_why3_const = add_qualified add_const_raw (fn ctxt => fn cname =>
287 fst (dest_Const (Proof_Context.read_const {proper = true, strict = false} ctxt cname)));
289 val add_why3_type = add_qualified add_type_raw (fn ctxt => fn tyname =>
290 fst (dest_Type (Proof_Context.read_type_name {proper = true, strict = false} ctxt tyname)));
292 val add_why3_thm = add_qualified add_thm_raw (K I);
293 val add_why3_thm_cmd = add_qualified add_thm_raw Attrib.eval_thms;
295 val add_why3_def = add_qualified add_def_raw (K I);
296 val add_why3_def_cmd = add_qualified add_def_raw Attrib.eval_thms;
298 fun lookup_name kind sel tab s s' = (case Symtab.lookup tab s of
299 NONE => error ("The theory " ^ s ^ " was not found")
300 | SOME tab' => (case Symtab.lookup (sel tab') s' of
301 NONE => error ("The " ^ kind ^ " " ^ s' ^
302 " was not found in theory " ^ s)
303 | SOME name => name));
305 fun lookup_const tab = lookup_name "constant" #consts tab;
306 fun lookup_type tab = lookup_name "type" #types tab;
308 fun lookup_name' sel thy (SOME (s, s')) =
309 (case Symtab.lookup (#theories (Why3_Data.get thy)) s of
310 NONE => NONE
311 | SOME tab' => (case Symtab.lookup (sel tab') s' of
312 NONE => NONE
313 | SOME name => SOME name))
314 | lookup_name' _ _ NONE = NONE;
316 fun lookup_const' thy = lookup_name' #consts thy;
317 fun lookup_type' thy = lookup_name' #types thy;
318 fun lookup_thm thy = lookup_name' #thms thy;
319 fun lookup_def thy = lookup_name' #defs thy;
321 fun prep_name lookup ctxt atts =
322 (case Why3_Data.get (Proof_Context.theory_of ctxt) of
323 {theories, env = SOME {thyname, ...}} =>
324 let val name = get_name atts
325 in case (get_bool "local" atts, get_opt_att "path" atts) of
326 (false, NONE) => name
327 | (true, _) => lookup theories thyname name
328 | (_, SOME thyname') => lookup theories thyname' name
329 end
330 | _ => err_no_env ());
332 fun read_type ctxt x = Syntax.check_typ ctxt
333 (typ (prep_name lookup_type ctxt) x);
335 fun read_term ctxt x = Syntax.check_term ctxt
336 (term (prep_name lookup_const ctxt) (prep_name lookup_type ctxt) x);
338 fun read_prop ctxt x = HOLogic.mk_Trueprop (read_term ctxt x);
340 fun prep_datatypes ctxt dts =
341 let val ctxt' = fold (fn ((s, _), args, _) =>
342 Typedecl.basic_typedecl {final = true} (Binding.name s, length args, NoSyn) #>
343 snd #> Local_Theory.background_theory (add_type s)) dts ctxt
344 in map (fn (b, args, constrs) =>
345 (b, args, map (apsnd (map (apsnd (read_type ctxt')))) constrs)) dts
346 end;
348 fun read_statement ctxt f atts [prems, concls] = f
349 (get_name' atts,
350 elem "prems" (K (map (read_prop ctxt))) prems,
351 elem "concls" (K (map (read_prop ctxt))) concls);
353 val read_ty_params = elem "params" (K (map (elem "param" (K o get_tvar))));
355 val gen_head_of_eqn =
356 HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst #> head_of;
358 val head_of_eqn = gen_head_of_eqn #> dest_Free;
359 val head_of_eqn' = gen_head_of_eqn #> dest_Const;
361 (* split up term containing case combinators into several terms *)
362 fun expand_cases ctxt t =
363 let
364 fun rename fmap = Term.map_aterms
365 (fn Free (s, T) => Free (the_default s (AList.lookup (op =) fmap s), T)
366 | t => t);
368 fun rename_case used (l, r) =
369 let val (fmap, _) = fold_map
370 (fn s => apfst (pair s) o Name.variant s)
371 (Term.add_free_names l []) used
372 in (rename fmap l, rename fmap r) end;
374 fun strip_case used t =
375 if null (loose_bnos t)
376 then (case Case_Translation.strip_case ctxt false t of
377 SOME (u as Free _, ps) => SOME (u, map (rename_case used) ps)
378 | _ => NONE)
379 else NONE;
381 fun mk_ctxt f = Option.map (fn (x, ps) => (x, map (apsnd f) ps));
383 fun strip_case' used t = (case strip_case used t of
384 NONE => (case t of
385 t1 $ t2 => (case strip_case' used t1 of
386 NONE => mk_ctxt (fn u => t1 $ u) (strip_case' used t2)
387 | p => mk_ctxt (fn u => u $ t2) p)
388 | Abs (s, T, r) => mk_ctxt (fn u => Abs (s, T, u))
389 (strip_case' used r)
390 | _ => NONE)
391 | p => p);
393 fun expand t =
394 (case strip_case' (Term.declare_term_frees t Name.context) t of
395 NONE => [t]
396 | SOME (x, ps) => maps (fn (l, r) =>
397 expand (Term.subst_atomic [(x, l)] r)) ps)
398 in expand t end;
400 fun read_decl ctxt = variant
401 [("lemma", read_statement ctxt Lemma),
402 ("axiom", read_statement ctxt (fn (name, prems, concls) =>
403 Axiom (name, map (fn concl =>
404 Logic.list_implies (prems, concl)) concls))),
405 ("typedecl", fn atts => fn params :: rhs => Typedecl
406 (get_name' atts,
407 read_ty_params params,
408 option (read_type ctxt) rhs)),
409 ("param", fn atts => fn [ty] => Param
410 (get_name' atts, read_type ctxt ty)),
411 ("definition", fn atts => fn [t] =>
412 Definition (get_name'' atts, read_prop ctxt t)),
413 ("datatypes", fn _ => fn xs => Datatype (prep_datatypes ctxt
414 (map (elem "datatype" (fn atts => fn [params, constrs] =>
415 (get_name' atts,
416 read_ty_params params,
417 elem "constrs"
418 (K (map (elem "constr" (fn atts => fn ys =>
419 (get_name' atts,
420 map (elem "carg" (fn atts => fn [z] =>
421 (get_opt_name atts, z))) ys))))) constrs))) xs))),
422 ("inductive", fn atts => fn xs => Inductive
423 (get_bool "coind" atts,
424 map (elem "pred" (fn atts => fn ty :: rls =>
425 (get_name' atts,
426 read_type ctxt ty,
427 map (elem "rule" (fn atts => fn [prems, concl] =>
428 (get_name' atts,
429 Logic.list_implies
430 (elem "prems" (K (map (read_prop ctxt))) prems,
431 read_prop ctxt concl)))) rls))) xs)),
432 ("function", fn _ => fn xs => Function
433 (map (elem "eqn" (fn atts => fn [t] =>
434 (get_name'' atts, expand_cases ctxt (read_prop ctxt t)))) xs))];
437 (**** pretty printing ****)
439 fun string_of_status NONE = "(* unproved *)"
440 | string_of_status (SOME _) = "(* proved *)";
442 fun pretty_typ s [] = Pretty.str s
443 | pretty_typ s [v] = Pretty.block
444 [Pretty.str v, Pretty.brk 1, Pretty.str s]
445 | pretty_typ s vs = Pretty.block
446 [Pretty.list "(" ")" (map Pretty.str vs), Pretty.brk 1, Pretty.str s];
448 fun blocks prfx1 prfx2 xs f = fst (fold_map (fn x => fn prfx =>
449 (Pretty.block (Pretty.str prfx :: Pretty.brk 1 :: f x),
450 prfx2))
451 xs prfx1);
453 fun pretty_decl (p, f) ctxt (Lemma ((s, _), prems, concls)) =
454 let
455 val SOME (opt, _, _) = lookup_vc (Proof_Context.theory_of ctxt) s;
456 val ctxt' = fold Proof_Context.augment (prems @ concls) ctxt;
457 val (context, stmt) = mk_vc true prems concls
458 in
459 if p opt then
460 SOME (Pretty.big_list ("lemma " ^ s ^ ": " ^ f opt)
461 (Element.pretty_ctxt ctxt' context @
462 Element.pretty_stmt ctxt' stmt))
463 else NONE
464 end
465 | pretty_decl _ ctxt (Axiom ((s, _), ts)) =
466 let val ctxt' = fold Proof_Context.augment ts ctxt
467 in SOME (Pretty.block
468 ([Pretty.str "axiomatization where", Pretty.brk 1,
469 Pretty.str s, Pretty.str ":", Pretty.brk 1] @
470 separate (Pretty.brk 1)
471 (map (Pretty.quote o Syntax.pretty_term ctxt') ts)))
472 end
473 | pretty_decl _ ctxt (Typedecl ((s, _), args, opt_rhs)) = SOME (Pretty.block
474 (case opt_rhs of
475 NONE => [Pretty.str "typedecl", Pretty.brk 1,
476 pretty_typ s args]
477 | SOME T => [Pretty.str "type_synonym", Pretty.brk 1,
478 pretty_typ s args, Pretty.str " =", Pretty.brk 1,
479 Pretty.quote (Syntax.pretty_typ ctxt T)]))
480 | pretty_decl _ ctxt (Param ((s, _), T)) = SOME (Pretty.block
481 [Pretty.str "axiomatization", Pretty.brk 1,
482 Pretty.str s, Pretty.str " ::", Pretty.brk 1,
483 Pretty.quote (Syntax.pretty_typ ctxt T)])
484 | pretty_decl _ ctxt (Definition (_, eqn)) =
485 let
486 val ctxt' = Proof_Context.augment eqn ctxt;
487 val (s, T) = head_of_eqn eqn
488 in SOME (Pretty.block [Pretty.str "definition ", Pretty.str s,
489 Pretty.str " ::", Pretty.brk 1,
490 Pretty.quote (Syntax.pretty_typ ctxt' T),
491 Pretty.str " where", Pretty.fbrk,
492 Pretty.quote (Syntax.pretty_term ctxt' eqn)])
493 end
494 | pretty_decl _ ctxt (Datatype dts) = SOME (Pretty.chunks
495 (blocks "datatype" "and" dts (fn ((s, _), args, constrs) =>
496 [pretty_typ s args,
497 Pretty.str " =", Pretty.brk 1] @
498 Pretty.separate " |"
499 (map (fn ((s', _), cargs) => Pretty.block
500 (separate (Pretty.brk 1) (Pretty.str s' :: (map
501 (fn (NONE, T) => Pretty.quote (Syntax.pretty_typ ctxt T)
502 | (SOME (sel, _), T) => Pretty.enclose "(" ")"
503 [Pretty.str sel, Pretty.str " :", Pretty.brk 1,
504 Pretty.quote (Syntax.pretty_typ ctxt T)]) cargs))))
505 constrs))))
506 | pretty_decl _ ctxt (Inductive (coind, preds)) =
507 let val ctxt' = fold (fold (Proof_Context.augment o snd) o #3) preds ctxt
508 in
509 SOME (Pretty.chunks
510 (blocks ((coind ? prefix "co") "inductive") "and" preds
511 (fn ((s, _), T, _) =>
512 [Pretty.str s, Pretty.str " ::", Pretty.brk 1,
513 Pretty.quote (Syntax.pretty_typ ctxt' T)]) @
514 Pretty.str "where" ::
515 blocks " " "|" (maps #3 preds) (fn ((s, _), t) =>
516 [Pretty.str s, Pretty.str ":",
517 Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt' t)])))
518 end
519 | pretty_decl _ ctxt (Function eqnss) =
520 let val ctxt' = fold (fold Proof_Context.augment o snd) eqnss ctxt
521 in
522 SOME (Pretty.chunks
523 (blocks "fun" "and" eqnss (fn (_, t :: _) =>
524 let val (s, T) = head_of_eqn t
525 in
526 [Pretty.str s, Pretty.str " ::", Pretty.brk 1,
527 Pretty.quote (Syntax.pretty_typ ctxt' T)]
528 end) @
529 Pretty.str "where" ::
530 blocks " " "|" (maps snd eqnss)
531 (single o Pretty.quote o Syntax.pretty_term ctxt')))
532 end;
534 fun path_of_decl (Lemma ((_, SOME (s, _)), _, _)) = s
535 | path_of_decl (Axiom ((_, SOME (s, _)), _)) = s
536 | path_of_decl (Typedecl ((_, SOME (s, _)), _, _)) = s
537 | path_of_decl (Param ((_, SOME (s, _)), _)) = s
538 | path_of_decl (Definition (SOME (s, _), _)) = s
539 | path_of_decl (Datatype (((_, SOME (s, _)), _, _) :: _)) = s
540 | path_of_decl (Inductive (_, ((_, SOME (s, _)), _, _) :: _)) = s
541 | path_of_decl (Function ((SOME (s, _), _) :: _)) = s
542 | path_of_decl _ = "local";
544 val why3_timing = Attrib.setup_config_bool @{binding "why3_timing"} (K false);
546 fun pretty_decl_timing sel ctxt (d, (tm, tm')) =
547 case pretty_decl sel ctxt d of
548 NONE => NONE
549 | SOME pr => SOME
550 (if Config.get ctxt why3_timing then
551 Pretty.chunks2
552 [pr, Pretty.enclose "(" ")"
553 [Pretty.str (Timing.message tm),
554 Pretty.str ",", Pretty.brk 1, Pretty.str "total: ",
555 Pretty.str (Timing.message tm')]]
556 else pr);
558 fun sum_timing
559 {elapsed = elapsed1, cpu = cpu1, gc = gc1}
560 {elapsed = elapsed2, cpu = cpu2, gc = gc2} =
561 {elapsed = elapsed1 + elapsed2, cpu = cpu1 + cpu2, gc = gc1 + gc2};
563 val zero_timing = {elapsed = Time.zeroTime, cpu = Time.zeroTime, gc = Time.zeroTime};
565 fun pretty_decls thy sel decls =
566 let
567 val ctxt = Proof_Context.init_global thy;
568 val decls' = AList.coalesce (op =)
569 (fst (fold_map (fn (d, tm) => fn tm' =>
570 let val tm'' = sum_timing tm tm'
571 in ((path_of_decl d, (d, (tm, tm''))), tm'') end)
572 decls zero_timing))
573 in
574 Pretty.chunks2 (maps (fn (s, ds) =>
575 Pretty.str ("(**** " ^ s ^ " ****)") ::
576 map_filter (pretty_decl_timing sel ctxt) ds) decls')
577 end;
579 fun add_type_names (Type (s, Ts)) = insert (op =) (Long_Name.base_name s) #> fold add_type_names Ts
580 | add_type_names _ = I;
582 val add_term_names = fold_term_types
583 (fn (Const (s, _)) =>
584 apfst (insert (op =) (Long_Name.base_name s)) oo apsnd o add_type_names
585 | _ => apsnd o add_type_names);
587 fun add_decl_names (Lemma (_, prems, concls)) =
588 fold add_term_names prems #> fold add_term_names concls
589 | add_decl_names (Axiom (_, ts)) = fold add_term_names ts
590 | add_decl_names (Typedecl ((s, _), _, opT)) =
591 apsnd (insert (op =) s #> (case opT of SOME T => add_type_names T | _ => I))
592 | add_decl_names (Param ((s, _), T)) =
593 apfst (insert (op =) s) #> apsnd (add_type_names T)
594 | add_decl_names (Definition (_, eqn)) =
595 apfst (insert (op =) (fst (head_of_eqn eqn))) #> add_term_names eqn
596 | add_decl_names (Datatype dts) = fold (fn ((tyname, _), _, constrs) =>
597 apsnd (insert (op =) tyname) #> fold (fn ((cname, _), cargs) =>
598 apfst (insert (op =) cname) #> fold
599 (fn (NONE, T) => apsnd (add_type_names T)
600 | (SOME (sel, _), T) => apfst (insert (op =) sel) #> apsnd (add_type_names T))
601 cargs) constrs) dts
602 | add_decl_names (Inductive (_, preds)) = fold (fn ((s, _), _, intrs) =>
603 apfst (insert (op =) s) #> fold (add_term_names o snd) intrs) preds
604 | add_decl_names (Function eqnss) = fold (fn (_, eqns) =>
605 apfst (insert (op =) (fst (head_of_eqn (hd eqns)))) #>
606 fold add_term_names eqns) eqnss;
608 fun mk_decl_filter (p, s) = filter (fn (decl, _) => p s (add_decl_names decl ([], [])));
610 fun has_cname s (cnames, _) = exists (String.isSubstring s) cnames;
611 fun has_tyname s (_, tynames) = exists (String.isSubstring s) tynames;
612 fun has_name s names = has_cname s names orelse has_tyname s names;
614 fun show_status thy (flt, sel) =
615 (case Why3_Data.get thy of
616 {env = SOME {decls, ...}, ...} => Pretty.writeln (pretty_decls thy sel (flt decls))
617 | _ => ());
620 (**** processing declarations ****)
622 fun rename_const ps = map_aterms
623 (fn t as Const (p as (_, T)) => (case AList.lookup (op =) ps p of
624 SOME s => Free (s, T)
625 | NONE => t)
626 | t => t);
628 fun string_of_id (SOME (s, s')) = s ^ "." ^ s';
630 fun lookup_list sel lookup xs =
631 let val ps = map (fn x => (x, lookup (sel x))) xs
632 in
633 if forall (is_none o snd) ps then NONE
634 else SOME (map
635 (fn (x, SOME y) => (x, y)
636 | (x, NONE) =>
637 error ("No association given for " ^ string_of_id (sel x)))
638 ps)
639 end;
641 fun fact_binding s = Binding.qualify false "facts" (Binding.name s);
643 fun err_decl thy s decl =
644 error (Pretty.string_of (Pretty.blk (0,
645 [Pretty.str s, Pretty.fbrk, Pretty.fbrk,
646 the (pretty_decl (K true, K "") (Proof_Context.init_global thy) decl)])));
648 fun make_record_aux rname cname
649 ({fields as (fname, _) :: _, extension = (ext_name, _),
650 args, select_convs, ...} : Record.info) thy =
651 let
652 val fields' = map fst fields @ [Long_Name.map_base_name (K "more") fname];
653 val [a, b] = Name.variant_list (map fst args) ["'a", "'b"];
654 val aT = TFree (a, @{sort type});
655 val bT = TFree (b, @{sort type});
656 val argsT = map TFree args;
657 val rT = Type (ext_name, argsT @ [aT]);
658 val rT' = Type (ext_name, argsT @ [HOLogic.unitT]);
659 val fld_names = map (Long_Name.base_name o fst) fields;
660 val Us = map snd fields;
661 val Ts = Us @ [aT];
662 val fT = Ts ---> bT;
663 val fN = singleton (Name.variant_list fld_names) "f";
664 val f = Free (fN, fT);
665 val x = Free ("x", rT);
666 val xs' = map Free (fld_names ~~ Us);
667 val xs = xs' @ [Free ("more", aT)];
669 val ((_, (_, case_def)), lthy1) = thy |> Named_Target.theory_init |>
670 Specification.definition NONE [] []
671 (Binding.empty_atts,
672 HOLogic.mk_Trueprop (HOLogic.mk_eq
673 (Free (rname ^ "_case", fT --> rT --> bT) $ f $ x,
674 list_comb (f, map2 (fn s => fn T => Const (s, rT --> T) $ x) fields' Ts))));
676 val case_eq = Goal.prove_sorry lthy1 (fN :: "more" :: fld_names) []
677 (HOLogic.mk_Trueprop (HOLogic.mk_eq
678 (Free (rname ^ "_case", fT --> rT --> bT) $ f $
679 list_comb (Const (ext_name, Ts ---> rT), xs),
680 list_comb (f, xs))))
681 (fn {context, ...} =>
682 simp_tac (put_simpset HOL_basic_ss context addsimps (case_def :: select_convs)) 1);
684 val case_name = Sign.intern_const (Proof_Context.theory_of lthy1) (rname ^ "_case")
685 in
686 lthy1 |>
687 Local_Theory.note
688 ((Binding.name (rname ^ "_case_eq"),
689 [Attrib.internal (K Simplifier.simp_add)]), [case_eq]) |> snd |>
690 Specification.abbreviation Syntax.mode_input NONE []
691 (Logic.mk_equals
692 (list_comb (Free (cname, Us ---> rT'), xs'),
693 list_comb (Const (ext_name, Us ---> HOLogic.unitT --> rT'),
694 xs' @ [HOLogic.unit]))) false |>
695 Local_Theory.exit_global |>
696 Context.theory_map (Case_Translation.register
697 (Const (case_name, fT --> rT --> bT)) [Const (ext_name, Ts ---> rT)])
698 end
699 | make_record_aux _ _ _ _ = error "make_record_aux: internal error";
701 fun make_record rname args cname flds thy =
702 let val thy' = Record.add_record {overloaded = false}
703 (args, Binding.name rname) NONE
704 (map (fn (fname, T) => (Binding.name fname, T, NoSyn)) flds) thy;
705 in
706 make_record_aux rname cname
707 (Record.the_info thy' (Sign.full_name thy' (Binding.name rname))) thy'
708 end;
710 fun add_axioms s [t] =
711 Specification.axiom ((fact_binding s, []), t) #> snd
712 | add_axioms s ts =
713 fold_map Specification.axiom
714 (map_index (fn (i, t) =>
715 ((fact_binding (s ^ "_" ^ string_of_int (i + 1)), []), t)) ts) #> snd
717 fun dest_record thy [((s, _), args, [((cname, _), cargs)])] =
718 let val tyname = Sign.full_name thy (Binding.name s)
719 in
720 if forall (fn (sel, T) => is_some sel andalso not (exists_subtype
721 (fn Type (tyname', _) => tyname = tyname' | _ => false) T)) cargs
722 then SOME (s, args, cname, map (apfst (fst o the)) cargs)
723 else NONE
724 end
725 | dest_record _ _ = NONE;
727 fun get_dt_spec thy err s =
728 case Ctr_Sugar.ctr_sugar_of_global thy s of
729 SOME {T, ctrs, selss, ...} =>
730 let
731 val ctrs' = map (apsnd binder_types o dest_Const) ctrs;
732 val selss' = (case selss of
733 [] => map (map (K NONE) o snd) ctrs'
734 | _ => map (map (SOME o fst o dest_Const)) selss)
735 in
736 (snd (dest_Type T),
737 map2 (fn (cname, cargs) => fn sels => (cname, sels ~~ cargs)) ctrs' selss',
738 NONE)
739 end
740 | NONE => (case Record.get_info thy s of
741 SOME (info as {args, fields, ...}) =>
742 (map TFree args, [("", map (apfst SOME) fields)], SOME info)
743 | NONE => err ());
745 val why3_records = Attrib.setup_config_bool @{binding "why3_records"} (K true);
747 fun add_inductive_global flags cnames_syn pnames pre_intros monos thy =
748 thy |>
749 Named_Target.theory_init |>
750 Inductive.add_inductive flags cnames_syn pnames pre_intros monos |> snd |>
751 Local_Theory.exit |>
752 Proof_Context.theory_of;
754 fun mk_decl _ (decl as Axiom ((s, id), ts)) thy =
755 (case lookup_thm thy id of
756 NONE =>
757 (add_axioms s ts thy, true)
758 | SOME thms =>
759 if length thms = length ts andalso
760 forall (Pattern.matches thy o apfst Thm.prop_of) (thms ~~ ts)
761 then (thy, false)
762 else err_decl thy ("Failed to match axiom " ^ string_of_id id) decl)
763 | mk_decl realize (Typedecl ((s, id), args, opt_rhs)) thy =
764 (case opt_rhs of
765 NONE =>
766 if realize then (thy, false) else
767 (case lookup_type' thy id of
768 NONE =>
769 (thy |> Named_Target.theory_map (Typedecl.typedecl {final = true}
770 (Binding.name s, map (rpair dummyS) args, NoSyn) #> snd) |>
771 add_type s,
772 true)
773 | SOME s' => (add_type_raw NONE (s, s') thy, false))
774 | SOME T =>
775 (thy |> Named_Target.theory_map (Typedecl.abbrev
776 (Binding.name s, args, NoSyn) T #> snd) |>
777 add_type s,
778 true))
779 | mk_decl realize (Param ((s, id), T)) thy =
780 if realize then (thy, false) else
781 (case lookup_const' thy id of
782 NONE =>
783 (thy |> Specification.axiomatization
784 [(Binding.name s, SOME T, NoSyn)] [] [] [] |> snd |>
785 add_const s,
786 true)
787 | SOME s' => (add_const_raw NONE (s, s') thy, false))
788 | mk_decl _ (decl as Definition (id, eqn)) thy =
789 let val (s, _) = head_of_eqn eqn
790 in
791 case lookup_def thy id of
792 NONE =>
793 (thy |> Named_Target.theory_map (Specification.definition
794 NONE [] [] (Binding.empty_atts, eqn) #> snd) |>
795 add_const s,
796 true)
797 | SOME [th] =>
798 let val p as (s', _) = head_of_eqn' (Thm.prop_of th)
799 handle TERM _ => err_decl thy
800 ("Bad equation for " ^ string_of_id id) decl
801 in
802 if Pattern.matches thy (rename_const [(p, s)] (Thm.prop_of th), eqn)
803 then (add_const_raw NONE (s, s') thy, false)
804 else err_decl thy
805 ("Failed to match definition " ^ string_of_id id) decl
806 end
807 | _ => err_decl thy ("Single theorem expected for " ^ string_of_id id) decl
808 end
809 | mk_decl _ (decl as Datatype dts) thy =
810 (case lookup_list (snd o #1) (lookup_type' thy) dts of
811 NONE =>
812 (case (Config.get_global thy why3_records, dest_record thy dts) of
813 (true, SOME (s, args, s', cargs)) =>
814 (thy |> make_record s (map (rpair @{sort type}) args) s' cargs |>
815 add_type s |>
816 add_const s' |>
817 fold (add_const o fst) cargs,
818 true)
819 | _ =>
820 (thy |> Named_Target.theory_map
821 (BNF_FP_Def_Sugar.co_datatypes BNF_Util.Least_FP BNF_LFP.construct_lfp
822 (Ctr_Sugar.default_ctr_options,
823 map (fn ((s, _), args, constrs) =>
824 (((((map (fn arg => (SOME Binding.empty, (TFree (arg, @{sort type}),
825 @{sort type}))) args, Binding.name s), NoSyn),
826 map (fn ((s', _), cargs) =>
827 (((Binding.empty, Binding.name s'),
828 map (fn (NONE, T) => (Binding.empty, T)
829 | (SOME (sel, _), T) => (Binding.name sel, T)) cargs),
830 NoSyn)) constrs),
831 (Binding.empty, Binding.empty, Binding.empty)),
832 [])) dts)) |>
833 fold (fn ((s, _), _, constrs) => add_type s #>
834 fold (add_const o fst o fst) constrs #>
835 fold add_const (map_filter (Option.map fst o fst) (snd (hd constrs)))) dts,
836 true))
837 | SOME dts' =>
838 let val tcmap = map (fn (((s, _), _, _), s') =>
839 (Sign.full_name thy (Binding.name s), s')) dts'
840 in
841 (fold (fn (((tyname, id), args, constrs), tyname') =>
842 let
843 val (args', constrs', opt_info) = get_dt_spec thy
844 (fn () => err_decl thy (string_of_id id ^
845 "must be mapped to a datatype or record type") decl) tyname';
846 fun err () = err_decl thy
847 ("Failed to match type " ^ string_of_id id) decl;
848 val _ =
849 length args = length args' andalso
850 length constrs = length constrs' orelse err ();
851 val tvmap = args ~~ args';
853 fun rename (Type (tc, Ts)) = Type
854 (the_default tc (AList.lookup (op =) tcmap tc),
855 map rename Ts)
856 | rename (T as TFree (a, _)) =
857 (the_default T (AList.lookup (op =) tvmap a))
858 | rename T = T
859 in
860 add_type_raw NONE (tyname, tyname') #>
861 rpair [] #>
862 fold2 (fn ((cname, _), cargs) => fn (cname', cargs') =>
863 if map (rename o snd) cargs = map snd cargs'
864 then
865 apfst (case opt_info of
866 NONE => add_const_raw NONE (cname, cname')
867 | SOME info =>
868 make_record_aux tyname cname info #>
869 add_const cname) #>
870 fold2
871 (fn (NONE, _) => K I
872 | (SOME (sel, _), _) =>
873 (fn (NONE, _) => err_decl thy
874 ("Missing selector " ^ sel ^
875 " for type " ^ string_of_id id) decl
876 | (SOME sel', _) => (fn p as (thy', sel_map) =>
877 (case AList.lookup (op =) sel_map sel of
878 NONE =>
879 (add_const_raw NONE (sel, sel') thy',
880 (sel, sel') :: sel_map)
881 | SOME sel'' =>
882 if sel' = sel'' then p
883 else err_decl thy
884 ("Inconsistent selector " ^ sel ^
885 " for type " ^ string_of_id id) decl))))
886 cargs cargs'
887 else err ()) constrs constrs' #>
888 fst
889 end) dts' thy,
890 false)
891 end)
892 | mk_decl _ (decl as Inductive (coind, preds)) thy =
893 (case lookup_list (snd o #1) (lookup_def thy) preds of
894 NONE =>
895 (thy |> add_inductive_global
896 {quiet_mode = true, verbose = false,
897 alt_name = Binding.empty, coind = coind,
898 no_elim = false, no_ind = false, skip_mono = false}
899 (map (fn ((s, _), T, _) => ((Binding.name s, T), NoSyn)) preds) []
900 (maps (map (apfst (rpair [] o Binding.name o fst)) o #3) preds) [] |>
901 fold (add_const o fst o #1) preds,
902 true)
903 | SOME preds' =>
904 let val cmap = map (fn (((s, id), _, _), th :: _) =>
905 (th |> Thm.concl_of |> HOLogic.dest_Trueprop |> head_of |>
906 dest_Const handle TERM _ =>
907 err_decl thy ("Bad introduction rule for " ^ string_of_id id) decl,
908 s)) preds'
909 in
910 app (fn (((_, id), _, intrs), intrs') =>
911 if length intrs = length intrs' andalso
912 ListPair.all (fn ((_, t), th) =>
913 Pattern.matches thy (rename_const cmap (Thm.prop_of th), t))
914 (intrs, intrs')
915 then ()
916 else err_decl thy
917 ("Failed to match predicate " ^ string_of_id id) decl) preds';
918 (fold (add_const_raw NONE o swap o apfst fst) cmap thy, false)
919 end)
920 | mk_decl _ (decl as Function eqnss) thy =
921 let val eqnss' = map (head_of_eqn o hd o snd) eqnss
922 in
923 case lookup_list fst (lookup_def thy) eqnss of
924 NONE =>
925 (thy |> Named_Target.theory_map (Function_Fun.add_fun
926 (map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) eqnss')
927 (map (fn t => ((Binding.empty_atts, t), [], [])) (maps snd eqnss))
928 Function_Fun.fun_config) |>
929 fold (add_const o fst) eqnss',
930 true)
931 | SOME eqnss'' =>
932 let val cmap = map2 (fn ((id, _), th :: _) => fn (s, _) =>
933 (th |> Thm.prop_of |> head_of_eqn' handle TERM _ =>
934 err_decl thy ("Bad equation for " ^ string_of_id id) decl,
935 s)) eqnss'' eqnss'
936 in
937 app (fn ((id, eqns), eqns') =>
938 if length eqns = length eqns' andalso
939 ListPair.all (fn (t, th) =>
940 Pattern.matches thy (rename_const cmap (Thm.prop_of th), t))
941 (eqns, eqns')
942 then ()
943 else err_decl thy
944 ("Failed to match function " ^ string_of_id id) decl) eqnss'';
945 (fold (add_const_raw NONE o swap o apfst fst) cmap thy, false)
946 end
947 end
948 | mk_decl _ _ thy = (thy, true);
950 fun init_decls thyname consts types = Why3_Data.map
951 (fn {theories, env = NONE} =>
952 {theories = Symtab.update_new
953 (thyname,
954 {consts = Symtab.make consts,
955 types = Symtab.make types,
956 thms = Symtab.empty,
957 defs = Symtab.empty})
958 theories handle Symtab.DUP _ =>
959 error ("Theory " ^ thyname ^ " has already been loaded."),
960 env = SOME
961 {thyname = thyname,
962 decls = [],
963 vcs = Symtab.empty}}
964 | _ => err_unfinished ());
966 fun put_decls decls = Why3_Data.map
967 (fn {theories, env = SOME {thyname, ...}} =>
968 {theories = theories,
969 env = SOME
970 {thyname = thyname,
971 decls = decls,
972 vcs = print_open_vcs I (fold
973 (fn (Lemma ((s, _), ps, cs), _) => Symtab.update_new (s, (NONE, ps, cs))
974 | _ => I) decls Symtab.empty
975 handle Symtab.DUP k => error ("Verification condition " ^ k ^
976 " has already been declared."))}}
977 | _ => err_no_env ());
979 fun close incomplete thy =
980 thy |>
981 Why3_Data.map (fn
982 {theories, env = SOME {thyname, vcs, ...}} =>
983 let
984 val (proved, unproved) = partition_vcs vcs;
985 val _ = Thm.consolidate (maps (#1 o snd) proved)
986 in
987 (if null unproved
988 then writeln ("Finished Why3 theory " ^ thyname)
989 else (if incomplete then warning else error)
990 (Pretty.string_of (pp_open_vcs unproved));
991 {theories = theories, env = NONE})
992 end
993 | _ => err_no_env ()) |>
994 Sign.parent_path;
996 val why3_warn_axioms = Attrib.setup_config_bool @{binding "why3_warn_axioms"} (K true);
998 fun unrealized_axioms thy decls =
999 if Config.get_global thy why3_warn_axioms then
1000 (case filter (fn (Axiom _, _) => true | _ => false) decls of
1001 [] => ()
1002 | decls' => warning (Pretty.string_of (Pretty.chunks2
1003 [Pretty.str "Unrealized axioms", pretty_decls thy (K true, K "") decls'])))
1004 else ();
1006 fun process_decls consts types x path = elem "theory" (fn atts =>
1007 (fn imports :: xs => elem "realized" (fn _ => fn rs => fn thy =>
1008 let
1009 val thyname = get_name atts;
1010 val realize = get_bool "realize" atts;
1011 val _ =
1012 realize orelse
1013 Path.is_basic path andalso
1014 let val (path', ext) = Path.split_ext path
1015 in
1016 Path.implode path' = Context.theory_name thy andalso
1017 ext = "xml"
1018 end orelse
1019 error "Name of Why3 file does not match name of theory";
1020 val (ds, thy') = thy |>
1021 Sign.add_path thyname |>
1022 init_decls thyname consts types |>
1023 pair [] |>
1024 fold (fn x => fn (ds, thy) =>
1025 let
1026 val d = read_decl (Named_Target.theory_init thy) x;
1027 val (tm, (thy', b)) = Timing.timing (mk_decl realize d) thy
1028 in ((b ? cons (d, tm)) ds, thy') end) xs |>
1029 apfst rev;
1030 val _ = unrealized_axioms thy' ds
1031 in put_decls ds thy' end) imports
1032 | _ => error "Bad theory specification")) x
1035 (**** commands ****)
1037 fun why3_open ((file, consts), types) thy =
1038 let val ({src_path, lines, ...}: Token.file, thy') = file thy;
1039 in process_decls
1040 (map (apsnd (Sign.intern_const thy)) consts)
1041 (map (apsnd (Sign.intern_type thy)) types)
1042 (parse_xml (cat_lines lines)) src_path thy'
1043 end;
1045 fun prove_vc vc_name lthy =
1046 let
1047 val thy = Proof_Context.theory_of lthy;
1048 val (ctxt, stmt) = get_vc thy vc_name
1049 in
1050 Specification.theorem true Thm.theoremK NONE
1051 (fn thmss => (Local_Theory.background_theory
1052 (mark_proved vc_name (flat thmss))))
1053 (fact_binding vc_name, []) [] [ctxt] stmt false lthy
1054 end;
1056 val _ =
1057 Outer_Syntax.command @{command_keyword "why3_open"}
1058 "open a new Why3 environment and load a Why3-generated .xml file"
1059 (Resources.provide_parse_file --
1060 Scan.optional (Parse.reserved "constants" |-- Parse.!!! (Scan.repeat1
1061 (Parse.name --| Args.$$$ "=" -- Parse.!!! Parse.name))) [] --
1062 Scan.optional (Parse.reserved "types" |-- (Scan.repeat1
1063 (Parse.name --| Args.$$$ "=" -- Parse.!!! Parse.name))) [] >>
1064 (Toplevel.theory o why3_open));
1066 val _ =
1067 Outer_Syntax.command @{command_keyword "why3_vc"}
1068 "enter into proof mode for a specific verification condition"
1069 (Parse.name >> (fn name =>
1070 (Toplevel.local_theory_to_proof NONE NONE (prove_vc name))));
1072 val _ =
1073 Outer_Syntax.command @{command_keyword "why3_status"}
1074 "show the name and state of all loaded verification conditions"
1075 (Scan.optional
1076 (( Args.$$$ "cname" >> K has_cname
1077 || Args.$$$ "tyname" >> K has_tyname
1078 || Args.$$$ "name" >> K has_name) --|
1079 Args.colon -- Args.name >> mk_decl_filter) I --
1080 Scan.optional
1081 (Args.parens
1082 ( Args.$$$ "proved" >> K (is_some, K "")
1083 || Args.$$$ "unproved" >> K (is_none, K "")))
1084 (K true, string_of_status) >> (fn args =>
1085 Toplevel.keep (fn state => show_status (Toplevel.theory_of state) args)))
1087 val _ =
1088 Outer_Syntax.command @{command_keyword "why3_end"}
1089 "close the current Why3 environment"
1090 (Scan.optional (@{keyword "("} |-- Parse.!!!
1091 (Parse.reserved "incomplete" --| @{keyword ")"}) >> K true) false >>
1092 (Toplevel.theory o close));
1094 val _ =
1095 Outer_Syntax.command @{command_keyword "why3_consts"}
1096 "associate Why3 constants with constants"
1097 (Scan.repeat1 (Parse.name --| Args.$$$ "=" -- Parse.name) >>
1098 (Toplevel.theory o fold add_why3_const));
1100 val _ =
1101 Outer_Syntax.command @{command_keyword "why3_types"}
1102 "associate Why3 types with types"
1103 (Scan.repeat1 (Parse.name --| Args.$$$ "=" -- Parse.name) >>
1104 (Toplevel.theory o fold add_why3_type));
1106 val _ =
1107 Outer_Syntax.command @{command_keyword "why3_thms"}
1108 "associate Why3 axioms with theorems"
1109 (Parse.and_list1 (Parse.name --| Args.$$$ "=" -- Parse.thms1) >>
1110 (Toplevel.theory o fold add_why3_thm_cmd));
1112 val _ =
1113 Outer_Syntax.command @{command_keyword "why3_defs"}
1114 "associate Why3 definitions with definitions"
1115 (Parse.and_list1 (Parse.name --| Args.$$$ "=" -- Parse.thms1) >>
1116 (Toplevel.theory o fold add_why3_def_cmd));
1118 val setup = Theory.at_end (fn thy =>
1119 let
1120 val _ = is_closed thy
1121 orelse error ("Found the end of the theory, " ^
1122 "but the last Why3 environment is still open.")
1123 in NONE end);
1125 end;