(*  Title:      src/Tools/isac/BridgeJEdit/Calculation.thy

    Author:     Walther Neuper, JKU Linz

    (c) due to copyright terms

Outer syntax for Isabelle/Isac's Calculation.

*)

theory Calculation

imports

  "~~/src/Tools/isac/MathEngine/MathEngine"

(**)"HOL-SPARK.SPARK" (** ) preliminarily for parsing Example files *)

(** )"HOL-Word.Word"( ** ) trial on ERROR in definition sdiv below *)

keywords

    "Example" :: thy_load ("str") (* "spark_vc" :: thy_goal *)

  and "Problem" :: thy_decl (* root-problem + recursively in Solution;

                               "spark_vc" :: thy_goal *)

  and "Specification" "Model" "References" "Solution" (* structure only *)

  and"Given" "Find" "Relate" "Where" (* await input of term *)

  and "RTheory" (* await input of string; "R" distingues "Problem".."RProblem" *)

  and "RProblem" "RMethod" (* await input of string list *)

    "Tactic" (* optional for each step 0..end of calculation *)

begin

(**)ML_file parseC.sml(**)

section \<open>new code for Outer_Syntax Example, Problem, ...\<close>

subsection \<open>code for Example\<close>

ML \<open>

\<close> ML \<open>

structure Refs_Data = Theory_Data

(

  type T = References.T

  val empty : T = References.empty

  val extend = I

  fun merge (_, refs) = refs

);

(*/----------------------------- shift to test/../? ----------------------------------------\*)

(* Pure/context.ML

signature THEORY_DATA =

sig

  type T

  val get: theory -> T

  val put: T -> theory -> theory

  val map: (T -> T) -> theory -> theory

end;*)

(*

Refs_Data.empty;                                    (*in Refs_Data defined workers are hidden*)

Refs_Data.extend;                                   (*in Refs_Data defined workers are hidden*)

Refs_Data.merge;                                    (*in Refs_Data defined workers are hidden*)

ML error\<^here>:

Value or constructor (empty) has not been declared in structure Refs *)

Refs_Data.get: theory -> Refs_Data.T;                            (*from signature THEORY_DATA*)

Refs_Data.put: Refs_Data.T -> theory -> theory;                  (*from signature THEORY_DATA*)

Refs_Data.map: (Refs_Data.T -> Refs_Data.T) -> theory -> theory; (*from signature THEORY_DATA*)

