wneuper/isa: test/Tools/isac/Test

     1 theory Test_Some

     2   imports "Isac.Build_Isac" "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"

     3 begin

     5 ML \<open>open ML_System\<close>

     6 ML \<open>

     7   open Kernel;

     8   open Math_Engine;

     9   open Test_Code;              Test_Code.init_calc @{context};

    10   open LItool;                 arguments_from_model;

    11   open Sub_Problem;

    12   open Fetch_Tacs;

    13   open Step

    14   open Env;

    15   open LI;                     scan_dn;

    16   open Istate;

    17   open Error_Pattern;

    18   open Error_Pattern_Def;

    19   open Specification;

    20   open Ctree;                  append_problem;

    21   open Pos;

    22   open Program;

    23   open Prog_Tac;

    24   open Tactical;

    25   open Prog_Expr;

    26   open Auto_Prog;              rule2stac;

    27   open Input_Descript;

    28   open Specify;

    29   open Specify;

    30   open Step_Specify;

    31   open Step_Solve;

    32   open Step;

    33   open Solve;                  (* NONE *)

    34   open ContextC;               transfer_asms_from_to;

    35   open Tactic;                 (* NONE *)

    36   open I_Model;

    37   open O_Model;

    38   open P_Model;                (* NONE *)

    39   open Rewrite;

    40   open Eval;                   get_pair;

    41   open TermC;                  atomt;

    42   open Rule;

    43   open Rule_Set;               Sequence;

    44   open Eval_Def

    45   open ThyC

    46   open ThmC_Def

    47   open ThmC

    48   open Rewrite_Ord

    49   open UnparseC;

    51   Know_Store.set_ref_last_thy @{theory};

    52   (*otherwise ERRORs in pbl-met-hierarchy.sml, refine.sml, evaluate.sml*)

    53 \<close>

    55 section \<open>code for copy & paste ===============================================================\<close>

    56 ML \<open>

    57 "~~~~~ fun xxx , args:"; val () = ();

    58 "~~~~~ and xxx , args:"; val () = ();

    59 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();

    60 "~~~~~ continue fun xxx"; val () = ();

    61 (*if*) (*then*); (*else*);   (*case*) (*of*);  (*return value*); (*in*) (*end*);

    62 "xx"

    63 ^ "xxx"   (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)

    64 \<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)

    65  (*//----------------- adhoc inserted n ----------------------------------------------------\\*)

    66 (*\\------------------ adhoc inserted n ----------------------------------------------------//*)

    67 \<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)

    69 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)

    70 (*//------------------ step into XXXXX -----------------------------------------------------\\*)

    71 (*keep for continuing YYYYY*)

    72 \<close> ML \<open> (*------------- continuing XXXXX ------------------------------------------------------*)

    73 (*-------------------- continuing XXXXX ------------------------------------------------------*)

    74 (*kept for continuing XXXXX*)

    75 (*-------------------- stop step into XXXXX --------------------------------------------------*)

    76 \<close> ML \<open> (*------------- stop step into XXXXX --------------------------------------------------*)

    77 (*\\------------------ step into XXXXX -----------------------------------------------------//*)

    78 \<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)

    80 (*/------------------- check entry to XXXXX -------------------------------------------------\*)

    81 (*\------------------- check entry to XXXXX -------------------------------------------------/*)

    82 (*/------------------- check within XXXXX ---------------------------------------------------\*)

    83 (*\------------------- check within XXXXX ---------------------------------------------------/*)

    84 (*/------------------- check result of XXXXX ------------------------------------------------\*)

    85 (*\------------------- check result of XXXXX ------------------------------------------------/*)

    86 (* final test ... ----------------------------------------------------------------------------*)

    88 \<close> ML \<open> (*//----------- inserted hidden code ------------------------------------------------\\*)

    89 (*//------------------ inserted hidden code ------------------------------------------------\\*)

    90 (*\\------------------ inserted hidden code ------------------------------------------------//*)

    91 \<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*)

    93 \<close> ML \<open> (*//----------- build new fun XXXXX -------------------------------------------------\\*)

    94 (*//------------------ build new fun XXXXX -------------------------------------------------\\*)

    95 (*\\------------------ build new fun XXXXX -------------------------------------------------//*)

    96 \<close> ML \<open> (*\\----------- build new fun XXXXX -------------------------------------------------//*)

    97 \<close>

    98 ML \<open>

    99 \<close> ML \<open>

   100 \<close> ML \<open>

   101 \<close>

   102 text \<open>

   103   declare [[show_types]]

   104   declare [[show_sorts]]

   105   find_theorems "?a <= ?a"

   107   print_theorems

   108   print_facts

   109   print_statement ""

   110   print_theory

   111   ML_command \<open>Pretty.writeln prt\<close>

   112   declare [[ML_print_depth = 999]]

   113   declare [[ML_exception_trace]]

   114 \<close>

   116 section \<open>===================================================================================\<close>

   117 ML \<open>

   118 \<close> ML \<open>

   119 \<close> ML \<open>

   120 \<close> ML \<open>

   121 \<close>

   123 section \<open>===================================================================================\<close>

   124 ML \<open>

   125 \<close> ML \<open>

   126 \<close> ML \<open>

   127 \<close> ML \<open>

   128 \<close>

   130 section \<open>===================================================================================\<close>

   131 ML \<open>

   132 \<close> ML \<open>

   133 \<close> ML \<open>

   134 \<close> ML \<open>

   135 \<close>

   137 section \<open>code for copy & paste ===============================================================\<close>

   138 ML \<open>

   139 "~~~~~ fun xxx , args:"; val () = ();

   140 "~~~~~ and xxx , args:"; val () = ();

   141 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();

   142 "~~~~~ continue fun xxx"; val () = ();

   143 (*if*) (*then*); (*else*);   (*case*) (*of*);  (*return value*); (*in*) (*end*);

   144 "xx"

   145 ^ "xxx"   (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)

   146 \<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)

   147  (*//----------------- adhoc inserted n ----------------------------------------------------\\*)

   148 (*\\------------------ adhoc inserted n ----------------------------------------------------//*)

   149 \<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)

   151 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)

   152 (*//------------------ step into XXXXX -----------------------------------------------------\\*)

   153 (*keep for continuing YYYYY*)

   154 \<close> ML \<open> (*------------- continuing XXXXX ------------------------------------------------------*)

   155 (*-------------------- continuing XXXXX ------------------------------------------------------*)

   156 (*kept for continuing XXXXX*)

   157 (*-------------------- stop step into XXXXX --------------------------------------------------*)

   158 \<close> ML \<open> (*------------- stop step into XXXXX --------------------------------------------------*)

   159 (*\\------------------ step into XXXXX -----------------------------------------------------//*)

   160 \<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)

   162 (*/------------------- check entry to XXXXX -------------------------------------------------\*)

   163 (*\------------------- check entry to XXXXX -------------------------------------------------/*)

   164 (*/------------------- check within XXXXX ---------------------------------------------------\*)

   165 (*\------------------- check within XXXXX ---------------------------------------------------/*)

   166 (*/------------------- check result of XXXXX ------------------------------------------------\*)

   167 (*\------------------- check result of XXXXX ------------------------------------------------/*)

   168 (* final test ... ----------------------------------------------------------------------------*)

   170 \<close> ML \<open> (*//----------- inserted hidden code ------------------------------------------------\\*)

   171 (*//------------------ inserted hidden code ------------------------------------------------\\*)

   172 (*\\------------------ inserted hidden code ------------------------------------------------//*)

   173 \<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*)

   175 \<close> ML \<open> (*//----------- build new fun XXXXX -------------------------------------------------\\*)

   176 (*//------------------ build new fun XXXXX -------------------------------------------------\\*)

   177 (*\\------------------ build new fun XXXXX -------------------------------------------------//*)

   178 \<close> ML \<open> (*\\----------- build new fun XXXXX -------------------------------------------------//*)

   179 \<close>

   180 end

author	wneuper <Walther.Neuper@jku.at>
	Wed, 11 Jan 2023 09:23:18 +0100
changeset 60649	b2ff1902420f
parent 60648	976b99bcfc96
child 60658	1c089105f581
permissions	-rw-r--r--