wneuper/isa: src/Tools/isac/BridgeJEdit/Calculation.thy@2fdf32b16c44

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

     2     Author:     Walther Neuper, JKU Linz

     3     (c) due to copyright terms

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

     6 *)

     8 theory Calculation

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

    10 keywords

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

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

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

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

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

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

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

    18 begin

    20 ML_file parseC.sml

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

    23 ML \<open>

    24 \<close> ML \<open>

    25 \<close> ML \<open>

    26 \<close> ML \<open>

    27 \<close>

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

    30 text \<open>

    31   We minimally change code for Example, until all works.

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

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

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

    37   must be outcommented.

    38 \<close>

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

    41 ML \<open>

    42 \<close> ML \<open>

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

    44     Author:     Walther Neuper, JKU Linz

    45     (c) due to copyright terms

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

    48 *)

    50 (** theory data **)

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

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

    56 val name_ord = prod_ord string_ord (option_ord int_ord) o

    57   apply2 (strip_number ##> Int.fromString);

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

    61 structure VCs = Theory_Data

    62 (

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

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

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

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

    67      env:

    68        {ctxt: Element.context_i list,

    69         defs: (binding * thm) list,

    70         types: Fdl_Parser.fdl_type Fdl_Parser.tab,

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

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

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

    74         proving: bool,

    75         vcs: (string * thm list option *

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

    77         path: Path.T,

    78         prefix: string} option}

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

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

    81   val extend = I

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

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

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

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

    86          env = NONE}

    87     | merge _ = err_unfinished ()

    88 )

    90 (** utilities **)

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

    95 (** set up verification conditions **)

    97 fun partition_opt f =

    98   let

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

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

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

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

   103   in part [] [] end;

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

   106   | dest_def _ = NONE;

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

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

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

   113 fun complex_expr (Fdl_Parser.Number _) = false

   114   | complex_expr (Fdl_Parser.Ident _) = false

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

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

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

   118   | complex_expr _ = true;

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

   121       complex_expr e orelse exists complex_expr es

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

   123       complex_expr e orelse complex_expr e' orelse

   124       exists complex_expr es;

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

   127   | is_trivial_vc _ = false;

   130 fun rulenames rules = commas

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

   134 val is_pfun =

   135   Symtab.defined builtin orf

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

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

   138   equal "succ" orf equal "pred";

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

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

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

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

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

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

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

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

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

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

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

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

   153       fold_opt (fold_expr f g) default #>

   154       fold (fold_pair

   155         (fold (fold (fold_pair

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

   157         (fold_expr f g)) assocs;

   160 fun add_expr_pfuns funs = fold_expr

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

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

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

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

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

   167       | x => x);

   169 fun fold_vcs f vcs =

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

   172 fun pfuns_of_vcs prfx funs pfuns vcs =

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

   174   filter (is_none o lookup_prfx prfx pfuns);

   176 val booleanN = "boolean";

   177 val integerN = "integer";

   180 fun get_type thy prfx ty =

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

   182   in lookup_prfx prfx type_map ty end;

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

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

   186   | mk_type' thy prfx ty =

   187       (case get_type thy prfx ty of

   188          NONE =>

   189            (Syntax.check_typ (Proof_Context.init_global thy)

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

   191             [])

   192        | SOME p => p);

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

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

   197     NONE => ()

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

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

   202 fun define_overloaded (def_name, eq) lthy =

   203   let

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

   205       Logic.dest_equals |>> dest_Free;

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

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

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

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

   210   in (thm', lthy') end;

   212 (** generate properties of enumeration types **)

   214 fun add_enum_type tyname tyname' thy =

   215   let

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

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

   218     val k = length cs;

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

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

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

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

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

   225     fun mk_binrel_def s f = Logic.mk_equals

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

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

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

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

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

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

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

   236         (p,

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

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

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

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

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

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

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

   246     val UNIV_eq = Goal.prove lthy [] []

   247       (HOLogic.mk_Trueprop (HOLogic.mk_eq

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

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

   250          resolve_tac ctxt @{thms subset_antisym} 1 THEN

   251          resolve_tac ctxt @{thms subsetI} 1 THEN

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

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

   254          ALLGOALS (asm_full_simp_tac ctxt));

   256     val finite_UNIV = Goal.prove lthy [] []

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

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

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

   261     val card_UNIV = Goal.prove lthy [] []

   262       (HOLogic.mk_Trueprop (HOLogic.mk_eq

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

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

   266     val range_pos = Goal.prove lthy [] []

   267       (HOLogic.mk_Trueprop (HOLogic.mk_eq

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

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

   270               p $ HOLogic.mk_UNIV T,

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

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

   273               HOLogic.mk_number HOLogic.intT 0 $

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

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

   276          simp_tac (ctxt addsimps [card_UNIV]) 1 THEN

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

   278          resolve_tac ctxt @{thms subset_antisym} 1 THEN

   279          simp_tac ctxt 1 THEN

   280          resolve_tac ctxt @{thms subsetI} 1 THEN

   281          asm_full_simp_tac (ctxt addsimps @{thms interval_expand}

   282            delsimps @{thms atLeastLessThan_iff}) 1);

   284     val lthy' =

   285       Class.prove_instantiation_instance (fn ctxt =>

   286         Class.intro_classes_tac ctxt [] THEN

   287         resolve_tac ctxt [finite_UNIV] 1 THEN

   288         resolve_tac ctxt [range_pos] 1 THEN

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

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

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

   293       let

   294         val n = HOLogic.mk_number HOLogic.intT i;

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

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

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

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

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

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

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

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

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

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

   306       (HOLogic.mk_Trueprop (HOLogic.mk_eq

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

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

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

   311       (HOLogic.mk_Trueprop (HOLogic.mk_eq

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

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

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

   315   in

   316     lthy' |>

   317     Local_Theory.note

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

   319     Local_Theory.note

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

   321     Local_Theory.note

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

   323     Local_Theory.note

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

   325     Local_Theory.note

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

   327     Local_Theory.exit_global

   328   end;

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

   333 fun check_enum [] [] = NONE

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

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

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

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

   338       if lcase_eq (el, cname) then check_enum els cs

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

   340         " or it is at the wrong position");

   342 fun strip_prfx s =

   343   let

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

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

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

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

   349 fun assoc_ty_err thy T s msg =

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

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

   353 fun check_enum [] [] = NONE

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

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

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

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

   358       if lcase_eq (el, cname) then check_enum els cs

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

   360         " or it is at the wrong position");

   362 fun unprefix_pfun "" s = s

   363   | unprefix_pfun prfx s =

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

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

   367 fun invert_map [] = I

   368   | invert_map cmap =

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

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

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

   373       Record.get_info thy (Long_Name.qualifier tyname)

   374   | _ => NONE);

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

   379       (check_no_assoc thy prfx s;

   380        (ids,

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

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

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

   385       let

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

   387             NONE =>

   388               let

   389                 val tyb = Binding.name s;

   390                 val tyname = Sign.full_name thy tyb

   391               in

   392                 (thy |>

   393                  BNF_LFP_Compat.add_datatype [BNF_LFP_Compat.Keep_Nesting]

   394                    [((tyb, [], NoSyn),

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

   396                  add_enum_type s tyname,

   397                  tyname)

   398               end

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

   400               (case BNF_LFP_Compat.get_constrs thy tyname of

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

   402                | SOME cs =>

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

   404                    in

   405                      case check_enum (map (unprefix_pfun prfx') els)

   406                          (invert_map cmap cs) of

   407                        NONE => (thy, tyname)

   408                      | SOME msg => assoc_ty_err thy T s msg

   409                    end)

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

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

   412       in

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

   414           fold Name.declare els ctxt),

   415          thy')

   416       end

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

   419       (check_no_assoc thy prfx s;

   420        (ids,

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

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

   423              mk_type thy prfx resty) thy |> snd))

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

   426       (ids,

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

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

   429        in case get_type thy prfx s of

   430            NONE =>

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

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

   433          | SOME (rT, cmap) =>

   434              (case get_record_info thy rT of

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

   436               | SOME {fields, ...} =>

   437                   let val fields' = invert_map cmap fields

   438                   in

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

   440                        [] => ()

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

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

   443                      map (fn (fld, T) =>

   444                        case AList.lookup lcase_eq fields' fld of

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

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

   447                            ("has field " ^

   448                             fld ^ " whose type\n" ^

   449                             Syntax.string_of_typ_global thy U ^

   450                             "\ndoes not match declared type\n" ^

   451                             Syntax.string_of_typ_global thy T)) fldTs;

   452                      thy)

   453                   end)

   454        end)

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

   457       (ids,

   458        case get_type thy prfx s of

   459          SOME _ => thy

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

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

   463       (check_no_assoc thy prfx s;

   464        (ids,

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

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

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

   469       let

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

   471             NONE =>

   472               let

   473                 val tyb = Binding.name s;

   474                 val tyname = Sign.full_name thy tyb

   475               in

   476                 (thy |>

   477                  BNF_LFP_Compat.add_datatype [BNF_LFP_Compat.Keep_Nesting]

   478                    [((tyb, [], NoSyn),

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

   480                  add_enum_type s tyname,

   481                  tyname)

   482               end

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

   484               (case BNF_LFP_Compat.get_constrs thy tyname of

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

   486                | SOME cs =>

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

   488                    in

   489                      case check_enum (map (unprefix_pfun prfx') els)

   490                          (invert_map cmap cs) of

   491                        NONE => (thy, tyname)

   492                      | SOME msg => assoc_ty_err thy T s msg

   493                    end)

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

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

   496       in

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

   498           fold Name.declare els ctxt),

   499          thy')

   500       end

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

   503       (check_no_assoc thy prfx s;

   504        (ids,

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

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

   507              mk_type thy prfx resty) thy |> snd))

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

   510       (ids,

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

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

   513        in case get_type thy prfx s of

   514            NONE =>

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

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

   517          | SOME (rT, cmap) =>

   518              (case get_record_info thy rT of

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

   520               | SOME {fields, ...} =>

   521                   let val fields' = invert_map cmap fields

   522                   in

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

   524                        [] => ()

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

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

   527                      map (fn (fld, T) =>

   528                        case AList.lookup lcase_eq fields' fld of

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

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

   531                            ("has field " ^

   532                             fld ^ " whose type\n" ^

   533                             Syntax.string_of_typ_global thy U ^

   534                             "\ndoes not match declared type\n" ^

   535                             Syntax.string_of_typ_global thy T)) fldTs;

   536                      thy)

   537                   end)

   538        end)

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

   541       (ids,

   542        case get_type thy prfx s of

   543          SOME _ => thy

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

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

   547   let

   548     val T = mk_type thy prfx ty;

   549     val b = Binding.name s;

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

   551   in

   552     (c,

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

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

   555   end;

   557 fun mk_unop s t =

   558   let val T = fastype_of t

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

   561 fun strip_underscores s =

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

   564 fun strip_tilde s =

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

   567 val mangle_name = strip_underscores #> strip_tilde;

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

   570   let

   571     val T = mk_type thy prfx ty;

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

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

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

   576 fun find_field [] fname fields =

   577       find_first (curry lcase_eq fname o fst) fields

   578   | find_field cmap fname fields =

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

   580          NONE => NONE

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

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

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

   586 fun mk_times (t, u) =

   587   let

   588     val setT = fastype_of t;

   589     val T = HOLogic.dest_setT setT;

   590     val U = HOLogic.dest_setT (fastype_of u)

   591   in

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

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

   594   end;

   597 fun term_of_expr thy prfx types pfuns =

   598   let

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   658       | tm_of (tab, _) (Fdl_Parser.Ident s) =

   659           (case Symtab.lookup tab s of

   660              SOME t_ty => t_ty

   661            | NONE => (case lookup_prfx prfx pfuns s of

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

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

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

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

   668           let

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

   670             val q = (case s of

   671                 "for_all" => HOLogic.mk_all

   672               | "for_some" => HOLogic.mk_exists)

   673           in

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

   675                ys (fst (tm_of vs' e)),

   676              booleanN)

   677           end

   679       | tm_of vs (Fdl_Parser.Funct (s, es)) =

   681           (* record field selection *)

   682           (case try (unprefix "fld_") s of

   683              SOME fname => (case es of

   684                [e] =>

   685                  let

   686                    val (t, rcdty) = tm_of vs e;

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

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

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

   690                        (case (find_field cmap fname fields,

   691                             find_field' fname fldtys) of

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

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

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

   695                             " has no field named " ^ fname))

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

   697                  end

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

   699            | NONE =>

   701           (* record field update *)

   702           (case try (unprefix "upf_") s of

   703              SOME fname => (case es of

   704                [e, e'] =>

   705                  let

   706                    val (t, rcdty) = tm_of vs e;

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

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

   709                    val fT = mk_type thy prfx fldty

   710                  in case get_record_info thy rT of

   711                      SOME {fields, ...} =>

   712                        (case find_field cmap fname fields of

   713                           SOME (fname', fU) =>

   714                             if fT = fU then

   715                               (Const (fname' ^ "_update",

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

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

   718                                rcdty)

   719                             else error ("Type\n" ^

   720                               Syntax.string_of_typ_global thy fT ^

   721                               "\ndoes not match type\n" ^

   722                               Syntax.string_of_typ_global thy fU ^

   723                               "\nof field " ^ fname)

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

   725                             " has no field named " ^ fname))

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

   727                  end

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

   729            | NONE =>

   731           (* enumeration type to integer *)

   732           (case try (unsuffix "__pos") s of

   733              SOME tyname => (case es of

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

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

   736                  integerN)

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

   738            | NONE =>

   740           (* integer to enumeration type *)

   741           (case try (unsuffix "__val") s of

   742              SOME tyname => (case es of

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

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

   745                  tyname)

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

   747            | NONE =>

   749           (* successor / predecessor of enumeration type element *)

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

   751               [e] =>

   752                 let

   753                   val (t, tyname) = tm_of vs e;

   754                   val T = mk_type thy prfx tyname

   755                 in (Const

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

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

   758                 end

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

   761           (* user-defined proof function *)

   762           else

   763             (case lookup_prfx prfx pfuns s of

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

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

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

   768       | tm_of vs (Fdl_Parser.Element (e, es)) =

   769           let val (t, ty) = tm_of vs e

   770           in case Fdl_Parser.lookup types ty of

   771               SOME (Fdl_Parser.Array_Type (_, elty)) =>

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

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

   774           end

   776       | tm_of vs (Fdl_Parser.Update (e, es, e')) =

   777           let val (t, ty) = tm_of vs e

   778           in case Fdl_Parser.lookup types ty of

   779               SOME (Fdl_Parser.Array_Type (idxtys, elty)) =>

   780                 let

   781                   val T = foldr1 HOLogic.mk_prodT

   782                     (map (mk_type thy prfx) idxtys);

   783                   val U = mk_type thy prfx elty;

   784                   val fT = T --> U

   785                 in

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

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

   788                        fst (tm_of vs e'),

   789                    ty)

   790                 end

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

   792           end

   794       | tm_of vs (Fdl_Parser.Record (s, flds)) =

   795           let

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

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

   798               (case get_record_info thy T of

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

   800                | SOME info => info);

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

   802             val fnames = fields |> invert_map cmap |>

   803               map (Long_Name.base_name o fst);

   804             val fnames' = map fst flds;

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

   806               case AList.lookup lcase_eq flds' s' of

   807                 SOME fval_ty => fval_ty

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

   809                   fnames);

   810             val _ = (case subtract lcase_eq fnames fnames' of

   811                 [] => ()

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

   813                   " in record " ^ s));

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

   815                 [] => ()

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

   817                   " in record " ^ s))

   818           in

   819             (list_comb

   820                (Const (ext_name,

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

   822                 fvals @ [HOLogic.unit]),

   823              s)

   824           end

   826       | tm_of vs (Fdl_Parser.Array (s, default, assocs)) =

   827           (case Fdl_Parser.lookup types s of

   828              SOME (Fdl_Parser.Array_Type (idxtys, elty)) =>

   829                let

   830                  val Ts = map (mk_type thy prfx) idxtys;

   831                  val T = foldr1 HOLogic.mk_prodT Ts;

   832                  val U = mk_type thy prfx elty;

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

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

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

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

   837                  fun mk_idx idx =

   838                    if length Ts <> length idx then

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

   840                    else foldr1 mk_times (map2 mk_idx' Ts idx);

   841                  fun mk_upd (idxs, e) t =

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

   843                    then

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

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

   846                        foldl1 HOLogic.mk_prod

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

   848                        fst (tm_of vs e)

   849                    else

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

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

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

   853                          (map mk_idx idxs) $

   854                        fst (tm_of vs e)

   855                in

   856                  (fold mk_upd assocs

   857                     (case default of

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

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

   860                   s)

   861                end

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

   864   in tm_of end;

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

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

   871   (case Fdl_Parser.lookup consts s of

   872     SOME ty =>

   873       let

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

   875         val T = mk_type thy prfx ty;

   876         val T' = mk_type thy prfx ty';

   877         val _ = T = T' orelse

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

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

   880         val id' = mk_rulename id;

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

   882           |> Specification.definition NONE [] []

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

   884         val phi =

   885           Proof_Context.export_morphism lthy'

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

   887       in

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

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

   890             Local_Theory.exit_global lthy'))

   891        end

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

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

   898 (* sort definitions according to their dependency *)

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

   900   | sort_defs prfx funs pfuns consts defs sdefs =

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

   902          forall (is_some o lookup_prfx prfx pfuns)

   903            (add_expr_pfuns funs e []) andalso

   904          forall (fn id =>

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

   906            consts id)

   907              (add_expr_idents e [])) defs of

   908          SOME d => sort_defs prfx funs pfuns consts

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

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

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

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

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

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

   917   fold_map (add_var prfx)

   918     (map_filter

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

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

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

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

   923         | NONE => NONE)

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

   925     ids_thy;

   927 fun term_of_rule thy prfx types pfuns ids rule =

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

   929   in case rule of

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

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

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

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

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

   935   end;

   938 fun pfun_type thy prfx (argtys, resty) =

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

   941 fun check_pfun_type thy prfx s t optty1 optty2 =

   942   let

   943     val T = fastype_of t;

   944     fun check ty =

   945       let val U = pfun_type thy prfx ty

   946       in

   947         T = U orelse

   948         error ("Type\n" ^

   949           Syntax.string_of_typ_global thy T ^

   950           "\nof function " ^

   951           Syntax.string_of_term_global thy t ^

   952           " associated with proof function " ^ s ^

   953           "\ndoes not match declared type\n" ^

   954           Syntax.string_of_typ_global thy U)

   955       end

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

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

   960 fun check_pfuns_types thy prfx funs =

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

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

   963    in

   964      (check_pfun_type thy prfx s t optty optty';

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

   966    end);

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

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

   974   | pp_open_vcs vcs = pp_vcs

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

   977 fun partition_vcs vcs = VCtab.fold_rev

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

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

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

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

   982   vcs ([], []);

   984 fun print_open_vcs f vcs =

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

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

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

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

   990            Path.T -> string -> theory -> theory *)

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

   992     {pfuns, type_map, env = NONE} =>

   993       {pfuns = pfuns,

   994        type_map = type_map,

   995        env = SOME

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

   997           pfuns = check_pfuns_types thy prefix funs pfuns,

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

   999           prefix = prefix}}

  1000   | _ => err_unfinished ()) thy;

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

  1002 (* Pure/context.ML

  1003 signature THEORY_DATA =

  1004 sig

  1005   type T                                  (*..VCs.T*)

  1006   val get: theory -> T

  1007   val put: T -> theory -> theory

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

  1009 end;

  1010 *)

  1011 \<close> text \<open>

  1012 val hdl =

  1013 \<close> ML \<open>

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

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

  1016   let

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

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

  1019       snd (Fdl_Parser.parse_declarations Position.start g_c_d_fdl_content)

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

  1021     val ((_, ident), vcs) =

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

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

  1024     val formalise :: _ = case header of xxx as

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

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

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

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

  1029     val (hdlPIDE, _, (dI, pI, mI), pors, frees, _) = Step_Specify.initialisePIDE formalise

  1032     val prfx' =

  1033       if opt_prfx = "" then

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

  1035       else opt_prfx;

  1036     val prfx = to_lower prfx';

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

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

  1039     val consts' =

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

  1041     (* ignore all complex rules in rls files *)

  1042     val (rules'', other_rules) =

  1043       List.partition (complex_rule o snd) rules';

  1044     val _ = if null rules'' then ()

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

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

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

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

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

  1052         (pfuns_of_vcs prfx funs pfuns vcs') of

  1053         [] => ()

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

  1056     val (((defs', vars''), ivars), (ids, thy')) =                                        (*..thy'*)

  1057       ((Symtab.empty |>

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

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

  1060         Name.context),                                      (*..ivars*)

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

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

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

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

  1065         ids_thy |>

  1066         fold_map (add_def prfx types pfuns consts)

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

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

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

  1071     val ctxt =

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

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

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

  1075          ((mk_rulename id, []),

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

  1077            other_rules),

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

  1080   in

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

  1082   end;

  1083 \<close> ML \<open>

  1084 \<close>

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

  1087 ML \<open>

  1088 \<close> ML \<open>

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

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

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

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

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

  1096 fun siv_header (_: chars) =

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

  1098 \<close> ML \<open>

  1099 \<close>

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

  1102 ML \<open>

  1103 \<close> ML \<open>

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

  1105     Author:     Walther Neuper, JKU Linz

  1106     (c) due to copyright terms

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

  1109 *)

  1111 fun spark_open header (files, prfx) thy =

  1112 (*Fdl_Lexer.siv_header*)

  1113   let

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

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

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

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

  1118       ], thy') =

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

  1120       files thy);

  1121 (*                                                                                    ^^^^^ arg!*)

  1122     val path = fst (Path.split_ext src_path);

  1123   in

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

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

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

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

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

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

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

  1131     (*SPARK_VCs.*)set_vcs

  1132 (*ADDED*) (**)

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

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

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

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

  1137       path prfx thy'

  1138   end;

  1139 \<close> ML \<open>

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

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

  1142 \<close> ML \<open>

  1143 \<close> ML \<open>

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

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

  1146         snd (Fdl_Parser.parse_declarations Position.start g_c_d_fdl_content)

  1147 \<close> ML \<open>

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

  1149         Fdl_Parser.parse_rules Position.start g_c_d_rls_content

  1150 \<close> ML \<open>

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

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

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

  1154 length vcs = 11;

  1155 vcs;

  1156 \<close> ML \<open>

  1157 \<close> ML \<open>

  1158 \<close>

  1160 section \<open>setup command_keyword \<close>

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

  1162 text \<open>

  1163 (*HIDE for development, activate for Test_Isac*)

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

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

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

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

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

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

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

  1174 fun siv_header (_: chars) =

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

  1176 (*HIDE for development, activate for Test_Isac*)

  1177 \<close> ML \<open>

  1178 \<close>

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

  1180 ML \<open>

  1181 \<close> ML \<open>

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

  1183 \<close> ML \<open>

  1184 val _ =

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

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

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

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

  1189 \<close> ML \<open>

  1190 \<close> ML \<open>

  1191 \<close>

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

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

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

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

  1197 ( ***Output:

  1199 *)

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

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

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

  1203 ( ***Output:

  1205 *)

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

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

  1209 text \<open>

  1210   Possible models, where a file is read and parsed:

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

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

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

  1214   We pursue the latter.

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

  1216   for scanning/parsing Formalise.T.

  1217 \<close>

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

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

  1221 ML \<open>

  1222 open Fdl_Lexer

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

  1224 (*

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

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

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

  1228            The following verification conditions remain to be proved:

  1229              procedure_g_c_d_4

  1230              procedure_g_c_d_11)

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

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

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

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

  1235            of g_c_d_siv_content to args of Fdl_Lexer.scan

  1236   step 3: parse the tokens created by  Fdl_Lexer.scan

  1237 *)

  1238 \<close> ML \<open>

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

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

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

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

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

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

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

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

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

  1249   (string, string2) =

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

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

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

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

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

  1255   case vcss of

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

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

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

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

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

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

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

  1263       [("procedure_g_c_d_4",

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

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

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

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

  1268 else error "Fdl_Parser.parse_vcs vcss CHANGED 2";

  1269 \<close> ML \<open>

  1270 \<close> ML \<open>

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

  1272 val level1_header_toks =

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

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

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

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

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

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

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

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

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

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

  1284   (string, string2) =

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

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

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

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

  1289   case toks of

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

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

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

  1293 else error "Fdl_Lexer.tokenize header CHANGED 2";

  1294 \<close> ML \<open>

  1295 \<close> ML \<open>

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

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

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

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

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

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

  1302                Fdl_Lexer.scan Fdl_Lexer.siv_header Fdl_Lexer.c_comment chars

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

  1305 case level2_header_toks of

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

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

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

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

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

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

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

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

  1314      Token (Traceability,

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

  1316      _ ),

  1317    []) => ()

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

  1319 \<close> ML \<open>

  1320 \<close> ML \<open>

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

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

  1323 \<close> ML \<open>

  1324 Fdl_Parser.vcs: T list ->

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

  1326   * T list;

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

  1328 \<close> ML \<open>

  1329 val (parsed', _) =

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

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

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

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

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

  1335 \<close> ML \<open>

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

  1337 \<close> ML \<open>

  1338 \<close>

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

  1341 ML \<open>

  1342 \<close> ML \<open>

  1343 val form_single_str = (

  1344   "(\n" ^

  1345 (* Formalise.model: *)

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

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

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

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

  1350 (* Formalise.spec: *)

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

  1352   ")")

  1353 \<close> ML \<open>

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

  1355 \<close> ML \<open>

  1356 val form_spec_str =

  1357 (* Formalise.spec: *)

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

  1359 val form_spec_str' =

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

  1361 \<close> ML \<open>

  1362 val form_model_str = (

  1363 (* Formalise.model: *)

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

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

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

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

  1368 val form_model_str' = ( (* NO whitespace *)

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

  1370 \<close> ML \<open>

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

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

  1373 \<close> ML \<open>

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

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

  1376 \<close> ML \<open>

  1377 \<close>

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

  1380 text \<open>

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

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

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

  1384 \<close>

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

  1387 ML \<open>

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

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

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

  1391 tokenize_string: chars -> T * chars

  1392 \<close> ML \<open>

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

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

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

  1396     [(",", {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}),

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

  1398 \<close> ML \<open>

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

  1400 val tokenize_strings =

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

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

  1403   Fdl_Lexer.keyword "]");

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

  1405 \<close> ML \<open>

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

  1407 tokenize_strings chars;(* =       THIS LOOKS PROMISING..

  1408    ([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}),

  1409      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}),

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

  1411     [])*)

  1412 \<close> ML \<open>

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

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

  1415 (* (*6*)

  1416 tokenize_strings chars;

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

  1418 \<close> ML \<open>

  1419 \<close> ML \<open>

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

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

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

  1423 \<close> ML \<open>

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

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

  1426 val xxx =

  1427   whitespace --

  1428     keyword "(" --

  1429       keyword "[";

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

  1431 \<close> ML \<open>

  1432 val xxx =

  1433                                       whitespace --

  1434     keyword "(" --

  1435       keyword "[" -- tokenize_string;

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

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

  1438 \<close> ML \<open>

  1439 val xxx =

  1440                                       whitespace --

  1441     keyword "(" --                    whitespace --

  1442       keyword "[" --                  whitespace --

  1443         tokenize_string;

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

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

  1446           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)

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

  1448 \<close> ML \<open>

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

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

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

  1452     [])*)

  1453 \<close> ML \<open>

  1454 tokenize_string: chars -> T * chars;

  1455 whitespace: chars -> chars * chars;

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

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

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

  1459 \<close> ML \<open>

  1460 \<close>

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

  1463 ML \<open>

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

  1465 \<close> ML \<open>

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

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

  1468     ( (*comment *)

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

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

  1471            keyword ":" >> make_token Traceability

  1472      || Scan.max leq_token

  1473           (Scan.literal lexicon >> make_token Keyword)

  1474           (   long_identifier >> make_token Long_Ident

  1475            || identifier >> make_token Ident

  1476           )

  1477      || number >> make_token Number

  1478     )

  1479   );

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

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

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

  1483    (    comment *)

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

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

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

  1487   (*||*)Scan.max leq_token

  1488           (Scan.literal lexicon >> make_token Keyword)

  1489           (   long_identifier >> make_token Long_Ident

  1490            || identifier >> make_token Ident

  1491           )                                                  : chars -> T * chars;

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

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

  1494 \<close> ML \<open>

  1495 val aaa =

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

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

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

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

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

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

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

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

  1504     )

  1505   );

  1506 \<close> ML \<open>

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

  1508 \<close> ML \<open>

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

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

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

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

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

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

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

  1516 \<close> ML \<open>

  1517 \<close> ML \<open>

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

  1519 val yyy = Scan.max leq_token

  1520              (Scan.literal lexicon >> make_token Keyword)

  1521              (   long_identifier >> make_token Long_Ident

  1522               || identifier >> make_token Ident);

  1523 yyy: chars -> T * chars;

  1524 \<close> ML \<open>

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

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

  1527 \<close> ML \<open>

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

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

  1530 \<close> ML \<open>

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

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

  1533 \<close> ML \<open>

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

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

  1536 \<close> ML \<open>

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

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

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

  1540 \<close> ML \<open>

  1541 \<close>

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

  1544 ML \<open>

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

  1546 tokenize_string                  : chars -> T * chars;

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

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

  1549 \<close> ML \<open>

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

  1551 whitespace chars;

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

  1553 \<close> ML \<open>

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

  1555 whitespace chars;

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

  1557 \<close> ML \<open>

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

  1559 whitespace chars;

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

  1561 \<close> ML \<open>

  1562 \<close> ML \<open>

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

  1564 \<close> ML \<open>

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

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

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

  1568 xxx chars;

  1569 (* = (((

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

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

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

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

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

  1575 \<close> ML \<open>

  1576 tokenize_string                                                            : chars -> T * chars;

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

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

  1579 \<close> ML \<open>

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

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

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

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

  1584 \<close> ML \<open>

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

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

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

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

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

  1590 \<close> ML \<open>

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

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

  1593 make_token Keyword                 :          chars                     -> T        ;

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

  1596 tokenize_string                    : chars ->                              T * chars;

  1597 whitespace                         : chars -> chars                          * chars;

  1598 \<close> ML \<open>

  1599 \<close> ML \<open>

  1600 val space_comma_space = xxx;

  1601 val make_token_comma = iii;

  1602 val comma_spaced = space_comma_space >> make_token_comma

  1603 \<close> ML \<open>

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

  1605 (**)

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

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

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

  1609 \<close> ML \<open>

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

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

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

  1613 \<close> ML \<open>

  1614 \<close> ML \<open>

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

  1616 val string_list =

  1617   Scan.repeat (tokenize_string || comma_spaced);

  1618 string_list: chars -> T list * chars

  1619 \<close> ML \<open>

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

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

  1622 string_list chars; (* =

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

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

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

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

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

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

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

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

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

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

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

  1634 \<close> ML \<open>

  1635 \<close> ML \<open>

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

  1637 string_list :                          chars ->  T list * chars;

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

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

  1640 \<close> ML \<open>

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

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

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

  1644 \<close> ML \<open>

  1645 \<close>

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

  1648 ML \<open>

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

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

  1651 val xxx =

  1652 (*fun scan (*header comment*) =

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

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

  1655     (!!! "bad input"

  1656        ( (*comment

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

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

  1659               keyword ":" >> make_token Traceability

  1660         || Scan.max leq_token

  1661              (Scan.literal lexicon >> make_token Keyword)

  1662              (   long_identifier >> make_token Long_Ident

  1663               || identifier >> make_token Ident)

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

  1665      whitespace) );

  1666 xxx: chars -> T list * chars;

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

  1668 \<close> ML \<open>

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

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

  1671 (** )

  1672 xxx chars;

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

  1674 \<close> ML \<open>

  1675 \<close> ML \<open>

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

  1677 val xxx =

  1678   keyword "[" -- whitespace --

  1679   Scan.repeat (tokenize_string || comma_spaced) --

  1680   keyword "]"

  1681 \<close> ML \<open>

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

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

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

  1685       [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}),

  1686        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}),

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

  1688        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})]),

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

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

  1691 \<close> ML \<open>

  1692 \<close> ML \<open>

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

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

  1695 val scan =

  1696 (*fun scan (*header comment*) =

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

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

  1699     (!!! "bad input"

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

  1701            (*comment

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

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

  1704               keyword ":" >> make_token Traceability*)

  1705         ||Scan.max leq_token

  1706              (Scan.literal lexicon >> make_token Keyword)

  1707              (   long_identifier >> make_token Long_Ident

  1708               || identifier >> make_token Ident)

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

  1710      whitespace) );

  1711 scan: chars -> T list * chars;

  1712 \<close> ML \<open>

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

  1714 (** )

  1715 xxx chars;

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

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

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

  1719 fun scan' pos str =

  1720 (Scan.finite char_stopper

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

  1722 \<close> ML \<open>

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

  1724 \<close> ML \<open>

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

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

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

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

  1729            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}),

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  1745     [])

  1746 \-- ^^ chars EXHAUSTED, PEFECT *)

  1747 \<close> ML \<open>

  1748 \<close> ML \<open>

  1749 \<close>

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

  1752 ML \<open>

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

  1754 Parse.enum1:

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

  1756 Parse.enum1:

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

  1758 Fdl_Parser.enum1:

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

  1760 \<close> ML \<open>

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

  1762 val xxx =

  1763   Fdl_Parser.$$$ "[" --

  1764     Fdl_Parser.$$$ "(" --

  1765       Fdl_Parser.$$$ "[" |--

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

  1767       Fdl_Parser.$$$ "]")

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

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

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

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

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

  1773 parse_string         : T list -> string * T list;    *)

  1774 \<close> ML \<open>

  1775 \<close> ML \<open> (*in analogy to Fdl_Parser ..*)

  1776 val identifier = Fdl_Parser.group "identifier"

  1777   (Scan.one (fn t => Fdl_Lexer.kind_of t = Fdl_Lexer.Ident) >>

  1778      Fdl_Lexer.content_of);

  1779 \<close> ML \<open> (*.. we implement..*)

  1780 val parse_string = Fdl_Parser.group "string"

  1781   (Scan.one (fn t => Fdl_Lexer.kind_of t = Fdl_Lexer.Comment) >>

  1782      Fdl_Lexer.content_of);

  1783 parse_string         : T list -> string * T list;

  1784 \<close> ML \<open> (*we copy the structure from *101* *)

  1785 val xxx =

  1786   Fdl_Parser.$$$ "[" --

  1787     Fdl_Parser.$$$ "(" --

  1788       (Fdl_Parser.$$$ "[" |-- Fdl_Parser.!!! (

  1789         Fdl_Parser.list1 parse_string --|

  1790       Fdl_Parser.$$$ "]")) --

  1791     Fdl_Parser.$$$ "," --

  1792       Fdl_Parser.$$$ "(" --

  1793         parse_string --                     (* "Biegelinie" *)

  1794       Fdl_Parser.$$$ "," --

  1795         (Fdl_Parser.$$$ "[" |-- Fdl_Parser.!!! (

  1796           Fdl_Parser.list1 parse_string --| (* ["Biegelinien"] *)

  1797         Fdl_Parser.$$$ "]")) --

  1798       Fdl_Parser.$$$ "," --

  1799         (Fdl_Parser.$$$ "[" |-- Fdl_Parser.!!! (

  1800           Fdl_Parser.list1 parse_string --| (* ["IntegrierenUndKonstanteBestimmen2"] *)

  1801         Fdl_Parser.$$$ "]")) --

  1802       Fdl_Parser.$$$ ")" --

  1803     Fdl_Parser.$$$ ")" --

  1804   Fdl_Parser.$$$ "]"

  1805 \<close> ML \<open> (*.. this compiles correctly, but we modularise into parse_form_model..*)

  1806 val parse_form_model =

  1807   (Fdl_Parser.$$$ "[" |-- Fdl_Parser.!!! (

  1808     Fdl_Parser.list1 parse_string --|

  1809   Fdl_Parser.$$$ "]"));

  1810 parse_form_model: T list -> string list * T list;

  1811 \<close> ML \<open>

  1812 type form_model =           string list;

  1813 parse_form_model: T list -> form_model   * T list

  1814 \<close> ML \<open>

  1815 \<close> ML \<open> (*.. and into parse_form_refs..*)

  1816 val parse_form_refs =

  1817   Fdl_Parser.$$$ "(" --

  1818     parse_string --                     (* "Biegelinie" *)

  1819   Fdl_Parser.$$$ "," --

  1820     (Fdl_Parser.$$$ "[" |-- Fdl_Parser.!!! (

  1821       Fdl_Parser.list1 parse_string --| (* ["Biegelinien"] *)

  1822     Fdl_Parser.$$$ "]")) --

  1823   Fdl_Parser.$$$ "," --

  1824     (Fdl_Parser.$$$ "[" |-- Fdl_Parser.!!! (

  1825       Fdl_Parser.list1 parse_string --| (* ["IntegrierenUndKonstanteBestimmen2"] *)

  1826     Fdl_Parser.$$$ "]")) --

  1827   Fdl_Parser.$$$ ")";

  1828 parse_form_refs: T list -> ((((((string * string) * string) * string list) * string) * string list) * string) * T list;

  1829 \<close> ML \<open>

  1830 type form_refs = (((((string * string) * string) * string list) * string) * string list) * string;

  1831 parse_form_refs: T list -> form_refs * T list; (*..how can we use this type --------------vvvvv*)

  1832 \<close> ML \<open>

  1833 \<close> ML \<open> (*we combinge parse_form_model and parse_form_refs..*)

  1834 (*val parse_formalise =   KEEP IDENTIFIERS CLOSE TO SPARK..*)

  1835 val vcs =

  1836   Fdl_Parser.!!! (

  1837     Fdl_Parser.$$$ "[" --

  1838       Fdl_Parser.$$$ "(" --

  1839         parse_form_model --

  1840       Fdl_Parser.$$$ "," --

  1841         parse_form_refs --

  1842       Fdl_Parser.$$$ ")" --

  1843     Fdl_Parser.$$$ "]");

  1844 (*                                      vvvvvvvvvv*)

  1845 vcs: T list -> ((((((string * string) * form_model) * string) * (*------------refs..*)

  1846   ((((((string * string) * string) * string list) * string) * string list) * string)) * string) * string) * T list;

  1847 \<close> ML \<open>

  1848 \<close> ML \<open> (*we use code from the parser..*)

  1849 val (parsed', []) = (*TODO *##* *)

  1850 Scan.finite Fdl_Lexer.stopper (Scan.error (Fdl_Parser.!!! vcs)) toks;

  1851 (*see SPARK 99, but ..^^^^^^^ we don't need that ---------vvv   vvvv*)

  1852 \<close> ML \<open>

  1853 val (parsed', []) =                                       vcs   toks;

  1854 \<close> ML \<open> (*..however, we adopt   vvvvvvvvvvvvvvvvvvvvvvvvvv error handling*)

  1855 val (parsed', []) =           (Scan.error (Fdl_Parser.!!! vcs)) toks;

  1856 \<close> ML \<open>

  1857 case parsed' of

  1858  ((((( (

  1859   "[",

  1860     "("),

  1861       [ "Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

  1862         "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x",

  1863         "GleichungsVariablen [c, c_2, c_3, c_4]", "AbleitungBiegelinie dy"

  1864       ]),

  1865     ","), ((((((

  1866       "(",

  1867         "Biegelinie"),

  1868       ","),

  1869         ["Biegelinien"]),

  1870       ","),

  1871         ["IntegrierenUndKonstanteBestimmen2"]),

  1872       ")")),

  1873     ")"),

  1874   "]") => ()

  1875 | _ => error "parse_formalise CHANGED";

  1876 \<close> ML \<open>

  1877 \<close> ML \<open> (*we read out Formalisation.T from the parser's result..*)

  1878 fun read_out_formalise ((((( (

  1879   "[",

  1880     "("),

  1881       form_model: TermC.as_string list),

  1882     ","), ((((((

  1883       "(",

  1884         thy_id: ThyC.id),

  1885       ","),

  1886         probl_id: Problem.id),

  1887       ","),

  1888         meth_id: Method.id),

  1889       ")")),

  1890     ")"),

  1891   "]") = [(form_model, (thy_id, probl_id, meth_id))]

  1892 | read_out_formalise _ =

  1893   raise ERROR "read_out_formalise: WRONGLY parsed";

  1894 read_out_formalise:

  1895   (((((string * string) * TermC.as_string list) * string) *

  1896       ((((((string * ThyC.id) * string) * Problem.id) * string) * Method.id) * string)) * string) * string ->

  1897     (TermC.as_string list * (ThyC.id * Problem.id * Method.id)) list;

  1898 \<close> ML \<open>

  1899 type formalise = (((((string * string) * TermC.as_string list) * string) *

  1900   ((((((string * ThyC.id) * string) * Problem.id) * string) * Method.id) * string)) * string) * string;

  1901 read_out_formalise: formalise -> Formalise.T list

  1902 \<close> ML \<open>

  1903 if (read_out_formalise parsed' : Formalise.T list ) =

  1904   [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

  1905      "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x",

  1906      "GleichungsVariablen [c, c_2, c_3, c_4]", "AbleitungBiegelinie dy"],

  1907    ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))]

  1908 then () else error "read_out_formalise CHANGED";

  1909 \<close> ML \<open>

  1910 \<close>

  1912 end

author	Walther Neuper <walther.neuper@jku.at>
	Thu, 26 Nov 2020 12:24:37 +0100
changeset 60113	2fdf32b16c44
parent 60112	04c8203454f2
child 60114	307fe00bbfc9
permissions	-rw-r--r--