31 %eqsystem.sml |
31 %eqsystem.sml |
32 %--------------------------------------------------------------------------- |
32 %--------------------------------------------------------------------------- |
33 %"----------- eval_sort -------------------------------------------"; |
33 %"----------- eval_sort -------------------------------------------"; |
34 %"----------- eval_sort -------------------------------------------"; |
34 %"----------- eval_sort -------------------------------------------"; |
35 %"----------- eval_sort -------------------------------------------"; |
35 %"----------- eval_sort -------------------------------------------"; |
36 %val ts = str2term "[c_2 = 0, -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0]"; |
36 %val ts = TermC.parse_test @{context} "[c_2 = 0, -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0]"; |
37 %val ts' = sort (ord_simplify_Integral_ false (assoc_thy"Isac.thy") []) |
37 %val ts' = sort (ord_simplify_Integral_ false (assoc_thy"Isac.thy") []) |
38 % (isalist2list ts); |
38 % (isalist2list ts); |
39 %terms2str ts'; |
39 %terms2str ts'; |
40 %val ts'' = list2isalist HOLogic.boolT ts'; |
40 %val ts'' = list2isalist HOLogic.boolT ts'; |
41 %if term2str ts'' = "[-1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0, c_2 = 0]" |
41 %if term2str ts'' = "[-1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0, c_2 = 0]" |
42 %then () else raise error "eqsystem.sml eval_sort 1"; |
42 %then () else raise error "eqsystem.sml eval_sort 1"; |
43 % |
43 % |
44 %val t = str2term "order_system [c_2 = 0,\ |
44 %val t = TermC.parse_test @{context} "order_system [c_2 = 0,\ |
45 % \-1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0]"; |
45 % \-1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0]"; |
46 %val Some (str,_) = eval_order_system "" "EqSystem.order'_system" t ""; |
46 %val Some (str,_) = eval_order_system "" "EqSystem.order'_system" t ""; |
47 %if str = "order_system [c_2 = 0, -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0] = [-1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0, c_2 = 0]" then () |
47 %if str = "order_system [c_2 = 0, -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0] = [-1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0, c_2 = 0]" then () |
48 %else raise error "eqsystem.sml eval_sort 2"; |
48 %else raise error "eqsystem.sml eval_sort 2"; |
49 % |
49 % |