(*\----------------------------- shift to test/../? ----------------------------------------/*)

\<close> ML \<open>

structure OMod_Data = Theory_Data

(

  type T = O_Model.T

  val empty : T = []

  val extend = I

  fun merge (_, o_model) = o_model

)

\<close> ML \<open>

structure Ctxt_Data = Theory_Data

(

  type T = Proof.context

  val empty : T = ContextC.empty

  val extend = I

  fun merge (_, ctxt) = ctxt

)

\<close> ML \<open>

(*

store_and_show: Formalise.T list -> theory -> theory;

*)

fun store_and_show formalise thy =

  let

(**)val file_read_correct = case formalise of xxx as

      [(["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"],

        ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))] => hd xxx

      | _ => error "magic failed: handling file exp_Statics_Biegel_Timischl_7-70.str failed"

(**)

    val formalise = hd formalise (*we expect only one Formalise.T in the list*)

    val (hdlPIDE, _, refs, o_model, var_type_ctxt) = Step_Specify.initialisePIDE formalise

  (*              ^^ TODO remove with cleanup in nxt_specify_init_calc *)

(*

  TODO: present "Problem hdlPIDE" via PIDE

*)

  in

    thy

      |> Refs_Data.put refs

      |> OMod_Data.put o_model

      |> Ctxt_Data.put var_type_ctxt

  end;

\<close> ML \<open>

store_and_show: Formalise.T list -> theory -> theory;

\<close> ML \<open>

\<close> ML \<open>

fun load_formalisation parser (files, _) thy =

  let

    val ([{lines, pos, ...}: Token.file], thy') = files thy;

  in

    store_and_show

      (ParseC.read_out_formalise (fst (parser (fst (ParseC.tokenize_formalise pos (cat_lines lines))))))

        thy'

  end;

fun load_formalisation parse (files, _) thy =

  let

    val ([{lines, pos, ...}: Token.file], thy') = files thy;

    val formalise = lines

      |> cat_lines 

      |> ParseC.tokenize_formalise pos

      |> fst

      |> parse

      |> fst

      |> ParseC.read_out_formalise

      |> store_and_show

    val _ = @{print} {a = "### load_formalisation \<rightarrow>", formalise = formalise}

  in

    formalise thy'

  end;

\<close> ML \<open>

\<close>

subsection \<open>code to write Problem ("Biegelinie", ["Biegelinien"]) to thy\<close>

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

subsection \<open>code for Problem\<close>

text \<open>

  Again, we copy code from spark_vc into Calculation.thy and

  add functionality for Problem

  such that the code keeps running during adaption from spark_vc to Problem.

\<close> ML \<open>

\<close> ML \<open>

\<close> 

subsubsection \<open>copied from fdl_parser.ML\<close>

ML \<open>

\<close> ML \<open>

datatype expr =

    Ident of string

  | Number of int

  | Quantifier of string * string list * string * expr

  | Funct of string * expr list

  | Element of expr * expr list

  | Update of expr * expr list * expr

  | Record of string * (string * expr) list

  | Array of string * expr option *

      ((expr * expr option) list list * expr) list;

\<close> ML \<open>

  datatype fdl_type =

      Basic_Type of string

    | Enum_Type of string list

    | Array_Type of string list * string

    | Record_Type of (string list * string) list

    | Pending_Type;

\<close> ML \<open>

(* also store items in a list to preserve order *)

type 'a tab = 'a Symtab.table * (string * 'a) list;

\<close> ML \<open>

fun lookup ((tab, _) : 'a tab) = Symtab.lookup tab;

\<close> ML \<open>

\<close>

subsubsection \<open>copied from spark_vcs.ML\<close>

ML \<open>

\<close> ML \<open>

(**)

fun err_unfinished () = error "An unfinished SPARK environment is still open."

\<close> ML \<open>

val strip_number = apply2 implode o chop_suffix Fdl_Lexer.is_digit o raw_explode;

\<close> ML \<open>

val name_ord = prod_ord string_ord (option_ord int_ord) o

  apply2 (strip_number ##> Int.fromString);

\<close> ML \<open>

structure VCtab = Table(type key = string val ord = name_ord);

\<close> ML \<open>

val builtin = Symtab.make (map (rpair ())

  ["->", "<->", "or", "and", "not", "=", "<>", "<", ">", "<=", ">=",

   "+", "-", "*", "/", "div", "mod", "**"]);

\<close> ML \<open>

val is_pfun =

  Symtab.defined builtin orf

  can (unprefix "fld_") orf can (unprefix "upf_") orf

  can (unsuffix "__pos") orf can (unsuffix "__val") orf

  equal "succ" orf equal "pred";

\<close> ML \<open>

fun fold_opt f = the_default I o Option.map f;

fun fold_pair f g (x, y) = f x #> g y;

\<close> ML \<open>

fun fold_expr f g (Funct (s, es)) = f s #> fold (fold_expr f g) es

  | fold_expr f g (Ident s) = g s

  | fold_expr f g (Number _) = I

  | fold_expr f g (Quantifier (_, _, _, e)) = fold_expr f g e

  | fold_expr f g (Element (e, es)) =

      fold_expr f g e #> fold (fold_expr f g) es

  | fold_expr f g (Update (e, es, e')) =

      fold_expr f g e #> fold (fold_expr f g) es #> fold_expr f g e'

  | fold_expr f g (Record (_, flds)) = fold (fold_expr f g o snd) flds

  | fold_expr f g (Array (_, default, assocs)) =

      fold_opt (fold_expr f g) default #>

      fold (fold_pair

        (fold (fold (fold_pair

          (fold_expr f g) (fold_opt (fold_expr f g)))))

        (fold_expr f g)) assocs;

\<close> ML \<open>

fun add_expr_pfuns funs = fold_expr

  (fn s => if is_pfun s then I else insert (op =) s)

  (fn s => if is_none (lookup funs s) then I else insert (op =) s);

\<close> ML \<open>

fun fold_vcs f vcs =

  VCtab.fold (fn (_, (_, _, ps, cs)) => fold f ps #> fold f cs) vcs;

\<close> ML \<open>

fun lookup_prfx "" tab s = Symtab.lookup tab s

  | lookup_prfx prfx tab s = (case Symtab.lookup tab s of

        NONE => Symtab.lookup tab (prfx ^ "__" ^ s)

      | x => x);

\<close> ML \<open>

fun pfuns_of_vcs prfx funs pfuns vcs =

  fold_vcs (add_expr_pfuns funs o snd) vcs [] |>

  filter (is_none o lookup_prfx prfx pfuns);

\<close> ML \<open>

fun pfuns_of_vcs prfx funs pfuns vcs =

  fold_vcs (add_expr_pfuns funs o snd) vcs [] |>

  filter (is_none o lookup_prfx prfx pfuns);

\<close> ML \<open>

structure VCs = Theory_Data

(

  type T =

    {pfuns: ((string list * string) option * term) Symtab.table,

     type_map: (typ * (string * string) list) Symtab.table,

     env:

       {ctxt: Element.context_i list,

        defs: (binding * thm) list,

        types: fdl_type tab,

        funs: (string list * string) tab,

        pfuns: ((string list * string) option * term) Symtab.table,

        ids: (term * string) Symtab.table * Name.context,

        proving: bool,

        vcs: (string * thm list option *

          (string * expr) list * (string * expr) list) VCtab.table,

        path: Path.T,

        prefix: string} option}

  val empty : T = {pfuns = Symtab.empty, type_map = Symtab.empty, env = NONE}

  val extend = I

  fun merge ({pfuns = pfuns1, type_map = type_map1, env = NONE},

        {pfuns = pfuns2, type_map = type_map2, env = NONE}) =

        {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2),

         type_map = Symtab.merge (op =) (type_map1, type_map2),

         env = NONE}

    | merge _ = err_unfinished ()

)

\<close> ML \<open>

fun get_type thy prfx ty =

  let val {type_map, ...} = VCs.get thy

  in lookup_prfx prfx type_map ty end;

\<close> ML \<open>

fun mk_type' _ _ "integer" = (HOLogic.intT, [])

  | mk_type' _ _ "boolean" = (HOLogic.boolT, [])

  | mk_type' thy prfx ty =

      (case get_type thy prfx ty of

         NONE =>

           (Syntax.check_typ (Proof_Context.init_global thy)

              (Type (Sign.full_name thy (Binding.name ty), [])),

            [])

       | SOME p => p);

\<close> ML \<open>

fun mk_type thy prfx ty = fst (mk_type' thy prfx ty);

\<close> ML \<open>

fun pfun_type thy prfx (argtys, resty) =

  map (mk_type thy prfx) argtys ---> mk_type thy prfx resty;

\<close> ML \<open>

fun declare_missing_pfuns thy prfx funs pfuns vcs (tab, ctxt) =

  let

    val (fs, (tys, Ts)) =

      pfuns_of_vcs prfx funs pfuns vcs |>

      map_filter (fn s => lookup funs s |>

        Option.map (fn ty => (s, (SOME ty, pfun_type thy prfx ty)))) |>

      split_list ||> split_list;

    val (fs', ctxt') = fold_map Name.variant fs ctxt

  in

    (fold Symtab.update_new (fs ~~ (tys ~~ map Free (fs' ~~ Ts))) pfuns,

     Element.Fixes (map2 (fn s => fn T =>

       (Binding.name s, SOME T, NoSyn)) fs' Ts),

     (tab, ctxt'))

  end;

\<close> ML \<open>

fun strip_underscores s =

  strip_underscores (unsuffix "_" s) handle Fail _ => s;

fun strip_tilde s =

  unsuffix "~" s ^ "_init" handle Fail _ => s;

\<close> ML \<open>

val mangle_name = strip_underscores #> strip_tilde;

\<close> ML \<open>

fun mk_variables thy prfx xs ty (tab, ctxt) =

  let

    val T = mk_type thy prfx ty;

    val (ys, ctxt') = fold_map Name.variant (map mangle_name xs) ctxt;

    val zs = map (Free o rpair T) ys;

  in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end;

\<close> ML \<open>

fun mk_unop s t =

  let val T = fastype_of t

  in Const (s, T --> T) $ t end;

\<close> ML \<open>

val booleanN = "boolean";

val integerN = "integer";

\<close> ML \<open>

val to_lower = raw_explode #> map Symbol.to_ascii_lower #> implode;

val lcase_eq = (op =) o apply2 (to_lower o Long_Name.base_name);

\<close> ML \<open>

fun find_field [] fname fields =

      find_first (curry lcase_eq fname o fst) fields

  | find_field cmap fname fields =

      (case AList.lookup (op =) cmap fname of

         NONE => NONE

       | SOME fname' => SOME (fname', the (AList.lookup (op =) fields fname')));

\<close> ML \<open>

fun get_record_info thy T = (case Record.dest_recTs T of

    [(tyname, [\<^typ>\<open>unit\<close>])] =>

      Record.get_info thy (Long_Name.qualifier tyname)

  | _ => NONE);

\<close> ML \<open>

fun find_field' fname = get_first (fn (flds, fldty) =>

  if member (op =) flds fname then SOME fldty else NONE);

\<close> ML \<open>

fun invert_map [] = I

  | invert_map cmap =

      map (apfst (the o AList.lookup (op =) (map swap cmap)));

\<close> ML \<open>

fun mk_times (t, u) =

  let

    val setT = fastype_of t;

    val T = HOLogic.dest_setT setT;

    val U = HOLogic.dest_setT (fastype_of u)

  in

    Const (\<^const_name>\<open>Sigma\<close>, setT --> (T --> HOLogic.mk_setT U) -->

      HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u)

  end;

\<close> ML \<open>

fun term_of_expr thy prfx types pfuns =

  let

    fun tm_of vs (Funct ("->", [e, e'])) =

          (HOLogic.mk_imp (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

      | tm_of vs (Funct ("<->", [e, e'])) =

          (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

      | tm_of vs (Funct ("or", [e, e'])) =

          (HOLogic.mk_disj (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

      | tm_of vs (Funct ("and", [e, e'])) =

          (HOLogic.mk_conj (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

      | tm_of vs (Funct ("not", [e])) =

          (HOLogic.mk_not (fst (tm_of vs e)), booleanN)

      | tm_of vs (Funct ("=", [e, e'])) =

          (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

      | tm_of vs (Funct ("<>", [e, e'])) = (HOLogic.mk_not

          (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e'))), booleanN)

      | tm_of vs (Funct ("<", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less\<close>

          (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

      | tm_of vs (Funct (">", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less\<close>

          (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)

      | tm_of vs (Funct ("<=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>

          (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

      | tm_of vs (Funct (">=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>

          (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)

      | tm_of vs (Funct ("+", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>plus\<close>

          (fst (tm_of vs e), fst (tm_of vs e')), integerN)

      | tm_of vs (Funct ("-", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>minus\<close>

          (fst (tm_of vs e), fst (tm_of vs e')), integerN)

      | tm_of vs (Funct ("*", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>times\<close>

          (fst (tm_of vs e), fst (tm_of vs e')), integerN)

      | tm_of vs (Funct ("/", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>divide\<close>

          (fst (tm_of vs e), fst (tm_of vs e')), integerN)

      | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>sdiv\<close>

          (fst (tm_of vs e), fst (tm_of vs e')), integerN)

      | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>modulo\<close>

          (fst (tm_of vs e), fst (tm_of vs e')), integerN)

      | tm_of vs (Funct ("-", [e])) =

          (mk_unop \<^const_name>\<open>uminus\<close> (fst (tm_of vs e)), integerN)

      | tm_of vs (Funct ("**", [e, e'])) =

          (Const (\<^const_name>\<open>power\<close>, HOLogic.intT --> HOLogic.natT -->

             HOLogic.intT) $ fst (tm_of vs e) $

               (\<^const>\<open>nat\<close> $ fst (tm_of vs e')), integerN)

      | tm_of (tab, _) (Ident s) =

          (case Symtab.lookup tab s of

             SOME t_ty => t_ty

           | NONE => (case lookup_prfx prfx pfuns s of

               SOME (SOME ([], resty), t) => (t, resty)

             | _ => error ("Undeclared identifier " ^ s)))

      | tm_of _ (Number i) = (HOLogic.mk_number HOLogic.intT i, integerN)

      | tm_of vs (Quantifier (s, xs, ty, e)) =

          let

            val (ys, vs') = mk_variables thy prfx xs ty vs;

            val q = (case s of

                "for_all" => HOLogic.mk_all

              | "for_some" => HOLogic.mk_exists)

          in

            (fold_rev (fn Free (x, T) => fn t => q (x, T, t))

               ys (fst (tm_of vs' e)),

             booleanN)

          end

      | tm_of vs (Funct (s, es)) =

          (* record field selection *)

          (case try (unprefix "fld_") s of

             SOME fname => (case es of

               [e] =>

                 let

                   val (t, rcdty) = tm_of vs e;

                   val (rT, cmap) = mk_type' thy prfx rcdty

                 in case (get_record_info thy rT, lookup types rcdty) of

                     (SOME {fields, ...}, SOME (Record_Type fldtys)) =>

                       (case (find_field cmap fname fields,

                            find_field' fname fldtys) of

                          (SOME (fname', fT), SOME fldty) =>

                            (Const (fname', rT --> fT) $ t, fldty)

                        | _ => error ("Record " ^ rcdty ^

                            " has no field named " ^ fname))

                   | _ => error (rcdty ^ " is not a record type")

                 end

             | _ => error ("Function " ^ s ^ " expects one argument"))

           | NONE =>

          (* record field update *)

          (case try (unprefix "upf_") s of

             SOME fname => (case es of

               [e, e'] =>

                 let

                   val (t, rcdty) = tm_of vs e;

                   val (rT, cmap) = mk_type' thy prfx rcdty;

                   val (u, fldty) = tm_of vs e';

                   val fT = mk_type thy prfx fldty

                 in case get_record_info thy rT of

                     SOME {fields, ...} =>

                       (case find_field cmap fname fields of

                          SOME (fname', fU) =>

                            if fT = fU then

                              (Const (fname' ^ "_update",

                                 (fT --> fT) --> rT --> rT) $

                                   Abs ("x", fT, u) $ t,

                               rcdty)

                            else error ("Type\n" ^

                              Syntax.string_of_typ_global thy fT ^

                              "\ndoes not match type\n" ^

                              Syntax.string_of_typ_global thy fU ^

                              "\nof field " ^ fname)

                        | NONE => error ("Record " ^ rcdty ^

                            " has no field named " ^ fname))

                   | _ => error (rcdty ^ " is not a record type")

                 end

             | _ => error ("Function " ^ s ^ " expects two arguments"))

           | NONE =>

          (* enumeration type to integer *)

          (case try (unsuffix "__pos") s of

             SOME tyname => (case es of

               [e] => (Const (\<^const_name>\<open>pos\<close>,

                   mk_type thy prfx tyname --> HOLogic.intT) $ fst (tm_of vs e),

                 integerN)

             | _ => error ("Function " ^ s ^ " expects one argument"))

           | NONE =>

          (* integer to enumeration type *)

          (case try (unsuffix "__val") s of

             SOME tyname => (case es of

               [e] => (Const (\<^const_name>\<open>val\<close>,

                   HOLogic.intT --> mk_type thy prfx tyname) $ fst (tm_of vs e),

                 tyname)

             | _ => error ("Function " ^ s ^ " expects one argument"))

           | NONE =>

          (* successor / predecessor of enumeration type element *)

          if s = "succ" orelse s = "pred" then (case es of

              [e] =>

                let

                  val (t, tyname) = tm_of vs e;

                  val T = mk_type thy prfx tyname

                in (Const

                  (if s = "succ" then \<^const_name>\<open>succ\<close>

                   else \<^const_name>\<open>pred\<close>, T --> T) $ t, tyname)

                end

            | _ => error ("Function " ^ s ^ " expects one argument"))

          (* user-defined proof function *)

          else

            (case lookup_prfx prfx pfuns s of

               SOME (SOME (_, resty), t) =>

                 (list_comb (t, map (fst o tm_of vs) es), resty)

             | _ => error ("Undeclared proof function " ^ s))))))

      | tm_of vs (Element (e, es)) =

          let val (t, ty) = tm_of vs e

          in case lookup types ty of

              SOME (Array_Type (_, elty)) =>

                (t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es), elty)

            | _ => error (ty ^ " is not an array type")

          end

      | tm_of vs (Update (e, es, e')) =

          let val (t, ty) = tm_of vs e

          in case lookup types ty of

              SOME (Array_Type (idxtys, elty)) =>

                let

                  val T = foldr1 HOLogic.mk_prodT

                    (map (mk_type thy prfx) idxtys);

                  val U = mk_type thy prfx elty;

                  val fT = T --> U

                in

                  (Const (\<^const_name>\<open>fun_upd\<close>, fT --> T --> U --> fT) $

                     t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es) $

                       fst (tm_of vs e'),

                   ty)

                end

            | _ => error (ty ^ " is not an array type")

          end

      | tm_of vs (Record (s, flds)) =

          let

            val (T, cmap) = mk_type' thy prfx s;

            val {extension = (ext_name, _), fields, ...} =

              (case get_record_info thy T of

                 NONE => error (s ^ " is not a record type")

               | SOME info => info);

            val flds' = map (apsnd (tm_of vs)) flds;

            val fnames = fields |> invert_map cmap |>

              map (Long_Name.base_name o fst);

            val fnames' = map fst flds;

            val (fvals, ftys) = split_list (map (fn s' =>

              case AList.lookup lcase_eq flds' s' of

                SOME fval_ty => fval_ty

              | NONE => error ("Field " ^ s' ^ " missing in record " ^ s))

                  fnames);

            val _ = (case subtract lcase_eq fnames fnames' of

                [] => ()

              | xs => error ("Extra field(s) " ^ commas xs ^

                  " in record " ^ s));

            val _ = (case duplicates (op =) fnames' of

                [] => ()

              | xs => error ("Duplicate field(s) " ^ commas xs ^

                  " in record " ^ s))

          in

            (list_comb

               (Const (ext_name,

                  map (mk_type thy prfx) ftys @ [HOLogic.unitT] ---> T),

                fvals @ [HOLogic.unit]),

             s)

          end

      | tm_of vs (Array (s, default, assocs)) =

          (case lookup types s of

             SOME (Array_Type (idxtys, elty)) =>

               let

                 val Ts = map (mk_type thy prfx) idxtys;

                 val T = foldr1 HOLogic.mk_prodT Ts;

                 val U = mk_type thy prfx elty;

                 fun mk_idx' T (e, NONE) = HOLogic.mk_set T [fst (tm_of vs e)]

                   | mk_idx' T (e, SOME e') = Const (\<^const_name>\<open>atLeastAtMost\<close>,

                       T --> T --> HOLogic.mk_setT T) $

                         fst (tm_of vs e) $ fst (tm_of vs e');

                 fun mk_idx idx =

                   if length Ts <> length idx then

                     error ("Arity mismatch in construction of array " ^ s)

                   else foldr1 mk_times (map2 mk_idx' Ts idx);

                 fun mk_upd (idxs, e) t =

                   if length idxs = 1 andalso forall (is_none o snd) (hd idxs)

                   then

                     Const (\<^const_name>\<open>fun_upd\<close>, (T --> U) -->

                         T --> U --> T --> U) $ t $

                       foldl1 HOLogic.mk_prod

                         (map (fst o tm_of vs o fst) (hd idxs)) $

                       fst (tm_of vs e)

                   else

                     Const (\<^const_name>\<open>fun_upds\<close>, (T --> U) -->

                         HOLogic.mk_setT T --> U --> T --> U) $ t $

                       foldl1 (HOLogic.mk_binop \<^const_name>\<open>sup\<close>)

                         (map mk_idx idxs) $

                       fst (tm_of vs e)

               in

                 (fold mk_upd assocs

                    (case default of

                       SOME e => Abs ("x", T, fst (tm_of vs e))

                     | NONE => Const (\<^const_name>\<open>undefined\<close>, T --> U)),

                  s)

               end

           | _ => error (s ^ " is not an array type"))

  in tm_of end;

\<close> ML \<open>

fun mk_pat s = (case Int.fromString s of

    SOME i => [HOLogic.mk_Trueprop (Var (("C", i), HOLogic.boolT))]

  | NONE => error ("Bad conclusion identifier: C" ^ s));

\<close> ML \<open>

fun mk_vc thy prfx types pfuns ids name_concl (tr, proved, ps, cs) =

  let val prop_of =

    HOLogic.mk_Trueprop o fst o term_of_expr thy prfx types pfuns ids

  in

    (tr, proved,

     Element.Assumes (map (fn (s', e) =>

       ((Binding.name ("H" ^ s'), []), [(prop_of e, [])])) ps),

     Element.Shows (map (fn (s', e) =>

       (if name_concl then (Binding.name ("C" ^ s'), [])

        else Binding.empty_atts,

        [(prop_of e, mk_pat s')])) cs))

  end;

\<close> ML \<open>

(*val lookup_vc: theory -> bool -> string -> (Element.context_i list *

    (string * thm list option * Element.context_i * Element.statement_i)) option

*)

fun lookup_vc thy name_concl name =

  (case VCs.get thy of

    {env = SOME {vcs, types, funs, pfuns, ids, ctxt, prefix, ...}, ...} =>

      (case VCtab.lookup vcs name of

         SOME vc =>

           let val (pfuns', ctxt', ids') =

             declare_missing_pfuns thy prefix funs pfuns vcs ids

           in

             SOME (ctxt @ [ctxt'],

               mk_vc thy prefix types pfuns' ids' name_concl vc)

           end

       | NONE => NONE)

  | _ => NONE);

\<close> ML \<open>

\<close> 

subsubsection \<open>copied from spark_commands.ML\<close>

ML \<open>

\<close> ML \<open>

fun get_vc thy vc_name =

  (case SPARK_VCs.lookup_vc thy false vc_name of

    SOME (ctxt, (_, proved, ctxt', stmt)) =>

      if is_some proved then

        error ("The verification condition " ^

          quote vc_name ^ " has already been proved.")

      else (ctxt @ [ctxt'], stmt)

  | NONE => error ("There is no verification condition " ^

      quote vc_name ^ "."));

\<close> ML \<open>

(*

val prefer_input: ThyC.id * Problem.id -> References.T -> O_Model.T -> References.T * O_Model.T

*)

fun prefer_input (inthy, inpbl : Problem.id) (thy, pbl, met_id) o_model =

  if inthy = thy andalso inpbl = pbl

  then ((thy, pbl, met_id) : References.T, o_model)

  else ((inthy, inpbl, Method.id_empty), [])

\<close> ML \<open>

(*

val prove_vc: ParseC.problem -> Proof.context -> Proof.state

*)

fun prove_vc (*vc_name*)problem lthy =

  let

    val _ = @{print} {a = "//--- Spark_Commands.prove_vc", headline = problem}

    val thy = Proof_Context.theory_of lthy;

    val vc_name = "procedure_g_c_d_4" (*fixed for spark_open \<open>greatest_common_divisor/g_c_d\<close>*)

    val (ctxt, stmt) = get_vc thy vc_name

(*//--------------------------------- new code --------------------------------\\*)

    val {thy_id, pbl_id, (*givens, wheres, ..*)...} = ParseC.read_out_problem problem

    val refs' = Refs_Data.get thy

    val (refs as (_, pbl_id, _), o_model) = prefer_input (thy_id, pbl_id) refs' (OMod_Data.get thy)

    val i_model = I_Model.initPIDE pbl_id

