Merge branch 'sort-munge-output' into multi_arch_refactor

tools/c-parser/CTranslation.thy

@@ -107,7 +107,6 @@ ML_file "recursive_records/recursive_record_pp.ML"
 ML_file "recursive_records/recursive_record_package.ML"
 ML_file "expression_typing.ML"
 ML_file "UMM_Proofs.ML"
-ML_file "Listsort.ML"
 ML_file "program_analysis.ML"
 ML_file "heapstatetype.ML"
 ML_file "MemoryModelExtras-sig.ML"

tools/c-parser/Listsort.ML

@@ -1,58 +0,0 @@
-(* Listsort *)
-signature LISTSORT =
-sig
-
-val sort   : ('a * 'a -> order) -> 'a list -> 'a list
-val sorted : ('a * 'a -> order) -> 'a list -> bool
-
-end;
-
-(*
-   [sort ordr xs] sorts the list xs in nondecreasing order, using the
-   given ordering.  Uses Richard O'Keefe's smooth applicative merge
-   sort.
-
-   [sorted ordr xs] checks that the list xs is sorted in nondecreasing
-   order, in the given ordering.
-*)
-structure Listsort : LISTSORT =
-struct
-(* Listsort *)
-
-(** Smooth Applicative Merge Sort, Richard O'Keefe 1982        **)
-(** From L.C. Paulson: ML for the Working Programmer, CUP 1991 **)
-(** Optimized for Moscow ML **)
-
-fun sort ordr []          = []
-  | sort ordr (xs as [_]) = xs
-  | sort ordr (xs as [x1, x2]) =
-    (case ordr(x1, x2) of
-	 GREATER => [x2, x1]
-       | _       => xs)
-  | sort ordr xs =
-    let fun merge []      ys = ys
-          | merge xs      [] = xs
-          | merge (x::xs) (y::ys) =
-            if ordr(x, y) <> GREATER then x :: merge xs (y::ys)
-            else y :: merge (x::xs) ys
-        fun mergepairs l1  []              k = [l1]
-          | mergepairs l1 (ls as (l2::lr)) k =
-            if k mod 2 = 1 then l1::ls
-            else mergepairs (merge l1 l2) lr (k div 2)
-	fun nextrun run []      = (run, [])
-	  | nextrun run (xs as (x::xr)) =
-	    if ordr(x, List.hd run) = LESS then (run, xs)
-	    else nextrun (x::run) xr
-        fun sorting []      ls r = List.hd(mergepairs [] ls 0)
-          | sorting (x::xs) ls r =
-	    let val (revrun, tail) = nextrun [x] xs
-	    in sorting tail (mergepairs (List.rev revrun) ls (r+1)) (r+1) end
-    in sorting xs [] 0 end;
-
-fun sorted ordr []         = true
-  | sorted ordr (y1 :: yr) =
-    let fun h x0 []       = true
-	  | h x0 (x1::xr) = ordr(x0, x1) <> GREATER andalso h x1 xr
-    in h y1 yr end;
-
-end;

tools/c-parser/program_analysis.ML

@@ -377,7 +377,7 @@ local
          defined_functions = defined_functions, allow_underscore_idents = aui,
          recursive_functions = recursive_functions, caller_info = caller_info,
          modify_locs = modify_locs, typedefs = typedefs, fnspecs = fnspecs,
-         read_globals = read_globals, globinits = globinits, owners = owners, 
+         read_globals = read_globals, globinits = globinits, owners = owners,
          munge_info_fname = munge_info_fname}
     (* fields in reverse order to above *)
     fun from' munge_info_fname owners globinits read_globals fnspecs typedefs modify_locs caller_info
@@ -2060,7 +2060,7 @@ fun export_mungedb (c as CSE cse) =
       fun foldthis (_, vinfos) acc = List.foldl tab_foldthis acc vinfos
       fun recurse tab = Symtab.fold foldthis tab []
       val data0 = recurse (get_vars c)
-      val data = Listsort.sort String.compare data0
+      val data = Library.sort String.compare data0
     in
       List.app (fn s => TextIO.output(outstrm, s)) data;
       TextIO.closeOut outstrm

tools/c-parser/standalone-parser/c-parser.mlb

@@ -33,7 +33,7 @@ in
   ../expression_typing.ML
   ../FunctionalRecordUpdate.ML
   ../complit.ML
-  ../Listsort.ML
+  library.ML
   ../program_analysis.ML
   ../syntax_transforms.ML
   ann

tools/c-parser/standalone-parser/library.ML

@@ -0,0 +1,67 @@
+(*
+ * Extracted from Isabelle sources (src/Pure/library.ML)
+ *
+ * @TAG(OTHER_BSD)
+ *)
+
+
+signature LIBRARY =
+sig
+
+  val sort : ('a * 'a -> order) -> 'a list -> 'a list
+
+end
+
+structure Library : LIBRARY =
+struct
+
+(*stable mergesort -- preserves order of equal elements*)
+fun mergesort unique ord =
+  let
+    fun merge (xs as x :: xs') (ys as y :: ys') =
+          (case ord (x, y) of
+            LESS => x :: merge xs' ys
+          | EQUAL =>
+              if unique then merge xs ys'
+              else x :: merge xs' ys
+          | GREATER => y :: merge xs ys')
+      | merge [] ys = ys
+      | merge xs [] = xs;
+
+    fun merge_all [xs] = xs
+      | merge_all xss = merge_all (merge_pairs xss)
+    and merge_pairs (xs :: ys :: xss) = merge xs ys :: merge_pairs xss
+      | merge_pairs xss = xss;
+
+    fun runs (x :: y :: xs) =
+          (case ord (x, y) of
+             LESS => ascending y [x] xs
+           | EQUAL =>
+               if unique then runs (x :: xs)
+               else ascending y [x] xs
+           | GREATER => descending y [x] xs)
+      | runs xs = [xs]
+
+    and ascending x xs (zs as y :: ys) =
+          (case ord (x, y) of
+             LESS => ascending y (x :: xs) ys
+           | EQUAL =>
+               if unique then ascending x xs ys
+               else ascending y (x :: xs) ys
+           | GREATER => rev (x :: xs) :: runs zs)
+      | ascending x xs [] = [rev (x :: xs)]
+
+    and descending x xs (zs as y :: ys) =
+          (case ord (x, y) of
+             GREATER => descending y (x :: xs) ys
+           | EQUAL =>
+               if unique then descending x xs ys
+               else (x :: xs) :: runs zs
+           | LESS => (x :: xs) :: runs zs)
+      | descending x xs [] = [x :: xs];
+
+  in merge_all o runs end;
+
+fun sort ord = mergesort false ord;
+
+end