test/Tools/isac/Interpret/me.sml
changeset 59279 255c853ea2f0
parent 59248 5eba5e6d5266
child 59582 23984b62804f
equal deleted inserted replaced
59278:a474900d5bd2 59279:255c853ea2f0
     8 *)
     8 *)
     9 
     9 
    10 "-----------------------------------------------------------------";
    10 "-----------------------------------------------------------------";
    11 "table of contents -----------------------------------------------";
    11 "table of contents -----------------------------------------------";
    12 "-----------------------------------------------------------------";
    12 "-----------------------------------------------------------------";
    13 "=====new ptree 1: crippled by cut_level_'_ ======================";
    13 "=====new ctree 1: crippled by cut_level_'_ ======================";
    14 "-------------- get_interval from ctree with move_dn:modspec.sml -";
    14 "-------------- get_interval from ctree with move_dn:modspec.sml -";
    15 "=====new ptree 2 without changes ================================";
    15 "=====new ctree 2 without changes ================================";
    16 "-------------- getFormulaeFromTo --------------------------------";
    16 "-------------- getFormulaeFromTo --------------------------------";
    17 "autoCalculate"; 
    17 "autoCalculate"; 
    18 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
    18 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
    19 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
    19 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
    20 "--------- maximum-example: complete_metitms ---------------------";
    20 "--------- maximum-example: complete_metitms ---------------------";
    23 "-----------------------------------------------------------------";
    23 "-----------------------------------------------------------------";
    24 "-----------------------------------------------------------------";
    24 "-----------------------------------------------------------------";
    25 
    25 
    26 
    26 
    27 
    27 
    28 "=====new ptree 1: crippled by cut_level_'_ ======================";
    28 "=====new ctree 1: crippled by cut_level_'_ ======================";
    29 "=====new ptree 1: crippled by cut_level_'_ ======================";
    29 "=====new ctree 1: crippled by cut_level_'_ ======================";
    30 "=====new ptree 1: crippled by cut_level_'_ ======================";
    30 "=====new ctree 1: crippled by cut_level_'_ ======================";
    31 reset_states ();
    31 reset_states ();
    32 CalcTree
    32 CalcTree
    33 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
    33 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
    34 	   "solveFor x","solutions L"], 
    34 	   "solveFor x","solutions L"], 
    35   ("RatEq",["univariate","equation"],["no_met"]))];
    35   ("RatEq",["univariate","equation"],["no_met"]))];
    58 getTactic 1 ([1,4],Res);(*Rewrite real_rat_mult_1*)
    58 getTactic 1 ([1,4],Res);(*Rewrite real_rat_mult_1*)
    59 
    59 
    60 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
    60 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
    61 interSteps 1 ([4,2],Res)(*..is activeFormula !?!*);
    61 interSteps 1 ([4,2],Res)(*..is activeFormula !?!*);
    62 val ((pt,_),_) = get_calc 1;
    62 val ((pt,_),_) = get_calc 1;
    63 writeln(pr_ptree pr_short pt);
    63 writeln(pr_ctree pr_short pt);
    64 (*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:
    64 (*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:
    65  ###########################################################################*)
    65  ###########################################################################*)
    66 val (pt, _) = cut_level_'_ [] [] pt ([4,1],Frm);                         (*#*)
    66 val (pt, _) = cut_level_'_ [] [] pt ([4,1],Frm);                         (*#*)
    67 (*##########################################################################*)
    67 (*##########################################################################*)
    68 writeln(pr_ptree pr_short pt);
    68 writeln(pr_ctree pr_short pt);
    69 (*##########################################################################
    69 (*##########################################################################
    70   attention: the ctree in states is still the old (perfect) !!!
    70   attention: the ctree in states is still the old (perfect) !!!
    71 ############################################################################*)
    71 ############################################################################*)
    72 
    72 
    73 
    73 
    74 
    74 
    75 "-------------- get_interval from ctree with move_dn:modspec.sml -";
    75 "-------------- get_interval from ctree with move_dn:modspec.sml -";
    76 "-------------- get_interval from ctree with move_dn:modspec.sml -";
    76 "-------------- get_interval from ctree with move_dn:modspec.sml -";
    77 "-------------- get_interval from ctree with move_dn:modspec.sml -";
    77 "-------------- get_interval from ctree with move_dn:modspec.sml -";
    78 writeln(pr_ptree pr_short pt);
    78 writeln(pr_ctree pr_short pt);
    79 writeln(posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
    79 writeln(posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
    80 
    80 
    81 case map fst (get_interval ([],Frm) ([],Res) 99999 pt) of
    81 case map fst (get_interval ([],Frm) ([],Res) 99999 pt) of
    82     [([], Frm), 
    82     [([], Frm), 
    83      ([1], Frm), 
    83      ([1], Frm), 
   217   | _ => error "diff.behav.in ctree.sml: get_interval lev 1g";
   217   | _ => error "diff.behav.in ctree.sml: get_interval lev 1g";
   218 
   218 
   219 
   219 
   220 
   220 
   221 
   221 
   222 "=====new ptree 2 without changes ================================";
   222 "=====new ctree 2 without changes ================================";
   223 "=====new ptree 2 without changes ================================";
   223 "=====new ctree 2 without changes ================================";
   224 "=====new ptree 2 without changes ================================";
   224 "=====new ctree 2 without changes ================================";
   225 reset_states ();
   225 reset_states ();
   226 CalcTree
   226 CalcTree
   227 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
   227 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
   228 	   "solveFor x","solutions L"], 
   228 	   "solveFor x","solutions L"], 
   229   ("RatEq",["univariate","equation"],["no_met"]))];
   229   ("RatEq",["univariate","equation"],["no_met"]))];
   231 autoCalculate 1 CompleteCalc; 
   231 autoCalculate 1 CompleteCalc; 
   232 val ((pt,_),_) = get_calc 1;
   232 val ((pt,_),_) = get_calc 1;
   233 val p = get_pos 1 1;
   233 val p = get_pos 1 1;
   234 val (Form f, tac, asms) = pt_extract (pt, p);
   234 val (Form f, tac, asms) = pt_extract (pt, p);
   235 if term2str f = "[x = 6 / 5]" andalso p = ([], Res) then ()
   235 if term2str f = "[x = 6 / 5]" andalso p = ([], Res) then ()
   236   else error "after ===new ptree 2 without changes ===";
   236   else error "after ===new ctree 2 without changes ===";
   237 writeln(pr_ptree pr_short pt);
   237 writeln(pr_ctree pr_short pt);
   238  
   238  
   239 
   239 
   240 "-------------- getFormulaeFromTo --------------------------------";
   240 "-------------- getFormulaeFromTo --------------------------------";
   241 "-------------- getFormulaeFromTo --------------------------------";
   241 "-------------- getFormulaeFromTo --------------------------------";
   242 "-------------- getFormulaeFromTo --------------------------------";
   242 "-------------- getFormulaeFromTo --------------------------------";