(*

  TODO: present Specification = i_model () + refs via PIDE

*)

(*----------------------------------- new code ----------------------------------*)

    val _ = @{print} {a = "prove_vc", o_model = o_model, refs = refs, i_model = i_model}

(*\\--------------------------------- new code --------------------------------//*)

  in

    Specification.theorem true Thm.theoremK NONE

      (fn thmss => (Local_Theory.background_theory

         (SPARK_VCs.mark_proved vc_name (flat thmss))))

      (Binding.name vc_name, []) [] ctxt stmt false lthy

  end;

\<close> ML \<open>

prove_vc: ParseC.problem -> Proof.context -> Proof.state

\<close> ML \<open>

\<close>

section \<open>setup command_keyword \<close>

ML \<open>

\<close> ML \<open>

val _ =                                                  

  Outer_Syntax.command \<^command_keyword>\<open>Example\<close> "start a Calculation from a Formalise-file"

    (Resources.provide_parse_files "Example" -- Parse.parname

      >> (Toplevel.theory o (load_formalisation ParseC.formalisation)));

\<close> ML \<open>

val _ =

  Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>Problem\<close>

    "start a Specification, either from scratch or from preceding 'Example'"

    (ParseC.problem >> prove_vc);

\<close> ML \<open>

\<close>

subsection \<open>test runs with Example\<close>

subsubsection \<open>with new code\<close>

text \<open>

  Starting the Calculation for the Example requires session Isac with Isac.Biegelinie etc.

  So, do ~~$ ./zcoding-to-test.sh and use Test_Some.thy to evaluate

    Example \<open>/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>

  This now gives no error, but also no <Output>. See child of 3ea616c84845.

\<close>

subsubsection \<open>with original SPARK code\<close>

text \<open>

  The sequence of code below is copied from SPARK/Examples/Gcd/Greatest_Common_Divisor.thy.

  But here the code works only partially (see ERROR at end).

  Thus it is advisable to run tests in Test_Some.thy, where "Example" has "Biegelinie".

  spark_proof_functions is required for proof below..

\<close>

(*//------------------- outcomment before creating session Isac ----------------------------\\* )

(**)

  spark_proof_functions gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"

(**)

spark_open \<open>~~/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>

(*Output..* )

The following verification conditions remain to be proved:

  procedure_g_c_d_4

  procedure_g_c_d_11

( **)

spark_vc procedure_g_c_d_4

proof -

  from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)

  with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1

    by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric])

