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

     Author:     Walther Neuper, JKU Linz

     (c) due to copyright terms

 Outer syntax for Isabelle/Isac. Compare src/Pure/Pure.thy

 *)

 theory Calculation

   imports "~~/src/Tools/isac/MathEngine/MathEngine" "HOL-SPARK.SPARK"

 keywords

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

   "Problem" and (* root-problem + recursively in Solution *)

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

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

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

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

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

 begin

 ML_file parseC.sml

 ML_file "~~/test/HOL/SPARK/test-data.sml" (*..:*)ML \<open>g_c_d_siv_content\<close>

 ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 section \<open>code for spark_open: cp.to cp_spark_vcs.ML, cp_spark_vcs.ML\<close>

 text \<open>

   We minimally change code for Example, until all works.

   The code is separated from Calculation.thy into files cp_spark_vcs.ML and cp_spark_commands.ML, 

   because text\<open>...\<close> and (*...*) for const_name>\<open>...\<close> etc and @ {thms ...} causes errors.

   Thus for Test_Isac (**)ML_file "cp_spark_vcs.ML", ""(*cp_spark_commands.ML*), "HOL-SPARK.SPARK"

   must be outcommented.

 \<close>

 subsection \<open>cp. HOL/SPARK/Tools/spark_vcs.ML\<close>

 ML \<open>

 \<close> ML \<open>

 (*  Title:      src/Tools/isac/BridgeJEdit/cp_spark_vcs.ML

     Author:     Walther Neuper, JKU Linz

     (c) due to copyright terms

 Preliminary code for developing Outer_Syntax.command..Example from spark_open as a model.

 The original signatures from this subsection are:

 *)

 signature SPARK_VCS_PARTIALLY =

 sig

   val err_unfinished: unit -> 'a

   val strip_number: string -> string * string

   val name_ord: string * string -> order

   structure VCtab: TABLE

   structure VCs: THEORY_DATA

   val to_lower: string -> string

   val partition_opt: ('a -> 'b option) -> 'a list -> 'b list * 'a list

   val dest_def: 'a * Fdl_Parser.fdl_rule -> ('a * (string * Fdl_Parser.expr)) option

   val builtin: unit Symtab.table

   val complex_expr: Fdl_Parser.expr -> bool

   val complex_rule: Fdl_Parser.fdl_rule -> bool

   val is_trivial_vc: 'a list * ('b * Fdl_Parser.expr) list -> bool

   val rulenames: ((string * int) * 'a) list -> string

   val is_pfun: Symtab.key -> bool

   val fold_opt: ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b

   val fold_pair: ('a -> 'b -> 'c) -> ('d -> 'c -> 'e) -> 'a * 'd -> 'b -> 'e

   val fold_expr: (string -> 'a -> 'a) -> (string -> 'a -> 'a) -> Fdl_Parser.expr -> 'a -> 'a

   val add_expr_pfuns: 'a Fdl_Parser.tab -> Fdl_Parser.expr -> Symtab.key list -> Symtab.key list

   val lookup_prfx: string -> 'a Symtab.table -> Symtab.key -> 'a option

   val fold_vcs: ('a -> 'b -> 'b) -> ('c * 'd * 'a list * 'a list) VCtab.table -> 'b -> 'b

   val pfuns_of_vcs: string -> 'a Fdl_Parser.tab -> 'b Symtab.table -> ('c * 'd * ('e * Fdl_Parser.expr) list * ('e * Fdl_Parser.expr) list) VCtab.table -> Symtab.key list

   val booleanN: string

   val integerN: string

   val get_type: theory -> string -> Symtab.key -> (typ * (string * string) list) option

   val mk_type': theory -> string -> string -> typ * (string * string) list

   val mk_type: theory -> string -> string -> typ

   val check_no_assoc: theory -> string -> string -> unit

   val define_overloaded: bstring * term -> Proof.context -> thm * local_theory

   val add_enum_type: string -> string -> theory -> theory

   val lcase_eq: string * string -> bool

   val check_enum: string list -> (string * 'a) list -> string option

   val strip_prfx: string -> string * string

   val assoc_ty_err: theory -> typ -> string -> string -> 'a

   val unprefix_pfun: string -> string -> string

   val invert_map: (''a * ''a) list -> (''a * 'b) list -> (''a * 'b) list

   val get_record_info: theory -> typ -> Record.info option

   val add_type_def: string -> string * Fdl_Parser.fdl_type -> ((term * bstring) Symtab.table * Name.context) * theory -> ((term * bstring) Symtab.table * Name.context) * theory

   val add_const: string -> bstring * string -> ((term * string) Symtab.table * Name.context) * theory -> term * (((term * string) Symtab.table * Name.context) * theory)

   val mk_unop: string -> term -> term

   val strip_underscores: string -> string

   val strip_tilde: string -> string

   val mangle_name: string -> string

   val mk_variables: theory -> string -> string list -> string -> (term * string) Symtab.table * Name.context -> term list * ((term * string) Symtab.table * Name.context)

   val find_field: (string * string) list -> string -> (string * 'a) list -> (string * 'a) option

   val find_field': ''a -> (''a list * 'b) list -> 'b option

   val mk_times: term * term -> term

   val term_of_expr: theory -> string -> Fdl_Parser.fdl_type Fdl_Parser.tab -> (('a list * string) option * term) Symtab.table -> (term * string) Symtab.table * Name.context -> Fdl_Parser.expr -> term * string

   val mk_rulename: string * int -> binding

   val add_def:

      string ->

        Fdl_Parser.fdl_type Fdl_Parser.tab ->

          (('a list * string) option * term) Symtab.table ->

            string Fdl_Parser.tab -> (string * int) * (string * Fdl_Parser.expr) -> ((term * string) Symtab.table * Name.context) * theory -> (binding * thm) * (((term * string) Symtab.table * Name.context) * theory)

   val add_expr_idents: Fdl_Parser.expr -> string list -> string list

   val sort_defs:

      string ->

        'a Fdl_Parser.tab ->

          'b Symtab.table -> (string -> bool) -> ((string * int) * (string * Fdl_Parser.expr)) list -> ((string * int) * (string * Fdl_Parser.expr)) list -> ((string * int) * (string * Fdl_Parser.expr)) list

   val add_var: string -> string * string -> ((term * string) Symtab.table * Name.context) * theory -> (string * typ) * (((term * string) Symtab.table * Name.context) * theory)

   val add_init_vars:

      string ->

        ('a * 'b * ('c * Fdl_Parser.expr) list * ('c * Fdl_Parser.expr) list) VCtab.table ->

          ((term * string) Symtab.table * Name.context) * theory -> (string * typ) list * (((term * string) Symtab.table * Name.context) * theory)

   val term_of_rule: theory -> string -> Fdl_Parser.fdl_type Fdl_Parser.tab -> (('a list * string) option * term) Symtab.table -> (term * string) Symtab.table * Name.context -> Fdl_Parser.fdl_rule -> term

   val pfun_type: theory -> string -> string list * string -> typ

   val check_pfun_type: theory -> string -> string -> term -> (string list * string) option -> (string list * string) option -> unit

   val upd_option: 'a option -> 'a option -> 'a option

   val check_pfuns_types: theory -> string -> (string list * string) Fdl_Parser.tab -> ((string list * string) option * term) Symtab.table -> ((string list * string) option * term) Symtab.table

   val pp_vcs: string -> (string * 'a) list -> Pretty.T

   val pp_open_vcs: (string * 'a) list -> Pretty.T

   val partition_vcs: ('a * 'b option * 'c * 'd) VCtab.table -> (VCtab.key * ('a * 'b * 'c * 'd)) list * (VCtab.key * ('a * 'c * 'd)) list

   val print_open_vcs: (Pretty.T -> Pretty.T) -> ('a * 'b option * 'c * 'd) VCtab.table -> ('a * 'b option * 'c * 'd) VCtab.table

 end

 (** theory data **)

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

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

 val name_ord = prod_ord string_ord (option_ord int_ord) o

   apply2 (strip_number ##> Int.fromString);

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

 structure VCs = Theory_Data

 (

   (*/----------------------------- this is stored in thy --------------------------------\*)

   type T = (*Pure/General/table.ML:             'a *)

     {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_Parser.fdl_type Fdl_Parser.tab,

         funs: (string list * string) Fdl_Parser.tab,

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

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

         proving: bool,

         vcs: (string * thm list option *

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

         path: Path.T,

         prefix: string} option}

   (*\----------------------------- this is stored in thy --------------------------------/*)

   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 ()

 )

 (** utilities **)

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

 (** set up verification conditions **)

 fun partition_opt f =

   let

     fun part ys zs [] = (rev ys, rev zs)

       | part ys zs (x :: xs) = (case f x of

             SOME y => part (y :: ys) zs xs

           | NONE => part ys (x :: zs) xs)

   in part [] [] end;

 fun dest_def (id, (Fdl_Parser.Substitution_Rule ([], Fdl_Parser.Ident s, rhs))) = SOME (id, (s, rhs))

   | dest_def _ = NONE;

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

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

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

 fun complex_expr (Fdl_Parser.Number _) = false

   | complex_expr (Fdl_Parser.Ident _) = false

   | complex_expr (Fdl_Parser.Funct (s, es)) =

       not (Symtab.defined builtin s) orelse exists complex_expr es

   | complex_expr (Fdl_Parser.Quantifier (_, _, _, e)) = complex_expr e

   | complex_expr _ = true;

 fun complex_rule (Fdl_Parser.Inference_Rule (es, e)) =

       complex_expr e orelse exists complex_expr es

   | complex_rule (Fdl_Parser.Substitution_Rule (es, e, e')) =

       complex_expr e orelse complex_expr e' orelse

       exists complex_expr es;

 fun is_trivial_vc ([], [(_, Fdl_Parser.Ident "true")]) = true

   | is_trivial_vc _ = false;

 fun rulenames rules = commas

   (map (fn ((s, i), _) => s ^ "(" ^ string_of_int i ^ ")") rules);

 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";

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

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

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

   | fold_expr f g (Fdl_Parser.Ident s) = g s

   | fold_expr f g (Fdl_Parser.Number _) = I

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

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

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

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

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

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

   | fold_expr f g (Fdl_Parser.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;

 fun add_expr_pfuns funs = fold_expr

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

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

 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);

 fun fold_vcs f vcs =

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

 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);

 val booleanN = "boolean";

 val integerN = "integer";

 fun get_type thy prfx ty =

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

   in lookup_prfx prfx type_map ty end;

 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);

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

 fun check_no_assoc thy prfx s = case get_type thy prfx s of

     NONE => ()

   | SOME _ => error ("Cannot associate a type with " ^ s ^

       "\nsince it is no record or enumeration type");

 fun define_overloaded (def_name, eq) lthy =

   let

     val ((c, _), rhs) = eq |> Syntax.check_term lthy |>

       Logic.dest_equals |>> dest_Free;

     val ((_, (_, thm)), lthy') = Local_Theory.define

       ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs)) lthy

     val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');

     val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm

   in (thm', lthy') end;

 (** generate properties of enumeration types **)

 fun add_enum_type tyname tyname' thy =

   let

     val {case_name, ...} = the (BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] tyname');

     val cs = map Const (the (BNF_LFP_Compat.get_constrs thy tyname'));

     val k = length cs;

     val T = Type (tyname', []);

     val p = Const (\<^const_name>\<open>pos\<close>, T --> HOLogic.intT);

     val v = Const (\<^const_name>\<open>val\<close>, HOLogic.intT --> T);

     val card = Const (\<^const_name>\<open>card\<close>,

       HOLogic.mk_setT T --> HOLogic.natT) $ HOLogic.mk_UNIV T;

     fun mk_binrel_def s f = Logic.mk_equals

       (Const (s, T --> T --> HOLogic.boolT),

        Abs ("x", T, Abs ("y", T,

          Const (s, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $

            (f $ Bound 1) $ (f $ Bound 0))));

     val (((def1, def2), def3), lthy) = thy |>

       Class.instantiation ([tyname'], [], \<^sort>\<open>spark_enum\<close>) |>

       define_overloaded ("pos_" ^ tyname ^ "_def", Logic.mk_equals

         (p,

          list_comb (Const (case_name, replicate k HOLogic.intT @

              [T] ---> HOLogic.intT),

            map (HOLogic.mk_number HOLogic.intT) (0 upto k - 1)))) ||>>

       define_overloaded ("less_eq_" ^ tyname ^ "_def",

         mk_binrel_def \<^const_name>\<open>less_eq\<close> p) ||>>

       define_overloaded ("less_" ^ tyname ^ "_def",

         mk_binrel_def \<^const_name>\<open>less\<close> p);

     val UNIV_eq = Goal.prove lthy [] []

       (HOLogic.mk_Trueprop (HOLogic.mk_eq

          (HOLogic.mk_UNIV T, HOLogic.mk_set T cs)))

       (fn {context = ctxt, ...} =>

          resolve_tac ctxt @{thms subset_antisym} 1 THEN

          resolve_tac ctxt @{thms subsetI} 1 THEN

          Old_Datatype_Aux.exh_tac ctxt (K (#exhaust (BNF_LFP_Compat.the_info

            (Proof_Context.theory_of ctxt) [BNF_LFP_Compat.Keep_Nesting] tyname'))) 1 THEN

          ALLGOALS (asm_full_simp_tac ctxt));

     val finite_UNIV = Goal.prove lthy [] []

       (HOLogic.mk_Trueprop (Const (\<^const_name>\<open>finite\<close>,

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

       (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [UNIV_eq]) 1);

     val card_UNIV = Goal.prove lthy [] []

       (HOLogic.mk_Trueprop (HOLogic.mk_eq

          (card, HOLogic.mk_number HOLogic.natT k)))

       (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [UNIV_eq]) 1);

     val range_pos = Goal.prove lthy [] []

       (HOLogic.mk_Trueprop (HOLogic.mk_eq

          (Const (\<^const_name>\<open>image\<close>, (T --> HOLogic.intT) -->

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

               p $ HOLogic.mk_UNIV T,

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

             HOLogic.intT --> HOLogic.mk_setT HOLogic.intT) $

               HOLogic.mk_number HOLogic.intT 0 $

               (\<^term>\<open>int\<close> $ card))))

       (fn {context = ctxt, ...} =>

          simp_tac (ctxt addsimps [card_UNIV]) 1 THEN

          simp_tac (ctxt addsimps [UNIV_eq, def1]) 1 THEN

          resolve_tac ctxt @{thms subset_antisym} 1 THEN

          simp_tac ctxt 1 THEN

          resolve_tac ctxt @{thms subsetI} 1 THEN

          asm_full_simp_tac (ctxt addsimps @{thms interval_expand}

            delsimps @{thms atLeastLessThan_iff}) 1);

     val lthy' =

       Class.prove_instantiation_instance (fn ctxt =>

         Class.intro_classes_tac ctxt [] THEN

         resolve_tac ctxt [finite_UNIV] 1 THEN

         resolve_tac ctxt [range_pos] 1 THEN

         simp_tac (put_simpset HOL_basic_ss ctxt addsimps [def3]) 1 THEN

         simp_tac (put_simpset HOL_basic_ss ctxt addsimps [def2]) 1) lthy;

     val (pos_eqs, val_eqs) = split_list (map_index (fn (i, c) =>

       let

         val n = HOLogic.mk_number HOLogic.intT i;

         val th = Goal.prove lthy' [] []

           (HOLogic.mk_Trueprop (HOLogic.mk_eq (p $ c, n)))

           (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [def1]) 1);

         val th' = Goal.prove lthy' [] []

           (HOLogic.mk_Trueprop (HOLogic.mk_eq (v $ n, c)))

           (fn {context = ctxt, ...} =>

              resolve_tac ctxt [@{thm inj_pos} RS @{thm injD}] 1 THEN

              simp_tac (ctxt addsimps [@{thm pos_val}, range_pos, card_UNIV, th]) 1)

       in (th, th') end) cs);

     val first_el = Goal.prove lthy' [] []

       (HOLogic.mk_Trueprop (HOLogic.mk_eq

          (Const (\<^const_name>\<open>first_el\<close>, T), hd cs)))

       (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [@{thm first_el_def}, hd val_eqs]) 1);

     val last_el = Goal.prove lthy' [] []

       (HOLogic.mk_Trueprop (HOLogic.mk_eq

          (Const (\<^const_name>\<open>last_el\<close>, T), List.last cs)))

       (fn {context = ctxt, ...} =>

         simp_tac (ctxt addsimps [@{thm last_el_def}, List.last val_eqs, card_UNIV]) 1);

   in

     lthy' |>

     Local_Theory.note

       ((Binding.name (tyname ^ "_card"), @{attributes [simp]}), [card_UNIV]) ||>>

     Local_Theory.note

       ((Binding.name (tyname ^ "_pos"), @{attributes [simp]}), pos_eqs) ||>>

     Local_Theory.note

       ((Binding.name (tyname ^ "_val"), @{attributes [simp]}), val_eqs) ||>>

     Local_Theory.note

       ((Binding.name (tyname ^ "_first_el"), @{attributes [simp]}), [first_el]) ||>>

     Local_Theory.note

       ((Binding.name (tyname ^ "_last_el"), @{attributes [simp]}), [last_el]) |> snd |>

     Local_Theory.exit_global

   end;

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

 fun check_enum [] [] = NONE

   | check_enum els [] = SOME ("has no element(s) " ^ commas els)

   | check_enum [] cs = SOME ("has extra element(s) " ^

       commas (map (Long_Name.base_name o fst) cs))

   | check_enum (el :: els) ((cname, _) :: cs) =

       if lcase_eq (el, cname) then check_enum els cs

       else SOME ("either has no element " ^ el ^

         " or it is at the wrong position");

 fun strip_prfx s =

   let

     fun strip ys [] = ("", implode ys)

       | strip ys ("_" :: "_" :: xs) = (implode (rev xs), implode ys)

       | strip ys (x :: xs) = strip (x :: ys) xs

   in strip [] (rev (raw_explode s)) end;

 fun assoc_ty_err thy T s msg =

   error ("Type " ^ Syntax.string_of_typ_global thy T ^

     " associated with SPARK type " ^ s ^ "\n" ^ msg);

 fun check_enum [] [] = NONE

   | check_enum els [] = SOME ("has no element(s) " ^ commas els)

   | check_enum [] cs = SOME ("has extra element(s) " ^

       commas (map (Long_Name.base_name o fst) cs))

   | check_enum (el :: els) ((cname, _) :: cs) =

       if lcase_eq (el, cname) then check_enum els cs

       else SOME ("either has no element " ^ el ^

         " or it is at the wrong position");

 fun unprefix_pfun "" s = s

   | unprefix_pfun prfx s =

       let val (prfx', s') = strip_prfx s

       in if prfx = prfx' then s' else s end;

 fun invert_map [] = I

   | invert_map cmap =

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

 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);

 fun add_type_def prfx (s, Fdl_Parser.Basic_Type ty) (ids, thy) =

       (check_no_assoc thy prfx s;

        (ids,

         Typedecl.abbrev_global (Binding.name s, [], NoSyn)

           (mk_type thy prfx ty) thy |> snd))

   | add_type_def prfx (s, Fdl_Parser.Enum_Type els) ((tab, ctxt), thy) =

       let

         val (thy', tyname) = (case get_type thy prfx s of

             NONE =>

               let

                 val tyb = Binding.name s;

                 val tyname = Sign.full_name thy tyb

               in

                 (thy |>

                  BNF_LFP_Compat.add_datatype [BNF_LFP_Compat.Keep_Nesting]

                    [((tyb, [], NoSyn),

                      map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |>

                  add_enum_type s tyname,

                  tyname)

               end

           | SOME (T as Type (tyname, []), cmap) =>

               (case BNF_LFP_Compat.get_constrs thy tyname of

                  NONE => assoc_ty_err thy T s "is not a datatype"

                | SOME cs =>

                    let val (prfx', _) = strip_prfx s

                    in

                      case check_enum (map (unprefix_pfun prfx') els)

                          (invert_map cmap cs) of

                        NONE => (thy, tyname)

                      | SOME msg => assoc_ty_err thy T s msg

                    end)

           | SOME (T, _) => assoc_ty_err thy T s "is not a datatype");

         val cs = map Const (the (BNF_LFP_Compat.get_constrs thy' tyname));

       in

         ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,

           fold Name.declare els ctxt),

          thy')

       end

   | add_type_def prfx (s, Fdl_Parser.Array_Type (argtys, resty)) (ids, thy) =

       (check_no_assoc thy prfx s;

        (ids,

         Typedecl.abbrev_global (Binding.name s, [], NoSyn)

           (foldr1 HOLogic.mk_prodT (map (mk_type thy prfx) argtys) -->

              mk_type thy prfx resty) thy |> snd))

   | add_type_def prfx (s, Fdl_Parser.Record_Type fldtys) (ids, thy) =

       (ids,

        let val fldTs = maps (fn (flds, ty) =>

          map (rpair (mk_type thy prfx ty)) flds) fldtys

        in case get_type thy prfx s of

            NONE =>

              Record.add_record {overloaded = false} ([], Binding.name s) NONE

                (map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy

          | SOME (rT, cmap) =>

              (case get_record_info thy rT of

                 NONE => assoc_ty_err thy rT s "is not a record type"

               | SOME {fields, ...} =>

                   let val fields' = invert_map cmap fields

                   in

                     (case subtract (lcase_eq o apply2 fst) fldTs fields' of

                        [] => ()

                      | flds => assoc_ty_err thy rT s ("has extra field(s) " ^

                          commas (map (Long_Name.base_name o fst) flds));

                      map (fn (fld, T) =>

                        case AList.lookup lcase_eq fields' fld of

                          NONE => assoc_ty_err thy rT s ("has no field " ^ fld)

                        | SOME U => T = U orelse assoc_ty_err thy rT s

                            ("has field " ^

                             fld ^ " whose type\n" ^

                             Syntax.string_of_typ_global thy U ^

                             "\ndoes not match declared type\n" ^

                             Syntax.string_of_typ_global thy T)) fldTs;

                      thy)

                   end)

        end)

   | add_type_def prfx (s, Fdl_Parser.Pending_Type) (ids, thy) =

       (ids,

        case get_type thy prfx s of

          SOME _ => thy

        | NONE => Typedecl.typedecl_global {final = true} (Binding.name s, [], NoSyn) thy |> snd);

 fun add_type_def prfx (s, Fdl_Parser.Basic_Type ty) (ids, thy) =

       (check_no_assoc thy prfx s;

        (ids,

         Typedecl.abbrev_global (Binding.name s, [], NoSyn)

           (mk_type thy prfx ty) thy |> snd))

   | add_type_def prfx (s, Fdl_Parser.Enum_Type els) ((tab, ctxt), thy) =

       let

         val (thy', tyname) = (case get_type thy prfx s of

             NONE =>

               let

                 val tyb = Binding.name s;

                 val tyname = Sign.full_name thy tyb

               in

                 (thy |>

                  BNF_LFP_Compat.add_datatype [BNF_LFP_Compat.Keep_Nesting]

                    [((tyb, [], NoSyn),

                      map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |>

                  add_enum_type s tyname,

                  tyname)

               end

           | SOME (T as Type (tyname, []), cmap) =>

               (case BNF_LFP_Compat.get_constrs thy tyname of

                  NONE => assoc_ty_err thy T s "is not a datatype"

                | SOME cs =>

                    let val (prfx', _) = strip_prfx s

                    in

                      case check_enum (map (unprefix_pfun prfx') els)

                          (invert_map cmap cs) of

                        NONE => (thy, tyname)

                      | SOME msg => assoc_ty_err thy T s msg

                    end)

           | SOME (T, _) => assoc_ty_err thy T s "is not a datatype");

         val cs = map Const (the (BNF_LFP_Compat.get_constrs thy' tyname));

       in

         ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,

           fold Name.declare els ctxt),

          thy')

       end

   | add_type_def prfx (s, Fdl_Parser.Array_Type (argtys, resty)) (ids, thy) =

       (check_no_assoc thy prfx s;

        (ids,

         Typedecl.abbrev_global (Binding.name s, [], NoSyn)

           (foldr1 HOLogic.mk_prodT (map (mk_type thy prfx) argtys) -->

              mk_type thy prfx resty) thy |> snd))

   | add_type_def prfx (s, Fdl_Parser.Record_Type fldtys) (ids, thy) =

       (ids,

        let val fldTs = maps (fn (flds, ty) =>

          map (rpair (mk_type thy prfx ty)) flds) fldtys

        in case get_type thy prfx s of

            NONE =>

              Record.add_record {overloaded = false} ([], Binding.name s) NONE

                (map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy

          | SOME (rT, cmap) =>

              (case get_record_info thy rT of

                 NONE => assoc_ty_err thy rT s "is not a record type"

               | SOME {fields, ...} =>

                   let val fields' = invert_map cmap fields

                   in

                     (case subtract (lcase_eq o apply2 fst) fldTs fields' of

                        [] => ()

                      | flds => assoc_ty_err thy rT s ("has extra field(s) " ^

                          commas (map (Long_Name.base_name o fst) flds));

                      map (fn (fld, T) =>

                        case AList.lookup lcase_eq fields' fld of

                          NONE => assoc_ty_err thy rT s ("has no field " ^ fld)

                        | SOME U => T = U orelse assoc_ty_err thy rT s

                            ("has field " ^

                             fld ^ " whose type\n" ^

                             Syntax.string_of_typ_global thy U ^

                             "\ndoes not match declared type\n" ^

                             Syntax.string_of_typ_global thy T)) fldTs;

                      thy)

                   end)

        end)

   | add_type_def prfx (s, Fdl_Parser.Pending_Type) (ids, thy) =

       (ids,

        case get_type thy prfx s of

          SOME _ => thy

        | NONE => Typedecl.typedecl_global {final = true} (Binding.name s, [], NoSyn) thy |> snd);

 fun add_const prfx (s, ty) ((tab, ctxt), thy) =

   let

     val T = mk_type thy prfx ty;

     val b = Binding.name s;

     val c = Const (Sign.full_name thy b, T)

   in

     (c,

      ((Symtab.update (s, (c, ty)) tab, Name.declare s ctxt),

       Sign.add_consts [(b, T, NoSyn)] thy))

   end;

 fun mk_unop s t =

   let val T = fastype_of t

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

 fun strip_underscores s =

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

 fun strip_tilde s =

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

 val mangle_name = strip_underscores #> strip_tilde;

 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;

 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')));

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

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

 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;

 fun term_of_expr thy prfx types pfuns =

   let

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

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

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

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

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

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

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

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

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

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

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

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

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

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

       | tm_of vs (Fdl_Parser.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 (Fdl_Parser.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 (Fdl_Parser.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 (Fdl_Parser.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 (Fdl_Parser.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 (Fdl_Parser.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 (Fdl_Parser.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 (Fdl_Parser.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 (Fdl_Parser.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 (Fdl_Parser.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 (Fdl_Parser.Funct ("-", [e])) =

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

       | tm_of vs (Fdl_Parser.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, _) (Fdl_Parser.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 _ (Fdl_Parser.Number i) = (HOLogic.mk_number HOLogic.intT i, integerN)

       | tm_of vs (Fdl_Parser.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 (Fdl_Parser.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, Fdl_Parser.lookup types rcdty) of

                      (SOME {fields, ...}, SOME (Fdl_Parser.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 (Fdl_Parser.Element (e, es)) =

           let val (t, ty) = tm_of vs e

           in case Fdl_Parser.lookup types ty of

               SOME (Fdl_Parser.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 (Fdl_Parser.Update (e, es, e')) =

           let val (t, ty) = tm_of vs e

           in case Fdl_Parser.lookup types ty of

               SOME (Fdl_Parser.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 (Fdl_Parser.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 (Fdl_Parser.Array (s, default, assocs)) =

           (case Fdl_Parser.lookup types s of

              SOME (Fdl_Parser.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;

 fun mk_rulename (s, i) = Binding.name (s ^ string_of_int i);

 fun add_def prfx types pfuns consts (id, (s, e)) (ids as (tab, ctxt), thy) =

   (case Fdl_Parser.lookup consts s of

     SOME ty =>

       let

         val (t, ty') = term_of_expr thy prfx types pfuns ids e;

         val T = mk_type thy prfx ty;

         val T' = mk_type thy prfx ty';

         val _ = T = T' orelse

           error ("Declared type " ^ ty ^ " of " ^ s ^

             "\ndoes not match type " ^ ty' ^ " in definition");

         val id' = mk_rulename id;

         val ((t', (_, th)), lthy') = Named_Target.theory_init thy

           |> Specification.definition NONE [] []

             ((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq (Free (s, T), t)));

         val phi =

           Proof_Context.export_morphism lthy'

             (Proof_Context.init_global (Proof_Context.theory_of lthy'));

       in

         ((id', Morphism.thm phi th),

           ((Symtab.update (s, (Morphism.term phi t', ty)) tab, Name.declare s ctxt),

             Local_Theory.exit_global lthy'))

        end

   | NONE => error ("Undeclared constant " ^ s));

 val add_expr_idents = fold_expr (K I) (insert (op =));

 (* sort definitions according to their dependency *)

 fun sort_defs _ _ _ _ [] sdefs = rev sdefs

   | sort_defs prfx funs pfuns consts defs sdefs =

       (case find_first (fn (_, (_, e)) =>

          forall (is_some o lookup_prfx prfx pfuns)

            (add_expr_pfuns funs e []) andalso

          forall (fn id =>

            member (fn (s, (_, (s', _))) => s = s') sdefs id orelse

            consts id)

              (add_expr_idents e [])) defs of

          SOME d => sort_defs prfx funs pfuns consts

            (remove (op =) d defs) (d :: sdefs)

        | NONE => error ("Bad definitions: " ^ rulenames defs));

 fun add_var prfx (s, ty) (ids, thy) =

   let val ([Free p], ids') = mk_variables thy prfx [s] ty ids

   in (p, (ids', thy)) end;

 fun add_init_vars prfx vcs (ids_thy as ((tab, _), _)) =

   fold_map (add_var prfx)

     (map_filter

        (fn s => case try (unsuffix "~") s of

           SOME s' => (case Symtab.lookup tab s' of

             SOME (_, ty) => SOME (s, ty)

           | NONE => error ("Undeclared identifier " ^ s'))

         | NONE => NONE)

        (fold_vcs (add_expr_idents o snd) vcs []))

     ids_thy;

 fun term_of_rule thy prfx types pfuns ids rule =

   let val tm_of = fst o term_of_expr thy prfx types pfuns ids

   in case rule of

       Fdl_Parser.Inference_Rule (es, e) => Logic.list_implies

         (map (HOLogic.mk_Trueprop o tm_of) es, HOLogic.mk_Trueprop (tm_of e))

     | Fdl_Parser.Substitution_Rule (es, e, e') => Logic.list_implies

         (map (HOLogic.mk_Trueprop o tm_of) es,

          HOLogic.mk_Trueprop (HOLogic.mk_eq (tm_of e, tm_of e')))

   end;

 fun pfun_type thy prfx (argtys, resty) =

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

 fun check_pfun_type thy prfx s t optty1 optty2 =

   let

     val T = fastype_of t;

     fun check ty =

       let val U = pfun_type thy prfx ty

       in

         T = U orelse

         error ("Type\n" ^

           Syntax.string_of_typ_global thy T ^

           "\nof function " ^

           Syntax.string_of_term_global thy t ^

           " associated with proof function " ^ s ^

           "\ndoes not match declared type\n" ^

           Syntax.string_of_typ_global thy U)

       end

   in (Option.map check optty1; Option.map check optty2; ()) end;

 fun upd_option x y = if is_some x then x else y;

 fun check_pfuns_types thy prfx funs =

   Symtab.map (fn s => fn (optty, t) =>

    let val optty' = Fdl_Parser.lookup funs (unprefix_pfun prfx s)

    in

      (check_pfun_type thy prfx s t optty optty';

       (NONE |> upd_option optty |> upd_option optty', t))

    end);

 fun pp_vcs msg vcs = Pretty.big_list msg (map (Pretty.str o fst) vcs);

 fun pp_open_vcs [] = Pretty.str "All verification conditions have been proved."

   | pp_open_vcs vcs = pp_vcs

       "The following verification conditions remain to be proved:" vcs;

 fun partition_vcs vcs = VCtab.fold_rev

   (fn (name, (trace, SOME thms, ps, cs)) =>

         apfst (cons (name, (trace, thms, ps, cs)))

     | (name, (trace, NONE, ps, cs)) =>

         apsnd (cons (name, (trace, ps, cs))))

   vcs ([], []);

 fun print_open_vcs f vcs =

   (Pretty.writeln (f (pp_open_vcs (snd (partition_vcs vcs)))); vcs);

 (*   set_env: Element.context_i list -> (binding * thm) list -> fdl_type tab ->

        (string list * string) tab -> term * string) Symtab.table * Name.context ->

          (string * thm list option * (string * expr) list * (string * expr) list) VCtab.table ->

            Path.T -> string -> theory -> theory 

   Context --vvvv is made Theory_Data by -------------------vvvvvvv, see.def. above *)

 fun set_env ctxt defs types funs ids vcs path prefix thy = VCs.map (fn

     {pfuns, type_map, env = NONE} =>

       {pfuns = pfuns,

        type_map = type_map,

        env = SOME

          {ctxt = ctxt, defs = defs, types = types, funs = funs,

           pfuns = check_pfuns_types thy prefix funs pfuns,

           ids = ids, proving = false, vcs = print_open_vcs I vcs, path = path,

           prefix = prefix}}

   | _ => err_unfinished ()) thy;

 VCs.map: (VCs.T -> VCs.T) -> theory -> theory;

 (* Pure/context.ML

 signature THEORY_DATA =

 sig

   type T                                  (*..VCs.T*)

   val get: theory -> T

   val put: T -> theory -> theory

   val map: (T -> T) -> theory -> theory   (*..(VCs.T -> VCs.T)*)

 end;

 *)

 \<close> ML \<open>

 structure Refs_Data = Theory_Data

 (

   type T = References.T

   val empty : T = References.empty

   val extend = I

   fun merge (_, refs) = refs

 );

 (*

 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*)

 \<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>

 \<close> ML \<open>

 fun set_vcs _(*{types, vars, consts, funs} : Fdl_Parser.decls*)

       _(*rules, _*) _(*(_, ident), vcs*) header path opt_prfx thy =

   let

   (*/----- keep running from spark_open \<open>greatest_common_divisor/g_c_d\<close> -----\*)

     val ({types, vars, consts, funs} : Fdl_Parser.decls) = 

       snd (Fdl_Parser.parse_declarations Position.start g_c_d_fdl_content)

     val (rules, _) = Fdl_Parser.parse_rules Position.start g_c_d_rls_content

     val ((_, ident), vcs) =

       snd (Fdl_Parser.parse_vcs Fdl_Lexer.siv_header Position.start g_c_d_siv_content)

   (*------ new argument:  ParseC.vcs = ParseC.formalise ----------------------*)

     val formalise = case header 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"

   (*\----- keep running from spark_open \<open>greatest_common_divisor/g_c_d\<close> -----/*)

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

   (*     ^^^^^^^ goes to PIDE as "Problem hdlPIDE"                            *)

     val prfx' =

       if opt_prfx = "" then

         space_implode "__" (Long_Name.explode (Long_Name.qualifier ident))

       else opt_prfx;

     val prfx = to_lower prfx';

     val {pfuns, ...} = VCs.get thy;                                                       (*..thy*)

     val (defs, rules') = partition_opt dest_def rules;

     val consts' =

       subtract (fn ((_, (s, _)), (s', _)) => s = s') defs (Fdl_Parser.items consts);

     (* ignore all complex rules in rls files *)

     val (rules'', other_rules) =

       List.partition (complex_rule o snd) rules';

     val _ = if null rules'' then ()

       else warning ("Ignoring rules: " ^ rulenames rules'');

     val vcs' = VCtab.make (maps (fn (tr, vcs) =>

       map (fn (s, (ps, cs)) => (s, (tr, NONE, ps, cs)))

         (filter_out (is_trivial_vc o snd) vcs)) vcs);

     val _ = (case filter_out (is_some o Fdl_Parser.lookup funs)

         (pfuns_of_vcs prfx funs pfuns vcs') of

         [] => ()

       | fs => error ("Undeclared proof function(s) " ^ commas fs));

     val (((defs', vars''), ivars)(*->*),(*<-*) (ids, thy')) =                            (*..thy'*)

       ((Symtab.empty |>

         Symtab.update ("false", (\<^term>\<open>False\<close>, booleanN)) |>

         Symtab.update ("true", (\<^term>\<open>True\<close>, booleanN)),     (*..(defs', vars'')*)

         Name.context)(*->*),(*<-*)                           (*..ivars*)

        thy |> Sign.add_path                                                               (*..thy*)

          ((if prfx' = "" then "" else prfx' ^ "__") ^ Long_Name.base_name ident)) |>

       fold (add_type_def prfx) (Fdl_Parser.items types) |>

       fold (snd oo add_const prfx) consts' |> (fn ids_thy as ((tab, _), _) =>

         ids_thy |>

         fold_map (add_def prfx types pfuns consts)

           (sort_defs prfx funs pfuns (Symtab.defined tab) defs []) ||>>

         fold_map (add_var prfx) (Fdl_Parser.items vars) ||>>

         add_init_vars prfx vcs');                            (*..(ids,                      thy')*)

     val ctxt =

       [Element.Fixes (map (fn (s, T) =>

          (Binding.name s, SOME T, NoSyn)) (vars'' @ ivars)),

        Element.Assumes (map (fn (id, rl) =>

          ((mk_rulename id, []),

           [(term_of_rule thy' prfx types pfuns ids rl, [])]))                            (*..thy'*)

            other_rules),

        Element.Notes ("", [((Binding.name "defns", []), map (rpair [] o single o snd) defs')])]

   in

     set_env ctxt defs' types funs ids vcs' path prfx thy'

       |> Refs_Data.put refs

       |> OMod_Data.put o_model

       |> Ctxt_Data.put var_type_ctxt

   end;

 \<close> ML \<open>

 \<close>

 subsection \<open>cp. HOL/SPARK/Tools/fdl_lexer.ML\<close>

 ML \<open>

 \<close> ML \<open>

 type chars = (string * Position.T) list;

 val e_chars = []: (string * Position.T) list;               

 type banner = string * string * string;               val e_banner = ("b1", "b2", "b3")

 type date = string * string * string;                 val e_date = ("d1", "d2", "d3")

 type time = string * string * string * string option; val e_time = ("t1", "t2", "t3", SOME "t4")

 fun siv_header (_: chars) = 

   ((e_banner, (e_date, e_time), (e_date, e_time), ("", "")), e_chars);

 \<close> ML \<open>

 \<close> 

 subsection \<open>cp. HOL/SPARK/Tools/spark_commands.ML\<close>

 ML \<open>

 \<close> ML \<open>

 (*  Title:      src/Tools/isac/BridgeJEdit/cp_spark_commands.ML

     Author:     Walther Neuper, JKU Linz

     (c) due to copyright terms

 Preliminary code for developing Outer_Syntax.command..Example from spark_open as a model.

 *)

 fun spark_open header (files, prfx) thy =

 (*Fdl_Lexer.siv_header*)

   let

 (** )val _ = @{print} {a = "//--- ###C spark_open", files = files, prfx = prfx};( **)

     val xxx as ([{src_path, lines = vc_lines, pos = vc_pos, ...}: Token.file (*,.siv*)

 (** )  {lines = fdl_lines, pos = fdl_pos, ...},                              ( *.fld*)

 (** )  {lines = rls_lines, pos = rls_pos, ...}                               ( *.rls*)

       ], thy') = 

     ((** @{print} {a = "###C spark_open: before call <files thy>, files = siv_header !"};( **)

       files thy);

 (*                                                                                    ^^^^^ arg!*)

     val path = fst (Path.split_ext src_path);

   in

 (** )@{print} {a = "###C spark_open: result from siv_header, without thy'", fst_xxx = fst xxx};( **)

 (** )@{print} {a = "###C spark_open: 1 arg for SPARK_VCs.set_vcs",

 (** ) arg1 = (snd (Fdl_Parser.parse_declarations fdl_pos (cat_lines fdl_lines))),

       arg2 = (Fdl_Parser.parse_rules rls_pos (cat_lines rls_lines)),            ( **)

 (** ) arg3 = (snd (Fdl_Parser.parse_vcs header vc_pos (cat_lines vc_lines))), ( **)

 (*                                                     !^^^^^^^!*)

       z = "\\--- ###C spark_open"};( **)

     (*SPARK_VCs.*)set_vcs

 (*ADDED*) (**)

 (** )  (snd (Fdl_Parser.parse_declarations fdl_pos (cat_lines fdl_lines)))( **)Fdl_Parser.empty_decls(**)

 (** )  (Fdl_Parser.parse_rules rls_pos (cat_lines rls_lines))             ( **)Fdl_Parser.empty_rules(**)

 (** )  (snd (Fdl_Parser.parse_vcs header vc_pos (cat_lines vc_lines)))    ( **)Fdl_Parser.empty_vcs(**)

 (**)   (ParseC.read_out_formalise (fst (header     (fst (ParseC.scan' vc_pos (cat_lines vc_lines))))))(**)

       path prfx thy'

   end;

 \<close> ML \<open>

 \<close> ML \<open> (* compose NEW argument "header"                               ^v^v^v^v^v^v^v^v^v^v^v^v^v^v*)

        (ParseC.read_out_formalise (fst (ParseC.vcs (fst (ParseC.scan' Position.start formalise_str)))))

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open> (* generate the arguments directly for: spark_open \<open>greatest_common_divisor/g_c_d\<close>*)

 (*     (snd (Fdl_Parser.parse_declarations fdl_pos (cat_lines fdl_lines))) *)

         snd (Fdl_Parser.parse_declarations Position.start g_c_d_fdl_content)

 \<close> ML \<open>

 (*     (Fdl_Parser.parse_rules rls_pos (cat_lines rls_lines)) *)

         Fdl_Parser.parse_rules Position.start g_c_d_rls_content

 \<close> ML \<open>

 val (("procedure", "Greatest_Common_Divisor.G_C_D"), vcs) =

 (*     (snd (Fdl_Parser.parse_vcs header vc_pos (cat_lines vc_lines))) *)

         snd (Fdl_Parser.parse_vcs Fdl_Lexer.siv_header Position.start g_c_d_siv_content);

 length vcs = 11;

 vcs;

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 section \<open>setup command_keyword \<close>

 subsection \<open>hide for development, use for Test_Isac\<close>

 text \<open>

 (*HIDE for development, activate for Test_Isac*)

 type chars = (string * Position.T) list;

 val e_chars = []: (string * Position.T) list;

 fun spark_open (_: ((*Fdl_Lexer.*)chars -> 'a * (*Fdl_Lexer.*)chars)) 

     (_: ('b -> Token.file list * theory) * string) (_: 'b) = @ {theory}

 type banner = string * string * string;               val e_banner = ("b1", "b2", "b3")

 type date = string * string * string;                 val e_date = ("d1", "d2", "d3")

 type time = string * string * string * string option; val e_time = ("t1", "t2", "t3", SOME "t4")

 fun siv_header (_: chars) = 

   ((e_banner, (e_date, e_time), (e_date, e_time), ("", "")), e_chars);

 (*HIDE for development, activate for Test_Isac*)

 \<close> ML \<open>

 \<close> 

 subsection \<open>def.for Build_Isac; for Test_Isac outcomment SPARK_Commands, Fdl_Lexer below\<close>

 ML \<open>

 \<close> ML \<open>

 val siv_header = ParseC.vcs; (*---------------------------------------------vvvvvvvvv*)

 \<close> ML \<open>

 val _ =                                                  

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

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

       >> (Toplevel.theory o ((*SPARK_Commands.*)spark_open (*Fdl_Lexer.( **)siv_header)));

 (*--------------------------------------------------------------------------^^^^^^^^^^*)

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

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

 (*======= vv-- Example =================================================================*)

 (** Test_Isac finds exp_Statics_Biegel_Timischl_7-70.siv ?!?* )

 Example \<open>/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>(*.str*)

 ( ***Output:

 *)

 (*====== ^^-- Example, spark_open--vv ==================================================*)

 (* DO THAT IN ..................... HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy)

 spark_open \<open>/usr/local/isabisac/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>

 ( ***Output:

 *)

 (*==================== spark_open--^^ ==================================================*)

 section \<open>Adapt SPARK's parser -> parse Formalise.T\<close>

 text \<open>

   Possible models, where a file is read and parsed:

   * for *.bib see usage of Resources.provide_parse_files     .. parsed by LaTeX

   * Outer_Syntax.command \ <command_keyword>\<open>external_file\<close>  .. ?!?

   * Outer_Syntax.command \<command_keyword>\<open>spark_open\<close>

   We pursue the latter.

   From c.f.2b9b4b38ab96 we have found Fdl_Lexer.scan as the very model

   for scanning/parsing Formalise.T.

 \<close>

 subsection \<open>testbed separates Fdl_Lexer.scan + Fdl_Parser from SPARK code\<close>

 declare [[ML_print_depth = 7]] (* 3 7 10 20 999999999 *)

 ML \<open>

 open Fdl_Lexer

 (** )open Fdl_Parser( *conflict with some of Fdl_Lexer.* *)

 (*

   step 1: go top down and keep respective results according to trace from

           spark_open \<open>greatest_common_divisor/g_c_d\<close> SPARK/../Greatest_Common_Divisor.thy.

           (in the example this is simple: just watch the bottom of Output

            The following verification conditions remain to be proved:

              procedure_g_c_d_4

              procedure_g_c_d_11)

         ! remove @~{print} from calling functions (higher level) 

           once you go down to the called functions (lower level)

           in order to reduce noise and to focus the code under actual consideration.

   step 2: at bottom gather the most elementary funs for transformation

            of g_c_d_siv_content to args of Fdl_Lexer.scan

   step 3: parse the tokens created by  Fdl_Lexer.scan

 *)

 \<close> ML \<open>

 \<close> ML \<open> (** high start level: parsing to header + VCs **)

 val parsed = Fdl_Parser.parse_vcs Fdl_Lexer.siv_header Position.start g_c_d_siv_content;

 \<close> ML \<open> (*               ^^^^^^^^^ <<<<<------------------------------------------------------*)

 val ((banner, (date, time), (date2, time2), (string, string2)), ((str, str2), vcss)) = parsed;

 if banner = ("Semantic Analysis of SPARK Text",

     "Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039",

     "Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.")  andalso

   (date, time) = (("29", "NOV", "2010"), ("14", "30", "10", NONE)) andalso

   (date2, time2) = (("29", "NOV", "2010"), ("14", "30", "11", NONE)) andalso

   (string, string2) =

     ("SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039",

     "Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.") andalso

   (str, str2) = ("procedure", "Greatest_Common_Divisor.G_C_D")

   then () else error "Fdl_Parser.parse_vcs header CHANGED";

 if length vcss = 11 (* verification conditions (VCs) from g_c_d_siv_content *) then

   case vcss of

     ("path(s) from start to run-time check associated with statement of line 8", 

       [("procedure_g_c_d_1", ([], [("1", Fdl_Parser.Ident "true")]))]) ::

     ("path(s) from start to run-time check associated with statement of line 8", 

       [("procedure_g_c_d_2", ([], [("1", Fdl_Parser.Ident "true")]))]) ::

     ("path(s) from start to assertion of line 10", 

       [("procedure_g_c_d_3", ([], [("1", Fdl_Parser.Ident "true")]))]) :: 

     ("path(s) from assertion of line 10 to assertion of line 10",

       [("procedure_g_c_d_4",

         (("1", Fdl_Parser.Funct (">=", [Fdl_Parser.Ident "c", Fdl_Parser.Number 0])) :: 

          ("2", Fdl_Parser.Funct (">", [Fdl_Parser.Ident "d", Fdl_Parser.Number 0])) :: _,

          _))]) :: _ => ()

   | _ => error "Fdl_Parser.parse_vcs vcss CHANGED 1"

 else error "Fdl_Parser.parse_vcs vcss CHANGED 2";

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open> (* lower level 1: tokenize string to header + VCs *)

 val level1_header_toks =

 (* tokenize to header + VCs is NON-standard ..

             vvvvvvvv--- parses vvvvvvvvvv     +     vvvvvvvvv, but leaves vcsss as Token list*)

   Fdl_Lexer.tokenize Fdl_Lexer.siv_header Fdl_Lexer.c_comment Position.start g_c_d_siv_content;

 \<close> ML \<open> (*   ^^^^^^^^ <<<<<-------------------------------------------------------------------*)

 val ((banner, (date, time), (date2, time2), (string, string2)), toks ) = level1_header_toks;

 if banner = ("Semantic Analysis of SPARK Text",

     "Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039",

     "Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.")  andalso

   (date, time) = (("29", "NOV", "2010"), ("14", "30", "10", NONE)) andalso

   (date2, time2) = (("29", "NOV", "2010"), ("14", "30", "11", NONE)) andalso

   (string, string2) =

     ("SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039",

     "Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.")

   then () else error "Fdl_Lexer.tokenize header CHANGED";

 if length toks = 319 (* tokens for str :: str :: verification conditions from g_c_d_siv_content *) then

   case toks of

     Token (Keyword, "procedure", _(*Position.T*)) :: 

     Token (Long_Ident, "Greatest_Common_Divisor.G_C_D", _(*Position.T*)) :: _  => ()

   | _ => error "Fdl_Lexer.tokenize tokens CHANGED 1"

 else error "Fdl_Lexer.tokenize header CHANGED 2";

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open> (* lower level 2: tokenize the string *)

 val chars = Fdl_Lexer.explode_pos g_c_d_siv_content(*_content*) Position.start;

 if length chars = 2886 then () else error "Fdl_Lexer.explode_pos g_c_d_siv_content CHANGED";

 val level2_header_toks = (Scan.finite char_stopper (*..from tokenize..*)

   (Scan.error (Fdl_Lexer.scan Fdl_Lexer.siv_header Fdl_Lexer.c_comment)) chars);

 (* ---------------------------------------------------------------------------\

                Fdl_Lexer.scan Fdl_Lexer.siv_header Fdl_Lexer.c_comment chars

 exception MORE () raised (line 176 of "General/scan.ML") ---------------------/ *)

 case level2_header_toks of

   (((("Semantic Analysis of SPARK Text", 

        "Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039", 

        "Copyright (C) 2010 Altran Praxis Limited, Bath, U.K."), 

        (("29", "NOV", "2010"), ("14", "30", "10", NONE)),

        (("29", "NOV", "2010"), ("14", "30", "11", NONE)), 

        ("SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039", 

          "Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.")),

      Token (Keyword, "procedure", _) :: Token (Long_Ident, "Greatest_Common_Divisor.G_C_D", _) ::

      Token (Traceability, 

        "path(s) from start to run-time check associated with statement of line 8", _) ::

      _ ),

    []) => ()

 | _ => error "Fdl_Lexer.scan level2 CHANGED";

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open> (* lower level 2: parse the tokens *)

 val ((_, tokens), _) = level2_header_toks;

 \<close> ML \<open>

 Fdl_Parser.vcs: T list ->

   ((string * string) * (string * (string * ((string * Fdl_Parser.expr) list * (string * Fdl_Parser.expr) list)) list) list)

   * T list;

 (filter Fdl_Lexer.is_proper): T list -> T list;

 \<close> ML \<open>

 val (parsed', _) =

   Scan.finite Fdl_Lexer.stopper (Scan.error (Fdl_Parser.!!! Fdl_Parser.vcs))

     (filter Fdl_Lexer.is_proper (*|*)tokens(*|*))

 (* ---------------------------------------------------------------------------\

                  Fdl_Parser.vcs (*|*)tokens(*|*)

 exception ABORT fn raised (line 109 of "General/scan.ML") --------------------/ *)

 \<close> ML \<open>

 if parsed' = ((str, str2), vcss) then () else error "Fdl_Parser.parse_vcs level 2 CHANGED 2";

 \<close> ML \<open>

 \<close>

 subsection \<open>test data for Isac's Formalise.T parser\<close>

 ML \<open>

 \<close> ML \<open>

 val form_single_str = (

   "(\n" ^

 (* Formalise.model: *)

   "  [\"Traegerlaenge L\", \"Streckenlast q_0\", \"Biegelinie y\",\n" ^

 	"    \"Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]\",\n" ^

 	"    \"FunktionsVariable x\", \"GleichungsVariablen [c, c_2, c_3, c_4]\",\n" ^

   "    \"AbleitungBiegelinie dy\"],\n" ^

 (* Formalise.spec: *)

   "  (\"Biegelinie\", [\"Biegelinien\"], [\"IntegrierenUndKonstanteBestimmen2\"])\n" ^

   ")")

 \<close> ML \<open>

 val formalise_str = "[" ^ form_single_str ^ "]"; (*..we assume one element ONLY *)

 \<close> ML \<open>

 val form_spec_str =

 (* Formalise.spec: *)

   "  (\"Biegelinie\", [\"Biegelinien\"], [\"IntegrierenUndKonstanteBestimmen2\"])";

 val form_spec_str' =

   "(\"Biegelinie\",[\"Biegelinien\"],[\"IntegrierenUndKonstanteBestimmen2\"])";

 \<close> ML \<open>

 val form_model_str = (

 (* Formalise.model: *)

   "  [\"Traegerlaenge L\", \"Streckenlast q_0\", \"Biegelinie y\",\n" ^

 	"    \"Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]\",\n" ^

 	"    \"FunktionsVariable x\", \"GleichungsVariablen [c, c_2, c_3, c_4]\",\n" ^

   "    \"AbleitungBiegelinie dy\"],\n")

 val form_model_str' = ( (* NO whitespace *)

   "[\"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\"]")

 \<close> ML \<open>

 val form_model_str'' = ( (* NO whitespace, NO [ ] *)

   "\"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\"]")

 \<close> ML \<open>

 val form_model_str''' = ( (* NO whitespace, NO [ ], NO "," *)

   "[\"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\"]")

 \<close> ML \<open>

 \<close>

 subsection \<open>Adapt SPARK's code for parsing Formalise.T\<close>

 text \<open>

 \<close> ML \<open> (* equip the string -----vvvvvvvvvvvvvvv with Positions..*)

 val chars = Fdl_Lexer.explode_pos form_single_str Position.start: Fdl_Lexer.chars;

 if length chars = 306 then () else error "Fdl_Lexer.explode_pos g_c_d_siv CHANGED";

 \<close> 

 subsubsection \<open>identify various code that might serve as model\<close>

 ML \<open>

 \<close> ML \<open> (* gen_comment adapted for a single string (*1*) on simplified form_model_str'' *)

 val tokenize_string = $$$ "\"" |-- !!! "unclosed string" (*2*)

   (Scan.repeat (Scan.unless ($$$ "\"") any) --| $$$ "\"") >> make_token Comment(*!!!*);

 tokenize_string: chars -> T * chars

 \<close> ML \<open>

 val chars = Fdl_Lexer.explode_pos form_model_str'' Position.start: Fdl_Lexer.chars;

 tokenize_string chars; (*3*) (* = WE ONLY GET THE FIRST ELEMENT tokenized, WHY?..

    (Token (Comment, "Traegerlaenge L", {line=1, offset=2}),

     [(",", {line=1, offset=18}), ("\"", {line=1, offset=19}), ("S", {line=1, offset=20}), ("t", {line=1, offset=21}), ("r", {line=1, offset=22}), ("e", {line=1, offset=23}), ("c", {line=1, offset=24}),

      ("k", {line=1, offset=25}), ("...", {line=1, offset=26}), ...])*)

 \<close> ML \<open>

 \<close> ML \<open> (* gen_comment adapted for several strings (*4*) on simplified form_model_str''' *)

 val tokenize_strings =

   Fdl_Lexer.keyword "[" |-- !!! "unclosed list"

     (Scan.repeat (Scan.unless (Fdl_Lexer.keyword "]") tokenize_string) --|

   Fdl_Lexer.keyword "]");

 tokenize_strings: chars -> T(*Token of kind * string * Position.T*) list * chars

 \<close> ML \<open>

 val chars = Fdl_Lexer.explode_pos form_model_str''' Position.start;

 tokenize_strings chars;(* =       THIS LOOKS PROMISING..

    ([Token (Comment, "Traegerlaenge L", {line=1, offset=3}), Token (Comment, "Streckenlast q_0", {line=1, offset=20}), Token (Comment, "Biegelinie y", {line=1, offset=38}),

      Token (Comment, "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", {line=1, offset=52}), Token (Comment, "FunktionsVariable x", {line=1, offset=118}),

      Token (Comment, "GleichungsVariablen [c, c_2, c_3, c_4]", {line=1, offset=139}), Token (Comment, "AbleitungBiegelinie dy", {line=1, offset=179})],

     [])*)

 \<close> ML \<open>

 \<close> ML \<open> (*.. BUT THAT DOESN'T WORK FOR MORE REALISTIC DATA..*)

 val chars = Fdl_Lexer.explode_pos form_model_str' Position.start;

 (* (*6*)

 tokenize_strings chars;

 exception ABORT fn raised (line 109 of "General/scan.ML")*)

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open> (*A NEW IDEA: postpone list-structure to Fld_Parser, now just make reasonable tokens *)

 val chars = Fdl_Lexer.explode_pos "\"GleichungsVariablen [c, c_2, c_3, c_4]\"" Position.start;

 tokenize_string chars; (* = (Token (Comment, "GleichungsVariablen [c, c_2, c_3, c_4]"*)

 \<close> ML \<open>

 \<close> ML \<open> (*..what about delimiters of lists?..*)

 \<close> ML \<open> (*let's go bottom up..*)

 val xxx =

   whitespace --

     keyword "(" --

       keyword "[";

 xxx: chars -> ((chars * chars) * chars) * chars;

 \<close> ML \<open>

 val xxx =

                                       whitespace --

     keyword "(" --

       keyword "[" -- tokenize_string;

 xxx: chars -> (((chars * chars) * chars) * T) * chars

 \<close> ML \<open> (*                                 ^^^ list ?!*)

 \<close> ML \<open>

 val xxx =

                                       whitespace --

     keyword "(" --                    whitespace --

       keyword "[" --                  whitespace --

         tokenize_string;

 xxx: chars -> (((((chars * chars) * chars) * chars) * chars) * T) * chars;

 \<close> ML \<open> (* how can we drop  ^^^^^    ^^^^^    ^^ and make here ^^^ a list ?!

           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)

 val chars = Fdl_Lexer.explode_pos "(\n  [\"Traegerlaenge L\""  Position.start;

 \<close> ML \<open>

 xxx chars; (* =  WE GET AN UNPLEASANT MIXTURE OF Fld_Lexer.T  AND Fld_Lexer.char ..

    (((((([], [("(", {line=1, offset=1})]), [("\n", {line=1, offset=2}), (" ", {line=2, offset=3}), (" ", {line=2, offset=4})]), [("[", {line=2, offset=5})]), []),

      Token (Comment, "Traegerlaenge L", {line=2, offset=7})),

     [])*)

 \<close> ML \<open>

 tokenize_string: chars -> T * chars;

 whitespace: chars -> chars * chars;

 tokenize: (chars -> 'a * chars) -> (chars -> T * chars) -> Position.T -> string -> 'a * T list;

 Scan.repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a

 (*                  ^^                ^^^^^^^                                           ^^^^^^*)

 \<close> ML \<open>

 \<close>  

 subsubsection \<open>have a closer look at SPARKs main tokenizer\<close>

 ML \<open>

 \<close> ML \<open> Fdl_Lexer.scan; (*7*) (*.. <ctrl><mouse> leads to the source *)

 \<close> ML \<open>

 val aaa = (*remove code specific for SPARK..*)

   Scan.repeat (Scan.unless (Scan.one is_char_eof)

     ( (*comment *)

         (keyword "For" -- whitespace1) |--

            Scan.repeat1 (Scan.unless (keyword ":") any) --|

            keyword ":" >> make_token Traceability             

      || Scan.max leq_token

           (Scan.literal lexicon >> make_token Keyword)

           (   long_identifier >> make_token Long_Ident

            || identifier >> make_token Ident

           )

      || number >> make_token Number

     )

   );

 \<close> ML \<open> (* we investigate the alternatives || and confirm observations from tracing:

           EACH ROUND OF LEXING CREATES one TOKEN ----------------------vvv *)

 (*fun scan header comment = ...                                                      (*8*)

    (    comment *)

   (*||*)(keyword "For" -- whitespace1) |--

            Scan.repeat1 (Scan.unless (keyword ":") any) --|

            keyword ":" >> make_token Traceability            : chars -> T * chars;

   (*||*)Scan.max leq_token

           (Scan.literal lexicon >> make_token Keyword)

           (   long_identifier >> make_token Long_Ident

            || identifier >> make_token Ident

           )                                                  : chars -> T * chars;

   (*||*)number >> make_token Number                          : chars -> T * chars;

 (*                                               ----------------------^^^ *)

 \<close> ML \<open>

 val aaa = 

   Scan.repeat (Scan.unless (Scan.one is_char_eof) (*8b*)

     ((**)   (tokenize_string (**)-- whitespace(**))      (* reads a first string including , ]  *)

      (**)|| (keyword "," >> tokenize_string)             (* further element of string list ?" " *)

      (**)|| ((Scan.max leq_token                         (* *)

      (**)    (Scan.literal lexicon >> make_token Keyword)(**)

      (**)    (   long_identifier >> make_token Long_Ident(**)

      (**)     || identifier >> make_token Ident)         (**)

      (**)    )  -- whitespace)                           (**)

     )

   );

 \<close> ML \<open>

 val chars = Fdl_Lexer.explode_pos "\"aa\",\"bb\"] ##" Position.start;

 \<close> ML \<open>

 aaa chars; (* --------vvvv here we get both as Tokens, list elements AND list delimiters

    ([(Token (Comment, "aa", {line=1, offset=2}), []),                            (*6a*)

      (Token (Keyword, ",", {line=1, offset=5}), []), 

      (Token (Comment, "bb", {line=1, offset=7}), []), 

      (Token (Keyword, "]", {line=1, offset=10}), 

      [(" ", {line=1, offset=11})])],

     [("#", {line=1, offset=12}), ("#", {line=1, offset=13})])*)

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open> (* what is this part of scan doing ..*)                    (*8*)

 val yyy = Scan.max leq_token

              (Scan.literal lexicon >> make_token Keyword)

              (   long_identifier >> make_token Long_Ident

               || identifier >> make_token Ident);

 yyy: chars -> T * chars;

 \<close> ML \<open>

 val chars = Fdl_Lexer.explode_pos "For " Position.start;

 (**)yyy chars;(* = (Token (Keyword, "For", {line=1, offset=1}), [(" ", ..*)

 \<close> ML \<open>

 val chars = Fdl_Lexer.explode_pos ", " Position.start;

 (**)yyy chars;(* = (Token (Keyword, ",", {line=1, offset=1}), [(" ", ..*)

 \<close> ML \<open>

 val chars = Fdl_Lexer.explode_pos " , " Position.start;

 (** )yyy chars;( * exception FAIL NONE raised (line 204 of "General/scan.ML") *)

 \<close> ML \<open>

 val chars = Fdl_Lexer.explode_pos "id " Position.start;

 (**)yyy chars;(* = (Token (Ident, "id", {line=1, offset=1}), [(" ", ..*)

 \<close> ML \<open>

 val chars = Fdl_Lexer.explode_pos "spec.id " Position.start;

 (**)yyy chars;(* = (Token (Long_Ident, "spec.id", {line=1, offset=1}), [(" ", ..*)

 \<close> ML \<open> (*..we see: this part of scan handles whitespace perfectly! *)

 \<close> ML \<open>

 \<close>  

 subsubsection \<open>play with function types and construct them systematically\<close>

 ML \<open>

 \<close> ML \<open> (* string list is a string || keyword "," || whitespace*)            (*10*)

 tokenize_string                  : chars -> T * chars;

 keyword "," >> make_token Keyword: chars -> T * chars;

 whitespace                       : chars -> chars * chars; (*? ? ? how make this of equal type *)

 \<close> ML \<open>

 val chars = Fdl_Lexer.explode_pos ",  " Position.start;                                     (*11*)

 whitespace chars;

 (* = ([], [(",", {line=1, offset=1}), (" ", {line=1, offset=2}), (" ", {line=1, offset=3})])*)

 \<close> ML \<open>

 val chars = Fdl_Lexer.explode_pos "  ," Position.start;                                     (*11*)

 whitespace chars;

 (* = ([(" ", {line=1, offset=1}), (" ", {line=1, offset=2})], [(",", {line=1, offset=3})])*)

 \<close> ML \<open>

 val chars = Fdl_Lexer.explode_pos " , " Position.start;                                     (*11*)

 whitespace chars;

 (* = ([(" ", {line=1, offset=1})], [(",", {line=1, offset=2}), (" ", {line=1, offset=3})])*)

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open> (* investigate (whitespace -- keyword "," -- whitespace) >> make_token Keyword*)

 \<close> ML \<open>

 val xxx = (* this nicely separates whitespace from "," *)                                   (*12*)

   (whitespace -- keyword "," -- whitespace): chars -> ((chars * chars) * chars) * chars;

 val chars = Fdl_Lexer.explode_pos "   ,   ." Position.start;

 xxx chars;

 (* = (((

     [(" ", {line=1, offset=1}), (" ", {line=1, offset=2}), (" ", {line=1, offset=3})], 

 \<longrightarrow> [(",", {line=1, offset=4})]), 

     [(" ", {line=1, offset=5}), (" ", {line=1, offset=6}), (" ", {line=1, offset=7})]),

     [(".", {line=1, offset=8})])

 ^^^^^^^^^^^^^^^^^^^^^^ this nicely separates whitespace from "," ^^^^^^^^^^^^^^^^^^^^^*)

 \<close> ML \<open>

 tokenize_string                                                            : chars -> T * chars;

 (*whitespace*)keyword ","(*whitespace*) >> make_token Keyword              : chars -> T * chars;

 (* we want this type uniformly for ||                                      ^^^^^^^^^^^^^^^^^^^^^ *)

 \<close> ML \<open>

 val eee = (fn (((_, chs1), _), chs2) => (chs1, chs2)) : (('a * 'b) * 'c) * 'd -> 'b * 'd;  (*14*)

 \<close> text \<open> HOW CORRECT THIS...

 (whitespace -- keyword "," -- whitespace) >> (fn (((_, chs1), _), chs2) => (chs1, chs2));

 ERROR Can't unify (string * Position.T) list to 'a * 'b

 \<close> ML \<open>

 val fff = (fn (((_, chars), _), _) => chars)                :       (('a * 'b) * 'c) * 'd -> 'b;(*14*)

 val ggg = (fn _ => (fn (((_, chars), _), _) => chars))      : 'a -> (('b * 'c) * 'd) * 'e -> 'c;

 val hhh = (fn xxx => (fn (((_, chars), _), _) => chars) xxx):       (('a * 'b) * 'c) * 'd -> 'b;

 val iii = (fn ((_, chars), _) => make_token Keyword chars)

                                                             :      ('a * chars) * 'b -> T

 \<close> ML \<open>

 \<close> ML \<open> (*after above trials we use this pattern for building comma_spaced *)                   (*11a*)

 keyword ","                        : chars -> chars                          * chars;

 make_token Keyword                 :          chars                     -> T        ; 

 keyword "," >> make_token Keyword  : chars ->                              T * chars;

 tokenize_string                    : chars ->                              T * chars;

 whitespace                         : chars -> chars                          * chars;

 \<close> ML \<open>

 \<close> ML \<open>

 val space_comma_space = xxx;

 val make_token_comma = iii;

 val comma_spaced = space_comma_space >> make_token_comma

 \<close> ML \<open>

 xxx  : chars -> ((chars * chars) * chars) * chars;

 (**)

 space_comma_space                  : chars -> ((chars * chars) * chars)      * chars;

 make_token_comma                   :          ((chars * chars) * chars) -> T        ;

 comma_spaced                       : chars ->                              T * chars; (**)

 \<close> ML \<open>

 val chars = Fdl_Lexer.explode_pos "   ,   ." Position.start;

 comma_spaced chars; (*(Token (Keyword, ",", {line=1, offset=4}), [(".", {line=1, offset=8})])*)

 (*\--------- found right type for arguments of Scan.repeat ---------------------------------/*)

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open> (*we use that for a list tokenizer..*) (*13*)

 val string_list = 

   Scan.repeat (tokenize_string || comma_spaced);

 string_list: chars -> T list * chars

 \<close> ML \<open>

 val chars = Fdl_Lexer.explode_pos form_model_str'' Position.start;

 \<close> ML \<open> (* tokenize_string_list works..*)

 string_list chars; (* =

    ([Token (Comment, "Traegerlaenge L", {line=1, offset=2})  , Token (Keyword, ",", {line=1, offset=18}), 

      Token (Comment, "Streckenlast q_0", {line=1, offset=20}), Token (Keyword, ",", {line=1, offset=37}),

      Token (Comment, "Biegelinie y", {line=1, offset=39})    , Token (Keyword, ",", {line=1, offset=52}), 

      Token (Comment, "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", {line=1, offset=54}), 

                                                                Token (Keyword, ",", {line=1, offset=119}), 

      Token (Comment, "FunktionsVariable x", {line=1, offset=121}), 

                                                                Token (Keyword, ",", {line=1, offset=141}),

      Token (Comment, "GleichungsVariablen [c, c_2, c_3, c_4]", {line=1, offset=144}), 

                                                                Token (Keyword, ",", {line=1, offset=183}), 

      Token (Comment, "AbleitungBiegelinie dy", {line=1, offset=185})],

     [("]", {line=1, offset=208})])*)

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open> (*but how connect with tokenizing other parts?..*)

 string_list :                          chars ->  T list * chars;

 Scan.repeat1: ('a    -> 'b * 'a   ) -> 'a    -> 'b list * 'a;

 Scan.repeat1: (chars -> 'b * chars) -> chars -> 'b list * chars;

 \<close> ML \<open>

 op @@@ : ('a -> 'b list * 'c) * ('c -> 'b list * 'd) -> 'a -> 'b list * 'd;

 op ::: : ('a -> 'b * 'c) * ('c -> 'b list * 'd) -> 'a -> 'b list * 'd;

 op --  : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e

 \<close> ML \<open>

 \<close> 

 subsubsection \<open>adapt Fdl_Lexer.scan to a tokenizer\<close>

 ML \<open>

 \<close> ML \<open> Fdl_Lexer.scan; (*<ctrl><mouse-click> jumps to the code*) (*14*) 

 \<close> ML \<open> (*the first top down trial fails..*)

 val xxx =

 (*fun scan (*header comment*) =

 ( *!!! "bad header" header --| whitespace --*)

   Scan.repeat (Scan.unless (Scan.one is_char_eof)

     (!!! "bad input"

        ( (*comment

         ||*)(keyword "For" -- whitespace1) |--

               Scan.repeat1 (Scan.unless (keyword ":") any) --|

               keyword ":" >> make_token Traceability             

         || Scan.max leq_token

              (Scan.literal lexicon >> make_token Keyword)

              (   long_identifier >> make_token Long_Ident

               || identifier >> make_token Ident)

         (*|| number >> make_token Number*)) --|

      whitespace) );

 xxx: chars -> T list * chars;

 \<close> ML \<open> (*.. but we see, that the scanner delivers a token per call..*)

 \<close> ML \<open>

 \<close> ML \<open> (*we want a string like "GleichungsVariablen [c, c_2, c_3, c_4]" in ONE token*)

 val chars = Fdl_Lexer.explode_pos (form_single_str ^ ",") Position.start;

 (** )

 xxx chars;

 ( ** )ERROR exception ABORT fn raised (line 109 of "General/scan.ML")( **)

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open> (*we have to tokenize [ and ] and , explicitly..*)

 val xxx =

   keyword "[" -- whitespace --

   Scan.repeat (tokenize_string || comma_spaced) --

   keyword "]"

 \<close> ML \<open>

 val chars = Fdl_Lexer.explode_pos (form_model_str' ^ ".") Position.start;

 xxx chars; (* =    AGAIN WE GET AN UNPLEASANT MIXTURE..

    (((([("[", {line=1, offset=1})], []),

       [Token (Comment, "Traegerlaenge L", {line=1, offset=3}), Token (Keyword, ",", {line=1, offset=19}), Token (Comment, "Streckenlast q_0", {line=1, offset=21}), Token (Keyword, ",", {line=1, offset=38}),

        Token (Comment, "Biegelinie y", {line=1, offset=40}), Token (Keyword, ",", {line=1, offset=53}), Token (Comment, "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", {line=1, offset=55}),

        Token (Keyword, ",", {line=1, offset=120}), Token (Comment, "FunktionsVariable x", {line=1, offset=122}), Token (Keyword, ",", {line=1, offset=142}),

        Token (Comment, "GleichungsVariablen [c, c_2, c_3, c_4]", {line=1, offset=145}), Token (Keyword, ",", {line=1, offset=184}), Token (Comment, "AbleitungBiegelinie dy", {line=1, offset=186})]),

      [("]", {line=1, offset=209})]),

     [(".", {line=1, offset=210})])*)

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open> (* IDEA COMBINING (*8*) and (*13*) for (*15*):

           we do NOT tokenize the whole (string) list, but tokenize_string FIRST *)

 val scan =

 (*fun scan (*header comment*) =

 ( *!!! "bad header" header --| whitespace --*)

   Scan.repeat (Scan.unless (Scan.one is_char_eof)

     (!!! "bad input"

        (   tokenize_string                              (*.. THIS MUST BE FIRST *)

            (*comment

         ||(keyword "For" -- whitespace1) |--

               Scan.repeat1 (Scan.unless (keyword ":") any) --|

               keyword ":" >> make_token Traceability*)

         ||Scan.max leq_token

              (Scan.literal lexicon >> make_token Keyword)

              (   long_identifier >> make_token Long_Ident

               || identifier >> make_token Ident)

       (*|| number >> make_token Number*) ) --|

      whitespace) );

 scan: chars -> T list * chars;

 \<close> ML \<open>

 val chars = Fdl_Lexer.explode_pos (form_single_str ^ ",") Position.start;

 (** )

 xxx chars;

 ( ** )ERROR exception ABORT fn raised (line 109 of "General/scan.ML")( **)

 \<close> ML \<open> (*BUT WITH THE WRAPPER IN tokenize THAT WORKS..*)

 (*fun tokenize_formalise pos str =   KEEP IDENTIFIERS CLOSE TO SPARK..*)

 fun scan' pos str =

 (Scan.finite char_stopper

     (Scan.error scan) (explode_pos str pos));

 \<close> ML \<open>

 val (toks, _) = scan' Position.start formalise_str

 \<close> ML \<open>

 (*it =       ----------------------------------------------------------------- IS PEFECT ! ! ! !

    ([Token (Keyword, "[", {line=1, offset=1}), 

        Token (Keyword, "(", {line=1, offset=2}), 

          Token (Keyword, "[", {line=2, offset=6}), 

            Token (Comment, "Traegerlaenge L", {line=2, offset=8}), Token (Keyword, ",", {line=2, offset=24}), Token (Comment, "Streckenlast q_0", {line=2, offset=27}), Token (Keyword, ",", {line=2, offset=44}), Token (Comment, "Biegelinie y", {line=2, offset=47}), Token (Keyword, ",", {line=2, offset=60}), Token (Comment, "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", {line=3, offset=67}), Token (Keyword, ",", {line=3, offset=132}), Token (Comment, "FunktionsVariable x", {line=4, offset=139}), Token (Keyword, ",", {line=4, offset=159}), Token (Comment, "GleichungsVariablen [c, c_2, c_3, c_4]", {line=4, offset=162}), Token (Keyword, ",", {line=4, offset=201}), Token (Comment, "AbleitungBiegelinie dy", {line=5, offset=208}), 

          Token (Keyword, "]", {line=5, offset=231}), 

        Token (Keyword, ",", {line=5, offset=232}),

          Token (Keyword, "(", {line=6, offset=236}), 

            Token (Comment, "Biegelinie", {line=6, offset=238}), 

          Token (Keyword, ",", {line=6, offset=249}), 

            Token (Keyword, "[", {line=6, offset=251}),

              Token (Comment, "Biegelinien", {line=6, offset=253}), 

            Token (Keyword, "]", {line=6, offset=265}), 

          Token (Keyword, ",", {line=6, offset=266}), 

            Token (Keyword, "[", {line=6, offset=268}),

              Token (Comment, "IntegrierenUndKonstanteBestimmen2", {line=6, offset=270}), 

            Token (Keyword, "]", {line=6, offset=304}), 

          Token (Keyword, ")", {line=6, offset=305}), 

        Token (Keyword, ")", {line=7, offset=307}),

      Token (Keyword, "]", {line=7, offset=308})],

     [])

 \-- ^^ chars EXHAUSTED, PEFECT *)

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 subsubsection \<open>Implement the parser\<close>

 ML \<open>

 \<close> ML \<open> (*the only difference between Parse and Fdl_Parser is Token.T versus Fdl_Lexer.T *)

 Parse.enum1: 

   string ->                      'a parser                                  -> 'a list parser;

 Parse.enum1: 

   string -> (Token.T     list -> 'a * Token.T     list) -> Token.T list     -> 'a list * Token.T     list;

 Fdl_Parser.enum1: 

   string -> (Fdl_Lexer.T list -> 'a * Fdl_Lexer.T list) -> Fdl_Lexer.T list -> 'a list * Fdl_Lexer.T list;

 \<close> ML \<open>

 \<close> ML \<open> (*we start with the initial parentheses..*)

 val xxx =

   Fdl_Parser.$$$ "[" --

     Fdl_Parser.$$$ "(" --

       Fdl_Parser.$$$ "[" |-- 

         Fdl_Parser.!!! (Fdl_Parser.list1 Fdl_Parser.identifier --| 

       Fdl_Parser.$$$ "]")

 \<close> ML \<open> (*need string_list_parser instead ^^^^^^^^^^^^^^^^^^^^^*)

 \<close> ML \<open> (*..vvvvvvvvvv is our model..*)

 Fdl_Parser.identifier: T list -> string * T list;

 \<close> ML \<open> (*we have..*)

 tokenize_string      : chars -> T * chars; (*we need:

 parse_string         : T list -> string * T list;    *)

 \<close> ML \<open>

 \<close> ML \<open> (*in analogy to Fdl_Parser ..*)

 val identifier = Fdl_Parser.group "identifier"

   (Scan.one (fn t => Fdl_Lexer.kind_of t = Fdl_Lexer.Ident) >>

      Fdl_Lexer.content_of);

 \<close> ML \<open> (*.. we implement..*)

 val parse_string = Fdl_Parser.group "string"

   (Scan.one (fn t => Fdl_Lexer.kind_of t = Fdl_Lexer.Comment) >>

      Fdl_Lexer.content_of);

 parse_string         : T list -> string * T list;

 \<close> ML \<open> (*we copy the structure from *101* *)

 val xxx =

   Fdl_Parser.$$$ "[" --

     Fdl_Parser.$$$ "(" --

       (Fdl_Parser.$$$ "[" |-- Fdl_Parser.!!! (

         Fdl_Parser.list1 parse_string --| 

       Fdl_Parser.$$$ "]")) --

     Fdl_Parser.$$$ "," --

       Fdl_Parser.$$$ "(" --

         parse_string --                     (* "Biegelinie" *)

       Fdl_Parser.$$$ "," --

         (Fdl_Parser.$$$ "[" |-- Fdl_Parser.!!! (

           Fdl_Parser.list1 parse_string --| (* ["Biegelinien"] *)

         Fdl_Parser.$$$ "]")) --

       Fdl_Parser.$$$ "," --

         (Fdl_Parser.$$$ "[" |-- Fdl_Parser.!!! (

           Fdl_Parser.list1 parse_string --| (* ["IntegrierenUndKonstanteBestimmen2"] *)

         Fdl_Parser.$$$ "]")) --

       Fdl_Parser.$$$ ")" --

     Fdl_Parser.$$$ ")" --

   Fdl_Parser.$$$ "]"

 \<close> ML \<open> (*.. this compiles correctly, but we modularise into parse_form_model..*)

 val parse_form_model =

   (Fdl_Parser.$$$ "[" |-- Fdl_Parser.!!! (

     Fdl_Parser.list1 parse_string --| 

   Fdl_Parser.$$$ "]"));

 parse_form_model: T list -> string list * T list;

 \<close> ML \<open>

 type form_model =           string list;

 parse_form_model: T list -> form_model   * T list

 \<close> ML \<open>

 \<close> ML \<open> (*.. and into parse_form_refs..*)

 val parse_form_refs = 

   Fdl_Parser.$$$ "(" --

     parse_string --                     (* "Biegelinie" *)

   Fdl_Parser.$$$ "," --

     (Fdl_Parser.$$$ "[" |-- Fdl_Parser.!!! (

       Fdl_Parser.list1 parse_string --| (* ["Biegelinien"] *)

     Fdl_Parser.$$$ "]")) --

   Fdl_Parser.$$$ "," --

     (Fdl_Parser.$$$ "[" |-- Fdl_Parser.!!! (

       Fdl_Parser.list1 parse_string --| (* ["IntegrierenUndKonstanteBestimmen2"] *)

     Fdl_Parser.$$$ "]")) --

   Fdl_Parser.$$$ ")";

 parse_form_refs: T list -> ((((((string * string) * string) * string list) * string) * string list) * string) * T list;

 \<close> ML \<open>

 type form_refs = (((((string * string) * string) * string list) * string) * string list) * string;

 parse_form_refs: T list -> form_refs * T list; (*..how can we use this type --------------vvvvv*)

 \<close> ML \<open>

 \<close> ML \<open> (*we combinge parse_form_model and parse_form_refs..*)

 (*val parse_formalise =   KEEP IDENTIFIERS CLOSE TO SPARK..*)

 val vcs =

   Fdl_Parser.!!! (

     Fdl_Parser.$$$ "[" --

       Fdl_Parser.$$$ "(" --

         parse_form_model --

       Fdl_Parser.$$$ "," --

         parse_form_refs --

       Fdl_Parser.$$$ ")" --

     Fdl_Parser.$$$ "]");

 (*                                      vvvvvvvvvv*)

 vcs: T list -> ((((((string * string) * form_model) * string) * (*------------refs..*)

   ((((((string * string) * string) * string list) * string) * string list) * string)) * string) * string) * T list;

 \<close> ML \<open>

 \<close> ML \<open> (*we use code from the parser..*)

 val (parsed', []) = (*TODO *##* *)

 Scan.finite Fdl_Lexer.stopper (Scan.error (Fdl_Parser.!!! vcs)) toks;

 (*see SPARK 99, but ..^^^^^^^ we don't need that ---------vvv   vvvv*)

 \<close> ML \<open>

 val (parsed', []) =                                       vcs   toks;

 \<close> ML \<open> (*..however, we adopt   vvvvvvvvvvvvvvvvvvvvvvvvvv error handling*)

 val (parsed', []) =           (Scan.error (Fdl_Parser.!!! vcs)) toks;

 \<close> ML \<open>

 case parsed' of

  ((((( (

   "[", 

     "("),

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

       ")")),

     ")"),

   "]") => ()

 | _ => error "parse_formalise CHANGED";

 \<close> ML \<open>

 \<close> ML \<open> (*we read out Formalisation.T from the parser's result..*)

 fun read_out_formalise ((((( (

   "[", 

     "("),

       form_model: TermC.as_string list),

     ","), ((((((

       "(", 

         thy_id: ThyC.id), 

       ","), 

         probl_id: Problem.id), 

       ","), 

         meth_id: Method.id), 

       ")")),

     ")"),

   "]") = [(form_model, (thy_id, probl_id, meth_id))]

 | read_out_formalise _ =

   raise ERROR "read_out_formalise: WRONGLY parsed";

 read_out_formalise:

   (((((string * string) * TermC.as_string list) * string) * 

       ((((((string * ThyC.id) * string) * Problem.id) * string) * Method.id) * string)) * string) * string ->

     (TermC.as_string list * (ThyC.id * Problem.id * Method.id)) list;

 \<close> ML \<open>

 type formalise = (((((string * string) * TermC.as_string list) * string) *

   ((((((string * ThyC.id) * string) * Problem.id) * string) * Method.id) * string)) * string) * string;

 read_out_formalise: formalise -> Formalise.T list

 \<close> ML \<open>

 if (read_out_formalise parsed' : Formalise.T list ) =

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

 then () else error "read_out_formalise CHANGED";

 \<close> ML \<open>

 \<close>

 end