# HG changeset patch
# User haftmann
# Date 1239869495 -7200
# Node ID 35f255987e18624428ac786606bd85ef4256832b
# Parent  86ca651da03e7fcd8118722c1290eeaf77f424d2
tuned order of functions

diff -r 86ca651da03e -r 35f255987e18 src/Tools/code/code_thingol.ML
--- a/src/Tools/code/code_thingol.ML	Thu Apr 16 10:11:35 2009 +0200
+++ b/src/Tools/code/code_thingol.ML	Thu Apr 16 10:11:35 2009 +0200
@@ -459,7 +459,45 @@
 
 (* translation *)
 
-fun ensure_class thy (algbr as (_, algebra)) funcgr class =
+fun ensure_tyco thy algbr funcgr tyco =
+  let
+    val stmt_datatype =
+      let
+        val (vs, cos) = Code.get_datatype thy tyco;
+      in
+        fold_map (translate_tyvar_sort thy algbr funcgr) vs
+        ##>> fold_map (fn (c, tys) =>
+          ensure_const thy algbr funcgr c
+          ##>> fold_map (translate_typ thy algbr funcgr) tys) cos
+        #>> (fn info => Datatype (tyco, info))
+      end;
+  in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end
+and ensure_const thy algbr funcgr c =
+  let
+    fun stmt_datatypecons tyco =
+      ensure_tyco thy algbr funcgr tyco
+      #>> (fn tyco => Datatypecons (c, tyco));
+    fun stmt_classparam class =
+      ensure_class thy algbr funcgr class
+      #>> (fn class => Classparam (c, class));
+    fun stmt_fun ((vs, ty), raw_thms) =
+      let
+        val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
+          then raw_thms
+          else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms;
+      in
+        fold_map (translate_tyvar_sort thy algbr funcgr) vs
+        ##>> translate_typ thy algbr funcgr ty
+        ##>> fold_map (translate_eq thy algbr funcgr) thms
+        #>> (fn info => Fun (c, info))
+      end;
+    val stmt_const = case Code.get_datatype_of_constr thy c
+     of SOME tyco => stmt_datatypecons tyco
+      | NONE => (case AxClass.class_of_param thy c
+         of SOME class => stmt_classparam class
+          | NONE => stmt_fun (Code_Wellsorted.typ funcgr c, Code_Wellsorted.eqns funcgr c))
+  in ensure_stmt lookup_const (declare_const thy) stmt_const c end
+and ensure_class thy (algbr as (_, algebra)) funcgr class =
   let
     val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
     val cs = #params (AxClass.get_info thy class);
@@ -477,65 +515,6 @@
       ##>> ensure_class thy algbr funcgr superclass
       #>> Classrel;
   in ensure_stmt lookup_classrel (declare_classrel thy) stmt_classrel (subclass, superclass) end
-and ensure_tyco thy algbr funcgr tyco =
-  let
-    val stmt_datatype =
-      let
-        val (vs, cos) = Code.get_datatype thy tyco;
-      in
-        fold_map (translate_tyvar_sort thy algbr funcgr) vs
-        ##>> fold_map (fn (c, tys) =>
-          ensure_const thy algbr funcgr c
-          ##>> fold_map (translate_typ thy algbr funcgr) tys) cos
-        #>> (fn info => Datatype (tyco, info))
-      end;
-  in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end
-and translate_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
-  fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
-  #>> (fn sort => (unprefix "'" v, sort))
-and translate_typ thy algbr funcgr (TFree (v, _)) =
-      pair (ITyVar (unprefix "'" v))
-  | translate_typ thy algbr funcgr (Type (tyco, tys)) =
-      ensure_tyco thy algbr funcgr tyco
-      ##>> fold_map (translate_typ thy algbr funcgr) tys
-      #>> (fn (tyco, tys) => tyco `%% tys)
-and translate_dicts thy (algbr as (proj_sort, algebra)) funcgr thm (ty, sort) =
-  let
-    val pp = Syntax.pp_global thy;
-    datatype typarg =
-        Global of (class * string) * typarg list list
-      | Local of (class * class) list * (string * (int * sort));
-    fun class_relation (Global ((_, tyco), yss), _) class =
-          Global ((class, tyco), yss)
-      | class_relation (Local (classrels, v), subclass) superclass =
-          Local ((subclass, superclass) :: classrels, v);
-    fun type_constructor tyco yss class =
-      Global ((class, tyco), (map o map) fst yss);
-    fun type_variable (TFree (v, sort)) =
-      let
-        val sort' = proj_sort sort;
-      in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
-    val typargs = Sorts.of_sort_derivation pp algebra
-      {class_relation = class_relation, type_constructor = type_constructor,
-       type_variable = type_variable} (ty, proj_sort sort)
-      handle Sorts.CLASS_ERROR e => not_wellsorted thy thm ty sort e;
-    fun mk_dict (Global (inst, yss)) =
-          ensure_inst thy algbr funcgr inst
-          ##>> (fold_map o fold_map) mk_dict yss
-          #>> (fn (inst, dss) => DictConst (inst, dss))
-      | mk_dict (Local (classrels, (v, (k, sort)))) =
-          fold_map (ensure_classrel thy algbr funcgr) classrels
-          #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
-  in fold_map mk_dict typargs end
-and translate_eq thy algbr funcgr (thm, linear) =
-  let
-    val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
-      o Logic.unvarify o prop_of) thm;
-  in
-    fold_map (translate_term thy algbr funcgr (SOME thm)) args
-    ##>> translate_term thy algbr funcgr (SOME thm) rhs
-    #>> rpair (thm, linear)
-  end
 and ensure_inst thy (algbr as (_, algebra)) funcgr (class, tyco) =
   let
     val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
