# HG changeset patch # User Adam Chlipala # Date 1213129366 14400 # Node ID 104d43266b334381f5064cf57d6d5a4f19916ab8 # Parent 145b536fc70299404930d0d2a17c79b04d370149 Field sorting for Flat diff -r 145b536fc702 -r 104d43266b33 src/flat_util.sig --- a/src/flat_util.sig Tue Jun 10 16:05:10 2008 -0400 +++ b/src/flat_util.sig Tue Jun 10 16:22:46 2008 -0400 @@ -28,6 +28,9 @@ signature FLAT_UTIL = sig structure Typ : sig + val compare : Flat.typ * Flat.typ -> order + val sortFields : (string * Flat.typ) list -> (string * Flat.typ) list + val mapfold : (Flat.typ', 'state, 'abort) Search.mapfolder -> (Flat.typ, 'state, 'abort) Search.mapfolder diff -r 145b536fc702 -r 104d43266b33 src/flat_util.sml --- a/src/flat_util.sml Tue Jun 10 16:05:10 2008 -0400 +++ b/src/flat_util.sml Tue Jun 10 16:22:46 2008 -0400 @@ -33,6 +33,49 @@ structure Typ = struct +fun join (o1, o2) = + case o1 of + EQUAL => o2 () + | v => v + +fun joinL f (os1, os2) = + case (os1, os2) of + (nil, nil) => EQUAL + | (nil, _) => LESS + | (h1 :: t1, h2 :: t2) => + join (f (h1, h2), fn () => joinL f (t1, t2)) + | (_ :: _, nil) => GREATER + +fun compare ((t1, _), (t2, _)) = + case (t1, t2) of + (TFun (d1, r1), TFun (d2, r2)) => + join (compare (d1, d2), fn () => compare (r1, r2)) + | (TCode (d1, r1), TCode (d2, r2)) => + join (compare (d1, d2), fn () => compare (r1, r2)) + | (TRecord xts1, TRecord xts2) => + let + val xts2 = sortFields xts1 + val xts2 = sortFields xts2 + in + joinL compareFields (xts1, xts2) + end + | (TNamed n1, TNamed n2) => Int.compare (n1, n2) + + | (TFun _, _) => LESS + | (_, TFun _) => GREATER + + | (TCode _, _) => LESS + | (_, TCode _) => GREATER + + | (TRecord _, _) => LESS + | (_, TRecord _) => GREATER + +and compareFields ((x1, t1), (x2, t2)) = + join (String.compare (x1, x2), + fn () => compare (t1, t2)) + +and sortFields xts = ListMergeSort.sort (fn (x, y) => compareFields (x, y) = GREATER) xts + fun mapfold fc = let fun mft c acc =