src/Tools/Code/code_ml.ML

 end;
 
 structure Code_ML : CODE_ML =
 struct
 
+open Basic_Code_Symbol;
 open Basic_Code_Thingol;
 open Code_Printer;
 
 infixr 5 @@;
 infixr 5 @|;

         superinst_params: ((string * (const * int)) * (thm * bool)) list };
 
 datatype ml_stmt =
     ML_Exc of string * (typscheme * int)
   | ML_Val of ml_binding
-  | ML_Funs of ml_binding list * Code_Symbol.symbol list
+  | ML_Funs of ml_binding list * Code_Symbol.T list
   | ML_Datas of (string * (vname list * ((string * vname list) * itype list) list)) list
   | ML_Class of string * (vname * ((class * class) list * (string * itype) list));
 
 fun print_product _ [] = NONE
   | print_product print [x] = SOME (print x)

 
 (** SML serializer **)
 
 fun print_sml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
   let
-    val deresolve_const = deresolve o Code_Symbol.Constant;
-    val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
-    val deresolve_class = deresolve o Code_Symbol.Type_Class;
-    val deresolve_classrel = deresolve o Code_Symbol.Class_Relation;
-    val deresolve_inst = deresolve o Code_Symbol.Class_Instance;
+    val deresolve_const = deresolve o Constant;
+    val deresolve_tyco = deresolve o Type_Constructor;
+    val deresolve_class = deresolve o Type_Class;
+    val deresolve_classrel = deresolve o Class_Relation;
+    val deresolve_inst = deresolve o Class_Instance;
     fun print_tyco_expr (sym, []) = (str o deresolve) sym
       | print_tyco_expr (sym, [ty]) =
           concat [print_typ BR ty, (str o deresolve) sym]
       | print_tyco_expr (sym, tys) =
           concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
     and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
-         of NONE => print_tyco_expr (Code_Symbol.Type_Constructor tyco, tys)
+         of NONE => print_tyco_expr (Type_Constructor tyco, tys)
           | SOME (_, print) => print print_typ fxy tys)
       | print_typ fxy (ITyVar v) = str ("'" ^ v);
