added group_stmts
authorhaftmann
Thu Oct 08 15:59:17 2009 +0200 (2009-10-08)
changeset 328956f3cdb4a9e11
parent 32894 cdd7800de437
child 32896 99cd75a18b78
added group_stmts
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Tools/Code/code_thingol.ML	Thu Oct 08 15:59:16 2009 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Oct 08 15:59:17 2009 +0200
     1.3 @@ -78,6 +78,10 @@
     1.4    val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
     1.5    val is_cons: program -> string -> bool
     1.6    val contr_classparam_typs: program -> string -> itype option list
     1.7 +  val labelled_name: theory -> program -> string -> string
     1.8 +  val group_stmts: theory -> program
     1.9 +    -> ((string * stmt) list * (string * stmt) list
    1.10 +      * ((string * stmt) list * (string * stmt) list)) list
    1.11  
    1.12    val expand_eta: theory -> int -> thm -> thm
    1.13    val clean_thms: theory -> thm list -> thm list
    1.14 @@ -492,6 +496,45 @@
    1.15        end
    1.16    | _ => [];
    1.17  
    1.18 +fun labelled_name thy program name = case Graph.get_node program name
    1.19 + of Fun (c, _) => quote (Code.string_of_const thy c)
    1.20 +  | Datatype (tyco, _) => "type " ^ quote (Sign.extern_type thy tyco)
    1.21 +  | Datatypecons (c, _) => quote (Code.string_of_const thy c)
    1.22 +  | Class (class, _) => "class " ^ quote (Sign.extern_class thy class)
    1.23 +  | Classrel (sub, super) => let
    1.24 +        val Class (sub, _) = Graph.get_node program sub
    1.25 +        val Class (super, _) = Graph.get_node program super
    1.26 +      in quote (Sign.extern_class thy sub ^ " < " ^ Sign.extern_class thy super) end
    1.27 +  | Classparam (c, _) => quote (Code.string_of_const thy c)
    1.28 +  | Classinst ((class, (tyco, _)), _) => let
    1.29 +        val Class (class, _) = Graph.get_node program class
    1.30 +        val Datatype (tyco, _) = Graph.get_node program tyco
    1.31 +      in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end
    1.32 +
    1.33 +fun group_stmts thy program =
    1.34 +  let
    1.35 +    fun is_fun (_, Fun _) = true | is_fun _ = false;
    1.36 +    fun is_datatypecons (_, Datatypecons _) = true | is_datatypecons _ = false;
    1.37 +    fun is_datatype (_, Datatype _) = true | is_datatype _ = false;
    1.38 +    fun is_class (_, Class _) = true | is_class _ = false;
    1.39 +    fun is_classrel (_, Classrel _) = true | is_classrel _ = false;
    1.40 +    fun is_classparam (_, Classparam _) = true | is_classparam _ = false;
    1.41 +    fun is_classinst (_, Classinst _) = true | is_classinst _ = false;
    1.42 +    fun group stmts =
    1.43 +      if forall (is_datatypecons orf is_datatype) stmts
    1.44 +      then (filter is_datatype stmts, [], ([], []))
    1.45 +      else if forall (is_class orf is_classrel orf is_classparam) stmts
    1.46 +      then ([], filter is_class stmts, ([], []))
    1.47 +      else if forall (is_fun orf is_classinst) stmts
    1.48 +      then ([], [], List.partition is_fun stmts)
    1.49 +      else error ("Illegal mutual dependencies: " ^
    1.50 +        (commas o map (labelled_name thy program o fst)) stmts)
    1.51 +  in
    1.52 +    rev (Graph.strong_conn program)
    1.53 +    |> map (AList.make (Graph.get_node program))
    1.54 +    |> map group
    1.55 +  end;
    1.56 +
    1.57  
    1.58  (** translation kernel **)
    1.59