# HG changeset patch
# User haftmann
# Date 1255010357 -7200
# Node ID 6f3cdb4a9e11fe9e905cfb218430344505dab86a
# Parent  cdd7800de437ce0a466dad0cf44bc9d200e2426d
added group_stmts

diff -r cdd7800de437 -r 6f3cdb4a9e11 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Thu Oct 08 15:59:16 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML	Thu Oct 08 15:59:17 2009 +0200
@@ -78,6 +78,10 @@
   val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
   val is_cons: program -> string -> bool
   val contr_classparam_typs: program -> string -> itype option list
+  val labelled_name: theory -> program -> string -> string
+  val group_stmts: theory -> program
+    -> ((string * stmt) list * (string * stmt) list
+      * ((string * stmt) list * (string * stmt) list)) list
 
   val expand_eta: theory -> int -> thm -> thm
   val clean_thms: theory -> thm list -> thm list
@@ -492,6 +496,45 @@
       end
   | _ => [];
 
+fun labelled_name thy program name = case Graph.get_node program name
+ of Fun (c, _) => quote (Code.string_of_const thy c)
+  | Datatype (tyco, _) => "type " ^ quote (Sign.extern_type thy tyco)
+  | Datatypecons (c, _) => quote (Code.string_of_const thy c)
+  | Class (class, _) => "class " ^ quote (Sign.extern_class thy class)
+  | Classrel (sub, super) => let
+        val Class (sub, _) = Graph.get_node program sub
+        val Class (super, _) = Graph.get_node program super
+      in quote (Sign.extern_class thy sub ^ " < " ^ Sign.extern_class thy super) end
+  | Classparam (c, _) => quote (Code.string_of_const thy c)
+  | Classinst ((class, (tyco, _)), _) => let
+        val Class (class, _) = Graph.get_node program class
+        val Datatype (tyco, _) = Graph.get_node program tyco
+      in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end
+
+fun group_stmts thy program =
+  let
+    fun is_fun (_, Fun _) = true | is_fun _ = false;
+    fun is_datatypecons (_, Datatypecons _) = true | is_datatypecons _ = false;
+    fun is_datatype (_, Datatype _) = true | is_datatype _ = false;
+    fun is_class (_, Class _) = true | is_class _ = false;
+    fun is_classrel (_, Classrel _) = true | is_classrel _ = false;
+    fun is_classparam (_, Classparam _) = true | is_classparam _ = false;
+    fun is_classinst (_, Classinst _) = true | is_classinst _ = false;
+    fun group stmts =
+      if forall (is_datatypecons orf is_datatype) stmts
+      then (filter is_datatype stmts, [], ([], []))
+      else if forall (is_class orf is_classrel orf is_classparam) stmts
+      then ([], filter is_class stmts, ([], []))
+      else if forall (is_fun orf is_classinst) stmts
+      then ([], [], List.partition is_fun stmts)
+      else error ("Illegal mutual dependencies: " ^
+        (commas o map (labelled_name thy program o fst)) stmts)
+  in
+    rev (Graph.strong_conn program)
+    |> map (AList.make (Graph.get_node program))
+    |> map group
+  end;
+
 
 (** translation kernel **)