Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/BridgeLibisabelle/thy-present.sml
author wneuper <walther.neuper@jku.at>
Mon, 19 Jul 2021 18:29:46 +0200
changeset 60337 cbad4e18e91b
parent 60331 40eb8aa2b0d6
child 60516 795d1352493a
permissions -rw-r--r--
cleanup after "eliminate ThmC.numerals_to_Free" 
     1 (* Title:  BridgeLibisabelle/thy-present.sml

     2    Author: Walther Neuper

     3    (c) due to copyright terms

     4 *)

     5 

     6 "--------------------------------------------------------";

     7 "--------------------------------------------------------";

     8 "table of contents --------------------------------------";

     9 "--------------------------------------------------------";

    10 "----------- fun thy_containing_rls ---------------------";

    11 "----------- apply thy_containing_rls -------------------";

    12 "----------- fun thy_containing_cal ---------------------";

    13 "----------- debugging on Tests/solve_linear_as_rootpbl -";

    14 "--------------------------------------------------------";

    15 (*============ inhibit exn WN120321 ==============================================

    16 "--------------------------------------------------------";

    17 "----------- fun filter_appl_rews -----------------------";

    18 ============ inhibit exn WN120321 ==============================================*)

    19 "----------- fun is_contained_in ------------------------";

    20 "--------------------------------------------------------";

    21 "--------------------------------------------------------";

    22 

    23 "----------- fun thy_containing_rls ---------------------";

    24 "----------- fun thy_containing_rls ---------------------";

    25 "----------- fun thy_containing_rls ---------------------";

    26 (*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"*)

    27 if Thy_Read.thy_containing_rls "Biegelinie" "norm_Poly" = ("IsacKnowledge", "Poly") then ()

    28 else error ("thy_containing_rls changed for 'Biegelinie', 'norm_Poly'")  

    29 ;

    30 "~~~~~ fun thy_containing_rls, args:"; val (thy', rls') = ("Biegelinie", "norm_Poly");

    31     val thy = ThyC.get_theory thy'; (*.., EqSystem, Isac.Biegelinie}*)

    32 val xxx = AList.lookup op= (KEStore_Elems.get_rlss thy) rls';

    33 val SOME (thy'', _) = xxx;

    34 val SOME ("Poly", _) = xxx;

    35 if thy'' = "Poly" then () else error "--- fun thy_containing_rls: changed";

    36 (*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main" *)

    37 if Thy_Read.partID' thy'' = "IsacKnowledge" then () else error "fun partID': changed"

    38 ;

    39 "~~~~~ fun partID', args:"; val (thy') = (thy');

    40 ThyC.get_theory thy' (*.., EqSystem, Isac.Biegelinie}*)

    41 ;

    42 "~~~~~ fun partID, args:"; val (thy) = (ThyC.get_theory thy');

    43 (*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"*)

    44 Thy_Read.knowthys () 

    45 ;

    46 "~~~~~ fun knowthys , args:"; val () = ();

    47         val allthys = filter_out (member Context.eq_thy

    48           [(*ThyC.get_theory "ProgLang",*) ThyC.get_theory "Interpret", 

    49             ThyC.get_theory "MathEngine", ThyC.get_theory "BridgeLibisabelle"]) 

    50           (Theory.ancestors_of (ThyC.get_theory "Build_Thydata"));

    51 length allthys = 152; (*in Isabelle2015/Isac*)

    52 (*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"

    53 ThyC.get_theory "Complex_Main";*)

    54 Thy_Info.get_theory "Complex_Main";;

    55 

    56 "----------- apply thy_containing_rls -------------------";

    57 "----------- apply thy_containing_rls -------------------";

    58 "----------- apply thy_containing_rls -------------------";

    59 if Thy_Read.thy_containing_rls "Biegelinie" "norm_Poly" = ("IsacKnowledge", "Poly") then ()

    60 else error ("Thy_Read.thy_containing_rls changed for 'Biegelinie', 'norm_Poly'")

    61 ;

    62 if Thy_Read.thy_containing_rls "Biegelinie" "empty" = ("IsacScripts", "Know_Store") then ()

    63 else error ("Thy_Read.thy_containing_rls changed for 'Biegelinie', 'e_rls'")

    64 ;

    65 if Thy_Read.thy_containing_rls "Build_Thydata" "prog_expr" = (*FIXME: handle redifinition in several thys*)

    66 (**)("IsacKnowledge", "Base_Tools")(**)

    67 (** )("IsacScripts", "Prog_Expr")( **)

    68 then () else error ("Thy_Read.thy_containing_rls changed for 'Biegelinie', 'prog_expr'")

    69 

    70 "----------- fun thy_containing_cal ---------------------";

    71 "----------- fun thy_containing_cal ---------------------";

    72 "----------- fun thy_containing_cal ---------------------";

    73 (* ATTENTION: both, "IsacKnowledge" and "Prog_Expr" are fixed as results for any input*)

    74 if Thy_Read.thy_containing_cal "Biegelinie" "PLUS" = ("IsacKnowledge", "Base_Tools")

    75 then () else error "(wrong) thy_containing_cal 'Biegelinie' 'PLUS' changed"

    76 

    77 

    78 "----------- debugging on Tests/solve_linear_as_rootpbl -";

    79 "----------- debugging on Tests/solve_linear_as_rootpbl -";

    80 "----------- debugging on Tests/solve_linear_as_rootpbl -";

    81 "----- initContext -----";

    82 reset_states ();

    83 CalcTree 

    84     [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],

    85       ("Test",

    86        ["LINEAR", "univariate", "equation", "test"],

    87        ["Test", "solve_linear"]))];

    88 Iterator 1; moveActiveRoot 1;

    89 autoCalculate 1 CompleteCalcHead;

    90 

    91 autoCalculate 1 (Steps 1); val (ptp as (pt,p), tacis) = get_calc 1; Test_Tool.show_pt pt;

    92 if is_curr_endof_calc pt ([1],Frm) then ()

    93 else error "rewtools.sml is_curr_endof_calc ([1],Frm)";

    94 

    95 autoCalculate 1 (Steps 1); val (ptp as (pt,p), tacis) = get_calc 1; Test_Tool.show_pt pt;

    96 

    97 if not (is_curr_endof_calc pt ([1],Frm)) then ()

    98 else error "rewtools.sml is_curr_endof_calc ([1],Frm) not";

    99 if is_curr_endof_calc pt ([1],Res) then ()

   100 else error "rewtools.sml is_curr_endof_calc ([1],Res)";

   101 

   102 (*//----------------- dropped with "purge code for theory-hierarchy" * )

   103 initContext 1 Ptool.Thy_ ([1],Res);

   104 

   105 "----- checkContext -----";

   106 reset_states ();

   107 CalcTree 

   108     [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],

   109       ("Test",

   110        ["LINEAR", "univariate", "equation", "test"],

   111        ["Test", "solve_linear"]))];

   112 Iterator 1; moveActiveRoot 1;

   113 autoCalculate 1 CompleteCalc;

   114 interSteps 1 ([1],Res);

   115 

   116 val (ptp as (pt,p), tacis) = get_calc 1; Test_Tool.show_pt pt;

   117 checkContext 1 ([1],Res) "thy_isac_Test-rls-Test_simplify";

   118 

   119 interSteps 1 ([2],Res);

   120 val (ptp as (pt,p), tacis) = get_calc 1; Test_Tool.show_pt pt;

   121 

   122 checkContext 1 ([2,1],Res) "thy_isac_Test-rls-Test_simplify";

   123 checkContext 1 ([2,2],Res) "thy_isac_Test-rls-Test_simplify";

   124 ( *//----------------- dropped with "purge code for theory-hierarchy" *)

   125 

   126 "----------- fun is_contained_in ------------------------";

   127 "----------- fun is_contained_in ------------------------";

   128 "----------- fun is_contained_in ------------------------";

   129 val r1 = Thm ("real_diff_minus", @{thm real_diff_minus});

   130 if Rule_Set.contains r1 Test_simplify then ()

   131 else error "rewtools.sml Rule_Set.contains Thm";

   132 

   133 val r1 = Eval (\<^const_name>\<open>plus\<close>, eval_binop "#add_");

   134 if Rule_Set.contains r1 Test_simplify then ()

   135 else error "rewtools.sml Rule_Set.contains Eval";

   136 

   137 val r1 = Eval (\<^const_name>\<open>minus\<close>, eval_binop "#add_");

   138 if not (Rule_Set.contains r1 Test_simplify) then ()

   139 else error "rewtools.sml Rule_Set.contains Eval";
wneuper/isa