1.1 --- a/src/Tools/isac/Interpret/script.sml Sat Jan 07 10:09:33 2012 +0100
1.2 +++ b/src/Tools/isac/Interpret/script.sml Sun Jan 08 08:41:35 2012 +0100
1.3 @@ -567,7 +567,7 @@
1.4 if f = f_ then Ass (m,f') else AssWeak (m,f')
1.5 else NotAss
1.6 | _ => NotAss)
1.7 -
1.8 +(*
1.9 | assod pt _ (m as Check_elementwise' (consts,_,(consts_chkd,_)))
1.10 (Const ("Script.Check'_elementwise",_) $ consts' $ _) =
1.11 (tracing("### assod Check'_elementwise: consts= "^(term2str consts)^
1.12 @@ -576,6 +576,12 @@
1.13 if consts = consts'
1.14 then (tracing"### assod Check'_elementwise: Ass"; Ass (m, consts_chkd))
1.15 else (tracing"### assod Check'_elementwise: NotAss"; NotAss))
1.16 +*)
1.17 + | assod pt _ (m as Check_elementwise' (consts,_,(consts_chkd,_)))
1.18 + (Const ("Script.Check'_elementwise",_) $ consts' $ _) =
1.19 + if consts = consts'
1.20 + then Ass (m, consts_chkd)
1.21 + else NotAss
1.22
1.23 | assod pt _ (m as Or_to_List' (ors, list)) (Const ("Script.Or'_to'_List",_) $ _) =
1.24 Ass (m, list)
2.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Sat Jan 07 10:09:33 2012 +0100
2.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Sun Jan 08 08:41:35 2012 +0100
2.3 @@ -527,33 +527,36 @@
2.4 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
2.5 (*solve the simple linear equilation for A TODO: return eq, not list of eq*)
2.6 val (p,_,fa,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.7 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.8 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.9 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.10 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.11 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.12 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.13 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.14 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.15 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.16 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.17 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.18 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.19 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.20 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.21 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.22 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.23 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.24 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.25 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.26 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.27 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.28 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.29 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.30 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.31 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.32 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.33 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.34 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (*Add_Given "equality (3 = 3 * A / 4)"*)
2.35 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (* Add_Given "solveFor A"*)
2.36 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (*Add_Find "solutions L"*)
2.37 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (*Specify_Theory "Isac"*)
2.38 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (*Specify_Problem ["normalize", "polynomial",
2.39 + "univariate", "equation"])*)
2.40 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (* Specify_Method ["PolyEq", "normalize_poly"]*)
2.41 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "normalize_poly"]*)
2.42 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (*Rewrite ("all_left", "PolyEq.all_left")*)
2.43 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (*Rewrite_Set_Inst (["(bdv, A)"], "make_ratpoly_in")*)
2.44 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (*Rewrite_Set "polyeq_simplify"*)
2.45 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (**)
2.46 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (**)
2.47 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (*Add_Given "equality (3 + -3 / 4 * A = 0)"*)
2.48 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (*Add_Given "solveFor A"*)
2.49 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (*Add_Find "solutions A_i"*)
2.50 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (**)
2.51 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (**)
2.52 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (**)
2.53 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
2.54 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (*Rewrite_Set_Inst (["(bdv, A)"], "d1_polyeq_simplify")*)
2.55 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (*Rewrite_Set "polyeq_simplify"*)
2.56 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (*Rewrite_Set "norm_Rational_parenthesized"*)
2.57 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (*Or_to_List*)
2.58 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (*Check_elementwise "Assumptions"*)
2.59 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (*Check_Postcond ["degree_1", "polynomial",
2.60 + "univariate", "equation"]*)
2.61 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (*Check_Postcond ["normalize", "polynomial",
2.62 + "univariate", "equation"]*)
2.63 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt; (*End_Proof'*)
2.64 f2str fa;
2.65 *}
2.66
2.67 @@ -829,11 +832,11 @@
2.68 (*([6], Res), 24 = ?A * (1 / 2 + -1 * (-1 / 4)) + ?B * (1 / 2 + -1 * (1 / 2))*)
2.69 " eq_a = (Rewrite_Set norm_Rational False) eq_a;"^
2.70 (*([7], Res), 24 = ?A * 3 / 4*)
2.71 - " (aaa::real) = argument_in (rhs eq_a);"^
2.72 - " x = Take aaa;"^
2.73 - "(* (A::bool list) = (SubProblem (PolyEq'," ^
2.74 + (*" (aaa::real) = argument_in (rhs eq_a);"^
2.75 + " x = Take aaa;"^*)
2.76 + " (num1::bool list) = (SubProblem (Isac'," ^
2.77 " [univariate,equation],[no_met])" ^
2.78 - " [BOOL eq_a, REAL A]);*)"^ (*GOON: probably doesn't work ?*)
2.79 + " [BOOL eq_a, REAL (A::real)]);"^
2.80 " (x::real) = 3"^(*only here that the last step of the ptree is visible in tracing output*)
2.81 " in X)"
2.82 ));
2.83 @@ -970,20 +973,25 @@
2.84 (*([6], Res), 24 = A * (1 / 2 + -1 * (-1 / 4)) + B * (1 / 2 + -1 * (1 / 2))*)
2.85 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.86 (*([7], Res), 24 = A * 3 / 4*)
2.87 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.88 +(*([8], Pbl), solve (24 = 3 * A / 4, A)*)
2.89 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Add_Given "equality (24 = 3 * A / 4)"*)
2.90 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Add_Given "solveFor A"*)
2.91 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Add_Find "solutions A_i"*)
2.92 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Specify_Theory "Isac"*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Specify_Problem ["normalize", "polynomial",
2.93 + "univariate", "equation"]*)
2.94 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Specify_Method ["PolyEq", "normalize_poly"]*)
2.95 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "normalize_poly"]*)
2.96 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Rewrite ("all_left", "PolyEq.all_left")*)
2.97 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Rewrite_Set_Inst (["(bdv, A)"], "make_ratpoly_in")*)
2.98 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Rewrite_Set "polyeq_simplify"*)
2.99 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Subproblem ("Isac", ["degree_1", "polynomial",
2.100 + "univariate", "equation"])*)
2.101 +*}
2.102 +ML {*
2.103 show_pt pt;
2.104 *}
2.105 -
2.106 ML {*
2.107 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.108 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.109 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.110 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.111 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.112 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.113 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.114 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.115 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.116 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.117 *}
2.118
2.119 section {*Write Tests for Crucial Details*}
2.120 @@ -993,7 +1001,7 @@
2.121
2.122 section {*Integrate Program into Knowledge*}
2.123 ML {*
2.124 -@{theory Isac}
2.125 +print_depth 999;
2.126 *}
2.127
2.128 end
3.1 --- a/test/Tools/isac/CLEANUP Sat Jan 07 10:09:33 2012 +0100
3.2 +++ b/test/Tools/isac/CLEANUP Sun Jan 08 08:41:35 2012 +0100
3.3 @@ -1,41 +1,41 @@
3.4 rm *~
3.5 rm *.tar*
3.6 - rm #*
3.7 - rm .#*
3.8 -rm *.orig
3.9 +rm #*
3.10 +rm .#*
3.11 +rm *.orig*
3.12 cd ADDTESTS
3.13 rm *~
3.14 rm #*
3.15 rm .#*
3.16 rm *.tar*
3.17 - rm *.orig
3.18 + rm *.orig*
3.19 cd course
3.20 rm *~
3.21 rm #*
3.22 rm .#*
3.23 rm *.tar*
3.24 - rm *.orig
3.25 + rm *.orig*
3.26 cd
3.27 cd ml_quickstart
3.28 rm *~
3.29 rm #*
3.30 rm .#*
3.31 rm *.tar*
3.32 - rm *.orig
3.33 + rm *.orig*
3.34 cd ..
3.35 cd phst11
3.36 rm *~
3.37 rm #*
3.38 rm .#*
3.39 rm *.tar*
3.40 - rm *.orig
3.41 + rm *.orig*
3.42 cd ..
3.43 cd SignalProcess
3.44 rm *~
3.45 rm #*
3.46 rm .#*
3.47 rm *.tar*
3.48 - rm *.orig
3.49 + rm *.orig*
3.50 cd ..
3.51 cd ..
3.52 cd file-depend
3.53 @@ -43,14 +43,14 @@
3.54 rm #*
3.55 rm .#*
3.56 rm *.tar*
3.57 - rm *.orig
3.58 + rm *.orig*
3.59 cd ..
3.60 cd test-depend
3.61 rm *~
3.62 rm #*
3.63 rm .#*
3.64 rm *.tar*
3.65 - rm *.orig
3.66 + rm *.orig*
3.67 cd ..
3.68 cd ..
3.69 cd ProgLang
3.70 @@ -58,40 +58,40 @@
3.71 rm #*
3.72 rm .#*
3.73 rm *.tar*
3.74 - rm *.orig
3.75 + rm *.orig*
3.76 cd ..
3.77 cd Minisubpbl
3.78 rm *~
3.79 rm #*
3.80 rm .#*
3.81 rm *.tar*
3.82 - rm *.orig
3.83 + rm *.orig*
3.84 cd ..
3.85 cd Interpret
3.86 rm *~
3.87 rm #*
3.88 rm .#*
3.89 rm *.tar*
3.90 - rm *.orig
3.91 + rm *.orig*
3.92 cd ..
3.93 cd xmlsrc
3.94 rm *~
3.95 rm #*
3.96 rm .#*
3.97 rm *.tar*
3.98 - rm *.orig
3.99 + rm *.orig*
3.100 cd ..
3.101 cd Frontend
3.102 rm *~
3.103 rm #*
3.104 rm .#*
3.105 rm *.tar*
3.106 - rm *.orig
3.107 + rm *.orig*
3.108 cd ..
3.109 cd Knowledge
3.110 rm *~
3.111 rm #*
3.112 rm .#*
3.113 rm *.tar*
3.114 - rm *.orig
3.115 + rm *.orig*
3.116 cd ..