(** )

proof -

  from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)

  with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1

    by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric])

next

  from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> show ?C2

    by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric] gcd_non_0_int)

qed

( **)oops(**)

(** )sorry( **)

spark_vc procedure_g_c_d_11

  sorry

(** )

spark_end

( *Bad path binding: "$ISABELLE_HOME/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.prv"*)

( *\\------------------- outcomment before creating session Isac ----------------------------//*)

section \<open>adapt spark_vc to Problem using Naproche as model\<close>

subsection \<open>survey on steps of investigation\<close>

text \<open>

  We stopped step 3.4 going down from Outer_Syntax.local_theory_to_proof into proof.

  Now we go the other way: Naproche checks the input via the Isabelle/server

  and outputs highlighting, semantic annotations and errors via PIDE ---

  and we investigate the output.

  Investigation of Naproche showed, that annotations are ONLY sent bY

  Output.report: string list -> unit, where string holds markup.

  For Output.report @ {print} is NOT available, so we trace all respective CALLS.

  However, NO @ {print} available in src/Pure is reached by "spark_vc procedure_g_c_d_4",

  so tracing is done by writeln (which breaks build between Main and Complex_Main

  by writing longer strings, see Pure/General/output.ML).

  Tracing is implemented in (1) Isabelle_Naproche and in (2) isabisac in parallel;

  (1) requires only Pure, thus is built quicker, but does NOT handle proofs within ML

  (2) requires HOL.SPARK, there is full proof handling, but this is complex.

  Tracing the calls of Output.report shows some properties of handling proofs,

  see text in SPARK/Examples/Gcd/Greatest_Common_Divisor.thy.

\<close>

subsection \<open>notes and testbed for Naproche in preliminary spark_vcs\<close>

text \<open>

  tracing "spark_vc procedure_g_c_d_4" see SPARK/Examples/Gcd/Greatest_Common_Divisor.thy

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

subsection \<open>testbed for Problem\<close>

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

end(* SEE "outcomment before creating session Isac" ABOVE !!! OTHERWISE YOU HAVE..

  ERROR: Found the end of the theory, but the last SPARK environment is still open.

  ..is acceptable for testing spark_vc .. proof - ...

*)