@@ -572,31 +551,12 @@
       #>> (fn ((((class, tyco), arity), superarities), classparams) =>
              Classinst ((class, (tyco, arity)), (superarities, classparams)));
   in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
-and ensure_const thy algbr funcgr c =
-  let
-    fun stmt_datatypecons tyco =
+and translate_typ thy algbr funcgr (TFree (v, _)) =
+      pair (ITyVar (unprefix "'" v))
+  | translate_typ thy algbr funcgr (Type (tyco, tys)) =
       ensure_tyco thy algbr funcgr tyco
-      #>> (fn tyco => Datatypecons (c, tyco));
-    fun stmt_classparam class =
-      ensure_class thy algbr funcgr class
-      #>> (fn class => Classparam (c, class));
-    fun stmt_fun ((vs, ty), raw_thms) =
-      let
-        val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
-          then raw_thms
-          else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms;
-      in
-        fold_map (translate_tyvar_sort thy algbr funcgr) vs
-        ##>> translate_typ thy algbr funcgr ty
-        ##>> fold_map (translate_eq thy algbr funcgr) thms
-        #>> (fn info => Fun (c, info))
-      end;
-    val stmt_const = case Code.get_datatype_of_constr thy c
-     of SOME tyco => stmt_datatypecons tyco
-      | NONE => (case AxClass.class_of_param thy c
-         of SOME class => stmt_classparam class
-          | NONE => stmt_fun (Code_Wellsorted.typ funcgr c, Code_Wellsorted.eqns funcgr c))
-  in ensure_stmt lookup_const (declare_const thy) stmt_const c end
+      ##>> fold_map (translate_typ thy algbr funcgr) tys
+      #>> (fn (tyco, tys) => tyco `%% tys)
 and translate_term thy algbr funcgr thm (Const (c, ty)) =
       translate_app thy algbr funcgr thm ((c, ty), [])
   | translate_term thy algbr funcgr thm (Free (v, _)) =
@@ -617,6 +577,15 @@
             translate_term thy algbr funcgr thm t'
             ##>> fold_map (translate_term thy algbr funcgr thm) ts
             #>> (fn (t, ts) => t `$$ ts)
+and translate_eq thy algbr funcgr (thm, linear) =
+  let
+    val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
+      o Logic.unvarify o prop_of) thm;
+  in
+    fold_map (translate_term thy algbr funcgr (SOME thm)) args
+    ##>> translate_term thy algbr funcgr (SOME thm) rhs
+    #>> rpair (thm, linear)
+  end
 and translate_const thy algbr funcgr thm (c, ty) =
   let
     val tys = Sign.const_typargs thy (c, ty);
@@ -695,7 +664,38 @@
 and translate_app thy algbr funcgr thm (c_ty_ts as ((c, _), _)) =
   case Code.get_case_scheme thy c
    of SOME case_scheme => translate_app_case thy algbr funcgr thm case_scheme c_ty_ts
-    | NONE => translate_app_const thy algbr funcgr thm c_ty_ts;
+    | NONE => translate_app_const thy algbr funcgr thm c_ty_ts
+and translate_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
+  fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
+  #>> (fn sort => (unprefix "'" v, sort))
+and translate_dicts thy (algbr as (proj_sort, algebra)) funcgr thm (ty, sort) =
+  let
+    val pp = Syntax.pp_global thy;
+    datatype typarg =
+        Global of (class * string) * typarg list list
+      | Local of (class * class) list * (string * (int * sort));
+    fun class_relation (Global ((_, tyco), yss), _) class =
+          Global ((class, tyco), yss)
+      | class_relation (Local (classrels, v), subclass) superclass =
+          Local ((subclass, superclass) :: classrels, v);
+    fun type_constructor tyco yss class =
+      Global ((class, tyco), (map o map) fst yss);
+    fun type_variable (TFree (v, sort)) =
+      let
+        val sort' = proj_sort sort;
+      in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
+    val typargs = Sorts.of_sort_derivation pp algebra
+      {class_relation = class_relation, type_constructor = type_constructor,
+       type_variable = type_variable} (ty, proj_sort sort)
+      handle Sorts.CLASS_ERROR e => not_wellsorted thy thm ty sort e;
+    fun mk_dict (Global (inst, yss)) =
+          ensure_inst thy algbr funcgr inst
+          ##>> (fold_map o fold_map) mk_dict yss
+          #>> (fn (inst, dss) => DictConst (inst, dss))
+      | mk_dict (Local (classrels, (v, (k, sort)))) =
+          fold_map (ensure_classrel thy algbr funcgr) classrels
+          #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
+  in fold_map mk_dict typargs end;
 
 
 (* store *)