src/Tools/Code/code_ml.ML
changeset 55147 bce3dbc11f95
parent 55145 2bb3cd36bcf7
child 55150 0940309ed8f1
     1.1 --- a/src/Tools/Code/code_ml.ML	Sat Jan 25 23:50:49 2014 +0100
     1.2 +++ b/src/Tools/Code/code_ml.ML	Sat Jan 25 23:50:49 2014 +0100
     1.3 @@ -28,17 +28,17 @@
     1.4  
     1.5  datatype ml_binding =
     1.6      ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
     1.7 -  | ML_Instance of string * { class: string, tyco: string, vs: (vname * sort) list,
     1.8 -        superinsts: (class * (string * (string * dict list list))) list,
     1.9 +  | ML_Instance of (string * class) * { class: class, tyco: string, vs: (vname * sort) list,
    1.10 +        superinsts: (class * dict list list) list,
    1.11          inst_params: ((string * (const * int)) * (thm * bool)) list,
    1.12          superinst_params: ((string * (const * int)) * (thm * bool)) list };
    1.13  
    1.14  datatype ml_stmt =
    1.15      ML_Exc of string * (typscheme * int)
    1.16    | ML_Val of ml_binding
    1.17 -  | ML_Funs of ml_binding list * string list
    1.18 +  | ML_Funs of ml_binding list * Code_Symbol.symbol list
    1.19    | ML_Datas of (string * (vname list * ((string * vname list) * itype list) list)) list
    1.20 -  | ML_Class of string * (vname * ((class * string) list * (string * itype) list));
    1.21 +  | ML_Class of string * (vname * ((class * class) list * (string * itype) list));
    1.22  
    1.23  fun print_product _ [] = NONE
    1.24    | print_product print [x] = SOME (print x)
    1.25 @@ -53,30 +53,35 @@
    1.26  
    1.27  fun print_sml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
    1.28    let
    1.29 -    fun print_tyco_expr (tyco, []) = (str o deresolve) tyco
    1.30 -      | print_tyco_expr (tyco, [ty]) =
    1.31 -          concat [print_typ BR ty, (str o deresolve) tyco]
    1.32 -      | print_tyco_expr (tyco, tys) =
    1.33 -          concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
    1.34 +    val deresolve_const = deresolve o Code_Symbol.Constant;
    1.35 +    val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
    1.36 +    val deresolve_class = deresolve o Code_Symbol.Type_Class;
    1.37 +    val deresolve_classrel = deresolve o Code_Symbol.Class_Relation;
    1.38 +    val deresolve_inst = deresolve o Code_Symbol.Class_Instance;
    1.39 +    fun print_tyco_expr (sym, []) = (str o deresolve) sym
    1.40 +      | print_tyco_expr (sym, [ty]) =
    1.41 +          concat [print_typ BR ty, (str o deresolve) sym]
    1.42 +      | print_tyco_expr (sym, tys) =
    1.43 +          concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
    1.44      and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
    1.45 -         of NONE => print_tyco_expr (tyco, tys)
    1.46 +         of NONE => print_tyco_expr (Code_Symbol.Type_Constructor tyco, tys)
    1.47            | SOME (_, print) => print print_typ fxy tys)
    1.48        | print_typ fxy (ITyVar v) = str ("'" ^ v);
    1.49 -    fun print_dicttyp (class, ty) = print_tyco_expr (class, [ty]);
    1.50 +    fun print_dicttyp (class, ty) = print_tyco_expr (Code_Symbol.Type_Class class, [ty]);
    1.51      fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
    1.52        (map_filter (fn (v, sort) =>
    1.53          (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
    1.54      fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
    1.55      fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
    1.56      fun print_classrels fxy [] ps = brackify fxy ps
    1.57 -      | print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve) classrel, brackify BR ps]
    1.58 +      | print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve_classrel) classrel, brackify BR ps]
    1.59        | print_classrels fxy classrels ps =
    1.60 -          brackify fxy [enum " o" "(" ")" (map (str o deresolve) classrels), brackify BR ps]
    1.61 +          brackify fxy [enum " o" "(" ")" (map (str o deresolve_classrel) classrels), brackify BR ps]
    1.62      fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
    1.63        print_classrels fxy classrels (print_plain_dict is_pseudo_fun fxy x)
    1.64      and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
    1.65 -          ((str o deresolve) inst ::
    1.66 -            (if is_pseudo_fun inst then [str "()"]
    1.67 +          ((str o deresolve_inst) inst ::
    1.68 +            (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
    1.69              else map_filter (print_dicts is_pseudo_fun BR) dss))
    1.70        | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
    1.71            [str (if k = 1 then first_upper v ^ "_"
    1.72 @@ -105,21 +110,22 @@
    1.73            in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
    1.74        | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
    1.75            (case Code_Thingol.unfold_const_app (#primitive case_expr)
    1.76 -           of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
    1.77 +           of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
    1.78 +                if is_none (const_syntax const)
    1.79                  then print_case is_pseudo_fun some_thm vars fxy case_expr
    1.80                  else print_app is_pseudo_fun some_thm vars fxy app
    1.81              | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
    1.82 -    and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
    1.83 -      if is_constr c then
    1.84 +    and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) =
    1.85 +      if is_constr sym then
    1.86          let val k = length dom in
    1.87            if k < 2 orelse length ts = k
    1.88 -          then (str o deresolve) c
    1.89 +          then (str o deresolve) sym
    1.90              :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
    1.91            else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
    1.92          end
    1.93 -      else if is_pseudo_fun c
    1.94 -        then (str o deresolve) c @@ str "()"
    1.95 -      else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss
    1.96 +      else if is_pseudo_fun sym
    1.97 +        then (str o deresolve) sym @@ str "()"
    1.98 +      else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss
    1.99          @ map (print_term is_pseudo_fun some_thm vars BR) ts
   1.100      and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
   1.101        (print_term is_pseudo_fun) const_syntax some_thm vars
   1.102 @@ -158,23 +164,23 @@
   1.103                :: map (print_select "|") clauses
   1.104              )
   1.105            end;
   1.106 -    fun print_val_decl print_typscheme (name, typscheme) = concat
   1.107 -      [str "val", str (deresolve name), str ":", print_typscheme typscheme];
   1.108 +    fun print_val_decl print_typscheme (sym, typscheme) = concat
   1.109 +      [str "val", str (deresolve sym), str ":", print_typscheme typscheme];
   1.110      fun print_datatype_decl definer (tyco, (vs, cos)) =
   1.111        let
   1.112 -        fun print_co ((co, _), []) = str (deresolve co)
   1.113 -          | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
   1.114 +        fun print_co ((co, _), []) = str (deresolve_const co)
   1.115 +          | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of",
   1.116                enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
   1.117        in
   1.118          concat (
   1.119            str definer
   1.120 -          :: print_tyco_expr (tyco, map ITyVar vs)
   1.121 +          :: print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs)
   1.122            :: str "="
   1.123            :: separate (str "|") (map print_co cos)
   1.124          )
   1.125        end;
   1.126      fun print_def is_pseudo_fun needs_typ definer
   1.127 -          (ML_Function (name, (vs_ty as (vs, ty), eq :: eqs))) =
   1.128 +          (ML_Function (const, (vs_ty as (vs, ty), eq :: eqs))) =
   1.129            let
   1.130              fun print_eqn definer ((ts, t), (some_thm, _)) =
   1.131                let
   1.132 @@ -184,12 +190,12 @@
   1.133                    |> intro_vars ((fold o Code_Thingol.fold_varnames)
   1.134                         (insert (op =)) ts []);
   1.135                  val prolog = if needs_typ then
   1.136 -                  concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty]
   1.137 -                    else (concat o map str) [definer, deresolve name];
   1.138 +                  concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty]
   1.139 +                    else (concat o map str) [definer, deresolve_const const];
   1.140                in
   1.141                  concat (
   1.142                    prolog
   1.143 -                  :: (if is_pseudo_fun name then [str "()"]
   1.144 +                  :: (if is_pseudo_fun (Code_Symbol.Constant const) then [str "()"]
   1.145                        else print_dict_args vs
   1.146                          @ map (print_term is_pseudo_fun some_thm vars BR) ts)
   1.147                    @ str "="
   1.148 @@ -199,53 +205,53 @@
   1.149              val shift = if null eqs then I else
   1.150                map (Pretty.block o single o Pretty.block o single);
   1.151            in pair
   1.152 -            (print_val_decl print_typscheme (name, vs_ty))
   1.153 +            (print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty))
   1.154              ((Pretty.block o Pretty.fbreaks o shift) (
   1.155                print_eqn definer eq
   1.156                :: map (print_eqn "|") eqs
   1.157              ))
   1.158            end
   1.159        | print_def is_pseudo_fun _ definer
   1.160 -          (ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) =
   1.161 +          (ML_Instance (inst as (tyco, class), { vs, superinsts, inst_params, ... })) =
   1.162            let
   1.163 -            fun print_super_instance (_, (classrel, x)) =
   1.164 +            fun print_super_instance (super_class, x) =
   1.165                concat [
   1.166 -                (str o Long_Name.base_name o deresolve) classrel,
   1.167 +                (str o Long_Name.base_name o deresolve_classrel) (class, super_class),
   1.168                  str "=",
   1.169 -                print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))
   1.170 +                print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), x)))
   1.171                ];
   1.172              fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
   1.173                concat [
   1.174 -                (str o Long_Name.base_name o deresolve) classparam,
   1.175 +                (str o Long_Name.base_name o deresolve_const) classparam,
   1.176                  str "=",
   1.177                  print_app (K false) (SOME thm) reserved NOBR (const, [])
   1.178                ];
   1.179            in pair
   1.180              (print_val_decl print_dicttypscheme
   1.181 -              (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
   1.182 +              (Code_Symbol.Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
   1.183              (concat (
   1.184                str definer
   1.185 -              :: (str o deresolve) inst
   1.186 -              :: (if is_pseudo_fun inst then [str "()"]
   1.187 +              :: (str o deresolve_inst) inst
   1.188 +              :: (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
   1.189                    else print_dict_args vs)
   1.190                @ str "="
   1.191                :: enum "," "{" "}"
   1.192                  (map print_super_instance superinsts
   1.193                    @ map print_classparam_instance inst_params)
   1.194                :: str ":"
   1.195 -              @@ print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
   1.196 +              @@ print_dicttyp (class, tyco `%% map (ITyVar o fst) vs)
   1.197              ))
   1.198            end;
   1.199 -    fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
   1.200 -          [print_val_decl print_typscheme (name, vs_ty)]
   1.201 +    fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair
   1.202 +          [print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty)]
   1.203            ((semicolon o map str) (
   1.204              (if n = 0 then "val" else "fun")
   1.205 -            :: deresolve name
   1.206 +            :: deresolve_const const
   1.207              :: replicate n "_"
   1.208              @ "="
   1.209              :: "raise"
   1.210              :: "Fail"
   1.211 -            @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name
   1.212 +            @@ ML_Syntax.print_string const
   1.213            ))
   1.214        | print_stmt (ML_Val binding) =
   1.215            let
   1.216 @@ -257,11 +263,11 @@
   1.217        | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
   1.218            let
   1.219              val print_def' = print_def (member (op =) pseudo_funs) false;
   1.220 -            fun print_pseudo_fun name = concat [
   1.221 +            fun print_pseudo_fun sym = concat [
   1.222                  str "val",
   1.223 -                (str o deresolve) name,
   1.224 +                (str o deresolve) sym,
   1.225                  str "=",
   1.226 -                (str o deresolve) name,
   1.227 +                (str o deresolve) sym,
   1.228                  str "();"
   1.229                ];
   1.230              val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
   1.231 @@ -273,7 +279,7 @@
   1.232            end
   1.233       | print_stmt (ML_Datas [(tyco, (vs, []))]) =
   1.234            let
   1.235 -            val ty_p = print_tyco_expr (tyco, map ITyVar vs);
   1.236 +            val ty_p = print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs);
   1.237            in
   1.238              pair
   1.239              [concat [str "type", ty_p]]
   1.240 @@ -288,42 +294,42 @@
   1.241              sig_ps
   1.242              (Pretty.chunks (ps @| semicolon [p]))
   1.243            end
   1.244 -     | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
   1.245 +     | print_stmt (ML_Class (class, (v, (classrels, classparams)))) =
   1.246            let
   1.247              fun print_field s p = concat [str s, str ":", p];
   1.248              fun print_proj s p = semicolon
   1.249                (map str ["val", s, "=", "#" ^ s, ":"] @| p);
   1.250 -            fun print_super_class_decl (super_class, classrel) =
   1.251 +            fun print_super_class_decl (classrel as (_, super_class)) =
   1.252                print_val_decl print_dicttypscheme
   1.253 -                (classrel, ([(v, [class])], (super_class, ITyVar v)));
   1.254 -            fun print_super_class_field (super_class, classrel) =
   1.255 -              print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v));
   1.256 -            fun print_super_class_proj (super_class, classrel) =
   1.257 -              print_proj (deresolve classrel)
   1.258 +                (Code_Symbol.Class_Relation classrel, ([(v, [class])], (super_class, ITyVar v)));
   1.259 +            fun print_super_class_field (classrel as (_, super_class)) =
   1.260 +              print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v));
   1.261 +            fun print_super_class_proj (classrel as (_, super_class)) =
   1.262 +              print_proj (deresolve_classrel classrel)
   1.263                  (print_dicttypscheme ([(v, [class])], (super_class, ITyVar v)));
   1.264              fun print_classparam_decl (classparam, ty) =
   1.265                print_val_decl print_typscheme
   1.266 -                (classparam, ([(v, [class])], ty));
   1.267 +                (Code_Symbol.Constant classparam, ([(v, [class])], ty));
   1.268              fun print_classparam_field (classparam, ty) =
   1.269 -              print_field (deresolve classparam) (print_typ NOBR ty);
   1.270 +              print_field (deresolve_const classparam) (print_typ NOBR ty);
   1.271              fun print_classparam_proj (classparam, ty) =
   1.272 -              print_proj (deresolve classparam)
   1.273 +              print_proj (deresolve_const classparam)
   1.274                  (print_typscheme ([(v, [class])], ty));
   1.275            in pair
   1.276              (concat [str "type", print_dicttyp (class, ITyVar v)]
   1.277 -              :: map print_super_class_decl super_classes
   1.278 +              :: map print_super_class_decl classrels
   1.279                @ map print_classparam_decl classparams)
   1.280              (Pretty.chunks (
   1.281                concat [
   1.282                  str ("type '" ^ v),
   1.283 -                (str o deresolve) class,
   1.284 +                (str o deresolve_class) class,
   1.285                  str "=",
   1.286                  enum "," "{" "};" (
   1.287 -                  map print_super_class_field super_classes
   1.288 +                  map print_super_class_field classrels
   1.289                    @ map print_classparam_field classparams
   1.290                  )
   1.291                ]
   1.292 -              :: map print_super_class_proj super_classes
   1.293 +              :: map print_super_class_proj classrels
   1.294                @ map print_classparam_proj classparams
   1.295              ))
   1.296            end;
   1.297 @@ -353,29 +359,34 @@
   1.298  
   1.299  fun print_ocaml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
   1.300    let
   1.301 -    fun print_tyco_expr (tyco, []) = (str o deresolve) tyco
   1.302 -      | print_tyco_expr (tyco, [ty]) =
   1.303 -          concat [print_typ BR ty, (str o deresolve) tyco]
   1.304 -      | print_tyco_expr (tyco, tys) =
   1.305 -          concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
   1.306 +    val deresolve_const = deresolve o Code_Symbol.Constant;
   1.307 +    val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
   1.308 +    val deresolve_class = deresolve o Code_Symbol.Type_Class;
   1.309 +    val deresolve_classrel = deresolve o Code_Symbol.Class_Relation;
   1.310 +    val deresolve_inst = deresolve o Code_Symbol.Class_Instance;
   1.311 +    fun print_tyco_expr (sym, []) = (str o deresolve) sym
   1.312 +      | print_tyco_expr (sym, [ty]) =
   1.313 +          concat [print_typ BR ty, (str o deresolve) sym]
   1.314 +      | print_tyco_expr (sym, tys) =
   1.315 +          concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
   1.316      and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
   1.317 -         of NONE => print_tyco_expr (tyco, tys)
   1.318 +         of NONE => print_tyco_expr (Code_Symbol.Type_Constructor tyco, tys)
   1.319            | SOME (_, print) => print print_typ fxy tys)
   1.320        | print_typ fxy (ITyVar v) = str ("'" ^ v);
   1.321 -    fun print_dicttyp (class, ty) = print_tyco_expr (class, [ty]);
   1.322 +    fun print_dicttyp (class, ty) = print_tyco_expr (Code_Symbol.Type_Class class, [ty]);
   1.323      fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
   1.324        (map_filter (fn (v, sort) =>
   1.325          (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
   1.326      fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
   1.327      fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
   1.328      val print_classrels =
   1.329 -      fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve) classrel])
   1.330 +      fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve_classrel) classrel])
   1.331      fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
   1.332        print_plain_dict is_pseudo_fun fxy x
   1.333        |> print_classrels classrels
   1.334      and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
   1.335 -          brackify BR ((str o deresolve) inst ::
   1.336 -            (if is_pseudo_fun inst then [str "()"]
   1.337 +          brackify BR ((str o deresolve_inst) inst ::
   1.338 +            (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
   1.339              else map_filter (print_dicts is_pseudo_fun BR) dss))
   1.340        | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
   1.341            str (if k = 1 then "_" ^ first_upper v
   1.342 @@ -401,21 +412,22 @@
   1.343            in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
   1.344        | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
   1.345            (case Code_Thingol.unfold_const_app (#primitive case_expr)
   1.346 -           of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
   1.347 +           of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
   1.348 +                if is_none (const_syntax const)
   1.349                  then print_case is_pseudo_fun some_thm vars fxy case_expr
   1.350                  else print_app is_pseudo_fun some_thm vars fxy app
   1.351              | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
   1.352 -    and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
   1.353 -      if is_constr c then
   1.354 +    and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) =
   1.355 +      if is_constr sym then
   1.356          let val k = length dom in
   1.357            if length ts = k
   1.358 -          then (str o deresolve) c
   1.359 +          then (str o deresolve) sym
   1.360              :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
   1.361            else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
   1.362          end
   1.363 -      else if is_pseudo_fun c
   1.364 -        then (str o deresolve) c @@ str "()"
   1.365 -      else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss
   1.366 +      else if is_pseudo_fun sym
   1.367 +        then (str o deresolve) sym @@ str "()"
   1.368 +      else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss
   1.369          @ map (print_term is_pseudo_fun some_thm vars BR) ts
   1.370      and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
   1.371        (print_term is_pseudo_fun) const_syntax some_thm vars
   1.372 @@ -449,23 +461,23 @@
   1.373                :: map (print_select "|") clauses
   1.374              )
   1.375            end;
   1.376 -    fun print_val_decl print_typscheme (name, typscheme) = concat
   1.377 -      [str "val", str (deresolve name), str ":", print_typscheme typscheme];
   1.378 +    fun print_val_decl print_typscheme (sym, typscheme) = concat
   1.379 +      [str "val", str (deresolve sym), str ":", print_typscheme typscheme];
   1.380      fun print_datatype_decl definer (tyco, (vs, cos)) =
   1.381        let
   1.382 -        fun print_co ((co, _), []) = str (deresolve co)
   1.383 -          | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
   1.384 +        fun print_co ((co, _), []) = str (deresolve_const co)
   1.385 +          | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of",
   1.386                enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
   1.387        in
   1.388          concat (
   1.389            str definer
   1.390 -          :: print_tyco_expr (tyco, map ITyVar vs)
   1.391 +          :: print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs)
   1.392            :: str "="
   1.393            :: separate (str "|") (map print_co cos)
   1.394          )
   1.395        end;
   1.396      fun print_def is_pseudo_fun needs_typ definer
   1.397 -          (ML_Function (name, (vs_ty as (vs, ty), eqs))) =
   1.398 +          (ML_Function (const, (vs_ty as (vs, ty), eqs))) =
   1.399            let
   1.400              fun print_eqn ((ts, t), (some_thm, _)) =
   1.401                let
   1.402 @@ -529,57 +541,57 @@
   1.403                      )
   1.404                    end;
   1.405              val prolog = if needs_typ then
   1.406 -              concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty]
   1.407 -                else (concat o map str) [definer, deresolve name];
   1.408 +              concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty]
   1.409 +                else (concat o map str) [definer, deresolve_const const];
   1.410            in pair
   1.411 -            (print_val_decl print_typscheme (name, vs_ty))
   1.412 +            (print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty))
   1.413              (concat (
   1.414                prolog
   1.415                :: print_dict_args vs
   1.416 -              @| print_eqns (is_pseudo_fun name) eqs
   1.417 +              @| print_eqns (is_pseudo_fun (Code_Symbol.Constant const)) eqs
   1.418              ))
   1.419            end
   1.420        | print_def is_pseudo_fun _ definer
   1.421 -          (ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) =
   1.422 +          (ML_Instance (inst as (tyco, class), { vs, superinsts, inst_params, ... })) =
   1.423            let
   1.424 -            fun print_super_instance (_, (classrel, x)) =
   1.425 +            fun print_super_instance (super_class, x) =
   1.426                concat [
   1.427 -                (str o deresolve) classrel,
   1.428 +                (str o deresolve_classrel) (class, super_class),
   1.429                  str "=",
   1.430 -                print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))
   1.431 +                print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), x)))
   1.432                ];
   1.433              fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
   1.434                concat [
   1.435 -                (str o deresolve) classparam,
   1.436 +                (str o deresolve_const) classparam,
   1.437                  str "=",
   1.438                  print_app (K false) (SOME thm) reserved NOBR (const, [])
   1.439                ];
   1.440            in pair
   1.441              (print_val_decl print_dicttypscheme
   1.442 -              (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
   1.443 +              (Code_Symbol.Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
   1.444              (concat (
   1.445                str definer
   1.446 -              :: (str o deresolve) inst
   1.447 -              :: (if is_pseudo_fun inst then [str "()"]
   1.448 +              :: (str o deresolve_inst) inst
   1.449 +              :: (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
   1.450                    else print_dict_args vs)
   1.451                @ str "="
   1.452                @@ brackets [
   1.453                  enum_default "()" ";" "{" "}" (map print_super_instance superinsts
   1.454                    @ map print_classparam_instance inst_params),
   1.455                  str ":",
   1.456 -                print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
   1.457 +                print_dicttyp (class, tyco `%% map (ITyVar o fst) vs)
   1.458                ]
   1.459              ))
   1.460            end;
   1.461 -     fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
   1.462 -          [print_val_decl print_typscheme (name, vs_ty)]
   1.463 +     fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair
   1.464 +          [print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty)]
   1.465            ((doublesemicolon o map str) (
   1.466              "let"
   1.467 -            :: deresolve name
   1.468 +            :: deresolve_const const
   1.469              :: replicate n "_"
   1.470              @ "="
   1.471              :: "failwith"
   1.472 -            @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name
   1.473 +            @@ ML_Syntax.print_string const
   1.474            ))
   1.475        | print_stmt (ML_Val binding) =
   1.476            let
   1.477 @@ -591,11 +603,11 @@
   1.478        | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
   1.479            let
   1.480              val print_def' = print_def (member (op =) pseudo_funs) false;
   1.481 -            fun print_pseudo_fun name = concat [
   1.482 +            fun print_pseudo_fun sym = concat [
   1.483                  str "let",
   1.484 -                (str o deresolve) name,
   1.485 +                (str o deresolve) sym,
   1.486                  str "=",
   1.487 -                (str o deresolve) name,
   1.488 +                (str o deresolve) sym,
   1.489                  str "();;"
   1.490                ];
   1.491              val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
   1.492 @@ -607,7 +619,7 @@
   1.493            end
   1.494       | print_stmt (ML_Datas [(tyco, (vs, []))]) =
   1.495            let
   1.496 -            val ty_p = print_tyco_expr (tyco, map ITyVar vs);
   1.497 +            val ty_p = print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs);
   1.498            in
   1.499              pair
   1.500              [concat [str "type", ty_p]]
   1.501 @@ -622,26 +634,26 @@
   1.502              sig_ps
   1.503              (Pretty.chunks (ps @| doublesemicolon [p]))
   1.504            end
   1.505 -     | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
   1.506 +     | print_stmt (ML_Class (class, (v, (classrels, classparams)))) =
   1.507            let
   1.508              fun print_field s p = concat [str s, str ":", p];
   1.509 -            fun print_super_class_field (super_class, classrel) =
   1.510 -              print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v));
   1.511 +            fun print_super_class_field (classrel as (_, super_class)) =
   1.512 +              print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v));
   1.513              fun print_classparam_decl (classparam, ty) =
   1.514                print_val_decl print_typscheme
   1.515 -                (classparam, ([(v, [class])], ty));
   1.516 +                (Code_Symbol.Constant classparam, ([(v, [class])], ty));
   1.517              fun print_classparam_field (classparam, ty) =
   1.518 -              print_field (deresolve classparam) (print_typ NOBR ty);
   1.519 +              print_field (deresolve_const classparam) (print_typ NOBR ty);
   1.520              val w = "_" ^ first_upper v;
   1.521              fun print_classparam_proj (classparam, _) =
   1.522 -              (concat o map str) ["let", deresolve classparam, w, "=",
   1.523 -                w ^ "." ^ deresolve classparam ^ ";;"];
   1.524 +              (concat o map str) ["let", deresolve_const classparam, w, "=",
   1.525 +                w ^ "." ^ deresolve_const classparam ^ ";;"];
   1.526              val type_decl_p = concat [
   1.527                  str ("type '" ^ v),
   1.528 -                (str o deresolve) class,
   1.529 +                (str o deresolve_class) class,
   1.530                  str "=",
   1.531                  enum_default "unit" ";" "{" "}" (
   1.532 -                  map print_super_class_field super_classes
   1.533 +                  map print_super_class_field classrels
   1.534                    @ map print_classparam_field classparams
   1.535                  )
   1.536                ];
   1.537 @@ -694,7 +706,7 @@
   1.538  
   1.539  (** SML/OCaml generic part **)
   1.540  
   1.541 -fun ml_program_of_program ctxt symbol_of module_name reserved identifiers program =
   1.542 +fun ml_program_of_program ctxt module_name reserved identifiers program =
   1.543    let
   1.544      fun namify_const upper base (nsp_const, nsp_type) =
   1.545        let
   1.546 @@ -712,76 +724,76 @@
   1.547        | namify_stmt (Code_Thingol.Classrel _) = namify_const false
   1.548        | namify_stmt (Code_Thingol.Classparam _) = namify_const false
   1.549        | namify_stmt (Code_Thingol.Classinst _) = namify_const false;
   1.550 -    fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, ((tysm as (vs, ty), raw_eqs), _))) =
   1.551 +    fun ml_binding_of_stmt (sym as Code_Symbol.Constant const, Code_Thingol.Fun ((tysm as (vs, ty), raw_eqs), _)) =
   1.552            let
   1.553              val eqs = filter (snd o snd) raw_eqs;
   1.554 -            val (eqs', some_value_name) = if null (filter_out (null o snd) vs) then case eqs
   1.555 +            val (eqs', some_sym) = if null (filter_out (null o snd) vs) then case eqs
   1.556                 of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
   1.557                    then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE)
   1.558 -                  else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name))
   1.559 +                  else (eqs, SOME (sym, member (op =) (Code_Thingol.add_constsyms t []) sym))
   1.560                  | _ => (eqs, NONE)
   1.561                else (eqs, NONE)
   1.562 -          in (ML_Function (name, (tysm, eqs')), some_value_name) end
   1.563 -      | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as { vs, ... })) =
   1.564 -          (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
   1.565 -      | ml_binding_of_stmt (name, _) =
   1.566 +          in (ML_Function (const, (tysm, eqs')), some_sym) end
   1.567 +      | ml_binding_of_stmt (sym as Code_Symbol.Class_Instance inst, Code_Thingol.Classinst (stmt as { vs, ... })) =
   1.568 +          (ML_Instance (inst, stmt), if forall (null o snd) vs then SOME (sym, false) else NONE)
   1.569 +      | ml_binding_of_stmt (sym, _) =
   1.570            error ("Binding block containing illegal statement: " ^ 
   1.571 -            (Code_Symbol.quote_symbol ctxt o symbol_of) name)
   1.572 -    fun modify_fun (name, stmt) =
   1.573 +            Code_Symbol.quote ctxt sym)
   1.574 +    fun modify_fun (sym, stmt) =
   1.575        let
   1.576 -        val (binding, some_value_name) = ml_binding_of_stmt (name, stmt);
   1.577 +        val (binding, some_value_sym) = ml_binding_of_stmt (sym, stmt);
   1.578          val ml_stmt = case binding
   1.579 -         of ML_Function (name, ((vs, ty), [])) =>
   1.580 -              ML_Exc (name, ((vs, ty),
   1.581 +         of ML_Function (const, ((vs, ty), [])) =>
   1.582 +              ML_Exc (const, ((vs, ty),
   1.583                  (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty))
   1.584 -          | _ => case some_value_name
   1.585 +          | _ => case some_value_sym
   1.586               of NONE => ML_Funs ([binding], [])
   1.587 -              | SOME (name, true) => ML_Funs ([binding], [name])
   1.588 -              | SOME (name, false) => ML_Val binding
   1.589 +              | SOME (sym, true) => ML_Funs ([binding], [sym])
   1.590 +              | SOME (sym, false) => ML_Val binding
   1.591        in SOME ml_stmt end;
   1.592      fun modify_funs stmts = single (SOME
   1.593        (ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))
   1.594      fun modify_datatypes stmts = single (SOME
   1.595        (ML_Datas (map_filter
   1.596 -        (fn (name, Code_Thingol.Datatype (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts)))
   1.597 +        (fn (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype stmt) => SOME (tyco, stmt) | _ => NONE) stmts)))
   1.598      fun modify_class stmts = single (SOME
   1.599        (ML_Class (the_single (map_filter
   1.600 -        (fn (name, Code_Thingol.Class (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts))))
   1.601 +        (fn (Code_Symbol.Type_Class class, Code_Thingol.Class stmt) => SOME (class, stmt) | _ => NONE) stmts))))
   1.602      fun modify_stmts ([stmt as (_, stmt' as Code_Thingol.Fun _)]) =
   1.603            if Code_Thingol.is_case stmt' then [] else [modify_fun stmt]
   1.604 -      | modify_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
   1.605 +      | modify_stmts ((stmts as (_, Code_Thingol.Fun _) :: _)) =
   1.606            modify_funs (filter_out (Code_Thingol.is_case o snd) stmts)
   1.607 -      | modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =
   1.608 +      | modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _) :: _)) =
   1.609            modify_datatypes stmts
   1.610 -      | modify_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) =
   1.611 +      | modify_stmts ((stmts as (_, Code_Thingol.Datatype _) :: _)) =
   1.612            modify_datatypes stmts
   1.613 -      | modify_stmts ((stmts as (_, Code_Thingol.Class _)::_)) =
   1.614 +      | modify_stmts ((stmts as (_, Code_Thingol.Class _) :: _)) =
   1.615            modify_class stmts
   1.616 -      | modify_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) =
   1.617 +      | modify_stmts ((stmts as (_, Code_Thingol.Classrel _) :: _)) =
   1.618            modify_class stmts
   1.619 -      | modify_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =
   1.620 +      | modify_stmts ((stmts as (_, Code_Thingol.Classparam _) :: _)) =
   1.621            modify_class stmts
   1.622        | modify_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =
   1.623            [modify_fun stmt]
   1.624 -      | modify_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
   1.625 +      | modify_stmts ((stmts as (_, Code_Thingol.Classinst _) :: _)) =
   1.626            modify_funs stmts
   1.627        | modify_stmts stmts = error ("Illegal mutual dependencies: " ^
   1.628 -          (Library.commas o map (Code_Symbol.quote_symbol ctxt o symbol_of o fst)) stmts);
   1.629 +          (Library.commas o map (Code_Symbol.quote ctxt o fst)) stmts);
   1.630    in
   1.631 -    Code_Namespace.hierarchical_program ctxt symbol_of {
   1.632 +    Code_Namespace.hierarchical_program ctxt {
   1.633        module_name = module_name, reserved = reserved, identifiers = identifiers,
   1.634        empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt,
   1.635        cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
   1.636    end;
   1.637  
   1.638  fun serialize_ml print_ml_module print_ml_stmt with_signatures ctxt
   1.639 -    { symbol_of, module_name, reserved_syms, identifiers, includes,
   1.640 +    { module_name, reserved_syms, identifiers, includes,
   1.641        class_syntax, tyco_syntax, const_syntax } program =
   1.642    let
   1.643  
   1.644      (* build program *)
   1.645      val { deresolver, hierarchical_program = ml_program } =
   1.646 -      ml_program_of_program ctxt symbol_of module_name (Name.make_context reserved_syms) identifiers program;
   1.647 +      ml_program_of_program ctxt module_name (Name.make_context reserved_syms) identifiers program;
   1.648  
   1.649      (* print statements *)
   1.650      fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt
   1.651 @@ -803,7 +815,7 @@
   1.652          lift_markup = apsnd } ml_program));
   1.653      fun write width NONE = writeln o format [] width
   1.654        | write width (SOME p) = File.write p o format [] width;
   1.655 -    fun prepare names width p = ([("", format names width p)], try (deresolver []));
   1.656 +    fun prepare syms width p = ([("", format syms width p)], try (deresolver []));
   1.657    in
   1.658      Code_Target.serialization write prepare p
   1.659    end;