theory scrtools

imports Isac.Build_Thydata

begin

subsection \<open> Compare with scrtools.sml: "--- test auto-generated script" \<close>

partial_function (tailrec) stepwise_test :: "real => real"

  where

"stepwise_test t_t =

  (Try (Rewrite_Set ''discard_minus'' False) @@

   Try (Rewrite_Set ''expand_poly'' False) @@      

   Try (Repeat (Calculate ''TIMES'')) @@           

   Try (Rewrite_Set ''order_mult_rls'' False) @@   

   Try (Rewrite_Set ''simplify_power'' False) @@   

   Try (Rewrite_Set ''calc_add_mult_pow'' False) @@

   Try (Rewrite_Set ''reduce_012_mult'' False) @@  

   Try (Rewrite_Set ''order_add_rls'' False) @@    

   Try (Rewrite_Set ''collect_numerals'' False) @@ 

   Try (Rewrite_Set ''reduce_012'' False) @@       

   Try (Rewrite_Set ''discard_parentheses'' False))

  t_t"

setup \<open>KEStore_Elems.add_mets

  [Specify.prep_met @{theory "Test"} "met_testinter" [] Celem.e_metID

      (["Test","test_interSteps_1"],

        [("#Given" ,["Term t_t"]), ("#Find"  ,["normalform n_n"])],

      {rew_ord' = "dummy_ord", rls' = tval_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,

        crls=tval_rls, errpats = [], nrls = Rule.e_rls},

      @{thm stepwise_test.simps}

	    (*"Program Stepwise t_t   =                        \

        \(Try (Rewrite_Set ''discard_minus'' False) @@     \

        \ Try (Rewrite_Set ''expand_poly'' False) @@       \

        \ Try (Repeat (Calculate ''TIMES'')) @@            \

        \ Try (Rewrite_Set ''order_mult_rls'' False) @@    \

        \ Try (Rewrite_Set ''simplify_power'' False) @@    \

        \ Try (Rewrite_Set ''calc_add_mult_pow'' False) @@ \

        \ Try (Rewrite_Set ''reduce_012_mult'' False) @@   \

        \ Try (Rewrite_Set ''order_add_rls'' False) @@     \

        \ Try (Rewrite_Set ''collect_numerals'' False) @@  \

        \ Try (Rewrite_Set ''reduce_012'' False) @@        \

        \ Try (Rewrite_Set ''discard_parentheses'' False)) \

        \ t_t"*)

    (*presently this script cannot become equal in types to auto_script, because:

      this t_t must be either 'real' or 'bool'  #1#, 

      while the auto_script must be 'z and type-instantiated before usage*))]

\<close>

text \<open> see scrtools.sml "--- test auto-generated script" \<close>

subsection \<open> Handle Var from parsing by partial_function \<close>

partial_function (tailrec) xxx ::

  "bool \<Rightarrow> bool list"

  where

  "xxx e_e = (let e_e = (Rewrite_Set ''yyy'' False) e_e in [e_e])"

text \<open> see scrtools.sml "--- Handle Var from parsing by partial_function" \<close>

subsection \<open> Compare program terms: from old parsing | from partial_function \<close>

partial_function (tailrec) minisubpbl ::

  "bool \<Rightarrow> real \<Rightarrow> bool list"

where "minisubpbl e_e v_v =

  (let e_e = ((Try (Rewrite_Set ''norm_equation'' False)) @@

              (Try (Rewrite_Set ''Test_simplify'' False))) e_e;

      (L_L::bool list) =

             (SubProblem (''TestX'',

                 [''LINEAR'', ''univariate'', ''equation'', ''test''],

                 [''Test'', ''solve_linear''])

               [BOOL e_e, REAL v_v])

   in Check_elementwise L_L {(v_v::real). Assumptions})"

thm "minisubpbl.simps"

ML \<open>

\<close> ML \<open>

\<close>

end