src/Tools/Code/code_haskell.ML

   "{-# LANGUAGE " ^ commas language_extensions ^ " #-}";
 
 val language_params =
   space_implode " " (map (prefix "-X") language_extensions);
 
+open Basic_Code_Symbol;
 open Basic_Code_Thingol;
 open Code_Printer;
 
 infixr 5 @@;
 infixr 5 @|;

 (** Haskell serializer **)
 
 fun print_haskell_stmt class_syntax tyco_syntax const_syntax
     reserved deresolve deriving_show =
   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_const = deresolve o Constant;
+    val deresolve_tyco = deresolve o Type_Constructor;
+    val deresolve_class = deresolve o Type_Class;
     fun class_name class = case class_syntax class
      of NONE => deresolve_class class
       | SOME class => class;
     fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
      of [] => []

             val (binds, t') = Code_Thingol.unfold_pat_abs t;
             val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars;
           in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
       | print_term tyvars 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 tyvars some_thm vars fxy case_expr
                 else print_app tyvars some_thm vars fxy app
             | NONE => print_case tyvars some_thm vars fxy case_expr)
     and print_app_expr tyvars some_thm vars ({ sym, dom, range, annotate, ... }, ts) =

               in semicolon [p, str "->", print_term tyvars some_thm vars' NOBR body] end;
           in Pretty.block_enclose
             (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
             (map print_select clauses)
           end;
-    fun print_stmt (Code_Symbol.Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
+    fun print_stmt (Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
           let
             val tyvars = intro_vars (map fst vs) reserved;
             fun print_err n =
               (semicolon o map str) (
                 deresolve_const const

               :: (case filter (snd o snd) raw_eqs
                of [] => [print_err ((length o fst o Code_Thingol.unfold_fun) ty)]
                 | eqs => map print_eqn eqs)
             )
           end
-      | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, [])) =
+      | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, [])) =
           let
             val tyvars = intro_vars vs reserved;
           in
             semicolon [
               str "data",
               print_typdecl tyvars (deresolve_tyco tyco, vs)
             ]
           end
-      | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, [((co, _), [ty])])) =
+      | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, [((co, _), [ty])])) =
           let
             val tyvars = intro_vars vs reserved;
           in
             semicolon (
               str "newtype"

               :: (str o deresolve_const) co
               :: print_typ tyvars BR ty
               :: (if deriving_show tyco then [str "deriving (Read, Show)"] else [])
             )
           end
-      | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, co :: cos)) =
+      | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, co :: cos)) =
           let
             val tyvars = intro_vars vs reserved;
             fun print_co ((co, _), tys) =
               concat (
                 (str o deresolve_const) co

               :: print_co co
               :: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos
               @ (if deriving_show tyco then [str "deriving (Read, Show)"] else [])
             )
           end
-      | print_stmt (Code_Symbol.Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
+      | print_stmt (Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
           let
             val tyvars = intro_vars [v] reserved;
             fun print_classparam (classparam, ty) =
               semicolon [
                 (str o deresolve_const) classparam,

                       str "=",
                       print_app tyvars (SOME thm) reserved NOBR (const, [])
                     ]
                 | SOME k =>
                     let
-                      val { sym = Code_Symbol.Constant c, dom, range, ... } = const;
+                      val { sym = Constant c, dom, range, ... } = const;
                       val (vs, rhs) = (apfst o map) fst
                         (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
                       val s = if (is_some o const_syntax) c
                         then NONE else (SOME o Long_Name.base_name o deresolve_const) c;
                       val vars = reserved
                         |> intro_vars (map_filter I (s :: vs));
-                      val lhs = IConst { sym = Code_Symbol.Constant classparam, typargs = [],
+                      val lhs = IConst { sym = Constant classparam, typargs = [],
                         dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
                         (*dictionaries are not relevant at this late stage,
                           and these consts never need type annotations for disambiguation *)
                     in
                       semicolon [

     (* print statements *)
     fun deriving_show tyco =
       let
         fun deriv _ "fun" = false
           | deriv tycos tyco = member (op =) tycos tyco
-              orelse case try (Code_Symbol.Graph.get_node program) (Code_Symbol.Type_Constructor tyco)
+              orelse case try (Code_Symbol.Graph.get_node program) (Type_Constructor tyco)
                 of SOME (Code_Thingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos))
                     (maps snd cs)
                  | NONE => true
         and deriv' tycos (tyco `%% tys) = deriv tycos tyco
               andalso forall (deriv' tycos) tys

   let
     fun dest_bind t1 t2 = case Code_Thingol.split_pat_abs t2
      of SOME ((pat, ty), t') =>
           SOME ((SOME ((pat, ty), true), t1), t')
       | NONE => NONE;
-    fun dest_monad (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
+    fun dest_monad (IConst { sym = Constant c, ... } `$ t1 `$ t2) =
           if c = c_bind then dest_bind t1 t2
           else NONE
       | dest_monad t = case Code_Thingol.split_let t
          of SOME (((pat, ty), tbind), t') =>
               SOME ((SOME ((pat, ty), false), tbind), t')

   let
     val c_bind = Code.read_const thy raw_c_bind;
   in
     if target = target' then
       thy
-      |> Code_Target.set_printings (Code_Symbol.Constant (c_bind, [(target,
+      |> Code_Target.set_printings (Constant (c_bind, [(target,
         SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))]))
     else error "Only Haskell target allows for monad syntax"
   end;
 
 

     (target, { serializer = serializer, literals = literals,
       check = { env_var = "ISABELLE_GHC", make_destination = I,
         make_command = fn module_name =>
           "\"$ISABELLE_GHC\" " ^ language_params  ^ " -odir build -hidir build -stubdir build -e \"\" " ^
             module_name ^ ".hs" } })
-  #> Code_Target.set_printings (Code_Symbol.Type_Constructor ("fun",
+  #> Code_Target.set_printings (Type_Constructor ("fun",
     [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
       brackify_infix (1, R) fxy (
         print_typ (INFX (1, X)) ty1,
         str "->",
         print_typ (INFX (1, R)) ty2