test/Tools/isac/ProgLang/auto_prog.sml
author wneuper <walther.neuper@jku.at>
Sun, 18 Jul 2021 21:15:21 +0200
changeset 60333 7c76b8278a9f
parent 60332 a05877a9f19b
child 60336 dcb37736d573
permissions -rw-r--r--
Test_Isac_Short.thy, Test_Some.the work on new src, new TOODOOs

notes
# the previous changeset run Test_Isac_Short.thy on src/* from before the merge
# errors coming from merge are outcommented with TOODOO
walther@59633
     1
(* Title:  ProgLang/auto_prog.sml
walther@59633
     2
   Author: Walther Neuper 190922
walther@59633
     3
   (c) due to copyright terms
walther@59633
     4
*)
walther@59633
     5
walther@59633
     6
"-----------------------------------------------------------------------------------------------";
walther@59633
     7
"-----------------------------------------------------------------------------------------------";
walther@59633
     8
"table of contents -----------------------------------------------------------------------------";
walther@59633
     9
"-----------------------------------------------------------------------------------------------";
walther@59633
    10
"-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
walther@59633
    11
"-------- test the same called by interSteps norm_Poly -----------------------------------------";
walther@59633
    12
"-------- test the same called by interSteps norm_Rational -------------------------------------";
walther@59637
    13
"-------- fun op #> ----------------------------------------------------------------------------";
walther@59633
    14
"-------- fun rules2scr_Rls --------------------------------------------------------------------";
walther@59633
    15
"-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
walther@59802
    16
"-------- fun stacpbls, fun eval_leaf -----------------------------------";
walther@59633
    17
"-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
walther@59636
    18
"-------- fun subst_typ ------------------------------------------------------------------------";
walther@59636
    19
"-------- fun subst_typs -----------------------------------------------------------------------";
walther@59633
    20
"-----------------------------------------------------------------------------------------------";
walther@59633
    21
"-----------------------------------------------------------------------------------------------";
walther@59633
    22
"-----------------------------------------------------------------------------------------------";
walther@59633
    23
walther@59633
    24
walther@59633
    25
"-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
walther@59633
    26
"-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
walther@59633
    27
"-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
walther@59633
    28
val rls = assoc_rls "integration";
walther@59802
    29
val thy' = @{theory "Integrate"}
walther@59802
    30
val t = @{term "ttt :: real"};
walther@59802
    31
walther@59802
    32
 Auto_Prog.gen thy' t rls;
walther@59932
    33
