wneuper/isa: test/Tools/isac/Test

     1 theory Test_Some

     2   imports "Isac.Build_Isac"

     3 begin

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

     6 ML \<open>

     7   open Kernel;

     8   open Math_Engine;

     9   open Test_Code;              CalcTreeTEST;

    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

    50 \<close>

    51 (*ML_file "BridgeJEdit/parseC.sml"*)

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

    54 ML \<open>

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

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

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

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

    59 "xx"

    60 ^ "xxx"   (*+*) (*+++*) (*!for return!*) (*isa*) (*REP*) (**)

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

    62 \<close> ML \<open>

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

    64 \<close> ML \<open> (*//---------------- adhoc copied up -----------------------------------------------\\*)

    65 \<close> ML \<open>

    66 \<close> ML \<open> (*\\---------------- adhoc copied up -----------------------------------------------//*)

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

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

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

    70 (*-------------------- contiue step into XXXXX ----------------------------------------------*)

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

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

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

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

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

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

    77 (* final test ...*)

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

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

    80 \<close> ML \<open>

    81 \<close>

    82 ML \<open>

    83 \<close> ML \<open>

    84 \<close> ML \<open>

    85 \<close>

    86 text \<open>

    87   declare [[show_types]]

    88   declare [[show_sorts]]

    89   find_theorems "?a <= ?a"

    91   print_theorems

    92   print_facts

    93   print_statement ""

    94   print_theory

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

    96   declare [[ML_print_depth = 999]]

    97   declare [[ML_exception_trace]]

    98 \<close>

   100 section \<open>===================================================================================\<close>

   101 ML \<open>

   102 \<close> ML \<open>

   103 \<close> ML \<open>

   104 \<close> ML \<open>

   105 \<close>

   107 section \<open>===================================================================================\<close>

   108 ML \<open>

   109 \<close> ML \<open>

   110 \<close> ML \<open>

   111 \<close> ML \<open>

   112 \<close>

   114 section \<open>===================================================================================\<close>

   115 ML \<open>

   116 \<close> ML \<open>

   117 \<close> ML \<open>

   118 \<close> ML \<open>

   119 \<close>

   121 section \<open>===================================================================================\<close>

   122 ML \<open>

   123 \<close> ML \<open>

   124 \<close> ML \<open>

   125 \<close> ML \<open>

   126 \<close>

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

   129 ML \<open>

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

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

   132 "~~~~~ from xxx to yyy return val:"; val ((*yyy*)) = ((*xxx*));

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

   134 "xx"

   135 ^ "xxx"   (*+*)

   136 \<close>

   137 end

author	wneuper <walther.neuper@jku.at>
	Tue, 03 Aug 2021 19:16:27 +0200
changeset 60347	301b4bf4655e
parent 60346	aa8a17a75749
child 60356	a14022b99b92
permissions	-rw-r--r--