test/Tools/isac/Interpret/ctree.sml
branchdecompose-isar
changeset 42185 332a0653d4c9
parent 42124 ba52b628c40c
child 42190 a48e6fdc934c
     1.1 --- a/test/Tools/isac/Interpret/ctree.sml	Mon Jul 25 14:19:50 2011 +0200
     1.2 +++ b/test/Tools/isac/Interpret/ctree.sml	Mon Jul 25 17:44:19 2011 +0200
     1.3 @@ -17,17 +17,14 @@
     1.4  "-------------- fun update_ctxt, fun g_ctxt ----------------------";
     1.5  "-------------- check positions in miniscript --------------------";
     1.6  "-------------- get_allpos' (from ptree above)--------------------";
     1.7 -(**#####################################################################(**)
     1.8  "-------------- cut_level (from ptree above)----------------------";
     1.9  "-------------- cut_tree (from ptree above)-----------------------";
    1.10  "=====new ptree 1a miniscript with mini-subpbl ===================";
    1.11  "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
    1.12 -(**)#####################################################################**)
    1.13  "=====new ptree 2 miniscript with mini-subpbl ====================";
    1.14  "-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
    1.15  "-------------- cappend (from ptree above)------------------------";
    1.16  "-------------- cappend minisubpbl -------------------------------";
    1.17 -
    1.18  "=====new ptree 3 ================================================";
    1.19  "-------------- move_dn ------------------------------------------";
    1.20  "-------------- move_dn: Frm -> Res ------------------------------";
    1.21 @@ -35,7 +32,6 @@
    1.22  "------ move into detail -----------------------------------------";
    1.23  "=====new ptree 3a ===============================================";
    1.24  "-------------- move_dn in Incomplete ctree ----------------------";
    1.25 -
    1.26  "=====new ptree 4: crooked by cut_level_'_ =======================";
    1.27  (*############## development stopped 0501 ########################*)
    1.28  (******************************************************************)
    1.29 @@ -46,18 +42,13 @@
    1.30  (*              val get_trace = SAVE_get_trace;                   *)
    1.31  (******************************************************************)
    1.32  (*############## development stopped 0501 ########################*)
    1.33 -
    1.34  "=====new ptree 4 ratequation ====================================";
    1.35  "-------------- pt_extract form, tac, asm<>[] --------------------";
    1.36  "=====new ptree 5 minisubpbl =====================================";
    1.37  "-------------- pt_extract form, tac, asm ------------------------";
    1.38 -
    1.39 -(**#####################################################################(**)
    1.40  "=====new ptree 6 minisubpbl intersteps ==========================";
    1.41  "-------------- get_allpos' new ----------------------------------";
    1.42  "-------------- cut_tree new (from ptree above)-------------------";
    1.43 -(**)#####################################################################**)
    1.44 -
    1.45  "-----------------------------------------------------------------";
    1.46  "-----------------------------------------------------------------";
    1.47  "-----------------------------------------------------------------";
    1.48 @@ -148,8 +139,6 @@
    1.49  
    1.50   show_pt pt;
    1.51  
    1.52 -
    1.53 -
    1.54  "-------------- get_allpos' (from ptree above)--------------------";
    1.55  "-------------- get_allpos' (from ptree above)--------------------";
    1.56  "-------------- get_allpos' (from ptree above)--------------------";
    1.57 @@ -213,8 +202,6 @@
    1.58  then () else error "ctree.sml: diff:behav. in get_allpos' 6";
    1.59  
    1.60  
    1.61 -(**##############################################################(**)
    1.62 -
    1.63  "-------------- cut_level (from ptree above)----------------------";
    1.64  "-------------- cut_level (from ptree above)----------------------";
    1.65  "-------------- cut_level (from ptree above)----------------------";
    1.66 @@ -387,6 +374,9 @@
    1.67   val ((pt,_),_) = get_calc 1;
    1.68   show_pt pt;
    1.69  
    1.70 +if (term2str o fst) (get_obj g_result pt [3,2,1]) = "x = 0 + 1" then ()
    1.71 +else error "mini-subpbl interSteps broken";
    1.72 +
    1.73  "-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
    1.74  "-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
    1.75  "-------------- cut_tree (intermedi.ptree: 3rd level)-------------";