1.1 --- a/src/Tools/isac/BaseDefinitions/theoryC.sml Tue May 12 06:37:04 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/theoryC.sml Tue May 12 07:27:21 2020 +0200
1.3 @@ -16,10 +16,7 @@
1.4 val id_empty: id
1.5 val Isac: 'a -> theory
1.6 val parent_of: theory -> theory -> theory
1.7 -(*/------- to ThyC from Stool -------\*)
1.8 -(*val common_subthy : theory * theory -> theory*)
1.9 val sub_common : theory * theory -> theory
1.10 -(*\------- to ThyC from Stool -------/*)
1.11
1.12 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.13 (*NONE*)
1.14 @@ -51,13 +48,11 @@
1.15
1.16 fun parent_of thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1;
1.17
1.18 -(*/------- to ThyC from Stool -------\*)
1.19 fun sub_common (thy1, thy2) =
1.20 if Context.subthy (thy1, thy2) then
1.21 thy2
1.22 else if Context.subthy (thy2, thy1) then
1.23 thy1
1.24 else get_theory "Isac_Knowledge"
1.25 -(*\------- to ThyC from Stool -------/*)
1.26
1.27 (**)end(**)
2.1 --- a/src/Tools/isac/Specify/Specify.thy Tue May 12 06:37:04 2020 +0200
2.2 +++ b/src/Tools/isac/Specify/Specify.thy Tue May 12 07:27:21 2020 +0200
2.3 @@ -14,7 +14,6 @@
2.4 ML_file model.sml
2.5 ML_file "pre-conditions.sml"
2.6 ML_file refine.sml
2.7 -(*ML_file "mstools.sml" ..TODO review*)
2.8 ML_file ptyps.sml (*..TODO review*)
2.9 ML_file "test-out.sml"
2.10 ML_file "specify-step.sml"
3.1 --- a/src/Tools/isac/Specify/model.sml Tue May 12 06:37:04 2020 +0200
3.2 +++ b/src/Tools/isac/Specify/model.sml Tue May 12 07:27:21 2020 +0200
3.3 @@ -7,12 +7,10 @@
3.4
3.5 signature MODEL =
3.6 sig
3.7 -(*/------- to Model from Stool -------\*)
3.8 datatype match =
3.9 Matches of Problem.id * P_Model.item P_Model.ppc
3.10 | NoMatch of Problem.id * P_Model.item P_Model.ppc
3.11 val matchs2str : match list -> string
3.12 -(*\------- to Model from Stool -------/*)
3.13
3.14 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.15 (*NONE*)
3.16 @@ -24,17 +22,11 @@
3.17 structure Model(**) : MODEL(**) =
3.18 struct
3.19
3.20 -(*/------- to Model from Stool -------\*)
3.21 datatype match =
3.22 Matches of Problem.id * P_Model.item P_Model.ppc
3.23 | NoMatch of Problem.id * P_Model.item P_Model.ppc;
3.24 fun match2str (Matches (pI, ppc)) = "Matches (" ^ strs2str pI ^ ", " ^ P_Model.itemppc2str ppc ^ ")"
3.25 | match2str (NoMatch (pI, ppc)) = "NoMatch (" ^ strs2str pI ^ ", " ^ P_Model.itemppc2str ppc ^ ")";
3.26 fun matchs2str ms = (strs2str o (map match2str)) ms;
3.27 -(*/------- unused -------\* )
3.28 -fun pblID_of_match (Matches (pI, _)) = pI
3.29 - | pblID_of_match (NoMatch (pI, _)) = pI;
3.30 -( *\------- unused -------/*)
3.31 -(*\------- to Model from Stool -------/*)
3.32
3.33 end
4.1 --- a/src/Tools/isac/Specify/mstools.sml Tue May 12 06:37:04 2020 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,80 +0,0 @@
4.4 -(* Title: tools for 'modeling' und 'specifying' to be used in
4.5 - modspec.sml. The types are separated into this file,
4.6 - because some of them are stored in the calc-tree, and thus are required
4.7 - _before_ ctree.sml.
4.8 - TODO: allocate elements of Selem and of Stool appropriately
4.9 - Author: Walther Neuper, Mathias Lehnfeld
4.10 - (c) due to copyright terms
4.11 -*)
4.12 -
4.13 -signature SPECIFY_TOOL =
4.14 -sig
4.15 -(*/------- to Pre_Conds from Stool -------\* )
4.16 - val check_preconds : 'a -> Rule_Set.T -> term list -> I_Model.T -> Pre_Conds.T
4.17 -( *\------- to Pre_Conds from Stool -------/*)
4.18 -
4.19 -(*/------- to Model from Stool -------\* )
4.20 - datatype match =
4.21 - Matches of Problem.id * P_Model.item P_Model.ppc
4.22 - | NoMatch of Problem.id * P_Model.item P_Model.ppc
4.23 - val matchs2str : match list -> string
4.24 -( *\------- to Model from Stool -------/*)
4.25 -(*/------- to ThyC from Stool -------\* )
4.26 - val common_subthy : theory * theory -> theory
4.27 -( *\------- to ThyC from Stool -------/*)
4.28 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.29 - (*NONE*)
4.30 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.31 -(*/------- unused -------\* )
4.32 - val refined : match list -> Problem.id
4.33 -(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
4.34 - val pblID_of_match : match -> Problem.id
4.35 - val refined_IDitms : match list -> match option
4.36 -( *\------- unused -------/*)
4.37 - (*NONE*)
4.38 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.39 -
4.40 -end
4.41 -
4.42 -(**)
4.43 -structure Stool(**) : SPECIFY_TOOL(**) =
4.44 -struct
4.45 -(**)
4.46 -
4.47 -(*/------- to Model from Stool -------\* )
4.48 -datatype match =
4.49 - Matches of Problem.id * P_Model.item P_Model.ppc
4.50 -| NoMatch of Problem.id * P_Model.item P_Model.ppc;
4.51 -fun match2str (Matches (pI, ppc)) = "Matches (" ^ strs2str pI ^ ", " ^ P_Model.itemppc2str ppc ^ ")"
4.52 - | match2str (NoMatch (pI, ppc)) = "NoMatch (" ^ strs2str pI ^ ", " ^ P_Model.itemppc2str ppc ^ ")";
4.53 -fun matchs2str ms = (strs2str o (map match2str)) ms;
4.54 -(*/------- unused -------\* )
4.55 -fun pblID_of_match (Matches (pI, _)) = pI
4.56 - | pblID_of_match (NoMatch (pI, _)) = pI;
4.57 -( *\------- unused -------/*)
4.58 -( *\------- to Model from Stool -------/*)
4.59 -
4.60 -(*/------- unused -------\* )
4.61 -(* the refined pbt is the last_element Matches in the list *)
4.62 -fun is_matches (Matches _) = true
4.63 - | is_matches _ = false;
4.64 -fun matches_pblID (Matches (pI, _)) = pI
4.65 - | matches_pblID _ = raise ERROR "matches_pblID: uncovered case in fun.def.";
4.66 -fun refined ms = ((matches_pblID o the o (find_first is_matches) o rev) ms)
4.67 - handle _ => [];
4.68 -fun refined_IDitms ms = ((find_first is_matches) o rev) ms;
4.69 -( *\------- unused -------/*)
4.70 -
4.71 -(*/------- to Pre_Conds from Stool -------\* )
4.72 -fun check_preconds _(*thy*) prls pres pbl = Pre_Conds.check prls pres pbl (I_Model.max_vt pbl);
4.73 -( *\------- to Pre_Conds from Stool -------/*)
4.74 -
4.75 -
4.76 -(*/------- to ThyC from Stool -------\* )
4.77 -fun common_subthy (thy1, thy2) =
4.78 - if Context.subthy (thy1, thy2) then thy2
4.79 - else if Context.subthy (thy2, thy1) then thy1
4.80 - else ThyC.get_theory "Isac_Knowledge"
4.81 -( *\------- to ThyC from Stool -------/*)
4.82 -
4.83 -end;
5.1 --- a/src/Tools/isac/Specify/pre-conditions.sml Tue May 12 06:37:04 2020 +0200
5.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml Tue May 12 07:27:21 2020 +0200
5.3 @@ -8,12 +8,10 @@
5.4 signature PRE_CONDITIONS =
5.5 sig
5.6 type T
5.7 + val to_string : T -> string
5.8 +
5.9 val check : Rule_Set.T -> term list -> I_Model.T -> 'a -> T
5.10 - val to_string : T -> string
5.11 -(*/------- to Pre_Conds from Stool -------\*)
5.12 -(*val check_preconds : 'a -> Rule_Set.T -> term list -> I_Model.T -> T*)
5.13 val check' : 'a -> Rule_Set.T -> term list -> I_Model.T -> T
5.14 -(*\------- to Pre_Conds from Stool -------/*)
5.15
5.16 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
5.17 (*NONE*)
5.18 @@ -46,8 +44,6 @@
5.19 val pres' = map (TermC.subst_atomic_all env) pres;
5.20 in map (eval prls) pres' end;
5.21
5.22 -(*/------- to Pre_Conds from Stool -------\*)
5.23 fun check' _(*thy*) prls pres pbl = check prls pres pbl (I_Model.max_vt pbl);
5.24 -(*\------- to Pre_Conds from Stool -------/*)
5.25
5.26 (**)end(**)
6.1 --- a/test/Tools/isac/BaseDefinitions/termC.sml Tue May 12 06:37:04 2020 +0200
6.2 +++ b/test/Tools/isac/BaseDefinitions/termC.sml Tue May 12 07:27:21 2020 +0200
6.3 @@ -262,7 +262,7 @@
6.4 (*examples see
6.5 test/../Knowledge/polyeq.sml:
6.6 Where=[Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)"*)
6.7 - (*test/../Interpret/ptyps.sml:
6.8 + (*test/../Specify/refine.sml:
6.9 |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],*)
6.10 val thy = @{theory "Complex_Main"};
6.11
7.1 --- a/test/Tools/isac/Interpret/ptyps.thy Tue May 12 06:37:04 2020 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,48 +0,0 @@
7.4 -(* Title: ~~test/../Interpret/ptyps.thy
7.5 - Author: Walther Neuper
7.6 -*)
7.7 -
7.8 -theory ptyps
7.9 -imports Isac.Build_Isac
7.10 -begin
7.11 -
7.12 -text \<open>
7.13 - *setup* KEStore_Elems.add_pbts is impossible in *.sml files.
7.14 - The respective test/../ptyps.sml is called in Test_Isac.thy.
7.15 -\<close>
7.16 -
7.17 -section \<open>data for test "-ptyps.thy: store test-pbtyps by 'setup' ---"\<close>
7.18 -setup \<open>KEStore_Elems.add_pbts
7.19 -[(Specify.prep_pbt thy "pbl_test_refine" [] Problem.id_empty
7.20 - (["refine", "test"], [], Rule_Set.empty, NONE, [])),
7.21 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla" [] Problem.id_empty
7.22 - (["pbla", "refine", "test"],
7.23 - [("#Given", ["fixedValues a_a"])], Rule_Set.empty, NONE, [])),
7.24 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla1" [] Problem.id_empty
7.25 - (["pbla1","pbla", "refine", "test"],
7.26 - [("#Given", ["fixedValues a_a","maximum a_1"])], Rule_Set.empty, NONE, [])),
7.27 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla2" [] Problem.id_empty
7.28 - (["pbla2","pbla", "refine", "test"],
7.29 - [("#Given", ["fixedValues a_a","valuesFor a_2"])], Rule_Set.empty, NONE, [])),
7.30 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla2x" [] Problem.id_empty
7.31 - (["pbla2x","pbla2","pbla", "refine", "test"],
7.32 - [("#Given", ["fixedValues a_a","valuesFor a_2","functionOf a2_x"])],
7.33 - Rule_Set.empty, NONE, [])),
7.34 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla2y" [] Problem.id_empty
7.35 - (["pbla2y","pbla2","pbla", "refine", "test"],
7.36 - [("#Given" ,["fixedValues a_a","valuesFor a_2","boundVariable a2_y"])],
7.37 - Rule_Set.empty, NONE, [])),
7.38 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla2z" [] Problem.id_empty
7.39 - (["pbla2z","pbla2","pbla", "refine", "test"],
7.40 - [("#Given" ,["fixedValues a_a","valuesFor a_2","interval a2_z"])],
7.41 - Rule_Set.empty, NONE, [])),
7.42 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla3" [] Problem.id_empty
7.43 - (["pbla3","pbla", "refine", "test"],
7.44 - [("#Given" ,["fixedValues a_a","relations a_3"])],
7.45 - Rule_Set.empty, NONE, []))]
7.46 -\<close>
7.47 -
7.48 -(*ML_file "~~/test/Tools/isac/Specify/ptyps.sml" ... is called in Test_Isac.thy below,
7.49 - so do NOT call it HERE; ?circularity*)
7.50 -
7.51 -end
8.1 --- a/test/Tools/isac/Specify/ptyps.sml Tue May 12 06:37:04 2020 +0200
8.2 +++ b/test/Tools/isac/Specify/ptyps.sml Tue May 12 07:27:21 2020 +0200
8.3 @@ -6,12 +6,6 @@
8.4 "-----------------------------------------------------------------";
8.5 "table of contents -----------------------------------------------";
8.6 "-----------------------------------------------------------------";
8.7 -"-ptyps.thy: store test-pbtyps by 'setup' ------------------------";
8.8 -"----------- testdata for refin, Specify.refine_ori ----------------------";
8.9 -(*"----------- refin test-pbtyps -------requires 'setup'------------";*)
8.10 -"----------- Specify.refine_ori test-pbtyps --requires 'setup'------------";
8.11 -"----------- refine test-pbtyps ------requires 'setup'------------";
8.12 -"----------- Refine_Problem (aus subp-rooteq.sml) ----------------";
8.13 "----------- fun coll_guhs ---------------------------------------";
8.14 "----------- fun guh2kestoreID -----------------------------------";
8.15 "----------- fun mark --------------------------------------------";
8.16 @@ -26,396 +20,6 @@
8.17 "-----------------------------------------------------------------";
8.18 "-----------------------------------------------------------------";
8.19
8.20 -"----------- testdata for refin, Specify.refine_ori ----------------------";
8.21 -"----------- testdata for refin, Specify.refine_ori ----------------------";
8.22 -"----------- testdata for refin, Specify.refine_ori ----------------------";
8.23 -Specify.show_ptyps();
8.24 -val thy = @{theory "Isac_Knowledge"};
8.25 -val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"};
8.26 -
8.27 -(*case 1: no refinement *)
8.28 -val (d1,ts1) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "fixedValues [aaa = 0]");
8.29 -val (d2,ts2) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "errorBound (ddd = 0)");
8.30 -val ori1 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]: O_Model.T;
8.31 -
8.32 -(*case 2: refined to pbt without children *)
8.33 -val (d2,ts2) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "relations [aaa333]");
8.34 -val ori2 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:O_Model.T;
8.35 -
8.36 -(*case 3: refined to pbt with children *)
8.37 -val (d2,ts2) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "valuesFor [aaa222]");
8.38 -val ori3 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:O_Model.T;
8.39 -
8.40 -(*case 4: refined to children (without child)*)
8.41 -val (d3,ts3) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "boundVariable aaa222yyy");
8.42 -val ori4 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2), (3,[1],"#Given",d3,ts3)]:O_Model.T;
8.43 -
8.44 -(*=================================================================
8.45 -This test expects pbls at a certain position in the tree.
8.46 -Since parallel evaluation (i.e. Theory_Data) this cannot be expected.
8.47 -Solutions would be
8.48 -* provide an access function for a branch (not only leaves)
8.49 -* sort the tree of pbls.
8.50 -"----------- refin test-pbtyps -----------------------------------";
8.51 -"----------- refin test-pbtyps -----------------------------------";
8.52 -"----------- refin test-pbtyps -----------------------------------";
8.53 -(* fragile test setup: expects ptyps as fixed *)
8.54 -val level_1 = case nth 9 (get_ptyps ()) of
8.55 -Store.Node ("test", _, level_1) => level_1 | _ => error "refin broken: root-branch in ptyps changed?"
8.56 -val level_2 = case nth 4 level_1 of
8.57 -Store.Node ("refine", _, level_2) => level_2 | _ => error "refin broken: lev1-branch in ptyps changed?"
8.58 -val pbla_branch = case level_2 of
8.59 -[Store.Node ("pbla", _, _)] => level_2 | _ => error "refin broken: lev2-branch in ptyps changed?";
8.60 -
8.61 -(*case 1: no refinement *)
8.62 -case refin [] ori1 (hd pbla_branch) of
8.63 - SOME ["pbla"] => () | _ => error "refin case 1 broken";
8.64 -
8.65 -(*case 2: refined to pbt without children *)
8.66 -case refin [] ori2 (hd pbla_branch) of
8.67 - SOME ["pbla", "pbla3"] => () | _ => error "refin case 2 broken";
8.68 -
8.69 -(*case 3: refined to pbt with children *)
8.70 -case refin [] ori3 (hd pbla_branch) of
8.71 - SOME ["pbla", "pbla2"] => () | _ => error "refin case 3 broken";
8.72 -
8.73 -(*case 4: refined to children (without child)*)
8.74 -case refin [] ori4 (hd pbla_branch) of
8.75 - SOME ["pbla", "pbla2", "pbla2y"] => () | _ => error "refin case 4 broken";
8.76 -
8.77 -(*case 5: start refinement somewhere in ptyps*)
8.78 -val [Store.Node ("pbla",_,[_, ppp as Store.Node ("pbla2",_,_), _])] = pbla_branch;
8.79 -case refin ["pbla"] ori4 ppp of
8.80 - SOME ["pbla", "pbla2", "pbla2y"] => () | _ => error "refin case 5 broken";
8.81 -==================================================================*)
8.82 -
8.83 -"----------- Specify.refine_ori test-pbtyps ------------------------------";
8.84 -"----------- Specify.refine_ori test-pbtyps ------------------------------";
8.85 -"----------- Specify.refine_ori test-pbtyps ------------------------------";
8.86 -(*case 1: no refinement *)
8.87 -case Specify.refine_ori ori1 ["pbla", "refine", "test"] of
8.88 - NONE => () | _ => error "Specify.refine_ori case 1 broken";
8.89 -
8.90 -(*case 2: refined to pbt without children *)
8.91 -case Specify.refine_ori ori2 ["pbla", "refine", "test"] of
8.92 - SOME ["pbla3", "pbla", "refine", "test"] => () | _ => error "Specify.refine_ori case 2 broken";
8.93 -
8.94 -(*case 3: refined to pbt with children *)
8.95 -case Specify.refine_ori ori3 ["pbla", "refine", "test"] of
8.96 - SOME ["pbla2", "pbla", "refine", "test"] => () | _ => error "Specify.refine_ori case 3 broken";
8.97 -
8.98 -(*case 4: refined to children (without child)*)
8.99 -case Specify.refine_ori ori4 ["pbla", "refine", "test"] of
8.100 - SOME ["pbla2y","pbla2","pbla", "refine", "test"] => () | _ => error "Specify.refine_ori case 4 broken";
8.101 -
8.102 -(*case 5: start refinement somewhere in ptyps*)
8.103 -case Specify.refine_ori ori4 ["pbla2","pbla", "refine", "test"] of
8.104 - SOME ["pbla2y", "pbla2", "pbla", "refine", "test"] => () | _ => error "Specify.refine_ori case 5 broken";
8.105 -
8.106 -"----------- refine test-pbtyps ----------------------------------";
8.107 -"----------- refine test-pbtyps ----------------------------------";
8.108 -"----------- refine test-pbtyps ----------------------------------";
8.109 -val fmz1 = ["fixedValues [aaa=0]","errorBound (ddd=0)"];
8.110 -val fmz2 = ["fixedValues [aaa=0]","relations aaa333"];
8.111 -val fmz3 = ["fixedValues [aaa=0]","valuesFor [aaa222]"];
8.112 -val fmz4 = ["fixedValues [aaa=0]","valuesFor [aaa222]",
8.113 - "boundVariable aaa222yyy"];
8.114 -
8.115 -(*case 1: no refinement *)
8.116 -case Specify.refine fmz1 ["pbla", "refine", "test"] of
8.117 - [Model.Matches (["pbla", "refine", "test"], _),
8.118 - Model.NoMatch (["pbla1", "pbla", "refine", "test"], _),
8.119 - Model.NoMatch (["pbla2", "pbla", "refine", "test"], _),
8.120 - Model.NoMatch (["pbla3", "pbla", "refine", "test"], _)] => ()
8.121 - | _ => error "--- Specify.refine test-pbtyps --- broken with case 1";
8.122 -(*
8.123 -*** pass ["pbla"]
8.124 -*** pass ["pbla","pbla1"]
8.125 -*** pass ["pbla","pbla2"]
8.126 -*** pass ["pbla","pbla3"]
8.127 -val it =
8.128 - [Model.Matches
8.129 - (["pbla"],
8.130 - {Find=[],
8.131 - Given=[Correct "fixedValues [aaa = #0]",
8.132 - Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),
8.133 - Model.NoMatch
8.134 - (["pbla1","pbla"],
8.135 - {Find=[],
8.136 - Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
8.137 - Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),
8.138 - Model.NoMatch
8.139 - (["pbla2","pbla"],
8.140 - {Find=[],
8.141 - Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_",
8.142 - Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),
8.143 - Model.NoMatch
8.144 - (["pbla3","pbla"],
8.145 - {Find=[],
8.146 - Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_",
8.147 - Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]})]
8.148 - : match list*)
8.149 -
8.150 -(*case 2: refined to pbt without children *)
8.151 -case Specify.refine fmz2 ["pbla", "refine", "test"] of
8.152 - [Model.Matches (["pbla", "refine", "test"], _),
8.153 - Model.NoMatch (["pbla1", "pbla", "refine", "test"], _),
8.154 - Model.NoMatch (["pbla2", "pbla", "refine", "test"], _),
8.155 - Model.Matches (["pbla3", "pbla", "refine", "test"], _)] => ()
8.156 - | _ => error "--- Specify.refine test-pbtyps --- broken with case 2";
8.157 -(*
8.158 -*** pass ["pbla"]
8.159 -*** pass ["pbla","pbla1"]
8.160 -*** pass ["pbla","pbla2"]
8.161 -*** pass ["pbla","pbla3"]
8.162 -val it =
8.163 - [Model.Matches
8.164 - (["pbla"],
8.165 - {Find=[],
8.166 - Given=[Correct "fixedValues [aaa = #0]",Superfl "relations aaa333"],
8.167 - Relate=[],Where=[],With=[]}),
8.168 - Model.NoMatch
8.169 - (["pbla1","pbla"],
8.170 - {Find=[],
8.171 - Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
8.172 - Superfl "relations aaa333"],Relate=[],Where=[],With=[]}),
8.173 - Model.NoMatch
8.174 - (["pbla2","pbla"],
8.175 - {Find=[],
8.176 - Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_",
8.177 - Superfl "relations aaa333"],Relate=[],Where=[],With=[]}),
8.178 - Model.Matches
8.179 - (["pbla3","pbla"],
8.180 - {Find=[],
8.181 - Given=[Correct "fixedValues [aaa = #0]",Correct "relations aaa333"],
8.182 - Relate=[],Where=[],With=[]})] : match list*)
8.183 -
8.184 -(*case 3: refined to pbt with children *)
8.185 -case Specify.refine fmz3 ["pbla", "refine", "test"] of
8.186 - [Model.Matches (["pbla", "refine", "test"], _),
8.187 - Model.NoMatch (["pbla1", "pbla", "refine", "test"], _),
8.188 - Model.Matches (["pbla2", "pbla", "refine", "test"], _),
8.189 - Model.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _),
8.190 - Model.NoMatch (["pbla2y", "pbla2", "pbla", "refine", "test"], _),
8.191 - Model.NoMatch (["pbla2z", "pbla2", "pbla", "refine", "test"], _),
8.192 - Model.NoMatch (["pbla3", "pbla", "refine", "test"], _)] => ()
8.193 - | _ => error "--- Specify.refine test-pbtyps --- broken with case 3";
8.194 -(*
8.195 -*** pass ["pbla"]
8.196 -*** pass ["pbla","pbla1"]
8.197 -*** pass ["pbla","pbla2"]
8.198 -*** pass ["pbla","pbla2","pbla2x"]
8.199 -*** pass ["pbla","pbla2","pbla2y"]
8.200 -*** pass ["pbla","pbla2","pbla2z"]
8.201 -*** pass ["pbla","pbla3"]
8.202 -val it =
8.203 - [Model.Matches
8.204 - (["pbla"],
8.205 - {Find=[],
8.206 - Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222"],
8.207 - Relate=[],Where=[],With=[]}),
8.208 - Model.NoMatch
8.209 - (["pbla1","pbla"],
8.210 - {Find=[],
8.211 - Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
8.212 - Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]}),
8.213 - Model.Matches
8.214 - (["pbla2","pbla"],
8.215 - {Find=[],
8.216 - Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222"],
8.217 - Relate=[],Where=[],With=[]}),
8.218 - Model.NoMatch
8.219 - (["pbla2x","pbla2","pbla"],
8.220 - {Find=[],
8.221 - Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
8.222 - Missing "functionOf a2x_"],Relate=[],Where=[],With=[]}),
8.223 - Model.NoMatch
8.224 - (["pbla2y","pbla2","pbla"],
8.225 - {Find=[],
8.226 - Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
8.227 - Missing "boundVariable a2y_"],Relate=[],Where=[],With=[]}),
8.228 - Model.NoMatch
8.229 - (["pbla2z","pbla2","pbla"],
8.230 - {Find=[],
8.231 - Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
8.232 - Missing "interval a2z_"],Relate=[],Where=[],With=[]}),
8.233 - Model.NoMatch
8.234 - (["pbla3","pbla"],
8.235 - {Find=[],
8.236 - Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_",
8.237 - Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]})]
8.238 - : match list*)
8.239 -
8.240 -(*case 4: refined to children (without child)*)
8.241 -case Specify.refine fmz4 ["pbla", "refine", "test"] of
8.242 - [Model.Matches (["pbla", "refine", "test"], _),
8.243 - Model.NoMatch (["pbla1", "pbla", "refine", "test"], _),
8.244 - Model.Matches (["pbla2", "pbla", "refine", "test"], _),
8.245 - Model.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _),
8.246 - Model.Matches (["pbla2y", "pbla2", "pbla", "refine", "test"], _)] => ()
8.247 - | _ => error "--- Specify.refine test-pbtyps --- broken with case 4";
8.248 -(*
8.249 -*** pass ["pbla"]
8.250 -*** pass ["pbla","pbla1"]
8.251 -*** pass ["pbla","pbla2"]
8.252 -*** pass ["pbla","pbla2","pbla2x"]
8.253 -*** pass ["pbla","pbla2","pbla2y"]
8.254 -val it =
8.255 - [Model.Matches
8.256 - (["pbla"],
8.257 - {Find=[],
8.258 - Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222",
8.259 - Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),
8.260 - Model.NoMatch
8.261 - (["pbla1","pbla"],
8.262 - {Find=[],
8.263 - Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
8.264 - Superfl "valuesFor aaa222",Superfl "boundVariable aaa222yyy"],
8.265 - Relate=[],Where=[],With=[]}),
8.266 - Model.Matches
8.267 - (["pbla2","pbla"],
8.268 - {Find=[],
8.269 - Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
8.270 - Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),
8.271 - Model.NoMatch
8.272 - (["pbla2x","pbla2","pbla"],
8.273 - {Find=[],
8.274 - Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
8.275 - Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"],
8.276 - Relate=[],Where=[],With=[]}),
8.277 - Model.Matches
8.278 - (["pbla2y","pbla2","pbla"],
8.279 - {Find=[],
8.280 - Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
8.281 - Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})]
8.282 - : match list*)
8.283 -
8.284 -(*case 5: start refinement somewhere in ptyps*)
8.285 -case Specify.refine fmz4 ["pbla2","pbla", "refine", "test"] of
8.286 - [Model.Matches (["pbla2", "pbla", "refine", "test"], _),
8.287 - Model.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _),
8.288 - Model.Matches (["pbla2y", "pbla2", "pbla", "refine", "test"], _)] => ()
8.289 - | _ => error "--- Specify.refine test-pbtyps --- broken with case 5";
8.290 -(*
8.291 -*** pass ["pbla","pbla2"]
8.292 -*** pass ["pbla","pbla2","pbla2x"]
8.293 -*** pass ["pbla","pbla2","pbla2y"]
8.294 -val it =
8.295 - [Model.Matches
8.296 - (["pbla2","pbla"],
8.297 - {Find=[],
8.298 - Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
8.299 - Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),
8.300 - Model.NoMatch
8.301 - (["pbla2x","pbla2","pbla"],
8.302 - {Find=[],
8.303 - Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
8.304 - Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"],
8.305 - Relate=[],Where=[],With=[]}),
8.306 - Model.Matches
8.307 - (["pbla2y","pbla2","pbla"],
8.308 - {Find=[],
8.309 - Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
8.310 - Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})]
8.311 - : match list*)
8.312 -
8.313 -"----------- Refine_Problem (aus subp-rooteq.sml) ----------------";
8.314 -"----------- Refine_Problem (aus subp-rooteq.sml) ----------------";
8.315 -"----------- Refine_Problem (aus subp-rooteq.sml) ----------------";
8.316 -val c = [];
8.317 -val fmz = ["equality ((x+1)*(x+2)=x^^^2+(8::real))","solveFor x",
8.318 - "errorBound (eps=0)","solutions L"];
8.319 -val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
8.320 - ["Test","squ-equ-test-subpbl1"]);
8.321 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.CalcTreeTEST [(fmz, (dI',pI',mI'))];
8.322 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.323 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.324 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "solutions L"*)
8.325 -
8.326 -(*=== specify a not-matching problem ---vvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
8.327 -val nxt = (Specify_Problem ["LINEAR","univariate","equation","test"]);
8.328 -(*=== specify a not-matching problem ---^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
8.329 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "solutions L"*)
8.330 -
8.331 -val www =
8.332 -case f of Test_Out.PpcKF (Test_Out.Problem [],
8.333 - {Find = [Incompl "solutions []"], With = [],
8.334 - Given = [Correct "equality ((x + 1) * (x + 2) = x ^^^ 2 + 8)", Correct "solveFor x"],
8.335 - Where = [False www(*! ! ! ! ! !*)],
8.336 - Relate = [],...}) => www(*! ! !*)
8.337 -| _ => error "--- Refine_Problem broken 1";
8.338 -if www = "matches (x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\nmatches (?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\nmatches (?a + x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\nmatches (?a + ?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8)"
8.339 -then () else error "--- Refine_Problem broken 2";
8.340 -(*ML> f;
8.341 -val it = Form' (Test_Out.PpcKF (0,EdUndef,0,Nundef,
8.342 - (Problem ["LINEAR","univariate","equation","test"], <<<<<===== diff.to above WN120313
8.343 - {Find=[Incompl "solutions []"],
8.344 - Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
8.345 - Correct "solveFor x"],Relate=[],
8.346 - Where=[False "matches (x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)
8.347 - |\nmatches (?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)
8.348 - |\nmatches (?a + x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)
8.349 - |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
8.350 - With=[]}))) : mout
8.351 -*)
8.352 -
8.353 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = (me nxt p c pt) (*Empty_Tac ?!?*);
8.354 -
8.355 -(*=== refine problem -----vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
8.356 -val nxt = (Refine_Problem ["univariate","equation","test"]);
8.357 -(*=== refine problem -----^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
8.358 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.359 -(*("Specify_Problem", Specify_Problem ["normalise", "univariate", ...])*)
8.360 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.361 -(*nxt = ("Specify_Theory", Specify_Theory "Test")*)
8.362 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.363 -(*nxt = ("Specify_Method", Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
8.364 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.365 -(*nxt = ("Apply_Method", *)
8.366 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.367 -(*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
8.368 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.369 -(*nxt = ("Rewrite_Set", Rewrite_Set "Test_simplify")*)
8.370 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.371 -(*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]*)
8.372 -
8.373 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.374 -(*nxt = Model_Problem ["LINEAR","univariate","equation","test"]*)
8.375 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.376 -(*nxt = ("Add_Given", Add_Given "equality (-6 + 3 * x = 0)"*)
8.377 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.378 -(**)
8.379 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.380 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.381 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.382 -(*nxt = Specify_Problem ["LINEAR","univariate","equation","test"])*)
8.383 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.384 -(*xt = ("Specify_Method", Specify_Method ["Test", "solve_linear"])*)
8.385 -val nxt = (Refine_Problem ["univariate","equation","test"]);
8.386 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.387 -(*("Specify_Problem", Specify_Problem ["LINEAR", "univariate", ...])*)
8.388 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.389 -(*val nxt = ("Specify_Method",Specify_Method ("Test","solve_linear"))*)
8.390 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.391 -(*val nxt = ("Apply_Method",Apply_Method ("Test","solve_linear"))*)
8.392 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.393 -(*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)
8.394 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.395 -(*val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify")*)
8.396 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.397 -(*val nxt = ("Check_Postcond",Check_Postcond ["LINEAR","univariate","eq*)
8.398 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.399 -(*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
8.400 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.401 -(*Check_Postcond ["normalise","univariate","equation","test"])*)
8.402 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.403 -val Test_Out.FormKF res = f;
8.404 -
8.405 -if res = "[x = 2]"
8.406 -then case nxt of End_Proof' => ()
8.407 - | _ => error "new behaviour in test:refine.sml:miniscript with mini-subpb 1"
8.408 -else error "new behaviour in test:refine.sml:miniscript with mini-subpb 2"
8.409 -
8.410 "----------- fun coll_guhs ---------------------------------------";
8.411 "----------- fun coll_guhs ---------------------------------------";
8.412 "----------- fun coll_guhs ---------------------------------------";
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/test/Tools/isac/Specify/refine.sml Tue May 12 07:27:21 2020 +0200
9.3 @@ -0,0 +1,412 @@
9.4 +(* Title: "Specify/refine.sml"
9.5 + Author: Walther Neuper
9.6 + (c) due to copyright terms
9.7 +*)
9.8 +
9.9 +"-----------------------------------------------------------------------------------------------";
9.10 +"table of contents -----------------------------------------------------------------------------";
9.11 +"-----------------------------------------------------------------------------------------------";
9.12 +"refine.thy: store test-pbtyps by 'setup' ------------------------------------------------------";
9.13 +"----------- testdata for refin, Specify.refine_ori --------------------------------------------";
9.14 +(*"----------- refin test-pbtyps -------requires specific 'setup'-------------------------------";*)
9.15 +"----------- Specify.refine_ori test-pbtyps --requires 'setup'----------------------------------";
9.16 +"----------- refine test-pbtyps ------requires 'setup'------------------------------------------";
9.17 +"----------- Refine_Problem (aus subp-rooteq.sml) ----------------------------------------------";
9.18 +"-----------------------------------------------------------------------------------------------";
9.19 +"-----------------------------------------------------------------------------------------------";
9.20 +"-----------------------------------------------------------------------------------------------";
9.21 +
9.22 +
9.23 +"----------- testdata for refin, Specify.refine_ori --------------------------------------------";
9.24 +"----------- testdata for refin, Specify.refine_ori --------------------------------------------";
9.25 +"----------- testdata for refin, Specify.refine_ori --------------------------------------------";
9.26 +Specify.show_ptyps();
9.27 +val thy = @{theory "Isac_Knowledge"};
9.28 +val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"};
9.29 +
9.30 +(*case 1: no refinement *)
9.31 +val (d1,ts1) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "fixedValues [aaa = 0]");
9.32 +val (d2,ts2) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "errorBound (ddd = 0)");
9.33 +val ori1 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]: O_Model.T;
9.34 +
9.35 +(*case 2: refined to pbt without children *)
9.36 +val (d2,ts2) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "relations [aaa333]");
9.37 +val ori2 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:O_Model.T;
9.38 +
9.39 +(*case 3: refined to pbt with children *)
9.40 +val (d2,ts2) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "valuesFor [aaa222]");
9.41 +val ori3 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:O_Model.T;
9.42 +
9.43 +(*case 4: refined to children (without child)*)
9.44 +val (d3,ts3) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "boundVariable aaa222yyy");
9.45 +val ori4 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2), (3,[1],"#Given",d3,ts3)]:O_Model.T;
9.46 +
9.47 +(*=================================================================
9.48 +This test expects pbls at a certain position in the tree.
9.49 +Since parallel evaluation (i.e. Theory_Data) this cannot be expected.
9.50 +Solutions would be
9.51 +* provide an access function for a branch (not only leaves)
9.52 +* sort the tree of pbls.
9.53 +"----------- refin test-pbtyps -------requires specific 'setup'-------------------------------";
9.54 +"----------- refin test-pbtyps -------requires specific 'setup'-------------------------------";
9.55 +"----------- refin test-pbtyps -------requires specific 'setup'-------------------------------";
9.56 +(* fragile test setup: expects ptyps as fixed *)
9.57 +val level_1 = case nth 9 (get_ptyps ()) of
9.58 +Store.Node ("test", _, level_1) => level_1 | _ => error "refin broken: root-branch in ptyps changed?"
9.59 +val level_2 = case nth 4 level_1 of
9.60 +Store.Node ("refine", _, level_2) => level_2 | _ => error "refin broken: lev1-branch in ptyps changed?"
9.61 +val pbla_branch = case level_2 of
9.62 +[Store.Node ("pbla", _, _)] => level_2 | _ => error "refin broken: lev2-branch in ptyps changed?";
9.63 +
9.64 +(*case 1: no refinement *)
9.65 +case refin [] ori1 (hd pbla_branch) of
9.66 + SOME ["pbla"] => () | _ => error "refin case 1 broken";
9.67 +
9.68 +(*case 2: refined to pbt without children *)
9.69 +case refin [] ori2 (hd pbla_branch) of
9.70 + SOME ["pbla", "pbla3"] => () | _ => error "refin case 2 broken";
9.71 +
9.72 +(*case 3: refined to pbt with children *)
9.73 +case refin [] ori3 (hd pbla_branch) of
9.74 + SOME ["pbla", "pbla2"] => () | _ => error "refin case 3 broken";
9.75 +
9.76 +(*case 4: refined to children (without child)*)
9.77 +case refin [] ori4 (hd pbla_branch) of
9.78 + SOME ["pbla", "pbla2", "pbla2y"] => () | _ => error "refin case 4 broken";
9.79 +
9.80 +(*case 5: start refinement somewhere in ptyps*)
9.81 +val [Store.Node ("pbla",_,[_, ppp as Store.Node ("pbla2",_,_), _])] = pbla_branch;
9.82 +case refin ["pbla"] ori4 ppp of
9.83 + SOME ["pbla", "pbla2", "pbla2y"] => () | _ => error "refin case 5 broken";
9.84 +==================================================================*)
9.85 +
9.86 +
9.87 +"----------- Specify.refine_ori test-pbtyps --requires 'setup'----------------------------------";
9.88 +"----------- Specify.refine_ori test-pbtyps --requires 'setup'----------------------------------";
9.89 +"----------- Specify.refine_ori test-pbtyps --requires 'setup'----------------------------------";
9.90 +(*case 1: no refinement *)
9.91 +case Specify.refine_ori ori1 ["pbla", "refine", "test"] of
9.92 + NONE => () | _ => error "Specify.refine_ori case 1 broken";
9.93 +
9.94 +(*case 2: refined to pbt without children *)
9.95 +case Specify.refine_ori ori2 ["pbla", "refine", "test"] of
9.96 + SOME ["pbla3", "pbla", "refine", "test"] => () | _ => error "Specify.refine_ori case 2 broken";
9.97 +
9.98 +(*case 3: refined to pbt with children *)
9.99 +case Specify.refine_ori ori3 ["pbla", "refine", "test"] of
9.100 + SOME ["pbla2", "pbla", "refine", "test"] => () | _ => error "Specify.refine_ori case 3 broken";
9.101 +
9.102 +(*case 4: refined to children (without child)*)
9.103 +case Specify.refine_ori ori4 ["pbla", "refine", "test"] of
9.104 + SOME ["pbla2y","pbla2","pbla", "refine", "test"] => () | _ => error "Specify.refine_ori case 4 broken";
9.105 +
9.106 +(*case 5: start refinement somewhere in ptyps*)
9.107 +case Specify.refine_ori ori4 ["pbla2","pbla", "refine", "test"] of
9.108 + SOME ["pbla2y", "pbla2", "pbla", "refine", "test"] => () | _ => error "Specify.refine_ori case 5 broken";
9.109 +
9.110 +
9.111 +"----------- refine test-pbtyps ------requires 'setup'------------------------------------------";
9.112 +"----------- refine test-pbtyps ------requires 'setup'------------------------------------------";
9.113 +"----------- refine test-pbtyps ------requires 'setup'------------------------------------------";
9.114 +val fmz1 = ["fixedValues [aaa=0]","errorBound (ddd=0)"];
9.115 +val fmz2 = ["fixedValues [aaa=0]","relations aaa333"];
9.116 +val fmz3 = ["fixedValues [aaa=0]","valuesFor [aaa222]"];
9.117 +val fmz4 = ["fixedValues [aaa=0]","valuesFor [aaa222]",
9.118 + "boundVariable aaa222yyy"];
9.119 +
9.120 +(*case 1: no refinement *)
9.121 +case Specify.refine fmz1 ["pbla", "refine", "test"] of
9.122 + [Model.Matches (["pbla", "refine", "test"], _),
9.123 + Model.NoMatch (["pbla1", "pbla", "refine", "test"], _),
9.124 + Model.NoMatch (["pbla2", "pbla", "refine", "test"], _),
9.125 + Model.NoMatch (["pbla3", "pbla", "refine", "test"], _)] => ()
9.126 + | _ => error "--- Specify.refine test-pbtyps --- broken with case 1";
9.127 +(*
9.128 +*** pass ["pbla"]
9.129 +*** pass ["pbla","pbla1"]
9.130 +*** pass ["pbla","pbla2"]
9.131 +*** pass ["pbla","pbla3"]
9.132 +val it =
9.133 + [Model.Matches
9.134 + (["pbla"],
9.135 + {Find=[],
9.136 + Given=[Correct "fixedValues [aaa = #0]",
9.137 + Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),
9.138 + Model.NoMatch
9.139 + (["pbla1","pbla"],
9.140 + {Find=[],
9.141 + Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
9.142 + Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),
9.143 + Model.NoMatch
9.144 + (["pbla2","pbla"],
9.145 + {Find=[],
9.146 + Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_",
9.147 + Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),
9.148 + Model.NoMatch
9.149 + (["pbla3","pbla"],
9.150 + {Find=[],
9.151 + Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_",
9.152 + Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]})]
9.153 + : match list*)
9.154 +
9.155 +(*case 2: refined to pbt without children *)
9.156 +case Specify.refine fmz2 ["pbla", "refine", "test"] of
9.157 + [Model.Matches (["pbla", "refine", "test"], _),
9.158 + Model.NoMatch (["pbla1", "pbla", "refine", "test"], _),
9.159 + Model.NoMatch (["pbla2", "pbla", "refine", "test"], _),
9.160 + Model.Matches (["pbla3", "pbla", "refine", "test"], _)] => ()
9.161 + | _ => error "--- Specify.refine test-pbtyps --- broken with case 2";
9.162 +(*
9.163 +*** pass ["pbla"]
9.164 +*** pass ["pbla","pbla1"]
9.165 +*** pass ["pbla","pbla2"]
9.166 +*** pass ["pbla","pbla3"]
9.167 +val it =
9.168 + [Model.Matches
9.169 + (["pbla"],
9.170 + {Find=[],
9.171 + Given=[Correct "fixedValues [aaa = #0]",Superfl "relations aaa333"],
9.172 + Relate=[],Where=[],With=[]}),
9.173 + Model.NoMatch
9.174 + (["pbla1","pbla"],
9.175 + {Find=[],
9.176 + Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
9.177 + Superfl "relations aaa333"],Relate=[],Where=[],With=[]}),
9.178 + Model.NoMatch
9.179 + (["pbla2","pbla"],
9.180 + {Find=[],
9.181 + Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_",
9.182 + Superfl "relations aaa333"],Relate=[],Where=[],With=[]}),
9.183 + Model.Matches
9.184 + (["pbla3","pbla"],
9.185 + {Find=[],
9.186 + Given=[Correct "fixedValues [aaa = #0]",Correct "relations aaa333"],
9.187 + Relate=[],Where=[],With=[]})] : match list*)
9.188 +
9.189 +(*case 3: refined to pbt with children *)
9.190 +case Specify.refine fmz3 ["pbla", "refine", "test"] of
9.191 + [Model.Matches (["pbla", "refine", "test"], _),
9.192 + Model.NoMatch (["pbla1", "pbla", "refine", "test"], _),
9.193 + Model.Matches (["pbla2", "pbla", "refine", "test"], _),
9.194 + Model.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _),
9.195 + Model.NoMatch (["pbla2y", "pbla2", "pbla", "refine", "test"], _),
9.196 + Model.NoMatch (["pbla2z", "pbla2", "pbla", "refine", "test"], _),
9.197 + Model.NoMatch (["pbla3", "pbla", "refine", "test"], _)] => ()
9.198 + | _ => error "--- Specify.refine test-pbtyps --- broken with case 3";
9.199 +(*
9.200 +*** pass ["pbla"]
9.201 +*** pass ["pbla","pbla1"]
9.202 +*** pass ["pbla","pbla2"]
9.203 +*** pass ["pbla","pbla2","pbla2x"]
9.204 +*** pass ["pbla","pbla2","pbla2y"]
9.205 +*** pass ["pbla","pbla2","pbla2z"]
9.206 +*** pass ["pbla","pbla3"]
9.207 +val it =
9.208 + [Model.Matches
9.209 + (["pbla"],
9.210 + {Find=[],
9.211 + Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222"],
9.212 + Relate=[],Where=[],With=[]}),
9.213 + Model.NoMatch
9.214 + (["pbla1","pbla"],
9.215 + {Find=[],
9.216 + Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
9.217 + Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]}),
9.218 + Model.Matches
9.219 + (["pbla2","pbla"],
9.220 + {Find=[],
9.221 + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222"],
9.222 + Relate=[],Where=[],With=[]}),
9.223 + Model.NoMatch
9.224 + (["pbla2x","pbla2","pbla"],
9.225 + {Find=[],
9.226 + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
9.227 + Missing "functionOf a2x_"],Relate=[],Where=[],With=[]}),
9.228 + Model.NoMatch
9.229 + (["pbla2y","pbla2","pbla"],
9.230 + {Find=[],
9.231 + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
9.232 + Missing "boundVariable a2y_"],Relate=[],Where=[],With=[]}),
9.233 + Model.NoMatch
9.234 + (["pbla2z","pbla2","pbla"],
9.235 + {Find=[],
9.236 + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
9.237 + Missing "interval a2z_"],Relate=[],Where=[],With=[]}),
9.238 + Model.NoMatch
9.239 + (["pbla3","pbla"],
9.240 + {Find=[],
9.241 + Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_",
9.242 + Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]})]
9.243 + : match list*)
9.244 +
9.245 +(*case 4: refined to children (without child)*)
9.246 +case Specify.refine fmz4 ["pbla", "refine", "test"] of
9.247 + [Model.Matches (["pbla", "refine", "test"], _),
9.248 + Model.NoMatch (["pbla1", "pbla", "refine", "test"], _),
9.249 + Model.Matches (["pbla2", "pbla", "refine", "test"], _),
9.250 + Model.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _),
9.251 + Model.Matches (["pbla2y", "pbla2", "pbla", "refine", "test"], _)] => ()
9.252 + | _ => error "--- Specify.refine test-pbtyps --- broken with case 4";
9.253 +(*
9.254 +*** pass ["pbla"]
9.255 +*** pass ["pbla","pbla1"]
9.256 +*** pass ["pbla","pbla2"]
9.257 +*** pass ["pbla","pbla2","pbla2x"]
9.258 +*** pass ["pbla","pbla2","pbla2y"]
9.259 +val it =
9.260 + [Model.Matches
9.261 + (["pbla"],
9.262 + {Find=[],
9.263 + Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222",
9.264 + Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),
9.265 + Model.NoMatch
9.266 + (["pbla1","pbla"],
9.267 + {Find=[],
9.268 + Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
9.269 + Superfl "valuesFor aaa222",Superfl "boundVariable aaa222yyy"],
9.270 + Relate=[],Where=[],With=[]}),
9.271 + Model.Matches
9.272 + (["pbla2","pbla"],
9.273 + {Find=[],
9.274 + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
9.275 + Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),
9.276 + Model.NoMatch
9.277 + (["pbla2x","pbla2","pbla"],
9.278 + {Find=[],
9.279 + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
9.280 + Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"],
9.281 + Relate=[],Where=[],With=[]}),
9.282 + Model.Matches
9.283 + (["pbla2y","pbla2","pbla"],
9.284 + {Find=[],
9.285 + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
9.286 + Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})]
9.287 + : match list*)
9.288 +
9.289 +(*case 5: start refinement somewhere in ptyps*)
9.290 +case Specify.refine fmz4 ["pbla2","pbla", "refine", "test"] of
9.291 + [Model.Matches (["pbla2", "pbla", "refine", "test"], _),
9.292 + Model.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _),
9.293 + Model.Matches (["pbla2y", "pbla2", "pbla", "refine", "test"], _)] => ()
9.294 + | _ => error "--- Specify.refine test-pbtyps --- broken with case 5";
9.295 +(*
9.296 +*** pass ["pbla","pbla2"]
9.297 +*** pass ["pbla","pbla2","pbla2x"]
9.298 +*** pass ["pbla","pbla2","pbla2y"]
9.299 +val it =
9.300 + [Model.Matches
9.301 + (["pbla2","pbla"],
9.302 + {Find=[],
9.303 + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
9.304 + Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),
9.305 + Model.NoMatch
9.306 + (["pbla2x","pbla2","pbla"],
9.307 + {Find=[],
9.308 + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
9.309 + Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"],
9.310 + Relate=[],Where=[],With=[]}),
9.311 + Model.Matches
9.312 + (["pbla2y","pbla2","pbla"],
9.313 + {Find=[],
9.314 + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
9.315 + Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})]
9.316 + : match list*)
9.317 +
9.318 +
9.319 +"----------- Refine_Problem (aus subp-rooteq.sml) ----------------------------------------------";
9.320 +"----------- Refine_Problem (aus subp-rooteq.sml) ----------------------------------------------";
9.321 +"----------- Refine_Problem (aus subp-rooteq.sml) ----------------------------------------------";
9.322 +val c = [];
9.323 +val fmz = ["equality ((x+1)*(x+2)=x^^^2+(8::real))","solveFor x",
9.324 + "errorBound (eps=0)","solutions L"];
9.325 +val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
9.326 + ["Test","squ-equ-test-subpbl1"]);
9.327 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.328 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.329 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.330 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "solutions L"*)
9.331 +
9.332 +(*=== specify a not-matching problem ---vvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
9.333 +val nxt = (Specify_Problem ["LINEAR","univariate","equation","test"]);
9.334 +(*=== specify a not-matching problem ---^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
9.335 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "solutions L"*)
9.336 +
9.337 +val www =
9.338 +case f of Test_Out.PpcKF (Test_Out.Problem [],
9.339 + {Find = [Incompl "solutions []"], With = [],
9.340 + Given = [Correct "equality ((x + 1) * (x + 2) = x ^^^ 2 + 8)", Correct "solveFor x"],
9.341 + Where = [False www(*! ! ! ! ! !*)],
9.342 + Relate = [],...}) => www(*! ! !*)
9.343 +| _ => error "--- Refine_Problem broken 1";
9.344 +if www = "matches (x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\nmatches (?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\nmatches (?a + x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\nmatches (?a + ?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8)"
9.345 +then () else error "--- Refine_Problem broken 2";
9.346 +(*ML> f;
9.347 +val it = Form' (Test_Out.PpcKF (0,EdUndef,0,Nundef,
9.348 + (Problem ["LINEAR","univariate","equation","test"], <<<<<===== diff.to above WN120313
9.349 + {Find=[Incompl "solutions []"],
9.350 + Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
9.351 + Correct "solveFor x"],Relate=[],
9.352 + Where=[False "matches (x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)
9.353 + |\nmatches (?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)
9.354 + |\nmatches (?a + x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)
9.355 + |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
9.356 + With=[]}))) : mout
9.357 +*)
9.358 +
9.359 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = (me nxt p c pt) (*Empty_Tac ?!?*);
9.360 +
9.361 +(*=== refine problem -----vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
9.362 +val nxt = (Refine_Problem ["univariate","equation","test"]);
9.363 +(*=== refine problem -----^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
9.364 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.365 +(*("Specify_Problem", Specify_Problem ["normalise", "univariate", ...])*)
9.366 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.367 +(*nxt = ("Specify_Theory", Specify_Theory "Test")*)
9.368 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.369 +(*nxt = ("Specify_Method", Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
9.370 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.371 +(*nxt = ("Apply_Method", *)
9.372 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.373 +(*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
9.374 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.375 +(*nxt = ("Rewrite_Set", Rewrite_Set "Test_simplify")*)
9.376 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.377 +(*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]*)
9.378 +
9.379 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.380 +(*nxt = Model_Problem ["LINEAR","univariate","equation","test"]*)
9.381 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.382 +(*nxt = ("Add_Given", Add_Given "equality (-6 + 3 * x = 0)"*)
9.383 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.384 +(**)
9.385 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.386 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.387 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.388 +(*nxt = Specify_Problem ["LINEAR","univariate","equation","test"])*)
9.389 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.390 +(*xt = ("Specify_Method", Specify_Method ["Test", "solve_linear"])*)
9.391 +val nxt = (Refine_Problem ["univariate","equation","test"]);
9.392 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.393 +(*("Specify_Problem", Specify_Problem ["LINEAR", "univariate", ...])*)
9.394 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.395 +(*val nxt = ("Specify_Method",Specify_Method ("Test","solve_linear"))*)
9.396 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.397 +(*val nxt = ("Apply_Method",Apply_Method ("Test","solve_linear"))*)
9.398 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.399 +(*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)
9.400 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.401 +(*val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify")*)
9.402 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.403 +(*val nxt = ("Check_Postcond",Check_Postcond ["LINEAR","univariate","eq*)
9.404 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.405 +(*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
9.406 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.407 +(*Check_Postcond ["normalise","univariate","equation","test"])*)
9.408 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.409 +val Test_Out.FormKF res = f;
9.410 +
9.411 +if res = "[x = 2]"
9.412 +then case nxt of End_Proof' => ()
9.413 + | _ => error "new behaviour in test:refine.sml:miniscript with mini-subpb 1"
9.414 +else error "new behaviour in test:refine.sml:miniscript with mini-subpb 2"
9.415 +
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/test/Tools/isac/Specify/refine.thy Tue May 12 07:27:21 2020 +0200
10.3 @@ -0,0 +1,49 @@
10.4 +(* Title: Interpret/refine.thy
10.5 + Author: Walther Neuper
10.6 + (c) due to copyright terms
10.7 +*)
10.8 +
10.9 +theory refine
10.10 +imports Isac.Build_Isac
10.11 +begin
10.12 +
10.13 +text \<open>
10.14 + *setup* KEStore_Elems.add_pbts is impossible in *.sml files.
10.15 + The respective test/../refine.sml is called in Test_Isac.thy.
10.16 +\<close>
10.17 +
10.18 +section \<open>data for test "-ptyps.thy: store test-pbtyps by 'setup' ---"\<close>
10.19 +setup \<open>KEStore_Elems.add_pbts
10.20 +[(Specify.prep_pbt thy "pbl_test_refine" [] Problem.id_empty
10.21 + (["refine", "test"], [], Rule_Set.empty, NONE, [])),
10.22 +(Specify.prep_pbt @{theory DiffApp} "pbl_pbla" [] Problem.id_empty
10.23 + (["pbla", "refine", "test"],
10.24 + [("#Given", ["fixedValues a_a"])], Rule_Set.empty, NONE, [])),
10.25 +(Specify.prep_pbt @{theory DiffApp} "pbl_pbla1" [] Problem.id_empty
10.26 + (["pbla1","pbla", "refine", "test"],
10.27 + [("#Given", ["fixedValues a_a","maximum a_1"])], Rule_Set.empty, NONE, [])),
10.28 +(Specify.prep_pbt @{theory DiffApp} "pbl_pbla2" [] Problem.id_empty
10.29 + (["pbla2","pbla", "refine", "test"],
10.30 + [("#Given", ["fixedValues a_a","valuesFor a_2"])], Rule_Set.empty, NONE, [])),
10.31 +(Specify.prep_pbt @{theory DiffApp} "pbl_pbla2x" [] Problem.id_empty
10.32 + (["pbla2x","pbla2","pbla", "refine", "test"],
10.33 + [("#Given", ["fixedValues a_a","valuesFor a_2","functionOf a2_x"])],
10.34 + Rule_Set.empty, NONE, [])),
10.35 +(Specify.prep_pbt @{theory DiffApp} "pbl_pbla2y" [] Problem.id_empty
10.36 + (["pbla2y","pbla2","pbla", "refine", "test"],
10.37 + [("#Given" ,["fixedValues a_a","valuesFor a_2","boundVariable a2_y"])],
10.38 + Rule_Set.empty, NONE, [])),
10.39 +(Specify.prep_pbt @{theory DiffApp} "pbl_pbla2z" [] Problem.id_empty
10.40 + (["pbla2z","pbla2","pbla", "refine", "test"],
10.41 + [("#Given" ,["fixedValues a_a","valuesFor a_2","interval a2_z"])],
10.42 + Rule_Set.empty, NONE, [])),
10.43 +(Specify.prep_pbt @{theory DiffApp} "pbl_pbla3" [] Problem.id_empty
10.44 + (["pbla3","pbla", "refine", "test"],
10.45 + [("#Given" ,["fixedValues a_a","relations a_3"])],
10.46 + Rule_Set.empty, NONE, []))]
10.47 +\<close>
10.48 +
10.49 +(*ML_file "~~/test/Tools/isac/Specify/refine.sml" ... is called in Test_Isac.thy below,
10.50 + so do NOT call it HERE; ?circularity*)
10.51 +
10.52 +end
11.1 --- a/test/Tools/isac/Test_Isac.thy Tue May 12 06:37:04 2020 +0200
11.2 +++ b/test/Tools/isac/Test_Isac.thy Tue May 12 07:27:21 2020 +0200
11.3 @@ -27,7 +27,7 @@
11.4 ~~$ ./xtest-to-coding.sh
11.5 ~~$ ./ztest-to-coding.sh # --"-- + go back to coding (!update thy!)
11.6
11.7 -********************* don't forget (2) BEFORE pushing to repository ****************************
11.8 +//******************* don't forget (2) BEFORE pushing to repository **************************\\
11.9 \<close>
11.10 subsection \<open>Decide between running Test_Isac_Short.thy and Test_Isac.thy\<close>
11.11 text \<open>
11.12 @@ -43,7 +43,7 @@
11.13 From time to time full testing in Test_Isac.thy is recommended. For that purpose
11.14 * set ML_system_64 = "true" in ~/.isabelle/isabisac/etc/preferences.
11.15
11.16 -********************* don't forget to re-set defaults BEFORE updating code *********************
11.17 +\\******************* don't forget to re-set defaults BEFORE updating code *******************//
11.18
11.19 Note that Isabelle/jEdit re-generates the preferences file on shutdown, thus always use
11.20 ***************** $ gedit ~/.isabelle/isabisac/etc/preferences &
11.21 @@ -57,25 +57,26 @@
11.22
11.23 theory Test_Isac
11.24 imports Isac.Build_Isac (* note that imports are WITHOUT open struct ..*)
11.25 + (* in case of ERROR Bad theory import "Draft.Thy_All"..., open each theory one by one *)
11.26 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
11.27 - "ADDTESTS/accumulate-val/Thy_All"
11.28 - "ADDTESTS/Ctxt"
11.29 - "ADDTESTS/test-depend/Build_Test"
11.30 - "ADDTESTS/All_Ctxt"
11.31 - "ADDTESTS/Test_Units"
11.32 - "ADDTESTS/course/phst11/T1_Basics"
11.33 - "ADDTESTS/course/phst11/T2_Rewriting"
11.34 - "ADDTESTS/course/phst11/T3_MathEngine"
11.35 - "ADDTESTS/file-depend/BuildC_Test"
11.36 - "ADDTESTS/session-get_theory/Foo"
11.37 + "~~/test/Tools/isac/ADDTESTS/accumulate-val/Thy_All" (*broken with 05944144a692 *)
11.38 +(**)"~~/test/Tools/isac/ADDTESTS/Ctxt" (*broken with 05944144a692 *)
11.39 +(**)"~~/test/Tools/isac/ADDTESTS/test-depend/Build_Test" (*broken with 05944144a692 *)
11.40 +(**)"~~/test/Tools/isac/ADDTESTS/All_Ctxt" (*broken with 05944144a692 *)
11.41 +(**)"~~/test/Tools/isac/ADDTESTS/Test_Units" (*broken with 05944144a692 *)
11.42 +(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics" (*broken with 05944144a692 *)
11.43 +(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting" (*broken with 05944144a692 *)
11.44 +(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"(*broken with 05944144a692 *)
11.45 +(**)"~~/test/Tools/isac/ADDTESTS/file-depend/BuildC_Test" (*broken with 05944144a692 *)
11.46 +(**)"~~/test/Tools/isac/ADDTESTS/session-get_theory/Foo" (*broken with 05944144a692 *)
11.47 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
11.48 ADDTESTS/------------------------------------------- see end of tests *)
11.49 (*"~~/test/Pure/Isar/Test_Parsers" dropped Isabelle2014-->2015 *)
11.50 (*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" lost at update 2009-2-->2011*)
11.51 - "~~/test/Pure/Isar/Test_Parse_Term"
11.52 +(**)"~~/test/Pure/Isar/Test_Parse_Term" (*broken with 05944144a692 *)
11.53 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
11.54 - "~~/test/Tools/isac/Interpret/ptyps" (* setup for ptyps.sml *)
11.55 - "~~/test/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml*)
11.56 + "~~/test/Tools/isac/Specify/refine" (* setup for refine.sml *)
11.57 + "~~/test/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *)
11.58 "~~/test/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
11.59 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
11.60 "~~/src/Tools/isac/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)
11.61 @@ -117,7 +118,6 @@
11.62 open Step_Solve;
11.63 open Step;
11.64 open Solve; (* NONE *)
11.65 - open Stool; (* NONE *)
11.66 open ContextC; transfer_asms_from_to;
11.67 open Tactic; (* NONE *)
11.68 open P_Model; (* NONE *)
11.69 @@ -191,11 +191,11 @@
11.70 ML_file "BaseDefinitions/substitution.sml"
11.71 ML_file "BaseDefinitions/contextC.sml"
11.72 ML_file "BaseDefinitions/environment.sml"
11.73 - ML_file "BaseDefinitions/kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
11.74 + ML_file "BaseDefinitions/kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
11.75 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
11.76 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
11.77
11.78 - ML_file "ProgLang/evaluate.sml" (* requires setup from calculate.thy *)
11.79 + ML_file "ProgLang/evaluate.sml" (* requires setup from calculate.thy *)
11.80 ML_file "ProgLang/listC.sml"
11.81 ML_file "ProgLang/prog_expr.sml"
11.82 ML_file "ProgLang/program.sml"
11.83 @@ -231,7 +231,6 @@
11.84 subsection \<open>further functionality alongside batch build sequence\<close>
11.85 ML_file "MathEngBasic/thmC.sml"
11.86 ML_file "MathEngBasic/rewrite.sml"
11.87 - ML_file "MathEngBasic/model.sml"
11.88 (*ML_file "MathEngBasic/mstools.sml"*)
11.89 ML_file "MathEngBasic/tactic.sml"
11.90 ML_file "MathEngBasic/ctree.sml"
11.91 @@ -239,9 +238,10 @@
11.92
11.93 ML_file "Specify/o-model.sml"
11.94 ML_file "Specify/i-model.sml"
11.95 - ML_file "Specify/ptyps.sml" (* requires setup from ptyps.thy *)
11.96 + ML_file "Specify/model.sml"
11.97 + ML_file "Specify/refine.sml" (* requires setup from refine.thy *)
11.98 + ML_file "Specify/ptyps.sml"
11.99 ML \<open>(*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*)\<close>
11.100 - ML_file "Specify/generate.sml"
11.101 ML_file "Specify/calchead.sml"
11.102 ML_file "Specify/step-specify.sml"
11.103 ML_file "Specify/specify.sml"
12.1 --- a/test/Tools/isac/Test_Isac_Short.thy Tue May 12 06:37:04 2020 +0200
12.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Tue May 12 07:27:21 2020 +0200
12.3 @@ -1,4 +1,4 @@
12.4 -t(* Title: All tests on isac (some outcommented since Isabelle2002-->2009-2)
12.5 +(* Title: All tests on isac (some outcommented since Isabelle2002-->2009-2)
12.6 Author: Walther Neuper 101001
12.7 (c) copyright due to license terms.
12.8
12.9 @@ -59,24 +59,24 @@
12.10 imports Isac.Build_Isac (* note that imports are WITHOUT open struct ..*)
12.11 (* in case of ERROR Bad theory import "Draft.Thy_All"..., open each theory one by one *)
12.12 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
12.13 - "~~/test/Tools/isac/ADDTESTS/accumulate-val/Thy_All" (*broken with 05944144a692 *)
12.14 -(*"~~/test/Tools/isac/ADDTESTS/Ctxt" broken with 05944144a692 *)
12.15 -(*"~~/test/Tools/isac/ADDTESTS/test-depend/Build_Test" broken with 05944144a692 *)
12.16 -(*"~~/test/Tools/isac/ADDTESTS/All_Ctxt" broken with 05944144a692 *)
12.17 -(*"~~/test/Tools/isac/ADDTESTS/Test_Units" broken with 05944144a692 *)
12.18 -(*"~~/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics" broken with 05944144a692 *)
12.19 -(*"~~/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting" broken with 05944144a692 *)
12.20 -(*"~~/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine" broken with 05944144a692 *)
12.21 -(*"~~/test/Tools/isac/ADDTESTS/file-depend/BuildC_Test" broken with 05944144a692 *)
12.22 -(*"~~/test/Tools/isac/ADDTESTS/session-get_theory/Foo" broken with 05944144a692 *)
12.23 + "~~/test/Tools/isac/ADDTESTS/accumulate-val/Thy_All" (*broken with 05944144a692 *)
12.24 +(**)"~~/test/Tools/isac/ADDTESTS/Ctxt" (*broken with 05944144a692 *)
12.25 +(**)"~~/test/Tools/isac/ADDTESTS/test-depend/Build_Test" (*broken with 05944144a692 *)
12.26 +(**)"~~/test/Tools/isac/ADDTESTS/All_Ctxt" (*broken with 05944144a692 *)
12.27 +(**)"~~/test/Tools/isac/ADDTESTS/Test_Units" (*broken with 05944144a692 *)
12.28 +(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics" (*broken with 05944144a692 *)
12.29 +(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting" (*broken with 05944144a692 *)
12.30 +(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"(*broken with 05944144a692 *)
12.31 +(**)"~~/test/Tools/isac/ADDTESTS/file-depend/BuildC_Test" (*broken with 05944144a692 *)
12.32 +(**)"~~/test/Tools/isac/ADDTESTS/session-get_theory/Foo" (*broken with 05944144a692 *)
12.33 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
12.34 ADDTESTS/------------------------------------------- see end of tests *)
12.35 (*"~~/test/Pure/Isar/Test_Parsers" dropped Isabelle2014-->2015 *)
12.36 (*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" lost at update 2009-2-->2011*)
12.37 -(*"~~/test/Pure/Isar/Test_Parse_Term" broken with 05944144a692 *)
12.38 +(**)"~~/test/Pure/Isar/Test_Parse_Term" (*broken with 05944144a692 *)
12.39 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
12.40 - "~~/test/Tools/isac/Interpret/ptyps" (* setup for ptyps.sml *)
12.41 - "~~/test/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml*)
12.42 + "~~/test/Tools/isac/Specify/refine" (* setup for refine.sml *)
12.43 + "~~/test/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *)
12.44 "~~/test/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
12.45 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
12.46 (*"~~/src/Tools/isac/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*) Test_Isac_Short*)
12.47 @@ -238,7 +238,9 @@
12.48
12.49 ML_file "Specify/o-model.sml"
12.50 ML_file "Specify/i-model.sml"
12.51 - ML_file "Specify/ptyps.sml" (* requires setup from ptyps.thy *)
12.52 + ML_file "Specify/model.sml"
12.53 + ML_file "Specify/refine.sml" (* requires setup from refine.thy *)
12.54 + ML_file "Specify/ptyps.sml"
12.55 ML \<open>(*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*)\<close>
12.56 ML_file "Specify/calchead.sml"
12.57 ML_file "Specify/step-specify.sml"