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 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)

     8                       (* these vvv test, if funs are intermediately opened in structure

     9                          in case of errors here consider ~~/xtest-to-coding.sh      *)

    10   open Kernel;

    11   open Math_Engine;

    12   open Test_Code;              CalcTreeTEST;

    13   open LItool;                 arguments_from_model;

    14   open Sub_Problem;

    15   open Fetch_Tacs;

    16   open Step

    17   open Env;

    18   open LI;                     scan_dn;

    19   open Istate;

    20   open Error_Pattern;

    21   open Error_Pattern_Def;

    22   open Specification;

    23   open Ctree;                  append_problem;

    24   open Pos;

    25   open Program;

    26   open Prog_Tac;

    27   open Tactical;

    28   open Prog_Expr;

    29   open Auto_Prog;              rule2stac;

    30   open Input_Descript;

    31   open Specify;

    32   open Specify;

    33   open Step_Specify;

    34   open Step_Solve;

    35   open Step;

    36   open Solve;                  (* NONE *)

    37   open ContextC;               transfer_asms_from_to;

    38   open Tactic;                 (* NONE *)

    39   open I_Model;

    40   open O_Model;

    41   open P_Model;                (* NONE *)

    42   open Rewrite;

    43   open Eval;                   get_pair;

    44   open TermC;                  atomt;

    45   open Rule;

    46   open Rule_Set;               Sequence;

    47   open Eval_Def

    48   open ThyC

    49   open ThmC_Def

    50   open ThmC

    51   open Rewrite_Ord

    52   open UnparseC

    53 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

    54 \<close>

    55 ML_file "BaseDefinitions/libraryC.sml"

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

    58 ML \<open>

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

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

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

    62 (*if*) (*then*); (*else*);   (*case*) (*of*);  (*return from xxx*);

    63 "xx"

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

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

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

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

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

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

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

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

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

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

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

    75 (* final test ...*)

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

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

    78 \<close> ML \<open>

    79 \<close>

    80 ML \<open>

    81 \<close> ML \<open>

    82 \<close> ML \<open>

    83 \<close>

    84 text \<open>

    85   declare [[show_types]]

    86   declare [[show_sorts]]

    87   find_theorems "?a <= ?a"

    89   print_theorems

    90   print_facts

    91   print_statement ""

    92   print_theory

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

    94   declare [[ML_print_depth = 999]]

    95   declare [[ML_exception_trace]]

    96 \<close>

    98 section \<open>=============== test prove_vc for Problem + sprak_vc (KEEP!) ======================\<close>

   100 (* requires startup with ./zcoding-to-test.sh ..*)

   101 Example \<open>~~/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>

   103 spark_open \<open>~~/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>

   104 (*..Problem adds to spark..*)

   105 Problem (*procedure_g_c_d_4*)("Biegelinie", ["Biegelinien"])

   106   Specification:

   107 (*1*)

   108     Model:

   109       Given: "Traegerlaenge ", "Streckenlast "

   110       Where: "q_0 ist_integrierbar_auf {| 0, L |}", "0 < L"

   111       Find: "Biegelinie "

   112       Relate: "Randbedingungen "

   113     References:

   114   (*2*)

   115       RTheory: ""

   116       RProblem: ["", ""]

   117       RMethod: ["", ""]

   118   (*2*)

   119 (*1*)

   120   Solution:

   122 ML \<open>

   123   (*

   124   AT ABOVE "ML" WE HAVE:

   125       Bad context for command "ML"\<^here> -- using reset state

   126   ..CAUSED BY INSUFFICIENT SEQUENCE OF SPARK keywords here in this test sequence,

   127   BUT spark_open + Problem  ABOVE SHOWS NO ERROR -- THAT IS WHAT WE WANT DURING ADAPTATION!

   128   *)

   129 \<close>

   130 (*//--------- SPARK keywords do work IF THERE IS NO spark_open ABOVE.. ----------------------\\* )

   131 (** )

   132 spark_proof_functions gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"

   133 ( **)

   135 (** )

   136 spark_open \<open>~~/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>

   137 ( ** )

   138 The following verification conditions remain to be proved:

   139   procedure_g_c_d_4

   140   procedure_g_c_d_11

   141 ( **)

   143 spark_vc procedure_g_c_d_4  (*Bad context for command "spark_vc"\<^here> -- using reset state*)

   144   sorry

   145 spark_vc procedure_g_c_d_11

   146   sorry

   147 (** )

   148 spark_end

   149 ( *Bad path binding: "$ISABELLE_HOME/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.prv"*)

   151 ( *\\--------- SPARK keywords do work IF THERE IS NO spark_open ABOVE.. ----------------------//*)

   153 subsection \<open>result Problem 1: got data from Example\<close>

   154 text \<open>

   155 trace:

   157 {a = "//--- Spark_Commands.prove_vc", o_model =

   158  [(1, [1], "#Given", Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), [Free ("L", "real")]), (2, [1], "#Given", Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), [Free ("q_0", "real")]),

   159   (3, [1], "#Find", Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("y", "real \<Rightarrow> real")]),

   160   (4, [1], "#Relate", Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"),

   161    [Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $ (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("0", "real")) $ Free ("0", "real")) $

   162       Const ("List.list.Nil", "bool list"),

   163     Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $ (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("L", "real")) $ Free ("0", "real")) $

   164       Const ("List.list.Nil", "bool list"),

   165     Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $ (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("0", "real")) $ Free ("0", "real")) $

   166       Const ("List.list.Nil", "bool list"),

   167     Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $ (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("L", "real")) $ Free ("0", "real")) $

   168       Const ("List.list.Nil", "bool list")]),

   169   (5, [1], "#undef", Const ("Biegelinie.FunktionsVariable", "real \<Rightarrow> una"), [Free ("x", "real")]),

   170   (6, [1], "#undef", Const ("Biegelinie.GleichungsVariablen", "real list \<Rightarrow> una"),

   171    [Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c", "real") $ Const ("List.list.Nil", "real list"),

   172     Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_2", "real") $ Const ("List.list.Nil", "real list"),

   173     Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_3", "real") $ Const ("List.list.Nil", "real list"),

   174     Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_4", "real") $ Const ("List.list.Nil", "real list")]),

   175   (7, [1], "#undef", Const ("Biegelinie.AbleitungBiegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("dy", "real \<Rightarrow> real")])],

   176  refs = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"])} (line 654 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")

   177 *)

   178 \<close>

   180 subsection \<open>result Problem 2: initial Specification parsed\<close>

   181 text \<open>

   182   Note: this kind of parsing is inappropriate with respect to integration:

   183   the Position.T are dropped, so no feedback can be allocated.

   185   trace:

   187 ### Private_Output.report keyword1

   188 {a = "//--- Spark_Commands.prove_vc", headline =

   189  (((((("(", "Biegelinie"), ","), ["Biegelinien"]), ")"),

   190    ((((("Specification", ":"),

   191        ((((((((((((((("Model", (("", ""), "")), ":"), "Given"), ":"), ["<markup>", "<markup>"]), "Where"), ":"),

   192                ["<markup>", "<markup>"]),

   193               "Find"),

   194              ":"),

   195             "<markup>"),

   196            "Relate"),

   197           ":"),

   198          ["<markup>"]),

   199         (("References", ":"), (((((((("RTheory", ":"), ""), "RProblem"), ":"), ["", ""]), "RMethod"), ":"), ["", ""])))),

   200       "Solution"),

   201      ":"),

   202     [])),

   203   "")} (line 677 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")

   204 {a = "prove_vc", i_model =

   205  [(0, [], false, "#Given", Inc ((Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),

   206   (0, [], false, "#Given", Inc ((Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),

   207   (0, [], false, "#Find", Inc ((Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),

   208   (0, [], false, "#Relate",

   209    Inc ((Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"), []), (Const ("empty", "??.'a"), [])))],

   210  o_model =

   211  [(1, [1], "#Given", Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), [Free ("L", "real")]),

   212   (2, [1], "#Given", Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), [Free ("q_0", "real")]),

   213   (3, [1], "#Find", Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("y", "real \<Rightarrow> real")]),

   214   (4, [1], "#Relate", Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"),

   215    [Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $

   216       (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("0", "real")) $ Free ("0", "real")) $

   217       Const ("List.list.Nil", "bool list"),

   218     Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $

   219       (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("L", "real")) $ Free ("0", "real")) $

   220       Const ("List.list.Nil", "bool list"),

   221     Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $

   222       (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("0", "real")) $

   223         Free ("0", "real")) $

   224       Const ("List.list.Nil", "bool list"),

   225     Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $

   226       (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("L", "real")) $

   227         Free ("0", "real")) $

   228       Const ("List.list.Nil", "bool list")]),

   229   (5, [1], "#undef", Const ("Biegelinie.FunktionsVariable", "real \<Rightarrow> una"), [Free ("x", "real")]),

   230   (6, [1], "#undef", Const ("Biegelinie.GleichungsVariablen", "real list \<Rightarrow> una"),

   231    [Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c", "real") $ Const ("List.list.Nil", "real list"),

   232     Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_2", "real") $ Const ("List.list.Nil", "real list"),

   233     Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_3", "real") $ Const ("List.list.Nil", "real list"),

   234     Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_4", "real") $ Const ("List.list.Nil", "real list")]),

   235   (7, [1], "#undef", Const ("Biegelinie.AbleitungBiegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("dy", "real \<Rightarrow> real")])],

   236  refs =

   237  ("Biegelinie", ["Biegelinien"],

   238   ["IntegrierenUndKonstanteBestimmen2"])} (line 690 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")

   239 ### Private_Output.report

   240 ### Syntax_Phases.check_typs

   241 :

   242 ### Syntax_Phases.check_terms

   243 :

   244 \<close>

   246 section \<open>===================================================================================\<close>

   247 ML \<open>

   248 \<close> ML \<open>

   249 \<close> ML \<open>

   250 \<close> ML \<open>

   251 \<close>

   253 section \<open>===================================================================================\<close>

   254 ML \<open>

   255 \<close> ML \<open>

   256 \<close> ML \<open>

   257 \<close> ML \<open>

   258 \<close>

   260 section \<open>===================================================================================\<close>

   261 ML \<open>

   262 \<close> ML \<open>

   263 \<close> ML \<open>

   264 \<close> ML \<open>

   265 \<close>

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

   268 ML \<open>

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

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

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

   272 (*if*) (*then*); (*else*);   (*case*) (*of*);  (*return value*);

   273 "xx"

   274 ^ "xxx"   (*+*)

   275 \<close>

   276 end

author	Walther Neuper <walther.neuper@jku.at>
	Thu, 17 Dec 2020 11:45:12 +0100
changeset 60137	12f0c14fc333
parent 60136	8ecaaee4c9bd
child 60145	d2659cf8652c
permissions	-rw-r--r--