# HG changeset patch
# User haftmann
# Date 1140019785 -3600
# Node ID 630b8dd0b31af958a27a1214eb340d5bfdd07f69
# Parent  1a8f08f9f8afbfe8efd6d89efdb60bb3760936ba
exported some interfaces useful for other code generator approaches

diff -r 1a8f08f9f8af -r 630b8dd0b31a src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Wed Feb 15 17:09:25 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Wed Feb 15 17:09:45 2006 +0100
@@ -39,6 +39,11 @@
     -> theory -> theory;
   val set_int_tyco: string -> theory -> theory;
 
+  val codegen_incr: term -> theory -> (string * CodegenThingol.def) list * theory;
+  val get_ml_fun_datatype: theory -> (string -> string)
+    -> ((string * CodegenThingol.funn) list -> Pretty.T)
+        * ((string * CodegenThingol.datatyp) list -> Pretty.T);
+
   val appgen_default: appgen;
   val appgen_let: (int -> term -> term list * term)
     -> appgen;
@@ -500,7 +505,7 @@
     |> Symtab.update (
          #ml CodegenSerializer.serializers
          |> apsnd (fn seri => seri
-            (nsp_dtcon, nsp_class, fn tyco' => tyco' = idf_of_name thy nsp_tyco tyco )
+            (nsp_dtcon, nsp_class, fn tyco' => tyco' = idf_of_name thy nsp_tyco tyco)
               [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst]]
             )
        )
@@ -591,7 +596,7 @@
               trns
               |> debug 5 (fn _ => "trying defgen class declaration for " ^ quote cls)
               |> fold_map (ensure_def_class thy tabs) (ClassPackage.the_superclasses thy cls)
-              ||>> (codegen_type thy tabs o map snd) cs
+              ||>> (exprsgen_type thy tabs o map snd) cs
               ||>> (fold_map o fold_map) (exprgen_tyvar_sort thy tabs) sortctxts
               |-> (fn ((supcls, memtypes), sortctxts) => succeed
                 (Class (supcls, ("a", idfs ~~ (sortctxts ~~ memtypes)))))
@@ -620,7 +625,7 @@
                     trns
                     |> debug 5 (fn _ => "trying defgen datatype for " ^ quote dtco)
                     |> fold_map (exprgen_tyvar_sort thy tabs) vars
