prefer explicit code symbol type over ad-hoc name mangling
authorhaftmann
Sat Jan 25 23:50:49 2014 +0100 (2014-01-25)
changeset 55147bce3dbc11f95
parent 55146 525309c2e4ee
child 55148 7e1b7cb54114
prefer explicit code symbol type over ad-hoc name mangling
src/Doc/Codegen/Adaptation.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/List.thy
src/HOL/Quickcheck_Narrowing.thy
src/HOL/Quickcheck_Random.thy
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/numeral.ML
src/HOL/Tools/string_code.ML
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_namespace.ML
src/Tools/Code/code_printer.ML
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_simp.ML
src/Tools/Code/code_symbol.ML
src/Tools/Code/code_target.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/Doc/Codegen/Adaptation.thy	Sat Jan 25 23:50:49 2014 +0100
     1.2 +++ b/src/Doc/Codegen/Adaptation.thy	Sat Jan 25 23:50:49 2014 +0100
     1.3 @@ -2,8 +2,8 @@
     1.4  imports Setup
     1.5  begin
     1.6  
     1.7 -setup %invisible {* Code_Target.extend_target ("\<SML>", ("SML", K I))
     1.8 -  #> Code_Target.extend_target ("\<SMLdummy>", ("Haskell", K I)) *}
     1.9 +setup %invisible {* Code_Target.extend_target ("\<SML>", ("SML", I))
    1.10 +  #> Code_Target.extend_target ("\<SMLdummy>", ("Haskell", I)) *}
    1.11  
    1.12  section {* Adaptation to target languages \label{sec:adaptation} *}
    1.13  
     2.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Sat Jan 25 23:50:49 2014 +0100
     2.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Sat Jan 25 23:50:49 2014 +0100
     2.3 @@ -671,25 +671,17 @@
     2.4  
     2.5  open Code_Thingol;
     2.6  
     2.7 -fun imp_program naming =
     2.8 +val imp_program =
     2.9    let
    2.10 -    fun is_const c = case lookup_const naming c
    2.11 -     of SOME c' => (fn c'' => c' = c'')
    2.12 -      | NONE => K false;
    2.13 -    val is_bind = is_const @{const_name bind};
    2.14 -    val is_return = is_const @{const_name return};
    2.15 +    val is_bind = curry (op =) @{const_name bind};
    2.16 +    val is_return = curry (op =) @{const_name return};
    2.17      val dummy_name = "";
    2.18      val dummy_case_term = IVar NONE;
    2.19      (*assumption: dummy values are not relevant for serialization*)
    2.20 -    val (unitt, unitT) = case lookup_const naming @{const_name Unity}
    2.21 -     of SOME unit' =>
    2.22 -          let
    2.23 -            val unitT = the (lookup_tyco naming @{type_name unit}) `%% []
    2.24 -          in
    2.25 -            (IConst { name = unit', typargs = [], dicts = [], dom = [],
    2.26 -              range = unitT, annotate = false }, unitT)
    2.27 -          end
    2.28 -      | NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants.");
    2.29 +    val unitT = @{type_name unit} `%% [];
    2.30 +    val unitt =
    2.31 +      IConst { sym = Code_Symbol.Constant @{const_name Unity}, typargs = [], dicts = [], dom = [],
    2.32 +        range = unitT, annotate = false };
    2.33      fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
    2.34        | dest_abs (t, ty) =
    2.35            let
    2.36 @@ -697,7 +689,7 @@
    2.37              val v = singleton (Name.variant_list vs) "x";
    2.38              val ty' = (hd o fst o unfold_fun) ty;
    2.39            in ((SOME v, ty'), t `$ IVar (SOME v)) end;
    2.40 -    fun force (t as IConst { name = c, ... } `$ t') = if is_return c
    2.41 +    fun force (t as IConst { sym = Code_Symbol.Constant c, ... } `$ t') = if is_return c
    2.42            then t' else t `$ unitt
    2.43        | force t = t `$ unitt;
    2.44      fun tr_bind'' [(t1, _), (t2, ty2)] =
    2.45 @@ -705,13 +697,13 @@
    2.46          val ((v, ty), t) = dest_abs (t2, ty2);
    2.47        in ICase { term = force t1, typ = ty, clauses = [(IVar v, tr_bind' t)], primitive = dummy_case_term } end
    2.48      and tr_bind' t = case unfold_app t
    2.49 -     of (IConst { name = c, dom = ty1 :: ty2 :: _, ... }, [x1, x2]) => if is_bind c
    2.50 +     of (IConst { sym = Code_Symbol.Constant c, dom = ty1 :: ty2 :: _, ... }, [x1, x2]) => if is_bind c
    2.51            then tr_bind'' [(x1, ty1), (x2, ty2)]
    2.52            else force t
    2.53        | _ => force t;
    2.54      fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=>
    2.55        ICase { term = IVar (SOME dummy_name), typ = unitT, clauses = [(unitt, tr_bind'' ts)], primitive = dummy_case_term }
    2.56 -    fun imp_monad_bind' (const as { name = c, dom = dom, ... }) ts = if is_bind c then case (ts, dom)
    2.57 +    fun imp_monad_bind' (const as { sym = Code_Symbol.Constant c, dom = dom, ... }) ts = if is_bind c then case (ts, dom)
    2.58         of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
    2.59          | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
    2.60          | (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))
    2.61 @@ -726,7 +718,7 @@
    2.62            ICase { term = imp_monad_bind t, typ = ty,
    2.63              clauses = (map o pairself) imp_monad_bind clauses, primitive = imp_monad_bind t0 };
    2.64  
    2.65 -  in (Graph.map o K o map_terms_stmt) imp_monad_bind end;
    2.66 +  in (Code_Symbol.Graph.map o K o map_terms_stmt) imp_monad_bind end;
    2.67  
    2.68  in
    2.69  
     3.1 --- a/src/HOL/List.thy	Sat Jan 25 23:50:49 2014 +0100
     3.2 +++ b/src/HOL/List.thy	Sat Jan 25 23:50:49 2014 +0100
     3.3 @@ -6318,14 +6318,14 @@
     3.4  
     3.5  fun implode_list nil' cons' t =
     3.6    let
     3.7 -    fun dest_cons (IConst { name = c, ... } `$ t1 `$ t2) =
     3.8 +    fun dest_cons (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
     3.9            if c = cons'
    3.10            then SOME (t1, t2)
    3.11            else NONE
    3.12        | dest_cons _ = NONE;
    3.13      val (ts, t') = Code_Thingol.unfoldr dest_cons t;
    3.14    in case t'
    3.15 -   of IConst { name = c, ... } => if c = nil' then SOME ts else NONE
    3.16 +   of IConst { sym = Code_Symbol.Constant c, ... } => if c = nil' then SOME ts else NONE
    3.17      | _ => NONE
    3.18    end;
    3.19  
     4.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Sat Jan 25 23:50:49 2014 +0100
     4.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Sat Jan 25 23:50:49 2014 +0100
     4.3 @@ -11,7 +11,7 @@
     4.4  
     4.5  subsubsection {* Code generation setup *}
     4.6  
     4.7 -setup {* Code_Target.extend_target ("Haskell_Quickcheck", (Code_Haskell.target, K I)) *}
     4.8 +setup {* Code_Target.extend_target ("Haskell_Quickcheck", (Code_Haskell.target, I)) *}
     4.9  
    4.10  code_printing
    4.11    type_constructor typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep"
     5.1 --- a/src/HOL/Quickcheck_Random.thy	Sat Jan 25 23:50:49 2014 +0100
     5.2 +++ b/src/HOL/Quickcheck_Random.thy	Sat Jan 25 23:50:49 2014 +0100
     5.3 @@ -9,7 +9,7 @@
     5.4  notation fcomp (infixl "\<circ>>" 60)
     5.5  notation scomp (infixl "\<circ>\<rightarrow>" 60)
     5.6  
     5.7 -setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, K I)) *}
     5.8 +setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, I)) *}
     5.9  
    5.10  subsection {* Catching Match exceptions *}
    5.11  
     6.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Jan 25 23:50:49 2014 +0100
     6.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Jan 25 23:50:49 2014 +0100
     6.3 @@ -309,9 +309,9 @@
     6.4  fun dynamic_value_strict opts cookie thy postproc t =
     6.5    let
     6.6      val ctxt = Proof_Context.init_global thy
     6.7 -    fun evaluator naming program ((_, vs_ty), t) deps =
     6.8 +    fun evaluator program ((_, vs_ty), t) deps =
     6.9        Exn.interruptible_capture (value opts ctxt cookie)
    6.10 -        (Code_Target.evaluator thy target naming program deps (vs_ty, t));
    6.11 +        (Code_Target.evaluator thy target program deps (vs_ty, t));
    6.12    in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
    6.13  
    6.14  (** counterexample generator **)
     7.1 --- a/src/HOL/Tools/numeral.ML	Sat Jan 25 23:50:49 2014 +0100
     7.2 +++ b/src/HOL/Tools/numeral.ML	Sat Jan 25 23:50:49 2014 +0100
     7.3 @@ -69,11 +69,11 @@
     7.4    let
     7.5      fun dest_numeral one' bit0' bit1' thm t =
     7.6        let
     7.7 -        fun dest_bit (IConst { name = c, ... }) = if c = bit0' then 0
     7.8 +        fun dest_bit (IConst { sym = Code_Symbol.Constant c, ... }) = if c = bit0' then 0
     7.9                else if c = bit1' then 1
    7.10                else Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit"
    7.11            | dest_bit _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit";
    7.12 -        fun dest_num (IConst { name = c, ... }) = if c = one' then 1
    7.13 +        fun dest_num (IConst { sym = Code_Symbol.Constant c, ... }) = if c = one' then 1
    7.14                else Code_Printer.eqn_error thm "Illegal numeral expression: illegal leading digit"
    7.15            | dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_bit t1
    7.16            | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
     8.1 --- a/src/HOL/Tools/string_code.ML	Sat Jan 25 23:50:49 2014 +0100
     8.2 +++ b/src/HOL/Tools/string_code.ML	Sat Jan 25 23:50:49 2014 +0100
     8.3 @@ -23,13 +23,13 @@
     8.4        | decode _ ~1 = NONE
     8.5        | decode n m = SOME (chr (n * 16 + m));
     8.6    in case tt
     8.7 -   of (IConst { name = c1, ... }, IConst { name = c2, ... }) => decode (idx c1) (idx c2)
     8.8 +   of (IConst { sym = Code_Symbol.Constant c1, ... }, IConst { sym = Code_Symbol.Constant c2, ... }) => decode (idx c1) (idx c2)
     8.9      | _ => NONE
    8.10    end;
    8.11     
    8.12  fun implode_string literals char' nibbles' ts =
    8.13    let
    8.14 -    fun implode_char (IConst { name = c, ... } `$ t1 `$ t2) =
    8.15 +    fun implode_char (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
    8.16            if c = char' then decode_char nibbles' (t1, t2) else NONE
    8.17        | implode_char _ = NONE;
    8.18      val ts' = map_filter implode_char ts;
     9.1 --- a/src/Tools/Code/code_haskell.ML	Sat Jan 25 23:50:49 2014 +0100
     9.2 +++ b/src/Tools/Code/code_haskell.ML	Sat Jan 25 23:50:49 2014 +0100
     9.3 @@ -37,8 +37,11 @@
     9.4  fun print_haskell_stmt class_syntax tyco_syntax const_syntax
     9.5      reserved deresolve deriving_show =
     9.6    let
     9.7 +    val deresolve_const = deresolve o Code_Symbol.Constant;
     9.8 +    val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
     9.9 +    val deresolve_class = deresolve o Code_Symbol.Type_Class;
    9.10      fun class_name class = case class_syntax class
    9.11 -     of NONE => deresolve class
    9.12 +     of NONE => deresolve_class class
    9.13        | SOME class => class;
    9.14      fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
    9.15       of [] => []
    9.16 @@ -53,7 +56,7 @@
    9.17      fun print_tyco_expr tyvars fxy (tyco, tys) =
    9.18        brackify fxy (str tyco :: map (print_typ tyvars BR) tys)
    9.19      and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
    9.20 -         of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys)
    9.21 +         of NONE => print_tyco_expr tyvars fxy (deresolve_tyco tyco, tys)
    9.22            | SOME (_, print) => print (print_typ tyvars) fxy tys)
    9.23        | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
    9.24      fun print_typdecl tyvars (tyco, vs) =
    9.25 @@ -81,18 +84,19 @@
    9.26            in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
    9.27        | print_term tyvars some_thm vars fxy (ICase case_expr) =
    9.28            (case Code_Thingol.unfold_const_app (#primitive case_expr)
    9.29 -           of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
    9.30 +           of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
    9.31 +                if is_none (const_syntax const)
    9.32                  then print_case tyvars some_thm vars fxy case_expr
    9.33                  else print_app tyvars some_thm vars fxy app
    9.34              | NONE => print_case tyvars some_thm vars fxy case_expr)
    9.35 -    and print_app_expr tyvars some_thm vars ({ name = c, dom, range, annotate, ... }, ts) =
    9.36 +    and print_app_expr tyvars some_thm vars ({ sym, dom, range, annotate, ... }, ts) =
    9.37        let
    9.38 -        val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (dom, range)
    9.39 +        val ty = Library.foldr (op `->) (dom, range)
    9.40          val printed_const =
    9.41            if annotate then
    9.42 -            brackets [(str o deresolve) c, str "::", print_typ tyvars NOBR ty]
    9.43 +            brackets [(str o deresolve) sym, str "::", print_typ tyvars NOBR ty]
    9.44            else
    9.45 -            (str o deresolve) c
    9.46 +            (str o deresolve) sym
    9.47        in 
    9.48          printed_const :: map (print_term tyvars some_thm vars BR) ts
    9.49        end
    9.50 @@ -122,17 +126,16 @@
    9.51              (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
    9.52              (map print_select clauses)
    9.53            end;
    9.54 -    fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
    9.55 +    fun print_stmt (Code_Symbol.Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
    9.56            let
    9.57              val tyvars = intro_vars (map fst vs) reserved;
    9.58              fun print_err n =
    9.59 -              semicolon (
    9.60 -                (str o deresolve) name
    9.61 -                :: map str (replicate n "_")
    9.62 -                @ str "="
    9.63 -                :: str "error"
    9.64 -                @@ (str o ML_Syntax.print_string
    9.65 -                    o Long_Name.base_name o Long_Name.qualifier) name
    9.66 +              (semicolon o map str) (
    9.67 +                deresolve_const const
    9.68 +                :: replicate n "_"
    9.69 +                @ "="
    9.70 +                :: "error"
    9.71 +                @@ ML_Syntax.print_string const
    9.72                );
    9.73              fun print_eqn ((ts, t), (some_thm, _)) =
    9.74                let
    9.75 @@ -143,7 +146,7 @@
    9.76                        (insert (op =)) ts []);
    9.77                in
    9.78                  semicolon (
    9.79 -                  (str o deresolve) name
    9.80 +                  (str o deresolve_const) const
    9.81                    :: map (print_term tyvars some_thm vars BR) ts
    9.82                    @ str "="
    9.83                    @@ print_term tyvars some_thm vars NOBR t
    9.84 @@ -152,7 +155,7 @@
    9.85            in
    9.86              Pretty.chunks (
    9.87                semicolon [
    9.88 -                (str o suffix " ::" o deresolve) name,
    9.89 +                (str o suffix " ::" o deresolve_const) const,
    9.90                  print_typscheme tyvars (vs, ty)
    9.91                ]
    9.92                :: (case filter (snd o snd) raw_eqs
    9.93 @@ -160,52 +163,52 @@
    9.94                  | eqs => map print_eqn eqs)
    9.95              )
    9.96            end
    9.97 -      | print_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
    9.98 +      | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, [])) =
    9.99            let
   9.100              val tyvars = intro_vars vs reserved;
   9.101            in
   9.102              semicolon [
   9.103                str "data",
   9.104 -              print_typdecl tyvars (deresolve name, vs)
   9.105 +              print_typdecl tyvars (deresolve_tyco tyco, vs)
   9.106              ]
   9.107            end
   9.108 -      | print_stmt (name, Code_Thingol.Datatype (_, (vs, [((co, _), [ty])]))) =
   9.109 +      | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, [((co, _), [ty])])) =
   9.110            let
   9.111              val tyvars = intro_vars vs reserved;
   9.112            in
   9.113              semicolon (
   9.114                str "newtype"
   9.115 -              :: print_typdecl tyvars (deresolve name, vs)
   9.116 +              :: print_typdecl tyvars (deresolve_tyco tyco, vs)
   9.117                :: str "="
   9.118 -              :: (str o deresolve) co
   9.119 +              :: (str o deresolve_const) co
   9.120                :: print_typ tyvars BR ty
   9.121 -              :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
   9.122 +              :: (if deriving_show tyco then [str "deriving (Read, Show)"] else [])
   9.123              )
   9.124            end
   9.125 -      | print_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
   9.126 +      | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, co :: cos)) =
   9.127            let
   9.128              val tyvars = intro_vars vs reserved;
   9.129              fun print_co ((co, _), tys) =
   9.130                concat (
   9.131 -                (str o deresolve) co
   9.132 +                (str o deresolve_const) co
   9.133                  :: map (print_typ tyvars BR) tys
   9.134                )
   9.135            in
   9.136              semicolon (
   9.137                str "data"
   9.138 -              :: print_typdecl tyvars (deresolve name, vs)
   9.139 +              :: print_typdecl tyvars (deresolve_tyco tyco, vs)
   9.140                :: str "="
   9.141                :: print_co co
   9.142                :: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos
   9.143 -              @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
   9.144 +              @ (if deriving_show tyco then [str "deriving (Read, Show)"] else [])
   9.145              )
   9.146            end
   9.147 -      | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
   9.148 +      | print_stmt (Code_Symbol.Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
   9.149            let
   9.150              val tyvars = intro_vars [v] reserved;
   9.151              fun print_classparam (classparam, ty) =
   9.152                semicolon [
   9.153 -                (str o deresolve) classparam,
   9.154 +                (str o deresolve_const) classparam,
   9.155                  str "::",
   9.156                  print_typ tyvars NOBR ty
   9.157                ]
   9.158 @@ -213,8 +216,8 @@
   9.159              Pretty.block_enclose (
   9.160                Pretty.block [
   9.161                  str "class ",
   9.162 -                Pretty.block (print_typcontext tyvars [(v, map fst super_classes)]),
   9.163 -                str (deresolve name ^ " " ^ lookup_var tyvars v),
   9.164 +                Pretty.block (print_typcontext tyvars [(v, map snd classrels)]),
   9.165 +                str (deresolve_class class ^ " " ^ lookup_var tyvars v),
   9.166                  str " where {"
   9.167                ],
   9.168                str "};"
   9.169 @@ -230,20 +233,20 @@
   9.170              fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
   9.171                case requires_args classparam
   9.172                 of NONE => semicolon [
   9.173 -                      (str o Long_Name.base_name o deresolve) classparam,
   9.174 +                      (str o Long_Name.base_name o deresolve_const) classparam,
   9.175                        str "=",
   9.176                        print_app tyvars (SOME thm) reserved NOBR (const, [])
   9.177                      ]
   9.178                  | SOME k =>
   9.179                      let
   9.180 -                      val { name = c, dom, range, ... } = const;
   9.181 +                      val { sym = Code_Symbol.Constant c, dom, range, ... } = const;
   9.182                        val (vs, rhs) = (apfst o map) fst
   9.183                          (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
   9.184                        val s = if (is_some o const_syntax) c
   9.185 -                        then NONE else (SOME o Long_Name.base_name o deresolve) c;
   9.186 +                        then NONE else (SOME o Long_Name.base_name o deresolve_const) c;
   9.187                        val vars = reserved
   9.188                          |> intro_vars (map_filter I (s :: vs));
   9.189 -                      val lhs = IConst { name = classparam, typargs = [],
   9.190 +                      val lhs = IConst { sym = Code_Symbol.Constant classparam, typargs = [],
   9.191                          dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
   9.192                          (*dictionaries are not relevant at this late stage,
   9.193                            and these consts never need type annotations for disambiguation *)
   9.194 @@ -268,7 +271,7 @@
   9.195            end;
   9.196    in print_stmt end;
   9.197  
   9.198 -fun haskell_program_of_program ctxt symbol_of module_prefix module_name reserved identifiers =
   9.199 +fun haskell_program_of_program ctxt module_prefix module_name reserved identifiers =
   9.200    let
   9.201      fun namify_fun upper base (nsp_fun, nsp_typ) =
   9.202        let
   9.203 @@ -279,7 +282,7 @@
   9.204        let
   9.205          val (base', nsp_typ') = Name.variant (first_upper base) nsp_typ;
   9.206        in (base', (nsp_fun, nsp_typ')) end;
   9.207 -    fun namify_stmt (Code_Thingol.Fun (_, (_, SOME _))) = pair
   9.208 +    fun namify_stmt (Code_Thingol.Fun (_, SOME _)) = pair
   9.209        | namify_stmt (Code_Thingol.Fun _) = namify_fun false
   9.210        | namify_stmt (Code_Thingol.Datatype _) = namify_typ
   9.211        | namify_stmt (Code_Thingol.Datatypecons _) = namify_fun true
   9.212 @@ -287,7 +290,7 @@
   9.213        | namify_stmt (Code_Thingol.Classrel _) = pair
   9.214        | namify_stmt (Code_Thingol.Classparam _) = namify_fun false
   9.215        | namify_stmt (Code_Thingol.Classinst _) = pair;
   9.216 -    fun select_stmt (Code_Thingol.Fun (_, (_, SOME _))) = false
   9.217 +    fun select_stmt (Code_Thingol.Fun (_, SOME _)) = false
   9.218        | select_stmt (Code_Thingol.Fun _) = true
   9.219        | select_stmt (Code_Thingol.Datatype _) = true
   9.220        | select_stmt (Code_Thingol.Datatypecons _) = false
   9.221 @@ -296,7 +299,7 @@
   9.222        | select_stmt (Code_Thingol.Classparam _) = false
   9.223        | select_stmt (Code_Thingol.Classinst _) = true;
   9.224    in
   9.225 -    Code_Namespace.flat_program ctxt symbol_of
   9.226 +    Code_Namespace.flat_program ctxt
   9.227        { module_prefix = module_prefix, module_name = module_name, reserved = reserved,
   9.228          identifiers = identifiers, empty_nsp = (reserved, reserved), namify_stmt = namify_stmt,
   9.229          modify_stmt = fn stmt => if select_stmt stmt then SOME stmt else NONE }
   9.230 @@ -323,25 +326,24 @@
   9.231    ("Maybe", ["Nothing", "Just"])
   9.232  ];
   9.233  
   9.234 -fun serialize_haskell module_prefix string_classes ctxt { symbol_of, module_name,
   9.235 +fun serialize_haskell module_prefix string_classes ctxt { module_name,
   9.236      reserved_syms, identifiers, includes, class_syntax, tyco_syntax, const_syntax } program =
   9.237    let
   9.238  
   9.239      (* build program *)
   9.240      val reserved = fold (insert (op =) o fst) includes reserved_syms;
   9.241      val { deresolver, flat_program = haskell_program } = haskell_program_of_program
   9.242 -      ctxt symbol_of module_prefix module_name (Name.make_context reserved) identifiers program;
   9.243 +      ctxt module_prefix module_name (Name.make_context reserved) identifiers program;
   9.244  
   9.245      (* print statements *)
   9.246      fun deriving_show tyco =
   9.247        let
   9.248          fun deriv _ "fun" = false
   9.249 -          | deriv tycos tyco = not (tyco = Code_Thingol.fun_tyco)
   9.250 -              andalso (member (op =) tycos tyco
   9.251 -              orelse case try (Graph.get_node program) tyco
   9.252 -                of SOME (Code_Thingol.Datatype (_, (_, cs))) => forall (deriv' (tyco :: tycos))
   9.253 +          | deriv tycos tyco = member (op =) tycos tyco
   9.254 +              orelse case try (Code_Symbol.Graph.get_node program) (Code_Symbol.Type_Constructor tyco)
   9.255 +                of SOME (Code_Thingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos))
   9.256                      (maps snd cs)
   9.257 -                 | NONE => true)
   9.258 +                 | NONE => true
   9.259          and deriv' tycos (tyco `%% tys) = deriv tycos tyco
   9.260                andalso forall (deriv' tycos) tys
   9.261            | deriv' _ (ITyVar _) = true
   9.262 @@ -369,10 +371,10 @@
   9.263          val deresolve = deresolver module_name;
   9.264          fun print_import module_name = (semicolon o map str) ["import qualified", module_name];
   9.265          val import_ps = import_common_ps @ map (print_qualified_import o fst) imports;
   9.266 -        fun print_stmt' name = case Graph.get_node gr name
   9.267 +        fun print_stmt' sym = case Code_Symbol.Graph.get_node gr sym
   9.268           of (_, NONE) => NONE
   9.269 -          | (_, SOME stmt) => SOME (markup_stmt name (print_stmt deresolve (name, stmt)));
   9.270 -        val body_ps = map_filter print_stmt' ((flat o rev o Graph.strong_conn) gr);
   9.271 +          | (_, SOME stmt) => SOME (markup_stmt sym (print_stmt deresolve (sym, stmt)));
   9.272 +        val body_ps = map_filter print_stmt' ((flat o rev o Code_Symbol.Graph.strong_conn) gr);
   9.273        in
   9.274          print_module_frame module_name
   9.275            ((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps)
   9.276 @@ -430,7 +432,7 @@
   9.277       of SOME ((pat, ty), t') =>
   9.278            SOME ((SOME ((pat, ty), true), t1), t')
   9.279        | NONE => NONE;
   9.280 -    fun dest_monad c_bind_name (IConst { name = c, ... } `$ t1 `$ t2) =
   9.281 +    fun dest_monad c_bind_name (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
   9.282            if c = c_bind_name then dest_bind t1 t2
   9.283            else NONE
   9.284        | dest_monad _ t = case Code_Thingol.split_let t
    10.1 --- a/src/Tools/Code/code_ml.ML	Sat Jan 25 23:50:49 2014 +0100
    10.2 +++ b/src/Tools/Code/code_ml.ML	Sat Jan 25 23:50:49 2014 +0100
    10.3 @@ -28,17 +28,17 @@
    10.4  
    10.5  datatype ml_binding =
    10.6      ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
    10.7 -  | ML_Instance of string * { class: string, tyco: string, vs: (vname * sort) list,
    10.8 -        superinsts: (class * (string * (string * dict list list))) list,
    10.9 +  | ML_Instance of (string * class) * { class: class, tyco: string, vs: (vname * sort) list,
   10.10 +        superinsts: (class * dict list list) list,
   10.11          inst_params: ((string * (const * int)) * (thm * bool)) list,
   10.12          superinst_params: ((string * (const * int)) * (thm * bool)) list };
   10.13  
   10.14  datatype ml_stmt =
   10.15      ML_Exc of string * (typscheme * int)
   10.16    | ML_Val of ml_binding
   10.17 -  | ML_Funs of ml_binding list * string list
   10.18 +  | ML_Funs of ml_binding list * Code_Symbol.symbol list
   10.19    | ML_Datas of (string * (vname list * ((string * vname list) * itype list) list)) list
   10.20 -  | ML_Class of string * (vname * ((class * string) list * (string * itype) list));
   10.21 +  | ML_Class of string * (vname * ((class * class) list * (string * itype) list));
   10.22  
   10.23  fun print_product _ [] = NONE
   10.24    | print_product print [x] = SOME (print x)
   10.25 @@ -53,30 +53,35 @@
   10.26  
   10.27  fun print_sml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
   10.28    let
   10.29 -    fun print_tyco_expr (tyco, []) = (str o deresolve) tyco
   10.30 -      | print_tyco_expr (tyco, [ty]) =
   10.31 -          concat [print_typ BR ty, (str o deresolve) tyco]
   10.32 -      | print_tyco_expr (tyco, tys) =
   10.33 -          concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
   10.34 +    val deresolve_const = deresolve o Code_Symbol.Constant;
   10.35 +    val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
   10.36 +    val deresolve_class = deresolve o Code_Symbol.Type_Class;
   10.37 +    val deresolve_classrel = deresolve o Code_Symbol.Class_Relation;
   10.38 +    val deresolve_inst = deresolve o Code_Symbol.Class_Instance;
   10.39 +    fun print_tyco_expr (sym, []) = (str o deresolve) sym
   10.40 +      | print_tyco_expr (sym, [ty]) =
   10.41 +          concat [print_typ BR ty, (str o deresolve) sym]
   10.42 +      | print_tyco_expr (sym, tys) =
   10.43 +          concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
   10.44      and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
   10.45 -         of NONE => print_tyco_expr (tyco, tys)
   10.46 +         of NONE => print_tyco_expr (Code_Symbol.Type_Constructor tyco, tys)
   10.47            | SOME (_, print) => print print_typ fxy tys)
   10.48        | print_typ fxy (ITyVar v) = str ("'" ^ v);
   10.49 -    fun print_dicttyp (class, ty) = print_tyco_expr (class, [ty]);
   10.50 +    fun print_dicttyp (class, ty) = print_tyco_expr (Code_Symbol.Type_Class class, [ty]);
   10.51      fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
   10.52        (map_filter (fn (v, sort) =>
   10.53          (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
   10.54      fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
   10.55      fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
   10.56      fun print_classrels fxy [] ps = brackify fxy ps
   10.57 -      | print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve) classrel, brackify BR ps]
   10.58 +      | print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve_classrel) classrel, brackify BR ps]
   10.59        | print_classrels fxy classrels ps =
   10.60 -          brackify fxy [enum " o" "(" ")" (map (str o deresolve) classrels), brackify BR ps]
   10.61 +          brackify fxy [enum " o" "(" ")" (map (str o deresolve_classrel) classrels), brackify BR ps]
   10.62      fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
   10.63        print_classrels fxy classrels (print_plain_dict is_pseudo_fun fxy x)
   10.64      and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
   10.65 -          ((str o deresolve) inst ::
   10.66 -            (if is_pseudo_fun inst then [str "()"]
   10.67 +          ((str o deresolve_inst) inst ::
   10.68 +            (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
   10.69              else map_filter (print_dicts is_pseudo_fun BR) dss))
   10.70        | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
   10.71            [str (if k = 1 then first_upper v ^ "_"
   10.72 @@ -105,21 +110,22 @@
   10.73            in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
   10.74        | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
   10.75            (case Code_Thingol.unfold_const_app (#primitive case_expr)
   10.76 -           of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
   10.77 +           of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
   10.78 +                if is_none (const_syntax const)
   10.79                  then print_case is_pseudo_fun some_thm vars fxy case_expr
   10.80                  else print_app is_pseudo_fun some_thm vars fxy app
   10.81              | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
   10.82 -    and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
   10.83 -      if is_constr c then
   10.84 +    and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) =
   10.85 +      if is_constr sym then
   10.86          let val k = length dom in
   10.87            if k < 2 orelse length ts = k
   10.88 -          then (str o deresolve) c
   10.89 +          then (str o deresolve) sym
   10.90              :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
   10.91            else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
   10.92          end
   10.93 -      else if is_pseudo_fun c
   10.94 -        then (str o deresolve) c @@ str "()"
   10.95 -      else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss
   10.96 +      else if is_pseudo_fun sym
   10.97 +        then (str o deresolve) sym @@ str "()"
   10.98 +      else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss
   10.99          @ map (print_term is_pseudo_fun some_thm vars BR) ts
  10.100      and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
  10.101        (print_term is_pseudo_fun) const_syntax some_thm vars
  10.102 @@ -158,23 +164,23 @@
  10.103                :: map (print_select "|") clauses
  10.104              )
  10.105            end;
  10.106 -    fun print_val_decl print_typscheme (name, typscheme) = concat
  10.107 -      [str "val", str (deresolve name), str ":", print_typscheme typscheme];
  10.108 +    fun print_val_decl print_typscheme (sym, typscheme) = concat
  10.109 +      [str "val", str (deresolve sym), str ":", print_typscheme typscheme];
  10.110      fun print_datatype_decl definer (tyco, (vs, cos)) =
  10.111        let
  10.112 -        fun print_co ((co, _), []) = str (deresolve co)
  10.113 -          | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
  10.114 +        fun print_co ((co, _), []) = str (deresolve_const co)
  10.115 +          | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of",
  10.116                enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
  10.117        in
  10.118          concat (
  10.119            str definer
  10.120 -          :: print_tyco_expr (tyco, map ITyVar vs)
  10.121 +          :: print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs)
  10.122            :: str "="
  10.123            :: separate (str "|") (map print_co cos)
  10.124          )
  10.125        end;
  10.126      fun print_def is_pseudo_fun needs_typ definer
  10.127 -          (ML_Function (name, (vs_ty as (vs, ty), eq :: eqs))) =
  10.128 +          (ML_Function (const, (vs_ty as (vs, ty), eq :: eqs))) =
  10.129            let
  10.130              fun print_eqn definer ((ts, t), (some_thm, _)) =
  10.131                let
  10.132 @@ -184,12 +190,12 @@
  10.133                    |> intro_vars ((fold o Code_Thingol.fold_varnames)
  10.134                         (insert (op =)) ts []);
  10.135                  val prolog = if needs_typ then
  10.136 -                  concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty]
  10.137 -                    else (concat o map str) [definer, deresolve name];
  10.138 +                  concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty]
  10.139 +                    else (concat o map str) [definer, deresolve_const const];
  10.140                in
  10.141                  concat (
  10.142                    prolog
  10.143 -                  :: (if is_pseudo_fun name then [str "()"]
  10.144 +                  :: (if is_pseudo_fun (Code_Symbol.Constant const) then [str "()"]
  10.145                        else print_dict_args vs
  10.146                          @ map (print_term is_pseudo_fun some_thm vars BR) ts)
  10.147                    @ str "="
  10.148 @@ -199,53 +205,53 @@
  10.149              val shift = if null eqs then I else
  10.150                map (Pretty.block o single o Pretty.block o single);
  10.151            in pair
  10.152 -            (print_val_decl print_typscheme (name, vs_ty))
  10.153 +            (print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty))
  10.154              ((Pretty.block o Pretty.fbreaks o shift) (
  10.155                print_eqn definer eq
  10.156                :: map (print_eqn "|") eqs
  10.157              ))
  10.158            end
  10.159        | print_def is_pseudo_fun _ definer
  10.160 -          (ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) =
  10.161 +          (ML_Instance (inst as (tyco, class), { vs, superinsts, inst_params, ... })) =
  10.162            let
  10.163 -            fun print_super_instance (_, (classrel, x)) =
  10.164 +            fun print_super_instance (super_class, x) =
  10.165                concat [
  10.166 -                (str o Long_Name.base_name o deresolve) classrel,
  10.167 +                (str o Long_Name.base_name o deresolve_classrel) (class, super_class),
  10.168                  str "=",
  10.169 -                print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))
  10.170 +                print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), x)))
  10.171                ];
  10.172              fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
  10.173                concat [
  10.174 -                (str o Long_Name.base_name o deresolve) classparam,
  10.175 +                (str o Long_Name.base_name o deresolve_const) classparam,
  10.176                  str "=",
  10.177                  print_app (K false) (SOME thm) reserved NOBR (const, [])
  10.178                ];
  10.179            in pair
  10.180              (print_val_decl print_dicttypscheme
  10.181 -              (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
  10.182 +              (Code_Symbol.Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
  10.183              (concat (
  10.184                str definer
  10.185 -              :: (str o deresolve) inst
  10.186 -              :: (if is_pseudo_fun inst then [str "()"]
  10.187 +              :: (str o deresolve_inst) inst
  10.188 +              :: (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
  10.189                    else print_dict_args vs)
  10.190                @ str "="
  10.191                :: enum "," "{" "}"
  10.192                  (map print_super_instance superinsts
  10.193                    @ map print_classparam_instance inst_params)
  10.194                :: str ":"
  10.195 -              @@ print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
  10.196 +              @@ print_dicttyp (class, tyco `%% map (ITyVar o fst) vs)
  10.197              ))
  10.198            end;
  10.199 -    fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
  10.200 -          [print_val_decl print_typscheme (name, vs_ty)]
  10.201 +    fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair
  10.202 +          [print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty)]
  10.203            ((semicolon o map str) (
  10.204              (if n = 0 then "val" else "fun")
  10.205 -            :: deresolve name
  10.206 +            :: deresolve_const const
  10.207              :: replicate n "_"
  10.208              @ "="
  10.209              :: "raise"
  10.210              :: "Fail"
  10.211 -            @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name
  10.212 +            @@ ML_Syntax.print_string const
  10.213            ))
  10.214        | print_stmt (ML_Val binding) =
  10.215            let
  10.216 @@ -257,11 +263,11 @@
  10.217        | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
  10.218            let
  10.219              val print_def' = print_def (member (op =) pseudo_funs) false;
  10.220 -            fun print_pseudo_fun name = concat [
  10.221 +            fun print_pseudo_fun sym = concat [
  10.222                  str "val",
  10.223 -                (str o deresolve) name,
  10.224 +                (str o deresolve) sym,
  10.225                  str "=",
  10.226 -                (str o deresolve) name,
  10.227 +                (str o deresolve) sym,
  10.228                  str "();"
  10.229                ];
  10.230              val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
  10.231 @@ -273,7 +279,7 @@
  10.232            end
  10.233       | print_stmt (ML_Datas [(tyco, (vs, []))]) =
  10.234            let
  10.235 -            val ty_p = print_tyco_expr (tyco, map ITyVar vs);
  10.236 +            val ty_p = print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs);
  10.237            in
  10.238              pair
  10.239              [concat [str "type", ty_p]]
  10.240 @@ -288,42 +294,42 @@
  10.241              sig_ps
  10.242              (Pretty.chunks (ps @| semicolon [p]))
  10.243            end
  10.244 -     | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
  10.245 +     | print_stmt (ML_Class (class, (v, (classrels, classparams)))) =
  10.246            let
  10.247              fun print_field s p = concat [str s, str ":", p];
  10.248              fun print_proj s p = semicolon
  10.249                (map str ["val", s, "=", "#" ^ s, ":"] @| p);
  10.250 -            fun print_super_class_decl (super_class, classrel) =
  10.251 +            fun print_super_class_decl (classrel as (_, super_class)) =
  10.252                print_val_decl print_dicttypscheme
  10.253 -                (classrel, ([(v, [class])], (super_class, ITyVar v)));
  10.254 -            fun print_super_class_field (super_class, classrel) =
  10.255 -              print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v));
  10.256 -            fun print_super_class_proj (super_class, classrel) =
  10.257 -              print_proj (deresolve classrel)
  10.258 +                (Code_Symbol.Class_Relation classrel, ([(v, [class])], (super_class, ITyVar v)));
  10.259 +            fun print_super_class_field (classrel as (_, super_class)) =
  10.260 +              print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v));
  10.261 +            fun print_super_class_proj (classrel as (_, super_class)) =
  10.262 +              print_proj (deresolve_classrel classrel)
  10.263                  (print_dicttypscheme ([(v, [class])], (super_class, ITyVar v)));
  10.264              fun print_classparam_decl (classparam, ty) =
  10.265                print_val_decl print_typscheme
  10.266 -                (classparam, ([(v, [class])], ty));
  10.267 +                (Code_Symbol.Constant classparam, ([(v, [class])], ty));
  10.268              fun print_classparam_field (classparam, ty) =
  10.269 -              print_field (deresolve classparam) (print_typ NOBR ty);
  10.270 +              print_field (deresolve_const classparam) (print_typ NOBR ty);
  10.271              fun print_classparam_proj (classparam, ty) =
  10.272 -              print_proj (deresolve classparam)
  10.273 +              print_proj (deresolve_const classparam)
  10.274                  (print_typscheme ([(v, [class])], ty));
  10.275            in pair
  10.276              (concat [str "type", print_dicttyp (class, ITyVar v)]
  10.277 -              :: map print_super_class_decl super_classes
  10.278 +              :: map print_super_class_decl classrels
  10.279                @ map print_classparam_decl classparams)
  10.280              (Pretty.chunks (
  10.281                concat [
  10.282                  str ("type '" ^ v),
  10.283 -                (str o deresolve) class,
  10.284 +                (str o deresolve_class) class,
  10.285                  str "=",
  10.286                  enum "," "{" "};" (
  10.287 -                  map print_super_class_field super_classes
  10.288 +                  map print_super_class_field classrels
  10.289                    @ map print_classparam_field classparams
  10.290                  )
  10.291                ]
  10.292 -              :: map print_super_class_proj super_classes
  10.293 +              :: map print_super_class_proj classrels
  10.294                @ map print_classparam_proj classparams
  10.295              ))
  10.296            end;
  10.297 @@ -353,29 +359,34 @@
  10.298  
  10.299  fun print_ocaml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
  10.300    let
  10.301 -    fun print_tyco_expr (tyco, []) = (str o deresolve) tyco
  10.302 -      | print_tyco_expr (tyco, [ty]) =
  10.303 -          concat [print_typ BR ty, (str o deresolve) tyco]
  10.304 -      | print_tyco_expr (tyco, tys) =
  10.305 -          concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
  10.306 +    val deresolve_const = deresolve o Code_Symbol.Constant;
  10.307 +    val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
  10.308 +    val deresolve_class = deresolve o Code_Symbol.Type_Class;
  10.309 +    val deresolve_classrel = deresolve o Code_Symbol.Class_Relation;
  10.310 +    val deresolve_inst = deresolve o Code_Symbol.Class_Instance;
  10.311 +    fun print_tyco_expr (sym, []) = (str o deresolve) sym
  10.312 +      | print_tyco_expr (sym, [ty]) =
  10.313 +          concat [print_typ BR ty, (str o deresolve) sym]
  10.314 +      | print_tyco_expr (sym, tys) =
  10.315 +          concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
  10.316      and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
  10.317 -         of NONE => print_tyco_expr (tyco, tys)
  10.318 +         of NONE => print_tyco_expr (Code_Symbol.Type_Constructor tyco, tys)
  10.319            | SOME (_, print) => print print_typ fxy tys)
  10.320        | print_typ fxy (ITyVar v) = str ("'" ^ v);
  10.321 -    fun print_dicttyp (class, ty) = print_tyco_expr (class, [ty]);
  10.322 +    fun print_dicttyp (class, ty) = print_tyco_expr (Code_Symbol.Type_Class class, [ty]);
  10.323      fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
  10.324        (map_filter (fn (v, sort) =>
  10.325          (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
  10.326      fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
  10.327      fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
  10.328      val print_classrels =
  10.329 -      fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve) classrel])
  10.330 +      fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve_classrel) classrel])
  10.331      fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
  10.332        print_plain_dict is_pseudo_fun fxy x
  10.333        |> print_classrels classrels
  10.334      and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
  10.335 -          brackify BR ((str o deresolve) inst ::
  10.336 -            (if is_pseudo_fun inst then [str "()"]
  10.337 +          brackify BR ((str o deresolve_inst) inst ::
  10.338 +            (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
  10.339              else map_filter (print_dicts is_pseudo_fun BR) dss))
  10.340        | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
  10.341            str (if k = 1 then "_" ^ first_upper v
  10.342 @@ -401,21 +412,22 @@
  10.343            in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
  10.344        | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
  10.345            (case Code_Thingol.unfold_const_app (#primitive case_expr)
  10.346 -           of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
  10.347 +           of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
  10.348 +                if is_none (const_syntax const)
  10.349                  then print_case is_pseudo_fun some_thm vars fxy case_expr
  10.350                  else print_app is_pseudo_fun some_thm vars fxy app
  10.351              | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
  10.352 -    and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
  10.353 -      if is_constr c then
  10.354 +    and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) =
  10.355 +      if is_constr sym then
  10.356          let val k = length dom in
  10.357            if length ts = k
  10.358 -          then (str o deresolve) c
  10.359 +          then (str o deresolve) sym
  10.360              :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
  10.361            else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
  10.362          end
  10.363 -      else if is_pseudo_fun c
  10.364 -        then (str o deresolve) c @@ str "()"
  10.365 -      else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss
  10.366 +      else if is_pseudo_fun sym
  10.367 +        then (str o deresolve) sym @@ str "()"
  10.368 +      else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss
  10.369          @ map (print_term is_pseudo_fun some_thm vars BR) ts
  10.370      and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
  10.371        (print_term is_pseudo_fun) const_syntax some_thm vars
  10.372 @@ -449,23 +461,23 @@
  10.373                :: map (print_select "|") clauses
  10.374              )
  10.375            end;
  10.376 -    fun print_val_decl print_typscheme (name, typscheme) = concat
  10.377 -      [str "val", str (deresolve name), str ":", print_typscheme typscheme];
  10.378 +    fun print_val_decl print_typscheme (sym, typscheme) = concat
  10.379 +      [str "val", str (deresolve sym), str ":", print_typscheme typscheme];
  10.380      fun print_datatype_decl definer (tyco, (vs, cos)) =
  10.381        let
  10.382 -        fun print_co ((co, _), []) = str (deresolve co)
  10.383 -          | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
  10.384 +        fun print_co ((co, _), []) = str (deresolve_const co)
  10.385 +          | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of",
  10.386                enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
  10.387        in
  10.388          concat (
  10.389            str definer
  10.390 -          :: print_tyco_expr (tyco, map ITyVar vs)
  10.391 +          :: print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs)
  10.392            :: str "="
  10.393            :: separate (str "|") (map print_co cos)
  10.394          )
  10.395        end;
  10.396      fun print_def is_pseudo_fun needs_typ definer
  10.397 -          (ML_Function (name, (vs_ty as (vs, ty), eqs))) =
  10.398 +          (ML_Function (const, (vs_ty as (vs, ty), eqs))) =
  10.399            let
  10.400              fun print_eqn ((ts, t), (some_thm, _)) =
  10.401                let
  10.402 @@ -529,57 +541,57 @@
  10.403                      )
  10.404                    end;
  10.405              val prolog = if needs_typ then
  10.406 -              concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty]
  10.407 -                else (concat o map str) [definer, deresolve name];
  10.408 +              concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty]
  10.409 +                else (concat o map str) [definer, deresolve_const const];
  10.410            in pair
  10.411 -            (print_val_decl print_typscheme (name, vs_ty))
  10.412 +            (print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty))
  10.413              (concat (
  10.414                prolog
  10.415                :: print_dict_args vs
  10.416 -              @| print_eqns (is_pseudo_fun name) eqs
  10.417 +              @| print_eqns (is_pseudo_fun (Code_Symbol.Constant const)) eqs
  10.418              ))
  10.419            end
  10.420        | print_def is_pseudo_fun _ definer
  10.421 -          (ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) =
  10.422 +          (ML_Instance (inst as (tyco, class), { vs, superinsts, inst_params, ... })) =
  10.423            let
  10.424 -            fun print_super_instance (_, (classrel, x)) =
  10.425 +            fun print_super_instance (super_class, x) =
  10.426                concat [
  10.427 -                (str o deresolve) classrel,
  10.428 +                (str o deresolve_classrel) (class, super_class),
  10.429                  str "=",
  10.430 -                print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))
  10.431 +                print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), x)))
  10.432                ];
  10.433              fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
  10.434                concat [
  10.435 -                (str o deresolve) classparam,
  10.436 +                (str o deresolve_const) classparam,
  10.437                  str "=",
  10.438                  print_app (K false) (SOME thm) reserved NOBR (const, [])
  10.439                ];
  10.440            in pair
  10.441              (print_val_decl print_dicttypscheme
  10.442 -              (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
  10.443 +              (Code_Symbol.Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
  10.444              (concat (
  10.445                str definer
  10.446 -              :: (str o deresolve) inst
  10.447 -              :: (if is_pseudo_fun inst then [str "()"]
  10.448 +              :: (str o deresolve_inst) inst
  10.449 +              :: (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
  10.450                    else print_dict_args vs)
  10.451                @ str "="
  10.452                @@ brackets [
  10.453                  enum_default "()" ";" "{" "}" (map print_super_instance superinsts
  10.454                    @ map print_classparam_instance inst_params),
  10.455                  str ":",
  10.456 -                print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
  10.457 +                print_dicttyp (class, tyco `%% map (ITyVar o fst) vs)
  10.458                ]
  10.459              ))
  10.460            end;
  10.461 -     fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
  10.462 -          [print_val_decl print_typscheme (name, vs_ty)]
  10.463 +     fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair
  10.464 +          [print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty)]
  10.465            ((doublesemicolon o map str) (
  10.466              "let"
  10.467 -            :: deresolve name
  10.468 +            :: deresolve_const const
  10.469              :: replicate n "_"
  10.470              @ "="
  10.471              :: "failwith"
  10.472 -            @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name
  10.473 +            @@ ML_Syntax.print_string const
  10.474            ))
  10.475        | print_stmt (ML_Val binding) =
  10.476            let
  10.477 @@ -591,11 +603,11 @@
  10.478        | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
  10.479            let
  10.480              val print_def' = print_def (member (op =) pseudo_funs) false;
  10.481 -            fun print_pseudo_fun name = concat [
  10.482 +            fun print_pseudo_fun sym = concat [
  10.483                  str "let",
  10.484 -                (str o deresolve) name,
  10.485 +                (str o deresolve) sym,
  10.486                  str "=",
  10.487 -                (str o deresolve) name,
  10.488 +                (str o deresolve) sym,
  10.489                  str "();;"
  10.490                ];
  10.491              val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
  10.492 @@ -607,7 +619,7 @@
  10.493            end
  10.494       | print_stmt (ML_Datas [(tyco, (vs, []))]) =
  10.495            let
  10.496 -            val ty_p = print_tyco_expr (tyco, map ITyVar vs);
  10.497 +            val ty_p = print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs);
  10.498            in
  10.499              pair
  10.500              [concat [str "type", ty_p]]
  10.501 @@ -622,26 +634,26 @@
  10.502              sig_ps
  10.503              (Pretty.chunks (ps @| doublesemicolon [p]))
  10.504            end
  10.505 -     | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
  10.506 +     | print_stmt (ML_Class (class, (v, (classrels, classparams)))) =
  10.507            let
  10.508              fun print_field s p = concat [str s, str ":", p];
  10.509 -            fun print_super_class_field (super_class, classrel) =
  10.510 -              print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v));
  10.511 +            fun print_super_class_field (classrel as (_, super_class)) =
  10.512 +              print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v));
  10.513              fun print_classparam_decl (classparam, ty) =
  10.514                print_val_decl print_typscheme
  10.515 -                (classparam, ([(v, [class])], ty));
  10.516 +                (Code_Symbol.Constant classparam, ([(v, [class])], ty));
  10.517              fun print_classparam_field (classparam, ty) =
  10.518 -              print_field (deresolve classparam) (print_typ NOBR ty);
  10.519 +              print_field (deresolve_const classparam) (print_typ NOBR ty);
  10.520              val w = "_" ^ first_upper v;
  10.521              fun print_classparam_proj (classparam, _) =
  10.522 -              (concat o map str) ["let", deresolve classparam, w, "=",
  10.523 -                w ^ "." ^ deresolve classparam ^ ";;"];
  10.524 +              (concat o map str) ["let", deresolve_const classparam, w, "=",
  10.525 +                w ^ "." ^ deresolve_const classparam ^ ";;"];
  10.526              val type_decl_p = concat [
  10.527                  str ("type '" ^ v),
  10.528 -                (str o deresolve) class,
  10.529 +                (str o deresolve_class) class,
  10.530                  str "=",
  10.531                  enum_default "unit" ";" "{" "}" (
  10.532 -                  map print_super_class_field super_classes
  10.533 +                  map print_super_class_field classrels
  10.534                    @ map print_classparam_field classparams
  10.535                  )
  10.536                ];
  10.537 @@ -694,7 +706,7 @@
  10.538  
  10.539  (** SML/OCaml generic part **)
  10.540  
  10.541 -fun ml_program_of_program ctxt symbol_of module_name reserved identifiers program =
  10.542 +fun ml_program_of_program ctxt module_name reserved identifiers program =
  10.543    let
  10.544      fun namify_const upper base (nsp_const, nsp_type) =
  10.545        let
  10.546 @@ -712,76 +724,76 @@
  10.547        | namify_stmt (Code_Thingol.Classrel _) = namify_const false
  10.548        | namify_stmt (Code_Thingol.Classparam _) = namify_const false
  10.549        | namify_stmt (Code_Thingol.Classinst _) = namify_const false;
  10.550 -    fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, ((tysm as (vs, ty), raw_eqs), _))) =
  10.551 +    fun ml_binding_of_stmt (sym as Code_Symbol.Constant const, Code_Thingol.Fun ((tysm as (vs, ty), raw_eqs), _)) =
  10.552            let
  10.553              val eqs = filter (snd o snd) raw_eqs;
  10.554 -            val (eqs', some_value_name) = if null (filter_out (null o snd) vs) then case eqs
  10.555 +            val (eqs', some_sym) = if null (filter_out (null o snd) vs) then case eqs
  10.556                 of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
  10.557                    then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE)
  10.558 -                  else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name))
  10.559 +                  else (eqs, SOME (sym, member (op =) (Code_Thingol.add_constsyms t []) sym))
  10.560                  | _ => (eqs, NONE)
  10.561                else (eqs, NONE)
  10.562 -          in (ML_Function (name, (tysm, eqs')), some_value_name) end
  10.563 -      | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as { vs, ... })) =
  10.564 -          (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
  10.565 -      | ml_binding_of_stmt (name, _) =
  10.566 +          in (ML_Function (const, (tysm, eqs')), some_sym) end
  10.567 +      | ml_binding_of_stmt (sym as Code_Symbol.Class_Instance inst, Code_Thingol.Classinst (stmt as { vs, ... })) =
  10.568 +          (ML_Instance (inst, stmt), if forall (null o snd) vs then SOME (sym, false) else NONE)
  10.569 +      | ml_binding_of_stmt (sym, _) =
  10.570            error ("Binding block containing illegal statement: " ^ 
  10.571 -            (Code_Symbol.quote_symbol ctxt o symbol_of) name)
  10.572 -    fun modify_fun (name, stmt) =
  10.573 +            Code_Symbol.quote ctxt sym)
  10.574 +    fun modify_fun (sym, stmt) =
  10.575        let
  10.576 -        val (binding, some_value_name) = ml_binding_of_stmt (name, stmt);
  10.577 +        val (binding, some_value_sym) = ml_binding_of_stmt (sym, stmt);
  10.578          val ml_stmt = case binding
  10.579 -         of ML_Function (name, ((vs, ty), [])) =>
  10.580 -              ML_Exc (name, ((vs, ty),
  10.581 +         of ML_Function (const, ((vs, ty), [])) =>
  10.582 +              ML_Exc (const, ((vs, ty),
  10.583                  (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty))
  10.584 -          | _ => case some_value_name
  10.585 +          | _ => case some_value_sym
  10.586               of NONE => ML_Funs ([binding], [])
  10.587 -              | SOME (name, true) => ML_Funs ([binding], [name])
  10.588 -              | SOME (name, false) => ML_Val binding
  10.589 +              | SOME (sym, true) => ML_Funs ([binding], [sym])
  10.590 +              | SOME (sym, false) => ML_Val binding
  10.591        in SOME ml_stmt end;
  10.592      fun modify_funs stmts = single (SOME
  10.593        (ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))
  10.594      fun modify_datatypes stmts = single (SOME
  10.595        (ML_Datas (map_filter
  10.596 -        (fn (name, Code_Thingol.Datatype (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts)))
  10.597 +        (fn (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype stmt) => SOME (tyco, stmt) | _ => NONE) stmts)))
  10.598      fun modify_class stmts = single (SOME
  10.599        (ML_Class (the_single (map_filter
  10.600 -        (fn (name, Code_Thingol.Class (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts))))
  10.601 +        (fn (Code_Symbol.Type_Class class, Code_Thingol.Class stmt) => SOME (class, stmt) | _ => NONE) stmts))))
  10.602      fun modify_stmts ([stmt as (_, stmt' as Code_Thingol.Fun _)]) =
  10.603            if Code_Thingol.is_case stmt' then [] else [modify_fun stmt]
  10.604 -      | modify_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
  10.605 +      | modify_stmts ((stmts as (_, Code_Thingol.Fun _) :: _)) =
  10.606            modify_funs (filter_out (Code_Thingol.is_case o snd) stmts)
  10.607 -      | modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =
  10.608 +      | modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _) :: _)) =
  10.609            modify_datatypes stmts
  10.610 -      | modify_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) =
  10.611 +      | modify_stmts ((stmts as (_, Code_Thingol.Datatype _) :: _)) =
  10.612            modify_datatypes stmts
  10.613 -      | modify_stmts ((stmts as (_, Code_Thingol.Class _)::_)) =
  10.614 +      | modify_stmts ((stmts as (_, Code_Thingol.Class _) :: _)) =
  10.615            modify_class stmts
  10.616 -      | modify_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) =
  10.617 +      | modify_stmts ((stmts as (_, Code_Thingol.Classrel _) :: _)) =
  10.618            modify_class stmts
  10.619 -      | modify_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =
  10.620 +      | modify_stmts ((stmts as (_, Code_Thingol.Classparam _) :: _)) =
  10.621            modify_class stmts
  10.622        | modify_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =
  10.623            [modify_fun stmt]
  10.624 -      | modify_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
  10.625 +      | modify_stmts ((stmts as (_, Code_Thingol.Classinst _) :: _)) =
  10.626            modify_funs stmts
  10.627        | modify_stmts stmts = error ("Illegal mutual dependencies: " ^
  10.628 -          (Library.commas o map (Code_Symbol.quote_symbol ctxt o symbol_of o fst)) stmts);
  10.629 +          (Library.commas o map (Code_Symbol.quote ctxt o fst)) stmts);
  10.630    in
  10.631 -    Code_Namespace.hierarchical_program ctxt symbol_of {
  10.632 +    Code_Namespace.hierarchical_program ctxt {
  10.633        module_name = module_name, reserved = reserved, identifiers = identifiers,
  10.634        empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt,
  10.635        cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
  10.636    end;
  10.637  
  10.638  fun serialize_ml print_ml_module print_ml_stmt with_signatures ctxt
  10.639 -    { symbol_of, module_name, reserved_syms, identifiers, includes,
  10.640 +    { module_name, reserved_syms, identifiers, includes,
  10.641        class_syntax, tyco_syntax, const_syntax } program =
  10.642    let
  10.643  
  10.644      (* build program *)
  10.645      val { deresolver, hierarchical_program = ml_program } =
  10.646 -      ml_program_of_program ctxt symbol_of module_name (Name.make_context reserved_syms) identifiers program;
  10.647 +      ml_program_of_program ctxt module_name (Name.make_context reserved_syms) identifiers program;
  10.648  
  10.649      (* print statements *)
  10.650      fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt
  10.651 @@ -803,7 +815,7 @@
  10.652          lift_markup = apsnd } ml_program));
  10.653      fun write width NONE = writeln o format [] width
  10.654        | write width (SOME p) = File.write p o format [] width;
  10.655 -    fun prepare names width p = ([("", format names width p)], try (deresolver []));
  10.656 +    fun prepare syms width p = ([("", format syms width p)], try (deresolver []));
  10.657    in
  10.658      Code_Target.serialization write prepare p
  10.659    end;
    11.1 --- a/src/Tools/Code/code_namespace.ML	Sat Jan 25 23:50:49 2014 +0100
    11.2 +++ b/src/Tools/Code/code_namespace.ML	Sat Jan 25 23:50:49 2014 +0100
    11.3 @@ -7,32 +7,32 @@
    11.4  signature CODE_NAMESPACE =
    11.5  sig
    11.6    type flat_program
    11.7 -  val flat_program: Proof.context -> (string -> Code_Symbol.symbol)
    11.8 +  val flat_program: Proof.context
    11.9      -> { module_prefix: string, module_name: string,
   11.10      reserved: Name.context, identifiers: Code_Target.identifier_data, empty_nsp: 'a,
   11.11      namify_stmt: Code_Thingol.stmt -> string -> 'a -> string * 'a,
   11.12      modify_stmt: Code_Thingol.stmt -> Code_Thingol.stmt option }
   11.13        -> Code_Thingol.program
   11.14 -      -> { deresolver: string -> string -> string,
   11.15 +      -> { deresolver: string -> Code_Symbol.symbol -> string,
   11.16             flat_program: flat_program }
   11.17  
   11.18    datatype ('a, 'b) node =
   11.19        Dummy
   11.20      | Stmt of 'a
   11.21 -    | Module of ('b * (string * ('a, 'b) node) Graph.T)
   11.22 +    | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T)
   11.23    type ('a, 'b) hierarchical_program
   11.24 -  val hierarchical_program: Proof.context -> (string -> Code_Symbol.symbol)
   11.25 +  val hierarchical_program: Proof.context
   11.26      -> { module_name: string,
   11.27      reserved: Name.context, identifiers: Code_Target.identifier_data,
   11.28      empty_nsp: 'c, namify_module: string -> 'c -> string * 'c,
   11.29      namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c,
   11.30 -    cyclic_modules: bool, empty_data: 'b, memorize_data: string -> 'b -> 'b,
   11.31 -    modify_stmts: (string * Code_Thingol.stmt) list -> 'a option list }
   11.32 +    cyclic_modules: bool, empty_data: 'b, memorize_data: Code_Symbol.symbol -> 'b -> 'b,
   11.33 +    modify_stmts: (Code_Symbol.symbol * Code_Thingol.stmt) list -> 'a option list }
   11.34        -> Code_Thingol.program
   11.35 -      -> { deresolver: string list -> string -> string,
   11.36 +      -> { deresolver: string list -> Code_Symbol.symbol -> string,
   11.37             hierarchical_program: ('a, 'b) hierarchical_program }
   11.38    val print_hierarchical: { print_module: string list -> string -> 'b -> 'c list -> 'c,
   11.39 -    print_stmt: string list -> string * 'a -> 'c,
   11.40 +    print_stmt: string list -> Code_Symbol.symbol * 'a -> 'c,
   11.41      lift_markup: (Pretty.T -> Pretty.T) -> 'c -> 'c }
   11.42        -> ('a, 'b) hierarchical_program -> 'c list
   11.43  end;
   11.44 @@ -42,24 +42,22 @@
   11.45  
   11.46  (** fundamental module name hierarchy **)
   11.47  
   11.48 -val split_name = apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
   11.49 -
   11.50 -fun lookup_identifier symbol_of identifiers name =
   11.51 -  Code_Symbol.lookup identifiers (symbol_of name)
   11.52 +fun lookup_identifier identifiers sym =
   11.53 +  Code_Symbol.lookup identifiers sym
   11.54    |> Option.map (split_last o Long_Name.explode);
   11.55  
   11.56 -fun force_identifier symbol_of fragments_tab force_module identifiers name =
   11.57 -  case lookup_identifier symbol_of identifiers name of
   11.58 -      NONE => (apfst (the o Symtab.lookup fragments_tab) o split_name) name
   11.59 +fun force_identifier ctxt fragments_tab force_module identifiers sym =
   11.60 +  case lookup_identifier identifiers sym of
   11.61 +      NONE => ((the o Symtab.lookup fragments_tab o Code_Symbol.namespace_prefix ctxt) sym, Code_Symbol.base_name sym)
   11.62      | SOME prefix_name => if null force_module then prefix_name
   11.63          else (force_module, snd prefix_name);
   11.64  
   11.65 -fun build_module_namespace { module_prefix, module_identifiers, reserved } program =
   11.66 +fun build_module_namespace ctxt { module_prefix, module_identifiers, reserved } program =
   11.67    let
   11.68      fun alias_fragments name = case module_identifiers name
   11.69       of SOME name' => Long_Name.explode name'
   11.70        | NONE => map (fn name => fst (Name.variant name reserved)) (Long_Name.explode name);
   11.71 -    val module_names = Graph.fold (insert (op =) o fst o split_name o fst) program [];
   11.72 +    val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.namespace_prefix ctxt o fst) program [];
   11.73    in
   11.74      fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ alias_fragments name))
   11.75        module_names Symtab.empty
   11.76 @@ -68,9 +66,9 @@
   11.77  
   11.78  (** flat program structure **)
   11.79  
   11.80 -type flat_program = ((string * Code_Thingol.stmt option) Graph.T * (string * string list) list) Graph.T;
   11.81 +type flat_program = ((string * Code_Thingol.stmt option) Code_Symbol.Graph.T * (string * Code_Symbol.symbol list) list) Graph.T;
   11.82  
   11.83 -fun flat_program ctxt symbol_of { module_prefix, module_name, reserved,
   11.84 +fun flat_program ctxt { module_prefix, module_name, reserved,
   11.85      identifiers, empty_nsp, namify_stmt, modify_stmt } program =
   11.86    let
   11.87  
   11.88 @@ -78,70 +76,70 @@
   11.89      val module_identifiers = if module_name = ""
   11.90        then Code_Symbol.lookup_module_data identifiers
   11.91        else K (SOME module_name);
   11.92 -    val fragments_tab = build_module_namespace { module_prefix = module_prefix,
   11.93 +    val fragments_tab = build_module_namespace ctxt { module_prefix = module_prefix,
   11.94        module_identifiers = module_identifiers, reserved = reserved } program;
   11.95 -    val prep_name = force_identifier symbol_of fragments_tab (Long_Name.explode module_name) identifiers
   11.96 +    val prep_sym = force_identifier ctxt fragments_tab (Long_Name.explode module_name) identifiers
   11.97        #>> Long_Name.implode;
   11.98  
   11.99      (* distribute statements over hierarchy *)
  11.100 -    fun add_stmt name stmt =
  11.101 +    fun add_stmt sym stmt =
  11.102        let
  11.103 -        val (module_name, base) = prep_name name;
  11.104 +        val (module_name, base) = prep_sym sym;
  11.105        in
  11.106 -        Graph.default_node (module_name, (Graph.empty, []))
  11.107 -        #> (Graph.map_node module_name o apfst) (Graph.new_node (name, (base, stmt)))
  11.108 +        Graph.default_node (module_name, (Code_Symbol.Graph.empty, []))
  11.109 +        #> (Graph.map_node module_name o apfst) (Code_Symbol.Graph.new_node (sym, (base, stmt)))
  11.110        end;
  11.111 -    fun add_dependency name name' =
  11.112 +    fun add_dependency sym sym' =
  11.113        let
  11.114 -        val (module_name, _) = prep_name name;
  11.115 -        val (module_name', _) = prep_name name';
  11.116 +        val (module_name, _) = prep_sym sym;
  11.117 +        val (module_name', _) = prep_sym sym';
  11.118        in if module_name = module_name'
  11.119 -        then (Graph.map_node module_name o apfst) (Graph.add_edge (name, name'))
  11.120 -        else (Graph.map_node module_name o apsnd) (AList.map_default (op =) (module_name', []) (insert (op =) name'))
  11.121 +        then (Graph.map_node module_name o apfst) (Code_Symbol.Graph.add_edge (sym, sym'))
  11.122 +        else (Graph.map_node module_name o apsnd) (AList.map_default (op =) (module_name', []) (insert (op =) sym'))
  11.123        end;
  11.124      val proto_program = Graph.empty
  11.125 -      |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
  11.126 -      |> Graph.fold (fn (name, (_, (_, names))) =>
  11.127 -          Graph.Keys.fold (add_dependency name) names) program;
  11.128 +      |> Code_Symbol.Graph.fold (fn (sym, (stmt, _)) => add_stmt sym stmt) program
  11.129 +      |> Code_Symbol.Graph.fold (fn (sym, (_, (_, syms))) =>
  11.130 +          Code_Symbol.Graph.Keys.fold (add_dependency sym) syms) program;
  11.131  
  11.132      (* name declarations and statement modifications *)
  11.133 -    fun declare name (base, stmt) (gr, nsp) = 
  11.134 +    fun declare sym (base, stmt) (gr, nsp) = 
  11.135        let
  11.136          val (base', nsp') = namify_stmt stmt base nsp;
  11.137 -        val gr' = (Graph.map_node name o apfst) (K base') gr;
  11.138 +        val gr' = (Code_Symbol.Graph.map_node sym o apfst) (K base') gr;
  11.139        in (gr', nsp') end;
  11.140      fun declarations gr = (gr, empty_nsp)
  11.141 -      |> fold (fn name => declare name (Graph.get_node gr name)) (Graph.keys gr) 
  11.142 +      |> fold (fn sym => declare sym (Code_Symbol.Graph.get_node gr sym)) (Code_Symbol.Graph.keys gr) 
  11.143        |> fst
  11.144 -      |> (Graph.map o K o apsnd) modify_stmt;
  11.145 +      |> (Code_Symbol.Graph.map o K o apsnd) modify_stmt;
  11.146      val flat_program = proto_program
  11.147        |> (Graph.map o K o apfst) declarations;
  11.148  
  11.149      (* qualified and unqualified imports, deresolving *)
  11.150 -    fun base_deresolver name = fst (Graph.get_node
  11.151 -      (fst (Graph.get_node flat_program (fst (prep_name name)))) name);
  11.152 +    fun base_deresolver sym = fst (Code_Symbol.Graph.get_node
  11.153 +      (fst (Graph.get_node flat_program (fst (prep_sym sym)))) sym);
  11.154      fun classify_names gr imports =
  11.155        let
  11.156          val import_tab = maps
  11.157 -          (fn (module_name, names) => map (rpair module_name) names) imports;
  11.158 -        val imported_names = map fst import_tab;
  11.159 -        val here_names = Graph.keys gr;
  11.160 +          (fn (module_name, syms) => map (rpair module_name) syms) imports;
  11.161 +        val imported_syms = map fst import_tab;
  11.162 +        val here_syms = Code_Symbol.Graph.keys gr;
  11.163        in
  11.164 -        Symtab.empty
  11.165 -        |> fold (fn name => Symtab.update (name, base_deresolver name)) here_names
  11.166 -        |> fold (fn name => Symtab.update (name,
  11.167 -            Long_Name.append (the (AList.lookup (op =) import_tab name))
  11.168 -              (base_deresolver name))) imported_names
  11.169 +        Code_Symbol.Table.empty
  11.170 +        |> fold (fn sym => Code_Symbol.Table.update (sym, base_deresolver sym)) here_syms
  11.171 +        |> fold (fn sym => Code_Symbol.Table.update (sym,
  11.172 +            Long_Name.append (the (AList.lookup (op =) import_tab sym))
  11.173 +              (base_deresolver sym))) imported_syms
  11.174        end;
  11.175      val deresolver_tab = Symtab.make (AList.make
  11.176        (uncurry classify_names o Graph.get_node flat_program)
  11.177          (Graph.keys flat_program));
  11.178 -    fun deresolver "" name =
  11.179 -          Long_Name.append (fst (prep_name name)) (base_deresolver name)
  11.180 -      | deresolver module_name name =
  11.181 -          the (Symtab.lookup (the (Symtab.lookup deresolver_tab module_name)) name)
  11.182 +    fun deresolver "" sym =
  11.183 +          Long_Name.append (fst (prep_sym sym)) (base_deresolver sym)
  11.184 +      | deresolver module_name sym =
  11.185 +          the (Code_Symbol.Table.lookup (the (Symtab.lookup deresolver_tab module_name)) sym)
  11.186            handle Option.Option => error ("Unknown statement name: "
  11.187 -            ^ (Code_Symbol.quote_symbol ctxt o symbol_of) name);
  11.188 +            ^ Code_Symbol.quote ctxt sym);
  11.189  
  11.190    in { deresolver = deresolver, flat_program = flat_program } end;
  11.191  
  11.192 @@ -151,18 +149,18 @@
  11.193  datatype ('a, 'b) node =
  11.194      Dummy
  11.195    | Stmt of 'a
  11.196 -  | Module of ('b * (string * ('a, 'b) node) Graph.T);
  11.197 +  | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T);
  11.198  
  11.199 -type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Graph.T;
  11.200 +type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Code_Symbol.Graph.T;
  11.201  
  11.202  fun map_module_content f (Module content) = Module (f content);
  11.203  
  11.204  fun map_module [] = I
  11.205    | map_module (name_fragment :: name_fragments) =
  11.206 -      apsnd o Graph.map_node name_fragment o apsnd o map_module_content
  11.207 +      apsnd o Code_Symbol.Graph.map_node (Code_Symbol.Module name_fragment) o apsnd o map_module_content
  11.208          o map_module name_fragments;
  11.209  
  11.210 -fun hierarchical_program ctxt symbol_of { module_name, reserved, identifiers, empty_nsp,
  11.211 +fun hierarchical_program ctxt { module_name, reserved, identifiers, empty_nsp,
  11.212        namify_module, namify_stmt, cyclic_modules, empty_data, memorize_data, modify_stmts } program =
  11.213    let
  11.214  
  11.215 @@ -170,95 +168,95 @@
  11.216      val module_identifiers = if module_name = ""
  11.217        then Code_Symbol.lookup_module_data identifiers
  11.218        else K (SOME module_name);
  11.219 -    val fragments_tab = build_module_namespace { module_prefix = "",
  11.220 +    val fragments_tab = build_module_namespace ctxt { module_prefix = "",
  11.221        module_identifiers = module_identifiers, reserved = reserved } program;
  11.222 -    val prep_name = force_identifier symbol_of fragments_tab (Long_Name.explode module_name) identifiers;
  11.223 +    val prep_sym = force_identifier ctxt fragments_tab (Long_Name.explode module_name) identifiers;
  11.224  
  11.225      (* building empty module hierarchy *)
  11.226 -    val empty_module = (empty_data, Graph.empty);
  11.227 +    val empty_module = (empty_data, Code_Symbol.Graph.empty);
  11.228      fun ensure_module name_fragment (data, nodes) =
  11.229 -      if can (Graph.get_node nodes) name_fragment then (data, nodes)
  11.230 +      if can (Code_Symbol.Graph.get_node nodes) (Code_Symbol.Module name_fragment) then (data, nodes)
  11.231        else (data,
  11.232 -        nodes |> Graph.new_node (name_fragment, (name_fragment, Module empty_module)));
  11.233 +        nodes |> Code_Symbol.Graph.new_node (Code_Symbol.Module name_fragment, (name_fragment, Module empty_module)));
  11.234      fun allocate_module [] = I
  11.235        | allocate_module (name_fragment :: name_fragments) =
  11.236            ensure_module name_fragment
  11.237 -          #> (apsnd o Graph.map_node name_fragment o apsnd o map_module_content o allocate_module) name_fragments;
  11.238 +          #> (apsnd o Code_Symbol.Graph.map_node (Code_Symbol.Module name_fragment) o apsnd o map_module_content o allocate_module) name_fragments;
  11.239      val empty_program =
  11.240        empty_module
  11.241        |> Symtab.fold (fn (_, fragments) => allocate_module fragments) fragments_tab
  11.242 -      |> Graph.fold (allocate_module o these o Option.map fst
  11.243 -          o lookup_identifier symbol_of identifiers o fst) program;
  11.244 +      |> Code_Symbol.Graph.fold (allocate_module o these o Option.map fst
  11.245 +          o lookup_identifier identifiers o fst) program;
  11.246  
  11.247      (* distribute statements over hierarchy *)
  11.248 -    fun add_stmt name stmt =
  11.249 +    fun add_stmt sym stmt =
  11.250        let
  11.251 -        val (name_fragments, base) = prep_name name;
  11.252 +        val (name_fragments, base) = prep_sym sym;
  11.253        in
  11.254 -        (map_module name_fragments o apsnd) (Graph.new_node (name, (base, Stmt stmt)))
  11.255 +        (map_module name_fragments o apsnd) (Code_Symbol.Graph.new_node (sym, (base, Stmt stmt)))
  11.256        end;
  11.257 -    fun add_dependency name name' =
  11.258 +    fun add_dependency sym sym' =
  11.259        let
  11.260 -        val (name_fragments, _) = prep_name name;
  11.261 -        val (name_fragments', _) = prep_name name';
  11.262 +        val (name_fragments, _) = prep_sym sym;
  11.263 +        val (name_fragments', _) = prep_sym sym';
  11.264          val (name_fragments_common, (diff, diff')) =
  11.265            chop_prefix (op =) (name_fragments, name_fragments');
  11.266          val is_module = not (null diff andalso null diff');
  11.267 -        val dep = pairself hd (diff @ [name], diff' @ [name']);
  11.268 +        val dep = pairself hd (map Code_Symbol.Module diff @ [sym], map Code_Symbol.Module diff' @ [sym']);
  11.269          val add_edge = if is_module andalso not cyclic_modules
  11.270 -          then (fn node => Graph.add_edge_acyclic dep node
  11.271 +          then (fn node => Code_Symbol.Graph.add_edge_acyclic dep node
  11.272              handle Graph.CYCLES _ => error ("Dependency "
  11.273 -              ^ (Code_Symbol.quote_symbol ctxt o symbol_of) name ^ " -> "
  11.274 -              ^ (Code_Symbol.quote_symbol ctxt o symbol_of) name'
  11.275 +              ^ Code_Symbol.quote ctxt sym ^ " -> "
  11.276 +              ^ Code_Symbol.quote ctxt sym'
  11.277                ^ " would result in module dependency cycle"))
  11.278 -          else Graph.add_edge dep
  11.279 +          else Code_Symbol.Graph.add_edge dep
  11.280        in (map_module name_fragments_common o apsnd) add_edge end;
  11.281      val proto_program = empty_program
  11.282 -      |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
  11.283 -      |> Graph.fold (fn (name, (_, (_, names))) =>
  11.284 -          Graph.Keys.fold (add_dependency name) names) program;
  11.285 +      |> Code_Symbol.Graph.fold (fn (sym, (stmt, _)) => add_stmt sym stmt) program
  11.286 +      |> Code_Symbol.Graph.fold (fn (sym, (_, (_, syms))) =>
  11.287 +          Code_Symbol.Graph.Keys.fold (add_dependency sym) syms) program;
  11.288  
  11.289      (* name declarations, data and statement modifications *)
  11.290      fun make_declarations nsps (data, nodes) =
  11.291        let
  11.292 -        val (module_fragments, stmt_names) = List.partition
  11.293 -          (fn name_fragment => case Graph.get_node nodes name_fragment
  11.294 -            of (_, Module _) => true | _ => false) (Graph.keys nodes);
  11.295 -        fun declare namify name (nsps, nodes) =
  11.296 +        val (module_fragments, stmt_syms) = List.partition
  11.297 +          (fn sym => case Code_Symbol.Graph.get_node nodes sym
  11.298 +            of (_, Module _) => true | _ => false) (Code_Symbol.Graph.keys nodes);
  11.299 +        fun declare namify sym (nsps, nodes) =
  11.300            let
  11.301 -            val (base, node) = Graph.get_node nodes name;
  11.302 +            val (base, node) = Code_Symbol.Graph.get_node nodes sym;
  11.303              val (base', nsps') = namify node base nsps;
  11.304 -            val nodes' = Graph.map_node name (K (base', node)) nodes;
  11.305 +            val nodes' = Code_Symbol.Graph.map_node sym (K (base', node)) nodes;
  11.306            in (nsps', nodes') end;
  11.307          val (nsps', nodes') = (nsps, nodes)
  11.308            |> fold (declare (K namify_module)) module_fragments
  11.309 -          |> fold (declare (namify_stmt o (fn Stmt stmt => stmt))) stmt_names;
  11.310 +          |> fold (declare (namify_stmt o (fn Stmt stmt => stmt))) stmt_syms;
  11.311          fun zip_fillup xs ys = xs ~~ ys @ replicate (length xs - length ys) NONE;
  11.312 -        fun select_names names = case filter (member (op =) stmt_names) names
  11.313 +        fun select_syms syms = case filter (member (op =) stmt_syms) syms
  11.314           of [] => NONE
  11.315 -          | xs => SOME xs;
  11.316 -        val modify_stmts' = AList.make (snd o Graph.get_node nodes)
  11.317 +          | syms => SOME syms;
  11.318 +        val modify_stmts' = AList.make (snd o Code_Symbol.Graph.get_node nodes)
  11.319            #> split_list
  11.320            ##> map (fn Stmt stmt => stmt)
  11.321 -          #> (fn (names, stmts) => zip_fillup names (modify_stmts (names ~~ stmts)));
  11.322 -        val stmtss' = (maps modify_stmts' o map_filter select_names o Graph.strong_conn) nodes;
  11.323 -        val nodes'' = Graph.map (fn name => apsnd (fn Module content => Module (make_declarations nsps' content)
  11.324 -            | _ => case AList.lookup (op =) stmtss' name of SOME (SOME stmt) => Stmt stmt | _ => Dummy)) nodes';
  11.325 -        val data' = fold memorize_data stmt_names data;
  11.326 +          #> (fn (syms, stmts) => zip_fillup syms (modify_stmts (syms ~~ stmts)));
  11.327 +        val stmtss' = (maps modify_stmts' o map_filter select_syms o Code_Symbol.Graph.strong_conn) nodes;
  11.328 +        val nodes'' = Code_Symbol.Graph.map (fn sym => apsnd (fn Module content => Module (make_declarations nsps' content)
  11.329 +            | _ => case AList.lookup (op =) stmtss' sym of SOME (SOME stmt) => Stmt stmt | _ => Dummy)) nodes';
  11.330 +        val data' = fold memorize_data stmt_syms data;
  11.331        in (data', nodes'') end;
  11.332      val (_, hierarchical_program) = make_declarations empty_nsp proto_program;
  11.333  
  11.334      (* deresolving *)
  11.335 -    fun deresolver prefix_fragments name =
  11.336 +    fun deresolver prefix_fragments sym =
  11.337        let
  11.338 -        val (name_fragments, _) = prep_name name;
  11.339 +        val (name_fragments, _) = prep_sym sym;
  11.340          val (_, (_, remainder)) = chop_prefix (op =) (prefix_fragments, name_fragments);
  11.341 -        val nodes = fold (fn name_fragment => fn nodes => case Graph.get_node nodes name_fragment
  11.342 +        val nodes = fold (fn name_fragment => fn nodes => case Code_Symbol.Graph.get_node nodes (Code_Symbol.Module name_fragment)
  11.343           of (_, Module (_, nodes)) => nodes) name_fragments hierarchical_program;
  11.344 -        val (base', _) = Graph.get_node nodes name;
  11.345 +        val (base', _) = Code_Symbol.Graph.get_node nodes sym;
  11.346        in Long_Name.implode (remainder @ [base']) end
  11.347 -        handle Graph.UNDEF _ => error ("Unknown statement name: "
  11.348 -          ^ (Code_Symbol.quote_symbol ctxt o symbol_of) name);
  11.349 +        handle Code_Symbol.Graph.UNDEF _ => error ("Unknown statement name: "
  11.350 +          ^ Code_Symbol.quote ctxt sym);
  11.351  
  11.352    in { deresolver = deresolver, hierarchical_program = hierarchical_program } end;
  11.353  
  11.354 @@ -266,10 +264,10 @@
  11.355    let
  11.356      fun print_node _ (_, Dummy) =
  11.357            NONE
  11.358 -      | print_node prefix_fragments (name, Stmt stmt) =
  11.359 -          SOME (lift_markup (Code_Printer.markup_stmt name)
  11.360 -            (print_stmt prefix_fragments (name, stmt)))
  11.361 -      | print_node prefix_fragments (name_fragment, Module (data, nodes)) =
  11.362 +      | print_node prefix_fragments (sym, Stmt stmt) =
  11.363 +          SOME (lift_markup (Code_Printer.markup_stmt sym)
  11.364 +            (print_stmt prefix_fragments (sym, stmt)))
  11.365 +      | print_node prefix_fragments (Code_Symbol.Module name_fragment, Module (data, nodes)) =
  11.366            let
  11.367              val prefix_fragments' = prefix_fragments @ [name_fragment]
  11.368            in
  11.369 @@ -278,9 +276,9 @@
  11.370            end
  11.371      and print_nodes prefix_fragments nodes =
  11.372        let
  11.373 -        val xs = (map_filter (fn name => print_node prefix_fragments
  11.374 -          (name, snd (Graph.get_node nodes name))) o rev o flat o Graph.strong_conn) nodes
  11.375 +        val xs = (map_filter (fn sym => print_node prefix_fragments
  11.376 +          (sym, snd (Code_Symbol.Graph.get_node nodes sym))) o rev o flat o Code_Symbol.Graph.strong_conn) nodes
  11.377        in if null xs then NONE else SOME xs end;
  11.378    in these o print_nodes [] end;
  11.379  
  11.380 -end;
  11.381 \ No newline at end of file
  11.382 +end;
    12.1 --- a/src/Tools/Code/code_printer.ML	Sat Jan 25 23:50:49 2014 +0100
    12.2 +++ b/src/Tools/Code/code_printer.ML	Sat Jan 25 23:50:49 2014 +0100
    12.3 @@ -25,8 +25,8 @@
    12.4    val semicolon: Pretty.T list -> Pretty.T
    12.5    val doublesemicolon: Pretty.T list -> Pretty.T
    12.6    val indent: int -> Pretty.T -> Pretty.T
    12.7 -  val markup_stmt: string -> Pretty.T -> Pretty.T
    12.8 -  val format: string list -> int -> Pretty.T -> string
    12.9 +  val markup_stmt: Code_Symbol.symbol -> Pretty.T -> Pretty.T
   12.10 +  val format: Code_Symbol.symbol list -> int -> Pretty.T -> string
   12.11  
   12.12    val first_upper: string -> string
   12.13    val first_lower: string -> string
   12.14 @@ -36,7 +36,7 @@
   12.15    val lookup_var: var_ctxt -> string -> string
   12.16    val intro_base_names: (string -> bool) -> (string -> string)
   12.17      -> string list -> var_ctxt -> var_ctxt
   12.18 -  val intro_base_names_for: (string -> bool) -> (string -> string)
   12.19 +  val intro_base_names_for: (string -> bool) -> (Code_Symbol.symbol -> string)
   12.20      -> iterm list -> var_ctxt -> var_ctxt
   12.21    val aux_params: var_ctxt -> iterm list list -> string list
   12.22  
   12.23 @@ -81,7 +81,7 @@
   12.24    val simple_const_syntax: simple_const_syntax -> const_syntax
   12.25    val complex_const_syntax: complex_const_syntax -> const_syntax
   12.26    val activate_const_syntax: theory -> literals
   12.27 -    -> string -> const_syntax -> Code_Thingol.naming -> activated_const_syntax * Code_Thingol.naming
   12.28 +    -> string -> const_syntax -> activated_const_syntax
   12.29    val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list)
   12.30      -> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
   12.31      -> (string -> activated_const_syntax option)
   12.32 @@ -125,17 +125,18 @@
   12.33  fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
   12.34  fun indent i = Print_Mode.setmp [] (Pretty.indent i);
   12.35  
   12.36 -fun markup_stmt name = Print_Mode.setmp [code_presentationN]
   12.37 -  (Pretty.mark (code_presentationN, [(stmt_nameN, name)]));
   12.38 +fun markup_stmt sym = Print_Mode.setmp [code_presentationN]
   12.39 +  (Pretty.mark (code_presentationN, [(stmt_nameN, Code_Symbol.marker sym)]));
   12.40  
   12.41  fun filter_presentation [] tree =
   12.42        Buffer.empty
   12.43        |> fold XML.add_content tree
   12.44 -  | filter_presentation presentation_names tree =
   12.45 +  | filter_presentation presentation_syms tree =
   12.46        let
   12.47 +        val presentation_idents = map Code_Symbol.marker presentation_syms
   12.48          fun is_selected (name, attrs) =
   12.49            name = code_presentationN
   12.50 -          andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN));
   12.51 +          andalso member (op =) presentation_idents (the (Properties.get attrs stmt_nameN));
   12.52          fun add_content_with_space tree (is_first, buf) =
   12.53            buf
   12.54            |> not is_first ? Buffer.add "\n\n"
   12.55 @@ -198,8 +199,8 @@
   12.56  
   12.57  fun intro_base_names_for no_syntax deresolve ts =
   12.58    []
   12.59 -  |> fold Code_Thingol.add_constnames ts 
   12.60 -  |> intro_base_names no_syntax deresolve;
   12.61 +  |> fold Code_Thingol.add_constsyms ts 
   12.62 +  |> intro_base_names (fn Code_Symbol.Constant const => no_syntax const | _ => true) deresolve;
   12.63  
   12.64  
   12.65  (** pretty literals **)
   12.66 @@ -304,30 +305,31 @@
   12.67  datatype activated_const_syntax = Plain_const_syntax of int * string
   12.68    | Complex_const_syntax of activated_complex_const_syntax;
   12.69  
   12.70 -fun activate_const_syntax thy literals c (plain_const_syntax s) naming =
   12.71 -      (Plain_const_syntax (Code.args_number thy c, s), naming)
   12.72 -  | activate_const_syntax thy literals c (complex_const_syntax (n, (cs, f))) naming =
   12.73 -      fold_map (Code_Thingol.ensure_declared_const thy) cs naming
   12.74 -      |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
   12.75 +fun activate_const_syntax thy literals c (plain_const_syntax s) =
   12.76 +      Plain_const_syntax (Code.args_number thy c, s)
   12.77 +  | activate_const_syntax thy literals c (complex_const_syntax (n, (cs, f)))=
   12.78 +      Complex_const_syntax (n, f literals cs);
   12.79  
   12.80  fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
   12.81 -    (app as ({ name = c, dom, ... }, ts)) =
   12.82 -  case const_syntax c of
   12.83 -    NONE => brackify fxy (print_app_expr some_thm vars app)
   12.84 -  | SOME (Plain_const_syntax (_, s)) =>
   12.85 -      brackify fxy (str s :: map (print_term some_thm vars BR) ts)
   12.86 -  | SOME (Complex_const_syntax (k, print)) =>
   12.87 -      let
   12.88 -        fun print' fxy ts =
   12.89 -          print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom);
   12.90 -      in
   12.91 -        if k = length ts
   12.92 -        then print' fxy ts
   12.93 -        else if k < length ts
   12.94 -        then case chop k ts of (ts1, ts2) =>
   12.95 -          brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2)
   12.96 -        else print_term some_thm vars fxy (Code_Thingol.eta_expand k app)
   12.97 -      end;
   12.98 +    (app as ({ sym, dom, ... }, ts)) =
   12.99 +  case sym of
  12.100 +    Code_Symbol.Constant const => (case const_syntax const of
  12.101 +      NONE => brackify fxy (print_app_expr some_thm vars app)
  12.102 +    | SOME (Plain_const_syntax (_, s)) =>
  12.103 +        brackify fxy (str s :: map (print_term some_thm vars BR) ts)
  12.104 +    | SOME (Complex_const_syntax (k, print)) =>
  12.105 +        let
  12.106 +          fun print' fxy ts =
  12.107 +            print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom);
  12.108 +        in
  12.109 +          if k = length ts
  12.110 +          then print' fxy ts
  12.111 +          else if k < length ts
  12.112 +          then case chop k ts of (ts1, ts2) =>
  12.113 +            brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2)
  12.114 +          else print_term some_thm vars fxy (Code_Thingol.eta_expand k app)
  12.115 +        end)
  12.116 +  | _ => brackify fxy (print_app_expr some_thm vars app);
  12.117  
  12.118  fun gen_print_bind print_term thm (fxy : fixity) pat vars =
  12.119    let
    13.1 --- a/src/Tools/Code/code_runtime.ML	Sat Jan 25 23:50:49 2014 +0100
    13.2 +++ b/src/Tools/Code/code_runtime.ML	Sat Jan 25 23:50:49 2014 +0100
    13.3 @@ -52,7 +52,7 @@
    13.4  datatype truth = Holds;
    13.5  
    13.6  val _ = Theory.setup
    13.7 -  (Code_Target.extend_target (target, (Code_ML.target_SML, K I))
    13.8 +  (Code_Target.extend_target (target, (Code_ML.target_SML, I))
    13.9    #> Code_Target.set_printings (Code_Symbol.Type_Constructor (@{type_name prop},
   13.10      [(target, SOME (0, (K o K o K) (Code_Printer.str s_truth)))]))
   13.11    #> Code_Target.set_printings (Code_Symbol.Constant (@{const_name Code_Generator.holds},
   13.12 @@ -87,10 +87,13 @@
   13.13      val ctxt = Proof_Context.init_global thy;
   13.14    in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end;
   13.15  
   13.16 -fun obtain_evaluator thy some_target naming program consts expr =
   13.17 -  Code_Target.evaluator thy (the_default target some_target) naming program consts expr
   13.18 +fun obtain_evaluator thy some_target program consts expr =
   13.19 +  Code_Target.evaluator thy (the_default target some_target) program consts expr
   13.20    |> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules));
   13.21  
   13.22 +fun obtain_evaluator' thy some_target program =
   13.23 +  obtain_evaluator thy some_target program o map Code_Symbol.Constant;
   13.24 +
   13.25  fun evaluation cookie thy evaluator vs_t args =
   13.26    let
   13.27      val ctxt = Proof_Context.init_global thy;
   13.28 @@ -110,8 +113,8 @@
   13.29      val _ = if ! trace
   13.30        then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term_global thy t))
   13.31        else ()
   13.32 -    fun evaluator naming program ((_, vs_ty), t) deps =
   13.33 -      evaluation cookie thy (obtain_evaluator thy some_target naming program deps) (vs_ty, t) args;
   13.34 +    fun evaluator program ((_, vs_ty), t) deps =
   13.35 +      evaluation cookie thy (obtain_evaluator thy some_target program deps) (vs_ty, t) args;
   13.36    in Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t end;
   13.37  
   13.38  fun dynamic_value_strict cookie thy some_target postproc t args =
   13.39 @@ -120,9 +123,9 @@
   13.40  fun dynamic_value cookie thy some_target postproc t args =
   13.41    partiality_as_none (dynamic_value_exn cookie thy some_target postproc t args);
   13.42  
   13.43 -fun static_evaluator cookie thy some_target naming program consts' =
   13.44 +fun static_evaluator cookie thy some_target program consts' =
   13.45    let
   13.46 -    val evaluator = obtain_evaluator thy some_target naming program consts'
   13.47 +    val evaluator = obtain_evaluator' thy some_target program consts'
   13.48    in fn ((_, vs_ty), t) => fn _ => evaluation cookie thy evaluator (vs_ty, t) [] end;
   13.49  
   13.50  fun static_value_exn cookie thy some_target postproc consts =
   13.51 @@ -175,13 +178,13 @@
   13.52  in
   13.53  
   13.54  fun dynamic_holds_conv thy = Code_Thingol.dynamic_conv thy
   13.55 -  (fn naming => fn program => fn vs_t => fn deps =>
   13.56 -    check_holds_oracle thy (obtain_evaluator thy NONE naming program deps) vs_t deps)
   13.57 +  (fn program => fn vs_t => fn deps =>
   13.58 +    check_holds_oracle thy (obtain_evaluator thy NONE program deps) vs_t deps)
   13.59        o reject_vars thy;
   13.60  
   13.61  fun static_holds_conv thy consts = Code_Thingol.static_conv thy consts
   13.62 -  (fn naming => fn program => fn consts' =>
   13.63 -    check_holds_oracle thy (obtain_evaluator thy NONE naming program consts'))
   13.64 +  (fn program => fn consts' =>
   13.65 +    check_holds_oracle thy (obtain_evaluator' thy NONE program consts'))
   13.66        o reject_vars thy;
   13.67  
   13.68  end; (*local*)
   13.69 @@ -192,23 +195,22 @@
   13.70  fun evaluation_code thy module_name tycos consts =
   13.71    let
   13.72      val ctxt = Proof_Context.init_global thy;
   13.73 -    val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
   13.74 -    val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
   13.75 +    val program = Code_Thingol.consts_program thy false consts;
   13.76      val (ml_modules, target_names) =
   13.77        Code_Target.produce_code_for thy
   13.78 -        target NONE module_name [] naming program (consts' @ tycos');
   13.79 +        target NONE module_name [] program (map Code_Symbol.Constant consts @ map Code_Symbol.Type_Constructor tycos);
   13.80      val ml_code = space_implode "\n\n" (map snd ml_modules);
   13.81 -    val (consts'', tycos'') = chop (length consts') target_names;
   13.82 +    val (consts', tycos') = chop (length consts) target_names;
   13.83      val consts_map = map2 (fn const =>
   13.84        fn NONE =>
   13.85            error ("Constant " ^ (quote o Code.string_of_const thy) const ^
   13.86              "\nhas a user-defined serialization")
   13.87 -       | SOME const'' => (const, const'')) consts consts''
   13.88 +       | SOME const' => (const, const')) consts consts'
   13.89      val tycos_map = map2 (fn tyco =>
   13.90        fn NONE =>
   13.91            error ("Type " ^ quote (Proof_Context.extern_type ctxt tyco) ^
   13.92              "\nhas a user-defined serialization")
   13.93 -        | SOME tyco'' => (tyco, tyco'')) tycos tycos'';
   13.94 +        | SOME tyco' => (tyco, tyco')) tycos tycos';
   13.95    in (ml_code, (tycos_map, consts_map)) end;
   13.96  
   13.97  
    14.1 --- a/src/Tools/Code/code_scala.ML	Sat Jan 25 23:50:49 2014 +0100
    14.2 +++ b/src/Tools/Code/code_scala.ML	Sat Jan 25 23:50:49 2014 +0100
    14.3 @@ -27,15 +27,18 @@
    14.4  fun print_scala_stmt tyco_syntax const_syntax reserved
    14.5      args_num is_constr (deresolve, deresolve_full) =
    14.6    let
    14.7 +    val deresolve_const = deresolve o Code_Symbol.Constant;
    14.8 +    val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
    14.9 +    val deresolve_class = deresolve o Code_Symbol.Type_Class;
   14.10      fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
   14.11      fun intro_tyvars vs = intro_vars (map (first_upper o fst) vs);
   14.12 -    fun print_tyco_expr tyvars fxy (tyco, tys) = applify "[" "]"
   14.13 -          (print_typ tyvars NOBR) fxy ((str o deresolve) tyco) tys
   14.14 +    fun print_tyco_expr tyvars fxy (sym, tys) = applify "[" "]"
   14.15 +          (print_typ tyvars NOBR) fxy ((str o deresolve) sym) tys
   14.16      and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
   14.17 -         of NONE => print_tyco_expr tyvars fxy (tyco, tys)
   14.18 +         of NONE => print_tyco_expr tyvars fxy (Code_Symbol.Type_Constructor tyco, tys)
   14.19            | SOME (_, print) => print (print_typ tyvars) fxy tys)
   14.20        | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
   14.21 -    fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (class, [ty]);
   14.22 +    fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (Code_Symbol.Type_Class class, [ty]);
   14.23      fun print_tupled_typ tyvars ([], ty) =
   14.24            print_typ tyvars NOBR ty
   14.25        | print_tupled_typ tyvars ([ty1], ty2) =
   14.26 @@ -67,20 +70,24 @@
   14.27            end
   14.28        | print_term tyvars is_pat some_thm vars fxy (ICase case_expr) =
   14.29            (case Code_Thingol.unfold_const_app (#primitive case_expr)
   14.30 -           of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
   14.31 +           of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
   14.32 +                if is_none (const_syntax const)
   14.33                  then print_case tyvars some_thm vars fxy case_expr
   14.34                  else print_app tyvars is_pat some_thm vars fxy app
   14.35              | NONE => print_case tyvars some_thm vars fxy case_expr)
   14.36      and print_app tyvars is_pat some_thm vars fxy
   14.37 -        (app as ({ name = c, typargs, dom, ... }, ts)) =
   14.38 +        (app as ({ sym, typargs, dom, ... }, ts)) =
   14.39        let
   14.40          val k = length ts;
   14.41          val typargs' = if is_pat then [] else typargs;
   14.42 -        val (l, print') = case const_syntax c
   14.43 -         of NONE => (args_num c, fn fxy => fn ts => gen_applify (is_constr c ) "(" ")"
   14.44 +        val syntax = case sym of
   14.45 +            Code_Symbol.Constant const => const_syntax const
   14.46 +          | _ => NONE;
   14.47 +        val (l, print') = case syntax of
   14.48 +            NONE => (args_num sym, fn fxy => fn ts => gen_applify (is_constr sym) "(" ")"
   14.49                (print_term tyvars is_pat some_thm vars NOBR) fxy
   14.50                  (applify "[" "]" (print_typ tyvars NOBR)
   14.51 -                  NOBR ((str o deresolve) c) typargs') ts)
   14.52 +                  NOBR ((str o deresolve) sym) typargs') ts)
   14.53            | SOME (Plain_const_syntax (k, s)) => (k, fn fxy => fn ts => applify "(" ")"
   14.54                (print_term tyvars is_pat some_thm vars NOBR) fxy
   14.55                  (applify "[" "]" (print_typ tyvars NOBR)
   14.56 @@ -137,32 +144,32 @@
   14.57              |> single
   14.58              |> enclose "(" ")"
   14.59            end;
   14.60 -    fun print_context tyvars vs name = applify "[" "]"
   14.61 +    fun print_context tyvars vs sym = applify "[" "]"
   14.62        (fn (v, sort) => (Pretty.block o map str)
   14.63 -        (lookup_tyvar tyvars v :: maps (fn sort => [" : ", deresolve sort]) sort))
   14.64 -          NOBR ((str o deresolve) name) vs;
   14.65 -    fun print_defhead tyvars vars name vs params tys ty =
   14.66 +        (lookup_tyvar tyvars v :: maps (fn class => [" : ", deresolve_class class]) sort))
   14.67 +          NOBR ((str o deresolve) sym) vs;
   14.68 +    fun print_defhead tyvars vars const vs params tys ty =
   14.69        Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) =>
   14.70          constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
   14.71 -          NOBR (print_context tyvars vs name) (params ~~ tys)) (print_typ tyvars NOBR ty),
   14.72 +          NOBR (print_context tyvars vs (Code_Symbol.Constant const)) (params ~~ tys)) (print_typ tyvars NOBR ty),
   14.73              str " ="];
   14.74 -    fun print_def name (vs, ty) [] =
   14.75 +    fun print_def const (vs, ty) [] =
   14.76            let
   14.77              val (tys, ty') = Code_Thingol.unfold_fun ty;
   14.78              val params = Name.invent (snd reserved) "a" (length tys);
   14.79              val tyvars = intro_tyvars vs reserved;
   14.80              val vars = intro_vars params reserved;
   14.81            in
   14.82 -            concat [print_defhead tyvars vars name vs params tys ty',
   14.83 -              str ("sys.error(\"" ^ name ^ "\")")]
   14.84 +            concat [print_defhead tyvars vars const vs params tys ty',
   14.85 +              str ("sys.error(\"" ^ const ^ "\")")]
   14.86            end
   14.87 -      | print_def name (vs, ty) eqs =
   14.88 +      | print_def const (vs, ty) eqs =
   14.89            let
   14.90              val tycos = fold (fn ((ts, t), _) =>
   14.91                fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
   14.92              val tyvars = reserved
   14.93                |> intro_base_names
   14.94 -                   (is_none o tyco_syntax) deresolve tycos
   14.95 +                   (is_none o tyco_syntax) deresolve_tyco tycos
   14.96                |> intro_tyvars vs;
   14.97              val simple = case eqs
   14.98               of [((ts, _), _)] => forall Code_Thingol.is_IVar ts
   14.99 @@ -188,7 +195,7 @@
  14.100                    tuplify (map (print_term tyvars true some_thm vars' NOBR) ts),
  14.101                    str "=>", print_rhs vars' eq]
  14.102                end;
  14.103 -            val head = print_defhead tyvars vars2 name vs params tys' ty';
  14.104 +            val head = print_defhead tyvars vars2 const vs params tys' ty';
  14.105            in if simple then
  14.106              concat [head, print_rhs vars2 (hd eqs)]
  14.107            else
  14.108 @@ -197,34 +204,34 @@
  14.109                  str "match", str "{"], str "}")
  14.110                (map print_clause eqs)
  14.111            end;
  14.112 -    val print_method = str o Library.enclose "`" "`" o deresolve_full;
  14.113 -    fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
  14.114 -          print_def name (vs, ty) (filter (snd o snd) raw_eqs)
  14.115 -      | print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
  14.116 +    val print_method = str o Library.enclose "`" "`" o deresolve_full o Code_Symbol.Constant;
  14.117 +    fun print_stmt (Code_Symbol.Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
  14.118 +          print_def const (vs, ty) (filter (snd o snd) raw_eqs)
  14.119 +      | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, cos)) =
  14.120            let
  14.121              val tyvars = intro_tyvars (map (rpair []) vs) reserved;
  14.122              fun print_co ((co, vs_args), tys) =
  14.123                concat [Pretty.block ((applify "[" "]" (str o lookup_tyvar tyvars) NOBR
  14.124 -                ((concat o map str) ["final", "case", "class", deresolve co]) vs_args)
  14.125 +                ((concat o map str) ["final", "case", "class", deresolve_const co]) vs_args)
  14.126                  @@ enum "," "(" ")" (map (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg))
  14.127                    (Name.invent_names (snd reserved) "a" tys))),
  14.128                  str "extends",
  14.129                  applify "[" "]" (str o lookup_tyvar tyvars) NOBR
  14.130 -                  ((str o deresolve) name) vs
  14.131 +                  ((str o deresolve_tyco) tyco) vs
  14.132                ];
  14.133            in
  14.134              Pretty.chunks (applify "[" "]" (str o lookup_tyvar tyvars)
  14.135 -              NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve name]) vs
  14.136 +              NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs
  14.137                  :: map print_co cos)
  14.138            end
  14.139 -      | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
  14.140 +      | print_stmt (Code_Symbol.Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
  14.141            let
  14.142 -            val tyvars = intro_tyvars [(v, [name])] reserved;
  14.143 +            val tyvars = intro_tyvars [(v, [class])] reserved;
  14.144              fun add_typarg s = Pretty.block
  14.145                [str s, str "[", (str o lookup_tyvar tyvars) v, str "]"];
  14.146              fun print_super_classes [] = NONE
  14.147 -              | print_super_classes classes = SOME (concat (str "extends"
  14.148 -                  :: separate (str "with") (map (add_typarg o deresolve o fst) classes)));
  14.149 +              | print_super_classes classrels = SOME (concat (str "extends"
  14.150 +                  :: separate (str "with") (map (add_typarg o deresolve_class o snd) classrels)));
  14.151              fun print_classparam_val (classparam, ty) =
  14.152                concat [str "val", constraint (print_method classparam)
  14.153                  ((print_tupled_typ tyvars o Code_Thingol.unfold_fun) ty)];
  14.154 @@ -238,22 +245,22 @@
  14.155                in
  14.156                  concat [str "def", constraint (Pretty.block [applify "(" ")"
  14.157                    (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
  14.158 -                  (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve classparam))
  14.159 +                  (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_const classparam))
  14.160                    (auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
  14.161 -                  add_typarg (deresolve name), str ")"]) (print_typ tyvars NOBR ty), str "=",
  14.162 +                  add_typarg (deresolve_class class), str ")"]) (print_typ tyvars NOBR ty), str "=",
  14.163                    applify "(" ")" (str o lookup_var vars) NOBR
  14.164                    (Pretty.block [str implicit_name, str ".", print_method classparam]) auxs]
  14.165                end;
  14.166            in
  14.167              Pretty.chunks (
  14.168                (Pretty.block_enclose
  14.169 -                (concat ([str "trait", (add_typarg o deresolve) name]
  14.170 -                  @ the_list (print_super_classes super_classes) @ [str "{"]), str "}")
  14.171 +                (concat ([str "trait", (add_typarg o deresolve_class) class]
  14.172 +                  @ the_list (print_super_classes classrels) @ [str "{"]), str "}")
  14.173                  (map print_classparam_val classparams))
  14.174                :: map print_classparam_def classparams
  14.175              )
  14.176            end
  14.177 -      | print_stmt (name, Code_Thingol.Classinst
  14.178 +      | print_stmt (sym, Code_Thingol.Classinst
  14.179            { class, tyco, vs, inst_params, superinst_params, ... }) =
  14.180            let
  14.181              val tyvars = intro_tyvars vs reserved;
  14.182 @@ -277,13 +284,13 @@
  14.183                end;
  14.184            in
  14.185              Pretty.block_enclose (concat [str "implicit def",
  14.186 -              constraint (print_context tyvars vs name) (print_dicttyp tyvars classtyp),
  14.187 +              constraint (print_context tyvars vs sym) (print_dicttyp tyvars classtyp),
  14.188                str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
  14.189                  (map print_classparam_instance (inst_params @ superinst_params))
  14.190            end;
  14.191    in print_stmt end;
  14.192  
  14.193 -fun scala_program_of_program ctxt symbol_of module_name reserved identifiers program =
  14.194 +fun scala_program_of_program ctxt module_name reserved identifiers program =
  14.195    let
  14.196      fun namify_module name_fragment ((nsp_class, nsp_object), nsp_common) =
  14.197        let
  14.198 @@ -312,49 +319,49 @@
  14.199        | namify_stmt (Code_Thingol.Classrel _) = namify_object
  14.200        | namify_stmt (Code_Thingol.Classparam _) = namify_object
  14.201        | namify_stmt (Code_Thingol.Classinst _) = namify_common false;
  14.202 -    fun memorize_implicits name =
  14.203 +    fun memorize_implicits sym =
  14.204        let
  14.205          fun is_classinst stmt = case stmt
  14.206           of Code_Thingol.Classinst _ => true
  14.207            | _ => false;
  14.208 -        val implicits = filter (is_classinst o Graph.get_node program)
  14.209 -          (Graph.immediate_succs program name);
  14.210 +        val implicits = filter (is_classinst o Code_Symbol.Graph.get_node program)
  14.211 +          (Code_Symbol.Graph.immediate_succs program sym);
  14.212        in union (op =) implicits end;
  14.213 -    fun modify_stmt (_, Code_Thingol.Fun (_, (_, SOME _))) = NONE
  14.214 +    fun modify_stmt (_, Code_Thingol.Fun (_, SOME _)) = NONE
  14.215        | modify_stmt (_, Code_Thingol.Datatypecons _) = NONE
  14.216        | modify_stmt (_, Code_Thingol.Classrel _) = NONE
  14.217        | modify_stmt (_, Code_Thingol.Classparam _) = NONE
  14.218        | modify_stmt (_, stmt) = SOME stmt;
  14.219    in
  14.220 -    Code_Namespace.hierarchical_program ctxt symbol_of
  14.221 +    Code_Namespace.hierarchical_program ctxt
  14.222        { module_name = module_name, reserved = reserved, identifiers = identifiers,
  14.223          empty_nsp = ((reserved, reserved), reserved), namify_module = namify_module,
  14.224          namify_stmt = namify_stmt, cyclic_modules = true, empty_data = [],
  14.225          memorize_data = memorize_implicits, modify_stmts = map modify_stmt } program
  14.226    end;
  14.227  
  14.228 -fun serialize_scala ctxt { symbol_of, module_name, reserved_syms, identifiers,
  14.229 +fun serialize_scala ctxt { module_name, reserved_syms, identifiers,
  14.230      includes, class_syntax, tyco_syntax, const_syntax } program =
  14.231    let
  14.232  
  14.233      (* build program *)
  14.234      val { deresolver, hierarchical_program = scala_program } =
  14.235 -      scala_program_of_program ctxt symbol_of module_name (Name.make_context reserved_syms) identifiers program;
  14.236 +      scala_program_of_program ctxt module_name (Name.make_context reserved_syms) identifiers program;
  14.237  
  14.238      (* print statements *)
  14.239 -    fun lookup_constr tyco constr = case Graph.get_node program tyco
  14.240 -     of Code_Thingol.Datatype (_, (_, constrs)) =>
  14.241 +    fun lookup_constr tyco constr = case Code_Symbol.Graph.get_node program (Code_Symbol.Type_Constructor tyco)
  14.242 +     of Code_Thingol.Datatype (_, constrs) =>
  14.243            the (AList.lookup (op = o apsnd fst) constrs constr);
  14.244 -    fun classparams_of_class class = case Graph.get_node program class
  14.245 -     of Code_Thingol.Class (_, (_, (_, classparams))) => classparams;
  14.246 -    fun args_num c = case Graph.get_node program c
  14.247 -     of Code_Thingol.Fun (_, (((_, ty), []), _)) =>
  14.248 +    fun classparams_of_class class = case Code_Symbol.Graph.get_node program (Code_Symbol.Type_Class class)
  14.249 +     of Code_Thingol.Class (_, (_, classparams)) => classparams;
  14.250 +    fun args_num (sym as Code_Symbol.Constant const) = case Code_Symbol.Graph.get_node program sym
  14.251 +     of Code_Thingol.Fun (((_, ty), []), _) =>
  14.252            (length o fst o Code_Thingol.unfold_fun) ty
  14.253 -      | Code_Thingol.Fun (_, ((_, ((ts, _), _) :: _), _)) => length ts
  14.254 -      | Code_Thingol.Datatypecons (_, tyco) => length (lookup_constr tyco c)
  14.255 -      | Code_Thingol.Classparam (_, class) =>
  14.256 +      | Code_Thingol.Fun ((_, ((ts, _), _) :: _), _) => length ts
  14.257 +      | Code_Thingol.Datatypecons tyco => length (lookup_constr tyco const)
  14.258 +      | Code_Thingol.Classparam class =>
  14.259            (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =)
  14.260 -            (classparams_of_class class)) c;
  14.261 +            (classparams_of_class class)) const;
  14.262      fun print_stmt prefix_fragments = print_scala_stmt
  14.263        tyco_syntax const_syntax (make_vars reserved_syms) args_num
  14.264        (Code_Thingol.is_constr program) (deresolver prefix_fragments, deresolver []);
  14.265 @@ -378,7 +385,7 @@
  14.266          lift_markup = I } scala_program);
  14.267      fun write width NONE = writeln o format [] width
  14.268        | write width (SOME p) = File.write p o format [] width;
  14.269 -    fun prepare names width p = ([("", format names width p)], try (deresolver []));
  14.270 +    fun prepare syms width p = ([("", format syms width p)], try (deresolver []));
  14.271    in
  14.272      Code_Target.serialization write prepare p
  14.273    end;
    15.1 --- a/src/Tools/Code/code_simp.ML	Sat Jan 25 23:50:49 2014 +0100
    15.2 +++ b/src/Tools/Code/code_simp.ML	Sat Jan 25 23:50:49 2014 +0100
    15.3 @@ -52,7 +52,7 @@
    15.4  
    15.5  (* build simpset and conversion from program *)
    15.6  
    15.7 -fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss =
    15.8 +fun add_stmt (Code_Thingol.Fun ((_, eqs), some_cong)) ss =
    15.9        ss
   15.10        |> fold Simplifier.add_simp ((map_filter (fst o snd)) eqs)
   15.11        |> fold Simplifier.add_cong (the_list some_cong)
   15.12 @@ -61,7 +61,7 @@
   15.13        |> fold Simplifier.add_simp (map (fst o snd) inst_params)
   15.14    | add_stmt _ ss = ss;
   15.15  
   15.16 -val add_program = Graph.fold (add_stmt o fst o snd);
   15.17 +val add_program = Code_Symbol.Graph.fold (add_stmt o fst o snd);
   15.18  
   15.19  fun simp_ctxt_program thy some_ss program =
   15.20    simp_ctxt_default thy some_ss
   15.21 @@ -77,7 +77,7 @@
   15.22  (* evaluation with dynamic code context *)
   15.23  
   15.24  fun dynamic_conv thy = Code_Thingol.dynamic_conv thy
   15.25 -  (fn _ => fn program => fn _ => fn _ => rewrite_modulo thy NONE program);
   15.26 +  (fn program => fn _ => fn _ => rewrite_modulo thy NONE program);
   15.27  
   15.28  fun dynamic_tac thy = CONVERSION (dynamic_conv thy) THEN' conclude_tac thy NONE (Proof_Context.init_global thy);
   15.29  
    16.1 --- a/src/Tools/Code/code_symbol.ML	Sat Jan 25 23:50:49 2014 +0100
    16.2 +++ b/src/Tools/Code/code_symbol.ML	Sat Jan 25 23:50:49 2014 +0100
    16.3 @@ -13,9 +13,12 @@
    16.4    type symbol = (string, string, class, class * class, string * class, string) attr
    16.5    structure Table: TABLE;
    16.6    structure Graph: GRAPH;
    16.7 -  val default_name: Proof.context -> symbol -> string * string
    16.8 -  val quote_symbol: Proof.context -> symbol -> string
    16.9 -  val tyco_fun: string
   16.10 +  val namespace_prefix: Proof.context -> symbol -> string
   16.11 +  val base_name: symbol -> string
   16.12 +  val quote: Proof.context -> symbol -> string
   16.13 +  val marker: symbol -> string
   16.14 +  val value: symbol
   16.15 +  val is_value: symbol -> bool
   16.16    val map_attr: ('a -> 'g) -> ('b -> 'h) -> ('c -> 'i) -> ('d -> 'j) -> ('e -> 'k) -> ('f -> 'l)
   16.17      -> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('g, 'h, 'i, 'j, 'k, 'l) attr
   16.18    val maps_attr: ('a -> 'g list) -> ('b -> 'h list)
   16.19 @@ -38,6 +41,8 @@
   16.20    val lookup_class_instance_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string * class -> 'e option
   16.21    val lookup_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'f option
   16.22    val lookup: ('a, 'a, 'a, 'a, 'a, 'a) data -> symbol -> 'a option
   16.23 +  val symbols_of: ('a, 'b, 'c, 'd, 'e, 'f) data -> symbol list
   16.24 +  val mapped_const_data: (string -> 'a -> 'g) -> ('a, 'b, 'c, 'd, 'e, 'f) data -> 'g Symtab.table
   16.25    val dest_constant_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'a) list
   16.26    val dest_type_constructor_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'b) list
   16.27    val dest_type_class_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (class * 'c) list
   16.28 @@ -89,40 +94,48 @@
   16.29      | NONE => (case Code.get_type_of_constr_or_abstr thy c
   16.30         of SOME (tyco, _) => thyname_of_type thy tyco
   16.31          | NONE => #theory_name (Name_Space.the_entry (Sign.const_space thy) c));
   16.32 -  fun base_rel (x, y) = Long_Name.base_name y ^ "_" ^ Long_Name.base_name x;
   16.33 -  fun plainify ctxt get_prefix get_basename thing =
   16.34 -    (get_prefix (Proof_Context.theory_of ctxt) thing,
   16.35 -      Name.desymbolize false (get_basename thing));
   16.36 +  fun prefix thy (Constant "") = "Code"
   16.37 +    | prefix thy (Constant c) = thyname_of_const thy c
   16.38 +    | prefix thy (Type_Constructor tyco) = thyname_of_type thy tyco
   16.39 +    | prefix thy (Type_Class class) = thyname_of_class thy class
   16.40 +    | prefix thy (Class_Relation (class, _)) = thyname_of_class thy class
   16.41 +    | prefix thy (Class_Instance inst) = thyname_of_instance thy inst;
   16.42 +  val base = Name.desymbolize false o Long_Name.base_name;
   16.43 +  fun base_rel (x, y) = base y ^ "_" ^ base x;
   16.44  in
   16.45  
   16.46 -fun default_name ctxt (Constant "==>") =
   16.47 -      plainify ctxt thyname_of_const (K "follows") "==>"
   16.48 -  | default_name ctxt (Constant "==") =
   16.49 -      plainify ctxt thyname_of_const (K "meta_eq") "=="
   16.50 -  | default_name ctxt (Constant c) =
   16.51 -      plainify ctxt thyname_of_const Long_Name.base_name c
   16.52 -  | default_name ctxt (Type_Constructor "fun") =
   16.53 -      plainify ctxt thyname_of_type (K "fun") "fun"
   16.54 -  | default_name ctxt (Type_Constructor tyco) =
   16.55 -      plainify ctxt thyname_of_type Long_Name.base_name tyco
   16.56 -  | default_name ctxt (Type_Class class) =
   16.57 -      plainify ctxt thyname_of_class Long_Name.base_name class
   16.58 -  | default_name ctxt (Class_Relation classrel) =
   16.59 -      plainify ctxt (fn thy => fn (class, _) => thyname_of_class thy class) base_rel classrel
   16.60 -  | default_name ctxt (Class_Instance inst) =
   16.61 -      plainify ctxt thyname_of_instance base_rel inst;
   16.62 +fun base_name (Constant "") = "value"
   16.63 +  | base_name (Constant "==>") = "follows"
   16.64 +  | base_name (Constant "==") = "meta_eq"
   16.65 +  | base_name (Constant c) = base c
   16.66 +  | base_name (Type_Constructor tyco) = base tyco
   16.67 +  | base_name (Type_Class class) = base class
   16.68 +  | base_name (Class_Relation classrel) = base_rel classrel
   16.69 +  | base_name (Class_Instance inst) = base_rel inst;
   16.70  
   16.71 -val tyco_fun = (uncurry Long_Name.append o default_name @{context}) (Type_Constructor "fun");
   16.72 +fun namespace_prefix ctxt = prefix (Proof_Context.theory_of ctxt);
   16.73 +
   16.74 +fun default_name ctxt sym = (namespace_prefix ctxt sym, base_name sym);
   16.75 +
   16.76 +val value = Constant "";
   16.77 +fun is_value (Constant "") = true
   16.78 +  | is_value _ = false;
   16.79  
   16.80  end;
   16.81  
   16.82 -fun quote_symbol ctxt (Constant c) = quote (Code.string_of_const (Proof_Context.theory_of ctxt) c)
   16.83 -  | quote_symbol ctxt (Type_Constructor tyco) = "type " ^ quote (Proof_Context.extern_type ctxt tyco)
   16.84 -  | quote_symbol ctxt (Type_Class class) = "class " ^ quote (Proof_Context.extern_class ctxt class)
   16.85 -  | quote_symbol ctxt (Class_Relation (sub, super)) =
   16.86 -      quote (Proof_Context.extern_class ctxt sub) ^ " < " ^ quote (Proof_Context.extern_class ctxt super)
   16.87 -  | quote_symbol ctxt (Class_Instance (tyco, class)) =
   16.88 -      quote (Proof_Context.extern_type ctxt tyco) ^ " :: " ^ quote (Proof_Context.extern_class ctxt class);
   16.89 +fun quote ctxt (Constant c) = Library.quote (Code.string_of_const (Proof_Context.theory_of ctxt) c)
   16.90 +  | quote ctxt (Type_Constructor tyco) = "type " ^ Library.quote (Proof_Context.extern_type ctxt tyco)
   16.91 +  | quote ctxt (Type_Class class) = "class " ^ Library.quote (Proof_Context.extern_class ctxt class)
   16.92 +  | quote ctxt (Class_Relation (sub, super)) =
   16.93 +      Library.quote (Proof_Context.extern_class ctxt sub) ^ " < " ^ Library.quote (Proof_Context.extern_class ctxt super)
   16.94 +  | quote ctxt (Class_Instance (tyco, class)) =
   16.95 +      Library.quote (Proof_Context.extern_type ctxt tyco) ^ " :: " ^ Library.quote (Proof_Context.extern_class ctxt class);
   16.96 +
   16.97 +fun marker (Constant c) = "CONST " ^ c
   16.98 +  | marker (Type_Constructor tyco) = "TYPE " ^ tyco
   16.99 +  | marker (Type_Class class) = "CLASS " ^ class
  16.100 +  | marker (Class_Relation (sub, super)) = "CLASSREL " ^ sub ^ " < " ^ super
  16.101 +  | marker (Class_Instance (tyco, class)) = "INSTANCE " ^ tyco ^ " :: " ^ class;
  16.102  
  16.103  fun map_attr const tyco class classrel inst module (Constant x) = Constant (const x)
  16.104    | map_attr const tyco class classrel inst module (Type_Constructor x) = Type_Constructor (tyco x)
  16.105 @@ -199,6 +212,15 @@
  16.106    | lookup data (Class_Instance x) = lookup_class_instance_data data x
  16.107    | lookup data (Module x) = lookup_module_data data x;
  16.108  
  16.109 +fun symbols_of x = (map Constant o Symtab.keys o #constant o dest_data) x
  16.110 +  @ (map Type_Constructor o Symtab.keys o #type_constructor o dest_data) x
  16.111 +  @ (map Type_Class o Symtab.keys o #type_class o dest_data) x
  16.112 +  @ (map Class_Relation o Symreltab.keys o #class_relation o dest_data) x
  16.113 +  @ (map Class_Instance o Symreltab.keys o #class_instance o dest_data) x
  16.114 +  @ (map Module o Symtab.keys o #module o dest_data) x;
  16.115 +
  16.116 +fun mapped_const_data f x = Symtab.map f ((#constant o dest_data) x);
  16.117 +
  16.118  fun dest_constant_data x = (Symtab.dest o #constant o dest_data) x;
  16.119  fun dest_type_constructor_data x = (Symtab.dest o #type_constructor o dest_data) x;
  16.120  fun dest_type_class_data x = (Symtab.dest o #type_class o dest_data) x;
    17.1 --- a/src/Tools/Code/code_target.ML	Sat Jan 25 23:50:49 2014 +0100
    17.2 +++ b/src/Tools/Code/code_target.ML	Sat Jan 25 23:50:49 2014 +0100
    17.3 @@ -11,26 +11,26 @@
    17.4    val read_const_exprs: theory -> string list -> string list
    17.5  
    17.6    val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
    17.7 -    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
    17.8 +    -> Code_Thingol.program -> Code_Symbol.symbol list -> unit
    17.9    val produce_code_for: theory -> string -> int option -> string -> Token.T list
   17.10 -    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> (string * string) list * string option list
   17.11 +    -> Code_Thingol.program -> Code_Symbol.symbol list -> (string * string) list * string option list
   17.12    val present_code_for: theory -> string -> int option -> string -> Token.T list
   17.13 -    -> Code_Thingol.naming -> Code_Thingol.program -> string list * string list -> string
   17.14 +    -> Code_Thingol.program -> Code_Symbol.symbol list * Code_Symbol.symbol list -> string
   17.15    val check_code_for: theory -> string -> bool -> Token.T list
   17.16 -    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
   17.17 +    -> Code_Thingol.program -> Code_Symbol.symbol list -> unit
   17.18  
   17.19    val export_code: theory -> string list
   17.20      -> (((string * string) * Path.T option) * Token.T list) list -> unit
   17.21    val produce_code: theory -> string list
   17.22      -> string -> int option -> string -> Token.T list -> (string * string) list * string option list
   17.23 -  val present_code: theory -> string list -> (Code_Thingol.naming -> string list)
   17.24 +  val present_code: theory -> string list -> Code_Symbol.symbol list
   17.25      -> string -> int option -> string -> Token.T list -> string
   17.26    val check_code: theory -> string list
   17.27      -> ((string * bool) * Token.T list) list -> unit
   17.28  
   17.29    val generatedN: string
   17.30 -  val evaluator: theory -> string -> Code_Thingol.naming -> Code_Thingol.program
   17.31 -    -> string list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
   17.32 +  val evaluator: theory -> string -> Code_Thingol.program
   17.33 +    -> Code_Symbol.symbol list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
   17.34      -> (string * string) list * string
   17.35  
   17.36    type serializer
   17.37 @@ -39,14 +39,14 @@
   17.38      check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } }
   17.39      -> theory -> theory
   17.40    val extend_target: string *
   17.41 -      (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
   17.42 +      (string * (Code_Thingol.program -> Code_Thingol.program))
   17.43      -> theory -> theory
   17.44    val assert_target: theory -> string -> string
   17.45    val the_literals: theory -> string -> literals
   17.46    type serialization
   17.47    val parse_args: 'a parser -> Token.T list -> 'a
   17.48    val serialization: (int -> Path.T option -> 'a -> unit)
   17.49 -    -> (string list -> int -> 'a -> (string * string) list * (string -> string option))
   17.50 +    -> (Code_Symbol.symbol list -> int -> 'a -> (string * string) list * (Code_Symbol.symbol -> string option))
   17.51      -> 'a -> serialization
   17.52    val set_default_code_width: int -> theory -> theory
   17.53  
   17.54 @@ -117,7 +117,7 @@
   17.55    (cert_class thy class, cert_tyco thy tyco);
   17.56  
   17.57  fun read_inst thy (raw_tyco, raw_class) =
   17.58 -  (read_class thy raw_class, read_tyco thy raw_tyco);
   17.59 +  (read_tyco thy raw_tyco, read_class thy raw_class);
   17.60  
   17.61  val parse_inst_ident = Parse.xname --| @{keyword "::"} -- Parse.class;
   17.62  
   17.63 @@ -154,21 +154,21 @@
   17.64  
   17.65  (* serialization: abstract nonsense to cover different destinies for generated code *)
   17.66  
   17.67 -datatype destination = Export of Path.T option | Produce | Present of string list;
   17.68 -type serialization = int -> destination -> ((string * string) list * (string -> string option)) option;
   17.69 +datatype destination = Export of Path.T option | Produce | Present of Code_Symbol.symbol list;
   17.70 +type serialization = int -> destination -> ((string * string) list * (Code_Symbol.symbol -> string option)) option;
   17.71  
   17.72  fun serialization output _ content width (Export some_path) =
   17.73        (output width some_path content; NONE)
   17.74    | serialization _ string content width Produce =
   17.75        string [] width content |> SOME
   17.76 -  | serialization _ string content width (Present stmt_names) =
   17.77 -     string stmt_names width content
   17.78 +  | serialization _ string content width (Present syms) =
   17.79 +     string syms width content
   17.80       |> (apfst o map o apsnd) (Pretty.output (SOME width) o Pretty.str)
   17.81       |> SOME;
   17.82  
   17.83  fun export some_path f = (f (Export some_path); ());
   17.84  fun produce f = the (f Produce);
   17.85 -fun present stmt_names f = space_implode "\n\n" (map snd (fst (the (f (Present stmt_names)))));
   17.86 +fun present syms f = space_implode "\n\n" (map snd (fst (the (f (Present syms)))));
   17.87  
   17.88  
   17.89  (* serializers: functions producing serializations *)
   17.90 @@ -176,7 +176,6 @@
   17.91  type serializer = Token.T list
   17.92    -> Proof.context
   17.93    -> {
   17.94 -    symbol_of: string -> Code_Symbol.symbol,
   17.95      module_name: string,
   17.96      reserved_syms: string list,
   17.97      identifiers: identifier_data,
   17.98 @@ -193,7 +192,7 @@
   17.99        check: { env_var: string, make_destination: Path.T -> Path.T,
  17.100          make_command: string -> string } }
  17.101    | Extension of string *
  17.102 -      (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
  17.103 +      (Code_Thingol.program -> Code_Thingol.program);
  17.104  
  17.105  
  17.106  (** theory data **)
  17.107 @@ -311,10 +310,10 @@
  17.108           of SOME data => data
  17.109            | NONE => error ("Unknown code target language: " ^ quote target);
  17.110        in case the_description data
  17.111 -       of Fundamental _ => (K I, data)
  17.112 +       of Fundamental _ => (I, data)
  17.113          | Extension (super, modify) => let
  17.114              val (modify', data') = collapse super
  17.115 -          in (fn naming => modify' naming #> modify naming, merge_target false target (data', data)) end
  17.116 +          in (modify' #> modify, merge_target false target (data', data)) end
  17.117        end;
  17.118    in collapse end;
  17.119  
  17.120 @@ -326,68 +325,37 @@
  17.121      val (modify, data) = collapse_hierarchy thy target;
  17.122    in (default_width, data, modify) end;
  17.123  
  17.124 -fun activate_const_syntax thy literals cs_data naming =
  17.125 -  (Symtab.empty, naming)
  17.126 -  |> fold_map (fn (c, data) => fn (tab, naming) =>
  17.127 -      case Code_Thingol.lookup_const naming c
  17.128 -       of SOME name => let
  17.129 -              val (syn, naming') =
  17.130 -                Code_Printer.activate_const_syntax thy literals c data naming
  17.131 -            in (SOME name, (Symtab.update_new (name, syn) tab, naming')) end
  17.132 -        | NONE => (NONE, (tab, naming))) cs_data
  17.133 -  |>> map_filter I;
  17.134 +fun activate_symbol_syntax thy literals printings =
  17.135 +  (Code_Symbol.symbols_of printings,
  17.136 +    (Symtab.lookup (Code_Symbol.mapped_const_data (Code_Printer.activate_const_syntax thy literals) printings),
  17.137 +      Code_Symbol.lookup_type_constructor_data printings, Code_Symbol.lookup_type_class_data printings))
  17.138  
  17.139 -fun activate_syntax lookup_name things =
  17.140 -  Symtab.empty
  17.141 -  |> fold_map (fn (thing_identifier, data) => fn tab => case lookup_name thing_identifier
  17.142 -       of SOME name => (SOME name, Symtab.update_new (name, data) tab)
  17.143 -        | NONE => (NONE, tab)) things
  17.144 -  |>> map_filter I;
  17.145 -
  17.146 -fun activate_symbol_syntax thy literals naming printings =
  17.147 -  let
  17.148 -    val (names_const, (const_syntax, _)) =
  17.149 -      activate_const_syntax thy literals (Code_Symbol.dest_constant_data printings) naming;
  17.150 -    val (names_tyco, tyco_syntax) =
  17.151 -      activate_syntax (Code_Thingol.lookup_tyco naming) (Code_Symbol.dest_type_constructor_data printings);
  17.152 -    val (names_class, class_syntax) =
  17.153 -      activate_syntax (Code_Thingol.lookup_class naming) (Code_Symbol.dest_type_class_data printings);
  17.154 -    val names_inst = map_filter (Code_Thingol.lookup_instance naming o fst)
  17.155 -      (Code_Symbol.dest_class_instance_data printings);
  17.156 -  in
  17.157 -    (names_const @ names_tyco @ names_class @ names_inst,
  17.158 -      (Symtab.lookup const_syntax, Symtab.lookup tyco_syntax, Symtab.lookup class_syntax))
  17.159 -  end;
  17.160 -
  17.161 -fun project_program thy names_hidden names1 program2 =
  17.162 +fun project_program thy syms_hidden syms1 program2 =
  17.163    let
  17.164      val ctxt = Proof_Context.init_global thy;
  17.165 -    val names2 = subtract (op =) names_hidden names1;
  17.166 -    val program3 = Graph.restrict (not o member (op =) names_hidden) program2;
  17.167 -    val names4 = Graph.all_succs program3 names2;
  17.168 +    val syms2 = subtract (op =) syms_hidden syms1;
  17.169 +    val program3 = Code_Symbol.Graph.restrict (not o member (op =) syms_hidden) program2;
  17.170 +    val syms4 = Code_Symbol.Graph.all_succs program3 syms2;
  17.171      val unimplemented = Code_Thingol.unimplemented program3;
  17.172      val _ =
  17.173        if null unimplemented then ()
  17.174        else error ("No code equations for " ^
  17.175          commas (map (Proof_Context.extern_const ctxt) unimplemented));
  17.176 -    val program4 = Graph.restrict (member (op =) names4) program3;
  17.177 -  in (names4, program4) end;
  17.178 +    val program4 = Code_Symbol.Graph.restrict (member (op =) syms4) program3;
  17.179 +  in (syms4, program4) end;
  17.180  
  17.181  fun prepare_serializer thy (serializer : serializer) literals reserved identifiers
  17.182 -    printings module_name args naming proto_program names =
  17.183 +    printings module_name args proto_program syms =
  17.184    let
  17.185 -    val (names_hidden, (const_syntax, tyco_syntax, class_syntax)) =
  17.186 -      activate_symbol_syntax thy literals naming printings;
  17.187 -    val (names_all, program) = project_program thy names_hidden names proto_program;
  17.188 +    val (syms_hidden, (const_syntax, tyco_syntax, class_syntax)) =
  17.189 +      activate_symbol_syntax thy literals printings;
  17.190 +    val (syms_all, program) = project_program thy syms_hidden syms proto_program;
  17.191      fun select_include (name, (content, cs)) =
  17.192 -      if null cs orelse exists (fn c => case Code_Thingol.lookup_const naming c
  17.193 -       of SOME name => member (op =) names_all name
  17.194 -        | NONE => false) cs
  17.195 +      if null cs orelse exists (fn c => member (op =) syms_all (Code_Symbol.Constant c)) cs
  17.196        then SOME (name, content) else NONE;
  17.197      val includes = map_filter select_include (Code_Symbol.dest_module_data printings);
  17.198    in
  17.199      (serializer args (Proof_Context.init_global thy) {
  17.200 -      symbol_of = Code_Thingol.symbol_of proto_program,
  17.201        module_name = module_name,
  17.202        reserved_syms = reserved,
  17.203        identifiers = identifiers,
  17.204 @@ -398,7 +366,7 @@
  17.205        program)
  17.206    end;
  17.207  
  17.208 -fun mount_serializer thy target some_width module_name args naming program names =
  17.209 +fun mount_serializer thy target some_width module_name args program syms =
  17.210    let
  17.211      val (default_width, data, modify) = activate_target thy target;
  17.212      val serializer = case the_description data
  17.213 @@ -406,15 +374,15 @@
  17.214      val (prepared_serializer, prepared_program) =
  17.215        prepare_serializer thy serializer (the_literals thy target)
  17.216          (the_reserved data) (the_identifiers data) (the_printings data)
  17.217 -        module_name args naming (modify naming program) names
  17.218 +        module_name args (modify program) syms
  17.219      val width = the_default default_width some_width;
  17.220    in (fn program => prepared_serializer program width, prepared_program) end;
  17.221  
  17.222 -fun invoke_serializer thy target some_width module_name args naming program names =
  17.223 +fun invoke_serializer thy target some_width module_name args program syms =
  17.224    let
  17.225      val check = if module_name = "" then I else check_name true;
  17.226      val (mounted_serializer, prepared_program) = mount_serializer thy
  17.227 -      target some_width (check module_name) args naming program names;
  17.228 +      target some_width (check module_name) args program syms;
  17.229    in mounted_serializer prepared_program end;
  17.230  
  17.231  fun assert_module_name "" = error "Empty module name not allowed here"
  17.232 @@ -429,23 +397,23 @@
  17.233  
  17.234  fun export_code_for thy some_path target some_width module_name args =
  17.235    export (using_master_directory thy some_path)
  17.236 -  ooo invoke_serializer thy target some_width module_name args;
  17.237 +  oo invoke_serializer thy target some_width module_name args;
  17.238  
  17.239  fun produce_code_for thy target some_width module_name args =
  17.240    let
  17.241      val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args;
  17.242 -  in fn naming => fn program => fn names =>
  17.243 -    produce (serializer naming program names) |> apsnd (fn deresolve => map deresolve names)
  17.244 +  in fn program => fn syms =>
  17.245 +    produce (serializer program syms) |> apsnd (fn deresolve => map deresolve syms)
  17.246    end;
  17.247  
  17.248  fun present_code_for thy target some_width module_name args =
  17.249    let
  17.250      val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args;
  17.251 -  in fn naming => fn program => fn (names, selects) =>
  17.252 -    present selects (serializer naming program names)
  17.253 +  in fn program => fn (syms, selects) =>
  17.254 +    present selects (serializer program syms)
  17.255    end;
  17.256  
  17.257 -fun check_code_for thy target strict args naming program names_cs =
  17.258 +fun check_code_for thy target strict args program syms =
  17.259    let
  17.260      val { env_var, make_destination, make_command } =
  17.261        (#check o the_fundamental thy) target;
  17.262 @@ -453,7 +421,7 @@
  17.263        let
  17.264          val destination = make_destination p;
  17.265          val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
  17.266 -          generatedN args naming program names_cs);
  17.267 +          generatedN args program syms);
  17.268          val cmd = make_command generatedN;
  17.269        in
  17.270          if Isabelle_System.bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
  17.271 @@ -468,46 +436,38 @@
  17.272      else Isabelle_System.with_tmp_dir "Code_Test" ext_check
  17.273    end;
  17.274  
  17.275 -fun evaluation mounted_serializer prepared_program consts ((vs, ty), t) =
  17.276 +fun evaluation mounted_serializer prepared_program syms ((vs, ty), t) =
  17.277    let
  17.278      val _ = if Code_Thingol.contains_dict_var t then
  17.279        error "Term to be evaluated contains free dictionaries" else ();
  17.280      val v' = singleton (Name.variant_list (map fst vs)) "a";
  17.281      val vs' = (v', []) :: vs;
  17.282 -    val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty];
  17.283 -    val value_name = "Value.value.value"
  17.284 +    val ty' = ITyVar v' `-> ty;
  17.285      val program = prepared_program
  17.286 -      |> Graph.new_node (value_name,
  17.287 -          Code_Thingol.Fun (@{const_name dummy_pattern}, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
  17.288 -      |> fold (curry (perhaps o try o Graph.add_edge) value_name) consts;
  17.289 +      |> Code_Symbol.Graph.new_node (Code_Symbol.value,
  17.290 +          Code_Thingol.Fun (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE))
  17.291 +      |> fold (curry (perhaps o try o
  17.292 +          Code_Symbol.Graph.add_edge) Code_Symbol.value) syms;
  17.293      val (program_code, deresolve) = produce (mounted_serializer program);
  17.294 -    val value_name' = the (deresolve value_name);
  17.295 -  in (program_code, value_name') end;
  17.296 +    val value_name = the (deresolve Code_Symbol.value);
  17.297 +  in (program_code, value_name) end;
  17.298  
  17.299 -fun evaluator thy target naming program consts =
  17.300 +fun evaluator thy target program syms =
  17.301    let
  17.302 -    val (mounted_serializer, prepared_program) = mount_serializer thy
  17.303 -      target NONE generatedN [] naming program consts;
  17.304 -  in evaluation mounted_serializer prepared_program consts end;
  17.305 +    val (mounted_serializer, prepared_program) =
  17.306 +      mount_serializer thy target NONE generatedN [] program syms;
  17.307 +  in evaluation mounted_serializer prepared_program syms end;
  17.308  
  17.309  end; (* local *)
  17.310  
  17.311  
  17.312  (* code generation *)
  17.313  
  17.314 -fun implemented_functions thy naming program =
  17.315 +fun read_const_exprs thy const_exprs =
  17.316    let
  17.317 -    val cs = Code_Thingol.unimplemented program;
  17.318 -    val names = map_filter (Code_Thingol.lookup_const naming) cs;
  17.319 -  in subtract (op =) (Graph.all_preds program names) (Graph.keys program) end;
  17.320 -
  17.321 -fun read_const_exprs thy cs =
  17.322 -  let
  17.323 -    val (cs1, cs2) = Code_Thingol.read_const_exprs thy cs;
  17.324 -    val (names2, (naming, program)) = Code_Thingol.consts_program thy true cs2;
  17.325 -    val names3 = implemented_functions thy naming program;
  17.326 -    val cs3 = map_filter (fn (c, name) =>
  17.327 -      if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2);
  17.328 +    val (cs1, cs2) = Code_Thingol.read_const_exprs thy const_exprs;
  17.329 +    val program = Code_Thingol.consts_program thy true cs2;
  17.330 +    val cs3 = Code_Thingol.implemented_deps program;
  17.331    in union (op =) cs3 cs1 end;
  17.332  
  17.333  fun prep_destination "" = NONE
  17.334 @@ -515,9 +475,9 @@
  17.335  
  17.336  fun export_code thy cs seris =
  17.337    let
  17.338 -    val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
  17.339 +    val program = Code_Thingol.consts_program thy false cs;
  17.340      val _ = map (fn (((target, module_name), some_path), args) =>
  17.341 -      export_code_for thy some_path target NONE module_name args naming program names_cs) seris;
  17.342 +      export_code_for thy some_path target NONE module_name args program (map Code_Symbol.Constant cs)) seris;
  17.343    in () end;
  17.344  
  17.345  fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs)
  17.346 @@ -525,19 +485,19 @@
  17.347  
  17.348  fun produce_code thy cs target some_width some_module_name args =
  17.349    let
  17.350 -    val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
  17.351 -  in produce_code_for thy target some_width some_module_name args naming program names_cs end;
  17.352 +    val program = Code_Thingol.consts_program thy false cs;
  17.353 +  in produce_code_for thy target some_width some_module_name args program (map Code_Symbol.Constant cs) end;
  17.354  
  17.355 -fun present_code thy cs names_stmt target some_width some_module_name args =
  17.356 +fun present_code thy cs syms target some_width some_module_name args =
  17.357    let
  17.358 -    val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
  17.359 -  in present_code_for thy target some_width some_module_name args naming program (names_cs, names_stmt naming) end;
  17.360 +    val program = Code_Thingol.consts_program thy false cs;
  17.361 +  in present_code_for thy target some_width some_module_name args program (map Code_Symbol.Constant cs, syms) end;
  17.362  
  17.363  fun check_code thy cs seris =
  17.364    let
  17.365 -    val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
  17.366 +    val program = Code_Thingol.consts_program thy false cs;
  17.367      val _ = map (fn ((target, strict), args) =>
  17.368 -      check_code_for thy target strict args naming program names_cs) seris;
  17.369 +      check_code_for thy target strict args program (map Code_Symbol.Constant cs)) seris;
  17.370    in () end;
  17.371  
  17.372  fun check_code_cmd raw_cs seris thy = check_code thy (read_const_exprs thy raw_cs) seris;
  17.373 @@ -547,22 +507,22 @@
  17.374  val parse_const_terms = Scan.repeat1 Args.term
  17.375    >> (fn ts => fn thy => map (Code.check_const thy) ts);
  17.376  
  17.377 -fun parse_names category parse internalize lookup =
  17.378 +fun parse_names category parse internalize mark_symbol =
  17.379    Scan.lift (Args.parens (Args.$$$ category)) |-- Scan.repeat1 parse
  17.380 -  >> (fn xs => fn thy => fn naming => map_filter (lookup naming o internalize thy) xs);
  17.381 +  >> (fn xs => fn thy => map (mark_symbol o internalize thy) xs);
  17.382  
  17.383  val parse_consts = parse_names "consts" Args.term
  17.384 -  Code.check_const Code_Thingol.lookup_const;
  17.385 +  Code.check_const Code_Symbol.Constant;
  17.386  
  17.387  val parse_types = parse_names "types" (Scan.lift Args.name)
  17.388 -  Sign.intern_type Code_Thingol.lookup_tyco;
  17.389 +  Sign.intern_type Code_Symbol.Type_Constructor;
  17.390  
  17.391  val parse_classes = parse_names "classes" (Scan.lift Args.name)
  17.392 -  Sign.intern_class Code_Thingol.lookup_class;
  17.393 +  Sign.intern_class Code_Symbol.Type_Class;
  17.394  
  17.395  val parse_instances = parse_names "instances" (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name))
  17.396 -  (fn thy => fn (raw_tyco, raw_class) => (Sign.intern_class thy raw_class, Sign.intern_type thy raw_tyco))
  17.397 -    Code_Thingol.lookup_instance;
  17.398 +  (fn thy => fn (raw_tyco, raw_class) => (Sign.intern_class thy raw_tyco, Sign.intern_type thy raw_class))
  17.399 +    Code_Symbol.Class_Instance;
  17.400  
  17.401  in
  17.402  
  17.403 @@ -574,7 +534,7 @@
  17.404      (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target, some_width)) =>
  17.405        let val thy = Proof_Context.theory_of ctxt in
  17.406          present_code thy (mk_cs thy)
  17.407 -          (fn naming => maps (fn f => f thy naming) mk_stmtss)
  17.408 +          (maps (fn f => f thy) mk_stmtss)
  17.409            target some_width "Example" []
  17.410        end);
  17.411  
    18.1 --- a/src/Tools/Code/code_thingol.ML	Sat Jan 25 23:50:49 2014 +0100
    18.2 +++ b/src/Tools/Code/code_thingol.ML	Sat Jan 25 23:50:49 2014 +0100
    18.3 @@ -8,6 +8,7 @@
    18.4  infix 8 `%%;
    18.5  infix 4 `$;
    18.6  infix 4 `$$;
    18.7 +infixr 3 `->;
    18.8  infixr 3 `|=>;
    18.9  infixr 3 `|==>;
   18.10  
   18.11 @@ -15,14 +16,14 @@
   18.12  sig
   18.13    type vname = string;
   18.14    datatype dict =
   18.15 -      Dict of string list * plain_dict
   18.16 +      Dict of (class * class) list * plain_dict
   18.17    and plain_dict = 
   18.18 -      Dict_Const of string * dict list list
   18.19 +      Dict_Const of (string * class) * dict list list
   18.20      | Dict_Var of vname * (int * int);
   18.21    datatype itype =
   18.22        `%% of string * itype list
   18.23      | ITyVar of vname;
   18.24 -  type const = { name: string, typargs: itype list, dicts: dict list list,
   18.25 +  type const = { sym: Code_Symbol.symbol, typargs: itype list, dicts: dict list list,
   18.26      dom: itype list, range: itype, annotate: bool };
   18.27    datatype iterm =
   18.28        IConst of const
   18.29 @@ -30,6 +31,7 @@
   18.30      | `$ of iterm * iterm
   18.31      | `|=> of (vname option * itype) * iterm
   18.32      | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm };
   18.33 +  val `-> : itype * itype -> itype;
   18.34    val `$$ : iterm * iterm list -> iterm;
   18.35    val `|==> : (vname option * itype) list * iterm -> iterm;
   18.36    type typscheme = (vname * sort) list * itype;
   18.37 @@ -38,7 +40,6 @@
   18.38  signature CODE_THINGOL =
   18.39  sig
   18.40    include BASIC_CODE_THINGOL
   18.41 -  val fun_tyco: string
   18.42    val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list
   18.43    val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a
   18.44    val unfold_fun: itype -> itype list * itype
   18.45 @@ -54,59 +55,50 @@
   18.46    val is_IAbs: iterm -> bool
   18.47    val eta_expand: int -> const * iterm list -> iterm
   18.48    val contains_dict_var: iterm -> bool
   18.49 -  val add_constnames: iterm -> string list -> string list
   18.50 +  val add_constsyms: iterm -> Code_Symbol.symbol list -> Code_Symbol.symbol list
   18.51    val add_tyconames: iterm -> string list -> string list
   18.52    val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
   18.53  
   18.54 -  type naming
   18.55 -  val empty_naming: naming
   18.56 -  val lookup_class: naming -> class -> string option
   18.57 -  val lookup_classrel: naming -> class * class -> string option
   18.58 -  val lookup_tyco: naming -> string -> string option
   18.59 -  val lookup_instance: naming -> class * string -> string option
   18.60 -  val lookup_const: naming -> string -> string option
   18.61 -  val ensure_declared_const: theory -> string -> naming -> string * naming
   18.62 -
   18.63    datatype stmt =
   18.64 -      NoStmt of string
   18.65 -    | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
   18.66 -    | Datatype of string * (vname list *
   18.67 -        ((string * vname list (*type argument wrt. canonical order*)) * itype list) list)
   18.68 -    | Datatypecons of string * string
   18.69 -    | Class of class * (vname * ((class * string) list * (string * itype) list))
   18.70 +      NoStmt
   18.71 +    | Fun of (typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option
   18.72 +    | Datatype of vname list *
   18.73 +        ((string * vname list (*type argument wrt. canonical order*)) * itype list) list
   18.74 +    | Datatypecons of string
   18.75 +    | Class of vname * ((class * class) list * (string * itype) list)
   18.76      | Classrel of class * class
   18.77 -    | Classparam of string * class
   18.78 +    | Classparam of class
   18.79      | Classinst of { class: string, tyco: string, vs: (vname * sort) list,
   18.80 -        superinsts: (class * (string * (string * dict list list))) list,
   18.81 +        superinsts: (class * dict list list) list,
   18.82          inst_params: ((string * (const * int)) * (thm * bool)) list,
   18.83          superinst_params: ((string * (const * int)) * (thm * bool)) list };
   18.84 -  type program = stmt Graph.T
   18.85 +  type program = stmt Code_Symbol.Graph.T
   18.86    val unimplemented: program -> string list
   18.87 +  val implemented_deps: program -> string list
   18.88    val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
   18.89    val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
   18.90 -  val is_constr: program -> string -> bool
   18.91 +  val is_constr: program -> Code_Symbol.symbol -> bool
   18.92    val is_case: stmt -> bool
   18.93 -  val symbol_of: program -> string -> Code_Symbol.symbol;
   18.94    val group_stmts: theory -> program
   18.95 -    -> ((string * stmt) list * (string * stmt) list
   18.96 -      * ((string * stmt) list * (string * stmt) list)) list
   18.97 +    -> ((Code_Symbol.symbol * stmt) list * (Code_Symbol.symbol * stmt) list
   18.98 +      * ((Code_Symbol.symbol * stmt) list * (Code_Symbol.symbol * stmt) list)) list
   18.99  
  18.100    val read_const_exprs: theory -> string list -> string list * string list
  18.101 -  val consts_program: theory -> bool -> string list -> string list * (naming * program)
  18.102 -  val dynamic_conv: theory -> (naming -> program
  18.103 -    -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
  18.104 +  val consts_program: theory -> bool -> string list -> program
  18.105 +  val dynamic_conv: theory -> (program
  18.106 +    -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.symbol list -> conv)
  18.107      -> conv
  18.108 -  val dynamic_value: theory -> ((term -> term) -> 'a -> 'a) -> (naming -> program
  18.109 -    -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
  18.110 +  val dynamic_value: theory -> ((term -> term) -> 'a -> 'a) -> (program
  18.111 +    -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.symbol list -> 'a)
  18.112      -> term -> 'a
  18.113 -  val static_conv: theory -> string list -> (naming -> program -> string list
  18.114 -    -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
  18.115 +  val static_conv: theory -> string list -> (program -> string list
  18.116 +    -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.symbol list -> conv)
  18.117      -> conv
  18.118    val static_conv_simple: theory -> string list
  18.119      -> (program -> (string * sort) list -> term -> conv) -> conv
  18.120    val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list ->
  18.121 -    (naming -> program -> string list
  18.122 -      -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
  18.123 +    (program -> string list
  18.124 +      -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.symbol list -> 'a)
  18.125      -> term -> 'a
  18.126  end;
  18.127  
  18.128 @@ -133,16 +125,29 @@
  18.129  type vname = string;
  18.130  
  18.131  datatype dict =
  18.132 -    Dict of string list * plain_dict
  18.133 +    Dict of (class * class) list * plain_dict
  18.134  and plain_dict = 
  18.135 -    Dict_Const of string * dict list list
  18.136 +    Dict_Const of (string * class) * dict list list
  18.137    | Dict_Var of vname * (int * int);
  18.138  
  18.139  datatype itype =
  18.140      `%% of string * itype list
  18.141    | ITyVar of vname;
  18.142  
  18.143 -type const = { name: string, typargs: itype list, dicts: dict list list,
  18.144 +fun ty1 `-> ty2 = "fun" `%% [ty1, ty2];
  18.145 +
  18.146 +val unfold_fun = unfoldr
  18.147 +  (fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2)
  18.148 +    | _ => NONE);
  18.149 +
  18.150 +fun unfold_fun_n n ty =
  18.151 +  let
  18.152 +    val (tys1, ty1) = unfold_fun ty;
  18.153 +    val (tys3, tys2) = chop n tys1;
  18.154 +    val ty3 = Library.foldr (op `->) (tys2, ty1);
  18.155 +  in (tys3, ty3) end;
  18.156 +
  18.157 +type const = { sym: Code_Symbol.symbol, typargs: itype list, dicts: dict list list,
  18.158    dom: itype list, range: itype, annotate: bool };
  18.159  
  18.160  datatype iterm =
  18.161 @@ -191,7 +196,7 @@
  18.162            #> fold (fn (p, body) => fold' p #> fold' body) clauses
  18.163    in fold' end;
  18.164  
  18.165 -val add_constnames = fold_constexprs (fn { name = c, ... } => insert (op =) c);
  18.166 +val add_constsyms = fold_constexprs (fn { sym, ... } => insert (op =) sym);
  18.167  
  18.168  fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys
  18.169    | add_tycos (ITyVar _) = I;
  18.170 @@ -238,15 +243,15 @@
  18.171          val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
  18.172        in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
  18.173  
  18.174 -fun eta_expand k (const as { name = c, dom = tys, ... }, ts) =
  18.175 +fun eta_expand k (const as { dom = tys, ... }, ts) =
  18.176    let
  18.177      val j = length ts;
  18.178      val l = k - j;
  18.179      val _ = if l > length tys
  18.180 -      then error ("Impossible eta-expansion for constant " ^ quote c) else ();
  18.181 -    val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
  18.182 +      then error "Impossible eta-expansion" else ();
  18.183 +    val vars = (fold o fold_varnames) Name.declare ts Name.context;
  18.184      val vs_tys = (map o apfst) SOME
  18.185 -      (Name.invent_names ctxt "a" ((take l o drop j) tys));
  18.186 +      (Name.invent_names vars "a" ((take l o drop j) tys));
  18.187    in vs_tys `|==> IConst const `$$ ts @ map (IVar o fst) vs_tys end;
  18.188  
  18.189  fun contains_dict_var t =
  18.190 @@ -262,178 +267,31 @@
  18.191    in cont_term t end;
  18.192  
  18.193  
  18.194 -(** namings **)
  18.195 -
  18.196 -(* policies *)
  18.197 -
  18.198 -local
  18.199 -  fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
  18.200 -  fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy);
  18.201 -  fun thyname_of_instance thy inst = case Axclass.thynames_of_arity thy (swap inst)
  18.202 -   of [] => error ("No such instance: " ^ quote (snd inst ^ " :: " ^ fst inst))
  18.203 -    | thyname :: _ => thyname;
  18.204 -  fun thyname_of_const thy c = case Axclass.class_of_param thy c
  18.205 -   of SOME class => thyname_of_class thy class
  18.206 -    | NONE => (case Code.get_type_of_constr_or_abstr thy c
  18.207 -       of SOME (tyco, _) => thyname_of_type thy tyco
  18.208 -        | NONE => #theory_name (Name_Space.the_entry (Sign.const_space thy) c));
  18.209 -  fun namify thy get_basename get_thyname name =
  18.210 -    let
  18.211 -      val prefix = get_thyname thy name;
  18.212 -      val base = (Name.desymbolize false o get_basename) name;
  18.213 -    in Long_Name.append prefix base end;
  18.214 -in
  18.215 -
  18.216 -fun namify_class thy = namify thy Long_Name.base_name thyname_of_class;
  18.217 -fun namify_classrel thy = namify thy (fn (sub_class, super_class) => 
  18.218 -    Long_Name.base_name super_class ^ "_" ^ Long_Name.base_name sub_class)
  18.219 -  (fn thy => thyname_of_class thy o fst);
  18.220 -  (*order fits nicely with composed projections*)
  18.221 -fun namify_tyco thy "fun" = "Pure.fun"
  18.222 -  | namify_tyco thy tyco = namify thy Long_Name.base_name thyname_of_type tyco;
  18.223 -fun namify_instance thy = namify thy (fn (class, tyco) => 
  18.224 -  Long_Name.base_name class ^ "_" ^ Long_Name.base_name tyco) thyname_of_instance;
  18.225 -fun namify_const thy "==>" = "Pure.follows"
  18.226 -  | namify_const thy "==" = "Pure.meta_eq"
  18.227 -  | namify_const thy c = namify thy Long_Name.base_name thyname_of_const c;
  18.228 -
  18.229 -end; (* local *)
  18.230 -
  18.231 -
  18.232 -(* data *)
  18.233 -
  18.234 -datatype naming = Naming of {
  18.235 -  class: class Symtab.table * Name.context,
  18.236 -  classrel: string Symreltab.table * Name.context,
  18.237 -  tyco: string Symtab.table * Name.context,
  18.238 -  instance: string Symreltab.table * Name.context,
  18.239 -  const: string Symtab.table * Name.context
  18.240 -}
  18.241 -
  18.242 -fun dest_Naming (Naming naming) = naming;
  18.243 -
  18.244 -val empty_naming = Naming {
  18.245 -  class = (Symtab.empty, Name.context),
  18.246 -  classrel = (Symreltab.empty, Name.context),
  18.247 -  tyco = (Symtab.empty, Name.context),
  18.248 -  instance = (Symreltab.empty, Name.context),
  18.249 -  const = (Symtab.empty, Name.context)
  18.250 -};
  18.251 -
  18.252 -local
  18.253 -  fun mk_naming (class, classrel, tyco, instance, const) =
  18.254 -    Naming { class = class, classrel = classrel,
  18.255 -      tyco = tyco, instance = instance, const = const };
  18.256 -  fun map_naming f (Naming { class, classrel, tyco, instance, const }) =
  18.257 -    mk_naming (f (class, classrel, tyco, instance, const));
  18.258 -in
  18.259 -  fun map_class f = map_naming
  18.260 -    (fn (class, classrel, tyco, inst, const) =>
  18.261 -      (f class, classrel, tyco, inst, const));
  18.262 -  fun map_classrel f = map_naming
  18.263 -    (fn (class, classrel, tyco, inst, const) =>
  18.264 -      (class, f classrel, tyco, inst, const));
  18.265 -  fun map_tyco f = map_naming
  18.266 -    (fn (class, classrel, tyco, inst, const) =>
  18.267 -      (class, classrel, f tyco, inst, const));
  18.268 -  fun map_instance f = map_naming
  18.269 -    (fn (class, classrel, tyco, inst, const) =>
  18.270 -      (class, classrel, tyco, f inst, const));
  18.271 -  fun map_const f = map_naming
  18.272 -    (fn (class, classrel, tyco, inst, const) =>
  18.273 -      (class, classrel, tyco, inst, f const));
  18.274 -end; (*local*)
  18.275 -
  18.276 -fun add_variant update (thing, name) (tab, used) =
  18.277 -  let
  18.278 -    val (name', used') = Name.variant name used;
  18.279 -    val tab' = update (thing, name') tab;
  18.280 -  in (tab', used') end;
  18.281 -
  18.282 -fun declare thy mapp lookup update namify thing =
  18.283 -  mapp (add_variant update (thing, namify thy thing))
  18.284 -  #> `(fn naming => the (lookup naming thing));
  18.285 -
  18.286 -
  18.287 -(* lookup and declare *)
  18.288 -
  18.289 -local
  18.290 -
  18.291 -val suffix_class = "class";
  18.292 -val suffix_classrel = "classrel"
  18.293 -val suffix_tyco = "tyco";
  18.294 -val suffix_instance = "inst";
  18.295 -val suffix_const = "const";
  18.296 -
  18.297 -fun add_suffix nsp NONE = NONE
  18.298 -  | add_suffix nsp (SOME name) = SOME (Long_Name.append name nsp);
  18.299 -
  18.300 -in
  18.301 -
  18.302 -val lookup_class = add_suffix suffix_class
  18.303 -  oo Symtab.lookup o fst o #class o dest_Naming;
  18.304 -val lookup_classrel = add_suffix suffix_classrel
  18.305 -  oo Symreltab.lookup o fst o #classrel o dest_Naming;
  18.306 -val lookup_tyco = add_suffix suffix_tyco
  18.307 -  oo Symtab.lookup o fst o #tyco o dest_Naming;
  18.308 -val lookup_instance = add_suffix suffix_instance
  18.309 -  oo Symreltab.lookup o fst o #instance o dest_Naming;
  18.310 -val lookup_const = add_suffix suffix_const
  18.311 -  oo Symtab.lookup o fst o #const o dest_Naming;
  18.312 -
  18.313 -fun declare_class thy = declare thy map_class
  18.314 -  lookup_class Symtab.update_new namify_class;
  18.315 -fun declare_classrel thy = declare thy map_classrel
  18.316 -  lookup_classrel Symreltab.update_new namify_classrel;
  18.317 -fun declare_tyco thy = declare thy map_tyco
  18.318 -  lookup_tyco Symtab.update_new namify_tyco;
  18.319 -fun declare_instance thy = declare thy map_instance
  18.320 -  lookup_instance Symreltab.update_new namify_instance;
  18.321 -fun declare_const thy = declare thy map_const
  18.322 -  lookup_const Symtab.update_new namify_const;
  18.323 -
  18.324 -fun ensure_declared_const thy const naming =
  18.325 -  case lookup_const naming const
  18.326 -   of SOME const' => (const', naming)
  18.327 -    | NONE => declare_const thy const naming;
  18.328 -
  18.329 -val fun_tyco = Long_Name.append (namify_tyco Pure.thy "fun") suffix_tyco
  18.330 -  (*depends on add_suffix*);
  18.331 -
  18.332 -val unfold_fun = unfoldr
  18.333 -  (fn tyco `%% [ty1, ty2] => if tyco = fun_tyco then SOME (ty1, ty2) else NONE
  18.334 -    | _ => NONE);
  18.335 -
  18.336 -fun unfold_fun_n n ty =
  18.337 -  let
  18.338 -    val (tys1, ty1) = unfold_fun ty;
  18.339 -    val (tys3, tys2) = chop n tys1;
  18.340 -    val ty3 = Library.foldr (fn (ty1, ty2) => fun_tyco `%% [ty1, ty2]) (tys2, ty1);
  18.341 -  in (tys3, ty3) end;
  18.342 -
  18.343 -end; (* local *)
  18.344 -
  18.345 -
  18.346  (** statements, abstract programs **)
  18.347  
  18.348  type typscheme = (vname * sort) list * itype;
  18.349  datatype stmt =
  18.350 -    NoStmt of string
  18.351 -  | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
  18.352 -  | Datatype of string * (vname list * ((string * vname list) * itype list) list)
  18.353 -  | Datatypecons of string * string
  18.354 -  | Class of class * (vname * ((class * string) list * (string * itype) list))
  18.355 +    NoStmt
  18.356 +  | Fun of (typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option
  18.357 +  | Datatype of vname list * ((string * vname list) * itype list) list
  18.358 +  | Datatypecons of string
  18.359 +  | Class of vname * ((class * class) list * (string * itype) list)
  18.360    | Classrel of class * class
  18.361 -  | Classparam of string * class
  18.362 +  | Classparam of class
  18.363    | Classinst of { class: string, tyco: string, vs: (vname * sort) list,
  18.364 -      superinsts: (class * (string * (string * dict list list))) list,
  18.365 +      superinsts: (class * dict list list) list,
  18.366        inst_params: ((string * (const * int)) * (thm * bool)) list,
  18.367        superinst_params: ((string * (const * int)) * (thm * bool)) list };
  18.368  
  18.369 -type program = stmt Graph.T;
  18.370 +type program = stmt Code_Symbol.Graph.T;
  18.371  
  18.372  fun unimplemented program =
  18.373 -  Graph.fold (fn (_, (NoStmt c, _)) => cons c | _ => I) program [];
  18.374 +  Code_Symbol.Graph.fold (fn (Code_Symbol.Constant c, (NoStmt, _)) => cons c | _ => I) program [];
  18.375 +
  18.376 +fun implemented_deps program =
  18.377 +  Code_Symbol.Graph.keys program
  18.378 +  |> subtract (op =) (Code_Symbol.Graph.all_preds program (map Code_Symbol.Constant (unimplemented program)))
  18.379 +  |> map_filter (fn Code_Symbol.Constant c => SOME c | _ => NONE);
  18.380  
  18.381  fun map_terms_bottom_up f (t as IConst _) = f t
  18.382    | map_terms_bottom_up f (t as IVar _) = f t
  18.383 @@ -449,9 +307,9 @@
  18.384  fun map_classparam_instances_as_term f =
  18.385    (map o apfst o apsnd o apfst) (fn const => case f (IConst const) of IConst const' => const')
  18.386  
  18.387 -fun map_terms_stmt f (NoStmt c) = (NoStmt c)
  18.388 -  | map_terms_stmt f (Fun (c, ((tysm, eqs), case_cong))) = Fun (c, ((tysm, (map o apfst)
  18.389 -      (fn (ts, t) => (map f ts, f t)) eqs), case_cong))
  18.390 +fun map_terms_stmt f NoStmt = NoStmt
  18.391 +  | map_terms_stmt f (Fun ((tysm, eqs), case_cong)) = Fun ((tysm, (map o apfst)
  18.392 +      (fn (ts, t) => (map f ts, f t)) eqs), case_cong)
  18.393    | map_terms_stmt f (stmt as Datatype _) = stmt
  18.394    | map_terms_stmt f (stmt as Datatypecons _) = stmt
  18.395    | map_terms_stmt f (stmt as Class _) = stmt
  18.396 @@ -463,41 +321,16 @@
  18.397            inst_params = map_classparam_instances_as_term f inst_params,
  18.398            superinst_params = map_classparam_instances_as_term f superinst_params };
  18.399  
  18.400 -fun is_constr program name = case Graph.get_node program name
  18.401 +fun is_constr program sym = case Code_Symbol.Graph.get_node program sym
  18.402   of Datatypecons _ => true
  18.403    | _ => false;
  18.404  
  18.405 -fun is_case (Fun (_, (_, SOME _))) = true
  18.406 +fun is_case (Fun (_, SOME _)) = true
  18.407    | is_case _ = false;
  18.408  
  18.409 -fun symbol_of program name = 
  18.410 -  case try (Graph.get_node program) name of
  18.411 -      NONE => Code_Symbol.Module "(unknown)"
  18.412 -        (*FIXME: need to be liberal due to ad-hoc introduction of value for evaluation*)
  18.413 -    | SOME stmt => case stmt of
  18.414 -          Fun (c, _) => Code_Symbol.Constant c
  18.415 -        | Datatype (tyco, _) => Code_Symbol.Type_Constructor tyco
  18.416 -        | Datatypecons (c, _) => Code_Symbol.Constant c
  18.417 -        | Class (class, _) => Code_Symbol.Type_Class class
  18.418 -        | Classrel (sub, super) =>
  18.419 -            let
  18.420 -              val Class (sub, _) = Graph.get_node program sub;
  18.421 -              val Class (super, _) = Graph.get_node program super;
  18.422 -            in
  18.423 -              Code_Symbol.Class_Relation (sub, super)
  18.424 -            end
  18.425 -        | Classparam (c, _) => Code_Symbol.Constant c
  18.426 -        | Classinst { class, tyco, ... } =>
  18.427 -            let
  18.428 -              val Class (class, _) = Graph.get_node program class;
  18.429 -              val Datatype (tyco, _) = Graph.get_node program tyco;
  18.430 -            in
  18.431 -              Code_Symbol.Class_Instance (tyco, class)
  18.432 -            end;
  18.433 -
  18.434  fun linear_stmts program =
  18.435 -  rev (Graph.strong_conn program)
  18.436 -  |> map (AList.make (Graph.get_node program));
  18.437 +  rev (Code_Symbol.Graph.strong_conn program)
  18.438 +  |> map (AList.make (Code_Symbol.Graph.get_node program));
  18.439  
  18.440  fun group_stmts thy program =
  18.441    let
  18.442 @@ -516,8 +349,8 @@
  18.443        else if forall (is_fun orf is_classinst) stmts
  18.444        then ([], [], List.partition is_fun stmts)
  18.445        else error ("Illegal mutual dependencies: " ^ (commas
  18.446 -        o map (Code_Symbol.quote_symbol (Proof_Context.init_global thy)
  18.447 -        o symbol_of program o fst)) stmts);
  18.448 +        o map (Code_Symbol.quote (Proof_Context.init_global thy)
  18.449 +        o fst)) stmts);
  18.450    in
  18.451      linear_stmts program
  18.452      |> map group
  18.453 @@ -528,31 +361,27 @@
  18.454  
  18.455  (* generic mechanisms *)
  18.456  
  18.457 -fun ensure_stmt lookup declare generate thing (dep, (naming, program)) =
  18.458 +fun ensure_stmt symbolize generate x (dep, program) =
  18.459    let
  18.460 -    fun add_dep name = case dep of NONE => I
  18.461 -      | SOME dep => Graph.add_edge (dep, name);
  18.462 -    val (name, naming') = case lookup naming thing
  18.463 -     of SOME name => (name, naming)
  18.464 -      | NONE => declare thing naming;
  18.465 +    val sym = symbolize x;
  18.466 +    val add_dep = case dep of NONE => I
  18.467 +      | SOME dep => Code_Symbol.Graph.add_edge (dep, sym);
  18.468    in
  18.469 -    if can (Graph.get_node program) name
  18.470 +    if can (Code_Symbol.Graph.get_node program) sym
  18.471      then
  18.472        program
  18.473 -      |> add_dep name
  18.474 -      |> pair naming'
  18.475 +      |> add_dep
  18.476        |> pair dep
  18.477 -      |> pair name
  18.478 +      |> pair x
  18.479      else
  18.480        program
  18.481 -      |> Graph.default_node (name, NoStmt "")
  18.482 -      |> add_dep name
  18.483 -      |> pair naming'
  18.484 -      |> curry generate (SOME name)
  18.485 +      |> Code_Symbol.Graph.default_node (sym, NoStmt)
  18.486 +      |> add_dep
  18.487 +      |> curry generate (SOME sym)
  18.488        ||> snd
  18.489 -      |-> (fn stmt => (apsnd o Graph.map_node name) (K stmt))
  18.490 +      |-> (fn stmt => (Code_Symbol.Graph.map_node sym) (K stmt))
  18.491        |> pair dep
  18.492 -      |> pair name
  18.493 +      |> pair x
  18.494    end;
  18.495  
  18.496  exception PERMISSIVE of unit;
  18.497 @@ -582,10 +411,6 @@
  18.498        (err_typ ^ "\n" ^ err_class)
  18.499    end;
  18.500  
  18.501 -fun undefineds thy (dep, (naming, program)) =
  18.502 -  (map_filter (lookup_const naming) (Code.undefineds thy),
  18.503 -    (dep, (naming, program)));
  18.504 -
  18.505  
  18.506  (* inference of type annotations for disambiguation with type classes *)
  18.507  
  18.508 @@ -640,18 +465,18 @@
  18.509          ensure_const thy algbr eqngr permissive c
  18.510          ##>> pair (map (unprefix "'" o fst) vs)
  18.511          ##>> fold_map (translate_typ thy algbr eqngr permissive) tys) cos
  18.512 -      #>> (fn info => Datatype (tyco, info));
  18.513 -  in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end
  18.514 +      #>> Datatype;
  18.515 +  in ensure_stmt Code_Symbol.Type_Constructor stmt_datatype tyco end
  18.516  and ensure_const thy algbr eqngr permissive c =
  18.517    let
  18.518      fun stmt_datatypecons tyco =
  18.519        ensure_tyco thy algbr eqngr permissive tyco
  18.520 -      #>> (fn tyco => Datatypecons (c, tyco));
  18.521 +      #>> Datatypecons;
  18.522      fun stmt_classparam class =
  18.523        ensure_class thy algbr eqngr permissive class
  18.524 -      #>> (fn class => Classparam (c, class));
  18.525 +      #>> Classparam;
  18.526      fun stmt_fun cert = case Code.equations_of_cert thy cert
  18.527 -     of (_, NONE) => pair (NoStmt c)
  18.528 +     of (_, NONE) => pair NoStmt
  18.529        | ((vs, ty), SOME eqns) =>
  18.530            let
  18.531              val eqns' = annotate_eqns thy algbr eqngr (c, ty) eqns
  18.532 @@ -661,34 +486,34 @@
  18.533              ##>> translate_typ thy algbr eqngr permissive ty
  18.534              ##>> translate_eqns thy algbr eqngr permissive eqns'
  18.535              #>>
  18.536 -             (fn (_, NONE) => NoStmt c
  18.537 -               | (tyscm, SOME eqns) => Fun (c, ((tyscm, eqns), some_case_cong)))
  18.538 +             (fn (_, NONE) => NoStmt
  18.539 +               | (tyscm, SOME eqns) => Fun ((tyscm, eqns), some_case_cong))
  18.540            end;
  18.541      val stmt_const = case Code.get_type_of_constr_or_abstr thy c
  18.542       of SOME (tyco, _) => stmt_datatypecons tyco
  18.543        | NONE => (case Axclass.class_of_param thy c
  18.544           of SOME class => stmt_classparam class
  18.545            | NONE => stmt_fun (Code_Preproc.cert eqngr c))
  18.546 -  in ensure_stmt lookup_const (declare_const thy) stmt_const c end
  18.547 +  in ensure_stmt Code_Symbol.Constant stmt_const c end
  18.548  and ensure_class thy (algbr as (_, algebra)) eqngr permissive class =
  18.549    let
  18.550      val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
  18.551      val cs = #params (Axclass.get_info thy class);
  18.552      val stmt_class =
  18.553 -      fold_map (fn super_class => ensure_class thy algbr eqngr permissive super_class
  18.554 -        ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)) super_classes
  18.555 +      fold_map (fn super_class =>
  18.556 +        ensure_classrel thy algbr eqngr permissive (class, super_class)) super_classes
  18.557        ##>> fold_map (fn (c, ty) => ensure_const thy algbr eqngr permissive c
  18.558          ##>> translate_typ thy algbr eqngr permissive ty) cs
  18.559 -      #>> (fn info => Class (class, (unprefix "'" Name.aT, info)))
  18.560 -  in ensure_stmt lookup_class (declare_class thy) stmt_class class end
  18.561 +      #>> (fn info => Class (unprefix "'" Name.aT, info))
  18.562 +  in ensure_stmt Code_Symbol.Type_Class stmt_class class end
  18.563  and ensure_classrel thy algbr eqngr permissive (sub_class, super_class) =
  18.564    let
  18.565      val stmt_classrel =
  18.566        ensure_class thy algbr eqngr permissive sub_class
  18.567        ##>> ensure_class thy algbr eqngr permissive super_class
  18.568        #>> Classrel;
  18.569 -  in ensure_stmt lookup_classrel (declare_classrel thy) stmt_classrel (sub_class, super_class) end
  18.570 -and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (class, tyco) =
  18.571 +  in ensure_stmt Code_Symbol.Class_Relation stmt_classrel (sub_class, super_class) end
  18.572 +and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (tyco, class) =
  18.573    let
  18.574      val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
  18.575      val these_class_params = these o try (#params o Axclass.get_info thy);
  18.576 @@ -703,10 +528,8 @@
  18.577      val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
  18.578      fun translate_super_instance super_class =
  18.579        ensure_class thy algbr eqngr permissive super_class
  18.580 -      ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)
  18.581        ##>> translate_dicts thy algbr eqngr permissive NONE (arity_typ, [super_class])
  18.582 -      #>> (fn ((super_class, classrel), [Dict ([], Dict_Const (inst, dss))]) =>
  18.583 -            (super_class, (classrel, (inst, dss))));
  18.584 +      #>> (fn (super_class, [Dict ([], Dict_Const (_, dss))]) => (super_class, dss));
  18.585      fun translate_classparam_instance (c, ty) =
  18.586        let
  18.587          val raw_const = Const (c, map_type_tfree (K arity_typ') ty);
  18.588 @@ -729,7 +552,7 @@
  18.589        #>> (fn (((((class, tyco), vs), superinsts), inst_params), superinst_params) =>
  18.590            Classinst { class = class, tyco = tyco, vs = vs,
  18.591              superinsts = superinsts, inst_params = inst_params, superinst_params = superinst_params });
  18.592 -  in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
  18.593 +  in ensure_stmt Code_Symbol.Class_Instance stmt_inst (tyco, class) end
  18.594  and translate_typ thy algbr eqngr permissive (TFree (v, _)) =
  18.595        pair (ITyVar (unprefix "'" v))
  18.596    | translate_typ thy algbr eqngr permissive (Type (tyco, tys)) =
  18.597 @@ -781,7 +604,7 @@
  18.598      ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (typargs ~~ sorts)
  18.599      ##>> fold_map (translate_typ thy algbr eqngr permissive) (range :: dom)
  18.600      #>> (fn (((c, typargs), dss), range :: dom) =>
  18.601 -      IConst { name = c, typargs = typargs, dicts = dss,
  18.602 +      IConst { sym = Code_Symbol.Constant c, typargs = typargs, dicts = dss,
  18.603          dom = dom, range = range, annotate = annotate })
  18.604    end
  18.605  and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
  18.606 @@ -790,6 +613,7 @@
  18.607    #>> (fn (t, ts) => t `$$ ts)
  18.608  and translate_case thy algbr eqngr permissive some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
  18.609    let
  18.610 +    val undefineds = Code.undefineds thy;
  18.611      fun arg_types num_args ty = fst (chop num_args (binder_types ty));
  18.612      val tys = arg_types num_args (snd c_ty);
  18.613      val ty = nth tys t_pos;
  18.614 @@ -801,11 +625,11 @@
  18.615      val constrs =
  18.616        if null case_pats then []
  18.617        else map_filter I (map2 mk_constr case_pats (nth_drop t_pos ts));
  18.618 -    fun casify undefineds constrs ty t_app ts =
  18.619 +    fun casify constrs ty t_app ts =
  18.620        let
  18.621          fun collapse_clause vs_map ts body =
  18.622            case body
  18.623 -           of IConst { name = c, ... } => if member (op =) undefineds c
  18.624 +           of IConst { sym = Code_Symbol.Constant c, ... } => if member (op =) undefineds c
  18.625                  then []
  18.626                  else [(ts, body)]
  18.627              | ICase { term = IVar (SOME v), clauses = clauses, ... } =>
  18.628 @@ -839,9 +663,8 @@
  18.629        #>> rpair n) constrs
  18.630      ##>> translate_typ thy algbr eqngr permissive ty
  18.631      ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
  18.632 -    ##>> undefineds thy
  18.633 -    #>> (fn ((((t, constrs), ty), ts), undefineds) =>
  18.634 -      casify undefineds constrs ty t ts)
  18.635 +    #>> (fn (((t, constrs), ty), ts) =>
  18.636 +      casify constrs ty t ts)
  18.637    end
  18.638  and translate_app_case thy algbr eqngr permissive some_thm (case_scheme as (num_args, _)) ((c, ty), ts) =
  18.639    if length ts < num_args then
  18.640 @@ -873,12 +696,12 @@
  18.641      datatype typarg_witness =
  18.642          Weakening of (class * class) list * plain_typarg_witness
  18.643      and plain_typarg_witness =
  18.644 -        Global of (class * string) * typarg_witness list list
  18.645 +        Global of (string * class) * typarg_witness list list
  18.646        | Local of string * (int * sort);
  18.647      fun class_relation ((Weakening (classrels, x)), sub_class) super_class =
  18.648        Weakening ((sub_class, super_class) :: classrels, x);
  18.649      fun type_constructor (tyco, _) dss class =
  18.650 -      Weakening ([], Global ((class, tyco), (map o map) fst dss));
  18.651 +      Weakening ([], Global ((tyco, class), (map o map) fst dss));
  18.652      fun type_variable (TFree (v, sort)) =
  18.653        let
  18.654          val sort' = proj_sort sort;
  18.655 @@ -905,31 +728,33 @@
  18.656  
  18.657  structure Program = Code_Data
  18.658  (
  18.659 -  type T = naming * program;
  18.660 -  val empty = (empty_naming, Graph.empty);
  18.661 +  type T = program;
  18.662 +  val empty = Code_Symbol.Graph.empty;
  18.663  );
  18.664  
  18.665  fun invoke_generation ignore_cache thy (algebra, eqngr) generate thing =
  18.666    Program.change_yield (if ignore_cache then NONE else SOME thy)
  18.667 -    (fn naming_program => (NONE, naming_program)
  18.668 +    (fn program => (NONE, program)
  18.669        |> generate thy algebra eqngr thing
  18.670 -      |-> (fn thing => fn (_, naming_program) => (thing, naming_program)));
  18.671 +      |-> (fn thing => fn (_, program) => (thing, program)));
  18.672  
  18.673  
  18.674  (* program generation *)
  18.675  
  18.676  fun consts_program thy permissive consts =
  18.677    let
  18.678 -    fun project_consts consts (naming, program) =
  18.679 -      if permissive then (consts, (naming, program))
  18.680 -      else (consts, (naming, Graph.restrict
  18.681 -        (member (op =) (Graph.all_succs program consts)) program));
  18.682 +    fun project program =
  18.683 +      if permissive then program
  18.684 +      else Code_Symbol.Graph.restrict
  18.685 +        (member (op =) (Code_Symbol.Graph.all_succs program
  18.686 +          (map Code_Symbol.Constant consts))) program;
  18.687      fun generate_consts thy algebra eqngr =
  18.688        fold_map (ensure_const thy algebra eqngr permissive);
  18.689    in
  18.690      invoke_generation permissive thy (Code_Preproc.obtain false thy consts [])
  18.691        generate_consts consts
  18.692 -    |-> project_consts
  18.693 +    |> snd
  18.694 +    |> project
  18.695    end;
  18.696  
  18.697  
  18.698 @@ -941,23 +766,24 @@
  18.699      val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
  18.700        o dest_TFree))) t [];
  18.701      val t' = annotate thy algbr eqngr (@{const_name dummy_pattern}, ty) [] t;
  18.702 +    val dummy_constant = Code_Symbol.Constant @{const_name dummy_pattern};
  18.703      val stmt_value =
  18.704        fold_map (translate_tyvar_sort thy algbr eqngr false) vs
  18.705        ##>> translate_typ thy algbr eqngr false ty
  18.706        ##>> translate_term thy algbr eqngr false NONE (t', NONE)
  18.707        #>> (fn ((vs, ty), t) => Fun
  18.708 -        (@{const_name dummy_pattern}, (((vs, ty), [(([], t), (NONE, true))]), NONE)));
  18.709 -    fun term_value (dep, (naming, program1)) =
  18.710 +        (((vs, ty), [(([], t), (NONE, true))]), NONE));
  18.711 +    fun term_value (dep, program1) =
  18.712        let
  18.713 -        val Fun (_, ((vs_ty, [(([], t), _)]), _)) =
  18.714 -          Graph.get_node program1 @{const_name dummy_pattern};
  18.715 -        val deps = Graph.immediate_succs program1 @{const_name dummy_pattern};
  18.716 -        val program2 = Graph.del_node @{const_name dummy_pattern} program1;
  18.717 -        val deps_all = Graph.all_succs program2 deps;
  18.718 -        val program3 = Graph.restrict (member (op =) deps_all) program2;
  18.719 -      in (((naming, program3), ((vs_ty, t), deps)), (dep, (naming, program2))) end;
  18.720 +        val Fun ((vs_ty, [(([], t), _)]), _) =
  18.721 +          Code_Symbol.Graph.get_node program1 dummy_constant;
  18.722 +        val deps = Code_Symbol.Graph.immediate_succs program1 dummy_constant;
  18.723 +        val program2 = Code_Symbol.Graph.del_node dummy_constant program1;
  18.724 +        val deps_all = Code_Symbol.Graph.all_succs program2 deps;
  18.725 +        val program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2;
  18.726 +      in ((program3, ((vs_ty, t), deps)), (dep, program2)) end;
  18.727    in
  18.728 -    ensure_stmt ((K o K) NONE) pair stmt_value @{const_name dummy_pattern}
  18.729 +    ensure_stmt Code_Symbol.Constant stmt_value @{const_name dummy_pattern}
  18.730      #> snd
  18.731      #> term_value
  18.732    end;
  18.733 @@ -967,9 +793,9 @@
  18.734  
  18.735  fun dynamic_evaluator thy evaluator algebra eqngr vs t =
  18.736    let
  18.737 -    val (((naming, program), (((vs', ty'), t'), deps)), _) =
  18.738 +    val ((program, (((vs', ty'), t'), deps)), _) =
  18.739        invoke_generation false thy (algebra, eqngr) ensure_value t;
  18.740 -  in evaluator naming program ((original_sorts vs vs', (vs', ty')), t') deps end;
  18.741 +  in evaluator program ((original_sorts vs vs', (vs', ty')), t') deps end;
  18.742  
  18.743  fun dynamic_conv thy evaluator =
  18.744    Code_Preproc.dynamic_conv thy (dynamic_evaluator thy evaluator);
  18.745 @@ -977,26 +803,26 @@
  18.746  fun dynamic_value thy postproc evaluator =
  18.747    Code_Preproc.dynamic_value thy postproc (dynamic_evaluator thy evaluator);
  18.748  
  18.749 -fun lift_evaluation thy evaluation' algebra eqngr naming program vs t =
  18.750 +fun lift_evaluation thy evaluation' algebra eqngr program vs t =
  18.751    let
  18.752 -    val (((_, _), (((vs', ty'), t'), deps)), _) =
  18.753 -      ensure_value thy algebra eqngr t (NONE, (naming, program));
  18.754 +    val ((_, (((vs', ty'), t'), deps)), _) =
  18.755 +      ensure_value thy algebra eqngr t (NONE, program);
  18.756    in evaluation' ((original_sorts vs vs', (vs', ty')), t') deps end;
  18.757  
  18.758  fun lift_evaluator thy evaluator' consts algebra eqngr =
  18.759    let
  18.760      fun generate_consts thy algebra eqngr =
  18.761        fold_map (ensure_const thy algebra eqngr false);
  18.762 -    val (consts', (naming, program)) =
  18.763 +    val (consts', program) =
  18.764        invoke_generation true thy (algebra, eqngr) generate_consts consts;
  18.765 -    val evaluation' = evaluator' naming program consts';
  18.766 -  in lift_evaluation thy evaluation' algebra eqngr naming program end;
  18.767 +    val evaluation' = evaluator' program consts';
  18.768 +  in lift_evaluation thy evaluation' algebra eqngr program end;
  18.769  
  18.770  fun lift_evaluator_simple thy evaluator' consts algebra eqngr =
  18.771    let
  18.772      fun generate_consts thy algebra eqngr =
  18.773        fold_map (ensure_const thy algebra eqngr false);
  18.774 -    val (_, (_, program)) =
  18.775 +    val (_, program) =
  18.776        invoke_generation true thy (algebra, eqngr) generate_consts consts;
  18.777    in evaluator' program end;
  18.778  
    19.1 --- a/src/Tools/nbe.ML	Sat Jan 25 23:50:49 2014 +0100
    19.2 +++ b/src/Tools/nbe.ML	Sat Jan 25 23:50:49 2014 +0100
    19.3 @@ -249,11 +249,11 @@
    19.4  
    19.5  val univs_cookie = (Univs.get, put_result, name_put);
    19.6  
    19.7 -val sloppy_name = Long_Name.base_name o Long_Name.qualifier
    19.8 +val sloppy_name = Code_Symbol.base_name;
    19.9  
   19.10 -fun nbe_fun idx_of 0 "" = "nbe_value"
   19.11 -  | nbe_fun idx_of i c = "c_" ^ string_of_int (idx_of c)
   19.12 -      ^ "_" ^ sloppy_name c ^ "_" ^ string_of_int i;
   19.13 +fun nbe_fun idx_of 0 (Code_Symbol.Constant "") = "nbe_value"
   19.14 +  | nbe_fun idx_of i sym = "c_" ^ string_of_int (idx_of sym)
   19.15 +      ^ "_" ^ sloppy_name sym ^ "_" ^ string_of_int i;
   19.16  fun nbe_dict v n = "d_" ^ v ^ "_" ^ string_of_int n;
   19.17  fun nbe_bound v = "v_" ^ v;
   19.18  fun nbe_bound_optional NONE = "_"
   19.19 @@ -291,24 +291,24 @@
   19.20        in (c, (num_args, (dicts, eqns))) end;
   19.21      val eqnss' = map prep_eqns eqnss;
   19.22  
   19.23 -    fun assemble_constapp c dss ts = 
   19.24 +    fun assemble_constapp sym dss ts = 
   19.25        let
   19.26          val ts' = (maps o map) assemble_dict dss @ ts;
   19.27 -      in case AList.lookup (op =) eqnss' c
   19.28 +      in case AList.lookup (op =) eqnss' sym
   19.29         of SOME (num_args, _) => if num_args <= length ts'
   19.30              then let val (ts1, ts2) = chop num_args ts'
   19.31 -            in nbe_apps (nbe_apps_local idx_of 0 c ts1) ts2
   19.32 -            end else nbe_apps (nbe_abss num_args (nbe_fun idx_of 0 c)) ts'
   19.33 -        | NONE => if member (op =) deps c
   19.34 -            then nbe_apps (nbe_fun idx_of 0 c) ts'
   19.35 -            else nbe_apps_constr idx_of c ts'
   19.36 +            in nbe_apps (nbe_apps_local idx_of 0 sym ts1) ts2
   19.37 +            end else nbe_apps (nbe_abss num_args (nbe_fun idx_of 0 sym)) ts'
   19.38 +        | NONE => if member (op =) deps sym
   19.39 +            then nbe_apps (nbe_fun idx_of 0 sym) ts'
   19.40 +            else nbe_apps_constr idx_of sym ts'
   19.41        end
   19.42      and assemble_classrels classrels =
   19.43 -      fold_rev (fn classrel => assemble_constapp classrel [] o single) classrels
   19.44 +      fold_rev (fn classrel => assemble_constapp (Code_Symbol.Class_Relation classrel) [] o single) classrels
   19.45      and assemble_dict (Dict (classrels, x)) =
   19.46            assemble_classrels classrels (assemble_plain_dict x)
   19.47      and assemble_plain_dict (Dict_Const (inst, dss)) =
   19.48 -          assemble_constapp inst dss []
   19.49 +          assemble_constapp (Code_Symbol.Class_Instance inst) dss []
   19.50        | assemble_plain_dict (Dict_Var (v, (n, _))) =
   19.51            nbe_dict v n
   19.52  
   19.53 @@ -318,7 +318,7 @@
   19.54            let
   19.55              val (t', ts) = Code_Thingol.unfold_app t
   19.56            in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
   19.57 -        and of_iapp match_cont (IConst { name = c, dicts = dss, ... }) ts = constapp c dss ts
   19.58 +        and of_iapp match_cont (IConst { sym, dicts = dss, ... }) ts = constapp sym dss ts
   19.59            | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts
   19.60            | of_iapp match_cont ((v, _) `|=> t) ts =
   19.61                nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts
   19.62 @@ -353,12 +353,12 @@
   19.63          val (args', _) = fold_map subst_vars args samepairs;
   19.64        in (samepairs, args') end;
   19.65  
   19.66 -    fun assemble_eqn c dicts default_args (i, (args, rhs)) =
   19.67 +    fun assemble_eqn sym dicts default_args (i, (args, rhs)) =
   19.68        let
   19.69 -        val match_cont = if c = "" then NONE
   19.70 -          else SOME (nbe_apps_local idx_of (i + 1) c (dicts @ default_args));
   19.71 +        val match_cont = if Code_Symbol.is_value sym then NONE
   19.72 +          else SOME (nbe_apps_local idx_of (i + 1) sym (dicts @ default_args));
   19.73          val assemble_arg = assemble_iterm
   19.74 -          (fn c => fn dss => fn ts => nbe_apps_constr idx_of c ((maps o map) (K "_") dss @ ts)) NONE;
   19.75 +          (fn sym' => fn dss => fn ts => nbe_apps_constr idx_of sym' ((maps o map) (K "_") dss @ ts)) NONE;
   19.76          val assemble_rhs = assemble_iterm assemble_constapp match_cont;
   19.77          val (samepairs, args') = subst_nonlin_vars args;
   19.78          val s_args = map assemble_arg args';
   19.79 @@ -370,17 +370,17 @@
   19.80            | SOME default_rhs =>
   19.81                [([ml_list (rev (dicts @ map2 ml_as default_args s_args))], s_rhs),
   19.82                  ([ml_list (rev (dicts @ default_args))], default_rhs)]
   19.83 -      in (nbe_fun idx_of i c, eqns) end;
   19.84 +      in (nbe_fun idx_of i sym, eqns) end;
   19.85  
   19.86 -    fun assemble_eqns (c, (num_args, (dicts, eqns))) =
   19.87 +    fun assemble_eqns (sym, (num_args, (dicts, eqns))) =
   19.88        let
   19.89          val default_args = map nbe_default
   19.90            (Name.invent Name.context "a" (num_args - length dicts));
   19.91 -        val eqns' = map_index (assemble_eqn c dicts default_args) eqns
   19.92 -          @ (if c = "" then [] else [(nbe_fun idx_of (length eqns) c,
   19.93 +        val eqns' = map_index (assemble_eqn sym dicts default_args) eqns
   19.94 +          @ (if Code_Symbol.is_value sym then [] else [(nbe_fun idx_of (length eqns) sym,
   19.95              [([ml_list (rev (dicts @ default_args))],
   19.96 -              nbe_apps_constr idx_of c (dicts @ default_args))])]);
   19.97 -      in (eqns', nbe_abss num_args (nbe_fun idx_of 0 c)) end;
   19.98 +              nbe_apps_constr idx_of sym (dicts @ default_args))])]);
   19.99 +      in (eqns', nbe_abss num_args (nbe_fun idx_of 0 sym)) end;
  19.100  
  19.101      val (fun_vars, fun_vals) = map_split assemble_eqns eqnss';
  19.102      val deps_vars = ml_list (map (nbe_fun idx_of 0) deps);
  19.103 @@ -394,9 +394,9 @@
  19.104        let
  19.105          val ctxt = Proof_Context.init_global thy;
  19.106          val (deps, deps_vals) = split_list (map_filter
  19.107 -          (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Graph.get_node nbe_program dep)))) raw_deps);
  19.108 +          (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Code_Symbol.Graph.get_node nbe_program dep)))) raw_deps);
  19.109          val idx_of = raw_deps
  19.110 -          |> map (fn dep => (dep, snd (Graph.get_node nbe_program dep)))
  19.111 +          |> map (fn dep => (dep, snd (Code_Symbol.Graph.get_node nbe_program dep)))
  19.112            |> AList.lookup (op =)
  19.113            |> (fn f => the o f);
  19.114          val s = assemble_eqnss idx_of deps eqnss;
  19.115 @@ -413,45 +413,45 @@
  19.116  
  19.117  (* extract equations from statements *)
  19.118  
  19.119 -fun dummy_const c dss =
  19.120 -  IConst { name = c, typargs = [], dicts = dss,
  19.121 +fun dummy_const sym dss =
  19.122 +  IConst { sym = sym, typargs = [], dicts = dss,
  19.123      dom = [], range = ITyVar "", annotate = false };
  19.124  
  19.125 -fun eqns_of_stmt (_, Code_Thingol.NoStmt _) =
  19.126 +fun eqns_of_stmt (_, Code_Thingol.NoStmt) =
  19.127        []
  19.128 -  | eqns_of_stmt (_, Code_Thingol.Fun (_, ((_, []), _))) =
  19.129 +  | eqns_of_stmt (_, Code_Thingol.Fun ((_, []), _)) =
  19.130        []
  19.131 -  | eqns_of_stmt (const, Code_Thingol.Fun (_, (((vs, _), eqns), _))) =
  19.132 -      [(const, (vs, map fst eqns))]
  19.133 +  | eqns_of_stmt (sym_const, Code_Thingol.Fun (((vs, _), eqns), _)) =
  19.134 +      [(sym_const, (vs, map fst eqns))]
  19.135    | eqns_of_stmt (_, Code_Thingol.Datatypecons _) =
  19.136        []
  19.137    | eqns_of_stmt (_, Code_Thingol.Datatype _) =
  19.138        []
  19.139 -  | eqns_of_stmt (class, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
  19.140 +  | eqns_of_stmt (sym_class, Code_Thingol.Class (v, (classrels, classparams))) =
  19.141        let
  19.142 -        val names = map snd super_classes @ map fst classparams;
  19.143 -        val params = Name.invent Name.context "d" (length names);
  19.144 -        fun mk (k, name) =
  19.145 -          (name, ([(v, [])],
  19.146 -            [([dummy_const class [] `$$ map (IVar o SOME) params],
  19.147 +        val syms = map Code_Symbol.Class_Relation classrels @ map (Code_Symbol.Constant o fst) classparams;
  19.148 +        val params = Name.invent Name.context "d" (length syms);
  19.149 +        fun mk (k, sym) =
  19.150 +          (sym, ([(v, [])],
  19.151 +            [([dummy_const sym_class [] `$$ map (IVar o SOME) params],
  19.152                IVar (SOME (nth params k)))]));
  19.153 -      in map_index mk names end
  19.154 +      in map_index mk syms end
  19.155    | eqns_of_stmt (_, Code_Thingol.Classrel _) =
  19.156        []
  19.157    | eqns_of_stmt (_, Code_Thingol.Classparam _) =
  19.158        []
  19.159 -  | eqns_of_stmt (inst, Code_Thingol.Classinst { class, vs, superinsts, inst_params, ... }) =
  19.160 -      [(inst, (vs, [([], dummy_const class [] `$$
  19.161 -        map (fn (_, (_, (inst, dss))) => dummy_const inst dss) superinsts
  19.162 +  | eqns_of_stmt (sym_inst, Code_Thingol.Classinst { class, tyco, vs, superinsts, inst_params, ... }) =
  19.163 +      [(sym_inst, (vs, [([], dummy_const (Code_Symbol.Type_Class class) [] `$$
  19.164 +        map (fn (class, dss) => dummy_const (Code_Symbol.Class_Instance (tyco, class)) dss) superinsts
  19.165          @ map (IConst o fst o snd o fst) inst_params)]))];
  19.166  
  19.167  
  19.168  (* compile whole programs *)
  19.169  
  19.170  fun ensure_const_idx name (nbe_program, (maxidx, idx_tab)) =
  19.171 -  if can (Graph.get_node nbe_program) name
  19.172 +  if can (Code_Symbol.Graph.get_node nbe_program) name
  19.173    then (nbe_program, (maxidx, idx_tab))
  19.174 -  else (Graph.new_node (name, (NONE, maxidx)) nbe_program,
  19.175 +  else (Code_Symbol.Graph.new_node (name, (NONE, maxidx)) nbe_program,
  19.176      (maxidx + 1, Inttab.update_new (maxidx, name) idx_tab));
  19.177  
  19.178  fun compile_stmts thy stmts_deps =
  19.179 @@ -468,20 +468,20 @@
  19.180        |> rpair nbe_program;
  19.181    in
  19.182      fold ensure_const_idx refl_deps
  19.183 -    #> apfst (fold (fn (name, deps) => fold (curry Graph.add_edge name) deps) names_deps
  19.184 +    #> apfst (fold (fn (name, deps) => fold (curry Code_Symbol.Graph.add_edge name) deps) names_deps
  19.185        #> compile
  19.186 -      #-> fold (fn (name, univ) => (Graph.map_node name o apfst) (K (SOME univ))))
  19.187 +      #-> fold (fn (name, univ) => (Code_Symbol.Graph.map_node name o apfst) (K (SOME univ))))
  19.188    end;
  19.189  
  19.190  fun compile_program thy program =
  19.191    let
  19.192 -    fun add_stmts names (nbe_program, (maxidx, idx_tab)) = if exists ((can o Graph.get_node) nbe_program) names
  19.193 +    fun add_stmts names (nbe_program, (maxidx, idx_tab)) = if exists ((can o Code_Symbol.Graph.get_node) nbe_program) names
  19.194        then (nbe_program, (maxidx, idx_tab))
  19.195        else (nbe_program, (maxidx, idx_tab))
  19.196 -        |> compile_stmts thy (map (fn name => ((name, Graph.get_node program name),
  19.197 -          Graph.immediate_succs program name)) names);
  19.198 +        |> compile_stmts thy (map (fn name => ((name, Code_Symbol.Graph.get_node program name),
  19.199 +          Code_Symbol.Graph.immediate_succs program name)) names);
  19.200    in
  19.201 -    fold_rev add_stmts (Graph.strong_conn program)
  19.202 +    fold_rev add_stmts (Code_Symbol.Graph.strong_conn program)
  19.203    end;
  19.204  
  19.205  
  19.206 @@ -493,7 +493,7 @@
  19.207    let 
  19.208      val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs;
  19.209    in
  19.210 -    ("", (vs, [([], t)]))
  19.211 +    (Code_Symbol.value, (vs, [([], t)]))
  19.212      |> singleton (compile_eqnss thy nbe_program deps)
  19.213      |> snd
  19.214      |> (fn t => apps t (rev dict_frees))
  19.215 @@ -502,43 +502,35 @@
  19.216  
  19.217  (* reconstruction *)
  19.218  
  19.219 -fun typ_of_itype program vs (ityco `%% itys) =
  19.220 -      let
  19.221 -        val Code_Thingol.Datatype (tyco, _) = Graph.get_node program ityco;
  19.222 -      in Type (tyco, map (typ_of_itype program vs) itys) end
  19.223 -  | typ_of_itype program vs (ITyVar v) =
  19.224 -      let
  19.225 -        val sort = (the o AList.lookup (op =) vs) v;
  19.226 -      in TFree ("'" ^ v, sort) end;
  19.227 +fun typ_of_itype vs (tyco `%% itys) =
  19.228 +      Type (tyco, map (typ_of_itype vs) itys)
  19.229 +  | typ_of_itype vs (ITyVar v) =
  19.230 +      TFree ("'" ^ v, (the o AList.lookup (op =) vs) v);
  19.231  
  19.232 -fun term_of_univ thy program idx_tab t =
  19.233 +fun term_of_univ thy idx_tab t =
  19.234    let
  19.235      fun take_until f [] = []
  19.236 -      | take_until f (x::xs) = if f x then [] else x :: take_until f xs;
  19.237 -    fun is_dict (Const (idx, _)) = (case (Graph.get_node program o the o Inttab.lookup idx_tab) idx
  19.238 -         of Code_Thingol.Class _ => true
  19.239 -          | Code_Thingol.Classrel _ => true
  19.240 -          | Code_Thingol.Classinst _ => true
  19.241 -          | _ => false)
  19.242 +      | take_until f (x :: xs) = if f x then [] else x :: take_until f xs;
  19.243 +    fun is_dict (Const (idx, _)) =
  19.244 +          (case Inttab.lookup idx_tab idx of
  19.245 +            SOME (Code_Symbol.Constant _) => false
  19.246 +          | _ => true)
  19.247        | is_dict (DFree _) = true
  19.248        | is_dict _ = false;
  19.249 -    fun const_of_idx idx = (case (Graph.get_node program o the o Inttab.lookup idx_tab) idx
  19.250 -     of Code_Thingol.NoStmt c => c
  19.251 -      | Code_Thingol.Fun (c, _) => c
  19.252 -      | Code_Thingol.Datatypecons (c, _) => c
  19.253 -      | Code_Thingol.Classparam (c, _) => c);
  19.254 +    fun const_of_idx idx =
  19.255 +      case Inttab.lookup idx_tab idx of SOME (Code_Symbol.Constant const) => const;
  19.256      fun of_apps bounds (t, ts) =
  19.257        fold_map (of_univ bounds) ts
  19.258        #>> (fn ts' => list_comb (t, rev ts'))
  19.259      and of_univ bounds (Const (idx, ts)) typidx =
  19.260            let
  19.261              val ts' = take_until is_dict ts;
  19.262 -            val c = const_of_idx idx;
  19.263 +            val const = const_of_idx idx;
  19.264              val T = map_type_tvar (fn ((v, i), _) =>
  19.265                Type_Infer.param typidx (v ^ string_of_int i, []))
  19.266 -                (Sign.the_const_type thy c);
  19.267 +                (Sign.the_const_type thy const);
  19.268              val typidx' = typidx + 1;
  19.269 -          in of_apps bounds (Term.Const (c, T), ts') typidx' end
  19.270 +          in of_apps bounds (Term.Const (const, T), ts') typidx' end
  19.271        | of_univ bounds (BVar (n, ts)) typidx =
  19.272            of_apps bounds (Bound (bounds - n - 1), ts) typidx
  19.273        | of_univ bounds (t as Abs _) typidx =
  19.274 @@ -550,11 +542,11 @@
  19.275  
  19.276  (* evaluation with type reconstruction *)
  19.277  
  19.278 -fun eval_term thy program (nbe_program, idx_tab) ((vs0, (vs, ty)), t) deps =
  19.279 +fun eval_term thy (nbe_program, idx_tab) ((vs0, (vs, ty)), t) deps =
  19.280    let
  19.281      val ctxt = Syntax.init_pretty_global thy;
  19.282      val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
  19.283 -    val ty' = typ_of_itype program vs0 ty;
  19.284 +    val ty' = typ_of_itype vs0 ty;
  19.285      fun type_infer t =
  19.286        Syntax.check_term (Config.put Type_Infer_Context.const_sorts false ctxt)
  19.287          (Type.constraint ty' t);
  19.288 @@ -563,7 +555,7 @@
  19.289        else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);
  19.290    in
  19.291      compile_term thy nbe_program deps (vs, t)
  19.292 -    |> term_of_univ thy program idx_tab
  19.293 +    |> term_of_univ thy idx_tab
  19.294      |> traced (fn t => "Normalized:\n" ^ string_of_term t)
  19.295      |> type_infer
  19.296      |> traced (fn t => "Types inferred:\n" ^ string_of_term t)
  19.297 @@ -576,8 +568,8 @@
  19.298  
  19.299  structure Nbe_Functions = Code_Data
  19.300  (
  19.301 -  type T = (Univ option * int) Graph.T * (int * string Inttab.table);
  19.302 -  val empty = (Graph.empty, (0, Inttab.empty));
  19.303 +  type T = (Univ option * int) Code_Symbol.Graph.T * (int * Code_Symbol.symbol Inttab.table);
  19.304 +  val empty = (Code_Symbol.Graph.empty, (0, Inttab.empty));
  19.305  );
  19.306  
  19.307  fun compile ignore_cache thy program =
  19.308 @@ -599,26 +591,23 @@
  19.309  
  19.310  val (_, raw_oracle) = Context.>>> (Context.map_theory_result
  19.311    (Thm.add_oracle (@{binding normalization_by_evaluation},
  19.312 -    fn (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct) =>
  19.313 -      mk_equals thy ct (eval_term thy program nbe_program_idx_tab vsp_ty_t deps))));
  19.314 +    fn (thy, nbe_program_idx_tab, vsp_ty_t, deps, ct) =>
  19.315 +      mk_equals thy ct (eval_term thy nbe_program_idx_tab vsp_ty_t deps))));
  19.316  
  19.317 -fun oracle thy program nbe_program_idx_tab vsp_ty_t deps ct =
  19.318 -  raw_oracle (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct);
  19.319 +fun oracle thy nbe_program_idx_tab vsp_ty_t deps ct =
  19.320 +  raw_oracle (thy, nbe_program_idx_tab, vsp_ty_t, deps, ct);
  19.321  
  19.322 -fun dynamic_conv thy = lift_triv_classes_conv thy (Code_Thingol.dynamic_conv thy
  19.323 -    (K (fn program => oracle thy program (compile false thy program))));
  19.324 +fun dynamic_conv thy = lift_triv_classes_conv thy
  19.325 +  (Code_Thingol.dynamic_conv thy (oracle thy o compile false thy));
  19.326  
  19.327  fun dynamic_value thy = lift_triv_classes_rew thy
  19.328 -  (Code_Thingol.dynamic_value thy I
  19.329 -    (K (fn program => eval_term thy program (compile false thy program))));
  19.330 +  (Code_Thingol.dynamic_value thy I (eval_term thy o compile false thy));
  19.331  
  19.332 -fun static_conv thy consts =
  19.333 -  lift_triv_classes_conv thy (Code_Thingol.static_conv thy consts
  19.334 -    (K (fn program => fn _ => oracle thy program (compile true thy program))));
  19.335 +fun static_conv thy consts = lift_triv_classes_conv thy
  19.336 +  (Code_Thingol.static_conv thy consts (K o oracle thy o compile true thy));
  19.337  
  19.338  fun static_value thy consts = lift_triv_classes_rew thy
  19.339 -  (Code_Thingol.static_value thy I consts
  19.340 -    (K (fn program => fn _ => eval_term thy program (compile true thy program))));
  19.341 +  (Code_Thingol.static_value thy I consts (K o eval_term thy o compile true thy));
  19.342  
  19.343  
  19.344  (** setup **)