"~~~~~ fun gen , args:"; val (thy, t, rls) = (thy', t, rls);
walther@59802
    34
    val prog = case rls of
walther@59851
    35
	      Rule_Set.Repeat {rules, ...} => rules2scr_Rls thy rules
walther@59878
    36
	    | Rule_Set.Sequence {rules, ...} => rules2scr_Seq thy rules
walther@59802
    37
    val auto_script = subst_typs prog (type_of t) (TermC.guess_bdv_typ t) (*return from generate*);
walther@59802
    38
walther@59868
    39
if UnparseC.term auto_script =
walther@59802
    40
  "auto_generated_inst t_t v =\n" ^
walther@59802
    41
  "(Try (Rewrite_Set_Inst [(''bdv'', v)] ''integration_rules'') #>\n" ^
walther@59802
    42
  " Try (Rewrite_Set_Inst [(''bdv'', v)] ''add_new_c'') #>\n" ^
walther@59802
    43
  " Try (Rewrite_Set_Inst [(''bdv'', v)] ''simplify_Integral''))\n" ^
walther@59802
    44
  " ??.empty"
walther@59802
    45
then () else error "Auto_Prog.gen integration CHANGED";
walther@59633
    46
walther@59633
    47
if contain_bdv (get_rules rls) then ()
walther@59633
    48
else error "scrtools.sml: contain_bdv doesnt work for 'integration'";
walther@59633
    49
walther@59997
    50
if UnparseC.terms (formal_args auto_script) = "[\"t_t\", \"v\"]"
walther@59633
    51
then () else error "formal_args of auto-gen.script changed";
walther@59802
    52
walther@60230
    53
    Istate.init_detail (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")) (TermC.str2term "someTermWithBdv");
walther@59935
    54
"~~~~~ fun init_detail , args:"; val ((Tactic.Rewrite_Set_Inst (subs, rls)), t)
walther@60230
    55
  = ((Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")), TermC.str2term "someTermWithBdv");
walther@59911
    56
      val v = case Subst.T_from_input (ThyC.get_theory "Isac_Knowledge") subs of
walther@59802
    57
        (_, v) :: _ => v;
walther@59802
    58
    (*case*) assoc_rls rls (*of*);
walther@59802
    59
walther@59633
    60
walther@59633
    61
"-------- test the same called by interSteps norm_Poly -----------------------------------------";
walther@59633
    62
"-------- test the same called by interSteps norm_Poly -----------------------------------------";
walther@59633
    63
"-------- test the same called by interSteps norm_Poly -----------------------------------------";
walther@59802
    64
val rls = assoc_rls "norm_Poly";
walther@59802
    65
val thy' = @{theory "Poly"}
walther@59802
    66
val t = @{term "ttt :: real"}
walther@59802
    67
val auto_script = Auto_Prog.gen thy' t rls;
walther@59802
    68
walther@59868
    69
if UnparseC.term auto_script =
walther@59802
    70
  "auto_generated t_t =\n" ^
walther@59802
    71
  "(Try (Rewrite_Set ''discard_minus'') #>\n" ^
walther@59802
    72
  " Try (Rewrite_Set ''expand_poly_'') #>\n" ^
walther@59802
    73
  " Try (Repeat (Calculate ''TIMES'')) #>\n" ^
walther@59802
    74
  " Try (Rewrite_Set ''order_mult_rls_'') #>\n" ^
walther@59802
    75
  " Try (Rewrite_Set ''simplify_power_'') #>\n" ^
walther@59802
    76
  " Try (Rewrite_Set ''calc_add_mult_pow_'') #>\n" ^
walther@59802
    77
  " Try (Rewrite_Set ''reduce_012_mult_'') #>\n" ^
walther@59802
    78
  " Try (Rewrite_Set ''order_add_rls_'') #>\n" ^
walther@59802
    79
  " Try (Rewrite_Set ''collect_numerals_'') #>\n" ^
walther@59802
    80
  " Try (Rewrite_Set ''reduce_012_'') #>\n" ^
walther@59802
    81
  " Try (Rewrite_Set ''discard_parentheses1''))\n" ^
walther@59802
    82
  " ??.empty"  (*                          ..WORKS, NEVERTHELESS*)
walther@59802
    83
then () else error "Auto_Prog.gen norm_Poly CHANGED";
walther@59633
    84
walther@59633
    85
reset_states (); (*<-- evaluate, if ML-blocks are edited below*)
walther@59633
    86
CalcTree
walther@59633
    87
[(["Term (b + a - b)", "normalform N"], 
walther@59997
    88
  ("Poly",["polynomial", "simplification"],
walther@59997
    89
  ["simplification", "for_polynomials"]))];
walther@59633
    90
Iterator 1;
walther@59633
    91
moveActiveRoot 1;
walther@59633
    92
walther@59633
    93
autoCalculate 1 CompleteCalc;
walther@59633
    94
val ((pt,p),_) = get_calc 1;
walther@59983
    95
Test_Tool.show_pt pt;
walther@59633
    96
(* isabisac17 = 15 [
walther@59633
    97
(([], Frm), Simplify (b + a - b)),
walther@59633
    98
(([1], Frm), b + a - b),
walther@59633
    99
(([1], Res), a),
walther@59633
   100
(([], Res), a)] *)
walther@59633
   101
walther@59633
   102
interSteps 1 ([], Res);
walther@59983
   103
val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
walther@59983
   104
Test_Tool.show_pt pt;
walther@59633
   105
(* isabisac17 = 15 [
walther@59633
   106
(([], Frm), Simplify (b + a - b)),
walther@59633
   107
(([1], Frm), b + a - b),
walther@59633
   108
(([1], Res), a),
walther@59633
   109
(([], Res), a)] *)
walther@59633
   110
walther@59633
   111
interSteps 1 ([1], Res);(*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 8</ERROR></SYSERROR>*)
walther@59633
   112
"~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1], Res));
walther@59633
   113
 val ((pt, p), tacis) = get_calc cI;
walther@59633
   114
(*if*) (not o is_interpos) ip = false;
walther@59633
   115
val ip' = lev_pred' pt ip;
walther@59633
   116
walther@59935
   117
(*Detail_Step.go pt ip      ..ERROR interSteps>..>init_detail: "norm_Poly" has Empty_Prog*)
walther@59833
   118
val ("donesteps", ctree_BEFORE_step_into, pos'_BEFORE_step_into) = Detail_Step.go pt ip;
walther@59833
   119
"~~~~~ fun go, args:"; val (pt, (pos as (p, _))) = (pt, ip);
walther@59633
   120
    val nd = Ctree.get_nd pt p
walther@59633
   121
    val cn = Ctree.children nd;
walther@59633
   122
(*if*) null cn = false;
walther@59633
   123
walther@59633
   124
"~~~~~ to detailrls return val:";
walther@59633
   125
(*else*) 
walther@59694
   126
val return_val = ("donesteps", pt, (p @ [length (Ctree.children (Ctree.get_nd pt p))], Pos.Res));
walther@59633
   127
if p @ [length (Ctree.children (Ctree.get_nd pt p))] = [1, 4]
walther@59633
   128
then () else error "detailrls: auto-generated norm_Poly doesnt work";
walther@59633
   129
walther@59983
   130
val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
walther@59983
   131
Test_Tool.show_pt pt; (*[
walther@59633
   132
(([], Frm), Simplify (b + a - b)),
walther@59633
   133
(([1], Frm), b + a - b),
walther@59633
   134
(([1,1], Frm), b + a - b),
walther@59633
   135
(([1,1], Res), b + a + -1 * b),
walther@59633
   136
(([1,2], Res), a + b + -1 * b),
walther@59633
   137
(([1,3], Res), a + 0 * b),
walther@59633
   138
(([1,4], Res), a),
walther@59633
   139
(([1], Res), a),
walther@59633
   140
(([], Res), a)]  *)
walther@59633
   141
if existpt' ([1,4], Res) pt then ()
walther@59633
   142
else error  "auto-generated norm_Poly doesnt work";
walther@59633
   143
walther@59802
   144
walther@59633
   145
"-------- test the same called by interSteps norm_Rational -------------------------------------";
walther@59633
   146
"-------- test the same called by interSteps norm_Rational -------------------------------------";
walther@59633
   147
"-------- test the same called by interSteps norm_Rational -------------------------------------";
walther@59802
   148
val auto_script =
walther@59802
   149
  Auto_Prog.gen  @{theory "Poly"} @{term "ttt :: real"} (assoc_rls "norm_Rational");
walther@59868
   150
writeln(UnparseC.term auto_script);
walther@60230
   151
TermC.atomty auto_script;
walther@59633
   152
(*** 
walther@59633
   153
*** Const (Program.Stepwise, 'z => 'z => 'z)
walther@59633
   154
*** . Free (t_t, 'z)
walther@59633
   155
*** . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
walther@59633
   156
*** . . Const (Program.Try, ('a => 'a) => 'a => 'a)
walther@60278
   157
*** . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
walther@59633
   158
*** . . . . Free (discard_minus, ID)
walther@59633
   159
*** . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
walther@59633
   160
*** . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
walther@60278
   161
*** . . . . Const (Program.Rewrite_Set, ID  => 'a => 'a)
walther@59633
   162
*** . . . . . Free (rat_mult_poly, ID)
walther@59633
   163
*** . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
walther@59633
   164
*** . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
walther@60278
   165
*** . . . . . Const (Program.Rewrite_Set, ID  => 'a => 'a)
walther@59633
   166
*** . . . . . . Free (make_rat_poly_with_parentheses, ID)
walther@59633
   167
*** . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
walther@59633
   168
*** . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
walther@60278
   169
*** . . . . . . Const (Program.Rewrite_Set, ID  => 'a => 'a)
walther@59633
   170
*** . . . . . . . Free (cancel_p_rls, ID)
walther@59633
   171
*** . . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
walther@59633
   172
*** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
walther@60278
   173
*** . . . . . . . Const (Program.Rewrite_Set, ID  => 'a => 'a)
walther@59633
   174
*** . . . . . . . . Free (norm_Rational_rls, ID)
walther@59633
   175
*** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
walther@60278
   176
*** . . . . . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
walther@59633
   177
*** . . . . . . . . Free (discard_parentheses1, ID)
walther@59633
   178
*** . . Const (empty, 'a)
walther@59633
   179
***)
walther@59633
   180
reset_states ();
walther@59633
   181
CalcTree
walther@59633
   182
[(["Term (b + a - b)", "normalform N"], 
walther@59997
   183
  ("Poly",["polynomial", "simplification"],
walther@59997
   184
  ["simplification", "of_rationals"]))];
walther@59633
   185
Iterator 1;
walther@59633
   186
moveActiveRoot 1;
walther@59633
   187
autoCalculate 1 CompleteCalc;
walther@59633
   188
walther@59633
   189
interSteps 1 ([], Res);
walther@59983
   190
val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
walther@59633
   191
walther@59633
   192
interSteps 1 ([1], Res);
walther@59983
   193
val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
walther@59633
   194
walther@59633
   195
(*with "Program SimplifyScript (t_::real) =                \
walther@59635
   196
       \  ((Rewrite_Set norm_Rational) t_)"
walther@59983
   197
val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([1], Res));
walther@59633
   198
*)
walther@59983
   199
val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([2], Res));
walther@59868
   200
case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
walther@59633
   201
    ("a", Check_Postcond ["polynomial", "simplification"], []) => ()
walther@59633
   202
  | _ => error "scrtools.sml: auto-generated norm_Rational doesnt work";
walther@59633
   203
walther@59802
   204
walther@59637
   205
"-------- fun op #> ----------------------------------------------------------------------------";
walther@59637
   206
"-------- fun op #> ----------------------------------------------------------------------------";
walther@59637
   207
"-------- fun op #> ----------------------------------------------------------------------------";
walther@59852
   208
 val rules = (#rules o Rule_Set.rep) isolate_root;
walther@59633
   209
 val rs = map (rule2stac @{theory}) rules;
walther@59637
   210
 val t = #> rs;
walther@59868
   211
if UnparseC.term t = "Try (Repeat (Rewrite ''rroot_to_lhs'')) #>\n" ^ 
walther@59637
   212
  "Try (Repeat (Rewrite ''rroot_to_lhs_mult'')) #>\n" ^ 
walther@59637
   213
  "Try (Repeat (Rewrite ''rroot_to_lhs_add_mult'')) #>\n" ^ 
walther@59637
   214
  "Try (Repeat (Rewrite ''risolate_root_add'')) #>\n" ^ 
walther@59637
   215
  "Try (Repeat (Rewrite ''risolate_root_mult'')) #>\n" ^ 
walther@59635
   216
  "Try (Repeat (Rewrite ''risolate_root_div''))"
walther@59637
   217
then () else error "fun #> changed"
walther@59633
   218
walther@59802
   219
walther@59633
   220
"-------- fun rules2scr_Rls --------------------------------------------------------------------";
walther@59633
   221
"-------- fun rules2scr_Rls --------------------------------------------------------------------";
walther@59633
   222
"-------- fun rules2scr_Rls --------------------------------------------------------------------";
walther@59633
   223
(*compare Prog_Expr.*)
walther@60333
   224
val prog = Auto_Prog.rules2scr_Rls @{theory} [\<^rule_thm>\<open>thm111\<close>, \<^rule_thm>\<open>refl\<close>]
walther@59633
   225
;
walther@59870
   226
writeln (UnparseC.term_in_thy @{theory} prog);
walther@59633
   227
(*auto_generated t_t =
walther@59633
   228
Repeat
walther@59637
   229
 ((Try (Repeat (Rewrite ''thm111'')) #>
walther@59635
   230
   Try (Repeat (Rewrite ''refl'')))
walther@59633
   231
   ??.empty)*)
walther@59633
   232
;
walther@59870
   233
if UnparseC.term_in_thy @{theory} prog =
walther@59635
   234
  "auto_generated t_t =\n" ^
walther@59635
   235
  "Repeat\n" ^
walther@59637
   236
  " ((Try (Repeat (Rewrite ''thm111'')) #> Try (Repeat (Rewrite ''refl'')))\n" ^
walther@59635
   237
  "   ??.empty)"
walther@59635
   238
then () else error "rules2scr_Rls auto_generated changed";
walther@59633
   239
walther@59802
   240
walther@59633
   241
"-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
walther@59633
   242
"-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
walther@59633
   243
"-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
walther@59871
   244
val t = rule2stac @{theory} (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}));
walther@59868
   245
if UnparseC.term t = "Try (Repeat (Rewrite ''real_diff_minus''))" then ()
walther@59633
   246
else error "rule2stac Thm.. changed";
walther@59633
   247
wenzelm@60309
   248
val t = rule2stac @{theory} (Eval (\<^const_name>\<open>plus\<close>, eval_binop "#add_"));
walther@59868
   249
if UnparseC.term t = "Try (Repeat (Calculate ''PLUS''))" then ()
walther@59878
   250
else error "rule2stac Eval.. changed";
walther@59633
   251
walther@59633
   252
val t = rule2stac @{theory} (Rls_ rearrange_assoc);
walther@59868
   253
if UnparseC.term t = "Try (Rewrite_Set ''rearrange_assoc'')" then ()
walther@59633
   254
else error "rule2stac Rls_.. changed";
walther@59633
   255
walther@59871
   256
val t = rule2stac_inst @{theory} (Thm ("risolate_bdv_add", ThmC.numerals_to_Free @{thm risolate_bdv_add}));
walther@59868
   257
if UnparseC.term t = "Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add''))" then ()
walther@59633
   258
else error "rule2stac_inst Thm.. changed";
walther@59633
   259
case t of
walther@59633
   260
  (Const ("Tactical.Try", _) $
walther@59633
   261
    (Const ("Tactical.Repeat", _) $
walther@60278
   262
      (Const ("Prog_Tac.Rewrite_Inst", _) $
wenzelm@60309
   263
        (Const (\<^const_name>\<open>Cons\<close>, _) $
wenzelm@60309
   264
          (Const (\<^const_name>\<open>Pair\<close>, _) $
walther@59633
   265
            bdv $
walther@59633
   266
            Free ("v", _)) $
wenzelm@60309
   267
          Const (\<^const_name>\<open>Nil\<close>, _)) $
walther@59635
   268
        risolate_bdv_add))) => 
walther@59633
   269
      (if HOLogic.dest_string bdv = "bdv" andalso 
walther@59633
   270
        HOLogic.dest_string risolate_bdv_add = "risolate_bdv_add" then ()
walther@59633
   271
      else error "rule2stac_inst changed 1")
walther@59633
   272
| _ => error "rule2stac_inst changed 2";
walther@59633
   273
walther@59802
   274
walther@59802
   275
"-------- fun stacpbls, fun eval_leaf -----------------------------------";
walther@59802
   276
"-------- fun stacpbls, fun eval_leaf -----------------------------------";
walther@59802
   277
"-------- fun stacpbls, fun eval_leaf -----------------------------------";
walther@60154
   278
val {scr, ...} = MethodC.from_store ["Test", "sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
walther@59633
   279
case stacpbls sc of
walther@59635
   280
  [Const ("Prog_Tac.Rewrite", _) $ square_equation_left,
walther@60278
   281
   Const ("Prog_Tac.Rewrite_Set", _) $ Test_simplify,
walther@60278
   282
   Const ("Prog_Tac.Rewrite_Set", _) $ rearrange_assoc,
walther@60278
   283
   Const ("Prog_Tac.Rewrite_Set", _) $ isolate_root,
walther@60278
   284
   Const ("Prog_Tac.Rewrite_Set", _) $ norm_equation,
walther@60278
   285
   Const ("Prog_Tac.Rewrite_Set_Inst", _) $
wenzelm@60309
   286
     (Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>Pair\<close>, _) $ bdv $ Free ("v_v", _)) $
wenzelm@60309
   287
       Const (\<^const_name>\<open>Nil\<close>, _)) $ isolate_bdv] => 
walther@59633
   288
     if HOLogic.dest_string square_equation_left = "square_equation_left" andalso
walther@59633
   289
       HOLogic.dest_string Test_simplify = "Test_simplify" andalso
walther@59633
   290
       HOLogic.dest_string rearrange_assoc = "rearrange_assoc" andalso
walther@59633
   291
       HOLogic.dest_string isolate_root = "isolate_root" andalso
walther@59633
   292
       HOLogic.dest_string norm_equation = "norm_equation" andalso
walther@59633
   293
       HOLogic.dest_string bdv = "bdv" andalso
walther@59633
   294
       HOLogic.dest_string isolate_bdv = "isolate_bdv"
walther@59633
   295
     then () else error "stacpbls (Test.Solve_root_equation) changed 2"
walther@59633
   296
| _  => error "stacpbls (Test.Solve_root_equation) changed 1";
walther@59633
   297
walther@59633
   298
(* inappropriate input is skipped *)
walther@59633
   299
val t = @{term "(a::real) = (rhs (NTH 1 sol_a))"};
walther@59633
   300
case stacpbls t of [] => () | _ => error "stacpbls rhs (NTH 1 sol_a) changed";
walther@59633
   301
walther@59633
   302
@{term "(SubProblem (BiegelinieX,[vonBelastungZu,Biegelinien], [Biegelinien,ausBelastung]) [REAL q__q, REAL v_v])"};
walther@59633
   303
case stacpbls t of [] => () | _ => error "stacpbls (SubProblem ...) changed";
walther@59633
   304
walther@59802
   305
walther@59633
   306
"-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
walther@59633
   307
"-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
walther@59633
   308
"-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
walther@59633
   309
val rls = prep_rls @{theory} Test_simplify; (* adds the Program *)
walther@59802
   310
val sc = Auto_Prog.gen thy' t rls;
walther@59633
   311
val stacs = stacpbls sc;
walther@59633
   312
walther@59633
   313
val calcs = filter is_calc stacs;
walther@59633
   314
val ids = map op_of_calc calcs;
walther@59633
   315
case ids of
walther@59633
   316
  ["PLUS", "TIMES", "DIVIDE", "POWER"] => ()
walther@59633
   317
| _ => error "op_of_calc";
walther@59633
   318
walther@59633
   319
val calcs = ((assoc_calc' @{theory} |> map) o (map Auto_Prog.op_of_calc) o
walther@59633
   320
  (filter Auto_Prog.is_calc) o Auto_Prog.stacpbls) sc;
walther@59633
   321
case calcs of
wenzelm@60309
   322
  [("PLUS", (\<^const_name>\<open>plus\<close>, _)), ("TIMES", (\<^const_name>\<open>times\<close>, _)), 
wenzelm@60309
   323
  ("DIVIDE", (\<^const_name>\<open>divide\<close>, _)), ("POWER", (\<^const_name>\<open>powr\<close>, _))] => ()
walther@59633
   324
| _ => error "get_calcs changed"
walther@59636
   325
walther@59802
   326
walther@59636
   327
"-------- fun subst_typ ------------------------------------------------------------------------";
walther@59636
   328
"-------- fun subst_typ ------------------------------------------------------------------------";
walther@59636
   329
"-------- fun subst_typ ------------------------------------------------------------------------";
walther@59802
   330
val prog = Auto_Prog.gen @{theory Isac_Knowledge} t (assoc_rls "isolate_bdv");
walther@59868
   331
(* UnparseC.term prog |> writeln
walther@59636
   332
auto_generated_inst t_t v =
walther@59636
   333
Repeat
walther@59637
   334
 ((Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add'')) #>
walther@59637
   335
   Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult_add'')) #>
walther@59637
   336
   Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult'')) #>
walther@59637
   337
   Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''mult_square'')) #>
