1 (* Title: src/Tools/isac/BridgeJEdit/Calculation.thy
2 Author: Walther Neuper, JKU Linz
3 (c) due to copyright terms
5 Outer syntax for Isabelle/Isac's Calculation.
10 "~~/src/Tools/isac/MathEngine/MathEngine"
11 (**)"HOL-SPARK.SPARK" (** ) preliminarily for parsing Example files *)
12 (** )"HOL-Word.Word"( ** ) trial on ERROR in definition sdiv below *)
14 "Example" :: thy_load ("str") (* "spark_vc" :: thy_goal *)
15 and "Problem" :: thy_decl (* root-problem + recursively in Solution;
16 "spark_vc" :: thy_goal *)
17 and "Specification" "Model" "References" "Solution" (* structure only *)
18 and"Given" "Find" "Relate" "Where" (* await input of term *)
19 and "RTheory" (* await input of string; "R" distingues "Problem".."RProblem" *)
20 and "RProblem" "RMethod" (* await input of string list *)
21 "Tactic" (* optional for each step 0..end of calculation *)
24 (**)ML_file parseC.sml(**)
26 section \<open>new code for Outer_Syntax Example, Problem, ...\<close>
28 subsection \<open>code for Example\<close>
31 structure Refs_Data = Theory_Data
34 val empty : T = References.empty
36 fun merge (_, refs) = refs
38 (*/----------------------------- shift to test/../? ----------------------------------------\*)
40 signature THEORY_DATA =
44 val put: T -> theory -> theory
45 val map: (T -> T) -> theory -> theory
48 Refs_Data.empty; (*in Refs_Data defined workers are hidden*)
49 Refs_Data.extend; (*in Refs_Data defined workers are hidden*)
50 Refs_Data.merge; (*in Refs_Data defined workers are hidden*)
52 Value or constructor (empty) has not been declared in structure Refs *)
54 Refs_Data.get: theory -> Refs_Data.T; (*from signature THEORY_DATA*)
55 Refs_Data.put: Refs_Data.T -> theory -> theory; (*from signature THEORY_DATA*)
56 Refs_Data.map: (Refs_Data.T -> Refs_Data.T) -> theory -> theory; (*from signature THEORY_DATA*)
57 (*\----------------------------- shift to test/../? ----------------------------------------/*)
59 structure OMod_Data = Theory_Data
64 fun merge (_, o_model) = o_model
67 structure Ctxt_Data = Theory_Data
69 type T = Proof.context
70 val empty : T = ContextC.empty
72 fun merge (_, ctxt) = ctxt
76 store_and_show: Formalise.T list -> theory -> theory;
78 fun store_and_show formalise thy =
80 (**)val file_read_correct = case formalise of xxx as
81 [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y", "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]", "AbleitungBiegelinie dy"],
82 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))] => hd xxx
83 | _ => error "magic failed: handling file exp_Statics_Biegel_Timischl_7-70.str failed"
85 val formalise = hd formalise (*we expect only one Formalise.T in the list*)
86 val (hdlPIDE, _, refs, o_model, var_type_ctxt) = Step_Specify.initialisePIDE formalise
87 (* ^^ TODO remove with cleanup in nxt_specify_init_calc *)
89 TODO: present "Problem hdlPIDE" via PIDE
94 |> OMod_Data.put o_model
95 |> Ctxt_Data.put var_type_ctxt
98 store_and_show: Formalise.T list -> theory -> theory;
101 fun load_formalisation parser (files, _) thy =
103 val ([{lines, pos, ...}: Token.file], thy') = files thy;
106 (ParseC.read_out_formalise (fst (parser (fst (ParseC.tokenize_formalise pos (cat_lines lines))))))
109 fun load_formalisation parse (files, _) thy =
111 val ([{lines, pos, ...}: Token.file], thy') = files thy;
112 val formalise = lines
114 |> ParseC.tokenize_formalise pos
118 |> ParseC.read_out_formalise
120 val _ = @{print} {a = "### load_formalisation \<rightarrow>", formalise = formalise}
127 subsection \<open>code to write Problem ("Biegelinie", ["Biegelinien"]) to thy\<close>
134 subsection \<open>code for Problem\<close>
136 Again, we copy code from spark_vc into Calculation.thy and
137 add functionality for Problem
138 such that the code keeps running during adaption from spark_vc to Problem.
143 subsubsection \<open>copied from fdl_parser.ML\<close>
149 | Quantifier of string * string list * string * expr
150 | Funct of string * expr list
151 | Element of expr * expr list
152 | Update of expr * expr list * expr
153 | Record of string * (string * expr) list
154 | Array of string * expr option *
155 ((expr * expr option) list list * expr) list;
159 | Enum_Type of string list
160 | Array_Type of string list * string
161 | Record_Type of (string list * string) list
164 (* also store items in a list to preserve order *)
165 type 'a tab = 'a Symtab.table * (string * 'a) list;
167 fun lookup ((tab, _) : 'a tab) = Symtab.lookup tab;
170 subsubsection \<open>copied from spark_vcs.ML\<close>
174 fun err_unfinished () = error "An unfinished SPARK environment is still open."
176 val strip_number = apply2 implode o chop_suffix Fdl_Lexer.is_digit o raw_explode;
178 val name_ord = prod_ord string_ord (option_ord int_ord) o
179 apply2 (strip_number ##> Int.fromString);
181 structure VCtab = Table(type key = string val ord = name_ord);
183 val builtin = Symtab.make (map (rpair ())
184 ["->", "<->", "or", "and", "not", "=", "<>", "<", ">", "<=", ">=",
185 "+", "-", "*", "/", "div", "mod", "**"]);
188 Symtab.defined builtin orf
189 can (unprefix "fld_") orf can (unprefix "upf_") orf
190 can (unsuffix "__pos") orf can (unsuffix "__val") orf
191 equal "succ" orf equal "pred";
193 fun fold_opt f = the_default I o Option.map f;
194 fun fold_pair f g (x, y) = f x #> g y;
196 fun fold_expr f g (Funct (s, es)) = f s #> fold (fold_expr f g) es
197 | fold_expr f g (Ident s) = g s
198 | fold_expr f g (Number _) = I
199 | fold_expr f g (Quantifier (_, _, _, e)) = fold_expr f g e
200 | fold_expr f g (Element (e, es)) =
201 fold_expr f g e #> fold (fold_expr f g) es
202 | fold_expr f g (Update (e, es, e')) =
203 fold_expr f g e #> fold (fold_expr f g) es #> fold_expr f g e'
204 | fold_expr f g (Record (_, flds)) = fold (fold_expr f g o snd) flds
205 | fold_expr f g (Array (_, default, assocs)) =
206 fold_opt (fold_expr f g) default #>
208 (fold (fold (fold_pair
209 (fold_expr f g) (fold_opt (fold_expr f g)))))
210 (fold_expr f g)) assocs;
212 fun add_expr_pfuns funs = fold_expr
213 (fn s => if is_pfun s then I else insert (op =) s)
214 (fn s => if is_none (lookup funs s) then I else insert (op =) s);
217 VCtab.fold (fn (_, (_, _, ps, cs)) => fold f ps #> fold f cs) vcs;
219 fun lookup_prfx "" tab s = Symtab.lookup tab s
220 | lookup_prfx prfx tab s = (case Symtab.lookup tab s of
221 NONE => Symtab.lookup tab (prfx ^ "__" ^ s)
224 fun pfuns_of_vcs prfx funs pfuns vcs =
225 fold_vcs (add_expr_pfuns funs o snd) vcs [] |>
226 filter (is_none o lookup_prfx prfx pfuns);
228 fun pfuns_of_vcs prfx funs pfuns vcs =
229 fold_vcs (add_expr_pfuns funs o snd) vcs [] |>
230 filter (is_none o lookup_prfx prfx pfuns);
232 structure VCs = Theory_Data
235 {pfuns: ((string list * string) option * term) Symtab.table,
236 type_map: (typ * (string * string) list) Symtab.table,
238 {ctxt: Element.context_i list,
239 defs: (binding * thm) list,
241 funs: (string list * string) tab,
242 pfuns: ((string list * string) option * term) Symtab.table,
243 ids: (term * string) Symtab.table * Name.context,
245 vcs: (string * thm list option *
246 (string * expr) list * (string * expr) list) VCtab.table,
248 prefix: string} option}
249 val empty : T = {pfuns = Symtab.empty, type_map = Symtab.empty, env = NONE}
251 fun merge ({pfuns = pfuns1, type_map = type_map1, env = NONE},
252 {pfuns = pfuns2, type_map = type_map2, env = NONE}) =
253 {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2),
254 type_map = Symtab.merge (op =) (type_map1, type_map2),
256 | merge _ = err_unfinished ()
259 fun get_type thy prfx ty =
260 let val {type_map, ...} = VCs.get thy
261 in lookup_prfx prfx type_map ty end;
263 fun mk_type' _ _ "integer" = (HOLogic.intT, [])
264 | mk_type' _ _ "boolean" = (HOLogic.boolT, [])
265 | mk_type' thy prfx ty =
266 (case get_type thy prfx ty of
268 (Syntax.check_typ (Proof_Context.init_global thy)
269 (Type (Sign.full_name thy (Binding.name ty), [])),
273 fun mk_type thy prfx ty = fst (mk_type' thy prfx ty);
275 fun pfun_type thy prfx (argtys, resty) =
276 map (mk_type thy prfx) argtys ---> mk_type thy prfx resty;
278 fun declare_missing_pfuns thy prfx funs pfuns vcs (tab, ctxt) =
280 val (fs, (tys, Ts)) =
281 pfuns_of_vcs prfx funs pfuns vcs |>
282 map_filter (fn s => lookup funs s |>
283 Option.map (fn ty => (s, (SOME ty, pfun_type thy prfx ty)))) |>
284 split_list ||> split_list;
285 val (fs', ctxt') = fold_map Name.variant fs ctxt
287 (fold Symtab.update_new (fs ~~ (tys ~~ map Free (fs' ~~ Ts))) pfuns,
288 Element.Fixes (map2 (fn s => fn T =>
289 (Binding.name s, SOME T, NoSyn)) fs' Ts),
293 fun strip_underscores s =
294 strip_underscores (unsuffix "_" s) handle Fail _ => s;
297 unsuffix "~" s ^ "_init" handle Fail _ => s;
299 val mangle_name = strip_underscores #> strip_tilde;
301 fun mk_variables thy prfx xs ty (tab, ctxt) =
303 val T = mk_type thy prfx ty;
304 val (ys, ctxt') = fold_map Name.variant (map mangle_name xs) ctxt;
305 val zs = map (Free o rpair T) ys;
306 in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end;
309 let val T = fastype_of t
310 in Const (s, T --> T) $ t end;
312 val booleanN = "boolean";
313 val integerN = "integer";
315 val to_lower = raw_explode #> map Symbol.to_ascii_lower #> implode;
316 val lcase_eq = (op =) o apply2 (to_lower o Long_Name.base_name);
318 fun find_field [] fname fields =
319 find_first (curry lcase_eq fname o fst) fields
320 | find_field cmap fname fields =
321 (case AList.lookup (op =) cmap fname of
323 | SOME fname' => SOME (fname', the (AList.lookup (op =) fields fname')));
325 fun get_record_info thy T = (case Record.dest_recTs T of
326 [(tyname, [\<^typ>\<open>unit\<close>])] =>
327 Record.get_info thy (Long_Name.qualifier tyname)
330 fun find_field' fname = get_first (fn (flds, fldty) =>
331 if member (op =) flds fname then SOME fldty else NONE);
333 fun invert_map [] = I
335 map (apfst (the o AList.lookup (op =) (map swap cmap)));
337 fun mk_times (t, u) =
339 val setT = fastype_of t;
340 val T = HOLogic.dest_setT setT;
341 val U = HOLogic.dest_setT (fastype_of u)
343 Const (\<^const_name>\<open>Sigma\<close>, setT --> (T --> HOLogic.mk_setT U) -->
344 HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u)
347 fun term_of_expr thy prfx types pfuns =
349 fun tm_of vs (Funct ("->", [e, e'])) =
350 (HOLogic.mk_imp (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
352 | tm_of vs (Funct ("<->", [e, e'])) =
353 (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
355 | tm_of vs (Funct ("or", [e, e'])) =
356 (HOLogic.mk_disj (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
358 | tm_of vs (Funct ("and", [e, e'])) =
359 (HOLogic.mk_conj (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
361 | tm_of vs (Funct ("not", [e])) =
362 (HOLogic.mk_not (fst (tm_of vs e)), booleanN)
364 | tm_of vs (Funct ("=", [e, e'])) =
365 (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
367 | tm_of vs (Funct ("<>", [e, e'])) = (HOLogic.mk_not
368 (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e'))), booleanN)
370 | tm_of vs (Funct ("<", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less\<close>
371 (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
373 | tm_of vs (Funct (">", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less\<close>
374 (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)
376 | tm_of vs (Funct ("<=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>
377 (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
379 | tm_of vs (Funct (">=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>
380 (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)
382 | tm_of vs (Funct ("+", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>plus\<close>
383 (fst (tm_of vs e), fst (tm_of vs e')), integerN)
385 | tm_of vs (Funct ("-", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>minus\<close>
386 (fst (tm_of vs e), fst (tm_of vs e')), integerN)
388 | tm_of vs (Funct ("*", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>times\<close>
389 (fst (tm_of vs e), fst (tm_of vs e')), integerN)
391 | tm_of vs (Funct ("/", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>divide\<close>
392 (fst (tm_of vs e), fst (tm_of vs e')), integerN)
394 | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>sdiv\<close>
395 (fst (tm_of vs e), fst (tm_of vs e')), integerN)
397 | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>modulo\<close>
398 (fst (tm_of vs e), fst (tm_of vs e')), integerN)
400 | tm_of vs (Funct ("-", [e])) =
401 (mk_unop \<^const_name>\<open>uminus\<close> (fst (tm_of vs e)), integerN)
403 | tm_of vs (Funct ("**", [e, e'])) =
404 (Const (\<^const_name>\<open>power\<close>, HOLogic.intT --> HOLogic.natT -->
405 HOLogic.intT) $ fst (tm_of vs e) $
406 (\<^const>\<open>nat\<close> $ fst (tm_of vs e')), integerN)
408 | tm_of (tab, _) (Ident s) =
409 (case Symtab.lookup tab s of
411 | NONE => (case lookup_prfx prfx pfuns s of
412 SOME (SOME ([], resty), t) => (t, resty)
413 | _ => error ("Undeclared identifier " ^ s)))
415 | tm_of _ (Number i) = (HOLogic.mk_number HOLogic.intT i, integerN)
417 | tm_of vs (Quantifier (s, xs, ty, e)) =
419 val (ys, vs') = mk_variables thy prfx xs ty vs;
421 "for_all" => HOLogic.mk_all
422 | "for_some" => HOLogic.mk_exists)
424 (fold_rev (fn Free (x, T) => fn t => q (x, T, t))
425 ys (fst (tm_of vs' e)),
429 | tm_of vs (Funct (s, es)) =
431 (* record field selection *)
432 (case try (unprefix "fld_") s of
433 SOME fname => (case es of
436 val (t, rcdty) = tm_of vs e;
437 val (rT, cmap) = mk_type' thy prfx rcdty
438 in case (get_record_info thy rT, lookup types rcdty) of
439 (SOME {fields, ...}, SOME (Record_Type fldtys)) =>
440 (case (find_field cmap fname fields,
441 find_field' fname fldtys) of
442 (SOME (fname', fT), SOME fldty) =>
443 (Const (fname', rT --> fT) $ t, fldty)
444 | _ => error ("Record " ^ rcdty ^
445 " has no field named " ^ fname))
446 | _ => error (rcdty ^ " is not a record type")
448 | _ => error ("Function " ^ s ^ " expects one argument"))
451 (* record field update *)
452 (case try (unprefix "upf_") s of
453 SOME fname => (case es of
456 val (t, rcdty) = tm_of vs e;
457 val (rT, cmap) = mk_type' thy prfx rcdty;
458 val (u, fldty) = tm_of vs e';
459 val fT = mk_type thy prfx fldty
460 in case get_record_info thy rT of
461 SOME {fields, ...} =>
462 (case find_field cmap fname fields of
465 (Const (fname' ^ "_update",
466 (fT --> fT) --> rT --> rT) $
467 Abs ("x", fT, u) $ t,
469 else error ("Type\n" ^
470 Syntax.string_of_typ_global thy fT ^
471 "\ndoes not match type\n" ^
472 Syntax.string_of_typ_global thy fU ^
473 "\nof field " ^ fname)
474 | NONE => error ("Record " ^ rcdty ^
475 " has no field named " ^ fname))
476 | _ => error (rcdty ^ " is not a record type")
478 | _ => error ("Function " ^ s ^ " expects two arguments"))
481 (* enumeration type to integer *)
482 (case try (unsuffix "__pos") s of
483 SOME tyname => (case es of
484 [e] => (Const (\<^const_name>\<open>pos\<close>,
485 mk_type thy prfx tyname --> HOLogic.intT) $ fst (tm_of vs e),
487 | _ => error ("Function " ^ s ^ " expects one argument"))
490 (* integer to enumeration type *)
491 (case try (unsuffix "__val") s of
492 SOME tyname => (case es of
493 [e] => (Const (\<^const_name>\<open>val\<close>,
494 HOLogic.intT --> mk_type thy prfx tyname) $ fst (tm_of vs e),
496 | _ => error ("Function " ^ s ^ " expects one argument"))
499 (* successor / predecessor of enumeration type element *)
500 if s = "succ" orelse s = "pred" then (case es of
503 val (t, tyname) = tm_of vs e;
504 val T = mk_type thy prfx tyname
506 (if s = "succ" then \<^const_name>\<open>succ\<close>
507 else \<^const_name>\<open>pred\<close>, T --> T) $ t, tyname)
509 | _ => error ("Function " ^ s ^ " expects one argument"))
511 (* user-defined proof function *)
513 (case lookup_prfx prfx pfuns s of
514 SOME (SOME (_, resty), t) =>
515 (list_comb (t, map (fst o tm_of vs) es), resty)
516 | _ => error ("Undeclared proof function " ^ s))))))
518 | tm_of vs (Element (e, es)) =
519 let val (t, ty) = tm_of vs e
520 in case lookup types ty of
521 SOME (Array_Type (_, elty)) =>
522 (t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es), elty)
523 | _ => error (ty ^ " is not an array type")
526 | tm_of vs (Update (e, es, e')) =
527 let val (t, ty) = tm_of vs e
528 in case lookup types ty of
529 SOME (Array_Type (idxtys, elty)) =>
531 val T = foldr1 HOLogic.mk_prodT
532 (map (mk_type thy prfx) idxtys);
533 val U = mk_type thy prfx elty;
536 (Const (\<^const_name>\<open>fun_upd\<close>, fT --> T --> U --> fT) $
537 t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es) $
541 | _ => error (ty ^ " is not an array type")
544 | tm_of vs (Record (s, flds)) =
546 val (T, cmap) = mk_type' thy prfx s;
547 val {extension = (ext_name, _), fields, ...} =
548 (case get_record_info thy T of
549 NONE => error (s ^ " is not a record type")
550 | SOME info => info);
551 val flds' = map (apsnd (tm_of vs)) flds;
552 val fnames = fields |> invert_map cmap |>
553 map (Long_Name.base_name o fst);
554 val fnames' = map fst flds;
555 val (fvals, ftys) = split_list (map (fn s' =>
556 case AList.lookup lcase_eq flds' s' of
557 SOME fval_ty => fval_ty
558 | NONE => error ("Field " ^ s' ^ " missing in record " ^ s))
560 val _ = (case subtract lcase_eq fnames fnames' of
562 | xs => error ("Extra field(s) " ^ commas xs ^
564 val _ = (case duplicates (op =) fnames' of
566 | xs => error ("Duplicate field(s) " ^ commas xs ^
571 map (mk_type thy prfx) ftys @ [HOLogic.unitT] ---> T),
572 fvals @ [HOLogic.unit]),
576 | tm_of vs (Array (s, default, assocs)) =
577 (case lookup types s of
578 SOME (Array_Type (idxtys, elty)) =>
580 val Ts = map (mk_type thy prfx) idxtys;
581 val T = foldr1 HOLogic.mk_prodT Ts;
582 val U = mk_type thy prfx elty;
583 fun mk_idx' T (e, NONE) = HOLogic.mk_set T [fst (tm_of vs e)]
584 | mk_idx' T (e, SOME e') = Const (\<^const_name>\<open>atLeastAtMost\<close>,
585 T --> T --> HOLogic.mk_setT T) $
586 fst (tm_of vs e) $ fst (tm_of vs e');
588 if length Ts <> length idx then
589 error ("Arity mismatch in construction of array " ^ s)
590 else foldr1 mk_times (map2 mk_idx' Ts idx);
591 fun mk_upd (idxs, e) t =
592 if length idxs = 1 andalso forall (is_none o snd) (hd idxs)
594 Const (\<^const_name>\<open>fun_upd\<close>, (T --> U) -->
595 T --> U --> T --> U) $ t $
596 foldl1 HOLogic.mk_prod
597 (map (fst o tm_of vs o fst) (hd idxs)) $
600 Const (\<^const_name>\<open>fun_upds\<close>, (T --> U) -->
601 HOLogic.mk_setT T --> U --> T --> U) $ t $
602 foldl1 (HOLogic.mk_binop \<^const_name>\<open>sup\<close>)
608 SOME e => Abs ("x", T, fst (tm_of vs e))
609 | NONE => Const (\<^const_name>\<open>undefined\<close>, T --> U)),
612 | _ => error (s ^ " is not an array type"))
616 fun mk_pat s = (case Int.fromString s of
617 SOME i => [HOLogic.mk_Trueprop (Var (("C", i), HOLogic.boolT))]
618 | NONE => error ("Bad conclusion identifier: C" ^ s));
620 fun mk_vc thy prfx types pfuns ids name_concl (tr, proved, ps, cs) =
622 HOLogic.mk_Trueprop o fst o term_of_expr thy prfx types pfuns ids
625 Element.Assumes (map (fn (s', e) =>
626 ((Binding.name ("H" ^ s'), []), [(prop_of e, [])])) ps),
627 Element.Shows (map (fn (s', e) =>
628 (if name_concl then (Binding.name ("C" ^ s'), [])
629 else Binding.empty_atts,
630 [(prop_of e, mk_pat s')])) cs))
633 (*val lookup_vc: theory -> bool -> string -> (Element.context_i list *
634 (string * thm list option * Element.context_i * Element.statement_i)) option
636 fun lookup_vc thy name_concl name =
638 {env = SOME {vcs, types, funs, pfuns, ids, ctxt, prefix, ...}, ...} =>
639 (case VCtab.lookup vcs name of
641 let val (pfuns', ctxt', ids') =
642 declare_missing_pfuns thy prefix funs pfuns vcs ids
644 SOME (ctxt @ [ctxt'],
645 mk_vc thy prefix types pfuns' ids' name_concl vc)
651 subsubsection \<open>copied from spark_commands.ML\<close>
654 fun get_vc thy vc_name =
655 (case SPARK_VCs.lookup_vc thy false vc_name of
656 SOME (ctxt, (_, proved, ctxt', stmt)) =>
657 if is_some proved then
658 error ("The verification condition " ^
659 quote vc_name ^ " has already been proved.")
660 else (ctxt @ [ctxt'], stmt)
661 | NONE => error ("There is no verification condition " ^
662 quote vc_name ^ "."));
665 val prefer_input: ThyC.id * Problem.id -> References.T -> O_Model.T -> References.T * O_Model.T
667 fun prefer_input (inthy, inpbl : Problem.id) (thy, pbl, met_id) o_model =
668 if inthy = thy andalso inpbl = pbl
669 then ((thy, pbl, met_id) : References.T, o_model)
670 else ((inthy, inpbl, Method.id_empty), [])
673 val prove_vc: ParseC.problem -> Proof.context -> Proof.state
675 fun prove_vc (*vc_name*)problem lthy =
677 val _ = @{print} {a = "//--- Spark_Commands.prove_vc", headline = problem}
678 val thy = Proof_Context.theory_of lthy;
679 val vc_name = "procedure_g_c_d_4" (*fixed for spark_open \<open>greatest_common_divisor/g_c_d\<close>*)
680 val (ctxt, stmt) = get_vc thy vc_name
681 (*//--------------------------------- new code --------------------------------\\*)
682 val {thy_id, pbl_id, (*givens, wheres, ..*)...} = ParseC.read_out_problem problem
683 val refs' = Refs_Data.get thy
684 val (refs as (_, pbl_id, _), o_model) = prefer_input (thy_id, pbl_id) refs' (OMod_Data.get thy)
685 val i_model = I_Model.initPIDE pbl_id
687 TODO: present Specification = i_model () + refs via PIDE
689 (*----------------------------------- new code ----------------------------------*)
690 val _ = @{print} {a = "prove_vc", o_model = o_model, refs = refs, i_model = i_model}
691 (*\\--------------------------------- new code --------------------------------//*)
693 Specification.theorem true Thm.theoremK NONE
694 (fn thmss => (Local_Theory.background_theory
695 (SPARK_VCs.mark_proved vc_name (flat thmss))))
696 (Binding.name vc_name, []) [] ctxt stmt false lthy
699 prove_vc: ParseC.problem -> Proof.context -> Proof.state
703 section \<open>setup command_keyword \<close>
707 Outer_Syntax.command \<^command_keyword>\<open>Example\<close> "start a Calculation from a Formalise-file"
708 (Resources.provide_parse_files "Example" -- Parse.parname
709 >> (Toplevel.theory o (load_formalisation ParseC.formalisation)));
712 Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>Problem\<close>
713 "start a Specification, either from scratch or from preceding 'Example'"
714 (ParseC.problem >> prove_vc);
718 subsection \<open>test runs with Example\<close>
719 subsubsection \<open>with new code\<close>
721 Starting the Calculation for the Example requires session Isac with Isac.Biegelinie etc.
722 So, do ~~$ ./zcoding-to-test.sh and use Test_Some.thy to evaluate
724 Example \<open>/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>
726 This now gives no error, but also no <Output>. See child of 3ea616c84845.
729 subsubsection \<open>with original SPARK code\<close>
731 The sequence of code below is copied from SPARK/Examples/Gcd/Greatest_Common_Divisor.thy.
732 But here the code works only partially (see ERROR at end).
733 Thus it is advisable to run tests in Test_Some.thy, where "Example" has "Biegelinie".
735 spark_proof_functions is required for proof below..
737 (*//------------------- outcomment before creating session Isac ----------------------------\\* )
739 spark_proof_functions gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"
741 spark_open \<open>~~/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>
743 The following verification conditions remain to be proved:
747 spark_vc procedure_g_c_d_4
749 from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)
750 with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1
751 by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric])
754 from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)
755 with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1
756 by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric])
758 from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> show ?C2
759 by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric] gcd_non_0_int)
764 spark_vc procedure_g_c_d_11
768 ( *Bad path binding: "$ISABELLE_HOME/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.prv"*)
770 ( *\\------------------- outcomment before creating session Isac ----------------------------//*)
773 section \<open>adapt spark_vc to Problem using Naproche as model\<close>
775 subsection \<open>survey on steps of investigation\<close>
777 We stopped step 3.4 going down from Outer_Syntax.local_theory_to_proof into proof.
778 Now we go the other way: Naproche checks the input via the Isabelle/server
779 and outputs highlighting, semantic annotations and errors via PIDE ---
780 and we investigate the output.
782 Investigation of Naproche showed, that annotations are ONLY sent bY
783 Output.report: string list -> unit, where string holds markup.
784 For Output.report @ {print} is NOT available, so we guard all respective calls.
785 However, NO @ {print} available in src/Pure is reached by "spark_vc procedure_g_c_d_4"
786 [[note: writeln is available earlier then print, e.g. in Pure/Isar/parse.ML]]
789 subsection \<open>notes and testbed for Naproche in preliminary spark_vcs\<close>
796 subsection \<open>testbed for Problem\<close>
804 end(* SEE "outcomment before creating session Isac" ABOVE !!! OTHERWISE YOU HAVE..
805 ERROR: Found the end of the theory, but the last SPARK environment is still open.
806 ..is acceptable for testing spark_vc .. proof - ...