-    fun print_dicttyp (class, ty) = print_tyco_expr (Code_Symbol.Type_Class class, [ty]);
+    fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]);
     fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
       (map_filter (fn (v, sort) =>
         (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
     fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
     fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);

           brackify fxy [enum " o" "(" ")" (map (str o deresolve_classrel) classrels), brackify BR ps]
     fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
       print_classrels fxy classrels (print_plain_dict is_pseudo_fun fxy x)
     and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
           ((str o deresolve_inst) inst ::
-            (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
+            (if is_pseudo_fun (Class_Instance inst) then [str "()"]
             else map_filter (print_dicts is_pseudo_fun BR) dss))
       | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
           [str (if k = 1 then first_upper v ^ "_"
             else first_upper v ^ string_of_int (i+1) ^ "_")]
     and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);

               #>> (fn p => concat [str "fn", p, str "=>"]);
             val (ps, vars') = fold_map print_abs binds vars;
           in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
       | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
           (case Code_Thingol.unfold_const_app (#primitive case_expr)
-           of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
+           of SOME (app as ({ sym = Constant const, ... }, _)) =>
                 if is_none (const_syntax const)
                 then print_case is_pseudo_fun some_thm vars fxy case_expr
                 else print_app is_pseudo_fun some_thm vars fxy app
             | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
     and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) =

           | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of",
               enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
       in
         concat (
           str definer
-          :: print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs)
+          :: print_tyco_expr (Type_Constructor tyco, map ITyVar vs)
           :: str "="
           :: separate (str "|") (map print_co cos)
         )
       end;
     fun print_def is_pseudo_fun needs_typ definer

                   concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty]
                     else (concat o map str) [definer, deresolve_const const];
               in
                 concat (
                   prolog
-                  :: (if is_pseudo_fun (Code_Symbol.Constant const) then [str "()"]
+                  :: (if is_pseudo_fun (Constant const) then [str "()"]
                       else print_dict_args vs
                         @ map (print_term is_pseudo_fun some_thm vars BR) ts)
                   @ str "="
                   @@ print_term is_pseudo_fun some_thm vars NOBR t
                 )
               end
             val shift = if null eqs then I else
               map (Pretty.block o single o Pretty.block o single);
           in pair
-            (print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty))
+            (print_val_decl print_typscheme (Constant const, vs_ty))
             ((Pretty.block o Pretty.fbreaks o shift) (
               print_eqn definer eq
               :: map (print_eqn "|") eqs
             ))
           end

                 str "=",
                 print_app (K false) (SOME thm) reserved NOBR (const, [])
               ];
           in pair
             (print_val_decl print_dicttypscheme
-              (Code_Symbol.Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
+              (Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
             (concat (
               str definer
               :: (str o deresolve_inst) inst
-              :: (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
+              :: (if is_pseudo_fun (Class_Instance inst) then [str "()"]
                   else print_dict_args vs)
               @ str "="
               :: enum "," "{" "}"
                 (map print_super_instance superinsts
                   @ map print_classparam_instance inst_params)
               :: str ":"
               @@ print_dicttyp (class, tyco `%% map (ITyVar o fst) vs)
             ))
           end;
     fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair
-          [print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty)]
+          [print_val_decl print_typscheme (Constant const, vs_ty)]
           ((semicolon o map str) (
             (if n = 0 then "val" else "fun")
             :: deresolve_const const
             :: replicate n "_"
             @ "="

             sig_ps
             (Pretty.chunks (ps @ semicolon [p] :: pseudo_ps))
           end
      | print_stmt (ML_Datas [(tyco, (vs, []))]) =
           let
-            val ty_p = print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs);
+            val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs);
           in
             pair
             [concat [str "type", ty_p]]
             (concat [str "datatype", ty_p, str "=", str "EMPTY__"])
           end

             fun print_field s p = concat [str s, str ":", p];
             fun print_proj s p = semicolon
               (map str ["val", s, "=", "#" ^ s, ":"] @| p);
             fun print_super_class_decl (classrel as (_, super_class)) =
               print_val_decl print_dicttypscheme
-                (Code_Symbol.Class_Relation classrel, ([(v, [class])], (super_class, ITyVar v)));
+                (Class_Relation classrel, ([(v, [class])], (super_class, ITyVar v)));
             fun print_super_class_field (classrel as (_, super_class)) =
               print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v));
             fun print_super_class_proj (classrel as (_, super_class)) =
               print_proj (deresolve_classrel classrel)
                 (print_dicttypscheme ([(v, [class])], (super_class, ITyVar v)));
             fun print_classparam_decl (classparam, ty) =
               print_val_decl print_typscheme
-                (Code_Symbol.Constant classparam, ([(v, [class])], ty));
+                (Constant classparam, ([(v, [class])], ty));
             fun print_classparam_field (classparam, ty) =
               print_field (deresolve_const classparam) (print_typ NOBR ty);
             fun print_classparam_proj (classparam, ty) =
               print_proj (deresolve_const classparam)
                 (print_typscheme ([(v, [class])], ty));

 
 (** OCaml serializer **)
 
 fun print_ocaml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
   let
-    val deresolve_const = deresolve o Code_Symbol.Constant;
-    val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
-    val deresolve_class = deresolve o Code_Symbol.Type_Class;
-    val deresolve_classrel = deresolve o Code_Symbol.Class_Relation;
-    val deresolve_inst = deresolve o Code_Symbol.Class_Instance;
+    val deresolve_const = deresolve o Constant;
+    val deresolve_tyco = deresolve o Type_Constructor;
+    val deresolve_class = deresolve o Type_Class;
+    val deresolve_classrel = deresolve o Class_Relation;
+    val deresolve_inst = deresolve o Class_Instance;
     fun print_tyco_expr (sym, []) = (str o deresolve) sym
       | print_tyco_expr (sym, [ty]) =
           concat [print_typ BR ty, (str o deresolve) sym]
       | print_tyco_expr (sym, tys) =
           concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
     and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
-         of NONE => print_tyco_expr (Code_Symbol.Type_Constructor tyco, tys)
+         of NONE => print_tyco_expr (Type_Constructor tyco, tys)
           | SOME (_, print) => print print_typ fxy tys)
       | print_typ fxy (ITyVar v) = str ("'" ^ v);
-    fun print_dicttyp (class, ty) = print_tyco_expr (Code_Symbol.Type_Class class, [ty]);
+    fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]);
     fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
       (map_filter (fn (v, sort) =>
         (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
     fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
     fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);

     fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
       print_plain_dict is_pseudo_fun fxy x
       |> print_classrels classrels
     and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
           brackify BR ((str o deresolve_inst) inst ::
-            (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
+            (if is_pseudo_fun (Class_Instance inst) then [str "()"]
             else map_filter (print_dicts is_pseudo_fun BR) dss))
       | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
           str (if k = 1 then "_" ^ first_upper v
             else "_" ^ first_upper v ^ string_of_int (i+1))
     and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);

             val (binds, t') = Code_Thingol.unfold_pat_abs t;
             val (ps, vars') = fold_map (print_bind is_pseudo_fun some_thm BR o fst) binds vars;
           in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
       | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
           (case Code_Thingol.unfold_const_app (#primitive case_expr)
-           of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
+           of SOME (app as ({ sym = Constant const, ... }, _)) =>
                 if is_none (const_syntax const)
                 then print_case is_pseudo_fun some_thm vars fxy case_expr
                 else print_app is_pseudo_fun some_thm vars fxy app
             | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
     and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) =

           | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of",
               enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
       in
         concat (
           str definer
-          :: print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs)
+          :: print_tyco_expr (Type_Constructor tyco, map ITyVar vs)
           :: str "="
           :: separate (str "|") (map print_co cos)
         )
       end;
     fun print_def is_pseudo_fun needs_typ definer

                   end;
             val prolog = if needs_typ then
               concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty]
                 else (concat o map str) [definer, deresolve_const const];
           in pair
-            (print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty))
+            (print_val_decl print_typscheme (Constant const, vs_ty))
             (concat (
               prolog
               :: print_dict_args vs
-              @| print_eqns (is_pseudo_fun (Code_Symbol.Constant const)) eqs
+              @| print_eqns (is_pseudo_fun (Constant const)) eqs
             ))
           end
       | print_def is_pseudo_fun _ definer
           (ML_Instance (inst as (tyco, class), { vs, superinsts, inst_params, ... })) =
           let

                 str "=",
                 print_app (K false) (SOME thm) reserved NOBR (const, [])
               ];
           in pair
             (print_val_decl print_dicttypscheme
-              (Code_Symbol.Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
+              (Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
             (concat (
               str definer
               :: (str o deresolve_inst) inst
-              :: (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
+              :: (if is_pseudo_fun (Class_Instance inst) then [str "()"]
                   else print_dict_args vs)
               @ str "="
               @@ brackets [
                 enum_default "()" ";" "{" "}" (map print_super_instance superinsts
                   @ map print_classparam_instance inst_params),

                 print_dicttyp (class, tyco `%% map (ITyVar o fst) vs)
               ]
             ))
           end;
      fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair
-          [print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty)]
+          [print_val_decl print_typscheme (Constant const, vs_ty)]
           ((doublesemicolon o map str) (
             "let"
             :: deresolve_const const
             :: replicate n "_"
             @ "="

             sig_ps
             (Pretty.chunks (ps @ doublesemicolon [p] :: pseudo_ps))
           end
      | print_stmt (ML_Datas [(tyco, (vs, []))]) =
           let
-            val ty_p = print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs);
+            val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs);
           in
             pair
             [concat [str "type", ty_p]]
             (concat [str "type", ty_p, str "=", str "EMPTY__"])
           end

             fun print_field s p = concat [str s, str ":", p];
             fun print_super_class_field (classrel as (_, super_class)) =
               print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v));
             fun print_classparam_decl (classparam, ty) =
               print_val_decl print_typscheme
-                (Code_Symbol.Constant classparam, ([(v, [class])], ty));
+                (Constant classparam, ([(v, [class])], ty));
             fun print_classparam_field (classparam, ty) =
               print_field (deresolve_const classparam) (print_typ NOBR ty);
             val w = "_" ^ first_upper v;
             fun print_classparam_proj (classparam, _) =
               (concat o map str) ["let", deresolve_const classparam, w, "=",

       | namify_stmt (Code_Thingol.Datatypecons _) = namify_const true
       | namify_stmt (Code_Thingol.Class _) = namify_type
       | namify_stmt (Code_Thingol.Classrel _) = namify_const false
       | namify_stmt (Code_Thingol.Classparam _) = namify_const false
       | namify_stmt (Code_Thingol.Classinst _) = namify_const false;
-    fun ml_binding_of_stmt (sym as Code_Symbol.Constant const, Code_Thingol.Fun ((tysm as (vs, ty), raw_eqs), _)) =
+    fun ml_binding_of_stmt (sym as Constant const, Code_Thingol.Fun ((tysm as (vs, ty), raw_eqs), _)) =
           let
             val eqs = filter (snd o snd) raw_eqs;
             val (eqs', some_sym) = if null (filter_out (null o snd) vs) then case eqs
                of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
                   then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE)
                   else (eqs, SOME (sym, member (op =) (Code_Thingol.add_constsyms t []) sym))
                 | _ => (eqs, NONE)
               else (eqs, NONE)
           in (ML_Function (const, (tysm, eqs')), some_sym) end
-      | ml_binding_of_stmt (sym as Code_Symbol.Class_Instance inst, Code_Thingol.Classinst (stmt as { vs, ... })) =
+      | ml_binding_of_stmt (sym as Class_Instance inst, Code_Thingol.Classinst (stmt as { vs, ... })) =
           (ML_Instance (inst, stmt), if forall (null o snd) vs then SOME (sym, false) else NONE)
       | ml_binding_of_stmt (sym, _) =
           error ("Binding block containing illegal statement: " ^ 
             Code_Symbol.quote ctxt sym)
     fun modify_fun (sym, stmt) =

       in SOME ml_stmt end;
     fun modify_funs stmts = single (SOME
       (ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))
     fun modify_datatypes stmts = single (SOME
       (ML_Datas (map_filter
-        (fn (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype stmt) => SOME (tyco, stmt) | _ => NONE) stmts)))
+        (fn (Type_Constructor tyco, Code_Thingol.Datatype stmt) => SOME (tyco, stmt) | _ => NONE) stmts)))
     fun modify_class stmts = single (SOME
       (ML_Class (the_single (map_filter
-        (fn (Code_Symbol.Type_Class class, Code_Thingol.Class stmt) => SOME (class, stmt) | _ => NONE) stmts))))
+        (fn (Type_Class class, Code_Thingol.Class stmt) => SOME (class, stmt) | _ => NONE) stmts))))
     fun modify_stmts ([stmt as (_, stmt' as Code_Thingol.Fun _)]) =
           if Code_Thingol.is_case stmt' then [] else [modify_fun stmt]
       | modify_stmts ((stmts as (_, Code_Thingol.Fun _) :: _)) =
           modify_funs (filter_out (Code_Thingol.is_case o snd) stmts)
       | modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _) :: _)) =

   #> Code_Target.add_target
     (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
       check = { env_var = "ISABELLE_OCAML",
         make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
         make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } })
-  #> Code_Target.set_printings (Code_Symbol.Type_Constructor ("fun",
+  #> Code_Target.set_printings (Type_Constructor ("fun",
     [(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))
   #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
   #> fold (Code_Target.add_reserved target_SML)
       ["ref" (*rebinding is illegal*), "o" (*dictionary projections use it already*),
         "Fail", "div", "mod" (*standard infixes*), "IntInf"]