walther@59637
   338
   Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''constant_square'')) #>
walther@59636
   339
   Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''constant_mult_square'')))
walther@59636
   340
   ??.empty) 
walther@59636
   341
*)
walther@59636
   342
walther@59802
   343
val frees = vars prog; (* = [Free ("t_t", "'z"), Free ("v", "real")]*)
walther@59802
   344
if length frees = 2 then () else error "test setup Auto_Prog.subst_typ changed 1";
walther@59802
   345
walther@59636
   346
val args = formal_args prog; (* = [Free ("t_t", "'z"), Free ("v", "real")]*)
walther@59636
   347
if length args = 2 then () else error "test setup Auto_Prog.subst_typ changed 2";
walther@59636
   348
walther@59636
   349
val typ_t = HOLogic.realT
walther@59636
   350
val typ_bdv = HOLogic.realT
walther@59636
   351
walther@59636
   352
val vars_v = (* = [Free ("v", "real"), Free ("v", "'a")]*)
walther@59636
   353
  filter (fn t => curry op = (t |> dest_Free |> fst) "v") frees
walther@59636
   354
val typs_v = (* = ["real", "'a"]*)
walther@59636
   355
  map (fn t => (t |> dest_Free |> snd)) vars_v;
walther@59636
   356
walther@59802
   357