-                    ||>> fold_map (fn (c, ty) => codegen_type thy tabs ty #-> (fn ty' => pair (c, ty'))) cos'
+                    ||>> fold_map (fn (c, ty) => exprsgen_type thy tabs ty #-> (fn ty' => pair (c, ty'))) cos'
                     |-> (fn (sorts, cos'') => succeed (Datatype
                          (sorts, cos'')))
                   end
@@ -657,7 +662,7 @@
       |> ensure_def_tyco thy tabs tyco
       ||>> fold_map (exprgen_type thy tabs) tys
       |-> (fn (tyco, tys) => pair (tyco `%% tys))
-and codegen_type thy tabs =
+and exprsgen_type thy tabs =
   fold_map (exprgen_type thy tabs) o snd o devarify_typs;
 
 fun exprgen_classlookup thy tabs (ClassPackage.Instance (inst, ls)) trns =
@@ -695,9 +700,9 @@
             end;
         in
           trns
-          |> (codegen_eqs thy tabs o map dest_eqthm) eq_thms
-          ||>> (codegen_eqs thy tabs o the_list o Option.map mk_default) default
-          ||>> codegen_type thy tabs [ty]
+          |> (exprsgen_eqs thy tabs o map dest_eqthm) eq_thms
+          ||>> (exprsgen_eqs thy tabs o the_list o Option.map mk_default) default
+          ||>> exprsgen_type thy tabs [ty]
           ||>> fold_map (exprgen_tyvar_sort thy tabs) sortctxt
           |-> (fn (((eqs, eq_default), [ty]), sortctxt) => (pair o SOME) (eqs @ eq_default, (sortctxt, ty)))
         end
@@ -825,18 +830,18 @@
             ||>> fold_map (exprgen_term thy tabs) ts
             |-> (fn (e, es) => pair (e `$$ es))
       end
-and codegen_term thy tabs =
+and exprsgen_term thy tabs =
   fold_map (exprgen_term thy tabs) o snd o devarify_term_typs
-and codegen_eqs thy tabs =
+and exprsgen_eqs thy tabs =
   apfst (map (fn (rhs::args) => (args, rhs)))
-    oo fold_burrow (codegen_term thy tabs)
+    oo fold_burrow (exprsgen_term thy tabs)
     o map (fn (args, rhs) => (rhs :: args))
 and appgen_default thy tabs ((c, ty), ts) trns =
   trns
   |> ensure_def_const thy tabs (c, ty)
   ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
          (ClassPackage.extract_classlookup thy (c, ty))
-  ||>> codegen_type thy tabs [ty]
+  ||>> exprsgen_type thy tabs [ty]
   ||>> fold_map (exprgen_term thy tabs) ts
   |-> (fn (((c, ls), [ty]), es) =>
          pair (IConst ((c, ty), ls) `$$ es))
@@ -925,7 +930,7 @@
     |> exprgen_type thy tabs ty'
     ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
            (ClassPackage.extract_classlookup thy (c, ty))
-    ||>> codegen_type thy tabs [ty_def]
+    ||>> exprsgen_type thy tabs [ty_def]
     ||>> exprgen_term thy tabs tf
     ||>> exprgen_term thy tabs tx
     |-> (fn ((((_, ls), [ty]), tf), tx) => pair (IConst ((idf, ty), ls) `$ tf `$ tx))
@@ -988,6 +993,8 @@
 
 fun mk_tabs thy =
   let
+    fun get_specifications thy c =
+      Defs.specifications_of (Theory.defs_of thy) c;
     fun extract_defs thy =
       let
         fun dest thm =
@@ -1037,6 +1044,25 @@
          |> fold (fn ty' => ConstNameMangler.declare (thy, deftab)
               (c, (ty, ty')) #> snd) tys)
       end;
+    (* über *alle*: (map fst o NameSpace.dest_table o Consts.space_of o Sign.consts_of) thy
+       * (c, ty) reicht dann zur zünftigen Deklaration
+       * somit fliegt ein Haufen Grusch raus, deftab bleibt allerdings wegen thyname
+      fun mk_overltabs thy =
+      (Symtab.empty, ConstNameMangler.empty)
+      |> Symtab.fold
+          (fn c => if (is_none o ClassPackage.lookup_const_class thy) c
+            then case get_specifications thy c
+             of [_] => NONE
+              | tys => fold
+                (fn (overltab1, overltab2) => (
+                    overltab1
+                    |> Symtab.update_new (c, (Sign.the_const_type thy c, tys)),
+                    overltab2
+                    |> fold (fn (ty, (_, thyname)) => ConstNameMangler.declare (thy, deftab)
+                         (c, (Sign.the_const_type thy c, ty)) #> snd) tys))
+                else I
+          ) deftab
+      |> add_monoeq thy deftab;*)
     fun mk_overltabs thy deftab =
       (Symtab.empty, ConstNameMangler.empty)
       |> Symtab.fold
@@ -1126,6 +1152,23 @@
     fold ensure (get_datatype_case_consts thy) thy
   end;
 
+fun codegen_incr t thy =
+  thy
+  |> `(#modl o CodegenData.get)
+  ||>> expand_module NONE (fn thy => fn tabs => exprsgen_term thy tabs [t])
+  ||>> `(#modl o CodegenData.get)
+  |-> (fn ((modl_old, _), modl_new) => pair (CodegenThingol.diff_module (modl_new, modl_old)));
+
+fun get_ml_fun_datatype thy resolv =
+  let
+    val target_data = 
+      ((fn data => (the o Symtab.lookup data) "ml") o #target_data o CodegenData.get) thy;
+  in
+    CodegenSerializer.ml_fun_datatype (nsp_dtcon, nsp_class, K false)
+      ((Option.map fst oo Symtab.lookup o #syntax_tyco) target_data,
+      (Option.map fst oo Symtab.lookup o #syntax_const) target_data)
+      resolv
+  end;
 
 
 (** target languages **)
@@ -1200,11 +1243,15 @@
       if Sign.declared_tyname thy tyco
       then tyco
       else error ("no such type constructor: " ^ quote tyco);
-    fun prep_tyco thy tyco =
-      tyco
+    fun prep_tyco thy raw_tyco =
+      raw_tyco
       |> Sign.intern_type thy
       |> check_tyco thy
       |> idf_of_name thy nsp_tyco;
+    fun no_args_tyco thy raw_tyco =
+      AList.lookup (op =) ((NameSpace.dest_table o #types o Type.rep_tsig o Sign.tsig_of) thy)
+        (Sign.intern_type thy raw_tyco)
+      |> (fn SOME ((Type.LogicalType i), _) => i);
     fun mk reader target thy =
       let
         val _ = get_serializer target;
@@ -1225,7 +1272,8 @@
               logic_data)))
       end;
   in
-    CodegenSerializer.parse_syntax (read_quote (fn thy => prep_tyco thy raw_tyco) read_typ codegen_type)
+    CodegenSerializer.parse_syntax (fn thy => no_args_tyco thy raw_tyco)
+    (read_quote (fn thy => prep_tyco thy raw_tyco) read_typ exprsgen_type)
     #-> (fn reader => pair (mk reader))
   end;
 
@@ -1246,6 +1294,8 @@
   let
     fun prep_const thy raw_const =
       idf_of_const thy (mk_tabs thy) (read_const thy raw_const);
+    fun no_args_const thy raw_const =
+      (length o fst o strip_type o snd o read_const thy) raw_const;
     fun mk reader target thy =
       let
         val _ = get_serializer target;
@@ -1257,7 +1307,8 @@
         |-> (fn pretty => add_pretty_syntax_const c target pretty)
       end;
   in
-    CodegenSerializer.parse_syntax (read_quote (fn thy => prep_const thy raw_const) Sign.read_term codegen_term)
+    CodegenSerializer.parse_syntax (fn thy => no_args_const thy raw_const)
+      (read_quote (fn thy => prep_const thy raw_const) Sign.read_term exprsgen_term)
     #-> (fn reader => pair (mk reader))
   end;
 
diff -r 1a8f08f9f8af -r 630b8dd0b31a src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Wed Feb 15 17:09:25 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Wed Feb 15 17:09:45 2006 +0100
@@ -18,14 +18,20 @@
       -> string list option
       -> CodegenThingol.module -> unit)
       * OuterParse.token list;
-  val parse_syntax: (string -> 'b -> 'a * 'b) -> OuterParse.token list ->
+  val parse_syntax: ('b -> int) -> (string -> 'b -> 'a * 'b) -> OuterParse.token list ->
     ('b -> 'a pretty_syntax * 'b) * OuterParse.token list;
   val parse_targetdef: string -> CodegenThingol.prim list;
   val pretty_list: string -> string -> int * string -> CodegenThingol.iexpr pretty_syntax;
   val serializers: {
     ml: string * (string * string * (string -> bool) -> serializer),
     haskell: string * (string list -> serializer)
-  }
+  };
+  val ml_fun_datatype: string * string * (string -> bool)
+    -> ((string -> CodegenThingol.itype pretty_syntax option)
+        * (string -> CodegenThingol.iexpr pretty_syntax option))
+    -> (string -> string)
+    -> ((string * CodegenThingol.funn) list -> Pretty.T)
+        * ((string * CodegenThingol.datatyp) list -> Pretty.T);
 end;
 
 structure CodegenSerializer: CODEGEN_SERIALIZER =
@@ -177,19 +183,20 @@
     || pair (parse_nonatomic_mixfix reader, BR)
   ) -- OuterParse.string --| OuterParse.$$$ ")" >> (fn ((p, fxy), s) => (p s, fxy));
 
-fun parse_syntax reader =
+fun parse_syntax no_args reader =
   let
     fun is_arg (Arg _) = true
       | is_arg Ignore = true
       | is_arg _ = false;
-    fun mk fixity mfx =
+    fun mk fixity mfx ctxt =
       let
-        val i = length (List.filter is_arg mfx)
-      in ((i, i), fillin_mixfix fixity mfx) end;
+        val i = (length o List.filter is_arg) mfx;
+        val _ = if i > no_args ctxt then error "too many arguments in codegen syntax" else ();
+      in (((i, i), fillin_mixfix fixity mfx), ctxt) end;
   in
     parse_syntax_proto reader
-    #-> (fn (mfx_reader, fixity) : ('Z -> 'Y mixfix list * 'Z) * fixity =>
-      pair (mfx_reader #-> (fn mfx => pair (mk fixity mfx)))
+    #-> (fn (mfx_reader, fixity) =>
+      pair (mfx_reader #-> (fn mfx => mk fixity mfx))
     )
   end;
 
@@ -342,55 +349,39 @@
 
 local
 
-fun ml_from_defs (is_cons, needs_type)
-    (from_prim, (_, tyco_syntax, const_syntax)) resolver prefix defs =
+fun ml_expr_seri (is_cons, needs_type) (tyco_syntax, const_syntax) resolv =
   let
-    val resolv = resolver prefix;
-    fun chunk_defs ps =
-      let
-        val (p_init, p_last) = split_last ps
-      in
-        Pretty.chunks (p_init @ [Pretty.block ([p_last, str ";"])])
-      end;
     val ml_from_label =
-      resolv
-      #> NameSpace.base
-      #> translate_string (fn "_" => "__" | "." => "_" | c => c)
-      #> str;
-    fun ml_from_label' l =
-      Pretty.block [str "#", ml_from_label l];
-    fun ml_from_lookup fxy [] p =
-          p
-      | ml_from_lookup fxy [l] p =
-          brackify fxy [
-            ml_from_label' l,
-            p
-          ]
-      | ml_from_lookup fxy ls p =
-          brackify fxy [
-            Pretty.enum " o" "(" ")" (map ml_from_label' ls),
-            p
-          ];
+      str o translate_string (fn "_" => "__" | "." => "_" | c => c)
+        o NameSpace.base o resolv;
     fun ml_from_sortlookup fxy ls =
       let
+        fun from_label l =
+          Pretty.block [str "#", ml_from_label l];
+        fun from_lookup fxy [] p = p
+          | from_lookup fxy [l] p =
+              brackify fxy [
+                from_label l,
+                p
+              ]
+          | from_lookup fxy ls p =
+              brackify fxy [
+                Pretty.enum " o" "(" ")" (map from_label ls),
+                p
+              ];
         fun from_classlookup fxy (Instance (inst, lss)) =
               brackify fxy (
                 (str o resolv) inst
                 :: map (ml_from_sortlookup BR) lss
               )
           | from_classlookup fxy (Lookup (classes, (v, ~1))) =
-              ml_from_lookup BR classes (str v)
+              from_lookup BR classes (str v)
           | from_classlookup fxy (Lookup (classes, (v, i))) =
-              ml_from_lookup BR (string_of_int (i+1) :: classes) (str v)
+              from_lookup BR (string_of_int (i+1) :: classes) (str v)
       in case ls
        of [l] => from_classlookup fxy l
         | ls => (Pretty.list "(" ")" o map (from_classlookup NOBR)) ls
       end;
-    val ml_from_label =
-      resolv
-      #> NameSpace.base
-      #> translate_string (fn "_" => "__" | "." => "_" | c => c)
-      #> str;
     fun ml_from_tycoexpr fxy (tyco, tys) =
       let
         val tyco' = (str o resolv) tyco
@@ -422,7 +413,7 @@
               ml_from_type (INFX (1, R)) t2
             ]
           end
-      | ml_from_type _ (IVarT (v, _)) =
+      | ml_from_type fxy (IVarT (v, _)) =
           str ("'" ^ v);
     fun ml_from_expr fxy (e as IApp (e1, e2)) =
           (case unfold_const_app e
@@ -512,19 +503,29 @@
               :: (lss
               @ map (ml_from_expr BR) es)
             );
+  in (ml_from_label, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, ml_from_expr) end;
+
+fun ml_fun_datatyp (is_cons, needs_type) (tyco_syntax, const_syntax) resolv =
+  let
+    val (ml_from_label, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, ml_from_expr) =
+      ml_expr_seri (is_cons, needs_type) (tyco_syntax, const_syntax) resolv;
+    fun chunk_defs ps =
+      let
+        val (p_init, p_last) = split_last ps
+      in
+        Pretty.chunks (p_init @ [Pretty.block ([p_last, str ";"])])
+      end;
     fun ml_from_funs (defs as def::defs_tl) =
       let
         fun mk_definer [] = "val"
           | mk_definer _ = "fun";
-        fun check_args (_, Fun ((pats, _)::_, _)) NONE =
+        fun check_args (_, ((pats, _)::_, _)) NONE =
               SOME (mk_definer pats)
-          | check_args (_, Fun ((pats, _)::_, _)) (SOME definer) =
+          | check_args (_, ((pats, _)::_, _)) (SOME definer) =
               if mk_definer pats = definer
               then SOME definer
               else error ("mixing simultaneous vals and funs not implemented")
-          | check_args _ _ =
-              error ("function definition block containing other definitions than functions")
-        fun mk_fun definer (name, Fun (eqs as eq::eq_tl, (sortctxt, ty))) =
+        fun mk_fun definer (name, (eqs as eq::eq_tl, (sortctxt, ty))) =
           let
             val shift = if null eq_tl then I else map (Pretty.block o single);
             fun mk_eq definer (pats, expr) =
@@ -545,16 +546,10 @@
         chunk_defs (
           mk_fun (the (fold check_args defs NONE)) def
           :: map (mk_fun "and") defs_tl
-        ) |> SOME
+        )
       end;
-    fun ml_from_datatypes defs =
+    fun ml_from_datatypes (defs as (def::defs_tl)) =
       let
-        val defs' = List.mapPartial
-          (fn (name, Datatype info) => SOME (name, info)
-            | (name, Datatypecons _) => NONE
-            | (name, def) => error ("datatype block containing illegal def: "
-                ^ (Pretty.output o pretty_def) def)
-          ) defs
         fun mk_cons (co, []) =
               str (resolv co)
           | mk_cons (co, tys) =
@@ -573,14 +568,27 @@
             :: separate (str "|") (map mk_cons cs)
           )
       in
-        case defs'
-         of (def::defs_tl) =>
-            chunk_defs (
-              mk_datatype "datatype" def
-              :: map (mk_datatype "and ") defs_tl
-            ) |> SOME
-          | _ => NONE
-      end
+        chunk_defs (
+          mk_datatype "datatype" def
+          :: map (mk_datatype "and") defs_tl
+        )
+      end;
+  in (ml_from_funs, ml_from_datatypes) end;
+
+fun ml_from_defs (is_cons, needs_type)
+    (from_prim, (_, tyco_syntax, const_syntax)) resolver prefix defs =
+  let
+    val resolv = resolver prefix;
+    val (ml_from_label, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, ml_from_expr) =
+      ml_expr_seri (is_cons, needs_type) (tyco_syntax, const_syntax) resolv;
+    val (ml_from_funs, ml_from_datatypes) =
+      ml_fun_datatyp (is_cons, needs_type) (tyco_syntax, const_syntax) resolv;
+    val filter_datatype =
+      List.mapPartial
+        (fn (name, Datatype info) => SOME (name, info)
+          | (name, Datatypecons _) => NONE
+          | (name, def) => error ("datatype block containing illegal def: "
+                ^ (Pretty.output o pretty_def) def));
     fun ml_from_def (name, Undef) =
           error ("empty definition during serialization: " ^ quote name)
       | ml_from_def (name, Prim prim) =
@@ -643,7 +651,7 @@
                 :: map (ml_from_sortlookup NOBR) lss
               );
             fun from_memdef (m, def) =
-              ((the o ml_from_funs) [(m, Fun def)], Pretty.block [
+              (ml_from_funs [(m, def)], Pretty.block [
                 ml_from_label m,
                 Pretty.brk 1,
                 str "=",
@@ -679,12 +687,22 @@
             ] |> SOME
           end;
   in case defs
-   of (_, Fun _)::_ => ml_from_funs defs
-    | (_, Datatypecons _)::_ => ml_from_datatypes defs
-    | (_, Datatype _)::_ => ml_from_datatypes defs
+   of (_, Fun _)::_ => (SOME o ml_from_funs o map (fn (name, Fun info) => (name, info))) defs
+    | (_, Datatypecons _)::_ => (SOME o ml_from_datatypes o filter_datatype) defs
+    | (_, Datatype _)::_ => (SOME o ml_from_datatypes o filter_datatype) defs
     | [def] => ml_from_def def
   end;
 
+fun ml_annotators (nsp_dtcon, nsp_class, is_int_tyco) =
+  let
+    fun needs_type (IType (tyco, _)) =
+          has_nsp tyco nsp_class
+          orelse is_int_tyco tyco
+      | needs_type _ =
+          false;
+    fun is_cons c = has_nsp c nsp_dtcon;
+  in (is_cons, needs_type) end;
+
 in
 
 fun ml_from_thingol target (nsp_dtcon, nsp_class, is_int_tyco) nspgrp =
@@ -701,12 +719,7 @@
         str "",
         str ("end; (* struct " ^ name ^ " *)")
       ]);
-    fun needs_type (IType (tyco, _)) =
-          has_nsp tyco nsp_class
-          orelse is_int_tyco tyco
-      | needs_type _ =
-          false;
-    fun is_cons c = has_nsp c nsp_dtcon;
+    val (is_cons, needs_type) = ml_annotators (nsp_dtcon, nsp_class, is_int_tyco);
     val serializer = abstract_serializer (target, nspgrp)
       "ROOT" (ml_from_defs (is_cons, needs_type), ml_from_module,
         abstract_validator reserved_ml, snd);
@@ -744,6 +757,9 @@
          (preprocess const_syntax) (class_syntax, tyco_syntax, const_syntax))
   end;
 
+fun ml_fun_datatype (nsp_dtcon, nsp_class, is_int_tyco) =
+  ml_fun_datatyp (ml_annotators (nsp_dtcon, nsp_class, is_int_tyco));
+
 end; (* local *)
 
 local
diff -r 1a8f08f9f8af -r 630b8dd0b31a src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Wed Feb 15 17:09:25 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML	Wed Feb 15 17:09:45 2006 +0100
@@ -45,6 +45,7 @@
   val `|--> : iexpr list * iexpr -> iexpr;
 
   type funn = (iexpr list * iexpr) list * (ClassPackage.sortcontext * itype);
+  type datatyp = (vname * sort) list * (string * itype list) list;
   datatype prim =
       Pretty of Pretty.T
     | Name;
@@ -53,7 +54,7 @@
     | Prim of (string * prim list) list
     | Fun of funn
     | Typesyn of (vname * sort) list * itype
-    | Datatype of (vname * sort) list * (string * itype list) list
+    | Datatype of datatyp
     | Datatypecons of string
     | Class of class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)
     | Classmember of class
@@ -72,6 +73,7 @@
   val ensure_prim: string -> string -> module -> module;
   val get_def: module -> string -> def;
   val merge_module: module * module -> module;
+  val diff_module: module * module -> (string * def) list;
   val partof: string list -> module -> module;
   val has_nsp: string -> string -> bool;
   val succeed: 'a -> transact -> 'a transact_fin;
@@ -379,6 +381,7 @@
 (* type definitions *)
 
 type funn = (iexpr list * iexpr) list * (ClassPackage.sortcontext * itype);
+type datatyp = (vname * sort) list * (string * itype list) list;
 
 datatype prim =
     Pretty of Pretty.T
@@ -389,7 +392,7 @@
   | Prim of (string * prim list) list
   | Fun of funn
   | Typesyn of (vname * sort) list * itype
-  | Datatype of (vname * sort) list * (string * itype list) list
+  | Datatype of datatyp
   | Datatypecons of string
   | Class of class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)
   | Classmember of class
@@ -672,6 +675,23 @@
       | join_module name _ = raise Graph.DUP name
   in Graph.join join_module modl12 end;
 
+fun diff_module modl12 =
+  let
+    fun diff_entry prefix modl2 (name, Def def1) = 
+          let
+            val e2 = try (Graph.get_node modl2) name
+          in if is_some e2 andalso eq_def (def1, (dest_def o the) e2)
+            then I
+            else cons (NameSpace.pack (prefix @ [name]), def1)
+          end
+      | diff_entry prefix modl2 (name, Module modl1) =
+          diff_modl (prefix @ [name]) (modl1,
+            (the_default empty_module o Option.map dest_modl o try (Graph.get_node modl2)) name)
+    and diff_modl prefix (modl1, modl2) =
+      fold (diff_entry prefix modl2)
+        ((AList.make (Graph.get_node modl1) o Library.flat o Graph.strong_conn) modl1)
+  in diff_modl [] modl12 [] end;
+
 fun partof names modl =
   let
     datatype pathnode = PN of (string list * (string * pathnode) list);