Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Knowledge/inssort.sml
author Walther Neuper <neuper@ist.tugraz.at>
Tue, 28 Sep 2010 09:06:56 +0200
branchisac-update-Isa09-2
changeset 38031 460c24a6a6ba
parent 37991 028442673981
child 38063 d2bdc4095e73
permissions -rw-r--r--
tuned error and writeln

# raise error --> error
# writeln in atomtyp, atomty, atomt and xmlsrc 
     1 (* use"test-inssort.sml";

     2    W.N.17.6.00

     3 *)

     4 

     5 (* insertion sort, would need lists different from script-lists WN.11.00

     6 WN.7.6.03: -"- started with someList :: 'a list => unl, fun dest_list *)

     7 

     8 "--------------- sort [1,4,3,2] by rewrite_set ----------------";

     9 val thy' = "InsSort";

    10 val ct = "sort [1,4,3,2]";

    11 "--- 1 ---";

    12 val rls = "ins_sort";

    13 val (ct,_) = the (rewrite_set thy' "eval_rls" false rls ct);

    14 if ct="[1, 2, 3, 4]" then "sort [1,4,3,2] OK"

    15 else error "sort [1,4,3,2] didn't work";

    16 

    17 

    18 "---------------- sort [1,3,2] by rewrite stepwise ----------------";

    19 val thy' = "InsSort";

    20 val ct = "sort [1,3,2]";

    21 "--- 1 ---";

    22 val thm = ("sort_def","");

    23 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

    24 (*val ct = "foldr ins [#1::real, #3::real, #2::real] []"*)

    25 "--- 2 ---";

    26 val thm = ("foldr_rec","");

    27 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

    28 (*val ct = "foldr ins [#3, #2] (ins [] #1)"*)

    29 "--- 3 ---";

    30 val thm = ("ins_base","");

    31 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

    32 (*val ct = "foldr ins [#3, #2] [#1]"*)

    33 "--- 4 ---";

    34 val thm = ("foldr_rec","");

    35 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

    36 (*val ct = "foldr ins [#2] (ins [#1] #3)"*)

    37 "--- 5 ---";

    38 val thm = ("ins_rec","");

    39 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

    40 (*val ct = "foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])"*)

    41 "--- 6 ---";

    42 val op_ = "le";

    43 val (ct,_) = the (calculate thy' op_ ct);

    44 (*val ct = "foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])"*)

    45 "--- 7 ---";

    46 val thm = ("if_True","");

    47 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

    48 (*val ct = "foldr ins [#2] (#1 # ins [] #3)"*)

    49 "--- 8 ---";

    50 val thm = ("ins_base","");

    51 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

    52 (*val ct = "foldr ins [#2] [#1, #3]"*)

    53 "--- 9 ---";

    54 val thm = ("foldr_rec","");

    55 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

    56 (*val ct = "foldr ins [] (ins [#1, #3] #2)"*)

    57 "--- 10 ---";

    58 val thm = ("ins_rec","");

    59 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

    60 (*val ct = "foldr ins [] (if #1 < #2 then #1 # ins [#3] #2 else [#2, #1, #3])"*)

    61 "--- 11 ---";

    62 val op_ = "le";

    63 val (ct,_) = the (calculate thy' op_ ct);

    64 (*val ct = "foldr ins [] (if True then #1 # ins [#3] #2 else [#2, #1, #3])"*)

    65 "--- 12 ---";

    66 val thm = ("if_True","");

    67 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

    68 (*"foldr ins [] (#1 # ins [#3] #2)"*)

    69 "--- 13 ---";

    70 val thm = ("ins_rec","");

    71 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

    72 (*"foldr ins [] (#1 # (if #3 < #2 then #3 # ins [] #2 else [#2, #3]))"*)

    73 "--- 14 ---";

    74 val op_ = "le";

    75 val (ct,_) = the (calculate thy' op_ ct);

    76 (*val ct = "foldr ins [] (#1 # (if False then #3 # ins [] #2 else [#2, #3]))"*)

    77 "--- 15 ---";

    78 val thm = ("if_False","");

    79 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

    80 (*val ct = "foldr ins [] [#1, #2, #3]"*)

    81 "--- 16 ---";

    82 val thm = ("foldr_base","");

    83 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

    84 (*val ct = "[#1, #2, #3]"*)

    85 if ct="[1, 2, 3]" then "sort [1,3,2] OK"

    86 else error "sort [1,3,2] didn't work";

    87 

    88 

    89 "---------------- sort [1,3,2] from script ----------------";

    90 val fmz = ["unsorted [1,3,2]", "sorted S"];

    91 val (dI',pI',mI') = 

    92   ("InsSort", ["inssort","functional"], ("InsSort","inssort"));

    93 val p = e_pos'; val c = []; 

    94 

    95 

    96 

    97 (* ------- 17.6.00: mit kleinen problemen aufgegeben

    98 val scr=Script ((term_of o the o (parse thy))

    99 	       "Script Sort (u_::'a list) =   \

   100 		\ Rewrite_Set ins_sort False u_");

   101 

   102 val scr=Script ((term_of o the o (parse thy))

   103       "Script Ins_sort (u_::real list) =          \

   104        \ (let u_ = Rewrite sort_def   False u_; \

   105        \      u_ = Rewrite foldr_rec  False u_; \

   106        \      u_ = Rewrite ins_base   False u_; \

   107        \      u_ = Rewrite foldr_rec  False u_; \

   108        \      u_ = Rewrite ins_rec    False u_; \

   109        \      u_ = Calculate le u_;             \

   110        \      u_ = Rewrite if_True    False u_; \

   111        \      u_ = Rewrite ins_base   False u_; \

   112        \      u_ = Rewrite foldr_rec  False u_; \

   113        \      u_ = Rewrite ins_rec    False u_; \

   114        \      u_ = Calculate le u_;             \

   115        \      u_ = Rewrite if_True    False u_; \

   116        \      u_ = Rewrite ins_rec    False u_; \

   117        \      u_ = Calculate le u_;             \

   118        \      u_ = Rewrite if_False   False u_; \

   119        \      u_ = Rewrite foldr_base False u_  \

   120        \  in u_)");

   121 val scr=parse thy

   122       "Script Ins_sort (u_::real list) =          \

   123        \ (let u_ = Rewrite sort_def   False u_; \

   124        \      u_ = Rewrite foldr_rec  False u_; \

   125        \      u_ = Rewrite ins_base   False u_; \

   126        \      u_ = Rewrite foldr_rec  False u_; \

   127        \      u_ = Rewrite ins_rec    False u_; \

   128        \      u_ = Calculate le u_;             \

   129        \      u_ = Rewrite if_True    False u_; \

   130        \      u_ = Rewrite ins_base   False u_; \

   131        \      u_ = Rewrite foldr_rec  False u_; \

   132        \      u_ = Rewrite ins_rec    False u_; \

   133        \      u_ = u_   \

   134        \  in u_)";

   135 

   136 atomty (term_of (the scr));

   137 

   138 ------- *)
wneuper/isa