val subst_ty = subst_typ "v" HOLogic.realT frees; (* = [("real", "real")]*)
walther@59802
   358
if length subst_ty = 1 then () else error "Auto_Prog.subst_typ changed";
walther@59802
   359
walther@59636
   360
walther@59636
   361
"-------- fun subst_typs -----------------------------------------------------------------------";
walther@59636
   362
"-------- fun subst_typs -----------------------------------------------------------------------";
walther@59636
   363
"-------- fun subst_typs -----------------------------------------------------------------------";
walther@59802
   364
val prog = Auto_Prog.gen thy' t (assoc_rls "isolate_bdv");
walther@59636
   365
val frees = vars prog; (* = [Free ("t_t", "'z"), Free ("v", "real"), Free ("v", "'a")]*)
walther@59802
   366
if length frees = 2 then () else error "test setup Auto_Prog.subst_typs changed 1";
walther@59802
   367
walther@59636
   368
val args = formal_args prog; (* = [Free ("t_t", "'z"), Free ("v", "real")]*)
walther@59636
   369
if length args = 2 then () else error "test setup Auto_Prog.subst_typs changed 2";
walther@59636
   370
walther@59636
   371
val prog' = subst_typs prog HOLogic.realT HOLogic.realT
walther@59636
   372
val frees' = vars prog'; (* = [Free ("t_t", "'z"), Free ("v", "real")]*);
walther@59636
   373
if length frees' = 2 then () else error "Auto_Prog.subst_typs changed 2"