4 |
4 |
5 use"../smltest/IsacKnowledge/diffapp.sml"; |
5 use"../smltest/IsacKnowledge/diffapp.sml"; |
6 use"diffapp.sml"; |
6 use"diffapp.sml"; |
7 *) |
7 *) |
8 |
8 |
9 Rewrite.trace_on := false; |
9 Rewrite.trace_on := false; (*true false*) |
10 "Contents----------------------------------------------"; |
10 "Contents----------------------------------------------"; |
11 " Specify_Problem (match_itms_oris) "; |
11 " Specify_Problem (match_itms_oris) "; |
12 " test specify, fmz <> [] "; |
12 " test specify, fmz <> [] "; |
13 " test specify, fmz = [] "; |
13 " test specify, fmz = [] "; |
14 " problemtypes + formalizations "; |
14 " problemtypes + formalizations "; |
666 val t = TermC.str2term "(hd o (filterVar (f_f::real))) (eqs::bool list)"; |
666 val t = TermC.str2term "(hd o (filterVar (f_f::real))) (eqs::bool list)"; |
667 val s = subst_atomic env t; |
667 val s = subst_atomic env t; |
668 UnparseC.term s; |
668 UnparseC.term s; |
669 val t = TermC.str2term |
669 val t = TermC.str2term |
670 "(hd o filterVar A) [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]"; |
670 "(hd o filterVar A) [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]"; |
671 Rewrite.trace_on := false; |
671 Rewrite.trace_on := false; (*true false*) |
672 val SOME (t',_) = rewrite_set_ thy false prog_expr t; |
672 val SOME (t',_) = rewrite_set_ thy false prog_expr t; |
673 Rewrite.trace_on:=false; |
673 Rewrite.trace_on:=false; (*true false*) |
674 val s' = UnparseC.term t'; |
674 val s' = UnparseC.term t'; |
675 (*=== inhibit exn 110726============================================================= |
675 (*=== inhibit exn 110726============================================================= |
676 if s' = "A = a * b" then() else error "new behaviour with prog_expr 3.1."; |
676 if s' = "A = a * b" then() else error "new behaviour with prog_expr 3.1."; |
677 val env = env @ [(TermC.str2term "h_h::bool", TermC.str2term s')]; |
677 val env = env @ [(TermC.str2term "h_h::bool", TermC.str2term s')]; |
678 === inhibit exn 110726=============================================================*) |
678 === inhibit exn 110726=============================================================*) |