minor improvements
authorhaftmann
Fri Feb 03 11:48:11 2006 +0100 (2006-02-03 ago)
changeset 189185590770e1b09
parent 18917 77e18862990f
child 18919 340ffeaaaede
minor improvements
src/Pure/Tools/class_package.ML
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_serializer.ML
src/Pure/Tools/codegen_thingol.ML
     1.1 --- a/src/Pure/Tools/class_package.ML	Fri Feb 03 11:47:57 2006 +0100
     1.2 +++ b/src/Pure/Tools/class_package.ML	Fri Feb 03 11:48:11 2006 +0100
     1.3 @@ -151,7 +151,7 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun gen_add_class add_locale prep_class bname raw_supclasses raw_body thy =
     1.8 +fun gen_add_class add_locale prep_class do_proof bname raw_supclasses raw_body thy =
     1.9    let
    1.10      val supclasses = map (prep_class thy) raw_supclasses;
    1.11      fun get_allcs class =
    1.12 @@ -170,46 +170,39 @@
    1.13                  supclasses;
    1.14      fun mk_c_lookup c_global supcs c_adds =
    1.15        map2 (fn ((c, _), _) => pair c) c_global supcs @ c_adds
    1.16 -    fun extract_assumes v c_lookup elems =
    1.17 -      elems
    1.18 -      |> (map o List.mapPartial)
    1.19 -          (fn (Element.Assumes asms) => (SOME o map (map fst o snd)) asms
    1.20 -            | _ => NONE)
    1.21 -      |> Library.flat o Library.flat o Library.flat
    1.22 +    fun extract_tyvar_consts thy name_locale =
    1.23 +      let
    1.24 +        fun extract_tyvar_name thy tys =
    1.25 +          fold (curry add_typ_tfrees) tys []
    1.26 +          |> (fn [(v, sort)] =>
    1.27 +                    if Sorts.sort_le (Sign.classes_of thy) (swap (sort, supsort))
    1.28 +                    then v 
    1.29 +                    else error ("illegal sort constraint on class type variable: " ^ Sign.string_of_sort thy sort)
    1.30 +               | [] => error ("no class type variable")
    1.31 +               | vs => error ("more than one type variable: " ^ (commas o map (Sign.string_of_typ thy o TFree)) vs))
    1.32 +        val raw_consts =
    1.33 +          Locale.parameters_of thy name_locale
    1.34 +          |> map (apsnd Syntax.unlocalize_mixfix)
    1.35 +          |> ((curry splitAt o length) supcs);
    1.36 +        val v = (extract_tyvar_name thy o map (snd o fst) o op @) raw_consts;
    1.37 +        fun subst_ty cs =
    1.38 +          map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) cs;
    1.39 +        val consts = (subst_ty (fst raw_consts), subst_ty (snd raw_consts));
    1.40 +        val _ = (writeln o commas o map (fst o fst)) (fst consts);
    1.41 +        val _ = (writeln o commas o map (fst o fst)) (snd consts);
    1.42 +      in (v, consts) end;
    1.43 +    fun add_global_const v ((c, ty), syn) thy =
    1.44 +      thy
    1.45 +      |> Sign.add_consts_i [(c, ty |> subst_clsvar v (TFree (v, Sign.defaultS thy)), syn)]
    1.46 +      |> `(fn thy => (c, (Sign.intern_const thy c |> print, ty)))
    1.47 +    fun extract_assumes thy name_locale c_lookup =
    1.48 +      Locale.local_asms_of thy name_locale
    1.49 +      |> map snd
    1.50 +      |> Library.flat
    1.51        |> (map o map_aterms) (fn Free (c, ty) => Const ((fst o the o AList.lookup (op =) c_lookup) c, ty)
    1.52                               | t => t)
    1.53        |> tap (fn ts => writeln ("(1) axclass axioms: " ^
    1.54            (commas o map (Sign.string_of_term thy)) ts));
    1.55 -    fun extract_tyvar_name thy tys =
    1.56 -      fold (curry add_typ_tfrees) tys []
    1.57 -      |> (fn [(v, sort)] =>
    1.58 -                if Sorts.sort_le (Sign.classes_of thy) (swap (sort, supsort))
    1.59 -                then v 
    1.60 -                else error ("illegal sort constraint on class type variable: " ^ Sign.string_of_sort thy sort)
    1.61 -           | [] => error ("no class type variable")
    1.62 -           | vs => error ("more than one type variable: " ^ (commas o map (Sign.string_of_typ thy o TFree)) vs))
    1.63 -    fun extract_tyvar_consts thy (import_elems, body_elems) =
    1.64 -      let
    1.65 -        fun get_elems elems =
    1.66 -          elems
    1.67 -          |> Library.flat
    1.68 -          |> List.mapPartial
    1.69 -               (fn (Element.Fixes consts) => SOME consts
    1.70 -                 | _ => NONE)
    1.71 -          |> Library.flat
    1.72 -          |> map (fn (c, ty, syn) => ((c, the ty), Syntax.unlocalize_mixfix syn))
    1.73 -        val import_consts = get_elems import_elems;
    1.74 -        val body_consts = get_elems body_elems;
    1.75 -        val v = extract_tyvar_name thy (map (snd o fst) (import_consts @ body_consts));
    1.76 -        fun subst_ty cs =
    1.77 -          map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) cs;
    1.78 -        val import_cs = subst_ty import_consts;
    1.79 -        val body_cs = subst_ty body_consts;
    1.80 -      in (v, (import_cs, body_cs)) end;
    1.81 -    fun add_global_const v ((c, ty), syn) thy =
    1.82 -      thy
    1.83 -      |> Sign.add_consts_i [(c, ty |> subst_clsvar v (TFree (v, Sign.defaultS thy)), syn)]
    1.84 -      |> `(fn thy => (c, (Sign.intern_const thy c, ty)))
    1.85      fun add_global_constraint v class (_, (c, ty)) thy =
    1.86        thy
    1.87        |> Sign.add_const_constraint_i (c, subst_clsvar v (TVar ((v, 0), [class])) ty);
    1.88 @@ -217,36 +210,37 @@
    1.89        thy
    1.90        |> Locale.interpretation (NameSpace.base name_locale, [])
    1.91             (Locale.Locale name_locale) (map (SOME o fst) cs)
    1.92 -      |> Proof.global_terminal_proof (Method.Basic (Method.fact ax_axioms), NONE);
    1.93 -    fun print_ctxt ctxt elem = 
    1.94 -      map Pretty.writeln (Element.pretty_ctxt ctxt elem)
    1.95 +      |> do_proof ax_axioms;
    1.96    in
    1.97      thy
    1.98      |> add_locale bname locexpr raw_body
    1.99 -    |-> (fn ((import_elems, body_elems), ctxt) =>
   1.100 +    |-> (fn ctxt =>
   1.101         `(fn thy => Locale.intern thy bname)
   1.102      #-> (fn name_locale =>
   1.103 -          `(fn thy => extract_tyvar_consts thy (import_elems, body_elems))
   1.104 +          `(fn thy => extract_tyvar_consts thy name_locale)
   1.105      #-> (fn (v, (c_global, c_defs)) =>
   1.106            fold_map (add_global_const v) c_defs
   1.107      #-> (fn c_adds =>
   1.108 -          AxClass.add_axclass_i (bname, supsort)
   1.109 -            (map (Thm.no_attributes o pair "") (extract_assumes v (mk_c_lookup c_global supcs c_adds) body_elems))
   1.110 +       `(fn thy => extract_assumes thy name_locale (mk_c_lookup c_global supcs c_adds))
   1.111 +    #-> (fn assumes =>
   1.112 +          AxClass.add_axclass_i (bname, supsort) (map (Thm.no_attributes o pair "") assumes))
   1.113      #-> (fn { axioms = ax_axioms : thm list, ...} =>
   1.114            `(fn thy => Sign.intern_class thy bname)
   1.115      #-> (fn name_axclass =>
   1.116            fold (add_global_constraint v name_axclass) c_adds
   1.117      #> add_class_data (name_locale, (supclasses, name_locale, name_axclass, v, map snd c_adds))
   1.118 -    #> tap (fn _ => (map o map) (print_ctxt ctxt) import_elems)
   1.119 -    #> tap (fn _ => (map o map) (print_ctxt ctxt) body_elems)
   1.120      #> interpret name_locale (supcs @ (map (fn ((c, ty), _) => (Sign.intern_const thy c, ty)) c_defs)) ax_axioms
   1.121      ))))))
   1.122    end;
   1.123  
   1.124  in
   1.125  
   1.126 -val add_class = gen_add_class (Locale.add_locale_context true) intern_class;
   1.127 -val add_class_i = gen_add_class (Locale.add_locale_context_i true) certify_class;
   1.128 +val add_class = gen_add_class (Locale.add_locale true) intern_class
   1.129 +  (fn ax_axioms => Proof.global_terminal_proof (Method.Basic (Method.fact ax_axioms), NONE));
   1.130 +val add_class_i = gen_add_class (Locale.add_locale_i true) certify_class
   1.131 +  (fn ax_axioms => Proof.global_terminal_proof (Method.Basic (Method.fact ax_axioms), NONE));
   1.132 +val add_class_exp = gen_add_class (Locale.add_locale true) intern_class
   1.133 +  (K I);
   1.134  
   1.135  end; (* local *)
   1.136  
   1.137 @@ -271,9 +265,10 @@
   1.138          |> Sign.add_const_constraint_i (c, ty2)
   1.139          |> pair (c, ty1)
   1.140        end;
   1.141 -    fun get_c_given thy = map (fst o dest_def o snd o tap_def thy o fst) raw_defs;
   1.142 -    fun check_defs c_given c_req thy =
   1.143 +    fun check_defs raw_defs c_req thy =
   1.144        let
   1.145 +        val thy' = Sign.add_arities_i [(tyco, asorts, sort)] thy;
   1.146 +        val c_given = map (fst o dest_def o snd o tap_def thy' o fst) raw_defs;
   1.147          fun eq_c ((c1, ty1), (c2, ty2)) = 
   1.148            let
   1.149              val ty1' = Type.varifyT ty1;
   1.150 @@ -297,12 +292,18 @@
   1.151        #> fold (fn class => add_inst_data (class, (tyco, Context.theory_name thy))) sort;
   1.152    in
   1.153      thy
   1.154 +    |> tap (fn thy => check_defs raw_defs c_req thy)
   1.155      |> fold_map get_remove_contraint (map fst c_req)
   1.156 -    ||> tap (fn thy => check_defs (get_c_given thy) c_req thy)
   1.157      ||> add_defs (true, raw_defs)
   1.158      |-> (fn cs => AxClass.instance_arity_i (after_qed cs) arity)
   1.159    end;
   1.160  
   1.161 +val _ : string option ->
   1.162 +    ((string * typ option * mixfix) option * ((string * Attrib.src list) * term)) list ->
   1.163 +    theory -> (term * (bstring * thm)) list * (Proof.context * theory)
   1.164 +  = Specification.definition_i;
   1.165 +
   1.166 +
   1.167  val add_instance_arity = fn x => gen_instance_arity (AxClass.read_arity) IsarThy.add_defs read_axm x;
   1.168  val add_instance_arity_i = fn x => gen_instance_arity (AxClass.cert_arity) IsarThy.add_defs_i (K I) x;
   1.169  
   1.170 @@ -521,6 +522,14 @@
   1.171        >> (Toplevel.theory_context
   1.172            o (fn ((bname, supclasses), elems) => add_class bname supclasses elems)));
   1.173  
   1.174 +val classP_exp =
   1.175 +  OuterSyntax.command (classK ^ "_exp") "operational type classes" K.thy_goal (
   1.176 +    P.name --| P.$$$ "="
   1.177 +    -- Scan.optional (Scan.repeat1 (P.name --| P.$$$ "+")) []
   1.178 +    -- Scan.optional (P.!!! (Scan.repeat1 P.context_element)) []
   1.179 +      >> (Toplevel.theory_to_proof
   1.180 +          o (fn ((bname, supclasses), elems) => add_class_exp bname supclasses elems)));
   1.181 +
   1.182  val instanceP =
   1.183    OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
   1.184        P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> AxClass.instance_subclass
   1.185 @@ -529,7 +538,7 @@
   1.186                  | (inst, defs) => add_instance_arity inst defs)
   1.187      ) >> (Toplevel.print oo Toplevel.theory_to_proof));
   1.188  
   1.189 -val _ = OuterSyntax.add_parsers [classP, instanceP];
   1.190 +val _ = OuterSyntax.add_parsers [classP, classP_exp, instanceP];
   1.191  
   1.192  end; (* local *)
   1.193  
     2.1 --- a/src/Pure/Tools/codegen_package.ML	Fri Feb 03 11:47:57 2006 +0100
     2.2 +++ b/src/Pure/Tools/codegen_package.ML	Fri Feb 03 11:48:11 2006 +0100
     2.3 @@ -505,19 +505,19 @@
     2.4    let
     2.5      fun add_rename (var as ((v, _), sort)) used = 
     2.6        let
     2.7 -        val v' = variant used v
     2.8 +        val v' = "'" ^ variant used (unprefix "'" v)
     2.9        in (((var, TFree (v', sort)), (v', TVar var)), v' :: used) end;
    2.10      fun typ_names (Type (tyco, tys)) (vars, names) =
    2.11            (vars, names |> insert (op =) (NameSpace.base tyco))
    2.12            |> fold typ_names tys
    2.13        | typ_names (TFree (v, _)) (vars, names) =
    2.14 -          (vars, names |> insert (op =) v)
    2.15 -      | typ_names (TVar (v, sort)) (vars, names) =
    2.16 -          (vars |> AList.update (op =) (v, sort), names);
    2.17 +          (vars, names |> insert (op =) (unprefix "'" v))
    2.18 +      | typ_names (TVar (vi, sort)) (vars, names) =
    2.19 +          (vars |> AList.update (op =) (vi, sort), names);
    2.20      val (vars, used) = fold typ_names tys ([], []);
    2.21      val (renames, reverse) = fold_map add_rename vars used |> fst |> split_list;
    2.22    in
    2.23 -    (reverse, (map o map_atyps) (Term.instantiateT renames) tys)
    2.24 +    (reverse, map (Term.instantiateT renames) tys)
    2.25    end;
    2.26  
    2.27  fun burrow_typs_yield f ts =
    2.28 @@ -553,7 +553,7 @@
    2.29      val (vars, used) = fold term_names ts ([], []);
    2.30      val (renames, reverse) = fold_map add_rename vars used |> fst |> split_list;
    2.31    in
    2.32 -    (reverse, (map o map_aterms) (Term.instantiate ([], renames)) ts)
    2.33 +    (reverse, map (Term.instantiate ([], renames)) ts)
    2.34    end;
    2.35  
    2.36  fun devarify_term_typs ts =
     3.1 --- a/src/Pure/Tools/codegen_serializer.ML	Fri Feb 03 11:47:57 2006 +0100
     3.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Fri Feb 03 11:48:11 2006 +0100
     3.3 @@ -404,11 +404,11 @@
     3.4            (case tyco_syntax tyco
     3.5             of NONE =>
     3.6                  let
     3.7 -                  val f' = (str o resolv) tyco
     3.8 +                  val tyco' = (str o resolv) tyco
     3.9                  in case map (ml_from_type BR) tys
    3.10 -                 of [] => f'
    3.11 -                  | [p] => Pretty.block [p, Pretty.brk 1, f']
    3.12 -                  | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, f']
    3.13 +                 of [] => tyco'
    3.14 +                  | [p] => Pretty.block [p, Pretty.brk 1, tyco']
    3.15 +                  | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
    3.16                  end
    3.17              | SOME ((i, k), pr) =>
    3.18                  if not (i <= length tys andalso length tys <= k)
    3.19 @@ -442,8 +442,16 @@
    3.20                  ])
    3.21        | ml_from_expr fxy (e as IConst x) =
    3.22            ml_from_app fxy (x, [])
    3.23 -      | ml_from_expr fxy (IVarE (v, _)) =
    3.24 -          str v
    3.25 +      | ml_from_expr fxy (IVarE (v, ty)) =
    3.26 +          if needs_type ty
    3.27 +            then
    3.28 +              Pretty.enclose "(" ")" [
    3.29 +                str v,
    3.30 +                str ":",
    3.31 +                ml_from_type NOBR ty
    3.32 +              ]
    3.33 +            else
    3.34 +              str v
    3.35        | ml_from_expr fxy (IAbs ((v, _), e)) =
    3.36            brackify fxy [
    3.37              str ("fn " ^ v ^ " =>"),
    3.38 @@ -537,7 +545,7 @@
    3.39      fun ml_from_datatypes defs =
    3.40        let
    3.41          val defs' = List.mapPartial
    3.42 -          (fn (name, Datatype info) => SOME (resolv name, info)
    3.43 +          (fn (name, Datatype info) => SOME (name, info)
    3.44              | (name, Datatypecons _) => NONE
    3.45              | (name, def) => error ("datatype block containing illegal def: "
    3.46                  ^ (Pretty.output o pretty_def) def)
    3.47 @@ -563,7 +571,7 @@
    3.48          case defs'
    3.49           of (def::defs_tl) =>
    3.50              chunk_defs (
    3.51 -              mk_datatype "datatype " def
    3.52 +              mk_datatype "datatype" def
    3.53                :: map (mk_datatype "and ") defs_tl
    3.54              ) |> SOME
    3.55            | _ => NONE
    3.56 @@ -877,7 +885,7 @@
    3.57        | hs_from_def (name, Fun (eqs, (sctxt, ty))) =
    3.58            Pretty.chunks [
    3.59              Pretty.block [
    3.60 -              (str o lower_first o resolv) (name ^ " ::"),
    3.61 +              (str o suffix " ::" o lower_first o resolv) name,
    3.62                Pretty.brk 1,
    3.63                hs_from_sctxt_type (sctxt, ty)
    3.64              ],
     4.1 --- a/src/Pure/Tools/codegen_thingol.ML	Fri Feb 03 11:47:57 2006 +0100
     4.2 +++ b/src/Pure/Tools/codegen_thingol.ML	Fri Feb 03 11:48:11 2006 +0100
     4.3 @@ -1044,27 +1044,20 @@
     4.4            ([], SOME tab)
     4.5        | get_path_name [p] tab =
     4.6            let
     4.7 -            val _ = writeln ("(1) " ^ p);
     4.8              val SOME (N (p', tab')) = Symtab.lookup tab p
     4.9            in ([p'], tab') end
    4.10        | get_path_name [p1, p2] tab =
    4.11 -          let
    4.12 -            val _ = (writeln o prefix "(2) " o NameSpace.pack) [p1, p2];
    4.13 -          in case Symtab.lookup tab p1
    4.14 +          case Symtab.lookup tab p1
    4.15             of SOME (N (p', SOME tab')) => 
    4.16                  let
    4.17 -                  val _ = writeln ("(2) 'twas a module");
    4.18                    val (ps', tab'') = get_path_name [p2] tab'
    4.19                  in (p' :: ps', tab'') end
    4.20              | NONE =>
    4.21                  let
    4.22 -                  val _ = writeln ("(2) 'twas a definition");
    4.23                    val SOME (N (p', NONE)) = Symtab.lookup tab (NameSpace.pack [p1, p2])
    4.24                  in ([p'], NONE) end
    4.25 -          end
    4.26        | get_path_name (p::ps) tab =
    4.27            let
    4.28 -            val _ = (writeln o prefix "(3) " o commas) (p::ps);
    4.29              val SOME (N (p', SOME tab')) = Symtab.lookup tab p
    4.30              val (ps', tab'') = get_path_name ps tab'
    4.31            in (p' :: ps', tab'') end;
    4.32 @@ -1072,107 +1065,18 @@
    4.33        if (is_some o Int.fromString) name
    4.34        then name
    4.35        else let
    4.36 -        val _ = writeln ("(0) prefix: " ^ commas prefix);
    4.37 -        val _ = writeln ("(0) name: " ^ name)
    4.38          val (common, (_, rem)) = get_prefix (op =) (prefix, NameSpace.unpack name);
    4.39 -        val _ = writeln ("(0) common: " ^ commas common);
    4.40 -        val _ = writeln ("(0) rem: " ^ commas rem);
    4.41          val (_, SOME tab') = get_path_name common tab;
    4.42          val (name', _) = get_path_name rem tab';
    4.43        in NameSpace.pack name' end;
    4.44    in deresolv (mk module (AList.make (K NameMangler.empty) nsp_conn) Symtab.empty) end;
    4.45  
    4.46 -val _ : module -> string list list -> (string * string -> string) -> (string -> string option) -> string list -> string -> string = mk_deresolver;
    4.47 -
    4.48 -fun mk_resolvtab' nsp_conn validate module =
    4.49 -  let
    4.50 -    fun validate' n = perhaps validate n;
    4.51 -    fun ensure_unique prfix prfix' name name' (locals, tab) =
    4.52 -      let
    4.53 -        fun uniquify name n =
    4.54 -          let
    4.55 -            val name' = if n = 0 then name else name ^ "_" ^ string_of_int n
    4.56 -          in
    4.57 -            if member (op =) locals name'
    4.58 -            then uniquify name (n+1)
    4.59 -            else case validate name
    4.60 -              of NONE => name'
    4.61 -               | SOME name' => uniquify name' n
    4.62 -          end;
    4.63 -        val name'' = uniquify name' 0;
    4.64 -      in
    4.65 -        (locals, tab)
    4.66 -        |> apsnd (Symtab.update_new
    4.67 -             (NameSpace.pack (prfix @ [name]), NameSpace.pack (prfix' @ [name''])))
    4.68 -        |> apfst (cons name'')
    4.69 -        |> pair name''
    4.70 -      end;
    4.71 -    fun fill_in prfix prfix' node tab =
    4.72 -      let
    4.73 -        val keys = Graph.keys node;
    4.74 -        val nodes = AList.make (Graph.get_node node) keys;
    4.75 -        val (mods, defs) =
    4.76 -          nodes
    4.77 -          |> List.partition (fn (_, Module _) => true | _ => false)
    4.78 -          |> apfst (map (fn (name, Module m) => (name, m)))
    4.79 -          |> apsnd (map fst)
    4.80 -        fun modl_validate (name, modl) (locals, tab) =
    4.81 -          (locals, tab)
    4.82 -          |> ensure_unique prfix prfix' name name
    4.83 -          |-> (fn name' => apsnd (fill_in (prfix @ [name]) (prfix @ [name']) modl))
    4.84 -        fun ensure_unique_sidf sidf =
    4.85 -          let
    4.86 -            val [shallow, name] = NameSpace.unpack sidf;
    4.87 -          in
    4.88 -            nsp_conn
    4.89 -            |> get_first
    4.90 -                (fn grp => if member (op =) grp shallow
    4.91 -                  then grp |> remove (op =) shallow |> SOME else NONE)
    4.92 -            |> these
    4.93 -            |> map (fn s => NameSpace.pack [s, name])
    4.94 -            |> exists (member (op =) defs)
    4.95 -            |> (fn b => if b then sidf else name)
    4.96 -          end;
    4.97 -        fun def_validate sidf (locals, tab) =
    4.98 -          (locals, tab)
    4.99 -          |> ensure_unique prfix prfix' sidf (ensure_unique_sidf sidf)
   4.100 -          |> snd
   4.101 -      in
   4.102 -        ([], tab)
   4.103 -        |> fold modl_validate mods
   4.104 -        |> fold def_validate defs
   4.105 -        |> snd
   4.106 -      end;
   4.107 -  in
   4.108 -    Symtab.empty
   4.109 -    |> fill_in [] [] module
   4.110 -  end;
   4.111 -
   4.112 -fun mk_resolv tab =
   4.113 -  let
   4.114 -    fun resolver modl name =
   4.115 -      if NameSpace.is_qualified name then
   4.116 -        let
   4.117 -          val _ = debug 12 (fn name' => "resolving " ^ quote name ^ " in "
   4.118 -               ^ (quote o NameSpace.pack) modl) ();
   4.119 -          val modl' = if null modl then [] else
   4.120 -            (NameSpace.unpack o the o Symtab.lookup tab o NameSpace.pack) modl;
   4.121 -          val name' = (NameSpace.unpack o the o Symtab.lookup tab) name
   4.122 -        in
   4.123 -          (NameSpace.pack o snd o snd o get_prefix (op =)) (modl', name')
   4.124 -          |> debug 12 (fn name' => "resolving " ^ quote name ^ " to "
   4.125 -               ^ quote name' ^ " in " ^ (quote o NameSpace.pack) modl)
   4.126 -        end
   4.127 -      else name
   4.128 -  in resolver end;
   4.129 -
   4.130  
   4.131  (* serialization *)
   4.132  
   4.133  fun serialize seri_defs seri_module validate nsp_conn name_root module =
   4.134    let
   4.135      val resolver = mk_deresolver module nsp_conn snd validate;
   4.136 -(*     val resolver = mk_resolv (mk_resolvtab' nsp_conn validate module);  *)
   4.137      fun mk_name prfx name =
   4.138        let
   4.139          val name_qual = NameSpace.pack (prfx @ [name])